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
|
module ForroPrinter
open System
open Forro
let PrintField f =
printf "."
match f with
| Head -> printf "head"
| Tail -> printf "tail"
| Valid -> printf "valid"
let PrintOp op =
printf " "
match op with
| Eq -> printf "=="
| Neq -> printf "!="
| Plus -> printf "+"
| Minus -> printf "-"
| Times -> printf "*"
| Less -> printf "<"
| AtMost -> printf "<="
| And -> printf "and"
| Or -> printf "or"
printf " "
let rec PrintExpr e outermost =
match e with
| Constant(x) -> printf "%i" x
| Null -> printf "null"
| Identifier(Var(x)) -> printf "%s" x
| Not(e) -> printf "not(" ; PrintExpr e true ; printf ")"
| Binary(op,a,b) ->
if outermost then () else printf "("
PrintExpr a false ; PrintOp op ; PrintExpr b false
if outermost then () else printf ")"
| Select(e,f) -> PrintExpr e false ; PrintField f
| Old(e) -> printf "old(" ; PrintExpr e true ; printf ")"
let rec Indent n =
if n = 0 then () else printf " " ; Indent (n-1)
let rec PrintStmt indent s =
Indent indent
let ind = indent + 2
match s with
| Assign(Var(x), e) -> printf "%s" x ; printf " := " ; PrintExpr e true
| Update(obj,f,rhs) -> PrintExpr obj false ; PrintField f ; printf " := " ; PrintExpr rhs true
| Alloc(Var(x),hd,tl) -> printf "%s" x ; printf " := new (" ; PrintExpr hd false ; printf ", " ; PrintExpr tl false ; printf ")"
| IfStmt(guard,thn,els) ->
printf "if " ; PrintExpr guard true ; printfn " then"
PrintStmtList ind thn
Indent indent ; printfn "else"
PrintStmtList ind els
Indent indent ; printf "end"
| WhileStmt(guard,invs,body) ->
printf "while " ; PrintExpr guard true ; printfn ""
List.iter (fun inv -> Indent ind ; printf "invariant " ; PrintExpr inv true ; printfn "") invs
Indent indent ; printfn "do"
PrintStmtList ind body
Indent indent ; printf "end"
| CallStmt(outs,id,ins) ->
printf "call "
if outs.IsEmpty then () else
ignore (List.fold (fun sep v -> printf "%s%s" sep (VarName v) ; ", ") "" outs) ; printf " :="
printf " %s" id
printf "("
ignore (List.fold (fun sep e -> printf "%s" sep ; PrintExpr e false ; ", ") "" ins)
printf ")"
| Assert(e) ->
printf "assert " ; PrintExpr e true
printfn ";"
and PrintStmtList indent slist =
match slist with
| Block(ss) -> List.iter (fun s -> PrintStmt indent s) ss
let PrintProc p =
match p with
| Proc(name, ins, outs, req, ens, body) ->
// signature
printf "procedure "
if outs.IsEmpty then () else
ignore (List.fold (fun sep v -> printf "%s%s" sep (VarName v) ; ", ") "" outs) ; printf " :="
printf " %s(" name
ignore (List.fold (fun sep v -> printf "%s%s" sep (VarName v) ; ", ") "" ins)
printfn ")"
// specification
printf " requires "
PrintExpr req true
printfn ""
printf " ensures "
PrintExpr ens true
printfn ""
// body
printfn "do"
PrintStmtList 2 body
printfn "end;"
let rec PrintProcs ps =
match ps with
| [] -> ()
| p::rest -> PrintProc p ; PrintProcs rest
let Print prog =
match prog with
| Prog(procs) -> PrintProcs procs
|
