aboutsummaryrefslogtreecommitdiff
path: root/src/interp
diff options
context:
space:
mode:
authordos-reis <gdr@axiomatics.org>2011-10-31 15:46:44 +0000
committerdos-reis <gdr@axiomatics.org>2011-10-31 15:46:44 +0000
commitd09e20ae6c0742e6cafc46385de80b3dbafaf9c5 (patch)
tree795a2793dea7688a45507ff1792a0b0baf48ad2d /src/interp
parent7989b128162c7b8ff385b9ac65a43df20591e8b9 (diff)
downloadopen-axiom-d09e20ae6c0742e6cafc46385de80b3dbafaf9c5.tar.gz
* interp/i-funsel.boot (evalMmCond0): Tidy. Call evalMmGuard to
validate modemap evaluation. (evalMmGuard): New. (evalMmCat): Do not call orderMmCatStack here. The stack is already ordered by evalMmGuard, sole caller. (hasCate): Handle domain query variables. (unifyStruct): Call unifyQueryStruct for query variables. (unifyQueryStruct): New. * interp/g-util.boot (postComposeSubst): New. (queryVar?): Likewise.
Diffstat (limited to 'src/interp')
-rw-r--r--src/interp/g-util.boot9
-rw-r--r--src/interp/i-funsel.boot52
2 files changed, 52 insertions, 9 deletions
diff --git a/src/interp/g-util.boot b/src/interp/g-util.boot
index e0c587e7..178ec1ab 100644
--- a/src/interp/g-util.boot
+++ b/src/interp/g-util.boot
@@ -497,6 +497,9 @@ insertWOC(x,y) ==
fn(x,t)
+++ Post-compose substitution `subst' with `s +-> v'
+postComposeSubst(subst,s,v) ==
+ [[x,:substitute(v,s,y)] for [x,:y] in subst]
--% Miscellaneous Functions for Working with Strings
@@ -960,6 +963,12 @@ gensymInt g ==
n := 10 * n + charDigitVal stringChar(p,i)
n
+++ Return true if var is a query variable, e.g. any identifier
+++ that starts with a question mark.
+queryVar? var ==
+ s := symbolName var
+ #s > 1 and stringChar(s,0) = char "?" and digit? stringChar(s,1)
+
++ Returns a newly allocated domain shell (a simple vector) of length `n'.
newShell: %Short -> SIMPLE_-ARRAY
newShell n ==
diff --git a/src/interp/i-funsel.boot b/src/interp/i-funsel.boot
index 8236dfbc..fb10e80a 100644
--- a/src/interp/i-funsel.boot
+++ b/src/interp/i-funsel.boot
@@ -1200,9 +1200,9 @@ evalMmCond(op,sig,st) ==
evalMmCond0(op,sig,st) ==
-- evaluates the nonempty list of modemap conditions st
-- the result is either 'failed or a substitution list
- SL:= evalMmDom st
+ SL := evalMmDom st
SL is 'failed => 'failed
- for p in SL until p1 and not b repeat b:=
+ for p in SL until p1 ~= nil and not b repeat b:=
p1 := objectAssoc(first p,$Subst)
p1 and
t1:= rest p1
@@ -1221,7 +1221,8 @@ evalMmCond0(op,sig,st) ==
canCoerceFrom(t1,t) => 'T
isSubDomain(t,t1) => p.rest := t1
t1 = $Symbol and canCoerceFrom(getSymbolType first p,t)
- ( SL and p1 and not b and 'failed ) or evalMmCat(op,sig,st,SL)
+ SL ~= nil and p1 ~= nil and not b => 'failed
+ evalMmGuard(op,sig,st,SL)
fixUpTypeArgs SL ==
for (p := [v, :t2]) in SL repeat
@@ -1298,7 +1299,7 @@ orderMmCatStack st ==
-- tries to reorder stack so that free pattern variables appear
-- as parameters first
st = nil or rest(st) = nil => st
- vars := DELETE_-DUPLICATES [second(s) for s in st | isPatternVar(second(s))]
+ vars := removeDuplicates [v for [.,v,.] in st | isPatternVar v]
vars = nil => st
havevars := nil
haventvars := nil
@@ -1320,11 +1321,28 @@ mmCatComp(c1, c2) ==
b1 and b2 = nil => true
false
+++ Evaluate the non-domain equality constraints of the predicates,
+++ given by `stack', guarding the selection of operator `op' with
+++ signature `sig'. If successful, return the resulting augmented
+++ substitution `SL', otherwise failed.
+evalMmGuard(op,sig,stack,SL) ==
+ SL := evalMmCat(op,sig,
+ orderMmCatStack [c for c in stack | c is ['ofCategory,:.]],SL)
+ SL is 'failed => 'failed
+ stack := [c for c in stack | c is ['%exist,:.]] or return SL
+ and/[SL := check(op,sig,vars,conds,SL) for [.,vars,conds] in stack
+ | SL isnt 'failed or leave 'failed] where
+ check(op,sig,vars,conds,SL) ==
+ -- Each query variable must have an assigned value
+ and/[symbolTarget(v,SL) for v in vars] or return 'failed
+ -- All constraints on query variables must be satisfied.
+ evalMmCat(op,sig,
+ orderMmCatStack [c for c in conds | c is ['ofCategory,:.]],SL)
+
+++ Like evalMmGuard, but evaluate only category satisfaction contraints.
evalMmCat(op,sig,stack,SL) ==
-- evaluates all ofCategory's of stack as soon as possible
$hope:local:= nil
- numConds:= #stack
- stack:= orderMmCatStack [mmC for mmC in stack | mmC is ["ofCategory",:.]]
while stack until not makingProgress repeat
st := stack
stack := nil
@@ -1360,15 +1378,15 @@ evalMmCat1(mmC is ['ofCategory,d,c],op, SL) ==
-- If c is not Set, Ring or Field then the more general mechanism
dom := defaultTypeForCategory(c, SL)
dom = nil =>
- op isnt 'coerce => 'failed -- evalMmCatLastChance(d,c,SL)
+ op isnt 'coerce => 'failed
null (p := objectAssoc(d,$Subst)) =>
dom =>
NSL := [[d,:dom]]
- op isnt 'coerce => 'failed -- evalMmCatLastChance(d,c,SL)
+ op isnt 'coerce => 'failed
if containsVars dom then dom := resolveTM(rest p, dom)
$Coerce and canCoerce(rest p, dom) =>
NSL := [[d,:dom]]
- op isnt 'coerce => 'failed -- evalMmCatLastChance(d,c,SL)
+ op isnt 'coerce => 'failed
NSL
hasCate(dom,cat,SL) ==
@@ -1387,6 +1405,11 @@ hasCate(dom,cat,SL) ==
'failed
SL1 := [[v,:d] for [v,:d] in SL | not containsVariables d]
if SL1 then cat := subCopy(cat, SL1)
+ -- Replace query variables by their values and try again
+ ident? dom and queryVar? dom =>
+ dom' := symbolTarget(dom,SL) =>
+ hasCate(dom',substitute(dom',dom,cat),SL)
+ 'failed
hasCaty(dom,cat,SL)
hasCate1(dom, cat, SL, domPvar) ==
@@ -1641,6 +1664,8 @@ unifyStruct(s1,s2,SL) ==
s1=s2 => SL
isPatternVar s1 => unifyStructVar(s1,s2,SL)
isPatternVar s2 => unifyStructVar(s2,s1,SL)
+ ident? s1 and queryVar? s1 => unifyQueryStruct(s1,s2,SL)
+ ident? s2 and queryVar? s2 => unifyQueryStruct(s2,s1,SL)
s1 isnt [.,:.] or s2 isnt [.,:.] => 'failed
until s1 = nil or s2 = nil or SL is 'failed repeat
SL:= unifyStruct(first s1,first s2,SL)
@@ -1686,6 +1711,15 @@ unifyStructVar(v,s,SL) ==
augmentSub(v,s,S)
augmentSub(v,s,SL)
+++ `v' is a query variable; we are asked to unify it with
+++ structure `s' and existing substitution `SL'.
+unifyQueryStruct(v,s,SL) ==
+ CONTAINED(v,s) => 'failed
+ s' := LASSOC(v,SL) =>
+ s = s' => SL
+ 'failed
+ [[v,:s],:SL]
+
ofCategory(dom,cat) ==
-- entry point to category evaluation from other points than type
-- analysis