Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2005-01-01 13:19:29 -0800 (Sat, 01 Jan 2005)
Revision: 6375
Log message:

      Replaced append with rev_append and map with rev_map where possible.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-01-03 11:37:16 -0800 (Mon, 03 Jan 2005)
Revision: 6376
Log message:

      Minor font adjustments.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-01-10 20:56:16 -0800 (Mon, 10 Jan 2005)
Revision: 6387
Log message:

      - Require OMake 0.9.4
      - (bug 118) use the generated include directory list on W32 as well.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-01-10 21:42:14 -0800 (Mon, 10 Jan 2005)
Revision: 6388
Log message:

      The .DEFAULT target now includes a "test-metaprl-startup" target which
      checks whether MetaPRL can start up successfully. This means that if somebody
      introduces a bug that is only visible at runtime, then a simple "omake"
      will detect it (making it less likely that the bug will be accidentally
      checked in).
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-01-11 19:11:30 -0800 (Tue, 11 Jan 2005)
Revision: 6389
Log message:

      Wow, finally commit those HOL files we did at TPHOLs.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-01-12 16:50:30 -0800 (Wed, 12 Jan 2005)
Revision: 6390
Log message:

      Minor "style" changes to a few of the "manual" intro resource enties.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-01-12 17:04:21 -0800 (Wed, 12 Jan 2005)
Revision: 6391
Log message:

      Minor code simplifcation
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-01-12 20:42:19 -0800 (Wed, 12 Jan 2005)
Revision: 6393
Log message:

      - This changes how dT interacts with autoT. Now every entry in the intro
        resource is marked with one of the auto_type values (AutoTrivial,
        AutoNormal, AutoComplete). In each stage of autoT only the corresponding
        entries will be used. When dT 0 is called outside of autoT, all the entries
        will be used.
      
      - The intro annotations on the rules w/o assumptions will now be added to
        AutoTrivial (instead of AutoNormal, as before) and will be attempted before
        the nth_hyp.
      
      - The annotation processors now return a _list_ of entries to be added to a
        resource instead of just a single entry. This is used, for example, to add
        a pair of an AutoNormal entry and an AutoComplete one when the
        "CondMustComplete" option is passed to an intro annotation.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-01-12 21:12:18 -0800 (Wed, 12 Jan 2005)
Revision: 6394
Log message:

      Imporved the display of sequents that is used in the absense of other dforms
      (as it is the case in the filter binaries). This should make error messages
      generated by the filter a bit nicer.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-01-12 21:18:42 -0800 (Wed, 12 Jan 2005)
Revision: 6395
Log message:

      Better indentation
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-01-12 22:39:21 -0800 (Wed, 12 Jan 2005)
Revision: 6396
Log message:

      - The term match table now supports sequent pattenrs that have a single
        context in the _middle_ of the hypothesis list (it used to be the case that
        it only supported a single context that is either at the end of the list or
        at the beginning, which caused confusing error messages - see bug 380).
      
      - Fixed the "omake check_status" rules.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-01-13 18:55:39 -0800 (Thu, 13 Jan 2005)
Revision: 6398
Log message:

      Fixing a typo
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-01-13 19:16:47 -0800 (Thu, 13 Jan 2005)
Revision: 6399
Log message:

      Add an "is_closed_term" function.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-01-13 20:02:25 -0800 (Thu, 13 Jan 2005)
Revision: 6401
Log message:

      Some fixes in the "omake check-status" rules
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-01-14 01:49:38 -0800 (Fri, 14 Jan 2005)
Revision: 6403
Log message:

      Bug 386 workaround for the "test-metaprl-startup" target
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-01-14 03:50:35 -0800 (Fri, 14 Jan 2005)
Revision: 6404
Log message:

      Fixed a few issues related to handling of generated files in OMakefiles
      (including a bug 387 workaround).
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-01-14 05:50:12 -0800 (Fri, 14 Jan 2005)
Revision: 6405
Log message:

      The addr type should be kept abstract in this interface.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-01-14 06:19:45 -0800 (Fri, 14 Jan 2005)
Revision: 6406
Log message:

      A small change in the addr type implementation.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-01-14 07:44:47 -0800 (Fri, 14 Jan 2005)
Revision: 6407
Log message:

      Moved a couple of "Perv" opname definitions into the Opname module
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-01-15 19:51:15 -0800 (Sat, 15 Jan 2005)
Revision: 6408
Log message:

      Added the conversion "findThenC test conv" that find the outermost
      subterms where test is true, and applies the conv.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-01-16 10:56:07 -0800 (Sun, 16 Jan 2005)
