1 files changed, 398 insertions, 0 deletions
diff --git a/checker/mod_checking.ml b/checker/mod_checking.ml
new file mode 100644
index 00000000..ecf8d633
--- /dev/null
+++ b/checker/mod_checking.ml
@@ -0,0 +1,398 @@
+
+open Pp
+open Util
+open Names
+open Term
+open Inductive
+open Reduction
+open Typeops
+open Indtypes
+open Modops
+open Subtyping
+open Declarations
+open Environ
+
+(************************************************************************)
+(* Checking constants *)
+
+let refresh_arity ar =
+  let ctxt, hd = decompose_prod_assum ar in
+  match hd with
+      Sort (Type u) when not (Univ.is_univ_variable u) ->
+        let u' = Univ.fresh_local_univ() in
+        mkArity (ctxt,Type u'),
+        Univ.enforce_geq u' u Univ.Constraint.empty
+    | _ -> ar, Univ.Constraint.empty
+
+let check_constant_declaration env kn cb =
+  Flags.if_verbose msgnl (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 _ = infer_type envty ty in
+        (match cb.const_body with
+          | Some bd ->
+              let j = infer env' (force_constr bd) in
+              conv_leq envty j ty
+          | None -> ())
+    | PolymorphicArity(ctxt,par) ->
+        let _ = check_ctxt env ctxt in
+        check_polymorphic_arity env ctxt par);
+  add_constant kn cb env
+
+(************************************************************************)
+(* Checking modules *)
+
+
+let rec add_struct_expr_constraints env = function
+  | SEBident _ -> env
+
+  | SEBfunctor (_,mtb,meb) -> 
+      add_struct_expr_constraints 
+	(add_modtype_constraints env mtb) meb
+
+  | SEBstruct (_,structure_body) ->
+      List.fold_left 
+        (fun env (l,item) -> add_struct_elem_constraints env item)
+        env
+        structure_body
+
+  | 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());      
+*)
+      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 
+  | 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
+  | SFBalias (mp,Some cst) -> Environ.add_constraints cst env
+  | SFBalias (mp,None) -> env
+  | SFBmodtype mtb -> add_modtype_constraints env mtb
+
+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 -> 
+	add_struct_expr_constraints env mtb
+  in
+    Environ.add_constraints mb.mod_constraints env
+
+and add_modtype_constraints env mtb = 
+  add_struct_expr_constraints env mtb.typ_expr
+
+exception Not_path
+
+let path_of_mexpr = function
+  | SEBident mp -> mp
+  | _ -> raise Not_path
+
+let rec list_split_assoc k rev_before = function
+  | [] -> raise Not_found
+  | (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 
+  |  []  -> (e,[],[])
+  |  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 = 
+
+    (* If the type of a constant is generated, it may mention
+       non-variable algebraic universes that the general conversion
+       algorithm is not ready to handle. Anyway, generated types of
+       constants are functions of the body of the constant. If the
+       bodies are the same in environments that are subtypes one of
+       the other, the types are subtypes too (i.e. if Gamma <= Gamma',
+       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 = 
+      if isArity t2 then
+        let (ctx2,s2) = destArity t2 in
+        match s2 with
+        | Type v when not (Univ.is_univ_variable v) ->
+          (* The type in the interface is inferred and is made of algebraic
+             universes *)
+          begin try
+            let (ctx1,s1) = dest_arity env t1 in
+            match s1 with
+            | Type u when not (Univ.is_univ_variable u) ->
+              (* Both types are inferred, no need to recheck them. We
+                 cheat and collapse the types to Prop *)
+                mkArity (ctx1,Prop Null), mkArity (ctx2,Prop Null)
+            | Prop _ ->
+              (* The type in the interface is inferred, it may be the case
+                 that the type in the implementation is smaller because
+                 the body is more reduced. We safely collapse the upper
+                 type to Prop *)
+                mkArity (ctx1,Prop Null), mkArity (ctx2,Prop Null)
+            | Type _ ->
+              (* The type in the interface is inferred and the type in the
+                 implementation is not inferred or is inferred but from a
+                 more reduced body so that it is just a variable. Since
+                 constraints of the form "univ <= max(...)" are not
+                 expressible in the system of algebraic universes: we fail
+                 (the user has to use an explicit type in the interface *)
+                raise Reduction.NotConvertible
+          with UserError _ (* "not an arity" *) ->
+            raise Reduction.NotConvertible end
+        | _ -> t1,t2
+      else
+        (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
+  check_type env typ1 typ2;
+  (match cb2 with
+    | {const_body=Some lc2;const_opaque=false} ->
+	let c2 = force_constr lc2 in
+	let c1 = match cb1.const_body with
+	  | Some lc1 -> force_constr lc1
+	  | None -> assert false in
+	Reduction.conv env c1 c2
+    | _ -> ())
+
+let rec check_with env mtb with_decl = 
+  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
+
+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
+    | _ -> error_signature_expected mtb
+  in
+  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
+  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
+	match with_decl with
+          | With_definition_body ([],_) -> assert false
+	  | With_definition_body ([id],c) -> 
+	      let cb = match spec with
+		  SFBconst cb -> cb
+		| _ -> error_not_a_constant l
+	      in 
+              check_definition_sub env' c cb
+	  | With_definition_body (_::_,_) ->
+	      let old = match spec with
+		  SFBmodule msb -> msb
+		| _ -> error_not_a_module l
+	      in
+		begin
+		  match old.mod_expr with
+                    | None ->
+			let new_with_decl = match with_decl with
+			    With_definition_body (_,c) ->
+                              With_definition_body (idl,c)
+			  | With_module_body (_,c,cst) ->
+                              With_module_body (idl,c,cst) in 
+			  check_with_aux_def env' (type_of_mb env old) new_with_decl
+                    | Some msb ->
+			error_a_generative_module_expected l
+		end
+	  | _ -> anomaly "Modtyping:incorrect use of with"
+    with
+	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)
+    | _ -> error_signature_expected mtb in
+  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
+  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
+	| i::r -> MPdot(mp_rec r,label_of_id i)
+      in 
+      let env' = Modops.add_signature (MPself msid) before 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'
+		| _ -> 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 old = match spec with
+		SFBmodule msb -> msb
+	      | _ -> error_not_a_module l
+	    in
+	      begin
+		match old.mod_expr with
+                    None ->
+                      let new_with_decl = match with_decl with
+			  With_definition_body (_,c) -> 
+			    With_definition_body (idl,c)
+			| With_module_body (_,c,cst) ->
+                            With_module_body (idl,c,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
+                  | Some msb ->
+                      error_a_generative_module_expected l
+              end
+	| _ -> anomaly "Modtyping:incorrect use of with"
+    with
+	Not_found -> error_no_such_label l
+      | 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
+
+and check_module env mb =
+  let env' = add_module_constraints env mb in
+  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
+  | SFBconst cb ->
+      let c = make_con mp empty_dirpath lab in
+      (s,check_constant_declaration env c cb)
+  | SFBmind mib ->
+      let kn = make_kn mp empty_dirpath lab in
+      (s,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
+         (add_module_constraints env msb))
+  | SFBalias(mp2,cst) ->
+      (try
+        let mp2' = scrape_alias mp2 env in
+        let msb = lookup_module mp2' env in
+        (join s (add_mp (MPdot(mp,lab)) mp2' msb.mod_alias),
+         Option.fold_right add_constraints cst
+           (register_alias (MPdot(mp,lab)) mp2 env))
+      with Not_found -> failwith "unkown aliased module")
+  | SFBmodtype mty ->
+      let kn = MPdot(mp, lab) in
+      check_module_type env mty;
+      (join s mty.typ_alias,
+       add_modtype kn mty (add_modtype_constraints env mty))
+
+and check_modexpr env mse = match mse with
+  | SEBident mp ->
+      let mtb = lookup_modtype mp env in 
+      mtb.typ_alias
+  | 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
+  | 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 mp =
+	try scrape_alias (path_of_mexpr m) env
+	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
+  | 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