Merge branch 'dev' into doc/rationale
This commit is contained in:
commit
a51bf6f807
GPG Key ID:
4D9B1C8D10EA4C50
|
|
@ -1,4 +1,5 @@
|
|||
import Pantograph.Condensed
|
||||
import Pantograph.Delate
|
||||
import Pantograph.Elab
|
||||
import Pantograph.Environment
|
||||
import Pantograph.Frontend
|
||||
import Pantograph.Goal
|
||||
|
|
|
|||
|
|
@ -1,95 +0,0 @@
|
|||
/- structures for FFI based interface -/
|
||||
import Lean
|
||||
import Pantograph.Goal
|
||||
import Pantograph.Expr
|
||||
|
||||
open Lean
|
||||
|
||||
namespace Pantograph
|
||||
namespace Condensed
|
||||
|
||||
-- Mirrors Lean's LocalDecl
|
||||
structure LocalDecl where
|
||||
-- Default value is for testing
|
||||
fvarId: FVarId := { name := .anonymous }
|
||||
userName: Name
|
||||
|
||||
-- Normalized expression
|
||||
type : Expr
|
||||
value? : Option Expr := .none
|
||||
|
||||
structure Goal where
|
||||
mvarId: MVarId := { name := .anonymous }
|
||||
userName: Name := .anonymous
|
||||
context: Array LocalDecl
|
||||
target: Expr
|
||||
|
||||
@[export pantograph_goal_is_lhs]
|
||||
def isLHS (g: Goal) : Bool := isLHSGoal? g.target |>.isSome
|
||||
|
||||
-- Functions for creating contexts and states
|
||||
@[export pantograph_elab_context]
|
||||
def elabContext: Elab.Term.Context := {
|
||||
errToSorry := false
|
||||
}
|
||||
|
||||
end Condensed
|
||||
|
||||
-- Get the list of visible (by default) free variables from a goal
|
||||
@[export pantograph_visible_fvars_of_mvar]
|
||||
protected def visibleFVarsOfMVar (mctx: MetavarContext) (mvarId: MVarId): Option (Array FVarId) := do
|
||||
let mvarDecl ← mctx.findDecl? mvarId
|
||||
let lctx := mvarDecl.lctx
|
||||
return lctx.decls.foldl (init := #[]) fun r decl? => match decl? with
|
||||
| some decl => if decl.isAuxDecl ∨ decl.isImplementationDetail then r else r.push decl.fvarId
|
||||
| none => r
|
||||
|
||||
@[export pantograph_to_condensed_goal_m]
|
||||
def toCondensedGoal (mvarId: MVarId): MetaM Condensed.Goal := do
|
||||
let ppAuxDecls := Meta.pp.auxDecls.get (← getOptions)
|
||||
let ppImplDetailHyps := Meta.pp.implementationDetailHyps.get (← getOptions)
|
||||
let mvarDecl ← mvarId.getDecl
|
||||
let lctx := mvarDecl.lctx
|
||||
let lctx := lctx.sanitizeNames.run' { options := (← getOptions) }
|
||||
Meta.withLCtx lctx mvarDecl.localInstances do
|
||||
let ppVar (localDecl : LocalDecl) : MetaM Condensed.LocalDecl := do
|
||||
match localDecl with
|
||||
| .cdecl _ fvarId userName type _ _ =>
|
||||
let type ← instantiate type
|
||||
return { fvarId, userName, type }
|
||||
| .ldecl _ fvarId userName type value _ _ => do
|
||||
let userName := userName.simpMacroScopes
|
||||
let type ← instantiate type
|
||||
let value ← instantiate value
|
||||
return { fvarId, userName, type, value? := .some value }
|
||||
let vars ← lctx.foldlM (init := []) fun acc (localDecl : LocalDecl) => do
|
||||
let skip := !ppAuxDecls && localDecl.isAuxDecl ||
|
||||
!ppImplDetailHyps && localDecl.isImplementationDetail
|
||||
if skip then
|
||||
return acc
|
||||
else
|
||||
let var ← ppVar localDecl
|
||||
return var::acc
|
||||
return {
|
||||
mvarId,
|
||||
userName := mvarDecl.userName,
|
||||
context := vars.reverse.toArray,
|
||||
target := ← instantiate mvarDecl.type
|
||||
}
|
||||
where
|
||||
instantiate := instantiateAll
|
||||
|
||||
@[export pantograph_goal_state_to_condensed_m]
|
||||
protected def GoalState.toCondensed (state: GoalState):
|
||||
CoreM (Array Condensed.Goal):= do
|
||||
let metaM := do
|
||||
let goals := state.goals.toArray
|
||||
goals.mapM fun goal => do
|
||||
match state.mctx.findDecl? goal with
|
||||
| .some _ =>
|
||||
let serializedGoal ← toCondensedGoal goal
|
||||
pure serializedGoal
|
||||
| .none => throwError s!"Metavariable does not exist in context {goal.name}"
|
||||
metaM.run' (s := state.savedState.term.meta.meta)
|
||||
|
||||
end Pantograph
|
||||
|
|
@ -0,0 +1,562 @@
|
|||
/-
|
||||
This file handles "Delation": The conversion of Kernel view into Search view.
|
||||
-/
|
||||
import Lean
|
||||
import Std.Data.HashMap
|
||||
import Pantograph.Goal
|
||||
import Pantograph.Protocol
|
||||
|
||||
open Lean
|
||||
|
||||
-- Symbol processing functions --
|
||||
|
||||
namespace Pantograph
|
||||
|
||||
structure ProjectionApplication where
|
||||
projector: Name
|
||||
numParams: Nat
|
||||
inner: Expr
|
||||
|
||||
@[export pantograph_expr_proj_to_app]
|
||||
def exprProjToApp (env: Environment) (e: Expr): ProjectionApplication :=
|
||||
let (typeName, idx, inner) := match e with
|
||||
| .proj typeName idx inner => (typeName, idx, inner)
|
||||
| _ => panic! "Argument must be proj"
|
||||
let ctor := getStructureCtor env typeName
|
||||
let fieldName := getStructureFields env typeName |>.get! idx
|
||||
let projector := getProjFnForField? env typeName fieldName |>.get!
|
||||
{
|
||||
projector,
|
||||
numParams := ctor.numParams,
|
||||
inner,
|
||||
}
|
||||
|
||||
def _root_.Lean.Name.isAuxLemma (n : Lean.Name) : Bool := n matches .num (.str _ "_auxLemma") _
|
||||
|
||||
/-- Unfold all lemmas created by `Lean.Meta.mkAuxLemma`. These end in `_auxLemma.nn` where `nn` is a number. -/
|
||||
@[export pantograph_unfold_aux_lemmas]
|
||||
def unfoldAuxLemmas (e : Expr) : CoreM Expr := do
|
||||
Lean.Meta.deltaExpand e Lean.Name.isAuxLemma
|
||||
|
||||
/--
|
||||
Force the instantiation of delayed metavariables even if they cannot be fully
|
||||
instantiated. This is used during resumption to provide diagnostic data about
|
||||
the current goal.
|
||||
|
||||
Since Lean 4 does not have an `Expr` constructor corresponding to delayed
|
||||
metavariables, any delayed metavariables must be recursively handled by this
|
||||
function to ensure that nested delayed metavariables can be properly processed.
|
||||
The caveat is this recursive call will lead to infinite recursion if a loop
|
||||
between metavariable assignment exists.
|
||||
|
||||
This function ensures any metavariable in the result is either
|
||||
1. Delayed assigned with its pending mvar not assigned in any form
|
||||
2. Not assigned (delay or not)
|
||||
-/
|
||||
partial def instantiateDelayedMVars (eOrig: Expr) : MetaM Expr := do
|
||||
--let padding := String.join $ List.replicate level "│ "
|
||||
--IO.println s!"{padding}Starting {toString eOrig}"
|
||||
let mut result ← Meta.transform (← instantiateMVars eOrig)
|
||||
(pre := fun e => e.withApp fun f args => do
|
||||
let .mvar mvarId := f | return .continue
|
||||
--IO.println s!"{padding}├V {e}"
|
||||
let mvarDecl ← mvarId.getDecl
|
||||
|
||||
-- This is critical to maintaining the interdependency of metavariables.
|
||||
-- Without setting `.syntheticOpaque`, Lean's metavariable elimination
|
||||
-- system will not make the necessary delayed assigned mvars in case of
|
||||
-- nested mvars.
|
||||
mvarId.setKind .syntheticOpaque
|
||||
|
||||
mvarId.withContext do
|
||||
let lctx ← MonadLCtx.getLCtx
|
||||
if mvarDecl.lctx.any (λ decl => !lctx.contains decl.fvarId) then
|
||||
let violations := mvarDecl.lctx.decls.foldl (λ acc decl? => match decl? with
|
||||
| .some decl => if lctx.contains decl.fvarId then acc else acc ++ [decl.fvarId.name]
|
||||
| .none => acc) []
|
||||
panic! s!"In the context of {mvarId.name}, there are local context variable violations: {violations}"
|
||||
|
||||
if let .some assign ← getExprMVarAssignment? mvarId then
|
||||
--IO.println s!"{padding}├A ?{mvarId.name}"
|
||||
assert! !(← mvarId.isDelayedAssigned)
|
||||
return .visit (mkAppN assign args)
|
||||
else if let some { fvars, mvarIdPending } ← getDelayedMVarAssignment? mvarId then
|
||||
--let substTableStr := String.intercalate ", " $ Array.zipWith fvars args (λ fvar assign => s!"{fvar.fvarId!.name} := {assign}") |>.toList
|
||||
--IO.println s!"{padding}├MD ?{mvarId.name} := ?{mvarIdPending.name} [{substTableStr}]"
|
||||
|
||||
if args.size < fvars.size then
|
||||
throwError "Not enough arguments to instantiate a delay assigned mvar. This is due to bad implementations of a tactic: {args.size} < {fvars.size}. Expr: {toString e}; Origin: {toString eOrig}"
|
||||
--if !args.isEmpty then
|
||||
--IO.println s!"{padding}├── Arguments Begin"
|
||||
let args ← args.mapM self
|
||||
--if !args.isEmpty then
|
||||
--IO.println s!"{padding}├── Arguments End"
|
||||
if !(← mvarIdPending.isAssignedOrDelayedAssigned) then
|
||||
--IO.println s!"{padding}├T1"
|
||||
let result := mkAppN f args
|
||||
return .done result
|
||||
|
||||
let pending ← mvarIdPending.withContext do
|
||||
let inner ← instantiateDelayedMVars (.mvar mvarIdPending) --(level := level + 1)
|
||||
--IO.println s!"{padding}├Pre: {inner}"
|
||||
pure <| (← inner.abstractM fvars).instantiateRev args
|
||||
|
||||
-- Tail arguments
|
||||
let result := mkAppRange pending fvars.size args.size args
|
||||
--IO.println s!"{padding}├MD {result}"
|
||||
return .done result
|
||||
else
|
||||
assert! !(← mvarId.isAssigned)
|
||||
assert! !(← mvarId.isDelayedAssigned)
|
||||
--if !args.isEmpty then
|
||||
-- IO.println s!"{padding}├── Arguments Begin"
|
||||
let args ← args.mapM self
|
||||
--if !args.isEmpty then
|
||||
-- IO.println s!"{padding}├── Arguments End"
|
||||
|
||||
--IO.println s!"{padding}├M ?{mvarId.name}"
|
||||
return .done (mkAppN f args))
|
||||
--IO.println s!"{padding}└Result {result}"
|
||||
return result
|
||||
where
|
||||
self e := instantiateDelayedMVars e --(level := level + 1)
|
||||
|
||||
/--
|
||||
Convert an expression to an equiavlent form with
|
||||
1. No nested delayed assigned mvars
|
||||
2. No aux lemmas
|
||||
3. No assigned mvars
|
||||
-/
|
||||
@[export pantograph_instantiate_all_m]
|
||||
def instantiateAll (e: Expr): MetaM Expr := do
|
||||
let e ← instantiateDelayedMVars e
|
||||
let e ← unfoldAuxLemmas e
|
||||
return e
|
||||
|
||||
structure DelayedMVarInvocation where
|
||||
mvarIdPending: MVarId
|
||||
args: Array (FVarId × (Option Expr))
|
||||
-- Extra arguments applied to the result of this substitution
|
||||
tail: Array Expr
|
||||
|
||||
-- The pending mvar of any delayed assigned mvar must not be assigned in any way.
|
||||
@[export pantograph_to_delayed_mvar_invocation_m]
|
||||
def toDelayedMVarInvocation (e: Expr): MetaM (Option DelayedMVarInvocation) := do
|
||||
let .mvar mvarId := e.getAppFn | return .none
|
||||
let .some decl ← getDelayedMVarAssignment? mvarId | return .none
|
||||
let mvarIdPending := decl.mvarIdPending
|
||||
let mvarDecl ← mvarIdPending.getDecl
|
||||
-- Print the function application e. See Lean's `withOverApp`
|
||||
let args := e.getAppArgs
|
||||
|
||||
assert! args.size ≥ decl.fvars.size
|
||||
assert! !(← mvarIdPending.isAssigned)
|
||||
assert! !(← mvarIdPending.isDelayedAssigned)
|
||||
let fvarArgMap: Std.HashMap FVarId Expr := Std.HashMap.ofList $ (decl.fvars.map (·.fvarId!) |>.zip args).toList
|
||||
let subst ← mvarDecl.lctx.foldlM (init := []) λ acc localDecl => do
|
||||
let fvarId := localDecl.fvarId
|
||||
let a := fvarArgMap[fvarId]?
|
||||
return acc ++ [(fvarId, a)]
|
||||
|
||||
assert! decl.fvars.all (λ fvar => mvarDecl.lctx.findFVar? fvar |>.isSome)
|
||||
|
||||
return .some {
|
||||
mvarIdPending,
|
||||
args := subst.toArray,
|
||||
tail := args.toList.drop decl.fvars.size |>.toArray,
|
||||
}
|
||||
|
||||
-- Condensed representation
|
||||
|
||||
namespace Condensed
|
||||
|
||||
-- Mirrors Lean's LocalDecl
|
||||
structure LocalDecl where
|
||||
-- Default value is for testing
|
||||
fvarId: FVarId := { name := .anonymous }
|
||||
userName: Name
|
||||
|
||||
-- Normalized expression
|
||||
type : Expr
|
||||
value? : Option Expr := .none
|
||||
|
||||
structure Goal where
|
||||
mvarId: MVarId := { name := .anonymous }
|
||||
userName: Name := .anonymous
|
||||
context: Array LocalDecl
|
||||
target: Expr
|
||||
|
||||
@[export pantograph_goal_is_lhs]
|
||||
def isLHS (g: Goal) : Bool := isLHSGoal? g.target |>.isSome
|
||||
|
||||
end Condensed
|
||||
|
||||
-- Get the list of visible (by default) free variables from a goal
|
||||
@[export pantograph_visible_fvars_of_mvar]
|
||||
protected def visibleFVarsOfMVar (mctx: MetavarContext) (mvarId: MVarId): Option (Array FVarId) := do
|
||||
let mvarDecl ← mctx.findDecl? mvarId
|
||||
let lctx := mvarDecl.lctx
|
||||
return lctx.decls.foldl (init := #[]) fun r decl? => match decl? with
|
||||
| some decl => if decl.isAuxDecl ∨ decl.isImplementationDetail then r else r.push decl.fvarId
|
||||
| none => r
|
||||
|
||||
@[export pantograph_to_condensed_goal_m]
|
||||
def toCondensedGoal (mvarId: MVarId): MetaM Condensed.Goal := do
|
||||
let ppAuxDecls := Meta.pp.auxDecls.get (← getOptions)
|
||||
let ppImplDetailHyps := Meta.pp.implementationDetailHyps.get (← getOptions)
|
||||
let mvarDecl ← mvarId.getDecl
|
||||
let lctx := mvarDecl.lctx
|
||||
let lctx := lctx.sanitizeNames.run' { options := (← getOptions) }
|
||||
Meta.withLCtx lctx mvarDecl.localInstances do
|
||||
let ppVar (localDecl : LocalDecl) : MetaM Condensed.LocalDecl := do
|
||||
match localDecl with
|
||||
| .cdecl _ fvarId userName type _ _ =>
|
||||
let type ← instantiate type
|
||||
return { fvarId, userName, type }
|
||||
| .ldecl _ fvarId userName type value _ _ => do
|
||||
let userName := userName.simpMacroScopes
|
||||
let type ← instantiate type
|
||||
let value ← instantiate value
|
||||
return { fvarId, userName, type, value? := .some value }
|
||||
let vars ← lctx.foldlM (init := []) fun acc (localDecl : LocalDecl) => do
|
||||
let skip := !ppAuxDecls && localDecl.isAuxDecl ||
|
||||
!ppImplDetailHyps && localDecl.isImplementationDetail
|
||||
if skip then
|
||||
return acc
|
||||
else
|
||||
let var ← ppVar localDecl
|
||||
return var::acc
|
||||
return {
|
||||
mvarId,
|
||||
userName := mvarDecl.userName,
|
||||
context := vars.reverse.toArray,
|
||||
target := ← instantiate mvarDecl.type
|
||||
}
|
||||
where
|
||||
instantiate := instantiateAll
|
||||
|
||||
@[export pantograph_goal_state_to_condensed_m]
|
||||
protected def GoalState.toCondensed (state: GoalState):
|
||||
CoreM (Array Condensed.Goal):= do
|
||||
let metaM := do
|
||||
let goals := state.goals.toArray
|
||||
goals.mapM fun goal => do
|
||||
match state.mctx.findDecl? goal with
|
||||
| .some _ =>
|
||||
let serializedGoal ← toCondensedGoal goal
|
||||
pure serializedGoal
|
||||
| .none => throwError s!"Metavariable does not exist in context {goal.name}"
|
||||
metaM.run' (s := state.savedState.term.meta.meta)
|
||||
|
||||
def typeExprToBound (expr: Expr): MetaM Protocol.BoundExpression := do
|
||||
Meta.forallTelescope expr fun arr body => do
|
||||
let binders ← arr.mapM fun fvar => do
|
||||
return (toString (← fvar.fvarId!.getUserName), toString (← Meta.ppExpr (← fvar.fvarId!.getType)))
|
||||
return { binders, target := toString (← Meta.ppExpr body) }
|
||||
|
||||
def serializeName (name: Name) (sanitize: Bool := true): String :=
|
||||
let internal := name.isInaccessibleUserName || name.hasMacroScopes
|
||||
if sanitize && internal then "_"
|
||||
else toString name |> addQuotes
|
||||
where
|
||||
addQuotes (n: String) :=
|
||||
let quote := "\""
|
||||
if n.contains Lean.idBeginEscape then s!"{quote}{n}{quote}" else n
|
||||
|
||||
/-- serialize a sort level. Expression is optimized to be compact e.g. `(+ u 2)` -/
|
||||
partial def serializeSortLevel (level: Level) (sanitize: Bool): String :=
|
||||
let k := level.getOffset
|
||||
let u := level.getLevelOffset
|
||||
let u_str := match u with
|
||||
| .zero => "0"
|
||||
| .succ _ => panic! "getLevelOffset should not return .succ"
|
||||
| .max v w =>
|
||||
let v := serializeSortLevel v sanitize
|
||||
let w := serializeSortLevel w sanitize
|
||||
s!"(:max {v} {w})"
|
||||
| .imax v w =>
|
||||
let v := serializeSortLevel v sanitize
|
||||
let w := serializeSortLevel w sanitize
|
||||
s!"(:imax {v} {w})"
|
||||
| .param name =>
|
||||
let name := serializeName name sanitize
|
||||
s!"{name}"
|
||||
| .mvar id =>
|
||||
let name := serializeName id.name sanitize
|
||||
s!"(:mv {name})"
|
||||
match k, u with
|
||||
| 0, _ => u_str
|
||||
| _, .zero => s!"{k}"
|
||||
| _, _ => s!"(+ {u_str} {k})"
|
||||
|
||||
|
||||
/--
|
||||
Completely serializes an expression tree. Json not used due to compactness
|
||||
|
||||
A `_` symbol in the AST indicates automatic deductions not present in the original expression.
|
||||
-/
|
||||
partial def serializeExpressionSexp (expr: Expr) (sanitize: Bool := true): MetaM String := do
|
||||
self expr
|
||||
where
|
||||
delayedMVarToSexp (e: Expr): MetaM (Option String) := do
|
||||
let .some invocation ← toDelayedMVarInvocation e | return .none
|
||||
let callee ← self $ .mvar invocation.mvarIdPending
|
||||
let sites ← invocation.args.mapM (λ (fvarId, arg) => do
|
||||
let arg := match arg with
|
||||
| .some arg => arg
|
||||
| .none => .fvar fvarId
|
||||
self arg
|
||||
)
|
||||
let tailArgs ← invocation.tail.mapM self
|
||||
|
||||
let sites := " ".intercalate sites.toList
|
||||
let result := if tailArgs.isEmpty then
|
||||
s!"(:subst {callee} {sites})"
|
||||
else
|
||||
let tailArgs := " ".intercalate tailArgs.toList
|
||||
s!"((:subst {callee} {sites}) {tailArgs})"
|
||||
return .some result
|
||||
|
||||
self (e: Expr): MetaM String := do
|
||||
if let .some result ← delayedMVarToSexp e then
|
||||
return result
|
||||
match e with
|
||||
| .bvar deBruijnIndex =>
|
||||
-- This is very common so the index alone is shown. Literals are handled below.
|
||||
-- The raw de Bruijn index should never appear in an unbound setting. In
|
||||
-- Lean these are handled using a `#` prefix.
|
||||
pure s!"{deBruijnIndex}"
|
||||
| .fvar fvarId =>
|
||||
let name := ofName fvarId.name
|
||||
pure s!"(:fv {name})"
|
||||
| .mvar mvarId => do
|
||||
let pref := if ← mvarId.isDelayedAssigned then "mvd" else "mv"
|
||||
let name := ofName mvarId.name
|
||||
pure s!"(:{pref} {name})"
|
||||
| .sort level =>
|
||||
let level := serializeSortLevel level sanitize
|
||||
pure s!"(:sort {level})"
|
||||
| .const declName _ =>
|
||||
-- The universe level of the const expression is elided since it should be
|
||||
-- inferrable from surrounding expression
|
||||
pure s!"(:c {declName})"
|
||||
| .app _ _ => do
|
||||
let fn' ← self e.getAppFn
|
||||
let args := (← e.getAppArgs.mapM self) |>.toList
|
||||
let args := " ".intercalate args
|
||||
pure s!"({fn'} {args})"
|
||||
| .lam binderName binderType body binderInfo => do
|
||||
let binderName' := ofName binderName
|
||||
let binderType' ← self binderType
|
||||
let body' ← self body
|
||||
let binderInfo' := binderInfoSexp binderInfo
|
||||
pure s!"(:lambda {binderName'} {binderType'} {body'}{binderInfo'})"
|
||||
| .forallE binderName binderType body binderInfo => do
|
||||
let binderName' := ofName binderName
|
||||
let binderType' ← self binderType
|
||||
let body' ← self body
|
||||
let binderInfo' := binderInfoSexp binderInfo
|
||||
pure s!"(:forall {binderName'} {binderType'} {body'}{binderInfo'})"
|
||||
| .letE name type value body _ => do
|
||||
-- Dependent boolean flag diacarded
|
||||
let name' := serializeName name
|
||||
let type' ← self type
|
||||
let value' ← self value
|
||||
let body' ← self body
|
||||
pure s!"(:let {name'} {type'} {value'} {body'})"
|
||||
| .lit v =>
|
||||
-- To not burden the downstream parser who needs to handle this, the literal
|
||||
-- is wrapped in a :lit sexp.
|
||||
let v' := match v with
|
||||
| .natVal val => toString val
|
||||
| .strVal val => s!"\"{val}\""
|
||||
pure s!"(:lit {v'})"
|
||||
| .mdata _ inner =>
|
||||
-- NOTE: Equivalent to expr itself, but mdata influences the prettyprinter
|
||||
-- It may become necessary to incorporate the metadata.
|
||||
self inner
|
||||
| .proj _ _ _ => do
|
||||
let env ← getEnv
|
||||
let projApp := exprProjToApp env e
|
||||
let autos := String.intercalate " " (List.replicate projApp.numParams "_")
|
||||
let inner ← self projApp.inner
|
||||
pure s!"((:c {projApp.projector}) {autos} {inner})"
|
||||
-- Elides all unhygenic names
|
||||
binderInfoSexp : Lean.BinderInfo → String
|
||||
| .default => ""
|
||||
| .implicit => " :implicit"
|
||||
| .strictImplicit => " :strictImplicit"
|
||||
| .instImplicit => " :instImplicit"
|
||||
ofName (name: Name) := serializeName name sanitize
|
||||
|
||||
def serializeExpression (options: @&Protocol.Options) (e: Expr): MetaM Protocol.Expression := do
|
||||
let pp?: Option String ← match options.printExprPretty with
|
||||
| true => pure $ .some $ toString $ ← Meta.ppExpr e
|
||||
| false => pure $ .none
|
||||
let sexp?: Option String ← match options.printExprAST with
|
||||
| true => pure $ .some $ ← serializeExpressionSexp e
|
||||
| false => pure $ .none
|
||||
let dependentMVars? ← match options.printDependentMVars with
|
||||
| true => pure $ .some $ (← Meta.getMVars e).map (λ mvarId => mvarId.name.toString)
|
||||
| false => pure $ .none
|
||||
return {
|
||||
pp?,
|
||||
sexp?
|
||||
dependentMVars?,
|
||||
}
|
||||
|
||||
|
||||
/-- Adapted from ppGoal -/
|
||||
def serializeGoal (options: @&Protocol.Options) (goal: MVarId) (mvarDecl: MetavarDecl) (parentDecl?: Option MetavarDecl := .none)
|
||||
: MetaM Protocol.Goal := do
|
||||
-- Options for printing; See Meta.ppGoal for details
|
||||
let showLetValues := true
|
||||
let ppAuxDecls := options.printAuxDecls
|
||||
let ppImplDetailHyps := options.printImplementationDetailHyps
|
||||
let lctx := mvarDecl.lctx
|
||||
let lctx := lctx.sanitizeNames.run' { options := (← getOptions) }
|
||||
Meta.withLCtx lctx mvarDecl.localInstances do
|
||||
let ppVarNameOnly (localDecl: LocalDecl): MetaM Protocol.Variable := do
|
||||
match localDecl with
|
||||
| .cdecl _ fvarId userName _ _ _ =>
|
||||
return {
|
||||
name := ofName fvarId.name,
|
||||
userName:= ofName userName.simpMacroScopes,
|
||||
isInaccessible := userName.isInaccessibleUserName
|
||||
}
|
||||
| .ldecl _ fvarId userName _ _ _ _ => do
|
||||
return {
|
||||
name := ofName fvarId.name,
|
||||
userName := toString userName.simpMacroScopes,
|
||||
isInaccessible := userName.isInaccessibleUserName
|
||||
}
|
||||
let ppVar (localDecl : LocalDecl) : MetaM Protocol.Variable := do
|
||||
match localDecl with
|
||||
| .cdecl _ fvarId userName type _ _ =>
|
||||
let userName := userName.simpMacroScopes
|
||||
let type ← instantiate type
|
||||
return {
|
||||
name := ofName fvarId.name,
|
||||
userName:= ofName userName,
|
||||
isInaccessible := userName.isInaccessibleUserName
|
||||
type? := .some (← serializeExpression options type)
|
||||
}
|
||||
| .ldecl _ fvarId userName type val _ _ => do
|
||||
let userName := userName.simpMacroScopes
|
||||
let type ← instantiate type
|
||||
let value? ← if showLetValues then
|
||||
let val ← instantiate val
|
||||
pure $ .some (← serializeExpression options val)
|
||||
else
|
||||
pure $ .none
|
||||
return {
|
||||
name := ofName fvarId.name,
|
||||
userName:= ofName userName,
|
||||
isInaccessible := userName.isInaccessibleUserName
|
||||
type? := .some (← serializeExpression options type)
|
||||
value? := value?
|
||||
}
|
||||
let vars ← lctx.foldlM (init := []) fun acc (localDecl : LocalDecl) => do
|
||||
let skip := !ppAuxDecls && localDecl.isAuxDecl ||
|
||||
!ppImplDetailHyps && localDecl.isImplementationDetail
|
||||
if skip then
|
||||
return acc
|
||||
else
|
||||
let nameOnly := options.noRepeat && (parentDecl?.map
|
||||
(λ decl => decl.lctx.find? localDecl.fvarId |>.isSome) |>.getD false)
|
||||
let var ← match nameOnly with
|
||||
| true => ppVarNameOnly localDecl
|
||||
| false => ppVar localDecl
|
||||
return var::acc
|
||||
return {
|
||||
name := ofName goal.name,
|
||||
userName? := if mvarDecl.userName == .anonymous then .none else .some (ofName mvarDecl.userName),
|
||||
isConversion := isLHSGoal? mvarDecl.type |>.isSome,
|
||||
target := (← serializeExpression options (← instantiate mvarDecl.type)),
|
||||
vars := vars.reverse.toArray
|
||||
}
|
||||
where
|
||||
instantiate := instantiateAll
|
||||
ofName (n: Name) := serializeName n (sanitize := false)
|
||||
|
||||
protected def GoalState.serializeGoals
|
||||
(state: GoalState)
|
||||
(parent: Option GoalState := .none)
|
||||
(options: @&Protocol.Options := {}):
|
||||
MetaM (Array Protocol.Goal):= do
|
||||
state.restoreMetaM
|
||||
let goals := state.goals.toArray
|
||||
let parentDecl? := parent.bind (λ parentState => parentState.mctx.findDecl? state.parentMVar?.get!)
|
||||
goals.mapM fun goal => do
|
||||
match state.mctx.findDecl? goal with
|
||||
| .some mvarDecl =>
|
||||
let serializedGoal ← serializeGoal options goal mvarDecl (parentDecl? := parentDecl?)
|
||||
pure serializedGoal
|
||||
| .none => throwError s!"Metavariable does not exist in context {goal.name}"
|
||||
|
||||
/-- Print the metavariables in a readable format -/
|
||||
@[export pantograph_goal_state_diag_m]
|
||||
protected def GoalState.diag (goalState: GoalState) (parent?: Option GoalState := .none) (options: Protocol.GoalDiag := {}): CoreM String := do
|
||||
let metaM: MetaM String := do
|
||||
goalState.restoreMetaM
|
||||
let savedState := goalState.savedState
|
||||
let goals := savedState.tactic.goals
|
||||
let mctx ← getMCtx
|
||||
let root := goalState.root
|
||||
-- Print the root
|
||||
let result: String ← match mctx.decls.find? root with
|
||||
| .some decl => printMVar ">" root decl
|
||||
| .none => pure s!">{root.name}: ??"
|
||||
let resultGoals ← goals.filter (· != root) |>.mapM (fun mvarId =>
|
||||
match mctx.decls.find? mvarId with
|
||||
| .some decl => printMVar "⊢" mvarId decl
|
||||
| .none => pure s!"⊢{mvarId.name}: ??"
|
||||
)
|
||||
let goals := goals.toSSet
|
||||
let resultOthers ← mctx.decls.toList.filter (λ (mvarId, _) =>
|
||||
!(goals.contains mvarId || mvarId == root) && options.printAll)
|
||||
|>.mapM (fun (mvarId, decl) => do
|
||||
let pref := if parentHasMVar mvarId then " " else "~"
|
||||
printMVar pref mvarId decl
|
||||
)
|
||||
pure $ result ++ "\n" ++ (resultGoals.map (· ++ "\n") |> String.join) ++ (resultOthers.map (· ++ "\n") |> String.join)
|
||||
metaM.run' {}
|
||||
where
|
||||
printMVar (pref: String) (mvarId: MVarId) (decl: MetavarDecl): MetaM String := mvarId.withContext do
|
||||
let resultFVars: List String ←
|
||||
if options.printContext then
|
||||
decl.lctx.fvarIdToDecl.toList.mapM (λ (fvarId, decl) =>
|
||||
do pure $ (← printFVar fvarId decl) ++ "\n")
|
||||
else
|
||||
pure []
|
||||
let type ← if options.instantiate
|
||||
then instantiateAll decl.type
|
||||
else pure $ decl.type
|
||||
let type_sexp ← if options.printSexp then
|
||||
let sexp ← serializeExpressionSexp type (sanitize := false)
|
||||
pure <| " " ++ sexp
|
||||
else
|
||||
pure ""
|
||||
let resultMain: String := s!"{pref}{mvarId.name}{userNameToString decl.userName}: {← Meta.ppExpr decl.type}{type_sexp}"
|
||||
let resultValue: String ←
|
||||
if options.printValue then
|
||||
if let .some value ← getExprMVarAssignment? mvarId then
|
||||
let value ← if options.instantiate
|
||||
then instantiateAll value
|
||||
else pure $ value
|
||||
pure s!"\n := {← Meta.ppExpr value}"
|
||||
else if let .some { mvarIdPending, .. } ← getDelayedMVarAssignment? mvarId then
|
||||
pure s!"\n ::= {mvarIdPending.name}"
|
||||
else
|
||||
pure ""
|
||||
else
|
||||
pure ""
|
||||
pure $ (String.join resultFVars) ++ resultMain ++ resultValue
|
||||
printFVar (fvarId: FVarId) (decl: LocalDecl): MetaM String := do
|
||||
pure s!" | {fvarId.name}{userNameToString decl.userName}: {← Meta.ppExpr decl.type}"
|
||||
userNameToString : Name → String
|
||||
| .anonymous => ""
|
||||
| other => s!"[{other}]"
|
||||
parentHasMVar (mvarId: MVarId): Bool := parent?.map (λ state => state.mctx.decls.contains mvarId) |>.getD true
|
||||
|
||||
end Pantograph
|
||||
|
|
@ -0,0 +1,40 @@
|
|||
import Lean
|
||||
open Lean
|
||||
|
||||
namespace Pantograph
|
||||
|
||||
-- Functions for creating contexts and states
|
||||
@[export pantograph_default_elab_context]
|
||||
def defaultElabContext: Elab.Term.Context := {
|
||||
errToSorry := false
|
||||
}
|
||||
|
||||
/-- Read syntax object from string -/
|
||||
def parseTerm (env: Environment) (s: String): Except String Syntax :=
|
||||
Parser.runParserCategory
|
||||
(env := env)
|
||||
(catName := `term)
|
||||
(input := s)
|
||||
(fileName := "<stdin>")
|
||||
|
||||
def parseTermM [Monad m] [MonadEnv m] (s: String): m (Except String Syntax) := do
|
||||
return Parser.runParserCategory
|
||||
(env := ← MonadEnv.getEnv)
|
||||
(catName := `term)
|
||||
(input := s)
|
||||
(fileName := "<stdin>")
|
||||
|
||||
/-- Parse a syntax object. May generate additional metavariables! -/
|
||||
def elabType (syn: Syntax): Elab.TermElabM (Except String Expr) := do
|
||||
try
|
||||
let expr ← Elab.Term.elabType syn
|
||||
return .ok expr
|
||||
catch ex => return .error (← ex.toMessageData.toString)
|
||||
def elabTerm (syn: Syntax) (expectedType? : Option Expr := .none): Elab.TermElabM (Except String Expr) := do
|
||||
try
|
||||
let expr ← Elab.Term.elabTerm (stx := syn) expectedType?
|
||||
return .ok expr
|
||||
catch ex => return .error (← ex.toMessageData.toString)
|
||||
|
||||
|
||||
end Pantograph
|
||||
|
|
@ -1,6 +1,9 @@
|
|||
import Pantograph.Delate
|
||||
import Pantograph.Elab
|
||||
import Pantograph.Protocol
|
||||
import Pantograph.Serial
|
||||
import Lean
|
||||
import Lean.Environment
|
||||
import Lean.Replay
|
||||
|
||||
open Lean
|
||||
open Pantograph
|
||||
|
|
|
|||
|
|
@ -1,162 +0,0 @@
|
|||
import Lean
|
||||
import Std.Data.HashMap
|
||||
|
||||
open Lean
|
||||
|
||||
namespace Pantograph
|
||||
|
||||
structure ProjectionApplication where
|
||||
projector: Name
|
||||
numParams: Nat
|
||||
inner: Expr
|
||||
|
||||
@[export pantograph_expr_proj_to_app]
|
||||
def exprProjToApp (env: Environment) (e: Expr): ProjectionApplication :=
|
||||
let (typeName, idx, inner) := match e with
|
||||
| .proj typeName idx inner => (typeName, idx, inner)
|
||||
| _ => panic! "Argument must be proj"
|
||||
let ctor := getStructureCtor env typeName
|
||||
let fieldName := getStructureFields env typeName |>.get! idx
|
||||
let projector := getProjFnForField? env typeName fieldName |>.get!
|
||||
{
|
||||
projector,
|
||||
numParams := ctor.numParams,
|
||||
inner,
|
||||
}
|
||||
|
||||
def _root_.Lean.Name.isAuxLemma (n : Lean.Name) : Bool := n matches .num (.str _ "_auxLemma") _
|
||||
|
||||
/-- Unfold all lemmas created by `Lean.Meta.mkAuxLemma`. These end in `_auxLemma.nn` where `nn` is a number. -/
|
||||
@[export pantograph_unfold_aux_lemmas]
|
||||
def unfoldAuxLemmas (e : Expr) : CoreM Expr := do
|
||||
Lean.Meta.deltaExpand e Lean.Name.isAuxLemma
|
||||
|
||||
/--
|
||||
Force the instantiation of delayed metavariables even if they cannot be fully
|
||||
instantiated. This is used during resumption to provide diagnostic data about
|
||||
the current goal.
|
||||
|
||||
Since Lean 4 does not have an `Expr` constructor corresponding to delayed
|
||||
metavariables, any delayed metavariables must be recursively handled by this
|
||||
function to ensure that nested delayed metavariables can be properly processed.
|
||||
The caveat is this recursive call will lead to infinite recursion if a loop
|
||||
between metavariable assignment exists.
|
||||
|
||||
This function ensures any metavariable in the result is either
|
||||
1. Delayed assigned with its pending mvar not assigned in any form
|
||||
2. Not assigned (delay or not)
|
||||
-/
|
||||
partial def instantiateDelayedMVars (eOrig: Expr) : MetaM Expr := do
|
||||
--let padding := String.join $ List.replicate level "│ "
|
||||
--IO.println s!"{padding}Starting {toString eOrig}"
|
||||
let mut result ← Meta.transform (← instantiateMVars eOrig)
|
||||
(pre := fun e => e.withApp fun f args => do
|
||||
let .mvar mvarId := f | return .continue
|
||||
--IO.println s!"{padding}├V {e}"
|
||||
let mvarDecl ← mvarId.getDecl
|
||||
|
||||
-- This is critical to maintaining the interdependency of metavariables.
|
||||
-- Without setting `.syntheticOpaque`, Lean's metavariable elimination
|
||||
-- system will not make the necessary delayed assigned mvars in case of
|
||||
-- nested mvars.
|
||||
mvarId.setKind .syntheticOpaque
|
||||
|
||||
mvarId.withContext do
|
||||
let lctx ← MonadLCtx.getLCtx
|
||||
if mvarDecl.lctx.any (λ decl => !lctx.contains decl.fvarId) then
|
||||
let violations := mvarDecl.lctx.decls.foldl (λ acc decl? => match decl? with
|
||||
| .some decl => if lctx.contains decl.fvarId then acc else acc ++ [decl.fvarId.name]
|
||||
| .none => acc) []
|
||||
panic! s!"In the context of {mvarId.name}, there are local context variable violations: {violations}"
|
||||
|
||||
if let .some assign ← getExprMVarAssignment? mvarId then
|
||||
--IO.println s!"{padding}├A ?{mvarId.name}"
|
||||
assert! !(← mvarId.isDelayedAssigned)
|
||||
return .visit (mkAppN assign args)
|
||||
else if let some { fvars, mvarIdPending } ← getDelayedMVarAssignment? mvarId then
|
||||
--let substTableStr := String.intercalate ", " $ Array.zipWith fvars args (λ fvar assign => s!"{fvar.fvarId!.name} := {assign}") |>.toList
|
||||
--IO.println s!"{padding}├MD ?{mvarId.name} := ?{mvarIdPending.name} [{substTableStr}]"
|
||||
|
||||
if args.size < fvars.size then
|
||||
throwError "Not enough arguments to instantiate a delay assigned mvar. This is due to bad implementations of a tactic: {args.size} < {fvars.size}. Expr: {toString e}; Origin: {toString eOrig}"
|
||||
--if !args.isEmpty then
|
||||
--IO.println s!"{padding}├── Arguments Begin"
|
||||
let args ← args.mapM self
|
||||
--if !args.isEmpty then
|
||||
--IO.println s!"{padding}├── Arguments End"
|
||||
if !(← mvarIdPending.isAssignedOrDelayedAssigned) then
|
||||
--IO.println s!"{padding}├T1"
|
||||
let result := mkAppN f args
|
||||
return .done result
|
||||
|
||||
let pending ← mvarIdPending.withContext do
|
||||
let inner ← instantiateDelayedMVars (.mvar mvarIdPending) --(level := level + 1)
|
||||
--IO.println s!"{padding}├Pre: {inner}"
|
||||
pure <| (← inner.abstractM fvars).instantiateRev args
|
||||
|
||||
-- Tail arguments
|
||||
let result := mkAppRange pending fvars.size args.size args
|
||||
--IO.println s!"{padding}├MD {result}"
|
||||
return .done result
|
||||
else
|
||||
assert! !(← mvarId.isAssigned)
|
||||
assert! !(← mvarId.isDelayedAssigned)
|
||||
--if !args.isEmpty then
|
||||
-- IO.println s!"{padding}├── Arguments Begin"
|
||||
let args ← args.mapM self
|
||||
--if !args.isEmpty then
|
||||
-- IO.println s!"{padding}├── Arguments End"
|
||||
|
||||
--IO.println s!"{padding}├M ?{mvarId.name}"
|
||||
return .done (mkAppN f args))
|
||||
--IO.println s!"{padding}└Result {result}"
|
||||
return result
|
||||
where
|
||||
self e := instantiateDelayedMVars e --(level := level + 1)
|
||||
|
||||
/--
|
||||
Convert an expression to an equiavlent form with
|
||||
1. No nested delayed assigned mvars
|
||||
2. No aux lemmas
|
||||
3. No assigned mvars
|
||||
-/
|
||||
@[export pantograph_instantiate_all_m]
|
||||
def instantiateAll (e: Expr): MetaM Expr := do
|
||||
let e ← instantiateDelayedMVars e
|
||||
let e ← unfoldAuxLemmas e
|
||||
return e
|
||||
|
||||
structure DelayedMVarInvocation where
|
||||
mvarIdPending: MVarId
|
||||
args: Array (FVarId × (Option Expr))
|
||||
-- Extra arguments applied to the result of this substitution
|
||||
tail: Array Expr
|
||||
|
||||
-- The pending mvar of any delayed assigned mvar must not be assigned in any way.
|
||||
@[export pantograph_to_delayed_mvar_invocation_m]
|
||||
def toDelayedMVarInvocation (e: Expr): MetaM (Option DelayedMVarInvocation) := do
|
||||
let .mvar mvarId := e.getAppFn | return .none
|
||||
let .some decl ← getDelayedMVarAssignment? mvarId | return .none
|
||||
let mvarIdPending := decl.mvarIdPending
|
||||
let mvarDecl ← mvarIdPending.getDecl
|
||||
-- Print the function application e. See Lean's `withOverApp`
|
||||
let args := e.getAppArgs
|
||||
|
||||
assert! args.size ≥ decl.fvars.size
|
||||
assert! !(← mvarIdPending.isAssigned)
|
||||
assert! !(← mvarIdPending.isDelayedAssigned)
|
||||
let fvarArgMap: Std.HashMap FVarId Expr := Std.HashMap.ofList $ (decl.fvars.map (·.fvarId!) |>.zip args).toList
|
||||
let subst ← mvarDecl.lctx.foldlM (init := []) λ acc localDecl => do
|
||||
let fvarId := localDecl.fvarId
|
||||
let a := fvarArgMap[fvarId]?
|
||||
return acc ++ [(fvarId, a)]
|
||||
|
||||
assert! decl.fvars.all (λ fvar => mvarDecl.lctx.findFVar? fvar |>.isSome)
|
||||
|
||||
return .some {
|
||||
mvarIdPending,
|
||||
args := subst.toArray,
|
||||
tail := args.toList.drop decl.fvars.size |>.toArray,
|
||||
}
|
||||
|
||||
end Pantograph
|
||||
|
|
@ -1,8 +1,7 @@
|
|||
import Pantograph.Condensed
|
||||
import Pantograph.Environment
|
||||
import Pantograph.Goal
|
||||
import Pantograph.Protocol
|
||||
import Pantograph.Serial
|
||||
import Pantograph.Delate
|
||||
import Pantograph.Version
|
||||
import Lean
|
||||
|
||||
|
|
@ -42,7 +41,7 @@ namespace Pantograph
|
|||
def runMetaM { α } (metaM: MetaM α): CoreM α :=
|
||||
metaM.run'
|
||||
def runTermElabM { α } (termElabM: Elab.TermElabM α): CoreM α :=
|
||||
termElabM.run' (ctx := Condensed.elabContext) |>.run'
|
||||
termElabM.run' (ctx := defaultElabContext) |>.run'
|
||||
|
||||
def errorI (type desc: String): Protocol.InteractionError := { error := type, desc := desc }
|
||||
|
||||
|
|
|
|||
|
|
@ -183,6 +183,12 @@ structure EnvAdd where
|
|||
structure EnvAddResult where
|
||||
deriving Lean.ToJson
|
||||
|
||||
structure EnvSaveLoad where
|
||||
path: System.FilePath
|
||||
deriving Lean.FromJson
|
||||
structure EnvSaveLoadResult where
|
||||
deriving Lean.ToJson
|
||||
|
||||
/-- Set options; See `Options` struct above for meanings -/
|
||||
structure OptionsSet where
|
||||
printJsonPretty?: Option Bool
|
||||
|
|
|
|||
|
|
@ -1,362 +1,73 @@
|
|||
/-
|
||||
All serialisation functions;
|
||||
This replicates the behaviour of `Scope`s in `Lean/Elab/Command.lean` without
|
||||
using `Scope`s.
|
||||
import Lean.Environment
|
||||
import Lean.Replay
|
||||
import Init.System.IOError
|
||||
import Std.Data.HashMap
|
||||
|
||||
/-!
|
||||
Input/Output functions
|
||||
|
||||
# Pickling and unpickling objects
|
||||
|
||||
By abusing `saveModuleData` and `readModuleData` we can pickle and unpickle objects to disk.
|
||||
-/
|
||||
import Lean
|
||||
import Pantograph.Condensed
|
||||
import Pantograph.Expr
|
||||
import Pantograph.Goal
|
||||
import Pantograph.Protocol
|
||||
|
||||
open Lean
|
||||
|
||||
-- Symbol processing functions --
|
||||
|
||||
namespace Pantograph
|
||||
|
||||
|
||||
--- Input Functions ---
|
||||
|
||||
/-- Read syntax object from string -/
|
||||
def parseTerm (env: Environment) (s: String): Except String Syntax :=
|
||||
Parser.runParserCategory
|
||||
(env := env)
|
||||
(catName := `term)
|
||||
(input := s)
|
||||
(fileName := "<stdin>")
|
||||
|
||||
def parseTermM [Monad m] [MonadEnv m] (s: String): m (Except String Syntax) := do
|
||||
return Parser.runParserCategory
|
||||
(env := ← MonadEnv.getEnv)
|
||||
(catName := `term)
|
||||
(input := s)
|
||||
(fileName := "<stdin>")
|
||||
|
||||
/-- Parse a syntax object. May generate additional metavariables! -/
|
||||
def elabType (syn: Syntax): Elab.TermElabM (Except String Expr) := do
|
||||
try
|
||||
let expr ← Elab.Term.elabType syn
|
||||
return .ok expr
|
||||
catch ex => return .error (← ex.toMessageData.toString)
|
||||
def elabTerm (syn: Syntax) (expectedType? : Option Expr := .none): Elab.TermElabM (Except String Expr) := do
|
||||
try
|
||||
let expr ← Elab.Term.elabTerm (stx := syn) expectedType?
|
||||
return .ok expr
|
||||
catch ex => return .error (← ex.toMessageData.toString)
|
||||
|
||||
|
||||
--- Output Functions ---
|
||||
|
||||
def typeExprToBound (expr: Expr): MetaM Protocol.BoundExpression := do
|
||||
Meta.forallTelescope expr fun arr body => do
|
||||
let binders ← arr.mapM fun fvar => do
|
||||
return (toString (← fvar.fvarId!.getUserName), toString (← Meta.ppExpr (← fvar.fvarId!.getType)))
|
||||
return { binders, target := toString (← Meta.ppExpr body) }
|
||||
|
||||
def serializeName (name: Name) (sanitize: Bool := true): String :=
|
||||
let internal := name.isInaccessibleUserName || name.hasMacroScopes
|
||||
if sanitize && internal then "_"
|
||||
else toString name |> addQuotes
|
||||
where
|
||||
addQuotes (n: String) :=
|
||||
let quote := "\""
|
||||
if n.contains Lean.idBeginEscape then s!"{quote}{n}{quote}" else n
|
||||
|
||||
/-- serialize a sort level. Expression is optimized to be compact e.g. `(+ u 2)` -/
|
||||
partial def serializeSortLevel (level: Level) (sanitize: Bool): String :=
|
||||
let k := level.getOffset
|
||||
let u := level.getLevelOffset
|
||||
let u_str := match u with
|
||||
| .zero => "0"
|
||||
| .succ _ => panic! "getLevelOffset should not return .succ"
|
||||
| .max v w =>
|
||||
let v := serializeSortLevel v sanitize
|
||||
let w := serializeSortLevel w sanitize
|
||||
s!"(:max {v} {w})"
|
||||
| .imax v w =>
|
||||
let v := serializeSortLevel v sanitize
|
||||
let w := serializeSortLevel w sanitize
|
||||
s!"(:imax {v} {w})"
|
||||
| .param name =>
|
||||
let name := serializeName name sanitize
|
||||
s!"{name}"
|
||||
| .mvar id =>
|
||||
let name := serializeName id.name sanitize
|
||||
s!"(:mv {name})"
|
||||
match k, u with
|
||||
| 0, _ => u_str
|
||||
| _, .zero => s!"{k}"
|
||||
| _, _ => s!"(+ {u_str} {k})"
|
||||
|
||||
/--
|
||||
Save an object to disk.
|
||||
If you need to write multiple objects from within a single declaration,
|
||||
you will need to provide a unique `key` for each.
|
||||
-/
|
||||
def pickle {α : Type} (path : System.FilePath) (x : α) (key : Name := by exact decl_name%) : IO Unit :=
|
||||
saveModuleData path key (unsafe unsafeCast x)
|
||||
|
||||
/--
|
||||
Completely serializes an expression tree. Json not used due to compactness
|
||||
Load an object from disk.
|
||||
Note: The returned `CompactedRegion` can be used to free the memory behind the value
|
||||
of type `α`, using `CompactedRegion.free` (which is only safe once all references to the `α` are
|
||||
released). Ignoring the `CompactedRegion` results in the data being leaked.
|
||||
Use `withUnpickle` to call `CompactedRegion.free` automatically.
|
||||
|
||||
A `_` symbol in the AST indicates automatic deductions not present in the original expression.
|
||||
This function is unsafe because the data being loaded may not actually have type `α`, and this
|
||||
may cause crashes or other bad behavior.
|
||||
-/
|
||||
partial def serializeExpressionSexp (expr: Expr) (sanitize: Bool := true): MetaM String := do
|
||||
self expr
|
||||
where
|
||||
delayedMVarToSexp (e: Expr): MetaM (Option String) := do
|
||||
let .some invocation ← toDelayedMVarInvocation e | return .none
|
||||
let callee ← self $ .mvar invocation.mvarIdPending
|
||||
let sites ← invocation.args.mapM (λ (fvarId, arg) => do
|
||||
let arg := match arg with
|
||||
| .some arg => arg
|
||||
| .none => .fvar fvarId
|
||||
self arg
|
||||
)
|
||||
let tailArgs ← invocation.tail.mapM self
|
||||
unsafe def unpickle (α : Type) (path : System.FilePath) : IO (α × CompactedRegion) := do
|
||||
let (x, region) ← readModuleData path
|
||||
pure (unsafeCast x, region)
|
||||
|
||||
let sites := " ".intercalate sites.toList
|
||||
let result := if tailArgs.isEmpty then
|
||||
s!"(:subst {callee} {sites})"
|
||||
else
|
||||
let tailArgs := " ".intercalate tailArgs.toList
|
||||
s!"((:subst {callee} {sites}) {tailArgs})"
|
||||
return .some result
|
||||
/-- Load an object from disk and run some continuation on it, freeing memory afterwards. -/
|
||||
unsafe def withUnpickle [Monad m] [MonadLiftT IO m] {α β : Type}
|
||||
(path : System.FilePath) (f : α → m β) : m β := do
|
||||
let (x, region) ← unpickle α path
|
||||
let r ← f x
|
||||
region.free
|
||||
pure r
|
||||
|
||||
self (e: Expr): MetaM String := do
|
||||
if let .some result ← delayedMVarToSexp e then
|
||||
return result
|
||||
match e with
|
||||
| .bvar deBruijnIndex =>
|
||||
-- This is very common so the index alone is shown. Literals are handled below.
|
||||
-- The raw de Bruijn index should never appear in an unbound setting. In
|
||||
-- Lean these are handled using a `#` prefix.
|
||||
pure s!"{deBruijnIndex}"
|
||||
| .fvar fvarId =>
|
||||
let name := ofName fvarId.name
|
||||
pure s!"(:fv {name})"
|
||||
| .mvar mvarId => do
|
||||
let pref := if ← mvarId.isDelayedAssigned then "mvd" else "mv"
|
||||
let name := ofName mvarId.name
|
||||
pure s!"(:{pref} {name})"
|
||||
| .sort level =>
|
||||
let level := serializeSortLevel level sanitize
|
||||
pure s!"(:sort {level})"
|
||||
| .const declName _ =>
|
||||
-- The universe level of the const expression is elided since it should be
|
||||
-- inferrable from surrounding expression
|
||||
pure s!"(:c {declName})"
|
||||
| .app _ _ => do
|
||||
let fn' ← self e.getAppFn
|
||||
let args := (← e.getAppArgs.mapM self) |>.toList
|
||||
let args := " ".intercalate args
|
||||
pure s!"({fn'} {args})"
|
||||
| .lam binderName binderType body binderInfo => do
|
||||
let binderName' := ofName binderName
|
||||
let binderType' ← self binderType
|
||||
let body' ← self body
|
||||
let binderInfo' := binderInfoSexp binderInfo
|
||||
pure s!"(:lambda {binderName'} {binderType'} {body'}{binderInfo'})"
|
||||
| .forallE binderName binderType body binderInfo => do
|
||||
let binderName' := ofName binderName
|
||||
let binderType' ← self binderType
|
||||
let body' ← self body
|
||||
let binderInfo' := binderInfoSexp binderInfo
|
||||
pure s!"(:forall {binderName'} {binderType'} {body'}{binderInfo'})"
|
||||
| .letE name type value body _ => do
|
||||
-- Dependent boolean flag diacarded
|
||||
let name' := serializeName name
|
||||
let type' ← self type
|
||||
let value' ← self value
|
||||
let body' ← self body
|
||||
pure s!"(:let {name'} {type'} {value'} {body'})"
|
||||
| .lit v =>
|
||||
-- To not burden the downstream parser who needs to handle this, the literal
|
||||
-- is wrapped in a :lit sexp.
|
||||
let v' := match v with
|
||||
| .natVal val => toString val
|
||||
| .strVal val => s!"\"{val}\""
|
||||
pure s!"(:lit {v'})"
|
||||
| .mdata _ inner =>
|
||||
-- NOTE: Equivalent to expr itself, but mdata influences the prettyprinter
|
||||
-- It may become necessary to incorporate the metadata.
|
||||
self inner
|
||||
| .proj _ _ _ => do
|
||||
let env ← getEnv
|
||||
let projApp := exprProjToApp env e
|
||||
let autos := String.intercalate " " (List.replicate projApp.numParams "_")
|
||||
let inner ← self projApp.inner
|
||||
pure s!"((:c {projApp.projector}) {autos} {inner})"
|
||||
-- Elides all unhygenic names
|
||||
binderInfoSexp : Lean.BinderInfo → String
|
||||
| .default => ""
|
||||
| .implicit => " :implicit"
|
||||
| .strictImplicit => " :strictImplicit"
|
||||
| .instImplicit => " :instImplicit"
|
||||
ofName (name: Name) := serializeName name sanitize
|
||||
/--
|
||||
Pickle an `Environment` to disk.
|
||||
|
||||
def serializeExpression (options: @&Protocol.Options) (e: Expr): MetaM Protocol.Expression := do
|
||||
let pp?: Option String ← match options.printExprPretty with
|
||||
| true => pure $ .some $ toString $ ← Meta.ppExpr e
|
||||
| false => pure $ .none
|
||||
let sexp?: Option String ← match options.printExprAST with
|
||||
| true => pure $ .some $ ← serializeExpressionSexp e
|
||||
| false => pure $ .none
|
||||
let dependentMVars? ← match options.printDependentMVars with
|
||||
| true => pure $ .some $ (← Meta.getMVars e).map (λ mvarId => mvarId.name.toString)
|
||||
| false => pure $ .none
|
||||
return {
|
||||
pp?,
|
||||
sexp?
|
||||
dependentMVars?,
|
||||
}
|
||||
We only store:
|
||||
* the list of imports
|
||||
* the new constants from `Environment.constants`
|
||||
and when unpickling, we build a fresh `Environment` from the imports,
|
||||
and then add the new constants.
|
||||
-/
|
||||
@[export pantograph_env_pickle_m]
|
||||
def env_pickle (env : Environment) (path : System.FilePath) : IO Unit :=
|
||||
Pantograph.pickle path (env.header.imports, env.constants.map₂)
|
||||
|
||||
/--
|
||||
Unpickle an `Environment` from disk.
|
||||
|
||||
/-- Adapted from ppGoal -/
|
||||
def serializeGoal (options: @&Protocol.Options) (goal: MVarId) (mvarDecl: MetavarDecl) (parentDecl?: Option MetavarDecl := .none)
|
||||
: MetaM Protocol.Goal := do
|
||||
-- Options for printing; See Meta.ppGoal for details
|
||||
let showLetValues := true
|
||||
let ppAuxDecls := options.printAuxDecls
|
||||
let ppImplDetailHyps := options.printImplementationDetailHyps
|
||||
let lctx := mvarDecl.lctx
|
||||
let lctx := lctx.sanitizeNames.run' { options := (← getOptions) }
|
||||
Meta.withLCtx lctx mvarDecl.localInstances do
|
||||
let ppVarNameOnly (localDecl: LocalDecl): MetaM Protocol.Variable := do
|
||||
match localDecl with
|
||||
| .cdecl _ fvarId userName _ _ _ =>
|
||||
return {
|
||||
name := ofName fvarId.name,
|
||||
userName:= ofName userName.simpMacroScopes,
|
||||
isInaccessible := userName.isInaccessibleUserName
|
||||
}
|
||||
| .ldecl _ fvarId userName _ _ _ _ => do
|
||||
return {
|
||||
name := ofName fvarId.name,
|
||||
userName := toString userName.simpMacroScopes,
|
||||
isInaccessible := userName.isInaccessibleUserName
|
||||
}
|
||||
let ppVar (localDecl : LocalDecl) : MetaM Protocol.Variable := do
|
||||
match localDecl with
|
||||
| .cdecl _ fvarId userName type _ _ =>
|
||||
let userName := userName.simpMacroScopes
|
||||
let type ← instantiate type
|
||||
return {
|
||||
name := ofName fvarId.name,
|
||||
userName:= ofName userName,
|
||||
isInaccessible := userName.isInaccessibleUserName
|
||||
type? := .some (← serializeExpression options type)
|
||||
}
|
||||
| .ldecl _ fvarId userName type val _ _ => do
|
||||
let userName := userName.simpMacroScopes
|
||||
let type ← instantiate type
|
||||
let value? ← if showLetValues then
|
||||
let val ← instantiate val
|
||||
pure $ .some (← serializeExpression options val)
|
||||
else
|
||||
pure $ .none
|
||||
return {
|
||||
name := ofName fvarId.name,
|
||||
userName:= ofName userName,
|
||||
isInaccessible := userName.isInaccessibleUserName
|
||||
type? := .some (← serializeExpression options type)
|
||||
value? := value?
|
||||
}
|
||||
let vars ← lctx.foldlM (init := []) fun acc (localDecl : LocalDecl) => do
|
||||
let skip := !ppAuxDecls && localDecl.isAuxDecl ||
|
||||
!ppImplDetailHyps && localDecl.isImplementationDetail
|
||||
if skip then
|
||||
return acc
|
||||
else
|
||||
let nameOnly := options.noRepeat && (parentDecl?.map
|
||||
(λ decl => decl.lctx.find? localDecl.fvarId |>.isSome) |>.getD false)
|
||||
let var ← match nameOnly with
|
||||
| true => ppVarNameOnly localDecl
|
||||
| false => ppVar localDecl
|
||||
return var::acc
|
||||
return {
|
||||
name := ofName goal.name,
|
||||
userName? := if mvarDecl.userName == .anonymous then .none else .some (ofName mvarDecl.userName),
|
||||
isConversion := isLHSGoal? mvarDecl.type |>.isSome,
|
||||
target := (← serializeExpression options (← instantiate mvarDecl.type)),
|
||||
vars := vars.reverse.toArray
|
||||
}
|
||||
where
|
||||
instantiate := instantiateAll
|
||||
ofName (n: Name) := serializeName n (sanitize := false)
|
||||
|
||||
protected def GoalState.serializeGoals
|
||||
(state: GoalState)
|
||||
(parent: Option GoalState := .none)
|
||||
(options: @&Protocol.Options := {}):
|
||||
MetaM (Array Protocol.Goal):= do
|
||||
state.restoreMetaM
|
||||
let goals := state.goals.toArray
|
||||
let parentDecl? := parent.bind (λ parentState => parentState.mctx.findDecl? state.parentMVar?.get!)
|
||||
goals.mapM fun goal => do
|
||||
match state.mctx.findDecl? goal with
|
||||
| .some mvarDecl =>
|
||||
let serializedGoal ← serializeGoal options goal mvarDecl (parentDecl? := parentDecl?)
|
||||
pure serializedGoal
|
||||
| .none => throwError s!"Metavariable does not exist in context {goal.name}"
|
||||
|
||||
/-- Print the metavariables in a readable format -/
|
||||
@[export pantograph_goal_state_diag_m]
|
||||
protected def GoalState.diag (goalState: GoalState) (parent?: Option GoalState := .none) (options: Protocol.GoalDiag := {}): CoreM String := do
|
||||
let metaM: MetaM String := do
|
||||
goalState.restoreMetaM
|
||||
let savedState := goalState.savedState
|
||||
let goals := savedState.tactic.goals
|
||||
let mctx ← getMCtx
|
||||
let root := goalState.root
|
||||
-- Print the root
|
||||
let result: String ← match mctx.decls.find? root with
|
||||
| .some decl => printMVar ">" root decl
|
||||
| .none => pure s!">{root.name}: ??"
|
||||
let resultGoals ← goals.filter (· != root) |>.mapM (fun mvarId =>
|
||||
match mctx.decls.find? mvarId with
|
||||
| .some decl => printMVar "⊢" mvarId decl
|
||||
| .none => pure s!"⊢{mvarId.name}: ??"
|
||||
)
|
||||
let goals := goals.toSSet
|
||||
let resultOthers ← mctx.decls.toList.filter (λ (mvarId, _) =>
|
||||
!(goals.contains mvarId || mvarId == root) && options.printAll)
|
||||
|>.mapM (fun (mvarId, decl) => do
|
||||
let pref := if parentHasMVar mvarId then " " else "~"
|
||||
printMVar pref mvarId decl
|
||||
)
|
||||
pure $ result ++ "\n" ++ (resultGoals.map (· ++ "\n") |> String.join) ++ (resultOthers.map (· ++ "\n") |> String.join)
|
||||
metaM.run' {}
|
||||
where
|
||||
printMVar (pref: String) (mvarId: MVarId) (decl: MetavarDecl): MetaM String := mvarId.withContext do
|
||||
let resultFVars: List String ←
|
||||
if options.printContext then
|
||||
decl.lctx.fvarIdToDecl.toList.mapM (λ (fvarId, decl) =>
|
||||
do pure $ (← printFVar fvarId decl) ++ "\n")
|
||||
else
|
||||
pure []
|
||||
let type ← if options.instantiate
|
||||
then instantiateAll decl.type
|
||||
else pure $ decl.type
|
||||
let type_sexp ← if options.printSexp then
|
||||
let sexp ← serializeExpressionSexp type (sanitize := false)
|
||||
pure <| " " ++ sexp
|
||||
else
|
||||
pure ""
|
||||
let resultMain: String := s!"{pref}{mvarId.name}{userNameToString decl.userName}: {← Meta.ppExpr decl.type}{type_sexp}"
|
||||
let resultValue: String ←
|
||||
if options.printValue then
|
||||
if let .some value ← getExprMVarAssignment? mvarId then
|
||||
let value ← if options.instantiate
|
||||
then instantiateAll value
|
||||
else pure $ value
|
||||
pure s!"\n := {← Meta.ppExpr value}"
|
||||
else if let .some { mvarIdPending, .. } ← getDelayedMVarAssignment? mvarId then
|
||||
pure s!"\n ::= {mvarIdPending.name}"
|
||||
else
|
||||
pure ""
|
||||
else
|
||||
pure ""
|
||||
pure $ (String.join resultFVars) ++ resultMain ++ resultValue
|
||||
printFVar (fvarId: FVarId) (decl: LocalDecl): MetaM String := do
|
||||
pure s!" | {fvarId.name}{userNameToString decl.userName}: {← Meta.ppExpr decl.type}"
|
||||
userNameToString : Name → String
|
||||
| .anonymous => ""
|
||||
| other => s!"[{other}]"
|
||||
parentHasMVar (mvarId: MVarId): Bool := parent?.map (λ state => state.mctx.decls.contains mvarId) |>.getD true
|
||||
We construct a fresh `Environment` with the relevant imports,
|
||||
and then replace the new constants.
|
||||
-/
|
||||
@[export pantograph_env_unpickle_m]
|
||||
def env_unpickle (path : System.FilePath) : IO (Environment × CompactedRegion) := unsafe do
|
||||
let ((imports, map₂), region) ← Pantograph.unpickle (Array Import × PHashMap Name ConstantInfo) path
|
||||
let env ← importModules imports {} 0
|
||||
return (← env.replay (Std.HashMap.ofList map₂.toList), region)
|
||||
|
||||
end Pantograph
|
||||
|
|
|
|||
18
Repl.lean
18
Repl.lean
|
|
@ -22,8 +22,9 @@ abbrev CR α := Except Protocol.InteractionError α
|
|||
def runMetaInMainM { α } (metaM: Lean.MetaM α): MainM α :=
|
||||
metaM.run'
|
||||
def runTermElabInMainM { α } (termElabM: Lean.Elab.TermElabM α) : MainM α :=
|
||||
termElabM.run' (ctx := Condensed.elabContext) |>.run'
|
||||
termElabM.run' (ctx := defaultElabContext) |>.run'
|
||||
|
||||
/-- Main loop command of the REPL -/
|
||||
def execute (command: Protocol.Command): MainM Lean.Json := do
|
||||
let run { α β: Type } [Lean.FromJson α] [Lean.ToJson β] (comm: α → MainM (CR β)): MainM Lean.Json :=
|
||||
match Lean.fromJson? command.payload with
|
||||
|
|
@ -32,6 +33,7 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
|
|||
| .ok result => return Lean.toJson result
|
||||
| .error ierror => return Lean.toJson ierror
|
||||
| .error error => return Lean.toJson $ errorCommand s!"Unable to parse json: {error}"
|
||||
try
|
||||
match command.cmd with
|
||||
| "reset" => run reset
|
||||
| "stat" => run stat
|
||||
|
|
@ -39,6 +41,8 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
|
|||
| "env.catalog" => run env_catalog
|
||||
| "env.inspect" => run env_inspect
|
||||
| "env.add" => run env_add
|
||||
| "env.save" => run env_save
|
||||
| "env.load" => run env_load
|
||||
| "options.set" => run options_set
|
||||
| "options.print" => run options_print
|
||||
| "goal.start" => run goal_start
|
||||
|
|
@ -51,9 +55,13 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
|
|||
let error: Protocol.InteractionError :=
|
||||
errorCommand s!"Unknown command {cmd}"
|
||||
return Lean.toJson error
|
||||
catch ex => do
|
||||
let error ← ex.toMessageData.toString
|
||||
return Lean.toJson $ errorIO error
|
||||
where
|
||||
errorCommand := errorI "command"
|
||||
errorIndex := errorI "index"
|
||||
errorIO := errorI "io"
|
||||
newGoalState (goalState: GoalState) : MainM Nat := do
|
||||
let state ← get
|
||||
let stateId := state.nextId
|
||||
|
|
@ -80,6 +88,14 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
|
|||
Environment.inspect args state.options
|
||||
env_add (args: Protocol.EnvAdd): MainM (CR Protocol.EnvAddResult) := do
|
||||
Environment.addDecl args
|
||||
env_save (args: Protocol.EnvSaveLoad): MainM (CR Protocol.EnvSaveLoadResult) := do
|
||||
let env ← Lean.MonadEnv.getEnv
|
||||
env_pickle env args.path
|
||||
return .ok {}
|
||||
env_load (args: Protocol.EnvSaveLoad): MainM (CR Protocol.EnvSaveLoadResult) := do
|
||||
let (env, _) ← env_unpickle args.path
|
||||
Lean.setEnv env
|
||||
return .ok {}
|
||||
expr_echo (args: Protocol.ExprEcho): MainM (CR Protocol.ExprEchoResult) := do
|
||||
let state ← get
|
||||
exprEcho args.expr (expectedType? := args.type?) (levels := args.levels.getD #[]) (options := state.options)
|
||||
|
|
|
|||
|
|
@ -1,7 +1,6 @@
|
|||
import Pantograph.Goal
|
||||
import Pantograph.Library
|
||||
import Pantograph.Protocol
|
||||
import Pantograph.Condensed
|
||||
import Lean
|
||||
import LSpec
|
||||
|
||||
|
|
@ -90,9 +89,9 @@ def runCoreMSeq (env: Environment) (coreM: CoreM LSpec.TestSeq) (options: Array
|
|||
def runMetaMSeq (env: Environment) (metaM: MetaM LSpec.TestSeq): IO LSpec.TestSeq :=
|
||||
runCoreMSeq env metaM.run'
|
||||
def runTermElabMInMeta { α } (termElabM: Lean.Elab.TermElabM α): Lean.MetaM α :=
|
||||
termElabM.run' (ctx := Condensed.elabContext)
|
||||
termElabM.run' (ctx := defaultElabContext)
|
||||
def runTermElabMSeq (env: Environment) (termElabM: Elab.TermElabM LSpec.TestSeq): IO LSpec.TestSeq :=
|
||||
runMetaMSeq env $ termElabM.run' (ctx := Condensed.elabContext)
|
||||
runMetaMSeq env $ termElabM.run' (ctx := defaultElabContext)
|
||||
|
||||
def exprToStr (e: Expr): Lean.MetaM String := toString <$> Meta.ppExpr e
|
||||
|
||||
|
|
|
|||
|
|
@ -1,10 +1,10 @@
|
|||
import LSpec
|
||||
import Pantograph.Serial
|
||||
import Pantograph.Delate
|
||||
import Test.Common
|
||||
import Lean
|
||||
|
||||
open Lean
|
||||
namespace Pantograph.Test.Serial
|
||||
namespace Pantograph.Test.Delate
|
||||
|
||||
open Pantograph
|
||||
|
||||
|
|
@ -64,7 +64,7 @@ def test_sexp_of_elab (env: Environment): IO LSpec.TestSeq := do
|
|||
| .ok expr => pure expr
|
||||
| .error e => return elabFailure e
|
||||
return LSpec.check source ((← serializeExpressionSexp expr) = target)
|
||||
let metaM := (Elab.Term.withLevelNames levels termElabM).run' (ctx := Condensed.elabContext)
|
||||
let metaM := (Elab.Term.withLevelNames levels termElabM).run' (ctx := defaultElabContext)
|
||||
return LSpec.TestSeq.append suites (← runMetaMSeq env metaM))
|
||||
LSpec.TestSeq.done
|
||||
|
||||
|
|
@ -85,7 +85,7 @@ def test_sexp_of_expr (env: Environment): IO LSpec.TestSeq := do
|
|||
let testCaseName := target.take 10
|
||||
let test := LSpec.check testCaseName ((← serializeExpressionSexp expr) = target)
|
||||
return LSpec.TestSeq.append suites test) LSpec.TestSeq.done
|
||||
runMetaMSeq env $ termElabM.run' (ctx := Condensed.elabContext)
|
||||
runMetaMSeq env $ termElabM.run' (ctx := defaultElabContext)
|
||||
|
||||
-- Instance parsing
|
||||
def test_instance (env: Environment): IO LSpec.TestSeq :=
|
||||
|
|
@ -106,4 +106,4 @@ def suite (env: Environment): List (String × IO LSpec.TestSeq) :=
|
|||
("Instance", test_instance env),
|
||||
]
|
||||
|
||||
end Pantograph.Test.Serial
|
||||
end Pantograph.Test.Delate
|
||||
|
|
@ -1,5 +1,5 @@
|
|||
import LSpec
|
||||
import Pantograph.Serial
|
||||
import Pantograph.Delate
|
||||
import Pantograph.Environment
|
||||
import Test.Common
|
||||
import Lean
|
||||
|
|
|
|||
|
|
@ -5,7 +5,7 @@ import Test.Integration
|
|||
import Test.Library
|
||||
import Test.Metavar
|
||||
import Test.Proofs
|
||||
import Test.Serial
|
||||
import Test.Delate
|
||||
import Test.Tactic
|
||||
|
||||
-- Test running infrastructure
|
||||
|
|
@ -50,7 +50,7 @@ def main (args: List String) := do
|
|||
("Library", Library.suite env_default),
|
||||
("Metavar", Metavar.suite env_default),
|
||||
("Proofs", Proofs.suite env_default),
|
||||
("Serial", Serial.suite env_default),
|
||||
("Delate", Delate.suite env_default),
|
||||
("Tactic/Congruence", Tactic.Congruence.suite env_default),
|
||||
("Tactic/Motivated Apply", Tactic.MotivatedApply.suite env_default),
|
||||
("Tactic/No Confuse", Tactic.NoConfuse.suite env_default),
|
||||
|
|
|
|||
|
|
@ -1,6 +1,6 @@
|
|||
import LSpec
|
||||
import Pantograph.Goal
|
||||
import Pantograph.Serial
|
||||
import Pantograph.Delate
|
||||
import Test.Common
|
||||
import Lean
|
||||
|
||||
|
|
@ -66,7 +66,7 @@ def proofRunner (env: Lean.Environment) (tests: TestM Unit): IO LSpec.TestSeq :=
|
|||
let termElabM := tests.run LSpec.TestSeq.done |>.run {} -- with default options
|
||||
|
||||
let coreContext: Lean.Core.Context ← createCoreContext #[]
|
||||
let metaM := termElabM.run' (ctx := Condensed.elabContext)
|
||||
let metaM := termElabM.run' (ctx := defaultElabContext)
|
||||
let coreM := metaM.run'
|
||||
match ← (coreM.run' coreContext { env := env }).toBaseIO with
|
||||
| .error exception =>
|
||||
|
|
|
|||
|
|
@ -3,7 +3,7 @@ Tests pertaining to goals with no interdependencies
|
|||
-/
|
||||
import LSpec
|
||||
import Pantograph.Goal
|
||||
import Pantograph.Serial
|
||||
import Pantograph.Delate
|
||||
import Test.Common
|
||||
|
||||
namespace Pantograph.Test.Proofs
|
||||
|
|
@ -74,7 +74,7 @@ def proofRunner (env: Lean.Environment) (tests: TestM Unit): IO LSpec.TestSeq :=
|
|||
let termElabM := tests.run LSpec.TestSeq.done |>.run {} -- with default options
|
||||
|
||||
let coreContext: Lean.Core.Context ← createCoreContext #[]
|
||||
let metaM := termElabM.run' (ctx := Condensed.elabContext)
|
||||
let metaM := termElabM.run' (ctx := defaultElabContext)
|
||||
let coreM := metaM.run'
|
||||
match ← (coreM.run' coreContext { env := env }).toBaseIO with
|
||||
| .error exception =>
|
||||
|
|
|
|||
Loading…
Reference in New Issue