module Term:`sig`

..`end`

The type of term types, operations on these types and a parser for types.

`type `

term =

`|` |
`Term of ` |
`(*` | Head symbol, supertypes, subterms | `*)` |

`|` |
`SVar of ` |
`(*` | Shared variable symbol, encoding depth, type, subterms | `*)` |

`|` |
`TVar of ` |
`(*` | Type variable symbol | `*)` |

Hierarchical terms.

`val fun_type_name : ``string`

The name for function type (type of un-applied function term).

Substituting superclasses corresponding to sharing variable types
while rewriting: "Let f X be X := t" syntax.

`val assign_name : ``string`

`val symbol_of_term : ``term -> string`

Head symbol, i.e. functor or variable name, of a term.

`val term_str : ``term -> string`

Concise readable form.

Super concise super readable form.

`val short_term : ``(term -> string) Pervasives.ref`

`val suffix : ``int -> term -> term`

Suffix all type variables, useful for renaming.

`val equal_mod_tvars : ``term -> term -> bool`

Check for equality but ignore RHS subterms corresponding to LHS
type variables.

`val size_up_to : ``int -> term -> int`

Size of a term up to a given value

`val s_vars_in_term : ``string list -> term -> string list`

List variables in the given term. First argument is the accumulator.

`val t_vars_in_term : ``string list -> term -> string list`

`val has_s_var : ``term -> bool`

`val has_t_var : ``term -> bool`

`val fn_apply : ``int -> ('a -> 'a) -> 'a -> 'a`

`val add_logic_name : ``string -> unit`

Logic names are functors whose terms should not decompose under
unification or ISA relation and its algorithms. Currently, logic
names are only

`BuiltinLang.parsed_tvar_name`

and
`BuiltinLang.universal_tvar_name`

. Logic names have to have
types.`type `

t_subst

Substitutions are kept abstract to make it easier to evolve term
semantics.

`type `

s_subst

type`substs =`

`s_subst * t_subst`

`exception UNIFY`

Exception used in unification algorithm on failure.

`val empty_s_sb : ``s_subst`

Operations on substitutions.

`val empty_t_sb : ``t_subst`

`val empty_sbs : ``substs`

Find a term corresponding to the name of a variable or raise

`Not_found`

.`val assoc_t_sb : ``string -> t_subst -> term`

`val assoc_s_sb : ``string -> s_subst -> term`

`val apply_sbs : ``substs -> term -> term`

`val head_grounding : ``term -> term`

Identity on non-variable terms, return type of sharing variable
and upper bound of type variable. Raises

`UNIFY`

on unbounded
type variables.
Return the supertypes of a term or type of a variable.

`val types_of : ``term -> term array`

`type `

position

Positions, in supertypes.

`val position_str : ``position -> string`

`val subst_t_pos : ``position -> subt:term -> term -> term`

`val get_t_pos : ``position -> term -> term`

`type `

iter_s_subst

`type `

iter_t_subst

type`isubsts =`

`iter_s_subst * iter_t_subst`

`val empty_t_isb : ``iter_t_subst`

`val empty_s_isb : ``iter_s_subst`

`val empty_isbs : ``isubsts`

`type `

add_to_decls =

`|` |
`Decls_OK` |
`(*` | Declaration added. | `*)` |

`|` |
`Decls_multi_glb of ` |
`(*` | The first two symbols already have the third symbol as a greatest lower bound, the proposed declaration would introduce alternative GLB for them. | `*)` |

`|` |
`Decls_multi_lub of ` |
`(*` | The proposed declaration together with the third symbol would have the first two symbols both as least upper bounds. | `*)` |

`|` |
`Decls_redundant_s of ` |
`(*` | Of proposed direct superclasses one ISA the second one. | `*)` |

`|` |
`Decls_polyconflict` |
`(*` | One of several supertypes is a type variable. | `*)` |

`|` |
`Decls_var` |
|||

`|` |
`Decls_repeating of ` |

Adding a declaration to a well-formed set of declarations.

`type `

decls_set

Data associated with a well-formed set of declarations; expected
to grow monotonically by adding new declarations.

`val create_decls : ``unit -> decls_set`

`val get_superclasses : ``decls_set -> string -> Aux.Strings.t`

`val get_subclasses : ``decls_set -> string -> string list`

