package gospel

  1. Overview
  2. Docs
type dty =
  1. | Tvar of dtvar
  2. | Tapp of Ttypes.tysymbol * dty list
  3. | Tty of Ttypes.ty
and dtvar = {
  1. dtv_id : int;
  2. mutable dtv_def : dty option;
}
val dty_fresh : unit -> dty
val dty_of_ty : Ttypes.ty -> dty
val ty_of_dty : dty -> Ttypes.ty
val dty_integer : dty
val dty_bool : dty
val dty_float : dty
val dty_char : dty
val dty_string : dty
val specialize_ls : Tterm.lsymbol -> dty list * dty option
exception ConstructorExpected of Tterm.lsymbol
val specialize_cs : loc:Ppxlib.Location.t -> Tterm.lsymbol -> dty list * dty
module Mstr : sig ... end
type dpattern = {
  1. dp_node : dpattern_node;
  2. dp_dty : dty;
  3. dp_vars : dty Mstr.t;
  4. dp_loc : Ppxlib.Location.t;
}
and dpattern_node =
  1. | DPwild
  2. | DPvar of Identifier.Preid.t
  3. | DPapp of Tterm.lsymbol * dpattern list
  4. | DPor of dpattern * dpattern
  5. | DPas of dpattern * Identifier.Preid.t
  6. | DPcast of dpattern * dty
type dbinder = Identifier.Preid.t * dty
type dterm = {
  1. dt_node : dterm_node;
  2. dt_dty : dty option;
  3. dt_loc : Ppxlib.Location.t;
}
and dterm_node =
  1. | DTattr of dterm * string list
  2. | DTvar of Identifier.Preid.t
  3. | DTconst of Ppxlib.Parsetree.constant
  4. | DTapp of Tterm.lsymbol * dterm list
  5. | DTif of dterm * dterm * dterm
  6. | DTlet of Identifier.Preid.t * dterm * dterm
  7. | DTcase of dterm * (dpattern * dterm) list
  8. | DTquant of Tterm.quant * dbinder list * dterm
  9. | DTbinop of Tterm.binop * dterm * dterm
  10. | DTnot of dterm
  11. | DTold of dterm
  12. | DTtrue
  13. | DTfalse
val dty_of_dterm : dterm -> dty
val head : dty -> dty
val occur : int -> dty -> bool
val unify_dty_ty : dty -> Ttypes.ty -> unit
exception PatternBadType of dty * dty
exception BadType of dty * dty
exception FmlaExpected
exception TermExpected
val app_unify : loc:Ppxlib.Location.t -> Tterm.lsymbol -> ('a -> 'b -> unit) -> 'a list -> 'b list -> unit
val app_unify_map : loc:Ppxlib.Location.t -> Tterm.lsymbol -> ('a -> 'b -> 'c) -> 'a list -> 'b list -> 'c list
val dpattern_unify : dpattern -> dty -> unit
val dty_unify : loc:Ppxlib.Location.t -> dty -> dty -> unit
val dterm_unify : dterm -> dty -> unit
val dfmla_unify : dterm -> unit
val unify : dterm -> dty option -> unit
type denv = dty Mstr.t
exception DuplicatedVar of string
exception UnboundVar of string
val denv_find : loc:Ppxlib.Location.t -> Mstr.key -> 'a Mstr.t -> 'b
val is_in_denv : 'a Mstr.t -> Mstr.key -> bool
val denv_empty : 'a Mstr.t
val denv_get_opt : 'a Mstr.t -> Mstr.key -> 'a option
val denv_add_var : 'a Mstr.t -> Mstr.key -> 'b -> 'a Mstr.t
val denv_add_var_quant : 'a Mstr.t -> (Identifier.Preid.t * 'b) list -> 'a Mstr.t

coercions

val apply_coercion : Tterm.lsymbol list -> dterm -> dterm
val ts_of_dty : dty option -> Ttypes.tysymbol
val ty_of_dty_raw : dty option -> Ttypes.ty
val max_dty : Coercion.t -> dterm list -> dty option
val dterm_expected_op : Coercion.t -> dterm -> dty option -> dterm
val dfmla_expected : Coercion.t -> dterm -> dterm
val dterm_expected : Coercion.t -> dterm -> dty -> dterm

dterm to tterm

val term_node : Tterm.vsymbol Mstr.t -> bool -> dty option -> dterm_node -> Ppxlib.Location.t -> Tterm.term
val flatten : dty -> dty
val print_dty : dty Utils.Fmt.t
val print_dpattern : dpattern Utils.Fmt.t
val print_dterm : dterm Utils.Fmt.t