TERM_MATCH_UNIF
- All Known Implementing Modules:
-
TermMatchUnif, ProofInfer
-
The First-Order LoopW Type Inference formula/term matching and unification.
Provides functions in order to perform pattern-matching and unification.
-
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.
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
-