diff options
| -rw-r--r-- | kernel/inductive.ml | 18 | ||||
| -rw-r--r-- | kernel/inductive.mli | 2 | ||||
| -rw-r--r-- | kernel/typeops.ml | 2 | ||||
| -rw-r--r-- | library/indrec.ml | 8 | ||||
| -rw-r--r-- | pretyping/cases.ml | 25 | ||||
| -rw-r--r-- | pretyping/pretyping.ml | 6 | ||||
| -rw-r--r-- | tactics/equality.ml | 6 |
7 files changed, 36 insertions, 31 deletions
diff --git a/kernel/inductive.ml b/kernel/inductive.ml index 3436bf9620..257305b006 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -260,27 +260,35 @@ let get_arity (IndFamily (mispec,params)) = (* Functions to build standard types related to inductive *) +let local_rels = + let rec relrec acc n = function (* more recent arg in front *) + | [] -> acc + | (_,None,_)::l -> relrec (mkRel n :: acc) (n+1) l + | (_,Some _,_)::l -> relrec acc (n+1) l + in relrec [] 1 + let build_dependent_constructor cs = applist (mkMutConstruct cs.cs_cstr, - (List.map (lift cs.cs_nargs) cs.cs_params)@(rel_list 0 cs.cs_nargs)) + (List.map (lift cs.cs_nargs) cs.cs_params)@(local_rels cs.cs_args)) -let build_dependent_inductive (IndFamily (mis, params)) = +let build_dependent_inductive (IndFamily (mis, params) as indf) = + let arsign,_ = get_arity indf in let nrealargs = mis_nrealargs mis in applist (mkMutInd (mis_inductive mis), - (List.map (lift nrealargs) params)@(rel_list 0 nrealargs)) + (List.map (lift nrealargs) params)@(local_rels arsign)) (* builds the arity of an elimination predicate in sort [s] *) let make_arity env dep indf s = let (arsign,_) = get_arity indf in if dep then (* We need names everywhere *) - it_prod_name env + it_mkProd_or_LetIn_name env (mkArrow (build_dependent_inductive indf) (mkSort s)) arsign else (* No need to enforce names *) - prod_it (mkSort s) arsign + it_mkProd_or_LetIn (mkSort s) arsign (* [p] is the predicate and [cs] a constructor summary *) let build_branch_type env dep p cs = diff --git a/kernel/inductive.mli b/kernel/inductive.mli index 727ccf4095..4f27c30b88 100644 --- a/kernel/inductive.mli +++ b/kernel/inductive.mli @@ -174,7 +174,7 @@ val get_constructor : inductive_family -> int -> constructor_summary of the products of the constructors types are not renamed when [Anonymous] *) -val get_arity : inductive_family -> flat_arity +val get_arity : inductive_family -> arity (* Examples: assume diff --git a/kernel/typeops.ml b/kernel/typeops.ml index 8421a05434..5aaa47847d 100644 --- a/kernel/typeops.ml +++ b/kernel/typeops.ml @@ -166,7 +166,7 @@ in let find_case_dep_nparams env sigma (c,p) (IndFamily (mis,_) as indf) typP = let kelim = mis_kelim mis in let arsign,s = get_arity indf in - let glob_t = prod_it (mkSort s) arsign in + let glob_t = it_mkProd_or_LetIn (mkSort s) arsign in let (dep,_) = is_correct_arity env sigma kelim (c,p) indf (typP,glob_t) in dep diff --git a/library/indrec.ml b/library/indrec.ml index f968711430..6f1a4cd122 100644 --- a/library/indrec.ml +++ b/library/indrec.ml @@ -53,7 +53,7 @@ let mis_make_case_com depopt env sigma mispec kind = let ind = make_ind_family (mispec,rel_list nbprod nparams) in let lnamesar,_ = get_arity ind in let ci = make_default_case_info mispec in - it_lambda_name env' + it_mkLambda_or_LetIn_name env' (lambda_create env' (build_dependent_inductive ind, mkMutCase (ci, @@ -242,16 +242,16 @@ let mis_make_indrec env sigma listdepkind mispec = let indf = make_ind_family (mispeci,rel_list (nrec+nbconstruct) nparams) in let deftyi = - it_lambda_name env + it_mkLambda_or_LetIn_name env (lambda_create env (build_dependent_inductive (lift_inductive_family nrec indf), mkMutCase (make_default_case_info mispeci, mkRel (dect+j+1), mkRel 1, branches))) - (lift_context nrec lnames) + (Sign.lift_rel_context nrec lnames) in let typtyi = - it_prod_name env + it_mkProd_or_LetIn_name env (prod_create env (build_dependent_inductive indf, (if dep then diff --git a/pretyping/cases.ml b/pretyping/cases.ml index 7ab208f596..655a4903e8 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -81,7 +81,7 @@ let count_rec_arg j = let build_notdep_pred env sigma indf pred = let arsign,_ = get_arity indf in let nar = List.length arsign in - it_lambda_name env (lift nar pred) arsign + it_mkLambda_or_LetIn_name env (lift nar pred) arsign let pred_case_ml_fail env sigma isrec (IndType (indf,realargs)) (i,ft) = let pred = @@ -598,15 +598,15 @@ let infer_predicate env isevars typs cstrs (IndFamily (mis,_) as indf) = let (sign,_) = get_arity indf in if array_for_all (fun (_,_,typ) -> the_conv_x env isevars typn typ) eqns then - let pred = lam_it (lift (List.length sign) typn) sign in + let pred = it_mkLambda_or_LetIn (lift (List.length sign) typn) sign in (false,pred) (* true = dependent -- par défaut *) else let s = get_sort_of env !isevars typs.(0) in - let predpred = lam_it (mkSort s) sign in + let predpred = it_mkLambda_or_LetIn (mkSort s) sign in let caseinfo = make_default_case_info mis in let brs = array_map2 abstract_conclusion typs cstrs in let predbody = mkMutCase (caseinfo, predpred, mkRel 1, brs) in - let pred = lam_it (lift (List.length sign) typn) sign in + let pred = it_mkLambda_or_LetIn (lift (List.length sign) typn) sign in (* "TODO4-2" *) error "General inference of annotation not yet implemented;\ you need to give the predicate"; @@ -667,17 +667,14 @@ let rec extract_predicate = function let abstract_predicate env sigma indf = function | PrProd _ | PrCcl _ -> anomaly "abstract_predicate: must be some LetIn" | PrLetIn ((_,copt),pred) -> - let asign,_ = get_arity indf in - let sign = - List.map (fun (na,t) -> (named_hd (Global.env()) t na,t)) asign in - let dep = copt<> None in + let sign,_ = get_arity indf in + let dep = copt <> None in let sign' = if dep then - let ind = build_dependent_inductive indf in - let na = named_hd (Global.env()) ind Anonymous in - (na,ind)::sign + let ind=get_assumption_of env sigma (build_dependent_inductive indf) + in (Anonymous,None,ind)::sign else sign in - (dep, lam_it (extract_predicate pred) sign') + (dep, it_mkLambda_or_LetIn_name env (extract_predicate pred) sign') let specialize_predicate_match tomatchs cs = function | PrProd _ | PrCcl _ -> @@ -979,8 +976,8 @@ let build_expected_arity env isevars isdep tomatchl = | tm::ltm -> let (ty1,aritysign) = cook n tm in let rec follow n = function - | (na,ty2)::sign -> mkProd (na, ty2, follow (n+1) sign) - | _ -> + | d::sign -> mkProd_or_LetIn d (follow (n+1) sign) + | [] -> if isdep then mkProd (Anonymous, ty1, buildrec (n+1) ltm) else buildrec n ltm in follow n (List.rev aritysign) diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 6b698e28f5..93a03dcfa1 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -60,18 +60,18 @@ let transform_rec loc env sigma (p,c,lf) (indt,pt) = (Array.map (lift (nar+2)) lf) constrs recargs in let deffix = - it_lambda_name env + it_mkLambda_or_LetIn_name env (lambda_create env (applist (mI,List.append (List.map (lift (nar+1)) params) (rel_list 0 nar)), mkMutCase (ci, lift (nar+2) p, mkRel 1, branches))) - (lift_context 1 lnames) + (lift_rel_context 1 lnames) in if noccurn 1 deffix then whd_beta (applist (pop deffix,realargs@[c])) else let typPfix = - it_prod_name env + it_mkProd_or_LetIn_name env (prod_create env (applist (mI,(List.append (List.map (lift nar) params) diff --git a/tactics/equality.ml b/tactics/equality.ml index c27aeb195e..b1d0348d3c 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -461,8 +461,8 @@ let descend_then sigma env head dirn = (dirn_nlams, dirn_env, (fun dirnval (dfltval,resty) -> - let aritysign,_ = get_arity indf in - let p = lam_it (lift (mis_nrealargs mispec) resty) aritysign in + let arign,_ = get_arity indf in + let p = it_mkLambda_or_LetIn (lift (mis_nrealargs mispec) resty) arign in let build_branch i = let result = if i = dirn then dirnval else dfltval in it_mkLambda_or_LetIn_name env result cstr.(i-1).cs_args @@ -505,7 +505,7 @@ let construct_discriminator sigma env dirn c sort = | Type_Type -> build_UnitT (), build_EmptyT (), (Type dummy_univ) | _ -> build_True (), build_False (), (Prop Null) in - let p = lam_it (mkSort sort_0) arsign in + let p = it_mkLambda_or_LetIn (mkSort sort_0) arsign in let cstrs = get_constructors indf in let build_branch i = let endpt = if i = dirn then true_0 else false_0 in |