aboutsummaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
authordos-reis <gdr@axiomatics.org>2011-10-31 03:08:11 +0000
committerdos-reis <gdr@axiomatics.org>2011-10-31 03:08:11 +0000
commit2eaece841c92e8a59aa4346ca85739babfd67fe9 (patch)
tree02126a77562d2d2079e5700e1428914d976f742a /src
parent8bb918e72e98092b6e927828d2ca66198608de4f (diff)
downloadopen-axiom-2eaece841c92e8a59aa4346ca85739babfd67fe9.tar.gz
* interp/compiler.boot (evaluateConstructorModemap): Rename from
substituteInfoFunctorModemap. (constructorCondition): New. * interp/define.boot (compDefineCategory2): Compute dual signature early on. (compDefineFunctor1): Likewise. (typingKind): New. (deduceImplicitParameters): Use it. * interp/database.boot (modemapsFromCategory): Take a first argument as a DB. Tidy. Adjust caller. Add constructor condition. (modemapsFromFunctor): Likewise. Lose last argument. (mkDatabasePred): Remove. (formal2Pattern): Likewise.
Diffstat (limited to 'src')
-rw-r--r--src/ChangeLog7
-rw-r--r--src/interp/compiler.boot35
-rw-r--r--src/interp/database.boot12
-rw-r--r--src/interp/define.boot18
4 files changed, 50 insertions, 22 deletions
diff --git a/src/ChangeLog b/src/ChangeLog
index fcc6e8b7..ea83924e 100644
--- a/src/ChangeLog
+++ b/src/ChangeLog
@@ -1,10 +1,15 @@
2011-10-30 Gabriel Dos Reis <gdr@cs.tamu.edu>
+ * interp/compiler.boot (evaluateConstructorModemap): Rename from
+ substituteInfoFunctorModemap.
+ (constructorCondition): New.
* interp/define.boot (compDefineCategory2): Compute dual signature
early on.
(compDefineFunctor1): Likewise.
+ (typingKind): New.
+ (deduceImplicitParameters): Use it.
* interp/database.boot (modemapsFromCategory): Take a first
- argument as a DB. Tidy. Adjust caller.
+ argument as a DB. Tidy. Adjust caller. Add constructor condition.
(modemapsFromFunctor): Likewise. Lose last argument.
(mkDatabasePred): Remove.
(formal2Pattern): Likewise.
diff --git a/src/interp/compiler.boot b/src/interp/compiler.boot
index 4afa3d4f..074d225e 100644
--- a/src/interp/compiler.boot
+++ b/src/interp/compiler.boot
@@ -589,8 +589,8 @@ compFormWithModemap(form,m,e,modemap) ==
[map:= [.,target,:sig],[pred,impl]]:= modemap
[op,:argl] := form := reshapeArgumentList(form,sig)
if isCategoryForm(target,e) and isFunctor op then
- [modemap,e]:= substituteIntoFunctorModemap(argl,modemap,e) or return nil
- [map:= [.,target,:.],:cexpr]:= modemap
+ [modemap,e] := evaluateConstructorModemap(argl,modemap,e) or return nil
+ [map:=[.,target,:.],:cexpr] := modemap
sv := listOfSharpVars map
if sv ~= nil then
-- SAY [ "compiling ", op, " in compFormWithModemap,
@@ -721,18 +721,27 @@ reshapeArgumentList(form,sig) ==
wantArgumentsAsTuple(args,sig) => [op,["%Comma",:args]]
form
-substituteIntoFunctorModemap(argl,modemap is [[dc,:sig],:.],e) ==
- #dc~=#sig =>
- keyedSystemError("S2GE0016",['"substituteIntoFunctorModemap",
+++ Return true is the constructor condition `cond' holds in the
+++ elaboration environmemt `e'.
+constructorCondition(cond,e) ==
+ cond --FIXME: solve it!
+
+++ The argument list `argl' is used to instantiate a constructor
+++ with `modemap' in environment `e'. Return the resulting
+++ modemap is instantiation is legit.
+evaluateConstructorModemap(argl,modemap is [[dc,:sig],:.],e) ==
+ #dc ~= #sig =>
+ keyedSystemError("S2GE0016",['"evaluateConstructorModemap",
'"Incompatible maps"])
- #argl=#sig.source =>
- --here, we actually have a functor form
- sig := applySubst(pairList(dc.args,argl),sig)
- --make new modemap, subst. actual for formal parametersinto modemap
- Tl:= [[.,.,e]:= compOrCroak(a,m,e) for a in argl for m in rest sig]
- substitutionList:= [[x,:T.expr] for x in dc.args for T in Tl]
- [applySubst(substitutionList,modemap),e]
- nil
+ #argl ~= #sig.source => nil
+ constructorCondition(applySubst(sl,modemap.mmCondition),e) isnt true => nil
+ sl := pairList(dc.args,argl)
+ --make new modemap, subst. actual for formal parameters into modemap
+ Tl := [[.,.,e] := compOrCroak(a,m,e)
+ for a in argl for m in applySubst(sl,modemap.mmSource)]
+ sl := [[x,:T.expr] for x in dc.args for T in Tl]
+ [applySubst(sl,modemap),e]
+
--% SPECIAL EVALUATION FUNCTIONS
diff --git a/src/interp/database.boot b/src/interp/database.boot
index 831de579..dc942f85 100644
--- a/src/interp/database.boot
+++ b/src/interp/database.boot
@@ -191,10 +191,14 @@ modemapsFromCategory(db,form,body,signature) ==
:[['ofCategory,a,m] for a in form.args for m in signature.source
for cat? in dbDualSignature(db).source | cat? ]]
op := dbConstructor db
+ cond :=
+ dbImplicitData db is [isubst,icond] =>
+ [['%exist,ASSOCRIGHT isubst,applySubst(sl,applySubst(isubst,icond))]]
+ nil
mms := nil
for (entry:= [[op,sig,:.],pred,sel]) in opAlist |
listMember?(sig,LASSOC(op,nonCategorySigAlist)) repeat
- pred' := MKPF([pred,:catPredList],'AND)
+ pred' := mkpf([pred,:catPredList,:cond],'AND)
modemap := [["*1",:sig],[pred',sel]]
mms := [[op,:interactiveModemapForm modemap],:mms]
mms
@@ -215,6 +219,10 @@ modemapsFromFunctor(db,form,opAlist) ==
$e := put(u,'mode,v,$e)
nonCategorySigAlist :=
mkAlistOfExplicitCategoryOps signature.target or return nil
+ catCond :=
+ dbImplicitData db is [isubst,icond] =>
+ [['%exist,ASSOCRIGHT isubst,applySubst(f2p,applySubst(isubst,icond))]]
+ nil
mms := nil
for (entry := [[op,sig,:.],pred,sel]) in opAlist |
or/[listMember?(sig,catSig) for catSig in
@@ -235,7 +243,7 @@ modemapsFromFunctor(db,form,opAlist) ==
'"by pattern match" ]
skip := 'SKIP
modemap := [[form,:substitute(form,"$",sig)],
- [mkpf([pred,:predList],'AND),
+ [mkpf([pred,:predList,:catCond],'AND),
substitute(form,"$",sel),:skip]]
mms := [[op,:interactiveModemapForm modemap],:mms]
mms
diff --git a/src/interp/define.boot b/src/interp/define.boot
index ce4b8bbc..a90d49fc 100644
--- a/src/interp/define.boot
+++ b/src/interp/define.boot
@@ -994,6 +994,11 @@ mkCategoryPackage(form is [op,:argl],cat,def) ==
$categoryPredicateList := substitute(nameForDollar,'$,$categoryPredicateList)
substitute(nameForDollar,'$,['DEF,[packageName,:packageArgl],packageSig,def])
+++ Return the typing constraint operator for `t' in the environment `e'.
+typingKind(t,e) ==
+ isCategoryForm(t,e) => 'ofCategory
+ 'ofType
+
++ Subroutine of compDefineFunctor1 and compDefineCategory2.
++ Given a constructor definition defining `db', compute implicit
++ parameters and store that list in `db'.
@@ -1012,12 +1017,13 @@ deduceImplicitParameters(db,e) ==
stackAndThrow('"Parameter %1b cannot be of type implicit parameter %2pb",
[p,m])
m isnt [.,:.] => nil
- q :=
- isCategoryForm(m,e) => 'ofCategory
- 'isDomain
- preds := [[q,dbSubstituteFormals(db,p),m],:preds]
- st := [[a,:v] for a in m.args for [v,:qvars] in tails qvars
- | ident? a and symbolMember?(a,nonparms)]
+ preds := [[typingKind(m,e),dbSubstituteFormals(db,p),m],:preds]
+ st := [qpair for a in m.args for [v,:qvars] in tails qvars
+ | ident? a and symbolMember?(a,nonparms)] where
+ qpair() ==
+ t := getXmode(a,e)
+ preds := [[typingKind(t,e),a,t],:preds]
+ [a,:v]
subst := [:st,:subst]
-- Now, build the predicate for implicit parameters.
for s in nonparms repeat