path: root/sucl/graph.icl

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

*/