[wp_strategies] refactor documentation

lustrec_wp_strategies/lustrec_wp_strategies.ml

 (** LustreC WP strategies plug-in.
 
-    No function is exported. *)
+    No function/module is exported. *)

lustrec_wp_strategies/lustrec_wp_strategies_definitions.ml

+(** This module contains the strategies that should be used by WP to
+    prove ACSL contracts generated by LustreC.
+
+    @author Lélio Brun
+ *)
+
+(* Globally open WP module. *)
 open Wp
 
-(* check that a given predicate name is a transition and return its index *)
+(** Checks that a given predicate name is a transition
+    and returns its index. *)
 let is_transition (f : Lang.lfun) : int option =
   let open Str in
   let r = regexp "_transition\\([0-9]+\\)$" in
@@ -10,7 +18,8 @@ let is_transition (f : Lang.lfun) : int option =
     Some (int_of_string (matched_group 1 s))
   with Not_found -> None
 
-(* check that a given predicate name is a transition with given index *)
+(** Checks that a given predicate name is a transition with a given
+    index. *)
 let is_transition_n (n : int) (f : Lang.lfun) : bool =
   let open Str in
   let r = regexp ("_transition" ^ string_of_int n ^ "$") in
@@ -19,7 +28,7 @@ let is_transition_n (n : int) (f : Lang.lfun) : bool =
     true
   with Not_found -> false
 
-(* check that a given predicate name is a memory pack simulation *)
+(** Checks that a given predicate name is a memory pack simulation. *)
 let is_pack (f : Lang.lfun) : bool =
   let open Str in
   let r = regexp "_pack\\(\\|[0-9]+\\|_base\\)$" in
@@ -29,17 +38,17 @@ let is_pack (f : Lang.lfun) : bool =
     true
   with Not_found -> false
 
-(* tactical selection of the goal *)
+(** Tactical selection of the goal. *)
 let select_g (g : Lang.F.pred) : Tactical.selection =
   let open Tactical in
   Clause (Goal g)
 
-(* tactical selection of an hypothesis *)
+(** Tactical selection of an hypothesis. *)
 let select_h (h : Conditions.step) : Tactical.selection =
   let open Tactical in
   Clause (Step h)
 
-(* get variables and predicate under existential binder *)
+(** Gets variables and predicate under existential binder. *)
 let existential_vars_g (g : Lang.F.pred) : Lang.F.var list * Lang.F.term =
   let open Lang.F in
   let copy = pool () in
@@ -48,7 +57,7 @@ let existential_vars_g (g : Lang.F.pred) : Lang.F.var list * Lang.F.term =
   let vars, g = e_open ~forall:false ~lambda:false ~pool (e_prop g) in
   List.map snd vars, g
 
-(* find the index of the first element that verifies p in l *)
+(** Finds the index of the first element that verifies [p] in [l]. *)
 let find_index p l =
   let rec aux i = function
     | [] ->
@@ -58,14 +67,15 @@ let find_index p l =
   in
   aux 0 l
 
-(* check if the term t is the variable v *)
+(** Checks if the term [t] is the variable [v]. *)
 let is_var (v : Lang.F.var) (t : Lang.F.term) : bool =
   match Repr.term t with Var w -> v = w | _ -> false
 
+(** Exception used when a witness is found. *)
 exception Found of Tactical.selection list
 
-(* a function to search a transition call in the hypotheses *)
-(*  that can be unified with a term *)
+(** Searches a transition call in the hypotheses that can
+    be unified with a term *)
 let rec unify (push : Strategy.strategy -> unit) (sequent : Conditions.sequent)
     (vars : Lang.F.var list) (term : Lang.F.term) : unit =
   let hyps = fst sequent in
@@ -122,7 +132,7 @@ let rec unify (push : Strategy.strategy -> unit) (sequent : Conditions.sequent)
   | _ ->
     Lang.F.lc_iter (unify push sequent vars) term
 
