Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2003-08-04 17:37:15 -0700 (Mon, 04 Aug 2003)
Revision: 4814
Log message:

      This is an unsatisfying workaround to the context scoping
      problem.  As mentioned in the previous commit, this is what
      we want:
      
       sequent [Lambda] { <H> >- 'e } : sequent [TyAll] { <K> >- 't<|K|> }
       <-->
       sequent [Lambda] { <H> >- TyConstrain{'e; 't<|H|>} } :
       sequent [TyAll] { <K> >- 't<|K|> }
      
      We should really get this notation to work.  In the meantime,
      we use this workaround:
      
       sequent [Lambda] { <H> >- 'e } : sequent [TyAll] { <K> >- 't<|K|> }
       <-->
              collect{ty_vars. sequent [Lambda] { <H> >-
                 TyConstrain{'e; Apply{sequent [Lambda] { <K> >- 't<|K|> }; 'ty_vars}} :
       sequent [TyAll] { <H> >- 't<|K|> }
      
      Remember, collect{ty_vars. sequent [...] { <H> >- ... }} builds
      a list of the binding vars in <H>.
      
      That is, we use beta-reduction to perform an explicit substitution.
      It should work, but makes the code large, slow, and ugly.
      

Changes	Path
+2 -1	metaprl/filter/filter/filter_patt.ml
+15 -3	mpcompiler-branches/mojave_sequents/mmc/core/mmc_core_cps.ml
+15 -16	mpcompiler-branches/mojave_sequents/mmc/core/mmc_core_type_infer.ml