From 2a89bcd9318f21df68405f2296a4e874052c1265 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 28 Jan 2020 15:51:36 -0800 Subject: [PATCH] feat: use `Coe` in the new frontend --- .../Lean/Elab/SynthesizeSyntheticMVars.lean | 22 +++- src/Init/Lean/Elab/Term.lean | 102 +++++++++++------- src/Init/Lean/Elab/TermApp.lean | 7 +- 3 files changed, 84 insertions(+), 47 deletions(-) diff --git a/src/Init/Lean/Elab/SynthesizeSyntheticMVars.lean b/src/Init/Lean/Elab/SynthesizeSyntheticMVars.lean index beb973b854..3c7b22af2d 100644 --- a/src/Init/Lean/Elab/SynthesizeSyntheticMVars.lean +++ b/src/Init/Lean/Elab/SynthesizeSyntheticMVars.lean @@ -70,6 +70,15 @@ withMVarContext instMVar $ catch | Exception.ex (Elab.Exception.error errMsg) => do logMessage errMsg; pure true | _ => unreachable!) +/-- + Similar to `synthesizePendingInstMVar`, but generates type mismatch error message. -/ +private def synthesizePendingCoeInstMVar (ref : Syntax) (instMVar : MVarId) (expectedType : Expr) (eType : Expr) (e : Expr) (f? : Option Expr) : TermElabM Bool := do +withMVarContext instMVar $ catch + (synthesizeInstMVarCore ref instMVar) + (fun ex => match ex with + | Exception.ex (Elab.Exception.error errMsg) => throwTypeMismatchError ref expectedType eType e f? errMsg.data + | _ => unreachable!) + /-- Return `true` iff `mvarId` is assigned to a term whose the head is not a metavariable. We use this method to process `SyntheticMVarKind.withDefault`. -/ @@ -80,11 +89,12 @@ pure $ !val.getAppFn.isMVar /-- Try to synthesize the given pending synthetic metavariable. -/ private def synthesizeSyntheticMVar (mvarSyntheticDecl : SyntheticMVarDecl) (postponeOnError : Bool) (runTactics : Bool) : TermElabM Bool := match mvarSyntheticDecl.kind with -| SyntheticMVarKind.typeClass => synthesizePendingInstMVar mvarSyntheticDecl.ref mvarSyntheticDecl.mvarId +| SyntheticMVarKind.typeClass => synthesizePendingInstMVar mvarSyntheticDecl.ref mvarSyntheticDecl.mvarId +| SyntheticMVarKind.coe expectedType eType e f? => synthesizePendingCoeInstMVar mvarSyntheticDecl.ref mvarSyntheticDecl.mvarId expectedType eType e f? -- NOTE: actual processing at `synthesizeSyntheticMVarsAux` -| SyntheticMVarKind.withDefault _ => checkWithDefault mvarSyntheticDecl.ref mvarSyntheticDecl.mvarId -| SyntheticMVarKind.postponed macroStack => resumePostponed macroStack mvarSyntheticDecl.ref mvarSyntheticDecl.mvarId postponeOnError -| SyntheticMVarKind.tactic tacticCode => do runTactic mvarSyntheticDecl.ref mvarSyntheticDecl.mvarId tacticCode; pure true +| SyntheticMVarKind.withDefault _ => checkWithDefault mvarSyntheticDecl.ref mvarSyntheticDecl.mvarId +| SyntheticMVarKind.postponed macroStack => resumePostponed macroStack mvarSyntheticDecl.ref mvarSyntheticDecl.mvarId postponeOnError +| SyntheticMVarKind.tactic tacticCode => do runTactic mvarSyntheticDecl.ref mvarSyntheticDecl.mvarId tacticCode; pure true /-- Try to synthesize the current list of pending synthetic metavariables. @@ -137,6 +147,10 @@ s.syntheticMVars.forM $ fun mvarSyntheticDecl => mvarDecl ← getMVarDecl mvarSyntheticDecl.mvarId; logError mvarSyntheticDecl.ref $ "failed to create type class instance for " ++ indentExpr mvarDecl.type + | SyntheticMVarKind.coe expectedType eType e f? => + withMVarContext mvarSyntheticDecl.mvarId $ do + mvarDecl ← getMVarDecl mvarSyntheticDecl.mvarId; + throwTypeMismatchError mvarSyntheticDecl.ref expectedType eType e f? (some ("failed to create type class instance for " ++ indentExpr mvarDecl.type)) | _ => unreachable! -- TODO handle other cases. private def getSomeSynthethicMVarsRef : TermElabM Syntax := do diff --git a/src/Init/Lean/Elab/Term.lean b/src/Init/Lean/Elab/Term.lean index a0d83b204e..194fde9fe4 100644 --- a/src/Init/Lean/Elab/Term.lean +++ b/src/Init/Lean/Elab/Term.lean @@ -38,6 +38,9 @@ structure Context extends Meta.Context := inductive SyntheticMVarKind -- typeclass instance search | typeClass +-- Similar to typeClass, but error messages are different, +-- we use "type mismatch" or "application type mismatch" (when `f?` is some) instead of "failed to synthesize" +| coe (expectedType : Expr) (eType : Expr) (e : Expr) (f? : Option Expr) -- tactic block execution | tactic (tacticCode : Syntax) -- `elabTerm` call that threw `Exception.postpone` (input is stored at `SyntheticMVarDecl.ref`) @@ -550,43 +553,6 @@ ctx ← read; let needReset := ctx.localInstances == mvarDecl.localInstances; withLCtx mvarDecl.lctx mvarDecl.localInstances $ resettingSynthInstanceCacheWhen needReset x -/-- - If `expectedType?` is `some t`, then ensure `t` and `eType` are definitionally equal. - If they are not, then try coercions. - Return `some e'` if successful, where `e'` may be different from `e` if coercions have been applied, - and `none` otherwise - -/ -def tryEnsureHasType? (ref : Syntax) (expectedType? : Option Expr) (eType : Expr) (e : Expr) : TermElabM (Option Expr) := -match expectedType? with -| none => pure (some e) -| some expectedType => - condM (isDefEq ref eType expectedType) - (pure (some e)) - -- TODO try `HasCoe` - (pure none) - -/-- - If `expectedType?` is `some t`, then ensure `t` and `eType` are definitionally equal. - If they are not, then try coercions. -/ -def ensureHasTypeAux (ref : Syntax) (expectedType? : Option Expr) (eType : Expr) (e : Expr) : TermElabM Expr := do -e? ← tryEnsureHasType? ref expectedType? eType e; -match e? with -| some e => pure e -| none => - let msg : MessageData := - "type mismatch" ++ indentExpr e - ++ Format.line ++ "has type" ++ indentExpr eType - ++ Format.line ++ "but it is expected to have type" ++ indentExpr expectedType?.get!; - throwError ref msg - -/-- - If `expectedType?` is `some t`, then ensure `t` and type of `e` are definitionally equal. - If they are not, then try coercions. -/ -def ensureHasType (ref : Syntax) (expectedType? : Option Expr) (e : Expr) : TermElabM Expr := -match expectedType? with -| none => pure e -| _ => do eType ← inferType ref e; ensureHasTypeAux ref expectedType? eType e - /- Try to synthesize metavariable using type class resolution. This method assumes the local context and local instances of `instMVar` coincide with the current local context and local instances. @@ -619,6 +585,68 @@ unlessM (synthesizeInstMVarCore ref mvarId) $ registerSyntheticMVar ref mvarId SyntheticMVarKind.typeClass; pure mvar +def throwTypeMismatchError {α} (ref : Syntax) (expectedType : Expr) (eType : Expr) (e : Expr) + (f? : Option Expr := none) (extraMsg? : Option MessageData := none) : TermElabM α := +let extraMsg : MessageData := match extraMsg? with + | none => Format.nil + | some extraMsg => Format.line ++ extraMsg; +match f? with +| none => + let msg : MessageData := + "type mismatch" ++ indentExpr e + ++ Format.line ++ "has type" ++ indentExpr eType + ++ Format.line ++ "but it is expected to have type" ++ indentExpr expectedType + ++ extraMsg; + throwError ref msg +| some f => do + env ← getEnv; mctx ← getMCtx; lctx ← getLCtx; opts ← getOptions; + throwError ref $ Meta.Exception.mkAppTypeMismatchMessage f e { env := env, mctx := mctx, lctx := lctx, opts := opts } ++ extraMsg + +/-- + Try to apply coercion to make sure `e` has type `expectedType`. + Relevant definitions: + ``` + class CoeT (α : Sort u) (a : α) (β : Sort v) + abbrev coe {α : Sort u} {β : Sort v} (a : α) [CoeT α a β] : β + ``` -/ +def tryCoe (ref : Syntax) (expectedType : Expr) (eType : Expr) (e : Expr) (f? : Option Expr) : TermElabM Expr := do +u ← getLevel ref eType; +v ← getLevel ref expectedType; +let coeTInstType := mkAppN (mkConst `CoeT [u, v]) #[eType, e, expectedType]; +mvar ← mkFreshExprMVar ref coeTInstType MetavarKind.synthetic; +let eNew := mkAppN (mkConst `coe [u, v]) #[eType, expectedType, e, mvar]; +let mvarId := mvar.mvarId!; +catch + (do + unlessM (synthesizeInstMVarCore ref mvarId) $ + registerSyntheticMVar ref mvarId (SyntheticMVarKind.coe expectedType eType e f?); + pure eNew) + (fun ex => + match ex with + | Exception.ex (Elab.Exception.error errMsg) => throwTypeMismatchError ref expectedType eType e f? errMsg.data + | _ => throwTypeMismatchError ref expectedType eType e f?) + +/-- + If `expectedType?` is `some t`, then ensure `t` and `eType` are definitionally equal. + If they are not, then try coercions. + + Argument `f?` is used only for generating error messages. -/ +def ensureHasTypeAux (ref : Syntax) (expectedType? : Option Expr) (eType : Expr) (e : Expr) (f? : Option Expr := none) : TermElabM Expr := +match expectedType? with +| none => pure e +| some expectedType => + condM (isDefEq ref eType expectedType) + (pure e) + (tryCoe ref expectedType eType e f?) + +/-- + If `expectedType?` is `some t`, then ensure `t` and type of `e` are definitionally equal. + If they are not, then try coercions. -/ +def ensureHasType (ref : Syntax) (expectedType? : Option Expr) (e : Expr) : TermElabM Expr := +match expectedType? with +| none => pure e +| _ => do eType ← inferType ref e; ensureHasTypeAux ref expectedType? eType e + /- ======================================= Builtin elaboration functions ======================================= -/ diff --git a/src/Init/Lean/Elab/TermApp.lean b/src/Init/Lean/Elab/TermApp.lean index 2e4a90693b..16460e31b1 100644 --- a/src/Init/Lean/Elab/TermApp.lean +++ b/src/Init/Lean/Elab/TermApp.lean @@ -47,12 +47,7 @@ instMVars.forM $ fun mvarId => private def ensureArgType (ref : Syntax) (f : Expr) (arg : Expr) (expectedType : Expr) : TermElabM Expr := do argType ← inferType ref arg; -arg? ← tryEnsureHasType? ref expectedType argType arg; -match arg? with -| some arg => pure arg -| none => do - env ← getEnv; mctx ← getMCtx; lctx ← getLCtx; opts ← getOptions; - throwError ref $ Meta.Exception.mkAppTypeMismatchMessage f arg { env := env, mctx := mctx, lctx := lctx, opts := opts } +ensureHasTypeAux ref expectedType argType arg f private def elabArg (ref : Syntax) (f : Expr) (arg : Arg) (expectedType : Expr) : TermElabM Expr := match arg with