[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, 0 insertions, 382 deletions

diff --git a/checker/typeops.ml b/checker/typeops.ml
deleted file mode 100644
index e4c3f4ae4b..0000000000
--- a/checker/typeops.ml
+++ /dev/null
@@ -1,382 +0,0 @@
-(************************************************************************)
-(*         *   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 CErrors
-open Util
-open Names
-open Cic
-open Term
-open Reduction
-open Type_errors
-open Inductive
-open Environ
-
-let inductive_of_constructor = fst
-
-let conv_leq_vecti env v1 v2 =
-  Array.fold_left2_i
-    (fun i _ t1 t2 ->
-      (try conv_leq env t1 t2
-      with NotConvertible -> raise (NotConvertibleVect i)); ())
-    ()
-    v1
-    v2
-
-let check_constraints cst env = 
-  if Environ.check_constraints cst env then ()
-  else error_unsatisfied_constraints env cst
-
-(* This should be a type (a priori without intension to be an assumption) *)
-let type_judgment env (c,ty as j) =
-  match whd_all env ty with
-    | Sort s -> (c,s)
-    | _ -> error_not_type env j
-
-(* This should be a type intended to be assumed. The error message is *)
-(* not as useful as for [type_judgment]. *)
-let assumption_of_judgment env j =
-  try fst(type_judgment env j)
-  with TypeError _ ->
-    error_assumption env j
-
-(************************************************)
-(* Incremental typing rules: builds a typing judgement given the *)
-(* judgements for the subterms. *)
-
-(*s Type of sorts *)
-
-(* Prop and Set *)
-
-let judge_of_prop = Sort (Type Univ.type1_univ)
-
-(* Type of Type(i). *)
-
-let judge_of_type u = Sort (Type (Univ.super u))
-
-(*s Type of a de Bruijn index. *)
-
-let judge_of_relative env n =
-  try
-    let LocalAssum (_,typ) | LocalDef (_,_,typ) = lookup_rel n env in
-    lift n typ
-  with Not_found ->
-    error_unbound_rel env n
-
-(* Type of constants *)
-
-let judge_of_constant env (kn,u as cst) =
-  let _cb =
-    try lookup_constant kn env
-    with Not_found ->
-      failwith ("Cannot find constant: "^Constant.to_string kn)
-  in
-  let ty, cu = constant_type env cst in
-  let () = check_constraints cu env in
-    ty
-
-(* Type of an application. *)
-
-let judge_of_apply env (f,funj) argjv =
-  let rec apply_rec n typ = function
-    | [] -> typ
-    | (h,hj)::restjl ->
-        (match whd_all env typ with
-          | Prod (_,c1,c2) ->
-	      (try conv_leq env hj c1
-	      with NotConvertible ->
-		error_cant_apply_bad_type env (n,c1, hj) (f,funj) argjv);
-	      apply_rec (n+1) (subst1 h c2) restjl
-          | _ ->
-	      error_cant_apply_not_functional env (f,funj) argjv)
-  in
-  apply_rec 1 funj (Array.to_list argjv)
-
-(* Type of product *)
-
-let sort_of_product env domsort rangsort =
-  match (domsort, rangsort) with
-    (* Product rule (s,Prop,Prop) *)
-    | _,       Prop  -> rangsort
-    (* Product rule (Prop/Set,Set,Set) *)
-    | (Prop | Set),  Set -> rangsort
-    (* Product rule (Type,Set,?) *)
-    | Type u1, Set ->
-        if engagement env = ImpredicativeSet then
-          (* Rule is (Type,Set,Set) in the Set-impredicative calculus *)
-          rangsort
-        else
-          (* Rule is (Type_i,Set,Type_i) in the Set-predicative calculus *)
-          Type (Univ.sup u1 Univ.type0_univ)
-    (* Product rule (Prop,Type_i,Type_i) *)
-    | Set,  Type u2  -> Type (Univ.sup Univ.type0_univ u2)
-    (* Product rule (Prop,Type_i,Type_i) *)
-    | Prop, Type _  -> rangsort
-    (* Product rule (Type_i,Type_i,Type_i) *)
-    | Type u1, Type u2 -> Type (Univ.sup u1 u2)
-
-(* Type of a type cast *)
-
-(* [judge_of_cast env (c,typ1) (typ2,s)] implements the rule
-
-    env |- c:typ1    env |- typ2:s    env |- typ1 <= typ2
-    ---------------------------------------------------------------------
-         env |- c:typ2
-*)
-
-let judge_of_cast env (c,cj) k tj =
-  let conversion =
-    match k with
-    | VMcast | NATIVEcast -> vm_conv CUMUL
-    | DEFAULTcast -> conv_leq in
-  try
-    conversion env cj tj
-  with NotConvertible ->
-    error_actual_type env (c,cj) tj
-
-(* Inductive types. *)
-
-(* The type is parametric over the uniform parameters whose conclusion
-   is in Type; to enforce the internal constraints between the
-   parameters and the instances of Type occurring in the type of the
-   constructors, we use the level variables _statically_ assigned to
-   the conclusions of the parameters as mediators: e.g. if a parameter
-   has conclusion Type(alpha), static constraints of the form alpha<=v
-   exist between alpha and the Type's occurring in the constructor
-   types; when the parameters is finally instantiated by a term of
-   conclusion Type(u), then the constraints u<=alpha is computed in
-   the App case of execute; from this constraints, the expected
-   dynamic constraints of the form u<=v are enforced *)
-
-let judge_of_inductive_knowing_parameters env (ind,u) (paramstyp:constr array) =
-  let specif =
-    try lookup_mind_specif env ind
-    with Not_found ->
-      failwith ("Cannot find mutual inductive block: "^MutInd.to_string (fst ind))
-  in
-  type_of_inductive_knowing_parameters env (specif,u) paramstyp
-
-let judge_of_inductive env ind =
-  judge_of_inductive_knowing_parameters env ind [||]
-
-(* Constructors. *)
-
-let judge_of_constructor env (c,u) =
-  let ind = inductive_of_constructor c in
-  let specif =
-    try lookup_mind_specif env ind
-    with Not_found ->
-      failwith ("Cannot find mutual inductive block: "^MutInd.to_string (fst ind))
-  in
-  type_of_constructor (c,u) specif
-
-(* Case. *)
-
-let check_branch_types env (c,cj) (lfj,explft) =
-  try conv_leq_vecti env lfj explft
-  with
-      NotConvertibleVect i ->
-        error_ill_formed_branch env c i lfj.(i) explft.(i)
-    | Invalid_argument _ ->
-        error_number_branches env (c,cj) (Array.length explft)
-
-let judge_of_case env ci pj (c,cj) lfj =
-  let indspec =
-    try find_rectype env cj
-    with Not_found -> error_case_not_inductive env (c,cj) in
-  let _ = check_case_info env (fst (fst indspec)) ci in
-  let (bty,rslty) = type_case_branches env indspec pj c in
-  check_branch_types env (c,cj) (lfj,bty);
-  rslty
-
-(* Projection. *)
-
-let judge_of_projection env p c ct =
-  let pty = lookup_projection p env in
-  let (ind,u), args =
-    try find_rectype env ct
-    with Not_found -> error_case_not_inductive env (c, ct)
-  in
-  let ty = subst_instance_constr u pty in
-  substl (c :: List.rev args) ty
-
-(* Fixpoints. *)
-
-(* Checks the type of a general (co)fixpoint, i.e. without checking *)
-(* the specific guard condition. *)
-
-let type_fixpoint env lna lar lbody vdefj =
-  let lt = Array.length vdefj in
-  assert (Array.length lar = lt && Array.length lbody = lt);
-  try
-    conv_leq_vecti env vdefj (Array.map (fun ty -> lift lt ty) lar)
-  with NotConvertibleVect i ->
-    let vdefj = Array.map2 (fun b ty -> b,ty) lbody vdefj in
-    error_ill_typed_rec_body env i lna vdefj lar
-
-(************************************************************************)
-(************************************************************************)
-
-
-(* let refresh_arity env ar = *)
-(*   let ctxt, hd = decompose_prod_assum ar in *)
-(*   match hd with *)
-(*       Sort (Type u) when not (is_univ_variable u) -> *)
-(*         let u' = fresh_local_univ() in *)
-(*         let env' = add_constraints (enforce_leq u u' empty_constraint) env in *)
-(*         env', mkArity (ctxt,Type u') *)
-(*     | _ -> env, ar *)
-
-
-(* The typing machine. *)
-let rec execute env cstr =
-  match cstr with
-    (* Atomic terms *)
-    | Sort (Prop | Set) -> judge_of_prop
-
-    | Sort (Type u) -> judge_of_type u
-
-    | Rel n -> judge_of_relative env n
-
-    | Var _ -> anomaly (Pp.str "Section variable in Coqchk!")
-
-    | Const c -> judge_of_constant env c
-
-    (* Lambda calculus operators *)
-    | App (App (f,args),args') ->
-        execute env (App(f,Array.append args args'))
-
-    | App (f,args) ->
-        let jl = execute_array env args in
-	let j =
-	  match f with
-	    | Ind ind ->
-		judge_of_inductive_knowing_parameters env ind jl
-	    | _ ->
-		(* No template polymorphism *)
-		execute env f
-	in
-        let jl = Array.map2 (fun c ty -> c,ty) args jl in
-	judge_of_apply env (f,j) jl
-
-    | Proj (p, c) ->
-        let ct = execute env c in
-          judge_of_projection env p c ct
-
-    | Lambda (name,c1,c2) ->
-        let _ = execute_type env c1 in
-	let env1 = push_rel (LocalAssum (name,c1)) env in
-        let j' = execute env1 c2 in
-        Prod(name,c1,j')
-
-    | Prod (name,c1,c2) ->
-        let varj = execute_type env c1 in
-	let env1 = push_rel (LocalAssum (name,c1)) env in
-        let varj' = execute_type env1 c2 in
-	Sort (sort_of_product env varj varj')
-
-    | LetIn (name,c1,c2,c3) ->
-        let j1 = execute env c1 in
-        (* /!\ c2 can be an inferred type => refresh
-           (but the pushed type is still c2) *)
-        let _ =
-          let env',c2' = (* refresh_arity env *) env, c2 in
-          let _ = execute_type env' c2' in
-          judge_of_cast env' (c1,j1) DEFAULTcast c2' in
-        let env1 = push_rel (LocalDef (name,c1,c2)) env in
-        let j' = execute env1 c3 in
-        subst1 c1 j'
-
-    | Cast (c,k,t) ->
-        let cj = execute env c in
-        let _ = execute_type env t in
-	judge_of_cast env (c,cj) k t;
-        t
-
-    (* Inductive types *)
-    | Ind ind -> judge_of_inductive env ind
-
-    | Construct c -> judge_of_constructor env c
-
-    | Case (ci,p,c,lf) ->
-        let cj = execute env c in
-        let pj = execute env p in
-        let lfj = execute_array env lf in
-        judge_of_case env ci (p,pj) (c,cj) lfj
-    | Fix ((_,i as vni),recdef) ->
-        let fix_ty = execute_recdef env recdef i in
-        let fix = (vni,recdef) in
-        check_fix env fix;
-	fix_ty
-
-    | CoFix (i,recdef) ->
-        let fix_ty = execute_recdef env recdef i in
-        let cofix = (i,recdef) in
-        check_cofix env cofix;
-	fix_ty
-
-    (* Partial proofs: unsupported by the kernel *)
-    | Meta _ ->
-	anomaly (Pp.str "the kernel does not support metavariables.")
-
-    | Evar _ ->
-	anomaly (Pp.str "the kernel does not support existential variables.")
-
-and execute_type env constr =
-  let j = execute env constr in
-  snd (type_judgment env (constr,j))
-
-and execute_recdef env (names,lar,vdef) i =
-  let larj = execute_array env lar in
-  let larj = Array.map2 (fun c ty -> c,ty) lar larj in
-  let lara = Array.map (assumption_of_judgment env) larj in
-  let env1 = push_rec_types (names,lara,vdef) env in
-  let vdefj = execute_array env1 vdef in
-  type_fixpoint env1 names lara vdef vdefj;
-  lara.(i)
-
-and execute_array env = Array.map (execute env)
-
-(* Derived functions *)
-let infer env constr = execute env constr
-let infer_type env constr = execute_type env constr
-
-(* Typing of several terms. *)
-
-let check_ctxt env rels =
-  fold_rel_context (fun d env ->
-    match d with
-      | LocalAssum (_,ty) ->
-          let _ = infer_type env ty in
-          push_rel d env
-      | LocalDef (_,bd,ty) ->
-          let j1 = infer env bd in
-          let _ = infer env ty in
-          conv_leq env j1 ty;
-          push_rel d env)
-    rels ~init:env
-
-(* Polymorphic arities utils *)
-
-let check_kind env ar u =
-  match (snd (dest_prod env ar)) with
-  | Sort (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 =
-    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)