Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2004-05-02 20:14:00 -0700 (Sun, 02 May 2004)
Revision: 5750
Log message:

      Some corrections on file dependencies.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2004-05-04 14:36:46 -0700 (Tue, 04 May 2004)
Revision: 5754
Log message:

      Add a "View" window to control what is displayed in the browser.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2004-05-04 20:14:55 -0700 (Tue, 04 May 2004)
Revision: 5755
Log message:

      o Added term "handles" in browser mode.  These allow more precise
        term selections.
      o "src" mode is parsable in most cases, at least in MMC.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2004-05-04 20:51:20 -0700 (Tue, 04 May 2004)
Revision: 5756
Log message:

      In HTML mode: the status line should give *relative* links.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-05-05 20:46:26 -0700 (Wed, 05 May 2004)
Revision: 5758
Log message:

      Fixing bug 219: only compute the "address array index" of a hyp context,
      when it is actually needed, and do not compute when processing an instance
      of a context already seen.
      

Changes by: Nataly Novak (nnovak at gc.cuny.edu)
Date: 2004-05-06 18:23:05 -0700 (Thu, 06 May 2004)
Revision: 5759
Log message:

      Started to work on case analysis operation for inductively defined types
      

Changes by: Nataly Novak (nnovak at gc.cuny.edu)
Date: 2004-05-09 20:17:58 -0700 (Sun, 09 May 2004)
Revision: 5760
Log message:

      1. some fixes in cic_lambda (got rid of WF{context} )
      2. completed proofs of listDef_wf, list_wf, nil_wf, cons_wf
      

