Jennisys:

  - added the following desugaring rule
     forall v :: v in {a1, a2, ..., an} ==> e  ~~~> e[v/a1] && e[v/a2] && ... && e[v/an]

  - added the "help" command line option

7 files changed, 197 insertions, 112 deletions

diff --git a/Jennisys/AstUtils.fs b/Jennisys/AstUtils.fs
index fa5a0a77..8322d1a7 100644
--- a/Jennisys/AstUtils.fs
+++ b/Jennisys/AstUtils.fs
@@ -7,8 +7,79 @@
 module AstUtils

 

 open Ast

+open Logger

 open Utils

 

+let rec Rewrite rewriterFunc expr =

+  let __RewriteOrRecurse e =

+    match rewriterFunc e with

+    | Some(ee) -> ee

+    | None -> Rewrite rewriterFunc e 

+  match expr with

+  | IntLiteral(_)

+  | BoolLiteral(_)                   

+  | Star      

+  | VarLiteral(_) 

+  | ObjLiteral(_)                      

+  | IdLiteral(_)                     -> match rewriterFunc expr with

+                                        | Some(e) -> e

+                                        | None -> expr

+  | Dot(e, id)                       -> Dot(__RewriteOrRecurse e, id)

+  | ForallExpr(vars,e)               -> ForallExpr(vars, __RewriteOrRecurse e)   

+  | UnaryExpr(op,e)                  -> UnaryExpr(op, __RewriteOrRecurse e)

+  | SeqLength(e)                     -> SeqLength(__RewriteOrRecurse e)

+  | SelectExpr(e1, e2)               -> SelectExpr(__RewriteOrRecurse e1, __RewriteOrRecurse e2)

+  | BinaryExpr(p,op,e1,e2)           -> BinaryExpr(p, op, __RewriteOrRecurse e1, __RewriteOrRecurse e2)

+  | IteExpr(e1,e2,e3)                -> IteExpr(__RewriteOrRecurse e1, __RewriteOrRecurse e2, __RewriteOrRecurse e3) 

+  | UpdateExpr(e1,e2,e3)             -> UpdateExpr(__RewriteOrRecurse e1, __RewriteOrRecurse e2, __RewriteOrRecurse e3) 

+  | SequenceExpr(exs)                -> SequenceExpr(exs |> List.map __RewriteOrRecurse)

+  | SetExpr(exs)                     -> SetExpr(exs |> List.map __RewriteOrRecurse)

+

+//  ====================================================

+/// Substitutes all occurences of all IdLiterals having 

+/// the same name as one of the variables in "vars" with

+/// VarLiterals, in "expr".

+//  ====================================================

+let RewriteVars vars expr = 

+  let __IdIsArg id = vars |> List.exists (function Var(name,_) -> name = id)

+  Rewrite (fun e ->

+             match e with 

+             | IdLiteral(id) when __IdIsArg id -> Some(VarLiteral(id))

+             | _ -> None) expr

+

+//  ================================================

+/// Substitutes all occurences of e1 with e2 in expr

+//  ================================================

+let Substitute e1 e2 expr = 

+  Rewrite (fun e ->

+             if e = e1 then

+               Some(e2)

+             else

+               None) expr

+

+let rec DescendExpr visitorFunc composeFunc leafVal expr = 

+  match expr with

+  | IntLiteral(_)

+  | BoolLiteral(_)                   

+  | Star      

+  | VarLiteral(_) 

+  | ObjLiteral(_)                      

+  | IdLiteral(_)                     -> leafVal

+  | Dot(e, _)

+  | ForallExpr(_,e)

+  | UnaryExpr(_,e)           

+  | SeqLength(e)                     -> composeFunc (visitorFunc e) (DescendExpr visitorFunc composeFunc leafVal e)

+  | SelectExpr(e1, e2)

+  | BinaryExpr(_,_,e1,e2)            -> composeFunc (composeFunc (composeFunc (visitorFunc e1) (visitorFunc e2)) (DescendExpr visitorFunc composeFunc leafVal e1)) (DescendExpr visitorFunc composeFunc leafVal e2)

+  | IteExpr(e1,e2,e3)                

