summaryrefslogtreecommitdiff
path: root/toplevel/record.ml
diff options
context:
space:
mode:
authorGravatar Stephane Glondu <steph@glondu.net>2012-01-12 16:02:20 +0100
committerGravatar Stephane Glondu <steph@glondu.net>2012-01-12 16:02:20 +0100
commit97fefe1fcca363a1317e066e7f4b99b9c1e9987b (patch)
tree97ec6b7d831cc5fb66328b0c63a11db1cbb2f158 /toplevel/record.ml
parent300293c119981054c95182a90c829058530a6b6f (diff)
Imported Upstream version 8.4~betaupstream/8.4_beta
Diffstat (limited to 'toplevel/record.ml')
-rw-r--r--toplevel/record.ml110
1 files changed, 63 insertions, 47 deletions
diff --git a/toplevel/record.ml b/toplevel/record.ml
index ee9b8d66..86849cbb 100644
--- a/toplevel/record.ml
+++ b/toplevel/record.ml
@@ -1,20 +1,17 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: record.ml 14641 2011-11-06 11:59:10Z herbelin $ *)
-
open Pp
open Util
open Names
open Libnames
open Nameops
open Term
-open Termops
open Environ
open Declarations
open Entries
@@ -33,10 +30,10 @@ open Topconstr
let interp_evars evdref env impls k typ =
let typ' = intern_gen true ~impls !evdref env typ in
- let imps = Implicit_quantifiers.implicits_of_rawterm typ' in
+ let imps = Implicit_quantifiers.implicits_of_glob_constr typ' in
imps, Pretyping.Default.understand_tcc_evars evdref env k typ'
-let interp_fields_evars evars env nots l =
+let interp_fields_evars evars env impls_env nots l =
List.fold_left2
(fun (env, uimpls, params, impls) no ((loc, i), b, t) ->
let impl, t' = interp_evars evars env impls Pretyping.IsType t in
@@ -44,12 +41,12 @@ let interp_fields_evars evars env nots l =
let impls =
match i with
| Anonymous -> impls
- | Name id -> (id, compute_internalization_data env Constrintern.Method t' impl) :: 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, [], [], []) nots l
+ (env, [], [], impls_env) nots l
let binder_of_decl = function
| Vernacexpr.AssumExpr(n,t) -> (n,None,t)
@@ -60,11 +57,23 @@ 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 (env1,newps), imps = interp_context_evars evars env0 ps in
- let fullarity = it_mkProd_or_LetIn (Option.cata (fun x -> x) (new_Type ()) t) newps 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 nots (binders_of_decls fs)
+ 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
@@ -153,7 +162,7 @@ let subst_projection fid l c =
let instantiate_possibly_recursive_type indsp paramdecls fields =
let subst = list_map_i (fun i _ -> mkRel i) 1 paramdecls in
- substl_rel_context (subst@[mkInd indsp]) fields
+ Termops.substl_rel_context (subst@[mkInd indsp]) fields
(* We build projections *)
let declare_projections indsp ?(kind=StructureComponent) ?name coers fieldimpls fields =
@@ -161,11 +170,11 @@ let declare_projections indsp ?(kind=StructureComponent) ?name coers fieldimpls
let (mib,mip) = Global.lookup_inductive indsp in
let paramdecls = mib.mind_params_ctxt in
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 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 = lift_rel_context 1 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 ->
@@ -194,11 +203,11 @@ let declare_projections indsp ?(kind=StructureComponent) ?name coers fieldimpls
try
let cie = {
const_entry_body = proj;
+ const_entry_secctx = None;
const_entry_type = Some projtyp;
- const_entry_opaque = false;
- const_entry_boxed = Flags.boxed_definitions() } in
+ const_entry_opaque = false } in
let k = (DefinitionEntry cie,IsDefinition kind) in
- let kn = declare_internal_constant fid k 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) ->
@@ -208,7 +217,7 @@ let declare_projections indsp ?(kind=StructureComponent) ?name coers fieldimpls
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 cl
+ 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
@@ -239,7 +248,7 @@ 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 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 =
@@ -253,7 +262,7 @@ let declare_structure finite infer id idbuild paramimpls params arity fieldimpls
(* there is probably a way to push this to "declare_mutual" *)
begin match finite with
| BiFinite ->
- if dependent (mkRel (nparams+1)) (it_mkProd_or_LetIn mkProp fields) then
+ 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;
@@ -282,18 +291,15 @@ let implicits_of_context ctx =
in ExplByPos (i, explname), (true, true, true))
1 (List.rev (Anonymous :: (List.map pi1 ctx)))
-let qualid_of_con c =
- Qualid (dummy_loc, shortest_qualid_of_global Idset.empty (ConstRef c))
-
-let declare_instance_cst glob con =
+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 None glob (ConstRef con))
+ | 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 sign =
+ ?(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
@@ -307,21 +313,21 @@ let declare_class finite def infer id idbuild paramimpls params arity fieldimpls
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;
- const_entry_boxed = false }
+ const_entry_opaque = false }
in
let cst = Declare.declare_constant (snd id)
(DefinitionEntry class_entry, IsDefinition Definition)
in
- let inst_type = appvectc (mkConst cst) (rel_vect 0 (List.length params)) 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;
- const_entry_boxed = false }
+ const_entry_opaque = false }
in
let proj_cst = Declare.declare_constant proj_name
(DefinitionEntry proj_entry, IsDefinition Definition)
@@ -329,22 +335,27 @@ let declare_class finite def infer id idbuild paramimpls params arity fieldimpls
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;
+ Classes.set_typeclass_transparency (EvalConstRef cst) false false;
if infer then Evd.fold (fun ev evi _ -> Recordops.declare_method (ConstRef cst) ev sign) sign ();
- cref, [proj_name, Some proj_cst]
+ 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) (ids_of_context (Global.env())) in
+ 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.cata (fun x -> x) (new_Type ()) arity) fieldimpls fields
+ params (Option.default (Termops.new_Type ()) arity) fieldimpls fields
~kind:Method ~name:idarg false (List.map (fun _ -> false) fields) sign
in
- IndRef ind, (List.map2 (fun (id, _, _) y -> (Nameops.out_name id, y))
- (List.rev fields) (Recordops.lookup_projections ind))
+ 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)*)
+ | Some (_, (cl, _)) -> Some (cl.cl_impl, true) (*List.exists (fun (_, n) -> n = na) supnames)*)
| None -> None)
params, params
in
@@ -354,9 +365,9 @@ let declare_class finite def infer id idbuild paramimpls params arity fieldimpls
cl_props = fields;
cl_projs = projs }
in
- List.iter2 (fun p sub ->
- if sub then match snd p with Some p -> declare_instance_cst true p | None -> ())
- k.cl_projs coers;
+(* 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 =
@@ -369,10 +380,12 @@ let interp_and_check_sort sort =
open Vernacexpr
open Autoinstance
-(* [fs] corresponds to fields and [ps] to parameters; [coers] is a boolean
- list telling if the corresponding fields must me declared as coercion *)
+(* [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
@@ -380,6 +393,8 @@ let definition_structure (kind,finite,infer,(is_coe,(loc,idstruc)),ps,cfs,idbuil
| _ -> 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 =
@@ -389,13 +404,14 @@ let definition_structure (kind,finite,infer,(is_coe,(loc,idstruc)),ps,cfs,idbuil
match kind with
| Class def ->
let gr = declare_class finite def infer (loc,idstruc) idbuild
- implpars params sc implfs fields is_coe coers sign in
+ 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 (new_Type ()) sc in
+ 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 coers sign 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