`val get_decl : ``decls_set -> string -> term`

`exception EXC_Decls_multi_lub of ``string * string * string`

`val add_to_decls : ``decls_set -> term -> add_to_decls`

Assuming that the given set of declarations is well-formed, check
if it will remain well-formed after adding the given declaration.
If so, add it and update the

`ISA`

order relation. Return whether
the declaration was added or the reason it was not added.`val glb : ``decls_set -> term -> term -> isubsts * term`

Greatest Lower Bound Unification w.r.t. the ISA relation. Returns
the unsubstituted GLB term and iterated substitutions, or raises

`UNIFY`

. Shared variables are merged using GLB-unification and
type variables are merged using LUB-unification. The returned term
contains variables from the substitution.
Substitutions are never applied during glb-unification. It
is important to return this intermediate representation, because
parsing is a "distributed glb-unification" as it produces a
single term that ISA a declaration.

`val aux_glb : ``decls_set ->`

isubsts -> term -> term -> isubsts * term

`val lub : ``decls_set -> term -> term -> isubsts * term`

Least Upper Bound Unification w.r.t. the ISA relation. Returns
the unsubstituted LUB term and iterated substitutions, or raises

`UNIFY`

. Shared variables are merged using GLB-unification and
type variables are merged using LUB-unification. See also `Term.glb`

.`val aux_lub : ``decls_set ->`

isubsts -> term -> term -> isubsts * term

`val aux_glb_lub_cont : ``decls_set -> isubsts -> isubsts -> isubsts`

`val isa_match : ``decls_set ->`

?for_rewrite:bool ->

pattern:term -> term -> substs * position

Returns the ISA-matching or raises

`UNIFY`

. First term is the
pattern. Shared variables are merged using MGU (eq-unification)
and type variables are merged using LUB-unification. See also
`Term.glb`

. With `for_rewrite=true`

, will ignore mismatches at purely
polymorphic supertypes. (A supertype of a class/functor is purely
polymorphic if in its position in the declaration is a type
variable, even if the variable is bounded.)
Similar to ISA-matching pattern against term and vice versa with
`for_rewriting`

set to true, but treats sharing variables as
constants and does not produce substitutions.

`val equal_for_rewriting : ``decls_set -> term -> term -> bool`

`val isa_unify : ``decls_set -> pattern:term -> term -> isubsts`

Returns the ISA-unification: like ISA-matching, but does not treat
the RHS type variables as constants, instead infers their upper
bounds. Shared variables are merged using GLB-unification and type
variables are merged using LUB-unification. See also

`Term.isa_match`

.`val aux_isa_unify : ``decls_set ->`

isubsts -> pattern:term -> term -> isubsts

`val is_superclass_of : ``decls_set -> pattern:term -> term -> bool`

A very quick check that ignores all subterms, if a term is a
superclass of another term (or the same class).

`val mgu_iter : ``decls_set -> term -> term -> isubsts`

Iterated Substitution based variant of the Most General Unifier
substitution, throws

`UNIFY`

if not unifiable. Both shared
variables and type variables are merged using MGU
(eq-unification).`val aux_mgu_i : ``decls_set -> isubsts -> term -> term -> isubsts`

`val aux_mgu_i_cont : ``decls_set -> isubsts -> isubsts -> isubsts`

`val apply_isbs : ``isubsts -> term -> term`

`val split_to_list : ``string -> Aux.split_result list`

Lexer for terms and types in internal format, to list

`val s_subst_str : ``s_subst -> string`

`val t_subst_str : ``t_subst -> string`

`val t_isubst_str : ``iter_t_subst -> string`

`val substs_str : ``substs -> string`

`val substs_fstr : ``(term -> string) -> substs -> string`

`val isubsts_str : ``isubsts -> string`

`val isubsts_fstr : ``(term -> string) -> isubsts -> string`

`val t_isubst_map : ``(term -> term) -> iter_t_subst -> iter_t_subst`

`val s_isubst_map_some : ``(string * (int * term) -> (string * (int * term)) option) ->`

iter_s_subst -> iter_s_subst

`val isubsts_map : ``(term -> term) -> isubsts -> isubsts`

module HashableTerm:`sig`

..`end`

module TermHashtbl:`sig`

..`end`