Up  Next

Module TermInner.Default.U

module U: TermInner.Util(sig


type t = TermInner.Default.t_ 




val repr : t -> t TermInner.view


val build : t TermInner.view -> t
end)
include struct ... end
val ty_type : T.t
val ty_kind : T.t
val ty_prop : T.t
val ty_unitype : T.t
val build : T.t TermInner.build
val const : TermInner.id -> T.t
val var : T.t TermInner.var -> T.t
val app : T.t -> T.t list -> T.t
val app_const : TermInner.id -> T.t list -> T.t
val mk_bind : TermInner.Binder.t -> T.t TermInner.var -> T.t -> T.t
val mk_bind_l : TermInner.Binder.t -> T.t TermInner.var list -> T.t -> T.t
val fun_ : T.t TermInner.var -> T.t -> T.t
val mu : T.t TermInner.var -> T.t -> T.t
val let_ : T.t TermInner.var -> T.t -> T.t -> T.t
val match_with : T.t -> T.t TermInner.cases -> T.t
val forall : T.t TermInner.var -> T.t -> T.t
val exists : T.t TermInner.var -> T.t -> T.t
val true_ : T.t
val false_ : T.t
val builtin : T.t TermInner.Builtin.t -> T.t
val app_builtin : T.t TermInner.Builtin.t -> T.t list -> T.t
val not_ : T.t -> T.t
val and_ : T.t list -> T.t
val or_ : T.t list -> T.t
val imply : T.t -> T.t -> T.t
val imply_l : T.t list -> T.t -> T.t
val eq : T.t -> T.t -> T.t
val neq : T.t -> T.t -> T.t
val ite : T.t -> T.t -> T.t -> T.t
val undefined_self : T.t -> T.t
val undefined_atom : ty:T.t -> T.t
val data_test : TermInner.id -> T.t -> T.t
val data_select : TermInner.id -> int -> T.t -> T.t
val unparsable : ty:T.t -> T.t
val guard : T.t -> T.t TermInner.Builtin.guard -> T.t
val asserting : T.t -> T.t list -> T.t
val assuming : T.t -> T.t list -> T.t
val ty_builtin : TermInner.TyBuiltin.t -> T.t
val ty_const : TermInner.id -> T.t
val ty_app : T.t -> T.t list -> T.t
val ty_arrow : T.t -> T.t -> T.t
val ty_arrow_l : T.t list -> T.t -> T.t
val ty_forall : T.t TermInner.var -> T.t -> T.t
val ty_var : T.t TermInner.var -> T.t
val ty_meta : T.t MetaVar.t -> T.t
val fun_l : T.t TermInner.var list -> T.t -> T.t
val forall_l : t_ TermInner.var list -> t_ -> t_
val exists_l : T.t TermInner.var list -> T.t -> T.t
val ty_forall_l : T.t TermInner.var list -> T.t -> T.t
val let_l : (T.t TermInner.var * T.t) list -> T.t -> T.t
val close_forall : t_ -> t_
val hash_fun : T.t -> CCHash.state -> CCHash.state
val hash_fun_alpha_eq : T.t -> CCHash.state -> CCHash.state
val hash : T.t -> int
val hash_alpha_eq : T.t -> int
type subst = (T.t, T.t) Subst.t 
type renaming = (t_, t_ Var.t) Var.Subst.t 
val rename_var : (T.t, T.t) Subst.t -> T.t Subst.var -> (T.t, T.t) Subst.t * T.t Var.t
val equal_with : subst:(T.t, T.t) Subst.t -> T.t -> T.t -> bool
val equal : T.t -> T.t -> bool
module Tbl: CCHashtbl.Make(As_key)
module Map: CCMap.Make(As_key)
val remove_dup : Tbl.key list -> t_ list
val and_nodup : Tbl.key CCList.t -> t_
val fold : f:('a -> 'b -> T.t -> 'a) ->
       bind:('b -> T.t TermInner.var -> 'b) -> 'a -> 'b -> T.t -> 'a
val iter : f:('a -> T.t -> unit) ->
       bind:('a -> T.t TermInner.var -> 'a) -> 'a -> T.t -> unit
val map' : f:('a -> T.t -> 'b) ->
       bind:('a -> T.t TermInner.var -> 'a * 'b TermInner.var) ->
       'a -> T.t -> 'b TermInner.view
val map : f:('a -> T.t -> T.t) ->
       bind:('a -> T.t TermInner.var -> 'a * T.t TermInner.var) -> 'a -> T.t -> T.t
val map_pol : f:('a -> P.t -> T.t -> T.t) ->
       bind:('a -> T.t TermInner.var -> 'a * T.t TermInner.var) ->
       'a -> P.t -> T.t -> T.t
val approx_infinite_quant_pol : [ `Eq | `Exists | `Forall ] ->
       Polarity.t -> [ `Keep | `Unsat_means_unknown of t_ ]
val size : T.t -> int
val deref : subst:(T.t, T.t) Subst.t -> T.t -> T.t
val eval : ?rec_:bool -> subst:(T.t, T.t) Subst.t -> T.t -> T.t
val eval_renaming : subst:(T.t, T.t Subst.var) Subst.t -> T.t -> T.t
val renaming_to_subst : ('a, T.t TermInner.var) Var.Subst.t -> ('a, T.t) Var.Subst.t
type apply_error = {
   ae_msg : string;
   ae_term : t_ option;
   ae_ty : t_;
   ae_args : t_ list;
   ae_args_ty : t_ list;
   ae_subst : subst;
} 
exception ApplyError of apply_error

Raised when a type application fails
exception UnifError of string * T.t * T.t

Raised for unification or matching errors
val ty_apply_full : t_ -> terms:t_ list -> tys:t_ list -> t_ * subst
val ty_apply : t_ -> terms:t_ list -> tys:t_ list -> t_
val ty_apply_mono : t_ -> tys:t_ list -> t_
type signature = TermInner.id -> T.t option 
val ty_exn : sigma:(TermInner.id -> t_ option) -> t_ -> t_
val ty : sigma:(TermInner.id -> t_ option) -> t_ -> (t_, string) CCResult.t
val match_exn : ?subst2:(T.t, T.t) Subst.t -> T.t -> T.t -> (T.t, T.t) Subst.t
val match_ : ?subst2:(T.t, T.t) Subst.t -> T.t -> T.t -> (T.t, T.t) Subst.t option