Commit fca4aaa5 authored by Vincent Zweije's avatar Vincent Zweije
Browse files

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

which included commits to RCS files with non-trunk default branches.
parent 56ab3a53
......@@ -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
/*
------------------------------------------------------------------------
......
......@@ -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
......@@ -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
......
......@@ -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
......
......@@ -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)])
*/
......@@ -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
......
......@@ -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
......
......@@ -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
......
......@@ -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``)
......
......@@ -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
......@@ -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
, 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
</