From bb2d3245e4b3e3e9a234409396ec29136a53e957 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Dennis=20M=C3=BCller?= Date: Mon, 9 Apr 2018 14:14:44 +0200 Subject: [PATCH 1/8] Viewfinder stuff --- .../mmt/api/refactoring/AlignmentFinder.scala | 117 +++++++++--------- .../mmt/api/refactoring/Consthasher.scala | 14 +-- .../src/info/kwarc/mmt/mitm/Viewfinder.scala | 42 +++++++ 3 files changed, 109 insertions(+), 64 deletions(-) create mode 100644 src/mmt-odk/src/info/kwarc/mmt/mitm/Viewfinder.scala diff --git a/src/mmt-api/src/main/info/kwarc/mmt/api/refactoring/AlignmentFinder.scala b/src/mmt-api/src/main/info/kwarc/mmt/api/refactoring/AlignmentFinder.scala index 28dcea6940..0d936dd15c 100644 --- a/src/mmt-api/src/main/info/kwarc/mmt/api/refactoring/AlignmentFinder.scala +++ b/src/mmt-api/src/main/info/kwarc/mmt/api/refactoring/AlignmentFinder.scala @@ -5,7 +5,6 @@ import info.kwarc.mmt.api.modules.DeclaredTheory import info.kwarc.mmt.api.symbols.FinalConstant import info.kwarc.mmt.api._ import info.kwarc.mmt.api.archives.Archive -import info.kwarc.mmt.api.objects._ import info.kwarc.mmt.api.ontology.FormalAlignment import info.kwarc.mmt.api.utils.File import info.kwarc.mmt.api.utils.time.Time @@ -13,7 +12,7 @@ import info.kwarc.mmt.api.utils.time.Time import scala.collection.mutable import scala.concurrent.{ExecutionContext, Future} -class FinderConfig(finder : AlignmentFinder, protected val report : Report) extends Logger { +class FinderConfig(val finder : AlignmentFinder, protected val report : Report) extends Logger { override def logPrefix: String = "viewfinder" private var fromTheories_var : List[DeclaredTheory] = Nil @@ -26,9 +25,9 @@ class FinderConfig(finder : AlignmentFinder, protected val report : Report) exte private var minimal_parameter_length_var = 0 private var multithreaded : Boolean = false - def fromTheories : List[DeclaredTheory] = fromTheories_var - def toTheories : List[DeclaredTheory] = toTheories_var - def commonTheories : List[DeclaredTheory] = commonTheories_var + // def fromTheories : List[DeclaredTheory] = fromTheories_var + // def toTheories : List[DeclaredTheory] = toTheories_var + // def commonTheories : List[DeclaredTheory] = commonTheories_var def fixing : List[AlignmentTranslation] = fixing_var def judg1: Option[GlobalName] = judg1_var def judg2: Option[GlobalName] = judg2_var @@ -38,6 +37,7 @@ class FinderConfig(finder : AlignmentFinder, protected val report : Report) exte def setMultithreaded(b : Boolean) = multithreaded = b + /* def addFrom(th : List[DeclaredTheory]) = { fromTheories_var :::= th val cs = fromTheories_var.filter(t => toTheories_var.contains(t) || commonTheories_var.contains(t)) @@ -54,6 +54,8 @@ class FinderConfig(finder : AlignmentFinder, protected val report : Report) exte toTheories_var = toTheories_var.filterNot(commonTheories_var.contains).distinct commonTheories_var = commonTheories_var.distinct } + */ + private def addAlignments(al : List[FormalAlignment]) = { fixing_var :::= al.map(finder.makeAlignment) } @@ -66,25 +68,26 @@ class FinderConfig(finder : AlignmentFinder, protected val report : Report) exte def setDoDefs(b : Boolean) = doDefs_var = b def setMinParLength(i : Int) = minimal_parameter_length_var = i - def findJudgments = { - log("finding Judgments...") - val judg1 = if (judg1_var.isDefined) judg1_var else finder.getJudgment(fromTheories ::: commonTheories) - val judg2 = if (judg2_var.isDefined) judg2_var else finder.getJudgment(toTheories ::: commonTheories) - log("Judgments are " + judg1 + " and " + judg2) - judg1.foreach(addJudgmentFrom) - judg2.foreach(addJudgmentTo) + def findJudgments(from : List[MPath], to : List[MPath]) = { + // log("finding Judgments...") + val j1 = if (judg1.isDefined) judg1 else finder.getJudgment(from) + val j2 = if (judg2.isDefined) judg2 else finder.getJudgment(to) + // log("Judgments are " + judg1 + " and " + judg2) + j1.foreach(addJudgmentFrom) + j2.foreach(addJudgmentTo) } + } class AlignmentFinder extends frontend.Extension { override def logPrefix: String = "viewfinder" implicit private val ec = ExecutionContext.global //.fromExecutor(Executors.newFixedThreadPool(10000)) - private[refactoring] def getJudgment(ths: List[DeclaredTheory]): Option[GlobalName] = { + private[refactoring] def getJudgment(ths: List[MPath]): Option[GlobalName] = { var i = 0 var judg: Option[GlobalName] = None while (judg.isEmpty && i < ths.length) { - judg = findJudgment(ths(i)) + judg = findJudgment(controller.getAs(classOf[DeclaredTheory],ths(i))) i += 1 } judg @@ -106,104 +109,104 @@ class AlignmentFinder extends frontend.Extension { list.headOption } - // controller.simplifier.apply(th) - // val ths = th.getIncludes.map(controller.get(_).asInstanceOf[DeclaredTheory])//closer.getIncludes(th,true) findJudgmentIt(th) } - def getConfig : FinderConfig = new FinderConfig(this,report) - - def getConfig(a1 : Archive, a2 : Archive) : FinderConfig = { - val cfg = getConfig + def getFlat(mpaths : List[MPath]) : List[DeclaredTheory] = { // TODO properly var dones : mutable.HashMap[MPath,Option[List[DeclaredTheory]]] = mutable.HashMap.empty // guarantees that the dependency closure is ordered def flatten(mp : MPath) : Option[List[DeclaredTheory]] = { - dones.getOrElse(mp, { + dones.getOrElseUpdate(mp, { log("Doing: " + mp.toString) // println(mp) - val ret = controller.getO(mp) match { + controller.getO(mp) match { case Some(th : DeclaredTheory) => val rec = th.getIncludes.map(flatten) if (rec.contains(None)) None else Some((rec.flatMap(_.get) ::: List(th)).distinct) case _ => None } - dones += ((mp,ret)) - ret }) } + mpaths foreach flatten + dones.values.collect { + case Some(thl) => thl + }.toList.flatten.distinct + } + + def getHasher : Hasher = new HashesNormal(new FinderConfig(this,report)) + def addArchives(a1 : Archive, a2 : Archive, hasher : Hasher) : Unit = { var lf = a1.root / "viewfinder_order" - if (lf.exists) { + val froms = if (lf.exists) { log("Reading file " + lf) val ls = File.read(lf).split("\n").toList.distinct val mps = ls.map(s => Path.parseM(s,NamespaceMap.empty)) log("Adding " + mps.length + " theories...") - cfg.addFrom(mps.indices.map{i => + val ret = mps.indices.map{i => print("\r " + (i + 1) + " of " + mps.indices.length) controller.getAs(classOf[DeclaredTheory],mps(i)) - }.toList) + }.toList println(" Done.") + ret } else { log("Collecting theories in " + a1.id) - val ths = a1.allContent.flatMap(flatten).flatten + val ths = getFlat(a1.allContent) File.write(lf,ths.map(_.path.toString).distinct.mkString("\n")) - cfg.addFrom(ths) - dones.clear() + ths } lf = a2.root / "viewfinder_order" - if (lf.exists) { + val tos = if (lf.exists) { log("Reading file " + lf) val ls = File.read(lf).split("\n").toList.distinct val mps = ls.map(s => Path.parseM(s,NamespaceMap.empty)) log("Adding " + mps.length + " theories...") - cfg.addTo(mps.indices.map{i => + val ret = mps.indices.map{i => print("\r " + (i + 1) + " of " + mps.indices.length) controller.getAs(classOf[DeclaredTheory],mps(i)) - }.toList) + }.toList println(" Done.") + ret } else { - log("Collecting theories in " + a2.id) - val ths = a2.allContent.flatMap(flatten).flatten + log("Collecting theories in " + a1.id) + val ths = getFlat(a1.allContent) File.write(lf,ths.map(_.path.toString).distinct.mkString("\n")) - cfg.addTo(ths) - dones.clear() + ths } - cfg - } - - def run(cfg : FinderConfig) = { - val hasher = new HashesNormal(cfg) - log("Hashing...") + val commons = froms.filter(tos.contains) + hasher.cfg.findJudgments(froms.map(_.path),tos.map(_.path)) val (t,_) = Time.measure { - cfg.commonTheories foreach (t => hasher.add(t,Hasher.COMMON)) - cfg.fromTheories foreach (t => hasher.add(t,Hasher.FROM)) - cfg.toTheories foreach (t => hasher.add(t,Hasher.TO)) + commons foreach (t => hasher.add(t,Hasher.COMMON)) + froms.filterNot(commons.contains) foreach (t => hasher.add(t,Hasher.FROM)) + tos.filterNot(commons.contains) foreach (t => hasher.add(t,Hasher.TO)) } - log("Done after " + t + "ms") - val proc = new FindingProcess(this.report,cfg,hasher) - log("Multithreaded: " + cfg.isMultithreaded) - proc.run + } + + def run(hasher : Hasher) = { + val proc = new FindingProcess(this.report,hasher) + log("Multithreaded: " + hasher.cfg.isMultithreaded) + log("Judgment symbols are " + hasher.cfg.judg1 + " and " + hasher.cfg.judg2) + proc.run() } } -class FindingProcess(val report : Report, cfg : FinderConfig, hash : Hasher) extends MMTTask with Logger { +class FindingProcess(val report : Report, hash : Hasher) extends MMTTask with Logger { override def logPrefix: String = "viewfinder" implicit private val ec = ExecutionContext.global //.fromExecutor(Executors.newFixedThreadPool(10000)) - def run = { + def run(from : List[Theoryhash]= Nil, to : List[Theoryhash] = Nil) = { log("Selecting Theories to use...") - val (t1,tops1) = Time.measure(select(hash.from)) - val (t2,tops2) = Time.measure(select(hash.to)) + val (t1,tops1) = if (from.nonEmpty) (0.toLong,from) else Time.measure(select(hash.from)) + val (t2,tops2) = if (to.nonEmpty) (0.toLong,to) else Time.measure(select(hash.to)) log("Done after " + (t1 + t2) + "ms") log(tops1.length + " and " + tops2.length + " selected elements") log("Finding Views...") - val (t,alls : Set[List[Map]]) = Time.measure(if (cfg.isMultithreaded) { + val (t,alls : Set[List[Map]]) = Time.measure(if (hash.cfg.isMultithreaded) { // One thread for each pair, should speed things up val ps = tops1.flatMap(t1 => tops2.map((t1,_))) val fs = Future.sequence(ps.map(p => @@ -252,8 +255,8 @@ class FindingProcess(val report : Report, cfg : FinderConfig, hash : Hasher) ext // gets starting points for viewfinding. Defaults to Axioms and minimal_parameter_length protected def getStartingPoints(implicit allpairs : List[(Consthash, Consthash)]): List[(Consthash, Consthash)] - = (if (cfg.judg1.isDefined || cfg.judg2.isDefined) allpairs.filter(p => p._1.isProp || p._2.isProp) - else allpairs).filter(p => p._1.pars.length >= cfg.minimal_parameter_length) + = (if (hash.cfg.judg1.isDefined || hash.cfg.judg2.isDefined) allpairs.filter(p => p._1.isProp || p._2.isProp) + else allpairs).filter(p => p._1.pars.length >= hash.cfg.minimal_parameter_length) // does something with the resulting lists of pairs. diff --git a/src/mmt-api/src/main/info/kwarc/mmt/api/refactoring/Consthasher.scala b/src/mmt-api/src/main/info/kwarc/mmt/api/refactoring/Consthasher.scala index d4bd2d7f22..93b80d24d6 100644 --- a/src/mmt-api/src/main/info/kwarc/mmt/api/refactoring/Consthasher.scala +++ b/src/mmt-api/src/main/info/kwarc/mmt/api/refactoring/Consthasher.scala @@ -70,14 +70,18 @@ object Hasher { trait Hasher { + val cfg : FinderConfig + def from : List[Theoryhash] def to : List[Theoryhash] def common : List[MPath] + def get(mp : MPath) : Option[Theoryhash] + def add(th : DeclaredTheory, as : Int) : Unit } -private class HashesNormal(cfg : FinderConfig) extends Hasher { +class HashesNormal(val cfg : FinderConfig) extends Hasher { private var theories : List[(Theoryhash,Int)] = Nil private var commons : List[MPath] = Nil private var numbers : List[GlobalName] = cfg.fixing.map { a => @@ -100,11 +104,7 @@ private class HashesNormal(cfg : FinderConfig) extends Hasher { }.reverse def common = commons - private def getTheory(p : MPath) : Theoryhash = theories.find(_._1.path == p).getOrElse { - val c = commons - println(p) - ??? - }._1 // TODO shouldn't happen though + def get(p : MPath) : Option[Theoryhash] = theories.find(_._1.path == p).map(_._1) def add (th : DeclaredTheory, as : Int) = as match { case Hasher.COMMON => @@ -123,7 +123,7 @@ private class HashesNormal(cfg : FinderConfig) extends Hasher { case c : FinalConstant if !cfg.fixing.exists(a => a.alignment.from.mmturi == c.path || a.alignment.to.mmturi == c.path) => c }) foreach (c => h.addConstant(doConstant(c))) - th.getIncludes.filterNot(commons.contains).foreach(t => h.addInclude(getTheory(t))) + th.getIncludes.filterNot(commons.contains).foreach(t => h.addInclude(get(t).getOrElse( ??? ))) } h.init h diff --git a/src/mmt-odk/src/info/kwarc/mmt/mitm/Viewfinder.scala b/src/mmt-odk/src/info/kwarc/mmt/mitm/Viewfinder.scala new file mode 100644 index 0000000000..cbac4fb173 --- /dev/null +++ b/src/mmt-odk/src/info/kwarc/mmt/mitm/Viewfinder.scala @@ -0,0 +1,42 @@ +package info.kwarc.mmt.mitm + +import info.kwarc.mmt.api.MPath +import info.kwarc.mmt.api.archives.{Archive, BuildTarget, Update} +import info.kwarc.mmt.api.modules.DeclaredTheory +import info.kwarc.mmt.api.refactoring.{AlignmentFinder, FindingProcess, Hasher, HashesNormal} +import info.kwarc.mmt.api.utils.FilePath + +import scala.collection.mutable + +class Viewfinder extends BuildTarget{ + val key = "viewfinding" + + lazy val alignmentFinder : AlignmentFinder = controller.extman.get(classOf[AlignmentFinder]).headOption.getOrElse { + val af = new AlignmentFinder + controller.extman.addExtension(af) + af + } + + lazy val mitm : Archive = controller.backend.getArchive("MitM/smglom").getOrElse(???) + + override def clean(a: Archive, in: FilePath): Unit = ??? + + override def build(a: Archive, up: Update, in: FilePath): Unit = ??? + + def find(mp : MPath, to : Archive) = { + val hasher = default(mp, to) // TODO + val proc = new FindingProcess(this.report,hasher) + proc.run(from = List(hasher.get(mp).get)) + } + + private def default(mp : MPath,to : Archive) = { + val hasher = alignmentFinder.getHasher + hasher.cfg.setDoDefs(false) + hasher.cfg.setMultithreaded(false) + alignmentFinder.addArchives(mitm,to,hasher) + val news = alignmentFinder.getFlat(List(mp)).filterNot(p => mitm.allContent.contains(p.path)) + news foreach (t => hasher.add(t,Hasher.FROM)) + hasher + } + +} From b9ca31562faf720bbbd731bdba29ac50991b233c Mon Sep 17 00:00:00 2001 From: Tom Wiesing Date: Mon, 9 Apr 2018 15:11:42 +0200 Subject: [PATCH 2/8] Log errors when lmh fails --- .../main/info/kwarc/mmt/api/archives/lmh/MathHub.scala | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) diff --git a/src/mmt-api/src/main/info/kwarc/mmt/api/archives/lmh/MathHub.scala b/src/mmt-api/src/main/info/kwarc/mmt/api/archives/lmh/MathHub.scala index 0901dd9009..7dc807a3a8 100644 --- a/src/mmt-api/src/main/info/kwarc/mmt/api/archives/lmh/MathHub.scala +++ b/src/mmt-api/src/main/info/kwarc/mmt/api/archives/lmh/MathHub.scala @@ -14,6 +14,7 @@ import scala.util.Try * @param https should we use https or ssh for cloning? */ class MathHub(val controller: Controller, var local: File, var remote: URI, var https: Boolean = true) extends LMHHub { + /** implements git */ protected val git: Git = OS.detect match {case Windows => new WindowsGit() case _ => UnixGit } // PATHS @@ -170,10 +171,10 @@ class MathHub(val controller: Controller, var local: File, var remote: URI, var val success = git(local, "clone", rp, id).success if (!success) { if (lp.exists) { - log("git failed, deleting " + lp) + logError(s"git clone $rp failed, deleting $lp") lp.deleteDir } else { - log("git failed") + logError(s"git clone $rp failed") } return None } @@ -183,7 +184,7 @@ class MathHub(val controller: Controller, var local: File, var remote: URI, var log(s"checking out ${version.get}") val vSuccess = git(lp, "checkout", "-f", version.get).success if (!vSuccess) { - log("checkout failed, Local version may differ from requested version. ") + logError("checkout failed, Local version may differ from requested version. ") } } } @@ -203,7 +204,7 @@ class MathHub(val controller: Controller, var local: File, var remote: URI, var Some(new MathHubEntry(lp)) } catch { case _: Exception => - log(s"download failed, aborting") + logError(s"download of '$url' failed, aborting") None } finally { zip.delete From 865b582c6ac9f9185e84a694ccb117321133786d Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Dennis=20M=C3=BCller?= Date: Tue, 10 Apr 2018 00:10:04 +0200 Subject: [PATCH 3/8] viewfinding --- .../mmt/api/refactoring/AlignmentFinder.scala | 36 ++++-- .../mmt/api/refactoring/Consthasher.scala | 48 +++++-- .../src/info/kwarc/mmt/mitm/Viewfinder.scala | 121 ++++++++++++++++-- 3 files changed, 175 insertions(+), 30 deletions(-) diff --git a/src/mmt-api/src/main/info/kwarc/mmt/api/refactoring/AlignmentFinder.scala b/src/mmt-api/src/main/info/kwarc/mmt/api/refactoring/AlignmentFinder.scala index 0d936dd15c..7ac6cc91df 100644 --- a/src/mmt-api/src/main/info/kwarc/mmt/api/refactoring/AlignmentFinder.scala +++ b/src/mmt-api/src/main/info/kwarc/mmt/api/refactoring/AlignmentFinder.scala @@ -5,7 +5,9 @@ import info.kwarc.mmt.api.modules.DeclaredTheory import info.kwarc.mmt.api.symbols.FinalConstant import info.kwarc.mmt.api._ import info.kwarc.mmt.api.archives.Archive +import info.kwarc.mmt.api.objects.Term import info.kwarc.mmt.api.ontology.FormalAlignment +import info.kwarc.mmt.api.refactoring.Hasher.Targetable import info.kwarc.mmt.api.utils.File import info.kwarc.mmt.api.utils.time.Time @@ -246,7 +248,9 @@ class FindingProcess(val report : Report, hash : Hasher) extends MMTTask with Lo // the method used for matching two constants. Defaults to hash equality with all parameters pairwise matched up protected def matches(c: Consthash, d: Consthash)(l: List[(GlobalName, GlobalName)]): Boolean = { if (c !<> d) false - else (c.pars zip d.pars).forall { case (p, q) => p == q || l.contains((p, q)) } + else (c.pars zip d.pars).forall { case (Hasher.Symbol(p), Hasher.Symbol(q)) => p == q || l.contains((p, q)) + case _ => true + } } //selects potential matches to work with; defaults to hash-equality @@ -354,10 +358,15 @@ class FindingProcess(val report : Report, hash : Hasher) extends MMTTask with Lo def get(from : Consthash, to : Consthash)(implicit allpairs : List[(Consthash, Consthash)]) : Option[Map] = maps.getOrElseUpdate((from.name,to.name), { if (from !<> to) return None - if (from.pars == to.pars) return Some(Map(from.name, to.name, Nil, 0)) + if (from.pars == to.pars) return Some(Map(Hasher.Symbol(from.name), Hasher.Symbol(to.name), Nil, 0)) - val rec = from.pars.indices.map(i => get(from.pars(i), to.pars(i))) - if (rec.forall(_.isDefined)) Some(Map(from.name,to.name,rec.map(_.get).toList,0)) else None + val rec = from.pars.indices.map(i => + (from.pars(i),to.pars(i)) match { + case (Hasher.Symbol(f),Hasher.Symbol(t)) => get(f,t) + case _ => None + } + ) + if (rec.forall(_.isDefined)) Some(Map(Hasher.Symbol(from.name),Hasher.Symbol(to.name),rec.map(_.get).toList,0)) else None }) } @@ -375,15 +384,17 @@ class FindingProcess(val report : Report, hash : Hasher) extends MMTTask with Lo current._1.pars.indices.foldLeft( Some((current._1.name, current._2.name) :: cp).asInstanceOf[Option[List[(GlobalName, GlobalName)]]] )((pt, i) => - pt match { - case None => None /* + (pt,current._1.pars(i),current._2.pars(i)) match { + case (None,_,_) => None /* case Some(path) if path contains ((current._1.pars(i), current._2.pars(i))) => Some(((current._1.pars(i), current._2.pars(i)) :: path).distinct) */ // case Some(path) if path exists (p => p._1 == current._1.pars(i)) => None - case Some(path) => pairs.collectFirst { case p if p._1.name == current._1.pars(i) && p._2.name == current._2.pars(i) => p } match { + case (Some(path),Hasher.Symbol(s1),Hasher.Symbol(s2)) => + pairs.collectFirst { case p if p._1.name == s1 && p._2.name == s2 => p } match { case None => None case Some(x) => iterate(pairs, x, path) } + case _ => pt } ).map(_.distinct) } @@ -414,12 +425,21 @@ class FindingProcess(val report : Report, hash : Hasher) extends MMTTask with Lo } -case class Map(from : GlobalName, to : GlobalName, requires : List[Map], value : Double) { +case class Map(from : Targetable, to : Targetable, requires : List[Map], value : Double) { + // val isSimple = from.isInstanceOf[Hasher.Symbol] && to.isInstanceOf[Hasher.Symbol] def asString() = "(" + value + ") " + from + " --> " + to + " requires: " + requires.mkString("["," , ","]") def allRequires : List[Map] = (requires.flatMap(_.requires) ::: requires).distinct override def toString: String = from + " -> " + to } +trait Preprocessor { + def apply(c : FinalConstant) : FinalConstant + + def +(that : Preprocessor) : Preprocessor = { c => + that.apply(this.apply(c)) + } +} + /* case class FinderResult(from : Theoryhash,to : Theoryhash, entries : List[(GlobalName,GlobalName,Int)], includes : List[FinderResult]) { diff --git a/src/mmt-api/src/main/info/kwarc/mmt/api/refactoring/Consthasher.scala b/src/mmt-api/src/main/info/kwarc/mmt/api/refactoring/Consthasher.scala index 93b80d24d6..829a1e642f 100644 --- a/src/mmt-api/src/main/info/kwarc/mmt/api/refactoring/Consthasher.scala +++ b/src/mmt-api/src/main/info/kwarc/mmt/api/refactoring/Consthasher.scala @@ -5,16 +5,16 @@ import info.kwarc.mmt.api.modules.DeclaredTheory import info.kwarc.mmt.api.objects._ import info.kwarc.mmt.api.symbols.FinalConstant import info.kwarc.mmt.api.utils._ -import info.kwarc.mmt.api.{GlobalName, LocalName, MPath} +import info.kwarc.mmt.api.{GlobalName, LocalName, MPath, utils} import scala.collection.mutable -case class Consthash(name:GlobalName, hash: List[Int], pars: List[GlobalName], - isProp: Boolean, optDef : Option[(Int,List[GlobalName])]) { +case class Consthash(name:GlobalName, hash: List[Int], pars: List[Hasher.Targetable], + isProp: Boolean, optDef : Option[(Int,List[Hasher.Targetable])]) { //def matches(l:List[(GlobalName,GlobalName)])(that:Consthash):Boolean = newPairs(l)(that).isEmpty - override def toString = name.toString + "[" + pars.map(_.name.toString).mkString(", ") + "]" + - optDef.map(p => " = [" + p._2.map(_.name.toString).mkString(", ") + "]").getOrElse("") + override def toString = name.toString + "[" + pars.map(_.toString).mkString(", ") + "]" + + optDef.map(p => " = [" + p._2.map(_.toString).mkString(", ") + "]").getOrElse("") def <>(that : Consthash) = this.hash == that.hash && this.pars.length == that.pars.length def !<>(that :Consthash) = !(this <> that) @@ -66,6 +66,34 @@ object Hasher { val FROM = 0 val TO = 1 val COMMON = 2 + + trait Targetable // todo symbols, free variables, ... + case class Symbol(gn : GlobalName) extends Targetable { + override def toString: String = gn.toString + } + class Complex(val tm : Term) extends Targetable { + override def equals(obj: scala.Any): Boolean = obj match { + case that : Complex => this.tm == that.tm + case _ => false + } + def asTerm : Term = OMA(OMS(utils.mmt.mmtcd ? "Targetable"),List(tm)) + } + + object Complex { + val path = utils.mmt.mmtcd ? "Targetable" + def unapply(tm : Term) = tm match { + case OMA(OMS(`path`),List(itm)) => Some(new Complex(itm)) + case _ => None + } + def apply(tm : Term) = OMA(OMS(utils.mmt.mmtcd ? "Targetable"),List(tm)) + } + /* + case class FreeVar(ln : LocalName) extends Targetable { + val tm = OMBINDC(OMS(utils.mmt.mmtcd ? "TargetableVariable"),VarDecl) + + override def toString: String = "Variable(" + } + */ } trait Hasher { @@ -131,21 +159,25 @@ class HashesNormal(val cfg : FinderConfig) extends Hasher { private def doConstant(c:FinalConstant) : Consthash = { var isAxiom = false - var pars : List[GlobalName] = Nil + var pars : List[Hasher.Targetable] = Nil def traverse(t: Term)(implicit vars : List[LocalName]) : List[Int] = { // assumption: at most one alignment applicable val al = cfg.fixing.find(_.applicable(t)) val tm = al.map(_.apply(t)).getOrElse(t) tm match { + case Hasher.Complex(itm) => List(-1,if (pars.contains(itm)) pars.length - (pars.indexOf(itm)+1) else { + pars ::= itm + pars.length-1 + }) case OMV(name) => List(0, 2 * vars.indexOf(name)) case OMS(path) => if (cfg.judg1.contains(path) || cfg.judg2.contains(path)) isAxiom = true val nopt = numbers.indexOf(path) val (i,j) = nopt match { - case -1 => (1,if (pars.contains(path)) pars.length - (pars.indexOf(path)+1) else { - pars ::= path + case -1 => (1,if (pars.contains(Hasher.Symbol(path))) pars.length - (pars.indexOf(path)+1) else { + pars ::= Hasher.Symbol(path) pars.length-1 }) case n => (0,n) diff --git a/src/mmt-odk/src/info/kwarc/mmt/mitm/Viewfinder.scala b/src/mmt-odk/src/info/kwarc/mmt/mitm/Viewfinder.scala index cbac4fb173..54b27ac154 100644 --- a/src/mmt-odk/src/info/kwarc/mmt/mitm/Viewfinder.scala +++ b/src/mmt-odk/src/info/kwarc/mmt/mitm/Viewfinder.scala @@ -1,15 +1,16 @@ package info.kwarc.mmt.mitm -import info.kwarc.mmt.api.MPath -import info.kwarc.mmt.api.archives.{Archive, BuildTarget, Update} -import info.kwarc.mmt.api.modules.DeclaredTheory -import info.kwarc.mmt.api.refactoring.{AlignmentFinder, FindingProcess, Hasher, HashesNormal} +import info.kwarc.mmt.api.{DPath, GlobalName, MPath} +import info.kwarc.mmt.api.archives._ +import info.kwarc.mmt.api.documents.Document +import info.kwarc.mmt.api.modules.{DeclaredTheory, DeclaredView} +import info.kwarc.mmt.api.objects.{OMS, Term} +import info.kwarc.mmt.api.refactoring._ +import info.kwarc.mmt.api.symbols.FinalConstant import info.kwarc.mmt.api.utils.FilePath +import info.kwarc.mmt.lf.ApplySpine -import scala.collection.mutable - -class Viewfinder extends BuildTarget{ - val key = "viewfinding" +class Viewfinder extends Exporter { lazy val alignmentFinder : AlignmentFinder = controller.extman.get(classOf[AlignmentFinder]).headOption.getOrElse { val af = new AlignmentFinder @@ -19,12 +20,11 @@ class Viewfinder extends BuildTarget{ lazy val mitm : Archive = controller.backend.getArchive("MitM/smglom").getOrElse(???) - override def clean(a: Archive, in: FilePath): Unit = ??? - - override def build(a: Archive, up: Update, in: FilePath): Unit = ??? - def find(mp : MPath, to : Archive) = { val hasher = default(mp, to) // TODO + val previous = hasher.common ::: hasher.from.map(_.path) + val news = alignmentFinder.getFlat(List(mp)).filterNot(p => previous.contains(p.path)) + news foreach (t => hasher.add(t,Hasher.FROM)) val proc = new FindingProcess(this.report,hasher) proc.run(from = List(hasher.get(mp).get)) } @@ -34,9 +34,102 @@ class Viewfinder extends BuildTarget{ hasher.cfg.setDoDefs(false) hasher.cfg.setMultithreaded(false) alignmentFinder.addArchives(mitm,to,hasher) - val news = alignmentFinder.getFlat(List(mp)).filterNot(p => mitm.allContent.contains(p.path)) - news foreach (t => hasher.add(t,Hasher.FROM)) hasher } + val key = "viewfinding" + override val outExt = "viewfinding" + + def exportTheory(t: DeclaredTheory, bf: BuildTask) { /* + rh("\n") + rh("\n") + t.getDeclarations foreach {d => + d.getComponents.foreach { + case DeclarationComponent(comp, tc: AbstractTermContainer) => + tc.get.foreach {t => + val node = {t.toCML} + rh(node.toString + "\n") + } + case _ => + } + } + rh("\n") */ + } + + def exportView(v: DeclaredView, bf: BuildTask) { + //excluding expressions from views for now + } + + + def exportNamespace(dpath: DPath, bd: BuildTask, namespaces: List[BuildTask], modules: List[BuildTask]) { + //Nothing to do - MathML in namespaces + } + + def exportDocument(doc : Document, bt: BuildTask) { + //Nothing to do - no MathML at document level + } + } + +class LFClassicHOLPreprocessor(ded : GlobalName, and : GlobalName, not : GlobalName, + or : Option[GlobalName], + implies : Option[GlobalName], + equiv : Option[GlobalName], + equals : Option[GlobalName], + forall : Option[GlobalName], + exists : Option[GlobalName], + hoasapply : Option[GlobalName] + ) extends Preprocessor { + + private object Apply { + def apply(f : Term, args : List[Term]) = if (hoasapply.isDefined) { + args.foldLeft(f)((nf,a) => ApplySpine(OMS(hoasapply.get), nf,a)) + } else ApplySpine(f,args :_*) + def unapply(tm : Term) : Option[(Term,List[Term])] = if (hoasapply.isDefined) { + val hoas = hoasapply.get + tm match { + case ApplySpine(OMS(`hoas`),List(nf,a)) => Some(unapply(nf).map(p => (p._1, p._2 ::: a :: Nil)).getOrElse((nf,List(a)))) + } + } else ApplySpine.unapply(tm) + } + + private object Ded { + ??? + } + + private object And { + ??? + } + + private object Not { + ??? + } + + private object Or { + ??? + } + + private object Implies { + ??? + } + + private object Equiv { + ??? + } + + private object Equals { + ??? + } + + private object Forall { + ??? + } + + private object Exists { + ??? + } + + def apply(c : FinalConstant): FinalConstant = ??? + + private def leq(t1 : Term, t2 : Term) : Boolean = t1.subobjects.length <= t2.subobjects.length +} \ No newline at end of file From 8a19fb3af752a5734581d95fc726ac7fe0b4e83d Mon Sep 17 00:00:00 2001 From: Florian Rabe Date: Tue, 10 Apr 2018 13:50:28 +0200 Subject: [PATCH 4/8] --- .../mmt/api/objects/ModuleOperators.scala | 27 +++++++++---------- 1 file changed, 12 insertions(+), 15 deletions(-) diff --git a/src/mmt-api/src/main/info/kwarc/mmt/api/objects/ModuleOperators.scala b/src/mmt-api/src/main/info/kwarc/mmt/api/objects/ModuleOperators.scala index 146784b412..5c3871fd1a 100644 --- a/src/mmt-api/src/main/info/kwarc/mmt/api/objects/ModuleOperators.scala +++ b/src/mmt-api/src/main/info/kwarc/mmt/api/objects/ModuleOperators.scala @@ -51,9 +51,9 @@ object Morph { } /** transform a morphism into a list of morphisms by using associativity of composition */ - def associateComposition(m: Term): List[Term] = m match { - case OMCOMP(ms) => ms flatMap associateComposition - case _ => List(m) + def associateComposition(mors: List[Term]): List[Term] = mors flatMap { + case OMCOMP(ms) => associateComposition(ms) + case m => List(m) } /** pre: mor is a valid morphism and includes all implicit morphisms @@ -62,19 +62,20 @@ object Morph { * @param preserveType if true, identity morphisms that restrict the type domain are preserved if they cannot be reduced; otherwise, they become OMCOMP() */ def simplify(mor: Term, preserveType: Boolean = false)(implicit lib: Lookup): Term = { - val mS = OMCOMP(associateComposition(mor)) - mS match { - case OMMOD(p) => mS + mor match { + case OMMOD(p) => mor case OMS(p) => // TODO dangerous assumption that [mpath] is always a PlainInclude! if (p.name.length == 1 && p.name.steps.head.isInstanceOf[ComplexStep]) OMCOMP() else - mS - case OMIDENT(t) => if (preserveType) mS else OMCOMP() + mor + case OMIDENT(t) => if (preserveType) mor else OMCOMP() case OMINST(t,args) => mor case OMStructuralInclude(f,t) => mor case OMCOMP(ms) => - var left = ms map {m => simplify(m,true)} //TODO can we skip simplification? Nothing much happens because there are no nested compositions anymore + val parts = associateComposition(ms) + var partsS = parts map {m => simplify(m,true)} //TODO can we skip simplification? Nothing much happens because there are no nested compositions anymore + var left = associateComposition(partsS) // usually redundant, but simplification may occasionally introduce a composition var result: List[Term] = Nil // we go through all morphisms m in 'ms', building the simplification in 'result' (in reverse order) // we put R = OMCOMP(result.reverse) for the morphism processed so far @@ -181,12 +182,8 @@ object Morph { case OMIDENT(_) => false case _ => true } - // aggregate to a morphism if necessary - result match { - case Nil => OMCOMP() - case h :: Nil => h - case msS => OMCOMP(msS) - } + // OMCOMP disappears if result has length 1 + OMCOMP(result) } } From d13141aac72728e3b85627ec0e15ad8042bd5290 Mon Sep 17 00:00:00 2001 From: Tom Wiesing Date: Tue, 10 Apr 2018 17:18:36 +0200 Subject: [PATCH 5/8] Fix pdflatex target Due to a scala bug in the Process.cat function, the pdflatex target was broken for files that required a pre- and post-amble. Previously, the target concatinated the input files and passed them via STDIN to pdflatex. Instead, this commit works around the issue by creating a temporary input file, which is then passed as a normal command line argument to pdflatex. --- .../src/info/kwarc/mmt/stex/LaTeXML.scala | 29 +++++++++++++++---- 1 file changed, 23 insertions(+), 6 deletions(-) diff --git a/src/mmt-stex/src/info/kwarc/mmt/stex/LaTeXML.scala b/src/mmt-stex/src/info/kwarc/mmt/stex/LaTeXML.scala index 1bec9d62c0..4e4ac853a6 100644 --- a/src/mmt-stex/src/info/kwarc/mmt/stex/LaTeXML.scala +++ b/src/mmt-stex/src/info/kwarc/mmt/stex/LaTeXML.scala @@ -484,15 +484,32 @@ class PdfLatex extends LaTeXBuildTarget { protected def runPdflatex(bt: BuildTask, output: StringBuffer): Int = { val in = bt.inFile - val pbCat = if (noAmble(in)) Process.cat(in.toJava) - else Process.cat(Seq(getAmbleFile("pre", bt), in, - getAmbleFile("post", bt)).map(_.toJava)) - val pb = pbCat #| Process(Seq(pdflatexPath, "-jobname", - in.stripExtension.getName, "-interaction", "scrollmode"), - in.up, env(bt): _*) + + // find files that have to be read + val texFiles = if(noAmble(in)){ List(in) + } else { + List(getAmbleFile("pre", bt), in, getAmbleFile("post", bt)) + } + + // create a temporary file to concatinate the inputs + val tmpFile = bt.inFile.addExtension("tmp") + File.write(tmpFile, texFiles.map(File.read) :_*) + + // create a process to compile the tex file + val pb = Process( + Seq(pdflatexPath, "-jobname", in.stripExtension.getName, "-interaction", "scrollmode", tmpFile.toString), + in.up, env(bt): _* + ) + + // run the process and delete the temporary file if it was successfull val exit = timeout(pb, procLogger(output, pipeOutput = pipeOutput)) + if (exit == 0) tmpFile.delete + + // and write a logFile val pdflogFile = in.setExtension("pdflog") if (!pipeOutput) File.write(pdflogFile, output.toString) + + // and return exit } From 4dd6c1704652547b96715437592197685a3f9f93 Mon Sep 17 00:00:00 2001 From: Florian Rabe Date: Tue, 10 Apr 2018 21:24:57 +0200 Subject: [PATCH 6/8] --- src/jEdit-mmt/src/info/kwarc/mmt/jedit/MMTOptions.scala | 2 +- src/jEdit-mmt/src/info/kwarc/mmt/jedit/MMTPlugin.scala | 7 ++++++- .../src/main/info/kwarc/mmt/api/frontend/Controller.scala | 4 ---- 3 files changed, 7 insertions(+), 6 deletions(-) diff --git a/src/jEdit-mmt/src/info/kwarc/mmt/jedit/MMTOptions.scala b/src/jEdit-mmt/src/info/kwarc/mmt/jedit/MMTOptions.scala index ee5df802b8..527439e0fc 100644 --- a/src/jEdit-mmt/src/info/kwarc/mmt/jedit/MMTOptions.scala +++ b/src/jEdit-mmt/src/info/kwarc/mmt/jedit/MMTOptions.scala @@ -86,7 +86,7 @@ class BooleanOption(val key: String, val label: String) extends MMTOption[Boolea object MMTOptions { val startup = new StringOption("startup", "custom startup msl file") val config = new StringOption("config", "custom configuration file") - val archives = new StringOption("archives", "custom folder that contains archives") + val archives = new StringOption("content folder (local mathhub root)", "local folder that contains archives") val lowAsciiDelims = new BooleanOption("lowAsciiDelims", "use ASCII 28-31 as delimiters") val semantichighlighting = new BooleanOption("SemanticHighlighting","Semantic highlighting (does not work yet)") /** the list of all options */ diff --git a/src/jEdit-mmt/src/info/kwarc/mmt/jedit/MMTPlugin.scala b/src/jEdit-mmt/src/info/kwarc/mmt/jedit/MMTPlugin.scala index d3df24c1b2..6e84afc31a 100644 --- a/src/jEdit-mmt/src/info/kwarc/mmt/jedit/MMTPlugin.scala +++ b/src/jEdit-mmt/src/info/kwarc/mmt/jedit/MMTPlugin.scala @@ -60,7 +60,12 @@ class MMTPlugin extends EBPlugin with Logger { errorlist.ErrorSource.registerErrorSource(errorSource) val archives = MMTOptions.archives.get orElse controller.getMathHub.map(_.local.toString) getOrElse "mars" - controller.addArchive(home resolve archives) + val archivesFolder = home resolve archives + controller.addArchive(archivesFolder) + // if no lmh root has been defined (e.g., in the custom mmtrc file), we use the archives folder + if (controller.getMathHub.isEmpty && archives != "mars") { + controller.getConfig.addEntry(LMHConf(archivesFolder, true, None)) + } // status bar is not actually available yet at this point controller.report.addHandler(StatusBarLogger) controller.extman.addExtension(mmtListener) diff --git a/src/mmt-api/src/main/info/kwarc/mmt/api/frontend/Controller.scala b/src/mmt-api/src/main/info/kwarc/mmt/api/frontend/Controller.scala index cf2f70fd32..175a32c49e 100644 --- a/src/mmt-api/src/main/info/kwarc/mmt/api/frontend/Controller.scala +++ b/src/mmt-api/src/main/info/kwarc/mmt/api/frontend/Controller.scala @@ -158,22 +158,18 @@ class Controller extends ROController with ActionHandling with Logger { /** integrate a configuration into the current state */ def loadConfig(conf: MMTConfig, loadEverything: Boolean) { state.config.add(conf) - // add entries to the namespace conf.getEntries(classOf[NamespaceConf]).foreach {case NamespaceConf(id,uri) => state.nsMap = state.nsMap.add(id, uri) } - // add archives to the MathPath conf.getEntries(classOf[MathPathConf]).foreach {c => addArchive(c.local) } - // update the lmh cache conf.getEntries(classOf[LMHConf]).foreach { c => lmh = Some(new MathHub(this, c.local, c.remote.getOrElse(MathHub.defaultURL), c.https)) } - if (loadEverything) { loadAllArchives(conf) loadAllNeededTargets(conf) From ae44c467c99f5fec74cec558b9369b12448f4b3f Mon Sep 17 00:00:00 2001 From: Florian Rabe Date: Tue, 10 Apr 2018 21:53:36 +0200 Subject: [PATCH 7/8] --- src/jEdit-mmt/src/info/kwarc/mmt/jedit/MMTOptions.scala | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/jEdit-mmt/src/info/kwarc/mmt/jedit/MMTOptions.scala b/src/jEdit-mmt/src/info/kwarc/mmt/jedit/MMTOptions.scala index 527439e0fc..d3e21b5fbc 100644 --- a/src/jEdit-mmt/src/info/kwarc/mmt/jedit/MMTOptions.scala +++ b/src/jEdit-mmt/src/info/kwarc/mmt/jedit/MMTOptions.scala @@ -86,7 +86,7 @@ class BooleanOption(val key: String, val label: String) extends MMTOption[Boolea object MMTOptions { val startup = new StringOption("startup", "custom startup msl file") val config = new StringOption("config", "custom configuration file") - val archives = new StringOption("content folder (local mathhub root)", "local folder that contains archives") + val archives = new StringOption("archives", "local folder that contains archives (mathhub root)") val lowAsciiDelims = new BooleanOption("lowAsciiDelims", "use ASCII 28-31 as delimiters") val semantichighlighting = new BooleanOption("SemanticHighlighting","Semantic highlighting (does not work yet)") /** the list of all options */ From 299ceab383825c2225d93396871a385024a0883c Mon Sep 17 00:00:00 2001 From: Florian Rabe Date: Tue, 10 Apr 2018 22:05:37 +0200 Subject: [PATCH 8/8] --- src/jEdit-mmt/src/info/kwarc/mmt/jedit/MMTPlugin.scala | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/src/jEdit-mmt/src/info/kwarc/mmt/jedit/MMTPlugin.scala b/src/jEdit-mmt/src/info/kwarc/mmt/jedit/MMTPlugin.scala index 6e84afc31a..7d8c94c3d0 100644 --- a/src/jEdit-mmt/src/info/kwarc/mmt/jedit/MMTPlugin.scala +++ b/src/jEdit-mmt/src/info/kwarc/mmt/jedit/MMTPlugin.scala @@ -64,7 +64,9 @@ class MMTPlugin extends EBPlugin with Logger { controller.addArchive(archivesFolder) // if no lmh root has been defined (e.g., in the custom mmtrc file), we use the archives folder if (controller.getMathHub.isEmpty && archives != "mars") { - controller.getConfig.addEntry(LMHConf(archivesFolder, true, None)) + val cf = new MMTConfig + cf.addEntry(LMHConf(archivesFolder, true, None)) + controller.loadConfig(cf,false) } // status bar is not actually available yet at this point controller.report.addHandler(StatusBarLogger)