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;
}
module Mstr : Stdlib.Map.S with type key = string
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 Symbols.lsymbol * dpattern list
  4. | DPor of dpattern * dpattern
  5. | DPas of dpattern * Identifier.Preid.t
  6. | DPcast of dpattern * dty
  7. | DPconst of Ppxlib.Parsetree.constant
  8. | DPinterval of char * char
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.constant
  4. | DTapp of Symbols.lsymbol * dterm list
  5. | DTif of dterm * dterm * dterm
  6. | DTlet of Identifier.Preid.t * dterm * dterm
  7. | DTcase of dterm * (dpattern * dterm option * dterm) list
  8. | DTquant of Tterm.quant * dbinder list * dterm
  9. | DTlambda of dpattern list * dterm
  10. | DTbinop of Tterm.binop * dterm * dterm
  11. | DTnot of dterm
  12. | DTold of dterm
  13. | DTtrue
  14. | DTfalse
type denv = dty Mstr.t
val dty_bool : dty
val dty_char : dty
val dty_float : dty
val dty_string : dty
val dty_integer : dty
val dty_int : dty
val dty_of_dterm : dterm -> dty
val dty_of_ty : Ttypes.ty -> dty
val dty_fresh : unit -> dty
val max_dty : Coercion.t -> dterm list -> dty option
val specialize_ls : Symbols.lsymbol -> dty list * dty option
val specialize_cs : loc:Ppxlib.Location.t -> Symbols.lsymbol -> dty list * dty
val dty_unify : loc:Ppxlib.Location.t -> dty -> dty -> unit
val dterm_unify : dterm -> dty -> unit
val app_unify : loc:Ppxlib.Location.t -> Symbols.lsymbol -> ('a -> 'b -> unit) -> 'a list -> 'b list -> unit
val app_unify_map : loc:Ppxlib.Location.t -> Symbols.lsymbol -> ('a -> 'b -> 'c) -> 'a list -> 'b list -> 'c list
val dfmla_unify : dterm -> unit
val dpattern_unify : dpattern -> dty -> unit
val unify : dterm -> dty option -> unit
val dterm_expected : Coercion.t -> dterm -> dty -> dterm
val dfmla_expected : Coercion.t -> dterm -> dterm
val dterm_expected_op : Coercion.t -> dterm -> dty option -> dterm
val denv_get_opt : 'a Mstr.t -> string -> 'a option
val denv_find : loc:Ppxlib.Location.t -> string -> denv -> dty
val is_in_denv : denv -> string -> bool
val denv_add_var : denv -> string -> dty -> denv
val denv_add_var_quant : denv -> (Identifier.Preid.t * dty) list -> denv
val term : Symbols.vsymbol Mstr.t -> dterm -> Tterm.term
val fmla : Symbols.vsymbol Mstr.t -> dterm -> Tterm.term
val pattern : dpattern -> Tterm.pattern * Symbols.vsymbol Mstr.t