diff options
| -rw-r--r-- | pretyping/evarconv.ml | 2 | ||||
| -rw-r--r-- | pretyping/evarsolve.ml | 8 | ||||
| -rw-r--r-- | pretyping/evarsolve.mli | 6 | ||||
| -rw-r--r-- | pretyping/patternops.ml | 3 | ||||
| -rw-r--r-- | pretyping/tacred.ml | 24 | ||||
| -rw-r--r-- | test-suite/bugs/closed/3648.v | 85 |
6 files changed, 109 insertions, 19 deletions
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index 15b16a36bc..3b3c9f9eed 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -850,7 +850,7 @@ let apply_on_subterm env evdref f c t = | _ -> map_constr_with_binders_left_to_right (fun d (env,(k,c)) -> (push_rel d env, (k+1,lift 1 c))) - applyrec acc !evdref t + applyrec acc t in applyrec (env,(0,c)) t diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml index e47fad81bb..ba877d35c8 100644 --- a/pretyping/evarsolve.ml +++ b/pretyping/evarsolve.ml @@ -101,14 +101,6 @@ let refresh_universes ?(inferred=false) ?(onlyalg=false) pbty env evd t = in if !modified then !evdref, t' else !evdref, t -let map_constr_with_binders_left_to_right g f (env, l as acc) sigma c = - match kind_of_term c with - | Proj (p, r) -> (* Treat specially for partial applications *) - let t = Retyping.expand_projection env sigma p r [] in - map_constr_with_binders_left_to_right g f acc t - | _ -> map_constr_with_binders_left_to_right g f acc c - - (************************) (* Unification results *) (************************) diff --git a/pretyping/evarsolve.mli b/pretyping/evarsolve.mli index 86c9908c84..0d0f3c0e51 100644 --- a/pretyping/evarsolve.mli +++ b/pretyping/evarsolve.mli @@ -69,9 +69,3 @@ val check_evar_instance : val remove_instance_local_defs : evar_map -> existential_key -> constr array -> constr list - -(* This is up to partial applications and primitive projection expansion *) -val map_constr_with_binders_left_to_right : - (Context.rel_declaration -> (env * 'a) -> (env * 'a)) -> - ((env * 'a) -> constr -> constr) -> - (env * 'a) -> evar_map -> constr -> constr diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml index 44ff2b5b8c..01317ba253 100644 --- a/pretyping/patternops.ml +++ b/pretyping/patternops.ml @@ -150,8 +150,7 @@ let pattern_of_constr sigma t = | 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 (constant_of_kn(canonical_con p), pattern_of_constr c) + | Proj (p, c) -> PProj (constant_of_kn(canonical_con p), pattern_of_constr c) | Evar (evk,ctxt as ev) -> (match snd (Evd.evar_source evk sigma) with | Evar_kinds.MatchingVar (b,id) -> diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml index f0d0d45267..6f6de95fcd 100644 --- a/pretyping/tacred.ml +++ b/pretyping/tacred.ml @@ -945,6 +945,26 @@ let matches_head env sigma c t = let is_pattern_meta = function Pattern.PMeta _ -> true | _ -> false +(** FIXME: Specific function to handle projections: it ignores what happens on the + parameters. This is a temporary fix while rewrite etc... are not up to equivalence + of the projection and it's eta expanded form. +*) +let change_map_constr_with_binders_left_to_right g f (env, l as acc) sigma c = + match kind_of_term c with + | Proj (p, r) -> (* Treat specially for partial applications *) + let t = Retyping.expand_projection env sigma p r [] in + let hdf, al = destApp t in + let a = al.(Array.length al - 1) in + let app = (mkApp (t, Array.sub al 0 (Array.length al - 1))) in + let app' = f acc app in + let a' = f acc a in + let hdf', al' = destApp app' in + if hdf' == hdf then + (* Still the same projection, we ignore the change in parameters *) + mkProj (p, a') + else mkApp (app', [| a' |]) + | _ -> map_constr_with_binders_left_to_right g f acc c + let e_contextually byhead (occs,c) f env sigma t = let (nowhere_except_in,locs) = Locusops.convert_occs occs in let maxocc = List.fold_right max locs 0 in @@ -977,9 +997,9 @@ let e_contextually byhead (occs,c) f env sigma t = else t with ConstrMatching.PatternMatchingFailure -> - map_constr_with_binders_left_to_right + change_map_constr_with_binders_left_to_right (fun d (env,c) -> (push_rel d env,lift_pattern 1 c)) - traverse envc t + traverse envc sigma t in let t' = traverse (env,c) t in if List.exists (fun o -> o >= !pos) locs then error_invalid_occurrence locs; diff --git a/test-suite/bugs/closed/3648.v b/test-suite/bugs/closed/3648.v new file mode 100644 index 0000000000..1256d125f5 --- /dev/null +++ b/test-suite/bugs/closed/3648.v @@ -0,0 +1,85 @@ +(* File reduced by coq-bug-finder from original input, then from 8808 lines to 424 lines, then from 432 lines to 196 lines, then from\ + 145 lines to 82 lines *) +(* coqc version trunk (September 2014) compiled on Sep 18 2014 21:0:5 with OCaml 4.01.0 + coqtop version cagnode16:/afs/csail.mit.edu/u/j/jgross/coq-trunk,trunk (07e4438bd758c2ced8caf09a6961ccd77d84e42b) *) + +Reserved Infix "o" (at level 40, left associativity). +Global Set Primitive Projections. + +Delimit Scope morphism_scope with morphism. +Delimit Scope category_scope with category. +Delimit Scope object_scope with object. + +Record PreCategory := + { object :> Type; + morphism : object -> object -> Type; + + identity : forall x, morphism x x; + compose : forall s d d', + morphism d d' + -> morphism s d + -> morphism s d' + where "f 'o' g" := (compose f g) + }. +Arguments identity {!C%category} / x%object : rename. + +Infix "o" := (@compose _ _ _ _) : morphism_scope. + +Local Open Scope morphism_scope. +Definition prodC (C D : PreCategory) : PreCategory. + refine (@Build_PreCategory + (C * D)%type + (fun s d => (morphism C (fst s) (fst d) + * morphism D (snd s) (snd d))%type) + (fun x => (identity (fst x), identity (snd x))) + (fun s d d' m2 m1 => (fst m2 o fst m1, snd m2 o snd m1))). +Defined. + +Local Infix "*" := prodC : category_scope. + +Delimit Scope functor_scope with functor. + +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); + identity_of : forall x, morphism_of _ _ (identity x) + = identity (object_of x) + }. +Arguments morphism_of [C%category] [D%category] F%functor [s%object d%object] m%morphism : rename, simpl nomatch. +Notation "F '_1' m" := (morphism_of F m) (at level 10, no associativity) : morphism_scope. + +Record NaturalTransformation C D (F G : Functor C D) := { components_of :> forall c, morphism D (F c) (G c) }. +Definition functor_category (C D : PreCategory) : PreCategory. + exact (@Build_PreCategory (Functor C D) + (@NaturalTransformation C D) + $(admit)$ + $(admit)$). +Defined. + +Local Notation "C -> D" := (functor_category C D) : category_scope. +Variable C1 : PreCategory. +Variable C2 : PreCategory. +Variable D : PreCategory. + +Definition functor_object_of +: (C1 -> (C2 -> D))%category -> (C1 * C2 -> D)%category. +Proof. + intro F; hnf in F |- *. + refine (Build_Functor + (prodC C1 C2) D + (fun c1c2 => F (fst c1c2) (snd c1c2)) + (fun s d m => F (fst d) _1 (snd m) o (@morphism_of _ _ F _ _ (fst m)) (snd s)) + _). + intros. + rewrite identity_of. + cbn. + rewrite (identity_of _ _ F (fst x)). + Undo. +(* Toplevel input, characters 20-55: +Error: +Found no subterm matching "F _1 (identity (fst x))" in the current goal. *) + rewrite identity_of. (* Toplevel input, characters 15-34: +Error: +Found no subterm matching "morphism_of ?202 (identity ?203)" in the current goal. *)
\ No newline at end of file |