fixed dependency problems with the checker

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10970 85f007b7-540e-0410-9357-904b9bb8a0f7

3 files changed, 186 insertions, 8 deletions

diff --git a/Makefile.build b/Makefile.build
index 759b461d8..a5c6d6e5b 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -895,14 +895,6 @@ endif
 	$(HIDE)echo "let keep_ocamldep_happy Do_not_compile_me = assert false" > $*.ml
 #End critical section
 
-%.ml.d: $(D_DEPEND_BEFORE_SRC) %.ml $(D_DEPEND_AFTER_SRC) $(GENFILES) $(ML4FILES:.ml4=.ml)
-	$(SHOW)'OCAMLDEP  $<'
-	$(HIDE)$(OCAMLDEP) $(DEPFLAGS) $< > "$@"
-
-%.mli.d: $(D_DEPEND_BEFORE_SRC) %.mli $(D_DEPEND_AFTER_SRC) $(GENFILES) $(ML4FILES:.ml4=.ml)
-	$(SHOW)'OCAMLDEP  $<'
-	$(HIDE)$(OCAMLDEP) $(DEPFLAGS) $< > "$@"
-
 checker/%.ml.d: $(D_DEPEND_BEFORE_SRC) checker/%.ml $(D_DEPEND_AFTER_SRC)
 	$(SHOW)'OCAMLDEP  $<'
 	$(HIDE)$(OCAMLDEP) -slash $(LOCALCHKLIBS) $< > "$@"
@@ -911,6 +903,14 @@ checker/%.mli.d: $(D_DEPEND_BEFORE_SRC) checker/%.mli $(D_DEPEND_AFTER_SRC)
 	$(SHOW)'OCAMLDEP  $<'
 	$(HIDE)$(OCAMLDEP) -slash $(LOCALCHKLIBS) $< > "$@"
 
+%.ml.d: $(D_DEPEND_BEFORE_SRC) %.ml $(D_DEPEND_AFTER_SRC) $(GENFILES) $(ML4FILES:.ml4=.ml)
+	$(SHOW)'OCAMLDEP  $<'
+	$(HIDE)$(OCAMLDEP) $(DEPFLAGS) $< > "$@"
+
+%.mli.d: $(D_DEPEND_BEFORE_SRC) %.mli $(D_DEPEND_AFTER_SRC) $(GENFILES) $(ML4FILES:.ml4=.ml)
+	$(SHOW)'OCAMLDEP  $<'
+	$(HIDE)$(OCAMLDEP) $(DEPFLAGS) $< > "$@"
+
 ## Veerry nasty hack to keep ocamldep happy
 %.ml: | %.ml4
 	$(SHOW)'TOUCH     $@'
