From 7b724139a09c5d875131c5861a32d225d5b4b07b Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Mon, 4 Feb 2019 15:52:30 +0100 Subject: Constructor type information uses the expanded form. It used to simply remember the normal form of the type of the constructor. This is somewhat problematic as this is ambiguous in presence of let-bindings. Rather, we store this data in a fully expanded way, relying on rel_contexts. Probably fixes a crapload of bugs with inductive types containing let-bindings, but it seems that not many were reported in the bugtracker. --- tactics/eqschemes.ml | 6 +++--- tactics/hipattern.ml | 58 +++++++++++++++++++++++++++++----------------------- tactics/tacticals.ml | 14 ++++++------- 3 files changed, 42 insertions(+), 36 deletions(-) (limited to 'tactics') diff --git a/tactics/eqschemes.ml b/tactics/eqschemes.ml index b12018cd66..3c1115d056 100644 --- a/tactics/eqschemes.ml +++ b/tactics/eqschemes.ml @@ -138,7 +138,7 @@ let get_sym_eq_data env (ind,u) = let realsign,_ = List.chop mip.mind_nrealdecls arityctxt in if List.exists is_local_def realsign then error "Inductive equalities with local definitions in arity not supported."; - let constrsign,ccl = decompose_prod_assum mip.mind_nf_lc.(0) in + let constrsign,ccl = mip.mind_nf_lc.(0) in let _,constrargs = decompose_app ccl in if not (Int.equal (Context.Rel.length constrsign) (Context.Rel.length mib.mind_params_ctxt)) then error "Constructor must have no arguments"; (* This can be relaxed... *) @@ -173,7 +173,7 @@ let get_non_sym_eq_data env (ind,u) = let realsign,_ = List.chop mip.mind_nrealdecls arityctxt in if List.exists is_local_def realsign then error "Inductive equalities with local definitions in arity not supported"; - let constrsign,ccl = decompose_prod_assum mip.mind_nf_lc.(0) in + let constrsign,ccl = mip.mind_nf_lc.(0) in let _,constrargs = decompose_app ccl in if not (Int.equal (Context.Rel.length constrsign) (Context.Rel.length mib.mind_params_ctxt)) then error "Constructor must have no arguments"; @@ -776,7 +776,7 @@ let build_congr env (eq,refl,ctx) ind = error "Inductive equalities with local definitions in arity not supported."; let env_with_arity = push_rel_context arityctxt env in let ty = RelDecl.get_type (lookup_rel (mip.mind_nrealargs - i + 1) env_with_arity) in - let constrsign,ccl = decompose_prod_assum mip.mind_nf_lc.(0) in + let constrsign,ccl = mip.mind_nf_lc.(0) in let _,constrargs = decompose_app ccl in if not (Int.equal (Context.Rel.length constrsign) (Context.Rel.length mib.mind_params_ctxt)) then error "Constructor must have no arguments"; diff --git a/tactics/hipattern.ml b/tactics/hipattern.ml index 708412720a..395b4928ce 100644 --- a/tactics/hipattern.ml +++ b/tactics/hipattern.ml @@ -106,22 +106,24 @@ let match_with_one_constructor sigma style onlybinary allow_rec t = && (Int.equal mip.mind_nrealargs 0) then if is_strict_conjunction style (* strict conjunction *) then - let ctx = - (prod_assum sigma (snd - (decompose_prod_n_assum sigma mib.mind_nparams (EConstr.of_constr mip.mind_nf_lc.(0))))) in + let (ctx, _) = mip.mind_nf_lc.(0) in + let ctx = List.skipn (Context.Rel.length mib.mind_params_ctxt) (List.rev ctx) in if + (* Constructor has a type of the form + c : forall (a_0 ... a_n : Type) (x_0 : A_0) ... (x_n : A_n). T **) List.for_all (fun decl -> let c = RelDecl.get_type decl in is_local_assum decl && - isRel sigma c && - Int.equal (destRel sigma c) mib.mind_nparams) ctx + Constr.isRel c && + Int.equal (Constr.destRel c) mib.mind_nparams) ctx then Some (hdapp,args) else None else + let ctx, cty = mip.mind_nf_lc.(0) in + let cty = EConstr.of_constr (Term.it_mkProd_or_LetIn cty ctx) in let ctyp = whd_beta_prod sigma - (Termops.prod_applist_assum sigma (Context.Rel.length mib.mind_params_ctxt) - (EConstr.of_constr mip.mind_nf_lc.(0)) args) in + (Termops.prod_applist_assum sigma (Context.Rel.length mib.mind_params_ctxt) cty args) in let cargs = List.map RelDecl.get_type (prod_assum sigma ctyp) in if not (is_lax_conjunction style) || has_nodep_prod sigma ctyp then (* Record or non strict conjunction *) @@ -165,12 +167,13 @@ let is_tuple sigma t = it is strict if it has the form "Inductive I A1 ... An := C1 (_:A1) | ... | Cn : (_:An)" *) -let test_strict_disjunction n lc = - let open Term in - Array.for_all_i (fun i c -> - match (prod_assum (snd (decompose_prod_n_assum n c))) with - | [LocalAssum (_,c)] -> Constr.isRel c && Int.equal (Constr.destRel c) (n - i) - | _ -> false) 0 lc +let test_strict_disjunction (mib, mip) = + let n = List.length mib.mind_params_ctxt in + let check i (ctx, _) = match List.skipn n (List.rev ctx) with + | [LocalAssum (_, c)] -> Constr.isRel c && Int.equal (Constr.destRel c) (n - i) + | _ -> false + in + Array.for_all_i check 0 mip.mind_nf_lc let match_with_disjunction ?(strict=false) ?(onlybinary=false) sigma t = let (hdapp,args) = decompose_app sigma t in @@ -183,14 +186,16 @@ let match_with_disjunction ?(strict=false) ?(onlybinary=false) sigma t = && (Int.equal mip.mind_nrealargs 0) then if strict then - if test_strict_disjunction mib.mind_nparams mip.mind_nf_lc then + if test_strict_disjunction (mib, mip) then Some (hdapp,args) else None else - let cargs = - Array.map (fun ar -> pi2 (destProd sigma (prod_applist sigma (EConstr.of_constr ar) args))) - mip.mind_nf_lc in + let map (ctx, cty) = + let ar = EConstr.of_constr (Term.it_mkProd_or_LetIn cty ctx) in + pi2 (destProd sigma (prod_applist sigma ar args)) + in + let cargs = Array.map map mip.mind_nf_lc in Some (hdapp,Array.to_list cargs) else None @@ -225,10 +230,8 @@ let match_with_unit_or_eq_type sigma t = match EConstr.kind sigma hdapp with | Ind (ind , _) -> let (mib,mip) = Global.lookup_inductive ind in - let constr_types = mip.mind_nf_lc in let nconstr = Array.length mip.mind_consnames in - let zero_args c = Int.equal (nb_prod sigma (EConstr.of_constr c)) mib.mind_nparams in - if Int.equal nconstr 1 && zero_args constr_types.(0) then + if Int.equal nconstr 1 && Int.equal mip.mind_consnrealargs.(0) 0 then Some hdapp else None @@ -308,11 +311,13 @@ let match_with_equation env sigma t = let constr_types = mip.mind_nf_lc in let nconstr = Array.length mip.mind_consnames in if Int.equal nconstr 1 then - if is_matching env sigma coq_refl_leibniz1_pattern (EConstr.of_constr constr_types.(0)) then + let (ctx, cty) = constr_types.(0) in + let cty = EConstr.of_constr (Term.it_mkProd_or_LetIn cty ctx) in + if is_matching env sigma coq_refl_leibniz1_pattern cty then None, hdapp, MonomorphicLeibnizEq(args.(0),args.(1)) - else if is_matching env sigma coq_refl_leibniz2_pattern (EConstr.of_constr constr_types.(0)) then + else if is_matching env sigma coq_refl_leibniz2_pattern cty then None, hdapp, PolymorphicLeibnizEq(args.(0),args.(1),args.(2)) - else if is_matching env sigma coq_refl_jm_pattern (EConstr.of_constr constr_types.(0)) then + else if is_matching env sigma coq_refl_jm_pattern cty then None, hdapp, HeterogenousEq(args.(0),args.(1),args.(2),args.(3)) else raise NoEquationFound else raise NoEquationFound @@ -378,8 +383,9 @@ let match_with_nodep_ind sigma t = | Ind (ind, _) -> let (mib,mip) = Global.lookup_inductive ind in if Array.length (mib.mind_packets)>1 then None else - let nodep_constr c = - has_nodep_prod_after (Context.Rel.length mib.mind_params_ctxt) sigma (EConstr.of_constr c) in + let nodep_constr (ctx, cty) = + let c = EConstr.of_constr (Term.it_mkProd_or_LetIn cty ctx) in + has_nodep_prod_after (Context.Rel.length mib.mind_params_ctxt) sigma c in if Array.for_all nodep_constr mip.mind_nf_lc then let params= if Int.equal mip.mind_nrealargs 0 then args else @@ -400,7 +406,7 @@ let match_with_sigma_type sigma t = && (Int.equal mip.mind_nrealargs 0) && (Int.equal (Array.length mip.mind_consnames)1) && has_nodep_prod_after (Context.Rel.length mib.mind_params_ctxt + 1) sigma - (EConstr.of_constr mip.mind_nf_lc.(0)) + (let (ctx, cty) = mip.mind_nf_lc.(0) in EConstr.of_constr (Term.it_mkProd_or_LetIn cty ctx)) then (*allowing only 1 existential*) Some (hdapp,args) diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml index bfbce8f6eb..ec8d4d0e14 100644 --- a/tactics/tacticals.ml +++ b/tactics/tacticals.ml @@ -20,6 +20,7 @@ open Tacmach open Clenv open Tactypes +module RelDecl = Context.Rel.Declaration module NamedDecl = Context.Named.Declaration (************************************************************************) @@ -223,8 +224,8 @@ let compute_induction_names = compute_induction_names_gen true (* Compute the let-in signature of case analysis or standard induction scheme *) let compute_constructor_signatures ~rec_flag ((_,k as ity),u) = let rec analrec c recargs = - match Constr.kind c, recargs with - | Prod (_,_,c), recarg::rest -> + match c, recargs with + | RelDecl.LocalAssum _ :: c, recarg::rest -> let rest = analrec c rest in begin match Declareops.dest_recarg recarg with | Norec | Imbr _ -> true :: rest @@ -232,14 +233,13 @@ let compute_constructor_signatures ~rec_flag ((_,k as ity),u) = if rec_flag && Int.equal j k then true :: true :: rest else true :: rest end - | LetIn (_,_,_,c), rest -> false :: analrec c rest - | _, [] -> [] + | RelDecl.LocalDef _ :: c, rest -> false :: analrec c rest + | [], [] -> [] | _ -> anomaly (Pp.str "compute_constructor_signatures.") in let (mib,mip) = Global.lookup_inductive ity in - let n = mib.mind_nparams in - let lc = - Array.map (fun c -> snd (Term.decompose_prod_n_assum n c)) mip.mind_nf_lc in + let map (ctx, _) = List.skipn (Context.Rel.length mib.mind_params_ctxt) (List.rev ctx) in + let lc = Array.map map mip.mind_nf_lc in let lrecargs = Declareops.dest_subterms mip.mind_recargs in Array.map2 analrec lc lrecargs -- cgit v1.2.3