Checker: empty sections hardcoded in cb and mind

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

11 files changed, 31 insertions, 91 deletions

diff --git a/checker/cic.mli b/checker/cic.mli
index e72563c7d..b125e3c72 100644
--- a/checker/cic.mli
+++ b/checker/cic.mli
@@ -104,17 +104,12 @@ type cofixpoint = constr pcofixpoint
 
 (** {6 Type of assumptions and contexts}  *)
 
-type named_declaration = Id.t * constr option * constr
 type rel_declaration = Name.t * constr option * constr
-
 type rel_context = rel_declaration list
 
-
-(*************************************************************************)
-(** {4 From sign.ml} *)
-
-type named_context = named_declaration list
-type section_context = named_context
+(** The declarations below in .vo should be outside sections,
+    so we expect there a value compatible with an empty list *)
+type section_context = unit
 
 
 (*************************************************************************)
diff --git a/checker/declarations.ml b/checker/declarations.ml
index 886901e1a..58a5f2602 100644
--- a/checker/declarations.ml
+++ b/checker/declarations.ml
@@ -491,7 +491,6 @@ let subst_arity sub = function
 (* NB: we leave bytecode and native code fields untouched *)
 let subst_const_body sub cb =
  { cb with
-    const_hyps = (assert (List.is_empty cb.const_hyps); []);
     const_body = subst_constant_def sub cb.const_body;
     const_type = subst_arity sub cb.const_type }
 
@@ -507,7 +506,7 @@ let subst_mind_packet sub mbp =
   { mind_consnames = mbp.mind_consnames;
     mind_consnrealdecls = mbp.mind_consnrealdecls;
     mind_typename = mbp.mind_typename;
-   mind_nf_lc = Array.smartmap (subst_mps sub) mbp.mind_nf_lc;
+    mind_nf_lc = Array.smartmap (subst_mps sub) mbp.mind_nf_lc;
     mind_arity_ctxt = subst_rel_context sub mbp.mind_arity_ctxt;
     mind_arity = subst_arity sub mbp.mind_arity;
     mind_user_lc = Array.smartmap (subst_mps sub) mbp.mind_user_lc;
@@ -521,17 +520,9 @@ let subst_mind_packet sub mbp =
 
 
 let subst_mind sub mib =
-  { mind_record = mib.mind_record ;
-    mind_finite = mib.mind_finite ;
-    mind_ntypes = mib.mind_ntypes ;
-    mind_hyps = (assert (List.is_empty mib.mind_hyps); []) ;
-    mind_nparams = mib.mind_nparams;
-    mind_nparams_rec = mib.mind_nparams_rec;
-    mind_params_ctxt =
-      map_rel_context (subst_mps sub) mib.mind_params_ctxt;
-    mind_packets = Array.smartmap (subst_mind_packet sub) mib.mind_packets ;
-    mind_constraints = mib.mind_constraints;
-    mind_native_name = mib.mind_native_name}
+  { mib with
+    mind_params_ctxt = map_rel_context (subst_mps sub) mib.mind_params_ctxt;
+    mind_packets = Array.smartmap (subst_mind_packet sub) mib.mind_packets }
 
 (* Modules *)
 
diff --git a/checker/environ.mli b/checker/environ.mli
index 4165f0bcf..3cd4ca6e0 100644
--- a/checker/environ.mli
+++ b/checker/environ.mli
@@ -1,6 +1,6 @@
 open Names
 open Cic
-
+open Term
 
 (* Environments *)
 
diff --git a/checker/indtypes.ml b/checker/indtypes.ml
index 69e16386e..c26349207 100644
--- a/checker/indtypes.ml
+++ b/checker/indtypes.ml
@@ -535,9 +535,6 @@ let check_inductive env kn mib =
   (* check mind_ntypes *)
   if Array.length mib.mind_packets <> mib.mind_ntypes then
     error "not the right number of packets";
-  (* check mind_hyps: should be empty *)
-  if mib.mind_hyps <> empty_named_context then
-    error "section context not empty";
   (* check mind_params_ctxt *)
   let params = mib.mind_params_ctxt in
   let _ = check_ctxt env params in
diff --git a/checker/mod_checking.ml b/checker/mod_checking.ml
index 089414f63..66f1194d3 100644
--- a/checker/mod_checking.ml
+++ b/checker/mod_checking.ml
@@ -28,15 +28,14 @@ let refresh_arity ar =
 let check_constant_declaration env kn cb =
   Flags.if_verbose ppnl (str "  checking cst: " ++ prcon kn);
 (*  let env = add_constraints cb.const_constraints env in*)
-  let env' = check_named_ctxt env cb.const_hyps in
   (match cb.const_type with
       NonPolymorphicType ty ->
         let ty, cu = refresh_arity ty in
-        let envty = add_constraints cu env' in
+        let envty = add_constraints cu env in
         let _ = infer_type envty ty in
         (match body_of_constant cb with
           | Some bd ->
-              let j = infer env' bd in
+              let j = infer env bd in
               conv_leq envty j ty
           | None -> ())
     | PolymorphicArity(ctxt,par) ->
@@ -110,7 +109,6 @@ let check_definition_sub env cb1 cb2 =
         (t1,t2) in
     Reduction.conv_leq env t1 t2
   in
-  assert (cb1.const_hyps=[] && cb2.const_hyps=[]) ;
   (*Start by checking types*)
   let typ1 = Typeops.type_of_constant_type env cb1.const_type in
   let typ2 = Typeops.type_of_constant_type env cb2.const_type in
diff --git a/checker/subtyping.ml b/checker/subtyping.ml
index 609918495..150e99bc9 100644
--- a/checker/subtyping.ml
+++ b/checker/subtyping.ml
@@ -154,7 +154,6 @@ let check_inductive  env mp1 l info1 mib2 spec2 subst1 subst2=
   let check f = if f mib1 <> f mib2 then error () in
   check (fun mib -> mib.mind_finite);
   check (fun mib -> mib.mind_ntypes);
-  assert (mib1.mind_hyps=[] && mib2.mind_hyps=[]);
   assert (Array.length mib1.mind_packets >= 1
 	    && Array.length mib2.mind_packets >= 1);
 
@@ -248,7 +247,6 @@ let check_constant env mp1 l info1 cb2 spec2 subst1 subst2 =
   in
     match info1 with
       | Constant cb1 ->
-	assert (cb1.const_hyps=[] && cb2.const_hyps=[]) ;
 	let cb1 = subst_const_body subst1 cb1 in
 	let cb2 = subst_const_body subst2 cb2 in
 	(*Start by checking types*)
@@ -278,7 +276,6 @@ let check_constant env mp1 l info1 cb2 spec2 subst1 subst2 =
 		      "instantiated by an inductive type. Hint: you can rename the " ^
 		      "inductive type and give a definition to map the old name to the new " ^
 		      "name."));
