ocaml-no-arith.drv 1.64 KB
 Jean-Christophe Filliatre committed Apr 16, 2015 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 ``````