package libsail

  1. Overview
  2. Docs
package libsail
Legend:
Library
Module
Module type
Parameter
Class
Class type
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 opt_coq_warn_nonexhaustive : bool Stdlib.ref

Warn about matches where we add a default case for Coq because they're not exhaustive

val opt_ddump_rewrite_ast : (string * int) option Stdlib.ref

Output each rewrite step (as produced by the rewrite function) to a file for debugging

val fresh_id : string -> Ast.l -> Ast.id

Generate a fresh id with the given prefix

val move_loop_measures : 'a Ast_defs.ast -> 'a Ast_defs.ast

Move loop termination measures into loop AST nodes

Re-write undefined to functions created by -undefined_gen flag

type rewriter =
  1. | Base_rewriter of Effects.side_effect_info -> Type_check.Env.t -> Type_check.tannot Ast_defs.ast -> Type_check.tannot Ast_defs.ast * Effects.side_effect_info * Type_check.Env.t
  2. | Bool_rewriter of bool -> rewriter
  3. | String_rewriter of string -> rewriter
  4. | Literal_rewriter of (Ast.lit -> bool) -> rewriter
val describe_rewriter : rewriter -> string list
val all_rewriters : (string * rewriter) list
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. | If_flag of bool Stdlib.ref
  4. | Bool_arg of bool
  5. | Flag_arg of bool Stdlib.ref
  6. | String_arg of string
  7. | Literal_arg of string
val instantiate_rewrites : (string * rewriter_arg list) list -> rewrite_sequence

Get the list of instantiated rewrites for a list of rewrites

Apply a sequence of rewrites to an AST

val rewrites_interpreter : (string * rewriter_arg list) list
val simple_typ : Ast.typ -> Ast.typ