- implemented code generation from a synthesis solution (simple field

   assignments only), along with resolving some values missing in the model.

11 files changed, 280 insertions, 114 deletions

diff --git a/Jennisys/Jennisys/Analyzer.fs b/Jennisys/Jennisys/Analyzer.fs
index 9a57ae64..12111196 100644
--- a/Jennisys/Jennisys/Analyzer.fs
+++ b/Jennisys/Jennisys/Analyzer.fs
@@ -2,11 +2,11 @@
 
 open Ast
 open AstUtils
+open CodeGen
 open DafnyModelUtils
 open PipelineUtils
 open Printer
 open DafnyPrinter
-open TypeChecker
 
 open Microsoft.Boogie
                     
@@ -34,7 +34,7 @@ let rec Substitute substMap = function
   | ForallExpr(vv,e) -> ForallExpr(vv, Substitute substMap e)
   | expr -> expr
 
-let GenerateMethodCode methodName signature pre post assumeInvInitially =
+let GenMethodAnalysisCode methodName signature pre post assumeInvInitially =
   "  method " + methodName + "()" + newline +
   "    modifies this;" + newline +
   "  {" + newline + 
@@ -53,108 +53,55 @@ let GenerateMethodCode methodName signature pre post assumeInvInitially =
   // if the following assert fails, the model hints at what code to generate; if the verification succeeds, an implementation would be infeasible
   "    // assert false to search for a model satisfying the assumed constraints" + newline + 
   "    assert false;" + newline + 
-  "  }" + newline                                      
-
-let GetFieldValidExpr (name: string) : Expr = 
-  BinaryImplies (BinaryNeq (IdLiteral(name)) (IdLiteral("null"))) (Dot(IdLiteral(name), "Valid()"))
-
-let GetFieldsForValidExpr (allFields: VarDecl list) prog : VarDecl list =
-  allFields |> List.filter (function Var(name, tp) when IsUserType prog tp -> true
-                                     | _                                   -> false)
-
-let GetFieldsValidExprList (allFields: VarDecl list) prog : Expr list =
-  let fields = GetFieldsForValidExpr allFields prog
-  fields |> List.map (function Var(name, _) -> GetFieldValidExpr name)
-
-let GenValidFunctionCode clsMembers modelInv vars prog : string = 
-  let invMembers = clsMembers |> List.filter (function Invariant(_) -> true | _ -> false)
-  let clsInvs = invMembers |> List.choose (function Invariant(exprList) -> Some(exprList) | _ -> None) |> List.concat
-  let allInvs = modelInv :: clsInvs
-  let fieldsValid = GetFieldsValidExprList vars prog
-  let idt = "    "
-  let invsStr = List.concat [allInvs ; fieldsValid] |> List.fold (fun acc e -> List.concat [acc ; SplitIntoConjunts e]) []
-                                                    |> List.fold (fun acc (e: Expr) -> 
-                                                                    if acc = "" then
-                                                                      sprintf "%s(%s)" idt (PrintExpr 0 e)
-                                                                    else
-                                                                      acc + " &&" + newline + sprintf "%s(%s)" idt (PrintExpr 0 e)) ""
-  // TODO: don't hardcode decr vars!!!
-  let decrVars = if List.choose (function Var(n,_) -> Some(n)) vars |> List.exists (fun n -> n = "next") then
-                   ["list"]
-                 else
-                   []
-  "  function Valid(): bool" + newline +
-  "    reads *;" + newline +
-  (if List.isEmpty decrVars then "" else sprintf "    decreases %s;%s" (PrintSep ", " (fun a -> a) decrVars) newline) +
-  "  {" + newline + 
-  invsStr + newline +
-  "  }" + newline
-
-let GetAnalyzeConstrCode mthd =
-  match mthd with 
-  | Constructor(methodName,signature,pre,post) -> (GenerateMethodCode methodName signature pre post false) + newline
-  | Method(methodName,signature,pre,post)      -> (GenerateMethodCode methodName signature pre post true) + newline
+  "  }" + newline  
+             
+let MethodAnalysisPrinter onlyForThisCompMethod comp mthd = 
+  match onlyForThisCompMethod with
+  | (c,m) when c = comp && m = mthd -> 
+    match m with 
+    | Constructor(methodName, sign, pre, post) -> (GenMethodAnalysisCode methodName sign pre post false) + newline
+    | _ -> ""
   | _ -> ""
 
