Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-01-25 16:37:16 -0800 (Tue, 25 Jan 2005)
Revision: 6505
Log message:

      This changes the sequent_arg in mmc_base_judgment to the following:
      
         declare sequent [sequent_arg] { Univ[name:UnivClass,i:l] : Univ[name:UnivClass,i':l] >- Prop } : Judgment
      
      where for convenience, we have the following:
      
         iform unfold_exp       : Exp <--> Univ["exp":t,0:l]
         iform unfold_ty_exp    : TyExp <--> Univ["exp":t,1:l]
         iform unfold_kind_exp  : KindExp <--> Univ["exp":t,2:l]
         iform unfold_prop_exp  : Prop <--> Univ["prop":t,1:l]
      
      The parameter quantifiers are *within* the hyps clause (still
      be added to the type checker).
      
         declare sequent [sequent_arg] { (all name:t, all i:l.
                                            Univ[name:UnivClass,i:l]
                                            : Univ[name:UnivClass,i':l])
                                        >- Prop } : Judgment
      
      The non-disjoint union types make a lot of sense, but are impossible
      to implement.
      
      This solution preserves parametric polymorphism.
      

Changes  Path
+5 -0 metaprl-branches/opname_classes2/filter/base/filter_cache_fun.ml
+41 -0 metaprl-branches/opname_classes2/filter/base/filter_grammar.ml
+7 -0 metaprl-branches/opname_classes2/filter/base/filter_grammar.mli
+1 -0 metaprl-branches/opname_classes2/filter/filter/filter_parse.ml
+9 -2 metaprl-branches/opname_classes2/filter/filter/term_grammar.ml
+3 -3 metaprl-branches/opname_classes2/refiner/reflib/term_ty_infer.ml
+1 -1 metaprl-branches/opname_classes2/support/display/perv.ml
+1 -1 metaprl-branches/opname_classes2/support/display/perv.mli
+25 -3 mpcompiler-branches/opname_classes2/mmc/base/mmc_base_judgment.ml
+24 -2 mpcompiler-branches/opname_classes2/mmc/base/mmc_base_judgment.mli
+10 -25 mpcompiler-branches/opname_classes2/mmc/core/mmc_core_ast.mli
+13 -27 mpcompiler-branches/opname_classes2/mmc/core/mmc_core_tast.mli
+22 -16 mpcompiler-branches/opname_classes2/mmc/core/mmc_core_type_check.ml
+11 -2 mpcompiler-branches/opname_classes2/mmc/core/mmc_core_type_check.mli