Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-06-01 00:47:49 -0700 (Sun, 01 Jun 2003)
Revision: 4635
Log message:

      - Bug clean-up of the Refine module: removed a lot of stuff from the
      interface - internal stuff that "outside world" has no business having access to.
      
      - Cleaned up capitalized/uncapitalized mess with module names. We has some
      places store and use capitalized module names and some would have uncapitalized
      ones, and it was becoming increazingly hard to keep things consistent. I switched it
      to using uncapitalized names _everywhere_, except for opnames and a small number of
      UI features (error messages, "extends" directives and mptop's Module.name
      fully-qualified variables).
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-06-01 21:08:23 -0700 (Sun, 01 Jun 2003)
Revision: 4636
Log message:

      Added a conversion from the "high-level" (filter/boot directory) proof
      representation into the "low-level" (Refiner.Refiner.Refine.extract) one.
      "check" and "check_all" top-loop operations will do the conversion.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-06-04 03:05:41 -0700 (Wed, 04 Jun 2003)
Revision: 4641
Log message:

      - Added a call-back interface to allow refiner to get ahold of the proof tree
      of a derived rule being used.
      - Fixed a number of bugs in Refine.term_of_extract (a few still remain,
      missing safety checks mostly - some explicitly marked in comments).
      - Added (temporarily, as I am hoping to implement a better API later) a function
      term_of_extract to MP toploop - it will return the proof extract, given
      extracts for rule assumptions.
      
      Still remaining: restore the disabled code that allows refiner to call rewriter
      with proper arguments when constructing the extract.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-06-04 03:48:37 -0700 (Wed, 04 Jun 2003)
Revision: 4642
Log message:

      Include the module name in error messages, not just the item name.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-06-04 07:41:18 -0700 (Wed, 04 Jun 2003)
Revision: 4643
Log message:

      - Fixed a few extracts on primitive rules.
      - One of the prim rules in itt_subtype can be derived.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-06-04 08:03:38 -0700 (Wed, 04 Jun 2003)
Revision: 4644
Log message:

      Simplified the [un]zip_mimplies interface.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-06-04 11:04:48 -0700 (Wed, 04 Jun 2003)
Revision: 4645
Log message:

      The bvar list in rewriter was being built in reverse order, have no idea why. Fixed.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-06-04 11:29:22 -0700 (Wed, 04 Jun 2003)
Revision: 4646
Log message:

      A number of extract fixes.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-06-04 13:56:02 -0700 (Wed, 04 Jun 2003)
Revision: 4647
Log message:

      Term extraction from proofs finally works!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!
      
      The current implementation is full of holes (basically, a lot of safety
      checks still need to be added - I believe most of these places are
      at least commented with a TODO now), but it's a start.
      
      To access the extracts from toploop, call the (temporarily added) term_of_extract
      function. It takes a list of terms that act as extracts for assumptions (the
      conclusion part of the sequent only) and outputs the extract for the goal
      (full sequent).
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-06-10 17:41:09 -0700 (Tue, 10 Jun 2003)
Revision: 4655
Log message:

      Minor updates to m-paper headers.
      
      Note: in the ICFP's ACM style (9pt, two column), the paper is 12-13 paper long
      (the limit is 15), but with any "honest" style (e.g., article) it's 25 or more...
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-06-11 17:07:46 -0700 (Wed, 11 Jun 2003)
Revision: 4658
Log message:

      Adding a capital lambda.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-06-11 17:29:12 -0700 (Wed, 11 Jun 2003)
Revision: 4659
Log message:

      Added Omega
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-06-12 19:33:45 -0700 (Thu, 12 Jun 2003)
Revision: 4661
Log message:

      Switching to dvipdfm and forcing the letter paper size.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2003-06-16 14:51:51 -0700 (Mon, 16 Jun 2003)
Revision: 4663
Log message:

      Some minor changes to the paper.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-06-16 17:00:18 -0700 (Mon, 16 Jun 2003)
Revision: 4664
Log message:

      New M-paper title.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-06-16 20:22:06 -0700 (Mon, 16 Jun 2003)
Revision: 4666
Log message:

      Changed the display for subscripting/assignment to use e.[e] instead of just e[e]
      (to avoid confusion with SO substitution).
      
      We really should have used display forms, not typing these things by hand...
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-06-16 21:09:44 -0700 (Mon, 16 Jun 2003)
Revision: 4667
Log message:

      Addressed a few comments by the first reviewer. I think I am close to being
      ready to submit...
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-06-16 21:26:48 -0700 (Mon, 16 Jun 2003)
Revision: 4668
Log message:

      Version to be submitted to MERLIN.
      

