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

chore: rename constructors

Browse source 
Before we start writing a lot of Expr code.

- `Expr.pi` does not make sense anymore.
- `Expr.elet` is weird. `«let»` is too inconvenient to write. So, I
   used `letE` short for `letExpr`. GHC avoids this issue because
   keywords are lowercase and constructors are capitalized.
This commit is contained in:
Leonardo de Moura 2019-10-24 13:53:33 -07:00
parent faf7d7daf6
commit ccfa57d657
8 changed files with 59 additions and 57 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
library/Init/Lean/Class.lean
View file

@ -84,8 +84,8 @@ def isOutParam (e : Expr) : Bool :=
e.isAppOfArity `outParam 1
def Expr.hasOutParam : Expr → Bool
| Expr.pi _ _ d b => isOutParam d || Expr.hasOutParam b
| _ => false
| Expr.forallE _ _ d b => isOutParam d || Expr.hasOutParam b
| _ => false
def addClass (env : Environment) (clsName : Name) : Except String Environment :=
if isClass env clsName then Except.error ("class has already been declared '" ++ toString clsName ++ "'")
@ -100,8 +100,8 @@ private def consumeNLambdas : Nat → Expr → Option Expr
| _, _ => none
partial def getClassName (env : Environment) : Expr → Option Name
| Expr.pi _ _ _ d => getClassName d
| e => do
| Expr.forallE _ _ _ d => getClassName d
| e => do
Expr.const c _ ← pure e.getAppFn | none;
info ← env.find c;
match info.value with

16
library/Init/Lean/Compiler/Util.lean
View file

@ -38,14 +38,14 @@ instance : HasAndthen Visitor :=
| {found := true, result := true} => {found := true, result := x != y}
def visit (x : Name) : Expr → Visitor
| Expr.fvar y => visitFVar y x
| Expr.app f a => visit a >> visit f
| Expr.lam _ _ d b => visit d >> visit b
| Expr.pi _ _ d b => visit d >> visit b
| Expr.elet _ t v b => visit t >> visit v >> visit b
| Expr.mdata _ e => visit e
| Expr.proj _ _ e => visit e
| _ => skip
| Expr.fvar y => visitFVar y x
| Expr.app f a => visit a >> visit f
| Expr.lam _ _ d b => visit d >> visit b
| Expr.forallE _ _ d b => visit d >> visit b
| Expr.letE _ t v b => visit t >> visit v >> visit b
| Expr.mdata _ e => visit e
| Expr.proj _ _ e => visit e
| _ => skip
end atMostOnce

46
library/Init/Lean/Expr.lean
View file

@ -42,19 +42,21 @@ abbrev empty : MData := {KVMap .}
instance : HasEmptyc MData := ⟨empty⟩
end MData
/- 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 → Expr -- bound variables
| fvar : Name → Expr -- free variables
| mvar : Name → Expr -- meta variables
| sort : Level → Expr -- Sort
| const : Name → List Level → Expr -- constants
| app : Expr → Expr → Expr -- application
| lam : Name → BinderInfo → Expr → Expr → Expr -- lambda abstraction
| pi : Name → BinderInfo → Expr → Expr → Expr -- Pi
| elet : Name → Expr → Expr → Expr → Expr -- let expressions
| lit : Literal → Expr -- literals
| mdata : MData → Expr → Expr -- metadata
| proj : Name → Nat → Expr → Expr -- projection
| bvar : Nat → Expr -- bound variables
| fvar : Name → Expr -- free variables
| mvar : Name → Expr -- meta variables
| sort : Level → Expr -- Sort
| const : Name → List Level → Expr -- constants
| app : Expr → Expr → Expr -- application
| lam : Name → BinderInfo → Expr → Expr → Expr -- lambda abstraction
| forallE : Name → BinderInfo → Expr → Expr → Expr -- (dependent) arrow
| letE : Name → Expr → Expr → Expr → Expr -- let expressions
| lit : Literal → Expr -- literals
| mdata : MData → Expr → Expr -- metadata
| proj : Name → Nat → Expr → Expr -- projection
instance exprIsInhabited : Inhabited Expr :=
⟨Expr.sort Level.zero⟩
@ -66,8 +68,8 @@ attribute [extern "lean_expr_mk_sort"] Expr.sort
attribute [extern "lean_expr_mk_const"] Expr.const
attribute [extern "lean_expr_mk_app"] Expr.app
attribute [extern "lean_expr_mk_lambda"] Expr.lam
attribute [extern "lean_expr_mk_pi"] Expr.pi
attribute [extern "lean_expr_mk_let"] Expr.elet
attribute [extern "lean_expr_mk_pi"] Expr.forallE
attribute [extern "lean_expr_mk_let"] Expr.letE
attribute [extern "lean_expr_mk_lit"] Expr.lit
attribute [extern "lean_expr_mk_mdata"] Expr.mdata
attribute [extern "lean_expr_mk_proj"] Expr.proj
@ -141,20 +143,20 @@ def isConst : Expr → Bool
| _ => false
def isForall : Expr → Bool
| Expr.pi _ _ _ _ => true
| forallE _ _ _ _ => true
| _ => false
def isLambda : Expr → Bool
| Expr.lam _ _ _ _ => true
| lam _ _ _ _ => true
| _ => false
def isBinding : Expr → Bool
| Expr.lam _ _ _ _ => true
| Expr.pi _ _ _ _ => true
| Expr.forallE _ _ _ _ => true
| _ => false
def isLet : Expr → Bool
| Expr.elet _ _ _ _ => true
| Expr.letE _ _ _ _ => true
| _ => false
def getAppFn : Expr → Expr
@ -211,14 +213,14 @@ def fvarName : Expr → Name
| _ => panic! "fvarName called on non-fvar"
def bindingDomain : Expr → Expr
| Expr.pi _ _ d _ => d
| Expr.forallE _ _ d _ => d
| Expr.lam _ _ d _ => d
| _ => default _
| _ => panic! "binding expected"
def bindingBody : Expr → Expr
| Expr.pi _ _ _ b => b
| Expr.forallE _ _ _ b => b
| Expr.lam _ _ _ b => b
| _ => default _
| _ => panic! "binding expected"
/-- Instantiate the loose bound variables in `e` using `subst`.
That is, a loose `Expr.bvar i` is replaced with `subst[i]`. -/

4
library/Init/Lean/LocalContext.lean
View file

@ -244,11 +244,11 @@ xs.size.foldRev (fun i b =>
if isLambda then
Expr.lam n bi ty b
else
Expr.pi n bi ty b
Expr.forallE n bi ty b
| some (LocalDecl.ldecl _ _ n ty val) =>
let ty := ty.abstractRange i xs;
let val := val.abstractRange i xs;
Expr.elet n ty val b
Expr.letE n ty val b
| none => b) b
def mkLambda (lctx : LocalContext) (xs : Array Expr) (b : Expr) : Expr :=

14
library/Init/Lean/TypeClass/Context.lean
View file

@ -84,7 +84,7 @@ partial def eFind (f : Expr → Bool) : Expr → Bool
else
match e with
| Expr.app f a => eFind f || eFind a
| Expr.pi _ _ d b => eFind d || eFind b
| Expr.forallE _ _ d b => eFind d || eFind b
| _ => false
def eOccursIn (t₀ : Expr) (e : Expr) : Bool :=
@ -235,10 +235,10 @@ partial def eInstantiate (ctx : Context) : Expr → Expr
then e
else
match e with
| Expr.pi n i d b => Expr.pi n i (eInstantiate d) (eInstantiate b)
| Expr.lam n i d b => Expr.lam n i (eInstantiate d) (eInstantiate b)
| Expr.const n ls => Expr.const n (ls.map $ uInstantiate ctx)
| Expr.app e₁ e₂ => Expr.app (eInstantiate e₁) (eInstantiate e₂)
| Expr.forallE n i d b => Expr.forallE n i (eInstantiate d) (eInstantiate b)
| Expr.lam n i d b => Expr.lam n i (eInstantiate d) (eInstantiate b)
| Expr.const n ls => Expr.const n (ls.map $ uInstantiate ctx)
| Expr.app e₁ e₂ => Expr.app (eInstantiate e₁) (eInstantiate e₂)
| _ =>
match eMetaIdx e with
| none => e
@ -289,10 +289,10 @@ partial def eAlphaNormalizeCore : Expr → State AlphaNormData Expr
f ← eAlphaNormalizeCore f;
a ← eAlphaNormalizeCore a;
pure $ Expr.app f a
| Expr.pi n i d b => do
| Expr.forallE n i d b => do
d ← eAlphaNormalizeCore d;
b ← eAlphaNormalizeCore b;
pure $ Expr.pi n i d b
pure $ Expr.forallE n i d b
| _ =>
match eMetaIdx e with
| none => pure e

18
library/Init/Lean/TypeClass/Synth.lean
View file

@ -78,12 +78,12 @@ abbrev TCMethod : Type → Type := EState String TCState
-- See: [type_context.cpp] optional<name> type_context_old::is_full_class(expr type)
-- TODO(dselsam): check if we need to call `get_decl()` as well in the `const` case.
def quickIsClass (env : Environment) : Expr → Option (Option Name)
| Expr.elet _ _ _ _ => none
| Expr.proj _ _ _ => none
| Expr.mdata _ e => quickIsClass e
| Expr.const n _ => if isClass env n then some (some n) else none
| Expr.pi _ _ _ b => quickIsClass b
| Expr.app e _ =>
| Expr.letE _ _ _ _ => none
| Expr.proj _ _ _ => none
| Expr.mdata _ e => quickIsClass e
| Expr.const n _ => if isClass env n then some (some n) else none
| Expr.forallE _ _ _ b => quickIsClass b
| Expr.app e _ =>
let f := e.getAppFn;
if f.isConst && isClass env f.constName then some (some f.constName)
else if f.isLambda then none
@ -112,7 +112,7 @@ do let mvarType := ctx.eInfer mvar;
}
partial def introduceMVars (lctx : LocalContext) (locals : Array Expr) : Context → Expr → Expr → Array Expr → Context × Expr × Expr × Array Expr
| ctx, instVal, Expr.pi _ info domain body, mvars => do
| 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 instVal := Expr.app instVal arg;
@ -123,7 +123,7 @@ partial def introduceMVars (lctx : LocalContext) (locals : Array Expr) : Context
| ctx, instVal, instType, mvars => (ctx, instVal, instType, mvars)
partial def introduceLocals : Nat → LocalContext → Array Expr → Expr → LocalContext × Expr × Array Expr
| nextIdx, lctx, ls, Expr.pi name info domain body =>
| nextIdx, lctx, ls, Expr.forallE name info domain body =>
let idxName : Name := mkNumName (mkSimpleName "_tmp") nextIdx;
let ⟨lDecl, lctx⟩ := lctx.mkLocalDecl idxName name domain info;
let l : Expr := Expr.fvar idxName;
@ -257,7 +257,7 @@ def collectEReplacements (env : Environment) (lctx : LocalContext) (locals : Arr
→ Context × Array (Expr × Expr) × Array Expr
| _, [], ctx, eReplacements, fArgs => (ctx, eReplacements, fArgs)
| Expr.pi _ _ d b, arg::args, ctx, eReplacements, fArgs =>
| 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;

4
tests/lean/run/expr_maps.lean
View file

@ -5,9 +5,9 @@ def exprType : Expr := Expr.sort Level.one
def biDef := BinderInfo.default
def exprNat := Expr.const `Nat []
-- Type -> Type
def TypeArrowType := Expr.pi `α biDef exprType exprType
def TypeArrowType := Expr.forallE `α biDef exprType exprType
-- Type -> Type
def TypeArrowType2 := Expr.pi `β biDef exprType exprType
def TypeArrowType2 := Expr.forallE `β biDef exprType exprType
-- fun (x : Nat), x
def exprT1 := Expr.lam `x biDef exprNat (Expr.bvar 0)
-- fun (y : Nat), x

6
tests/lean/typeclass_context.lean
View file

@ -31,13 +31,13 @@ get >>= λ (ctx : Context) => pure $ ctx.eInstantiate t
def testEUnify4 : EState String Context Expr := do
t₁ ← EState.fromState $ eNewMeta (mkConst "Term");
t₂ ← EState.fromState $ eNewMeta (mkConst "Term");
eUnify (Expr.pi "foo" BinderInfo.default t₂ t₁) (Expr.pi "foo" BinderInfo.default t₁ t₂);
eUnify (Expr.forallE "foo" BinderInfo.default t₂ t₁) (Expr.forallE "foo" BinderInfo.default t₁ t₂);
get >>= λ (ctx : Context) => pure $ ctx.eInstantiate t₂
def testEUnify5 : EState String Context Expr := do
t₁ ← EState.fromState $ eNewMeta (mkConst "Term");
t₂ ← EState.fromState $ eNewMeta (mkConst "Term");
eUnify (Expr.pi "foo" BinderInfo.default t₁ t₂) (Expr.pi "foo" BinderInfo.default t₂ t₁);
eUnify (Expr.forallE "foo" BinderInfo.default t₁ t₂) (Expr.forallE "foo" BinderInfo.default t₂ t₁);
get >>= λ (ctx : Context) => pure $ ctx.eInstantiate t₂
def testEUnify6 : EState String Context Expr := do
@ -98,7 +98,7 @@ pure $ αNorm (mkConst "f")
def testAlphaNorm4 : EState String Context Expr := do
t₁ ← EState.fromState $ eNewMeta (mkConst "Term");
t₂ ← EState.fromState $ eNewMeta (mkConst "Term");
pure $ αNorm $ Expr.pi "foo" BinderInfo.default (mkApp (mkConst "f") #[t₂]) (mkApp (mkConst "g") #[t₁])
pure $ αNorm $ Expr.forallE "foo" BinderInfo.default (mkApp (mkConst "f") #[t₂]) (mkApp (mkConst "g") #[t₁])
#eval testEUnify1.run {}
#eval testEUnify2.run {}