diff options
95 files changed, 1090 insertions, 361 deletions
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..ab0ea41a36 100644 --- a/checker/checker.ml +++ b/checker/checker.ml @@ -299,6 +299,7 @@ let explain_exn = function | UnsatisfiedConstraints _ -> str"UnsatisfiedConstraints" | DisallowedSProp -> str"DisallowedSProp" | BadRelevance -> str"BadRelevance" + | BadInvert -> str"BadInvert" | UndeclaredUniverse _ -> str"UndeclaredUniverse")) | InductiveError e -> 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/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/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 34110f96cf..3df6f986ce 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -296,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)) -> @@ -408,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/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/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 0db9f498b9..423af1d4ec 100644 --- a/engine/evarutil.ml +++ b/engine/evarutil.ml @@ -144,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/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/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/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 dcca694200..f773157c52 100644 --- a/plugins/funind/gen_principle.ml +++ b/plugins/funind/gen_principle.ml @@ -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/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..162013c556 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 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/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/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/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/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/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/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/record.ml b/vernac/record.ml index 3468f5fc36..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 diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 65af66435b..b0e483ee74 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -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 = |