This commit was generated by cvs2svn to compensate for changes in r599,

which included commits to RCS files with non-trunk default branches.

git-svn-id: https://svn.cs.ru.nl/repos/clean-compiler/trunk@600 1f8540f1-abd5-4d5b-9d24-4c5ce8603e2d

10 files changed, 260 insertions, 23 deletions

diff --git a/sucl/Makefile b/sucl/Makefile
index 7f462df..7732f75 100644
--- a/sucl/Makefile
+++ b/sucl/Makefile
@@ -6,7 +6,7 @@ COCL = cocl
 #COCLFLAGS = -lat
 SYS = Clean\ System\ Files
 
-MODULES = basic pretty pfun graph dnc rule trd rewr complete history spine trace absmodule spine strat loop law coreclean convert supercompile
+MODULES = basic pretty pfun graph dnc rule trd rewr complete history spine trace absmodule strat loop coreclean law canon cli extract newfold newtest convert supercompile
 
 ABC = $(patsubst %,$(SYS)/%.abc,$(MODULES))
 
@@ -25,10 +25,11 @@ tags: *.dcl *.icl ../compiler/*.dcl ../compiler/*.icl
 $(SYS)/%.abc: %.icl
 	$(COCL) $(COCLFLAGS) $*
 
-$(SYS)/supercompile.abc: supercompile.icl supercompile.dcl
-$(SYS)/convert.abc: convert.icl convert.dcl coreclean.dcl rule.dcl
-$(SYS)/coreclean.abc: coreclean.icl coreclean.dcl
-$(SYS)/law.abc: law.icl law.dcl
+$(SYS)/supercompile.abc: supercompile.icl supercompile.dcl convert.dcl
+$(SYS)/convert.abc: convert.icl convert.dcl coreclean.dcl rule.dcl graph.dcl basic.dcl
+$(SYS)/cli.abc: cli.icl cli.dcl absmodule.dcl coreclean.dcl law.dcl strat.dcl rule.dcl basic.dcl
+$(SYS)/coreclean.abc: coreclean.icl coreclean.dcl strat.dcl spine.dcl rule.dcl graph.dcl
+$(SYS)/law.abc: law.icl law.dcl coreclean.dcl strat.dcl spine.dcl rule.dcl graph.dcl dnc.dcl basic.dcl
 $(SYS)/loop.abc: loop.icl loop.dcl trace.dcl strat.dcl history.dcl rule.dcl graph.dcl basic.dcl
 $(SYS)/strat.abc: strat.icl strat.dcl history.dcl spine.dcl dnc.dcl rule.dcl graph.dcl pfun.dcl basic.dcl
 $(SYS)/history.abc: history.icl history.dcl spine.dcl rule.dcl graph.dcl basic.dcl
diff --git a/sucl/absmodule.dcl b/sucl/absmodule.dcl
index 2cf9a35..ccea9f3 100644
--- a/sucl/absmodule.dcl
+++ b/sucl/absmodule.dcl
@@ -5,11 +5,11 @@ definition module absmodule
 from rule import Rule
 
 :: Module sym pvar tsym tvar
-   = { exportedtypesymbols :: [tsym]                        // Exported type symbols (from DCL)
-     , typealias           :: [(tsym,Rule tsym tvar)]       // Alias types
-     , typeconstructors    :: [(tsym,[sym])]                // All constructor symbols of each declared algebraic type
-     , exportedsymbols     :: [sym]                         // Exported function/constructor symbols
-     , aliases             :: [(sym,Rule sym pvar)]         // Macros
-     , typerules           :: [(sym,Rule tsym tvar,[Bool])] // Info from type rules (actual type and argument strictnesses)
-     , rules               :: [(sym,[Rule sym pvar])]       // Rewrite rules of each symbol, absent if imported
+   = { exportedtypesymbols :: [tsym]                            // Exported type symbols (from DCL)
+     , typealias           :: [(tsym,Rule tsym tvar)]           // Alias types
+     , typeconstructors    :: [(tsym,[sym])]                    // All constructor symbols of each declared algebraic type
+     , exportedsymbols     :: [sym]                             // Exported function/constructor symbols
+     , aliases             :: [(sym,Rule sym pvar)]             // Macros
+     , typerules           :: [(sym,(Rule tsym tvar,[Bool]))]   // Info from type rules (actual type and argument strictnesses)
+     , rules               :: [(sym,[Rule sym pvar])]           // Rewrite rules of each symbol, absent if imported
      }
diff --git a/sucl/absmodule.icl b/sucl/absmodule.icl
index 3f30317..f18ecc6 100644
--- a/sucl/absmodule.icl
+++ b/sucl/absmodule.icl
@@ -42,13 +42,13 @@ Module implementation.
 */
 
 :: Module sym pvar tsym tvar
