From 82cad0ccf06b80e3fb68e0636e4dfb9c320e2f55 Mon Sep 17 00:00:00 2001 From: aspiwack Date: Mon, 19 Jan 2009 19:17:09 +0000 Subject: Les records déclarés avec Record ne peuvent plus être récursifs (le comportement est similaire à la 8.1). Les records récursifs peuvent-être déclarés avec Inductive et CoInductive, avec les effets idoines sur leur nature. MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit J'ai fait quelques changements dans VernacInductive pour que tout ceci fonctionne bien ensemble. Il reste du nettoyage à faire et probablement des ajustement dans le Printing. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11808 85f007b7-540e-0410-9357-904b9bb8a0f7 --- contrib/funind/rawterm_to_relation.ml | 8 ++++---- contrib/interface/name_to_ast.ml | 4 ++-- contrib/interface/xlate.ml | 2 +- library/decl_kinds.ml | 15 +++++++++++++++ library/decl_kinds.mli | 10 ++++++++++ parsing/g_vernac.ml4 | 16 +++++++++------- parsing/ppvernac.ml | 9 ++++----- toplevel/record.ml | 29 +++++++++++++++++++---------- toplevel/record.mli | 5 +++-- toplevel/vernacentries.ml | 10 +++++----- toplevel/vernacexpr.ml | 6 +++--- 11 files changed, 75 insertions(+), 39 deletions(-) diff --git a/contrib/funind/rawterm_to_relation.ml b/contrib/funind/rawterm_to_relation.ml index f0e5c6256..7e9ba3f8e 100644 --- a/contrib/funind/rawterm_to_relation.ml +++ b/contrib/funind/rawterm_to_relation.ml @@ -1370,12 +1370,12 @@ let do_build_inductive let _time3 = System.get_time () in (* Pp.msgnl (str "error : "++ str (string_of_float (System.time_difference time2 time3))); *) let repacked_rel_inds = - List.map (fun ((a , b , c , l),ntn) -> ((false,a) , b, c , None, Vernacexpr.Constructors l),ntn ) + List.map (fun ((a , b , c , l),ntn) -> ((false,a) , b, c , Vernacexpr.Inductive_kw, Vernacexpr.Constructors l),ntn ) rel_inds in let msg = str "while trying to define"++ spc () ++ - Ppvernac.pr_vernac (Vernacexpr.VernacInductive(true,false,repacked_rel_inds)) + Ppvernac.pr_vernac (Vernacexpr.VernacInductive(Decl_kinds.Finite,false,repacked_rel_inds)) ++ fnl () ++ msg in @@ -1385,12 +1385,12 @@ let do_build_inductive let _time3 = System.get_time () in (* Pp.msgnl (str "error : "++ str (string_of_float (System.time_difference time2 time3))); *) let repacked_rel_inds = - List.map (fun ((a , b , c , l),ntn) -> ((false,a) , b, c , None, Vernacexpr.Constructors l),ntn ) + List.map (fun ((a , b , c , l),ntn) -> ((false,a) , b, c , Vernacexpr.Inductive_kw, Vernacexpr.Constructors l),ntn ) rel_inds in let msg = str "while trying to define"++ spc () ++ - Ppvernac.pr_vernac (Vernacexpr.VernacInductive(true,false,repacked_rel_inds)) + Ppvernac.pr_vernac (Vernacexpr.VernacInductive(Decl_kinds.Finite,false,repacked_rel_inds)) ++ fnl () ++ Cerrors.explain_exn e in diff --git a/contrib/interface/name_to_ast.ml b/contrib/interface/name_to_ast.ml index 5180bdad2..668a581e1 100644 --- a/contrib/interface/name_to_ast.ml +++ b/contrib/interface/name_to_ast.ml @@ -109,7 +109,7 @@ let convert_one_inductive sp tyi = let sp = sp_of_global (IndRef (sp, tyi)) in (((false,(dummy_loc,basename sp)), convert_env(List.rev params), - Some (extern_constr true envpar arity), None, + Some (extern_constr true envpar arity), Vernacexpr.Inductive_kw , Constructors (convert_constructors envpar cstrnames cstrtypes)), None);; (* This function converts a Mutual inductive definition to a Coqast.t. @@ -121,7 +121,7 @@ let mutual_to_ast_list sp mib = let _, l = Array.fold_right (fun mi (n,l) -> (n+1, (convert_one_inductive sp n)::l)) mipv (0, []) in - VernacInductive (mib.mind_finite, false, l) + VernacInductive ((if mib.mind_finite then Decl_kinds.Finite else Decl_kinds.CoFinite), false, l) :: (implicit_args_to_ast_list sp mipv);; let constr_to_ast v = diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml index 71cef59e2..c8684a9a0 100644 --- a/contrib/interface/xlate.ml +++ b/contrib/interface/xlate.ml @@ -1984,7 +1984,7 @@ let rec xlate_vernac = (* xlate_formula (Option.get c1), record_constructor, *) (* build_record_field_list field_list) *) | VernacInductive (isind, _, lmi) -> - let co_or_ind = if isind then "Inductive" else "CoInductive" in + let co_or_ind = if Decl_kinds.recursivity_flag_of_kind isind then "Inductive" else "CoInductive" in let strip_mutind = function (((_, (_,s)), parameters, c, _, Constructors constructors), notopt) -> CT_ind_spec diff --git a/library/decl_kinds.ml b/library/decl_kinds.ml index 735a8fb07..03b14e31c 100644 --- a/library/decl_kinds.ml +++ b/library/decl_kinds.ml @@ -112,3 +112,18 @@ let strength_of_global = function let string_of_strength = function | Local -> "Local" | Global -> "Global" + + +(* Recursive power *) + +(* spiwack: this definition might be of use in the kernel, for now I do not + push them deeper than needed, though. *) +type recursivity_kind = + | Finite (* = inductive *) + | CoFinite (* = coinductive *) + | BiFinite (* = non-recursive, like in "Record" definitions *) + +(* helper, converts to "finiteness flag" booleans *) +let recursivity_flag_of_kind = function + | Finite | BiFinite -> true + | CoFinite -> false diff --git a/library/decl_kinds.mli b/library/decl_kinds.mli index 7aa1df0c9..e42cb9621 100644 --- a/library/decl_kinds.mli +++ b/library/decl_kinds.mli @@ -82,3 +82,13 @@ val string_of_definition_kind : val strength_of_global : global_reference -> locality val string_of_strength : locality -> string + +(* About recursive power of type declarations *) + +type recursivity_kind = + | Finite (* = inductive *) + | CoFinite (* = coinductive *) + | BiFinite (* = non-recursive, like in "Record" definitions *) + +(* helper, converts to "finiteness flag" booleans *) +val recursivity_flag_of_kind : recursivity_kind -> bool diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index ff6d998e2..03b146648 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -151,6 +151,8 @@ GEXTEND Gram (* Gallina inductive declarations *) | f = finite_token; indl = LIST1 inductive_definition SEP "with" -> + let (k,f) = f in + let indl=List.map (fun ((a,b,c,d),e) -> ((a,b,c,k,d),e)) indl in VernacInductive (f,false,indl) | IDENT "Boxed";"Fixpoint"; recs = LIST1 rec_definition SEP "with" -> VernacFixpoint (recs,true) @@ -171,7 +173,7 @@ GEXTEND Gram cfs = [ ":="; l = constructor_list_or_record_decl -> l | -> RecordDecl (None, []) ] -> let (recf,indf) = b in - VernacInductive (indf,infer,[((oc,name),ps,s,Some recf,cfs),None]) + VernacInductive (indf,infer,[((oc,name),ps,s,recf,cfs),None]) ] ] ; typeclass_context: @@ -214,16 +216,16 @@ GEXTEND Gram [ ["Inline" -> true | -> false] ] ; finite_token: - [ [ "Inductive" -> true - | "CoInductive" -> false ] ] + [ [ "Inductive" -> (Inductive_kw,Finite) + | "CoInductive" -> (CoInductive,CoFinite) ] ] ; infer_token: [ [ "Infer" -> true | -> false ] ] ; record_token: - [ [ IDENT "Record" -> (Record,true) - | IDENT "Structure" -> (Structure,true) - | IDENT "Class" -> (Class true,true) ] ] + [ [ IDENT "Record" -> (Record,BiFinite) + | IDENT "Structure" -> (Structure,BiFinite) + | IDENT "Class" -> (Class true,BiFinite) ] ] ; (* Simple definitions *) def_body: @@ -249,7 +251,7 @@ GEXTEND Gram [ [ id = identref; oc = opt_coercion; indpar = binders_let; c = OPT [ ":"; c = lconstr -> c ]; ":="; lc = constructor_list_or_record_decl; ntn = decl_notation -> - (((oc,id),indpar,c,None,lc),ntn) ] ] + (((oc,id),indpar,c,lc),ntn) ] ] ; constructor_list_or_record_decl: [ [ "|"; l = LIST1 constructor SEP "|" -> Constructors l diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml index 496af5b6e..7b3491de2 100644 --- a/parsing/ppvernac.ml +++ b/parsing/ppvernac.ml @@ -594,10 +594,9 @@ let rec pr_vernac = function pr_record_decl b c fs in let pr_oneind key (((coe,id),indpar,s,k,lc),ntn) = let kw = - match k with - | None -> str key - | Some b -> str (match b with Record -> "Record" | Structure -> "Structure" - | Class b -> if b then "Definitional Class" else "Class") + str (match k with Record -> "Record" | Structure -> "Structure" + | Inductive_kw -> "Inductive" | CoInductive -> "CoInductive" + | Class b -> if b then "Definitional Class" else "Class") in hov 0 ( kw ++ spc() ++ @@ -608,7 +607,7 @@ let rec pr_vernac = function str" :=") ++ pr_constructor_list k lc ++ pr_decl_notation pr_constr ntn in - hov 1 (pr_oneind (if f then "Inductive" else "CoInductive") (List.hd l)) + hov 1 (pr_oneind (if (Decl_kinds.recursivity_flag_of_kind f) then "Inductive" else "CoInductive") (List.hd l)) ++ (prlist (fun ind -> fnl() ++ hov 1 (pr_oneind "with" ind)) (List.tl l)) diff --git a/toplevel/record.ml b/toplevel/record.ml index 3ef7eccad..10d4e5dc6 100644 --- a/toplevel/record.ml +++ b/toplevel/record.ml @@ -250,10 +250,19 @@ let declare_structure finite infer id idbuild paramimpls params arity fieldimpls mind_entry_consnames = [idbuild]; mind_entry_lc = [type_constructor] } in + (* spiwack: raises an error if the structure is supposed to be non-recursive, + but isn't *) + (* there is probably a way to push this to "declare_mutual" *) + begin match finite with + | BiFinite -> + if dependent (mkRel (nparams+1)) (it_mkProd_or_LetIn mkProp fields) then + error "Records declared with the keyword Record or Structure cannot be recursive. Maybe you meant to define an Inductive or CoInductive record." + | _ -> () + end; let mie = { mind_entry_params = List.map degenerate_decl params; mind_entry_record = true; - mind_entry_finite = finite; + mind_entry_finite = recursivity_flag_of_kind finite; mind_entry_inds = [mie_ind] } in let kn = Command.declare_mutual_with_eliminations true mie [(paramimpls,[])] in let rsp = (kn,0) in (* This is ind path of idstruc *) @@ -333,7 +342,7 @@ let declare_class finite def infer id idbuild paramimpls params arity fieldimpls cref, [proj_name, Some proj_cst] | _ -> let idarg = Nameops.next_ident_away (snd id) (ids_of_context (Global.env())) in - let ind = declare_structure true infer (snd id) idbuild paramimpls + let ind = declare_structure BiFinite infer (snd id) idbuild paramimpls params (Option.cata (fun x -> x) (new_Type ()) arity) fieldimpls fields ~kind:Method ~name:idarg false (List.map (fun _ -> false) fields) sign in @@ -386,16 +395,16 @@ let definition_structure (kind,finite,infer,(is_coe,(loc,idstruc)),ps,cfs,idbuil States.with_heavy_rollback (fun () -> typecheck_params_and_fields idstruc sc ps notations fs) () in let sign = structure_signature (fields@params) in - match kind with - | Record | Structure -> - let arity = Option.default (new_Type ()) sc in - let implfs = List.map - (fun impls -> implpars @ Impargs.lift_implicits (succ (List.length params)) impls) implfs in - let ind = declare_structure finite infer idstruc idbuild implpars params arity implfs fields is_coe coers sign in - if infer then search_record declare_record_instance (ConstructRef (ind,1)) sign; - IndRef ind + match kind with | Class def -> let gr = declare_class finite def infer (loc,idstruc) idbuild implpars params sc implfs fields is_coe coers sign in if infer then search_record declare_class_instance gr sign; gr + | _ -> + let arity = Option.default (new_Type ()) sc in + let implfs = List.map + (fun impls -> implpars @ Impargs.lift_implicits (succ (List.length params)) impls) implfs in + let ind = declare_structure finite infer idstruc idbuild implpars params arity implfs fields is_coe coers sign in + if infer then search_record declare_record_instance (ConstructRef (ind,1)) sign; + IndRef ind diff --git a/toplevel/record.mli b/toplevel/record.mli index 564d4409f..0e23af5c0 100644 --- a/toplevel/record.mli +++ b/toplevel/record.mli @@ -27,7 +27,8 @@ val declare_projections : bool list -> manual_explicitation list list -> rel_context -> (name * bool) list * constant option list -val declare_structure : bool (*coinductive?*)-> bool (*infer?*) -> identifier -> identifier -> +val declare_structure : Decl_kinds.recursivity_kind -> + bool (*infer?*) -> identifier -> identifier -> manual_explicitation list -> rel_context -> (* params *) constr -> (* arity *) Impargs.manual_explicitation list list -> rel_context -> (* fields *) ?kind:Decl_kinds.definition_object_kind -> ?name:identifier -> @@ -37,6 +38,6 @@ val declare_structure : bool (*coinductive?*)-> bool (*infer?*) -> identifier -> inductive val definition_structure : - record_kind * bool (*coinductive?*) * bool(*infer?*)* lident with_coercion * local_binder list * + inductive_kind * Decl_kinds.recursivity_kind * bool(*infer?*)* lident with_coercion * local_binder list * (local_decl_expr with_coercion with_notation) list * identifier * constr_expr option -> global_reference diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 39a545215..5796d79ee 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -399,17 +399,17 @@ let vernac_inductive finite infer indl = | _ -> () (* dumping is done by vernac_record (called below) *) ) indl; match indl with - | [ ( id , bl , c , Some b, RecordDecl (oc,fs) ), None ] -> + | [ ( id , bl , c , b, RecordDecl (oc,fs) ), None ] -> vernac_record (match b with Class true -> Class false | _ -> b) finite infer id bl c oc fs - | [ ( id , bl , c , Some (Class true), Constructors [l]), _ ] -> + | [ ( id , bl , c , Class true, Constructors [l]), _ ] -> let f = let (coe, ((loc, id), ce)) = l in ((coe, AssumExpr ((loc, Name id), ce)), None) in vernac_record (Class true) finite infer id bl c None [f] - | [ ( id , bl , c , Some (Class true), _), _ ] -> + | [ ( id , bl , c , Class true, _), _ ] -> Util.error "Definitional classes must have a single method" - | [ ( id , bl , c , Some (Class false), Constructors _), _ ] -> + | [ ( id , bl , c , Class false, Constructors _), _ ] -> Util.error "Inductive classes not supported" | [ ( _ , _ , _ , _, RecordDecl _ ) , _ ] -> Util.error "where clause not supported for (co)inductive records" @@ -418,7 +418,7 @@ let vernac_inductive finite infer indl = | _ -> Util.error "Cannot handle mutually (co)inductive records." in let indl = List.map unpack indl in - Command.build_mutual indl finite + Command.build_mutual indl (recursivity_flag_of_kind finite) let vernac_fixpoint l b = if Dumpglob.dump () then diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml index aa6a48d66..b94526a6e 100644 --- a/toplevel/vernacexpr.ml +++ b/toplevel/vernacexpr.ml @@ -140,7 +140,7 @@ type locality_flag = bool (* true = Local; false = Global *) type coercion_flag = bool (* true = AddCoercion; false = NoCoercion *) type export_flag = bool (* true = Export; false = Import *) type specif_flag = bool (* true = Specification; false = Implementation *) -type inductive_flag = bool (* true = Inductive; false = CoInductive *) +type inductive_flag = Decl_kinds.recursivity_kind type onlyparsing_flag = bool (* true = Parse only; false = Print also *) type infer_flag = bool (* true = try to Infer record; false = nothing *) @@ -155,7 +155,7 @@ type local_decl_expr = | AssumExpr of lname * constr_expr | DefExpr of lname * constr_expr * constr_expr option -type record_kind = Record | Structure | Class of bool (* true = definitional, false = inductive *) +type inductive_kind = Inductive_kw | CoInductive | Record | Structure | Class of bool (* true = definitional, false = inductive *) type decl_notation = (string * constr_expr * scope_name option) option type simple_binder = lident list * constr_expr type class_binder = lident * constr_expr list @@ -166,7 +166,7 @@ type constructor_list_or_record_decl_expr = | Constructors of constructor_expr list | RecordDecl of lident option * local_decl_expr with_coercion with_notation list type inductive_expr = - lident with_coercion * local_binder list * constr_expr option * record_kind option * + lident with_coercion * local_binder list * constr_expr option * inductive_kind * constructor_list_or_record_decl_expr type module_binder = bool option * lident list * module_type_ast -- cgit v1.2.3