Skip to content

Commit

Permalink
Mostly metamath stuff, I think
Browse files Browse the repository at this point in the history
  • Loading branch information
@Jazzpirate
Jazzpirate committed Aug 30, 2016
1 parent 6daa5a5 commit 0e5bcad
Show file tree
Hide file tree
Showing 8 changed files with 75 additions and 48 deletions.
3 changes: 3 additions & 0 deletions src/mmt-api/src/main/info/kwarc/mmt/api/symbols/DerivedDeclaration.scala
View file
Expand Up @@ -189,6 +189,9 @@ class BoundTheoryParameters(id : String, pi : GlobalName, lambda : GlobalName, a
case tc: TermContainer => tc.get.getOrElse {
throw GetError("")
}
case mc : MPathContainer => mc.get.getOrElse {
throw GetError("")
}
case _ =>
throw GetError("")
}
Expand Down
76 changes: 46 additions & 30 deletions src/mmt-metamath/src/info/kwarc/mmt/metamath/LFTranslator.scala
View file
Expand Up @@ -4,8 +4,9 @@ import scala.collection.mutable.HashMap
import scala.collection.mutable.Stack
import scala.collection.mutable.TreeSet
import org.metamath.scala._
import info.kwarc.mmt.api.LocalName
import info.kwarc.mmt.api._
import info.kwarc.mmt.api.archives.BuildTask
import info.kwarc.mmt.api.checking.{Checker, CheckingEnvironment, RelationHandler}
import info.kwarc.mmt.api.documents.{Document, MRef}
import info.kwarc.mmt.api.frontend.Controller
import info.kwarc.mmt.api.frontend.Logger
Expand All @@ -17,43 +18,47 @@ import info.kwarc.mmt.api.objects.OMV
import info.kwarc.mmt.api.objects.Term
import info.kwarc.mmt.api.opaque.OpaqueText
import info.kwarc.mmt.api.opaque.StringFragment
import info.kwarc.mmt.api.symbols
import info.kwarc.mmt.lf.Apply
import info.kwarc.mmt.lf.Arrow
import info.kwarc.mmt.lf.Lambda
import info.kwarc.mmt.lf.Pi
import info.kwarc.mmt.lf.LF

