From 0ab38742dbfff04f9c77d3de12952e83c4fd96f7 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 24 Oct 2020 06:18:01 -0700 Subject: [PATCH] chore: cleanup --- src/Lean/Expr.lean | 868 +++++++++++++++--------------- src/Lean/InternalExceptionId.lean | 28 +- src/Lean/KeyedDeclsAttribute.lean | 180 +++---- src/Lean/Level.lean | 402 +++++++------- src/Lean/Modifiers.lean | 42 +- src/Lean/MonadEnv.lean | 114 ++-- src/Lean/PrettyPrinter.lean | 50 +- src/Lean/ProjFns.lean | 46 +- src/Lean/ReducibilityAttrs.lean | 20 +- src/Lean/ResolveName.lean | 185 +++---- 10 files changed, 967 insertions(+), 968 deletions(-) diff --git a/src/Lean/Expr.lean b/src/Lean/Expr.lean index 242b2a50fc..57a674be39 100644 --- a/src/Lean/Expr.lean +++ b/src/Lean/Expr.lean @@ -10,70 +10,70 @@ import Lean.Level namespace Lean inductive Literal -| natVal (val : Nat) -| strVal (val : String) + | natVal (val : Nat) + | strVal (val : String) instance : Inhabited Literal := ⟨Literal.natVal 0⟩ protected def Literal.hash : Literal → USize -| Literal.natVal v => hash v -| Literal.strVal v => hash v + | Literal.natVal v => hash v + | Literal.strVal v => hash v instance : Hashable Literal := ⟨Literal.hash⟩ def Literal.beq : Literal → Literal → Bool -| Literal.natVal v₁, Literal.natVal v₂ => v₁ == v₂ -| Literal.strVal v₁, Literal.strVal v₂ => v₁ == v₂ -| _, _ => false + | Literal.natVal v₁, Literal.natVal v₂ => v₁ == v₂ + | Literal.strVal v₁, Literal.strVal v₂ => v₁ == v₂ + | _, _ => false instance : HasBeq Literal := ⟨Literal.beq⟩ def Literal.lt : Literal → Literal → Bool -| Literal.natVal _, Literal.strVal _ => true -| Literal.natVal v₁, Literal.natVal v₂ => v₁ < v₂ -| Literal.strVal v₁, Literal.strVal v₂ => v₁ < v₂ -| _, _ => false + | Literal.natVal _, Literal.strVal _ => true + | Literal.natVal v₁, Literal.natVal v₂ => v₁ < v₂ + | Literal.strVal v₁, Literal.strVal v₂ => v₁ < v₂ + | _, _ => false instance : HasLess Literal := ⟨fun a b => a.lt b⟩ instance (a b : Literal) : Decidable (a < b) := -inferInstanceAs (Decidable (a.lt b)) + inferInstanceAs (Decidable (a.lt b)) inductive BinderInfo -| default | implicit | strictImplicit | instImplicit | auxDecl + | default | implicit | strictImplicit | instImplicit | auxDecl def BinderInfo.hash : BinderInfo → USize -| BinderInfo.default => 947 -| BinderInfo.implicit => 1019 -| BinderInfo.strictImplicit => 1087 -| BinderInfo.instImplicit => 1153 -| BinderInfo.auxDecl => 1229 + | BinderInfo.default => 947 + | BinderInfo.implicit => 1019 + | BinderInfo.strictImplicit => 1087 + | BinderInfo.instImplicit => 1153 + | BinderInfo.auxDecl => 1229 def BinderInfo.isExplicit : BinderInfo → Bool -| BinderInfo.implicit => false -| BinderInfo.strictImplicit => false -| BinderInfo.instImplicit => false -| _ => true + | BinderInfo.implicit => false + | BinderInfo.strictImplicit => false + | BinderInfo.instImplicit => false + | _ => true instance : Hashable BinderInfo := ⟨BinderInfo.hash⟩ instance : Inhabited BinderInfo := ⟨BinderInfo.default⟩ def BinderInfo.isInstImplicit : BinderInfo → Bool -| BinderInfo.instImplicit => true -| _ => false + | BinderInfo.instImplicit => true + | _ => false def BinderInfo.isAuxDecl : BinderInfo → Bool -| BinderInfo.auxDecl => true -| _ => false + | BinderInfo.auxDecl => true + | _ => false protected def BinderInfo.beq : BinderInfo → BinderInfo → Bool -| BinderInfo.default, BinderInfo.default => true -| BinderInfo.implicit, BinderInfo.implicit => true -| BinderInfo.strictImplicit, BinderInfo.strictImplicit => true -| BinderInfo.instImplicit, BinderInfo.instImplicit => true -| BinderInfo.auxDecl, BinderInfo.auxDecl => true -| _, _ => false + | BinderInfo.default, BinderInfo.default => true + | BinderInfo.implicit, BinderInfo.implicit => true + | BinderInfo.strictImplicit, BinderInfo.strictImplicit => true + | BinderInfo.instImplicit, BinderInfo.instImplicit => true + | BinderInfo.auxDecl, BinderInfo.auxDecl => true + | _, _ => false instance : HasBeq BinderInfo := ⟨BinderInfo.beq⟩ @@ -93,74 +93,74 @@ abbrev MData.empty : MData := {} def Expr.Data := UInt64 instance: Inhabited Expr.Data := -inferInstanceAs (Inhabited UInt64) + inferInstanceAs (Inhabited UInt64) def Expr.Data.hash (c : Expr.Data) : USize := -c.toUInt32.toUSize + c.toUInt32.toUSize instance : HasBeq Expr.Data := -⟨fun (a b : UInt64) => a == b⟩ + ⟨fun (a b : UInt64) => a == b⟩ def Expr.Data.looseBVarRange (c : Expr.Data) : UInt32 := -(c.shiftRight 40).toUInt32 + (c.shiftRight 40).toUInt32 def Expr.Data.hasFVar (c : Expr.Data) : Bool := -((c.shiftRight 32).land 1) == 1 + ((c.shiftRight 32).land 1) == 1 def Expr.Data.hasExprMVar (c : Expr.Data) : Bool := -((c.shiftRight 33).land 1) == 1 + ((c.shiftRight 33).land 1) == 1 def Expr.Data.hasLevelMVar (c : Expr.Data) : Bool := -((c.shiftRight 34).land 1) == 1 + ((c.shiftRight 34).land 1) == 1 def Expr.Data.hasLevelParam (c : Expr.Data) : Bool := -((c.shiftRight 35).land 1) == 1 + ((c.shiftRight 35).land 1) == 1 def Expr.Data.nonDepLet (c : Expr.Data) : Bool := -((c.shiftRight 36).land 1) == 1 + ((c.shiftRight 36).land 1) == 1 @[extern c inline "(uint8_t)((#1 << 24) >> 61)"] def Expr.Data.binderInfo (c : Expr.Data) : BinderInfo := -let bi := (c.shiftLeft 24).shiftRight 61 -if bi == 0 then BinderInfo.default -else if bi == 1 then BinderInfo.implicit -else if bi == 2 then BinderInfo.strictImplicit -else if bi == 3 then BinderInfo.instImplicit -else BinderInfo.auxDecl + let bi := (c.shiftLeft 24).shiftRight 61 + if bi == 0 then BinderInfo.default + else if bi == 1 then BinderInfo.implicit + else if bi == 2 then BinderInfo.strictImplicit + else if bi == 3 then BinderInfo.instImplicit + else BinderInfo.auxDecl @[extern c inline "(uint64_t)#1"] def BinderInfo.toUInt64 : BinderInfo → UInt64 -| BinderInfo.default => 0 -| BinderInfo.implicit => 1 -| BinderInfo.strictImplicit => 2 -| BinderInfo.instImplicit => 3 -| BinderInfo.auxDecl => 4 + | BinderInfo.default => 0 + | BinderInfo.implicit => 1 + | BinderInfo.strictImplicit => 2 + | BinderInfo.instImplicit => 3 + | BinderInfo.auxDecl => 4 @[inline] private def Expr.mkDataCore (h : USize) (looseBVarRange : Nat) (hasFVar hasExprMVar hasLevelMVar hasLevelParam nonDepLet : Bool) (bi : BinderInfo) : Expr.Data := -if looseBVarRange > Nat.pow 2 24 - 1 then panic! "bound variable index is too big" -else - let r : UInt64 := - h.toUInt32.toUInt64 + - hasFVar.toUInt64.shiftLeft 32 + - hasExprMVar.toUInt64.shiftLeft 33 + - hasLevelMVar.toUInt64.shiftLeft 34 + - hasLevelParam.toUInt64.shiftLeft 35 + - nonDepLet.toUInt64.shiftLeft 36 + - bi.toUInt64.shiftLeft 37 + - looseBVarRange.toUInt64.shiftLeft 40 - r + if looseBVarRange > Nat.pow 2 24 - 1 then panic! "bound variable index is too big" + else + let r : UInt64 := + h.toUInt32.toUInt64 + + hasFVar.toUInt64.shiftLeft 32 + + hasExprMVar.toUInt64.shiftLeft 33 + + hasLevelMVar.toUInt64.shiftLeft 34 + + hasLevelParam.toUInt64.shiftLeft 35 + + nonDepLet.toUInt64.shiftLeft 36 + + bi.toUInt64.shiftLeft 37 + + looseBVarRange.toUInt64.shiftLeft 40 + r def Expr.mkData (h : USize) (looseBVarRange : Nat := 0) (hasFVar hasExprMVar hasLevelMVar hasLevelParam : Bool := false) : Expr.Data := -Expr.mkDataCore h looseBVarRange hasFVar hasExprMVar hasLevelMVar hasLevelParam false BinderInfo.default + Expr.mkDataCore h looseBVarRange hasFVar hasExprMVar hasLevelMVar hasLevelParam false BinderInfo.default def Expr.mkDataForBinder (h : USize) (looseBVarRange : Nat) (hasFVar hasExprMVar hasLevelMVar hasLevelParam : Bool) (bi : BinderInfo) : Expr.Data := -Expr.mkDataCore h looseBVarRange hasFVar hasExprMVar hasLevelMVar hasLevelParam false bi + Expr.mkDataCore h looseBVarRange hasFVar hasExprMVar hasLevelMVar hasLevelParam false bi def Expr.mkDataForLet (h : USize) (looseBVarRange : Nat) (hasFVar hasExprMVar hasLevelMVar hasLevelParam nonDepLet : Bool) : Expr.Data := -Expr.mkDataCore h looseBVarRange hasFVar hasExprMVar hasLevelMVar hasLevelParam nonDepLet BinderInfo.default + Expr.mkDataCore h looseBVarRange hasFVar hasExprMVar hasLevelMVar hasLevelParam nonDepLet BinderInfo.default open Expr @@ -170,82 +170,82 @@ abbrev FVarId := Name /- We use the `E` suffix (short for `Expr`) to avoid collision with keywords. We considered using «...», but it is too inconvenient to use. -/ inductive Expr -| bvar : Nat → Data → Expr -- bound variables -| fvar : FVarId → Data → Expr -- free variables -| mvar : MVarId → Data → Expr -- meta variables -| sort : Level → Data → Expr -- Sort -| const : Name → List Level → Data → Expr -- constants -| app : Expr → Expr → Data → Expr -- application -| lam : Name → Expr → Expr → Data → Expr -- lambda abstraction -| forallE : Name → Expr → Expr → Data → Expr -- (dependent) arrow -| letE : Name → Expr → Expr → Expr → Data → Expr -- let expressions -| lit : Literal → Data → Expr -- literals -| mdata : MData → Expr → Data → Expr -- metadata -| proj : Name → Nat → Expr → Data → Expr -- projection --- IMPORTANT: the following constructor will be deleted -| localE : Name → Name → Expr → Data → Expr -- Lean2 legacy. TODO: delete + | bvar : Nat → Data → Expr -- bound variables + | fvar : FVarId → Data → Expr -- free variables + | mvar : MVarId → Data → Expr -- meta variables + | sort : Level → Data → Expr -- Sort + | const : Name → List Level → Data → Expr -- constants + | app : Expr → Expr → Data → Expr -- application + | lam : Name → Expr → Expr → Data → Expr -- lambda abstraction + | forallE : Name → Expr → Expr → Data → Expr -- (dependent) arrow + | letE : Name → Expr → Expr → Expr → Data → Expr -- let expressions + | lit : Literal → Data → Expr -- literals + | mdata : MData → Expr → Data → Expr -- metadata + | proj : Name → Nat → Expr → Data → Expr -- projection + -- IMPORTANT: the following constructor will be deleted + | localE : Name → Name → Expr → Data → Expr -- Lean2 legacy. TODO: delete namespace Expr instance : Inhabited Expr := -⟨sort (arbitrary _) (arbitrary _)⟩ + ⟨sort (arbitrary _) (arbitrary _)⟩ @[inline] def data : Expr → Data -| bvar _ d => d -| fvar _ d => d -| mvar _ d => d -| sort _ d => d -| const _ _ d => d -| app _ _ d => d -| lam _ _ _ d => d -| forallE _ _ _ d => d -| letE _ _ _ _ d => d -| lit _ d => d -| mdata _ _ d => d -| proj _ _ _ d => d -| localE _ _ _ d => d + | bvar _ d => d + | fvar _ d => d + | mvar _ d => d + | sort _ d => d + | const _ _ d => d + | app _ _ d => d + | lam _ _ _ d => d + | forallE _ _ _ d => d + | letE _ _ _ _ d => d + | lit _ d => d + | mdata _ _ d => d + | proj _ _ _ d => d + | localE _ _ _ d => d def ctorName : Expr → String -| bvar _ _ => "bvar" -| fvar _ _ => "fvar" -| mvar _ _ => "mvar" -| sort _ _ => "sort" -| const _ _ _ => "const" -| app _ _ _ => "app" -| lam _ _ _ _ => "lam" -| forallE _ _ _ _ => "forallE" -| letE _ _ _ _ _ => "letE" -| lit _ _ => "lit" -| mdata _ _ _ => "mdata" -| proj _ _ _ _ => "proj" -| localE _ _ _ _ => "localE" + | bvar _ _ => "bvar" + | fvar _ _ => "fvar" + | mvar _ _ => "mvar" + | sort _ _ => "sort" + | const _ _ _ => "const" + | app _ _ _ => "app" + | lam _ _ _ _ => "lam" + | forallE _ _ _ _ => "forallE" + | letE _ _ _ _ _ => "letE" + | lit _ _ => "lit" + | mdata _ _ _ => "mdata" + | proj _ _ _ _ => "proj" + | localE _ _ _ _ => "localE" protected def hash (e : Expr) : USize := -e.data.hash + e.data.hash instance : Hashable Expr := ⟨Expr.hash⟩ def hasFVar (e : Expr) : Bool := -e.data.hasFVar + e.data.hasFVar def hasExprMVar (e : Expr) : Bool := -e.data.hasExprMVar + e.data.hasExprMVar def hasLevelMVar (e : Expr) : Bool := -e.data.hasLevelMVar + e.data.hasLevelMVar def hasMVar (e : Expr) : Bool := -let d := e.data -d.hasExprMVar || d.hasLevelMVar + let d := e.data + d.hasExprMVar || d.hasLevelMVar def hasLevelParam (e : Expr) : Bool := -e.data.hasLevelParam + e.data.hasLevelParam def looseBVarRange (e : Expr) : Nat := -e.data.looseBVarRange.toNat + e.data.looseBVarRange.toNat def binderInfo (e : Expr) : BinderInfo := -e.data.binderInfo + e.data.binderInfo @[export lean_expr_hash] def hashEx : Expr → USize := hash @[export lean_expr_has_fvar] def hasFVarEx : Expr → Bool := hasFVar @@ -259,92 +259,92 @@ e.data.binderInfo end Expr def mkLit (l : Literal) : Expr := -Expr.lit l $ mkData (mixHash 3 (hash l)) + Expr.lit l $ mkData (mixHash 3 (hash l)) def mkNatLit (n : Nat) : Expr := -mkLit (Literal.natVal n) + mkLit (Literal.natVal n) def mkStrLit (s : String) : Expr := -mkLit (Literal.strVal s) + mkLit (Literal.strVal s) def mkConst (n : Name) (lvls : List Level := []) : Expr := -Expr.const n lvls $ mkData (mixHash 5 $ mixHash (hash n) (hash lvls)) 0 false false (lvls.any Level.hasMVar) (lvls.any Level.hasParam) + Expr.const n lvls $ mkData (mixHash 5 $ mixHash (hash n) (hash lvls)) 0 false false (lvls.any Level.hasMVar) (lvls.any Level.hasParam) def Literal.type : Literal → Expr -| Literal.natVal _ => mkConst `Nat -| Literal.strVal _ => mkConst `String + | Literal.natVal _ => mkConst `Nat + | Literal.strVal _ => mkConst `String @[export lean_lit_type] def Literal.typeEx : Literal → Expr := Literal.type def mkBVar (idx : Nat) : Expr := -Expr.bvar idx $ mkData (mixHash 7 $ hash idx) (idx+1) + Expr.bvar idx $ mkData (mixHash 7 $ hash idx) (idx+1) def mkSort (lvl : Level) : Expr := -Expr.sort lvl $ mkData (mixHash 11 $ hash lvl) 0 false false lvl.hasMVar lvl.hasParam + Expr.sort lvl $ mkData (mixHash 11 $ hash lvl) 0 false false lvl.hasMVar lvl.hasParam def mkFVar (fvarId : FVarId) : Expr := -Expr.fvar fvarId $ mkData (mixHash 13 $ hash fvarId) 0 true + Expr.fvar fvarId $ mkData (mixHash 13 $ hash fvarId) 0 true def mkMVar (fvarId : MVarId) : Expr := -Expr.mvar fvarId $ mkData (mixHash 17 $ hash fvarId) 0 false true + Expr.mvar fvarId $ mkData (mixHash 17 $ hash fvarId) 0 false true def mkMData (d : MData) (e : Expr) : Expr := -Expr.mdata d e $ mkData (mixHash 19 $ hash e) e.looseBVarRange e.hasFVar e.hasExprMVar e.hasLevelMVar e.hasLevelParam + Expr.mdata d e $ mkData (mixHash 19 $ hash e) e.looseBVarRange e.hasFVar e.hasExprMVar e.hasLevelMVar e.hasLevelParam def mkProj (s : Name) (i : Nat) (e : Expr) : Expr := -Expr.proj s i e $ mkData (mixHash 23 $ mixHash (hash s) $ mixHash (hash i) (hash e)) - e.looseBVarRange e.hasFVar e.hasExprMVar e.hasLevelMVar e.hasLevelParam + Expr.proj s i e $ mkData (mixHash 23 $ mixHash (hash s) $ mixHash (hash i) (hash e)) + e.looseBVarRange e.hasFVar e.hasExprMVar e.hasLevelMVar e.hasLevelParam def mkApp (f a : Expr) : Expr := -Expr.app f a $ mkData (mixHash 29 $ mixHash (hash f) (hash a)) - (Nat.max f.looseBVarRange a.looseBVarRange) - (f.hasFVar || a.hasFVar) - (f.hasExprMVar || a.hasExprMVar) - (f.hasLevelMVar || a.hasLevelMVar) - (f.hasLevelParam || a.hasLevelParam) + Expr.app f a $ mkData (mixHash 29 $ mixHash (hash f) (hash a)) + (Nat.max f.looseBVarRange a.looseBVarRange) + (f.hasFVar || a.hasFVar) + (f.hasExprMVar || a.hasExprMVar) + (f.hasLevelMVar || a.hasLevelMVar) + (f.hasLevelParam || a.hasLevelParam) def mkLambda (x : Name) (bi : BinderInfo) (t : Expr) (b : Expr) : Expr := --- let x := x.eraseMacroScopes -Expr.lam x t b $ mkDataForBinder (mixHash 31 $ mixHash (hash t) (hash b)) - (Nat.max t.looseBVarRange (b.looseBVarRange - 1)) - (t.hasFVar || b.hasFVar) - (t.hasExprMVar || b.hasExprMVar) - (t.hasLevelMVar || b.hasLevelMVar) - (t.hasLevelParam || b.hasLevelParam) - bi + -- let x := x.eraseMacroScopes + Expr.lam x t b $ mkDataForBinder (mixHash 31 $ mixHash (hash t) (hash b)) + (Nat.max t.looseBVarRange (b.looseBVarRange - 1)) + (t.hasFVar || b.hasFVar) + (t.hasExprMVar || b.hasExprMVar) + (t.hasLevelMVar || b.hasLevelMVar) + (t.hasLevelParam || b.hasLevelParam) + bi def mkForall (x : Name) (bi : BinderInfo) (t : Expr) (b : Expr) : Expr := --- let x := x.eraseMacroScopes -Expr.forallE x t b $ mkDataForBinder (mixHash 37 $ mixHash (hash t) (hash b)) - (Nat.max t.looseBVarRange (b.looseBVarRange - 1)) - (t.hasFVar || b.hasFVar) - (t.hasExprMVar || b.hasExprMVar) - (t.hasLevelMVar || b.hasLevelMVar) - (t.hasLevelParam || b.hasLevelParam) - bi + -- let x := x.eraseMacroScopes + Expr.forallE x t b $ mkDataForBinder (mixHash 37 $ mixHash (hash t) (hash b)) + (Nat.max t.looseBVarRange (b.looseBVarRange - 1)) + (t.hasFVar || b.hasFVar) + (t.hasExprMVar || b.hasExprMVar) + (t.hasLevelMVar || b.hasLevelMVar) + (t.hasLevelParam || b.hasLevelParam) + bi /- Return `Unit -> type`. Do not confuse with `Thunk type` -/ def mkSimpleThunkType (type : Expr) : Expr := -mkForall Name.anonymous BinderInfo.default (Lean.mkConst `Unit) type + mkForall Name.anonymous BinderInfo.default (Lean.mkConst `Unit) type /- Return `fun (_ : Unit), e` -/ def mkSimpleThunk (type : Expr) : Expr := -mkLambda `_ BinderInfo.default (Lean.mkConst `Unit) type + mkLambda `_ BinderInfo.default (Lean.mkConst `Unit) type def mkLet (x : Name) (t : Expr) (v : Expr) (b : Expr) (nonDep : Bool := false) : Expr := --- let x := x.eraseMacroScopes -Expr.letE x t v b $ mkDataForLet (mixHash 41 $ mixHash (hash t) $ mixHash (hash v) (hash b)) - (Nat.max (Nat.max t.looseBVarRange v.looseBVarRange) (b.looseBVarRange - 1)) - (t.hasFVar || v.hasFVar || b.hasFVar) - (t.hasExprMVar || v.hasExprMVar || b.hasExprMVar) - (t.hasLevelMVar || v.hasLevelMVar || b.hasLevelMVar) - (t.hasLevelParam || v.hasLevelParam || b.hasLevelParam) - nonDep + -- let x := x.eraseMacroScopes + Expr.letE x t v b $ mkDataForLet (mixHash 41 $ mixHash (hash t) $ mixHash (hash v) (hash b)) + (Nat.max (Nat.max t.looseBVarRange v.looseBVarRange) (b.looseBVarRange - 1)) + (t.hasFVar || v.hasFVar || b.hasFVar) + (t.hasExprMVar || v.hasExprMVar || b.hasExprMVar) + (t.hasLevelMVar || v.hasLevelMVar || b.hasLevelMVar) + (t.hasLevelParam || v.hasLevelParam || b.hasLevelParam) + nonDep -- TODO: delete def mkLocal (x u : Name) (t : Expr) (bi : BinderInfo) : Expr := -Expr.localE x u t $ mkDataForBinder (mixHash 43 $ hash t) t.looseBVarRange true t.hasExprMVar t.hasLevelMVar t.hasLevelParam bi + Expr.localE x u t $ mkDataForBinder (mixHash 43 $ hash t) t.looseBVarRange true t.hasExprMVar t.hasLevelMVar t.hasLevelParam bi @[export lean_expr_mk_bvar] def mkBVarEx : Nat → Expr := mkBVar @[export lean_expr_mk_fvar] def mkFVarEx : FVarId → Expr := mkFVar @@ -361,252 +361,252 @@ Expr.localE x u t $ mkDataForBinder (mixHash 43 $ hash t) t.looseBVarRange true @[export lean_expr_mk_local] def mkLocalEx : Name → Name → Expr → BinderInfo → Expr := mkLocal def mkAppN (f : Expr) (args : Array Expr) : Expr := -args.foldl mkApp f + args.foldl mkApp f private partial def mkAppRangeAux (n : Nat) (args : Array Expr) (i : Nat) (e : Expr) : Expr := -if i < n then mkAppRangeAux n args (i+1) (mkApp e (args.get! i)) else e + if i < n then mkAppRangeAux n args (i+1) (mkApp e (args.get! i)) else e /-- `mkAppRange f i j #[a_1, ..., a_i, ..., a_j, ... ]` ==> the expression `f a_i ... a_{j-1}` -/ def mkAppRange (f : Expr) (i j : Nat) (args : Array Expr) : Expr := -mkAppRangeAux j args i f + mkAppRangeAux j args i f def mkAppRev (fn : Expr) (revArgs : Array Expr) : Expr := -revArgs.foldr (fun a r => mkApp r a) fn + revArgs.foldr (fun a r => mkApp r a) fn namespace Expr -- TODO: implement it in Lean @[extern "lean_expr_dbg_to_string"] -constant dbgToString (e : @& Expr) : String := arbitrary String +constant dbgToString (e : @& Expr) : String @[extern "lean_expr_quick_lt"] -constant quickLt (a : @& Expr) (b : @& Expr) : Bool := arbitrary _ +constant quickLt (a : @& Expr) (b : @& Expr) : Bool @[extern "lean_expr_lt"] -constant lt (a : @& Expr) (b : @& Expr) : Bool := arbitrary _ +constant lt (a : @& Expr) (b : @& Expr) : Bool /- Return true iff `a` and `b` are alpha equivalent. Binder annotations are ignored. -/ @[extern "lean_expr_eqv"] -constant eqv (a : @& Expr) (b : @& Expr) : Bool := arbitrary _ +constant eqv (a : @& Expr) (b : @& Expr) : Bool instance : HasBeq Expr := ⟨Expr.eqv⟩ /- Return true iff `a` and `b` are equal. Binder names and annotations are taking into account. -/ @[extern "lean_expr_equal"] -constant equal (a : @& Expr) (b : @& Expr) : Bool := arbitrary _ +constant equal (a : @& Expr) (b : @& Expr) : Bool def isSort : Expr → Bool -| sort _ _ => true -| _ => false + | sort _ _ => true + | _ => false def isBVar : Expr → Bool -| bvar _ _ => true -| _ => false + | bvar _ _ => true + | _ => false def isMVar : Expr → Bool -| mvar _ _ => true -| _ => false + | mvar _ _ => true + | _ => false def isFVar : Expr → Bool -| fvar _ _ => true -| _ => false + | fvar _ _ => true + | _ => false def isApp : Expr → Bool -| app _ _ _ => true -| _ => false + | app .. => true + | _ => false def isProj : Expr → Bool -| proj _ _ _ _ => true -| _ => false + | proj .. => true + | _ => false def isConst : Expr → Bool -| const _ _ _ => true -| _ => false + | const .. => true + | _ => false def isConstOf : Expr → Name → Bool -| const n _ _, m => n == m -| _, _ => false + | const n _ _, m => n == m + | _, _ => false def isForall : Expr → Bool -| forallE _ _ _ _ => true -| _ => false + | forallE .. => true + | _ => false def isLambda : Expr → Bool -| lam _ _ _ _ => true -| _ => false + | lam .. => true + | _ => false def isBinding : Expr → Bool -| lam _ _ _ _ => true -| forallE _ _ _ _ => true -| _ => false + | lam .. => true + | forallE .. => true + | _ => false def isLet : Expr → Bool -| letE _ _ _ _ _ => true -| _ => false + | letE .. => true + | _ => false def isMData : Expr → Bool -| mdata _ _ _ => true -| _ => false + | mdata .. => true + | _ => false def isLit : Expr → Bool -| lit _ _ => true -| _ => false + | lit .. => true + | _ => false def getAppFn : Expr → Expr -| app f a _ => getAppFn f -| e => e + | app f a _ => getAppFn f + | e => e def getAppNumArgsAux : Expr → Nat → Nat -| app f a _, n => getAppNumArgsAux f (n+1) -| e, n => n + | app f a _, n => getAppNumArgsAux f (n+1) + | e, n => n def getAppNumArgs (e : Expr) : Nat := -getAppNumArgsAux e 0 + getAppNumArgsAux e 0 private def getAppArgsAux : Expr → Array Expr → Nat → Array Expr -| app f a _, as, i => getAppArgsAux f (as.set! i a) (i-1) -| _, as, _ => as + | app f a _, as, i => getAppArgsAux f (as.set! i a) (i-1) + | _, as, _ => as @[inline] def getAppArgs (e : Expr) : Array Expr := -let dummy := mkSort levelZero -let nargs := e.getAppNumArgs -getAppArgsAux e (mkArray nargs dummy) (nargs-1) + let dummy := mkSort levelZero + let nargs := e.getAppNumArgs + getAppArgsAux e (mkArray nargs dummy) (nargs-1) private def getAppRevArgsAux : Expr → Array Expr → Array Expr -| app f a _, as => getAppRevArgsAux f (as.push a) -| _, as => as + | app f a _, as => getAppRevArgsAux f (as.push a) + | _, as => as @[inline] def getAppRevArgs (e : Expr) : Array Expr := -getAppRevArgsAux e (Array.mkEmpty e.getAppNumArgs) + getAppRevArgsAux e (Array.mkEmpty e.getAppNumArgs) @[specialize] def withAppAux {α} (k : Expr → Array Expr → α) : Expr → Array Expr → Nat → α -| app f a _, as, i => withAppAux k f (as.set! i a) (i-1) -| f, as, i => k f as + | app f a _, as, i => withAppAux k f (as.set! i a) (i-1) + | f, as, i => k f as @[inline] def withApp {α} (e : Expr) (k : Expr → Array Expr → α) : α := -let dummy := mkSort levelZero -let nargs := e.getAppNumArgs -withAppAux k e (mkArray nargs dummy) (nargs-1) + let dummy := mkSort levelZero + let nargs := e.getAppNumArgs + withAppAux k e (mkArray nargs dummy) (nargs-1) @[specialize] private def withAppRevAux {α} (k : Expr → Array Expr → α) : Expr → Array Expr → α -| app f a _, as => withAppRevAux k f (as.push a) -| f, as => k f as + | app f a _, as => withAppRevAux k f (as.push a) + | f, as => k f as @[inline] def withAppRev {α} (e : Expr) (k : Expr → Array Expr → α) : α := -withAppRevAux k e (Array.mkEmpty e.getAppNumArgs) + withAppRevAux k e (Array.mkEmpty e.getAppNumArgs) def getRevArgD : Expr → Nat → Expr → Expr -| app f a _, 0, _ => a -| app f _ _, i+1, v => getRevArgD f i v -| _, _, v => v + | app f a _, 0, _ => a + | app f _ _, i+1, v => getRevArgD f i v + | _, _, v => v def getRevArg! : Expr → Nat → Expr -| app f a _, 0 => a -| app f _ _, i+1 => getRevArg! f i -| _, _ => panic! "invalid index" + | app f a _, 0 => a + | app f _ _, i+1 => getRevArg! f i + | _, _ => panic! "invalid index" @[inline] def getArg! (e : Expr) (i : Nat) (n := e.getAppNumArgs) : Expr := -getRevArg! e (n - i - 1) + getRevArg! e (n - i - 1) @[inline] def getArgD (e : Expr) (i : Nat) (v₀ : Expr) (n := e.getAppNumArgs) : Expr := -getRevArgD e (n - i - 1) v₀ + getRevArgD e (n - i - 1) v₀ def isAppOf (e : Expr) (n : Name) : Bool := -match e.getAppFn with -| const c _ _ => c == n -| _ => false + match e.getAppFn with + | const c _ _ => c == n + | _ => false def isAppOfArity : Expr → Name → Nat → Bool -| const c _ _, n, 0 => c == n -| app f _ _, n, a+1 => isAppOfArity f n a -| _, _, _ => false + | const c _ _, n, 0 => c == n + | app f _ _, n, a+1 => isAppOfArity f n a + | _, _, _ => false def appFn! : Expr → Expr -| app f _ _ => f -| _ => panic! "application expected" + | app f _ _ => f + | _ => panic! "application expected" def appArg! : Expr → Expr -| app _ a _ => a -| _ => panic! "application expected" + | app _ a _ => a + | _ => panic! "application expected" def isNatLit : Expr → Bool -| lit (Literal.natVal _) _ => true -| _ => false + | lit (Literal.natVal _) _ => true + | _ => false def natLit? : Expr → Option Nat -| lit (Literal.natVal v) _ => v -| _ => none + | lit (Literal.natVal v) _ => v + | _ => none def isStringLit : Expr → Bool -| lit (Literal.strVal _) _ => true -| _ => false + | lit (Literal.strVal _) _ => true + | _ => false def isCharLit (e : Expr) : Bool := -e.isAppOfArity `Char.ofNat 1 && e.appArg!.isNatLit + e.isAppOfArity `Char.ofNat 1 && e.appArg!.isNatLit def constName! : Expr → Name -| const n _ _ => n -| _ => panic! "constant expected" + | const n _ _ => n + | _ => panic! "constant expected" def constName? : Expr → Option Name -| const n _ _ => some n -| _ => none + | const n _ _ => some n + | _ => none def constLevels! : Expr → List Level -| const _ ls _ => ls -| _ => panic! "constant expected" + | const _ ls _ => ls + | _ => panic! "constant expected" def bvarIdx! : Expr → Nat -| bvar idx _ => idx -| _ => panic! "bvar expected" + | bvar idx _ => idx + | _ => panic! "bvar expected" def fvarId! : Expr → FVarId -| fvar n _ => n -| _ => panic! "fvar expected" + | fvar n _ => n + | _ => panic! "fvar expected" def mvarId! : Expr → MVarId -| mvar n _ => n -| _ => panic! "mvar expected" + | mvar n _ => n + | _ => panic! "mvar expected" def bindingName! : Expr → Name -| forallE n _ _ _ => n -| lam n _ _ _ => n -| _ => panic! "binding expected" + | forallE n _ _ _ => n + | lam n _ _ _ => n + | _ => panic! "binding expected" def bindingDomain! : Expr → Expr -| forallE _ d _ _ => d -| lam _ d _ _ => d -| _ => panic! "binding expected" + | forallE _ d _ _ => d + | lam _ d _ _ => d + | _ => panic! "binding expected" def bindingBody! : Expr → Expr -| forallE _ _ b _ => b -| lam _ _ b _ => b -| _ => panic! "binding expected" + | forallE _ _ b _ => b + | lam _ _ b _ => b + | _ => panic! "binding expected" def bindingInfo! : Expr → BinderInfo -| forallE _ _ _ c => c.binderInfo -| lam _ _ _ c => c.binderInfo -| _ => panic! "binding expected" + | forallE _ _ _ c => c.binderInfo + | lam _ _ _ c => c.binderInfo + | _ => panic! "binding expected" def letName! : Expr → Name -| letE n _ _ _ _ => n -| _ => panic! "let expression expected" + | letE n _ _ _ _ => n + | _ => panic! "let expression expected" def consumeMData : Expr → Expr -| mdata _ e _ => consumeMData e -| e => e + | mdata _ e _ => consumeMData e + | e => e def hasLooseBVars (e : Expr) : Bool := -e.looseBVarRange > 0 + e.looseBVarRange > 0 @[extern "lean_expr_has_loose_bvar"] -constant hasLooseBVar (e : @& Expr) (bvarIdx : @& Nat) : Bool := arbitrary _ +constant hasLooseBVar (e : @& Expr) (bvarIdx : @& Nat) : Bool /-- Return true if `e` contains the loose bound variable `bvarIdx` in an explicit parameter, or in the range if `tryRange == true`. -/ def hasLooseBVarInExplicitDomain : Expr → Nat → Bool → Bool -| Expr.forallE _ d b c, bvarIdx, tryRange => (c.binderInfo.isExplicit && hasLooseBVar d bvarIdx) || hasLooseBVarInExplicitDomain b (bvarIdx+1) tryRange -| e, bvarIdx, tryRange => tryRange && hasLooseBVar e bvarIdx + | Expr.forallE _ d b c, bvarIdx, tryRange => (c.binderInfo.isExplicit && hasLooseBVar d bvarIdx) || hasLooseBVarInExplicitDomain b (bvarIdx+1) tryRange + | e, bvarIdx, tryRange => tryRange && hasLooseBVar e bvarIdx /-- Lower the loose bound variables `>= s` in `e` by `d`. @@ -615,12 +615,12 @@ def hasLooseBVarInExplicitDomain : Expr → Nat → Bool → Bool Remark: if `s < d`, then result is `e` -/ @[extern "lean_expr_lower_loose_bvars"] -constant lowerLooseBVars (e : @& Expr) (s d : @& Nat) : Expr := arbitrary _ +constant lowerLooseBVars (e : @& Expr) (s d : @& Nat) : Expr /-- Lift loose bound variables `>= s` in `e` by `d`. -/ @[extern "lean_expr_lift_loose_bvars"] -constant liftLooseBVars (e : @& Expr) (s d : @& Nat) : Expr := arbitrary _ +constant liftLooseBVars (e : @& Expr) (s d : @& Nat) : Expr /-- `inferImplicit e numParams considerRange` updates the first `numParams` parameter binder annotations of the `e` forall type. @@ -631,70 +631,68 @@ constant liftLooseBVars (e : @& Expr) (s d : @& Nat) : Expr := arbitrary _ When the `{}` annotation is used in these commands, we set `considerRange == false`. -/ def inferImplicit : Expr → Nat → Bool → Expr -| Expr.forallE n d b c, i+1, considerRange => - let b := inferImplicit b i considerRange - let newInfo := if c.binderInfo.isExplicit && hasLooseBVarInExplicitDomain b 0 considerRange then BinderInfo.implicit else c.binderInfo - mkForall n newInfo d b -| e, 0, _ => e -| e, _, _ => e + | Expr.forallE n d b c, i+1, considerRange => + let b := inferImplicit b i considerRange + let newInfo := if c.binderInfo.isExplicit && hasLooseBVarInExplicitDomain b 0 considerRange then BinderInfo.implicit else c.binderInfo + mkForall n newInfo d b + | e, 0, _ => e + | e, _, _ => e /-- Instantiate the loose bound variables in `e` using `subst`. That is, a loose `Expr.bvar i` is replaced with `subst[i]`. -/ @[extern "lean_expr_instantiate"] -constant instantiate (e : @& Expr) (subst : @& Array Expr) : Expr := arbitrary _ +constant instantiate (e : @& Expr) (subst : @& Array Expr) : Expr @[extern "lean_expr_instantiate1"] -constant instantiate1 (e : @& Expr) (subst : @& Expr) : Expr := arbitrary _ +constant instantiate1 (e : @& Expr) (subst : @& Expr) : Expr /-- Similar to instantiate, but `Expr.bvar i` is replaced with `subst[subst.size - i - 1]` -/ @[extern "lean_expr_instantiate_rev"] -constant instantiateRev (e : @& Expr) (subst : @& Array Expr) : Expr := arbitrary _ +constant instantiateRev (e : @& Expr) (subst : @& Array Expr) : Expr /-- Similar to `instantiate`, but consider only the variables `xs` in the range `[beginIdx, endIdx)`. Function panics if `beginIdx <= endIdx <= xs.size` does not hold. -/ @[extern "lean_expr_instantiate_range"] -constant instantiateRange (e : @& Expr) (beginIdx endIdx : @& Nat) (xs : @& Array Expr) : Expr := arbitrary _ +constant instantiateRange (e : @& Expr) (beginIdx endIdx : @& Nat) (xs : @& Array Expr) : Expr /-- Similar to `instantiateRev`, but consider only the variables `xs` in the range `[beginIdx, endIdx)`. Function panics if `beginIdx <= endIdx <= xs.size` does not hold. -/ @[extern "lean_expr_instantiate_rev_range"] -constant instantiateRevRange (e : @& Expr) (beginIdx endIdx : @& Nat) (xs : @& Array Expr) : Expr := arbitrary _ +constant instantiateRevRange (e : @& Expr) (beginIdx endIdx : @& Nat) (xs : @& Array Expr) : Expr /-- Replace free variables `xs` with loose bound variables. -/ @[extern "lean_expr_abstract"] -constant abstract (e : @& Expr) (xs : @& Array Expr) : Expr := arbitrary _ +constant abstract (e : @& Expr) (xs : @& Array Expr) : Expr /-- Similar to `abstract`, but consider only the first `min n xs.size` entries in `xs`. -/ @[extern "lean_expr_abstract_range"] -constant abstractRange (e : @& Expr) (n : @& Nat) (xs : @& Array Expr) : Expr := arbitrary _ +constant abstractRange (e : @& Expr) (n : @& Nat) (xs : @& Array Expr) : Expr /-- Replace occurrences of the free variable `fvar` in `e` with `v` -/ def replaceFVar (e : Expr) (fvar : Expr) (v : Expr) : Expr := -(e.abstract #[fvar]).instantiate1 v + (e.abstract #[fvar]).instantiate1 v /-- Replace occurrences of the free variable `fvarId` in `e` with `v` -/ def replaceFVarId (e : Expr) (fvarId : FVarId) (v : Expr) : Expr := -replaceFVar e (mkFVar fvarId) v + replaceFVar e (mkFVar fvarId) v /-- Replace occurrences of the free variables `fvars` in `e` with `vs` -/ def replaceFVars (e : Expr) (fvars : Array Expr) (vs : Array Expr) : Expr := -(e.abstract fvars).instantiateRev vs + (e.abstract fvars).instantiateRev vs -instance : HasToString Expr := -⟨Expr.dbgToString⟩ +instance : HasToString Expr := ⟨Expr.dbgToString⟩ -- TODO: should not use dbgToString, but constructors. -instance : HasRepr Expr := -⟨Expr.dbgToString⟩ +instance : HasRepr Expr := ⟨Expr.dbgToString⟩ def isAtomic : Expr → Bool -| Expr.const _ _ _ => true -| Expr.sort _ _ => true -| Expr.bvar _ _ => true -| Expr.lit _ _ => true -| Expr.mvar _ _ => true -| Expr.fvar _ _ => true -| _ => false + | Expr.const _ _ _ => true + | Expr.sort _ _ => true + | Expr.bvar _ _ => true + | Expr.lit _ _ => true + | Expr.mvar _ _ => true + | Expr.fvar _ _ => true + | _ => false end Expr @@ -710,10 +708,10 @@ def mkApp9 (f a b c d e₁ e₂ e₃ e₄ e₅ : Expr) := mkApp5 (mkApp4 f a b c def mkApp10 (f a b c d e₁ e₂ e₃ e₄ e₅ e₆ : Expr) := mkApp6 (mkApp4 f a b c d) e₁ e₂ e₃ e₄ e₅ e₆ def mkDecIsTrue (pred proof : Expr) := -mkAppB (mkConst `Decidable.isTrue) pred proof + mkAppB (mkConst `Decidable.isTrue) pred proof def mkDecIsFalse (pred proof : Expr) := -mkAppB (mkConst `Decidable.isFalse) pred proof + mkAppB (mkConst `Decidable.isFalse) pred proof open Std (HashMap HashSet PHashMap PHashSet) @@ -725,17 +723,17 @@ abbrev PExprSet := PersistentExprSet /- Auxiliary type for forcing `==` to be structural equality for `Expr` -/ structure ExprStructEq := -(val : Expr) + (val : Expr) instance : Coe Expr ExprStructEq := ⟨ExprStructEq.mk⟩ namespace ExprStructEq protected def beq : ExprStructEq → ExprStructEq → Bool -| ⟨e₁⟩, ⟨e₂⟩ => Expr.equal e₁ e₂ + | ⟨e₁⟩, ⟨e₂⟩ => Expr.equal e₁ e₂ protected def hash : ExprStructEq → USize -| ⟨e⟩ => e.hash + | ⟨e⟩ => e.hash instance : Inhabited ExprStructEq := ⟨{ val := arbitrary _ }⟩ instance : HasBeq ExprStructEq := ⟨ExprStructEq.beq⟩ @@ -758,19 +756,19 @@ private partial def mkAppRevRangeAux (revArgs : Array Expr) (start : Nat) (b : E /-- `mkAppRevRange f b e args == mkAppRev f (revArgs.extract b e)` -/ def mkAppRevRange (f : Expr) (beginIdx endIdx : Nat) (revArgs : Array Expr) : Expr := -mkAppRevRangeAux revArgs beginIdx f endIdx + mkAppRevRangeAux revArgs beginIdx f endIdx private def betaRevAux (revArgs : Array Expr) (sz : Nat) : Expr → Nat → Expr -| Expr.lam _ _ b _, i => - if i + 1 < sz then - betaRevAux revArgs sz b (i+1) - else - let n := sz - (i + 1) + | Expr.lam _ _ b _, i => + if i + 1 < sz then + betaRevAux revArgs sz b (i+1) + else + let n := sz - (i + 1) + mkAppRevRange (b.instantiateRange n sz revArgs) 0 n revArgs + | Expr.mdata _ b _, i => betaRevAux revArgs sz b i + | b, i => + let n := sz - i mkAppRevRange (b.instantiateRange n sz revArgs) 0 n revArgs -| Expr.mdata _ b _, i => betaRevAux revArgs sz b i -| b, i => - let n := sz - i - mkAppRevRange (b.instantiateRange n sz revArgs) 0 n revArgs /-- If `f` is a lambda expression, than "beta-reduce" it using `revArgs`. This function is often used with `getAppRev` or `withAppRev`. @@ -783,29 +781,29 @@ private def betaRevAux (revArgs : Array Expr) (sz : Nat) : Expr → Nat → Expr `args := t.getAppRev` is `#[d, c, b, a]`, and `betaRev (fun x y => t x y) #[d, c, b, a]` is `t a b c d`. -/ def betaRev (f : Expr) (revArgs : Array Expr) : Expr := -if revArgs.size == 0 then f -else betaRevAux revArgs revArgs.size f 0 + if revArgs.size == 0 then f + else betaRevAux revArgs revArgs.size f 0 def isHeadBetaTargetFn : Expr → Bool -| Expr.lam _ _ _ _ => true -| Expr.mdata _ b _ => isHeadBetaTargetFn b -| _ => false + | Expr.lam _ _ _ _ => true + | Expr.mdata _ b _ => isHeadBetaTargetFn b + | _ => false def headBeta (e : Expr) : Expr := -let f := e.getAppFn -if f.isHeadBetaTargetFn then betaRev f e.getAppRevArgs else e + let f := e.getAppFn + if f.isHeadBetaTargetFn then betaRev f e.getAppRevArgs else e def isHeadBetaTarget (e : Expr) : Bool := -e.getAppFn.isHeadBetaTargetFn + e.getAppFn.isHeadBetaTargetFn private def etaExpandedBody : Expr → Nat → Nat → Option Expr -| app f (bvar j _) _, n+1, i => if j == i then etaExpandedBody f n (i+1) else none -| _, n+1, _ => none -| f, 0, _ => if f.hasLooseBVars then none else some f + | app f (bvar j _) _, n+1, i => if j == i then etaExpandedBody f n (i+1) else none + | _, n+1, _ => none + | f, 0, _ => if f.hasLooseBVars then none else some f private def etaExpandedAux : Expr → Nat → Option Expr -| lam _ _ b _, n => etaExpandedAux b (n+1) -| e, n => etaExpandedBody e n 0 + | lam _ _ b _, n => etaExpandedAux b (n+1) + | e, n => etaExpandedBody e n 0 /-- If `e` is of the form `(fun x₁ ... xₙ => f x₁ ... xₙ)` and `f` does not contain `x₁`, ..., `xₙ`, @@ -815,45 +813,45 @@ private def etaExpandedAux : Expr → Nat → Option Expr Remark: `ₙ` may be 0 -/ def etaExpanded? (e : Expr) : Option Expr := -etaExpandedAux e 0 + etaExpandedAux e 0 /-- Similar to `etaExpanded?`, but only succeeds if `ₙ ≥ 1`. -/ def etaExpandedStrict? : Expr → Option Expr -| lam _ _ b _ => etaExpandedAux b 1 -| _ => none + | lam _ _ b _ => etaExpandedAux b 1 + | _ => none def getOptParamDefault? (e : Expr) : Option Expr := -if e.isAppOfArity `optParam 2 then - some e.appArg! -else - none + if e.isAppOfArity `optParam 2 then + some e.appArg! + else + none def getAutoParamTactic? (e : Expr) : Option Expr := -if e.isAppOfArity `autoParam 2 then - some e.appArg! -else - none + if e.isAppOfArity `autoParam 2 then + some e.appArg! + else + none def isOptParam (e : Expr) : Bool := -e.isAppOfArity `optParam 2 + e.isAppOfArity `optParam 2 def isAutoParam (e : Expr) : Bool := -e.isAppOfArity `autoParam 2 + e.isAppOfArity `autoParam 2 /-- Return true iff `e` contains a free variable which statisfies `p`. -/ @[inline] def hasAnyFVar (e : Expr) (p : FVarId → Bool) : Bool := -let rec @[specialize] visit (e : Expr) := if !e.hasFVar then false else - match e with - | Expr.forallE _ d b _ => visit d || visit b - | Expr.lam _ d b _ => visit d || visit b - | Expr.mdata _ e _ => visit e - | Expr.letE _ t v b _ => visit t || visit v || visit b - | Expr.app f a _ => visit f || visit a - | Expr.proj _ _ e _ => visit e - | Expr.localE _ _ _ _ => unreachable! - | e@(Expr.fvar fvarId _) => p fvarId - | e => false -visit e + let rec @[specialize] visit (e : Expr) := if !e.hasFVar then false else + match e with + | Expr.forallE _ d b _ => visit d || visit b + | Expr.lam _ d b _ => visit d || visit b + | Expr.mdata _ e _ => visit e + | Expr.letE _ t v b _ => visit t || visit v || visit b + | Expr.app f a _ => visit f || visit a + | Expr.proj _ _ e _ => visit e + | Expr.localE _ _ _ _ => unreachable! + | e@(Expr.fvar fvarId _) => p fvarId + | e => false + visit e /- The update functions here are defined using C code. They will try to avoid @@ -867,145 +865,145 @@ visit e @[extern "lean_expr_update_app"] def updateApp (e : Expr) (newFn : Expr) (newArg : Expr) (h : e.isApp = true) : Expr := -mkApp newFn newArg + mkApp newFn newArg @[inline] def updateApp! (e : Expr) (newFn : Expr) (newArg : Expr) : Expr := -match e with -| app fn arg c => updateApp (app fn arg c) newFn newArg rfl -| _ => panic! "application expected" + match e with + | app fn arg c => updateApp (app fn arg c) newFn newArg rfl + | _ => panic! "application expected" @[extern "lean_expr_update_const"] def updateConst (e : Expr) (newLevels : List Level) (h : e.isConst = true) : Expr := -mkConst e.constName! newLevels + mkConst e.constName! newLevels @[inline] def updateConst! (e : Expr) (newLevels : List Level) : Expr := -match e with -| const n ls c => updateConst (const n ls c) newLevels rfl -| _ => panic! "constant expected" + match e with + | const n ls c => updateConst (const n ls c) newLevels rfl + | _ => panic! "constant expected" @[extern "lean_expr_update_sort"] def updateSort (e : Expr) (newLevel : Level) (h : e.isSort = true) : Expr := -mkSort newLevel + mkSort newLevel @[inline] def updateSort! (e : Expr) (newLevel : Level) : Expr := -match e with -| sort l c => updateSort (sort l c) newLevel rfl -| _ => panic! "level expected" + match e with + | sort l c => updateSort (sort l c) newLevel rfl + | _ => panic! "level expected" @[extern "lean_expr_update_proj"] def updateProj (e : Expr) (newExpr : Expr) (h : e.isProj = true) : Expr := -match e with -| proj s i _ _ => mkProj s i newExpr -| _ => e -- unreachable because of `h` + match e with + | proj s i _ _ => mkProj s i newExpr + | _ => e -- unreachable because of `h` @[extern "lean_expr_update_mdata"] def updateMData (e : Expr) (newExpr : Expr) (h : e.isMData = true) : Expr := -match e with -| mdata d _ _ => mkMData d newExpr -| _ => e -- unreachable because of `h` + match e with + | mdata d _ _ => mkMData d newExpr + | _ => e -- unreachable because of `h` @[inline] def updateMData! (e : Expr) (newExpr : Expr) : Expr := -match e with -| mdata d e c => updateMData (mdata d e c) newExpr rfl -| _ => panic! "mdata expected" + match e with + | mdata d e c => updateMData (mdata d e c) newExpr rfl + | _ => panic! "mdata expected" @[inline] def updateProj! (e : Expr) (newExpr : Expr) : Expr := -match e with -| proj s i e c => updateProj (proj s i e c) newExpr rfl -| _ => panic! "proj expected" + match e with + | proj s i e c => updateProj (proj s i e c) newExpr rfl + | _ => panic! "proj expected" @[extern "lean_expr_update_forall"] def updateForall (e : Expr) (newBinfo : BinderInfo) (newDomain : Expr) (newBody : Expr) (h : e.isForall = true) : Expr := -mkForall e.bindingName! newBinfo newDomain newBody + mkForall e.bindingName! newBinfo newDomain newBody @[inline] def updateForall! (e : Expr) (newBinfo : BinderInfo) (newDomain : Expr) (newBody : Expr) : Expr := -match e with -| forallE n d b c => updateForall (forallE n d b c) newBinfo newDomain newBody rfl -| _ => panic! "forall expected" + match e with + | forallE n d b c => updateForall (forallE n d b c) newBinfo newDomain newBody rfl + | _ => panic! "forall expected" @[inline] def updateForallE! (e : Expr) (newDomain : Expr) (newBody : Expr) : Expr := -match e with -| forallE n d b c => updateForall (forallE n d b c) c.binderInfo newDomain newBody rfl -| _ => panic! "forall expected" + match e with + | forallE n d b c => updateForall (forallE n d b c) c.binderInfo newDomain newBody rfl + | _ => panic! "forall expected" @[extern "lean_expr_update_lambda"] def updateLambda (e : Expr) (newBinfo : BinderInfo) (newDomain : Expr) (newBody : Expr) (h : e.isLambda = true) : Expr := -mkLambda e.bindingName! newBinfo newDomain newBody + mkLambda e.bindingName! newBinfo newDomain newBody @[inline] def updateLambda! (e : Expr) (newBinfo : BinderInfo) (newDomain : Expr) (newBody : Expr) : Expr := -match e with -| lam n d b c => updateLambda (lam n d b c) newBinfo newDomain newBody rfl -| _ => panic! "lambda expected" + match e with + | lam n d b c => updateLambda (lam n d b c) newBinfo newDomain newBody rfl + | _ => panic! "lambda expected" @[inline] def updateLambdaE! (e : Expr) (newDomain : Expr) (newBody : Expr) : Expr := -match e with -| lam n d b c => updateLambda (lam n d b c) c.binderInfo newDomain newBody rfl -| _ => panic! "lambda expected" + match e with + | lam n d b c => updateLambda (lam n d b c) c.binderInfo newDomain newBody rfl + | _ => panic! "lambda expected" @[extern "lean_expr_update_let"] def updateLet (e : Expr) (newType : Expr) (newVal : Expr) (newBody : Expr) (h : e.isLet = true) : Expr := -mkLet e.letName! newType newVal newBody + mkLet e.letName! newType newVal newBody @[inline] def updateLet! (e : Expr) (newType : Expr) (newVal : Expr) (newBody : Expr) : Expr := -match e with -| letE n t v b c => updateLet (letE n t v b c) newType newVal newBody rfl -| _ => panic! "let expression expected" + match e with + | letE n t v b c => updateLet (letE n t v b c) newType newVal newBody rfl + | _ => panic! "let expression expected" def updateFn : Expr → Expr → Expr -| e@(app f a _), g => e.updateApp! (updateFn f g) a -| _, g => g + | e@(app f a _), g => e.updateApp! (updateFn f g) a + | _, g => g /- Instantiate level parameters -/ @[inline] def instantiateLevelParamsCore (s : Name → Option Level) (e : Expr) : Expr := -let rec @[specialize] visit (e : Expr) : Expr := - if !e.hasLevelParam then e - else match e with - | lam n d b _ => e.updateLambdaE! (visit d) (visit b) - | forallE n d b _ => e.updateForallE! (visit d) (visit b) - | letE n t v b _ => e.updateLet! (visit t) (visit v) (visit b) - | app f a _ => e.updateApp! (visit f) (visit a) - | proj _ _ s _ => e.updateProj! (visit s) - | mdata _ b _ => e.updateMData! (visit b) - | const _ us _ => e.updateConst! (us.map (fun u => u.instantiateParams s)) - | sort u _ => e.updateSort! (u.instantiateParams s) - | localE .. => unreachable! - | e => e -visit e + let rec @[specialize] visit (e : Expr) : Expr := + if !e.hasLevelParam then e + else match e with + | lam n d b _ => e.updateLambdaE! (visit d) (visit b) + | forallE n d b _ => e.updateForallE! (visit d) (visit b) + | letE n t v b _ => e.updateLet! (visit t) (visit v) (visit b) + | app f a _ => e.updateApp! (visit f) (visit a) + | proj _ _ s _ => e.updateProj! (visit s) + | mdata _ b _ => e.updateMData! (visit b) + | const _ us _ => e.updateConst! (us.map (fun u => u.instantiateParams s)) + | sort u _ => e.updateSort! (u.instantiateParams s) + | localE .. => unreachable! + | e => e + visit e private def getParamSubst : List Name → List Level → Name → Option Level -| p::ps, u::us, p' => if p == p' then some u else getParamSubst ps us p' -| _, _, _ => none + | p::ps, u::us, p' => if p == p' then some u else getParamSubst ps us p' + | _, _, _ => none def instantiateLevelParams (e : Expr) (paramNames : List Name) (lvls : List Level) : Expr := -instantiateLevelParamsCore (getParamSubst paramNames lvls) e + instantiateLevelParamsCore (getParamSubst paramNames lvls) e private partial def getParamSubstArray (ps : Array Name) (us : Array Level) (p' : Name) (i : Nat) : Option Level := -if h : i < ps.size then - let p := ps.get ⟨i, h⟩ - if h : i < us.size then - let u := us.get ⟨i, h⟩ - if p == p' then some u else getParamSubstArray ps us p' (i+1) + if h : i < ps.size then + let p := ps.get ⟨i, h⟩ + if h : i < us.size then + let u := us.get ⟨i, h⟩ + if p == p' then some u else getParamSubstArray ps us p' (i+1) + else none else none -else none def instantiateLevelParamsArray (e : Expr) (paramNames : Array Name) (lvls : Array Level) : Expr := -instantiateLevelParamsCore (fun p => getParamSubstArray paramNames lvls p 0) e + instantiateLevelParamsCore (fun p => getParamSubstArray paramNames lvls p 0) e end Expr def mkAnnotation (kind : Name) (e : Expr) : Expr := -mkMData (KVMap.empty.insert kind (DataValue.ofBool true)) e + mkMData (KVMap.empty.insert kind (DataValue.ofBool true)) e def annotation? (kind : Name) (e : Expr) : Option Expr := -match e with -| Expr.mdata d b _ => if d.size == 1 && d.getBool kind false then some b else none -| _ => none + match e with + | Expr.mdata d b _ => if d.size == 1 && d.getBool kind false then some b else none + | _ => none def mkFreshFVarId {m : Type → Type} [Monad m] [MonadNameGenerator m] : m FVarId := -mkFreshId + mkFreshId def mkFreshMVarId {m : Type → Type} [Monad m] [MonadNameGenerator m] : m FVarId := -mkFreshId + mkFreshId end Lean diff --git a/src/Lean/InternalExceptionId.lean b/src/Lean/InternalExceptionId.lean index 324f350dd2..4b64551ef0 100644 --- a/src/Lean/InternalExceptionId.lean +++ b/src/Lean/InternalExceptionId.lean @@ -7,30 +7,30 @@ Authors: Leonardo de Moura namespace Lean structure InternalExceptionId := -(idx : Nat := 0) + (idx : Nat := 0) instance : Inhabited InternalExceptionId := ⟨{}⟩ instance : HasBeq InternalExceptionId := -⟨fun id₁ id₂ => id₁.idx == id₂.idx⟩ + ⟨fun id₁ id₂ => id₁.idx == id₂.idx⟩ builtin_initialize internalExceptionsRef : IO.Ref (Array Name) ← IO.mkRef #[] def registerInternalExceptionId (name : Name) : IO InternalExceptionId := do -let exs ← internalExceptionsRef.get -if exs.contains name then throw $ IO.userError s!"invalid internal exception id, '{name}' has already been used" -let nextIdx := exs.size -internalExceptionsRef.modify fun a => a.push name -pure { idx := nextIdx } + let exs ← internalExceptionsRef.get + if exs.contains name then throw $ IO.userError s!"invalid internal exception id, '{name}' has already been used" + let nextIdx := exs.size + internalExceptionsRef.modify fun a => a.push name + pure { idx := nextIdx } def InternalExceptionId.toString (id : InternalExceptionId) : String := -s!"internal exception #{id.idx}" + s!"internal exception #{id.idx}" def InternalExceptionId.getName (id : InternalExceptionId) : IO Name := do -let exs ← internalExceptionsRef.get -let i := id.idx; -if h : i < exs.size then - pure $ exs.get ⟨i, h⟩ -else - throw $ IO.userError "invalid internal exception id" + let exs ← internalExceptionsRef.get + let i := id.idx; + if h : i < exs.size then + pure $ exs.get ⟨i, h⟩ + else + throw $ IO.userError "invalid internal exception id" end Lean diff --git a/src/Lean/KeyedDeclsAttribute.lean b/src/Lean/KeyedDeclsAttribute.lean index e1a5806c1a..a4e2c246b8 100644 --- a/src/Lean/KeyedDeclsAttribute.lean +++ b/src/Lean/KeyedDeclsAttribute.lean @@ -29,140 +29,140 @@ abbrev Key := Name Important: `mkConst valueTypeName` and `γ` must be definitionally equal. -/ structure Def (γ : Type) := -(builtinName : Name) -- Builtin attribute name (e.g., `builtinTermElab) -(name : Name) -- Attribute name (e.g., `termElab) -(descr : String) -- Attribute description -(valueTypeName : Name) --- Convert `Syntax` into a `Key`, the default implementation expects an identifier. -(evalKey : Bool → Syntax → AttrM Key := - fun builtin arg => match attrParamSyntaxToIdentifier arg with - | some id => pure id - | none => throwError "invalid attribute argument, expected identifier") + (builtinName : Name) -- Builtin attribute name (e.g., `builtinTermElab) + (name : Name) -- Attribute name (e.g., `termElab) + (descr : String) -- Attribute description + (valueTypeName : Name) + -- Convert `Syntax` into a `Key`, the default implementation expects an identifier. + (evalKey : Bool → Syntax → AttrM Key := + fun builtin arg => match attrParamSyntaxToIdentifier arg with + | some id => pure id + | none => throwError "invalid attribute argument, expected identifier") instance {γ} : Inhabited (Def γ) := -⟨{ builtinName := arbitrary _, name := arbitrary _, descr := arbitrary _, valueTypeName := arbitrary _ }⟩ + ⟨{ builtinName := arbitrary _, name := arbitrary _, descr := arbitrary _, valueTypeName := arbitrary _ }⟩ structure OLeanEntry := -(key : Key) -(decl : Name) -- Name of a declaration stored in the environment which has type `mkConst Def.valueTypeName`. + (key : Key) + (decl : Name) -- Name of a declaration stored in the environment which has type `mkConst Def.valueTypeName`. structure AttributeEntry (γ : Type) extends OLeanEntry := -/- Recall that we cannot store `γ` into .olean files because it is a closure. - Given `OLeanEntry.decl`, we convert it into a `γ` by using the unsafe function `evalConstCheck`. -/ -(value : γ) + /- Recall that we cannot store `γ` into .olean files because it is a closure. + Given `OLeanEntry.decl`, we convert it into a `γ` by using the unsafe function `evalConstCheck`. -/ + (value : γ) abbrev Table (γ : Type) := SMap Key (List γ) structure ExtensionState (γ : Type) := -(newEntries : List OLeanEntry := []) -(table : Table γ := {}) + (newEntries : List OLeanEntry := []) + (table : Table γ := {}) abbrev Extension (γ : Type) := PersistentEnvExtension OLeanEntry (AttributeEntry γ) (ExtensionState γ) end KeyedDeclsAttribute structure KeyedDeclsAttribute (γ : Type) := -(defn : KeyedDeclsAttribute.Def γ) --- imported/builtin instances -(tableRef : IO.Ref (KeyedDeclsAttribute.Table γ)) --- instances from current module -(ext : KeyedDeclsAttribute.Extension γ) + (defn : KeyedDeclsAttribute.Def γ) + -- imported/builtin instances + (tableRef : IO.Ref (KeyedDeclsAttribute.Table γ)) + -- instances from current module + (ext : KeyedDeclsAttribute.Extension γ) namespace KeyedDeclsAttribute def Table.insert {γ : Type} (table : Table γ) (k : Key) (v : γ) : Table γ := -match table.find? k with -| some vs => SMap.insert table k (v::vs) -| none => SMap.insert table k [v] + match table.find? k with + | some vs => SMap.insert table k (v::vs) + | none => SMap.insert table k [v] instance {γ} : Inhabited (ExtensionState γ) := ⟨{}⟩ instance {γ} : Inhabited (KeyedDeclsAttribute γ) := -⟨{ defn := arbitrary _, tableRef := arbitrary _, ext := arbitrary _ }⟩ + ⟨{ defn := arbitrary _, tableRef := arbitrary _, ext := arbitrary _ }⟩ private def mkInitial {γ} (tableRef : IO.Ref (Table γ)) : IO (ExtensionState γ) := do -let table ← tableRef.get -pure { table := table } + let table ← tableRef.get + pure { table := table } private unsafe def addImported {γ} (df : Def γ) (tableRef : IO.Ref (Table γ)) (es : Array (Array OLeanEntry)) : ImportM (ExtensionState γ) := do -let ctx ← read -let table ← tableRef.get -let table ← es.foldlM - (fun table entries => - entries.foldlM - (fun (table : Table γ) entry => - match ctx.env.evalConstCheck γ ctx.opts df.valueTypeName entry.decl with - | Except.ok f => pure $ table.insert entry.key f - | Except.error ex => throw (IO.userError ex)) - table) - table -pure { table := table } + let ctx ← read + let table ← tableRef.get + let table ← es.foldlM + (fun table entries => + entries.foldlM + (fun (table : Table γ) entry => + match ctx.env.evalConstCheck γ ctx.opts df.valueTypeName entry.decl with + | Except.ok f => pure $ table.insert entry.key f + | Except.error ex => throw (IO.userError ex)) + table) + table + pure { table := table } private def addExtensionEntry {γ} (s : ExtensionState γ) (e : AttributeEntry γ) : ExtensionState γ := -{ table := s.table.insert e.key e.value, newEntries := e.toOLeanEntry :: s.newEntries } + { table := s.table.insert e.key e.value, newEntries := e.toOLeanEntry :: s.newEntries } def addBuiltin {γ} (attr : KeyedDeclsAttribute γ) (key : Key) (val : γ) : IO Unit := -attr.tableRef.modify $ fun m => m.insert key val + attr.tableRef.modify $ fun m => m.insert key val /-- def _regBuiltin$(declName) : IO Unit := @addBuiltin $(mkConst valueTypeName) $(mkConst attrDeclName) $(key) $(mkConst declName) -/ def declareBuiltin {γ} (df : Def γ) (attrDeclName : Name) (env : Environment) (key : Key) (declName : Name) : IO Environment := -let name := `_regBuiltin ++ declName -let type := mkApp (mkConst `IO) (mkConst `Unit) -let val := mkAppN (mkConst `Lean.KeyedDeclsAttribute.addBuiltin) #[mkConst df.valueTypeName, mkConst attrDeclName, toExpr key, mkConst declName] -let decl := Declaration.defnDecl { name := name, lparams := [], type := type, value := val, hints := ReducibilityHints.opaque, isUnsafe := false } -match env.addAndCompile {} decl with --- TODO: pretty print error -| Except.error e => do - let msg ← (e.toMessageData {}).toString - throw (IO.userError s!"failed to emit registration code for builtin '{declName}': {msg}") -| Except.ok env => IO.ofExcept (setBuiltinInitAttr env name) + let name := `_regBuiltin ++ declName + let type := mkApp (mkConst `IO) (mkConst `Unit) + let val := mkAppN (mkConst `Lean.KeyedDeclsAttribute.addBuiltin) #[mkConst df.valueTypeName, mkConst attrDeclName, toExpr key, mkConst declName] + let decl := Declaration.defnDecl { name := name, lparams := [], type := type, value := val, hints := ReducibilityHints.opaque, isUnsafe := false } + match env.addAndCompile {} decl with + -- TODO: pretty print error + | Except.error e => do + let msg ← (e.toMessageData {}).toString + throw (IO.userError s!"failed to emit registration code for builtin '{declName}': {msg}") + | Except.ok env => IO.ofExcept (setBuiltinInitAttr env name) /- TODO: add support for scoped attributes -/ protected unsafe def init {γ} (df : Def γ) (attrDeclName : Name) : IO (KeyedDeclsAttribute γ) := do -let tableRef ← IO.mkRef ({} : Table γ) -let ext : Extension γ ← registerPersistentEnvExtension { - name := df.name, - mkInitial := mkInitial tableRef, - addImportedFn := addImported df tableRef, - addEntryFn := addExtensionEntry, - exportEntriesFn := fun s => s.newEntries.reverse.toArray, - statsFn := fun s => f!"number of local entries: {s.newEntries.length}" -} -registerBuiltinAttribute { - name := df.builtinName, - descr := "(builtin) " ++ df.descr, - add := fun declName arg persistent => do - unless persistent do throwError! "invalid attribute '{df.builtinName}', must be persistent" - let key ← df.evalKey true arg - let decl ← getConstInfo declName - match decl.type with - | Expr.const c _ _ => - if c != df.valueTypeName then throwError! "unexpected type at '{declName}', '{df.valueTypeName}' expected" - else - let env ← getEnv - let env ← liftIO $ declareBuiltin df attrDeclName env key declName - setEnv env - | _ => throwError! "unexpected type at '{declName}', '{df.valueTypeName}' expected", - applicationTime := AttributeApplicationTime.afterCompilation -} -registerBuiltinAttribute { - name := df.name, - descr := df.descr, - add := fun constName arg persistent => do - let key ← df.evalKey false arg - let val ← evalConstCheck γ df.valueTypeName constName - let env ← getEnv - setEnv $ ext.addEntry env { key := key, decl := constName, value := val }, - applicationTime := AttributeApplicationTime.afterCompilation -} -pure { defn := df, tableRef := tableRef, ext := ext } + let tableRef ← IO.mkRef ({} : Table γ) + let ext : Extension γ ← registerPersistentEnvExtension { + name := df.name, + mkInitial := mkInitial tableRef, + addImportedFn := addImported df tableRef, + addEntryFn := addExtensionEntry, + exportEntriesFn := fun s => s.newEntries.reverse.toArray, + statsFn := fun s => f!"number of local entries: {s.newEntries.length}" + } + registerBuiltinAttribute { + name := df.builtinName, + descr := "(builtin) " ++ df.descr, + add := fun declName arg persistent => do + unless persistent do throwError! "invalid attribute '{df.builtinName}', must be persistent" + let key ← df.evalKey true arg + let decl ← getConstInfo declName + match decl.type with + | Expr.const c _ _ => + if c != df.valueTypeName then throwError! "unexpected type at '{declName}', '{df.valueTypeName}' expected" + else + let env ← getEnv + let env ← liftIO $ declareBuiltin df attrDeclName env key declName + setEnv env + | _ => throwError! "unexpected type at '{declName}', '{df.valueTypeName}' expected", + applicationTime := AttributeApplicationTime.afterCompilation + } + registerBuiltinAttribute { + name := df.name, + descr := df.descr, + add := fun constName arg persistent => do + let key ← df.evalKey false arg + let val ← evalConstCheck γ df.valueTypeName constName + let env ← getEnv + setEnv $ ext.addEntry env { key := key, decl := constName, value := val }, + applicationTime := AttributeApplicationTime.afterCompilation + } + pure { defn := df, tableRef := tableRef, ext := ext } /-- Retrieve values tagged with `[attr key]` or `[builtinAttr key]`. -/ def getValues {γ} (attr : KeyedDeclsAttribute γ) (env : Environment) (key : Name) : List γ := -(attr.ext.getState env).table.findD key [] + (attr.ext.getState env).table.findD key [] end KeyedDeclsAttribute diff --git a/src/Lean/Level.lean b/src/Lean/Level.lean index 62ec9d54bc..ac880dca3a 100644 --- a/src/Lean/Level.lean +++ b/src/Lean/Level.lean @@ -25,62 +25,62 @@ namespace Lean def Level.Data := UInt64 instance : Inhabited Level.Data := -inferInstanceAs (Inhabited UInt64) + inferInstanceAs (Inhabited UInt64) def Level.Data.hash (c : Level.Data) : USize := -c.toUInt32.toUSize + c.toUInt32.toUSize instance : HasBeq Level.Data := -⟨fun (a b : UInt64) => a == b⟩ + ⟨fun (a b : UInt64) => a == b⟩ def Level.Data.depth (c : Level.Data) : UInt32 := -(c.shiftRight 40).toUInt32 + (c.shiftRight 40).toUInt32 def Level.Data.hasMVar (c : Level.Data) : Bool := -((c.shiftRight 32).land 1) == 1 + ((c.shiftRight 32).land 1) == 1 def Level.Data.hasParam (c : Level.Data) : Bool := -((c.shiftRight 33).land 1) == 1 + ((c.shiftRight 33).land 1) == 1 def Level.mkData (h : USize) (depth : Nat) (hasMVar hasParam : Bool) : Level.Data := -if depth > Nat.pow 2 24 - 1 then panic! "universe level depth is too big" -else - let r : UInt64 := h.toUInt32.toUInt64 + hasMVar.toUInt64.shiftLeft 32 + hasParam.toUInt64.shiftLeft 33 + depth.toUInt64.shiftLeft 40 - r + if depth > Nat.pow 2 24 - 1 then panic! "universe level depth is too big" + else + let r : UInt64 := h.toUInt32.toUInt64 + hasMVar.toUInt64.shiftLeft 32 + hasParam.toUInt64.shiftLeft 33 + depth.toUInt64.shiftLeft 40 + r open Level inductive Level -| zero : Data → Level -| succ : Level → Data → Level -| max : Level → Level → Data → Level -| imax : Level → Level → Data → Level -| param : Name → Data → Level -| mvar : Name → Data → Level + | zero : Data → Level + | succ : Level → Data → Level + | max : Level → Level → Data → Level + | imax : Level → Level → Data → Level + | param : Name → Data → Level + | mvar : Name → Data → Level namespace Level @[inline] def data : Level → Data -| zero d => d -| mvar _ d => d -| param _ d => d -| succ _ d => d -| max _ _ d => d -| imax _ _ d => d + | zero d => d + | mvar _ d => d + | param _ d => d + | succ _ d => d + | max _ _ d => d + | imax _ _ d => d protected def hash (u : Level) : USize := -u.data.hash + u.data.hash instance : Hashable Level := ⟨Level.hash⟩ def depth (u : Level) : Nat := -u.data.depth.toNat + u.data.depth.toNat def hasMVar (u : Level) : Bool := -u.data.hasMVar + u.data.hasMVar def hasParam (u : Level) : Bool := -u.data.hasParam + u.data.hasParam @[export lean_level_hash] def hashEx : Level → USize := Level.hash @[export lean_level_has_mvar] def hasMVarEx : Level → Bool := hasMVar @@ -90,26 +90,26 @@ u.data.hasParam end Level def levelZero := -Level.zero $ mkData 2221 0 false false + Level.zero $ mkData 2221 0 false false def mkLevelMVar (mvarId : Name) := -Level.mvar mvarId $ mkData (mixHash 2237 $ hash mvarId) 0 true false + Level.mvar mvarId $ mkData (mixHash 2237 $ hash mvarId) 0 true false def mkLevelParam (name : Name) := -Level.param name $ mkData (mixHash 2239 $ hash name) 0 false true + Level.param name $ mkData (mixHash 2239 $ hash name) 0 false true def mkLevelSucc (u : Level) := -Level.succ u $ mkData (mixHash 2243 $ hash u) (u.depth + 1) u.hasMVar u.hasParam + Level.succ u $ mkData (mixHash 2243 $ hash u) (u.depth + 1) u.hasMVar u.hasParam def mkLevelMax (u v : Level) := -Level.max u v $ mkData (mixHash 2251 $ mixHash (hash u) (hash v)) (Nat.max u.depth v.depth + 1) - (u.hasMVar || v.hasMVar) - (u.hasParam || v.hasParam) + Level.max u v $ mkData (mixHash 2251 $ mixHash (hash u) (hash v)) (Nat.max u.depth v.depth + 1) + (u.hasMVar || v.hasMVar) + (u.hasParam || v.hasParam) def mkLevelIMax (u v : Level) := -Level.imax u v $ mkData (mixHash 2267 $ mixHash (hash u) (hash v)) (Nat.max u.depth v.depth + 1) - (u.hasMVar || v.hasMVar) - (u.hasParam || v.hasParam) + Level.imax u v $ mkData (mixHash 2267 $ mixHash (hash u) (hash v)) (Nat.max u.depth v.depth + 1) + (u.hasMVar || v.hasMVar) + (u.hasParam || v.hasParam) def levelOne := mkLevelSucc levelZero @@ -125,79 +125,79 @@ namespace Level instance : Inhabited Level := ⟨levelZero⟩ def isZero : Level → Bool -| zero _ => true -| _ => false + | zero _ => true + | _ => false def isSucc : Level → Bool -| succ _ _ => true -| _ => false + | succ .. => true + | _ => false def isMax : Level → Bool -| max _ _ _ => true -| _ => false + | max .. => true + | _ => false def isIMax : Level → Bool -| imax _ _ _ => true -| _ => false + | imax .. => true + | _ => false def isMaxIMax : Level → Bool -| max _ _ _ => true -| imax _ _ _ => true -| _ => false + | max .. => true + | imax .. => true + | _ => false def isParam : Level → Bool -| param _ _ => true -| _ => false + | param .. => true + | _ => false def isMVar : Level → Bool -| mvar _ _ => true -| _ => false + | mvar .. => true + | _ => false def mvarId! : Level → Name -| mvar mvarId _ => mvarId -| _ => panic! "metavariable expected" + | mvar mvarId _ => mvarId + | _ => panic! "metavariable expected" /-- If result is true, then forall assignments `A` which assigns all parameters and metavariables occuring in `l`, `l[A] != zero` -/ def isNeverZero : Level → Bool -| zero _ => false -| param _ _ => false -| mvar _ _ => false -| succ _ _ => true -| max l₁ l₂ _ => isNeverZero l₁ || isNeverZero l₂ -| imax l₁ l₂ _ => isNeverZero l₂ + | zero _ => false + | param .. => false + | mvar .. => false + | succ .. => true + | max l₁ l₂ _ => isNeverZero l₁ || isNeverZero l₂ + | imax l₁ l₂ _ => isNeverZero l₂ def ofNat : Nat → Level -| 0 => levelZero -| n+1 => mkLevelSucc (ofNat n) + | 0 => levelZero + | n+1 => mkLevelSucc (ofNat n) def addOffsetAux : Nat → Level → Level -| 0, u => u -| (n+1), u => addOffsetAux n (mkLevelSucc u) + | 0, u => u + | (n+1), u => addOffsetAux n (mkLevelSucc u) def addOffset (u : Level) (n : Nat) : Level := -u.addOffsetAux n + u.addOffsetAux n def isExplicit : Level → Bool -| zero _ => true -| succ u _ => !u.hasMVar && !u.hasParam && isExplicit u -| _ => false + | zero _ => true + | succ u _ => !u.hasMVar && !u.hasParam && isExplicit u + | _ => false def getOffsetAux : Level → Nat → Nat -| succ u _, r => getOffsetAux u (r+1) -| _, r => r + | succ u _, r => getOffsetAux u (r+1) + | _, r => r def getOffset (lvl : Level) : Nat := - getOffsetAux lvl 0 + getOffsetAux lvl 0 def getLevelOffset : Level → Level -| succ u _ => getLevelOffset u -| u => u + | succ u _ => getLevelOffset u + | u => u def toNat (lvl : Level) : Option Nat := -match lvl.getLevelOffset with -| zero _ => lvl.getOffset -| _ => none + match lvl.getLevelOffset with + | zero _ => lvl.getOffset + | _ => none @[extern "lean_level_eq"] protected constant beq (a : @& Level) (b : @& Level) : Bool := arbitrary _ @@ -206,34 +206,34 @@ instance : HasBeq Level := ⟨Level.beq⟩ /-- `occurs u l` return `true` iff `u` occurs in `l`. -/ def occurs : Level → Level → Bool -| u, v@(succ v₁ _) => u == v || occurs u v₁ -| u, v@(max v₁ v₂ _) => u == v || occurs u v₁ || occurs u v₂ -| u, v@(imax v₁ v₂ _) => u == v || occurs u v₁ || occurs u v₂ -| u, v => u == v + | u, v@(succ v₁ _) => u == v || occurs u v₁ + | u, v@(max v₁ v₂ _) => u == v || occurs u v₁ || occurs u v₂ + | u, v@(imax v₁ v₂ _) => u == v || occurs u v₁ || occurs u v₂ + | u, v => u == v def ctorToNat : Level → Nat -| zero _ => 0 -| param _ _ => 1 -| mvar _ _ => 2 -| succ _ _ => 3 -| max _ _ _ => 4 -| imax _ _ _ => 5 +| zero .. => 0 +| param .. => 1 +| mvar .. => 2 +| succ .. => 3 +| max .. => 4 +| imax .. => 5 /- TODO: use well founded recursion. -/ partial def normLtAux : Level → Nat → Level → Nat → Bool -| succ l₁ _, k₁, l₂, k₂ => normLtAux l₁ (k₁+1) l₂ k₂ -| l₁, k₁, succ l₂ _, k₂ => normLtAux l₁ k₁ l₂ (k₂+1) -| l₁@(max l₁₁ l₁₂ _), k₁, l₂@(max l₂₁ l₂₂ _), k₂ => - if l₁ == l₂ then k₁ < k₂ - else if l₁₁ == l₂₁ then normLtAux l₁₁ 0 l₂₁ 0 - else normLtAux l₁₂ 0 l₂₂ 0 -| l₁@(imax l₁₁ l₁₂ _), k₁, l₂@(imax l₂₁ l₂₂ _), k₂ => - if l₁ == l₂ then k₁ < k₂ - else if l₁₁ == l₂₁ then normLtAux l₁₁ 0 l₂₁ 0 - else normLtAux l₁₂ 0 l₂₂ 0 -| param n₁ _, k₁, param n₂ _, k₂ => if n₁ == n₂ then k₁ < k₂ else Name.lt n₁ n₂ -- use Name.lt because it is lexicographical -| mvar n₁ _, k₁, mvar n₂ _, k₂ => if n₁ == n₂ then k₁ < k₂ else Name.quickLt n₁ n₂ -- metavariables are temporary, the actual order doesn't matter -| l₁, k₁, l₂, k₂ => if l₁ == l₂ then k₁ < k₂ else ctorToNat l₁ < ctorToNat l₂ + | succ l₁ _, k₁, l₂, k₂ => normLtAux l₁ (k₁+1) l₂ k₂ + | l₁, k₁, succ l₂ _, k₂ => normLtAux l₁ k₁ l₂ (k₂+1) + | l₁@(max l₁₁ l₁₂ _), k₁, l₂@(max l₂₁ l₂₂ _), k₂ => + if l₁ == l₂ then k₁ < k₂ + else if l₁₁ == l₂₁ then normLtAux l₁₁ 0 l₂₁ 0 + else normLtAux l₁₂ 0 l₂₂ 0 + | l₁@(imax l₁₁ l₁₂ _), k₁, l₂@(imax l₂₁ l₂₂ _), k₂ => + if l₁ == l₂ then k₁ < k₂ + else if l₁₁ == l₂₁ then normLtAux l₁₁ 0 l₂₁ 0 + else normLtAux l₁₂ 0 l₂₂ 0 + | param n₁ _, k₁, param n₂ _, k₂ => if n₁ == n₂ then k₁ < k₂ else Name.lt n₁ n₂ -- use Name.lt because it is lexicographical + | mvar n₁ _, k₁, mvar n₂ _, k₂ => if n₁ == n₂ then k₁ < k₂ else Name.quickLt n₁ n₂ -- metavariables are temporary, the actual order doesn't matter + | l₁, k₁, l₂, k₂ => if l₁ == l₂ then k₁ < k₂ else ctorToNat l₁ < ctorToNat l₂ /-- A total order on level expressions that has the following properties @@ -241,30 +241,30 @@ partial def normLtAux : Level → Nat → Level → Nat → Bool - `zero` is the minimal element. This total order is used in the normalization procedure. -/ def normLt (l₁ l₂ : Level) : Bool := -normLtAux l₁ 0 l₂ 0 + normLtAux l₁ 0 l₂ 0 private def isAlreadyNormalizedCheap : Level → Bool -| zero _ => true -| param _ _ => true -| mvar _ _ => true -| succ u _ => isAlreadyNormalizedCheap u -| _ => false + | zero _ => true + | param _ _ => true + | mvar _ _ => true + | succ u _ => isAlreadyNormalizedCheap u + | _ => false /- Auxiliary function used at `normalize` -/ private def mkIMaxAux : Level → Level → Level -| _, u@(zero _) => u -| zero _, u => u -| u₁, u₂ => if u₁ == u₂ then u₁ else mkLevelIMax u₁ u₂ + | _, u@(zero _) => u + | zero _, u => u + | u₁, u₂ => if u₁ == u₂ then u₁ else mkLevelIMax u₁ u₂ /- Auxiliary function used at `normalize` -/ @[specialize] private partial def getMaxArgsAux (normalize : Level → Level) : Level → Bool → Array Level → Array Level -| max l₁ l₂ _, alreadyNormalized, lvls => getMaxArgsAux normalize l₂ alreadyNormalized (getMaxArgsAux normalize l₁ alreadyNormalized lvls) -| l, false, lvls => getMaxArgsAux normalize (normalize l) true lvls -| l, true, lvls => lvls.push l + | max l₁ l₂ _, alreadyNormalized, lvls => getMaxArgsAux normalize l₂ alreadyNormalized (getMaxArgsAux normalize l₁ alreadyNormalized lvls) + | l, false, lvls => getMaxArgsAux normalize (normalize l) true lvls + | l, true, lvls => lvls.push l private def accMax (result : Level) (prev : Level) (offset : Nat) : Level := -if result.isZero then prev.addOffset offset -else mkLevelMax result (prev.addOffset offset) + if result.isZero then prev.addOffset offset + else mkLevelMax result (prev.addOffset offset) /- Auxiliary function used at `normalize`. Remarks: @@ -275,26 +275,26 @@ else mkLevelMax result (prev.addOffset offset) - `result` is the accumulator -/ private partial def mkMaxAux (lvls : Array Level) (extraK : Nat) (i : Nat) (prev : Level) (prevK : Nat) (result : Level) : Level := -if h : i < lvls.size then - let lvl := lvls.get ⟨i, h⟩ - let curr := lvl.getLevelOffset - let currK := lvl.getOffset - if curr == prev then - mkMaxAux lvls extraK (i+1) curr currK result + if h : i < lvls.size then + let lvl := lvls.get ⟨i, h⟩ + let curr := lvl.getLevelOffset + let currK := lvl.getOffset + if curr == prev then + mkMaxAux lvls extraK (i+1) curr currK result + else + mkMaxAux lvls extraK (i+1) curr currK (accMax result prev (extraK + prevK)) else - mkMaxAux lvls extraK (i+1) curr currK (accMax result prev (extraK + prevK)) -else - accMax result prev (extraK + prevK) + accMax result prev (extraK + prevK) /- Auxiliary function for `normalize`. It assumes `lvls` has been sorted using `normLt`. It finds the first position that is not an explicit universe. -/ private partial def skipExplicit (lvls : Array Level) (i : Nat) : Nat := -if h : i < lvls.size then - let lvl := lvls.get ⟨i, h⟩ - if lvl.getLevelOffset.isZero then skipExplicit lvls (i+1) else i -else - i + if h : i < lvls.size then + let lvl := lvls.get ⟨i, h⟩ + if lvl.getLevelOffset.isZero then skipExplicit lvls (i+1) else i + else + i /- Auxiliary function for `normalize`. @@ -303,19 +303,19 @@ else `i` starts at the first non explict level. It assumes `lvls` has been sorted using `normLt`. -/ private partial def isExplicitSubsumedAux (lvls : Array Level) (maxExplicit : Nat) (i : Nat) : Bool := -if h : i < lvls.size then - let lvl := lvls.get ⟨i, h⟩ - if lvl.getOffset ≥ maxExplicit then true - else isExplicitSubsumedAux lvls maxExplicit (i+1) -else - false + if h : i < lvls.size then + let lvl := lvls.get ⟨i, h⟩ + if lvl.getOffset ≥ maxExplicit then true + else isExplicitSubsumedAux lvls maxExplicit (i+1) + else + false /- Auxiliary function for `normalize`. See `isExplicitSubsumedAux` -/ private def isExplicitSubsumed (lvls : Array Level) (firstNonExplicit : Nat) : Bool := -if firstNonExplicit == 0 then false -else - let max := (lvls.get! (firstNonExplicit - 1)).getOffset; - isExplicitSubsumedAux lvls max firstNonExplicit + if firstNonExplicit == 0 then false + else + let max := (lvls.get! (firstNonExplicit - 1)).getOffset; + isExplicitSubsumedAux lvls max firstNonExplicit partial def normalize (l : Level) : Level := if isAlreadyNormalizedCheap l then l @@ -344,74 +344,74 @@ partial def normalize (l : Level) : Level := /- Return true if `u` and `v` denote the same level. Check is currently incomplete. -/ def isEquiv (u v : Level) : Bool := -u == v || u.normalize == v.normalize + u == v || u.normalize == v.normalize /-- Reduce (if possible) universe level by 1 -/ def dec : Level → Option Level -| zero _ => none -| param _ _ => none -| mvar _ _ => none -| succ l _ => l -| max l₁ l₂ _ => mkLevelMax <$> dec l₁ <*> dec l₂ -/- Remark: `mkLevelMax` in the following line is not a typo. - If `dec l₂` succeeds, then `imax l₁ l₂` is equivalent to `max l₁ l₂`. -/ -| imax l₁ l₂ _ => mkLevelMax <$> dec l₁ <*> dec l₂ + | zero _ => none + | param _ _ => none + | mvar _ _ => none + | succ l _ => l + | max l₁ l₂ _ => mkLevelMax <$> dec l₁ <*> dec l₂ + /- Remark: `mkLevelMax` in the following line is not a typo. + If `dec l₂` succeeds, then `imax l₁ l₂` is equivalent to `max l₁ l₂`. -/ + | imax l₁ l₂ _ => mkLevelMax <$> dec l₁ <*> dec l₂ /- Level to Format -/ namespace LevelToFormat inductive Result -| leaf : Format → Result -| num : Nat → Result -| offset : Result → Nat → Result -| maxNode : List Result → Result -| imaxNode : List Result → Result + | leaf : Format → Result + | num : Nat → Result + | offset : Result → Nat → Result + | maxNode : List Result → Result + | imaxNode : List Result → Result def Result.succ : Result → Result -| Result.offset f k => Result.offset f (k+1) -| Result.num k => Result.num (k+1) -| f => Result.offset f 1 + | Result.offset f k => Result.offset f (k+1) + | Result.num k => Result.num (k+1) + | f => Result.offset f 1 def Result.max : Result → Result → Result -| f, Result.maxNode Fs => Result.maxNode (f::Fs) -| f₁, f₂ => Result.maxNode [f₁, f₂] + | f, Result.maxNode Fs => Result.maxNode (f::Fs) + | f₁, f₂ => Result.maxNode [f₁, f₂] def Result.imax : Result → Result → Result -| f, Result.imaxNode Fs => Result.imaxNode (f::Fs) -| f₁, f₂ => Result.imaxNode [f₁, f₂] + | f, Result.imaxNode Fs => Result.imaxNode (f::Fs) + | f₁, f₂ => Result.imaxNode [f₁, f₂] def parenIfFalse : Format → Bool → Format -| f, true => f -| f, false => f.paren + | f, true => f + | f, false => f.paren @[specialize] private def formatLst (fmt : Result → Format) : List Result → Format -| [] => Format.nil -| r::rs => Format.line ++ fmt r ++ formatLst fmt rs + | [] => Format.nil + | r::rs => Format.line ++ fmt r ++ formatLst fmt rs partial def Result.format : Result → Bool → Format -| Result.leaf f, _ => f -| Result.num k, _ => toString k -| Result.offset f 0, r => format f r -| Result.offset f (k+1), r => - let f' := format f false; - parenIfFalse (f' ++ "+" ++ fmt (k+1)) r -| Result.maxNode fs, r => parenIfFalse (Format.group $ "max" ++ formatLst (fun r => format r false) fs) r -| Result.imaxNode fs, r => parenIfFalse (Format.group $ "imax" ++ formatLst (fun r => format r false) fs) r + | Result.leaf f, _ => f + | Result.num k, _ => toString k + | Result.offset f 0, r => format f r + | Result.offset f (k+1), r => + let f' := format f false; + parenIfFalse (f' ++ "+" ++ fmt (k+1)) r + | Result.maxNode fs, r => parenIfFalse (Format.group $ "max" ++ formatLst (fun r => format r false) fs) r + | Result.imaxNode fs, r => parenIfFalse (Format.group $ "imax" ++ formatLst (fun r => format r false) fs) r def toResult : Level → Result -| zero _ => Result.num 0 -| succ l _ => Result.succ (toResult l) -| max l₁ l₂ _ => Result.max (toResult l₁) (toResult l₂) -| imax l₁ l₂ _ => Result.imax (toResult l₁) (toResult l₂) -| param n _ => Result.leaf (fmt n) -| mvar n _ => - let n := n.replacePrefix `_uniq `u; - Result.leaf ("?" ++ fmt n) + | zero _ => Result.num 0 + | succ l _ => Result.succ (toResult l) + | max l₁ l₂ _ => Result.max (toResult l₁) (toResult l₂) + | imax l₁ l₂ _ => Result.imax (toResult l₁) (toResult l₂) + | param n _ => Result.leaf (fmt n) + | mvar n _ => + let n := n.replacePrefix `_uniq `u; + Result.leaf ("?" ++ fmt n) end LevelToFormat protected def format (l : Level) : Format := -(LevelToFormat.toResult l).format true + (LevelToFormat.toResult l).format true instance : HasFormat Level := ⟨Level.format⟩ instance : HasToString Level := ⟨Format.pretty ∘ Level.format⟩ @@ -427,47 +427,47 @@ instance : HasToString Level := ⟨Format.pretty ∘ Level.format⟩ @[extern "lean_level_update_succ"] def updateSucc (lvl : Level) (newLvl : Level) (h : lvl.isSucc = true) : Level := -mkLevelSucc newLvl + mkLevelSucc newLvl @[inline] def updateSucc! (lvl : Level) (newLvl : Level) : Level := match lvl with -| succ lvl d => updateSucc (succ lvl d) newLvl rfl -| _ => panic! "succ level expected" + | succ lvl d => updateSucc (succ lvl d) newLvl rfl + | _ => panic! "succ level expected" @[extern "lean_level_update_max"] def updateMax (lvl : Level) (newLhs : Level) (newRhs : Level) (h : lvl.isMax = true) : Level := -mkLevelMax newLhs newRhs + mkLevelMax newLhs newRhs @[inline] def updateMax! (lvl : Level) (newLhs : Level) (newRhs : Level) : Level := -match lvl with -| max lhs rhs d => updateMax (max lhs rhs d) newLhs newRhs rfl -| _ => panic! "max level expected" + match lvl with + | max lhs rhs d => updateMax (max lhs rhs d) newLhs newRhs rfl + | _ => panic! "max level expected" @[extern "lean_level_update_imax"] def updateIMax (lvl : Level) (newLhs : Level) (newRhs : Level) (h : lvl.isIMax = true) : Level := -mkLevelIMax newLhs newRhs + mkLevelIMax newLhs newRhs @[inline] def updateIMax! (lvl : Level) (newLhs : Level) (newRhs : Level) : Level := -match lvl with -| imax lhs rhs d => updateIMax (imax lhs rhs d) newLhs newRhs rfl -| _ => panic! "imax level expected" + match lvl with + | imax lhs rhs d => updateIMax (imax lhs rhs d) newLhs newRhs rfl + | _ => panic! "imax level expected" def mkNaryMax : List Level → Level -| [] => levelZero -| [u] => u -| u::us => mkLevelMax u (mkNaryMax us) + | [] => levelZero + | [u] => u + | u::us => mkLevelMax u (mkNaryMax us) /- Level to Format -/ @[specialize] def instantiateParams (s : Name → Option Level) : Level → Level -| u@(zero _) => u -| u@(succ v _) => if u.hasParam then u.updateSucc! (instantiateParams s v) else u -| u@(max v₁ v₂ _) => if u.hasParam then u.updateMax! (instantiateParams s v₁) (instantiateParams s v₂) else u -| u@(imax v₁ v₂ _) => if u.hasParam then u.updateIMax! (instantiateParams s v₁) (instantiateParams s v₂) else u -| u@(param n _) => match s n with - | some u' => u' - | none => u -| u => u + | u@(zero _) => u + | u@(succ v _) => if u.hasParam then u.updateSucc! (instantiateParams s v) else u + | u@(max v₁ v₂ _) => if u.hasParam then u.updateMax! (instantiateParams s v₁) (instantiateParams s v₂) else u + | u@(imax v₁ v₂ _) => if u.hasParam then u.updateIMax! (instantiateParams s v₁) (instantiateParams s v₂) else u + | u@(param n _) => match s n with + | some u' => u' + | none => u + | u => u end Level @@ -482,4 +482,4 @@ abbrev PLevelSet := PersistentLevelSet end Lean abbrev Nat.toLevel (n : Nat) : Lean.Level := -Lean.Level.ofNat n + Lean.Level.ofNat n diff --git a/src/Lean/Modifiers.lean b/src/Lean/Modifiers.lean index 5c4087d4f9..15a4af5b75 100644 --- a/src/Lean/Modifiers.lean +++ b/src/Lean/Modifiers.lean @@ -12,11 +12,11 @@ builtin_initialize protectedExt : TagDeclarationExtension ← mkTagDeclarationEx @[export lean_add_protected] def addProtected (env : Environment) (n : Name) : Environment := -protectedExt.tag env n + protectedExt.tag env n @[export lean_is_protected] def isProtected (env : Environment) (n : Name) : Bool := -protectedExt.isTagged env n + protectedExt.isTagged env n builtin_initialize privateExt : EnvExtension Nat ← registerEnvExtension (pure 1) @@ -36,44 +36,44 @@ def privateHeader : Name := `_private @[export lean_mk_private_prefix] def mkUniquePrivatePrefix (env : Environment) : Environment × Name := -let idx := privateExt.getState env -let p := mkNameNum (privateHeader ++ env.mainModule) idx -let env := privateExt.setState env (idx+1) -(env, p) + let idx := privateExt.getState env + let p := mkNameNum (privateHeader ++ env.mainModule) idx + let env := privateExt.setState env (idx+1) + (env, p) @[export lean_mk_private_name] def mkUniquePrivateName (env : Environment) (n : Name) : Environment × Name := -let (env, p) := mkUniquePrivatePrefix env -(env, p ++ n) + let (env, p) := mkUniquePrivatePrefix env + (env, p ++ n) def mkPrivateName (env : Environment) (n : Name) : Name := -mkNameNum (privateHeader ++ env.mainModule) 0 ++ n + mkNameNum (privateHeader ++ env.mainModule) 0 ++ n def isPrivateName : Name → Bool -| n@(Name.str p _ _) => n == privateHeader || isPrivateName p -| Name.num p _ _ => isPrivateName p -| _ => false + | n@(Name.str p _ _) => n == privateHeader || isPrivateName p + | Name.num p _ _ => isPrivateName p + | _ => false @[export lean_is_private_name] def isPrivateNameExport (n : Name) : Bool := -isPrivateName n + isPrivateName n private def privateToUserNameAux : Name → Name -| Name.str p s _ => mkNameStr (privateToUserNameAux p) s -| _ => Name.anonymous + | Name.str p s _ => mkNameStr (privateToUserNameAux p) s + | _ => Name.anonymous @[export lean_private_to_user_name] def privateToUserName? (n : Name) : Option Name := -if isPrivateName n then privateToUserNameAux n -else none + if isPrivateName n then privateToUserNameAux n + else none private def privatePrefixAux : Name → Name -| Name.str p _ _ => privatePrefixAux p -| n => n + | Name.str p _ _ => privatePrefixAux p + | n => n @[export lean_private_prefix] def privatePrefix (n : Name) : Option Name := -if isPrivateName n then privatePrefixAux n -else none + if isPrivateName n then privatePrefixAux n + else none end Lean diff --git a/src/Lean/MonadEnv.lean b/src/Lean/MonadEnv.lean index dba50c21f8..8aec2f484b 100644 --- a/src/Lean/MonadEnv.lean +++ b/src/Lean/MonadEnv.lean @@ -14,107 +14,107 @@ section Methods variables {m : Type → Type} [MonadEnv m] def setEnv (env : Environment) : m Unit := -modifyEnv fun _ => env + modifyEnv fun _ => env @[inline] def withoutModifyingEnv [Monad m] [MonadFinally m] {α : Type} (x : m α) : m α := do -let env ← getEnv -try x finally setEnv env + let env ← getEnv + try x finally setEnv env @[inline] def matchConst [Monad m] {α : Type} (e : Expr) (failK : Unit → m α) (k : ConstantInfo → List Level → m α) : m α := do -match e with -| Expr.const constName us _ => do - match (← getEnv).find? constName with - | some cinfo => k cinfo us - | none => failK () -| _ => failK () + match e with + | Expr.const constName us _ => do + match (← getEnv).find? constName with + | some cinfo => k cinfo us + | none => failK () + | _ => failK () @[inline] def matchConstInduct [Monad m] {α : Type} (e : Expr) (failK : Unit → m α) (k : InductiveVal → List Level → m α) : m α := -matchConst e failK fun cinfo us => - match cinfo with - | ConstantInfo.inductInfo val => k val us - | _ => failK () + matchConst e failK fun cinfo us => + match cinfo with + | ConstantInfo.inductInfo val => k val us + | _ => failK () @[inline] def matchConstCtor [Monad m] {α : Type} (e : Expr) (failK : Unit → m α) (k : ConstructorVal → List Level → m α) : m α := -matchConst e failK fun cinfo us => - match cinfo with - | ConstantInfo.ctorInfo val => k val us - | _ => failK () + matchConst e failK fun cinfo us => + match cinfo with + | ConstantInfo.ctorInfo val => k val us + | _ => failK () @[inline] def matchConstRec [Monad m] {α : Type} (e : Expr) (failK : Unit → m α) (k : RecursorVal → List Level → m α) : m α := -matchConst e failK fun cinfo us => - match cinfo with - | ConstantInfo.recInfo val => k val us - | _ => failK () + matchConst e failK fun cinfo us => + match cinfo with + | ConstantInfo.recInfo val => k val us + | _ => failK () section variables [Monad m] def hasConst (constName : Name) : m Bool := do -return (← getEnv).contains constName + return (← getEnv).contains constName private partial def mkAuxNameAux (env : Environment) (base : Name) (i : Nat) : Name := -let candidate := base.appendIndexAfter i -if env.contains candidate then - mkAuxNameAux env base (i+1) -else - candidate + let candidate := base.appendIndexAfter i + if env.contains candidate then + mkAuxNameAux env base (i+1) + else + candidate def mkAuxName (baseName : Name) (idx : Nat) : m Name := do -return mkAuxNameAux (← getEnv) baseName idx + return mkAuxNameAux (← getEnv) baseName idx variables [MonadExceptOf Exception m] [Ref m] [AddErrorMessageContext m] def getConstInfo (constName : Name) : m ConstantInfo := do -match (← getEnv).find? constName with -| some info => pure info -| none => throwError! "unknown constant '{mkConst constName}'" + match (← getEnv).find? constName with + | some info => pure info + | none => throwError! "unknown constant '{mkConst constName}'" def getConstInfoInduct (constName : Name) : m InductiveVal := do -match (← getConstInfo constName) with -| ConstantInfo.inductInfo v => pure v -| _ => throwError! "'{mkConst constName}' is not a inductive type" + match (← getConstInfo constName) with + | ConstantInfo.inductInfo v => pure v + | _ => throwError! "'{mkConst constName}' is not a inductive type" def getConstInfoCtor (constName : Name) : m ConstructorVal := do -match (← getConstInfo constName) with -| ConstantInfo.ctorInfo v => pure v -| _ => throwError! "'{mkConst constName}' is not a constructor" + match (← getConstInfo constName) with + | ConstantInfo.ctorInfo v => pure v + | _ => throwError! "'{mkConst constName}' is not a constructor" def getConstInfoRec (constName : Name) : m RecursorVal := do -match (← getConstInfo constName) with -| ConstantInfo.recInfo v => pure v -| _ => throwError! "'{mkConst constName}' is not a recursor" + match (← getConstInfo constName) with + | ConstantInfo.recInfo v => pure v + | _ => throwError! "'{mkConst constName}' is not a recursor" @[inline] def matchConstStruct {α : Type} (e : Expr) (failK : Unit → m α) (k : InductiveVal → List Level → ConstructorVal → m α) : m α := -matchConstInduct e failK fun ival us => do - if ival.isRec then failK () - else match ival.ctors with - | [ctor] => - match (← getConstInfo ctor) with - | ConstantInfo.ctorInfo cval => k ival us cval + matchConstInduct e failK fun ival us => do + if ival.isRec then failK () + else match ival.ctors with + | [ctor] => + match (← getConstInfo ctor) with + | ConstantInfo.ctorInfo cval => k ival us cval + | _ => failK () | _ => failK () - | _ => failK () def addDecl [MonadOptions m] (decl : Declaration) : m Unit := do -match (← getEnv).addDecl decl with -| Except.ok env => setEnv env -| Except.error ex => throwKernelException ex + match (← getEnv).addDecl decl with + | Except.ok env => setEnv env + | Except.error ex => throwKernelException ex def compileDecl [MonadOptions m] (decl : Declaration) : m Unit := do -match (← getEnv).compileDecl (← getOptions) decl with -| Except.ok env => setEnv env -| Except.error ex => throwKernelException ex + match (← getEnv).compileDecl (← getOptions) decl with + | Except.ok env => setEnv env + | Except.error ex => throwKernelException ex def addAndCompile [MonadOptions m] (decl : Declaration) : m Unit := do -addDecl decl; -compileDecl decl + addDecl decl; + compileDecl decl variables [MonadExceptOf Exception m] [Ref m] [AddErrorMessageContext m] [MonadOptions m] unsafe def evalConst (α) (constName : Name) : m α := do -ofExcept $ (← getEnv).evalConst α (← getOptions) constName + ofExcept $ (← getEnv).evalConst α (← getOptions) constName unsafe def evalConstCheck (α) (typeName : Name) (constName : Name) : m α := do -ofExcept $ (← getEnv).evalConstCheck α (← getOptions) typeName constName + ofExcept $ (← getEnv).evalConstCheck α (← getOptions) typeName constName end diff --git a/src/Lean/PrettyPrinter.lean b/src/Lean/PrettyPrinter.lean index 3c0a38c99b..0dc664b66e 100644 --- a/src/Lean/PrettyPrinter.lean +++ b/src/Lean/PrettyPrinter.lean @@ -12,51 +12,51 @@ import Lean.Parser.Module namespace Lean def PPContext.runCoreM {α : Type} (ppCtx : PPContext) (x : CoreM α) : IO α := -Prod.fst <$> x.toIO { options := ppCtx.opts } { env := ppCtx.env } + Prod.fst <$> x.toIO { options := ppCtx.opts } { env := ppCtx.env } def PPContext.runMetaM {α : Type} (ppCtx : PPContext) (x : MetaM α) : IO α := -ppCtx.runCoreM $ x.run' { lctx := ppCtx.lctx } { mctx := ppCtx.mctx } + ppCtx.runCoreM $ x.run' { lctx := ppCtx.lctx } { mctx := ppCtx.mctx } namespace PrettyPrinter def ppTerm (stx : Syntax) : CoreM Format := do -let opts ← getOptions -let stx := (sanitizeSyntax stx).run' { options := opts } -parenthesizeTerm stx >>= formatTerm + let opts ← getOptions + let stx := (sanitizeSyntax stx).run' { options := opts } + parenthesizeTerm stx >>= formatTerm def ppExpr (currNamespace : Name) (openDecls : List OpenDecl) (e : Expr) : MetaM Format := do -let lctx ← getLCtx -let opts ← getOptions -let lctx := lctx.sanitizeNames.run' { options := opts } -Meta.withLCtx lctx #[] do - let stx ← delab currNamespace openDecls e - ppTerm stx + let lctx ← getLCtx + let opts ← getOptions + let lctx := lctx.sanitizeNames.run' { options := opts } + Meta.withLCtx lctx #[] do + let stx ← delab currNamespace openDecls e + ppTerm stx @[export lean_pp_expr] def ppExprLegacy (env : Environment) (mctx : MetavarContext) (lctx : LocalContext) (opts : Options) (e : Expr) : IO Format := -Prod.fst <$> ((ppExpr Name.anonymous [] e).run' { lctx := lctx } { mctx := mctx }).toIO { options := opts } { env := env } + Prod.fst <$> ((ppExpr Name.anonymous [] e).run' { lctx := lctx } { mctx := mctx }).toIO { options := opts } { env := env } def ppCommand (stx : Syntax) : CoreM Format := -parenthesizeCommand stx >>= formatCommand + parenthesizeCommand stx >>= formatCommand def ppModule (stx : Syntax) : CoreM Format := do -parenthesize Lean.Parser.Module.module.parenthesizer stx >>= format Lean.Parser.Module.module.formatter + parenthesize Lean.Parser.Module.module.parenthesizer stx >>= format Lean.Parser.Module.module.formatter private partial def noContext : MessageData → MessageData -| MessageData.withContext ctx msg => noContext msg -| MessageData.withNamingContext ctx msg => MessageData.withNamingContext ctx (noContext msg) -| MessageData.nest n msg => MessageData.nest n (noContext msg) -| MessageData.group msg => MessageData.group (noContext msg) -| MessageData.compose msg₁ msg₂ => MessageData.compose (noContext msg₁) (noContext msg₂) -| MessageData.tagged tag msg => MessageData.tagged tag (noContext msg) -| MessageData.node msgs => MessageData.node (msgs.map noContext) -| msg => msg + | MessageData.withContext ctx msg => noContext msg + | MessageData.withNamingContext ctx msg => MessageData.withNamingContext ctx (noContext msg) + | MessageData.nest n msg => MessageData.nest n (noContext msg) + | MessageData.group msg => MessageData.group (noContext msg) + | MessageData.compose msg₁ msg₂ => MessageData.compose (noContext msg₁) (noContext msg₂) + | MessageData.tagged tag msg => MessageData.tagged tag (noContext msg) + | MessageData.node msgs => MessageData.node (msgs.map noContext) + | msg => msg -- strip context (including environments with registered pretty printers) to prevent infinite recursion when pretty printing pretty printer error private def withoutContext {m} [MonadExcept Exception m] (x : m Format) : m Format := -tryCatch x fun - | Exception.error ref msg => throw $ Exception.error ref (noContext msg) - | ex => throw ex + tryCatch x fun + | Exception.error ref msg => throw $ Exception.error ref (noContext msg) + | ex => throw ex builtin_initialize ppFnsRef.set { diff --git a/src/Lean/ProjFns.lean b/src/Lean/ProjFns.lean index 07e6a1135b..75794659be 100644 --- a/src/Lean/ProjFns.lean +++ b/src/Lean/ProjFns.lean @@ -11,19 +11,19 @@ namespace Lean /- Given a structure `S`, Lean automatically creates an auxiliary definition (projection function) for each field. This structure caches information about these auxiliary definitions. -/ structure ProjectionFunctionInfo := -(ctorName : Name) -- Constructor associated with the auxiliary projection function. -(nparams : Nat) -- Number of parameters in the structure -(i : Nat) -- The field index associated with the auxiliary projection function. -(fromClass : Bool) -- `true` if the structure is a class + (ctorName : Name) -- Constructor associated with the auxiliary projection function. + (nparams : Nat) -- Number of parameters in the structure + (i : Nat) -- The field index associated with the auxiliary projection function. + (fromClass : Bool) -- `true` if the structure is a class @[export lean_mk_projection_info] def mkProjectionInfoEx (ctorName : Name) (nparams : Nat) (i : Nat) (fromClass : Bool) : ProjectionFunctionInfo := -{ctorName := ctorName, nparams := nparams, i := i, fromClass := fromClass } + {ctorName := ctorName, nparams := nparams, i := i, fromClass := fromClass } @[export lean_projection_info_from_class] -def ProjectionFunctionInfo.fromClassEx (info : ProjectionFunctionInfo) : Bool := info.fromClass + def ProjectionFunctionInfo.fromClassEx (info : ProjectionFunctionInfo) : Bool := info.fromClass instance : Inhabited ProjectionFunctionInfo := -⟨{ ctorName := arbitrary _, nparams := arbitrary _, i := 0, fromClass := false }⟩ + ⟨{ ctorName := arbitrary _, nparams := arbitrary _, i := 0, fromClass := false }⟩ builtin_initialize projectionFnInfoExt : SimplePersistentEnvExtension (Name × ProjectionFunctionInfo) (NameMap ProjectionFunctionInfo) ← registerSimplePersistentEnvExtension { @@ -35,32 +35,32 @@ builtin_initialize projectionFnInfoExt : SimplePersistentEnvExtension (Name × P @[export lean_add_projection_info] def addProjectionFnInfo (env : Environment) (projName : Name) (ctorName : Name) (nparams : Nat) (i : Nat) (fromClass : Bool) : Environment := -projectionFnInfoExt.addEntry env (projName, { ctorName := ctorName, nparams := nparams, i := i, fromClass := fromClass }) + projectionFnInfoExt.addEntry env (projName, { ctorName := ctorName, nparams := nparams, i := i, fromClass := fromClass }) namespace Environment @[export lean_get_projection_info] def getProjectionFnInfo? (env : Environment) (projName : Name) : Option ProjectionFunctionInfo := -match env.getModuleIdxFor? projName with -| some modIdx => - match (projectionFnInfoExt.getModuleEntries env modIdx).binSearch (projName, arbitrary _) (fun a b => Name.quickLt a.1 b.1) with - | some e => some e.2 - | none => none -| none => (projectionFnInfoExt.getState env).find? projName + match env.getModuleIdxFor? projName with + | some modIdx => + match (projectionFnInfoExt.getModuleEntries env modIdx).binSearch (projName, arbitrary _) (fun a b => Name.quickLt a.1 b.1) with + | some e => some e.2 + | none => none + | none => (projectionFnInfoExt.getState env).find? projName def isProjectionFn (env : Environment) (n : Name) : Bool := -match env.getModuleIdxFor? n with -| some modIdx => (projectionFnInfoExt.getModuleEntries env modIdx).binSearchContains (n, arbitrary _) (fun a b => Name.quickLt a.1 b.1) -| none => (projectionFnInfoExt.getState env).contains n + match env.getModuleIdxFor? n with + | some modIdx => (projectionFnInfoExt.getModuleEntries env modIdx).binSearchContains (n, arbitrary _) (fun a b => Name.quickLt a.1 b.1) + | none => (projectionFnInfoExt.getState env).contains n /-- If `projName` is the name of a projection function, return the associated structure name -/ def getProjectionStructureName? (env : Environment) (projName : Name) : Option Name := -match env.getProjectionFnInfo? projName with -| none => none -| some projInfo => - match env.find? projInfo.ctorName with - | some (ConstantInfo.ctorInfo val) => some val.induct - | _ => none + match env.getProjectionFnInfo? projName with + | none => none + | some projInfo => + match env.find? projInfo.ctorName with + | some (ConstantInfo.ctorInfo val) => some val.induct + | _ => none end Environment end Lean diff --git a/src/Lean/ReducibilityAttrs.lean b/src/Lean/ReducibilityAttrs.lean index 91f69c2bea..5c6de7d11a 100644 --- a/src/Lean/ReducibilityAttrs.lean +++ b/src/Lean/ReducibilityAttrs.lean @@ -9,7 +9,7 @@ import Lean.Attributes namespace Lean inductive ReducibilityStatus -| reducible | semireducible | irreducible + | reducible | semireducible | irreducible instance : Inhabited ReducibilityStatus := ⟨ReducibilityStatus.semireducible⟩ @@ -21,19 +21,19 @@ builtin_initialize reducibilityAttrs : EnumAttributes ReducibilityStatus ← @[export lean_get_reducibility_status] def getReducibilityStatus (env : Environment) (n : Name) : ReducibilityStatus := -match reducibilityAttrs.getValue env n with -| some s => s -| none => ReducibilityStatus.semireducible + match reducibilityAttrs.getValue env n with + | some s => s + | none => ReducibilityStatus.semireducible @[export lean_set_reducibility_status] def setReducibilityStatus (env : Environment) (n : Name) (s : ReducibilityStatus) : Environment := -match reducibilityAttrs.setValue env n s with -| Except.ok env => env -| _ => env -- TODO(Leo): we should extend EnumAttributes.setValue in the future and ensure it never fails + match reducibilityAttrs.setValue env n s with + | Except.ok env => env + | _ => env -- TODO(Leo): we should extend EnumAttributes.setValue in the future and ensure it never fails def isReducible (env : Environment) (n : Name) : Bool := -match getReducibilityStatus env n with -| ReducibilityStatus.reducible => true -| _ => false + match getReducibilityStatus env n with + | ReducibilityStatus.reducible => true + | _ => false end Lean diff --git a/src/Lean/ResolveName.lean b/src/Lean/ResolveName.lean index c639b6e14e..9248beb5ec 100644 --- a/src/Lean/ResolveName.lean +++ b/src/Lean/ResolveName.lean @@ -18,9 +18,9 @@ abbrev AliasState := SMap Name (List Name) abbrev AliasEntry := Name × Name def addAliasEntry (s : AliasState) (e : AliasEntry) : AliasState := -match s.find? e.1 with -| none => s.insert e.1 [e.2] -| some es => if es.elem e.2 then s else s.insert e.1 (e.2 :: es) + match s.find? e.1 with + | none => s.insert e.1 [e.2] + | some es => if es.elem e.2 then s else s.insert e.1 (e.2 :: es) builtin_initialize aliasExtension : SimplePersistentEnvExtension AliasEntry AliasState ← registerSimplePersistentEnvExtension { @@ -31,101 +31,101 @@ builtin_initialize aliasExtension : SimplePersistentEnvExtension AliasEntry Alia /- Add alias `a` for `e` -/ @[export lean_add_alias] def addAlias (env : Environment) (a : Name) (e : Name) : Environment := -aliasExtension.addEntry env (a, e) + aliasExtension.addEntry env (a, e) def getAliases (env : Environment) (a : Name) : List Name := -match aliasExtension.getState env $.find? a with -| none => [] -| some es => es + match aliasExtension.getState env $.find? a with + | none => [] + | some es => es -- slower, but only used in the pretty printer def getRevAliases (env : Environment) (e : Name) : List Name := -(aliasExtension.getState env).fold (fun as a es => if List.contains es e then a :: as else as) [] + (aliasExtension.getState env).fold (fun as a es => if List.contains es e then a :: as else as) [] /- Global name resolution -/ namespace ResolveName /- Check whether `ns ++ id` is a valid namepace name and/or there are aliases names `ns ++ id`. -/ private def resolveQualifiedName (env : Environment) (ns : Name) (id : Name) : List Name := -let resolvedId := ns ++ id -let resolvedIds := getAliases env resolvedId -if env.contains resolvedId && (!id.isAtomic || !isProtected env resolvedId) then - resolvedId :: resolvedIds -else - -- Check whether environment contains the private version. That is, `_private..ns.id`. - let resolvedIdPrv := mkPrivateName env resolvedId - if env.contains resolvedIdPrv then resolvedIdPrv :: resolvedIds - else resolvedIds + let resolvedId := ns ++ id + let resolvedIds := getAliases env resolvedId + if env.contains resolvedId && (!id.isAtomic || !isProtected env resolvedId) then + resolvedId :: resolvedIds + else + -- Check whether environment contains the private version. That is, `_private..ns.id`. + let resolvedIdPrv := mkPrivateName env resolvedId + if env.contains resolvedIdPrv then resolvedIdPrv :: resolvedIds + else resolvedIds /- Check surrounding namespaces -/ private def resolveUsingNamespace (env : Environment) (id : Name) : Name → List Name -| ns@(Name.str p _ _) => - match resolveQualifiedName env ns id with - | [] => resolveUsingNamespace env id p - | resolvedIds => resolvedIds -| _ => [] + | ns@(Name.str p _ _) => + match resolveQualifiedName env ns id with + | [] => resolveUsingNamespace env id p + | resolvedIds => resolvedIds + | _ => [] /- Check exact name -/ private def resolveExact (env : Environment) (id : Name) : Option Name := -if id.isAtomic then none -else - let resolvedId := id.replacePrefix rootNamespace Name.anonymous - if env.contains resolvedId then some resolvedId + if id.isAtomic then none else - -- We also allow `_root` when accessing private declarations. - -- If we change our minds, we should just replace `resolvedId` with `id` - let resolvedIdPrv := mkPrivateName env resolvedId - if env.contains resolvedIdPrv then some resolvedIdPrv - else none + let resolvedId := id.replacePrefix rootNamespace Name.anonymous + if env.contains resolvedId then some resolvedId + else + -- We also allow `_root` when accessing private declarations. + -- If we change our minds, we should just replace `resolvedId` with `id` + let resolvedIdPrv := mkPrivateName env resolvedId + if env.contains resolvedIdPrv then some resolvedIdPrv + else none /- Check open namespaces -/ private def resolveOpenDecls (env : Environment) (id : Name) : List OpenDecl → List Name → List Name -| [], resolvedIds => resolvedIds -| OpenDecl.simple ns exs :: openDecls, resolvedIds => - if exs.elem id then + | [], resolvedIds => resolvedIds + | OpenDecl.simple ns exs :: openDecls, resolvedIds => + if exs.elem id then + resolveOpenDecls env id openDecls resolvedIds + else + let newResolvedIds := resolveQualifiedName env ns id + resolveOpenDecls env id openDecls (newResolvedIds ++ resolvedIds) + | OpenDecl.explicit openedId resolvedId :: openDecls, resolvedIds => + let resolvedIds := if id == openedId then resolvedId :: resolvedIds else resolvedIds resolveOpenDecls env id openDecls resolvedIds - else - let newResolvedIds := resolveQualifiedName env ns id - resolveOpenDecls env id openDecls (newResolvedIds ++ resolvedIds) -| OpenDecl.explicit openedId resolvedId :: openDecls, resolvedIds => - let resolvedIds := if id == openedId then resolvedId :: resolvedIds else resolvedIds - resolveOpenDecls env id openDecls resolvedIds def resolveGlobalName (env : Environment) (ns : Name) (openDecls : List OpenDecl) (id : Name) : List (Name × List String) := --- decode macro scopes from name before recursion -let extractionResult := extractMacroScopes id -let rec loop : Name → List String → List (Name × List String) - | id@(Name.str p s _), projs => - -- NOTE: we assume that macro scopes always belong to the projected constant, not the projections - let id := { extractionResult with name := id }.review - match resolveUsingNamespace env id ns with - | resolvedIds@(_ :: _) => resolvedIds.eraseDups.map fun id => (id, projs) - | [] => - match resolveExact env id with - | some newId => [(newId, projs)] - | none => - let resolvedIds := if env.contains id then [id] else [] - let idPrv := mkPrivateName env id - let resolvedIds := if env.contains idPrv then [idPrv] ++ resolvedIds else resolvedIds - let resolvedIds := resolveOpenDecls env id openDecls resolvedIds - let resolvedIds := getAliases env id ++ resolvedIds - match resolvedIds with - | _ :: _ => resolvedIds.eraseDups.map fun id => (id, projs) - | [] => loop p (s::projs) - | _, _ => [] -loop extractionResult.name [] + -- decode macro scopes from name before recursion + let extractionResult := extractMacroScopes id + let rec loop : Name → List String → List (Name × List String) + | id@(Name.str p s _), projs => + -- NOTE: we assume that macro scopes always belong to the projected constant, not the projections + let id := { extractionResult with name := id }.review + match resolveUsingNamespace env id ns with + | resolvedIds@(_ :: _) => resolvedIds.eraseDups.map fun id => (id, projs) + | [] => + match resolveExact env id with + | some newId => [(newId, projs)] + | none => + let resolvedIds := if env.contains id then [id] else [] + let idPrv := mkPrivateName env id + let resolvedIds := if env.contains idPrv then [idPrv] ++ resolvedIds else resolvedIds + let resolvedIds := resolveOpenDecls env id openDecls resolvedIds + let resolvedIds := getAliases env id ++ resolvedIds + match resolvedIds with + | _ :: _ => resolvedIds.eraseDups.map fun id => (id, projs) + | [] => loop p (s::projs) + | _, _ => [] + loop extractionResult.name [] /- Namespace resolution -/ def resolveNamespaceUsingScope (env : Environment) (n : Name) : Name → Option Name -| Name.anonymous => none -| ns@(Name.str p _ _) => if env.isNamespace (ns ++ n) then some (ns ++ n) else resolveNamespaceUsingScope env n p -| _ => unreachable! + | Name.anonymous => none + | ns@(Name.str p _ _) => if env.isNamespace (ns ++ n) then some (ns ++ n) else resolveNamespaceUsingScope env n p + | _ => unreachable! def resolveNamespaceUsingOpenDecls (env : Environment) (n : Name) : List OpenDecl → Option Name -| [] => none -| OpenDecl.simple ns [] :: ds => if env.isNamespace (ns ++ n) then some (ns ++ n) else resolveNamespaceUsingOpenDecls env n ds -| _ :: ds => resolveNamespaceUsingOpenDecls env n ds + | [] => none + | OpenDecl.simple ns [] :: ds => if env.isNamespace (ns ++ n) then some (ns ++ n) else resolveNamespaceUsingOpenDecls env n ds + | _ :: ds => resolveNamespaceUsingOpenDecls env n ds /- Given a name `id` try to find namespace it refers to. The resolution procedure works as follows @@ -136,24 +136,25 @@ Given a name `id` try to find namespace it refers to. The resolution procedure w We search "backwards" again. That is, we try the most recent `open` command first. We only consider simple `open` commands. -/ def resolveNamespace? (env : Environment) (ns : Name) (openDecls : List OpenDecl) (id : Name) : Option Name := -if env.isNamespace id then some id -else match resolveNamespaceUsingScope env id ns with - | some n => some n - | none => - match resolveNamespaceUsingOpenDecls env id openDecls with + if env.isNamespace id then some id + else match resolveNamespaceUsingScope env id ns with | some n => some n - | none => none -end ResolveName + | none => + match resolveNamespaceUsingOpenDecls env id openDecls with + | some n => some n + | none => none + end ResolveName class MonadResolveName (m : Type → Type) := -(getCurrNamespace : m Name) -(getOpenDecls : m (List OpenDecl)) + (getCurrNamespace : m Name) + (getOpenDecls : m (List OpenDecl)) export MonadResolveName (getCurrNamespace getOpenDecls) -instance (m n) [MonadResolveName m] [MonadLift m n] : MonadResolveName n := -{ getCurrNamespace := liftM (getCurrNamespace : m _), - getOpenDecls := liftM (getOpenDecls : m _) } +instance (m n) [MonadResolveName m] [MonadLift m n] : MonadResolveName n := { + getCurrNamespace := liftM (getCurrNamespace : m _), + getOpenDecls := liftM (getOpenDecls : m _) +} section Methods @@ -182,27 +183,27 @@ variables {m : Type → Type} [Monad m] [MonadResolveName m] [MonadEnv m] - `resolveGlobalName x.z.w` => `[(Foo.x, [z, w]), (Boo.x, [z, w])]` -/ def resolveGlobalName (id : Name) : m (List (Name × List String)) := do -return ResolveName.resolveGlobalName (← getEnv) (← getCurrNamespace) (← getOpenDecls) id + return ResolveName.resolveGlobalName (← getEnv) (← getCurrNamespace) (← getOpenDecls) id variables [MonadExceptOf Exception m] [Ref m] [AddErrorMessageContext m] def resolveNamespace (id : Name) : m Name := do -match ResolveName.resolveNamespace? (← getEnv) (← getCurrNamespace) (← getOpenDecls) id with -| some ns => return ns -| none => throwError s!"unknown namespace '{id}'" + match ResolveName.resolveNamespace? (← getEnv) (← getCurrNamespace) (← getOpenDecls) id with + | some ns => return ns + | none => throwError s!"unknown namespace '{id}'" /- Similar to `resolveGlobalName`, but discard any candidate whose `fieldList` is not empty. -/ def resolveGlobalConst (n : Name) : m (List Name) := do -let cs ← resolveGlobalName n -let cs := cs.filter fun (_, fieldList) => fieldList.isEmpty -if cs.isEmpty then throwUnknownConstant n -return cs.map (·.1) + let cs ← resolveGlobalName n + let cs := cs.filter fun (_, fieldList) => fieldList.isEmpty + if cs.isEmpty then throwUnknownConstant n + return cs.map (·.1) def resolveGlobalConstNoOverload (n : Name) : m Name := do -let cs ← resolveGlobalConst n -match cs with -| [c] => pure c -| _ => throwError s!"ambiguous identifier '{mkConst n}', possible interpretations: {cs.map mkConst}" + let cs ← resolveGlobalConst n + match cs with + | [c] => pure c + | _ => throwError s!"ambiguous identifier '{mkConst n}', possible interpretations: {cs.map mkConst}" end Methods end Lean