implementation module canon

// $Id$

import rule
import graph
import basic
import general
import StdEnv

/*

canon.lit - Area canonicalization
=================================

Description
-----------

This script defines functions for folding areas and generating canonical
forms from them for renewed symbolic reduction.

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

Interface
---------

Exported identifiers:

>   %export
>       canonise  ||  Transform an area into canonical form
>       foldarea  ||  Fold an area to an application of its assigned symbol
>       labelarea ||  Use a list of symbols to label a list of areas

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

Includes
--------

>   %include "basic.lit" -uncurry -split
>   %include "graph.lit" -extgraph
>   %include "rule.lit"

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

`Canonise heap' canonises an area to a  standard  form,  so  that  equal
areas  are  detected by the `=' operator.  Canonisation is done in three
steps:

(1) Splitting arguments to prevent too much sharing and  allowing  delta
    functions to be recognised.

(2) Adding extra arguments to the full complement according to the  type
    rule for the top symbol.

(3) Relabeling the nodes in a standard way.

>   canonise :: (*->rule **** *****) -> [***] -> rgraph * ** -> rgraph * ***
>   canonise typerule heap = relabel heap.etaexpand typerule.splitrg.relabel localheap

*/

canonise :: (sym -> Rule tsym tvar) [var2] (Rgraph sym var1) -> Rgraph sym var2 | == var1
canonise typerule heap rg
 = ((relabel heap o etaexpand typerule o splitrg o relabel localheap) rg <--- "canon.canonise ends") ---> "canon.canonise begins"

/*

>   split :: rgraph * num -> rgraph * num
>   split rgraph
>   =   foldsingleton single rgraph rgraph
>       where single root sym args = mkrgraph root (updategraph root (sym,fst (claim args (localheap--[root]))) emptygraph)

*/

splitrg :: (Rgraph sym Int) -> Rgraph sym Int
splitrg rgraph
 = foldsingleton single rgraph rgraph
   where single root sym args = mkrgraph root (updategraph root (sym,fst (claim args (removeMembers localheap [root]))) emptygraph)

/*
>   uncurry :: (*->rule **** *****) -> rgraph * num -> rgraph * num
>   uncurry typerule rgraph
>   =   f (nc root)
>       where f (True,(sym,args))
>             =   mkrgraph root (updategraph root (sym,fst (claim targs (args++localheap--nodelist graph [root]))) graph)
>                 where targs = lhs (typerule sym)
>             f cont = rgraph
>             nc = nodecontents graph
>             root = rgraphroot rgraph; graph = rgraphgraph rgraph
*/

etaexpand :: (sym->Rule tsym tvar) (Rgraph sym Int) -> Rgraph sym Int
etaexpand typerule rgraph
 = f (nc root)
   where f (True,(sym,args))
          = mkrgraph root (updategraph root (sym,fst (claim targs (args++(removeMembers localheap (varlist graph [root]))))) graph)
            where targs = arguments (typerule sym)
         f cont = rgraph
         nc = varcontents graph
         root = rgraphroot rgraph; graph = rgraphgraph rgraph

localheap :: [Int]
localheap =: [0..]

/*
------------------------------------------------------------------------

>   foldarea :: (rgraph * **->*) -> rgraph * ** -> (*,[**])
>   foldarea label rgraph
>   =   (label rgraph,foldsingleton single nosingle rgraph)
>       where single root sym args = args
>             nosingle = snd (varset (rgraphgraph rgraph) [rgraphroot rgraph])
*/

foldarea :: ((Rgraph sym var) -> sym) (Rgraph sym var) -> Node sym var | == var
foldarea label rgraph
 = ((id (labelrgraph,foldsingleton single nosingle rgraph)) <--- "canon.foldarea ends") ---> "canon.foldarea begins"
   where single root sym args = args
         nosingle = snd (graphvars (rgraphgraph rgraph) [rgraphroot rgraph])
         labelrgraph = (label rgraph <--- "canon.foldarea.labelrgraph ends") ---> "canon.foldarea.labelrgraph begins"

