Skip to content

GitLab

Commit 331a9155 authored by Vincent Zweije's avatar Vincent Zweije
Browse files

Revert to old history pattern structure

parent 6648ed22
Hide whitespace changes
Inline Side-by-side
sucl/extract.dcl
View file @ 331a9155
......@@ -14,7 +14,8 @@ actualfold ::
[(pvar,Graph sym pvar)]
(Rule sym var)
-> Optional (Rule sym var,[Rgraph sym var])
| == var
| == sym
& == var
& == pvar
splitrule ::
......
sucl/extract.icl
View file @ 331a9155
......@@ -70,7 +70,8 @@ actualfold ::
[(pvar,Graph sym pvar)]
(Rule sym var)
-> Optional (Rule sym var,[Rgraph sym var])
| == var
| == sym
& == var
& == pvar
actualfold deltanodes rnfnodes foldarea self foldcont hist rule
......@@ -100,7 +101,8 @@ findoccs ::
(Rule sym var)
var
-> [[(pvar,var)]]
| == var
| == sym
& == var
& == pvar
findoccs hist rule rnode
......@@ -120,8 +122,6 @@ findoccs hist rule rnode
where inner = map (lookup mapping) (fst (graphvars hgraph [hroot]))
outer = removeMembers (varlist (prunegraph rnode rgraph) [rroot:rargs]) [rnode]
instantiate = undef
/*
------------------------------------------------------------------------
......
sucl/graph.dcl
View file @ 331a9155
......@@ -218,3 +218,12 @@ compilegraph :: ![(var,Node sym var)] -> Graph sym var
extgraph :: (Graph sym var) (Graph sym pvar) [pvar] (Pfun pvar var) (Graph sym var) -> Graph sym var | == var & == pvar
instance == (Graph sym var) | == sym & == var
instantiate ::
(Graph sym pvar,Graph sym var)
(pvar,var)
([(pvar,var)],[(pvar,var)],[(pvar,var)])
-> ([(pvar,var)],[(pvar,var)],[(pvar,var)])
| == sym
& == var
& == pvar
sucl/graph.icl
View file @ 331a9155
......@@ -229,31 +229,50 @@ Uses in Miranda:
* extract.lit.m: used to find instances of patterns in the termination history, while folding trace tips.
* transform.lit.m: Uses a different `instantiate' from rewr.lit.m.
> instantiate :: (graph * ***,graph * **) -> (***,**) -> ([(***,**)],[(***,**)],[(***,**)]) -> ([(***,**)],[(***,**)],[(***,**)])
> instantiate (pgraph,sgraph) (pnode,snode) (seen,mapping,errs)
> = (seen,mapping,errs), if member seen psnode
> = (psnode:seen,mapping,psnode:errs), if member (map fst seen) pnode
> = (psnode:seen,psnode:mapping,errs), if ~pdef
> = (psnode:seen,mapping,psnode:errs), if ~sdef
> = (psnode:seen,mapping,psnode:errs), if ~(psym=ssym&eqlen pargs sargs)
> = (seen',psnode:mapping',errs'), otherwise
> where (pdef,(psym,pargs)) = nodecontents pgraph pnode
> (sdef,(ssym,sargs)) = nodecontents sgraph snode
> (seen',mapping',errs') = instantiateargs (pgraph,sgraph) (zip2 pargs sargs) (psnode:seen,mapping,errs)
> psnode = (pnode,snode)
`Instantiateargs' is the logical extension of `instantiate' to lists of node pairs.
> instantiateargs :: (graph * ***,graph * **) -> [(***,**)] -> ([(***,**)],[(***,**)],[(***,**)]) -> ([(***,**)],[(***,**)],[(***,**)])
*/
> instantiateargs psgraph [] = id
> instantiateargs psgraph (psnode:psnodes) (seen,mapping,errs)
> = (seen'',mapping'',errs'')
> where (seen',mapping'',errs'') = instantiate psgraph psnode (seen,mapping',errs')
> (seen'',mapping',errs') = instantiateargs psgraph psnodes (seen',mapping,errs)
instantiate ::
(Graph sym pvar,Graph sym var)
(pvar,var)
([(pvar,var)],[(pvar,var)],[(pvar,var)])
-> ([(pvar,var)],[(pvar,var)],[(pvar,var)])
| == sym
& == var
& == pvar
*/
instantiate (pgraph,sgraph) (pnode,snode) (seen,mapping,errs)
| isMember psnode seen
= (seen,mapping,errs)
| isMember pnode (map fst seen)
= ([psnode:seen],mapping,[psnode:errs])
| not pdef
= ([psnode:seen],[psnode:mapping],errs)
| not sdef
= ([psnode:seen],mapping,[psnode:errs])
| not (psym==ssym && eqlen pargs sargs)
= ([psnode:seen],mapping,[psnode:errs])
= (seen`,[psnode:mapping`],errs`)
where (pdef,(psym,pargs)) = varcontents pgraph pnode
(sdef,(ssym,sargs)) = varcontents sgraph snode
(seen`,mapping`,errs`) = instantiateargs (pgraph,sgraph) (zip2 pargs sargs) ([psnode:seen],mapping,errs)
psnode = (pnode,snode)
instantiateargs ::
(Graph sym pvar,Graph sym var)
[(pvar,var)]
([(pvar,var)],[(pvar,var)],[(pvar,var)])
-> ([(pvar,var)],[(pvar,var)],[(pvar,var)])
| == sym
& == var
& == pvar
instantiateargs psgraph [] sme = sme
instantiateargs psgraph [psnode:psnodes] (seen,mapping,errs)
= (seen``,mapping``,errs``)
where (seen`,mapping``,errs``) = instantiate psgraph psnode (seen,mapping`,errs`)
(seen``,mapping`,errs`) = instantiateargs psgraph psnodes (seen`,mapping,errs)
:: Matchstate var pvar
:== ( [(pvar,var)] // Pattern-subject var combo's already visited
......
sucl/history.dcl
View file @ 331a9155
......@@ -2,6 +2,7 @@ definition module history
// $Id$
from rule import Rgraph
from graph import Graph
from general import Optional
from StdOverloaded import ==
......@@ -12,15 +13,13 @@ from StdOverloaded import ==
// An association between a node-id in the subject graph and a history pattern
:: HistoryAssociation sym var
:== ( var // Attachment point in the subject graph where the history pattern is "housed"
, HistoryPattern sym var // The pattern in the history
:== ( var // Attachment point in the subject graph where the history pattern is "housed"
, [HistoryPattern sym var] // The pattern in the history
)
// 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
:== Rgraph sym var
// 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
......
sucl/history.icl
View file @ 331a9155
......@@ -15,15 +15,13 @@ import StdEnv
// An association between a node-id in the subject graph and a history pattern
:: HistoryAssociation sym var
:== ( var // Attachment point in the subject graph where the history pattern is "housed"
, HistoryPattern sym var // The pattern in the history
:== ( var // Attachment point in the subject graph where the history pattern is "housed"
, [HistoryPattern sym var] // The pattern in the history
)
// 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
:== Rgraph sym var
// 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
......@@ -47,16 +45,17 @@ matchhistory
matchhistory hist spinenodes sgraph snode
= foldr (checkassoc spinenodes sgraph snode) [] hist
checkassoc spinenodes sgraph snode (var,pat) rest
| isMember var spinenodes && checkpat sgraph pat snode
= [pat:rest]
= rest
checkpat :: (Graph sym var) (HistoryPattern sym var) var -> Bool | == sym & == var
checkpat sgraph (Closed psym pargs) snode
# (sdef,(ssym,sargs)) = varcontents sgraph snode
= sdef && psym==ssym && eqlen pargs sargs && and [checkpat sgraph parg sarg \\ parg<-pargs & sarg<-sargs]
checkpat sgraph OpenHist snode
= not (fst (varcontents sgraph snode))
checkpat _ (Extensible _) _
= True
checkassoc spinenodes sgraph snode (var,pats) rest
= if (isMember var spinenodes) (foldr checkpat rest pats) rest
where checkpat pat rest
= if (isinstance (hgraph,hroot) (sgraph,snode)) [pat:rest] rest
where hgraph = rgraphgraph pat; hroot = rgraphroot pat
/*
instantiate ::
(HistoryPattern sym pvar)
(Graph sym var)
var
([(pvar,var)],[(pvar,var)],[(pvar,var)])
-> ([(pvar,var)],[(pvar,var)],[(pvar,var)])
*/
sucl/loop.icl
View file @ 331a9155
......@@ -304,7 +304,7 @@ tryinstantiate onode rpattern anode sargs
where success = continue history failinfo True stricts` sroot subject` heap`
fail = continue history failinfo` True stricts` sroot subject heap
failinfo` = adjust onode [rpattern:failinfo onode] failinfo
(heap`,subject`) = instantiate pgraph proot onode (heap,subject)
(heap`,subject`) = rewrinstantiate pgraph proot onode (heap,subject)
proot = rgraphroot rpattern; pgraph = rgraphgraph rpattern
stricts` = if instdone stricts (map2 ((||) o (==) onode) sargs stricts)
......@@ -359,7 +359,8 @@ 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)
history` = extendhistory subject spine history
history` = extendhistory subject redirect spine history
redirect = adjust redexroot reductroot id
trace = continue history` failinfo instdone stricts sroot` subject` heap`
tryannotate
......
sucl/newfold.icl
View file @ 331a9155
......@@ -140,8 +140,6 @@ recurse foldarea fnsymbol
where rroot = ruleroot rule; rgraph = rulegraph rule
newhist` = [(rroot,rgraph):newhist]
foldtips = undef
/*
`Foldtips foldarea foldcont hist trace' folds all occurrences of (rooted
......@@ -150,8 +148,6 @@ which are the results of folding, and a list of areas for which
functions must be introduced. If no occurrences were found, Absent is
returned.
> addstrict stricts (rule,areas) = (stricts,[rule],areas)
> foldtips ::
> (rgraph * **->(*,[**])) ->
> (*,[**]) ->
......@@ -184,6 +180,8 @@ returned.
> || exres = (False,mapfst3 only (extract noetrc foldarea trace ([],[],[])))
> exres = (False,newextract noetrc foldarea trace)
> addstrict stricts (rule,areas) = (stricts,[rule],areas)
> noetrc trace area = id
> pair x y = (x,y)
......@@ -191,7 +189,53 @@ returned.
> only :: [*] -> *
> only [x] = x
> only xs = error "only: not a singleton list"
*/
foldtips ::
((Rgraph sym var)->(sym,[var]))
(sym,[var])
-> ([(var,Graph sym var)],[(var,Graph sym var)])
(Trace sym var pvar)
-> (Bool,([Bool],[Rule sym var],[Rgraph sym var]))
| == sym
& == var
& == pvar
foldtips foldarea foldcont
= ft
where ft hist trace
= ft` transf
where (Trace stricts rule answer history transf) = trace
ft` Stop
= foldoptional exres (pair True o addstrict stricts) (actualfold deltanodes rnfnodes foldarea (==) foldcont (snd hist) rule)
where deltanodes = foldoptional [] getdeltanodes answer
rnfnodes = foldoptional [ruleroot rule] (const []) answer
ft` (Instantiate yestrace notrace)
= ft`` (ft hist yestrace) (ft hist notrace)
where ft`` (False,yessra) (False,nosra) = exres
ft`` (yesfound,(yesstricts,yesrules,yesareas)) (nofound,(nostricts,norules,noareas))
= (True,(stricts,yesrules++norules,yesareas++noareas))
ft` (Reduce reductroot trace)
= ft`` (ft (fst hist,fst hist) trace)
where ft`` (False,sra) = exres
ft`` (found,sra) = (True,sra)
ft` (Annotate trace)
= ft`` (ft hist trace)
where ft`` (False,sra) = exres
ft`` (found,sra) = (True,sra)
exres = (False,newextract noetrc foldarea trace)
addstrict stricts (rule,areas) = (stricts,[rule],areas)
noetrc trace area = id
pair x y = (x,y)
only :: [.elem] -> .elem
only [x] = x
only xs = abort "only: not a singleton list"
/*
------------------------------------------------------------------------
`Extract foldarea trace (rules,areas)' folds the trace, creating rules
......
sucl/rewr.dcl
View file @ 331a9155
......@@ -43,7 +43,7 @@ getmapping
& == var
& == pvar
instantiate
rewrinstantiate
:: .(Graph sym pvar) // Pattern to instantiate with
pvar // Root of the pattern
var // Open node to instantiate
......
sucl/rewr.icl
View file @ 331a9155
......@@ -100,7 +100,7 @@ xunfold redexroot rule (heap,root,subject,matching)
= build (rulegraph rule) (ruleroot rule) (heap,[],subject,matching)
redirection = adjust redexroot rhs` id
instantiate
rewrinstantiate
:: .(Graph sym pvar) // Pattern to instantiate with
pvar // Root of the pattern
var // Open node to instantiate
......@@ -109,7 +109,7 @@ instantiate
| == var
& == pvar
instantiate pattern proot node (heap,graph)
rewrinstantiate pattern proot node (heap,graph)
| not closed
= (heap,graph)
= (heap``,graph``)
......
sucl/spine.dcl
View file @ 331a9155
......@@ -199,10 +199,10 @@ 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
:: (Graph sym var)
(var -> var)
(Spine sym var pvar)
(History sym var)
-> History sym var
| == var
& == pvar
sucl/spine.icl
View file @ 331a9155
......@@ -4,6 +4,7 @@ implementation module spine
import history
import rule
import dnc
import graph
import pfun
import basic
......@@ -260,276 +261,58 @@ ifopen open other spine
-> 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
:: (Graph sym var)
(var -> var)
(Spine sym var pvar)
(History sym var)
-> History sym var
| == 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))
extendhistory sgraph redirection spine history
= snd (foldspine (extendpair sgraph redirection) d d (const id) d (const d) (extendpartial sgraph) (const d) (extendredex sgraph history) d spine)
where d = (emptygraph,history)
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->var)
var
(Link var)
(LinkExtender sym var)
-> ( HistoryAssociation sym var
, HistoryPattern sym var
, LinkExtender sym var
)
(Graph sym var,History sym var)
-> (Graph sym var,History 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
// 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
(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
extendpair sgraph redirect snode (hgraph,history)
= (hgraph`,remap (redirect snode) [mkrgraph snode hgraph`:foldmap id [] history snode] (forget snode history))
where hgraph` = if sdef (updategraph snode scont hgraph) hgraph
(sdef,scont) = dnc (const "in extendpair") sgraph snode
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
:: (Graph sym var)
(Rule sym pvar)
(Pfun pvar var)
pvar
(Graph sym var,History sym var)
-> (Graph sym var,History sym var)
| == var
& == pvar
extendpartial sgraph rule matching subnode extendsub snode link restextender
= extendfunction sgraph rule matching ((==)subnode) (const extendsub) snode link restextender
extendpartial sgraph rule matching rnode (hgraph,history)
= (extgraph` sgraph rule matching hgraph,history)
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