Merge PR #8515: Command driven attributes

1 files changed, 50 insertions, 10 deletions

diff --git a/interp/modintern.ml b/interp/modintern.ml
index c27cc9cc07..51e27299e3 100644
--- a/interp/modintern.ml
+++ b/interp/modintern.ml
@@ -61,13 +61,52 @@ let lookup_module_or_modtype kind qid =
 
 let lookup_module lqid = fst (lookup_module_or_modtype Module lqid)
 
-let transl_with_decl env = function
+let lookup_polymorphism env base kind fqid =
+  let m = match kind with
+    | Module -> (Environ.lookup_module base env).mod_type
+    | ModType -> (Environ.lookup_modtype base env).mod_type
+    | ModAny -> assert false
+  in
+  let rec defunctor = function
+    | NoFunctor m -> m
+    | MoreFunctor (_,_,m) -> defunctor m
+  in
+  let rec aux m fqid =
+    let open Names in
+    match fqid with
+    | [] -> assert false
+    | [id] ->
+      let test (lab,obj) =
+        match Id.equal (Label.to_id lab) id, obj with
+        | false, _ | _, (SFBmodule _ | SFBmodtype _) -> None
+        | true, SFBmind mind -> Some (Declareops.inductive_is_polymorphic mind)
+        | true, SFBconst const -> Some (Declareops.constant_is_polymorphic const)
+      in
+      (try CList.find_map test m with Not_found -> false (* error later *))
+    | id::rem ->
+      let next = function
+        | MoreFunctor _ -> false (* error later *)
+        | NoFunctor body -> aux body rem
+      in
+      let test (lab,obj) =
+        match Id.equal (Label.to_id lab) id, obj with
+        | false, _ | _, (SFBconst _ | SFBmind _) -> None
+        | true, SFBmodule body -> Some (next body.mod_type)
+        | true, SFBmodtype body ->  (* XXX is this valid? If not error later *)
+          Some (next body.mod_type)
+      in
+      (try CList.find_map test m with Not_found -> false (* error later *))
+  in
+  aux (defunctor m) fqid
+
+let transl_with_decl env base kind = function
   | CWith_Module ({CAst.v=fqid},qid) ->
       WithMod (fqid,lookup_module qid), Univ.ContextSet.empty
   | CWith_Definition ({CAst.v=fqid},udecl,c) ->
     let sigma, udecl = Constrexpr_ops.interp_univ_decl_opt env udecl in
     let c, ectx = interp_constr env sigma c in
-    begin match UState.check_univ_decl ~poly:(Flags.is_universe_polymorphism()) ectx udecl with
+    let poly = lookup_polymorphism env base kind fqid in
+    begin match UState.check_univ_decl ~poly ectx udecl with
       | Entries.Polymorphic_const_entry ctx ->
         let inst, ctx = Univ.abstract_universes ctx in
         let c = EConstr.Vars.subst_univs_level_constr (Univ.make_instance_subst inst) c in
@@ -86,23 +125,24 @@ let loc_of_module l = l.CAst.loc
 let rec interp_module_ast env kind m cst = match m with
   | {CAst.loc;v=CMident qid} ->
       let (mp,kind) = lookup_module_or_modtype kind qid in
-      (MEident mp, kind, cst)
+      (MEident mp, mp, kind, cst)
   | {CAst.loc;v=CMapply (me1,me2)} ->
-      let me1',kind1, cst = interp_module_ast env kind me1 cst in
-      let me2',kind2, cst = interp_module_ast env ModAny me2 cst in
+      let me1', base, kind1, cst = interp_module_ast env kind me1 cst in
+      let me2', _, kind2, cst = interp_module_ast env ModAny me2 cst in
       let mp2 = match me2' with
         | MEident mp -> mp
         | _ -> error_application_to_not_path (loc_of_module me2) me2'
       in
       if kind2 == ModType then
         error_application_to_module_type (loc_of_module me2);
-      (MEapply (me1',mp2), kind1, cst)
+      (MEapply (me1',mp2), base, kind1, cst)
   | {CAst.loc;v=CMwith (me,decl)} ->
-      let me,kind,cst = interp_module_ast env kind me cst in
+      let me,base,kind,cst = interp_module_ast env kind me cst in
       if kind == Module then error_incorrect_with_in_module m.CAst.loc;
-      let decl, cst' = transl_with_decl env decl in
+      let decl, cst' = transl_with_decl env base kind decl in
       let cst = Univ.ContextSet.union cst cst' in
-      (MEwith(me,decl), kind, cst)
+      (MEwith(me,decl), base, kind, cst)
 
 let interp_module_ast env kind m =
-  interp_module_ast env kind m Univ.ContextSet.empty
+  let me, _, kind, cst = interp_module_ast env kind m Univ.ContextSet.empty in
+  me, kind, cst