Commit 7c454a39 authored by MARCHE Claude's avatar MARCHE Claude

create_type_decl does not return metas anymore

metas are stored in a new field pd_metas aside the field pd_pure
parent 12fc9ca6
......@@ -133,6 +133,7 @@ let create_rec_variant_decl s csl =
type pdecl = {
pd_node : pdecl_node;
pd_pure : decl list;
pd_metas : (Theory.meta * Theory.meta_arg list) list;
pd_syms : Sid.t;
pd_news : Sid.t;
pd_tag : int;
......@@ -292,12 +293,14 @@ let get_syms node pure =
| PDexn xs -> syms_ity syms xs.xs_ity
| PDpure -> syms
let mk_decl = let r = ref 0 in fun node pure ->
{ pd_node = node; pd_pure = pure;
let mk_decl_metas = let r = ref 0 in fun metas node pure ->
{ pd_node = node; pd_pure = pure; pd_metas = metas;
pd_syms = get_syms node pure;
pd_news = get_news node pure;
pd_tag = (incr r; !r) }
let mk_decl = mk_decl_metas []
let create_type_decl dl =
if dl = [] then invalid_arg "Pdecl.create_type_decl";
let add_itd ({itd_its = s} as itd) (abst,defn,rest,metas) =
......@@ -396,7 +399,7 @@ let create_type_decl dl =
in
let abst,defn,rest,metas = List.fold_right add_itd dl ([],[],[],[]) in
let defn = if defn = [] then [] else [create_data_decl defn] in
mk_decl (PDtype dl) (abst @ defn @ rest), metas
mk_decl_metas metas (PDtype dl) (abst @ defn @ rest)
(* TODO: share with Eliminate_definition *)
let rec t_insert hd t = match t.t_node with
......
......@@ -77,6 +77,7 @@ val create_float_decl : preid -> Number.float_format -> its_defn
type pdecl = private {
pd_node : pdecl_node;
pd_pure : Decl.decl list;
pd_metas : (Theory.meta * Theory.meta_arg list) list;
pd_syms : Sid.t;
pd_news : Sid.t;
pd_tag : int;
......@@ -89,7 +90,7 @@ and pdecl_node = private
| PDpure
val create_type_decl :
its_defn list -> pdecl * (Theory.meta * Theory.meta_arg list) list
its_defn list -> pdecl
val create_let_decl : let_defn -> pdecl
......
......@@ -289,6 +289,7 @@ let add_pdecl_no_logic uc d =
let add_pdecl_raw ?(warn=true) uc d =
let uc = add_pdecl_no_logic uc d in
let th = List.fold_left (add_decl ~warn) uc.muc_theory d.pd_pure in
let th = List.fold_left (fun th (m,l) -> Theory.add_meta th m l) th d.pd_metas in
{ uc with muc_theory = th }
(** {2 Builtin symbols} *)
......@@ -327,8 +328,7 @@ let unit_module =
let uc = empty_module dummy_env (id_fresh "Unit") ["why3";"Unit"] in
let uc = use_export uc (tuple_module 0) in
let td = create_alias_decl (id_fresh "unit") [] ity_unit in
let d,metas = create_type_decl [td] in
assert (metas = []);
let d = create_type_decl [td] in
close_module (add_pdecl_raw ~warn:false uc d)
let create_module env ?(path=[]) n =
......@@ -932,11 +932,8 @@ let clone_pdecl inst cl uc d = match d.pd_node with
| PDtype tdl ->
let tdl, vcl = clone_type_decl inst cl tdl uc.muc_known in
if tdl = [] then List.fold_left add_vc uc vcl else
let d,metas = create_type_decl tdl in
List.fold_left
(fun uc (m,a) -> add_meta uc m a)
(add_pdecl ~warn:false ~vc:false uc d)
metas
let d = create_type_decl tdl in
add_pdecl ~warn:false ~vc:false uc d
| PDlet (LDsym (rs, c)) when Mrs.mem rs inst.mi_rs ->
(* refine only [val] symbols *)
if c.c_node <> Cany then raise (BadInstance rs.rs_name);
......@@ -1003,7 +1000,9 @@ let clone_pdecl inst cl uc d = match d.pd_node with
cl.xs_table <- Mxs.add xs xs' cl.xs_table;
add_pdecl ~warn:false ~vc:false uc (create_exn_decl xs')
| PDpure ->
List.fold_left (clone_decl inst cl) uc d.pd_pure
let uc = List.fold_left (clone_decl inst cl) uc d.pd_pure in
assert (d.pd_metas = []); (* FIXME! *)
uc
let theory_add_clone = Theory.add_clone_internal ()
......
......@@ -939,11 +939,9 @@ let add_types muc tdl =
Mstr.iter (visit ~alias:Mstr.empty ~alg:Mstr.empty) def;
let tdl = List.map (fun d -> Hstr.find htd d.td_ident.id_str) tdl in
let d,metas = create_type_decl tdl in
List.fold_left
(fun uc (m,a) -> add_meta uc m a)
(add_pdecl ~vc:true muc d)
metas
let d = create_type_decl tdl in
add_pdecl ~vc:true muc d
let tyl_of_params {muc_theory = tuc} pl =
let ty_of_param (loc,_,gh,ty) =
......
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