Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-07-15 23:08:33 -0700 (Tue, 15 Jul 2003)
Revision: 4751
Log message:

      Added proper parsing for meta-terms and rule/rewrite arguments -- now the
      contexts in arguments are deduced base on what goes on in the meta-term.
      
      I was very surprized by how many rules currently allow SO variable in and
      out of contexts! Even with some reasonable heuristicts for figuring out the
      correct contexts, I still had to specify them manually in many places.
      
      Unfortunately, it seems that the grammar for bound contexts "killed" the nice
      grammar for the set types - so now I have to mess some more with the grammar :-(
      

Changes  Path
+3 -3 metaprl-branches/bound_contexts/filter/base/filter_summary_util.ml
+15 -0 metaprl-branches/bound_contexts/filter/filter/filter_parse.ml
+7 -9 metaprl-branches/bound_contexts/filter/filter/term_grammar.ml
+1 -1 metaprl-branches/bound_contexts/refiner/refiner/refine_error.ml
+5 -2 metaprl-branches/bound_contexts/refiner/reflib/refine_exn.ml
+1 -1 metaprl-branches/bound_contexts/refiner/refsig/refine_error_sig.ml
+2 -0 metaprl-branches/bound_contexts/refiner/refsig/term_meta_sig.ml
+5 -5 metaprl-branches/bound_contexts/refiner/rewrite/rewrite_compile_contractum.ml
+57 -50 metaprl-branches/bound_contexts/refiner/rewrite/rewrite_compile_redex.ml
+6 -2 metaprl-branches/bound_contexts/refiner/rewrite/rewrite_util.ml
+5 -6 metaprl-branches/bound_contexts/refiner/term_gen/term_addr_gen.ml
+1 -1 metaprl-branches/bound_contexts/refiner/term_gen/term_man_gen.ml
+46 -3 metaprl-branches/bound_contexts/refiner/term_gen/term_meta_gen.ml
+1 -1 metaprl-branches/bound_contexts/theories/itt/itt_equal.ml
+1 -1 metaprl-branches/bound_contexts/theories/itt/itt_equal.mli
+1 -1 metaprl-branches/bound_contexts/theories/itt/itt_pointwise.mli
+8 -8 metaprl-branches/bound_contexts/theories/itt/itt_squash.ml
+1 -1 metaprl-branches/bound_contexts/theories/itt/itt_squiggle.ml
+3 -3 metaprl-branches/bound_contexts/theories/itt/itt_struct.ml
+2 -2 metaprl-branches/bound_contexts/theories/itt/itt_struct.mli