From 7572e56a59fcf6c9db025a8aff896577905389a8 Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Tue, 7 Apr 2020 14:30:51 +0200
Subject: [PATCH] [wp] Initialized types generated only when necessary
---
src/plugins/wp/Definitions.ml | 35 ++++++++++++++++++++++++++++++----
src/plugins/wp/Definitions.mli | 3 ++-
src/plugins/wp/ProverCoq.ml | 2 +-
src/plugins/wp/ProverErgo.ml | 2 +-
src/plugins/wp/ProverWhy3.ml | 2 +-
src/plugins/wp/TacLemma.ml | 2 +-
6 files changed, 37 insertions(+), 9 deletions(-)
diff --git a/src/plugins/wp/Definitions.ml b/src/plugins/wp/Definitions.ml
index 47199e0f72a..6a5c7ee962d 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 de1f82c3610..20beeda15d9 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 4e15ae25ccb..1f3b14409a7 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 17684a97957..1e9a0feae7c 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 a977d9f39ce..07b0ef0257e 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 8509c54131f..5a36bffa186 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 = ()
--
GitLab