diff options
| -rw-r--r-- | pretyping/patternops.ml | 30 | ||||
| -rw-r--r-- | pretyping/retyping.ml | 2 | ||||
| -rw-r--r-- | tactics/auto.ml | 4 | ||||
| -rw-r--r-- | test-suite/bugs/closed/3661.v | 88 |
4 files changed, 108 insertions, 16 deletions
diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml index 9b7726692..4a1dc1dd6 100644 --- a/pretyping/patternops.ml +++ b/pretyping/patternops.ml @@ -21,6 +21,7 @@ open Misctypes open Decl_kinds open Pattern open Evd +open Environ let case_info_pattern_eq i1 i2 = i1.cip_style == i2.cip_style && @@ -122,7 +123,7 @@ let head_of_constr_reference c = match kind_of_term c with let pattern_of_constr env sigma t = let ctx = ref [] in - let rec pattern_of_constr t = + let rec pattern_of_constr env t = match kind_of_term t with | Rel n -> PRel n | Meta n -> PMeta (Some (Id.of_string ("META" ^ string_of_int n))) @@ -130,10 +131,13 @@ let pattern_of_constr env sigma t = | Sort (Prop Null) -> PSort GProp | Sort (Prop Pos) -> PSort GSet | Sort (Type _) -> PSort (GType []) - | Cast (c,_,_) -> pattern_of_constr c - | LetIn (na,c,_,b) -> PLetIn (na,pattern_of_constr c,pattern_of_constr b) - | Prod (na,c,b) -> PProd (na,pattern_of_constr c,pattern_of_constr b) - | Lambda (na,c,b) -> PLambda (na,pattern_of_constr c,pattern_of_constr b) + | Cast (c,_,_) -> pattern_of_constr env c + | LetIn (na,c,t,b) -> PLetIn (na,pattern_of_constr env c, + pattern_of_constr (push_rel (na,Some c,t) env) b) + | Prod (na,c,b) -> PProd (na,pattern_of_constr env c, + pattern_of_constr (push_rel (na, None, c) env) b) + | Lambda (na,c,b) -> PLambda (na,pattern_of_constr env c, + pattern_of_constr (push_rel (na, None, c) env) b) | App (f,a) -> (match match kind_of_term f with @@ -145,19 +149,19 @@ let pattern_of_constr env sigma t = | _ -> None) | _ -> None with - | Some n -> PSoApp (n,Array.to_list (Array.map pattern_of_constr a)) - | None -> PApp (pattern_of_constr f,Array.map (pattern_of_constr) a)) + | Some n -> PSoApp (n,Array.to_list (Array.map (pattern_of_constr env) a)) + | None -> PApp (pattern_of_constr env f,Array.map (pattern_of_constr env) a)) | Const (sp,u) -> PRef (ConstRef (constant_of_kn(canonical_con sp))) | Ind (sp,u) -> PRef (canonical_gr (IndRef sp)) | Construct (sp,u) -> PRef (canonical_gr (ConstructRef sp)) - | Proj (p, c) -> PProj (Projection.map (fun kn -> constant_of_kn(canonical_con kn)) p, - pattern_of_constr c) + | Proj (p, c) -> + pattern_of_constr env (Retyping.expand_projection env sigma p c []) | Evar (evk,ctxt as ev) -> (match snd (Evd.evar_source evk sigma) with | Evar_kinds.MatchingVar (b,id) -> ctx := (id,None,existential_type sigma ev)::!ctx; assert (not b); PMeta (Some id) - | Evar_kinds.GoalEvar -> PEvar (evk,Array.map pattern_of_constr ctxt) + | Evar_kinds.GoalEvar -> PEvar (evk,Array.map (pattern_of_constr env) ctxt) | _ -> PMeta None) | Case (ci,p,a,br) -> let cip = @@ -167,13 +171,13 @@ let pattern_of_constr env sigma t = cip_extensible = false } in let branch_of_constr i c = - (i, ci.ci_cstr_ndecls.(i), pattern_of_constr c) + (i, ci.ci_cstr_ndecls.(i), pattern_of_constr env c) in - PCase (cip, pattern_of_constr p, pattern_of_constr a, + PCase (cip, pattern_of_constr env p, pattern_of_constr env a, Array.to_list (Array.mapi branch_of_constr br)) | Fix f -> PFix f | CoFix f -> PCoFix f in - let p = pattern_of_constr t in + let p = pattern_of_constr env t in (* side-effect *) (* Warning: the order of dependencies in ctx is not ensured *) (!ctx,p) diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml index b16cf75f5..89ad9ee68 100644 --- a/pretyping/retyping.ml +++ b/pretyping/retyping.ml @@ -244,6 +244,6 @@ let sorts_of_context env evc ctxt = let expand_projection env sigma pr c args = let ty = get_type_of env sigma c in - let (i,u), ind_args = Inductive.find_rectype env ty in + let (i,u), ind_args = Inductiveops.find_mrectype env sigma ty in mkApp (mkConstU (Projection.constant pr,u), Array.of_list (ind_args @ (c :: args))) diff --git a/tactics/auto.ml b/tactics/auto.ml index 564e111e0..356b208b8 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -604,7 +604,7 @@ let make_apply_entry env sigma (eapply,hnf,verbose) pri poly ?(name=PathAny) (c, let sigma' = Evd.merge_context_set univ_flexible dummy_goal.sigma ctx in let ce = mk_clenv_from { dummy_goal with sigma = sigma' } (c,cty) in let c' = clenv_type (* ~reduce:false *) ce in - let pat = snd (Patternops.pattern_of_constr env sigma c') in + let pat = snd (Patternops.pattern_of_constr env ce.evd c') in let hd = try head_pattern_bound pat with BoundPattern -> failwith "make_apply_entry" in @@ -701,7 +701,7 @@ let make_trivial env sigma poly ?(name=PathAny) r = let ce = mk_clenv_from dummy_goal (c,t) in (Some hd, { pri=1; poly = poly; - pat = Some (snd (Patternops.pattern_of_constr env sigma (clenv_type ce))); + pat = Some (snd (Patternops.pattern_of_constr env ce.evd (clenv_type ce))); name = name; code=Res_pf_THEN_trivial_fail(c,t,ctx) }) diff --git a/test-suite/bugs/closed/3661.v b/test-suite/bugs/closed/3661.v new file mode 100644 index 000000000..fdca49bc4 --- /dev/null +++ b/test-suite/bugs/closed/3661.v @@ -0,0 +1,88 @@ +(* File reduced by coq-bug-finder from original input, then from 11218 lines to 438 lines, then from 434 lines to 202 lines, then from 140 lines to 94 lines *) +(* coqc version trunk (September 2014) compiled on Sep 25 2014 2:53:46 with OCaml 4.01.0 + coqtop version cagnode16:/afs/csail.mit.edu/u/j/jgross/coq-trunk,trunk (bec7e0914f4a7144cd4efa8ffaccc9f72dbdb790) *) +Inductive paths {A : Type} (a : A) : A -> Type := idpath : paths a a. +Set Implicit Arguments. +Delimit Scope morphism_scope with morphism. +Record PreCategory := { object :> Type ; morphism : object -> object -> Type }. +Bind Scope category_scope with PreCategory. +Local Open Scope morphism_scope. +Record Functor (C D : PreCategory) := + { object_of :> C -> D; + morphism_of : forall s d, morphism C s d -> morphism D (object_of s) (object_of d) }. +Set Primitive Projections. +Class IsIsomorphism {C : PreCategory} {s d} (m : morphism C s d) := { morphism_inverse : morphism C d s }. +Record NaturalTransformation C D (F G : Functor C D) := { components_of :> forall c, morphism D (F c) (G c) }. +Unset Primitive Projections. +Class Isomorphic {C : PreCategory} s d := + { morphism_isomorphic :> morphism C s d; + isisomorphism_isomorphic :> IsIsomorphism morphism_isomorphic }. +Arguments morphism_inverse {C s d} m {_} / . +Local Notation "m ^-1" := (morphism_inverse m) (at level 3, format "m '^-1'") : morphism_scope. +Definition functor_category (C D : PreCategory) : PreCategory. + exact (@Build_PreCategory (Functor C D) + (@NaturalTransformation C D)). +Defined. +Local Notation "C -> D" := (functor_category C D) : category_scope. +Generalizable All Variables. +Definition isisomorphism_components_of `{@IsIsomorphism (C -> D) F G T} x : IsIsomorphism (T x). +Proof. + constructor. + exact (T^-1 x). +Defined. +Hint Immediate isisomorphism_components_of : typeclass_instances. +Goal forall (x3 x9 : PreCategory) (x12 f0 : Functor x9 x3) + (x35 : @Isomorphic (@functor_category x9 x3) f0 x12) + (x37 : object x9) + (H3 : morphism x3 (@object_of x9 x3 f0 x37) + (@object_of x9 x3 f0 x37)) + (x34 : @Isomorphic (@functor_category x9 x3) x12 f0) + (m : morphism x3 (x12 x37) (f0 x37) -> + morphism x3 (f0 x37) (x12 x37) -> + morphism x3 (f0 x37) (f0 x37)), + @paths + (morphism x3 (@object_of x9 x3 f0 x37) (@object_of x9 x3 f0 x37)) + H3 + (m + (@components_of x9 x3 x12 f0 + (@morphism_inverse (@functor_category x9 x3) f0 x12 + (@morphism_isomorphic (@functor_category x9 x3) f0 x12 x35) + (@isisomorphism_isomorphic (@functor_category x9 x3) f0 x12 + x35)) x37) + (@components_of x9 x3 f0 x12 + (@morphism_inverse (@functor_category x9 x3) x12 f0 + (@morphism_isomorphic (@functor_category x9 x3) x12 f0 x34) + (@isisomorphism_isomorphic (@functor_category x9 x3) x12 f0 + x34)) x37)). + Unset Printing All. + intros. + match goal with + | [ |- context[components_of ?T^-1 ?x] ] + => progress let T1 := constr:(T^-1 x) in + let T2 := constr:((T x)^-1) in + change T1 with T2 || fail 1 "too early" + end. + + Undo. + + match goal with + | [ |- context[components_of ?T^-1 ?x] ] + => progress let T1 := constr:(T^-1 x) in + change T1 with ((T x)^-1) || fail 1 "too early 2" + end. + + Undo. + + match goal with + | [ |- context[components_of ?T^-1 ?x] ] + => progress let T2 := constr:((T x)^-1) in + change (T^-1 x) with T2 + end. (* not convertible *) + +(* + + (@components_of x9 x3 x12 f0 + (@morphism_inverse _ _ _ + (@morphism_isomorphic (functor_category x9 x3) f0 x12 x35) _) x37) + +*)
\ No newline at end of file |