diff options
Diffstat (limited to 'pretyping/indrec.ml')
-rw-r--r-- | pretyping/indrec.ml | 281 |
1 files changed, 160 insertions, 121 deletions
diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml index c7cdb302..54d47fbe 100644 --- a/pretyping/indrec.ml +++ b/pretyping/indrec.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -11,66 +11,75 @@ (* This file builds various inductive schemes *) open Pp +open Errors open Util open Names open Libnames +open Globnames open Nameops open Term +open Vars +open Context open Namegen open Declarations -open Entries +open Declareops open Inductive open Inductiveops open Environ open Reductionops -open Typeops -open Type_errors -open Safe_typing open Nametab -open Sign type dep_flag = bool (* Errors related to recursors building *) type recursion_scheme_error = - | NotAllowedCaseAnalysis of (*isrec:*) bool * sorts * inductive + | NotAllowedCaseAnalysis of (*isrec:*) bool * sorts * pinductive | NotMutualInScheme of inductive * inductive exception RecursionSchemeError of recursion_scheme_error 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) +let mkLambda_string s t c = mkLambda (Name (Id.of_string s), t, c) (*******************************************) (* Building curryfied elimination *) (*******************************************) +let is_private mib = + match mib.mind_private with + | Some true -> true + | _ -> false + +let check_privacy_block mib = + if is_private mib then + errorlabstrm ""(str"case analysis on a private inductive type") + (**********************************************************************) (* Building case analysis schemes *) (* Christine Paulin, 1996 *) -let mis_make_case_com dep env sigma ind (mib,mip as specif) kind = - let lnamespar = List.map - (fun (n, c, t) -> (n, c, Termops.refresh_universes t)) - mib.mind_params_ctxt +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, Termops.extended_rel_list 0 lnamespar) in + let constrs = get_constructors env indf in + let projs = get_projections env indf in + + let () = if Option.is_empty projs then check_privacy_block mib in + let () = + if not (Sorts.List.mem kind (elim_sorts specif)) then + raise + (RecursionSchemeError + (NotAllowedCaseAnalysis (false, fst (Universes.fresh_sort_in_family env kind), pind))) in + let ndepar = mip.mind_nrealdecls + 1 in - if not (List.mem kind (elim_sorts specif)) then - raise - (RecursionSchemeError - (NotAllowedCaseAnalysis (false, Termops.new_sort_in_family kind, ind))); - - let ndepar = mip.mind_nrealargs_ctxt + 1 in - - (* Pas génant car env ne sert pas à typer mais juste à renommer les Anonym *) - (* mais pas très joli ... (mais manque get_sort_of à ce niveau) *) + (* Pas génant car env ne sert pas à typer mais juste à renommer les Anonym *) + (* mais pas très joli ... (mais manque get_sort_of à ce niveau) *) let env' = push_rel_context lnamespar env in - let indf = make_ind_family(ind, Termops.extended_rel_list 0 lnamespar) in - let constrs = get_constructors env indf in let rec add_branch env k = - if k = Array.length mip.mind_consnames then + if Int.equal k (Array.length mip.mind_consnames) then let nbprod = k+1 in let indf' = lift_inductive_family nbprod indf in @@ -78,7 +87,7 @@ let mis_make_case_com dep env sigma ind (mib,mip as specif) kind = let depind = build_dependent_inductive env indf' in let deparsign = (Anonymous,None,depind)::arsign in - let ci = make_case_info env ind RegularStyle in + let ci = make_case_info env (fst pind) RegularStyle in let pbody = appvect (mkRel (ndepar + nbprod), @@ -90,21 +99,34 @@ let mis_make_case_com dep env sigma ind (mib,mip as specif) kind = (Anonymous,depind,pbody)) arsign in - it_mkLambda_or_LetIn_name env' - (mkCase (ci, lift ndepar p, - mkRel 1, - Termops.rel_vect ndepar k)) - deparsign + let obj = + match projs with + | None -> mkCase (ci, lift ndepar p, mkRel 1, + Termops.rel_vect ndepar k) + | Some ps -> + let term = + mkApp (mkRel 2, + Array.map + (fun p -> mkProj (Projection.make p true, mkRel 1)) ps) in + if dep then + let ty = mkApp (mkRel 3, [| mkRel 1 |]) in + mkCast (term, DEFAULTcast, ty) + else term + in + 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 mkLambda_string "f" t (add_branch (push_rel (Anonymous, None, t) env) (k+1)) in - let typP = make_arity env' dep indf (Termops.new_sort_in_family kind) in - it_mkLambda_or_LetIn_name env + let sigma, s = Evd.fresh_sort_in_family ~rigid:Evd.univ_flexible_alg env sigma kind in + let typP = make_arity env' dep indf s in + let c = + it_mkLambda_or_LetIn_name env (mkLambda_string "P" typP - (add_branch (push_rel (Anonymous,None,typP) env') 0)) lnamespar + (add_branch (push_rel (Anonymous,None,typP) env') 0)) lnamespar + in sigma, c (* check if the type depends recursively on one of the inductive scheme *) @@ -137,7 +159,7 @@ let type_rec_branch is_rec dep env sigma (vargs,depPvect,decP) tyi cs recargs = let d = (n,Some b,t) in mkLetIn (n,b,t,prec (push_rel d env) (i+1) (d::sign) c) | Ind (_,_) -> - let realargs = list_skipn nparams largs in + let realargs = List.skipn nparams largs in let base = applist (lift i pk,realargs) in if depK then Reduction.beta_appvect @@ -158,7 +180,7 @@ let type_rec_branch is_rec dep env sigma (vargs,depPvect,decP) tyi cs recargs = (match dest_recarg ra with | Mrec (_,j) when is_rec -> (depPvect.(j),rest) | Imbr _ -> - Flags.if_warn msg_warning (str "Ignoring recursive call"); + msg_warning (strbrk "Ignoring recursive call"); (None,rest) | _ -> (None, rest)) in @@ -172,7 +194,7 @@ let type_rec_branch is_rec dep env sigma (vargs,depPvect,decP) tyi cs recargs = let nP = lift (i+1+decP) p in let env' = push_rel (n,None,t) env in let t_0 = process_pos env' dep' nP (lift 1 t) in - make_prod_dep (dep or dep') env + make_prod_dep (dep || dep') env (n,t, mkArrow t_0 (process_constr @@ -186,9 +208,9 @@ let type_rec_branch is_rec dep env sigma (vargs,depPvect,decP) tyi cs recargs = | _ -> assert false else if dep then - let realargs = List.map (fun k -> mkRel (i-k)) (List.rev li) in + let realargs = List.rev_map (fun k -> mkRel (i-k)) li in let params = List.map (lift i) vargs in - let co = applist (mkConstruct cs.cs_cstr,params@realargs) in + let co = applist (mkConstructU cs.cs_cstr,params@realargs) in Reduction.beta_appvect c [|co|] else c in @@ -212,14 +234,14 @@ let make_rec_branch_arg env sigma (nparrec,fvect,decF) f cstr recargs = let d = (n,Some b,t) in mkLetIn (n,b,t,prec (push_rel d env) (i+1) (d::hyps) c) | Ind _ -> - let realargs = list_skipn nparrec largs + let realargs = List.skipn nparrec largs and arg = appvect (mkRel (i+1), Termops.extended_rel_vect 0 hyps) in applist(lift i fk,realargs@[arg]) | _ -> assert false in prec env 0 [] in - (* ici, cstrprods est la liste des produits du constructeur instantié *) + (* ici, cstrprods est la liste des produits du constructeur instantié *) let rec process_constr env i f = function | (n,None,t as d)::cprest, recarg::rest -> let optionpos = @@ -248,7 +270,7 @@ 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 "process_constr" + | _,[] | [],_ -> anomaly (Pp.str "process_constr") in process_constr env 0 f (List.rev cstr.cs_args, recargs) @@ -264,21 +286,21 @@ let context_chop k ctx = | (_, []) -> failwith "context_chop" in chop_aux [] (k,ctx) - (* Main function *) -let mis_make_indrec env sigma listdepkind mib = +let mis_make_indrec env sigma listdepkind mib u = let nparams = mib.mind_nparams in - let nparrec = mib. mind_nparams_rec in + let nparrec = mib.mind_nparams_rec in + let evdref = ref sigma in let lnonparrec,lnamesparrec = - context_chop (nparams-nparrec) mib.mind_params_ctxt in + context_chop (nparams-nparrec) (Vars.subst_instance_context u mib.mind_params_ctxt) in let nrec = List.length listdepkind in let depPvec = - Array.create mib.mind_ntypes (None : (bool * constr) option) in + Array.make mib.mind_ntypes (None : (bool * constr) option) in let _ = let rec assign k = function | [] -> () - | (indi,mibi,mipi,dep,_)::rest -> + | ((indi,u),mibi,mipi,dep,_)::rest -> (Array.set depPvec (snd indi) (Some(dep,mkRel k)); assign (k-1) rest) in @@ -287,12 +309,12 @@ let mis_make_indrec env sigma listdepkind mib = Array.map (fun mip -> mip.mind_recargs) mib.mind_packets in (* recarg information for non recursive parameters *) let rec recargparn l n = - if n = 0 then l else recargparn (mk_norec::l) (n-1) in + if Int.equal n 0 then l else recargparn (mk_norec::l) (n-1) in let recargpar = recargparn [] (nparams-nparrec) in let make_one_rec p = let makefix nbconstruct = let rec mrec i ln ltyp ldef = function - | (indi,mibi,mipi,dep,_)::rest -> + | ((indi,u),mibi,mipi,dep,_)::rest -> let tyi = snd indi in let nctyi = Array.length mipi.mind_consnames in (* nb constructeurs du type*) @@ -300,7 +322,7 @@ let mis_make_indrec env sigma listdepkind mib = (* arity in the context of the fixpoint, i.e. P1..P_nrec f1..f_nbconstruct *) let args = Termops.extended_rel_list (nrec+nbconstruct) lnamesparrec in - let indf = make_ind_family(indi,args) in + let indf = make_ind_family((indi,u),args) in let arsign,_ = get_arity env indf in let depind = build_dependent_inductive env indf in @@ -315,7 +337,7 @@ let mis_make_indrec env sigma listdepkind mib = P1..P_nrec f1..f_nbconstruct F_1..F_nrec a_1..a_nar x:I *) let args' = Termops.extended_rel_list (dect+nrec) lnamesparrec in let args'' = Termops.extended_rel_list ndepar lnonparrec in - let indf' = make_ind_family(indi,args'@args'') in + let indf' = make_ind_family((indi,u),args'@args'') in let branches = let constrs = get_constructors env indf' in @@ -324,8 +346,8 @@ let mis_make_indrec env sigma listdepkind mib = (fun f -> appvect (f, Termops.extended_rel_vect ndepar lnonparrec)) fi in - array_map3 - (make_rec_branch_arg env sigma + Array.map3 + (make_rec_branch_arg env !evdref (nparrec,depPvec,larsign)) vecfi constrs (dest_subterms recargsvec.(tyi)) in @@ -359,10 +381,27 @@ let mis_make_indrec env sigma listdepkind mib = (Anonymous,depind',concl)) arsign' in - it_mkLambda_or_LetIn_name env - (mkCase (ci, pred, - mkRel 1, - branches)) + let obj = + let projs = get_projections env indf in + match projs with + | None -> (mkCase (ci, pred, + mkRel 1, + branches)) + | Some ps -> + let branch = branches.(0) in + let ctx, br = decompose_lam_assum branch in + let n, subst = + List.fold_right (fun (na,b,t) (i, subst) -> + if b == None then + let t = mkProj (Projection.make ps.(i) true, mkRel 1) in + (i + 1, t :: subst) + else (i, mkRel 0 :: subst)) + ctx (0, []) + in + let term = substl subst br in + term + in + it_mkLambda_or_LetIn_name env obj (Termops.lift_rel_context nrec deparsign) in @@ -383,26 +422,26 @@ let mis_make_indrec env sigma listdepkind mib = let fixn = Array.of_list (List.rev ln) in let fixtyi = Array.of_list (List.rev ltyp) in let fixdef = Array.of_list (List.rev ldef) in - let names = Array.create nrec (Name(id_of_string "F")) in + let names = Array.make nrec (Name(Id.of_string "F")) in mkFix ((fixn,p),(names,fixtyi,fixdef)) in mrec 0 [] [] [] in let rec make_branch env i = function - | (indi,mibi,mipi,dep,_)::rest -> + | ((indi,u),mibi,mipi,dep,_)::rest -> let tyi = snd indi in let nconstr = Array.length mipi.mind_consnames in let rec onerec env j = - if j = nconstr then + if Int.equal j nconstr then make_branch env (i+j) rest else let recarg = (dest_subterms recargsvec.(tyi)).(j) in let recarg = recargpar@recarg in let vargs = Termops.extended_rel_list (nrec+i+j) lnamesparrec in - let cs = get_constructor (indi,mibi,mipi,vargs) (j+1) in + let cs = get_constructor ((indi,u),mibi,mipi,vargs) (j+1) in let p_0 = type_rec_branch - true dep env sigma (vargs,depPvec,i+j) tyi cs recarg + true dep env !evdref (vargs,depPvec,i+j) tyi cs recarg in mkLambda_string "f" p_0 (onerec (push_rel (Anonymous,None,p_0) env) (j+1)) @@ -411,9 +450,13 @@ let mis_make_indrec env sigma listdepkind mib = makefix i listdepkind in let rec put_arity env i = function - | (indi,_,_,dep,kinds)::rest -> - let indf = make_ind_family (indi, Termops.extended_rel_list i lnamesparrec) in - let typP = make_arity env dep indf (Termops.new_sort_in_family kinds) in + | ((indi,u),_,_,dep,kinds)::rest -> + let indf = make_ind_family ((indi,u), Termops.extended_rel_list 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 mkLambda_string "P" typP (put_arity (push_rel (Anonymous,None,typP) env) (i+1) rest) | [] -> @@ -421,33 +464,38 @@ let mis_make_indrec env sigma listdepkind mib = in (* Body on make_one_rec *) - let (indi,mibi,mipi,dep,kind) = List.nth listdepkind p in + let ((indi,u),mibi,mipi,dep,kind) = List.nth listdepkind p in if (mis_is_recursive_subset - (List.map (fun (indi,_,_,_,_) -> snd indi) listdepkind) + (List.map (fun ((indi,u),_,_,_,_) -> snd indi) listdepkind) mipi.mind_recargs) then let env' = push_rel_context lnamesparrec env in it_mkLambda_or_LetIn_name env (put_arity env' 0 listdepkind) lnamesparrec else - mis_make_case_com dep env sigma indi (mibi,mipi) kind + let evd', c = mis_make_case_com dep env !evdref (indi,u) (mibi,mipi) kind in + evdref := evd'; c in (* Body of mis_make_indrec *) - list_tabulate make_one_rec nrec + !evdref, List.init nrec make_one_rec (**********************************************************************) (* This builds elimination predicate for Case tactic *) -let build_case_analysis_scheme env sigma ity dep kind = - let (mib,mip) = lookup_mind_specif env ity in - mis_make_case_com dep env sigma ity (mib,mip) kind +let build_case_analysis_scheme env sigma pity dep kind = + let (mib,mip) = lookup_mind_specif env (fst pity) in + mis_make_case_com dep env sigma pity (mib,mip) kind -let build_case_analysis_scheme_default env sigma ity kind = - let (mib,mip) = lookup_mind_specif env ity in - let dep = inductive_sort_family mip <> InProp in - mis_make_case_com dep env sigma ity (mib,mip) kind +let is_in_prop mip = + match inductive_sort_family mip with + | InProp -> true + | _ -> false +let build_case_analysis_scheme_default env sigma pity kind = + let (mib,mip) = lookup_mind_specif env (fst pity) in + let dep = not (is_in_prop mip) in + mis_make_case_com dep env sigma pity (mib,mip) kind (**********************************************************************) (* [modify_sort_scheme s rec] replaces the sort of the scheme @@ -456,87 +504,78 @@ let build_case_analysis_scheme_default env sigma ity kind = let change_sort_arity sort = let rec drec a = match kind_of_term a with | Cast (c,_,_) -> drec c - | Prod (n,t,c) -> mkProd (n, t, drec c) - | LetIn (n,b,t,c) -> mkLetIn (n,b, t, drec c) - | Sort _ -> mkSort sort + | 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') + | Sort s -> s, mkSort sort | _ -> assert false in drec -(* [npar] is the number of expected arguments (then excluding letin's) *) -let modify_sort_scheme sort = - let rec drec npar elim = - match kind_of_term elim with - | Lambda (n,t,c) -> - if npar = 0 then - mkLambda (n, change_sort_arity sort t, c) - else - mkLambda (n, t, drec (npar-1) c) - | LetIn (n,b,t,c) -> mkLetIn (n,b,t,drec npar c) - | _ -> anomaly "modify_sort_scheme: wrong elimination type" - in - drec - (* Change the sort in the type of an inductive definition, builds the corresponding eta-expanded term *) -let weaken_sort_scheme sort npars term = +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 | Prod (n,t,c) -> - if np = 0 then - let t' = change_sort_arity sort t in - mkProd (n, t', c), - mkLambda (n, t', mkApp(term,Termops.rel_vect 0 (npars+1))) + if Int.equal np 0 then + let osort, t' = change_sort_arity sort t in + evdref := (if set then Evd.set_eq_sort else Evd.set_leq_sort) env !evdref sort osort; + mkProd (n, t', c), + mkLambda (n, t', mkApp(term,Termops.rel_vect 0 (npars+1))) else let c',term' = drec (np-1) c in 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 "weaken_sort_scheme: wrong elimination type" + | _ -> anomaly ~label:"weaken_sort_scheme" (Pp.str "wrong elimination type") in - drec npars + let ty, term = drec npars ty in + !evdref, ty, term (**********************************************************************) (* Interface to build complex Scheme *) (* Check inductive types only occurs once (otherwise we obtain a meaning less scheme) *) -let check_arities listdepkind = +let check_arities env listdepkind = let _ = List.fold_left - (fun ln ((_,ni as mind),mibi,mipi,dep,kind) -> + (fun ln (((_,ni as mind),u),mibi,mipi,dep,kind) -> let kelim = elim_sorts (mibi,mipi) in - if not (List.exists ((=) kind) kelim) then raise + if not (Sorts.List.mem kind kelim) then raise (RecursionSchemeError - (NotAllowedCaseAnalysis (true, Termops.new_sort_in_family kind,mind))) - else if List.mem ni ln then raise + (NotAllowedCaseAnalysis (true, fst (Universes.fresh_sort_in_family env + kind),(mind,u)))) + else if Int.List.mem ni ln then raise (RecursionSchemeError (NotMutualInScheme (mind,mind))) else ni::ln) [] listdepkind in true let build_mutual_induction_scheme env sigma = function - | (mind,dep,s)::lrecspec -> - let (mib,mip) = Global.lookup_inductive mind in + | ((mind,u),dep,s)::lrecspec -> + let (mib,mip) = lookup_mind_specif env mind in let (sp,tyi) = mind in let listdepkind = - (mind,mib,mip,dep,s):: + ((mind,u),mib,mip,dep,s):: (List.map - (function (mind',dep',s') -> + (function ((mind',u'),dep',s') -> let (sp',_) = mind' in - if sp=sp' then + if eq_mind sp sp' then let (mibi',mipi') = lookup_mind_specif env mind' in - (mind',mibi',mipi',dep',s') + ((mind',u'),mibi',mipi',dep',s') else raise (RecursionSchemeError (NotMutualInScheme (mind,mind')))) lrecspec) in - let _ = check_arities listdepkind in - mis_make_indrec env sigma listdepkind mib - | _ -> anomaly "build_induction_scheme expects a non empty list of inductive types" + 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") -let build_induction_scheme env sigma ind dep kind = - let (mib,mip) = lookup_mind_specif env ind in - List.hd (mis_make_indrec env sigma [(ind,mib,mip,dep,kind)] mib) +let build_induction_scheme env sigma pind dep kind = + let (mib,mip) = lookup_mind_specif env (fst pind) in + let sigma, l = mis_make_indrec env sigma [(pind,mib,mip,dep,kind)] mib (snd pind) in + sigma, List.hd l (*s Eliminations. *) @@ -559,17 +598,17 @@ 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 (make_kn mp dp (Label.of_id id)) in let _ = Global.lookup_constant cst in - mkConst cst + ConstRef cst with Not_found -> (* Then try to get a user-defined eliminator in some other places *) (* using short name (e.g. for "eq_rec") *) - try constr_of_global (Nametab.locate (qualid_of_ident id)) + try Nametab.locate (qualid_of_ident id) with Not_found -> errorlabstrm "default_elim" (strbrk "Cannot find the elimination combinator " ++ pr_id id ++ strbrk ", the elimination of the inductive definition " ++ - pr_global_env Idset.empty (IndRef ind_sp) ++ + pr_global_env Id.Set.empty (IndRef ind_sp) ++ strbrk " on sort " ++ Termops.pr_sort_family s ++ strbrk " is probably not allowed.") |