summaryrefslogtreecommitdiff
path: root/toplevel/record.ml
diff options
context:
space:
mode:
Diffstat (limited to 'toplevel/record.ml')
-rw-r--r--toplevel/record.ml176
1 files changed, 99 insertions, 77 deletions
diff --git a/toplevel/record.ml b/toplevel/record.ml
index 4c0e34cd..320030e1 100644
--- a/toplevel/record.ml
+++ b/toplevel/record.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: record.ml 12080 2009-04-11 16:56:20Z herbelin $ *)
+(* $Id$ *)
open Pp
open Util
@@ -31,30 +31,27 @@ open Topconstr
(********** definition d'un record (structure) **************)
-let interp_evars evdref env ?(impls=([],[])) k typ =
- let typ' = intern_gen true ~impls (Evd.evars_of !evdref) env typ in
+let interp_evars evdref env impls k typ =
+ let impls = set_internalization_env_params impls [] in
+ let typ' = intern_gen true ~impls !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 (na, (Constrintern.Method, [], impl, Notation.compute_arguments_scope typ))
-
-let interp_fields_evars isevars env nots l =
+let interp_fields_evars evars 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 impls =
+ 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 na -> (fst impls, mk_interning_data env na impl t' :: snd impls)
+ | Name id -> (id, compute_internalization_data env Constrintern.Method t' impl) :: impls
in
let d = (i,b',t') in
- (* 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 impls' = set_internalization_env_params impls [] in
+ List.iter (Metasyntax.set_notation_for_interpretation 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)
@@ -64,7 +61,7 @@ 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.create_evar_defs Evd.empty) in
+ let evars = ref 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
@@ -73,7 +70,7 @@ let typecheck_params_and_fields id t ps nots fs =
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 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
@@ -84,7 +81,7 @@ let typecheck_params_and_fields id t ps nots fs =
let degenerate_decl (na,b,t) =
let id = match na with
| Name id -> id
- | Anonymous -> anomaly "Unnamed record variable" in
+ | Anonymous -> anomaly "Unnamed record variable" in
match b with
| None -> (id, Entries.LocalAssum t)
| Some b -> (id, Entries.LocalDef b)
@@ -99,21 +96,21 @@ let warning_or_error coe indsp err =
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_coma pr_id projs ++ spc () ++ str have ++
+ 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 ++
+ (pr_id fi ++
strbrk" cannot be defined because it is informative and " ++
Printer.pr_inductive (Global.env()) indsp ++
- strbrk " is not.")
+ strbrk " is not.")
| ElimArity (_,_,_,_,Some (_,_,StrongEliminationOnNonSmallType)) ->
- (pr_id fi ++
+ (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;
@@ -136,20 +133,20 @@ let subst_projection fid l c =
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
+ 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 -> assert false
- else
+ 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
+ if !bad_projs <> [] then
raise (NotDefinable (MissingProj (fid,List.rev !bad_projs)));
c''
@@ -165,7 +162,7 @@ let declare_projections indsp ?(kind=StructureComponent) ?name coers fieldimpls
let r = mkInd indsp in
let rp = applist (r, extended_rel_list 0 paramdecls) in
let paramargs = extended_rel_list 1 paramdecls in (*def in [[params;x:rp]]*)
- let x = match name with Some n -> Name n | None -> Termops.named_hd (Global.env()) r Anonymous in
+ 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 = lift_rel_context 1 fields in
let (_,kinds,sp_projs,_) =
@@ -222,8 +219,24 @@ let declare_projections indsp ?(kind=StructureComponent) ?name coers fieldimpls
(List.length fields,[],[],[]) coers (List.rev fields) (List.rev fieldimpls)
in (kinds,sp_projs)
-let declare_structure finite id idbuild paramimpls params arity fieldimpls fields
- ?(kind=StructureComponent) ?name is_coe coers =
+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 = extended_rel_list nfields params in
let ind = applist (mkRel (1+nparams+nfields), args) in
@@ -238,7 +251,7 @@ let declare_structure finite id idbuild paramimpls params arity fieldimpls field
but isn't *)
(* there is probably a way to push this to "declare_mutual" *)
begin match finite with
- | BiFinite ->
+ | 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."
| _ -> ()
@@ -248,44 +261,40 @@ let declare_structure finite id idbuild paramimpls params arity fieldimpls field
mind_entry_record = true;
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
+(* TODO : maybe switch to KernelVerbose *)
+ let kn = Command.declare_mutual_inductive_with_eliminations KernelSilent 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 (rsp,1) in
- if is_coe then Class.try_add_new_coercion build Global;
- Recordops.declare_structure(rsp,(rsp,1),List.rev kinds,List.rev sp_projs);
- kn,0
+ 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
+ let explname =
+ match name with
| Name n -> Some n
| Anonymous -> None
- in ExplByPos (i, explname), (true, true))
+ in ExplByPos (i, explname), (true, 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
+ let _, r = decompose_prod_assum instance in
match class_of_constr r with
- | Some tc -> add_instance (new_instance tc None glob con)
+ | Some tc -> add_instance (new_instance tc None glob (ConstRef 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 =
+let declare_class finite def infer id idbuild paramimpls params arity fieldimpls fields
+ ?(kind=StructureComponent) ?name is_coe coers 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
@@ -303,37 +312,37 @@ let declare_class finite def id idbuild paramimpls params arity fieldimpls field
const_entry_boxed = false }
in
let cst = Declare.declare_constant (snd id)
- (DefinitionEntry class_entry, IsDefinition Definition)
+ (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 =
+ 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)
+ (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]
+ 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;
+ if infer then Evd.fold (fun ev evi _ -> Recordops.declare_method (ConstRef cst) ev sign) sign ();
+ 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
+ let idarg = Namegen.next_ident_away (snd id) (ids_of_context (Global.env())) in
+ let ind = declare_structure BiFinite infer (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)
+ ~kind:Method ~name:idarg false (List.map (fun _ -> false) fields) sign
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) ->
+ 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)
@@ -345,16 +354,24 @@ let declare_class finite def id idbuild paramimpls params arity fieldimpls field
cl_props = fields;
cl_projs = projs }
in
- List.iter2 (fun p sub ->
+ 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
+ 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 boolean
+(* [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 (kind,finite,(is_coe,(loc,idstruc)),ps,cfs,idbuild,s) =
+let definition_structure (kind,finite,infer,(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
@@ -364,16 +381,21 @@ let definition_structure (kind,finite,(is_coe,(loc,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 sc = Option.map mkSort s in
- let implpars, params, implfs, fields =
+ 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
+ typecheck_params_and_fields idstruc sc ps notations fs) () in
+ let sign = structure_signature (fields@params) in
match kind with
- | Class b ->
- declare_class finite b (loc,idstruc) idbuild implpars params sc implfs fields is_coe coers
+ | Class def ->
+ let gr = declare_class finite def infer (loc,idstruc) idbuild
+ implpars params sc implfs fields is_coe coers sign in
+ if infer then search_record declare_class_instance gr sign;
+ gr
| _ ->
- let arity = Option.cata (fun x -> x) (new_Type ()) sc in
+ let arity = Option.default (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)
+ (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 coers sign in
+ if infer then search_record declare_record_instance (ConstructRef (ind,1)) sign;
+ IndRef ind
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-20 16:35:22 +0000