From 3e96002677226c0cdaa8f355938a76cfb37a722a Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Thu, 14 Oct 2010 17:51:11 +0200 Subject: Imported Upstream version 8.3 --- tactics/auto.ml | 11 ++++---- tactics/evar_tactics.ml | 5 ++-- tactics/extratactics.ml4 | 7 +++++- tactics/rewrite.ml4 | 47 +++++++++++++++++----------------- tactics/tacinterp.ml | 25 +++++++++++-------- tactics/tactics.ml | 65 +++++++++++++++++++++++------------------------- 6 files changed, 84 insertions(+), 76 deletions(-) (limited to 'tactics') diff --git a/tactics/auto.ml b/tactics/auto.ml index faf0482b..ca2f4916 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: auto.ml 13323 2010-07-24 15:57:30Z herbelin $ *) +(* $Id: auto.ml 13390 2010-09-02 08:03:01Z herbelin $ *) open Pp open Util @@ -706,12 +706,11 @@ let print_applicable_hint () = (* displays the whole hint database db *) let print_hint_db db = let (ids, csts) = Hint_db.transparent_state db in - msg (hov 0 + msgnl (hov 0 ((if Hint_db.use_dn db then str"Discriminated database" - else str"Non-discriminated database") ++ fnl ())); - msg (hov 0 - (str"Unfoldable variable definitions: " ++ pr_idpred ids ++ fnl () ++ - str"Unfoldable constant definitions: " ++ pr_cpred csts ++ fnl ())); + else str"Non-discriminated database"))); + msgnl (hov 2 (str"Unfoldable variable definitions: " ++ pr_idpred ids)); + msgnl (hov 2 (str"Unfoldable constant definitions: " ++ pr_cpred csts)); Hint_db.iter (fun head hintlist -> match head with diff --git a/tactics/evar_tactics.ml b/tactics/evar_tactics.ml index 3e2191d1..825ec492 100644 --- a/tactics/evar_tactics.ml +++ b/tactics/evar_tactics.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: evar_tactics.ml 13323 2010-07-24 15:57:30Z herbelin $ *) +(* $Id: evar_tactics.ml 13428 2010-09-17 18:03:40Z herbelin $ *) open Term open Util @@ -53,7 +53,8 @@ let instantiate n (ist,rawc) ido gl = gl let let_evar name typ gls = - let sigma',evar = Evarutil.new_evar gls.sigma (pf_env gls) typ in + let src = (dummy_loc,GoalEvar) in + let sigma',evar = Evarutil.new_evar gls.sigma (pf_env gls) ~src typ in Refiner.tclTHEN (Refiner.tclEVARS sigma') (Tactics.letin_tac None name evar None nowhere) gls diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4 index e1ac42c2..3f069ab2 100644 --- a/tactics/extratactics.ml4 +++ b/tactics/extratactics.ml4 @@ -8,7 +8,7 @@ (*i camlp4deps: "parsing/grammar.cma" i*) -(* $Id: extratactics.ml4 13323 2010-07-24 15:57:30Z herbelin $ *) +(* $Id: extratactics.ml4 13434 2010-09-18 20:11:37Z msozeau $ *) open Pp open Pcoq @@ -624,3 +624,8 @@ TACTIC EXTEND hget_evar END (**********************************************************************) + +TACTIC EXTEND constr_eq +| [ "constr_eq" constr(x) constr(y) ] -> [ + if eq_constr x y then tclIDTAC else tclFAIL 0 (str "Not equal") ] +END diff --git a/tactics/rewrite.ml4 b/tactics/rewrite.ml4 index 9d99ad96..d8497a7d 100644 --- a/tactics/rewrite.ml4 +++ b/tactics/rewrite.ml4 @@ -431,29 +431,30 @@ let pointwise_or_dep_relation n t car rel = [| t; mkLambda (n, t, car); mkLambda (n, t, rel) |]) let lift_cstr env sigma evars (args : constr list) ty cstr = - let cstr = - let start env car = - match cstr with - | None | Some (_, None) -> - Evarutil.e_new_evar evars env (mk_relation car) - | Some (ty, Some rel) -> rel - in - let rec aux env prod n = - if n = 0 then start env prod - else - match kind_of_term (Reduction.whd_betadeltaiota env prod) with - | Prod (na, ty, b) -> - if noccurn 1 b then - let b' = lift (-1) b in - let rb = aux env b' (pred n) in - mkApp (Lazy.force pointwise_relation, [| ty; b'; rb |]) - else - let rb = aux (Environ.push_rel (na, None, ty) env) b (pred n) in - mkApp (Lazy.force forall_relation, - [| ty; mkLambda (na, ty, b); mkLambda (na, ty, rb) |]) - | _ -> assert false - in aux env ty (List.length args) - in Some (ty, cstr) + let start env car = + match cstr with + | None | Some (_, None) -> + Evarutil.e_new_evar evars env (mk_relation car) + | Some (ty, Some rel) -> rel + in + let rec aux env prod n args = + if n = 0 then Some (start env prod) + else + match kind_of_term (Reduction.whd_betadeltaiota env prod) with + | Prod (na, ty, b) -> + if noccurn 1 b then + let b' = lift (-1) b in + let rb = aux env b' (pred n) (List.tl args) in + Option.map (fun rb -> mkApp (Lazy.force pointwise_relation, [| ty; b'; rb |])) + rb + else + let rb = aux (Environ.push_rel (na, None, ty) env) b (pred n) (List.tl args) in + Option.map + (fun rb -> mkApp (Lazy.force forall_relation, + [| ty; mkLambda (na, ty, b); mkLambda (na, ty, rb) |])) + rb + | _ -> None + in Option.map (fun rel -> (ty, rel)) (aux env ty (List.length args) args) let unlift_cstr env sigma = function | None -> None diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index 95e44c40..ba9a5173 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: tacinterp.ml 13360 2010-07-30 08:47:08Z herbelin $ *) +(* $Id: tacinterp.ml 13489 2010-10-03 22:27:12Z herbelin $ *) open Constrintern open Closure @@ -401,8 +401,10 @@ let intern_ltac_variable ist = function raise Not_found let intern_constr_reference strict ist = function - | Ident (_,id) when (not strict & find_hyp id ist) or find_ctxvar id ist -> - RVar (dloc,id), None + | Ident (_,id) as r when not strict & find_hyp id ist -> + RVar (dloc,id), Some (CRef r) + | Ident (_,id) as r when find_ctxvar id ist -> + RVar (dloc,id), if strict then None else Some (CRef r) | r -> let loc,_ as lqid = qualid_of_reference r in RRef (loc,locate_global_with_alias lqid), if strict then None else Some (CRef r) @@ -564,9 +566,10 @@ let intern_evaluable_reference_or_by_notation ist = function (* Globalize a reduction expression *) let intern_evaluable ist = function | AN (Ident (loc,id)) when find_ltacvar id ist -> ArgVar (loc,id) - | AN (Ident (_,id)) when - (not !strict_check & find_hyp id ist) or find_ctxvar id ist -> - ArgArg (EvalVarRef id, None) + | AN (Ident (loc,id)) when not !strict_check & find_hyp id ist -> + ArgArg (EvalVarRef id, Some (loc,id)) + | AN (Ident (loc,id)) when find_ctxvar id ist -> + ArgArg (EvalVarRef id, if !strict_check then None else Some (loc,id)) | r -> let e = intern_evaluable_reference_or_by_notation ist r in let na = short_name r in @@ -1138,7 +1141,8 @@ let interp_hyp ist gl (loc,id as locid) = with Not_found -> (* Then look if bound in the proof context at calling time *) if is_variable env id then id - else user_err_loc (loc,"eval_variable",pr_id id ++ str " not found.") + else user_err_loc (loc,"eval_variable", + str "No such hypothesis: " ++ pr_id id ++ str ".") let hyp_list_of_VList env = function | VList l -> List.map (coerce_to_hyp env) l @@ -1210,7 +1214,7 @@ let interp_evaluable ist env = function with Not_found -> match r with | EvalConstRef _ -> r - | _ -> Pretype_errors.error_var_not_found_loc loc id) + | _ -> error_global_not_found_loc (loc,qualid_of_ident id)) | ArgArg (r,None) -> r | ArgVar locid -> interp_ltac_var (coerce_to_evaluable_ref env) ist (Some env) locid @@ -1616,8 +1620,9 @@ let interp_induction_arg ist gl sigma arg = let env = pf_env gl in match arg with | ElimOnConstr c -> - let sigma, c = interp_constr_with_bindings ist env sigma c in - sigma, ElimOnConstr c + let sigma', (c,b) = interp_constr_with_bindings ist env sigma c in + let sigma, c = solve_remaining_evars false true env sigma sigma' c in + sigma, ElimOnConstr (c,b) | ElimOnAnonHyp n as x -> sigma, x | ElimOnIdent (loc,id) -> try diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 9e4be0af..4ecc4739 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: tactics.ml 13332 2010-07-26 22:12:43Z msozeau $ *) +(* $Id: tactics.ml 13464 2010-09-24 22:23:02Z herbelin $ *) open Pp open Util @@ -868,13 +868,18 @@ type conjunction_status = | DefinedRecord of constant option list | NotADefinedRecordUseScheme of constr -let make_projection params cstr sign elim i n c = +let make_projection sigma params cstr sign elim i n c = let elim = match elim with | NotADefinedRecordUseScheme elim -> let (na,b,t) = List.nth cstr.cs_args i in let b = match b with None -> mkRel (i+1) | Some b -> b in let branch = it_mkLambda_or_LetIn b cstr.cs_args in - if noccur_between 1 (n-i-1) t then + if + (* excludes dependent projection types *) + noccur_between 1 (n-i-1) t + (* excludes flexible projection types *) + && not (isEvar (fst (whd_betaiota_stack sigma t))) + then let t = lift (i+1-n) t in Some (beta_applist (elim,params@[t;branch]),t) else @@ -883,7 +888,8 @@ let make_projection params cstr sign elim i n c = match List.nth l i with | Some proj -> let t = Typeops.type_of_constant (Global.env()) proj in - Some (beta_applist (mkConst proj,params),prod_applist t (params@[c])) + let args = extended_rel_vect 0 sign in + Some (beta_applist (mkConst proj,params),prod_applist t (params@[mkApp (c,args)])) | None -> None in Option.map (fun (abselim,elimt) -> let c = beta_applist (abselim,[mkApp (c,extended_rel_vect 0 sign)]) in @@ -908,7 +914,7 @@ let descend_in_conjunctions tac exit c gl = NotADefinedRecordUseScheme elim in tclFIRST (list_tabulate (fun i gl -> - match make_projection params cstr sign elim i n c with + match make_projection (project gl) params cstr sign elim i n c with | None -> tclFAIL 0 (mt()) gl | Some (p,pt) -> tclTHENS @@ -2188,6 +2194,8 @@ let coq_eq_refl = lazy ((Coqlib.build_coq_eq_data ()).Coqlib.refl) 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 coq_block = lazy (Coqlib.coq_constant "tactics" ["Program";"Equality"] "block") + let mkEq t x y = mkApp (Lazy.force coq_eq, [| refresh_universes_strict t; x; y |]) @@ -2303,23 +2311,6 @@ let hyps_of_vars env sign nogen hyps = sign in lh -exception Seen - -let linear vars args = - let seen = ref vars in - try - Array.iter (fun i -> - let rels = ids_of_constr ~all:true Idset.empty i in - let seen' = - Idset.fold (fun id acc -> - if Idset.mem id acc then raise Seen - else Idset.add id acc) - rels !seen - in seen := seen') - args; - true - with Seen -> false - let is_defined_variable env id = pi2 (lookup_named id env) <> None @@ -2373,19 +2364,23 @@ let abstract_args gl generalize_vars dep id defined f args = nongenvars, Idset.union argvars vars, env) in let f', args' = decompose_indapp f args in + let parvars = ids_of_constr ~all:true Idset.empty f' in let dogen, f', args' = - let parvars = ids_of_constr ~all:true Idset.empty f' in - if not (linear parvars args') then true, f, args - else - match array_find_i (fun i x -> not (isVar x) || is_defined_variable env (destVar x)) args' with - | None -> false, f', args' - | Some nonvar -> - let before, after = array_chop nonvar args' in - true, mkApp (f', before), after + let seen = ref parvars in + let find i x = not (isVar x) || + let v = destVar x in + if is_defined_variable env v || Idset.mem v !seen then true + else (seen := Idset.add v !seen; false) + in + match array_find_i find args' with + | None -> false, f', args' + | Some nonvar -> + let before, after = array_chop nonvar args' in + true, mkApp (f', before), after in if dogen then let arity, ctx, ctxenv, c', args, eqs, refls, nogen, vars, env = - Array.fold_left aux (pf_type_of gl f',[],env,f',[],[],[],Idset.empty,Idset.empty,env) args' + Array.fold_left aux (pf_type_of gl f',[],env,f',[],[],[],parvars,Idset.empty,env) args' in let args, refls = List.rev args, List.rev refls in let vars = @@ -2440,14 +2435,14 @@ let specialize_eqs id gl = match kind_of_term ty with | Prod (na, t, b) -> (match kind_of_term t with - | App (eq, [| eqty; x; y |]) when eq_constr eq (Lazy.force coq_eq) -> + | App (eq, [| eqty; x; y |]) when in_eqs && eq_constr eq (Lazy.force coq_eq) -> let c = if noccur_between 1 (List.length ctx) x then y else x in let pt = mkApp (Lazy.force coq_eq, [| eqty; c; c |]) in let p = mkApp (Lazy.force coq_eq_refl, [| eqty; c |]) in 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 - | App (heq, [| eqty; x; eqty'; y |]) when eq_constr heq (Lazy.force coq_heq) -> + | App (heq, [| eqty; x; eqty'; y |]) when in_eqs && eq_constr heq (Lazy.force coq_heq) -> let eqt, c = if noccur_between 1 (List.length ctx) x then eqty', y else eqty, x in let pt = mkApp (Lazy.force coq_heq, [| eqt; c; eqt; c |]) in let p = mkApp (Lazy.force coq_heq_refl, [| eqt; c |]) in @@ -2459,8 +2454,10 @@ let specialize_eqs id gl = 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) + | App (f, args) when eq_constr f (Lazy.force coq_block) && not in_eqs -> + aux true ctx acc args.(1) | 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) -> -- cgit v1.2.3