gospel 0.2.0 · OCaml Package

type dty =

and dtvar = {

}

module Mstr : Map.S with type key = string

type dpattern = {

}

and dpattern_node =

type dbinder = Identifier.Preid.t * dty

type dterm = {

}

and dterm_node =

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

package gospel