libsail 0.17.1 · OCaml Package

module Big_int = Nat_big_num

val opt_tc_debug : int ref

val depth : int ref

val indent : int -> string

val typ_debug : ?level:int -> string Lazy.t -> unit

val typ_print : string Lazy.t -> unit

val adding : string

type constraint_reason = (Ast.l * string) option

type type_variables = {

vars : (Ast.l * Ast.kind_aux) Ast_util.KBindings.t;
shadows : int Ast_util.KBindings.t;

}

type type_error =

| Err_no_casts of Ast_util.uannot Ast.exp * Ast.typ * Ast.typ * type_error * type_error list
| Err_no_overloading of Ast.id * (Ast.id * type_error) list
| 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
| Err_failed_constraint of Ast.n_constraint * (Ast_util.mut * Ast.typ) Ast_util.Bindings.t * type_variables * Ast.n_constraint list
| Err_subtype of Ast.typ * Ast.typ * Ast.n_constraint option * (constraint_reason * Ast.n_constraint) list * type_variables
| Err_no_num_ident of Ast.id
| Err_other of string
| 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_qi_aux : Ast.quant_item_aux -> Ast.quant_item_aux

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 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

package libsail