1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
|
module Printer
open Ast
open AstUtils
let newline = System.Environment.NewLine // "\r\n"
let rec PrintSep sep f list =
match list with
| [] -> ""
| [a] -> f a
| a :: more -> (f a) + sep + (PrintSep sep f more)
let rec PrintType ty =
match ty with
| IntType -> "int"
| BoolType -> "bool"
| NamedType(id, args) -> if List.isEmpty args then id else (PrintSep ", " (fun s -> s) args)
| SeqType(t) -> sprintf "seq[%s]" (PrintType t)
| SetType(t) -> sprintf "set[%s]" (PrintType t)
| InstantiatedType(id,args) -> sprintf "%s[%s]" id (PrintSep ", " (fun a -> PrintType a) args)
let PrintVarDecl vd =
match vd with
| 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(d) -> sprintf "%d" d
| BoolLiteral(b) -> sprintf "%b" b
| ObjLiteral(id)
| VarLiteral(id)
| IdLiteral(id) -> id
| Star -> "*"
| 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 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 "%s ? %s : %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 = ctx <> 0
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 PrintSig signature =
match signature with
| Sig(ins, outs) ->
let returnClause =
if outs <> [] then sprintf " returns (%s)" (outs |> PrintSep ", " PrintVarDecl)
else ""
sprintf "(%s)%s" (ins |> PrintSep ", " PrintVarDecl) returnClause
let rec Indent i =
if i = 0 then "" else " " + (Indent (i-1))
let rec PrintStmt stmt indent =
let idt = (Indent indent)
match stmt with
| Block(stmts) ->
idt + "{" + newline +
(PrintStmtList stmts (indent + 2)) +
idt + "}" + newline
| Assign(lhs,rhs) -> sprintf "%s%s := %s%s" idt (PrintExpr 0 lhs) (PrintExpr 0 rhs) newline
and PrintStmtList stmts indent =
stmts |> List.fold (fun acc s -> acc + (PrintStmt s indent)) ""
let PrintRoutine signature pre body =
let preStr = pre |> ForeachConjunct (fun e -> sprintf " requires %s%s" (PrintExpr 0 e) newline)
sprintf "%s%s%s%s" (PrintSig signature) newline preStr (PrintExpr 0 body)
let PrintMember m =
match m with
| Field(vd) -> sprintf " var %s%s" (PrintVarDecl vd) newline
| Method(id,signature,pre,body,true) -> sprintf " constructor %s%s" id (PrintRoutine signature pre body)
| Method(id,signature,pre,body,false) -> sprintf " method %s%s" id (PrintRoutine signature pre body)
| Invariant(_) -> "" // invariants are handled separately
let PrintTopLevelDeclHeader kind id typeParams =
let typeParamStr =
match typeParams with
| [] -> ""
| _ -> sprintf "[%s]" (typeParams |> PrintSep ", " (fun tp -> tp))
sprintf "%s %s%s {%s" kind id typeParamStr newline
let PrintDecl d =
match d with
| Class(id,typeParams,members) ->
sprintf "%s%s}%s" (PrintTopLevelDeclHeader "class" id typeParams)
(List.fold (fun acc m -> acc + (PrintMember m)) "" members)
newline
| Model(id,typeParams,vars,frame,inv) ->
(PrintTopLevelDeclHeader "model" id typeParams) +
(vars |> List.fold (fun acc vd -> acc + " var " + (PrintVarDecl vd) + newline) "") +
" frame" + newline +
(frame |> List.fold (fun acc fr -> acc + " " + (PrintExpr 0 fr) + newline) "") +
" invariant" + newline +
(inv |> ForeachConjunct (fun e -> " " + (PrintExpr 0 e) + newline)) +
"}" + newline
| Code(id,typeParams) ->
(PrintTopLevelDeclHeader "code" id typeParams) + "}" + newline
let PrintMethodSignFull indent comp m =
let idt = Indent indent
let __PrintPrePost pfix expr = SplitIntoConjunts expr |> PrintSep newline (fun e -> pfix + (PrintExpr 0 e) + ";")
let compName = GetComponentName comp
match m with
| Method(methodName, sgn, pre, post, isConstr) ->
let mc = if isConstr then "constructor" else "method"
let preStr = (__PrintPrePost (idt + " requires ") pre)
let postStr = (__PrintPrePost (idt + " ensures ") post)
idt + mc + " " + compName + "." + methodName + (PrintSig sgn) + newline +
preStr + (if preStr = "" then "" else newline) +
postStr
| _ -> failwithf "not a method: %O" m
let Print prog =
match prog with
| SProgram(decls) -> List.fold (fun acc d -> acc + (PrintDecl d)) "" decls
let PrintObjRefName o =
match o with
| ThisConst(_,_) -> "this";
| NewObj(name, _) -> PrintGenSym name
| _ -> failwith ("unresolved object ref: " + o.ToString())
|
