diff options
Diffstat (limited to 'toplevel/record.ml')
| -rw-r--r-- | toplevel/record.ml | 175 |
1 files changed, 100 insertions, 75 deletions
diff --git a/toplevel/record.ml b/toplevel/record.ml index 04da628c..ef09f6fa 100644 --- a/toplevel/record.ml +++ b/toplevel/record.ml @@ -7,13 +7,12 @@ (************************************************************************) open Pp -open Errors +open CErrors open Util open Names open Globnames open Nameops open Term -open Context open Vars open Environ open Declarations @@ -25,6 +24,8 @@ open Type_errors open Constrexpr open Constrexpr_ops open Goptions +open Sigma.Notations +open Context.Rel.Declaration (********** definition d'un record (structure) **************) @@ -69,16 +70,19 @@ let interp_fields_evars env evars impls_env nots l = | Anonymous -> impls | Name id -> Id.Map.add id (compute_internalization_data env Constrintern.Method t' impl) impls in - let d = (i,b',t') in + let d = match b' with + | None -> LocalAssum (i,t') + | Some b' -> LocalDef (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 compute_constructor_level evars env l = - List.fold_right (fun (n,b,t as d) (env, univ) -> + List.fold_right (fun d (env, univ) -> let univ = - if b = None then - let s = Retyping.get_sort_of env evars t in + if is_local_assum d then + let s = Retyping.get_sort_of env evars (get_type d) in Univ.sup (univ_of_sort s) univ else univ in (push_rel d env, univ)) @@ -103,27 +107,33 @@ let typecheck_params_and_fields def id pl t ps nots fs = in List.iter (function LocalRawDef (b, _) -> error default_binder_kind b - | LocalRawAssum (ls, bk, ce) -> List.iter (error bk) ls) ps + | LocalRawAssum (ls, bk, ce) -> List.iter (error bk) ls + | LocalPattern _ -> assert false) ps in let impls_env, ((env1,newps), imps) = interp_context_evars env0 evars ps in let t', template = match t with | Some t -> let env = push_rel_context newps env0 in + let poly = + match t with + | CSort (_, Misctypes.GType []) -> true | _ -> false in let s = interp_type_evars env evars ~impls:empty_internalization_env t in - let sred = Reductionops.whd_betadeltaiota env !evars s in + let sred = Reductionops.whd_all env !evars s in (match kind_of_term sred with | Sort s' -> - (match Evd.is_sort_variable !evars s' with - | Some l -> evars := Evd.make_flexible_variable !evars true (* (not def) *) l; - sred, true - | None -> s, false) + (if poly then + match Evd.is_sort_variable !evars s' with + | Some l -> evars := Evd.make_flexible_variable !evars true l; + sred, true + | None -> s, false + else s, false) | _ -> user_err_loc (constr_loc t,"", str"Sort expected.")) | None -> - let uvarkind = if (* not def *) true then Evd.univ_flexible_alg else Evd.univ_flexible in - mkSort (Evarutil.evd_comb0 (Evd.new_sort_variable uvarkind) evars), false + let uvarkind = Evd.univ_flexible_alg in + mkSort (Evarutil.evd_comb0 (Evd.new_sort_variable uvarkind) evars), true 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 env_ar = push_rel_context newps (push_rel (LocalAssum (Name id,fullarity)) env0) in let env2,impls,newfs,data = interp_fields_evars env_ar evars impls_env nots (binders_of_decls fs) in @@ -135,43 +145,51 @@ let typecheck_params_and_fields def id pl t ps nots fs = let _, univ = compute_constructor_level evars env_ar newfs in let ctx, aritysort = Reduction.dest_arity env0 arity in assert(List.is_empty ctx); (* Ensured by above analysis *) - if Sorts.is_prop aritysort || - (Sorts.is_set aritysort && is_impredicative_set env0) then + if not def && (Sorts.is_prop aritysort || + (Sorts.is_set aritysort && is_impredicative_set env0)) then arity, evars else let evars = Evd.set_leq_sort env_ar evars (Type univ) aritysort in - if Univ.is_small_univ univ then - (* We can assume that the level aritysort is not constrained - and clear it. *) - mkArity (ctx, Sorts.sort_of_univ univ), - Evd.set_eq_sort env_ar evars (Prop Pos) aritysort - else arity, evars + if Univ.is_small_univ univ && + Option.cata (Evd.is_flexible_level evars) false (Evd.is_sort_variable evars aritysort) then + (* We can assume that the level in aritysort is not constrained + and clear it, if it is flexible *) + mkArity (ctx, Sorts.sort_of_univ univ), + Evd.set_eq_sort env_ar evars (Prop Pos) aritysort + else arity, evars in let evars, nf = Evarutil.nf_evars_and_universes evars in - let newps = map_rel_context nf newps in - let newfs = map_rel_context nf 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); + let newps = Context.Rel.map nf newps in + let newfs = Context.Rel.map nf newfs in + let ce t = Pretyping.check_evars env0 Evd.empty evars t in + List.iter (iter_constr ce) (List.rev newps); + List.iter (iter_constr ce) (List.rev newfs); Evd.universe_context ?names:pl evars, nf arity, template, imps, newps, impls, newfs -let degenerate_decl (na,b,t) = - let id = match na with +let degenerate_decl decl = + let id = match get_name decl with | Name id -> id | Anonymous -> anomaly (Pp.str "Unnamed record variable") in - match b with - | None -> (id, LocalAssum t) - | Some b -> (id, LocalDef b) + match decl with + | LocalAssum (_,t) -> (id, LocalAssumEntry t) + | LocalDef (_,b,_) -> (id, LocalDefEntry b) type record_error = | MissingProj of Id.t * Id.t list | BadTypedProj of Id.t * env * Type_errors.type_error +let warn_cannot_define_projection = + CWarnings.create ~name:"cannot-define-projection" ~category:"records" + (fun msg -> hov 0 msg) + +(* If a projection is not definable, we throw an error if the user +asked it to be a coercion. Otherwise, we just print an info +message. The user might still want to name the field of the record. *) 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(Id.to_string fi) ++ + (pr_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.") @@ -191,7 +209,7 @@ let warning_or_error coe indsp err = (pr_id fi ++ strbrk " cannot be defined because it is not typable.") in if coe then errorlabstrm "structure" st; - Flags.if_verbose msg_warning (hov 0 st) + Flags.if_verbose Feedback.msg_info (hov 0 st) type field_status = | NoProjection of Name.t @@ -234,6 +252,12 @@ let instantiate_possibly_recursive_type indu paramdecls fields = let subst = List.map_i (fun i _ -> mkRel i) 1 paramdecls in Termops.substl_rel_context (subst@[mkIndU indu]) fields +let warn_non_primitive_record = + CWarnings.create ~name:"non-primitive-record" ~category:"record" + (fun (env,indsp) -> + (hov 0 (str "The record " ++ Printer.pr_inductive env indsp ++ + strbrk" could not be defined as a primitive record"))) + (* We build projections *) let declare_projections indsp ?(kind=StructureComponent) binder_name coers fieldimpls fields = let env = Global.env() in @@ -244,8 +268,8 @@ let declare_projections indsp ?(kind=StructureComponent) binder_name coers field let ctx = Univ.instantiate_univ_context mib.mind_universes in let indu = indsp, u in let r = mkIndU (indsp,u) 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 rp = applist (r, Context.Rel.to_extended_list 0 paramdecls) in + let paramargs = Context.Rel.to_extended_list 1 paramdecls in (*def in [[params;x:rp]]*) let x = Name binder_name in let fields = instantiate_possibly_recursive_type indu paramdecls fields in let lifted_fields = Termops.lift_rel_context 1 fields in @@ -257,31 +281,31 @@ let declare_projections indsp ?(kind=StructureComponent) binder_name coers field | Some None | None -> false in if not is_primitive then - Flags.if_verbose msg_warning - (hov 0 (str "The record " ++ Printer.pr_inductive env indsp ++ - str" could not be defined as a primitive record")); + warn_non_primitive_record (env,indsp); is_primitive else false in let (_,_,kinds,sp_projs,_) = List.fold_left3 - (fun (nfi,i,kinds,sp_projs,subst) coe (fi,optci,ti) impls -> + (fun (nfi,i,kinds,sp_projs,subst) coe decl impls -> + let fi = get_name decl in + let ti = get_type decl in let (sp_projs,i,subst) = match fi with | Anonymous -> (None::sp_projs,i,NoProjection fi::subst) | Name fid -> try let kn, term = - if optci = None && primitive then + if is_local_assum decl && primitive then (** Already defined in the kernel silently *) let kn = destConstRef (Nametab.locate (Libnames.qualid_of_ident fid)) in Declare.definition_message fid; kn, mkProj (Projection.make kn false,mkRel 1) else let ccl = subst_projection fid subst ti in - let body = match optci with - | Some ci -> subst_projection fid subst ci - | None -> + let body = match decl with + | LocalDef (_,ci,_) -> subst_projection fid subst ci + | LocalAssum _ -> (* [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 @@ -323,28 +347,32 @@ let declare_projections indsp ?(kind=StructureComponent) binder_name coers field let cl = Class.class_of_global (IndRef indsp) in Class.try_add_new_coercion_with_source refi ~local:false poly ~source:cl end; - let i = if Option.is_empty optci then i+1 else i in + let i = if is_local_assum decl then i+1 else i in (Some kn::sp_projs, i, Projection term::subst) with NotDefinable why -> warning_or_error coe indsp why; (None::sp_projs,i,NoProjection fi::subst) in - (nfi-1,i,(fi, Option.is_empty optci)::kinds,sp_projs,subst)) + (nfi-1,i,(fi, is_local_assum decl)::kinds,sp_projs,subst)) (List.length fields,0,[],[],[]) 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)] -> + | [decl] -> let env = Environ.empty_named_context_val in - let (evm, _) = Evarutil.new_pure_evar env evm typ in + let evm = Sigma.Unsafe.of_evar_map evm in + let Sigma (_, evm, _) = Evarutil.new_pure_evar env evm (get_type decl) in + let evm = Sigma.to_evar_map evm in evm - | (_,_,typ)::tl -> + | decl::tl -> let env = Environ.empty_named_context_val in - let (evm, ev) = Evarutil.new_pure_evar env evm typ in + let evm = Sigma.Unsafe.of_evar_map evm in + let Sigma (ev, evm, _) = Evarutil.new_pure_evar env evm (get_type decl) in + let evm = Sigma.to_evar_map evm 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 + (fun pos decl -> + map_type (fun t -> Termops.replace_term (mkRel pos) (mkEvar(ev,[||])) t) decl) 1 tl in deps_to_evar evm new_tl in deps_to_evar Evd.empty (List.rev ctx) @@ -353,7 +381,7 @@ open Typeclasses let declare_structure finite poly ctx id idbuild paramimpls params arity template 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 args = Context.Rel.to_extended_list nfields params in let ind = applist (mkRel (1+nparams+nfields), args) in let type_constructor = it_mkProd_or_LetIn ind fields in let binder_name = @@ -375,7 +403,9 @@ let declare_structure finite poly ctx id idbuild paramimpls params arity templat mind_entry_inds = [mie_ind]; mind_entry_polymorphic = poly; mind_entry_private = None; - mind_entry_universes = ctx } in + mind_entry_universes = ctx; + } + in let kn = Command.declare_mutual_inductive_with_eliminations mie [] [(paramimpls,[])] in let rsp = (kn,0) in (* This is ind path of idstruc *) let cstr = (rsp,1) in @@ -392,7 +422,7 @@ let implicits_of_context ctx = | Name n -> Some n | Anonymous -> None in ExplByPos (i, explname), (true, true, true)) - 1 (List.rev (Anonymous :: (List.map pi1 ctx))) + 1 (List.rev (Anonymous :: (List.map get_name ctx))) let declare_class finite def poly ctx id idbuild paramimpls params arity template fieldimpls fields ?(kind=StructureComponent) is_coe coers priorities sign = @@ -405,11 +435,11 @@ let declare_class finite def poly ctx id idbuild paramimpls params arity let binder_name = Namegen.next_ident_away (snd id) (Termops.ids_of_context (Global.env())) in let impl, projs = match fields with - | [(Name proj_name, _, field)] when def -> + | [LocalAssum (Name proj_name, field) | LocalDef (Name proj_name, _, field)] when def -> let class_body = it_mkLambda_or_LetIn field params in - let _class_type = it_mkProd_or_LetIn arity params in + let class_type = it_mkProd_or_LetIn arity params in let class_entry = - Declare.definition_entry (* ?types:class_type *) ~poly ~univs:ctx class_body in + Declare.definition_entry ~types:class_type ~poly ~univs:ctx class_body in let cst = Declare.declare_constant (snd id) (DefinitionEntry class_entry, IsDefinition Definition) in @@ -446,13 +476,13 @@ let declare_class finite def poly ctx id idbuild paramimpls params arity if b then Backward, pri else Forward, pri) coe) coers priorities in - let l = List.map3 (fun (id, _, _) b y -> (id, b, y)) + let l = List.map3 (fun decl b y -> get_name decl, b, y) (List.rev fields) coers (Recordops.lookup_projections ind) in IndRef ind, l in let ctx_context = - List.map (fun (na, b, t) -> - match Typeclasses.class_of_constr t with + List.map (fun decl -> + match Typeclasses.class_of_constr (get_type decl) with | Some (_, ((cl,_), _)) -> Some (cl.cl_impl, true) | None -> None) params, params @@ -474,7 +504,7 @@ let add_constant_class cst = let tc = { cl_impl = ConstRef cst; cl_context = (List.map (const None) ctx, ctx); - cl_props = [(Anonymous, None, arity)]; + cl_props = [LocalAssum (Anonymous, arity)]; cl_projs = []; cl_strict = !typeclasses_strict; cl_unique = !typeclasses_unique @@ -487,19 +517,13 @@ let add_inductive_class ind = let k = let ctx = oneind.mind_arity_ctxt in let inst = Univ.UContext.instance mind.mind_universes in - let map = function - | (_, Some _, _) -> None - | (_, None, t) -> Some (lazy t) - in - let args = List.map_filter map ctx in - let ty = Inductive.type_of_inductive_knowing_parameters + let ty = Inductive.type_of_inductive (push_rel_context ctx (Global.env ())) ((mind,oneind),inst) - (Array.of_list args) in { cl_impl = IndRef ind; cl_context = List.map (const None) ctx, ctx; - cl_props = [Anonymous, None, ty]; + cl_props = [LocalAssum (Anonymous, ty)]; cl_projs = []; cl_strict = !typeclasses_strict; cl_unique = !typeclasses_unique } @@ -516,7 +540,7 @@ open Vernacexpr (* [fs] corresponds to fields and [ps] to parameters; [coers] is a list telling if the corresponding fields must me declared as coercions - or subinstances *) + or subinstances. *) let definition_structure (kind,poly,finite,(is_coe,((loc,idstruc),pl)),ps,cfs,idbuild,s) = let cfs,notations = List.split cfs in let cfs,priorities = List.split cfs in @@ -537,15 +561,16 @@ let definition_structure (kind,poly,finite,(is_coe,((loc,idstruc),pl)),ps,cfs,id typecheck_params_and_fields (kind = Class true) idstruc pl s ps notations fs) () in let sign = structure_signature (fields@params) in let gr = match kind with - | Class def -> - let gr = declare_class finite def poly ctx (loc,idstruc) idbuild + | Class def -> + let priorities = List.map (fun id -> {hint_priority = id; hint_pattern = None}) priorities in + let gr = declare_class finite def poly ctx (loc,idstruc) idbuild implpars params arity template implfs fields is_coe coers priorities sign in gr | _ -> let implfs = List.map (fun impls -> implpars @ Impargs.lift_implicits (succ (List.length params)) impls) implfs in - let ind = declare_structure finite poly ctx idstruc + let ind = declare_structure finite poly ctx idstruc idbuild implpars params arity template implfs fields is_coe (List.map (fun coe -> not (Option.is_empty coe)) coers) sign in IndRef ind |