-let AnalyzeMethod prog mthd mthdCodeFunc: string =
-  match prog with
-  | Program(components) -> components |> List.fold (fun acc comp -> 
-      match comp with  
-      | Component(Class(name,typeParams,members), Model(_,_,cVars,frame,inv), code) ->
-        let aVars = Fields members
-        let allVars = List.concat [aVars ; cVars];
-        // Now print it as a Dafny program
-        acc + 
-        (sprintf "class %s%s {" name (PrintTypeParams typeParams)) + newline +       
-        // the fields: original abstract fields plus concrete fields
-        (sprintf "%s" (PrintFields aVars 2 true)) + newline +     
-        (sprintf "%s" (PrintFields cVars 2 false)) + newline +                           
-        // generate the Valid function
-        (sprintf "%s" (GenValidFunctionCode members inv allVars prog)) + newline +
-        // generate code for the given method
-        (if List.exists (fun a -> a = mthd) members then
-           mthdCodeFunc mthd
-         else
-           "") +
-        // the end of the class
-        "}" + newline + newline
-      | _ -> assert false; "") ""
 
-let PrintImplCode (heap, env, ctx) =
-  
-  ()  
 
-let Analyze prog =
-  let models = ref null
-  let methods = Methods prog     
-  // synthesize constructors
-  methods |> List.iter (fun (comp, m) -> 
-    match m with
-    | Constructor(methodName,signature,pre,post) -> 
-        use file = System.IO.File.CreateText(dafnyScratchFile)
-        file.AutoFlush <- true
-        let code = AnalyzeMethod prog m GetAnalyzeConstrCode
-        printfn "analyzing constructor %s" methodName 
-//        printfn "%s" code
-//        printfn "-------------------------"
-        fprintf file "%s" code
-        file.Close()
-        RunDafny dafnyScratchFile dafnyModelFile
-        use modelFile = System.IO.File.OpenText(dafnyModelFile)
+let AnalyzeConstructor prog comp methodName signature pre post =
+  let m = Constructor(methodName, signature, pre, post)
+  use file = System.IO.File.CreateText(dafnyScratchFile)
+  file.AutoFlush <- true
+  let code = PrintDafnyCodeSkeleton prog (MethodAnalysisPrinter (comp,m))
+  printfn "analyzing constructor %s" methodName 
+  fprintf file "%s" code
+  file.Close()
+  RunDafny dafnyScratchFile dafnyModelFile
+  use modelFile = System.IO.File.OpenText(dafnyModelFile)
         
-        let models = Microsoft.Boogie.Model.ParseModels modelFile
-        if models.Count = 0 then
-          printfn "spec for method %s.%s is inconsistent (no valid solution exists)" (GetClassName comp) methodName
-        else 
-          assert (models.Count = 1) // TODO
-          let model = models.[0]
-
-          let (heap,env,ctx) = ReadFieldValuesFromModel model prog comp m 
-          PrintImplCode (heap, env, ctx) |> ignore
-          printfn "done with %s" methodName
-          System.Environment.Exit(1)
-    | _ -> ())
+  let models = Microsoft.Boogie.Model.ParseModels modelFile
+  if models.Count = 0 then
+    printfn "spec for method %s.%s is inconsistent (no valid solution exists)" (GetClassName comp) methodName
+    failwith "inconsistent spec"      // TODO: instead of failing, just continue
+  else 
+    if models.Count > 1 then failwith "why did we get more than one model for a single constructor analysis???"
+    let model = models.[0]
+    ReadFieldValuesFromModel model prog comp m 
+
+let rec AnalyzeMethods prog methods = 
+  match methods with
+  | (comp,m) :: rest -> 
+      match m with
+      | Constructor(methodName,signature,pre,post) -> 
+          let (heap,env,ctx) = AnalyzeConstructor prog comp methodName signature pre post
+          AnalyzeMethods prog rest |> Map.add (comp,m) (heap,env,ctx)
+      | _ -> AnalyzeMethods prog rest
+  | [] -> Map.empty
 
