Translate module newtest (main module)

Cutoff points (undefs): fullfold from module newfold
                        continuations for strategy answers in module loop

sucl/Makefile

@@ -27,17 +27,21 @@ $(SYS)/%.abc: %.icl
 
 $(SYS)/supercompile.abc: supercompile.icl supercompile.dcl convert.dcl
 $(SYS)/convert.abc: convert.icl convert.dcl coreclean.dcl rule.dcl graph.dcl basic.dcl
-$(SYS)/cli.abc: cli.icl cli.dcl absmodule.dcl coreclean.dcl law.dcl strat.dcl rule.dcl basic.dcl
-$(SYS)/coreclean.abc: coreclean.icl coreclean.dcl strat.dcl spine.dcl rule.dcl graph.dcl
-$(SYS)/law.abc: law.icl law.dcl coreclean.dcl strat.dcl spine.dcl rule.dcl graph.dcl dnc.dcl basic.dcl
-$(SYS)/loop.abc: loop.icl loop.dcl trace.dcl strat.dcl history.dcl rule.dcl graph.dcl basic.dcl
-$(SYS)/strat.abc: strat.icl strat.dcl history.dcl spine.dcl dnc.dcl rule.dcl graph.dcl pfun.dcl basic.dcl
-$(SYS)/history.abc: history.icl history.dcl spine.dcl rule.dcl graph.dcl basic.dcl
-$(SYS)/spine.abc: spine.icl spine.dcl rule.dcl pfun.dcl basic.dcl
+$(SYS)/newtest.abc: newtest.icl newtest.dcl newfold.dcl cli.dcl canon.dcl coreclean.dcl loop.dcl trace.dcl spine.dcl history.dcl complete.dcl trd.dcl rule.dcl graph.dcl basic.dcl
+$(SYS)/newfold.abc: newfold.icl newfold.dcl trace.dcl spine.dcl history.dcl rule.dcl
+$(SYS)/extract.abc: extract.icl extract.dcl 
+$(SYS)/cli.abc: cli.icl cli.dcl law.dcl coreclean.dcl strat.dcl absmodule.dcl rule.dcl dnc.dcl graph.dcl basic.dcl
+$(SYS)/canon.abc: canon.icl canon.dcl rule.dcl graph.dcl basic.dcl
+$(SYS)/law.abc: law.icl law.dcl coreclean.dcl strat.dcl spine.dcl rule.dcl dnc.dcl graph.dcl basic.dcl
+$(SYS)/coreclean.abc: coreclean.icl coreclean.dcl strat.dcl spine.dcl rule.dcl graph.dcl basic.dcl
+$(SYS)/loop.abc: loop.icl loop.dcl strat.dcl trace.dcl spine.dcl history.dcl rewr.dcl rule.dcl graph.dcl pfun.dcl basic.dcl
+$(SYS)/strat.abc: strat.icl strat.dcl spine.dcl history.dcl rule.dcl dnc.dcl graph.dcl pfun.dcl basic.dcl
 $(SYS)/absmodule.abc: absmodule.icl absmodule.dcl rule.dcl
-$(SYS)/trace.abc: trace.icl trace.dcl rule.dcl
+$(SYS)/trace.abc: trace.icl trace.dcl spine.dcl history.dcl rule.dcl basic.dcl
+$(SYS)/spine.abc: spine.icl spine.dcl history.dcl rule.dcl graph.dcl pfun.dcl basic.dcl
+$(SYS)/history.abc: history.icl history.dcl rule.dcl graph.dcl pfun.dcl basic.dcl
 $(SYS)/complete.abc: complete.icl complete.dcl graph.dcl
-$(SYS)/rewr.abc: rewr.icl rewr.dcl graph.dcl pfun.dcl basic.dcl
+$(SYS)/rewr.abc: rewr.icl rewr.dcl rule.dcl graph.dcl pfun.dcl basic.dcl
 $(SYS)/trd.abc: trd.icl trd.dcl rule.dcl graph.dcl basic.dcl
 $(SYS)/rule.abc: rule.icl rule.dcl graph.dcl basic.dcl
 $(SYS)/dnc.abc: dnc.icl dnc.dcl graph.dcl

