Debugging type import.

src/main/scala/UclidMain.scala

@@ -159,7 +159,8 @@ object UclidMain {
     val filenameAdderPass = new AddFilenameRewriter(None) 
     passManager.addPass(filenameAdderPass)
     passManager.addPass(new ForLoopIndexRewriter())
-    // passManager.addPass(new ExternalTypeRewriter())
+    passManager.addPass(new ExternalTypeAnalysis())
+    passManager.addPass(new ExternalTypeRewriter())
     passManager.addPass(new TypeSynonymFinder())
     passManager.addPass(new TypeSynonymRewriter())
     passManager.addPass(new BitVectorSliceFindWidth())
@@ -196,7 +197,6 @@ object UclidMain {
       (acc, m) =>
         val modules = acc._1
         val context = acc._2
-        // println("context::modules: " + context.moduleDefinitionMap.toString)
         val mP = passManager.run(m, context).get
         (mP :: modules, context +& mP)
     }._1
@@ -211,12 +211,12 @@ object UclidMain {
     val passManager = new PassManager()
     passManager.addPass(new ModuleInstanceChecker(moduleList))
     passManager.addPass(new ModuleDependencyFinder(moduleList, mainModuleName))
+    // passManager.addPass(new ASTPrinter("ASTPrinter$4"))
     passManager.addPass(new ModuleFlattener(moduleList, mainModuleName))
     passManager.addPass(new ModuleEliminator(mainModuleName))
     passManager.addPass(new ModuleCleaner())
     passManager.addPass(new ExpressionTypeChecker())
     passManager.addPass(new ModuleTypeChecker())
-    // passManager.addPass(new ASTPrinter("ASTPrinter$4"))
     passManager.addPass(new SemanticAnalyzer())
 
     // run passes.

src/main/scala/lang/ASTVistors.scala

@@ -228,8 +228,8 @@ class ASTAnalyzer[T] (_passName : String, _pass: ReadOnlyPass[T]) extends ASTAna
   /** The pass itself. */
   def pass : ReadOnlyPass[T] = _pass
   /** The input/outputs of the pass. */
-  private[this] var _in : Option[T] = None
-  private[this] var _out : Option[T] = None
+  protected[this] var _in : Option[T] = None
+  protected[this] var _out : Option[T] = None
   /** The pseudo-variable 'in' sets the input to the analysis. */
   def in : Option[T] = _in
   def in_=(i : Option[T]): Unit = {
@@ -904,7 +904,6 @@ class ASTRewriter (_passName : String, _pass: RewritePass, setFilename : Boolean
   }
 
   def visitModule(module : Module, initContext : Scope) : Option[Module] = {
-    val initContext = Scope.empty
     val context = initContext + module
     val id = visitIdentifier(module.id, context)
     val decls = module.decls.map(visitDecl(_, context)).flatten

src/main/scala/lang/ExternalTypeRewriter.scala

@@ -1,24 +1,57 @@
 package uclid
 package lang
 
-class ExternalTypeRewriterPass extends RewritePass {
-  override def rewriteExternalType(extT : ExternalType, context : Scope) : Option[Type] = {
-    println("external type: " + extT.toString)
-    println("context::module: " + context.moduleDefinitionMap.toString)
-
-    context.moduleDefinitionMap.get(extT.moduleId) match {
-      case Some(mod) =>
-        mod.typeDeclarationMap.get(extT.typeId) match {
-          case Some(typ) => Some(typ)
-          case None => 
-            println("Can't find type in module!")
-            Some(extT)
+class ExternalTypeAnalysisPass extends ReadOnlyPass[(List[ModuleError], Map[ExternalType, Type])] {
+  type T = (List[ModuleError], Map[ExternalType, Type])
+  override def applyOnExternalType(d : TraversalDirection.T, extT : ExternalType, in : T, context : Scope) : T = {
+    if (d == TraversalDirection.Up) {
+      if (in._2.contains(extT)) {
+        in
+      } else {
+        context.moduleDefinitionMap.get(extT.moduleId) match {
+          case Some(mod) =>
+            mod.typeDeclarationMap.get(extT.typeId) match {
+              case Some(typ) => 
+                (in._1, in._2 + (extT -> typ))
+              case None =>
+                val msg = "Unknown type '%s' in module '%s'.".format(extT.typeId.toString, mod.id.toString)
+                (ModuleError(msg, extT.typeId.position) :: in._1, in._2)
+            }
+          case None =>
+            val msg = "Unknown module: %s.".format(extT.moduleId.toString)
+            (ModuleError(msg, extT.moduleId.position) :: in._1, in._2)
         }
-      case None =>
-        println("Can't find module!")
-        Some(extT)
+      }
+    } else {
+      in
     }
   }
 }
-class ExternalTypeRewriter extends ASTRewriter(
-    "ExternalTypeRewriter", new ExternalTypeRewriterPass())
+class ExternalTypeAnalysis extends ASTAnalyzer("ExternalTypeAnalysis", new ExternalTypeAnalysisPass()) {
+  in = Some((List.empty[ModuleError], Map.empty[ExternalType, Type]))
+
+  override def visit(module : Module, context : Scope) : Option[Module] = {
+    val analysisResult = visitModule(module, _in.get, context) 
+    val errors = analysisResult._1
+    if (errors.size > 0) {
+      throw new Utils.ParserErrorList(errors.map(e => (e.msg, e.position)))
+    }
+    _out = Some(analysisResult)
+    return Some(module)
+  }
+}
+
+class ExternalTypeRewriterPass extends RewritePass {
+  lazy val manager : PassManager = analysis.manager
+  lazy val externalTypeAnalysis = manager.pass("ExternalTypeAnalysis").asInstanceOf[ExternalTypeAnalysis]
+  lazy val typeMap : Map[ExternalType, Type] = externalTypeAnalysis.out.get._2
+
+  override def rewriteExternalType(extT : ExternalType, context : Scope) : Option[Type] = {
+    val typP = typeMap.get(extT)
+    Utils.assert(typP.isDefined, "Unknown external types must have been eliminated by now.")
+    typP
+  }
+}
+
+class ExternalTypeRewriter extends ASTRewriter("ExternalTypeRewriter", new ExternalTypeRewriterPass())
+

src/main/scala/lang/ModuleFlattener.scala

@@ -82,7 +82,8 @@ class ModuleInstanceCheckerPass(modules : List[Module]) extends ReadOnlyPass[Lis
   }
 
   def checkInstance(inst : InstanceDecl, in : List[ModuleError], context : Scope) : List[ModuleError] = {
-    moduleMap.get(inst.moduleId) match {
+    val targetModOption = moduleMap.get(inst.moduleId)
+    targetModOption match {
       case None =>
         val error = ModuleError("Unknown module being instantiated: " + inst.moduleId.toString, inst.moduleId.position)
         error :: in
@@ -123,6 +124,7 @@ class ModuleInstanceChecker(modules : List[Module]) extends ASTAnalyzer(
     in = Some(List.empty[ModuleError])
   }
   override def finish() {
+    println("finish")
     val errors = out.get
     if (errors.size > 0) {
       throw new Utils.ParserErrorList(errors.map((e) => (e.msg, e.position)))

src/main/scala/lang/PassManager.scala

@@ -67,19 +67,20 @@ class PassManager {
 
   // run on a list of modules.
   def run(modules : List[Module]) : List[Module] = {
-    passes.foreach(_.reset())
     val modulesP = passes.foldLeft(modules) { 
       (mods, pass) => {
-        mods.map {
+        pass.reset()
+        val modsP = mods.map {
           m => {
             val mP = pass.visit(m, Scope.empty)
             pass.rewind()
             mP
           }
         }.flatten
+        pass.finish()
+        modsP
       }
     }
-    passes.foreach(_.finish())
     modulesP
   }
 

src/main/scala/lang/UclidLanguage.scala

@@ -612,7 +612,7 @@ sealed abstract class Decl extends ASTNode {
   def declNames : List[Identifier]
 }
 
-case class InstanceDecl(moduleId : Identifier, instanceId : Identifier, arguments: List[(Identifier, Option[Expr])], instType : Option[ModuleInstanceType], modType : Option[ModuleType]) extends Decl
+case class InstanceDecl(instanceId : Identifier, moduleId : Identifier, arguments: List[(Identifier, Option[Expr])], instType : Option[ModuleInstanceType], modType : Option[ModuleType]) extends Decl
 {
   lazy val argMap = arguments.foldLeft(Map.empty[Identifier, Expr]) { 
     (acc, arg) => {

src/main/scala/lang/UclidParser.scala

@@ -419,11 +419,11 @@ object UclidParser extends UclidTokenParsers with PackratParsers {
       }
     }
 
-    lazy val VarDecl : PackratParser[lang.StateVarDecl] = positioned {
-      keyword(KwVar) ~> IdType <~ ";" ^^ { case (id,typ) => lang.StateVarDecl(id,typ)}
-    }
     lazy val VarsDecl : PackratParser[lang.StateVarsDecl] = positioned {
-      keyword(KwVar) ~> IdList ~ ":" ~ Type <~ ";" ^^ { case ids ~ ":" ~ typ => lang.StateVarsDecl(ids, typ) }
+      KwVar ~> IdList ~ ":" ~ Type <~ ";" ^^ { case ids ~ ":" ~ typ => lang.StateVarsDecl(ids, typ) }
+    }
+    lazy val VarDecl : PackratParser[lang.StateVarDecl] = positioned {
+      KwVar ~> IdType <~ ";" ^^ { case (id,typ) => lang.StateVarDecl(id,typ)}
     }
     lazy val InputDecl : PackratParser[lang.InputVarDecl] = positioned {
       KwInput ~> IdType <~ ";" ^^ { case (id,typ) => lang.InputVarDecl(id,typ)}

test/test-type-import.ucl4

@@ -1,19 +1,74 @@
 module common {
   type addr_t = bv8;
-  type data_t = bv8;
-  
-  type opcode_t = enum { add, sub, load, store };
-  type mem_t = [addr_t]data_t;
+  type word_t = bv8;
+
+  type op_t = enum { add, sub, load, store };
+  type mem_t = [addr_t]word_t;
 }
 
-module main {
+module cpu {
   type addr_t = common :: addr_t;
   type mem_t = common :: mem_t;
+  type word_t = common :: word_t;
+  type op_t = common :: op_t;
+
+  type regindex_t;
+  type regs_t = [regindex_t]word_t;
+
 
   var mem : mem_t;
+  var regs : regs_t;
+  var pc : addr_t;
+
+  function word2op(w : word_t) : op_t;
+  function word2reg0(w : word_t) : regindex_t;
+  function word2reg1(w : word_t) : regindex_t;
+  function word2nextPC(w : word_t)  : addr_t;
+
+  procedure next_instruction() returns () {
+      var inst : word_t;
+      var op : op_t;
+      var r0ind : regindex_t;
+      var r1ind : regindex_t;
+      var r0 : word_t;
+      var r1 : word_t;
+      var result : word_t;
+
+      // get the next instruction.
+      inst := mem[pc];
+      // find its operation
+      op := word2op(inst);
+      // and its operands
+      r0ind := word2reg0(inst);
+      r1ind := word2reg1(inst);
+      r0 := regs[r0ind];
+      r1 := regs[r1ind];
+      // now execute
+      case
+        (op == add)   : { result := r0 + r1; }
+        (op == sub)   : { result := r0 - r1; }
+        (op == load)  : { result := mem[r1]; }
+        (op == store) : { result := r0; mem[r0] := r1; }
+      esac
+      regs[r0ind] := result;
+  }
+
+  init {
+      assume (forall (r : regindex_t) :: regs[r] == 0bv8);
+  }
+
+  next {
+      call () := next_instruction();
+  }
+}
 
+module main {
+
+  instance cpu_i : cpu();
+  next {
+      call (cpu_i);
+  }
   control {
     print_module;
   }
 }
-

vim/uclid.vim

@@ -21,7 +21,7 @@ syn keyword ucl4Type            bool int bv\d\+ enum
 " repeat / condition / label
 syn keyword ucl4Expr            forall exists Lambda 
 syn keyword ucl4Stmt            if else assert assume havoc for skip case esac
-syn keyword ucl4Decl            module init next control function procedure type var input output constant property instance axiom
+syn keyword ucl4Decl            module init next control function procedure returns call type var input output constant property instance axiom 
 syn keyword ucl4Cmd             initialize simulate decide print_module print_cex print_results k_induction_base k_induction_step clear_context
 " user labels
 syn keyword ucl4Constant        false true