Commit 3c139e9c authored by Vincent Zweije's avatar Vincent Zweije
Browse files

Start of translating remainder,

global termination bug and all,
from Miranda to Clean
parent 81b22c45
...@@ -6,7 +6,7 @@ COCL = cocl ...@@ -6,7 +6,7 @@ COCL = cocl
#COCLFLAGS = -lat #COCLFLAGS = -lat
SYS = Clean\ System\ Files 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)) ABC = $(patsubst %,$(SYS)/%.abc,$(MODULES))
...@@ -25,10 +25,11 @@ tags: *.dcl *.icl ../compiler/*.dcl ../compiler/*.icl ...@@ -25,10 +25,11 @@ tags: *.dcl *.icl ../compiler/*.dcl ../compiler/*.icl
$(SYS)/%.abc: %.icl $(SYS)/%.abc: %.icl
$(COCL) $(COCLFLAGS) $* $(COCL) $(COCLFLAGS) $*
$(SYS)/supercompile.abc: supercompile.icl supercompile.dcl $(SYS)/supercompile.abc: supercompile.icl supercompile.dcl convert.dcl
$(SYS)/convert.abc: convert.icl convert.dcl coreclean.dcl rule.dcl $(SYS)/convert.abc: convert.icl convert.dcl coreclean.dcl rule.dcl graph.dcl basic.dcl
$(SYS)/coreclean.abc: coreclean.icl coreclean.dcl $(SYS)/cli.abc: cli.icl cli.dcl absmodule.dcl coreclean.dcl law.dcl strat.dcl rule.dcl basic.dcl
$(SYS)/law.abc: law.icl law.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)/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)/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 $(SYS)/history.abc: history.icl history.dcl spine.dcl rule.dcl graph.dcl basic.dcl
......
...@@ -5,11 +5,11 @@ definition module absmodule ...@@ -5,11 +5,11 @@ definition module absmodule
from rule import Rule from rule import Rule
:: Module sym pvar tsym tvar :: Module sym pvar tsym tvar
= { exportedtypesymbols :: [tsym] // Exported type symbols (from DCL) = { exportedtypesymbols :: [tsym] // Exported type symbols (from DCL)
, typealias :: [(tsym,Rule tsym tvar)] // Alias types , typealias :: [(tsym,Rule tsym tvar)] // Alias types
, typeconstructors :: [(tsym,[sym])] // All constructor symbols of each declared algebraic type , typeconstructors :: [(tsym,[sym])] // All constructor symbols of each declared algebraic type
, exportedsymbols :: [sym] // Exported function/constructor symbols , exportedsymbols :: [sym] // Exported function/constructor symbols
, aliases :: [(sym,Rule sym pvar)] // Macros , aliases :: [(sym,Rule sym pvar)] // Macros
, typerules :: [(sym,Rule tsym tvar,[Bool])] // Info from type rules (actual type and argument strictnesses) , 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 , rules :: [(sym,[Rule sym pvar])] // Rewrite rules of each symbol, absent if imported
} }
...@@ -42,13 +42,13 @@ Module implementation. ...@@ -42,13 +42,13 @@ Module implementation.
*/ */
:: Module sym pvar tsym tvar :: Module sym pvar tsym tvar
= { exportedtypesymbols :: [tsym] // Exported type symbols (from DCL) = { exportedtypesymbols :: [tsym] // Exported type symbols (from DCL)
, typealias :: [(tsym,Rule tsym tvar)] // Alias types , typealias :: [(tsym,Rule tsym tvar)] // Alias types
, typeconstructors :: [(tsym,[sym])] // All constructor symbols of each declared algebraic type , typeconstructors :: [(tsym,[sym])] // All constructor symbols of each declared algebraic type
, exportedsymbols :: [sym] // Exported function/constructor symbols , exportedsymbols :: [sym] // Exported function/constructor symbols
, aliases :: [(sym,Rule sym pvar)] // Macros , aliases :: [(sym,Rule sym pvar)] // Macros
, typerules :: [(sym,Rule tsym tvar,[Bool])] // Info from type rules (actual type and argument strictnesses) , 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 , rules :: [(sym,[Rule sym pvar])] // Rewrite rules of each symbol, absent if imported
} }
/* /*
......
...@@ -53,6 +53,9 @@ disjoint :: .[elem] !.[elem] -> Bool | == elem ...@@ -53,6 +53,9 @@ disjoint :: .[elem] !.[elem] -> Bool | == elem
// `Eqlen xs ys' determines whether `xs' and `ys' are equally long. // `Eqlen xs ys' determines whether `xs' and `ys' are equally long.
eqlen :: ![.elem1] ![.elem2] -> .Bool 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' is a combination of foldl and map.
foldlm :: ((.collect,.elem) -> (.collect,.elem`)) !(.collect,![.elem]) -> (.collect,[.elem`]) foldlm :: ((.collect,.elem) -> (.collect,.elem`)) !(.collect,![.elem]) -> (.collect,[.elem`])
......
...@@ -71,6 +71,10 @@ eqlen [x:xs] [y:ys] = eqlen xs ys ...@@ -71,6 +71,10 @@ eqlen [x:xs] [y:ys] = eqlen xs ys
eqlen [] [] = True eqlen [] [] = True
eqlen xs ys = False 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' is a combination of foldl and map.
foldlm :: ((.collect,.elem) -> (.collect,.elem`)) !(.collect,![.elem]) -> (.collect,[.elem`]) foldlm :: ((.collect,.elem) -> (.collect,.elem`)) !(.collect,![.elem]) -> (.collect,[.elem`])
foldlm f (l,[]) = (l,[]) foldlm f (l,[]) = (l,[])
......
definition module canon
definition module cli
...@@ -2,6 +2,14 @@ implementation module cli ...@@ -2,6 +2,14 @@ implementation module cli
// $Id$ // $Id$
import absmodule
import coreclean
import law
import strat
import rule
import basic
import StdEnv
/* /*
cli.lit - Clean implementation modules cli.lit - Clean implementation modules
...@@ -94,7 +102,11 @@ Abstype implementation. ...@@ -94,7 +102,11 @@ Abstype implementation.
> aliases :: cli -> [(typesymbol,rule typesymbol typenode)] > aliases :: cli -> [(typesymbol,rule typesymbol typenode)]
> macros :: cli -> [(symbol,rule symbol node)] > macros :: cli -> [(symbol,rule symbol node)]
> stripexports :: [char] -> cli -> cli > stripexports :: [char] -> cli -> cli
*/
:: Cli :== Module SuclSymbol SuclVariable SuclTypeSymbol SuclTypeVariable
/*
> cli == module symbol node typesymbol typenode > cli == module symbol node typesymbol typenode
> readcli = compilecli.readcleanparts > readcli = compilecli.readcleanparts
...@@ -126,13 +138,26 @@ Abstype implementation. ...@@ -126,13 +138,26 @@ Abstype implementation.
> ) (corestrategy matchable) || Checks rules for symbols in the language core (IF, _AP, ...) > ) (corestrategy matchable) || Checks rules for symbols in the language core (IF, _AP, ...)
> where islocal (User m i) = member (map fst rs) (User m i) > where islocal (User m i) = member (map fst rs) (User m i)
> islocal rsym = True || Symbols in the language core are always completely known > 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]) typearity :: (Rule SuclTypeSymbol SuclTypeVariable,[Bool]) -> Int
> maxtypeinfo ts = extendfn ts coretypeinfo typearity ti = length (arguments (fst ti))
> extendfn :: [(*,**)] -> (*->**) -> * -> ** maxtypeinfo :: [(SuclSymbol,(Rule SuclTypeSymbol SuclTypeVariable,[Bool]))] SuclSymbol -> (Rule SuclTypeSymbol SuclTypeVariable,[Bool])
> extendfn mapping f x = foldmap id (f x) mapping x maxtypeinfo defs sym = extendfn defs coretypeinfo sym
/*
> constrs ((tes,tas,tcs),defs) = tcs > constrs ((tes,tas,tcs),defs) = tcs
> complete ((tes,tas,tcs),(es,as,ts,rs)) = mkclicomplete tcs (fst.maxtypeinfo ts) > complete ((tes,tas,tcs),(es,as,ts,rs)) = mkclicomplete tcs (fst.maxtypeinfo ts)
......
...@@ -107,7 +107,7 @@ convert_atype atype (heap,(graph,rest,srest)) ...@@ -107,7 +107,7 @@ convert_atype atype (heap,(graph,rest,srest))
where (heap``,(graph``,fnargs,[_:_])) = convert_atype functype (heap`,(graph`,suclargtype,[])) // _ => forget annotations of subtypes where (heap``,(graph``,fnargs,[_:_])) = convert_atype functype (heap`,(graph`,suclargtype,[])) // _ => forget annotations of subtypes
(heap```,(graph`,suclargtype,[_:_])) = convert_atype argtype (heap``,(graph,[],[])) // _ => forget annotations of subtypes (heap```,(graph`,suclargtype,[_:_])) = convert_atype argtype (heap``,(graph,[],[])) // _ => forget annotations of subtypes
[suclrestype:heap`] = heap [suclrestype:heap`] = heap
graph``` = updategraph suclrestype (SuclFN,fnargs) graph`` graph``` = updategraph suclrestype (SuclFN 1,fnargs) graph``
// A basic type, which is translated to an application of a basic type symbol to the empty list of arguments // A basic type, which is translated to an application of a basic type symbol to the empty list of arguments
TB basictype TB basictype
......
...@@ -2,9 +2,14 @@ definition module coreclean ...@@ -2,9 +2,14 @@ definition module coreclean
// $Id$ // $Id$
from strat import Strategy
from rule import Rule
from syntax import TypeSymbIdent,Ident,TypeVar,ExprInfoPtr,VarInfoPtr from syntax import TypeSymbIdent,Ident,TypeVar,ExprInfoPtr,VarInfoPtr
// Transitive necessities // Transitive necessities
from strat import Substrategy
from spine import Spine,Subspine
from graph import Graph,Node
from syntax import SymbolPtr,SymbolTableEntry,STE_Kind,Index,Level,Global,TypeSymbProperties,SignClassification,PropClassification,TypeVarInfoPtr,TypeVarInfo,ExprInfo,VarInfo from syntax import SymbolPtr,SymbolTableEntry,STE_Kind,Index,Level,Global,TypeSymbProperties,SignClassification,PropClassification,TypeVarInfoPtr,TypeVarInfo,ExprInfo,VarInfo
from general import BITVECT from general import BITVECT
from Heap import Ptr,PtrN,HeapN from Heap import Ptr,PtrN,HeapN
...@@ -12,10 +17,10 @@ from StdOverloaded import == ...@@ -12,10 +17,10 @@ from StdOverloaded import ==
from StdString import String from StdString import String
:: SuclTypeSymbol :: SuclTypeSymbol
= SuclUSER TypeSymbIdent = SuclUSER TypeSymbIdent // A user-defined type symbol
| SuclFN | SuclFN Int // THE function type for a function with specified arity
| SuclINT | SuclINT // Built-in integer
| SuclCHAR | SuclCHAR // Etc.
| SuclREAL | SuclREAL
| SuclBOOL | SuclBOOL
| SuclDYNAMIC | SuclDYNAMIC
...@@ -45,4 +50,10 @@ sucltypeheap :: [SuclTypeVariable] ...@@ -45,4 +50,10 @@ sucltypeheap :: [SuclTypeVariable]
= SuclAnonymous Int = SuclAnonymous Int
| SuclNamed VarInfoPtr | SuclNamed VarInfoPtr
suclheap :: [SuclVariable]
instance == SuclSymbol
instance == SuclVariable instance == SuclVariable
// Get the type rule and strictness of a built in core clean symbol
coretypeinfo :: SuclSymbol -> (Rule SuclTypeSymbol SuclTypeVariable,[Bool])
...@@ -2,11 +2,15 @@ implementation module coreclean ...@@ -2,11 +2,15 @@ implementation module coreclean
// $Id$ // $Id$
import strat
import spine
import rule
import graph
import syntax import syntax
:: SuclTypeSymbol :: SuclTypeSymbol
= SuclUSER TypeSymbIdent = SuclUSER TypeSymbIdent
| SuclFN | SuclFN Int
| SuclINT | SuclINT
| SuclCHAR | SuclCHAR
| SuclREAL | SuclREAL
...@@ -39,7 +43,39 @@ sucltypeheap =: map SuclANONYMOUS [0..] ...@@ -39,7 +43,39 @@ sucltypeheap =: map SuclANONYMOUS [0..]
= SuclAnonymous Int = SuclAnonymous Int
| SuclNamed VarInfoPtr | SuclNamed VarInfoPtr
suclheap :: [SuclVariable]
suclheap =: map SuclAnonymous [0..]
instance == SuclSymbol
where (==) (SuclUser sptr1) (SuclUser sptr2) = sptr1 == sptr2
(==) (SuclCase eptr1) (SuclCase eptr2) = eptr1 == eptr2
(==) (SuclApply int1 ) (SuclApply int2 ) = int1 == int2
(==) (SuclInt int1 ) (SuclInt int2 ) = int1 == int2
(==) (SuclReal real1) (SuclReal real2) = real1 == real2
(==) (SuclBool bool1) (SuclBool bool2) = bool1 == bool2
(==) _ _ = False
instance == SuclVariable instance == SuclVariable
where (==) (SuclAnonymous i1) (SuclAnonymous i2) = i1 == i2 where (==) (SuclAnonymous i1) (SuclAnonymous i2) = i1 == i2
(==) (SuclNamed p1) (SuclNamed p2) = p1 == p2 (==) (SuclNamed p1) (SuclNamed p2) = p1 == p2
(==) _ _ = False (==) _ _ = False
// Get the type rule and strictness of a built in core clean symbol
coretypeinfo :: SuclSymbol -> (Rule SuclTypeSymbol SuclTypeVariable,[Bool])
coretypeinfo sym
= (trule,corestricts sym)
where corestricts (SuclApply argc) = [True,False]
corestricts sym = map (const False) (arguments trule)
trule = coretyperule sym
coretyperule :: SuclSymbol -> Rule SuclTypeSymbol SuclTypeVariable
coretyperule (SuclApply argc)
= mkrule [infunctype,argtype] outfunctype` (updategraph infunctype (SuclFN argc,[argtype:argtypes]++[restype]) outfuncgraph)
where [infunctype,outfunctype,argtype,restype:sucltypeheap`] = sucltypeheap
argtypes = take argc sucltypeheap`
(outfunctype`,outfuncgraph)
= if (argc==0)
(restype,emptygraph)
(outfunctype,updategraph outfunctype (SuclFN (argc-1),argtypes++[restype]) emptygraph)
coretyperule _
= undef
definition module extract
definition module law definition module law
// $Id$ // $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
...@@ -2,6 +2,15 @@ implementation module law ...@@ -2,6 +2,15 @@ implementation module law
// $Id$ // $Id$
import coreclean
import strat
import spine
import rule
import graph
import dnc
import basic
import StdEnv
/* /*
> %export > %export
...@@ -101,7 +110,12 @@ implementation module law ...@@ -101,7 +110,12 @@ implementation module law
------------------------------------------------------------------------ ------------------------------------------------------------------------
> cleanlaws :: [(symbol,law symbol ** node ****)] > cleanlaws :: [(symbol,law symbol ** node ****)]
*/
cleanlaws :: [(SuclSymbol,Law SuclSymbol var SuclVariable result)]
cleanlaws =: []
/*
> cleanlaws > cleanlaws
> = [(User "deltaI" "*",law) | law <- mullaws] ++ > = [(User "deltaI" "*",law) | law <- mullaws] ++
> [(User "deltaI" "+",law) | law <- addlaws] ++ > [(User "deltaI" "+",law) | law <- addlaws] ++
...@@ -134,7 +148,24 @@ Also, using trylaw is easier ...@@ -134,7 +148,24 @@ Also, using trylaw is easier
> corestrategy matchable substrat subject found rnf (ssym,snodes) > corestrategy matchable substrat subject found rnf (ssym,snodes)
> = rnf > = 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 :: (bool,(*,[**])) -> rule * node
> applyrule (sdef,scont) > applyrule (sdef,scont)
> = aprule (anode,(sym,aargs)) [enode] aroot > = aprule (anode,(sym,aargs)) [enode] aroot
...@@ -143,7 +174,17 @@ Also, using trylaw is easier ...@@ -143,7 +174,17 @@ Also, using trylaw is easier
> = scont, if sdef > = scont, if sdef
> = (nosym,[]), otherwise > = (nosym,[]), otherwise
> nosym = error "applyrule: no function symbol available" > 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 :: (***,(*,[***])) -> [***] -> *** -> rule * ***
> aprule (anode,(sym,aargs)) anodes aroot > aprule (anode,(sym,aargs)) anodes aroot
> = mkrule (anode:anodes) aroot agraph > = mkrule (anode:anodes) aroot agraph
...@@ -151,7 +192,17 @@ Also, using trylaw is easier ...@@ -151,7 +192,17 @@ Also, using trylaw is easier
> = ( updategraph aroot (sym,aargs++anodes) > = ( updategraph aroot (sym,aargs++anodes)
> . updategraph anode (sym,aargs) > . updategraph anode (sym,aargs)
> ) emptygraph > ) 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 :: [**] -> [***] -> pfun *** **
> apmatching snodes anodes > apmatching snodes anodes
> = foldr (uncurry extend) emptypfun nodepairs > = foldr (uncurry extend) emptypfun nodepairs
......
...@@ -28,6 +28,140 @@ like instantiation, reduction or strict annotation. ...@@ -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