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

feat: avoid unnecessary metavars

Browse source
This commit is contained in:
Leonardo de Moura 2019-12-19 11:26:47 -08:00
parent fc5fb07fc3
commit 76e75a1b53
1 changed files with 4 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/Init/Lean/Elab/Term.lean
View file

@ -241,6 +241,8 @@ def mkFreshExprMVar (ref : Syntax) (type? : Option Expr := none) (kind : Metavar
match type? with
| some type => liftMetaM ref $ Meta.mkFreshExprMVar type userName? kind
| none => liftMetaM ref $ do u ← Meta.mkFreshLevelMVar; type ← Meta.mkFreshExprMVar (mkSort u); Meta.mkFreshExprMVar type userName? kind
def mkFreshTypeMVar (ref : Syntax) (kind : MetavarKind := MetavarKind.natural) (userName? : Name := Name.anonymous) : TermElabM Expr :=
liftMetaM ref $ do u ← Meta.mkFreshLevelMVar; Meta.mkFreshExprMVar (mkSort u) userName? kind
def getLevel (ref : Syntax) (type : Expr) : TermElabM Level := liftMetaM ref $ Meta.getLevel type
def mkForall (ref : Syntax) (xs : Array Expr) (e : Expr) : TermElabM Expr := liftMetaM ref $ Meta.mkForall xs e
def mkLambda (ref : Syntax) (xs : Array Expr) (e : Expr) : TermElabM Expr := liftMetaM ref $ Meta.mkLambda xs e
@ -392,7 +394,7 @@ def expandCDot? : Syntax → TermElabM (Option Syntax)
private def exceptionToSorry (ref : Syntax) (ex : Elab.Exception) (expectedType? : Option Expr) : TermElabM Expr := do
expectedType : Expr ← match expectedType? with
| none => mkFreshExprMVar ref
| none => mkFreshTypeMVar ref
| some expectedType => pure expectedType;
u ← getLevel ref expectedType;
let syntheticSorry := mkApp2 (mkConst `sorryAx [u]) expectedType (mkConst `Bool.true);
@ -814,7 +816,7 @@ fun stx expectedType? => do
val ← match (stx.getArg 0).isNatLit? with
| some val => pure (mkNatLit val)
| none => throwError stx.val "ill-formed syntax";
typeMVar ← mkFreshExprMVar ref none MetavarKind.synthetic;
typeMVar ← mkFreshTypeMVar ref MetavarKind.synthetic;
registerSyntheticMVar ref typeMVar.mvarId! (SyntheticMVarKind.withDefault (Lean.mkConst `Nat));
match expectedType? with
| some expectedType => do isDefEq ref expectedType typeMVar; pure ()