max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat: simplify Coe again

Browse source 
Users may add the expensive instances if they want.
The goal is to make sure the default configuration is solid, and
covers all examples we really want to support.

cc @kha @dselsam
This commit is contained in:
Leonardo de Moura 2020-01-29 22:08:42 -08:00
parent 812c47d463
commit 0c4030137f
2 changed files with 26 additions and 31 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

55
src/Init/Coe.lean
View file

@ -12,12 +12,9 @@ universes u v w w'
class Coe (α : Sort u) (β : Sort v) :=
(coe : α → β)
class CoeDep (α : Sort u) (a : α) (β : Sort v) :=
(coe : β)
/-- Auxiliary class that contains the transitive closure of `Coe` and `CoeDep`. -/
class CoeTC (α : Sort u) (a : α) (β : Sort v) :=
(coe : β)
/-- Auxiliary class that contains the transitive closure of `Coe`. -/
class CoeTC (α : Sort u) (β : Sort v) :=
(coe : α → β)
/- Expensive coercion that can only appear at the beggining of a sequence of coercions. -/
class CoeHead (α : Sort u) (β : Sort v) :=
@ -27,7 +24,10 @@ class CoeHead (α : Sort u) (β : Sort v) :=
class CoeTail (α : Sort u) (β : Sort v) :=
(coe : α → β)
/- CoeHead + CoeTC + CoeTail -/
class CoeDep (α : Sort u) (a : α) (β : Sort v) :=
(coe : β)
/- Combines CoeHead, CoeTC, CoeTail, CoeDep -/
class CoeT (α : Sort u) (a : α) (β : Sort v) :=
(coe : β)
@ -37,20 +37,20 @@ class CoeFun (α : Sort u) (γ : outParam (α → outParam (Sort v))) :=
class CoeSort (α : Sort u) (β : outParam (Sort v)) :=
(coe : α → β)
abbrev coeB {α : Sort u} {β : Sort v} (a : α) [Coe α β] : β :=
abbrev coeB {α : Sort u} {β : Sort v} [Coe α β] (a : α) : β :=
@Coe.coe α β _ a
abbrev coeHead {α : Sort u} {β : Sort v} (a : α) [CoeHead α β] : β :=
abbrev coeHead {α : Sort u} {β : Sort v} [CoeHead α β] (a : α) : β :=
@CoeHead.coe α β _ a
abbrev coeTail {α : Sort u} {β : Sort v} (a : α) [CoeTail α β] : β :=
abbrev coeTail {α : Sort u} {β : Sort v} [CoeTail α β] (a : α) : β :=
@CoeTail.coe α β _ a
abbrev coeD {α : Sort u} {β : Sort v} (a : α) [CoeDep α a β] : β :=
@CoeDep.coe α a β _
abbrev coeTC {α : Sort u} {β : Sort v} (a : α) [CoeTC α a β] : β :=
@CoeTC.coe α a β _
abbrev coeTC {α : Sort u} {β : Sort v} [CoeTC α β] (a : α) : β :=
@CoeTC.coe α β _ a
/-- Apply coercion manually. -/
abbrev coe {α : Sort u} {β : Sort v} (a : α) [CoeT α a β] : β :=
@ -62,27 +62,19 @@ abbrev coeFun {α : Sort u} {γ : α → Sort v} (a : α) [CoeFun α γ] : γ a
abbrev coeSort {α : Sort u} {β : Sort v} (a : α) [CoeSort α β] : β :=
@CoeSort.coe α β _ a
instance coeDepTrans {α : Sort u} {β : Sort v} {δ : Sort w} (a : α) [CoeTC α a β] [CoeDep β (coeTC a) δ] : CoeTC α a δ :=
{ coe := coeD (coeTC a : β) }
instance coeTrans {α : Sort u} {β : Sort v} {δ : Sort w} [CoeTC α β] [Coe β δ] : CoeTC α δ :=
{ coe := fun a => coeB (coeTC a : β) }
instance coeTrans {α : Sort u} {β : Sort v} {δ : Sort w} (a : α) [CoeTC α a β] [Coe β δ] : CoeTC α a δ :=
{ coe := coeB (coeTC a : β) }
instance coeBase {α : Sort u} {β : Sort v} [Coe α β] : CoeTC α β :=
{ coe := fun a => coeB a }
instance coeBase {α : Sort u} {β : Sort v} (a : α) [Coe α β] : CoeTC α a β :=
{ coe := coeB a }
instance coeDepBase {α : Sort u} {β : Sort v} (a : α) [CoeDep α a β] : CoeTC α a β :=
{ coe := coeD a }
@[inferTCGoalsLR]
instance coeOfHeafOfTCOfTail {α : Sort u} {β : Sort v} {δ : Sort w} {γ : Sort w'} (a : α) [CoeHead α β] [CoeTail δ γ] [CoeTC β (coeHead a) δ] : CoeT α a γ :=
instance coeOfHeafOfTCOfTail {α : Sort u} {β : Sort v} {δ : Sort w} {γ : Sort w'} (a : α) [CoeTC β δ] [CoeTail δ γ] [CoeHead α β] : CoeT α a γ :=
{ coe := coeTail (coeTC (coeHead a : β) : δ) }
@[inferTCGoalsLR]
instance coeOfHeadOfTC {α : Sort u} {β : Sort v} {δ : Sort w} (a : α) [CoeHead α β] [CoeTC β (coeHead a) δ] : CoeT α a δ :=
instance coeOfHeadOfTC {α : Sort u} {β : Sort v} {δ : Sort w} (a : α) [CoeTC β δ] [CoeHead α β] : CoeT α a δ :=
{ coe := coeTC (coeHead a : β) }
instance coeOfTCOfTail {α : Sort u} {β : Sort v} {δ : Sort w} (a : α) [CoeTC α a β] [CoeTail β δ] : CoeT α a δ :=
instance coeOfTCOfTail {α : Sort u} {β : Sort v} {δ : Sort w} (a : α) [CoeTC α β] [CoeTail β δ] : CoeT α a δ :=
{ coe := coeTail (coeTC a : β) }
instance coeOfHead {α : Sort u} {β : Sort v} (a : α) [CoeHead α β] : CoeT α a β :=
@ -91,13 +83,16 @@ instance coeOfHead {α : Sort u} {β : Sort v} (a : α) [CoeHead α β] : CoeT
instance coeOfTail {α : Sort u} {β : Sort v} (a : α) [CoeTail α β] : CoeT α a β :=
{ coe := coeTail a }
instance coeOfTC {α : Sort u} {β : Sort v} (a : α) [CoeTC α a β] : CoeT α a β :=
instance coeOfTC {α : Sort u} {β : Sort v} (a : α) [CoeTC α β] : CoeT α a β :=
{ coe := coeTC a }
instance coeFunTrans {α : Sort u} {β : Sort v} {γ : β → Sort w} [Coe α β] [CoeFun β γ] : CoeFun α (fun a => γ (coe a)) :=
instance coeOfDep {α : Sort u} {β : Sort v} (a : α) [CoeDep α a β] : CoeT α a β :=
{ coe := coeD a }
instance coeFunTrans {α : Sort u} {β : Sort v} {γ : β → Sort w} [CoeFun β γ] [Coe α β] : CoeFun α (fun a => γ (coe a)) :=
{ coe := fun a => coeFun (coeB a : β) }
instance coeSortTrans {α : Sort u} {β : Sort v} {δ : Sort w} [Coe α β] [CoeSort β δ] : CoeSort α δ :=
instance coeSortTrans {α : Sort u} {β : Sort v} {δ : Sort w} [CoeSort β δ] [Coe α β] : CoeSort α δ :=
{ coe := fun a => coeSort (coeB a : β) }
/- Basic instances -/

2
tests/lean/run/CoeNew.lean
View file

@ -22,7 +22,7 @@ set_option pp.implicit true
#synth CoeT { x : Nat // x > 0 } ⟨1, sorryAx _⟩ Bool
#synth CoeT Nat 0 (Option Nat)
#synth CoeT Bool true (Option Nat)
#synth CoeT Prop (0 = 1) Nat
#synth CoeT Prop (0 = 1) Bool
#synth CoeT Bool true (Option Nat)
def f (c : ConstantFunction Nat Nat) : Nat :=