path: root/sucl/loop.icl

implementation module loop

// $Id$

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

mstub = stub "loop"
block func = mstub func "blocked for debugging"

/*

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.

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

The function that produces a trace is given an initial task expression.

The function first determines a transformation (Reduce,Annotate,Instantiate) to
apply, using the strategy.

This may fail when the termination history indicates a required abstraction
higher up.  In that case, return at once with failure, and the current graph
(with shared parts excluded) as the most specific generaliser.

After application of the transformation, a trace is produced for the resulting
graph(s).

However, the production of the subtraces may fail initially because of a
necessary abstraction higher-up which wasn't there (introduced recursion).

Therefore, producing a trace can return one of two results: either a successful
trace, or failure, with an indication of which abstraction was actually
necessary.

The needed generalisation is computed by taking the most specific generaliser
for each pattern in the termination history.

In the general case, generation of the subtraces fails for both the history
pattern of the current transformation, and some patterns higher up (which were
also passed to the trace generation function.  There are now two courses of
action:

[1] Apply abstraction instead of the current transformation.  Use the returned
    most specific generaliser and the original graph to determine how to
    abstract.  Then, generate subtraces.  There should be no more abstractions
    necessary for the current node, because they should be handled in the
    graphs resulting from the abstraction.[*]

[2] Immediately return the failure, assuming (rule of thumb) that when the
    upper generalisation was necessary, the lower one won't make it go away.
    This is probably an optimisation of the optimisation process, but it can be
    important, as some backtracking code (exponential!) may not have to be
    executed.

[*] This may not be entirely true in the case of sharing.  Because shared parts
    must be pruned, the termination pattern may get smaller in the abstraction
    operation.

Questions:

[?] Which would yield better results and/or perform better: [1] or [2] above?

[?] Must the abstracted areas be associated with termination patterns that
    caused their introduction?  Or somehow with the trace node where they were
    introduced?  The termination patterns don't have to be the same over
    different branches of the trace!  Do they play a role at all in selecting
    the abstracted part?  Actually, they don't.  We just need their roots so we
    can find the corresponding subgraphs and determine the MSG's.

It would appear we can traverse the trace when everything is done and collected
all the introduced functions from it.

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

*/

