diff options
Diffstat (limited to 'sucl/complete.icl')
| -rw-r--r-- | sucl/complete.icl | 148 |
1 files changed, 0 insertions, 148 deletions
diff --git a/sucl/complete.icl b/sucl/complete.icl deleted file mode 100644 index 136db40..0000000 --- a/sucl/complete.icl +++ /dev/null @@ -1,148 +0,0 @@ -implementation module complete - -// $Id$ - -import graph -import basic -import StdEnv - -/* - -To check completeness of patterns, we need to know whether, given a list -of (constructor) symbols, this list completely covers a type. - - complete :: [sym] -> Bool - -It is assumed that a type can never be empty, so an empty list of -constructors can never cover a type. Otherwise, separate type -information would be needed to determine the completeness of an empty -list of constructors. - - -The algorithm uses /multipatterns/, which are lists of simple patterns. A -multipattern is used to match at multiple node-ids in a graph in parallel. -This is necessary in the case of matching of product types. - -*/ - -:: Pattern sym var - :== (Graph sym var,[var]) - -/* - -Coveredby checks whether a multipattern is covered by a list of -multipatterns. There are five cases to consider. - - First, if the multipattern is not the empty list, then to cover it - some multipattern must exist, so if the list of multipatterns is - empty, then the multipattern is not covered. - - Second, if the multipattern is the empty list, it is trivially - covered by any list of multipatterns, including the empty. - - Third, if the first pattern of the multipattern is closed, we select - only the multipatterns that it can match, then continue with the - arguments, and then the rest of the multipattern. - - Fourth, if the first pattern of the multipattern is open, and all - its type constructors are present in the first patterns of the - multipatterns in the list of multipatterns, then the first pattern - of the multipattern is split according to all constructors, and all - possibilities must be covered. - - Fifth, if not all constructors are present, then the multipatterns - of which the first pattern is open must cover the multipattern. So - those are selected and we continue with the tails of the - multipatterns in this list. - -To understand the order of the first two cases, check how a single open -integer pattern is covered by a list of integer patterns either -containing or not containing an open pattern. - -*/ - -coveredby - :: ([sym]->Bool) - (Graph sym var) - ![Pattern sym pvar] - [var] - -> Bool - | == sym - & == var - & == pvar - -coveredby complete subject [] svars = False -coveredby complete subject pvarss [] = True -coveredby complete subject pvarss [svar:svars] -| sdef -= coveredby complete subject tmpvalue (sargs++svars) -| complete (map fst3 closeds) -= and (map covered closeds) -= coveredby complete subject opens svars - where (opens,closeds) = psplit pvarss - covered (sym,repvar`,pvarss`) = coveredby complete subject pvarss` (repvar (repvar` dummyvar) svar++svars) - (sdef,(ssym,sargs)) = varcontents subject svar - tmpvalue = (fst (foldr (spl (repvar sargs) ssym) ([],[]) pvarss)) - dummyvar = abort "complete: error: accessing dummy variable" - -repvar pvars svar = map (const svar) pvars - -/* - -Split splits a list of multipatterns into parts; on one hand, those of -which the first pattern is open, and on the other hand, for every -constructor, the list of applicable multipatterns, in which case the -multipatterns with an open pattern are expanded and added as well. - -*/ - -psplit - :: [Pattern sym var] - -> ( [Pattern sym var] - , [ ( sym - , var->[var] - , [Pattern sym var] - ) - ] - ) - | == sym - & == var - -psplit [] = ([],[]) -psplit [(subject,[svar:svars]):svarss] -| not sdef -= ([(subject,svars):opens`],map add closeds`) -= (opens,[(ssym,repvar,[(subject,sargs++svars):ins]):closeds]) - where (opens`,closeds`) = psplit svarss - add (sym,repvar,svarss`) = (sym,repvar,[(subject,repvar svar++svars):svarss`]) - (opens,closeds) = psplit outs - (ins,outs) = foldr (spl repvar ssym) ([],[]) svarss - repvar svar = map (const svar) sargs - (sdef,(ssym,sargs)) = varcontents subject svar - -/* - -Spl, given a symbol, derives two lists of multipatterns from one. The -first are the multipatterns of which the first pattern can match the -symbol, i.e. open ones and closed ones with the correct symbol. The -second are the multipatterns that can match other symbols, i.e. also -open ones, and closed ones with the wrong symbol. - -*/ - -spl - :: (var -> [var]) - sym - (Pattern sym var) - ([Pattern sym var],[Pattern sym var]) - -> ([Pattern sym var],[Pattern sym var]) - | == sym - & == var - -spl repvar sym (subject,[svar:svars]) (ins,outs) -| not sdef -= ([(subject,repvar svar++svars):ins],[(subject,[svar:svars]):outs]) -| ssym==sym -= ([(subject,sargs++svars):ins],outs) -= (ins,[(subject,[svar:svars]):outs]) - where (sdef,(ssym,sargs)) = varcontents subject svar |