Changes by: ( at unknown.email)
Date: 2003-06-16 21:26:48 -0700 (Mon, 16 Jun 2003)
Revision: 4669
Log message:

      This commit was manufactured by cvs2svn to create tag
      'M_PAPER_MERLIN_2003_SUBMISSION'.

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-06-17 19:58:16 -0700 (Tue, 17 Jun 2003)
Revision: 4671
Log message:

      Added (during the last CS101 lecture) a "smallest_element" theorem
      that establishes an existence of the smallest element in any list.
      This can be used to demo the extractor (once it actually works).
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-06-18 15:37:06 -0700 (Wed, 18 Jun 2003)
Revision: 4672
Log message:

      Typeinf types no longer need to be in tactic_boot_sig
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2003-06-18 17:22:31 -0700 (Wed, 18 Jun 2003)
Revision: 4673
Log message:

      Added a "simple" type inference resource.
      This is supposed to be a strict type inference algorithm,
      for languages where type inference is well-defined,
      for example in ML-like languages.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-06-19 17:27:08 -0700 (Thu, 19 Jun 2003)
Revision: 4675
Log message:

      Fixing display form for the ML rewrites.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-06-20 00:39:40 -0700 (Fri, 20 Jun 2003)
Revision: 4676
Log message:

      Adding a version number to cmiz/cmoz/prla/prlb files.
      
      Before this change we had a magic number that was responsible for making sure that
      the file has format we expect it to have and that it has a compatible version
      of the format. Now there is a separate magic number responsible for the format
      (which is not supposed to change, unless we add/remove formats) and the version number
      that is supposed to change whenever the format
      (or underlying data structures/data representation) changes.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-06-20 23:54:53 -0700 (Fri, 20 Jun 2003)
Revision: 4677
Log message:

      Sequent args in the tests directory were outdated.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-06-21 20:56:15 -0700 (Sat, 21 Jun 2003)
Revision: 4678
Log message:

      In filter, I implemented exdplicit PRL bindings, so that embedding of terms and
      opnames into expressions is explicit on the summary level (and only
      degenerates to things like term_of_string internally in Filter_prog).
      
      Still TODO: update display forms accordingly (should be really easy, actually!)
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-06-24 06:50:21 -0700 (Tue, 24 Jun 2003)
Revision: 4681
Log message:

      Display forms for the new PRL bindings.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-06-24 14:29:21 -0700 (Tue, 24 Jun 2003)
Revision: 4682
Log message:

      Automatically remove all .prlb on "realclean".
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2003-06-24 16:45:21 -0700 (Tue, 24 Jun 2003)
Revision: 4683
Log message:

      Minor omake changes.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2003-06-24 17:04:51 -0700 (Tue, 24 Jun 2003)
Revision: 4684
Log message:

      Decided to commit the extraction-disabling code, until we get it working.
      To find it, look in refiner.ml for the string
      "JYH: extraction disabled for now".
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-06-25 09:12:21 -0700 (Wed, 25 Jun 2003)
Revision: 4685
Log message:

      Moved all the term/mterm "of_string" calls into one big "of_string" unmarshalling
      at the beginning of each PRL-compiled module. This:
      - reduces the size of the mp.opt binary (THEORIES=all) by 1.8Mb (12%) as the
      duplicated subterms are now only represented once per module instead of multiple times.
      - reduces the mp.opt statup time by about 15%
      - probably reduces the compilation time (not measures)
      - does not seem to affect the "status_all" time.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2003-06-25 15:59:56 -0700 (Wed, 25 Jun 2003)
Revision: 4686
Log message:

      In addition to marshaling terms and meta_terms in Aleksey's last
      update, also marshal opnames and nums.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2003-06-25 17:07:56 -0700 (Wed, 25 Jun 2003)
Revision: 4687
Log message:

      Added nums to the "binding" mechanism defined in Filter_util.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-06-26 10:53:54 -0700 (Thu, 26 Jun 2003)
Revision: 4688
Log message:

      Deleting some code that was added during a recent attempt to make the extraction work.
      That code (allowing more than one mention of the same seq. condext among redexes)
      was incomplete, not quite valid and not the right way to go anyway.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2003-06-26 15:47:34 -0700 (Thu, 26 Jun 2003)
Revision: 4689
Log message:

      Added initial internal support for term patterns.  It turns out
      the previous method I suggested does not work because CamlP4
      does not have "when" patterns.
      
      Instead, we'll have to extend the grammar with a full
      match expression.  This is the syntax I envision:
      
      matchterm t with
         << ... >> -> e1
       | << ... >> -> e2
       ...
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2003-06-30 11:15:39 -0700 (Mon, 30 Jun 2003)
Revision: 4690
Log message:

      Initial implementation of pattern matching.
      This uses a new parameter type "match_param", which
      gives a simplified representation of parameters that
      requires no "when" clauses during pattern matching.