+let Analyze prog =
+  let solutions = AnalyzeMethods prog (Methods prog)
+  use file = System.IO.File.CreateText(dafnySynthFile)
+  file.AutoFlush <- true
+  let synthCode = PrintImplCode prog solutions
+  fprintfn file "%s" synthCode
+  ()
 
 //let AnalyzeComponent_rustan c =
 //  match c with
diff --git a/Jennisys/Jennisys/Ast.fs b/Jennisys/Jennisys/Ast.fs
index eeb2f753..b2bd27c0 100644
--- a/Jennisys/Jennisys/Ast.fs
+++ b/Jennisys/Jennisys/Ast.fs
@@ -14,8 +14,9 @@ type Type =
 type Const = 

   | IntConst   of int

   | BoolConst  of bool

-  | SetConst   of Set<Const>

+  | SetConst   of Set<Const option>

   | SeqConst   of (Const option) list

+  | NullConst

   | ThisConst  of (* loc id *) string * Type option

   | NewObj     of (* loc id *) string * Type option

   | Unresolved of (* loc id *) string 

diff --git a/Jennisys/Jennisys/AstUtils.fs b/Jennisys/Jennisys/AstUtils.fs
index 794a89dc..3e32fd5c 100644
--- a/Jennisys/Jennisys/AstUtils.fs
+++ b/Jennisys/Jennisys/AstUtils.fs
@@ -27,9 +27,15 @@ let FalseLiteral = IdLiteral("false")
 

 // --- search functions ---

                                                

-let Fields members =
+let FilterFieldMembers members =
   members |> List.choose (function Field(vd) -> Some(vd) | _ -> None)
 
+let FilterConstructorMembers members = 
+  members |> List.choose (function Constructor(_,_,_,_) as m -> Some(m) | _ -> None)
+
+let FilterMethodMembers members = 
+  members |> List.choose (function Method(_,_,_,_) as m -> Some(m) | _ -> None)
+
 let Methods prog = 
   match prog with
   | Program(components) ->
@@ -41,7 +47,7 @@ let Methods prog =
 let AllFields c = 

   match c with
   | Component(Class(_,_,members), Model(_,_,cVars,_,_), _) ->
-      let aVars = Fields members
+      let aVars = FilterFieldMembers members
       List.concat [aVars ; cVars]

   | _ -> []

 

diff --git a/Jennisys/Jennisys/CodeGen.fs b/Jennisys/Jennisys/CodeGen.fs
new file mode 100644
index 00000000..c7c2e274
--- /dev/null
+++ b/Jennisys/Jennisys/CodeGen.fs
@@ -0,0 +1,119 @@
+module CodeGen

+

+open Ast

+open AstUtils

+open Utils
+open Printer   

+open TypeChecker

+open DafnyPrinter

+

+let GetFieldValidExpr (name: string) : Expr = 
+  BinaryImplies (BinaryNeq (IdLiteral(name)) (IdLiteral("null"))) (Dot(IdLiteral(name), "Valid()"))
+
+let GetFieldsForValidExpr (allFields: VarDecl list) prog : VarDecl list =
+  allFields |> List.filter (function Var(name, tp) when IsUserType prog tp -> true
+                                     | _                                   -> false)
+
+let GetFieldsValidExprList (allFields: VarDecl list) prog : Expr list =
+  let fields = GetFieldsForValidExpr allFields prog
+  fields |> List.map (function Var(name, _) -> GetFieldValidExpr name)
+
+let PrintValidFunctionCode clsMembers modelInv vars prog : string = 
+  let invMembers = clsMembers |> List.filter (function Invariant(_) -> true | _ -> false)
+  let clsInvs = invMembers |> List.choose (function Invariant(exprList) -> Some(exprList) | _ -> None) |> List.concat
+  let allInvs = modelInv :: clsInvs
+  let fieldsValid = GetFieldsValidExprList vars prog
+  let idt = "    "
+  let invsStr = List.concat [allInvs ; fieldsValid] |> List.fold (fun acc e -> List.concat [acc ; SplitIntoConjunts e]) []
+                                                    |> List.fold (fun acc (e: Expr) -> 
+                                                                    if acc = "" then
+                                                                      sprintf "%s(%s)" idt (PrintExpr 0 e)
+                                                                    else
+                                                                      acc + " &&" + newline + sprintf "%s(%s)" idt (PrintExpr 0 e)) ""
+  // TODO: don't hardcode decr vars!!!
+  let decrVars = if List.choose (function Var(n,_) -> Some(n)) vars |> List.exists (fun n -> n = "next") then
+                   ["list"]
+                 else
+                   []
+  "  function Valid(): bool" + newline +
+  "    reads *;" + newline +
+  (if List.isEmpty decrVars then "" else sprintf "    decreases %s;%s" (PrintSep ", " (fun a -> a) decrVars) newline) +
+  "  {" + newline + 
+  invsStr + newline +
+  "  }" + newline

