computeLib.unmapped

STRUCTURE

SYNOPSIS

List unmapped elements in compset

LIBRARY

compute

DESCRIPTION

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

EVAL, listItems