(************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) (* let impl, t' = interp_evars evars env impls Pretyping.IsType t in let b' = Option.map (fun x -> snd (interp_evars evars env impls (Pretyping.OfType (Some t')) x)) b in let impls = match i with | Anonymous -> impls | Name id -> Idmap.add id (compute_internalization_data env Constrintern.Method t' impl) impls in let d = (i,b',t') in List.iter (Metasyntax.set_notation_for_interpretation impls) no; (push_rel d env, impl :: uimpls, d::params, impls)) (env, [], [], impls_env) nots 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 nots fs = let env0 = Global.env () in let evars = ref Evd.empty in let _ = let error bk (loc, name) = match bk with | Default _ -> if name = Anonymous then user_err_loc (loc, "record", str "Record parameters must be named") | _ -> () in List.iter (function LocalRawDef (b, _) -> error default_binder_kind b | LocalRawAssum (ls, bk, ce) -> List.iter (error bk) ls) ps in let impls_env, ((env1,newps), imps) = interp_context_evars evars env0 ps in let fullarity = it_mkProd_or_LetIn (Option.cata (fun x -> x) (Termops.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 impls_env nots (binders_of_decls fs) in let evars = Evarconv.consider_remaining_unif_problems env_ar !evars in let evars = Typeclasses.resolve_typeclasses env_ar evars in let sigma = 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) (List.rev newps); List.iter (fun (n, b, t) -> Option.iter ce b; ce t) (List.rev newfs); imps, newps, impls, newfs let degenerate_decl (na,b,t) = let id = match na with | Name id -> id | Anonymous -> anomaly "Unnamed record variable" in match b with | None -> (id, Entries.LocalAssum t) | Some b -> (id, Entries.LocalDef b) type record_error = | MissingProj of identifier * identifier list | BadTypedProj of identifier * env * Type_errors.type_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","were" else "","was" in (str(string_of_id fi) ++ strbrk" cannot be defined because the projection" ++ str s ++ spc () ++ prlist_with_sep pr_comma pr_id projs ++ spc () ++ str have ++ strbrk " not defined.") | BadTypedProj (fi,ctx,te) -> match te with | ElimArity (_,_,_,_,Some (_,_,NonInformativeToInformative)) -> (pr_id fi ++ strbrk" cannot be defined because it is informative and " ++ Printer.pr_inductive (Global.env()) indsp ++ strbrk " is not.") | ElimArity (_,_,_,_,Some (_,_,StrongEliminationOnNonSmallType)) -> (pr_id fi ++ strbrk" cannot be defined because it is large and " ++ Printer.pr_inductive (Global.env()) indsp ++ strbrk " is not.") | _ -> (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)) type field_status = | NoProjection of name | Projection of constr exception NotDefinable of record_error (* This replaces previous projection bodies in current projection *) (* Undefined projs are collected and, at least one undefined proj occurs *) (* in the body of current projection then the latter can not be defined *) (* [c] is defined in ctxt [[params;fields]] and [l] is an instance of *) (* [[fields]] defined in ctxt [[params;x:ind]] *) let subst_projection fid l c = let lv = List.length l in let bad_projs = ref [] in let rec substrec depth c = match kind_of_term c with | Rel k -> (* We are in context [[params;fields;x:ind;...depth...]] *) if k <= depth+1 then c else if k-depth-1 <= lv then match List.nth l (k-depth-2) with | Projection t -> lift depth t | NoProjection (Name id) -> bad_projs := id :: !bad_projs; mkRel k | NoProjection Anonymous -> errorlabstrm "" (str "Field " ++ pr_id fid ++ str " depends on the " ++ pr_nth (k-depth-1) ++ str " field which has no name.") else mkRel (k-lv) | _ -> map_constr_with_binders succ substrec depth c in let c' = lift 1 c in (* to get [c] defined in ctxt [[params;fields;x:ind]] *) let c'' = substrec 0 c' in if !bad_projs <> [] then raise (NotDefinable (MissingProj (fid,List.rev !bad_projs))); c'' let instantiate_possibly_recursive_type indsp paramdecls fields = let subst = list_map_i (fun i _ -> mkRel i) 1 paramdecls in Termops.substl_rel_context (subst@[mkInd indsp]) fields (* We build projections *) 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 let r = mkInd indsp in let rp = applist (r, Termops.extended_rel_list 0 paramdecls) in let paramargs = Termops.extended_rel_list 1 paramdecls in (*def in [[params;x:rp]]*) let x = match name with Some n -> Name n | None -> Namegen.named_hd (Global.env()) r Anonymous in let fields = instantiate_possibly_recursive_type indsp paramdecls fields in let lifted_fields = Termops.lift_rel_context 1 fields in let (_,kinds,sp_projs,_) = list_fold_left3 (fun (nfi,kinds,sp_projs,subst) coe (fi,optci,ti) impls -> let (sp_projs,subst) = match fi with | Anonymous -> (None::sp_projs,NoProjection fi::subst) | Name fid -> try let ccl = subst_projection fid subst ti in let body = match optci with | Some ci -> subst_projection fid subst ci | None -> (* [ccl] is defined in context [params;x:rp] *) (* [ccl'] is defined in context [params;x:rp;x:rp] *) let ccl' = liftn 1 2 ccl in let p = mkLambda (x, lift 1 rp, ccl') in let branch = it_mkLambda_or_LetIn (mkRel nfi) lifted_fields in let ci = Inductiveops.make_case_info env indsp LetStyle in mkCase (ci, p, mkRel 1, [|branch|]) in let proj = it_mkLambda_or_LetIn (mkLambda (x,rp,body)) paramdecls in let projtyp = it_mkProd_or_LetIn (mkProd (x,rp,ccl)) paramdecls in let kn = try let cie = { const_entry_body = proj; const_entry_secctx = None; const_entry_type = Some projtyp; const_entry_opaque = false } in let k = (DefinitionEntry cie,IsDefinition kind) in let kn = declare_constant ~internal:KernelSilent fid k in Flags.if_verbose message (string_of_id fid ^" is defined"); kn with Type_errors.TypeError (ctx,te) -> 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 impls; if coe then begin let cl = Class.class_of_global (IndRef indsp) in Class.try_add_new_coercion_with_source refi Global ~source:cl end; let proj_args = (*Rel 1 refers to "x"*) paramargs@[mkRel 1] in let constr_fip = applist (constr_fi,proj_args) in (Some kn::sp_projs, Projection constr_fip::subst) with NotDefinable why -> warning_or_error coe indsp why; (None::sp_projs,NoProjection fi::subst) in (nfi-1,(fi, optci=None)::kinds,sp_projs,subst)) (List.length fields,[],[],[]) coers (List.rev fields) (List.rev fieldimpls) in (kinds,sp_projs) let structure_signature ctx = let rec deps_to_evar evm l = match l with [] -> Evd.empty | [(_,_,typ)] -> Evd.add evm (Evarutil.new_untyped_evar()) (Evd.make_evar Environ.empty_named_context_val typ) | (_,_,typ)::tl -> let ev = Evarutil.new_untyped_evar() in let evm = Evd.add evm ev (Evd.make_evar Environ.empty_named_context_val typ) in let new_tl = Util.list_map_i (fun pos (n,c,t) -> n,c, Termops.replace_term (mkRel pos) (mkEvar(ev,[||])) t) 1 tl in deps_to_evar evm new_tl in deps_to_evar Evd.empty (List.rev ctx) open Typeclasses let declare_structure finite infer id idbuild paramimpls params arity fieldimpls fields ?(kind=StructureComponent) ?name is_coe coers sign = let nparams = List.length params and nfields = List.length fields in let args = Termops.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 = id; mind_entry_arity = arity; mind_entry_consnames = [idbuild]; 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 Termops.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 = recursivity_flag_of_kind finite; mind_entry_inds = [mie_ind] } in let kn = Command.declare_mutual_inductive_with_eliminations KernelVerbose mie [(paramimpls,[])] in let rsp = (kn,0) in (* This is ind path of idstruc *) let cstr = (rsp,1) in let kinds,sp_projs = declare_projections rsp ~kind ?name coers fieldimpls fields in let build = ConstructRef cstr in if is_coe then Class.try_add_new_coercion build Global; Recordops.declare_structure(rsp,cstr,List.rev kinds,List.rev sp_projs); if infer then Evd.fold (fun ev evi () -> Recordops.declare_method (ConstructRef cstr) ev sign) sign (); rsp 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, true)) 1 (List.rev (Anonymous :: (List.map pi1 ctx))) let declare_instance_cst glob con pri = let instance = Typeops.type_of_constant (Global.env ()) con in let _, r = decompose_prod_assum instance in match class_of_constr r with | Some (_, (tc, _)) -> add_instance (new_instance tc pri glob (ConstRef con)) | None -> errorlabstrm "" (Pp.strbrk "Constant does not build instances of a declared type class.") let declare_class finite def infer id idbuild paramimpls params arity fieldimpls fields ?(kind=StructureComponent) ?name is_coe coers priorities sign = 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_secctx = None; const_entry_type = class_type; const_entry_opaque = false } in let cst = Declare.declare_constant (snd id) (DefinitionEntry class_entry, IsDefinition Definition) in let inst_type = appvectc (mkConst cst) (Termops.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_secctx = None; const_entry_type = Some proj_type; const_entry_opaque = 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]; Classes.set_typeclass_transparency (EvalConstRef cst) false false; if infer then Evd.fold (fun ev evi _ -> Recordops.declare_method (ConstRef cst) ev sign) sign (); let sub = match List.hd coers with Some b -> Some ((if b then Backward else Forward), List.hd priorities) | None -> None in cref, [Name proj_name, sub, Some proj_cst] | _ -> let idarg = Namegen.next_ident_away (snd id) (Termops.ids_of_context (Global.env())) in let ind = declare_structure BiFinite infer (snd id) idbuild paramimpls params (Option.default (Termops.new_Type ()) arity) fieldimpls fields ~kind:Method ~name:idarg false (List.map (fun _ -> false) fields) sign in let coers = List.map2 (fun coe pri -> Option.map (fun b -> if b then Backward, pri else Forward, pri) coe) coers priorities in IndRef ind, (list_map3 (fun (id, _, _) b y -> (id, b, y)) (List.rev fields) coers (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_iter3 (fun p sub pri -> *) (* if sub then match p with (_, _, Some p) -> declare_instance_cst true p pri | _ -> ()) *) (* k.cl_projs coers priorities; *) add_class k; impl let interp_and_check_sort sort = Option.map (fun sort -> let env = Global.env() and sigma = Evd.empty in let s = interp_constr sigma env sort in if isSort (Reductionops.whd_betadeltaiota env sigma s) then s else user_err_loc (constr_loc sort,"", str"Sort expected.")) sort open Vernacexpr open Autoinstance (* [fs] corresponds to fields and [ps] to parameters; [coers] is a list telling if the corresponding fields must me declared as coercions or subinstances *) let definition_structure (kind,finite,infer,(is_coe,(loc,idstruc)),ps,cfs,idbuild,s) = let cfs,notations = List.split cfs in let cfs,priorities = List.split cfs in 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"; if not (kind = Class false) && List.exists ((<>) None) priorities then error "Priorities only allowed for type class substructures"; (* Now, younger decl in params and fields is on top *) let sc = interp_and_check_sort s in let implpars, params, implfs, fields = States.with_state_protection (fun () -> typecheck_params_and_fields idstruc sc ps notations fs) () in let sign = structure_signature (fields@params) in match kind with | Class def -> let gr = declare_class finite def infer (loc,idstruc) idbuild implpars params sc implfs fields is_coe coers priorities sign in if infer then search_record declare_class_instance gr sign; gr | _ -> let arity = Option.default (Termops.new_Type ()) sc in let implfs = List.map (fun impls -> implpars @ Impargs.lift_implicits (succ (List.length params)) impls) implfs in let ind = declare_structure finite infer idstruc idbuild implpars params arity implfs fields is_coe (List.map (fun coe -> coe <> None) coers) sign in if infer then search_record declare_record_instance (ConstructRef (ind,1)) sign; IndRef ind