Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-06-24 01:26:53 -0700 (Thu, 24 Jun 2004)
Revision: 6007
Log message:

      This is a first step towards making some of our module signature and functor
      setup a bit saner (and bring us closer to being able to solve the "have to open
      too many modules" bug 169).
      
      This commit does exactly one thing instead of repeating all the TermType types
      in the Term module (and corresponding signature) and keep saying all over the
      place that the types are actually identical, this creates a _submodule_
      Term.TermTypes that contains those repeated types.
      
      This reduces the amount of the "useless" signature code by almost 800 lines -
      mostly by allowing to replace a long list of "with type foo = TermType.foo"
      with a single "with module TermTypes = TermType".
      
      The way this is related to bug 169 is that OCaml does not allow to include
      two modules that both have the same type field. E.g.
      "include Refiner.Refiner.TermType;; include Refiner.Refiner.Term"
      used to result in a "duplicate type term" error. However now that
      Refiner.Refiner.Term does not have a term type (only Refiner.Refiner.Term.TermTypes
      does), it should now be possible to include both modules into a single one.
      One _all_ repeated types in all the basics modules are resolved this way,
      we should be able to solve bug 169 by creating a module that includes all
      the modules we care about.
      

Changes  Path
+2 -2 metaprl/editor/ml/nuprl_jprover.mli
+1 -1 metaprl/editor/ml/nuprl_run.mli
+2 -2 metaprl/filter/base/filter_cache.ml
+1 -1 metaprl/filter/base/filter_cache.mli
+1 -1 metaprl/filter/base/filter_summary_util.mli
+2 -2 metaprl/filter/base/filter_type.ml
+1 -1 metaprl/filter/filter/filter_prog.ml
+5 -5 metaprl/filter/phobos/phobos_constants.mli
+6 -9 metaprl/filter/phobos/phobos_type.ml
+10 -10 metaprl/filter/phobos/phobos_type.mli
+5 -5 metaprl/library/basic.mli
+7 -7 metaprl/library/db.mli
+40 -40 metaprl/library/definition.mli
+213 -213 metaprl/library/library.mli
+1 -0 metaprl/library/library_type_base.ml
+5 -5 metaprl/library/library_type_base.mli
+6 -7 metaprl/library/link.mli
+1 -1 metaprl/library/mbterm.mli
+1 -1 metaprl/library/nuprl5.mli
+1 -0 metaprl/library/oidtable.ml
+36 -36 metaprl/library/oidtable.mli
+11 -11 metaprl/library/orb.mli
+2 -8 metaprl/refiner/refiner/refine.ml
+6 -12 metaprl/refiner/refiner/refine.mli
+1 -1 metaprl/refiner/reflib/dform.mli
+1 -1 metaprl/refiner/reflib/term_dtable.mli
+1 -1 metaprl/refiner/reflib/term_stable.mli
+1 -17 metaprl/refiner/refsig/refiner_sig.ml
+3 -15 metaprl/refiner/refsig/term_base_minimal_sig.ml
+2 -16 metaprl/refiner/refsig/term_base_sig.ml
+2 -30 metaprl/refiner/refsig/termmod_sig.ml
+4 -19 metaprl/refiner/rewrite/rewrite.ml
+1 -16 metaprl/refiner/rewrite/rewrite.mli
+1 -16 metaprl/refiner/rewrite/rewrite_build_contractum.ml
+1 -16 metaprl/refiner/rewrite/rewrite_build_contractum.mli
+1 -16 metaprl/refiner/rewrite/rewrite_compile_contractum.ml
+1 -16 metaprl/refiner/rewrite/rewrite_compile_contractum.mli
+1 -16 metaprl/refiner/rewrite/rewrite_compile_redex.ml
+1 -16 metaprl/refiner/rewrite/rewrite_compile_redex.mli
+1 -11 metaprl/refiner/rewrite/rewrite_debug.ml
+1 -11 metaprl/refiner/rewrite/rewrite_debug.mli
+1 -16 metaprl/refiner/rewrite/rewrite_match_redex.ml
+1 -16 metaprl/refiner/rewrite/rewrite_match_redex.mli
+1 -13 metaprl/refiner/rewrite/rewrite_meta.ml
+1 -13 metaprl/refiner/rewrite/rewrite_meta.mli
+1 -11 metaprl/refiner/rewrite/rewrite_util.ml
+1 -11 metaprl/refiner/rewrite/rewrite_util.mli
+1 -19 metaprl/refiner/term_ds/rob_ds.mli
+1 -19 metaprl/refiner/term_ds/term_addr_ds.ml
+1 -19 metaprl/refiner/term_ds/term_addr_ds.mli
+1 -18 metaprl/refiner/term_ds/term_base_ds.ml
+1 -20 metaprl/refiner/term_ds/term_base_ds.mli
+2 -19 metaprl/refiner/term_ds/term_ds_sig.ml
+1 -14 metaprl/refiner/term_ds/term_eval_ds.ml
+5 -18 metaprl/refiner/term_ds/term_eval_ds.mli
+8 -26 metaprl/refiner/term_ds/term_man_ds.ml
+8 -26 metaprl/refiner/term_ds/term_man_ds.mli
+1 -19 metaprl/refiner/term_ds/term_op_ds.ml
+1 -19 metaprl/refiner/term_ds/term_op_ds.mli
+1 -20 metaprl/refiner/term_ds/term_subst_ds.ml
+5 -24 metaprl/refiner/term_ds/term_subst_ds.mli
+1 -6 metaprl/refiner/term_gen/term_addr_gen.ml
+5 -10 metaprl/refiner/term_gen/term_addr_gen.mli
+1 -15 metaprl/refiner/term_gen/term_man_gen.ml
+1 -15 metaprl/refiner/term_gen/term_man_gen.mli
+1 -8 metaprl/refiner/term_gen/term_meta_gen.ml
+5 -12 metaprl/refiner/term_gen/term_meta_gen.mli
+3 -10 metaprl/refiner/term_gen/term_shape_gen.ml
+3 -10 metaprl/refiner/term_gen/term_shape_gen.mli
+1 -16 metaprl/refiner/term_std/term_base_std.ml
+1 -17 metaprl/refiner/term_std/term_base_std.mli
+2 -15 metaprl/refiner/term_std/term_eval_std.ml
+5 -18 metaprl/refiner/term_std/term_eval_std.mli
+1 -14 metaprl/refiner/term_std/term_op_std.ml
+5 -18 metaprl/refiner/term_std/term_op_std.mli
+2 -16 metaprl/refiner/term_std/term_std_sig.ml
+1 -14 metaprl/refiner/term_std/term_subst_std.ml
+5 -18 metaprl/refiner/term_std/term_subst_std.mli
+1 -1 metaprl/support/display/perv.mli
+1 -1 metaprl/support/shell/browser_resource.mli
+1 -1 metaprl/support/shell/session.mli
+1 -1 metaprl/support/shell/session_sig.mlz
+1 -1 metaprl/support/tactics/auto_tactic.mli
+1 -1 metaprl/support/tactics/simp_typeinf.mli
+1 -1 metaprl/support/tactics/typeinf.mli
+1 -1 metaprl/support/tactics/var.mli
+1 -1 metaprl/theories/czf/czf_itt_member.mli
+1 -1 metaprl/theories/czf/czf_itt_nat.mli
+1 -1 metaprl/theories/czf/czf_itt_set.mli
+1 -1 metaprl/theories/experimental/compile/m_dead.ml
+1 -1 metaprl/theories/experimental/compile/m_dead.mli
+1 -1 metaprl/theories/experimental/compile/m_ir.mli
+1 -1 metaprl/theories/experimental/compile/m_ir_ast.ml
+1 -1 metaprl/theories/experimental/compile/m_prog.mli
+1 -1 metaprl/theories/experimental/compile/m_x86_spill.mli
+1 -1 metaprl/theories/experimental/compile/m_x86_term.mli
+1 -1 metaprl/theories/fir/mfir_termOp.mli
+1 -1 metaprl/theories/fir/mfir_termOp_base.mli
+1 -1 metaprl/theories/itt/itt_atom.mli
+1 -1 metaprl/theories/itt/itt_bool.mli
+1 -1 metaprl/theories/itt/itt_collection.mli
+1 -1 metaprl/theories/itt/itt_dfun.mli
+1 -1 metaprl/theories/itt/itt_disect.mli
+1 -1 metaprl/theories/itt/itt_dprod.mli
+1 -1 metaprl/theories/itt/itt_equal.mli
+1 -1 metaprl/theories/itt/itt_eta.mli
+1 -1 metaprl/theories/itt/itt_ext_equal.mli
+1 -1 metaprl/theories/itt/itt_int_ext.mli
+1 -1 metaprl/theories/itt/itt_isect.mli
+1 -1 metaprl/theories/itt/itt_list.mli
+1 -1 metaprl/theories/itt/itt_nat.mli
+1 -1 metaprl/theories/itt/itt_prec.mli
+1 -1 metaprl/theories/itt/itt_quotient.mli
+1 -1 metaprl/theories/itt/itt_record.mli
+1 -1 metaprl/theories/itt/itt_record_label.mli
+1 -1 metaprl/theories/itt/itt_record_label0.mli
+1 -1 metaprl/theories/itt/itt_record_renaming.mli
+1 -1 metaprl/theories/itt/itt_relation_str.mli
+1 -1 metaprl/theories/itt/itt_rfun.mli
+1 -1 metaprl/theories/itt/itt_set.mli
+1 -1 metaprl/theories/itt/itt_squash.mli
+1 -1 metaprl/theories/itt/itt_squiggle.mli
+1 -1 metaprl/theories/itt/itt_srec.mli
+1 -1 metaprl/theories/itt/itt_struct.mli
+1 -1 metaprl/theories/itt/itt_struct2.mli
+3 -4 metaprl/theories/itt/itt_subset.mli
+1 -1 metaprl/theories/itt/itt_subtype.mli
+1 -1 metaprl/theories/itt/itt_union.mli
+1 -1 metaprl/theories/itt/itt_unit.mli
+1 -1 metaprl/theories/itt/itt_void.mli
+1 -1 metaprl/theories/itt/itt_w.mli