Commit dffa2d69 authored by Florian Rabe's avatar Florian Rabe

no message

parent 9a6e4f28
......@@ -28,6 +28,11 @@ class SFOLTermGenerator(controller: Controller) {
println("inputs: " + ins.mkString(", "))
println("output: " + out)
}
val lits = theory.getLiterals
lits.foreach {case (a,rt) =>
println("literals for type: " + a)
println("semantic values: " + rt.semType)
}
}
}
......@@ -35,7 +40,8 @@ object SFOLTermGeneratorTest {
def main(args: Array[String]) {
val controller = Controller.make(true, true, List("MMT/urtheories", "MMT/LATIN2"))
val thyS = "latin:/algebraic?Group"
// val thyS = "latin:/algebraic?Group"
val thyS = "latin:/?Nat"
val thy = Path.parseM(thyS, controller.getNamespaceMap)
val gen = new SFOLTermGenerator(controller)
gen.makeTerms(thy)
......
......@@ -83,8 +83,9 @@ object SFOLPatterns {
class SFOLTheoryAdapter(controller: Controller, path: MPath) {
import SFOLPatterns._
private val lup = controller.globalLookup
private lazy val init = {
val theory = controller.globalLookup.getAs(classOf[Theory], path)
val theory = lup.getAs(classOf[Theory], path)
controller.simplifier(theory)
val constants = Theory.primitiveConstants(path, controller.globalLookup)
println(constants)
......@@ -118,9 +119,12 @@ class SFOLTheoryAdapter(controller: Controller, path: MPath) {
}
def getLiterals = {
val rules = RuleSet.collectRules(controller, Context(path))
val primitive = constants.map(_._1)
rules.get(classOf[RealizedType]) flatMap {rt =>
rt.synType match {
case TypedTerms.tm(a) => List((a, rt))
val st = lup.ExpandDefinitions(rt.synType, p => !primitive.contains(p))
st match {
case TypedTerms.tm(a) =>
List((a, rt))
case _ => Nil
}
}
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment