diff options
74 files changed, 1420 insertions, 674 deletions
@@ -55,7 +55,7 @@ Notations - The syntax "x -> y" is now declared at level 99. In particular, it has now a lower priority than "<->": "A -> B <-> C" is now "A -> (B <-> C)" (possible source of incompatibilities) -- Notations accept term-provinding tactics using the $(...)$ syntax. +- Notations accept term-providing tactics using the $(...)$ syntax. Specification Language @@ -109,6 +109,7 @@ Tactics - Injection now also deduces equality of arguments of sort Prop. Old behavior can be restored by "Unset Injection On Proofs". Also improved the error messages. +- Tactic "subst id" now supports id occurring in dependent local definitions. Program diff --git a/checker/checker.ml b/checker/checker.ml index b9009da82..f3c583b83 100644 --- a/checker/checker.ml +++ b/checker/checker.ml @@ -297,7 +297,8 @@ let rec explain_exn = function str("\nCantApplyBadType at argument " ^ string_of_int n) | CantApplyNonFunctional _ -> str"CantApplyNonFunctional" | IllFormedRecBody _ -> str"IllFormedRecBody" - | IllTypedRecBody _ -> str"IllTypedRecBody")) + | IllTypedRecBody _ -> str"IllTypedRecBody" + | UnsatisfiedConstraints _ -> str"UnsatisfiedConstraints")) | Indtypes.InductiveError e -> hov 0 (str "Error related to inductive types") diff --git a/checker/cic.mli b/checker/cic.mli index d2f785abf..484d64973 100644 --- a/checker/cic.mli +++ b/checker/cic.mli @@ -79,6 +79,10 @@ type 'constr pfixpoint = (int array * int) * 'constr prec_declaration type 'constr pcofixpoint = int * 'constr prec_declaration +type 'a puniverses = 'a Univ.puniverses +type pconstant = constant puniverses +type pinductive = inductive puniverses +type pconstructor = constructor puniverses type constr = | Rel of int @@ -91,12 +95,13 @@ type constr = | Lambda of Name.t * constr * constr | LetIn of Name.t * constr * constr * constr | App of constr * constr array - | Const of constant - | Ind of inductive - | Construct of constructor + | Const of pconstant + | Ind of pinductive + | Construct of pconstructor | Case of case_info * constr * constr * constr array | Fix of constr pfixpoint | CoFix of constr pcofixpoint + | Proj of constant * constr type existential = constr pexistential type rec_declaration = constr prec_declaration @@ -163,7 +168,17 @@ type engagement = ImpredicativeSet (** {6 Representation of constants (Definition/Axiom) } *) -type constant_type = constr + +type template_arity = { + template_param_levels : Univ.universe option list; + template_level : Univ.universe; +} + +type ('a, 'b) declaration_arity = + | RegularArity of 'a + | TemplateArity of 'b + +type constant_type = (constr, rel_context * template_arity) declaration_arity (** Inlining level of parameters at functor applications. This is ignored by the checker. *) @@ -173,11 +188,24 @@ type inline = int option (** A constant can have no body (axiom/parameter), or a transparent body, or an opaque one *) +(** Projections are a particular kind of constant: + always transparent. *) + +type projection_body = { + proj_ind : mutual_inductive; + proj_npars : int; + proj_arg : int; + proj_type : constr; (* Type under params *) + proj_body : constr; (* For compatibility, the match version *) +} + type constant_def = | Undef of inline | Def of constr_substituted | OpaqueDef of lazy_constr +type constant_universes = Univ.universe_context + type constant_body = { const_hyps : section_context; (** New: younger hyp at top *) const_body : constant_def; @@ -185,6 +213,9 @@ type constant_body = { const_body_code : to_patch_substituted; const_constraints : Univ.constraints; const_native_name : native_name ref; + const_polymorphic : bool; (** Is it polymorphic or not *) + const_universes : constant_universes; + const_proj : projection_body option; const_inline_code : bool } (** {6 Representation of mutual inductive types } *) @@ -196,6 +227,13 @@ type recarg = type wf_paths = recarg Rtree.t +type regular_inductive_arity = { + mind_user_arity : constr; + mind_sort : sorts; +} + +type inductive_arity = (regular_inductive_arity, template_arity) declaration_arity + type one_inductive_body = { (** {8 Primitive datas } *) @@ -203,7 +241,7 @@ type one_inductive_body = { mind_arity_ctxt : rel_context; (** Arity context of [Ii] with parameters: [forall params, Ui] *) - mind_arity : constr; (** Arity sort and original user arity if monomorphic *) + mind_arity : inductive_arity; (** Arity sort and original user arity if monomorphic *) mind_consnames : Id.t array; (** Names of the constructors: [cij] *) @@ -245,7 +283,9 @@ type mutual_inductive_body = { mind_packets : one_inductive_body array; (** The component of the mutual inductive block *) - mind_record : bool; (** Whether the inductive type has been declared as a record *) + mind_record : (constr * constant array) option; + (** Whether the inductive type has been declared as a record, + In that case we get its canonical eta-expansion and list of projections. *) mind_finite : bool; (** Whether the type is inductive or coinductive *) @@ -259,7 +299,11 @@ type mutual_inductive_body = { mind_params_ctxt : rel_context; (** The context of parameters (includes let-in declaration) *) - mind_constraints : Univ.constraints; (** Universes constraints enforced by the inductive declaration *) + mind_polymorphic : bool; (** Is it polymorphic or not *) + + mind_universes : Univ.universe_context; (** Local universe variables and constraints *) + + mind_private : bool option; (** allow pattern-matching: Some true ok, Some false blocked *) (** {8 Data for native compilation } *) diff --git a/checker/closure.ml b/checker/closure.ml index 831f50454..5bd636b16 100644 --- a/checker/closure.ml +++ b/checker/closure.ml @@ -160,16 +160,19 @@ let betaiotazeta = mkflags [fBETA;fIOTA;fZETA] * instantiations (cbv or lazy) are. *) -type table_key = - | ConstKey of constant +type 'a tableKey = + | ConstKey of 'a | VarKey of Id.t | RelKey of int +type table_key = constant puniverses tableKey + module KeyHash = struct type t = table_key let equal k1 k2 = match k1, k2 with - | ConstKey c1, ConstKey c2 -> Constant.UserOrd.equal c1 c2 + | ConstKey (c1,u1), ConstKey (c2,u2) -> Constant.UserOrd.equal c1 c2 + && Univ.Instance.equal u1 u2 | VarKey id1, VarKey id2 -> Id.equal id1 id2 | RelKey i1, RelKey i2 -> Int.equal i1 i2 | (ConstKey _ | VarKey _ | RelKey _), _ -> false @@ -177,7 +180,7 @@ struct open Hashset.Combine let hash = function - | ConstKey c -> combinesmall 1 (Constant.UserOrd.hash c) + | ConstKey (c,u) -> combinesmall 1 (Constant.UserOrd.hash c) | VarKey id -> combinesmall 2 (Id.hash id) | RelKey i -> combinesmall 3 (Int.hash i) end @@ -223,10 +226,7 @@ let defined_rels flags env = let mind_equiv_infos info = mind_equiv info.i_env -let eq_table_key k1 k2 = - match k1,k2 with - | ConstKey con1 ,ConstKey con2 -> eq_con_chk con1 con2 - | _,_ -> k1=k2 +let eq_table_key = KeyHash.equal let create mk_cl flgs env = { i_flags = flgs; @@ -273,9 +273,10 @@ and fterm = | FAtom of constr (* Metas and Sorts *) | FCast of fconstr * cast_kind * fconstr | FFlex of table_key - | FInd of inductive - | FConstruct of constructor + | FInd of pinductive + | FConstruct of pconstructor | FApp of fconstr * fconstr array + | FProj of constant * fconstr | FFix of fixpoint * fconstr subs | FCoFix of cofixpoint * fconstr subs | FCases of case_info * fconstr * fconstr * fconstr array @@ -305,6 +306,7 @@ let update v1 (no,t) = type stack_member = | Zapp of fconstr array | Zcase of case_info * fconstr * fconstr array + | Zproj of int * int * constant | Zfix of fconstr * stack | Zshift of int | Zupdate of fconstr @@ -390,6 +392,9 @@ let rec compact_constr (lg, subs as s) c k = let (f',s) = compact_constr s f k in let (v',s) = compact_vect s v k in if f==f' && v==v' then c,s else App(f',v'), s + | Proj (p, t) -> + let (t', s) = compact_constr s t k in + if t' == t then c,s else Proj(p,t'), s | Lambda(n,a,b) -> let (a',s) = compact_constr s a k in let (b',s) = compact_constr s b (k+1) in @@ -459,7 +464,7 @@ let mk_clos e t = | Meta _ | Sort _ -> { norm = Norm; term = FAtom t } | Ind kn -> { norm = Norm; term = FInd kn } | Construct kn -> { norm = Cstr; term = FConstruct kn } - | (CoFix _|Lambda _|Fix _|Prod _|Evar _|App _|Case _|Cast _|LetIn _) -> + | (CoFix _|Lambda _|Fix _|Prod _|Evar _|App _|Case _|Cast _|LetIn _|Proj _) -> {norm = Red; term = FCLOS(t,e)} let mk_clos_vect env v = Array.map (mk_clos env) v @@ -478,6 +483,9 @@ let mk_clos_deep clos_fun env t = | App (f,v) -> { norm = Red; term = FApp (clos_fun env f, Array.map (clos_fun env) v) } + | Proj (p,c) -> + { norm = Red; + term = FProj (p, clos_fun env c) } | Case (ci,p,c,v) -> { norm = Red; term = FCases (ci, clos_fun env p, clos_fun env c, @@ -533,6 +541,8 @@ let rec to_constr constr_fun lfts v = | FApp (f,ve) -> App (constr_fun lfts f, Array.map (constr_fun lfts) ve) + | FProj (p,c) -> + Proj (p,constr_fun lfts c) | FLambda _ -> let (na,ty,bd) = destFLambda mk_clos2 v in Lambda (na, constr_fun lfts ty, @@ -584,6 +594,8 @@ let rec zip m stk = | Zcase(ci,p,br)::s -> let t = FCases(ci, p, m, br) in zip {norm=neutr m.norm; term=t} s + | Zproj (i,j,cst) :: s -> + zip {norm=neutr m.norm; term=FProj (cst,m)} s | Zfix(fx,par)::s -> zip fx (par @ append_stack [|m|] s) | Zshift(n)::s -> @@ -660,7 +672,7 @@ let rec get_args n tys f e stk = (* Eta expansion: add a reference to implicit surrounding lambda at end of stack *) let rec eta_expand_stack = function - | (Zapp _ | Zfix _ | Zcase _ | Zshift _ | Zupdate _ as e) :: s -> + | (Zapp _ | Zfix _ | Zcase _ | Zshift _ | Zupdate _ | Zproj _ as e) :: s -> e :: eta_expand_stack s | [] -> [Zshift 1; Zapp [|{norm=Norm; term= FRel 1}|]] @@ -690,6 +702,65 @@ let rec drop_parameters depth n stk = | [] -> assert (n=0); [] | _ -> assert false (* we know that n < stack_args_size(stk) *) +(** Projections and eta expansion *) + +let rec get_parameters depth n argstk = + match argstk with + Zapp args::s -> + let q = Array.length args in + if n > q then Array.append args (get_parameters depth (n-q) s) + else if Int.equal n q then [||] + else Array.sub args 0 n + | Zshift(k)::s -> + get_parameters (depth-k) n s + | [] -> (* we know that n < stack_args_size(argstk) (if well-typed term) *) + if Int.equal n 0 then [||] + else raise Not_found (* Trying to eta-expand a partial application..., should do + eta expansion first? *) + | _ -> assert false + (* strip_update_shift_app only produces Zapp and Zshift items *) + +let eta_expand_ind_stack env lft (ind,u) m s (lft, h) = + let mib = lookup_mind (fst ind) env in + match mib.mind_record with + | None -> raise Not_found + | Some (exp,_) -> + let pars = mib.mind_nparams in + let h' = fapp_stack h in + let (depth, args, _) = strip_update_shift_app m s in + let paramargs = get_parameters depth pars args in + let subs = subs_cons (Array.append paramargs [|h'|], subs_id 0) in + let fexp = mk_clos subs exp in + (lft, (fexp, [])) + +let eta_expand_ind_stacks env ind m s h = + let mib = lookup_mind (fst ind) env in + match mib.mind_record with + | Some (exp,projs) when Array.length projs > 0 -> + let pars = mib.mind_nparams in + let h' = fapp_stack h in + let (depth, args, _) = strip_update_shift_app m s in + let primitive = Environ.is_projection projs.(0) env in + if primitive then + let s' = drop_parameters depth pars args in + (* Construct, pars1 .. parsm :: arg1...argn :: s ~= (t, []) -> + arg1..argn :: s ~= (proj1 t...projn t) s + *) + let hstack = Array.map (fun p -> { norm = Red; + term = FProj (p, h') }) projs in + s', [Zapp hstack] + else raise Not_found (* disallow eta-exp for non-primitive records *) + | _ -> raise Not_found + +let rec project_nth_arg n argstk = + match argstk with + | Zapp args :: s -> + let q = Array.length args in + if n >= q then project_nth_arg (n - q) s + else (* n < q *) args.(n) + | _ -> assert false + (* After drop_parameters we have a purely applicative stack *) + (* Iota reduction: expansion of a fixpoint. * Given a fixpoint and a substitution, returns the corresponding @@ -721,33 +792,44 @@ let contract_fix_vect fix = atom or a subterm that may produce a redex (abstraction, constructor, cofix, letin, constant), or a neutral term (product, inductive) *) -let rec knh m stk = +let rec knh info m stk = match m.term with - | FLIFT(k,a) -> knh a (zshift k stk) - | FCLOS(t,e) -> knht e t (zupdate m stk) + | FLIFT(k,a) -> knh info a (zshift k stk) + | FCLOS(t,e) -> knht info e t (zupdate m stk) | FLOCKED -> assert false - | FApp(a,b) -> knh a (append_stack b (zupdate m stk)) - | FCases(ci,p,t,br) -> knh t (Zcase(ci,p,br)::zupdate m stk) + | FApp(a,b) -> knh info a (append_stack b (zupdate m stk)) + | FCases(ci,p,t,br) -> knh info t (Zcase(ci,p,br)::zupdate m stk) | FFix(((ri,n),(_,_,_)),_) -> (match get_nth_arg m ri.(n) stk with - (Some(pars,arg),stk') -> knh arg (Zfix(m,pars)::stk') + (Some(pars,arg),stk') -> knh info arg (Zfix(m,pars)::stk') | (None, stk') -> (m,stk')) - | FCast(t,_,_) -> knh t stk + | FCast(t,_,_) -> knh info t stk + + | FProj (p,c) -> + (* if red_set info.i_flags (fCONST p) then *) + (match try Some (lookup_projection p (info.i_env)) with Not_found -> None with + | None -> (m, stk) + | Some pb -> + knh info c (Zproj (pb.proj_npars, pb.proj_arg, p) + :: zupdate m stk)) + (* else (m,stk) *) + (* cases where knh stops *) | (FFlex _|FLetIn _|FConstruct _|FEvar _| FCoFix _|FLambda _|FRel _|FAtom _|FInd _|FProd _) -> (m, stk) (* The same for pure terms *) -and knht e t stk = +and knht info e t stk = match t with | App(a,b) -> - knht e a (append_stack (mk_clos_vect e b) stk) + knht info e a (append_stack (mk_clos_vect e b) stk) | Case(ci,p,t,br) -> - knht e t (Zcase(ci, mk_clos e p, mk_clos_vect e br)::stk) - | Fix _ -> knh (mk_clos2 e t) stk - | Cast(a,_,_) -> knht e a stk - | Rel n -> knh (clos_rel e n) stk + knht info e t (Zcase(ci, mk_clos e p, mk_clos_vect e br)::stk) + | Fix _ -> knh info (mk_clos2 e t) stk + | Cast(a,_,_) -> knht info e a stk + | Rel n -> knh info (clos_rel e n) stk + | Proj (p,c) -> knh info (mk_clos2 e t) stk | (Lambda _|Prod _|Construct _|CoFix _|Ind _| LetIn _|Const _|Var _|Evar _|Meta _|Sort _) -> (mk_clos2 e t, stk) @@ -762,7 +844,7 @@ let rec knr info m stk = (match get_args n tys f e stk with Inl e', s -> knit info e' f s | Inr lam, s -> (lam,s)) - | FFlex(ConstKey kn) when red_set info.i_flags (fCONST kn) -> + | FFlex(ConstKey kn) when red_set info.i_flags (fCONST (fst kn)) -> (match ref_value_cache info (ConstKey kn) with Some v -> kni info v stk | None -> (set_norm m; (m,stk))) @@ -774,7 +856,7 @@ let rec knr info m stk = (match ref_value_cache info (RelKey k) with Some v -> kni info v stk | None -> (set_norm m; (m,stk))) - | FConstruct(ind,c) when red_set info.i_flags fIOTA -> + | FConstruct((ind,c),u) when red_set info.i_flags fIOTA -> (match strip_update_shift_app m stk with (depth, args, Zcase(ci,_,br)::s) -> assert (ci.ci_npar>=0); @@ -785,6 +867,10 @@ let rec knr info m stk = let stk' = par @ append_stack [|rarg|] s in let (fxe,fxbd) = contract_fix_vect fx.term in knit info fxe fxbd stk' + | (depth, args, Zproj (n, m, cst)::s) -> + let rargs = drop_parameters depth n args in + let rarg = project_nth_arg m rargs in + kni info rarg s | (_,args,s) -> (m,args@s)) | FCoFix _ when red_set info.i_flags fIOTA -> (match strip_update_shift_app m stk with @@ -798,10 +884,10 @@ let rec knr info m stk = (* Computes the weak head normal form of a term *) and kni info m stk = - let (hm,s) = knh m stk in + let (hm,s) = knh info m stk in knr info hm s and knit info e t stk = - let (ht,s) = knht e t stk in + let (ht,s) = knht info e t stk in knr info ht s let kh info v stk = fapp_stack(kni info v stk) @@ -823,6 +909,9 @@ let whd_stack infos m stk = (* cache of constants: the body is computed only when needed. *) type clos_infos = fconstr infos +let infos_env x = x.i_env +let infos_flags x = x.i_flags + let create_clos_infos flgs env = create (fun _ -> inject) flgs env diff --git a/checker/closure.mli b/checker/closure.mli index 13bc0c07e..9b152eb6a 100644 --- a/checker/closure.mli +++ b/checker/closure.mli @@ -66,11 +66,13 @@ val betaiotazeta : reds val betadeltaiotanolet : reds (***********************************************************************) -type table_key = - | ConstKey of constant +type 'a tableKey = + | ConstKey of 'a | VarKey of Id.t | RelKey of int +type table_key = constant puniverses tableKey + type 'a infos val ref_value_cache: 'a infos -> table_key -> 'a option val create: ('a infos -> constr -> 'a) -> reds -> env -> 'a infos @@ -90,9 +92,10 @@ type fterm = | FAtom of constr (* Metas and Sorts *) | FCast of fconstr * cast_kind * fconstr | FFlex of table_key - | FInd of inductive - | FConstruct of constructor + | FInd of pinductive + | FConstruct of pconstructor | FApp of fconstr * fconstr array + | FProj of constant * fconstr | FFix of fixpoint * fconstr subs | FCoFix of cofixpoint * fconstr subs | FCases of case_info * fconstr * fconstr * fconstr array @@ -112,6 +115,7 @@ type fterm = type stack_member = | Zapp of fconstr array | Zcase of case_info * fconstr * fconstr array + | Zproj of int * int * constant | Zfix of fconstr * stack | Zshift of int | Zupdate of fconstr @@ -121,6 +125,12 @@ and stack = stack_member list val append_stack : fconstr array -> stack -> stack val eta_expand_stack : stack -> stack +val eta_expand_ind_stack : env -> lift -> pinductive -> fconstr -> stack -> + (lift * (fconstr * stack)) -> lift * (fconstr * stack) + +val eta_expand_ind_stacks : env -> inductive -> fconstr -> stack -> + (fconstr * stack) -> stack * stack + (* To lazy reduce a constr, create a [clos_infos] with [create_clos_infos], inject the term to reduce with [inject]; then use a reduction function *) @@ -135,6 +145,8 @@ val destFLambda : (* Global and local constant cache *) type clos_infos val create_clos_infos : reds -> env -> clos_infos +val infos_env : clos_infos -> env +val infos_flags : clos_infos -> reds (* Reduction function *) diff --git a/checker/declarations.ml b/checker/declarations.ml index 4dd814d57..f500693ce 100644 --- a/checker/declarations.ml +++ b/checker/declarations.ml @@ -186,12 +186,12 @@ let make_con_equiv mpu mpc dir l = if mpu == mpc then constant_of_kn knu else constant_of_kn_equiv knu (make_kn mpc dir l) -let subst_con0 sub con = +let subst_con0 sub con u = let kn1,kn2 = user_con con,canonical_con con in let mp1,dir,l = repr_kn kn1 in let mp2,_,_ = repr_kn kn2 in let rebuild_con mp1 mp2 = make_con_equiv mp1 mp2 dir l in - let dup con = con, Const con in + let dup con = con, Const (con, u) in let side,con',resolve = gen_subst_mp rebuild_con sub mp1 mp2 in match constant_of_delta_with_inline resolve con' with | Some t -> con', t @@ -205,13 +205,21 @@ let subst_con0 sub con = let rec map_kn f f' c = let func = map_kn f f' in match c with - | Const kn -> (try snd (f' kn) with No_subst -> c) - | Ind (kn,i) -> + | Const (kn, u) -> (try snd (f' kn u) with No_subst -> c) + | Proj (kn,t) -> + let kn' = + try fst (f' kn Univ.Instance.empty) + with No_subst -> kn + in + let t' = func t in + if kn' == kn && t' == t then c + else Proj (kn', t') + | Ind ((kn,i),u) -> let kn' = f kn in - if kn'==kn then c else Ind (kn',i) - | Construct ((kn,i),j) -> + if kn'==kn then c else Ind ((kn',i),u) + | Construct (((kn,i),j),u) -> let kn' = f kn in - if kn'==kn then c else Construct ((kn',i),j) + if kn'==kn then c else Construct (((kn',i),j),u) | Case (ci,p,ct,l) -> let ci_ind = let (kn,i) = ci.ci_ind in @@ -491,8 +499,35 @@ let eq_wf_paths = Rtree.equal eq_recarg with In (params) : Un := cn1 : Tn1 | ... | cnpn : Tnpn *) -let subst_arity sub s = subst_mps sub s +let subst_decl_arity f g sub ar = + match ar with + | RegularArity x -> + let x' = f sub x in + if x' == x then ar + else RegularArity x' + | TemplateArity x -> + let x' = g sub x in + if x' == x then ar + else TemplateArity x' + +let map_decl_arity f g = function + | RegularArity a -> RegularArity (f a) + | TemplateArity a -> TemplateArity (g a) + + +let subst_rel_declaration sub (id,copt,t as x) = + let copt' = Option.smartmap (subst_mps sub) copt in + let t' = subst_mps sub t in + if copt == copt' && t == t' then x else (id,copt',t') + +let subst_rel_context sub = List.smartmap (subst_rel_declaration sub) + +let subst_template_cst_arity sub (ctx,s as arity) = + let ctx' = subst_rel_context sub ctx in + if ctx==ctx' then arity else (ctx',s) + +let subst_arity sub s = subst_decl_arity subst_mps subst_template_cst_arity sub s (* TODO: should be changed to non-coping after Term.subst_mps *) (* NB: we leave bytecode and native code fields untouched *) @@ -501,6 +536,18 @@ let subst_const_body sub cb = const_body = subst_constant_def sub cb.const_body; const_type = subst_arity sub cb.const_type } + +let subst_regular_ind_arity sub s = + let uar' = subst_mps sub s.mind_user_arity in + if uar' == s.mind_user_arity then s + else { mind_user_arity = uar'; mind_sort = s.mind_sort } + +let subst_template_ind_arity sub s = s + +(* FIXME records *) +let subst_ind_arity = + subst_decl_arity subst_regular_ind_arity subst_template_ind_arity + let subst_mind_packet sub mbp = { mind_consnames = mbp.mind_consnames; mind_consnrealdecls = mbp.mind_consnrealdecls; @@ -508,7 +555,7 @@ let subst_mind_packet sub mbp = mind_typename = mbp.mind_typename; mind_nf_lc = Array.smartmap (subst_mps sub) mbp.mind_nf_lc; mind_arity_ctxt = subst_rel_context sub mbp.mind_arity_ctxt; - mind_arity = subst_arity sub mbp.mind_arity; + mind_arity = subst_ind_arity sub mbp.mind_arity; mind_user_lc = Array.smartmap (subst_mps sub) mbp.mind_user_lc; mind_nrealargs = mbp.mind_nrealargs; mind_nrealargs_ctxt = mbp.mind_nrealargs_ctxt; diff --git a/checker/environ.ml b/checker/environ.ml index 79234e9e2..d650e194e 100644 --- a/checker/environ.ml +++ b/checker/environ.ml @@ -84,6 +84,9 @@ let add_constraints c env = { env with env_stratification = { s with env_universes = merge_constraints c s.env_universes } } +let check_constraints cst env = + Univ.check_constraints cst env.env_stratification.env_universes + (* Global constants *) let lookup_constant kn env = @@ -104,20 +107,54 @@ let add_constant kn cs env = type const_evaluation_result = NoBody | Opaque +(* Constant types *) + +let universes_and_subst_of cb u = + let univs = cb.const_universes in + let subst = Univ.make_universe_subst u univs in + subst, Univ.instantiate_univ_context subst univs + +let map_regular_arity f = function + | RegularArity a as ar -> + let a' = f a in + if a' == a then ar else RegularArity a' + | TemplateArity _ -> assert false + +(* constant_type gives the type of a constant *) +let constant_type env (kn,u) = + let cb = lookup_constant kn env in + if cb.const_polymorphic then + let subst, csts = universes_and_subst_of cb u in + (map_regular_arity (subst_univs_constr subst) cb.const_type, csts) + else cb.const_type, Univ.Constraint.empty + exception NotEvaluableConst of const_evaluation_result -let constant_value env kn = +let constant_value env (kn,u) = let cb = lookup_constant kn env in - match cb.const_body with - | Def l_body -> force_constr l_body + match cb.const_body with + | Def l_body -> + let b = force_constr l_body in + if cb.const_polymorphic then + let subst = Univ.make_universe_subst u cb.const_universes in + subst_univs_constr subst b + else b | OpaqueDef _ -> raise (NotEvaluableConst Opaque) | Undef _ -> raise (NotEvaluableConst NoBody) (* A global const is evaluable if it is defined and not opaque *) let evaluable_constant cst env = - try let _ = constant_value env cst in true + try let _ = constant_value env (cst, Univ.Instance.empty) in true with Not_found | NotEvaluableConst _ -> false +let is_projection cst env = + not (Option.is_empty (lookup_constant cst env).const_proj) + +let lookup_projection cst env = + match (lookup_constant cst env).const_proj with + | Some pb -> pb + | None -> anomaly ("lookup_projection: constant is not a projection") + (* Mutual Inductives *) let scrape_mind env kn= try diff --git a/checker/environ.mli b/checker/environ.mli index 46b390d0a..d3448b127 100644 --- a/checker/environ.mli +++ b/checker/environ.mli @@ -39,15 +39,20 @@ val push_rec_types : name array * constr array * 'a -> env -> env (* Universes *) val universes : env -> Univ.universes val add_constraints : Univ.constraints -> env -> env +val check_constraints : Univ.constraints -> env -> bool (* Constants *) val lookup_constant : constant -> env -> Cic.constant_body val add_constant : constant -> Cic.constant_body -> env -> env +val constant_type : env -> constant puniverses -> constant_type Univ.constrained type const_evaluation_result = NoBody | Opaque exception NotEvaluableConst of const_evaluation_result -val constant_value : env -> constant -> constr +val constant_value : env -> constant puniverses -> constr val evaluable_constant : constant -> env -> bool +val is_projection : constant -> env -> bool +val lookup_projection : constant -> env -> projection_body + (* Inductives *) val mind_equiv : env -> inductive -> inductive -> bool diff --git a/checker/indtypes.ml b/checker/indtypes.ml index 5927e1633..bfc20d7f8 100644 --- a/checker/indtypes.ml +++ b/checker/indtypes.ml @@ -139,12 +139,15 @@ let typecheck_arity env params inds = let nparamargs = rel_context_nhyps params in let nparamdecls = rel_context_length params in let check_arity arctxt = function - mar -> - let _ = infer_type env mar in - mar in - (* | Polymorphic par -> *) - (* check_polymorphic_arity env params par; *) - (* it_mkProd_or_LetIn (Sort(Type par.poly_level)) arctxt in *) + | RegularArity mar -> + let ar = mar.mind_user_arity in + let _ = infer_type env ar in + conv env (it_mkProd_or_LetIn (Sort mar.mind_sort) arctxt) ar; + ar + | TemplateArity par -> + check_polymorphic_arity env params par; + it_mkProd_or_LetIn (Sort(Type par.template_level)) arctxt + in let env_arities = Array.fold_left (fun env_ar ind -> @@ -189,8 +192,8 @@ let check_predicativity env s small level = let sort_of_ind = function - mar -> snd (destArity mar) - (* | Polymorphic par -> Type par.poly_level *) + | RegularArity mar -> mar.mind_sort + | TemplateArity par -> Type par.template_level let all_sorts = [InProp;InSet;InType] let small_sorts = [InProp;InSet] @@ -371,12 +374,12 @@ let abstract_mind_lc env ntyps npars lc = let ienv_push_var (env, n, ntypes, lra) (x,a,ra) = (push_rel (x,None,a) env, n+1, ntypes, (Norec,ra)::lra) -let ienv_push_inductive (env, n, ntypes, ra_env) (mi,lpar) = +let ienv_push_inductive (env, n, ntypes, ra_env) ((mi,u),lpar) = let auxntyp = 1 in let specif = lookup_mind_specif env mi in let env' = push_rel (Anonymous,None, - hnf_prod_applist env (type_of_inductive env specif) lpar) env in + hnf_prod_applist env (type_of_inductive env (specif,u)) lpar) env in let ra_env' = (Imbr mi,(Rtree.mk_rec_calls 1).(0)) :: List.map (fun (r,t) -> (r,Rtree.lift 1 t)) ra_env in @@ -429,7 +432,7 @@ let check_positivity_one (env, _,ntypes,_ as ienv) hyps nrecp (_,i as ind) indlc else failwith_non_pos_list n ntypes (x::largs) (* accesses to the environment are not factorised, but is it worth it? *) - and check_positive_imbr (env,n,ntypes,ra_env as ienv) (mi, largs) = + and check_positive_imbr (env,n,ntypes,ra_env as ienv) ((mi,u), largs) = let (mib,mip) = lookup_mind_specif env mi in let auxnpar = mib.mind_nparams_rec in let nonrecpar = mib.mind_nparams - auxnpar in @@ -447,7 +450,7 @@ let check_positivity_one (env, _,ntypes,_ as ienv) hyps nrecp (_,i as ind) indlc let auxlcvect = abstract_mind_lc env auxntyp auxnpar mip.mind_nf_lc in (* Extends the environment with a variable corresponding to the inductive def *) - let (env',_,_,_ as ienv') = ienv_push_inductive ienv (mi,lpar) in + let (env',_,_,_ as ienv') = ienv_push_inductive ienv ((mi,u),lpar) in (* Parameters expressed in env' *) let lpar' = List.map (lift auxntyp) lpar in let irecargs = @@ -528,7 +531,7 @@ let check_positivity env_ar mind params nrecp inds = let check_inductive env kn mib = Flags.if_verbose ppnl (str " checking ind: " ++ pr_mind kn); pp_flush (); (* check mind_constraints: should be consistent with env *) - let env = add_constraints mib.mind_constraints env in + let env = add_constraints (Univ.UContext.constraints mib.mind_universes) env in (* check mind_record : TODO ? check #constructor = 1 ? *) (* check mind_finite : always OK *) (* check mind_ntypes *) diff --git a/checker/inductive.ml b/checker/inductive.ml index b32379b35..55acd9f97 100644 --- a/checker/inductive.ml +++ b/checker/inductive.ml @@ -39,32 +39,58 @@ let find_rectype env c = let find_inductive env c = let (t, l) = decompose_app (whd_betadeltaiota env c) in match t with - | Ind ind + | Ind (ind,_) when (fst (lookup_mind_specif env ind)).mind_finite -> (ind, l) | _ -> raise Not_found let find_coinductive env c = let (t, l) = decompose_app (whd_betadeltaiota env c) in match t with - | Ind ind + | Ind (ind,_) when not (fst (lookup_mind_specif env ind)).mind_finite -> (ind, l) | _ -> raise Not_found let inductive_params (mib,_) = mib.mind_nparams +(** Polymorphic inductives *) + +let make_inductive_subst mib u = + if mib.mind_polymorphic then + make_universe_subst u mib.mind_universes + else Univ.empty_subst + +let inductive_params_ctxt (mib,u) = + let subst = make_inductive_subst mib u in + subst_univs_context subst mib.mind_params_ctxt + +let inductive_instance mib = + if mib.mind_polymorphic then + UContext.instance mib.mind_universes + else Instance.empty + +let inductive_context mib = + if mib.mind_polymorphic then + mib.mind_universes + else UContext.empty + +let instantiate_inductive_constraints mib subst = + if mib.mind_polymorphic then + instantiate_univ_context subst mib.mind_universes + else Constraint.empty + (************************************************************************) (* Build the substitution that replaces Rels by the appropriate *) (* inductives *) -let ind_subst mind mib = +let ind_subst mind mib u = let ntypes = mib.mind_ntypes in - let make_Ik k = Ind (mind,ntypes-k-1) in + let make_Ik k = Ind ((mind,ntypes-k-1),u) in List.init ntypes make_Ik (* Instantiate inductives in constructor type *) -let constructor_instantiate mind mib c = - let s = ind_subst mind mib in - substl s c +let constructor_instantiate mind u subst mib c = + let s = ind_subst mind mib u in + substl s (subst_univs_constr subst c) let instantiate_params full t args sign = let fail () = @@ -83,13 +109,16 @@ let instantiate_params full t args sign = if rem_args <> [] then fail(); substl subs ty -let full_inductive_instantiate mib params sign = +let full_inductive_instantiate mib u params sign = let dummy = Prop Null in let t = mkArity (sign,dummy) in - fst (destArity (instantiate_params true t params mib.mind_params_ctxt)) + let subst = make_inductive_subst mib u in + let ar = fst (destArity (instantiate_params true t params mib.mind_params_ctxt)) in + subst_univs_context subst ar -let full_constructor_instantiate ((mind,_),(mib,_),params) = - let inst_ind = constructor_instantiate mind mib in +let full_constructor_instantiate ((mind,_),u,(mib,_),params) = + let subst = make_inductive_subst mib u in + let inst_ind = constructor_instantiate mind u subst mib in (fun t -> instantiate_params true (inst_ind t) params mib.mind_params_ctxt) @@ -173,25 +202,82 @@ let rec make_subst env = function | [], _, _ -> assert false -(* let instantiate_universes env ctx ar argsorts = *) -(* let args = Array.to_list argsorts in *) -(* let ctx,subst = make_subst env (ctx,ar.poly_param_levels,args) in *) -(* let level = subst_large_constraints subst ar.poly_level in *) -(* ctx, *) -(* if is_type0m_univ level then Prop Null *) -(* else if is_type0_univ level then Prop Pos *) -(* else Type level *) - -let type_of_inductive_knowing_parameters env mip paramtyps = - mip.mind_arity - (* | Polymorphic ar -> *) - (* let ctx = List.rev mip.mind_arity_ctxt in *) - (* let ctx,s = instantiate_universes env ctx ar paramtyps in *) - (* mkArity (List.rev ctx,s) *) + +exception SingletonInductiveBecomesProp of Id.t + +let instantiate_universes env ctx ar argsorts = + let args = Array.to_list argsorts in + let ctx,subst = make_subst env (ctx,ar.template_param_levels,args) in + let level = subst_large_constraints subst ar.template_level in + let ty = + (* Singleton type not containing types are interpretable in Prop *) + if is_type0m_univ level then Prop Null + (* Non singleton type not containing types are interpretable in Set *) + else if is_type0_univ level then Prop Pos + (* This is a Type with constraints *) + else Type level + in + (ctx, ty) + +(* Type of an inductive type *) + +let is_prop_sort = function + | Prop Null -> true + | _ -> false + +let type_of_inductive_subst ?(polyprop=true) env ((mib,mip),u) paramtyps = + match mip.mind_arity with + | RegularArity a -> + if not mib.mind_polymorphic then (a.mind_user_arity, Univ.LMap.empty) + else + let subst = make_inductive_subst mib u in + (subst_univs_constr subst a.mind_user_arity, subst) + | TemplateArity ar -> + let ctx = List.rev mip.mind_arity_ctxt in + let ctx,s = instantiate_universes env ctx ar paramtyps in + (* The Ocaml extraction cannot handle (yet?) "Prop-polymorphism", i.e. + the situation where a non-Prop singleton inductive becomes Prop + when applied to Prop params *) + if not polyprop && not (is_type0m_univ ar.template_level) && is_prop_sort s + then raise (SingletonInductiveBecomesProp mip.mind_typename); + mkArity (List.rev ctx,s), Univ.LMap.empty + +let type_of_inductive_gen ?(polyprop=true) env ((mib,mip),u) paramtyps = + match mip.mind_arity with + | RegularArity a -> + if not mib.mind_polymorphic then a.mind_user_arity + else + let subst = make_inductive_subst mib u in + (subst_univs_constr subst a.mind_user_arity) + | TemplateArity ar -> + let ctx = List.rev mip.mind_arity_ctxt in + let ctx,s = instantiate_universes env ctx ar paramtyps in + (* The Ocaml extraction cannot handle (yet?) "Prop-polymorphism", i.e. + the situation where a non-Prop singleton inductive becomes Prop + when applied to Prop params *) + if not polyprop && not (is_type0m_univ ar.template_level) && is_prop_sort s + then raise (SingletonInductiveBecomesProp mip.mind_typename); + mkArity (List.rev ctx,s) + +let type_of_inductive env pind = + type_of_inductive_gen env pind [||] + +let constrained_type_of_inductive env ((mib,mip),u as pind) = + let ty, subst = type_of_inductive_subst env pind [||] in + let cst = instantiate_inductive_constraints mib subst in + (ty, cst) + +let constrained_type_of_inductive_knowing_parameters env ((mib,mip),u as pind) args = + let ty, subst = type_of_inductive_subst env pind args in + let cst = instantiate_inductive_constraints mib subst in + (ty, cst) + +let type_of_inductive_knowing_parameters env mip args = + type_of_inductive_gen env mip args (* Type of a (non applied) inductive type *) -let type_of_inductive env (_,mip) = +let type_of_inductive env mip = type_of_inductive_knowing_parameters env mip [||] (* The max of an array of universes *) @@ -207,17 +293,36 @@ let max_inductive_sort = (************************************************************************) (* Type of a constructor *) -let type_of_constructor cstr (mib,mip) = +let type_of_constructor_subst cstr u subst (mib,mip) = let ind = inductive_of_constructor cstr in let specif = mip.mind_user_lc in let i = index_of_constructor cstr in let nconstr = Array.length mip.mind_consnames in - if i > nconstr then error "Not enough constructors in the type"; - constructor_instantiate (fst ind) mib specif.(i-1) + if i > nconstr then error "Not enough constructors in the type."; + let c = constructor_instantiate (fst ind) u subst mib specif.(i-1) in + c + +let type_of_constructor_gen (cstr,u) (mib,mip as mspec) = + let subst = make_inductive_subst mib u in + type_of_constructor_subst cstr u subst mspec, subst + +let type_of_constructor cstru mspec = + fst (type_of_constructor_gen cstru mspec) -let arities_of_specif kn (mib,mip) = +let type_of_constructor_in_ctx cstr (mib,mip as mspec) = + let u = UContext.instance mib.mind_universes in + let c = type_of_constructor_gen (cstr, u) mspec in + (fst c, mib.mind_universes) + +let constrained_type_of_constructor (cstr,u as cstru) (mib,mip as ind) = + let ty, subst = type_of_constructor_gen cstru ind in + let cst = instantiate_inductive_constraints mib subst in + (ty, cst) + +let arities_of_specif (kn,u) (mib,mip) = let specif = mip.mind_nf_lc in - Array.map (constructor_instantiate kn mib) specif + let subst = make_inductive_subst mib u in + Array.map (constructor_instantiate kn u subst mib) specif @@ -234,14 +339,16 @@ let error_elim_expln kp ki = (* Get type of inductive, with parameters instantiated *) let inductive_sort_family mip = - family_of_sort (snd (destArity mip.mind_arity)) + match mip.mind_arity with + | RegularArity s -> family_of_sort s.mind_sort + | TemplateArity _ -> InType let mind_arity mip = mip.mind_arity_ctxt, inductive_sort_family mip -let get_instantiated_arity (mib,mip) params = +let get_instantiated_arity (ind,u) (mib,mip) params = let sign, s = mind_arity mip in - full_inductive_instantiate mib params sign, s + full_inductive_instantiate mib u params sign, s let elim_sorts (_,mip) = mip.mind_kelim @@ -269,7 +376,7 @@ let check_allowed_sort ksort specif = raise (LocalArity (Some(ksort,s,error_elim_expln ksort s))) let is_correct_arity env c (p,pj) ind specif params = - let arsign,_ = get_instantiated_arity specif params in + let arsign,_ = get_instantiated_arity ind specif params in let rec srec env pt ar = let pt' = whd_betadeltaiota env pt in match pt', ar with @@ -305,9 +412,9 @@ let is_correct_arity env c (p,pj) ind specif params = (* [p] is the predicate, [i] is the constructor number (starting from 0), and [cty] is the type of the constructor (params not instantiated) *) -let build_branches_type ind (_,mip as specif) params dep p = +let build_branches_type (ind,u) (_,mip as specif) params dep p = let build_one_branch i cty = - let typi = full_constructor_instantiate (ind,specif,params) cty in + let typi = full_constructor_instantiate (ind,u,specif,params) cty in let (args,ccl) = decompose_prod_assum typi in let nargs = rel_context_length args in let (_,allargs) = decompose_app ccl in @@ -316,7 +423,7 @@ let build_branches_type ind (_,mip as specif) params dep p = if dep then let cstr = ith_constructor_of_inductive ind (i+1) in let dep_cstr = - applist (Construct cstr,lparams@extended_rel_list 0 args) in + applist (Construct (cstr,u),lparams@extended_rel_list 0 args) in vargs @ [dep_cstr] else vargs in @@ -330,12 +437,12 @@ let build_case_type dep p c realargs = let args = if dep then realargs@[c] else realargs in beta_appvect p (Array.of_list args) -let type_case_branches env (ind,largs) (p,pj) c = - let specif = lookup_mind_specif env ind in +let type_case_branches env (pind,largs) (p,pj) c = + let specif = lookup_mind_specif env (fst pind) in let nparams = inductive_params specif in let (params,realargs) = List.chop nparams largs in - let dep = is_correct_arity env c (p,pj) ind specif params in - let lc = build_branches_type ind specif params dep p in + let dep = is_correct_arity env c (p,pj) pind specif params in + let lc = build_branches_type pind specif params dep p in let ty = build_case_type dep p c realargs in (lc, ty) @@ -724,11 +831,11 @@ let check_one_fix renv recpos def = else check_rec_call renv' [] body) bodies - | Const kn -> + | Const (kn,u) -> if evaluable_constant kn renv.env then try List.iter (check_rec_call renv []) l with (FixGuardError _ ) -> - let value = (applist(constant_value renv.env kn, l)) in + let value = (applist(constant_value renv.env (kn,u), l)) in check_rec_call renv stack value else List.iter (check_rec_call renv []) l @@ -761,6 +868,8 @@ let check_one_fix renv recpos def = | (App _ | LetIn _ | Cast _) -> assert false (* beta zeta reduction *) + | Proj (p, c) -> check_rec_call renv [] c + and check_nested_fix_body renv decr recArgsDecrArg body = if decr = 0 then check_rec_call (assign_var_spec renv (1,recArgsDecrArg)) [] body @@ -859,7 +968,7 @@ let check_one_cofix env nbfix def deftype = else if not(List.for_all (noccur_with_meta n nbfix) args) then raise (CoFixGuardError (env,NestedRecursiveOccurrences)) - | Construct (_,i as cstr_kn) -> + | Construct ((_,i as cstr_kn),u) -> let lra = vlra.(i-1) in let mI = inductive_of_constructor cstr_kn in let (mib,mip) = lookup_mind_specif env mI in diff --git a/checker/inductive.mli b/checker/inductive.mli index 082bdae19..e223af0c9 100644 --- a/checker/inductive.mli +++ b/checker/inductive.mli @@ -14,7 +14,7 @@ open Environ (*s Extracting an inductive type from a construction *) -val find_rectype : env -> constr -> inductive * constr list +val find_rectype : env -> constr -> pinductive * constr list type mind_specif = mutual_inductive_body * one_inductive_body @@ -22,12 +22,15 @@ type mind_specif = mutual_inductive_body * one_inductive_body Raises [Not_found] if the inductive type is not found. *) val lookup_mind_specif : env -> inductive -> mind_specif -val type_of_inductive : env -> mind_specif -> constr +val make_inductive_subst : mutual_inductive_body -> Univ.universe_instance -> Univ.universe_subst +val inductive_instance : mutual_inductive_body -> Univ.universe_instance + +val type_of_inductive : env -> mind_specif puniverses -> constr (* Return type as quoted by the user *) -val type_of_constructor : constructor -> mind_specif -> constr +val type_of_constructor : pconstructor -> mind_specif -> constr -val arities_of_specif : mutual_inductive -> mind_specif -> constr array +val arities_of_specif : mutual_inductive puniverses -> mind_specif -> constr array (* [type_case_branches env (I,args) (p:A) c] computes useful types about the following Cases expression: @@ -36,7 +39,7 @@ val arities_of_specif : mutual_inductive -> mind_specif -> constr array introduced by products) and the type for the whole expression. *) val type_case_branches : - env -> inductive * constr list -> constr * constr -> constr + env -> pinductive * constr list -> constr * constr -> constr -> constr array * constr (* Check a [case_info] actually correspond to a Case expression on the @@ -50,12 +53,12 @@ val check_cofix : env -> cofixpoint -> unit (*s Support for sort-polymorphic inductive types *) val type_of_inductive_knowing_parameters : - env -> one_inductive_body -> constr array -> constr + env -> mind_specif puniverses -> constr array -> constr val max_inductive_sort : sorts array -> Univ.universe -(* val instantiate_universes : env -> rel_context -> *) -(* inductive_arity -> constr array -> rel_context * sorts *) +val instantiate_universes : env -> rel_context -> + template_arity -> constr array -> rel_context * sorts (***************************************************************) (* Debug *) diff --git a/checker/mod_checking.ml b/checker/mod_checking.ml index 53316a2cb..12a97bf68 100644 --- a/checker/mod_checking.ml +++ b/checker/mod_checking.ml @@ -14,30 +14,31 @@ open Environ (** {6 Checking constants } *) -(* let refresh_arity ar = *) -(* let ctxt, hd = decompose_prod_assum ar in *) -(* match hd with *) -(* Sort (Type u) when not (Univ.is_univ_variable u) -> *) -(* let u' = Univ.fresh_local_univ() in *) -(* mkArity (ctxt,Type u'), *) -(* Univ.enforce_leq u u' Univ.empty_constraint *) -(* | _ -> ar, Univ.empty_constraint *) +let refresh_arity ar = + let ctxt, hd = decompose_prod_assum ar in + match hd with + Sort (Type u) when not (Univ.is_univ_variable u) -> + let u' = Univ.Universe.make (Univ.Level.make empty_dirpath 1) in + mkArity (ctxt,Prop Null), + Univ.enforce_leq u u' Univ.empty_constraint + | _ -> ar, Univ.empty_constraint let check_constant_declaration env kn cb = Flags.if_verbose ppnl (str " checking cst: " ++ prcon kn); -(* let env = add_constraints cb.const_constraints env in*) + let env = add_constraints (Univ.UContext.constraints cb.const_universes) env in (match cb.const_type with - ty -> - let env' = add_constraints cb.const_constraints env in (*MS: FIXME*) - let _ = infer_type env' ty in - (match body_of_constant cb with + RegularArity ty -> + let ty, cu = refresh_arity ty in + let envty = add_constraints cu env in + let _ = infer_type envty ty in + (match body_of_constant cb with | Some bd -> - let j = infer env' bd in - conv_leq env' j ty + let j = infer envty bd in + conv_leq envty j ty | None -> ()) - (* | PolymorphicArity(ctxt,par) -> *) - (* let _ = check_ctxt env ctxt in *) - (* check_polymorphic_arity env ctxt par *)); + | TemplateArity(ctxt,par) -> + let _ = check_ctxt env ctxt in + check_polymorphic_arity env ctxt par); add_constant kn cb env diff --git a/checker/modops.ml b/checker/modops.ml index 2d20dd0f3..c27c5d598 100644 --- a/checker/modops.ml +++ b/checker/modops.ml @@ -90,7 +90,11 @@ let strengthen_const mp_from l cb resolver = | _ -> let con = Constant.make2 mp_from l in (* let con = constant_of_delta resolver con in*) - { cb with const_body = Def (Declarations.from_val (Const con)) } + let u = + if cb.const_polymorphic then Univ.UContext.instance cb.const_universes + else Univ.Instance.empty + in + { cb with const_body = Def (Declarations.from_val (Const (con,u))) } let rec strengthen_mod mp_from mp_to mb = if Declarations.mp_in_delta mb.mod_mp mb.mod_delta then diff --git a/checker/print.ml b/checker/print.ml index f25b8cf09..8a5464dae 100644 --- a/checker/print.ml +++ b/checker/print.ml @@ -10,6 +10,8 @@ open Format open Cic open Names +let print_instance i = Pp.pp (Univ.Instance.pr i) + let print_pure_constr csr = let rec term_display c = match c with | Rel n -> print_string "#"; print_int n @@ -43,19 +45,22 @@ let print_pure_constr csr = Array.iter (fun x -> print_space (); box_display x) l; print_string ")" | Evar _ -> print_string "Evar#" - | Const c -> print_string "Cons("; + | Const (c,u) -> print_string "Cons("; sp_con_display c; + print_string ","; print_instance u; print_string ")" - | Ind (sp,i) -> + | Ind ((sp,i),u) -> print_string "Ind("; sp_display sp; print_string ","; print_int i; + print_string ","; print_instance u; print_string ")" - | Construct ((sp,i),j) -> + | Construct (((sp,i),j),u) -> print_string "Constr("; sp_display sp; print_string ","; - print_int i; print_string ","; print_int j; print_string ")" + print_int i; print_string ","; print_int j; + print_string ","; print_instance u; print_string ")" | Case (ci,p,c,bl) -> open_vbox 0; print_string "<"; box_display p; print_string ">"; @@ -94,6 +99,9 @@ let print_pure_constr csr = print_cut(); done in print_string"{"; print_fix (); print_string"}" + | Proj (p, c) -> + print_string "Proj("; sp_con_display p; print_string ","; + box_display c; print_string ")" and box_display c = open_hovbox 1; term_display c; close_box() diff --git a/checker/reduction.ml b/checker/reduction.ml index 54d79484e..384b9ad7f 100644 --- a/checker/reduction.ml +++ b/checker/reduction.ml @@ -50,6 +50,7 @@ let compare_stack_shape stk1 stk2 = type lft_constr_stack_elt = Zlapp of (lift * fconstr) array + | Zlproj of Names.constant * lift | Zlfix of (lift * fconstr) * lft_constr_stack | Zlcase of case_info * lift * fconstr * fconstr array and lft_constr_stack = lft_constr_stack_elt list @@ -68,6 +69,8 @@ let pure_stack lfts stk = | (Zshift n,(l,pstk)) -> (el_shft n l, pstk) | (Zapp a, (l,pstk)) -> (l,zlapp (Array.map (fun t -> (l,t)) a) pstk) + | (Zproj (n,m,c), (l,pstk)) -> + (l, Zlproj (c,l)::pstk) | (Zfix(fx,a),(l,pstk)) -> let (lfx,pa) = pure_rec l a in (l, Zlfix((lfx,fx),pa)::pstk) @@ -116,6 +119,10 @@ type 'a conversion_function = env -> 'a -> 'a -> unit exception NotConvertible exception NotConvertibleVect of int +let convert_universes univ u u' = + if Univ.Instance.check_eq univ u u' then () + else raise NotConvertible + let compare_stacks f fmind lft1 stk1 lft2 stk2 = let rec cmp_rec pstk1 pstk2 = match (pstk1,pstk2) with @@ -163,6 +170,7 @@ let rec no_arg_available = function | Zupdate _ :: stk -> no_arg_available stk | Zshift _ :: stk -> no_arg_available stk | Zapp v :: stk -> Array.length v = 0 && no_arg_available stk + | Zproj _ :: _ -> true | Zcase _ :: _ -> true | Zfix _ :: _ -> true @@ -174,6 +182,7 @@ let rec no_nth_arg_available n = function let k = Array.length v in if n >= k then no_nth_arg_available (n-k) stk else false + | Zproj _ :: _ -> true | Zcase _ :: _ -> true | Zfix _ :: _ -> true @@ -182,6 +191,7 @@ let rec no_case_available = function | Zupdate _ :: stk -> no_case_available stk | Zshift _ :: stk -> no_case_available stk | Zapp _ :: stk -> no_case_available stk + | Zproj (_,_,_) :: _ -> false | Zcase _ :: _ -> false | Zfix _ :: _ -> true @@ -192,7 +202,7 @@ let in_whnf (t,stk) = | FConstruct _ -> no_case_available stk | FCoFix _ -> no_case_available stk | FFix(((ri,n),(_,_,_)),_) -> no_nth_arg_available ri.(n) stk - | (FFlex _ | FProd _ | FEvar _ | FInd _ | FAtom _ | FRel _) -> true + | (FFlex _ | FProd _ | FEvar _ | FInd _ | FAtom _ | FRel _ | FProj _) -> true | FLOCKED -> assert false let oracle_order fl1 fl2 = @@ -201,6 +211,15 @@ let oracle_order fl1 fl2 = | _, ConstKey _ -> true | _ -> false +let unfold_projection infos p c = + (* if RedFlags.red_set infos.i_flags (RedFlags.fCONST p) then *) + (match try Some (lookup_projection p (infos_env infos)) with Not_found -> None with + | Some pb -> + let s = Zproj (pb.proj_npars, pb.proj_arg, p) in + Some (c, s) + | None -> None) + (* else None *) + (* Conversion between [lft1]term1 and [lft2]term2 *) let rec ccnv univ cv_pb infos lft1 lft2 term1 term2 = eqappr univ cv_pb infos (lft1, (term1,[])) (lft2, (term2,[])) @@ -255,19 +274,49 @@ and eqappr univ cv_pb infos (lft1,st1) (lft2,st2) = let (app1,app2) = if oracle_order fl1 fl2 then match unfold_reference infos fl1 with - | Some def1 -> ((lft1, whd_stack infos def1 v1), appr2) - | None -> - (match unfold_reference infos fl2 with - | Some def2 -> (appr1, (lft2, whd_stack infos def2 v2)) - | None -> raise NotConvertible) + | Some def1 -> ((lft1, whd_stack infos def1 v1), appr2) + | None -> + (match unfold_reference infos fl2 with + | Some def2 -> (appr1, (lft2, whd_stack infos def2 v2)) + | None -> raise NotConvertible) else match unfold_reference infos fl2 with - | Some def2 -> (appr1, (lft2, whd_stack infos def2 v2)) - | None -> - (match unfold_reference infos fl1 with - | Some def1 -> ((lft1, whd_stack infos def1 v1), appr2) - | None -> raise NotConvertible) in - eqappr univ cv_pb infos app1 app2) + | Some def2 -> (appr1, (lft2, whd_stack infos def2 v2)) + | None -> + (match unfold_reference infos fl1 with + | Some def1 -> ((lft1, whd_stack infos def1 v1), appr2) + | None -> raise NotConvertible) in + eqappr univ cv_pb infos app1 app2) + + | (FProj (p1,c1), FProj (p2, c2)) -> + (* Projections: prefer unfolding to first-order unification, + which will happen naturally if the terms c1, c2 are not in constructor + form *) + (match unfold_projection infos p1 c1 with + | Some (def1,s1) -> + eqappr univ cv_pb infos (lft1, whd_stack infos def1 (s1 :: v1)) appr2 + | None -> + match unfold_projection infos p2 c2 with + | Some (def2,s2) -> + eqappr univ cv_pb infos appr1 (lft2, whd_stack infos def2 (s2 :: v2)) + | None -> + if Names.eq_con_chk p1 p2 && compare_stack_shape v1 v2 then + let () = ccnv univ CONV infos el1 el2 c1 c2 in + convert_stacks univ infos lft1 lft2 v1 v2 + else (* Two projections in WHNF: unfold *) + raise NotConvertible) + + | (FProj (p1,c1), t2) -> + (match unfold_projection infos p1 c1 with + | Some (def1,s1) -> + eqappr univ cv_pb infos (lft1, whd_stack infos def1 (s1 :: v1)) appr2 + | None -> raise NotConvertible) + + | (_, FProj (p2,c2)) -> + (match unfold_projection infos p2 c2 with + | Some (def2,s2) -> + eqappr univ cv_pb infos appr1 (lft2, whd_stack infos def2 (s2 :: v2)) + | None -> raise NotConvertible) (* other constructors *) | (FLambda _, FLambda _) -> @@ -300,29 +349,47 @@ and eqappr univ cv_pb infos (lft1,st1) (lft2,st2) = (el_lift lft1,(hd1,eta_expand_stack v1)) (el_lift lft2,(bd2,[])) (* only one constant, defined var or defined rel *) - | (FFlex fl1, _) -> + | (FFlex fl1, c2) -> (match unfold_reference infos fl1 with | Some def1 -> eqappr univ cv_pb infos (lft1, whd_stack infos def1 v1) appr2 - | None -> raise NotConvertible) - | (_, FFlex fl2) -> + | None -> + match c2 with + | FConstruct ((ind2,j2),u2) -> + (try + let v2, v1 = + eta_expand_ind_stacks (infos_env infos) ind2 hd2 v2 (snd appr1) + in convert_stacks univ infos lft1 lft2 v1 v2 + with Not_found -> raise NotConvertible) + | _ -> raise NotConvertible) + + | (c1, FFlex fl2) -> (match unfold_reference infos fl2 with | Some def2 -> eqappr univ cv_pb infos appr1 (lft2, whd_stack infos def2 v2) - | None -> raise NotConvertible) + | None -> + match c1 with + | FConstruct ((ind1,j1),u1) -> + (try let v1, v2 = + eta_expand_ind_stacks (infos_env infos) ind1 hd1 v1 (snd appr2) + in convert_stacks univ infos lft1 lft2 v1 v2 + with Not_found -> raise NotConvertible) + | _ -> raise NotConvertible) (* Inductive types: MutInd MutConstruct Fix Cofix *) - | (FInd ind1, FInd ind2) -> - if mind_equiv_infos infos ind1 ind2 - then - convert_stacks univ infos lft1 lft2 v1 v2 - else raise NotConvertible + | (FInd (ind1,u1), FInd (ind2,u2)) -> + if mind_equiv_infos infos ind1 ind2 + then + (let () = convert_universes univ u1 u2 in + convert_stacks univ infos lft1 lft2 v1 v2) + else raise NotConvertible - | (FConstruct (ind1,j1), FConstruct (ind2,j2)) -> + | (FConstruct ((ind1,j1),u1), FConstruct ((ind2,j2),u2)) -> if Int.equal j1 j2 && mind_equiv_infos infos ind1 ind2 then - convert_stacks univ infos lft1 lft2 v1 v2 + (let () = convert_universes univ u1 u2 in + convert_stacks univ infos lft1 lft2 v1 v2) else raise NotConvertible | (FFix ((op1,(_,tys1,cl1)),e1), FFix((op2,(_,tys2,cl2)),e2)) -> diff --git a/checker/subtyping.ml b/checker/subtyping.ml index 070ed1924..6c66ca60b 100644 --- a/checker/subtyping.ml +++ b/checker/subtyping.ml @@ -93,6 +93,15 @@ let check_inductive env mp1 l info1 mib2 spec2 subst1 subst2= | _ -> error () in let mib2 = subst_mind subst2 mib2 in + let check eq f = if not (eq (f mib1) (f mib2)) then error () in + let bool_equal (x : bool) (y : bool) = x = y in + let u = + check bool_equal (fun x -> x.mind_polymorphic); + if mib1.mind_polymorphic then ( + check Univ.Instance.equal (fun x -> Univ.UContext.instance x.mind_universes); + UContext.instance mib1.mind_universes) + else Instance.empty + in let check_inductive_type env t1 t2 = (* Due to sort-polymorphism in inductive types, the conclusions of @@ -146,15 +155,13 @@ let check_inductive env mp1 l info1 mib2 spec2 subst1 subst2= (* params_ctxt done because part of the inductive types *) (* Don't check the sort of the type if polymorphic *) check_inductive_type env - (type_of_inductive env (mib1,p1)) (type_of_inductive env (mib2,p2)) + (type_of_inductive env ((mib1,p1),u)) (type_of_inductive env ((mib2,p2),u)) in let check_cons_types i p1 p2 = Array.iter2 (check_conv conv env) - (arities_of_specif kn (mib1,p1)) - (arities_of_specif kn (mib2,p2)) + (arities_of_specif (kn,u) (mib1,p1)) + (arities_of_specif (kn,u) (mib2,p2)) in - let check eq f = if not (eq (f mib1) (f mib2)) then error () in - let bool_equal (x : bool) (y : bool) = x = y in check bool_equal (fun mib -> mib.mind_finite); check Int.equal (fun mib -> mib.mind_ntypes); assert (Array.length mib1.mind_packets >= 1 @@ -179,8 +186,15 @@ let check_inductive env mp1 l info1 mib2 spec2 subst1 subst2= if kn1 <> kn2 then error () end;*) (* we check that records and their field names are preserved. *) - check bool_equal (fun mib -> mib.mind_record); - if mib1.mind_record then begin + let record_equal x y = + match x, y with + | None, None -> true + | Some (r1,p1), Some (r2,p2) -> + eq_constr r1 r2 && Array.for_all2 eq_con_chk p1 p2 + | _, _ -> false + in + check record_equal (fun mib -> mib.mind_record); + if mib1.mind_record != None then begin let rec names_prod_letin t = match t with | Prod(n,_,t) -> n::(names_prod_letin t) | LetIn(n,_,_,t) -> n::(names_prod_letin t) @@ -282,7 +296,8 @@ let check_constant env mp1 l info1 cb2 spec2 subst1 subst2 = "inductive type and give a definition to map the old name to the new " ^ "name.")); if constant_has_body cb2 then error () ; - let arity1 = type_of_inductive env (mind1,mind1.mind_packets.(i)) in + let u = inductive_instance mind1 in + let arity1 = type_of_inductive env ((mind1,mind1.mind_packets.(i)),u) in let typ2 = Typeops.type_of_constant_type env cb2.const_type in check_conv conv_leq env arity1 typ2 | IndConstr (((kn,i),j) as cstr,mind1) -> @@ -292,7 +307,8 @@ let check_constant env mp1 l info1 cb2 spec2 subst1 subst2 = "constructor and give a definition to map the old name to the new " ^ "name.")); if constant_has_body cb2 then error () ; - let ty1 = type_of_constructor cstr (mind1,mind1.mind_packets.(i)) in + let u1 = inductive_instance mind1 in + let ty1 = type_of_constructor (cstr,u1) (mind1,mind1.mind_packets.(i)) in let ty2 = Typeops.type_of_constant_type env cb2.const_type in check_conv conv env ty1 ty2 diff --git a/checker/term.ml b/checker/term.ml index ea81f5dab..ad26c5edc 100644 --- a/checker/term.ml +++ b/checker/term.ml @@ -76,6 +76,7 @@ let iter_constr_with_binders g f n c = match c with | CoFix (_,(_,tl,bl)) -> Array.iter (f n) tl; Array.iter (f (iterate g (Array.length tl) n)) bl + | Proj (p, c) -> f n c exception LocalOccur @@ -152,6 +153,7 @@ let map_constr_with_binders g f l c = match c with | CoFix(ln,(lna,tl,bl)) -> let l' = iterate g (Array.length tl) l in CoFix (ln,(lna,Array.map (f l) tl,Array.map (f l') bl)) + | Proj (p, c) -> Proj (p, f l c) (* The generic lifting function *) let rec exliftn el c = match c with @@ -351,6 +353,9 @@ let compare_sorts s1 s2 = match s1, s2 with | Prop _, Type _ -> false | Type _, Prop _ -> false +let eq_puniverses f (c1,u1) (c2,u2) = + Univ.Instance.equal u1 u2 && f c1 c2 + let compare_constr f t1 t2 = match t1, t2 with | Rel n1, Rel n2 -> Int.equal n1 n2 @@ -372,9 +377,10 @@ let compare_constr f t1 t2 = f h1 h2 && List.for_all2 f l1 l2 else false | Evar (e1,l1), Evar (e2,l2) -> Int.equal e1 e2 && Array.equal f l1 l2 - | Const c1, Const c2 -> eq_con_chk c1 c2 - | Ind c1, Ind c2 -> eq_ind_chk c1 c2 - | Construct (c1,i1), Construct (c2,i2) -> Int.equal i1 i2 && eq_ind_chk c1 c2 + | Const c1, Const c2 -> eq_puniverses eq_con_chk c1 c2 + | Ind c1, Ind c2 -> eq_puniverses eq_ind_chk c1 c2 + | Construct ((c1,i1),u1), Construct ((c2,i2),u2) -> Int.equal i1 i2 && eq_ind_chk c1 c2 + && Univ.Instance.equal u1 u2 | Case (_,p1,c1,bl1), Case (_,p2,c2,bl2) -> f p1 p2 && f c1 c2 && Array.equal f bl1 bl2 | Fix ((ln1, i1),(_,tl1,bl1)), Fix ((ln2, i2),(_,tl2,bl2)) -> @@ -389,3 +395,88 @@ let rec eq_constr m n = compare_constr eq_constr m n let eq_constr m n = eq_constr m n (* to avoid tracing a recursive fun *) + +(* Universe substitutions *) + +let subst_univs_puniverses subst = + if Univ.is_empty_level_subst subst then fun c -> c + else + let f = Univ.Instance.subst subst in + fun ((c, u) as x) -> let u' = f u in if u' == u then x else (c, u') + +let subst_univs_fn_puniverses fn = + let f = Univ.Instance.subst_fn fn in + fun ((c, u) as x) -> let u' = f u in if u' == u then x else (c, u') + +let map_constr f c = map_constr_with_binders (fun x -> x) (fun _ c -> f c) 0 c + +let subst_univs_fn_constr f c = + let changed = ref false in + let fu = Univ.subst_univs_universe f in + let fi = Univ.Instance.subst_fn (Univ.level_subst_of f) in + let rec aux t = + match t with + | Sort (Type u) -> + let u' = fu u in + if u' == u then t else + (changed := true; Sort (Type u')) + | Const (c, u) -> + let u' = fi u in + if u' == u then t + else (changed := true; Const (c, u')) + | Ind (i, u) -> + let u' = fi u in + if u' == u then t + else (changed := true; Ind (i, u')) + | Construct (c, u) -> + let u' = fi u in + if u' == u then t + else (changed := true; Construct (c, u')) + | _ -> map_constr aux t + in + let c' = aux c in + if !changed then c' else c + +let subst_univs_constr subst c = + if Univ.is_empty_subst subst then c + else + let f = Univ.make_subst subst in + subst_univs_fn_constr f c + + +let subst_univs_level_constr subst c = + if Univ.is_empty_level_subst subst then c + else + let f = Univ.Instance.subst_fn (Univ.subst_univs_level_level subst) in + let changed = ref false in + let rec aux t = + match t with + | Const (c, u) -> + if Univ.Instance.is_empty u then t + else + let u' = f u in + if u' == u then t + else (changed := true; Const (c, u')) + | Ind (i, u) -> + if Univ.Instance.is_empty u then t + else + let u' = f u in + if u' == u then t + else (changed := true; Ind (i, u')) + | Construct (c, u) -> + if Univ.Instance.is_empty u then t + else + let u' = f u in + if u' == u then t + else (changed := true; Construct (c, u')) + | Sort (Type u) -> + let u' = Univ.subst_univs_level_universe subst u in + if u' == u then t else + (changed := true; Sort (Type u')) + | _ -> map_constr aux t + in + let c' = aux c in + if !changed then c' else c + +let subst_univs_context s = + map_rel_context (subst_univs_constr s) diff --git a/checker/term.mli b/checker/term.mli index f75341b9d..cf488f536 100644 --- a/checker/term.mli +++ b/checker/term.mli @@ -52,3 +52,7 @@ val destArity : constr -> arity val isArity : constr -> bool val compare_constr : (constr -> constr -> bool) -> constr -> constr -> bool val eq_constr : constr -> constr -> bool + +val subst_univs_constr : Univ.universe_subst -> constr -> constr +val subst_univs_level_constr : Univ.universe_level_subst -> constr -> constr +val subst_univs_context : Univ.universe_subst -> rel_context -> rel_context diff --git a/checker/type_errors.ml b/checker/type_errors.ml index e800ee3ef..565005b90 100644 --- a/checker/type_errors.ml +++ b/checker/type_errors.ml @@ -45,7 +45,7 @@ type type_error = | NotAType of unsafe_judgment | BadAssumption of unsafe_judgment | ReferenceVariables of constr - | ElimArity of inductive * sorts_family list * constr * unsafe_judgment + | ElimArity of pinductive * sorts_family list * constr * unsafe_judgment * (sorts_family * sorts_family * arity_error) option | CaseNotInductive of unsafe_judgment | WrongCaseInfo of inductive * case_info @@ -59,6 +59,7 @@ type type_error = | IllFormedRecBody of guard_error * name array * int | IllTypedRecBody of int * name array * unsafe_judgment array * constr array + | UnsatisfiedConstraints of Univ.constraints exception TypeError of env * type_error @@ -107,4 +108,5 @@ let error_ill_formed_rec_body env why lna i = let error_ill_typed_rec_body env i lna vdefj vargs = raise (TypeError (env, IllTypedRecBody (i,lna,vdefj,vargs))) - +let error_unsatisfied_constraints env c = + raise (TypeError (env, UnsatisfiedConstraints c)) diff --git a/checker/type_errors.mli b/checker/type_errors.mli index bcd4360b3..24086f16f 100644 --- a/checker/type_errors.mli +++ b/checker/type_errors.mli @@ -47,7 +47,7 @@ type type_error = | NotAType of unsafe_judgment | BadAssumption of unsafe_judgment | ReferenceVariables of constr - | ElimArity of inductive * sorts_family list * constr * unsafe_judgment + | ElimArity of pinductive * sorts_family list * constr * unsafe_judgment * (sorts_family * sorts_family * arity_error) option | CaseNotInductive of unsafe_judgment | WrongCaseInfo of inductive * case_info @@ -61,6 +61,7 @@ type type_error = | IllFormedRecBody of guard_error * name array * int | IllTypedRecBody of int * name array * unsafe_judgment array * constr array + | UnsatisfiedConstraints of Univ.constraints exception TypeError of env * type_error @@ -75,7 +76,7 @@ val error_assumption : env -> unsafe_judgment -> 'a val error_reference_variables : env -> constr -> 'a val error_elim_arity : - env -> inductive -> sorts_family list -> constr -> unsafe_judgment -> + env -> pinductive -> sorts_family list -> constr -> unsafe_judgment -> (sorts_family * sorts_family * arity_error) option -> 'a val error_case_not_inductive : env -> unsafe_judgment -> 'a @@ -99,3 +100,4 @@ val error_ill_formed_rec_body : val error_ill_typed_rec_body : env -> int -> name array -> unsafe_judgment array -> constr array -> 'a +val error_unsatisfied_constraints : env -> Univ.constraints -> 'a diff --git a/checker/typeops.ml b/checker/typeops.ml index 6a705b198..887d9dc1d 100644 --- a/checker/typeops.ml +++ b/checker/typeops.ml @@ -28,6 +28,10 @@ let conv_leq_vecti env v1 v2 = v1 v2 +let check_constraints cst env = + if Environ.check_constraints cst env then () + else error_unsatisfied_constraints env cst + (* This should be a type (a priori without intension to be an assumption) *) let type_judgment env (c,ty as j) = match whd_betadeltaiota env ty with @@ -66,23 +70,34 @@ let judge_of_relative env n = (* Type of constants *) -let type_of_constant_knowing_parameters env t paramtyps = - t - (* | PolymorphicArity (sign,ar) -> *) - (* let ctx = List.rev sign in *) - (* let ctx,s = instantiate_universes env ctx ar paramtyps in *) - (* mkArity (List.rev ctx,s) *) + +let type_of_constant_type_knowing_parameters env t paramtyps = + match t with + | RegularArity t -> t + | TemplateArity (sign,ar) -> + let ctx = List.rev sign in + let ctx,s = instantiate_universes env ctx ar paramtyps in + mkArity (List.rev ctx,s) + +let type_of_constant_knowing_parameters env cst paramtyps = + let ty, cu = constant_type env cst in + type_of_constant_type_knowing_parameters env ty paramtyps, cu let type_of_constant_type env t = - type_of_constant_knowing_parameters env t [||] + type_of_constant_type_knowing_parameters env t [||] -let judge_of_constant_knowing_parameters env cst paramstyp = - let cb = - try lookup_constant cst env +let type_of_constant env cst = + type_of_constant_knowing_parameters env cst [||] + +let judge_of_constant_knowing_parameters env (kn,u as cst) paramstyp = + let _cb = + try lookup_constant kn env with Not_found -> - failwith ("Cannot find constant: "^string_of_con cst) + failwith ("Cannot find constant: "^string_of_con kn) in - type_of_constant_knowing_parameters env cb.const_type paramstyp + let ty, cu = type_of_constant_knowing_parameters env cst paramstyp in + let () = check_constraints cu env in + ty let judge_of_constant env cst = judge_of_constant_knowing_parameters env cst [||] @@ -160,27 +175,27 @@ let judge_of_cast env (c,cj) k tj = the App case of execute; from this constraints, the expected dynamic constraints of the form u<=v are enforced *) -let judge_of_inductive_knowing_parameters env ind (paramstyp:constr array) = - let (mib,mip) = +let judge_of_inductive_knowing_parameters env (ind,u) (paramstyp:constr array) = + let specif = try lookup_mind_specif env ind with Not_found -> failwith ("Cannot find inductive: "^string_of_mind (fst ind)) in - type_of_inductive_knowing_parameters env mip paramstyp + type_of_inductive_knowing_parameters env (specif,u) paramstyp let judge_of_inductive env ind = judge_of_inductive_knowing_parameters env ind [||] (* Constructors. *) -let judge_of_constructor env c = +let judge_of_constructor env (c,u) = let ind = inductive_of_constructor c in let specif = try lookup_mind_specif env ind with Not_found -> failwith ("Cannot find inductive: "^string_of_mind (fst ind)) in - type_of_constructor c specif + type_of_constructor (c,u) specif (* Case. *) @@ -196,11 +211,24 @@ let judge_of_case env ci pj (c,cj) lfj = let indspec = try find_rectype env cj with Not_found -> error_case_not_inductive env (c,cj) in - let _ = check_case_info env (fst indspec) ci in + let _ = check_case_info env (fst (fst indspec)) ci in let (bty,rslty) = type_case_branches env indspec pj c in check_branch_types env (c,cj) (lfj,bty); rslty +(* Projection. *) + +let judge_of_projection env p c ct = + let pb = lookup_projection p env in + let (ind,u), args = + try find_rectype env ct + with Not_found -> error_case_not_inductive env (c, ct) + in + assert(eq_mind pb.proj_ind (fst ind)); + let usubst = make_inductive_subst (fst (lookup_mind_specif env ind)) u in + let ty = subst_univs_constr usubst pb.proj_type in + substl (c :: List.rev args) ty + (* Fixpoints. *) (* Checks the type of a general (co)fixpoint, i.e. without checking *) @@ -264,6 +292,10 @@ let rec execute env cstr = let jl = Array.map2 (fun c ty -> c,ty) args jl in judge_of_apply env (f,j) jl + | Proj (p, c) -> + let ct = execute env c in + judge_of_projection env p c ct + | Lambda (name,c1,c2) -> let _ = execute_type env c1 in let env1 = push_rel (name,None,c1) env in @@ -364,14 +396,14 @@ let check_kind env ar u = if snd (dest_prod env ar) = Sort(Type u) then () else failwith "not the correct sort" -(* let check_polymorphic_arity env params par = *) -(* let pl = par.poly_param_levels in *) -(* let rec check_p env pl params = *) -(* match pl, params with *) -(* Some u::pl, (na,None,ty)::params -> *) -(* check_kind env ty u; *) -(* check_p (push_rel (na,None,ty) env) pl params *) -(* | None::pl,d::params -> check_p (push_rel d env) pl params *) -(* | [], _ -> () *) -(* | _ -> failwith "check_poly: not the right number of params" in *) -(* check_p env pl (List.rev params) *) +let check_polymorphic_arity env params par = + let pl = par.template_param_levels in + let rec check_p env pl params = + match pl, params with + Some u::pl, (na,None,ty)::params -> + check_kind env ty u; + check_p (push_rel (na,None,ty) env) pl params + | None::pl,d::params -> check_p (push_rel d env) pl params + | [], _ -> () + | _ -> failwith "check_poly: not the right number of params" in + check_p env pl (List.rev params) diff --git a/checker/typeops.mli b/checker/typeops.mli index 97d79fe54..32920b02f 100644 --- a/checker/typeops.mli +++ b/checker/typeops.mli @@ -16,8 +16,8 @@ open Environ val infer : env -> constr -> constr val infer_type : env -> constr -> sorts val check_ctxt : env -> rel_context -> env -(* val check_polymorphic_arity : *) -(* env -> rel_context -> polymorphic_arity -> unit *) +val check_polymorphic_arity : + env -> rel_context -> template_arity -> unit -val type_of_constant_type : env -> constr -> constr +val type_of_constant_type : env -> constant_type -> constr diff --git a/dev/doc/changes.txt b/dev/doc/changes.txt index 2164830a7..d4e42142b 100644 --- a/dev/doc/changes.txt +++ b/dev/doc/changes.txt @@ -75,6 +75,9 @@ check_evars_are_solved explicitly to check that evars are solved. See also the corresponding commit log. +- Tactics API: new_induct -> induction; new_destruct -> destruct; + letin_pat_tac do not accept a type anymore + ========================================= = CHANGES BETWEEN COQ V8.3 AND COQ V8.4 = ========================================= diff --git a/dev/printers.mllib b/dev/printers.mllib index fb8d4c73e..5a9acb6dd 100644 --- a/dev/printers.mllib +++ b/dev/printers.mllib @@ -39,7 +39,6 @@ Explore Predicate Rtree Heap -Dnet Genarg Stateid Ephemeron @@ -121,7 +120,6 @@ Cbv Pretype_errors Evarutil Evarsolve -Term_dnet Recordops Evarconv Arguments_renaming diff --git a/doc/refman/RefMan-tacex.tex b/doc/refman/RefMan-tacex.tex index 463e2b81a..6667fd5a4 100644 --- a/doc/refman/RefMan-tacex.tex +++ b/doc/refman/RefMan-tacex.tex @@ -64,7 +64,7 @@ induction H. As the hypothesis itself did not appear in the goal, we did not need to use an heterogeneous equality to relate the new hypothesis to the old -one (which just disappeared here). However, the tactic works just a well +one (which just disappeared here). However, the tactic works just as well in this case, e.g.: \begin{coq_eval} diff --git a/kernel/constr.ml b/kernel/constr.ml index f72eb2acb..c6eacc289 100644 --- a/kernel/constr.ml +++ b/kernel/constr.ml @@ -556,7 +556,7 @@ let eq_constr_univs univs m n = if m == n then true else let eq_universes _ = Univ.Instance.check_eq univs in - let eq_sorts s1 s2 = Univ.check_eq univs (Sorts.univ_of_sort s1) (Sorts.univ_of_sort s2) in + let eq_sorts s1 s2 = s1 == s2 || Univ.check_eq univs (Sorts.univ_of_sort s1) (Sorts.univ_of_sort s2) in let rec eq_constr' m n = m == n || compare_head_gen eq_universes eq_sorts eq_constr' m n in compare_head_gen eq_universes eq_sorts eq_constr' m n @@ -565,8 +565,10 @@ let leq_constr_univs univs m n = if m == n then true else let eq_universes _ = Univ.Instance.check_eq univs in - let eq_sorts s1 s2 = Univ.check_eq univs (Sorts.univ_of_sort s1) (Sorts.univ_of_sort s2) in - let leq_sorts s1 s2 = Univ.check_leq univs (Sorts.univ_of_sort s1) (Sorts.univ_of_sort s2) in + let eq_sorts s1 s2 = s1 == s2 || + Univ.check_eq univs (Sorts.univ_of_sort s1) (Sorts.univ_of_sort s2) in + let leq_sorts s1 s2 = s1 == s2 || + Univ.check_leq univs (Sorts.univ_of_sort s1) (Sorts.univ_of_sort s2) in let rec eq_constr' m n = m == n || compare_head_gen eq_universes eq_sorts eq_constr' m n in @@ -582,9 +584,11 @@ let eq_constr_universes m n = let eq_universes strict l l' = cstrs := Univ.enforce_eq_instances_univs strict l l' !cstrs; true in let eq_sorts s1 s2 = - cstrs := Univ.UniverseConstraints.add - (Sorts.univ_of_sort s1, Univ.UEq, Sorts.univ_of_sort s2) !cstrs; - true + if Sorts.equal s1 s2 then true + else + (cstrs := Univ.UniverseConstraints.add + (Sorts.univ_of_sort s1, Univ.UEq, Sorts.univ_of_sort s2) !cstrs; + true) in let rec eq_constr' m n = m == n || compare_head_gen eq_universes eq_sorts eq_constr' m n @@ -599,12 +603,17 @@ let leq_constr_universes m n = let eq_universes strict l l' = cstrs := Univ.enforce_eq_instances_univs strict l l' !cstrs; true in let eq_sorts s1 s2 = - cstrs := Univ.UniverseConstraints.add - (Sorts.univ_of_sort s1,Univ.UEq,Sorts.univ_of_sort s2) !cstrs; true + if Sorts.equal s1 s2 then true + else (cstrs := Univ.UniverseConstraints.add + (Sorts.univ_of_sort s1,Univ.UEq,Sorts.univ_of_sort s2) !cstrs; + true) in let leq_sorts s1 s2 = - cstrs := Univ.UniverseConstraints.add - (Sorts.univ_of_sort s1,Univ.ULe,Sorts.univ_of_sort s2) !cstrs; true + if Sorts.equal s1 s2 then true + else + (cstrs := Univ.UniverseConstraints.add + (Sorts.univ_of_sort s1,Univ.ULe,Sorts.univ_of_sort s2) !cstrs; + true) in let rec eq_constr' m n = m == n || compare_head_gen eq_universes eq_sorts eq_constr' m n diff --git a/kernel/declarations.mli b/kernel/declarations.mli index b8dfe63d3..85dac4bfc 100644 --- a/kernel/declarations.mli +++ b/kernel/declarations.mli @@ -27,7 +27,7 @@ type engagement = ImpredicativeSet *) type template_arity = { - template_param_levels : Univ.universe option list; + template_param_levels : Univ.universe_level option list; template_level : Univ.universe; } diff --git a/kernel/declareops.ml b/kernel/declareops.ml index 55868097f..dd906bab2 100644 --- a/kernel/declareops.ml +++ b/kernel/declareops.ml @@ -31,8 +31,8 @@ let map_decl_arity f g = function | TemplateArity a -> TemplateArity (g a) let hcons_template_arity ar = - { template_param_levels = - List.smartmap (Option.smartmap Univ.hcons_univ) ar.template_param_levels; + { template_param_levels = ar.template_param_levels; + (* List.smartmap (Option.smartmap Univ.hcons_univ_level) ar.template_param_levels; *) template_level = Univ.hcons_univ ar.template_level } (** {6 Constants } *) diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index 0f9c7421f..85d04e5e2 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -195,11 +195,11 @@ let is_impredicative env u = let param_ccls params = let has_some_univ u = function - | Some v when Universe.equal u v -> true + | Some v when Univ.Level.equal u v -> true | _ -> false in let remove_some_univ u = function - | Some v when Universe.equal u v -> None + | Some v when Univ.Level.equal u v -> None | x -> x in let fold l (_, b, p) = match b with @@ -210,10 +210,13 @@ let param_ccls params = (* polymorphism unless there is aliasing (i.e. non distinct levels) *) begin match kind_of_term c with | Sort (Type u) -> - if List.exists (has_some_univ u) l then - None :: List.map (remove_some_univ u) l - else - Some u :: l + (match Univ.Universe.level u with + | Some u -> + if List.exists (has_some_univ u) l then + None :: List.map (remove_some_univ u) l + else + Some u :: l + | None -> None :: l) | _ -> None :: l end diff --git a/kernel/inductive.ml b/kernel/inductive.ml index 7cf5dd62d..3f1c4e75f 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -155,10 +155,7 @@ let sort_as_univ = function (* Template polymorphism *) let cons_subst u su subst = - try - (u, sup su (List.assoc_f Universe.equal u subst)) :: - List.remove_assoc_f Universe.equal u subst - with Not_found -> (u, su) :: subst + Univ.LMap.add u su subst let actualize_decl_level env lev t = let sign,s = dest_arity env t in @@ -192,7 +189,7 @@ let rec make_subst env = function d::ctx, subst | sign, [], _ -> (* Uniform parameters are exhausted *) - sign,[] + sign, Univ.LMap.empty | [], _, _ -> assert false @@ -201,7 +198,7 @@ exception SingletonInductiveBecomesProp of Id.t let instantiate_universes env ctx ar argsorts = let args = Array.to_list argsorts in let ctx,subst = make_subst env (ctx,ar.template_param_levels,args) in - let level = subst_large_constraints subst ar.template_level in + let level = Univ.subst_univs_universe (Univ.make_subst subst) ar.template_level in let ty = (* Singleton type not containing types are interpretable in Prop *) if is_type0m_univ level then prop_sort @@ -214,11 +211,13 @@ let instantiate_universes env ctx ar argsorts = (* Type of an inductive type *) -let type_of_inductive_gen ?(polyprop=true) env ((mib,mip),u) paramtyps = +let type_of_inductive_subst ?(polyprop=true) env ((mib,mip),u) paramtyps = match mip.mind_arity with | RegularArity a -> - let subst = make_inductive_subst mib u in - (subst_univs_constr subst a.mind_user_arity, subst) + if not mib.mind_polymorphic then (a.mind_user_arity, Univ.LMap.empty) + else + let subst = make_inductive_subst mib u in + (subst_univs_constr subst a.mind_user_arity, subst) | TemplateArity ar -> let ctx = List.rev mip.mind_arity_ctxt in let ctx,s = instantiate_universes env ctx ar paramtyps in @@ -229,21 +228,38 @@ let type_of_inductive_gen ?(polyprop=true) env ((mib,mip),u) paramtyps = then raise (SingletonInductiveBecomesProp mip.mind_typename); mkArity (List.rev ctx,s), Univ.LMap.empty +let type_of_inductive_gen ?(polyprop=true) env ((mib,mip),u) paramtyps = + match mip.mind_arity with + | RegularArity a -> + if not mib.mind_polymorphic then a.mind_user_arity + else + let subst = make_inductive_subst mib u in + (subst_univs_constr subst a.mind_user_arity) + | TemplateArity ar -> + let ctx = List.rev mip.mind_arity_ctxt in + let ctx,s = instantiate_universes env ctx ar paramtyps in + (* The Ocaml extraction cannot handle (yet?) "Prop-polymorphism", i.e. + the situation where a non-Prop singleton inductive becomes Prop + when applied to Prop params *) + if not polyprop && not (is_type0m_univ ar.template_level) && is_prop_sort s + then raise (SingletonInductiveBecomesProp mip.mind_typename); + mkArity (List.rev ctx,s) + let type_of_inductive env pind = - fst (type_of_inductive_gen env pind [||]) + type_of_inductive_gen env pind [||] let constrained_type_of_inductive env ((mib,mip),u as pind) = - let ty, subst = type_of_inductive_gen env pind [||] in + let ty, subst = type_of_inductive_subst env pind [||] in let cst = instantiate_inductive_constraints mib subst in (ty, cst) let constrained_type_of_inductive_knowing_parameters env ((mib,mip),u as pind) args = - let ty, subst = type_of_inductive_gen env pind args in + let ty, subst = type_of_inductive_subst env pind args in let cst = instantiate_inductive_constraints mib subst in (ty, cst) let type_of_inductive_knowing_parameters env ?(polyprop=false) mip args = - fst (type_of_inductive_gen env mip args) + type_of_inductive_gen env mip args (* The max of an array of universes *) diff --git a/kernel/typeops.ml b/kernel/typeops.ml index c6355b3ea..49f883628 100644 --- a/kernel/typeops.ml +++ b/kernel/typeops.ml @@ -115,7 +115,7 @@ let check_hyps_inclusion env c sign = let extract_level env p = let _,c = dest_prod_assum env p in - match kind_of_term c with Sort (Type u) -> Some u | _ -> None + match kind_of_term c with Sort (Type u) -> Univ.Universe.level u | _ -> None let extract_context_levels env l = let fold l (_, b, p) = match b with diff --git a/lib/lib.mllib b/lib/lib.mllib index edef3da03..b5421a8c8 100644 --- a/lib/lib.mllib +++ b/lib/lib.mllib @@ -16,7 +16,6 @@ Explore Predicate Rtree Heap -Dnet Unionfind Genarg Ephemeron diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml index 0ddc7c006..cce6aff28 100644 --- a/plugins/extraction/extraction.ml +++ b/plugins/extraction/extraction.ml @@ -207,7 +207,7 @@ let oib_equal o1 o2 = | RegularArity {mind_user_arity=c1; mind_sort=s1}, RegularArity {mind_user_arity=c2; mind_sort=s2} -> eq_constr c1 c2 && Sorts.equal s1 s2 | TemplateArity p1, TemplateArity p2 -> - let eq o1 o2 = Option.equal Univ.Universe.equal o1 o2 in + let eq o1 o2 = Option.equal Univ.Level.equal o1 o2 in List.equal eq p1.template_param_levels p2.template_param_levels && Univ.Universe.equal p1.template_level p2.template_level | _, _ -> false diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index 3f728ddcd..70a892a3b 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -26,8 +26,8 @@ let is_rec_info scheme_info = let choose_dest_or_ind scheme_info = if is_rec_info scheme_info - then Tactics.new_induct false - else Tactics.new_destruct false + then Tactics.induction false + else Tactics.destruct false let functional_induction with_clean c princl pat = Dumpglob.pause (); diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index a92698566..6bf621b05 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -889,10 +889,14 @@ let second_order_matching ts env_rhs evd (evk,args) argoccs rhs = in force_instantiation evd !evsref | [] -> - Evd.define evk rhs evd in - + let evd = + try Evarsolve.check_evar_instance evd evk rhs (evar_conv_x ts) + with IllTypedInstance _ -> raise (TypingFailed evd) + in + Evd.define evk rhs evd + in abstract_free_holes evd subst, true - with TypingFailed evd -> Evd.define evk rhs evd, false + with TypingFailed evd -> evd, false let second_order_matching_with_args ts env evd ev l t = (* diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml index 128a7e55c..18c91c0e3 100644 --- a/pretyping/evarutil.ml +++ b/pretyping/evarutil.ml @@ -139,10 +139,9 @@ let has_undefined_evars or_sorts evd t = has_ev c; Array.iter has_ev args | Evar_empty -> raise NotInstantiatedEvar) - | Sort (Type _) (*FIXME could be finer, excluding Prop and Set universes *) when or_sorts -> - raise Not_found | Ind (_,l) | Const (_,l) | Construct (_,l) - when or_sorts && not (Univ.Instance.is_empty l) (* has_flexible_level evd l *) -> raise Not_found + when or_sorts && not (Univ.Instance.is_empty l) -> + raise Not_found | _ -> iter_constr has_ev t in try let _ = has_ev t in false with (Not_found | NotInstantiatedEvar) -> true @@ -831,7 +830,7 @@ let get_template_constructor_type evdref (ind, i) n = | Some u :: l, Prod (na, t, t') -> let u' = evd_comb0 (new_univ_variable Evd.univ_flexible) evdref in (* evdref := set_leq_sort !evdref u'l (Type u); *) - let s = Univ.LMap.add (Option.get (Univ.Universe.level u)) + let s = Univ.LMap.add u (Option.get (Univ.Universe.level u')) Univ.LMap.empty in let dom = subst_univs_level_constr s t in (* let codom = subst_univs_level_constr s t' in *) diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli index 7715691b0..aa302bac6 100644 --- a/pretyping/evarutil.mli +++ b/pretyping/evarutil.mli @@ -221,7 +221,7 @@ val evd_comb2 : (evar_map -> 'b -> 'c -> evar_map * 'a) -> evar_map ref -> 'b -> (* val get_template_constructor_type : evar_map ref -> constructor -> int -> types *) val get_template_constructor_type : evar_map ref -> constructor -> int -> - (Univ.universe option list * types) + (Univ.universe_level option list * types) val get_template_inductive_type : evar_map ref -> inductive -> int -> - (Univ.universe option list * types) + (Univ.universe_level option list * types) diff --git a/pretyping/evd.ml b/pretyping/evd.ml index 5a9281c89..1f462197c 100644 --- a/pretyping/evd.ml +++ b/pretyping/evd.ml @@ -743,6 +743,9 @@ let evars_reset_evd ?(with_conv_pbs=false) ?(with_univs=true) evd d = let merge_universe_context evd uctx' = { evd with universes = union_evar_universe_context evd.universes uctx' } +let set_universe_context evd uctx' = + { evd with universes = uctx' } + let add_conv_pb pb d = {d with conv_pbs = pb::d.conv_pbs} let evar_source evk d = (find d evk).evar_source diff --git a/pretyping/evd.mli b/pretyping/evd.mli index 49a91f524..a360351b7 100644 --- a/pretyping/evd.mli +++ b/pretyping/evd.mli @@ -468,6 +468,7 @@ val universes : evar_map -> Univ.universes val merge_universe_context : evar_map -> evar_universe_context -> evar_map +val set_universe_context : evar_map -> evar_universe_context -> evar_map val merge_context_set : rigid -> evar_map -> Univ.universe_context_set -> evar_map val merge_universe_subst : evar_map -> Universes.universe_opt_subst -> evar_map diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml index 0b7cd89f2..e180c1346 100644 --- a/pretyping/inductiveops.ml +++ b/pretyping/inductiveops.ml @@ -465,7 +465,7 @@ let rec instantiate_universes env evdref scl is = function let s = (* Does the sort of parameter [u] appear in (or equal) the sort of inductive [is] ? *) - if univ_depends u is then + if univ_depends (Univ.Universe.make u) is then scl (* constrained sort: replace by scl *) else (* unconstriained sort: replace by fresh universe *) diff --git a/pretyping/pretyping.mllib b/pretyping/pretyping.mllib index 469be6d9e..a4c72f482 100644 --- a/pretyping/pretyping.mllib +++ b/pretyping/pretyping.mllib @@ -11,7 +11,6 @@ Cbv Pretype_errors Evarutil Evarsolve -Term_dnet Recordops Evarconv Arguments_renaming diff --git a/pretyping/unification.ml b/pretyping/unification.ml index b1b2bc05b..7b6fb262a 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -92,8 +92,11 @@ let abstract_list_all_with_dependencies env evd typ c l = let evd,b = Evarconv.second_order_matching empty_transparent_state env evd ev' argoccs c in - let p = nf_evar evd (existential_value evd (destEvar ev)) in - if b then evd, p else error_cannot_find_well_typed_abstraction env evd p l None + if b then + let p = nf_evar evd (existential_value evd (destEvar ev)) in + evd, p + else error_cannot_find_well_typed_abstraction env evd + (nf_evar evd c) l None (**) @@ -419,17 +422,18 @@ let isAllowedEvar flags c = match kind_of_term c with | Evar (evk,_) -> not (Evar.Set.mem evk flags.frozen_evars) | _ -> false -let check_compatibility env flags (sigma,metasubst,evarsubst) tyM tyN = +let check_compatibility env pbty flags (sigma,metasubst,evarsubst) tyM tyN = match subst_defined_metas metasubst tyM with - | None -> () + | None -> sigma | Some m -> match subst_defined_metas metasubst tyN with - | None -> () + | None -> sigma | Some n -> - if not (is_trans_fconv CONV flags.modulo_delta env sigma m n) - && is_ground_term sigma m && is_ground_term sigma n - then - error_cannot_unify env sigma (m,n) + if is_ground_term sigma m && is_ground_term sigma n then + let sigma, b = infer_conv ~pb:pbty ~ts:flags.modulo_delta env sigma m n in + if b then sigma + else error_cannot_unify env sigma (m,n) + else sigma let unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb flags m n = let rec unirec_rec (curenv,nb as curenvnb) pb b wt ((sigma,metasubst,evarsubst) as substn) curm curn = @@ -439,21 +443,28 @@ let unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb flag | Meta k1, Meta k2 -> if Int.equal k1 k2 then substn else let stM,stN = extract_instance_status pb in - if wt && flags.check_applied_meta_types then - (let tyM = Typing.meta_type sigma k1 in - let tyN = Typing.meta_type sigma k2 in - check_compatibility curenv flags substn tyM tyN); + let sigma = + if wt && flags.check_applied_meta_types then + let tyM = Typing.meta_type sigma k1 in + let tyN = Typing.meta_type sigma k2 in + let l, r = if k2 < k1 then tyN, tyM else tyM, tyN in + check_compatibility curenv CUMUL flags substn l r + else sigma + in if k2 < k1 then sigma,(k1,cN,stN)::metasubst,evarsubst else sigma,(k2,cM,stM)::metasubst,evarsubst | Meta k, _ when not (dependent cM cN) (* helps early trying alternatives *) -> - if wt && flags.check_applied_meta_types then - (try - let tyM = Typing.meta_type sigma k in - let tyN = get_type_of curenv ~lax:true sigma cN in - check_compatibility curenv flags substn tyM tyN - with RetypeError _ -> - (* Renounce, maybe metas/evars prevents typing *) ()); + let sigma = + if wt && flags.check_applied_meta_types then + (try + let tyM = Typing.meta_type sigma k in + let tyN = get_type_of curenv ~lax:true sigma cN in + check_compatibility curenv CUMUL flags substn tyN tyM + with RetypeError _ -> + (* Renounce, maybe metas/evars prevents typing *) sigma) + else sigma + in (* Here we check that [cN] does not contain any local variables *) if Int.equal nb 0 then sigma,(k,cN,snd (extract_instance_status pb))::metasubst,evarsubst @@ -464,13 +475,16 @@ let unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb flag else error_cannot_unify_local curenv sigma (m,n,cN) | _, Meta k when not (dependent cN cM) (* helps early trying alternatives *) -> - if wt && flags.check_applied_meta_types then + let sigma = + if wt && flags.check_applied_meta_types then (try let tyM = get_type_of curenv ~lax:true sigma cM in let tyN = Typing.meta_type sigma k in - check_compatibility curenv flags substn tyM tyN + check_compatibility curenv CUMUL flags substn tyM tyN with RetypeError _ -> - (* Renounce, maybe metas/evars prevents typing *) ()); + (* Renounce, maybe metas/evars prevents typing *) sigma) + else sigma + in (* Here we check that [cM] does not contain any local variables *) if Int.equal nb 0 then (sigma,(k,cM,fst (extract_instance_status pb))::metasubst,evarsubst) @@ -641,7 +655,7 @@ let unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb flag | None -> (* some undefined Metas in cN *) None | Some n1 -> (* No subterm restriction there, too much incompatibilities *) - let b = check_conv ~pb ~ts:convflags env sigma m1 n1 in + let sigma, b = infer_conv ~pb ~ts:convflags env sigma m1 n1 in if b then Some (sigma, metasubst, evarsubst) else if is_ground_term sigma m1 && is_ground_term sigma n1 then diff --git a/proofs/proofview.ml b/proofs/proofview.ml index 83a703a3a..6651e4965 100644 --- a/proofs/proofview.ml +++ b/proofs/proofview.ml @@ -682,6 +682,9 @@ module V82 = struct let tclEVARS evd = Proof.modify (fun ps -> { ps with solution = evd }) + let tclEVARUNIVCONTEXT ctx = + Proof.modify (fun ps -> { ps with solution = Evd.set_universe_context ps.solution ctx }) + let has_unresolved_evar pv = Evd.has_undefined pv.solution diff --git a/proofs/proofview.mli b/proofs/proofview.mli index dddf9b1c2..6177803c7 100644 --- a/proofs/proofview.mli +++ b/proofs/proofview.mli @@ -298,6 +298,9 @@ module V82 : sig val tclEVARS : Evd.evar_map -> unit tactic + (* Set the evar universe context *) + val tclEVARUNIVCONTEXT : Evd.evar_universe_context -> unit tactic + val has_unresolved_evar : proofview -> bool (* Main function in the implementation of Grab Existential Variables. diff --git a/proofs/refiner.ml b/proofs/refiner.ml index da9e8c68d..157faae3d 100644 --- a/proofs/refiner.ml +++ b/proofs/refiner.ml @@ -325,6 +325,8 @@ let rec tclREPEAT_MAIN t g = (* Change evars *) let tclEVARS sigma gls = tclIDTAC {gls with sigma=sigma} +let tclEVARUNIVCONTEXT ctx gls = tclIDTAC {gls with sigma= Evd.set_universe_context gls.sigma ctx} + (* Push universe context *) let tclPUSHCONTEXT rigid ctx tac gl = tclTHEN (tclEVARS (Evd.merge_context_set rigid (project gl) ctx)) tac gl diff --git a/proofs/refiner.mli b/proofs/refiner.mli index 25ab1fb76..a74d8a46d 100644 --- a/proofs/refiner.mli +++ b/proofs/refiner.mli @@ -33,6 +33,7 @@ val tclIDTAC_MESSAGE : Pp.std_ppcmds -> tactic (** [tclEVARS sigma] changes the current evar map *) val tclEVARS : evar_map -> tactic +val tclEVARUNIVCONTEXT : Evd.evar_universe_context -> tactic val tclPUSHCONTEXT : Evd.rigid -> Univ.universe_context_set -> tactic -> tactic val tclPUSHEVARUNIVCONTEXT : Evd.evar_universe_context -> tactic diff --git a/lib/dnet.ml b/tactics/dnet.ml index 22ca7e78d..22ca7e78d 100644 --- a/lib/dnet.ml +++ b/tactics/dnet.ml diff --git a/lib/dnet.mli b/tactics/dnet.mli index d2373a0d6..d2373a0d6 100644 --- a/lib/dnet.mli +++ b/tactics/dnet.mli diff --git a/tactics/equality.ml b/tactics/equality.ml index 6e4f46c67..5b73fbea2 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -1357,7 +1357,13 @@ let dEqThen with_evars ntac = function let dEq with_evars = dEqThen with_evars (fun c x -> Proofview.tclUNIT ()) -let _ = declare_intro_decomp_eq (fun tac -> decompEqThen (fun _ -> tac)) +let intro_decompe_eq tac data cl = + Proofview.Goal.raw_enter begin fun gl -> + let cl = pf_apply make_clenv_binding gl cl NoBindings in + decompEqThen (fun _ -> tac) data cl + end + +let _ = declare_intro_decomp_eq intro_decompe_eq let swap_equality_args = function | MonomorphicLeibnizEq (e1,e2) -> [e2;e1] @@ -1612,35 +1618,24 @@ let subst_one dep_proof_ok x (hyp,rhs,dir) = let hyps = Proofview.Goal.hyps gl in let concl = Proofview.Goal.concl gl in (* The set of hypotheses using x *) - let depdecls = - let test (id,_,c as dcl) = - if not (Id.equal id hyp) && occur_var_in_decl env x dcl then Some dcl - else None in - List.rev (List.map_filter test hyps) in - let dephyps = List.map (fun (id,_,_) -> id) depdecls in + let dephyps = + List.rev (snd (List.fold_right (fun (id,b,_ as dcl) (deps,allhyps) -> + if not (Id.equal id hyp) + && List.exists (fun y -> occur_var_in_decl env y dcl) deps + then + ((if b = None then deps else id::deps), id::allhyps) + else + (deps,allhyps)) + hyps + ([x],[]))) in (* Decides if x appears in conclusion *) let depconcl = occur_var env x concl in - (* The set of non-defined hypothesis: they must be abstracted, - rewritten and reintroduced *) - let abshyps = - List.map_filter (function (id, None, _) -> Some (mkVar id) | _ -> None) - depdecls in - (* a tactic that either introduce an abstracted and rewritten hyp, - or introduce a definition where x was replaced *) - let introtac = function - (id,None,_) -> intro_using id - | (id,Some hval,htyp) -> - letin_tac None (Name id) - (replace_term (mkVar x) rhs hval) - (Some (replace_term (mkVar x) rhs htyp)) nowhere - in let need_rewrite = not (List.is_empty dephyps) || depconcl in tclTHENLIST ((if need_rewrite then - [Proofview.V82.tactic (generalize abshyps); + [Proofview.V82.tactic (revert dephyps); general_rewrite dir AllOccurrences true dep_proof_ok (mkVar hyp); - Proofview.V82.tactic (thin dephyps); - (tclMAP introtac depdecls)] + (tclMAP intro_using dephyps)] else [Proofview.tclUNIT ()]) @ [tclTRY (clear [x; hyp])]) diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index a4d840cf0..0d2b3d5a1 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -543,6 +543,13 @@ let pf_interp_casted_constr ist gl c = let pf_interp_constr ist gl = interp_constr ist (pf_env gl) (project gl) +let new_interp_constr ist c k = + let open Proofview in + Proofview.Goal.raw_enter begin fun gl -> + let (sigma, c) = interp_constr ist (Goal.env gl) (Goal.sigma gl) c in + Proofview.tclTHEN (Proofview.V82.tclEVARS sigma) (k c) + end + let interp_constr_in_compound_list inj_fun dest_fun interp_fun ist env sigma l = let try_expand_ltac_var sigma x = try match dest_fun x with @@ -591,12 +598,9 @@ let interp_constr_with_occurrences ist sigma env (occs,c) = let (sigma,c_interp) = interp_constr ist sigma env c in sigma , (interp_occurrences ist occs, c_interp) -let interp_typed_pattern_with_occurrences ist env sigma (occs,c) = - let sign,p = interp_typed_pattern ist env sigma c in - sign, (interp_occurrences ist occs, p) - -let interp_closed_typed_pattern_with_occurrences ist env sigma occl = - snd (interp_typed_pattern_with_occurrences ist env sigma occl) +let interp_closed_typed_pattern_with_occurrences ist env sigma (occs, c) = + let _, p = interp_typed_pattern ist env sigma c in + interp_occurrences ist occs, p let interp_constr_with_occurrences_and_name_as_list = interp_constr_in_compound_list @@ -1453,21 +1457,11 @@ and interp_atomic ist tac = gl end | TacExactNoCheck c -> - Proofview.V82.tactic begin fun gl -> - let (sigma,c_interp) = pf_interp_constr ist gl c in - tclTHEN - (tclEVARS sigma) - (Tactics.exact_no_check c_interp) - gl - end + (new_interp_constr ist c) + (fun c -> Proofview.V82.tactic (Tactics.exact_no_check c)) | TacVmCastNoCheck c -> - Proofview.V82.tactic begin fun gl -> - let (sigma,c_interp) = pf_interp_constr ist gl c in - tclTHEN - (tclEVARS sigma) - (Tactics.vm_cast_no_check c_interp) - gl - end + (new_interp_constr ist c) + (fun c -> Proofview.V82.tactic (Tactics.vm_cast_no_check c)) | TacApply (a,ev,cb,cl) -> Proofview.Goal.raw_enter begin fun gl -> let env = Proofview.Goal.env gl in @@ -1578,13 +1572,8 @@ and interp_atomic ist tac = tclWITHHOLES false (Tactics.Simple.generalize_gen) sigma cl gl end | TacGeneralizeDep c -> - Proofview.V82.tactic begin fun gl -> - let (sigma,c_interp) = pf_interp_constr ist gl c in - tclTHEN - (tclEVARS sigma) - (Tactics.generalize_dep c_interp) - gl - end + (new_interp_constr ist c) + (fun c -> Proofview.V82.tactic (Tactics.generalize_dep c)) | TacLetTac (na,c,clp,b,eqpat) -> Proofview.V82.nf_evar_goals <*> Proofview.Goal.enter begin fun gl -> @@ -1610,7 +1599,7 @@ and interp_atomic ist tac = let let_pat_tac b na c cl eqpat = let id = Option.default (Loc.ghost,IntroAnonymous) eqpat in let with_eq = if b then None else Some (true,id) in - Tactics.letin_pat_tac with_eq na c None cl + Tactics.letin_pat_tac with_eq na c cl in let_pat_tac b (interp_fresh_name ist env na) (interp_pure_open_constr ist env sigma c) clp eqpat @@ -1665,26 +1654,13 @@ and interp_atomic ist tac = let h2 = interp_quantified_hypothesis ist h2 in Elim.h_double_induction h1 h2 | TacDecomposeAnd c -> - Proofview.Goal.enter begin fun gl -> - let (sigma,c_interp) = Tacmach.New.of_old (fun gl -> pf_interp_constr ist gl c) gl in - Tacticals.New.tclTHEN - (Proofview.V82.tclEVARS sigma) - (Elim.h_decompose_and c_interp) - end + new_interp_constr ist c Elim.h_decompose_and | TacDecomposeOr c -> - Proofview.Goal.enter begin fun gl -> - let (sigma,c_interp) = Tacmach.New.of_old (fun gl -> pf_interp_constr ist gl c) gl in - Tacticals.New.tclTHEN - (Proofview.V82.tclEVARS sigma) - (Elim.h_decompose_or c_interp) - end + new_interp_constr ist c Elim.h_decompose_or | TacDecompose (l,c) -> - Proofview.Goal.enter begin fun gl -> - let l = List.map (interp_inductive ist) l in - let (sigma,c_interp) = Tacmach.New.of_old (fun gl -> pf_interp_constr ist gl c) gl in - Tacticals.New.tclTHEN - (Proofview.V82.tclEVARS sigma) - (Elim.h_decompose l c_interp) + (new_interp_constr ist c) begin fun c -> + let l = List.map (interp_inductive ist) l in + Elim.h_decompose l c end | TacSpecialize (n,cb) -> Proofview.Goal.raw_enter begin fun gl -> @@ -1696,12 +1672,7 @@ and interp_atomic ist tac = end end | TacLApply c -> - Proofview.Goal.enter begin fun gl -> - let (sigma,c_interp) = Tacmach.New.of_old (pf_interp_constr ist) gl c in - Tacticals.New.tclTHEN - (Proofview.V82.tclEVARS sigma) - (Tactics.cut_and_apply c_interp) - end + new_interp_constr ist c Tactics.cut_and_apply (* Context management *) | TacClear (b,l) -> @@ -1833,14 +1804,7 @@ and interp_atomic ist tac = begin match c with | None -> Tactics.intros_transitivity None | Some c -> - Proofview.Goal.enter begin fun gl -> - let (sigma,c_interp) = - Tacmach.New.of_old (fun gl -> pf_interp_constr ist gl c) gl - in - Tacticals.New.tclTHEN - (Proofview.V82.tclEVARS sigma) - (Tactics.intros_transitivity (Some c_interp)) - end + (new_interp_constr ist c) (fun c -> Tactics.intros_transitivity (Some c)) end (* Equality and inversion *) diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 0a3141e0a..78d215ac8 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -324,7 +324,7 @@ let tclWITHEVARS f k gl = tclTHEN (tclEVARS evm) (k c') gl let e_reduct_in_concl (redfun,sty) gl = - tclWITHEVARS + tclWITHEVARS (fun env sigma -> redfun env sigma (pf_concl gl)) (fun c -> convert_concl_no_check c sty) gl @@ -339,7 +339,7 @@ let e_pf_reduce_decl (redfun : e_reduction_function) where (id,c,ty) env sigma = let sigma',b' = if where != InHypTypeOnly then redfun env sigma b else sigma, b in let sigma',ty' = if where != InHypValueOnly then redfun env sigma ty else sigma', ty in sigma', (id,Some b',ty') - + let e_reduct_in_hyp redfun (id,where) gl = tclWITHEVARS (e_pf_reduce_decl redfun where (pf_get_hyp gl id)) @@ -695,27 +695,6 @@ let map_induction_arg f = function | ElimOnIdent id -> ElimOnIdent id (**************************) -(* Refinement tactics *) -(**************************) - -let apply_type hdcty argl gl = - refine (applist (mkCast (Evarutil.mk_new_meta(),DEFAULTcast, hdcty),argl)) gl - -let bring_hyps hyps = - if List.is_empty hyps then Tacticals.New.tclIDTAC - else - Proofview.Goal.raw_enter begin fun gl -> - let env = Proofview.Goal.env gl in - let concl = Tacmach.New.pf_nf_concl gl in - let newcl = List.fold_right mkNamedProd_or_LetIn hyps concl in - let args = Array.of_list (instance_from_named_context hyps) in - Proofview.Refine.refine begin fun h -> - let (h, ev) = Proofview.Refine.new_evar h env newcl in - (h, (mkApp (ev, args))) - end - end - -(**************************) (* Cut tactics *) (**************************) @@ -753,13 +732,13 @@ let cut_intro t = Tacticals.New.tclTHENFIRST (cut t) intro (* [assert_replacing id T tac] adds the subgoals of the proof of [T] before the current goal - id:T0 id:T0 id:T - ===== ------> tac(=====) + ==== + id:T0 id:T0 id:T + ===== ------> tac(=====) + ==== G T G It fails if the hypothesis to replace appears in the goal or in another hypothesis. -*) +*) let assert_replacing id t tac = tclTHENFIRST (internal_cut_replace id t) tac @@ -829,7 +808,8 @@ let index_of_ind_arg t = | None -> error "Could not find inductive argument of elimination scheme." in aux None 0 t -let elimination_clause_scheme with_evars ?(flags=elim_flags ()) i elimclause indclause gl = +let elimination_clause_scheme with_evars ?(flags=elim_flags ()) i (elim, elimty, bindings) indclause gl = + let elimclause = make_clenv_binding (pf_env gl) (project gl) (elim, elimty) bindings in let indmv = (match kind_of_term (nth_arg i elimclause.templval.rebus) with | Meta mv -> mv @@ -857,14 +837,13 @@ let general_elim_clause_gen elimtac indclause elim gl = let elimt = pf_type_of gl elimc in let i = match elim.elimindex with None -> index_of_ind_arg elimt | Some i -> i in - let elimclause = pf_apply make_clenv_binding gl (elimc,elimt) lbindelimc in - elimtac i elimclause indclause gl + elimtac i (elimc, elimt, lbindelimc) indclause gl let general_elim_clause elimtac (c,lbindc) elim gl = let ct = pf_type_of gl c in let t = try snd (pf_reduce_to_quantified_ind gl ct) with UserError _ -> ct in - let indclause = pf_apply make_clenv_binding gl (c,t) lbindc in - general_elim_clause_gen elimtac indclause elim gl + let indclause = pf_apply make_clenv_binding gl (c, t) lbindc in + general_elim_clause_gen elimtac indclause elim gl let general_elim with_evars c e = general_elim_clause (elimination_clause_scheme with_evars) c e @@ -959,7 +938,8 @@ let clenv_fchain_in id ?(flags=elim_flags ()) mv elimclause hypclause = (* Set the hypothesis name in the message *) raise (PretypeError (env,evd,NoOccurrenceFound (op,Some id))) -let elimination_in_clause_scheme with_evars ?(flags=elim_flags ()) id i elimclause indclause gl = +let elimination_in_clause_scheme with_evars ?(flags=elim_flags ()) id i (elim, elimty, bindings) indclause gl = + let elimclause = make_clenv_binding (pf_env gl) (project gl) (elim, elimty) bindings in let indmv = destMeta (nth_arg i elimclause.templval.rebus) in let hypmv = try match List.remove Int.equal indmv (clenv_independent elimclause) with @@ -1008,10 +988,10 @@ let make_projection env sigma params cstr sign elim i n c u = match List.nth l i with | Some proj -> let args = extended_rel_vect 0 sign in - let proj = + let proj = if Environ.is_projection proj env then - mkProj (proj, mkApp (c, args)) - else + mkProj (proj, mkApp (c, args)) + else mkApp (mkConstU (proj,u), Array.append (Array.of_list params) [|mkApp (c, args)|]) in @@ -1042,7 +1022,7 @@ let descend_in_conjunctions tac exit c gl = (List.init n (fun i gl -> match pf_apply make_projection gl params cstr sign elim i n c u with | None -> tclFAIL 0 (mt()) gl - | Some (p,pt) -> + | Some (p,pt) -> tclTHENS (internal_cut id pt) [refine p; (* Might be ill-typed due to forbidden elimination. *) @@ -1226,7 +1206,7 @@ let vm_cast_no_check c gl = let exact_proof c gl = let c,ctx = Constrintern.interp_casted_constr (project gl) (pf_env gl) c (pf_concl gl) - in tclTHEN (tclPUSHEVARUNIVCONTEXT ctx) (refine_no_check c) gl + in tclTHEN (tclEVARUNIVCONTEXT ctx) (refine_no_check c) gl let assumption = let rec arec gl only_eq = function @@ -1244,8 +1224,8 @@ let assumption = let env = Proofview.Goal.env gl in infer_conv env sigma t concl in - if is_same_type then - (Proofview.V82.tclEVARS sigma) <*> + if is_same_type then + (Proofview.V82.tclEVARS sigma) <*> Proofview.Refine.refine (fun h -> (h, mkVar id)) else arec gl only_eq rest in @@ -1293,7 +1273,7 @@ let rec intros_clearing = function let specialize mopt (c,lbind) g = let tac, term = - if lbind == NoBindings then + if lbind == NoBindings then let evd = Typeclasses.resolve_typeclasses (pf_env g) (project g) in tclEVARS evd, nf_evar evd c else @@ -1368,8 +1348,8 @@ let constructor_tac with_evars expctdnumopt i lbind = let nconstr = Array.length (snd (Global.lookup_inductive (fst mind))).mind_consnames in check_number_of_constructors expctdnumopt i nconstr; - - let sigma, cons = Evd.fresh_constructor_instance + + let sigma, cons = Evd.fresh_constructor_instance (Proofview.Goal.env gl) (Proofview.Goal.sigma gl) (fst mind, i) in let cons = mkConstructU cons in @@ -1465,10 +1445,9 @@ let intro_decomp_eq loc b l l' thin tac id = let t = Tacmach.New.pf_type_of gl c in let _,t = Tacmach.New.pf_reduce_to_quantified_ind gl t in let eq,u,eq_args = my_find_eq_data_decompose gl t in - let eq_clause = Tacmach.New.pf_apply make_clenv_binding gl (c,t) NoBindings in !intro_decomp_eq_function (fun n -> tac ((dloc,id)::thin) (adjust_intro_patterns n l @ l')) - (eq,t,eq_args) eq_clause + (eq,t,eq_args) (c, t) end let intro_or_and_pattern loc b ll l' thin tac id = @@ -1689,150 +1668,28 @@ let tclMAPFIRST tacfun l = let tacfun x = Proofview.V82.tactic (tacfun x) in List.fold_right (fun x -> Tacticals.New.tclTHENFIRST (tacfun x)) l (Proofview.tclUNIT()) -let general_apply_in sidecond_first with_delta with_destruct with_evars +let general_apply_in sidecond_first with_delta with_destruct with_evars id lemmas ipat = if sidecond_first then (* Skip the side conditions of the applied lemma *) Tacticals.New.tclTHENLAST (tclMAPLAST - (apply_in_once sidecond_first with_delta with_destruct with_evars id) + (apply_in_once sidecond_first with_delta with_destruct with_evars id) lemmas) (as_tac id ipat) - else + else Tacticals.New.tclTHENFIRST (tclMAPFIRST - (apply_in_once sidecond_first with_delta with_destruct with_evars id) + (apply_in_once sidecond_first with_delta with_destruct with_evars id) lemmas) (as_tac id ipat) let apply_in simple with_evars id lemmas ipat = general_apply_in false simple simple with_evars id lemmas ipat -(**************************) -(* Generalize tactics *) -(**************************) - -let generalized_name c t ids cl = function - | Name id as na -> - if Id.List.mem id ids then - errorlabstrm "" (pr_id id ++ str " is already used"); - na - | Anonymous -> - match kind_of_term c with - | Var id -> - (* Keep the name even if not occurring: may be used by intros later *) - Name id - | _ -> - if noccurn 1 cl then Anonymous else - (* On ne s'etait pas casse la tete : on avait pris pour nom de - variable la premiere lettre du type, meme si "c" avait ete une - constante dont on aurait pu prendre directement le nom *) - named_hd (Global.env()) t Anonymous - -let generalize_goal gl i ((occs,c,b),na) (cl,evd) = - let t = pf_type_of gl c in - let decls,cl = decompose_prod_n_assum i cl in - let dummy_prod = it_mkProd_or_LetIn mkProp decls in - let newdecls,_ = decompose_prod_n_assum i (subst_term_gen eq_constr_nounivs c dummy_prod) in - let cl',evd' = subst_closed_term_univs_occ evd occs c (it_mkProd_or_LetIn cl newdecls) in - let na = generalized_name c t (pf_ids_of_hyps gl) cl' na in - mkProd_or_LetIn (na,b,t) cl', evd - -let generalize_dep ?(with_let=false) c gl = - let env = pf_env gl in - let sign = pf_hyps gl in - let init_ids = ids_of_named_context (Global.named_context()) in - let seek d toquant = - if List.exists (fun (id,_,_) -> occur_var_in_decl env id d) toquant - || dependent_in_decl c d then - d::toquant - else - toquant in - let to_quantify = Context.fold_named_context seek sign ~init:[] in - let to_quantify_rev = List.rev to_quantify in - let qhyps = List.map (fun (id,_,_) -> id) to_quantify_rev in - let tothin = List.filter (fun id -> not (Id.List.mem id init_ids)) qhyps in - let tothin' = - match kind_of_term c with - | Var id when mem_named_context id sign && not (Id.List.mem id init_ids) - -> id::tothin - | _ -> tothin - in - let cl' = it_mkNamedProd_or_LetIn (pf_concl gl) to_quantify in - let body = - if with_let then - match kind_of_term c with - | Var id -> pi2 (pf_get_hyp gl id) - | _ -> None - else None - in - let cl'',evd = generalize_goal gl 0 ((AllOccurrences,c,body),Anonymous) - (cl',project gl) in - let args = instance_from_named_context to_quantify_rev in - tclTHENLIST - [tclPUSHEVARUNIVCONTEXT (Evd.evar_universe_context evd); - apply_type cl'' (if Option.is_empty body then c::args else args); - thin (List.rev tothin')] - gl - -let generalize_gen_let lconstr gl = - let newcl, evd = - List.fold_right_i (generalize_goal gl) 0 lconstr - (pf_concl gl,project gl) - in - tclTHEN (tclPUSHEVARUNIVCONTEXT (Evd.evar_universe_context evd)) - (apply_type newcl (List.map_filter (fun ((_,c,b),_) -> - if Option.is_empty b then Some c else None) lconstr)) gl - -let generalize_gen lconstr = - generalize_gen_let (List.map (fun ((occs,c),na) -> - (occs,c,None),na) lconstr) - -let generalize l = - generalize_gen_let (List.map (fun c -> ((AllOccurrences,c,None),Anonymous)) l) - -let revert hyps gl = - let lconstr = List.map (fun id -> - let (_, b, _) = pf_get_hyp gl id in - ((AllOccurrences, mkVar id, b), Anonymous)) - hyps - in tclTHEN (generalize_gen_let lconstr) (clear hyps) gl - -(* Faudra-t-il une version avec plusieurs args de generalize_dep ? -Cela peut-être troublant de faire "Generalize Dependent H n" dans -"n:nat; H:n=n |- P(n)" et d'échouer parce que H a disparu après la -généralisation dépendante par n. - -let quantify lconstr = - List.fold_right - (fun com tac -> tclTHEN tac (tactic_com generalize_dep c)) - lconstr - tclIDTAC -*) - -(* A dependent cut rule à la sequent calculus - ------------------------------------------ - Sera simplifiable le jour où il y aura un let in primitif dans constr - - [letin_tac b na c (occ_hyp,occ_ccl) gl] transforms - [...x1:T1(c),...,x2:T2(c),... |- G(c)] into - [...x:T;Heqx:(x=c);x1:T1(x),...,x2:T2(x),... |- G(x)] if [b] is false or - [...x:=c:T;x1:T1(x),...,x2:T2(x),... |- G(x)] if [b] is true - - [occ_hyp,occ_ccl] tells which occurrences of [c] have to be substituted; - if [occ_hyp = []] and [occ_ccl = None] then [c] is substituted - wherever it occurs, otherwise [c] is substituted only in hyps - present in [occ_hyps] at the specified occurrences (everywhere if - the list of occurrences is empty), and in the goal at the specified - occurrences if [occ_goal] is not [None]; - - if name = Anonymous, the name is build from the first letter of the type; - - The tactic first quantify the goal over x1, x2,... then substitute then - re-intro x1, x2,... at their initial place ([marks] is internally - used to remember the place of x1, x2, ...: it is the list of hypotheses on - the left of each x1, ...). -*) +(*****************************) +(* Tactics abstracting terms *) +(*****************************) let out_arg = function | ArgVar _ -> anomaly (Pp.str "Unevaluated or_var variable") @@ -1876,35 +1733,52 @@ let default_matching_flags sigma = { allow_K_in_toplevel_higher_order_unification = false } +(* This supports search of occurrences of term from a pattern *) + let make_pattern_test env sigma0 (sigma,c) = let flags = default_matching_flags sigma0 in let matching_fun _ t = - try let sigma = w_unify env sigma Reduction.CONV ~flags c t in + try let sigma = w_unify env sigma Reduction.CONV ~flags c t in Some(sigma, t) with e when Errors.noncritical e -> raise NotUnifiable in let merge_fun c1 c2 = match c1, c2 with - | Some (evd,c1), Some (_,c2) -> + | Some (evd,c1), Some (_,c2) -> (try let evd = w_unify env evd Reduction.CONV ~flags c1 c2 in - Some (evd, c1) + Some (evd, c1) with e when Errors.noncritical e -> raise NotUnifiable) | Some _, None -> c1 | None, Some _ -> c2 - | None, None -> None + | None, None -> None in - { match_fun = matching_fun; merge_fun = merge_fun; + { match_fun = matching_fun; merge_fun = merge_fun; testing_state = None; last_found = None }, (fun test -> match test.testing_state with - | None -> + | None -> let ctx, c = finish_evar_resolution env sigma0 (sigma,c) in - Proofview.V82.tactic (tclPUSHEVARUNIVCONTEXT ctx), c - | Some (sigma,_) -> + Proofview.V82.tclEVARUNIVCONTEXT ctx, c + | Some (sigma,_) -> let univs, subst = nf_univ_variables sigma in - Proofview.V82.tactic (tclPUSHEVARUNIVCONTEXT (Evd.evar_universe_context univs)), + Proofview.V82.tclEVARUNIVCONTEXT (Evd.evar_universe_context univs), subst_univs_constr subst (nf_evar sigma c)) -let letin_abstract id c (test,out) (occs,check_occs) gl = - let env = pf_env gl in +let make_eq_test evd c = + let out cstr = + let tac = Proofview.V82.tclEVARUNIVCONTEXT (Evd.evar_universe_context cstr.testing_state) in + tac, c + in + (Tacred.make_eq_univs_test evd c, out) + +let make_abstraction_core name (test,out) (sigmac,c) ty occs check_occs gl = + let env = Proofview.Goal.env gl in + let id = + let t = match ty with Some t -> t | None -> typ_of env sigmac c in + let x = id_of_name_using_hdchar (Global.env()) t name in + if name == Anonymous then Tacmach.New.of_old (fresh_id [] x) gl else + let hyps = Proofview.Goal.hyps gl in + if not (mem_named_context x hyps) then x else + error ("The variable "^(Id.to_string x)^" is already declared.") + in let compute_dependency _ (hyp,_,_ as d) depdecls = match occurrences_of_hyp hyp occs with | None -> depdecls @@ -1920,31 +1794,50 @@ let letin_abstract id c (test,out) (occs,check_occs) gl = let newdecl = subst_closed_term_occ_decl_modulo occ test d in (subst1_named_decl (mkVar id) newdecl)::depdecls in let depdecls = fold_named_context compute_dependency env ~init:[] in + let concl = Proofview.Goal.concl gl in let ccl = match occurrences_of_goal occs with - | None -> pf_concl gl + | None -> concl | Some occ -> - subst1 (mkVar id) (subst_closed_term_occ_modulo occ test None (pf_concl gl)) in + subst1 (mkVar id) (subst_closed_term_occ_modulo occ test None concl) in let lastlhyp = if List.is_empty depdecls then MoveLast else MoveAfter(pi1(List.last depdecls)) in - (depdecls,lastlhyp,ccl,out test) + (id,depdecls,lastlhyp,ccl,out test) + +(** [make_abstraction] is the main entry point to abstract over a term + or pattern at some occurrences; it returns: + - the id used for the abstraction + - the type of the abstraction + - the hypotheses from the context which depend on the term or pattern + - the most recent hyp before which there is no dependency in the term of pattern + - the abstracted conclusion + - a tactic to apply to take evars effects into account + - the term or pattern to abstract fully instantiated +*) + +type abstraction_request = +| AbstractPattern of Name.t * (evar_map * constr) * clause * bool +| AbstractExact of Name.t * constr * types option * clause * bool + +let make_abstraction abs gl = + let evd = Proofview.Goal.sigma gl in + let env = Proofview.Goal.env gl in + match abs with + | AbstractPattern (name,c,occs,check_occs) -> + make_abstraction_core name (make_pattern_test env evd c) c None occs check_occs gl + | AbstractExact (name,c,ty,occs,check_occs) -> + make_abstraction_core name (make_eq_test evd c) (evd,c) ty occs check_occs gl + +(* [letin_tac b (... abstract over c ...) gl] transforms + [...x1:T1(c),...,x2:T2(c),... |- G(c)] into + [...x:T;Heqx:(x=c);x1:T1(x),...,x2:T2(x),... |- G(x)] if [b] is false or + [...x:=c:T;x1:T1(x),...,x2:T2(x),... |- G(x)] if [b] is true +*) -let letin_tac_gen with_eq name (sigmac,c) test ty occs = +let letin_tac_gen with_eq abs ty = Proofview.Goal.enter begin fun gl -> let env = Proofview.Goal.env gl in - let hyps = Proofview.Goal.hyps gl in - let id = - let t = match ty with Some t -> t | None -> typ_of env sigmac c in - let x = id_of_name_using_hdchar (Global.env()) t name in - if name == Anonymous then Tacmach.New.of_old (fresh_id [] x) gl else - if not (mem_named_context x hyps) then x else - error ("The variable "^(Id.to_string x)^" is already declared.") - in - let (depdecls,lastlhyp,ccl,(tac,c)) = - Tacmach.New.of_old (letin_abstract id c test occs) gl - in - let t = - match ty with Some t -> t | None -> Tacmach.New.pf_apply (fun e s -> typ_of e s c) gl - in + let (id,depdecls,lastlhyp,ccl,(tac,c)) = make_abstraction abs gl in + let t = match ty with Some t -> t | _ -> typ_of env (Proofview.Goal.sigma gl) c in let (sigma,newcl,eq_tac) = match with_eq with | Some (lr,(loc,ido)) -> let heq = match ido with @@ -1972,25 +1865,11 @@ let letin_tac_gen with_eq name (sigmac,c) test ty occs = eq_tac ] end -let make_eq_test evd c = - let out cstr = - let tac = tclPUSHEVARUNIVCONTEXT (Evd.evar_universe_context cstr.testing_state) in - Proofview.V82.tactic tac, c - in - (Tacred.make_eq_univs_test Evd.empty c, out) - let letin_tac with_eq name c ty occs = - Proofview.tclEVARMAP >>= fun sigma -> - letin_tac_gen with_eq name (sigma,c) (make_eq_test sigma c) ty (occs,true) + letin_tac_gen with_eq (AbstractExact (name,c,ty,occs,true)) ty -let letin_pat_tac with_eq name c ty occs = - Proofview.Goal.raw_enter begin fun gl -> - let sigma = Proofview.Goal.sigma gl in - let env = Proofview.Goal.env gl in - letin_tac_gen with_eq name c - (make_pattern_test env sigma c) - ty (occs,true) - end +let letin_pat_tac with_eq name c occs = + letin_tac_gen with_eq (AbstractPattern (name,c,occs,false)) None (* Tactics "pose proof" (usetac=None) and "assert" (otherwise) *) let forward usetac ipat c = @@ -2006,6 +1885,179 @@ let forward usetac ipat c = let pose_proof na c = forward None (ipat_of_name na) c let assert_by na t tac = forward (Some tac) (ipat_of_name na) t +(***************************) +(* Generalization tactics *) +(***************************) + +(* Given a type [T] convertible to [forall x1..xn:A1..An(x1..xn-1), G(x1..xn)] + and [a1..an:A1..An(a1..an-1)] such that the goal is [G(a1..an)], + this generalizes [hyps |- goal] into [hyps |- T] *) + +let apply_type hdcty argl gl = + refine (applist (mkCast (Evarutil.mk_new_meta(),DEFAULTcast, hdcty),argl)) gl + +(* Given a context [hyps] with domain [x1..xn], possibly with let-ins, + and well-typed in the current goal, [bring_hyps hyps] generalizes + [ctxt |- G(x1..xn] into [ctxt |- forall hyps, G(x1..xn)] *) + +let bring_hyps hyps = + if List.is_empty hyps then Tacticals.New.tclIDTAC + else + Proofview.Goal.raw_enter begin fun gl -> + let env = Proofview.Goal.env gl in + let concl = Tacmach.New.pf_nf_concl gl in + let newcl = List.fold_right mkNamedProd_or_LetIn hyps concl in + let args = Array.of_list (instance_from_named_context hyps) in + Proofview.Refine.refine begin fun h -> + let (h, ev) = Proofview.Refine.new_evar h env newcl in + (h, (mkApp (ev, args))) + end + end + +(* Compute a name for a generalization *) + +let generalized_name c t ids cl = function + | Name id as na -> + if Id.List.mem id ids then + errorlabstrm "" (pr_id id ++ str " is already used"); + na + | Anonymous -> + match kind_of_term c with + | Var id -> + (* Keep the name even if not occurring: may be used by intros later *) + Name id + | _ -> + if noccurn 1 cl then Anonymous else + (* On ne s'etait pas casse la tete : on avait pris pour nom de + variable la premiere lettre du type, meme si "c" avait ete une + constante dont on aurait pu prendre directement le nom *) + named_hd (Global.env()) t Anonymous + +(* Abstract over [c] in [forall x1:A1(c)..xi:Ai(c).T(c)] producing + [forall x, x1:A1(x1), .., xi:Ai(x). T(x)] with all [c] abtracted in [Ai] + but only those at [occs] in [T] *) + +let generalize_goal_gen ids i ((occs,c,b),na) t (cl,evd) = + let decls,cl = decompose_prod_n_assum i cl in + let dummy_prod = it_mkProd_or_LetIn mkProp decls in + let newdecls,_ = decompose_prod_n_assum i (subst_term_gen eq_constr_nounivs c dummy_prod) in + let cl',evd' = subst_closed_term_univs_occ evd occs c (it_mkProd_or_LetIn cl newdecls) in + let na = generalized_name c t ids cl' na in + mkProd_or_LetIn (na,b,t) cl', evd' + +let generalize_goal gl i ((occs,c,b),na as o) cl = + let t = pf_type_of gl c in + generalize_goal_gen (pf_ids_of_hyps gl) i o t cl + +let generalize_dep ?(with_let=false) c gl = + let env = pf_env gl in + let sign = pf_hyps gl in + let init_ids = ids_of_named_context (Global.named_context()) in + let seek d toquant = + if List.exists (fun (id,_,_) -> occur_var_in_decl env id d) toquant + || dependent_in_decl c d then + d::toquant + else + toquant in + let to_quantify = Context.fold_named_context seek sign ~init:[] in + let to_quantify_rev = List.rev to_quantify in + let qhyps = List.map (fun (id,_,_) -> id) to_quantify_rev in + let tothin = List.filter (fun id -> not (Id.List.mem id init_ids)) qhyps in + let tothin' = + match kind_of_term c with + | Var id when mem_named_context id sign && not (Id.List.mem id init_ids) + -> id::tothin + | _ -> tothin + in + let cl' = it_mkNamedProd_or_LetIn (pf_concl gl) to_quantify in + let body = + if with_let then + match kind_of_term c with + | Var id -> pi2 (pf_get_hyp gl id) + | _ -> None + else None + in + let cl'',evd = generalize_goal gl 0 ((AllOccurrences,c,body),Anonymous) + (cl',project gl) in + let args = instance_from_named_context to_quantify_rev in + tclTHENLIST + [tclEVARS evd; + apply_type cl'' (if Option.is_empty body then c::args else args); + thin (List.rev tothin')] + gl + +(** *) +let generalize_gen_let lconstr gl = + let newcl, evd = + List.fold_right_i (generalize_goal gl) 0 lconstr + (pf_concl gl,project gl) + in + tclTHEN (tclEVARS evd) + (apply_type newcl (List.map_filter (fun ((_,c,b),_) -> + if Option.is_empty b then Some c else None) lconstr)) gl + +let new_generalize_gen_let lconstr = + Proofview.Goal.raw_enter begin fun gl -> + let gl = Proofview.Goal.assume gl in + let concl = Proofview.Goal.concl gl in + let sigma = Proofview.Goal.sigma gl in + let env = Proofview.Goal.env gl in + let ids = Tacmach.New.pf_ids_of_hyps gl in + let (newcl, sigma), args = + List.fold_right_i + (fun i ((_,c,b),_ as o) (cl, args) -> + let t = Tacmach.New.pf_type_of gl c in + let args = if Option.is_empty b then c :: args else args in + generalize_goal_gen ids i o t cl, args) + 0 lconstr ((concl, sigma), []) + in + Proofview.V82.tclEVARS sigma <*> + Proofview.Refine.refine begin fun h -> + let (h, ev) = Proofview.Refine.new_evar h env newcl in + (h, (applist (ev, args))) + end + end + +let generalize_gen lconstr = + generalize_gen_let (List.map (fun ((occs,c),na) -> + (occs,c,None),na) lconstr) + +let new_generalize_gen lconstr = + new_generalize_gen_let (List.map (fun ((occs,c),na) -> + (occs,c,None),na) lconstr) + +let generalize l = + generalize_gen_let (List.map (fun c -> ((AllOccurrences,c,None),Anonymous)) l) + +let new_generalize l = + new_generalize_gen_let (List.map (fun c -> ((AllOccurrences,c,None),Anonymous)) l) + +let revert hyps gl = + let lconstr = List.map (fun id -> + let (_, b, _) = pf_get_hyp gl id in + ((AllOccurrences, mkVar id, b), Anonymous)) + hyps + in tclTHEN (generalize_gen_let lconstr) (clear hyps) gl + +let new_revert hyps = + Proofview.Goal.raw_enter begin fun gl -> + let gl = Proofview.Goal.assume gl in + let ctx = List.map (fun id -> Tacmach.New.pf_get_hyp id gl) hyps in + (bring_hyps ctx) <*> (Proofview.V82.tactic (clear hyps)) + end + +(* Faudra-t-il une version avec plusieurs args de generalize_dep ? +Cela peut-être troublant de faire "Generalize Dependent H n" dans +"n:nat; H:n=n |- P(n)" et d'échouer parce que H a disparu après la +généralisation dépendante par n. + +let quantify lconstr = + List.fold_right + (fun com tac -> tclTHEN tac (tactic_com generalize_dep c)) + lconstr + tclIDTAC +*) + (*****************************) (* Ad hoc unfold *) (*****************************) @@ -2503,16 +2555,16 @@ let coq_heq = lazy (Coqlib.coq_constant "mkHEq" ["Logic";"JMeq"] "JMeq") let coq_heq_refl = lazy (Coqlib.coq_constant "mkHEq" ["Logic";"JMeq"] "JMeq_refl") -let mkEq t x y = +let mkEq t x y = mkApp (Lazy.force coq_eq, [| t; x; y |]) - -let mkRefl t x = + +let mkRefl t x = mkApp (Lazy.force coq_eq_refl, [| t; x |]) let mkHEq t x u y = mkApp (Lazy.force coq_heq, [| t; x; u; y |]) - + let mkHRefl t x = mkApp (Lazy.force coq_heq_refl, [| t; x |]) @@ -2531,7 +2583,7 @@ let ids_of_constr ?(all=false) vars c = let rec aux vars c = match kind_of_term c with | Var id -> Id.Set.add id vars - | App (f, args) -> + | App (f, args) -> (match kind_of_term f with | Construct ((ind,_),_) | Ind (ind,_) -> @@ -2542,7 +2594,7 @@ let ids_of_constr ?(all=false) vars c = | _ -> fold_constr aux vars c) | _ -> fold_constr aux vars c in aux vars c - + let decompose_indapp f args = match kind_of_term f with | Construct ((ind,_),_) @@ -2589,7 +2641,7 @@ let make_abstract_generalize gl id concl dep ctx body c eqs args refls = mkApp (appeqs, abshypt) let hyps_of_vars env sign nogen hyps = - if Id.Set.is_empty hyps then [] + if Id.Set.is_empty hyps then [] else let (_,lh) = Context.fold_named_context_reverse @@ -2602,17 +2654,17 @@ let hyps_of_vars env sign nogen hyps = (Id.Set.add x hs, x :: hl) else (hs, hl)) ~init:(hyps,[]) - sign + sign in lh exception Seen -let linear vars args = +let linear vars args = let seen = ref vars in - try - Array.iter (fun i -> + try + Array.iter (fun i -> let rels = ids_of_constr ~all:true Id.Set.empty i in - let seen' = + let seen' = Id.Set.fold (fun id acc -> if Id.Set.mem id acc then raise Seen else Id.Set.add id acc) @@ -2639,7 +2691,7 @@ let abstract_args gl generalize_vars dep id defined f args = (* Build application generalized w.r.t. the argument plus the necessary eqs. From env |- c : forall G, T and args : G we build (T[G'], G' : ctx, env ; G' |- args' : G, eqs := G'_i = G_i, refls : G' = G, vars to generalize) - + eqs are not lifted w.r.t. each other yet. (* will be needed when going to dependent indexes *) *) let aux (prod, ctx, ctxenv, c, args, eqs, refls, nongenvars, vars, env) arg = @@ -2672,9 +2724,9 @@ let abstract_args gl generalize_vars dep id defined f args = let eqs = eq :: lift_list eqs in let refls = refl :: refls in let argvars = ids_of_constr vars arg in - (arity, ctx, push_rel decl ctxenv, c', args, eqs, refls, + (arity, ctx, push_rel decl ctxenv, c', args, eqs, refls, nongenvars, Id.Set.union argvars vars, env) - in + in let f', args' = decompose_indapp f args in let dogen, f', args' = let parvars = ids_of_constr ~all:true Id.Set.empty f' in @@ -2687,11 +2739,11 @@ let abstract_args gl generalize_vars dep id defined f args = true, mkApp (f', before), after in if dogen then - let arity, ctx, ctxenv, c', args, eqs, refls, nogen, vars, env = + let arity, ctx, ctxenv, c', args, eqs, refls, nogen, vars, env = Array.fold_left aux (pf_type_of gl f',[],env,f',[],[],[],Id.Set.empty,Id.Set.empty,env) args' in let args, refls = List.rev args, List.rev refls in - let vars = + let vars = if generalize_vars then let nogen = Id.Set.add id nogen in hyps_of_vars (pf_env gl) (pf_hyps gl) nogen vars @@ -2711,28 +2763,28 @@ let abstract_generalize ?(generalize_vars=true) ?(force_dep=false) id = match b with | None -> let f, args = decompose_app t in (f, args, false, id, oldid) - | Some t -> + | Some t -> let f, args = decompose_app t in (f, args, true, id, oldid) in if List.is_empty args then Proofview.tclUNIT () - else + else let args = Array.of_list args in let newc = Tacmach.New.of_old (fun gl -> abstract_args gl generalize_vars force_dep id def f args) gl in match newc with | None -> Proofview.tclUNIT () - | Some (newc, dep, n, vars) -> + | Some (newc, dep, n, vars) -> let tac = if dep then - Tacticals.New.tclTHENLIST [Proofview.V82.tactic (refine newc); Proofview.V82.tactic (rename_hyp [(id, oldid)]); Tacticals.New.tclDO n intro; + Tacticals.New.tclTHENLIST [Proofview.V82.tactic (refine newc); Proofview.V82.tactic (rename_hyp [(id, oldid)]); Tacticals.New.tclDO n intro; Proofview.V82.tactic (generalize_dep ~with_let:true (mkVar oldid))] else Tacticals.New.tclTHENLIST [Proofview.V82.tactic (refine newc); Proofview.V82.tactic (clear [id]); Tacticals.New.tclDO n intro] in if List.is_empty vars then tac - else Tacticals.New.tclTHEN tac + else Tacticals.New.tclTHEN tac (Proofview.V82.tactic (fun gl -> tclFIRST [revert vars ; - tclMAP (fun id -> + tclMAP (fun id -> tclTRY (generalize_dep ~with_let:true (mkVar id))) vars] gl)) end @@ -2744,12 +2796,12 @@ let specialize_eqs id gl = let env = pf_env gl in let ty = pf_get_hyp_typ gl id in let evars = ref (project gl) in - let unif env evars c1 c2 = - compare_upto_variables c1 c2 && Evarconv.e_conv env evars c1 c2 + let unif env evars c1 c2 = + compare_upto_variables c1 c2 && Evarconv.e_conv env evars c1 c2 in let rec aux in_eqs ctx acc ty = match kind_of_term ty with - | Prod (na, t, b) -> + | Prod (na, t, b) -> (match kind_of_term t with | App (eq, [| eqty; x; y |]) when eq_constr (Lazy.force coq_eq) eq -> let c = if noccur_between 1 (List.length ctx) x then y else x in @@ -2765,13 +2817,13 @@ let specialize_eqs id gl = if unif (push_rel_context ctx env) evars pt t then aux true ctx (mkApp (acc, [| p |])) (subst1 p b) else acc, in_eqs, ctx, ty - | _ -> + | _ -> if in_eqs then acc, in_eqs, ctx, ty - else + else let e = e_new_evar evars (push_rel_context ctx env) t in aux false ((na, Some e, t) :: ctx) (mkApp (lift 1 acc, [| mkRel 1 |])) b) | t -> acc, in_eqs, ctx, ty - in + in let acc, worked, ctx, ty = aux false [] (mkVar id) ty in let ctx' = nf_rel_context_evar !evars ctx in let ctx'' = List.map (fun (n,b,t as decl) -> @@ -2781,14 +2833,14 @@ let specialize_eqs id gl = in let ty' = it_mkProd_or_LetIn ty ctx'' in let acc' = it_mkLambda_or_LetIn acc ctx'' in - let ty' = Tacred.whd_simpl env !evars ty' + let ty' = Tacred.whd_simpl env !evars ty' and acc' = Tacred.whd_simpl env !evars acc' in let ty' = Evarutil.nf_evar !evars ty' in if worked then tclTHENFIRST (Tacmach.internal_cut true id ty') (exact_no_check ((* refresh_universes_strict *) acc')) gl else tclFAIL 0 (str "Nothing to do in hypothesis " ++ pr_id id) gl - + let specialize_eqs id gl = if @@ -3234,10 +3286,8 @@ let induction_tac with_evars elim (varname,lbind) typ gl = let ({elimindex=i;elimbody=(elimc,lbindelimc)},elimt) = elim in let indclause = pf_apply make_clenv_binding gl (mkVar varname,typ) lbind in let i = match i with None -> index_of_ind_arg elimt | Some i -> i in - let elimclause = - pf_apply make_clenv_binding gl - (mkCast (elimc,DEFAULTcast,elimt),elimt) lbindelimc in - elimination_clause_scheme with_evars i elimclause indclause gl + let elimc = mkCast (elimc, DEFAULTcast, elimt) in + elimination_clause_scheme with_evars i (elimc, elimt, lbindelimc) indclause gl let induction_from_context isrec with_evars (indref,nparams,elim) (hyp0,lbind) names inhyps = @@ -3280,7 +3330,7 @@ let induction_without_atomization isrec with_evars elim names lid = let nlid = List.length lid in if not (Int.equal nlid awaited_nargs) then Proofview.tclZERO (Errors.UserError ("", str"Not the right number of induction arguments.")) - else + else Proofview.tclTHEN (Proofview.V82.tclEVARS sigma) (induction_from_context_l with_evars elim_info lid names) end @@ -3314,7 +3364,7 @@ let clear_unselected_context id inhyps cls gl = thin ids gl | None -> tclIDTAC gl -let new_induct_gen isrec with_evars elim (eqname,names) (sigma,(c,lbind)) cls = +let induction_gen isrec with_evars elim (eqname,names) (sigma,(c,lbind)) cls = let inhyps = match cls with | Some {onhyps=Some hyps} -> List.map (fun ((_,id),_) -> id) hyps | _ -> [] in @@ -3328,7 +3378,6 @@ let new_induct_gen isrec with_evars elim (eqname,names) (sigma,(c,lbind)) cls = isrec with_evars elim names (id,lbind) inhyps) | _ -> Proofview.Goal.raw_enter begin fun gl -> - let defs = Proofview.Goal.sigma gl in let env = Proofview.Goal.env gl in let x = id_of_name_using_hdchar (Global.env()) (typ_of env sigma c) Anonymous in @@ -3337,12 +3386,10 @@ let new_induct_gen isrec with_evars elim (eqname,names) (sigma,(c,lbind)) cls = let with_eq = Option.map (fun eq -> (false,eq)) eqname in (* TODO: if ind has predicate parameters, use JMeq instead of eq *) Proofview.Goal.raw_enter begin fun gl -> - let env = Proofview.Goal.env gl in Tacticals.New.tclTHEN (* Warning: letin is buggy when c is not of inductive type *) - (letin_tac_gen with_eq (Name id) (sigma,c) - (make_pattern_test env defs (sigma,c)) - None (Option.default allHypsAndConcl cls,false)) + (letin_tac_gen with_eq + (AbstractPattern (Name id,(sigma,c),(Option.default allHypsAndConcl cls),false)) None) (induction_with_atomization_of_ind_arg isrec with_evars elim names (id,lbind) inhyps) end @@ -3352,8 +3399,8 @@ let new_induct_gen isrec with_evars elim (eqname,names) (sigma,(c,lbind)) cls = atomic (using letins), then do induction. The specificity here is that all arguments and parameters of the scheme are given (mandatory for the moment), so we don't need to deal with - parameters of the inductive type as in new_induct_gen. *) -let new_induct_gen_l isrec with_evars elim (eqname,names) lc = + parameters of the inductive type as in induction_gen. *) +let induction_gen_l isrec with_evars elim (eqname,names) lc = if not (Option.is_empty eqname) then errorlabstrm "" (str "Do not know what to do with " ++ Miscprint.pr_intro_pattern (Option.get eqname)); @@ -3399,14 +3446,14 @@ let new_induct_gen_l isrec with_evars elim (eqname,names) lc = principles). TODO: really unify induction with one and induction with several args *) -let induct_destruct isrec with_evars (lc,elim,names,cls) = +let induction_destruct_core isrec with_evars (lc,elim,names,cls) = assert (List.length lc > 0); (* ensured by syntax, but if called inside caml? *) Proofview.Goal.raw_enter begin fun gl -> let ifi = is_functional_induction elim gl in if Int.equal (List.length lc) 1 && not ifi then (* standard induction *) onOpenInductionArg - (fun c -> new_induct_gen isrec with_evars elim names c cls) + (fun c -> induction_gen isrec with_evars elim names c cls) (List.hd lc) else begin (* functional induction *) @@ -3429,7 +3476,7 @@ let induct_destruct isrec with_evars (lc,elim,names,cls) = (fun (c,lbind) -> if lbind != NoBindings then error "'with' clause not supported here."; - new_induct_gen_l isrec with_evars elim names [c]) (List.hd lc) + induction_gen_l isrec with_evars elim names [c]) (List.hd lc) | _ -> let newlc = List.map (fun x -> @@ -3437,28 +3484,28 @@ let induct_destruct isrec with_evars (lc,elim,names,cls) = | ElimOnConstr (x,NoBindings) -> x | _ -> error "Don't know where to find some argument.") lc in - new_induct_gen_l isrec with_evars elim names newlc + induction_gen_l isrec with_evars elim names newlc end end end let induction_destruct isrec with_evars = function | [],_,_ -> Proofview.tclUNIT () - | [a,b],el,cl -> induct_destruct isrec with_evars ([a],el,b,cl) + | [a,b],el,cl -> induction_destruct_core isrec with_evars ([a],el,b,cl) | (a,b)::l,None,cl -> Tacticals.New.tclTHEN - (induct_destruct isrec with_evars ([a],None,b,cl)) - (Tacticals.New.tclMAP (fun (a,b) -> induct_destruct false with_evars ([a],None,b,cl)) l) + (induction_destruct_core isrec with_evars ([a],None,b,cl)) + (Tacticals.New.tclMAP (fun (a,b) -> induction_destruct_core false with_evars ([a],None,b,cl)) l) | l,Some el,cl -> let check_basic_using = function | a,(None,None) -> a | _ -> error "Unsupported syntax for \"using\"." in let l' = List.map check_basic_using l in - induct_destruct isrec with_evars (l', Some el, (None,None), cl) + induction_destruct_core isrec with_evars (l', Some el, (None,None), cl) -let new_induct ev lc e idl cls = induct_destruct true ev (lc,e,idl,cls) -let new_destruct ev lc e idl cls = induct_destruct false ev (lc,e,idl,cls) +let induction ev lc e idl cls = induction_destruct_core true ev (lc,e,idl,cls) +let destruct ev lc e idl cls = induction_destruct_core false ev (lc,e,idl,cls) (* The registered tactic, which calls the default elimination * if no elimination constant is provided. *) @@ -3509,8 +3556,8 @@ let elim_type t gl = let case_type t gl = let (ind,t) = pf_reduce_to_atomic_ind gl t in - let evd, elimc = - pf_apply build_case_analysis_scheme_default gl ind (elimination_sort_of_goal gl) + let evd, elimc = + pf_apply build_case_analysis_scheme_default gl ind (elimination_sort_of_goal gl) in tclTHEN (tclEVARS evd) (elim_scheme_type elimc t) gl @@ -3742,7 +3789,7 @@ let abstract_subproof id gk tac = with Uninstantiated_evar _ -> error "\"abstract\" cannot handle existentials." in - let evd, ctx, concl = + let evd, ctx, concl = (* FIXME: should be done only if the tactic succeeds *) let evd, nf = nf_evars_and_universes (Proofview.Goal.sigma gl) in let ctx = Evd.universe_context_set evd in @@ -3772,7 +3819,7 @@ let abstract_subproof id gk tac = let eff = Safe_typing.sideff_of_con (Global.safe_env ()) cst in let effs = cons_side_effects eff no_seff in let args = List.rev (instance_from_named_context sign) in - let solve = Proofview.V82.tclEVARS evd <*> + let solve = Proofview.V82.tclEVARS evd <*> Proofview.tclEFFECTS effs <*> new_exact_no_check (applist (lem, args)) in if not safe then Proofview.mark_as_unsafe <*> solve else solve end @@ -3783,11 +3830,11 @@ let tclABSTRACT name_op tac = let open Proof_global in let default_gk = (Global, false, Proof Theorem) in let s, gk = match name_op with - | Some s -> + | Some s -> (try let _, gk, _ = current_proof_statement () in s, gk with NoCurrentProof -> s, default_gk) | None -> - let name, gk = + let name, gk = try let name, gk, _ = current_proof_statement () in name, gk with NoCurrentProof -> anon_id, default_gk in add_suffix name "_subproof", gk diff --git a/tactics/tactics.mli b/tactics/tactics.mli index 937efdae1..c3c799bae 100644 --- a/tactics/tactics.mli +++ b/tactics/tactics.mli @@ -166,6 +166,7 @@ val move_hyp : bool -> Id.t -> Id.t move_location -> tactic val rename_hyp : (Id.t * Id.t) list -> tactic val revert : Id.t list -> tactic +val new_revert : Id.t list -> unit Proofview.tactic (** {6 Resolution tactics. } *) @@ -247,12 +248,13 @@ type eliminator = { } val elimination_clause_scheme : evars_flag -> ?flags:unify_flags -> - int -> clausenv -> clausenv -> tactic + int -> (constr * types * constr bindings) -> clausenv -> tactic val elimination_in_clause_scheme : evars_flag -> ?flags:unify_flags -> - Id.t -> int -> clausenv -> clausenv -> tactic + Id.t -> int -> (constr * types * constr bindings) -> clausenv -> tactic -val general_elim_clause_gen : (int -> Clenv.clausenv -> 'a -> tactic) -> +val general_elim_clause_gen : + (int -> (constr * types * constr bindings) -> 'a -> tactic) -> 'a -> eliminator -> tactic val general_elim : evars_flag -> @@ -265,7 +267,7 @@ val elim : val simple_induct : quantified_hypothesis -> unit Proofview.tactic -val new_induct : evars_flag -> +val induction : evars_flag -> (evar_map * constr with_bindings) induction_arg list -> constr with_bindings option -> intro_pattern_expr located option * intro_pattern_expr located option -> @@ -277,7 +279,7 @@ val general_case_analysis : evars_flag -> constr with_bindings -> unit Proofvie val simplest_case : constr -> unit Proofview.tactic val simple_destruct : quantified_hypothesis -> unit Proofview.tactic -val new_destruct : evars_flag -> +val destruct : evars_flag -> (evar_map * constr with_bindings) induction_arg list -> constr with_bindings option -> intro_pattern_expr located option * intro_pattern_expr located option -> @@ -345,13 +347,16 @@ val forward : unit Proofview.tactic option -> intro_pattern_expr located optio val letin_tac : (bool * intro_pattern_expr located) option -> Name.t -> constr -> types option -> clause -> unit Proofview.tactic val letin_pat_tac : (bool * intro_pattern_expr located) option -> Name.t -> - evar_map * constr -> types option -> clause -> unit Proofview.tactic + evar_map * constr -> clause -> unit Proofview.tactic val assert_tac : Name.t -> types -> unit Proofview.tactic val assert_by : Name.t -> types -> unit Proofview.tactic -> unit Proofview.tactic val pose_proof : Name.t -> constr -> unit Proofview.tactic val generalize : constr list -> tactic val generalize_gen : ((occurrences * constr) * Name.t) list -> tactic +val new_generalize : constr list -> unit Proofview.tactic +val new_generalize_gen : ((occurrences * constr) * Name.t) list -> unit Proofview.tactic + val generalize_dep : ?with_let:bool (** Don't lose let bindings *) -> constr -> tactic val unify : ?state:Names.transparent_state -> constr -> constr -> tactic @@ -373,7 +378,7 @@ val subst_one : val declare_intro_decomp_eq : ((int -> unit Proofview.tactic) -> Coqlib.coq_eq_data * types * (types * constr * constr) -> - clausenv -> unit Proofview.tactic) -> unit + constr * types -> unit Proofview.tactic) -> unit module Simple : sig (** Simplified version of some of the above tactics *) diff --git a/tactics/tactics.mllib b/tactics/tactics.mllib index 27ded2357..4eb4318ee 100644 --- a/tactics/tactics.mllib +++ b/tactics/tactics.mllib @@ -1,4 +1,5 @@ Geninterp +Dnet Dn Btermdn Tacticals @@ -20,5 +21,6 @@ Tacenv TacticMatching Tacinterp Evar_tactics +Term_dnet Autorewrite Tactic_option diff --git a/pretyping/term_dnet.ml b/tactics/term_dnet.ml index e05f4bcfe..e05f4bcfe 100644 --- a/pretyping/term_dnet.ml +++ b/tactics/term_dnet.ml diff --git a/pretyping/term_dnet.mli b/tactics/term_dnet.mli index 7825ebdf1..7825ebdf1 100644 --- a/pretyping/term_dnet.mli +++ b/tactics/term_dnet.mli diff --git a/test-suite/bugs/closed/3043.v b/test-suite/bugs/closed/3043.v index 1be5056f9..654663b4f 100644 --- a/test-suite/bugs/closed/3043.v +++ b/test-suite/bugs/closed/3043.v @@ -1,4 +1,4 @@ -Goal (fun A (P : A -> Prop) (X : sigT P) => proj1_sig X) = +Goal (fun A (P : A -> Prop) (X : sigT P) => proj1_sig (sig_of_sigT X)) = (fun A (P : A -> Prop) (X : sigT P) => projT1 X). reflexivity. Qed. diff --git a/test-suite/bugs/closed/3242.v b/test-suite/bugs/closed/3242.v new file mode 100644 index 000000000..805baee15 --- /dev/null +++ b/test-suite/bugs/closed/3242.v @@ -0,0 +1,2 @@ +Inductive Foo (x := Type) := C : Foo -> Foo. + diff --git a/test-suite/bugs/closed/3305.v b/test-suite/bugs/closed/3305.v new file mode 100644 index 000000000..f3f219522 --- /dev/null +++ b/test-suite/bugs/closed/3305.v @@ -0,0 +1,13 @@ +Require Export Coq.Classes.RelationClasses. + +Section defs. + Variable A : Type. + Variable lt : A -> A -> Prop. + Context {ltso : StrictOrder lt}. + + Goal forall (a : A), lt a a -> False. + Proof. + intros a H. + contradict (irreflexivity H). + Qed. +End defs. diff --git a/test-suite/bugs/closed/3306.v b/test-suite/bugs/closed/3306.v new file mode 100644 index 000000000..599e8391a --- /dev/null +++ b/test-suite/bugs/closed/3306.v @@ -0,0 +1,12 @@ + +Inductive Foo(A : Type) : Prop := + foo: A -> Foo A. + +Arguments foo [A] _. + +Scheme Foo_elim := Induction for Foo Sort Prop. + +Goal forall (fn : Foo nat), { x: nat | foo x = fn }. +intro fn. +Fail induction fn as [n] using Foo_elim. (* should fail in a non-Prop context *) +Admitted. diff --git a/test-suite/output/Arguments.out b/test-suite/output/Arguments.out index d1a6be9bd..5a3578f7d 100644 --- a/test-suite/output/Arguments.out +++ b/test-suite/output/Arguments.out @@ -1,11 +1,13 @@ minus : nat -> nat -> nat +minus is monomorphic Argument scopes are [nat_scope nat_scope] The reduction tactics unfold minus avoiding to expose match constructs minus is transparent Expands to: Constant Coq.Init.Peano.minus minus : nat -> nat -> nat +minus is monomorphic Argument scopes are [nat_scope nat_scope] The reduction tactics unfold minus when applied to 1 argument avoiding to expose match constructs @@ -13,6 +15,7 @@ minus is transparent Expands to: Constant Coq.Init.Peano.minus minus : nat -> nat -> nat +minus is monomorphic Argument scopes are [nat_scope nat_scope] The reduction tactics unfold minus when the 1st argument evaluates to a constructor and @@ -21,6 +24,7 @@ minus is transparent Expands to: Constant Coq.Init.Peano.minus minus : nat -> nat -> nat +minus is monomorphic Argument scopes are [nat_scope nat_scope] The reduction tactics unfold minus when the 1st and 2nd arguments evaluate to a constructor and when applied to 2 arguments @@ -28,6 +32,7 @@ minus is transparent Expands to: Constant Coq.Init.Peano.minus minus : nat -> nat -> nat +minus is monomorphic Argument scopes are [nat_scope nat_scope] The reduction tactics unfold minus when the 1st and 2nd arguments evaluate to a constructor @@ -37,6 +42,7 @@ pf : forall D1 C1 : Type, (D1 -> C1) -> forall D2 C2 : Type, (D2 -> C2) -> D1 * D2 -> C1 * C2 +pf is monomorphic Arguments D2, C2 are implicit Arguments D1, C1 are implicit and maximally inserted Argument scopes are [foo_scope type_scope _ _ _ _ _] @@ -45,6 +51,7 @@ pf is transparent Expands to: Constant Top.pf fcomp : forall A B C : Type, (B -> C) -> (A -> B) -> A -> C +fcomp is monomorphic Arguments A, B, C are implicit and maximally inserted Argument scopes are [type_scope type_scope type_scope _ _ _] The reduction tactics unfold fcomp when applied to 6 arguments @@ -52,17 +59,20 @@ fcomp is transparent Expands to: Constant Top.fcomp volatile : nat -> nat +volatile is monomorphic Argument scope is [nat_scope] The reduction tactics always unfold volatile volatile is transparent Expands to: Constant Top.volatile f : T1 -> T2 -> nat -> unit -> nat -> nat +f is monomorphic Argument scopes are [_ _ nat_scope _ nat_scope] f is transparent Expands to: Constant Top.S1.S2.f f : T1 -> T2 -> nat -> unit -> nat -> nat +f is monomorphic Argument scopes are [_ _ nat_scope _ nat_scope] The reduction tactics unfold f when the 3rd, 4th and 5th arguments evaluate to a constructor @@ -70,6 +80,7 @@ f is transparent Expands to: Constant Top.S1.S2.f f : forall T2 : Type, T1 -> T2 -> nat -> unit -> nat -> nat +f is monomorphic Argument T2 is implicit Argument scopes are [type_scope _ _ nat_scope _ nat_scope] The reduction tactics unfold f when the 4th, 5th and @@ -78,6 +89,7 @@ f is transparent Expands to: Constant Top.S1.f f : forall T1 T2 : Type, T1 -> T2 -> nat -> unit -> nat -> nat +f is monomorphic Arguments T1, T2 are implicit Argument scopes are [type_scope type_scope _ _ nat_scope _ nat_scope] The reduction tactics unfold f when the 5th, 6th and @@ -86,6 +98,7 @@ f is transparent Expands to: Constant Top.f f : forall T1 T2 : Type, T1 -> T2 -> nat -> unit -> nat -> nat +f is monomorphic The reduction tactics unfold f when the 5th, 6th and 7th arguments evaluate to a constructor f is transparent diff --git a/test-suite/output/ArgumentsScope.out b/test-suite/output/ArgumentsScope.out index 6643c1429..358a96bc3 100644 --- a/test-suite/output/ArgumentsScope.out +++ b/test-suite/output/ArgumentsScope.out @@ -1,56 +1,70 @@ a : bool -> bool +a is monomorphic Argument scope is [bool_scope] Expands to: Variable a b : bool -> bool +b is monomorphic Argument scope is [bool_scope] Expands to: Variable b negb'' : bool -> bool +negb'' is monomorphic Argument scope is [bool_scope] negb'' is transparent Expands to: Constant Top.A.B.negb'' negb' : bool -> bool +negb' is monomorphic Argument scope is [bool_scope] negb' is transparent Expands to: Constant Top.A.negb' negb : bool -> bool +negb is monomorphic Argument scope is [bool_scope] negb is transparent Expands to: Constant Coq.Init.Datatypes.negb a : bool -> bool +a is monomorphic Expands to: Variable a b : bool -> bool +b is monomorphic Expands to: Variable b negb : bool -> bool +negb is monomorphic negb is transparent Expands to: Constant Coq.Init.Datatypes.negb negb' : bool -> bool +negb' is monomorphic negb' is transparent Expands to: Constant Top.A.negb' negb'' : bool -> bool +negb'' is monomorphic negb'' is transparent Expands to: Constant Top.A.B.negb'' a : bool -> bool +a is monomorphic Expands to: Variable a negb : bool -> bool +negb is monomorphic negb is transparent Expands to: Constant Coq.Init.Datatypes.negb negb' : bool -> bool +negb' is monomorphic negb' is transparent Expands to: Constant Top.negb' negb'' : bool -> bool +negb'' is monomorphic negb'' is transparent Expands to: Constant Top.negb'' diff --git a/test-suite/output/Arguments_renaming.out b/test-suite/output/Arguments_renaming.out index 695efb260..c440d5ba7 100644 --- a/test-suite/output/Arguments_renaming.out +++ b/test-suite/output/Arguments_renaming.out @@ -20,6 +20,7 @@ For eq: Argument scopes are [type_scope _ _] For eq_refl: Argument scopes are [type_scope _] eq_refl : forall (A : Type) (x : A), x = x +eq_refl is monomorphic Arguments are renamed to B, y When applied to no arguments: Arguments B, y are implicit and maximally inserted @@ -35,6 +36,7 @@ For myEq: Argument scopes are [type_scope _ _] For myrefl: Argument scopes are [type_scope _ _] myrefl : forall (B : Type) (x : A), B -> myEq B x x +myrefl is monomorphic Arguments are renamed to C, x, _ Argument C is implicit and maximally inserted Argument scopes are [type_scope _ _] @@ -47,11 +49,13 @@ fix myplus (T : Type) (t : T) (n m : nat) {struct n} : nat := end : forall T : Type, T -> nat -> nat -> nat +myplus is monomorphic Arguments are renamed to Z, t, n, m Argument Z is implicit and maximally inserted Argument scopes are [type_scope _ nat_scope nat_scope] myplus : forall T : Type, T -> nat -> nat -> nat +myplus is monomorphic Arguments are renamed to Z, t, n, m Argument Z is implicit and maximally inserted Argument scopes are [type_scope _ nat_scope nat_scope] @@ -70,6 +74,7 @@ For myEq: Argument scopes are [type_scope type_scope _ _] For myrefl: Argument scopes are [type_scope type_scope _ _] myrefl : forall (A B : Type) (x : A), B -> myEq A B x x +myrefl is monomorphic Arguments are renamed to A, C, x, _ Argument C is implicit and maximally inserted Argument scopes are [type_scope type_scope _ _] @@ -84,11 +89,13 @@ fix myplus (T : Type) (t : T) (n m : nat) {struct n} : nat := end : forall T : Type, T -> nat -> nat -> nat +myplus is monomorphic Arguments are renamed to Z, t, n, m Argument Z is implicit and maximally inserted Argument scopes are [type_scope _ nat_scope nat_scope] myplus : forall T : Type, T -> nat -> nat -> nat +myplus is monomorphic Arguments are renamed to Z, t, n, m Argument Z is implicit and maximally inserted Argument scopes are [type_scope _ nat_scope nat_scope] diff --git a/test-suite/output/Cases.out b/test-suite/output/Cases.out index be1bff48b..6515b368d 100644 --- a/test-suite/output/Cases.out +++ b/test-suite/output/Cases.out @@ -6,6 +6,8 @@ fix F (t : t) : P t := end : forall P : t -> Type, (let x := t in forall x0 : x, P x0 -> P (k x0)) -> forall t : t, P t + +t_rect is monomorphic proj = fun (x y : nat) (P : nat -> Type) (def : P x) (prf : P y) => match eq_nat_dec x y with @@ -16,6 +18,7 @@ match eq_nat_dec x y with end : forall (x y : nat) (P : nat -> Type), P x -> P y -> P y +proj is monomorphic Argument scopes are [nat_scope nat_scope _ _ _] foo = fix foo (A : Type) (l : list A) {struct l} : option A := @@ -26,6 +29,7 @@ fix foo (A : Type) (l : list A) {struct l} : option A := end : forall A : Type, list A -> option A +foo is monomorphic Argument scopes are [type_scope list_scope] uncast = fun (A : Type) (x : I A) => match x with @@ -33,9 +37,12 @@ fun (A : Type) (x : I A) => match x with end : forall A : Type, I A -> A +uncast is monomorphic Argument scopes are [type_scope _] foo' = if A 0 then true else false : bool + +foo' is monomorphic f = fun H : B => match H with @@ -46,3 +53,5 @@ match H with else fun _ : P false => Logic.I) x end : B -> True + +f is monomorphic diff --git a/test-suite/output/Errors.out b/test-suite/output/Errors.out index 839611b65..bcc37b635 100644 --- a/test-suite/output/Errors.out +++ b/test-suite/output/Errors.out @@ -4,4 +4,4 @@ The command has indeed failed with message: => Error: Unable to unify "nat" with "True". The command has indeed failed with message: => In nested Ltac calls to "f" and "apply x", last call failed. - Error: Unable to unify "nat" with "True". +Error: Unable to unify "nat" with "True". diff --git a/test-suite/output/Implicit.out b/test-suite/output/Implicit.out index 3b65003c2..d1cd5e84f 100644 --- a/test-suite/output/Implicit.out +++ b/test-suite/output/Implicit.out @@ -5,6 +5,7 @@ ex_intro (P:=fun _ : nat => True) (x:=0) I d2 = fun x : nat => d1 (y:=x) : forall x x0 : nat, x0 = x -> x0 = x +d2 is monomorphic Arguments x, x0 are implicit Argument scopes are [nat_scope nat_scope _] map id (1 :: nil) diff --git a/test-suite/output/PrintInfos.out b/test-suite/output/PrintInfos.out index e0fb7d5a9..62889f802 100644 --- a/test-suite/output/PrintInfos.out +++ b/test-suite/output/PrintInfos.out @@ -1,5 +1,6 @@ existT : forall (A : Type) (P : A -> Type) (x : A), P x -> {x : A & P x} +existT is template universe polymorphic Argument A is implicit Argument scopes are [type_scope _ _ _] Expands to: Constructor Coq.Init.Specif.existT @@ -24,6 +25,7 @@ For eq: Argument scopes are [type_scope _ _] For eq_refl: Argument scopes are [type_scope _] eq_refl : forall (A : Type) (x : A), x = x +eq_refl is monomorphic When applied to no arguments: Arguments A, x are implicit and maximally inserted When applied to 1 argument: @@ -44,9 +46,11 @@ fix plus (n m : nat) {struct n} : nat := end : nat -> nat -> nat +plus is monomorphic Argument scopes are [nat_scope nat_scope] plus : nat -> nat -> nat +plus is monomorphic Argument scopes are [nat_scope nat_scope] plus is transparent Expands to: Constant Coq.Init.Peano.plus @@ -54,6 +58,7 @@ plus : nat -> nat -> nat plus_n_O : forall n : nat, n = n + 0 +plus_n_O is monomorphic Argument scope is [nat_scope] plus_n_O is opaque Expands to: Constant Coq.Init.Peano.plus_n_O @@ -75,11 +80,13 @@ For le_n: Argument scope is [nat_scope] For le_S: Argument scopes are [nat_scope nat_scope _] comparison : Set +comparison is monomorphic Expands to: Inductive Coq.Init.Datatypes.comparison Inductive comparison : Set := Eq : comparison | Lt : comparison | Gt : comparison bar : foo +bar is monomorphic Expanded type for implicit arguments bar : forall x : nat, x = 0 @@ -87,12 +94,14 @@ Argument x is implicit and maximally inserted Expands to: Constant Top.bar *** [ bar : foo ] +bar is monomorphic Expanded type for implicit arguments bar : forall x : nat, x = 0 Argument x is implicit and maximally inserted bar : foo +bar is monomorphic Expanded type for implicit arguments bar : forall x : nat, x = 0 @@ -100,6 +109,7 @@ Argument x is implicit and maximally inserted Expands to: Constant Top.bar *** [ bar : foo ] +bar is monomorphic Expanded type for implicit arguments bar : forall x : nat, x = 0 diff --git a/test-suite/output/TranspModtype.out b/test-suite/output/TranspModtype.out index f94ed6423..dbbd73dcd 100644 --- a/test-suite/output/TranspModtype.out +++ b/test-suite/output/TranspModtype.out @@ -1,7 +1,15 @@ TrM.A = M.A : Set + +TrM.A is monomorphic OpM.A = M.A : Set + +OpM.A is monomorphic TrM.B = M.B : Set + +TrM.B is monomorphic *** [ OpM.B : Set ] + +OpM.B is monomorphic diff --git a/test-suite/output/inference.out b/test-suite/output/inference.out index a394c56dd..466faaccb 100644 --- a/test-suite/output/inference.out +++ b/test-suite/output/inference.out @@ -4,6 +4,8 @@ fun e : option L => match e with | None => None end : option L -> option L + +P is monomorphic fun (m n p : nat) (H : S m <= S n + p) => le_S_n m (n + p) H : forall m n p : nat, S m <= S n + p -> m <= n + p fun n : nat => let x := A n in ?12 ?15:T n diff --git a/test-suite/success/rewrite.v b/test-suite/success/rewrite.v index 08c406be9..0e1e77863 100644 --- a/test-suite/success/rewrite.v +++ b/test-suite/success/rewrite.v @@ -129,3 +129,12 @@ intros. Fail rewrite H in H0. Abort. +(* Test subst in the presence of a dependent let-in *) +(* Was not working prior to May 2014 *) + +Goal forall x y, x=y+0 -> let z := x+1 in x+1=y -> z=z -> z=x. +intros. +subst x. (* was failing *) +rewrite H0. +reflexivity. +Qed. diff --git a/theories/Classes/RelationClasses.v b/theories/Classes/RelationClasses.v index 61edb2b98..3bd9dcd12 100644 --- a/theories/Classes/RelationClasses.v +++ b/theories/Classes/RelationClasses.v @@ -202,6 +202,8 @@ Hint Extern 3 (PreOrder (flip _)) => class_apply flip_PreOrder : typeclass_insta Hint Extern 4 (subrelation (flip _) _) => class_apply @subrelation_symmetric : typeclass_instances. +Arguments irreflexivity {A R Irreflexive} [x] _. + Hint Resolve irreflexivity : ord. Unset Implicit Arguments. diff --git a/theories/Init/Logic.v b/theories/Init/Logic.v index f994b4ca6..e944d3f04 100644 --- a/theories/Init/Logic.v +++ b/theories/Init/Logic.v @@ -229,10 +229,6 @@ Notation "'IF' c1 'then' c2 'else' c3" := (IF_then_else c1 c2 c3) is provided too. *) -(** Remark: [exists x, Q] denotes [ex (fun x => Q)] so that [exists x, - P x] is in fact equivalent to [ex (fun x => P x)] which may be not - convertible to [ex P] if [P] is not itself an abstraction *) - Inductive ex (A:Type) (P:A -> Prop) : Prop := ex_intro : forall x:A, P x -> ex (A:=A) P. diff --git a/theories/MSets/MSetInterface.v b/theories/MSets/MSetInterface.v index a61ef8bcd..bd8811689 100644 --- a/theories/MSets/MSetInterface.v +++ b/theories/MSets/MSetInterface.v @@ -595,7 +595,7 @@ Module Raw2SetsOn (O:OrderedType)(M:RawSets O) <: SetsOn O. (** Specification of [lt] *) Instance lt_strorder : StrictOrder lt. Proof. constructor ; unfold lt; red. - unfold complement. red. intros. apply (irreflexivity _ H). + unfold complement. red. intros. apply (irreflexivity H). intros. transitivity y; auto. Qed. diff --git a/theories/Structures/OrderedType.v b/theories/Structures/OrderedType.v index fb28e0cfc..fa08f9366 100644 --- a/theories/Structures/OrderedType.v +++ b/theories/Structures/OrderedType.v @@ -328,7 +328,7 @@ Module KeyOrderedType(O:OrderedType). Proof. split; eauto. Qed. Global Instance ltk_strorder : StrictOrder ltk. - Proof. constructor; eauto. intros x; apply (irreflexivity (fst x)). Qed. + Proof. constructor; eauto. intros x; apply (irreflexivity (x:=fst x)). Qed. Global Instance ltk_compat : Proper (eqk==>eqk==>iff) ltk. Proof. diff --git a/toplevel/auto_ind_decl.ml b/toplevel/auto_ind_decl.ml index 5129beeab..de0459089 100644 --- a/toplevel/auto_ind_decl.ml +++ b/toplevel/auto_ind_decl.ml @@ -78,12 +78,12 @@ let sumbool = Coqlib.build_coq_sumbool let andb = fun _ -> (Coqlib.build_bool_type()).Coqlib.andb let induct_on c = - new_induct false + induction false [Tacexpr.ElimOnConstr (Evd.empty,(c,NoBindings))] None (None,None) None let destruct_on_using c id = - new_destruct false + destruct false [Tacexpr.ElimOnConstr (Evd.empty,(c,NoBindings))] None (None,Some (dl,IntroOrAndPattern [ @@ -92,7 +92,7 @@ let destruct_on_using c id = None let destruct_on c = - new_destruct false + destruct false [Tacexpr.ElimOnConstr (Evd.empty,(c,NoBindings))] None (None,None) None @@ -592,7 +592,7 @@ repeat ( apply andb_prop in z;let z1:= fresh "Z" in destruct z as [z1 z]). apply_in false false freshz [Loc.ghost, (andb_prop(), NoBindings)] None; Proofview.Goal.enter begin fun gl -> let fresht = fresh_id (Id.of_string "Z") gl in - (new_destruct false [Tacexpr.ElimOnConstr + (destruct false [Tacexpr.ElimOnConstr (Evd.empty,((mkVar freshz,NoBindings)))] None (None, Some (dl,IntroOrAndPattern [[ |