package libsail

  1. Overview
  2. Docs
package libsail
Legend:
Library
Module
Module type
Parameter
Class
Class type
module Big_int = Nat_big_num
val opt_tc_debug : int Stdlib.ref
val depth : int Stdlib.ref
val indent : int -> string
val typ_debug : ?level:int -> string Stdlib.Lazy.t -> unit
val typ_print : string Stdlib.Lazy.t -> unit
val adding : string
type constraint_reason = (Ast.l * string) option
type type_variables = {
  1. vars : (Ast.l * Ast.kind_aux) Ast_util.KBindings.t;
  2. shadows : int Ast_util.KBindings.t;
}
type type_error =
  1. | Err_no_casts of Ast_util.uannot Ast.exp * Ast.typ * Ast.typ * type_error * type_error list
  2. | Err_no_overloading of Ast.id * (Ast.id * type_error) list
  3. | Err_unresolved_quants of Ast.id * Ast.quant_item list * (Ast_util.mut * Ast.typ) Ast_util.Bindings.t * type_variables * Ast.n_constraint list
  4. | Err_failed_constraint of Ast.n_constraint * (Ast_util.mut * Ast.typ) Ast_util.Bindings.t * type_variables * Ast.n_constraint list
  5. | Err_subtype of Ast.typ * Ast.typ * Ast.n_constraint option * (constraint_reason * Ast.n_constraint) list * type_variables
  6. | Err_no_num_ident of Ast.id
  7. | Err_other of string
  8. | Err_inner of type_error * Parse_ast.l * string * string option * type_error
val err_because : (type_error * Parse_ast.l * type_error) -> type_error
exception Type_error of Ast.l * type_error
val typ_error : Ast.l -> string -> 'a
val typ_raise : Ast.l -> type_error -> 'a
val string_of_bind : (Ast.typquant * Ast.typ) -> string
val unloc_id : Ast.id -> Ast.id
val unloc_kid : Ast.kid -> Ast.kid
val unloc_nexp_aux : Ast.nexp_aux -> Ast.nexp_aux
val unloc_nexp : Ast.nexp -> Ast.nexp
val unloc_n_constraint_aux : Ast.n_constraint_aux -> Ast.n_constraint_aux
val unloc_n_constraint : Ast.n_constraint -> Ast.n_constraint
val unloc_typ_arg : Ast.typ_arg -> Ast.typ_arg
val unloc_typ_arg_aux : Ast.typ_arg_aux -> Ast.typ_arg_aux
val unloc_typ_aux : Ast.typ_aux -> Ast.typ_aux
val unloc_typ : Ast.typ -> Ast.typ
val unloc_typq : Ast.typquant -> Ast.typquant
val unloc_typq_aux : Ast.typquant_aux -> Ast.typquant_aux
val unloc_quant_item : Ast.quant_item -> Ast.quant_item
val unloc_kinded_id : Ast.kinded_id -> Ast.kinded_id
val unloc_kinded_id_aux : Ast.kinded_id_aux -> Ast.kinded_id_aux
val unloc_kind : Ast.kind -> Ast.kind
val typ_nexps : Ast.typ -> Ast.nexp list
val typ_arg_nexps : Ast.typ_arg -> Ast.nexp list
val constraint_nexps : Ast.n_constraint -> Ast.nexp list
val nexp_power_variables : Ast.nexp -> Ast_util.KidSet.t
val constraint_power_variables : Ast.n_constraint -> Ast_util.KidSet.t
val ex_counter : int Stdlib.ref
val fresh_existential : Ast.l -> Ast.kind_aux -> Ast.kinded_id
val named_existential : Ast.l -> Ast.kind_aux -> string option -> Ast.kinded_id
val destruct_exist_plain : ?name:string option -> Ast.typ -> (Ast.kinded_id list * Ast.n_constraint * Ast.typ) option
val destruct_numeric : ?name:string option -> Ast.typ -> (Ast.kid list * Ast.n_constraint * Ast.nexp) option

Destructure and canonicalise a numeric type into a list of type variables, a constraint on those type variables, and an N-expression that represents that numeric type in the environment. For example:

  • 'n, 'n <= 10. atom('n) => 'n, 'n <= 10, 'n
  • int => 'n, true, 'n (where x is fresh)
  • atom('n) => , true, 'n *
val destruct_boolean : ?name:'a option -> Ast.typ -> (Ast.kid * Ast.n_constraint) option
val destruct_exist : ?name:string option -> Ast.typ -> (Ast.kinded_id list * Ast.n_constraint * Ast.typ) option