- defdata-testing has been replaced by defdata-attach.  defdata-attach
  is a more general utility that can be used to change/add type
  metadata associated with each type stored via register-type and
  defdata in the table type-metadata-table.

- defdata moved from cgen to a separate directory to reflect its more
  independent status. Although cgen currently still is tightly coupled
  with defdata, especially the type-metadata table, enumerators
  support and random-state library. Cgen now has its own package.

- defdata has been (almost) completely rewritten with an eye towards
  easy debuggability and extensibility. It is now a truely a framework
  and not a library. There is a slightly outdated design essay at the
  bottom of defdata-core.lisp

- The core defdata language is implemented in defdata-core.lisp and
  builtin-combinators.lisp.  defdata-core contains the parsing code,
  the top-level defdata-events generating function and predicate
  events generating functions. The rest of the defdata framework is
  implemented using plugins (pre/post hooks). This plugin
  functionality is implemented using defdata-defaults-table and using
  funcalls (ev-fncall-w).

- Currently the sugar on top of core defdata language is added via
  register-combinator macro defined in its own file. The files listof,
  alistof, map, and record use this macro to implement their
  respective functionality (especially theory events).

- Records (and maps) theory has been made much faster, by
  orchestrating the enabling/disabling of rules and turning off the
  rewrite rule-class of certain rules. (I used accumulated-persistence
  to debug slow proofs). This makes a huge difference. Earlier the
  more the records, the slower the defdata became, taking as much as
  30-40 seconds. Maps were taking even longer.

- Enumerator generation has its own file and it is possible for users
  to use defdata without enumerators, but currently this is not
  allowed via an invariant in register-type. register-type requires
  the enumerator to be given. But in the future it should be possible
  to generate the enumerator on the fly given just the predicate
  definition. (This way we can add enumerator support to
  std::defenum/defaggregate/etc easily).

- tau-characterization and polymorphic signatures are implemented in
  their own files and connect to defdata via hook functions.

- Tau characterization implemented. Basically this provides the
  following guarantee. If TAU was complete over the type reasoning
  theory, then adding a type to the current theory via defdata
  maintains this completeness. We also add other rule-classes for
  helping the simplification engine too.

- Parametric Polymorphism simulated using macro sig and defdata. We
  (try to) provide the following invariants:
  1. Every new defdata type is instantiated for every polymorphic
     signature (specified via sig) that matches (one of its argument
     types).
  2. Every new polymorphic signature is appropriately instantiated for
     all defdata types in the current world.

- top.lisp brings (core defdata) base and the rest of the (fancy
  sugar) functionality together.

- Added allp (the TOP type) alias support. Allp aka the Top type in
  the defdata types is handled specially, since TAU does not play well
  with everywhere-true and everywhere-false (and more generally with
  predicates that hide equality-to-constants). Allp aliases are
  tracked in the table called allp-aliases.

- Comment on dest-elim support in record.lisp: We use override-hints
   and computed hints to do the following at
   stable-under-simplification. Enable the rules that rewrite
   (mget :field x) to (record-name-field x) destructor calls.  Disable
   the destructor functions. We then expect dest-elim to fire in the
   following waterfall round(s). But things are slightly more tricky
   for nested dest-elim: One needs to take transitive closure of all
   constituent type relation and take that into account to do a
   sequence of nested dest-elims all in one dest-elim iteration.

- Map implementation changed to allow msetting of nil values.  This
  affects base.lisp and map lemmas. An additional lemma added to map
  theory at Mitesh's request.  It says the type is preserved if an
  entry is deleted in a map.

- Heuristic changes in nth-all and other enumerators, tweaking the
  test data distribution for these standard enumerators.

- Added dependent type hypotheses support to sig (polymorphic
  signatures).

- Added defxdoc for defdata, register-type, register-data-constructor
  and sig.
Cgen has been refactored to be usable as an API. In particular, a new
function prove/cgen has been implemented which provides programmatic
access to Cgen (even from non-event contexts). The following are the
major highlights of this refactoring:

- test? has been rewritten using the API function prove/cgen and thus
  provides an example to anyone wishing to use Cgen programmatically.

- The code has been now spread across separate files. Cgen-search.lisp
  contains the heart of the cgen/testing driver code. callback.lisp
  implements the test-checkpoint callback function used in the
  override+backtrack hints (observer-style hints). The main Cgen API
  function prove/cgen is in the file that is named after it; it also
  contains the printing stuff. test? has been moved to top.lisp.
  build-enumcalls.lisp contains the code that builds enumerator call
  expressions and generates the defun, next-sigma, that when called,
  generates the next \sigma (test assignment) to be used in testing.
  Type inference related functions have been moved to type.lisp.

