ocaml-no-arith.drv 1.96 KB
Newer Older
1 2 3

(** Arithmetic-independent OCaml driver *)

4
(* FIXME
5 6 7 8 9
theory HighOrd
  syntax type func "(%1 -> %2)"
  syntax type pred "(%1 -> bool)"
  syntax function (@) "(%1 %2)"
end
10
*)
11 12

theory option.Option
13
  syntax type     option "%1 option"
14
  syntax function None   "None"
15
  syntax function Some   "Some %1"
16 17 18 19 20 21 22 23 24 25 26 27 28 29 30
end

(* bool *)

theory Bool
  syntax type     bool  "bool"
  syntax function True  "true"
  syntax function False "false"
end

theory bool.Ite
  syntax function ite "(if %1 then %2 else %3)"
end

theory bool.Bool
31 32 33 34 35
  syntax function andb  "%1 && %2"
  syntax function orb   "%1 || %2"
  syntax function xorb  "%1 <> %2"
  syntax function notb  "not %1"
  syntax function implb "not %1 || %2"
36 37 38 39 40 41 42
end

(* list *)

theory list.List
  syntax type     list "%1 list"
  syntax function Nil  "[]"
43
  syntax function Cons "%1 :: %2"
44 45 46
end

theory list.Mem
47
  syntax predicate mem "List.mem %1 %2"
48 49 50
end

theory list.Append
51
  syntax function (++) "List.append %1 %2"
52 53 54
end

theory list.Reverse
55
  syntax function reverse "List.rev %1"
56 57 58
end

theory list.RevAppend
59
  syntax function rev_append "List.rev_append %1 %2"
60 61 62
end

theory list.Combine
63
  syntax function combine "List.combine %1 %2"
64 65 66 67 68
end

(* WhyML *)

module ref.Ref
69 70 71 72 73
  syntax type     ref      "%1 ref"
  syntax function contents "!%1"
  syntax val      ref      "ref %1"
  syntax val      (!_)     "!%1"
  syntax val      (:=)     "%1 := %2"
74 75
end

Mário Pereira's avatar
Mário Pereira committed
76 77
(* FIXME: once we extract ref.Refint, this module
          will no longer be useful in the driver *)
Mário Pereira's avatar
Mário Pereira committed
78 79
module ref.Refint
  syntax val incr "%1 := Z.succ (Pervasives.(!) %1)"
Mário Pereira's avatar
Mário Pereira committed
80 81 82 83
  syntax val decr "%1 := Z.pred (Pervasives.(!) %1)"
  syntax val (+=) "%1 := Z.add (Pervasives.(!) %1) %2"
  syntax val (-=) "%1 := Z.sub (Pervasives.(!) %1) %2"
  syntax val ( *= ) "%1 := Z.mul (Pervasives.(!) %1) %2"
Mário Pereira's avatar
Mário Pereira committed
84 85
end

86 87 88 89 90 91 92 93 94
module null.Null

  syntax type t           "%1"
  syntax val  create_null "(fun () -> Obj.magic (ref 0))"
  syntax val  eq_null     "(==)"
  syntax val  create      "(fun x -> x)"
  syntax val  get         "(fun x -> x)"

end