feat: Minor updates to serialization #26

Merged
aniva merged 2 commits from io/serial into dev 2023-10-30 14:47:42 -07:00
5 changed files with 18 additions and 12 deletions
Showing only changes of commit d87217c6bb - Show all commits

View File

@ -54,8 +54,9 @@ structure Variable where
value?: Option Expression := .none value?: Option Expression := .none
deriving Lean.ToJson deriving Lean.ToJson
structure Goal where structure Goal where
/-- String case id -/ name: String := ""
caseName?: Option String := .none /-- Name of the metavariable -/
userName?: Option String := .none
/-- Is the goal in conversion mode -/ /-- Is the goal in conversion mode -/
isConversion: Bool := false isConversion: Bool := false
/-- target expression type -/ /-- target expression type -/

View File

@ -168,7 +168,7 @@ def serialize_expression (options: Protocol.Options) (e: Expr): MetaM Protocol.E
} }
/-- Adapted from ppGoal -/ /-- Adapted from ppGoal -/
def serialize_goal (options: Protocol.Options) (mvarDecl: MetavarDecl) (parentDecl?: Option MetavarDecl) def serialize_goal (options: Protocol.Options) (goal: MVarId) (mvarDecl: MetavarDecl) (parentDecl?: Option MetavarDecl)
: MetaM Protocol.Goal := do : MetaM Protocol.Goal := do
-- Options for printing; See Meta.ppGoal for details -- Options for printing; See Meta.ppGoal for details
let showLetValues := true let showLetValues := true
@ -229,7 +229,8 @@ def serialize_goal (options: Protocol.Options) (mvarDecl: MetavarDecl) (parentDe
| false => ppVar localDecl | false => ppVar localDecl
return var::acc return var::acc
return { return {
caseName? := if mvarDecl.userName == .anonymous then .none else .some (of_name mvarDecl.userName), name := of_name goal.name,
userName? := if mvarDecl.userName == .anonymous then .none else .some (of_name mvarDecl.userName),
isConversion := isLHSGoal? mvarDecl.type |>.isSome, 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
@ -246,7 +247,7 @@ protected def GoalState.serializeGoals (state: GoalState) (parent: Option GoalSt
goals.mapM fun goal => do goals.mapM fun goal => do
match state.mctx.findDecl? goal with match state.mctx.findDecl? goal with
| .some mvarDecl => | .some mvarDecl =>
let serializedGoal ← serialize_goal options mvarDecl (parentDecl? := parentDecl?) let serializedGoal ← serialize_goal options goal mvarDecl (parentDecl? := parentDecl?)
pure serializedGoal pure serializedGoal
| .none => throwError s!"Metavariable does not exist in context {goal.name}" | .none => throwError s!"Metavariable does not exist in context {goal.name}"

View File

@ -7,6 +7,7 @@ namespace Protocol
def Goal.devolatilize (goal: Goal): Goal := def Goal.devolatilize (goal: Goal): Goal :=
{ {
goal with goal with
name := "",
vars := goal.vars.map removeInternalAux, vars := goal.vars.map removeInternalAux,
} }
where removeInternalAux (v: Variable): Variable := where removeInternalAux (v: Variable): Variable :=

View File

@ -84,6 +84,7 @@ def test_malformed_command : IO LSpec.TestSeq :=
] ]
def test_tactic : IO LSpec.TestSeq := def test_tactic : IO LSpec.TestSeq :=
let goal: Protocol.Goal := { let goal: Protocol.Goal := {
name := "_uniq.10",
target := { pp? := .some "∀ (q : Prop), x q → q x" }, target := { pp? := .some "∀ (q : Prop), x q → q x" },
vars := #[{ name := "_uniq.9", userName := "x", isInaccessible? := .some false, type? := .some { pp? := .some "Prop" }}], vars := #[{ name := "_uniq.9", userName := "x", isInaccessible? := .some false, type? := .some { pp? := .some "Prop" }}],
} }

View File

@ -66,9 +66,9 @@ def startProof (start: Start): TestM (Option GoalState) := do
def assertUnreachable (message: String): LSpec.TestSeq := LSpec.check message false def assertUnreachable (message: String): LSpec.TestSeq := LSpec.check message false
def buildGoal (nameType: List (String × String)) (target: String) (caseName?: Option String := .none): Protocol.Goal := def buildGoal (nameType: List (String × String)) (target: String) (userName?: Option String := .none): Protocol.Goal :=
{ {
caseName?, userName?,
target := { pp? := .some target}, target := { pp? := .some target},
vars := (nameType.map fun x => ({ vars := (nameType.map fun x => ({
userName := x.fst, userName := x.fst,
@ -293,13 +293,13 @@ def proof_or_comm: TestM Unit := do
return () return ()
where where
typeProp: Protocol.Expression := { pp? := .some "Prop" } typeProp: Protocol.Expression := { pp? := .some "Prop" }
branchGoal (caseName name: String): Protocol.Goal := { branchGoal (caseName varName: String): Protocol.Goal := {
caseName? := .some caseName, userName? := .some caseName,
target := { pp? := .some "q p" }, target := { pp? := .some "q p" },
vars := #[ vars := #[
{ userName := "p", type? := .some typeProp, isInaccessible? := .some false }, { userName := "p", type? := .some typeProp, isInaccessible? := .some false },
{ userName := "q", type? := .some typeProp, isInaccessible? := .some false }, { userName := "q", type? := .some typeProp, isInaccessible? := .some false },
{ userName := "h✝", type? := .some { pp? := .some name }, isInaccessible? := .some true } { userName := "h✝", type? := .some { pp? := .some varName }, isInaccessible? := .some true }
] ]
} }
@ -352,9 +352,11 @@ def proof_proposition_generation: TestM Unit := do
return () return ()
addTest $ LSpec.check "apply PSigma.mk" ((← state1.serializeGoals (options := ← read)).map (·.devolatilize) = addTest $ LSpec.check "apply PSigma.mk" ((← state1.serializeGoals (options := ← read)).map (·.devolatilize) =
#[ #[
buildGoal [] "?fst" (caseName? := .some "snd"), buildGoal [] "?fst" (userName? := .some "snd"),
buildGoal [] "Prop" (caseName? := .some "fst") buildGoal [] "Prop" (userName? := .some "fst")
]) ])
if let #[goal1, goal2] := ← state1.serializeGoals (options := { (← read) with printExprAST := true }) then
addTest $ LSpec.test "(1 reference)" (goal1.target.sexp? = .some s!"(:mv {goal2.name})")
addTest $ LSpec.test "(1 root)" state1.rootExpr?.isNone addTest $ LSpec.test "(1 root)" state1.rootExpr?.isNone
let state2 ← match ← state1.tryAssign (goalId := 0) (expr := "λ (x: Nat) => _") with let state2 ← match ← state1.tryAssign (goalId := 0) (expr := "λ (x: Nat) => _") with