Commit abeaa94b authored by MARCHE Claude's avatar MARCHE Claude

Ocaml realization of map.Map

parent 88a4d5b2
......@@ -1201,7 +1201,8 @@ clean::
OCAMLLIBS_FILES = why3__BigInt why3__BuiltIn why3__Prelude \
int__Int int__Abs int__ComputerDivision int__Lex2 int__MinMax \
ref__Refint ref__Ref array__Array
ref__Refint ref__Ref \
map__Map array__Array
OCAMLLIBS_MODULES := $(addprefix lib/ocaml/, $(OCAMLLIBS_FILES))
......@@ -1248,10 +1249,11 @@ lib/why3/why3extract.cmx: $(OCAMLLIBS_CMX)
$(OCAMLOPT) $(OFLAGS) -pack -o $@ $^
install_no_local::
mkdir -p $(LIBDIR)/why3/ocaml
cp lib/why3/why3extract.cma lib/why3/why3extract.cmxa $(LIBDIR)/why3/ocaml
install_no_local_lib::
mkdir -p $(OCAMLINSTALLLIB)/why3
cp -f lib/why3/why3extract.cm* lib/why3/why3extract.[ao] \
$(OCAMLINSTALLLIB)/why3
################
......
(* This file has been generated from Why3 theory Map *)
type ('a, 'b) map = (* inefficient implementation *)
{ default : 'b;
table : ('a * 'b) list;
}
let get (x: ('a, 'b) map) (x1: 'a) : 'b =
try
List.assoc x1 x.table
with Not_found -> x.default
let rec update l x y =
match l with
| [] -> [x,y]
| (z,_) as t :: r ->
if x = z then (z,y) :: r else t :: update r x y
let set (x: ('a, 'b) map) (x1: 'a) (x2: 'b) : ('a, 'b) map =
{ x with table = update x.table x1 x2 }
let mixfix_lbrb (a: ('a, 'b) map) (i: 'a) : 'b = get a i
let mixfix_lblsmnrb (a: ('a, 'b) map) (i: 'a) (v: 'b) : ('a, 'b) map =
set a i v
let const (x: 'b) : ('a, 'b) map =
{ default = x ; table = [] }
module BigInt = Why3__BigInt
type int = BigInt.t
type int = Why3__BigInt.t
let infix_eq = Pervasives.(=)
let int_constant = BigInt.of_string
let int_constant = Why3__BigInt.of_string
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