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 [] = []
