feat: Elementarized tactics with motives, congruence, and absurdity #72

Merged
aniva merged 41 commits from goal/mapply into dev 2024-06-12 13:52:46 -07:00
2 changed files with 8 additions and 3 deletions
Showing only changes of commit 6dcff8b151 - Show all commits

View File

@ -273,6 +273,7 @@ structure GoalDiag where
-- Print all mvars
printAll: Bool := false
instantiate: Bool := true
printSexp: Bool := false
abbrev CR α := Except InteractionError α

View File

@ -311,7 +311,7 @@ protected def GoalState.diag (goalState: GoalState) (options: Protocol.GoalDiag
)
pure $ result ++ (resultGoals.map (· ++ "\n") |> String.join) ++ (resultOthers.map (· ++ "\n") |> String.join)
where
printMVar (pref: String) (mvarId: MVarId) (decl: MetavarDecl): MetaM String := do
printMVar (pref: String) (mvarId: MVarId) (decl: MetavarDecl): MetaM String := mvarId.withContext do
let resultFVars: List String ←
if options.printContext then
decl.lctx.fvarIdToDecl.toList.mapM (λ (fvarId, decl) =>
@ -321,8 +321,12 @@ protected def GoalState.diag (goalState: GoalState) (options: Protocol.GoalDiag
let type ← if options.instantiate
then instantiateAll decl.type
else pure $ decl.type
let type_sexp ← serializeExpressionSexp type (sanitize := false)
let resultMain: String := s!"{pref}{mvarId.name}{userNameToString decl.userName}: {← Meta.ppExpr decl.type} {type_sexp}"
let type_sexp ← if options.printSexp then
let sexp ← serializeExpressionSexp type (sanitize := false)
pure <| " " ++ sexp
else
pure ""
let resultMain: String := s!"{pref}{mvarId.name}{userNameToString decl.userName}: {← Meta.ppExpr decl.type}{type_sexp}"
let resultValue: String ←
if options.printValue then
if let Option.some value := (← getMCtx).eAssignment.find? mvarId then