package libsail

  1. Overview
  2. Docs

Module Libsail.Type_internalSource

module Big_int = Nat_big_num
Sourceval opt_tc_debug : int ref
Sourceval depth : int ref
Sourceval indent : int -> string
Sourceval typ_debug : ?level:??? -> string Lazy.t -> unit
Sourceval typ_print : string Lazy.t -> unit
Sourceval adding : string
Sourcetype constraint_reason = (Ast.l * string) option
Sourcetype type_var_origin =
  1. | Normal
  2. | Outcome
Sourcetype type_variables = {
  1. vars : (Ast.l * Ast.kind_aux * type_var_origin) Ast_compare.KBindings.t;
  2. shadows : int Ast_compare.KBindings.t;
}
Sourcetype type_error =
  1. | Err_no_overloading of Ast.id * (Ast.id * Parse_ast.l * type_error) list
  2. | Err_unresolved_quants of Ast.id * Ast.quant_item list * (Ast_util.mut * Ast.typ) Ast_compare.Bindings.t * type_variables * Ast.n_constraint list
  3. | Err_failed_constraint of Ast.n_constraint * Parse_ast.l list * (Ast_util.mut * Ast.typ) Ast_compare.Bindings.t * type_variables * Ast.n_constraint list
  4. | Err_subtype of Ast.typ * Ast.typ * Ast.n_constraint option * (constraint_reason * Ast.n_constraint) list * type_variables
  5. | Err_no_num_ident of Ast.id
  6. | Err_other of string
  7. | Err_inner of type_error * Parse_ast.l * string * type_error
  8. | Err_not_in_scope of string option * Parse_ast.l option * string Project.spanned option * string Project.spanned option * bool * bool
  9. | Err_instantiation_info of int * type_error
  10. | Err_function_arg of Parse_ast.l * Ast.typ * type_error
  11. | Err_no_function_type of {
    1. id : Ast.id;
    2. functions : (Ast.typquant * Ast.typ) Ast_compare.Bindings.t;
    }
  12. | Err_unbound_id of {
    1. id : Ast.id;
    2. locals : (Ast_util.mut * Ast.typ) Ast_compare.Bindings.t;
    3. have_function : bool;
    }
  13. | Err_vector_subrange of {
    1. n : Big_int.num;
    2. m : Big_int.num;
    3. order : Ast.order;
    }
  14. | Err_hint of string
  15. | Err_with_hint of string * type_error
  16. | Err_alternate of type_error * (string * Parse_ast.l * type_error) list
Sourceexception Type_error of Ast.l * type_error
Sourceval typ_error : Ast.l -> string -> 'a
Sourceval typ_raise : Ast.l -> type_error -> 'a
Sourceval string_of_bind : (Ast.typquant * Ast.typ) -> string
Sourceval unloc_id : Ast.id -> Ast.id
Sourceval unloc_kid : Ast.kid -> Ast.kid
Sourceval unloc_nexp_aux : Ast.nexp_aux -> Ast.nexp_aux
Sourceval unloc_nexp : Ast.nexp -> Ast.nexp
Sourceval unloc_n_constraint_aux : Ast.n_constraint_aux -> Ast.n_constraint_aux
Sourceval unloc_n_constraint : Ast.n_constraint -> Ast.n_constraint
Sourceval unloc_typ_arg : Ast.typ_arg -> Ast.typ_arg
Sourceval unloc_typ_arg_aux : Ast.typ_arg_aux -> Ast.typ_arg_aux
Sourceval unloc_typ_aux : Ast.typ_aux -> Ast.typ_aux
Sourceval unloc_typ : Ast.typ -> Ast.typ
Sourceval unloc_typq : Ast.quant_item list -> Ast.quant_item list
Sourceval unloc_quant_item : Ast.quant_item -> Ast.quant_item
Sourceval unloc_kinded_id : Ast.kinded_id -> Ast.kinded_id
Sourceval unloc_kinded_id_aux : Ast.kinded_id_aux -> Ast.kinded_id_aux
Sourceval unloc_kind : Ast.kind -> Ast.kind
Sourceval typ_nexps : Ast.typ -> Ast.nexp list
Sourceval typ_arg_nexps : Ast.typ_arg -> Ast.nexp list
Sourceval constraint_nexps : Ast.n_constraint -> Ast.nexp list
Sourceval nexp_power_variables : Ast.nexp -> Ast_compare.KidSet.t
Sourceval constraint_power_variables : Ast.n_constraint -> Ast_compare.KidSet.t
Sourceval ex_counter : int ref
Sourceval fresh_existential : Parse_ast.l -> Ast.kind_aux -> Ast.kinded_id
Sourceval named_existential : Ast.l -> Ast.kind_aux -> string option -> Ast.kinded_id
Sourceval destruct_exist_plain : ?name:??? -> Ast.typ -> (Ast.kinded_id list * Ast.n_constraint * Ast.typ) option
Sourceval destruct_numeric : ?name:??? -> 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)} to ['n], 'n <= 10, 'n v
  • int to ['n], true, 'n (where 'n is fresh)
  • atom('n) to [], true, 'n *
Sourceval destruct_boolean : ?name:??? -> Ast.typ -> (Ast.kid * Ast.n_constraint) option
Sourceval destruct_exist : ?name:??? -> Ast.typ -> (Ast.kinded_id list * Ast.n_constraint * Ast.typ) option