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

feat: add Repr instances for Level and Expr

Browse source 
closes #619

TODO: a better `Repr` instance for `Expr.Data`
This commit is contained in:
Leonardo de Moura 2022-01-20 09:26:06 -08:00
parent d190d6dda4
commit ff4be1e1db
9 changed files with 50 additions and 53 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/Lean/Data/KVMap.lean
View file

@ -14,7 +14,7 @@ inductive DataValue where
| ofNat (v : Nat)
| ofInt (v : Int)
| ofSyntax (v : Syntax)
deriving Inhabited, BEq
deriving Inhabited, BEq, Repr
@[export lean_data_value_beq]
def DataValue.beqExp (a b : DataValue) : Bool :=
@ -58,7 +58,7 @@ instance : Coe Syntax DataValue := ⟨DataValue.ofSyntax⟩
generate C++ code from Lean code. -/
structure KVMap where
entries : List (Name × DataValue) := []
deriving Inhabited
deriving Inhabited, Repr
namespace KVMap
instance : ToString KVMap := ⟨fun m => toString m.entries⟩

21
src/Lean/Expr.lean
View file

@ -79,7 +79,7 @@ abbrev MData.empty : MData := {}
binderInfo : 3-bits
approxDepth : 8-bits -- the approximate depth is used to minimize the number of hash collisions
looseBVarRange : 16-bits -/
def Expr.Data := UInt64
def Expr.Data := UInt64 deriving Repr
instance: Inhabited Expr.Data :=
inferInstanceAs (Inhabited UInt64)
@ -128,9 +128,9 @@ def BinderInfo.toUInt64 : BinderInfo → UInt64
| BinderInfo.instImplicit => 3
| BinderInfo.auxDecl => 4
@[inline] private def Expr.mkDataCore
(h : UInt64) (looseBVarRange : Nat) (approxDepth : UInt8)
(hasFVar hasExprMVar hasLevelMVar hasLevelParam nonDepLet : Bool) (bi : BinderInfo)
def Expr.mkData
(h : UInt64) (looseBVarRange : Nat := 0) (approxDepth : UInt8 := 0)
(hasFVar hasExprMVar hasLevelMVar hasLevelParam : Bool := false) (bi : BinderInfo := BinderInfo.default) (nonDepLet : Bool := false)
: Expr.Data :=
if looseBVarRange > Nat.pow 2 16 - 1 then panic! "bound variable index is too big"
else
@ -146,14 +146,11 @@ def BinderInfo.toUInt64 : BinderInfo → UInt64
looseBVarRange.toUInt64.shiftLeft 48
r
def Expr.mkData (h : UInt64) (looseBVarRange : Nat := 0) (approxDepth : UInt8 := 0) (hasFVar hasExprMVar hasLevelMVar hasLevelParam : Bool := false) : Expr.Data :=
Expr.mkDataCore h looseBVarRange approxDepth hasFVar hasExprMVar hasLevelMVar hasLevelParam false BinderInfo.default
@[inline] def Expr.mkDataForBinder (h : UInt64) (looseBVarRange : Nat) (approxDepth : UInt8) (hasFVar hasExprMVar hasLevelMVar hasLevelParam : Bool) (bi : BinderInfo) : Expr.Data :=
Expr.mkData h looseBVarRange approxDepth hasFVar hasExprMVar hasLevelMVar hasLevelParam bi false
def Expr.mkDataForBinder (h : UInt64) (looseBVarRange : Nat) (approxDepth : UInt8) (hasFVar hasExprMVar hasLevelMVar hasLevelParam : Bool) (bi : BinderInfo) : Expr.Data :=
Expr.mkDataCore h looseBVarRange approxDepth hasFVar hasExprMVar hasLevelMVar hasLevelParam false bi
def Expr.mkDataForLet (h : UInt64) (looseBVarRange : Nat) (approxDepth : UInt8) (hasFVar hasExprMVar hasLevelMVar hasLevelParam nonDepLet : Bool) : Expr.Data :=
Expr.mkDataCore h looseBVarRange approxDepth hasFVar hasExprMVar hasLevelMVar hasLevelParam nonDepLet BinderInfo.default
@[inline] def Expr.mkDataForLet (h : UInt64) (looseBVarRange : Nat) (approxDepth : UInt8) (hasFVar hasExprMVar hasLevelMVar hasLevelParam nonDepLet : Bool) : Expr.Data :=
Expr.mkData h looseBVarRange approxDepth hasFVar hasExprMVar hasLevelMVar hasLevelParam BinderInfo.default nonDepLet
open Expr
@ -194,7 +191,7 @@ inductive Expr where
| lit : Literal → Data → Expr -- literals
| mdata : MData → Expr → Data → Expr -- metadata
| proj : Name → Nat → Expr → Data → Expr -- projection
deriving Inhabited
deriving Inhabited, Repr
namespace Expr

