From ccfa57d657d8ed391bbcfd9d301d21065b9b8d25 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 24 Oct 2019 13:53:33 -0700 Subject: [PATCH] chore: rename constructors MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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. --- library/Init/Lean/Class.lean | 8 ++--- library/Init/Lean/Compiler/Util.lean | 16 ++++----- library/Init/Lean/Expr.lean | 46 ++++++++++++------------ library/Init/Lean/LocalContext.lean | 4 +-- library/Init/Lean/TypeClass/Context.lean | 14 ++++---- library/Init/Lean/TypeClass/Synth.lean | 18 +++++----- tests/lean/run/expr_maps.lean | 4 +-- tests/lean/typeclass_context.lean | 6 ++-- 8 files changed, 59 insertions(+), 57 deletions(-) diff --git a/library/Init/Lean/Class.lean b/library/Init/Lean/Class.lean index 8841815e69..121f4ce62f 100644 --- a/library/Init/Lean/Class.lean +++ b/library/Init/Lean/Class.lean @@ -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 diff --git a/library/Init/Lean/Compiler/Util.lean b/library/Init/Lean/Compiler/Util.lean index 1765405c4f..cb94e6c4bd 100644 --- a/library/Init/Lean/Compiler/Util.lean +++ b/library/Init/Lean/Compiler/Util.lean @@ -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 diff --git a/library/Init/Lean/Expr.lean b/library/Init/Lean/Expr.lean index cc2a2a853e..f5fc726134 100644 --- a/library/Init/Lean/Expr.lean +++ b/library/Init/Lean/Expr.lean @@ -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]`. -/ diff --git a/library/Init/Lean/LocalContext.lean b/library/Init/Lean/LocalContext.lean index 8df403f0b1..59ec512166 100644 --- a/library/Init/Lean/LocalContext.lean +++ b/library/Init/Lean/LocalContext.lean @@ -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 := diff --git a/library/Init/Lean/TypeClass/Context.lean b/library/Init/Lean/TypeClass/Context.lean index a92306ae5e..87aa3d9783 100644 --- a/library/Init/Lean/TypeClass/Context.lean +++ b/library/Init/Lean/TypeClass/Context.lean @@ -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 diff --git a/library/Init/Lean/TypeClass/Synth.lean b/library/Init/Lean/TypeClass/Synth.lean index 30496f0e2a..3ec9ab84d1 100644 --- a/library/Init/Lean/TypeClass/Synth.lean +++ b/library/Init/Lean/TypeClass/Synth.lean @@ -78,12 +78,12 @@ abbrev TCMethod : Type → Type := EState String TCState -- See: [type_context.cpp] optional 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; diff --git a/tests/lean/run/expr_maps.lean b/tests/lean/run/expr_maps.lean index b13f093187..f17595382a 100644 --- a/tests/lean/run/expr_maps.lean +++ b/tests/lean/run/expr_maps.lean @@ -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 diff --git a/tests/lean/typeclass_context.lean b/tests/lean/typeclass_context.lean index a89b10f2ba..179d015ed5 100644 --- a/tests/lean/typeclass_context.lean +++ b/tests/lean/typeclass_context.lean @@ -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 {}