(** Arithmetic-independent OCaml driver *) (* FIXME 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 ref" syntax function contents "!%1" syntax val ref "ref %1" syntax val (!_) "!%1" syntax val (:=) "%1 := %2" end (* FIXME: once we extract ref.Refint, this module will no longer be useful in the driver *) module ref.Refint syntax val incr "%1 := Z.succ (Pervasives.(!) %1)" 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" 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