Commit f82f1e54 authored by MARCHE Claude's avatar MARCHE Claude
Browse files

fix keeping of labels in WP + their printing in the IDE

parent 3e80f5ad
......@@ -3,9 +3,17 @@ module M1
use import int.Int
let f (x:int) : int =
let f (x "0":int) : int =
{ }
if x >= 42 then x + 3 else 0
{ result <= 50 }
use import module ref.Ref
let g (x "0": ref int) : int =
{ }
x := !x + 1;
if !x >= 42 then !x + 3 else 0
{ result <= 50 }
end
......@@ -3,7 +3,7 @@ theory T1
use import int.Int
goal G : forall x "0":int. ("cond" x >= 42) -> x + 3 <= 50
goal G : forall x "1":int. ("cond" x >= 42) -> x + 3 <= 50
end
......
......@@ -27,6 +27,27 @@
shape="ainfix &lt;=iainfix &gt;=V0c42ainfix +V0c3c0c50F">
<label
name="expl:parameter f"/>
<proof
prover="0"
timelimit="5"
memlimit="0"
edited="altmnergomnmodels-WP_M1-WP_parameter_f_1.why"
obsolete="false"
archived="false">
<result status="unknown" time="0.00"/>
</proof>
</goal>
<goal
name="WP_parameter g"
locfile="alt-ergo-models/../alt-ergo-models.mlw"
loclnum="13" loccnumb="6" loccnume="7"
expl="parameter g"
sum="044c6d04c9bbd10bd6ec37d09f41f130"
proved="false"
expanded="true"
shape="iainfix &gt;=V1c42ainfix &lt;=ainfix +V1c3c50ainfix &lt;=c0c50Iainfix =V1ainfix +V0c1FF">
<label
name="expl:parameter g"/>
<proof
prover="0"
timelimit="5"
......@@ -60,9 +81,10 @@
prover="0"
timelimit="5"
memlimit="0"
obsolete="false"
archived="false">
<result status="unknown" time="0.00"/>
edited="altmnergomnmodels-T1-G_1.why"
obsolete="true"
archived="false"><undone/>
</proof>
</goal>
</theory>
......
......@@ -53,14 +53,30 @@ let forget_all () =
forget_all tprinter;
forget_all pprinter
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 &&
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
(* type variables always start with a quote *)
let print_tv fmt tv =
fprintf fmt "'%s" (id_unique aprinter tv.tv_name)
(* logic variables always start with a lower case letter *)
let print_vs fmt vs =
let id = vs.vs_name in
let sanitizer = String.uncapitalize in
fprintf fmt "%s" (id_unique iprinter ~sanitizer vs.vs_name)
fprintf fmt "%s" (id_unique iprinter ~sanitizer id);
print_ident_labels fmt id
let forget_var vs = forget_id iprinter vs.vs_name
......@@ -186,19 +202,6 @@ let prio_binop = function
| Timplies -> 1
| Tiff -> 1
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 &&
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
let rec print_term fmt t = print_lterm 0 fmt t
......
......@@ -998,6 +998,15 @@ let rec purify_itype_v = function
(List.map (fun (v,_) -> v.i_impure.vs_ty) bl)
(purify_itype_v c.ic_result_type)
let label_set_from_list loc labels =
List.fold_left
(fun (labels,loc) lab ->
match lab with
| Lstr s -> (Ident.Slab.add s labels,loc)
| Lpos l -> (labels,l))
(Slab.empty,loc)
labels
let rec iutype_v env = function
| DUTpure ty ->
ITpure (Denv.ty_of_dty ty)
......@@ -1016,7 +1025,8 @@ and iutype_c env c =
and iubinder env (x, ty, tyv) =
let tyv = iutype_v env tyv in
let ty = Denv.ty_of_dty ty in
let env, v = iadd_local env (id_user x.id x.id_loc) ty in
let label, _ = label_set_from_list x.id_loc x.id_lab in
let env, v = iadd_local env (id_user ~label x.id x.id_loc) ty in
env, (v, tyv)
let mk_iexpr loc ty d =
......@@ -1943,15 +1953,6 @@ let add_effect_decl uc ls =
let add_impure_decl uc ls =
Pgm_module.add_impure_decl (Decl.create_param_decl ls) uc
let label_set_from_list loc labels =
List.fold_left
(fun (labels,loc) lab ->
match lab with
| Lstr s -> (Ident.Slab.add s labels,loc)
| Lpos l -> (labels,l))
(Slab.empty,loc)
labels
let add_global_fun loc ~labels x tyv uc =
let x = parameter x in
try
......
......@@ -102,7 +102,15 @@ let fresh_mark () =
create_vsymbol (id_fresh "mark") ty_mark
let wp_binder x f = match x.pv_tv with
| Tpure _ -> wp_forall x.pv_pure f
| Tpure _ ->
(*
let v = x.pv_pure in
let label = Slab.singleton (create_label "clone:bind") in
let id = id_clone ~label v.vs_name in
let v' = create_vsymbol id v.vs_ty in
wp_forall v' f
*)
wp_forall x.pv_pure f
| Tarrow _ -> f
let wp_binders = List.fold_right wp_binder
......@@ -234,7 +242,10 @@ let quantify env rm sreg f =
| Tyvar _ -> assert false
in
let id = Spv.fold test vars None in
let id = id_clone (def_option r.R.r_tv.tv_name id) in
(**)
let label = Slab.singleton (create_label "0") in
(**)
let id = id_clone ~label (def_option r.R.r_tv.tv_name id) in
let r' = create_vsymbol id (purify r.R.r_ty) in
Mtv.add r.R.r_tv r' m
in
......@@ -243,7 +254,10 @@ let quantify env rm sreg f =
let vv' =
let add pv s =
let v = pv.pv_pure in
let v' = create_vsymbol (id_clone v.vs_name) v.vs_ty in
(**)
let label = Slab.singleton (create_label "clone:quantify(2)") in
(**)
let v' = create_vsymbol (id_clone ~label v.vs_name) v.vs_ty in
Mvs.add v v' s
in
Spv.fold add vars Mvs.empty
......
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