diff options
author | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-09-14 10:27:38 +0200 |
---|---|---|
committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-09-14 11:10:25 +0200 |
commit | 3e794be5f02ed438cdc5a351d09bdfb54c0be01a (patch) | |
tree | 3bbed56609e021f5c560a10037bafdae62e0db14 | |
parent | 0e94cb62410354e5df4e65b34e7cbf8451b31d6e (diff) | |
parent | 2aaa58c22e37b05e3637ac7161bb464da7db054a (diff) |
Merge branch 'v8.5' into v8.6
-rw-r--r-- | interp/notation_ops.ml | 3 | ||||
-rw-r--r-- | pretyping/pretyping.ml | 17 | ||||
-rw-r--r-- | pretyping/typing.ml | 12 | ||||
-rw-r--r-- | pretyping/typing.mli | 5 | ||||
-rw-r--r-- | test-suite/bugs/closed/5077.v | 8 | ||||
-rw-r--r-- | test-suite/output/Notations2.out | 2 | ||||
-rw-r--r-- | test-suite/output/Notations2.v | 5 | ||||
-rw-r--r-- | test-suite/success/TestRefine.v | 2 |
8 files changed, 35 insertions, 19 deletions
diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml index fcb4a345e..1262864c7 100644 --- a/interp/notation_ops.ml +++ b/interp/notation_ops.ml @@ -615,7 +615,8 @@ let add_env (alp,alpmetas) (terms,onlybinders,termlists,binderlists) var v = notation, as in "Notation "'twice_upto' y" := (fun x => x + x + y)". Then we keep (z,x) in alp, and we have to check that what the [v] which is bound to [var] does not contain z *) - if List.exists (fun (id,_) ->occur_glob_constr id v) alp then raise No_match; + if not (Id.equal ldots_var var) && + List.exists (fun (id,_) -> occur_glob_constr id v) alp then raise No_match; (* [alpmetas] is used when matching a pattern "fun x => ... x ... ?var ... x ..." with an actual term "fun z => ... z ..." when "x" is bound in the notation and the name "x" cannot be changed to "z", e.g. because diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index f46674003..46f0219f9 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -348,21 +348,6 @@ let process_inference_flags flags env initial_sigma (sigma,c) = (* Allow references to syntactically nonexistent variables (i.e., if applied on an inductive) *) let allow_anonymous_refs = ref false -(* Utilisé pour inférer le prédicat des Cases *) -(* Semble exagérement fort *) -(* Faudra préférer une unification entre les types de toutes les clauses *) -(* et autoriser des ? à rester dans le résultat de l'unification *) - -let evar_type_fixpoint loc env evdref lna lar vdefj = - let lt = Array.length vdefj in - if Int.equal (Array.length lar) lt then - for i = 0 to lt-1 do - if not (e_cumul env.ExtraEnv.env evdref (vdefj.(i)).uj_type - (lift lt lar.(i))) then - error_ill_typed_rec_body_loc loc env.ExtraEnv.env !evdref - i lna vdefj lar - done - (* coerce to tycon if any *) let inh_conv_coerce_to_tycon resolve_tc loc env evdref j = function | None -> j @@ -652,7 +637,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre { uj_val = it_mkLambda_or_LetIn j.uj_val ctxt; uj_type = it_mkProd_or_LetIn j.uj_type ctxt }) ctxtv vdef in - evar_type_fixpoint loc env evdref names ftys vdefj; + Typing.check_type_fixpoint loc env.ExtraEnv.env evdref names ftys vdefj; let ftys = Array.map (nf_evar !evdref) ftys in let fdefs = Array.map (fun x -> nf_evar !evdref (j_val x)) vdefj in let fixj = match fixkind with diff --git a/pretyping/typing.ml b/pretyping/typing.ml index 696d419af..9e9997f73 100644 --- a/pretyping/typing.ml +++ b/pretyping/typing.ml @@ -126,6 +126,16 @@ let e_judge_of_case env evdref ci pj cj lfj = { uj_val = mkCase (ci, pj.uj_val, cj.uj_val, Array.map j_val lfj); uj_type = rslty } +let check_type_fixpoint loc env evdref lna lar vdefj = + let lt = Array.length vdefj in + if Int.equal (Array.length lar) lt then + for i = 0 to lt-1 do + if not (Evarconv.e_cumul env evdref (vdefj.(i)).uj_type + (lift lt lar.(i))) then + Pretype_errors.error_ill_typed_rec_body_loc loc env !evdref + i lna vdefj lar + done + (* FIXME: might depend on the level of actual parameters!*) let check_allowed_sort env sigma ind c p = let pj = Retyping.get_judgment_of env sigma p in @@ -263,7 +273,7 @@ and execute_recdef env evdref (names,lar,vdef) = let env1 = push_rec_types (names,lara,vdef) env in let vdefj = execute_array env1 evdref vdef in let vdefv = Array.map j_val vdefj in - let _ = type_fixpoint env1 names lara vdefj in + let _ = check_type_fixpoint Loc.ghost env1 evdref names lara vdefj in (names,lara,vdefv) and execute_array env evdref = Array.map (execute env evdref) diff --git a/pretyping/typing.mli b/pretyping/typing.mli index e524edcca..04e5e40bc 100644 --- a/pretyping/typing.mli +++ b/pretyping/typing.mli @@ -39,3 +39,8 @@ val e_solve_evars : env -> evar_map ref -> constr -> constr (** (first constr is term to match, second is return predicate) *) val check_allowed_sort : env -> evar_map -> pinductive -> constr -> constr -> unit + +(** Raise an error message if bodies have types not unifiable with the + expected ones *) +val check_type_fixpoint : Loc.t -> env -> evar_map ref -> + Names.Name.t array -> types array -> unsafe_judgment array -> unit diff --git a/test-suite/bugs/closed/5077.v b/test-suite/bugs/closed/5077.v new file mode 100644 index 000000000..7e7f2c373 --- /dev/null +++ b/test-suite/bugs/closed/5077.v @@ -0,0 +1,8 @@ +(* Testing robustness of typing for a fixpoint with evars in its type *) + +Inductive foo (n : nat) : Type := . +Definition foo_denote {n} (x : foo n) : Type := match x with end. + +Definition baz : forall n (x : foo n), foo_denote x. +refine (fix go n (x : foo n) : foo_denote x := _). +Abort. diff --git a/test-suite/output/Notations2.out b/test-suite/output/Notations2.out index 20101f48e..5541ccf57 100644 --- a/test-suite/output/Notations2.out +++ b/test-suite/output/Notations2.out @@ -58,3 +58,5 @@ exist (Q x) y conj : nat -> nat % j : nat -> nat +{1, 2} + : nat -> Prop diff --git a/test-suite/output/Notations2.v b/test-suite/output/Notations2.v index 3cf89818d..1d8278c08 100644 --- a/test-suite/output/Notations2.v +++ b/test-suite/output/Notations2.v @@ -111,3 +111,8 @@ Check (exist (Q x) y conj). Notation "% i" := (fun i : nat => i) (at level 0, i ident). Check %i. Check %j. + +(* Check bug raised on coq-club on Sep 12, 2016 *) + +Notation "{ x , y , .. , v }" := (fun a => (or .. (or (a = x) (a = y)) .. (a = v))). +Check ({1, 2}). diff --git a/test-suite/success/TestRefine.v b/test-suite/success/TestRefine.v index c8a8b862f..023cb5f59 100644 --- a/test-suite/success/TestRefine.v +++ b/test-suite/success/TestRefine.v @@ -53,7 +53,7 @@ Abort. Lemma essai2 : forall x : nat, x = x. -Fail refine (fix f (x : nat) : x = x := _). +refine (fix f (x : nat) : x = x := _). Restart. |