From 205fa71046508498526e17a7084f7eb64b381121 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?L=C3=A9onard=20G=C3=A9rard?= <leonard.gerard@ens.fr>
Date: Sun, 15 Aug 2010 20:22:18 +0200
Subject: [PATCH] Automata file cleaned a bit, still needs documentation and
 good comments.

---
 compiler/heptagon/transformations/automata.ml | 85 +++++++++----------
 1 file changed, 40 insertions(+), 45 deletions(-)

diff --git a/compiler/heptagon/transformations/automata.ml b/compiler/heptagon/transformations/automata.ml
index 67ed26a..45fa2d7 100644
--- a/compiler/heptagon/transformations/automata.ml
+++ b/compiler/heptagon/transformations/automata.ml
@@ -50,15 +50,15 @@ let intro_type states =
     (mk_type_dec state_type (Type_enum (list states))) :: !state_type_dec_list;
   Name(state_type)
 
-(* an automaton may be a Moore automaton, i.e., with only weak transitions; *)
-(* a Mealy one, i.e., with only strong transition or mixed *)
-let moore_mealy state_handlers =
-  let handler (moore, mealy) { s_until = l1; s_unless = l2 } =
-    (moore or (l1 <> []), mealy or (l2 <> [])) in
-  List.fold_left handler (false, false) state_handlers
+(** Allows to classify an automaton :
+    Moore automatons doesn't have strong transitions,
+    Mealy automatons may have some. *)
+let no_strong_transition state_handlers =
+  let handler no_strong { s_unless = l } = no_strong & (l = []) in
+  List.fold_left handler true state_handlers
+
 
 let translate_automaton v eq_list handlers =
-  let has_until, has_unless = moore_mealy handlers in
   let states =
     let suffix = gen_symbol () in
     List.fold_left
@@ -116,44 +116,39 @@ let translate_automaton v eq_list handlers =
       (mk_var_dec resetname (Tid Initial.pbool)) ::
       (mk_var_dec next_resetname (Tid Initial.pbool)) ::
       (mk_var_dec pre_next_resetname (Tid Initial.pbool)) :: v in
-  (* we optimise the case of an only strong automaton *)
-  (* or only weak automaton *)
-  match has_until, has_unless with
-    | true, false ->
-        let switch_e = mk_exp_fby_state initial (statevar next_statename) in
-        let switch_handlers = (List.map
-                                 (fun ({ s_state = n } as case) ->
-                                    { w_name = name n; w_block = weak case })
-                                 handlers) in
-        let switch_eq = mk_switch_equation switch_e switch_handlers in
-        let nr_eq = mk_simple_equation (Evarpat pre_next_resetname)
-          (mk_exp_fby_false (boolvar (next_resetname))) in
-        let pnr_eq = mk_simple_equation (Evarpat resetname)
-          (boolvar pre_next_resetname) in
-        (* a Moore automaton with only weak transitions *)
-        v, switch_eq :: nr_eq :: pnr_eq :: eq_list
-    | _ ->
-        (* the general case; two switch to generate,
-           statename variable used and defined *)
-        let v = (mk_var_dec statename (Tid statetype)) :: v in
-
-        let ns_switch_e = mk_exp_fby_state initial (statevar next_statename) in
-        let ns_switch_handlers = List.map
-          (fun ({ s_state = n } as case) ->
-             { w_name = name n; w_block = strong case })
-          handlers in
-        let ns_switch_eq = mk_switch_equation ns_switch_e ns_switch_handlers in
-
-        let switch_e = statevar statename in
-        let switch_handlers = List.map
-          (fun ({ s_state = n } as case) ->
-             { w_name = name n; w_block = weak case })
-          handlers in
-        let switch_eq = mk_switch_equation switch_e switch_handlers in
-
-        let pnr_eq = mk_simple_equation (Evarpat pre_next_resetname)
-          (mk_exp_fby_false (boolvar (next_resetname))) in
-        v, ns_switch_eq :: switch_eq :: pnr_eq :: eq_list
+  if no_strong_transition handlers
+  then (* Only weak transitions : a Moore automaton. *)
+    let switch_e = mk_exp_fby_state initial (statevar next_statename) in
+    let switch_handlers =
+      List.map (fun ({ s_state = n } as case) ->
+                  { w_name = name n; w_block = weak case })
+               handlers in
+    let switch_eq = mk_switch_equation switch_e switch_handlers in
+    let nr_eq =
+      mk_simple_equation (Evarpat pre_next_resetname)
+                         (mk_exp_fby_false (boolvar (next_resetname))) in
+    let pnr_eq =
+      mk_simple_equation (Evarpat resetname) (boolvar pre_next_resetname) in
+    v, switch_eq :: nr_eq :: pnr_eq :: eq_list
+  else (* General case,
+          two switch to generate statename variable used and defined *)
+    let v = (mk_var_dec statename (Tid statetype)) :: v in
+    let ns_switch_e = mk_exp_fby_state initial (statevar next_statename) in
+    let ns_switch_handlers =
+      List.map (fun ({ s_state = n } as case) ->
+                  { w_name = name n; w_block = strong case })
+               handlers in
+    let ns_switch_eq = mk_switch_equation ns_switch_e ns_switch_handlers in
+    let switch_e = statevar statename in
+    let switch_handlers =
+      List.map (fun ({ s_state = n } as case) ->
+                  { w_name = name n; w_block = weak case })
+               handlers in
+    let switch_eq = mk_switch_equation switch_e switch_handlers in
+    let pnr_eq =
+      mk_simple_equation (Evarpat pre_next_resetname)
+                         (mk_exp_fby_false (boolvar (next_resetname))) in
+    v, ns_switch_eq :: switch_eq :: pnr_eq :: eq_list
 
 let rec eq funs (v, eq_list) eq =
   let eq, (v, eq_list) = Hept_mapfold.eq funs (v, eq_list) eq in