package sail

  1. Overview
  2. Docs
val opt_mono_rewrites : bool Stdlib.ref
val opt_mono_complex_nexps : bool Stdlib.ref
val opt_mono_split : ((string * int) * string) list Stdlib.ref
val opt_dmono_analysis : int Stdlib.ref
val opt_auto_mono : bool Stdlib.ref
val opt_dall_split_errors : bool Stdlib.ref
val opt_dmono_continue : bool Stdlib.ref
val fresh_id : string -> Ast.l -> Ast.id
val move_loop_measures : 'a Ast.defs -> 'a Ast.defs
val rewrite_defs_target : string -> (string * (Type_check.Env.t -> Type_check.tannot Ast.defs -> Type_check.tannot Ast.defs * Type_check.Env.t)) list
type rewriter =
  1. | Basic_rewriter of Type_check.Env.t -> Type_check.tannot Ast.defs -> Type_check.tannot Ast.defs
  2. | Checking_rewriter of Type_check.Env.t -> Type_check.tannot Ast.defs -> Type_check.tannot Ast.defs * Type_check.Env.t
  3. | Bool_rewriter of bool -> rewriter
  4. | String_rewriter of string -> rewriter
  5. | Literal_rewriter of (Ast.lit -> bool) -> rewriter
val rewrite_lit_ocaml : Ast.lit -> bool
val rewrite_lit_lem : Ast.lit -> bool
type rewriter_arg =
  1. | If_mono_arg
  2. | If_mwords_arg
  3. | Bool_arg of bool
  4. | String_arg of string
  5. | Literal_arg of string
val all_rewrites : (string * rewriter) list
val opt_coq_warn_nonexhaustive : bool Stdlib.ref
val rewrite_defs_check : (string * (Type_check.Env.t -> Type_check.tannot Ast.defs -> Type_check.tannot Ast.defs * Type_check.Env.t)) list
val simple_typ : Ast.typ -> Ast.typ
OCaml

Innovation. Community. Security.