diff options
140 files changed, 1653 insertions, 777 deletions
diff --git a/Makefile.ide b/Makefile.ide index 640ee7b188..789acee5ec 100644 --- a/Makefile.ide +++ b/Makefile.ide @@ -296,10 +296,12 @@ $(COQIDEAPP):$(COQIDEAPP)/Contents/Resources # CoqIde for Windows special targets ########################################################################### +# This is either x86_64-w64-mingw32 or i686-w64-mingw32 +TARGET_ARCH=$(shell $CC -dumpmachine) + %.o: %.rc $(SHOW)'WINDRES $<' - $(HIDE)i686-w64-mingw32-windres -i $< -o $@ - + $(HIDE)$(TARGET_ARCH)-windres -i $< -o $@ # For emacs: # Local Variables: diff --git a/checker/checkFlags.ml b/checker/checkFlags.ml index 1f5e76bd83..369623e8c5 100644 --- a/checker/checkFlags.ml +++ b/checker/checkFlags.ml @@ -18,6 +18,7 @@ let set_local_flags flags env = check_universes = flags.check_universes; conv_oracle = flags.conv_oracle; cumulative_sprop = flags.cumulative_sprop; + allow_uip = flags.allow_uip; } in Environ.set_typing_flags flags env diff --git a/checker/checker.ml b/checker/checker.ml index 086acc482c..e2c90e2b93 100644 --- a/checker/checker.ml +++ b/checker/checker.ml @@ -95,12 +95,10 @@ let add_rec_path ~unix_path ~coq_root = else Feedback.msg_warning (str "Cannot open " ++ str unix_path) -(* By the option -include -I or -R of the command line *) +(* By the option -R/-Q of the command line *) let includes = ref [] let push_include (s, alias) = includes := (s,alias) :: !includes -let set_default_include d = - push_include (d, Check.default_root_prefix) let set_include d p = let p = dirpath_of_string p in push_include (d,p) @@ -127,7 +125,7 @@ let init_load_path () = List.iter (fun s -> add_rec_path ~unix_path:s ~coq_root:Check.default_root_prefix) coqpath; (* then current directory *) add_path ~unix_path:"." ~coq_root:Check.default_root_prefix; - (* additional loadpath, given with -I -include -R options *) + (* additional loadpath, given with -R/-Q options *) List.iter (fun (unix_path, coq_root) -> add_rec_path ~unix_path ~coq_root) (List.rev !includes); @@ -299,6 +297,7 @@ let explain_exn = function | UnsatisfiedConstraints _ -> str"UnsatisfiedConstraints" | DisallowedSProp -> str"DisallowedSProp" | BadRelevance -> str"BadRelevance" + | BadInvert -> str"BadInvert" | UndeclaredUniverse _ -> str"UndeclaredUniverse")) | InductiveError e -> @@ -320,9 +319,6 @@ let explain_exn = function report ()) | e -> CErrors.print e (* for anomalies and other uncaught exceptions *) -let deprecated flag = - Feedback.msg_warning (str "Deprecated flag " ++ quote (str flag)) - let parse_args argv = let rec parse = function | [] -> () @@ -338,16 +334,8 @@ let parse_args argv = Envars.set_user_coqlib s; parse rem - | ("-I"|"-include") :: d :: "-as" :: p :: rem -> deprecated "-I"; set_include d p; parse rem - | ("-I"|"-include") :: d :: "-as" :: [] -> usage () - | ("-I"|"-include") :: d :: rem -> deprecated "-I"; set_default_include d; parse rem - | ("-I"|"-include") :: [] -> usage () - - | "-Q" :: d :: p :: rem -> set_include d p;parse rem - | "-Q" :: ([] | [_]) -> usage () - - | "-R" :: d :: p :: rem -> set_include d p;parse rem - | "-R" :: ([] | [_]) -> usage () + | ("-Q"|"-R") :: d :: p :: rem -> set_include d p;parse rem + | ("-Q"|"-R") :: ([] | [_]) -> usage () | "-debug" :: rem -> set_debug (); parse rem diff --git a/checker/values.ml b/checker/values.ml index cce0ce7203..178a3d8624 100644 --- a/checker/values.ml +++ b/checker/values.ml @@ -147,7 +147,7 @@ let rec v_constr = [|v_puniverses v_cst|]; (* Const *) [|v_puniverses v_ind|]; (* Ind *) [|v_puniverses v_cons|]; (* Construct *) - [|v_caseinfo;v_constr;v_constr;Array v_constr|]; (* Case *) + [|v_caseinfo;v_constr;v_case_invert;v_constr;Array v_constr|]; (* Case *) [|v_fix|]; (* Fix *) [|v_cofix|]; (* CoFix *) [|v_proj;v_constr|]; (* Proj *) @@ -159,6 +159,7 @@ and v_prec = Tuple ("prec_declaration", [|Array (v_binder_annot v_name); Array v_constr; Array v_constr|]) and v_fix = Tuple ("pfixpoint", [|Tuple ("fix2",[|Array Int;Int|]);v_prec|]) and v_cofix = Tuple ("pcofixpoint",[|Int;v_prec|]) +and v_case_invert = Sum ("case_inversion", 1, [|[|v_instance;Array v_constr|]|]) let v_rdecl = v_sum "rel_declaration" 0 [| [|v_binder_annot v_name; v_constr|]; (* LocalAssum *) @@ -244,7 +245,7 @@ let v_typing_flags = v_tuple "typing_flags" [|v_bool; v_bool; v_bool; v_oracle; v_bool; v_bool; - v_bool; v_bool; v_bool|] + v_bool; v_bool; v_bool; v_bool|] let v_univs = v_sum "universes" 0 [|[|v_context_set|]; [|v_abs_context|]|] diff --git a/dev/build/windows/makecoq_mingw.sh b/dev/build/windows/makecoq_mingw.sh index 6ceb7f54b2..cc9fd13fdc 100755 --- a/dev/build/windows/makecoq_mingw.sh +++ b/dev/build/windows/makecoq_mingw.sh @@ -1401,10 +1401,6 @@ function make_coq { logn configure ./configure -with-doc no -prefix "$PREFIXCOQ" fi - # The windows resource compiler binary name is hard coded - sed -i "s/i686-w64-mingw32-windres/$TARGET_ARCH-windres/" Makefile.build - sed -i "s/i686-w64-mingw32-windres/$TARGET_ARCH-windres/" Makefile.ide || true - # 8.4x doesn't support parallel make if [[ $COQ_VERSION == 8.4* ]] ; then log1 make diff --git a/dev/ci/user-overlays/10390-SkySkimmer-uip.sh b/dev/ci/user-overlays/10390-SkySkimmer-uip.sh new file mode 100644 index 0000000000..80107ac9c5 --- /dev/null +++ b/dev/ci/user-overlays/10390-SkySkimmer-uip.sh @@ -0,0 +1,30 @@ +if [ "$CI_PULL_REQUEST" = "10390" ] || [ "$CI_BRANCH" = "uip" ]; then + + unicoq_CI_REF=uip + unicoq_CI_GITURL=https://github.com/SkySkimmer/unicoq + + mtac2_CI_REF=uip + mtac2_CI_GITURL=https://github.com/SkySkimmer/Mtac2 + + elpi_CI_REF=uip + elpi_CI_GITURL=https://github.com/SkySkimmer/coq-elpi + + equations_CI_REF=uip + equations_CI_GITURL=https://github.com/SkySkimmer/Coq-Equations + + paramcoq_CI_REF=uip + paramcoq_CI_GITURL=https://github.com/SkySkimmer/paramcoq + + relation_algebra_CI_REF=uip + relation_algebra_CI_GITURL=https://github.com/SkySkimmer/relation-algebra + + coq_dpdgraph_CI_REF=uip + coq_dpdgraph_CI_GITURL=https://github.com/SkySkimmer/coq-dpdgraph + + coqhammer_CI_REF=uip + coqhammer_CI_GITURL=https://github.com/SkySkimmer/coqhammer + + metacoq_CI_REF=uip + metacoq_CI_GITURL=https://github.com/SkySkimmer/metacoq + +fi diff --git a/dev/ci/user-overlays/12523-term-notation-custom.sh b/dev/ci/user-overlays/12523-term-notation-custom.sh new file mode 100644 index 0000000000..6217312a2a --- /dev/null +++ b/dev/ci/user-overlays/12523-term-notation-custom.sh @@ -0,0 +1,6 @@ +if [ "$CI_PULL_REQUEST" = "12523" ] || [ "$CI_BRANCH" = "fix-11121" ]; then + + equations_CI_REF=fix-11121 + equations_CI_GITURL=https://github.com/maximedenes/Coq-Equations + +fi diff --git a/dev/doc/SProp.md b/dev/doc/SProp.md index f263dbb867..d517983046 100644 --- a/dev/doc/SProp.md +++ b/dev/doc/SProp.md @@ -39,3 +39,32 @@ Relevance can be inferred from a well-typed term using functions in term, note the difference between its relevance as a term (is `x : (_ : SProp)`) and as a type (is `x : SProp`), there are functions for both kinds. + +## Case inversion + +Inductives in SProp with 1 constructor which has no arguments have a +special reduction rule for matches. To implement it the Case +constructor is extended with a `case_invert` field. + +If you are constructing a match on a normal (non-special reduction) +inductive you must fill the new field with `NoInvert`. Otherwise you +must fill it with `CaseInvert {univs ; args}` where `univs` is the +universe instance of the type you are matching and `args` the +parameters and indices. + +For instance, in + +~~~coq +Inductive seq {A} (a:A) : A -> SProp := + srefl : seq a a. + +Definition seq_to_eq {A x y} (e:seq x y) : x = y :> A + := match e with srefl => eq_refl end. +~~~ + +the `match e with ...` has `CaseInvert {univs = Instance.empty; args = [|A x y|]}`. +(empty instance since we defined a universe monomorphic `seq`). + +In practice, you should use `Inductiveops.make_case_or_project` which +will take care of this for you (and also handles primitive records +correctly etc). diff --git a/dev/top_printers.ml b/dev/top_printers.ml index f14edec639..3df6f986ce 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -238,7 +238,9 @@ let ppnamedcontextval e = let ppaucontext auctx = let nas = AUContext.names auctx in let prlev l = match Level.var_index l with - | Some n -> Name.print nas.(n) + | Some n -> (match nas.(n) with + | Anonymous -> prlev l + | Name id -> Id.print id) | None -> prlev l in pp (pr_universe_context prlev (AUContext.repr auctx)) @@ -294,7 +296,7 @@ let constr_display csr = "MutConstruct(("^(MutInd.to_string sp)^","^(string_of_int i)^")," ^","^(universes_display u)^(string_of_int j)^")" | Proj (p, c) -> "Proj("^(Constant.to_string (Projection.constant p))^","^term_display c ^")" - | Case (ci,p,c,bl) -> + | Case (ci,p,iv,c,bl) -> "MutCase(<abs>,"^(term_display p)^","^(term_display c)^"," ^(array_display bl)^")" | Fix ((t,i),(lna,tl,bl)) -> @@ -406,7 +408,7 @@ let print_pure_constr csr = print_int i; print_string ","; print_int j; print_string ","; universes_display u; print_string ")" - | Case (ci,p,c,bl) -> + | Case (ci,p,iv,c,bl) -> open_vbox 0; print_string "<"; box_display p; print_string ">"; print_cut(); print_string "Case"; diff --git a/doc/changelog/01-kernel/10390-uip.rst b/doc/changelog/01-kernel/10390-uip.rst new file mode 100644 index 0000000000..dab096d8db --- /dev/null +++ b/doc/changelog/01-kernel/10390-uip.rst @@ -0,0 +1,5 @@ +- **Added:** + Definitional UIP, only when :flag:`Definitional UIP` is enabled. See + documentation of the flag for details. + (`#10390 <https://github.com/coq/coq/pull/10390>`_, + by Gaëtan Gilbert). diff --git a/doc/changelog/03-notations/12523-term-notation-custom.rst b/doc/changelog/03-notations/12523-term-notation-custom.rst new file mode 100644 index 0000000000..1a611f3fb1 --- /dev/null +++ b/doc/changelog/03-notations/12523-term-notation-custom.rst @@ -0,0 +1,4 @@ +- **Added:** + Simultaneous definition of terms and notations now support custom entries. + Fixes `#11121 <https://github.com/coq/coq/pull/11121>`_. + (`#12523 <https://github.com/coq/coq/pull/11523>`_, by Maxime Dénès). diff --git a/doc/changelog/04-tactics/12572-fix-12571.rst b/doc/changelog/04-tactics/12572-fix-12571.rst new file mode 100644 index 0000000000..98b217e86b --- /dev/null +++ b/doc/changelog/04-tactics/12572-fix-12571.rst @@ -0,0 +1,6 @@ +- **Fixed:** + typeclasses eauto (and discriminated hint bases) now correctly + classify local variables as being unfoldable + (`#12572 <https://github.com/coq/coq/pull/12572>`_, + fixes `#12571 <https://github.com/coq/coq/issues/12571>`_, + by Pierre-Marie Pédrot). diff --git a/doc/changelog/05-tactic-language/12594-fix-ltac2-type-params.rst b/doc/changelog/05-tactic-language/12594-fix-ltac2-type-params.rst new file mode 100644 index 0000000000..555020d319 --- /dev/null +++ b/doc/changelog/05-tactic-language/12594-fix-ltac2-type-params.rst @@ -0,0 +1,5 @@ +- **Fixed:** + Fix the parsing of multi-parameters Ltac2 types + (`#12594 <https://github.com/coq/coq/pull/12594>`_, + fixes `#12595 <https://github.com/coq/coq/issues/12595>`_, + by Pierre-Marie Pédrot). diff --git a/doc/changelog/08-tools/12613-coqchk-noi.rst b/doc/changelog/08-tools/12613-coqchk-noi.rst new file mode 100644 index 0000000000..b83c9c69a2 --- /dev/null +++ b/doc/changelog/08-tools/12613-coqchk-noi.rst @@ -0,0 +1,3 @@ +- **Removed:** The option ``-I`` of coqchk was removed (it was + deprecated in Coq 8.8) (`#12613 + <https://github.com/coq/coq/pull/12613>`_, by Gaëtan Gilbert). diff --git a/doc/sphinx/addendum/sprop.rst b/doc/sphinx/addendum/sprop.rst index b19239ed22..6c62ff3116 100644 --- a/doc/sphinx/addendum/sprop.rst +++ b/doc/sphinx/addendum/sprop.rst @@ -173,6 +173,79 @@ strict propositions. For instance: Definition eq_true_is_true b (H:true=b) : is_true b := match H in _ = x return is_true x with eq_refl => stt end. +Definitional UIP +---------------- + +.. flag:: Definitional UIP + + This flag, off by default, allows the declaration of non-squashed + inductive types with 1 constructor which takes no argument in + |SProp|. Since this includes equality types, it provides + definitional uniqueness of identity proofs. + + Because squashing is a universe restriction, unsetting + :flag:`Universe Checking` is stronger than setting + :flag:`Definitional UIP`. + +Definitional UIP involves a special reduction rule through which +reduction depends on conversion. Consider the following code: + +.. coqtop:: in + + Set Definitional UIP. + + Inductive seq {A} (a:A) : A -> SProp := + srefl : seq a a. + + Axiom e : seq 0 0. + Definition hidden_arrow := match e return Set with srefl _ => nat -> nat end. + + Check (fun (f : hidden_arrow) (x:nat) => (f : nat -> nat) x). + +By the usual reduction rules :g:`hidden_arrow` is a stuck match, but +by proof irrelevance :g:`e` is convertible to :g:`srefl 0` and then by +congruence :g:`hidden_arrow` is convertible to `nat -> nat`. + +The special reduction reduces any match on a type which uses +definitional UIP when the indices are convertible to those of the +constructor. For `seq`, this means a match on a value of type `seq x +y` reduces if and only if `x` and `y` are convertible. + +Such matches are indicated in the printed representation by inserting +a cast around the discriminee: + +.. coqtop:: out + + Print hidden_arrow. + +Non Termination with UIP +++++++++++++++++++++++++ + +The special reduction rule of UIP combined with an impredicative sort +breaks termination of reduction +:cite:`abel19:failur_normal_impred_type_theor`: + +.. coqtop:: all + + Axiom all_eq : forall (P Q:Prop), P -> Q -> seq P Q. + + Definition transport (P Q:Prop) (x:P) (y:Q) : Q + := match all_eq P Q x y with srefl _ => x end. + + Definition top : Prop := forall P : Prop, P -> P. + + Definition c : top := + fun P p => + transport + (top -> top) + P + (fun x : top => x (top -> top) (fun x => x) x) + p. + + Fail Timeout 1 Eval lazy in c (top -> top) (fun x => x) c. + +The term :g:`c (top -> top) (fun x => x) c` infinitely reduces to itself. + Issues with non-cumulativity ---------------------------- diff --git a/doc/sphinx/biblio.bib b/doc/sphinx/biblio.bib index 3d73f9bd6e..e0eec2ae2d 100644 --- a/doc/sphinx/biblio.bib +++ b/doc/sphinx/biblio.bib @@ -608,3 +608,12 @@ the Calculus of Inductive Constructions}}, publisher = {ACM}, address = {New York, NY, USA}, } + +@techreport{abel19:failur_normal_impred_type_theor, + author = {Andreas Abel AND Thierry Coquand}, + title = {{Failure of Normalization in Impredicative Type + Theory with Proof-Irrelevant Propositional + Equality}}, + year = 2019, + institution = {Chalmers and Gothenburg University}, +} diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst index 3c92206fd2..fcd5ecc070 100644 --- a/doc/sphinx/user-extensions/syntax-extensions.rst +++ b/doc/sphinx/user-extensions/syntax-extensions.rst @@ -368,13 +368,14 @@ a :token:`decl_notations` clause after the definition of the (co)inductive type (co)recursive term (or after the definition of each of them in case of mutual definitions). The exact syntax is given by :n:`@decl_notation` for inductive, co-inductive, recursive and corecursive definitions and in :ref:`record-types` -for records. +for records. Note that only syntax modifiers that do not require to add or +change a parsing rule are accepted. .. insertprodn decl_notations decl_notation .. prodn:: decl_notations ::= where @decl_notation {* and @decl_notation } - decl_notation ::= @string := @one_term {? ( only parsing ) } {? : @scope_name } + decl_notation ::= @string := @one_term {? ( {+, @syntax_modifier } ) } {? : @scope_name } Here are examples: diff --git a/engine/eConstr.ml b/engine/eConstr.ml index 42c9359ff0..32eb63a818 100644 --- a/engine/eConstr.ml +++ b/engine/eConstr.ml @@ -69,7 +69,7 @@ let mkInd i = of_kind (Ind (in_punivs i)) let mkConstructU pc = of_kind (Construct pc) let mkConstruct c = of_kind (Construct (in_punivs c)) let mkConstructUi ((ind,u),i) = of_kind (Construct ((ind,i),u)) -let mkCase (ci, c, r, p) = of_kind (Case (ci, c, r, p)) +let mkCase (ci, c, iv, r, p) = of_kind (Case (ci, c, iv, r, p)) let mkFix f = of_kind (Fix f) let mkCoFix f = of_kind (CoFix f) let mkProj (p, c) = of_kind (Proj (p, c)) @@ -194,7 +194,7 @@ let destCoFix sigma c = match kind sigma c with | _ -> raise DestKO let destCase sigma c = match kind sigma c with -| Case (ci, t, c, p) -> (ci, t, c, p) +| Case (ci, t, iv, c, p) -> (ci, t, iv, c, p) | _ -> raise DestKO let destProj sigma c = match kind sigma c with @@ -356,7 +356,7 @@ let iter_with_full_binders sigma g f n c = | LetIn (na,b,t,c) -> f n b; f n t; f (g (LocalDef (na, b, t)) n) c | App (c,l) -> f n c; Array.Fun1.iter f n l | Evar (_,l) -> List.iter (fun c -> f n c) l - | Case (_,p,c,bl) -> f n p; f n c; Array.Fun1.iter f n bl + | Case (_,p,iv,c,bl) -> f n p; iter_invert (f n) iv; f n c; Array.Fun1.iter f n bl | Proj (p,c) -> f n c | Fix (_,(lna,tl,bl)) -> Array.iter (f n) tl; @@ -380,7 +380,7 @@ let compare_gen k eq_inst eq_sort eq_constr nargs c1 c2 = let eq_constr sigma c1 c2 = let kind c = kind sigma c in - let eq_inst _ _ i1 i2 = EInstance.equal sigma i1 i2 in + let eq_inst _ i1 i2 = EInstance.equal sigma i1 i2 in let eq_sorts s1 s2 = ESorts.equal sigma s1 s2 in let rec eq_constr nargs c1 c2 = compare_gen kind eq_inst eq_sorts eq_constr nargs c1 c2 @@ -390,13 +390,13 @@ let eq_constr sigma c1 c2 = let eq_constr_nounivs sigma c1 c2 = let kind c = kind sigma c in let rec eq_constr nargs c1 c2 = - compare_gen kind (fun _ _ _ _ -> true) (fun _ _ -> true) eq_constr nargs c1 c2 + compare_gen kind (fun _ _ _ -> true) (fun _ _ -> true) eq_constr nargs c1 c2 in eq_constr 0 c1 c2 let compare_constr sigma cmp c1 c2 = let kind c = kind sigma c in - let eq_inst _ _ i1 i2 = EInstance.equal sigma i1 i2 in + let eq_inst _ i1 i2 = EInstance.equal sigma i1 i2 in let eq_sorts s1 s2 = ESorts.equal sigma s1 s2 in let cmp nargs c1 c2 = cmp c1 c2 in compare_gen kind eq_inst eq_sorts cmp 0 c1 c2 @@ -442,22 +442,22 @@ let cmp_constructors (mind, ind, cns as spec) nargs u1 u2 cstrs = Array.fold_left2 (fun cstrs u1 u2 -> UnivProblem.(Set.add (UWeak (u1,u2)) cstrs)) cstrs (Univ.Instance.to_array u1) (Univ.Instance.to_array u2) -let eq_universes env sigma cstrs cv_pb ref nargs l l' = +let eq_universes env sigma cstrs cv_pb refargs l l' = if EInstance.is_empty l then (assert (EInstance.is_empty l'); true) else let l = EInstance.kind sigma l and l' = EInstance.kind sigma l' in let open GlobRef in let open UnivProblem in - match ref with - | VarRef _ -> assert false (* variables don't have instances *) - | ConstRef _ -> + match refargs with + | None | Some (ConstRef _, _) -> cstrs := enforce_eq_instances_univs true l l' !cstrs; true - | IndRef ind -> + | Some (VarRef _, _) -> assert false (* variables don't have instances *) + | Some (IndRef ind, nargs) -> let mind = Environ.lookup_mind (fst ind) env in cstrs := cmp_inductives cv_pb (mind,snd ind) nargs l l' !cstrs; true - | ConstructRef ((mi,ind),ctor) -> + | Some (ConstructRef ((mi,ind),ctor), nargs) -> let mind = Environ.lookup_mind mi env in cstrs := cmp_constructors (mind,ind,ctor) nargs l l' !cstrs; true @@ -469,8 +469,8 @@ let test_constr_universes env sigma leq m n = else let cstrs = ref Set.empty in let cv_pb = if leq then Reduction.CUMUL else Reduction.CONV in - let eq_universes ref nargs l l' = eq_universes env sigma cstrs Reduction.CONV ref nargs l l' - and leq_universes ref nargs l l' = eq_universes env sigma cstrs cv_pb ref nargs l l' in + let eq_universes refargs l l' = eq_universes env sigma cstrs Reduction.CONV refargs l l' + and leq_universes refargs l l' = eq_universes env sigma cstrs cv_pb refargs l l' in let eq_sorts s1 s2 = let s1 = ESorts.kind sigma s1 in let s2 = ESorts.kind sigma s2 in @@ -777,5 +777,7 @@ let to_named_context = = fun Refl x -> x in gen unsafe_eq +let to_case_invert = unsafe_to_case_invert + let eq = unsafe_eq end diff --git a/engine/eConstr.mli b/engine/eConstr.mli index aea441b90b..2bf8f69af7 100644 --- a/engine/eConstr.mli +++ b/engine/eConstr.mli @@ -128,7 +128,7 @@ val mkIndU : inductive * EInstance.t -> t val mkConstruct : constructor -> t val mkConstructU : constructor * EInstance.t -> t val mkConstructUi : (inductive * EInstance.t) * int -> t -val mkCase : case_info * t * t * t array -> t +val mkCase : case_info * t * (t,EInstance.t) case_invert * t * t array -> t val mkFix : (t, t) pfixpoint -> t val mkCoFix : (t, t) pcofixpoint -> t val mkArrow : t -> Sorts.relevance -> t -> t @@ -198,7 +198,7 @@ val destConst : Evd.evar_map -> t -> Constant.t * EInstance.t val destEvar : Evd.evar_map -> t -> t pexistential val destInd : Evd.evar_map -> t -> inductive * EInstance.t val destConstruct : Evd.evar_map -> t -> constructor * EInstance.t -val destCase : Evd.evar_map -> t -> case_info * t * t * t array +val destCase : Evd.evar_map -> t -> case_info * t * (t,EInstance.t) case_invert * t * t array val destProj : Evd.evar_map -> t -> Projection.t * t val destFix : Evd.evar_map -> t -> (t, t) pfixpoint val destCoFix : Evd.evar_map -> t -> (t, t) pcofixpoint @@ -341,6 +341,8 @@ val of_rel_decl : (Constr.t, Constr.types) Context.Rel.Declaration.pt -> (t, typ val to_rel_decl : Evd.evar_map -> (t, types) Context.Rel.Declaration.pt -> (Constr.t, Constr.types) Context.Rel.Declaration.pt +val of_case_invert : (Constr.t,Univ.Instance.t) case_invert -> (t,EInstance.t) case_invert + (** {5 Unsafe operations} *) module Unsafe : @@ -365,6 +367,8 @@ sig val to_instance : EInstance.t -> Univ.Instance.t (** Physical identity. Does not care for normalization. *) + val to_case_invert : (t,EInstance.t) case_invert -> (Constr.t,Univ.Instance.t) case_invert + val eq : (t, Constr.t) eq (** Use for transparent cast between types. *) end diff --git a/engine/evarutil.ml b/engine/evarutil.ml index eea7e38f87..423af1d4ec 100644 --- a/engine/evarutil.ml +++ b/engine/evarutil.ml @@ -127,10 +127,11 @@ let is_ground_env evd env = (* Memoization is safe since evar_map and environ are applicative structures *) let memo f = - let m = ref None in - fun x y -> match !m with - | Some (x', y', r) when x == x' && y == y' -> r - | _ -> let r = f x y in m := Some (x, y, r); r + let module E = Ephemeron.K2 in + let m = E.create () in + fun x y -> match E.get_key1 m, E.get_key2 m with + | Some x', Some y' when x == x' && y == y' -> Option.get (E.get_data m) + | _ -> let r = f x y in E.set_key1 m x; E.set_key2 m y; E.set_data m r; r let is_ground_env = memo is_ground_env @@ -143,7 +144,7 @@ let head_evar sigma c = let c = EConstr.Unsafe.to_constr c in let rec hrec c = match kind c with | Evar (evk,_) -> evk - | Case (_,_,c,_) -> hrec c + | Case (_,_,_,c,_) -> hrec c | App (c,_) -> hrec c | Cast (c,_,_) -> hrec c | Proj (p, c) -> hrec c diff --git a/engine/evd.ml b/engine/evd.ml index f0ee8ae68f..c570f75c6b 100644 --- a/engine/evd.ml +++ b/engine/evd.ml @@ -1398,6 +1398,9 @@ module MiniEConstr = struct let unsafe_to_rel_decl d = d let to_rel_decl sigma d = Context.Rel.Declaration.map_constr (to_constr sigma) d + let unsafe_to_case_invert x = x + let of_case_invert x = x + end (** The following functions return the set of evars immediately diff --git a/engine/evd.mli b/engine/evd.mli index d9b7bd76e7..679173ca72 100644 --- a/engine/evd.mli +++ b/engine/evd.mli @@ -732,6 +732,8 @@ module MiniEConstr : sig (Constr.t, Constr.types) Context.Named.Declaration.pt val unsafe_to_rel_decl : (t, t) Context.Rel.Declaration.pt -> (Constr.t, Constr.types) Context.Rel.Declaration.pt + val of_case_invert : (constr,Univ.Instance.t) case_invert -> (econstr,EInstance.t) case_invert + val unsafe_to_case_invert : (econstr,EInstance.t) case_invert -> (constr,Univ.Instance.t) case_invert val of_rel_decl : (Constr.t, Constr.types) Context.Rel.Declaration.pt -> (t, t) Context.Rel.Declaration.pt val to_rel_decl : evar_map -> (t, t) Context.Rel.Declaration.pt -> diff --git a/engine/namegen.ml b/engine/namegen.ml index c4472050f8..1cf5be10ae 100644 --- a/engine/namegen.ml +++ b/engine/namegen.ml @@ -118,7 +118,7 @@ let head_name sigma c = (* Find the head constant of a constr if any *) Some (Nametab.basename_of_global (global_of_constr c)) | Fix ((_,i),(lna,_,_)) | CoFix (i,(lna,_,_)) -> Some (match lna.(i).binder_name with Name id -> id | _ -> assert false) - | Sort _ | Rel _ | Meta _|Evar _|Case (_, _, _, _) | Int _ | Float _ -> None + | Sort _ | Rel _ | Meta _|Evar _|Case _ | Int _ | Float _ -> None in hdrec c @@ -163,7 +163,7 @@ let hdchar env sigma c = let id = match lna.(i).binder_name with Name id -> id | _ -> assert false in lowercase_first_char id | Evar _ (* We could do better... *) - | Meta _ | Case (_, _, _, _) -> "y" + | Meta _ | Case _ -> "y" | Int _ -> "i" | Float _ -> "f" in diff --git a/engine/termops.ml b/engine/termops.ml index c51e753d46..f6d0807823 100644 --- a/engine/termops.ml +++ b/engine/termops.ml @@ -639,13 +639,14 @@ let map_constr_with_binders_left_to_right sigma g f l c = let al' = List.map_left (f l) al in if List.for_all2 (==) al' al then c else mkEvar (e, al') - | Case (ci,p,b,bl) -> + | Case (ci,p,iv,b,bl) -> (* In v8 concrete syntax, predicate is after the term to match! *) let b' = f l b in + let iv' = map_invert (f l) iv in let p' = f l p in let bl' = Array.map_left (f l) bl in - if b' == b && p' == p && bl' == bl then c - else mkCase (ci, p', b', bl') + if b' == b && p' == p && iv' == iv && bl' == bl then c + else mkCase (ci, p', iv', b', bl') | Fix (ln,(lna,tl,bl as fx)) -> let l' = fold_rec_types g fx l in let (tl', bl') = map_left2 (f l) tl (f l') bl in @@ -709,18 +710,20 @@ let map_constr_with_full_binders_gen userview sigma g f l cstr = | Evar (e,al) -> let al' = List.map (f l) al in if List.for_all2 (==) al al' then cstr else mkEvar (e, al') - | Case (ci,p,c,bl) when userview -> + | Case (ci,p,iv,c,bl) when userview -> let p' = map_return_predicate_with_full_binders sigma g f l ci p in + let iv' = map_invert (f l) iv in let c' = f l c in let bl' = map_branches_with_full_binders sigma g f l ci bl in - if p==p' && c==c' && bl'==bl then cstr else - mkCase (ci, p', c', bl') - | Case (ci,p,c,bl) -> + if p==p' && iv'==iv && c==c' && bl'==bl then cstr else + mkCase (ci, p', iv', c', bl') + | Case (ci,p,iv,c,bl) -> let p' = f l p in + let iv' = map_invert (f l) iv in let c' = f l c in let bl' = Array.map (f l) bl in - if p==p' && c==c' && Array.for_all2 (==) bl bl' then cstr else - mkCase (ci, p', c', bl') + if p==p' && iv'==iv && c==c' && Array.for_all2 (==) bl bl' then cstr else + mkCase (ci, p', iv', c', bl') | Fix (ln,(lna,tl,bl as fx)) -> let tl' = Array.map (f l) tl in let l' = fold_rec_types g fx l in diff --git a/engine/univProblem.ml b/engine/univProblem.ml index 08ff9efa5b..8d6689933c 100644 --- a/engine/univProblem.ml +++ b/engine/univProblem.ml @@ -150,7 +150,7 @@ let eq_constr_univs_infer_with kind1 kind2 univs fold m n accu = [kind1,kind2], because [kind1] and [kind2] may be different, typically evaluating [m] and [n] in different evar maps. *) let cstrs = ref accu in - let eq_universes _ _ = UGraph.check_eq_instances univs in + let eq_universes _ = UGraph.check_eq_instances univs in let eq_sorts s1 s2 = if Sorts.equal s1 s2 then true else diff --git a/engine/univSubst.ml b/engine/univSubst.ml index 92211d5f3d..f06aeaf54e 100644 --- a/engine/univSubst.ml +++ b/engine/univSubst.ml @@ -146,7 +146,11 @@ let nf_evars_and_universes_opt_subst f subst = if pu' == pu then c else mkConstructU pu' | Sort (Type u) -> let u' = Univ.subst_univs_universe subst u in - if u' == u then c else mkSort (sort_of_univ u') + if u' == u then c else mkSort (sort_of_univ u') + | Case (ci,p,CaseInvert {univs;args},t,br) -> + let univs' = Instance.subst_fn lsubst univs in + if univs' == univs then Constr.map aux c + else Constr.map aux (mkCase (ci,p,CaseInvert {univs=univs';args},t,br)) | _ -> Constr.map aux c in aux diff --git a/interp/constrexpr.ml b/interp/constrexpr.ml index 21f682ac0e..9c4b78f4ed 100644 --- a/interp/constrexpr.ml +++ b/interp/constrexpr.ml @@ -29,10 +29,10 @@ type notation_entry_level = InConstrEntrySomeLevel | InCustomEntryLevel of strin type notation_key = string (* A notation associated to a given parsing rule *) -type notation = notation_entry_level * notation_key +type notation = notation_entry * notation_key (* A notation associated to a given interpretation *) -type specific_notation = notation_with_optional_scope * notation +type specific_notation = notation_with_optional_scope * (notation_entry * notation_key) type 'a or_by_notation_r = | AN of 'a diff --git a/interp/constrextern.ml b/interp/constrextern.ml index 63079993c8..b087431e85 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -359,14 +359,14 @@ let make_notation_gen loc ntn mknot mkprim destprim l bl = (* Special case to avoid writing "- 3" for e.g. (Z.opp 3) *) | "- _", [Some (Numeral p)] when not (NumTok.Signed.is_zero p) -> assert (bl=[]); - mknot (loc,ntn,([mknot (loc,(InConstrEntrySomeLevel,"( _ )"),l,[])]),[]) + mknot (loc,ntn,([mknot (loc,(InConstrEntry,"( _ )"),l,[])]),[]) | _ -> match decompose_notation_key ntn, l with - | (InConstrEntrySomeLevel,[Terminal "-"; Terminal x]), [] -> + | (InConstrEntry,[Terminal "-"; Terminal x]), [] -> begin match NumTok.Unsigned.parse_string x with | Some n -> mkprim (loc, Numeral (NumTok.SMinus,n)) | None -> mknot (loc,ntn,l,bl) end - | (InConstrEntrySomeLevel,[Terminal x]), [] -> + | (InConstrEntry,[Terminal x]), [] -> begin match NumTok.Unsigned.parse_string x with | Some n -> mkprim (loc, Numeral (NumTok.SPlus,n)) | None -> mknot (loc,ntn,l,bl) end @@ -486,7 +486,13 @@ and apply_notation_to_pattern ?loc gr ((subst,substlist),(no_implicit,nb_to_drop function | NotationRule (_,ntn as specific_ntn) -> begin - match availability_of_entry_coercion custom (fst ntn) with + let notation_entry_level = match (fst ntn) with + | InConstrEntry -> InConstrEntrySomeLevel + | InCustomEntry s -> + let (_,level,_) = Notation.level_of_notation ntn in + InCustomEntryLevel (s, level) + in + match availability_of_entry_coercion custom notation_entry_level with | None -> raise No_match | Some coercion -> match availability_of_notation specific_ntn (tmp_scope,scopes) with @@ -1260,7 +1266,13 @@ and extern_notation (custom,scopes as allscopes) vars t rules = (* Try availability of interpretation ... *) match keyrule with | NotationRule (_,ntn as specific_ntn) -> - (match availability_of_entry_coercion custom (fst ntn) with + let notation_entry_level = match (fst ntn) with + | InConstrEntry -> InConstrEntrySomeLevel + | InCustomEntry s -> + let (_,level,_) = Notation.level_of_notation ntn in + InCustomEntryLevel (s, level) + in + (match availability_of_entry_coercion custom notation_entry_level with | None -> raise No_match | Some coercion -> match availability_of_notation specific_ntn scopes with diff --git a/interp/constrintern.ml b/interp/constrintern.ml index ee041ed088..d95554de56 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -224,35 +224,35 @@ let expand_notation_string ntn n = (* Remark: expansion of squash at definition is done in metasyntax.ml *) let contract_curly_brackets ntn (l,ll,bl,bll) = match ntn with - | InCustomEntryLevel _,_ -> ntn,(l,ll,bl,bll) - | InConstrEntrySomeLevel, ntn -> + | InCustomEntry _,_ -> ntn,(l,ll,bl,bll) + | InConstrEntry, ntn -> let ntn' = ref ntn in let rec contract_squash n = function | [] -> [] - | { CAst.v = CNotation (None,(InConstrEntrySomeLevel,"{ _ }"),([a],[],[],[])) } :: l -> + | { CAst.v = CNotation (None,(InConstrEntry,"{ _ }"),([a],[],[],[])) } :: l -> ntn' := expand_notation_string !ntn' n; contract_squash n (a::l) | a :: l -> a::contract_squash (n+1) l in let l = contract_squash 0 l in (* side effect; don't inline *) - (InConstrEntrySomeLevel,!ntn'),(l,ll,bl,bll) + (InConstrEntry,!ntn'),(l,ll,bl,bll) let contract_curly_brackets_pat ntn (l,ll) = match ntn with - | InCustomEntryLevel _,_ -> ntn,(l,ll) - | InConstrEntrySomeLevel, ntn -> + | InCustomEntry _,_ -> ntn,(l,ll) + | InConstrEntry, ntn -> let ntn' = ref ntn in let rec contract_squash n = function | [] -> [] - | { CAst.v = CPatNotation (None,(InConstrEntrySomeLevel,"{ _ }"),([a],[]),[]) } :: l -> + | { CAst.v = CPatNotation (None,(InConstrEntry,"{ _ }"),([a],[]),[]) } :: l -> ntn' := expand_notation_string !ntn' n; contract_squash n (a::l) | a :: l -> a::contract_squash (n+1) l in let l = contract_squash 0 l in (* side effect; don't inline *) - (InConstrEntrySomeLevel,!ntn'),(l,ll) + (InConstrEntry,!ntn'),(l,ll) type intern_env = { ids: Names.Id.Set.t; @@ -1688,11 +1688,11 @@ let drop_notations_pattern looked_for genv = (* but not scopes in expl_pl *) let (argscs1,_) = find_remaining_scopes expl_pl pl g in DAst.make ?loc @@ RCPatCstr (g, List.map2 (in_pat_sc scopes) argscs1 expl_pl @ List.map (in_pat false scopes) pl, []) - | CPatNotation (_,(InConstrEntrySomeLevel,"- _"),([a],[]),[]) when is_non_zero_pat a -> + | CPatNotation (_,(InConstrEntry,"- _"),([a],[]),[]) when is_non_zero_pat a -> let p = match a.CAst.v with CPatPrim (Numeral (_, p)) -> p | _ -> assert false in let pat, _df = Notation.interp_prim_token_cases_pattern_expr ?loc (ensure_kind false loc) (Numeral (SMinus,p)) scopes in rcp_of_glob scopes pat - | CPatNotation (_,(InConstrEntrySomeLevel,"( _ )"),([a],[]),[]) -> + | CPatNotation (_,(InConstrEntry,"( _ )"),([a],[]),[]) -> in_pat top scopes a | CPatNotation (_,ntn,fullargs,extrargs) -> let ntn,(terms,termlists) = contract_curly_brackets_pat ntn fullargs in @@ -2006,10 +2006,10 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c = DAst.make ?loc @@ GLetIn (na.CAst.v, inc1, int, intern_restart_binders (push_name_env ntnvars (impls_term_list 1 inc1) env na) c2) - | CNotation (_,(InConstrEntrySomeLevel,"- _"), ([a],[],[],[])) when is_non_zero a -> + | CNotation (_,(InConstrEntry,"- _"), ([a],[],[],[])) when is_non_zero a -> let p = match a.CAst.v with CPrim (Numeral (_, p)) -> p | _ -> assert false in intern env (CAst.make ?loc @@ CPrim (Numeral (SMinus,p))) - | CNotation (_,(InConstrEntrySomeLevel,"( _ )"),([a],[],[],[])) -> intern env a + | CNotation (_,(InConstrEntry,"( _ )"),([a],[],[],[])) -> intern env a | CNotation (_,ntn,args) -> let c = intern_notation intern env ntnvars loc ntn args in let x, impl, scopes = find_appl_head_data c in diff --git a/interp/dumpglob.ml b/interp/dumpglob.ml index 57ec708b07..d57c05788d 100644 --- a/interp/dumpglob.ml +++ b/interp/dumpglob.ml @@ -207,7 +207,7 @@ let cook_notation (from,df) sc = done; let df = Bytes.sub_string ntn 0 !j in let df_sc = match sc with Some sc -> ":" ^ sc ^ ":" ^ df | _ -> "::" ^ df in - let from_df_sc = match from with Constrexpr.InCustomEntryLevel (from,_) -> ":" ^ from ^ df_sc | Constrexpr.InConstrEntrySomeLevel -> ":" ^ df_sc in + let from_df_sc = match from with Constrexpr.InCustomEntry from -> ":" ^ from ^ df_sc | Constrexpr.InConstrEntry -> ":" ^ df_sc in from_df_sc let dump_notation_location posl df (((path,secpath),_),sc) = diff --git a/interp/impargs.ml b/interp/impargs.ml index a1b029c381..c6405b40fc 100644 --- a/interp/impargs.ml +++ b/interp/impargs.ml @@ -229,7 +229,7 @@ let add_free_rels_until strict strongly_strict revpat bound env sigma m pos acc let rec is_rigid_head sigma t = match kind sigma t with | Rel _ | Evar _ -> false | Ind _ | Const _ | Var _ | Sort _ -> true - | Case (_,_,f,_) -> is_rigid_head sigma f + | Case (_,_,_,f,_) -> is_rigid_head sigma f | Proj (p,c) -> true | App (f,args) -> (match kind sigma f with diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml index 3d29da025e..4016a3600e 100644 --- a/interp/implicit_quantifiers.ml +++ b/interp/implicit_quantifiers.ml @@ -92,7 +92,7 @@ let free_vars_of_constr_expr c ?(bound=Id.Set.empty) l = let rec aux bdvars l c = match CAst.(c.v) with | CRef (qid,_) when qualid_is_ident qid -> found c.CAst.loc (qualid_basename qid) bdvars l - | CNotation (_,(InConstrEntrySomeLevel,"{ _ : _ | _ }"), ({ CAst.v = CRef (qid,_) } :: _, [], [], [])) when + | CNotation (_,(InConstrEntry,"{ _ : _ | _ }"), ({ CAst.v = CRef (qid,_) } :: _, [], [], [])) when qualid_is_ident qid && not (Id.Set.mem (qualid_basename qid) bdvars) -> Constrexpr_ops.fold_constr_expr_with_binders (fun a l -> Id.Set.add a l) aux (Id.Set.add (qualid_basename qid) bdvars) l c | _ -> Constrexpr_ops.fold_constr_expr_with_binders (fun a l -> Id.Set.add a l) aux bdvars l c diff --git a/interp/notation.ml b/interp/notation.ml index d4a44d9622..e282d62396 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -56,9 +56,9 @@ let notation_with_optional_scope_eq inscope1 inscope2 = match (inscope1,inscope2 | (LastLonelyNotation | NotationInScope _), _ -> false let notation_eq (from1,ntn1) (from2,ntn2) = - notation_entry_level_eq from1 from2 && String.equal ntn1 ntn2 + notation_entry_eq from1 from2 && String.equal ntn1 ntn2 -let pr_notation (from,ntn) = qstring ntn ++ match from with InConstrEntrySomeLevel -> mt () | InCustomEntryLevel (s,n) -> str " in custom " ++ str s +let pr_notation (from,ntn) = qstring ntn ++ match from with InConstrEntry -> mt () | InCustomEntry s -> str " in custom " ++ str s module NotationOrd = struct @@ -337,6 +337,33 @@ let notation_constr_key = function (* Rem: NApp(NRef ref,[]) stands for @ref *) | NApp (_,args) -> Oth, Some (List.length args) | _ -> Oth, None +(** Dealing with precedences *) + +type level = notation_entry * entry_level * entry_relative_level list + (* first argument is InCustomEntry s for custom entries *) + +let entry_relative_level_eq t1 t2 = match t1, t2 with +| LevelLt n1, LevelLt n2 -> Int.equal n1 n2 +| LevelLe n1, LevelLe n2 -> Int.equal n1 n2 +| LevelSome, LevelSome -> true +| (LevelLt _ | LevelLe _ | LevelSome), _ -> false + +let level_eq (s1, l1, t1) (s2, l2, t2) = + notation_entry_eq s1 s2 && Int.equal l1 l2 && List.equal entry_relative_level_eq t1 t2 + +let notation_level_map = Summary.ref ~name:"notation_level_map" NotationMap.empty + +let declare_notation_level ntn level = + try + let _ = NotationMap.find ntn !notation_level_map in + anomaly (str "Notation " ++ pr_notation ntn ++ str " is already assigned a level.") + with Not_found -> + notation_level_map := NotationMap.add ntn level !notation_level_map + +let level_of_notation ntn = + NotationMap.find ntn !notation_level_map + + (**********************************************************************) (* Interpreting numbers (not in summary because functional objects) *) @@ -1228,8 +1255,8 @@ let find_notation ntn sc = NotationMap.find ntn (find_scope sc).notations let notation_of_prim_token = function - | Constrexpr.Numeral (SPlus,n) -> InConstrEntrySomeLevel, NumTok.Unsigned.sprint n - | Constrexpr.Numeral (SMinus,n) -> InConstrEntrySomeLevel, "- "^NumTok.Unsigned.sprint n + | Constrexpr.Numeral (SPlus,n) -> InConstrEntry, NumTok.Unsigned.sprint n + | Constrexpr.Numeral (SMinus,n) -> InConstrEntry, "- "^NumTok.Unsigned.sprint n | String _ -> raise Not_found let find_prim_token check_allowed ?loc p sc = @@ -1256,7 +1283,7 @@ let find_prim_token check_allowed ?loc p sc = let interp_prim_token_gen ?loc g p local_scopes = let scopes = make_current_scopes local_scopes in - let p_as_ntn = try notation_of_prim_token p with Not_found -> InConstrEntrySomeLevel,"" in + let p_as_ntn = try notation_of_prim_token p with Not_found -> InConstrEntry,"" in try let (pat,loc), sc = find_interpretation p_as_ntn (find_prim_token ?loc g p) scopes in pat, (loc,sc) @@ -1336,7 +1363,8 @@ module EntryCoercionOrd = module EntryCoercionMap = Map.Make(EntryCoercionOrd) -let entry_coercion_map = ref EntryCoercionMap.empty +let entry_coercion_map : (((entry_level option * entry_level option) * entry_coercion) list EntryCoercionMap.t) ref = + ref EntryCoercionMap.empty let level_ord lev lev' = match lev, lev' with @@ -1349,13 +1377,18 @@ let rec search nfrom nto = function | ((pfrom,pto),coe)::l -> if level_ord pfrom nfrom && level_ord nto pto then coe else search nfrom nto l -let decompose_custom_entry = function +let make_notation_entry_level entry level = + match entry with + | InConstrEntry -> InConstrEntrySomeLevel + | InCustomEntry s -> InCustomEntryLevel (s,level) + +let decompose_notation_entry_level = function | InConstrEntrySomeLevel -> InConstrEntry, None | InCustomEntryLevel (s,n) -> InCustomEntry s, Some n let availability_of_entry_coercion entry entry' = - let entry, lev = decompose_custom_entry entry in - let entry', lev' = decompose_custom_entry entry' in + let entry, lev = decompose_notation_entry_level entry in + let entry', lev' = decompose_notation_entry_level entry' in if notation_entry_eq entry entry' && level_ord lev' lev then Some [] else try Some (search lev lev' (EntryCoercionMap.find (entry,entry') !entry_coercion_map)) @@ -1377,28 +1410,27 @@ let rec insert_coercion_path path = function else if shorter_path path path' then path::allpaths else path'::insert_coercion_path path paths -let declare_entry_coercion (scope,(entry,_) as specific_ntn) entry' = - let entry, lev = decompose_custom_entry entry in - let entry', lev' = decompose_custom_entry entry' in +let declare_entry_coercion (scope,(entry,key)) lev entry' = + let entry', lev' = decompose_notation_entry_level entry' in (* Transitive closure *) let toaddleft = EntryCoercionMap.fold (fun (entry'',entry''') paths l -> List.fold_right (fun ((lev'',lev'''),path) l -> if notation_entry_eq entry entry''' && level_ord lev lev''' && not (notation_entry_eq entry' entry'') - then ((entry'',entry'),((lev'',lev'),path@[specific_ntn]))::l else l) paths l) + then ((entry'',entry'),((lev'',lev'),path@[(scope,(entry,key))]))::l else l) paths l) !entry_coercion_map [] in let toaddright = EntryCoercionMap.fold (fun (entry'',entry''') paths l -> List.fold_right (fun ((lev'',lev'''),path) l -> if entry' = entry'' && level_ord lev' lev'' && entry <> entry''' - then ((entry,entry'''),((lev,lev'''),path@[specific_ntn]))::l else l) paths l) + then ((entry,entry'''),((lev,lev'''),path@[(scope,(entry,key))]))::l else l) paths l) !entry_coercion_map [] in entry_coercion_map := List.fold_right (fun (pair,path) -> let olds = try EntryCoercionMap.find pair !entry_coercion_map with Not_found -> [] in EntryCoercionMap.add pair (insert_coercion_path path olds)) - (((entry,entry'),((lev,lev'),[specific_ntn]))::toaddright@toaddleft) + (((entry,entry'),((lev,lev'),[(scope,(entry,key))]))::toaddright@toaddleft) !entry_coercion_map let entry_has_global_map = ref String.Map.empty diff --git a/interp/notation.mli b/interp/notation.mli index e7e917463b..c39bfa6e28 100644 --- a/interp/notation.mli +++ b/interp/notation.mli @@ -298,8 +298,8 @@ type symbol = val symbol_eq : symbol -> symbol -> bool (** Make/decompose a notation of the form "_ U _" *) -val make_notation_key : notation_entry_level -> symbol list -> notation -val decompose_notation_key : notation -> notation_entry_level * symbol list +val make_notation_key : notation_entry -> symbol list -> notation +val decompose_notation_key : notation -> notation_entry * symbol list (** Decompose a notation of the form "a 'U' b" *) val decompose_raw_notation : string -> symbol list @@ -313,8 +313,10 @@ val locate_notation : (glob_constr -> Pp.t) -> notation_key -> val pr_visibility: (glob_constr -> Pp.t) -> scope_name option -> Pp.t +val make_notation_entry_level : notation_entry -> entry_level -> notation_entry_level + type entry_coercion = (notation_with_optional_scope * notation) list -val declare_entry_coercion : specific_notation -> notation_entry_level -> unit +val declare_entry_coercion : specific_notation -> entry_level option -> notation_entry_level -> unit val availability_of_entry_coercion : notation_entry_level -> notation_entry_level -> entry_coercion option val declare_custom_entry_has_global : string -> int -> unit @@ -323,6 +325,20 @@ val declare_custom_entry_has_ident : string -> int -> unit val entry_has_global : notation_entry_level -> bool val entry_has_ident : notation_entry_level -> bool +(** Dealing with precedences *) + +type level = notation_entry * entry_level * entry_relative_level list + (* first argument is InCustomEntry s for custom entries *) + +val level_eq : level -> level -> bool +val entry_relative_level_eq : entry_relative_level -> entry_relative_level -> bool + +(** {6 Declare and test the level of a (possibly uninterpreted) notation } *) + +val declare_notation_level : notation -> level -> unit +val level_of_notation : notation -> level + (** raise [Not_found] if not declared *) + (** Rem: printing rules for primitive token are canonical *) val with_notation_protection : ('a -> 'b) -> 'a -> 'b diff --git a/kernel/cClosure.ml b/kernel/cClosure.ml index de02882370..9640efd8eb 100644 --- a/kernel/cClosure.ml +++ b/kernel/cClosure.ml @@ -343,6 +343,7 @@ and fterm = | FFix of fixpoint * fconstr subs | FCoFix of cofixpoint * fconstr subs | FCaseT of case_info * constr * fconstr * constr array * fconstr subs (* predicate and branches are closures *) + | FCaseInvert of case_info * constr * finvert * fconstr * constr array * fconstr subs | FLambda of int * (Name.t Context.binder_annot * constr) list * constr * fconstr subs | FProd of Name.t Context.binder_annot * fconstr * constr * fconstr subs | FLetIn of Name.t Context.binder_annot * fconstr * fconstr * constr * fconstr subs @@ -353,6 +354,8 @@ and fterm = | FCLOS of constr * fconstr subs | FLOCKED +and finvert = Univ.Instance.t * fconstr array + let fterm_of v = v.term let set_norm v = v.mark <- Mark.set_norm v.mark let is_val v = match Mark.red_state v.mark with Norm -> true | Cstr | Whnf | Red -> false @@ -375,16 +378,30 @@ type infos_cache = { i_env : env; i_sigma : existential -> constr option; i_share : bool; + i_univs : UGraph.t; } type clos_infos = { i_flags : reds; + i_relevances : Sorts.relevance Range.t; i_cache : infos_cache } type clos_tab = (fconstr, Empty.t) constant_def KeyTable.t let info_flags info = info.i_flags let info_env info = info.i_cache.i_env +let info_univs info = info.i_cache.i_univs + +let push_relevance infos r = + { infos with i_relevances = Range.cons r.Context.binder_relevance infos.i_relevances } + +let push_relevances infos nas = + { infos with i_relevances = Array.fold_left (fun l x -> Range.cons x.Context.binder_relevance l) + infos.i_relevances nas } + +let set_info_relevances info r = { info with i_relevances = r } + +let info_relevances info = info.i_relevances (**********************************************************************) (* The type of (machine) stacks (= lambda-bar-calculus' contexts) *) @@ -438,7 +455,7 @@ let rec lft_fconstr n ft = {mark=mark Cstr r; term=FCoFix(cfx,subs_shft(n,e))} | FLIFT(k,m) -> lft_fconstr (n+k) m | FLOCKED -> assert false - | FFlex (RelKey _) | FAtom _ | FApp _ | FProj _ | FCaseT _ | FProd _ + | FFlex (RelKey _) | FAtom _ | FApp _ | FProj _ | FCaseT _ | FCaseInvert _ | FProd _ | FLetIn _ | FEvar _ | FCLOS _ -> {mark=ft.mark; term=FLIFT(n,ft)} let lift_fconstr k f = if Int.equal k 0 then f else lft_fconstr k f @@ -558,14 +575,10 @@ let rec to_constr lfts v = | FFlex (ConstKey op) -> mkConstU op | FInd op -> mkIndU op | FConstruct op -> mkConstructU op - | FCaseT (ci,p,c,ve,env) -> - if is_subs_id env && is_lift_id lfts then - mkCase (ci, p, to_constr lfts c, ve) - else - let subs = comp_subs lfts env in - mkCase (ci, subst_constr subs p, - to_constr lfts c, - Array.map (fun b -> subst_constr subs b) ve) + | FCaseT (ci,p,c,ve,env) -> to_constr_case lfts ci p NoInvert c ve env + | FCaseInvert (ci,p,(univs,args),c,ve,env) -> + let iv = CaseInvert {univs;args=Array.map (to_constr lfts) args} in + to_constr_case lfts ci p iv c ve env | FFix ((op,(lna,tys,bds)) as fx, e) -> if is_subs_id e && is_lift_id lfts then mkFix fx @@ -628,6 +641,15 @@ let rec to_constr lfts v = subst_constr subs t | FLOCKED -> assert false (*mkVar(Id.of_string"_LOCK_")*) +and to_constr_case lfts ci p iv c ve env = + if is_subs_id env && is_lift_id lfts then + mkCase (ci, p, iv, to_constr lfts c, ve) + else + let subs = comp_subs lfts env in + mkCase (ci, subst_constr subs p, iv, + to_constr lfts c, + Array.map (fun b -> subst_constr subs b) ve) + and subst_constr subst c = match [@ocaml.warning "-4"] Constr.kind c with | Rel i -> begin match expand_rel i subst with @@ -931,7 +953,7 @@ let rec knh info m stk = | Some s -> knh info c (s :: zupdate info m stk)) (* cases where knh stops *) - | (FFlex _|FLetIn _|FConstruct _|FEvar _| + | (FFlex _|FLetIn _|FConstruct _|FEvar _|FCaseInvert _| FCoFix _|FLambda _|FRel _|FAtom _|FInd _|FProd _|FInt _|FFloat _) -> (m, stk) @@ -940,8 +962,11 @@ and knht info e t stk = match kind t with | App(a,b) -> knht info e a (append_stack (mk_clos_vect e b) stk) - | Case(ci,p,t,br) -> + | Case(ci,p,NoInvert,t,br) -> knht info e t (ZcaseT(ci, p, br, e)::stk) + | Case(ci,p,CaseInvert{univs;args},t,br) -> + let term = FCaseInvert (ci, p, (univs,Array.map (mk_clos e) args), mk_clos e t, br, e) in + { mark = mark Red Unknown; term }, stk | Fix fx -> knh info { mark = mark Cstr Unknown; term = FFix (fx, e) } stk | Cast(a,_,_) -> knht info e a stk | Rel n -> knh info (clos_rel e n) stk @@ -1250,6 +1275,10 @@ module FredNative = RedNative(FNativeEntries) (************************************************************************) +let conv : (clos_infos -> clos_tab -> fconstr -> fconstr -> bool) ref + = ref (fun _ _ _ _ -> (assert false : bool)) +let set_conv f = conv := f + (* Computes a weak head normal form from the result of knh. *) let rec knr info tab m stk = match m.term with @@ -1325,8 +1354,13 @@ let rec knr info tab m stk = kni info tab a (Zprimitive(op,c,rargs,nargs)::s) end | (_, _, s) -> (m, s)) + | FCaseInvert (ci,_p,iv,_c,v,env) when red_set info.i_flags fMATCH -> + begin match case_inversion info tab ci iv v with + | Some c -> knit info tab env c stk + | None -> (m, stk) + end | FLOCKED | FRel _ | FAtom _ | FFlex (RelKey _ | ConstKey _ | VarKey _) | FInd _ | FApp _ | FProj _ - | FFix _ | FCoFix _ | FCaseT _ | FLambda _ | FProd _ | FLetIn _ | FLIFT _ + | FFix _ | FCoFix _ | FCaseT _ | FCaseInvert _ | FLambda _ | FProd _ | FLetIn _ | FLIFT _ | FCLOS _ -> (m, stk) @@ -1338,6 +1372,28 @@ and knit info tab e t stk = let (ht,s) = knht info e t stk in knr info tab ht s +and case_inversion info tab ci (univs,args) v = + let open Declarations in + if Array.is_empty args then Some v.(0) + else + let env = info_env info in + let ind = ci.ci_ind in + let params, indices = Array.chop ci.ci_npar args in + let psubst = subs_cons (params, subs_id 0) in + let mib = Environ.lookup_mind (fst ind) env in + let mip = mib.mind_packets.(snd ind) in + (* indtyping enforces 1 ctor with no letins in the context *) + let _, expect = mip.mind_nf_lc.(0) in + let _ind, expect_args = destApp expect in + let check_index i index = + let expected = expect_args.(ci.ci_npar + i) in + let expected = Vars.subst_instance_constr univs expected in + let expected = mk_clos psubst expected in + !conv {info with i_flags=all} tab expected index + in + if Array.for_all_i check_index 0 indices + then Some v.(0) else None + let kh info tab v stk = fapp_stack(kni info tab v stk) (************************************************************************) @@ -1348,7 +1404,7 @@ let rec zip_term zfun m stk = | Zapp args :: s -> zip_term zfun (mkApp(m, Array.map zfun args)) s | ZcaseT(ci,p,br,e)::s -> - let t = mkCase(ci, zfun (mk_clos e p), m, + let t = mkCase(ci, zfun (mk_clos e p), NoInvert, m, Array.map (fun b -> zfun (mk_clos e b)) br) in zip_term zfun t s | Zproj p::s -> @@ -1388,31 +1444,34 @@ and norm_head info tab m = | FLambda(_n,tys,f,e) -> let (e',info,rvtys) = List.fold_left (fun (e,info,ctxt) (na,ty) -> + let info = push_relevance info na in (subs_lift e, info, (na,kl info tab (mk_clos e ty))::ctxt)) (e,info,[]) tys in let bd = kl info tab (mk_clos e' f) in List.fold_left (fun b (na,ty) -> mkLambda(na,ty,b)) bd rvtys | FLetIn(na,a,b,f,e) -> let c = mk_clos (subs_lift e) f in - mkLetIn(na, kl info tab a, kl info tab b, kl info tab c) + mkLetIn(na, kl info tab a, kl info tab b, kl (push_relevance info na) tab c) | FProd(na,dom,rng,e) -> - mkProd(na, kl info tab dom, kl info tab (mk_clos (subs_lift e) rng)) + mkProd(na, kl info tab dom, kl (push_relevance info na) tab (mk_clos (subs_lift e) rng)) | FCoFix((n,(na,tys,bds)),e) -> let ftys = Array.Fun1.map mk_clos e tys in let fbds = Array.Fun1.map mk_clos (subs_liftn (Array.length na) e) bds in - mkCoFix(n,(na, CArray.map (kl info tab) ftys, CArray.map (kl info tab) fbds)) + let infobd = push_relevances info na in + mkCoFix(n,(na, CArray.map (kl info tab) ftys, CArray.map (kl infobd tab) fbds)) | FFix((n,(na,tys,bds)),e) -> let ftys = Array.Fun1.map mk_clos e tys in let fbds = Array.Fun1.map mk_clos (subs_liftn (Array.length na) e) bds in - mkFix(n,(na, CArray.map (kl info tab) ftys, CArray.map (kl info tab) fbds)) + let infobd = push_relevances info na in + mkFix(n,(na, CArray.map (kl info tab) ftys, CArray.map (kl infobd tab) fbds)) | FEvar((i,args),env) -> mkEvar(i, List.map (fun a -> kl info tab (mk_clos env a)) args) | FProj (p,c) -> mkProj (p, kl info tab c) | FLOCKED | FRel _ | FAtom _ | FFlex _ | FInd _ | FConstruct _ - | FApp _ | FCaseT _ | FLIFT _ | FCLOS _ | FInt _ | FFloat _ -> term_of_fconstr m + | FApp _ | FCaseT _ | FCaseInvert _ | FLIFT _ | FCLOS _ | FInt _ | FFloat _ -> term_of_fconstr m (* Initialization and then normalization *) @@ -1434,14 +1493,16 @@ let whd_stack infos tab m stk = match Mark.red_state m.mark with let () = if infos.i_cache.i_share then ignore (fapp_stack k) in (* to unlock Zupdates! *) k -let create_clos_infos ?(evars=fun _ -> None) flgs env = +let create_clos_infos ?univs ?(evars=fun _ -> None) flgs env = + let univs = Option.default (universes env) univs in let share = (Environ.typing_flags env).Declarations.share_reduction in let cache = { i_env = env; i_sigma = evars; i_share = share; + i_univs = univs; } in - { i_flags = flgs; i_cache = cache } + { i_flags = flgs; i_relevances = Range.empty; i_cache = cache } let create_tab () = KeyTable.create 17 diff --git a/kernel/cClosure.mli b/kernel/cClosure.mli index 79092813bc..c1e5f12df7 100644 --- a/kernel/cClosure.mli +++ b/kernel/cClosure.mli @@ -95,10 +95,11 @@ module KeyTable : Hashtbl.S with type key = table_key (** [fconstr] is the type of frozen constr *) type fconstr - (** [fconstr] can be accessed by using the function [fterm_of] and by matching on type [fterm] *) +type finvert + type fterm = | FRel of int | FAtom of constr (** Metas and Sorts *) @@ -110,6 +111,7 @@ type fterm = | FFix of fixpoint * fconstr subs | FCoFix of cofixpoint * fconstr subs | FCaseT of case_info * constr * fconstr * constr array * fconstr subs (* predicate and branches are closures *) + | FCaseInvert of case_info * constr * finvert * fconstr * constr array * fconstr subs | FLambda of int * (Name.t Context.binder_annot * constr) list * constr * fconstr subs | FProd of Name.t Context.binder_annot * fconstr * constr * fconstr subs | FLetIn of Name.t Context.binder_annot * fconstr * fconstr * constr * fconstr subs @@ -173,15 +175,22 @@ val set_relevance : Sorts.relevance -> fconstr -> unit type clos_infos type clos_tab val create_clos_infos : - ?evars:(existential->constr option) -> reds -> env -> clos_infos + ?univs:UGraph.t -> ?evars:(existential->constr option) -> reds -> env -> clos_infos val oracle_of_infos : clos_infos -> Conv_oracle.oracle val create_tab : unit -> clos_tab val info_env : clos_infos -> env val info_flags: clos_infos -> reds +val info_univs : clos_infos -> UGraph.t val unfold_projection : clos_infos -> Projection.t -> stack_member option +val push_relevance : clos_infos -> 'b Context.binder_annot -> clos_infos +val push_relevances : clos_infos -> 'b Context.binder_annot array -> clos_infos +val set_info_relevances : clos_infos -> Sorts.relevance Range.t -> clos_infos + +val info_relevances : clos_infos -> Sorts.relevance Range.t + val infos_with_reds : clos_infos -> reds -> clos_infos (** Reduction function *) @@ -214,6 +223,9 @@ val eta_expand_ind_stack : env -> inductive -> fconstr -> stack -> (** [unfold_reference] unfolds references in a [fconstr] *) val unfold_reference : clos_infos -> clos_tab -> table_key -> (fconstr, Util.Empty.t) constant_def +(** Hook for Reduction *) +val set_conv : (clos_infos -> clos_tab -> fconstr -> fconstr -> bool) -> unit + (*********************************************************************** i This is for lazy debug *) diff --git a/kernel/clambda.ml b/kernel/clambda.ml index 65de52c0f6..0d77cae077 100644 --- a/kernel/clambda.ml +++ b/kernel/clambda.ml @@ -710,7 +710,7 @@ let rec lambda_of_constr env c = | Construct _ -> lambda_of_app env c empty_args - | Case(ci,t,a,branches) -> + | Case(ci,t,_iv,a,branches) -> (* XXX handle iv *) let ind = ci.ci_ind in let mib = lookup_mind (fst ind) env.global_env in let oib = mib.mind_packets.(snd ind) in diff --git a/kernel/constr.ml b/kernel/constr.ml index 703e3616a0..d0598bdad1 100644 --- a/kernel/constr.ml +++ b/kernel/constr.ml @@ -83,6 +83,10 @@ type pconstant = Constant.t puniverses type pinductive = inductive puniverses type pconstructor = constructor puniverses +type ('constr, 'univs) case_invert = + | NoInvert + | CaseInvert of { univs : 'univs; args : 'constr array } + (* [Var] is used for named variables and [Rel] for variables as de Bruijn indices. *) type ('constr, 'types, 'sort, 'univs) kind_of_term = @@ -99,7 +103,7 @@ type ('constr, 'types, 'sort, 'univs) kind_of_term = | Const of (Constant.t * 'univs) | Ind of (inductive * 'univs) | Construct of (constructor * 'univs) - | Case of case_info * 'constr * 'constr * 'constr array + | Case of case_info * 'constr * ('constr, 'univs) case_invert * 'constr * 'constr array | Fix of ('constr, 'types) pfixpoint | CoFix of ('constr, 'types) pcofixpoint | Proj of Projection.t * 'constr @@ -189,7 +193,7 @@ let mkConstructU c = Construct c let mkConstructUi ((ind,u),i) = Construct ((ind,i),u) (* Constructs the term <p>Case c of c1 | c2 .. | cn end *) -let mkCase (ci, p, c, ac) = Case (ci, p, c, ac) +let mkCase (ci, p, iv, c, ac) = Case (ci, p, iv, c, ac) (* If recindxs = [|i1,...in|] funnames = [|f1,...fn|] @@ -417,7 +421,7 @@ let destConstruct c = match kind c with (* Destructs a term <p>Case c of lc1 | lc2 .. | lcn end *) let destCase c = match kind c with - | Case (ci,p,c,v) -> (ci,p,c,v) + | Case (ci,p,iv,c,v) -> (ci,p,iv,c,v) | _ -> raise DestKO let destProj c = match kind c with @@ -461,6 +465,11 @@ let decompose_appvect c = starting from [acc] and proceeding from left to right according to the usual representation of the constructions; it is not recursive *) +let fold_invert f acc = function + | NoInvert -> acc + | CaseInvert {univs=_;args} -> + Array.fold_left f acc args + let fold f acc c = match kind c with | (Rel _ | Meta _ | Var _ | Sort _ | Const _ | Ind _ | Construct _ | Int _ | Float _) -> acc @@ -471,7 +480,7 @@ let fold f acc c = match kind c with | App (c,l) -> Array.fold_left f (f acc c) l | Proj (_p,c) -> f acc c | Evar (_,l) -> List.fold_left f acc l - | Case (_,p,c,bl) -> Array.fold_left f (f (f acc p) c) bl + | Case (_,p,iv,c,bl) -> Array.fold_left f (f (fold_invert f (f acc p) iv) c) bl | Fix (_,(_lna,tl,bl)) -> Array.fold_left2 (fun acc t b -> f (f acc t) b) acc tl bl | CoFix (_,(_lna,tl,bl)) -> @@ -481,6 +490,11 @@ let fold f acc c = match kind c with not recursive and the order with which subterms are processed is not specified *) +let iter_invert f = function + | NoInvert -> () + | CaseInvert {univs=_; args;} -> + Array.iter f args + let iter f c = match kind c with | (Rel _ | Meta _ | Var _ | Sort _ | Const _ | Ind _ | Construct _ | Int _ | Float _) -> () @@ -491,7 +505,7 @@ let iter f c = match kind c with | App (c,l) -> f c; Array.iter f l | Proj (_p,c) -> f c | Evar (_,l) -> List.iter f l - | Case (_,p,c,bl) -> f p; f c; Array.iter f bl + | Case (_,p,iv,c,bl) -> f p; iter_invert f iv; f c; Array.iter f bl | Fix (_,(_,tl,bl)) -> Array.iter f tl; Array.iter f bl | CoFix (_,(_,tl,bl)) -> Array.iter f tl; Array.iter f bl @@ -510,7 +524,7 @@ let iter_with_binders g f n c = match kind c with | LetIn (_,b,t,c) -> f n b; f n t; f (g n) c | App (c,l) -> f n c; Array.Fun1.iter f n l | Evar (_,l) -> List.iter (fun c -> f n c) l - | Case (_,p,c,bl) -> f n p; f n c; Array.Fun1.iter f n bl + | Case (_,p,iv,c,bl) -> f n p; iter_invert (f n) iv; f n c; Array.Fun1.iter f n bl | Proj (_p,c) -> f n c | Fix (_,(_,tl,bl)) -> Array.Fun1.iter f n tl; @@ -537,7 +551,7 @@ let fold_constr_with_binders g f n acc c = | App (c,l) -> Array.fold_left (f n) (f n acc c) l | Proj (_p,c) -> f n acc c | Evar (_,l) -> List.fold_left (f n) acc l - | Case (_,p,c,bl) -> Array.fold_left (f n) (f n (f n acc p) c) bl + | Case (_,p,iv,c,bl) -> Array.fold_left (f n) (f n (fold_invert (f n) (f n acc p) iv) c) bl | Fix (_,(_,tl,bl)) -> let n' = iterate g (Array.length tl) n in let fd = Array.map2 (fun t b -> (t,b)) tl bl in @@ -623,6 +637,13 @@ let map_branches_with_full_binders g f l ci bl = let map_return_predicate_with_full_binders g f l ci p = map_under_context_with_full_binders g f l (List.length ci.ci_pp_info.ind_tags) p +let map_invert f = function + | NoInvert -> NoInvert + | CaseInvert {univs;args;} as orig -> + let args' = Array.Smart.map f args in + if args == args' then orig + else CaseInvert {univs;args=args';} + let map_gen userview f c = match kind c with | (Rel _ | Meta _ | Var _ | Sort _ | Const _ | Ind _ | Construct _ | Int _ | Float _) -> c @@ -660,18 +681,20 @@ let map_gen userview f c = match kind c with let l' = List.Smart.map f l in if l'==l then c else mkEvar (e, l') - | Case (ci,p,b,bl) when userview -> + | Case (ci,p,iv,b,bl) when userview -> let b' = f b in + let iv' = map_invert f iv in let p' = map_return_predicate f ci p in let bl' = map_branches f ci bl in - if b'==b && p'==p && bl'==bl then c - else mkCase (ci, p', b', bl') - | Case (ci,p,b,bl) -> + if b'==b && iv'==iv && p'==p && bl'==bl then c + else mkCase (ci, p', iv', b', bl') + | Case (ci,p,iv,b,bl) -> let b' = f b in + let iv' = map_invert f iv in let p' = f p in let bl' = Array.Smart.map f bl in - if b'==b && p'==p && bl'==bl then c - else mkCase (ci, p', b', bl') + if b'==b && iv'==iv && p'==p && bl'==bl then c + else mkCase (ci, p', iv', b', bl') | Fix (ln,(lna,tl,bl)) -> let tl' = Array.Smart.map f tl in let bl' = Array.Smart.map f bl in @@ -688,6 +711,13 @@ let map = map_gen false (* Like {!map} but with an accumulator. *) +let fold_map_invert f acc = function + | NoInvert -> acc, NoInvert + | CaseInvert {univs;args;} as orig -> + let acc, args' = Array.fold_left_map f acc args in + if args==args' then acc, orig + else acc, CaseInvert {univs;args=args';} + let fold_map f accu c = match kind c with | (Rel _ | Meta _ | Var _ | Sort _ | Const _ | Ind _ | Construct _ | Int _ | Float _) -> accu, c @@ -726,12 +756,13 @@ let fold_map f accu c = match kind c with let accu, l' = List.fold_left_map f accu l in if l'==l then accu, c else accu, mkEvar (e, l') - | Case (ci,p,b,bl) -> + | Case (ci,p,iv,b,bl) -> let accu, b' = f accu b in + let accu, iv' = fold_map_invert f accu iv in let accu, p' = f accu p in let accu, bl' = Array.Smart.fold_left_map f accu bl in - if b'==b && p'==p && bl'==bl then accu, c - else accu, mkCase (ci, p', b', bl') + if b'==b && iv'==iv && p'==p && bl'==bl then accu, c + else accu, mkCase (ci, p', iv', b', bl') | Fix (ln,(lna,tl,bl)) -> let accu, tl' = Array.Smart.fold_left_map f accu tl in let accu, bl' = Array.Smart.fold_left_map f accu bl in @@ -786,12 +817,13 @@ let map_with_binders g f l c0 = match kind c0 with let al' = List.Smart.map (fun c -> f l c) al in if al' == al then c0 else mkEvar (e, al') - | Case (ci, p, c, bl) -> + | Case (ci, p, iv, c, bl) -> let p' = f l p in + let iv' = map_invert (f l) iv in let c' = f l c in let bl' = Array.Fun1.Smart.map f l bl in - if p' == p && c' == c && bl' == bl then c0 - else mkCase (ci, p', c', bl') + if p' == p && iv' == iv && c' == c && bl' == bl then c0 + else mkCase (ci, p', iv', c', bl') | Fix (ln, (lna, tl, bl)) -> let tl' = Array.Fun1.Smart.map f l tl in let l' = iterate g (Array.length tl) l in @@ -836,7 +868,7 @@ let fold_with_full_binders g f n acc c = | App (c,l) -> Array.fold_left (f n) (f n acc c) l | Proj (_,c) -> f n acc c | Evar (_,l) -> List.fold_left (f n) acc l - | Case (_,p,c,bl) -> Array.fold_left (f n) (f n (f n acc p) c) bl + | Case (_,p,iv,c,bl) -> Array.fold_left (f n) (f n (fold_invert (f n) (f n acc p) iv) c) bl | Fix (_,(lna,tl,bl)) -> let n' = CArray.fold_left2_i (fun i c n t -> g (LocalAssum (n,lift i t)) c) n lna tl in let fd = Array.map2 (fun t b -> (t,b)) tl bl in @@ -847,7 +879,7 @@ let fold_with_full_binders g f n acc c = Array.fold_left (fun acc (t,b) -> f n' (f n acc t) b) acc fd -type 'univs instance_compare_fn = GlobRef.t -> int -> +type 'univs instance_compare_fn = (GlobRef.t * int) option -> 'univs -> 'univs -> bool type 'constr constr_compare_fn = int -> 'constr -> 'constr -> bool @@ -863,6 +895,14 @@ type 'constr constr_compare_fn = int -> 'constr -> 'constr -> bool optimisation that physically equal arrays are equals (hence the calls to {!Array.equal_norefl}). *) +let eq_invert eq leq_universes iv1 iv2 = + match iv1, iv2 with + | NoInvert, NoInvert -> true + | NoInvert, CaseInvert _ | CaseInvert _, NoInvert -> false + | CaseInvert {univs;args}, CaseInvert iv2 -> + leq_universes univs iv2.univs + && Array.equal eq args iv2.args + let compare_head_gen_leq_with kind1 kind2 leq_universes leq_sorts eq leq nargs t1 t2 = match kind_nocast_gen kind1 t1, kind_nocast_gen kind2 t2 with | Cast _, _ | _, Cast _ -> assert false (* kind_nocast *) @@ -884,12 +924,12 @@ let compare_head_gen_leq_with kind1 kind2 leq_universes leq_sorts eq leq nargs t | Evar (e1,l1), Evar (e2,l2) -> Evar.equal e1 e2 && List.equal (eq 0) l1 l2 | Const (c1,u1), Const (c2,u2) -> (* The args length currently isn't used but may as well pass it. *) - Constant.equal c1 c2 && leq_universes (GlobRef.ConstRef c1) nargs u1 u2 - | Ind (c1,u1), Ind (c2,u2) -> eq_ind c1 c2 && leq_universes (GlobRef.IndRef c1) nargs u1 u2 + Constant.equal c1 c2 && leq_universes (Some (GlobRef.ConstRef c1, nargs)) u1 u2 + | Ind (c1,u1), Ind (c2,u2) -> eq_ind c1 c2 && leq_universes (Some (GlobRef.IndRef c1, nargs)) u1 u2 | Construct (c1,u1), Construct (c2,u2) -> - eq_constructor c1 c2 && leq_universes (GlobRef.ConstructRef c1) nargs u1 u2 - | Case (_,p1,c1,bl1), Case (_,p2,c2,bl2) -> - eq 0 p1 p2 && eq 0 c1 c2 && Array.equal (eq 0) bl1 bl2 + eq_constructor c1 c2 && leq_universes (Some (GlobRef.ConstructRef c1, nargs)) u1 u2 + | Case (_,p1,iv1,c1,bl1), Case (_,p2,iv2,c2,bl2) -> + eq 0 p1 p2 && eq_invert (eq 0) (leq_universes None) iv1 iv2 && eq 0 c1 c2 && Array.equal (eq 0) bl1 bl2 | Fix ((ln1, i1),(_,tl1,bl1)), Fix ((ln2, i2),(_,tl2,bl2)) -> Int.equal i1 i2 && Array.equal Int.equal ln1 ln2 && Array.equal_norefl (eq 0) tl1 tl2 && Array.equal_norefl (eq 0) bl1 bl2 @@ -923,7 +963,7 @@ let compare_head_gen_with kind1 kind2 eq_universes eq_sorts eq t1 t2 = let compare_head_gen eq_universes eq_sorts eq t1 t2 = compare_head_gen_leq eq_universes eq_sorts eq eq t1 t2 -let compare_head = compare_head_gen (fun _ _ -> Univ.Instance.equal) Sorts.equal +let compare_head = compare_head_gen (fun _ -> Univ.Instance.equal) Sorts.equal (*******************************) (* alpha conversion functions *) @@ -932,14 +972,14 @@ let compare_head = compare_head_gen (fun _ _ -> Univ.Instance.equal) Sorts.equal (* alpha conversion : ignore print names and casts *) let rec eq_constr nargs m n = - (m == n) || compare_head_gen (fun _ _ -> Instance.equal) Sorts.equal eq_constr nargs m n + (m == n) || compare_head_gen (fun _ -> Instance.equal) Sorts.equal eq_constr nargs m n let equal n m = eq_constr 0 m n (* to avoid tracing a recursive fun *) let eq_constr_univs univs m n = if m == n then true else - let eq_universes _ _ = UGraph.check_eq_instances univs in + let eq_universes _ = UGraph.check_eq_instances univs in let eq_sorts s1 s2 = s1 == s2 || UGraph.check_eq univs (Sorts.univ_of_sort s1) (Sorts.univ_of_sort s2) in let rec eq_constr' nargs m n = m == n || compare_head_gen eq_universes eq_sorts eq_constr' nargs m n @@ -948,7 +988,7 @@ let eq_constr_univs univs m n = let leq_constr_univs univs m n = if m == n then true else - let eq_universes _ _ = UGraph.check_eq_instances univs in + let eq_universes _ = UGraph.check_eq_instances univs in let eq_sorts s1 s2 = s1 == s2 || UGraph.check_eq univs (Sorts.univ_of_sort s1) (Sorts.univ_of_sort s2) in let leq_sorts s1 s2 = s1 == s2 || @@ -965,7 +1005,7 @@ let eq_constr_univs_infer univs m n = if m == n then true, Constraint.empty else let cstrs = ref Constraint.empty in - let eq_universes _ _ = UGraph.check_eq_instances univs in + let eq_universes _ = UGraph.check_eq_instances univs in let eq_sorts s1 s2 = if Sorts.equal s1 s2 then true else @@ -985,7 +1025,7 @@ let leq_constr_univs_infer univs m n = if m == n then true, Constraint.empty else let cstrs = ref Constraint.empty in - let eq_universes _ _ l l' = UGraph.check_eq_instances univs l l' in + let eq_universes _ l l' = UGraph.check_eq_instances univs l l' in let eq_sorts s1 s2 = if Sorts.equal s1 s2 then true else @@ -1015,7 +1055,16 @@ let leq_constr_univs_infer univs m n = res, !cstrs let rec eq_constr_nounivs m n = - (m == n) || compare_head_gen (fun _ _ _ _ -> true) (fun _ _ -> true) (fun _ -> eq_constr_nounivs) 0 m n + (m == n) || compare_head_gen (fun _ _ _ -> true) (fun _ _ -> true) (fun _ -> eq_constr_nounivs) 0 m n + +let compare_invert f iv1 iv2 = + match iv1, iv2 with + | NoInvert, NoInvert -> 0 + | NoInvert, CaseInvert _ -> -1 + | CaseInvert _, NoInvert -> 1 + | CaseInvert iv1, CaseInvert iv2 -> + (* univs ignored deliberately *) + Array.compare f iv1.args iv2.args let constr_ord_int f t1 t2 = let (=?) f g i1 i2 j1 j2= @@ -1060,8 +1109,12 @@ let constr_ord_int f t1 t2 = | Ind _, _ -> -1 | _, Ind _ -> 1 | Construct (ct1,_u1), Construct (ct2,_u2) -> constructor_ord ct1 ct2 | Construct _, _ -> -1 | _, Construct _ -> 1 - | Case (_,p1,c1,bl1), Case (_,p2,c2,bl2) -> - ((f =? f) ==? (Array.compare f)) p1 p2 c1 c2 bl1 bl2 + | Case (_,p1,iv1,c1,bl1), Case (_,p2,iv2,c2,bl2) -> + let c = f p1 p2 in + if Int.equal c 0 then let c = compare_invert f iv1 iv2 in + if Int.equal c 0 then let c = f c1 c2 in + if Int.equal c 0 then Array.compare f bl1 bl2 + else c else c else c | Case _, _ -> -1 | _, Case _ -> 1 | Fix (ln1,(_,tl1,bl1)), Fix (ln2,(_,tl2,bl2)) -> ((fix_cmp =? (Array.compare f)) ==? (Array.compare f)) @@ -1129,6 +1182,14 @@ let array_eqeq t1 t2 = (Int.equal i (Array.length t1)) || (t1.(i) == t2.(i) && aux (i + 1)) in aux 0) +let invert_eqeq iv1 iv2 = + match iv1, iv2 with + | NoInvert, NoInvert -> true + | NoInvert, CaseInvert _ | CaseInvert _, NoInvert -> false + | CaseInvert iv1, CaseInvert iv2 -> + iv1.univs == iv2.univs + && iv1.args == iv2.args + let hasheq t1 t2 = match t1, t2 with | Rel n1, Rel n2 -> n1 == n2 @@ -1146,8 +1207,8 @@ let hasheq t1 t2 = | Const (c1,u1), Const (c2,u2) -> c1 == c2 && u1 == u2 | Ind (ind1,u1), Ind (ind2,u2) -> ind1 == ind2 && u1 == u2 | Construct (cstr1,u1), Construct (cstr2,u2) -> cstr1 == cstr2 && u1 == u2 - | Case (ci1,p1,c1,bl1), Case (ci2,p2,c2,bl2) -> - ci1 == ci2 && p1 == p2 && c1 == c2 && array_eqeq bl1 bl2 + | Case (ci1,p1,iv1,c1,bl1), Case (ci2,p2,iv2,c2,bl2) -> + ci1 == ci2 && p1 == p2 && invert_eqeq iv1 iv2 && c1 == c2 && array_eqeq bl1 bl2 | Fix ((ln1, i1),(lna1,tl1,bl1)), Fix ((ln2, i2),(lna2,tl2,bl2)) -> Int.equal i1 i2 && Array.equal Int.equal ln1 ln2 @@ -1236,12 +1297,13 @@ let hashcons (sh_sort,sh_ci,sh_construct,sh_ind,sh_con,sh_na,sh_id) = let u', hu = sh_instance u in (Construct (sh_construct c, u'), combinesmall 11 (combine (constructor_syntactic_hash c) hu)) - | Case (ci,p,c,bl) -> + | Case (ci,p,iv,c,bl) -> let p, hp = sh_rec p + and iv, hiv = sh_invert iv and c, hc = sh_rec c in let bl,hbl = hash_term_array bl in - let hbl = combine (combine hc hp) hbl in - (Case (sh_ci ci, p, c, bl), combinesmall 12 hbl) + let hbl = combine4 hc hp hiv hbl in + (Case (sh_ci ci, p, iv, c, bl), combinesmall 12 hbl) | Fix (ln,(lna,tl,bl)) -> let bl,hbl = hash_term_array bl in let tl,htl = hash_term_array tl in @@ -1271,6 +1333,13 @@ let hashcons (sh_sort,sh_ci,sh_construct,sh_ind,sh_con,sh_na,sh_id) = (t, combinesmall 18 (combine h l)) | Float f -> (t, combinesmall 19 (Float64.hash f)) + and sh_invert = function + | NoInvert -> NoInvert, 0 + | CaseInvert {univs;args;} -> + let univs, hu = sh_instance univs in + let args, ha = hash_term_array args in + CaseInvert {univs;args;}, combinesmall 1 (combine hu ha) + and sh_rec t = let (y, h) = hash_term t in (* [h] must be positive. *) @@ -1332,8 +1401,8 @@ let rec hash t = combinesmall 10 (combine (ind_hash ind) (Instance.hash u)) | Construct (c,u) -> combinesmall 11 (combine (constructor_hash c) (Instance.hash u)) - | Case (_ , p, c, bl) -> - combinesmall 12 (combine3 (hash c) (hash p) (hash_term_array bl)) + | Case (_ , p, iv, c, bl) -> + combinesmall 12 (combine4 (hash c) (hash p) (hash_invert iv) (hash_term_array bl)) | Fix (_ln ,(_, tl, bl)) -> combinesmall 13 (combine (hash_term_array bl) (hash_term_array tl)) | CoFix(_ln, (_, tl, bl)) -> @@ -1345,6 +1414,11 @@ let rec hash t = | Int i -> combinesmall 18 (Uint63.hash i) | Float f -> combinesmall 19 (Float64.hash f) +and hash_invert = function + | NoInvert -> 0 + | CaseInvert {univs;args;} -> + combinesmall 1 (combine (Instance.hash univs) (hash_term_array args)) + and hash_term_array t = Array.fold_left (fun acc t -> combine acc (hash t)) 0 t @@ -1476,9 +1550,9 @@ let rec debug_print c = | Construct (((sp,i),j),u) -> str"Constr(" ++ pr_puniverses (MutInd.print sp ++ str"," ++ int i ++ str"," ++ int j) u ++ str")" | Proj (p,c) -> str"Proj(" ++ Constant.debug_print (Projection.constant p) ++ str"," ++ bool (Projection.unfolded p) ++ debug_print c ++ str")" - | Case (_ci,p,c,bl) -> v 0 + | Case (_ci,p,iv,c,bl) -> v 0 (hv 0 (str"<"++debug_print p++str">"++ cut() ++ str"Case " ++ - debug_print c ++ str"of") ++ cut() ++ + debug_print c ++ debug_invert iv ++ str"of") ++ cut() ++ prlist_with_sep (fun _ -> brk(1,2)) debug_print (Array.to_list bl) ++ cut() ++ str"end") | Fix f -> debug_print_fix debug_print f @@ -1492,3 +1566,9 @@ let rec debug_print c = str"}") | Int i -> str"Int("++str (Uint63.to_string i) ++ str")" | Float i -> str"Float("++str (Float64.to_string i) ++ str")" + +and debug_invert = let open Pp in function + | NoInvert -> mt() + | CaseInvert {univs;args;} -> + spc() ++ str"Invert {univs=" ++ Instance.pr Level.pr univs ++ + str "; args=" ++ prlist_with_sep spc debug_print (Array.to_list args) ++ str "} " diff --git a/kernel/constr.mli b/kernel/constr.mli index 00051d7551..0c151bb43c 100644 --- a/kernel/constr.mli +++ b/kernel/constr.mli @@ -49,6 +49,14 @@ type case_info = ci_pp_info : case_printing (* not interpreted by the kernel *) } +type ('constr, 'univs) case_invert = + | NoInvert + (** Normal reduction: match when the scrutinee is a constructor. *) + + | CaseInvert of { univs : 'univs; args : 'constr array; } + (** Reduce when the indices match those of the unique constructor. + (SProp to non SProp only) *) + (** {6 The type of constructions } *) type t @@ -148,7 +156,7 @@ val mkRef : GlobRef.t Univ.puniverses -> constr [ac]{^ ith} element is ith constructor case presented as {e lambda construct_args (without params). case_term } *) -val mkCase : case_info * constr * constr * constr array -> constr +val mkCase : case_info * constr * (constr,Univ.Instance.t) case_invert * constr * constr array -> constr (** If [recindxs = [|i1,...in|]] [funnames = [|f1,.....fn|]] @@ -232,7 +240,7 @@ type ('constr, 'types, 'sort, 'univs) kind_of_term = | Ind of (inductive * 'univs) (** A name of an inductive type defined by [Variant], [Inductive] or [Record] Vernacular-commands. *) | Construct of (constructor * 'univs) (** A constructor of an inductive type defined by [Variant], [Inductive] or [Record] Vernacular-commands. *) - | Case of case_info * 'constr * 'constr * 'constr array + | Case of case_info * 'constr * ('constr,'univs) case_invert * 'constr * 'constr array | Fix of ('constr, 'types) pfixpoint | CoFix of ('constr, 'types) pcofixpoint | Proj of Projection.t * 'constr @@ -339,7 +347,7 @@ Ci(...yij...) => ti | ... end] (or [let (..y1i..) := c as x in I args return P in t1], or [if c then t1 else t2]) @return [(info,c,fun args x => P,[|...|fun yij => ti| ...|])] where [info] is pretty-printing information *) -val destCase : constr -> case_info * constr * constr * constr array +val destCase : constr -> case_info * constr * (constr,Univ.Instance.t) case_invert * constr * constr array (** Destructs a projection *) val destProj : constr -> Projection.t * constr @@ -497,12 +505,16 @@ val fold_with_full_binders : (rel_declaration -> 'a -> 'a) -> ('a -> 'b -> constr -> 'b) -> 'a -> 'b -> constr -> 'b +val fold_invert : ('a -> 'b -> 'a) -> 'a -> ('b, 'c) case_invert -> 'a + (** [map f c] maps [f] on the immediate subterms of [c]; it is not recursive and the order with which subterms are processed is not specified *) val map : (constr -> constr) -> constr -> constr +val map_invert : ('a -> 'a) -> ('a, 'b) case_invert -> ('a, 'b) case_invert + (** [map_user_view f c] maps [f] on the immediate subterms of [c]; it differs from [map f c] in that the typing context and body of the return predicate and of the branches of a [match] are considered as @@ -514,6 +526,9 @@ val map_user_view : (constr -> constr) -> constr -> constr val fold_map : ('a -> constr -> 'a * constr) -> 'a -> constr -> 'a * constr +val fold_map_invert : ('a -> 'b -> 'a * 'b) -> + 'a -> ('b, 'c) case_invert -> 'a * ('b, 'c) case_invert + (** [map_with_binders g f n c] maps [f n] on the immediate subterms of [c]; it carries an extra data [n] (typically a lift index) which is processed by [g] (which typically add 1 to [n]) at @@ -529,6 +544,8 @@ val map_with_binders : val iter : (constr -> unit) -> constr -> unit +val iter_invert : ('a -> unit) -> ('a, 'b) case_invert -> unit + (** [iter_with_binders g f n c] iters [f n] on the immediate subterms of [c]; it carries an extra data [n] (typically a lift index) which is processed by [g] (which typically add 1 to [n]) at @@ -558,7 +575,7 @@ val compare_head : constr constr_compare_fn -> constr constr_compare_fn (** Convert a global reference applied to 2 instances. The int says how many arguments are given (as we can only use cumulativity for fully applied inductives/constructors) .*) -type 'univs instance_compare_fn = GlobRef.t -> int -> +type 'univs instance_compare_fn = (GlobRef.t * int) option -> 'univs -> 'univs -> bool (** [compare_head_gen u s f c1 c2] compare [c1] and [c2] using [f] to @@ -605,6 +622,9 @@ val compare_head_gen_leq : Univ.Instance.t instance_compare_fn -> constr constr_compare_fn -> constr constr_compare_fn +val eq_invert : ('a -> 'a -> bool) -> ('b -> 'b -> bool) + -> ('a, 'b) case_invert -> ('a, 'b) case_invert -> bool + (** {6 Hashconsing} *) val hash : constr -> int diff --git a/kernel/cooking.ml b/kernel/cooking.ml index a17aff9b09..fdcf44c943 100644 --- a/kernel/cooking.ml +++ b/kernel/cooking.ml @@ -75,23 +75,30 @@ let share_univs cache r u l = let (u', args) = share cache r l in mkApp (instantiate_my_gr r (Instance.append u' u), args) -let update_case_info cache ci modlist = - try - let (_u,l) = share cache (IndRef ci.ci_ind) modlist in - { ci with ci_npar = ci.ci_npar + Array.length l } - with Not_found -> - ci +let update_case cache ci iv modlist = + match share cache (IndRef ci.ci_ind) modlist with + | exception Not_found -> ci, iv + | u, l -> + let iv = match iv with + | NoInvert -> NoInvert + | CaseInvert {univs; args;} -> + let univs = Instance.append u univs in + let args = Array.append l args in + CaseInvert {univs; args;} + in + { ci with ci_npar = ci.ci_npar + Array.length l }, iv let is_empty_modlist (cm, mm) = Cmap.is_empty cm && Mindmap.is_empty mm let expmod_constr cache modlist c = let share_univs = share_univs cache in - let update_case_info = update_case_info cache in + let update_case = update_case cache in let rec substrec c = match kind c with - | Case (ci,p,t,br) -> - Constr.map substrec (mkCase (update_case_info ci modlist,p,t,br)) + | Case (ci,p,iv,t,br) -> + let ci,iv = update_case ci iv modlist in + Constr.map substrec (mkCase (ci,p,iv,t,br)) | Ind (ind,u) -> (try diff --git a/kernel/declarations.ml b/kernel/declarations.ml index 2f6a870c8a..68bd1cbac9 100644 --- a/kernel/declarations.ml +++ b/kernel/declarations.ml @@ -94,6 +94,10 @@ type typing_flags = { cumulative_sprop : bool; (** SProp <= Type *) + + allow_uip: bool; + (** Allow definitional UIP (breaks termination) *) + } (* some contraints are in constant_constraints, some other may be in diff --git a/kernel/declareops.ml b/kernel/declareops.ml index 0ab99cab35..3de2cb00a4 100644 --- a/kernel/declareops.ml +++ b/kernel/declareops.ml @@ -27,6 +27,7 @@ let safe_flags oracle = { enable_native_compiler = true; indices_matter = true; cumulative_sprop = false; + allow_uip = false; } (** {6 Arities } *) diff --git a/kernel/environ.ml b/kernel/environ.ml index 182ed55d0e..0ae6f242f6 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -449,6 +449,7 @@ let same_flags { enable_VM; enable_native_compiler; cumulative_sprop; + allow_uip; } alt = check_guarded == alt.check_guarded && check_positive == alt.check_positive && @@ -458,7 +459,8 @@ let same_flags { share_reduction == alt.share_reduction && enable_VM == alt.enable_VM && enable_native_compiler == alt.enable_native_compiler && - cumulative_sprop == alt.cumulative_sprop + cumulative_sprop == alt.cumulative_sprop && + allow_uip == alt.allow_uip [@warning "+9"] let set_cumulative_sprop b = map_universes (UGraph.set_cumulative_sprop b) diff --git a/kernel/indTyping.ml b/kernel/indTyping.ml index e9687991c0..179353d3f0 100644 --- a/kernel/indTyping.ml +++ b/kernel/indTyping.ml @@ -134,11 +134,18 @@ let check_constructors env_ar_par isrecord params lc (arity,indices,univ_info) = (* Empty type: all OK *) | 0 -> univ_info - (* SProp primitive records are OK, if we squash and become fakerecord also OK *) - | 1 when isrecord -> univ_info - - (* Unit and identity types must squash if SProp *) - | 1 -> check_univ_leq env_ar_par Univ.Universe.type0m univ_info + | 1 -> + (* SProp primitive records are OK, if we squash and become fakerecord also OK *) + if isrecord then univ_info + (* 1 constructor with no arguments also OK in SProp (to make + things easier on ourselves when reducing we forbid letins) *) + else if (Environ.typing_flags env_ar_par).allow_uip + && fst (splayed_lc.(0)) = [] + && List.for_all Context.Rel.Declaration.is_local_assum params + then univ_info + (* 1 constructor with arguments must squash if SProp + (we could allow arguments in SProp but the reduction rule is a pain) *) + else check_univ_leq env_ar_par Univ.Universe.type0m univ_info (* More than 1 constructor: must squash if Prop/SProp *) | _ -> check_univ_leq env_ar_par Univ.Universe.type0 univ_info diff --git a/kernel/inductive.ml b/kernel/inductive.ml index 8423813639..c51d82ce07 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -756,7 +756,7 @@ let rec subterm_specif renv stack t = let f,l = decompose_app (whd_all renv.env t) in match kind f with | Rel k -> subterm_var k renv - | Case (ci,p,c,lbr) -> + | Case (ci,p,_iv,c,lbr) -> (* iv ignored: it's just a cache *) let stack' = push_stack_closures renv l stack in let cases_spec = branches_specif renv (lazy_subterm_specif renv [] c) ci @@ -954,7 +954,7 @@ let check_one_fix renv recpos trees def = check_rec_call renv stack (Term.applist(lift p c,l)) end - | Case (ci,p,c_0,lrest) -> + | Case (ci,p,iv,c_0,lrest) -> (* iv ignored: it's just a cache *) begin try List.iter (check_rec_call renv []) (c_0::p::l); (* compute the recarg info for the arguments of each branch *) @@ -976,7 +976,7 @@ let check_one_fix renv recpos trees def = (* the call to whd_betaiotazeta will reduce the apparent iota redex away *) check_rec_call renv [] - (Term.applist (mkCase (ci,p,c_0,lrest), l)) + (Term.applist (mkCase (ci,p,iv,c_0,lrest), l)) | _ -> Exninfo.iraise exn end @@ -1254,7 +1254,7 @@ let check_one_cofix env nbfix def deftype = else raise (CoFixGuardError (env,UnguardedRecursiveCall c)) - | Case (_,p,tm,vrest) -> + | Case (_,p,_,tm,vrest) -> (* iv ignored: just a cache *) begin let tree = match restrict_spec env (Subterm (Strict, tree)) p with | Dead_code -> assert false diff --git a/kernel/inferCumulativity.ml b/kernel/inferCumulativity.ml index 662ad550b8..71a3e95d25 100644 --- a/kernel/inferCumulativity.ml +++ b/kernel/inferCumulativity.ml @@ -139,6 +139,11 @@ let rec infer_fterm cv_pb infos variances hd stk = let variances = infer_vect infos variances (Array.map (mk_clos le) cl) in infer_stack infos variances stk + | FCaseInvert (_,p,_,_,br,e) -> + let infer c variances = infer_fterm CONV infos variances (mk_clos e c) [] in + let variances = infer p variances in + Array.fold_right infer br variances + (* Removed by whnf *) | FLOCKED | FCaseT _ | FLetIn _ | FApp _ | FLIFT _ | FCLOS _ -> assert false diff --git a/kernel/mod_subst.ml b/kernel/mod_subst.ml index 317141e324..2aeb1ea202 100644 --- a/kernel/mod_subst.ml +++ b/kernel/mod_subst.ml @@ -364,20 +364,21 @@ let rec map_kn f f' c = | Construct (((kn,i),j),u) -> let kn' = f kn in if kn'==kn then c else mkConstructU (((kn',i),j),u) - | Case (ci,p,ct,l) -> + | Case (ci,p,iv,ct,l) -> let ci_ind = let (kn,i) = ci.ci_ind in let kn' = f kn in if kn'==kn then ci.ci_ind else kn',i in let p' = func p in + let iv' = map_invert func iv in let ct' = func ct in let l' = Array.Smart.map func l in - if (ci.ci_ind==ci_ind && p'==p + if (ci.ci_ind==ci_ind && p'==p && iv'==iv && l'==l && ct'==ct)then c else mkCase ({ci with ci_ind = ci_ind}, - p',ct', l') + p',iv',ct', l') | Cast (ct,k,t) -> let ct' = func ct in let t'= func t in diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml index f30ddce4d7..c8cee7db73 100644 --- a/kernel/nativecode.ml +++ b/kernel/nativecode.ml @@ -2088,7 +2088,7 @@ let compile_deps env sigma prefix ~interactive init t = | Proj (p,c) -> let init = compile_mind_deps env prefix ~interactive init (Projection.mind p) in aux env lvl init c - | Case (ci, _p, _c, _ac) -> + | Case (ci, _p, _iv, _c, _ac) -> let mind = fst ci.ci_ind in let init = compile_mind_deps env prefix ~interactive init mind in fold_constr_with_binders succ (aux env) lvl init t diff --git a/kernel/nativelambda.ml b/kernel/nativelambda.ml index 02ee501f5f..3819cfd8ee 100644 --- a/kernel/nativelambda.ml +++ b/kernel/nativelambda.ml @@ -521,7 +521,7 @@ let rec lambda_of_constr cache env sigma c = let prefix = get_mind_prefix env (fst ind) in mkLapp (Lproj (prefix, ind, Projection.arg p)) [|lambda_of_constr cache env sigma c|] - | Case(ci,t,a,branches) -> + | Case(ci,t,_iv,a,branches) -> (* XXX handle iv *) let (mind,i as ind) = ci.ci_ind in let mib = lookup_mind mind env in let oib = mib.mind_packets.(i) in diff --git a/kernel/reduction.ml b/kernel/reduction.ml index 4ff90dd70d..e4b0bb17d4 100644 --- a/kernel/reduction.ml +++ b/kernel/reduction.ml @@ -209,12 +209,16 @@ type conv_pb = let is_cumul = function CUMUL -> true | CONV -> false -type 'a universe_compare = - { (* Might raise NotConvertible *) - compare_sorts : env -> conv_pb -> Sorts.t -> Sorts.t -> 'a -> 'a; - compare_instances: flex:bool -> Univ.Instance.t -> Univ.Instance.t -> 'a -> 'a; - compare_cumul_instances : conv_pb -> Univ.Variance.t array -> - Univ.Instance.t -> Univ.Instance.t -> 'a -> 'a } +type 'a universe_compare = { + (* used in reduction *) + compare_graph : 'a -> UGraph.t; + + (* Might raise NotConvertible *) + compare_sorts : env -> conv_pb -> Sorts.t -> Sorts.t -> 'a -> 'a; + compare_instances: flex:bool -> Univ.Instance.t -> Univ.Instance.t -> 'a -> 'a; + compare_cumul_instances : conv_pb -> Univ.Variance.t array -> + Univ.Instance.t -> Univ.Instance.t -> 'a -> 'a; +} type 'a universe_state = 'a * 'a universe_compare @@ -302,7 +306,6 @@ let unfold_ref_with_args infos tab fl v = type conv_tab = { cnv_inf : clos_infos; - relevances : Sorts.relevance Range.t; lft_tab : clos_tab; rgt_tab : clos_tab; } @@ -313,13 +316,13 @@ type conv_tab = { passed to each respective side of the conversion function below. *) let push_relevance infos r = - { infos with relevances = Range.cons r.Context.binder_relevance infos.relevances } + { infos with cnv_inf = CClosure.push_relevance infos.cnv_inf r } let push_relevances infos nas = - { infos with relevances = Array.fold_left (fun l x -> Range.cons x.Context.binder_relevance l) infos.relevances nas } + { infos with cnv_inf = CClosure.push_relevances infos.cnv_inf nas } let rec skip_pattern infos relevances n c1 c2 = - if Int.equal n 0 then {infos with relevances}, c1, c2 + if Int.equal n 0 then {infos with cnv_inf = CClosure.set_info_relevances infos.cnv_inf relevances}, c1, c2 else match kind c1, kind c2 with | Lambda (x, _, c1), Lambda (_, _, c2) -> skip_pattern infos (Range.cons x.Context.binder_relevance relevances) (pred n) c1 c2 @@ -327,11 +330,11 @@ let rec skip_pattern infos relevances n c1 c2 = let skip_pattern infos n c1 c2 = if Int.equal n 0 then infos, c1, c2 - else skip_pattern infos infos.relevances n c1 c2 + else skip_pattern infos (info_relevances infos.cnv_inf) n c1 c2 let is_irrelevant infos lft c = let env = info_env infos.cnv_inf in - try Relevanceops.relevance_of_fterm env infos.relevances lft c == Sorts.Irrelevant with _ -> false + try Relevanceops.relevance_of_fterm env (info_relevances infos.cnv_inf) lft c == Sorts.Irrelevant with _ -> false (* Conversion between [lft1]term1 and [lft2]term2 *) let rec ccnv cv_pb l2r infos lft1 lft2 term1 term2 cuniv = @@ -633,12 +636,20 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv = if Float64.equal f1 f2 then convert_stacks l2r infos lft1 lft2 v1 v2 cuniv else raise NotConvertible + | FCaseInvert (ci1,p1,_,_,br1,e1), FCaseInvert (ci2,p2,_,_,br2,e2) -> + (if not (eq_ind ci1.ci_ind ci2.ci_ind) then raise NotConvertible); + let el1 = el_stack lft1 v1 and el2 = el_stack lft2 v2 in + let ccnv = ccnv CONV l2r infos el1 el2 in + let cuniv = ccnv (mk_clos e1 p1) (mk_clos e2 p2) cuniv in + Array.fold_right2 (fun b1 b2 cuniv -> ccnv (mk_clos e1 b1) (mk_clos e2 b2) cuniv) + br1 br2 cuniv + (* Should not happen because both (hd1,v1) and (hd2,v2) are in whnf *) | ( (FLetIn _, _) | (FCaseT _,_) | (FApp _,_) | (FCLOS _,_) | (FLIFT _,_) | (_, FLetIn _) | (_,FCaseT _) | (_,FApp _) | (_,FCLOS _) | (_,FLIFT _) | (FLOCKED,_) | (_,FLOCKED) ) -> assert false - | (FRel _ | FAtom _ | FInd _ | FFix _ | FCoFix _ + | (FRel _ | FAtom _ | FInd _ | FFix _ | FCoFix _ | FCaseInvert _ | FProd _ | FEvar _ | FInt _ | FFloat _), _ -> raise NotConvertible and convert_stacks l2r infos lft1 lft2 stk1 stk2 cuniv = @@ -711,10 +722,10 @@ and convert_list l2r infos lft1 lft2 v1 v2 cuniv = match v1, v2 with let clos_gen_conv trans cv_pb l2r evars env univs t1 t2 = let reds = CClosure.RedFlags.red_add_transparent betaiotazeta trans in - let infos = create_clos_infos ~evars reds env in + let graph = (snd univs).compare_graph (fst univs) in + let infos = create_clos_infos ~univs:graph ~evars reds env in let infos = { cnv_inf = infos; - relevances = Range.empty; lft_tab = create_tab (); rgt_tab = create_tab (); } in @@ -759,10 +770,25 @@ let check_inductive_instances cv_pb variance u1 u2 univs = else raise NotConvertible let checked_universes = - { compare_sorts = checked_sort_cmp_universes; + { compare_graph = (fun x -> x); + compare_sorts = checked_sort_cmp_universes; compare_instances = check_convert_instances; compare_cumul_instances = check_inductive_instances; } +let () = + let conv infos tab a b = + try + let univs = info_univs infos in + let infos = { cnv_inf = infos; lft_tab = tab; rgt_tab = tab; } in + let univs', _ = ccnv CONV false infos el_id el_id a b + (univs, checked_universes) + in + assert (univs==univs'); + true + with NotConvertible -> false + in + CClosure.set_conv conv + let infer_eq (univs, cstrs as cuniv) u u' = if UGraph.check_eq univs u u' then cuniv else @@ -807,7 +833,8 @@ let infer_inductive_instances cv_pb variance u1 u2 (univs,csts') = (univs, Univ.Constraint.union csts csts') let inferred_universes : (UGraph.t * Univ.Constraint.t) universe_compare = - { compare_sorts = infer_cmp_universes; + { compare_graph = (fun (x,_) -> x); + compare_sorts = infer_cmp_universes; compare_instances = infer_convert_instances; compare_cumul_instances = infer_inductive_instances; } diff --git a/kernel/reduction.mli b/kernel/reduction.mli index ff5934c66c..4ae3838691 100644 --- a/kernel/reduction.mli +++ b/kernel/reduction.mli @@ -36,12 +36,15 @@ type 'a extended_conversion_function = type conv_pb = CONV | CUMUL -type 'a universe_compare = - { (* Might raise NotConvertible *) - compare_sorts : env -> conv_pb -> Sorts.t -> Sorts.t -> 'a -> 'a; - compare_instances: flex:bool -> Univ.Instance.t -> Univ.Instance.t -> 'a -> 'a; - compare_cumul_instances : conv_pb -> Univ.Variance.t array -> - Univ.Instance.t -> Univ.Instance.t -> 'a -> 'a } +type 'a universe_compare = { + compare_graph : 'a -> UGraph.t; (* used for case inversion in reduction *) + + (* Might raise NotConvertible *) + compare_sorts : env -> conv_pb -> Sorts.t -> Sorts.t -> 'a -> 'a; + compare_instances: flex:bool -> Univ.Instance.t -> Univ.Instance.t -> 'a -> 'a; + compare_cumul_instances : conv_pb -> Univ.Variance.t array -> + Univ.Instance.t -> Univ.Instance.t -> 'a -> 'a; +} type 'a universe_state = 'a * 'a universe_compare diff --git a/kernel/relevanceops.ml b/kernel/relevanceops.ml index 3f3e722245..3dd965aca4 100644 --- a/kernel/relevanceops.ml +++ b/kernel/relevanceops.ml @@ -61,7 +61,7 @@ let rec relevance_of_fterm env extra lft f = | FProj (p, _) -> relevance_of_projection env p | FFix (((_,i),(lna,_,_)), _) -> (lna.(i)).binder_relevance | FCoFix ((i,(lna,_,_)), _) -> (lna.(i)).binder_relevance - | FCaseT (ci, _, _, _, _) -> ci.ci_relevance + | FCaseT (ci, _, _, _, _) | FCaseInvert (ci, _, _, _, _, _) -> ci.ci_relevance | FLambda (len, tys, bdy, e) -> let extra = List.fold_left (fun accu (x, _) -> Range.cons (binder_relevance x) accu) extra tys in let lft = Esubst.el_liftn len lft in @@ -97,7 +97,7 @@ and relevance_of_term_extra env extra lft subs c = | App (c, _) -> relevance_of_term_extra env extra lft subs c | Const (c,_) -> relevance_of_constant env c | Construct (c,_) -> relevance_of_constructor env c - | Case (ci, _, _, _) -> ci.ci_relevance + | Case (ci, _, _, _, _) -> ci.ci_relevance | Fix ((_,i),(lna,_,_)) -> (lna.(i)).binder_relevance | CoFix (i,(lna,_,_)) -> (lna.(i)).binder_relevance | Proj (p, _) -> relevance_of_projection env p diff --git a/kernel/type_errors.ml b/kernel/type_errors.ml index 42fc6b2e45..ae5c4b6880 100644 --- a/kernel/type_errors.ml +++ b/kernel/type_errors.ml @@ -68,6 +68,7 @@ type ('constr, 'types) ptype_error = | UndeclaredUniverse of Level.t | DisallowedSProp | BadRelevance + | BadInvert type type_error = (constr, types) ptype_error @@ -159,6 +160,9 @@ let error_disallowed_sprop env = let error_bad_relevance env = raise (TypeError (env, BadRelevance)) +let error_bad_invert env = + raise (TypeError (env, BadInvert)) + let map_pguard_error f = function | NotEnoughAbstractionInFixBody -> NotEnoughAbstractionInFixBody | RecursionNotOnInductiveType c -> RecursionNotOnInductiveType (f c) @@ -202,3 +206,4 @@ let map_ptype_error f = function | UndeclaredUniverse l -> UndeclaredUniverse l | DisallowedSProp -> DisallowedSProp | BadRelevance -> BadRelevance +| BadInvert -> BadInvert diff --git a/kernel/type_errors.mli b/kernel/type_errors.mli index a58d9aa50d..b1f7eb8a34 100644 --- a/kernel/type_errors.mli +++ b/kernel/type_errors.mli @@ -69,6 +69,7 @@ type ('constr, 'types) ptype_error = | UndeclaredUniverse of Level.t | DisallowedSProp | BadRelevance + | BadInvert type type_error = (constr, types) ptype_error @@ -143,5 +144,7 @@ val error_disallowed_sprop : env -> 'a val error_bad_relevance : env -> 'a +val error_bad_invert : env -> 'a + val map_pguard_error : ('c -> 'd) -> 'c pguard_error -> 'd pguard_error val map_ptype_error : ('c -> 'd) -> ('c, 'c) ptype_error -> ('d, 'd) ptype_error diff --git a/kernel/typeops.ml b/kernel/typeops.ml index 19d76bfee6..58a099f7f6 100644 --- a/kernel/typeops.ml +++ b/kernel/typeops.ml @@ -407,7 +407,20 @@ let check_branch_types env (ind,u) c ct lft explft = | Invalid_argument _ -> error_number_branches env (make_judge c ct) (Array.length explft) -let type_of_case env ci p pt c ct _lf lft = +let should_invert_case env ci = + ci.ci_relevance == Sorts.Relevant && + let mib,mip = lookup_mind_specif env ci.ci_ind in + mip.mind_relevance == Sorts.Irrelevant && + (* NB: it's possible to have 2 ctors or arguments to 1 ctor by unsetting univ checks + but we don't do special reduction in such cases + + XXX Someday consider more carefully what happens with letin params and arguments + (currently they're squashed, see indtyping) + *) + Array.length mip.mind_nf_lc = 1 && + List.length (fst mip.mind_nf_lc.(0)) = List.length mib.mind_params_ctxt + +let type_of_case env ci p pt iv c ct _lf lft = let (pind, _ as indspec) = try find_rectype env ct with Not_found -> error_case_not_inductive env (make_judge c ct) in @@ -418,6 +431,14 @@ let type_of_case env ci p pt c ct _lf lft = else (warn_bad_relevance_ci (); {ci with ci_relevance=rp}) in let () = check_case_info env pind rp ci in + let () = + let is_inversion = match iv with + | NoInvert -> false + | CaseInvert _ -> true (* contents already checked *) + in + if not (is_inversion = should_invert_case env ci) + then error_bad_invert env + in let (bty,rslty) = type_case_branches env indspec (make_judge p pt) c in let () = check_branch_types env pind c ct lft bty in @@ -564,13 +585,22 @@ let rec execute env cstr = | Construct c -> cstr, type_of_constructor env c - | Case (ci,p,c,lf) -> + | Case (ci,p,iv,c,lf) -> let c', ct = execute env c in + let iv' = match iv with + | NoInvert -> NoInvert + | CaseInvert {univs;args} -> + let ct' = mkApp (mkIndU (ci.ci_ind,univs), args) in + let (ct', _) : constr * Sorts.t = execute_is_type env ct' in + let () = conv_leq false env ct ct' in + let _, args' = decompose_appvect ct' in + if args == args' then iv else CaseInvert {univs;args=args'} + in let p', pt = execute env p in let lf', lft = execute_array env lf in - let ci', t = type_of_case env ci p' pt c' ct lf' lft in - let cstr = if ci == ci' && c == c' && p == p' && lf == lf' then cstr - else mkCase(ci',p',c',lf') + let ci', t = type_of_case env ci p' pt iv' c' ct lf' lft in + let cstr = if ci == ci' && c == c' && p == p' && iv == iv' && lf == lf' then cstr + else mkCase(ci',p',iv',c',lf') in cstr, t @@ -710,10 +740,10 @@ let judge_of_inductive env indu = let judge_of_constructor env cu = make_judge (mkConstructU cu) (type_of_constructor env cu) -let judge_of_case env ci pj cj lfj = +let judge_of_case env ci pj iv cj lfj = let lf, lft = dest_judgev lfj in - let ci, t = type_of_case env ci pj.uj_val pj.uj_type cj.uj_val cj.uj_type lf lft in - make_judge (mkCase (ci, (*nf_betaiota*) pj.uj_val, cj.uj_val, lft)) t + let ci, t = type_of_case env ci pj.uj_val pj.uj_type iv cj.uj_val cj.uj_type lf lft in + make_judge (mkCase (ci, (*nf_betaiota*) pj.uj_val, iv, cj.uj_val, lft)) t (* Building type of primitive operators and type *) diff --git a/kernel/typeops.mli b/kernel/typeops.mli index e61d5c399e..65531ed38a 100644 --- a/kernel/typeops.mli +++ b/kernel/typeops.mli @@ -94,8 +94,9 @@ val judge_of_constructor : env -> constructor puniverses -> unsafe_judgment (** {6 Type of Cases. } *) val judge_of_case : env -> case_info - -> unsafe_judgment -> unsafe_judgment -> unsafe_judgment array - -> unsafe_judgment + -> unsafe_judgment -> (constr,Instance.t) case_invert -> unsafe_judgment + -> unsafe_judgment array + -> unsafe_judgment (** {6 Type of global references. } *) @@ -128,3 +129,7 @@ val type_of_prim : env -> CPrimitives.t -> types val warn_bad_relevance_name : string (** Allow the checker to make this warning into an error. *) + +val should_invert_case : env -> case_info -> bool +(** We have case inversion exactly when going from irrelevant nonempty + (ie 1 constructor) inductive to relevant type. *) diff --git a/kernel/vars.ml b/kernel/vars.ml index a4465c293b..63d88c659a 100644 --- a/kernel/vars.ml +++ b/kernel/vars.ml @@ -252,6 +252,12 @@ let subst_univs_level_constr subst c = let u' = Univ.subst_univs_level_universe subst u in if u' == u then t else (changed := true; mkSort (Sorts.sort_of_univ u')) + | Case (ci,p,CaseInvert {univs;args},c,br) -> + if Univ.Instance.is_empty univs then Constr.map aux t + else + let univs' = f univs in + if univs' == univs then Constr.map aux t + else (changed:=true; Constr.map aux (mkCase (ci,p,CaseInvert {univs=univs';args},c,br))) | _ -> Constr.map aux t in let c' = aux c in @@ -288,6 +294,10 @@ let subst_instance_constr subst c = let u' = Univ.subst_instance_universe subst u in if u' == u then t else (mkSort (Sorts.sort_of_univ u')) + | Case (ci,p,CaseInvert {univs;args},c,br) -> + let univs' = f univs in + if univs' == univs then Constr.map aux t + else Constr.map aux (mkCase (ci,p,CaseInvert {univs=univs';args},c,br)) | _ -> Constr.map aux t in aux c diff --git a/parsing/g_constr.mlg b/parsing/g_constr.mlg index c19dd00b38..429e740403 100644 --- a/parsing/g_constr.mlg +++ b/parsing/g_constr.mlg @@ -165,11 +165,11 @@ GRAMMAR EXTEND Gram collapse -(3) into the numeral -3. *) (match c.CAst.v with | CPrim (Numeral (NumTok.SPlus,n)) -> - CAst.make ~loc @@ CNotation(None,(InConstrEntrySomeLevel,"( _ )"),([c],[],[],[])) + CAst.make ~loc @@ CNotation(None,(InConstrEntry,"( _ )"),([c],[],[],[])) | _ -> c) } | "{|"; c = record_declaration; bar_cbrace -> { c } | "{"; c = binder_constr ; "}" -> - { CAst.make ~loc @@ CNotation(None,(InConstrEntrySomeLevel,"{ _ }"),([c],[],[],[])) } + { CAst.make ~loc @@ CNotation(None,(InConstrEntry,"{ _ }"),([c],[],[],[])) } | "`{"; c = operconstr LEVEL "200"; "}" -> { CAst.make ~loc @@ CGeneralization (MaxImplicit, None, c) } | "`("; c = operconstr LEVEL "200"; ")" -> @@ -346,7 +346,7 @@ GRAMMAR EXTEND Gram collapse -(3) into the numeral -3. *) match p.CAst.v with | CPatPrim (Numeral (NumTok.SPlus,n)) -> - CAst.make ~loc @@ CPatNotation(None,(InConstrEntrySomeLevel,"( _ )"),([p],[]),[]) + CAst.make ~loc @@ CPatNotation(None,(InConstrEntry,"( _ )"),([p],[]),[]) | _ -> p } | "("; p = pattern LEVEL "200"; "|" ; pl = LIST1 pattern LEVEL "200" SEP "|"; ")" -> { CAst.make ~loc @@ CPatOr (p::pl) } diff --git a/parsing/notation_gram.ml b/parsing/notation_gram.ml index 7940931dfc..045f497070 100644 --- a/parsing/notation_gram.ml +++ b/parsing/notation_gram.ml @@ -9,13 +9,6 @@ (************************************************************************) open Names -open Extend -open Constrexpr - -(** Dealing with precedences *) - -type level = notation_entry * entry_level * entry_relative_level list * constr_entry_key list - (* first argument is InCustomEntry s for custom entries *) type grammar_constr_prod_item = | GramConstrTerminal of string Tok.p @@ -28,10 +21,11 @@ type grammar_constr_prod_item = (** Grammar rules for a notation *) type one_notation_grammar = { - notgram_level : level; + notgram_level : Notation.level; notgram_assoc : Gramlib.Gramext.g_assoc option; notgram_notation : Constrexpr.notation; notgram_prods : grammar_constr_prod_item list list; + notgram_typs : Extend.constr_entry_key list; } type notation_grammar = one_notation_grammar list diff --git a/parsing/notgram_ops.ml b/parsing/notgram_ops.ml index 1d18e7dcfa..74ced431c9 100644 --- a/parsing/notgram_ops.ml +++ b/parsing/notgram_ops.ml @@ -12,63 +12,33 @@ open Pp open CErrors open Util open Notation -open Constrexpr -(* Register the level of notation for parsing and printing +(* Register the grammar of notation for parsing and printing (also register the parsing rule if not onlyprinting) *) -let notation_level_map = Summary.ref ~name:"notation_level_map" NotationMap.empty +let notation_grammar_map = Summary.ref ~name:"notation_grammar_map" NotationMap.empty -let declare_notation_level ntn parsing_rule level = +let declare_notation_grammar ntn rule = try - let _ = NotationMap.find ntn !notation_level_map in - anomaly (str "Notation " ++ pr_notation ntn ++ str " is already assigned a level.") + let _ = NotationMap.find ntn !notation_grammar_map in + anomaly (str "Notation " ++ pr_notation ntn ++ str " is already assigned a grammar.") with Not_found -> - notation_level_map := NotationMap.add ntn (parsing_rule,level) !notation_level_map + notation_grammar_map := NotationMap.add ntn rule !notation_grammar_map -let level_of_notation ntn = - NotationMap.find ntn !notation_level_map +let grammar_of_notation ntn = + NotationMap.find ntn !notation_grammar_map -let get_defined_notations () = - NotationSet.elements @@ NotationMap.domain !notation_level_map - -(**********************************************************************) -(* Equality *) - -open Extend - -let entry_relative_level_eq t1 t2 = match t1, t2 with -| LevelLt n1, LevelLt n2 -> Int.equal n1 n2 -| LevelLe n1, LevelLe n2 -> Int.equal n1 n2 -| LevelSome, LevelSome -> true -| (LevelLt _ | LevelLe _ | LevelSome), _ -> false - -let production_position_eq pp1 pp2 = match (pp1,pp2) with -| BorderProd (side1,assoc1), BorderProd (side2,assoc2) -> side1 = side2 && assoc1 = assoc2 -| InternalProd, InternalProd -> true -| (BorderProd _ | InternalProd), _ -> false +let notation_subentries_map = Summary.ref ~name:"notation_subentries_map" NotationMap.empty -let production_level_eq l1 l2 = match (l1,l2) with -| NextLevel, NextLevel -> true -| NumLevel n1, NumLevel n2 -> Int.equal n1 n2 -| DefaultLevel, DefaultLevel -> true -| (NextLevel | NumLevel _ | DefaultLevel), _ -> false - -let constr_entry_key_eq eq v1 v2 = match v1, v2 with -| ETIdent, ETIdent -> true -| ETGlobal, ETGlobal -> true -| ETBigint, ETBigint -> true -| ETBinder b1, ETBinder b2 -> b1 == b2 -| ETConstr (s1,bko1,lev1), ETConstr (s2,bko2,lev2) -> - notation_entry_eq s1 s2 && eq lev1 lev2 && Option.equal (=) bko1 bko2 -| ETPattern (b1,n1), ETPattern (b2,n2) -> b1 = b2 && Option.equal Int.equal n1 n2 -| (ETIdent | ETGlobal | ETBigint | ETBinder _ | ETConstr _ | ETPattern _), _ -> false +let declare_notation_subentries ntn entries = + try + let _ = NotationMap.find ntn !notation_grammar_map in + anomaly (str "Notation " ++ pr_notation ntn ++ str " is already assigned a grammar.") + with Not_found -> + notation_subentries_map := NotationMap.add ntn entries !notation_subentries_map -let level_eq_gen strict (s1, l1, t1, u1) (s2, l2, t2, u2) = - let prod_eq (l1,pp1) (l2,pp2) = - not strict || - (production_level_eq l1 l2 && production_position_eq pp1 pp2) in - notation_entry_eq s1 s2 && Int.equal l1 l2 && List.equal entry_relative_level_eq t1 t2 - && List.equal (constr_entry_key_eq prod_eq) u1 u2 +let subentries_of_notation ntn = + NotationMap.find ntn !notation_subentries_map -let level_eq = level_eq_gen false +let get_defined_notations () = + NotationSet.elements @@ NotationMap.domain !notation_grammar_map diff --git a/parsing/notgram_ops.mli b/parsing/notgram_ops.mli index dd1375a1f1..15b8717705 100644 --- a/parsing/notgram_ops.mli +++ b/parsing/notgram_ops.mli @@ -12,14 +12,14 @@ open Constrexpr open Notation_gram -val level_eq : level -> level -> bool -val entry_relative_level_eq : entry_relative_level -> entry_relative_level -> bool +(** {6 Declare the parsing rules and entries of a (possibly uninterpreted) notation } *) -(** {6 Declare and test the level of a (possibly uninterpreted) notation } *) - -val declare_notation_level : notation -> notation_grammar option -> level -> unit -val level_of_notation : notation -> notation_grammar option * level +val declare_notation_grammar : notation -> notation_grammar -> unit +val grammar_of_notation : notation -> notation_grammar (** raise [Not_found] if not declared *) +val declare_notation_subentries : notation -> Extend.constr_entry_key list -> unit +val subentries_of_notation : notation -> Extend.constr_entry_key list + (** Returns notations with defined parsing/printing rules *) val get_defined_notations : unit -> notation list diff --git a/parsing/ppextend.ml b/parsing/ppextend.ml index b888614ecb..fe6e8360c1 100644 --- a/parsing/ppextend.ml +++ b/parsing/ppextend.ml @@ -13,7 +13,6 @@ open Pp open CErrors open Notation open Constrexpr -open Notgram_ops (*s Pretty-print. *) diff --git a/plugins/btauto/refl_btauto.ml b/plugins/btauto/refl_btauto.ml index 52c6c5d0f9..23f8fe04a3 100644 --- a/plugins/btauto/refl_btauto.ml +++ b/plugins/btauto/refl_btauto.ml @@ -112,7 +112,7 @@ module Bool = struct else if head === negb && Array.length args = 1 then Negb (aux args.(0)) else Var (Env.add env c) - | Case (info, r, arg, pats) -> + | Case (info, r, _iv, arg, pats) -> let is_bool = let i = info.ci_ind in Names.eq_ind i (Lazy.force ind) diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml index 0f96b9bbe8..a7c926f50c 100644 --- a/plugins/extraction/extraction.ml +++ b/plugins/extraction/extraction.ml @@ -291,7 +291,7 @@ let rec extract_type env sg db j c args = let reason = if lvl == TypeScheme then Ktype else Kprop in Tarr (Tdummy reason, mld))) | Sort _ -> Tdummy Ktype (* The two logical cases. *) - | _ when sort_of env sg (applistc c args) == InProp -> Tdummy Kprop + | _ when info_of_family (sort_of env sg (applistc c args)) == Logic -> Tdummy Kprop | Rel n -> (match EConstr.lookup_rel n env with | LocalDef (_,t,_) -> @@ -672,8 +672,9 @@ let rec extract_term env sg mle mlt c args = (* we unify it with an fresh copy of the stored type of [Rel n]. *) let extract_rel mlt = put_magic (mlt, Mlenv.get mle n) (MLrel n) in extract_app env sg mle mlt extract_rel args - | Case ({ci_ind=ip},_,c0,br) -> - extract_app env sg mle mlt (extract_case env sg mle (ip,c0,br)) args + | Case ({ci_ind=ip},_,iv,c0,br) -> + (* If invert_case then this is a match that will get erased later, but right now we don't care. *) + extract_app env sg mle mlt (extract_case env sg mle (ip,c0,br)) args | Fix ((_,i),recd) -> extract_app env sg mle mlt (extract_fix env sg mle i recd) args | CoFix (i,recd) -> @@ -852,8 +853,8 @@ and extract_case env sg mle ((kn,i) as ip,c,br) mlt = end else (* [c] has an inductive type, and is not a type scheme type. *) let t = type_of env sg c in - (* The only non-informative case: [c] is of sort [Prop] *) - if (sort_of env sg t) == InProp then + (* The only non-informative case: [c] is of sort [Prop]/[SProp] *) + if info_of_family (sort_of env sg t) == Logic then begin add_recursors env kn; (* May have passed unseen if logical ... *) (* Logical singleton case: *) @@ -1016,7 +1017,7 @@ let extract_fixpoint env sg vkn (fi,ti,ci) = (* for replacing recursive calls [Rel ..] by the corresponding [Const]: *) let sub = List.rev_map EConstr.mkConst kns in for i = 0 to n-1 do - if sort_of env sg ti.(i) != InProp then + if info_of_family (sort_of env sg ti.(i)) != Logic then try let e,t = extract_std_constant env sg vkn.(i) (EConstr.Vars.substl sub ci.(i)) ti.(i) in @@ -1073,7 +1074,7 @@ let fake_match_projection env p = else let p = mkLambda (x, lift 1 indty, liftn 1 2 ty) in let branch = lift 1 (it_mkLambda_or_LetIn (mkRel (List.length ctx - (j-1))) ctx) in - let body = mkCase (ci, p, mkRel 1, [|branch|]) in + let body = mkCase (ci, p, NoInvert, mkRel 1, [|branch|]) in it_mkLambda_or_LetIn (mkLambda (x,indty,body)) mib.mind_params_ctxt | LocalDef (_,c,t) :: rem -> let c = liftn 1 j c in diff --git a/plugins/firstorder/unify.ml b/plugins/firstorder/unify.ml index 9c3debe48f..c62bc73e41 100644 --- a/plugins/firstorder/unify.ml +++ b/plugins/firstorder/unify.ml @@ -67,10 +67,10 @@ let unif env evd t1 t2= | _,Cast(_,_,_)->Queue.add (nt1,strip_outer_cast evd nt2) bige | (Prod(_,a,b),Prod(_,c,d))|(Lambda(_,a,b),Lambda(_,c,d))-> Queue.add (a,c) bige;Queue.add (pop b,pop d) bige - | Case (_,pa,ca,va),Case (_,pb,cb,vb)-> - Queue.add (pa,pb) bige; - Queue.add (ca,cb) bige; - let l=Array.length va in + | Case (_,pa,_,ca,va),Case (_,pb,_,cb,vb)-> + Queue.add (pa,pb) bige; + Queue.add (ca,cb) bige; + let l=Array.length va in if not (Int.equal l (Array.length vb)) then raise (UFAIL (nt1,nt2)) else diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index 9b578d4697..f2658a395f 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -585,10 +585,10 @@ let build_proof (interactive_proof : bool) (fnames : Constant.t list) ptes_infos let sigma = project g in (* observe (str "proving on " ++ Printer.pr_lconstr_env (pf_env g) term);*) match EConstr.kind sigma dyn_infos.info with - | Case (ci, ct, t, cb) -> + | Case (ci, ct, iv, t, cb) -> let do_finalize_t dyn_info' g = let t = dyn_info'.info in - let dyn_infos = {dyn_info' with info = mkCase (ci, ct, t, cb)} in + let dyn_infos = {dyn_info' with info = mkCase (ci, ct, iv, t, cb)} in let g_nb_prod = nb_prod (project g) (pf_concl g) in let g, type_of_term = tac_type_of g t in let term_eq = make_refl_eq (Lazy.force refl_equal) type_of_term t in diff --git a/plugins/funind/gen_principle.ml b/plugins/funind/gen_principle.ml index 167cf37026..f773157c52 100644 --- a/plugins/funind/gen_principle.ml +++ b/plugins/funind/gen_principle.ml @@ -70,7 +70,7 @@ let build_newrecursive lnameargsardef = CErrors.user_err ~hdr:"Function" (Pp.str "Body of Function must be given") in - States.with_state_protection (List.map f) lnameargsardef + Vernacstate.System.protect (List.map f) lnameargsardef in (recdef, rec_impls) @@ -987,7 +987,7 @@ and intros_with_rewrite_aux : Tacmach.tactic = ( UnivGen.constr_of_monomorphic_global @@ Coqlib.lib_ref "core.False.type" )) -> Proofview.V82.of_tactic tauto g - | Case (_, _, v, _) -> + | Case (_, _, _, v, _) -> tclTHENLIST [Proofview.V82.of_tactic (simplest_case v); intros_with_rewrite] g @@ -1026,7 +1026,7 @@ let rec reflexivity_with_destruct_cases g = match EConstr.kind (project g) (snd (destApp (project g) (pf_concl g))).(2) with - | Case (_, _, v, _) -> + | Case (_, _, _, v, _) -> tclTHENLIST [ Proofview.V82.of_tactic (simplest_case v) ; Proofview.V82.of_tactic intros diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index 884792cc15..701ea56c2a 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -312,7 +312,7 @@ let check_not_nested env sigma forbidden e = | Const _ -> () | Ind _ -> () | Construct _ -> () - | Case (_, t, e, a) -> + | Case (_, t, _, e, a) -> check_not_nested t; check_not_nested e; Array.iter check_not_nested a @@ -374,7 +374,13 @@ type journey_info = ; lambdA : (Name.t * types * constr, constr) journey_info_tac ; casE : ((constr infos -> tactic) -> constr infos -> tactic) - -> (case_info * constr * constr * constr array, constr) journey_info_tac + -> ( case_info + * constr + * (constr, EInstance.t) case_invert + * constr + * constr array + , constr ) + journey_info_tac ; otherS : (unit, constr) journey_info_tac ; apP : (constr * constr list, constr) journey_info_tac ; app_reC : (constr * constr list, constr) journey_info_tac @@ -474,9 +480,9 @@ let rec travel_aux jinfo continuation_tac (expr_info : constr infos) g = ++ Printer.pr_leconstr_env env sigma expr_info.info ++ str " can not contain a recursive call to " ++ Id.print expr_info.f_id ) ) - | Case (ci, t, a, l) -> + | Case (ci, t, iv, a, l) -> let continuation_tac_a = - jinfo.casE (travel jinfo) (ci, t, a, l) expr_info continuation_tac + jinfo.casE (travel jinfo) (ci, t, iv, a, l) expr_info continuation_tac in travel jinfo continuation_tac_a {expr_info with info = a; is_main_branch = false; is_final = false} @@ -767,7 +773,8 @@ let mkDestructEq not_on_hyp expr g = in (g, tac, to_revert) -let terminate_case next_step (ci, a, t, l) expr_info continuation_tac infos g = +let terminate_case next_step (ci, a, iv, t, l) expr_info continuation_tac infos + g = let sigma = project g in let env = pf_env g in let f_is_present = @@ -779,7 +786,7 @@ let terminate_case next_step (ci, a, t, l) expr_info continuation_tac infos g = let a' = infos.info in let new_info = { infos with - info = mkCase (ci, t, a', l) + info = mkCase (ci, t, iv, a', l) ; is_main_branch = expr_info.is_main_branch ; is_final = expr_info.is_final } in @@ -916,10 +923,10 @@ let prove_terminate = travel terminate_info (* Equation proof *) -let equation_case next_step (ci, a, t, l) expr_info continuation_tac infos = +let equation_case next_step case expr_info continuation_tac infos = observe_tac (fun _ _ -> str "equation case") - (terminate_case next_step (ci, a, t, l) expr_info continuation_tac infos) + (terminate_case next_step case expr_info continuation_tac infos) let rec prove_le g = let sigma = project g in diff --git a/plugins/ltac/extratactics.mlg b/plugins/ltac/extratactics.mlg index 40c64a1c26..66c72a30a2 100644 --- a/plugins/ltac/extratactics.mlg +++ b/plugins/ltac/extratactics.mlg @@ -776,7 +776,7 @@ let rec find_a_destructable_match sigma t = let cl = [cl, (None, None), None], None in let dest = TacAtom (CAst.make @@ TacInductionDestruct(false, false, cl)) in match EConstr.kind sigma t with - | Case (_,_,x,_) when closed0 sigma x -> + | Case (_,_,_,x,_) when closed0 sigma x -> if isVar sigma x then (* TODO check there is no rel n. *) raise (Found (Tacinterp.eval_tactic dest)) diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml index 40dea90c00..fb149071c9 100644 --- a/plugins/ltac/rewrite.ml +++ b/plugins/ltac/rewrite.ml @@ -923,8 +923,8 @@ let reset_env env = let env' = Global.env_of_context (Environ.named_context_val env) in Environ.push_rel_context (Environ.rel_context env) env' -let fold_match env sigma c = - let (ci, p, c, brs) = destCase sigma c in +let fold_match ?(force=false) env sigma c = + let (ci, p, iv, c, brs) = destCase sigma c in let cty = Retyping.get_type_of env sigma c in let dep, pred, exists, sk = let env', ctx, body = @@ -1184,7 +1184,7 @@ let subterm all flags (s : 'a pure_strategy) : 'a pure_strategy = | Fail | Identity -> b' in state, res - | Case (ci, p, c, brs) -> + | Case (ci, p, iv, c, brs) -> let cty = Retyping.get_type_of env (goalevars evars) c in let evars', eqty = app_poly_sort prop env evars coq_eq [| cty |] in let cstr' = Some eqty in @@ -1194,7 +1194,7 @@ let subterm all flags (s : 'a pure_strategy) : 'a pure_strategy = let state, res = match c' with | Success r -> - let case = mkCase (ci, lift 1 p, mkRel 1, Array.map (lift 1) brs) in + let case = mkCase (ci, lift 1 p, map_invert (lift 1) iv, mkRel 1, Array.map (lift 1) brs) in let res = make_leibniz_proof env case ty r in state, Success (coerce env unfresh (prop,cstr) res) | Fail | Identity -> @@ -1216,7 +1216,7 @@ let subterm all flags (s : 'a pure_strategy) : 'a pure_strategy = in match found with | Some r -> - let ctxc = mkCase (ci, lift 1 p, lift 1 c, Array.of_list (List.rev (brs' c'))) in + let ctxc = mkCase (ci, lift 1 p, map_invert (lift 1) iv, lift 1 c, Array.of_list (List.rev (brs' c'))) in state, Success (make_leibniz_proof env ctxc ty r) | None -> state, c' else diff --git a/plugins/ltac/tacentries.ml b/plugins/ltac/tacentries.ml index e6c59f446d..f8c25d5dd0 100644 --- a/plugins/ltac/tacentries.ml +++ b/plugins/ltac/tacentries.ml @@ -489,7 +489,7 @@ let register_ltac local ?deprecation tacl = in (* STATE XXX: Review what is going on here. Why does this needs protection? Why is not the STM level protection enough? Fishy *) - let defs = States.with_state_protection defs () in + let defs = Vernacstate.System.protect defs () in let iter (def, tac) = match def with | NewTac id -> Tacenv.register_ltac false local id tac ?deprecation; diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml index 878f7a834e..95faede7d0 100644 --- a/plugins/setoid_ring/newring.ml +++ b/plugins/setoid_ring/newring.ml @@ -77,7 +77,7 @@ let protect_red map env sigma c0 = let evars ev = Evarutil.safe_evar_value sigma ev in let c = EConstr.Unsafe.to_constr c0 in let tab = create_tab () in - let infos = create_clos_infos ~evars all env in + let infos = create_clos_infos ~univs:(Evd.universes sigma) ~evars all env in let map = lookup_map map sigma c0 in let rec eval n c = match Constr.kind c with | Prod (na, t, u) -> Constr.mkProd (na, eval n t, eval (n + 1) u) diff --git a/plugins/ssrmatching/ssrmatching.ml b/plugins/ssrmatching/ssrmatching.ml index 5d6e7c51d0..1ed632f03f 100644 --- a/plugins/ssrmatching/ssrmatching.ml +++ b/plugins/ssrmatching/ssrmatching.ml @@ -308,7 +308,7 @@ let iter_constr_LR f c = match kind c with | Prod (_, t, b) | Lambda (_, t, b) -> f t; f b | LetIn (_, v, t, b) -> f v; f t; f b | App (cf, a) -> f cf; Array.iter f a - | Case (_, p, v, b) -> f v; f p; Array.iter f b + | Case (_, p, iv, v, b) -> f v; iter_invert f iv; f p; Array.iter f b | Fix (_, (_, t, b)) | CoFix (_, (_, t, b)) -> for i = 0 to Array.length t - 1 do f t.(i); f b.(i) done | Proj(_,a) -> f a @@ -859,7 +859,7 @@ let glob_cpattern gs p = | k, (v, Some t), _ as orig -> if k = 'x' then glob_ssrterm gs ('(', (v, Some t), None) else match t.CAst.v with - | CNotation(_,(InConstrEntrySomeLevel,"( _ in _ )"), ([t1; t2], [], [], [])) -> + | CNotation(_,(InConstrEntry,"( _ in _ )"), ([t1; t2], [], [], [])) -> (try match glob t1, glob t2 with | (r1, None), (r2, None) -> encode k "In" [r1;r2] | (r1, Some _), (r2, Some _) when isCVar t1 -> @@ -867,11 +867,11 @@ let glob_cpattern gs p = | (r1, Some _), (r2, Some _) -> encode k "In" [r1; r2] | _ -> CErrors.anomaly (str"where are we?.") with _ when isCVar t1 -> encode k "In" [bind_in t1 t2]) - | CNotation(_,(InConstrEntrySomeLevel,"( _ in _ in _ )"), ([t1; t2; t3], [], [], [])) -> + | CNotation(_,(InConstrEntry,"( _ in _ in _ )"), ([t1; t2; t3], [], [], [])) -> check_var t2; encode k "In" [fst (glob t1); bind_in t2 t3] - | CNotation(_,(InConstrEntrySomeLevel,"( _ as _ )"), ([t1; t2], [], [], [])) -> + | CNotation(_,(InConstrEntry,"( _ as _ )"), ([t1; t2], [], [], [])) -> encode k "As" [fst (glob t1); fst (glob t2)] - | CNotation(_,(InConstrEntrySomeLevel,"( _ as _ in _ )"), ([t1; t2; t3], [], [], [])) -> + | CNotation(_,(InConstrEntry,"( _ as _ in _ )"), ([t1; t2; t3], [], [], [])) -> check_var t2; encode k "As" [fst (glob t1); bind_in t2 t3] | _ -> glob_ssrterm gs orig ;; diff --git a/plugins/ssrsearch/g_search.mlg b/plugins/ssrsearch/g_search.mlg index f5cbf2005b..5e002e09cc 100644 --- a/plugins/ssrsearch/g_search.mlg +++ b/plugins/ssrsearch/g_search.mlg @@ -59,7 +59,7 @@ let interp_search_notation ?loc tag okey = (Bytes.set s' i' '_'; loop (j + 1) (i' + 2)) else (String.blit s i s' i' m; loop (j + 1) (i' + m + 1)) in loop 0 1 in - let trim_ntn (pntn, m) = (InConstrEntrySomeLevel,Bytes.sub_string pntn 1 (max 0 m)) in + let trim_ntn (pntn, m) = (InConstrEntry,Bytes.sub_string pntn 1 (max 0 m)) in let pr_ntn ntn = str "(" ++ Notation.pr_notation ntn ++ str ")" in let pr_and_list pr = function | [x] -> pr x diff --git a/pretyping/cases.ml b/pretyping/cases.ml index 25353b7c12..a459229256 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -1131,14 +1131,14 @@ let rec ungeneralize sigma n ng body = | LetIn (na,b,t,c) -> (* We traverse an alias *) mkLetIn (na,b,t,ungeneralize sigma (n+1) ng c) - | Case (ci,p,c,brs) -> + | Case (ci,p,iv,c,brs) -> (* We traverse a split *) let p = let sign,p = decompose_lam_assum sigma p in let sign2,p = decompose_prod_n_assum sigma ng p in let p = prod_applist sigma p [mkRel (n+List.length sign+ng)] in it_mkLambda_or_LetIn (it_mkProd_or_LetIn p sign2) sign in - mkCase (ci,p,c,Array.map2 (fun q c -> + mkCase (ci,p,iv,c,Array.map2 (fun q c -> let sign,b = decompose_lam_n_decls sigma q c in it_mkLambda_or_LetIn (ungeneralize sigma (n+q) ng b) sign) ci.ci_cstr_ndecls brs) @@ -1161,7 +1161,7 @@ let rec is_dependent_generalization sigma ng body = | LetIn (na,b,t,c) -> (* We traverse an alias *) is_dependent_generalization sigma ng c - | Case (ci,p,c,brs) -> + | Case (ci,p,iv,c,brs) -> (* We traverse a split *) Array.exists2 (fun q c -> let _,b = decompose_lam_n_decls sigma q c in @@ -1448,7 +1448,7 @@ let compile ~program_mode sigma pb = let rci = Typing.check_allowed_sort !!(pb.env) sigma mind current pred in let ci = make_case_info !!(pb.env) (fst mind) rci pb.casestyle in let pred = nf_betaiota !!(pb.env) sigma pred in - let case = make_case_or_project !!(pb.env) sigma indf ci pred current brvals in + let case = make_case_or_project !!(pb.env) sigma indt ci pred current brvals in let sigma, _ = Typing.type_of !!(pb.env) sigma pred in sigma, { uj_val = applist (case, inst); uj_type = prod_applist sigma typ inst } diff --git a/pretyping/cbv.ml b/pretyping/cbv.ml index b39ec37cd1..b713d7812e 100644 --- a/pretyping/cbv.ml +++ b/pretyping/cbv.ml @@ -75,7 +75,8 @@ type cbv_value = and cbv_stack = | TOP | APP of cbv_value array * cbv_stack - | CASE of constr * constr array * case_info * cbv_value subs * cbv_stack + | CASE of constr * constr array * (constr,Univ.Instance.t) case_invert + * case_info * cbv_value subs * cbv_stack | PROJ of Projection.t * cbv_stack (* les vars pourraient etre des constr, @@ -134,7 +135,7 @@ let rec stack_concat stk1 stk2 = match stk1 with TOP -> stk2 | APP(v,stk1') -> APP(v,stack_concat stk1' stk2) - | CASE(c,b,i,s,stk1') -> CASE(c,b,i,s,stack_concat stk1' stk2) + | CASE(c,b,iv,i,s,stk1') -> CASE(c,b,iv,i,s,stack_concat stk1' stk2) | PROJ (p,stk1') -> PROJ (p,stack_concat stk1' stk2) (* merge stacks when there is no shifts in between *) @@ -339,9 +340,9 @@ let rec reify_stack t = function | TOP -> t | APP (args,st) -> reify_stack (mkApp(t,Array.map reify_value args)) st - | CASE (ty,br,ci,env,st) -> + | CASE (ty,br,iv,ci,env,st) -> reify_stack - (mkCase (ci, ty, t,br)) + (mkCase (ci, ty, iv, t, br)) st | PROJ (p, st) -> reify_stack (mkProj (p, t)) st @@ -400,7 +401,7 @@ let rec norm_head info env t stack = they could be computed when getting out of the stack *) let nargs = Array.map (cbv_stack_term info TOP env) args in norm_head info env head (stack_app nargs stack) - | Case (ci,p,c,v) -> norm_head info env c (CASE(p,v,ci,env,stack)) + | Case (ci,p,iv,c,v) -> norm_head info env c (CASE(p,v,iv,ci,env,stack)) | Cast (ct,_,_) -> norm_head info env ct stack | Proj (p, c) -> @@ -514,14 +515,14 @@ and cbv_stack_value info env = function cbv_stack_term info stk envf redfix (* constructor in a Case -> IOTA *) - | (CONSTR(((sp,n),u),[||]), APP(args,CASE(_,br,ci,env,stk))) + | (CONSTR(((sp,n),u),[||]), APP(args,CASE(_,br,iv,ci,env,stk))) when red_set info.reds fMATCH -> let cargs = Array.sub args ci.ci_npar (Array.length args - ci.ci_npar) in cbv_stack_term info (stack_app cargs stk) env br.(n-1) (* constructor of arity 0 in a Case -> IOTA *) - | (CONSTR(((_,n),u),[||]), CASE(_,br,_,env,stk)) + | (CONSTR(((_,n),u),[||]), CASE(_,br,_,_,env,stk)) when red_set info.reds fMATCH -> cbv_stack_term info stk env br.(n-1) @@ -597,9 +598,9 @@ let rec apply_stack info t = function | TOP -> t | APP (args,st) -> apply_stack info (mkApp(t,Array.map (cbv_norm_value info) args)) st - | CASE (ty,br,ci,env,st) -> + | CASE (ty,br,iv,ci,env,st) -> apply_stack info - (mkCase (ci, cbv_norm_term info env ty, t, + (mkCase (ci, cbv_norm_term info env ty, iv, t, Array.map (cbv_norm_term info env) br)) st | PROJ (p, st) -> diff --git a/pretyping/cbv.mli b/pretyping/cbv.mli index fdd4370613..d7804edf6d 100644 --- a/pretyping/cbv.mli +++ b/pretyping/cbv.mli @@ -41,7 +41,8 @@ type cbv_value = and cbv_stack = | TOP | APP of cbv_value array * cbv_stack - | CASE of constr * constr array * case_info * cbv_value subs * cbv_stack + | CASE of constr * constr array * (constr,Univ.Instance.t) case_invert + * case_info * cbv_value subs * cbv_stack | PROJ of Projection.t * cbv_stack val shift_value : int -> cbv_value -> cbv_value diff --git a/pretyping/constr_matching.ml b/pretyping/constr_matching.ml index 25aa8915ba..656739657d 100644 --- a/pretyping/constr_matching.ml +++ b/pretyping/constr_matching.ml @@ -351,7 +351,7 @@ let matches_core env sigma allow_bound_rels sorec (push_binder na1 na2 t2 ctx) (EConstr.push_rel (LocalDef (na2,c2,t2)) env) (add_binders na1 na2 binding_vars (sorec ctx env subst c1 c2)) d1 d2 - | PIf (a1,b1,b1'), Case (ci,_,a2,[|b2;b2'|]) -> + | PIf (a1,b1,b1'), Case (ci,_,_,a2,[|b2;b2'|]) -> let ctx_b2,b2 = decompose_lam_n_decls sigma ci.ci_cstr_ndecls.(0) b2 in let ctx_b2',b2' = decompose_lam_n_decls sigma ci.ci_cstr_ndecls.(1) b2' in let n = Context.Rel.length ctx_b2 in @@ -367,7 +367,7 @@ let matches_core env sigma allow_bound_rels else raise PatternMatchingFailure - | PCase (ci1,p1,a1,br1), Case (ci2,p2,a2,br2) -> + | PCase (ci1,p1,a1,br1), Case (ci2,p2,_,a2,br2) -> let n2 = Array.length br2 in let () = match ci1.cip_ind with | None -> () @@ -498,9 +498,9 @@ let sub_match ?(closed=true) env sigma pat c = | [app';c] -> mk_ctx (mkApp (app',[|c|])) | _ -> assert false in try_aux [(env, app); (env, Array.last lc)] mk_ctx next - | Case (ci,hd,c1,lc) -> + | Case (ci,hd,iv,c1,lc) -> let next_mk_ctx = function - | c1 :: hd :: lc -> mk_ctx (mkCase (ci,hd,c1,Array.of_list lc)) + | c1 :: hd :: lc -> mk_ctx (mkCase (ci,hd,iv,c1,Array.of_list lc)) | _ -> assert false in let sub = (env, c1) :: (env, hd) :: subargs env lc in diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index 13946208bc..02c04c2300 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -429,7 +429,7 @@ and align_tree nal isgoal (e,c as rhs) sigma = match nal with | [] -> [Id.Set.empty,[],rhs] | na::nal -> match EConstr.kind sigma c with - | Case (ci,p,c,cl) when + | Case (ci,p,iv,c,cl) when eq_constr sigma c (mkRel (List.index Name.equal na (fst (snd e)))) && not (Int.equal (Array.length cl) 0) && (* don't contract if p dependent *) @@ -498,40 +498,46 @@ let it_destRLambda_or_LetIn_names l c = | _ -> DAst.make @@ GApp (c,[a])) in aux l [] c -let detype_case computable detype detype_eqns testdep avoid data p c bl = - let (indsp,st,constagsl,k) = data in +let detype_case computable detype detype_eqns testdep avoid ci p iv c bl = let synth_type = synthetize_type () in let tomatch = detype c in + let tomatch = match iv with + | NoInvert -> tomatch + | CaseInvert {univs;args} -> + let t = mkApp (mkIndU (ci.ci_ind,univs), args) in + DAst.make @@ GCast (tomatch, CastConv (detype t)) + in let alias, aliastyp, pred= if (not !Flags.raw_print) && synth_type && computable && not (Int.equal (Array.length bl) 0) then Anonymous, None, None else let p = detype p in - let nl,typ = it_destRLambda_or_LetIn_names k p in + let nl,typ = it_destRLambda_or_LetIn_names ci.ci_pp_info.ind_tags p in let n,typ = match DAst.get typ with | GLambda (x,_,t,c) -> x, c | _ -> Anonymous, typ in let aliastyp = if List.for_all (Name.equal Anonymous) nl then None - else Some (CAst.make (indsp,nl)) in + else Some (CAst.make (ci.ci_ind,nl)) in n, aliastyp, Some typ in - let constructs = Array.init (Array.length bl) (fun i -> (indsp,i+1)) in - let tag = + let constructs = Array.init (Array.length bl) (fun i -> (ci.ci_ind,i+1)) in + let tag = let st = ci.ci_pp_info.style in try if !Flags.raw_print then RegularStyle else if st == LetPatternStyle then st - else if PrintingLet.active indsp then + else if PrintingLet.active ci.ci_ind then LetStyle - else if PrintingIf.active indsp then + else if PrintingIf.active ci.ci_ind then IfStyle else st with Not_found -> st in + let constagsl = ci.ci_pp_info.cstr_tags in match tag, aliastyp with | LetStyle, None -> let bl' = Array.map detype bl in @@ -793,14 +799,12 @@ and detype_r d flags avoid env sigma t = GRef (GlobRef.IndRef ind_sp, detype_instance sigma u) | Construct (cstr_sp,u) -> GRef (GlobRef.ConstructRef cstr_sp, detype_instance sigma u) - | Case (ci,p,c,bl) -> + | Case (ci,p,iv,c,bl) -> let comp = computable sigma p (List.length (ci.ci_pp_info.ind_tags)) in detype_case comp (detype d flags avoid env sigma) (detype_eqns d flags avoid env sigma ci comp) (is_nondep_branch sigma) avoid - (ci.ci_ind,ci.ci_pp_info.style, - ci.ci_pp_info.cstr_tags,ci.ci_pp_info.ind_tags) - p c bl + ci p iv c bl | Fix (nvn,recdef) -> detype_fix (detype d) flags avoid env sigma nvn recdef | CoFix (n,recdef) -> detype_cofix (detype d) flags avoid env sigma n recdef | Int i -> GInt i diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index 366203faeb..0206d4e70d 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -208,7 +208,7 @@ let occur_rigidly flags env evd (evk,_) t = if rigid_normal_occ b' || rigid_normal_occ t' then Rigid true else Reducible | Rel _ | Var _ -> Reducible - | Case (_,_,c,_) -> + | Case (_,_,_,c,_) -> (match aux c with | Rigid b -> Rigid b | _ -> Reducible) @@ -382,7 +382,7 @@ let ise_stack2 no_app env evd f sk1 sk2 = else None, x in match sk1, sk2 with | [], [] -> None, Success i - | Stack.Case (_,t1,c1)::q1, Stack.Case (_,t2,c2)::q2 -> + | Stack.Case (_,t1,_,c1)::q1, Stack.Case (_,t2,_,c2)::q2 -> (match f env i CONV t1 t2 with | Success i' -> (match ise_array2 i' (fun ii -> f env ii CONV) c1 c2 with @@ -417,7 +417,7 @@ let exact_ise_stack2 env evd f sk1 sk2 = let rec ise_stack2 i sk1 sk2 = match sk1, sk2 with | [], [] -> Success i - | Stack.Case (_,t1,c1)::q1, Stack.Case (_,t2,c2)::q2 -> + | Stack.Case (_,t1,_,c1)::q1, Stack.Case (_,t2,_,c2)::q2 -> ise_and i [ (fun i -> ise_stack2 i q1 q2); (fun i -> ise_array2 i (fun ii -> f env ii CONV) c1 c2); diff --git a/pretyping/heads.ml b/pretyping/heads.ml index 908b8b00d6..98cfbf7fa7 100644 --- a/pretyping/heads.ml +++ b/pretyping/heads.ml @@ -78,7 +78,7 @@ and kind_of_head env t = | App (c,al) -> aux k (Array.to_list al @ l) c b | Proj (p,c) -> RigidHead RigidOther - | Case (_,_,c,_) -> aux k [] c true + | Case (_,_,_,c,_) -> aux k [] c true | Int _ | Float _ -> ConstructorHead | Fix ((i,j),_) -> let n = i.(j) in diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml index 6132365b27..0e7fac35f1 100644 --- a/pretyping/indrec.ml +++ b/pretyping/indrec.ml @@ -119,8 +119,10 @@ let mis_make_case_com dep env sigma (ind, u as pind) (mib,mip as specif) kind = in let obj = match projs with - | None -> mkCase (ci, lift ndepar p, mkRel 1, - Termops.rel_vect ndepar k) + | None -> + let iv = make_case_invert env (find_rectype env sigma (EConstr.of_constr (lift 1 depind))) ci in + let iv = EConstr.Unsafe.to_case_invert iv in + mkCase (ci, lift ndepar p, iv, mkRel 1, Termops.rel_vect ndepar k) | Some ps -> let term = mkApp (mkRel 2, @@ -407,7 +409,8 @@ let mis_make_indrec env sigma ?(force_mutual=false) listdepkind mib u = arsign' in let obj = - Inductiveops.make_case_or_project env !evdref indf ci (EConstr.of_constr pred) + let indty = find_rectype env sigma (EConstr.of_constr depind) in + Inductiveops.make_case_or_project env !evdref indty ci (EConstr.of_constr pred) (EConstr.mkRel 1) (Array.map EConstr.of_constr branches) in let obj = EConstr.to_constr !evdref obj in diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml index e77c5082dd..23145b1629 100644 --- a/pretyping/inductiveops.ml +++ b/pretyping/inductiveops.ml @@ -66,6 +66,8 @@ let relevance_of_inductive_family env ((ind,_),_ : inductive_family) = type inductive_type = IndType of inductive_family * EConstr.constr list +let ind_of_ind_type = function IndType (((ind,_),_),_) -> ind + let make_ind_type (indf, realargs) = IndType (indf,realargs) let dest_ind_type (IndType (indf,realargs)) = (indf,realargs) @@ -332,16 +334,26 @@ let get_constructors env (ind,params) = let get_projections = Environ.get_projections -let make_case_or_project env sigma indf ci pred c branches = +let make_case_invert env (IndType (((ind,u),params),indices)) ci = + if Typeops.should_invert_case env ci + then + let univs = EConstr.EInstance.make u in + let params = Array.map_of_list EConstr.of_constr params in + let args = Array.append params (Array.of_list indices) in + CaseInvert {univs;args} + else NoInvert + +let make_case_or_project env sigma indt ci pred c branches = let open EConstr in - let projs = get_projections env (fst (fst indf)) in + let IndType (((ind,_),_),_) = indt in + let projs = get_projections env ind in match projs with - | None -> (mkCase (ci, pred, c, branches)) + | None -> + mkCase (ci, pred, make_case_invert env indt ci, c, branches) | Some ps -> assert(Array.length branches == 1); let na, ty, t = destLambda sigma pred in let () = - let (ind, _), _ = dest_ind_family indf in let mib, _ = Inductive.lookup_mind_specif env ind in if (* dependent *) not (Vars.noccurn sigma 1 t) && not (has_dependent_elim mib) then diff --git a/pretyping/inductiveops.mli b/pretyping/inductiveops.mli index 2bec86599e..1e2bba9f73 100644 --- a/pretyping/inductiveops.mli +++ b/pretyping/inductiveops.mli @@ -48,6 +48,7 @@ val map_inductive_type : (EConstr.constr -> EConstr.constr) -> inductive_type -> val liftn_inductive_type : int -> int -> inductive_type -> inductive_type val lift_inductive_type : int -> inductive_type -> inductive_type val substnl_ind_type : EConstr.constr list -> int -> inductive_type -> inductive_type +val ind_of_ind_type : inductive_type -> inductive val relevance_of_inductive_type : env -> inductive_type -> Sorts.relevance @@ -204,9 +205,12 @@ val make_case_info : env -> inductive -> Sorts.relevance -> case_style -> case_i Fail with an error if the elimination is dependent while the inductive type does not allow dependent elimination. *) val make_case_or_project : - env -> evar_map -> inductive_family -> case_info -> + env -> evar_map -> inductive_type -> case_info -> (* pred *) EConstr.constr -> (* term *) EConstr.constr -> (* branches *) EConstr.constr array -> EConstr.constr +val make_case_invert : env -> inductive_type -> case_info + -> (EConstr.constr,EConstr.EInstance.t) case_invert + (*i Compatibility val make_default_case_info : env -> case_style -> inductive -> case_info i*) diff --git a/pretyping/nativenorm.ml b/pretyping/nativenorm.ml index d672ddc906..89bd7e196f 100644 --- a/pretyping/nativenorm.ml +++ b/pretyping/nativenorm.ml @@ -317,6 +317,11 @@ and nf_atom_type env sigma atom = | Avar id -> mkVar id, Typeops.type_of_variable env id | Acase(ans,accu,p,bs) -> + let () = if Typeops.should_invert_case env ans.asw_ci then + (* TODO implement case inversion readback (properly reducing + it is a problem for the kernel) *) + CErrors.user_err Pp.(str "Native compute readback of case inversion not implemented.") + in let a,ta = nf_accu_type env sigma accu in let ((mind,_),u as ind),allargs = find_rectype_a env ta in let (mib,mip) = Inductive.lookup_mind_specif env (fst ind) in @@ -338,8 +343,7 @@ and nf_atom_type env sigma atom = in let branchs = Array.mapi mkbranch bsw in let tcase = build_case_type p realargs a in - let ci = ans.asw_ci in - mkCase(ci, p, a, branchs), tcase + mkCase(ans.asw_ci, p, NoInvert, a, branchs), tcase | Afix(tt,ft,rp,s) -> let tt = Array.map (fun t -> nf_type_sort env sigma t) tt in let tt = Array.map fst tt and rt = Array.map snd tt in diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml index 6d30e0338e..4aedeb43e3 100644 --- a/pretyping/patternops.ml +++ b/pretyping/patternops.ml @@ -193,8 +193,8 @@ let pattern_of_constr env sigma t = else PEvar (evk,List.map (pattern_of_constr env) ctxt) | Evar_kinds.MatchingVar (Evar_kinds.SecondOrderPatVar ido) -> assert false | _ -> - PMeta None) - | Case (ci,p,a,br) -> + PMeta None) + | Case (ci,p,_,a,br) -> let cip = { cip_style = ci.ci_pp_info.style; cip_ind = Some ci.ci_ind; diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 1b6c17fcf9..e4403d5bf4 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -991,7 +991,7 @@ struct let pretype tycon env sigma c = eval_pretyper self ~program_mode ~poly resolve_tc tycon env sigma c in let pretype_type tycon env sigma c = eval_type_pretyper self ~program_mode ~poly resolve_tc tycon env sigma c in let sigma, cj = pretype empty_tycon env sigma c in - let (IndType (indf,realargs)) = + let (IndType (indf,realargs)) as indty = try find_rectype !!env sigma cj.uj_type with Not_found -> let cloc = loc_of_glob_constr c in @@ -1028,11 +1028,11 @@ struct let fsign = Context.Rel.map (whd_betaiota !!env sigma) fsign in let hypnaming = if program_mode then ProgramNaming else KeepUserNameAndRenameExistingButSectionNames in let fsign,env_f = push_rel_context ~hypnaming sigma fsign env in - let obj ind rci p v f = + let obj indt rci p v f = if not record then let f = it_mkLambda_or_LetIn f fsign in - let ci = make_case_info !!env (fst ind) rci LetStyle in - mkCase (ci, p, cj.uj_val,[|f|]) + let ci = make_case_info !!env (ind_of_ind_type indt) rci LetStyle in + mkCase (ci, p, make_case_invert !!env indt ci, cj.uj_val,[|f|]) else it_mkLambda_or_LetIn f fsign in (* Make dependencies from arity signature impossible *) @@ -1060,7 +1060,7 @@ struct let v = let ind,_ = dest_ind_family indf in let rci = Typing.check_allowed_sort !!env sigma ind cj.uj_val p in - obj ind rci p cj.uj_val fj.uj_val + obj indty rci p cj.uj_val fj.uj_val in sigma, { uj_val = v; uj_type = (substl (realargs@[cj.uj_val]) ccl) } @@ -1079,7 +1079,7 @@ struct let v = let ind,_ = dest_ind_family indf in let rci = Typing.check_allowed_sort !!env sigma ind cj.uj_val p in - obj ind rci p cj.uj_val fj.uj_val + obj indty rci p cj.uj_val fj.uj_val in sigma, { uj_val = v; uj_type = ccl }) let pretype_cases self (sty, po, tml, eqns) = @@ -1092,7 +1092,7 @@ struct let open Context.Rel.Declaration in let pretype tycon env sigma c = eval_pretyper self ~program_mode ~poly resolve_tc tycon env sigma c in let sigma, cj = pretype empty_tycon env sigma c in - let (IndType (indf,realargs)) = + let (IndType (indf,realargs)) as indty = try find_rectype !!env sigma cj.uj_type with Not_found -> let cloc = loc_of_glob_constr c in @@ -1148,7 +1148,7 @@ struct let pred = nf_evar sigma pred in let rci = Typing.check_allowed_sort !!env sigma ind cj.uj_val pred in let ci = make_case_info !!env (fst ind) rci IfStyle in - mkCase (ci, pred, cj.uj_val, [|b1;b2|]) + mkCase (ci, pred, make_case_invert !!env indty ci, cj.uj_val, [|b1;b2|]) in let cj = { uj_val = v; uj_type = p } in discard_trace @@ inh_conv_coerce_to_tycon ?loc ~program_mode resolve_tc env sigma cj tycon diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index 8ab040b3b1..18a0637efa 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -179,7 +179,7 @@ sig type 'a member = | App of 'a app_node - | Case of case_info * 'a * 'a array + | Case of case_info * 'a * ('a, EInstance.t) case_invert * 'a array | Proj of Projection.t | Fix of ('a, 'a) pfixpoint * 'a t | Primitive of CPrimitives.t * (Constant.t * EInstance.t) * 'a t * CPrimitives.args_red @@ -231,7 +231,7 @@ struct type 'a member = | App of 'a app_node - | Case of case_info * 'a * 'a array + | Case of case_info * 'a * ('a, EInstance.t) case_invert * 'a array | Proj of Projection.t | Fix of ('a, 'a) pfixpoint * 'a t | Primitive of CPrimitives.t * (Constant.t * EInstance.t) * 'a t * CPrimitives.args_red @@ -244,7 +244,7 @@ struct let pr_c x = hov 1 (pr_c x) in match member with | App app -> str "ZApp" ++ pr_app_node pr_c app - | Case (_,_,br) -> + | Case (_,_,_,br) -> str "ZCase(" ++ prvect_with_sep (pr_bar) pr_c br ++ str ")" @@ -285,7 +285,7 @@ struct ([],[]) -> Int.equal bal 0 | (App (i,_,j)::s1, _) -> compare_rec (bal + j + 1 - i) s1 stk2 | (_, App (i,_,j)::s2) -> compare_rec (bal - j - 1 + i) stk1 s2 - | (Case(c1,_,_)::s1, Case(c2,_,_)::s2) -> + | (Case(c1,_,_,_)::s1, Case(c2,_,_,_)::s2) -> Int.equal bal 0 (* && c1.ci_ind = c2.ci_ind *) && compare_rec 0 s1 s2 | (Proj (p)::s1, Proj(p2)::s2) -> Int.equal bal 0 && compare_rec 0 s1 s2 @@ -305,7 +305,7 @@ struct let t1,l1 = decomp_node_last n1 q1 in let t2,l2 = decomp_node_last n2 q2 in aux (f o t1 t2) l1 l2 - | Case (_,t1,a1) :: q1, Case (_,t2,a2) :: q2 -> + | Case (_,t1,_,a1) :: q1, Case (_,t2,_,a2) :: q2 -> aux (Array.fold_left2 f (f o t1 t2) a1 a2) q1 q2 | Proj (p1) :: q1, Proj (p2) :: q2 -> aux o q1 q2 @@ -321,7 +321,8 @@ struct | App (i,a,j) -> let le = j - i + 1 in App (0,Array.map f (Array.sub a i le), le-1) - | Case (info,ty,br) -> Case (info, f ty, Array.map f br) + | Case (info,ty,iv,br) -> + Case (info, f ty, map_invert f iv, Array.map f br) | Fix ((r,(na,ty,bo)),arg) -> Fix ((r,(na,Array.map f ty, Array.map f bo)),map f arg) | Primitive (p,c,args,kargs) -> @@ -403,7 +404,7 @@ struct then a else Array.sub a i (j - i + 1) in zip (mkApp (f, a'), s) - | f, (Case (ci,rt,br)::s) -> zip (mkCase (ci,rt,f,br), s) + | f, (Case (ci,rt,iv,br)::s) -> zip (mkCase (ci,rt,iv,f,br), s) | f, (Fix (fix,st)::s) -> zip (mkFix fix, st @ (append_app [|f|] s)) | f, (Proj (p)::s) -> zip (mkProj (p,f),s) @@ -536,12 +537,13 @@ let reduce_and_refold_cofix recfun env sigma cofix sk = let reduce_mind_case sigma mia = match EConstr.kind sigma mia.mconstr with | Construct ((ind_sp,i),u) -> -(* let ncargs = (fst mia.mci).(i-1) in*) +(* let ncargs = (fst mia.mci).(i-1) in*) let real_cargs = List.skipn mia.mci.ci_npar mia.mcargs in applist (mia.mlf.(i-1),real_cargs) | CoFix cofix -> let cofix_def = contract_cofix sigma cofix in - mkCase (mia.mci, mia.mP, applist(cofix_def,mia.mcargs), mia.mlf) + (* XXX Is NoInvert OK here? *) + mkCase (mia.mci, mia.mP, NoInvert, applist(cofix_def,mia.mcargs), mia.mlf) | _ -> assert false (* contracts fix==FIX[nl;i](A1...Ak;[F1...Fk]{B1....Bk}) to produce @@ -805,8 +807,8 @@ let rec whd_state_gen flags env sigma = | _ -> fold ()) | _ -> fold ()) - | Case (ci,p,d,lf) -> - whrec (d, Stack.Case (ci,p,lf) :: stack) + | Case (ci,p,iv,d,lf) -> + whrec (d, Stack.Case (ci,p,iv,lf) :: stack) | Fix ((ri,n),_ as f) -> (match Stack.strip_n_app ri.(n) stack with @@ -819,7 +821,7 @@ let rec whd_state_gen flags env sigma = let use_fix = CClosure.RedFlags.red_set flags CClosure.RedFlags.fFIX in if use_match || use_fix then match Stack.strip_app stack with - |args, (Stack.Case(ci, _, lf)::s') when use_match -> + |args, (Stack.Case(ci, _, _, lf)::s') when use_match -> whrec (lf.(c-1), (Stack.tail ci.ci_npar args) @ s') |args, (Stack.Proj (p)::s') when use_match -> whrec (Stack.nth args (Projection.npars p + Projection.arg p), s') @@ -901,8 +903,8 @@ let local_whd_state_gen flags _env sigma = | Proj (p,c) when CClosure.RedFlags.red_projection flags p -> (whrec (c, Stack.Proj (p) :: stack)) - | Case (ci,p,d,lf) -> - whrec (d, Stack.Case (ci,p,lf) :: stack) + | Case (ci,p,iv,d,lf) -> + whrec (d, Stack.Case (ci,p,iv,lf) :: stack) | Fix ((ri,n),_ as f) -> (match Stack.strip_n_app ri.(n) stack with @@ -920,7 +922,7 @@ let local_whd_state_gen flags _env sigma = let use_fix = CClosure.RedFlags.red_set flags CClosure.RedFlags.fFIX in if use_match || use_fix then match Stack.strip_app stack with - |args, (Stack.Case(ci, _, lf)::s') when use_match -> + |args, (Stack.Case(ci, _, _, lf)::s') when use_match -> whrec (lf.(c-1), (Stack.tail ci.ci_npar args) @ s') |args, (Stack.Proj (p) :: s') when use_match -> whrec (Stack.nth args (Projection.npars p + Projection.arg p), s') @@ -1035,7 +1037,7 @@ let clos_norm_flags flgs env sigma t = try let evars ev = safe_evar_value sigma ev in EConstr.of_constr (CClosure.norm_val - (CClosure.create_clos_infos ~evars flgs env) + (CClosure.create_clos_infos ~univs:(Evd.universes sigma) ~evars flgs env) (CClosure.create_tab ()) (CClosure.inject (EConstr.Unsafe.to_constr t))) with e when is_anomaly e -> user_err Pp.(str "Tried to normalize ill-typed term") @@ -1044,7 +1046,7 @@ let clos_whd_flags flgs env sigma t = try let evars ev = safe_evar_value sigma ev in EConstr.of_constr (CClosure.whd_val - (CClosure.create_clos_infos ~evars flgs env) + (CClosure.create_clos_infos ~univs:(Evd.universes sigma) ~evars flgs env) (CClosure.create_tab ()) (CClosure.inject (EConstr.Unsafe.to_constr t))) with e when is_anomaly e -> user_err Pp.(str "Tried to normalize ill-typed term") @@ -1148,7 +1150,8 @@ let sigma_check_inductive_instances cv_pb variance u1 u2 sigma = let sigma_univ_state = let open Reduction in - { compare_sorts = sigma_compare_sorts; + { compare_graph = Evd.universes; + compare_sorts = sigma_compare_sorts; compare_instances = sigma_compare_instances; compare_cumul_instances = sigma_check_inductive_instances; } diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli index a0cbd8ccf7..58fff49faa 100644 --- a/pretyping/reductionops.mli +++ b/pretyping/reductionops.mli @@ -58,7 +58,7 @@ module Stack : sig type 'a member = | App of 'a app_node - | Case of case_info * 'a * 'a array + | Case of case_info * 'a * ('a, EInstance.t) case_invert * 'a array | Proj of Projection.t | Fix of ('a, 'a) pfixpoint * 'a t | Primitive of CPrimitives.t * (Constant.t * EInstance.t) * 'a t * CPrimitives.args_red diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml index 5ec5005b3e..bb518bc2f9 100644 --- a/pretyping/retyping.ml +++ b/pretyping/retyping.ml @@ -121,7 +121,7 @@ let retype ?(polyprop=true) sigma = | Evar ev -> existential_type sigma ev | Ind (ind, u) -> EConstr.of_constr (rename_type_of_inductive env (ind, EInstance.kind sigma u)) | Construct (cstr, u) -> EConstr.of_constr (rename_type_of_constructor env (cstr, EInstance.kind sigma u)) - | Case (_,p,c,lf) -> + | Case (_,p,_iv,c,lf) -> let Inductiveops.IndType(indf,realargs) = let t = type_of env c in try Inductiveops.find_rectype env sigma t @@ -297,7 +297,7 @@ let relevance_of_term env sigma c = | Const (c,_) -> Relevanceops.relevance_of_constant env c | Ind _ -> Sorts.Relevant | Construct (c,_) -> Relevanceops.relevance_of_constructor env c - | Case (ci, _, _, _) -> ci.ci_relevance + | Case (ci, _, _, _, _) -> ci.ci_relevance | Fix ((_,i),(lna,_,_)) -> (lna.(i)).binder_relevance | CoFix (i,(lna,_,_)) -> (lna.(i)).binder_relevance | Proj (p, _) -> Relevanceops.relevance_of_projection env p diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml index 5b9bc91b84..baa32565f6 100644 --- a/pretyping/tacred.ml +++ b/pretyping/tacred.ml @@ -277,8 +277,8 @@ let compute_consteval_direct env sigma ref = | Fix fix when not onlyproj -> (try check_fix_reversibility sigma labs l fix with Elimconst -> NotAnElimination) - | Case (_,_,d,_) when isRel sigma d && not onlyproj -> EliminationCases n - | Case (_,_,d,_) -> srec env n labs true d + | Case (_,_,_,d,_) when isRel sigma d && not onlyproj -> EliminationCases n + | Case (_,_,_,d,_) -> srec env n labs true d | Proj (p, d) when isRel sigma d -> EliminationProj n | _ -> NotAnElimination in @@ -538,7 +538,8 @@ let reduce_mind_case_use_function func env sigma mia = fun _ -> None in let cofix_def = contract_cofix_use_function env sigma build_cofix_name cofix in - mkCase (mia.mci, mia.mP, applist(cofix_def,mia.mcargs), mia.mlf) + (* Is NoInvert OK here? *) + mkCase (mia.mci, mia.mP, NoInvert, applist(cofix_def,mia.mcargs), mia.mlf) | _ -> assert false @@ -573,7 +574,7 @@ let match_eval_ref_value env sigma constr stack = env |> lookup_rel n |> RelDecl.get_value |> Option.map (lift n) | _ -> None -let special_red_case env sigma whfun (ci, p, c, lf) = +let special_red_case env sigma whfun (ci, p, iv, c, lf) = let rec redrec s = let (constr, cargs) = whfun s in match match_eval_ref env sigma constr cargs with @@ -619,9 +620,9 @@ let reduce_proj env sigma whfun whfun' c = let proj_narg = Projection.npars proj + Projection.arg proj in List.nth cargs proj_narg | _ -> raise Redelimination) - | Case (n,p,c,brs) -> + | Case (n,p,iv,c,brs) -> let c' = redrec c in - let p = (n,p,c',brs) in + let p = (n,p,iv,c',brs) in (try special_red_case env sigma whfun' p with Redelimination -> mkCase p) | _ -> raise Redelimination @@ -772,9 +773,9 @@ and whd_simpl_stack env sigma = | LetIn (n,b,t,c) -> redrec (applist (Vars.substl [b] c, stack)) | App (f,cl) -> redrec (applist(f, (Array.to_list cl)@stack)) | Cast (c,_,_) -> redrec (applist(c, stack)) - | Case (ci,p,c,lf) -> + | Case (ci,p,iv,c,lf) -> (try - redrec (applist(special_red_case env sigma redrec (ci,p,c,lf), stack)) + redrec (applist(special_red_case env sigma redrec (ci,p,iv,c,lf), stack)) with Redelimination -> s') | Fix fix -> @@ -867,7 +868,7 @@ let try_red_product env sigma c = let open Context.Rel.Declaration in mkProd (x, a, redrec (push_rel (LocalAssum (x, a)) env) b) | LetIn (x,a,b,t) -> redrec env (Vars.subst1 a t) - | Case (ci,p,d,lf) -> simpfun (mkCase (ci,p,redrec env d,lf)) + | Case (ci,p,iv,d,lf) -> simpfun (mkCase (ci,p,iv,redrec env d,lf)) | Proj (p, c) -> let c' = match EConstr.kind sigma c with @@ -1264,10 +1265,10 @@ let one_step_reduce env sigma c = | App (f,cl) -> redrec (f, (Array.to_list cl)@stack) | LetIn (_,f,_,cl) -> (Vars.subst1 f cl,stack) | Cast (c,_,_) -> redrec (c,stack) - | Case (ci,p,c,lf) -> + | Case (ci,p,iv,c,lf) -> (try (special_red_case env sigma (whd_simpl_stack env sigma) - (ci,p,c,lf), stack) + (ci,p,iv,c,lf), stack) with Redelimination -> raise NotStepReducible) | Fix fix -> (try match reduce_fix (whd_construct_stack env) sigma fix stack with diff --git a/pretyping/typing.ml b/pretyping/typing.ml index f0882d4594..b4a1153731 100644 --- a/pretyping/typing.ml +++ b/pretyping/typing.ml @@ -178,7 +178,7 @@ let type_case_branches env sigma (ind,largs) pj c = let ty = whd_betaiota env sigma (lambda_applist_assum sigma (n+1) p (realargs@[c])) in sigma, (lc, ty, Sorts.relevance_of_sort ps) -let judge_of_case env sigma ci pj cj lfj = +let judge_of_case env sigma ci pj iv cj lfj = let ((ind, u), spec) = try find_mrectype env sigma cj.uj_type with Not_found -> error_case_not_inductive env sigma cj in @@ -186,7 +186,10 @@ let judge_of_case env sigma ci pj cj lfj = let sigma, (bty,rslty,rci) = type_case_branches env sigma indspec pj cj.uj_val in let () = check_case_info env (fst indspec) rci ci in let sigma = check_branch_types env sigma (fst indspec) cj (lfj,bty) in - sigma, { uj_val = mkCase (ci, pj.uj_val, cj.uj_val, Array.map j_val lfj); + let () = if (match iv with | NoInvert -> false | CaseInvert _ -> true) != should_invert_case env ci + then Type_errors.error_bad_invert env + in + sigma, { uj_val = mkCase (ci, pj.uj_val, iv, cj.uj_val, Array.map j_val lfj); uj_type = rslty } let check_type_fixpoint ?loc env sigma lna lar vdefj = @@ -361,11 +364,20 @@ let rec execute env sigma cstr = let sigma, ty = type_of_constructor env sigma ctor in sigma, make_judge cstr ty - | Case (ci,p,c,lf) -> + | Case (ci,p,iv,c,lf) -> let sigma, cj = execute env sigma c in let sigma, pj = execute env sigma p in let sigma, lfj = execute_array env sigma lf in - judge_of_case env sigma ci pj cj lfj + let sigma = match iv with + | NoInvert -> sigma + | CaseInvert {univs;args} -> + let t = mkApp (mkIndU (ci.ci_ind,univs), args) in + let sigma, tj = execute env sigma t in + let sigma, tj = type_judgment env sigma tj in + let sigma = Evarconv.unify_leq_delay env sigma cj.uj_type tj.utj_val in + sigma + in + judge_of_case env sigma ci pj iv cj lfj | Fix ((vn,i as vni),recdef) -> let sigma, (_,tys,_ as recdef') = execute_recdef env sigma recdef in diff --git a/pretyping/unification.ml b/pretyping/unification.ml index 95b07e227e..ef58f41489 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -567,7 +567,7 @@ let is_rigid_head sigma flags t = | Construct _ | Int _ | Float _ -> true | Fix _ | CoFix _ -> true | Rel _ | Var _ | Meta _ | Evar _ | Sort _ | Cast (_, _, _) | Prod _ - | Lambda _ | LetIn _ | App (_, _) | Case (_, _, _, _) + | Lambda _ | LetIn _ | App (_, _) | Case (_, _, _, _, _) | Proj (_, _) -> false (* Why aren't Prod, Sort rigid heads ? *) let force_eqs c = @@ -657,7 +657,7 @@ let rec is_neutral env sigma ts t = not (TransparentState.is_transparent_variable ts id) | Rel n -> true | Evar _ | Meta _ -> true - | Case (_, p, c, cl) -> is_neutral env sigma ts c + | Case (_, p, _, c, _) -> is_neutral env sigma ts c | Proj (p, c) -> is_neutral env sigma ts c | Lambda _ | LetIn _ | Construct _ | CoFix _ | Int _ | Float _ -> false | Sort _ | Cast (_, _, _) | Prod (_, _, _) | Ind _ -> false (* Really? *) @@ -847,7 +847,7 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst : subst0) conv_at_top e unify_app_pattern true curenvnb pb opt substn cM f1 l1 cN f2 l2 | _ -> raise ex) - | Case (ci1,p1,c1,cl1), Case (ci2,p2,c2,cl2) -> + | Case (ci1,p1,_,c1,cl1), Case (ci2,p2,_,c2,cl2) -> (try if not (eq_ind ci1.ci_ind ci2.ci_ind) then error_cannot_unify curenv sigma (cM,cN); let opt' = {opt with at_top = true; with_types = false} in @@ -1782,7 +1782,7 @@ let w_unify_to_subterm env evd ?(flags=default_unify_flags ()) (op,cl) = matchrec c1 with ex when precatchable_exception ex -> matchrec c2) - | Case(_,_,c,lf) -> (* does not search in the predicate *) + | Case(_,_,_,c,lf) -> (* does not search in the predicate *) (try matchrec c with ex when precatchable_exception ex -> @@ -1867,7 +1867,7 @@ let w_unify_to_subterm_all env evd ?(flags=default_unify_flags ()) (op,cl) = let c2 = args.(n-1) in bind (matchrec c1) (matchrec c2) - | Case(_,_,c,lf) -> (* does not search in the predicate *) + | Case(_,_,_,c,lf) -> (* does not search in the predicate *) bind (matchrec c) (bind_iter matchrec lf) | Proj (p,c) -> matchrec c diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml index 37c34d55cf..efe1efd74e 100644 --- a/pretyping/vnorm.ml +++ b/pretyping/vnorm.ml @@ -261,6 +261,12 @@ and nf_stk ?from:(from=0) env sigma c t stk = nf_stk env sigma (mkApp(fa,[|c|])) (subst1 c codom) stk | Zswitch sw :: stk -> assert (from = 0) ; + let ci = sw.sw_annot.Vmvalues.ci in + let () = if Typeops.should_invert_case env ci then + (* TODO implement case inversion readback (properly reducing + it is a problem for the kernel) *) + CErrors.user_err Pp.(str "VM compute readback of case inversion not implemented.") + in let ((mind,_ as ind), u), allargs = find_rectype_a env t in let (mib,mip) = Inductive.lookup_mind_specif env ind in let nparams = mib.mind_nparams in @@ -280,8 +286,7 @@ and nf_stk ?from:(from=0) env sigma c t stk = in let branchs = Array.mapi mkbranch bsw in let tcase = build_case_type p realargs c in - let ci = sw.sw_annot.Vmvalues.ci in - nf_stk env sigma (mkCase(ci, p, c, branchs)) tcase stk + nf_stk env sigma (mkCase(ci, p, NoInvert, c, branchs)) tcase stk | Zproj p :: stk -> assert (from = 0) ; let p' = Projection.make p true in diff --git a/printing/printer.ml b/printing/printer.ml index 96213b3b8b..f8413f3588 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -855,10 +855,11 @@ let pr_goal_emacs ~proof gid sid = It is used primarily by the Print Assumptions command. *) type axiom = - | Constant of Constant.t (* An axiom or a constant. *) - | Positive of MutInd.t (* A mutually inductive definition which has been assumed positive. *) - | Guarded of GlobRef.t (* a constant whose (co)fixpoints have been assumed to be guarded *) - | TypeInType of GlobRef.t (* a constant which relies on type in type *) + | Constant of Constant.t + | Positive of MutInd.t + | Guarded of GlobRef.t + | TypeInType of GlobRef.t + | UIP of MutInd.t type context_object = | Variable of Id.t (* A section variable or a Let definition *) @@ -874,14 +875,21 @@ struct let compare_axiom x y = match x,y with | Constant k1 , Constant k2 -> - Constant.CanOrd.compare k1 k2 - | Positive m1 , Positive m2 -> - MutInd.CanOrd.compare m1 m2 - | Guarded k1 , Guarded k2 -> - GlobRef.Ordered.compare k1 k2 - | _ , Constant _ -> 1 - | _ , Positive _ -> 1 - | _ -> -1 + Constant.CanOrd.compare k1 k2 + | Positive m1 , Positive m2 + | UIP m1, UIP m2 -> + MutInd.CanOrd.compare m1 m2 + | Guarded k1 , Guarded k2 + | TypeInType k1, TypeInType k2 -> + GlobRef.Ordered.compare k1 k2 + | Constant _, _ -> -1 + | _, Constant _ -> 1 + | Positive _, _ -> -1 + | _, Positive _ -> 1 + | Guarded _, _ -> -1 + | _, Guarded _ -> 1 + | TypeInType _, _ -> -1 + | _, TypeInType _ -> 1 let compare x y = match x , y with @@ -942,7 +950,9 @@ let pr_assumptionset env sigma s = | Guarded gr -> hov 2 (safe_pr_global env gr ++ spc () ++ strbrk"is assumed to be guarded.") | TypeInType gr -> - hov 2 (safe_pr_global env gr ++ spc () ++ strbrk"relies on an unsafe hierarchy.") + hov 2 (safe_pr_global env gr ++ spc () ++ strbrk"relies on an unsafe hierarchy.") + | UIP mind -> + hov 2 (safe_pr_inductive env mind ++ spc () ++ strbrk"relies on definitional UIP.") in let fold t typ accu = let (v, a, o, tr) = accu in @@ -1021,4 +1031,5 @@ let pr_typing_flags flags = str "check_guarded: " ++ bool flags.check_guarded ++ fnl () ++ str "check_positive: " ++ bool flags.check_positive ++ fnl () ++ str "check_universes: " ++ bool flags.check_universes ++ fnl () - ++ str "cumulative sprop: " ++ bool flags.cumulative_sprop + ++ str "cumulative sprop: " ++ bool flags.cumulative_sprop ++ fnl () + ++ str "definitional uip: " ++ bool flags.allow_uip diff --git a/printing/printer.mli b/printing/printer.mli index 8805819890..a25cbebe91 100644 --- a/printing/printer.mli +++ b/printing/printer.mli @@ -246,6 +246,7 @@ type axiom = | Positive of MutInd.t (* A mutually inductive definition which has been assumed positive. *) | Guarded of GlobRef.t (* a constant whose (co)fixpoints have been assumed to be guarded *) | TypeInType of GlobRef.t (* a constant which relies on type in type *) + | UIP of MutInd.t (* An inductive using the special reduction rule. *) type context_object = | Variable of Id.t (* A section variable or a Let definition *) diff --git a/proofs/clenv.ml b/proofs/clenv.ml index 7fb3a21813..4d148756b4 100644 --- a/proofs/clenv.ml +++ b/proofs/clenv.ml @@ -263,7 +263,7 @@ let meta_reducible_instance env evd b = let rec irec u = let u = whd_betaiota env Evd.empty u (* FIXME *) in match EConstr.kind evd u with - | Case (ci,p,c,bl) when EConstr.isMeta evd (strip_outer_cast evd c) -> + | Case (ci,p,iv,c,bl) when EConstr.isMeta evd (strip_outer_cast evd c) -> let m = destMeta evd (strip_outer_cast evd c) in (match try @@ -272,8 +272,8 @@ let meta_reducible_instance env evd b = if isConstruct evd g || not is_coerce then Some g else None with Not_found -> None with - | Some g -> irec (mkCase (ci,p,g,bl)) - | None -> mkCase (ci,irec p,c,Array.map irec bl)) + | Some g -> irec (mkCase (ci,p,iv,g,bl)) + | None -> mkCase (ci,irec p,iv,c,Array.map irec bl)) | App (f,l) when EConstr.isMeta evd (strip_outer_cast evd f) -> let m = destMeta evd (strip_outer_cast evd f) in (match @@ -621,8 +621,8 @@ let clenv_cast_meta clenv = else mkCast (mkMeta mv, DEFAULTcast, b) with Not_found -> u) | App(f,args) -> mkApp (crec_hd f, Array.map crec args) - | Case(ci,p,c,br) -> - mkCase (ci, crec_hd p, crec_hd c, Array.map crec br) + | Case(ci,p,iv,c,br) -> + mkCase (ci, crec_hd p, map_invert crec_hd iv, crec_hd c, Array.map crec br) | Proj (p, c) -> mkProj (p, crec_hd c) | _ -> u in diff --git a/proofs/logic.ml b/proofs/logic.ml index 07ea2ea572..f159395177 100644 --- a/proofs/logic.ml +++ b/proofs/logic.ml @@ -265,14 +265,15 @@ let collect_meta_variables c = let rec collrec deep acc c = match kind c with | Meta mv -> if deep then error_unsupported_deep_meta () else mv::acc | Cast(c,_,_) -> collrec deep acc c - | Case(ci,p,c,br) -> - (* Hack assuming only two situations: the legacy one that branches, - if with Metas, are Meta, and the new one with eta-let-expanded - branches *) - let br = Array.map2 (fun n b -> try snd (Term.decompose_lam_n_decls n b) with UserError _ -> b) ci.ci_cstr_ndecls br in - Array.fold_left (collrec deep) - (Constr.fold (collrec deep) (Constr.fold (collrec deep) acc p) c) - br + | Case(ci,p,iv,c,br) -> + (* Hack assuming only two situations: the legacy one that branches, + if with Metas, are Meta, and the new one with eta-let-expanded + branches *) + let br = Array.map2 (fun n b -> try snd (Term.decompose_lam_n_decls n b) with UserError _ -> b) ci.ci_cstr_ndecls br in + let acc = Constr.fold (collrec deep) acc p in + let acc = Constr.fold_invert (collrec deep) acc iv in + let acc = Constr.fold (collrec deep) acc c in + Array.fold_left (collrec deep) acc br | App _ -> Constr.fold (collrec deep) acc c | Proj (_, c) -> collrec deep acc c | _ -> Constr.fold (collrec true) acc c @@ -368,14 +369,15 @@ let rec mk_refgoals ~check env sigma goalacc conclty trm = let ty = EConstr.Unsafe.to_constr ty in (acc',ty,sigma,c) - | Case (ci,p,c,lf) -> + | Case (ci,p,iv,c,lf) -> + (* XXX Is ignoring iv OK? *) let (acc',lbrty,conclty',sigma,p',c') = mk_casegoals ~check env sigma goalacc p c in let sigma = check_conv_leq_goal ~check env sigma trm conclty' conclty in let (acc'',sigma,rbranches) = treat_case ~check env sigma ci lbrty lf acc' in let lf' = Array.rev_of_list rbranches in let ans = if p' == p && c' == c && Array.equal (==) lf' lf then trm - else mkCase (ci,p',c',lf') + else mkCase (ci,p',iv,c',lf') in (acc'',conclty',sigma, ans) @@ -416,13 +418,14 @@ and mk_hdgoals ~check env sigma goalacc trm = let ans = if applicand == f && args == l then trm else mkApp (applicand, args) in (acc'',conclty',sigma, ans) - | Case (ci,p,c,lf) -> + | Case (ci,p,iv,c,lf) -> + (* XXX is ignoring iv OK? *) let (acc',lbrty,conclty',sigma,p',c') = mk_casegoals ~check env sigma goalacc p c in let (acc'',sigma,rbranches) = treat_case ~check env sigma ci lbrty lf acc' in let lf' = Array.rev_of_list rbranches in let ans = if p' == p && c' == c && Array.equal (==) lf' lf then trm - else mkCase (ci,p',c',lf') + else mkCase (ci,p',iv,c',lf') in (acc'',conclty',sigma, ans) diff --git a/stm/stm.ml b/stm/stm.ml index 652d064b83..3b7921f638 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -199,16 +199,11 @@ let mkTransTac cast cblock cqueue = let mkTransCmd cast cids ceff cqueue = Cmd { ctac = false; cast; cblock = None; cqueue; cids; ceff } -(* Parts of the system state that are morally part of the proof state *) -let summary_pstate = Evarutil.meta_counter_summary_tag, - Evd.evar_counter_summary_tag, - Declare.Obls.State.prg_tag - type cached_state = | EmptyState - | ParsingState of Vernacstate.Parser.state + | ParsingState of Vernacstate.Parser.t | FullState of Vernacstate.t - | ErrorState of Vernacstate.Parser.state option * Exninfo.iexn + | ErrorState of Vernacstate.Parser.t option * Exninfo.iexn type branch = Vcs_.Branch.t * branch_type Vcs_.branch_info type backup = { mine : branch; others : branch list } @@ -334,7 +329,7 @@ module VCS : sig type vcs = (branch_type, transaction, vcs state_info, box) Vcs_.t - val init : stm_doc_type -> id -> Vernacstate.Parser.state -> doc + val init : stm_doc_type -> id -> Vernacstate.Parser.t -> doc (* val get_type : unit -> stm_doc_type *) val set_ldir : Names.DirPath.t -> unit val get_ldir : unit -> Names.DirPath.t @@ -364,8 +359,8 @@ module VCS : sig val goals : id -> int -> unit val set_state : id -> cached_state -> unit val get_state : id -> cached_state - val set_parsing_state : id -> Vernacstate.Parser.state -> unit - val get_parsing_state : id -> Vernacstate.Parser.state option + val set_parsing_state : id -> Vernacstate.Parser.t -> unit + val get_parsing_state : id -> Vernacstate.Parser.t option val get_proof_mode : id -> Pvernac.proof_mode option (* cuts from start -> stop, raising Expired if some nodes are not there *) @@ -678,7 +673,7 @@ end = struct (* {{{ *) { info with state = EmptyState; vcs_backup = None,None } in let make_shallow = function - | FullState st -> FullState (Vernacstate.make_shallow st) + | FullState st -> FullState (Vernacstate.Stm.make_shallow st) | x -> x in let copy_info_w_state v id = @@ -870,22 +865,13 @@ end = struct (* {{{ *) let invalidate_cur_state () = cur_id := Stateid.dummy - type proof_part = - Vernacstate.LemmaStack.t option * - int * (* Evarutil.meta_counter_summary_tag *) - int * (* Evd.evar_counter_summary_tag *) - Declare.Obls.State.t + type proof_part = Vernacstate.Stm.pstate type partial_state = [ `Full of Vernacstate.t | `ProofOnly of Stateid.t * proof_part ] - let proof_part_of_frozen { Vernacstate.lemmas; system } = - let st = States.summary_of_state system in - lemmas, - Summary.project_from_summary st Util.(pi1 summary_pstate), - Summary.project_from_summary st Util.(pi2 summary_pstate), - Summary.project_from_summary st Util.(pi3 summary_pstate) + let proof_part_of_frozen st = Vernacstate.Stm.pstate st let cache_state ~marshallable id = VCS.set_state id (FullState (Vernacstate.freeze_interp_state ~marshallable)) @@ -952,21 +938,10 @@ end = struct (* {{{ *) else s with VCS.Expired -> s in VCS.set_state id (FullState s) - | `ProofOnly(ontop,(pstate,c1,c2,c3)) -> + | `ProofOnly(ontop,pstate) -> if is_cached_and_valid ontop then let s = get_cached ontop in - let s = { s with lemmas = - PG_compat.copy_terminators ~src:s.lemmas ~tgt:pstate } in - let s = { s with system = - States.replace_summary s.system - begin - let st = States.summary_of_state s.system in - let st = Summary.modify_summary st Util.(pi1 summary_pstate) c1 in - let st = Summary.modify_summary st Util.(pi2 summary_pstate) c2 in - let st = Summary.modify_summary st Util.(pi3 summary_pstate) c3 in - st - end - } in + let s = Vernacstate.Stm.set_pstate s pstate in VCS.set_state id (FullState s) with VCS.Expired -> () @@ -978,12 +953,7 @@ end = struct (* {{{ *) execution_error ?loc id (iprint (e, info)); (e, Stateid.add info ~valid id) - let same_env { Vernacstate.system = s1 } { Vernacstate.system = s2 } = - let s1 = States.summary_of_state s1 in - let e1 = Summary.project_from_summary s1 Global.global_env_summary_tag in - let s2 = States.summary_of_state s2 in - let e2 = Summary.project_from_summary s2 Global.global_env_summary_tag in - e1 == e2 + let same_env = Vernacstate.Stm.same_env (* [define] puts the system in state [id] calling [f ()] *) (* [safe_id] is the last known valid state before execution *) @@ -2373,21 +2343,16 @@ let known_state ~doc ?(redefine_qed=false) ~cache id = (* ugly functions to process nested lemmas, i.e. hard to reproduce * side effects *) - let cherry_pick_non_pstate () = - let st = Summary.freeze_summaries ~marshallable:false in - let st = Summary.remove_from_summary st Util.(pi1 summary_pstate) in - let st = Summary.remove_from_summary st Util.(pi2 summary_pstate) in - let st = Summary.remove_from_summary st Util.(pi3 summary_pstate) in - st, Lib.freeze () in - let inject_non_pstate (s,l) = Summary.unfreeze_summaries ~partial:true s; Lib.unfreeze l; update_global_env () in + let rec pure_cherry_pick_non_pstate safe_id id = State.purify (fun id -> stm_prerr_endline (fun () -> "cherry-pick non pstate " ^ Stateid.to_string id); reach ~safe_id id; - cherry_pick_non_pstate ()) + let st = Vernacstate.freeze_interp_state ~marshallable:false in + Vernacstate.Stm.non_pstate st) id (* traverses the dag backward from nodes being already calculated *) diff --git a/tactics/btermdn.ml b/tactics/btermdn.ml index 6e6af42010..3bed329d31 100644 --- a/tactics/btermdn.ml +++ b/tactics/btermdn.ml @@ -77,7 +77,7 @@ let constr_val_discr_st sigma ts t = | Const (c,u) -> if TransparentState.is_transparent_constant ts c then Everything else Label(GRLabel (ConstRef c),l) | Ind (ind_sp,u) -> Label(GRLabel (IndRef ind_sp),l) | Construct (cstr_sp,u) -> Label(GRLabel (ConstructRef cstr_sp),l) - | Var id when not (TransparentState.is_transparent_variable ts id) -> Label(GRLabel (VarRef id),l) + | Var id -> if TransparentState.is_transparent_variable ts id then Everything else Label(GRLabel (VarRef id),l) | Prod (n, d, c) -> Label(ProdLabel, [d; c]) | Lambda (n, d, c) -> if List.is_empty l then @@ -85,7 +85,8 @@ let constr_val_discr_st sigma ts t = else Everything | Sort _ -> Label(SortLabel, []) | Evar _ -> Everything - | _ -> Nothing + | Rel _ | Meta _ | Cast _ | LetIn _ | App _ | Case _ | Fix _ | CoFix _ + | Proj _ | Int _ | Float _ -> Nothing let constr_pat_discr_st ts t = let open GlobRef in diff --git a/tactics/cbn.ml b/tactics/cbn.ml index 21e38df6db..74f793cdfb 100644 --- a/tactics/cbn.ml +++ b/tactics/cbn.ml @@ -106,7 +106,7 @@ sig type 'a member = | App of 'a app_node - | Case of case_info * 'a * 'a array * Cst_stack.t + | Case of case_info * 'a * ('a, EInstance.t) case_invert * 'a array * Cst_stack.t | Proj of Projection.t * Cst_stack.t | Fix of ('a, 'a) pfixpoint * 'a t * Cst_stack.t | Primitive of CPrimitives.t * (Constant.t * EInstance.t) * 'a t * CPrimitives.args_red * Cst_stack.t @@ -158,7 +158,7 @@ struct type 'a member = | App of 'a app_node - | Case of case_info * 'a * 'a array * Cst_stack.t + | Case of case_info * 'a * ('a, EInstance.t) case_invert * 'a array * Cst_stack.t | Proj of Projection.t * Cst_stack.t | Fix of ('a, 'a) pfixpoint * 'a t * Cst_stack.t | Primitive of CPrimitives.t * (Constant.t * EInstance.t) * 'a t * CPrimitives.args_red * Cst_stack.t @@ -172,7 +172,7 @@ struct let pr_c x = hov 1 (pr_c x) in match member with | App app -> str "ZApp" ++ pr_app_node pr_c app - | Case (_,_,br,cst) -> + | Case (_,_,_,br,cst) -> str "ZCase(" ++ prvect_with_sep (pr_bar) pr_c br ++ str ")" @@ -236,7 +236,7 @@ struct let t1,s1' = decomp_node_last a1 s1 in let t2,s2' = decomp_node_last a2 s2 in (f t1 t2) && (equal_rec s1' s2') - | Case (_,t1,a1,_) :: s1, Case (_,t2,a2,_) :: s2 -> + | Case (_,t1,_,a1,_) :: s1, Case (_,t2,_,a2,_) :: s2 -> f t1 t2 && CArray.equal (fun x y -> f x y) a1 a2 && equal_rec s1 s2 | (Proj (p,_)::s1, Proj(p2,_)::s2) -> Projection.Repr.equal (Projection.repr p) (Projection.repr p2) @@ -284,7 +284,7 @@ struct let will_expose_iota args = List.exists - (function (Fix (_,_,l) | Case (_,_,_,l) | + (function (Fix (_,_,l) | Case (_,_,_,_,l) | Proj (_,l) | Cst (_,_,_,_,l)) when Cst_stack.is_empty l -> true | _ -> false) args @@ -346,9 +346,9 @@ struct then a else Array.sub a i (j - i + 1) in zip (mkApp (f, a'), s) - | f, (Case (ci,rt,br,cst_l)::s) when refold -> - zip (best_state sigma (mkCase (ci,rt,f,br), s) cst_l) - | f, (Case (ci,rt,br,_)::s) -> zip (mkCase (ci,rt,f,br), s) + | f, (Case (ci,rt,iv,br,cst_l)::s) when refold -> + zip (best_state sigma (mkCase (ci,rt,iv,f,br), s) cst_l) + | f, (Case (ci,rt,iv,br,_)::s) -> zip (mkCase (ci,rt,iv,f,br), s) | f, (Fix (fix,st,cst_l)::s) when refold -> zip (best_state sigma (mkFix fix, st @ (append_app [|f|] s)) cst_l) | f, (Fix (fix,st,_)::s) -> zip @@ -699,8 +699,8 @@ let rec whd_state_gen ?csts ~refold ~tactic_mode flags env sigma = | _ -> fold ()) | _ -> fold ()) - | Case (ci,p,d,lf) -> - whrec Cst_stack.empty (d, Stack.Case (ci,p,lf,cst_l) :: stack) + | Case (ci,p,iv,d,lf) -> + whrec Cst_stack.empty (d, Stack.Case (ci,p,iv,lf,cst_l) :: stack) | Fix ((ri,n),_ as f) -> (match Stack.strip_n_app ri.(n) stack with @@ -713,7 +713,7 @@ let rec whd_state_gen ?csts ~refold ~tactic_mode flags env sigma = let use_fix = CClosure.RedFlags.red_set flags CClosure.RedFlags.fFIX in if use_match || use_fix then match Stack.strip_app stack with - |args, (Stack.Case(ci, _, lf,_)::s') when use_match -> + |args, (Stack.Case(ci, _, _, lf,_)::s') when use_match -> whrec Cst_stack.empty (lf.(c-1), (Stack.tail ci.ci_npar args) @ s') |args, (Stack.Proj (p,_)::s') when use_match -> whrec Cst_stack.empty (Stack.nth args (Projection.npars p + Projection.arg p), s') diff --git a/tactics/eqschemes.ml b/tactics/eqschemes.ml index 6da2248cc3..955a7957bf 100644 --- a/tactics/eqschemes.ml +++ b/tactics/eqschemes.ml @@ -221,6 +221,7 @@ let build_sym_scheme env ind = [Context.Rel.to_extended_vect mkRel (3*nrealargs+2) paramsctxt1; rel_vect 1 nrealargs; rel_vect (2*nrealargs+2) nrealargs])), + NoInvert, mkRel 1 (* varH *), [|cstr (nrealargs+1)|])))) in c, UState.of_context_set ctx @@ -295,6 +296,7 @@ let build_sym_involutive_scheme env ind = rel_vect 1 nrealargs; [|mkRel 1|]])|]]); mkRel 1|])), + NoInvert, mkRel 1 (* varH *), [|mkApp(eqrefl,[|applied_ind_C;cstr (nrealargs+1)|])|])))) in (c, UState.of_context_set ctx) @@ -434,9 +436,11 @@ let build_l2r_rew_scheme dep env ind kind = [|mkRel 2|]])|]]) in let main_body = mkCase (ci, - my_it_mkLambda_or_LetIn_name realsign_ind_G applied_PG, - applied_sym_C 3, - [|mkVar varHC|]) in + my_it_mkLambda_or_LetIn_name realsign_ind_G applied_PG, + NoInvert, + applied_sym_C 3, + [|mkVar varHC|]) + in let c = (my_it_mkLambda_or_LetIn paramsctxt (my_it_mkLambda_or_LetIn_name realsign @@ -444,12 +448,13 @@ let build_l2r_rew_scheme dep env ind kind = (my_it_mkProd_or_LetIn (if dep then realsign_ind_P else realsign_P) s) (mkNamedLambda (make_annot varHC indr) applied_PC (mkNamedLambda (make_annot varH indr) (lift 2 applied_ind) - (if dep then (* we need a coercion *) + (if dep then (* we need a coercion *) mkCase (cieq, mkLambda (make_annot (Name varH) indr,lift 3 applied_ind, mkLambda (make_annot Anonymous indr, mkApp (eq,[|lift 4 applied_ind;applied_sym_sym;mkRel 1|]), applied_PR)), + NoInvert, mkApp (sym_involutive, Array.append (Context.Rel.to_extended_vect mkRel 3 mip.mind_arity_ctxt) [|mkVar varH|]), [|main_body|]) @@ -540,6 +545,7 @@ let build_l2r_forward_rew_scheme dep env ind kind = (my_it_mkProd_or_LetIn (if dep then realsign_ind_P 2 applied_ind_P else realsign_P 2) s) (mkNamedProd (make_annot varHC indr) applied_PC applied_PG)), + NoInvert, (mkVar varH), [|mkNamedLambda (make_annot varP indr) (my_it_mkProd_or_LetIn @@ -616,6 +622,7 @@ let build_r2l_forward_rew_scheme dep env ind kind = my_it_mkLambda_or_LetIn_name (lift_rel_context (nrealargs+3) realsign_ind) (mkArrow applied_PG indr (lift (2*nrealargs+5) applied_PC)), + NoInvert, mkRel 3 (* varH *), [|mkLambda (make_annot (Name varHC) indr, @@ -830,6 +837,7 @@ let build_congr env (eq,refl,ctx) ind = [|mkVar varB; mkApp (mkVar varf, [|lift (2*mip.mind_nrealdecls+4) b|]); mkApp (mkVar varf, [|mkRel (mip.mind_nrealargs - i + 2)|])|]))), + NoInvert, mkVar varH, [|mkApp (refl, [|mkVar varB; diff --git a/tactics/equality.ml b/tactics/equality.ml index 3aa7626aaa..a2325b69cc 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -877,7 +877,7 @@ let injectable env sigma ~keep_proofs t1 t2 = *) let descend_then env sigma head dirn = - let IndType (indf,_) = + let IndType (indf,_) as indt = try find_rectype env sigma (get_type_of env sigma head) with Not_found -> user_err Pp.(str "Cannot project on an inductive type derived from a dependency.") @@ -904,7 +904,7 @@ let descend_then env sigma head dirn = (List.interval 1 (Array.length mip.mind_consnames)) in let rci = Sorts.Relevant in (* TODO relevance *) let ci = make_case_info env ind rci RegularStyle in - Inductiveops.make_case_or_project env sigma indf ci p head (Array.of_list brl))) + Inductiveops.make_case_or_project env sigma indt ci p head (Array.of_list brl))) (* Now we need to construct the discriminator, given a discriminable position. This boils down to: @@ -924,7 +924,7 @@ let descend_then env sigma head dirn = branch giving [special], and all the rest giving [default]. *) let build_selector env sigma dirn c ind special default = - let IndType(indf,_) = + let IndType(indf,_) as indt = try find_rectype env sigma ind with Not_found -> (* one can find Rel(k) in case of dependent constructors @@ -950,7 +950,7 @@ let build_selector env sigma dirn c ind special default = List.map build_branch(List.interval 1 (Array.length mip.mind_consnames)) in let rci = Sorts.Relevant in (* TODO relevance *) let ci = make_case_info env ind rci RegularStyle in - let ans = Inductiveops.make_case_or_project env sigma indf ci p c (Array.of_list brl) in + let ans = Inductiveops.make_case_or_project env sigma indt ci p c (Array.of_list brl) in ans let build_coq_False () = pf_constr_of_global (lib_ref "core.False.type") diff --git a/tactics/hints.ml b/tactics/hints.ml index 7a5615dd8e..386224824f 100644 --- a/tactics/hints.ml +++ b/tactics/hints.ml @@ -562,7 +562,7 @@ struct let head_evar sigma c = let rec hrec c = match EConstr.kind sigma c with | Evar (evk,_) -> evk - | Case (_,_,c,_) -> hrec c + | Case (_,_,_,c,_) -> hrec c | App (c,_) -> hrec c | Cast (c,_,_) -> hrec c | Proj (p, c) -> hrec c diff --git a/tactics/term_dnet.ml b/tactics/term_dnet.ml index 553eb903fa..0f76fdda79 100644 --- a/tactics/term_dnet.ml +++ b/tactics/term_dnet.ml @@ -315,7 +315,7 @@ struct meta in Meta meta - | Case (ci,c1,c2,ca) -> + | Case (ci,c1,_iv,c2,ca) -> Term(DCase(ci,pat_of_constr c1,pat_of_constr c2,Array.map pat_of_constr ca)) | Fix ((ia,i),(_,ta,ca)) -> Term(DFix(ia,i,Array.map pat_of_constr ta, Array.map pat_of_constr ca)) diff --git a/test-suite/bugs/closed/bug_11121.v b/test-suite/bugs/closed/bug_11121.v new file mode 100644 index 0000000000..6112a443ab --- /dev/null +++ b/test-suite/bugs/closed/bug_11121.v @@ -0,0 +1,21 @@ +Declare Custom Entry example. + +Module M1. +Fixpoint stupid (x : nat) : nat := 1. +Reserved Notation " x '==' 1 " (in custom example at level 0, x constr). +Notation " x '==' 1" := (stupid x) (in custom example). +End M1. + +Module M2. +Fixpoint stupid (x : nat) : nat := 1. +Notation " x '==' 1" := (stupid x) (in custom example at level 0). +Fail Notation " x '==' 1" := (stupid x) (in custom example at level 1). +End M2. + +Module M3. +Reserved Notation " x '==' 1 " (in custom example at level 55, x constr). + +Fixpoint stupid (x : nat) : nat := 1 +where " x '==' 1" := (stupid x) (in custom example). + +End M3. diff --git a/test-suite/bugs/closed/bug_12571.v b/test-suite/bugs/closed/bug_12571.v new file mode 100644 index 0000000000..c348626921 --- /dev/null +++ b/test-suite/bugs/closed/bug_12571.v @@ -0,0 +1,20 @@ +Axiom IsTrunc : Type -> Type. + +Existing Class IsTrunc. + +Declare Instance trunc_forall : + forall (A : Type) (P : A -> Type), + IsTrunc (forall a : A, P a). + +Axiom Graph : Set. +Axiom in_N : forall (n : Graph), Type. + +Definition N : Type := @sigT Graph in_N. + +Goal forall (P : N -> Type) + (Q := fun m : Graph => forall mrec : in_N m, P (existT _ m mrec)) + (A : Graph), IsTrunc (Q A). +Proof. +intros. +solve [typeclasses eauto]. +Qed. diff --git a/test-suite/failure/uip_loop.v b/test-suite/failure/uip_loop.v new file mode 100644 index 0000000000..5b4a88e7cc --- /dev/null +++ b/test-suite/failure/uip_loop.v @@ -0,0 +1,24 @@ +Set Definitional UIP. + +Inductive seq {A} (a:A) : A -> SProp := + srefl : seq a a. +Arguments srefl {_ _}. + +(* Axiom implied by propext (so consistent) *) +Axiom all_eq : forall (P Q:Prop), P -> Q -> seq P Q. + +Definition transport (P Q:Prop) (x:P) (y:Q) : Q + := match all_eq P Q x y with srefl => x end. + +Definition top : Prop := forall P : Prop, P -> P. + +Definition c : top := + fun P p => + transport + (top -> top) + P + (fun x : top => x (top -> top) (fun x => x) x) + p. + +Fail Timeout 1 Eval lazy in c (top -> top) (fun x => x) c. +(* loops *) diff --git a/test-suite/ltac2/syntax.v b/test-suite/ltac2/syntax.v new file mode 100644 index 0000000000..872b2142d0 --- /dev/null +++ b/test-suite/ltac2/syntax.v @@ -0,0 +1,12 @@ +Require Import Ltac2.Ltac2. + +Ltac2 Type ('a, 'b, 'c) t. +Ltac2 Type ('a) u. +Ltac2 Type 'a v. + +Ltac2 foo + (f : ('a, 'b, 'c) t -> ('a -> 'a, 'b -> 'c, 'c * 'c) t) + (x : ('a, 'b, 'c) t) := + f x. + +Ltac2 bar (x : 'a u) (y : ('b) v) := x. diff --git a/test-suite/output/PrintAssumptions.out b/test-suite/output/PrintAssumptions.out index ca4858d7a7..ba316ceb64 100644 --- a/test-suite/output/PrintAssumptions.out +++ b/test-suite/output/PrintAssumptions.out @@ -7,6 +7,8 @@ bli : Type Axioms: bli : Type Axioms: +@seq relies on definitional UIP. +Axioms: extensionality : forall (P Q : Type) (f g : P -> Q), (forall x : P, f x = g x) -> f = g Axioms: diff --git a/test-suite/output/PrintAssumptions.v b/test-suite/output/PrintAssumptions.v index 4c980fddba..71e642519c 100644 --- a/test-suite/output/PrintAssumptions.v +++ b/test-suite/output/PrintAssumptions.v @@ -45,6 +45,32 @@ Module Poly. End Poly. +Module UIP. + Set Definitional UIP. + + Inductive seq {A} (a:A) : A -> SProp := + srefl : seq a a. + Arguments srefl {_ _}. + + Definition eq_to_seq {A x y} (e:x = y :> A) : seq x y + := match e with eq_refl => srefl end. + Definition seq_to_eq {A x y} (e:seq x y) : x = y :> A + := match e with srefl => eq_refl end. + + Definition norm {A x y} (e:x = y :> A) : x = y + := seq_to_eq (eq_to_seq e). + + Definition norm_id {A x y} (e:x = y :> A) : norm e = e + := match e with eq_refl => eq_refl end. + + Theorem UIP {A x y} (e e':x = y :> A) : e = e'. + Proof. + rewrite <-(norm_id e), <-(norm_id e'). + reflexivity. + Defined. + + Print Assumptions UIP. +End UIP. (* The original test-case of the bug-report *) diff --git a/test-suite/success/sprop.v b/test-suite/success/sprop.v index 268c1880d2..d3e2749088 100644 --- a/test-suite/success/sprop.v +++ b/test-suite/success/sprop.v @@ -112,6 +112,7 @@ Inductive Istrue : bool -> SProp := istrue : Istrue true. Definition Istrue_sym (b:bool) := if b then sUnit else sEmpty. Definition Istrue_to_sym b (i:Istrue b) : Istrue_sym b := match i with istrue => stt end. +(* We don't need primitive elimination to relevant types for this *) Definition Istrue_rec (P:forall b, Istrue b -> Set) (H:P true istrue) b (i:Istrue b) : P b i. Proof. destruct b. diff --git a/test-suite/success/sprop_uip.v b/test-suite/success/sprop_uip.v new file mode 100644 index 0000000000..508cc2be7d --- /dev/null +++ b/test-suite/success/sprop_uip.v @@ -0,0 +1,101 @@ + +Set Allow StrictProp. +Set Definitional UIP. + +Set Warnings "+bad-relevance". + +(** Case inversion, conversion and universe polymorphism. *) +Set Universe Polymorphism. +Inductive IsTy@{i j} : Type@{j} -> SProp := + isty : IsTy Type@{i}. + +Definition IsTy_rec_red@{i j+} (P:forall T : Type@{j}, IsTy@{i j} T -> Set) + v (e:IsTy@{i j} Type@{i}) + : IsTy_rec P v _ e = v + := eq_refl. + + +(** Identity! Currently we have UIP. *) +Inductive seq {A} (a:A) : A -> SProp := + srefl : seq a a. + +Definition transport {A} (P:A -> Type) {x y} (e:seq x y) (v:P x) : P y := + match e with + srefl _ => v + end. + +Definition transport_refl {A} (P:A -> Type) {x} (e:seq x x) v + : transport P e v = v + := @eq_refl (P x) v. + +Definition id_unit (x : unit) := x. +Definition transport_refl_id {A} (P : A -> Type) {x : A} (u : P x) + : P (transport (fun _ => A) (srefl _ : seq (id_unit tt) tt) x) + := u. + +(** We don't ALWAYS reduce (this uses a constant transport so that the + equation is well-typed) *) +Fail Definition transport_block A B (x y:A) (e:seq x y) v + : transport (fun _ => B) e v = v + := @eq_refl B v. + +Inductive sBox (A:SProp) : Prop + := sbox : A -> sBox A. + +Definition transport_refl_box (A:SProp) P (x y:A) (e:seq (sbox A x) (sbox A y)) v + : transport P e v = v + := eq_refl. + +(** TODO? add tests for binders which aren't lambda. *) +Definition transport_box := + Eval lazy in (fun (A:SProp) P (x y:A) (e:seq (sbox A x) (sbox A y)) v => + transport P e v). + +Lemma transport_box_ok : transport_box = fun A P x y e v => v. +Proof. + unfold transport_box. + match goal with |- ?x = ?x => reflexivity end. +Qed. + +(** Play with UIP *) +Lemma of_seq {A:Type} {x y:A} (p:seq x y) : x = y. +Proof. + destruct p. reflexivity. +Defined. + +Lemma to_seq {A:Type} {x y:A} (p: x = y) : seq x y. +Proof. + destruct p. reflexivity. +Defined. + +Lemma eq_srec (A:Type) (x y:A) (P:x=y->Type) : (forall e : seq x y, P (of_seq e)) -> forall e, P e. +Proof. + intros H e. destruct e. + apply (H (srefl _)). +Defined. + +Lemma K : forall {A x} (p:x=x:>A), p = eq_refl. +Proof. + intros A x. apply eq_srec. intros;reflexivity. +Defined. + +Definition K_refl : forall {A x}, @K A x eq_refl = eq_refl + := fun A x => eq_refl. + +Section funext. + + Variable sfunext : forall {A B} (f g : A -> B), (forall x, seq (f x) (g x)) -> seq f g. + + Lemma funext {A B} (f g : A -> B) (H:forall x, (f x) = (g x)) : f = g. + Proof. + apply of_seq,sfunext;intros x;apply to_seq,H. + Defined. + + Definition funext_refl A B (f : A -> B) : funext f f (fun x => eq_refl) = eq_refl + := eq_refl. +End funext. + +(* check that extraction doesn't fall apart on matches with special reduction *) +Require Extraction. + +Extraction seq_rect. diff --git a/theories/Logic/StrictProp.v b/theories/Logic/StrictProp.v index af97b60ee6..b12867ad4e 100644 --- a/theories/Logic/StrictProp.v +++ b/theories/Logic/StrictProp.v @@ -23,9 +23,6 @@ Arguments squash {_} _. Inductive sEmpty : SProp :=. Inductive sUnit : SProp := stt. -Definition sUnit_rect (P:sUnit -> Type) (v:P stt) (u:sUnit) : P u := v. -Definition sUnit_rec (P:sUnit -> Set) (v:P stt) (u:sUnit) : P u := v. -Definition sUnit_ind (P:sUnit -> Prop) (v:P stt) (u:sUnit) : P u := v. Set Primitive Projections. Record Ssig {A:Type} (P:A->SProp) := Sexists { Spr1 : A; Spr2 : P Spr1 }. diff --git a/tools/CoqMakefile.in b/tools/CoqMakefile.in index 9097195721..0086516785 100644 --- a/tools/CoqMakefile.in +++ b/tools/CoqMakefile.in @@ -467,7 +467,7 @@ vok: $(VOFILES:%.vo=%.vok) .PHONY: vok validate: $(VOFILES) - $(TIMER) $(COQCHK) $(COQCHKFLAGS) $(COQLIBS) $^ + $(TIMER) $(COQCHK) $(COQCHKFLAGS) $(COQLIBS_NOML) $^ .PHONY: validate only: $(TGTS) diff --git a/tools/coqdep.ml b/tools/coqdep.ml index 20ffdfe81d..2177da0c75 100644 --- a/tools/coqdep.ml +++ b/tools/coqdep.ml @@ -35,9 +35,7 @@ let usage () = eprintf " -sort : output the given file name ordered by dependencies\n"; eprintf " -noglob | -no-glob : \n"; eprintf " -f file : read -I, -Q, -R and filenames from _CoqProject-formatted FILE."; - eprintf " -I dir -as logname : add (non recursively) dir to coq load path under logical name logname\n"; eprintf " -I dir : add (non recursively) dir to ocaml path\n"; - eprintf " -R dir -as logname : add and import dir recursively to coq load path under logical name logname\n"; (* deprecate? *) eprintf " -R dir logname : add and import dir recursively to coq load path under logical name logname\n"; eprintf " -Q dir logname : add (recursively) and open (non recursively) dir to coq load path under logical name logname\n"; eprintf " -vos : also output dependencies about .vos files\n"; diff --git a/toplevel/coqc.ml b/toplevel/coqc.ml index c6bb38e005..03c53d6991 100644 --- a/toplevel/coqc.ml +++ b/toplevel/coqc.ml @@ -11,7 +11,7 @@ let outputstate opts = Option.iter (fun ostate_file -> let fname = CUnix.make_suffix ostate_file ".coq" in - Library.extern_state fname) opts.Coqcargs.outputstate + Vernacstate.System.dump fname) opts.Coqcargs.outputstate let coqc_init _copts ~opts = Flags.quiet := true; diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index 2d450d430a..4231915be1 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -52,7 +52,7 @@ let print_memory_stat () = let inputstate opts = Option.iter (fun istate_file -> let fname = Loadpath.locate_file (CUnix.make_suffix istate_file ".coq") in - Library.intern_state fname) opts.inputstate + Vernacstate.System.load fname) opts.inputstate (******************************************************************************) (* Fatal Errors *) diff --git a/user-contrib/Ltac2/Constr.v b/user-contrib/Ltac2/Constr.v index 94d468e640..4023b5a277 100644 --- a/user-contrib/Ltac2/Constr.v +++ b/user-contrib/Ltac2/Constr.v @@ -22,6 +22,11 @@ Module Unsafe. Ltac2 Type case. +Ltac2 Type case_invert := [ +| NoInvert +| CaseInvert (instance,constr array) +]. + Ltac2 Type kind := [ | Rel (int) | Var (ident) @@ -36,7 +41,7 @@ Ltac2 Type kind := [ | Constant (constant, instance) | Ind (inductive, instance) | Constructor (constructor, instance) -| Case (case, constr, constr, constr array) +| Case (case, constr, case_invert, constr, constr array) | Fix (int array, int, binder array, constr array) | CoFix (int, binder array, constr array) | Proj (projection, constr) diff --git a/user-contrib/Ltac2/g_ltac2.mlg b/user-contrib/Ltac2/g_ltac2.mlg index 3af39ec59a..bec9632e84 100644 --- a/user-contrib/Ltac2/g_ltac2.mlg +++ b/user-contrib/Ltac2/g_ltac2.mlg @@ -262,12 +262,16 @@ GRAMMAR EXTEND Gram | "1" LEFTA [ t = SELF; qid = Prim.qualid -> { CAst.make ~loc @@ CTypRef (RelId qid, [t]) } ] | "0" - [ "("; t = tac2type LEVEL "5"; ")" -> { t } + [ "("; p = LIST1 tac2type LEVEL "5" SEP ","; ")"; qid = OPT Prim.qualid -> + { match p, qid with + | [t], None -> t + | _, None -> CErrors.user_err ~loc (Pp.str "Syntax error") + | ts, Some qid -> CAst.make ~loc @@ CTypRef (RelId qid, p) + } | id = typ_param -> { CAst.make ~loc @@ CTypVar (Name id) } | "_" -> { CAst.make ~loc @@ CTypVar Anonymous } | qid = Prim.qualid -> { CAst.make ~loc @@ CTypRef (RelId qid, []) } - | "("; p = LIST1 tac2type LEVEL "5" SEP ","; ")"; qid = Prim.qualid -> - { CAst.make ~loc @@ CTypRef (RelId qid, p) } ] + ] ]; locident: [ [ id = Prim.ident -> { CAst.make ~loc id } ] ] diff --git a/user-contrib/Ltac2/tac2core.ml b/user-contrib/Ltac2/tac2core.ml index 0299da6a25..ef666ba9e3 100644 --- a/user-contrib/Ltac2/tac2core.ml +++ b/user-contrib/Ltac2/tac2core.ml @@ -107,6 +107,19 @@ let to_rec_declaration (nas, cs) = Array.map snd nas, Value.to_array Value.to_constr cs) +let of_case_invert = let open Constr in function + | NoInvert -> ValInt 0 + | CaseInvert {univs;args} -> + v_blk 0 [|of_instance univs; of_array of_constr args|] + +let to_case_invert = let open Constr in function + | ValInt 0 -> NoInvert + | ValBlk (0, [|univs;args|]) -> + let univs = to_instance univs in + let args = to_array to_constr args in + CaseInvert {univs;args} + | _ -> CErrors.anomaly Pp.(str "unexpected value shape") + let of_result f = function | Inl c -> v_blk 0 [|f c|] | Inr e -> v_blk 1 [|Value.of_exn e|] @@ -421,10 +434,11 @@ let () = define1 "constr_kind" constr begin fun c -> Value.of_ext Value.val_constructor cstr; of_instance u; |] - | Case (ci, c, t, bl) -> + | Case (ci, c, iv, t, bl) -> v_blk 13 [| Value.of_ext Value.val_case ci; Value.of_constr c; + of_case_invert iv; Value.of_constr t; Value.of_array Value.of_constr bl; |] @@ -507,12 +521,13 @@ let () = define1 "constr_make" valexpr begin fun knd -> let cstr = Value.to_ext Value.val_constructor cstr in let u = to_instance u in EConstr.mkConstructU (cstr, u) - | (13, [|ci; c; t; bl|]) -> + | (13, [|ci; c; iv; t; bl|]) -> let ci = Value.to_ext Value.val_case ci in let c = Value.to_constr c in + let iv = to_case_invert iv in let t = Value.to_constr t in let bl = Value.to_array Value.to_constr bl in - EConstr.mkCase (ci, c, t, bl) + EConstr.mkCase (ci, c, iv, t, bl) | (14, [|recs; i; nas; cs|]) -> let recs = Value.to_array Value.to_int recs in let i = Value.to_int i in diff --git a/vernac/assumptions.ml b/vernac/assumptions.ml index 2bb4bac9a4..848cd501c6 100644 --- a/vernac/assumptions.ml +++ b/vernac/assumptions.ml @@ -179,7 +179,7 @@ let rec traverse current ctx accu t = | Construct (((mind, _), _) as cst, _) -> traverse_inductive accu mind (ConstructRef cst) | Meta _ | Evar _ -> assert false -| Case (_,oty,c,[||]) -> +| Case (_,oty,_,c,[||]) -> (* non dependent match on an inductive with no constructors *) begin match Constr.(kind oty, kind c) with | Lambda(_,_,oty), Const (kn, _) @@ -306,6 +306,13 @@ let traverse current t = considering terms out of any valid environment, so use with caution. *) let type_of_constant cb = cb.Declarations.const_type +let uses_uip mib = + Array.exists (fun mip -> + mip.mind_relevance == Sorts.Irrelevant + && Array.length mip.mind_nf_lc = 1 + && List.length (fst mip.mind_nf_lc.(0)) = List.length mib.mind_params_ctxt) + mib.mind_packets + let assumptions ?(add_opaque=false) ?(add_transparent=false) st gr t = (* Only keep the transitive dependencies *) let (_, graph, ax2ty) = traverse (label_of gr) t in @@ -363,5 +370,11 @@ let assumptions ?(add_opaque=false) ?(add_transparent=false) st gr t = let l = try GlobRef.Map_env.find obj ax2ty with Not_found -> [] in ContextObjectMap.add (Axiom (TypeInType obj, l)) Constr.mkProp accu in + let accu = + if not (uses_uip mind) then accu + else + let l = try GlobRef.Map_env.find obj ax2ty with Not_found -> [] in + ContextObjectMap.add (Axiom (UIP m, l)) Constr.mkProp accu + in accu in GlobRef.Map_env.fold fold graph ContextObjectMap.empty diff --git a/vernac/auto_ind_decl.ml b/vernac/auto_ind_decl.ml index bb640a83f6..ef6f8652e9 100644 --- a/vernac/auto_ind_decl.ml +++ b/vernac/auto_ind_decl.ml @@ -350,13 +350,13 @@ let build_beq_scheme mode kn = done; ar.(i) <- (List.fold_left (fun a decl -> mkLambda (RelDecl.get_annot decl, RelDecl.get_type decl, a)) - (mkCase (ci,do_predicate rel_list nb_cstr_args, + (mkCase (ci,do_predicate rel_list nb_cstr_args,NoInvert, mkVar (Id.of_string "Y") ,ar2)) (constrsi.(i).cs_args)) done; mkNamedLambda (make_annot (Id.of_string "X") Sorts.Relevant) (mkFullInd ind (nb_ind-1+1)) ( mkNamedLambda (make_annot (Id.of_string "Y") Sorts.Relevant) (mkFullInd ind (nb_ind-1+2)) ( - mkCase (ci, do_predicate rel_list 0,mkVar (Id.of_string "X"),ar))) + mkCase (ci, do_predicate rel_list 0,NoInvert,mkVar (Id.of_string "X"),ar))) in (* build_beq_scheme *) let names = Array.make nb_ind (make_annot Anonymous Sorts.Relevant) and types = Array.make nb_ind mkSet and diff --git a/vernac/comDefinition.ml b/vernac/comDefinition.ml index f9b2d8b1d1..b9ed4f838d 100644 --- a/vernac/comDefinition.ml +++ b/vernac/comDefinition.ml @@ -66,9 +66,9 @@ let protect_pattern_in_binder bl c ctypopt = | LetIn (x,b,t,c) -> let evd,c = aux (push_rel (LocalDef (x,b,t)) env) evd c in evd, mkLetIn (x,t,b,c) - | Case (ci,p,a,bl) -> + | Case (ci,p,iv,a,bl) -> let evd,bl = Array.fold_left_map (aux env) evd bl in - evd, mkCase (ci,p,a,bl) + evd, mkCase (ci,p,iv,a,bl) | Cast (c,_,_) -> f env evd c (* we remove the cast we had set *) (* This last case may happen when reaching the proof of an impossible case, as when pattern-matching on a vector of length 1 *) diff --git a/vernac/egramcoq.ml b/vernac/egramcoq.ml index fdc8b1ba4c..cbd83e88b6 100644 --- a/vernac/egramcoq.ml +++ b/vernac/egramcoq.ml @@ -542,7 +542,7 @@ let make_act : type r. r target -> _ -> r gen_eval = function CAst.make ~loc @@ CPatNotation (None, notation, env, []) let extend_constr state forpat ng = - let custom,n,_,_ = ng.notgram_level in + let custom,n,_ = ng.notgram_level in let assoc = ng.notgram_assoc in let (entry, level) = interp_constr_entry_key custom forpat n in let fold (accu, state) pt = diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg index 45bf61d79e..e1f1affb2f 100644 --- a/vernac/g_vernac.mlg +++ b/vernac/g_vernac.mlg @@ -51,6 +51,7 @@ let record_field = Entry.create "vernac:record_field" let of_type_with_opt_coercion = Entry.create "vernac:of_type_with_opt_coercion" let section_subset_expr = Entry.create "vernac:section_subset_expr" let scope_delimiter = Entry.create "vernac:scope_delimiter" +let syntax_modifiers = Entry.create "vernac:syntax_modifiers" let only_parsing = Entry.create "vernac:only_parsing" let make_bullet s = @@ -321,10 +322,13 @@ GRAMMAR EXTEND Gram | -> { None } ] ] ; decl_notation: - [ [ ntn = ne_lstring; ":="; c = constr; b = only_parsing; + [ [ ntn = ne_lstring; ":="; c = constr; + modl = syntax_modifiers; scopt = OPT [ ":"; sc = IDENT -> { sc } ] -> { { decl_ntn_string = ntn; decl_ntn_interp = c; - decl_ntn_only_parsing = b; decl_ntn_scope = scopt } } ] ] + decl_ntn_scope = scopt; + decl_ntn_modifiers = modl; + } } ] ] ; decl_sep: [ [ IDENT "and" -> { () } ] ] @@ -1118,7 +1122,7 @@ GRAMMAR EXTEND Gram (* Grammar extensions *) GRAMMAR EXTEND Gram - GLOBAL: syntax only_parsing; + GLOBAL: syntax only_parsing syntax_modifiers; syntax: [ [ IDENT "Open"; IDENT "Scope"; sc = IDENT -> @@ -1136,7 +1140,7 @@ GRAMMAR EXTEND Gram refl = LIST1 class_rawexpr -> { VernacBindScope (sc,refl) } | IDENT "Infix"; op = ne_lstring; ":="; p = constr; - modl = [ "("; l = LIST1 syntax_modifier SEP ","; ")" -> { l } | -> { [] } ]; + modl = syntax_modifiers; sc = OPT [ ":"; sc = IDENT -> { sc } ] -> { VernacInfix ((op,modl),p,sc) } | IDENT "Notation"; id = identref; @@ -1145,20 +1149,20 @@ GRAMMAR EXTEND Gram (id,(idl,c),{ onlyparsing = b }) } | IDENT "Notation"; s = lstring; ":="; c = constr; - modl = [ "("; l = LIST1 syntax_modifier SEP ","; ")" -> { l } | -> { [] } ]; + modl = syntax_modifiers; sc = OPT [ ":"; sc = IDENT -> { sc } ] -> { VernacNotation (c,(s,modl),sc) } | IDENT "Format"; IDENT "Notation"; n = STRING; s = STRING; fmt = STRING -> { VernacNotationAddFormat (n,s,fmt) } | IDENT "Reserved"; IDENT "Infix"; s = ne_lstring; - l = [ "("; l = LIST1 syntax_modifier SEP ","; ")" -> { l } | -> { [] } ] -> + l = syntax_modifiers -> { let s = CAst.map (fun s -> "x '"^s^"' y") s in VernacSyntaxExtension (true,(s,l)) } | IDENT "Reserved"; IDENT "Notation"; s = ne_lstring; - l = [ "("; l = LIST1 syntax_modifier SEP ","; ")" -> { l } | -> { [] } ] + l = syntax_modifiers -> { VernacSyntaxExtension (false, (s,l)) } (* "Print" "Grammar" and "Declare" "Scope" should be here but are in "command" entry in order @@ -1196,6 +1200,11 @@ GRAMMAR EXTEND Gram | x = IDENT; typ = syntax_extension_type -> { SetEntryType (x,typ) } ] ] ; + syntax_modifiers: + [ [ "("; l = LIST1 syntax_modifier SEP ","; ")" -> { l } + | -> { [] } + ] ] + ; syntax_extension_type: [ [ IDENT "ident" -> { ETIdent } | IDENT "global" -> { ETGlobal } | IDENT "bigint" -> { ETBigint } diff --git a/vernac/himsg.ml b/vernac/himsg.ml index 0c4f76f682..f9ecf10d1b 100644 --- a/vernac/himsg.ml +++ b/vernac/himsg.ml @@ -736,6 +736,9 @@ let explain_disallowed_sprop () = let explain_bad_relevance env = strbrk "Bad relevance (maybe a bugged tactic)." +let explain_bad_invert env = + strbrk "Bad case inversion (maybe a bugged tactic)." + let explain_type_error env sigma err = let env = make_all_name_different env sigma in match err with @@ -779,6 +782,7 @@ let explain_type_error env sigma err = explain_undeclared_universe env sigma l | DisallowedSProp -> explain_disallowed_sprop () | BadRelevance -> explain_bad_relevance env + | BadInvert -> explain_bad_invert env let pr_position (cl,pos) = let clpos = match cl with diff --git a/vernac/library.ml b/vernac/library.ml index c30331b221..e580927bfd 100644 --- a/vernac/library.ml +++ b/vernac/library.ml @@ -514,12 +514,3 @@ let get_used_load_paths () = String.Set.empty !libraries_loaded_list) let _ = Nativelib.get_load_paths := get_used_load_paths - -(* These commands may not be very safe due to ML-side plugin loading - etc... use at your own risk *) -let extern_state s = - System.extern_state Coq_config.state_magic_number s (States.freeze ~marshallable:true) - -let intern_state s = - States.unfreeze (System.with_magic_number_check (System.intern_state Coq_config.state_magic_number) s); - overwrite_library_filenames s diff --git a/vernac/library.mli b/vernac/library.mli index 633d266821..d0e9f84691 100644 --- a/vernac/library.mli +++ b/vernac/library.mli @@ -76,7 +76,3 @@ val native_name_from_filename : string -> string (** {6 Opaque accessors} *) val indirect_accessor : Opaqueproof.indirect_accessor - -(** Low-level state overwriting, not very safe *) -val intern_state : string -> unit -val extern_state : string -> unit diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml index 8435612abd..e9b86f323b 100644 --- a/vernac/metasyntax.ml +++ b/vernac/metasyntax.ml @@ -249,9 +249,9 @@ let quote_notation_token x = if (n > 0 && norm) || (n > 2 && x.[0] == '\'') then "'"^x^"'" else x -let is_numeral symbs = - match List.filter (function Break _ -> false | _ -> true) symbs with - | ([Terminal "-"; Terminal x] | [Terminal x]) -> +let is_numeral_in_constr entry symbs = + match entry, List.filter (function Break _ -> false | _ -> true) symbs with + | InConstrEntry, ([Terminal "-"; Terminal x] | [Terminal x]) -> NumTok.Unsigned.parse_string x <> None | _ -> false @@ -749,25 +749,25 @@ let pr_arg_level from (lev,typ) = | LevelSome -> mt () in Ppvernac.pr_set_entry_type (fun _ -> (*TO CHECK*) mt()) typ ++ pplev lev -let pr_level ntn (from,fromlevel,args,typs) = +let pr_level ntn (from,fromlevel,args) typs = (match from with InConstrEntry -> mt () | InCustomEntry s -> str "in " ++ str s ++ spc()) ++ str "at level " ++ int fromlevel ++ spc () ++ str "with arguments" ++ spc() ++ prlist_with_sep pr_comma (pr_arg_level fromlevel) (List.combine args typs) -let error_incompatible_level ntn oldprec prec = +let error_incompatible_level ntn oldprec oldtyps prec typs = user_err (str "Notation " ++ pr_notation ntn ++ str " is already defined" ++ spc() ++ - pr_level ntn oldprec ++ + pr_level ntn oldprec oldtyps ++ spc() ++ str "while it is now required to be" ++ spc() ++ - pr_level ntn prec ++ str ".") + pr_level ntn prec typs ++ str ".") -let error_parsing_incompatible_level ntn ntn' oldprec prec = +let error_parsing_incompatible_level ntn ntn' oldprec oldtyps prec typs = user_err (str "Notation " ++ pr_notation ntn ++ str " relies on a parsing rule for " ++ pr_notation ntn' ++ spc() ++ str " which is already defined" ++ spc() ++ - pr_level ntn oldprec ++ + pr_level ntn oldprec oldtyps ++ spc() ++ str "while it is now required to be" ++ spc() ++ - pr_level ntn prec ++ str ".") + pr_level ntn prec typs ++ str ".") let warn_incompatible_format = CWarnings.create ~name:"notation-incompatible-format" ~category:"parsing" @@ -780,9 +780,10 @@ let warn_incompatible_format = strbrk " was already defined with a different format" ++ scope ++ str ".") type syntax_parsing_extension = { - synext_level : Notation_gram.level; + synext_level : Notation.level; synext_notation : notation; synext_notgram : notation_grammar option; + synext_nottyps : Extend.constr_entry_key list; } type syntax_printing_extension = { @@ -827,8 +828,16 @@ let check_and_extend_constr_grammar ntn rule = let ntn_for_grammar = rule.notgram_notation in if notation_eq ntn ntn_for_grammar then raise Not_found; let prec = rule.notgram_level in - let oldparsing,oldprec = Notgram_ops.level_of_notation ntn_for_grammar in - if not (Notgram_ops.level_eq prec oldprec) && oldparsing <> None then error_parsing_incompatible_level ntn ntn_for_grammar oldprec prec; + let typs = rule.notgram_typs in + let oldprec = Notation.level_of_notation ntn_for_grammar in + let oldparsing = + try + Some (Notgram_ops.grammar_of_notation ntn_for_grammar) + with Not_found -> None + in + let oldtyps = Notgram_ops.subentries_of_notation ntn_for_grammar in + if not (Notation.level_eq prec oldprec) && oldparsing <> None then + error_parsing_incompatible_level ntn ntn_for_grammar oldprec oldtyps prec typs; if oldparsing = None then raise Not_found with Not_found -> Egramcoq.extend_constr_grammar rule @@ -839,12 +848,21 @@ let cache_one_syntax_extension (pa_se,pp_se) = (* Check and ensure that the level and the precomputed parsing rule is declared *) let oldparsing = try - let oldparsing,oldprec = Notgram_ops.level_of_notation ntn in - if not (Notgram_ops.level_eq prec oldprec) && (oldparsing <> None || pa_se.synext_notgram = None) then error_incompatible_level ntn oldprec prec; + let oldprec = Notation.level_of_notation ntn in + let oldparsing = + try + Some (Notgram_ops.grammar_of_notation ntn) + with Not_found -> None + in + let oldtyps = Notgram_ops.subentries_of_notation ntn in + if not (Notation.level_eq prec oldprec) && (oldparsing <> None || pa_se.synext_notgram = None) then + error_incompatible_level ntn oldprec oldtyps prec pa_se.synext_nottyps; oldparsing with Not_found -> (* Declare the level and the precomputed parsing rule *) - let _ = Notgram_ops.declare_notation_level ntn pa_se.synext_notgram prec in + let () = Notation.declare_notation_level ntn prec in + let () = Notgram_ops.declare_notation_subentries ntn pa_se.synext_nottyps in + let () = Option.iter (Notgram_ops.declare_notation_grammar ntn) pa_se.synext_notgram in None in (* Declare the parsing rule *) begin match oldparsing, pa_se.synext_notgram with @@ -1009,20 +1027,14 @@ let check_binder_type recvars etyps = strbrk " is only for use in recursive notations for binders.") | _ -> ()) etyps -let not_a_syntax_modifier = function -| SetOnlyParsing -> true -| SetOnlyPrinting -> true -| _ -> false - -let no_syntax_modifiers mods = List.for_all not_a_syntax_modifier mods - -let is_only_parsing mods = - let test = function SetOnlyParsing -> true | _ -> false in - List.exists test mods - -let is_only_printing mods = - let test = function SetOnlyPrinting -> true | _ -> false in - List.exists test mods +let interp_non_syntax_modifiers mods = + let set modif (only_parsing,only_printing,entry) = match modif with + | SetOnlyParsing -> Some (true,only_printing,entry) + | SetOnlyPrinting -> Some (only_parsing,true,entry) + | SetCustomEntry(entry,None) -> Some (only_parsing,only_printing,InCustomEntry entry) + | _ -> None + in + List.fold_left (fun st modif -> Option.bind st @@ set modif) (Some (false,false,InConstrEntry)) mods (* Compute precedences from modifiers (or find default ones) *) @@ -1141,33 +1153,29 @@ let warn_non_reversible_notation = str " not occur in the right-hand side." ++ spc() ++ strbrk "The notation will not be used for printing as it is not reversible.") -let make_custom_entry custom level = - match custom with - | InConstrEntry -> InConstrEntrySomeLevel - | InCustomEntry s -> InCustomEntryLevel (s,level) - type entry_coercion_kind = | IsEntryCoercion of notation_entry_level | IsEntryGlobal of string * int | IsEntryIdent of string * int -let is_coercion = function - | Some (custom,n,_,[e]) -> +let is_coercion level typs = + match level, typs with + | Some (custom,n,_), [e] -> (match e, custom with | ETConstr _, _ -> - let customkey = make_custom_entry custom n in + let customkey = make_notation_entry_level custom n in let subentry = subentry_of_constr_prod_entry e in if notation_entry_level_eq subentry customkey then None else Some (IsEntryCoercion subentry) | ETGlobal, InCustomEntry s -> Some (IsEntryGlobal (s,n)) | ETIdent, InCustomEntry s -> Some (IsEntryIdent (s,n)) | _ -> None) - | Some _ -> assert false - | None -> None + | Some _, _ -> assert false + | None, _ -> None -let printability level onlyparse reversibility = function +let printability level typs onlyparse reversibility = function | NVar _ when reversibility = APrioriReversible -> - let coe = is_coercion level in + let coe = is_coercion level typs in if not onlyparse && coe = None then warn_notation_bound_to_variable (); true, coe @@ -1229,7 +1237,7 @@ let find_precedence custom lev etyps symbols onlyprint = [],Option.get lev let check_curly_brackets_notation_exists () = - try let _ = Notgram_ops.level_of_notation (InConstrEntrySomeLevel,"{ _ }") in () + try let _ = Notation.level_of_notation (InConstrEntry,"{ _ }") in () with Not_found -> user_err Pp.(str "Notations involving patterns of the form \"{ _ }\" are treated \n\ specially and require that the notation \"{ _ }\" is already reserved.") @@ -1284,10 +1292,12 @@ module SynData = struct (* Notation data for parsing *) level : level; + subentries : constr_entry_key list; pa_syntax_data : subentry_types * symbol list; pp_syntax_data : subentry_types * symbol list; not_data : notation * (* notation *) - level * (* level, precedence, types *) + level * (* level, precedence *) + constr_entry_key list * bool; (* needs_squash *) } @@ -1328,12 +1338,11 @@ let compute_syntax_data ~local deprecation df modifiers = (* Notations for interp and grammar *) let msgs,n = find_precedence mods.custom mods.level mods.etyps symbols onlyprint in - let custom = make_custom_entry mods.custom n in - let ntn_for_interp = make_notation_key custom symbols in + let ntn_for_interp = make_notation_key mods.custom symbols in let symbols_for_grammar = - if custom = InConstrEntrySomeLevel then remove_curly_brackets symbols else symbols in + if mods.custom = InConstrEntry then remove_curly_brackets symbols else symbols in let need_squash = not (List.equal Notation.symbol_eq symbols symbols_for_grammar) in - let ntn_for_grammar = if need_squash then make_notation_key custom symbols_for_grammar else ntn_for_interp in + let ntn_for_grammar = if need_squash then make_notation_key mods.custom symbols_for_grammar else ntn_for_interp in if mods.custom = InConstrEntry && not onlyprint then check_rule_productivity symbols_for_grammar; (* To globalize... *) let etyps = join_auxiliary_recursive_types recvars mods.etyps in @@ -1348,7 +1357,7 @@ let compute_syntax_data ~local deprecation df modifiers = check_locality_compatibility local mods.custom sy_typs; let pa_sy_data = (sy_typs_for_grammar,symbols_for_grammar) in let pp_sy_data = (sy_typs,symbols) in - let sy_fulldata = (ntn_for_grammar,(mods.custom,n,prec_for_grammar,List.map snd sy_typs_for_grammar),need_squash) in + let sy_fulldata = (ntn_for_grammar,(mods.custom,n,prec_for_grammar),List.map snd sy_typs_for_grammar,need_squash) in let df' = ((Lib.library_dp(),Lib.current_dirpath true),df) in let i_data = ntn_for_interp, df' in @@ -1367,7 +1376,8 @@ let compute_syntax_data ~local deprecation df modifiers = mainvars; intern_typs = i_typs; - level = (mods.custom,n,prec,List.map snd sy_typs); + level = (mods.custom,n,prec); + subentries = List.map snd sy_typs; pa_syntax_data = pa_sy_data; pp_syntax_data = pp_sy_data; not_data = sy_fulldata; @@ -1433,7 +1443,13 @@ let open_notation i (_, nobj) = Notation.declare_uninterpretation (NotationRule specific_ntn) pat; (* Declare a possible coercion *) (match nobj.notobj_coercion with - | Some (IsEntryCoercion entry) -> Notation.declare_entry_coercion specific_ntn entry + | Some (IsEntryCoercion entry) -> + let (_,level,_) = Notation.level_of_notation ntn in + let level = match fst ntn with + | InConstrEntry -> None + | InCustomEntry _ -> Some level + in + Notation.declare_entry_coercion specific_ntn level entry | Some (IsEntryGlobal (entry,n)) -> Notation.declare_custom_entry_has_global entry n | Some (IsEntryIdent (entry,n)) -> Notation.declare_custom_entry_has_ident entry n | None -> ()) @@ -1488,10 +1504,14 @@ exception NoSyntaxRule let recover_notation_syntax ntn = let pa = try - let pa_rule,prec = Notgram_ops.level_of_notation ntn in + let prec = Notation.level_of_notation ntn in + let pa_typs = Notgram_ops.subentries_of_notation ntn in + let pa_rule = try Some (Notgram_ops.grammar_of_notation ntn) with Not_found -> None in { synext_level = prec; synext_notation = ntn; - synext_notgram = pa_rule } + synext_notgram = pa_rule; + synext_nottyps = pa_typs; + } with Not_found -> raise NoSyntaxRule in let pp = @@ -1506,7 +1526,7 @@ let recover_notation_syntax ntn = pa,pp let recover_squash_syntax sy = - let sq,_ = recover_notation_syntax (InConstrEntrySomeLevel,"{ _ }") in + let sq,_ = recover_notation_syntax (InConstrEntry,"{ _ }") in match sq.synext_notgram with | Some gram -> sy :: gram | None -> raise NoSyntaxRule @@ -1514,7 +1534,7 @@ let recover_squash_syntax sy = (**********************************************************************) (* Main entry point for building parsing and printing rules *) -let make_pa_rule level (typs,symbols) ntn need_squash = +let make_pa_rule level entries (typs,symbols) ntn need_squash = let assoc = recompute_assoc typs in let prod = make_production typs symbols in let sy = { @@ -1522,6 +1542,7 @@ let make_pa_rule level (typs,symbols) ntn need_squash = notgram_assoc = assoc; notgram_notation = ntn; notgram_prods = prod; + notgram_typs = entries; } in (* By construction, the rule for "{ _ }" is declared, but we need to redeclare it because the file where it is declared needs not be open @@ -1541,14 +1562,15 @@ let make_pp_rule level (typs,symbols) fmt = hunks_of_format (level, List.split typs) (symbols, parse_format fmt) let make_parsing_rules (sd : SynData.syn_data) = let open SynData in - let ntn_for_grammar, prec_for_grammar, need_squash = sd.not_data in + let ntn_for_grammar, prec_for_grammar, typs_for_grammar, need_squash = sd.not_data in let pa_rule = if sd.only_printing then None - else Some (make_pa_rule prec_for_grammar sd.pa_syntax_data ntn_for_grammar need_squash) + else Some (make_pa_rule prec_for_grammar typs_for_grammar sd.pa_syntax_data ntn_for_grammar need_squash) in { synext_level = sd.level; synext_notation = fst sd.info; synext_notgram = pa_rule; + synext_nottyps = typs_for_grammar; } let warn_irrelevant_format = @@ -1556,7 +1578,7 @@ let warn_irrelevant_format = (fun () -> str "The format modifier is irrelevant for only parsing rules.") let make_printing_rules reserved (sd : SynData.syn_data) = let open SynData in - let custom,level,_,_ = sd.level in + let custom,level,_ = sd.level in let pp_rule = make_pp_rule level sd.pp_syntax_data sd.format in if sd.only_parsing then (if sd.format <> None then warn_irrelevant_format (); None) else Some { @@ -1587,7 +1609,8 @@ let add_notation_in_scope ~local deprecation df env c mods scope = let (acvars, ac, reversibility) = interp_notation_constr env nenv c in let interp = make_interpretation_vars sd.recvars acvars (fst sd.pa_syntax_data) in let map (x, _) = try Some (x, Id.Map.find x interp) with Not_found -> None in - let onlyparse,coe = printability (Some sd.level) sd.only_parsing reversibility ac in + let onlyparse,coe = printability (Some sd.level) sd.subentries sd.only_parsing reversibility ac in + let notation, location = sd.info in let notation = { notobj_local = local; notobj_scope = scope; @@ -1597,7 +1620,7 @@ let add_notation_in_scope ~local deprecation df env c mods scope = notobj_coercion = coe; notobj_onlyprint = sd.only_printing; notobj_deprecation = sd.deprecation; - notobj_notation = sd.info; + notobj_notation = (notation, location); notobj_specific_pp_rules = sy_pp_rules; } in let gen_sy_pp_rules = @@ -1610,20 +1633,21 @@ let add_notation_in_scope ~local deprecation df env c mods scope = Lib.add_anonymous_leaf (inNotation notation); sd.info -let add_notation_interpretation_core ~local df env ?(impls=empty_internalization_env) c scope onlyparse onlyprint deprecation = +let add_notation_interpretation_core ~local df env ?(impls=empty_internalization_env) entry c scope onlyparse onlyprint deprecation = let (recvars,mainvars,symbs) = analyze_notation_tokens ~onlyprint df in (* Recover types of variables and pa/pp rules; redeclare them if needed *) - let level, i_typs, onlyprint, pp_sy = if not (is_numeral symbs) then begin - let (pa_sy,pp_sy as sy) = recover_notation_syntax (make_notation_key InConstrEntrySomeLevel symbs) in + let notation_key = make_notation_key entry symbs in + let level, i_typs, onlyprint, pp_sy = if not (is_numeral_in_constr entry symbs) then begin + let (pa_sy,pp_sy as sy) = recover_notation_syntax notation_key in let () = Lib.add_anonymous_leaf (inSyntaxExtension (local,sy)) in (* If the only printing flag has been explicitly requested, put it back *) let onlyprint = onlyprint || pa_sy.synext_notgram = None in - let _,_,_,typs = pa_sy.synext_level in + let typs = pa_sy.synext_nottyps in Some pa_sy.synext_level, typs, onlyprint, pp_sy end else None, [], false, None in (* Declare interpretation *) let path = (Lib.library_dp(), Lib.current_dirpath true) in - let df' = (make_notation_key InConstrEntrySomeLevel symbs, (path,df)) in + let df' = notation_key, (path,df) in let i_vars = make_internalization_vars recvars mainvars (List.map internalization_type_of_entry_type i_typs) in let nenv = { ninterp_var_type = to_map i_vars; @@ -1632,7 +1656,7 @@ let add_notation_interpretation_core ~local df env ?(impls=empty_internalization let (acvars, ac, reversibility) = interp_notation_constr env ~impls nenv c in let interp = make_interpretation_vars recvars acvars (List.combine mainvars i_typs) in let map (x, _) = try Some (x, Id.Map.find x interp) with Not_found -> None in - let onlyparse,coe = printability level onlyparse reversibility ac in + let onlyparse,coe = printability level i_typs onlyparse reversibility ac in let notation = { notobj_local = local; notobj_scope = scope; @@ -1663,36 +1687,44 @@ let add_notation_interpretation env decl_ntn = let { decl_ntn_string = { CAst.loc ; v = df }; decl_ntn_interp = c; - decl_ntn_only_parsing = onlyparse; - decl_ntn_scope = sc } = decl_ntn in - let df' = add_notation_interpretation_core ~local:false df env c sc onlyparse false None in - Dumpglob.dump_notation (loc,df') sc true + decl_ntn_modifiers = modifiers; + decl_ntn_scope = sc; + } = decl_ntn in + match interp_non_syntax_modifiers modifiers with + | None -> CErrors.user_err (str"Only modifiers not affecting parsing are supported here") + | Some (only_parsing,only_printing,entry) -> + let df' = add_notation_interpretation_core ~local:false df env entry c sc only_parsing false None in + Dumpglob.dump_notation (loc,df') sc true let set_notation_for_interpretation env impls decl_ntn = let { decl_ntn_string = { CAst.v = df }; decl_ntn_interp = c; - decl_ntn_only_parsing = onlyparse; - decl_ntn_scope = sc } = decl_ntn in - (try ignore - (Flags.silently (fun () -> add_notation_interpretation_core ~local:false df env ~impls c sc onlyparse false None) ()); - with NoSyntaxRule -> - user_err Pp.(str "Parsing rule for this notation has to be previously declared.")); - Option.iter (fun sc -> Notation.open_close_scope (false,true,sc)) sc + decl_ntn_modifiers = modifiers; + decl_ntn_scope = sc; + } = decl_ntn in + match interp_non_syntax_modifiers modifiers with + | None -> CErrors.user_err (str"Only modifiers not affecting parsing are supported here") + | Some (only_parsing,only_printing,entry) -> + (try ignore + (Flags.silently (fun () -> add_notation_interpretation_core ~local:false df env ~impls entry c sc only_parsing false None) ()); + with NoSyntaxRule -> + user_err Pp.(str "Parsing rule for this notation has to be previously declared.")); + Option.iter (fun sc -> Notation.open_close_scope (false,true,sc)) sc (* Main entry point *) let add_notation ~local deprecation env c ({CAst.loc;v=df},modifiers) sc = let df' = - if no_syntax_modifiers modifiers then + match interp_non_syntax_modifiers modifiers with + | Some (only_parsing,only_printing,entry) -> (* No syntax data: try to rely on a previously declared rule *) - let onlyparse = is_only_parsing modifiers in - let onlyprint = is_only_printing modifiers in - try add_notation_interpretation_core ~local df env c sc onlyparse onlyprint deprecation + begin try add_notation_interpretation_core ~local df env entry c sc only_parsing only_printing deprecation with NoSyntaxRule -> (* Try to determine a default syntax rule *) add_notation_in_scope ~local deprecation df env c modifiers sc - else + end + | None -> (* Declare both syntax and interpretation *) add_notation_in_scope ~local deprecation df env c modifiers sc in @@ -1701,7 +1733,7 @@ let add_notation ~local deprecation env c ({CAst.loc;v=df},modifiers) sc = let add_notation_extra_printing_rule df k v = let notk = let _,_, symbs = analyze_notation_tokens ~onlyprint:true df in - make_notation_key InConstrEntrySomeLevel symbs in + make_notation_key InConstrEntry symbs in add_notation_extra_printing_rule notk k v (* Infix notations *) @@ -1809,7 +1841,7 @@ let add_syntactic_definition ~local deprecation env ident (vars,c) { onlyparsing let in_pat id = (id,ETConstr (Constrexpr.InConstrEntry,None,(NextLevel,0))) in let interp = make_interpretation_vars ~default_if_binding:AsIdentOrPattern [] acvars (List.map in_pat vars) in let vars = List.map (fun x -> (x, Id.Map.find x interp)) vars in - let onlyparsing = onlyparsing || fst (printability None false reversibility pat) in + let onlyparsing = onlyparsing || fst (printability None [] false reversibility pat) in Syntax_def.declare_syntactic_definition ~local deprecation ident ~onlyparsing (vars,pat) (**********************************************************************) diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml index 2c52c605b5..7af6a6a405 100644 --- a/vernac/ppvernac.ml +++ b/vernac/ppvernac.ml @@ -462,11 +462,11 @@ open Pputils let { decl_ntn_string = {CAst.loc;v=ntn}; decl_ntn_interp = c; - decl_ntn_only_parsing = onlyparsing; + decl_ntn_modifiers = modifiers; decl_ntn_scope = scopt } = decl_ntn in fnl () ++ keyword "where " ++ qs ntn ++ str " := " ++ Flags.without_option Flags.beautify prc c - ++ pr_only_parsing_clause onlyparsing + ++ pr_syntax_modifiers modifiers ++ pr_opt (fun sc -> str ": " ++ str sc) scopt let pr_rec_definition { fname; univs; rec_order; binders; rtype; body_def; notations } = diff --git a/vernac/printmod.ml b/vernac/printmod.ml index 219e445c56..fdf7f6c74a 100644 --- a/vernac/printmod.ml +++ b/vernac/printmod.ml @@ -406,11 +406,11 @@ let rec printable_body dir = state after the printing *) let print_expression' is_type extent env mp me = - States.with_state_protection + Vernacstate.System.protect (fun e -> print_expression is_type extent env mp [] e) me let print_signature' is_type extent env mp me = - States.with_state_protection + Vernacstate.System.protect (fun e -> print_signature is_type extent env mp [] e) me let unsafe_print_module extent env mp with_body mb = diff --git a/vernac/record.ml b/vernac/record.ml index 9d99036273..820bcba0b6 100644 --- a/vernac/record.ml +++ b/vernac/record.ml @@ -343,8 +343,9 @@ let declare_projections indsp ctx ?(kind=Decls.StructureComponent) binder_name f let p = mkLambda (x, lift 1 rp, ccl') in let branch = it_mkLambda_or_LetIn (mkRel nfi) lifted_fields in let ci = Inductiveops.make_case_info env indsp rci LetStyle in - (* Record projections have no is *) - mkCase (ci, p, mkRel 1, [|branch|]), None + (* Record projections are always NoInvert because + they're at constant relevance *) + mkCase (ci, p, NoInvert, mkRel 1, [|branch|]), None in let proj = it_mkLambda_or_LetIn (mkLambda (x,rp,body)) paramdecls in let projtyp = it_mkProd_or_LetIn (mkProd (x,rp,ccl)) paramdecls in @@ -710,7 +711,7 @@ let definition_structure udecl kind ~template ~cumulative ~poly finite records = let () = check_priorities kind records in let ps, data = extract_record_data records in let ubinders, univs, auto_template, params, implpars, data = - States.with_state_protection (fun () -> + Vernacstate.System.protect (fun () -> typecheck_params_and_fields (kind = Class true) poly udecl ps data) () in let template = template, auto_template in match kind with diff --git a/vernac/states.ml b/vernac/states.ml deleted file mode 100644 index b6904263df..0000000000 --- a/vernac/states.ml +++ /dev/null @@ -1,33 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * Copyright INRIA, CNRS and contributors *) -(* <O___,, * (see version control and CREDITS file for authors & dates) *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(* * (see LICENSE file for the text of the license) *) -(************************************************************************) - -type state = Lib.frozen * Summary.frozen - -let lib_of_state = fst -let summary_of_state = snd -let replace_summary (lib,_) st = lib, st -let replace_lib (_,st) lib = lib, st - -let freeze ~marshallable = - (Lib.freeze (), Summary.freeze_summaries ~marshallable) - -let unfreeze (fl,fs) = - Lib.unfreeze fl; - Summary.unfreeze_summaries fs - -(* Rollback. *) - -let with_state_protection f x = - let st = freeze ~marshallable:false in - try - let a = f x in unfreeze st; a - with reraise -> - let reraise = Exninfo.capture reraise in - (unfreeze st; Exninfo.iraise reraise) diff --git a/vernac/states.mli b/vernac/states.mli deleted file mode 100644 index 51db83ca03..0000000000 --- a/vernac/states.mli +++ /dev/null @@ -1,32 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * Copyright INRIA, CNRS and contributors *) -(* <O___,, * (see version control and CREDITS file for authors & dates) *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(* * (see LICENSE file for the text of the license) *) -(************************************************************************) - -(** {6 States of the system} *) - -(** In that module, we provide functions to get - and set the state of the whole system. Internally, it is done by - freezing the states of both [Lib] and [Summary]. We provide functions - to write and restore state to and from a given file. *) - -type state -val freeze : marshallable:bool -> state -val unfreeze : state -> unit - -val summary_of_state : state -> Summary.frozen -val lib_of_state : state -> Lib.frozen -val replace_summary : state -> Summary.frozen -> state -val replace_lib : state -> Lib.frozen -> state - -(** {6 Rollback } *) - -(** [with_state_protection f x] applies [f] to [x] and restores the - state of the whole system as it was before applying [f] *) - -val with_state_protection : ('a -> 'b) -> 'a -> 'b diff --git a/vernac/vernac.mllib b/vernac/vernac.mllib index f357a04668..994592a88a 100644 --- a/vernac/vernac.mllib +++ b/vernac/vernac.mllib @@ -1,9 +1,6 @@ Vernacexpr Attributes Pvernac -States -Declaremods -Printmod G_vernac G_proofs Vernacprop @@ -21,6 +18,7 @@ Declare ComHints Canonical RecLemmas +Declaremods Library ComCoercion Auto_ind_decl @@ -32,10 +30,12 @@ ComAssumption DeclareInd Search ComSearch -Prettyp ComInductive ComFixpoint ComProgramFixpoint +Vernacstate +Printmod +Prettyp Record Assumptions Mltop @@ -43,5 +43,4 @@ Topfmt Loadpath ComArguments Vernacentries -Vernacstate Vernacinterp diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index f5ef5ee86f..b0e483ee74 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -1269,11 +1269,11 @@ let vernac_chdir = function let vernac_write_state file = let file = CUnix.make_suffix file ".coq" in - Library.extern_state file + Vernacstate.System.dump file let vernac_restore_state file = let file = Loadpath.locate_file (CUnix.make_suffix file ".coq") in - Library.intern_state file + Vernacstate.System.load file (************) (* Commands *) @@ -1553,6 +1553,15 @@ let () = optread = (fun () -> (Global.typing_flags ()).Declarations.check_universes); optwrite = (fun b -> Global.set_check_universes b) } +let () = + declare_bool_option + { optdepr = false; + optkey = ["Definitional"; "UIP"]; + optread = (fun () -> (Global.typing_flags ()).Declarations.allow_uip); + optwrite = (fun b -> Global.set_typing_flags + {(Global.typing_flags ()) with Declarations.allow_uip = b}) + } + let vernac_set_strategy ~local l = let local = Option.default false local in let glob_ref r = diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml index 0fdf9e2a7b..06ac7f8d48 100644 --- a/vernac/vernacexpr.ml +++ b/vernac/vernacexpr.ml @@ -137,11 +137,21 @@ type definition_expr = | DefineBody of local_binder_expr list * Genredexpr.raw_red_expr option * constr_expr * constr_expr option +type syntax_modifier = + | SetItemLevel of string list * Notation_term.constr_as_binder_kind option * Extend.production_level + | SetLevel of int + | SetCustomEntry of string * int option + | SetAssoc of Gramlib.Gramext.g_assoc + | SetEntryType of string * Extend.simple_constr_prod_entry_key + | SetOnlyParsing + | SetOnlyPrinting + | SetFormat of string * lstring + type decl_notation = { decl_ntn_string : lstring ; decl_ntn_interp : constr_expr - ; decl_ntn_only_parsing : bool ; decl_ntn_scope : scope_name option + ; decl_ntn_modifiers : syntax_modifier list } type 'a fix_expr_gen = @@ -192,16 +202,6 @@ and typeclass_context = typeclass_constraint list type proof_expr = ident_decl * (local_binder_expr list * constr_expr) -type syntax_modifier = - | SetItemLevel of string list * Notation_term.constr_as_binder_kind option * Extend.production_level - | SetLevel of int - | SetCustomEntry of string * int option - | SetAssoc of Gramlib.Gramext.g_assoc - | SetEntryType of string * Extend.simple_constr_prod_entry_key - | SetOnlyParsing - | SetOnlyPrinting - | SetFormat of string * lstring - type opacity_flag = Opaque | Transparent type proof_end = diff --git a/vernac/vernacstate.ml b/vernac/vernacstate.ml index 17c89897fe..073ef1c2d7 100644 --- a/vernac/vernacstate.ml +++ b/vernac/vernacstate.ml @@ -10,7 +10,7 @@ module Parser = struct - type state = Pcoq.frozen_t + type t = Pcoq.frozen_t let init () = Pcoq.freeze ~marshallable:false @@ -24,6 +24,58 @@ module Parser = struct end +module System : sig + type t + val protect : ('a -> 'b) -> 'a -> 'b + val freeze : marshallable:bool -> t + val unfreeze : t -> unit + + val dump : string -> unit + val load : string -> unit + + module Stm : sig + val make_shallow : t -> t + val lib : t -> Lib.frozen + val summary : t -> Summary.frozen + val replace_summary : t -> Summary.frozen -> t + end +end = struct + type t = Lib.frozen * Summary.frozen + + let freeze ~marshallable = + (Lib.freeze (), Summary.freeze_summaries ~marshallable) + + let unfreeze (fl,fs) = + Lib.unfreeze fl; + Summary.unfreeze_summaries fs + + let protect f x = + let st = freeze ~marshallable:false in + try + let a = f x in unfreeze st; a + with reraise -> + let reraise = Exninfo.capture reraise in + (unfreeze st; Exninfo.iraise reraise) + + (* These commands may not be very safe due to ML-side plugin loading + etc... use at your own risk *) + (* XXX: EJGA: this is ignoring parsing state, it works for now? *) + let dump s = + System.extern_state Coq_config.state_magic_number s (freeze ~marshallable:true) + + let load s = + unfreeze (System.with_magic_number_check (System.intern_state Coq_config.state_magic_number) s); + Library.overwrite_library_filenames s + + (* STM-specific state manipulations *) + module Stm = struct + let make_shallow (lib, summary) = Lib.drop_objects lib, summary + let lib = fst + let summary = snd + let replace_summary (lib,_) summary = (lib,summary) + end +end + module LemmaStack = struct type t = Declare.Proof.t * Declare.Proof.t list @@ -58,8 +110,8 @@ module LemmaStack = struct end type t = { - parsing : Parser.state; - system : States.state; (* summary + libstack *) + parsing : Parser.t; + system : System.t; (* summary + libstack *) lemmas : LemmaStack.t option; (* proofs of lemmas currently opened *) shallow : bool (* is the state trimmed down (libstack) *) } @@ -84,26 +136,19 @@ let do_if_not_cached rf f v = () let freeze_interp_state ~marshallable = - { system = update_cache s_cache (States.freeze ~marshallable); + { system = update_cache s_cache (System.freeze ~marshallable); lemmas = !s_lemmas; shallow = false; parsing = Parser.cur_state (); } let unfreeze_interp_state { system; lemmas; parsing } = - do_if_not_cached s_cache States.unfreeze system; + do_if_not_cached s_cache System.unfreeze system; s_lemmas := lemmas; Pcoq.unfreeze parsing -let make_shallow st = - let lib = States.lib_of_state st.system in - { st with - system = States.replace_lib st.system @@ Lib.drop_objects lib; - shallow = true; - } - (* Compatibility module *) -module Declare = struct +module Declare_ = struct let get () = !s_lemmas let set x = s_lemmas := x @@ -182,3 +227,61 @@ module Declare = struct | Some src, Some tgt -> Some (LemmaStack.copy_info ~src ~tgt) end + +(* STM-specific state-handling *) +module Stm = struct + + (* Proof-related state, for workers; ideally the two counters would + be contained in the lemmas state themselves, as there is no need + for evar / metas to be global among proofs *) + type nonrec pstate = + LemmaStack.t option * + int * (* Evarutil.meta_counter_summary_tag *) + int * (* Evd.evar_counter_summary_tag *) + Declare.Obls.State.t + + (* Parts of the system state that are morally part of the proof state *) + let pstate { lemmas; system } = + let st = System.Stm.summary system in + lemmas, + Summary.project_from_summary st Evarutil.meta_counter_summary_tag, + Summary.project_from_summary st Evd.evar_counter_summary_tag, + Summary.project_from_summary st Declare.Obls.State.prg_tag + + let set_pstate ({ lemmas; system } as s) (pstate,c1,c2,c3) = + { s with + lemmas = + Declare_.copy_terminators ~src:s.lemmas ~tgt:pstate + ; system = + System.Stm.replace_summary s.system + begin + let st = System.Stm.summary s.system in + let st = Summary.modify_summary st Evarutil.meta_counter_summary_tag c1 in + let st = Summary.modify_summary st Evd.evar_counter_summary_tag c2 in + let st = Summary.modify_summary st Declare.Obls.State.prg_tag c3 in + st + end + } + + let non_pstate { system } = + let st = System.Stm.summary system in + let st = Summary.remove_from_summary st Evarutil.meta_counter_summary_tag in + let st = Summary.remove_from_summary st Evd.evar_counter_summary_tag in + let st = Summary.remove_from_summary st Declare.Obls.State.prg_tag in + st, System.Stm.lib system + + let same_env { system = s1 } { system = s2 } = + let s1 = System.Stm.summary s1 in + let e1 = Summary.project_from_summary s1 Global.global_env_summary_tag in + let s2 = System.Stm.summary s2 in + let e2 = Summary.project_from_summary s2 Global.global_env_summary_tag in + e1 == e2 + + let make_shallow st = + { st with + system = System.Stm.make_shallow st.system + ; shallow = true + } + +end +module Declare = Declare_ diff --git a/vernac/vernacstate.mli b/vernac/vernacstate.mli index c99db34873..8c23ac0698 100644 --- a/vernac/vernacstate.mli +++ b/vernac/vernacstate.mli @@ -9,12 +9,27 @@ (************************************************************************) module Parser : sig - type state + type t + + val init : unit -> t + val cur_state : unit -> t + + val parse : t -> 'a Pcoq.Entry.t -> Pcoq.Parsable.t -> 'a + +end + +(** System State *) +module System : sig - val init : unit -> state - val cur_state : unit -> state + (** The system state includes the summary and the libobject *) + type t + + (** [protect f x] runs [f x] and discards changes in the system state *) + val protect : ('a -> 'b) -> 'a -> 'b - val parse : state -> 'a Pcoq.Entry.t -> Pcoq.Parsable.t -> 'a + (** Load / Dump provide unsafe but convenient state dumping from / to disk *) + val dump : string -> unit + val load : string -> unit end @@ -31,9 +46,9 @@ module LemmaStack : sig end type t = - { parsing : Parser.state + { parsing : Parser.t (** parsing state [parsing state may not behave 100% functionally yet, beware] *) - ; system : States.state + ; system : System.t (** summary + libstack *) ; lemmas : LemmaStack.t option (** proofs of lemmas currently opened *) @@ -44,11 +59,21 @@ type t = val freeze_interp_state : marshallable:bool -> t val unfreeze_interp_state : t -> unit -val make_shallow : t -> t - (* WARNING: Do not use, it will go away in future releases *) val invalidate_cache : unit -> unit +(* STM-specific state handling *) +module Stm : sig + type pstate + + (** Surgery on states related to proof state *) + val pstate : t -> pstate + val set_pstate : t -> pstate -> t + val non_pstate : t -> Summary.frozen * Lib.frozen + val same_env : t -> t -> bool + val make_shallow : t -> t +end + (* Compatibility module: Do Not Use *) module Declare : sig |