Skip to content

Commit

Permalink
Use endpoint framework in widget
Browse files Browse the repository at this point in the history
  • Loading branch information
PatrickMassot committed Feb 20, 2024
1 parent 7d1e628 commit e49589e
Show file tree
Hide file tree
Showing 6 changed files with 262 additions and 321 deletions.
17 changes: 17 additions & 0 deletions Verbose/English/Common.lean
Original file line number Diff line number Diff line change
Expand Up @@ -21,6 +21,17 @@ def maybeAppliedToTerm : TSyntax `maybeApplied → MetaM Term
| `(maybeApplied| $e:term applied to [$args:term,*]) => `($e $args*)
| _ => pure ⟨Syntax.missing⟩ -- This should never happen

/-- Build a maybe applied syntax from a list of term.
When the list has at least two elements, the first one is a function
and the second one is its main arguments. When there is a third element, it is assumed
to be the type of a prop argument. -/
def listTermToMaybeApplied : List Term → MetaM (TSyntax `maybeApplied)
| [x] => `(maybeApplied|$x:term)
| [x, y] => `(maybeApplied|$x:term applied to $y)
| [x, y, z] => `(maybeApplied|$x:term applied to $y using that $z)
| x::y::l => `(maybeApplied|$x:term applied to $y:term using [$(.ofElems l.toArray),*])
| _ => pure ⟨Syntax.missing⟩ -- This should never happen

declare_syntax_cat newStuffEN
syntax (ppSpace colGt maybeTypedIdent)* : newStuffEN
syntax maybeTypedIdent "such that" (ppSpace colGt maybeTypedIdent)* : newStuffEN
Expand All @@ -31,6 +42,12 @@ def newStuffENToArray : TSyntax `newStuffEN → Array MaybeTypedIdent
#[toMaybeTypedIdent x] ++ (Array.map toMaybeTypedIdent news)
| _ => #[]

def listMaybeTypedIdentToNewStuffSuchThatEN : List MaybeTypedIdent → MetaM (TSyntax `newStuffEN)
| [x] => do `(newStuffEN| $(← x.stx):maybeTypedIdent)
| [x, y] => do `(newStuffEN| $(← x.stx):maybeTypedIdent such that $(← y.stx'))
| [x, y, z] => do `(newStuffEN| $(← x.stx):maybeTypedIdent such that $(← y.stx) $(← z.stx))
| _ => pure default

declare_syntax_cat newFacts
syntax colGt namedType : newFacts
syntax colGt namedType " and " colGt namedType : newFacts
Expand Down
186 changes: 24 additions & 162 deletions Verbose/English/Widget.lean
Original file line number Diff line number Diff line change
Expand Up @@ -6,168 +6,30 @@ open Lean Meta Server

open ProofWidgets

def mkMaybeApp (selectedForallME : MyExpr) (selectedForallIdent : Ident) (data : Expr) :
MetaM (TSyntax `maybeApplied) := do
let dataS ← PrettyPrinter.delab data
match selectedForallME with
| .forall_simple e _v _t prop => do
match prop with
| .impl ..=> do
let leS ← PrettyPrinter.delab (e.bindingBody!.bindingDomain!.instantiate1 data)
`(maybeApplied|$selectedForallIdent:term applied to $dataS:term using that $leS)
| _ => `(maybeApplied|$selectedForallIdent:term applied to $dataS:term)
| .forall_rel _ _ _ rel rhs _ => do
let relS ← mkRelStx' data rel rhs
`(maybeApplied|$selectedForallIdent:term applied to $dataS:term using that $relS)
| _ => unreachable!

def mkNewStuff (selectedForallME : MyExpr) (selectedForallType : Expr) (data : Expr) (goal : MVarId)
(newsIdent : Ident) : MetaM (Expr × TSyntax `newStuffEN) := do
let obtained := match selectedForallME with
| .forall_simple _ _ _ prop =>
match prop with
| .impl .. => selectedForallType.bindingBody!.bindingBody!.instantiate1 data
| _ => selectedForallType.bindingBody!.instantiate1 data
| .forall_rel _ _ _ _ _ _ => selectedForallType.bindingBody!.bindingBody!.instantiate1 data
| _ => unreachable!

