Commit 899633cf authored by Vincent Zweije's avatar Vincent Zweije
Browse files

Implement checking the subject graph against the history

parent b01c6056
...@@ -2,16 +2,34 @@ definition module history ...@@ -2,16 +2,34 @@ definition module history
// $Id$ // $Id$
from graph import Graph
from spine import Spine from spine import Spine
from graph import Graph
from general import Optional
from StdOverloaded import == from StdOverloaded import ==
// Transitive necessities // Transitive necessities
from spine import Subspine from spine import Subspine
// A history relates node-ids in the subject graph to patterns
:: History sym var :: History sym var
:== [HistoryAssociation sym var]
// An association between a node-id in the subject graph and a history pattern
:: HistoryAssociation sym var
:== ( (Link 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
// 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 extendhistory
:: (Graph sym var) // Subject graph :: (Graph sym var) // Subject graph
(Spine sym var pvar) // Spine leading to the reduction operation (Spine sym var pvar) // Spine leading to the reduction operation
...@@ -20,3 +38,13 @@ extendhistory ...@@ -20,3 +38,13 @@ extendhistory
| == sym | == sym
& == var & == var
& == pvar & == pvar
// Check the current subject graph in the history
checkhistory
:: (History sym var)
[Link var]
(Graph sym var)
var
-> [HistoryPattern sym var]
| == sym
& == var
...@@ -31,27 +31,17 @@ import StdEnv ...@@ -31,27 +31,17 @@ import StdEnv
:: Link var :: Link var
:== Optional (var,Int) :== Optional (var,Int)
/*********************************************
* Extending the history according to a spine *
*********************************************/
// A function that associates specific patterns with extensible nodes // A function that associates specific patterns with extensible nodes
// To be used for extending history patterns // To be used for extending history patterns
:: LinkExtender sym var :: LinkExtender sym var
:== (Link var) // The extensible link to look for :== (Link var) // The extensible link to look for
-> HistoryPattern sym var // The associated pattern -> HistoryPattern sym var // The associated pattern
/*
> history * ** == [(**,[rgraph * **])]
> showhistory :: (*->[char]) -> (**->[char]) -> history * ** -> [char]
> showhistory showa showb = showlist (showpair showb (showlist (showrgraph showa showb)))
> printhistory :: (*->[char]) -> (**->[char]) -> history * ** -> [[char]]
> printhistory showa showb
> = concat.map print
> where print (node,rgraphs)
> = showb node:map2 (++) ("<= ":repeat " ") (map (printrgraph showa showb) rgraphs)
*/
extendhistory extendhistory
:: (Graph sym var) // Subject graph :: (Graph sym var) // Subject graph
(Spine sym var pvar) // Spine leading to the reduction operation (Spine sym var pvar) // Spine leading to the reduction operation
...@@ -159,14 +149,6 @@ extendopen _ _ link extender0 ...@@ -159,14 +149,6 @@ extendopen _ _ link extender0
newpattern = (link,histpat) newpattern = (link,histpat)
extender1 = adjust link histpat extender0 extender1 = adjust link histpat extender0
/*
> extendpartial :: graph * ** -> rule * *** -> pfun *** ** -> (graph * **,history * **) -> (graph * **,history * **)
> extendpartial sgraph rule matching (hgraph,history)
> = (extgraph' sgraph rule matching hgraph,history)
*/
extendpartial extendpartial
:: (Graph sym var) // Subject graph :: (Graph sym var) // Subject graph
(Rule sym pvar) // Applied rewrite rule (Rule sym pvar) // Applied rewrite rule
...@@ -322,6 +304,42 @@ extendnode sgraph rgraph matching issub extendsub (link,rnode) (newpattern0,rest ...@@ -322,6 +304,42 @@ extendnode sgraph rgraph matching issub extendsub (link,rnode) (newpattern0,rest
= (newpattern0,[Extensible link:rest],extender0) = (newpattern0,[Extensible link:rest],extender0)
(rdef,(rsym,rargs)) = varcontents rgraph rnode (rdef,(rsym,rargs)) = varcontents rgraph rnode
/************************************************
* Verifying a subject graph against the history *
************************************************/
checkhistory
:: (History sym var)
[Link var]
(Graph sym var)
var
-> [HistoryPattern sym var]
| == sym
& == var
checkhistory hist spinelinks sgraph snode
= foldr (checkassoc spinelinks sgraph snode) [] hist
checkassoc spinelinks sgraph snode (link,pat) rest
| isMember link spinelinks && 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
/****************
* Miscellaneous *
****************/
instance == (Optional a) | == a instance == (Optional a) | == a
where (==) No No = True where (==) No No = True
(==) (Yes x1) (Yes x2) = x1==x2 (==) (Yes x1) (Yes x2) = x1==x2
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment