diff --git a/Pantograph.lean b/Pantograph.lean index 1ac16fc..c91ebde 100644 --- a/Pantograph.lean +++ b/Pantograph.lean @@ -71,7 +71,7 @@ def execute (command: Protocol.Command): MainM Lean.Json := do Environment.addDecl args expr_echo (args: Protocol.ExprEcho): MainM (CR Protocol.ExprEchoResult) := do let state ← get - exprEcho args.expr args.type? state.options + exprEcho args.expr (expectedType? := args.type?) (levels := args.levels.getD #[]) (options := state.options) options_set (args: Protocol.OptionsSet): MainM (CR Protocol.OptionsSetResult) := do let state ← get let options := state.options @@ -94,7 +94,7 @@ def execute (command: Protocol.Command): MainM Lean.Json := do let state ← get let env ← Lean.MonadEnv.getEnv let expr?: Except _ GoalState ← runTermElabM (match args.expr, args.copyFrom with - | .some expr, .none => goalStartExpr expr + | .some expr, .none => goalStartExpr expr (args.levels.getD #[]) | .none, .some copyFrom => (match env.find? <| copyFrom.toName with | .none => return .error <| errorIndex s!"Symbol not found: {copyFrom}" diff --git a/Pantograph/Library.lean b/Pantograph/Library.lean index d3df45f..367d4d7 100644 --- a/Pantograph/Library.lean +++ b/Pantograph/Library.lean @@ -34,16 +34,16 @@ def setOptionFromString' (opts : Options) (entry : String) : ExceptT String IO O end Lean +open Lean + namespace Pantograph -def defaultTermElabMContext: Lean.Elab.Term.Context := { - autoBoundImplicit := true, - declName? := .some `_pantograph, +def defaultTermElabMContext: Elab.Term.Context := { errToSorry := false } -def runMetaM { α } (metaM: Lean.MetaM α): Lean.CoreM α := +def runMetaM { α } (metaM: MetaM α): CoreM α := metaM.run' -def runTermElabM { α } (termElabM: Lean.Elab.TermElabM α): Lean.CoreM α := +def runTermElabM { α } (termElabM: Elab.TermElabM α): CoreM α := termElabM.run' (ctx := defaultTermElabMContext) |>.run' def errorI (type desc: String): Protocol.InteractionError := { error := type, desc := desc } @@ -56,13 +56,13 @@ unsafe def initSearch (sp: String): IO Unit := do /-- Creates a Core.Context object needed to run all monads -/ @[export pantograph_create_core_context] -def createCoreContext (options: Array String): IO Lean.Core.Context := do - let options? ← options.foldlM Lean.setOptionFromString' Lean.Options.empty |>.run +def createCoreContext (options: Array String): IO Core.Context := do + let options? ← options.foldlM setOptionFromString' Options.empty |>.run let options ← match options? with | .ok options => pure options | .error e => throw $ IO.userError s!"Options cannot be parsed: {e}" return { - currNamespace := Lean.Name.str .anonymous "Aniva" + currNamespace := Name.str .anonymous "Aniva" openDecls := [], -- No 'open' directives needed fileName := "", fileMap := { source := "", positions := #[0] }, @@ -71,7 +71,7 @@ def createCoreContext (options: Array String): IO Lean.Core.Context := do /-- Creates a Core.State object needed to run all monads -/ @[export pantograph_create_core_state] -def createCoreState (imports: Array String): IO Lean.Core.State := do +def createCoreState (imports: Array String): IO Core.State := do let env ← Lean.importModules (imports := imports.map (λ str => { module := str.toName, runtimeOnly := false })) (opts := {}) @@ -83,33 +83,33 @@ def createMetaContext: IO Lean.Meta.Context := do return {} @[export pantograph_env_catalog_m] -def envCatalog: Lean.CoreM Protocol.EnvCatalogResult := +def envCatalog: CoreM Protocol.EnvCatalogResult := Environment.catalog ({}: Protocol.EnvCatalog) @[export pantograph_env_inspect_m] def envInspect (name: String) (value: Bool) (dependency: Bool) (options: @&Protocol.Options): - Lean.CoreM (Protocol.CR Protocol.EnvInspectResult) := + CoreM (Protocol.CR Protocol.EnvInspectResult) := Environment.inspect ({ name, value? := .some value, dependency?:= .some dependency }: Protocol.EnvInspect) options @[export pantograph_env_add_m] def envAdd (name: String) (type: String) (value: String) (isTheorem: Bool): - Lean.CoreM (Protocol.CR Protocol.EnvAddResult) := + CoreM (Protocol.CR Protocol.EnvAddResult) := Environment.addDecl { name, type, value, isTheorem } -def parseElabType (type: String): Lean.Elab.TermElabM (Protocol.CR Lean.Expr) := do - let env ← Lean.MonadEnv.getEnv +def parseElabType (type: String): Elab.TermElabM (Protocol.CR Expr) := do + let env ← MonadEnv.getEnv let syn ← match parseTerm env type with | .error str => return .error $ errorI "parsing" str | .ok syn => pure syn match ← elabType syn with | .error str => return .error $ errorI "elab" str - | .ok expr => return .ok (← Lean.instantiateMVars expr) + | .ok expr => return .ok (← instantiateMVars expr) /-- This must be a TermElabM since the parsed expr contains extra information -/ -def parseElabExpr (expr: String) (expectedType?: Option String := .none): Lean.Elab.TermElabM (Protocol.CR Lean.Expr) := do - let env ← Lean.MonadEnv.getEnv +def parseElabExpr (expr: String) (expectedType?: Option String := .none): Elab.TermElabM (Protocol.CR Expr) := do + let env ← MonadEnv.getEnv let expectedType? ← match ← expectedType?.mapM parseElabType with | .none => pure $ .none | .some (.ok t) => pure $ .some t @@ -119,17 +119,17 @@ def parseElabExpr (expr: String) (expectedType?: Option String := .none): Lean.E | .ok syn => pure syn match ← elabTerm syn expectedType? with | .error str => return .error $ errorI "elab" str - | .ok expr => return .ok (← Lean.instantiateMVars expr) + | .ok expr => return .ok (← instantiateMVars expr) @[export pantograph_expr_echo_m] -def exprEcho (expr: String) (expectedType?: Option String := .none) (options: @&Protocol.Options): - Lean.CoreM (Protocol.CR Protocol.ExprEchoResult) := - runTermElabM do +def exprEcho (expr: String) (expectedType?: Option String := .none) (levels: Array String := #[]) (options: @&Protocol.Options := {}): + CoreM (Protocol.CR Protocol.ExprEchoResult) := + runTermElabM $ Elab.Term.withLevelNames (levels.toList.map (·.toName)) do let expr ← match ← parseElabExpr expr expectedType? with | .error e => return .error e | .ok expr => pure expr try - let type ← unfoldAuxLemmas (← Lean.Meta.inferType expr) + let type ← unfoldAuxLemmas (← Meta.inferType expr) return .ok { type := (← serializeExpression options type), expr := (← serializeExpression options expr) @@ -138,8 +138,8 @@ def exprEcho (expr: String) (expectedType?: Option String := .none) (options: @& return .error $ errorI "typing" (← exception.toMessageData.toString) @[export pantograph_goal_start_expr_m] -def goalStartExpr (expr: String): Lean.CoreM (Protocol.CR GoalState) := - runTermElabM do +def goalStartExpr (expr: String) (levels: Array String): CoreM (Protocol.CR GoalState) := + runTermElabM $ Elab.Term.withLevelNames (levels.toList.map (·.toName)) do let expr ← match ← parseElabType expr with | .error e => return .error e | .ok expr => pure $ expr @@ -154,11 +154,11 @@ def goalContinue (target: GoalState) (branch: GoalState): Except String GoalStat target.continue branch @[export pantograph_goal_serialize_m] -def goalSerialize (state: GoalState) (options: @&Protocol.Options): Lean.CoreM (Array Protocol.Goal) := +def goalSerialize (state: GoalState) (options: @&Protocol.Options): CoreM (Array Protocol.Goal) := runMetaM <| state.serializeGoals (parent := .none) options @[export pantograph_goal_print_m] -def goalPrint (state: GoalState) (options: @&Protocol.Options): Lean.CoreM Protocol.GoalPrintResult := +def goalPrint (state: GoalState) (options: @&Protocol.Options): CoreM Protocol.GoalPrintResult := runMetaM do state.restoreMetaM return { @@ -170,38 +170,38 @@ def goalPrint (state: GoalState) (options: @&Protocol.Options): Lean.CoreM Proto serializeExpression options (← instantiateAll expr)), } @[export pantograph_goal_diag_m] -def goalDiag (state: GoalState) (diagOptions: Protocol.GoalDiag) : Lean.CoreM String := +def goalDiag (state: GoalState) (diagOptions: Protocol.GoalDiag) : CoreM String := runMetaM $ state.diag diagOptions @[export pantograph_goal_tactic_m] -def goalTactic (state: GoalState) (goalId: Nat) (tactic: String): Lean.CoreM TacticResult := +def goalTactic (state: GoalState) (goalId: Nat) (tactic: String): CoreM TacticResult := runTermElabM <| state.tryTactic goalId tactic @[export pantograph_goal_assign_m] -def goalAssign (state: GoalState) (goalId: Nat) (expr: String): Lean.CoreM TacticResult := +def goalAssign (state: GoalState) (goalId: Nat) (expr: String): CoreM TacticResult := runTermElabM <| state.tryAssign goalId expr @[export pantograph_goal_have_m] -def goalHave (state: GoalState) (goalId: Nat) (binderName: String) (type: String): Lean.CoreM TacticResult := +def goalHave (state: GoalState) (goalId: Nat) (binderName: String) (type: String): CoreM TacticResult := runTermElabM <| state.tryHave goalId binderName type @[export pantograph_goal_let_m] -def goalLet (state: GoalState) (goalId: Nat) (binderName: String) (type: String): Lean.CoreM TacticResult := +def goalLet (state: GoalState) (goalId: Nat) (binderName: String) (type: String): CoreM TacticResult := runTermElabM <| state.tryLet goalId binderName type @[export pantograph_goal_conv_m] -def goalConv (state: GoalState) (goalId: Nat): Lean.CoreM TacticResult := +def goalConv (state: GoalState) (goalId: Nat): CoreM TacticResult := runTermElabM <| state.conv goalId @[export pantograph_goal_conv_exit_m] -def goalConvExit (state: GoalState): Lean.CoreM TacticResult := +def goalConvExit (state: GoalState): CoreM TacticResult := runTermElabM <| state.convExit @[export pantograph_goal_calc_m] -def goalCalc (state: GoalState) (goalId: Nat) (pred: String): Lean.CoreM TacticResult := +def goalCalc (state: GoalState) (goalId: Nat) (pred: String): CoreM TacticResult := runTermElabM <| state.tryCalc goalId pred @[export pantograph_goal_focus] def goalFocus (state: GoalState) (goalId: Nat): Option GoalState := state.focus goalId @[export pantograph_goal_motivated_apply_m] -def goalMotivatedApply (state: GoalState) (goalId: Nat) (recursor: String): Lean.CoreM TacticResult := +def goalMotivatedApply (state: GoalState) (goalId: Nat) (recursor: String): CoreM TacticResult := runTermElabM <| state.tryMotivatedApply goalId recursor @[export pantograph_goal_no_confuse_m] -def goalNoConfuse (state: GoalState) (goalId: Nat) (eq: String): Lean.CoreM TacticResult := +def goalNoConfuse (state: GoalState) (goalId: Nat) (eq: String): CoreM TacticResult := runTermElabM <| state.tryNoConfuse goalId eq inductive TacticExecute where @@ -209,7 +209,7 @@ inductive TacticExecute where | congruenceFun | congruence @[export pantograph_goal_tactic_execute_m] -def goalTacticExecute (state: GoalState) (goalId: Nat) (tacticExecute: TacticExecute): Lean.CoreM TacticResult := +def goalTacticExecute (state: GoalState) (goalId: Nat) (tacticExecute: TacticExecute): CoreM TacticResult := runTermElabM do state.restoreElabM state.execute goalId $ match tacticExecute with diff --git a/Pantograph/Protocol.lean b/Pantograph/Protocol.lean index 271d4b7..69e28fc 100644 --- a/Pantograph/Protocol.lean +++ b/Pantograph/Protocol.lean @@ -101,6 +101,8 @@ structure StatResult where structure ExprEcho where expr: String type?: Option String + -- universe levels + levels: Option (Array String) := .none deriving Lean.FromJson structure ExprEchoResult where expr: Expression @@ -197,6 +199,8 @@ structure OptionsPrint where structure GoalStart where -- Only one of the fields below may be populated. expr: Option String -- Directly parse in an expression + -- universe levels + levels: Option (Array String) := .none copyFrom: Option String -- Copy the type from a theorem in the environment deriving Lean.FromJson structure GoalStartResult where diff --git a/Pantograph/Serial.lean b/Pantograph/Serial.lean index 5cccb4e..159b78e 100644 --- a/Pantograph/Serial.lean +++ b/Pantograph/Serial.lean @@ -1,5 +1,7 @@ /- -All serialisation functions +All serialisation functions; +This replicates the behaviour of `Scope`s in `Lean/Elab/Command.lean` without +using `Scope`s. -/ import Lean import Pantograph.Expr diff --git a/README.md b/README.md index 508d026..c136337 100644 --- a/README.md +++ b/README.md @@ -82,8 +82,8 @@ where the application of `assumption` should lead to a failure. See `Pantograph/Protocol.lean` for a description of the parameters and return values in JSON. * `reset`: Delete all cached expressions and proof trees * `stat`: Display resource usage -* `expr.echo {"expr": , "type": }`: Determine the - type of an expression and format it +* `expr.echo {"expr": , "type": , ["levels": []]}`: Determine the + type of an expression and format it. * `env.catalog`: Display a list of all safe Lean symbols in the current environment * `env.inspect {"name": , "value": }`: Show the type and package of a given symbol; If value flag is set, the value is printed or hidden. By default @@ -91,7 +91,7 @@ See `Pantograph/Protocol.lean` for a description of the parameters and return va * `options.set { key: value, ... }`: Set one or more options (not Lean options; those have to be set via command line arguments.), for options, see `Pantograph/Protocol.lean` * `options.print`: Display the current set of options -* `goal.start {["name": ], ["expr": ], ["copyFrom": ]}`: +* `goal.start {["name": ], ["expr": ], ["levels": []], ["copyFrom": ]}`: Start a new proof from a given expression or symbol * `goal.tactic {"stateId": , "goalId": , ...}`: Execute a tactic string on a given goal. The tactic is supplied as additional key-value pairs in one of the following formats: diff --git a/Test/Integration.lean b/Test/Integration.lean index 66b3637..9f7ad92 100644 --- a/Test/Integration.lean +++ b/Test/Integration.lean @@ -35,7 +35,7 @@ def subroutine_runner (steps: List (MainM LSpec.TestSeq)): IO LSpec.TestSeq := d def test_elab : IO LSpec.TestSeq := subroutine_runner [ subroutine_step "expr.echo" - [("expr", .str "λ {α : Sort (u + 1)} => List α")] + [("expr", .str "λ {α : Sort (u + 1)} => List α"), ("levels", .arr #["u"])] (Lean.toJson ({ type := { pp? := .some "{α : Type u} → Type u" }, expr := { pp? := .some "fun {α} => List α" } diff --git a/Test/Serial.lean b/Test/Serial.lean index 093dd8b..2d2b9d1 100644 --- a/Test/Serial.lean +++ b/Test/Serial.lean @@ -47,24 +47,26 @@ def test_sexp_of_symbol (env: Environment): IO LSpec.TestSeq := do return LSpec.TestSeq.append suites test) LSpec.TestSeq.done def test_sexp_of_elab (env: Environment): IO LSpec.TestSeq := do - let entries: List (String × String) := [ - ("λ x: Nat × Bool => x.1", "(:lambda x ((:c Prod) (:c Nat) (:c Bool)) ((:c Prod.fst) (:c Nat) (:c Bool) 0))"), - ("λ x: Array Nat => x.data", "(:lambda x ((:c Array) (:c Nat)) ((:c Array.data) (:c Nat) 0))"), - -- This tests `autoBoundImplicit` - ("λ {α : Sort (u + 1)} => List α", "(:lambda α (:sort (+ u 1)) ((:c List) 0) :implicit)"), - ("(2: Nat) <= (5: Nat)", "((:c LE.le) (:mv _uniq.37) (:mv _uniq.38) ((:c OfNat.ofNat) (:mv _uniq.23) (:lit 2) (:mv _uniq.24)) ((:c OfNat.ofNat) (:mv _uniq.33) (:lit 5) (:mv _uniq.34)))"), + let entries: List (String × (List Name) × String) := [ + ("λ x: Nat × Bool => x.1", [], "(:lambda x ((:c Prod) (:c Nat) (:c Bool)) ((:c Prod.fst) (:c Nat) (:c Bool) 0))"), + ("λ x: Array Nat => x.data", [], "(:lambda x ((:c Array) (:c Nat)) ((:c Array.data) (:c Nat) 0))"), + ("λ {α: Sort (u + 1)} => List α", [`u], "(:lambda α (:sort (+ u 1)) ((:c List) 0) :implicit)"), + ("λ {α} => List α", [], "(:lambda α (:sort (+ (:mv _uniq.4) 1)) ((:c List) 0) :implicit)"), + ("(2: Nat) <= (5: Nat)", [], "((:c LE.le) (:mv _uniq.18) (:mv _uniq.19) ((:c OfNat.ofNat) (:mv _uniq.4) (:lit 2) (:mv _uniq.5)) ((:c OfNat.ofNat) (:mv _uniq.14) (:lit 5) (:mv _uniq.15)))"), ] - let termElabM: Elab.TermElabM LSpec.TestSeq := entries.foldlM (λ suites (source, target) => do - let env ← MonadEnv.getEnv - let s ← match parseTerm env source with - | .ok s => pure s - | .error e => return parseFailure e - let expr ← match (← elabTerm s) with - | .ok expr => pure expr - | .error e => return elabFailure e - let test := LSpec.check source ((← serializeExpressionSexp expr) = target) - return LSpec.TestSeq.append suites test) LSpec.TestSeq.done - runMetaMSeq env $ termElabM.run' (ctx := defaultTermElabMContext) + entries.foldlM (λ suites (source, levels, target) => + let termElabM := do + let env ← MonadEnv.getEnv + let s ← match parseTerm env source with + | .ok s => pure s + | .error e => return parseFailure e + let expr ← match (← elabTerm s) with + | .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 := defaultTermElabMContext) + return LSpec.TestSeq.append suites (← runMetaMSeq env metaM)) + LSpec.TestSeq.done def test_sexp_of_expr (env: Environment): IO LSpec.TestSeq := do let entries: List (Expr × String) := [