summaryrefslogtreecommitdiff
path: root/Source/Forro/Printer.fs
diff options
context:
space:
mode:
Diffstat (limited to 'Source/Forro/Printer.fs')
-rw-r--r--Source/Forro/Printer.fs214
1 files changed, 107 insertions, 107 deletions
diff --git a/Source/Forro/Printer.fs b/Source/Forro/Printer.fs
index 2a9eac84..d168e094 100644
--- a/Source/Forro/Printer.fs
+++ b/Source/Forro/Printer.fs
@@ -1,107 +1,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
+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
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-02 01:05:29 +0000