Merge PR #6443: [vernac] Cleanup of do_definition.

1 files changed, 46 insertions, 45 deletions

diff --git a/vernac/comDefinition.ml b/vernac/comDefinition.ml
index 883121479..d376696f7 100644
--- a/vernac/comDefinition.ml
+++ b/vernac/comDefinition.ml
@@ -11,7 +11,6 @@ open Util
 open Constr
 open Environ
 open Entries
-open Termops
 open Redexpr
 open Declare
 open Constrintern
@@ -49,55 +48,57 @@ let warn_implicits_in_term =
           strbrk "Implicit arguments declaration relies on type." ++ spc () ++
             strbrk "The term declares more implicits than the type here.")
 
+let check_imps ~impsty ~impsbody =
+  let b =
+    try
+      List.for_all (fun (key, (va:bool*bool*bool)) ->
+          (* Pervasives.(=) is OK for this type *)
+          Pervasives.(=) (List.assoc_f Impargs.explicitation_eq key impsty) va)
+        impsbody
+    with Not_found -> false
+  in
+  if not b then warn_implicits_in_term ()
+
 let interp_definition pl bl poly red_option c ctypopt =
+  let open EConstr in
   let env = Global.env() in
+  (* Explicitly bound universes and constraints *)
   let evd, decl = Univdecls.interp_univ_decl_opt env pl in
+  (* Build the parameters *)
   let evd, (impls, ((env_bl, ctx), imps1)) = interp_context_evars env evd bl in
-  let ctx = List.map (fun d -> map_rel_decl EConstr.Unsafe.to_constr d) ctx in
-  let nb_args = Context.Rel.nhyps ctx in
-  let evd,imps,ce =
-    match ctypopt with
-      None ->
-        let evd, subst = Evd.nf_univ_variables evd in
-        let ctx = Context.Rel.map (Vars.subst_univs_constr subst) ctx in
-        let env_bl = push_rel_context ctx env in
-        let evd, (c, imps2) = interp_constr_evars_impls ~impls env_bl evd c in
-        let c = EConstr.Unsafe.to_constr c in
-        let evd,nf = Evarutil.nf_evars_and_universes evd in
-        let body = nf (it_mkLambda_or_LetIn c ctx) in
-        let vars = EConstr.universes_of_constr env evd (EConstr.of_constr body) in
-        let evd = Evd.restrict_universe_context evd vars in
-        let uctx = Evd.check_univ_decl ~poly evd decl in
-        evd, imps1@(Impargs.lift_implicits nb_args imps2),
-          definition_entry ~univs:uctx body
-    | Some ctyp ->
-        let evd, (ty, impsty) = interp_type_evars_impls ~impls env_bl evd ctyp in
-        let evd, subst = Evd.nf_univ_variables evd in
-        let ctx = Context.Rel.map (Vars.subst_univs_constr subst) ctx in
-        let env_bl = push_rel_context ctx env in
-        let evd, (c, imps2) = interp_casted_constr_evars_impls ~impls env_bl evd c ty in
-        let c = EConstr.Unsafe.to_constr c in
-        let evd, nf = Evarutil.nf_evars_and_universes evd in
-        let body = nf (it_mkLambda_or_LetIn c ctx) in
-        let ty = EConstr.Unsafe.to_constr ty in
-        let typ = nf (Term.it_mkProd_or_LetIn ty ctx) in
-        let beq b1 b2 = if b1 then b2 else not b2 in
-        let impl_eq (x,y,z) (x',y',z') = beq x x' && beq y y' && beq z z' in
-        (* Check that all implicit arguments inferable from the term
-           are inferable from the type *)
-        let chk (key,va) =
-          impl_eq (List.assoc_f Pervasives.(=) key impsty) va (* FIXME *)
-        in
-        if not (try List.for_all chk imps2 with Not_found -> false)
-        then warn_implicits_in_term ();
-        let bodyvars = EConstr.universes_of_constr env evd (EConstr.of_constr body) in
-        let tyvars = EConstr.universes_of_constr env evd (EConstr.of_constr ty) in
-        let vars = Univ.LSet.union bodyvars tyvars in
-        let evd = Evd.restrict_universe_context evd vars in
-        let uctx = Evd.check_univ_decl ~poly evd decl in
-        evd, imps1@(Impargs.lift_implicits nb_args impsty),
-          definition_entry ~types:typ ~univs:uctx body
+  (* Build the type *)
+  let evd, tyopt = Option.fold_left_map
+      (interp_type_evars_impls ~impls env_bl)
+      evd ctypopt
+  in
+  (* Build the body, and merge implicits from parameters and from type/body *)
+  let evd, c, imps, tyopt =
+    match tyopt with
+    | None ->
+      let evd, (c, impsbody) = interp_constr_evars_impls ~impls env_bl evd c in
+      evd, c, imps1@Impargs.lift_implicits (Context.Rel.nhyps ctx) impsbody, None
+    | Some (ty, impsty) ->
+      let evd, (c, impsbody) = interp_casted_constr_evars_impls ~impls env_bl evd c ty in
+      check_imps ~impsty ~impsbody;
+      evd, c, imps1@Impargs.lift_implicits (Context.Rel.nhyps ctx) impsty, Some ty
+  in
+  (* universe minimization *)
+  let evd = Evd.nf_constraints evd in
+  (* Substitute evars and universes, and add parameters.
+     Note: in program mode some evars may remain. *)
+  let ctx = List.map (EConstr.to_rel_decl evd) ctx in
+  let c = Term.it_mkLambda_or_LetIn (EConstr.to_constr evd c) ctx in
+  let tyopt = Option.map (fun ty -> Term.it_mkProd_or_LetIn (EConstr.to_constr evd ty) ctx) tyopt in
+  (* Keep only useful universes. *)
+  let uvars_fold uvars c =
+    Univ.LSet.union uvars (universes_of_constr env evd (of_constr c))
   in
+  let uvars = List.fold_left uvars_fold Univ.LSet.empty (Option.List.cons tyopt [c]) in
+  let evd = Evd.restrict_universe_context evd uvars in
+  (* Check we conform to declared universes *)
+  let uctx = Evd.check_univ_decl ~poly evd decl in
+  (* We're done! *)
+  let ce = definition_entry ?types:tyopt ~univs:uctx c in
   (red_constant_entry (Context.Rel.length ctx) ce evd red_option, evd, decl, imps)
 
 let check_definition (ce, evd, _, imps) =