From 000dc91d690701c4d641727c4c4a384b2a54ebe8 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?L=C3=A9onard=20G=C3=A9rard?= <leonard.gerard@ens.fr>
Date: Thu, 8 Jul 2010 17:41:00 +0200
Subject: [PATCH] Heptagon and Types mapfold.

---
 compiler/global/types.ml          |  55 +++++++
 compiler/heptagon/hept_mapfold.ml | 264 ++++++++++++++++++++++++++++++
 compiler/heptagon/hept_mapred.ml  | 149 -----------------
 compiler/utilities/misc.ml        |   8 +
 compiler/utilities/misc.mli       |   7 +
 5 files changed, 334 insertions(+), 149 deletions(-)
 create mode 100644 compiler/heptagon/hept_mapfold.ml
 delete mode 100644 compiler/heptagon/hept_mapred.ml

diff --git a/compiler/global/types.ml b/compiler/global/types.ml
index e14d669..45940d0 100644
--- a/compiler/global/types.ml
+++ b/compiler/global/types.ml
@@ -8,6 +8,7 @@
 (**************************************************************************)
 
 open Names
+open Misc
 open Location
 
 type static_exp = { se_desc: static_exp_desc; se_ty: ty; se_loc: location }
@@ -31,6 +32,60 @@ let invalid_type = Tprod []
 let mk_static_exp ?(loc = no_location) ?(ty = invalid_type) desc =
   { se_desc = desc; se_ty = ty; se_loc = loc }
 
+
+(**Iterators*)
+
+type 'a types_it_funs = {
+  static_exp : 'a types_it_funs -> 'a -> static_exp -> static_exp * 'a;
+  static_exp_desc :
+    'a types_it_funs -> 'a -> static_exp_desc -> static_exp_desc * 'a;
+  ty : 'a types_it_funs -> 'a -> ty -> ty * 'a }
+
+let rec static_exp_it funs acc se = funs.static_exp funs acc se
+and static_exp funs acc se =
+  let se_desc, acc = static_exp_desc_it funs acc se.se_desc in
+  let se_ty, acc = ty_it funs acc se.se_ty in
+  { se with se_desc = se_desc; se_ty = se_ty }, acc
+
+and static_exp_desc_it funs acc sd =
+  try funs.static_exp_desc funs acc sd
+  with Fallback -> static_exp_desc funs acc sd
+
+and static_exp_desc funs acc sd = match sd with
+  | Svar _ | Sint _ | Sfloat _ | Sbool _ | Sconstructor _ -> sd, acc
+  | Stuple se_l ->
+      let se_l, acc = mapfold (static_exp_it funs) acc se_l in
+      Stuple se_l, acc
+  | Sarray se_l ->
+      let se_l, acc = mapfold (static_exp_it funs) acc se_l in
+      Sarray se_l, acc
+  | Sop (n, se_l) ->
+      let se_l, acc = mapfold (static_exp_it funs) acc se_l in
+      Sop (n, se_l), acc
+  | Sarray_power (se1, se2) ->
+      let se1, acc = static_exp_it funs acc se1 in
+      let se2, acc = static_exp_it funs acc se2 in
+      Sarray_power(se1, se2), acc
+  | Srecord f_se_l ->
+      let aux acc (f,se) = let se,acc = static_exp_it funs acc se in
+        (f, se), acc in
+      let f_se_l, acc = mapfold aux acc f_se_l in
+      Srecord f_se_l, acc
+
+and ty_it funs acc t = try funs.ty funs acc t with Fallback -> ty funs acc t
+and ty funs acc t = match t with
+  | Tid _ -> t, acc
+  | Tprod t_l -> let t_l, acc = mapfold (ty_it funs) acc t_l in Tprod t_l, acc
+  | Tarray (t, se) ->
+      let t, acc = ty_it funs acc t in
+      let se, acc = static_exp_it funs acc se in
+      Tarray (t, se), acc
+
+let types_funs_default = {
+  static_exp = static_exp;
+  static_exp_desc = static_exp_desc;
+  ty = ty }
+
 open Pp_tools
 open Format
 
