diff options
Diffstat (limited to 'plugins/cc')
| -rw-r--r-- | plugins/cc/ccalgo.ml | 22 | ||||
| -rw-r--r-- | plugins/cc/cctac.ml | 268 | ||||
| -rw-r--r-- | plugins/cc/cctac.mli | 4 | ||||
| -rw-r--r-- | plugins/cc/g_congruence.ml4 | 1 |
4 files changed, 168 insertions, 127 deletions
diff --git a/plugins/cc/ccalgo.ml b/plugins/cc/ccalgo.ml index bc53b113df..aa71a45658 100644 --- a/plugins/cc/ccalgo.ml +++ b/plugins/cc/ccalgo.ml @@ -444,7 +444,7 @@ and applist_projection c l = let p = Projection.make (fst c) false in (match l with | [] -> (* Expand the projection *) - let ty,_ = Typeops.type_of_constant (Global.env ()) c in + let ty = Typeops.type_of_constant_in (Global.env ()) c in (* FIXME constraints *) let pb = Environ.lookup_projection p (Global.env()) in let ctx,_ = Term.decompose_prod_n_assum (pb.Declarations.proj_npars + 1) ty in it_mkLambda_or_LetIn (mkProj(p,mkRel 1)) ctx @@ -452,8 +452,9 @@ and applist_projection c l = applistc (mkProj (p, hd)) tl) | _ -> applistc c l -let rec canonize_name c = - let func = canonize_name in +let rec canonize_name sigma c = + let c = EConstr.Unsafe.to_constr c in + let func c = canonize_name sigma (EConstr.of_constr c) in match kind_of_term c with | Const (kn,u) -> let canon_const = constant_of_kn (canonical_con kn) in @@ -497,10 +498,10 @@ let rec inst_pattern subst = function args t let pr_idx_term uf i = str "[" ++ int i ++ str ":=" ++ - Termops.print_constr (constr_of_term (term uf i)) ++ str "]" + Termops.print_constr (EConstr.of_constr (constr_of_term (term uf i))) ++ str "]" let pr_term t = str "[" ++ - Termops.print_constr (constr_of_term t) ++ str "]" + Termops.print_constr (EConstr.of_constr (constr_of_term t)) ++ str "]" let rec add_term state t= let uf=state.uf in @@ -508,8 +509,8 @@ let rec add_term state t= Not_found -> let b=next uf in let trm = constr_of_term t in - let typ = pf_unsafe_type_of state.gls trm in - let typ = canonize_name typ in + let typ = pf_unsafe_type_of state.gls (EConstr.of_constr trm) in + let typ = canonize_name (project state.gls) typ in let new_node= match t with Symb _ | Product (_,_) -> @@ -615,7 +616,7 @@ let add_inst state (inst,int_subst) = begin debug (fun () -> (str "Adding new equality, depth="++ int state.rew_depth) ++ fnl () ++ - (str " [" ++ Termops.print_constr prf ++ str " : " ++ + (str " [" ++ Termops.print_constr (EConstr.of_constr prf) ++ str " : " ++ pr_term s ++ str " == " ++ pr_term t ++ str "]")); add_equality state prf s t end @@ -623,7 +624,7 @@ let add_inst state (inst,int_subst) = begin debug (fun () -> (str "Adding new disequality, depth="++ int state.rew_depth) ++ fnl () ++ - (str " [" ++ Termops.print_constr prf ++ str " : " ++ + (str " [" ++ Termops.print_constr (EConstr.of_constr prf) ++ str " : " ++ pr_term s ++ str " <> " ++ pr_term t ++ str "]")); add_disequality state (Hyp prf) s t end @@ -832,7 +833,8 @@ let complete_one_class state i= let id = new_state_var etyp state in app (Appli(t,Eps id)) (substl [mkVar id] rest) (n-1) in let _c = pf_unsafe_type_of state.gls - (constr_of_term (term state.uf pac.cnode)) in + (EConstr.of_constr (constr_of_term (term state.uf pac.cnode))) in + let _c = EConstr.Unsafe.to_constr _c in let _args = List.map (fun i -> constr_of_term (term state.uf i)) pac.args in diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml index b5ca2f50fc..00b31cccee 100644 --- a/plugins/cc/cctac.ml +++ b/plugins/cc/cctac.ml @@ -13,6 +13,7 @@ open Names open Inductiveops open Declarations open Term +open EConstr open Vars open Tacmach open Tactics @@ -39,13 +40,11 @@ let _False = reference ["Init";"Logic"] "False" let _True = reference ["Init";"Logic"] "True" let _I = reference ["Init";"Logic"] "I" -let whd env= - let infos=CClosure.create_clos_infos CClosure.betaiotazeta env in - (fun t -> CClosure.whd_val infos (CClosure.inject t)) +let whd env sigma t = + Reductionops.clos_whd_flags CClosure.betaiotazeta env sigma t -let whd_delta env= - let infos=CClosure.create_clos_infos CClosure.all env in - (fun t -> CClosure.whd_val infos (CClosure.inject t)) +let whd_delta env sigma t = + Reductionops.clos_whd_flags CClosure.all env sigma t (* decompose member of equality in an applicative format *) @@ -53,12 +52,12 @@ let whd_delta env= let sf_of env sigma c = e_sort_of env (ref sigma) c let rec decompose_term env sigma t= - match kind_of_term (whd env t) with + match EConstr.kind sigma (whd env sigma t) with App (f,args)-> let tf=decompose_term env sigma f in let targs=Array.map (decompose_term env sigma) args in Array.fold_left (fun s t->Appli (s,t)) tf targs - | Prod (_,a,_b) when not (Termops.dependent (mkRel 1) _b) -> + | Prod (_,a,_b) when noccurn sigma 1 _b -> let b = Termops.pop _b in let sort_b = sf_of env sigma b in let sort_a = sf_of env sigma a in @@ -67,6 +66,7 @@ let rec decompose_term env sigma t= decompose_term env sigma b) | Construct c -> let (((mind,i_ind),i_con),u)= c in + let u = EInstance.kind sigma u in let canon_mind = mind_of_kn (canonical_mind mind) in let canon_ind = canon_mind,i_ind in let (oib,_)=Global.lookup_inductive (canon_ind) in @@ -76,28 +76,30 @@ let rec decompose_term env sigma t= ci_nhyps=nargs-oib.mind_nparams} | Ind c -> let (mind,i_ind),u = c in + let u = EInstance.kind sigma u in let canon_mind = mind_of_kn (canonical_mind mind) in - let canon_ind = canon_mind,i_ind in (Symb (mkIndU (canon_ind,u))) + let canon_ind = canon_mind,i_ind in (Symb (Constr.mkIndU (canon_ind,u))) | Const (c,u) -> + let u = EInstance.kind sigma u in let canon_const = constant_of_kn (canonical_con c) in - (Symb (mkConstU (canon_const,u))) + (Symb (Constr.mkConstU (canon_const,u))) | Proj (p, c) -> let canon_const kn = constant_of_kn (canonical_con kn) in let p' = Projection.map canon_const p in - (Appli (Symb (mkConst (Projection.constant p')), decompose_term env sigma c)) + (Appli (Symb (Constr.mkConst (Projection.constant p')), decompose_term env sigma c)) | _ -> - let t = Termops.strip_outer_cast t in - if closed0 t then Symb t else raise Not_found + let t = Termops.strip_outer_cast sigma t in + if closed0 sigma t then Symb (EConstr.to_constr sigma t) else raise Not_found (* decompose equality in members and type *) -open Globnames +open Termops let atom_of_constr env sigma term = - let wh = (whd_delta env term) in - let kot = kind_of_term wh in + let wh = whd_delta env sigma term in + let kot = EConstr.kind sigma wh in match kot with App (f,args)-> - if is_global (Lazy.force _eq) f && Int.equal (Array.length args) 3 + if is_global sigma (Lazy.force _eq) f && Int.equal (Array.length args) 3 then `Eq (args.(0), decompose_term env sigma args.(1), decompose_term env sigma args.(2)) @@ -105,14 +107,14 @@ let atom_of_constr env sigma term = | _ -> `Other (decompose_term env sigma term) let rec pattern_of_constr env sigma c = - match kind_of_term (whd env c) with + match EConstr.kind sigma (whd env sigma c) with App (f,args)-> let pf = decompose_term env sigma f in let pargs,lrels = List.split (Array.map_to_list (pattern_of_constr env sigma) args) in PApp (pf,List.rev pargs), List.fold_left Int.Set.union Int.Set.empty lrels - | Prod (_,a,_b) when not (Termops.dependent (mkRel 1) _b) -> + | Prod (_,a,_b) when noccurn sigma 1 _b -> let b = Termops.pop _b in let pa,sa = pattern_of_constr env sigma a in let pb,sb = pattern_of_constr env sigma b in @@ -131,19 +133,19 @@ let non_trivial = function let patterns_of_constr env sigma nrels term= let f,args= - try destApp (whd_delta env term) with DestKO -> raise Not_found in - if is_global (Lazy.force _eq) f && Int.equal (Array.length args) 3 + try destApp sigma (whd_delta env sigma term) with DestKO -> raise Not_found in + if is_global sigma (Lazy.force _eq) f && Int.equal (Array.length args) 3 then let patt1,rels1 = pattern_of_constr env sigma args.(1) and patt2,rels2 = pattern_of_constr env sigma args.(2) in let valid1 = if not (Int.equal (Int.Set.cardinal rels1) nrels) then Creates_variables else if non_trivial patt1 then Normal - else Trivial args.(0) + else Trivial (EConstr.to_constr sigma args.(0)) and valid2 = if not (Int.equal (Int.Set.cardinal rels2) nrels) then Creates_variables else if non_trivial patt2 then Normal - else Trivial args.(0) in + else Trivial (EConstr.to_constr sigma args.(0)) in if valid1 != Creates_variables || valid2 != Creates_variables then nrels,valid1,patt1,valid2,patt2 @@ -151,28 +153,28 @@ let patterns_of_constr env sigma nrels term= else raise Not_found let rec quantified_atom_of_constr env sigma nrels term = - match kind_of_term (whd_delta env term) with + match EConstr.kind sigma (whd_delta env sigma term) with Prod (id,atom,ff) -> - if is_global (Lazy.force _False) ff then + if is_global sigma (Lazy.force _False) ff then let patts=patterns_of_constr env sigma nrels atom in `Nrule patts else - quantified_atom_of_constr (Environ.push_rel (RelDecl.LocalAssum (id,atom)) env) sigma (succ nrels) ff + quantified_atom_of_constr (EConstr.push_rel (RelDecl.LocalAssum (id,atom)) env) sigma (succ nrels) ff | _ -> let patts=patterns_of_constr env sigma nrels term in `Rule patts let litteral_of_constr env sigma term= - match kind_of_term (whd_delta env term) with + match EConstr.kind sigma (whd_delta env sigma term) with | Prod (id,atom,ff) -> - if is_global (Lazy.force _False) ff then + if is_global sigma (Lazy.force _False) ff then match (atom_of_constr env sigma atom) with `Eq(t,a,b) -> `Neq(t,a,b) | `Other(p) -> `Nother(p) else begin try - quantified_atom_of_constr (Environ.push_rel (RelDecl.LocalAssum (id,atom)) env) sigma 1 ff + quantified_atom_of_constr (EConstr.push_rel (RelDecl.LocalAssum (id,atom)) env) sigma 1 ff with Not_found -> `Other (decompose_term env sigma term) end @@ -183,9 +185,10 @@ let litteral_of_constr env sigma term= (* store all equalities from the context *) let make_prb gls depth additionnal_terms = + let open Tacmach.New in let env=pf_env gls in - let sigma=sig_sig gls in - let state = empty depth gls in + let sigma=project gls in + let state = empty depth {it = Proofview.Goal.goal (Proofview.Goal.assume gls); sigma } in let pos_hyps = ref [] in let neg_hyps =ref [] in List.iter @@ -196,7 +199,7 @@ let make_prb gls depth additionnal_terms = (fun decl -> let id = NamedDecl.get_id decl in begin - let cid=mkVar id in + let cid=Constr.mkVar id in match litteral_of_constr env sigma (NamedDecl.get_type decl) with `Eq (t,a,b) -> add_equality state cid a b | `Neq (t,a,b) -> add_disequality state (Hyp cid) a b @@ -214,9 +217,9 @@ let make_prb gls depth additionnal_terms = neg_hyps:=(cid,nh):: !neg_hyps | `Rule patts -> add_quant state id true patts | `Nrule patts -> add_quant state id false patts - end) (Environ.named_context_of_val (Goal.V82.nf_hyps gls.sigma gls.it)); + end) (Proofview.Goal.hyps gls); begin - match atom_of_constr env sigma (Evarutil.nf_evar sigma (pf_concl gls)) with + match atom_of_constr env sigma (pf_concl gls) with `Eq (t,a,b) -> add_disequality state Goal a b | `Other g -> List.iter @@ -228,6 +231,7 @@ let make_prb gls depth additionnal_terms = (* indhyps builds the array of arrays of constructor hyps for (ind largs) *) let build_projection intype (cstr:pconstructor) special default gls= + let open Tacmach.New in let ci= (snd(fst cstr)) in let body=Equality.build_selector (pf_env gls) (project gls) ci (mkRel 1) intype special default in let id=pf_get_new_id (Id.of_string "t") gls in @@ -235,20 +239,43 @@ let build_projection intype (cstr:pconstructor) special default gls= (* generate an adhoc tactic following the proof tree *) -let _M =mkMeta - let app_global f args k = - Tacticals.pf_constr_of_global (Lazy.force f) (fun fc -> k (mkApp (fc, args))) - -let new_app_global f args k = - Tacticals.New.pf_constr_of_global (Lazy.force f) (fun fc -> k (mkApp (fc, args))) - -let new_refine c = Proofview.V82.tactic (refine c) + Tacticals.New.pf_constr_of_global (Lazy.force f) >>= fun fc -> k (mkApp (fc, args)) + +let rec gen_holes env sigma t n accu = + let open Sigma in + if Int.equal n 0 then (sigma, List.rev accu) + else match EConstr.kind sigma t with + | Prod (_, u, t) -> + let sigma = Sigma.Unsafe.of_evar_map sigma in + let Sigma (ev, sigma, _) = Evarutil.new_evar env sigma u in + let sigma = Sigma.to_evar_map sigma in + let t = EConstr.Vars.subst1 ev t in + gen_holes env sigma t (pred n) (ev :: accu) + | _ -> assert false + +let app_global_with_holes f args n = + Proofview.Goal.enter { enter = begin fun gl -> + Tacticals.New.pf_constr_of_global (Lazy.force f) >>= fun fc -> + let env = Proofview.Goal.env gl in + let concl = Proofview.Goal.concl gl in + Refine.refine { Sigma.run = begin fun sigma -> + let sigma = Sigma.to_evar_map sigma in + let t = Tacmach.New.pf_get_type_of gl fc in + let t = Termops.prod_applist sigma t (Array.to_list args) in + let ans = mkApp (fc, args) in + let (sigma, holes) = gen_holes env sigma t n [] in + let ans = applist (ans, holes) in + let evdref = ref sigma in + let () = Typing.e_check env evdref ans concl in + Sigma.Unsafe.of_pair (ans, !evdref) + end } + end } let assert_before n c = - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.s_enter { s_enter = begin fun gl -> let evm, _ = Tacmach.New.pf_apply type_of gl c in - Tacticals.New.tclTHEN (Proofview.V82.tactic (Refiner.tclEVARS evm)) (assert_before n c) + Sigma.Unsafe.of_pair (assert_before n c, evm) end } let refresh_type env evm ty = @@ -256,35 +283,38 @@ let refresh_type env evm ty = (Some false) env evm ty let refresh_universes ty k = - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.s_enter { s_enter = begin fun gl -> let env = Proofview.Goal.env gl in let evm = Tacmach.New.project gl in let evm, ty = refresh_type env evm ty in - Tacticals.New.tclTHEN (Proofview.V82.tactic (Refiner.tclEVARS evm)) (k ty) + Sigma.Unsafe.of_pair (k ty, evm) end } +let constr_of_term c = EConstr.of_constr (constr_of_term c) + let rec proof_tac p : unit Proofview.tactic = - Proofview.Goal.nf_enter { enter = begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let type_of t = Tacmach.New.pf_unsafe_type_of gl t in try (* type_of can raise exceptions *) match p.p_rule with - Ax c -> exact_check c + Ax c -> exact_check (EConstr.of_constr c) | SymAx c -> + let c = EConstr.of_constr c in let l=constr_of_term p.p_lhs and r=constr_of_term p.p_rhs in refresh_universes (type_of l) (fun typ -> - new_app_global _sym_eq [|typ;r;l;c|] exact_check) + app_global _sym_eq [|typ;r;l;c|] exact_check) | Refl t -> let lr = constr_of_term t in refresh_universes (type_of lr) (fun typ -> - new_app_global _refl_equal [|typ;constr_of_term t|] exact_check) + app_global _refl_equal [|typ;constr_of_term t|] exact_check) | Trans (p1,p2)-> let t1 = constr_of_term p1.p_lhs and t2 = constr_of_term p1.p_rhs and t3 = constr_of_term p2.p_rhs in refresh_universes (type_of t2) (fun typ -> - let prf = new_app_global _trans_eq [|typ;t1;t2;t3;_M 1;_M 2|] in - Tacticals.New.tclTHENS (prf new_refine) [(proof_tac p1);(proof_tac p2)]) + let prf = app_global_with_holes _trans_eq [|typ;t1;t2;t3;|] 2 in + Tacticals.New.tclTHENS prf [(proof_tac p1);(proof_tac p2)]) | Congr (p1,p2)-> let tf1=constr_of_term p1.p_lhs and tx1=constr_of_term p2.p_lhs @@ -293,20 +323,20 @@ let rec proof_tac p : unit Proofview.tactic = refresh_universes (type_of tf1) (fun typf -> refresh_universes (type_of tx1) (fun typx -> refresh_universes (type_of (mkApp (tf1,[|tx1|]))) (fun typfx -> - let id = Tacmach.New.of_old (fun gls -> pf_get_new_id (Id.of_string "f") gls) gl in + let id = Tacmach.New.pf_get_new_id (Id.of_string "f") gl in let appx1 = mkLambda(Name id,typf,mkApp(mkRel 1,[|tx1|])) in - let lemma1 = app_global _f_equal [|typf;typfx;appx1;tf1;tf2;_M 1|] in - let lemma2 = app_global _f_equal [|typx;typfx;tf2;tx1;tx2;_M 1|] in + let lemma1 = app_global_with_holes _f_equal [|typf;typfx;appx1;tf1;tf2|] 1 in + let lemma2 = app_global_with_holes _f_equal [|typx;typfx;tf2;tx1;tx2|] 1 in let prf = - app_global _trans_eq + app_global_with_holes _trans_eq [|typfx; mkApp(tf1,[|tx1|]); mkApp(tf2,[|tx1|]); - mkApp(tf2,[|tx2|]);_M 2;_M 3|] in - Tacticals.New.tclTHENS (Proofview.V82.tactic (prf refine)) - [Tacticals.New.tclTHEN (Proofview.V82.tactic (lemma1 refine)) (proof_tac p1); + mkApp(tf2,[|tx2|])|] 2 in + Tacticals.New.tclTHENS prf + [Tacticals.New.tclTHEN lemma1 (proof_tac p1); Tacticals.New.tclFIRST - [Tacticals.New.tclTHEN (Proofview.V82.tactic (lemma2 refine)) (proof_tac p2); + [Tacticals.New.tclTHEN lemma2 (proof_tac p2); reflexivity; Tacticals.New.tclZEROMSG (Pp.str @@ -319,48 +349,50 @@ let rec proof_tac p : unit Proofview.tactic = refresh_universes (type_of ti) (fun intype -> refresh_universes (type_of default) (fun outtype -> let proj = - Tacmach.New.of_old (build_projection intype cstr special default) gl + build_projection intype cstr special default gl in let injt= - app_global _f_equal [|intype;outtype;proj;ti;tj;_M 1|] in - Tacticals.New.tclTHEN (Proofview.V82.tactic (injt refine)) (proof_tac prf))) + app_global_with_holes _f_equal [|intype;outtype;proj;ti;tj|] 1 in + Tacticals.New.tclTHEN injt (proof_tac prf))) with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e end } let refute_tac c t1 t2 p = - Proofview.Goal.nf_enter { enter = begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let tt1=constr_of_term t1 and tt2=constr_of_term t2 in - let hid = Tacmach.New.of_old (pf_get_new_id (Id.of_string "Heq")) gl in + let hid = Tacmach.New.pf_get_new_id (Id.of_string "Heq") gl in let false_t=mkApp (c,[|mkVar hid|]) in let k intype = - let neweq= new_app_global _eq [|intype;tt1;tt2|] in + let neweq= app_global _eq [|intype;tt1;tt2|] in Tacticals.New.tclTHENS (neweq (assert_before (Name hid))) [proof_tac p; simplest_elim false_t] in refresh_universes (Tacmach.New.pf_unsafe_type_of gl tt1) k end } -let refine_exact_check c gl = - let evm, _ = pf_apply type_of gl c in - Tacticals.tclTHEN (Refiner.tclEVARS evm) (Proofview.V82.of_tactic (exact_check c)) gl +let refine_exact_check c = + Proofview.Goal.s_enter { s_enter = begin fun gl -> + let evm, _ = Tacmach.New.pf_apply type_of gl c in + Sigma.Unsafe.of_pair (exact_check c, evm) + end } let convert_to_goal_tac c t1 t2 p = - Proofview.Goal.nf_enter { enter = begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let tt1=constr_of_term t1 and tt2=constr_of_term t2 in let k sort = - let neweq= new_app_global _eq [|sort;tt1;tt2|] in - let e = Tacmach.New.of_old (pf_get_new_id (Id.of_string "e")) gl in - let x = Tacmach.New.of_old (pf_get_new_id (Id.of_string "X")) gl in + let neweq= app_global _eq [|sort;tt1;tt2|] in + let e = Tacmach.New.pf_get_new_id (Id.of_string "e") gl in + let x = Tacmach.New.pf_get_new_id (Id.of_string "X") gl in let identity=mkLambda (Name x,sort,mkRel 1) in - let endt=app_global _eq_rect [|sort;tt1;identity;c;tt2;mkVar e|] in + let endt = app_global _eq_rect [|sort;tt1;identity;c;tt2;mkVar e|] in Tacticals.New.tclTHENS (neweq (assert_before (Name e))) - [proof_tac p; Proofview.V82.tactic (endt refine_exact_check)] + [proof_tac p; endt refine_exact_check] in refresh_universes (Tacmach.New.pf_unsafe_type_of gl tt2) k end } let convert_to_hyp_tac c1 t1 c2 t2 p = - Proofview.Goal.nf_enter { enter = begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let tt2=constr_of_term t2 in - let h = Tacmach.New.of_old (pf_get_new_id (Id.of_string "H")) gl in + let h = Tacmach.New.pf_get_new_id (Id.of_string "H") gl in let false_t=mkApp (c2,[|mkVar h|]) in Tacticals.New.tclTHENS (assert_before (Name h) tt2) [convert_to_goal_tac c1 t1 t2 p; @@ -368,46 +400,48 @@ let convert_to_hyp_tac c1 t1 c2 t2 p = end } let discriminate_tac (cstr,u as cstru) p = - Proofview.Goal.nf_enter { enter = begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let t1=constr_of_term p.p_lhs and t2=constr_of_term p.p_rhs in let env = Proofview.Goal.env gl in let concl = Proofview.Goal.concl gl in - let xid = Tacmach.New.of_old (pf_get_new_id (Id.of_string "X")) gl in + let xid = Tacmach.New.pf_get_new_id (Id.of_string "X") gl in let identity = Universes.constr_of_global (Lazy.force _I) in + let identity = EConstr.of_constr identity in let trivial = Universes.constr_of_global (Lazy.force _True) in + let trivial = EConstr.of_constr trivial in let evm = Tacmach.New.project gl in let evm, intype = refresh_type env evm (Tacmach.New.pf_unsafe_type_of gl t1) in let evm, outtype = Evd.new_sort_variable Evd.univ_flexible evm in let outtype = mkSort outtype in let pred = mkLambda(Name xid,outtype,mkRel 1) in - let hid = Tacmach.New.of_old (pf_get_new_id (Id.of_string "Heq")) gl in - let proj = Tacmach.New.of_old (build_projection intype cstru trivial concl) gl in - let injt=app_global _f_equal + let hid = Tacmach.New.pf_get_new_id (Id.of_string "Heq") gl in + let proj = build_projection intype cstru trivial concl gl in + let injt = app_global _f_equal [|intype;outtype;proj;t1;t2;mkVar hid|] in let endt k = injt (fun injt -> app_global _eq_rect [|outtype;trivial;pred;identity;concl;injt|] k) in - let neweq=new_app_global _eq [|intype;t1;t2|] in + let neweq = app_global _eq [|intype;t1;t2|] in Tacticals.New.tclTHEN (Proofview.Unsafe.tclEVARS evm) (Tacticals.New.tclTHENS (neweq (assert_before (Name hid))) - [proof_tac p; Proofview.V82.tactic (endt refine_exact_check)]) + [proof_tac p; endt refine_exact_check]) end } (* wrap everything *) -let build_term_to_complete uf meta pac = +let build_term_to_complete uf pac = let cinfo = get_constructor_info uf pac.cnode in - let real_args = List.map (fun i -> constr_of_term (term uf i)) pac.args in - let dummy_args = List.rev (List.init pac.arity meta) in - let all_args = List.rev_append real_args dummy_args in - applistc (mkConstructU cinfo.ci_constr) all_args + let real_args = List.rev_map (fun i -> constr_of_term (term uf i)) pac.args in + let (kn, u) = cinfo.ci_constr in + (applist (mkConstructU (kn, EInstance.make u), real_args), pac.arity) let cc_tactic depth additionnal_terms = - Proofview.Goal.nf_enter { enter = begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> + let sigma = Tacmach.New.project gl in Coqlib.check_required_library Coqlib.logic_module_name; let _ = debug (fun () -> Pp.str "Reading subgoal ...") in - let state = Tacmach.New.of_old (fun gls -> make_prb gls depth additionnal_terms) gl in + let state = make_prb gl depth additionnal_terms in let _ = debug (fun () -> Pp.str "Problem built, solving ...") in let sol = execute true state in let _ = debug (fun () -> Pp.str "Computation completed.") in @@ -422,16 +456,17 @@ let cc_tactic depth additionnal_terms = let cstr=(get_constructor_info uf ipac.cnode).ci_constr in discriminate_tac cstr p | Incomplete -> + let open Glob_term in let env = Proofview.Goal.env gl in - let metacnt = ref 0 in - let newmeta _ = incr metacnt; _M !metacnt in - let terms_to_complete = - List.map - (build_term_to_complete uf newmeta) - (epsilons uf) in + let terms_to_complete = List.map (build_term_to_complete uf) (epsilons uf) in + let hole = GHole (Loc.ghost, Evar_kinds.InternalHole, Misctypes.IntroAnonymous, None) in + let pr_missing (c, missing) = + let c = Detyping.detype ~lax:true false [] env sigma c in + let holes = List.init missing (fun _ -> hole) in + Printer.pr_glob_constr_env env (GApp (Loc.ghost, c, holes)) + in Feedback.msg_info - (Pp.str "Goal is solvable by congruence but \ - some arguments are missing."); + (Pp.str "Goal is solvable by congruence but some arguments are missing."); Feedback.msg_info (Pp.str " Try " ++ hov 8 @@ -439,7 +474,7 @@ let cc_tactic depth additionnal_terms = str "\"congruence with (" ++ prlist_with_sep (fun () -> str ")" ++ spc () ++ str "(") - (Termops.print_constr_env env) + pr_missing terms_to_complete ++ str ")\"," end ++ @@ -450,20 +485,23 @@ let cc_tactic depth additionnal_terms = let ta=term uf dis.lhs and tb=term uf dis.rhs in match dis.rule with Goal -> proof_tac p - | Hyp id -> refute_tac id ta tb p + | Hyp id -> refute_tac (EConstr.of_constr id) ta tb p | HeqG id -> + let id = EConstr.of_constr id in convert_to_goal_tac id ta tb p | HeqnH (ida,idb) -> + let ida = EConstr.of_constr ida in + let idb = EConstr.of_constr idb in convert_to_hyp_tac ida ta idb tb p end } -let cc_fail gls = - user_err ~hdr:"Congruence" (Pp.str "congruence failed.") +let cc_fail = + Tacticals.New.tclZEROMSG (Pp.str "congruence failed.") let congruence_tac depth l = Tacticals.New.tclORELSE (Tacticals.New.tclTHEN (Tacticals.New.tclREPEAT introf) (cc_tactic depth l)) - (Proofview.V82.tactic cc_fail) + cc_fail (* Beware: reflexivity = constructor 1 = apply refl_equal might be slow now, let's rather do something equivalent @@ -477,31 +515,31 @@ let congruence_tac depth l = *) let mk_eq f c1 c2 k = - Tacticals.New.pf_constr_of_global (Lazy.force f) (fun fc -> - Proofview.Goal.enter { enter = begin fun gl -> + Tacticals.New.pf_constr_of_global (Lazy.force f) >>= fun fc -> + Proofview.Goal.s_enter { s_enter = begin fun gl -> let open Tacmach.New in let evm, ty = pf_apply type_of gl c1 in let evm, ty = Evarsolve.refresh_universes (Some false) (pf_env gl) evm ty in let term = mkApp (fc, [| ty; c1; c2 |]) in let evm, _ = type_of (pf_env gl) evm term in - Tacticals.New.tclTHEN (Proofview.V82.tactic (Refiner.tclEVARS evm)) - (k term) - end }) + Sigma.Unsafe.of_pair (k term, evm) + end } let f_equal = - Proofview.Goal.nf_enter { enter = begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let concl = Proofview.Goal.concl gl in + let sigma = Tacmach.New.project gl in let cut_eq c1 c2 = try (* type_of can raise an exception *) Tacticals.New.tclTHENS (mk_eq _eq c1 c2 Tactics.cut) - [Proofview.tclUNIT ();Tacticals.New.tclTRY ((new_app_global _refl_equal [||]) apply)] + [Proofview.tclUNIT ();Tacticals.New.tclTRY ((app_global _refl_equal [||]) apply)] with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e in Proofview.tclORELSE - begin match kind_of_term concl with - | App (r,[|_;t;t'|]) when Globnames.is_global (Lazy.force _eq) r -> - begin match kind_of_term t, kind_of_term t' with + begin match EConstr.kind sigma concl with + | App (r,[|_;t;t'|]) when is_global sigma (Lazy.force _eq) r -> + begin match EConstr.kind sigma t, EConstr.kind sigma t' with | App (f,v), App (f',v') when Int.equal (Array.length v) (Array.length v') -> let rec cuts i = if i < 0 then Tacticals.New.tclTRY (congruence_tac 1000 []) @@ -512,7 +550,7 @@ let f_equal = | _ -> Proofview.tclUNIT () end begin function (e, info) -> match e with - | Type_errors.TypeError _ -> Proofview.tclUNIT () + | Pretype_errors.PretypeError _ | Type_errors.TypeError _ -> Proofview.tclUNIT () | e -> Proofview.tclZERO ~info e end end } diff --git a/plugins/cc/cctac.mli b/plugins/cc/cctac.mli index 7c1d9f1c07..5099d847b0 100644 --- a/plugins/cc/cctac.mli +++ b/plugins/cc/cctac.mli @@ -7,14 +7,14 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Term +open EConstr open Proof_type val proof_tac: Ccproof.proof -> unit Proofview.tactic val cc_tactic : int -> constr list -> unit Proofview.tactic -val cc_fail : tactic +val cc_fail : unit Proofview.tactic val congruence_tac : int -> constr list -> unit Proofview.tactic diff --git a/plugins/cc/g_congruence.ml4 b/plugins/cc/g_congruence.ml4 index 6f6811334d..7e76854b16 100644 --- a/plugins/cc/g_congruence.ml4 +++ b/plugins/cc/g_congruence.ml4 @@ -8,6 +8,7 @@ (*i camlp4deps: "grammar/grammar.cma" i*) +open Ltac_plugin open Cctac open Stdarg |