Updates documentations and notations

src/semantics/FPBigStep.v

@@ -117,7 +117,7 @@ Module FP_BIGSTEP (EVAL_Def: EVAL_ENV)
             e
         end
       else
-        (** The function returns true, the stage end *)
+        (** The function returns false, the stage end *)
         (** Break if the option is enabled *)
         let e'' := app_trace e' (init_stage :: nil) in
         if get_call_break params then
@@ -167,7 +167,7 @@ Module FP_BIGSTEP (EVAL_Def: EVAL_ENV)
     (** The stage has a until condition?*)
     match until with
     | Some u =>
-        (** Evaluate the condition ad jump to the next stage
+        (** Evaluate the condition and jump to the next stage
             if the condition is true *)
         let '(b, e) := evalc e u in
         let e' := change_trace e' (get_trace e) in

src/semantics/FPBigStepGeneric.v

@@ -230,7 +230,7 @@ Module COMMON_SEM (G_FP: GENERIC_FP)
       else
         (** Deroute forbidden? *)
         let exec := get_expt_exec ex in
-        let e'' := app_trace e' (fp_exec_to_trace exec) in
+        let e'' := app_trace e' (opt_c_code_to_trace exec) in
         (true, goto_block e'' id).
   
   Fixpoint test_exceptions (e: fp_env) (exs: fp_exceptions):

src/semantics/FPEnvironment.v

@@ -105,14 +105,14 @@ Module FP_ENV (EVAL_Def: EVAL_ENV).
         let new_stages := get_stages fp new_id in
         mk_fp_env new_id new_stages nav_block nav_stages t.
 
-        Definition normalise (fp: flight_plan) (e: fp_env): fp_env :=
-          let nav_block := get_nav_block e in
-          let nav_stages := get_nav_stages e in
-          let last_block := get_last_block e in
-          let last_stages := get_last_stages e in
-          let t := get_trace e in
-          mk_fp_env (normalise_block_id fp nav_block) nav_stages
-                    last_block last_stages t.
+    Definition normalise (fp: flight_plan) (e: fp_env): fp_env :=
+      let nav_block := get_nav_block e in
+      let nav_stages := get_nav_stages e in
+      let last_block := get_last_block e in
+      let last_stages := get_last_stages e in
+      let t := get_trace e in
+      mk_fp_env (normalise_block_id fp nav_block) nav_stages
+                last_block last_stages t.
 
     Definition get_current_block (fp: flight_plan) (e:fp_env): fp_block := 
       (get_block fp (get_nav_block e)).

src/semantics/FPNavigationModeSem.v

@@ -78,7 +78,7 @@ else {
 
 (** Function that return the c_code of the nav_cond if it is possible *)
 
-Definition approaching_time_sem (p: fp_params_go): c_code :=
+Definition approaching_time_sem (p: fp_params_go): c_cond :=
   match get_go_approaching_time p with
   | AT a => a
   | ET e => "-" ++ e

src/syntax/FlightPlanGeneric.v

@@ -79,7 +79,7 @@ Definition mk_fp_pderoute := create_fp_pderoute.
 Definition fp_params_return := bool. (** reset_stage : default value false*)
 
 (** Conversion of a option C code into a trace *)
-Definition fp_exec_to_trace (exec: option c_code): fp_trace :=
+Definition opt_c_code_to_trace (exec: option c_code): fp_trace :=
   match exec with
   | None => nil
   | Some e => (C_CODE e) :: nil
@@ -187,16 +187,16 @@ Module COMMON_FP_FUN (G_FP: GENERIC_FP) <: COMMON_FP_FUN_SIG G_FP.
 
   (** Getter for block params *)
   Definition get_code_block_pre_call (block: fp_block): fp_trace := 
-    fp_exec_to_trace (get_block_pre_call block).
+    opt_c_code_to_trace (get_block_pre_call block).
 
   Definition get_code_block_post_call (block: fp_block): fp_trace := 
-    fp_exec_to_trace (get_block_post_call block).
+    opt_c_code_to_trace (get_block_post_call block).
 
   Definition get_code_on_enter (block: fp_block): fp_trace := 
-    fp_exec_to_trace (get_block_on_enter block).
+    opt_c_code_to_trace (get_block_on_enter block).
 
   Definition get_code_on_exit (block: fp_block): fp_trace := 
-    fp_exec_to_trace (get_block_on_exit block).
+    opt_c_code_to_trace (get_block_on_exit block).
 
   (** Getter for enter/exit code of a block *)
   Definition on_enter (fp: flight_plan) (id: block_id): fp_trace :=

src/verification/ExtractTraceFPEnv.v

@@ -358,7 +358,7 @@ Module EXTRACT_TRACE_FPENV (EVAL_Def: EVAL_ENV)
     apply (trace_appended_trans
       (trace_appended_app_trace e [COND c true])).
     apply (trace_appended_trans
-      (trace_appended_app_trace _ (fp_exec_to_trace code))).
+      (trace_appended_app_trace _ (opt_c_code_to_trace code))).
     apply (trace_appended_trans (extract_goto_block' _ id)).
     apply trace_appended_refl.
 

src/verification/MatchFPSwFPC.v

@@ -386,7 +386,7 @@ Module MATCH_FPS_C (EVAL_Def: EVAL_ENV)
 
   Lemma exec_to_trace_fp_trace:
   forall func,
-    fp_trace_to_trace (fp_exec_to_trace func) = exec_to_trace func.
+    fp_trace_to_trace (opt_c_code_to_trace func) = exec_to_trace func.
   Proof. by destruct func. Qed.
 
   Lemma app_trace_preserve_match:

src/verification/VerifFPToFPE.v

@@ -327,7 +327,7 @@ Module FP_TO_FPE_VERIF (EVAL_Def: EVAL_ENV)
     simpl in Hex.
     destruct (FP_BS.Common_Sem.goto_block _ _ _) as [e'' o''] eqn:Hg;
       symmetry in Hg.
-    remember (fp_exec_to_trace _) as t.
+    remember (opt_c_code_to_trace _) as t.
     have Hg' := match_goto_block (match_app_trace t He2') Hg;
       destruct Hg' as [e2'' [Hg' He2'']]; exists e2''.
       injection Hex as Hres He1'.