From e1010899051546467b790bca0409174bde824270 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sat, 26 Nov 2016 00:36:34 +0100 Subject: Omega API using EConstr. --- plugins/omega/coq_omega.ml | 252 ++++++++++++++++++++++++--------------------- 1 file changed, 136 insertions(+), 116 deletions(-) (limited to 'plugins/omega/coq_omega.ml') diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml index 665486272..9e0d591b6 100644 --- a/plugins/omega/coq_omega.ml +++ b/plugins/omega/coq_omega.ml @@ -18,6 +18,7 @@ open Util open Names open Nameops open Term +open EConstr open Tacticals open Tacmach open Tactics @@ -149,7 +150,7 @@ let mk_then = tclTHENLIST let exists_tac c = constructor_tac false (Some 1) 1 (ImplicitBindings [c]) -let generalize_tac t = generalize (List.map EConstr.of_constr t) +let generalize_tac t = generalize t let elim t = simplest_elim t let exact t = Tacmach.refine t let unfold s = Tactics.unfold_in_concl [Locus.AllOccurrences, Lazy.force s] @@ -172,8 +173,8 @@ let tag_hypothesis,tag_of_hyp, hyp_of_tag, clear_tags = let hide_constr,find_constr,clear_constr_tables,dump_tables = let l = ref ([]:(constr * (Id.t * Id.t * bool)) list) in (fun h id eg b -> l := (h,(id,eg,b)):: !l), - (fun h -> - try List.assoc_f eq_constr_nounivs h !l with Not_found -> failwith "find_contr"), + (fun sigma h -> + try List.assoc_f (eq_constr_nounivs sigma) h !l with Not_found -> failwith "find_contr"), (fun () -> l := []), (fun () -> !l) @@ -197,6 +198,7 @@ let coq_modules = init_modules @arith_modules @ [logic_dir] @ zarith_base_modules @ [["Coq"; "omega"; "OmegaLemmas"]] +let gen_constant_in_modules n m s = EConstr.of_constr (gen_constant_in_modules n m s) let init_constant = gen_constant_in_modules "Omega" init_modules let constant = gen_constant_in_modules "Omega" coq_modules @@ -348,11 +350,18 @@ let coq_not_iff = lazy (constant "not_iff") let coq_not_not = lazy (constant "not_not") let coq_imp_simp = lazy (constant "imp_simp") let coq_iff = lazy (constant "iff") +let coq_not = lazy (init_constant "not") +let coq_and = lazy (init_constant "and") +let coq_or = lazy (init_constant "or") +let coq_eq = lazy (init_constant "eq") +let coq_ex = lazy (init_constant "ex") +let coq_False = lazy (init_constant "False") +let coq_True = lazy (init_constant "True") (* uses build_coq_and, build_coq_not, build_coq_or, build_coq_ex *) (* For unfold *) -let evaluable_ref_of_constr s c = match kind_of_term (Lazy.force c) with +let evaluable_ref_of_constr s c = match EConstr.kind Evd.empty (Lazy.force c) with | Const (kn,u) when Tacred.is_evaluable (Global.env()) (EvalConstRef kn) -> EvalConstRef kn | _ -> anomaly ~label:"Coq_omega" (Pp.str (s^" is not an evaluable constant")) @@ -364,21 +373,21 @@ let sp_Zle = lazy (evaluable_ref_of_constr "Z.le" coq_Zle) let sp_Zgt = lazy (evaluable_ref_of_constr "Z.gt" coq_Zgt) let sp_Zge = lazy (evaluable_ref_of_constr "Z.ge" coq_Zge) let sp_Zlt = lazy (evaluable_ref_of_constr "Z.lt" coq_Zlt) -let sp_not = lazy (evaluable_ref_of_constr "not" (lazy (build_coq_not ()))) +let sp_not = lazy (evaluable_ref_of_constr "not" coq_not) let mk_var v = mkVar (Id.of_string v) let mk_plus t1 t2 = mkApp (Lazy.force coq_Zplus, [| t1; t2 |]) let mk_times t1 t2 = mkApp (Lazy.force coq_Zmult, [| t1; t2 |]) let mk_minus t1 t2 = mkApp (Lazy.force coq_Zminus, [| t1;t2 |]) -let mk_eq t1 t2 = mkApp (Universes.constr_of_global (build_coq_eq ()), +let mk_eq t1 t2 = mkApp (Lazy.force coq_eq, [| Lazy.force coq_Z; t1; t2 |]) let mk_le t1 t2 = mkApp (Lazy.force coq_Zle, [| t1; t2 |]) -let mk_gt t1 t2 = EConstr.of_constr (mkApp (Lazy.force coq_Zgt, [| t1; t2 |])) +let mk_gt t1 t2 = mkApp (Lazy.force coq_Zgt, [| t1; t2 |]) let mk_inv t = mkApp (Lazy.force coq_Zopp, [| t |]) -let mk_and t1 t2 = mkApp (build_coq_and (), [| t1; t2 |]) -let mk_or t1 t2 = mkApp (build_coq_or (), [| t1; t2 |]) -let mk_not t = mkApp (build_coq_not (), [| t |]) -let mk_eq_rel t1 t2 = mkApp (Universes.constr_of_global (build_coq_eq ()), +let mk_and t1 t2 = mkApp (Lazy.force coq_and, [| t1; t2 |]) +let mk_or t1 t2 = mkApp (Lazy.force coq_or, [| t1; t2 |]) +let mk_not t = mkApp (Lazy.force coq_not, [| t |]) +let mk_eq_rel t1 t2 = mkApp (Lazy.force coq_eq, [| Lazy.force coq_comparison; t1; t2 |]) let mk_inj t = mkApp (Lazy.force coq_Z_of_nat, [| t |]) @@ -420,22 +429,23 @@ type result = the term parts that we manipulate, but rather Var's. Said otherwise: all constr manipulated here are closed *) -let destructurate_prop t = - let c, args = decompose_app t in - match kind_of_term c, args with - | _, [_;_;_] when is_global (build_coq_eq ()) c -> Kapp (Eq,args) +let destructurate_prop sigma t = + let eq_constr c1 c2 = eq_constr sigma c1 c2 in + let c, args = decompose_app sigma t in + match EConstr.kind sigma c, args with + | _, [_;_;_] when eq_constr (Lazy.force coq_eq) c -> Kapp (Eq,args) | _, [_;_] when eq_constr c (Lazy.force coq_neq) -> Kapp (Neq,args) | _, [_;_] when eq_constr c (Lazy.force coq_Zne) -> Kapp (Zne,args) | _, [_;_] when eq_constr c (Lazy.force coq_Zle) -> Kapp (Zle,args) | _, [_;_] when eq_constr c (Lazy.force coq_Zlt) -> Kapp (Zlt,args) | _, [_;_] when eq_constr c (Lazy.force coq_Zge) -> Kapp (Zge,args) | _, [_;_] when eq_constr c (Lazy.force coq_Zgt) -> Kapp (Zgt,args) - | _, [_;_] when eq_constr c (build_coq_and ()) -> Kapp (And,args) - | _, [_;_] when eq_constr c (build_coq_or ()) -> Kapp (Or,args) + | _, [_;_] when eq_constr c (Lazy.force coq_and) -> Kapp (And,args) + | _, [_;_] when eq_constr c (Lazy.force coq_or) -> Kapp (Or,args) | _, [_;_] when eq_constr c (Lazy.force coq_iff) -> Kapp (Iff, args) - | _, [_] when eq_constr c (build_coq_not ()) -> Kapp (Not,args) - | _, [] when eq_constr c (build_coq_False ()) -> Kapp (False,args) - | _, [] when eq_constr c (build_coq_True ()) -> Kapp (True,args) + | _, [_] when eq_constr c (Lazy.force coq_not) -> Kapp (Not,args) + | _, [] when eq_constr c (Lazy.force coq_False) -> Kapp (False,args) + | _, [] when eq_constr c (Lazy.force coq_True) -> Kapp (True,args) | _, [_;_] when eq_constr c (Lazy.force coq_le) -> Kapp (Le,args) | _, [_;_] when eq_constr c (Lazy.force coq_lt) -> Kapp (Lt,args) | _, [_;_] when eq_constr c (Lazy.force coq_ge) -> Kapp (Ge,args) @@ -451,16 +461,18 @@ let destructurate_prop t = | Prod (Name _,_,_),[] -> error "Omega: Not a quantifier-free goal" | _ -> Kufo -let destructurate_type t = - let c, args = decompose_app t in - match kind_of_term c, args with +let destructurate_type sigma t = + let eq_constr c1 c2 = eq_constr sigma c1 c2 in + let c, args = decompose_app sigma t in + match EConstr.kind sigma c, args with | _, [] when eq_constr c (Lazy.force coq_Z) -> Kapp (Z,args) | _, [] when eq_constr c (Lazy.force coq_nat) -> Kapp (Nat,args) | _ -> Kufo -let destructurate_term t = - let c, args = decompose_app t in - match kind_of_term c, args with +let destructurate_term sigma t = + let eq_constr c1 c2 = eq_constr sigma c1 c2 in + let c, args = decompose_app sigma t in + match EConstr.kind sigma c, args with | _, [_;_] when eq_constr c (Lazy.force coq_Zplus) -> Kapp (Zplus,args) | _, [_;_] when eq_constr c (Lazy.force coq_Zmult) -> Kapp (Zmult,args) | _, [_;_] when eq_constr c (Lazy.force coq_Zminus) -> Kapp (Zminus,args) @@ -480,15 +492,16 @@ let destructurate_term t = | Var id,[] -> Kvar id | _ -> Kufo -let recognize_number t = +let recognize_number sigma t = + let eq_constr c1 c2 = eq_constr sigma c1 c2 in let rec loop t = - match decompose_app t with + match decompose_app sigma t with | f, [t] when eq_constr f (Lazy.force coq_xI) -> one + two * loop t | f, [t] when eq_constr f (Lazy.force coq_xO) -> two * loop t | f, [] when eq_constr f (Lazy.force coq_xH) -> one | _ -> failwith "not a number" in - match decompose_app t with + match decompose_app sigma t with | f, [t] when eq_constr f (Lazy.force coq_Zpos) -> loop t | f, [t] when eq_constr f (Lazy.force coq_Zneg) -> neg (loop t) | f, [] when eq_constr f (Lazy.force coq_Z0) -> zero @@ -504,9 +517,9 @@ type constr_path = | P_ARITY | P_ARG -let context operation path (t : constr) = +let context sigma operation path (t : constr) = let rec loop i p0 t = - match (p0,kind_of_term t) with + match (p0,EConstr.kind sigma t) with | (p, Cast (c,k,t)) -> mkCast (loop i p c,k,t) | ([], _) -> operation i t | ((P_APP n :: p), App (f,v)) -> @@ -517,7 +530,7 @@ let context operation path (t : constr) = let v' = Array.copy v in v'.(n) <- loop i p v'.(n); (mkCase (ci,q,c,v')) | ((P_ARITY :: p), App (f,l)) -> - appvect (loop i p f,l) + mkApp (loop i p f,l) | ((P_ARG :: p), App (f,v)) -> let v' = Array.copy v in v'.(0) <- loop i p v'.(0); mkApp (f,v') @@ -542,8 +555,8 @@ let context operation path (t : constr) = in loop 1 path t -let occurrence path (t : constr) = - let rec loop p0 t = match (p0,kind_of_term t) with +let occurrence sigma path (t : constr) = + let rec loop p0 t = match (p0,EConstr.kind sigma t) with | (p, Cast (c,_,_)) -> loop p c | ([], _) -> t | ((P_APP n :: p), App (f,v)) -> loop p v.(pred n) @@ -562,14 +575,13 @@ let occurrence path (t : constr) = in loop path t -let abstract_path typ path t = +let abstract_path sigma typ path t = let term_occur = ref (mkRel 0) in - let abstract = context (fun i t -> term_occur:= t; mkRel i) path t in + let abstract = context sigma (fun i t -> term_occur:= t; mkRel i) path t in mkLambda (Name (Id.of_string "x"), typ, abstract), !term_occur let focused_simpl path gl = - let newc = context (fun i t -> EConstr.Unsafe.to_constr (pf_nf gl (EConstr.of_constr t))) (List.rev path) (EConstr.Unsafe.to_constr (pf_concl gl)) in - let newc = EConstr.of_constr newc in + let newc = context (project gl) (fun i t -> pf_nf gl t) (List.rev path) (pf_concl gl) in Proofview.V82.of_tactic (convert_concl_no_check newc DEFAULTcast) gl let focused_simpl path = focused_simpl path @@ -632,8 +644,7 @@ let mkNewMeta () = mkMeta (Evarutil.new_meta()) let clever_rewrite_base_poly typ p result theorem gl = let full = pf_concl gl in - let full = EConstr.Unsafe.to_constr full in - let (abstracted,occ) = abstract_path typ (List.rev p) full in + let (abstracted,occ) = abstract_path (project gl) typ (List.rev p) full in let t = applist (mkLambda @@ -646,7 +657,7 @@ let clever_rewrite_base_poly typ p result theorem gl = [| typ; result; mkRel 2; mkRel 1; occ; theorem |]))), [abstracted]) in - exact (EConstr.of_constr (applist(t,[mkNewMeta()]))) gl + exact (applist(t,[mkNewMeta()])) gl let clever_rewrite_base p result theorem gl = clever_rewrite_base_poly (Lazy.force coq_Z) p result theorem gl @@ -664,11 +675,10 @@ let clever_rewrite_gen_nat p result (t,args) = let clever_rewrite p vpath t gl = let full = pf_concl gl in - let full = EConstr.Unsafe.to_constr full in - let (abstracted,occ) = abstract_path (Lazy.force coq_Z) (List.rev p) full in - let vargs = List.map (fun p -> occurrence p occ) vpath in + let (abstracted,occ) = abstract_path (project gl) (Lazy.force coq_Z) (List.rev p) full in + let vargs = List.map (fun p -> occurrence (project gl) p occ) vpath in let t' = applist(t, (vargs @ [abstracted])) in - exact (EConstr.of_constr (applist(t',[mkNewMeta()]))) gl + exact (applist(t',[mkNewMeta()])) gl let rec shuffle p (t1,t2) = match t1,t2 with @@ -910,10 +920,10 @@ let rec negate p = function | Oz i -> [focused_simpl p],Oz(neg i) | Oufo c -> [], Oufo (mkApp (Lazy.force coq_Zopp, [| c |])) -let rec transform p t = +let rec transform sigma p t = let default isnat t' = try - let v,th,_ = find_constr t' in + let v,th,_ = find_constr sigma t' in [clever_rewrite_base p (mkVar v) (mkVar th)], Oatom v with e when CErrors.noncritical e -> let v = new_identifier_var () @@ -921,29 +931,29 @@ let rec transform p t = hide_constr t' v th isnat; [clever_rewrite_base p (mkVar v) (mkVar th)], Oatom v in - try match destructurate_term t with + try match destructurate_term sigma t with | Kapp(Zplus,[t1;t2]) -> - let tac1,t1' = transform (P_APP 1 :: p) t1 - and tac2,t2' = transform (P_APP 2 :: p) t2 in + let tac1,t1' = transform sigma (P_APP 1 :: p) t1 + and tac2,t2' = transform sigma (P_APP 2 :: p) t2 in let tac,t' = shuffle p (t1',t2') in tac1 @ tac2 @ tac, t' | Kapp(Zminus,[t1;t2]) -> let tac,t = - transform p + transform sigma p (mkApp (Lazy.force coq_Zplus, [| t1; (mkApp (Lazy.force coq_Zopp, [| t2 |])) |])) in Proofview.V82.of_tactic (unfold sp_Zminus) :: tac,t | Kapp(Zsucc,[t1]) -> - let tac,t = transform p (mkApp (Lazy.force coq_Zplus, + let tac,t = transform sigma p (mkApp (Lazy.force coq_Zplus, [| t1; mk_integer one |])) in Proofview.V82.of_tactic (unfold sp_Zsucc) :: tac,t | Kapp(Zpred,[t1]) -> - let tac,t = transform p (mkApp (Lazy.force coq_Zplus, + let tac,t = transform sigma p (mkApp (Lazy.force coq_Zplus, [| t1; mk_integer negone |])) in Proofview.V82.of_tactic (unfold sp_Zpred) :: tac,t | Kapp(Zmult,[t1;t2]) -> - let tac1,t1' = transform (P_APP 1 :: p) t1 - and tac2,t2' = transform (P_APP 2 :: p) t2 in + let tac1,t1' = transform sigma (P_APP 1 :: p) t1 + and tac2,t2' = transform sigma (P_APP 2 :: p) t2 in begin match t1',t2' with | (_,Oz n) -> let tac,t' = scalar p n t1' in tac1 @ tac2 @ tac,t' | (Oz n,_) -> @@ -954,11 +964,11 @@ let rec transform p t = | _ -> default false t end | Kapp((Zpos|Zneg|Z0),_) -> - (try ([],Oz(recognize_number t)) + (try ([],Oz(recognize_number sigma t)) with e when CErrors.noncritical e -> default false t) | Kvar s -> [],Oatom s | Kapp(Zopp,[t]) -> - let tac,t' = transform (P_APP 1 :: p) t in + let tac,t' = transform sigma (P_APP 1 :: p) t in let tac',t'' = negate p t' in tac @ tac', t'' | Kapp(Z_of_nat,[t']) -> default true t' @@ -1088,13 +1098,12 @@ let replay_history tactic_normalisation = let p_initial = [P_APP 2;P_TYPE] in let tac = shuffle_cancel p_initial e1.body in let solve_le = - let not_sup_sup = mkApp (Universes.constr_of_global (build_coq_eq ()), + let not_sup_sup = mkApp (Lazy.force coq_eq, [| Lazy.force coq_comparison; Lazy.force coq_Gt; Lazy.force coq_Gt |]) in - let not_sup_sup = EConstr.of_constr not_sup_sup in Tacticals.New.tclTHENS (Tacticals.New.tclTHENLIST [ unfold sp_Zle; @@ -1120,7 +1129,7 @@ let replay_history tactic_normalisation = let state_eg = mk_eq eq1 rhs in let tac = scalar_norm_add [P_APP 3] e2.body in Tacticals.New.tclTHENS - (cut (EConstr.of_constr state_eg)) + (cut state_eg) [ Tacticals.New.tclTHENS (Tacticals.New.tclTHENLIST [ (intros_using [aux]); @@ -1189,7 +1198,7 @@ let replay_history tactic_normalisation = if e1.kind == DISE then let tac = scalar_norm [P_APP 3] e2.body in Tacticals.New.tclTHENS - (cut (EConstr.of_constr state_eq)) + (cut state_eq) [Tacticals.New.tclTHENLIST [ (intros_using [aux1]); (generalize_tac @@ -1201,7 +1210,7 @@ let replay_history tactic_normalisation = Tacticals.New.tclTHEN (Proofview.V82.tactic (mk_then tac)) reflexivity ] else let tac = scalar_norm [P_APP 3] e2.body in - Tacticals.New.tclTHENS (cut (EConstr.of_constr state_eq)) + Tacticals.New.tclTHENS (cut state_eq) [ Tacticals.New.tclTHENS (cut (mk_gt kk izero)) @@ -1231,7 +1240,7 @@ let replay_history tactic_normalisation = scalar_norm [P_APP 3] e1.body in Tacticals.New.tclTHENS - (cut (EConstr.of_constr (mk_eq eq1 (mk_inv eq2)))) + (cut (mk_eq eq1 (mk_inv eq2))) [Tacticals.New.tclTHENLIST [ (intros_using [aux]); (generalize_tac [mkApp (Lazy.force coq_OMEGA8, @@ -1249,7 +1258,7 @@ let replay_history tactic_normalisation = and eq2 = val_of(decompile orig) in let vid = unintern_id v in let theorem = - mkApp (build_coq_ex (), [| + mkApp (Lazy.force coq_ex, [| Lazy.force coq_Z; mkLambda (Name vid, @@ -1264,7 +1273,7 @@ let replay_history tactic_normalisation = shuffle_mult_right p_initial orig.body m ({c= negone;v= v}::def.body) in Tacticals.New.tclTHENS - (cut (EConstr.of_constr theorem)) + (cut theorem) [Tacticals.New.tclTHENLIST [ (intros_using [aux]); (elim_id aux); @@ -1277,7 +1286,7 @@ let replay_history tactic_normalisation = (clear [aux]); (intros_using [id]); (loop l) ]; - Tacticals.New.tclTHEN (exists_tac (EConstr.of_constr eq1)) reflexivity ] + Tacticals.New.tclTHEN (exists_tac eq1) reflexivity ] | SPLIT_INEQ(e,(e1,act1),(e2,act2)) :: l -> let id1 = new_identifier () and id2 = new_identifier () in @@ -1287,7 +1296,7 @@ let replay_history tactic_normalisation = let tac2 = scalar_norm_add [P_APP 2;P_TYPE] e.body in let eq = val_of(decompile e) in Tacticals.New.tclTHENS - (simplest_elim (EConstr.of_constr (applist (Lazy.force coq_OMEGA19, [eq; mkVar id])))) + (simplest_elim (applist (Lazy.force coq_OMEGA19, [eq; mkVar id]))) [Tacticals.New.tclTHENLIST [ Proofview.V82.tactic (mk_then tac1); (intros_using [id1]); (loop act1) ]; Tacticals.New.tclTHENLIST [ Proofview.V82.tactic (mk_then tac2); (intros_using [id2]); (loop act2) ]] | SUM(e3,(k1,e1),(k2,e2)) :: l -> @@ -1360,15 +1369,15 @@ let replay_history tactic_normalisation = in loop -let normalize p_initial t = - let (tac,t') = transform p_initial t in +let normalize sigma p_initial t = + let (tac,t') = transform sigma p_initial t in let (tac',t'') = condense p_initial t' in let (tac'',t''') = clear_zero p_initial t'' in tac @ tac' @ tac'' , t''' -let normalize_equation id flag theorem pos t t1 t2 (tactic,defs) = +let normalize_equation sigma id flag theorem pos t t1 t2 (tactic,defs) = let p_initial = [P_APP pos ;P_TYPE] in - let (tac,t') = normalize p_initial t in + let (tac,t') = normalize sigma p_initial t in let shift_left = tclTHEN (Proofview.V82.of_tactic (generalize_tac [mkApp (theorem, [| t1; t2; mkVar id |]) ])) @@ -1383,34 +1392,35 @@ let normalize_equation id flag theorem pos t t1 t2 (tactic,defs) = (tactic,defs) let destructure_omega gl tac_def (id,c) = + let sigma = project gl in if String.equal (atompart_of_id id) "State" then tac_def else - try match destructurate_prop c with + try match destructurate_prop sigma c with | Kapp(Eq,[typ;t1;t2]) - when begin match destructurate_type (EConstr.Unsafe.to_constr (pf_nf gl (EConstr.of_constr typ))) with Kapp(Z,[]) -> true | _ -> false end -> + when begin match destructurate_type sigma (pf_nf gl typ) with Kapp(Z,[]) -> true | _ -> false end -> let t = mk_plus t1 (mk_inv t2) in - normalize_equation + normalize_equation sigma id EQUA (Lazy.force coq_Zegal_left) 2 t t1 t2 tac_def | Kapp(Zne,[t1;t2]) -> let t = mk_plus t1 (mk_inv t2) in - normalize_equation + normalize_equation sigma id DISE (Lazy.force coq_Zne_left) 1 t t1 t2 tac_def | Kapp(Zle,[t1;t2]) -> let t = mk_plus t2 (mk_inv t1) in - normalize_equation + normalize_equation sigma id INEQ (Lazy.force coq_Zle_left) 2 t t1 t2 tac_def | Kapp(Zlt,[t1;t2]) -> let t = mk_plus (mk_plus t2 (mk_integer negone)) (mk_inv t1) in - normalize_equation + normalize_equation sigma id INEQ (Lazy.force coq_Zlt_left) 2 t t1 t2 tac_def | Kapp(Zge,[t1;t2]) -> let t = mk_plus t1 (mk_inv t2) in - normalize_equation + normalize_equation sigma id INEQ (Lazy.force coq_Zge_left) 2 t t1 t2 tac_def | Kapp(Zgt,[t1;t2]) -> let t = mk_plus (mk_plus t1 (mk_integer negone)) (mk_inv t2) in - normalize_equation + normalize_equation sigma id INEQ (Lazy.force coq_Zgt_left) 2 t t1 t2 tac_def | _ -> tac_def with e when catchable_exception e -> tac_def @@ -1426,7 +1436,6 @@ let coq_omega = Proofview.Goal.nf_enter { enter = begin fun gl -> clear_constr_tables (); let hyps_types = Tacmach.New.pf_hyps_types gl in - let hyps_types = List.map (on_snd EConstr.Unsafe.to_constr) hyps_types in let destructure_omega = Tacmach.New.of_old destructure_omega gl in let tactic_normalisation, system = List.fold_left destructure_omega ([],[]) hyps_types in @@ -1438,7 +1447,7 @@ let coq_omega = let i = new_id () in tag_hypothesis id i; (Tacticals.New.tclTHENLIST [ - (simplest_elim (EConstr.of_constr (applist (Lazy.force coq_intro_Z, [t])))); + (simplest_elim (applist (Lazy.force coq_intro_Z, [t]))); (intros_using [v; id]); (elim_id id); (clear [id]); @@ -1449,7 +1458,7 @@ let coq_omega = constant = zero; id = i} :: sys else (Tacticals.New.tclTHENLIST [ - (simplest_elim (EConstr.of_constr (applist (Lazy.force coq_new_var, [t])))); + (simplest_elim (applist (Lazy.force coq_new_var, [t]))); (intros_using [v;th]); tac ]), sys) @@ -1480,7 +1489,8 @@ let nat_inject = Proofview.Goal.nf_enter { enter = begin fun gl -> let is_conv = Tacmach.New.pf_apply Reductionops.is_conv gl in let rec explore p t : unit Proofview.tactic = - try match destructurate_term t with + Proofview.tclEVARMAP >>= fun sigma -> + try match destructurate_term sigma t with | Kapp(Plus,[t1;t2]) -> Tacticals.New.tclTHENLIST [ Proofview.V82.tactic (clever_rewrite_gen p (mk_plus (mk_inj t1) (mk_inj t2)) @@ -1499,7 +1509,7 @@ let nat_inject = let id = new_identifier () in Tacticals.New.tclTHENS (Tacticals.New.tclTHEN - (simplest_elim (EConstr.of_constr (applist (Lazy.force coq_le_gt_dec, [t2;t1])))) + (simplest_elim (applist (Lazy.force coq_le_gt_dec, [t2;t1]))) (intros_using [id])) [ Tacticals.New.tclTHENLIST [ @@ -1516,14 +1526,14 @@ let nat_inject = ] | Kapp(S,[t']) -> let rec is_number t = - try match destructurate_term t with + try match destructurate_term sigma t with Kapp(S,[t]) -> is_number t | Kapp(O,[]) -> true | _ -> false with e when catchable_exception e -> false in let rec loop p t : unit Proofview.tactic = - try match destructurate_term t with + try match destructurate_term sigma t with Kapp(S,[t]) -> (Tacticals.New.tclTHEN (Proofview.V82.tactic (clever_rewrite_gen p @@ -1549,7 +1559,8 @@ let nat_inject = and loop = function | [] -> Proofview.tclUNIT () | (i,t)::lit -> - begin try match destructurate_prop t with + Proofview.tclEVARMAP >>= fun sigma -> + begin try match destructurate_prop sigma t with Kapp(Le,[t1;t2]) -> Tacticals.New.tclTHENLIST [ (generalize_tac @@ -1596,7 +1607,7 @@ let nat_inject = (loop lit) ] | Kapp(Eq,[typ;t1;t2]) -> - if is_conv (EConstr.of_constr typ) (EConstr.of_constr (Lazy.force coq_nat)) then + if is_conv typ (Lazy.force coq_nat) then Tacticals.New.tclTHENLIST [ (generalize_tac [mkApp (Lazy.force coq_inj_eq, [| t1;t2;mkVar i |]) ]); @@ -1610,7 +1621,6 @@ let nat_inject = with e when catchable_exception e -> loop lit end in let hyps_types = Tacmach.New.pf_hyps_types gl in - let hyps_types = List.map (on_snd EConstr.Unsafe.to_constr) hyps_types in loop (List.rev hyps_types) end } @@ -1647,7 +1657,7 @@ let not_binop = function exception Undecidable let rec decidability gl t = - match destructurate_prop t with + match destructurate_prop (project gl) t with | Kapp(Or,[t1;t2]) -> mkApp (Lazy.force coq_dec_or, [| t1; t2; decidability gl t1; decidability gl t2 |]) @@ -1665,7 +1675,7 @@ let rec decidability gl t = | Kapp(Not,[t1]) -> mkApp (Lazy.force coq_dec_not, [| t1; decidability gl t1 |]) | Kapp(Eq,[typ;t1;t2]) -> - begin match destructurate_type (EConstr.Unsafe.to_constr (pf_nf gl (EConstr.of_constr typ))) with + begin match destructurate_type (project gl) (pf_nf gl typ) with | Kapp(Z,[]) -> mkApp (Lazy.force coq_dec_eq, [| t1;t2 |]) | Kapp(Nat,[]) -> mkApp (Lazy.force coq_dec_eq_nat, [| t1;t2 |]) | _ -> raise Undecidable @@ -1696,6 +1706,15 @@ let onClearedName2 id tac = Tacticals.New.tclTHENLIST [ introduction id1; introduction id2; tac id1 id2 ] end }) +let local_assum (na, t) = + let inj = EConstr.Unsafe.to_constr in + LocalAssum (na, inj t) + +let rec is_Prop sigma c = match EConstr.kind sigma c with + | Sort (Prop Null) -> true + | Cast (c,_,_) -> is_Prop sigma c + | _ -> false + let destructure_hyps = Proofview.Goal.nf_enter { enter = begin fun gl -> let type_of = Tacmach.New.pf_unsafe_type_of gl in @@ -1705,46 +1724,47 @@ let destructure_hyps = | [] -> (Tacticals.New.tclTHEN nat_inject coq_omega) | decl::lit -> let i = NamedDecl.get_id decl in - begin try match destructurate_prop (NamedDecl.get_type decl) with + Proofview.tclEVARMAP >>= fun sigma -> + begin try match destructurate_prop sigma (EConstr.of_constr (NamedDecl.get_type decl)) with | Kapp(False,[]) -> elim_id i | Kapp((Zle|Zge|Zgt|Zlt|Zne),[t1;t2]) -> loop lit | Kapp(Or,[t1;t2]) -> (Tacticals.New.tclTHENS (elim_id i) - [ onClearedName i (fun i -> (loop (LocalAssum (i,t1)::lit))); - onClearedName i (fun i -> (loop (LocalAssum (i,t2)::lit))) ]) + [ onClearedName i (fun i -> (loop (local_assum (i,t1)::lit))); + onClearedName i (fun i -> (loop (local_assum (i,t2)::lit))) ]) | Kapp(And,[t1;t2]) -> Tacticals.New.tclTHEN (elim_id i) (onClearedName2 i (fun i1 i2 -> - loop (LocalAssum (i1,t1) :: LocalAssum (i2,t2) :: lit))) + loop (local_assum (i1,t1) :: local_assum (i2,t2) :: lit))) | Kapp(Iff,[t1;t2]) -> Tacticals.New.tclTHEN (elim_id i) (onClearedName2 i (fun i1 i2 -> - loop (LocalAssum (i1,mkArrow t1 t2) :: LocalAssum (i2,mkArrow t2 t1) :: lit))) + loop (local_assum (i1,mkArrow t1 t2) :: local_assum (i2,mkArrow t2 t1) :: lit))) | Kimp(t1,t2) -> (* t1 and t2 might be in Type rather than Prop. For t1, the decidability check will ensure being Prop. *) - if is_Prop (EConstr.Unsafe.to_constr (type_of (EConstr.of_constr t2))) + if is_Prop sigma (type_of t2) then let d1 = decidability t1 in Tacticals.New.tclTHENLIST [ (generalize_tac [mkApp (Lazy.force coq_imp_simp, [| t1; t2; d1; mkVar i|])]); (onClearedName i (fun i -> - (loop (LocalAssum (i,mk_or (mk_not t1) t2) :: lit)))) + (loop (local_assum (i,mk_or (mk_not t1) t2) :: lit)))) ] else loop lit | Kapp(Not,[t]) -> - begin match destructurate_prop t with + begin match destructurate_prop sigma t with Kapp(Or,[t1;t2]) -> Tacticals.New.tclTHENLIST [ (generalize_tac [mkApp (Lazy.force coq_not_or,[| t1; t2; mkVar i |])]); (onClearedName i (fun i -> - (loop (LocalAssum (i,mk_and (mk_not t1) (mk_not t2)) :: lit)))) + (loop (local_assum (i,mk_and (mk_not t1) (mk_not t2)) :: lit)))) ] | Kapp(And,[t1;t2]) -> let d1 = decidability t1 in @@ -1753,7 +1773,7 @@ let destructure_hyps = [mkApp (Lazy.force coq_not_and, [| t1; t2; d1; mkVar i |])]); (onClearedName i (fun i -> - (loop (LocalAssum (i,mk_or (mk_not t1) (mk_not t2)) :: lit)))) + (loop (local_assum (i,mk_or (mk_not t1) (mk_not t2)) :: lit)))) ] | Kapp(Iff,[t1;t2]) -> let d1 = decidability t1 in @@ -1763,7 +1783,7 @@ let destructure_hyps = [mkApp (Lazy.force coq_not_iff, [| t1; t2; d1; d2; mkVar i |])]); (onClearedName i (fun i -> - (loop (LocalAssum (i, mk_or (mk_and t1 (mk_not t2)) + (loop (local_assum (i, mk_or (mk_and t1 (mk_not t2)) (mk_and (mk_not t1) t2)) :: lit)))) ] | Kimp(t1,t2) -> @@ -1775,14 +1795,14 @@ let destructure_hyps = [mkApp (Lazy.force coq_not_imp, [| t1; t2; d1; mkVar i |])]); (onClearedName i (fun i -> - (loop (LocalAssum (i,mk_and t1 (mk_not t2)) :: lit)))) + (loop (local_assum (i,mk_and t1 (mk_not t2)) :: lit)))) ] | Kapp(Not,[t]) -> let d = decidability t in Tacticals.New.tclTHENLIST [ (generalize_tac [mkApp (Lazy.force coq_not_not, [| t; d; mkVar i |])]); - (onClearedName i (fun i -> (loop (LocalAssum (i,t) :: lit)))) + (onClearedName i (fun i -> (loop (local_assum (i,t) :: lit)))) ] | Kapp(op,[t1;t2]) -> (try @@ -1795,32 +1815,32 @@ let destructure_hyps = with Not_found -> loop lit) | Kapp(Eq,[typ;t1;t2]) -> if !old_style_flag then begin - match destructurate_type (EConstr.Unsafe.to_constr (pf_nf (EConstr.of_constr typ))) with + match destructurate_type sigma (pf_nf typ) with | Kapp(Nat,_) -> Tacticals.New.tclTHENLIST [ (simplest_elim - (EConstr.of_constr (mkApp - (Lazy.force coq_not_eq, [|t1;t2;mkVar i|])))); + (mkApp + (Lazy.force coq_not_eq, [|t1;t2;mkVar i|]))); (onClearedName i (fun _ -> loop lit)) ] | Kapp(Z,_) -> Tacticals.New.tclTHENLIST [ (simplest_elim - (EConstr.of_constr (mkApp - (Lazy.force coq_not_Zeq, [|t1;t2;mkVar i|])))); + (mkApp + (Lazy.force coq_not_Zeq, [|t1;t2;mkVar i|]))); (onClearedName i (fun _ -> loop lit)) ] | _ -> loop lit end else begin - match destructurate_type (EConstr.Unsafe.to_constr (pf_nf (EConstr.of_constr typ))) with + match destructurate_type sigma (pf_nf typ) with | Kapp(Nat,_) -> (Tacticals.New.tclTHEN - (convert_hyp_no_check (NamedDecl.set_type (mkApp (Lazy.force coq_neq, [| t1;t2|])) + (convert_hyp_no_check (NamedDecl.set_type (EConstr.Unsafe.to_constr (mkApp (Lazy.force coq_neq, [| t1;t2|]))) decl)) (loop lit)) | Kapp(Z,_) -> (Tacticals.New.tclTHEN - (convert_hyp_no_check (NamedDecl.set_type (mkApp (Lazy.force coq_Zne, [| t1;t2|])) + (convert_hyp_no_check (NamedDecl.set_type (EConstr.Unsafe.to_constr (mkApp (Lazy.force coq_Zne, [| t1;t2|]))) decl)) (loop lit)) | _ -> loop lit @@ -1842,7 +1862,8 @@ let destructure_goal = let concl = Proofview.Goal.concl gl in let decidability = Tacmach.New.of_old decidability gl in let rec loop t = - match destructurate_prop t with + Proofview.tclEVARMAP >>= fun sigma -> + match destructurate_prop sigma t with | Kapp(Not,[t]) -> (Tacticals.New.tclTHEN (Tacticals.New.tclTHEN (unfold sp_not) intro) @@ -1855,13 +1876,12 @@ let destructure_goal = let dec = decidability t in Tacticals.New.tclTHEN (Proofview.V82.tactic (Tacmach.refine - (EConstr.of_constr (mkApp (Lazy.force coq_dec_not_not, [| t; dec; mkNewMeta () |]))))) + (mkApp (Lazy.force coq_dec_not_not, [| t; dec; mkNewMeta () |])))) intro - with Undecidable -> Tactics.elim_type (EConstr.of_constr (build_coq_False ())) + with Undecidable -> Tactics.elim_type (Lazy.force coq_False) in Tacticals.New.tclTHEN goal_tac destructure_hyps in - let concl = EConstr.Unsafe.to_constr concl in (loop concl) end } -- cgit v1.2.3