-      assert (mind1.mind_hyps=[] && cb2.const_hyps=[]) ;
       if constant_has_body cb2 then error () ;
       let arity1 = type_of_inductive env (mind1,mind1.mind_packets.(i)) in
       let typ2 = Typeops.type_of_constant_type env cb2.const_type in
@@ -289,7 +286,6 @@ let check_constant env mp1 l info1 cb2 spec2 subst1 subst2 =
        "instantiated by a constructor. Hint: you can rename the " ^
        "constructor and give a definition to map the old name to the new " ^
        "name."));
-      assert (mind1.mind_hyps=[] && cb2.const_hyps=[]) ;
       if constant_has_body cb2 then error () ;
       let ty1 = type_of_constructor cstr (mind1,mind1.mind_packets.(i)) in
       let ty2 = Typeops.type_of_constant_type env cb2.const_type in
diff --git a/checker/term.ml b/checker/term.ml
index b52f08cfa..a3c9225f5 100644
--- a/checker/term.ml
+++ b/checker/term.ml
@@ -209,6 +209,9 @@ let subst1 lam = substl [lam]
 (*     Type of assumptions and contexts                                    *)
 (***************************************************************************)
 
+type named_declaration = Id.t * constr option * constr
+type named_context = named_declaration list
+
 let empty_named_context = []
 let fold_named_context f l ~init = List.fold_right f l init
 
diff --git a/checker/term.mli b/checker/term.mli
index 127fc113d..7316b18e5 100644
--- a/checker/term.mli
+++ b/checker/term.mli
@@ -29,9 +29,12 @@ val substnl : constr list -> int -> constr -> constr
 val substl : constr list -> constr -> constr
 val subst1 : constr -> constr -> constr
 
+type named_declaration = Id.t * constr option * constr
+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
+
 val empty_rel_context : rel_context
 val rel_context_length : rel_context -> int
 val rel_context_nhyps : rel_context -> int
diff --git a/checker/typeops.ml b/checker/typeops.ml
index 3c6fa7c04..7ff99bd93 100644
--- a/checker/typeops.ml
+++ b/checker/typeops.ml
@@ -71,26 +71,6 @@ let judge_of_variable env id =
   with Not_found ->
     error_unbound_var env id
 
-(* Management of context of variables. *)
-
-(* Checks if a context of variable can be instantiated by the
-   variables of the current env *)
-(* TODO: check order? *)
-let check_hyps_inclusion env sign =
-  fold_named_context
-    (fun (id,_,ty1) () ->
-      let ty2 = named_type id env in
-      if not (eq_constr ty2 ty1) then
-        error "types do not match")
-    sign
-    ~init:()
-
-
-let check_args env c hyps =
-  try check_hyps_inclusion env hyps
-  with UserError _ | Not_found ->
-    error_reference_variables env c
-
 (* Type of constants *)
 
 let type_of_constant_knowing_parameters env t paramtyps =
