implementation module loop

// $Id$

import trace
import strat
import history
import spine
import rewr
import rule
import graph
import pfun
import basic
from general import Yes,No
import StdEnv

/*

loop.lit - Looping to produce a trace
=====================================

Description
-----------

This module describes the transformation of a  tree  of  spines  into  a
trace.   This  is where the actual transformations on graphs are applied
like instantiation, reduction or strict annotation.

------------------------------------------------------------

Types
-----

*/

/* The action itself takes various arguments, and returns a transformation
*/

:: Action sym var pvar
   :== (Actcont sym var pvar)  //  Continuation to do subsequent symbolic reduction
       (History sym var)       //  Termination patterns
       (Failinfo sym var pvar) //  Failed matches
       Bool                    //  Instantiation attempted
       [Bool]                  //  Strict arguments of function to generate
       var                     //  Root of subject graph
       (Graph sym var)         //  Subject graph
       [var]                   //  Heap of unused nodes
   ->  Transformation sym var pvar

/* Action continuation
   An action continuation takes the result of a single partial evaluation action,
   and ultimately collects all suchs actions into a trace.
*/

:: Actcont sym var pvar
   :== (History sym var)       //  Termination patterns
       (Failinfo sym var pvar) //  Failed matches
       Bool                    //  Instantiation attempted
       [Bool]                  //  Strict arguments of function to generate
       var                     //  Root of subject graph
       (Graph sym var)         //  Subject graph
       [var]                   //  Heap of unused nodes
   ->  Trace sym var pvar

/* Failinfo is a function type
   A function of this type assigns a list of rooted graphs to a varable.
   This list of rooted graphs are precisely those patterns that symfailedsym to
   match at the given variable in the subject graph.
*/

:: Failinfo sym var pvar
   :== var
   ->  [Rgraph sym pvar]

/*

------------------------------------------------------------

Implementation
--------------

*/

loop
 :: (((Graph sym pvar) pvar var -> ub:Bool) -> Strategy sym var pvar (Answer sym var pvar))
    ([Rgraph sym pvar] (Rgraph sym pvar) -> ub:Bool)
    !(.[var],.Rule sym var)
 -> Trace sym var pvar
 |  == sym
 &  == var
 &  == pvar

loop strategy matchable (initheap,rule)
= maketrace inithistory initfailinfo initinstdone initstricts initsroot initsubject initheap

  where maketrace history failinfo instdone stricts sroot subject heap
        = Trace stricts (mkrule sargs sroot subject) answer history transf
          where answer = makernfstrategy history (strategy matchable`) rnfnodes sroot subject
                transf = transform sroot sargs answer maketrace history failinfo instdone stricts sroot subject heap

                rnfnodes = removeDup (listselect stricts sargs++fst (graphvars subject sargs))

                matchable` pgraph pnode snode
                = matchable (failinfo snode) (mkrgraph pnode pgraph)

        inithistory = []
        initfailinfo = const []
        initinstdone = False
        initstricts = map (const False) sargs

        sargs = arguments rule; initsroot = ruleroot rule; initsubject = rulegraph rule

listselect :: [.Bool] [.elem] -> [.elem]
listselect _ _ = undef

initrule
 :: ![var]
    (sym->[pvar])
    sym
 -> ([var],Rule sym var)

initrule [root:heap] template sym
= (heap`,mkrule args root (updategraph root (sym,args) emptygraph))
  where (args,heap`) = claim (template sym) heap
initrule _ _ _
= abort "initrule: out of heap space"

/* ------------------------------------------------------------------------ */

transform
 :: var                    // Top of spine (starting point for strategy)
    [var]                  // Arguments of function to generate
    !(Answer sym var pvar) // Result of strategy
 -> Action sym var pvar
 |  == var
 &  == pvar

transform anode sargs (Yes spine)
= selectfromtip (spinetip spine)
  where selectfromtip (nid,Open rgraph) = tryinstantiate nid rgraph anode sargs
        selectfromtip (nid,Redex rule matching) = tryunfold nid rule matching spine
        selectfromtip (nid,Strict) = tryannotate nid sargs
        selectfromtip spine = dostop

transform anode sargs No
= dostop

// ==== ATTEMPT TO INSTANTIATE A FREE VARIABLE WITH A PATTERN ====

tryinstantiate
 :: var               // The open node
    (Rgraph sym pvar) // The pattern to instantiate with
    var               // The root of the spine
    [var]             // Arguments of the function to generate
 -> Action sym var pvar
 |  == var
 &  == pvar

tryinstantiate onode rpattern anode sargs
= act
  where act continue history failinfo instdone stricts sroot subject heap
        | anode==sroot                                   // Check if strategy applied at root
          && goodorder strictargs sargs subject subject` // Check if order of arguments of rule ok
        = Instantiate success fail
        = Stop
          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)
                proot = rgraphroot rpattern; pgraph = rgraphgraph rpattern

                stricts` = if instdone stricts (map2 ((||) o (==) onode) sargs stricts)
                // Quickly annotate the open node as strict if this is the first instantiation

                strictargs = [sarg\\(True,sarg)<-zip2 stricts` sargs]

goodorder
 :: [var]
    [var]
    (Graph sym var)
    (Graph sym var)
 -> Bool
 |  == var

goodorder stricts sargs subject subject`
= startswith match match`
  where match = removeMembers (fst (graphvars subject sargs)) stricts
        match` = removeMembers (fst (graphvars subject` sargs)) stricts

// See if second argument list has the first one as its initial part
startswith
 :: .[elem] // list S
    .[elem] // list L
 -> .Bool   // whether L starts with S
 |  == elem

startswith [] _ = True
startswith [x:xs] [y:ys]
| x==y
= startswith xs ys
startswith _ _  = False


// ==== ATTEMPT TO UNFOLD A REWRITE RULE ====

tryunfold
 :: var                  // The root of the redex
    (Rule sym pvar)      // The rule to unfold
    (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
 &  == pvar

tryunfold redexroot rule matching spine
= act
  where act continue history failinfo instdone stricts sroot subject heap
        = Reduce reductroot trace
          where (heap`,sroot`,subject`,matching`)
                = 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
                trace = continue history` failinfo instdone stricts sroot` subject` heap`

tryannotate
 :: var   // The node to be made strict
    [var] // Arguments of the function to generate
 -> Action sym var pvar
 |  == var

tryannotate strictnode sargs
= act
  where act continue history failinfo instdone stricts sroot subject heap
        | not instdone && isMember strictnode sargs
        = Annotate trace
        = Stop
          where stricts` = map2 ((||) o (==) strictnode) sargs stricts
                trace = continue history failinfo instdone stricts` sroot subject heap


// ==== STOP PARTIAL EVALUATION ====

dostop
 :: Action sym var pvar

dostop
= ds
  where ds continue history failinfo instdone stricts sroot subject heap = Stop