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 | 13 | ||||
| -rw-r--r-- | plugins/cc/ccproof.ml | 2 | ||||
| -rw-r--r-- | plugins/cc/cctac.ml | 99 | ||||
| -rw-r--r-- | plugins/cc/g_congruence.ml4 | 2 |
5 files changed, 50 insertions, 67 deletions
diff --git a/plugins/cc/cc_plugin.mllib b/plugins/cc/cc_plugin.mlpack index 1bcfc5378b..27e903fd38 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 5d16edfc6a..bc53b113df 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 @@ -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 diff --git a/plugins/cc/ccproof.ml b/plugins/cc/ccproof.ml index d2bbaf6a7d..f58847cafb 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 diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml index c8d857b31f..fd46d80695 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 @@ -153,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 @@ -168,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 @@ -189,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 @@ -222,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) @@ -256,25 +244,25 @@ let new_app_global f args k = 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 begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let env = Proofview.Goal.env gl in - let evm = Proofview.Goal.sigma 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 + 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 @@ -328,17 +316,17 @@ let rec proof_tac p : unit Proofview.tactic = 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 + let proj = + 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))) 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 hid = Tacmach.New.of_old (pf_get_new_id (Id.of_string "Heq")) gl in let false_t=mkApp (c,[|mkVar hid|]) in @@ -347,14 +335,14 @@ let refute_tac c t1 t2 p = 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 + 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 -> +let convert_to_goal_tac c t1 t2 p = + Proofview.Goal.nf_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 @@ -365,33 +353,33 @@ let convert_to_goal_tac c t1 t2 p = Tacticals.New.tclTHENS (neweq (assert_before (Name e))) [proof_tac p; Proofview.V82.tactic (endt refine_exact_check)] in refresh_universes (Tacmach.New.pf_unsafe_type_of gl tt2) k - end + 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 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 identity = Universes.constr_of_global (Lazy.force _I) in let trivial = Universes.constr_of_global (Lazy.force _True) in - let evm = 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 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 let endt k = @@ -402,7 +390,7 @@ let discriminate_tac (cstr,u as cstru) p = 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 + end } (* wrap everything *) @@ -414,7 +402,7 @@ 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 (fun () -> Pp.str "Reading subgoal ...") in let state = Tacmach.New.of_old (fun gls -> make_prb gls depth additionnal_terms) gl in @@ -439,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 @@ -465,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.") @@ -488,8 +476,7 @@ 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 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 @@ -497,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 *) @@ -526,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 5dbc340caa..52a1351199 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" |