implementation module loop import trace import strat import history import spine import rewr import rule import graph import pfun import basic 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 (Present 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 Absent = 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