ocaml-no-arith.drv 1.64 KB
Newer Older
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

(** Arithmetic-independent OCaml driver *)

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

theory option.Option
  syntax type     option "(%1 option)"
  syntax function None   "None"
  syntax function Some   "(Some %1)"
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
  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)"
end

(* list *)

theory list.List
  syntax type     list "%1 list"
  syntax function Nil  "[]"
  syntax function Cons "(%1 :: %2)"
end

theory list.Mem
  syntax predicate mem "(List.mem %1 %2)"
end

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

theory list.Reverse
  syntax function reverse "(List.rev %1)"
end

theory list.RevAppend
  syntax function rev_append "(List.rev_append %1 %2)"
end

theory list.Combine
  syntax function combine "(List.combine %1 %2)"
end

(* WhyML *)

module ref.Ref
  syntax type     ref      "(%1 Pervasives.ref)"
  syntax function contents "%1.Pervasives.contents"
  syntax val      ref      "Pervasives.ref"
  syntax val      (!_)     "Pervasives.(!)"
  syntax val      (:=)     "Pervasives.(:=)"
end

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