ocaml.drv 1.06 KB
Newer Older
1

2
printer "ocaml"
3 4

theory BuiltIn
5 6 7 8 9 10
  syntax predicate  (=)   "((%1) = (%2))"
end

theory HighOrd
  syntax type func "((%1) -> (%2))"
  syntax type pred "((%1) -> bool)"
11
  syntax function (@) "((%1) (%2))"
12 13 14
end

theory option.Option
15
  syntax type     option "((%1) option)"
16
  syntax function None   "None"
17
  syntax function Some   "(Some (%1))"
18 19 20
end

theory Bool
21
  syntax type     bool  "bool"
22 23 24 25 26
  syntax function True  "true"
  syntax function False "false"
end

theory bool.Bool
27 28
  syntax function andb  "((%1) && (%2))"
  syntax function orb   "((%1) || (%2))"
29
  (* syntax function xorb  "(xorb (%1) (%2))" *)
30
  syntax function notb  "(not (%1))"
31
  (* syntax function implb "(implb (%1))" *)
32 33 34
end

theory list.List
35
  syntax type     list "(%1) list"
36
  syntax function Nil  "[]"
37
  syntax function Cons "((%1) :: (%2))"
38 39 40
end


41 42 43
(* WhyML *)

module ref.Ref
44
  syntax type     ref      "((%1) Pervasives.ref)"
45
  syntax function contents "(%1).Pervasives.contents"
46 47 48
  syntax val      ref      "Pervasives.ref"
  syntax val      (!_)     "Pervasives.(!)"
  syntax val      (:=)     "Pervasives.(:=)"
49 50
end