From 1e860f937d14a87dbacfed230f1ae6095ccb7e19 Mon Sep 17 00:00:00 2001 From: svenw <26742574+SvenWille@users.noreply.github.com> Date: Tue, 24 May 2022 02:28:14 +0200 Subject: [PATCH 1/3] starting to integrate the interactive prover stuff into the devel version of MMT --- src/.bsp/sbt.json | 1 + .../runConfigurations/Plain_MMT_Shell.xml | 12 ---- ...the_path_to_your_mathhub_folder_works_.xml | 13 ---- .../kwarc/mmt/api/checking/Constraints.scala | 10 ++-- .../info/kwarc/mmt/api/checking/Solver.scala | 60 ++----------------- .../mmt/api/checking/SolverAlgorithms.scala | 8 +-- 6 files changed, 14 insertions(+), 90 deletions(-) create mode 100644 src/.bsp/sbt.json delete mode 100644 src/.idea/runConfigurations/Plain_MMT_Shell.xml delete mode 100644 src/.idea/runConfigurations/Shell_with_MathHub_test_msl__works_if_the_path_to_your_mathhub_folder_works_.xml diff --git a/src/.bsp/sbt.json b/src/.bsp/sbt.json new file mode 100644 index 000000000..0b5405006 --- /dev/null +++ b/src/.bsp/sbt.json @@ -0,0 +1 @@ +{"name":"sbt","version":"1.6.2","bspVersion":"2.0.0-M5","languages":["scala"],"argv":["/usr/lib/jvm/java-11-openjdk/bin/java","-Xms100m","-Xmx100m","-classpath","/home/johan/.local/share/JetBrains/IdeaIC2022.1/Scala/launcher/sbt-launch.jar","-Dsbt.script=/usr/bin/sbt","xsbt.boot.Boot","-bsp"]} \ No newline at end of file diff --git a/src/.idea/runConfigurations/Plain_MMT_Shell.xml b/src/.idea/runConfigurations/Plain_MMT_Shell.xml deleted file mode 100644 index dff037f91..000000000 --- a/src/.idea/runConfigurations/Plain_MMT_Shell.xml +++ /dev/null @@ -1,12 +0,0 @@ - - - - \ No newline at end of file diff --git a/src/.idea/runConfigurations/Shell_with_MathHub_test_msl__works_if_the_path_to_your_mathhub_folder_works_.xml b/src/.idea/runConfigurations/Shell_with_MathHub_test_msl__works_if_the_path_to_your_mathhub_folder_works_.xml deleted file mode 100644 index f69c9dcca..000000000 --- a/src/.idea/runConfigurations/Shell_with_MathHub_test_msl__works_if_the_path_to_your_mathhub_folder_works_.xml +++ /dev/null @@ -1,13 +0,0 @@ - - - - \ No newline at end of file diff --git a/src/mmt-api/src/main/info/kwarc/mmt/api/checking/Constraints.scala b/src/mmt-api/src/main/info/kwarc/mmt/api/checking/Constraints.scala index 4f60d6a06..c8d4392c2 100644 --- a/src/mmt-api/src/main/info/kwarc/mmt/api/checking/Constraints.scala +++ b/src/mmt-api/src/main/info/kwarc/mmt/api/checking/Constraints.scala @@ -4,7 +4,6 @@ import info.kwarc.mmt.api._ import info.kwarc.mmt.api.presentation.Presenter import objects._ -class BranchInfo(val history: History, val backtrack: Branchpoint) /** A wrapper around a Judgement to maintain meta-information while a constraint is delayed * @param incomplete pursuing this constraint is an incomplete reasoning step @@ -12,9 +11,8 @@ class BranchInfo(val history: History, val backtrack: Branchpoint) abstract class DelayedConstraint { def notTriedYet: Boolean val freeVars: scala.collection.Set[LocalName] - val branchInfo: BranchInfo - def history = branchInfo.history - def branch = branchInfo.backtrack + val history : History + /** true if a solved variable occurs free in this Constraint */ def isActivatable(solved: List[LocalName]) = notTriedYet || (solved exists {name => freeVars contains name}) /** unknown-solving equalities that are sufficient but not necessary to discharge this */ @@ -22,13 +20,13 @@ abstract class DelayedConstraint { } /** A wrapper around a Judgement to maintain meta-information while a constraint is delayed */ -class DelayedJudgement(val constraint: Judgement, val branchInfo: BranchInfo, val suffices: Option[List[Equality]] = None, val notTriedYet: Boolean = false) extends DelayedConstraint { +class DelayedJudgement(val constraint: Judgement, val history : History , val suffices: Option[List[Equality]] = None, val notTriedYet: Boolean = false) extends DelayedConstraint { val freeVars = constraint.freeVars override def toString = constraint.toString } /** A wrapper around a continuation function to be delayed until a certain type inference succeeds */ -class DelayedInference(val stack: Stack, val branchInfo: BranchInfo, val tm: Term, val cont: Term => Boolean) extends DelayedConstraint { +class DelayedInference(val stack: Stack, val history : History, val tm: Term, val cont: Term => Boolean) extends DelayedConstraint { def notTriedYet = false def suffices = None val freeVars = { diff --git a/src/mmt-api/src/main/info/kwarc/mmt/api/checking/Solver.scala b/src/mmt-api/src/main/info/kwarc/mmt/api/checking/Solver.scala index 8c12ffc47..e185c5ea3 100644 --- a/src/mmt-api/src/main/info/kwarc/mmt/api/checking/Solver.scala +++ b/src/mmt-api/src/main/info/kwarc/mmt/api/checking/Solver.scala @@ -196,55 +196,7 @@ class Solver(val controller: Controller, val checkingUnit: CheckingUnit, val rul } } - /* first attempt at full backtracking; the code below is already partially used but has no effect yet - * - branchpoints build the tree and save the current state - * - backtracking restores current state - * - cached inferred types store the branchpoint, results are only valid if on branch - * - * - new solutions are still collected in the state but not used anymore (minor de-optimization) to make constraints stateless - * - * problems - * - how to avoid reproving constraints that are unaffected by backtracking? - * - how to backtrack when an error stems from a delayed constraint and the call to backtrackable has already terminated? - */ - private var currentBranch: Branchpoint = makeBranchpoint(None) - def getCurrentBranch = currentBranch - def setCurrentBranch(bp: Branchpoint) { - currentBranch = bp - } - /** restore the state from immediately before bp was created */ - private def backtrack(bp: Branchpoint) { - // restore constraints - _delayed = bp.delayed - // remove new dependencies - _dependencies = _dependencies.drop(_dependencies.length - bp.depLength) - // restore old solution - _solution = bp.solution - // no need to restore errors - any error should result in backtracking when !currentBranch.isRoot - } - private def makeBranchpoint(parent: Option[Branchpoint] = Some(currentBranch)) = { - new Branchpoint(parent, delayed, dependencies.length, solution) - } - class Backtrack extends Throwable - /** set a backtracking point and run code - * @return result of code or None if error occurred - * - * even if this succeeds, new constraints may have been added that will fail in the future - */ - def backtrackable[A](code: => A): Option[A] = { - val bp = makeBranchpoint() - currentBranch = bp - try { - Some(code) - } catch { - case b: Backtrack => - backtrack(bp) - None - } finally { - // even if we do not backtrack, we must update the current branch - currentBranch = currentBranch.parent.get // is defined because it was set above - } - } + } import state._ @@ -763,8 +715,8 @@ class Solver(val controller: Controller, val checkingUnit: CheckingUnit, val rul */ def apply(j: Judgement): Boolean = { val h = new History(Nil) - val bi = new BranchInfo(h, getCurrentBranch) - addConstraint(new DelayedJudgement(j, bi, notTriedYet = true))(h) + + addConstraint(new DelayedJudgement(j, h , notTriedYet = true))(h) activateRepeatedly if (errors.nonEmpty) { // definitely disproved @@ -794,8 +746,7 @@ class Solver(val controller: Controller, val checkingUnit: CheckingUnit, val rul } else { log("delaying: " + j.present) history += "(delayed)" - val bi = new BranchInfo(history, getCurrentBranch) - val dc = new DelayedJudgement(j, bi, suffices) + val dc = new DelayedJudgement(j, history, suffices) addConstraint(dc) } true @@ -812,7 +763,6 @@ class Solver(val controller: Controller, val checkingUnit: CheckingUnit, val rul // activates a constraint def activate(dc: DelayedConstraint) = { removeConstraint(dc) - setCurrentBranch(dc.branch) dc match { case dj: DelayedJudgement => val j = dj.constraint @@ -1047,7 +997,7 @@ object Solver { } /** used by [[Solver]] to store inferred types with terms */ -object InferredType extends TermProperty[(Branchpoint,Term)](Solver.propertyURI / "inferred") +object InferredType extends TermProperty[Term](Solver.propertyURI / "inferred") /** used by [[Solver]] to mark a term as head-normal: no simplification rule can change the head symbol */ class Stability(id: Int) extends BooleanTermProperty(Solver.propertyURI / "stability" / id.toString) diff --git a/src/mmt-api/src/main/info/kwarc/mmt/api/checking/SolverAlgorithms.scala b/src/mmt-api/src/main/info/kwarc/mmt/api/checking/SolverAlgorithms.scala index 48c43e444..6d9a70925 100644 --- a/src/mmt-api/src/main/info/kwarc/mmt/api/checking/SolverAlgorithms.scala +++ b/src/mmt-api/src/main/info/kwarc/mmt/api/checking/SolverAlgorithms.scala @@ -533,7 +533,7 @@ trait SolverAlgorithms {self: Solver => history += "inferring type of " + presentObj(tm) // return previously inferred type, if any (previously unsolved variables are substituted) InferredType.get(tm) match { - case Some((bp,tmI)) if getCurrentBranch.descendsFrom(bp) => + case Some(tmI) => return Some(tmI ^^ solution.toPartialSubstitution) case _ => } @@ -635,7 +635,7 @@ trait SolverAlgorithms {self: Solver => history += "inferred: " + presentObj(tm) + " : " + res.map(presentObj).getOrElse("failed") //remember inferred type if (!isDryRun) { - res foreach {r => InferredType.put(tm, (getCurrentBranch,r))} + res foreach {r => InferredType.put(tm, r)} } res map {r => substituteSolution(r)} // this used to call simplify (without defnition expansion) } @@ -651,8 +651,8 @@ trait SolverAlgorithms {self: Solver => case Some(tp) => cont(tp) case None => - val bi = new BranchInfo(history + "(inference delayed)", getCurrentBranch) - addConstraint(new DelayedInference(stack, bi, tm, cont)) + + addConstraint(new DelayedInference(stack, h , tm, cont)) true } } From be916eb6987bd647a056c1e4c58e41df3ab5bfe6 Mon Sep 17 00:00:00 2001 From: svenw <26742574+SvenWille@users.noreply.github.com> Date: Tue, 24 May 2022 02:22:52 +0200 Subject: [PATCH 2/3] added the prover to MMTd --- .../proofgui/MMTProofStateDockable.scala | 292 +++++++ .../proofgui/util/GenInteractiveProof.scala | 79 ++ src/jEdit-mmt/src/resources/actions.xml | 5 + src/jEdit-mmt/src/resources/dockables.xml | 3 + src/jEdit-mmt/src/resources/mmtplugin.props | 2 + .../info/kwarc/mmt/api/checking/Solver.scala | 317 +++++--- .../mmt/api/checking/SolverAlgorithms.scala | 2 +- .../info/kwarc/mmt/api/proving/itp/Goal.scala | 87 +++ .../info/kwarc/mmt/api/proving/itp/Msg.scala | 59 ++ .../kwarc/mmt/api/proving/itp/Proof.scala | 191 +++++ .../kwarc/mmt/api/proving/itp/ProofUtil.scala | 70 ++ .../kwarc/mmt/api/proving/itp/TypedTerm.scala | 8 + .../src/info/kwarc/mmt/itp/Constants.scala | 16 - src/mmt-lf/src/info/kwarc/mmt/itp/Rules.scala | 18 - .../kwarc/mmt/lf/itp/InteractiveProof.scala | 136 ++++ .../InteractiveStructuredProof/Fixity.scala | 27 + .../InteractiveStructuredProof.scala | 10 + .../NewTactic.scala | 5 + .../StructuredProofParseRule.scala | 9 + .../StructuredProofParser.scala | 50 ++ .../kwarc/mmt/lf/itp/NewTacticParser.scala | 7 + .../kwarc/mmt/lf/itp/ProofGenerator.scala | 75 ++ .../src/info/kwarc/mmt/lf/itp/ProofUtil.scala | 546 +++++++++++++ .../src/info/kwarc/mmt/lf/itp/Tactic.scala | 53 ++ .../info/kwarc/mmt/lf/itp/TacticError.scala | 9 + .../info/kwarc/mmt/lf/itp/TacticParser.scala | 406 ++++++++++ .../info/kwarc/mmt/lf/itp/TacticRule.scala | 35 + .../Tactics/InteractiveTacticParseRule.scala | 8 + .../kwarc/mmt/lf/itp/Tactics/Tactics.scala | 736 ++++++++++++++++++ .../kwarc/mmt/lf/itp/TacticsParserA.scala | 268 +++++++ .../kwarc/mmt/lf/itp/Utils/OMLTraverser.scala | 10 + .../lf/itp/Utils/OutOfOrderApplierLF.scala | 93 +++ .../mmt/lf/itp/Utils/StandAloneChecks.scala | 31 + .../kwarc/mmt/lf/itp/Utils/TermUtil.scala | 240 ++++++ .../Utils/Unifier/MoreGeneralUnifier.scala | 23 + .../mmt/lf/itp/Utils/Unifier/Unifier.scala | 48 ++ 36 files changed, 3827 insertions(+), 147 deletions(-) create mode 100644 src/jEdit-mmt/src/info/kwarc/mmt/jedit/proofgui/MMTProofStateDockable.scala create mode 100644 src/jEdit-mmt/src/info/kwarc/mmt/jedit/proofgui/util/GenInteractiveProof.scala create mode 100644 src/mmt-api/src/main/info/kwarc/mmt/api/proving/itp/Goal.scala create mode 100644 src/mmt-api/src/main/info/kwarc/mmt/api/proving/itp/Msg.scala create mode 100644 src/mmt-api/src/main/info/kwarc/mmt/api/proving/itp/Proof.scala create mode 100644 src/mmt-api/src/main/info/kwarc/mmt/api/proving/itp/ProofUtil.scala create mode 100644 src/mmt-api/src/main/info/kwarc/mmt/api/proving/itp/TypedTerm.scala delete mode 100644 src/mmt-lf/src/info/kwarc/mmt/itp/Constants.scala delete mode 100644 src/mmt-lf/src/info/kwarc/mmt/itp/Rules.scala create mode 100644 src/mmt-lf/src/info/kwarc/mmt/lf/itp/InteractiveProof.scala create mode 100644 src/mmt-lf/src/info/kwarc/mmt/lf/itp/InteractiveStructuredProof/Fixity.scala create mode 100644 src/mmt-lf/src/info/kwarc/mmt/lf/itp/InteractiveStructuredProof/InteractiveStructuredProof.scala create mode 100644 src/mmt-lf/src/info/kwarc/mmt/lf/itp/InteractiveStructuredProof/NewTactic.scala create mode 100644 src/mmt-lf/src/info/kwarc/mmt/lf/itp/InteractiveStructuredProof/StructuredProofParseRule.scala create mode 100644 src/mmt-lf/src/info/kwarc/mmt/lf/itp/InteractiveStructuredProof/StructuredProofParser.scala create mode 100644 src/mmt-lf/src/info/kwarc/mmt/lf/itp/NewTacticParser.scala create mode 100644 src/mmt-lf/src/info/kwarc/mmt/lf/itp/ProofGenerator.scala create mode 100644 src/mmt-lf/src/info/kwarc/mmt/lf/itp/ProofUtil.scala create mode 100644 src/mmt-lf/src/info/kwarc/mmt/lf/itp/Tactic.scala create mode 100644 src/mmt-lf/src/info/kwarc/mmt/lf/itp/TacticError.scala create mode 100644 src/mmt-lf/src/info/kwarc/mmt/lf/itp/TacticParser.scala create mode 100644 src/mmt-lf/src/info/kwarc/mmt/lf/itp/TacticRule.scala create mode 100644 src/mmt-lf/src/info/kwarc/mmt/lf/itp/Tactics/InteractiveTacticParseRule.scala create mode 100644 src/mmt-lf/src/info/kwarc/mmt/lf/itp/Tactics/Tactics.scala create mode 100644 src/mmt-lf/src/info/kwarc/mmt/lf/itp/TacticsParserA.scala create mode 100644 src/mmt-lf/src/info/kwarc/mmt/lf/itp/Utils/OMLTraverser.scala create mode 100644 src/mmt-lf/src/info/kwarc/mmt/lf/itp/Utils/OutOfOrderApplierLF.scala create mode 100644 src/mmt-lf/src/info/kwarc/mmt/lf/itp/Utils/StandAloneChecks.scala create mode 100644 src/mmt-lf/src/info/kwarc/mmt/lf/itp/Utils/TermUtil.scala create mode 100644 src/mmt-lf/src/info/kwarc/mmt/lf/itp/Utils/Unifier/MoreGeneralUnifier.scala create mode 100644 src/mmt-lf/src/info/kwarc/mmt/lf/itp/Utils/Unifier/Unifier.scala diff --git a/src/jEdit-mmt/src/info/kwarc/mmt/jedit/proofgui/MMTProofStateDockable.scala b/src/jEdit-mmt/src/info/kwarc/mmt/jedit/proofgui/MMTProofStateDockable.scala new file mode 100644 index 000000000..208e8a8b3 --- /dev/null +++ b/src/jEdit-mmt/src/info/kwarc/mmt/jedit/proofgui/MMTProofStateDockable.scala @@ -0,0 +1,292 @@ +package info.kwarc.mmt.jedit.proofgui + +import info.kwarc.mmt.api.gui.Swing +import info.kwarc.mmt.api.objects.Stack +import info.kwarc.mmt.api.proving.itp.{HasError, ProofUtil, WarningMsg} +import info.kwarc.mmt.jedit.proofgui.util.GenInteractiveProof +import info.kwarc.mmt.lf.itp.{InteractiveProof, Tactic, TacticError} +import org.gjt.sp.jedit.gui.{HistoryTextArea, HistoryTextField} +import org.gjt.sp.jedit.{Abbrevs, View} + +import java.awt.event.{ActionEvent, ActionListener, KeyEvent} +import java.awt.{BorderLayout, Dimension} +import java.util +import java.util.Calendar +import javax.swing._ + +/** + * the Java-swing that is used as a containter for concret gui implementations like the proof display + * @param view the current jedit view + * @param position the position of the dockable inside of jedit (not actively used but required by jedit) + */ +class MMTProofStateDockable (view: View, position: String) extends JTabbedPane { + + + val tacticsproof = new TacticsProof(view) + tacticsproof.setDividerLocation(0.5) + tacticsproof.setResizeWeight(0.5) + addTab("Tactics Proof", tacticsproof) + + +} + +/** + * TacticsProof implements a concrete gui for the MMTproofStateDockable. + * It consists of three parts: the top display containing the proof state [[textarea0]] , + * the input bar at the bottom [[tacticsinput]] and the middle tabbed display for different kinds of outputs [[tabs]] + * @param view the current jedit view + */ +class TacticsProof(view : View) extends JSplitPane(SwingConstants.HORIZONTAL){ + + /** the concrete InteractiveProof instance used for proof management by the GUI + * + */ + var ip : Option[InteractiveProof] = None + + /** abbrevs contains all the ascii to unicode translations used for the input bar + * this is used to translate an ascii sequence into an unicode using the MMT-abbreviations (f.ex. jrA for the big + * unicode right arrow, in latex it would be \Rightarrow) + */ + val abbrevs: util.Hashtable[String, String] = Abbrevs.getModeAbbrevs.get("mmt") + + + val top = new JPanel() + val bottom = new JPanel() + /** + * tabs used in the bottom panel + */ + val tabs = new JTabbedPane() + + + + top.setLayout(new BorderLayout()) + bottom.setLayout(new BorderLayout()) + add(top) + add(bottom) + + // not writeable textarea (in the top half of the proof gui) used to display the proof state + val txtarea0= new JTextArea() + txtarea0.setLineWrap(true) + txtarea0.setPreferredSize(new Dimension(top.getWidth, top.getHeight)) + txtarea0.setEditable(false) + + // the bottom text area is used + val btmtxt = new JTextArea() + btmtxt.setLineWrap(true) + btmtxt.setPreferredSize(new Dimension(bottom.getWidth, bottom.getHeight)) + + // the bar at the very bottom where one enters the tactics + val tacticsinput = new HistoryTextField("tactics input") // new JTextField(30) + tacticsinput.setEnterAddsToHistory(true) + + + bottom.add(tacticsinput, BorderLayout.SOUTH) + + bottom.add(tabs ,BorderLayout.CENTER) + tabs.addTab("output" , btmtxt) + + val tacticsHistory = new JTextArea() + + + tabs.addTab("input" , tacticsHistory) + + val history = new HistoryTextArea("internal mmt history") + + // tabs.addTab("history" , history) + + val proofTermTxt = new JTextArea() + proofTermTxt.setLineWrap(true) + + tabs.addTab("proof term", proofTermTxt ) + + top.add(txtarea0, BorderLayout.CENTER) + + + val jtb0 = new JToolBar() + + + + val proofbtn : JButton = Swing.Button("Proof", "Proof current term") { + ip = GenInteractiveProof.genInteractiveProof(view) + if (ip.isDefined){val tmp = ip.get.pr.proofStateToString(ip.get.slvr); txtarea0.setText(tmp) ; btmtxt.setText("")} + } + + + val undobtn : JButton = Swing.Button("Undo", "Undo the last step"){if (ip.isDefined) {ip.get.undo; val tmp = ip.get.pr.proofStateToString(ip.get.slvr); txtarea0.setText(tmp) ; ip.get.stepsS.remove(ip.get.stepsS.length - 1); tacticsHistory.setText(ip.get.stepsS.mkString(";\n"))} } + val genProofTermBtn : JButton = Swing.Button("Proof Term (S)" , "Generate and display the proof term (simplified)"){ + if (ip.isDefined){ + val slvr = ip.get.slvr + proofTermTxt.setText(slvr.presentObj(ip.get.slvr.simplify(ip.get.pr.proofTerm)(Stack(ip.get.slvr.checkingUnit.context), ip.get.hist))) + // val tmp = slvr.asInstanceOf[ExtendedSolver].presentBracketed(ip.get.slvr.simplify(ip.get.pr.proofTermAlt)(Stack(ip.get.slvr.checkingUnit.context), ip.get.hist)) + } + } + val genProofTermBtnAlt : JButton = Swing.Button("Proof Term" , "Generate and display the proof term (unsimplified)"){ + if (ip.isDefined){ + val slvr = ip.get.slvr + proofTermTxt.setText(slvr.presentObj(ip.get.pr.proofTermAlt)) + // val tmp = Presenter.bracket() + } + } + + val genProofTermBtnBrack : JButton = Swing.Button("Proof Term (SB)" , "Generate and display the proof term (simplified with brackets)"){ + if (ip.isDefined){ + val slvr = ip.get.slvr + val tmp = ProofUtil.presentBracketed(ip.get.slvr.controller , ip.get.slvr.report , ip.get.slvr.simplify(ip.get.pr.proofTerm)(Stack(ip.get.slvr.checkingUnit.context), ip.get.hist)) + proofTermTxt.setText(tmp) + } + } + + val genProofTermBtnBrackAlt : JButton = Swing.Button("Proof Term (B)" , "Generate and display the proof term (unsimplified with brackets)"){ + if (ip.isDefined){ + val slvr = ip.get.slvr + // proofTermTxt.setText(slvr.presentObj(ip.get.slvr.simplify(ip.get.pr.proofTermAlt)(Stack(ip.get.slvr.checkingUnit.context), ip.get.hist))) + val tmp = ProofUtil.presentBracketed(ip.get.slvr.controller,ip.get.slvr.report, (ip.get.pr.proofTermAlt)) + proofTermTxt.setText(tmp) + } + } + + + val testrunbutton : JButton = Swing.Button("Test" , "treats this proof as a test run (less checks, no proof term generation, useful for debugging and using experimental features)"){ + if (ip.isDefined){ + ip.get.testrun = true + btmtxt.append("is testrun: " + ip.get.testrun.toString) + // proofTermTxt.setText(slvr.presentObj(ip.get.slvr.simplify(ip.get.pr.proofTermAlt)(Stack(ip.get.slvr.checkingUnit.context), ip.get.hist))) + + } + } + + val saveProofTermBtn : JButton = Swing.Button("Save Proof" , "Save the proof (this will only save the proof steps)"){} + val loadProofTermBtn : JButton = Swing.Button("Load Proof" , "Load the proof (this will only load the proof steps, if any are available)"){} + val helpBtn : JButton = Swing.Button("Displays Help" , "Show help for several topics like \"which tactics are available\""){} + val hist : JButton = Swing.Button("Print History" , "Print the internal mmt history"){ + if (ip.isDefined){ + val ipp = ip.get + history.setText(ipp.hist.toString) + } + } + jtb0.add(proofbtn) + jtb0.add(undobtn) + jtb0.add(genProofTermBtn) + jtb0.add(genProofTermBtnAlt) + jtb0.add(testrunbutton) + + + jtb0.add(genProofTermBtnBrack) + jtb0.add(genProofTermBtnBrackAlt) + + + top.add(jtb0 , BorderLayout.NORTH) + + + tacticsinput.addActionListener(new tacticsinputaction) + + + /** prints an error to the output panel (including the date) + * + * @param s the string to be printed + */ + def printError(s : String): Unit ={ + val time = Calendar.getInstance().getTime + val times = time.toString + val errorstring = times + "\n-----------------\n\n" + s + btmtxt.setText(errorstring) + } + + /** + * contains all input triggers, restricted to the input bar + */ + val imap: InputMap = tacticsinput.getInputMap(JComponent.WHEN_ANCESTOR_OF_FOCUSED_COMPONENT) + /** + * contains all actions that can be called by the input action map. This includes the unicode completion for the input bar + */ + val amap: ActionMap = tacticsinput.getActionMap + // trigger the unicode completion when the space bar is pressed + imap.put(KeyStroke.getKeyStroke(KeyEvent.VK_SPACE,0,false) , "unic") + + // add the unicode completion to the action map + amap.put("unic" , new unicodecomplete) + + /** + * class used for the unicode completion in the input bar (not the source code area) + */ + class unicodecomplete extends AbstractAction { + /** + * handler that gets called when the space bar is pressed in the input bar + * @param actionEvent ignored + */ + override def actionPerformed(actionEvent: ActionEvent): Unit = { + // get the text from the input bar + val txt = tacticsinput.getText() + // position of the caret in the input bar + val i = tacticsinput.getCaretPosition + // represents the start of the string that is to be transformed into an unicode character + var start = i + // find the start of the word by going back until the start of the input bar or a whitespace is found + while(0 < start && ! txt(start - 1).isWhitespace){ + start -= 1 + } + if (start != i){ + val sub = txt.substring(start , i) + if(abbrevs.containsKey(sub)){ + val res = abbrevs.get(sub) + val hd = txt.take(start) + val tl = txt.drop(i) + tacticsinput.setText(hd + res + tl) + val newpos = start + res.length // + (if (start != 0) -1 else 0 ) + tacticsinput.setCaretPosition(newpos) + } + } + } + } + + /** + * class called when processing input from the input bar (by pressing enter) + */ + class tacticsinputaction extends ActionListener{ + + + /** + * processes the input bar text by first parsing it and if sucessfull, executing the parsed tactic + * @param actionEvent ignored + */ + override def actionPerformed(actionEvent: ActionEvent): Unit = { + if (ip.isEmpty) return + + val tmp = tacticsinput.getText + + tacticsinput.setText("") + //get the tactics parser + val tp = ip.get.tp + val ipp = ip.get + // save the current proof state in the history + ipp.saveCurrState + + + + + val pr = try { tp.parseAll(tp.multiTacticPA, tmp)} catch { + case TacticError(s) => tp.Error(s , null) + case e => tp.Error("error while parsing: " + e.toString , null) + } + pr match { + case tp.Success(result, next) =>{ + ip.get.executeStep(result.asInstanceOf[Tactic]) match { + case HasError(s) => { + printError(s) + } + case WarningMsg(s) => {printError(s) ; ip.get.stepsS.append(tmp)} + case _ => ip.get.stepsS.append(tmp) + } + val st = ip.get.pr.proofStateToString(ip.get.slvr) + txtarea0.setText(st) + val tmp0 = ip.get.stepsS.map(_.toString).mkString(";\n") + tacticsHistory.setText(tmp0) + + } + case tp.Failure(msg,nxt) => printError(msg) ; ipp.undo + case tp.Error(msg, nxt) => printError(msg) ; ipp.undo + } + } + } + +} diff --git a/src/jEdit-mmt/src/info/kwarc/mmt/jedit/proofgui/util/GenInteractiveProof.scala b/src/jEdit-mmt/src/info/kwarc/mmt/jedit/proofgui/util/GenInteractiveProof.scala new file mode 100644 index 000000000..5956fa713 --- /dev/null +++ b/src/jEdit-mmt/src/info/kwarc/mmt/jedit/proofgui/util/GenInteractiveProof.scala @@ -0,0 +1,79 @@ +package info.kwarc.mmt.jedit.proofgui.util + +import info.kwarc.mmt.api.ComponentKey +import info.kwarc.mmt.api.frontend.Controller +import info.kwarc.mmt.api.symbols.FinalConstant +import info.kwarc.mmt.jedit.{JElemAsset, MMTPlugin} +import info.kwarc.mmt.lf.itp.{InteractiveProof, ProofGenerator} +import org.gjt.sp.jedit.textarea.JEditTextArea +import org.gjt.sp.jedit.{View, jEdit} +import sidekick.SideKickParsedData + +import javax.swing.tree.{DefaultMutableTreeNode, TreePath} + +/** + * object for creating a proof manager ([[InteractiveProof]]) + */ +object GenInteractiveProof { + + /** + * a function that searches for the `type` of a declaration + * @param arr the array representation of the source path in the tree representation the caret is currently on + * @return the `type`. None, if no type exists + */ + def findConstant(arr : Array[DefaultMutableTreeNode]): Option[DefaultMutableTreeNode] = arr match { + case Array() => None + case Array(x , xs @ _* ) =>{ + x.getUserObject match { + case y: JElemAsset => y.elem match { + case _ : FinalConstant => Some(x) + case _ => findConstant(arr.tail) + } + case _ => findConstant(arr.tail) + } + } + } + + /** generates a new proof manager ([[InteractiveProof]]). + * This will be done by looking at the mmt source interpreted as a tree of tokens. The created proof sould be the one the caret indicates. + * The path the caret is on will have a type wich in turn will be the goal for the created proof. + * + * @param v the jedit view + * @return a new [[InteractiveProof]]-instance, None if no provable object was encountered near the caret position + */ + def genInteractiveProof(v : View ): Option[InteractiveProof] ={ + // get the tree representation for the source in the textare of the current jedit view + val pd : SideKickParsedData = SideKickParsedData.getParsedData(v) + val ta : JEditTextArea = v.getTextArea + val caretpos : Int = ta.getCaretPosition + // the path from the root of the source tree to where the caret currently is + val tmp : TreePath = pd.getTreePathForPosition(caretpos) + // explicitely type the TreePath as Array[DefaultMutableTreeNode] otherwise (because scala can't figure it out on its own) + val pth : Array[DefaultMutableTreeNode] = tmp.getPath.map(x => x.asInstanceOf[DefaultMutableTreeNode]) + // find the type + val pth0 = findConstant(pth) + val (tp,mp,cp) = pth0 match { + case None => return None + case Some(v) => { + val cst = v.getUserObject.asInstanceOf[JElemAsset].elem.asInstanceOf[FinalConstant] + val tp = cst.tp.getOrElse(return None) + // get the mpath the type belongs to + val mp = cst.home.toMPath + val k : ComponentKey = ComponentKey.parse("type") + // get the componet path the type belongs to + val cp = Some(mp ? cst.name $ k) + (tp,mp,cp) + + } + } + + val mmtp : MMTPlugin = jEdit.getPlugin("info.kwarc.mmt.jedit.MMTPlugin", true).asInstanceOf[MMTPlugin] + val c : Controller = mmtp.controller + // generate a new InteractiveProof with the data gathered + ProofGenerator.setupNewProof(c , Some(mp), cp , tp) + + } + + + +} \ No newline at end of file diff --git a/src/jEdit-mmt/src/resources/actions.xml b/src/jEdit-mmt/src/resources/actions.xml index 45b87bfab..dc1f08669 100644 --- a/src/jEdit-mmt/src/resources/actions.xml +++ b/src/jEdit-mmt/src/resources/actions.xml @@ -66,4 +66,9 @@ jEdit.getPlugin("info.kwarc.mmt.jedit.MMTPlugin", true).editActions().showNormalization(view, true); + + + wm.addDockableWindow("mmt-proofdockable"); + + diff --git a/src/jEdit-mmt/src/resources/dockables.xml b/src/jEdit-mmt/src/resources/dockables.xml index e2ba3d5de..5eb8a7699 100644 --- a/src/jEdit-mmt/src/resources/dockables.xml +++ b/src/jEdit-mmt/src/resources/dockables.xml @@ -11,4 +11,7 @@ new info.kwarc.mmt.jedit.MMTGraphDockable(view, position); + + new info.kwarc.mmt.jedit.proofgui.MMTProofStateDockable(view, position); + \ No newline at end of file diff --git a/src/jEdit-mmt/src/resources/mmtplugin.props b/src/jEdit-mmt/src/resources/mmtplugin.props index 1dde00813..f40767834 100644 --- a/src/jEdit-mmt/src/resources/mmtplugin.props +++ b/src/jEdit-mmt/src/resources/mmtplugin.props @@ -37,6 +37,7 @@ mmt-insert-GS.label=Insert Module Delimiter (MD) mmt-introduce-hole.label=Introduce hole for expected type mmt-show-normalization.label=Show normalization mmt-normalize-selection.label=Normalize selection +mmt-proofdockable-show.label=Show Proof Dockable # labels for actions defined in browser.actions.xml mmt-browser-build.label=Build @@ -55,6 +56,7 @@ mmt-dockable.title=MMT mmt-treedockable.title=Theory Tree mmt-refactordockable.title=MMT refactoring mmt-graphdockable.title=MMT Theory Graphing +mmt-proofdockable.title=MMT Proof # options pane plugin.info.kwarc.mmt.jedit.MMTPlugin.option-pane=info.kwarc.mmt.jedit.MMTPlugin diff --git a/src/mmt-api/src/main/info/kwarc/mmt/api/checking/Solver.scala b/src/mmt-api/src/main/info/kwarc/mmt/api/checking/Solver.scala index e185c5ea3..a43f75200 100644 --- a/src/mmt-api/src/main/info/kwarc/mmt/api/checking/Solver.scala +++ b/src/mmt-api/src/main/info/kwarc/mmt/api/checking/Solver.scala @@ -12,7 +12,7 @@ import objects._ import proving._ import parser.ParseResult -import scala.collection.mutable.HashSet +import scala.collection.mutable.{HashSet, ListMap} import scala.runtime.NonLocalReturnControl /* ideas @@ -51,7 +51,7 @@ import scala.runtime.NonLocalReturnControl * * Use: Create a new instance for every problem, call apply on all constraints, then call getSolution. */ -class Solver(val controller: Controller, val checkingUnit: CheckingUnit, val rules: RuleSet) +class Solver(val controller: Controller, val checkingUnit: CheckingUnit, val rules: RuleSet , val initstate : Option[state] = None) extends CheckingCallback with SolverAlgorithms with Logger { /** for Logger */ @@ -69,137 +69,182 @@ class Solver(val controller: Controller, val checkingUnit: CheckingUnit, val rul /** * to have better control over state changes, all stateful variables are encapsulated a second time */ - protected object state { - /** tracks the solution, initially equal to unknowns, then a definiens is added for every solved variable */ - private var _solution : Context = initUnknowns - import scala.collection.mutable.ListMap - private var _bounds = new ListMap[LocalName,List[TypeBound]] //TODO bounds should be saved as a part of the context (that may require an artificial symbol) - /** tracks the delayed constraints, in any order */ - private var _delayed : List[DelayedConstraint] = Nil - /** tracks the errors in reverse order of encountering */ - private var _errors: List[SolverError] = Nil - /** tracks the dependencies in reverse order of encountering */ - private var _dependencies : List[CPath] = Nil - - // accessor methods for the above - def solution = _solution - def delayed = _delayed - def errors = _errors - def dependencies = _dependencies - def bounds(n: LocalName) = _bounds.getOrElse(n,Nil) - - // adder methods for the stateful lists - - /** registers a constraint */ - def addConstraint(d: DelayedConstraint)(implicit history: History) { - if (!mutable && !pushedStates.head.allowDelay) { - throw MightFail(history) - } else { - _delayed ::= d - if (!mutable) { - pushedStates.head.delayedInThisRun ::= d - } - } - } - /** registers an error */ - def addError(e: SolverError) { - if (mutable) _errors ::= e - else { - throw WouldFail + + object currentStateObj { + + + + var currentState: state = if(initstate.nonEmpty) {initstate.get} else{ new state(_solution = checkingUnit.unknowns) } + def getCurrentState = currentState + def saveCurrentState() = currentState = currentState.pushState() + def undoCurrentState() = currentState = currentState.head + + + /** + * For cycle detection in solveEquality + */ + + // private var currentState : state = state(initUnknowns , new ListMap[LocalName,List[TypeBound]] , Nil , Nil , Nil, Nil, allowDelay = true , allowSolving = true) + // private def solveEqualityStack : List[Equality] = currentState.solveEqualityStack + object SolveEqualityStack { + def apply(j : Equality)(a : => Boolean): Boolean = try { + if (currentState.solveEqualityStack contains j) { + log("Cycle in solveEquality!") + return false } - } + currentState.solveEqualityStack ::= j + val ret = a + assert(currentState.solveEqualityStack.head == j) + currentState = currentState.copy(solveEqualityStack = currentState.solveEqualityStack.tail) + ret + } catch { + case rc : NonLocalReturnControl[Boolean@unchecked] => + assert(currentState.solveEqualityStack.head == j) + currentState = currentState.copy( solveEqualityStack = currentState.solveEqualityStack.tail) + rc.value + } + } + + + // accessor methods for the above + def solution = currentState._solution // _solution + def solution_= (news : Context) { currentState._solution = news} + def delayed = currentState._delayed // _delayed + def delayed_= (ds : List[DelayedConstraint]){currentState._delayed = ds} + def errors = currentState._errors // _errors + def errors_= (ers : List[SolverError] ){currentState._errors = ers} + def dependencies = currentState._dependencies // _dependencies + def dependencies_= (deps : List[CPath]){currentState._dependencies = deps} + def bounds(n: LocalName) = currentState._bounds.getOrElse(n ,Nil) // _bounds.getOrElse(n,Nil) + def isDryRun = currentState.isDryRun + def isDryRun_= (b : Boolean) {currentState.isDryRun = b} + + + - /** registers a dependency */ - def addDependency(p: CPath) { - _dependencies ::= p - } - // more complex mutator methods for the stateful lists + // adder methods for the stateful lists - def removeConstraint(dc: DelayedConstraint) { - _delayed = _delayed filterNot (_ == dc) + def pushedStates = currentState.parent + + /** registers a constraint */ + def addConstraint(d: DelayedConstraint)(implicit history: History) { + if (!mutable && !currentState.allowDelay) { + throw MightFail(history) + } else { + currentState._delayed ::= d if (!mutable) { - val state = pushedStates.head - state.delayedInThisRun = state.delayedInThisRun.filterNot(_ == dc) - } - } - def setNewSolution(newSol: Context) { - if (!mutable && !pushedStates.head.allowSolving) { - throw MightFail(NoHistory) - } - _solution = newSol - } - // special case of setNewSolution that does not count as a side effect - def reorderSolution(newSol: Context) { - _solution = newSol - } - - def setNewBounds(n: LocalName, bs: List[TypeBound]) { - if (!mutable && !pushedStates.head.allowSolving) { - throw MightFail(NoHistory) + currentState.delayedInThisRun ::= d } - _bounds(n) = bs - } + } + } + /** registers an error */ + def addError(e: SolverError) { + if (mutable) currentState._errors ::= e + else { + throw WouldFail + } + } + + /** registers a dependency */ + def addDependency(p: CPath) { + currentState._dependencies ::= p + } + + // more complex mutator methods for the stateful lists + + def removeConstraint(dc: DelayedConstraint) { + currentState._delayed = currentState._delayed filterNot (_ == dc) + if (!mutable) { + val state = pushedStates.head + state.delayedInThisRun = state.delayedInThisRun.filterNot(_ == dc) + } + } + def setNewSolution(newSol: Context) { + if (!mutable && !currentState.allowSolving) { + throw MightFail(NoHistory) + } + currentState._solution = newSol + } + // special case of setNewSolution that does not count as a side effect + def reorderSolution(newSol: Context) { + currentState._solution = newSol + } + + def setNewBounds(n: LocalName, bs: List[TypeBound]) { + if (!mutable && !currentState.allowSolving) { + throw MightFail(NoHistory) + } + currentState._bounds(n) = bs + } - // instead of full backtracking, we allow exploratory runs that do not have side effects + // instead of full backtracking, we allow exploratory runs that do not have side effects - /** if false, all mutator methods have no effect on the state + /** if false, all mutator methods have no effect on the state * they may throw a [[DryRunResult]] */ - private def mutable = pushedStates.isEmpty - /** the state that is stored here for backtracking */ - private case class StateData(solutions: Context, bounds: ListMap[LocalName,List[TypeBound]], - dependencies: List[CPath], delayed: List[DelayedConstraint], - allowDelay: Boolean, allowSolving: Boolean) { - var delayedInThisRun: List[DelayedConstraint] = Nil - } - /** a stack of states for dry runs */ - private var pushedStates: List[StateData] = Nil + private def mutable = !currentState.isDryRun // pushedStates.isEmpty - /** true if we are currently in a dry run */ - def isDryRun = !mutable - /** + /** (kept for backwards copatability) * evaluates its arguments without generating new constraints * * all state changes are rolled back unless evaluation is successful and commitOnSuccess is true */ - def immutably[A](allowDelay: Boolean, allowSolving: Boolean, commitOnSuccess: A => Boolean)(a: => A): DryRunResult = { - val tempState = StateData(solution, _bounds, dependencies, _delayed, allowDelay, allowSolving) - pushedStates ::= tempState - def rollback { - val oldState = pushedStates.head - pushedStates = pushedStates.tail - _solution = oldState.solutions - _bounds = oldState.bounds - _dependencies = oldState.dependencies - _delayed = oldState.delayed - } - try { - val aR = a - if (tempState.delayedInThisRun.nonEmpty) { - activateRepeatedly - tempState.delayedInThisRun.headOption.foreach {h => - throw MightFail(h.history) - } - } - if (commitOnSuccess(aR)) { - pushedStates = pushedStates.tail - } else { - rollback + def immutably[A](allowDelay: Boolean, allowSolving: Boolean, commitOnSuccess: A => Boolean)(a: => A): DryRunResult = { + currentState = currentState.pushState(allowDelay = allowDelay , allowSolving = allowSolving) + currentState.isDryRun = true + def rollback { + currentState = pushedStates.head + } + try { + val aR = a + if (currentState.delayedInThisRun.nonEmpty) { + activateRepeatedly + currentState.delayedInThisRun.headOption.foreach {h => + throw MightFail(h.history) } - Success(aR) - } catch { - case e: ThrowableDryRunResult => - rollback - e } - } + if (commitOnSuccess(aR)) { + // pushedStates = pushedStates.tail + currentState.popState + currentState.isDryRun = false + } else { + rollback + } + Success(aR) + } catch { + case e: ThrowableDryRunResult => + rollback + e + } + } + def dryRunAllowErrors[A](a: => A): A = { + saveCurrentState() + val res = a + undoCurrentState() + res + } + + + def undoSlvr() : Solver = { + + val tmp = new Solver(controller ,checkingUnit , rules , Some(currentState.head)) + //tmp.currentStateObj.setCurrentState(currentState.head) // states.appendAll(states.asInstanceOf[ListBuffer[tmp.SolverState]] ) + tmp + } + + def resetErrors(e : List[SolverError]) = { + currentState._errors = Nil + } } - import state._ + + + + import currentStateObj._ /** true if unresolved constraints are left */ def hasUnresolvedConstraints : Boolean = ! delayed.isEmpty /** true if unsolved variables are left */ @@ -599,7 +644,7 @@ class Solver(val controller: Controller, val checkingUnit: CheckingUnit, val rul var toEnd = Context(it) var toEndNames = List(name) rest.foreach {vd => - val vdVars = vd.freeVars ::: state.bounds(vd.name).flatMap(_.bound.freeVars) + val vdVars = vd.freeVars ::: bounds(vd.name).flatMap(_.bound.freeVars) if (utils.disjoint(vdVars, toEndNames)) { // no dependency: move over vd toLeft = toLeft ++ vd @@ -905,6 +950,54 @@ class Solver(val controller: Controller, val checkingUnit: CheckingUnit, val rul } } } +class state(var _solution: Context = Context.empty, var _bounds: ListMap[LocalName,List[TypeBound]] = new ListMap[LocalName,List[TypeBound]](), + var _dependencies: List[CPath] = Nil, var _delayed: List[DelayedConstraint] = Nil, var solveEqualityStack : List[Equality] = Nil, var _errors : List[SolverError] = Nil, + var allowDelay: Boolean = true , var allowSolving: Boolean = true , var isDryRun : Boolean = false , var parent : Option[state] = None ) { + + def copy( _solution: Context = this._solution, _bounds: ListMap[LocalName,List[TypeBound]] = this._bounds, + _dependencies: List[CPath] = this._dependencies, _delayed: List[DelayedConstraint] = this._delayed, solveEqualityStack : List[Equality] = this.solveEqualityStack, _errors : List[SolverError] = this._errors, + allowDelay: Boolean = this.allowDelay , allowSolving: Boolean = this.allowSolving , isDryRun : Boolean = this.isDryRun , parent : Option[state] = this.parent): state ={ + new state(_solution , _bounds, _dependencies, _delayed, solveEqualityStack , _errors, allowDelay , allowSolving , isDryRun , parent) + } + + def copyFromState(s : state = this): state ={ + new state(s._solution , s._bounds, s._dependencies, s._delayed, s.solveEqualityStack , s._errors, s.allowDelay , s.allowSolving , s.isDryRun , s.parent) + } + + def copyValues(s : state) = { + _solution = s._solution + _bounds = s._bounds + _dependencies = s._dependencies + _delayed = s._delayed + solveEqualityStack = s.solveEqualityStack + _errors = s._errors + allowDelay = s.allowDelay + allowSolving = s.allowSolving + isDryRun = s.isDryRun + parent = s.parent + } + + var delayedInThisRun: List[DelayedConstraint] = Nil + def head = parent.getOrElse(this) + def tail = parent.get.parent.get + def isroot = parent.isEmpty + def pushState( _solution: Context = this._solution, _bounds: ListMap[LocalName,List[TypeBound]] = this._bounds, + _dependencies: List[CPath] = this._dependencies, _delayed: List[DelayedConstraint] = this._delayed, solveEqualityStack : List[Equality] = this.solveEqualityStack, _errors : List[SolverError] = this._errors, + allowDelay: Boolean = this.allowDelay , allowSolving: Boolean = this.allowSolving , isDryRun : Boolean = this.isDryRun) = { + val tmp = this.copy(_solution , _bounds , _dependencies, _delayed, solveEqualityStack,_errors, allowDelay, allowSolving,isDryRun ,parent = Some(this)) + tmp + } + def popState = parent match { + case Some(v) => { + parent = v.parent + } + case None => + } + def descendsFrom(anc: state): Boolean = parent.contains(anc) || (parent match { + case None => false + case Some(p) => p.descendsFrom(anc) + }) +} /** auxiliary methods and high-level type reconstruction API */ object Solver { diff --git a/src/mmt-api/src/main/info/kwarc/mmt/api/checking/SolverAlgorithms.scala b/src/mmt-api/src/main/info/kwarc/mmt/api/checking/SolverAlgorithms.scala index 6d9a70925..6ef9ff952 100644 --- a/src/mmt-api/src/main/info/kwarc/mmt/api/checking/SolverAlgorithms.scala +++ b/src/mmt-api/src/main/info/kwarc/mmt/api/checking/SolverAlgorithms.scala @@ -18,7 +18,7 @@ import scala.runtime.NonLocalReturnControl * factored out from the [[Solver]] class, which holds all bureaucracy */ trait SolverAlgorithms {self: Solver => - import state._ + import currentStateObj._ private implicit val sa = new MemoizedSubstitutionApplier /** precomputes relevant rule sets, ordered by priority */ diff --git a/src/mmt-api/src/main/info/kwarc/mmt/api/proving/itp/Goal.scala b/src/mmt-api/src/main/info/kwarc/mmt/api/proving/itp/Goal.scala new file mode 100644 index 000000000..dcbc795d4 --- /dev/null +++ b/src/mmt-api/src/main/info/kwarc/mmt/api/proving/itp/Goal.scala @@ -0,0 +1,87 @@ +package info.kwarc.mmt.api.proving.itp + +import info.kwarc.mmt.api.LocalName +import info.kwarc.mmt.api.checking.Solver +import info.kwarc.mmt.api.objects.{Context, Sub, Term, VarDecl} + +import scala.collection.mutable.ListBuffer + +/** + * represents a (sub)goal in a [[Proof]] + * @param g the conclusion/goal of the current (sub)goal + * @param ctx the local context of the goal + * @param ukname the name of the unknown it represents in the proof term [[Proof.proofTerm]]/[[Proof.proofTermAlt]] + */ +case class Goal(g : Term , ctx : Context , ukname : LocalName) { + + // var gname : LocalName = null + + /** + * gives a string representation of all of the (sub)goals + * @param s + * @return + */ + def printGoal(s: Solver): String = { + val res: ListBuffer[String] = ListBuffer[String]() + res.append("Focused Goal: " + ukname) + res.append("---------------") + for (i <- ctx.variables) { + val nm = i.name.toString + val tp = i.tp.map(x => s.presentObj(x)).getOrElse("no type") + res.append(nm + " : " + tp) + } + res.append("---------------") + res.append(s.presentObj(g)) + res.mkString("\n") + } + + def makeUnknown(s: Solver, u: LocalName) = { + s.Unknown(u, ctx.variables.map(x => x.toTerm).toList) + } + + + /** + * clreates a copy/clone of the proof (used for the history in the proof manager) + * @return + */ + def copy: Goal = { + val tmpg = Goal(g: Term, ctx, ukname) + // tmpg.gname = gname.copy() + tmpg + } + + /** + * convenience method to get the first substitution with name `ln` + * @param ln + * @param ls + * @return + */ + def getFirst(ln: LocalName, ls: List[Sub]): Option[Term] = ls match { + case Nil => None + case Sub(nm, t) :: xs => { + if (nm == ln) { + Some(t) + } else { + getFirst(ln, xs) + } + } + } + + /** + * same as [[getFirst]] but for [[VarDecl]] + * @param ln + * @param ls + * @return + */ + def getFirstV(ln: LocalName, ls: List[VarDecl]): Option[VarDecl] = ls match { + case Nil => None + case v :: xs => { + if (v.name == ln) { + Some(v) + } else { + getFirstV(ln, xs) + } + } + } + +} \ No newline at end of file diff --git a/src/mmt-api/src/main/info/kwarc/mmt/api/proving/itp/Msg.scala b/src/mmt-api/src/main/info/kwarc/mmt/api/proving/itp/Msg.scala new file mode 100644 index 000000000..84273da3c --- /dev/null +++ b/src/mmt-api/src/main/info/kwarc/mmt/api/proving/itp/Msg.scala @@ -0,0 +1,59 @@ +package info.kwarc.mmt.api.proving.itp + +/** + * the returnmessgae of a tactic when executed + */ +trait Msg { + def combineMsg(m : Msg): Msg +} + +/** + * error message + * @param s + */ +case class HasError(s : String ) extends Msg { + override def combineMsg(m: Msg): Msg = this + + /*m match { + case HasError(st) => HasError(s ++ "\n" ++ st) + case WarningMsg(st) => HasError(s ++ "\n" ++ st) + case NoMsg() => this + } + + */ +} + +/** + * warning message + * @param s + */ +case class WarningMsg(s : String) extends Msg { + override def combineMsg(m: Msg): Msg = m match { + case HasError(st) => HasError(s ++ "\n" ++ st) + case WarningMsg(st) => WarningMsg(s ++ "\n" ++ st) + case NoMsg() => this + } +} + +/** + * plain message (i.e. no error or warning) + * @param s + */ +case class SimpleMsg(s : String) extends Msg { + override def combineMsg(m: Msg): Msg = m match { + case HasError(st) => HasError(s ++ "\n" ++ st) + case WarningMsg(st) => WarningMsg(s ++ "\n" ++ st) + case NoMsg() => this + } +} + +/** + * no message at all (i.e. no warning or error) + */ +case class NoMsg() extends Msg { + override def combineMsg(m: Msg): Msg = m match { + case HasError(st) => HasError(st) + case WarningMsg(st) => WarningMsg(st) + case NoMsg() => this + } +} \ No newline at end of file diff --git a/src/mmt-api/src/main/info/kwarc/mmt/api/proving/itp/Proof.scala b/src/mmt-api/src/main/info/kwarc/mmt/api/proving/itp/Proof.scala new file mode 100644 index 000000000..0cbba7c82 --- /dev/null +++ b/src/mmt-api/src/main/info/kwarc/mmt/api/proving/itp/Proof.scala @@ -0,0 +1,191 @@ +package info.kwarc.mmt.api.proving.itp + +import info.kwarc.mmt.api.LocalName +import info.kwarc.mmt.api.checking.Solver +import info.kwarc.mmt.api.objects._ + +import scala.collection.mutable.{ListBuffer, Map => mmap, Set => MSet} + +class Proof(t : Term, globalContext : Context , igoal : Term ) { + val currentState : ListBuffer[Goal] = ListBuffer(Goal(t, Context(), LocalName("" , "goal"))) + /** + * not actively used. Meant to trace intergoal dependencies (for example if let introduces new unkowns) + */ + val goalDependencies : mmap[LocalName , ListBuffer[(LocalName,LocalName)]] = mmap.empty + val solvedVariables : MSet[LocalName] = MSet() + val gctx : Context = globalContext + val initGoal : Term = igoal + var goalcounter : Int = 0 + + + /** + * the proof term that represents the proof. This proof term represents a hole as application of free variables to an unknown + */ + var proofTerm : Term = null + /** + * an alternative representation of [[proofTerm]] that removes the free vars + */ + var proofTermAlt : Term = null + + /** + * + * @return new unique goal name + */ + def getNewGoalName() : LocalName = { + goalcounter += 1 + LocalName("" , "goal" , goalcounter.toString ) + } + + /** + * convenience method for updating the unknowns in the [[proofTerm]] + * @param s + */ + def updateProofTerm(s : Solver) = { + proofTerm = s.substituteSolution(proofTerm) + } + + /** + * like [[updateProofTerm]] but as a terverser + * @param ln + * @param t + */ + class UpdateGoalTraverser(ln : LocalName, t : Term) extends StatelessTraverser { + override def traverse(tt: Term)(implicit con: Context, state: State): Term = tt match { + case OMV(lnn) if lnn == ln => t + case _ => Traverser(this , tt) + } + } + + /** + * + * @param ls + * @param t + */ + def updateGoalProofTerm(ls : LocalName , t : Term) = { + val tr = new UpdateGoalTraverser(ls, t) + val res = tr.traverse(proofTermAlt)(Context() , ()) + proofTermAlt = res + } + + + /** + * + * @param s + * @return + */ + def proofStateToString(s : Solver) : String ={ + if(currentState.isEmpty) { + return "all goals solved" + } + val res = ListBuffer[String]() + res.append( currentState.head.printGoal(s)) + for(i <- currentState.tail){ + res.append(s.presentObj(i.g)) + } + res.mkString("\n") + } + + /** + * convenience function to get the first goal + * @return the first goal + */ + def getCurrentGoal : Goal = currentState.head + + /** + * + * @return the conclusion/goal of the first goal + */ + def getCurrentConc : Term = currentState.head.g + + def getCurrCtx : Context = currentState.head.ctx + + /** + * update the first goal + * @param g the updated value + */ + def update(g : Goal) = {val tmp = currentState.remove(0); currentState.insert(0,g) } + + + def getCurrCtxMp : Context = getCurrCtx ++ globalContext + + + /** + * generates a copy/clone of the proof + * @return copy/clone of the current proof state + */ + def copy : Proof = { + val p = new Proof(t , globalContext, initGoal) + p.currentState.remove(0) + for (g <- currentState){ + val newg = g.copy + p.currentState.append(newg) + } + p.proofTerm = proofTerm + p.proofTermAlt = proofTermAlt + p.goalcounter = goalcounter + p.solvedVariables ++= solvedVariables.toList + p.goalDependencies ++= goalDependencies + p + } + + /** + * sometimes an unknown gets solved but its solution will not necessarily be subsituted in the whole proof, this function, which gets called after + * a tactic has been executed, takes all new solutions and substitutes them in the whole proof + * @param s + * @return + */ + def updateUnknowns(s : Solver): Msg = { + // get all solved variables. This will get all variables solved so far in this proof + val sols = s.getSolvedVariables + // get all unknowns + val ps = s.getPartialSolution + var nrem = 0 + for(i <- currentState.indices){ + val tmp = currentState(i - nrem) + if (sols.contains(tmp.ukname)) { + val vd = ps.get(tmp.ukname) + val fv = vd.df.get.freeVars + if (!fv.forall(p => tmp.ctx.exists((x : VarDecl) => x.name == p))) { + return HasError(tmp.ukname.toString + " was solved illegally") + } + currentState.remove(i - nrem) + updateGoalProofTerm(vd.name , vd.df.get) + nrem += 1 + } + } + + for (i <- ps){ + if (i.tp.isEmpty) return HasError("could not infer type of " + i.name) + } + + val newsols = s.getSolvedVariables.filter(p => ! solvedVariables.contains(p)) + val newsols0 = newsols.map(x => s.getPartialSolution.get(x)) + val subs = Substitution(newsols0.map(x => Sub(x.name , x.df.get)) : _*) + for(i <- currentState.indices){ + val Goal(g, gctx , gukname) = currentState(i) + val newg = Goal(g.substitute(subs)(PlainSubstitutionApplier) , gctx.map(x => x.copy(tp = Some(x.tp.get.substitute(subs)(PlainSubstitutionApplier)))) , gukname ) + currentState.update(i , newg) + } + + + solvedVariables ++= newsols + NoMsg() + } + + /** + * currently not really used + * @param ctx + * @param gname + * @param hname + */ + def addukdeps( ctx : Context , gname : LocalName , hname : LocalName): Unit = { + ctx.foreach(v => { + lazy val deps = goalDependencies(v.name) + if (goalDependencies.contains(v.name)){ + deps.insert(0,(gname , hname)) + }else { + goalDependencies(v.name) = ListBuffer((gname , hname)) + } + }) + } +} \ No newline at end of file diff --git a/src/mmt-api/src/main/info/kwarc/mmt/api/proving/itp/ProofUtil.scala b/src/mmt-api/src/main/info/kwarc/mmt/api/proving/itp/ProofUtil.scala new file mode 100644 index 000000000..b7e74090e --- /dev/null +++ b/src/mmt-api/src/main/info/kwarc/mmt/api/proving/itp/ProofUtil.scala @@ -0,0 +1,70 @@ +package info.kwarc.mmt.api.proving.itp + +import info.kwarc.mmt.api.checking.{CheckingUnit, History, Solver} +import info.kwarc.mmt.api.frontend.{Controller, Report} +import info.kwarc.mmt.api.objects._ +import info.kwarc.mmt.api.presentation.{MMTSyntaxPresenter, NotationBasedPresenter, PresentationContext} + +object ProofUtil { + /** + * print an MMT-Object with as many, non repeating brackets as possible. + * @param controller + * @param report + * @param o the MMT-Object to be printed + * @return + */ + def presentBracketed(controller : Controller , report : Report, o :Obj) : String = { + + val ps = controller.presenter.asInstanceOf[MMTSyntaxPresenter] + val tmp = ps.objectLevel + val c = controller + val r = report + val b = new NotationBasedPresenter /* with info.kwarc.mmt.api.frontend.Extension */ { + controller = c + report = r + + override def twoDimensional: Boolean = false + + override def doUnbracketedGroup(body: => Unit)(implicit pc: PresentationContext): Unit = super.doBracketedGroup(body) + } + val bpres = new MMTSyntaxPresenter(b) + + bpres.asString(o) + } + + + def standAloneInfer(t : Term , uks : Context , currctx : Context , hist : History, s : Solver) = { + val cu = new CheckingUnit(None , currctx ,uks , null) + val exslv = new Solver(s.controller , cu , s.rules) + val res = exslv.inferType(t , false)(Stack(Context.empty) ,hist) + (res , exslv.getPartialSolution , exslv.getErrors , exslv.getConstraints) + } + + def unify(ctx : Context , goal : Term , params : Context , query : Term , hist : History , s : Solver) = { + + val (newparams , subparams) = Context.makeFresh(params , ctx.variables.map(_.name).toList) + val revert = subparams.map(x => (x.target.asInstanceOf[OMV].name , x.name)) + val unifier = new Solver(s.controller , CheckingUnit(None, s.constantContext , newparams, null) , s.rules ) + val ures = unifier.apply(Equality(Stack(ctx) , goal , query ^ subparams , None)) + + ures && unifier.getConstraints.isEmpty && unifier.getErrors.isEmpty match { + case false => None + case true => { + // val res = unifier.dryRun(false, ((p : Unit) => true))(() : Unit) + Some(Substitution(unifier.getPartialSolution.toPartialSubstitution.map(x => {val tmp = revert.find(p => p._1 == x.name).get ; x.copy(name = tmp._2) }) : _ *)) + } + } + } + +/* + def executeAndReset[A](a: => A, ip : InteractiveProof): A = { + val tmps = ip.slvr.state + // saveCurrState() + val res = a + // undoState() + + res + } + + */ +} diff --git a/src/mmt-api/src/main/info/kwarc/mmt/api/proving/itp/TypedTerm.scala b/src/mmt-api/src/main/info/kwarc/mmt/api/proving/itp/TypedTerm.scala new file mode 100644 index 000000000..ec01617c0 --- /dev/null +++ b/src/mmt-api/src/main/info/kwarc/mmt/api/proving/itp/TypedTerm.scala @@ -0,0 +1,8 @@ +package info.kwarc.mmt.api.proving.itp + + + + + + + diff --git a/src/mmt-lf/src/info/kwarc/mmt/itp/Constants.scala b/src/mmt-lf/src/info/kwarc/mmt/itp/Constants.scala deleted file mode 100644 index 3b3dc28e6..000000000 --- a/src/mmt-lf/src/info/kwarc/mmt/itp/Constants.scala +++ /dev/null @@ -1,16 +0,0 @@ -package info.kwarc.mmt.itp - -import info.kwarc.mmt.lf._ -import info.kwarc.mmt.api._ -import utils._ -import objects._ -import uom._ - -object ITP { - val _base = Typed._base / ".." / "examples" - val _path = _base ? "ITP" - - object proof extends FlexaryConstantScala(_path, "proof") - - object assume extends BinaryConstantScala(_path, "assume") -} diff --git a/src/mmt-lf/src/info/kwarc/mmt/itp/Rules.scala b/src/mmt-lf/src/info/kwarc/mmt/itp/Rules.scala deleted file mode 100644 index efcc18671..000000000 --- a/src/mmt-lf/src/info/kwarc/mmt/itp/Rules.scala +++ /dev/null @@ -1,18 +0,0 @@ -package info.kwarc.mmt.itp - -import info.kwarc.mmt.api.{checking, _} -import checking._ -import uom._ -import objects._ -import objects.Conversions._ -import info.kwarc.mmt.lf._ - -import ITP._ - -/** */ -object ProofTerm extends InferenceRule(ITP.proof.path, OfType.path) { - def apply(solver: Solver)(tm: Term, covered: Boolean)(implicit stack: Stack, history: History) : Option[Term] = { - val proof(args) = tm - None - } -} diff --git a/src/mmt-lf/src/info/kwarc/mmt/lf/itp/InteractiveProof.scala b/src/mmt-lf/src/info/kwarc/mmt/lf/itp/InteractiveProof.scala new file mode 100644 index 000000000..d49b9436d --- /dev/null +++ b/src/mmt-lf/src/info/kwarc/mmt/lf/itp/InteractiveProof.scala @@ -0,0 +1,136 @@ +package info.kwarc.mmt.lf.itp + +import info.kwarc.mmt.api.MPath +import info.kwarc.mmt.api.checking.{History, Solver} +import info.kwarc.mmt.api.objects.{Inhabitable, Stack, Typing} +import info.kwarc.mmt.api.proving.itp._ + +import scala.collection.mutable.ListBuffer + +/** + * a proof manager (here called [[InteractiveProof]]) manages a proof and its meta + * @param s the solver used for this proof + * @param p the actual proof (i.e. a collection of goals and its contexts) + * @param mpath the mmt path of this proof + */ +class InteractiveProof(s : Solver , p : Proof , mpath : Option[MPath], generateProofTermInit : Boolean = true ){ + var testrun : Boolean = false + var pr : Proof = p + var slvr : Solver = s + val tp = new TacticParser(this) + val mp = mpath + val steps : ListBuffer[Tactic]= ListBuffer() + val stepsS : ListBuffer[String] = ListBuffer() + var generateProofTerm : Boolean = generateProofTermInit + def dontGenerateProofTerm : Boolean = ! generateProofTerm + /** + * the history saves previous proof steps used for undo-actions + */ + val history : ListBuffer[Proof ] = ListBuffer() + val hist = new History(Nil) + + /** + * saves the current proof state in the history + */ + def saveCurrState = { + val old = pr.copy + slvr.currentStateObj.saveCurrentState() + history.insert(0 , old) + } + + /** + * executes a tactics , undos the state changes coused by the tactic if it fails + * @param t the tactic to be executed + * @return the potential warning/error message generated by the tactic + */ + def executeStep(t : Tactic): Msg ={ + // execute the tactic + val ret = try { + t.applyToProof(pr, this) + }catch + { + case e => HasError(e.getStackTrace.mkString("\n")) + } + val dbg1 = () + if(testrun) { + ret match { + case HasError(s) => undo ; return ret + case _ => + } + val ret1 = if (slvr.getErrors.nonEmpty) { + val errs = slvr.getErrors; undo; return ret.combineMsg(HasError(errs.mkString("\n"))) + } else ret + + val ret2 = if (slvr.getConstraints.nonEmpty) { + val msg = slvr.getConstraints.toString(); undo; return ret1.combineMsg(HasError("could not solve constrains " + msg)) + } else ret1 + val dbg = () + ret2 match { + case NoMsg() | WarningMsg(_) => ret2 + case HasError(_) => undo; ret2 + } + }else { + + val ret0 = ret match { + case NoMsg() | WarningMsg(_) => { + try { + pr.updateProofTerm(slvr); ret + } catch { + case e => HasError(e.getStackTrace.mkString("\n")) + } + } + case HasError(s) => { + undo + return ret + + } + } + val ret1 = if (slvr.getErrors.nonEmpty) { + val errs = slvr.getErrors; undo; return ret0.combineMsg(HasError(errs.mkString("\n"))) + } else ret0 + val ret2 = if (slvr.getConstraints.nonEmpty) { + val msg = slvr.getConstraints.toString(); undo; return ret1.combineMsg(HasError("could not solve constrains " + msg)) + } else ret1 + val ukmsg0 = pr.updateUnknowns(slvr).combineMsg(ret2) + val ukmsg1 = if (pr.currentState.isEmpty) { + val bl = slvr.check(Typing(Stack(slvr.checkingUnit.context), pr.proofTermAlt, pr.initGoal))(hist) + if (bl && slvr.getErrors.isEmpty && slvr.getUnsolvedVariables.isEmpty) { + ukmsg0 + } else { + HasError("solution doesn't check out").combineMsg(ukmsg0) + } + } else ukmsg0 + val ukmsg2 = if (pr.currentState.isEmpty) { + val bl = slvr.check(Typing(Stack(slvr.checkingUnit.context), pr.proofTerm, pr.initGoal))(hist) + if (bl && slvr.getErrors.isEmpty && slvr.getUnsolvedVariables.isEmpty) { + ukmsg1 + } else { + HasError("solution doesn't check out").combineMsg(ukmsg1) + } + } else ukmsg1 + val ukmsg = if (pr.currentState.isEmpty) { + val bl = slvr.applyMain + if (bl && slvr.getErrors.isEmpty && slvr.getUnsolvedVariables.isEmpty) { + ukmsg2 + } else { + HasError("solution doesn't check out").combineMsg(ukmsg2) + } + } else ukmsg2 + ukmsg match { + case NoMsg() | WarningMsg(_) => ukmsg + case HasError(_) => undo; ukmsg + } + } + } + + /** + * perform an undo step + */ + def undo : Unit ={ + if (history.isEmpty) return + val prold = history.remove(0) + pr = prold + slvr = slvr.currentStateObj.undoSlvr() + } + +} \ No newline at end of file diff --git a/src/mmt-lf/src/info/kwarc/mmt/lf/itp/InteractiveStructuredProof/Fixity.scala b/src/mmt-lf/src/info/kwarc/mmt/lf/itp/InteractiveStructuredProof/Fixity.scala new file mode 100644 index 000000000..2ce300349 --- /dev/null +++ b/src/mmt-lf/src/info/kwarc/mmt/lf/itp/InteractiveStructuredProof/Fixity.scala @@ -0,0 +1,27 @@ +package info.kwarc.mmt.lf.itp.InteractiveStructuredProof + +trait Argpos { + def getprio : Int +} + +case class ArgL(prio : Int) extends Argpos{ + override def getprio: Int = prio +} +case class ArgR(prio : Int) extends Argpos{ + override def getprio: Int = prio +} + + + + +abstract class Fixity(val prio:Int , val arglist : List[Argpos]) { + def isleft : Boolean +} + +case class FixityLeft(override val prio:Int, override val arglist : List[Argpos]) extends Fixity(prio, arglist){ + override def isleft: Boolean = true +} +case class FixityRight(override val prio:Int, override val arglist : List[Argpos]) extends Fixity(prio,arglist){ + override def isleft: Boolean = false +} + diff --git a/src/mmt-lf/src/info/kwarc/mmt/lf/itp/InteractiveStructuredProof/InteractiveStructuredProof.scala b/src/mmt-lf/src/info/kwarc/mmt/lf/itp/InteractiveStructuredProof/InteractiveStructuredProof.scala new file mode 100644 index 000000000..1f6c7206b --- /dev/null +++ b/src/mmt-lf/src/info/kwarc/mmt/lf/itp/InteractiveStructuredProof/InteractiveStructuredProof.scala @@ -0,0 +1,10 @@ +package info.kwarc.mmt.lf.itp.InteractiveStructuredProof + +import info.kwarc.mmt.lf.itp.InteractiveProof + +class InteractiveStructuredProof(ip : InteractiveProof) { + + def parseAndExecute(s : String ): Unit = { + + } +} diff --git a/src/mmt-lf/src/info/kwarc/mmt/lf/itp/InteractiveStructuredProof/NewTactic.scala b/src/mmt-lf/src/info/kwarc/mmt/lf/itp/InteractiveStructuredProof/NewTactic.scala new file mode 100644 index 000000000..af9835bd0 --- /dev/null +++ b/src/mmt-lf/src/info/kwarc/mmt/lf/itp/InteractiveStructuredProof/NewTactic.scala @@ -0,0 +1,5 @@ +package info.kwarc.mmt.lf.itp.InteractiveStructuredProof + + + + diff --git a/src/mmt-lf/src/info/kwarc/mmt/lf/itp/InteractiveStructuredProof/StructuredProofParseRule.scala b/src/mmt-lf/src/info/kwarc/mmt/lf/itp/InteractiveStructuredProof/StructuredProofParseRule.scala new file mode 100644 index 000000000..b43ff2d4f --- /dev/null +++ b/src/mmt-lf/src/info/kwarc/mmt/lf/itp/InteractiveStructuredProof/StructuredProofParseRule.scala @@ -0,0 +1,9 @@ +package info.kwarc.mmt.lf.itp.InteractiveStructuredProof + +import info.kwarc.mmt.api.Rule +import info.kwarc.mmt.lf.itp.{InteractiveProof, Tactic} + +trait StructuredProofParseRule extends Rule { + var fixity : Fixity + def parseTactic(sp : StructuredProofParser , ip : InteractiveProof) : sp.Parser[Tactic] +} diff --git a/src/mmt-lf/src/info/kwarc/mmt/lf/itp/InteractiveStructuredProof/StructuredProofParser.scala b/src/mmt-lf/src/info/kwarc/mmt/lf/itp/InteractiveStructuredProof/StructuredProofParser.scala new file mode 100644 index 000000000..32768b5f2 --- /dev/null +++ b/src/mmt-lf/src/info/kwarc/mmt/lf/itp/InteractiveStructuredProof/StructuredProofParser.scala @@ -0,0 +1,50 @@ +package info.kwarc.mmt.lf.itp.InteractiveStructuredProof + +import info.kwarc.mmt.api.Rule +import info.kwarc.mmt.api.checking.Solver +import info.kwarc.mmt.lf.itp.{InteractiveProof, Tactic} + +import scala.util.parsing.combinator.{JavaTokenParsers, PackratParsers} +import scala.util.parsing.input.CharSequenceReader + +class StructuredProofParser extends JavaTokenParsers with PackratParsers{ + def parseStructuredProof(ip : InteractiveProof , str : String) : Option[Tactic] = { + + val parsers = ip.slvr.rules.getOrdered(classOf[StructuredProofParseRule]).map(x => x.parseTactic(this, ip)) + + def findparser(prs: List[Parser[(Tactic, Fixity)]], in: Input): ParseResult[(Tactic, Fixity)] = prs match { + case Nil => Error("no applicable parser", in) + case x :: xs => x.apply(in) match { + case s@Success(tac, nxt) => s + case _ => findparser(xs, in) + } + } +/* + def parseloop(in: Input): Option[List[(Tactic, Fixity)]] = if (in.atEnd) Some(Nil) else findparser(parsers, in) match { + case Success(t, nxt) => { + parseloop(nxt).map(t :: _) + + } + case _ => None + } + + val tmp = parseloop(new CharSequenceReader(str)) + + val orderedprio = tmp.map(x => x.sortWith((x,y) => x._2.prio < y._2.prio || x._2.prio == y._2.prio && x._2.isleft && !y._2.isleft ).distinct) + val tmp0 = tmp.map(_.zipWithIndex) + + def buildparsetree(ls : List[((Tactic, Fixity ),Int)], ls0 : List[(Tactic,Fixity)]) = ls0 match { + case Nil => + case (t, FixityLeft(p , al))::xs => { + + } + case(t , FixityRight(p , al)):: xs => { + + } + } + + */ + +??? + } +} diff --git a/src/mmt-lf/src/info/kwarc/mmt/lf/itp/NewTacticParser.scala b/src/mmt-lf/src/info/kwarc/mmt/lf/itp/NewTacticParser.scala new file mode 100644 index 000000000..677d6b41a --- /dev/null +++ b/src/mmt-lf/src/info/kwarc/mmt/lf/itp/NewTacticParser.scala @@ -0,0 +1,7 @@ +package info.kwarc.mmt.lf.itp + +import scala.util.parsing.combinator.JavaTokenParsers + +object NewTacticParser extends JavaTokenParsers{ + +} diff --git a/src/mmt-lf/src/info/kwarc/mmt/lf/itp/ProofGenerator.scala b/src/mmt-lf/src/info/kwarc/mmt/lf/itp/ProofGenerator.scala new file mode 100644 index 000000000..366e8b2a6 --- /dev/null +++ b/src/mmt-lf/src/info/kwarc/mmt/lf/itp/ProofGenerator.scala @@ -0,0 +1,75 @@ +package info.kwarc.mmt.lf.itp + +import info.kwarc.mmt.api.checking.{CheckingUnit, Solver} +import info.kwarc.mmt.api.frontend.Controller +import info.kwarc.mmt.api.objects._ +import info.kwarc.mmt.api.proving.itp.Proof +import info.kwarc.mmt.api.{CPath, LocalName, MPath, RuleSet} + +/** + * contains functions to generate new proof manager [[InteractiveProof]] + */ +object ProofGenerator { + /** + * generate a new proof manager + * @param c crontoller used in the proof manager + * @param mp the MPath that this proof manager belongs to + * @param cp the content path this proof manager belongs to + * @param tp term to be provern + * @return a new proof manager + */ + def setupNewProof(c: Controller, mp: Option[MPath], cp: Option[CPath], tp: Term) = { + val goal = VarDecl(LocalName("", "goal"), tp, null) + val mpc = if (mp.isEmpty) Context.empty else Context(mp.get) + val cu = new CheckingUnit(cp, mpc, Context(goal), Inhabitable(Stack(Context()), tp)) + val s = new Solver(c, cu, RuleSet.collectRules(c, mpc)) + + val p = new Proof(tp, mpc, tp ) + p.proofTerm = OMV(LocalName("", "goal")) + p.proofTermAlt = OMV(LocalName("", "goal")) + Some(new InteractiveProof(s, p, mp)) + } + + /** + * like [[setupNewProof]] but gets an explicit proof context + * @param s + * @param tp + * @param globalctx + * @param mp + * @return + */ + def setupNewProofA(s : Solver, tp : Term, globalctx : Context , mp : MPath) = { + val p = new Proof(tp, globalctx, tp) + p.proofTerm = OMV(LocalName("", "goal")) + p.proofTermAlt = OMV(LocalName("", "goal")) + // s.addUnknowns(Context(VarDecl(LocalName("", "goal"), tp, null)) , None) + val tmp = new InteractiveProof(s, p, Some(mp)) + tmp.slvr.addUnknowns(Context(VarDecl(LocalName("", "goal"), tp, null)) , None) + Some(tmp) + } + + + def setupNewProofAA(s : Solver, tp : Term) = { + + val (mp , ctx ) = if (s.checkingUnit.component.isEmpty){ + (None , Context.empty) + }else { + val (Some(dp) , Some(mn) , _) = s.checkingUnit.component.get.parent.toTriple + val tmpmp = dp ? mn + (Some(tmpmp) , Context(tmpmp)) + } + + setupNewProof(s.controller , mp , s.checkingUnit.component , tp) + /* val p = new Proof(tp, ctx , tp) + p.proofTerm = OMV(LocalName("", "goal")) + p.proofTermAlt = OMV(LocalName("", "goal")) + // s.addUnknowns(Context(VarDecl(LocalName("", "goal"), tp, null)) , None) + val tmp = new InteractiveProof(s, p, mp) + tmp.slvr.addUnknowns(Context(VarDecl(LocalName("", "goal"), tp, null)) , None) + Some(tmp) + + + */ + + } +} diff --git a/src/mmt-lf/src/info/kwarc/mmt/lf/itp/ProofUtil.scala b/src/mmt-lf/src/info/kwarc/mmt/lf/itp/ProofUtil.scala new file mode 100644 index 000000000..639370d44 --- /dev/null +++ b/src/mmt-lf/src/info/kwarc/mmt/lf/itp/ProofUtil.scala @@ -0,0 +1,546 @@ +package info.kwarc.mmt.lf.itp + +import info.kwarc.mmt.api.LocalName +import info.kwarc.mmt.api.checking.{CheckingUnit, History, Hole, Solver} +import info.kwarc.mmt.api.objects.{Context, Equality, Free, MatchFail, MatchSuccess, Matcher, OMA, OMATTR, OMBINDC, OMFOREIGN, OMID, OML, OMLIT, OMLITTrait, OMSemiFormal, OMV, PlainSubstitutionApplier, Stack, StatelessTraverser, Sub, Substitution, Term, Traverser, Typing, UnknownOMLIT, VarDecl} +import info.kwarc.mmt.api.proving.itp.Goal +import info.kwarc.mmt.api.proving.itp.ProofUtil.unify +import info.kwarc.mmt.lf.{Arrow, FunType, Lambda, OfType, Pi} + +import scala.collection.Map +import scala.collection.mutable.ListBuffer +import scala.collection.{Map, mutable} +import scala.collection.mutable.{ListBuffer, Map => MMap} +/** + * contains several helper methods used throughout the prover implementation + */ +object ProofUtil { + + /** + * generates a new hypothesis name, unlike [[Context.pickFresh(...)]] this function avoids backslash + * @param s the original name upon which a unique variant of it is to be created + * @param ctx the context in which the new name should be unique + * @return a new hypothesis name that is unique in the context of `ctx` + */ + def pickFreshHypName(s : String , ctx : Context) : String = { + var i : Option[Int]= None + var res = s + val names = ctx.variables.map(x => x.name.toString) + while(names.contains(res)){ + res = s + i.getOrElse("0") + i = Some(i.getOrElse(0) + 1) + } + res + } + + + /** + * get all the `LocalName`s of bound vairables in the term `t0` + * @param t0 the term to be searched + * @param lss list containing `LocalName` + * @return + */ + def getBoundNames(t0 : Term, lss : List[LocalName]): List[LocalName] = { + + + def getBoundNamesL(t: Term, ls : List[LocalName]): List[LocalName] = { + t match { + case Lambda(nm ,tp , bd) => getBoundNamesL(bd , nm :: ls) + case Pi(nm , tp , bd) => getBoundNamesL(bd , nm :: ls) + case OMID(path) => if (ls.contains((x : LocalName) => x == path.name)) Nil else List(path.name) + case OMBINDC(binder, context, scopes) => ??? + case OMA(fun, args) =>getBoundNamesL(fun , ls) ++ args.flatMap(x => getBoundNamesL(x , ls)) + case OMV(name) => if (ls.contains((x : LocalName) => x == name)) Nil else List(name) + case OMATTR(arg, key, value) => ??? + case tTrait: OMLITTrait => ??? + case OMLIT(value, rt) => ??? + case UnknownOMLIT(valueString, synType) => ??? + case OMFOREIGN(node) => ??? + case OMSemiFormal(tokens) => ??? + case OML(name, tp, df, nt, featureOpt) => ??? + } + } + + getBoundNamesL(t0 ,lss) + } + + + /** + * just returns the first element in ls that satisfies p + * @param ls + * @param p + * @tparam A + * @return + */ + def getFirst[A](ls : List[A] , p : A => Boolean ) : Option[A] = ls match { + case Nil => None + case x::xs => { + if (p(x)) return Some(x) else getFirst(xs , p) + } + } + + /** + * a substitute function that can replace whole terms `old0` (not just OMVs) by + * @param t0 term which contains the to be replaced (sub)term + * @param old0 term to be replaced + * @param newt0 term that replaces `old0` + * @param rel relation that decides whether a subterm and `old0` are equal + * @return `t0` but with old0 replaced by + */ + def substitute(t0 : Term , old0 : Term , newt0 : Term, rel : (Term , Term, Context) => Boolean) : Term = { + val tmp = getBoundNames(newt0, Nil) + + + def substituteL(t : Term , old : Term , newt : Term, additionalContext : Context) : Term = { + if (rel(t , old, additionalContext)) return newt + t match { + case Lambda(nm, tp, bd) => { + if (tmp.contains(nm)) { + val newn = pickFreshHypName(nm.toString , Context(tmp.map(x => VarDecl(x)) : _*)) + val newbd = bd.substitute(Substitution(Sub(nm , OMV(newn))))(PlainSubstitutionApplier) + val newbd0 = substituteL(newbd , old , newt, additionalContext ++ VarDecl(LocalName(newn) , tp , null )) + Lambda(LocalName(newn) , tp , newbd0) + }else {Lambda(nm , tp , substituteL(bd , old , newt, additionalContext ++ VarDecl(nm , tp , null)))} + } + case Pi(nm ,tp, bd) if (nm.toString != "_") => { + if (tmp.contains(nm)) { + val newn = pickFreshHypName(nm.toString , Context(tmp.map(x => VarDecl(x)) : _*)) + val newbd = bd.substitute(Substitution(Sub(nm , OMV(newn))))(PlainSubstitutionApplier) + val newbd0 = substituteL(newbd , old , newt, additionalContext ++ VarDecl(LocalName(newn) , tp , null)) + Pi(LocalName(newn) , tp , newbd0) + }else {Pi(nm , tp , substituteL(bd , old , newt ,additionalContext ++ VarDecl(nm , tp , null)))} + } + case OMA(fun , args) => { + OMA(substituteL(fun , old , newt , additionalContext) , args.map(x => substituteL(x , old , newt, additionalContext))) + } + case _ => t + } + + } + substituteL(t0 , old0 , newt0 , Context()) + } + + /** + * traverser used for substitution + * @param old + * @param newt + * @param rel + * @param pos + */ + class SubTraverser(old : Term , newt : Term, rel : (Term , Term, Context) => Boolean , pos : Option[Int]) extends StatelessTraverser { + var currpos = pos + val tmp = newt.freeVars + + override def traverse(t: Term)(implicit additionalContext: Context, state: Unit): Term = { + if (currpos.isDefined && currpos.get < 0) return t + if (rel(t , old, additionalContext)) { + if (currpos.isEmpty || (currpos.get == 0)) { + currpos = currpos.map(x => x - 1) + return newt + }else { + currpos = currpos.map(x => x - 1) + } + } + t match { + case Lambda(nm, tp, bd) => { + if (tmp.contains(nm)) { + val newn = pickFreshHypName(nm.toString , Context(tmp.map(x => VarDecl(x)) : _*)) + val newbd = bd.substitute(Substitution(Sub(nm , OMV(newn))))(PlainSubstitutionApplier) + val newbd0 = traverse(newbd)( additionalContext ++ VarDecl(LocalName(newn) , tp , null ) , ()) + Lambda(LocalName(newn) , tp , newbd0) + }else {Lambda(nm , tp , traverse(bd)(additionalContext ++ VarDecl(nm , tp , null) , ()) )} + } + case Pi(nm ,tp, bd) if (nm.toString != "_") => { + if (tmp.contains(nm)) { + val newn = pickFreshHypName(nm.toString , Context(tmp.map(x => VarDecl(x)) : _*)) + val newbd = bd.substitute(Substitution(Sub(nm , OMV(newn))))(PlainSubstitutionApplier) + val newbd0 = traverse(newbd)( additionalContext ++ VarDecl(LocalName(newn) , tp , null), ()) + Pi(LocalName(newn) , tp , newbd0) + }else {Pi(nm , tp , traverse(bd)(additionalContext ++ VarDecl(nm , tp , null) , ()))} + } + + case _ => Traverser(this , t) + } + } + } + + /** + * check if t is an lf-arrow or pi + * @param t + * @return + */ + def isArrowOrPi(t : Term): Boolean = t match { + case Arrow(hd , bd) => true + case Pi(_ , _ , _) => true + case _ => false + } + + /** + * if a term is a Free(context , term) then this function removes all variables in this Free which are also in ctx + * @param t + * @param ctx + * @return + */ + def remOuterFree(t : Term , ctx : Context) : Term = t match { + case Free(ctx0 , bd) => { + val newctx = ctx0.filter(p => ctx.index(p.name).isEmpty ) + if(newctx.nonEmpty) Free(newctx , bd) else bd + } + case _ => t + } + + /** + * like [[remOuterFree]] but returns the remaining variables in Free which are not also in ctx + * @param t + * @param ctx + * @return + */ + def remOuterFreeA(t : Term , ctx : Context) : (Term , List[VarDecl]) = t match { + case Free(ctx0 , bd) => { + val rems = ctx0.filter(p => ctx.index(p.name).isEmpty ) + (bd, rems) + } + case _ => (t, Nil) + } + + /** + * adds dependencies to ln by applying ctx to ln + * @param ln + * @param ctx + */ + class ExtendUnkownInTerm( ln : LocalName , ctx: Context) extends StatelessTraverser { + override def traverse(t: Term)(implicit con: Context, state: State ): Term = t match { + case Lambda(nm , tp , bd) if (nm == ln) => t + case OMA(OMV(vname) , args) if ln == vname =>{ + OMA(OMV(vname) , ctx.variables.map(x => x.toTerm).toList ++ args) + } + case OMV(vname) if ln == vname => { + OMA(OMV(vname) , ctx.variables.map(x => x.toTerm).toList ) + } + case _ => Traverser( this, t) + } + } + + /** + * removes depdendencies from unknowns + * @param ctx + */ + class Appremover(ctx : Context) extends StatelessTraverser { + override def traverse(t: Term)(implicit con: Context, state: State): Term = t match { + case OMA(OMV(ln) , args) if ctx.getO(ln).isDefined => OMV(ln) + case _ => Traverser(this , t) + } + } + + /** + * check if t contains a hole + * @param t + * @return + */ + def containsMissing(t : Term): Boolean = t match { + case Hole(_) => true + case OMID(path) => false + case OMBINDC(binder, context, scopes) => (binder :: scopes).exists(p => containsMissing(p)) + case OMA(fun, args) => (fun :: args).exists(p => containsMissing(p)) + case OMV(name) => false + case OMATTR(arg, key, value) => ??? + case tTrait: OMLITTrait => ??? + case OMLIT(value, rt) => ??? + case UnknownOMLIT(valueString, synType) => ??? + case OMFOREIGN(node) => ??? + case OMSemiFormal(tokens) => ??? + case OML(name, tp, df, nt, featureOpt) => ??? + } + + + def simpleApplyTermToTerm(ctx : Context, applicants : List[Term] , to : Term, hist : History , s : Solver): Option[(List[Goal] , Term , Term)] ={ + abstract class Param { + def getTp : Term + } + case class PPi(nm : LocalName, tp : Term) extends Param { + override def getTp: Term = tp + } + case class PArr(tp : Term) extends Param { + override def getTp: Term = tp + } + case class Const(tp : Term) extends Param { + override def getTp: Term = tp + } + + val terms = MMap[Int , Param]() + val subs = MMap[Int , Option[Term]]() + + val totp0 = s.inferType(to)(Stack(ctx), hist).getOrElse(return None) + // val apptp = inferType(applicant)(Stack(ctx), hist).getOrElse(return None) + val apptps0 = applicants.map(x => s.inferType(x)(Stack(ctx), hist).getOrElse(return None)) + val apptps = applicants.zip(apptps0) + + + class AlphaRename() extends StatelessTraverser { + // val subs = MMap[LocalName , LocalName]() + + override def apply(t: Term, con: Context): Term = t match { + case Arrow(hd , bd) => Arrow(hd , apply(bd , con)) + case Pi(nm , tp , bd) => { + if (con.variables.exists(p => p.name == nm)){ + val (newnm , sb) = Context.pickFresh(con, nm) + // if (! subs.contains(nm)) subs(nm) = newnm + // val sb = Substitution(Sub(nm , OMV(newnm))) + Pi(newnm , tp , apply(bd ^ sb , con ++ VarDecl(newnm))) + }else { + t + } + } + case _ => Traverser(this , t)(con , ()) + } + + override def traverse(t: Term)(implicit con: Context, state: this.State): Term = apply(t, con) + } + + + val totp = new AlphaRename()(totp0 , ctx) + + + def splitTerm(t : Term, pos : Int) : Int = t match { + case Arrow(hd , bd) => { + terms(pos) = PArr(hd) + splitTerm(bd , pos + 1) + } + case Pi(nm , tp , bd) => { + terms(pos) = PPi(nm , tp) + splitTerm(bd , pos + 1) + } + case _ =>{ terms(pos) = Const(t) ; pos } + } + + + + def genTerm(ls : List[Param]):Term = ls match { + case List(Const(tp)) => tp + case PArr(tp)::xs => Arrow(tp ,genTerm(xs)) + case PPi(nm , tp) :: xs => Pi(nm , tp , genTerm(xs)) + } + + + + // val maxpos = splitTerm(totp , 0) + val initlen = splitTerm(totp, 0) + def maxpos = terms.toList.length - 1 + + + def splitTermA(t : Term , pos : Int ) : Unit = { + if (pos >= initlen) {terms(initlen) = Const(t) ;return } + t match { + case Arrow(hd , bd) => { + terms(pos) = PArr(hd) + splitTermA(bd , pos + 1) + } + case Pi(nm , tp , bd) => { + terms(pos) = PPi(nm , tp) + splitTermA(bd , pos + 1) + } + case _ =>{ terms(pos) = Const(t)} + } + } + def subfrom(pos : Int , s: Substitution) = { + val tmp = terms.filter(p => p._1 >= pos).toList + val tmp0 = tmp.sortBy(x => x._1).map(x => x._2) + val t = genTerm(tmp0) ^ s + splitTermA(t , pos) + } + + def preparesubs(ls : List[(Int,Param)]): Unit = ls match { + case Nil => + case (pos , PPi(nm , tp))::xs => { + subs(pos) = None + preparesubs(xs) + } + case _::xs => preparesubs(xs) + } + + preparesubs(terms.toList) + + def traverse(pos : Int, app : List[(Term , Term)], vars : Map[LocalName , (Term ,Int)]): Boolean = { + if (pos < 0) return false + if (pos >= initlen) return subs.forall(p => p._2.isDefined) && app.isEmpty + val tm = terms(pos) + lazy val res : Option[Substitution] = if (app.isEmpty) None else { + val tmp = unifyA(ctx , app.head._2 , Context(vars.toList.map(x => VarDecl(n = x._1, tp = x._2._1)) : _*) , tm.getTp, hist, s) + tmp + // termMatcher(ctx , app.head._2 , Context(vars.toList.map(x => VarDecl(n = x._1, tp = x._2._1)) : _*) , tm.getTp) + } + (app , tm , res) match { + case (Nil , PPi(_,_), _) => false + case ((app0)::xs, PPi(nm , tp), None) => { + val newvars = vars + (nm -> (tp, pos)) + traverse(pos + 1, app, newvars) + } + // case ((app0)::xs, PPi(nm, tp) , Some((sb, ct , tt , false))) => { + // traverse(pos + 1, app , vars.updated(nm , (tp , pos))) + // } + case ((applicant,app0)::xs, PPi(nm, tp) , Some((sb))) => { + sb.foreach(f => { + var (_ , fpos) = vars(f.name) + subfrom(fpos + 1 , Substitution(f)) + if (subs(fpos).isDefined && subs(fpos).get != f.target) {return false} + subs(fpos) = Some(f.target) + }) + subfrom(pos + 1 , Substitution(Sub(nm , applicant))) + subs(pos) = Some(applicant) + // subs.forall(p => p._2.isDefined) + traverse(pos + 1 , xs , vars) + + } + case (Nil , PArr(tp) , _) => subs.forall(p => p._2.isDefined) + case (app0::xs , PArr(tp) , None) => { + traverse(pos + 1 , app , vars) + } + // case (app0::xs , PArr(tp) , Some((_ , _ , _ , false))) => { + // traverse(pos + 1 , app , vars) + // } + case ((applicant, app0)::xs , PArr(tp) , Some((sb ))) => { + sb.foreach(f => { + var (_ , fpos) = vars(f.name) + subfrom(fpos + 1 , Substitution(f)) + if (subs(fpos).isDefined && subs(fpos).get != f.target) {return false} + subs(fpos) = Some(f.target) + }) + subs(pos) = Some(applicant) + // subs.forall(p => p._2.isDefined) + traverse(pos + 1 , xs , vars) + } + case _ => subs.forall(p => p._2.isDefined) + } + } + + if (! traverse(0 , apptps , Map.empty)) return None + + def buildTermAndGoals: (List[Goal],Term) = { + + var gnames = ctx ++ s.getPartialSolution + + def loop(pos : Int) : (List[Goal],List[Term]) = { + if (pos >= initlen) return (Nil , Nil) + val tmp = terms(pos) + lazy val sb = subs.get(pos) + val (gls , tms) = loop(pos + 1) + (tmp, sb) match { + case (PPi(nm, tp), Some(Some(sbt))) => { + (gls, sbt :: tms) + } + case (PArr(tp) , None) => { + val newgname = Context.pickFresh(gnames , LocalName("", "goal")) + gnames = gnames ++ VarDecl(newgname._1) + ( Goal(tp , ctx , newgname._1) :: gls , s.Unknown(newgname._1 , ctx.variables.map(x => x.toTerm).toList) :: tms) + } + case (PArr(tp) , Some(Some(sbt))) => { + (gls , sbt :: tms) + } + case _ => (Nil , Nil) + } + + } + + val (gls , tms ) = loop(0) + val resterm = if (tms.isEmpty) to else OMA(to , tms) + (gls , resterm) + + + } + + val (gls, resterm) = buildTermAndGoals + Some(gls, resterm , terms(initlen).getTp) + } + + def makeSubgoals(context: Context, uks : Context , goal: Term, fact: Term, s : Solver): Option[Context] = { + // tp must be of the form Pi bindings.scope + val (bindings, scope) = FunType.unapply(fact).get + val (paramList, subgoalList) = bindings.span(_._1.isDefined) + // we do not allow named arguments after unnamed ones + if (subgoalList.exists(_._1.isDefined)) + return None + // we do not allow shadowed parameters + val paramNames = paramList.map(_._1) + if (paramNames.distinct.length != paramNames.length) + return None + // the free variables of scope (we drop the types because matching does not need them) + val params = FunType.argsAsContext(paramList) + // fact may contain free variables from stack.context, so make sure there are no name clashes + // sub is a renaming from unknowns to unknownsFresh + val (paramsFresh, rename) = Context.makeFresh(params, context.map(_.name)) + val scopeFresh = scope ^? rename + // match goal against scope, trying to solve for scope's free variables + // TODO using a first-order matcher is too naive in general - for the general case, we need to use the Solver + // val unifiableparams = Context(paramsFresh.map(x => x.copy(tp = x.tp.map(tpp => Free(context, tpp)))) : _ *) + val (unifiableparams0 , unifiablesub) = paramsFresh.foldLeft(Nil : List[VarDecl] , Substitution())((res , x) => { + // val newctx = Context(ctx.map(y => y.copy(df = y.df.map(z => z ^ res._2) , tp = y.tp.map(z => z ^ res._2)) ) : _ *) + val tmp = x.copy(tp = x.tp.map(tpp => Free(context, tpp ^ res._2))) + val tmpsub = Sub(x.name, if (context.isEmpty) OMV(x.name) else OMA(OMV(x.name) , context.map(x => x.toTerm))) +: res._2.subs + ( res._1 ++ List(tmp) , Substitution( tmpsub : _*)) + } ) + + val unifiableparams = Context(unifiableparams0 : _*) + // val unifiablesub = Substitution(paramsFresh.map(x => Sub(x.name, if (context.isEmpty) OMV(x.name) else OMA(OMV(x.name) , context.map(x => x.toTerm)))) : _ *) + val unifiablescope = scopeFresh ^ unifiablesub + // val unifyresult = unify(context, goal , paramsFresh ++ uks , scopeFresh,new History(Nil)) + val unifyresult0 = unify(context, goal , (unifiableparams ++ uks).filter(x => unifiablescope.freeVars.contains(x.name)) , unifiablescope,new History(Nil), s) + + val solution0 = unifyresult0 match { + case Some(subs) => subs + case None => return None + } + val solution = Substitution(solution0.subs.map(x => Sub(x.name , ProofUtil.remOuterFree(x.target , context))) : _*) + // now scope ^ rename ^ solution == goal + var result = Context() + bindings foreach {b => + // named bound variables that are substituted by solution can be filled in + // others are holes representing subgoals + val renameResult = rename ^ result.toPartialSubstitution // maps unsolved variables to their renaming + b match { + case (Some(x), xtp) => + val xFresh = (OMV(x) ^ rename).asInstanceOf[OMV].name // rename is a renaming + result ++= VarDecl(xFresh, None, Some(xtp ^? renameResult), solution(xFresh), None) + case (None, anontp) => + result ++= VarDecl(OMV.anonymous, anontp ^? renameResult) + } + } + + val ukssol = solution0.filter(p => uks.variables.exists(v => v.name == p.name)) + ukssol.foreach(x => s.solve(x.name , x.target)(new History(Nil))) + val result0 = result ^ Substitution(ukssol : _*) + Some(result0) + } + + def standAloneTypeCheck(t : Term , tp : Term , uks : Context , currctx : Context, s : Solver) = { + val cu = new CheckingUnit(None , currctx ,uks , Typing(Stack(currctx), t, tp , Some(OfType.path))) + val exslv = new Solver(s.controller , cu , s.rules) + val res = exslv.applyMain + (res , exslv.getPartialSolution) + } + + def unifyA(ctx : Context , goal : Term , params0 : Context , query : Term , hist : History, s : Solver) = { + val params = params0.filter(x => query.freeVars.contains(x.name)) + val (unifiableparams0 , unifiablesub) = params.foldLeft(Nil : List[VarDecl] , Substitution())((res , x) => { + val tmp = x.copy(tp = x.tp.map(tpp => Free(ctx, tpp ^ res._2))) + val tmpsub = Sub(x.name, if (ctx.isEmpty) OMV(x.name) else OMA(OMV(x.name) , ctx.map(x => x.toTerm))) +: res._2.subs + ( res._1 ++ List(tmp) , Substitution( tmpsub : _*)) + } ) + + val unifiableparams = Context(unifiableparams0 : _*) + val unifiablescope = query ^ unifiablesub + + val (newparams , subparams) = Context.makeFresh(unifiableparams , ctx.variables.map(_.name).toList) + val revert = subparams.map(x => (x.target.asInstanceOf[OMV].name , x.name)) + val unifier = new Solver(s.controller , CheckingUnit(None, s.constantContext , newparams, null) , s.rules ) + val ures = unifier.apply(Equality(Stack(ctx) , goal , unifiablescope ^ subparams , Some(OfType))) + + ures && unifier.getConstraints.isEmpty && unifier.getErrors.isEmpty match { + case false => None + case true => { + Some(Substitution(unifier.getPartialSolution.toPartialSubstitution.map(x => {val tmp = revert.find(p => p._1 == x.name).get ; x.copy(name = tmp._2 , target = ProofUtil.remOuterFree(x.target , ctx)) }) : _ *)) + } + } + } +} + + diff --git a/src/mmt-lf/src/info/kwarc/mmt/lf/itp/Tactic.scala b/src/mmt-lf/src/info/kwarc/mmt/lf/itp/Tactic.scala new file mode 100644 index 000000000..b2e724df5 --- /dev/null +++ b/src/mmt-lf/src/info/kwarc/mmt/lf/itp/Tactic.scala @@ -0,0 +1,53 @@ +package info.kwarc.mmt.lf.itp + +import info.kwarc.mmt.api.proving.itp.{Msg, Proof} + +/** + * this class represents a tactic + */ +trait Tactic { + /** + * method that executes the tactic + * @param p for convenience this is passed separately even though it is containt in `ip` + * @param ip the current proof manager + * @return Error of an empty message + */ + def applyToProof(p: Proof, ip: InteractiveProof): Msg + + +} + + +trait MetaTactic extends Tactic { + def execute(p : Proof , ip : InteractiveProof) : Msg +} + +trait ConcreteTactic extends Tactic { + + +} + +trait ProofChangingTactic extends ConcreteTactic { + abstract class ParamProofStateGeneration + abstract class ReturnProofStateGeneration + + var cppsg : Option[ParamProofStateGeneration] = None + var crpsg : Option[ParamProofStateGeneration] = None + + def genNewProofState() : Msg +} + +trait TermGeneratingTactic extends ProofChangingTactic { + abstract class ParamTermGeneration + abstract class ReturnTermGeneration + + var cptg : Option[ParamTermGeneration] = None + var crtg : Option[ReturnTermGeneration] = None + + def genTerm() : Msg + +} + + + + diff --git a/src/mmt-lf/src/info/kwarc/mmt/lf/itp/TacticError.scala b/src/mmt-lf/src/info/kwarc/mmt/lf/itp/TacticError.scala new file mode 100644 index 000000000..eb98a341a --- /dev/null +++ b/src/mmt-lf/src/info/kwarc/mmt/lf/itp/TacticError.scala @@ -0,0 +1,9 @@ +package info.kwarc.mmt.lf.itp + +/** this class extends the Exeptions with a custom Exeption signaling an error in the prover + * + * @param s the errormessage + */ +case class TacticError(s : String ) extends Exception { + +} \ No newline at end of file diff --git a/src/mmt-lf/src/info/kwarc/mmt/lf/itp/TacticParser.scala b/src/mmt-lf/src/info/kwarc/mmt/lf/itp/TacticParser.scala new file mode 100644 index 000000000..a46c9bbf9 --- /dev/null +++ b/src/mmt-lf/src/info/kwarc/mmt/lf/itp/TacticParser.scala @@ -0,0 +1,406 @@ +package info.kwarc.mmt.lf.itp + +import info.kwarc.mmt.api.{ErrorHandler, ErrorThrower} +import info.kwarc.mmt.api.documents.InterpretationInstructionContext +import info.kwarc.mmt.api.objects.{Context, PlainSubstitutionApplier, Stack, Term, Typing, VarDecl} +import info.kwarc.mmt.api.parser.{NotationBasedParser, ParseResult, ParsingUnit, SourceRef} +import info.kwarc.mmt.api.proving.itp.Goal +import info.kwarc.mmt.lf.itp.Tactics._ + +import scala.collection.mutable.ArrayBuffer +import scala.util.matching.Regex +import scala.util.parsing.combinator.JavaTokenParsers +import scala.util.parsing.input.{CharArrayReader, CharSequenceReader} + +/** + * class containing hard coded parser for tactics and several generic helper parser + * @param ip the proof manager, needed as an argument for concrete tactics like [[assume]] + */ +class TacticParser(val ip :InteractiveProof) extends JavaTokenParsers { + + /** + * parser representing a valid hypothesis name + */ + val hypName: Regex = "([a-z]|[A-Z])+([a-z]|[A-Z]|[0-9]|[/_])*".r + + /** + * parser representing a valid hypothesis name with a slash somewhere after the first character (usually used for explicitely named unknownws) + */ + val hypNameWithSlash : Regex = "([a-z]|[A-Z]|/)+([a-z]|[A-Z]|[0-9]|[/_])*".r + /** + * parser that matches any expression + */ + val anyExpr : Regex = ".*".r + /** + * parser that matches any expression inside of matching round brackets + */ + val anyExprBrack : Regex = "\\(.*\\)".r + /** + * parser that matches any expression in matching round brackets unless it contains keywords (currently only the keyword `in`) + */ + val anyExprBrackNoKeyWord : Parser[String] = anyExprBrack >> {s => if (s.contains("in")) {failure("should not contain keyword \"in\"")} else {success(s)} } + /** + * parser that matches an arbitrary amount of whitespace characters + */ + val spaces : Regex = """[ \n\t\s]*""".r + /** + * parser that matches at least one whitespace character + */ + val nespaces : Regex = """[ \n\t\s]+""".r + + /** + * prefents the implicit skipping of whitespaces in parser, otherwise a parser of the shape A ~ B could parse strings like AB + */ + override val skipWhitespace = false + + + /** + * parses a raw mmt term + * @param t the mmt expression + * @return the parsed term and the found unknowns + */ + def simpleTermParser(t : String) : ( Term, Context) = { + + val c = ip.slvr.controller + val nbp = c.extman.get(classOf[NotationBasedParser]).head + val cxt = ip.pr.currentState.head.ctx ++ (if (ip.mp.isDefined) Context(ip.mp.get) else Context()) + val pu = ParsingUnit(SourceRef.anonymous("interactive") , cxt , t ,InterpretationInstructionContext(ip.slvr.controller.getNamespaceMap) ) + val eh : ErrorHandler = ErrorThrower + val ParseResult(u,f,tt) = nbp(pu)(eh) + // val newmiss = u.map(x => ip.pr.getCurrentGoal.makeMiss(x.name)) + (tt, u ) + } + + /** + * parses a raw mmt term and adds unkowns to the goals of the current proof + * @param t the mmt expression + * @return the parsed term and the found unknowns + */ + def currGoalParseTerm(t : String) : ( Term, Context) = { + + val c = ip.slvr.controller + val nbp = c.extman.get(classOf[NotationBasedParser]).head + val cxt = ip.pr.currentState.head.ctx ++ (if (ip.mp.isDefined) Context(ip.mp.get) else Context()) + val pu = ParsingUnit(SourceRef.anonymous("interactive") , cxt , t ,InterpretationInstructionContext(ip.slvr.controller.getNamespaceMap) ) + val eh : ErrorHandler = ErrorThrower + val ParseResult(u,f,tt) = nbp(pu)(eh) + val Goal(g , gctx , ukn) = ip.pr.getCurrentGoal + // val newmiss = u.map(x => ip.pr.getCurrentGoal.makeMiss(x.name)) + ip.pr.update(Goal(g , gctx , ukn )) + ip.slvr.addUnknowns(u, None) + + (tt, u ) + } + + + /** + * parses a raw mmt term and adds unkowns to the goals of the current proof. This version also tries to infer types of unkowns more eagerly + * @param t the mmt expression + * @return the parsed term and the found unknowns + */ + def currGoalParseTermA(t : String) : ( Term, Context) = { + + + def newnames(ctx0 : Context, tt : Term): (Context, Term) = { + val ps = ip.slvr.getPartialSolution + var res = Context() + var restt = tt + + def loop(ctx : List[VarDecl]) : Unit = ctx match { + case Nil => + case (x::xs) => { + val (newn , subn) = Context.pickFresh(Context(xs : _ *) ++ res ++ ps , x.name) + restt = restt.substitute(subn)(PlainSubstitutionApplier) + res = res ++ x.copy(name = newn) + loop(xs) + } + } + loop(ctx0.variables.toList) + (res , restt) + } + + val c = ip.slvr.controller + val nbp = c.extman.get(classOf[NotationBasedParser]).head + val cxt = ip.pr.currentState.head.ctx ++ (if (ip.mp.isDefined) Context(ip.mp.get) else Context()) + // val uxt = ip.pr.getCurrUks.map(x => x.ln) + val pu = ParsingUnit(SourceRef.anonymous("interactive") , cxt , t ,InterpretationInstructionContext(ip.slvr.controller.getNamespaceMap) ) + val eh : ErrorHandler = ErrorThrower + val ParseResult(u0,frees,tt0) = nbp(pu)(eh) + val gl@Goal(g , gctx , ukn) = ip.pr.getCurrentGoal + + val (u,tt1) = newnames(u0,tt0) + lazy val sub = u.map(x => new ProofUtil.ExtendUnkownInTerm( x.name , gctx )) // Substitution(u.variables.map(v => Sub(v.name , gl.makeUnknown(ip.slvr , v.name))) : _*) + val tt = if (gctx.isEmpty) tt1 else sub.foldLeft(tt1)((tres , sub) => sub(tres , gctx)) // tt1.substitute(sub)(PlainSubstitutionApplier) + ip.slvr.addUnknowns(u , None) + val tmp = ip.slvr.inferType(tt , false)(Stack(ip.pr.getCurrCtx), ip.hist) // ip.slvr.asInstanceOf[ExtendedSolver].standAloneInfer(tt,u,ip.pr.getCurrCtx,ip.hist) // ip.slvr.inferType(tt , false)(Stack(ip.pr.getCurrCtx), ip.hist) //check(Typing(Stack(Context()) , tm , tp))(new History(Nil)) + val tmp1 = ip.slvr.getPartialSolution.filter(x => u.index(x.name).isDefined) + val ukres = tmp match { + case None => throw new TacticError("could not infer type of: " + ip.slvr.presentObj(tt)) + case Some(ttp) => { + val (res, ures ) = ProofUtil.standAloneTypeCheck(tt , ttp , tmp1 , ip.pr.getCurrCtx, ip.slvr) + Context(ures.map(x => if (x.df.isDefined && ProofUtil.containsMissing(x.df.get)) x.copy(df = None) else x ) : _ *) + } + } + + + ukres.foreach(x => { + if (x.df.isDefined && ! ProofUtil.containsMissing(x.df.get)) { + ip.slvr.solve(x.name , x.df.get)(ip.hist) + // val newsub = Substitution(Sub(x.name , x.df.get)) + // ttres = ttres ^ newsub + } + if (x.tp.isDefined && ! ProofUtil.containsMissing(x.tp.get)) ip.slvr.solveTyping(Typing(Stack(gctx) , x.toTerm , x.tp.get ))(ip.hist) + }) + + // val us = ip.slvr.getUnsolvedVariables + val newuks = ukres.filter(x => x.df.isEmpty) // us.variables.filter(p => u.variables.exists((x : VarDecl) => x.name == p.name)) + val newukgoals = newuks.map(v => Goal(ProofUtil.remOuterFree(v.tp.get , gctx) , ip.pr.getCurrCtx, v.name)) + ip.pr.currentState.append(newukgoals : _*) + val ukret = ukres.map(v => { + val newtp = v.tp match { + case None => None + case Some(tpp) => if (ProofUtil.containsMissing(tpp)) None else Some(tpp) + } + val newdf = v.df match { + case None => None + case Some(dff) => if (ProofUtil.containsMissing(dff)) None else Some(dff) + } + v.copy(tp = newtp , df = newdf) + }) + // val subs = Substitution( ukre : _ *) + // val ttnew = tt & subs + val ttres = ip.slvr.substituteSolution(tt) + (ttres ,ukret) + } + + + abstract class EParser[+T] extends Parser[T] { + def ?~>[A](p : => Parser[A]) : Parser[Option[A]] = { + this ~> """\s*""".r ~ p.? >> { + case ws ~ (r@Some(pr)) => if (ws.length > 0) success(r) else failure("arguments have to be separated by whitespace") + case ws ~ None => success(None) + } + } + + def ??~>[A](p : => Parser[Option[A]]) : Parser[Option[A]] = { + this ~> """\s*""".r ~ p >> { + case ws ~ (r@Some(pr)) => if (ws.length > 0) success(r) else failure("arguments have to be separated by whitespace") + case ws ~ None => success(None) + } + } + + def &~>[A](p : => Parser[A]) : Parser[A] = { + this ~> """\s+""".r ~> p + + } + + def &~[A](p : => Parser[A]) : Parser[~[T,A]] = { + this ~ """\s+""".r ~ p ^^ {case a ~ b ~ c => new ~(a , c) } + + } + + def ??~[A](p : => Parser[Option[A]]) : Parser[~[T,Option[A]]] = { + this ~ """\s*""".r ~ p >> { + case a ~ ws ~ (r@Some(pr)) => if (ws.length > 0) success(new ~(a,r)) else failure("arguments have to be separated by whitespace") + case a~ ws ~ None => success(new ~(a,None)) + } + } + + def ?~[A](p : => Parser[A]) : Parser[~[T,Option[A]]] = { + this ~ """\s*""".r ~ p.? >> { + case a ~ ws ~ (r@Some(pr)) if ws.nonEmpty => success(new ~(a,Some(pr))) + case a ~ ws ~ (Some(pr)) if (ws.length <= 0) => { + val aa = a + val prr = pr + val dbg = () + failure("arguments have to be separated by whitespace error(123)") + } + case a~ ws ~ None => success(new ~(a,None)) + } + } + + def ?~:[A](p : => Parser[A]) : Parser[~[T,Option[A]]] = { + this ~ """\s*""".r ~ p.? >> { + case a ~ ws ~ (r@Some(pr)) if ws.nonEmpty => success(new ~(a,Some(pr))) + case a ~ ws ~ (Some(pr)) if (ws.length <= 0) => { + val aa = a + val prr = pr + val dbg = () + failure("arguments have to be separated by whitespace error(123)") + } + case a~ ws ~ None => success(new ~(a,None)) + } + } + + + + def done[A](p : => Parser[A]) : Parser[A] = { + """\s*""".r ~> p <~ """\s*""".r + } + + + } + + implicit def ptoep[A](p : Parser[A]) : EParser[A] = { + new EParser[A]{override def apply(i : Input) = p.apply(i)} + } + + implicit def eliteral(s : String): EParser[String] = { + ptoep[String](literal(s)) + } + + implicit def eregex(r : Regex) : EParser[String] = { + ptoep(regex(r)) + } + + def inbalbracksOpt[A](p : => Parser[A] , initcount: Int = 0 , removeOuterBrackets : Boolean = false) : Parser[A] = { + new EParser[A]{ + override def apply(i : Input): ParseResult[A] = { + if(i.atEnd) return Failure("empty expression", i) + var curr : Char = i.first + var rest = i.rest + var oldrest = rest + while((! i.atEnd) && List(' ' , '\t' , '\n' ).contains(curr) ){ + curr = rest.first + oldrest = rest + rest = rest.rest + } + if(curr == '(' || initcount > 0) { + var bcount = initcount + {if (curr == '(') 1 else 0} + val newi : ArrayBuffer[Char] = ArrayBuffer[Char](curr) + while ((!rest.atEnd) && bcount != 0){ + curr = rest.first + oldrest = rest + rest = rest.rest + if (curr == '(') { + bcount += 1 + }else if (curr == ')'){ + bcount -= 1 + } + newi.append(curr) + + } + if(removeOuterBrackets){newi.remove(0) ; newi.remove(newi.length - 1)} + val newi0 = new CharArrayReader(newi.toArray,0) + if (rest.atEnd) oldrest = rest + p.apply(newi0) match { + case Success(result, next) => { + if (! next.atEnd) return Failure("could not parse argument", next) + else { + Success(result , rest) + } + } + case ns : NoSuccess => ns + } + }else { + val newi : ArrayBuffer[Char] = ArrayBuffer[Char](curr) + while((! rest.atEnd) && ! List(' ' , '\t' , '\n' ).contains(curr)){ + curr = rest.first + oldrest = rest + rest = rest.rest + if (! List(' ' , '\t' , '\n' ).contains(curr)) newi.append(curr) + } + if (rest.atEnd) oldrest = rest + val newi0 = new CharArrayReader(newi.toArray,0) + p.apply(newi0) match { + case Success(result, next) => { + if (! next.atEnd) return Failure("could not parse argument", next) + else { + Success(result , oldrest) + } + } + case ns : NoSuccess => ns + } + } + } + } + } + + + def multiTacticPA : Parser[Tactic] = { + new EParser[Tactic] { + override def apply(in: Input): ParseResult[Tactic] = { + val src = in.source.toString + val strs = src.split(";") + Success(multiTactic(strs.toList, TacticParser.this) , new CharSequenceReader("", 0)) + } + } + } + + def useP : Parser[Tactic] = ("use" &~> inbalbracksOpt(anyExpr)) ^^ {h => { val tmp = currGoalParseTermA(h) ; use(tmp._1 , tmp._2)}} + def assumeP : Parser[Tactic] = ("assume"| "asm") ?~> hypName ^^ {h => assume(h)} + + def letP : Parser[Tactic] = "let" &~> hypName &~ ( anyExprBrack | hypName ) ^^ {case h ~ t => let(h , currGoalParseTermA(t))} + + + def applyP : Parser[Tactic] = ( "apply" | "app") &~> hypName &~ rep1sep( inbalbracksOpt(anyExpr), nespaces) ^^ {case h ~ ls => applyT(h, ls.map(s => currGoalParseTermA(s)))} + + def subproofP : Parser[Tactic] = "subproof" &~> hypName &~( hypName| anyExprBrack ) ^^ {case h ~ t => subproof(h , currGoalParseTermA(t))} + def preferP : Parser[Tactic] = "prefer" &~> decimalNumber ^^ (d => prefer(d.toInt)) + def backwardP : Parser[Tactic] = ("bwd" | "backward") &~> anyExpr ^^ {ex =>backward(currGoalParseTermA(ex)) } + def fixP : Parser[Tactic] = ("fix") ?~> hypName ^^ {h => fix(h) } + // def undoP : Parser[Tactic] = "undo" ^^ {x => undo()} + + def unfoldArgsP : Parser[Option[String] ~ Option[String]] = { + val opt1 = "in" &~> hypName + val opt2 = "at" &~> decimalNumber + ( opt1 ?~ opt2 >> {case x ~ y => success(new ~(Some(x) , y))} | opt2 >> {y => success(new ~(None, Some(y)))}) + } + + // def unfoldP: Parser[Tactic] = ("unfold" | "unf" ) &~> hypName ?~ ("in" &~> hypName)^^ {case x ~ in => unfold(x,in)} + def unfoldP: Parser[Tactic] = ("unfold" | "unf" ) &~> hypName ?~ unfoldArgsP ^^ {case x ~ Some(in ~ at) => unfold(x,in,at) ; case x ~ None => unfold(x,None, None)} + def deleteP : Parser[Tactic] = ("delete" | "del") &~> hypName ^^ {x => delete(x)} + + def multiTacticP : Parser[Tactic] = rep1sep("""[^;]*""".r , ";") ^^ {ls =>multiTactic(ls, this) } + + // def addunknownP : Parser[Tactic]= ("aduk" | "addunkown") &~> hypName ^^ {x => addunknown(x)} + // def setunkownP : Parser[Tactic] = ("setuk" | "setunkown") &~> hypNameWithSlash &~ ( hypNameWithSlash| anyExprBrack ) ^^ {case h ~ t => setunkown(h , currGoalParseTermA(t))} + def voidP : Parser[Tactic] = "void" ^^ {x => void()} + def ignoreP : Parser[Tactic] = "ignore" ^^ {x => ignore()} + def messageP : Parser[Tactic] = "message" &~> anyExprBrack ^^ {exp => message(exp)} + + def simpArgsP : Parser[Option[String] ~ Option[String]] = (((anyExprBrackNoKeyWord &~ ("in" &~> hypName)) >> {case a ~ b => success(new ~(Some(a) , Some(b))) }) | (failure("").? ~ ("in" &~> hypName) >> {case None ~ b => success(new ~(None.asInstanceOf[Option[String]], Some(b)))}) | (anyExprBrackNoKeyWord >> {m => success(new ~(Some(m) , None))}) ) + def simpP : Parser[Tactic] = "simp" ?~> simpArgsP ^^ {case Some(Some(e) ~ x) => simp(Some(currGoalParseTermA(e)) , x); case Some(None ~ x) => simp(None , x) ; case None => simp(None, None)} + // def tryP : Parser[Tactic] = "try" &~> "(" ~> parseSingleTactic <~ ")" ^^ {t => Try(t)} + def repeatP : Parser[Tactic] = ("repeat" | "rep" ) &~> decimalNumber &~ ("(" ~> parseSingleTactic <~ ")") ^^ {case d ~ t => repeat(Some(d.toInt) , t)} + def applytoP : Parser[Tactic] = ("applyto" | "apt") &~> repsep(decimalNumber , ":") &~ ("(" ~> parseSingleTactic <~ ")") ^^ {case ls ~ t => applyto(ls.map(_.toInt) , t )} + def revertP : Parser[Tactic] = ("rev" | "revert") &~> rep1sep(hypName , whiteSpace) ^^ {ls => revert(ls)} + + def fixsP : Parser[Tactic] = "fixs" ?~> rep1sep(hypName , nespaces) ^^ {x => fixs(x)} + def gettypeP : Parser[Tactic] = "gettype" &~> """.*""".r ^^ {x => val tmp = simpleTermParser(x) ; gettype(tmp._1 ,tmp._2)} + def gettyperawP : Parser[Tactic] = "gettyperaw" &~> """.*""".r ^^ {x => val tmp = simpleTermParser(x) ; gettyperaw(tmp._1 ,tmp._2)} + def printrawP : Parser[Tactic] = "printraw" &~> """.*""".r ^^ {x => val tmp = simpleTermParser(x) ; printraw(tmp._1)} + def buildP : Parser[Tactic] = "build" &~> """.*""".r ^^ {x => val tmp = simpleTermParser(x) ; build(tmp._1 , tmp._2)} + def forwardP : Parser[Tactic] = ("fwd" | "forward") &~> hypName &~ inbalbracksOpt(anyExpr) &~ rep(inbalbracksOpt(anyExpr)) ^^ {case h ~ x ~ ls => val tmp = currGoalParseTermA(x); val tmps = ls.map(y => currGoalParseTermA(y)); forward(h , tmp._1 , tmp._2, tmps) } + + + /** + * list containing all available parser + */ + lazy val newTactics : List[Parser[Tactic]] = ip.slvr.rules.getOrdered(classOf[InteractiveTacticParseRule]).map(_.parseTactic(this)).map(x => remws(x)) + lazy val allTactics0 : List[Parser[Tactic]] = (List(fixP, fixsP, simpP ,assumeP, useP, letP, applyP, backwardP , preferP , voidP , messageP , subproofP , unfoldP , ignoreP, deleteP , repeatP , applytoP, gettypeP, gettyperawP, printrawP, buildP , forwardP)).map(x => remws(x)) ++ newTactics // ++ newTactis.map(x => x.tacticParserGenerator(ip).asInstanceOf[Parser[Tactic]])).map(x => remws(x)) + lazy val allTactics : List[Parser[Tactic]] = allTactics0.map(x => x <~ not(".*")) + /** + * removes/skips the left/rightmost whitespace from an expression(needed since whitepsace isn't skipped by default) + * @param p the concrete parser + * @tparam A + * @return parser without the outmost whitespaces + */ + def remws[A](p : Parser[A]) = spaces ~> p <~ spaces + + + /** + * Parser that goes though all available tactics-parser an tries all until one doesn't fail. Fails otherwise + * @return the succseeding parser + */ + def parseSingleTactic : Parser[Tactic] = { + + // the inner `loop` of the function + def parseSingelTacticL(ls : List[Parser[Tactic]]) : Parser[Tactic] = ls match { + case List() => failure("no tactic found") + case x::xs => (x ||| parseSingelTacticL(xs)) + } + + parseSingelTacticL(allTactics) + } +} \ No newline at end of file diff --git a/src/mmt-lf/src/info/kwarc/mmt/lf/itp/TacticRule.scala b/src/mmt-lf/src/info/kwarc/mmt/lf/itp/TacticRule.scala new file mode 100644 index 000000000..072d6b3a4 --- /dev/null +++ b/src/mmt-lf/src/info/kwarc/mmt/lf/itp/TacticRule.scala @@ -0,0 +1,35 @@ +package info.kwarc.mmt.lf.itp + +import info.kwarc.mmt.api.{LocalName, Rule} +import info.kwarc.mmt.api.objects.{OMID, OMV, Term} +import info.kwarc.mmt.api.symbols.Constant +import info.kwarc.mmt.api.uom.ConstantScala + + +trait TokenTrait { + def toTactic : TacticTrait +} + +trait TacticTrait extends Constant with Tactic { + +} + +/** + * class representing not hardcoded tactics + */ +abstract class TacticRule extends Rule { + + + // type TT = TokenTrait + + /** + * a tactic token is an intermediate representation of a tactic. The difference is that a tactic token has still + * unparsed raw mmt strings in it + */ + + // val mmtTactic : T + def ConcreteTacticParser : TacticParser#Parser[TacticTrait] + + + +} diff --git a/src/mmt-lf/src/info/kwarc/mmt/lf/itp/Tactics/InteractiveTacticParseRule.scala b/src/mmt-lf/src/info/kwarc/mmt/lf/itp/Tactics/InteractiveTacticParseRule.scala new file mode 100644 index 000000000..8d0a17fae --- /dev/null +++ b/src/mmt-lf/src/info/kwarc/mmt/lf/itp/Tactics/InteractiveTacticParseRule.scala @@ -0,0 +1,8 @@ +package info.kwarc.mmt.lf.itp.Tactics + +import info.kwarc.mmt.api.Rule +import info.kwarc.mmt.lf.itp.{Tactic, TacticParser} + +trait InteractiveTacticParseRule extends Rule { + def parseTactic(tp : TacticParser) : tp.Parser[Tactic] +} diff --git a/src/mmt-lf/src/info/kwarc/mmt/lf/itp/Tactics/Tactics.scala b/src/mmt-lf/src/info/kwarc/mmt/lf/itp/Tactics/Tactics.scala new file mode 100644 index 000000000..f5884c6ed --- /dev/null +++ b/src/mmt-lf/src/info/kwarc/mmt/lf/itp/Tactics/Tactics.scala @@ -0,0 +1,736 @@ +package info.kwarc.mmt.lf.itp.Tactics + +import info.kwarc.mmt.api.LocalName +import info.kwarc.mmt.api.objects.{Context, Equality, Free, OMID, OMV, PlainSubstitutionApplier, Stack, Sub, Substitution, Term, Typing, VarDecl} +import info.kwarc.mmt.api.proving.itp.ProofUtil.standAloneInfer +import info.kwarc.mmt.api.proving.itp.{Goal, HasError, Msg, NoMsg, Proof, WarningMsg} +import info.kwarc.mmt.lf.itp.{InteractiveProof, ProofUtil, Tactic, TacticError, TacticParser} +import info.kwarc.mmt.lf.itp.ProofUtil.{Appremover, makeSubgoals} +import info.kwarc.mmt.lf.{Apply, ApplySpine, Arrow, Lambda, Pi} + + +/** + * takes unnamed hypothesis from the goal an puts them in the local context + * @param hs optional names for the newly introduced hypothesis + */ +case class assume(hs : Option[String]) extends Tactic { + override def applyToProof(p: Proof, ip: InteractiveProof): Msg = { + val Goal(g, ctx, ukn ) = p.currentState.head + g match { + case Arrow(h, t) => { + val old = p.currentState.remove(0) + val newname = ProofUtil.pickFreshHypName(hs.getOrElse("h") , ctx) + val newh = VarDecl(LocalName(newname) ,tp = h) + p.currentState.insert(0, Goal(t , ctx ++ newh, ip.pr.getNewGoalName()) ) + if (!ip.testrun) genTerm(old , newname , h , t , ip) + NoMsg() + } + case _ => HasError("assume has to be applied to a goal of the form a -> b") + } + } + + /** + * update the proof terms + * @param old old goal + * @param s hypotehsis name + * @param tp type of new hypothesis + * @param bd new goal + * @param ip + */ + def genTerm( old : Goal , s : String, tp : Term ,bd : Term ,ip : InteractiveProof) = { + val g : Goal = ip.pr.getCurrentGoal + ip.slvr.addUnknowns(Context(VarDecl(LocalName(g.ukname) , Free(g.ctx , bd) , null)) , None) + val newl = Lambda( Context(VarDecl(LocalName(s) , tp ,null )) , g.makeUnknown(ip.slvr , g.ukname)) + ip.slvr.solve(old.ukname , Free( old.ctx ,newl)) (ip.hist) + ip.pr.updateGoalProofTerm(old.ukname , Lambda( Context(VarDecl(LocalName(s) , tp ,null )) , OMV(g.ukname))) + } +} + +/** + * solves a goal + * @param t term to used the first goal in [[Proof.currentState]] + * @param uks newly introced unknowns + */ +case class use(t : Term, uks : Context) extends Tactic { + override def applyToProof(p: Proof, ip: InteractiveProof): Msg = { + val sol = ip.slvr.getSolvedVariables + if (uks.variables.exists(p => ! sol.contains(p.name))) return HasError("the term" + ip.slvr.presentObj(t) + " must not contain unkowns/holes") + val res = ip.slvr.check(Typing(Stack(p.getCurrCtx) , t , p.getCurrentConc))(ip.hist) + if (res) { + val old = p.currentState.remove(0) + if(!ip.testrun) genTerm(old, t , ip) + NoMsg() + }else { + HasError("term " + ip.slvr.presentObj(t) + " is not the same type as the goal") + } + } + + /** + * updates the proof terms + * @param old old goal + * @param t + * @param ip + */ + def genTerm(old : Goal , t : Term , ip : InteractiveProof) = { + ip.slvr.solve(old.ukname , Free(old.ctx , t))(ip.hist) + ip.pr.updateGoalProofTerm(old.ukname ,t ) + } +} + +/** + * adds hypothesis to local goal context + * @param h hypothesis name + * @param tup tuple consisting of the term to add to the context and the unknown it introduces + */ +case class let(h : String , tup : (Term,Context) ) extends Tactic { + val (t , unk) = tup + override def applyToProof(p: Proof, ip: InteractiveProof): Msg = { + val currg@Goal(g , ctx , ukn) = p.currentState.head + // val sub = Substitution(unk.map(v => Sub(v.name, currg.makeUnknown(ip.slvr , (v.name)))) : _*) + // val newt = t.substitute(sub)(PlainSubstitutionApplier) + val newhtp0 = ip.slvr.inferType(t , false)(Stack(ctx) , ip.hist) + if (newhtp0.isEmpty) return HasError("error in let tactic: Could not infer the type of " + t.toString) + val old = p.currentState.remove(0) + val newh = ProofUtil.pickFreshHypName(h , ctx) + // val newunk : Substitution = Substitution(unk.map(v => Sub(v.name, old.makeUnknown(ip.slvr , (v.name)))) : _*) + val newhtp = newhtp0.get // .substitute(newunk)(PlainSubstitutionApplier) + p.currentState.insert(0,Goal(g, ctx ++ VarDecl(LocalName(newh) , newhtp ) , ip.pr.getNewGoalName())) + genTerm(old, LocalName(newh), newhtp, t , ip) + ip.pr.addukdeps(unk, ukn, LocalName(newh)) + NoMsg() + } + + /** + * update the proof terms + * @param old + * @param hname + * @param tp + * @param ref + * @param ip + */ + def genTerm(old : Goal, hname : LocalName , tp : Term, ref : Term , ip : InteractiveProof ) = { + + // val revisedtp = unk.variables.foldLeft(tp)((res ,v) => res.substitute(Sub(v.name, Free(old.ctx , OMV(v.name))))(PlainSubstitutionApplier)) + val g = ip.pr.getCurrentGoal + val gname = ip.pr.getCurrentGoal.ukname + val newlam = Apply (Lambda(hname , tp , g.makeUnknown(ip.slvr , gname) ) , ref) + ip.slvr.addUnknowns(Context(VarDecl(gname , Free(g.ctx , g.g) , null)) , None) + ip.slvr.solve(old.ukname , Free(old.ctx , newlam))(ip.hist) + ip.pr.updateGoalProofTerm(old.ukname, Apply (Lambda(hname , tp , OMV(gname) ) , ref)) + } +} + + +/** + * applies a term to a hypothesis + * @param h + * @param lstup + */ +case class applyT(h : String , lstup : List[(Term, Context)] ) extends Tactic { + val ls = lstup.map(_._1) + + override def applyToProof(p: Proof, ip: InteractiveProof): Msg = { + val c = p.getCurrentGoal.ctx.getO(h) + c match { + case None => HasError("no hypothesis named " + h + " found") + case Some(vd@VarDecl(nm, _, tp, _, _)) => { + val tmp = vd.toTerm + val tmp0 = ip.slvr.inferType(ApplySpine(tmp, ls: _*))(Stack(ip.pr.getCurrentGoal.ctx), ip.hist) + tmp0 match { + case None => HasError("could not apply " + ls.toList + " to " + h) + case Some(newtp) => { + val newctx0 = ip.pr.getCurrCtx.filter(x => x.name != LocalName(h)) + val hyp = ip.pr.getCurrCtx(LocalName(h)) + val newhyp = VarDecl(hyp.name, hyp.feature, tmp0, hyp.df, hyp.not) + val newctx = Context(newctx0 : _*) ++ newhyp + val newG = Goal(ip.pr.getCurrentConc, newctx, ip.pr.getNewGoalName()) + val old = ip.pr.getCurrentGoal + ip.pr.update(newG) + genTerm(old , LocalName(h) , newtp , ls , ip) + NoMsg() + } + } + } + } + + } + + /** + * update the proof terms + * @param old + * @param ln + * @param tp + * @param ctx + * @param ip + */ + def genTerm(old : Goal , ln : LocalName, tp : Term , ctx : List[Term] , ip : InteractiveProof) = { + val g = ip.pr.getCurrentGoal + val newLam = Apply(Lambda( ln , tp , g.makeUnknown(ip.slvr , g.ukname)) , (ApplySpine(OMV(ln) , ctx : _*))) + val newLamA = Apply(Lambda( ln , tp , OMV(g.ukname)) , (ApplySpine(OMV(ln) , ctx : _*))) + ip.slvr.addUnknowns(VarDecl(g.ukname , Free(g.ctx, g.g) , null) , None) + ip.slvr.solve(old.ukname , Free(old.ctx , newLam ))(ip.hist) + ip.pr.updateGoalProofTerm(old.ukname, newLamA) + } +} + + +/** + * performs a backward step + * @param tup + */ +case class backward(tup : (Term, Context)) extends Tactic { + val (t, unk) = tup + val unks = unk.filter(p => p.df.isDefined) + val unku = unk.filter(p => p.df.isEmpty) + + def mergeVarWithG(ctx : List[VarDecl] , gls : List[Goal] ) : List[(VarDecl , Option[Goal])] = (ctx , gls) match { + case (Nil , Nil) => Nil + case (x :: xs , ys) if x.df.isDefined => (x , None) :: mergeVarWithG(xs , ys) + case (x :: xs , y :: ys) => (x , Some(y)) :: mergeVarWithG(xs , ys) + case _ => throw new TacticError("internal error in backward tactic during unification: #goals <> #unsolved variables " ) + } + + override def applyToProof(p: Proof, ip: InteractiveProof): Msg = { + val Goal(g,gctx, guks) = p.getCurrentGoal + + val htp = ip.slvr.inferType(t)(Stack(gctx), ip.hist) + if (htp.isEmpty) return HasError("could not infer the type of " + t.toString) + val makegs = try {makeSubgoals(gctx , unku , g , htp.get , ip.slvr).get} catch {case e => return HasError("could not unify goal") } + val hs = makegs.filter(p => p.df.isEmpty) + val solved = makegs.filter(p => p.df.isDefined) + // val (hs , c) = ProofUtil.splitConcHyps(htp.get) + // if(ip.slvr.check(Equality(Stack(gctx) , c , g, None))(ip.hist)){ + val old = p.currentState.remove(0) + val newgls = hs.map(x => Goal(x.tp.get, gctx, ip.pr.getNewGoalName() )) + p.currentState.insertAll(0, newgls) + genTerm(old, t, mergeVarWithG(makegs.variables.toList , newgls ) , newgls , ip) + NoMsg() + // } + // HasError("could not unify goal with conclusion") + } + + def genTerm(old : Goal , t : Term, params : List[(VarDecl , Option[Goal])] , newgls : List[Goal] , ip : InteractiveProof ) = { + + val newlam = ApplySpine( t , params.map(x => if (x._1.df.isEmpty) {old.makeUnknown(ip.slvr , x._2.get.ukname)} else {x._1.df.get} ) : _* ) + val newlamA = ApplySpine( t , params.map(x => {if (x._1.df.isEmpty) {OMV(x._2.get.ukname)} else {x._1.df.get}}) : _* ) + ip.slvr.addUnknowns(Context(newgls.map(x => VarDecl(x.ukname , Free(x.ctx, x.g) , null)) : _*) , None) + ip.pr.updateGoalProofTerm(old.ukname , newlamA) + ip.slvr.solve(old.ukname , Free(old.ctx , newlam))(ip.hist) + + + } +} + + +/** + * introduce a pi to the local context + * @param hs + */ +case class fix(hs : Option[String]) extends Tactic { + override def applyToProof(p: Proof, ip: InteractiveProof): Msg = { + val Goal(g, ctx, uks ) = p.currentState.head + g match { + case Pi(nmm , nmtp, bd) => { + val nm = if (nmm.toString == "_") LocalName(ProofUtil.pickFreshHypName("h" , ip.pr.getCurrCtx)) else nmm + val old = p.currentState.remove(0) + val newname = ProofUtil.pickFreshHypName(hs.getOrElse(nm.toString) , ctx) + val newh = VarDecl(LocalName(newname) ,tp = nmtp) + val newctx = ctx ++ newh + val newg =bd.substitute(Substitution(Sub(nm , OMV(newname))))(PlainSubstitutionApplier) + p.currentState.insert(0, Goal(newg , newctx, ip.pr.getNewGoalName()) ) + // val tmp = newctx ++ VarDecl(LocalName("c")) + if(!ip.testrun) genTerm(old , newname , nmtp, ip ) + NoMsg() + } + case _ => HasError("fix has to be applied to a goal of the form `{a} b` or `a -> b`") + } + } + def genTerm( old : Goal , s : String, tp : Term ,ip : InteractiveProof) = { + val g : Goal = ip.pr.getCurrentGoal + ip.slvr.addUnknowns(Context(VarDecl(LocalName(g.ukname) , Free(g.ctx , g.g) , null)) , None) + val newl = Lambda( Context(VarDecl(LocalName(s) , tp ,null )) , g.makeUnknown(ip.slvr , g.ukname)) + ip.slvr.solve(old.ukname , Free( old.ctx ,newl)) (ip.hist) + ip.pr.updateGoalProofTerm(old.ukname , Lambda( Context(VarDecl(LocalName(s) , tp ,null )) , OMV(g.ukname))) + } + +} + +/** + * introduce multiple PIs to the local context + * @param hss0 + */ +case class fixs(hss0 : Option[List[String]]) extends Tactic { + override def applyToProof(p: Proof, ip: InteractiveProof): Msg = { + def loop(hss : Option[List[String]]) : Msg = { + val c = p.getCurrentConc + val pora = ProofUtil.isArrowOrPi(c) + + + hss match { + case None if pora => fix(None).applyToProof(p, ip) match { + case r@HasError(s) => r + case r@WarningMsg(s) => { + r.combineMsg(loop(None)) + } + case NoMsg() => loop(None) + } + case None => NoMsg() + case Some(x :: xs) if pora => fix(Some(x)).applyToProof(p, ip) match { + case HasError(s) => HasError(s) + case r@WarningMsg(s) => r.combineMsg(loop(Some(xs))) + case NoMsg() => loop(Some(xs)) + } + case Some(Nil) => NoMsg() + case Some(x :: xs) => WarningMsg("more names for hypothesis supplied then needed") + } + } + loop(hss0) + } +} + + +/** + * start a new subproof + * @param h + * @param tup + */ +case class subproof(h : String , tup : (Term, Context)) extends Tactic{ + val (t, unk) = tup + override def applyToProof(p: Proof, ip: InteractiveProof): Msg = { + val Goal(g, ctx, uks) = p.getCurrentGoal + val newh = ProofUtil.pickFreshHypName(h ,p.getCurrCtx) + val old = p.getCurrentGoal + p.update(Goal(g, ctx ++ VarDecl(LocalName(newh) , None , Some(t) , None, None), ip.pr.getNewGoalName())) + p.currentState.insert(0 , Goal(t, ctx, ip.pr.getNewGoalName())) + genTerm( old , p.currentState(1) , LocalName(newh) , t , ip ) + NoMsg() + } + + def genTerm(old : Goal , updatedgoal : Goal , ln: LocalName ,tp : Term , ip :InteractiveProof) = { + val g = ip.pr.getCurrentGoal + val newlamA = Apply(Lambda( ln , tp , OMV(updatedgoal.ukname) ) , OMV(g.ukname)) + val newlam = Apply(Lambda( ln , tp , updatedgoal.makeUnknown(ip.slvr , updatedgoal.ukname) ) , g.makeUnknown(ip.slvr,g.ukname)) + ip.slvr.addUnknowns(Context(VarDecl(updatedgoal.ukname , Free(updatedgoal.ctx , updatedgoal.g) , null) , VarDecl(g.ukname , Free(g.ctx, g.g) , null)) , None) + ip.slvr.solve(old.ukname , Free(old.ctx , newlam))(ip.hist) + ip.pr.updateGoalProofTerm(old.ukname , newlamA) + } +} + +/** + * changes the order of goals by putting the ith goal first + * @param i + */ +case class prefer(i : Int) extends Tactic{ + override def applyToProof(p: Proof, ip: InteractiveProof): Msg = { + (ip.pr.currentState.length < i, i < 0) match { + case (true, _) => HasError("the index for the prefer tactic is larger then the number of available goals (counting starts from zero)") + case (_ , true) => HasError("the index for the prefer tactic has to be a positive number") + case _ => { + val pg = ip.pr.currentState.remove(i) + ip.pr.currentState.insert(0,pg) + NoMsg() + } + } + } +} + +case class repeat(n : Option[Int] , t : Tactic) extends Tactic { + override def applyToProof(p: Proof, ip: InteractiveProof): Msg = ??? +} + + +case class applyto(n : List[Int] , t : Tactic) extends Tactic{ + override def applyToProof(p: Proof, ip: InteractiveProof): Msg = ??? +} + +case class revert(h : List[String]) extends Tactic { + override def applyToProof(p: Proof, ip: InteractiveProof): Msg = ??? +} + +case class autostep() { + +} + +/* +case class undo() extends Tactic { + override def applyToProof(p: Proof, ip: InteractiveProof): Msg = { + if(ip.history.isEmpty) { + WarningMsg("no undo possible") + }else{ + ip.undo + NoMsg() + } + } +} +*/ + +/** + * unfolds a definiition + * @param h + * @param target + * @param pos + */ +case class unfold(h : String, target : Option[String] , pos : Option[String]) extends Tactic{ + override def applyToProof(p: Proof, ip: InteractiveProof): Msg = { + val poss = pos.map(s => s.toInt) + val Goal(g , gctx, guks) = ip.pr.getCurrentGoal + val prs = new TacticParser(ip) + val (t ,unk) = prs.currGoalParseTerm(h) + if (unk.nonEmpty) return HasError("term to unfold contains unknowns , which it should not") + val res = t match { + case omid : OMID => { + ip.slvr.getDef(omid.path.toMPath.toGlobalName)(ip.hist) match { + case None => return HasError("could not find definition for " + omid.toString) + case r@Some(_) => r + } + } + case omv : OMV => { + gctx.getO(omv.name) match { + case None => None + case Some(dd) => Some(dd.df.getOrElse( return HasError("could not find definition for " + dd.name.toString))) + } + } + case _ => None + } + val newg = (res,target) match { + case (None, _) => return HasError("identifier " + h + " has no definition to unfold") + case (Some(df), None) => { + val gg = new ProofUtil.SubTraverser(t, df , ((x , y , addc) => x == y ), poss).traverse(g)(p.getCurrCtx, ()) // ProofUtil.substitute(g, t , df, ((x , y , addc) => x == y ) ) + Goal(gg, gctx , guks) + } + case (Some(df), Some(tg)) => { + if (gctx.getO(tg).isEmpty) return HasError("no such hypothesis named " + tg) + val newctx = gctx.map(x => { + if(x.name == LocalName(tg)) { + val newtp = new ProofUtil.SubTraverser(t, df , ((x , y , addc) => x == y ) , poss).traverse(x.tp.get)(p.getCurrCtx, ()) /// ProofUtil.substitute(x.tp.get, t , df, ((x , y , addc) => x == y ) ) + x.copy(tp = Some(newtp)) + } else x + }) + Goal(g , newctx, guks) + } + } + ip.pr.update(newg) + NoMsg() + } +} + +/** + * delete a hypothesis from the local context + * @param h + */ +case class delete(h : String) extends Tactic { + override def applyToProof(p: Proof, ip: InteractiveProof): Msg = { + val old@Goal(g, gctx, guks) = p.getCurrentGoal + val gtmp = g.freeVars + if (gtmp.contains(LocalName(h))) return HasError("hypothesis " + h + " is used in conclusion") + val tmpctx = gctx.filter(p => p.name != LocalName(h)) + tmpctx.foreach(p => { + val dff = p.df.map(t => t.freeVars).getOrElse(Nil) + val tpf = p.tp.map(t => t.freeVars).getOrElse(Nil) + if (dff.contains(LocalName(h))) return HasError(h + " is used in definition of " + p.name) + if (tpf.contains(LocalName(h))) return HasError(h + " is used in type of " + p.name) + }) + val newgname = p.goalcounter + val newg = Goal(g, Context(tmpctx : _*), guks) + p.update(newg) + genTerm() + NoMsg() + } + + + def genTerm() = { + + } +} +/* +case class Try(t : Tactic) extends Tactic { + override def applyToProof(p: Proof, ip: InteractiveProof): Msg = { + try { + ip.saveCurrState + val res = t.applyToProof(p,ip) + res match { + case NoMsg() => NoMsg() + case WarningMsg(_) => res + case HasError(s) => { + ip.undo + WarningMsg(s) + } + } + } + catch { + case e => { + ip.undo + WarningMsg(e.toString) + } + } + } +} + + */ + +/* + +case class setunkown(h : String , tup : ( Term, Context)) extends Tactic { + val (t, _) = tup + override def applyToProof(p: Proof, ip: InteractiveProof): Msg = { + val g@Goal(gl , ctx , uks) = p.getCurrentGoal + val uk = uks.filter(x => x.ln.name.toString == h) + uk match { + case Nil => WarningMsg("setunkown: no such unkown " + h) + case (x::Nil) => { + val tmp = ip.slvr.check(Equality(Stack(ip.pr.getCompleteCtx) ,x.toUnkown , t, None))(ip.hist) + if (tmp) {NoMsg()} else {HasError("setunkown: could not set " + h + " to " + t.toString)} + } + } + } +} + +*/ + +/** + * skip the currently focused proof + */ +case class ignore() extends Tactic { + override def applyToProof(p: Proof, ip: InteractiveProof): Msg = { + ip.pr.currentState.remove(0) + WarningMsg("ignoring current goal, skipping it without proof") + } +} + + +/** + * execute multiple tactics in a sequence + * @param ls + * @param tp + */ +case class multiTactic(ls : List[String] , tp : TacticParser) extends Tactic { + override def applyToProof(p: Proof, ip: InteractiveProof): Msg = { + + def loop(lss : List[String]): Msg = lss match { + case Nil => NoMsg() + case x :: xs => { + val tmp = tp.parseAll(tp.parseSingleTactic, x) + tmp.getOrElse(return HasError(tmp.toString)).applyToProof(p, ip) match { + case NoMsg() => p.updateUnknowns(ip.slvr) ; loop(xs) + case m@WarningMsg(s) => { + p.updateUnknowns(ip.slvr) + m.combineMsg(loop(xs)) + } + case m@HasError(s) => m + } + } + } + loop(ls) + } +} + + +/** + * simplifies terms + * @param tup + * @param h + */ +case class simp(tup : Option[(Term,Context)], h : Option[String]) extends Tactic { + lazy val Some((t,cc)) = tup + override def applyToProof(p: Proof, ip: InteractiveProof): Msg = { + lazy val res = ip.slvr.simplify(t)(Stack(ip.pr.getCurrCtx) , ip.hist) + val g@Goal(gg , ctx, uks) = ip.pr.getCurrentGoal + (h,tup.isDefined) match { + case (None,false) => { + val newg = ip.slvr.simplify(gg)(Stack(ip.pr.getCurrCtx) , ip.hist) + ip.pr.update(Goal(newg , ctx , uks)) + NoMsg() + } + case (None,true) => { + val rep = ProofUtil.substitute(gg , t , res, ((x,y,addc) => ip.slvr.currentStateObj.dryRunAllowErrors(ip.slvr.check(Equality(Stack(ctx ++ addc) , x , y, None)) (ip.hist)))) + ip.pr.update(Goal(rep , ctx, uks)) + NoMsg() + } + case (Some(nm),true) => { + if (ctx.getO(nm).isEmpty) return HasError("no such hypothesis named " + nm) + val newctx = ctx.map(x =>{ + if (x.name.toString == nm ){ + val newtp = ProofUtil.substitute(x.tp.get , t , res, ((x,y,addc) => ip.slvr.currentStateObj.dryRunAllowErrors(ip.slvr.check(Equality(Stack(ctx ++ addc) , x , y, None)) (ip.hist)))) + x.copy(tp = Some(newtp)) + }else { + x + } + }) + ip.pr.update(Goal(gg, newctx, uks )) + NoMsg() + } + case (Some(nm),false) => { + if (ctx.getO(nm).isEmpty) return HasError("no such hypothesis named " + nm) + + val newctx = ctx.map(x =>{ + if (x.name.toString == nm ){ + val simptp = ip.slvr.simplify(x.tp.get)(Stack(ip.pr.getCurrCtx) , ip.hist) + x.copy(tp = Some(simptp)) + }else { + x + } + }) + ip.pr.update(Goal(gg, newctx, uks )) + NoMsg() + } + } + } +} + + + +case class fold(t : Term) extends Tactic { //fold a term back into a name + override def applyToProof(p: Proof, ip: InteractiveProof): Msg = {???} +} + +case class addunknown(u : String) extends Tactic { + override def applyToProof(p: Proof, ip: InteractiveProof): Msg = { + val Goal(g , ctx, uks ) = p.getCurrentGoal + ip.slvr.addUnknowns(Context(VarDecl(LocalName(u))), None ) + // p.update(Goal(g , ctx , (p.getCurrentGoal.makeMiss(LocalName(u))) :: uks )) + NoMsg() + } +} + + +/** + * does nothing, useful for debugging + */ +case class void() extends Tactic { + override def applyToProof(p: Proof, ip: InteractiveProof): Msg = { + NoMsg() + } +} + +/** + * prints a message + * @param s + */ +case class message(s : String) extends Tactic { + override def applyToProof(p: Proof, ip: InteractiveProof): Msg = { + WarningMsg(s) + } +} + +/** + * progresses by directly building the proof term + * @param t0 + * @param uks + */ +case class build(t0 : Term , uks : Context) extends Tactic { + override def applyToProof(p: Proof, ip: InteractiveProof): Msg = { + val (newuks, subss) = Context.makeFresh(uks , (p.getCurrCtx ++ ip.slvr.getPartialSolution).map(_.name)) + ip.slvr.addUnknowns(newuks , None) + val t = t0.substitute(subss)(PlainSubstitutionApplier) + val lam : Term = new Appremover(newuks)(t, p.getCurrCtx) + lazy val subs = newuks.map(x => new ProofUtil.ExtendUnkownInTerm( x.name , p.getCurrCtx )) + val newt = if (p.getCurrCtx.isEmpty) t else subs.foldLeft(t)((tres , sub) => sub(tres , p.getCurrCtx)) + val tmp = ip.slvr.check(Typing(Stack(p.getCurrCtx) , newt , p.getCurrentConc))(ip.hist) + if (!tmp){return HasError("could not tie type of goal to the given term " + ip.slvr.presentObj(t))} + ip.slvr.getPartialSolution.foreach(f => if (f.df.isDefined && f.tp.isEmpty){ + val tmp = ip.slvr.inferType(f.df.get , false)(Stack(p.getCurrCtx) , ip.hist) + if (tmp.isEmpty) HasError("could not infer type of newly one or more of the introduced holes/goals") + val tmp0 = ip.slvr.solveTyping(Typing(Stack(p.getCurrCtx) , f.toTerm, tmp.get))(ip.hist) + if (! tmp0) return HasError("could not solve type for " + f.name) + }) + val newgs0 = ip.slvr.getPartialSolution.filter(p => newuks.getO(p.name).isDefined) + if (newgs0.exists(p => p.tp.isEmpty)) return HasError("could not infer type of newly one or more of the introduced holes/goals") + val newgs = newgs0.map(x => { + val (tm , addctx) = ProofUtil.remOuterFreeA(x.tp.get , p.getCurrCtx) + Goal(tm , p.getCurrCtx ++ addctx , x.name) + }) + val old = p.currentState.remove(0) + p.currentState.insertAll(0, newgs) + genTerm(old, newt , lam , ip) + NoMsg() + + } + + def genTerm(old : Goal , newt : Term, newtt : Term ,ip : InteractiveProof) = { + ip.slvr.solve(old.ukname , Free(old.ctx , newt))(ip.hist) + ip.pr.updateGoalProofTerm(old.ukname , newtt) + } +} + +case class getdef() { + +} + +/** + * get the type of a term + * @param t + * @param uks + */ +case class gettype(t : Term , uks : Context) extends Tactic { + override def applyToProof(p: Proof, ip: InteractiveProof): Msg = { + val tp = standAloneInfer(t , uks , p.getCurrCtx, ip.hist, ip.slvr) + val tmp = WarningMsg(ip.slvr.presentObj(tp._1.getOrElse(return HasError("Could not infer the type of " + ip.slvr.presentObj(t))))) + val tmp0 = if (tp._3.nonEmpty) tmp.combineMsg(HasError("generated errors:\n" + tp._3.toString())) else tmp + val tmp1 = if (tp._4.nonEmpty) tmp0.combineMsg(HasError("generated constraints:\n" + tp._4.toString())) else tmp0 + tmp1 + } +} + +/** + * like [[gettype]] but prints the type fully qualified + * @param t + * @param uks + */ +case class gettyperaw(t : Term , uks : Context) extends Tactic { + override def applyToProof(p: Proof, ip: InteractiveProof): Msg = { + val tp = standAloneInfer(t , uks , p.getCurrCtx, ip.hist, ip.slvr) + WarningMsg(tp._1.getOrElse(return HasError("Could not infer the type of " + ip.slvr.presentObj(t))).toString()) + } +} + +/** + * print a term fully qualified + * @param t + */ +case class printraw(t : Term) extends Tactic { + override def applyToProof(p: Proof, ip: InteractiveProof): Msg = { + WarningMsg(t.toString) + } +} + +/** + * executes a forward step + * @param hypname + * @param t + * @param uks + * @param tms + */ +case class forward(hypname : String , t : Term , uks : Context, tms : List[(Term,Context)]) extends Tactic { + override def applyToProof(p: Proof, ip: InteractiveProof): Msg = { + // val res = ip.slvr.asInstanceOf[ExtendedSolver].termMatcher(p.getCurrCtx , Context() , t ) + ProofUtil.simpleApplyTermToTerm(p.getCurrCtx , tms.map(x => x._1) , t , ip.hist , ip.slvr) match { + case Some((gls, trm , newhyp)) => { + val gnames = gls.map(f => f.ukname) ::: ip.slvr.getPartialSolution.map(f => f.name) + val old@Goal(g, gctx, u) = p.currentState.remove(0) + val newhname = ProofUtil.pickFreshHypName(hypname, gctx) + var newgname = LocalName("", "goal") + while (gnames.contains(newgname)){ + newgname = p.getNewGoalName() + } + p.currentState.insertAll(0, gls ) + p.currentState.insert(0 , Goal(g , gctx ++ VarDecl(n = LocalName(newhname), tp = newhyp) , newgname)) + + + genTerm(old, gls , trm , LocalName(newhname) , newhyp, ip) + NoMsg() + } + case None => HasError("could not apply " + ip.slvr.presentObj(tms.head._1) + " to " + ip.slvr.presentObj(t)) + } + + } + + def genTerm(old : Goal, gls : List[Goal], hyptrm : Term , hypname : LocalName, hypType : Term , ip : InteractiveProof ) = { + val curr@Goal(g, gctx, gname) = ip.pr.getCurrentGoal + val newlam = Apply(Lambda(hypname , hypType , OMV(gname) ) , hyptrm) + val newlam0 = Apply(Lambda(hypname , hypType , curr.makeUnknown(ip.slvr, gname) ) , hyptrm) + val glsctx = Context(VarDecl(n = gname , tp = Free(gctx ,g)) :: gls.map(x => VarDecl(n = x.ukname , tp = Free(old.ctx ,x.g))) : _ *) + ip.slvr.addUnknowns( glsctx, None) + ip.slvr.solve(old.ukname , Free(old.ctx , newlam0))(ip.hist) + ip.pr.updateGoalProofTerm(old.ukname, newlam) + } +} \ No newline at end of file diff --git a/src/mmt-lf/src/info/kwarc/mmt/lf/itp/TacticsParserA.scala b/src/mmt-lf/src/info/kwarc/mmt/lf/itp/TacticsParserA.scala new file mode 100644 index 000000000..2d57fd792 --- /dev/null +++ b/src/mmt-lf/src/info/kwarc/mmt/lf/itp/TacticsParserA.scala @@ -0,0 +1,268 @@ +package info.kwarc.mmt.lf.itp + +import info.kwarc.mmt.api.{ErrorHandler, ErrorThrower} +import info.kwarc.mmt.api.documents.InterpretationInstructionContext +import info.kwarc.mmt.api.objects.{Context, PlainSubstitutionApplier, Stack, Term, Typing, VarDecl} +import info.kwarc.mmt.api.parser.{NotationBasedParser, ParseResult, ParsingUnit, SourceRef} +import info.kwarc.mmt.api.proving.itp.Goal + +import scala.collection.mutable.ArrayBuffer +import scala.util.matching.Regex +import scala.util.parsing.combinator.JavaTokenParsers +import scala.util.parsing.input.CharArrayReader + +/** + * almost the same as [[TacticsParser]] but with the slight modification that it can be extended without specifying the proof manager [[InteractiveProof]] + */ +trait TacticsParserA extends JavaTokenParsers{ + val hypName: Regex = "([a-z]|[A-Z])+([a-z]|[A-Z]|[0-9]|[/_])*".r + val hypNameWithSlash : Regex = "([a-z]|[A-Z]|/)+([a-z]|[A-Z]|[0-9]|[/_])*".r + val anyExpr : Regex = ".*".r + val anyExprBrack : Regex = "\\(.*\\)".r + val anyExprBrackNoKeyWord : Parser[String] = anyExprBrack >> {s => if (s.contains("in")) {failure("should not contain keyword \"in\"")} else {success(s)} } + val spaces : Regex = """[ \n\t\s]*""".r + val nespaces : Regex = """[ \n\t\s]+""".r + + // override val whiteSpace : Regex = """\s+""".r + override val skipWhitespace = false + + // override def handleWhiteSpace(source: CharSequence, offset: Int): Int = super.handleWhiteSpace(source, offset) + + + def simpleTermParser(t : String, ip : InteractiveProof) : ( Term, Context) = { + + val c = ip.slvr.controller + val nbp = c.extman.get(classOf[NotationBasedParser]).head + val cxt = ip.pr.currentState.head.ctx ++ (if (ip.mp.isDefined) Context(ip.mp.get) else Context()) + val pu = ParsingUnit(SourceRef.anonymous("interactive") , cxt , t ,InterpretationInstructionContext(ip.slvr.controller.getNamespaceMap) ) + val eh : ErrorHandler = ErrorThrower + val ParseResult(u,f,tt) = nbp(pu)(eh) + // val newmiss = u.map(x => ip.pr.getCurrentGoal.makeMiss(x.name)) + (tt, u ) + } + + + def currGoalParseTerm(t : String , ip : InteractiveProof) : ( Term, Context) = { + + val c = ip.slvr.controller + val nbp = c.extman.get(classOf[NotationBasedParser]).head + val cxt = ip.pr.currentState.head.ctx ++ (if (ip.mp.isDefined) Context(ip.mp.get) else Context()) + val pu = ParsingUnit(SourceRef.anonymous("interactive") , cxt , t ,InterpretationInstructionContext(ip.slvr.controller.getNamespaceMap) ) + val eh : ErrorHandler = ErrorThrower + val ParseResult(u,f,tt) = nbp(pu)(eh) + val Goal(g , gctx , ukn) = ip.pr.getCurrentGoal + // val newmiss = u.map(x => ip.pr.getCurrentGoal.makeMiss(x.name)) + ip.pr.update(Goal(g , gctx , ukn )) + ip.slvr.addUnknowns(u, None) + + (tt, u ) + } + + + + def currGoalParseTermA(t : String, ip : InteractiveProof) : ( Term, Context) = { + + + def newnames(ctx0 : Context, tt : Term): (Context, Term) = { + val ps = ip.slvr.getPartialSolution + var res = Context() + var restt = tt + + def loop(ctx : List[VarDecl]) : Unit = ctx match { + case Nil => + case (x::xs) => { + val (newn , subn) = Context.pickFresh(Context(xs : _ *) ++ res ++ ps , x.name) + restt = restt.substitute(subn)(PlainSubstitutionApplier) + res = res ++ x.copy(name = newn) + loop(xs) + } + } + loop(ctx0.variables.toList) + (res , restt) + } + + val c = ip.slvr.controller + val nbp = c.extman.get(classOf[NotationBasedParser]).head + val cxt = ip.pr.currentState.head.ctx ++ (if (ip.mp.isDefined) Context(ip.mp.get) else Context()) + // val uxt = ip.pr.getCurrUks.map(x => x.ln) + val pu = ParsingUnit(SourceRef.anonymous("interactive") , cxt , t ,InterpretationInstructionContext(ip.slvr.controller.getNamespaceMap) ) + val eh : ErrorHandler = ErrorThrower + val ParseResult(u0,frees,tt0) = nbp(pu)(eh) + val gl@Goal(g , gctx , ukn) = ip.pr.getCurrentGoal + + val (u,tt1) = newnames(u0,tt0) + lazy val sub = u.map(x => new ProofUtil.ExtendUnkownInTerm( x.name , gctx )) // Substitution(u.variables.map(v => Sub(v.name , gl.makeUnknown(ip.slvr , v.name))) : _*) + val tt = if (gctx.isEmpty) tt1 else sub.foldLeft(tt1)((tres , sub) => sub(tres , gctx)) // tt1.substitute(sub)(PlainSubstitutionApplier) + ip.slvr.addUnknowns(u , None) + val tmp = ip.slvr.inferType(tt , false)(Stack(ip.pr.getCurrCtx), ip.hist) // ip.slvr.asInstanceOf[ExtendedSolver].standAloneInfer(tt,u,ip.pr.getCurrCtx,ip.hist) // ip.slvr.inferType(tt , false)(Stack(ip.pr.getCurrCtx), ip.hist) //check(Typing(Stack(Context()) , tm , tp))(new History(Nil)) + val tmp1 = ip.slvr.getPartialSolution.filter(x => u.index(x.name).isDefined) + val ukres = tmp match { + case None => throw new TacticError("could not infer type of: " + ip.slvr.presentObj(tt)) + case Some(ttp) => { + val (res, ures ) = ProofUtil.standAloneTypeCheck(tt , ttp , tmp1 , ip.pr.getCurrCtx, ip.slvr) + Context(ures.map(x => if (x.df.isDefined && ProofUtil.containsMissing(x.df.get)) x.copy(df = None) else x ) : _ *) + } + } + + /* val alluks = ukres // ip.slvr.getPartialSolution + alluks.foreach(x => (x.tp , x.df) match { + case (None , None) => throw new TacticError("could not infer type of unkown " + x.name.toString + " in term " + ip.slvr.presentObj(tt) + " (raw: " + tt.toString + " )") + case (Some(tpv) , None) => + case (None , Some(dfv)) => { + } + case _ => + }) + + */ + // ip.slvr.addUnknowns(ukres, if (u.nonEmpty) Some(u(0).name) else None) + // var ttres = tt + ukres.foreach(x => { + if (x.df.isDefined && ! ProofUtil.containsMissing(x.df.get)) { + ip.slvr.solve(x.name , x.df.get)(ip.hist) + // val newsub = Substitution(Sub(x.name , x.df.get)) + // ttres = ttres ^ newsub + } + if (x.tp.isDefined && ! ProofUtil.containsMissing(x.tp.get)) ip.slvr.solveTyping(Typing(Stack(gctx) , x.toTerm , x.tp.get ))(ip.hist) + }) + + // val us = ip.slvr.getUnsolvedVariables + val newuks = ukres.filter(x => x.df.isEmpty) // us.variables.filter(p => u.variables.exists((x : VarDecl) => x.name == p.name)) + val newukgoals = newuks.map(v => Goal(ProofUtil.remOuterFree(v.tp.get , gctx) , ip.pr.getCurrCtx, v.name)) + ip.pr.currentState.appendAll(newukgoals ) + val ukret = ukres.map(v => { + val newtp = v.tp match { + case None => None + case Some(tpp) => if (ProofUtil.containsMissing(tpp)) None else Some(tpp) + } + val newdf = v.df match { + case None => None + case Some(dff) => if (ProofUtil.containsMissing(dff)) None else Some(dff) + } + v.copy(tp = newtp , df = newdf) + }) + // val subs = Substitution( ukre : _ *) + // val ttnew = tt & subs + val ttres = ip.slvr.substituteSolution(tt) + (ttres ,ukret) + } + + + abstract class EParser[+T] extends Parser[T] { + def ?~>[A](p : => Parser[A]) : Parser[Option[A]] = { + this ~> """\s*""".r ~ p.? >> { + case ws ~ (r@Some(pr)) => if (ws.length > 0) success(r) else failure("arguments have to be separated by whitespace") + case ws ~ None => success(None) + } + } + + def ??~>[A](p : => Parser[Option[A]]) : Parser[Option[A]] = { + this ~> """\s*""".r ~ p >> { + case ws ~ (r@Some(pr)) => if (ws.length > 0) success(r) else failure("arguments have to be separated by whitespace") + case ws ~ None => success(None) + } + } + + def &~>[A](p : => Parser[A]) : Parser[A] = { + this ~> """\s+""".r ~> p + + } + + def &~[A](p : => Parser[A]) : Parser[~[T,A]] = { + this ~ """\s+""".r ~ p ^^ {case a ~ b ~ c => new ~(a , c) } + + } + + def ??~[A](p : => Parser[Option[A]]) : Parser[~[T,Option[A]]] = { + this ~ """\s*""".r ~ p >> { + case a ~ ws ~ (r@Some(pr)) => if (ws.length > 0) success(new ~(a,r)) else failure("arguments have to be separated by whitespace") + case a~ ws ~ None => success(new ~(a,None)) + } + } + + def ?~[A](p : => Parser[A]) : Parser[~[T,Option[A]]] = { + this ~ """\s*""".r ~ p.? >> { + case a ~ ws ~ (r@Some(pr)) => if (ws.length > 0) success(new ~(a,Some(pr))) else failure("arguments have to be separated by whitespace") + case a~ ws ~ None => success(new ~(a,None)) + } + } + + def done[A](p : => Parser[A]) : Parser[A] = { + """\s*""".r ~> p <~ """\s*""".r + } + + + } + + implicit def ptoep[A](p : Parser[A]) : EParser[A] = { + new EParser[A]{override def apply(i : Input) = p.apply(i)} + } + + implicit def eliteral(s : String): EParser[String] = { + ptoep[String](literal(s)) + } + + implicit def eregex(r : Regex) : EParser[String] = { + ptoep(regex(r)) + } + + def inbalbracksOpt[A](p : => Parser[A]) : Parser[A] = { + new EParser[A]{ + override def apply(i : Input): ParseResult[A] = { + if(i.atEnd) return Failure("empty expression", i) + var curr : Char = i.first + var rest = i.rest + var oldrest = rest + while((! i.atEnd) && List(' ' , '\t' , '\n' ).contains(curr) ){ + curr = rest.first + oldrest = rest + rest = rest.rest + } + if(curr == '(') { + var bcount = 1 + val newi : ArrayBuffer[Char] = ArrayBuffer[Char](curr) + while ((!rest.atEnd) && bcount != 0){ + curr = rest.first + oldrest = rest + rest = rest.rest + if (curr == '(') { + bcount += 1 + }else if (curr == ')'){ + bcount -= 1 + } + newi.append(curr) + } + val newi0 = new CharArrayReader(newi.toArray,0) + if (rest.atEnd) oldrest = rest + p.apply(newi0) match { + case Success(result, next) => { + if (! next.atEnd) return Failure("could not parse argument", next) + else { + Success(result , rest) + } + } + case ns : NoSuccess => ns + } + }else { + val newi : ArrayBuffer[Char] = ArrayBuffer[Char](curr) + while((! rest.atEnd) && ! List(' ' , '\t' , '\n' ).contains(curr)){ + curr = rest.first + oldrest = rest + rest = rest.rest + if (! List(' ' , '\t' , '\n' ).contains(curr)) newi.append(curr) + } + if (rest.atEnd) oldrest = rest + val newi0 = new CharArrayReader(newi.toArray,0) + p.apply(newi0) match { + case Success(result, next) => { + if (! next.atEnd) return Failure("could not parse argument", next) + else { + Success(result , oldrest) + } + } + case ns : NoSuccess => ns + } + } + } + } + } +} \ No newline at end of file diff --git a/src/mmt-lf/src/info/kwarc/mmt/lf/itp/Utils/OMLTraverser.scala b/src/mmt-lf/src/info/kwarc/mmt/lf/itp/Utils/OMLTraverser.scala new file mode 100644 index 000000000..b99408505 --- /dev/null +++ b/src/mmt-lf/src/info/kwarc/mmt/lf/itp/Utils/OMLTraverser.scala @@ -0,0 +1,10 @@ +package info.kwarc.mmt.lf.itp.Utils + +import info.kwarc.mmt.api.objects._ + +class OMLTraverser extends StatelessTraverser { + override def traverse(t: Term)(implicit con: Context, state: State): Term = t match{ + case OML(nm , None , None , None , None) => OMV(nm) + case _ => Traverser(this, t ) + } +} diff --git a/src/mmt-lf/src/info/kwarc/mmt/lf/itp/Utils/OutOfOrderApplierLF.scala b/src/mmt-lf/src/info/kwarc/mmt/lf/itp/Utils/OutOfOrderApplierLF.scala new file mode 100644 index 000000000..4dce3964e --- /dev/null +++ b/src/mmt-lf/src/info/kwarc/mmt/lf/itp/Utils/OutOfOrderApplierLF.scala @@ -0,0 +1,93 @@ +package info.kwarc.mmt.lf.itp.Utils + +import info.kwarc.mmt.api.LocalName +import info.kwarc.mmt.api.objects.{Context, Term} +import info.kwarc.mmt.lf.{Arrow, FunType, Pi} + +import scala.collection.mutable.{Map => mmap} + + +/* +object OutOfOrderApplierLF { + + def alpharename(t : Term , ctx : Context) : Term = { + val FunType(args , conc) = t + + def alpharenameL(ags : List[(Option[LocalName] , Term )], lctx :Context) = ags match { + case Nil => + case (Some(nm) , tt):: xs => { + + } + case (None , tt)::xs => { + + } + } + } + + + def forward(t : Term, ctx : Context ) = { + val FunType(args , conc) = t + + val mp : mmap[(Int , LocalName), Int] = mmap() + + def alpharename(ags : List[(Option[LocalName] , Term)] , pos : Int): Unit = ags match { + case Nil => () + case (Some(nm) , tt )::xs => { + + } + case (None, tt)::xs => { + + } + } + + } +} + + */ +/* + def deconstructLFTerm(t : Term) = t match { + + } + + + */ + /* + def mkRefs(t : Term, g : Term => Term, s : Term => (Term => Term) , b : Box[Term]): List[Ref[Term]] = t match { + case Arrow(h,tl) => { + val news = { x : Term =>{ + y : Term => { + g(x) match { case Arrow(hh,tt) => s(x)(Arrow(hh, y))} + } + }} + + val tmp = mkRefs(tl , {x : Term => g(x) match {case Arrow(hh,tt) => tt }}, news , b) + val newss = {x : Term => b.v = s(b.v)(x)} + new Ref(g(b.v) ,newss) :: tmp + } + case Pi(nm , tp , bd) => { + val news = { x : Term =>{ + y : Term => { + g(x) match { case Pi(nmm, tpp ,bdd) => s(x)(Pi(nmm, tpp, y))} + } + }} + + val tmp = mkRefs(bd , {x : Term => g(x) match {case Pi(nmm,tpp, bdd) => bdd }}, news , b) + val newss = {x : Term => b.v = s(b.v)(x)} + new Ref(g(b.v) ,newss) :: tmp + } + case _ => { + val newss = {x : Term => b.v = s(b.v)(x)} + List(new Ref(g(b.v) , newss)) + } + } + + + + def makedeps() : Map[Ref[Term], List[Ref[Term]]] = { + + } + + +} + + */ diff --git a/src/mmt-lf/src/info/kwarc/mmt/lf/itp/Utils/StandAloneChecks.scala b/src/mmt-lf/src/info/kwarc/mmt/lf/itp/Utils/StandAloneChecks.scala new file mode 100644 index 000000000..1a70fbf94 --- /dev/null +++ b/src/mmt-lf/src/info/kwarc/mmt/lf/itp/Utils/StandAloneChecks.scala @@ -0,0 +1,31 @@ +package info.kwarc.mmt.lf.itp.Utils + +import info.kwarc.mmt.api.checking.{CheckingUnit, History, Solver, state} +import info.kwarc.mmt.api.frontend.Controller +import info.kwarc.mmt.api.objects._ +import info.kwarc.mmt.api.{LocalName, MPath, RuleSet} + +object StandAloneChecks { + def standAloneEqCheck(s: Solver, uks: List[(LocalName, Term)], localctx: Context, tm: Term, tm0: Term) = { + val clondestate = new state() //.copyValues(s.currentStateObj.getCurrentState) + clondestate.copyValues(s.currentStateObj.getCurrentState) + val clones = new Solver(s.controller, s.checkingUnit, s.rules, Some(clondestate)) + clones.addUnknowns(uks.map(f => VarDecl(f._1, tp = f._2)), None) + clones.check(Equality(Stack(localctx), tm, tm0, None))(new History(Nil)) + } + + def standAloneEqCheck(c: Controller, mp: MPath, uks: List[(LocalName, Term)], localctx: Context, tm: Term, tm0: Term) = { + val cu = new CheckingUnit(None, Context(mp), uks.map(f => VarDecl(f._1, tp = f._2)), null) + val rules = RuleSet.collectRules(c, Context(mp)) + val clones = new Solver(c, cu, rules, None) + clones.check(Equality(Stack(localctx), tm, tm0, None))(new History(Nil)) + } + + def standAloneInfer(t : Term , c : Controller , mp : MPath , uks : Context , lctx : Context) : (Context , Term) = { + val cu = new CheckingUnit(None , Context(mp) , uks , null) + val rules = RuleSet.collectRules(c, Context(mp)) + val sol = new Solver(c, cu , rules , None) + val Some(res) = sol.inferType(t , false )(Stack(lctx) , new History(Nil)) + (sol.getPartialSolution , res ) + } +} diff --git a/src/mmt-lf/src/info/kwarc/mmt/lf/itp/Utils/TermUtil.scala b/src/mmt-lf/src/info/kwarc/mmt/lf/itp/Utils/TermUtil.scala new file mode 100644 index 000000000..c84a512c6 --- /dev/null +++ b/src/mmt-lf/src/info/kwarc/mmt/lf/itp/Utils/TermUtil.scala @@ -0,0 +1,240 @@ +package info.kwarc.mmt.lf.itp.Utils + +import info.kwarc.mmt.api.LocalName +import info.kwarc.mmt.api.objects.Obj.getConstants +import info.kwarc.mmt.api.objects._ +import info.kwarc.mmt.lf.{Apply, ApplySpine, Arrow, Pi} + +object TermUtil { + def getTerm(tt: Term, ninit: Int): (Term => Term, Term) = { + val currprevini = (x: Term) => x + val currini: Term = tt + def getTermLoop(currprev : Term => Term , curr : Term , n : Int): (Term => Term , Term) = { + if (n == 0) return (currprev, curr) + curr match { + case Arrow(h, tl) => { + val tmp = (x: Term) => currprev(Arrow(h, x)) + getTermLoop(tmp , tl , n - 1) + } + case Pi(nm, tp, bd) => { + val tmp = (x: Term) => currprev(Pi(nm, tp, x)) + getTermLoop(tmp, bd, n - 1) + } + case v => (currprev, curr) + } + + + } + getTermLoop(currprevini , currini , ninit) + + } + + def getTermSafe(tt: Term, ninit: Int): Option[(Term => Term, Term)] = { + val currprevini = (x: Term) => x + val currini: Term = tt + def getTermLoop(currprev : Term => Term , curr : Term , n : Int): Option[(Term => Term , Term)] = { + if (n == 0) return Some((currprev, curr)) + curr match { + case Arrow(h, tl) => { + val tmp = (x: Term) => currprev(Arrow(h, x)) + getTermLoop(tmp , tl , n - 1) + } + case Pi(nm, tp, bd) => { + val tmp = (x: Term) => currprev(Pi(nm, tp, x)) + getTermLoop(tmp, bd, n - 1) + } + case v => None + } + + + } + getTermLoop(currprevini , currini , ninit) + + } + + def getTermByName(tt: Term, l: LocalName, pos: Int): Option[(Term, Int)] = tt match { + case Arrow(h, tl) => getTermByName(h, l, pos + 1) + case Pi(nm, tp, bd) => { + if (nm == l) { + Some(tt, pos) + } else { + getTermByName(bd, l, pos + 1) + } + } + case _ => None + } + + + def getTermByNameWithExternalBinders(tt: Term, l: LocalName, pos: Int): Option[(Term, Int)] = tt match { + case Arrow(h, tl) => getTermByName(h, l, pos + 1) + case Pi(nm, tp, bd) => { + if (nm == l) { + Some(tt, pos) + } else { + getTermByNameWithExternalBinders(bd, l, pos + 1) + } + } + case _ => None + } + + def termlength(tt: Term): Int = tt match { + case Arrow(_, tl) => { + termlength(tl) + 1 + } + case Pi(_, _, bd) => { + termlength(bd) + 1 + } + case _ => 1 + } + + def genDeps(ttt: Term): List[Set[(LocalName, Term, Int)]] = { + def loopGenDeps(tt: Term, vars: Set[(LocalName, Term, Int)], pos: Int): List[Set[(LocalName, Term, Int)]] = tt match { + case Arrow(h, tl) => { + val tmp = loopGenDeps(tl, vars, pos + 1) + vars :: tmp + } + case Pi(nm, tp, bd) => { + val newelm: (LocalName, Term, Int) = (nm, tp, pos) + val tmp = loopGenDeps(bd, vars + newelm, pos + 1) + vars :: tmp + } + case trm => List(vars) + } + + loopGenDeps(ttt, Set.empty, 0) + } + + + def genDepsSmart(ttt: Term): List[Set[(LocalName, Term, Int)]] = { + def loopGenDepsSmart(tt: Term, vars: Set[(LocalName, Term, Int)], pos: Int): List[Set[(LocalName, Term, Int)]] = tt match { + case Arrow(h, tl) => { + val tmp = loopGenDepsSmart(tl, vars, pos + 1) + vars.filter(x => h.freeVars.contains(x._1)) :: tmp + } + case Pi(nm, tp, bd) => { + val newelm: (LocalName, Term, Int) = (nm, tp, pos) + val newvars = vars.filter(p => p._1 != nm) + val tmp = loopGenDepsSmart(bd, newvars + newelm, pos + 1) + vars.filter(x => tp.freeVars.contains(x._1)) :: tmp + } + case trm => List(vars.filter(v => trm.freeVars.contains(v))) + } + + loopGenDepsSmart(ttt, Set.empty, 0) + } + + + def toBinaryRelation(t : Term, rel : Option[Term] = None ) : Term ={ + t match{ + case OMA(OMID(Apply.path) , List(rel,a,b)) => t + case OMA(OMID(Apply.path) , rel:: x::xs) => { + toBinaryRelation(ApplySpine(Apply(rel , x) , xs : _* )) + } + } + } + + + def arrowify(t : Term) : Term = t match { + case Arrow(h , tl) => Arrow(h , arrowify(tl)) + case Pi(nm , tp , bd) => { + if (bd.freeVars.contains(nm)){ + Pi(nm , tp , arrowify(bd)) + }else { + Arrow(tp, arrowify(bd) ) + } + } + case _ => t + } + + class ExternalBinder(val position : Int) + + + +/* + def genDepsSmartWithExternalBinders(ttt: Term , extbind : List[(LocalName, Term)]): (List[Set[(LocalName, Term, Either[Int, ExternalBinder])]] , List[(LocalName,Term,ExternalBinder)]) = { + def loopGenDepsSmartWithExternalBinders(tt: Term, vars: Set[(LocalName, Term, Either[Int,ExternalBinder ])], pos: Int): List[Set[(LocalName, Term, Either[Int,ExternalBinder ])]] = tt match { + case Arrow(h, tl) => { + val tmp = loopGenDepsSmartWithExternalBinders(tl, vars, pos + 1) + vars.filter(x => h.freeVars.contains(x._1)) :: tmp + } + case Pi(nm, tp, bd) => { + val newelm: (LocalName, Term, Either[Int,ExternalBinder ]) = (nm, tp, Left(pos) : Either[Int, ExternalBinder ]) + val newvars = vars.filter(p => p._1 != nm) + val tmp = loopGenDepsSmartWithExternalBinders(bd, newvars + newelm, pos + 1) + vars.filter(x => tp.freeVars.contains(x._1)) :: tmp + } + case trm => List(vars.filter(v => trm.freeVars.contains(v))) + } + val actualexternalbinders = extbind.foldLeft(List[(LocalName,Term, Either[Int,ExternalBinder])]() , 0)((f ,curr) => ((curr._1 , curr._2 , Right(new ExternalBinder(f._2))) :: f._1 , f._2 + 1))._1.filter(ff => ttt.freeVars.contains(ff._1)) + val res = loopGenDepsSmartWithExternalBinders(ttt, Set.from(actualexternalbinders.foldLeft(List[(LocalName,Term, Either[Int,ExternalBinder])]() , 0)((f ,curr) => ((curr._1 , curr._2 , Right(new ExternalBinder(f._2))) :: f._1 , f._2 + 1))._1 ), 0) + ( res , actualexternalbinders.map(pp => pp.copy(_3 = pp._3.asInstanceOf[Right].value.asInstanceOf[ExternalBinder])) ) + } + + */ +/* + def getHyps(t : Term) : List[Term] = { + + } + + + */ + def getConclusion(t : Term) : Term = t match { + case Arrow(h , tl) => getConclusion(tl) + case Pi(nm , tp , bd) => getConclusion(bd) + case _ => t + } + + def nextBinders(t : Term) : List[LocalName] = t match { + case Arrow(h,tl) => nextBinders(tl) + case Pi(nm , tp , bd) => { + val res = nextBinders(bd) + nm::res + + } + case _ => Nil + } + + + + def binderRenaming(t : Term, lctx : Context , prev : List[LocalName]) : Term = t match { + case Arrow(h , tl) => Arrow(h , binderRenaming(tl , lctx , prev)) + case Pi(nm , tp , bd) => { + val nxtbinders = nextBinders(bd).map(f => VarDecl(f)) + val (ln , su) = Context.pickFresh( lctx ++ Context.list2context(prev.map(x => VarDecl(n = x))) ++ Context.list2context(nxtbinders), nm) + val newrestterm = bd.substitute(su)(PlainSubstitutionApplier) + val res = binderRenaming(newrestterm, lctx , nm :: prev) + Pi(ln , tp, res) + } + case _ => t + } + + def getNotLocallyBoundNames(t : Term) = getConstants(t).map(_.name) ++ t.freeVars + /* + def binderRenaiming(t : Term , lctx : Context) : Term = { + val nms = getNotLocallyBoundNames() + } + + */ +/* + def getNotLocallyBoundNames (t : Term, binders : List[LocalName]) : List[LocalName] = t match { + case OMV(name) => { + if (binders.contains(name)) { + Nil + } else { + List(name) + } + } + case Arrow(h , tl) => { + val res = getNotLocallyBoundNames(h , binders) + val res0 = getNotLocallyBoundNames(tl , binders) + res ++ res0 + } + case Pi(nm , tp , bd ) => { + getNotLocallyBoundNames(bd , nm :: binders) + } + case OMID(path) => List(path.name) + case _ => Nil + } + + */ +} diff --git a/src/mmt-lf/src/info/kwarc/mmt/lf/itp/Utils/Unifier/MoreGeneralUnifier.scala b/src/mmt-lf/src/info/kwarc/mmt/lf/itp/Utils/Unifier/MoreGeneralUnifier.scala new file mode 100644 index 000000000..b04e6e827 --- /dev/null +++ b/src/mmt-lf/src/info/kwarc/mmt/lf/itp/Utils/Unifier/MoreGeneralUnifier.scala @@ -0,0 +1,23 @@ +package info.kwarc.mmt.lf.itp.Utils.Unifier + +import info.kwarc.mmt.api.checking.{CheckingUnit, Solver} +import info.kwarc.mmt.api.frontend.Controller +import info.kwarc.mmt.api.objects.{Context, Equality, Stack, Term} +import info.kwarc.mmt.api.{MPath, RuleSet} + +object MoreGeneralUnifier { + def apply(t : Term , t0 : Term , uks : Context , uks0 : Context, c : Controller , pth : MPath , cctx : Context, rls : RuleSet, localContext : Context): Option[(Context , Term)] = { + val cu = CheckingUnit(None, cctx , uks ++ uks0 , null ) + // val rules = RuleSet.collectRules(c, Context(pth)) + val solver = new Solver(c, cu, rls) + val res = solver.apply(Equality( Stack(localContext), t, t0 ,None )) + + if (res && !solver.hasUnresolvedConstraints && ! solver.hasUnsolvedVariables && solver.getErrors.isEmpty){ + val tmp = solver.getPartialSolution + val tres = solver.substituteSolution(t) + Some((tmp , tres)) + }else { + None + } + } +} diff --git a/src/mmt-lf/src/info/kwarc/mmt/lf/itp/Utils/Unifier/Unifier.scala b/src/mmt-lf/src/info/kwarc/mmt/lf/itp/Utils/Unifier/Unifier.scala new file mode 100644 index 000000000..ea802caaa --- /dev/null +++ b/src/mmt-lf/src/info/kwarc/mmt/lf/itp/Utils/Unifier/Unifier.scala @@ -0,0 +1,48 @@ +package info.kwarc.mmt.lf.itp.Utils.Unifier + +import info.kwarc.mmt.api.RuleSet +import info.kwarc.mmt.api.checking.{CheckingUnit, Solver} +import info.kwarc.mmt.api.frontend.Controller +import info.kwarc.mmt.api.objects.Context.context2list +import info.kwarc.mmt.api.objects._ +import info.kwarc.mmt.lf.itp.Utils.TermUtil + +object Unifier { + def apply(t: Term, uks: Context, query: Term, c: Controller, cctx: Context, rls: RuleSet, lctx: Context): Option[(Context , Term)] = { + val mtcher = new Matcher(c, rls ) + val names = TermUtil.getNotLocallyBoundNames(t) + /// val (ndup, dup) = uks.partition(names.contains(_)) + val alphauks = Context.makeFresh( uks , names ++ lctx.map(_.name) ) + val alphaquery = query.substitute(alphauks._2)(PlainSubstitutionApplier) + + mtcher.apply(lctx, t, alphauks._1, alphaquery) match { + case MatchFail => + case MatchSuccess(solution, false) => { + val dbg = () + } + case MatchSuccess(solution, true) => { + return { + val alphasol = solution.map(ss => {val tmp = alphauks._2.find(_.target.asInstanceOf[OMV].name == ss.name) ; VarDecl(tmp.get.name, df = ss.target)}) + val solctx = Context.list2context(alphasol) // Context(alphasol.map(ss => VarDecl(n = ss.name , df = ss.target)) : _*) + val solt = alphaquery.substitute(solution)(PlainSubstitutionApplier) + Some((solctx, solt)) + } + } + } + + + val cu = CheckingUnit(None, cctx , alphauks._1 , null ) + // val rules = RuleSet.collectRules(c, Context(pth)) + val solver = new Solver(c, cu, rls) + val res = solver.apply(Equality( Stack((lctx)), t, alphaquery ,None )) + + if (res && !solver.hasUnresolvedConstraints && ! solver.hasUnsolvedVariables && solver.getErrors.isEmpty){ + val tmp = solver.getPartialSolution + val alphasol = tmp.map(v => {val tmp0 = alphauks._2.find(ss => ss.target.asInstanceOf[OMV].name == v.name).get ; new VarDecl(tmp0.name , None , v.tp , v.df , None )} ) + val tres = solver.substituteSolution(alphaquery) + Some((alphasol , tres)) + }else { + None + } + } +} From a30b31a00a0d37da0f07b3b0309a1f109f6f87d5 Mon Sep 17 00:00:00 2001 From: svenw <26742574+SvenWille@users.noreply.github.com> Date: Tue, 24 May 2022 23:24:26 +0200 Subject: [PATCH 3/3] removed the branchpoint class --- .../src/main/info/kwarc/mmt/api/checking/Solver.scala | 10 ---------- 1 file changed, 10 deletions(-) diff --git a/src/mmt-api/src/main/info/kwarc/mmt/api/checking/Solver.scala b/src/mmt-api/src/main/info/kwarc/mmt/api/checking/Solver.scala index a43f75200..55980df5a 100644 --- a/src/mmt-api/src/main/info/kwarc/mmt/api/checking/Solver.scala +++ b/src/mmt-api/src/main/info/kwarc/mmt/api/checking/Solver.scala @@ -1124,13 +1124,3 @@ case class Success[A](result: A) extends DryRunResult { override def toString = "will succeed" } -// TODO variable bounds are missing -/** experimental backtracking support in [[Solver]] */ -class Branchpoint(val parent: Option[Branchpoint], val delayed: List[DelayedConstraint], val depLength: Int, val solution: Context) { - def isRoot = parent.isEmpty - /** @return true if this branch contains anc */ - def descendsFrom(anc: Branchpoint): Boolean = parent.contains(anc) || (parent match { - case None => false - case Some(p) => p.descendsFrom(anc) - }) -} \ No newline at end of file