aboutsummaryrefslogtreecommitdiff
path: root/sucl/trd.icl
diff options
context:
space:
mode:
Diffstat (limited to 'sucl/trd.icl')
-rw-r--r--sucl/trd.icl203
1 files changed, 203 insertions, 0 deletions
diff --git a/sucl/trd.icl b/sucl/trd.icl
new file mode 100644
index 0000000..5ecc2c9
--- /dev/null
+++ b/sucl/trd.icl
@@ -0,0 +1,203 @@
+implementation module trd
+
+import rule
+import graph
+import basic
+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] -> .(z:(Graph tsym tvar) -> .(x:[y:(var,tvar)] -> .result))) // Continuation
+ .[tvar] // Type heap
+ w:(Graph tsym tvar) // Type graph build so far
+ u:[v:(var,tvar)] // Assignment of type variables to variables
+ -> .result // Final result
+ | == var
+ & == trvar
+ , [u<=x,v<=y,w<=z]
+
+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 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:(x:(Graph sym var2) -> .result)) // Continuation
+ (.var->var2) // Redirection
+ u:(Graph sym var2) // Graph before redirection
+ -> .result // Final result
+ | == sym
+ & == var2
+ , [u<=x,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 [] = []