summaryrefslogtreecommitdiff
path: root/miralib/ex/unify.m
diff options
context:
space:
mode:
authorJakob Kaivo <jkk@ung.org>2022-03-04 12:32:20 -0500
committerJakob Kaivo <jkk@ung.org>2022-03-04 12:32:20 -0500
commit55f277e77428d7423ae906a8e1f1324d35b07a7d (patch)
tree5c1c04703dff89c46b349025d2d3ec88ea9b3819 /miralib/ex/unify.m
import Miranda 2.066 from upstream
Diffstat (limited to 'miralib/ex/unify.m')
-rw-r--r--miralib/ex/unify.m79
1 files changed, 79 insertions, 0 deletions
diff --git a/miralib/ex/unify.m b/miralib/ex/unify.m
new file mode 100644
index 0000000..1ce4034
--- /dev/null
+++ b/miralib/ex/unify.m
@@ -0,0 +1,79 @@
+||Package for doing (first order) unification, parameterised on an
+||abstract theory of expressions. (DT)
+
+||see the file <ex/polish> for an example of the use of this package.
+
+%free { expr,operator,var::type;
+ isvar::expr->bool; getvar::expr->var; putvar::var->expr;
+ rator::expr->operator; rands::expr->[expr];
+ construct::operator->[expr]->expr;
+ }
+
+||Our theory of expressions is as follows - an expression is either a
+||variable, or else it consists of a rator together with a list of
+||rands. So for example a constant will be viewed as a rator which has
+||an empty list of rands. The nature of variables, and the collection
+||of possible rators and their arities, is determined at %include time.
+||This enables us to use the same code for performing unification in
+||quite different object languages.
+
+||for each e::expr, one of the following propositions will be true
+||either isvar e & e = putvar(getvar e)
+||or ~isvar e & e = construct(rator e)(rands e)
+
+%export unifyexprs unify ult q
+
+q * ::= FAIL | SUCCEED * ||useful type operator
+
+unifyexprs :: expr->expr->q expr ||convenient for testing
+
+unify :: subst->expr->expr->q subst
+
+||this implements the unification algorithm - it takes a substition
+||(mapping from variables to expressions) and a pair of expressions, and
+||returns the least extension of the substitution under which the
+||expressions become the same - or FAIL if there is none.
+
+ult :: subst->expr->expr
+
+||computes the result of applying a substitution to an expression.
+
+unifyexprs x y = f(unify [] x y)
+ where
+ f FAIL = FAIL
+ f (SUCCEED s) = SUCCEED (ult s x)
+ ||note that (ult s y) = (ult s y)
+ ||if the unification succeeds
+
+subst == [(var,expr)]
+
+||We represent a substitution as a list of variable-expression pairs.
+||The representation is lazy, in the sense that the expressions may
+||contain occurrences of the variables in the domain of the substitution
+||- this is taken care of in the definition of ult.
+
+unify s x y
+ = unifier s (ult s x) (ult s y)
+ where
+ unifier s x y = SUCCEED s, if x=y
+ = SUCCEED((getvar x,y):s), if isvar x & ~occurs x y
+ = SUCCEED((getvar y,x):s), if isvar y & ~occurs y x
+ = unifylist (SUCCEED s) (rands x) (rands y),
+ if ~isvar x & ~isvar y & conforms x y
+ = FAIL, otherwise
+ unifylist qs [] [] = qs
+ unifylist (SUCCEED s) (a:x) (b:y) = unifylist (unify s a b) x y
+ unifylist FAIL x y = FAIL
+
+ult s x = lookup s (getvar x), if isvar x
+ = construct(rator x)(map (ult s) (rands x)), otherwise
+ where
+ lookup [] a = putvar a
+ lookup ((a,y):t) a = ult s y ||note recursive call of ult
+ lookup ((b,y):t) a = lookup t a
+
+occurs y x || does subexpression y occur in formula x ?
+ = x=y, if isvar x
+ = or (map (occurs y) (rands x)), otherwise
+
+conforms x y = rator x = rator y & #rands x = #rands y