summaryrefslogtreecommitdiff
path: root/toplevel/record.ml
diff options
context:
space:
mode:
Diffstat (limited to 'toplevel/record.ml')
-rw-r--r--toplevel/record.ml186
1 files changed, 153 insertions, 33 deletions
diff --git a/toplevel/record.ml b/toplevel/record.ml
index 306ab047..4a2ef7db 100644
--- a/toplevel/record.ml
+++ b/toplevel/record.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: record.ml 11309 2008-08-06 10:30:35Z herbelin $ *)
+(* $Id: record.ml 11809 2009-01-20 11:39:55Z aspiwack $ *)
open Pp
open Util
@@ -38,17 +38,23 @@ let interp_evars evdref env ?(impls=([],[])) k typ =
let mk_interning_data env na impls typ =
let impl = Impargs.compute_implicits_with_manual env typ (Impargs.is_implicit_args()) impls
- in (out_name na, ([], impl, Notation.compute_arguments_scope typ))
+ in (na, (Constrintern.Method, [], impl, Notation.compute_arguments_scope typ))
-let interp_fields_evars isevars env l =
- List.fold_left
- (fun (env, uimpls, params, impls) ((loc, i), b, t) ->
+let interp_fields_evars isevars env nots l =
+ List.fold_left2
+ (fun (env, uimpls, params, impls) no ((loc, i), b, t) ->
let impl, t' = interp_evars isevars env ~impls Pretyping.IsType t in
let b' = Option.map (fun x -> snd (interp_evars isevars env ~impls (Pretyping.OfType (Some t')) x)) b in
- let data = mk_interning_data env i impl t' in
+ let impls =
+ match i with
+ | Anonymous -> impls
+ | Name na -> (fst impls, mk_interning_data env na impl t' :: snd impls)
+ in
let d = (i,b',t') in
- (push_rel d env, impl :: uimpls, d::params, ([], data :: snd impls)))
- (env, [], [], ([], [])) l
+ (* Temporary declaration of notations and scopes *)
+ Option.iter (declare_interning_data impls) no;
+ (push_rel d env, impl :: uimpls, d::params, impls))
+ (env, [], [], ([], [])) nots l
let binder_of_decl = function
| Vernacexpr.AssumExpr(n,t) -> (n,None,t)
@@ -56,18 +62,21 @@ let binder_of_decl = function
let binders_of_decls = List.map binder_of_decl
-let typecheck_params_and_fields id t ps fs =
+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 (binders_of_decls fs)
+ 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
@@ -198,8 +207,7 @@ let declare_projections indsp ?(kind=StructureComponent) ?name coers fieldimpls
raise (NotDefinable (BadTypedProj (fid,ctx,te))) in
let refi = ConstRef kn in
let constr_fi = mkConst kn in
- Impargs.maybe_declare_manual_implicits
- false refi (Impargs.is_implicit_args()) impls;
+ Impargs.maybe_declare_manual_implicits false refi impls;
if coe then begin
let cl = Class.class_of_global (IndRef indsp) in
Class.try_add_new_coercion_with_source refi Global cl
@@ -210,11 +218,11 @@ let declare_projections indsp ?(kind=StructureComponent) ?name coers fieldimpls
with NotDefinable why ->
warning_or_error coe indsp why;
(None::sp_projs,NoProjection fi::subst) in
- (nfi-1,(optci=None)::kinds,sp_projs,subst))
+ (nfi-1,(fi, optci=None)::kinds,sp_projs,subst))
(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
@@ -224,26 +232,130 @@ 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
+ (* 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 = not declare_as_coind;
+ 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 *)
let kinds,sp_projs = declare_projections rsp ~kind ?name coers fieldimpls fields in
let build = ConstructRef (rsp,1) in
if is_coe then Class.try_add_new_coercion build Global;
- Recordops.declare_structure(rsp,idbuild,List.rev kinds,List.rev sp_projs);
- kn
+ Recordops.declare_structure(rsp,(rsp,1),List.rev kinds,List.rev sp_projs);
+ 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 def 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)] when def ->
+ 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 BiFinite (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
+
+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 ((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
Vernacexpr.AssumExpr((_,Name id),_) -> id::acc
@@ -252,8 +364,16 @@ let definition_structure ((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 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
-
+ let sc = Option.map mkSort s in
+ let implpars, params, implfs, fields =
+ States.with_heavy_rollback (fun () ->
+ typecheck_params_and_fields idstruc sc ps notations fs) ()
+ in
+ match kind with
+ | Class b ->
+ declare_class finite b (loc,idstruc) idbuild implpars params sc implfs fields is_coe coers
+ | _ ->
+ 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)
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-18 19:04:06 +0000