From 32c83676c96ae4a218de0bec75d2f3353381dfb3 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Thu, 28 Aug 2014 19:49:16 +0200 Subject: Change the way primitive projections are declared to the kernel. Now kernel/indtypes builds the corresponding terms (has to be trusted) while translate_constant just binds a constant name to the already entered projection body, avoiding the dubious "check" of user given terms. "case" Pattern-matching on primitive records is now disallowed, and the default scheme is implemented using projections and eta (all elimination tactics now use projections as well). Elaborate "let (x, y) := p in t" using let bindings for the projections of p too. --- toplevel/command.ml | 4 +++- toplevel/ind_tables.ml | 2 +- toplevel/indschemes.ml | 2 +- toplevel/obligations.ml | 2 +- toplevel/record.ml | 28 ++++++++++++++++++---------- 5 files changed, 24 insertions(+), 14 deletions(-) (limited to 'toplevel') diff --git a/toplevel/command.ml b/toplevel/command.ml index a675fe028c..b10a4da06d 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -578,7 +578,9 @@ let declare_mutual_inductive_with_eliminations isrecord mie impls = constrimpls) impls; if_verbose msg_info (minductive_message names); - if mie.mind_entry_private == None then declare_default_schemes mind; + if mie.mind_entry_private == None + && not (mie.mind_entry_record = Some true) + then declare_default_schemes mind; mind type one_inductive_impls = diff --git a/toplevel/ind_tables.ml b/toplevel/ind_tables.ml index 6f3f5cc49b..1f09d76205 100644 --- a/toplevel/ind_tables.ml +++ b/toplevel/ind_tables.ml @@ -126,7 +126,7 @@ let define internal id c p univs = const_entry_body = Future.from_val ((c,Univ.ContextSet.empty), Declareops.no_seff); const_entry_secctx = None; const_entry_type = None; - const_entry_proj = false; + const_entry_proj = None; const_entry_polymorphic = p; const_entry_universes = Evd.evar_context_universe_context ctx; const_entry_opaque = false; diff --git a/toplevel/indschemes.ml b/toplevel/indschemes.ml index d7d6b4c6d1..d413564a9b 100644 --- a/toplevel/indschemes.ml +++ b/toplevel/indschemes.ml @@ -120,7 +120,7 @@ let define id internal ctx c t = { const_entry_body = c; const_entry_secctx = None; const_entry_type = t; - const_entry_proj = false; + const_entry_proj = None; const_entry_polymorphic = true; const_entry_universes = Evd.universe_context ctx; const_entry_opaque = false; diff --git a/toplevel/obligations.ml b/toplevel/obligations.ml index 47aa2688d1..18e85266ee 100644 --- a/toplevel/obligations.ml +++ b/toplevel/obligations.ml @@ -629,7 +629,7 @@ let declare_obligation prg obl body ty uctx = { const_entry_body = Future.from_val((body,Univ.ContextSet.empty),Declareops.no_seff); const_entry_secctx = None; const_entry_type = if List.is_empty ctx then ty else None; - const_entry_proj = false; + const_entry_proj = None; const_entry_polymorphic = poly; const_entry_universes = uctx; const_entry_opaque = opaque; diff --git a/toplevel/record.ml b/toplevel/record.ml index 302fe6280e..2fbe7483f2 100644 --- a/toplevel/record.ml +++ b/toplevel/record.ml @@ -219,13 +219,13 @@ let declare_projections indsp ?(kind=StructureComponent) ?name coers fieldimpls let x = match name with Some n -> Name n | None -> Namegen.named_hd (Global.env()) r Anonymous in let fields = instantiate_possibly_recursive_type indu paramdecls fields in let lifted_fields = Termops.lift_rel_context 1 fields in - let (_,kinds,sp_projs,_) = + let (_,_,kinds,sp_projs,_) = List.fold_left3 - (fun (nfi,kinds,sp_projs,subst) coe (fi,optci,ti) impls -> - let (sp_projs,subst) = + (fun (nfi,i,kinds,sp_projs,subst) coe (fi,optci,ti) impls -> + let (sp_projs,i,subst) = match fi with | Anonymous -> - (None::sp_projs,NoProjection fi::subst) + (None::sp_projs,i,NoProjection fi::subst) | Name fid -> try let ccl = subst_projection fid subst ti in @@ -247,8 +247,9 @@ let declare_projections indsp ?(kind=StructureComponent) ?name coers fieldimpls let kn = try let makeprim = - if !primitive_flag && optci = None then true - else false + if !primitive_flag && optci = None then + Some (fst indsp, i) + else None in let cie = { const_entry_body = @@ -280,12 +281,12 @@ let declare_projections indsp ?(kind=StructureComponent) ?name coers fieldimpls let proj_args = (*Rel 1 refers to "x"*) paramargs@[mkRel 1] in applist (mkConstU (kn,u),proj_args) in - (Some kn::sp_projs, Projection constr_fip::subst) + (Some kn::sp_projs, i+1, Projection constr_fip::subst) with NotDefinable why -> warning_or_error coe indsp why; - (None::sp_projs,NoProjection fi::subst) in - (nfi-1,(fi, Option.is_empty optci)::kinds,sp_projs,subst)) - (List.length fields,[],[],[]) coers (List.rev fields) (List.rev fieldimpls) + (None::sp_projs,i,NoProjection fi::subst) in + (nfi-1,i,(fi, Option.is_empty optci)::kinds,sp_projs,subst)) + (List.length fields,0,[],[],[]) coers (List.rev fields) (List.rev fieldimpls) in (kinds,sp_projs) let structure_signature ctx = @@ -341,6 +342,13 @@ let declare_structure finite infer poly ctx id idbuild paramimpls params arity f let cstr = (rsp,1) in let kinds,sp_projs = declare_projections rsp ~kind ?name coers fieldimpls fields in let build = ConstructRef cstr in + let () = + if !primitive_flag then + (* declare_mutual won't have tried to define the eliminations, we do it now that + the projections have been defined. *) + Indschemes.declare_default_schemes kn + else () + 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 -- cgit v1.2.3