summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--Jennisys/Jennisys/Analyzer.fs112
-rw-r--r--Jennisys/Jennisys/Ast.fs2
-rw-r--r--Jennisys/Jennisys/AstUtils.fs84
-rw-r--r--Jennisys/Jennisys/CodeGen.fs39
-rw-r--r--Jennisys/Jennisys/DafnyPrinter.fs148
-rw-r--r--Jennisys/Jennisys/Jennisys.fsproj2
-rw-r--r--Jennisys/Jennisys/Printer.fs2
7 files changed, 269 insertions, 120 deletions
diff --git a/Jennisys/Jennisys/Analyzer.fs b/Jennisys/Jennisys/Analyzer.fs
index 0970a193..fffaa2bd 100644
--- a/Jennisys/Jennisys/Analyzer.fs
+++ b/Jennisys/Jennisys/Analyzer.fs
@@ -84,6 +84,7 @@ let rec IsArgsOnly args expr =
| SequenceExpr(exprs) | SetExpr(exprs) -> exprs |> List.fold (fun acc e -> acc && (IsArgsOnly args e)) true
| SeqLength(e) -> IsArgsOnly args e
| ForallExpr(vars,e) -> IsArgsOnly (List.concat [args; vars]) e
+ | MethodCall(rcv,_,aparams) -> rcv :: aparams |> List.fold (fun acc e -> acc && (IsArgsOnly args e)) true
let AddUnif indent e v unifMap =
let idt = Indent indent
@@ -365,11 +366,14 @@ and TryInferConditionals indent prog comp m unifs heapInst =
with
ex -> raise ex
+let GetAllMethodsToAnalyze prog =
+ FilterMembers prog FilterConstructorMembers
+
let GetMethodsToAnalyze prog =
let mOpt = Options.CONFIG.methodToSynth;
if mOpt = "*" then
(* all *)
- FilterMembers prog FilterConstructorMembers
+ GetAllMethodsToAnalyze prog
elif mOpt = "paramsOnly" then
(* only with parameters *)
FilterMembers prog FilterConstructorMembersWithParams
@@ -411,39 +415,121 @@ let rec AnalyzeMethods prog members =
| _ -> AnalyzeMethods prog rest
| [] -> Map.empty
+let GetModularBranch prog comp meth cond hInst =
+ let rec __AddDirectChildren e acc =
+ match e with
+ | ObjLiteral(_) when not (e = ThisLiteral || e = NullLiteral) -> acc |> Set.add e
+ | SequenceExpr(elist)
+ | SetExpr(elist) -> elist |> List.fold (fun acc2 e2 -> __AddDirectChildren e2 acc2) acc
+ | _ -> acc
+ let __GetDirectChildren =
+ let thisRhsExprs = hInst.assignments |> List.choose (function ((obj,_),e) when obj.name = "this" -> Some(e) | _ -> None)
+ thisRhsExprs |> List.fold (fun acc e -> __AddDirectChildren e acc) Set.empty
+ |> Set.toList
+ let __IsAbstractField ty var =
+ let builder = CascadingBuilder<_>(false)
+ let varName = GetVarName var
+ builder {
+ let! comp = FindComponent prog (GetTypeShortName ty)
+ let! fld = GetAbstractFields comp |> List.fold (fun acc v -> if GetVarName v = varName then Some(varName) else acc) None
+ return true
+ }
+ let __GetSpecFor objLitName =
+ let absFieldAssignments = hInst.assignments |> List.choose (fun ((obj,var),e) ->
+ if obj.name = objLitName && __IsAbstractField obj.objType var then
+ Some(var,e)
+ else
+ None)
+ absFieldAssignments |> List.fold (fun acc (Var(varName,_),e) -> BinaryAnd acc (BinaryEq (IdLiteral(varName)) e)) TrueLiteral
+ let __GetArgsUsed expr =
+ let args = GetMethodArgs meth
+ let argSet = DescendExpr2 (fun e acc ->
+ match e with
+ | VarLiteral(vname) ->
+ match args |> List.tryFind (function Var(name,_) when vname = name -> true | _ -> false) with
+ | Some(var) -> acc |> Set.add var
+ | None -> acc
+ | _ -> acc
+ ) expr Set.empty
+ argSet |> Set.toList
+ let rec __GetDelegateMethods objs acc =
+ match objs with
+ | ObjLiteral(name) as obj :: rest ->
+ let mName = sprintf "_init_%s_%s" (GetMethodFullName comp meth |> String.map (fun c -> if c = '.' then '_' else c)) name
+ let pre = TrueLiteral
+ let post = __GetSpecFor name
+ let ins = __GetArgsUsed (BinaryAnd pre post)
+ let sgn = Sig(ins, [])
+ let m = Method(mName, sgn, pre, post, true)
+ __GetDelegateMethods rest (acc |> Map.add obj m)
+ | _ :: rest -> failwith "internal error: expected to see only ObjLiterals"
+ | [] -> acc
+ let __FindObj objName =
+ try
+ hInst.assignments |> List.find (fun ((obj,_),_) -> obj.name = objName) |> fst |> fst
+ with
+ | ex -> failwithf "obj %s not found for method %s" objName (GetMethodFullName comp meth)
+ (* --- function body starts here --- *)
+ let directChildren = __GetDirectChildren
+ let delegateMethods = __GetDelegateMethods directChildren Map.empty
+ let initChildrenExprList = delegateMethods |> Map.toList
+ |> List.map (fun (receiver, mthd) ->
+ let key = __FindObj (PrintExpr 0 receiver), Var("", None)
+ let args = GetMethodArgs mthd |> List.map (fun (Var(name,_)) -> VarLiteral(name))
+ let e = MethodCall(receiver, GetMethodName mthd, args)
+ (key, e)
+ )
+ let newAssgns = hInst.assignments |> List.filter (fun ((obj,_),_) -> if obj.name = "this" then true else false)
+ let newProg = delegateMethods |> Map.fold (fun acc receiver mthd ->
+ let obj = __FindObj (PrintExpr 0 receiver)
+ let comp = FindComponent acc (GetTypeShortName obj.objType) |> Utils.ExtractOption
+ AddReplaceMethod acc comp mthd None |> fst
+ ) prog
+ newProg, { hInst with assignments = initChildrenExprList @ newAssgns }
+
let GetModularSol prog sol =
-
- sol
+ let comp = fst (fst sol)
+ let meth = snd (fst sol)
+ let rec __xxx prog lst =
+ match lst with
+ | (cond, hInst) :: rest ->
+ let newProg, newhInst = GetModularBranch prog comp meth cond hInst
+ let newProg, newRest = __xxx newProg rest
+ newProg, ((cond, newhInst) :: newRest)
+ | [] -> prog, []
+ let newProg, newSolutions = __xxx prog (snd sol)
+ let newComp = FindComponent newProg (GetComponentName comp) |> Utils.ExtractOption
+ newProg, ((newComp, meth), newSolutions)
let Modularize prog solutions =
- let rec __Modularize sols acc =
+ let rec __Modularize prog sols acc =
match sols with
| sol :: rest ->
- let newSol = GetModularSol prog sol
+ let (newProg, newSol) = GetModularSol prog sol
let newAcc = acc |> Map.add (fst newSol) (snd newSol)
- __Modularize rest newAcc
- | [] -> acc
+ __Modularize newProg rest newAcc
+ | [] -> (prog, acc)
(* --- function body starts here --- *)
- __Modularize (Map.toList solutions) Map.empty
+ __Modularize prog (Map.toList solutions) Map.empty
let Analyze prog filename =
/// Prints given solutions to a file
- let __PrintSolution outFileName solutions =
+ let __PrintSolution prog outFileName solutions =
use file = System.IO.File.CreateText(outFileName)
file.AutoFlush <- true
- let synthCode = PrintImplCode prog solutions GetMethodsToAnalyze Options.CONFIG.genRepr
+ let synthCode = PrintImplCode prog solutions GetAllMethodsToAnalyze Options.CONFIG.genRepr
fprintfn file "%s" synthCode
(* --- function body starts here --- *)
let solutions = AnalyzeMethods prog (GetMethodsToAnalyze prog)
let progName = System.IO.Path.GetFileNameWithoutExtension(filename)
let outFlatSolFileName = dafnySynthFileNameTemplate.Replace("###", progName)
Logger.InfoLine "Printing synthesized code"
- __PrintSolution outFlatSolFileName solutions
+ __PrintSolution prog outFlatSolFileName solutions
// try to modularize
- let modularSolutions = Modularize prog solutions
+ let newProg, modularSolutions = Modularize prog solutions
let outModSolFileName = dafnyModularSynthFileNameTemplate.Replace("###", progName)
Logger.InfoLine "Printing modularized code"
- __PrintSolution outModSolFileName modularSolutions
+ __PrintSolution newProg outModSolFileName modularSolutions
()
//let AnalyzeComponent_rustan c =
diff --git a/Jennisys/Jennisys/Ast.fs b/Jennisys/Jennisys/Ast.fs
index b9105254..ab3dc8bb 100644
--- a/Jennisys/Jennisys/Ast.fs
+++ b/Jennisys/Jennisys/Ast.fs
@@ -45,7 +45,7 @@ type Expr =
| SeqLength of Expr
| SetExpr of Expr list //TODO: maybe this should really be a set instead of a list
| ForallExpr of VarDecl list * Expr
-
+ | MethodCall of (* receiver *) Expr * (* name *) string * (* actual parameters *) Expr list
type Const =
| IntConst of int
| BoolConst of bool
diff --git a/Jennisys/Jennisys/AstUtils.fs b/Jennisys/Jennisys/AstUtils.fs
index 2c8c4440..5a8198d5 100644
--- a/Jennisys/Jennisys/AstUtils.fs
+++ b/Jennisys/Jennisys/AstUtils.fs
@@ -10,6 +10,9 @@ open Ast
open Logger
open Utils
+let ThisLiteral = ObjLiteral("this")
+let NullLiteral = ObjLiteral("null")
+
let rec Rewrite rewriterFunc expr =
let __RewriteOrRecurse e =
match rewriterFunc e with
@@ -34,6 +37,7 @@ let rec Rewrite rewriterFunc expr =
| 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)
+ | MethodCall(rcv,name,aparams) -> MethodCall(__RewriteOrRecurse rcv, name, aparams |> List.map __RewriteOrRecurse)
// ====================================================
/// Substitutes all occurences of all IdLiterals having
@@ -58,6 +62,10 @@ let Substitute e1 e2 expr =
None) expr
let rec DescendExpr visitorFunc composeFunc leafVal expr =
+ let __Compose elist =
+ match elist with
+ | [] -> leafVal
+ | fs :: rest -> rest |> List.fold (fun acc e -> composeFunc (composeFunc acc (visitorFunc e)) (DescendExpr visitorFunc composeFunc leafVal e)) (visitorFunc fs)
match expr with
| IntLiteral(_)
| BoolLiteral(_)
@@ -68,18 +76,18 @@ let rec DescendExpr visitorFunc composeFunc leafVal expr =
| Dot(e, _)
| ForallExpr(_,e)
| UnaryExpr(_,e)
- | SeqLength(e) -> composeFunc (visitorFunc e) (DescendExpr visitorFunc composeFunc leafVal e)
+ | SeqLength(e) -> __Compose (e :: [])
| SelectExpr(e1, e2)
- | BinaryExpr(_,_,e1,e2) -> composeFunc (composeFunc (composeFunc (visitorFunc e1) (visitorFunc e2)) (DescendExpr visitorFunc composeFunc leafVal e1)) (DescendExpr visitorFunc composeFunc leafVal e2)
+ | BinaryExpr(_,_,e1,e2) -> __Compose (e1 :: 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)
+ | UpdateExpr(e1,e2,e3) -> __Compose (e1 :: e2 :: e3 :: [])
+ | MethodCall(rcv,_,aparams) -> __Compose (rcv :: aparams)
| 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)
+ | SetExpr(exs) -> __Compose exs
let rec DescendExpr2 visitorFunc expr acc =
let newAcc = acc |> visitorFunc expr
+ let __Pipe elist = elist |> List.fold (fun a e -> a |> DescendExpr2 visitorFunc e) newAcc
match expr with
| IntLiteral(_)
| BoolLiteral(_)
@@ -90,13 +98,14 @@ let rec DescendExpr2 visitorFunc expr acc =
| Dot(e, _)
| ForallExpr(_,e)
| UnaryExpr(_,e)
- | SeqLength(e) -> newAcc |> DescendExpr2 visitorFunc e
+ | SeqLength(e) -> __Pipe (e :: [])
| SelectExpr(e1, e2)
- | BinaryExpr(_,_,e1,e2) -> newAcc |> DescendExpr2 visitorFunc e1 |> DescendExpr2 visitorFunc e2
+ | BinaryExpr(_,_,e1,e2) -> __Pipe (e1 :: e2 :: [])
| IteExpr(e1,e2,e3)
- | UpdateExpr(e1,e2,e3) -> newAcc |> DescendExpr2 visitorFunc e1 |> DescendExpr2 visitorFunc e2 |> DescendExpr2 visitorFunc e3
+ | UpdateExpr(e1,e2,e3) -> __Pipe (e1 :: e2 :: e3 :: [])
+ | MethodCall(rcv,_,aparams) -> __Pipe (rcv :: aparams)
| SequenceExpr(exs)
- | SetExpr(exs) -> exs |> List.fold (fun a e -> a |> DescendExpr2 visitorFunc e) newAcc
+ | SetExpr(exs) -> __Pipe exs
let PrintGenSym name =
sprintf "gensym%s" name
@@ -269,16 +278,22 @@ let FilterMembers prog filter =
| Component(Class(_,_,members),_,_) -> List.concat [acc ; members |> filter |> List.choose (fun m -> Some(comp, m))]
| _ -> acc) []
+let GetAbstractFields comp =
+ match comp with
+ | Component(Class(_,_,members), _, _) -> FilterFieldMembers members
+ | _ -> failwithf "internal error: invalid component: %O" comp
+
+let GetConcreteFields comp =
+ match comp with
+ | Component(_, Model(_,_,cVars,_,_), _) -> cVars
+ | _ -> failwithf "internal error: invalid component: %O" comp
+
// =================================
/// Returns all fields of a component
// =================================
let GetAllFields comp =
- match comp with
- | Component(Class(_,_,members), Model(_,_,cVars,_,_), _) ->
- let aVars = FilterFieldMembers members
- List.concat [aVars ; cVars]
- | _ -> []
-
+ List.concat [GetAbstractFields comp; GetConcreteFields comp]
+
// ===========================================================
/// Returns a map (Type |--> Set<Var>) where all
/// the given fields are grouped by their type
@@ -374,6 +389,14 @@ let GetVarName var =
| Var(name,_) -> name
// ==================================
+/// Returns component name
+// ==================================
+let GetComponentName comp =
+ match comp with
+ | Component(Class(name,_,_),_,_) -> name
+ | _ -> failwithf "invalid component %O" comp
+
+// ==================================
/// Returns all members of a component
// ==================================
let GetMembers comp =
@@ -433,13 +456,24 @@ let GetFrameFields comp =
////////////////////////
-let AddPrecondition prog comp m e =
- match prog, comp, m with
- | Program(clist), Component(Class(cname, ctypeParams, members), model, code), Method(mn, sgn, pre, post, cstr) ->
- let newMthd = Method(mn, sgn, BinaryAnd pre e, post, cstr)
- let newCls = Class(cname, ctypeParams, Utils.ListReplace m newMthd members)
+let AddReplaceMethod prog comp newMthd oldMethod =
+ match prog, comp with
+ | Program(clist), Component(Class(cname, ctypeParams, members), model, code) ->
+ let newMembers =
+ match oldMethod with
+ | None -> members @ [newMthd]
+ | Some(m) -> Utils.ListReplace m newMthd members
+ let newCls = Class(cname, ctypeParams, newMembers)
let newComp = Component(newCls, model, code)
let newProg = Program(Utils.ListReplace comp newComp clist)
+ newProg, newComp
+ | _ -> failwithf "Invalid component: %O" comp
+
+let AddPrecondition prog comp m e =
+ match m with
+ | Method(mn, sgn, pre, post, cstr) ->
+ let newMthd = Method(mn, sgn, BinaryAnd pre e, post, cstr)
+ let newProg, newComp = AddReplaceMethod prog comp newMthd (Some(m))
newProg, newComp, newMthd
| _ -> failwithf "Not a method: %O" m
@@ -495,6 +529,10 @@ let rec __EvalSym resolverFunc ctx expr =
| SetExpr(elist) ->
let eset' = elist |> List.fold (fun acc e -> Set.add (__EvalSym resolverFunc ctx e) acc) Set.empty
SetExpr(Set.toList eset')
+ | MethodCall(rcv,name,aparams) ->
+ let rcv' = __EvalSym resolverFunc ctx rcv
+ let aparams' = aparams |> List.fold (fun acc e -> __EvalSym resolverFunc ctx e :: acc) [] |> List.rev
+ MethodCall(rcv', name, aparams')
| SelectExpr(lst, idx) ->
let lst', idx' = __EvalSym resolverFunc ctx lst, __EvalSym resolverFunc ctx idx
match lst', idx' with
@@ -702,7 +740,8 @@ let rec Desugar expr =
| SelectExpr(_)
| SeqLength(_)
| UpdateExpr(_)
- | SetExpr(_)
+ | SetExpr(_)
+ | MethodCall(_)
| SequenceExpr(_) -> expr
// forall v :: v in {a1 a2 ... an} ==> e ~~~> e[v/a1] && e[v/a2] && ... && e[v/an]
// forall v :: v in [a1 a2 ... an] ==> e ~~~> e[v/a1] && e[v/a2] && ... && e[v/an]
@@ -768,5 +807,6 @@ let ChangeThisReceiver receiver expr =
| UpdateExpr(e1,e2,e3) -> UpdateExpr(__ChangeThis locals e1, __ChangeThis locals e2, __ChangeThis locals e3)
| SequenceExpr(exs) -> SequenceExpr(exs |> List.map (__ChangeThis locals))
| SetExpr(exs) -> SetExpr(exs |> List.map (__ChangeThis locals))
+ | MethodCall(rcv,name,aparams) -> MethodCall(__ChangeThis locals rcv, name, aparams |> List.map (__ChangeThis locals))
(* --- function body starts here --- *)
__ChangeThis Set.empty expr
diff --git a/Jennisys/Jennisys/CodeGen.fs b/Jennisys/Jennisys/CodeGen.fs
index 54c22053..5a1f108c 100644
--- a/Jennisys/Jennisys/CodeGen.fs
+++ b/Jennisys/Jennisys/CodeGen.fs
@@ -159,17 +159,22 @@ let PrintVarAssignments heapInst indent =
let idt = Indent indent
heapInst.assignments |> List.fold (fun acc ((o,f),e) ->
let fldName = PrintVarName f
- let value = PrintExpr 0 e
- acc + (sprintf "%s%s.%s := %s;" idt o.name fldName value) + newline
+ let exprStr =
+ if fldName = "" then
+ sprintf "%s;" (PrintExpr 0 e)
+ else
+ let value = PrintExpr 0 e
+ sprintf "%s.%s := %s;" o.name fldName value
+ acc + idt + exprStr + newline
) ""
let PrintReprAssignments prog heapInst indent =
let __FollowsFunc o1 o2 =
heapInst.assignments |> List.fold (fun acc ((srcObj,fld),value) ->
acc || (srcObj = o1 && value = ObjLiteral(o2.name))
- ) false
+ ) false
let idt = Indent indent
- let objs = heapInst.assignments |> List.fold (fun acc ((obj,fld),_) -> acc |> Set.add obj) Set.empty
+ let objs = heapInst.assignments |> List.fold (fun acc ((obj,(Var(fldName,_))),_) -> if fldName = "" then acc else acc |> Set.add obj) Set.empty
|> Set.toList
|> Utils.TopSort __FollowsFunc
|> List.rev
@@ -224,18 +229,30 @@ let rec PrintHeapCreationCode prog sol indent genRepr =
(__ReprAssignments indent)
| [] -> ""
+let PrintPrePost pfix expr =
+ SplitIntoConjunts expr |> PrintSep "" (fun e -> pfix + (PrintExpr 0 e) + ";")
+
+let GetPostconditionForMethod m genRepr =
+ let validExpr = IdLiteral("Valid()");
+ match m with
+ | Method(_,_,_,post,_) ->
+ let postExpr = BinaryAnd validExpr post
+ if genRepr then
+ BinaryAnd (IdLiteral("fresh(Repr - {this})")) postExpr
+ else
+ postExpr
+ | _ -> failwithf "expected a method, got %O" m
+
let GenConstructorCode mthd body genRepr =
let validExpr = IdLiteral("Valid()");
match mthd with
| Method(methodName, sign, pre, post, _) ->
- let __PrintPrePost pfix expr = SplitIntoConjunts expr |> PrintSep "" (fun e -> pfix + (PrintExpr 0 e) + ";")
let preExpr = pre
- let postExpr = BinaryAnd validExpr post
+ let postExpr = GetPostconditionForMethod mthd genRepr
" method " + methodName + (PrintSig sign) + newline +
" modifies this;" +
- (__PrintPrePost (newline + " requires ") preExpr) +
- Utils.Ite genRepr (newline + " ensures fresh(Repr - {this});") "" +
- (__PrintPrePost (newline + " ensures ") postExpr) +
+ (PrintPrePost (newline + " requires ") preExpr) +
+ (PrintPrePost (newline + " ensures ") postExpr) +
newline +
" {" + newline +
body +
@@ -249,7 +266,9 @@ let PrintImplCode prog solutions methodsToPrintFunc genRepr =
if Utils.ListContains (comp,mthd) methods then
let mthdBody = match Map.tryFind (comp,mthd) solutions with
| Some(sol) -> PrintHeapCreationCode prog sol 4 genRepr
- | _ -> " //unable to synthesize" + newline
+ | _ ->
+ " //unable to synthesize" +
+ PrintPrePost (newline + " assume ") (GetPostconditionForMethod mthd genRepr) + newline
(GenConstructorCode mthd mthdBody genRepr) + newline
else
"") genRepr \ No newline at end of file
diff --git a/Jennisys/Jennisys/DafnyPrinter.fs b/Jennisys/Jennisys/DafnyPrinter.fs
index 86974f20..495daba9 100644
--- a/Jennisys/Jennisys/DafnyPrinter.fs
+++ b/Jennisys/Jennisys/DafnyPrinter.fs
@@ -1,76 +1,78 @@
-module DafnyPrinter
-
-open Ast
-open AstUtils
-open Printer
-
-let rec PrintType ty =
- match ty with
- | IntType -> "int"
- | BoolType -> "bool"
- | SeqType(t) -> sprintf "seq<%s>" (PrintType t)
- | SetType(t) -> sprintf "set<%s>" (PrintType t)
- | NamedType(id,args) -> if List.isEmpty args then id else sprintf "%s<%s>" id (PrintSep ", " (fun s -> s) args)
- | InstantiatedType(id,args) -> sprintf "%s<%s>" id (PrintSep ", " (fun t -> PrintType t) args)
-
-let rec PrintExpr ctx expr =
- match expr with
- | IntLiteral(d) -> sprintf "%d" d
- | BoolLiteral(b) -> sprintf "%b" b
- | ObjLiteral(id)
- | VarLiteral(id)
- | IdLiteral(id) -> id
- | Star -> assert false; "" // I hope this won't happen
- | Dot(e,id) -> sprintf "%s.%s" (PrintExpr 100 e) id
- | UnaryExpr(op,UnaryExpr(op2, e2)) -> sprintf "%s(%s)" op (PrintExpr 90 (UnaryExpr(op2, e2)))
- | UnaryExpr(op,e) -> sprintf "%s%s" op (PrintExpr 90 e)
- | BinaryExpr(strength,op,e0,e1) ->
- let op =
- match op with
- | "=" -> "=="
- | "div" -> "/"
- | "mod" -> "%"
- | _ -> op
- let needParens = strength <= ctx
- let openParen = if needParens then "(" else ""
- let closeParen = if needParens then ")" else ""
- sprintf "%s%s %s %s%s" openParen (PrintExpr strength e0) op (PrintExpr strength e1) closeParen
- | IteExpr(c,e1,e2) -> sprintf "(if %s then %s else %s)" (PrintExpr 25 c) (PrintExpr 25 e1) (PrintExpr 25 e2)
- | SelectExpr(e,i) -> sprintf "%s[%s]" (PrintExpr 100 e) (PrintExpr 0 i)
- | UpdateExpr(e,i,v) -> sprintf "%s[%s := %s]" (PrintExpr 100 e) (PrintExpr 0 i) (PrintExpr 0 v)
- | SequenceExpr(ee) -> sprintf "[%s]" (ee |> PrintSep ", " (PrintExpr 0))
- | SeqLength(e) -> sprintf "|%s|" (PrintExpr 0 e)
- | SetExpr(ee) -> sprintf "{%s}" (ee |> PrintSep ", " (PrintExpr 0))
- | ForallExpr(vv,e) ->
- let needParens = true
- let openParen = if needParens then "(" else ""
- let closeParen = if needParens then ")" else ""
- sprintf "%sforall %s :: %s%s" openParen (vv |> PrintSep ", " PrintVarDecl) (PrintExpr 0 e) closeParen
-
-let rec PrintConst cst =
- match cst with
- | IntConst(v) -> sprintf "%d" v
- | BoolConst(b) -> sprintf "%b" b
- | VarConst(v) -> sprintf "%s" v
- | SetConst(cset) -> sprintf "{%s}" (PrintSep ", " (fun c -> PrintConst c) (Set.toList cset))
- | SeqConst(cseq) -> sprintf "[%s]" (PrintSep ", " (fun c -> PrintConst c) cseq)
- | NullConst -> "null"
- | NoneConst -> "<none>"
- | ThisConst(_,_) -> "this"
- | NewObj(name,_) -> PrintGenSym name
- | Unresolved(name) -> sprintf "Unresolved(%s)" name
-
-let PrintTypeParams typeParams =
- match typeParams with
- | [] -> ""
- | _ -> sprintf "<%s>" (typeParams |> PrintSep ", " (fun tp -> tp))
-
-let PrintFields vars indent ghost =
- let ghostStr = if ghost then "ghost " else ""
- vars |> List.fold (fun acc v -> match v with
- | Var(nm,None) -> acc + (sprintf "%s%svar %s;%s" (Indent indent) ghostStr nm newline)
- | Var(nm,Some(tp)) -> acc + (sprintf "%s%svar %s: %s;%s" (Indent indent) ghostStr nm (PrintType tp) newline)) ""
-
+module DafnyPrinter
+
+open Ast
+open AstUtils
+open Printer
+
+let rec PrintType ty =
+ match ty with
+ | IntType -> "int"
+ | BoolType -> "bool"
+ | SeqType(t) -> sprintf "seq<%s>" (PrintType t)
+ | SetType(t) -> sprintf "set<%s>" (PrintType t)
+ | NamedType(id,args) -> if List.isEmpty args then id else sprintf "%s<%s>" id (PrintSep ", " (fun s -> s) args)
+ | InstantiatedType(id,args) -> sprintf "%s<%s>" id (PrintSep ", " (fun t -> PrintType t) args)
+
+let rec PrintExpr ctx expr =
+ match expr with
+ | IntLiteral(d) -> sprintf "%d" d
+ | BoolLiteral(b) -> sprintf "%b" b
+ | ObjLiteral(id)
+ | VarLiteral(id)
+ | IdLiteral(id) -> id
+ | Star -> assert false; "" // I hope this won't happen
+ | Dot(e,id) -> sprintf "%s.%s" (PrintExpr 100 e) id
+ | UnaryExpr(op,UnaryExpr(op2, e2)) -> sprintf "%s(%s)" op (PrintExpr 90 (UnaryExpr(op2, e2)))
+ | UnaryExpr(op,e) -> sprintf "%s%s" op (PrintExpr 90 e)
+ | BinaryExpr(strength,op,e0,e1) ->
+ let op =
+ match op with
+ | "=" -> "=="
+ | "div" -> "/"
+ | "mod" -> "%"
+ | _ -> op
+ let needParens = strength <= ctx
+ let openParen = if needParens then "(" else ""
+ let closeParen = if needParens then ")" else ""
+ sprintf "%s%s %s %s%s" openParen (PrintExpr strength e0) op (PrintExpr strength e1) closeParen
+ | IteExpr(c,e1,e2) -> sprintf "(if %s then %s else %s)" (PrintExpr 25 c) (PrintExpr 25 e1) (PrintExpr 25 e2)
+ | SelectExpr(e,i) -> sprintf "%s[%s]" (PrintExpr 100 e) (PrintExpr 0 i)
+ | UpdateExpr(e,i,v) -> sprintf "%s[%s := %s]" (PrintExpr 100 e) (PrintExpr 0 i) (PrintExpr 0 v)
+ | SequenceExpr(ee) -> sprintf "[%s]" (ee |> PrintSep ", " (PrintExpr 0))
+ | SeqLength(e) -> sprintf "|%s|" (PrintExpr 0 e)
+ | SetExpr(ee) -> sprintf "{%s}" (ee |> PrintSep ", " (PrintExpr 0))
+ | ForallExpr(vv,e) ->
+ let needParens = true
+ let openParen = if needParens then "(" else ""
+ let closeParen = if needParens then ")" else ""
+ sprintf "%sforall %s :: %s%s" openParen (vv |> PrintSep ", " PrintVarDecl) (PrintExpr 0 e) closeParen
+ | MethodCall(rcv, name, aparams) ->
+ sprintf "%s.%s(%s)" (PrintExpr 0 rcv) name (aparams |> PrintSep ", " (PrintExpr 0))
+
+let rec PrintConst cst =
+ match cst with
+ | IntConst(v) -> sprintf "%d" v
+ | BoolConst(b) -> sprintf "%b" b
+ | VarConst(v) -> sprintf "%s" v
+ | SetConst(cset) -> sprintf "{%s}" (PrintSep ", " (fun c -> PrintConst c) (Set.toList cset))
+ | SeqConst(cseq) -> sprintf "[%s]" (PrintSep ", " (fun c -> PrintConst c) cseq)
+ | NullConst -> "null"
+ | NoneConst -> "<none>"
+ | ThisConst(_,_) -> "this"
+ | NewObj(name,_) -> PrintGenSym name
+ | Unresolved(name) -> sprintf "Unresolved(%s)" name
+
+let PrintTypeParams typeParams =
+ match typeParams with
+ | [] -> ""
+ | _ -> sprintf "<%s>" (typeParams |> PrintSep ", " (fun tp -> tp))
+
+let PrintFields vars indent ghost =
+ let ghostStr = if ghost then "ghost " else ""
+ vars |> List.fold (fun acc v -> match v with
+ | Var(nm,None) -> acc + (sprintf "%s%svar %s;%s" (Indent indent) ghostStr nm newline)
+ | Var(nm,Some(tp)) -> acc + (sprintf "%s%svar %s: %s;%s" (Indent indent) ghostStr nm (PrintType tp) newline)) ""
+
let rec PrintStmt stmt indent =
let idt = (Indent indent)
match stmt with
diff --git a/Jennisys/Jennisys/Jennisys.fsproj b/Jennisys/Jennisys/Jennisys.fsproj
index 69ab0ff2..49696e58 100644
--- a/Jennisys/Jennisys/Jennisys.fsproj
+++ b/Jennisys/Jennisys/Jennisys.fsproj
@@ -23,7 +23,7 @@
<WarningLevel>3</WarningLevel>
<PlatformTarget>x86</PlatformTarget>
<DocumentationFile>bin\Debug\Language.XML</DocumentationFile>
- <StartArguments>examples/Set.jen /method:Set.Double /genRepr /noVerifyParSol</StartArguments>
+ <StartArguments>examples/List.jen /method:List.Double /genRepr</StartArguments>
<StartWorkingDirectory>C:\boogie\Jennisys\Jennisys\</StartWorkingDirectory>
</PropertyGroup>
<PropertyGroup Condition=" '$(Configuration)|$(Platform)' == 'Release|x86' ">
diff --git a/Jennisys/Jennisys/Printer.fs b/Jennisys/Jennisys/Printer.fs
index f8f2933b..ca65f495 100644
--- a/Jennisys/Jennisys/Printer.fs
+++ b/Jennisys/Jennisys/Printer.fs
@@ -56,6 +56,8 @@ let rec PrintExpr ctx expr =
let openParen = if needParens then "(" else ""
let closeParen = if needParens then ")" else ""
sprintf "%sforall %s :: %s%s" openParen (vv |> PrintSep ", " PrintVarDecl) (PrintExpr 0 e) closeParen
+ | MethodCall(rcv,name,aparams) ->
+ sprintf "%s.%s(%s)" (PrintExpr 0 rcv) name (aparams |> PrintSep ", " (PrintExpr 0))
let rec PrintConst cst =
match cst with
generated by cgit v1.2.3 (git 2.39.1) at 2024-09-17 06:38:59 +0000