/*
------------------------------------------------------------------------

>   labelarea :: [rgraph * **] -> [*] -> rgraph * ** -> *
>   labelarea areas labels
>   =   foldmap id nolabel (maketable areas labels)
>       where nolabel = error "labelarea: no label assigned to area"

>   maketable :: [rgraph * **] -> [*] -> [(rgraph * **,*)]
>   maketable [] = const []
>   maketable (area:areas) labels
>   =   (area,label):maketable areas labels'
>       where (label,labels') = getlabel (nc aroot) labels
>             getlabel (True,(asym,aargs)) labels = (asym,labels), if ~or (map (fst.nc) aargs)
>             getlabel acont (label:labels) = (label,labels)
>             getlabel = error "maketable: out of labels"
>             nc = varcontents agraph
>             aroot = rgraphroot area; agraph = rgraphgraph area
*/

labelarea :: [Rgraph sym var] [sym] (Rgraph sym var) -> sym | == sym & == var
labelarea areas labels rg
 = ((foldmap--->"canon.labelarea uses foldmap") id nolabel ((maketable--->"canon.maketable begins from canon.labelarea") ((areas<---"canon.labelarea.areas ends")--->"canon.labelarea.areas begins") ((labels<---"canon.labelarea.labels ends")--->"canon.labelarea.labels begins")) ((rg<---"canon.labelarea.rg ends")--->"canon.labelarea.rg begins") <--- "canon.labelarea ends") ---> "canon.labelarea begins"
   where nolabel = abort "canon: labelarea: no label assigned to area"

maketable :: [Rgraph sym var] [sym] -> [(Rgraph sym var,sym)] | == var
maketable [] _ = [] <--- "canon.maketable ends empty"
maketable [area:areas] labels
 = [(((area<---"canon.maketable.area ends")--->"canon.maketable.area begins",(label<---"canon.maketable.label ends")--->"canon.maketable.label begins") <--- "canon.maketable.head ends") ---> "canon.maketable.head begins":(maketable--->"canon.maketable begins from maketable") areas labels`] <--- "canon.maketable ends nonempty"
   where (label,labels`) = getlabel (nc aroot) labels
         getlabel (True,(asym,aargs)) labels
          | not (or (map (fst o nc) aargs))
            = (asym,labels)
         getlabel acont [label:labels]
          = (label,labels)
         getlabel _ _
          = abort "canon: maketable: out of labels"
         nc = varcontents agraph
         aroot = rgraphroot area; agraph = rgraphgraph area

/*
------------------------------------------------------------------------

>   relabel :: [***] -> rgraph * ** -> rgraph * ***

>   relabel heap rgraph
>   =   mkrgraph (move root) graph'
>       where root = rgraphroot rgraph; graph = rgraphgraph rgraph
>             nodes = nodelist graph [root]
>             table = zip2 nodes heap
>             move = foldmap id nonew table
>             nonew = error "relabel: no new node assigned to node"
>             graph' = foldr addnode emptygraph table
>             addnode (node,node')
>             =   updategraph node' (sym,map move args), if def
>             =   id, otherwise
>                 where (def,(sym,args)) = nc node
>             nc = nodecontents graph
*/

relabel :: [var2] (Rgraph sym var1) -> Rgraph sym var2 | == var1
relabel heap rgraph
 = mkrgraph (move root) graph`
   where root = rgraphroot rgraph; graph = rgraphgraph rgraph
         nodes = varlist graph [root]
         table = zip2 nodes heap
         move = foldmap id nonew table
         nonew = abort "relabel: no new node assigned to node"
         graph` = foldr addnode emptygraph table
         addnode (node,node`)
          | def
            = updategraph node` (sym,map move args)
          = id
            where (def,(sym,args)) = nc node
         nc = varcontents graph

/*
>   foldsingleton
>   ::  (**->*->[**]->***) ->
>       *** ->
>       rgraph * ** ->
>       ***

>   foldsingleton single nosingle rgraph
>   =   f (nc root)
>       where f (True,(sym,args)) = single root sym args, if ~or (map (fst.nc) args)
>             f cont = nosingle
>             nc = nodecontents graph
>             root = rgraphroot rgraph; graph = rgraphgraph rgraph
*/

foldsingleton ::
    (var sym [var] -> pvar)
    pvar
    (Rgraph sym var)
 -> pvar
 |  == var

foldsingleton single nosingle rgraph
 = case nc root
   of (True,(sym,args))
       | not (or (map (fst o nc) args))
         -> single root sym args
      _
       -> nosingle
   where nc = varcontents graph
         root = rgraphroot rgraph; graph = rgraphgraph rgraph