summaryrefslogtreecommitdiff
path: root/plugins/cc
diff options
context:
space:
mode:
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.ml39
-rw-r--r--plugins/cc/ccalgo.mli2
-rw-r--r--plugins/cc/ccproof.ml14
-rw-r--r--plugins/cc/cctac.ml206
-rw-r--r--plugins/cc/g_congruence.ml42
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"
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-19 00:17:51 +0000