extraction: fixed OCaml drivers

parent 967ad04e
......@@ -12,7 +12,7 @@ theory BuiltIn
syntax predicate (=) "(%1 = %2)"
end
import "ocaml-no-arith.drv"
(* import "ocaml-no-arith.drv" *)
(* int *)
......@@ -150,8 +150,7 @@ module mach.int.Int31
syntax val ( * ) "( * )"
syntax val ( / ) "( / )"
syntax val ( % ) "(mod)"
syntax val eq "(=)"
syntax val ne "(<>)"
syntax val (=) "(=)"
syntax val (<=) "(<=)"
syntax val (<) "(<)"
syntax val (>=) "(>=)"
......@@ -170,8 +169,7 @@ module mach.int.Int63
syntax val ( * ) "( * )"
syntax val ( / ) "( / )"
syntax val ( % ) "(mod)"
syntax val eq "(=)"
syntax val ne "(<>)"
syntax val (=) "(=)"
syntax val (<=) "(<=)"
syntax val (<) "(<)"
syntax val (>=) "(>=)"
......@@ -207,7 +205,7 @@ module mach.array.Array31
syntax val self_blit "Array.blit"
end
module mach.array.Array63
syntax type array63 "(%1 array)"
syntax type array "(%1 array)"
syntax val make "Array.make"
syntax val ([]) "Array.get"
......
......@@ -370,11 +370,11 @@ module mach.matrix.Matrix63
syntax function rows "Array.length %1"
syntax function columns "Array.length %1.(0)"
syntax val rows "Array.length %1"
syntax val columns "Array.length m.(0)"
syntax val get "m.(%1).(%2)"
syntax val set "m.(%1).(%2) <- %3"
syntax val defensive_get "m.(%1).(%2)"
syntax val defensive_set "m.(%1).(%2) <- %3"
syntax val columns "Array.length %1.(0)"
syntax val get "%1.(%2).(%3)"
syntax val set "%1.(%2).(%3) <- %4"
syntax val defensive_get "%1.(%2).(%3)"
syntax val defensive_set "%1.(%2).(%3) <- %4"
syntax val make "Array.make_matrix %1 %2 %3"
syntax val copy "Array.map Array.copy %1"
end
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment