Imported Upstream snapshot 8.3~beta0+13298

1 files changed, 143 insertions, 162 deletions

diff --git a/checker/mod_checking.ml b/checker/mod_checking.ml
index 24000591..23ba4893 100644
--- a/checker/mod_checking.ml
+++ b/checker/mod_checking.ml
@@ -31,7 +31,7 @@ let check_constant_declaration env kn cb =
   (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 cb.const_body with
           | Some bd ->
@@ -58,19 +58,15 @@ let rec list_split_assoc k rev_before = function
   | (k',b)::after when k=k' -> rev_before,b,after
   | h::tail -> list_split_assoc k (h::rev_before) tail
 
-let rec list_fold_map2 f e = function 
+let rec list_fold_map2 f e = function
   |  []  -> (e,[],[])
-  |  h::t -> 
+  |  h::t ->
        let e',h1',h2' = f e h in
        let e'',t1',t2' = list_fold_map2 f e' t in
 	 e'',h1'::t1',h2'::t2'
 
-
-let check_alias (s1:substitution) s2 =
-  if s1 <> s2 then failwith "Incorrect alias"
-
 let check_definition_sub env cb1 cb2 =
-  let check_type env t1 t2 = 
+  let check_type env t1 t2 =
 
     (* If the type of a constant is generated, it may mention
        non-variable algebraic universes that the general conversion
@@ -81,7 +77,7 @@ let check_definition_sub env cb1 cb2 =
        Gamma |- A |> T, Gamma |- A' |> T' and Gamma |- A=A' then T <= T').
        Hence they don't have to be checked again *)
 
-    let t1,t2 = 
+    let t1,t2 =
       if isArity t2 then
         let (ctx2,s2) = destArity t2 in
         match s2 with
@@ -135,38 +131,38 @@ let lookup_modtype mp env =
   with Not_found ->
     failwith ("Unknown module type: "^string_of_mp mp)
 
-
-let rec check_with env mtb with_decl = 
+let rec check_with env mtb with_decl mp=
   match with_decl with
-    | With_definition_body _ -> 
-	check_with_aux_def env mtb with_decl;
-	empty_subst
-    | With_module_body _ -> 
-	check_with_aux_mod env mtb with_decl
+    | With_definition_body _ ->
+	check_with_aux_def env mtb with_decl mp;
+	mtb
+    | With_module_body _ ->
+	check_with_aux_mod env mtb with_decl mp;
+	mtb
 
-and check_with_aux_def env mtb with_decl = 
-  let msid,sig_b = match (eval_struct env mtb) with 
-    | SEBstruct(msid,sig_b) ->
-	msid,sig_b
+and check_with_aux_def env mtb with_decl mp =
+  let sig_b = match mtb with
+    | SEBstruct(sig_b) ->
+	sig_b
     | _ -> error_signature_expected mtb
   in
-  let id,idl = match with_decl with 
-    | With_definition_body (id::idl,_) | With_module_body (id::idl,_,_,_) ->
+  let id,idl = match with_decl with
+    | With_definition_body (id::idl,_) | With_module_body (id::idl,_) ->
                                            id,idl
-    | With_definition_body ([],_) | With_module_body ([],_,_,_) -> assert false
+    | With_definition_body ([],_) | With_module_body ([],_) -> assert false
   in
   let l = label_of_id id in
     try
       let rev_before,spec,after = list_split_assoc l [] sig_b in
       let before = List.rev rev_before in
-      let env' = Modops.add_signature (MPself msid) before env in
+      let env' = Modops.add_signature mp before empty_delta_resolver env in
 	match with_decl with
           | With_definition_body ([],_) -> assert false
-	  | With_definition_body ([id],c) -> 
+	  | With_definition_body ([id],c) ->
 	      let cb = match spec with
 		  SFBconst cb -> cb
 		| _ -> error_not_a_constant l
-	      in 
+	      in
               check_definition_sub env' c cb
 	  | With_definition_body (_::_,_) ->
 	      let old = match spec with
@@ -179,9 +175,9 @@ and check_with_aux_def env mtb with_decl =
 			let new_with_decl = match with_decl with
 			    With_definition_body (_,c) ->
                               With_definition_body (idl,c)
-			  | With_module_body (_,c,t,cst) ->
-                              With_module_body (idl,c,t,cst) in 
-			  check_with_aux_def env' (type_of_mb env old) new_with_decl
+			  | With_module_body (_,c) ->
+                              With_module_body (idl,c) in
+			  check_with_aux_def env' old.mod_type new_with_decl (MPdot(mp,l))
                     | Some msb ->
 			error_a_generative_module_expected l
 		end
@@ -190,46 +186,35 @@ and check_with_aux_def env mtb with_decl =
 	Not_found -> error_no_such_label l
       | Reduction.NotConvertible -> error_with_incorrect l
 
-and check_with_aux_mod env mtb with_decl = 
-  let initmsid,msid,sig_b =
-    match eval_struct env mtb with 
-    | SEBstruct(msid,sig_b) ->
-        let msid'=(refresh_msid msid) in
-	msid,msid',(subst_signature_msid msid (MPself(msid')) sig_b)
+and check_with_aux_mod env mtb with_decl mp =
+  let sig_b =
+    match mtb with
+    | SEBstruct(sig_b) ->
+	sig_b
     | _ -> error_signature_expected mtb in
