diff options
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/classes.ml | 233 | ||||
| -rw-r--r-- | toplevel/classes.mli | 20 | ||||
| -rw-r--r-- | toplevel/command.ml | 6 | ||||
| -rw-r--r-- | toplevel/command.mli | 2 | ||||
| -rw-r--r-- | toplevel/record.ml | 126 | ||||
| -rw-r--r-- | toplevel/record.mli | 10 | ||||
| -rw-r--r-- | toplevel/vernacentries.ml | 42 | ||||
| -rw-r--r-- | toplevel/vernacexpr.ml | 22 |
8 files changed, 182 insertions, 279 deletions
diff --git a/toplevel/classes.ml b/toplevel/classes.ml index 22d87829a4..555f262ef0 100644 --- a/toplevel/classes.ml +++ b/toplevel/classes.ml @@ -48,7 +48,7 @@ let _ = Auto.add_hints false [typeclasses_db] (Vernacexpr.HintsResolve [pri, false, CAppExpl (dummy_loc, (None, qualid_of_con inst), [])])) ()) - + let declare_instance_cst glob con = let instance = Typeops.type_of_constant (Global.env ()) con in let _, r = decompose_prod_assum instance in @@ -71,196 +71,15 @@ type binder_list = (identifier located * bool * constr_expr) list (* Calls to interpretation functions. *) -let interp_binders_evars isevars env avoid l = - List.fold_left - (fun (env, ids, params) ((loc, i), t) -> - let n = Name i in - let t' = interp_binder_evars isevars env n t in - let d = (i,None,t') in - (push_named d env, i :: ids, d::params)) - (env, avoid, []) l - -let interp_typeclass_context_evars isevars env avoid l = - List.fold_left - (fun (env, ids, params) (iid, bk, l) -> - let t' = interp_binder_evars isevars env (snd iid) l in - let i = match snd iid with - | Anonymous -> Nameops.next_name_away (Termops.named_hd env t' Anonymous) ids - | Name id -> id - in - let d = (i,None,t') in - (push_named d env, i :: ids, d::params)) - (env, avoid, []) l - let interp_type_evars evdref env ?(impls=([],[])) typ = let typ' = intern_gen true ~impls (Evd.evars_of !evdref) env typ in let imps = Implicit_quantifiers.implicits_of_rawterm typ' in imps, Pretyping.Default.understand_tcc_evars evdref env Pretyping.IsType typ' - -let mk_interning_data env na impls typ = - let impl = Impargs.compute_implicits_with_manual env typ (Impargs.is_implicit_args()) impls - in (na, (Constrintern.Method, [], impl, Notation.compute_arguments_scope typ)) -let interp_fields_evars isevars env avoid l = - List.fold_left - (fun (env, uimpls, ids, params, impls) ((loc, i), _, t) -> - let impl, t' = interp_type_evars isevars env ~impls t in - let data = mk_interning_data env i impl t' in - let d = (Name i,None,t') in - (push_rel d env, impl :: uimpls, Idset.add i ids, d::params, ([], data :: snd impls))) - (env, [], avoid, [], ([], [])) l - (* Declare everything in the parameters as implicit, and the class instance as well *) open Topconstr - -let implicits_of_context ctx = - list_map_i (fun i name -> - let explname = - match name with - | Name n -> Some n - | Anonymous -> None - in ExplByPos (i, explname), (true, true)) - 1 (List.rev (Anonymous :: (List.map pi1 ctx))) - -let name_typeclass_binder avoid = function - | LocalRawAssum ([loc, Anonymous], bk, c) -> - let name = - let id = - match c with - CApp (_, (_, CRef (Ident (loc,id))), _) -> id - | _ -> id_of_string "assum" - in Implicit_quantifiers.make_fresh avoid (Global.env ()) id - in LocalRawAssum ([loc, Name name], bk, c), Idset.add name avoid - | x -> x, avoid - -let name_typeclass_binders avoid l = - let l', avoid = - List.fold_left - (fun (binders, avoid) b -> let b', avoid = name_typeclass_binder avoid b in - b' :: binders, avoid) - ([], avoid) l - in List.rev l', avoid - -let new_class id par ar sup props = - let env0 = Global.env() in - let isevars = ref (Evd.create_evar_defs Evd.empty) in - let bound = Implicit_quantifiers.ids_of_list (Termops.ids_of_context env0) in - let bound, ids = Implicit_quantifiers.free_vars_of_binders ~bound [] (sup @ par) in - let bound = Idset.union bound (Implicit_quantifiers.ids_of_list ids) in - let sup, bound = name_typeclass_binders bound sup in - let par, bound = name_typeclass_binders bound par in - let supnames = - List.fold_left (fun acc b -> - match b with - | LocalRawAssum (nl, _, _) -> nl @ acc - | LocalRawDef _ -> assert(false)) - [] sup - in - - (* Interpret the arity *) - let arity_imps, fullarity = - let ar = - match ar with - Some ar -> ar | None -> (dummy_loc, Rawterm.RType None) - in - let arity = CSort (fst ar, snd ar) in - let term = prod_constr_expr (prod_constr_expr arity par) sup in - interp_type_evars isevars env0 term - in - let ctx_params, arity = decompose_prod_assum fullarity in - let env_params = push_rel_context ctx_params env0 in - - (* Interpret the definitions and propositions *) - let env_props, prop_impls, bound, ctx_props, _ = - interp_fields_evars isevars env_params bound props - in - let subs = List.map (fun ((loc, id), b, _) -> b) props in - (* Instantiate evars and check all are resolved *) - let isevars,_ = Evarconv.consider_remaining_unif_problems env_props !isevars in - let isevars = Typeclasses.resolve_typeclasses env_props isevars in - let sigma = Evd.evars_of isevars in - let ctx_params = Evarutil.nf_rel_context_evar sigma ctx_params in - let ctx_props = Evarutil.nf_rel_context_evar sigma ctx_props in - let arity = Reductionops.nf_evar sigma arity in - let ce t = Evarutil.check_evars env0 Evd.empty isevars t in - let fieldimpls = - (* Make the class and all params implicits in the projections *) - let ctx_impls = implicits_of_context ctx_params in - let len = succ (List.length ctx_params) in - List.map (fun x -> ctx_impls @ Impargs.lift_implicits len x) prop_impls - in - let impl, projs = - let params = ctx_params and fields = ctx_props in - List.iter (fun (_,c,t) -> ce t; match c with Some c -> ce c | None -> ()) (params @ fields); - match fields with - | [(Name proj_name, _, field)] -> - let class_body = it_mkLambda_or_LetIn field params in - let class_type = - match ar with - | Some _ -> Some (it_mkProd_or_LetIn arity params) - | None -> None - in - let class_entry = - { const_entry_body = class_body; - const_entry_type = class_type; - const_entry_opaque = false; - const_entry_boxed = false } - in - let cst = Declare.declare_constant (snd id) - (DefinitionEntry class_entry, IsDefinition Definition) - in - let inst_type = appvectc (mkConst cst) (rel_vect 0 (List.length params)) in - let proj_type = it_mkProd_or_LetIn (mkProd(Name (snd id), inst_type, lift 1 field)) params in - let proj_body = it_mkLambda_or_LetIn (mkLambda (Name (snd id), inst_type, mkRel 1)) params in - let proj_entry = - { const_entry_body = proj_body; - const_entry_type = Some proj_type; - const_entry_opaque = false; - const_entry_boxed = false } - in - let proj_cst = Declare.declare_constant proj_name - (DefinitionEntry proj_entry, IsDefinition Definition) - in - let cref = ConstRef cst in - Impargs.declare_manual_implicits false cref arity_imps; - Impargs.declare_manual_implicits false (ConstRef proj_cst) (List.hd fieldimpls); - set_rigid cst; - cref, [proj_name, Some proj_cst] - | _ -> - 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 true (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)) - (List.rev fields) (Recordops.lookup_projections (kn,0))) - in - let ctx_context = - List.map (fun (na, b, t) -> - match Typeclasses.class_of_constr t with - | Some cl -> Some (cl.cl_impl, List.exists (fun (_, n) -> n = na) supnames) - | None -> None) - ctx_params, ctx_params - in - let k = - { cl_impl = impl; - cl_context = ctx_context; - cl_props = ctx_props; - cl_projs = projs } - in - List.iter2 (fun p sub -> - if sub then match snd p with Some p -> declare_instance_cst true p | None -> ()) - k.cl_projs subs; - add_class k -type binder_def_list = (identifier located * identifier located list * constr_expr) list - -let binders_of_lidents l = - List.map (fun (loc, id) -> - LocalRawAssum ([loc, Name id], Default Rawterm.Explicit, - CHole (loc, Some (BinderType (Name id))))) l - let type_ctx_instance isevars env ctx inst subst = let (s, _) = List.fold_left2 @@ -362,29 +181,33 @@ let new_instance ?(global=false) ctx (instid, bk, cl) props ?(generalize=true) end else begin - let subst = - let props = - List.map (fun (x, l, d) -> - x, Topconstr.abstract_constr_expr d (binders_of_lidents l)) - props - in - if List.length props > List.length k.cl_props then - mismatched_props env' (List.map snd props) k.cl_props; - let props, rest = - List.fold_left - (fun (props, rest) (id,_,_) -> - try - let ((loc, mid), c) = List.find (fun ((_,id'), c) -> Name id' = id) rest in - let rest' = List.filter (fun ((_,id'), c) -> Name id' <> id) rest in - Option.iter (fun x -> Dumpglob.add_glob loc (ConstRef x)) (List.assoc mid k.cl_projs); - c :: props, rest' - with Not_found -> (CHole (Util.dummy_loc, None) :: props), rest) - ([], props) k.cl_props - in - if rest <> [] then - unbound_method env' k.cl_impl (fst (List.hd rest)) - else - type_ctx_instance isevars env' k.cl_props props substctx + let props = match props with CRecord (loc, _, fs) -> fs | _ -> assert false in + if List.length props > List.length k.cl_props then + mismatched_props env' (List.map snd props) k.cl_props; + let subst = + match k.cl_props with + | [(na,b,ty)] -> + let term = match props with [] -> CHole (Util.dummy_loc, None) + | [(_,f)] -> f | _ -> assert false in + let ty' = substl subst ty in + let c = interp_casted_constr_evars isevars env' term ty' in + c :: subst + | _ -> + let props, rest = + List.fold_left + (fun (props, rest) (id,_,_) -> + try + let ((loc, mid), c) = List.find (fun ((_,id'), c) -> Name id' = id) rest in + let rest' = List.filter (fun ((_,id'), c) -> Name id' <> id) rest in + Option.iter (fun x -> Dumpglob.add_glob loc (ConstRef x)) (List.assoc mid k.cl_projs); + c :: props, rest' + with Not_found -> (CHole (Util.dummy_loc, None) :: props), rest) + ([], props) k.cl_props + in + if rest <> [] then + unbound_method env' k.cl_impl (fst (List.hd rest)) + else + type_ctx_instance isevars env' k.cl_props props substctx in let app, ty_constr = instance_constructor k (List.rev subst) in let termtype = diff --git a/toplevel/classes.mli b/toplevel/classes.mli index 4f20f1649c..c79eccab84 100644 --- a/toplevel/classes.mli +++ b/toplevel/classes.mli @@ -29,24 +29,6 @@ val mismatched_params : env -> constr_expr list -> rel_context -> 'a val mismatched_props : env -> constr_expr list -> rel_context -> 'a -type binder_list = (identifier located * bool * constr_expr) list -type binder_def_list = (identifier located * identifier located list * constr_expr) list - -val binders_of_lidents : identifier located list -> local_binder list - -val name_typeclass_binders : Idset.t -> - Topconstr.local_binder list -> - Topconstr.local_binder list * Idset.t - -(* val declare_implicit_proj : typeclass -> (identifier * constant) -> *) -(* Impargs.manual_explicitation list -> bool -> unit *) - -val new_class : identifier located -> - local_binder list -> - Vernacexpr.sort_expr located option -> - local_binder list -> - binder_list -> unit - (* Instance declaration *) val declare_instance : bool -> identifier located -> unit @@ -66,7 +48,7 @@ val new_instance : ?global:bool -> (* Not global by default. *) local_binder list -> typeclass_constraint -> - binder_def_list -> + constr_expr -> ?generalize:bool -> ?tac:Proof_type.tactic -> ?hook:(constant -> unit) -> diff --git a/toplevel/command.ml b/toplevel/command.ml index 5cccc225cd..47c51b83fd 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -528,7 +528,9 @@ let interp_mutual paramsl indl notations finite = check_all_names_different indl; let env0 = Global.env() in let evdref = ref (Evd.create_evar_defs Evd.empty) in - let (env_params, ctx_params), userimpls = interp_context_evars evdref env0 paramsl in + let (env_params, ctx_params), userimpls = + interp_context_evars ~fail_anonymous:false evdref env0 paramsl + in let indnames = List.map (fun ind -> ind.ind_name) indl in (* Names of parameters as arguments of the inductive type (defs removed) *) @@ -622,7 +624,7 @@ let prepare_inductive ntnl indl = let indl = List.map (fun ((_,indname),_,ar,lc) -> { ind_name = indname; - ind_arity = ar; + ind_arity = Option.cata (fun x -> x) (CSort (dummy_loc, Rawterm.RType None)) ar; ind_lc = List.map (fun (_,((_,id),t)) -> (id,t)) lc }) indl in List.fold_right Option.List.cons ntnl [], indl diff --git a/toplevel/command.mli b/toplevel/command.mli index 3866635380..8ccaaed35f 100644 --- a/toplevel/command.mli +++ b/toplevel/command.mli @@ -67,7 +67,7 @@ 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 : ((lident * local_binder list * constr_expr * constructor_expr list) * +val build_mutual : ((lident * local_binder list * constr_expr option * constructor_expr list) * decl_notation) list -> bool -> unit val declare_mutual_with_eliminations : diff --git a/toplevel/record.ml b/toplevel/record.ml index 5ebd897892..c066bae5c1 100644 --- a/toplevel/record.ml +++ b/toplevel/record.ml @@ -64,16 +64,19 @@ let binders_of_decls = List.map binder_of_decl let typecheck_params_and_fields id t ps nots fs = let env0 = Global.env () in - let (env1,newps), imps = interp_context Evd.empty env0 ps in - let fullarity = it_mkProd_or_LetIn t newps in - let env_ar = push_rel_context newps (push_rel (Name id,None,fullarity) env0) in let evars = ref (Evd.create_evar_defs Evd.empty) in + let (env1,newps), imps = interp_context_evars ~fail_anonymous:false evars env0 ps in + let fullarity = it_mkProd_or_LetIn (Option.cata (fun x -> x) (new_Type ()) t) newps in + let env_ar = push_rel_context newps (push_rel (Name id,None,fullarity) env0) in let env2,impls,newfs,data = interp_fields_evars evars env_ar nots (binders_of_decls fs) in - let newps = Evarutil.nf_rel_context_evar (Evd.evars_of !evars) newps in - let newfs = Evarutil.nf_rel_context_evar (Evd.evars_of !evars) newfs in - let ce t = Evarutil.check_evars env0 Evd.empty !evars t in + let evars,_ = Evarconv.consider_remaining_unif_problems env_ar !evars in + let evars = Typeclasses.resolve_typeclasses env_ar evars in + let sigma = Evd.evars_of evars in + let newps = Evarutil.nf_rel_context_evar sigma newps in + let newfs = Evarutil.nf_rel_context_evar sigma newfs in + let ce t = Evarutil.check_evars env0 Evd.empty evars t in List.iter (fun (n, b, t) -> Option.iter ce b; ce t) newps; List.iter (fun (n, b, t) -> Option.iter ce b; ce t) newfs; imps, newps, impls, newfs @@ -242,11 +245,105 @@ let declare_structure finite id idbuild paramimpls params arity fieldimpls field let build = ConstructRef (rsp,1) in if is_coe then Class.try_add_new_coercion build Global; Recordops.declare_structure(rsp,(rsp,1),List.rev kinds,List.rev sp_projs); - kn + kn,0 + +let implicits_of_context ctx = + list_map_i (fun i name -> + let explname = + match name with + | Name n -> Some n + | Anonymous -> None + in ExplByPos (i, explname), (true, true)) + 1 (List.rev (Anonymous :: (List.map pi1 ctx))) + +open Typeclasses + +let typeclasses_db = "typeclass_instances" + +let qualid_of_con c = + Qualid (dummy_loc, shortest_qualid_of_global Idset.empty (ConstRef c)) + +let set_rigid c = + Auto.add_hints false [typeclasses_db] + (Vernacexpr.HintsTransparency ([qualid_of_con c], false)) + +let declare_instance_cst glob con = + let instance = Typeops.type_of_constant (Global.env ()) con in + let _, r = Sign.decompose_prod_assum instance in + match class_of_constr r with + | Some tc -> add_instance (new_instance tc None glob con) + | None -> errorlabstrm "" (Pp.strbrk "Constant does not build instances of a declared type class.") + +let declare_class finite id idbuild paramimpls params arity fieldimpls fields + ?(kind=StructureComponent) ?name is_coe coers = + let fieldimpls = + (* Make the class and all params implicits in the projections *) + let ctx_impls = implicits_of_context params in + let len = succ (List.length params) in + List.map (fun x -> ctx_impls @ Impargs.lift_implicits len x) fieldimpls + in + let impl, projs = + match fields with + | [(Name proj_name, _, field)] -> + let class_body = it_mkLambda_or_LetIn field params in + let class_type = Option.map (fun ar -> it_mkProd_or_LetIn ar params) arity in + let class_entry = + { const_entry_body = class_body; + const_entry_type = class_type; + const_entry_opaque = false; + const_entry_boxed = false } + in + let cst = Declare.declare_constant (snd id) + (DefinitionEntry class_entry, IsDefinition Definition) + in + let inst_type = appvectc (mkConst cst) (rel_vect 0 (List.length params)) in + let proj_type = it_mkProd_or_LetIn (mkProd(Name (snd id), inst_type, lift 1 field)) params in + let proj_body = it_mkLambda_or_LetIn (mkLambda (Name (snd id), inst_type, mkRel 1)) params in + let proj_entry = + { const_entry_body = proj_body; + const_entry_type = Some proj_type; + const_entry_opaque = false; + const_entry_boxed = false } + in + let proj_cst = Declare.declare_constant proj_name + (DefinitionEntry proj_entry, IsDefinition Definition) + in + let cref = ConstRef cst in + Impargs.declare_manual_implicits false cref paramimpls; + Impargs.declare_manual_implicits false (ConstRef proj_cst) (List.hd fieldimpls); + set_rigid cst; (* set_rigid proj_cst; *) + 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 (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) + in + (* List.iter (Option.iter (declare_interning_data ((),[]))) notations; *) + IndRef ind, (List.map2 (fun (id, _, _) y -> (Nameops.out_name id, y)) + (List.rev fields) (Recordops.lookup_projections ind)) + in + let ctx_context = + List.map (fun (na, b, t) -> + match Typeclasses.class_of_constr t with + | Some cl -> Some (cl.cl_impl, true) (*List.exists (fun (_, n) -> n = na) supnames)*) + | None -> None) + params, params + in + let k = + { cl_impl = impl; + cl_context = ctx_context; + cl_props = fields; + cl_projs = projs } + in + List.iter2 (fun p sub -> + if sub then match snd p with Some p -> declare_instance_cst true p | None -> ()) + k.cl_projs coers; + add_class k; impl (* [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 (finite,(is_coe,(_,idstruc)),ps,cfs,idbuild,s) = +let definition_structure (kind,finite,(is_coe,(loc,idstruc)),ps,cfs,idbuild,s) = let cfs,notations = List.split cfs in let coers,fs = List.split cfs in let extract_name acc = function @@ -256,11 +353,14 @@ let definition_structure (finite,(is_coe,(_,idstruc)),ps,cfs,idbuild,s) = let allnames = idstruc::(List.fold_left extract_name [] fs) in if not (list_distinct allnames) then error "Two objects have the same name"; (* Now, younger decl in params and fields is on top *) + let sc = Option.map mkSort s in let implpars, params, implfs, fields = States.with_heavy_rollback (fun () -> - typecheck_params_and_fields idstruc (mkSort s) ps notations fs) () + typecheck_params_and_fields idstruc sc ps notations fs) () in - let implfs = - List.map (fun impls -> implpars @ Impargs.lift_implicits (succ (List.length params)) impls) implfs - in declare_structure finite idstruc idbuild implpars params (mkSort s) implfs fields is_coe coers - + 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 diff --git a/toplevel/record.mli b/toplevel/record.mli index 7aea948f31..57d8cccc0b 100644 --- a/toplevel/record.mli +++ b/toplevel/record.mli @@ -15,6 +15,7 @@ open Sign open Vernacexpr open Topconstr open Impargs +open Libnames (*i*) (* [declare_projections ref name coers params fields] declare projections of @@ -27,14 +28,13 @@ val declare_projections : (name * bool) list * constant option list val declare_structure : bool (*coinductive?*)-> identifier -> identifier -> - manual_explicitation list -> rel_context -> (* params *) - Term.constr -> (* arity *) + manual_explicitation list -> rel_context -> (* params *) constr -> (* arity *) Impargs.manual_explicitation list list -> Sign.rel_context -> (* fields *) ?kind:Decl_kinds.definition_object_kind -> ?name:identifier -> bool -> (* coercion? *) bool list -> (* field coercions *) - mutual_inductive + inductive val definition_structure : - bool (*coinductive?*)*lident with_coercion * local_binder list * - (local_decl_expr with_coercion with_notation) list * identifier * sorts -> kernel_name + bool (* structure or class *) * 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/vernacentries.ml b/toplevel/vernacentries.ml index 5045611008..4b4f7abb55 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -372,26 +372,27 @@ let vernac_assumption kind l nl= 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 vernac_record k 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 + let s = Option.map (fun x -> + let s = Reductionops.whd_betadeltaiota env sigma (interp_constr sigma env x) in + match kind_of_term s with + | Sort s -> s + | _ -> user_err_loc + (constr_loc x,"definition_structure", str "Sort expected.")) sort + 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)) + ignore(Record.definition_structure (k,finite,struc,binders,cfs,const,s)) let vernac_inductive finite indl = if Dumpglob.dump () then @@ -404,16 +405,16 @@ let vernac_inductive finite indl = | _ -> () (* dumping is done by vernac_record (called below) *) ) indl; match indl with - | [ ( id , bl , c ,RecordDecl (oc,fs) ), None ] -> - vernac_record finite (false,id) bl c oc fs + | [ ( id , bl , c ,RecordDecl (b,oc,fs) ), None ] -> + vernac_record b finite (false,id) bl c oc fs | [ ( _ , _ , _ , RecordDecl _ ) , _ ] -> - Util.error "where clause not supported for (co)inductive records" + 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 + | ( 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 @@ -609,11 +610,6 @@ let vernac_identity_coercion stre id qids qidt = Class.try_add_new_identity_coercion id stre source target (* Type classes *) -let vernac_class id par ar sup props = - if Dumpglob.dump () then ( - Dumpglob.dump_definition id false "class"; - List.iter (fun (lid, _, _) -> Dumpglob.dump_definition lid false "meth") props); - Classes.new_class id par ar sup props let vernac_instance glob sup inst props pri = Dumpglob.dump_constraint inst false "inst"; @@ -1327,7 +1323,7 @@ let interp c = match c with | VernacEndSegment lid -> vernac_end_segment lid - | VernacRecord ((_,finite),id,bl,s,idopt,fs) -> vernac_record finite id bl s idopt fs + | VernacRecord ((k,finite),id,bl,s,idopt,fs) -> vernac_record k 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 @@ -1335,7 +1331,7 @@ let interp c = match c with | VernacIdentityCoercion (str,(_,id),s,t) -> vernac_identity_coercion str id s t (* Type classes *) - | VernacClass (id, par, ar, sup, props) -> vernac_class id par ar sup props +(* | VernacClass (id, par, ar, sup, props) -> vernac_class id par ar sup props *) | VernacInstance (glob, sup, inst, props, pri) -> vernac_instance glob sup inst props pri | VernacContext sup -> vernac_context sup diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml index 2727100bfa..8addcd3ca5 100644 --- a/toplevel/vernacexpr.ml +++ b/toplevel/vernacexpr.ml @@ -163,9 +163,9 @@ 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 lident option * local_decl_expr with_coercion with_notation list + | RecordDecl of bool * lident option * local_decl_expr with_coercion with_notation list type inductive_expr = - lident * local_binder list * constr_expr * constructor_list_or_record_decl_expr + lident * local_binder list * constr_expr option * constructor_list_or_record_decl_expr type module_binder = bool option * lident list * module_type_ast @@ -216,9 +216,9 @@ type vernac_expr = | VernacCombinedScheme of lident * lident list (* Gallina extensions *) - | VernacRecord of (bool*bool) (* = Record or Structure * Inductive or CoInductive *) + | VernacRecord of (bool*bool) (* = Structure or Class * Inductive or CoInductive *) * lident with_coercion * local_binder list - * constr_expr * lident option * local_decl_expr with_coercion with_notation list + * constr_expr option * lident option * local_decl_expr with_coercion with_notation list | VernacBeginSection of lident | VernacEndSegment of lident | VernacRequire of @@ -230,18 +230,18 @@ type vernac_expr = class_rawexpr * class_rawexpr (* Type classes *) - | VernacClass of - lident * (* name *) - local_binder list * (* params *) - sort_expr located option * (* arity *) - local_binder list * (* constraints *) - (lident * bool * constr_expr) list (* props, with substructure hints *) +(* | VernacClass of *) +(* lident * (\* name *\) *) +(* local_binder list * (\* params *\) *) +(* sort_expr located option * (\* arity *\) *) +(* local_binder list * (\* constraints *\) *) +(* (lident * bool * constr_expr) list (\* props, with substructure hints *\) *) | VernacInstance of bool * (* global *) local_binder list * (* super *) typeclass_constraint * (* instance name, class name, params *) - (lident * lident list * constr_expr) list * (* props *) + constr_expr * (* props *) int option (* Priority *) | VernacContext of local_binder list |