summaryrefslogtreecommitdiff
path: root/toplevel/record.ml
diff options
context:
space:
mode:
Diffstat (limited to 'toplevel/record.ml')
-rw-r--r--toplevel/record.ml127
1 files changed, 77 insertions, 50 deletions
diff --git a/toplevel/record.ml b/toplevel/record.ml
index 5629bb71..306ab047 100644
--- a/toplevel/record.ml
+++ b/toplevel/record.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: record.ml 11024 2008-05-30 12:41:39Z msozeau $ *)
+(* $Id: record.ml 11309 2008-08-06 10:30:35Z herbelin $ *)
open Pp
open Util
@@ -31,29 +31,46 @@ open Topconstr
(********** definition d'un record (structure) **************)
-let interp_decl sigma env = function
- | Vernacexpr.AssumExpr((_,id),t) -> (id,None,interp_type Evd.empty env t)
- | Vernacexpr.DefExpr((_,id),c,t) ->
- let c = match t with
- | None -> c
- | Some t -> mkCastC (c, Rawterm.CastConv (DEFAULTcast,t))
- in
- let j = interp_constr_judgment Evd.empty env c in
- (id,Some j.uj_val, refresh_universes j.uj_type)
+let interp_evars evdref env ?(impls=([],[])) k 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 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))
+
+let interp_fields_evars isevars env l =
+ List.fold_left
+ (fun (env, uimpls, params, impls) ((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 d = (i,b',t') in
+ (push_rel d env, impl :: uimpls, d::params, ([], data :: snd impls)))
+ (env, [], [], ([], [])) l
+
+let binder_of_decl = function
+ | Vernacexpr.AssumExpr(n,t) -> (n,None,t)
+ | Vernacexpr.DefExpr(n,c,t) -> (n,Some c, match t with Some c -> c | None -> CHole (fst n, None))
+
+let binders_of_decls = List.map binder_of_decl
let typecheck_params_and_fields id t ps fs =
let env0 = Global.env () in
- let (env1,newps), _ = interp_context Evd.empty env0 ps 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 env2,newfs =
- List.fold_left
- (fun (env,newfs) d ->
- let decl = interp_decl Evd.empty env d in
- (push_rel decl env, decl::newfs))
- (env_ar,[]) fs
+ let evars = ref (Evd.create_evar_defs Evd.empty) in
+ let env2,impls,newfs,data =
+ interp_fields_evars evars env_ar (binders_of_decls fs)
in
- newps, newfs
+ 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
+ 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
let degenerate_decl (na,b,t) =
let id = match na with
@@ -70,24 +87,25 @@ type record_error =
let warning_or_error coe indsp err =
let st = match err with
| MissingProj (fi,projs) ->
- let s,have = if List.length projs > 1 then "s","have" else "","has" in
+ let s,have = if List.length projs > 1 then "s","were" else "","was" in
(str(string_of_id fi) ++
- str" cannot be defined because the projection" ++ str s ++ spc () ++
- prlist_with_sep pr_coma pr_id projs ++ spc () ++ str have ++ str "n't.")
+ strbrk" cannot be defined because the projection" ++ str s ++ spc () ++
+ prlist_with_sep pr_coma pr_id projs ++ spc () ++ str have ++
+ strbrk " not defined.")
| BadTypedProj (fi,ctx,te) ->
match te with
| ElimArity (_,_,_,_,Some (_,_,NonInformativeToInformative)) ->
(pr_id fi ++
- str" cannot be defined because it is informative and " ++
+ strbrk" cannot be defined because it is informative and " ++
Printer.pr_inductive (Global.env()) indsp ++
- str " is not.")
+ strbrk " is not.")
| ElimArity (_,_,_,_,Some (_,_,StrongEliminationOnNonSmallType)) ->
(pr_id fi ++
- str" cannot be defined because it is large and " ++
+ strbrk" cannot be defined because it is large and " ++
Printer.pr_inductive (Global.env()) indsp ++
- str " is not.")
+ strbrk " is not.")
| _ ->
- (pr_id fi ++ str " cannot be defined because it is not typable")
+ (pr_id fi ++ strbrk " cannot be defined because it is not typable.")
in
if coe then errorlabstrm "structure" st;
Flags.if_verbose ppnl (hov 0 (str"Warning: " ++ st))
@@ -131,7 +149,7 @@ let instantiate_possibly_recursive_type indsp paramdecls fields =
substl_rel_context (subst@[mkInd indsp]) fields
(* We build projections *)
-let declare_projections indsp ?(kind=StructureComponent) ?name coers fields =
+let declare_projections indsp ?(kind=StructureComponent) ?name coers fieldimpls fields =
let env = Global.env() in
let (mib,mip) = Global.lookup_inductive indsp in
let paramdecls = mib.mind_params_ctxt in
@@ -142,8 +160,8 @@ let declare_projections indsp ?(kind=StructureComponent) ?name coers fields =
let fields = instantiate_possibly_recursive_type indsp paramdecls fields in
let lifted_fields = lift_rel_context 1 fields in
let (_,kinds,sp_projs,_) =
- List.fold_left2
- (fun (nfi,kinds,sp_projs,subst) coe (fi,optci,ti) ->
+ list_fold_left3
+ (fun (nfi,kinds,sp_projs,subst) coe (fi,optci,ti) impls ->
let (sp_projs,subst) =
match fi with
| Anonymous ->
@@ -180,6 +198,8 @@ let declare_projections indsp ?(kind=StructureComponent) ?name coers fields =
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;
if coe then begin
let cl = Class.class_of_global (IndRef indsp) in
Class.try_add_new_coercion_with_source refi Global cl
@@ -191,28 +211,18 @@ let declare_projections indsp ?(kind=StructureComponent) ?name coers fields =
warning_or_error coe indsp why;
(None::sp_projs,NoProjection fi::subst) in
(nfi-1,(optci=None)::kinds,sp_projs,subst))
- (List.length fields,[],[],[]) coers (List.rev fields)
+ (List.length fields,[],[],[]) coers (List.rev fields) (List.rev fieldimpls)
in (kinds,sp_projs)
-(* [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 coers,fs = List.split cfs in
- let extract_name acc = function
- Vernacexpr.AssumExpr((_,Name id),_) -> id::acc
- | Vernacexpr.DefExpr ((_,Name id),_,_) -> id::acc
- | _ -> acc in
- 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 params,fields = typecheck_params_and_fields idstruc (mkSort s) ps fs in
+let declare_structure 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
let ind = applist (mkRel (1+nparams+nfields), args) in
let type_constructor = it_mkProd_or_LetIn ind fields in
let mie_ind =
- { mind_entry_typename = idstruc;
- mind_entry_arity = mkSort s;
+ { mind_entry_typename = id;
+ mind_entry_arity = arity;
mind_entry_consnames = [idbuild];
mind_entry_lc = [type_constructor] } in
let declare_as_coind =
@@ -223,10 +233,27 @@ let definition_structure ((is_coe,(_,idstruc)),ps,cfs,idbuild,s) =
mind_entry_record = true;
mind_entry_finite = not declare_as_coind;
mind_entry_inds = [mie_ind] } in
- let kn = declare_mutual_with_eliminations true mie [] 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 coers fields in
- let build = ConstructRef (rsp,1) in (* This is construct path of idbuild *)
- if is_coe then Class.try_add_new_coercion build Global;
- Recordops.declare_structure(rsp,idbuild,List.rev kinds,List.rev sp_projs);
- kn
+ 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
+
+(* [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 coers,fs = List.split cfs in
+ let extract_name acc = function
+ Vernacexpr.AssumExpr((_,Name id),_) -> id::acc
+ | Vernacexpr.DefExpr ((_,Name id),_,_) -> id::acc
+ | _ -> acc in
+ 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
+
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-19 03:42:51 +0000