sucl/cli.dcl

@@ -3,8 +3,20 @@ definition module cli
 // $Id$
 
 from coreclean import SuclSymbol,SuclVariable,SuclTypeSymbol,SuclTypeVariable
+from strat import Strategy
 from rule import Rule
+from graph import Graph
+from StdOverloaded import ==
+
+// Transitive necessities
+
+from strat import Substrategy
+from spine import Spine,Subspine
+from graph import Node
 
 :: Cli
 
 typerule :: Cli SuclSymbol -> Rule SuclTypeSymbol SuclTypeVariable
+exports :: Cli -> [SuclSymbol]
+complete :: Cli -> [SuclSymbol] -> Bool
+clistrategy :: Cli ((Graph SuclSymbol SuclVariable) SuclVariable var -> Bool) -> Strategy SuclSymbol var SuclVariable answer | == var

sucl/cli.icl

@@ -2,11 +2,12 @@ implementation module cli
 
 // $Id$
 
-import absmodule
-import coreclean
 import law
+import coreclean
 import strat
+import absmodule
 import rule
+import dnc
 import basic
 import StdEnv
 
@@ -117,12 +118,18 @@ Abstype implementation.
 >   stripexports main (tdefs,(es,as,ts,rs)) = (tdefs,([User m i|User m i<-es;m=main],as,ts,rs))
 
 >   exports (tdefs,(es,as,ts,rs)) = es
+*/
+
+exports :: Cli -> [SuclSymbol]
+exports m = m.exportedsymbols
 
+/*
 >   typerule (tdefs,(es,as,ts,rs)) = fst.maxtypeinfo ts
 */
 
 typerule :: Cli SuclSymbol -> Rule SuclTypeSymbol SuclTypeVariable
-typerule _ _ = undef
+typerule m sym
+= fst (maxtypeinfo m.typerules sym)
 
 /*
 >   rules (tdefs,(es,as,ts,rs)) = foldmap Present Absent rs
@@ -166,7 +173,12 @@ maxtypeinfo defs sym = extendfn defs coretypeinfo sym
 >   constrs ((tes,tas,tcs),defs) = tcs
 
 >   complete ((tes,tas,tcs),(es,as,ts,rs)) = mkclicomplete tcs (fst.maxtypeinfo ts)
+*/
+
+complete :: Cli -> [SuclSymbol] -> Bool
+complete m = mkclicomplete m.typeconstructors (fst o maxtypeinfo m.typerules)
 
+/*
 >   showcli = printcli
 
 >   mkclicomplete
@@ -181,7 +193,24 @@ maxtypeinfo defs sym = extendfn defs coretypeinfo sym
 >   =   foldmap superset (corecomplete tsym) tcs tsym syms, otherwise
 >       where trule = typerule (hd syms)
 >             (tdef,(tsym,targs)) = dnc (const "in mkclicomplete") (rulegraph trule) (rhs trule)
+*/
+
+mkclicomplete ::
+    [(SuclTypeSymbol,[SuclSymbol])]
+    (SuclSymbol->Rule SuclTypeSymbol tvar)
+    [SuclSymbol]
+ -> Bool
+ |  == tvar
+
+mkclicomplete tcs typerule [] = False
+mkclicomplete tcs typerule syms
+| not tdef
+  = False
+= foldmap superset (corecomplete tsym) tcs tsym syms
+  where trule = typerule (hd syms)
+        (tdef,(tsym,_)) = dnc (const "in mkclicomplete") (rulegraph trule) (ruleroot trule)
 
