From 9fe895d340a2a578d682c077b66e7a3171d31c87 Mon Sep 17 00:00:00 2001 From: aspiwack Date: Wed, 5 Nov 2008 16:45:18 +0000 Subject: Nouvelle syntaxe pour écrire des records (co)inductifs : MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit CoInductive stream (A:Type) := { hd : A ; tl : stream A }. Inductive nelist (A:Type) := { hd : A ; tl : option (nelist A) }. L'affichage n'est pas encore poli. Il reste à choisir l'exact destin de la syntaxe qui était apparue dans la 8.2beta pour les records coinductifs (qui consistait à utiliser "Record" au lieu de "CoInductive" comme maintenant). VernacRecord et VernacInductive semblent maintenant faire doublon, il doit y avoir moyen de les fusionner. Les records mutuellement inductifs restent aussi à faire. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11539 85f007b7-540e-0410-9357-904b9bb8a0f7 --- CHANGES | 4 +-- contrib/funind/merge.ml | 2 +- contrib/funind/rawterm_to_relation.ml | 14 ++++++-- parsing/g_vernac.ml4 | 38 +++++++++++++------- parsing/ppvernac.ml | 52 +++++++++++++++------------ toplevel/classes.ml | 2 +- toplevel/command.mli | 3 +- toplevel/record.ml | 14 ++++---- toplevel/record.mli | 4 +-- toplevel/vernacentries.ml | 67 +++++++++++++++++++++-------------- toplevel/vernacexpr.ml | 21 ++++++----- 11 files changed, 132 insertions(+), 89 deletions(-) diff --git a/CHANGES b/CHANGES index f0de89eac..64f51f1d7 100644 --- a/CHANGES +++ b/CHANGES @@ -20,8 +20,8 @@ Language arguments in terms. - Sort of Record/Structure, Inductive and CoInductive defaults to Type if omitted. -- Record/Structure now usable for defining coinductive types - (e.g. "Record stream := { hd : nat; tl : stream }.") +- (Co)Inductive types can be defined as records + (e.g. "CoInductive stream := { hd : nat; tl : stream }.") - New syntax "Theorem id1:t1 ... with idn:tn" for proving mutually dependent statements. - Support for sort-polymorphism on constants denoting inductive types. diff --git a/contrib/funind/merge.ml b/contrib/funind/merge.ml index ec456aae6..b7cee7390 100644 --- a/contrib/funind/merge.ml +++ b/contrib/funind/merge.ml @@ -855,7 +855,7 @@ let merge_rec_params_and_arity prms1 prms2 shift (concl:constr) = [rawlist], named ident. FIXME: params et cstr_expr (arity) *) let rawterm_list_to_inductive_expr prms1 prms2 mib1 mib2 shift - (rawlist:(identifier * rawconstr) list):inductive_expr = + (rawlist:(identifier * rawconstr) list) = let lident = dummy_loc, shift.ident in let bindlist , cstr_expr = (* params , arities *) merge_rec_params_and_arity prms1 prms2 shift mkSet in diff --git a/contrib/funind/rawterm_to_relation.ml b/contrib/funind/rawterm_to_relation.ml index 7534ce2ca..48a96f8b6 100644 --- a/contrib/funind/rawterm_to_relation.ml +++ b/contrib/funind/rawterm_to_relation.ml @@ -1226,9 +1226,14 @@ let do_build_inductive | UserError(s,msg) as e -> 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) -> (a , b, c , Vernacexpr.Constructors l),ntn ) + rel_inds + in let msg = str "while trying to define"++ spc () ++ - Ppvernac.pr_vernac (Vernacexpr.VernacInductive(true,rel_inds)) ++ fnl () ++ + Ppvernac.pr_vernac (Vernacexpr.VernacInductive(true,repacked_rel_inds)) + ++ fnl () ++ msg in observe (msg); @@ -1236,9 +1241,14 @@ let do_build_inductive | e -> 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) -> (a , b, c , Vernacexpr.Constructors l),ntn ) + rel_inds + in let msg = str "while trying to define"++ spc () ++ - Ppvernac.pr_vernac (Vernacexpr.VernacInductive(true,rel_inds)) ++ fnl () ++ + Ppvernac.pr_vernac (Vernacexpr.VernacInductive(true,repacked_rel_inds)) + ++ fnl () ++ Cerrors.explain_exn e in observe msg; diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index f0ea35d92..3f8adb92f 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -224,7 +224,7 @@ GEXTEND Gram | "CoInductive" -> false ] ] ; record_token: - [ [ IDENT "Record" -> true | IDENT "Structure" -> false ] ] + [ [ IDENT "Record" -> (true,true) | IDENT "Structure" -> (false,true) ]] ; (* Simple definitions *) def_body: @@ -249,13 +249,18 @@ GEXTEND Gram inductive_definition: [ [ id = identref; indpar = binders_let; c = [ ":"; c = lconstr -> c | -> CSort (loc,Rawterm.RType None) ]; - ":="; lc = constructor_list; ntn = decl_notation -> - ((id,indpar,c,lc),ntn) ] ] - ; - constructor_list: - [ [ "|"; l = LIST1 constructor SEP "|" -> l - | l = LIST1 constructor SEP "|" -> l - | -> [] ] ] + ":="; lc = constructor_list_or_record_decl; ntn = decl_notation -> + ((id,indpar,c,lc),ntn) ] ] + ; + constructor_list_or_record_decl: + [ [ "|"; l = LIST1 constructor SEP "|" -> Constructors l + | id = identref ; c = constructor_type; "|"; l = LIST0 constructor SEP "|" -> + Constructors ((c id)::l) + | id = identref ; c = constructor_type -> Constructors [ c id ] + | cstr = identref; "{"; fs = LIST0 record_field SEP ";"; "}" -> + RecordDecl (Some cstr,fs) + | "{";fs = LIST0 record_field SEP ";"; "}" -> RecordDecl (None,fs) + | -> Constructors [] ] ] ; (* csort: @@ -346,12 +351,19 @@ GEXTEND Gram [ [ idl = LIST1 identref; oc = of_type_with_opt_coercion; c = lconstr -> (oc,(idl,c)) ] ] ; + + constructor_type: + [[ l = binders_let; + t= [ coe = of_type_with_opt_coercion; c = lconstr -> + fun l id -> (coe,(id,mkCProdN loc l c)) + | -> + fun l id -> (false,(id,mkCProdN loc l (CHole (loc, None)))) ] + -> t l + ]] +; + constructor: - [ [ id = identref; l = binders_let; - coe = of_type_with_opt_coercion; c = lconstr -> - (coe,(id,mkCProdN loc l c)) - | id = identref; l = binders_let -> - (false,(id,mkCProdN loc l (CHole (loc, None)))) ] ] + [ [ id = identref; c=constructor_type -> c id ] ] ; of_type_with_opt_coercion: [ [ ":>" -> true diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml index 2233bbd6a..e2237450c 100644 --- a/parsing/ppvernac.ml +++ b/parsing/ppvernac.ml @@ -412,6 +412,27 @@ let pr_lident_constr sep (i,c) = pr_lident i ++ sep ++ pr_constrarg c in let pr_instance_def sep (i,l,c) = pr_lident i ++ prlist_with_sep spc pr_lident l ++ sep ++ pr_constrarg c in + let pr_record_field = function + | (oc,AssumExpr (id,t)) -> + hov 1 (pr_lname id ++ + (if oc then str" :>" else str" :") ++ spc() ++ + pr_lconstr_expr t) + | (oc,DefExpr(id,b,opt)) -> + (match opt with + | Some t -> + hov 1 (pr_lname id ++ + (if oc then str" :>" else str" :") ++ spc() ++ + pr_lconstr_expr t ++ str" :=" ++ pr_lconstr b) + | None -> + hov 1 (pr_lname id ++ str" :=" ++ spc() ++ + pr_lconstr b)) +in + +let pr_record_decl c fs = + pr_opt pr_lident c ++ str"{" ++ + hv 0 (prlist_with_sep pr_semicolon pr_record_field fs ++ str"}") +in + let rec pr_vernac = function (* Proof management *) @@ -565,12 +586,15 @@ let rec pr_vernac = function (if coe then str":>" else str":") ++ pr_spc_lconstr c) in let pr_constructor_list l = match l with - | [] -> mt() - | _ -> + | Constructors [] -> mt() + | Constructors l -> pr_com_at (begin_of_inductive l) ++ fnl() ++ str (if List.length l = 1 then " " else " | ") ++ - prlist_with_sep (fun _ -> fnl() ++ str" | ") pr_constructor l in + prlist_with_sep (fun _ -> fnl() ++ str" | ") pr_constructor l + | RecordDecl (c,fs) -> + spc() ++ + pr_record_decl c fs in let pr_oneind key ((id,indpar,s,lc),ntn) = hov 0 ( str key ++ spc() ++ @@ -644,30 +668,12 @@ let rec pr_vernac = function (* Gallina extensions *) - | VernacRecord (b,(oc,name),ps,s,c,fs) -> - let pr_record_field = function - | (oc,AssumExpr (id,t)) -> - hov 1 (pr_lname id ++ - (if oc then str" :>" else str" :") ++ spc() ++ - pr_lconstr_expr t) - | (oc,DefExpr(id,b,opt)) -> (match opt with - | Some t -> - hov 1 (pr_lname id ++ - (if oc then str" :>" else str" :") ++ spc() ++ - pr_lconstr_expr t ++ str" :=" ++ pr_lconstr b) - | None -> - hov 1 (pr_lname id ++ str" :=" ++ spc() ++ - pr_lconstr b)) in + | VernacRecord ((b,coind),(oc,name),ps,s,c,fs) -> hov 2 (str (if b then "Record" else "Structure") ++ (if oc then str" > " else str" ") ++ pr_lident name ++ pr_and_type_binders_arg ps ++ str" :" ++ spc() ++ - pr_lconstr_expr s ++ str" := " ++ - (match c with - | None -> mt() - | Some sc -> pr_lident sc) ++ - spc() ++ str"{" ++ - hv 0 (prlist_with_sep pr_semicolon pr_record_field fs ++ str"}")) + pr_lconstr_expr s ++ str" := " ++ pr_record_decl c fs) | VernacBeginSection id -> hov 2 (str"Section" ++ spc () ++ pr_lident id) | VernacEndSegment id -> hov 2 (str"End" ++ spc() ++ pr_lident id) | VernacRequire (exp,spe,l) -> hov 2 diff --git a/toplevel/classes.ml b/toplevel/classes.ml index 4eca304c2..b3e646858 100644 --- a/toplevel/classes.ml +++ b/toplevel/classes.ml @@ -230,7 +230,7 @@ let new_class id par ar sup props = | _ -> let idb = id_of_string ("Build_" ^ (string_of_id (snd id))) in let idarg = Nameops.next_ident_away (snd id) (ids_of_context (Global.env())) in - let kn = Record.declare_structure (snd id) idb arity_imps + let kn = Record.declare_structure false (snd id) idb arity_imps params arity fieldimpls fields ~kind:Method ~name:idarg false (List.map (fun _ -> false) fields) in IndRef (kn,0), (List.map2 (fun (id, _, _) y -> (Nameops.out_name id, y)) diff --git a/toplevel/command.mli b/toplevel/command.mli index a1e976c79..386663538 100644 --- a/toplevel/command.mli +++ b/toplevel/command.mli @@ -67,7 +67,8 @@ val compute_interning_datas : Environ.env -> Constrintern.var_internalisation_ty val check_mutuality : Environ.env -> definition_object_kind -> (identifier * types) list -> unit -val build_mutual : (inductive_expr * decl_notation) list -> bool -> unit +val build_mutual : ((lident * local_binder list * constr_expr * constructor_expr list) * + decl_notation) list -> bool -> unit val declare_mutual_with_eliminations : bool -> Entries.mutual_inductive_entry -> diff --git a/toplevel/record.ml b/toplevel/record.ml index 75a0c1293..8d3dd67e7 100644 --- a/toplevel/record.ml +++ b/toplevel/record.ml @@ -217,7 +217,7 @@ let declare_projections indsp ?(kind=StructureComponent) ?name coers fieldimpls (List.length fields,[],[],[]) coers (List.rev fields) (List.rev fieldimpls) in (kinds,sp_projs) -let declare_structure id idbuild paramimpls params arity fieldimpls fields +let declare_structure finite id idbuild paramimpls params arity fieldimpls fields ?(kind=StructureComponent) ?name is_coe coers = let nparams = List.length params and nfields = List.length fields in let args = extended_rel_list nfields params in @@ -227,14 +227,12 @@ let declare_structure id idbuild paramimpls params arity fieldimpls fields { mind_entry_typename = id; mind_entry_arity = arity; mind_entry_consnames = [idbuild]; - mind_entry_lc = [type_constructor] } in - let declare_as_coind = - (* CoInd if recursive; otherwise Ind to have compat on _ind schemes *) - dependent (mkRel (nparams+1)) (it_mkProd_or_LetIn mkProp fields) in + mind_entry_lc = [type_constructor] } + in let mie = { mind_entry_params = List.map degenerate_decl params; mind_entry_record = true; - mind_entry_finite = not declare_as_coind; + mind_entry_finite = 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 *) @@ -246,7 +244,7 @@ let declare_structure id idbuild paramimpls params arity fieldimpls fields (* [fs] corresponds to fields and [ps] to parameters; [coers] is a boolean list telling if the corresponding fields must me declared as coercion *) -let definition_structure ((is_coe,(_,idstruc)),ps,cfs,idbuild,s) = +let definition_structure (finite,(is_coe,(_,idstruc)),ps,cfs,idbuild,s) = let coers,fs = List.split cfs in let extract_name acc = function Vernacexpr.AssumExpr((_,Name id),_) -> id::acc @@ -258,5 +256,5 @@ let definition_structure ((is_coe,(_,idstruc)),ps,cfs,idbuild,s) = let implpars, params, implfs, fields = typecheck_params_and_fields idstruc (mkSort s) ps fs in let implfs = List.map (fun impls -> implpars @ Impargs.lift_implicits (succ (List.length params)) impls) implfs in - declare_structure idstruc idbuild implpars params (mkSort s) implfs fields is_coe coers + declare_structure finite idstruc idbuild implpars params (mkSort s) implfs fields is_coe coers diff --git a/toplevel/record.mli b/toplevel/record.mli index 7799162df..9ac96641a 100644 --- a/toplevel/record.mli +++ b/toplevel/record.mli @@ -26,7 +26,7 @@ val declare_projections : bool list -> manual_explicitation list list -> rel_context -> bool list * constant option list -val declare_structure : identifier -> identifier -> +val declare_structure : bool (*coinductive?*)-> identifier -> identifier -> manual_explicitation list -> rel_context -> (* params *) Term.constr -> (* arity *) Impargs.manual_explicitation list list -> Sign.rel_context -> (* fields *) @@ -36,5 +36,5 @@ val declare_structure : identifier -> identifier -> mutual_inductive val definition_structure : - lident with_coercion * local_binder list * + bool (*coinductive?*)*lident with_coercion * local_binder list * (local_decl_expr with_coercion) list * identifier * sorts -> kernel_name diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index d1c972e2b..5a28d60cf 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -371,15 +371,49 @@ let vernac_assumption kind l nl= if global then Dumpglob.dump_definition lid false "ax" else Dumpglob.dump_definition lid true "var") idl; declare_assumption idl is_coe kind [] c false false nl) l + +let vernac_record finite struc binders sort nameopt cfs = + let const = match nameopt with + | None -> add_prefix "Build_" (snd (snd struc)) + | Some (_,id as lid) -> + Dumpglob.dump_definition lid false "constr"; id in + let sigma = Evd.empty in + let env = Global.env() in + let s = interp_constr sigma env sort in + let s = Reductionops.whd_betadeltaiota env sigma s in + let s = match kind_of_term s with + | Sort s -> s + | _ -> user_err_loc + (constr_loc sort,"definition_structure", str "Sort expected.") in + if Dumpglob.dump () then ( + Dumpglob.dump_definition (snd struc) false "rec"; + List.iter (fun (_, x) -> + match x with + | Vernacexpr.AssumExpr ((loc, Name id), _) -> Dumpglob.dump_definition (loc,id) false "proj" + | _ -> ()) cfs); + ignore(Record.definition_structure (finite,struc,binders,cfs,const,s)) -let vernac_inductive f indl = +let vernac_inductive finite indl = if Dumpglob.dump () then List.iter (fun ((lid, _, _, cstrs), _) -> - Dumpglob.dump_definition lid false "ind"; - List.iter (fun (_, (lid, _)) -> - Dumpglob.dump_definition lid false "constr") cstrs) + match cstrs with + | Constructors cstrs -> + Dumpglob.dump_definition lid false "ind"; + List.iter (fun (_, (lid, _)) -> + Dumpglob.dump_definition lid false "constr") cstrs + | _ -> () (* dumping is done by vernac_record (called below) *) ) indl; - build_mutual indl f + match indl with + | [ ( id , bl , c ,RecordDecl (oc,fs) ), None ] -> + vernac_record finite (false,id) bl c oc fs + | [ ( _ , _ , _ , RecordDecl _ ) , _ ] -> + Util.error "where clause not supported for (co)inductive records" + | _ -> let unpack = function + | ( id , bl , c , Constructors l ) , ntn -> ( id , bl , c , l ) , ntn + | _ -> Util.error "Cannot handle mutually (co)inductive records." + in + let indl = List.map unpack indl in + Command.build_mutual indl finite let vernac_fixpoint l b = if Dumpglob.dump () then @@ -527,27 +561,6 @@ let vernac_include = function (**********************) (* Gallina extensions *) - -let vernac_record struc binders sort nameopt cfs = - let const = match nameopt with - | None -> add_prefix "Build_" (snd (snd struc)) - | Some (_,id as lid) -> - Dumpglob.dump_definition lid false "constr"; id in - let sigma = Evd.empty in - let env = Global.env() in - let s = interp_constr sigma env sort in - let s = Reductionops.whd_betadeltaiota env sigma s in - let s = match kind_of_term s with - | Sort s -> s - | _ -> user_err_loc - (constr_loc sort,"definition_structure", str "Sort expected.") in - if Dumpglob.dump () then ( - Dumpglob.dump_definition (snd struc) false "rec"; - List.iter (fun (_, x) -> - match x with - | AssumExpr ((loc, Name id), _) -> Dumpglob.dump_definition (loc,id) false "proj" - | _ -> ()) cfs); - ignore(Record.definition_structure (struc,binders,cfs,const,s)) (* Sections *) @@ -1314,7 +1327,7 @@ let interp c = match c with | VernacEndSegment lid -> vernac_end_segment lid - | VernacRecord (_,id,bl,s,idopt,fs) -> vernac_record id bl s idopt fs + | VernacRecord ((_,finite),id,bl,s,idopt,fs) -> vernac_record finite id bl s idopt fs | VernacRequire (export,spec,qidl) -> vernac_require export spec qidl | VernacImport (export,qidl) -> vernac_import export qidl | VernacCanonical qid -> vernac_canonical qid diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml index 19b913708..ca539f28a 100644 --- a/toplevel/vernacexpr.ml +++ b/toplevel/vernacexpr.ml @@ -146,14 +146,6 @@ type onlyparsing_flag = bool (* true = Parse only; false = Print also *) type sort_expr = Rawterm.rawsort -type decl_notation = (string * constr_expr * scope_name option) option -type simple_binder = lident list * constr_expr -type class_binder = lident * constr_expr list -type 'a with_coercion = coercion_flag * 'a -type constructor_expr = (lident * constr_expr) with_coercion -type inductive_expr = - lident * local_binder list * constr_expr * constructor_expr list - type definition_expr = | ProveBody of local_binder list * constr_expr | DefineBody of local_binder list * raw_red_expr option * constr_expr @@ -163,6 +155,17 @@ type local_decl_expr = | AssumExpr of lname * constr_expr | DefExpr of lname * constr_expr * constr_expr option +type decl_notation = (string * constr_expr * scope_name option) option +type simple_binder = lident list * constr_expr +type class_binder = lident * constr_expr list +type 'a with_coercion = coercion_flag * 'a +type constructor_expr = (lident * constr_expr) with_coercion +type constructor_list_or_record_decl_expr = + | Constructors of constructor_expr list + | RecordDecl of lident option * local_decl_expr with_coercion list +type inductive_expr = + lident * local_binder list * constr_expr * constructor_list_or_record_decl_expr + type module_binder = bool option * lident list * module_type_ast type grammar_production = @@ -212,7 +215,7 @@ type vernac_expr = | VernacCombinedScheme of lident * lident list (* Gallina extensions *) - | VernacRecord of bool (* = Record or Structure *) + | VernacRecord of (bool*bool) (* = Record or Structure * Inductive or CoInductive *) * lident with_coercion * local_binder list * constr_expr * lident option * local_decl_expr with_coercion list | VernacBeginSection of lident -- cgit v1.2.3