Commit e0230d0e authored by Andrei Paskevich's avatar Andrei Paskevich

automatically generate projection functions for the named

constructor parameters : mainly useful for records, see 
examples/programs/vacid_0_sparse_array
parent 518ac666
......@@ -33,16 +33,14 @@ back +-+-+-+-------------------+
logic (#) (a : array 'a) (i : int) : 'a = A.select a i
type sparse_array = (array elt, array int, array int, int (*sz*), int (*n*))
logic sa_val (a : sparse_array) : array elt = let (v, _, _, _, _) = a in v
logic sa_idx (a : sparse_array) : array int = let (_, i, _, _, _) = a in i
logic sa_back(a : sparse_array) : array int = let (_, _, b, _, _) = a in b
logic sa_sz (a : sparse_array) : int = let (_, _, _, s, _) = a in s
logic sa_n (a : sparse_array) : int = let (_, _, _, _, n) = a in n
type sparse_array = SA (sa_val : array elt)
(sa_idx : array int)
(sa_back : array int)
(sa_sz : int)
(sa_n : int)
logic is_elt (a : sparse_array) (i : int) =
let (val, idx, back, _, n) = a in
let (SA val idx back _ n) = a in
0 <= idx#i < n and back#(idx#i) = i
logic model (a : sparse_array) (i : int) : elt =
......@@ -52,7 +50,7 @@ back +-+-+-+-------------------+
default
logic invariant (a : sparse_array) =
let (val, idx, back, sz, n) = a in
let (SA val idx back sz n) = a in
0 <= n <= sz <= maxlen and
forall i : int. 0 <= i < n -> 0 <= back#i < sz and idx#(back#i) = i
......@@ -79,7 +77,7 @@ back +-+-+-+-------------------+
lemma Inter6 :
forall a : sparse_array . invariant a ->
let (val, idx, back, sz, n) = a in
let (SA val idx back sz n) = a in
n = sz ->
permutation sz back and
forall i : int. 0 <= i < sz ->
......@@ -99,7 +97,7 @@ parameter malloc : n:int -> {} array 'a { A.length result = n }
let create sz =
{ 0 <= sz <= maxlen }
ref ((malloc sz, malloc sz, malloc sz, sz, 0) : sparse_array)
ref (SA (malloc sz) (malloc sz) (malloc sz) sz 0)
{ invariant !result and
sa_sz !result = sz and forall i:int. model !result i = default }
......@@ -147,12 +145,12 @@ let set a i v =
let n = sa_n !a in
let val = A.store val i v in
if test a i then
a := (val, idx, back, sz, n)
a := SA val idx back sz n
else begin
assert { n < sz };
let idx = A.store idx i n in
let back = A.store back n i in
a := (val, idx, back, sz, n+1)
a := SA val idx back sz (n+1)
end
{ invariant !a and
sa_sz !a = sa_sz (old !a) and
......
......@@ -7,18 +7,13 @@
logic (#) (a : array 'a) (i : int) : 'a = A.select a i
type uf = ((* link: *) array int,
(* dist: *) array int, (* distance to representative *)
(* size: *) int,
(* num : *) int)
logic link (u : uf) : array int = let (l, _, _, _) = u in l
logic dist (u : uf) : array int = let (_, d, _, _) = u in d
logic size (u : uf) : int = let (_, _, s, _) = u in s
logic num (u : uf) : int = let (_, _, _, n) = u in n
type uf = UF (link : array int)
(dist : array int) (* distance to representative *)
(size : int)
(num : int)
logic inv (u : uf) =
let (l, d, s, n) = u in
let (UF l d s n) = u in
(forall i:int. 0 <= i < s -> 0 <= l#i < s) and
(forall i:int. 0 <= i < s ->
(d#i = 0 and l#i = i or d#i > 0 and d#(l#i) = d#i - 1))
......@@ -51,7 +46,7 @@ let create (n:int) =
i := !i + 1
done;
ref ((!l, A.const_length 0 n, n, n))
ref (UF !l (A.const_length 0 n) n n)
{ inv !result and
num !result = n and size !result = n and
forall x:int. 0 <= x < n -> repr !result x = x }
......@@ -100,7 +95,7 @@ let union (u:ref uf) (a b:int) =
let rb = find u b in
let l = link !u in
let d = increment u ra in
u := (A.store l ra rb, d, size !u, num !u - 1)
u := UF (A.store l ra rb) d (size !u) (num !u - 1)
{ inv !u and
same !u a b and
size !u = size (old !u) and num !u = num (old !u) - 1 and
......
......@@ -396,9 +396,9 @@ let do_input env drv = function
Queue.iter (do_local_theory drv fname m) tlist
with
| Loc.Located (loc, e) ->
eprintf "%a%a@." Loc.report_position loc report e; exit 1
eprintf "@[%a%a@]@." Loc.report_position loc report e; exit 1
| e ->
eprintf "%a@." report e; exit 1
eprintf "@[%a@]@." report e; exit 1
let () =
try
......
......@@ -544,6 +544,51 @@ and dtype_args s loc env el tl =
in
check_arg (el, tl)
(** Add projection functions for the algebraic types *)
let add_projection cl p (fs,tyarg,tyval) th =
let vs = create_vsymbol (id_fresh p) tyval in
let per_cs (_,id,pl) =
let cs = find_lsymbol (Qident id) th in
let tc = match cs.ls_value with
| None -> assert false
| Some t -> t
in
let m = ty_match Mtv.empty tc tyarg in
let per_param ty (n,_) = match n with
| Some id when id.id = p -> pat_var vs
| _ -> pat_wild (ty_inst m ty)
in
let al = List.map2 per_param cs.ls_args pl in
[pat_app cs al tyarg], t_var vs
in
let vs = create_vsymbol (id_fresh "u") tyarg in
let t = t_case [t_var vs] (List.map per_cs cl) tyval in
let d = make_fs_defn fs [vs] t in
add_logic_decl th [d]
let add_projections th d = match d.td_def with
| TDabstract | TDalias _ -> th
| TDalgebraic cl ->
let per_cs acc (_,id,pl) =
let cs = find_lsymbol (Qident id) th in
let tc = match cs.ls_value with
| None -> assert false
| Some t -> t
in
let per_param acc ty (n,_) = match n with
| Some id when not (Mstr.mem id.id acc) ->
let fn = id_user id.id id.id_loc in
let fs = create_fsymbol fn [tc] ty in
Mstr.add id.id (fs,tc,ty) acc
| _ -> acc
in
List.fold_left2 per_param acc cs.ls_args pl
in
let ps = List.fold_left per_cs Mstr.empty cl in
try Mstr.fold (add_projection cl) ps th
with e -> raise (Loc.Located (d.td_loc, e))
(** Typing declarations, that is building environments. *)
open Ptree
......@@ -643,8 +688,10 @@ let add_types dl th =
in
ts, d
in
try add_ty_decls th (List.map decl dl)
with ClashSymbol s -> error ~loc:(Hashtbl.find csymbols s) (Clash s)
let th = try add_ty_decls th (List.map decl dl)
with ClashSymbol s -> error ~loc:(Hashtbl.find csymbols s) (Clash s)
in
List.fold_left add_projections th dl
let env_of_vsymbol_list vl =
List.fold_left (fun env v -> Mstr.add v.vs_name.id_string v env) Mstr.empty vl
......
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