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