Enable handling of m-Coupled goals #20

Merged
aniva merged 11 commits from goal/dependency into dev 2023-10-27 19:30:21 -07:00
6 changed files with 20 additions and 20 deletions
Showing only changes of commit 8c93d30ab7 - Show all commits

View File

@ -6,7 +6,7 @@ TEST_EXE := build/bin/test
TEST_SOURCE := $(wildcard Test/*.lean) TEST_SOURCE := $(wildcard Test/*.lean)
$(LIB) $(EXE): $(SOURCE) $(LIB) $(EXE): $(SOURCE)
lake build lake build pantograph
$(TEST_EXE): $(LIB) $(TEST_SOURCE) $(TEST_EXE): $(LIB) $(TEST_SOURCE)
lake build test lake build test
@ -14,4 +14,7 @@ $(TEST_EXE): $(LIB) $(TEST_SOURCE)
test: $(TEST_EXE) test: $(TEST_EXE)
lake env $(TEST_EXE) lake env $(TEST_EXE)
.PHONY: test clean:
lake clean
.PHONY: test clean

View File

@ -1,7 +1,7 @@
import Pantograph.Commands import Pantograph.Commands
import Pantograph.Serial import Pantograph.Serial
import Pantograph.Symbols import Pantograph.Symbols
import Pantograph.Tactic import Pantograph.Goal
import Pantograph.SemihashMap import Pantograph.SemihashMap
namespace Pantograph namespace Pantograph

View File

@ -31,12 +31,15 @@ structure GoalState where
abbrev M := Elab.TermElabM abbrev M := Elab.TermElabM
def GoalState.create (expr: Expr): M GoalState := do def GoalState.create (expr: Expr): M GoalState := do
-- Immediately synthesise all metavariables if we need to leave the elaboration context.
-- See https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Unknown.20universe.20metavariable/near/360130070
--Elab.Term.synthesizeSyntheticMVarsNoPostponing
let expr ← instantiateMVars expr let expr ← instantiateMVars expr
let goal := (← Meta.mkFreshExprMVar expr (kind := MetavarKind.synthetic)) let goal := (← Meta.mkFreshExprMVar expr (kind := MetavarKind.synthetic) (userName := .anonymous))
let savedStateMonad: Elab.Tactic.TacticM Elab.Tactic.SavedState := MonadBacktrack.saveState let savedStateMonad: Elab.Tactic.TacticM Elab.Tactic.SavedState := MonadBacktrack.saveState
let savedState ← savedStateMonad { elaborator := .anonymous } |>.run' { goals := [goal.mvarId!]} let savedState ← savedStateMonad { elaborator := .anonymous } |>.run' { goals := [goal.mvarId!]}
return { return {
savedState := savedState, savedState,
mvarId := goal.mvarId! mvarId := goal.mvarId!
} }
@ -52,7 +55,9 @@ def execute_tactic (state: Elab.Tactic.SavedState) (goal: MVarId) (tactic: Strin
let errors ← (messages.map Message.data).mapM fun md => md.toString let errors ← (messages.map Message.data).mapM fun md => md.toString
return .error errors return .error errors
else else
return .ok (← MonadBacktrack.saveState, ← Elab.Tactic.getUnsolvedGoals) let unsolved ← Elab.Tactic.getUnsolvedGoals
-- The order of evaluation is important here
return .ok (← MonadBacktrack.saveState, unsolved)
catch exception => catch exception =>
return .error #[← exception.toMessageData.toString] return .error #[← exception.toMessageData.toString]
match Parser.runParserCategory match Parser.runParserCategory

View File

@ -28,19 +28,11 @@ def syntax_from_str (env: Environment) (s: String): Except String Syntax :=
def syntax_to_expr_type (syn: Syntax): Elab.TermElabM (Except String Expr) := do def syntax_to_expr_type (syn: Syntax): Elab.TermElabM (Except String Expr) := do
try try
let expr ← Elab.Term.elabType syn let expr ← Elab.Term.elabType syn
-- Immediately synthesise all metavariables if we need to leave the elaboration context.
-- See https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Unknown.20universe.20metavariable/near/360130070
--Elab.Term.synthesizeSyntheticMVarsNoPostponing
let expr ← instantiateMVars expr
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 syntax_to_expr (syn: Syntax): 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? := .none)
-- Immediately synthesise all metavariables if we need to leave the elaboration context.
-- See https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Unknown.20universe.20metavariable/near/360130070
--Elab.Term.synthesizeSyntheticMVarsNoPostponing
let expr ← instantiateMVars expr
return .ok expr return .ok expr
catch ex => return .error (← ex.toMessageData.toString) catch ex => return .error (← ex.toMessageData.toString)
@ -249,7 +241,7 @@ def serialize_goal (options: Commands.Options) (mvarDecl: MetavarDecl) (parentDe
caseName? := match mvarDecl.userName with caseName? := match mvarDecl.userName with
| Name.anonymous => .none | Name.anonymous => .none
| name => .some <| toString name, | name => .some <| toString name,
isConversion := "| " == (Meta.getGoalPrefix mvarDecl) isConversion := isLHSGoal? mvarDecl.type |>.isSome,
target := (← serialize_expression options (← instantiateMVars mvarDecl.type)), target := (← serialize_expression options (← instantiateMVars mvarDecl.type)),
vars := vars.reverse.toArray vars := vars.reverse.toArray
} }

View File

@ -1,5 +1,5 @@
import LSpec import LSpec
import Pantograph.Tactic import Pantograph.Goal
import Pantograph.Serial import Pantograph.Serial
namespace Pantograph.Test.Holes namespace Pantograph.Test.Holes

View File

@ -1,5 +1,5 @@
import LSpec import LSpec
import Pantograph.Tactic import Pantograph.Goal
import Pantograph.Serial import Pantograph.Serial
namespace Pantograph.Test.Proofs namespace Pantograph.Test.Proofs
@ -39,7 +39,7 @@ def start_proof (start: Start): TestM (Option GoalState) := do
IO.println error IO.println error
return Option.none return Option.none
| .ok syn => | .ok syn =>
let expr? ← syntax_to_expr syn let expr? ← syntax_to_expr_type syn
add_test $ LSpec.check s!"Elaborating" expr?.isOk add_test $ LSpec.check s!"Elaborating" expr?.isOk
match expr? with match expr? with
| .error error => | .error error =>
@ -213,7 +213,7 @@ def proof_runner (env: Lean.Environment) (tests: TestM Unit): IO LSpec.TestSeq :
let termElabM := tests.run LSpec.TestSeq.done |>.run {} -- with default options let termElabM := tests.run LSpec.TestSeq.done |>.run {} -- with default options
let coreContext: Lean.Core.Context := { let coreContext: Lean.Core.Context := {
currNamespace := str_to_name "Aniva", currNamespace := Name.append .anonymous "Aniva",
openDecls := [], -- No 'open' directives needed openDecls := [], -- No 'open' directives needed
fileName := "<Pantograph>", fileName := "<Pantograph>",
fileMap := { source := "", positions := #[0], lines := #[1] } fileMap := { source := "", positions := #[0], lines := #[1] }
@ -232,7 +232,7 @@ def proof_runner (env: Lean.Environment) (tests: TestM Unit): IO LSpec.TestSeq :
/-- Tests the most basic form of proofs whose goals do not relate to each other -/ /-- Tests the most basic form of proofs whose goals do not relate to each other -/
def suite: IO LSpec.TestSeq := do def suite: IO LSpec.TestSeq := do
let env: Lean.Environment ← Lean.importModules let env: Lean.Environment ← Lean.importModules
(imports := #["Init"].map (λ str => { module := str_to_name str, runtimeOnly := false })) (imports := #[{ module := Name.append .anonymous "Init", runtimeOnly := false}])
(opts := {}) (opts := {})
(trustLevel := 1) (trustLevel := 1)
let tests := [ let tests := [