diff --git a/src/plugins/wp/Definitions.ml b/src/plugins/wp/Definitions.ml
index 47199e0f72ab7ffedc1411ea24cfd3517031bd6f..6a5c7ee962d1fb992777297437fd9690e6236c05 100644
--- a/src/plugins/wp/Definitions.ml
+++ b/src/plugins/wp/Definitions.ml
@@ -45,6 +45,7 @@ type cluster = {
c_position : Filepath.position option ;
mutable c_age : int ;
mutable c_records : compinfo list ;
+ mutable c_irecords : compinfo list ;
mutable c_types : logic_type_info list ;
mutable c_symbols : dfun list ;
mutable c_lemmas : dlemma list ;
@@ -205,6 +206,7 @@ let newcluster ~id ?title ?position () =
c_age = 0 ;
c_types = [] ;
c_records = [] ;
+ c_irecords = [] ;
c_symbols = [] ;
c_lemmas = [] ;
}
@@ -242,6 +244,17 @@ let compinfo c =
in cluster.c_records <- [c] ; cluster)
(Lang.comp_id c)
+let icompinfo c =
+ Cluster.memoize
+ (fun id ->
+ let title =
+ if c.cstruct
+ then Printf.sprintf "Init Struct '%s'" c.cname
+ else Printf.sprintf "Init Union '%s'" c.cname in
+ let cluster = newcluster ~id ~title ()
+ in cluster.c_irecords <- [c] ; cluster)
+ (Lang.comp_init_id c)
+
let matrix = function
| C_array _ -> assert false
| C_comp c -> compinfo c
@@ -282,6 +295,7 @@ class virtual visitor main =
val mutable terms = Tset.empty
val mutable types = DT.empty
val mutable comps = DR.empty
+ val mutable icomps = DR.empty
val mutable symbols = DF.empty
val mutable dlemmas = DS.empty
val mutable lemmas = DS.empty
@@ -333,22 +347,34 @@ class virtual visitor main =
self#vtau t ; Cfield (f, KValue) , t
) r.cfields
in self#on_comp r fts ;
+ end
+ end
+
+ method vicomp r =
+ if not (DR.mem r icomps) then
+ begin
+ icomps <- DR.add r icomps ;
+ let c = icompinfo r in
+ if self#do_local c then
+ begin
let fts = List.map
(fun f ->
let t = Lang.init_of_ctype f.ftype in
self#vtau t ; Cfield (f, KInit) , t
) r.cfields
- in self#on_comp_init r fts ;
+ in self#on_icomp r fts ;
end
end
method vfield = function
| Mfield(a,_,_,_) -> self#vlibrary a.ext_library
- | Cfield(f, _) -> self#vcomp f.fcomp
+ | Cfield(f, KValue) -> self#vcomp f.fcomp
+ | Cfield(f, KInit) -> self#vicomp f.fcomp
method vadt = function
| Mtype a | Mrecord(a,_) -> self#vlibrary a.ext_library
- | Comp(r, _) -> self#vcomp r
+ | Comp(r, KValue) -> self#vcomp r
+ | Comp(r, KInit) -> self#vicomp r
| Atype t -> self#vtype t
method vtau = function
@@ -521,6 +547,7 @@ class virtual visitor main =
method vtypes = (* Visit the types *)
rev_iter self#vcomp main.c_records ;
+ rev_iter self#vicomp main.c_irecords ;
rev_iter self#vtype main.c_types
method vsymbols = (* Visit the definitions *)
@@ -541,7 +568,7 @@ class virtual visitor main =
method virtual on_cluster : cluster -> unit
method virtual on_type : logic_type_info -> typedef -> unit
method virtual on_comp : compinfo -> (field * tau) list -> unit
- method virtual on_comp_init : compinfo -> (field * tau) list -> unit
+ method virtual on_icomp : compinfo -> (field * tau) list -> unit
method virtual on_dlemma : dlemma -> unit
method virtual on_dfun : dfun -> unit
diff --git a/src/plugins/wp/Definitions.mli b/src/plugins/wp/Definitions.mli
index de1f82c36101fd73ae216991d5e6986c4993d458..20beeda15d92f1f238c00c73806dc1c5d4117846 100644
--- a/src/plugins/wp/Definitions.mli
+++ b/src/plugins/wp/Definitions.mli
@@ -107,6 +107,7 @@ class virtual visitor : cluster ->
method vadt : ADT.t -> unit
method vtype : logic_type_info -> unit
method vcomp : compinfo -> unit
+ method vicomp : compinfo -> unit
method vfield : Field.t -> unit
method vtau : tau -> unit
method vparam : var -> unit
@@ -129,7 +130,7 @@ class virtual visitor : cluster ->
method virtual on_cluster : cluster -> unit (** Outer cluster to import *)
method virtual on_type : logic_type_info -> typedef -> unit (** This local type must be defined *)
method virtual on_comp : compinfo -> (field * tau) list -> unit (** This local compinfo must be defined *)
- method virtual on_comp_init : compinfo -> (field * tau) list -> unit (** This local compinfo must be defined *)
+ method virtual on_icomp : compinfo -> (field * tau) list -> unit (** This local compinfo initialization must be defined *)
method virtual on_dlemma : dlemma -> unit (** This local lemma must be defined *)
method virtual on_dfun : dfun -> unit (** This local function must be defined *)
diff --git a/src/plugins/wp/ProverCoq.ml b/src/plugins/wp/ProverCoq.ml
index 4e15ae25ccbde8413a8f89b56228709b9acd3182..1f3b14409a7ba05c7b5d7851fb388ce2fdc34625 100644
--- a/src/plugins/wp/ProverCoq.ml
+++ b/src/plugins/wp/ProverCoq.ml
@@ -182,7 +182,7 @@ class visitor fmt c =
engine#declare_type fmt (Lang.comp c) 0 (Qed.Engine.Trec fts) ;
end
- method on_comp_init c fts =
+ method on_icomp c fts =
begin
self#paragraph ;
engine#declare_type fmt (Lang.comp_init c) 0 (Qed.Engine.Trec fts) ;
diff --git a/src/plugins/wp/ProverErgo.ml b/src/plugins/wp/ProverErgo.ml
index 17684a979571816e605533bd3473c4aa18727fba..1e9a0feae7cd9372939cd1f55a56a0d8c1b37d57 100644
--- a/src/plugins/wp/ProverErgo.ml
+++ b/src/plugins/wp/ProverErgo.ml
@@ -187,7 +187,7 @@ class visitor fmt c =
engine#declare_type fmt (Lang.comp c) 0 (Qed.Engine.Trec fts) ;
end
- method on_comp_init c fts =
+ method on_icomp c fts =
begin
self#lines ;
engine#declare_type fmt (Lang.comp_init c) 0 (Qed.Engine.Trec fts) ;
diff --git a/src/plugins/wp/ProverWhy3.ml b/src/plugins/wp/ProverWhy3.ml
index a977d9f39ce949284cbb341bda1df313fa49ce13..07b0ef0257e942702a812436a6d212057a865a3b 100644
--- a/src/plugins/wp/ProverWhy3.ml
+++ b/src/plugins/wp/ProverWhy3.ml
@@ -925,7 +925,7 @@ class visitor (ctx:context) c =
end
method on_comp = self#on_comp_gen KValue
- method on_comp_init = self#on_comp_gen KInit
+ method on_icomp = self#on_comp_gen KInit
method private make_lemma cnv (l: Definitions.dlemma) =
let id = Why3.Ident.id_fresh (Lang.lemma_id l.l_name) in
diff --git a/src/plugins/wp/TacLemma.ml b/src/plugins/wp/TacLemma.ml
index 8509c54131f401e534b00c0ad479ef1c714223c5..5a36bffa18669a916bb1a216915cda30721e8cb6 100644
--- a/src/plugins/wp/TacLemma.ml
+++ b/src/plugins/wp/TacLemma.ml
@@ -46,7 +46,7 @@ class browser ?on_cluster f cluster =
method on_library _ = ()
method on_type _ _ = ()
method on_comp _ _ = ()
- method on_comp_init _ _ = ()
+ method on_icomp _ _ = ()
method on_dfun _ = ()
method! vtypes = ()
method! vsymbols = ()