aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--sucl/Makefile11
-rw-r--r--sucl/absmodule.dcl14
-rw-r--r--sucl/absmodule.icl14
-rw-r--r--sucl/basic.dcl3
-rw-r--r--sucl/basic.icl4
-rw-r--r--sucl/cli.icl33
-rw-r--r--sucl/law.dcl16
-rw-r--r--sucl/law.icl51
-rw-r--r--sucl/loop.icl134
-rw-r--r--sucl/spine.icl3
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