+

+let PrintDafnyCodeSkeleton prog methodPrinterFunc: string =
+  match prog with
+  | Program(components) -> components |> List.fold (fun acc comp -> 
+      match comp with  
+      | Component(Class(name,typeParams,members), Model(_,_,cVars,frame,inv), code) ->
+        let aVars = FilterFieldMembers members
+        let allVars = List.concat [aVars ; cVars];
+        let compMethods = FilterConstructorMembers members
+        // Now print it as a Dafny program
+        acc + 
+        (sprintf "class %s%s {" name (PrintTypeParams typeParams)) + newline +       
+        // the fields: original abstract fields plus concrete fields
+        (sprintf "%s" (PrintFields aVars 2 true)) + newline +     
+        (sprintf "%s" (PrintFields cVars 2 false)) + newline +                           
+        // generate the Valid function
+        (sprintf "%s" (PrintValidFunctionCode members inv allVars prog)) + newline +
+        // call the method printer function on all methods of this component
+        (compMethods |> List.fold (fun acc m -> acc + (methodPrinterFunc comp m)) "") +
+        // the end of the class
+        "}" + newline + newline
+      | _ -> assert false; "") ""

+  

+let PrintAllocNewObjects (heap,env,ctx) indent = 
+  let idt = Indent indent
+  env |> Map.fold (fun acc l v ->
+                     match v with 
+                     | NewObj(_,_) -> acc |> Set.add v
+                     | _ -> acc
+                  ) Set.empty
+      |> Set.fold (fun acc newObjConst ->
+                    match newObjConst with
+                    | NewObj(name, Some(tp)) -> acc + (sprintf "%svar %s := new %s;%s" idt (PrintGenSym name) (PrintType tp) newline)
+                    | _ -> failwith ("NewObj doesn't have a type: " + newObjConst.ToString())
+                  ) ""
+
+let PrintObjRefName o (env,ctx) = 
+  match Resolve o (env,ctx) with
+  | ThisConst(_,_) -> "this";
+  | NewObj(name, _) -> PrintGenSym name
+  | _ -> failwith ("unresolved object ref: " + o.ToString())
+
+let PrintVarAssignments (heap,env,ctx) indent = 
+  let idt = Indent indent
+  heap |> Map.fold (fun acc (o,f) l ->
+                      let objRef = PrintObjRefName o (env,ctx)
+                      let fldName = PrintVarName f
+                      let value = Resolve l (env,ctx) |> PrintConst
+                      acc + (sprintf "%s%s.%s := %s;" idt objRef fldName value) + newline
+                   ) ""
+
+let PrintHeapCreationCode (heap,env,ctx) indent = 
+  (PrintAllocNewObjects (heap,env,ctx) indent) +
+  (PrintVarAssignments (heap,env,ctx) indent)
+
+let GenConstructorCode mthd body =
+  match mthd with
+  | Constructor(methodName, sign, pre, post) -> 
+      "  method " + methodName + (PrintSig sign) + newline +
+      "    modifies this;" + newline +
+      "    requires " + (PrintExpr 0 pre) + ";" + newline +
+      "    ensures " + (PrintExpr 0 post) + ";" + newline + 
+      "    ensures Valid(); " + newline +
+      "  {" + newline + 
+      body + 
+      "  }" + newline
+  | _ -> ""
+
+// solutions: (comp, constructor) |--> (heap, env, ctx) 
+let PrintImplCode prog solutions =
+  PrintDafnyCodeSkeleton prog (fun comp mthd ->
+                                 let mthdBody = match Map.tryFind (comp,mthd) solutions with
+                                                | Some(heap,env,ctx) -> PrintHeapCreationCode (heap,env,ctx) 4
+                                                | _ -> "//unable to synthesize"
+                                 (GenConstructorCode mthd mthdBody) + newline
+                              )
\ No newline at end of file
diff --git a/Jennisys/Jennisys/DafnyModelUtils.fs b/Jennisys/Jennisys/DafnyModelUtils.fs
index c3db8e83..800a65d5 100644
--- a/Jennisys/Jennisys/DafnyModelUtils.fs
+++ b/Jennisys/Jennisys/DafnyModelUtils.fs
@@ -79,7 +79,18 @@ let AddConstr c1 c2 ctx =
     ctx

   else

     match c1, c2 with