/* Disable the new abstraction node
   Unsafe subtraces are going to be pruned again.

:: FallibleTrace sym var pvar
   = GoodTrace (Trace sym var pvar)
   | NeedAbstraction [Rgraph sym var]

:: Strat sym var pvar
   :== (History sym var)
       (Rgraph sym var)
    -> Answer sym var pvar

maketrace
 :: (Strat sym var pvar)        // The strategy
    (History sym var)           // Patterns to stop partial evaluation
    (Rgraph sym var)            // Subject graph
 -> FallibleTrace sym var pvar  // The result

maketrace strategy history subject
 = ( case answer
     of No                          // Root normal form, abstract and continue with arguments
         -> handlernf
        Yes spine                   // Do something, even if it is to fail
         -> ( case subspine
              of Cycle              // Cycle in spine.  Generate x:_Strict x x with _Strict :: !a b -> b.  Probably becomes a #!
                  -> handlecycle
                 Delta              // Primitive function.  Abstract its application and continue with remainder.
                  -> handledelta
                 Force n (spine)    // Shouldn't happen
                  -> abort "loop: maketrace: spinetip returned Force???"
                 MissingCase        // Missing case.  Generate _MissingCase, possibly parametrised with user function?
                  -> handlemissingcase
                 Open pattern       // Need instantiation.  Generate two branches, extend history (for both) and continue.
                  -> handleopen pattern
                 Partial rule match rulenode spine
                  -> abort "loop: maketrace: spinetop returned Partial???"
                 Unsafe histpat     // Require pattern from history.
                  -> handleunsafe histpat // If we have a more general version with a name attached, use that.  
                                    // Otherwise, fail with the corresponding subgraph
                 Redex rule match   // Found a redex.  Unfold, extend history and continue.
                  -> handleredex rule match
                 Strict             // Need to put a strictness annotation on an open node-id.
                  -> handlestrict   // Abstract _Strict <mumble> <mumble> and continue with rest.
            ) spine
            where (redexroot,subspine) = spinetip spine
   ) strategy history subject
   where answer = strategy history subject

handlernf :: (Strat sym var pvar) (History sym var) (Rgraph sym var) -> FallibleTrace sym var pvar
handlernf _ _ _ = undef

handlecycle :: (Spine sym var pvar) (Strat sym var pvar) (History sym var) (Rgraph sym var) -> FallibleTrace sym var pvar
handlecycle _ _ _ _ = undef

handledelta :: (Spine sym var pvar) (Strat sym var pvar) (History sym var) (Rgraph sym var) -> FallibleTrace sym var pvar
handledelta _ _ _ _ = undef

handlemissingcase :: (Spine sym var pvar) (Strat sym var pvar) (History sym var) (Rgraph sym var) -> FallibleTrace sym var pvar
handlemissingcase _ _ _ _ = undef

handleopen :: (Rgraph sym pvar) (Spine sym var pvar) (Strat sym var pvar) (History sym var) (Rgraph sym var) -> FallibleTrace sym var pvar
handleopen _ _ _ _ _ = undef

handleunsafe :: (HistoryPattern sym var) (Spine sym var pvar) (Strat sym var pvar) (History sym var) (Rgraph sym var) -> FallibleTrace sym var pvar
handleunsafe _ _ _ _ _ = undef

handleredex :: (Rule sym pvar) (Pfun pvar var) (Spine sym var pvar) (Strat sym var pvar) (History sym var) (Rgraph sym var) -> FallibleTrace sym var pvar
handleredex _ _ _ _ _ _ = undef

handlestrict :: (Spine sym var pvar) (Strat sym var pvar) (History sym var) (Rgraph sym var) -> FallibleTrace sym var pvar
handlestrict _ _ _ _ = undef

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

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
 &  toString sym    // Debugging
 &  toString var    // Debugging
 &  <<< var         // Debugging

// loop _ _ _ = block "loop"
loop strategy matchable (initheap,rule)
= result
  where result = maketrace inithistory initfailinfo initinstdone initstricts initsroot initsubject initheap
        maketrace history failinfo instdone stricts sroot subject heap
        = (Trace stricts currentrule answer history transf ---> ("loop.loop.maketrace rule "+++ruleToString toString currentrule)) ---> ("loop.loop.maketrace history "+++historyToString history)
          where answer = makernfstrategy history (strategy matchable`) rnfnodes sroot subject
                transf = (transform--->"loop.transform begins from loop.loop") 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)

                currentrule = mkrule sargs sroot subject

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

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

listselect :: [.Bool] [.elem] -> [.elem]
listselect [True:bs] [x:xs] = [x:listselect bs xs]
listselect [False:bs] [x:xs] = listselect bs xs
listselect _ _ = []

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--->"basic.claim begins from loop.initrule") (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
 |  == sym
 &  == var
 &  == pvar

transform anode sargs (Yes spine)
= (selectfromtip--->"loop.transform.selectfromtip begins from loop.transform") (spinetip spine) <--- "loop.transform ends for some spine"
  where selectfromtip (nid,Open rgraph) = (tryinstantiate--->"loop.tryinstantiate begins from loop.transform.selectfromtip") nid rgraph anode sargs <--- "loop.transform.selectfromtip ends for Open spine"
        selectfromtip (nid,Redex rule matching) = (tryunfold--->"loop.tryunfold begins from loop.transform.selectfromtip") nid rule matching spine <--- "loop.transform.selectfromtip ends for Redex spine"
        selectfromtip (nid,Strict) = (tryannotate--->"loop.tryannotate begins from loop.transform.selectfromtip") nid sargs <--- "loop.transform.selectfromtip ends for Strict spine"
        selectfromtip (nid,Cycle) = (dostop--->"loop.dostop begins from loop.transform.selectfromtip") <--- "loop.transform.selectfromtip ends for Cycle spine"
        selectfromtip (nid,Delta) = (dostop--->"loop.dostop begins from loop.transform.selectfromtip") <--- "loop.transform.selectfromtip ends for Delta spine"
        selectfromtip (nid,Force _ _) = (dostop--->"loop.dostop begins from loop.transform.selectfromtip") <--- "loop.transform.selectfromtip ends for Force spine"
        selectfromtip (nid,MissingCase) = (dostop--->"loop.dostop begins from loop.transform.selectfromtip") <--- "loop.transform.selectfromtip ends for MissingCase spine"
        selectfromtip (nid,Partial _ _ _ _) = (dostop--->"loop.dostop begins from loop.transform.selectfromtip") <--- "loop.transform.selectfromtip ends for Partial spine"
        selectfromtip (nid,Unsafe _) = (dostop--->"loop.dostop begins from loop.transform.selectfromtip") <--- "loop.transform.selectfromtip ends for Unsafe spine"
        //selectfromtip spine = (dostop--->"loop.dostop begins from loop.transform.selectfromtip") <--- "loop.transform.selectfromtip ends for other spine"

transform anode sargs No
= (dostop--->"loop.dostop begins from loop.transform") <--- "loop.transform ends for no spine"

// ==== 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 <--- "loop.tryinstantiate ends"
  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 ipattern 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
                ipattern = mkrgraph onode subject`
                (heap`,subject`) = rewrinstantiate 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 = fst (graphvars subject sargs)--stricts
        match` = 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
 |  == sym
 &  == var
 &  == pvar

tryunfold redexroot rule matching spine
= act <--- "loop.tryunfold ends"
  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)
                history` = extendhistory subject redirect spine history
                redirect = adjust redexroot reductroot id
                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 <--- "loop.tryannotate ends"
  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 <--- "loop.dostop ends"
  where ds continue history failinfo instdone stricts sroot subject heap = Stop