+  | UpdateExpr(e1,e2,e3)             -> composeFunc (composeFunc (composeFunc (composeFunc (composeFunc (visitorFunc e1) (visitorFunc e2)) (visitorFunc e3)) (DescendExpr visitorFunc composeFunc leafVal e1)) (DescendExpr visitorFunc composeFunc leafVal e2)) (DescendExpr visitorFunc composeFunc leafVal e3)

+  | SequenceExpr(exs)                

+  | SetExpr(exs)                     -> match exs with

+                                        | [] -> leafVal

+                                        | fs :: rest -> rest |> List.fold (fun acc e -> composeFunc (composeFunc acc (visitorFunc e)) (DescendExpr visitorFunc composeFunc leafVal e)) (visitorFunc fs)

+              

+

+

 let PrintGenSym name =

   sprintf "gensym%s" name

 

@@ -572,15 +643,27 @@ let rec __EvalSym resolverFunc ctx expr =
         | [] -> BoolLiteral(true)

       match vars with

       | v :: restV -> 

-          let vDom = GetVarDomain resolverFunc v e

+          let vDom = GetVarDomain resolverFunc ctx v e

           __ExhaustVar v restV vDom

       | [] -> __EvalSym resolverFunc ctx e

-and GetVarDomain resolverFunc var expr = 

-  //TODO: don't hardcode this!!!

-  let elems = __EvalSym resolverFunc [] (Dot(ObjLiteral("this"), "elems"))

-  match elems with 

-  | SetExpr(elist) -> elist

-  | _ -> failwith "this is bogus"

+and GetVarDomain resolverFunc ctx var expr = 

+  match expr with 

+  | BinaryExpr(_, "==>", lhs, rhs) -> 

+      let conjs = SplitIntoConjunts lhs

+      conjs |> List.fold (fun acc e ->

+                            match e with

+                            | BinaryExpr(_, "in", VarLiteral(vn), rhs) when GetVarName var = vn ->

+                                match __EvalSym resolverFunc ctx rhs with

+                                | SetExpr(elist)

+                                | SequenceExpr(elist) -> elist |> List.append acc

+                                | _ -> failwith "illegal 'in' expression"

+                            | BinaryExpr(_, op, VarLiteral(vn),oth)

+                            | BinaryExpr(_, op, oth, VarLiteral(vn)) when GetVarName var = vn && Set.ofList ["<"; "<="; ">"; ">="] |> Set.contains op -> 

+                                failwith "not supported yet"

+                            | _ -> []) []

+  | _ -> 

+      Logger.WarnLine ("unknown pattern for a quantified expression; cannot infer domain of quantified variable \"" + (GetVarName var) + "\"")

+      []

 

 let EvalSym resolverFunc expr = 

   __EvalSym resolverFunc [] expr 

@@ -603,9 +686,16 @@ let rec Desugar expr =
   | UpdateExpr(_)     

   | SetExpr(_)     

   | SequenceExpr(_)        -> expr 

+  // forall v :: v in {a1, a2, ..., an} ==> e  ~~~> e[v/a1] && e[v/a2] && ... && e[v/an] 

+  | ForallExpr([Var(vn1,ty1)] as v, BinaryExpr(_, "==>", BinaryExpr(_, "in", VarLiteral(vn2), rhsCol), sub)) when vn1 = vn2 ->

+      match rhsCol with 

+      | SetExpr(elist)

+      | SequenceExpr(elist) -> elist |> List.fold (fun acc e -> BinaryAnd acc (Desugar (Substitute (VarLiteral(vn2)) e sub))) TrueLiteral

+      | _ -> ForallExpr(v, Desugar sub)

   | ForallExpr(v,e)        -> ForallExpr(v, Desugar e)

   | UnaryExpr(op,e)        -> UnaryExpr(op, Desugar e)

   | IteExpr(c,e1,e2)       -> IteExpr(c, Desugar e1, Desugar e2)

+  // lst = [a1 a2 ... an] ~~~> lst = [a1 a2 ... an] && lst[0] = a1 && lst[1] = a2 && ... && lst[n-1] = an

   | BinaryExpr(p,op,e1,e2) -> 

       let be = BinaryExpr(p, op, Desugar e1, Desugar e2)

       try