-    | Unresolved(_), _ | _, Unresolved(_) -> Set.add (Set.ofList [c1; c2]) ctx

+    | Unresolved(_), _ | _, Unresolved(_) -> 

+        // find partitions

+        let s1Opt = ctx |> Set.filter (fun ss -> Set.contains c1 ss) |> Utils.SetToOption

+        let s2Opt = ctx |> Set.filter (fun ss -> Set.contains c2 ss) |> Utils.SetToOption

+        match s1Opt, s2Opt with

+        // both already exist --> so just merge them

+        | Some(s1), Some(s2) -> ctx |> Set.remove s1 |> Set.remove s2 |> Set.add (Set.union s1 s2)

+        // exactly one already exists --> add to existing

+        | Some(s1), None -> ctx |> Set.remove s1 |> Set.add (Set.add c2 s1)

+        | None, Some(s2) -> ctx |> Set.remove s2 |> Set.add (Set.add c1 s2)

+        // neither exists --> create a new one

+        | None, None -> ctx |> Set.add (Set.ofList [c1; c2])

     | _ -> failwith ("trying to add an equality constraint between two constants: " + c1.ToString() + ", and " + c2.ToString())

                                            

 let rec UpdateContext lst1 lst2 ctx = 

@@ -114,12 +125,14 @@ let ReadHeap (model: Microsoft.Boogie.Model) prog =
                         let clsName = if dotIdx = -1 then "" else fldFullName.Substring(0, dotIdx)
                         let refVal = ft.Result
                         let refObj = Unresolved(GetRefName ref)
-                        let fldVar = FindVar prog clsName fldName
-                        let fldType = match fldVar with 
-                                      | Some(Var(_,t)) -> t
-                                      | _              -> None
-                        let fldVal = ConvertValue model refVal
-                        acc |> Map.add (refObj, fldVar) fldVal
+                        let fldVarOpt = FindVar prog clsName fldName
+                        match fldVarOpt with
+                        | Some(fldVar) ->
+                            let fldType = match fldVar with 
+                                          | Var(_,t) -> t
+                            let fldVal = ConvertValue model refVal
+                            acc |> Map.add (refObj, fldVar) fldVal
+                        | None -> acc
                       ) Map.empty

 

 let rec ReadSeqLen (model: Microsoft.Boogie.Model) (len_tuples: Model.FuncTuple list) (envMap,ctx) =

@@ -167,9 +180,17 @@ let ReadSeq (model: Microsoft.Boogie.Model) (envMap,ctx) =
                |> ReadSeqIndex model (List.ofSeq f_seq_idx.Apps)

                |> ReadSeqBuild model (List.ofSeq f_seq_bld.Apps)

 

-let ReadSet (model: Microsoft.Boogie.Model) envMap =

-  envMap

 

+let ReadSet (model: Microsoft.Boogie.Model) (envMap,ctx) =

+  (envMap,ctx)

+

+let ReadNull (model: Microsoft.Boogie.Model) (envMap,ctx) = 

+  let f_null = model.MkFunc("null", 0)

