Commit 1cc1d001 authored by Andrei Paskevich's avatar Andrei Paskevich

hash-consing of labels

parent b3900e7b
......@@ -22,7 +22,26 @@ open Util
(** Labels *)
type label = string
type label = {
lab_string : string;
lab_tag : int;
}
module Hslab = Hashcons.Make (struct
type t = label
let equal lab1 lab2 = lab1.lab_string = lab2.lab_string
let hash lab = Hashtbl.hash lab.lab_string
let tag n lab = { lab with lab_tag = n }
end)
let create_label s = Hslab.hashcons {
lab_string = s;
lab_tag = -1
}
let lab_equal : label -> label -> bool = (==)
let lab_hash (lab : label) = lab.lab_tag
(** Identifiers *)
......
......@@ -23,7 +23,15 @@ open Stdlib
(** {2 Labels} *)
type label = string
type label = private {
lab_string : string;
lab_tag : int;
}
val lab_equal : label -> label -> bool
val lab_hash : label -> int
val create_label : string -> label
(** {2 Identifiers} *)
......
......@@ -186,7 +186,7 @@ let prio_binop = function
| Tiff -> 1
let print_label fmt l =
if l = "" then () else fprintf fmt "\"%s\"" l
fprintf fmt "\"%s\"" l.lab_string
let print_loc fmt l =
let (f,l,b,e) = Loc.get l in
......
......@@ -771,7 +771,7 @@ let t_or = t_binary Tor
let t_implies = t_binary Timplies
let t_iff = t_binary Tiff
let asym_label = "asym_split"
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)
......
......@@ -931,7 +931,7 @@ sident:
/* Misc */
label:
| STRING { Lstr $1 }
| STRING { Lstr (Ident.create_label $1) }
| POSITION { Lpos $1 }
;
......
......@@ -375,7 +375,8 @@ let term_at lab t =
t_app fs_at [t; t_var lab] t.t_ty
let wp_expl l f =
t_label ?loc:f.t_loc (("expl:"^l)::Split_goal.stop_split::f.t_label) f
let lab = Ident.create_label ("expl:"^l) in
t_label ?loc:f.t_loc (lab::Split_goal.stop_split::f.t_label) f
(* 0 <= phi0 and phi < phi0 *)
let default_variant le lt phi phi0 =
......@@ -459,7 +460,8 @@ 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 t1 = t_label ~loc:e1.expr_loc ["let"] (t_var v1) in
let ll = [Ident.create_label "let"] in
let t1 = t_label ~loc:e1.expr_loc ll (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)
......@@ -715,7 +717,8 @@ let add_wp_decl ps f uc =
(* prepare a proposition symbol *)
let name = ps.ps_pure.ls_name in
let s = "WP_" ^ name.id_string in
let label = ("expl:" ^ name.id_string) :: name.id_label in
let lab = Ident.create_label ("expl:" ^ name.id_string) in
let label = 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 *)
......
......@@ -357,7 +357,7 @@ let save_ident fmt id =
file lnum cnumb cnume
let save_label fmt s =
fprintf fmt "@\n@[<v 1><label@ name=\"%s\">@,</label>@]" s
fprintf fmt "@\n@[<v 1><label@ name=\"%s\">@,</label>@]" s.Ident.lab_string
let rec save_goal provers fmt g =
assert (g.goal_shape <> "");
......@@ -429,6 +429,7 @@ let expl_regexp = Str.regexp "expl:\\(.*\\)"
exception Found of string
let check_expl lab =
let lab = lab.Ident.lab_string in
if Str.string_match expl_regexp lab 0 then
raise (Found (Str.matched_group 1 lab))
......@@ -742,7 +743,9 @@ let load_ident elt =
let label = List.fold_left
(fun acc label ->
match label with
| {Xml.name = "label"} -> string_attribute "name" label::acc
| {Xml.name = "label"} ->
let lab = string_attribute "name" label in
Ident.create_label lab :: acc
| _ -> acc
) [] elt.Xml.elements in
let preid =
......
......@@ -152,8 +152,8 @@ let ls_of_const =
(* unprotected and unprotecting idents *)
let unprotected_label = "encoding : unprotected"
let unprotecting_label = "encoding : unprotecting"
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
......
......@@ -41,7 +41,7 @@ let split_case forig spl c acc tl bl =
apply_append fn acc bll
let asym_split = Term.asym_label
let stop_split = "stop_split"
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
......
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