- The prove/cgen API function, explicitly takes a context, called
  cgen-state and gets back the modified cgen-state with the relevant
  result/data/statistics recorded. The cgen-state data-structure is an
  alist that collects the previous data-structures gcs% and s-hist and
  also other data of interest, like the acl2s defaults, the
  stopping-condition, processor-hist, and couple of other fields which
  resided in gcs% but were not really 'global coverage statistics'.  I
  have not documented this data-structure separately, but anybody who
  wants to deconstruct cgen-state should look at the function
  print-testing-summary-fn which prints the information stored in
  cgen-state.

- In prove/cgen, as opposed to before, we call prove directly instead
  of thm (which is an event); this gives us slightly more control,
  since we dont have to go through the event pre/post functions.

- Change in initialize-event-user and finalize-event-user functions:
  earlier we supposedly had some nested testing support via cgen-stack
  which stored the current globals gcs% and s-hist in the top of the
  stack -- this code has been thrown/removed. What we now have is a
  global cgen-state which stores the current cgen/testing's state and
  is used to communicate across callbacks (test-checkpoint). But there
  is still a stack called event-stack which stores the ctx of the
  event under consideration. This stack is used to recognize a
  thm/defthm to be tested -- the matching finalize then calls
  print-testing-summary-fn under appropriate conditions. All other
  events are ignored (the ctx :ignore-cgen is added).

  Here are other changes to Cgen:

- Threw away dest-elim Cgen hack (elim.lisp deleted) for records and
  maps, to using computed override-hints and rule-sets that invert the
  implementation of destructors back to dest calls. See comment in
  defdata/records.lisp

- Added a new parameter, print-cgen-summary that can be turned on or
  off using acl2-defaults macro. Also the main printing function
  print-testing-summary is now defattachable.

- The trans-eval in simple-search runs in 'guard-checking :none'. This
  ensures that all eval runs in the logic, precluding the possibility
  of raw lisp errors during testing. Unfortunately, this also makes
  Cgen/testing twice as slow.

- Shifted with-timeout wrapper from outside cgen-search-fn to inside
  it wrapping the run-tests call, so that it does not escape the
  trans-eval make-event call in simple-search. This is important to
  maintain a sane cgen::event-stack and fixes some bugs arising in
  behaviors with interrupts and timeouts.

- Replaced subgoal-timeout by cgen-timeout in acl2s parameters.

- IMP: Found recently a problem with globals that keep track of
  possibly nested calls to test-checkpoint and cgen. If we abort using
  Ctrl-C interrupt, or say one was using :brr t and there was a break,
  there is no guarantee that these Cgen globals are safe/well-formed.
  To take care of interrupts and breaks, we need to flush the globals
  event-stack and cgen-state to a safe state; this can be done by
  calling (cgen::flush). See :doc cgen::flush

- IMP Design Change: DEFUN event context has now been removed from
  contexts that Cgen/testing works. CCG manually calls prove via
  prove-no-er. This bungles up the event-stack discipline used by Cgen
  to keep track of nested events.

- added defxdoc for cgen, test?, cgen::flush and prove/cgen

- Cgen now prints evalable counterexamples/witnesses (that can be
  copied into a let* bindings)

- Tuned debugging (printing/verbosity-level) support.

- Added a call to genrandom-seed to get a new seed at TIMEOUTs (this
  serves to provide some progress in random seed generation and not
  get stuck with the same sequence of random seeds)

- Removed make-event from inside the trans-eval call in the driver
  code of simple-search (cgen-search.lisp). This was motivated by
  making prove/cgen usable from non-event contexts. Unfortunately, we
  need to do redefine some temp functions, but then we already use
  ttags, so we can drop in a (set-ld-redefinition-action).

- While producing numbers for range types, use small numbers as is the
  norm in nth-all and other numbers in base.lisp -- in particular use
  nth-nat-testing instead of using the random natural seed directly.
  This really helps in avoiding complex timeouts and non-responsive
  behavior for factorial/exponential like functions.
Merge pull request #257 from harshrc/master

ACL2 Sedan changes (Cgen and Defdata)
Merge branch 'master' of https://github.com/ragerdl/acl2