+  assert (f_null.AppCount = 1)

+  let e = (f_null.Apps |> Seq.nth 0).Result

+  let newEnv = envMap |> Map.add (GetLoc e) NullConst

+  (newEnv,ctx)

+  

 let ReadEnv (model: Microsoft.Boogie.Model) = 

   let f_dtype = model.MkFunc("dtype", 1)
   let refs = f_dtype.Apps |> Seq.choose (fun ft -> Some(ft.Args.[0]))

@@ -179,11 +200,12 @@ let ReadEnv (model: Microsoft.Boogie.Model) =
                                            let loc = Unresolved(locName)

                                            let locType = GetType ft.Result

                                            let value = match elemName with

-                                                       | Some(n) when n.StartsWith("this") -> ThisConst(locName, locType)

-                                                       | _                                 -> NewObj(locName, locType)

+                                                       | Some(n) when n.StartsWith("this") -> ThisConst(locName.Replace("*", ""), locType)

+                                                       | _                                 -> NewObj(locName.Replace("*", ""), locType)

                                            acc |> Map.add loc value

                                         ) Map.empty

-  (envMap, Set.ofList([])) |> ReadSeq model 

+  (envMap, Set.ofList([])) |> ReadNull model

+                           |> ReadSeq model 

                            |> ReadSet model

 

 let ReadFieldValuesFromModel (model: Microsoft.Boogie.Model) prog comp meth =
diff --git a/Jennisys/Jennisys/Jennisys.fs b/Jennisys/Jennisys/Jennisys.fs
index 0c69f797..28824237 100644
--- a/Jennisys/Jennisys/Jennisys.fs
+++ b/Jennisys/Jennisys/Jennisys.fs
@@ -64,4 +64,4 @@ let args = Environment.GetCommandLineArgs()
 try 
   start 1 args false true null
 with 
-| _ as e -> printfn "%s" e.StackTrace
\ No newline at end of file
+| e -> printfn "%s" e.StackTrace
\ No newline at end of file
diff --git a/Jennisys/Jennisys/Jennisys.fsproj b/Jennisys/Jennisys/Jennisys.fsproj
index 1ec66a98..fb1008d0 100644
--- a/Jennisys/Jennisys/Jennisys.fsproj
+++ b/Jennisys/Jennisys/Jennisys.fsproj
@@ -64,6 +64,7 @@
     <Compile Include="Printer.fs" />

     <Compile Include="DafnyPrinter.fs" />

     <Compile Include="TypeChecker.fs" />

+    <Compile Include="CodeGen.fs" />

     <Compile Include="Analyzer.fs" />

     <Compile Include="Jennisys.fs" />

   </ItemGroup>

diff --git a/Jennisys/Jennisys/PipelineUtils.fs b/Jennisys/Jennisys/PipelineUtils.fs
index 0f7eb847..17c1c058 100644
--- a/Jennisys/Jennisys/PipelineUtils.fs
+++ b/Jennisys/Jennisys/PipelineUtils.fs
@@ -3,6 +3,7 @@
 let dafnyScratchFile = @"c:\tmp\jennisys-scratch.dfy"
 let dafnyModelFile = @"c:\tmp\jennisys-scratch.model"
 let dafnyOutFile = @"c:\tmp\jennisys-scratch.out"
