Overview  Index  Help 

TERM_MATCH_UNIF

All Known Implementing Modules:

TermMatchUnifProofInfer


The First-Order LoopW Type Inference formula/term matching and unification. Provides functions in order to perform pattern-matching and unification.

           
Value summary

val match
    : ProofAst.ident list ->
        ProofAst.formula * ProofAst.formula ->
          (ProofAst.ident * ProofAst.term) list

           performs the pattern-matching where the pattern meta-variables belongs to an identifiers list.

val matchList
    : ProofAst.ident list ->
        (ProofAst.ident * ProofAst.formula) list *
        (ProofAst.ident * ProofAst.formula) list ->
          (ProofAst.ident * ProofAst.term) list

           performs the pattern-matching of a formulas list with a patterns list where the pattern meta-variables belongs to an identifiers list.

val matchOrderedList
    : ProofAst.ident list ->
        ProofAst.formula list * ProofAst.formula list ->
          (ProofAst.ident * ProofAst.term) list

           performs the pattern-matching of a formulas list with a patterns list where the pattern meta-variables belongs to an identifiers list.

val matchUnifList
    : ProofAst.ident list ->
        (ProofAst.ident * ProofAst.formula) list *
        (ProofAst.ident * ProofAst.formula) list ->
          (ProofAst.ident * ProofAst.formula * ProofAst.formula) list *
          (ProofAst.ident * ProofAst.term * ProofAst.term) list *
          (ProofAst.ident * ProofAst.term) list

           performs the pattern-matching and unification where the pattern meta-variables belongs to an identifiers list.

val unify
    : ProofAst.formula * ProofAst.formula ->
        ProofAst.formula * (ProofAst.ident * ProofAst.term * ProofAst.term) list

           performs the unification of two formulas on the term-level.

val unifyList
    : (ProofAst.ident * ProofAst.formula) list *
      (ProofAst.ident * ProofAst.formula) list ->
        (ProofAst.ident * ProofAst.formula) list *
        (ProofAst.ident * ProofAst.term * ProofAst.term) list

           performs the unification of two (identifiers, formulas) list on the term-level.

val unifyOrderedList
    : ProofAst.formula list * ProofAst.formula list ->
        (ProofAst.formula *
         (ProofAst.ident * ProofAst.term * ProofAst.term) list) list

           performs the unification of two formulas list on the term-level.

 
Exception summary

exception AbsentIdent of ProofAst.ident *
                         (ProofAst.ident * ProofAst.formula) list

          no identifier found error

exception LengthMismatch
          length mismatch beetwen lists error

exception MatchErrorTerms of ProofAst.term * ProofAst.term
          matching error for terms

exception MatchErrorTypeList of ProofAst.formula list * ProofAst.formula list
          matching error for types lists

exception MatchErrorTypes of ProofAst.formula * ProofAst.formula
          matching error for types

exception MatchUnifErrorTerms of ProofAst.term * ProofAst.term
          matching+unification error for terms

exception MatchUnifErrorTypeList of ProofAst.formula list *
                                    ProofAst.formula list

          matching+unification error for types lists

exception MatchUnifErrorTypes of ProofAst.formula * ProofAst.formula
          matching+unification error for types

exception NotUnifyableTerms of ProofAst.term * ProofAst.term
          unification error for terms

exception NotUnifyableTypes of ProofAst.formula * ProofAst.formula
          unification error for types

       
Value detail

match

fun match idl (p, t)
    : ProofAst.ident list ->
        ProofAst.formula * ProofAst.formula ->
          (ProofAst.ident * ProofAst.term) list

performs the pattern-matching where the pattern meta-variables belongs to an identifiers list.

Parameters:
idl
the identifier list of pattern meta-variables.
p
the formula pattern.
t
the formula to match.
Returns:
the substitutions list that matches.
Exception:
MatchErrorTypes
if the pattern cannot match the formula.

matchOrderedList

fun matchOrderedList idl (pl, fl)
    : ProofAst.ident list ->
        ProofAst.formula list * ProofAst.formula list ->
          (ProofAst.ident * ProofAst.term) list

performs the pattern-matching of a formulas list with a patterns list where the pattern meta-variables belongs to an identifiers list. The pattern-matching is performed all along the lists, using the same order.

Parameters:
idl
the identifier list of pattern meta-variables.
pl
the formulas list pattern.
fl
the formulas list to match.
Returns:
the substitutions list that matches.
Exception:
MatchErrorTypeList
if the pattern cannot match the formula.
LengthMismatch
if the length of the lists differs.

matchList

fun matchList idl (pl, fl)
    : ProofAst.ident list ->
        (ProofAst.ident * ProofAst.formula) list *
        (ProofAst.ident * ProofAst.formula) list ->
          (ProofAst.ident * ProofAst.term) list

