implementation module trd

// $Id$

import rule
import graph
import basic
from general import --->
import StdEnv

/*

trd.lit - Type rule derivation
==============================

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

This module defines the derivation of a type rule from a given rule.

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

Interface
---------

Exported identifiers:

>   %export
>       ruletype  ||  Derive a type rule from a rule

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

Includes
--------

>   %include "basic.lit"
>   %include "pfun.lit"
>   %include "graph.lit"
>   %include "rule.lit"

Naming conventions:

    *      - symbol (sym)
    **     - node (node)
    ***    - type symbol (tsym)
    ****   - type node in type rule to build (tnode)
    *****  - type node in given type rules (trnode)

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

Implementation
--------------

`Ruletype' determines the type of a rule.

First, for every closed node, its type rule  is  copied  into  a  global
(initially  unconnected) type graph, and for every open node, a distinct
type node is allocated in the same type graph.  Then  for  every  closed
node n and argument n-i, the result type of n-i is unified with the i-th
argument type of n.

>   ruletype
>   ::  [****] ->
>       ((*,[**])->rule *** *****) ->
>       rule * ** ->
>       rule *** ****

>   ruletype theap typerule rule
>   =   foldr (buildtype typerule graph) bcont nodes theap emptygraph []
>       where args = lhs rule; root = rhs rule; graph = rulegraph rule
>             nodes = nodelist graph (root:args)
>             bcont theap tgraph assignment
>             =   foldr sharepair spcont pairs id tgraph assignment
>                 where pairs = mkpairs assignment
>             spcont redirection tgraph assignment
>             =   mkrule (map lookup args) (lookup root) tgraph
>                 where lookup = redirection.foldmap id notype assignment
>             notype = error "ruletype: no type node assigned to node"

*/

ruletype
 :: .[tvar]
    ((Node sym var) -> Rule tsym trvar)
    (Rule sym var)
 -> .Rule tsym tvar
 |  == var
 &  == tsym
 &  == tvar
 &  == trvar

ruletype theap typerule rule
= foldr (buildtype typerule graph) bcont nodes theap emptygraph []
  where args = arguments rule
        root = ruleroot rule
        graph = rulegraph rule
        nodes = varlist graph [root:args]
        bcont theap tgraph assignment
        = foldr sharepair spcont pairs id tgraph assignment
          where pairs = mkpairs assignment
        spcont redirection tgraph assignment
        = mkrule (map lookup args) (lookup root) tgraph
          where lookup = redirection o (foldmap id notype assignment)
        notype = abort "ruletype: no type node assigned to node"

/*

`Buildtype' builds the part of the global type graph corresponding to  a
node.   For  a closed node, the type rule is copied; for an open node, a
single type node is allocated.  Track is kept of which type  nodes  have
been assigned to the node and its arguments.

*/

buildtype
 :: .((Node sym var) -> Rule tsym trvar)                                       // Assignement of type rules to symbols
    .(Graph sym var)                                                            // Graph to which to apply typing
    var                                                                         // ???
    .([tvar] -> .(u:(Graph tsym tvar) -> .(v:[w:(var,tvar)] -> .result)))       // Continuation
    .[tvar]                                                                     // Type heap
    u:(Graph tsym tvar)                                                         // Type graph build so far
    x:[y:(var,tvar)]                                                            // Assignment of type variables to variables
 -> .result                                                                     // Final result
 |  == var
 &  == trvar
 ,  [x<=v,v y<=w,x<=y]

buildtype typerule graph node bcont theap tgraph assignment
| def
= bcont theap` tgraph` assignment`
= bcont (tl theap) tgraph [(node,hd theap):assignment]
  where (def,cont) = varcontents graph node
        (_,args) = cont
        trule = typerule cont
        trargs = arguments trule; trroot = ruleroot trule; trgraph = rulegraph trule
        trnodes = varlist trgraph [trroot:trargs]
        (tnodes,theap`) = (claim--->"basic.claim begins from trd.buildtype") trnodes theap
        matching = zip2 trnodes tnodes
        tgraph` = foldr addnode tgraph matching
        addnode (trnode,tnode)
        | trdef
        = updategraph tnode (mapsnd (map match) trcont)
        = id
          where (trdef,trcont) = varcontents trgraph trnode
        match = foldmap id nomatch matching
        nomatch = abort "buildtype: no match from type rule node to type node"
        assignment` = zip2 [node:args] (map match [trroot:trargs])++assignment

sharepair
 :: (.var,.var)                                    // Variables to share
    w:((.var->var2) -> v:((Graph sym var2) -> .result))       // Continuation
    (.var->var2)                                   // Redirection
    (Graph sym var2)                              // Graph before redirection
 -> .result                  // Final result
 |  == sym
 &  == var2
 ,  [v<=w]

sharepair lrnode spcont redirection graph
= share (mappair redirection redirection lrnode) spcont redirection graph

/*

`Share' shares two nodes in a graph by redirecting all  references  from
one  to the other, and sharing the arguments recursively.  The resulting
redirection function is also returned.

*/
/*
share ::
   (var,var)                                    // Variables to share
   ((var->var) (Graph sym var) -> result)       // Continuation
   (var->var)                                   // Redirection
   (Graph sym var)                              // Graph before redirection
   -> result | == sym & == var                  // Final result
*/
share lrnode scont redirect graph
| lnode==rnode
= scont redirect graph
| ldef && rdef
= foldr share scont lrargs redirect` graph`
= scont redirect` graph`
  where (lnode,rnode) = lrnode
        (ldef,(lsym,largs)) = varcontents graph lnode
        (rdef,(rsym,rargs)) = varcontents graph rnode
        lrargs
        | lsym<>rsym
        = abort "share: incompatible symbols"
        | not (eqlen largs rargs)
        = abort "share: incompatible arities"
        = zip2 (redargs largs) (redargs rargs)
        redargs = map adjustone
        redirect` = adjustone o redirect
        adjustone
        | ldef
        = adjust rnode lnode id
        = adjust lnode rnode id
        graph` = redirectgraph adjustone graph
/*
mkpairs :: [(var1,var2)] -> [(var2,var2)] | == var1
*/
mkpairs pairs
= f (map snd (partition fst snd pairs))
  where f [[x1,x2:xs]:xss] = [(x1,x2):f [[x2:xs]:xss]]
        f [xs:xss] = f xss
        f [] = []