Previous  Up  Next

Module Term

module Term: sig .. end
The type of term types, operations on these types and a parser for types.
type term =
| Term of string * term array * term array (*Head symbol, supertypes, subterms*)
| SVar of string * int * term * term array (*Shared variable symbol, encoding depth, type, subterms*)
| TVar of string * term option (*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

Type Unification


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

ISA relation and iterated substitution based operations.


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
Iterated substitutions are sets of term equations in solved form, but without disjointness between the domain and variables in the image of substitution. See "Term Rewriting and All That" p. 82. Currently implemented as sorted association lists.
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 string * string * string (*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 string * string * string (*The proposed declaration together with the third symbol would have the first two symbols both as least upper bounds.*)
| Decls_redundant_s of string * string (*Of proposed direct superclasses one ISA the second one.*)
| Decls_polyconflict (*One of several supertypes is a type variable.*)
| Decls_var
| Decls_repeating of string
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

Parsing and Printing Types


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

Hashtable for Terms


module HashableTerm: sig .. end
module TermHashtbl: sig .. end