ocaml.drv 1.1 KB
Newer Older
1

2
printer "ocaml"
3 4

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

theory HighOrd
  syntax type func "((%1) -> (%2))"
  syntax type pred "((%1) -> bool)"
  syntax function (@!) "((%1) (%2))"
  syntax predicate (@?) "((%1) (%2))"
13 14 15
end

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

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

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

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


42 43 44
(* WhyML *)

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