-- Copyright (c) 1991-2002, The Numerical Algorithms Group Ltd. -- All rights reserved. -- Copyright (C) 2007-2012, Gabriel Dos Reis. -- All rights reserved. -- -- Redistribution and use in source and binary forms, with or without -- modification, are permitted provided that the following conditions are -- met: -- -- - Redistributions of source code must retain the above copyright -- notice, this list of conditions and the following disclaimer. -- -- - Redistributions in binary form must reproduce the above copyright -- notice, this list of conditions and the following disclaimer in -- the documentation and/or other materials provided with the -- distribution. -- -- - Neither the name of The Numerical Algorithms Group Ltd. nor the -- names of its contributors may be used to endorse or promote products -- derived from this software without specific prior written permission. -- -- THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS -- IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED -- TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A -- PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER -- OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, -- EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, -- PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR -- PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF -- LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING -- NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS -- SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. import c_-util import g_-cndata namespace BOOT --% ++ List of global attributes. $Attributes := [] --% ++ Returns true if `a' is a category (runtime) object. categoryObject?: %Thing -> %Boolean categoryObject? a == vector? a and #a > 5 and vectorRef(a,3) = $Category ++ Return true if the form `x' designates an instantiaion of a ++ category constructor known to the global database or the ++ envronement `e'. isCategoryForm: (%Form,%Env) -> %Boolean isCategoryForm(x,e) == if x isnt [.,:.] then x := macroExpand(x,e) x isnt [.,:.] => ident? x and getmode(x,e) = $Category getConstructorKind(x.op) is 'category -- FIXME: check arguments too. ++ Returns a freshly built category object for a domain or package ++ (as indicated by `domainOrPackage'), with signature list ++ designated by `sigList', attribute list designated by `attList', ++ used domains list designated by `domList', and a princical ancestor ++ category object designated by `principal'. mkCategory: (%ConstructorKind,%List %Sig,%List %Form,%List %Instantiation, %Maybe %Shell) -> %Shell mkCategory(domainOrPackage,sigList,attList,domList,principal) == NSigList := nil -- Unless extending a principal ancestor (from the end), start -- from the first free, unencumbered slot. count := principal = nil => $NRTbase #principal sigList:= [if s is [sig,pred] then -- Don't retain duplicate signatures. -- ??? Should we not check for predicate subsumption too? or/[x is [[ =sig,.,:impl],:num] for x in NSigList] => [sig,pred,:impl] --only needed for multiple copies of sig num := domainOrPackage is "domain" => count count-5 nsig := mkOperatorEntry(sig,pred,num) NSigList := [[nsig,:count],:NSigList] count := count+1 nsig else s for s in sigList] NewLocals:= nil for s in sigList repeat NewLocals:= union(NewLocals,Prepare s.mmTarget) where Prepare u == "union"/[Prepare2 v for v in u] Prepare2 v == v is '$ => nil string? v => nil v isnt [.,:.] => [v] v.op is 'Union => "union"/[Prepare2 x for x in stripTags v.args] v.op is 'Mapping => "union"/[Prepare2 x for x in v.args] v.op is 'Record => "union"/[Prepare2 third x for x in v.args] v.op is 'Enumeration => nil [v] OldLocals:= nil -- Remove possible duplicate local domain caches. if principal then for u in (OldLocals := categoryLocals principal) repeat NewLocals := remove(NewLocals,first u) -- New local domains caches are hosted in slots at the end onward for u in NewLocals repeat OldLocals := [[u,:count],:OldLocals] count := count+1 -- Build a fresh category object stuffed with all updated information v := newShell count canonicalForm(v) := nil categoryExports(v) := sigList categoryAttributes(v) := attList categoryRef(v,3) := $Category if principal ~= nil then for x in $NRTbase..#principal-1 repeat categoryRef(v,x) := categoryRef(principal,x) categoryAssociatedTypes(v) := [categoryPrincipals principal, categoryAncestors principal, OldLocals] else categoryAssociatedTypes(v) := [nil,nil,OldLocals] categoryRef(v,5) := domList for [nsig,:n] in NSigList repeat categoryRef(v,n) := nsig v --% Subsumption code (for operators) DropImplementations a == a is [sig,pred,[q,:.]] and q in '(ELT CONST) => q = "ELT" => [sig,pred] [[:sig,'constant],pred] a SigListUnion(extra,original,principal,tbl) == --augments original %with everything in extra that is not in original for (o:=[[ofn,osig,:.],opred,:.]) in original repeat -- The purpose of this loop is to detect cases when the -- original list contains, e.g. ** with NonNegativeIntegers, and -- the extra list would like to add ** with PositiveIntegers. -- The PI map is therefore gives an implementation of "Subsumed" for x in SigListOpSubsume(o,extra) repeat [[xfn,xsig,:.],xpred,:.] := x symbolEq?(xfn,ofn) and xsig = osig => --checking name and signature, but not a 'constant' marker xpred = opred => extra := remove(extra,x) --same signature and same predicate opred = true => extra := remove(extra,x) -- PRETTYPRINT ("we ought to subsume",x,o) not MachineLevelSubsume(first o,first x) => '"Source level subsumption not implemented" extra := remove(extra,x) for e in extra repeat [esig,epred,:.]:= e eimplem:=[] for x in SigListOpSubsume(e,original) repeat --PRETTYPRINT(["SigListOpSubsume",e,x]) not MachineLevelSubsume(first e,first x) => --systemError '"Source level subsumption not implemented" original:= [e,:original] return nil -- this exits from the innermost for loop original := remove(original,x) [xsig,xpred,:ximplem]:= x -- if xsig ~= esig then -- not quite strong enough if first xsig ~= first esig or second xsig ~= second esig then -- the new version won't get confused by "constant"markers if ximplem is [["Subsumed",:.],:.] then original := [x,:original] else original:= [[xsig,xpred,["Subsumed",:esig]],:original] else epred := mkOr(epred,xpred,tbl,$e) -- this used always to be done, as noted below, but that's not safe if not(ximplem is [["Subsumed",:.],:.]) then eimplem:= ximplem if eimplem then esig:=[first esig,second esig] -- in case there's a constant marker e:= [esig,epred,:eimplem] -- e:= [esig,mkOr(xpred,epred,tbl,$e),:ximplem] -- Original version -gets it wrong if the new operator is only -- present under certain conditions -- We must pick up the previous implementation, if any --+ if ximplem is [[q,.,index]] and integer? index and (q="ELT" or q="CONST") then bufferRef(principal,index) := e original:= [e,:original] original mkOr: (%Form,%Form,%Table,%Env) -> %Form mkOr(a,b,tbl,e) == a=true => true b=true => true b=a => a l:= a is ["OR",:a'] => (b is ["OR",:b'] => union(a',b'); mkOr2(b,a',tbl,e) ) b is ["OR",:b'] => mkOr2(a,b',tbl,e) (a is ["has",avar,acat]) and (b is ["has",=avar,bcat]) => descendant?(acat,bcat,tbl,e) => [b] descendant?(bcat,acat,tbl,e) => [a] [a,b] a is ['AND,:a'] and listMember?(b,a') => [b] b is ['AND,:b'] and listMember?(a,b') => [a] a is ["and",:a'] and listMember?(b,a') => [b] b is ["and",:b'] and listMember?(a,b') => [a] [a,b] #l = 1 => first l ["OR",:l] mkOr2: (%Form,%Form,%Table,%Env) -> %Form mkOr2(a,b,tbl,e) == --a is a condition, "b" a list of them listMember?(a,b) => b a is ["has",avar,acat] => aRedundant:=false for c in b | c is ["has",=avar,ccat] repeat descendant?(acat,ccat,tbl,e) => return (aRedundant:=true) if descendant?(ccat,acat,tbl,e) then b := remove(b,c) aRedundant => b [a,:b] [a,:b] mkAnd: (%Form,%Form,%Table,%Env) -> %Form mkAnd(a,b,tbl,e) == a=true => b b=true => a b=a => a l:= a is ["AND",:a'] => (b is ["AND",:b'] => union(a',b'); mkAnd2(b,a',tbl,e) ) b is ["AND",:b'] => mkAnd2(a,b',tbl,e) (a is ["has",avar,acat]) and (b is ["has",=avar,bcat]) => descendant?(acat,bcat,tbl,e) => [a] descendant?(bcat,acat,tbl,e) => [b] [a,b] [a,b] #l = 1 => first l ["AND",:l] mkAnd2: (%Form,%Form,%Table,%Env) -> %Form mkAnd2(a,b,tbl,e) == --a is a condition, "b" a list of them listMember?(a,b) => b a is ["has",avar,acat] => aRedundant:=false for c in b | c is ["has",=avar,ccat] repeat descendant?(ccat,acat,tbl,e) => return (aRedundant:=true) if descendant?(acat,ccat,tbl,e) then b := remove(b,c) aRedundant => b [a,:b] [a,:b] ++ Return true if `a implies b' in the logical sense. predicateImplies(a,b) == b is true => true a is true => false a = b -- for now. SigListOpSubsume([[name1,sig1,:.],:.],list) == --does m subsume another operator in the list? --see "operator subsumption" in JHD's report --if it does, returns the subsumed member lsig1 := #sig1 ans := [] for (n:=[[name2,sig2,:.],:.]) in list | symbolEq?(name1,name2) repeat lsig1 = #sig2 and sig1 = sig2 => ans := [n,:ans] return ans MachineLevelSubsume([name1,[out1,:in1],:flag1],[name2,[out2,:in2],:flag2]) == -- Checks for machine-level subsumption -- true if the first signature subsumes the second -- flag1 = flag2 and: this really should be checked, but symbolEq?(name1,name2) and MachineLevelSubset(out1,out2) and (and/[MachineLevelSubset(inarg2,inarg1) for inarg1 in in1 for inarg2 in in2] ) MachineLevelSubset(a,b) == --true if a is a machine-level subset of b a=b => true b is ["Union",:blist] and listMember?(a,blist) and (and/[string? x for x in blist | x~=a]) => true --all other branches must be distinct objects not null isSubDomain(a,b) --we assume all subsets are true at the machine level --% Ancestor chasing code ++ Subroutine of JoinInner. ++ Given a list `l' of 2-list [cat,pred] of category object and associated ++ predicate, return a list of similar structures of all fundamental ++ ancestors with appropriate conditions. FindFundAncs(l,tbl,e) == l = nil => nil [hd:=[f1,p1],:l] := l canonicalForm f1 = nil => FindFundAncs(l,tbl,e) ans := FindFundAncs(l,tbl,e) for u in FindFundAncs([[CatEval(first x,tbl,e),mkAnd(p1,second x,tbl,e)] for x in categoryAncestors f1],tbl,e) repeat x := objectAssoc(first u,ans) => ans := [[first u,mkOr(second x,second u,tbl,e)],:remove(ans,x)] ans := [u,:ans] --testing to see if hd is already there x := objectAssoc(f1,ans) => [[f1,mkOr(p1,second x,tbl,e)],:remove(ans,x)] p1 is true => for x in categoryPrincipals f1 repeat if y := objectAssoc(CatEval(x,tbl,e),ans) then ans := remove(ans,y) [hd,:ans] for x in categoryPrincipals f1 repeat if y := objectAssoc(CatEval(x,tbl,e),ans) then ans:= [[first y,mkOr(p1,second y,tbl,e)],:remove(ans,y)] [hd,:ans] -- Our new thing may have, as an alternate view, a principal -- descendant of something previously added which is therefore -- subsumed CatEval: (%Thing,%Table,%Env) -> %Shell CatEval(x,tbl,e) == vector? x => x if $InteractiveMode then e := $CategoryFrame getCategoryObject(tbl,x,e) ancestor?: (%Form,%List %Instantiation,%Table,%Env) -> %Form ancestor?(xname,leaves,tbl,env) == -- checks for being a principal ancestor of one of the leaves listMember?(xname,leaves) => xname for y in leaves repeat listMember?(xname,categoryPrincipals CatEval(y,tbl,env)) => return y conditionalAncestor?(xname,leaves,condition,tbl,env) == -- checks for being a principal ancestor of one of the leaves for u in leaves repeat u':=first u ucond:= null rest u => true second u xname = u' or listMember?(xname,categoryPrincipals CatEval(u',tbl,env)) => predicateImplies(condition,ucond) => return u' ++ Returns true if the form `a' designates a category that is any ++ kind of descendant of the category designated by the form `b'. descendant?: (%Form,%Form,%Table,%Env) -> %Boolean descendant?(a,b,tbl,e) == a=b => true a is ["ATTRIBUTE",:.] => false a is ["SIGNATURE",:.] => false a:= CatEval(a,tbl,e) b is ["ATTRIBUTE",b'] => (l := assoc(b',categoryAttributes a)) => TruthP second l listMember?(b,categoryPrincipals a) => true ancestor?(b,[first u for u in categoryAncestors a],tbl,e) --% The implementation of Join ++ We have a list `l' of category objects to be joined. ++ Some of them may harbor other categories that exist only under ++ certain conditions. Collect all those that are indisputably conditional ++ and attempt to detect those apparent conditional categories whose ++ predicates are satified in the current elaboration environment. ++ The end result is a 2-list, the first component being a list of ++ (catobj,pred) pairs and the second component being the list of ++ newly discovered unconditional categories. filterConditionalCategories(l,tbl,e) == conditionals := nil unconditionals := nil for cat in l repeat for [at,pred] in categoryAttributes cat repeat if at isnt [.,:.] then at := [at] -- the variable $Attributes is built globally, so that true -- attributes can be detected without calling isCategoryForm symbolMember?(first at,$Attributes) => nil not isCategoryForm(at,e) => $Attributes := [first at,:$Attributes] listMember?(pred,get("$Information","special",e)) => --It's true, so we add it as unconditional unconditionals := [CatEval(at,tbl,e),:unconditionals] pred isnt ['and,:.] => conditionals := [[CatEval(at,tbl,e),pred],:conditionals] -- Predicate is a conjunctive; decompose it. pred' := [x for x in pred.args | not listMember?(x,get("$Information","special",e)) and x isnt true] pred' = nil => unconditionals := [CatEval(at,tbl,e),:unconditionals] pred' is [x] => conditionals := [[CatEval(at,tbl,e),x],:conditionals] conditionals := [[CatEval(at,tbl,e),mkpf(pred','and)],:conditionals] [conditionals,reverse! unconditionals] JoinInner(l,$e) == tbl := makeTable function valueEq? [CondList,uncondList] := filterConditionalCategories(l,tbl,$e) [principal,:l] := [:l,:uncondList] principal := mkBuffer principal l' := [:CondList,:[[u,true] for u in l]] -- This is a list of all the categories that this extends -- conditionally or unconditionally sigl := categoryExports bufferData principal attl := categoryAttributes bufferData principal globalDomains := categoryParameters bufferData principal FundamentalAncestors := categoryAncestors bufferData principal if name := canonicalForm bufferData principal then FundamentalAncestors := [[name],:FundamentalAncestors] -- this skips buggy code which discards needed categories for [b,condition] in FindFundAncs(l',tbl,$e) | bname := b.0 repeat conditionalAncestor?(bname,FundamentalAncestors,condition,tbl,$e) => nil f := ancestor?(bname,[first u for u in FundamentalAncestors],tbl,$e) => [.,.,index] := assoc(f,FundamentalAncestors) FundamentalAncestors := [[bname,condition,index],:FundamentalAncestors] PrinAncb := categoryPrincipals CatEval(bname,tbl,$e) --Principal Ancestors of b reallynew := true -- This loop implements Category Subsumption for anc in FundamentalAncestors | listMember?(first anc,PrinAncb) repeat if rest anc then anccond := second anc ancindex := third anc else anccond := true ancindex := nil if predicateImplies(anccond,condition) then FundamentalAncestors := -- the new 'b' is more often true than the old one 'anc' [[bname,condition,ancindex],:remove(FundamentalAncestors,anc)] else if ancindex then --the new 'b' is less often true newentry := [bname,condition,ancindex] if not listMember?(newentry,FundamentalAncestors) then FundamentalAncestors := [newentry,:FundamentalAncestors] else ancindex := nil if ancindex then bufferRef(principal,ancindex) := bname reallynew := false if reallynew then n := bufferLength principal FundamentalAncestors := [[b.0,condition,n],:FundamentalAncestors] resizeBuffer(principal,n + 1) bufferRef(principal,n) := b.0 for b in l repeat sigl := SigListUnion([DropImplementations u for u in categoryExports b], sigl,principal,tbl) attl := S_+(categoryAttributes b,attl) globalDomains := [:globalDomains,:S_-(categoryParameters b,globalDomains)] for b in CondList repeat newpred := second b for u in categoryAttributes first b repeat v := assoc(first u,attl) null v => attl := [[first u,mkpf([newpred,second u],'and)],:attl] second v is true => nil attl := remove(attl,v) attl := second u is true => [[first u,mkOr(second v,newpred,tbl,$e)],:attl] [[first u,mkOr(second v,mkAnd(newpred,second u,tbl,$e),tbl,$e)],:attl] sigl := SigListUnion( [AddPredicate(DropImplementations u,newpred) for u in categoryExports(first b)],sigl,principal,tbl) where AddPredicate(op is [sig,oldpred,:implem],newpred) == newpred is true => op oldpred is true => [sig,newpred,:implem] [sig,mkpf([oldpred,newpred],'and),:implem] FundamentalAncestors := [x for x in FundamentalAncestors | rest x] --strip out the pointer to Principal Ancestor c := categoryPrincipals bufferData principal pName := canonicalForm bufferData principal if pName and not listMember?(pName,c) then c := [pName,:c] categoryAssociatedTypes(bufferData principal) := [c,FundamentalAncestors,categoryLocals bufferData principal] mkCategory("domain",sigl,attl,globalDomains,bufferToVector principal) Join(:l) == l = nil => mkCategory("domain",nil,nil,nil,nil) e := null $e or $InteractiveMode => $CategoryFrame $e JoinInner(l, e)