From c768a247357ebd446a3312db9371af007ad80e91 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 14 Nov 2019 15:44:17 -0800 Subject: [PATCH] chore: `mkApp` => `mkAppN` We are goint to use `mkApp` for creating unary applications --- library/Init/Lean/Compiler/ConstFolding.lean | 6 +- library/Init/Lean/Elaborator/Basic.lean | 2 +- library/Init/Lean/Expr.lean | 34 ++++++--- library/Init/Lean/Parser/Parser.lean | 2 +- library/Init/Lean/ToExpr.lean | 4 +- library/Init/Lean/TypeClass/Synth.lean | 6 +- library/Init/Lean/WHNF.lean | 2 +- tests/lean/mvar1.lean | 62 ++++++++-------- tests/lean/mvar2.lean | 42 +++++------ tests/lean/mvar3.lean | 36 +++++----- tests/lean/run/expr1.lean | 58 +++++++-------- tests/lean/run/meta1.lean | 76 ++++++++++---------- tests/lean/typeclass_context.lean | 18 ++--- 13 files changed, 180 insertions(+), 168 deletions(-) diff --git a/library/Init/Lean/Compiler/ConstFolding.lean b/library/Init/Lean/Compiler/ConstFolding.lean index 2dd70fb11a..87a04ae81a 100644 --- a/library/Init/Lean/Compiler/ConstFolding.lean +++ b/library/Init/Lean/Compiler/ConstFolding.lean @@ -89,13 +89,13 @@ def foldNatMod (_ : Bool) := foldNatBinOp HasMod.mod def foldNatPow (_ : Bool) := foldNatBinOp HasPow.pow def mkNatEq (a b : Expr) : Expr := -mkBinApp (Expr.app (Expr.const `Eq [Level.one]) (Expr.const `Nat [])) a b +mkAppB (Expr.app (Expr.const `Eq [Level.one]) (Expr.const `Nat [])) a b def mkNatLt (a b : Expr) : Expr := -mkBinApp (mkBinApp (Expr.const `HasLt.lt [Level.zero]) (Expr.const `Nat []) (Expr.const `Nat.HasLt [])) a b +mkAppB (mkAppB (Expr.const `HasLt.lt [Level.zero]) (Expr.const `Nat []) (Expr.const `Nat.HasLt [])) a b def mkNatLe (a b : Expr) : Expr := -mkBinApp (mkBinApp (Expr.const `HasLt.le [Level.zero]) (Expr.const `Nat []) (Expr.const `Nat.HasLe [])) a b +mkAppB (mkAppB (Expr.const `HasLt.le [Level.zero]) (Expr.const `Nat []) (Expr.const `Nat.HasLe [])) a b def toDecidableExpr (beforeErasure : Bool) (pred : Expr) (r : Bool) : Expr := match beforeErasure, r with diff --git a/library/Init/Lean/Elaborator/Basic.lean b/library/Init/Lean/Elaborator/Basic.lean index e881023486..695cc35f8f 100644 --- a/library/Init/Lean/Elaborator/Basic.lean +++ b/library/Init/Lean/Elaborator/Basic.lean @@ -123,7 +123,7 @@ match attrParamSyntaxToIdentifier arg with def declareBuiltinElab (env : Environment) (addFn : Name) (kind : SyntaxNodeKind) (declName : Name) : IO Environment := let name := `_regBuiltinTermElab ++ declName; let type := Expr.app (mkConst `IO) (mkConst `Unit); -let val := mkCApp addFn #[toExpr kind, toExpr declName, mkConst declName]; +let val := mkCAppN addFn #[toExpr kind, toExpr declName, 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 diff --git a/library/Init/Lean/Expr.lean b/library/Init/Lean/Expr.lean index 74e39ce88f..8db2f560a4 100644 --- a/library/Init/Lean/Expr.lean +++ b/library/Init/Lean/Expr.lean @@ -87,7 +87,22 @@ def type : Literal → Expr | strVal _ => Expr.const `String [] end Literal -def mkApp (f : Expr) (args : Array Expr) : Expr := +def mkConst (n : Name) (ls : List Level := []) : Expr := +Expr.const n ls + +def mkBVar (idx : Nat) : Expr := +Expr.bvar idx + +def mkSort (lvl : Level) : Expr := +Expr.sort lvl + +def mkFVar (fvarId : Name) : Expr := +Expr.fvar fvarId + +def mkMVar (fvarId : Name) : Expr := +Expr.mvar fvarId + +def mkAppN (f : Expr) (args : Array Expr) : Expr := args.foldl Expr.app f private partial def mkAppRangeAux (n : Nat) (args : Array Expr) : Nat → Expr → Expr @@ -97,9 +112,6 @@ private partial def mkAppRangeAux (n : Nat) (args : Array Expr) : Nat → Expr def mkAppRange (f : Expr) (i j : Nat) (args : Array Expr) : Expr := mkAppRangeAux j args i f -def mkCApp (fn : Name) (args : Array Expr) : Expr := -mkApp (Expr.const fn []) args - def mkAppRev (fn : Expr) (revArgs : Array Expr) : Expr := revArgs.foldr (fun a r => Expr.app r a) fn @@ -364,20 +376,20 @@ instance : HasRepr Expr := end Expr -def mkConst (n : Name) (ls : List Level := []) : Expr := -Expr.const n ls +def mkCAppN (n : Name) (args : Array Expr) : Expr := +mkAppN (mkConst n) args -def mkBinApp (f a b : Expr) := +def mkAppB (f a b : Expr) := Expr.app (Expr.app f a) b -def mkBinCApp (f : Name) (a b : Expr) := -mkBinApp (mkConst f) a b +def mkCAppB (n : Name) (a b : Expr) := +Expr.app (Expr.app (mkConst n) a) b def mkDecIsTrue (pred proof : Expr) := -mkBinApp (Expr.const `Decidable.isTrue []) pred proof +mkAppB (Expr.const `Decidable.isTrue []) pred proof def mkDecIsFalse (pred proof : Expr) := -mkBinApp (Expr.const `Decidable.isFalse []) pred proof +mkAppB (Expr.const `Decidable.isFalse []) pred proof abbrev ExprMap (α : Type) := HashMap Expr α abbrev PersistentExprMap (α : Type) := PHashMap Expr α diff --git a/library/Init/Lean/Parser/Parser.lean b/library/Init/Lean/Parser/Parser.lean index a0d896cb1a..b181f258dd 100644 --- a/library/Init/Lean/Parser/Parser.lean +++ b/library/Init/Lean/Parser/Parser.lean @@ -1443,7 +1443,7 @@ do tables ← tablesRef.get; def declareBuiltinParser (env : Environment) (addFnName : Name) (refDeclName : Name) (declName : Name) : IO Environment := let name := `_regBuiltinParser ++ declName; let type := Expr.app (mkConst `IO) (mkConst `Unit); -let val := mkCApp addFnName #[mkConst refDeclName, toExpr declName, mkConst declName]; +let val := mkCAppN addFnName #[mkConst refDeclName, toExpr declName, 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 diff --git a/library/Init/Lean/ToExpr.lean b/library/Init/Lean/ToExpr.lean index 9bea2784c0..b4378131a0 100644 --- a/library/Init/Lean/ToExpr.lean +++ b/library/Init/Lean/ToExpr.lean @@ -22,8 +22,8 @@ instance strToExpr : ToExpr String := ⟨fun s => Expr.lit (Literal.strVal s)⟩ def nameToExprAux : Name → Expr | Name.anonymous => mkConst `Lean.Name.anonymous -| Name.mkString p s => mkBinCApp `Lean.Name.mkString (nameToExprAux p) (toExpr s) -| Name.mkNumeral p n => mkBinCApp `Lean.Name.mkNumeral (nameToExprAux p) (toExpr n) +| Name.mkString p s => mkCAppB `Lean.Name.mkString (nameToExprAux p) (toExpr s) +| Name.mkNumeral p n => mkCAppB `Lean.Name.mkNumeral (nameToExprAux p) (toExpr n) instance nameToExpr : ToExpr Name := ⟨nameToExprAux⟩ diff --git a/library/Init/Lean/TypeClass/Synth.lean b/library/Init/Lean/TypeClass/Synth.lean index 31165e8b86..4058b75557 100644 --- a/library/Init/Lean/TypeClass/Synth.lean +++ b/library/Init/Lean/TypeClass/Synth.lean @@ -128,7 +128,7 @@ do let mvarType := ctx.eInstantiate (ctx.eInfer mvar); partial def introduceMVars (lctx : LocalContext) (locals : Array Expr) : Context → Expr → Expr → List Expr → Context × Expr × Expr × List Expr | ctx, instVal, Expr.forallE _ info domain body, mvars => do let ⟨mvar, ctx⟩ := (Context.eNewMeta $ lctx.mkForall locals domain).run ctx; - let arg := mkApp mvar locals; + let arg := mkAppN mvar locals; let instVal := Expr.app instVal arg; let instType := body.instantiate1 arg; let mvars := if info.isInstImplicit then mvar::mvars else mvars; @@ -279,7 +279,7 @@ def collectEReplacements (env : Environment) (lctx : LocalContext) (locals : Arr | Expr.forallE _ _ d b, arg::args, ctx, eReplacements, fArgs => if isOutParam d then let ⟨eMeta, ctx⟩ := (Context.eNewMeta $ lctx.mkForall locals d).run ctx; - let fArg : Expr := mkApp eMeta locals; + let fArg : Expr := mkAppN eMeta locals; collectEReplacements (b.instantiate1 fArg) args ctx (eReplacements.push (eMeta, arg)) (fArgs.push fArg) else collectEReplacements (b.instantiate1 arg) args ctx eReplacements (fArgs.push arg) @@ -303,7 +303,7 @@ else | none => panic! "found constant not in the environment" | some cInfo => cInfo.instantiateTypeLevelParams CLevels.toList; let (ctx, eReplacements, fArgs) := collectEReplacements env lctx locals fType fArgs.toList ctx #[] #[]; -- TODO: avoid fArgs.toList - (ctx, lctx.mkForall locals $ mkApp f fArgs, uReplacements, eReplacements) + (ctx, lctx.mkForall locals $ mkAppN f fArgs, uReplacements, eReplacements) def synth (goalType₀ : Expr) (fuel : Nat := 100000) : TCMethod Expr := do env ← get >>= λ ϕ => pure ϕ.env; diff --git a/library/Init/Lean/WHNF.lean b/library/Init/Lean/WHNF.lean index 2fe621abc4..76ae60cc12 100644 --- a/library/Init/Lean/WHNF.lean +++ b/library/Init/Lean/WHNF.lean @@ -47,7 +47,7 @@ private def mkNullaryCtor {m : Type → Type} [Monad m] match type.getAppFn with | Expr.const d lvls => do (some ctor) ← getFirstCtor getConst d | pure none; - pure $ mkApp (Expr.const ctor lvls) (type.getAppArgs.shrink nparams) + pure $ mkAppN (Expr.const ctor lvls) (type.getAppArgs.shrink nparams) | _ => pure none private def toCtorIfLit : Expr → Expr diff --git a/tests/lean/mvar1.lean b/tests/lean/mvar1.lean index dca48246e0..6a2cfa05ed 100644 --- a/tests/lean/mvar1.lean +++ b/tests/lean/mvar1.lean @@ -4,35 +4,35 @@ open Lean def check (b : Bool) : IO Unit := unless b (throw "error") -def f := Expr.const `f [] -def g := Expr.const `g [] -def a := Expr.const `a [] -def b := Expr.const `b [] -def c := Expr.const `c [] +def f := mkConst `f [] +def g := mkConst `g [] +def a := mkConst `a [] +def b := mkConst `b [] +def c := mkConst `c [] -def b0 := Expr.bvar 0 -def b1 := Expr.bvar 1 -def b2 := Expr.bvar 2 +def b0 := mkBVar 0 +def b1 := mkBVar 1 +def b2 := mkBVar 2 def u := Level.param `u -def typeE := Expr.sort Level.one -def natE := Expr.const `Nat [] -def boolE := Expr.const `Bool [] -def vecE := Expr.const `Vec [Level.zero] +def typeE := mkSort Level.one +def natE := mkConst `Nat [] +def boolE := mkConst `Bool [] +def vecE := mkConst `Vec [Level.zero] -def α := Expr.fvar `α -def x := Expr.fvar `x -def y := Expr.fvar `y -def z := Expr.fvar `z -def w := Expr.fvar `w +def α := mkFVar `α +def x := mkFVar `x +def y := mkFVar `y +def z := mkFVar `z +def w := mkFVar `w -def m1 := Expr.mvar `m1 -def m2 := Expr.mvar `m2 -def m3 := Expr.mvar `m3 -def m4 := Expr.mvar `m4 -def m5 := Expr.mvar `m5 -def m6 := Expr.mvar `m6 +def m1 := mkMVar `m1 +def m2 := mkMVar `m2 +def m3 := mkMVar `m3 +def m4 := mkMVar `m4 +def m5 := mkMVar `m5 +def m6 := mkMVar `m6 def bi := BinderInfo.default def arrow (d b : Expr) := Expr.forallE `_ bi d b @@ -41,10 +41,10 @@ def lctx1 : LocalContext := {} def lctx2 := lctx1.mkLocalDecl `α `α typeE def lctx3 := lctx2.mkLocalDecl `x `x natE def lctx4 := lctx3.mkLocalDecl `y `y α -def lctx5 := lctx4.mkLocalDecl `z `z (mkApp vecE #[x]) -def lctx6 := lctx5.mkLocalDecl `w `w (arrow natE (mkApp m6 #[α, x, y])) +def lctx5 := lctx4.mkLocalDecl `z `z (mkAppN vecE #[x]) +def lctx6 := lctx5.mkLocalDecl `w `w (arrow natE (mkAppN m6 #[α, x, y])) -def t1 := lctx5.mkLambda #[α, x, y] $ mkApp f #[α, mkApp g #[x, y], lctx5.mkLambda #[z] (Expr.app f z)] +def t1 := lctx5.mkLambda #[α, x, y] $ mkAppN f #[α, mkAppN g #[x, y], lctx5.mkLambda #[z] (Expr.app f z)] #eval check (!t1.hasFVar) #eval t1 @@ -56,10 +56,10 @@ def mctx5 := mctx4.addExprMVarDecl `m4 `m4 lctx1 (arrow typeE (arrow natE (arro def mctx6 := mctx5.addExprMVarDecl `m5 `m5 lctx5 typeE def mctx7 := mctx5.addExprMVarDecl `m6 `m6 lctx5 (arrow typeE (arrow natE (arrow α natE))) def mctx8 := mctx7.assignDelayed `m4 lctx4 #[α, x, y] m3 -def mctx9 := mctx8.assignExpr `m3 (mkApp g #[x, y]) +def mctx9 := mctx8.assignExpr `m3 (mkAppN g #[x, y]) def mctx10 := mctx9.assignExpr `m1 a -def t2 := lctx5.mkLambda #[α, x, y] $ mkApp f #[mkApp m4 #[α, x, y], x] +def t2 := lctx5.mkLambda #[α, x, y] $ mkAppN f #[mkAppN m4 #[α, x, y], x] #eval check (!t2.hasFVar) #eval t2 @@ -69,13 +69,13 @@ def t2 := lctx5.mkLambda #[α, x, y] $ mkApp f #[mkApp m4 #[α, x, y], x] #eval (mctx9.instantiateMVars t2).1 -- t3 is ill-formed since m3's localcontext contains ‵α`, `x` and `y` -def t3 := lctx5.mkLambda #[α, x, y] $ mkApp f #[m3, x] +def t3 := lctx5.mkLambda #[α, x, y] $ mkAppN f #[m3, x] #eval check (mctx10.instantiateMVars t3).1.hasFVar #eval (mctx7.instantiateMVars t3).1 def mkDiamond : Nat → Expr | 0 => m1 -| (n+1) => mkApp f #[mkDiamond n, mkDiamond n] +| (n+1) => mkAppN f #[mkDiamond n, mkDiamond n] #eval (mctx7.instantiateMVars (mkDiamond 3)).1 #eval (mctx10.instantiateMVars (mkDiamond 3)).1 @@ -85,7 +85,7 @@ def mkDiamond : Nat → Expr def mctx11 := mctx10.assignDelayed `m6 lctx5 #[α, x, y] m5 def mctx12 := mctx11.assignExpr `m5 (arrow α α) -def t4 := lctx6.mkLambda #[α, x, y, w] $ mkApp f #[mkApp m4 #[α, x, y], x] +def t4 := lctx6.mkLambda #[α, x, y, w] $ mkAppN f #[mkAppN m4 #[α, x, y], x] #eval t4 #eval (mctx9.instantiateMVars t4).1 diff --git a/tests/lean/mvar2.lean b/tests/lean/mvar2.lean index beb283407f..a3fcd5c790 100644 --- a/tests/lean/mvar2.lean +++ b/tests/lean/mvar2.lean @@ -4,32 +4,32 @@ open Lean def check (b : Bool) : IO Unit := unless b (throw "error") -def f := Expr.const `f [] -def g := Expr.const `g [] -def a := Expr.const `a [] -def b := Expr.const `b [] -def c := Expr.const `c [] +def f := mkConst `f [] +def g := mkConst `g [] +def a := mkConst `a [] +def b := mkConst `b [] +def c := mkConst `c [] -def b0 := Expr.bvar 0 -def b1 := Expr.bvar 1 -def b2 := Expr.bvar 2 +def b0 := mkBVar 0 +def b1 := mkBVar 1 +def b2 := mkBVar 2 def u := Level.param `u def typeE := Expr.sort Level.one -def natE := Expr.const `Nat [] -def boolE := Expr.const `Bool [] -def vecE := Expr.const `Vec [Level.zero] +def natE := mkConst `Nat [] +def boolE := mkConst `Bool [] +def vecE := mkConst `Vec [Level.zero] -def α := Expr.fvar `α -def x := Expr.fvar `x -def y := Expr.fvar `y -def z := Expr.fvar `z -def w := Expr.fvar `w +def α := mkFVar `α +def x := mkFVar `x +def y := mkFVar `y +def z := mkFVar `z +def w := mkFVar `w -def m1 := Expr.mvar `m1 -def m2 := Expr.mvar `m2 -def m3 := Expr.mvar `m3 +def m1 := mkMVar `m1 +def m2 := mkMVar `m2 +def m3 := mkMVar `m3 def bi := BinderInfo.default def arrow (d b : Expr) := Expr.forallE `_ bi d b @@ -37,7 +37,7 @@ def arrow (d b : Expr) := Expr.forallE `_ bi d b def lctx1 : LocalContext := {} def lctx2 := lctx1.mkLocalDecl `α `α typeE def lctx3 := lctx2.mkLocalDecl `x `x m1 -def lctx4 := lctx3.mkLocalDecl `y `y (arrow natE (mkApp m3 #[α, x])) +def lctx4 := lctx3.mkLocalDecl `y `y (arrow natE (mkAppN m3 #[α, x])) def mctx1 : MetavarContext := {} def mctx2 := mctx1.addExprMVarDecl `m1 `m1 lctx1 typeE @@ -47,7 +47,7 @@ def mctx5 := mctx4.assignDelayed `m3 lctx3 #[α, x] m2 def mctx6 := mctx5.assignExpr `m2 (arrow α α) def mctx7 := mctx6.assignExpr `m1 natE -def t2 := lctx4.mkLambda #[α, x, y] $ mkApp f #[mkApp m3 #[α, x], x] +def t2 := lctx4.mkLambda #[α, x, y] $ mkAppN f #[mkAppN m3 #[α, x], x] #eval check (!t2.hasFVar) #eval t2 diff --git a/tests/lean/mvar3.lean b/tests/lean/mvar3.lean index f5e94f53ab..bb0e62ef0d 100644 --- a/tests/lean/mvar3.lean +++ b/tests/lean/mvar3.lean @@ -10,28 +10,28 @@ match MetavarContext.mkLambda xs e lctx { mctx := mctx, ngen := ngen } with def check (b : Bool) : IO Unit := unless b (throw "error") -def f := Expr.const `f [] -def g := Expr.const `g [] -def a := Expr.const `a [] -def b := Expr.const `b [] -def c := Expr.const `c [] +def f := mkConst `f +def g := mkConst `g +def a := mkConst `a +def b := mkConst `b +def c := mkConst `c -def b0 := Expr.bvar 0 -def b1 := Expr.bvar 1 -def b2 := Expr.bvar 2 +def b0 := mkBVar 0 +def b1 := mkBVar 1 +def b2 := mkBVar 2 def u := Level.param `u def typeE := Expr.sort Level.one -def natE := Expr.const `Nat [] -def boolE := Expr.const `Bool [] -def vecE := Expr.const `Vec [Level.zero] +def natE := mkConst `Nat +def boolE := mkConst `Bool +def vecE := mkConst `Vec [Level.zero] -def α := Expr.fvar `α -def x := Expr.fvar `x -def y := Expr.fvar `y -def z := Expr.fvar `z -def w := Expr.fvar `w +def α := mkFVar `α +def x := mkFVar `x +def y := mkFVar `y +def z := mkFVar `z +def w := mkFVar `w def m1 := Expr.mvar `m1 def m2 := Expr.mvar `m2 @@ -52,7 +52,7 @@ def mctx4 := mctx3.addExprMVarDecl `m3 `m3 lctx3 natE def mctx4' := mctx3.addExprMVarDecl `m3 `m3 lctx3 natE true def R1 := -match mkLambda mctx4 {namePrefix := `n} lctx4 #[α, x, y] $ mkApp f #[m3, x] with +match mkLambda mctx4 {namePrefix := `n} lctx4 #[α, x, y] $ mkAppN f #[m3, x] with | Except.ok s => s | Except.error e => panic! (toString e) def e1 := R1.2.2 @@ -64,7 +64,7 @@ def mctx5 := R1.1 #eval check (!e1.hasFVar) def R2 := -match mkLambda mctx4' {namePrefix := `n} lctx4 #[α, x, y] $ mkApp f #[m3, y] with +match mkLambda mctx4' {namePrefix := `n} lctx4 #[α, x, y] $ mkAppN f #[m3, y] with | Except.ok s => s | Except.error e => panic! (toString e) def e2 := R2.2.2 diff --git a/tests/lean/run/expr1.lean b/tests/lean/run/expr1.lean index efaae84793..e3c13a5f80 100644 --- a/tests/lean/run/expr1.lean +++ b/tests/lean/run/expr1.lean @@ -2,10 +2,10 @@ import Init.Lean.Expr open Lean def tst1 : IO Unit := -do let f := Expr.const `f []; - let a := Expr.const `a []; - let b := Expr.const `b []; - let t := mkApp f #[a, b, b]; +do let f := mkConst `f []; + let a := mkConst `a []; + let b := mkConst `b []; + let t := mkAppN f #[a, b, b]; let as₁ := t.getAppArgs; let as₂ := t.getAppRevArgs; IO.println as₁; @@ -26,11 +26,11 @@ do let l1 := Level.max (Level.param `a) (Level.param `b); #eval tst2 def tst3 : IO Unit := -do let f := Expr.const `f []; - let a := Expr.const `a []; - let b := Expr.const `b []; - let c := Expr.const `c []; - let t := mkApp f #[a, b, c]; +do let f := mkConst `f []; + let a := mkConst `a []; + let b := mkConst `b []; + let c := mkConst `c []; + let t := mkAppN f #[a, b, c]; IO.println $ t.getArg! 0; IO.println $ t.getArg! 1; IO.println $ t.getArg! 2; @@ -40,15 +40,15 @@ do let f := Expr.const `f []; def tst4 : IO Unit := -do let f := Expr.const `f []; - let a := Expr.const `a []; - let b := Expr.const `b []; - let x0 := Expr.bvar 0; - let x1 := Expr.bvar 1; - let t1 := mkApp f #[a, b]; - let t2 := mkApp f #[a, x0]; - let t3 := Expr.lam `x BinderInfo.default (Expr.sort Level.zero) (mkApp f #[a, x0]); - let t4 := Expr.lam `x BinderInfo.default (Expr.sort Level.zero) (mkApp f #[a, x1]); +do let f := mkConst `f []; + let a := mkConst `a []; + let b := mkConst `b []; + let x0 := mkBVar 0; + let x1 := mkBVar 1; + let t1 := mkAppN f #[a, b]; + let t2 := mkAppN f #[a, x0]; + let t3 := Expr.lam `x BinderInfo.default (Expr.sort Level.zero) (mkAppN f #[a, x0]); + let t4 := Expr.lam `x BinderInfo.default (Expr.sort Level.zero) (mkAppN f #[a, x1]); unless (!t1.hasLooseBVar 0) $ throw "failed-1"; unless (t2.hasLooseBVar 0) $ throw "failed-2"; unless (!t3.hasLooseBVar 0) $ throw "failed-3"; @@ -60,30 +60,30 @@ do let f := Expr.const `f []; #eval tst4 def tst5 : IO Unit := -do let f := Expr.const `f []; - let a := Expr.const `a []; - let nat := Expr.const `Nat []; - let x0 := Expr.bvar 0; - let x1 := Expr.bvar 1; - let x2 := Expr.bvar 2; +do let f := mkConst `f []; + let a := mkConst `a []; + let nat := mkConst `Nat []; + let x0 := mkBVar 0; + let x1 := mkBVar 1; + let x2 := mkBVar 2; let t := Expr.lam `x BinderInfo.default nat (Expr.app f x0); IO.println t.etaExpanded?; unless (t.etaExpanded? == some f) $ throw "failed-1"; let t := Expr.lam `x BinderInfo.default nat (Expr.app f x1); unless (t.etaExpanded? == none) $ throw "failed-2"; - let t := Expr.lam `x BinderInfo.default nat (mkApp f #[a, x0]); + let t := Expr.lam `x BinderInfo.default nat (mkAppN f #[a, x0]); unless (t.etaExpanded? == some (Expr.app f a)) $ throw "failed-3"; - let t := Expr.lam `x BinderInfo.default nat (mkApp f #[x0, x0]); + let t := Expr.lam `x BinderInfo.default nat (mkAppN f #[x0, x0]); unless (t.etaExpanded? == none) $ throw "failed-4"; let t := Expr.lam `x BinderInfo.default nat (Expr.lam `y BinderInfo.default nat (Expr.app f x0)); unless (t.etaExpanded? == none) $ throw "failed-5"; - let t := Expr.lam `x BinderInfo.default nat (Expr.lam `y BinderInfo.default nat (mkApp f #[x1, x0])); + let t := Expr.lam `x BinderInfo.default nat (Expr.lam `y BinderInfo.default nat (mkAppN f #[x1, x0])); IO.println t; unless (t.etaExpanded? == some f) $ throw "failed-6"; - let t := Expr.lam `x BinderInfo.default nat (Expr.lam `y BinderInfo.default nat (Expr.lam `z BinderInfo.default nat (mkApp f #[x2, x1, x0]))); + let t := Expr.lam `x BinderInfo.default nat (Expr.lam `y BinderInfo.default nat (Expr.lam `z BinderInfo.default nat (mkAppN f #[x2, x1, x0]))); IO.println t; unless (t.etaExpanded? == some f) $ throw "failed-7"; - let t := Expr.lam `x BinderInfo.default nat (Expr.lam `y BinderInfo.default nat (Expr.lam `z BinderInfo.default nat (mkApp f #[a, x2, x1, x0]))); + let t := Expr.lam `x BinderInfo.default nat (Expr.lam `y BinderInfo.default nat (Expr.lam `z BinderInfo.default nat (mkAppN f #[a, x2, x1, x0]))); IO.println t; unless (t.etaExpanded? == some (Expr.app f a)) $ throw "failed-8"; IO.println t.etaExpanded?; diff --git a/tests/lean/run/meta1.lean b/tests/lean/run/meta1.lean index 772593f633..2b7b896e8a 100644 --- a/tests/lean/run/meta1.lean +++ b/tests/lean/run/meta1.lean @@ -21,10 +21,10 @@ do env ← importModules mods; | EStateM.Result.error err _ => throw (IO.userError (toString err)) def t1 : Expr := -let map := Expr.const `List.map [Level.one, Level.one]; -let nat := Expr.const `Nat []; -let bool := Expr.const `Bool []; -mkApp map #[nat, bool] +let map := mkConst `List.map [Level.one, Level.one]; +let nat := mkConst `Nat []; +let bool := mkConst `Bool []; +mkAppN map #[nat, bool] #eval tstInferType [`Init.Data.List] t1 @@ -35,24 +35,24 @@ Expr.forallE `x BinderInfo.default prop prop #eval tstInferType [`Init.Core] t2 def t3 : Expr := -let nat := Expr.const `Nat []; -let natLe := Expr.const `Nat.le []; +let nat := mkConst `Nat []; +let natLe := mkConst `Nat.le []; let zero := Expr.lit (Literal.natVal 0); -let p := mkApp natLe #[Expr.bvar 0, zero]; +let p := mkAppN natLe #[Expr.bvar 0, zero]; Expr.forallE `x BinderInfo.default nat p #eval tstInferType [`Init.Data.Nat] t3 def t4 : Expr := -let nat := Expr.const `Nat []; -let p := mkApp (Expr.const `Nat.succ []) #[Expr.bvar 0]; +let nat := mkConst `Nat []; +let p := mkAppN (mkConst `Nat.succ []) #[Expr.bvar 0]; Expr.lam `x BinderInfo.default nat p #eval tstInferType [`Init.Core] t4 def t5 : Expr := -let add := Expr.const `Nat.add []; -mkApp add #[Expr.lit (Literal.natVal 3), Expr.lit (Literal.natVal 5)] +let add := mkConst `Nat.add []; +mkAppN add #[Expr.lit (Literal.natVal 3), Expr.lit (Literal.natVal 5)] #eval tstWHNF [`Init.Data.Nat] t5 #eval tstWHNF [`Init.Data.Nat] t5 TransparencyMode.reducible @@ -61,26 +61,26 @@ set_option pp.all true #check @List.cons Nat def t6 : Expr := -let map := Expr.const `List.map [Level.one, Level.one]; -let nat := Expr.const `Nat []; -let add := Expr.const `Nat.add []; -let f := Expr.lam `x BinderInfo.default nat (mkApp add #[Expr.bvar 0, Expr.lit (Literal.natVal 1)]); -let cons := Expr.app (Expr.const `List.cons [Level.zero]) nat; -let nil := Expr.app (Expr.const `List.nil [Level.zero]) nat; +let map := mkConst `List.map [Level.one, Level.one]; +let nat := mkConst `Nat []; +let add := mkConst `Nat.add []; +let f := Expr.lam `x BinderInfo.default nat (mkAppN add #[Expr.bvar 0, Expr.lit (Literal.natVal 1)]); +let cons := Expr.app (mkConst `List.cons [Level.zero]) nat; +let nil := Expr.app (mkConst `List.nil [Level.zero]) nat; let one := Expr.lit (Literal.natVal 1); let four := Expr.lit (Literal.natVal 4); let xs := Expr.app (Expr.app cons one) (Expr.app (Expr.app cons four) nil); -mkApp map #[nat, nat, f, xs] +mkAppN map #[nat, nat, f, xs] #eval tstInferType [`Init.Data.List] t6 #eval tstWHNF [`Init.Data.List] t6 #eval tstInferType [] $ Expr.sort Level.zero -#eval tstInferType [`Init.Data.List] $ Expr.lam `a BinderInfo.implicit (Expr.sort Level.one) (Expr.lam `x BinderInfo.default (Expr.bvar 0) (Expr.lam `xs BinderInfo.default (Expr.app (Expr.const `List [Level.zero]) (Expr.bvar 1)) (Expr.bvar 0))) +#eval tstInferType [`Init.Data.List] $ Expr.lam `a BinderInfo.implicit (Expr.sort Level.one) (Expr.lam `x BinderInfo.default (Expr.bvar 0) (Expr.lam `xs BinderInfo.default (Expr.app (mkConst `List [Level.zero]) (Expr.bvar 1)) (Expr.bvar 0))) def t7 : Expr := -let nat := Expr.const `Nat []; +let nat := mkConst `Nat []; let one := Expr.lit (Literal.natVal 1); Expr.letE `x nat one one @@ -88,16 +88,16 @@ Expr.letE `x nat one one #eval tstWHNF [`Init.Core] $ t7 def t8 : Expr := -let nat := Expr.const `Nat []; +let nat := mkConst `Nat []; let one := Expr.lit (Literal.natVal 1); -let add := Expr.const `Nat.add []; -Expr.letE `x nat one (mkApp add #[one, Expr.bvar 0]) +let add := mkConst `Nat.add []; +Expr.letE `x nat one (mkAppN add #[one, Expr.bvar 0]) #eval tstInferType [`Init.Core] $ t8 #eval tstWHNF [`Init.Core] $ t8 def t9 : Expr := -let nat := Expr.const `Nat []; +let nat := mkConst `Nat []; Expr.letE `a (Expr.sort Level.one) nat (Expr.forallE `x BinderInfo.default (Expr.bvar 0) (Expr.bvar 1)) #eval tstInferType [`Init.Core] $ t9 @@ -107,35 +107,35 @@ Expr.letE `a (Expr.sort Level.one) nat (Expr.forallE `x BinderInfo.default (Expr #eval tstInferType [`Init.Core] $ Expr.lit (Literal.strVal "hello") #eval tstInferType [`Init.Core] $ Expr.mdata {} $ Expr.lit (Literal.natVal 10) -#eval tstInferType [`Init.Lean.Trace] (Expr.proj `Inhabited 0 (Expr.const `Lean.TraceState.Inhabited [])) -#eval tstInferType [`Init.Lean.Trace] (Expr.proj `Lean.TraceState 0 (Expr.proj `Inhabited 0 (Expr.const `Lean.TraceState.Inhabited []))) -#eval tstWHNF [`Init.Lean.Trace] (Expr.proj `Inhabited 0 (Expr.const `Lean.TraceState.Inhabited [])) -#eval tstWHNF [`Init.Lean.Trace] (Expr.proj `Lean.TraceState 0 (Expr.proj `Inhabited 0 (Expr.const `Lean.TraceState.Inhabited []))) +#eval tstInferType [`Init.Lean.Trace] (Expr.proj `Inhabited 0 (mkConst `Lean.TraceState.Inhabited [])) +#eval tstInferType [`Init.Lean.Trace] (Expr.proj `Lean.TraceState 0 (Expr.proj `Inhabited 0 (mkConst `Lean.TraceState.Inhabited []))) +#eval tstWHNF [`Init.Lean.Trace] (Expr.proj `Inhabited 0 (mkConst `Lean.TraceState.Inhabited [])) +#eval tstWHNF [`Init.Lean.Trace] (Expr.proj `Lean.TraceState 0 (Expr.proj `Inhabited 0 (mkConst `Lean.TraceState.Inhabited []))) def t10 : Expr := -let nat := Expr.const `Nat []; -let refl := Expr.app (Expr.const `Eq.refl [Level.one]) nat; +let nat := mkConst `Nat []; +let refl := Expr.app (mkConst `Eq.refl [Level.one]) nat; Expr.lam `a BinderInfo.default nat (Expr.app refl (Expr.bvar 0)) #eval tstInferType [`Init.Core] t10 #eval tstIsProp [`Init.Core] t10 -#eval tstIsProp [`Init.Core] (mkApp (Expr.const `And []) #[Expr.const `True [], Expr.const `True []]) +#eval tstIsProp [`Init.Core] (mkAppN (mkConst `And []) #[mkConst `True [], mkConst `True []]) -#eval tstIsProp [`Init.Core] (Expr.const `And []) +#eval tstIsProp [`Init.Core] (mkConst `And []) -- Example where isPropQuick fails -#eval tstIsProp [`Init.Core] (mkApp (Expr.const `id [Level.zero]) #[Expr.sort Level.zero, mkApp (Expr.const `And []) #[Expr.const `True [], Expr.const +#eval tstIsProp [`Init.Core] (mkAppN (mkConst `id [Level.zero]) #[Expr.sort Level.zero, mkAppN (mkConst `And []) #[mkConst `True [], mkConst `True []]]) -#eval tstIsProp [`Init.Core] (mkApp (Expr.const `Eq [Level.one]) #[Expr.const `Nat [], Expr.lit (Literal.natVal 0), Expr.lit (Literal.natVal 1)]) +#eval tstIsProp [`Init.Core] (mkAppN (mkConst `Eq [Level.one]) #[mkConst `Nat [], Expr.lit (Literal.natVal 0), Expr.lit (Literal.natVal 1)]) #eval tstIsProp [`Init.Core] $ - Expr.forallE `x BinderInfo.default (Expr.const `Nat []) - (mkApp (Expr.const `Eq [Level.one]) #[Expr.const `Nat [], Expr.bvar 0, Expr.lit (Literal.natVal 1)]) + Expr.forallE `x BinderInfo.default (mkConst `Nat []) + (mkAppN (mkConst `Eq [Level.one]) #[mkConst `Nat [], Expr.bvar 0, Expr.lit (Literal.natVal 1)]) #eval tstIsProp [`Init.Core] $ Expr.app - (Expr.lam `x BinderInfo.default (Expr.const `Nat []) - (mkApp (Expr.const `Eq [Level.one]) #[Expr.const `Nat [], Expr.bvar 0, Expr.lit (Literal.natVal 1)])) + (Expr.lam `x BinderInfo.default (mkConst `Nat []) + (mkAppN (mkConst `Eq [Level.one]) #[mkConst `Nat [], Expr.bvar 0, Expr.lit (Literal.natVal 1)])) (Expr.lit (Literal.natVal 0)) diff --git a/tests/lean/typeclass_context.lean b/tests/lean/typeclass_context.lean index 6087f12f0d..788298bc69 100644 --- a/tests/lean/typeclass_context.lean +++ b/tests/lean/typeclass_context.lean @@ -15,12 +15,12 @@ open Lean.TypeClass.Context def testEUnify1 : EStateM String Context Expr := do t ← EStateM.fromStateM $ eNewMeta (mkConst "Term"); -eUnify (mkApp (mkConst "f") #[mkConst "a"]) t; +eUnify (mkAppN (mkConst "f") #[mkConst "a"]) t; get >>= λ (ctx : Context) => pure $ ctx.eInstantiate t def testEUnify2 : EStateM String Context Expr := do t ← EStateM.fromStateM $ eNewMeta (mkConst "Term"); -eUnify (mkApp (mkConst "f") #[mkConst "a"]) (mkApp (mkConst "f") #[t]); +eUnify (mkAppN (mkConst "f") #[mkConst "a"]) (mkAppN (mkConst "f") #[t]); get >>= λ (ctx : Context) => pure $ ctx.eInstantiate t def testEUnify3 : EStateM String Context Expr := do @@ -56,7 +56,7 @@ get >>= λ (ctx : Context) => pure $ ctx.eInstantiate t₂ def testEAssign1 : EStateM String Context Expr := do t ← EStateM.fromStateM $ eNewMeta (mkConst "Term"); -EStateM.fromStateM $ eAssign t $ mkApp (mkConst "f") #[mkConst "a"]; +EStateM.fromStateM $ eAssign t $ mkAppN (mkConst "f") #[mkConst "a"]; get >>= λ (ctx : Context) => pure $ ctx.eInstantiate t def testClash1 : EStateM String Context Expr := do @@ -64,15 +64,15 @@ eUnify (mkConst "f") (mkConst "g"); pure $ arbitrary _ def testClash2 : EStateM String Context Expr := do -eUnify (mkApp (mkConst "f") #[mkConst "a"]) (mkApp (mkConst "g") #[mkConst "a"]); +eUnify (mkAppN (mkConst "f") #[mkConst "a"]) (mkAppN (mkConst "g") #[mkConst "a"]); pure $ arbitrary _ def testClash3 : EStateM String Context Expr := do -eUnify (mkApp (mkConst "f") #[mkConst "a"]) (mkApp (mkConst "f") #[mkConst "b"]); +eUnify (mkAppN (mkConst "f") #[mkConst "a"]) (mkAppN (mkConst "f") #[mkConst "b"]); pure $ arbitrary _ def testClash4 : EStateM String Context Expr := do -eUnify (mkApp (mkConst "f") #[mkConst "a"]) (mkApp (mkConst "f") #[]); +eUnify (mkAppN (mkConst "f") #[mkConst "a"]) (mkAppN (mkConst "f") #[]); pure $ arbitrary _ def testChain1 : EStateM String Context Expr := do @@ -85,12 +85,12 @@ get >>= λ (ctx : Context) => pure $ ctx.eInstantiate t₁ def testAlphaNorm1 : EStateM String Context Expr := do t₁ ← EStateM.fromStateM $ eNewMeta (mkConst "Term"); t₂ ← EStateM.fromStateM $ eNewMeta (mkConst "Term"); -pure $ αNorm $ mkApp (mkConst "f") #[t₁, t₂] +pure $ αNorm $ mkAppN (mkConst "f") #[t₁, t₂] def testAlphaNorm2 : EStateM String Context Expr := do t₁ ← EStateM.fromStateM $ eNewMeta (mkConst "Term"); t₂ ← EStateM.fromStateM $ eNewMeta (mkConst "Term"); -pure $ αNorm $ mkApp (mkConst "f") #[t₂, t₁] +pure $ αNorm $ mkAppN (mkConst "f") #[t₂, t₁] def testAlphaNorm3 : EStateM String Context Expr := do pure $ αNorm (mkConst "f") @@ -98,7 +98,7 @@ pure $ αNorm (mkConst "f") def testAlphaNorm4 : EStateM String Context Expr := do t₁ ← EStateM.fromStateM $ eNewMeta (mkConst "Term"); t₂ ← EStateM.fromStateM $ eNewMeta (mkConst "Term"); -pure $ αNorm $ Expr.forallE "foo" BinderInfo.default (mkApp (mkConst "f") #[t₂]) (mkApp (mkConst "g") #[t₁]) +pure $ αNorm $ Expr.forallE "foo" BinderInfo.default (mkAppN (mkConst "f") #[t₂]) (mkAppN (mkConst "g") #[t₁]) #eval testEUnify1.run {} #eval testEUnify2.run {}