diff --git a/checker/environ.mli b/checker/environ.mli
new file mode 100644
index 000000000..a3f531dd0
--- /dev/null
+++ b/checker/environ.mli
@@ -0,0 +1,67 @@
+open Names
+open Term
+
+type globals = {
+  env_constants : Declarations.constant_body Cmap.t;
+  env_inductives : Declarations.mutual_inductive_body KNmap.t;
+  env_modules : Declarations.module_body MPmap.t;
+  env_modtypes : Declarations.module_type_body MPmap.t;
+  env_alias : module_path MPmap.t;
+}
+type stratification = {
+  env_universes : Univ.universes;
+  env_engagement : Declarations.engagement option;
+}
+type env = {
+  env_globals : globals;
+  env_named_context : named_context;
+  env_rel_context : rel_context;
+  env_stratification : stratification;
+  env_imports : Digest.t MPmap.t;
+}
+val empty_env : env
+val engagement : env -> Declarations.engagement option
+val universes : env -> Univ.universes
+val named_context : env -> named_context
+val rel_context : env -> rel_context
+val set_engagement : Declarations.engagement -> env -> env
+
+val add_digest : env -> dir_path -> Digest.t -> env
+val lookup_digest : env -> dir_path -> Digest.t
+
+val lookup_rel : int -> env -> rel_declaration
+val push_rel : rel_declaration -> env -> env
+val push_rel_context : rel_context -> env -> env
+val push_rec_types : name array * constr array * 'a -> env -> env
+
+val push_named : named_declaration -> env -> env
+val lookup_named : identifier -> env -> named_declaration
+val named_type : identifier -> env -> constr
+
+val add_constraints : Univ.constraints -> env -> env
+
+val lookup_constant : constant -> env -> Declarations.constant_body
+val add_constant : constant -> Declarations.constant_body -> env -> env
+val constant_type : env -> constant -> Declarations.constant_type
+type const_evaluation_result = NoBody | Opaque
+exception NotEvaluableConst of const_evaluation_result
+val constant_value : env -> constant -> constr
+val constant_opt_value : env -> constant -> constr option
+val evaluable_constant : constant -> env -> bool
+
+val lookup_mind :
+  mutual_inductive -> env -> Declarations.mutual_inductive_body
+val scrape_mind : env -> mutual_inductive -> mutual_inductive
+val add_mind :
+  mutual_inductive -> Declarations.mutual_inductive_body -> env -> env
+val mind_equiv : env -> inductive -> inductive -> bool
+
+val add_modtype :
+  module_path -> Declarations.module_type_body -> env -> env
+val shallow_add_module :
+  module_path -> Declarations.module_body -> env -> env
+val register_alias : module_path -> module_path -> env -> env
+val scrape_alias : module_path -> env -> module_path
+val lookup_module : module_path -> env -> Declarations.module_body
+val lookup_modtype : module_path -> env -> Declarations.module_type_body
+val lookup_alias : module_path -> env -> module_path
diff --git a/checker/term.mli b/checker/term.mli
new file mode 100644
index 000000000..30a2c03a5
--- /dev/null
+++ b/checker/term.mli
@@ -0,0 +1,111 @@
+open Names
+
+type existential_key = int
+type metavariable = int
+type case_style =
+    LetStyle
+  | IfStyle
+  | LetPatternStyle
+  | MatchStyle
+  | RegularStyle
+type case_printing = { ind_nargs : int; style : case_style; }
+type case_info = {
+  ci_ind : inductive;
+  ci_npar : int;
+  ci_cstr_nargs : int array;
+  ci_pp_info : case_printing;
+}
+type contents = Pos | Null
+type sorts = Prop of contents | Type of Univ.universe
+type sorts_family = InProp | InSet | InType
+val family_of_sort : sorts -> sorts_family
+type 'a pexistential = existential_key * 'a array
+type 'a prec_declaration = name array * 'a array * 'a array
+type 'a pfixpoint = (int array * int) * 'a prec_declaration
+type 'a pcofixpoint = int * 'a prec_declaration
+type cast_kind = VMcast | DEFAULTcast
+type constr =
+    Rel of int
+  | Var of identifier
+  | Meta of metavariable
+  | Evar of constr pexistential
+  | Sort of sorts
+  | Cast of constr * cast_kind * constr
+  | Prod of name * constr * constr
+  | Lambda of name * constr * constr
+  | LetIn of name * constr * constr * constr
+  | App of constr * constr array
+  | Const of constant
+  | Ind of inductive
+  | Construct of constructor
+  | Case of case_info * constr * constr * constr array
+  | Fix of constr pfixpoint
+  | CoFix of constr pcofixpoint
+type existential = constr pexistential
+type rec_declaration = constr prec_declaration
+type fixpoint = constr pfixpoint
+type cofixpoint = constr pcofixpoint
+val strip_outer_cast : constr -> constr
+val collapse_appl : constr -> constr
+val decompose_app : constr -> constr * constr list
+val applist : constr * constr list -> constr
+val iter_constr_with_binders :
+  ('a -> 'a) -> ('a -> constr -> unit) -> 'a -> constr -> unit
+exception LocalOccur
+val closedn : int -> constr -> bool
+val closed0 : constr -> bool
+val noccurn : int -> constr -> bool
+val noccur_between : int -> int -> constr -> bool
+val noccur_with_meta : int -> int -> constr -> bool
+val map_constr_with_binders :
+  ('a -> 'a) -> ('a -> constr -> constr) -> 'a -> constr -> constr
+val exliftn : Esubst.lift -> constr -> constr
+val liftn : int -> int -> constr -> constr
+val lift : int -> constr -> constr
+type info = Closed | Open | Unknown
+type 'a substituend = { mutable sinfo : info; sit : 'a; }
+val lift_substituend : int -> constr substituend -> constr
+val make_substituend : 'a -> 'a substituend
+val substn_many : constr substituend array -> int -> constr -> constr
+val substnl : constr list -> int -> constr -> constr
+val substl : constr list -> constr -> constr
+val subst1 : constr -> constr -> constr
+
+type named_declaration = identifier * constr option * constr
+type rel_declaration = name * constr option * constr
+val map_named_declaration :
+  (constr -> constr) -> named_declaration -> named_declaration
+val map_rel_declaration :
+  (constr -> constr) -> rel_declaration -> rel_declaration
+val fold_named_declaration :
+  (constr -> 'a -> 'a) -> named_declaration -> 'a -> 'a
+val fold_rel_declaration :
+  (constr -> 'a -> 'a) -> rel_declaration -> 'a -> 'a
+type named_context = named_declaration list
+val empty_named_context : named_context
+val fold_named_context :
+  (named_declaration -> 'a -> 'a) -> named_context -> init:'a -> 'a
+type section_context = named_context
+type rel_context = rel_declaration list
+val empty_rel_context : rel_context
+val rel_context_length : rel_context -> int
+val rel_context_nhyps : rel_context -> int
+val fold_rel_context :
+  (rel_declaration -> 'a -> 'a) -> rel_context -> init:'a -> 'a
+val map_context : (constr -> constr) -> named_context -> named_context
+val map_rel_context : (constr -> constr) -> rel_context -> rel_context
+val extended_rel_list : int -> rel_context -> constr list
+val compose_lam : (name * constr) list -> constr -> constr
+val decompose_lam : constr -> (name * constr) list * constr
+val decompose_lam_n_assum : int -> constr -> rel_context * constr
+val mkProd_or_LetIn : name * constr option * constr -> constr -> constr
+val it_mkProd_or_LetIn : constr -> rel_context -> constr
+val decompose_prod_assum : constr -> rel_context * constr
+val decompose_prod_n_assum : int -> constr -> rel_context * constr
+
+type arity = rel_context * sorts
+val mkArity : arity -> constr
+val destArity : constr -> arity
+val isArity : constr -> bool
+val compare_constr : (constr -> constr -> bool) -> constr -> constr -> bool
+val eq_constr : constr -> constr -> bool