diff --git a/compiler/heptagon/hept_mapfold.ml b/compiler/heptagon/hept_mapfold.ml
new file mode 100644
index 0000000..c89d33c
--- /dev/null
+++ b/compiler/heptagon/hept_mapfold.ml
@@ -0,0 +1,264 @@
+ (**************************************************************************)
+(*                                                                        *)
+(*  Heptagon                                                              *)
+(*                                                                        *)
+(*  Author : Marc Pouzet                                                  *)
+(*  Organization : Demons, LRI, University of Paris-Sud, Orsay            *)
+(*                                                                        *)
+(**************************************************************************)
+(* Generic mapred over Heptagon Ast *)
+
+
+(* /!\ do never, never put in your funs record one
+  of the generic iterator function (_omega),
+  either yours either the _default version *)
+
+
+open Misc
+open Types
+open Heptagon
+
+
+type 'a hept_it_funs = {
+  app: 'a hept_it_funs -> 'a -> Heptagon.app -> Heptagon.app * 'a;
+  block: 'a hept_it_funs -> 'a -> Heptagon.block -> Heptagon.block * 'a;
+  edesc: 'a hept_it_funs -> 'a -> Heptagon.desc -> Heptagon.desc * 'a;
+  eq: 'a hept_it_funs -> 'a -> Heptagon.eq -> Heptagon.eq * 'a;
+  eqdesc: 'a hept_it_funs -> 'a -> Heptagon.eqdesc -> Heptagon.eqdesc * 'a;
+  escape_unless :
+    'a hept_it_funs -> 'a -> Heptagon.escape -> Heptagon.escape * 'a;
+  escape_until:
+    'a hept_it_funs -> 'a -> Heptagon.escape -> Heptagon.escape * 'a;
+  exp: 'a hept_it_funs -> 'a -> Heptagon.exp -> Heptagon.exp * 'a;
+  pat: 'a hept_it_funs -> 'a -> pat -> Heptagon.pat * 'a;
+  present_handler:
+    'a hept_it_funs -> 'a -> Heptagon.present_handler
+                          -> Heptagon.present_handler * 'a;
+  state_handler:
+    'a hept_it_funs -> 'a -> Heptagon.state_handler
+                          -> Heptagon.state_handler * 'a;
+  switch_handler:
+    'a hept_it_funs -> 'a -> Heptagon.switch_handler
+                          -> Heptagon.switch_handler * 'a;
+  var_dec: 'a hept_it_funs -> 'a -> Heptagon.var_dec -> Heptagon.var_dec * 'a;
+  last: 'a hept_it_funs -> 'a -> Heptagon.last -> Heptagon.last * 'a;
+  contract:
+    'a hept_it_funs -> 'a -> Heptagon.contract -> Heptagon.contract * 'a;
+  node_dec:
+    'a hept_it_funs -> 'a -> Heptagon.node_dec -> Heptagon.node_dec * 'a;
+  const_dec:
+    'a hept_it_funs -> 'a -> Heptagon.const_dec -> Heptagon.const_dec * 'a;
+  program:
+    'a hept_it_funs -> 'a -> Heptagon.program -> Heptagon.program * 'a;
+  ty_funs: 'a Types.types_it_funs }
+
+
+let rec exp_it funs acc e = funs.exp funs acc e
+and exp funs acc e =
+  let ed, acc = edesc_it funs acc e.e_desc in
+  { e with e_desc = ed }, acc
+
+
+and edesc_it funs acc ed =
+  try funs.edesc funs acc ed
+  with Fallback -> edesc funs acc ed
+and edesc funs acc ed = match ed with
+  | Econst se ->
+      let se, acc = static_exp_it funs.ty_funs acc se in
+      Econst se, acc
+  | Evar _ | Elast _ -> ed, acc
+  | Epre (se, e) ->
+      let se, acc = optional_wacc (static_exp_it funs.ty_funs) acc se in
+      let e, acc = exp_it funs acc e in
+      Epre (se, e), acc
+  | Epre (Some se, e) ->
+      let se, acc = static_exp_it funs.ty_funs acc se in
+      let e, acc = exp_it funs acc e in
+      Epre (Some se, e), acc
+  | Efby (e1, e2) ->
+      let e1, acc = exp_it funs acc e1 in
+      let e2, acc = exp_it funs acc e2 in
+      Efby (e1,e2), acc
+  | Efield (e, n) ->
+      let e, acc = exp_it funs acc e in
+      Efield(e, n), acc
+  | Estruct n_e_list ->
+      let aux acc (n,e) =
+        let e, acc = exp_it funs acc e in
+        (n,e), acc in
+      let n_e_list, acc = mapfold aux acc n_e_list in
+      Estruct n_e_list, acc
+  | Eapp (app, args, reset) ->
+      let app, acc = app_it funs acc app in
+      let args, acc = mapfold (exp_it funs) acc args in
+      let reset, acc = optional_wacc (exp_it funs) acc reset in
+      Eapp (app, args, reset), acc
+  | Eiterator (i, app, param, args, reset) ->
+      let app, acc = app_it funs acc app in
+      let param, acc = static_exp_it funs.ty_funs acc param in
+      let args, acc = mapfold (exp_it funs) acc args in
+      let reset, acc = optional_wacc (exp_it funs) acc reset in
+      Eiterator (i, app, param, args, reset), acc
+
+
+and app_it funs acc a = funs.app funs acc a
+and app funs acc a =
+  let p, acc = mapfold (static_exp_it funs.ty_funs) acc a.a_params in
+  { a with a_params = p }, acc
+
+
+and pat_it funs acc p =
+  try funs.pat funs acc p
+  with Fallback -> pat funs acc p
+and pat funs acc p = match p with
+  | Etuplepat pl ->
+      let pl, acc = mapfold (pat_it funs) acc pl in
+      Etuplepat pl, acc
+  | Evarpat _ -> p, acc
+
+
+and eq_it funs acc eq = funs.eq funs acc eq
+and eq funs acc eq =
+  let eqdesc, acc = eqdesc_it funs acc eq.eq_desc in
+  { eq with eq_desc = eqdesc }, acc
+
+
+and eqdesc_it funs acc eqd =
+  try funs.eqdesc funs acc eqd
+  with Fallback -> eqdesc funs acc eqd
+and eqdesc funs acc eqd = match eqd with
+  | Eautomaton st_h_l ->
+      let st_h_l, acc = mapfold (state_handler_it funs) acc st_h_l in
+      Eautomaton st_h_l, acc
+  | Eswitch (e, sw_h_l) ->
+      let e, acc = exp_it funs acc e in
+      let sw_h_l, acc = mapfold (switch_handler_it funs) acc sw_h_l in
+      Eswitch (e, sw_h_l), acc
+  | Epresent (p_h_l, b) ->
+      let p_h_l, acc = mapfold (present_handler_it funs) acc p_h_l in
+      let b, acc = block_it funs acc b in
+      Epresent (p_h_l, b), acc
+  | Ereset (eq_l, e) ->
+      let eq_l, acc = mapfold (eq_it funs) acc eq_l in
+      let e, acc = exp_it funs acc e in
+      Ereset (eq_l, e), acc
+  | Eeq (p, e) ->
+      let p, acc = pat_it funs acc p in
+      let e, acc = exp_it funs acc e in
+      Eeq (p, e), acc
+
+
+and block_it funs acc b = funs.block funs acc b
+and block funs acc b =
+  let b_local, acc = mapfold (var_dec_it funs) acc b.b_local in
+  let b_equs, acc = mapfold (eq_it funs) acc b.b_equs in
+  { b with b_local = b_local; b_equs = b_equs }, acc
+
+
+and state_handler_it funs acc s = funs.state_handler funs acc s
+and state_handler funs acc s =
+  let s_unless, acc = mapfold (escape_unless_it funs) acc s.s_unless in
+  let s_block, acc = block_it funs acc s.s_block in
+  let s_until, acc = mapfold (escape_until_it funs) acc s.s_until in
+  { s with s_block = s_block; s_until = s_until; s_unless = s_unless }, acc
+
+
+(** escape is a generic function to deal with the automaton state escapes,
+    still the iterator function record differentiate until and unless
+    with escape_until_it and escape_unless_it *)
+and escape_unless_it funs acc esc = funs.escape_unless funs acc esc
+and escape_until_it funs acc esc = funs.escape_until funs acc esc
+and escape funs acc esc =
+  let e_cond, acc = exp_it funs acc esc.e_cond in
+  { esc with e_cond = e_cond }, acc
+
+
+and switch_handler_it funs acc sw = funs.switch_handler funs acc sw
+and switch_handler funs acc sw =
+  let w_block, acc = block_it funs acc sw.w_block in
+  { sw with w_block = w_block }, acc
+
+
+and present_handler_it funs acc ph = funs.present_handler funs acc ph
+and present_handler funs acc ph =
+  let p_cond, acc = exp_it funs acc ph.p_cond in
+  let p_block, acc = block_it funs acc ph.p_block in
+  { ph with p_cond = p_cond; p_block = p_block }, acc
+
+and var_dec_it funs acc vd = funs.var_dec funs acc vd
+and var_dec funs acc vd =
+  let v_last, acc = last_it funs acc vd.v_last in
+  { vd with v_last = v_last }, acc
+
+
+and last_it funs acc l =
+  try funs.last funs acc l
+  with Fallback -> last funs acc l
+and last funs acc l = match l with
+  | Var -> l, acc
+  | Last sto ->
+      let sto, acc = optional_wacc (static_exp_it funs.ty_funs) acc sto in
+      Last sto, acc
+
+
+and contract_it funs acc c = funs.contract funs acc c
+and contract funs acc c =
+  let c_assume, acc = exp_it funs acc c.c_assume in
+  let c_enforce, acc = exp_it funs acc c.c_enforce in
+  let c_local, acc = mapfold (var_dec_it funs) acc c.c_local in
+  let c_eq, acc = mapfold (eq_it funs) acc c.c_eq in
+  { c with
+    c_assume = c_assume; c_enforce = c_enforce; c_local = c_local; c_eq = c_eq }
+  , acc
+
+
+and node_dec_it funs acc nd = funs.node_dec funs acc nd
+and node_dec funs acc nd =
+  let n_input, acc = mapfold (var_dec_it funs) acc nd.n_input in
+  let n_output, acc = mapfold (var_dec_it funs) acc nd.n_output in
+  let n_local, acc = mapfold (var_dec_it funs) acc nd.n_local in
+  let n_equs, acc = mapfold (eq_it funs) acc nd.n_equs in
+  { nd with
+    n_input = n_input; n_output = n_output; n_local = n_local; n_equs = n_equs }
+  , acc
+
+
+
+and const_dec_it funs acc c = funs.const_dec funs acc c
+and const_dec funs acc c =
+  let se, acc = static_exp_it funs.ty_funs acc c.c_value in
+  { c with c_value = se }, acc
+
+and program_it funs acc p = funs.program funs acc p
+and program funs acc p =
+  let cd_list, acc = mapfold (const_dec_it funs) acc p.p_consts in
+  let nd_list, acc = mapfold (node_dec_it funs) acc p.p_nodes in
+  { p with p_consts = cd_list; p_nodes = nd_list }, acc
+
+let hept_funs_default = {
+  app = app;
+  block = block;
+  edesc = edesc;
+  eq = eq;
+  eqdesc = eqdesc;
+  escape_unless = escape;
+  escape_until = escape;
+  exp = exp;
+  pat = pat;
+  present_handler = present_handler;
+  state_handler = state_handler;
+  switch_handler = switch_handler;
+  var_dec = var_dec;
+  last = last;
+  contract = contract;
+  node_dec = node_dec;
+  const_dec = const_dec;
+  program = program;
+  ty_funs = Types.types_funs_default }
+
+
+
+
+
+
+
diff --git a/compiler/heptagon/hept_mapred.ml b/compiler/heptagon/hept_mapred.ml
deleted file mode 100644
index 0887222..0000000
--- a/compiler/heptagon/hept_mapred.ml
+++ /dev/null
@@ -1,149 +0,0 @@
- (**************************************************************************)
-(*                                                                        *)
-(*  Heptagon                                                              *)
-(*                                                                        *)
-(*  Author : Marc Pouzet                                                  *)
-(*  Organization : Demons, LRI, University of Paris-Sud, Orsay            *)
-(*                                                                        *)
-(**************************************************************************)
-(* Generic mapred over Heptagon Ast *)
-
-open Misc
-open Heptagon
-
-exception Fall_back
-
-type exp = { e_desc : edesc }
-
-and edesc =
-  | Econst of static_exp
-  | Evar of var_ident
-  | Elast of var_ident
-  | Epre of static_exp option * exp
-  | Efby of exp * exp
-  | Efield of exp * field_name
-  | Estruct of (field_name * exp) list
-  | Eapp of app * exp list * exp option
-  | Eiterator of iterator_type * app * static_exp * exp list * exp option
-
-
-
-let exp_it funs acc e =
-  let ed, acc = funs.edesc_it funs acc e.edesc in
-  { e with e_desc = ed }, acc
-
-let edesc_it_default funs acc ed = match ed with
-  | Econst se -> let se, acc = funs.static_exp_it funs acc se in Econst se, acc
-  | Evar _ | Elast _ -> ed, acc
-  | Epre (None, e) -> let e, acc = funs.exp_it funs acc e in Epre (None, e), acc
-  | Epre (Some se, e) ->
-      let se, acc = funs.static_exp_it funs acc se in
-      let e, acc = funs.exp_it funs acc e in Epre (Some se, e), acc
-  | Efby (e1, e2) ->
-      let e1, acc = funs.exp_it funs acc e1 in
-      let e2, acc = funs.exp_it funs acc e2 in Efby (e1,e2), acc
-  | Efby of exp * exp
-  | Efield of exp * field_name
-  | Estruct of (field_name * exp) list
-  | Eapp of app * exp list * exp option
-  | Eiterator of iterator_type * app * static_exp * exp list * exp option
-
-let edesc_it funs acc e =
-  try funs.edesc_it funs acc e
-  with Fall_back -> edesc_it_default funs acc e
-
-
-
-
-(** const_dec : traverse static_exps *)
-let const_it funs acc c =
-  let se, acc = funs.static_exp_it funs acc c.c_value in
-  { c with c_value = se }, acc
-
-
-
-and app = { a_op: op; a_params: static_exp list; a_unsafe: bool }
-
-and pat =
-  | Etuplepat of pat list
-  | Evarpat of var_ident
-
-type eq = { eq_desc : eqdesc; eq_statefull : bool; eq_loc : location }
-
-and eqdesc =
-  | Eautomaton of state_handler list
-  | Eswitch of exp * switch_handler list
-  | Epresent of present_handler list * block
-  | Ereset of eq list * exp
-  | Eeq of pat * exp
-
-and block = {
-  b_local : var_dec list;
-  b_equs : eq list;
-  mutable b_defnames : ty Env.t;
-  mutable b_statefull : bool;
-  b_loc : location }
-
-and state_handler = {
-  s_state : state_name;
-  s_block : block;
-  s_until : escape list;
-  s_unless : escape list }
-
-and escape = {
-  e_cond : exp;
-  e_reset : bool;
-  e_next_state : state_name }
-
-and switch_handler = { w_name : constructor_name; w_block : block }
-
-and present_handler = { p_cond : exp; p_block : block }
-
-and var_dec = {
-  v_ident : var_ident;
-  mutable v_type : ty;
-  v_last : last;
-  v_loc : location }
-
-and last = Var | Last of static_exp option
-
-
-type contract = {
-  c_assume : exp;
-  c_enforce : exp;
-  c_local : var_dec list;
-  c_eq : eq list }
-
-type node_dec = {
-  n_input : var_dec list;
-  n_output : var_dec list;
-  n_local : var_dec list;
-  n_equs : eq list }
-
-
-
-
-
-
-(** const_dec : traverse static_exps *)
-let const_it funs acc c =
-  let se, acc = funs.static_exp_it funs acc c.c_value in
-  { c with c_value = se }, acc
-
-(** program : traverse const_dec chained to node_dec *)
-let program_it funs acc p =
-  let cd_list, acc = mapfold (funs.const_it funs) acc p.p_consts in
-  let nd_list, acc = mapfold (funs.node_it funs) acc p.p_nodes in
-  { p with p_consts = cd_list; p_nodes = nd_list }, acc
-
-
-let hept_mapfolds = { program_it .... }
-
-
-
-
-
-
-
-
-
diff --git a/compiler/utilities/misc.ml b/compiler/utilities/misc.ml
index de3e35b..1711454 100644
--- a/compiler/utilities/misc.ml
+++ b/compiler/utilities/misc.ml
@@ -100,6 +100,10 @@ let optional f = function
   | None -> None
   | Some x -> Some (f x)
 
