From 1388171a48d8e068d5d0ed93b74faa4ac7da5f7f Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Fri, 27 Feb 2015 14:23:02 +0100 Subject: Fixing typo resulting in wrong printing of return clauses for inductive types with let-in in arity. --- pretyping/inductiveops.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'pretyping') diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml index adf714db35..356a699c66 100644 --- a/pretyping/inductiveops.ml +++ b/pretyping/inductiveops.ml @@ -273,7 +273,7 @@ let projection_nparams p = projection_nparams_env (Global.env ()) p let make_case_info env ind style = let (mib,mip) = Inductive.lookup_mind_specif env ind in let ind_tags = - rel_context_tags (List.firstn mip.mind_nrealargs mip.mind_arity_ctxt) in + rel_context_tags (List.firstn mip.mind_nrealdecls mip.mind_arity_ctxt) in let cstr_tags = Array.map2 (fun c n -> let d,_ = decompose_prod_assum c in -- cgit v1.2.3 From 172388eab4f34da71d82c4fab269bd6426c73853 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Fri, 27 Feb 2015 14:24:19 +0100 Subject: Fixing first part of bug #3210 (inference of pattern-matching return clause in the presence of let-ins in the arity of inductive type). --- pretyping/cases.ml | 27 ++++++++++++++++++++------- 1 file changed, 20 insertions(+), 7 deletions(-) (limited to 'pretyping') diff --git a/pretyping/cases.ml b/pretyping/cases.ml index 7c3165fa8e..fcbe90b6a7 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -285,11 +285,13 @@ let inductive_template evdref env tmloc ind = applist (mkIndU indu,List.rev evarl) let try_find_ind env sigma typ realnames = - let (IndType(_,realargs) as ind) = find_rectype env sigma typ in + let (IndType(indf,realargs) as ind) = find_rectype env sigma typ in let names = match realnames with | Some names -> names - | None -> List.make (List.length realargs) Anonymous in + | None -> + let ind = fst (fst (dest_ind_family indf)) in + List.make (inductive_nrealdecls ind) Anonymous in IsInd (typ,ind,names) let inh_coerce_to_ind evdref env loc ty tyi = @@ -730,7 +732,17 @@ let set_declaration_name x (_,c,t) = (x,c,t) let recover_initial_subpattern_names = List.map2 set_declaration_name -let recover_alias_names get_name = List.map2 (fun x (_,c,t) ->(get_name x,c,t)) +let recover_and_adjust_alias_names names sign = + let rec aux = function + | [],[] -> + [] + | x::names, (_,None,t)::sign -> + (x,(alias_of_pat x,None,t)) :: aux (names,sign) + | names, (na,(Some _ as c),t)::sign -> + (PatVar (Loc.ghost,na),(na,c,t)) :: aux (names,sign) + | _ -> assert false + in + List.split (aux (names,sign)) let push_rels_eqn sign eqn = {eqn with @@ -1695,11 +1707,12 @@ let build_inversion_problem loc env sigma tms t = let pat,acc = make_patvar t acc in let indf' = lift_inductive_family n indf in let sign = make_arity_signature env true indf' in - let sign = recover_alias_names alias_of_pat (pat :: List.rev patl) sign in - let p = List.length realargs in + let patl = pat :: List.rev patl in + let patl,sign = recover_and_adjust_alias_names patl sign in + let p = List.length patl in let env' = push_rel_context sign env in - let patl',acc_sign,acc = aux (n+p+1) env' (sign@acc_sign) tms acc in - patl@pat::patl',acc_sign,acc + let patl',acc_sign,acc = aux (n+p) env' (sign@acc_sign) tms acc in + List.rev_append patl patl',acc_sign,acc | (t, NotInd (bo,typ)) :: tms -> let pat,acc = make_patvar t acc in let d = (alias_of_pat pat,None,typ) in -- cgit v1.2.3 From b286c9f4f42febfd37f9715d81eaf118ab24aa94 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Fri, 27 Feb 2015 16:29:28 +0100 Subject: Add support so that the type of a match in an inductive type with let-in is reduced as if without let-in, when applied to arguments. This allows e.g. to have a head-betazeta-reduced goal in the following example. Inductive Foo : let X := Set in X := I : Foo. Definition foo (x : Foo) : x = x. destruct x. (* or case x, etc. *) --- pretyping/inductiveops.ml | 2 +- pretyping/reductionops.ml | 13 +++++++++++++ pretyping/reductionops.mli | 1 + pretyping/retyping.ml | 5 +++-- 4 files changed, 18 insertions(+), 3 deletions(-) (limited to 'pretyping') diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml index 356a699c66..7f6a4a6442 100644 --- a/pretyping/inductiveops.ml +++ b/pretyping/inductiveops.ml @@ -526,7 +526,7 @@ let type_case_branches_with_names env indspec p c = let (params,realargs) = List.chop nparams args in let lbrty = Inductive.build_branches_type ind specif params p in (* Build case type *) - let conclty = Reduction.beta_appvect p (Array.of_list (realargs@[c])) in + let conclty = Reduction.betazeta_appvect (mip.mind_nrealdecls+1) p (Array.of_list (realargs@[c])) in (* Adjust names *) if is_elim_predicate_explicitly_dependent env p (ind,params) then (set_pattern_names env (fst ind) lbrty, conclty) diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index ec34383820..2c70a6c9a0 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -1628,3 +1628,16 @@ let head_unfold_under_prod ts env _ c = | Const cst -> beta_applist (unfold cst,l) | _ -> c in aux c + +let betazetaevar_applist sigma n c l = + let rec stacklam n env t stack = + if Int.equal n 0 then applist (substl env t, stack) else + match kind_of_term t, stack with + | Lambda(_,_,c), arg::stacktl -> stacklam (n-1) (arg::env) c stacktl + | LetIn(_,b,_,c), _ -> stacklam (n-1) (b::env) c stack + | Evar ev, _ -> + (match safe_evar_value sigma ev with + | Some body -> stacklam n env body stack + | None -> applist (substl env t, stack)) + | _ -> anomaly (Pp.str "Not enough lambda/let's") in + stacklam n [] c l diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli index 7c61d4e143..d4f061c5be 100644 --- a/pretyping/reductionops.mli +++ b/pretyping/reductionops.mli @@ -278,6 +278,7 @@ val whd_meta : evar_map -> constr -> constr val plain_instance : constr Metamap.t -> constr -> constr val instance : evar_map -> constr Metamap.t -> constr -> constr val head_unfold_under_prod : transparent_state -> reduction_function +val betazetaevar_applist : evar_map -> int -> constr -> constr list -> constr (** {6 Heuristic for Conversion with Evar } *) diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml index cd52ba44da..213d7ddda4 100644 --- a/pretyping/retyping.ml +++ b/pretyping/retyping.ml @@ -100,7 +100,7 @@ let retype ?(polyprop=true) sigma = | Ind ind -> rename_type_of_inductive env ind | Construct cstr -> rename_type_of_constructor env cstr | Case (_,p,c,lf) -> - let Inductiveops.IndType(_,realargs) = + let Inductiveops.IndType(indf,realargs) = let t = type_of env c in try Inductiveops.find_rectype env sigma t with Not_found -> @@ -109,7 +109,8 @@ let retype ?(polyprop=true) sigma = Inductiveops.find_rectype env sigma t with Not_found -> retype_error BadRecursiveType in - let t = whd_beta sigma (applist (p, realargs)) in + let n = inductive_nrealdecls (fst (fst (dest_ind_family indf))) in + let t = betazetaevar_applist sigma n p realargs in (match kind_of_term (whd_betadeltaiota env sigma (type_of env t)) with | Prod _ -> whd_beta sigma (applist (t, [c])) | _ -> t) -- cgit v1.2.3 From e43abf43a78a5bbeed720d50cd1ea68fdfc672f2 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 27 Feb 2015 17:27:12 +0100 Subject: simpl: honor Global for "simpl: never" (Close: 3206) It was an integer overflow! All sorts of memories. --- pretyping/reductionops.ml | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) (limited to 'pretyping') diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index 2c70a6c9a0..09eb38bd12 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -64,7 +64,10 @@ module ReductionBehaviour = struct if Lib.is_in_section (ConstRef c) then let vars, _, _ = Lib.section_segment_of_constant c in let extra = List.length vars in - let nargs' = if b.b_nargs < 0 then b.b_nargs else b.b_nargs + extra in + let nargs' = + if b.b_nargs = max_int then max_int + else if b.b_nargs < 0 then b.b_nargs + else b.b_nargs + extra in let recargs' = List.map ((+) extra) b.b_recargs in { b with b_nargs = nargs'; b_recargs = recargs' } else b -- cgit v1.2.3 From 9f09cbfe36c38a97644ea98c5497636fe74d98d6 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Fri, 27 Feb 2015 18:59:59 +0100 Subject: Taking current env and not global env in b286c9f4f42f (4 commits ago, as revealed by #2141). --- pretyping/retyping.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'pretyping') diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml index 213d7ddda4..a56861c683 100644 --- a/pretyping/retyping.ml +++ b/pretyping/retyping.ml @@ -109,7 +109,7 @@ let retype ?(polyprop=true) sigma = Inductiveops.find_rectype env sigma t with Not_found -> retype_error BadRecursiveType in - let n = inductive_nrealdecls (fst (fst (dest_ind_family indf))) in + let n = inductive_nrealdecls_env env (fst (fst (dest_ind_family indf))) in let t = betazetaevar_applist sigma n p realargs in (match kind_of_term (whd_betadeltaiota env sigma (type_of env t)) with | Prod _ -> whd_beta sigma (applist (t, [c])) -- cgit v1.2.3