Changes by: Brian Emre Aydemir (baydemir at cis.upenn.edu)
Date: 2004-05-10 11:15:25 -0700 (Mon, 10 May 2004)
Revision: 5761
Log message:

      itt_list2: exposing rev{'l} so that it can be used in other modules
      itt_int_arith: proved one of the remaining rules (le2ge I think)
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2004-05-10 15:08:00 -0700 (Mon, 10 May 2004)
Revision: 5762
Log message:

      unistd.h is not present in under win32 so it should not be included there
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2004-05-10 15:14:54 -0700 (Mon, 10 May 2004)
Revision: 5763
Log message:

      term_op - dep0_dep0_dep2 operations added to support induction over naturals
      itt_int_base - <<'a -@ 0>> added to reduce-resource
      itt_int_ext - added reductions for max and min over literals
      itt_nat - added dest_ind,mk_ind,is_ind and reduction for ind{number;...}
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2004-05-10 15:22:27 -0700 (Mon, 10 May 2004)
Revision: 5764
Log message:

      I started the theory of multivariate (or multivariable?) polynomials on top of
      one-var polynomials.
      I want to try to use it for polynomials normalization (convertion to a standard form)
      I managed to build reduction list so that resonable polynomials are evaluated
      (eval_mpoly) to what one would expect (even if values for vars are not literals!).
      Unfortunately it might still be too slow for practical purposes but we'll see.
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2004-05-10 21:52:59 -0700 (Mon, 10 May 2004)
Revision: 5765
Log message:

      next step to normalization:
      stdT field [t_1,...,t_n] T
      asserts that T is equal to T' where each t_i is replaced
      with a polynomial "x_n" evaluated on [t1...tn]
      this equality is proved automatically by (repeatT reduceT ttca)
      
      todo: lifting of polynomial evaluations in T' to outermost operation and evaluating
      it. AFAI understand it will evaluate to a "standard" form of T
      

Changes by: Nathaniel Gray (n8gray at caltech.edu)
Date: 2004-05-12 17:14:42 -0700 (Wed, 12 May 2004)
Revision: 5767
Log message:

      Allow user to override font and bold color with env. vars MPFONT and MPBOLD.
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2004-05-12 21:40:18 -0700 (Wed, 12 May 2004)
Revision: 5769
Log message:

      added Z.1 and Z.eq so Z is actually in unitringCE
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-05-13 02:35:26 -0700 (Thu, 13 May 2004)
Revision: 5770
Log message:

      Removing unused code (it was a part of the old-style comments support).
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2004-05-14 20:52:40 -0700 (Fri, 14 May 2004)
Revision: 5778
Log message:

      list2 - added standard helpers for length{} like mk_length_term, etc
      ring2, ring2_uce - a couple of lemmas about Z
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2004-05-14 21:02:50 -0700 (Fri, 14 May 2004)
Revision: 5779
Log message:

      normalization is kind of work but really slow - 10 secs for
      x + (x * y) + y + 1
      
      and the weird slowness is experienced at /itt_mpoly/test12/2/1/1
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2004-05-16 22:06:46 -0700 (Sun, 16 May 2004)
Revision: 5783
Log message:

      I'm trying another approach to multivariate polynomials:
      Polynomial is a (arbitrary) list of monomials.
      Each monomial is a pair of its coefficient and function from var-index to its exponent.
      This approach allows many representations of the same polinomial hence
      standartization/normalization function is provided.
      
      At this moment this approach looks an order of magnitude faster than itt_mpoly.
      (on eval(standardize(p)))
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2004-05-17 14:26:37 -0700 (Mon, 17 May 2004)
Revision: 5785
Log message:

      removed timingT
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-05-17 18:28:30 -0700 (Mon, 17 May 2004)
Revision: 5786
Log message:

      Moved the param' type to the top-level of the Term_sig module
      (to avoid having 5 copies of it).
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-05-17 19:37:03 -0700 (Mon, 17 May 2004)
Revision: 5787
Log message:

      Use dest_params instead of (List.map dest_param) and similar constructs.
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2004-05-17 21:47:14 -0700 (Mon, 17 May 2004)
Revision: 5788
Log message:

      Polynomial normalization works fine,
      still an order of magnitude faster than itt_mpoly.
      Time to add it to SupInf.
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2004-05-18 22:57:51 -0700 (Tue, 18 May 2004)
Revision: 5792
Log message:

      makefiles - removed references to itt_mpoly
      itt_mpoly2 - switched to W-type (up to this didn't use any recursion-type),
      AFAI understand W-type permits to do structural induction;
      proved several lemmas
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-05-19 02:02:14 -0700 (Wed, 19 May 2004)
Revision: 5793
Log message:

      A bit more profiling support. Now to get the profile text, one only needs to
      enable the NATIVE_PROFILING_ENABLED in mk.config and run
      "omake editor/ml/native_profile.txt".
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-05-19 05:14:07 -0700 (Wed, 19 May 2004)
Revision: 5794
Log message:

      Minor code clean-up (should also speed up things a little).
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-05-20 01:09:17 -0700 (Thu, 20 May 2004)
Revision: 5796
Log message:

      Minor code cleanup.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-05-20 03:45:43 -0700 (Thu, 20 May 2004)
Revision: 5797
Log message:

      Minor clean-up.
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2004-05-21 12:52:24 -0700 (Fri, 21 May 2004)
Revision: 5798
Log message:

      Tiny adjustments
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-05-21 13:01:38 -0700 (Fri, 21 May 2004)
Revision: 5799
Log message:

      Removing couple of unused types.
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2004-05-21 13:16:08 -0700 (Fri, 21 May 2004)
Revision: 5800
Log message:

      Made a benchmarking:
      arithT(+normalizeC)  vs  arithT+itt_mpoly2.standardizeT
      on itt_int_arith/test* arithT+normalizeC is 12 times faster.
      Partly because of lot's of wf-subgoals.
      (There was an impression that a reflection based normalization
      is not supposed to make a lot of wf-subgoals.)
      Partly because of inefficient strategy of computation I guess.
      So I have to figure out what's going on. First, I'm going to strip out
      itt_mpoly2 computations into a separate resource (it's in reduce now)
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2004-05-21 18:45:24 -0700 (Fri, 21 May 2004)
Revision: 5801
Log message:

      Infinite cycle was due to a rule added to elim-resource that can be
      applied to result of itself. Fixed.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-05-21 19:25:05 -0700 (Fri, 21 May 2004)
Revision: 5802
Log message:

      Comented out the "crwhigher" refiner mechanism. The tactics module will now
      use the external mechanism for a higherC of a conditional rewrite.
      
      The above should make it harder (but not entirely impossible yet) to improperly
      lift a variable out of its scope by a conditional rewrite.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-05-21 21:33:15 -0700 (Fri, 21 May 2004)
Revision: 5803
Log message:

      Simplified the internal address type in Term_ds. The Term_std could probably be
      simplified as well, but it's not worth spending time on.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-05-21 21:34:10 -0700 (Fri, 21 May 2004)
Revision: 5804
Log message:

      Oops, forgot the .mli change in the last commit.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-05-21 22:20:05 -0700 (Fri, 21 May 2004)
Revision: 5805
Log message:

      Fixed the out-of-scope test for assumptions produced by the conditional
      rewrites. Hopefully this fixes bug 156.
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2004-05-22 09:30:25 -0700 (Sat, 22 May 2004)
Revision: 5806
Log message:

      A fix to one of two proofs broken yesterday.
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2004-05-22 17:47:53 -0700 (Sat, 22 May 2004)
Revision: 5807
Log message:

      This repairs the second of two proofs broken yesterday.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-05-22 18:36:34 -0700 (Sat, 22 May 2004)
Revision: 5808
Log message:

      Added stricter checking of the shapes for opnames specified using the FQN notation.
      

Changes by: ( at unknown.email)
Date: 2004-05-22 18:36:34 -0700 (Sat, 22 May 2004)
Revision: 5809
Log message:

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

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-05-22 18:51:10 -0700 (Sat, 22 May 2004)
Revision: 5810
Log message:

      Adding the Quote parameter to the list of the possible term paramaters.
      I have changed the filter_cache_fun's opname handling to ignore the quotation
      level when checking whether opname is declared (in other words, delcaring an
      unquoted operator also implicitly declares all the quoted version of it).
      
      Of course, this does not compile as nothing else was changed yet.
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2004-05-22 22:49:50 -0700 (Sat, 22 May 2004)
Revision: 5811
Log message:

      Split all evaluations to a separate resource, for now it refers to
      reduceC for basic computations.
      Now it's only 9 times slower than normalizeC
      (primarily because of reduced number of wf-subgoals).
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2004-05-23 21:06:00 -0700 (Sun, 23 May 2004)
Revision: 5812
Log message:

      Tiny bugfix: reduce_cmp_lexi had incorrect base case.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-05-24 16:42:33 -0700 (Mon, 24 May 2004)
Revision: 5813
Log message:

      Give a better error message in interface/implementation mismatch.
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2004-05-24 23:30:20 -0700 (Mon, 24 May 2004)
Revision: 5814
Log message:

      list2 - unfold_mklist was not in the interface
      mpoly2 - change in the representation:
      monom was represented as a function from var-index to its exponent
      now monom is a list of exponents of _all_ variables
      with this version intermediate steps of computation are much more readable,
      which permitted to make several optimizations in the order of computations.
      
      I'm going to switch to the third version - monom is a list of non-zero exponents
      (with variable indices).
      Or even reject polynomials as an intermediate representation and
      do all manipulations on the raw reflected syntax.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-05-26 14:41:58 -0700 (Wed, 26 May 2004)
Revision: 5815
Log message:

      Use an explicit MLast.loc type (as opposed to expanding it into "int * int")
      where appropriate.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-05-26 15:21:31 -0700 (Wed, 26 May 2004)
Revision: 5816
Log message:

      Use a "canonical" Filter_util.dummy_loc instead of using "(0, 0)" all over
      the place.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-05-26 15:43:57 -0700 (Wed, 26 May 2004)
Revision: 5817
Log message:

      Removing an unused file.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-05-26 15:46:35 -0700 (Wed, 26 May 2004)
Revision: 5818
Log message:

      One more place where MLast.loc should be used instead of int * int
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-05-27 14:06:13 -0700 (Thu, 27 May 2004)
Revision: 5819
Log message:

      Minor code cleanup/optimization.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2004-05-27 19:00:18 -0700 (Thu, 27 May 2004)
Revision: 5820
Log message:

      This is the browser update I've been putting off.
         1. Browser now support both Mozilla *and* IE.
            I haven't tested on others like Safari.
            To get this to work, I had to use iframes
            and code custom menus.  Bleh.
         2. Connections are now SSL.  That is, you need to
            use https: connections instead of http:
         3. File editing is partially supported.  By default
            you edit in the browser.  However, you can define
            the application/x-metaprl MIME type to invoke
            an external editor.
      
            This is the main reason for using SSL.  At some
            point, we should do a code review to make sure
            we believe the security model
            (MD5 challenge/response).
      
      TODO:
         1. Currently, edited files are not saved.  This is
            just a precaution for the moment.
         2. Need to add make/restart commands.  Easy, just
            haven't done it yet.
      
      NOTE: I haven't checked that win32 compiles.  Working on that
      next.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-05-27 21:41:05 -0700 (Thu, 27 May 2004)
Revision: 5821
Log message:

      More code clean-up.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2004-05-27 23:03:51 -0700 (Thu, 27 May 2004)
Revision: 5822
Log message:

      SSL should be off by default.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-05-27 23:08:24 -0700 (Thu, 27 May 2004)
Revision: 5823
Log message:

      The generated proxyedit_lex.ml should be ignored and cleaned.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-05-27 23:10:10 -0700 (Thu, 27 May 2004)
Revision: 5824
Log message:

      Delete lib/*.gif and lib/*.pem on "omake clean"
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-05-28 00:34:56 -0700 (Fri, 28 May 2004)
Revision: 5825
Log message:

      More code clean-up. This speeds up "status_all" by about 1%.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2004-05-28 09:11:44 -0700 (Fri, 28 May 2004)
Revision: 5826
Log message:

      Win32 bugfix update.   MetaPRL should now compile correctly on win32.
      Also, the proxyedit application compiles with SSL.
      
      Question: to use MetaPRL on win32 from a remote server, all you need
      is the proxyedit application (if you want it).  Should we put it on
      some standard site like www.metaprl.org?  Or should we commit it as
      part of MetaPRL CVS.  The advantage of the latter is that we can
      use MetaPRL even without global Internet access.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-05-28 13:47:37 -0700 (Fri, 28 May 2004)
Revision: 5827
Log message:

      More clean-up.
      

Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2004-05-28 17:14:30 -0700 (Fri, 28 May 2004)
Revision: 5828
Log message:

      Updated the refiner directory with the quote parameter.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2004-05-28 22:42:51 -0700 (Fri, 28 May 2004)
Revision: 5829
Log message:

      New SSL method to provide a "standard" socket interface,
      except certificates are required for some calls.
      
      Tested on RedHat 9.
         - Not tested on old Redhat mojave clients.
         - Not tested on win32 (that is next).
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2004-05-28 23:45:16 -0700 (Fri, 28 May 2004)
Revision: 5830
Log message:

      Proxyedit now works on win32, so we can call an external editor on windows.
         1. The default editor is notepad (bleh), but it can be changed to
            a sensible editor by placing the command in ~/.metaprl/editor.
         2. We get the usual extra-dumb console windows on M$.  I
            believe Microlimp sucks.  Anyway, we can consider using a
            runemacs-style hack to hide the console window.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-05-29 00:47:01 -0700 (Sat, 29 May 2004)
Revision: 5831
Log message:

      More code clean-up.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-05-29 13:06:51 -0700 (Sat, 29 May 2004)
Revision: 5832
Log message:

      - in unquote_term, make sure term does not have one of the "special" (var or
        sequent) opnames.
      - declare quotation operators in the sinature file
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2004-05-30 12:12:31 -0700 (Sun, 30 May 2004)
Revision: 5833
Log message:

      Added some additional functions.  Status: tested with and without SSL on
      RH9; not tested on mojave clients; mostly tested on win32.  I'll check
      the others after this commit.  Tested against Mozilla and IE.  It should
      be clean, but let me know if you see problems!
      
      Added the following functions to the toploop:
         !ls: int                -- filesystem directory listing
         !cd: string -> int      -- change directory
         !pwd: string            -- print working directory
         !mkdir: string -> int   -- create a new directory
         !rm: string -> int      -- remove a file
         !edit: string -> int    -- edit a file
         !omake: int             -- rebuild the system
         !restart: int           -- restart MetaPRL
         !cvs: string -> int     -- CVS operations
      Note that the syntax of these "syscall" commands uses dereferencing.
      
      These functions work with the terminal and browser interfaces
      (with slightly different behavior).
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2004-05-30 12:55:20 -0700 (Sun, 30 May 2004)
Revision: 5834
Log message:

      Minor changes to get Win32 to run.
      Note that Unix.fstat and Unix.fchmod do not work on
      win32.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2004-05-30 12:55:48 -0700 (Sun, 30 May 2004)
Revision: 5835
Log message:

      Ignore more files.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2004-05-30 13:39:53 -0700 (Sun, 30 May 2004)
Revision: 5836
Log message:

      Minor fixes.
      Tested on win32 and mojave clients.
      

Changes by: Brian Emre Aydemir (baydemir at cis.upenn.edu)
Date: 2004-05-31 20:04:40 -0700 (Mon, 31 May 2004)
Revision: 5841
Log message:

      Itt_list2: filled in a few proofs.
      Itt_nat: added a display form for nat_plus.