@@ -661,36 +751,3 @@ let ChangeThisReceiver receiver expr =
     | SetExpr(exs)                     -> SetExpr(exs |> List.map (__ChangeThis locals))

   (* --- function body starts here --- *)

   __ChangeThis Set.empty expr

-

-let rec Rewrite rewriterFunc expr =

-  let __RewriteOrRecurse e =

-    match rewriterFunc e with

-    | Some(ee) -> ee

-    | None -> Rewrite rewriterFunc e 

-  match expr with

-  | IntLiteral(_)

-  | BoolLiteral(_)                   

-  | Star      

-  | VarLiteral(_) 

-  | ObjLiteral(_)                      

-  | IdLiteral(_)                     -> match rewriterFunc expr with

-                                        | Some(e) -> e

-                                        | None -> expr

-  | Dot(e, id)                       -> Dot(__RewriteOrRecurse e, id)

-  | ForallExpr(vars,e)               -> ForallExpr(vars, __RewriteOrRecurse e)   

-  | UnaryExpr(op,e)                  -> UnaryExpr(op, __RewriteOrRecurse e)

-  | SeqLength(e)                     -> SeqLength(__RewriteOrRecurse e)

-  | SelectExpr(e1, e2)               -> SelectExpr(__RewriteOrRecurse e1, __RewriteOrRecurse e2)

-  | BinaryExpr(p,op,e1,e2)           -> BinaryExpr(p, op, __RewriteOrRecurse e1, __RewriteOrRecurse e2)

-  | IteExpr(e1,e2,e3)                -> IteExpr(__RewriteOrRecurse e1, __RewriteOrRecurse e2, __RewriteOrRecurse e3) 

-  | UpdateExpr(e1,e2,e3)             -> UpdateExpr(__RewriteOrRecurse e1, __RewriteOrRecurse e2, __RewriteOrRecurse e3) 

-  | SequenceExpr(exs)                -> SequenceExpr(exs |> List.map __RewriteOrRecurse)

-  | SetExpr(exs)                     -> SetExpr(exs |> List.map __RewriteOrRecurse)

-

-let RewriteVars vars expr = 

-  let __IdIsArg id = vars |> List.exists (function Var(name,_) -> name = id)

-  Rewrite (fun e ->

-             match e with 

-             | IdLiteral(id) when __IdIsArg id -> Some(VarLiteral(id))

-             | _ -> None) expr

-              
\ No newline at end of file
diff --git a/Jennisys/DafnyModelUtils.fs b/Jennisys/DafnyModelUtils.fs
index 83de2292..65fd97d2 100644
--- a/Jennisys/DafnyModelUtils.fs
+++ b/Jennisys/DafnyModelUtils.fs
@@ -213,6 +213,8 @@ let ReadSeq (model: Microsoft.Boogie.Model) (envMap,ctx) =
         __ReadSeqIndex model rest (newEnv,newCtx)

     | _ -> (envMap,ctx)

 

+  //TODO: This has become obsolete now, as the Seq#Build function has a different meaning now.

+  //      On the plus site, it might be that it is not necessary to read the model for this function anymore.

   // reads stuff from Seq#Build

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

     match bld_tuples with

@@ -251,7 +253,7 @@ let ReadSeq (model: Microsoft.Boogie.Model) (envMap,ctx) =
   let f_seq_app = model.MkFunc("Seq#Append", 2)

   (envMap,ctx) |> __ReadSeqLen model (List.ofSeq f_seq_len.Apps)

                |> __ReadSeqIndex model (List.ofSeq f_seq_idx.Apps)

-         //      |> __ReadSeqBuild model (List.ofSeq f_seq_bld.Apps)

+             //  |> __ReadSeqBuild model (List.ofSeq f_seq_bld.Apps)

                |> __ReadSeqAppend model (List.ofSeq f_seq_app.Apps)

 

 

diff --git a/Jennisys/Jennisys.fs b/Jennisys/Jennisys.fs
index d0a47fe1..604f02f8 100644
--- a/Jennisys/Jennisys.fs
+++ b/Jennisys/Jennisys.fs
@@ -40,7 +40,16 @@ let readAndProcess (filename: string) =
 
 try 
   let args = Environment.GetCommandLineArgs()