+/*
 ------------------------------------------------------------------------
 
 >   printcli :: module symbol node typesymbol typenode -> [char]

sucl/convert.icl

@@ -41,7 +41,7 @@ convert_fundef fundef (typerulemap,strictsmap,fundefs0,kindmap)
    , [(funsym,kind):kindmap]
    )
    where {fun_symb,fun_body,fun_type,fun_kind} = fundef
-         funsym = SuclUser fun_symb.id_info
+         funsym = SuclUser fun_symb
          (typerule,stricts) = foldoptional notyperule convert_symboltype fun_type
          notyperule = abort "convert: convert_fundef: fun_type is absent"
          fundefs1 = convert_functionbody funsym fun_body fundefs0
@@ -188,7 +188,7 @@ convert_expression bounds (App appinfo) ((heap0,seen0),(nodes0,fundefs0,globals0
    where [root:heap1] = heap0
          ((heap2,seen1),(nodes1,fundefs1,globals1,args0))
           = convert_expressions bounds appinfo.app_args ((heap1,seen0),(nodes0,fundefs0,globals0))
-         nodes2 = [(root,(SuclUser appinfo.app_symb.symb_name.id_info,args0)):nodes1]
+         nodes2 = [(root,(SuclUser appinfo.app_symb.symb_name,args0)):nodes1]
 
 convert_expression bounds (expr @ exprs) ((heap0,seen0),(nodes0,fundefs0,globals0,rest))
  = ((heap2,seen1),(nodes2,fundefs1,globals1,[root:rest]))
@@ -270,7 +270,7 @@ convert_algebraic_pattern ap ((heap0,seen0),(nodes0,rest))
          argmap = [(fv.fv_info_ptr,SuclNamed fv.fv_info_ptr) \\ fv <- ap.ap_vars]
          seen1 = argmap++seen0
          args0 = map snd argmap
-         nodes1 = [(root,(SuclUser ap.ap_symbol.glob_object.ds_ident.id_info,args0)):nodes0]
+         nodes1 = [(root,(SuclUser ap.ap_symbol.glob_object.ds_ident,args0)):nodes0]
 
 convert_basic_branch branch ((heap0,seen0),(globals0,fundefs0,alternatives0))
  = ((heap2,seen2),(globals1,fundefs1,alternatives1))
@@ -313,4 +313,4 @@ cts_exports :: {#FunType} -> [SuclSymbol]
 cts_exports funtypes = [convert_funtype funtype\\funtype<-:funtypes]
 
 convert_funtype :: FunType -> SuclSymbol
-convert_funtype funtype = SuclUser funtype.ft_symb.id_info
+convert_funtype funtype = SuclUser funtype.ft_symb

sucl/coreclean.dcl

@@ -34,10 +34,11 @@ from StdString import String
 sucltypeheap :: [SuclTypeVariable]
 
 :: SuclSymbol
- = SuclUser SymbolPtr
+ = SuclUser Ident
  | SuclCase ExprInfoPtr
  | SuclApply Int
  | SuclInt Int
+ | SuclChar Char
  | SuclReal Real
  | SuclBool Bool
 
@@ -52,8 +53,13 @@ sucltypeheap :: [SuclTypeVariable]
 
 suclheap :: [SuclVariable]
 
+instance == SuclTypeSymbol
+instance == SuclTypeVariable
 instance == SuclSymbol
 instance == SuclVariable
 
 // Get the type rule and strictness of a built in core clean symbol
 coretypeinfo :: SuclSymbol -> (Rule SuclTypeSymbol SuclTypeVariable,[Bool])
+
+// Determine if a list of constructors completely covers a given type
+corecomplete :: SuclTypeSymbol -> [SuclSymbol] -> Bool

sucl/coreclean.icl

@@ -6,7 +6,10 @@ import strat
 import spine
 import rule
 import graph
+import basic
+import StdCompare
 import syntax
+//import StdEnv
 
 :: SuclTypeSymbol
  = SuclUSER TypeSymbIdent
@@ -27,10 +30,11 @@ sucltypeheap :: [SuclTypeVariable]
 sucltypeheap =: map SuclANONYMOUS [0..]
 
 :: SuclSymbol
- = SuclUser SymbolPtr
+ = SuclUser Ident
  | SuclCase ExprInfoPtr
  | SuclApply Int
  | SuclInt Int
+ | SuclChar Char
  | SuclReal Real
  | SuclBool Bool
 
@@ -46,8 +50,25 @@ sucltypeheap =: map SuclANONYMOUS [0..]
 suclheap :: [SuclVariable]
 suclheap =: map SuclAnonymous [0..]
 
+instance == SuclTypeSymbol
+where (==) (SuclUSER tsid1 ) (SuclUSER tsid2 ) = tsid1==tsid2
+      (==) (SuclFN   arity1) (SuclFN   arity2) = arity1==arity2
+      (==)  SuclINT           SuclINT          = True
+      (==)  SuclCHAR          SuclCHAR         = True
+      (==)  SuclREAL          SuclREAL         = True
+      (==)  SuclBOOL          SuclBOOL         = True
+      (==)  SuclDYNAMIC       SuclDYNAMIC      = True
+      (==)  SuclFILE          SuclFILE         = True
+      (==)  SuclWORLD         SuclWORLD        = True
+      (==)  _                 _                = False
+
+instance == SuclTypeVariable
+where (==) (SuclANONYMOUS i1) (SuclANONYMOUS i2) = i1 == i2
+      (==) (SuclNAMED     p1) (SuclNAMED     p2) = p1 == p2
+      (==) _                  _                  = False
+
 instance == SuclSymbol
-where (==) (SuclUser  sptr1)  (SuclUser  sptr2)  = sptr1 == sptr2
+where (==) (SuclUser  id1  )  (SuclUser  id2  )  = id1   == id2
       (==) (SuclCase  eptr1)  (SuclCase  eptr2)  = eptr1 == eptr2
       (==) (SuclApply int1 )  (SuclApply int2 )  = int1  == int2
       (==) (SuclInt   int1 )  (SuclInt   int2 )  = int1  == int2
@@ -78,6 +99,7 @@ coretyperule (SuclApply argc)
                (restype,emptygraph)
                (outfunctype,updategraph outfunctype (SuclFN (argc-1),argtypes++[restype]) emptygraph)
 coretyperule (SuclInt _) = consttyperule SuclINT
+coretyperule (SuclChar _) = consttyperule SuclCHAR
 coretyperule (SuclReal _) = consttyperule SuclREAL
 coretyperule (SuclBool _) = consttyperule SuclBOOL
 coretyperule (SuclUser _) = abort "coreclean: coretyperule: untyped user symbol"
@@ -86,3 +108,15 @@ coretyperule (SuclCase _) = abort "coreclean: coretyperule: untyped case symbol"
 consttyperule tsym
  = mkrule [] root (updategraph root (tsym,[]) emptygraph)
    where root = SuclANONYMOUS 0
+
+corecomplete :: SuclTypeSymbol -> [SuclSymbol] -> Bool
+
+corecomplete (SuclUSER tsid) = const False  // Must be an abstype...
+corecomplete (SuclFN arity) = const False
+corecomplete SuclINT = const False
+corecomplete SuclCHAR = superset (map (SuclChar o toChar) [0..255]) // 256 alternatives... doubtful is this is useful, but hey...
+corecomplete SuclREAL = const False
+corecomplete SuclBOOL = superset (map SuclBool [False,True])
+corecomplete SuclDYNAMIC = const False
+corecomplete SuclFILE = const False
+corecomplete SuclWORLD = const False

sucl/history.icl

@@ -2,7 +2,6 @@ implementation module history
 
 // $Id$
 
-import spine
 import rule
 import graph
 import pfun

sucl/law.icl

@@ -6,8 +6,8 @@ import coreclean
 import strat
 import spine
 import rule
-import graph
 import dnc
+import graph
 import basic
 import StdEnv
 

sucl/loop.dcl

@@ -3,18 +3,18 @@ definition module loop
 // $Id$
 
 from strat import Strategy
-from spine import Answer
 from trace import Trace
+from spine import Answer
 from history import HistoryAssociation,HistoryPattern
 from rule import Rgraph,Rule
 from graph import Graph
 from StdOverloaded import ==
 
 from strat import Substrategy,Subspine   // for Strategy
+from trace import History,Transformation // for Trace
+from spine import Spine                  // for Answer
 from graph import Node                   // for Strategy
 from basic import Optional               // for Answer
-from spine import Spine                  // for Answer
-from trace import History,Transformation // for Trace
 
 loop
  :: (((Graph sym pvar) pvar var -> ub:Bool) -> Strategy sym var pvar (Answer sym var pvar))

sucl/loop.icl

@@ -2,10 +2,10 @@ implementation module loop
 
 // $Id$
 
-import trace
 import strat
-import history
+import trace
 import spine
+import history
 import rewr
 import rule
 import graph
@@ -245,7 +245,9 @@ loop strategy matchable (initheap,rule)
         sargs = arguments rule; initsroot = ruleroot rule; initsubject = rulegraph rule
 
 listselect :: [.Bool] [.elem] -> [.elem]
-listselect _ _ = undef
+listselect [True:bs] [x:xs] = [x:listselect bs xs]
+listselect [False:bs] [x:xs] = listselect bs xs
+listselect _ _ = []
 
 initrule
  :: ![var]

sucl/newfold.dcl

 definition module newfold
+
+// $Id$
+
+from trace import Trace,Transformation
+from spine import Answer,Spine,Subspine
+from history import History,HistoryAssociation,HistoryPattern
+from rule import Rgraph,Rule
+from general import Optional
+
+:: Etracer sym var pvar :==
+       (Trace sym var pvar)
+       (Rgraph sym var)
+       Bool
+    -> Bool
+
+fullfold ::
+    (Etracer sym var pvar)
+    ((Rgraph sym var)->(sym,[var]))
+    sym
+    (Trace sym var pvar)
+ -> ([Bool],[Rule sym var],[Rgraph sym var])

sucl/newfold.icl

@@ -2,6 +2,10 @@ implementation module newfold
 
 // $Id$
 
+import trace
+import rule
+import StdEnv
+
 /*
 
 newfold.lit - New folding function
@@ -86,8 +90,25 @@ occurs within any subtrace.
 >|| =   mapfst3 only (extract trc foldarea trace ([],[],[])), otherwise
 >   =   newextract trc foldarea trace, otherwise
 >       where (recursive,recurseresult) = recurse foldarea fnsymbol trace
+*/
+
+fullfold ::
+    (Etracer sym var pvar)
+    ((Rgraph sym var)->(sym,[var]))
+    sym
+    (Trace sym var pvar)
+ -> ([Bool],[Rule sym var],[Rgraph sym var])
+
+fullfold trc foldarea fnsymbol trace
+| recursive
+  = recurseresult
+= newextract trc foldarea trace
+  where (recursive,recurseresult) = recurse foldarea fnsymbol trace
 