-   = { exportedtypesymbols :: [tsym]                        // Exported type symbols (from DCL)
-     , typealias           :: [(tsym,Rule tsym tvar)]       // Alias types
-     , typeconstructors    :: [(tsym,[sym])]                // All constructor symbols of each declared algebraic type
-     , exportedsymbols     :: [sym]                         // Exported function/constructor symbols
-     , aliases             :: [(sym,Rule sym pvar)]         // Macros
-     , typerules           :: [(sym,Rule tsym tvar,[Bool])] // Info from type rules (actual type and argument strictnesses)
-     , rules               :: [(sym,[Rule sym pvar])]       // Rewrite rules of each symbol, absent if imported
+   = { exportedtypesymbols :: [tsym]                            // Exported type symbols (from DCL)
+     , typealias           :: [(tsym,Rule tsym tvar)]           // Alias types
+     , typeconstructors    :: [(tsym,[sym])]                    // All constructor symbols of each declared algebraic type
+     , exportedsymbols     :: [sym]                             // Exported function/constructor symbols
+     , aliases             :: [(sym,Rule sym pvar)]             // Macros
+     , typerules           :: [(sym,(Rule tsym tvar,[Bool]))]   // Info from type rules (actual type and argument strictnesses)
+     , rules               :: [(sym,[Rule sym pvar])]           // Rewrite rules of each symbol, absent if imported
      }
 
 /*
diff --git a/sucl/basic.dcl b/sucl/basic.dcl
index b288043..be3260a 100644
--- a/sucl/basic.dcl
+++ b/sucl/basic.dcl
@@ -53,6 +53,9 @@ disjoint :: .[elem] !.[elem] -> Bool | == elem
 // `Eqlen xs ys' determines whether `xs' and `ys' are equally long.
 eqlen :: ![.elem1] ![.elem2] -> .Bool
 
+// Extend a function using the elements of a mapping
+extendfn :: [(src,dst)] (src->dst) src -> dst | == src
+
 // `Foldlm' is a combination of foldl and map.
 foldlm :: ((.collect,.elem) -> (.collect,.elem`)) !(.collect,![.elem]) -> (.collect,[.elem`])
 
diff --git a/sucl/basic.icl b/sucl/basic.icl
index 86770b5..a508599 100644
--- a/sucl/basic.icl
+++ b/sucl/basic.icl
@@ -71,6 +71,10 @@ eqlen [x:xs] [y:ys] = eqlen xs ys
 eqlen [] [] = True
 eqlen xs ys = False
 
+// Extend a function using the elements of a mapping
+extendfn :: [(src,dst)] (src->dst) src -> dst | == src
+extendfn mapping f x = foldmap id (f x) mapping x
+
 // `Foldlm' is a combination of foldl and map.
 foldlm :: ((.collect,.elem) -> (.collect,.elem`)) !(.collect,![.elem]) -> (.collect,[.elem`])
 foldlm f (l,[]) = (l,[])
diff --git a/sucl/cli.icl b/sucl/cli.icl
index 88bbe6e..3e1c8ae 100644
--- a/sucl/cli.icl
+++ b/sucl/cli.icl
@@ -2,6 +2,14 @@ implementation module cli
 
 // $Id$
 
+import absmodule
+import coreclean
+import law
+import strat
+import rule
+import basic
+import StdEnv
+
 /*
 
 cli.lit - Clean implementation modules
@@ -94,7 +102,11 @@ Abstype implementation.
 >        aliases :: cli -> [(typesymbol,rule typesymbol typenode)]
 >        macros :: cli -> [(symbol,rule symbol node)]
 >        stripexports :: [char] -> cli -> cli
+*/
 
+:: Cli :== Module SuclSymbol SuclVariable SuclTypeSymbol SuclTypeVariable
+
+/*
 >   cli == module symbol node typesymbol typenode
 
 >   readcli = compilecli.readcleanparts
@@ -126,13 +138,26 @@ Abstype implementation.
 >       ) (corestrategy matchable)         ||  Checks rules for symbols in the language core (IF, _AP, ...)
 >       where islocal (User m i) = member (map fst rs) (User m i)
 >             islocal rsym = True ||  Symbols in the language core are always completely known
+*/
+
+clistrategy :: Cli ((Graph SuclSymbol SuclVariable) SuclVariable var -> Bool) -> Strategy SuclSymbol var SuclVariable answer | == var
+clistrategy cli=:{exportedtypesymbols=tes,typealias=tas,typeconstructors=tcs,exportedsymbols=es,aliases=as,typerules=ts,rules=rs} matchable
+ = ( checkarity (typearity o maxtypeinfo ts)        // Checks curried occurrences and strict arguments
+   o checklaws cleanlaws                            // Checks for special (hard coded) rules (+x0=x /y1=y ...)
+   o checkrules matchable (foldmap id [] rs)        // Checks normal rewrite rules
+   o checkimport islocal                            // Checks for delta symbols
+   o checkconstr (flip isMember (flatten (map snd tcs))) // Checks for constructors
+   ) (corestrategy matchable)                       // Checks rules for symbols in the language core (IF, _AP, ...)
+   where islocal rsym=:(SuclUser s) = isMember rsym (map fst rs)
+         islocal rsym = True                        // Symbols in the language core are always completely known
 
->   maxtypeinfo :: [(symbol,(rule typesymbol typenode,[bool]))] -> symbol -> (rule typesymbol typenode,[bool])
->   maxtypeinfo ts = extendfn ts coretypeinfo
+typearity :: (Rule SuclTypeSymbol SuclTypeVariable,[Bool]) -> Int
+typearity ti = length (arguments (fst ti))
 
->   extendfn :: [(*,**)] -> (*->**) -> * -> **
->   extendfn mapping f x = foldmap id (f x) mapping x
+maxtypeinfo :: [(SuclSymbol,(Rule SuclTypeSymbol SuclTypeVariable,[Bool]))] SuclSymbol -> (Rule SuclTypeSymbol SuclTypeVariable,[Bool])
+maxtypeinfo defs sym = extendfn defs coretypeinfo sym
 
+/*
 >   constrs ((tes,tas,tcs),defs) = tcs
 
 >   complete ((tes,tas,tcs),(es,as,ts,rs)) = mkclicomplete tcs (fst.maxtypeinfo ts)
diff --git a/sucl/law.dcl b/sucl/law.dcl
index e17f005..e136b46 100644
--- a/sucl/law.dcl
+++ b/sucl/law.dcl
@@ -1,3 +1,19 @@
 definition module law
 
 // $Id$
+
+from coreclean import SuclSymbol,SuclVariable
+from strat import Law,Strategy
+from StdOverloaded import ==
+
+// Transitive necessities
+
+from strat import Substrategy
+from spine import Spine,Subspine
+from graph import Graph,Node
+
+// The list of special Clean transformation laws
+cleanlaws :: [(SuclSymbol,Law SuclSymbol var SuclVariable result)]
+
+// The strategy for built in clean symbols
+corestrategy :: ((Graph SuclSymbol SuclVariable) SuclVariable var -> Bool) -> Strategy SuclSymbol var SuclVariable result | == var
diff --git a/sucl/law.icl b/sucl/law.icl
index b8cede6..1f14ee4 100644
--- a/sucl/law.icl
+++ b/sucl/law.icl
@@ -2,6 +2,15 @@ implementation module law
 
 // $Id$
 
+import coreclean
+import strat
+import spine
+import rule
+import graph
+import dnc
+import basic
+import StdEnv
+
 /*
 
 >   %export
@@ -101,7 +110,12 @@ implementation module law
 ------------------------------------------------------------------------
 
 >   cleanlaws :: [(symbol,law symbol ** node ****)]
+*/
 
+cleanlaws :: [(SuclSymbol,Law SuclSymbol var SuclVariable result)]
+cleanlaws =: []
+
+/*
 >   cleanlaws
 >   =   [(User "deltaI" "*",law) | law <- mullaws] ++
 >       [(User "deltaI" "+",law) | law <- addlaws] ++
@@ -134,7 +148,24 @@ Also, using trylaw is easier
 
 >   corestrategy matchable substrat subject found rnf (ssym,snodes)
 >   =   rnf
+*/
+
+// The strategy for built in clean symbols
+corestrategy :: ((Graph SuclSymbol SuclVariable) SuclVariable var -> Bool) -> Strategy SuclSymbol var SuclVariable result | == var
+corestrategy matchable =(\ substrat subject found rnf snode
+ -> let (ssym,sargs) = snode
+    in case ssym
+       of SuclUser sptr
+           -> found MissingCase
+          SuclCase eptr
+           -> found MissingCase
+          SuclApply argc
+           -> trylaw subject found sargs (applyrule nc) (found Delta)
+              where nc = dnc (const "in corestrategy") subject (hd sargs)
+          _
+           -> rnf)
 
+/*
 >   applyrule :: (bool,(*,[**])) -> rule * node
 >   applyrule (sdef,scont)
 >   =   aprule (anode,(sym,aargs)) [enode] aroot
@@ -143,7 +174,17 @@ Also, using trylaw is easier
 >             =   scont, if sdef
 >             =   (nosym,[]), otherwise
 >             nosym = error "applyrule: no function symbol available"
+*/
+
+applyrule :: (Bool,Node sym var) -> Rule sym SuclVariable
+applyrule (sdef,scont)
+ = aprule (anode,(sym,aargs)) [enode] aroot
+   where (aargs,[anode,aroot,enode:_]) = claim sargs suclheap
+         (sym,sargs)
+          = if sdef scont (nosym,[])
+         nosym = abort "applyrule: no function symbol available"
 
+/*
 >   aprule :: (***,(*,[***])) -> [***] -> *** -> rule * ***
 >   aprule (anode,(sym,aargs)) anodes aroot
 >   =   mkrule (anode:anodes) aroot agraph
@@ -151,7 +192,17 @@ Also, using trylaw is easier
 >             =   (   updategraph aroot (sym,aargs++anodes)
 >                 .   updategraph anode (sym,aargs)
 >                 ) emptygraph
+*/
+
+aprule :: (pvar,Node sym pvar) [pvar] pvar -> Rule sym pvar
+aprule (anode,(sym,aargs)) anodes aroot
+ = mkrule [anode:anodes] aroot agraph
+   where agraph
+          = ( updategraph aroot (sym,aargs++anodes)
+            o updategraph anode (sym,aargs)
+            ) emptygraph
 
+/*
 >   apmatching :: [**] -> [***] -> pfun *** **
 >   apmatching snodes anodes
 >   =   foldr (uncurry extend) emptypfun nodepairs
diff --git a/sucl/loop.icl b/sucl/loop.icl
index c94c1b6..85d1233 100644
--- a/sucl/loop.icl
+++ b/sucl/loop.icl
@@ -28,6 +28,140 @@ like instantiation, reduction or strict annotation.
 
 ------------------------------------------------------------
 
+The function that produces a trace is given an initial task expression.
+
+The function first determines a transformation (Reduce,Annotate,Instantiate) to
+apply, using the strategy.
+
+This may fail when the termination history indicates a required abstraction
+higher up.  In that case, return at once with failure, and the current graph
+(with shared parts excluded) as the most specific generaliser.
+
+After application of the transformation, a trace is produced for the resulting
+graph(s).
+
+However, the production of the subtraces may fail initially because of a
+necessary abstraction higher-up which wasn't there (introduced recursion).
+
+Therefore, producing a trace can return one of two results: either a successful
+trace, or failure, with an indication of which abstraction was actually
+necessary.
+
+The needed generalisation is computed by taking the most specific generaliser
+for each pattern in the termination history.
+
+In the general case, generation of the subtraces fails for both the history
+pattern of the current transformation, and some patterns higher up (which were
+also passed to the trace generation function.  There are now two courses of
+action:
+
+[1] Apply abstraction instead of the current transformation.  Use the returned
+    most specific generaliser and the original graph to determine how to
+    abstract.  Then, generate subtraces.  There should be no more abstractions
+    necessary for the current node, because they should be handled in the
+    graphs resulting from the abstraction.[*]
+
+[2] Immediately return the failure, assuming (rule of thumb) that when the
+    upper generalisation was necessary, the lower one won't make it go away.
+    This is probably an optimisation of the optimisation process, but it can be
+    important, as some backtracking code (exponential!) may not have to be
+    executed.
+
+[*] This may not be entirely true in the case of sharing.  Because shared parts
+    must be pruned, the termination pattern may get smaller in the abstraction
+    operation.
+
+Questions:
+
+[?] Which would yield better results and/or perform better: [1] or [2] above?
+
+[?] Must the abstracted areas be associated with termination patterns that
+    caused their introduction?  Or somehow with the trace node where they were
+    introduced?  The termination patterns don't have to be the same over
+    different branches of the trace!  Do they play a role at all in selecting
+    the abstracted part?  Actually, they don't.  We just need their roots so we
+    can find the corresponding subgraphs and determine the MSG's.
+
+It would appear we can traverse the trace when everything is done and collected
+all the introduced functions from it.
+
+------------------------------------------------------------
+
+*/
+
+:: FallibleTrace sym var pvar
+   = GoodTrace (Trace sym var pvar)
+   | NeedAbstraction [Rgraph sym var]
+
+:: Strat sym var pvar
+   :== (History sym var)
+       (Rgraph sym var)
+    -> Answer sym var pvar
+
+maketrace
+ :: (Strat sym var pvar)        // The strategy
+    (History sym var)           // Patterns to stop partial evaluation
+    (Rgraph sym var)            // Subject graph
+ -> FallibleTrace sym var pvar  // The result
+
+maketrace strategy history subject
+ = ( case answer
+     of No                          // Root normal form, abstract and continue with arguments
+         -> handlernf
+        Yes spine                   // Do something, even if it is to fail
+         -> ( case subspine
+              of Cycle              // Cycle in spine.  Generate x:_Strict x x with _Strict :: !a b -> b.  Probably becomes a #!
+                  -> handlecycle
+                 Delta              // Primitive function.  Abstract its application and continue with remainder.
+                  -> handledelta
+                 Force n (spine)    // Shouldn't happen
+                  -> abort "loop: maketrace: spinetip returned Force???"
+                 MissingCase        // Missing case.  Generate _MissingCase, possibly parametrised with user function?
+                  -> handlemissingcase
+                 Open pattern       // Need instantiation.  Generate two branches, extend history (for both) and continue.
+                  -> handleopen pattern
+                 Partial rule match rulenode spine
+                  -> abort "loop: maketrace: spinetop returned Partial???"
+                 Unsafe histpat     // Require pattern from history.
+                  -> handleunsafe histpat // If we have a more general version with a name attached, use that.  
+                                    // Otherwise, fail with the corresponding subgraph
+                 Redex rule match   // Found a redex.  Unfold, extend history and continue.
+                  -> handleredex rule match
+                 Strict             // Need to put a strictness annotation on an open node-id.
+                  -> handlestrict   // Abstract _Strict <mumble> <mumble> and continue with rest.
+            ) spine
+            where (redexroot,subspine) = spinetip spine
+   ) strategy history subject
+   where answer = strategy history subject
+
+handlernf :: (Strat sym var pvar) (History sym var) (Rgraph sym var) -> FallibleTrace sym var pvar
+handlernf _ _ _ = undef
+
+handlecycle :: (Spine sym var pvar) (Strat sym var pvar) (History sym var) (Rgraph sym var) -> FallibleTrace sym var pvar
+handlecycle _ _ _ _ = undef
+
+handledelta :: (Spine sym var pvar) (Strat sym var pvar) (History sym var) (Rgraph sym var) -> FallibleTrace sym var pvar
+handledelta _ _ _ _ = undef
+
+handlemissingcase :: (Spine sym var pvar) (Strat sym var pvar) (History sym var) (Rgraph sym var) -> FallibleTrace sym var pvar
+handlemissingcase _ _ _ _ = undef
+
+handleopen :: (Rgraph sym pvar) (Spine sym var pvar) (Strat sym var pvar) (History sym var) (Rgraph sym var) -> FallibleTrace sym var pvar
+handleopen _ _ _ _ _ = undef
+
+handleunsafe :: (HistoryPattern sym var) (Spine sym var pvar) (Strat sym var pvar) (History sym var) (Rgraph sym var) -> FallibleTrace sym var pvar
+handleunsafe _ _ _ _ _ = undef
+
+handleredex :: (Rule sym pvar) (Pfun pvar var) (Spine sym var pvar) (Strat sym var pvar) (History sym var) (Rgraph sym var) -> FallibleTrace sym var pvar
+handleredex _ _ _ _ _ _ = undef
+
+handlestrict :: (Spine sym var pvar) (Strat sym var pvar) (History sym var) (Rgraph sym var) -> FallibleTrace sym var pvar
+handlestrict _ _ _ _ = undef
+
+/*
+
+------------------------------------------------------------
+
 Types
 -----
 
diff --git a/sucl/spine.icl b/sucl/spine.icl
index 89da146..735cd95 100644
--- a/sucl/spine.icl
+++ b/sucl/spine.icl
@@ -349,6 +349,9 @@ extendforce sgraph argno forcesub snode link extender0
          extender2 = adjust link histpat1 extender1
 
 // Extend history patterns according to an Open spine
+// FIXME: this should build TWO extended versions:
+//        one for succesful instantiation
+//        one for failed instantiation
 extendopen
  :: rgraph                      // Pattern to drive instantiation (not used)
     var                         // Node-id in subject graph that was open