diff options
Diffstat (limited to 'sucl/graph.icl')
| -rw-r--r-- | sucl/graph.icl | 379 |
1 files changed, 379 insertions, 0 deletions
diff --git a/sucl/graph.icl b/sucl/graph.icl new file mode 100644 index 0000000..3e7f848 --- /dev/null +++ b/sucl/graph.icl @@ -0,0 +1,379 @@ +implementation module graph + +import pfun +import basic +import StdEnv + +/* + +graph.lit - Unrooted graphs +=========================== + +Description +----------- + +This script implements an abstract type for unrooted graphs and useful +functions to manipulate them. + +*/ + +// A mapping from variables to nodes (unrooted) +:: Graph sym var + :== Pfun var (Node sym var) + +// A node, bearing the contents of a variable +:: Node sym var + :== (sym,[var]) + +// ==> Symbols and variables are going to be defined in different modules. +// They're here now because I don't want to throw them away. +:: Symbol + = Apply // Unwritten expression application + | Cons // Non-empty list + | Nil // Empty list + | Int Int // A specified integer + | Char Char // A specified character + | User String String // A user-supplied symbol + | Tuple Int // A tuple symbol of specified arity + | Select Int Int // A tuple selection operator of specified arity and index + | If // Predefined IF function + | Bool Bool // A specified boolean +// | MkRecord [Field] // Record construction? +// | GetField [Field] Field // Record field selection? + +:: Variable + = Named String // Variable was named in the program + | Anonymous Int // Implicit variable + +/* + +> emptygraph = emptypfun +> updategraph = extend +> prunegraph = restrict +> restrictgraph = domres +> redirectgraph = postcomp.mapsnd.map +> overwritegraph = overwrite +> showgraph showfunc shownode = showpfun shownode (showpair showfunc (showlist shownode)) +*/ + +// The empty set of bindings +emptygraph :: Graph .sym .var +emptygraph = emptypfun + +updategraph :: .var (Node .sym .var) (Graph .sym .var) -> Graph .sym .var +updategraph var node graph = extend var node graph + +prunegraph :: .var (Graph .sym .var) -> Graph .sym .var +prunegraph var graph = restrict var graph + +restrictgraph :: !.[var] .(Graph sym var) -> Graph sym var | == var +restrictgraph vars graph = domres vars graph + +redirectgraph :: (.var->.var) !(Graph .sym .var) -> Graph .sym .var | == var +redirectgraph redirection graph += postcomp (mapsnd (map redirection)) graph + +overwritegraph :: !(Graph .sym .var) (Graph .sym .var) -> Graph .sym .var +overwritegraph newgraph oldgraph = overwrite newgraph oldgraph + +movegraph :: (var1->.var2) !.[var1] .(Graph sym var1) -> Graph sym .var2 | == var1 +movegraph movevar varspace oldgraph += foldr addvar emptygraph varspace + where addvar var + | def + = updategraph (movevar var) (sym,map movevar args) + = id + where (def,(sym,args)) = varcontents oldgraph var + +/* +> nodecontents +> = total (False,(nosym,noargs)).postcomp s +> where s x = (True,x) +> nosym = error "nodecontents: getting symbol of open node" +> noargs = error "nodecontents: getting arguments of open node" +*/ + +varcontents :: !(Graph .sym var) var -> (.Bool,Node .sym var) | == var +varcontents g v += (total (False,(nosym,noargs)) o postcomp found) g v + where found x = (True,x) + nosym = abort "varcontents: getting symbol of free variable" + noargs = abort "varcontents: getting arguments of free variable" + +graphvars :: .(Graph sym var) !.[var] -> (.[var],.[var]) | == var +graphvars graph roots += graphvars` [] graph roots + +// Finds bound and free variables in a graph +// Excludes the variables only reachable through "prune" +graphvars` :: .[var] .(Graph sym var) .[var] -> (.[var],.[var]) | == var +graphvars` prune graph roots += snd (foldlr ns (prune,([],[])) roots) + where ns var (seen,boundfree=:(bound,free)) + | isMember var seen = (seen,boundfree) + | not def = ([var:seen],(bound,[var:free])) + = (seen`,([var:bound`],free`)) + where (seen`,(bound`,free`)) = foldlr ns ([var:seen],boundfree) args + (def,(_,args)) = varcontents graph var + +varlist :: .(Graph sym var) !.[var] -> .[var] | == var +varlist graph roots += depthfirst arguments id roots + where arguments var + | def = args + = [] + where (def,(_,args)) = varcontents graph var + +/* +> prefix graph without nodes +> = foldlr f (without,[]) nodes +> where f node (seen,nodes) +> = (seen,nodes), if member seen node +> = (seen',node:nodes'), otherwise +> where (seen',nodes') +> = (node:seen,nodes), if ~def +> = foldlr f (node:seen,nodes) args, otherwise +> (def,(sym,args)) = nodecontents graph node +*/ +prefix :: .(Graph sym var) .[var] !.[var] -> .([var],[var]) | == var +prefix graph without vars += foldlr f (without,[]) vars + where f var (seen,vars) + | isMember var seen = (seen,vars) + = (seen`,[var:vars`]) + where (seen`,vars`) + = if (not def) ([var:seen],vars) + (foldlr f ([var:seen],vars) args) + (def,(_,args)) = varcontents graph var + +/* +> printgraph showfunc shownode graph nodes +> = prntgrph showfunc shownode (refcount graph nodes) graph nodes + +> prntgrph showfunc shownode count graph +> = snd.foldlr pg ([],[]) +> where pg node (seen,reprs) +> = (seen2,repr3:reprs) +> where repr3 +> = shownode node++':':repr2, if ~member seen node & def & count node>1 +> = repr2, otherwise +> (seen2,repr2) +> = (seen,shownode node), if member seen node \/ ~def +> = (seen1,showfunc func), if args=[] +> = (seen1,'(':showfunc func++concat (map (' ':) repr1)++")"), otherwise +> (seen1,repr1) = foldlr pg (node:seen,[]) args +> (def,(func,args)) = nodecontents graph node + +> refcount graph +> = foldr rfcnt (const 0) +> where rfcnt node count +> = count', if count node>0 \/ ~def +> = foldr rfcnt count' args, otherwise +> where count' = inc node count +> (def,(func,args)) = nodecontents graph node + +> inc n f n = f n+1 +> inc m f n = f n +*/ +refcount :: .(Graph sym var) !.[var] -> (var -> Int) | == var +refcount graph roots += foldr rfcnt (const 0) roots + where rfcnt var count + | (count var>0) || (not def) = count` + = foldr rfcnt count` args + where count` = inccounter var count + (def,(_,args)) = varcontents graph var + +inccounter m f n = if (n==m) (f n+1) (f n) + +/* + +Compilegraph compiles a graph from parts. +Uses in Miranda: + * reading a parsed program from a file. + +> compilegraph :: [(**,(*,[**]))] -> graph * ** +> compilegraph = foldr (uncurry updategraph) emptygraph + +`Instance g1 g2' determines whether g2 is an instance of g1. +Uses in Miranda: + * strat.lit.m: checking whether the strategy is starting a graph that is already in the history. + * newfold.lit.m: checking whether a tail of the spine occurs in the history. + +> instance :: (graph * ***,***) -> (graph * **,**) -> bool +> instance (pgraph,pnode) (sgraph,snode) +> = errs=[] +> where (seen,mapping,errs) = instantiate (pgraph,sgraph) (pnode,snode) ([],[],[]) + +*/ + +isinstance + :: (.Graph sym pvar,pvar) + (.Graph sym var,var) + -> Bool + | == sym + & == var + & == pvar + +isinstance (pgraph,pvar) (sgraph,svar) += isEmpty (thd3 (findmatching (pgraph,sgraph) (pvar,svar) ([],[],[]))) + +/* + +Suppose `Instantiate (pattern,graph) (pnode,gnode) (seen,mapping,errs)' +returns `(seen',mapping',errs')'. + +Then `mapping'' is the best attempt at extending the `mapping' to show that `graph' is an instance of `pattern'. +If it is not, then `errs'' is `errs' extended with node pairs that fail to match. +In the mean time, the nodes pairs examined are added to `seen', and returned as `seen''. +Node pairs already in `seen' are assumed to have already been checked and are not checked again. + +Uses in Miranda: + * extract.lit.m: used to find instances of patterns in the termination history, while folding trace tips. + * transform.lit.m: Uses a different `instantiate' from rewr.lit.m. + +> instantiate :: (graph * ***,graph * **) -> (***,**) -> ([(***,**)],[(***,**)],[(***,**)]) -> ([(***,**)],[(***,**)],[(***,**)]) + +> instantiate (pgraph,sgraph) (pnode,snode) (seen,mapping,errs) +> = (seen,mapping,errs), if member seen psnode +> = (psnode:seen,mapping,psnode:errs), if member (map fst seen) pnode +> = (psnode:seen,psnode:mapping,errs), if ~pdef +> = (psnode:seen,mapping,psnode:errs), if ~sdef +> = (psnode:seen,mapping,psnode:errs), if ~(psym=ssym&eqlen pargs sargs) +> = (seen',psnode:mapping',errs'), otherwise +> where (pdef,(psym,pargs)) = nodecontents pgraph pnode +> (sdef,(ssym,sargs)) = nodecontents sgraph snode +> (seen',mapping',errs') = instantiateargs (pgraph,sgraph) (zip2 pargs sargs) (psnode:seen,mapping,errs) +> psnode = (pnode,snode) + +`Instantiateargs' is the logical extension of `instantiate' to lists of node pairs. + +> instantiateargs :: (graph * ***,graph * **) -> [(***,**)] -> ([(***,**)],[(***,**)],[(***,**)]) -> ([(***,**)],[(***,**)],[(***,**)]) + +> instantiateargs psgraph [] = id +> instantiateargs psgraph (psnode:psnodes) (seen,mapping,errs) +> = (seen'',mapping'',errs'') +> where (seen',mapping'',errs'') = instantiate psgraph psnode (seen,mapping',errs') +> (seen'',mapping',errs') = instantiateargs psgraph psnodes (seen',mapping,errs) + +*/ + +:: Matchstate var pvar + :== ( [(pvar,var)] // Pattern-subject var combo's already visited + , [(pvar,var)] // Mapping from pattern vars to subject vars + , [(pvar,var)] // Pattern-subject var combo's that don't match (different symbol or arities) + ) + +findmatching + :: (Graph sym pvar,Graph sym var) + .(pvar,var) + u:(Matchstate var pvar) + -> u:Matchstate var pvar + | == sym + & == var + & == pvar + +findmatching (pgraph,sgraph) (pvar,svar) (seen,mapping,errs) +| isMember psvar seen += (seen,mapping,errs) +| isMember pvar (map fst seen) += ([psvar:seen],mapping,[psvar:errs]) +| not pdef += ([psvar:seen],[psvar:mapping],errs) +| not sdef += ([psvar:seen],mapping,[psvar:errs]) +| not (psym==ssym && eqlen pargs sargs) += ([psvar:seen],mapping,[psvar:errs]) += (seen`,[psvar:mapping`],errs`) + where (pdef,(psym,pargs)) = varcontents pgraph pvar + (sdef,(ssym,sargs)) = varcontents sgraph svar + (seen`,mapping`,errs`) = findargmatching (pgraph,sgraph) (zip2 pargs sargs) ([psvar:seen],mapping,errs) + psvar = (pvar,svar) + +findargmatching + :: (Graph sym pvar,Graph sym var) + [.(pvar,var)] + u:(Matchstate var pvar) + -> v:Matchstate var pvar + | == sym + & == var + & == pvar + , [u<=v] + +findargmatching psgraph [] seenmappingerrs = seenmappingerrs +findargmatching psgraph [psvar:psvars] (seen,mapping,errs) += (seen``,mapping``,errs``) + where (seen`,mapping``,errs``) = findmatching psgraph psvar (seen,mapping`,errs`) + (seen``,mapping`,errs`) = findargmatching psgraph psvars (seen`,mapping,errs) + +/* + +------------------------------------------------------------------------ + +A folding function for graphs. +Uses in Miranda: + * clean.lit.m: pretty-printing rewrite rules. + * pretty.lit.m: pretty-printing rewrite rules. + +> foldgraph +> :: (**->***->***) -> +> (**->***) -> +> (*->[***]->***) -> +> graph * ** -> +> [**] -> +> [***] + +> foldgraph folddef foldref foldcont graph roots +> = foldedroots +> where count = refcount graph roots +> (unused,foldedroots) = foldlm fold ([],roots) +> fold (seen,node) +> = (seen,foldref node), if member seen node +> = (seen'',cond (def&count node>1) (folddef node folded) folded), otherwise +> where (seen'',folded) +> = (seen',foldcont sym foldedargs), if def +> = (node:seen,foldref node), otherwise +> (seen',foldedargs) = foldlm fold (node:seen,args) +> (def,(sym,args)) = nodecontents graph node + +`Paths' lists all paths in a graph. +Never used in Miranda. + +> paths :: graph * ** -> ** -> [[**]] +> paths graph node +> = paths' [] node [] +> where paths' top node rest +> = rest, if member top node +> = top':cond def (foldr (paths' top') rest args) rest, otherwise +> where (def,(sym,args)) = nodecontents graph node +> top' = node:top + +`Extgraph sgraph pattern pnodes matching' extends some graph according +to the closed nodes in sgraph that closed nodes in pgraph are mapped to. +That is, we take the nodes from `pnodes', see if they are closed, +follow the mapping to `sgraph', see if they are closed there too, +and if so, add the contents in `sgraph' to the graph we're extending. + +Uses in Miranda: + * newfold.lit.m: function `findspinepart', to find parts of a spine. + Specifically, to extend history patterns as one traverses down the trace. + * transtree.lit.m: to extend the history when the reduce transformation is applied. + * transform.lit.m: idem. + +`Extgraph' is excluded in most import statements, +but there doesn't seem to be any other definition of it. + +> extgraph :: graph * ** -> graph * *** -> [***] -> pfun *** ** -> graph * ** -> graph * ** +> extgraph sgraph pattern pnodes matching graph +> = foldr addnode graph pnodes +> where addnode pnode +> = total id (postcomp addnode' matching) pnode, if fst (nodecontents pattern pnode) +> = id, otherwise +> addnode' snode +> = updategraph snode scont, if sdef +> = id, otherwise +>|| = error "extgraph: closed node mapped to open node", otherwise +> || Could have used id, but let's report error when there is one... +> where (sdef,scont) = nodecontents sgraph snode + +*/ |