+recurse = undef
+newextract = undef
 
+/*
 `Recurse foldarea fnsymbol trace' is a pair `(recursive,recurseresult)'.
 `Recurseresult'  is  the derived function definition (strictness, rules,
 and new areas), obtained by folding the trace.  `Recurse' tries to  fold
@@ -193,7 +214,15 @@ in the supertrace.
 >       rgraph * ** ->
 >       bool ->
 >       bool
+*/
 
+:: Etracer sym var pvar :==
+       (Trace sym var pvar)
+       (Rgraph sym var)
+       Bool
+    -> Bool
+
+/*
 >   extract
 >   ::  etracer * ** *** ->
 >       (rgraph * **->(*,[**])) ->

sucl/newtest.dcl

 definition module newtest
+
+// $Id$
+
+from cli import Cli
+from coreclean import SuclTypeSymbol,SuclTypeVariable,SuclSymbol,SuclVariable
+from trace import Trace,Transformation
+from spine import Answer,Spine,Subspine
+from history import History,HistoryAssociation,HistoryPattern
+from rule import Rgraph,Rule
+from general import Optional
+
+:: Symredresult sym var tsym tvar
+   :== ( Rgraph sym var    // The initial area in canonical form
+       , sym               // The assigned symbol
+       , [Bool]            // Strictness annotations
+       , Rule tsym tvar    // Type rule
+       , Trace sym var var // Truncated and folded trace
+       , [Rule sym var]    // Resulting rewrite rules
+       , [Rgraph sym var]  // New areas for further symbolic reduction (not necessarily canonical)
+       )
+
+fullsymred ::
+    [SuclSymbol]    // Fresh function symbols
+    Cli             // Module to optimise
+ -> [Symredresult SuclSymbol SuclVariable SuclTypeSymbol SuclTypeVariable]

sucl/newtest.icl

@@ -4,6 +4,13 @@ implementation module newtest
 
 import cli
 import coreclean
+import newfold
+import complete
+import trd
+import loop
+import trace
+import rule
+import graph
 import canon
 import basic
 import StdEnv
@@ -138,7 +145,19 @@ these tuples.
 >           [rule * **],      ||  Resulting rewrite rules
 >           [rgraph * **]     ||  New areas for further symbolic reduction (not necessarily canonical)
 >       )
+*/
+
+:: Symredresult sym var tsym tvar
+   :== ( Rgraph sym var    // The initial area in canonical form
+       , sym               // The assigned symbol
+       , [Bool]            // Strictness annotations
+       , Rule tsym tvar    // Type rule
+       , Trace sym var var // Truncated and folded trace
+       , [Rule sym var]    // Resulting rewrite rules
+       , [Rgraph sym var]  // New areas for further symbolic reduction (not necessarily canonical)
+       )
 
