libsail 0.18 (latest) · OCaml Package

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, 'b) Ast_defs.ast -> ('a, 'b) Ast_defs.ast

Move loop termination measures into loop AST nodes

val rewrite_undefined : 
  bool ->
  Type_check.Env.t ->
  Type_check.typed_ast ->
  Type_check.typed_ast

Re-write undefined to functions created by -undefined_gen flag

type rewriter =

| Full_rewriter of Initial_check.ctx -> Effects.side_effect_info -> Type_check.Env.t -> Type_check.typed_ast -> Initial_check.ctx * Type_check.typed_ast * Effects.side_effect_info * Type_check.Env.t
| Bool_rewriter of bool -> rewriter
| String_rewriter of string -> rewriter
| Literal_rewriter of (Ast.lit -> bool) -> rewriter

val describe_rewriter : rewriter -> string list

val all_rewriters : (string * rewriter) list

type rewrite_sequence =
  (string
   * (Initial_check.ctx ->
   Effects.side_effect_info ->
   Type_check.Env.t ->
   Type_check.typed_ast ->
   Initial_check.ctx
   * Type_check.typed_ast
   * Effects.side_effect_info
   * Type_check.Env.t))
    list

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 Stdlib.ref
| Bool_arg of bool
| Flag_arg of bool Stdlib.ref
| String_arg of string
| 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

val rewrite : 
  Initial_check.ctx ->
  Effects.side_effect_info ->
  Type_check.Env.t ->
  rewrite_sequence ->
  Type_check.typed_ast ->
  Initial_check.ctx
  * Type_check.typed_ast
  * Effects.side_effect_info
  * Type_check.Env.t

Apply a sequence of rewrites to an AST

val rewrites_interpreter : (string * rewriter_arg list) list

val simple_typ : Ast.typ -> Ast.typ

package libsail