From b18b40878f071b6c7d67d1a2d031370f7a498d0b Mon Sep 17 00:00:00 2001 From: Arnaud Spiwack Date: Wed, 3 Sep 2014 11:40:27 +0200 Subject: Print [Variant] types with the keyword [Variant]. Involves changing the [mind_finite] field in the kernel from a bool to the trivalued type [Decl_kinds.recursivity_kind]. This is why so many files are (unfortunately) affected. It would not be very surprising if some bug was introduced. --- interp/dumpglob.ml | 17 +++++++++++++---- kernel/closure.ml | 2 +- kernel/declarations.mli | 2 +- kernel/entries.mli | 2 +- kernel/inductive.ml | 4 ++-- kernel/nativelambda.ml | 2 +- kernel/subtyping.ml | 2 +- library/declare.ml | 2 +- plugins/extraction/extraction.ml | 4 ++-- plugins/funind/glob_term_to_relation.ml | 2 +- plugins/funind/merge.ml | 6 +++--- plugins/xml/xmlcommand.ml | 4 ++-- pretyping/evarconv.ml | 2 +- pretyping/inductiveops.ml | 4 ++-- pretyping/unification.ml | 2 +- printing/printer.ml | 9 ++++++++- printing/printmod.ml | 10 ++++++++-- stm/lemmas.ml | 6 +++--- tactics/hipattern.ml4 | 2 +- tools/coqdoc/index.ml | 4 ++-- toplevel/command.mli | 4 ++-- toplevel/indschemes.ml | 4 ++-- toplevel/record.ml | 2 +- toplevel/vernacentries.ml | 2 +- 24 files changed, 61 insertions(+), 39 deletions(-) diff --git a/interp/dumpglob.ml b/interp/dumpglob.ml index bf9d2c0b9..87c8cb04d 100644 --- a/interp/dumpglob.ml +++ b/interp/dumpglob.ml @@ -111,10 +111,19 @@ let type_of_global_ref gr = | Globnames.IndRef ind -> let (mib,oib) = Inductive.lookup_mind_specif (Global.env ()) ind in if mib.Declarations.mind_record <> None then - if mib.Declarations.mind_finite then "rec" - else "corec" - else if mib.Declarations.mind_finite then "ind" - else "coind" + let open Decl_kinds in + begin match mib.Declarations.mind_finite with + | Finite -> "indrec" + | BiFinite -> "rec" + | CoFinite -> "corec" + end + else + let open Decl_kinds in + begin match mib.Declarations.mind_finite with + | Finite -> "ind" + | BiFinite -> "variant" + | CoFinite -> "coind" + end | Globnames.ConstructRef _ -> "constr" let remove_sections dir = diff --git a/kernel/closure.ml b/kernel/closure.ml index fcbe939a9..d0a9ffd64 100644 --- a/kernel/closure.ml +++ b/kernel/closure.ml @@ -867,7 +867,7 @@ let eta_expand_ind_stacks env ind m s (f, s') = let mib = lookup_mind (fst ind) env in match mib.Declarations.mind_record with | Some (projs,pbs) when Array.length projs > 0 - && mib.Declarations.mind_finite -> + && mib.Declarations.mind_finite <> Decl_kinds.CoFinite -> (* (Construct, pars1 .. parsm :: arg1...argn :: []) ~= (f, s') -> arg1..argn ~= (proj1 t...projn t) where t = zip (f,s') *) let pars = mib.Declarations.mind_nparams in diff --git a/kernel/declarations.mli b/kernel/declarations.mli index 2c516cafd..6b3f6c72f 100644 --- a/kernel/declarations.mli +++ b/kernel/declarations.mli @@ -158,7 +158,7 @@ type mutual_inductive_body = { In the case it is primitive we get its projection names and checked projection bodies, otherwise both arrays are empty. *) - mind_finite : bool; (** Whether the type is inductive or coinductive *) + mind_finite : Decl_kinds.recursivity_kind; (** Whether the type is inductive or coinductive *) mind_ntypes : int; (** Number of types in the block *) diff --git a/kernel/entries.mli b/kernel/entries.mli index 2d7b7bb0f..bf47ff90e 100644 --- a/kernel/entries.mli +++ b/kernel/entries.mli @@ -44,7 +44,7 @@ type mutual_inductive_entry = { mind_entry_record : bool option; (** Some true: primitive record Some false: non-primitive record *) - mind_entry_finite : bool; + mind_entry_finite : Decl_kinds.recursivity_kind; mind_entry_params : (Id.t * local_entry) list; mind_entry_inds : one_inductive_entry list; mind_entry_polymorphic : bool; diff --git a/kernel/inductive.ml b/kernel/inductive.ml index 189c2f4d2..6975544ac 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -38,14 +38,14 @@ let find_inductive env c = let (t, l) = decompose_app (whd_betadeltaiota env c) in match kind_of_term t with | Ind ind - when (fst (lookup_mind_specif env (out_punivs ind))).mind_finite -> (ind, l) + when (fst (lookup_mind_specif env (out_punivs ind))).mind_finite <> Decl_kinds.CoFinite -> (ind, l) | _ -> raise Not_found let find_coinductive env c = let (t, l) = decompose_app (whd_betadeltaiota env c) in match kind_of_term t with | Ind ind - when not (fst (lookup_mind_specif env (out_punivs ind))).mind_finite -> (ind, l) + when (fst (lookup_mind_specif env (out_punivs ind))).mind_finite == Decl_kinds.CoFinite -> (ind, l) | _ -> raise Not_found let inductive_params (mib,_) = mib.mind_nparams diff --git a/kernel/nativelambda.ml b/kernel/nativelambda.ml index 16ca444e3..34ed33f94 100644 --- a/kernel/nativelambda.ml +++ b/kernel/nativelambda.ml @@ -599,7 +599,7 @@ let rec lambda_of_constr env sigma c = { asw_ind = ind; asw_ci = ci; asw_reloc = tbl; - asw_finite = mib.mind_finite; + asw_finite = mib.mind_finite <> Decl_kinds.CoFinite; asw_prefix = prefix} in (* translation of the argument *) diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml index 61420d7ca..f1402a3db 100644 --- a/kernel/subtyping.ml +++ b/kernel/subtyping.ml @@ -168,7 +168,7 @@ let check_inductive cst env mp1 l info1 mp2 mib2 spec2 subst1 subst2 reso1 reso2 (arities_of_specif (mind,u) (mib2,p2)) in let check f test why = if not (test (f mib1) (f mib2)) then error (why (f mib2)) in - check (fun mib -> mib.mind_finite) (==) (fun x -> FiniteInductiveFieldExpected x); + check (fun mib -> mib.mind_finite<>Decl_kinds.CoFinite) (==) (fun x -> FiniteInductiveFieldExpected x); check (fun mib -> mib.mind_ntypes) Int.equal (fun x -> InductiveNumbersFieldExpected x); assert (List.is_empty mib1.mind_hyps && List.is_empty mib2.mind_hyps); assert (Array.length mib1.mind_packets >= 1 diff --git a/library/declare.ml b/library/declare.ml index 6f0ead941..94239d0bf 100644 --- a/library/declare.ml +++ b/library/declare.ml @@ -372,7 +372,7 @@ let dummy_one_inductive_entry mie = { let dummy_inductive_entry (_,m) = ([],{ mind_entry_params = []; mind_entry_record = None; - mind_entry_finite = true; + mind_entry_finite = Decl_kinds.BiFinite; mind_entry_inds = List.map dummy_one_inductive_entry m.mind_entry_inds; mind_entry_polymorphic = false; mind_entry_universes = Univ.UContext.empty; diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml index d2e95a74b..bbbc9bce7 100644 --- a/plugins/extraction/extraction.ml +++ b/plugins/extraction/extraction.ml @@ -220,7 +220,7 @@ let eq_record x y = let mib_equal m1 m2 = Array.equal oib_equal m1.mind_packets m1.mind_packets && eq_record m1.mind_record m2.mind_record && - (m1.mind_finite : bool) == m2.mind_finite && + (m1.mind_finite : Decl_kinds.recursivity_kind) == m2.mind_finite && Int.equal m1.mind_ntypes m2.mind_ntypes && List.equal eq_named_declaration m1.mind_hyps m2.mind_hyps && Int.equal m1.mind_nparams m2.mind_nparams && @@ -437,7 +437,7 @@ and extract_ind env kn = (* kn is supposed to be in long form *) let ip = (kn, 0) in let r = IndRef ip in if is_custom r then raise (I Standard); - if not mib.mind_finite then raise (I Coinductive); + if mib.mind_finite == Decl_kinds.CoFinite then raise (I Coinductive); if not (Int.equal mib.mind_ntypes 1) then raise (I Standard); let p,u = packets.(0) in if p.ip_logical then raise (I Standard); diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml index 40abdb68b..507ba1970 100644 --- a/plugins/funind/glob_term_to_relation.ml +++ b/plugins/funind/glob_term_to_relation.ml @@ -1405,7 +1405,7 @@ let do_build_inductive (* in *) let _time2 = System.get_time () in try - with_full_print (Flags.silently (Command.do_mutual_inductive rel_inds false false)) true + with_full_print (Flags.silently (Command.do_mutual_inductive rel_inds false false)) Decl_kinds.Finite with | UserError(s,msg) as e -> let _time3 = System.get_time () in diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml index 6eabe6e87..0886e7f71 100644 --- a/plugins/funind/merge.ml +++ b/plugins/funind/merge.ml @@ -355,8 +355,8 @@ let ind2name = Id.of_string "__ind2" be co-inductive, and for the moment they must not be mutual either. *) let verify_inds mib1 mib2 = - if not mib1.mind_finite then error "First argument is coinductive"; - if not mib2.mind_finite then error "Second argument is coinductive"; + if mib1.mind_finite == Decl_kinds.CoFinite then error "First argument is coinductive"; + if mib2.mind_finite == Decl_kinds.CoFinite then error "Second argument is coinductive"; if not (Int.equal mib1.mind_ntypes 1) then error "First argument is mutual"; if not (Int.equal mib2.mind_ntypes 1) then error "Second argument is mutual"; () @@ -885,7 +885,7 @@ let merge_inductive (ind1: inductive) (ind2: inductive) (* Declare inductive *) let indl,_,_ = Command.extract_mutual_inductive_declaration_components [(indexpr,[])] in let mie,impls = Command.interp_mutual_inductive indl [] - false (*FIXMEnon-poly *) false (* means not private *) true (* means: not coinductive *) in + false (*FIXMEnon-poly *) false (* means not private *) Decl_kinds.Finite (* means: not coinductive *) in (* Declare the mutual inductive block with its associated schemes *) ignore (Command.declare_mutual_inductive_with_eliminations Declare.UserVerbose mie impls) diff --git a/plugins/xml/xmlcommand.ml b/plugins/xml/xmlcommand.ml index ef5e18201..d65e6f317 100644 --- a/plugins/xml/xmlcommand.ml +++ b/plugins/xml/xmlcommand.ml @@ -272,7 +272,7 @@ let theory_output_string ?(do_not_quote = false) s = let kind_of_inductive isrecord kn = "DEFINITION", - if (fst (Global.lookup_inductive (kn,0))).Declarations.mind_finite + if (fst (Global.lookup_inductive (kn,0))).Declarations.mind_finite <> Decl_kinds.CoFinite then begin match isrecord with | Declare.KernelSilent -> "Record" @@ -389,7 +389,7 @@ let print internal glob_ref kind xml_library_root = Declarations.mind_packets=packs ; Declarations.mind_hyps=hyps; Declarations.mind_finite=finite} = mib in - Cic2acic.Inductive kn,mk_inductive_obj kn mib packs variables nparams hyps finite + Cic2acic.Inductive kn,mk_inductive_obj kn mib packs variables nparams hyps (finite<>Decl_kinds.CoFinite) | Globnames.ConstructRef _ -> Errors.error ("a single constructor cannot be printed in XML") in diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index edd108071..7ce6bc3e2 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -762,7 +762,7 @@ and eta_constructor ts env evd sk1 ((ind, i), u) sk2 term2 = let mib = lookup_mind (fst ind) env in match mib.Declarations.mind_record with | Some (projs, pbs) when Array.length projs > 0 - && mib.Declarations.mind_finite -> + && mib.Declarations.mind_finite <> Decl_kinds.CoFinite -> let pars = mib.Declarations.mind_nparams in (try let l1' = Stack.tail pars sk1 in diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml index 913afb219..4b6107c4e 100644 --- a/pretyping/inductiveops.ml +++ b/pretyping/inductiveops.ml @@ -441,7 +441,7 @@ let find_inductive env sigma c = let (t, l) = decompose_app (whd_betadeltaiota env sigma c) in match kind_of_term t with | Ind ind - when (fst (Inductive.lookup_mind_specif env (fst ind))).mind_finite -> + when (fst (Inductive.lookup_mind_specif env (fst ind))).mind_finite <> Decl_kinds.CoFinite -> (ind, l) | _ -> raise Not_found @@ -449,7 +449,7 @@ let find_coinductive env sigma c = let (t, l) = decompose_app (whd_betadeltaiota env sigma c) in match kind_of_term t with | Ind ind - when not (fst (Inductive.lookup_mind_specif env (fst ind))).mind_finite -> + when (fst (Inductive.lookup_mind_specif env (fst ind))).mind_finite == Decl_kinds.CoFinite -> (ind, l) | _ -> raise Not_found diff --git a/pretyping/unification.ml b/pretyping/unification.ml index 46f65271f..d5dfd7bf0 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -461,7 +461,7 @@ let is_eta_constructor_app env f l1 = let mib = lookup_mind (fst ind) env in (match mib.Declarations.mind_record with | Some (exp,projs) when Array.length projs > 0 - && mib.Declarations.mind_finite -> + && mib.Declarations.mind_finite <> Decl_kinds.CoFinite -> Array.length projs == Array.length l1 - mib.Declarations.mind_nparams | _ -> false) | _ -> false diff --git a/printing/printer.ml b/printing/printer.ml index 7938b7bb0..7971e0aaa 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -780,8 +780,15 @@ let print_one_inductive env mib ((_,i) as ind) = let print_mutual_inductive env mind mib = let inds = List.init (Array.length mib.mind_packets) (fun x -> (mind, x)) in + let keyword = + let open Decl_kinds in + match mib.mind_finite with + | Finite -> "Inductive " + | BiFinite -> "Variant " + | CoFinite -> "CoInductive " + in hov 0 (pr_polymorphic mib.mind_polymorphic ++ - str (if mib.mind_finite then "Inductive " else "CoInductive ") ++ + str keyword ++ prlist_with_sep (fun () -> fnl () ++ str" with ") (print_one_inductive env mib) inds ++ pr_universe_ctx (Univ.instantiate_univ_context mib.mind_universes)) diff --git a/printing/printmod.ml b/printing/printmod.ml index 7dd59cf05..ffee2e244 100644 --- a/printing/printmod.ml +++ b/printing/printmod.ml @@ -160,8 +160,14 @@ let print_body is_impl env mp (l,body) = let env = Option.get env in Printer.pr_mutual_inductive_body env (MutInd.make2 mp l) mib with e when Errors.noncritical e -> - (if mib.mind_finite then str "Inductive " else str "CoInductive") - ++ name) + let keyword = + let open Decl_kinds in + match mib.mind_finite with + | Finite -> "Inductive " + | BiFinite -> "Variant " + | CoFinite -> "CoInductive " + in + str keyword ++ name) let print_struct is_impl env mp struc = prlist_with_sep spc (print_body is_impl env mp) struc diff --git a/stm/lemmas.ml b/stm/lemmas.ml index b81429240..bec80f70d 100644 --- a/stm/lemmas.ml +++ b/stm/lemmas.ml @@ -93,7 +93,7 @@ let find_mutually_recursive_statements thms = (match kind_of_term t with | Ind ((kn,_ as ind), u) when let mind = Global.lookup_mind kn in - mind.mind_finite && Option.is_empty b -> + mind.mind_finite == Decl_kinds.Finite && Option.is_empty b -> [ind,x,i],[] | _ -> error "Decreasing argument is not an inductive assumption.") @@ -110,7 +110,7 @@ let find_mutually_recursive_statements thms = match kind_of_term t with | Ind ((kn,_ as ind),u) when let mind = Global.lookup_mind kn in - mind.mind_finite && Option.is_empty b -> + mind.mind_finite <> Decl_kinds.CoFinite && Option.is_empty b -> [ind,x,i] | _ -> []) 0 (List.rev whnf_hyp_hds)) in @@ -120,7 +120,7 @@ let find_mutually_recursive_statements thms = match kind_of_term whnf_ccl with | Ind ((kn,_ as ind),u) when let mind = Global.lookup_mind kn in - Int.equal mind.mind_ntypes n && not mind.mind_finite -> + Int.equal mind.mind_ntypes n && mind.mind_finite == Decl_kinds.CoFinite -> [ind,x,0] | _ -> [] in diff --git a/tactics/hipattern.ml4 b/tactics/hipattern.ml4 index 84fcd6dee..fd871349c 100644 --- a/tactics/hipattern.ml4 +++ b/tactics/hipattern.ml4 @@ -48,7 +48,7 @@ let match_with_non_recursive_type t = let (hdapp,args) = decompose_app t in (match kind_of_term hdapp with | Ind (ind,u) -> - if not (Global.lookup_mind (fst ind)).mind_finite then + if (Global.lookup_mind (fst ind)).mind_finite == Decl_kinds.CoFinite then Some (hdapp,args) else None diff --git a/tools/coqdoc/index.ml b/tools/coqdoc/index.ml index 980f805ef..3da8de072 100644 --- a/tools/coqdoc/index.ml +++ b/tools/coqdoc/index.ml @@ -273,9 +273,9 @@ let type_of_string = function | "def" | "coe" | "subclass" | "canonstruc" | "fix" | "cofix" | "ex" | "scheme" -> Definition | "prf" | "thm" -> Lemma - | "ind" | "coind" -> Inductive + | "ind" | "variant" | "coind" -> Inductive | "constr" -> Constructor - | "rec" | "corec" -> Record + | "indrec" | "rec" | "corec" -> Record | "proj" -> Projection | "class" -> Class | "meth" -> Method diff --git a/toplevel/command.mli b/toplevel/command.mli index d14af7394..bd6da2dbe 100644 --- a/toplevel/command.mli +++ b/toplevel/command.mli @@ -90,7 +90,7 @@ type one_inductive_impls = val interp_mutual_inductive : structured_inductive_expr -> decl_notation list -> polymorphic -> - private_flag -> bool(*finite*) -> + private_flag -> Decl_kinds.recursivity_kind -> mutual_inductive_entry * one_inductive_impls list (** Registering a mutual inductive definition together with its @@ -104,7 +104,7 @@ val declare_mutual_inductive_with_eliminations : val do_mutual_inductive : (one_inductive_expr * decl_notation list) list -> polymorphic -> - private_flag -> bool -> unit + private_flag -> Decl_kinds.recursivity_kind -> unit (** {6 Fixpoints and cofixpoints} *) diff --git a/toplevel/indschemes.ml b/toplevel/indschemes.ml index b422e67b1..7db71c097 100644 --- a/toplevel/indschemes.ml +++ b/toplevel/indschemes.ml @@ -232,7 +232,7 @@ let declare_one_induction_scheme ind = let declare_induction_schemes kn = let mib = Global.lookup_mind kn in - if mib.mind_finite then begin + if mib.mind_finite <> Decl_kinds.CoFinite then begin for i = 0 to Array.length mib.mind_packets - 1 do declare_one_induction_scheme (kn,i); done; @@ -242,7 +242,7 @@ let declare_induction_schemes kn = let declare_eq_decidability_gen internal names kn = let mib = Global.lookup_mind kn in - if mib.mind_finite then + if mib.mind_finite <> Decl_kinds.CoFinite then ignore (define_mutual_scheme eq_dec_scheme_kind internal names kn) let eq_dec_scheme_msg ind = (* TODO: mutual inductive case *) diff --git a/toplevel/record.ml b/toplevel/record.ml index fedf63eed..3134a6be6 100644 --- a/toplevel/record.ml +++ b/toplevel/record.ml @@ -344,7 +344,7 @@ let declare_structure finite infer poly ctx id idbuild paramimpls params arity f let mie = { mind_entry_params = List.map degenerate_decl params; mind_entry_record = Some !primitive_flag; - mind_entry_finite = finite != CoFinite; + mind_entry_finite = finite; mind_entry_inds = [mie_ind]; mind_entry_polymorphic = poly; mind_entry_private = None; diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 4f6b2d5f7..9cb88f541 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -556,7 +556,7 @@ let vernac_inductive poly lo finite infer indl = | _ -> Errors.error "Cannot handle mutually (co)inductive records." in let indl = List.map unpack indl in - do_mutual_inductive indl poly lo (finite != CoFinite) + do_mutual_inductive indl poly lo finite let vernac_fixpoint locality poly local l = let local = enforce_locality_exp locality local in -- cgit v1.2.3