From fa914a0fab970de22aa1382cb7b44c6acc9b0814 Mon Sep 17 00:00:00 2001 From: msozeau Date: Mon, 10 Nov 2008 11:15:41 +0000 Subject: Fix mixup between Record, Structure and Class by adding a new variant for the three cases. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11572 85f007b7-540e-0410-9357-904b9bb8a0f7 --- parsing/g_vernac.ml4 | 12 +++++++----- parsing/ppvernac.ml | 2 +- toplevel/record.ml | 16 ++++++++++------ toplevel/record.mli | 2 +- toplevel/vernacexpr.ml | 5 +++-- 5 files changed, 22 insertions(+), 15 deletions(-) diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index b48548f98..d870c85eb 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -220,7 +220,9 @@ GEXTEND Gram | "CoInductive" -> false ] ] ; record_token: - [ [ IDENT "Record" -> (true,true) | IDENT "Structure" -> (false,true) ]] + [ [ IDENT "Record" -> (Record,true) + | IDENT "Structure" -> (Structure,true) + | IDENT "Class" -> (Class,true) ] ] ; (* Simple definitions *) def_body: @@ -254,8 +256,8 @@ GEXTEND Gram Constructors ((c id)::l) | id = identref ; c = constructor_type -> Constructors [ c id ] | cstr = identref; "{"; fs = LIST0 record_field SEP ";"; "}" -> - RecordDecl (false,Some cstr,fs) - | "{";fs = LIST0 record_field SEP ";"; "}" -> RecordDecl (false,None,fs) + RecordDecl (Record,Some cstr,fs) + | "{";fs = LIST0 record_field SEP ";"; "}" -> RecordDecl (Record,None,fs) | -> Constructors [] ] ] ; (* @@ -503,7 +505,7 @@ GEXTEND Gram | IDENT "Class"; qid = identref; pars = binders_let; s = OPT [ ":"; c = lconstr -> c ]; fs = class_fields -> - VernacInductive (false, [((qid,pars,s,RecordDecl (false,None,fs)),None)]) + VernacInductive (false, [((qid,pars,s,RecordDecl (Class,None,fs)),None)]) (* Type classes *) | IDENT "Class"; sup = OPT [ l = binders_let; "=>" -> l ]; @@ -511,7 +513,7 @@ GEXTEND Gram s = OPT [ ":"; c = lconstr -> c ]; fs = class_fields -> VernacInductive - (false, [((qid,Option.cata (fun x -> x) [] sup @ pars,s,RecordDecl (false,None,fs)),None)]) + (false, [((qid,Option.cata (fun x -> x) [] sup @ pars,s,RecordDecl (Class,None,fs)),None)]) | IDENT "Context"; c = binders_let -> VernacContext c diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml index e16b4e533..0fc28d35f 100644 --- a/parsing/ppvernac.ml +++ b/parsing/ppvernac.ml @@ -667,7 +667,7 @@ let rec pr_vernac = function (* Gallina extensions *) | VernacRecord ((b,coind),(oc,name),ps,s,c,fs) -> hov 2 - (str (if b then "Record" else "Class") ++ + (str (match b with Record -> "Record" | Structure -> "Structure" | Class -> "Class") ++ (if oc then str" > " else str" ") ++ pr_lident name ++ pr_and_type_binders_arg ps ++ str" :" ++ spc() ++ Option.cata pr_lconstr_expr (mt()) s ++ str" := " ++ pr_record_decl b c fs) diff --git a/toplevel/record.ml b/toplevel/record.ml index c066bae5c..f1ee0ab65 100644 --- a/toplevel/record.ml +++ b/toplevel/record.ml @@ -341,6 +341,8 @@ let declare_class finite id idbuild paramimpls params arity fieldimpls fields k.cl_projs coers; add_class k; impl +open Vernacexpr + (* [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 (kind,finite,(is_coe,(loc,idstruc)),ps,cfs,idbuild,s) = @@ -358,9 +360,11 @@ let definition_structure (kind,finite,(is_coe,(loc,idstruc)),ps,cfs,idbuild,s) = States.with_heavy_rollback (fun () -> typecheck_params_and_fields idstruc sc ps notations fs) () in - if kind then - let arity = Option.cata (fun x -> x) (new_Type ()) sc in - let implfs = List.map - (fun impls -> implpars @ Impargs.lift_implicits (succ (List.length params)) impls) implfs - in IndRef (declare_structure finite idstruc idbuild implpars params arity implfs fields is_coe coers) - else declare_class finite (loc,idstruc) idbuild implpars params sc implfs fields is_coe coers + match kind with + | Record | Structure -> + let arity = Option.cata (fun x -> x) (new_Type ()) sc in + let implfs = List.map + (fun impls -> implpars @ Impargs.lift_implicits (succ (List.length params)) impls) implfs + in IndRef (declare_structure finite idstruc idbuild implpars params arity implfs fields is_coe coers) + | Class -> + declare_class finite (loc,idstruc) idbuild implpars params sc implfs fields is_coe coers diff --git a/toplevel/record.mli b/toplevel/record.mli index 57d8cccc0..8a4ca735c 100644 --- a/toplevel/record.mli +++ b/toplevel/record.mli @@ -36,5 +36,5 @@ val declare_structure : bool (*coinductive?*)-> identifier -> identifier -> inductive val definition_structure : - bool (* structure or class *) * bool (*coinductive?*)*lident with_coercion * local_binder list * + record_kind * bool (*coinductive?*)*lident with_coercion * local_binder list * (local_decl_expr with_coercion with_notation) list * identifier * sorts option -> global_reference diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml index 8addcd3ca..5fff24fef 100644 --- a/toplevel/vernacexpr.ml +++ b/toplevel/vernacexpr.ml @@ -155,6 +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 type decl_notation = (string * constr_expr * scope_name option) option type simple_binder = lident list * constr_expr type class_binder = lident * constr_expr list @@ -163,7 +164,7 @@ type 'a with_notation = 'a * decl_notation type constructor_expr = (lident * constr_expr) with_coercion type constructor_list_or_record_decl_expr = | Constructors of constructor_expr list - | RecordDecl of bool * lident option * local_decl_expr with_coercion with_notation list + | RecordDecl of record_kind * lident option * local_decl_expr with_coercion with_notation list type inductive_expr = lident * local_binder list * constr_expr option * constructor_list_or_record_decl_expr @@ -216,7 +217,7 @@ type vernac_expr = | VernacCombinedScheme of lident * lident list (* Gallina extensions *) - | VernacRecord of (bool*bool) (* = Structure or Class * Inductive or CoInductive *) + | VernacRecord of (record_kind*bool) (* = Structure or Class * Inductive or CoInductive *) * lident with_coercion * local_binder list * constr_expr option * lident option * local_decl_expr with_coercion with_notation list | VernacBeginSection of lident -- cgit v1.2.3