Imported Upstream version 8.5~beta1+dfsg

1 files changed, 64 insertions, 95 deletions

diff --git a/checker/modops.ml b/checker/modops.ml
index 11793af9..8ccf118d 100644
--- a/checker/modops.ml
+++ b/checker/modops.ml
@@ -1,126 +1,111 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
 (*i*)
+open Errors
 open Util
 open Pp
 open Names
-open Univ
-open Term
+open Cic
 open Declarations
-open Environ
 (*i*)
 
 let error_not_a_constant l =
-  error ("\""^(string_of_label l)^"\" is not a constant")
+  error ("\""^(Label.to_string l)^"\" is not a constant")
 
-let error_not_a_functor _ = error "Application of not a functor"
+let error_not_a_functor () = error "Application of not a functor"
 
 let error_incompatible_modtypes _ _ = error "Incompatible module types"
 
 let error_not_match l _ =
-  error ("Signature components for label "^string_of_label l^" do not match")
+  error ("Signature components for label "^Label.to_string l^" do not match")
 
-let error_no_such_label l = error ("No such label "^string_of_label l)
+let error_no_such_label l = error ("No such label "^Label.to_string l)
 
 let error_no_such_label_sub l l1 =
   let l1 = string_of_mp l1 in
   error ("The field "^
-         string_of_label l^" is missing in "^l1^".")
+         Label.to_string l^" is missing in "^l1^".")
 
 let error_not_a_module_loc loc s =
-  user_err_loc (loc,"",str ("\""^string_of_label s^"\" is not a module"))
+  user_err_loc (loc,"",str ("\""^Label.to_string s^"\" is not a module"))
 
-let error_not_a_module s = error_not_a_module_loc dummy_loc s
+let error_not_a_module s = error_not_a_module_loc Loc.ghost s
 
-let error_with_incorrect l =
-  error ("Incorrect constraint for label \""^(string_of_label l)^"\"")
+let error_with_module () =
+  error "Unsupported 'with' constraint in module implementation"
 
-let error_a_generative_module_expected l =
-  error ("The module " ^ string_of_label l ^ " is not generative. Only " ^
-         "component of generative modules can be changed using the \"with\" " ^
-         "construct.")
+let is_functor = function
+  | MoreFunctor _ -> true
+  | NoFunctor _ -> false
 
-let error_signature_expected mtb =
-  error "Signature expected"
+let destr_functor = function
+  | MoreFunctor (arg_id,arg_t,body_t) -> (arg_id,arg_t,body_t)
+  | NoFunctor _ -> error_not_a_functor ()
 
-let error_application_to_not_path _ = error "Application to not path"
+let module_body_of_type mp mtb =
+  { mtb with mod_mp = mp; mod_expr = Abstract }
 
-let destr_functor env mtb =
-  match mtb with
-  | SEBfunctor (arg_id,arg_t,body_t) ->
-      	    (arg_id,arg_t,body_t)
-  | _ -> error_not_a_functor mtb
-
-let module_body_of_type mp mtb = 
-  { mod_mp = mp;
-    mod_type = mtb.typ_expr;
-    mod_type_alg = mtb.typ_expr_alg;
-    mod_expr = None;
-    mod_constraints = mtb.typ_constraints;
-    mod_delta = mtb.typ_delta;
-    mod_retroknowledge = []}
-
-let rec add_signature mp sign resolver env = 
+let rec add_structure mp sign resolver env =
   let add_one env (l,elem) =
-    let kn = make_kn mp empty_dirpath l in
-    let con = constant_of_kn kn in
-    let mind = mind_of_delta resolver (mind_of_kn kn) in
+    let kn = KerName.make2 mp l in
+    let con = Constant.make1 kn in
+    let mind = mind_of_delta resolver (MutInd.make1 kn) in
       match elem with
-	| SFBconst cb -> 
+	| SFBconst cb ->
 	   (* let con =  constant_of_delta resolver con in*)
 	      Environ.add_constant con cb env
-	| SFBmind mib -> 
+	| SFBmind mib ->
 	   (* let mind =  mind_of_delta resolver mind in*)
 	    Environ.add_mind mind mib env
 	| SFBmodule mb -> add_module mb env
 	      (* adds components as well *)
-	| SFBmodtype mtb -> Environ.add_modtype mtb.typ_mp mtb env
+	| SFBmodtype mtb -> Environ.add_modtype mtb.mod_mp mtb env
   in
-    List.fold_left add_one env sign
+  List.fold_left add_one env sign
 
-and add_module mb env = 
+and add_module mb env =
   let mp = mb.mod_mp in
   let env = Environ.shallow_add_module mp mb env in
