Merge remote branch 'experiments' into experiments

1 files changed, 44 insertions, 7 deletions

diff --git a/src/rewriter.mli b/src/rewriter.mli
index c107be25..cd293ca5 100644
--- a/src/rewriter.mli
+++ b/src/rewriter.mli
@@ -9,7 +9,14 @@
 (*    Robert Norton-Wright                                                *)
 (*    Christopher Pulte                                                   *)
 (*    Peter Sewell                                                        *)
+(*    Alasdair Armstrong                                                  *)
+(*    Brian Campbell                                                      *)
 (*    Thomas Bauereiss                                                    *)
+(*    Anthony Fox                                                         *)
+(*    Jon French                                                          *)
+(*    Dominic Mulligan                                                    *)
+(*    Stephen Kell                                                        *)
+(*    Mark Wassell                                                        *)
 (*                                                                        *)
 (*  All rights reserved.                                                  *)
 (*                                                                        *)
@@ -55,13 +62,23 @@ type 'a rewriters = { rewrite_exp  : 'a rewriters -> 'a exp -> 'a exp;
                     }
 
 val rewrite_exp : tannot rewriters -> tannot exp -> tannot exp
+
+val rewriters_base : tannot rewriters
+
+(* The identity re-writer *)
 val rewrite_defs : tannot defs -> tannot defs
-val rewrite_undefined : bool -> tannot defs -> tannot defs
-val rewrite_defs_ocaml : (string * (tannot defs -> tannot defs)) list (*Perform rewrites to exclude AST nodes not supported for ocaml out*)
-val rewrite_defs_lem : (string * (tannot defs -> tannot defs)) list (*Perform rewrites to exclude AST nodes not supported for lem out*)
-val rewrite_defs_check : (string * (tannot defs -> tannot defs)) list
 
-val simple_typ : typ -> typ
+val rewrite_defs_base : tannot rewriters -> tannot defs -> tannot defs
+
+val rewrite_lexp : tannot rewriters -> tannot lexp -> tannot lexp
+
+val rewrite_pat : tannot rewriters -> tannot pat -> tannot pat
+
+val rewrite_let : tannot rewriters -> tannot letbind -> tannot letbind
+
+val rewrite_def : tannot rewriters -> tannot def -> tannot def
+
+val rewrite_fun : tannot rewriters -> tannot fundef -> tannot fundef
 
 (* the type of interpretations of pattern-matching expressions *)
 type ('a,'pat,'pat_aux,'fpat,'fpat_aux) pat_alg =
@@ -82,10 +99,8 @@ type ('a,'pat,'pat_aux,'fpat,'fpat_aux) pat_alg =
   ; fP_aux           : 'fpat_aux * 'a annot -> 'fpat
   ; fP_Fpat          : id * 'pat -> 'fpat_aux
   }
-
 (* fold over pat_aux expressions *)
 
-
 (* the type of interpretations of expressions *)
 type ('a,'exp,'exp_aux,'lexp,'lexp_aux,'fexp,'fexp_aux,'fexps,'fexps_aux,
       'opt_default_aux,'opt_default,'pexp,'pexp_aux,'letbind_aux,'letbind,
@@ -118,6 +133,7 @@ type ('a,'exp,'exp_aux,'lexp,'lexp_aux,'fexp,'fexp_aux,'fexps,'fexps_aux,
  ; e_sizeof                 : nexp -> 'exp_aux
  ; e_constraint             : n_constraint -> 'exp_aux
  ; e_exit                   : 'exp -> 'exp_aux
+ ; e_throw                  : 'exp -> 'exp_aux
  ; e_return                 : 'exp -> 'exp_aux
  ; e_assert                 : 'exp * 'exp -> 'exp_aux
  ; e_internal_cast          : 'a annot * 'exp -> 'exp_aux
@@ -177,3 +193,24 @@ val compute_exp_alg : 'b -> ('b -> 'b -> 'b) ->
   ('b * 'a opt_default_aux),('b * 'a opt_default),('b * 'a pexp),('b * 'a pexp_aux),
   ('b * 'a letbind_aux),('b * 'a letbind),
   ('b * 'a pat),('b * 'a pat_aux),('b * 'a fpat),('b * 'a fpat_aux)) exp_alg
+
+val simple_annot : Parse_ast.l -> typ -> Parse_ast.l * tannot
+
+val union_eff_exps : (tannot exp) list -> effect
+
+val fix_eff_exp : tannot exp -> tannot exp
+
+val fix_eff_lexp : tannot lexp -> tannot lexp
+
+val fix_eff_lb : tannot letbind -> tannot letbind
+
+val fix_eff_pexp : tannot pexp -> tannot pexp
+
+val fix_eff_fexp : tannot fexp -> tannot fexp
+
+val fix_eff_fexps : tannot fexps -> tannot fexps
+
+val fix_eff_opt_default : tannot opt_default -> tannot opt_default
+
+(* AA: How this is used in rewrite_pat seems suspect to me *)
+val vector_string_to_bit_list : Parse_ast.l -> lit_aux -> lit list