6
src/Lean/Level.lean
View file

@ -22,7 +22,7 @@ namespace Lean
hasMVar : 1-bit
hasParam : 1-bit
depth : 24-bits -/
def Level.Data := UInt64
def Level.Data := UInt64 deriving Repr
instance : Inhabited Level.Data :=
inferInstanceAs (Inhabited UInt64)
@ -52,7 +52,7 @@ open Level
structure MVarId where
name : Name
deriving Inhabited, BEq, Hashable
deriving Inhabited, BEq, Hashable, Repr
instance : Repr MVarId where
reprPrec n p := reprPrec n.name p
@ -78,7 +78,7 @@ inductive Level where
| imax : Level → Level → Data → Level
| param : Name → Data → Level
| mvar : MVarId → Data → Level
deriving Inhabited
deriving Inhabited, Repr
namespace Level

24
tests/lean/mvar1.lean
View file

@ -52,7 +52,7 @@ def lctx6 := lctx5.mkLocalDecl `w `w (arrow natE (mkAppN m6 #[α, x, y]))
def t1 := lctx5.mkLambda #[α, x, y] $ mkAppN f #[α, mkAppN g #[x, y], lctx5.mkLambda #[z] (mkApp f z)]
#eval check (!t1.hasFVar)
#eval t1
#eval toString t1
def mctx1 : MetavarContext := {}
def mctx2 := mctx1.addExprMVarDecl `m1 `m1 lctx3 #[] natE
@ -68,34 +68,34 @@ def mctx10 := mctx9.assignExpr `m1 a
def t2 := lctx5.mkLambda #[α, x, y] $ mkAppN f #[mkAppN m4 #[α, x, y], x]
#eval check (!t2.hasFVar)
#eval t2
#eval (mctx6.instantiateMVars t2).1
#eval toString t2
#eval toString (mctx6.instantiateMVars t2).1
#eval check (!(mctx9.instantiateMVars t2).1.hasMVar)
#eval check (!(mctx9.instantiateMVars t2).1.hasFVar)
#eval (mctx9.instantiateMVars t2).1
#eval toString (mctx9.instantiateMVars t2).1
-- t3 is ill-formed since m3's localcontext contains ‵α`, `x` and `y`
def t3 := lctx5.mkLambda #[α, x, y] $ mkAppN f #[m3, x]
#eval check (mctx10.instantiateMVars t3).1.hasFVar
#eval (mctx7.instantiateMVars t3).1
#eval toString (mctx7.instantiateMVars t3).1
partial def mkDiamond : Nat → Expr
| 0 => m1
| (n+1) => mkAppN f #[mkDiamond n, mkDiamond n]
#eval (mctx7.instantiateMVars (mkDiamond 3)).1
#eval (mctx10.instantiateMVars (mkDiamond 3)).1
#eval (mctx7.instantiateMVars (mkDiamond 100)).1.getAppFn
#eval (mctx10.instantiateMVars (mkDiamond 100)).1.getAppFn
#eval toString (mctx7.instantiateMVars (mkDiamond 3)).1
#eval toString (mctx10.instantiateMVars (mkDiamond 3)).1
#eval toString (mctx7.instantiateMVars (mkDiamond 100)).1.getAppFn
#eval toString (mctx10.instantiateMVars (mkDiamond 100)).1.getAppFn
def mctx11 := mctx10.assignDelayed `m6 lctx5 #[α, x, y] m5
def mctx12 := mctx11.assignExpr `m5 (arrow α α)
def t4 := lctx6.mkLambda #[α, x, y, w] $ mkAppN f #[mkAppN m4 #[α, x, y], x]
#eval t4
#eval (mctx9.instantiateMVars t4).1
#eval (mctx12.instantiateMVars t4).1
#eval toString t4
#eval toString (mctx9.instantiateMVars t4).1
#eval toString (mctx12.instantiateMVars t4).1
#eval check (mctx9.instantiateMVars t4).1.hasMVar
#eval check (!((mctx9.instantiateMVars t4).1.hasFVar))
#eval check (!(mctx12.instantiateMVars t4).1.hasMVar)

24
tests/lean/mvar1.lean.expected.out
View file

@ -1,20 +1,20 @@
fun (α : Type) (x : Nat) (y : α) => f α (g x y) (fun (z : Vec.{0} x) => f z)
"fun (α : Type) (x : Nat) (y : α) => f α (g x y) (fun (z : Vec.{0} x) => f z)"
fun (α : Type) (x : Nat) (y : α) => f (?m4 α x y) x
fun (α : Type) (x : Nat) (y : α) => f (?m4 α x y) x
"fun (α : Type) (x : Nat) (y : α) => f (?m4 α x y) x"
"fun (α : Type) (x : Nat) (y : α) => f (?m4 α x y) x"
fun (α : Type) (x : Nat) (y : α) => f (g x y) x
"fun (α : Type) (x : Nat) (y : α) => f (g x y) x"
fun (α : Type) (x : Nat) (y : α) => f ?m3 x
f (f (f ?m1 ?m1) (f ?m1 ?m1)) (f (f ?m1 ?m1) (f ?m1 ?m1))
f (f (f a a) (f a a)) (f (f a a) (f a a))
f
f
fun (α : Type) (x : Nat) (y : α) (w : Nat -> (?m6 α x y)) => f (?m4 α x y) x
fun (α : Type) (x : Nat) (y : α) (w : Nat -> (?m6 α x y)) => f (g x y) x
fun (α : Type) (x : Nat) (y : α) (w : Nat -> α -> α) => f (g x y) x
"fun (α : Type) (x : Nat) (y : α) => f ?m3 x"
"f (f (f ?m1 ?m1) (f ?m1 ?m1)) (f (f ?m1 ?m1) (f ?m1 ?m1))"
"f (f (f a a) (f a a)) (f (f a a) (f a a))"
"f"
"f"
"fun (α : Type) (x : Nat) (y : α) (w : Nat -> (?m6 α x y)) => f (?m4 α x y) x"
"fun (α : Type) (x : Nat) (y : α) (w : Nat -> (?m6 α x y)) => f (g x y) x"
"fun (α : Type) (x : Nat) (y : α) (w : Nat -> α -> α) => f (g x y) x"

6
tests/lean/mvar2.lean
View file

@ -57,6 +57,6 @@ def mctx7 := mctx6.assignExpr `m1 natE
def t2 := lctx4.mkLambda #[α, x, y] $ mkAppN f #[mkAppN m3 #[α, x], x]
#eval check (!t2.hasFVar)
#eval t2
#eval (mctx6.instantiateMVars t2).1
#eval (mctx7.instantiateMVars t2).1
#eval toString t2
#eval toString (mctx6.instantiateMVars t2).1
#eval toString (mctx7.instantiateMVars t2).1

6
tests/lean/mvar2.lean.expected.out
View file

@ -1,4 +1,4 @@
fun (α : Type) (x : ?m1) (y : Nat -> (?m3 α x)) => f (?m3 α x) x
fun (α : Type) (x : ?m1) (y : Nat -> α -> α) => f (α -> α) x
fun (α : Type) (x : Nat) (y : Nat -> α -> α) => f (α -> α) x
"fun (α : Type) (x : ?m1) (y : Nat -> (?m3 α x)) => f (?m3 α x) x"
"fun (α : Type) (x : ?m1) (y : Nat -> α -> α) => f (α -> α) x"
"fun (α : Type) (x : Nat) (y : Nat -> α -> α) => f (α -> α) x"

6
tests/lean/mvar3.lean
View file

@ -76,7 +76,7 @@ def sortNamePairs {α} [Inhabited α] (xs : List (MVarId × α)) : List (MVarId
#eval toString $ sortNames $ mctx5.decls.toList.map (·.1.name)
#eval toString $ sortNamePairs $ mctx5.eAssignment.toList
#eval e1
#eval toString e1
#eval check (!e1.hasFVar)
def R2 :=
@ -90,7 +90,7 @@ def mctx6 := R2.1
#eval toString $ sortNamePairs $ mctx6.eAssignment.toList
-- ?n.2 was delayed assigned because ?m.3 is synthetic
#eval toString $ sortNames $ mctx6.dAssignment.toList.map (·.1.name)
#eval e2
#eval toString e2
#print "assigning ?m1 and ?n.1"
def R3 :=
@ -100,4 +100,4 @@ let mctx := mctx.assignExpr (Name.mkNum `n 1) (mkLambda `_ bi typeE natE);
(mctx.instantiateMVars e2)
def e3 := R3.1
def mctx7 := R3.2
#eval e3
#eval toString e3

6
tests/lean/mvar3.lean.expected.out
View file

@ -1,10 +1,10 @@
"[n.1, n.2, n.3, m1, m2, m3]"
"[(m1, ?n α), (m2, ?n α x), (m3, ?n α x)]"
fun (α : Type) (x : ?n α) (y : Nat -> (?n α x)) => f (?n α x) x
"fun (α : Type) (x : ?n α) (y : Nat -> (?n α x)) => f (?n α x) x"
"[n.1, n.2, n.3, m1, m2, m3]"
"[(m1, ?n α), (m2, ?n α x)]"
"[n.2]"
fun (α : Type) (x : ?n α) (y : Nat -> (?n α x)) => f (?n α x) y
"fun (α : Type) (x : ?n α) (y : Nat -> (?n α x)) => f (?n α x) y"
assigning ?m1 and ?n
fun (α : Type) (x : Nat) (y : Nat -> (?n α x)) => f x y
"fun (α : Type) (x : Nat) (y : Nat -> (?n α x)) => f x y"