+/*
 >   listopt :: [char] -> [[char]] -> [char]
 
 >   listopt main = listnew main.loadclis
@@ -253,7 +272,7 @@ these tuples.
 fullsymred ::
     [SuclSymbol]    // Fresh function symbols
     Cli             // Module to optimise
- -> [Symredresult symbol node typesymbol typenode]
+ -> [Symredresult SuclSymbol SuclVariable SuclTypeSymbol SuclTypeVariable]
 
 fullsymred freshsymbols cli
  = results
@@ -265,11 +284,6 @@ fullsymred freshsymbols cli
          labelarea` = labelarea (map getinit results) freshsymbols
          canonise` = canonise (typerule cli) suclheap
 
-initareas = undef
-getareas = undef
-symredarea = undef
-getinit = undef
-
 /*
 `Initareas cli' is the list  of  initial  rooted  graphs  that  must  be
 symbolically  reduced.  An initial rooted graph is formed by applying an
@@ -290,7 +304,23 @@ its type rule.
 
 >   getareas :: symredresult * ** **** ***** -> [rgraph * **]
 >   getareas (area,symbol,stricts,trule,trace,rules,areas) = areas
+*/
+
+initareas :: Cli -> [Rgraph SuclSymbol SuclVariable]
+initareas cli
+= map (initialise suclheap) (exports cli)
+  where initialise [root:nodes] symbol
+        = mkrgraph root (updategraph root (symbol,args) emptygraph)
+          where args = map2 const nodes targs
+                targs = arguments (typerule cli symbol)
 
