diff options
Diffstat (limited to 'toplevel/record.ml')
| -rw-r--r-- | toplevel/record.ml | 579 |
1 files changed, 0 insertions, 579 deletions
diff --git a/toplevel/record.ml b/toplevel/record.ml deleted file mode 100644 index ef09f6fa..00000000 --- a/toplevel/record.ml +++ /dev/null @@ -1,579 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -open Pp -open CErrors -open Util -open Names -open Globnames -open Nameops -open Term -open Vars -open Environ -open Declarations -open Entries -open Declare -open Constrintern -open Decl_kinds -open Type_errors -open Constrexpr -open Constrexpr_ops -open Goptions -open Sigma.Notations -open Context.Rel.Declaration - -(********** definition d'un record (structure) **************) - -(** Flag governing use of primitive projections. Disabled by default. *) -let primitive_flag = ref false -let _ = - declare_bool_option - { optsync = true; - optdepr = false; - optname = "use of primitive projections"; - optkey = ["Primitive";"Projections"]; - optread = (fun () -> !primitive_flag) ; - optwrite = (fun b -> primitive_flag := b) } - -let typeclasses_strict = ref false -let _ = - declare_bool_option - { optsync = true; - optdepr = false; - optname = "strict typeclass resolution"; - optkey = ["Typeclasses";"Strict";"Resolution"]; - optread = (fun () -> !typeclasses_strict); - optwrite = (fun b -> typeclasses_strict := b); } - -let typeclasses_unique = ref false -let _ = - declare_bool_option - { optsync = true; - optdepr = false; - optname = "unique typeclass instances"; - optkey = ["Typeclasses";"Unique";"Instances"]; - optread = (fun () -> !typeclasses_unique); - optwrite = (fun b -> typeclasses_unique := b); } - -let interp_fields_evars env evars impls_env nots l = - List.fold_left2 - (fun (env, uimpls, params, impls) no ((loc, i), b, t) -> - let t', impl = interp_type_evars_impls env evars ~impls t in - let b' = Option.map (fun x -> fst (interp_casted_constr_evars_impls env evars ~impls x t')) b in - let impls = - match i with - | Anonymous -> impls - | Name id -> Id.Map.add id (compute_internalization_data env Constrintern.Method t' impl) impls - 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 d (env, univ) -> - let univ = - 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)) - l (env, Univ.type0m_univ) - -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, Misctypes.IntroAnonymous, None)) - -let binders_of_decls = List.map binder_of_decl - -let typecheck_params_and_fields def id pl t ps nots fs = - let env0 = Global.env () in - let ctx = Evd.make_evar_universe_context env0 pl in - let evars = ref (Evd.from_ctx ctx) in - let _ = - let error bk (loc, name) = - match bk, name with - | Default _, Anonymous -> - 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 - | 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_all env !evars s in - (match kind_of_term sred with - | Sort s' -> - (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 = 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 (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 - let sigma = - Pretyping.solve_remaining_evars Pretyping.all_and_fail_flags env_ar !evars (Evd.empty,!evars) in - let evars, nf = Evarutil.nf_evars_and_universes sigma in - let arity = nf t' in - let arity, evars = - 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 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 && - 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 = 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 decl = - let id = match get_name decl with - | Name id -> id - | Anonymous -> anomaly (Pp.str "Unnamed record variable") in - 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 - (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.") - | 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 Feedback.msg_info (hov 0 st) - -type field_status = - | NoProjection of Name.t - | 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 not (List.is_empty !bad_projs) then - raise (NotDefinable (MissingProj (fid,List.rev !bad_projs))); - c'' - -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 - let (mib,mip) = Global.lookup_inductive indsp in - let u = Declareops.inductive_instance mib in - let paramdecls = Inductive.inductive_paramdecls (mib, u) in - let poly = mib.mind_polymorphic in - 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, 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 - let primitive = - if !primitive_flag then - let is_primitive = - match mib.mind_record with - | Some (Some _) -> true - | Some None | None -> false - in - if not is_primitive then - 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 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 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 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 - 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 - try - let entry = { - const_entry_body = - Future.from_val (Safe_typing.mk_pure_proof proj); - const_entry_secctx = None; - const_entry_type = Some projtyp; - const_entry_polymorphic = poly; - const_entry_universes = - if poly then ctx else Univ.UContext.empty; - const_entry_opaque = false; - const_entry_inline_code = false; - const_entry_feedback = None } in - let k = (DefinitionEntry entry,IsDefinition kind) in - let kn = declare_constant ~internal:InternalTacticRequest fid k in - let constr_fip = - let proj_args = (*Rel 1 refers to "x"*) paramargs@[mkRel 1] in - applist (mkConstU (kn,u),proj_args) - in - Declare.definition_message fid; - kn, constr_fip - with Type_errors.TypeError (ctx,te) -> - raise (NotDefinable (BadTypedProj (fid,ctx,te))) - in - let refi = ConstRef 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 ~local:false poly ~source:cl - end; - 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, 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 - | [decl] -> - let env = Environ.empty_named_context_val 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 - | decl::tl -> - let env = Environ.empty_named_context_val 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 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) - -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 = 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 = - match name with - | None -> Id.of_string (Unicode.lowercase_first_char (Id.to_string id)) - | Some n -> n - in - let mie_ind = - { mind_entry_typename = id; - mind_entry_arity = arity; - mind_entry_template = not poly && template; - mind_entry_consnames = [idbuild]; - mind_entry_lc = [type_constructor] } - in - let mie = - { mind_entry_params = List.map degenerate_decl params; - mind_entry_record = Some (if !primitive_flag then Some binder_name else None); - mind_entry_finite = finite; - mind_entry_inds = [mie_ind]; - mind_entry_polymorphic = poly; - mind_entry_private = None; - 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 - let kinds,sp_projs = declare_projections rsp ~kind binder_name coers fieldimpls fields in - let build = ConstructRef cstr in - let () = if is_coe then Class.try_add_new_coercion build ~local:false poly in - Recordops.declare_structure(rsp,cstr,List.rev kinds,List.rev sp_projs); - 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 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 = - let fieldimpls = - (* Make the class implicit in the projections, and the params if applicable. *) - let len = List.length params in - let impls = implicits_of_context params in - List.map (fun x -> impls @ Impargs.lift_implicits (succ len) x) fieldimpls - in - let binder_name = Namegen.next_ident_away (snd id) (Termops.ids_of_context (Global.env())) in - let impl, projs = - match fields with - | [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_entry = - 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 - let cstu = (cst, if poly then Univ.UContext.instance ctx else Univ.Instance.empty) in - let inst_type = appvectc (mkConstU cstu) - (Termops.rel_vect 0 (List.length params)) in - let proj_type = - it_mkProd_or_LetIn (mkProd(Name binder_name, inst_type, lift 1 field)) params in - let proj_body = - it_mkLambda_or_LetIn (mkLambda (Name binder_name, inst_type, mkRel 1)) params in - let proj_entry = - Declare.definition_entry ~types:proj_type ~poly - ~univs:(if poly then ctx else Univ.UContext.empty) proj_body - 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; - 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 ind = declare_structure BiFinite poly ctx (snd id) idbuild paramimpls - params arity template fieldimpls fields - ~kind:Method ~name:binder_name 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 - 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 decl -> - match Typeclasses.class_of_constr (get_type decl) with - | Some (_, ((cl,_), _)) -> Some (cl.cl_impl, true) - | None -> None) - params, params - in - let k = - { cl_impl = impl; - cl_strict = !typeclasses_strict; - cl_unique = !typeclasses_unique; - cl_context = ctx_context; - cl_props = fields; - cl_projs = projs } - in - add_class k; impl - - -let add_constant_class cst = - let ty = Universes.unsafe_type_of_global (ConstRef cst) in - let ctx, arity = decompose_prod_assum ty in - let tc = - { cl_impl = ConstRef cst; - cl_context = (List.map (const None) ctx, ctx); - cl_props = [LocalAssum (Anonymous, arity)]; - cl_projs = []; - cl_strict = !typeclasses_strict; - cl_unique = !typeclasses_unique - } - in add_class tc; - set_typeclass_transparency (EvalConstRef cst) false false - -let add_inductive_class ind = - let mind, oneind = Global.lookup_inductive ind in - let k = - let ctx = oneind.mind_arity_ctxt in - let inst = Univ.UContext.instance mind.mind_universes in - let ty = Inductive.type_of_inductive - (push_rel_context ctx (Global.env ())) - ((mind,oneind),inst) - in - { cl_impl = IndRef ind; - cl_context = List.map (const None) ctx, ctx; - cl_props = [LocalAssum (Anonymous, ty)]; - cl_projs = []; - cl_strict = !typeclasses_strict; - cl_unique = !typeclasses_unique } - in add_class k - -let declare_existing_class g = - match g with - | ConstRef x -> add_constant_class x - | IndRef x -> add_inductive_class x - | _ -> user_err_loc (Loc.dummy_loc, "declare_existing_class", - Pp.str"Unsupported class type, only constants and inductives are allowed") - -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. *) -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 - 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_f Id.compare allnames) - then error "Two objects have the same name"; - let isnot_class = match kind with Class false -> false | _ -> true in - if isnot_class && List.exists (fun opt -> not (Option.is_empty opt)) priorities then - error "Priorities only allowed for type class substructures"; - (* Now, younger decl in params and fields is on top *) - let (pl, ctx), arity, template, implpars, params, implfs, fields = - States.with_state_protection (fun () -> - 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 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 - idbuild implpars params arity template implfs - fields is_coe (List.map (fun coe -> not (Option.is_empty coe)) coers) sign in - IndRef ind - in - Universes.register_universe_binders gr pl; - gr |