class LFTranslator(val controller: Controller, bt: BuildTask, index: Document => Unit) extends Logger {
def logPrefix = "mm-omdoc"
protected def report = controller.report

val path = bt.narrationDPath.^!.^!
val path = bt.narrationDPath

def addDatabase(db: Database): Document = {
val mod = Metamath.setmm
val doc = new Document(path, root = true)
controller add doc
val theory = new DeclaredTheory(path, mod.name, Some(LF.theoryPath), Context.empty)
val theory = new DeclaredTheory(mod.doc, mod.name, Some(Metamath.prelude))
controller add theory
controller add MRef(doc.path, theory.path)
val tr = new LFDBTranslator()(db)
db.decls foreach {
// TODO restricted to the first 1000 constants for inspection
val consts = db.decls.filter{case c: Comment => false case _ => true}
consts/*.dropRight(consts.length - 1000)*/ foreach {
case a: Assert if a.syntax || a.typecode.id == "|-" =>
controller add symbols.Constant(OMMOD(mod), LocalName(a.label), Nil,
controller add symbols.Constant(theory.toTerm, LocalName(a.label), Nil,
Some(tr.translateAssert(a)), tr.translateProof(a), None)
case c: Comment =>
controller add new OpaqueText(mod.toDPath, List(StringFragment(c.text)))
controller add new OpaqueText(theory.asDocument.path, List(StringFragment(c.text)))
case _ =>
}
val checker = controller.extman.get(classOf[Checker], "mmt").getOrElse {
throw GeneralError(s"no MMT checker found")
}
checker(theory)(new CheckingEnvironment(new ErrorLogger(report), RelationHandler.ignore))
doc
}
}

class LFDBTranslator(implicit db: Database) {
val boundVars = new HashMap[Assert, Array[Option[Array[Byte]]]]
val syntaxToDefn = new HashMap[Assert, Assert]
val alignments = new HashMap[Assert, String]
val alignments = new HashMap[Assert, GlobalName]

val SET = db.syms("set")
val DED = db.syms("|-")
Expand All @@ -75,20 +80,21 @@ class LFDBTranslator(implicit db: Database) {
(CAB, Array(None, Some(Array(1, 0)))))

alignments += (
(WN, "not"),
(WI, "impl"),
(WB, "equiv"),
(WAL, "forall"),
(db.asserts("wa"), "and"),
(db.asserts("wo"), "or"),
(db.asserts("wtru"), "true"),
(db.asserts("wex"), "exists"),
(db.asserts("pm3.2i"), "andI"),
(db.asserts("simpli"), "andEl"),
(db.asserts("simpri"), "andEr"),
(db.asserts("orci"), "orIl"),
(db.asserts("olci"), "orIr"),
(db.asserts("impl"), "_impl"))
(WN, Metamath.not),
(WI, Metamath.impl),
(WB, Metamath.equiv),
(WAL, Metamath.setmm ? "forall"),
//(db.asserts("wff"), Metamath.wff),
(db.asserts("wa"), Metamath.and),
(db.asserts("wo"), Metamath.or),
(db.asserts("wtru"), Metamath.setmm ? "true"),
(db.asserts("wex"), Metamath.setmm ? "exists"),
(db.asserts("pm3.2i"), Metamath.setmm ? "andI"),
(db.asserts("simpli"), Metamath.setmm ? "andEl"),
(db.asserts("simpri"), Metamath.setmm ? "andEr"),
(db.asserts("orci"), Metamath.setmm ? "orIl"),
(db.asserts("olci"), Metamath.setmm ? "orIr"),
(db.asserts("impl"), Metamath.setmm ? "_impl"))

db.decls foreach {
case a: Assert => processBoundVars(a)
Expand Down Expand Up @@ -163,9 +169,10 @@ class LFDBTranslator(implicit db: Database) {
}

def align(a: Assert): Term =
OMS(Metamath.setmm ? alignments.getOrElse(a,a.label))
OMS(alignments.getOrElse(a, Metamath.setmm ? a.label))

type DependVars = HashMap[Floating, TreeSet[Floating]]

def getDependVars(stmt: Assert): DependVars = {
implicit val dependVars = new DependVars
stmt.hyps foreach {
Expand All @@ -187,9 +194,14 @@ class LFDBTranslator(implicit db: Database) {
dependVars
}

val LF_SET = OMS(Metamath.setmm ? "set")
def LF_type(s: Statement): Term = OMS(Metamath.setmm ? s.typecode.id)
val LF_DED = OMS(Metamath.setmm ? "|-")
val LF_SET = OMS(Metamath.set)

def LF_type(s: Statement): Term = s.typecode.id match {
case "wff" => OMS(Metamath.wff)
case _ => OMS(Metamath.setmm ? s.typecode.id)
}

val LF_DED = OMS(Metamath.|-)

def LF_var(v: Floating): LocalName = LocalName(v.v.id)

Expand Down Expand Up @@ -250,7 +262,9 @@ class LFDBTranslator(implicit db: Database) {
case Some(b) =>
val needsFree = (b(i) & 2) != 0 ||
child.zipWithIndex.exists { case (c, j) => b(j) == 3 && c.stmt.typecode != SET }
if (needsFree) node match { case HypNode(v: Floating) => Apply(ap, OMV(LF_var(v))) }
if (needsFree) node match {
case HypNode(v: Floating) => Apply(ap, OMV(LF_var(v)))
}
else ap
case _ =>
Apply(ap, child.zip(bv).foldRight(translateTerm(node))((k, t) => k match {
Expand All @@ -268,7 +282,9 @@ class LFDBTranslator(implicit db: Database) {
syntaxToDefn.getOrElse(a, return None).parse match {
case AssertNode(eq, List(AssertNode(ax, child), p)) =>
val bv = getBoundVars(a)
val t = try { translateTerm(p) } catch {
val t = try {
translateTerm(p)
} catch {
case e: IllegalArgumentException => return None
}
Some(child.zipWithIndex.foldRight(t)((k, t) => k match {
Expand All @@ -289,6 +305,7 @@ class LFDBTranslator(implicit db: Database) {

class ScanExpr(free: Option[TreeSet[Floating]] = None)(implicit val dependVars: DependVars) {
val stack = new Stack[Floating]

def scan(p: ParseTree) {
p match {
case HypNode(h: Floating) => free match {
Expand All @@ -308,5 +325,4 @@ class LFDBTranslator(implicit db: Database) {
}
}
}

}
25 changes: 14 additions & 11 deletions src/mmt-metamath/src/info/kwarc/mmt/metamath/Theory.scala
View file
Expand Up @@ -8,7 +8,8 @@ import info.kwarc.mmt.api.utils.URI
object Metamath {
val _base = DPath(URI.http colon "us.metamath.org")
val prelude = _base ? "Prelude"

val setmm = _base ? "set.mm"
/*
/** Application symbol for $d sets */
val DV = OMS(prelude ? "DV")
/** Application symbol for $e (essential) hypotheses */
Expand All @@ -33,15 +34,17 @@ object Metamath {
* </pre>
*/
val FL = OMS(prelude ? "FL")
*/
def setconst(s: String) = OMS(setmm ? s)
def prelconst(s : String) = prelude ? s

val setmm = _base ? "set.mm"

def sconst(s: String) = OMS(setmm ? s)

val set = sconst("set")
val _class = sconst("class")
val wff = sconst("wff")
val |- = sconst("|-")


val set = prelconst("set")
val _class = prelconst("class")
val wff = prelconst("wff")
val |- = prelconst("ded")
val not = prelconst("not")
val impl = prelconst("impl")
val equiv = prelconst("equiv")
val and = prelconst("and")
val or = prelconst("or")
}
5 changes: 3 additions & 2 deletions src/mmt-metamath/src/info/kwarc/mmt/metamath/Translator.scala
View file
Expand Up @@ -13,7 +13,7 @@ import info.kwarc.mmt.api.opaque.StringFragment
import org.metamath.scala._
import info.kwarc.mmt.api.MPath


/*
class Translator(val controller: Controller, bt: BuildTask, index: Document => Unit) extends Logger {
def logPrefix = "mm-omdoc"
protected def report = controller.report
Expand Down Expand Up @@ -46,4 +46,5 @@ class Translator(val controller: Controller, bt: BuildTask, index: Document => U
}
controller add theory
}
}
}
*/
9 changes: 6 additions & 3 deletions src/mmt-pvs/src/info/kwarc/mmt/pvs/Translator.scala
View file
Expand Up @@ -203,11 +203,12 @@ class PVSImportTask(val controller: Controller, bt: BuildTask, index: Document =

def doFormal(f:FormalParameter) : Unit = f match {
case formal_type_decl(named,nonempty) =>
state.unknowns = 0
val v = VarDecl(doName(named.named.id),Some(PVSTheory.tp.term),None,None)
state.th.parameters = state.th.parameters ++ v
if (nonempty.nonempty_p && nonempty.contains.isDefined) {
state.th.add(Constant(state.th.toTerm,newName("INTERNAL_Assumption"),Nil,Some(
PVSTheory.is_nonempty(OMV(v.name),doExprAs(nonempty.contains.get,OMV(v.name)))),
state.bindUnknowns(PVSTheory.is_nonempty(OMV(v.name),doExprAs(nonempty.contains.get,OMV(v.name))))),
None,Some("Assumption")))
} else if (nonempty.nonempty_p) {
state.th.add(Constant(state.th.toTerm,newName("INTERNAL_Assumption"),Nil,Some(
Expand All @@ -223,7 +224,7 @@ class PVSImportTask(val controller: Controller, bt: BuildTask, index: Document =
state.th.parameters = state.th.parameters ++ v
if (nonempty.nonempty_p && nonempty.contains.isDefined) {
state.th.add(Constant(state.th.toTerm,newName("INTERNAL_Assumption"),Nil,Some(
PVSTheory.is_nonempty(OMV(v.name),doExprAs(nonempty.contains.get,OMV(v.name)))),
state.bindUnknowns(PVSTheory.is_nonempty(OMV(v.name),doExprAs(nonempty.contains.get,OMV(v.name))))),
None,Some("Assumption")))
} else if (nonempty.nonempty_p) {
state.th.add(Constant(state.th.toTerm,newName("INTERNAL_Assumption"),Nil,Some(
Expand Down Expand Up @@ -263,7 +264,8 @@ class PVSImportTask(val controller: Controller, bt: BuildTask, index: Document =
case var_decl(id, unnamed, tp) => // Not needed

case tcc_decl(ChainedDecl(NamedDecl(id, _, _), _, _), Assertion(kind, formula)) =>
val c = Constant(state.th.toTerm, newName(id + "_TCC"), Nil, Some(PVSTheory.proof(kind, doExprAs(formula, PVSTheory.bool.term))), None,
state.unknowns = 0
val c = Constant(state.th.toTerm, newName(id + "_TCC"), Nil, Some(state.bind(PVSTheory.proof(kind, doExprAs(formula, PVSTheory.bool.term)))), None,
Some(if (isAss) "Assumption_TCC" else "TCC"))
state.th add c
state.tcc = Some(c)
Expand All @@ -283,6 +285,7 @@ class PVSImportTask(val controller: Controller, bt: BuildTask, index: Document =

case formula_decl(ChainedDecl(NamedDecl(id, _, _), _, _), Assertion(kind, form)) =>
state.vars = Nil
state.unknowns = 0
val phi = doExprAs(form, PVSTheory.bool.term)
state.th add Constant(state.th.toTerm, newName(id), Nil, Some(state.bind(PVSTheory.proof(kind, phi))), None, if (isAss) Some("Assumption") else None)

Expand Down
1 change: 1 addition & 0 deletions src/mmt-stex/src/info/kwarc/mmt/stex/STeXAnalysis.scala
View file
Expand Up @@ -150,6 +150,7 @@ trait STeXAnalysis {
def join(s: STeXStructure) = {
struct = struct.join(s)
}

lines.foreach { line =>
val l = stripComment(line).trim
val verbIndex = l.indexOf("\\verb")
Expand Down
2 changes: 1 addition & 1 deletion src/mmt-stex/src/info/kwarc/mmt/stex/STeXUtils.scala
View file
Expand Up @@ -57,7 +57,7 @@ object STeXUtils {
}

def readSourceRebust(f: File): BufferedSource =
scala.io.Source.fromFile(f)
scala.io.Source.fromFile(f)(Codec.UTF8)

def stripComment(line: String): String = {
val idx = line.indexOf('%')
Expand Down
2 changes: 1 addition & 1 deletion src/test/preamble.scala
View file
Expand Up @@ -50,7 +50,7 @@ abstract class Test(archivepath : String,
* As an example, here's my default. All test files of mine just extend this:
*/
abstract class DennisTest(prefixes : String*) extends Test(
"/home/raupi/lmh/MathHub",
"/home/raupi/lmh/localmh/MathHub",
prefixes.toList,
"/home/raupi/lmh/Stuff/Public",
Some(8080),
Expand Down

0 comments on commit 0e5bcad

Please sign in to comment.