diff options
55 files changed, 317 insertions, 218 deletions
diff --git a/dev/top_printers.ml b/dev/top_printers.ml index 6bf294967..2cbac2175 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -239,7 +239,7 @@ let constr_display csr = | Construct (((sp,i),j),u) -> "MutConstruct(("^(string_of_mind sp)^","^(string_of_int i)^")," ^","^(universes_display u)^(string_of_int j)^")" - | Proj (p, c) -> "Proj("^(string_of_con p)^","^term_display c ^")" + | Proj (p, c) -> "Proj("^(string_of_con (Projection.constant p))^","^term_display c ^")" | Case (ci,p,c,bl) -> "MutCase(<abs>,"^(term_display p)^","^(term_display c)^"," ^(array_display bl)^")" @@ -328,7 +328,7 @@ let print_pure_constr csr = print_string ","; universes_display u; print_string ")" | Proj (p,c') -> print_string "Proj("; - sp_con_display p; + sp_con_display (Projection.constant p); print_string ","; box_display c'; print_string ")" diff --git a/interp/constrextern.ml b/interp/constrextern.ml index 885b0e6b4..63461c11a 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -983,7 +983,8 @@ let rec glob_of_pat env sigma = function GVar (loc,id) | PMeta None -> GHole (loc,Evar_kinds.InternalHole, None) | PMeta (Some n) -> GPatVar (loc,(false,n)) - | PProj (p,c) -> GApp (loc,GRef (loc, ConstRef p,None),[glob_of_pat env sigma c]) + | PProj (p,c) -> GApp (loc,GRef (loc, ConstRef (Projection.constant p),None), + [glob_of_pat env sigma c]) | PApp (f,args) -> GApp (loc,glob_of_pat env sigma f,Array.map_to_list (glob_of_pat env sigma) args) | PSoApp (n,args) -> diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 56780e240..6b3de2621 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -684,14 +684,6 @@ let intern_var genv (ltacvars,ntnvars) namedctx loc id = (* [id] a goal variable *) GVar (loc,id), [], [], [] -let is_projection_ref = function - | ConstRef r -> - if Environ.is_projection r (Global.env ()) then - let pb = Environ.lookup_projection r (Global.env ()) in - Some (r, pb.Declarations.proj_npars) - else None - | _ -> None - let proj_impls r impls = let env = Global.env () in let f (x, l) = x, projection_implicits env r l in @@ -710,17 +702,15 @@ let find_appl_head_data c = | GRef (loc,ref,_) as x -> let impls = implicits_of_global ref in let scopes = find_arguments_scope ref in - let isproj = is_projection_ref ref in - x, isproj, impls, scopes, [] + x, impls, scopes, [] | GApp (_,GRef (_,ref,_),l) as x when l != [] && Flags.version_strictly_greater Flags.V8_2 -> let n = List.length l in let impls = implicits_of_global ref in let scopes = find_arguments_scope ref in - let isproj = is_projection_ref ref in - x, isproj, List.map (drop_first_implicits n) impls, + x, List.map (drop_first_implicits n) impls, List.skipn_at_least n scopes,[] - | x -> x,None,[],[],[] + | x -> x,[],[],[] let error_not_enough_arguments loc = user_err_loc (loc,"",str "Abbreviation is not applied enough.") @@ -777,26 +767,24 @@ let intern_applied_reference intern env namedctx lvar us args = function try intern_qualid loc qid intern env lvar us args with Not_found -> error_global_not_found_loc loc qid in - let x, isproj, imp, scopes, l = find_appl_head_data r in - let isproj = if projapp then isproj else None in - (x,imp,scopes,l), isproj, args2 + let x, imp, scopes, l = find_appl_head_data r in + (x,imp,scopes,l), args2 | Ident (loc, id) -> - try intern_var env lvar namedctx loc id, None, args + try intern_var env lvar namedctx loc id, args with Not_found -> let qid = qualid_of_ident id in try let r, projapp, args2 = intern_non_secvar_qualid loc qid intern env lvar us args in - let x, isproj, imp, scopes, l = find_appl_head_data r in - let isproj = if projapp then isproj else None in - (x,imp,scopes,l), isproj, args2 + let x, imp, scopes, l = find_appl_head_data r in + (x,imp,scopes,l), args2 with Not_found -> (* Extra allowance for non globalizing functions *) if !interning_grammar || env.unb then - (GVar (loc,id), [], [], []), None, args + (GVar (loc,id), [], [], []), args else error_global_not_found_loc loc qid let interp_reference vars r = - let (r,_,_,_),_,_ = + let (r,_,_,_),_ = intern_applied_reference (fun _ -> error_not_enough_arguments Loc.ghost) {ids = Id.Set.empty; unb = false ; tmp_scope = None; scopes = []; impls = empty_internalization_env} [] @@ -1358,11 +1346,11 @@ let extract_explicit_arg imps args = let internalize globalenv env allow_patvar lvar c = let rec intern env = function | CRef (ref,us) as x -> - let (c,imp,subscopes,l),isproj,_ = + let (c,imp,subscopes,l),_ = intern_applied_reference intern env (Environ.named_context globalenv) lvar us [] ref in - apply_impargs (None, isproj) c env imp subscopes l (constr_loc x) + apply_impargs c env imp subscopes l (constr_loc x) | CFix (loc, (locid,iddef), dl) -> let lf = List.map (fun ((_, id),_,_,_,_) -> id) dl in @@ -1457,7 +1445,7 @@ let internalize globalenv env allow_patvar lvar c = intern {env with tmp_scope = None; scopes = find_delimiters_scope loc key :: env.scopes} e | CAppExpl (loc, (isproj,ref,us), args) -> - let (f,_,args_scopes,_),isprojf,args = + let (f,_,args_scopes,_),args = let args = List.map (fun a -> (a,None)) args in intern_applied_reference intern env (Environ.named_context globalenv) lvar us args ref @@ -1466,23 +1454,23 @@ let internalize globalenv env allow_patvar lvar c = GApp (loc, f, intern_args env args_scopes (List.map fst args)) | CApp (loc, (isproj,f), args) -> - let isproj,f,args = match f with + let f,args = match f with (* Compact notations like "t.(f args') args" *) - | CApp (_,(Some _ as isproj',f), args') when not (Option.has_some isproj) -> - isproj',f,args'@args + | CApp (_,(Some _,f), args') when not (Option.has_some isproj) -> + f,args'@args (* Don't compact "(f args') args" to resolve implicits separately *) - | _ -> isproj,f,args in - let (c,impargs,args_scopes,l),isprojf,args = + | _ -> f,args in + let (c,impargs,args_scopes,l),args = match f with | CRef (ref,us) -> intern_applied_reference intern env (Environ.named_context globalenv) lvar us args ref | CNotation (loc,ntn,([],[],[])) -> let c = intern_notation intern env lvar loc ntn ([],[],[]) in - let x, isproj, impl, scopes, l = find_appl_head_data c in - (x,impl,scopes,l), None, args - | x -> (intern env f,[],[],[]), None, args in - apply_impargs (isproj,isprojf) c env impargs args_scopes + let x, impl, scopes, l = find_appl_head_data c in + (x,impl,scopes,l), args + | x -> (intern env f,[],[],[]), args in + apply_impargs c env impargs args_scopes (merge_impargs l args) loc | CRecord (loc, _, fs) -> @@ -1719,7 +1707,7 @@ let internalize globalenv env allow_patvar lvar c = intern_args env subscopes rargs in aux 1 l subscopes eargs rargs - and apply_impargs (isproj,isprojf) c env imp subscopes l loc = + and apply_impargs c env imp subscopes l loc = let imp = select_impargs_size (List.length l) imp in let l = intern_impargs c env imp subscopes l in smart_gapp c loc l diff --git a/interp/notation.ml b/interp/notation.ml index 6cc99ddb4..e765701d4 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -535,7 +535,7 @@ let compute_scope_class t = let t', _ = decompose_appvect (Reductionops.whd_betaiotazeta Evd.empty t) in match kind_of_term t' with | Var _ | Const _ | Ind _ -> ScopeRef (global_of_constr t') - | Proj (p, c) -> ScopeRef (ConstRef p) + | Proj (p, c) -> ScopeRef (ConstRef (Projection.constant p)) | Sort _ -> ScopeSort | _ -> raise Not_found diff --git a/kernel/cbytegen.ml b/kernel/cbytegen.ml index 36a022fd9..6fd1c689f 100644 --- a/kernel/cbytegen.ml +++ b/kernel/cbytegen.ml @@ -501,11 +501,12 @@ let rec compile_constr reloc c sz cont = | Evar _ -> invalid_arg "Cbytegen.compile_constr : Evar" | Proj (p,c) -> (* compile_const reloc p [|c|] sz cont *) - let cb = lookup_constant p !global_env in + let kn = Projection.constant p in + let cb = lookup_constant kn !global_env in (* TODO: better representation of projections *) let pb = Option.get cb.const_proj in let args = Array.make pb.proj_npars mkProp in - compile_const reloc p Univ.Instance.empty (Array.append args [|c|]) sz cont + compile_const reloc kn Univ.Instance.empty (Array.append args [|c|]) sz cont | Cast(c,_,_) -> compile_constr reloc c sz cont diff --git a/kernel/closure.ml b/kernel/closure.ml index 14afcc4db..23861347a 100644 --- a/kernel/closure.ml +++ b/kernel/closure.ml @@ -88,6 +88,7 @@ module type RedFlagsSig = sig val red_add_transparent : reds -> transparent_state -> reds val mkflags : red_kind list -> reds val red_set : reds -> red_kind -> bool + val red_projection : reds -> projection -> bool end module RedFlags = (struct @@ -168,6 +169,10 @@ module RedFlags = (struct | DELTA -> (* Used for Rel/Var defined in context *) incr_cnt red.r_delta delta + let red_projection red p = + if Projection.unfolded p then true + else red_set red (fCONST (Projection.constant p)) + end : RedFlagsSig) open RedFlags @@ -338,7 +343,7 @@ and fterm = | FInd of pinductive | FConstruct of pconstructor | FApp of fconstr * fconstr array - | FProj of constant * fconstr + | FProj of projection * fconstr | FFix of fixpoint * fconstr subs | FCoFix of cofixpoint * fconstr subs | FCases of case_info * fconstr * fconstr * fconstr array @@ -708,7 +713,7 @@ let rec zip m stk rem = match stk with let t = FCases(ci, p, m, br) in zip {norm=neutr m.norm; term=t} s rem | Zproj (i,j,cst) :: s -> - zip {norm=neutr m.norm; term=FProj (cst,m)} s rem + zip {norm=neutr m.norm; term=FProj (Projection.make cst true,m)} s rem | Zfix(fx,par)::s -> zip fx par ((Zapp [|m|] :: s) :: rem) | Zshift(n)::s -> @@ -876,7 +881,7 @@ let eta_expand_ind_stack env ind m s (f, s') = (** Try to drop the params, might fail on partially applied constructors. *) let argss = try_drop_parameters depth pars args in let hstack = Array.map (fun p -> { norm = Red; (* right can't be a constructor though *) - term = FProj (p, right) }) projs in + term = FProj (Projection.make p true, right) }) projs in argss, [Zapp hstack] | _ -> raise Not_found (* disallow eta-exp for non-primitive records *) @@ -932,11 +937,13 @@ let rec knh info m stk = | (None, stk') -> (m,stk')) | FCast(t,_,_) -> knh info t stk | FProj (p,c) -> - if red_set info.i_flags (fCONST p) then + let unf = Projection.unfolded p in + if unf || red_set info.i_flags (fCONST (Projection.constant p)) then (match try Some (lookup_projection p (info_env info)) with Not_found -> None with | None -> (m, stk) | Some pb -> - knh info c (Zproj (pb.Declarations.proj_npars, pb.Declarations.proj_arg, p) + knh info c (Zproj (pb.Declarations.proj_npars, pb.Declarations.proj_arg, + Projection.constant p) :: zupdate m stk)) else (m,stk) @@ -1033,7 +1040,7 @@ let rec zip_term zfun m stk = let t = mkCase(ci, zfun p, m, Array.map zfun br) in zip_term zfun t s | Zproj(_,_,p)::s -> - let t = mkProj (p, m) in + let t = mkProj (Projection.make p true, m) in zip_term zfun t s | Zfix(fx,par)::s -> let h = mkApp(zip_term zfun (zfun fx) par,[|m|]) in diff --git a/kernel/closure.mli b/kernel/closure.mli index 1062d0e61..445fcb7bc 100644 --- a/kernel/closure.mli +++ b/kernel/closure.mli @@ -64,7 +64,10 @@ module type RedFlagsSig = sig (** Tests if a reduction kind is set *) val red_set : reds -> red_kind -> bool - + + (** This tests if the projection is in unfolded state already or + is unfodable due to delta. *) + val red_projection : reds -> projection -> bool end module RedFlags : RedFlagsSig @@ -113,7 +116,7 @@ type fterm = | FInd of inductive puniverses | FConstruct of constructor puniverses | FApp of fconstr * fconstr array - | FProj of constant * fconstr + | FProj of projection * fconstr | FFix of fixpoint * fconstr subs | FCoFix of cofixpoint * fconstr subs | FCases of case_info * fconstr * fconstr * fconstr array diff --git a/kernel/constr.ml b/kernel/constr.ml index 2a13f938b..912067629 100644 --- a/kernel/constr.ml +++ b/kernel/constr.ml @@ -85,7 +85,7 @@ type ('constr, 'types) kind_of_term = | Case of case_info * 'constr * 'constr * 'constr array | Fix of ('constr, 'types) pfixpoint | CoFix of ('constr, 'types) pcofixpoint - | Proj of constant * 'constr + | Proj of projection * 'constr (* constr is the fixpoint of the previous type. Requires option -rectypes of the Caml compiler to be set *) type t = (t,t) kind_of_term @@ -486,7 +486,7 @@ let compare_head_gen eq_universes eq_sorts f t1 t2 = Int.equal (Array.length l1) (Array.length l2) && f c1 c2 && Array.equal f l1 l2 | Evar (e1,l1), Evar (e2,l2) -> Evar.equal e1 e2 && Array.equal f l1 l2 - | Proj (p1,c1), Proj (p2,c2) -> eq_constant p1 p2 && f c1 c2 + | Proj (p1,c1), Proj (p2,c2) -> Projection.equal p1 p2 && f c1 c2 | Const (c1,u1), Const (c2,u2) -> eq_constant c1 c2 && eq_universes true u1 u2 | Ind (c1,u1), Ind (c2,u2) -> eq_ind c1 c2 && eq_universes false u1 u2 | Construct (c1,u1), Construct (c2,u2) -> eq_constructor c1 c2 && eq_universes false u1 u2 @@ -523,7 +523,7 @@ let compare_head_gen_leq eq_universes eq_sorts leq_sorts eq leq t1 t2 = | App (c1,l1), App (c2,l2) -> Int.equal (Array.length l1) (Array.length l2) && eq c1 c2 && Array.equal eq l1 l2 - | Proj (p1,c1), Proj (p2,c2) -> eq_constant p1 p2 && eq c1 c2 + | Proj (p1,c1), Proj (p2,c2) -> Projection.equal p1 p2 && eq c1 c2 | Evar (e1,l1), Evar (e2,l2) -> Evar.equal e1 e2 && Array.equal eq l1 l2 | Const (c1,u1), Const (c2,u2) -> eq_constant c1 c2 && eq_universes true u1 u2 | Ind (c1,u1), Ind (c2,u2) -> eq_ind c1 c2 && eq_universes false u1 u2 @@ -657,7 +657,7 @@ let constr_ord_int f t1 t2 = | App (Cast(c1,_,_),l1), _ -> f (mkApp (c1,l1)) t2 | _, App (Cast(c2, _,_),l2) -> f t1 (mkApp (c2,l2)) | App (c1,l1), App (c2,l2) -> (f =? (Array.compare f)) c1 c2 l1 l2 - | Proj (p1,c1), Proj (p2,c2) -> (con_ord =? f) p1 p2 c1 c2 + | Proj (p1,c1), Proj (p2,c2) -> (Projection.compare =? f) p1 p2 c1 c2 | Evar (e1,l1), Evar (e2,l2) -> (Evar.compare =? (Array.compare f)) e1 e2 l1 l2 | Const (c1,u1), Const (c2,u2) -> con_ord c1 c2 @@ -820,8 +820,8 @@ let hashcons (sh_sort,sh_ci,sh_construct,sh_ind,sh_con,sh_na,sh_id) = (Evar (e,l), combinesmall 8 (combine (Evar.hash e) hl)) | Proj (p,c) -> let c, hc = sh_rec c in - let p' = sh_con p in - (Proj (p', c), combinesmall 17 (combine (Constant.hash p') hc)) + let p' = Projection.hashcons p in + (Proj (p', c), combinesmall 17 (combine (Projection.hash p') hc)) | Const (c,u) -> let c' = sh_con c in let u', hu = sh_instance u in @@ -906,7 +906,7 @@ let rec hash t = | App (c,l) -> combinesmall 7 (combine (hash_term_array l) (hash c)) | Proj (p,c) -> - combinesmall 17 (combine (Constant.hash p) (hash c)) + combinesmall 17 (combine (Projection.hash p) (hash c)) | Evar (e,l) -> combinesmall 8 (combine (Evar.hash e) (hash_term_array l)) | Const (c,u) -> diff --git a/kernel/constr.mli b/kernel/constr.mli index 58f248b03..da7ac6a0d 100644 --- a/kernel/constr.mli +++ b/kernel/constr.mli @@ -103,7 +103,7 @@ val mkConst : constant -> constr val mkConstU : pconstant -> constr (** Constructs a projection application *) -val mkProj : (constant * constr) -> constr +val mkProj : (projection * constr) -> constr (** Inductive types *) @@ -190,7 +190,7 @@ type ('constr, 'types) kind_of_term = | Case of case_info * 'constr * 'constr * 'constr array | Fix of ('constr, 'types) pfixpoint | CoFix of ('constr, 'types) pcofixpoint - | Proj of constant * 'constr + | Proj of projection * 'constr (** User view of [constr]. For [App], it is ensured there is at least one argument and the function is not itself an applicative diff --git a/kernel/cooking.ml b/kernel/cooking.ml index 2d316fc1d..5f6aebc4e 100644 --- a/kernel/cooking.ml +++ b/kernel/cooking.ml @@ -123,12 +123,13 @@ let expmod_constr cache modlist c = | Proj (p, c') -> (try - let p' = share_univs (ConstRef p) Univ.Instance.empty modlist in + let p' = share_univs (ConstRef (Projection.constant p)) Univ.Instance.empty modlist in + let make c = Projection.make c (Projection.unfolded p) in match kind_of_term p' with - | Const (p',_) -> mkProj (p', substrec c') + | Const (p',_) -> mkProj (make p', substrec c') | App (f, args) -> (match kind_of_term f with - | Const (p', _) -> mkProj (p', substrec c') + | Const (p', _) -> mkProj (make p', substrec c') | _ -> assert false) | _ -> assert false with Not_found -> map_constr substrec c) diff --git a/kernel/environ.ml b/kernel/environ.ml index 6b0b0bdba..b331d8da7 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -328,7 +328,7 @@ let template_polymorphic_pconstant (cst,u) env = else template_polymorphic_constant cst env let lookup_projection cst env = - match (lookup_constant cst env).const_proj with + match (lookup_constant (Projection.constant cst) env).const_proj with | Some pb -> pb | None -> anomaly (Pp.str "lookup_projection: constant is not a projection") diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index 4feec40e8..73a23ef05 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -692,14 +692,15 @@ let compute_projections ((kn, _ as ind), u as indsp) n nparamargs params | Name id -> let kn = Constant.make1 (KerName.make mp dp (Label.of_id id)) in let ty = substl subst (liftn 1 j t) in - let term = mkProj (kn, mkRel 1) in + let term = mkProj (Projection.make kn true, mkRel 1) in + let fterm = mkProj (Projection.make kn false, mkRel 1) in let compat = compat_body ty (j - 1) in let etab = it_mkLambda_or_LetIn (mkLambda (x, rp, term)) params in let etat = it_mkProd_or_LetIn (mkProd (x, rp, ty)) params in let body = { proj_ind = fst ind; proj_npars = nparamargs; proj_arg = i; proj_type = ty; proj_eta = etab, etat; proj_body = compat } in - (i + 1, j + 1, kn :: kns, body :: pbs, term :: subst) + (i + 1, j + 1, kn :: kns, body :: pbs, fterm :: subst) | Anonymous -> raise UndefinableExpansion in let (_, _, kns, pbs, subst) = List.fold_right projections ctx (0, 1, [], [], []) in diff --git a/kernel/mod_subst.ml b/kernel/mod_subst.ml index cfe46152e..b65fdb3ac 100644 --- a/kernel/mod_subst.ml +++ b/kernel/mod_subst.ml @@ -342,13 +342,15 @@ let rec map_kn f f' c = let func = map_kn f f' in match kind_of_term c with | Const kn -> (try snd (f' kn) with No_subst -> c) - | Proj (kn,t) -> - let kn' = try fst (f' (kn,Univ.Instance.empty)) - with No_subst -> kn + | Proj (p,t) -> + let p' = + try + Projection.map (fun kn -> fst (f' (kn,Univ.Instance.empty))) p + with No_subst -> p in let t' = func t in - if kn' == kn && t' == t then c - else mkProj (kn', t') + if p' == p && t' == t then c + else mkProj (p', t') | Ind ((kn,i),u) -> let kn' = f kn in if kn'==kn then c else mkIndU ((kn',i),u) diff --git a/kernel/names.ml b/kernel/names.ml index c76d95937..5d73bd520 100644 --- a/kernel/names.ml +++ b/kernel/names.ml @@ -782,7 +782,33 @@ let kn_ord = KerName.compare (** Compatibility layer for [Constant] *) type constant = Constant.t -type projection = constant + + +module Projection = +struct + type t = constant * bool + + let make c b = (c, b) + + let constant = fst + let unfolded = snd + let unfold (c, b as p) = if b then p else (c, true) + let equal (c, b) (c', b') = Constant.equal c c' && b == b' + let hash (c, b) = (if b then 0 else 1) + Constant.hash c + let hashcons (c, b as x) = + let c' = hcons_con c in + if c' == c then x else (c', b) + + let compare (c, b) (c', b') = + if b == b' then Constant.CanOrd.compare c c' + else if b then 1 else -1 + + let map f (c, b as x) = + let c' = f c in + if c' == c then x else (c', b) +end + +type projection = Projection.t let constant_of_kn = Constant.make1 let constant_of_kn_equiv = Constant.make diff --git a/kernel/names.mli b/kernel/names.mli index 49a838ae5..893cad09d 100644 --- a/kernel/names.mli +++ b/kernel/names.mli @@ -634,7 +634,25 @@ val kn_ord : kernel_name -> kernel_name -> int type constant = Constant.t (** @deprecated Alias type *) -type projection = constant +module Projection : sig + type t + + val make : constant -> bool -> t + + val constant : t -> constant + val unfolded : t -> bool + val unfold : t -> t + + val equal : t -> t -> bool + val hash : t -> int + val hashcons : t -> t + + val compare : t -> t -> int + + val map : (constant -> constant) -> t -> t +end + +type projection = Projection.t val constant_of_kn_equiv : KerName.t -> KerName.t -> constant (** @deprecated Same as [Constant.make] *) diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml index bd659a471..041751ecf 100644 --- a/kernel/nativecode.ml +++ b/kernel/nativecode.ml @@ -1923,7 +1923,8 @@ let rec compile_deps env sigma prefix ~interactive init t = comp_stack, (mind_updates, const_updates) | Construct (((mind,_),_),u) -> compile_mind_deps env prefix ~interactive init mind | Proj (p,c) -> - compile_deps env sigma prefix ~interactive init (mkApp (mkConst p, [|c|])) + let term = mkApp (mkConst (Projection.constant p), [|c|]) in + compile_deps env sigma prefix ~interactive init term | Case (ci, p, c, ac) -> let mind = fst ci.ci_ind in let init = compile_mind_deps env prefix ~interactive init mind in diff --git a/kernel/nativelambda.ml b/kernel/nativelambda.ml index 34ed33f94..ba45c329f 100644 --- a/kernel/nativelambda.ml +++ b/kernel/nativelambda.ml @@ -586,7 +586,8 @@ let rec lambda_of_constr env sigma c = | Construct _ -> lambda_of_app env sigma c empty_args | Proj (p, c) -> - mkLapp (Lproj (get_const_prefix !global_env p, p)) [|lambda_of_constr env sigma c|] + let kn = Projection.constant p in + mkLapp (Lproj (get_const_prefix !global_env kn, kn)) [|lambda_of_constr env sigma c|] | Case(ci,t,a,branches) -> let (mind,i as ind) = ci.ci_ind in diff --git a/kernel/reduction.ml b/kernel/reduction.ml index 802d2b67b..9a7146890 100644 --- a/kernel/reduction.ml +++ b/kernel/reduction.ml @@ -275,12 +275,14 @@ let in_whnf (t,stk) = | FLOCKED -> assert false let unfold_projection infos p c = - if RedFlags.red_set infos.i_flags (RedFlags.fCONST p) then - (match try Some (lookup_projection p (info_env infos)) with Not_found -> None with - | Some pb -> - let s = Zproj (pb.Declarations.proj_npars, pb.Declarations.proj_arg, p) in - Some (c, s) - | None -> None) + let unf = Projection.unfolded p in + if unf || RedFlags.red_set infos.i_flags (RedFlags.fCONST (Projection.constant p)) then + (match try Some (lookup_projection p (info_env infos)) with Not_found -> None with + | Some pb -> + let s = Zproj (pb.Declarations.proj_npars, pb.Declarations.proj_arg, + Projection.constant p) in + Some (c, s) + | None -> None) else None (* Conversion between [lft1]term1 and [lft2]term2 *) @@ -368,7 +370,7 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv = | Some (def2,s2) -> eqappr cv_pb l2r infos appr1 (lft2, whd def2 (s2 :: v2)) cuniv | None -> - if eq_constant p1 p2 && compare_stack_shape v1 v2 then + if Projection.equal p1 p2 && compare_stack_shape v1 v2 then let u1 = ccnv CONV l2r infos el1 el2 c1 c2 cuniv in convert_stacks l2r infos lft1 lft2 v1 v2 u1 else (* Two projections in WHNF: unfold *) diff --git a/kernel/term.ml b/kernel/term.ml index 3b6b69a28..ab678666f 100644 --- a/kernel/term.ml +++ b/kernel/term.ml @@ -89,7 +89,7 @@ type ('constr, 'types) kind_of_term = ('constr, 'types) Constr.kind_of_term = | Case of case_info * 'constr * 'constr * 'constr array | Fix of ('constr, 'types) pfixpoint | CoFix of ('constr, 'types) pcofixpoint - | Proj of constant * 'constr + | Proj of projection * 'constr type values = Constr.values diff --git a/kernel/term.mli b/kernel/term.mli index 5ff5f9ba1..28ebc41e2 100644 --- a/kernel/term.mli +++ b/kernel/term.mli @@ -86,7 +86,7 @@ type ('constr, 'types) kind_of_term = ('constr, 'types) Constr.kind_of_term = | Case of case_info * 'constr * 'constr * 'constr array | Fix of ('constr, 'types) pfixpoint | CoFix of ('constr, 'types) pcofixpoint - | Proj of constant * 'constr + | Proj of projection * 'constr type values = Constr.values @@ -405,7 +405,7 @@ val mkLambda : Name.t * types * constr -> constr val mkLetIn : Name.t * constr * types * constr -> constr val mkApp : constr * constr array -> constr val mkConst : constant -> constr -val mkProj : (constant * constr) -> constr +val mkProj : projection * constr -> constr val mkInd : inductive -> constr val mkConstruct : constructor -> constr val mkConstU : constant puniverses -> constr diff --git a/kernel/typeops.ml b/kernel/typeops.ml index fa7dd105c..5421020d2 100644 --- a/kernel/typeops.ml +++ b/kernel/typeops.ml @@ -184,7 +184,8 @@ let judge_of_constant_knowing_parameters env (kn,u as cst) args = let judge_of_constant env cst = judge_of_constant_knowing_parameters env cst [||] -let type_of_projection env (cst,u) = +let type_of_projection env (p,u) = + let cst = Projection.constant p in let cb = lookup_constant cst env in match cb.const_proj with | Some pb -> diff --git a/kernel/vconv.ml b/kernel/vconv.ml index 976380ede..3f9345ff8 100644 --- a/kernel/vconv.ml +++ b/kernel/vconv.ml @@ -203,7 +203,9 @@ let rec conv_eq env pb t1 t2 cu = else raise NotConvertible | Const c1, Const c2 -> eq_puniverses eq_constant c1 c2 cu | Proj (p1,c1), Proj (p2,c2) -> - if eq_constant p1 p2 then conv_eq env pb c1 c2 cu else raise NotConvertible + if eq_constant (Projection.constant p1) (Projection.constant p2) then + conv_eq env pb c1 c2 cu + else raise NotConvertible | Ind c1, Ind c2 -> eq_puniverses eq_ind c1 c2 cu | Construct c1, Construct c2 -> diff --git a/library/heads.ml b/library/heads.ml index 31908816b..8b28f0500 100644 --- a/library/heads.ml +++ b/library/heads.ml @@ -84,7 +84,7 @@ let kind_of_head env t = | Meta _ | Evar _ -> NotImmediatelyComputableHead | App (c,al) -> aux k (Array.to_list al @ l) c b | Proj (p,c) -> - (try on_subterm k (c :: l) b (constant_head p) + (try on_subterm k (c :: l) b (constant_head (Projection.constant p)) with Not_found -> assert false) | Case (_,_,c,_) -> aux k [] c true diff --git a/library/universes.ml b/library/universes.ml index 7fe4258c2..cc0153311 100644 --- a/library/universes.ml +++ b/library/universes.ml @@ -220,7 +220,7 @@ let compare_head_gen_proj env equ eqs eqc' m n = | Proj (p, c), App (f, args) | App (f, args), Proj (p, c) -> (match kind_of_term f with - | Const (p', u) when eq_constant p p' -> + | Const (p', u) when eq_constant (Projection.constant p) p' -> let pb = Environ.lookup_projection p env in let npars = pb.Declarations.proj_npars in if Array.length args == npars + 1 then @@ -429,7 +429,7 @@ let global_app_of_constr c = | Ind (i, u) -> (IndRef i, u), None | Construct (c, u) -> (ConstructRef c, u), None | Var id -> (VarRef id, Instance.empty), None - | Proj (p, c) -> (ConstRef p, Instance.empty), Some c + | Proj (p, c) -> (ConstRef (Projection.constant p), Instance.empty), Some c | _ -> raise Not_found open Declarations diff --git a/plugins/cc/ccalgo.ml b/plugins/cc/ccalgo.ml index 50b647e44..5a4a435a5 100644 --- a/plugins/cc/ccalgo.ml +++ b/plugins/cc/ccalgo.ml @@ -425,15 +425,15 @@ and applist_proj c l = and applist_projection c l = match kind_of_term c with | Const c when Environ.is_projection (fst c) (Global.env()) -> + let p = Projection.make (fst c) false in (match l with | [] -> (* Expand the projection *) - let kn = fst c in let ty,_ = Typeops.type_of_constant (Global.env ()) c in - let pb = Environ.lookup_projection kn (Global.env()) in + let pb = Environ.lookup_projection p (Global.env()) in let ctx,_ = Term.decompose_prod_n_assum (pb.Declarations.proj_npars + 1) ty in - it_mkLambda_or_LetIn (mkProj(kn,mkRel 1)) ctx + it_mkLambda_or_LetIn (mkProj(p,mkRel 1)) ctx | hd :: tl -> - applistc (mkProj (fst c, hd)) tl) + applistc (mkProj (p, hd)) tl) | _ -> applistc c l let rec canonize_name c = @@ -456,9 +456,10 @@ let rec canonize_name c = mkLetIn (na, func b,func t,func ct) | App (ct,l) -> mkApp (func ct,Array.smartmap func l) - | Proj(kn,c) -> - let canon_const = constant_of_kn (canonical_con kn) in - (mkProj (canon_const, func c)) + | Proj(p,c) -> + let p' = Projection.map (fun kn -> + constant_of_kn (canonical_con kn)) p in + (mkProj (p', func c)) | _ -> c (* rebuild a term from a pattern and a substitution *) diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml index 45d6a9393..364a71d28 100644 --- a/plugins/cc/cctac.ml +++ b/plugins/cc/cctac.ml @@ -78,8 +78,9 @@ let rec decompose_term env sigma t= let canon_const = constant_of_kn (canonical_con c) in (Symb (mkConstU (canon_const,u))) | Proj (p, c) -> - let canon_const = constant_of_kn (canonical_con p) in - (Appli (Symb (mkConst canon_const), decompose_term env sigma c)) + let canon_const kn = constant_of_kn (canonical_con kn) in + let p' = Projection.map canon_const p in + (Appli (Symb (mkConst (Projection.constant p')), decompose_term env sigma c)) | _ ->if closed0 t then (Symb t) else raise Not_found (* decompose equality in members and type *) diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml index bbbc9bce7..aa0232d19 100644 --- a/plugins/extraction/extraction.ml +++ b/plugins/extraction/extraction.ml @@ -617,7 +617,7 @@ let rec extract_term env mle mlt c args = | Construct (cp,u) -> extract_cons_app env mle mlt cp u args | Proj (p, c) -> - extract_cst_app env mle mlt p Univ.Instance.empty (c :: args) + extract_cst_app env mle mlt (Projection.constant p) Univ.Instance.empty (c :: args) | Rel n -> (* As soon as the expected [mlt] for the head is known, *) (* we unify it with an fresh copy of the stored type of [Rel n]. *) diff --git a/plugins/quote/quote.ml b/plugins/quote/quote.ml index 745e190cb..ed7f18001 100644 --- a/plugins/quote/quote.ml +++ b/plugins/quote/quote.ml @@ -211,9 +211,9 @@ let compute_rhs bodyi index_of_f = let i = destRel (Array.last args) in PMeta (Some (coerce_meta_in i)) | App (f,args) -> - PApp (snd (pattern_of_constr Evd.empty f), Array.map aux args) + PApp (snd (pattern_of_constr (Global.env()) Evd.empty f), Array.map aux args) | Cast (c,_,_) -> aux c - | _ -> snd (pattern_of_constr Evd.empty c) + | _ -> snd (pattern_of_constr (Global.env())(*FIXME*) Evd.empty c) in aux bodyi diff --git a/pretyping/cases.ml b/pretyping/cases.ml index 726e64e81..c9c6cecb1 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -1283,7 +1283,8 @@ let mk_case pb (ci,pred,c,brs) = let mib = lookup_mind (fst ci.ci_ind) pb.env in match mib.mind_record with | Some (cs, pbs) when Array.length pbs > 0 -> - Reduction.beta_appvect brs.(0) (Array.map (fun p -> mkProj (p, c)) cs) + Reduction.beta_appvect brs.(0) + (Array.map (fun p -> mkProj (Projection.make p false, c)) cs) | _ -> mkCase (ci,pred,c,brs) (**********************************************************************) diff --git a/pretyping/cbv.ml b/pretyping/cbv.ml index 4c1e3c3af..d491ded72 100644 --- a/pretyping/cbv.ml +++ b/pretyping/cbv.ml @@ -197,7 +197,7 @@ let rec norm_head info env t stack = | Cast (ct,_,_) -> norm_head info env ct stack | Proj (p, c) -> - let pinfo = Option.get ((Environ.lookup_constant p (info_env info)).Declarations.const_proj) in + let pinfo = Environ.lookup_projection p (info_env info) in norm_head info env c (PROJ (p, pinfo, stack)) (* constants, axioms diff --git a/pretyping/classops.ml b/pretyping/classops.ml index f754f9f3f..73534210c 100644 --- a/pretyping/classops.ml +++ b/pretyping/classops.ml @@ -31,7 +31,7 @@ type cl_typ = | CL_SECVAR of variable | CL_CONST of constant | CL_IND of inductive - | CL_PROJ of projection + | CL_PROJ of constant type cl_info_typ = { cl_param : int @@ -196,7 +196,8 @@ let find_class_type sigma t = match kind_of_term t' with | Var id -> CL_SECVAR id, Univ.Instance.empty, args | Const (sp,u) -> CL_CONST sp, u, args - | Proj (p, c) -> CL_PROJ p, Univ.Instance.empty, c :: args + | Proj (p, c) when not (Projection.unfolded p) -> + CL_PROJ (Projection.constant p), Univ.Instance.empty, c :: args | Ind (ind_sp,u) -> CL_IND ind_sp, u, args | Prod (_,_,_) -> CL_FUN, Univ.Instance.empty, [] | Sort _ -> CL_SORT, Univ.Instance.empty, [] @@ -406,7 +407,7 @@ let reference_arity_length ref = let projection_arity_length p = let len = reference_arity_length (ConstRef p) in - let pb = Environ.lookup_projection p (Global.env ()) in + let pb = Environ.lookup_projection (Projection.make p false) (Global.env ()) in len - pb.Declarations.proj_npars let class_params = function diff --git a/pretyping/classops.mli b/pretyping/classops.mli index e39b2bba4..1db7bbd61 100644 --- a/pretyping/classops.mli +++ b/pretyping/classops.mli @@ -19,7 +19,7 @@ type cl_typ = | CL_SECVAR of variable | CL_CONST of constant | CL_IND of inductive - | CL_PROJ of projection + | CL_PROJ of constant (** Equality over [cl_typ] *) val cl_typ_eq : cl_typ -> cl_typ -> bool diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml index 6a48d84ed..0ae873643 100644 --- a/pretyping/coercion.ml +++ b/pretyping/coercion.ml @@ -350,7 +350,7 @@ let apply_coercion env sigma p hj typ_cl = (if isid then { uj_val = ja.uj_val; uj_type = jres.uj_type } else if isproj then - { uj_val = mkProj (fst (destConst fv.uj_val), ja.uj_val); + { uj_val = mkProj (Projection.make (fst (destConst fv.uj_val)) false, ja.uj_val); uj_type = jres.uj_type } else jres), diff --git a/pretyping/constrMatching.ml b/pretyping/constrMatching.ml index 7af639633..b0f1dd920 100644 --- a/pretyping/constrMatching.ml +++ b/pretyping/constrMatching.ml @@ -227,10 +227,10 @@ let matches_core env sigma convert allow_partial_app allow_bound_rels pat c = | PApp (c1,arg1), App (c2,arg2) -> (match c1, kind_of_term c2 with - | PRef (ConstRef r), Proj (pr,c) when not (eq_constant r pr) -> + | PRef (ConstRef r), Proj (pr,c) when not (eq_constant r (Projection.constant pr)) -> raise PatternMatchingFailure | PProj (pr1,c1), Proj (pr,c) -> - if eq_constant pr1 pr then + if eq_constant (Projection.constant pr1) (Projection.constant pr) then try Array.fold_left2 (sorec stk env) (sorec stk env subst c1 c) arg1 arg2 with Invalid_argument _ -> raise PatternMatchingFailure else raise PatternMatchingFailure @@ -241,14 +241,16 @@ let matches_core env sigma convert allow_partial_app allow_bound_rels pat c = try Array.fold_left2 (sorec stk env) (sorec stk env subst c1 c2) arg1 arg2 with Invalid_argument _ -> raise PatternMatchingFailure) - | PApp (PRef (ConstRef c1), _), Proj (pr, c2) when not (eq_constant c1 pr) -> + | PApp (PRef (ConstRef c1), _), Proj (pr, c2) when not (eq_constant c1 + (Projection.constant pr)) -> raise PatternMatchingFailure | PApp (c, args), Proj (pr, c2) -> let term = Retyping.expand_projection env sigma pr c2 [] in sorec stk env subst p term - | PProj (p1,c1), Proj (p2,c2) when eq_constant p1 p2 -> + | PProj (p1,c1), Proj (p2,c2) when + eq_constant (Projection.constant p1) (Projection.constant p2) -> sorec stk env subst c1 c2 | PProd (na1,c1,d1), Prod(na2,c2,d2) -> diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index 07540af57..0b0ff2fb5 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -445,12 +445,22 @@ let rec detype flags avoid env sigma t = | Proj (p,c) -> if fst flags || !Flags.in_debugger || !Flags.in_toplevel then (* lax mode, used by debug printers only *) - GApp (dl, GRef (dl, ConstRef p, None), + GApp (dl, GRef (dl, ConstRef (Projection.constant p), None), [detype flags avoid env sigma c]) - else let ty = Retyping.get_type_of (snd env) sigma c in - let (ind, args) = Inductive.find_rectype (snd env) ty in - GApp (dl, GRef (dl, ConstRef p, None), - List.map (detype flags avoid env sigma) (args @ [c])) + else + if Projection.unfolded p then + (** Print the compatibility match version *) + let pb = Environ.lookup_projection p (snd env) in + let body = pb.Declarations.proj_body in + let ty = Retyping.get_type_of (snd env) sigma c in + let (ind, args) = Inductive.find_rectype (snd env) ty in + let body' = strip_lam_assum body in + detype flags avoid env sigma (substl (c :: List.rev args) body') + else + let ty = Retyping.get_type_of (snd env) sigma c in + let (ind, args) = Inductive.find_rectype (snd env) ty in + GApp (dl, GRef (dl, ConstRef (Projection.constant p), None), + List.map (detype flags avoid env sigma) (args @ [c])) | Evar (evk,cl) -> let id,l = try Evd.evar_ident evk sigma, diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index e27ee84aa..ddaf69676 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -33,18 +33,24 @@ let _ = Goptions.declare_bool_option { Goptions.optwrite = (fun a -> debug_unification:=a); } -let unfold_projection env p c stk = +let unfold_projection env ts p c stk = (match try Some (lookup_projection p env) with Not_found -> None with | Some pb -> + let cst = Projection.constant p in let unfold () = - let s = Stack.Proj (pb.Declarations.proj_npars, pb.Declarations.proj_arg, p) in + let s = Stack.Proj (pb.Declarations.proj_npars, pb.Declarations.proj_arg, + Projection.constant p) in Some (c, s :: stk) in - (match ReductionBehaviour.get (Globnames.ConstRef p) with - | None -> unfold () - | Some (recargs, nargs, flags) -> - if (List.mem `ReductionNeverUnfold flags) then None - else unfold ()) + if Projection.unfolded p then unfold () + else + if is_transparent_constant ts cst then + (match ReductionBehaviour.get (Globnames.ConstRef cst) with + | None -> unfold () + | Some (recargs, nargs, flags) -> + if (List.mem `ReductionNeverUnfold flags) then None + else unfold ()) + else None | None -> None) let eval_flexible_term ts env c stk = @@ -64,10 +70,7 @@ let eval_flexible_term ts env c stk = with Not_found -> None) | LetIn (_,b,_,c) -> Some (subst1 b c, stk) | Lambda _ -> Some (c, stk) - | Proj (p, c) -> - if is_transparent_constant ts p - then unfold_projection env p c stk - else None + | Proj (p, c) -> unfold_projection env ts p c stk | _ -> assert false type flex_kind_of_term = @@ -527,7 +530,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty in ise_try evd [f1; f2] - | Proj (p, c), Proj (p', c') when eq_constant p p' -> + | Proj (p, c), Proj (p', c') when Projection.equal p p' -> let f1 i = ise_and i [(fun i -> evar_conv_x ts env i CONV c c'); @@ -539,7 +542,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty in ise_try evd [f1; f2] - | Proj (p, t), Const (p',_) when eq_constant p p' -> + | Proj (p, t), Const (p',_) when eq_constant (Projection.constant p) p' -> let f1 i = let pb = Environ.lookup_projection p env in (match Stack.strip_n_app pb.Declarations.proj_npars sk2' with @@ -554,7 +557,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty in evar_eqappr_x ts env i pbty out1 out2 in ise_try evd [f1;f2] - | Const (p',_), Proj (p, t) when eq_constant p p' -> + | Const (p',_), Proj (p, t) when eq_constant (Projection.constant p) p' -> let f1 i = let pb = Environ.lookup_projection p env in (match Stack.strip_n_app pb.Declarations.proj_npars sk1' with @@ -801,7 +804,7 @@ and eta_constructor ts env evd sk1 ((ind, i), u) sk2 term2 = let l1' = Stack.tail pars sk1 in let l2' = let term = Stack.zip (term2,sk2) in - List.map (fun p -> mkProj (p, term)) (Array.to_list projs) + List.map (fun p -> mkProj (Projection.make p false, term)) (Array.to_list projs) in exact_ise_stack2 env evd (evar_conv_x (fst ts, false)) l1' (Stack.append_app_list l2' Stack.empty) diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml index 9f460d08f..6e32d70c0 100644 --- a/pretyping/indrec.ml +++ b/pretyping/indrec.ml @@ -104,7 +104,8 @@ let mis_make_case_com dep env sigma (ind, u as pind) (mib,mip as specif) kind = | None -> mkCase (ci, lift ndepar p, mkRel 1, Termops.rel_vect ndepar k) | Some ps -> - let term = mkApp (mkRel 2, Array.map (fun p -> mkProj (p, mkRel 1)) ps) in + let term = mkApp (mkRel 2, + Array.map (fun p -> mkProj (Projection.make p true, mkRel 1)) ps) in if dep then let ty = mkApp (mkRel 3, [| mkRel 1 |]) in mkCast (term, DEFAULTcast, ty) @@ -390,7 +391,7 @@ let mis_make_indrec env sigma listdepkind mib u = let n, subst = List.fold_right (fun (na,b,t) (i, subst) -> if b == None then - let t = mkProj (ps.(i), mkRel 1) in + let t = mkProj (Projection.make ps.(i) true, mkRel 1) in (i + 1, t :: subst) else (i, mkRel 0 :: subst)) ctx (0, []) diff --git a/pretyping/namegen.ml b/pretyping/namegen.ml index 245c7f943..a6c0149a4 100644 --- a/pretyping/namegen.ml +++ b/pretyping/namegen.ml @@ -83,7 +83,7 @@ let head_name c = (* Find the head constant of a constr if any *) match kind_of_term c with | Prod (_,_,c) | Lambda (_,_,c) | LetIn (_,_,_,c) | Cast (c,_,_) | App (c,_) -> hdrec c - | Proj (kn,_) -> Some (Label.to_id (con_label kn)) + | Proj (kn,_) -> Some (Label.to_id (con_label (Projection.constant kn))) | Const _ | Ind _ | Construct _ | Var _ -> Some (basename_of_global (global_of_constr c)) | Fix ((_,i),(lna,_,_)) | CoFix (i,(lna,_,_)) -> @@ -104,7 +104,7 @@ let hdchar env c = match kind_of_term c with | Prod (_,_,c) | Lambda (_,_,c) | LetIn (_,_,_,c) -> hdrec (k+1) c | Cast (c,_,_) | App (c,_) -> hdrec k c - | Proj (kn,_) + | Proj (kn,_) -> lowercase_first_char (Label.to_id (con_label (Projection.constant kn))) | Const (kn,_) -> lowercase_first_char (Label.to_id (con_label kn)) | Ind (x,_) -> lowercase_first_char (basename_of_global (IndRef x)) | Construct (x,_) -> lowercase_first_char (basename_of_global (ConstructRef x)) diff --git a/pretyping/nativenorm.ml b/pretyping/nativenorm.ml index 829fa106c..60db95e25 100644 --- a/pretyping/nativenorm.ml +++ b/pretyping/nativenorm.ml @@ -268,7 +268,7 @@ and nf_atom env atom = | Aevar (ev,_) -> mkEvar ev | Aproj(p,c) -> let c = nf_accu env c in - mkProj(p,c) + mkProj(Projection.make p false,c) | _ -> fst (nf_atom_type env atom) and nf_atom_type env atom = @@ -342,7 +342,7 @@ and nf_atom_type env atom = | Aproj(p,c) -> let c,tc = nf_accu_type env c in let cj = make_judge c tc in - let uj = Typeops.judge_of_projection env p cj in + let uj = Typeops.judge_of_projection env (Projection.make p true) cj in uj.uj_val, uj.uj_type diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml index 01317ba25..9b7726692 100644 --- a/pretyping/patternops.ml +++ b/pretyping/patternops.ml @@ -106,7 +106,7 @@ let rec head_pattern_bound t = | PCase (_,p,c,br) -> head_pattern_bound c | PRef r -> r | PVar id -> VarRef id - | PProj (p,c) -> ConstRef p + | PProj (p,c) -> ConstRef (Projection.constant p) | PEvar _ | PRel _ | PMeta _ | PSoApp _ | PSort _ | PFix _ -> raise BoundPattern (* Perhaps they were arguments, but we don't beta-reduce *) @@ -120,7 +120,7 @@ let head_of_constr_reference c = match kind_of_term c with | Var id -> VarRef id | _ -> anomaly (Pp.str "Not a rigid reference") -let pattern_of_constr sigma t = +let pattern_of_constr env sigma t = let ctx = ref [] in let rec pattern_of_constr t = match kind_of_term t with @@ -150,7 +150,8 @@ let pattern_of_constr sigma t = | Const (sp,u) -> PRef (ConstRef (constant_of_kn(canonical_con sp))) | Ind (sp,u) -> PRef (canonical_gr (IndRef sp)) | Construct (sp,u) -> PRef (canonical_gr (ConstructRef sp)) - | Proj (p, c) -> PProj (constant_of_kn(canonical_con p), pattern_of_constr c) + | Proj (p, c) -> PProj (Projection.map (fun kn -> constant_of_kn(canonical_con kn)) p, + pattern_of_constr c) | Evar (evk,ctxt as ev) -> (match snd (Evd.evar_source evk sigma) with | Evar_kinds.MatchingVar (b,id) -> @@ -203,7 +204,7 @@ let error_instantiate_pattern id l = ++ strbrk " in pattern because the term refers to " ++ pr_enum pr_id l ++ strbrk " which " ++ str is ++ strbrk " not bound in the pattern.") -let instantiate_pattern sigma lvar c = +let instantiate_pattern env sigma lvar c = let rec aux vars = function | PVar id as x -> (try @@ -215,7 +216,7 @@ let instantiate_pattern sigma lvar c = ctx in let c = substl inst c in - snd (pattern_of_constr sigma c) + snd (pattern_of_constr env sigma c) with Not_found (* List.index failed *) -> let vars = List.map_filter (function Name id -> Some id | _ -> None) vars in @@ -240,13 +241,13 @@ let rec subst_pattern subst pat = | PRef ref -> let ref',t = subst_global subst ref in if ref' == ref then pat else - snd (pattern_of_constr Evd.empty t) + snd (pattern_of_constr (Global.env()) Evd.empty t) | PVar _ | PEvar _ | PRel _ -> pat | PProj (p,c) -> - let p',t = subst_global subst (ConstRef p) in - let p' = destConstRef p' in + let p' = Projection.map (fun p -> + destConstRef (fst (subst_global subst (ConstRef p)))) p in let c' = subst_pattern subst c in if p' == p && c' == c then pat else PProj(p',c') diff --git a/pretyping/patternops.mli b/pretyping/patternops.mli index cfe71510a..382357a8d 100644 --- a/pretyping/patternops.mli +++ b/pretyping/patternops.mli @@ -39,7 +39,7 @@ val head_of_constr_reference : Term.constr -> global_reference a pattern; currently, no destructor (Cases, Fix, Cofix) and no existential variable are allowed in [c] *) -val pattern_of_constr : Evd.evar_map -> constr -> named_context * constr_pattern +val pattern_of_constr : Environ.env -> Evd.evar_map -> constr -> named_context * constr_pattern (** [pattern_of_glob_constr l c] translates a term [c] with metavariables into a pattern; variables bound in [l] are replaced by the pattern to which they @@ -48,7 +48,7 @@ val pattern_of_constr : Evd.evar_map -> constr -> named_context * constr_pattern val pattern_of_glob_constr : glob_constr -> patvar list * constr_pattern -val instantiate_pattern : +val instantiate_pattern : Environ.env -> Evd.evar_map -> extended_patvar_map -> constr_pattern -> constr_pattern diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 5c18297c0..8c4dbfd98 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -566,6 +566,7 @@ let rec pretype resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_var let app_f = match kind_of_term fj.uj_val with | Const (p, u) when Environ.is_projection p env -> + let p = Projection.make p false in let pb = Environ.lookup_projection p env in let npars = pb.Declarations.proj_npars in fun n -> @@ -705,7 +706,8 @@ let rec pretype resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_var let rec aux n k names l = match names, l with | na :: names, ((_, None, t) :: l) -> - (na, Some (lift (cs.cs_nargs - n) (mkProj (ps.(cs.cs_nargs - k), cj.uj_val))), t) + let proj = Projection.make ps.(cs.cs_nargs - k) false in + (na, Some (lift (cs.cs_nargs - n) (mkProj (proj, cj.uj_val))), t) :: aux (n+1) (k + 1) names l | na :: names, ((_, c, t) :: l) -> (na, c, t) :: aux (n+1) k names l diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index 4c9fc4dc5..fb66923a6 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -208,7 +208,7 @@ sig type 'a member = | App of 'a app_node | Case of case_info * 'a * 'a array * Cst_stack.t - | Proj of int * int * projection + | Proj of int * int * constant | Fix of fixpoint * 'a t * Cst_stack.t | Cst of 'a cst_member * int * int list * 'a t * Cst_stack.t | Shift of int @@ -262,7 +262,7 @@ struct type 'a member = | App of 'a app_node | Case of Term.case_info * 'a * 'a array * Cst_stack.t - | Proj of int * int * projection + | Proj of int * int * constant | Fix of fixpoint * 'a t * Cst_stack.t | Cst of 'a cst_member * int * int list * 'a t * Cst_stack.t | Shift of int @@ -302,7 +302,7 @@ struct if Univ.Instance.is_empty u then Constant.print c else str"(" ++ Constant.print c ++ str ", " ++ Univ.Instance.pr u ++ str")" | Cst_proj (p, c) -> - pr_c c ++ str".(" ++ Constant.print p ++ str")" + pr_c c ++ str".(" ++ Constant.print (Projection.constant p) ++ str")" let empty = [] let is_empty = CList.is_empty @@ -329,7 +329,7 @@ struct | Cst_const (c1,u1), Cst_const (c2, u2) -> Constant.equal c1 c2 && Univ.Instance.equal u1 u2 | Cst_proj (p1,c1), Cst_proj (p2,c2) -> - Constant.equal p1 p2 && f (c1,lft1) (c2,lft2) + Projection.equal p1 p2 && f (c1,lft1) (c2,lft2) | _, _ -> false in let rec equal_rec sk1 lft1 sk2 lft2 = @@ -347,7 +347,7 @@ struct then equal_rec s1 lft1 s2 lft2 else None | (Proj (n1,m1,p)::s1, Proj(n2,m2,p2)::s2) -> - if Int.equal n1 n2 && Int.equal m1 m2 && Names.Constant.CanOrd.equal p p2 + if Int.equal n1 n2 && Int.equal m1 m2 && Constant.equal p p2 then equal_rec s1 lft1 s2 lft2 else None | Fix (f1,s1,_) :: s1', Fix (f2,s2,_) :: s2' -> @@ -537,7 +537,7 @@ struct | f, (Cst (cst,_,_,params,_)::s) -> zip ~refold (constr_of_cst_member cst (params @ (append_app [|f|] s))) | f, (Shift n::s) -> zip ~refold (lift n f, s) - | f, (Proj (n,m,p)::s) -> zip ~refold (mkProj (p,f),s) + | f, (Proj (n,m,p)::s) -> zip ~refold (mkProj (Projection.make p true,f),s) | _, (Update _::_) -> assert false end @@ -829,13 +829,14 @@ let rec whd_state_gen ?csts tactic_mode flags env sigma = | Some (bef,arg,s') -> whrec Cst_stack.empty (arg,Stack.Cst(Stack.Cst_const const,curr,remains,bef,cst_l)::s') ) - | Proj (p, c) when Closure.RedFlags.red_set flags (Closure.RedFlags.fCONST p) -> + | Proj (p, c) when Closure.RedFlags.red_projection flags p -> (let pb = lookup_projection p env in + let kn = Projection.constant p in let npars = pb.Declarations.proj_npars and arg = pb.Declarations.proj_arg in - match ReductionBehaviour.get (Globnames.ConstRef p) with + match ReductionBehaviour.get (Globnames.ConstRef kn) with | None -> - let stack' = (c, Stack.Proj (npars, arg, p) :: stack) in + let stack' = (c, Stack.Proj (npars, arg, kn) :: stack) in whrec Cst_stack.empty(* cst_l *) stack' | Some (recargs, nargs, flags) -> if (List.mem `ReductionNeverUnfold flags @@ -850,7 +851,7 @@ let rec whd_state_gen ?csts tactic_mode flags env sigma = |[] -> (* if nargs has been specified *) (* CAUTION : the constant is NEVER refold (even when it hides a (co)fix) *) - let stack' = (c, Stack.Proj (npars, arg, p) :: stack) in + let stack' = (c, Stack.Proj (npars, arg, kn) :: stack) in whrec Cst_stack.empty(* cst_l *) stack' | curr::remains -> if curr == 0 then (* Try to reduce the record argument *) @@ -931,7 +932,7 @@ let rec whd_state_gen ?csts tactic_mode flags env sigma = match Stack.strip_n_app 0 stack with | None -> assert false | Some (_,arg,s'') -> - whrec Cst_stack.empty (arg, Stack.Proj (npars,narg,p) :: s'')) + whrec Cst_stack.empty (arg, Stack.Proj (npars,narg,Projection.constant p) :: s'')) | next :: remains' -> match Stack.strip_n_app (next-curr-1) s'' with | None -> fold () | Some (bef,arg,s''') -> @@ -984,9 +985,10 @@ let local_whd_state_gen flags sigma = | _ -> s) | _ -> s) - | Proj (p,c) when Closure.RedFlags.red_set flags (Closure.RedFlags.fCONST p) -> + | Proj (p,c) when Closure.RedFlags.red_projection flags p -> (let pb = lookup_projection p (Global.env ()) in - whrec (c, Stack.Proj (pb.Declarations.proj_npars, pb.Declarations.proj_arg, p) + whrec (c, Stack.Proj (pb.Declarations.proj_npars, pb.Declarations.proj_arg, + Projection.constant p) :: stack)) | Case (ci,p,d,lf) -> diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli index 6672c7fa7..9a9b34751 100644 --- a/pretyping/reductionops.mli +++ b/pretyping/reductionops.mli @@ -57,7 +57,7 @@ module Stack : sig type 'a member = | App of 'a app_node | Case of case_info * 'a * 'a array * Cst_stack.t - | Proj of int * int * projection + | Proj of int * int * constant | Fix of fixpoint * 'a t * Cst_stack.t | Cst of 'a cst_member * int (** current foccussed arg *) * int list (** remaining args *) * 'a t * Cst_stack.t diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml index 3374da327..b16cf75f5 100644 --- a/pretyping/retyping.ml +++ b/pretyping/retyping.ml @@ -245,5 +245,5 @@ let sorts_of_context env evc ctxt = let expand_projection env sigma pr c args = let ty = get_type_of env sigma c in let (i,u), ind_args = Inductive.find_rectype env ty in - mkApp (mkConstU (pr,u), + mkApp (mkConstU (Projection.constant pr,u), Array.of_list (ind_args @ (c :: args))) diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml index 0088563fa..a2584571d 100644 --- a/pretyping/tacred.ml +++ b/pretyping/tacred.ml @@ -585,7 +585,7 @@ let reduce_proj env sigma whfun whfun' c = (match kind_of_term constr with | Construct _ -> let proj_narg = - let pb = Option.get ((lookup_constant proj env).Declarations.const_proj) in + let pb = lookup_projection proj env in pb.Declarations.proj_npars + pb.Declarations.proj_arg in List.nth cargs proj_narg | _ -> raise Redelimination) @@ -738,24 +738,26 @@ and whd_simpl_stack env sigma = | Proj (p, c) -> (try - if is_evaluable env (EvalConstRef p) then - let pb = Option.get ((lookup_constant p env).Declarations.const_proj) in - (match ReductionBehaviour.get (ConstRef p) with - | Some (l, n, f) when List.mem `ReductionNeverUnfold f -> (* simpl never *) s' - | Some (l, n, f) when not (List.is_empty l) -> - let l' = List.map_filter (fun i -> - let idx = (i - (pb.Declarations.proj_npars + 1)) in - if idx < 0 then None else Some idx) l in - let stack = reduce_params env sigma stack l' in - (match reduce_projection env sigma pb - (whd_construct_stack env sigma c) stack - with - | Reduced s' -> redrec (applist s') - | NotReducible -> s') - | _ -> - match reduce_projection env sigma pb (whd_construct_stack env sigma c) stack with - | Reduced s' -> redrec (applist s') - | NotReducible -> s') + let unf = Projection.unfolded p in + if unf || is_evaluable env (EvalConstRef (Projection.constant p)) then + let pb = lookup_projection p env in + (match unf, ReductionBehaviour.get (ConstRef (Projection.constant p)) with + | false, Some (l, n, f) when List.mem `ReductionNeverUnfold f -> + (* simpl never *) s' + | false, Some (l, n, f) when not (List.is_empty l) -> + let l' = List.map_filter (fun i -> + let idx = (i - (pb.Declarations.proj_npars + 1)) in + if idx < 0 then None else Some idx) l in + let stack = reduce_params env sigma stack l' in + (match reduce_projection env sigma pb + (whd_construct_stack env sigma c) stack + with + | Reduced s' -> redrec (applist s') + | NotReducible -> s') + | _ -> + match reduce_projection env sigma pb (whd_construct_stack env sigma c) stack with + | Reduced s' -> redrec (applist s') + | NotReducible -> s') else s' with Redelimination -> s') @@ -826,12 +828,10 @@ let try_red_product env sigma c = | Construct _ -> c | _ -> redrec env c in - (match match_eval_proj env p with - | Some pb -> - (match reduce_projection env sigma pb (whd_betaiotazeta_stack sigma c') [] with - | Reduced s -> simpfun (applist s) - | NotReducible -> raise Redelimination) - | None -> raise Redelimination) + let pb = lookup_projection p env in + (match reduce_projection env sigma pb (whd_betaiotazeta_stack sigma c') [] with + | Reduced s -> simpfun (applist s) + | NotReducible -> raise Redelimination) | _ -> (match match_eval_ref env x with | Some (ref, u) -> @@ -920,7 +920,7 @@ let whd_simpl_orelse_delta_but_fix env sigma c = | CoFix _ | Fix _ -> s' | Proj (p,c) when (match kind_of_term constr with - | Const (c', _) -> eq_constant p c' + | Const (c', _) -> eq_constant (Projection.constant p) c' | _ -> false) -> let pb = Environ.lookup_projection p env in if List.length stack <= pb.Declarations.proj_npars then @@ -947,7 +947,7 @@ let simpl env sigma c = strong whd_simpl env sigma c let matches_head env sigma c t = match kind_of_term t with | App (f,_) -> ConstrMatching.matches env sigma c f - | Proj (p, _) -> ConstrMatching.matches env sigma c (mkConst p) + | Proj (p, _) -> ConstrMatching.matches env sigma c (mkConst (Projection.constant p)) | _ -> raise ConstrMatching.PatternMatchingFailure let is_pattern_meta = function Pattern.PMeta _ -> true | _ -> false diff --git a/pretyping/termops.ml b/pretyping/termops.ml index c1347c9b4..d6926dac3 100644 --- a/pretyping/termops.ml +++ b/pretyping/termops.ml @@ -79,7 +79,7 @@ let rec pr_constr c = match kind_of_term c with | Ind ((sp,i),u) -> str"Ind(" ++ pr_puniverses (pr_mind sp ++ str"," ++ int i) u ++ str")" | Construct (((sp,i),j),u) -> str"Constr(" ++ pr_puniverses (pr_mind sp ++ str"," ++ int i ++ str"," ++ int j) u ++ str")" - | Proj (p,c) -> str"Proj(" ++ pr_con p ++ str"," ++ pr_constr c ++ str")" + | Proj (p,c) -> str"Proj(" ++ pr_con (Projection.constant p) ++ str"," ++ bool (Projection.unfolded p) ++ pr_constr c ++ str")" | Case (ci,p,c,bl) -> v 0 (hv 0 (str"<"++pr_constr p++str">"++ cut() ++ str"Case " ++ pr_constr c ++ str"of") ++ cut() ++ diff --git a/pretyping/unification.ml b/pretyping/unification.ml index 3f7f238c4..050103542 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -370,7 +370,7 @@ let use_metas_pattern_unification flags nb l = type key = | IsKey of Closure.table_key - | IsProj of constant * constr + | IsProj of projection * constr let expand_table_key env = function | ConstKey cst -> constant_opt_value_in env cst @@ -380,7 +380,8 @@ let expand_table_key env = function let unfold_projection env p stk = (match try Some (lookup_projection p env) with Not_found -> None with | Some pb -> - let s = Stack.Proj (pb.Declarations.proj_npars, pb.Declarations.proj_arg, p) in + let s = Stack.Proj (pb.Declarations.proj_npars, pb.Declarations.proj_arg, + Projection.constant p) in s :: stk | None -> assert false) @@ -405,7 +406,8 @@ let key_of env b flags f = | Var id when is_transparent env (VarKey id) && Id.Pred.mem id (fst flags.modulo_delta) -> Some (IsKey (VarKey id)) - | Proj (p, c) when Cpred.mem p (snd flags.modulo_delta) -> + | Proj (p, c) when Projection.unfolded p + || Cpred.mem (Projection.constant p) (snd flags.modulo_delta) -> Some (IsProj (p, c)) | _ -> None @@ -417,7 +419,7 @@ let translate_key = function let translate_key = function | IsKey k -> translate_key k - | IsProj (c, _) -> ConstKey c + | IsProj (c, _) -> ConstKey (Projection.constant c) let oracle_order env cf1 cf2 = match cf1 with @@ -430,8 +432,10 @@ let oracle_order env cf1 cf2 = | None -> Some true | Some k2 -> match k1, k2 with - | IsProj (p, _), IsKey (ConstKey (p',_)) when eq_constant p p' -> Some false - | IsKey (ConstKey (p,_)), IsProj (p', _) when eq_constant p p' -> Some true + | IsProj (p, _), IsKey (ConstKey (p',_)) + when eq_constant (Projection.constant p) p' -> Some false + | IsKey (ConstKey (p,_)), IsProj (p', _) + when eq_constant p (Projection.constant p') -> Some true | _ -> Some (Conv_oracle.oracle_order (Environ.oracle env) false (translate_key k1) (translate_key k2)) @@ -508,7 +512,7 @@ let eta_constructor_app env f l1 term = | Some (projs, _) -> let pars = mib.Declarations.mind_nparams in let l1' = Array.sub l1 pars (Array.length l1 - pars) in - let l2 = Array.map (fun p -> mkProj (p, term)) projs in + let l2 = Array.map (fun p -> mkProj (Projection.make p false, term)) projs in l1', l2 | _ -> assert false) | _ -> assert false @@ -666,11 +670,8 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb | Some l -> solve_pattern_eqn_array curenvnb f2 l cM substn) - | App (f1,l1), App (f2,l2) -> - unify_app curenvnb pb b substn cM f1 l1 cN f2 l2 - | Proj (p1,c1), Proj (p2,c2) -> - if eq_constant p1 p2 then + if eq_constant (Projection.constant p1) (Projection.constant p2) then try let substn = unirec_rec curenvnb CONV true wt substn c1 c2 in try (* Force unification of the types to fill in parameters *) @@ -679,6 +680,7 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb unify_0_with_initial_metas substn true env cv_pb { flags with modulo_conv_on_closed_terms = Some full_transparent_state; modulo_delta = full_transparent_state; + modulo_eta = true; modulo_betaiota = true } ty1 ty2 with RetypeError _ -> substn @@ -687,6 +689,23 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb else unify_not_same_head curenvnb pb b wt substn cM cN + | App (f1, l1), Proj (p', c) when isConst f1 && + eq_constant (fst (destConst f1)) (Projection.constant p') -> + expand curenvnb pb b false substn cM f1 l1 cN cN [||] + + | Proj (p', c), App (f1, l1) when isConst f1 && + eq_constant (fst (destConst f1)) (Projection.constant p') -> + expand curenvnb pb b false substn cM f1 l1 cN cN [||] + + | App (f1,l1), App (f2,l2) -> + (match kind_of_term f1, kind_of_term f2 with + | Const (p, u), Proj (p', c) when eq_constant p (Projection.constant p') -> + expand curenvnb pb b false substn cM f1 l1 cN f2 l2 + | Proj (p', _), Const (p, _) when eq_constant p (Projection.constant p') -> + expand curenvnb pb b false substn cM f1 l1 cN f2 l2 + | _ -> + unify_app curenvnb pb b substn cM f1 l1 cN f2 l2) + | _ -> unify_not_same_head curenvnb pb b wt substn cM cN diff --git a/tactics/auto.ml b/tactics/auto.ml index 6fa4342d3..564e111e0 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -198,7 +198,7 @@ let strip_params env c = (match cb.Declarations.const_proj with | Some pb -> let n = pb.Declarations.proj_npars in - mkApp (mkProj (p, args.(n)), + mkApp (mkProj (Projection.make p false, args.(n)), Array.sub args (n+1) (Array.length args - (n + 1))) | None -> c) | _ -> c) @@ -585,7 +585,7 @@ let make_exact_entry env sigma pri poly ?(name=PathAny) (c, cty, ctx) = match kind_of_term cty with | Prod _ -> failwith "make_exact_entry" | _ -> - let pat = snd (Patternops.pattern_of_constr sigma cty) in + let pat = snd (Patternops.pattern_of_constr env sigma cty) in let hd = try head_pattern_bound pat with BoundPattern -> failwith "make_exact_entry" @@ -604,7 +604,7 @@ let make_apply_entry env sigma (eapply,hnf,verbose) pri poly ?(name=PathAny) (c, let sigma' = Evd.merge_context_set univ_flexible dummy_goal.sigma ctx in let ce = mk_clenv_from { dummy_goal with sigma = sigma' } (c,cty) in let c' = clenv_type (* ~reduce:false *) ce in - let pat = snd (Patternops.pattern_of_constr sigma c') in + let pat = snd (Patternops.pattern_of_constr env sigma c') in let hd = try head_pattern_bound pat with BoundPattern -> failwith "make_apply_entry" in @@ -701,7 +701,7 @@ let make_trivial env sigma poly ?(name=PathAny) r = let ce = mk_clenv_from dummy_goal (c,t) in (Some hd, { pri=1; poly = poly; - pat = Some (snd (Patternops.pattern_of_constr sigma (clenv_type ce))); + pat = Some (snd (Patternops.pattern_of_constr env sigma (clenv_type ce))); name = name; code=Res_pf_THEN_trivial_fail(c,t,ctx) }) diff --git a/tactics/btermdn.ml b/tactics/btermdn.ml index 5fbc6f5b2..ef813744e 100644 --- a/tactics/btermdn.ml +++ b/tactics/btermdn.ml @@ -33,7 +33,7 @@ type 'res lookup_res = 'res Dn.lookup_res = Label of 'res | Nothing | Everything let decomp_pat = let rec decrec acc = function | PApp (f,args) -> decrec (Array.to_list args @ acc) f - | PProj (p, c) -> (PRef (ConstRef p), c :: acc) + | PProj (p, c) -> (PRef (ConstRef (Projection.constant p)), c :: acc) | c -> (c,acc) in decrec [] @@ -41,7 +41,7 @@ let decomp_pat = let decomp = let rec decrec acc c = match kind_of_term c with | App (f,l) -> decrec (Array.fold_right (fun a l -> a::l) l acc) f - | Proj (p, c) -> (mkConst p, c :: acc) + | Proj (p, c) -> (mkConst (Projection.constant p), c :: acc) | Cast (c1,_,_) -> decrec acc c1 | _ -> (c,acc) in diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index e25a862dd..991eac57e 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -584,7 +584,7 @@ let interp_pure_open_constr ist = let interp_typed_pattern ist env sigma (c,_) = let sigma, c = interp_gen WithoutTypeConstraint ist true pure_open_constr_flags env sigma c in - pattern_of_constr sigma c + pattern_of_constr env sigma c (* Interprets a constr expression casted by the current goal *) let pf_interp_casted_constr ist gl c = @@ -986,7 +986,7 @@ let eval_pattern lfun ist env sigma (_,pat as c) = if use_types then snd (interp_typed_pattern ist env sigma c) else - instantiate_pattern sigma lfun pat + instantiate_pattern env sigma lfun pat let read_pattern lfun ist env sigma = function | Subterm (b,ido,c) -> Subterm (b,ido,eval_pattern lfun ist env sigma c) diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 23b649809..69a72db4f 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -124,7 +124,7 @@ let head_constr_bound t = let hd,args = decompose_app ccl in match kind_of_term hd with | Const _ | Ind _ | Construct _ | Var _ -> hd - | Proj (p, _) -> mkConst p + | Proj (p, _) -> mkConst (Projection.constant p) | _ -> raise Bound let head_constr c = @@ -139,7 +139,7 @@ let decompose_app_bound t = | Ind (i,u) -> IndRef i, args | Construct (c,u) -> ConstructRef c, args | Var id -> VarRef id, args - | Proj (p, c) -> ConstRef p, Array.cons c args + | Proj (p, c) -> ConstRef (Projection.constant p), Array.cons c args | _ -> raise Bound (******************************************) @@ -1172,7 +1172,7 @@ let make_projection env sigma params cstr sign elim i n c u = let args = extended_rel_vect 0 sign in let proj = if Environ.is_projection proj env then - mkProj (proj, mkApp (c, args)) + mkProj (Projection.make proj false, mkApp (c, args)) else mkApp (mkConstU (proj,u), Array.append (Array.of_list params) [|mkApp (c, args)|]) diff --git a/tactics/term_dnet.ml b/tactics/term_dnet.ml index f8d7a197b..9826ecdff 100644 --- a/tactics/term_dnet.ml +++ b/tactics/term_dnet.ml @@ -288,7 +288,7 @@ struct Array.fold_left (fun c a -> Term (DApp (c,a))) (pat_of_constr f) (Array.map pat_of_constr ca) | Proj (p,c) -> - Term (DApp (Term (DRef (ConstRef p)), pat_of_constr c)) + Term (DApp (Term (DRef (ConstRef (Projection.constant p))), pat_of_constr c)) and ctx_of_constr ctx c = match kind_of_term c with | Prod (_,t,c) -> ctx_of_constr (Term(DCons((pat_of_constr t,None),ctx))) c diff --git a/test-suite/bugs/opened/3660.v b/test-suite/bugs/opened/3660.v index f962e1f04..ed8964ce1 100644 --- a/test-suite/bugs/opened/3660.v +++ b/test-suite/bugs/opened/3660.v @@ -18,10 +18,10 @@ admit. Defined. Local Open Scope equiv_scope. Axiom equiv_path : forall (A B : Type) (p : A = B), A <~> B. + Goal forall (C D : hSet), IsEquiv (fun x : C = D => (equiv_path C D (ap setT x))). intros. change (IsEquiv (equiv_path C D o @ap _ _ setT C D)). apply @isequiv_compose; [ | admit ]. - solve [ apply isequiv_ap_setT ]. - Undo. - Fail typeclasses eauto. + Set Typeclasses Debug. + typeclasses eauto. diff --git a/toplevel/record.ml b/toplevel/record.ml index 177aa1cd6..7694869a5 100644 --- a/toplevel/record.ml +++ b/toplevel/record.ml @@ -266,7 +266,7 @@ let declare_projections indsp ?(kind=StructureComponent) ?name coers fieldimpls (** Already defined in the kernel silently *) let kn = destConstRef (Nametab.locate (Libnames.qualid_of_ident fid)) in Declare.definition_message fid; - kn, mkProj (kn,mkRel 1) + kn, mkProj (Projection.make kn false,mkRel 1) else let ccl = subst_projection fid subst ti in let body = match optci with |