-  ParseCmdLineArgs (List.ofArray args)
-  readAndProcess CONFIG.inputFilename
+  ParseCmdLineArgs (List.ofArray args |> List.tail)
+  if CONFIG.help then 
+    printfn "%s" PrintHelpMsg
+  else 
+    if CONFIG.inputFilename = "" then
+      printfn "*** Error: No input file was specified."
+    else
+      readAndProcess CONFIG.inputFilename
 with
-  | InvalidCmdLineOption(msg) as ex -> printfn "%s" msg; printfn "%s" ex.StackTrace
\ No newline at end of file
+  | InvalidCmdLineOption(msg) 
+  | InvalidCmdLineArg(msg) as ex -> 
+      printfn "  [ERROR] %s" msg; 
+      printfn "%s" PrintHelpMsg
\ No newline at end of file
diff --git a/Jennisys/Jennisys.fsproj b/Jennisys/Jennisys.fsproj
index 8642cb6b..b88b6330 100644
--- a/Jennisys/Jennisys.fsproj
+++ b/Jennisys/Jennisys.fsproj
@@ -23,7 +23,8 @@
     <WarningLevel>3</WarningLevel>

     <PlatformTarget>x86</PlatformTarget>

     <DocumentationFile>bin\Debug\Language.XML</DocumentationFile>

-    <StartArguments>C:\boogie\Jennisys\Jennisys\examples\Set.jen /method:Set.Triple /genRepr /noVerifyParSol</StartArguments>

+    <StartArguments>

+    </StartArguments>

   </PropertyGroup>

   <PropertyGroup Condition=" '$(Configuration)|$(Platform)' == 'Release|x86' ">

     <DebugType>pdbonly</DebugType>

@@ -42,6 +43,7 @@
     <FsYaccOutputFolder>$(IntermediateOutputPath)</FsYaccOutputFolder>

   </PropertyGroup>

   <ItemGroup>

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

     <Compile Include="Utils.fs" />

     <Compile Include="Options.fs" />

     <Compile Include="PipelineUtils.fs" />

@@ -65,7 +67,6 @@
     </FsLex>

     <Compile Include="Printer.fs" />

     <Compile Include="DafnyPrinter.fs" />

-    <Compile Include="Logger.fs" />

     <Compile Include="TypeChecker.fs" />

     <Compile Include="Resolver.fs" />

     <Compile Include="CodeGen.fs" />

diff --git a/Jennisys/Logger.fs b/Jennisys/Logger.fs
index 09b576fd..d9df47a7 100644
--- a/Jennisys/Logger.fs
+++ b/Jennisys/Logger.fs
@@ -5,8 +5,8 @@
 //  #######################################################

 

 module Logger

-

-open Printer

+             

+let newline =  System.Environment.NewLine

 

 let _ALL = 100

 let _TRACE = 90

diff --git a/Jennisys/Options.fs b/Jennisys/Options.fs
index 4bd59b11..567967ae 100644
--- a/Jennisys/Options.fs
+++ b/Jennisys/Options.fs
@@ -9,6 +9,7 @@ module Options
 open Utils

 

 type Config = {

+   help: bool;

    inputFilename: string;

    methodToSynth: string;

    verifyPartialSolutions: bool;

@@ -19,7 +20,72 @@ type Config = {
    numLoopUnrolls: int;

 }

 

+type CfgOption<'a> = {

+   optionName: string; 

+   optionType: string;

+   optionSetter: 'a -> Config -> Config;

+   descr: string;

+}

+

+exception InvalidCmdLineArg of string

+exception InvalidCmdLineOption of string

+

+let CheckNonEmpty value optName =

+  if value = "" then raise (InvalidCmdLineArg("A value for option " + optName + " must not be empty")) else value

+

+let CheckInt value optName =

+  try 

+    System.Int32.Parse value

+  with 

+    | ex -> raise (InvalidCmdLineArg("A value for option " + optName + " must be a boolean"))

+

+let CheckBool value optName =

+  if value = "" then

+    true

+  else

+    try 

+      System.Boolean.Parse value

+    with 

+      | ex -> raise (InvalidCmdLineArg("A value for option " + optName + " must be an integer"))

