diff options
Diffstat (limited to 'src/rewriter.mli')
| -rw-r--r-- | src/rewriter.mli | 51 |
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 |