diff options
Diffstat (limited to 'pretyping/indrec.ml')
| -rw-r--r-- | pretyping/indrec.ml | 138 |
1 files changed, 80 insertions, 58 deletions
diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml index 39aeb41f..3143f8a5 100644 --- a/pretyping/indrec.ml +++ b/pretyping/indrec.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* * 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 *) +(* // * 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) *) (************************************************************************) (* File initially created by Christine Paulin, 1996 *) @@ -18,6 +20,7 @@ open Libnames open Globnames open Nameops open Term +open Constr open Vars open Namegen open Declarations @@ -27,19 +30,30 @@ open Inductiveops open Environ open Reductionops open Nametab -open Sigma.Notations open Context.Rel.Declaration type dep_flag = bool (* Errors related to recursors building *) type recursion_scheme_error = - | NotAllowedCaseAnalysis of (*isrec:*) bool * sorts * pinductive + | NotAllowedCaseAnalysis of (*isrec:*) bool * Sorts.t * pinductive | NotMutualInScheme of inductive * inductive | NotAllowedDependentAnalysis of (*isrec:*) bool * inductive exception RecursionSchemeError of recursion_scheme_error +let named_hd env t na = named_hd env Evd.empty (EConstr.of_constr t) na +let name_assumption env = function +| LocalAssum (na,t) -> LocalAssum (named_hd env t na, t) +| LocalDef (na,c,t) -> LocalDef (named_hd env c na, c, t) + +let mkLambda_or_LetIn_name env d b = mkLambda_or_LetIn (name_assumption env d) b +let mkProd_or_LetIn_name env d b = mkProd_or_LetIn (name_assumption env d) b +let mkLambda_name env (n,a,b) = mkLambda_or_LetIn_name env (LocalAssum (n,a)) b +let mkProd_name env (n,a,b) = mkProd_or_LetIn_name env (LocalAssum (n,a)) b +let it_mkProd_or_LetIn_name env b l = List.fold_left (fun c d -> mkProd_or_LetIn_name env d c) b l +let it_mkLambda_or_LetIn_name env b l = List.fold_left (fun c d -> mkLambda_or_LetIn_name env d c) b l + let make_prod_dep dep env = if dep then mkProd_name env else mkProd let mkLambda_string s t c = mkLambda (Name (Id.of_string s), t, c) @@ -55,7 +69,7 @@ let is_private mib = let check_privacy_block mib = if is_private mib then - errorlabstrm ""(str"case analysis on a private inductive type") + user_err (str"case analysis on a private inductive type") (**********************************************************************) (* Building case analysis schemes *) @@ -63,7 +77,7 @@ let check_privacy_block mib = let mis_make_case_com dep env sigma (ind, u as pind) (mib,mip as specif) kind = let lnamespar = Vars.subst_instance_context u mib.mind_params_ctxt in - let indf = make_ind_family(pind, Context.Rel.to_extended_list 0 lnamespar) in + let indf = make_ind_family(pind, Context.Rel.to_extended_list mkRel 0 lnamespar) in let constrs = get_constructors env indf in let projs = get_projections env indf in @@ -93,8 +107,8 @@ let mis_make_case_com dep env sigma (ind, u as pind) (mib,mip as specif) kind = let pbody = appvect (mkRel (ndepar + nbprod), - if dep then Context.Rel.to_extended_vect 0 deparsign - else Context.Rel.to_extended_vect 1 arsign) in + if dep then Context.Rel.to_extended_vect mkRel 0 deparsign + else Context.Rel.to_extended_vect mkRel 1 arsign) in let p = it_mkLambda_or_LetIn_name env' ((if dep then mkLambda_name env' else mkLambda) @@ -118,18 +132,19 @@ let mis_make_case_com dep env sigma (ind, u as pind) (mib,mip as specif) kind = it_mkLambda_or_LetIn_name env' obj deparsign else let cs = lift_constructor (k+1) constrs.(k) in - let t = build_branch_type env dep (mkRel (k+1)) cs in + let t = build_branch_type env sigma dep (mkRel (k+1)) cs in mkLambda_string "f" t (add_branch (push_rel (LocalAssum (Anonymous, t)) env) (k+1)) in - let Sigma (s, sigma, p) = Sigma.fresh_sort_in_family ~rigid:Evd.univ_flexible_alg env sigma kind in - let typP = make_arity env' dep indf s in + let (sigma, s) = Evd.fresh_sort_in_family ~rigid:Evd.univ_flexible_alg env sigma kind in + let typP = make_arity env' sigma dep indf s in + let typP = EConstr.Unsafe.to_constr typP in let c = it_mkLambda_or_LetIn_name env (mkLambda_string "P" typP (add_branch (push_rel (LocalAssum (Anonymous,typP)) env') 0)) lnamespar in - Sigma (c, sigma, p) + (sigma, c) (* check if the type depends recursively on one of the inductive scheme *) @@ -153,8 +168,10 @@ let type_rec_branch is_rec dep env sigma (vargs,depPvect,decP) tyi cs recargs = let nparams = List.length vargs in let process_pos env depK pk = let rec prec env i sign p = - let p',largs = whd_allnolet_stack env sigma p in - match kind_of_term p' with + let p',largs = whd_allnolet_stack env sigma (EConstr.of_constr p) in + let p' = EConstr.Unsafe.to_constr p' in + let largs = List.map EConstr.Unsafe.to_constr largs in + match kind p' with | Prod (n,t,c) -> let d = LocalAssum (n,t) in make_prod env (n,t,prec (push_rel d env) (i+1) (d::sign) c) @@ -166,18 +183,19 @@ let type_rec_branch is_rec dep env sigma (vargs,depPvect,decP) tyi cs recargs = let base = applist (lift i pk,realargs) in if depK then Reduction.beta_appvect - base [|applist (mkRel (i+1), Context.Rel.to_extended_list 0 sign)|] + base [|applist (mkRel (i+1), Context.Rel.to_extended_list mkRel 0 sign)|] else base | _ -> - let t' = whd_all env sigma p in - if Term.eq_constr p' t' then assert false + let t' = whd_all env sigma (EConstr.of_constr p) in + let t' = EConstr.Unsafe.to_constr t' in + if Constr.equal p' t' then assert false else prec env i sign t' in prec env 0 [] in let rec process_constr env i c recargs nhyps li = - if nhyps > 0 then match kind_of_term c with + if nhyps > 0 then match kind c with | Prod (n,t,c_0) -> let (optionpos,rest) = match recargs with @@ -229,8 +247,10 @@ let type_rec_branch is_rec dep env sigma (vargs,depPvect,decP) tyi cs recargs = let make_rec_branch_arg env sigma (nparrec,fvect,decF) f cstr recargs = let process_pos env fk = let rec prec env i hyps p = - let p',largs = whd_allnolet_stack env sigma p in - match kind_of_term p' with + let p',largs = whd_allnolet_stack env sigma (EConstr.of_constr p) in + let p' = EConstr.Unsafe.to_constr p' in + let largs = List.map EConstr.Unsafe.to_constr largs in + match kind p' with | Prod (n,t,c) -> let d = LocalAssum (n,t) in mkLambda_name env (n,t,prec (push_rel d env) (i+1) (d::hyps) c) @@ -239,11 +259,12 @@ let make_rec_branch_arg env sigma (nparrec,fvect,decF) f cstr recargs = mkLetIn (n,b,t,prec (push_rel d env) (i+1) (d::hyps) c) | Ind _ -> let realargs = List.skipn nparrec largs - and arg = appvect (mkRel (i+1), Context.Rel.to_extended_vect 0 hyps) in + and arg = appvect (mkRel (i+1), Context.Rel.to_extended_vect mkRel 0 hyps) in applist(lift i fk,realargs@[arg]) | _ -> - let t' = whd_all env sigma p in - if Term.eq_constr t' p' then assert false + let t' = whd_all env sigma (EConstr.of_constr p) in + let t' = EConstr.Unsafe.to_constr t' in + if Constr.equal t' p' then assert false else prec env i hyps t' in prec env 0 [] @@ -261,7 +282,7 @@ let make_rec_branch_arg env sigma (nparrec,fvect,decF) f cstr recargs = | None -> mkLambda_name env (n,t,process_constr (push_rel d env) (i+1) - (whd_beta Evd.empty (applist (lift 1 f, [(mkRel 1)]))) + (EConstr.Unsafe.to_constr (whd_beta Evd.empty (EConstr.of_constr (applist (lift 1 f, [(mkRel 1)]))))) (cprest,rest)) | Some(_,f_0) -> let nF = lift (i+1+decF) f_0 in @@ -269,7 +290,7 @@ let make_rec_branch_arg env sigma (nparrec,fvect,decF) f cstr recargs = let arg = process_pos env' nF (lift 1 t) in mkLambda_name env (n,t,process_constr env' (i+1) - (whd_beta Evd.empty (applist (lift 1 f, [(mkRel 1); arg]))) + (EConstr.Unsafe.to_constr (whd_beta Evd.empty (EConstr.of_constr (applist (lift 1 f, [(mkRel 1); arg]))))) (cprest,rest))) | (LocalDef (n,c,t) as d)::cprest, rest -> mkLetIn @@ -277,13 +298,13 @@ let make_rec_branch_arg env sigma (nparrec,fvect,decF) f cstr recargs = process_constr (push_rel d env) (i+1) (lift 1 f) (cprest,rest)) | [],[] -> f - | _,[] | [],_ -> anomaly (Pp.str "process_constr") + | _,[] | [],_ -> anomaly (Pp.str "process_constr.") in process_constr env 0 f (List.rev cstr.cs_args, recargs) (* Main function *) -let mis_make_indrec env sigma listdepkind mib u = +let mis_make_indrec env sigma ?(force_mutual=false) listdepkind mib u = let nparams = mib.mind_nparams in let nparrec = mib.mind_nparams_rec in let evdref = ref sigma in @@ -317,7 +338,7 @@ let mis_make_indrec env sigma listdepkind mib u = (* arity in the context of the fixpoint, i.e. P1..P_nrec f1..f_nbconstruct *) - let args = Context.Rel.to_extended_list (nrec+nbconstruct) lnamesparrec in + let args = Context.Rel.to_extended_list mkRel (nrec+nbconstruct) lnamesparrec in let indf = make_ind_family((indi,u),args) in let arsign,_ = get_arity env indf in @@ -331,15 +352,15 @@ let mis_make_indrec env sigma listdepkind mib u = (* constructors in context of the Cases expr, i.e. P1..P_nrec f1..f_nbconstruct F_1..F_nrec a_1..a_nar x:I *) - let args' = Context.Rel.to_extended_list (dect+nrec) lnamesparrec in - let args'' = Context.Rel.to_extended_list ndepar lnonparrec in + let args' = Context.Rel.to_extended_list mkRel (dect+nrec) lnamesparrec in + let args'' = Context.Rel.to_extended_list mkRel ndepar lnonparrec in let indf' = make_ind_family((indi,u),args'@args'') in let branches = let constrs = get_constructors env indf' in let fi = Termops.rel_vect (dect-i-nctyi) nctyi in let vecfi = Array.map - (fun f -> appvect (f, Context.Rel.to_extended_vect ndepar lnonparrec)) + (fun f -> appvect (f, Context.Rel.to_extended_vect mkRel ndepar lnonparrec)) fi in Array.map3 @@ -360,9 +381,9 @@ let mis_make_indrec env sigma listdepkind mib u = let deparsign' = LocalAssum (Anonymous,depind')::arsign' in let pargs = - let nrpar = Context.Rel.to_extended_list (2*ndepar) lnonparrec - and nrar = if dep then Context.Rel.to_extended_list 0 deparsign' - else Context.Rel.to_extended_list 1 arsign' + let nrpar = Context.Rel.to_extended_list mkRel (2*ndepar) lnonparrec + and nrar = if dep then Context.Rel.to_extended_list mkRel 0 deparsign' + else Context.Rel.to_extended_list mkRel 1 arsign' in nrpar@nrar in @@ -378,9 +399,10 @@ let mis_make_indrec env sigma listdepkind mib u = arsign' in let obj = - Inductiveops.make_case_or_project env indf ci pred - (mkRel 1) branches + Inductiveops.make_case_or_project env !evdref indf ci (EConstr.of_constr pred) + (EConstr.mkRel 1) (Array.map EConstr.of_constr branches) in + let obj = EConstr.to_constr !evdref obj in it_mkLambda_or_LetIn_name env obj (Termops.lift_rel_context nrec deparsign) in @@ -389,8 +411,8 @@ let mis_make_indrec env sigma listdepkind mib u = let typtyi = let concl = - let pargs = if dep then Context.Rel.to_extended_vect 0 deparsign - else Context.Rel.to_extended_vect 1 arsign + let pargs = if dep then Context.Rel.to_extended_vect mkRel 0 deparsign + else Context.Rel.to_extended_vect mkRel 1 arsign in appvect (mkRel (nbconstruct+ndepar+nonrecpar+j),pargs) in it_mkProd_or_LetIn_name env concl @@ -417,7 +439,7 @@ let mis_make_indrec env sigma listdepkind mib u = else let recarg = (dest_subterms recargsvec.(tyi)).(j) in let recarg = recargpar@recarg in - let vargs = Context.Rel.to_extended_list (nrec+i+j) lnamesparrec in + let vargs = Context.Rel.to_extended_list mkRel (nrec+i+j) lnamesparrec in let cs = get_constructor ((indi,u),mibi,mipi,vargs) (j+1) in let p_0 = type_rec_branch @@ -431,12 +453,13 @@ let mis_make_indrec env sigma listdepkind mib u = in let rec put_arity env i = function | ((indi,u),_,_,dep,kinds)::rest -> - let indf = make_ind_family ((indi,u), Context.Rel.to_extended_list i lnamesparrec) in + let indf = make_ind_family ((indi,u), Context.Rel.to_extended_list mkRel i lnamesparrec) in let s = Evarutil.evd_comb1 (Evd.fresh_sort_in_family ~rigid:Evd.univ_flexible_alg env) evdref kinds in - let typP = make_arity env dep indf s in + let typP = make_arity env !evdref dep indf s in + let typP = EConstr.Unsafe.to_constr typP in mkLambda_string "P" typP (put_arity (push_rel (LocalAssum (Anonymous,typP)) env) (i+1) rest) | [] -> @@ -446,7 +469,7 @@ let mis_make_indrec env sigma listdepkind mib u = (* Body on make_one_rec *) let ((indi,u),mibi,mipi,dep,kind) = List.nth listdepkind p in - if (mis_is_recursive_subset + if force_mutual || (mis_is_recursive_subset (List.map (fun ((indi,u),_,_,_,_) -> snd indi) listdepkind) mipi.mind_recargs) then @@ -454,10 +477,9 @@ let mis_make_indrec env sigma listdepkind mib u = it_mkLambda_or_LetIn_name env (put_arity env' 0 listdepkind) lnamesparrec else - let sigma = Sigma.Unsafe.of_evar_map !evdref in - let Sigma (c, sigma, _) = mis_make_case_com dep env sigma (indi,u) (mibi,mipi) kind in - let evd' = Sigma.to_evar_map sigma in - evdref := evd'; c + let evd = !evdref in + let (evd, c) = mis_make_case_com dep env evd (indi,u) (mibi,mipi) kind in + evdref := evd; c in (* Body of mis_make_indrec *) !evdref, List.init nrec make_one_rec @@ -486,7 +508,7 @@ let build_case_analysis_scheme_default env sigma pity kind = [rec] by [s] *) let change_sort_arity sort = - let rec drec a = match kind_of_term a with + let rec drec a = match kind a with | Cast (c,_,_) -> drec c | Prod (n,t,c) -> let s, c' = drec c in s, mkProd (n, t, c') | LetIn (n,b,t,c) -> let s, c' = drec c in s, mkLetIn (n,b,t,c') @@ -500,7 +522,7 @@ let change_sort_arity sort = let weaken_sort_scheme env evd set sort npars term ty = let evdref = ref evd in let rec drec np elim = - match kind_of_term elim with + match kind elim with | Prod (n,t,c) -> if Int.equal np 0 then let osort, t' = change_sort_arity sort t in @@ -512,7 +534,7 @@ let weaken_sort_scheme env evd set sort npars term ty = mkProd (n, t, c'), mkLambda (n, t, term') | LetIn (n,b,t,c) -> let c',term' = drec np c in mkLetIn (n,b,t,c'), mkLetIn (n,b,t,term') - | _ -> anomaly ~label:"weaken_sort_scheme" (Pp.str "wrong elimination type") + | _ -> anomaly ~label:"weaken_sort_scheme" (Pp.str "wrong elimination type.") in let ty, term = drec npars ty in !evdref, ty, term @@ -536,7 +558,7 @@ let check_arities env listdepkind = [] listdepkind in true -let build_mutual_induction_scheme env sigma = function +let build_mutual_induction_scheme env sigma ?(force_mutual=false) = function | ((mind,u),dep,s)::lrecspec -> let (mib,mip) = lookup_mind_specif env mind in if dep && not (Inductiveops.has_dependent_elim mib) then @@ -547,7 +569,7 @@ let build_mutual_induction_scheme env sigma = function (List.map (function ((mind',u'),dep',s') -> let (sp',_) = mind' in - if eq_mind sp sp' then + if MutInd.equal sp sp' then let (mibi',mipi') = lookup_mind_specif env mind' in ((mind',u'),mibi',mipi',dep',s') else @@ -555,8 +577,8 @@ let build_mutual_induction_scheme env sigma = function lrecspec) in let _ = check_arities env listdepkind in - mis_make_indrec env sigma listdepkind mib u - | _ -> anomaly (Pp.str "build_induction_scheme expects a non empty list of inductive types") + mis_make_indrec env sigma ~force_mutual listdepkind mib u + | _ -> anomaly (Pp.str "build_induction_scheme expects a non empty list of inductive types.") let build_induction_scheme env sigma pind dep kind = let (mib,mip) = lookup_mind_specif env (fst pind) in @@ -586,7 +608,7 @@ let lookup_eliminator ind_sp s = (* Try first to get an eliminator defined in the same section as the *) (* inductive type *) try - let cst =Global.constant_of_delta_kn (make_kn mp dp (Label.of_id id)) in + let cst =Global.constant_of_delta_kn (KerName.make mp dp (Label.of_id id)) in let _ = Global.lookup_constant cst in ConstRef cst with Not_found -> @@ -594,9 +616,9 @@ let lookup_eliminator ind_sp s = (* using short name (e.g. for "eq_rec") *) try Nametab.locate (qualid_of_ident id) with Not_found -> - errorlabstrm "default_elim" + user_err ~hdr:"default_elim" (strbrk "Cannot find the elimination combinator " ++ - pr_id id ++ strbrk ", the elimination of the inductive definition " ++ + Id.print id ++ strbrk ", the elimination of the inductive definition " ++ pr_global_env Id.Set.empty (IndRef ind_sp) ++ strbrk " on sort " ++ Termops.pr_sort_family s ++ strbrk " is probably not allowed.") |