let newS ← parse obtained fun obtainedME ↦ do
match obtainedME with
| .exist_simple _e v _t propo => do
let vN ← goal.getUnusedUserName v
let vS := mkIdent vN
let hS := mkIdent (← goal.getUnusedUserName ("h"++ toString vN : String))
withRenamedFVar v vN do
let obtainedS ← PrettyPrinter.delab (propo.toExpr.instantiate1 data)
`(newStuffEN|$vS:ident such that $hS:ident : $obtainedS:term)
| .exist_rel _e v _t rel rel_rhs propo => do
let vN ← goal.getUnusedUserName v
let vS := mkIdent vN
let relI := mkIdent s!"{v}{symb_to_hyp rel rel_rhs}"
let relS ← mkRelStx vN rel rel_rhs
let hS := mkIdent (← goal.getUnusedUserName ("h"++ toString vN : String))
withRenamedFVar v vN do
let obtainedS ← PrettyPrinter.delab (propo.toExpr.instantiate1 data)
`(newStuffEN|$vS:ident such that ($relI : $relS) ($hS:ident : $obtainedS:term))
| _ => do
let obtainedS ← PrettyPrinter.delab (obtained.instantiate1 data)
`(newStuffEN|$newsIdent:ident : $obtainedS:term)
return (obtained, newS)

def mkUnfoldSuggestion (selected : Array SubExpr.GoalsLocation) (goal : MVarId) (debug : Bool) (curIndent : ℕ) : MetaM (Array SuggestionInfo):= do
if h : selected.size ≠ 1 then
return if debug then #[⟨"more than one selection", "", none⟩] else #[]
else
have : 0 < selected.size := by rw [not_not] at h; simp [h]
let sel := selected[0]
unless sel.mvarId.name = goal.name do return if debug then
#[⟨s!"Not the right goal: {sel.mvarId.name} vs {goal.name}", "", none⟩] else #[]
goal.withContext do
let ctx ← getLCtx
match sel.loc with
| .hyp fvarId => do
let ld := ctx.get! fvarId
unless ← ld.type.isAppFnUnfoldable do
return if debug then #[⟨"Could not expand", "", none⟩] else #[]
if let some e ← ld.type.expandHeadFun then
let hI := mkIdent ld.userName
let eS ← PrettyPrinter.delab e
let s ← toString <$> PrettyPrinter.ppTactic (← `(tactic|We reformulate $hI as $eS))
return #[⟨s, ppAndIndentNewLine curIndent s, none⟩]
else
return if debug then #[⟨"Could not expand", "", none⟩] else #[]
| .hypType fvarId pos => do
let ld := ctx.get! fvarId
unless ← ld.type.isAppFnUnfoldable do
return if debug then #[⟨"Could not expand def in a value", "", none⟩] else #[]
try
let expanded ← replaceSubexpr Lean.Expr.expandHeadFun! pos ld.type
let hI := mkIdent ld.userName
let eS ← PrettyPrinter.delab expanded
let s ← toString <$> PrettyPrinter.ppTactic (← `(tactic|We reformulate $hI as $eS))
return #[⟨s, ppAndIndentNewLine curIndent s, none⟩]
catch _ => return if debug then #[⟨"Could not expand", "", none⟩] else #[]
| .hypValue .. => return if debug then #[⟨"Cannot expand def in a value", "", none⟩] else #[]
| .target pos => do
let goalType ← goal.getType
unless ← goalType.isAppFnUnfoldable do
return if debug then #[⟨"Could not expand", "", none⟩] else #[]
try
let expanded ← replaceSubexpr Lean.Expr.expandHeadFun! pos goalType
let eS ← PrettyPrinter.delab expanded
let s ← toString <$> PrettyPrinter.ppTactic (← `(tactic|Let's prove that $eS))
return #[⟨s, ppAndIndentNewLine curIndent s, none⟩]
catch _ => return if debug then #[⟨"Could not expand", "", none⟩] else #[]


def makeSuggestionsOnlyLocal (selectionInfo : SelectionInfo) (goal : MVarId) (debug : Bool) (curIndent : ℕ) :
MetaM (Array SuggestionInfo) := do
let forallFVars ← selectionInfo.forallFVars
match forallFVars with
| #[selectedForallDecl] => do
let selectedForallType ← whnf selectedForallDecl.type
let selectedForallIdent := mkIdent selectedForallDecl.userName
-- We will try specializing the selected forall to each element of `datas`.
let datas ← selectionInfo.mkData selectedForallType.bindingDomain!
let newsIdent := mkIdent (← goal.getUnusedUserName `H)
parse selectedForallType fun selectedForallME ↦ do
let mut sugs := #[]
for data in datas do
let maybeApp ← mkMaybeApp selectedForallME selectedForallIdent data

let (obtained, newStuffEN) ← mkNewStuff selectedForallME selectedForallType data goal newsIdent
let tac ← if ← isDefEq (obtained.instantiate1 data) (← goal.getType) then
`(tactic|We conclude by $maybeApp:maybeApplied)
else
`(tactic|By $maybeApp:maybeApplied we get $newStuffEN)
sugs := sugs.push (← toString <$> PrettyPrinter.ppTactic tac)
if sugs.isEmpty then
return if debug then #[⟨s!"Bouh typStr: {← ppExpr selectedForallType.bindingDomain!}, si.dataFVars: {selectionInfo.dataFVars}, datas: {← datas.mapM ppExpr}", "", none⟩] else #[]
return sugs.map fun x ↦ ⟨x, ppAndIndentNewLine curIndent x, none⟩
| _ => return if debug then #[⟨s!"Only local decls : {forallFVars.map (fun l ↦ l.userName)}", "", none⟩] else #[]

def makeSuggestions (selectionInfo : SelectionInfo) (goal : MVarId) (selected : Array SubExpr.GoalsLocation) (curIndent : ℕ) :
MetaM (Array SuggestionInfo) :=
withoutModifyingState do
let debug := (← getOptions).getBool `verbose.suggestion_debug
if selectionInfo.onlyFullGoal then
let (s, _msg) ← gatherSuggestions (helpAtGoal goal)
return ← s.mapM fun sug ↦ do
let text ← sug.suggestion.pretty
pure ⟨toString text, ppAndIndentNewLine curIndent text, none⟩
if let some ld := selectionInfo.singleProp then
let (s, _msg) ← gatherSuggestions (helpAtHyp goal ld.userName)
return ← s.mapM fun sug ↦ do
let text ← sug.suggestion.pretty
pure ⟨toString text, ppAndIndentNewLine curIndent text, none⟩
let unfoldSuggestions ← mkUnfoldSuggestion selected goal debug curIndent
if selectionInfo.fullGoal then
parse (← goal.getType) fun goalME ↦ do
match goalME with
| .exist_simple e _ typ _ | .exist_rel e _ typ .. => do
let wits ← selectionInfo.mkData typ
let mut sugs := #[]
for wit in wits do
let witS ← PrettyPrinter.delab wit
sugs := sugs.push (← do
let newGoal ← PrettyPrinter.delab (e.getAppArgs'[1]!.bindingBody!.instantiate1 wit)
let tac ← `(tactic|Let's prove that $witS works : $newGoal)
toString <$> (PrettyPrinter.ppTactic tac))
return unfoldSuggestions ++ sugs.map fun x ↦ ⟨x, x ++ "\n ", none⟩
| _ => do
if selectionInfo.dataFVars.isEmpty && 0 < selectionInfo.propFVars.size && selectionInfo.propFVars.size ≤ 4 then
let goalS ← PrettyPrinter.delab (← goal.getType)
let propsS ← selectionInfo.propFVars.mapM fun ld ↦ PrettyPrinter.delab ld.type
let factsS ← arrayToFacts propsS
let tac ← PrettyPrinter.ppTactic (← `(tactic|Since $factsS we conclude that $goalS))
return #[⟨toString tac, toString tac, none⟩]
else
return if debug then #[⟨"fullGoal not exist", "", none⟩] else #[]
else if selectionInfo.onlyLocalDecls then
return unfoldSuggestions ++ (← makeSuggestionsOnlyLocal selectionInfo goal debug curIndent)
else
return unfoldSuggestions ++ if debug then #[⟨"bottom", "", none⟩] else #[]

endpoint (lang := en) mkReformulateHypTacStx (hyp : Ident) (new : Term) : MetaM (TSyntax `tactic) :=
`(tactic|We reformulate $hyp as $new)

endpoint (lang := en) mkShowTacStx (new : Term) : MetaM (TSyntax `tactic) :=
`(tactic|Let's prove that $new)

endpoint (lang := en) mkConcludeTacStx (args : List Term) : MetaM (TSyntax `tactic) := do
let concl ← listTermToMaybeApplied args
`(tactic|We conclude by $concl)

endpoint (lang := en) mkObtainTacStx (args : List Term) (news : List MaybeTypedIdent) :
MetaM (TSyntax `tactic) := do
let maybeApp ← listTermToMaybeApplied args
let newStuff ← listMaybeTypedIdentToNewStuffSuchThatEN news
`(tactic|By $maybeApp we get $newStuff)

endpoint (lang := en) mkUseTacStx (wit : Term) : Option Term → MetaM (TSyntax `tactic)
| some goal => `(tactic|Let's prove that $wit works : $goal)
| none => `(tactic|Let's prove that $wit works)

endpoint (lang := en) mkSinceTacStx (facts : Array Term) (concl : Term) :
MetaM (TSyntax `tactic) := do
let factsS ← arrayToFacts facts
`(tactic|Since $factsS we conclude that $concl)

@[server_rpc_method]
def suggestionsPanel.rpc := mkPanelRPC makeSuggestions
Expand Down
17 changes: 17 additions & 0 deletions Verbose/French/Common.lean
Original file line number Diff line number Diff line change
Expand Up @@ -21,6 +21,17 @@ def maybeAppliedFRToTerm : TSyntax `maybeAppliedFR → MetaM Term
| `(maybeAppliedFR| $e:term appliqué à [$args:term,*]) => `($e $args*)
| _ => pure ⟨Syntax.missing⟩ -- This should never happen

/-- Build a maybe applied syntax from a list of term.
When the list has at least two elements, the first one is a function
and the second one is its main arguments. When there is a third element, it is assumed
to be the type of a prop argument. -/
def listTermToMaybeApplied : List Term → MetaM (TSyntax `maybeAppliedFR)
| [x] => `(maybeAppliedFR|$x:term)
| [x, y] => `(maybeAppliedFR|$x:term appliqué à $y)
| [x, y, z] => `(maybeAppliedFR|$x:term appliqué à $y en utilisant que $z)
| x::y::l => `(maybeAppliedFR|$x:term appliqué à $y:term en utilisant que [$(.ofElems l.toArray),*])
| _ => pure ⟨Syntax.missing⟩ -- This should never happen

declare_syntax_cat newStuffFR
syntax (ppSpace colGt maybeTypedIdent)* : newStuffFR
syntax maybeTypedIdent "tel que" (ppSpace colGt maybeTypedIdent)* : newStuffFR
Expand All @@ -31,6 +42,12 @@ def newStuffFRToArray : TSyntax `newStuffFR → Array MaybeTypedIdent
#[toMaybeTypedIdent x] ++ (Array.map toMaybeTypedIdent news)
| _ => #[]

def listMaybeTypedIdentToNewStuffSuchThatFR : List MaybeTypedIdent → MetaM (TSyntax `newStuffFR)
| [x] => do `(newStuffFR| $(← x.stx):maybeTypedIdent)
| [x, y] => do `(newStuffFR| $(← x.stx):maybeTypedIdent tel que $(← y.stx'))
| [x, y, z] => do `(newStuffFR| $(← x.stx):maybeTypedIdent tel que $(← y.stx) $(← z.stx))
| _ => pure default

declare_syntax_cat newFactsFR
syntax colGt namedType : newFactsFR
syntax colGt namedType " et " colGt namedType : newFactsFR
Expand Down
Loading

0 comments on commit e49589e

Please sign in to comment.