Revision: 6410
Log message:

      Trying to figure out the rewriter bug.
      This is just a code reformat as I try to understand the code.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-01-16 12:42:32 -0800 (Sun, 16 Jan 2005)
Revision: 6411
Log message:

      This addresses the problem with failed rewrites that
      include contexts.  The problem was the scope of the
      rewrite arguments.
      
      For example, in the following rule, the argument
      is intended to be interpreted as being
      within the sequent context.
      
         prim concl_subst TyEqual{'t1; 't2} :
            sequent { <H> >- TyEqual{'t1; 't2} } -->
            sequent { <H> >- 'e in 't2 } -->
            sequent { <H> >- 'e in 't1 }
      
      Rewrites are different--the args are intended to
      be closed.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-01-16 12:55:31 -0800 (Sun, 16 Jan 2005)
Revision: 6412
Log message:

      Forgot to remove the debugging print statements.
      

Changes by: ( at unknown.email)
Date: 2005-01-16 12:57:40 -0800 (Sun, 16 Jan 2005)
Revision: 6414
Log message:

      This commit was manufactured by cvs2svn to create branch
      'opname_classes'.

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-01-16 19:48:54 -0800 (Sun, 16 Jan 2005)
Revision: 6415
Log message:

      This branch views the token parameter as an opname (see bug #370),
      with rudimentary support for opname classes.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-01-16 20:02:36 -0800 (Sun, 16 Jan 2005)
Revision: 6416
Log message:

      Eliminated the .mlz files in refiner/refsig.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-01-16 20:20:12 -0800 (Sun, 16 Jan 2005)
Revision: 6417
Log message:

      Eliminate the .mlz files in filter/base
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-01-16 23:37:14 -0800 (Sun, 16 Jan 2005)
Revision: 6422
Log message:

      Initial opname class testing.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-01-17 17:27:19 -0800 (Mon, 17 Jan 2005)
Revision: 6426
Log message:

      This extends the term classification system.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-01-17 18:30:19 -0800 (Mon, 17 Jan 2005)
Revision: 6427
Log message:

      Some syntax changes.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-01-17 18:38:26 -0800 (Mon, 17 Jan 2005)
Revision: 6428
Log message:

      Added some new class tests in Syntax_test.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-01-17 19:02:56 -0800 (Mon, 17 Jan 2005)
Revision: 6429
Log message:

      Long parameter type names should be treated as token classes.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-01-18 13:33:18 -0800 (Tue, 18 Jan 2005)
Revision: 6432
Log message:

      I think that keeping track of the class information in signatures
      is not necessary, so this is a commit before removal.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-01-18 15:34:32 -0800 (Tue, 18 Jan 2005)
Revision: 6433
Log message:

      Aleksey is right, we need to keep opname info in signatures.
      This commit includes a opname type checker (not working at
      the moment).
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-01-18 17:48:46 -0800 (Tue, 18 Jan 2005)
Revision: 6434
Log message:

      No-op: minor code reordering
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-01-18 18:22:54 -0800 (Tue, 18 Jan 2005)
Revision: 6435
Log message:

      (Bug 382) This patch:
      
      1) Changes all the sequents to have exactly one conclusion
      
      2) Fixes a lot of places in the code that confuses "goals" with "conclusions".
      I tried making a clearer distinction between hyps/concls of a sequent and
      assums/goals of a meta-sequent. In particular, the "sequent_goals" field
      became "sequent_concl", "replace_goal" function became "replace_concl", etc.
      
      3) The syntax allows for either one conclusion, or none. If no conclusions is
      given, the xnil_term will be used.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-01-18 18:59:07 -0800 (Tue, 18 Jan 2005)
Revision: 6437
Log message:

      1. Added some cases to refine_error.
      2. Added Term_subst_sig.so_vars, to compute non-zero arity so-vars.
      3. Opname type checking now works at least minimally.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-01-18 20:15:00 -0800 (Tue, 18 Jan 2005)
Revision: 6438
Log message:

      Tracking of the full set of bindings in redex match was a bit incomplete, fixing
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-01-18 20:15:58 -0800 (Tue, 18 Jan 2005)
Revision: 6439
Log message:

      Added checking to inline terms.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-01-18 23:13:13 -0800 (Tue, 18 Jan 2005)
