Overview  Index  Help 

TermMatchUnif


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

Opened structures

ProofAst

Terms

               
Value summary

val fresh
           generates a new fresh variable.

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

           performs the pattern-matching of formulas 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 matchUnif
           performs the pattern-matching and unification 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 new_term_subst
           builds a new unification equation with a fresh identifier.

val new_term_subst_eq
           builds a new unification equation with a fresh identifier.

val term_match
           performs the pattern-matching of terms where the pattern meta-variables belongs to an identifiers list.

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

val term_unify
           performs the unification of two terms.

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

fresh

val fresh

generates a new fresh variable.

Returns:
a fresh variable "unif".

term_match

fun term_match idl (p, t)

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

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

match

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

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

Parameters:
idl
the identifier list of pattern meta-variables.
p
the formula pattern.
f
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.

new_term_subst_eq

fun new_term_subst_eq (a, b) eql

builds a new unification equation with a fresh identifier.

Parameters:
a
the first term of the equation.
b
the second term of the equation.
eql
the equation list to which add the new equation.
Returns:
the fresh identifier and the new equation list.

term_matchUnif

fun term_matchUnif idl (p, f)

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}.
p
the term pattern t[i][n/j].
f
the term to match t[u/i][m/j].
Returns:
the terms with unification variables, the unification variables associated with equations and the substitutions list that matches ((t[i][j], t[u/i][j]), (j,n,m), (i,u)).
Exception:
MatchUnifErrorTerms
if the pattern cannot match the term.

matchUnif

fun matchUnif idl (p, f)

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}.
p
the formula pattern f[i][n/j].
f
the formula to match f[u/i][m/j].
Returns:
the formulas with unification variables, the unification variables associated with equations and the substitutions list that matches ((f[i][j], f[u/i][j]), (j,n,m), (i,u)).
Exception:
MatchUnifErrorTypes
if the pattern cannot match the formula.

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.

new_term_subst

fun new_term_subst (a, b) eql

builds a new unification equation with a fresh identifier.

Parameters:
a
the first term of the equation.
b
the second term of the equation.
eql
the equation list to which add the new equation.
Returns:
the fresh identifier and the new equation list.

term_unify

fun term_unify (a, b)

performs the unification of two terms.

Parameters:
a
the first term to unify t[n/i].
b
the second term to unify t[m/i].
Returns:
the term with meta-variables t[i] and the equations list (i, n = m).

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