ocaml.drv 1.58 KB
Newer Older
1

2
printer "ocaml"
3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21

theory BuiltIn
  syntax type       int   "Num.num"
  syntax predicate  (=)   "(%1 = %2)"
end

theory option.Option
  syntax type     option "(%1 option)"
  syntax function None   "None"
  syntax function Some   "(Some %1)"
end

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

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

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

theory int.Int
36 37
  (* TODO: make a for_num prelude function *)

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
  syntax function zero "(Num.num_of_int 0)"
  syntax function one  "(Num.num_of_int 1)"

  syntax function (+)  "(Num.add_num %1 %2)"
  syntax function (-)  "(Num.sub_num %1 %2)"
  syntax function (*)  "(Num.mult_num %1 %2)"
  syntax function (-_) "(Num.minus_num %1)"

  syntax predicate (<=) "(Num.le_num %1 %2)"
  syntax predicate (<)  "(Num.lt_num %1 %2)"
  syntax predicate (>=) "(Num.ge_num %1 %2)"
  syntax predicate (>)  "(Num.gt_num %1 %2)"
end

theory int.Abs
  syntax function abs "(Num.abs_num %1)"
end

theory int.MinMax
  syntax function min "(Num.min_num %1 %2)"
  syntax function max "(Num.max_num %1 %2)"
end

(* Note: documentation for Num says ``Euclidean division'' but this is
   rather a computer division *)
theory int.ComputerDivision
  syntax function div "(Num.quo_num %1 %2)"
  syntax function mod "(Num.mod_num %1 %2)"
end