[checker] Refactor by sharing code with the kernel

For historical reasons, the checker was duplicating a lot of code of the
kernel. The main differences I found were bug fixes that had not been
backported.

With this patch, the checker uses the kernel as a library to serve the
same purpose as before: validation of a `.vo` file, re-typechecking all
definitions a posteriori.

We also rename some files from the checker so that they don't clash with
kernel files.

1 files changed, 270 insertions, 0 deletions

diff --git a/checker/checkInductive.ml b/checker/checkInductive.ml
new file mode 100644
index 0000000000..cf086049ca
--- /dev/null
+++ b/checker/checkInductive.ml
@@ -0,0 +1,270 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+open Sorts
+open Pp
+open Declarations
+open Environ
+open Names
+open CErrors
+open Univ
+open Util
+open Constr
+
+let check_kind env ar u =
+  match Constr.kind (snd (Reduction.dest_prod env ar)) with
+  | Sort (Sorts.Type u') when Univ.Universe.equal u' (Univ.Universe.make u) -> ()
+  | _ -> failwith "not the correct sort"
+
+let check_polymorphic_arity env params par =
+  let pl = par.template_param_levels in
+  let rec check_p env pl params =
+    let open Context.Rel.Declaration in
+    match pl, params with
+        Some u::pl, LocalAssum (na,ty)::params ->
+          check_kind env ty u;
+          check_p (push_rel (LocalAssum (na,ty)) env) pl params
+      | None::pl,d::params -> check_p (push_rel d env) pl params
+      | [], _ -> ()
+      | _ -> failwith "check_poly: not the right number of params" in
+  check_p env pl (List.rev params)
+
+let conv_ctxt_prefix env (ctx1:rel_context) ctx2 =
+  let rec chk env rctx1 rctx2 =
+    let open Context.Rel.Declaration in
+    match rctx1, rctx2 with
+        (LocalAssum (_,ty1) as d1)::rctx1', LocalAssum (_,ty2)::rctx2' ->
+          Reduction.conv env ty1 ty2;
+          chk (push_rel d1 env) rctx1' rctx2'
+      | (LocalDef (_,bd1,ty1) as d1)::rctx1', LocalDef (_,bd2,ty2)::rctx2' ->
+          Reduction.conv env ty1 ty2;
+          Reduction.conv env bd1 bd2;
+          chk (push_rel d1 env) rctx1' rctx2'
+      | [],_ -> ()
+      | _ -> failwith "non convertible contexts" in
+  chk env (List.rev ctx1) (List.rev ctx2)
+
+(* check information related to inductive arity *)
+let typecheck_arity env params inds =
+  let nparamargs = Context.Rel.nhyps params in
+  let nparamdecls = Context.Rel.length params in
+  let check_arity arctxt = function
+    | RegularArity mar ->
+        let ar = mar.mind_user_arity in
+        let _ = Typeops.infer_type env ar in
+        Reduction.conv env (Term.it_mkProd_or_LetIn (Constr.mkSort mar.mind_sort) arctxt) ar;
+        ar
+    | TemplateArity par ->
+      check_polymorphic_arity env params par;
+      Term.it_mkProd_or_LetIn (Constr.mkSort(Sorts.Type par.template_level)) arctxt
+  in
+  let env_arities =
+    Array.fold_left
+      (fun env_ar ind ->
+        let ar_ctxt = ind.mind_arity_ctxt in
+        let _ = Typeops.check_context env ar_ctxt in
+        conv_ctxt_prefix env params ar_ctxt;
+        (* Arities (with params) are typed-checked here *)
+        let arity = check_arity ar_ctxt ind.mind_arity in
+        (* mind_nrealargs *)
+        let nrealargs = Context.Rel.nhyps ar_ctxt - nparamargs in
+        if ind.mind_nrealargs <> nrealargs then
+             failwith "bad number of real inductive arguments";
+        let nrealargs_ctxt = Context.Rel.length ar_ctxt - nparamdecls in
+        if ind.mind_nrealdecls <> nrealargs_ctxt then
+             failwith "bad length of real inductive arguments signature";
+        (* We do not need to generate the universe of full_arity; if
+           later, after the validation of the inductive definition,
+           full_arity is used as argument or subject to cast, an
+           upper universe will be generated *)
+        let id = ind.mind_typename in
+        let env_ar' = push_rel (Context.Rel.Declaration.LocalAssum (Name id, arity)) env_ar in
+        env_ar')
+      env
+      inds in
+  env_arities
+
+(* Check that the subtyping information inferred for inductive types in the block is correct. *)
+(* This check produces a value of the unit type if successful or raises an anomaly if check fails. *)
+let check_subtyping cumi paramsctxt env arities =
+    let numparams = Context.Rel.nhyps paramsctxt in
+  (** In [env] we already have [ Var(0) ... Var(n-1) |- cst ] available.
+      We must produce the substitution σ : [ Var(i) -> Var (i + n) | 0 <= i < n]
+      and push the constraints [ Var(n) ... Var(2n - 1) |- cst{σ} ], together
+      with the cumulativity constraints [ cumul_cst ]. *)
+  let uctx = ACumulativityInfo.univ_context cumi in
+  let len = AUContext.size uctx in
+  let inst = Instance.of_array @@ Array.init len (fun i -> Level.var (i + len)) in
+
+  let other_context = ACumulativityInfo.univ_context cumi in
+  let uctx_other = UContext.make (inst, AUContext.instantiate inst other_context) in
+  let cumul_cst =
+    Array.fold_left_i (fun i csts var ->
+        match var with
+        | Variance.Irrelevant -> csts
+        | Variance.Covariant -> Constraint.add (Level.var i,Le,Level.var (i+len)) csts
+        | Variance.Invariant -> Constraint.add (Level.var i,Eq,Level.var (i+len)) csts)
+      Constraint.empty (ACumulativityInfo.variance cumi)
+  in
+  let env = Environ.push_context uctx_other env in
+  let env = Environ.add_constraints cumul_cst env in
+  let dosubst = Vars.subst_instance_constr inst in
+    (* process individual inductive types: *)
+    Array.iter (fun { mind_user_lc = lc; mind_arity = arity } ->
+      match arity with
+        | RegularArity { mind_user_arity = full_arity} ->
+           Indtypes.check_subtyping_arity_constructor env dosubst full_arity numparams true;
+           Array.iter (fun cnt -> Indtypes.check_subtyping_arity_constructor env dosubst cnt numparams false) lc
+        | TemplateArity _ ->
+          anomaly ~label:"check_subtyping"
+            Pp.(str "template polymorphism and cumulative polymorphism are not compatible")
+    ) arities
+
+(* An inductive definition is a "unit" if it has only one constructor
+   and that all arguments expected by this constructor are
+   logical, this is the case for equality, conjunction of logical properties
+*)
+let is_unit constrsinfos =
+  match constrsinfos with  (* One info = One constructor *)
+   | [|constrinfos|] -> Univ.is_type0m_univ constrinfos
+   | [||] -> (* type without constructors *) true
+   | _ -> false
+
+let small_unit constrsinfos =
+  let issmall = Array.for_all Univ.is_small_univ constrsinfos
+  and isunit = is_unit constrsinfos in
+  issmall, isunit
+
+let all_sorts = [InProp;InSet;InType]
+let small_sorts = [InProp;InSet]
+let logical_sorts = [InProp]
+
+let allowed_sorts issmall isunit s =
+  match Sorts.family s with
+  (* Type: all elimination allowed *)
+  | InType -> all_sorts
+
+  (* Small Set is predicative: all elimination allowed *)
+  | InSet when issmall -> all_sorts
+
+  (* Large Set is necessarily impredicative: forbids large elimination *)
+  | InSet -> small_sorts
+
+  (* Unitary/empty Prop: elimination to all sorts are realizable *)
+  (* unless the type is large. If it is large, forbids large elimination *)
+  (* which otherwise allows simulating the inconsistent system Type:Type *)
+  | InProp when isunit -> if issmall then all_sorts else small_sorts
+
+  (* Other propositions: elimination only to Prop *)
+  | InProp -> logical_sorts
+
+let check_predicativity env s small level =
+  match s, engagement env with
+      Type u, _ ->
+        (* let u' = fresh_local_univ () in *)
+        (* let cst = *)
+        (*   merge_constraints (enforce_leq u u' empty_constraint) *)
+        (*     (universes env) in *)
+        if not (UGraph.check_leq (universes env) level u) then
+          failwith "impredicative Type inductive type"
+    | Set, ImpredicativeSet -> ()
+    | Set, _ ->
+        if not small then failwith "impredicative Set inductive type"
+    | Prop,_ -> ()
+
+let sort_of_ind = function
+  | RegularArity mar -> mar.mind_sort
+  | TemplateArity par -> Type par.template_level
+
+let compute_elim_sorts env_ar params arity lc =
+  let inst = Context.Rel.to_extended_list Constr.mkRel 0 params in
+  let env_params = push_rel_context params env_ar in
+  let lc = Array.map
+    (fun c ->
+      Reduction.hnf_prod_applist env_params (Vars.lift (Context.Rel.length params) c) inst)
+    lc in
+  let s = sort_of_ind arity in
+  let infos = Array.map (Indtypes.infos_and_sort env_params) lc in
+  let (small,unit) = small_unit infos in
+  (* We accept recursive unit types... *)
+  (* compute the max of the sorts of the products of the constructor type *)
+  let min = if Array.length lc > 1 then Universe.type0 else Universe.type0m in
+  let level = Array.fold_left (fun max l -> Universe.sup max l) min infos in
+  check_predicativity env_ar s small level;
+  allowed_sorts small unit s
+
+let typecheck_one_inductive env params mip =
+  (* mind_typename and mind_consnames not checked *)
+  (* mind_reloc_tbl, mind_nb_constant, mind_nb_args not checked (VM) *)
+  (* mind_arity_ctxt, mind_arity, mind_nrealargs DONE (typecheck_arity) *)
+  (* mind_user_lc *)
+  let _ = Array.map (Typeops.infer_type env) mip.mind_user_lc in
+  (* mind_nf_lc *)
+  let _ = Array.map (Typeops.infer_type env) mip.mind_nf_lc in
+  Array.iter2 (Reduction.conv env) mip.mind_nf_lc mip.mind_user_lc;
+  (* mind_consnrealdecls *)
+  let check_cons_args c n =
+    let ctx,_ = Term.decompose_prod_assum c in
+    if n <> Context.Rel.length ctx - Context.Rel.length params then
+      failwith "bad number of real constructor arguments" in
+  Array.iter2 check_cons_args mip.mind_nf_lc mip.mind_consnrealdecls;
+  (* mind_kelim: checked by positivity criterion ? *)
+  let sorts =
+    compute_elim_sorts env params mip.mind_arity mip.mind_nf_lc in
+  let reject_sort s = not (List.mem_f Sorts.family_equal s sorts) in
+  if List.exists reject_sort mip.mind_kelim then
+    failwith "elimination not allowed";
+  (* mind_recargs: checked by positivity criterion *)
+  ()
+
+let check_inductive env kn mib =
+  Flags.if_verbose Feedback.msg_notice (str "  checking mutind block: " ++ MutInd.print kn);
+  (* check mind_constraints: should be consistent with env *)
+  let env0 =
+    match mib.mind_universes with
+    | Monomorphic_ind _ -> env
+    | Polymorphic_ind auctx ->
+      let uctx = Univ.AUContext.repr auctx in
+      Environ.push_context uctx env
+    | Cumulative_ind cumi ->
+      let uctx = Univ.AUContext.repr (Univ.ACumulativityInfo.univ_context cumi) in
+      Environ.push_context uctx env
+  in
+  (** Locally set the oracle for further typechecking *)
+  let env0 = Environ.set_oracle env0 mib.mind_typing_flags.conv_oracle in
+  (* check mind_record : TODO ? check #constructor = 1 ? *)
+  (* check mind_finite : always OK *)
+  (* check mind_ntypes *)
+  if Array.length mib.mind_packets <> mib.mind_ntypes then
+    user_err Pp.(str "not the right number of packets");
+  (* check mind_params_ctxt *)
+  let params = mib.mind_params_ctxt in
+  let _ = Typeops.check_context env0 params in
+  (* check mind_nparams *)
+  if Context.Rel.nhyps params <> mib.mind_nparams then
+    user_err Pp.(str "number the right number of parameters");
+  (* mind_packets *)
+  (*  - check arities *)
+  let env_ar = typecheck_arity env0 params mib.mind_packets in
+  (*  - check constructor types *)
+  Array.iter (typecheck_one_inductive env_ar params) mib.mind_packets;
+  (* check the inferred subtyping relation *)
+  let () =
+    match mib.mind_universes with
+    | Monomorphic_ind _ | Polymorphic_ind _ -> ()
+    | Cumulative_ind acumi ->
+      check_subtyping acumi params env_ar mib.mind_packets
+  in
+  (* check mind_nparams_rec: positivity condition *)
+  let packets = Array.map (fun p -> (p.mind_typename, Array.to_list p.mind_consnames, p.mind_user_lc, (p.mind_arity_ctxt,()))) mib.mind_packets in
+  let _ = Indtypes.check_positivity ~chkpos:true kn env_ar mib.mind_params_ctxt mib.mind_finite packets in
+  (* check mind_equiv... *)
+  (* Now we can add the inductive *)
+  add_mind kn mib env