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
|
module Printer
open Ast
let rec PrintSep sep f list =
match list with
| [] -> ()
| [a] -> f a
| a :: more -> f a ; printf "%s" sep ; PrintSep sep f more
let rec PrintType ty =
match ty with
| NamedType(id) -> printf "%s" id
| InstantiatedType(id,arg) -> printf "%s[" id ; PrintType arg ; printf "]"
let PrintVarDecl vd =
match vd with
| Var(id,None) -> printf "%s" id
| Var(id,Some(ty)) -> printf "%s: " id ; PrintType ty
let rec PrintExpr ctx expr =
match expr with
| IntLiteral(n) -> printf "%O" n
| IdLiteral(id) -> printf "%s" id
| Star -> printf "*"
| Dot(e,id) -> PrintExpr 100 e ; printf ".%s" id
| UnaryExpr(op,e) -> printf "%s" op ; PrintExpr 90 e
| BinaryExpr((strength,op),e0,e1) ->
let needParens = strength <= ctx
if needParens then printf "(" else ()
PrintExpr strength e0 ; printf " %s " op ; PrintExpr strength e1
if needParens then printf ")" else ()
| SelectExpr(e,i) -> PrintExpr 100 e ; printf "[" ; PrintExpr 0 i ; printf "]"
| UpdateExpr(e,i,v) -> PrintExpr 100 e ; printf "[" ; PrintExpr 0 i ; printf " := " ; PrintExpr 0 v ; printf "]"
| SequenceExpr(ee) -> printf "[" ; ee |> PrintSep ", " (PrintExpr 0) ; printf "]"
| SeqLength(e) -> printf "|" ; PrintExpr 0 e ; printf "|"
| ForallExpr(vv,e) ->
let needParens = ctx <> 0
if needParens then printf "(" else ()
printf "forall " ; vv |> PrintSep ", " PrintVarDecl ; printf " :: " ; PrintExpr 0 e
if needParens then printf ")" else ()
let PrintSig signature =
match signature with
| Sig(ins, outs) ->
printf "("
ins |> PrintSep ", " PrintVarDecl
printf ")"
if outs <> [] then
printf " returns ("
outs |> PrintSep ", " PrintVarDecl
printf ")"
else ()
let rec ForeachConjunct f expr =
match expr with
| IdLiteral("true") -> ()
| BinaryExpr((_,"&&"),e0,e1) -> ForeachConjunct f e0 ; ForeachConjunct f e1
| _ -> f expr
let rec Indent i =
if i = 0 then () else printf " " ; Indent (i-1)
let rec PrintStmt stmt indent =
match stmt with
| Block(stmts) ->
Indent indent ; printfn "{"
PrintStmtList stmts (indent + 2)
Indent indent ; printfn "}"
| Assign(lhs,rhs) -> Indent indent ; PrintExpr 0 lhs ; printf " := " ; PrintExpr 0 rhs ; printfn ""
and PrintStmtList stmts indent =
stmts |> List.iter (fun s -> PrintStmt s indent)
let PrintRoutine signature pre body =
PrintSig signature
printfn ""
pre |> ForeachConjunct (fun e -> printf " requires " ; PrintExpr 0 e ; printfn "")
PrintStmtList body 2
let PrintMember m =
match m with
| Field(vd) -> printf " var " ; PrintVarDecl vd ; printfn ""
| Constructor(id,signature,pre,body) -> printf " constructor %s" id ; PrintRoutine signature pre body
| Method(id,signature,pre,body) -> printf " method %s" id ; PrintRoutine signature pre body
let PrintTopLevelDeclHeader kind id typeParams =
printf "%s %s" kind id
match typeParams with
| [] -> ()
| _ -> printf "[" ; typeParams |> PrintSep ", " (fun tp -> printf "%s" tp) ; printf "]"
printfn " {"
let PrintDecl d =
match d with
| Class(id,typeParams,members) ->
PrintTopLevelDeclHeader "class" id typeParams
List.iter PrintMember members
printfn "}"
| Model(id,typeParams,vars,frame,inv) ->
PrintTopLevelDeclHeader "model" id typeParams
vars |> List.iter (fun vd -> printf " var " ; PrintVarDecl vd ; printfn "")
printfn " frame"
frame |> List.iter (fun fr -> printf " " ; PrintExpr 0 fr ; printfn "")
printfn " invariant"
inv |> ForeachConjunct (fun e -> printf " " ; PrintExpr 0 e ; printfn "")
printfn "}"
| Code(id,typeParams) ->
PrintTopLevelDeclHeader "code" id typeParams
printfn "}"
let Print prog =
match prog with
| Program(decls) -> List.iter PrintDecl decls
|