performs the pattern-matching of a formulas list with a patterns list where the pattern meta-variables belongs to an identifiers list. The pattern-matching is performed according to the identifier associated with the patterns and formulas elements.

Parameters:
idl
the identifier list of pattern meta-variables.
pl
the (identifiers, formulas) list pattern.
fl
the (identifiers, formulas) list to match.
Returns:
the substitutions list that matches.
Exception:
MatchErrorTypeList
if the pattern cannot match the formula.
LengthMismatch
if the length of the lists differs.
AbsentIdent
if an identifier belongs to pl and not to fl.

matchUnifList

fun matchUnifList idl (pl, fl)
    : ProofAst.ident list ->
        (ProofAst.ident * ProofAst.formula) list *
        (ProofAst.ident * ProofAst.formula) list ->
          (ProofAst.ident * ProofAst.formula * ProofAst.formula) list *
          (ProofAst.ident * ProofAst.term * ProofAst.term) list *
          (ProofAst.ident * ProofAst.term) list

performs the pattern-matching and unification where the pattern meta-variables belongs to an identifiers list.

Parameters:
idl
the identifier list of pattern meta-variables {i}.
pl
the (identifier, formula) list pattern (x:f)[i][n/j].
fl
the (identifier, formula) list to match (x:f)[u/i][m/j].
Returns:
the formulas with unification variables, the unification variables associated with equations and the substitutions list that matches (((x:f)[i][j], (x:f)[u/i][j]), (j,n,m), (i,u)).
Exception:
MatchUnifErrorTypes
if the pattern cannot match the formula.

unify

fun unify (a, b)
    : ProofAst.formula * ProofAst.formula ->
        ProofAst.formula * (ProofAst.ident * ProofAst.term * ProofAst.term) list

performs the unification of two formulas on the term-level.

Parameters:
a
the first formula to unify f[n/i].
b
the second formula to unify f[m/i].
Returns:
the formula with meta-variables f[i] and the equations list (i, n = m).
Exception:
NotUnifyableTypes
when unification is impossible (formulas structure differs).

unifyOrderedList

fun unifyOrderedList (l1, l2)
    : ProofAst.formula list * ProofAst.formula list ->
        (ProofAst.formula *
         (ProofAst.ident * ProofAst.term * ProofAst.term) list) list

performs the unification of two formulas list on the term-level. The unification is performed all along the lists, using to the same order.

Parameters:
l1
the first formula to unify l1[n/i].
l2
the second formula to unify l2[m/i].
Returns:
the list of formula with meta-variables f[i] associated with the equations list (i, n = m).
Exception:
LengthMismatch
if lists size differs.

unifyList

fun unifyList (xl1, xl2)
    : (ProofAst.ident * ProofAst.formula) list *
      (ProofAst.ident * ProofAst.formula) list ->
        (ProofAst.ident * ProofAst.formula) list *
        (ProofAst.ident * ProofAst.term * ProofAst.term) list

performs the unification of two (identifiers, formulas) list on the term-level. The unification is performed according to the identifier associated with the formulas.

Parameters:
xl1
the first formula to unify xl1[n/i].
xl2
the second formula to unify xl2[m/i].
Returns:
the list of formula with meta-variables f[i] associated with the equations list (i, n = m).
Exception:
LengthMismatch
if lists size differs.
AbsentIdent
if lists differs for some identifier.

 
Exception detail

MatchErrorTypes

exception MatchErrorTypes of ProofAst.formula * ProofAst.formula

matching error for types


MatchErrorTypeList

exception MatchErrorTypeList of ProofAst.formula list * ProofAst.formula list

matching error for types lists


MatchErrorTerms

exception MatchErrorTerms of ProofAst.term * ProofAst.term

matching error for terms


MatchUnifErrorTypes

exception MatchUnifErrorTypes of ProofAst.formula * ProofAst.formula

matching+unification error for types


MatchUnifErrorTypeList

exception MatchUnifErrorTypeList of ProofAst.formula list *
                                    ProofAst.formula list

matching+unification error for types lists


MatchUnifErrorTerms

exception MatchUnifErrorTerms of ProofAst.term * ProofAst.term

matching+unification error for terms


NotUnifyableTypes

exception NotUnifyableTypes of ProofAst.formula * ProofAst.formula

unification error for types


NotUnifyableTerms

exception NotUnifyableTerms of ProofAst.term * ProofAst.term

unification error for terms


AbsentIdent

exception AbsentIdent of ProofAst.ident *
                         (ProofAst.ident * ProofAst.formula) list

no identifier found error


LengthMismatch

exception LengthMismatch

length mismatch beetwen lists error


Overview  Index  Help