Declaration/Module.translate now take context as argument; MMTStructu…

…reChecker does 'proper' timeout; timeout can do something if it gets killed prematurely

src/jEdit-mmt/src/info/kwarc/mmt/jedit/MMTSideKick.scala

@@ -132,7 +132,7 @@ class MMTSideKick extends SideKickParser("mmt") with Logger {
    // this is called from another tread and should interrupt parsing
    override def stop {
       // this may cause an inconsistent state but calling clear in parse method should fix most problems  
-      currentTask.foreach {_.kill}
+      currentTask.foreach {_.kill((Unit) => ())}
    }
 
    private def getRegion(e: metadata.HasMetaData) : Option[SourceRegion] = SourceRef.get(e).map(_.region)

src/mmt-api/src/main/info/kwarc/mmt/api/checking/MMTStructureChecker.scala

@@ -49,6 +49,13 @@ class MMTStructureChecker(objectChecker: ObjectChecker) extends Checker(objectCh
     val cont = getContext(e)
     check(cont, e,t)
   }
+  def elabContext(th : DeclaredTheory)(implicit ce: CheckingEnvironment): Context = {
+    //val con = getContext(th)
+    val rules = RuleSet.collectRules(controller,Context.empty)
+    implicit val env = new ExtendedCheckingEnvironment(ce, objectChecker, rules, th.path)
+    implicit val task = ce.task
+    checkContext(Context.empty, getExtraInnerContext(th))
+  }
 
   /** computes the context in which an element must be checked
    *  during top-down traversal, this method allows checking to start in the middle
@@ -230,7 +237,10 @@ class MMTStructureChecker(objectChecker: ObjectChecker) extends Checker(objectCh
             val (pr, valid) = prepareTerm(t)
             if (valid) {
               val j = Inhabitable(Stack(pr.free), pr.term)
-              objectChecker(CheckingUnit(Some(c.path $ TypeComponent), context, pr.unknown, j).diesWith, env.rules)
+              val cu = if (timeout == 0) CheckingUnit(Some(c.path $ TypeComponent), context, pr.unknown, j).diesWith
+              else CheckingUnit(Some(c.path $ TypeComponent), context, pr.unknown, j).newKillButton
+              if (timeout != 0) cu.setTimeout(timeout)((Unit) => log("Timed out!"))
+              objectChecker(cu, env.rules)
             }
           }
           // == additional check in a link ==
@@ -267,7 +277,10 @@ class MMTStructureChecker(objectChecker: ObjectChecker) extends Checker(objectCh
               }
               val j = Typing(Stack(pr.free), pr.term, expTp, None)
               if (performCheck) {
-                val cr = objectChecker(CheckingUnit(Some(cp), context, unknowns, j).diesWith, env.rules)
+                val cu = if (timeout == 0) CheckingUnit(Some(cp), context, unknowns, j).diesWith
+                  else CheckingUnit(Some(cp), context, unknowns, j).newKillButton
+                if (timeout != 0) cu.setTimeout(timeout)((Unit) => log("Timed out!"))
+                val cr = objectChecker(cu, env.rules)
                 if (inferType && cr.solved) {
                   // if no expected type was known but the type could be inferred, add it
                   cr.solution.foreach { sol =>
@@ -293,7 +306,8 @@ class MMTStructureChecker(objectChecker: ObjectChecker) extends Checker(objectCh
             case _ => // cOrg has no definiens, nothing to do
           }
         }
-        //TODO the code below has to go; if at all, it should use CancellableTask, but the low-level stuff never belongs here
+        checknow
+        /*
         if (timeout == 0) checknow else {
           import scala.concurrent.duration._
           import java.util.concurrent.TimeoutException
@@ -332,6 +346,7 @@ class MMTStructureChecker(objectChecker: ObjectChecker) extends Checker(objectCh
               }
           }
         }
+        */
       case _ =>
         //succeed for everything else but signal error
         logError("unchecked " + path)

src/mmt-api/src/main/info/kwarc/mmt/api/checking/Solver.scala

@@ -664,6 +664,7 @@ class Solver(val controller: Controller, checkingUnit: CheckingUnit, val rules:
     */
    def check(j: Judgement)(implicit history: History): Boolean = {
       if (checkingUnit.isKilled) {
+        checkingUnit.killact
         return error("checking was cancelled by external signal")
       }
       history += j

src/mmt-api/src/main/info/kwarc/mmt/api/modules/Module.scala

@@ -16,7 +16,7 @@ abstract class Module(val parent : DPath, val name : LocalName) extends ContentE
    // sharper type
    def getDeclarations: List[Declaration]
    //def parameters : Context
-   def translate(newNS: DPath, prefix: LocalName, translator: Translator): Module 
+   def translate(newNS: DPath, prefix: LocalName, translator: Translator, context : Context): Module
 }
 
 /**
@@ -26,14 +26,14 @@ trait DeclaredModule extends Module with Body {
    /** the meta-theory, domain, and codomain are not part of the term components because it is just a Path */
    def getInnerContext: Context
    def asDocument: documents.Document
-   def translate(newNS: DPath, prefix: LocalName, translator: Translator): DeclaredModule 
+   def translate(newNS: DPath, prefix: LocalName, translator: Translator, context : Context): DeclaredModule
 }
 
 /**
  * Module given by existing modules/morphisms
  */
 trait DefinedModule extends Module with ModuleDefiniens {
-   def translate(newNS: DPath, prefix: LocalName, translator: Translator): DefinedModule
+   def translate(newNS: DPath, prefix: LocalName, translator: Translator, context : Context): DefinedModule
 }
 
 /**

src/mmt-api/src/main/info/kwarc/mmt/api/modules/Theory.scala

@@ -84,10 +84,11 @@ class DeclaredTheory(doc : DPath, name : LocalName, mt : Option[MPath], val para
       streamInnerNodes(rh)
       rh << "</theory>"
    }
-   def translate(newNS: DPath, newName: LocalName, translator: Translator): DeclaredTheory = {
+   def translate(newNS: DPath, newName: LocalName, translator: Translator, context : Context): DeclaredTheory = {
      val res = new DeclaredTheory(newNS, newName, mt)
+     val ncont = context ++ parameters
      getDeclarations foreach {d =>
-       res.add(d.translate(res.toTerm, LocalName.empty, translator))
+       res.add(d.translate(res.toTerm, LocalName.empty, translator,ncont))
      }
      res
    }
@@ -102,8 +103,8 @@ class DefinedTheory(doc : DPath, name : LocalName, val dfC : TermContainer) exte
     <theory name={name.last.toPath} base={doc.toPath}>
         {innerNodes}
     </theory>
-   def translate(newNS: DPath, newName: LocalName, translator: Translator): DefinedTheory = {
-     new DefinedTheory(newNS, newName, dfC.map(translator.applyModule(Context.empty, _)))
+   def translate(newNS: DPath, newName: LocalName, translator: Translator, context : Context): DefinedTheory = {
+     new DefinedTheory(newNS, newName, dfC.map(translator.applyModule(context, _)))
    }
 }
 

src/mmt-api/src/main/info/kwarc/mmt/api/modules/View.scala

@@ -49,11 +49,11 @@ class DeclaredView(doc : DPath, name : LocalName, val from : Term, val to : Term
    def getInnerContext = codomainAsContext
    def getComponents = List(DomComponent(new FinalTermContainer(from)),CodComponent(new FinalTermContainer(to)))
 
-   def translate(newNS: DPath, newName: LocalName, translator: Translator): DeclaredView = {
-     def tl(m: Term)= translator.applyModule(Context.empty, m)
+   def translate(newNS: DPath, newName: LocalName, translator: Translator,context:Context): DeclaredView = {
+     def tl(m: Term)= translator.applyModule(context, m)
      val res = new DeclaredView(newNS, newName, tl(from), tl(to), isImplicit)
      getDeclarations foreach {d =>
-       res.add(d.translate(res.toTerm, LocalName.empty, translator))
+       res.add(d.translate(res.toTerm, LocalName.empty, translator,context))
      }
      res
    }
@@ -72,8 +72,8 @@ class DeclaredView(doc : DPath, name : LocalName, val from : Term, val to : Term
 class DefinedView(doc : DPath, name : LocalName, val from : Term, val to : Term, val dfC : TermContainer, val isImplicit : Boolean)
       extends View(doc, name) with DefinedModule with DefinedLink {
    def getComponents = List(DeclarationComponent(DefComponent, dfC))
-   def translate(newNS: DPath, prefix: LocalName, translator: Translator): DefinedModule = {
-     def tl(m: Term)= translator.applyModule(Context.empty, m)
+   def translate(newNS: DPath, prefix: LocalName, translator: Translator, context : Context): DefinedModule = {
+     def tl(m: Term)= translator.applyModule(context, m)
      new DefinedView(newNS, prefix/name, tl(from), tl(to), dfC map tl, isImplicit)
    }
 }

src/mmt-api/src/main/info/kwarc/mmt/api/patterns/Instance.scala

@@ -81,7 +81,7 @@ class InstanceFeature extends StructuralFeature(Instance.feature) {
          case _ => d
        }
        val subs = (params zip args) map {case (vd,a) => Sub(vd.name, a)}
-       val dT = dN.translate(dd.home, dd.name, ApplySubs(subs) compose Renamer.prefix(pattern.module.path, dd.path))
+       val dT = dN.translate(dd.home, dd.name, ApplySubs(subs) compose Renamer.prefix(pattern.module.path, dd.path),Context.empty)
        Some(dT)
      }
    }

src/mmt-api/src/main/info/kwarc/mmt/api/proving/Searcher.scala

@@ -98,6 +98,7 @@ class Searcher(controller: Controller, val goal: Goal, rules: RuleSet, provingUn
 
    private def search(levels: Int) {
       if (provingUnit.isKilled) {
+         provingUnit.killact
         return
       }
       if (levels == 0) return

src/mmt-api/src/main/info/kwarc/mmt/api/symbols/Constant.scala

@@ -36,11 +36,11 @@ abstract class Constant extends Declaration with HasNotation {
   type ThisType = Constant
 
   // finalizes the Constant if it is not final
-  def translate(newHome: Term, prefix: LocalName, translator: Translator): FinalConstant = {
+  def translate(newHome: Term, prefix: LocalName, translator: Translator, context : Context): FinalConstant = {
      Constant(
          newHome, prefix / name, alias.map(prefix / _),
-         tpC.get map {t => translator.applyType(Context.empty, t)},
-         dfC.get map {d => translator.applyDef(Context.empty, d)},
+         tpC.get map {t => translator.applyType(context, t)},
+         dfC.get map {d => translator.applyDef(context, d)},
          rl, notC
      )
   }

src/mmt-api/src/main/info/kwarc/mmt/api/symbols/Declaration.scala

@@ -67,9 +67,9 @@ abstract class Declaration extends ContentElement {
     *  @param newHome the home theory of the result
     *  @param prefix the prefix used to form the name of the new declaration
     */
-   def translate(newHome: Term, prefix: LocalName, translator: Translator): ThisType
+   def translate(newHome: Term, prefix: LocalName, translator: Translator, context : Context): ThisType
    /** a recursively translated copy of this declaration */
-   def translate(translator: Translator): ThisType = translate(home, LocalName.empty, translator)
+   def translate(translator: Translator, context : Context): ThisType = translate(home, LocalName.empty, translator, context)
    /** a new declaration with the same path obtained by replacing fields in 'this' with corresponding fields of 'that'
     *  Unfortunately, this must take any declaration and throw an error if 'not (that : ThisType)' 
     */
@@ -97,8 +97,8 @@ class NestedModule(val home: Term, val name: LocalName, mod: Module) extends Dec
    def module = mod
    //val home = OMMOD(module.parent ? module.name.init)
    //val name = LocalName(module.name.last)
-   def translate(newHome: Term, prefix: LocalName, translator: Translator): NestedModule = {
-     val modT = mod.translate(utils.mmt.mmtbase, LocalName(newHome.toMPath/prefix)/name, translator)
+   def translate(newHome: Term, prefix: LocalName, translator: Translator, context : Context): NestedModule = {
+     val modT = mod.translate(utils.mmt.mmtbase, LocalName(newHome.toMPath/prefix)/name, translator,context)
      new NestedModule(newHome, prefix/name, modT)
    }
    //TODO this is where patterns (seen as defined theories) can be mapped to larger theories

src/mmt-api/src/main/info/kwarc/mmt/api/symbols/DerivedDeclaration.scala

@@ -56,9 +56,9 @@ class DerivedDeclaration(h: Term, name: LocalName, override val feature: String,
     feature + s1 + tpC.get.map(" " + _.toString).getOrElse("") + s2
   }
 
-  override def translate(newHome: Term, prefix: LocalName, translator: Translator): DerivedDeclaration = {
+  override def translate(newHome: Term, prefix: LocalName, translator: Translator,context : Context): DerivedDeclaration = {
      // translate this as a [[NestedModue]], then extend the result to a DerivedDeclaration
-     val superT = super.translate(newHome, prefix, translator) // temporary, will be used to build result
+     val superT = super.translate(newHome, prefix, translator,context) // temporary, will be used to build result
      val tpT = tpC.get map {tp => translator.applyType(Context.empty, tp)}
      // splice super in to res
      val res = new DerivedDeclaration(superT.home, superT.name, feature, TermContainer(tpT), notC)
@@ -261,7 +261,7 @@ class GenerativePushout extends StructuralFeature("generative") with IncludeLike
             val rest = name.drop(dd.name.steps.length)
             body.getO(rest) map {
               case d: Declaration =>
-                val dT = d.translate(parent.toTerm, dd.name, translator)
+                val dT = d.translate(parent.toTerm, dd.name, translator,Context.empty)
                 val dTM = dd.module.getO(rest) match {
                   case None => dT
                   case Some(a) => dT merge a
@@ -428,7 +428,7 @@ class BoundTheoryParameters(id : String, pi : GlobalName, lambda : GlobalName, a
         case d if body.getDerivedDeclarations(feature).exists(i => d.getOrigin == ElaborationOf(i.path)) => Nil
         case d =>
           // println(controller.presenter.asString(d))
-          val ret = d.translate(parent.toTerm, prefix, translator)
+          val ret = d.translate(parent.toTerm, prefix, translator,Context.empty)
           // println(controller.presenter.asString(ret))
           List(ret)//d.translate(parent.toTerm, prefix, translator))
       /*  DM's old code

src/mmt-api/src/main/info/kwarc/mmt/api/symbols/RuleConstant.scala

@@ -23,8 +23,8 @@ class RuleConstant(val home : Term, val name : LocalName, val tp: Term, var df:
    def getDeclarations = Nil
    type ThisType = RuleConstant
    /** translated rule must still be created from translated type */
-   def translate(newHome: Term, prefix: LocalName, translator: Translator) = {
-     new RuleConstant(newHome, prefix/name, translator.applyType(Context.empty, tp), None)
+   def translate(newHome: Term, prefix: LocalName, translator: Translator, context : Context) = {
+     new RuleConstant(newHome, prefix/name, translator.applyType(context, tp), None)
    }
    def merge(that: Declaration) = mergeError(that)
 }

src/mmt-api/src/main/info/kwarc/mmt/api/symbols/Structure.scala

@@ -60,11 +60,11 @@ class DeclaredStructure(val home : Term, val name : LocalName, val tpC: TermCont
       extends Structure with DeclaredLink {
    def getComponents = List(DomComponent(tpC))
 
-   def translate(newHome: Term, prefix: LocalName, translator: Translator): DeclaredStructure = {
+   def translate(newHome: Term, prefix: LocalName, translator: Translator,context : Context): DeclaredStructure = {
      def tl(m: Term)= translator.applyModule(Context.empty, m)
      val res = new DeclaredStructure(home, prefix/name, tpC map tl, isImplicit)
      getDeclarations foreach {d =>
-       res.add(d.translate(res.toTerm, LocalName.empty, translator))
+       res.add(d.translate(res.toTerm, LocalName.empty, translator,context))
      }
      res
    }
@@ -104,8 +104,8 @@ class DefinedStructure(val home : Term, val name : LocalName,
       extends Structure with DefinedLink {
    def getComponents = List(DomComponent(tpC), DefComponent(dfC))
 
-   def translate(newHome: Term, prefix: LocalName, translator: Translator): DefinedStructure = {
-     def tl(m: Term)= translator.applyModule(Context.empty, m)
+   def translate(newHome: Term, prefix: LocalName, translator: Translator, context : Context): DefinedStructure = {
+     def tl(m: Term)= translator.applyModule(context, m)
      new DefinedStructure(home, prefix/name, tpC map tl, dfC map tl, isImplicit)
    }
    def merge(that: Declaration): DefinedStructure = {

src/mmt-api/src/main/info/kwarc/mmt/api/uom/ElaborationBasedSimplifier.scala

@@ -2,13 +2,14 @@ package info.kwarc.mmt.api.uom
 
 import info.kwarc.mmt.api._
 import frontend._
+import info.kwarc.mmt.api.checking.{Checker, CheckingEnvironment, MMTStructureChecker, RelationHandler}
 import modules._
 import symbols._
 import patterns._
 import objects._
-
 import utils.MyList.fromList
-import collection.immutable.{HashSet, HashMap}
+
+import collection.immutable.{HashMap, HashSet}
 
 /** used by [[MMTStructureSimplifier]] */
 case class ByStructureSimplifier(home: Term, view: Term) extends Origin
@@ -128,10 +129,14 @@ class ElaborationBasedSimplifier(oS: uom.ObjectSimplifier) extends Simplifier(oS
               val elab = sf.elaborate(parent, dd)
               dd.module.setOrigin(GeneratedBy(dd.path))
               val simp = oS.toTranslator(rules)
-              elab.getDeclarations/*.map {d =>
-                val dS = d.translate(simp)
+             val checker = controller.extman.get(classOf[Checker], "mmt").getOrElse {
+               throw GeneralError(s"no mmt checker found")
+             }.asInstanceOf[MMTStructureChecker]
+             val cont = checker.elabContext(parent)(new CheckingEnvironment(new ErrorLogger(report), RelationHandler.ignore,new MMTTask{}))
+              elab.getDeclarations.map {d =>
+                val dS = d.translate(simp,cont)
                 dS
-              }*/
+              }
          }
       case _ =>
         Nil

src/mmt-api/src/main/info/kwarc/mmt/api/utils/CancellableTask.scala

@@ -11,13 +11,19 @@ import java.lang.Thread
  */
 
 class KillButton {
-  private var killed: Boolean = false
+  @volatile private var killed: Boolean = false
+  @volatile private var action: Option[Unit => Any] = None
 
-  def press {
+  def press[A](f : Unit => A) {
     killed = true
+    action = Some(f)
   }
 
   def isPressed = killed
+  def doAction : Any = {
+    action.foreach(f => f.apply())
+    action = None
+  }
 
 }
 
@@ -32,12 +38,13 @@ trait Killable {
   private var killButton: Option[KillButton] = None
 
   /** signals aborting of processing */
-  def kill {
-    killButton.foreach(_.press)
+  def kill[A](f : Unit => A) {
+    killButton.foreach(_.press(f))
   }
 
   /** processing should be aborted gracefully if true */
-  def isKilled = killButton.map(_.isPressed).getOrElse(false)
+  def isKilled = killButton.exists(_.isPressed)
+  def killact = killButton.foreach(_.doAction)
 
   /**
    * gives a killable object the same kill button as one that is already around
@@ -48,12 +55,17 @@ trait Killable {
     this.killButton = that.killButton
     this
   }
+
+  def newKillButton: this.type = {
+    this.killButton = Some(new KillButton)
+    this
+  }
 
   /** presses the kill button after the specified number of milli seconds */
-  def setTimeout(millisec: Int) {
+  def setTimeout[A](millisec: Int)(f : Unit => Unit) {
     Future {
       Thread.sleep(millisec)
-      killButton.foreach(_.press)
+      killButton.foreach(_.press(f))
     }
   }
 

src/mmt-mizar/src/info/kwarc/mmt/mizar/translator/Controller.scala

@@ -94,7 +94,7 @@ object TranslationController {
      org.omdoc.latin.foundations.mizar.IntroductionRule.allRules.foreach {rules.declares(_)}
      val complifier = controller.complifier(rules).toTranslator
      try {
-       d.translate(complifier)
+       d.translate(complifier,Context.empty)
      } catch {case e: Exception =>
        println("error while complifying instance " + d.path)
        d

src/mmt-pvs/src/info/kwarc/mmt/pvs/Translator.scala

@@ -157,7 +157,7 @@ class PVSImportTask(val controller: Controller, bt: BuildTask, index: Document =
         val checker = controller.extman.get(classOf[Checker], "mmt").getOrElse {
           throw GeneralError(s"no checker $id found")
         }.asInstanceOf[MMTStructureChecker]
-        ths foreach (p => checker.timeoutCheck(p,180)(
+        ths foreach (p => checker.timeoutCheck(p,30000)(
           new CheckingEnvironment(new ErrorLogger(report), RelationHandler.ignore,this)))
       }
       index(doc)