diff options
| -rw-r--r-- | .gitlab-ci.yml | 7 | ||||
| -rw-r--r-- | Makefile.ci | 2 | ||||
| -rwxr-xr-x | dev/ci/ci-basic-overlay.sh | 5 | ||||
| -rwxr-xr-x | dev/ci/ci-deriving.sh | 10 | ||||
| -rw-r--r-- | engine/termops.ml | 79 | ||||
| -rw-r--r-- | engine/termops.mli | 14 | ||||
| -rw-r--r-- | sysinit/usage.ml | 2 | ||||
| -rw-r--r-- | tactics/tactics.ml | 19 | ||||
| -rw-r--r-- | test-suite/bugs/closed/bug_13896.v | 24 | ||||
| -rw-r--r-- | toplevel/coqc.ml | 2 |
10 files changed, 104 insertions, 60 deletions
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index d0ffedab2a..a8bca2bffe 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -820,6 +820,13 @@ library:ci-vst: - build:edge+flambda - library:ci-flocq +library:ci-deriving: + extends: .ci-template-flambda + stage: stage-3 + needs: + - build:edge+flambda + - library:ci-mathcomp + # Plugins are by definition the projects that depend on Coq's ML API plugin:ci-aac_tactics: diff --git a/Makefile.ci b/Makefile.ci index d549ed1b39..c589c95258 100644 --- a/Makefile.ci +++ b/Makefile.ci @@ -24,6 +24,7 @@ CI_TARGETS= \ ci-coq_performance_tests \ ci-coq_tools \ ci-coqprime \ + ci-deriving \ ci-elpi \ ci-engine_bench \ ci-ext_lib \ @@ -74,6 +75,7 @@ ci-color: ci-bignums ci-coqprime: ci-bignums ci-coquelicot: ci-mathcomp +ci-deriving: ci-mathcomp ci-math_classes: ci-bignums ci-corn: ci-math_classes diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh index 8bcbd90f0b..4799755b15 100755 --- a/dev/ci/ci-basic-overlay.sh +++ b/dev/ci/ci-basic-overlay.sh @@ -308,3 +308,8 @@ project sf "https://github.com/DeepSpec/sf" "master" # Coqtail ######################################################################## project coqtail "https://github.com/whonore/Coqtail" "master" + +######################################################################## +# Deriving +######################################################################## +project deriving "https://github.com/arthuraa/deriving" "master" diff --git a/dev/ci/ci-deriving.sh b/dev/ci/ci-deriving.sh new file mode 100755 index 0000000000..ec3625c177 --- /dev/null +++ b/dev/ci/ci-deriving.sh @@ -0,0 +1,10 @@ +#!/usr/bin/env bash + +ci_dir="$(dirname "$0")" +. "${ci_dir}/ci-common.sh" + +install_ssreflect + +git_download deriving + +( cd "${CI_BUILD_DIR}/deriving" && make && make tests && make install ) diff --git a/engine/termops.ml b/engine/termops.ml index 4dc584cfa8..d60aa69ccb 100644 --- a/engine/termops.ml +++ b/engine/termops.ml @@ -979,69 +979,52 @@ let collapse_appl sigma c = match EConstr.kind sigma c with (* First utilities for avoiding telescope computation for subst_term *) -let prefix_application sigma eq_fun (k,c) t = +let prefix_application sigma eq_fun k l1 t = let open EConstr in - let c' = collapse_appl sigma c and t' = collapse_appl sigma t in - match EConstr.kind sigma c', EConstr.kind sigma t' with - | App (f1,cl1), App (f2,cl2) -> - let l1 = Array.length cl1 - and l2 = Array.length cl2 in + let t' = collapse_appl sigma t in + if 0 < l1 then match EConstr.kind sigma t' with + | App (f2,cl2) -> + let l2 = Array.length cl2 in if l1 <= l2 - && eq_fun sigma c' (mkApp (f2, Array.sub cl2 0 l1)) then - Some (mkApp (mkRel k, Array.sub cl2 l1 (l2 - l1))) + && eq_fun sigma k (mkApp (f2, Array.sub cl2 0 l1)) then + Some (Array.sub cl2 l1 (l2 - l1)) else None | _ -> None + else None -let my_prefix_application sigma eq_fun (k,c) by_c t = - let open EConstr in - let c' = collapse_appl sigma c and t' = collapse_appl sigma t in - match EConstr.kind sigma c', EConstr.kind sigma t' with - | App (f1,cl1), App (f2,cl2) -> - let l1 = Array.length cl1 - and l2 = Array.length cl2 in - if l1 <= l2 - && eq_fun sigma c' (mkApp (f2, Array.sub cl2 0 l1)) then - Some (mkApp ((Vars.lift k by_c), Array.sub cl2 l1 (l2 - l1))) - else - None - | _ -> None - -(* Recognizing occurrences of a given subterm in a term: [subst_term c t] - substitutes [(Rel 1)] for all occurrences of term [c] in a term [t]; - works if [c] has rels *) - -let subst_term_gen sigma eq_fun c t = - let open EConstr in - let open Vars in - let rec substrec (k,c as kc) t = - match prefix_application sigma eq_fun kc t with - | Some x -> x - | None -> - if eq_fun sigma c t then mkRel k - else - EConstr.map_with_binders sigma (fun (k,c) -> (k+1,lift 1 c)) substrec kc t +let eq_upto_lift cache c sigma k t = + let c = + try Int.Map.find k !cache + with Not_found -> + let c = EConstr.Vars.lift k c in + let () = cache := Int.Map.add k c !cache in + c in - substrec (1,c) t - -let subst_term sigma c t = subst_term_gen sigma EConstr.eq_constr c t + EConstr.eq_constr sigma c t (* Recognizing occurrences of a given subterm in a term : [replace_term c1 c2 t] substitutes [c2] for all occurrences of term [c1] in a term [t]; works if [c1] and [c2] have rels *) -let replace_term_gen sigma eq_fun c by_c in_t = - let rec substrec (k,c as kc) t = - match my_prefix_application sigma eq_fun kc by_c t with - | Some x -> x +let replace_term_gen sigma eq_fun ar by_c in_t = + let rec substrec k t = + match prefix_application sigma eq_fun k ar t with + | Some args -> EConstr.mkApp (EConstr.Vars.lift k by_c, args) | None -> - (if eq_fun sigma c t then (EConstr.Vars.lift k by_c) else - EConstr.map_with_binders sigma (fun (k,c) -> (k+1,EConstr.Vars.lift 1 c)) - substrec kc t) + (if eq_fun sigma k t then (EConstr.Vars.lift k by_c) else + EConstr.map_with_binders sigma succ substrec k t) in - substrec (0,c) in_t + substrec 0 in_t + +let replace_term sigma c byc t = + let cache = ref Int.Map.empty in + let c = collapse_appl sigma c in + let ar = Array.length (snd (decompose_app_vect sigma c)) in + let eq sigma k t = eq_upto_lift cache c sigma k t in + replace_term_gen sigma eq ar byc t -let replace_term sigma c byc t = replace_term_gen sigma EConstr.eq_constr c byc t +let subst_term sigma c t = replace_term sigma c (EConstr.mkRel 1) t let vars_of_env env = let s = Environ.ids_of_named_context_val (Environ.named_context_val env) in diff --git a/engine/termops.mli b/engine/termops.mli index 12df61e4c8..bdde2c450d 100644 --- a/engine/termops.mli +++ b/engine/termops.mli @@ -122,16 +122,12 @@ val pop : constr -> constr (** Substitution of an arbitrary large term. Uses equality modulo reduction of let *) -(** [subst_term_gen eq d c] replaces [d] by [Rel 1] in [c] using [eq] - as equality *) -val subst_term_gen : Evd.evar_map -> - (Evd.evar_map -> constr -> constr -> bool) -> constr -> constr -> constr - -(** [replace_term_gen eq d e c] replaces [d] by [e] in [c] using [eq] - as equality *) +(** [replace_term_gen eq arity e c] replaces matching subterms according to + [eq] by [e] in [c]. If [arity] is non-zero applications of larger length + are handled atomically. *) val replace_term_gen : - Evd.evar_map -> (Evd.evar_map -> constr -> constr -> bool) -> - constr -> constr -> constr -> constr + Evd.evar_map -> (Evd.evar_map -> int -> constr -> bool) -> + int -> constr -> constr -> constr (** [subst_term d c] replaces [d] by [Rel 1] in [c] *) val subst_term : Evd.evar_map -> constr -> constr -> constr diff --git a/sysinit/usage.ml b/sysinit/usage.ml index d00b916f23..5886b1c5b5 100644 --- a/sysinit/usage.ml +++ b/sysinit/usage.ml @@ -73,8 +73,6 @@ let print_usage_common co command = \n -debug debug mode (implies -bt)\ \n -xml-debug debug mode and print XML messages to/from coqide\ \n -diffs (on|off|removed) highlight differences between proof steps\ -\n -noglob do not dump globalizations\ -\n -dump-glob f dump globalizations in file f (to be used by coqdoc)\ \n -impredicative-set set sort Set impredicative\ \n -allow-sprop allow using the proof irrelevant SProp sort\ \n -disallow-sprop forbid using the proof irrelevant SProp sort\ diff --git a/tactics/tactics.ml b/tactics/tactics.ml index cbf12ac22f..67bf8d0d29 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -2796,7 +2796,24 @@ let generalize_goal_gen env sigma ids i ((occs,c,b),na) t cl = let open Context.Rel.Declaration in let decls,cl = decompose_prod_n_assum sigma i cl in let dummy_prod = it_mkProd_or_LetIn mkProp decls in - let newdecls,_ = decompose_prod_n_assum sigma i (subst_term_gen sigma EConstr.eq_constr_nounivs c dummy_prod) in + let newdecls,_ = + let c = Termops.collapse_appl sigma c in + let arity = Array.length (snd (Termops.decompose_app_vect sigma c)) in + let cache = ref Int.Map.empty in + let eq sigma k t = + let c = + try Int.Map.find k !cache + with Not_found -> + let c = EConstr.Vars.lift k c in + let () = cache := Int.Map.add k c !cache in + c + in + (* We use a nounivs equality because generalize morally takes a pattern as + argument, so we have to ignore freshly generated sorts. *) + EConstr.eq_constr_nounivs sigma c t + in + decompose_prod_n_assum sigma i (replace_term_gen sigma eq arity (mkRel 1) dummy_prod) + in let cl',sigma' = subst_closed_term_occ env sigma (AtOccs occs) c (it_mkProd_or_LetIn cl newdecls) in let na = generalized_name env sigma c t ids cl' na in let r = Retyping.relevance_of_type env sigma t in diff --git a/test-suite/bugs/closed/bug_13896.v b/test-suite/bugs/closed/bug_13896.v new file mode 100644 index 0000000000..10f24d8564 --- /dev/null +++ b/test-suite/bugs/closed/bug_13896.v @@ -0,0 +1,24 @@ +Inductive type : Set := + Tptr : type -> type + | Tref : type -> type + | Trv_ref : type -> type + | Tint : type -> type -> type + | Tvoid : type + | Tarray : type -> type -> type + | Tnamed : type -> type + | Tfunction : type -> type -> type -> type + | Tbool : type + | Tmember_pointer : type -> type -> type + | Tfloat : type -> type + | Tqualified : type -> type -> type + | Tnullptr : type + | Tarch : type -> type -> type +. +Definition type_eq_dec : forall (ty1 ty2 : type), { ty1 = ty2 } + { ty1 <> ty2 }. +Proof. fix IHty1 1. decide equality. Defined. + +Goal (if type_eq_dec (Tptr Tvoid) (Tptr Tvoid) then True else False). +Proof. +timeout 1 cbn. +constructor. +Qed. diff --git a/toplevel/coqc.ml b/toplevel/coqc.ml index b7af66b2ee..b78bcce6db 100644 --- a/toplevel/coqc.ml +++ b/toplevel/coqc.ml @@ -26,6 +26,8 @@ let coqc_specific_usage = Usage.{ coqc specific options:\ \n -o f.vo use f.vo as the output file name\ \n -verbose compile and output the input file\ +\n -noglob do not dump globalizations\ +\n -dump-glob f dump globalizations in file f (to be used by coqdoc)\ \n -schedule-vio2vo j f1..fn run up to j instances of Coq to turn each fi.vio\ \n into fi.vo\ \n -schedule-vio-checking j f1..fn run up to j instances of Coq to check all\ |