Revision: 6440
Log message:

      This changes how the rewriter handles free variables in the term paramerers
      (not redex) of a rewrite (or a rule). Bsically, the rwrriter is reasonably
      smart to allow those variables to be captured by the allowed contexts as
      appropriate and to disallow capture (by alpha-renaming, not by raising an
      exception) by the context that is not free in the parameter.
      
      P.S. This implements the algorithm outlined in
      https://lists.metaprl.org/mailman/private/metaprl-research/2005-January/000174.html
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-01-19 02:26:01 -0800 (Wed, 19 Jan 2005)
Revision: 6441
Log message:

      - Restructured the rewriter-related signatures a bit to make further changes
        easier
      
      - Updated the list of implicit PRL dependencies in the ocamldep to better
        match what the filter_prog is actually doing.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-01-19 11:26:36 -0800 (Wed, 19 Jan 2005)
Revision: 6442
Log message:

      Global update to use token opnames instead of strings.
      The theories that use records will get a lot of warning like this:
      
         warning: undeclared token: car
      
      To fix this, you need to declare the term 'car'.
      For most of labels, declaring them will be sufficient.
      For car, there are two places in the code that look like this:
      
         let car_opname = mk_opname "car" nil_opname
      
      Once you decide where to declare the opname, you should put this
      there.
      
         let car_opname = opname_of_term << car >>
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-01-19 12:40:47 -0800 (Wed, 19 Jan 2005)
Revision: 6443
Log message:

      Rewrites with tokens work fine, but the dtactic is not recognizing
      them properly.  I don't see how params affect the term_match_table
      care about params...
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-01-19 13:15:05 -0800 (Wed, 19 Jan 2005)
Revision: 6444
Log message:

      No-op: removed a number of unused "open" statements
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-01-19 14:40:52 -0800 (Wed, 19 Jan 2005)
Revision: 6445
Log message:

      Make it easier to mix MetaPRL and non-MetaPRL .ml files in theories.
      
      This is useful because non-MetaPRL compilation makes .mli optional,
      is faster, iand can be done without waiting for the filter to be built.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-01-19 18:14:46 -0800 (Wed, 19 Jan 2005)
Revision: 6446
Log message:

      I discovered than in each rule application, the rewriter was accessed _twice_.
      I've accidentally introduced this over a year ago :-(
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-01-19 19:09:45 -0800 (Wed, 19 Jan 2005)
Revision: 6447
Log message:

      The rewriter needed a RewriteToken value in addition to
      RewriteString.
      
      At this point, all proofs check.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-01-19 20:22:09 -0800 (Wed, 19 Jan 2005)
Revision: 6448
Log message:

      Added some display forms for the new declarations.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-01-19 21:21:00 -0800 (Wed, 19 Jan 2005)
Revision: 6449
Log message:

      Tweaked GC parameters a bit
      

Changes by: ( at unknown.email)
Date: 2005-01-19 21:21:00 -0800 (Wed, 19 Jan 2005)
Revision: 6450
Log message:

      This commit was manufactured by cvs2svn to create branch
      'opname_classes2'.

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-01-19 22:24:44 -0800 (Wed, 19 Jan 2005)
Revision: 6451
Log message:

      Merged the opname_classes onto the trank and branched again, creating a fresh
      branch called "opname_classes2".
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-01-20 00:03:57 -0800 (Thu, 20 Jan 2005)
Revision: 6452
Log message:

      Token types were not being checked.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-01-20 01:08:22 -0800 (Thu, 20 Jan 2005)
Revision: 6453
Log message:

      No-op: simplified Tactic_boot module structure a bit
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-01-20 11:33:49 -0800 (Thu, 20 Jan 2005)
Revision: 6454
Log message:

      Added the kinding relation.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-01-20 15:26:41 -0800 (Thu, 20 Jan 2005)
Revision: 6455
Log message:

      Minor clean-up from Jason
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-01-20 18:53:38 -0800 (Thu, 20 Jan 2005)
Revision: 6459
Log message:

      This is a nop-commit.  I just renamed Term_class to Term_ty, which
      is a bit more descriptive.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-01-20 20:05:53 -0800 (Thu, 20 Jan 2005)
Revision: 6460
Log message:

      Changed the names in Filter_cache_fun:
         "kinds" -> "typeclasses"
         "classes" -> "typeenv"
         "types"   -> "termenv"
      
      All typeclass names are now in Perv.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-01-20 20:08:11 -0800 (Thu, 20 Jan 2005)
Revision: 6463
Log message:

      Forgot to add these two files.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-01-21 10:03:45 -0800 (Fri, 21 Jan 2005)
Revision: 6464
Log message:

      Added type checking for non-sequent contexts.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-01-21 10:18:28 -0800 (Fri, 21 Jan 2005)
Revision: 6465
Log message:

      Added the occurs-check.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-01-21 14:40:51 -0800 (Fri, 21 Jan 2005)