+getinit :: (Symredresult sym var tsym tvar) -> Rgraph sym var
+getinit (area,symbol,stricts,trule,trace,rules,areas) = area
+
+getareas :: (Symredresult sym var tsym tvar) -> [Rgraph sym var]
+getareas (area,symbol,stricts,trule,trace,rules,areas) = areas
+
+/*
 `Symredarea' is the function that does symbolic reduction  of  a  single
 area.
 
@@ -311,13 +341,38 @@ area.
 >             complete' = (~).converse matchable' (mkrgraph () emptygraph)
 >             matchable' = matchable (complete cli)
 >             strategy' = clistrategy cli
+*/
+
+:: Unit = Unit
+
+symredarea ::
+    ((Rgraph SuclSymbol SuclVariable)->(SuclSymbol,[SuclVariable]))
+    Cli
+    (Rgraph SuclSymbol SuclVariable)
+ -> Symredresult SuclSymbol SuclVariable SuclTypeSymbol SuclTypeVariable
+
+symredarea foldarea cli area
+= (area,symbol,stricts,trule,trace,rules,areas)
+  where agraph = rgraphgraph area; aroot = rgraphroot area
+        (symbol,aargs) = foldarea area
+        arule = mkrule aargs aroot agraph
+        trule = ruletype sucltypeheap (ctyperule SuclFN sucltypeheap (typerule cli)) arule
+        trace = loop strategy` matchable` (removeMembers suclheap (varlist agraph [aroot]),arule)
+        (stricts,rules,areas) = fullfold (trc symbol) foldarea symbol trace
+        matchable` = matchable (complete cli)
+        strategy` = clistrategy cli
 