+

+let cfgOptions = [

+  { optionName = "help";            optionType = "bool";   optionSetter = (fun v (cfg: Config) -> {cfg with help                   =      CheckBool v "help"});           descr = "description not available"; }

+  { optionName = "method";          optionType = "string"; optionSetter = (fun v (cfg: Config) -> {cfg with methodToSynth          = CheckNonEmpty v "method"});          descr = "description not available"; }

+  { optionName = "verifyParSol";    optionType = "bool";   optionSetter = (fun v (cfg: Config) -> {cfg with verifyPartialSolutions =      CheckBool v "verifyParSol"});   descr = "description not available"; }

+  { optionName = "noVerifyParSol";  optionType = "bool";   optionSetter = (fun v (cfg: Config) -> {cfg with verifyPartialSolutions = not (CheckBool v "verifyParSol")});  descr = "description not available"; }

+  { optionName = "verifySol";       optionType = "bool";   optionSetter = (fun v (cfg: Config) -> {cfg with verifySolutions        =      CheckBool v "verifySol"});      descr = "description not available"; }

+  { optionName = "noVerifySol";     optionType = "bool";   optionSetter = (fun v (cfg: Config) -> {cfg with verifySolutions        = not (CheckBool v "verifySol")});     descr = "description not available"; } 

+  { optionName = "checkUnifs";      optionType = "bool";   optionSetter = (fun v (cfg: Config) -> {cfg with checkUnifications      =      CheckBool v "checkUnifs"});     descr = "description not available"; } 

+  { optionName = "noCheckUnifs";    optionType = "bool";   optionSetter = (fun v (cfg: Config) -> {cfg with checkUnifications      = not (CheckBool v "noCheckUnifs")});  descr = "description not available"; }

+  { optionName = "genRepr";         optionType = "bool";   optionSetter = (fun v (cfg: Config) -> {cfg with genRepr                =      CheckBool v "genRepr"});        descr = "description not available"; }

+  { optionName = "noGenRepr";       optionType = "bool";   optionSetter = (fun v (cfg: Config) -> {cfg with genRepr                = not (CheckBool v "noGenRepr")});     descr = "description not available"; }

+  { optionName = "timeout";         optionType = "int";    optionSetter = (fun v (cfg: Config) -> {cfg with timeout                =      CheckInt v "timeout"});         descr = "description not available"; }

+  { optionName = "unrolls";         optionType = "int";    optionSetter = (fun v (cfg: Config) -> {cfg with numLoopUnrolls         =      CheckInt v "unrolls"});         descr = "description not available"; }

+]

+

+let cfgOptMap = cfgOptions |> List.fold (fun acc o -> acc |> Map.add o.optionName o) Map.empty

+

+let newline = System.Environment.NewLine

+

+let PrintHelpMsg = 

+  let maxw = cfgOptions |> List.fold (fun acc o -> if String.length o.optionName > acc then String.length o.optionName else acc) 0

+  let maxwStr = sprintf "%d" (maxw + 2)

+  let strf = new Printf.StringFormat<_>("  %-" + maxwStr + "s: %-6s | %s")

+  let rec __PrintHelp optLst = 

+    match optLst with

+    | fs :: []   -> (sprintf strf fs.optionName fs.optionType fs.descr)

+    | fs :: rest -> (sprintf strf fs.optionName fs.optionType fs.descr) + newline + (__PrintHelp rest)

+    | [] -> ""

+  (* --- function body starts here --- *)

+  newline +

+  "Jennisys usage: Jennisys [ option ... ] filename" + newline +

+  "  where <option> is one of " + newline + newline +

+  "  ----- General options -----------------------------------------------------" + newline + 

+  "        (available switches are: /, -, --)" + newline + newline +

+  (__PrintHelp cfgOptions)

