chore: mkApp => mkAppN
We are goint to use `mkApp` for creating unary applications
This commit is contained in:
Leonardo de Moura
parent
fd66963e85
commit
c768a24735
13 changed files with 180 additions and 168 deletions
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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 α
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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⟩
|
||||
|
||||
|
|
|
|||
|
|
@ -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;
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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?;
|
||||
|
|
|
|||
|
|
@ -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))
|
||||
|
|
|
|||
|
|
@ -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 {}
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue