Commit f80668a1 authored by Andrei Paskevich's avatar Andrei Paskevich

t_label_copy merges the labels

Thanks to Johannes Kanig for this useful suggestion.
parent 1cc1d001
......@@ -27,6 +27,14 @@ type label = {
lab_tag : int;
}
module Lab = StructMake (struct
type t = label
let tag lab = lab.lab_tag
end)
module Slab = Lab.S
module Mlab = Lab.M
module Hslab = Hashcons.Make (struct
type t = label
let equal lab1 lab2 = lab1.lab_string = lab2.lab_string
......@@ -47,7 +55,7 @@ let lab_hash (lab : label) = lab.lab_tag
type ident = {
id_string : string; (* non-unique name *)
id_label : label list; (* identifier labels *)
id_label : Slab.t; (* identifier labels *)
id_loc : Loc.position option; (* optional location *)
id_tag : Hashweak.tag; (* unique magical tag *)
}
......@@ -79,17 +87,19 @@ let create_ident name labels loc = {
id_tag = Hashweak.dummy_tag;
}
let id_fresh ?(label = []) ?loc nm =
let id_fresh ?(label = Slab.empty) ?loc nm =
create_ident nm label loc
let id_user ?(label = []) nm loc =
let id_user ?(label = Slab.empty) nm loc =
create_ident nm label (Some loc)
let id_clone ?(label = []) id =
create_ident id.id_string (label @ id.id_label) id.id_loc
let id_clone ?(label = Slab.empty) id =
let ll = Slab.union label id.id_label in
create_ident id.id_string ll id.id_loc
let id_derive ?(label = []) nm id =
create_ident nm (label @ id.id_label) id.id_loc
let id_derive ?(label = Slab.empty) nm id =
let ll = Slab.union label id.id_label in
create_ident nm ll id.id_loc
(** Unique names for pretty printing *)
......
......@@ -28,6 +28,9 @@ type label = private {
lab_tag : int;
}
module Mlab : Map.S with type key = label
module Slab : Mlab.Set
val lab_equal : label -> label -> bool
val lab_hash : label -> int
......@@ -37,7 +40,7 @@ val create_label : string -> label
type ident = private {
id_string : string; (* non-unique name *)
id_label : label list; (* identifier labels *)
id_label : Slab.t; (* identifier labels *)
id_loc : Loc.position option; (* optional location *)
id_tag : Hashweak.tag; (* unique magical tag *)
}
......@@ -57,16 +60,16 @@ type preid
val id_register : preid -> ident
(* create a fresh pre-ident *)
val id_fresh : ?label:(label list) -> ?loc:Loc.position -> string -> preid
val id_fresh : ?label:Slab.t -> ?loc:Loc.position -> string -> preid
(* create a localized pre-ident *)
val id_user : ?label:(label list) -> string -> Loc.position -> preid
val id_user : ?label:Slab.t -> string -> Loc.position -> preid
(* create a duplicate pre-ident *)
val id_clone : ?label:(label list) -> ident -> preid
val id_clone : ?label:Slab.t -> ident -> preid
(* create a derived pre-ident (inherit labels and location) *)
val id_derive : ?label:(label list) -> string -> ident -> preid
val id_derive : ?label:Slab.t -> string -> ident -> preid
(** Unique persistent names for pretty printing *)
......
......@@ -188,13 +188,16 @@ let prio_binop = function
let print_label fmt l =
fprintf fmt "\"%s\"" l.lab_string
let print_labels = print_iter1 Slab.iter space print_label
let print_loc fmt l =
let (f,l,b,e) = Loc.get l in
fprintf fmt "#\"%s\" %d %d %d#" f l b e
let print_ident_labels fmt id =
if Debug.test_flag debug_print_labels && id.id_label <> [] then
fprintf fmt "@ %a" (print_list space print_label) id.id_label;
if Debug.test_flag debug_print_labels &&
not (Slab.is_empty id.id_label) then
fprintf fmt "@ %a" print_labels id.id_label;
if Debug.test_flag debug_print_locs then
Util.option_iter (fprintf fmt "@ %a" print_loc) id.id_loc
......@@ -202,9 +205,9 @@ let rec print_term fmt t = print_lterm 0 fmt t
and print_lterm pri fmt t =
let print_tlab pri fmt t =
if Debug.test_flag debug_print_labels && t.t_label <> []
if Debug.test_flag debug_print_labels && not (Slab.is_empty t.t_label)
then fprintf fmt (protect_on (pri > 0) "@[<hov 0>%a@ %a@]")
(print_list space print_label) t.t_label (print_tnode 0) t
print_labels t.t_label (print_tnode 0) t
else print_tnode pri fmt t in
let print_tloc pri fmt t =
if Debug.test_flag debug_print_locs && t.t_loc <> None
......@@ -273,7 +276,7 @@ and print_tnode pri fmt t = match t.t_node with
| Tfalse ->
fprintf fmt "false"
| Tbinop (b,f1,f2) ->
let asym = List.mem Term.asym_label t.t_label in
let asym = Slab.mem Term.asym_label t.t_label in
let p = prio_binop b in
fprintf fmt (protect_on (pri > p) "@[<hov 1>%a %a@ %a@]")
(print_lterm (p + 1)) f1 (print_binop ~asym) b (print_lterm p) f2
......
......@@ -272,7 +272,7 @@ type constant =
type term = {
t_node : term_node;
t_ty : ty option;
t_label : label list;
t_label : Slab.t;
t_loc : Loc.position option;
t_vars : int Mvs.t;
t_tag : int;
......@@ -397,7 +397,7 @@ module Hsterm = Hashcons.Make (struct
let equal t1 t2 =
oty_equal t1.t_ty t2.t_ty &&
t_equal_node t1.t_node t2.t_node &&
list_all2 (=) t1.t_label t2.t_label &&
Slab.equal t1.t_label t2.t_label &&
option_eq Loc.equal t1.t_loc t2.t_loc
let t_hash_bound (v,b,t) =
......@@ -427,9 +427,10 @@ module Hsterm = Hashcons.Make (struct
| Tfalse -> 1
let hash t =
let comb l = Hashcons.combine (lab_hash l) in
Hashcons.combine2 (t_hash_node t.t_node)
(Hashcons.combine_option Loc.hash t.t_loc)
(Hashcons.combine_list Hashtbl.hash (oty_hash t.t_ty) t.t_label)
(Slab.fold comb t.t_label (oty_hash t.t_ty))
let t_vars_node = function
| Tvar v -> Mvs.singleton v 1
......@@ -461,7 +462,7 @@ module Hterm = Term.H
let mk_term n ty = Hsterm.hashcons {
t_node = n;
t_label = [];
t_label = Slab.empty;
t_loc = None;
t_vars = Mvs.empty;
t_ty = ty;
......@@ -483,12 +484,16 @@ let t_not f = mk_term (Tnot f) None
let t_true = mk_term (Ttrue) None
let t_false = mk_term (Tfalse) None
let t_label ?loc l t = Hsterm.hashcons { t with t_label = l; t_loc = loc }
let t_label_add l t = Hsterm.hashcons { t with t_label = l :: t.t_label }
let t_label ?loc l t =
Hsterm.hashcons { t with t_label = l; t_loc = loc }
let t_label_copy { t_label = l; t_loc = p } t =
if t.t_label = [] && t.t_loc = None && (l <> [] || p <> None)
then t_label ?loc:p l t else t
let t_label_add l t =
Hsterm.hashcons { t with t_label = Slab.add l t.t_label }
let t_label_copy { t_label = lab; t_loc = loc } t =
let lab = Slab.union lab t.t_label in
let loc = if t.t_loc = None then loc else t.t_loc in
Hsterm.hashcons { t with t_label = lab; t_loc = loc }
(* unsafe map *)
......@@ -772,8 +777,10 @@ let t_implies = t_binary Timplies
let t_iff = t_binary Tiff
let asym_label = create_label "asym_split"
let t_and_asym t1 t2 = t_label [asym_label] (t_and t1 t2)
let t_or_asym t1 t2 = t_label [asym_label] (t_or t1 t2)
let asym_labels = Slab.singleton asym_label
let t_and_asym t1 t2 = t_label asym_labels (t_and t1 t2)
let t_or_asym t1 t2 = t_label asym_labels (t_or t1 t2)
(* closing constructors *)
......
......@@ -133,7 +133,7 @@ type constant =
type term = private {
t_node : term_node;
t_ty : ty option;
t_label : label list;
t_label : Slab.t;
t_loc : Loc.position option;
t_vars : int Mvs.t;
t_tag : int;
......@@ -246,7 +246,7 @@ val t_quant_close : quant -> vsymbol list -> trigger -> term -> term
val t_forall_close : vsymbol list -> trigger -> term -> term
val t_exists_close : vsymbol list -> trigger -> term -> term
val t_label : ?loc:Loc.position -> label list -> term -> term
val t_label : ?loc:Loc.position -> Slab.t -> term -> term
val t_label_add : label -> term -> term
val t_label_copy : term -> term -> term
......
......@@ -142,10 +142,10 @@ and dpattern_node =
let create_user_id { id = x ; id_lab = ll ; id_loc = loc } =
let get_labels (ll,p) = function
| Lstr l -> l::ll, p
| Lstr l -> Slab.add l ll, p
| Lpos p -> ll, Some p
in
let label,p = List.fold_left get_labels ([],None) ll in
let label,p = List.fold_left get_labels (Slab.empty,None) ll in
id_user ~label x (default_option loc p)
let create_user_vs id ty = create_vsymbol (create_user_id id) ty
......@@ -226,11 +226,11 @@ let rec term env t = match t.dt_node with
t_case (term env t1) (List.map branch bl)
| Tnamed _ ->
let rec collect p ll e = match e.dt_node with
| Tnamed (Lstr l, e) -> collect p (l::ll) e
| Tnamed (Lstr l, e) -> collect p (Slab.add l ll) e
| Tnamed (Lpos p, e) -> collect (Some p) ll e
| _ -> t_label ?loc:p (List.rev ll) (term env e)
| _ -> t_label ?loc:p ll (term env e)
in
collect None [] t
collect None Slab.empty t
| Teps (id, ty, e1) ->
let v = create_user_vs id (ty_of_dty ty) in
let env = Mstr.add id.id v env in
......@@ -275,11 +275,11 @@ and fmla env = function
t_case (term env t) (List.map branch bl)
| (Fnamed _) as f ->
let rec collect p ll = function
| Fnamed (Lstr l, e) -> collect p (l::ll) e
| Fnamed (Lstr l, e) -> collect p (Slab.add l ll) e
| Fnamed (Lpos p, e) -> collect (Some p) ll e
| e -> t_label ?loc:p (List.rev ll) (fmla env e)
| e -> t_label ?loc:p ll (fmla env e)
in
collect None [] f
collect None Slab.empty f
| Fvar f ->
f
......
......@@ -157,17 +157,18 @@ let prio_binop = function
| Tiff -> 1
let print_label = Pretty.print_label
let print_labels = print_iter1 Slab.iter space print_label
let print_ident_labels fmt id =
if id.id_label <> [] then
fprintf fmt "@ %a" (print_list space print_label) id.id_label
if not (Slab.is_empty id.id_label) then
fprintf fmt "@ %a" print_labels id.id_label
let rec print_term fmt t = print_lterm 0 fmt t
and print_lterm pri fmt t = match t.t_label with
| [] -> print_tnode pri fmt t
| ll -> fprintf fmt (protect_on (pri > 0) "%a %a")
(print_list space print_label) ll (print_tnode 0) t
and print_lterm pri fmt t =
if Slab.is_empty t.t_label then print_tnode pri fmt t
else fprintf fmt (protect_on (pri > 0) "%a %a")
print_labels t.t_label (print_tnode 0) t
and print_app pri fs fmt tl =
match query_syntax fs.ls_name with
......@@ -214,7 +215,7 @@ and print_tnode pri fmt t = match t.t_node with
| Tfalse ->
fprintf fmt "false"
| Tbinop (b,f1,f2) ->
let asym = List.mem Term.asym_label t.t_label in
let asym = Slab.mem Term.asym_label t.t_label in
let p = prio_binop b in
fprintf fmt (protect_on (pri > p) "%a %a@ %a")
(print_lterm (p + 1)) f1 (print_binop ~asym) b (print_lterm p) f2
......
......@@ -1937,9 +1937,9 @@ let add_global_fun loc ~labels x tyv uc =
List.fold_left
(fun (labels,loc) lab ->
match lab with
| Lstr s -> (s::labels,loc)
| Lstr s -> (Ident.Slab.add s labels,loc)
| Lpos l -> (labels,l))
([],loc)
(Slab.empty,loc)
labels
in
let ls, ps = create_psymbol_fun (id_user ~label x loc) tyv in
......
......@@ -57,7 +57,7 @@ let get_mutable_field ts i =
let wp_label e f =
let loc = if f.t_loc = None then Some e.expr_loc else f.t_loc in
let lab = e.expr_lab @ f.t_label in
let lab = List.fold_right Ident.Slab.add e.expr_lab f.t_label in
t_label ?loc lab f
let wp_and ?(sym=false) f1 f2 =
......@@ -375,8 +375,9 @@ let term_at lab t =
t_app fs_at [t; t_var lab] t.t_ty
let wp_expl l f =
let lab = Ident.create_label ("expl:"^l) in
t_label ?loc:f.t_loc (lab::Split_goal.stop_split::f.t_label) f
let lab = Slab.add Split_goal.stop_split f.t_label in
let lab = Slab.add (Ident.create_label ("expl:" ^ l)) lab in
t_label ?loc:f.t_loc lab f
(* 0 <= phi0 and phi < phi0 *)
let default_variant le lt phi phi0 =
......@@ -460,8 +461,10 @@ and wp_desc env rm e q = match e.expr_desc with
wp_expr env rm e2 (filter_post e2.expr_effect q)
in
let v1 = v_result x.pv_pure.vs_ty in
let ll = [Ident.create_label "let"] in
let t1 = t_label ~loc:e1.expr_loc ll (t_var v1) in
(* (* FIXME? Why do we need this label? *)
let ll = Slab.singleton (Ident.create_label "let") in
let t1 = t_label ~loc:e1.expr_loc ll (t_var v1) in *)
let t1 = t_label ~loc:e1.expr_loc Slab.empty (t_var v1) in
let q1 = v1, t_subst_single x.pv_pure t1 w2 in
let q1 = saturate_post e1.expr_effect q1 q in
wp_label e (wp_expr env rm e1 q1)
......@@ -617,8 +620,8 @@ and wp_desc env rm e q = match e.expr_desc with
| Eany c ->
(* TODO: propagate call labels into c.c_post *)
let w = opaque_wp env rm c.c_effect.E.writes c.c_post q in
let p = wp_expl "precondition" c.c_pre in
let p = t_label ~loc:e.expr_loc (p.t_label @ e.expr_lab) p in
let p = wp_label e (wp_expl "precondition" c.c_pre) in
let p = t_label ~loc:e.expr_loc p.t_label p in
wp_and p w
and wp_triple env rm bl (p, e, q) =
......@@ -626,8 +629,7 @@ and wp_triple env rm bl (p, e, q) =
let q =
let (v, q), l = q in
(v, wp_expl "normal postcondition" q),
List.map (fun (e, (v, q)) ->
e, (v, wp_expl "exceptional postcondition" q)) l
List.map (fun (e,(v,q)) -> e,(v,wp_expl "exceptional postcondition" q)) l
in
let f = wp_expr env rm e q in
let f = wp_implies p f in
......@@ -718,7 +720,7 @@ let add_wp_decl ps f uc =
let name = ps.ps_pure.ls_name in
let s = "WP_" ^ name.id_string in
let lab = Ident.create_label ("expl:" ^ name.id_string) in
let label = lab :: name.id_label in
let label = Slab.add lab name.id_label in
let id = id_fresh ~label ?loc:name.id_loc s in
let pr = create_prsymbol id in
(* prepare the VC formula *)
......
......@@ -368,7 +368,7 @@ expanded=\"%b\"@ shape=\"%s\">"
(opt "expl") g.goal_expl
g.goal_checksum g.goal_verified g.goal_expanded
g.goal_shape;
List.iter (save_label fmt) g.goal_name.Ident.id_label;
Ident.Slab.iter (save_label fmt) g.goal_name.Ident.id_label;
PHprover.iter (save_proof_attempt provers fmt) g.goal_external_proofs;
PHstr.iter (save_trans provers fmt) g.goal_transformations;
fprintf fmt "@]@\n</goal>"
......@@ -384,7 +384,7 @@ let save_theory provers fmt t =
"@\n@[<v 1><theory@ %a@ verified=\"%b\"@ expanded=\"%b\">"
save_ident t.theory_name
t.theory_verified t.theory_expanded;
List.iter (save_label fmt) t.theory_name.Ident.id_label;
Ident.Slab.iter (save_label fmt) t.theory_name.Ident.id_label;
List.iter (save_goal provers fmt) t.theory_goals;
fprintf fmt "@]@\n</theory>"
......@@ -434,7 +434,7 @@ let check_expl lab =
raise (Found (Str.matched_group 1 lab))
let rec get_expl_fmla f =
List.iter check_expl (List.rev f.Term.t_label);
Ident.Slab.iter check_expl f.Term.t_label;
(match f.Term.t_node with
| Term.Tbinop(Term.Timplies,_,f) -> get_expl_fmla f
| Term.Tquant(Term.Tforall,fq) ->
......@@ -451,7 +451,7 @@ let get_explanation id task =
let fmla = Task.task_goal_fmla task in
try
get_expl_fmla fmla;
List.iter check_expl (List.rev id.Ident.id_label);
Ident.Slab.iter check_expl id.Ident.id_label;
None
with Found e -> Some e
......@@ -745,9 +745,9 @@ let load_ident elt =
match label with
| {Xml.name = "label"} ->
let lab = string_attribute "name" label in
Ident.create_label lab :: acc
Ident.Slab.add (Ident.create_label lab) acc
| _ -> acc
) [] elt.Xml.elements in
) Ident.Slab.empty elt.Xml.elements in
let preid =
try
let load_exn attr g = List.assoc attr g.Xml.attributes in
......@@ -1309,7 +1309,7 @@ let associate_subgoals gname (old_goals : 'a goal list) new_goals =
(fun g -> Hashtbl.add old_goals_map g.goal_checksum g)
old_goals;
(*
we make an array of new goals with their numbers and checksums
we make an array of new goals with their numbers and checksums
*)
let new_goals_array =
array_map_list
......@@ -1378,7 +1378,7 @@ let associate_subgoals gname (old_goals : 'a goal list) new_goals =
match pairing_array.(i) with
| Some _ -> acc
| None ->
let shape =
let shape =
Termcode.t_shape_buf (Task.task_goal_fmla g)
in
shape_array.(i) <- shape;
......@@ -1387,7 +1387,7 @@ let associate_subgoals gname (old_goals : 'a goal list) new_goals =
new_goals_array
in
let sort_by_shape =
List.sort (fun (s1,_) (s2,_) -> String.compare s1 s2)
List.sort (fun (s1,_) (s2,_) -> String.compare s1 s2)
all_goals_without_pairing
in
(*
......
......@@ -67,10 +67,6 @@ let rec add_quant kn (vl,tl,f) v =
| _ ->
(v::vl, tl, f)
let t_label_merge { t_label = l; t_loc = p } t =
let p = if t.t_loc = None then p else t.t_loc in
t_label ?loc:p (l @ t.t_label) t
let eval_match ~inline kn t =
let rec eval env t = match t.t_node with
| Tapp (ls, tl) when inline kn ls (List.map t_type tl) t.t_ty ->
......@@ -78,17 +74,17 @@ let eval_match ~inline kn t =
| None ->
t_map (eval env) t
| Some def ->
t_label_merge t (eval env (unfold def tl t.t_ty))
eval env (unfold def tl t.t_ty)
end
| Tlet (t1, tb2) ->
let t1 = eval env t1 in
let x, t2, close = t_open_bound_cb tb2 in
let t2 = eval (Mvs.add x t1 env) t2 in
t_label_merge t (t_let_simp t1 (close x t2))
t_let_simp t1 (close x t2)
| Tcase (t1, bl1) ->
let t1 = eval env t1 in
let t1flat = dive env t1 in
let r = try match t1flat.t_node with
begin try match t1flat.t_node with
| Tapp (ls,_) when is_constructor kn ls ->
eval env (make_flat_case kn t1flat bl1)
| Tcase (t2, bl2) ->
......@@ -108,24 +104,20 @@ let eval_match ~inline kn t =
close p (eval env t)
in
t_case t1 (List.map mk_b bl1)
in
t_label_merge t r
end
| Tquant (q, qf) ->
let vl,tl,f,close = t_open_quant_cb qf in
let vl,tl,f = List.fold_left (add_quant kn) ([],tl,f) vl in
t_label_merge t (t_quant_simp q (close (List.rev vl) tl (eval env f)))
t_quant_simp q (close (List.rev vl) tl (eval env f))
| _ ->
t_map_simp (eval env) t
in
eval Mvs.empty t
t_label_copy t (eval Mvs.empty t)
let rec linear vars t = match t.t_node with
| Tvar x when Svs.mem x vars ->
raise Exit
| Tvar x ->
Svs.add x vars
| _ ->
t_fold linear vars t
| Tvar x when Svs.mem x vars -> raise Exit
| Tvar x -> Svs.add x vars
| _ -> t_fold linear vars t
let linear t =
try ignore (linear Svs.empty t); true with Exit -> false
......
......@@ -155,11 +155,11 @@ let ls_of_const =
let unprotected_label = Ident.create_label "encoding : unprotected"
let unprotecting_label = Ident.create_label "encoding : unprotecting"
let id_unprotected n = id_fresh ~label:[unprotected_label] n
let id_unprotecting n = id_fresh ~label:[unprotecting_label] n
let id_unprotected n = id_fresh ~label:(Slab.singleton unprotected_label) n
let id_unprotecting n = id_fresh ~label:(Slab.singleton unprotecting_label) n
let is_protected_id id = not (List.mem unprotected_label id.id_label)
let is_protecting_id id = not (List.mem unprotecting_label id.id_label)
let is_protected_id id = not (Slab.mem unprotected_label id.id_label)
let is_protecting_id id = not (Slab.mem unprotecting_label id.id_label)
let is_protected_vs kept vs =
is_protected_id vs.vs_name && Sty.mem vs.vs_ty kept
......
......@@ -43,12 +43,11 @@ let split_case forig spl c acc tl bl =
let asym_split = Term.asym_label
let stop_split = Ident.create_label "stop_split"
let asym f = List.mem asym_split f.t_label
let stop f = List.mem stop_split f.t_label
let asym f = Slab.mem asym_split f.t_label
let stop f = Slab.mem stop_split f.t_label
let unstop f =
let ll = List.filter ((<>) stop_split) f.t_label in
t_label ?loc:f.t_loc ll f
t_label ?loc:f.t_loc (Slab.remove stop_split f.t_label) f
let rec split_pos ro acc f = match f.t_node with
| _ when ro && stop f -> unstop f :: acc
......
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