\DOC unmapped

\TYPE {unmapped : compset -> (string * string) list}

\SYNOPSIS
List unmapped elements in compset

\KEYWORDS
evaluation.

\LIBRARY
compute

\DESCRIBE
The function {unmapped} takes a {compset} value and returns a
listing of the elements of the compset that have no transformation 
attached to them. 

\EXAMPLE
The listing omits constructors, but can include constants
that effectively act as constructors for rewrites in the compset. 
{
   > val compset = reduceLib.num_compset();
   val compset = <compset>: computeLib.compset

   > computeLib.unmapped compset;
   val it =
     [("BIT1", "arithmetic"), 
      ("BIT2", "arithmetic"),
      ("ZERO", "arithmetic")]
     : (string * string) list
}

\EXAMPLE
In the following example, a function is added to a compset without 
also adding functions that get "called" by it:
{
   > load "sortingTheory";
   val it = (): unit

  > sortingTheory.QSORT_DEF;
  val it =
     |- (!ord. QSORT ord [] = []) /\
        !t ord h.
          QSORT ord (h::t) =
           (let (l1,l2) = PARTITION (\y. ord y h) t
           in
           QSORT ord l1 ++ [h] ++ QSORT ord l2) : thm

   > val () = computeLib.add_thms [sortingTheory.QSORT_DEF] compset;

   > computeLib.unmapped compset;
   val it =
      [("APPEND", "list"), 
       ("BIT1", "arithmetic"), 
       ("BIT2", "arithmetic"),
       ("PARTITION", "sorting"), 
       ("UNCURRY", "pair"), 
       ("ZERO", "arithmetic")]
   :(string * string) list
}

\COMMENTS
Intended to support the construction of large compsets, where it is often
unclear what functions and conversions still need to be added in order to 
make applications of {EVAL_CONV} terminate.

\FAILURE
Never fails.

\SEEALSO
bossLib.EVAL, computeLib.listItems.

\ENDDOC