@@ -105,12 +85,11 @@ let type_of_constant_type env t =
   type_of_constant_knowing_parameters env t [||]
 
 let judge_of_constant_knowing_parameters env cst paramstyp =
-  let c = Const cst in
   let cb =
     try lookup_constant cst env
     with Not_found ->
-      failwith ("Cannot find constant: "^string_of_con cst) in
-  let _ = check_args env c cb.const_hyps in
+      failwith ("Cannot find constant: "^string_of_con cst)
+  in
   type_of_constant_knowing_parameters env cb.const_type paramstyp
 
 let judge_of_constant env cst =
@@ -190,12 +169,11 @@ let judge_of_cast env (c,cj) k tj =
    dynamic constraints of the form u<=v are enforced *)
 
 let judge_of_inductive_knowing_parameters env ind (paramstyp:constr array) =
-  let c = Ind ind in
   let (mib,mip) =
     try lookup_mind_specif env ind
     with Not_found ->
-      failwith ("Cannot find inductive: "^string_of_mind (fst ind)) in
-  check_args env c mib.mind_hyps;
+      failwith ("Cannot find inductive: "^string_of_mind (fst ind))
+  in
   type_of_inductive_knowing_parameters env mip paramstyp
 
 let judge_of_inductive env ind =
@@ -204,15 +182,12 @@ let judge_of_inductive env ind =
 (* Constructors. *)
 
 let judge_of_constructor env c =
-  let constr = Construct c in
-  let _ =
-    let ((kn,_),_) = c in
-    let mib =
-      try lookup_mind kn env
-      with Not_found ->
-        failwith ("Cannot find inductive: "^string_of_mind (fst (fst c))) in
-    check_args env constr mib.mind_hyps in
-  let specif = lookup_mind_specif env (inductive_of_constructor c) in
+  let ind = inductive_of_constructor c in
+  let specif =
+    try lookup_mind_specif env ind
+    with Not_found ->
+      failwith ("Cannot find inductive: "^string_of_mind (fst ind))
+  in
   type_of_constructor c specif
 
 (* Case. *)
@@ -391,24 +366,6 @@ let check_ctxt env rels =
           push_rel d env)
     rels ~init:env
 
-let check_named_ctxt env ctxt =
-  fold_named_context (fun (id,_,_ as d) env ->
-    let _ =
-      try
-        let _ = lookup_named id env in
-        failwith ("variable "^Id.to_string id^" defined twice")
-      with Not_found -> () in
-    match d with
-        (_,None,ty) ->
-          let _ = infer_type env ty in
-          push_named d env
-      | (_,Some bd,ty) ->
-          let j1 = infer env bd in
-          let _ = infer env ty in
-          conv_leq env j1 ty;
-          push_named d env)
-    ctxt ~init:env
-
 (* Polymorphic arities utils *)
 
 let check_kind env ar u =
diff --git a/checker/typeops.mli b/checker/typeops.mli
index 5e71ec77f..3c56c15ef 100644
--- a/checker/typeops.mli
+++ b/checker/typeops.mli
@@ -9,6 +9,7 @@
 (*i*)
 open Names
 open Cic
+open Term
 open Environ
 (*i*)
 
@@ -17,7 +18,6 @@ open Environ
 val infer      : env -> constr      -> constr
 val infer_type : env -> constr      -> sorts
 val check_ctxt : env -> rel_context -> env
-val check_named_ctxt : env -> named_context -> env
 val check_polymorphic_arity :
   env -> rel_context -> polymorphic_arity -> unit
 
diff --git a/checker/values.ml b/checker/values.ml
index 2e096e2a4..386f85365 100644
--- a/checker/values.ml
+++ b/checker/values.ml
@@ -128,11 +128,11 @@ and v_fix = Tuple ("pfixpoint", [|Tuple ("fix2",[|Array Int;Int|]);v_prec|])
 and v_cofix = Tuple ("pcofixpoint",[|Int;v_prec|])
 
 
-let v_ndecl = v_tuple "named_declaration" [|v_id;Opt v_constr;v_constr|]
 let v_rdecl = v_tuple "rel_declaration" [|v_name;Opt v_constr;v_constr|]
-let v_nctxt = List v_ndecl
 let v_rctxt = List v_rdecl
 
+let v_section_ctxt = v_enum "emptylist" 1
+
 
 (** kernel/mod_subst *)
 
@@ -181,7 +181,7 @@ let v_cst_def =
     [|[|Opt Int|]; [|v_cstr_subst|]; [|v_lazy_constr|]|]
 
 let v_cb = v_tuple "constant_body"
-  [|v_nctxt;
+  [|v_section_ctxt;
     v_cst_def;
     v_cst_type;
     Any;
@@ -225,7 +225,7 @@ let v_ind_pack = v_tuple "mutual_inductive_body"
     v_bool;
     v_bool;
     Int;
-    v_nctxt;
+    v_section_ctxt;
     Int;
     Int;
     v_rctxt;