Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2004-12-12 02:33:42 -0800 (Sun, 12 Dec 2004)
Revision: 6356
Log message:

       - Added the var_bterm case support for make_bterm in base_reflection.
       - Fixed some bugs in itt_reflection; Added some primitive rules.
      
      The four lemmas for "subst_make_bterm" haven't been proved yet.
      
      Just want to do the commit before fixing this bug:
      ---------
        Do we consider these two bterms are the same?
           1. 'b1 = bterm{| x: term >- it[@] |}
           2. 'b2 = bterm{| >- it[@] |}
      
        If yes, then we should modify the definition of if_simple_bterm.
      
        If no, then "makebterm_same_op" is not valid, since
           make_bterm { 'b1; [] } <-->
           make_bterm{ 'b1; subterms{'b1} } <-->
           'b1
        and
           make_bterm{ 'b1; [] } <-->
           make_bterm{ 'b1; subterms{'b2} } <-->
           'b2
        which gives
           'b1 <--> 'b2
      

Changes  Path
+16 -3 metaprl/theories/base/base_reflection.ml
+17 -0 metaprl/theories/itt/itt_int_ext.ml
+12 -0 metaprl/theories/itt/itt_int_ext.mli
+7334 -6899 metaprl/theories/itt/itt_int_ext.prla
+5 -0 metaprl/theories/itt/itt_list.ml
+5 -0 metaprl/theories/itt/itt_list2.ml
+3493 -3323 metaprl/theories/itt/itt_list2.prla
+214 -40 metaprl/theories/itt/itt_reflection.ml
+4 -0 metaprl/theories/itt/itt_reflection.mli
+6720 -3949 metaprl/theories/itt/itt_reflection.prla