-(* Transitions heuristic *)
+(** Class defining transitions heuristic. *)
 class lustrec_transitions : Strategy.heuristic =
   object
     method id = "LustreC:Transitions" (* required, must be unique *)
@@ -151,7 +161,8 @@ class lustrec_transitions : Strategy.heuristic =
         ()
   end
 
-(* unfold f(es) in the given context (context is handled with side-effects) *)
+(** Unfolds [f] function(s) in the given context (context is
+    handled with side-effects). *)
 let definition (context : WpContext.context) (f : Lang.lfun)
     (es : Lang.F.term list) : Lang.F.term =
   let on_ctx f = WpContext.on_context context f in
@@ -163,7 +174,7 @@ let definition (context : WpContext.context) (f : Lang.lfun)
   | _ ->
     assert false
 
-(* rewrite a sequent by unfolding a top-level memory pack relation *)
+(** Rewrites a sequent by unfolding a top-level memory pack relation. *)
 let unfold_process (context : WpContext.context) (t : Lang.F.term)
     (sequent : Conditions.sequent) : Conditions.sequent option =
   match Repr.term t with
@@ -173,11 +184,11 @@ let unfold_process (context : WpContext.context) (t : Lang.F.term)
   | _ ->
     None
 
-(* sequent equality *)
+(** Defines an equality relation on sequents. *)
 let eq_sequent s1 s2 = Lang.F.eqp (snd s1) (snd s2)
 
-(* rewrite a sequent by recursively unfolding memory pack relations, by *)
-(* iterating over sub-terms *)
+(** Rewrites a sequent by recursively unfolding memory pack relations
+    by iterating over sub-terms. *)
 let rec rewrite_process (context : WpContext.context)
     (sequent : Conditions.sequent) : Conditions.sequent =
   let goal = Lang.F.e_prop (snd sequent) in
@@ -203,7 +214,7 @@ let rec rewrite_process (context : WpContext.context)
       sequent
     with Found sequent' -> rewrite_process context sequent')
 
-(* Memory Packs tactical *)
+(** Class defining Memory Packs tactical. *)
 class unfold_rec =
   object
     inherit
@@ -219,10 +230,10 @@ class unfold_rec =
         (fun sequent -> [ "", rewrite_process context sequent ])
   end
 
-(* Memory Packs strategy *)
+(** Memory Packs strategy. *)
 let unfold_rec_strategy = Strategy.make (new unfold_rec) ~arguments:[]
 
-(* Memory Packs heuristic *)
+(** Class defining Memory Packs heuristic. *)
 class lustrec_memory_packs : Strategy.heuristic =
   object
     method id = "LustreC:MemoryPacks" (* required, must be unique *)

lustrec_wp_strategies/lustrec_wp_strategies_options.ml

-(* Register the plugin *)
+(** This module contains options for the LustreC WP strategies plugin.
+
+    @author Christophe Garion
+*)
+
+(** Content of the welcome message. *)
 let help_msg = "WP strategies needed for proving ACSL assertions generating with LustreC"
 
+(** Register the plugin to Frama-C. *)
 module Self = Plugin.Register
   (struct
     let name = "LustreC WP Strategies"

lustrec_wp_strategies/lustrec_wp_strategies_run.ml

-(* Register strategies and print simple message *)
+(** This module contains the function to be run when the module is
+    loaded and also registers the strategies wrt WP plugin.
+
+    @author Christophe Garion
+    @author Lelio Brun
+*)
+
+(** Prints a message when the plugin is loaded. *)
 let run () =
   Lustrec_wp_strategies_options.Self.result "LustreC WP strategies available."
 
+(** Register strategies to WP and print simple message when used. *)
 let () =
   Wp.Strategy.register (new Lustrec_wp_strategies_definitions.lustrec_transitions);
   Wp.Strategy.register (new Lustrec_wp_strategies_definitions.lustrec_memory_packs);