Module `Libsail.Rewrites`Source

Sourceval opt_mono_rewrites : bool ref

Sourceval opt_mono_complex_nexps : bool ref

Sourceval opt_mono_split : ((string * int) * string) list ref

Sourceval opt_dmono_analysis : int ref

Sourceval opt_auto_mono : bool ref

Sourceval opt_dall_split_errors : bool ref

Sourceval opt_dmono_continue : bool ref

Sourceval opt_coq_warn_nonexhaustive : bool ref

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

Sourceval opt_ddump_rewrite_ast : (string * int) option ref

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

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

Generate a fresh id with the given prefix

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

Move loop termination measures into loop AST nodes

Source

val rewrite_undefined : 
  bool ->
  Type_check.Env.t ->
  Type_check.tannot Ast_defs.ast ->
  Type_check.tannot Ast_defs.ast

Re-write undefined to functions created by -undefined_gen flag

Sourcetype rewriter =

| 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
| Bool_rewriter of bool -> rewriter
| String_rewriter of string -> rewriter
| Literal_rewriter of (Ast.lit -> bool) -> rewriter

Sourceval describe_rewriter : rewriter -> string list

Sourceval all_rewriters : (string * rewriter) list

Source

type rewrite_sequence =
  (string
   * (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))
    list

Sourceval rewrite_lit_ocaml : Ast.lit -> bool

Sourceval rewrite_lit_lem : Ast.lit -> bool

Sourcetype rewriter_arg =

| If_mono_arg
| If_mwords_arg
| If_flag of bool ref
| Bool_arg of bool
| Flag_arg of bool ref
| String_arg of string
| Literal_arg of string

Source

val instantiate_rewrites : 
  (string * rewriter_arg list) list ->
  rewrite_sequence

Get the list of instantiated rewrites for a list of rewrites

Source

val rewrite : 
  Effects.side_effect_info ->
  Type_check.Env.t ->
  rewrite_sequence ->
  Type_check.tannot Ast_defs.ast ->
  Type_check.tannot Ast_defs.ast * Effects.side_effect_info * Type_check.Env.t

Apply a sequence of rewrites to an AST

Sourceval rewrites_interpreter : (string * rewriter_arg list) list

Sourceval simple_typ : Ast.typ -> Ast.typ

package libsail

Module Libsail.RewritesSource

Module `Libsail.Rewrites`Source