sail

Sail is a language for describing the instruction semantics of processors
IN THIS PACKAGE
Module Rewrites
val opt_mono_rewrites : bool ref
val opt_mono_complex_nexps : bool ref
val opt_mono_split : ((string * int) * string) list ref
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 fresh_id : string -> Ast.l -> Ast.id
val move_loop_measures : 'a Ast_defs.ast -> 'a Ast_defs.ast
val rewrite_ast_target : string -> (string * ( Type_check.Env.t -> Type_check.tannot Ast_defs.ast -> Type_check.tannot Ast_defs.ast * Type_check.Env.t )) list
type rewriter =
| Basic_rewriter of Type_check.Env.t -> Type_check.tannot Ast_defs.ast -> Type_check.tannot Ast_defs.ast
| Checking_rewriter of Type_check.Env.t -> Type_check.tannot Ast_defs.ast -> Type_check.tannot Ast_defs.ast * Type_check.Env.t
| Bool_rewriter of bool -> rewriter
| String_rewriter of string -> rewriter
| Literal_rewriter of ( Ast.lit -> bool ) -> rewriter
val rewrite_lit_ocaml : Ast.lit -> bool
val rewrite_lit_lem : Ast.lit -> bool
type rewriter_arg =
| If_mono_arg
| If_mwords_arg
| If_flag of bool ref
| Bool_arg of bool
| String_arg of string
| Literal_arg of string
val all_rewrites : (string * rewriter) list
val opt_coq_warn_nonexhaustive : bool ref
val simple_typ : Ast.typ -> Ast.typ