diff options
author | Stephane Glondu <steph@glondu.net> | 2010-07-21 09:46:51 +0200 |
---|---|---|
committer | Stephane Glondu <steph@glondu.net> | 2010-07-21 09:46:51 +0200 |
commit | 5b7eafd0f00a16d78f99a27f5c7d5a0de77dc7e6 (patch) | |
tree | 631ad791a7685edafeb1fb2e8faeedc8379318ae /toplevel/record.ml | |
parent | da178a880e3ace820b41d38b191d3785b82991f5 (diff) |
Imported Upstream snapshot 8.3~beta0+13298
Diffstat (limited to 'toplevel/record.ml')
-rw-r--r-- | toplevel/record.ml | 176 |
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 |