feat: Specify type in echo #55
|
@ -71,7 +71,7 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
|
||||||
Environment.addDecl args
|
Environment.addDecl args
|
||||||
expr_echo (args: Protocol.ExprEcho): MainM (CR Protocol.ExprEchoResult) := do
|
expr_echo (args: Protocol.ExprEcho): MainM (CR Protocol.ExprEchoResult) := do
|
||||||
let state ← get
|
let state ← get
|
||||||
exprEcho args.expr state.options
|
exprEcho args.expr args.type state.options
|
||||||
options_set (args: Protocol.OptionsSet): MainM (CR Protocol.OptionsSetResult) := do
|
options_set (args: Protocol.OptionsSet): MainM (CR Protocol.OptionsSetResult) := do
|
||||||
let state ← get
|
let state ← get
|
||||||
let options := state.options
|
let options := state.options
|
||||||
|
|
|
@ -98,13 +98,13 @@ def inspect (args: Protocol.EnvInspect) (options: @&Protocol.Options): CoreM (Pr
|
||||||
def addDecl (args: Protocol.EnvAdd): CoreM (Protocol.CR Protocol.EnvAddResult) := do
|
def addDecl (args: Protocol.EnvAdd): CoreM (Protocol.CR Protocol.EnvAddResult) := do
|
||||||
let env ← Lean.MonadEnv.getEnv
|
let env ← Lean.MonadEnv.getEnv
|
||||||
let tvM: Elab.TermElabM (Except String (Expr × Expr)) := do
|
let tvM: Elab.TermElabM (Except String (Expr × Expr)) := do
|
||||||
let type ← match syntax_from_str env args.type with
|
let type ← match parseTerm env args.type with
|
||||||
| .ok syn => do
|
| .ok syn => do
|
||||||
match ← syntax_to_expr syn with
|
match ← elabTerm syn with
|
||||||
| .error e => return .error e
|
| .error e => return .error e
|
||||||
| .ok expr => pure expr
|
| .ok expr => pure expr
|
||||||
| .error e => return .error e
|
| .error e => return .error e
|
||||||
let value ← match syntax_from_str env args.value with
|
let value ← match parseTerm env args.value with
|
||||||
| .ok syn => do
|
| .ok syn => do
|
||||||
try
|
try
|
||||||
let expr ← Elab.Term.elabTerm (stx := syn) (expectedType? := .some type)
|
let expr ← Elab.Term.elabTerm (stx := syn) (expectedType? := .some type)
|
||||||
|
|
|
@ -109,21 +109,34 @@ def envAdd (name: String) (type: String) (value: String) (isTheorem: Bool):
|
||||||
Lean.CoreM (Protocol.CR Protocol.EnvAddResult) :=
|
Lean.CoreM (Protocol.CR Protocol.EnvAddResult) :=
|
||||||
Environment.addDecl { name, type, value, isTheorem }
|
Environment.addDecl { name, type, value, isTheorem }
|
||||||
|
|
||||||
/-- This must be a TermElabM since the parsed expr contains extra information -/
|
def typeParse (typeParse: String): Lean.Elab.TermElabM (Protocol.CR Lean.Expr) := do
|
||||||
def exprParse (s: String): Lean.Elab.TermElabM (Protocol.CR Lean.Expr) := do
|
|
||||||
let env ← Lean.MonadEnv.getEnv
|
let env ← Lean.MonadEnv.getEnv
|
||||||
let syn ← match syntax_from_str env s with
|
let syn ← match parseTerm env typeParse with
|
||||||
| .error str => return .error $ errorI "parsing" str
|
| .error str => return .error $ errorI "parsing" str
|
||||||
| .ok syn => pure syn
|
| .ok syn => pure syn
|
||||||
match ← syntax_to_expr syn with
|
match ← elabType syn with
|
||||||
|
| .error str => return .error $ errorI "elab" str
|
||||||
|
| .ok expr => return .ok expr
|
||||||
|
|
||||||
|
/-- This must be a TermElabM since the parsed expr contains extra information -/
|
||||||
|
def exprParse (exprStr: String) (expectedType?: Option String := .none): Lean.Elab.TermElabM (Protocol.CR Lean.Expr) := do
|
||||||
|
let env ← Lean.MonadEnv.getEnv
|
||||||
|
let expectedType? ← match ← expectedType?.mapM typeParse with
|
||||||
|
| .none => pure $ .none
|
||||||
|
| .some (.ok t) => pure $ .some t
|
||||||
|
| .some (.error e) => return .error e
|
||||||
|
let syn ← match parseTerm env exprStr with
|
||||||
|
| .error str => return .error $ errorI "parsing" str
|
||||||
|
| .ok syn => pure syn
|
||||||
|
match ← elabTerm syn expectedType? with
|
||||||
| .error str => return .error $ errorI "elab" str
|
| .error str => return .error $ errorI "elab" str
|
||||||
| .ok expr => return .ok expr
|
| .ok expr => return .ok expr
|
||||||
|
|
||||||
@[export pantograph_expr_echo_m]
|
@[export pantograph_expr_echo_m]
|
||||||
def exprEcho (expr: String) (options: @&Protocol.Options):
|
def exprEcho (expr: String) (expectedType?: Option String := .none) (options: @&Protocol.Options):
|
||||||
Lean.CoreM (Protocol.CR Protocol.ExprEchoResult) := do
|
Lean.CoreM (Protocol.CR Protocol.ExprEchoResult) := do
|
||||||
let termElabM: Lean.Elab.TermElabM _ := do
|
let termElabM: Lean.Elab.TermElabM _ := do
|
||||||
let expr ← match ← exprParse expr with
|
let expr ← match ← exprParse expr expectedType? with
|
||||||
| .error e => return .error e
|
| .error e => return .error e
|
||||||
| .ok expr => pure expr
|
| .ok expr => pure expr
|
||||||
try
|
try
|
||||||
|
|
|
@ -98,6 +98,7 @@ structure StatResult where
|
||||||
-- Return the type of an expression
|
-- Return the type of an expression
|
||||||
structure ExprEcho where
|
structure ExprEcho where
|
||||||
expr: String
|
expr: String
|
||||||
|
type: Option String
|
||||||
deriving Lean.FromJson
|
deriving Lean.FromJson
|
||||||
structure ExprEchoResult where
|
structure ExprEchoResult where
|
||||||
expr: Expression
|
expr: Expression
|
||||||
|
|
|
@ -25,23 +25,22 @@ def instantiateAll (e: Lean.Expr) : Lean.MetaM Lean.Expr := do
|
||||||
--- Input Functions ---
|
--- Input Functions ---
|
||||||
|
|
||||||
/-- Read syntax object from string -/
|
/-- Read syntax object from string -/
|
||||||
def syntax_from_str (env: Environment) (s: String): Except String Syntax :=
|
def parseTerm (env: Environment) (s: String): Except String Syntax :=
|
||||||
Parser.runParserCategory
|
Parser.runParserCategory
|
||||||
(env := env)
|
(env := env)
|
||||||
(catName := `term)
|
(catName := `term)
|
||||||
(input := s)
|
(input := s)
|
||||||
(fileName := "<stdin>")
|
(fileName := "<stdin>")
|
||||||
|
|
||||||
|
|
||||||
/-- Parse a syntax object. May generate additional metavariables! -/
|
/-- Parse a syntax object. May generate additional metavariables! -/
|
||||||
def syntax_to_expr_type (syn: Syntax): Elab.TermElabM (Except String Expr) := do
|
def elabType (syn: Syntax): Elab.TermElabM (Except String Expr) := do
|
||||||
try
|
try
|
||||||
let expr ← Elab.Term.elabType syn
|
let expr ← Elab.Term.elabType syn
|
||||||
return .ok expr
|
return .ok expr
|
||||||
catch ex => return .error (← ex.toMessageData.toString)
|
catch ex => return .error (← ex.toMessageData.toString)
|
||||||
def syntax_to_expr (syn: Syntax): Elab.TermElabM (Except String Expr) := do
|
def elabTerm (syn: Syntax) (expectedType? : Option Expr := .none): Elab.TermElabM (Except String Expr) := do
|
||||||
try
|
try
|
||||||
let expr ← Elab.Term.elabTerm (stx := syn) (expectedType? := .none)
|
let expr ← Elab.Term.elabTerm (stx := syn) expectedType?
|
||||||
return .ok expr
|
return .ok expr
|
||||||
catch ex => return .error (← ex.toMessageData.toString)
|
catch ex => return .error (← ex.toMessageData.toString)
|
||||||
|
|
||||||
|
|
|
@ -17,12 +17,12 @@ def addTest (test: LSpec.TestSeq): TestM Unit := do
|
||||||
def test_instantiate_mvar: TestM Unit := do
|
def test_instantiate_mvar: TestM Unit := do
|
||||||
let env ← Lean.MonadEnv.getEnv
|
let env ← Lean.MonadEnv.getEnv
|
||||||
let value := "@Nat.le_trans 2 2 5 (@of_eq_true (@LE.le Nat instLENat 2 2) (@eq_true (@LE.le Nat instLENat 2 2) (@Nat.le_refl 2))) (@of_eq_true (@LE.le Nat instLENat 2 5) (@eq_true_of_decide (@LE.le Nat instLENat 2 5) (@Nat.decLe 2 5) (@Eq.refl Bool Bool.true)))"
|
let value := "@Nat.le_trans 2 2 5 (@of_eq_true (@LE.le Nat instLENat 2 2) (@eq_true (@LE.le Nat instLENat 2 2) (@Nat.le_refl 2))) (@of_eq_true (@LE.le Nat instLENat 2 5) (@eq_true_of_decide (@LE.le Nat instLENat 2 5) (@Nat.decLe 2 5) (@Eq.refl Bool Bool.true)))"
|
||||||
let syn ← match syntax_from_str env value with
|
let syn ← match parseTerm env value with
|
||||||
| .ok s => pure $ s
|
| .ok s => pure $ s
|
||||||
| .error e => do
|
| .error e => do
|
||||||
addTest $ assertUnreachable e
|
addTest $ assertUnreachable e
|
||||||
return ()
|
return ()
|
||||||
let expr ← match ← syntax_to_expr syn with
|
let expr ← match ← elabTerm syn with
|
||||||
| .ok expr => pure $ expr
|
| .ok expr => pure $ expr
|
||||||
| .error e => do
|
| .error e => do
|
||||||
addTest $ assertUnreachable e
|
addTest $ assertUnreachable e
|
||||||
|
@ -36,14 +36,14 @@ def test_instantiate_mvar: TestM Unit := do
|
||||||
|
|
||||||
def startProof (expr: String): TestM (Option GoalState) := do
|
def startProof (expr: String): TestM (Option GoalState) := do
|
||||||
let env ← Lean.MonadEnv.getEnv
|
let env ← Lean.MonadEnv.getEnv
|
||||||
let syn? := syntax_from_str env expr
|
let syn? := parseTerm env expr
|
||||||
addTest $ LSpec.check s!"Parsing {expr}" (syn?.isOk)
|
addTest $ LSpec.check s!"Parsing {expr}" (syn?.isOk)
|
||||||
match syn? with
|
match syn? with
|
||||||
| .error error =>
|
| .error error =>
|
||||||
IO.println error
|
IO.println error
|
||||||
return Option.none
|
return Option.none
|
||||||
| .ok syn =>
|
| .ok syn =>
|
||||||
let expr? ← syntax_to_expr_type syn
|
let expr? ← elabType syn
|
||||||
addTest $ LSpec.check s!"Elaborating" expr?.isOk
|
addTest $ LSpec.check s!"Elaborating" expr?.isOk
|
||||||
match expr? with
|
match expr? with
|
||||||
| .error error =>
|
| .error error =>
|
||||||
|
|
|
@ -32,14 +32,14 @@ def startProof (start: Start): TestM (Option GoalState) := do
|
||||||
| .none =>
|
| .none =>
|
||||||
return Option.none
|
return Option.none
|
||||||
| .expr expr =>
|
| .expr expr =>
|
||||||
let syn? := syntax_from_str env expr
|
let syn? := parseTerm env expr
|
||||||
addTest $ LSpec.check s!"Parsing {expr}" (syn?.isOk)
|
addTest $ LSpec.check s!"Parsing {expr}" (syn?.isOk)
|
||||||
match syn? with
|
match syn? with
|
||||||
| .error error =>
|
| .error error =>
|
||||||
IO.println error
|
IO.println error
|
||||||
return Option.none
|
return Option.none
|
||||||
| .ok syn =>
|
| .ok syn =>
|
||||||
let expr? ← syntax_to_expr_type syn
|
let expr? ← elabType syn
|
||||||
addTest $ LSpec.check s!"Elaborating" expr?.isOk
|
addTest $ LSpec.check s!"Elaborating" expr?.isOk
|
||||||
match expr? with
|
match expr? with
|
||||||
| .error error =>
|
| .error error =>
|
||||||
|
|
|
@ -55,8 +55,8 @@ def test_sexp_of_expr (env: Environment): IO LSpec.TestSeq := do
|
||||||
]
|
]
|
||||||
let termElabM: Elab.TermElabM LSpec.TestSeq := entries.foldlM (λ suites (source, target) => do
|
let termElabM: Elab.TermElabM LSpec.TestSeq := entries.foldlM (λ suites (source, target) => do
|
||||||
let env ← MonadEnv.getEnv
|
let env ← MonadEnv.getEnv
|
||||||
let s := syntax_from_str env source |>.toOption |>.get!
|
let s := parseTerm env source |>.toOption |>.get!
|
||||||
let expr := (← syntax_to_expr s) |>.toOption |>.get!
|
let expr := (← elabTerm s) |>.toOption |>.get!
|
||||||
let test := LSpec.check source ((← serialize_expression_ast expr) = target)
|
let test := LSpec.check source ((← serialize_expression_ast expr) = target)
|
||||||
return LSpec.TestSeq.append suites test) LSpec.TestSeq.done
|
return LSpec.TestSeq.append suites test) LSpec.TestSeq.done
|
||||||
let metaM := termElabM.run' (ctx := defaultTermElabMContext)
|
let metaM := termElabM.run' (ctx := defaultTermElabMContext)
|
||||||
|
@ -67,8 +67,8 @@ def test_instance (env: Environment): IO LSpec.TestSeq := do
|
||||||
let metaM: MetaM LSpec.TestSeq := do
|
let metaM: MetaM LSpec.TestSeq := do
|
||||||
let env ← MonadEnv.getEnv
|
let env ← MonadEnv.getEnv
|
||||||
let source := "λ x y: Nat => HAdd.hAdd Nat Nat Nat (instHAdd Nat instAddNat) x y"
|
let source := "λ x y: Nat => HAdd.hAdd Nat Nat Nat (instHAdd Nat instAddNat) x y"
|
||||||
let s := syntax_from_str env source |>.toOption |>.get!
|
let s := parseTerm env source |>.toOption |>.get!
|
||||||
let _expr := (← runTermElabMInMeta <| syntax_to_expr s) |>.toOption |>.get!
|
let _expr := (← runTermElabMInMeta <| elabTerm s) |>.toOption |>.get!
|
||||||
return LSpec.TestSeq.done
|
return LSpec.TestSeq.done
|
||||||
runMetaMSeq env metaM
|
runMetaMSeq env metaM
|
||||||
|
|
||||||
|
|
Loading…
Reference in New Issue