package sail

  1. Overview
  2. Docs
package sail
Legend:
Library
Module
Module type
Parameter
Class
Class type
val parse_file : ?loc:Parse_ast.l -> string -> Lexer.comment list * Parse_ast.def list
val clear_symbols : unit -> unit
val have_symbol : string -> bool
val add_symbol : string -> unit
val preprocess : (Arg.key * Arg.spec * Arg.doc) list -> Parse_ast.def list -> Parse_ast.def list
val opt_file_out : string option ref
val opt_memo_z3 : bool ref
val opt_just_check : bool ref
val opt_reformat : string option ref
val opt_ddump_initial_ast : bool ref
val opt_ddump_tc_ast : bool ref
val opt_ddump_rewrite_ast : (string * int) option ref
val opt_dno_cast : bool ref
val opt_lem_output_dir : string option ref
val opt_isa_output_dir : string option ref
val opt_coq_output_dir : string option ref
val opt_alt_modules_coq : string list ref
val opt_alt_modules2_coq : string list ref
type out_type =
  1. | Lem_out of string list
  2. | Coq_out of string list
val output : string -> out_type -> (string * Type_check.Env.t * Type_check.tannot Ast_defs.ast) list -> unit
val always_replace_files : bool ref
val load_files : ?check:bool -> (Arg.key * Arg.spec * Arg.doc) list -> Type_check.Env.t -> string list -> string * Type_check.tannot Ast_defs.ast * Type_check.Env.t