Commit f530689a authored by Andrei Paskevich's avatar Andrei Paskevich

store locations in term/formulas, not in labels

- the new syntax for localisation "labels" in Why is as follows:

    goal Toto #"file" line bchar echar#     - after an ident
    #"file" line bchar echar" (A and B)     - before a term/fmla

- the new syntax for buffer relocation is as follows:

    ##"file" line char##
parent b8823b2e
......@@ -22,9 +22,7 @@ open Util
(** Labels *)
type label = string * Loc.position option
let label ?loc s = (s,loc)
type label = string
(** Identifiers *)
......@@ -68,21 +66,7 @@ let create_ident name origin labels = {
}
let id_fresh ?(labels = []) nm = create_ident nm Fresh labels
let id_user ?(labels = []) nm loc =
let new_loc = ref loc in
let new_labels = List.fold_left
(fun acc ((s,l) as lab) ->
match l with
| None -> lab :: acc
| Some loc ->
new_loc := loc;
match s with
| "" -> acc
| _ -> lab :: acc)
[] labels
in
create_ident nm (User !new_loc) new_labels
let id_user ?(labels = []) nm loc = create_ident nm (User loc) labels
let id_derive ?(labels = []) nm id = create_ident nm (Derived id) labels
let id_clone ?(labels = []) id =
......
......@@ -23,9 +23,7 @@ open Stdlib
(** {2 Labels} *)
type label = string * Loc.position option
val label : ?loc:Loc.position -> string -> label
type label = string
(** {2 Identifiers} *)
......
......@@ -184,7 +184,7 @@ let prio_binop = function
| Fimplies -> 1
| Fiff -> 1
let print_label fmt (l,_) =
let print_label fmt l =
if l = "" then () else fprintf fmt "\"%s\"" l
let print_ident_labels fmt id =
......
......@@ -272,6 +272,7 @@ type constant =
type term = {
t_node : term_node;
t_label : label list;
t_loc : Loc.position option;
t_vars : Svs.t;
t_ty : ty;
t_tag : int;
......@@ -280,6 +281,7 @@ type term = {
and fmla = {
f_node : fmla_node;
f_label : label list;
f_loc : Loc.position option;
f_vars : Svs.t;
f_tag : int;
}
......@@ -547,6 +549,7 @@ module Hfmla = Fmla.H
let mk_term n ty = Hsterm.hashcons {
t_node = n;
t_label = [];
t_loc = None;
t_vars = Svs.empty;
t_ty = ty;
t_tag = -1
......@@ -562,17 +565,19 @@ let t_let t1 bt ty = mk_term (Tlet (t1, bt)) ty
let t_case t1 bl ty = mk_term (Tcase (t1, bl)) ty
let t_eps bf ty = mk_term (Teps bf) ty
let t_label l t = Hsterm.hashcons { t with t_label = l }
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_add l t = Hsterm.hashcons { t with t_label = l :: t.t_label }
let t_label_copy { t_label = l } t =
if t.t_label = [] && l <> [] then t_label l t else t
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
(* hash-consing constructors for formulas *)
let mk_fmla n = Hsfmla.hashcons {
f_node = n;
f_label = [];
f_loc = None;
f_vars = Svs.empty;
f_tag = -1
}
......@@ -587,11 +592,12 @@ let f_if f1 f2 f3 = mk_fmla (Fif (f1, f2, f3))
let f_let t bf = mk_fmla (Flet (t, bf))
let f_case t bl = mk_fmla (Fcase (t, bl))
let f_label l f = Hsfmla.hashcons { f with f_label = l }
let f_label_add l f = Hsfmla.hashcons { f with f_label = l :: f.f_label }
let f_label ?loc l f = Hsfmla.hashcons { f with f_label = l; f_loc = loc }
let f_label_add l f = Hsfmla.hashcons { f with f_label = l :: f.f_label }
let f_label_copy { f_label = l } f =
if f.f_label = [] && l <> [] then f_label l f else f
let f_label_copy { f_label = l; f_loc = p } f =
if f.f_label = [] && f.f_loc = None && (l <> [] || p <> None)
then f_label ?loc:p l f else f
let f_and = f_binary Fand
let f_or = f_binary For
......
......@@ -129,6 +129,7 @@ type constant =
type term = private {
t_node : term_node;
t_label : label list;
t_loc : Loc.position option;
t_vars : Svs.t;
t_ty : ty;
t_tag : int;
......@@ -137,6 +138,7 @@ type term = private {
and fmla = private {
f_node : fmla_node;
f_label : label list;
f_loc : Loc.position option;
f_vars : Svs.t;
f_tag : int;
}
......@@ -258,7 +260,7 @@ val t_eps_close : vsymbol -> fmla -> term
val t_app_infer : lsymbol -> term list -> term
val t_label : label list -> term -> term
val t_label : ?loc:Loc.position -> label list -> term -> term
val t_label_add : label -> term -> term
val t_label_copy : term -> term -> term
......@@ -285,7 +287,7 @@ val f_quant_close : quant -> vsymbol list -> trigger list -> fmla -> fmla
val f_forall_close : vsymbol list -> trigger list -> fmla -> fmla
val f_exists_close : vsymbol list -> trigger list -> fmla -> fmla
val f_label : label list -> fmla -> fmla
val f_label : ?loc:Loc.position -> label list -> fmla -> fmla
val f_label_add : label -> fmla -> fmla
val f_label_copy : fmla -> fmla -> fmla
......
......@@ -536,7 +536,7 @@ let info_window ?(callback=(fun () -> ())) mt s =
let get_explanation id =
let r = ref None in
List.iter
(fun (s,_) ->
(fun s ->
if Str.string_match expl_regexp s 0 then
r := Some (Str.matched_group 1 s))
id.Ident.id_label;
......@@ -1798,21 +1798,17 @@ let scroll_to_id id =
"Derived ident (no position available)\n";
set_current_file ""
let color_label = function
| _, Some loc ->
let f, l, b, e = Loc.get loc in
if f = !current_file then
color_loc source_view l b e
| _ ->
()
let color_loc loc =
let f, l, b, e = Loc.get loc in
if f = !current_file then color_loc source_view l b e
let rec color_f_labels () f =
List.iter color_label f.Term.f_label;
Term.f_fold color_t_labels color_f_labels () f
let rec color_f_locs () f =
Util.option_iter color_loc f.Term.f_loc;
Term.f_fold color_t_locs color_f_locs () f
and color_t_labels () t =
List.iter color_label t.Term.t_label;
Term.t_fold color_t_labels color_f_labels () t
and color_t_locs () t =
Util.option_iter color_loc t.Term.t_loc;
Term.t_fold color_t_locs color_f_locs () t
let scroll_to_source_goal g =
let t = g.Model.task in
......@@ -1823,7 +1819,7 @@ let scroll_to_source_goal g =
{ Task.task_decl =
{ Theory.td_node =
Theory.Decl { Decl.d_node = Decl.Dprop (Decl.Pgoal, _, f)}}} ->
color_f_labels () f
color_f_locs () f
| _ ->
assert false
......
......@@ -20,8 +20,8 @@
open Format
open Pp
open Util
open Ptree
open Ident
open Ptree
open Ty
open Term
open Theory
......@@ -129,18 +129,26 @@ and dpattern_node =
| Por of dpattern * dpattern
| Pas of dpattern * ident
let create_user_id { id = x ; id_lab = ll ; id_loc = loc } =
let get_labels (ll,p) = function
| Lstr l -> l::ll, p
| Lpos p -> ll, Some p
in
let labels,p = List.fold_left get_labels ([],None) ll in
id_user ~labels x (default_option loc p)
let create_user_vs id ty = create_vsymbol (create_user_id id) ty
let rec pattern_env env p = match p.dp_node with
| Pwild -> env
| Papp (_, pl) -> List.fold_left pattern_env env pl
| Por (p, _) -> pattern_env env p
| Pvar { id = x ; id_lab = labels ; id_loc = loc } ->
let ty = ty_of_dty p.dp_ty in
let vs = create_vsymbol (id_user ~labels x loc) ty in
Mstr.add x vs env
| Pas (p, { id = x ; id_lab = labels ; id_loc = loc }) ->
let ty = ty_of_dty p.dp_ty in
let vs = create_vsymbol (id_user ~labels x loc) ty in
pattern_env (Mstr.add x vs env) p
| Pvar id ->
let vs = create_user_vs id (ty_of_dty p.dp_ty) in
Mstr.add id.id vs env
| Pas (p, id) ->
let vs = create_user_vs id (ty_of_dty p.dp_ty) in
pattern_env (Mstr.add id.id vs env) p
let get_pat_var env p x = try Mstr.find x env with Not_found ->
raise (Term.UncoveredVar (create_vsymbol (id_fresh x) (ty_of_dty p.dp_ty)))
......@@ -194,11 +202,10 @@ let rec term env t = match t.dt_node with
t_app s (List.map (term env) tl) (ty_of_dty t.dt_ty)
| Tif (f, t1, t2) ->
t_if (fmla env f) (term env t1) (term env t2)
| Tlet (e1, { id = x ; id_lab = labels ; id_loc = loc }, e2) ->
let ty = ty_of_dty e1.dt_ty in
| Tlet (e1, id, e2) ->
let e1 = term env e1 in
let v = create_vsymbol (id_user ~labels x loc) ty in
let env = Mstr.add x v env in
let v = create_user_vs id e1.t_ty in
let env = Mstr.add id.id v env in
let e2 = term env e2 in
t_let_close v e1 e2
| Tmatch (t1, bl) ->
......@@ -206,13 +213,16 @@ let rec term env t = match t.dt_node with
let env, p = pattern env p in t_close_branch p (term env e)
in
t_case (term env t1) (List.map branch bl)
| Tnamed (x, e1) ->
let e1 = term env e1 in
t_label_add x e1
| Teps ({ id = x ; id_lab = labels ; id_loc = loc }, ty, e1) ->
let ty = ty_of_dty ty in
let v = create_vsymbol (id_user ~labels x loc) ty in
let env = Mstr.add x v env in
| Tnamed _ ->
let rec collect p ll e = match e.dt_node with
| Tnamed (Lstr l, e) -> collect p (l::ll) e
| Tnamed (Lpos p, e) -> collect (Some p) ll e
| _ -> t_label ?loc:p ll (term env e)
in
collect None [] 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
let e1 = fmla env e1 in
t_eps_close v e1
......@@ -228,10 +238,9 @@ and fmla env = function
| Fif (f1, f2, f3) ->
f_if (fmla env f1) (fmla env f2) (fmla env f3)
| Fquant (q, uqu, trl, f1) ->
let uquant env ({ id = x ; id_lab = labels ; id_loc = loc },ty) =
let ty = ty_of_dty ty in
let v = create_vsymbol (id_user ~labels x loc) ty in
Mstr.add x v env, v
let uquant env (id,ty) =
let v = create_user_vs id (ty_of_dty ty) in
Mstr.add id.id v env, v
in
let env, vl = map_fold_left uquant env uqu in
let trigger = function
......@@ -242,11 +251,10 @@ and fmla env = function
f_quant_close q vl trl (fmla env f1)
| Fapp (s, tl) ->
f_app s (List.map (term env) tl)
| Flet (e1, { id = x ; id_lab = labels ; id_loc = loc }, f2) ->
let ty = ty_of_dty e1.dt_ty in
| Flet (e1, id, f2) ->
let e1 = term env e1 in
let v = create_vsymbol (id_user ~labels x loc) ty in
let env = Mstr.add x v env in
let v = create_user_vs id e1.t_ty in
let env = Mstr.add id.id v env in
let f2 = fmla env f2 in
f_let_close v e1 f2
| Fmatch (t, bl) ->
......@@ -254,9 +262,13 @@ and fmla env = function
let env, p = pattern env p in f_close_branch p (fmla env e)
in
f_case (term env t) (List.map branch bl)
| Fnamed (x, f1) ->
let f1 = fmla env f1 in
f_label_add x f1
| (Fnamed _) as f ->
let rec collect p ll = function
| Fnamed (Lstr l, e) -> collect p (l::ll) e
| Fnamed (Lpos p, e) -> collect (Some p) ll e
| e -> f_label ?loc:p ll (fmla env e)
in
collect None [] f
| Fvar f ->
f
......@@ -284,8 +296,9 @@ let specialize_lsymbol ~loc s =
let ident_of_vs ~loc vs =
{ id = vs.vs_name.id_string;
id_lab = vs.vs_name.id_label;
id_lab = List.map (fun l -> Lstr l) vs.vs_name.id_label;
id_loc = match vs.vs_name.id_origin with
(* FIXME: should we add this loc to id_lab? *)
| User loc -> loc
| _ -> loc }
......@@ -310,7 +323,9 @@ let rec specialize_term ~loc htv t =
{ dt_node = specialize_term_node ~loc htv t.t_node;
dt_ty = specialize_ty ~loc htv t.t_ty; }
in
List.fold_left (fun t l -> { t with dt_node = Tnamed (l, t) }) dt t.t_label
let add_label l t = { t with dt_node = Tnamed (l, t) } in
let dt = option_apply dt (fun p -> add_label (Lpos p) dt) t.t_loc in
List.fold_left (fun t l -> add_label (Lstr l) t) dt t.t_label
and specialize_term_node ~loc htv = function
| Term.Tvar v ->
......@@ -336,10 +351,10 @@ and specialize_term_node ~loc htv = function
Teps (ident_of_vs ~loc v, specialize_ty ~loc htv v.vs_ty,
specialize_fmla ~loc htv f)
(* TODO: labels are lost *)
and specialize_fmla ~loc htv f =
let df = specialize_fmla_node ~loc htv f.f_node in
List.fold_left (fun f l -> Fnamed (l, f)) df f.f_label
let df = option_apply df (fun p -> Fnamed (Lpos p,df)) f.f_loc in
List.fold_left (fun f l -> Fnamed (Lstr l, f)) df f.f_label
and specialize_fmla_node ~loc htv = function
| Term.Fapp (ls, tl) ->
......
......@@ -47,6 +47,8 @@ val ty_of_dty : dty -> ty
type ident = Ptree.ident
val create_user_id : Ptree.ident -> Ident.preid
type dpattern = { dp_node : dpattern_node; dp_ty : dty }
and dpattern_node =
......@@ -67,7 +69,7 @@ and dterm_node =
| Tif of dfmla * dterm * dterm
| Tlet of dterm * ident * dterm
| Tmatch of dterm * (dpattern * dterm) list
| Tnamed of Ident.label * dterm
| Tnamed of Ptree.label * dterm
| Teps of ident * dty * dfmla
and dfmla =
......@@ -80,7 +82,7 @@ and dfmla =
| Fif of dfmla * dfmla * dfmla
| Flet of dterm * ident * dfmla
| Fmatch of dterm * (dpattern * dfmla) list
| Fnamed of Ident.label * dfmla
| Fnamed of Ptree.label * dfmla
| Fvar of fmla
and dtrigger =
......@@ -95,8 +97,7 @@ val fmla : vsymbol Mstr.t -> dfmla -> fmla
val specialize_ty : loc:Ptree.loc -> type_var Htv.t -> ty -> dty
val specialize_lsymbol :
loc:Ptree.loc -> lsymbol -> dty list * dty option
val specialize_lsymbol : loc:Ptree.loc -> lsymbol -> dty list * dty option
val specialize_term : loc:Ptree.loc -> type_var Htv.t -> term -> dterm
......
......@@ -171,9 +171,14 @@ let op_char_1234 = op_char_1 | op_char_234
let op_char_pref = ['!' '?']
rule token = parse
| "#" space* ("\"" ([^ '\010' '\013' '"' ]* as file) "\"")?
space* (digit+ as line) space* (digit+ as char) space* "#"
| "##" space* ("\"" ([^ '\010' '\013' '"' ]* as file) "\"")?
space* (digit+ as line) space* (digit+ as char) space* "##"
{ update_loc lexbuf file line char; token lexbuf }
| "#" space* "\"" ([^ '\010' '\013' '"' ]* as file) "\""
space* (digit+ as line) space* (digit+ as bchar) space*
(digit+ as echar) space* "#"
{ POSITION (Loc.user_position file (int_of_string line)
(int_of_string bchar) (int_of_string echar)) }
| newline
{ newline lexbuf; token lexbuf }
| space+
......
......@@ -148,6 +148,7 @@
%token <string> OP1 OP2 OP3 OP4 OPPREF
%token <Ptree.real_constant> FLOAT
%token <string> STRING
%token <Loc.position> POSITION
/* keywords */
......@@ -244,8 +245,8 @@ list0_theory:
theory_head:
| THEORY uident labels
{ let id = add_lab $2 $3 and labels = $3 in
let name = Ident.id_user ~labels id.id id.id_loc in
{ let id = add_lab $2 $3 in
let name = Denv.create_user_id id in
ref_push uc_ref (create_theory name); id }
;
......@@ -516,11 +517,11 @@ lexpr:
| lexpr OR lexpr
{ infix_pp $1 PPor $3 }
| lexpr BARBAR lexpr
{ mk_pp (PPnamed (Ident.label "asym_split", infix_pp $1 PPor $3)) }
{ mk_pp (PPnamed (Lstr "asym_split", infix_pp $1 PPor $3)) }
| lexpr AND lexpr
{ infix_pp $1 PPand $3 }
| lexpr AMPAMP lexpr
{ mk_pp (PPnamed (Ident.label "asym_split", infix_pp $1 PPand $3)) }
{ mk_pp (PPnamed (Lstr "asym_split", infix_pp $1 PPand $3)) }
| NOT lexpr
{ prefix_pp PPnot $2 }
| lexpr EQUAL lexpr
......@@ -869,12 +870,9 @@ qualid:
label:
| STRING
{ Ident.label $1 }
| STRING BACKQUOTE INTEGER BACKQUOTE INTEGER
BACKQUOTE INTEGER BACKQUOTE STRING
{ let loc = Loc.user_position $9 (int_of_string $3) (int_of_string $5)
(int_of_string $7)
in Ident.label ~loc $1 }
{ Lstr $1 }
| POSITION
{ Lpos $1 }
;
labels:
......
......@@ -25,7 +25,10 @@ type loc = Loc.position
type real_constant = Term.real_constant
type constant = Term.constant
type label = Ident.label
type label =
| Lstr of Ident.label
| Lpos of Loc.position
type pp_quant =
| PPforall | PPexists | PPlambda | PPfunc | PPpred
......@@ -241,7 +244,7 @@ type program_decl =
type module_ = {
mod_name : ident;
mod_labels : Ident.label list;
mod_labels : label list;
mod_decl : program_decl list;
}
......
......@@ -460,11 +460,12 @@ let apply_highord loc x tl = match List.rev tl with
let rec dterm ?(localize=false) env { pp_loc = loc; pp_desc = t } =
let n, ty = dterm_node ~localize loc env t in
let t = { dt_node = n; dt_ty = ty } in
if localize then
let n = Tnamed (Ident.label ~loc "", t) in
{ dt_node = n; dt_ty = ty }
else
t
let rec down e = match e.dt_node with
| Tnamed (Lstr _, e) -> down e
| Tnamed (Lpos _, _) -> t
| _ -> { dt_node = Tnamed (Lpos loc, t); dt_ty = ty }
in
if localize then down t else t
and dterm_node ~localize loc env = function
| PPvar (Qident {id=x}) when Mstr.mem x env.dvars ->
......@@ -521,6 +522,10 @@ and dterm_node ~localize loc env = function
let bl = List.map branch bl in
Tmatch (t1, bl), tb
| PPnamed (x, e1) ->
let localize = match x with
| Lpos _ -> false
| Lstr _ -> true
in
let e1 = dterm ~localize env e1 in
Tnamed (x, e1), e1.dt_ty
| PPcast (e1, ty) ->
......@@ -647,8 +652,13 @@ and dterm_node ~localize loc env = function
error ~loc TermExpected
and dfmla ?(localize=false) env { pp_loc = loc; pp_desc = f } =
let n = dfmla_node ~localize loc env f in
if localize then Fnamed (Ident.label ~loc "", n) else n
let f = dfmla_node ~localize loc env f in
let rec down e = match e with
| Fnamed (Lstr _, e) -> down e
| Fnamed (Lpos _, _) -> f
| _ -> Fnamed (Lpos loc, f)
in
if localize then down f else f
and dfmla_node ~localize loc env = function
| PPtrue ->
......@@ -719,6 +729,10 @@ and dfmla_node ~localize loc env = function
in
Fmatch (t1, List.map branch bl)
| PPnamed (x, f1) ->
let localize = match x with
| Lpos _ -> false
| Lstr _ -> true
in
let f1 = dfmla ~localize env f1 in
Fnamed (x, f1)
| PPvar (Qident s | Qdot (_,s) as x) when is_uppercase s.id.[0] ->
......@@ -788,11 +802,10 @@ let add_projections th d = match d.td_def with
| Some t -> t
in
let per_param acc ty (n,_) = match n with
| Some { id = id ; id_lab = labels ; id_loc = loc }
when not (Mstr.mem id acc) ->
let fn = id_user ~labels id loc in
| Some id when not (Mstr.mem id.id acc) ->
let fn = create_user_id id in
let fs = create_fsymbol fn [tc] ty in
Mstr.add id (fs,tc,ty) acc
Mstr.add id.id (fs,tc,ty) acc
| _ -> acc
in
List.fold_left2 per_param acc cs.ls_args pl
......@@ -822,18 +835,15 @@ let add_types dl th =
with Not_found ->
Hashtbl.add tysymbols x None;
let d = Mstr.find x def in
let id = d.td_ident.id in
let vars = Hashtbl.create 17 in
let vl =
List.map
(fun { id = v ; id_lab = labels ; id_loc = loc } ->
if Hashtbl.mem vars v then error ~loc (DuplicateTypeVar v);
let i = create_tvsymbol (id_user ~labels v loc) in
Hashtbl.add vars v i;
i)
d.td_params
let vl = List.map (fun id ->
if Hashtbl.mem vars id.id then
error ~loc:id.id_loc (DuplicateTypeVar id.id);
let i = create_tvsymbol (create_user_id id) in
Hashtbl.add vars id.id i;
i) d.td_params
in
let id = id_user id ~labels:d.td_ident.id_lab d.td_loc in
let id = create_user_id d.td_ident in
let ts = match d.td_def with
| TDalias ty ->
let rec apply = function
......@@ -891,11 +901,11 @@ let add_types dl th =
Tabstract
| TDalgebraic cl ->
let ty = ty_app ts (List.map ty_var ts.ts_args) in
let constructor (loc, { id = id ; id_lab = labels }, pl) =
let constructor (loc, id, pl) =
let param (_,t) = ty_of_dty (dty th' t) in
let tyl = List.map param pl in
Hashtbl.replace csymbols id loc;
create_fsymbol (id_user ~labels id loc) tyl ty
Hashtbl.replace csymbols id.id loc;
create_fsymbol (create_user_id id) tyl ty
in
Talgebraic (List.map constructor cl)
| TDrecord _ ->
......@@ -933,7 +943,7 @@ let add_logics dl th =
(* 1. create all symbols and make an environment with these symbols *)
let create_symbol th d =
let id = d.ld_ident.id in
let v = id_user ~labels:d.ld_ident.id_lab id d.ld_loc in
let v = create_user_id d.ld_ident in
let denv = create_denv th in
Hashtbl.add denvs id denv;
let type_ty (_,t) = ty_of_dty (dty denv t) in
......@@ -964,7 +974,7 @@ let add_logics dl th =
let create_var (x, _) ty =
let id = match x with
| None -> id_fresh "%x"
| Some id -> id_user ~labels:id.id_lab id.id id.id_loc
| Some id -> create_user_id id
in
create_vsymbol id ty
in
......@@ -1011,7 +1021,7 @@ let type_fmla denv env f =
fmla env f
let add_prop k loc s f th =
let pr = create_prsymbol (id_user ~labels:s.id_lab s.id loc) in
let pr = create_prsymbol (create_user_id s) in
try add_prop_decl th k pr (type_fmla (create_denv th) Mstr.empty f)
with ClashSymbol s -> error ~loc (Clash s)
......@@ -1025,7 +1035,7 @@ let add_inductives dl th =
let psymbols = Hashtbl.create 17 in
let create_symbol th d =
let id = d.in_ident.id in
let v = id_user ~labels:d.in_ident.id_lab id d.in_loc in
let v = create_user_id d.in_ident in
let type_ty (_,t) = ty_of_dty (dty denv t) in
let pl = List.map type_ty d.in_params in
let ps = create_psymbol v pl in
......@@ -1040,10 +1050,10 @@ let add_inductives dl th =
let type_decl d =
let id = d.in_ident.id in
let ps = Hashtbl.find psymbols id in
let clause (loc, { id = id ; id_lab = labels }, f) =
Hashtbl.replace propsyms id loc;
let clause (loc, id, f) =
Hashtbl.replace propsyms id.id loc;
let f = type_fmla denv Mstr.empty f in
create_prsymbol (id_user ~labels id loc), f
create_prsymbol (create_user_id id), f
in
ps, List.map clause d.in_def
in
......
......@@ -138,9 +138,14 @@ and specialize_type_c ~loc htv c =
dc_post = specialize_post ~loc htv c.c_post; }
and specialize_binder ~loc htv v =
let id = { id = v.pv_name.id_string;
id_lab = v.pv_name.id_label;
id_loc = loc } in
let id = {
id = v.pv_name.id_string;
id_lab = List.map (fun l -> Lstr l) v.pv_name.id_label;
(* FIXME? We do the same here as in Denv.ident_of_vs *)
id_loc = match v.pv_name.id_origin with
| User loc -> loc
| _ -> loc }
in
let v = specialize_type_v ~loc htv v.pv_tv in
id, dpurify_type_v v, v
......
......@@ -259,8 +259,9 @@ let well_founded_rel = function
(* Recursive computation of the weakest precondition *)
let propose_label l f =
if f.f_label = [] then f_label [l] f else f
let wp_label ?loc f =
if List.mem "WP" f.f_label then f
else f_label ?loc ("WP"::f.f_label) f
let t_True env =
t_app (find_ls env "True") [] (ty_app (find_ts env "bool") [])
......@@ -270,7 +271,7 @@ let rec wp_expr env e q =
let q = post_map (old_label env lab) q in
let f = wp_desc env e q in
let f = erase_label env lab f in
let f = propose_label (label ~loc:e.expr_loc "WP") f in
let f = wp_label ~loc:e.expr_loc f in
if Debug.test_flag debug then begin
eprintf "@[--------@\n@[<hov 2>e = %a@]@\n" Pgm_pretty.print_expr e;
eprintf "@[<hov 2>q = %a@]@\n" Pretty.print_fmla (snd (fst q));
......@@ -297,7 +298,7 @@ and wp_desc env e q = match e.expr_desc with
| Elet (x, e1, e2) ->
let w2 = wp_expr env e2 (filter_post e2.expr_effect q) in
let v1 = v_result x.pv_vs.vs_ty in
let t1 = t_label_add (label ~loc:e1.expr_loc "let") (t_var v1) in
let t1 = t_label ~loc:e1.expr_loc ["let"] (t_var v1) in
let q1 = v1, f_subst (subst1 x.pv_vs t1) w2 in
let q1 = saturate_post e1.expr_effect q1 q in
wp_expr env e1 q1
......@@ -305,14 +306,13 @@ and wp_desc env e q = match e.expr_desc with
let w1 = wp_expr env e1 q in
let wl = List.map (wp_recfun env) dl in
wp_ands ~sym:true (w1 :: wl)
| Eif (e1, e2, e3) ->
let w2 = wp_expr env e2 (filter_post e2.expr_effect q) in
let w3 = wp_expr env e3 (filter_post e3.expr_effect q) in
let q1 = (* if result=True then w2 else w3 *)
let res = v_result e1.expr_type in
let test = f_equ (t_var res) (t_True env) in