Revision: 6466
Log message:

      The single-conclusion patch was a bit buggy in Term_gen (TERMS = std), fixing.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-01-21 15:13:46 -0800 (Fri, 21 Jan 2005)
Revision: 6467
Log message:

      Removed some unused code
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-01-21 18:08:31 -0800 (Fri, 21 Jan 2005)
Revision: 6468
Log message:

      Reduced the number of things that are compiled with -linkall.
      
      Now compiled w/o -linkall:
      - most helper libraries (including libmojave)
      - MetaPRL main binary (3.5% reduction in size of mp.opt)
      
      Still compiled with -linkall:
      - All the theory libraries (because their contents are the whole point!)
      - The filter binaries - this is pretty unfortunate, but the way camlp4 is
        compiled makes this almost unavoidable. I've filed
          http://caml.inria.fr/bin/caml-bugs?selectid=3439 about this.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-01-21 18:25:53 -0800 (Fri, 21 Jan 2005)
Revision: 6469
Log message:

      Added sequent types (but no sequent type checking yet).
      Here are some invariants.
      
      Typeclasses, declaring a new class class1.
      
         declare class1 <- class2
            -- Any term in class2 is also in class1.
      
         declare class1 -> class2
            -- Any term in class1 is also in class2.
      
         declare class1
            -- No subtyping relationship.
      
         -- The term << class1 >> has type << type >>.
         -- The term << class1 >> has typeclass << class1 >>.
      
      Type declarations, declaring a new type << ty{'a; 'b; 'c} >>.
      
         declare type ty{'a; 'b; 'c} : tc
            -- The term << ty{'a; 'b; 'c} >> has type << type >>
            -- The term << ty{'a; 'b; 'c} >> has typeclass << tc >>
      
         declare type ty{'a; 'b; 'c}
            -- The term << ty{'a; 'b; 'c} >> has type << type >>
            -- The term << ty{'a; 'b; 'c} >> has typeclass << term >>
      
      Term declarations:
      
         declare t[typedparams]{typed_bterms} : ty
      
         Typed items include : constraints.  Consider the following
         for example.
      
            declare typeclass foo -> term
            declare type list{'a : type} : foo
            declare nil : list{'a}
            declare cons{'hd : 'a; 'tl : list{'a}} : list{'a}
      
         If a constraint is missing, the type is << term >> by default.
         The term << list{'a : type} >> is a type for any type << 'a >>,
         and << nil >> and << cons{'hd; 'tl} >> have the expected types.
      
         Also, << nil >> and << cons{'hd; 'tl} >> have typeclass << foo >>,
         which is included in << term >>.
      
         The terms << foo >> and << list{'a} >> have type << type >>.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-01-22 12:27:15 -0800 (Sat, 22 Jan 2005)
Revision: 6471
Log message:

      - sequent_arg is no longer used except in the 0-arity form.
      - All proofs now replay without opname hacks.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-01-22 14:41:17 -0800 (Sat, 22 Jan 2005)
Revision: 6472
Log message:

      - Added initial sequent type checking.
      - Upgraded CIC to single-conclusion sequents.
        For compatibility, added sequent args in the form
           sequent [|term|] { ... }
        where term is wrapped as << sequent_arg{term} >>.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-01-22 18:51:22 -0800 (Sat, 22 Jan 2005)
Revision: 6473
Log message:

      Added type checking for context arguments <|H,J|>, etc.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-01-22 21:50:07 -0800 (Sat, 22 Jan 2005)
Revision: 6474
Log message:

      Added checking of rules and rewrites.
      
      I don't know the status of the simple-context work, but
      it needs to make is_context_term return true on contexts
      I think (see Itt_test.context_rw).
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-01-23 09:55:56 -0800 (Sun, 23 Jan 2005)
Revision: 6475
Log message:

      Move the term record definitions into Term_sig proper.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-01-23 14:11:01 -0800 (Sun, 23 Jan 2005)
Revision: 6476
Log message:

      I have started writing a module that would provide a "debug" Refiner which
      would run the "std" and the "ds" refiners in parallel and check for
      consistency. So far, I've only implemented a miniscule portion of the API,
      and this file is not added to the normal MetaPRL compilation in any way.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-01-23 15:17:56 -0800 (Sun, 23 Jan 2005)
Revision: 6477
Log message:

      Made the order in subterm_addresses more consistent with term_ds
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-01-23 17:26:12 -0800 (Sun, 23 Jan 2005)
Revision: 6478
Log message:

      Make the Term_grammar produce terms of type "parsed_term", which
      is an abstract type.  This forces us to to do a term_of_parsed_term
      and a type check before getting a real term.
      
      All proofs still check.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-01-23 19:03:44 -0800 (Sun, 23 Jan 2005)
Revision: 6479
Log message:

      Separated tokens from normal terms.
      
      The final thing to do is get mmc to compile, then we should merge.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-01-23 19:56:31 -0800 (Sun, 23 Jan 2005)
Revision: 6480
Log message:

      Upgrading mmc.
         - Added typeclasses for grammar symbols.
         - Do not check that iforms preserve types.
      
      mmc doesn't compile yet, and probably won't for a while
      until I am done.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-01-23 21:56:23 -0800 (Sun, 23 Jan 2005)
Revision: 6482
Log message:

      Finished TermType, Term and most of TermOp
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-01-23 22:29:36 -0800 (Sun, 23 Jan 2005)
Revision: 6483
Log message:

      Finished TermOp
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-01-23 23:04:46 -0800 (Sun, 23 Jan 2005)
Revision: 6484
Log message:

      Finished TermAddr, working on TermMan
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-01-23 23:49:52 -0800 (Sun, 23 Jan 2005)
Revision: 6485
Log message:

      Finished TermMan
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-01-24 00:09:13 -0800 (Mon, 24 Jan 2005)
Revision: 6486
Log message:

      Finished TermSubst
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-01-24 00:51:21 -0800 (Mon, 24 Jan 2005)
Revision: 6487
Log message:

      Finished TermMeta
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-01-24 01:17:53 -0800 (Mon, 24 Jan 2005)
Revision: 6488
Log message:

      Removing the unused TermEval.
      
      TermEval was the very first thing I tried to do in MetaPRL (back in 1998).
      A lot of things came out if the ideas behind that attempt (including the
      Term_ds module), but the TermEval implementation never got far and was
      never used in any way.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-01-24 10:26:29 -0800 (Mon, 24 Jan 2005)
Revision: 6489
Log message:

      Working on RefineError
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-01-24 10:47:09 -0800 (Mon, 24 Jan 2005)
Revision: 6490
Log message:

      Wrapped everything with an exception handler
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-01-24 11:47:46 -0800 (Mon, 24 Jan 2005)
Revision: 6491
Log message:

      Minor signature simplification
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-01-24 11:57:08 -0800 (Mon, 24 Jan 2005)
Revision: 6492
Log message:

      Finished Rewriter
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-01-24 12:28:29 -0800 (Mon, 24 Jan 2005)
Revision: 6493
Log message:

      Making progress with the Refine module
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-01-24 12:56:05 -0800 (Mon, 24 Jan 2005)
Revision: 6494
Log message:

      Finished the Refine module
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-01-24 13:09:02 -0800 (Mon, 24 Jan 2005)
Revision: 6495
Log message:

      The Refiner_debug module compiles now. It probably does not work yet, but
      if someone want to try, they are welcome to set "TERMS = both" in mk/config
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-01-24 15:42:39 -0800 (Mon, 24 Jan 2005)
Revision: 6496
Log message:

      The output of the context_vars is interpreted as a set, so it should be
      a SymbolSet.t, not var list.
      

Changes by: Alexei Kopylov (kopylov at cs.caltech.edu)
Date: 2005-01-24 17:30:33 -0800 (Mon, 24 Jan 2005)
Revision: 6497
Log message:

      Change definition of make_bterm
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-01-24 18:17:57 -0800 (Mon, 24 Jan 2005)
Revision: 6498
Log message:

      Minor optimization
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-01-24 20:14:24 -0800 (Mon, 24 Jan 2005)
Revision: 6499
Log message:

      Minor optimizations
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-01-24 22:55:29 -0800 (Mon, 24 Jan 2005)
Revision: 6500
Log message:

      Upgrading mmc.
      
      Currently in Mmc_core_type_check.
      
      Judgments like the following are a problem.
      
         sequent { <H> >- LetFunDecl{| <J> >- LetFunDef {| <K> >- 'prop |} |} }
      
      We *could* make such typings as the follows:
      
         LetFunDecl {| Exp : TyExp >- 'a |} : 'a
      
      But I don't know if this is so wise to let the body be so polymorphic.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-01-25 01:05:31 -0800 (Tue, 25 Jan 2005)
Revision: 6502
Log message:

      Minor fix in Refiner_debug: shapes are expected to be == in some cases
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-01-25 01:13:08 -0800 (Tue, 25 Jan 2005)
Revision: 6503
Log message:

      The integer tactics had some code that made some weird assumtions about how
      rewriting works - the assumptions that just happen to be true with TERMS=ds,
      but not with TERMS=std. I've changed the code to something more "safe".