1\DOC unmapped
2
3\TYPE {unmapped : compset -> (string * string) list}
4
5\SYNOPSIS
6List unmapped elements in compset
7
8\KEYWORDS
9evaluation.
10
11\LIBRARY
12compute
13
14\DESCRIBE
15The function {unmapped} takes a {compset} value and returns a
16listing of the elements of the compset that have no transformation 
17attached to them. 
18
19\EXAMPLE
20The listing omits constructors, but can include constants
21that effectively act as constructors for rewrites in the compset. 
22{
23   > val compset = reduceLib.num_compset();
24   val compset = <compset>: computeLib.compset
25
26   > computeLib.unmapped compset;
27   val it =
28     [("BIT1", "arithmetic"), 
29      ("BIT2", "arithmetic"),
30      ("ZERO", "arithmetic")]
31     : (string * string) list
32}
33
34\EXAMPLE
35In the following example, a function is added to a compset without 
36also adding functions that get "called" by it:
37{
38   > load "sortingTheory";
39   val it = (): unit
40
41  > sortingTheory.QSORT_DEF;
42  val it =
43     |- (!ord. QSORT ord [] = []) /\
44        !t ord h.
45          QSORT ord (h::t) =
46           (let (l1,l2) = PARTITION (\y. ord y h) t
47           in
48           QSORT ord l1 ++ [h] ++ QSORT ord l2) : thm
49
50   > val () = computeLib.add_thms [sortingTheory.QSORT_DEF] compset;
51
52   > computeLib.unmapped compset;
53   val it =
54      [("APPEND", "list"), 
55       ("BIT1", "arithmetic"), 
56       ("BIT2", "arithmetic"),
57       ("PARTITION", "sorting"), 
58       ("UNCURRY", "pair"), 
59       ("ZERO", "arithmetic")]
60   :(string * string) list
61}
62
63\COMMENTS
64Intended to support the construction of large compsets, where it is often
65unclear what functions and conversions still need to be added in order to 
66make applications of {EVAL_CONV} terminate.
67
68\FAILURE
69Never fails.
70
71\SEEALSO
72bossLib.EVAL, computeLib.listItems.
73
74\ENDDOC
75