[vernac] Split `command.ml` into separate files.

Over the time, `Command` grew organically and it has become now one of
the most complex files in the codebase; however, its functionality is
well separated into 4 key components that have little to do with each
other.

We thus split the file, and also document the interfaces. Some parts
of `Command` export tricky internals to use by other plugins, and it
is common that plugin writers tend to get confused, so we are more
explicit about these parts now.

This patch depends on #6413.

1 files changed, 131 insertions, 0 deletions

diff --git a/vernac/comDefinition.ml b/vernac/comDefinition.ml
new file mode 100644
index 000000000..c8b289c9d
--- /dev/null
+++ b/vernac/comDefinition.ml
@@ -0,0 +1,131 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2018     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+open Pp
+open Util
+open Constr
+open Environ
+open Entries
+open Termops
+open Redexpr
+open Declare
+open Constrintern
+open Pretyping
+
+open Context.Rel.Declaration
+
+(* Commands of the interface: Constant definitions *)
+
+let rec under_binders env sigma f n c =
+  if Int.equal n 0 then f env sigma (EConstr.of_constr c) else
+    match Constr.kind c with
+      | Lambda (x,t,c) ->
+          mkLambda (x,t,under_binders (push_rel (LocalAssum (x,t)) env) sigma f (n-1) c)
+      | LetIn (x,b,t,c) ->
+          mkLetIn (x,b,t,under_binders (push_rel (LocalDef (x,b,t)) env) sigma f (n-1) c)
+      | _ -> assert false
+
+let red_constant_entry n ce sigma = function
+  | None -> ce
+  | Some red ->
+      let proof_out = ce.const_entry_body in
+      let env = Global.env () in
+      let (redfun, _) = reduction_of_red_expr env red in
+      let redfun env sigma c =
+        let (_, c) = redfun env sigma c in
+        EConstr.Unsafe.to_constr c
+      in
+      { ce with const_entry_body = Future.chain proof_out
+        (fun ((body,ctx),eff) -> (under_binders env sigma redfun n body,ctx),eff) }
+
+let warn_implicits_in_term =
+  CWarnings.create ~name:"implicits-in-term" ~category:"implicits"
+         (fun () ->
+          strbrk "Implicit arguments declaration relies on type." ++ spc () ++
+            strbrk "The term declares more implicits than the type here.")
+
+let interp_definition pl bl poly red_option c ctypopt =
+  let env = Global.env() in
+  let evd, decl = Univdecls.interp_univ_decl_opt env pl in
+  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
+  in
+  (red_constant_entry (Context.Rel.length ctx) ce evd red_option, evd, decl, imps)
+
+let check_definition (ce, evd, _, imps) =
+  check_evars_are_solved (Global.env ()) evd Evd.empty;
+  ce
+
+let do_definition ident k univdecl bl red_option c ctypopt hook =
+  let (ce, evd, univdecl, imps as def) =
+    interp_definition univdecl bl (pi2 k) red_option c ctypopt
+  in
+    if Flags.is_program_mode () then
+      let env = Global.env () in
+      let (c,ctx), sideff = Future.force ce.const_entry_body in
+      assert(Safe_typing.empty_private_constants = sideff);
+      assert(Univ.ContextSet.is_empty ctx);
+      let typ = match ce.const_entry_type with
+        | Some t -> t
+        | None -> EConstr.to_constr evd (Retyping.get_type_of env evd (EConstr.of_constr c))
+      in
+      Obligations.check_evars env evd;
+      let obls, _, c, cty =
+        Obligations.eterm_obligations env ident evd 0 c typ
+      in
+      let ctx = Evd.evar_universe_context evd in
+      let hook = Lemmas.mk_hook (fun l r _ -> Lemmas.call_hook (fun exn -> exn) hook l r) in
+      ignore(Obligations.add_definition
+          ident ~term:c cty ctx ~univdecl ~implicits:imps ~kind:k ~hook obls)
+    else let ce = check_definition def in
+      ignore(DeclareDef.declare_definition ident k ce (Evd.universe_binders evd) imps
+        (Lemmas.mk_hook
+          (fun l r -> Lemmas.call_hook (fun exn -> exn) hook l r;r)))