defs-program, pretty-program: add informative error messages for failures

git-svn-id: http://acl2-books.googlecode.com/svn/trunk@2983 303c5b2c-9740-0410-b014-fd8f9db7be32
defsort: add option to generate a proof that the mergesort is equivalent to an insertion sort

git-svn-id: http://acl2-books.googlecode.com/svn/trunk@2984 303c5b2c-9740-0410-b014-fd8f9db7be32
defsort: allow extra arguments, e.g. to parameterize the sort

git-svn-id: http://acl2-books.googlecode.com/svn/trunk@2985 303c5b2c-9740-0410-b014-fd8f9db7be32
add better error messages for xdoc/str

git-svn-id: http://acl2-books.googlecode.com/svn/trunk@2986 303c5b2c-9740-0410-b014-fd8f9db7be32
add missing files

git-svn-id: http://acl2-books.googlecode.com/svn/trunk@2987 303c5b2c-9740-0410-b014-fd8f9db7be32
defsort bugfix

git-svn-id: http://acl2-books.googlecode.com/svn/trunk@2988 303c5b2c-9740-0410-b014-fd8f9db7be32
another defsort fix. probably all ok now

git-svn-id: http://acl2-books.googlecode.com/svn/trunk@2989 303c5b2c-9740-0410-b014-fd8f9db7be32
VL parser updates

 - VL's parsing functions now pass around a new "parse state" object instead of
   a list of warnings.  The list of warnings are moved into this structure.
   The structure also tracks the names of user-defined data types.  This
   appears to be necessary to resolve an ambiguity between datatypes and
   expressions, i.e.,: is foo_t the name of a wire or a type?

   This is a rather rough feature that doesn't properly account for scoping.
   In the future we may want to extend it to support shadowing type names, etc.

 - VL now supports additional parts of SystemVerilog's port declaration
   syntax, e.g., things like "input logic [3:0] foo" are now supported.
   This is currently overly permissive.

 - Added various tests of the new port handling.

git-svn-id: http://acl2-books.googlecode.com/svn/trunk@2990 303c5b2c-9740-0410-b014-fd8f9db7be32