1 files changed, 17 insertions, 10 deletions
diff --git a/kvx/abstractbb/ImpSimuTest.v b/kvx/abstractbb/ImpSimuTest.v
index c914eee1..97d1a234 100644
--- a/kvx/abstractbb/ImpSimuTest.v
+++ b/kvx/abstractbb/ImpSimuTest.v
@@ -10,9 +10,11 @@
 (*                                                             *)
 (* *************************************************************)
 
-(** Implementation of a symbolic execution of sequential semantics of Abstract Basic Blocks
+(** Implementation of a simulation test (ie a "scheduling verifier") for the sequential semantics of Abstract Basic Blocks.
 
-with imperative hash-consing, and rewriting.
+It is based on a symbolic execution procedure of Abstract Basic Blocks with imperative hash-consing and rewriting.
+
+It also provides debugging information when the test fails.
 
 *)
 
@@ -32,6 +34,7 @@ Import ListNotations.
 Local Open Scope list_scope.
 
 
+(** * Interface of (impure) equality tests for operators *)
 Module Type ImpParam.
 
 Include LangParam.
@@ -54,6 +57,8 @@ Include MkSeqLanguage LP.
 End ISeqLanguage.
 
 
+(** * A generic dictinary on PseudoRegisters with an impure equality test  *)
+
 Module Type ImpDict.
 
 Declare Module R: PseudoRegisters.
@@ -91,26 +96,27 @@ Parameter eq_test_correct: forall A (d1 d2: t A),
 
 (* NB: we could also take an eq_test on R.t (but not really useful with "pure" dictionaries  *)
 
-
-(* only for debugging *)
+(** only for debugging *)
 Parameter not_eq_witness: forall {A}, t A -> t A -> ?? option R.t.
 
 End ImpDict.
 
 
+(** * Specification of the provided tests *)
 Module Type ImpSimuInterface.
 
 Declare Module CoreL: ISeqLanguage.
 Import CoreL.
 Import Terms.
 
+(** the silent test (without debugging informations) *)
 Parameter bblock_simu_test: reduction -> bblock -> bblock -> ?? bool.
 
 Parameter bblock_simu_test_correct: forall reduce (p1 p2 : bblock),
     WHEN bblock_simu_test reduce p1 p2 ~> b
     THEN b = true -> forall ge : genv, bblock_simu ge p1 p2.
 
-
+(** the verbose test extended with debugging informations *)
 Parameter verb_bblock_simu_test
      : reduction ->
        (R.t -> ?? pstring) ->
@@ -127,6 +133,7 @@ Parameter verb_bblock_simu_test_correct:
 End ImpSimuInterface.
 
 
+(** * Implementation of the provided tests *)
 
 Module ImpSimu (L: ISeqLanguage) (Dict: ImpDict with Module R:=L.LP.R): ImpSimuInterface with Module CoreL := L.
 
@@ -168,7 +175,7 @@ Section SimuWithReduce.
 
 Variable reduce: reduction.
 
-Section CanonBuilding.
+Section CanonBuilding. (** Implementation of the symbolic execution (ie a "canonical form" representing the semantics of an abstract basic block) *)
 
 Variable hC_term: hashinfo term -> ?? term.
 Hypothesis hC_term_correct: forall t, WHEN hC_term t ~> t' THEN forall ge m, term_eval ge (hdata t) m = term_eval ge t' m.
@@ -1117,9 +1124,9 @@ Extraction Inline lift.
 
 End ImpSimu.
 
-Require Import FMapPositive.
-
 
+(** * Implementation of the Dictionary (based on PositiveMap) *)
+Require Import FMapPositive.
 Require Import PArith.
 Require Import FMapPositive.
 
@@ -1206,7 +1213,7 @@ Proof.
 Qed.
 Global Opaque eq_test.
 
-(* ONLY FOR DEBUGGING INFO: get some key of a non-empty d *)
+(** ONLY FOR DEBUGGING INFO: get some key of a non-empty d *)
 Fixpoint pick {A} (d: t A): ?? R.t :=
   match d with
   | Leaf _ => FAILWITH "unexpected empty dictionary"
@@ -1219,7 +1226,7 @@ Fixpoint pick {A} (d: t A): ?? R.t :=
     RET (xO p)
   end.
 
-(* ONLY FOR DEBUGGING INFO: find one variable on which d1 and d2 differs *)
+(** ONLY FOR DEBUGGING INFO: find one variable on which d1 and d2 differs *)
 Fixpoint not_eq_witness {A} (d1 d2: t A): ?? option R.t :=
   match d1, d2 with
   | Leaf _, Leaf _ => RET None