+let optional_wacc f acc = function
+  | None -> None, acc
+  | Some x -> let x, acc = f acc x in Some x, acc
+
 let optunit f = function
   | None -> ()
   | Some x -> f x
@@ -193,6 +197,10 @@ let rec assocd value = function
       else
         assocd value l
 
+
+(** Compiler iterators *)
+exception Fallback
+
 (** Mapfold *)
 let mapfold f acc l =
   let l,acc = List.fold_left (fun (l,acc) e -> let e,acc = f acc e in e::l, acc)
diff --git a/compiler/utilities/misc.mli b/compiler/utilities/misc.mli
index 9b22ff9..dc7691c 100644
--- a/compiler/utilities/misc.mli
+++ b/compiler/utilities/misc.mli
@@ -106,6 +106,8 @@ val use_new_reset_encoding : bool ref
 
 (* Misc. functions *)
 val optional : ('a -> 'b) -> 'a option -> 'b option
+(** Optional with accumulator *)
+val optional_wacc : ('a -> 'b -> 'c*'a) -> 'a -> 'b option -> ('c option * 'a)
 val optunit : ('a -> unit) -> 'a option -> unit
 val split_string : string -> char -> string list
 
@@ -153,5 +155,10 @@ val memd_assoc : 'b -> ('a * 'b) list -> bool
 (** Same as List.assoc but searching for a data and returning the key. *)
 val assocd: 'b -> ('a * 'b) list -> 'a
 
+
+(** Ast iterators *)
+exception Fallback
+
+
 (** Mapfold *)
 val mapfold: ('a -> 'b -> 'c * 'a) -> 'a -> 'b list -> 'c list * 'a
\ No newline at end of file