Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-11-02 11:56:52 -0800 (Tue, 02 Nov 2004)
Revision: 6256
Log message:

      Do not use ocamlfind, even if it is installed.
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2004-11-09 22:52:49 -0800 (Tue, 09 Nov 2004)
Revision: 6257
Log message:

      New code that generates trace of supinf's reasoning and than constructs the proof.
      It proves all but the biggest test (itt_supinf/inttestn).
      Couldn't submit the proofs because metaprl crashes on export.
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2004-11-10 10:58:03 -0800 (Wed, 10 Nov 2004)
Revision: 6258
Log message:

      My previous commit introduced a bug in SupInf which was causing "wrong" results in
      the inttestn. This commit fixes the problem.
      inttestn still can't be proved but this is alright because currently SupInf
      only makes one pass but full Shostak's SupInf does multi-pass.
      It might not be easy to implement multipass SupInf
      (not because of practical reasons but because of theoretical ones).
      Multipass version on n+1 pass takes the bounds [a;b] for variable v found on n-pass
      and replaces v with any integer from [a;b] then do SupInf again.
      Of course we can't do it in a tactic without proving it correct.
      what I'm going to do is instead of replacing v with some integer from [a;b]
      I'll add  ceiling(a) <= v <= floor(b).
      Though I'm not sure yet that this approach would give the same results as the original.
      

Changes by: Alexei Kopylov (kopylov at cs.caltech.edu)
Date: 2004-11-10 16:18:44 -0800 (Wed, 10 Nov 2004)
Revision: 6259
Log message:

      Define a type for simple lambda terms.
      To do this I had too add several theories:
      
        - Itt_sqsimple defines types with squiggle equality
        - Itt_power defines the type Power[i:l]{'T} -- type of all subsets of T.
        - Itt_functions defines the image  of functions, surjection, injection, reversible function and so on
        - Itt_closure defines closure of collection of function on a type T
        - Itt_pairwise defines axioms for pairwise functionality (we need this for the induction principle).
        - Itt_pairwise2 has theorems that are true only in  pairwise functionality.
        - Itt_reflection_example_lambda defines the type for simple lambda terms.
      
      
      Also:
      
      -Add squash stability for <=, >, <, <> in Itt_int_ext
      
      -Add some other simple theorems.
      
      -Add AutoMustComplete option to subtype_axiomFormation.
      It could break some proofs, I'll fix them later.
      
      Some proofs are still unfinished.
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2004-11-10 21:25:54 -0800 (Wed, 10 Nov 2004)
Revision: 6260
Log message:

      Forgot to switch off the debug output
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-11-12 18:35:54 -0800 (Fri, 12 Nov 2004)
Revision: 6263
Log message:

      The Smap module was just a dup of Lm_serial_map.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-11-12 18:52:43 -0800 (Fri, 12 Nov 2004)
Revision: 6264
Log message:

      The CVS version of OCaml now supports "unused variable" warnings.
      I've just started going over the MetaPRL code and eliminating these
      warnings. So far I've found one real bug - Lm_symbol.compare_triple
      was incorrect.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-11-12 19:01:52 -0800 (Fri, 12 Nov 2004)
Revision: 6265
Log message:

      Committed a bit too much in my last commit.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-11-13 11:17:28 -0800 (Sat, 13 Nov 2004)
Revision: 6266
Log message:

      Fixing another breakage from yesterday's commit. Sorry for not fixing it earlier.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-11-13 11:21:12 -0800 (Sat, 13 Nov 2004)
Revision: 6267
Log message:

      In automated scripts, unset OMAKEFLAGS before running omake.
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2004-11-14 15:20:00 -0800 (Sun, 14 Nov 2004)
Revision: 6268
Log message:

      Finally, I've managed to export most of the proofs.
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2004-11-14 18:54:28 -0800 (Sun, 14 Nov 2004)
Revision: 6269
Log message:

      A little more proofs.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-11-16 20:03:00 -0800 (Tue, 16 Nov 2004)
Revision: 6270
Log message:

      Updating some of the autoT stuff to fix some of the proofs broken by
      Alexei's big Nov 10th commit.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-11-16 23:02:15 -0800 (Tue, 16 Nov 2004)
Revision: 6271
Log message:

      More unused variables eliminated.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-11-17 12:33:52 -0800 (Wed, 17 Nov 2004)
Revision: 6272
Log message:

      Split couple of long lines.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-11-17 18:52:42 -0800 (Wed, 17 Nov 2004)
Revision: 6273
Log message:

      Chages and comments from today's reflection meeting (I haven't yet made any
      attempts at fixing the proofs, though).
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-11-17 21:25:05 -0800 (Wed, 17 Nov 2004)
Revision: 6274
Log message:

      Fixing some of the proofs broken by today's reflection changes.
      Xin, I am leaving the rest of them to you.
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2004-11-18 11:41:36 -0800 (Thu, 18 Nov 2004)
Revision: 6279
Log message:

      Moved some code from itt_supinf to reflib/supinf
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-11-18 22:32:50 -0800 (Thu, 18 Nov 2004)
Revision: 6281
Log message:

      Fixed "omake doc".
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-11-20 12:35:57 -0800 (Sat, 20 Nov 2004)
Revision: 6282
Log message:

      Do not use -file-line-error-style yet.
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2004-11-20 20:14:37 -0800 (Sat, 20 Nov 2004)
Revision: 6283
Log message:

      itt_rat - definition of GCD was incorrect on negative numbers
      refiner/reflib/supinf - removed some unused cases.
      itt_supinf - minor modifications
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2004-11-21 22:39:51 -0800 (Sun, 21 Nov 2004)
Revision: 6285
Log message:

      Now it does not normalize hypotheses that are not used.
      Though it re-normalizes used hypotheses as many times as they used.
      (will fix it next time)
      At this point it is only 3.5 slower than Arith
      but the speed up is mainly due inttestn which is not proved anyway.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-11-24 15:53:48 -0800 (Wed, 24 Nov 2004)
Revision: 6289
Log message:

      MetaPRL works fine with 3.08.2 (no special patches needed).
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-11-24 22:18:41 -0800 (Wed, 24 Nov 2004)
Revision: 6291
Log message:

      Xstr_search was borrowed from somebody else's package and I am unsure
      what the license on that is. Turns out it wasn't used in any really
      meaningful way, so I got rid of it.
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2004-11-29 18:35:46 -0800 (Mon, 29 Nov 2004)
Revision: 6292
Log message:

      "is_empty" added to the interface
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2004-11-29 18:44:04 -0800 (Mon, 29 Nov 2004)
Revision: 6293
Log message:

      1. Fixed two bugs in old code (since spring)
      2. Now it's more like Shostak's version - if first variable did not produce
      a contradiction it attempts the next variable, etc.
      ToDo: If SupInf computed that a<=v<=b and there is no integer between
      a and b we can conclude a contradiction.
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2004-11-29 19:20:31 -0800 (Mon, 29 Nov 2004)
Revision: 6294
Log message:

      Forgot to uncomment one little bit of code.
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2004-11-29 22:23:09 -0800 (Mon, 29 Nov 2004)
Revision: 6295
Log message:

      Now it understands that there is no integers between 'n and 'n+1