diff options
Diffstat (limited to 'plugins/cc')
| -rw-r--r-- | plugins/cc/cc_plugin.mlpack (renamed from plugins/cc/cc_plugin.mllib) | 1 | ||||
| -rw-r--r-- | plugins/cc/ccalgo.ml | 39 | ||||
| -rw-r--r-- | plugins/cc/ccalgo.mli | 2 | ||||
| -rw-r--r-- | plugins/cc/ccproof.ml | 14 | ||||
| -rw-r--r-- | plugins/cc/cctac.ml | 206 | ||||
| -rw-r--r-- | plugins/cc/g_congruence.ml4 | 2 |
6 files changed, 125 insertions, 139 deletions
diff --git a/plugins/cc/cc_plugin.mllib b/plugins/cc/cc_plugin.mlpack index 1bcfc537..27e903fd 100644 --- a/plugins/cc/cc_plugin.mllib +++ b/plugins/cc/cc_plugin.mlpack @@ -2,4 +2,3 @@ Ccalgo Ccproof Cctac G_congruence -Cc_plugin_mod diff --git a/plugins/cc/ccalgo.ml b/plugins/cc/ccalgo.ml index bc3d9ed5..bc53b113 100644 --- a/plugins/cc/ccalgo.ml +++ b/plugins/cc/ccalgo.ml @@ -10,7 +10,7 @@ (* Downey,Sethi and Tarjan. *) (* Plus some e-matching and constructor handling by P. Corbineau *) -open Errors +open CErrors open Util open Pp open Goptions @@ -25,7 +25,7 @@ let init_size=5 let cc_verbose=ref false let debug x = - if !cc_verbose then msg_debug x + if !cc_verbose then Feedback.msg_debug (x ()) let _= let gdopt= @@ -154,11 +154,6 @@ let rec term_equal t1 t2 = open Hashset.Combine -let hash_sorts_family = function -| InProp -> 0 -| InSet -> 1 -| InType -> 2 - let rec hash_term = function | Symb c -> combine 1 (hash_constr c) | Product (s1, s2) -> combine3 2 (Sorts.hash s1) (Sorts.hash s2) @@ -489,7 +484,7 @@ let build_subst uf subst = Array.map (fun i -> try term uf i - with e when Errors.noncritical e -> + with e when CErrors.noncritical e -> anomaly (Pp.str "incomplete matching")) subst @@ -603,7 +598,7 @@ let add_inst state (inst,int_subst) = Control.check_for_interrupt (); if state.rew_depth > 0 then if is_redundant state inst.qe_hyp_id int_subst then - debug (str "discarding redundant (dis)equality") + debug (fun () -> str "discarding redundant (dis)equality") else begin Identhash.add state.q_history inst.qe_hyp_id int_subst; @@ -618,7 +613,7 @@ let add_inst state (inst,int_subst) = state.rew_depth<-pred state.rew_depth; if inst.qe_pol then begin - debug ( + debug (fun () -> (str "Adding new equality, depth="++ int state.rew_depth) ++ fnl () ++ (str " [" ++ Termops.print_constr prf ++ str " : " ++ pr_term s ++ str " == " ++ pr_term t ++ str "]")); @@ -626,7 +621,7 @@ let add_inst state (inst,int_subst) = end else begin - debug ( + debug (fun () -> (str "Adding new disequality, depth="++ int state.rew_depth) ++ fnl () ++ (str " [" ++ Termops.print_constr prf ++ str " : " ++ pr_term s ++ str " <> " ++ pr_term t ++ str "]")); @@ -657,7 +652,7 @@ let join_path uf i j= min_path (down_path uf i [],down_path uf j []) let union state i1 i2 eq= - debug (str "Linking " ++ pr_idx_term state.uf i1 ++ + debug (fun () -> str "Linking " ++ pr_idx_term state.uf i1 ++ str " and " ++ pr_idx_term state.uf i2 ++ str "."); let r1= get_representative state.uf i1 and r2= get_representative state.uf i2 in @@ -698,7 +693,7 @@ let union state i1 i2 eq= let merge eq state = (* merge and no-merge *) debug - (str "Merging " ++ pr_idx_term state.uf eq.lhs ++ + (fun () -> str "Merging " ++ pr_idx_term state.uf eq.lhs ++ str " and " ++ pr_idx_term state.uf eq.rhs ++ str "."); let uf=state.uf in let i=find uf eq.lhs @@ -711,7 +706,7 @@ let merge eq state = (* merge and no-merge *) let update t state = (* update 1 and 2 *) debug - (str "Updating term " ++ pr_idx_term state.uf t ++ str "."); + (fun () -> str "Updating term " ++ pr_idx_term state.uf t ++ str "."); let (i,j) as sign = signature state.uf t in let (u,v) = subterms state.uf t in let rep = get_representative state.uf i in @@ -773,7 +768,7 @@ let process_constructor_mark t i rep pac state = let process_mark t m state = debug - (str "Processing mark for term " ++ pr_idx_term state.uf t ++ str "."); + (fun () -> str "Processing mark for term " ++ pr_idx_term state.uf t ++ str "."); let i=find state.uf t in let rep=get_representative state.uf i in match m with @@ -794,7 +789,7 @@ let check_disequalities state = else (str "No", check_aux q) in let _ = debug - (str "Checking if " ++ pr_idx_term state.uf dis.lhs ++ str " = " ++ + (fun () -> str "Checking if " ++ pr_idx_term state.uf dis.lhs ++ str " = " ++ pr_idx_term state.uf dis.rhs ++ str " ... " ++ info) in ans | [] -> None @@ -824,7 +819,7 @@ let __eps__ = Id.of_string "_eps_" let new_state_var typ state = let id = pf_get_new_id __eps__ state.gls in let {it=gl ; sigma=sigma} = state.gls in - let gls = Goal.V82.new_goal_with sigma gl [id,None,typ] in + let gls = Goal.V82.new_goal_with sigma gl [Context.Named.Declaration.LocalAssum (id,typ)] in state.gls<- gls; id @@ -979,7 +974,7 @@ let find_instances state = let pb_stack= init_pb_stack state in let res =ref [] in let _ = - debug (str "Running E-matching algorithm ... "); + debug (fun () -> str "Running E-matching algorithm ... "); try while true do Control.check_for_interrupt (); @@ -990,7 +985,7 @@ let find_instances state = !res let rec execute first_run state = - debug (str "Executing ... "); + debug (fun () -> str "Executing ... "); try while Control.check_for_interrupt (); @@ -1000,7 +995,7 @@ let rec execute first_run state = None -> if not(Int.Set.is_empty state.pa_classes) then begin - debug (str "First run was incomplete, completing ... "); + debug (fun () -> str "First run was incomplete, completing ... "); complete state; execute false state end @@ -1015,12 +1010,12 @@ let rec execute first_run state = end else begin - debug (str "Out of instances ... "); + debug (fun () -> str "Out of instances ... "); None end else begin - debug (str "Out of depth ... "); + debug (fun () -> str "Out of depth ... "); None end | Some dis -> Some diff --git a/plugins/cc/ccalgo.mli b/plugins/cc/ccalgo.mli index b73c8eef..c7fa2f56 100644 --- a/plugins/cc/ccalgo.mli +++ b/plugins/cc/ccalgo.mli @@ -120,7 +120,7 @@ val term_equal : term -> term -> bool val constr_of_term : term -> constr -val debug : Pp.std_ppcmds -> unit +val debug : (unit -> Pp.std_ppcmds) -> unit val forest : state -> forest diff --git a/plugins/cc/ccproof.ml b/plugins/cc/ccproof.ml index c188bf3b..f58847ca 100644 --- a/plugins/cc/ccproof.ml +++ b/plugins/cc/ccproof.ml @@ -9,7 +9,7 @@ (* This file uses the (non-compressed) union-find structure to generate *) (* proof-trees that will be transformed into proof-terms in cctac.ml4 *) -open Errors +open CErrors open Term open Ccalgo open Pp @@ -93,13 +93,13 @@ let pinject p c n a = p_rule=Inject(p,c,n,a)} let rec equal_proof uf i j= - debug (str "equal_proof " ++ pr_idx_term uf i ++ brk (1,20) ++ pr_idx_term uf j); + debug (fun () -> str "equal_proof " ++ pr_idx_term uf i ++ brk (1,20) ++ pr_idx_term uf j); if i=j then prefl (term uf i) else let (li,lj)=join_path uf i j in ptrans (path_proof uf i li) (psym (path_proof uf j lj)) and edge_proof uf ((i,j),eq)= - debug (str "edge_proof " ++ pr_idx_term uf i ++ brk (1,20) ++ pr_idx_term uf j); + debug (fun () -> str "edge_proof " ++ pr_idx_term uf i ++ brk (1,20) ++ pr_idx_term uf j); let pi=equal_proof uf i eq.lhs in let pj=psym (equal_proof uf j eq.rhs) in let pij= @@ -115,7 +115,7 @@ and edge_proof uf ((i,j),eq)= ptrans (ptrans pi pij) pj and constr_proof uf i ipac= - debug (str "constr_proof " ++ pr_idx_term uf i ++ brk (1,20)); + debug (fun () -> str "constr_proof " ++ pr_idx_term uf i ++ brk (1,20)); let t=find_oldest_pac uf i ipac in let eq_it=equal_proof uf i t in if ipac.args=[] then @@ -128,20 +128,20 @@ and constr_proof uf i ipac= ptrans eq_it (pcongr p (prefl targ)) and path_proof uf i l= - debug (str "path_proof " ++ pr_idx_term uf i ++ brk (1,20) ++ str "{" ++ + debug (fun () -> str "path_proof " ++ pr_idx_term uf i ++ brk (1,20) ++ str "{" ++ (prlist_with_sep (fun () -> str ",") (fun ((_,j),_) -> int j) l) ++ str "}"); match l with | [] -> prefl (term uf i) | x::q->ptrans (path_proof uf (snd (fst x)) q) (edge_proof uf x) and congr_proof uf i j= - debug (str "congr_proof " ++ pr_idx_term uf i ++ brk (1,20) ++ pr_idx_term uf j); + debug (fun () -> str "congr_proof " ++ pr_idx_term uf i ++ brk (1,20) ++ pr_idx_term uf j); let (i1,i2) = subterms uf i and (j1,j2) = subterms uf j in pcongr (equal_proof uf i1 j1) (equal_proof uf i2 j2) and ind_proof uf i ipac j jpac= - debug (str "ind_proof " ++ pr_idx_term uf i ++ brk (1,20) ++ pr_idx_term uf j); + debug (fun () -> str "ind_proof " ++ pr_idx_term uf i ++ brk (1,20) ++ pr_idx_term uf j); let p=equal_proof uf i j and p1=constr_proof uf i ipac and p2=constr_proof uf j jpac in diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml index 0baa5337..fd46d806 100644 --- a/plugins/cc/cctac.ml +++ b/plugins/cc/cctac.ml @@ -20,8 +20,10 @@ open Typing open Ccalgo open Ccproof open Pp -open Errors +open CErrors open Util +open Proofview.Notations +open Context.Rel.Declaration let reference dir s = lazy (Coqlib.gen_reference "CC" dir s) @@ -36,17 +38,17 @@ let _True = reference ["Init";"Logic"] "True" let _I = reference ["Init";"Logic"] "I" let whd env= - let infos=Closure.create_clos_infos Closure.betaiotazeta env in - (fun t -> Closure.whd_val infos (Closure.inject t)) + let infos=CClosure.create_clos_infos CClosure.betaiotazeta env in + (fun t -> CClosure.whd_val infos (CClosure.inject t)) let whd_delta env= - let infos=Closure.create_clos_infos Closure.betadeltaiota env in - (fun t -> Closure.whd_val infos (Closure.inject t)) + let infos=CClosure.create_clos_infos CClosure.all env in + (fun t -> CClosure.whd_val infos (CClosure.inject t)) (* decompose member of equality in an applicative format *) (** FIXME: evar leak *) -let sf_of env sigma c = sort_of env (ref sigma) c +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 @@ -80,8 +82,10 @@ let rec decompose_term env sigma t= | 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)) - | _ ->if closed0 t then (Symb t) else raise Not_found + (Appli (Symb (mkConst (Projection.constant p')), decompose_term env sigma c)) + | _ -> + let t = strip_outer_cast t in + if closed0 t then Symb t else raise Not_found (* decompose equality in members and type *) open Globnames @@ -151,7 +155,7 @@ let rec quantified_atom_of_constr env sigma nrels term = let patts=patterns_of_constr env sigma nrels atom in `Nrule patts else - quantified_atom_of_constr (Environ.push_rel (id,None,atom) env) sigma (succ nrels) ff + quantified_atom_of_constr (Environ.push_rel (LocalAssum (id,atom)) env) sigma (succ nrels) ff | _ -> let patts=patterns_of_constr env sigma nrels term in `Rule patts @@ -166,7 +170,7 @@ let litteral_of_constr env sigma term= else begin try - quantified_atom_of_constr (Environ.push_rel (id,None,atom) env) sigma 1 ff + quantified_atom_of_constr (Environ.push_rel (LocalAssum (id,atom)) env) sigma 1 ff with Not_found -> `Other (decompose_term env sigma term) end @@ -187,7 +191,8 @@ let make_prb gls depth additionnal_terms = let t = decompose_term env sigma c in ignore (add_term state t)) additionnal_terms; List.iter - (fun (id,_,e) -> + (fun decl -> + let (id,_,e) = Context.Named.Declaration.to_tuple decl in begin let cid=mkVar id in match litteral_of_constr env sigma e with @@ -220,24 +225,9 @@ let make_prb gls depth additionnal_terms = (* indhyps builds the array of arrays of constructor hyps for (ind largs) *) -let build_projection intype outtype (cstr:pconstructor) special default gls= - let env=pf_env gls in - let (h,argv) = try destApp intype with DestKO -> (intype,[||]) in - let ind,u=destInd h in - let types=Inductiveops.arities_of_constructors env (ind,u) in - let lp=Array.length types in - let ci=pred (snd(fst cstr)) in - let branch i= - let ti= prod_appvect types.(i) argv in - let rc=fst (decompose_prod_assum ti) in - let head= - if Int.equal i ci then special else default in - it_mkLambda_or_LetIn head rc in - let branches=Array.init lp branch in - let casee=mkRel 1 in - let pred=mkLambda(Anonymous,intype,outtype) in - let case_info=make_case_info (pf_env gls) ind RegularStyle in - let body= mkCase(case_info, pred, casee, branches) in +let build_projection intype (cstr:pconstructor) special default gls= + 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 mkLambda(Name id,intype,body) @@ -245,22 +235,34 @@ let build_projection intype outtype (cstr:pconstructor) special default gls= let _M =mkMeta -let app_global f args k = +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 = +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) let assert_before n c = - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.enter { 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) - end - + end } + +let refresh_type env evm ty = + Evarsolve.refresh_universes ~status:Evd.univ_flexible ~refreshset:true + (Some false) env evm ty + +let refresh_universes ty k = + Proofview.Goal.enter { 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) + end } + let rec proof_tac p : unit Proofview.tactic = - Proofview.Goal.nf_enter begin fun gl -> + Proofview.Goal.nf_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 @@ -268,35 +270,31 @@ let rec proof_tac p : unit Proofview.tactic = | SymAx c -> let l=constr_of_term p.p_lhs and r=constr_of_term p.p_rhs in - let typ = (* Termops.refresh_universes *) type_of l in - new_app_global _sym_eq [|typ;r;l;c|] exact_check + refresh_universes (type_of l) (fun typ -> + new_app_global _sym_eq [|typ;r;l;c|] exact_check) | Refl t -> let lr = constr_of_term t in - let typ = (* Termops.refresh_universes *) type_of lr in - new_app_global _refl_equal [|typ;constr_of_term t|] exact_check + refresh_universes (type_of lr) (fun typ -> + new_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 - let typ = (* Termops.refresh_universes *) (type_of t2) 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)] + Tacticals.New.tclTHENS (prf new_refine) [(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 and tf2=constr_of_term p1.p_rhs and tx2=constr_of_term p2.p_rhs in - let typf = (* Termops.refresh_universes *)(type_of tf1) in - let typx = (* Termops.refresh_universes *) (type_of tx1) in - let typfx = (* Termops.refresh_universes *) (type_of (mkApp (tf1,[|tx1|]))) in + 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 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 _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 prf = app_global _trans_eq [|typfx; @@ -310,96 +308,89 @@ let rec proof_tac p : unit Proofview.tactic = reflexivity; Tacticals.New.tclZEROMSG (Pp.str - "I don't know how to handle dependent equality")]] + "I don't know how to handle dependent equality")]]))) | Inject (prf,cstr,nargs,argind) -> let ti=constr_of_term prf.p_lhs in let tj=constr_of_term prf.p_rhs in let default=constr_of_term p.p_lhs in - let intype = (* Termops.refresh_universes *) (type_of ti) in - let outtype = (* Termops.refresh_universes *) (type_of default) in let special=mkRel (1+nargs-argind) in + refresh_universes (type_of ti) (fun intype -> + refresh_universes (type_of default) (fun outtype -> let proj = - Tacmach.New.of_old (build_projection intype outtype cstr special default) gl + Tacmach.New.of_old (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) + Tacticals.New.tclTHEN (Proofview.V82.tactic (injt refine)) (proof_tac prf))) with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e - end + end } let refute_tac c t1 t2 p = - Proofview.Goal.nf_enter begin fun gl -> + Proofview.Goal.nf_enter { enter = begin fun gl -> let tt1=constr_of_term t1 and tt2=constr_of_term t2 in - let intype = - Tacmach.New.of_old (fun gls -> (* Termops.refresh_universes *) (pf_unsafe_type_of gls tt1)) gl - in - let neweq= new_app_global _eq [|intype;tt1;tt2|] in let hid = Tacmach.New.of_old (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 Tacticals.New.tclTHENS (neweq (assert_before (Name hid))) [proof_tac p; simplest_elim false_t] - end + 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 convert_to_goal_tac c t1 t2 p = - Proofview.Goal.nf_enter begin fun gl -> + Proofview.Goal.nf_enter { enter = begin fun gl -> let tt1=constr_of_term t1 and tt2=constr_of_term t2 in - let sort = - Tacmach.New.of_old (fun gls -> (* Termops.refresh_universes *) (pf_unsafe_type_of gls tt2)) gl - in - 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 identity=mkLambda (Name x,sort,mkRel 1) in - let endt=app_global _eq_rect [|sort;tt1;identity;c;tt2;mkVar e|] 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 identity=mkLambda (Name x,sort,mkRel 1) 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)] - end + [proof_tac p; Proofview.V82.tactic (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 begin fun gl -> + Proofview.Goal.nf_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 false_t=mkApp (c2,[|mkVar h|]) in Tacticals.New.tclTHENS (assert_before (Name h) tt2) [convert_to_goal_tac c1 t1 t2 p; simplest_elim false_t] - end + end } let discriminate_tac (cstr,u as cstru) p = - Proofview.Goal.nf_enter begin fun gl -> + Proofview.Goal.nf_enter { enter = begin fun gl -> let t1=constr_of_term p.p_lhs and t2=constr_of_term p.p_rhs in - let intype = - Tacmach.New.of_old (fun gls -> (* Termops.refresh_universes *) (pf_unsafe_type_of gls t1)) gl - in + let env = Proofview.Goal.env gl in let concl = Proofview.Goal.concl gl in - (* let evm,outsort = Evd.new_sort_variable Evd.univ_rigid (project gls) in *) - (* let outsort = mkSort outsort in *) let xid = Tacmach.New.of_old (pf_get_new_id (Id.of_string "X")) gl in - (* let tid = Tacmach.New.of_old (pf_get_new_id (Id.of_string "t")) gl in *) - (* let identity=mkLambda(Name xid,outsort,mkLambda(Name tid,mkRel 1,mkRel 1)) in *) let identity = Universes.constr_of_global (Lazy.force _I) in - (* let trivial=pf_unsafe_type_of gls identity in *) let trivial = Universes.constr_of_global (Lazy.force _True) in - let evm, outtype = Evd.new_sort_variable Evd.univ_flexible (Proofview.Goal.sigma gl) 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 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 outtype cstru trivial concl) gl in + let proj = Tacmach.New.of_old (build_projection intype cstru trivial concl) gl in let injt=app_global _f_equal - [|intype;outtype;proj;t1;t2;mkVar hid|] in + [|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 + app_global _eq_rect + [|outtype;trivial;pred;identity;concl;injt|] k) in let neweq=new_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)]) - end + (Tacticals.New.tclTHENS (neweq (assert_before (Name hid))) + [proof_tac p; Proofview.V82.tactic (endt refine_exact_check)]) + end } (* wrap everything *) @@ -411,18 +402,18 @@ let build_term_to_complete uf meta pac = applistc (mkConstructU cinfo.ci_constr) all_args let cc_tactic depth additionnal_terms = - Proofview.Goal.nf_enter begin fun gl -> + Proofview.Goal.nf_enter { enter = begin fun gl -> Coqlib.check_required_library Coqlib.logic_module_name; - let _ = debug (Pp.str "Reading subgoal ...") in + 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 _ = debug (Pp.str "Problem built, solving ...") in + let _ = debug (fun () -> Pp.str "Problem built, solving ...") in let sol = execute true state in - let _ = debug (Pp.str "Computation completed.") in + let _ = debug (fun () -> Pp.str "Computation completed.") in let uf=forest state in match sol with None -> Tacticals.New.tclFAIL 0 (str "congruence failed") | Some reason -> - debug (Pp.str "Goal solved, generating proof ..."); + debug (fun () -> Pp.str "Goal solved, generating proof ..."); match reason with Discrimination (i,ipac,j,jpac) -> let p=build_proof uf (`Discr (i,ipac,j,jpac)) in @@ -436,10 +427,10 @@ let cc_tactic depth additionnal_terms = List.map (build_term_to_complete uf newmeta) (epsilons uf) in - Pp.msg_info + Feedback.msg_info (Pp.str "Goal is solvable by congruence but \ some arguments are missing."); - Pp.msg_info + Feedback.msg_info (Pp.str " Try " ++ hov 8 begin @@ -462,7 +453,7 @@ let cc_tactic depth additionnal_terms = convert_to_goal_tac id ta tb p | HeqnH (ida,idb) -> convert_to_hyp_tac ida ta idb tb p - end + end } let cc_fail gls = errorlabstrm "Congruence" (Pp.str "congruence failed.") @@ -482,11 +473,10 @@ let congruence_tac depth l = This isn't particularly related with congruence, apart from the fact that congruence is called internally. *) - + let mk_eq f c1 c2 k = Tacticals.New.pf_constr_of_global (Lazy.force f) (fun fc -> - Proofview.Goal.enter begin - fun gl -> + Proofview.Goal.enter { 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 @@ -494,10 +484,10 @@ let mk_eq f c1 c2 k = let evm, _ = type_of (pf_env gl) evm term in Tacticals.New.tclTHEN (Proofview.V82.tactic (Refiner.tclEVARS evm)) (k term) - end) - + end }) + let f_equal = - Proofview.Goal.nf_enter begin fun gl -> + Proofview.Goal.nf_enter { enter = begin fun gl -> let concl = Proofview.Goal.concl gl in let cut_eq c1 c2 = try (* type_of can raise an exception *) @@ -523,4 +513,4 @@ let f_equal = | Type_errors.TypeError _ -> Proofview.tclUNIT () | e -> Proofview.tclZERO ~info e end - end + end } diff --git a/plugins/cc/g_congruence.ml4 b/plugins/cc/g_congruence.ml4 index 5dbc340c..52a13511 100644 --- a/plugins/cc/g_congruence.ml4 +++ b/plugins/cc/g_congruence.ml4 @@ -9,6 +9,8 @@ (*i camlp4deps: "grammar/grammar.cma" i*) open Cctac +open Stdarg +open Constrarg DECLARE PLUGIN "cc_plugin" |