diff options
Diffstat (limited to 'src/rewrites.mli')
| -rw-r--r-- | src/rewrites.mli | 18 |
1 files changed, 17 insertions, 1 deletions
diff --git a/src/rewrites.mli b/src/rewrites.mli index 811d52e8..f5b26f3a 100644 --- a/src/rewrites.mli +++ b/src/rewrites.mli @@ -59,7 +59,6 @@ val opt_dmono_analysis : int ref val opt_auto_mono : bool ref val opt_dall_split_errors : bool ref val opt_dmono_continue : bool ref -val opt_separate_execute : bool ref (* Generate a fresh id with the given prefix *) val fresh_id : string -> l -> id @@ -79,6 +78,23 @@ val rewrite_defs_lem : (string * (Env.t -> tannot defs -> tannot defs)) list (* Perform rewrites to exclude AST nodes not supported for coq out*) val rewrite_defs_coq : (string * (Env.t -> tannot defs -> tannot defs)) list +type rewriter = + | Basic_rewriter of (Env.t -> tannot defs -> tannot defs) + | Bool_rewriter of (bool -> rewriter) + | String_rewriter of (string -> rewriter) + | Literal_rewriter of ((lit -> bool) -> rewriter) + +val rewrite_lit_ocaml : lit -> bool +val rewrite_lit_lem : lit -> bool + +type rewriter_arg = + | If_mono_arg + | Bool_arg of bool + | String_arg of string + | Literal_arg of string + +val all_rewrites : (string * rewriter) list + (* Warn about matches where we add a default case for Coq because they're not exhaustive *) val opt_coq_warn_nonexhaustive : bool ref |