diff options
Diffstat (limited to 'src/rewriter.mli')
| -rw-r--r-- | src/rewriter.mli | 93 |
1 files changed, 72 insertions, 21 deletions
diff --git a/src/rewriter.mli b/src/rewriter.mli index 3f57b745..9fa17a53 100644 --- a/src/rewriter.mli +++ b/src/rewriter.mli @@ -50,26 +50,35 @@ open Big_int open Ast -open Type_internal -type typ = Type_internal.t -type 'a exp = 'a Ast.exp -type 'a emap = 'a Envmap.t -type envs = Type_check.envs -type 'a namemap = (typ * 'a exp) emap - -type 'a rewriters = { rewrite_exp : 'a rewriters -> (nexp_map * 'a namemap) option -> 'a exp -> 'a exp; - rewrite_lexp : 'a rewriters -> (nexp_map * 'a namemap) option -> 'a lexp -> 'a lexp; - rewrite_pat : 'a rewriters -> (nexp_map * 'a namemap) option -> 'a pat -> 'a pat; - rewrite_let : 'a rewriters -> (nexp_map * 'a namemap) option -> 'a letbind -> 'a letbind; +open Type_check + +type 'a rewriters = { rewrite_exp : 'a rewriters -> 'a exp -> 'a exp; + rewrite_lexp : 'a rewriters -> 'a lexp -> 'a lexp; + rewrite_pat : 'a rewriters -> 'a pat -> 'a pat; + rewrite_let : 'a rewriters -> 'a letbind -> 'a letbind; rewrite_fun : 'a rewriters -> 'a fundef -> 'a fundef; rewrite_def : 'a rewriters -> 'a def -> 'a def; rewrite_defs : 'a rewriters -> 'a defs -> 'a defs; } - -val rewrite_exp : tannot rewriters -> (nexp_map * tannot namemap) option -> tannot exp -> tannot 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_defs_ocaml : tannot defs -> tannot defs (*Perform rewrites to exclude AST nodes not supported for ocaml out*) -val rewrite_defs_lem : tannot defs -> tannot defs (*Perform rewrites to exclude AST nodes not supported for lem out*) + +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 = @@ -78,21 +87,20 @@ type ('a,'pat,'pat_aux,'fpat,'fpat_aux) pat_alg = ; p_as : 'pat * id -> 'pat_aux ; p_typ : Ast.typ * 'pat -> 'pat_aux ; p_id : id -> 'pat_aux + ; p_var : 'pat * kid -> 'pat_aux ; p_app : id * 'pat list -> 'pat_aux ; p_record : 'fpat list * bool -> 'pat_aux ; p_vector : 'pat list -> 'pat_aux - ; p_vector_indexed : (int * 'pat) list -> 'pat_aux ; p_vector_concat : 'pat list -> 'pat_aux ; p_tup : 'pat list -> 'pat_aux ; p_list : 'pat list -> 'pat_aux + ; p_cons : 'pat * 'pat -> 'pat_aux ; p_aux : 'pat_aux * 'a annot -> 'pat ; 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, @@ -107,8 +115,8 @@ type ('a,'exp,'exp_aux,'lexp,'lexp_aux,'fexp,'fexp_aux,'fexps,'fexps_aux, ; e_tuple : 'exp list -> 'exp_aux ; e_if : 'exp * 'exp * 'exp -> 'exp_aux ; e_for : id * 'exp * 'exp * 'exp * Ast.order * 'exp -> 'exp_aux + ; e_loop : loop * 'exp * 'exp -> 'exp_aux ; e_vector : 'exp list -> 'exp_aux - ; e_vector_indexed : (int * 'exp) list * 'opt_default -> 'exp_aux ; e_vector_access : 'exp * 'exp -> 'exp_aux ; e_vector_subrange : 'exp * 'exp * 'exp -> 'exp_aux ; e_vector_update : 'exp * 'exp * 'exp -> 'exp_aux @@ -122,12 +130,16 @@ type ('a,'exp,'exp_aux,'lexp,'lexp_aux,'fexp,'fexp_aux,'fexps,'fexps_aux, ; e_case : 'exp * 'pexp list -> 'exp_aux ; e_let : 'letbind * 'exp -> 'exp_aux ; e_assign : 'lexp * 'exp -> 'exp_aux + ; e_sizeof : nexp -> 'exp_aux + ; e_constraint : n_constraint -> 'exp_aux ; e_exit : 'exp -> 'exp_aux ; e_return : 'exp -> 'exp_aux ; e_assert : 'exp * 'exp -> 'exp_aux ; e_internal_cast : 'a annot * 'exp -> 'exp_aux ; e_internal_exp : 'a annot -> 'exp_aux ; e_internal_exp_user : 'a annot * 'a annot -> 'exp_aux + ; e_comment : string -> 'exp_aux + ; e_comment_struc : 'exp -> 'exp_aux ; e_internal_let : 'lexp * 'exp * 'exp -> 'exp_aux ; e_internal_plet : 'pat * 'exp * 'exp -> 'exp_aux ; e_internal_return : 'exp -> 'exp_aux @@ -148,17 +160,56 @@ type ('a,'exp,'exp_aux,'lexp,'lexp_aux,'fexp,'fexp_aux,'fexps,'fexps_aux, ; def_val_dec : 'exp -> 'opt_default_aux ; def_val_aux : 'opt_default_aux * 'a annot -> 'opt_default ; pat_exp : 'pat * 'exp -> 'pexp_aux + ; pat_when : 'pat * 'exp * 'exp -> 'pexp_aux ; pat_aux : 'pexp_aux * 'a annot -> 'pexp - ; lB_val_explicit : typschm * 'pat * 'exp -> 'letbind_aux - ; lB_val_implicit : 'pat * 'exp -> 'letbind_aux + ; lB_val : 'pat * 'exp -> 'letbind_aux ; lB_aux : 'letbind_aux * 'a annot -> 'letbind ; pat_alg : ('a,'pat,'pat_aux,'fpat,'fpat_aux) pat_alg } +(* fold over patterns *) +val fold_pat : ('a,'pat,'pat_aux,'fpat,'fpat_aux) pat_alg -> 'a pat -> 'pat + (* fold over expressions *) val fold_exp : ('a,'exp,'exp_aux,'lexp,'lexp_aux,'fexp,'fexp_aux,'fexps,'fexps_aux, 'opt_default_aux,'opt_default,'pexp,'pexp_aux,'letbind_aux,'letbind, 'pat,'pat_aux,'fpat,'fpat_aux) exp_alg -> 'a exp -> 'exp val id_pat_alg : ('a,'a pat, 'a pat_aux, 'a fpat, 'a fpat_aux) pat_alg +val id_exp_alg : + ('a,'a exp,'a exp_aux,'a lexp,'a lexp_aux,'a fexp, + 'a fexp_aux,'a fexps,'a fexps_aux, + 'a opt_default_aux,'a opt_default,'a pexp,'a pexp_aux, + 'a letbind_aux,'a letbind, + 'a pat,'a pat_aux,'a fpat,'a fpat_aux) exp_alg + +val compute_pat_alg : 'b -> ('b -> 'b -> 'b) -> + ('a,('b * 'a pat),('b * 'a pat_aux),('b * 'a fpat),('b * 'a fpat_aux)) pat_alg + +val compute_exp_alg : 'b -> ('b -> 'b -> 'b) -> + ('a,('b * 'a exp),('b * 'a exp_aux),('b * 'a lexp),('b * 'a lexp_aux),('b * 'a fexp), + ('b * 'a fexp_aux),('b * 'a fexps),('b * 'a fexps_aux), + ('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 |