Module `Gospel.Dterm`Source

Sourcetype dty =

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

Sourceand dtvar = {

dtv_id : int;
mutable dtv_def : dty option;

}

Sourceval dty_fresh : unit -> dty

Sourceval dty_of_ty : Ttypes.ty -> dty

Sourceval ty_of_dty : dty -> Ttypes.ty

Sourceval dty_integer : dty

Sourceval dty_bool : dty

Sourceval dty_float : dty

Sourceval dty_char : dty

Sourceval dty_string : dty

Sourceval specialize_ls : Tterm.lsymbol -> dty list * dty option

Sourceexception ConstructorExpected of Tterm.lsymbol

Sourceval specialize_cs : loc:Ppxlib.Location.t -> Tterm.lsymbol -> dty list * dty

Sourcemodule Mstr : sig ... end

Sourcetype dpattern = {

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

}

Sourceand 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

Sourcetype dbinder = Identifier.Preid.t * dty

Sourcetype dterm = {

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

}

Sourceand 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

Sourceval dty_of_dterm : dterm -> dty

Sourceval head : dty -> dty

Sourceval occur : int -> dty -> bool

Sourceval unify_dty_ty : dty -> Ttypes.ty -> unit

Sourceexception PatternBadType of dty * dty

Sourceexception BadType of dty * dty

Sourceexception FmlaExpected

Sourceexception TermExpected

Source

val app_unify : 
  loc:Ppxlib.Location.t ->
  Tterm.lsymbol ->
  ('a -> 'b -> unit) ->
  'a list ->
  'b list ->
  unit

Source

val app_unify_map : 
  loc:Ppxlib.Location.t ->
  Tterm.lsymbol ->
  ('a -> 'b -> 'c) ->
  'a list ->
  'b list ->
  'c list

Sourceval dpattern_unify : dpattern -> dty -> unit

Sourceval dty_unify : loc:Ppxlib.Location.t -> dty -> dty -> unit

Sourceval dterm_unify : dterm -> dty -> unit

Sourceval dfmla_unify : dterm -> unit

Sourceval unify : dterm -> dty option -> unit

Sourcetype denv = dty Mstr.t

Sourceexception DuplicatedVar of string

Sourceexception UnboundVar of string

Sourceval denv_find : loc:Ppxlib.Location.t -> Mstr.key -> 'a Mstr.t -> 'a

Sourceval is_in_denv : 'a Mstr.t -> Mstr.key -> bool

Sourceval denv_empty : 'a Mstr.t

Sourceval denv_get_opt : 'a Mstr.t -> Mstr.key -> 'a option

Sourceval denv_add_var : 'a Mstr.t -> Mstr.key -> 'a -> 'a Mstr.t

Source

val denv_add_var_quant : 
  'a Mstr.t ->
  (Identifier.Preid.t * 'a) list ->
  'a Mstr.t

coercions

Sourceval apply_coercion : Tterm.lsymbol list -> dterm -> dterm

Sourceval ts_of_dty : dty option -> Ttypes.tysymbol

Sourceval ty_of_dty_raw : dty option -> Ttypes.ty

Sourceval max_dty : Coercion.t -> dterm list -> dty option

Sourceval dterm_expected_op : Coercion.t -> dterm -> dty option -> dterm

Sourceval dfmla_expected : Coercion.t -> dterm -> dterm

Sourceval dterm_expected : Coercion.t -> dterm -> dty -> dterm

dterm to tterm

Sourceval pattern : dpattern -> Tterm.pattern * Tterm.vsymbol Mstr.t

Source

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

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

Sourceval term : Tterm.vsymbol Mstr.t -> dterm -> Tterm.term

Sourceval flatten : dty -> dty

Sourceval print_dty : dty Utils.Fmt.t

Sourceval print_dpattern : dpattern Utils.Fmt.t

Sourceval print_dterm : dterm Utils.Fmt.t

package gospel

Module Gospel.DtermSource

Module `Gospel.Dterm`Source