From 8c93d30ab76763f2c2a9011d5f77436bcd10144d Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Sun, 15 Oct 2023 12:31:22 -0700 Subject: [PATCH] Rename tactic to goal and restructure --- Makefile | 7 +++++-- Pantograph.lean | 2 +- Pantograph/{Tactic.lean => Goal.lean} | 11 ++++++++--- Pantograph/Serial.lean | 10 +--------- Test/Holes.lean | 2 +- Test/Proofs.lean | 8 ++++---- 6 files changed, 20 insertions(+), 20 deletions(-) rename Pantograph/{Tactic.lean => Goal.lean} (87%) diff --git a/Makefile b/Makefile index edee774..39350b6 100644 --- a/Makefile +++ b/Makefile @@ -6,7 +6,7 @@ TEST_EXE := build/bin/test TEST_SOURCE := $(wildcard Test/*.lean) $(LIB) $(EXE): $(SOURCE) - lake build + lake build pantograph $(TEST_EXE): $(LIB) $(TEST_SOURCE) lake build test @@ -14,4 +14,7 @@ $(TEST_EXE): $(LIB) $(TEST_SOURCE) test: $(TEST_EXE) lake env $(TEST_EXE) -.PHONY: test +clean: + lake clean + +.PHONY: test clean diff --git a/Pantograph.lean b/Pantograph.lean index 3e53859..c5d56a1 100644 --- a/Pantograph.lean +++ b/Pantograph.lean @@ -1,7 +1,7 @@ import Pantograph.Commands import Pantograph.Serial import Pantograph.Symbols -import Pantograph.Tactic +import Pantograph.Goal import Pantograph.SemihashMap namespace Pantograph diff --git a/Pantograph/Tactic.lean b/Pantograph/Goal.lean similarity index 87% rename from Pantograph/Tactic.lean rename to Pantograph/Goal.lean index a736064..ea81c36 100644 --- a/Pantograph/Tactic.lean +++ b/Pantograph/Goal.lean @@ -31,12 +31,15 @@ structure GoalState where abbrev M := Elab.TermElabM 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 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 savedState ← savedStateMonad { elaborator := .anonymous } |>.run' { goals := [goal.mvarId!]} return { - savedState := savedState, + savedState, 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 return .error errors 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 => return .error #[← exception.toMessageData.toString] match Parser.runParserCategory diff --git a/Pantograph/Serial.lean b/Pantograph/Serial.lean index 924c77b..27251b6 100644 --- a/Pantograph/Serial.lean +++ b/Pantograph/Serial.lean @@ -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 try 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 catch ex => return .error (← ex.toMessageData.toString) def syntax_to_expr (syn: Syntax): Elab.TermElabM (Except String Expr) := do try 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 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 | Name.anonymous => .none | name => .some <| toString name, - isConversion := "| " == (Meta.getGoalPrefix mvarDecl) + isConversion := isLHSGoal? mvarDecl.type |>.isSome, target := (← serialize_expression options (← instantiateMVars mvarDecl.type)), vars := vars.reverse.toArray } diff --git a/Test/Holes.lean b/Test/Holes.lean index 8935ea9..64f2e2c 100644 --- a/Test/Holes.lean +++ b/Test/Holes.lean @@ -1,5 +1,5 @@ import LSpec -import Pantograph.Tactic +import Pantograph.Goal import Pantograph.Serial namespace Pantograph.Test.Holes diff --git a/Test/Proofs.lean b/Test/Proofs.lean index c9daf84..3aaea0f 100644 --- a/Test/Proofs.lean +++ b/Test/Proofs.lean @@ -1,5 +1,5 @@ import LSpec -import Pantograph.Tactic +import Pantograph.Goal import Pantograph.Serial namespace Pantograph.Test.Proofs @@ -39,7 +39,7 @@ def start_proof (start: Start): TestM (Option GoalState) := do IO.println error return Option.none | .ok syn => - let expr? ← syntax_to_expr syn + let expr? ← syntax_to_expr_type syn add_test $ LSpec.check s!"Elaborating" expr?.isOk match expr? with | .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 coreContext: Lean.Core.Context := { - currNamespace := str_to_name "Aniva", + currNamespace := Name.append .anonymous "Aniva", openDecls := [], -- No 'open' directives needed fileName := "", 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 -/ def suite: IO LSpec.TestSeq := do 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 := {}) (trustLevel := 1) let tests := [