implementation module graph
// $Id$
import pfun
import basic
import general
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
= GraphAlias !(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 = GraphAlias emptypfun
updategraph :: var .(Node sym var) !.(Graph sym var) -> .Graph sym var
updategraph var node graph = mapgraph (extend var node) graph
prunegraph :: var !.(Graph sym var) -> .Graph sym var
prunegraph var graph = mapgraph (restrict var) graph
restrictgraph :: .[var] .(Graph sym var) -> .Graph sym var | == var
restrictgraph vars graph = mapgraph (domres vars) graph
redirectgraph :: (var->var) !.(Graph sym var) -> .Graph sym var
redirectgraph redirection graph
= mapgraph (postcomp (mapsnd (map redirection))) graph
overwritegraph :: !.(Graph sym var) !.(Graph sym var) -> .Graph sym var
overwritegraph (GraphAlias newpf) oldgraph = mapgraph (overwrite newpf) 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
varcontents :: !.(Graph sym var) var -> (.Bool,Node sym var) | == var
varcontents (GraphAlias pfun) v
= (total (False,(nosym,noargs)) o postcomp found) pfun 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 seenboundfree
| isMember var seen = seenboundfree
| 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
(seen,boundfree=:(bound,free)) = seenboundfree
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
*/
printgraph :: .(Graph sym var) .[var] -> .[String] | toString sym & toString var & == var
printgraph graph nodes = printgraphBy toString toString graph nodes
printgraphBy :: (sym->String) (var->String) .(Graph sym var) .[var] -> .[String] | == var
printgraphBy showsym showvar graph nodes
= prntgrph showsym showvar (refcount graph nodes) graph nodes
prntgrph showsym showvar count graph nodes
= snd (foldlr pg ([],[]) nodes)
where pg node (seen,reprs)
= (seen2,[repr3:reprs])
where repr3
= if (not (isMember node seen) && def && count node>1)
(showvar node+++":"+++repr2)
repr2
(seen2,repr2)
= if (isMember node seen || not def)
(seen,showvar node)
(if (args==[])
(seen1,showsym func)
(seen1,"("+++showsym func+++foldr (+++) ")" (map ((+++)" ") repr1)))
(seen1,repr1) = foldlr pg ([node:seen],[]) args
(def,(func,args)) = varcontents 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
/*
Compilegraph compiles a graph from parts.
Uses in Miranda:
* reading a parsed program from a file.
*/
compilegraph :: ![(var,Node sym var)] -> Graph sym var
compilegraph nds = foldr (uncurry updategraph) emptygraph nds
/*
`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) ([],[],[]))) <--- "graph.isinstance ends"
/*
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.
`Instantiateargs' is the logical extension of `instantiate' to lists of node pairs.
*/
instantiate ::
(Graph sym pvar,Graph sym var)
(pvar,var)
([(pvar,var)],[(pvar,var)],[(pvar,var)])
-> ([(pvar,var)],[(pvar,var)],[(pvar,var)])
| == sym
& == var
& == pvar
instantiate (pgraph,sgraph) (pnode,snode) (seen,mapping,errs)
| isMember psnode seen
= (seen,mapping,errs)
| isMember pnode (map fst seen)
= ([psnode:seen],mapping,[psnode:errs])
| not pdef
= ([psnode:seen],[psnode:mapping],errs)
| not sdef
= ([psnode:seen],mapping,[psnode:errs])
| not (psym==ssym && eqlen pargs sargs)
= ([psnode:seen],mapping,[psnode:errs])
= (seen`,[psnode:mapping`],errs`)
where (pdef,(psym,pargs)) = varcontents pgraph pnode
(sdef,(ssym,sargs)) = varcontents sgraph snode
(seen`,mapping`,errs`) = instantiateargs (pgraph,sgraph) (zip2 pargs sargs) ([psnode:seen],mapping,errs)
psnode = (pnode,snode)
instantiateargs ::
(Graph sym pvar,Graph sym var)
[(pvar,var)]
([(pvar,var)],[(pvar,var)],[(pvar,var)])
-> ([(pvar,var)],[(pvar,var)],[(pvar,var)])
| == sym
& == var
& == pvar
instantiateargs psgraph [] sme = sme
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 sym var) (Graph sym pvar) [pvar] (Pfun pvar var) (Graph sym var) -> Graph sym var | == var & == pvar
extgraph sgraph pattern pnodes matching graph
= foldr addnode graph pnodes
where addnode pnode
= if (fst (varcontents pattern pnode)) (total id (postcomp addnode` matching) pnode) id
addnode` snode
= if sdef (updategraph snode scont) id
where (sdef,scont) = varcontents sgraph snode
mapgraph ::
!( (Pfun var1 (sym1,[var1]))
-> Pfun var2 (sym2,[var2])
)
!.(Graph sym1 var1)
-> .Graph sym2 var2
mapgraph f (GraphAlias pfun) = GraphAlias (f pfun)
instance == (Graph sym var) | == sym & == var
where (==) (GraphAlias pf1) (GraphAlias pf2)
= pf1 == pf2