From 52f26022da43a652fd7887956d1f1a33bd2496d2 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 28 Oct 2019 11:10:25 -0700 Subject: [PATCH] chore: enforce naming convention --- library/Init/Lean/Expr.lean | 24 ++++++++++++------------ library/Init/Lean/TypeClass/Context.lean | 14 +++++++------- library/Init/Lean/TypeClass/Synth.lean | 12 ++++++------ 3 files changed, 25 insertions(+), 25 deletions(-) diff --git a/library/Init/Lean/Expr.lean b/library/Init/Lean/Expr.lean index c35c9d20c3..e528667f81 100644 --- a/library/Init/Lean/Expr.lean +++ b/library/Init/Lean/Expr.lean @@ -231,38 +231,38 @@ def isAppOfArity : Expr → Name → Nat → Bool | app f _, n, a+1 => isAppOfArity f n a | _, _, _ => false -def constName : Expr → Name +def constName! : Expr → Name | const n _ => n | _ => panic! "constant expected" -def constLevels : Expr → List Level +def constLevels! : Expr → List Level | const _ ls => ls | _ => panic! "constant expected" -def bvarIdx : Expr → Nat +def bvarIdx! : Expr → Nat | bvar idx => idx | _ => panic! "bvar expected" -def fvarName : Expr → Name +def fvarName! : Expr → Name | fvar n => n | _ => panic! "fvar expected" -def bindingName : Expr → Name +def bindingName! : Expr → Name | forallE n _ _ _ => n | lam n _ _ _ => n | _ => panic! "binding expected" -def bindingDomain : Expr → Expr +def bindingDomain! : Expr → Expr | forallE _ _ d _ => d | lam _ _ d _ => d | _ => panic! "binding expected" -def bindingBody : Expr → Expr +def bindingBody! : Expr → Expr | forallE _ _ _ b => b | lam _ _ _ b => b | _ => panic! "binding expected" -def letName : Expr → Name +def letName! : Expr → Name | letE n _ _ _ => n | _ => panic! "let expression expected" @@ -404,7 +404,7 @@ match e with @[extern "lean_expr_update_const"] def updateConst (e : Expr) (newLevels : List Level) (h : e.isConst = true) : Expr := -const e.constName newLevels +const e.constName! newLevels @[inline] def updateConst! (e : Expr) (newLevels : List Level) : Expr := match e with @@ -444,7 +444,7 @@ match e with @[extern "lean_expr_update_forall"] def updateForall (e : Expr) (newBinfo : BinderInfo) (newDomain : Expr) (newBody : Expr) (h : e.isForall = true) : Expr := -forallE e.bindingName newBinfo newDomain newBody +forallE e.bindingName! newBinfo newDomain newBody @[inline] def updateForall! (e : Expr) (newBinfo : BinderInfo) (newDomain : Expr) (newBody : Expr) : Expr := match e with @@ -458,7 +458,7 @@ match e with @[extern "lean_expr_update_lambda"] def updateLambda (e : Expr) (newBinfo : BinderInfo) (newDomain : Expr) (newBody : Expr) (h : e.isLambda = true) : Expr := -lam e.bindingName newBinfo newDomain newBody +lam e.bindingName! newBinfo newDomain newBody @[inline] def updateLambda! (e : Expr) (newBinfo : BinderInfo) (newDomain : Expr) (newBody : Expr) : Expr := match e with @@ -472,7 +472,7 @@ match e with @[extern "lean_expr_update_let"] def updateLet (e : Expr) (newType : Expr) (newVal : Expr) (newBody : Expr) (h : e.isLet = true) : Expr := -letE e.letName newType newVal newBody +letE e.letName! newType newVal newBody @[inline] def updateLet! (e : Expr) (newType : Expr) (newVal : Expr) (newBody : Expr) : Expr := match e with diff --git a/library/Init/Lean/TypeClass/Context.lean b/library/Init/Lean/TypeClass/Context.lean index 3660c2010c..8c6282428d 100644 --- a/library/Init/Lean/TypeClass/Context.lean +++ b/library/Init/Lean/TypeClass/Context.lean @@ -184,7 +184,7 @@ partial def uInstantiate (ctx : Context) : Level → Level def eHasTmpMVar (e : Expr) : Bool := if e.hasMVar -then eFind (λ t => eIsMeta t || (t.isConst && t.constLevels.any uHasTmpMVar)) e +then eFind (λ t => eIsMeta t || (t.isConst && t.constLevels!.any uHasTmpMVar)) e else false partial def slowWhnfApp (args : Array Expr) : Expr → Nat → Expr @@ -211,18 +211,18 @@ partial def eUnify : Expr → Expr → EState String Context Unit e₂ ← slowWhnf <$> (EState.fromState $ eShallowInstantiate e₂); if e₁.isMVar && e₂.isMVar && e₁ == e₂ then pure () else if eIsMeta e₂ && !(eIsMeta e₁) then eUnify e₂ e₁ - else if e₁.isBVar && e₂.isBVar && e₁.bvarIdx == e₂.bvarIdx then pure () - else if e₁.isFVar && e₂.isFVar && e₁.fvarName == e₂.fvarName then pure () - else if e₁.isConst && e₂.isConst && e₁.constName == e₂.constName then - List.forM₂ uUnify e₁.constLevels e₂.constLevels + else if e₁.isBVar && e₂.isBVar && e₁.bvarIdx! == e₂.bvarIdx! then pure () + else if e₁.isFVar && e₂.isFVar && e₁.fvarName! == e₂.fvarName! then pure () + else if e₁.isConst && e₂.isConst && e₁.constName! == e₂.constName! then + List.forM₂ uUnify e₁.constLevels! e₂.constLevels! else if e₁.isApp && e₂.isApp && e₁.getAppNumArgs == e₂.getAppNumArgs then do let args₁ := e₁.getAppArgs; let args₂ := e₂.getAppArgs; eUnify e₁.getAppFn e₂.getAppFn; args₁.size.forM $ fun i => eUnify (args₁.get! i) (args₂.get! i) else if e₁.isForall && e₂.isForall then do - eUnify e₁.bindingDomain e₂.bindingDomain; - eUnify e₁.bindingBody e₂.bindingBody + eUnify e₁.bindingDomain! e₂.bindingDomain!; + eUnify e₁.bindingBody! e₂.bindingBody! else if eIsMeta e₁ && !(eOccursIn e₂ e₁) then match eMetaIdx e₁ with | some idx => EState.fromState $ eAssignIdx idx e₂ diff --git a/library/Init/Lean/TypeClass/Synth.lean b/library/Init/Lean/TypeClass/Synth.lean index 4ef2753712..86d2d43d3d 100644 --- a/library/Init/Lean/TypeClass/Synth.lean +++ b/library/Init/Lean/TypeClass/Synth.lean @@ -85,7 +85,7 @@ def quickIsClass (env : Environment) : Expr → Option (Option Name) | Expr.forallE _ _ _ b => quickIsClass b | Expr.app e _ => let f := e.getAppFn; - if f.isConst && isClass env f.constName then some (some f.constName) + if f.isConst && isClass env f.constName! then some (some f.constName!) else if f.isLambda then none else some none | _ => some none @@ -268,19 +268,19 @@ def collectEReplacements (env : Environment) (lctx : LocalContext) (locals : Arr | _, arg::args, _, _, _ => panic! "TODO(dselsam): this case not yet handled" def preprocessForOutParams (env : Environment) (goalType : Expr) : Context × Expr × Array (Level × Level) × Array (Expr × Expr) := -if !goalType.hasMVar && goalType.getAppFn.isConst && !hasOutParams env goalType.getAppFn.constName +if !goalType.hasMVar && goalType.getAppFn.isConst && !hasOutParams env goalType.getAppFn.constName! then ({}, goalType, #[], #[]) else let ⟨lctx, bodyGoalType, locals⟩ := introduceLocals 0 {} #[] goalType; let f := goalType.getAppFn; let fArgs := goalType.getAppArgs; - if !(f.isConst && isClass env f.constName) + if !(f.isConst && isClass env f.constName!) then ({}, goalType, #[], #[]) else - let ⟨ctx, uReplacements, CLevels⟩ := collectUReplacements f.constLevels {} #[] #[]; - let f := if uReplacements.isEmpty then f else Expr.const f.constName CLevels.toList; + let ⟨ctx, uReplacements, CLevels⟩ := collectUReplacements f.constLevels! {} #[] #[]; + let f := if uReplacements.isEmpty then f else Expr.const f.constName! CLevels.toList; let fType := - match env.find f.constName with + match env.find f.constName! with | none => panic! "found constant not in the environment" | some cInfo => cInfo.instantiateTypeUnivParams CLevels.toList; let (ctx, eReplacements, fArgs) := collectEReplacements env lctx locals fType fArgs.toList ctx #[] #[]; -- TODO: avoid fArgs.toList