-    match mb.mod_type with
-      | SEBstruct (sign) -> 
-	    add_signature mp sign mb.mod_delta env
-      | SEBfunctor _ -> env
-      | _ -> anomaly "Modops:the evaluation of the structure failed "
+  match mb.mod_type with
+  | NoFunctor struc -> add_structure mp struc mb.mod_delta env
+  | MoreFunctor _ -> env
 
+let add_module_type mp mtb env = add_module (module_body_of_type mp mtb) env
 
 let strengthen_const mp_from l cb resolver =
   match cb.const_body with
     | Def _ -> cb
     | _ ->
-      let con = make_con mp_from empty_dirpath l in
+      let con = Constant.make2 mp_from l in
       (* let con =  constant_of_delta resolver con in*)
-      { cb with const_body = Def (Declarations.from_val (Const con)) }
+      let u = 
+	if cb.const_polymorphic then Univ.UContext.instance cb.const_universes 
+	else Univ.Instance.empty
+      in
+      { cb with const_body = Def (Declarations.from_val (Const (con,u))) }
 
 let rec strengthen_mod mp_from mp_to mb =
-  if Declarations.mp_in_delta mb.mod_mp mb.mod_delta then
-    mb
-  else
-    match mb.mod_type with
-     | SEBstruct (sign) -> 
-	 let resolve_out,sign_out = 
-	   strengthen_sig mp_from sign mp_to mb.mod_delta in
-	   { mb with
-	       mod_expr = Some (SEBident mp_to);
-	       mod_type = SEBstruct(sign_out);
-	       mod_type_alg = mb.mod_type_alg;
-	       mod_constraints = mb.mod_constraints;
-	       mod_delta = resolve_out(*add_mp_delta_resolver mp_from mp_to 
-	       (add_delta_resolver mb.mod_delta resolve_out)*);
-	       mod_retroknowledge = mb.mod_retroknowledge}
-     | SEBfunctor _ -> mb
-     | _ -> anomaly "Modops:the evaluation of the structure failed "
-	 
+  if Declarations.mp_in_delta mb.mod_mp mb.mod_delta then mb
+  else strengthen_body true mp_from mp_to mb
+
+and strengthen_body is_mod mp_from mp_to mb =
+  match mb.mod_type with
+  | MoreFunctor _ -> mb
+  | NoFunctor sign ->
+    let resolve_out,sign_out = strengthen_sig mp_from sign mp_to mb.mod_delta
+    in
+    { mb with
+      mod_expr =
+        (if is_mod then Algebraic (NoFunctor (MEident mp_to)) else Abstract);
+      mod_type = NoFunctor sign_out;
+      mod_delta = resolve_out }
+
 and strengthen_sig mp_from sign mp_to resolver =
   match sign with
     | [] -> empty_delta_resolver,[]
@@ -139,39 +124,23 @@ and strengthen_sig mp_from sign mp_to resolver =
 	let resolve_out,rest' = strengthen_sig mp_from rest mp_to resolver in
 	resolve_out (*add_delta_resolver resolve_out mb.mod_delta*),
 	item':: rest'
-    | (l,SFBmodtype mty as item) :: rest -> 
+    | (l,SFBmodtype mty as item) :: rest ->
 	let resolve_out,rest' = strengthen_sig mp_from rest mp_to resolver in
 	resolve_out,item::rest'
 
 let strengthen mtb mp =
-    match mtb.typ_expr with
-      | SEBstruct (sign) -> 
-	  let resolve_out,sign_out =
-	    strengthen_sig mtb.typ_mp sign mp mtb.typ_delta in
-	    {mtb with
-	       typ_expr = SEBstruct(sign_out);
-	       typ_delta = resolve_out(*add_delta_resolver mtb.typ_delta
-		(add_mp_delta_resolver mtb.typ_mp mp resolve_out)*)}
-      | SEBfunctor _ -> mtb
-      | _ -> anomaly "Modops:the evaluation of the structure failed "
+  strengthen_body false mtb.mod_mp mp mtb
 
 let subst_and_strengthen mb mp =
   strengthen_mod mb.mod_mp mp (subst_module (map_mp mb.mod_mp mp) mb)
 
-
 let module_type_of_module mp mb =
+  let mtb =
+    { mb with
+      mod_expr = Abstract;
+      mod_type_alg = None;
+      mod_retroknowledge = [] }
+  in
   match mp with
-      Some mp ->
-	strengthen {
-	  typ_mp = mp;
-	  typ_expr = mb.mod_type;
-	  typ_expr_alg = None;
-	  typ_constraints = mb.mod_constraints;
-	  typ_delta = mb.mod_delta} mp
-	  
-    | None ->
-	{typ_mp = mb.mod_mp;
-	 typ_expr = mb.mod_type;
-	 typ_expr_alg = None;
-	 typ_constraints = mb.mod_constraints;
-	 typ_delta = mb.mod_delta}
+  | Some mp -> strengthen {mtb with mod_mp = mp} mp
+  | None -> mtb