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
module LangDef.Extra

open LangDef
open PrettyPrint
open StarCombinator
open WithBottom
open Doc
open MachineIntegers

let string_of_binop = function | Plus -> "+" | Minus -> "-" | Mult -> "*" | Eq -> "=" | Lt -> "<" | And -> "&&" | Or -> "||"
let string_of_varname = function | VA -> "a" | VB -> "b" | VC -> "c" | VD -> "d"
let rec string_of_expr' e par
  = let lparen = if par then "(" else "" in
    let rparen = if par then ")" else "" in
    match e with
  | Const i -> string_of_int i
  | BinOp op a b -> lparen ^ string_of_expr' a true ^ " " ^ string_of_binop op ^ " " ^ string_of_expr' b true ^ rparen
  | Var v -> string_of_varname v
  | _ -> "?"

let string_of_expr e = string_of_expr' e false

let rec doc_of_stmt (s: stmt): doc unit = match s with
  | Assign v e -> str (string_of_varname v) <+> str " = " <+> str (string_of_expr e)
  | Assume e -> str "assume" <+> space <+> lparen <+> str (string_of_expr e) <+> rparen
  | If c a b -> str "if" <+> space <+> lparen <+> str (string_of_expr c) <+> rparen
           <+> lbrace <+> indent (nl <+> doc_of_stmt a) <+> nl
           <+> rbrace <+> str " else "
           <+> lbrace <+> indent (nl <+> doc_of_stmt b) <+> nl <+> rbrace
  | Seq a b -> doc_of_stmt a <+> str ";" <+> nl <+> doc_of_stmt b
  | Loop a -> str "loop " <+> lbrace <+> indent (nl <+> doc_of_stmt a) <+> nl <+> rbrace <+> nl

let string_of_stmt s = doc_to_string (doc_of_stmt s)

let int_m_parser: parser int_m
  = flatten_option
    ((fun (x: int) -> if inbounds x then Some (x <: int_m) else None) @<< number)
    "This number is not in [-127;127]"

let operator' (l: _ {l <> []}) = spaces <*>> choice (List.Tot.map exact_string l) <<*> spaces

let binop_parser: parser binop
  = (function
    | "+"  -> Plus
    | "-"  -> Minus
    | "*"  -> Mult
    | "==" -> Eq
    | "<"  -> Lt
    | "&&" -> And
    | _ -> Or
    ) @<< operator' ["+";"-";"*";"<";"==";"&&";"||"]
  
let varname_parser: parser varname
  =   VA *<< (exact_string "a")
  <|> VB *<< (exact_string "b")
  <|> VC *<< (exact_string "c")
  <|> VD *<< (exact_string "d")

let between_par = between_kwd "(" ")"
let between_braces = between_kwd "{" "}"

let expr_parser: parser expr =
  let rec no_rec (): parser expr =
          between_par  (admitP (()<<()); delayMe h')
      <|> Const @<< number
      <|> Var @<< varname_parser
  and h' (): parser expr = admitP (() << ()); let h = delayMe h' in
       (function 
       | (e, None) -> e
       | (l, Some (op, r)) -> BinOp op l r
       )@<< (no_rec () <*> maybe (binop_parser <*> h))
  in wrapspace (h' ())

let stmt_parser: parser stmt =
  let rec no_rec (): parser stmt =
           Assume @<< (keyword "assume" <*>> expr_parser)
      <|> (fun (v, n) -> Assign v n) @<< (varname_parser <*> (operator "=" <*>> expr_parser))
  and h' (): parser stmt = admitP (() << ()); let h = delayMe h' in
      begin
        (function
        | (l, Some r) -> Seq l r
        | (l, None) -> l
        ) @<<
        ((    (fun ((c, a), b) -> If c a b) @<< ((keyword "if" <*>> between_par expr_parser) <*> between_braces h <*> (keyword "else" <*>> between_braces h))
          <|> Loop @<< (keyword "loop" <*>> between_braces h)) <*> maybe h)
      end
      <|> (function 
          | (e, None) -> e
          | (l, Some r) -> Seq l r
          ) @<< (no_rec () <*> maybe (operator ";" <*>> h))
  in wrapspace (h' ()) <<*> maybe (operator ";")

instance stmt_pp: prettyprintable stmt = { print = string_of_stmt }
instance expr_pp: prettyprintable expr = { print = string_of_expr }
instance binop_pp: prettyprintable binop = { print = string_of_binop }
instance varname_pp: prettyprintable varname = { print = string_of_varname }