+let dafnySynthFile = @"c:\tmp\jennisys-synth.dfy"
 
 let RunDafny inputFile modelFile =

   async {

diff --git a/Jennisys/Jennisys/Printer.fs b/Jennisys/Jennisys/Printer.fs
index 2c6315a3..b0d4746c 100644
--- a/Jennisys/Jennisys/Printer.fs
+++ b/Jennisys/Jennisys/Printer.fs
@@ -4,12 +4,33 @@ open Ast
 
 let newline = System.Environment.NewLine // "\r\n"
 
+let PrintGenSym name =
+  sprintf "gensym%s" name
+
 let rec PrintSep sep f list =
   match list with
   | [] -> ""
   | [a] -> f a
   | a :: more -> (f a) + sep + (PrintSep sep f more)
   
+let rec PrintConst cst = 
+  match cst with 
+  | IntConst(v)        -> sprintf "%d" v
+  | BoolConst(b)       -> sprintf "%b" b
+  | SetConst(cset)     -> cset.ToString() //TODO: this won't work
+  | SeqConst(cseq)     -> 
+      let seqCont = cseq |> List.fold (fun acc cOpt ->
+                                         let sep = if acc = "" then "" else ", "
+                                         match cOpt with 
+                                         | Some(c) -> acc + sep + (PrintConst c)
+                                         | None -> acc + sep + "null"
+                                      ) ""
+      sprintf "[%s]" seqCont
+  | NullConst          -> "null"
+  | ThisConst(_,_)     -> "this"
+  | NewObj(name,_)     -> PrintGenSym name
+  | Unresolved(name)   -> sprintf "Unresolved(%s)" name
+
 let rec PrintType ty =
   match ty with
   | IntType                  -> "int"
@@ -24,6 +45,10 @@ let PrintVarDecl vd =
   | Var(id,None) -> id
   | Var(id,Some(ty)) -> sprintf "%s: %s" id (PrintType ty)
 
+let PrintVarName vd =
+  match vd with
+  | Var(id,_) -> id
+
 let rec PrintExpr ctx expr =
   match expr with
   | IntLiteral(n)     -> sprintf "%O" n
diff --git a/Jennisys/Jennisys/TypeChecker.fs b/Jennisys/Jennisys/TypeChecker.fs
index 6ca13453..79d5fe89 100644
--- a/Jennisys/Jennisys/TypeChecker.fs
+++ b/Jennisys/Jennisys/TypeChecker.fs
@@ -36,3 +36,40 @@ let TypeCheck prog =
       let componentNames = decls |> List.choose (function Class(name,_,_) -> Some(name) | _ -> None)

       let clist = componentNames |> List.map (fun name -> Component(GetClass name decls, GetModel name decls, GetCode name decls))

       Some(Program(clist))

+

+// resolving values

+ 

+let rec Resolve cst (env,ctx) =

+  match cst with

+  | Unresolved(_) as u -> 

+      // see if it is in the env map first

+      let envVal = Map.tryFind cst env

+      match envVal with

+      | Some(c) -> Resolve c (env,ctx)

+      | None -> 

+          // not found in the env map --> check the equality sets

+          let eq = ctx |> Set.filter (fun eqSet -> Set.contains u eqSet)

+                       |> Utils.SetToOption

+          match eq with 

+          | Some(eqSet) -> 

+              let cOpt = eqSet |> Set.filter (function Unresolved(_) -> false | _ -> true)

+                               |> Utils.SetToOption

+              match cOpt with 

+              | Some(c) -> c

+              | _ -> failwith ("failed to resolve " + cst.ToString())

+          | _ -> failwith ("failed to resolve " + cst.ToString())

+  | SeqConst(cseq) -> 

+      let resolvedLst = cseq |> List.fold (fun acc cOpt ->

+                                             match cOpt with

+                                             | Some(c) -> Some(Resolve c (env,ctx)) :: acc 

+                                             | None -> cOpt :: acc

+                                          ) []

+      SeqConst(resolvedLst)

+  | SetConst(cset) ->

+      let resolvedSet = cset |> Set.fold (fun acc cOpt ->

+                                            match cOpt with

+                                            | Some(c) -> acc |> Set.add (Some(Resolve c (env,ctx)))

+                                            | None -> acc |> Set.add(cOpt)

+                                          ) Set.empty

+      SetConst(resolvedSet)

+  | _ -> cst

diff --git a/Jennisys/Jennisys/Utils.fs b/Jennisys/Jennisys/Utils.fs
index 8a2e107e..9a743fe0 100644
--- a/Jennisys/Jennisys/Utils.fs
+++ b/Jennisys/Jennisys/Utils.fs
@@ -18,6 +18,13 @@ let SeqToOption seq =
   else

     Some(Seq.nth 0 seq)

 

+let SetToOption set = 

+  assert (Set.count set <= 1)

+  if (Set.isEmpty set) then

+    None

+  else 

+    Some(set |> Set.toList |> List.head)

+

 let rec GenList n =

   if n = 0 then

     []