+

 let defaultConfig: Config = {

+  help              = false;

   inputFilename     = "";

   methodToSynth     = "*";

   verifyPartialSolutions = true;

@@ -34,9 +100,6 @@ let defaultConfig: Config = {
 /// typically called only once at the beginning of the program execution 

 let mutable CONFIG = defaultConfig

 

-exception InvalidCmdLineArg of string

-exception InvalidCmdLineOption of string

-

 let ParseCmdLineArgs args = 

   let __StripSwitches str =

     match str with 

@@ -59,67 +122,17 @@ let ParseCmdLineArgs args =
       else

         let x = __StripSwitches splits.[0]

         (x, "")

-

-  let __CheckNonEmpty value optName =

-    if value = "" then raise (InvalidCmdLineArg("A value for option " + optName + " must not be empty"))

-

-  let __CheckInt value optName =

-    try 

-      System.Int32.Parse value

-    with 

-      | ex -> raise (InvalidCmdLineArg("A value for option " + optName + " must be a boolean"))

-

-  let __CheckBool value optName =

-    if value = "" then

-      true

-    else

-      try 

-        System.Boolean.Parse value

-      with 

-        | ex -> raise (InvalidCmdLineArg("A value for option " + optName + " must be an integer"))

-               

+                 

   let rec __Parse args cfg =

     match args with

     | fs :: rest -> 

         let opt,value = __Split fs

-        match opt with

-        | "method"    -> 

-            __CheckNonEmpty value opt

-            __Parse rest { cfg with methodToSynth = value }

-        | "verifyParSol" -> 

-            let b = __CheckBool value opt

-            __Parse rest { cfg with verifyPartialSolutions = b }

-        | "noVerifyParSol" -> 

-            let b = __CheckBool value opt

-            __Parse rest { cfg with verifyPartialSolutions = not b }

-        | "verifySol" -> 

-            let b = __CheckBool value opt

-            __Parse rest { cfg with verifySolutions = b }

-        | "noVerifySol" -> 

-            let b = __CheckBool value opt

-            __Parse rest { cfg with verifySolutions = not b }

-        | "checkUnifs" -> 

-            let b = __CheckBool value opt

-            __Parse rest { cfg with checkUnifications = b }

-        | "noCheckUnifs" -> 

-            let b = __CheckBool value opt

-            __Parse rest { cfg with checkUnifications = not b }

-        | "genRepr" -> 

-            let b = __CheckBool value opt

-            __Parse rest { cfg with genRepr = b }

-        | "noGenRepr" -> 

-            let b = __CheckBool value opt

-            __Parse rest { cfg with genRepr = not b }

-        | "timeout" ->

-            let t = __CheckInt value opt

-            __Parse rest { cfg with timeout = t }

-        | "unrolls" ->

-            let t = __CheckInt value opt

-            __Parse rest { cfg with numLoopUnrolls = t }

-        | "" -> 

-            __Parse rest { cfg with inputFilename = value }

-        | _ -> 

-            raise (InvalidCmdLineOption("Unknown option: " + opt))

+        if opt = "" then

+          __Parse rest { cfg with inputFilename = CheckNonEmpty value opt }

+        else 

+          match Map.tryFind opt cfgOptMap with

+          | Some(opt) -> __Parse rest (opt.optionSetter value cfg)

+          | None -> raise (InvalidCmdLineOption("Unknown option: " + opt))

     | [] -> cfg   

     

   (* --- function body starts here --- *)           

diff --git a/Jennisys/examples/Number.jen b/Jennisys/examples/Number.jen
index 75417168..3d37e6a4 100644
--- a/Jennisys/examples/Number.jen
+++ b/Jennisys/examples/Number.jen
@@ -22,17 +22,20 @@ class Number {
     ensures num in {a b c}
     ensures num <= a && num <= b && num <= c
 
+  constructor Min32(a: int, b: int, c: int)
+    ensures num in {a b c}
+    ensures forall x :: x in {a b c} ==> num <= x
+
  constructor MinSum(a: int, b: int, c: int)
     ensures num in {a+b a+c b+c}
     ensures num <= a+b && num <= b+c && num <= a+c
 
  constructor Min4(a: int, b: int, c: int, d: int)
     ensures num in {a b c d}
-    ensures num <= a && num <= b && num <= c && num <= d
+    ensures forall x :: x in {a b c d} ==> num <= x
 
-  constructor Abs(a: int) 
-    ensures a < 0 ==> num = -a
-    ensures a >= 0 ==> num = a
+  constructor Abs(a: int)  
+    ensures num in {a (-a)} && num >= 0
 }
 
 model Number {