gospel 0.1.0 · OCaml Package

type dty =

| Tvar of dtvar
| Tapp of Ttypes.tysymbol * dty list
| Tty of Ttypes.ty

and dtvar = {

dtv_id : int;
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 = {

dp_node : dpattern_node;
dp_dty : dty;
dp_vars : dty Mstr.t;
dp_loc : Ppxlib.Location.t;

}

and dpattern_node =

| DPwild
| DPvar of Identifier.Preid.t
| DPapp of Tterm.lsymbol * dpattern list
| DPor of dpattern * dpattern
| DPas of dpattern * Identifier.Preid.t
| DPcast of dpattern * dty

type dbinder = Identifier.Preid.t * dty

type dterm = {

dt_node : dterm_node;
dt_dty : dty option;
dt_loc : Ppxlib.Location.t;

}

and dterm_node =

| DTattr of dterm * string list
| DTvar of Identifier.Preid.t
| DTconst of Ppxlib.Parsetree.constant
| DTapp of Tterm.lsymbol * dterm list
| DTif of dterm * dterm * dterm
| DTlet of Identifier.Preid.t * dterm * dterm
| DTcase of dterm * (dpattern * dterm) list
| DTquant of Tterm.quant * dbinder list * dterm
| DTbinop of Tterm.binop * dterm * dterm
| DTnot of dterm
| DTold of dterm
| DTtrue
| 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 pattern : dpattern -> Tterm.pattern * Tterm.vsymbol Mstr.t

val term_node : 
  Tterm.vsymbol Mstr.t ->
  bool ->
  dty option ->
  dterm_node ->
  Ppxlib.Location.t ->
  Tterm.term

val fmla : Tterm.vsymbol Mstr.t -> dterm -> Tterm.term

val term : Tterm.vsymbol Mstr.t -> dterm -> 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

package gospel