+/*
 >   trc :: symbol -> trace symbol node node -> rgraph symbol node -> bool -> bool
 
 >   trc symbol trace area recursive
 >   =   error (lay ("Trace is recursive in area":printrgraph showsymbol shownode area:printtrace symbol showsymbol shownode shownode trace)), if esymbol symbol & recursive
 >   =   recursive, otherwise
+*/
+
+trc symbol trace area recursive = recursive
 
+/*
 >   esymbol (User m "E") = True
 >   esymbol symbol = False
 
@@ -403,7 +458,20 @@ area.
 
 >   matchable complete patterns rgraph
 >   =   ~coveredby complete (rgraphgraph rgraph) [(rgraphgraph pattern,[rgraphroot pattern])|pattern<-patterns] [rgraphroot rgraph]
+*/
+
+matchable ::
+    ([sym]->Bool)
+    [Rgraph sym pvar]
+    (Rgraph sym var)
+ -> Bool
+ |  == sym
+ &  == var
+ &  == pvar
+matchable complete patterns rgraph
+= not (coveredby complete (rgraphgraph rgraph) [(rgraphgraph pattern,[rgraphroot pattern]) \\ pattern<-patterns] [rgraphroot rgraph])
 
+/*
 ------------------------------------------------------------------------
 
 `Ctyperule' cli (sym,args)' is the typerule of an occurrence  of  symbol
@@ -424,7 +492,25 @@ sym with the given arguments, curried if there are too few.
 >             (troot',tgraph',theap') = foldr build (troot,tgraph,typeheap--nodelist tgraph (troot:targs)) targs''
 >             build targ (troot,tgraph,tnode:tnodes)
 >             =   (tnode,updategraph tnode (fn,[targ,troot]) tgraph,tnodes)
+*/
 
->   newsymbols main = map (User main.("New_"++)) identifiers
+ctyperule ::
+    (Int -> tsym)           // The arrow type symbol for functions of given arity
+    [tvar]                  // Fresh type variables
+    (sym->Rule tsym tvar)   // Type rule of a symbol
+    (sym,[var])             // Node to abstract
+ -> Rule tsym tvar
+ |  == tvar
+
+ctyperule fn typeheap typerule (sym,args)
+= mkrule targs` troot` tgraph`
+  where targs = arguments trule; troot = ruleroot trule; tgraph = rulegraph trule
+        trule = typerule sym
+        (targs`,targs``) = claim args targs
+        (troot`,tgraph`,_) = foldr build (troot,tgraph,removeMembers typeheap (varlist tgraph [troot:targs])) targs``
+        build targ (troot,tgraph,[tnode:tnodes])
+        = (tnode,updategraph tnode (fn 1,[targ,troot]) tgraph,tnodes)
 
+/*
+>   newsymbols main = map (User main.("New_"++)) identifiers
 */

sucl/strat.dcl

@@ -2,8 +2,8 @@ definition module strat
 
 // $Id$
 
-from history import History
 from spine import Answer
+from history import History
 from rule import Rule
 from graph import Graph,Node
 from StdOverloaded import ==

sucl/strat.icl

@@ -2,10 +2,10 @@ implementation module strat
 
 // $Id$
 
-import history
 import spine
-import dnc
+import history