why3__Map.ml 740 Bytes
Newer Older
MARCHE Claude's avatar
MARCHE Claude committed
1

2 3 4 5
(* inefficient implementation of theory map.Map
   to be used in OCaml extracted code (see driver ocaml.drv) *)

type ('a, 'b) map =
MARCHE Claude's avatar
MARCHE Claude committed
6 7 8 9
  { default : 'b;
    table : ('a * 'b) list;
  }

10
let get (x: ('a, 'b) map) (x1: 'a) : 'b =
MARCHE Claude's avatar
MARCHE Claude committed
11
  try
12
    List.assoc x1 x.table
MARCHE Claude's avatar
MARCHE Claude committed
13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28
  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

29
let const (x: 'b) : ('a, 'b) map =
MARCHE Claude's avatar
MARCHE Claude committed
30 31 32
  { default = x ; table = [] }