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

which included commits to RCS files with non-trunk default branches.

git-svn-id: https://svn.cs.ru.nl/repos/clean-compiler/trunk@592 1f8540f1-abd5-4d5b-9d24-4c5ce8603e2d

2 files changed, 70 insertions, 24 deletions

diff --git a/sucl/history.dcl b/sucl/history.dcl
index b27567b..cacc651 100644
--- a/sucl/history.dcl
+++ b/sucl/history.dcl
@@ -2,16 +2,34 @@ definition module history
 
 // $Id$
 
-from graph import Graph
 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]
+
+// 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
  :: (Graph sym var)         // Subject graph
     (Spine sym var pvar)    // Spine leading to the reduction operation
@@ -20,3 +38,13 @@ extendhistory
  |  == sym
  &  == var
  &  == pvar
+
+// Check the current subject graph in the history
+checkhistory
+ :: (History sym var)
+    [Link var]
+    (Graph sym var)
+    var
+ -> [HistoryPattern sym var]
+ |  == sym
+ &  == var
diff --git a/sucl/history.icl b/sucl/history.icl
index 42c8315..ab49965 100644
--- a/sucl/history.icl
+++ b/sucl/history.icl
@@ -31,27 +31,17 @@ import StdEnv
 :: Link var
    :== 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
 
-/*
-
->   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
  :: (Graph sym var)         // Subject graph
     (Spine sym var pvar)    // Spine leading to the reduction operation
@@ -159,14 +149,6 @@ extendopen _ _ link extender0
          newpattern = (link,histpat)
          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
  :: (Graph sym var)             // Subject graph
     (Rule sym pvar)             // Applied rewrite rule
@@ -322,6 +304,42 @@ extendnode sgraph rgraph matching issub extendsub (link,rnode) (newpattern0,rest
           = (newpattern0,[Extensible link:rest],extender0)
          (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
  where (==) No No = True
        (==) (Yes x1) (Yes x2) = x1==x2