-  let id,idl = match with_decl with 
-    | With_definition_body (id::idl,_) | With_module_body (id::idl,_,_,_) ->
+  let id,idl = match with_decl with
+    | With_definition_body (id::idl,_) | With_module_body (id::idl,_) ->
         id,idl
-    | With_definition_body ([],_) | With_module_body ([],_,_,_) -> assert false
+    | With_definition_body ([],_) | With_module_body ([],_) -> assert false
   in
   let l = label_of_id id in
     try
       let rev_before,spec,after = list_split_assoc l [] sig_b in
       let before = List.rev rev_before in
       let rec mp_rec = function
-	| [] -> MPself initmsid
+	| [] -> mp
 	| i::r -> MPdot(mp_rec r,label_of_id i)
-      in 
-      let env' = Modops.add_signature (MPself msid) before env in
+      in
+      let env' = Modops.add_signature mp before empty_delta_resolver env in
 	match with_decl with
-          | With_module_body ([],_,_,_) -> assert false
-	  | With_module_body ([id], mp,_,_) ->
-	      let old,alias = match spec with
-		  SFBmodule msb -> Some msb,None
-		| SFBalias (mp',_,_) -> None,Some mp'
+          | With_module_body ([],_) -> assert false
+	  | With_module_body ([id], mp1) ->
+	      let _ = match spec with
+		  SFBmodule msb -> msb
 		| _ -> error_not_a_module l
 	      in
-	      let mtb' = lookup_modtype mp env' in
-	      let _ =
-		match old,alias with
-		    Some msb,None -> ()
-		  | None,Some mp' ->
-		      check_modpath_equiv env' mp mp'
-		  | _,_ ->
-		      anomaly "Mod_typing:no implementation and no alias"
-	      in
-		join (map_mp (mp_rec [id]) mp) mtb'.typ_alias
-        | With_module_body (_::_,mp,_,_) -> 
+	      let _ = (lookup_module mp1 env) in ()
+        | With_module_body (_::_,mp) ->
 	    let old = match spec with
 		SFBmodule msb -> msb
 	      | _ -> error_not_a_module l
@@ -238,14 +223,12 @@ and check_with_aux_mod env mtb with_decl =
 		match old.mod_expr with
                     None ->
                       let new_with_decl = match with_decl with
-			  With_definition_body (_,c) -> 
+			  With_definition_body (_,c) ->
 			    With_definition_body (idl,c)
-			| With_module_body (_,c,t,cst) ->
-                            With_module_body (idl,c,t,cst) in
-		      let sub =
-			check_with_aux_mod env' 
-			  (type_of_mb env old) new_with_decl in
-		      join (map_mp (mp_rec idl) mp) sub
+			| With_module_body (_,c) ->
+                            With_module_body (idl,c) in
+		 	check_with_aux_mod env'
+			  old.mod_type new_with_decl (MPdot(mp,l))
                   | Some msb ->
                       error_a_generative_module_expected l
               end
@@ -255,113 +238,111 @@ and check_with_aux_mod env mtb with_decl =
       | Reduction.NotConvertible -> error_with_incorrect l
 
 and check_module_type env mty =
-  if mty.typ_strength <> None then
-    failwith "strengthening of module types not supported";
-  let sub = check_modexpr env mty.typ_expr in
-  check_alias mty.typ_alias sub
+  let _ = check_modtype env mty.typ_expr mty.typ_mp in ()
 
-and check_module env mb =
-  let sub =
-    match mb.mod_expr, mb.mod_type with
-      | None, None -> 
-	  anomaly "Mod_typing.translate_module: empty type and expr in module entry"
-      | None, Some mtb -> check_modexpr env mtb
-
-      | Some mexpr, _ -> 
-	  let sub1 = check_modexpr env mexpr in
-	  (match mb.mod_type with
-	    | None ->  sub1
-	    | Some mte -> 
-		let sub2 = check_modexpr env mte in
-                check_subtypes env
-		  {typ_expr = mexpr;
-		   typ_strength = None;
-		   typ_alias = sub1;}
-		  {typ_expr = mte;
-		   typ_strength = None;
-		   typ_alias = sub2;};
-		sub2) in
-  check_alias mb.mod_alias sub
-
-and check_structure_field (s,env) mp lab = function
+							 
+and check_module env mp mb =
+  match mb.mod_expr, mb.mod_type with
+    | None,mtb -> 
+	let _ = check_modtype env mtb mb.mod_mp in ()
+    | Some mexpr, mtb when mtb==mexpr ->
+	let _ = check_modtype env mtb mb.mod_mp in ()
+    | Some mexpr, _ ->
+	let sign = check_modexpr env mexpr mb.mod_mp mb.mod_delta in
+	let _ = check_modtype env mb.mod_type mb.mod_mp mb.mod_delta in
+          check_subtypes env 
+	    {typ_mp=mp;
+	     typ_expr=sign;
+	     typ_expr_alg=None;
+	     typ_constraints=Univ.Constraint.empty;
+	     typ_delta = mb.mod_delta;}
+	    {typ_mp=mp;
+	     typ_expr=mb.mod_type;
+	     typ_expr_alg=None;
+	     typ_constraints=Univ.Constraint.empty;
+	     typ_delta = mb.mod_delta;};
+	  
+and check_structure_field env mp lab res = function
   | SFBconst cb ->
       let c = make_con mp empty_dirpath lab in
-      (s,check_constant_declaration env c cb)
+	check_constant_declaration env c cb
   | SFBmind mib ->
-      let kn = make_kn mp empty_dirpath lab in
-      (s,Indtypes.check_inductive env kn mib)
+      let kn = make_mind mp empty_dirpath lab in
+      let kn = mind_of_delta res kn in
+	Indtypes.check_inductive env kn mib
   | SFBmodule msb ->
-      check_module env msb;
-      let mp1 = MPdot(mp,lab) in
-      let is_fun, sub = Modops.update_subst env msb mp1 in
-      ((if is_fun then s else join s sub),
-       Modops.add_module (MPdot(mp,lab)) msb env)
-  | SFBalias(mp2,_,cst) ->
-      (* cf Safe_typing.add_alias *)
-      (try
-        let mp' = MPdot(mp,lab) in
-        let mp2' = scrape_alias mp2 env in
-        let _,sub = Modops.update_subst env (lookup_module mp2' env) mp2' in
-        let sub = update_subst sub (map_mp mp' mp2') in
-        let sub = join_alias sub (map_mp mp' mp2') in
-        let sub = add_mp mp' mp2' sub in
-        (join s sub, register_alias mp' mp2 env)
-      with Not_found -> failwith "unknown aliased module")
+      let _= check_module env (MPdot(mp,lab)) msb in
+	Modops.add_module msb env
   | SFBmodtype mty ->
-      let kn = MPdot(mp, lab) in
       check_module_type env mty;
-      (join s mty.typ_alias, add_modtype kn mty env)
-
-and check_modexpr env mse = match mse with
+      add_modtype (MPdot(mp,lab)) mty env
+	
+and check_modexpr env mse mp_mse res = match mse with
+  | SEBident mp ->
+      let mb = lookup_module mp env in
+      	(subst_and_strengthen mb mp_mse env).mod_type
+  | SEBfunctor (arg_id, mtb, body) ->
+      check_module_type env mtb ;
+      let env' = add_module (module_body_of_type (MPbound arg_id) mtb) env in
+      let sign = check_modexpr env' body mp_mse res in
+	SEBfunctor (arg_id, mtb, sign)
+  | SEBapply (f,m,cst) ->
+      let sign = check_modexpr env f mp_mse res in
+      let farg_id, farg_b, fbody_b = destr_functor env sign in
+      let mp =
+	try (path_of_mexpr m)
+	with Not_path -> error_application_to_not_path m
+	  (* place for nondep_supertype *) in
+      let mtb = module_type_of_module env (Some mp) (lookup_module mp env) in
+	check_subtypes env mtb farg_b;
+	(subst_struct_expr (map_mbid farg_id mp) fbody_b)
+  | SEBwith(mte, with_decl) ->
+      let sign = check_modexpr env mte mp_mse res in
+      let sign = check_with env sign with_decl mp_mse in 
+	sign
+  | SEBstruct(msb) ->
+      let _ = List.fold_left (fun env (lab,mb) ->
+		   check_structure_field env mp_mse lab res mb) env msb in
+	SEBstruct(msb)
+	
+and check_modtype env mse mp_mse res = match mse with
   | SEBident mp ->
-      let mp = scrape_alias mp env in
       let mtb = lookup_modtype mp env in
-      mtb.typ_alias
+	mtb.typ_expr
   | SEBfunctor (arg_id, mtb, body) ->
       check_module_type env mtb;
-      let env' = add_module (MPbound arg_id) (module_body_of_type mtb) env in
-      let sub = check_modexpr env' body in
-      sub
+      let env' = add_module (module_body_of_type (MPbound arg_id) mtb) env in
+      let body = check_modtype env' body mp_mse res in
+	SEBfunctor(arg_id,mtb,body)
   | SEBapply (f,m,cst) ->
-      let sub1 = check_modexpr env f in
-      let f'= eval_struct env f in
-      let farg_id, farg_b, fbody_b = destr_functor env f' in
+      let sign = check_modtype env f mp_mse res in
+      let farg_id, farg_b, fbody_b = destr_functor env sign in
       let mp =
-	try scrape_alias (path_of_mexpr m) env
+	try (path_of_mexpr m)
 	with Not_path -> error_application_to_not_path m
-	      (* place for nondep_supertype *) in
-      let mtb = lookup_modtype mp env in
-      check_subtypes env mtb farg_b;
-      let sub2 = match eval_struct env m with
-	| SEBstruct (msid,sign) -> 
-	    join_alias 
-	      (subst_key (map_msid msid mp) mtb.typ_alias)
-	      (map_msid msid mp)
-	| _ -> mtb.typ_alias in
-      let sub3 = join_alias sub1 (map_mbid farg_id mp) in
-      let sub4 = update_subst sub2 sub3 in
-      join sub3 sub4
+	  (* place for nondep_supertype *) in
+      let mtb = module_type_of_module env (Some mp) (lookup_module mp env) in
+	check_subtypes env mtb farg_b;
+	subst_struct_expr (map_mbid farg_id mp) fbody_b
   | SEBwith(mte, with_decl) ->
-	let sub1 = check_modexpr env mte in
-	let sub2 = check_with env mte with_decl in
-	join sub1 sub2
-  | SEBstruct(msid,msb) ->
-      let mp = MPself msid in
-      let (sub,_) =
-        List.fold_left (fun env (lab,mb) ->
-          check_structure_field env mp lab mb) (empty_subst,env) msb in
-      sub
-
+      let sign = check_modtype env mte mp_mse res in
+      let sign = check_with env sign with_decl mp_mse in
+	sign
+  | SEBstruct(msb) ->
+      let _ = List.fold_left (fun env (lab,mb) ->
+		   check_structure_field env mp_mse lab res mb) env msb in
+      SEBstruct(msb)
+	
 (*
-let rec add_struct_expr_constraints env = function
+  let rec add_struct_expr_constraints env = function
   | SEBident _ -> env
-
-  | SEBfunctor (_,mtb,meb) -> 
-      add_struct_expr_constraints 
-	(add_modtype_constraints env mtb) meb
+  
+  | SEBfunctor (_,mtb,meb) ->
+  add_struct_expr_constraints
+  (add_modtype_constraints env mtb) meb
 
   | SEBstruct (_,structure_body) ->
-      List.fold_left 
+      List.fold_left
         (fun env (l,item) -> add_struct_elem_constraints env item)
         env
         structure_body
@@ -369,20 +350,20 @@ let rec add_struct_expr_constraints env = function
   | SEBapply (meb1,meb2,cst) ->
 (*  let g = Univ.merge_constraints cst Univ.initial_universes in
 msgnl(str"ADDING FUNCTOR APPLICATION CONSTRAINTS:"++fnl()++
-      Univ.pr_universes g++str"============="++fnl());      
+      Univ.pr_universes g++str"============="++fnl());
 *)
-      Environ.add_constraints cst 
-        (add_struct_expr_constraints 
-	  (add_struct_expr_constraints env meb1) 
+      Environ.add_constraints cst
+        (add_struct_expr_constraints
+	  (add_struct_expr_constraints env meb1)
 	  meb2)
   | SEBwith(meb,With_definition_body(_,cb))->
       Environ.add_constraints cb.const_constraints
 	(add_struct_expr_constraints env meb)
   | SEBwith(meb,With_module_body(_,_,cst))->
       Environ.add_constraints cst
-	(add_struct_expr_constraints env meb)	
-		
-and add_struct_elem_constraints env = function 
+	(add_struct_expr_constraints env meb)
+
+and add_struct_elem_constraints env = function
   | SFBconst cb -> Environ.add_constraints cb.const_constraints env
   | SFBmind mib -> Environ.add_constraints mib.mind_constraints env
   | SFBmodule mb -> add_module_constraints env mb
@@ -390,18 +371,18 @@ and add_struct_elem_constraints env = function
   | SFBalias (mp,None) -> env
   | SFBmodtype mtb -> add_modtype_constraints env mtb
 
-and add_module_constraints env mb = 
+and add_module_constraints env mb =
   let env = match mb.mod_expr with
     | None -> env
     | Some meb -> add_struct_expr_constraints env meb
   in
   let env = match mb.mod_type with
     | None -> env
-    | Some mtb -> 
+    | Some mtb ->
 	add_struct_expr_constraints env mtb
   in
     Environ.add_constraints mb.mod_constraints env
 
-and add_modtype_constraints env mtb = 
+and add_modtype_constraints env mtb =
   add_struct_expr_constraints env mtb.typ_expr
 *)