Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-02-06 15:21:43 -0800 (Sun, 06 Feb 2005)
Revision: 6607
Log message:

      Typechecking is now stricter.
         -- For rules and rewrites, the goal types are existentially quantified.
         -- Rewrites are type-invariant.  For example, the following will fail.
      
            declare typeclass A
            declare typeclass B -> A
            declare foo : A
            declare bar : B
      
            prim_rw bad : foo <--> bar
      
            This is rejected because the (bar --> foo) rewrite is bogus.
      
      At this point, the type system is basically sound, apart from
      rule and rewrite arguments, and assuming the implementation is
      correct.  Let's merge.
      

Changes  Path
+6 -6 metaprl-branches/opname_classes4/filter/base/filter_cache_fun.ml
+1 -0 metaprl-branches/opname_classes4/filter/base/filter_summary_type.ml
+21 -18 metaprl-branches/opname_classes4/filter/base/filter_type.ml
+24 -23 metaprl-branches/opname_classes4/filter/filter/filter_parse.ml
+6 -0 metaprl-branches/opname_classes4/filter/filter/term_grammar.ml
+2 -0 metaprl-branches/opname_classes4/refiner/refiner/refiner_debug.ml
+343 -395 metaprl-branches/opname_classes4/refiner/reflib/term_ty_infer.ml
+7 -6 metaprl-branches/opname_classes4/refiner/reflib/term_ty_infer.mli
+1 -0 metaprl-branches/opname_classes4/refiner/refsig/term_meta_sig.ml
+7 -9 metaprl-branches/opname_classes4/support/display/perv.mli
+7 -0 metaprl-branches/opname_classes4/support/shell/package_info.ml
+9 -8 metaprl-branches/opname_classes4/support/shell/package_info.mli
+1 -0 metaprl-branches/opname_classes4/support/shell/shell_core.ml
+66 -55 metaprl-branches/opname_classes4/support/shell/shell_state.ml
+1 -0 metaprl-branches/opname_classes4/support/shell/shell_state.mli
+0 -0 metaprl-branches/opname_classes4/theories/base/base_reflection.ml
+2 -2 metaprl-branches/opname_classes4/theories/experimental/compile/m_ir_ast.ml
+4 -0 metaprl-branches/opname_classes4/theories/phobos/phobos_base.mli
+2 -2 metaprl-branches/opname_classes4/theories/phobos/phobos_theory.ml
+6 -10 mpcompiler-branches/opname_classes4/mmc/arch/x86/mmc_x86_asm.mli
+3 -2 mpcompiler-branches/opname_classes4/mmc/arch/x86/mmc_x86_closure.ml
+4 -4 mpcompiler-branches/opname_classes4/mmc/arch/x86/mmc_x86_codegen.mli
+1 -1 mpcompiler-branches/opname_classes4/mmc/arch/x86/mmc_x86_convention.ml
+1 -1 mpcompiler-branches/opname_classes4/mmc/arch/x86/mmc_x86_frame.ml
+8 -8 mpcompiler-branches/opname_classes4/mmc/arch/x86/mmc_x86_frame.mli
+11 -4 mpcompiler-branches/opname_classes4/mmc/arch/x86/mmc_x86_prologue.ml
+1 -1 mpcompiler-branches/opname_classes4/mmc/arch/x86/mmc_x86_prologue.mli
+1 -1 mpcompiler-branches/opname_classes4/mmc/arch/x86/mmc_x86_slop.ml
+3 -1 mpcompiler-branches/opname_classes4/mmc/arch/x86/mmc_x86_spill.ml
+8 -0 mpcompiler-branches/opname_classes4/mmc/base/mmc_base_judgment.mli
+3 -1 mpcompiler-branches/opname_classes4/mmc/core/mmc_core_hoist.ml
+1 -1 mpcompiler-branches/opname_classes4/mmc/extensions/array/mmc_ext_array_x86.ml