Skip to content
GitLab
Commit d694793d authored by Vincent Zweije's avatar Vincent Zweije
Browse files

Spine depends on history (HistoryPattern in Unsafe spine) 

Swap spine,history module dependencies
Move extendhistory from history to spine
parent db20db1e
Hide whitespace changes
Inline Side-by-side
sucl/Makefile
View file @ d694793d
......@@ -6,7 +6,7 @@ COCL = cocl
#COCLFLAGS = -lat
SYS = Clean\ System\ Files
MODULES = basic pretty pfun graph dnc rule trd rewr complete spine history trace absmodule spine strat loop law coreclean convert supercompile
MODULES = basic pretty pfun graph dnc rule trd rewr complete history spine trace absmodule spine strat loop law coreclean convert supercompile
ABC = $(patsubst %,$(SYS)/%.abc,$(MODULES))
......
sucl/history.dcl
View file @ d694793d
......@@ -2,15 +2,10 @@ definition module history
// $Id$
from spine import Spine
from graph import Graph
from general import Optional
from StdOverloaded import ==
// Transitive necessities
from spine import Subspine
// A history relates node-ids in the subject graph to patterns
:: History sym var
:== [HistoryAssociation sym var]
......@@ -23,22 +18,15 @@ from spine import Subspine
// A pattern in the history, specifying the most general subject graph (footprint) for a reduction sequence
:: HistoryPattern sym var
= Closed sym [HistoryPattern sym var] // Indicates a closed node-id in the subject graph (created by a (partial) match)
| OpenHist // Indicates an open node-id in the subject graph (created by instantiation)
| Extensible (Link var) // Indicates a link to an untouched node-id in the subject graph, where this pattern can be extended
// A link in a graph, indicated by its source node-id and the argument number
// The root of a graph can be indicated by the No constructor
:: Link var
:== Optional (var,Int)
// Extend the history according to a spine
extendhistory
:: (Graph sym var) // Subject graph
(Spine sym var pvar) // Spine leading to the reduction operation
(History sym var) // Old history
-> History sym var // New history
| == sym
& == var
& == pvar
// Check the current subject graph in the history
matchhistory
:: (History sym var) // Complete history against which to check
......
sucl/history.icl
View file @ d694793d
......@@ -32,279 +32,6 @@ import StdEnv
:== Optional (var,Int)
/*********************************************
* Extending the history according to a spine *
*********************************************/
// A function that associates specific patterns with extensible nodes
// To be used for extending history patterns
:: LinkExtender sym var
:== (Link var) // The extensible link to look for
-> HistoryPattern sym var // The associated pattern
extendhistory
:: (Graph sym var) // Subject graph
(Spine sym var pvar) // Spine leading to the reduction operation
(History sym var) // Old history
-> History sym var // New history
| == sym
& == var
& == pvar
extendhistory sgraph spine history
= [newpattern:touchmod history]
where (newpattern,_,extender)
= foldspine extendpair extenddefault extenddefault (extendforce sgraph) extenddefault extendopen (extendpartial sgraph) (const extenddefault) (extendredex sgraph) extenddefault spine No Extensible
touchmod = map (mapsnd (patextend extender))
patextend
:: (LinkExtender sym var)
(HistoryPattern sym var)
-> HistoryPattern sym var
patextend extender (Closed sym args) = Closed sym (map (patextend extender) args)
patextend extender OpenHist = OpenHist
patextend extender (Extensible link) = extender link
extendpair
:: var // Subject node-id where spine is rooted
( var
(Link var)
(LinkExtender sym var)
-> ( HistoryAssociation sym var
, HistoryPattern sym var
, LinkExtender sym var
)
)
(Link var) // Link in subject graph to this spine
(LinkExtender sym var) // Input link extender
-> ( HistoryAssociation sym var
, HistoryPattern sym var // Returned history pattern
, LinkExtender sym var // Returned link extender
)
extendpair snode extendsub link extender
= extendsub snode link extender
extenddefault
:: var
(Link var)
(LinkExtender sym var)
-> ( HistoryAssociation sym var
, HistoryPattern sym var
, LinkExtender sym var
)
extenddefault _ link extender
= (nonewpattern,Extensible link,extender)
where nonewpattern = abort "history: extenddefault: no new pattern for default spine"
// Extend history for a Force spine
// FIXME: For now, only look at function node and to-be-strict argument
// Forget what was already determined strict
extendforce
:: (Graph sym var)
Int
( (Link var)
(LinkExtender sym var)
-> ( HistoryAssociation sym var
, HistoryPattern sym var
, LinkExtender sym var
)
)
var
(Link var)
(LinkExtender sym var)
-> ( HistoryAssociation sym var
, HistoryPattern sym var
, LinkExtender sym var
)
| == var
extendforce sgraph argno forcesub snode link extender0
| not sdef
= abort "history: extendforce: force from open node-id???"
= (newpattern,histpat1,extender2)
where (newpattern,histpat0,extender1) = forcesub (Yes (snode,argno)) extender0
histpat1 = Closed ssym [argpat i \\ i <- [0..] & _ <- sargs]
argpat i
= if (i==argno) histpat0 (Extensible (Yes (snode,i)))
(sdef,(ssym,sargs)) = varcontents sgraph snode
extender2 = adjust link histpat1 extender1
// Extend history patterns according to an Open spine
extendopen
:: rgraph // Pattern to drive instantiation (not used)
var // Node-id in subject graph that was open
(Link var) // Where subject graph pointed to this open node-id
(LinkExtender sym var) // Input link extender
-> ( HistoryAssociation sym var
, HistoryPattern sym var // Pattern for this spine
, LinkExtender sym var // Resulting link extender
)
| == var
extendopen _ snode link extender0
= (newpattern,histpat,extender1)
where histpat = OpenHist
newpattern = (snode,histpat)
extender1 = adjust link histpat extender0
extendpartial
:: (Graph sym var) // Subject graph
(Rule sym pvar) // Applied rewrite rule
(Pfun pvar var) // Partial match from rewrite rule's pattern to subject graph
pvar // Node-id in rule where partial match went to subspine
( (Link var) // Link passed to subspine handler
(LinkExtender sym var) // Link extender input to subspine handler
-> ( HistoryAssociation sym var
, HistoryPattern sym var // Pattern returned for subspine
, LinkExtender sym var // Link extender returned for subspine
)
)
var // Node-id in subject with function application
(Link var) // Link to root of partial match in subject graph
(LinkExtender sym var) // Remaining link extender
-> ( HistoryAssociation sym var
, HistoryPattern sym var // History patterns with derived pattern prefixed
, LinkExtender sym var // Extended link extender
)
| == sym
& == var
& == pvar
extendpartial sgraph rule matching subnode extendsub snode link restextender
= extendfunction sgraph rule matching ((==)subnode) (const extendsub) snode link restextender
extendredex
:: (Graph sym var) // Subject graph
(Rule sym pvar) // Applied rewrite rule
(Pfun pvar var) // Partial match from rewrite rule's pattern to subject graph
var // Root of redex in subject graph
(Link var) // Link to root of redex in subject graph
(LinkExtender sym var) // Remaining link extender
-> ( HistoryAssociation sym var
, HistoryPattern sym var // History patterns with derived pattern prefixed
, LinkExtender sym var // Extended link extender
)
| == sym
& == var
& == pvar
extendredex sgraph rule matching snode link extender
= extendfunction sgraph rule matching (const False) nosub snode link extender
where nosub = abort "history: extendredex: full match with subspine??"
extendfunction
:: (Graph sym var) // Subject graph
(Rule sym pvar) // Applied rewrite rule
(Pfun pvar var) // Partial match from rewrite rule's pattern to subject graph
(pvar -> Bool) // Checks whether the subspine applies here
( (HistoryAssociation sym var)
(Link var) // Link passed to subspine handler
(LinkExtender sym var) // Link extender input to subspine handler
-> ( HistoryAssociation sym var
, HistoryPattern sym var // Pattern returned for subspine
, LinkExtender sym var // Link extender returned for subspine
)
)
var // Root of partial match in subject graph
(Link var) // Link to root of partial match in subject graph
(LinkExtender sym var) // Remaining link extender
-> ( HistoryAssociation sym var
, HistoryPattern sym var // History patterns with derived pattern prefixed
, LinkExtender sym var // Extended link extender
)
| == sym
& == var
& == pvar
extendfunction sgraph rule matching issub extendsub snode link extender0
| not sdef
= abort "history: extendfunction: partial or full match at open node-id???"
= (newpattern,thispat,extender2)
where extender2 = adjust link thispat extender1
thispat = Closed ssym argpatts
(newpattern,argpatts,extender1) = extendnodes sgraph rgraph matching snode issub extendsub thisnewpattern extender0 rargs
(sdef,(ssym,_)) = varcontents sgraph snode
rgraph = rulegraph rule
rargs = arguments rule
thisnewpattern = (snode,thispat)
extendnodes
:: (Graph sym var) // Subject graph
(Graph sym pvar) // Applied rewrite rule
(Pfun pvar var) // Partial match from rewrite rule's pattern to subject graph
var // Parent node-id in subject graph to this node-id list for creating links
(pvar -> Bool) // Tells if this is where the subspine was attached
( (HistoryAssociation sym var)
(Link var) // Link passed to subspine handler
(LinkExtender sym var) // Link extender input to subspine handler
-> ( HistoryAssociation sym var
, HistoryPattern sym var // Pattern returned for subspine
, LinkExtender sym var // Link extender returned for subspine
)
)
(HistoryAssociation sym var)
(LinkExtender sym var) // Remaining link extender
[pvar] // Node-ids in rule to handle
-> ( HistoryAssociation sym var
, [HistoryPattern sym var] // History patterns with derived pattern prefixed
, LinkExtender sym var // Extended link extender
)
| == sym
& == var
& == pvar
extendnodes sgraph rgraph matching sparent issub extendsub newpattern restextender rnodes
= foldr (extendnode sgraph rgraph matching issub extendsub) (newpattern,[],restextender) (zip2 links rnodes)
where links = [Yes (sparent,i)\\i<-[0..]]
extendnode
:: (Graph sym var) // Subject graph
(Graph sym pvar) // Applied rewrite rule
(Pfun pvar var) // Partial match from rewrite rule's pattern to subject graph
(pvar -> Bool) // Tells if this is where the subspine was attached
( (HistoryAssociation sym var)
(Link var) // Link passed to subspine handler
(LinkExtender sym var) // Link extender input to subspine handler
-> ( HistoryAssociation sym var
, HistoryPattern sym var // Pattern returned for subspine
, LinkExtender sym var // Link extender returned for subspine
)
)
( Link var // Referring link to current node-id
, pvar // Current node-id in rule
)
( HistoryAssociation sym var
, [HistoryPattern sym var] // History patterns to prefix derived patterns to
, (LinkExtender sym var) // Remaining link extender
)
-> ( HistoryAssociation sym var
, [HistoryPattern sym var] // History patterns with derived pattern prefixed
, (LinkExtender sym var) // Extended link extender
)
| == sym
& == var
& == pvar
extendnode sgraph rgraph matching issub extendsub (link,rnode) (newpattern0,rest,extender0)
| issub rnode
= (subnewpattern,[subpattern:rest],subextender)
| rdef
= foldpfun mapped unmapped matching rnode
= unmapped
where (subnewpattern,subpattern,subextender)
= extendsub newpattern0 link extender0
mapped snode
= (newpattern1,[thispat:rest],extender2)
where extender2 = adjust link thispat extender1
thispat = Closed rsym argpatts
(newpattern1,argpatts,extender1) = extendnodes sgraph rgraph matching snode issub extendsub newpattern0 extender0 rargs
unmapped
= (newpattern0,[Extensible link:rest],extender0)
(rdef,(rsym,rargs)) = varcontents rgraph rnode
/************************************************
* Verifying a subject graph against the history *
************************************************/
......@@ -334,13 +61,3 @@ checkpat sgraph OpenHist snode
= not (fst (varcontents sgraph snode))
checkpat _ (Extensible _) _
= True
/****************
* Miscellaneous *
****************/
instance == (Optional a) | == a
where (==) No No = True
(==) (Yes x1) (Yes x2) = x1==x2
(==) _ _ = False
sucl/loop.dcl
View file @ d694793d
......@@ -5,6 +5,7 @@ definition module loop
from strat import Strategy
from spine import Answer
from trace import Trace
from history import HistoryAssociation,HistoryPattern
from rule import Rgraph,Rule
from graph import Graph
from StdOverloaded import ==
......
sucl/loop.icl
View file @ d694793d
......@@ -132,7 +132,8 @@ transform
[var] // Arguments of function to generate
!(Answer sym var pvar) // Result of strategy
-> Action sym var pvar
| == var
| == sym
& == var
& == pvar
transform anode sargs (Yes spine)
......@@ -209,7 +210,8 @@ tryunfold
(Pfun pvar var) // The matching from rule's pattern to subject
(Spine sym var pvar) // The spine returned by the strategy
-> Action sym var pvar
| == var
| == sym
& == var
& == pvar
tryunfold redexroot rule matching spine
......@@ -220,8 +222,7 @@ tryunfold redexroot rule matching spine
= xunfold redexroot rule (heap,sroot,subject,matching)
noredir = abort "transtree: no mapping foor root of replacement"
reductroot = total noredir matching` (ruleroot rule)
redirect = adjust redexroot reductroot id
history` = extendhistory subject redirect spine history
history` = extendhistory subject spine history
trace = continue history` failinfo instdone stricts sroot` subject` heap`
tryannotate
......
sucl/spine.dcl
View file @ d694793d
......@@ -2,9 +2,12 @@ definition module spine
// $Id$
from history import History,HistoryAssociation,HistoryPattern
from rule import Rgraph,Rule
from graph import Graph
from pfun import Pfun
from general import Optional
from StdOverloaded import ==
/*
......@@ -163,7 +166,7 @@ in a graph.
| MissingCase // All alternatives failed for a function symbol
| Open (Rgraph sym pvar) // Need root normal form of open node for matching
| Partial (Rule sym pvar) (Pfun pvar var) pvar (Spine sym var pvar) // A rule was strictly partially matched
| Unsafe (Rgraph sym var) // Terminated due to immininent recursion
| Unsafe (HistoryPattern sym var) // Terminated due to immininent recursion
| Redex (Rule sym pvar) (Pfun pvar var) // Total match
| Strict // Need root normal form due to strictness
......@@ -176,7 +179,7 @@ foldspine
.subresult // Fold a MissingCase subspine
((Rgraph sym pvar) -> .subresult) // Fold an Open subspine
((Rule sym pvar) (Pfun pvar var) pvar .result -> .subresult) // Fold a Partial subspine
((Rgraph sym var) -> .subresult) // Fold an Unsafe subspine
((HistoryPattern sym var) -> .subresult) // Fold an Unsafe subspine
((Rule sym pvar) (Pfun pvar var) -> .subresult) // Fold a Redex subspine
.subresult // Fold a Strict subspine
.(Spine sym var pvar) // The spine to fold
......@@ -193,3 +196,13 @@ spinenodes :: .(Spine sym var pvar) -> [var]
// Make a decision (continuation based) on whether a spine ends in Open
ifopen :: result result !.(Answer sym var pvar) -> result
// Extend the history according to a spine
extendhistory
:: (Graph sym var) // Subject graph
(Spine sym var pvar) // Spine leading to the reduction operation
(History sym var) // Old history
-> History sym var // New history
| == sym
& == var
& == pvar
sucl/spine.icl
View file @ d694793d
......@@ -2,9 +2,12 @@ implementation module spine
// $Id$
import history
import rule
import graph
import pfun
import basic
from general import No,Yes
import StdEnv
/*
......@@ -164,7 +167,7 @@ in a graph.
| MissingCase // All alternatives failed for a function symbol
| Open (Rgraph sym pvar) // Need root normal form of open node for matching
| Partial (Rule sym pvar) (Pfun pvar var) pvar (Spine sym var pvar) // A rule was strictly partially matched
| Unsafe (Rgraph sym var) // Terminated due to immininent recursion
| Unsafe (HistoryPattern sym var) // Terminated due to immininent recursion
| Redex (Rule sym pvar) (Pfun pvar var) // Total match
| Strict // Need root normal form due to strictness
......@@ -200,18 +203,18 @@ in a graph.
*/
foldspine
:: !(var .subresult -> .result)
.subresult
.subresult
(Int .result -> .subresult)
.subresult
((Rgraph sym pvar) -> .subresult)
((Rule sym pvar) (Pfun pvar var) pvar .result -> .subresult)
((Rgraph sym var) -> .subresult)
((Rule sym pvar) (Pfun pvar var) -> .subresult)
.subresult
.(Spine sym var pvar)
-> .result
:: !(var .subresult -> .result) // Fold the spine itself
.subresult // Fold a Cycle subspine
.subresult // Fold a Delta subspine
(Int .result -> .subresult) // Fold a Force subspine
.subresult // Fold a MissingCase subspine
((Rgraph sym pvar) -> .subresult) // Fold an Open subspine
((Rule sym pvar) (Pfun pvar var) pvar .result -> .subresult) // Fold a Partial subspine
((HistoryPattern sym var) -> .subresult) // Fold an Unsafe subspine
((Rule sym pvar) (Pfun pvar var) -> .subresult) // Fold a Redex subspine
.subresult // Fold a Strict subspine
.(Spine sym var pvar) // The spine to fold
-> .result // The final result
foldspine pair cycle delta force missingcase open partial unsafe redex strict spine
= fold spine
......@@ -224,7 +227,7 @@ foldspine pair cycle delta force missingcase open partial unsafe redex strict sp
foldsub MissingCase = missingcase
foldsub (Open rgraph) = open rgraph
foldsub (Partial rule matching rnode spine) = partial rule matching rnode (fold spine)
foldsub (Unsafe rgraph) = unsafe rgraph
foldsub (Unsafe histpat) = unsafe histpat
foldsub (Redex rule matching) = redex rule matching
foldsub Strict = strict
......@@ -244,3 +247,286 @@ ifopen open other spine
= foldoptional other (checkopen o spinetip) spine
where checkopen (onode,Open pattern) = open
checkopen tip = other
/*********************************************
* Extending the history according to a spine *
*********************************************/
// A function that associates specific patterns with extensible nodes
// To be used for extending history patterns
:: LinkExtender sym var
:== (Link var) // The extensible link to look for
-> HistoryPattern sym var // The associated pattern
extendhistory
:: (Graph sym var) // Subject graph
(Spine sym var pvar) // Spine leading to the reduction operation
(History sym var) // Old history
-> History sym var // New history
| == sym
& == var
& == pvar
extendhistory sgraph spine history
= [newpattern:touchmod history]
where (newpattern,_,extender)
= foldspine extendpair extenddefault extenddefault (extendforce sgraph) extenddefault extendopen (extendpartial sgraph) (const extenddefault) (extendredex sgraph) extenddefault spine No Extensible
touchmod = map (mapsnd (patextend extender))
patextend
:: (LinkExtender sym var)
(HistoryPattern sym var)
-> HistoryPattern sym var
patextend extender (Closed sym args) = Closed sym (map (patextend extender) args)
patextend extender OpenHist = OpenHist
patextend extender (Extensible link) = extender link
extendpair
:: var // Subject node-id where spine is rooted
( var
(Link var)
(LinkExtender sym var)
-> ( HistoryAssociation sym var
, HistoryPattern sym var
, LinkExtender sym var
)
)
(Link var) // Link in subject graph to this spine
(LinkExtender sym var) // Input link extender
-> ( HistoryAssociation sym var
, HistoryPattern sym var // Returned history pattern
, LinkExtender sym var // Returned link extender
)
extendpair snode extendsub link extender
= extendsub snode link extender
extenddefault
:: var
(Link var)
(LinkExtender sym var)
-> ( HistoryAssociation sym var
, HistoryPattern sym var
, LinkExtender sym var
)
extenddefault _ link extender
= (nonewpattern,Extensible link,extender)
where nonewpattern = abort "history: extenddefault: no new pattern for default spine"
// Extend history for a Force spine
// FIXME: For now, only look at function node and to-be-strict argument
// Forget what was already determined strict
extendforce
:: (Graph sym var)
Int
( (Link var)
(LinkExtender sym var)
-> ( HistoryAssociation sym var
, HistoryPattern sym var
, LinkExtender sym var
)
)
var
(Link var)
(LinkExtender sym var)
-> ( HistoryAssociation sym var
, HistoryPattern sym var
, LinkExtender sym var
)
| == var
extendforce sgraph argno forcesub snode link extender0
| not sdef
= abort "history: extendforce: force from open node-id???"
= (newpattern,histpat1,extender2)
where (newpattern,histpat0,extender1) = forcesub (Yes (snode,argno)) extender0
histpat1 = Closed ssym [argpat i \\ i <- [0..] & _ <- sargs]
argpat i
= if (i==argno) histpat0 (Extensible (Yes (snode,i)))
(sdef,(ssym,sargs)) = varcontents sgraph snode
extender2 = adjust link histpat1 extender1