aboutsummaryrefslogtreecommitdiff
path: root/plugins/cc
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/cc')
-rw-r--r--plugins/cc/ccalgo.ml29
-rw-r--r--plugins/cc/ccalgo.mli5
-rw-r--r--plugins/cc/ccproof.ml5
-rw-r--r--plugins/cc/ccproof.mli1
-rw-r--r--plugins/cc/cctac.ml97
-rw-r--r--plugins/cc/cctac.mli1
-rw-r--r--plugins/cc/g_congruence.ml41
7 files changed, 72 insertions, 67 deletions
diff --git a/plugins/cc/ccalgo.ml b/plugins/cc/ccalgo.ml
index 5dea4631c4..5c7cad7ff5 100644
--- a/plugins/cc/ccalgo.ml
+++ b/plugins/cc/ccalgo.ml
@@ -10,6 +10,7 @@
(* Downey,Sethi and Tarjan. *)
(* Plus some e-matching and constructor handling by P. Corbineau *)
+open API
open CErrors
open Util
open Pp
@@ -61,7 +62,7 @@ module ST=struct
let enter t sign st=
if IntPairTable.mem st.toterm sign then
- anomaly ~label:"enter" (Pp.str "signature already entered")
+ anomaly ~label:"enter" (Pp.str "signature already entered.")
else
IntPairTable.replace st.toterm sign t;
IntTable.replace st.tosign t sign
@@ -135,7 +136,7 @@ let family_eq f1 f2 = match f1, f2 with
type term=
Symb of constr
- | Product of sorts * sorts
+ | Product of Sorts.t * Sorts.t
| Eps of Id.t
| Appli of term*term
| Constructor of cinfo (* constructor arity + nhyps *)
@@ -269,7 +270,7 @@ type state =
mutable rew_depth:int;
mutable changed:bool;
by_type: Int.Set.t Typehash.t;
- mutable gls:Proof_type.goal Tacmach.sigma}
+ mutable gls:Proof_type.goal Evd.sigma}
let dummy_node =
{
@@ -321,7 +322,7 @@ let find uf i= find_aux uf [] i
let get_representative uf i=
match uf.map.(i).clas with
Rep r -> r
- | _ -> anomaly ~label:"get_representative" (Pp.str "not a representative")
+ | _ -> anomaly ~label:"get_representative" (Pp.str "not a representative.")
let get_constructors uf i= uf.map.(i).constructors
@@ -339,7 +340,7 @@ let rec find_oldest_pac uf i pac=
let get_constructor_info uf i=
match uf.map.(i).term with
Constructor cinfo->cinfo
- | _ -> anomaly ~label:"get_constructor" (Pp.str "not a constructor")
+ | _ -> anomaly ~label:"get_constructor" (Pp.str "not a constructor.")
let size uf i=
(get_representative uf i).weight
@@ -384,7 +385,7 @@ let term uf i=uf.map.(i).term
let subterms uf i=
match uf.map.(i).vertex with
Node(j,k) -> (j,k)
- | _ -> anomaly ~label:"subterms" (Pp.str "not a node")
+ | _ -> anomaly ~label:"subterms" (Pp.str "not a node.")
let signature uf i=
let j,k=subterms uf i in (find uf j,find uf k)
@@ -456,13 +457,13 @@ let rec canonize_name sigma c =
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
+ let canon_const = Constant.make1 (Constant.canonical kn) in
(mkConstU (canon_const,u))
| Ind ((kn,i),u) ->
- let canon_mind = mind_of_kn (canonical_mind kn) in
+ let canon_mind = MutInd.make1 (MutInd.canonical kn) in
(mkIndU ((canon_mind,i),u))
| Construct (((kn,i),j),u) ->
- let canon_mind = mind_of_kn (canonical_mind kn) in
+ let canon_mind = MutInd.make1 (MutInd.canonical kn) in
mkConstructU (((canon_mind,i),j),u)
| Prod (na,t,ct) ->
mkProd (na,func t, func ct)
@@ -474,7 +475,7 @@ let rec canonize_name sigma c =
mkApp (func ct,Array.smartmap func l)
| Proj(p,c) ->
let p' = Projection.map (fun kn ->
- constant_of_kn (canonical_con kn)) p in
+ Constant.make1 (Constant.canonical kn)) p in
(mkProj (p', func c))
| _ -> c
@@ -485,7 +486,7 @@ let build_subst uf subst =
(fun i ->
try term uf i
with e when CErrors.noncritical e ->
- anomaly (Pp.str "incomplete matching"))
+ anomaly (Pp.str "incomplete matching."))
subst
let rec inst_pattern subst = function
@@ -750,7 +751,7 @@ let process_constructor_mark t i rep pac state =
state.combine;
f (n-1) q1 q2
| _-> anomaly ~label:"add_pacs"
- (Pp.str "weird error in injection subterms merge")
+ (Pp.str "weird error in injection subterms merge.")
in f cinfo.ci_nhyps opac.args pac.args
| Partial_applied | Partial _ ->
(* add_pac state.uf.map.(i) pac t; *)
@@ -841,7 +842,7 @@ let complete_one_class state i=
let ct = app (term state.uf i) typ pac.arity in
state.uf.epsilons <- pac :: state.uf.epsilons;
ignore (add_term state ct)
- | _ -> anomaly (Pp.str "wrong incomplete class")
+ | _ -> anomaly (Pp.str "wrong incomplete class.")
let complete state =
Int.Set.iter (complete_one_class state) state.pa_classes
@@ -981,7 +982,7 @@ let find_instances state =
Control.check_for_interrupt ();
do_match state res pb_stack
done;
- anomaly (Pp.str "get out of here !")
+ anomaly (Pp.str "get out of here!")
with Stack.Empty -> () in
!res
diff --git a/plugins/cc/ccalgo.mli b/plugins/cc/ccalgo.mli
index c7fa2f56fd..505029992a 100644
--- a/plugins/cc/ccalgo.mli
+++ b/plugins/cc/ccalgo.mli
@@ -6,6 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
+open API
open Util
open Term
open Names
@@ -30,7 +31,7 @@ type cinfo =
type term =
Symb of constr
- | Product of sorts * sorts
+ | Product of Sorts.t * Sorts.t
| Eps of Id.t
| Appli of term*term
| Constructor of cinfo (* constructor arity + nhyps *)
@@ -128,7 +129,7 @@ val axioms : forest -> (term * term) Constrhash.t
val epsilons : forest -> pa_constructor list
-val empty : int -> Proof_type.goal Tacmach.sigma -> state
+val empty : int -> Proof_type.goal Evd.sigma -> state
val add_term : state -> term -> int
diff --git a/plugins/cc/ccproof.ml b/plugins/cc/ccproof.ml
index f58847cafb..eecb7bc983 100644
--- a/plugins/cc/ccproof.ml
+++ b/plugins/cc/ccproof.ml
@@ -9,6 +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 API
open CErrors
open Term
open Ccalgo
@@ -47,7 +48,7 @@ let rec ptrans p1 p3=
{p_lhs=p1.p_lhs;
p_rhs=p3.p_rhs;
p_rule=Trans (p1,p3)}
- else anomaly (Pp.str "invalid cc transitivity")
+ else anomaly (Pp.str "invalid cc transitivity.")
let rec psym p =
match p.p_rule with
@@ -85,7 +86,7 @@ let rec nth_arg t n=
if n>0 then
nth_arg t1 (n-1)
else t2
- | _ -> anomaly ~label:"nth_arg" (Pp.str "not enough args")
+ | _ -> anomaly ~label:"nth_arg" (Pp.str "not enough args.")
let pinject p c n a =
{p_lhs=nth_arg p.p_lhs (n-a);
diff --git a/plugins/cc/ccproof.mli b/plugins/cc/ccproof.mli
index eacbfeac70..4e4d42f869 100644
--- a/plugins/cc/ccproof.mli
+++ b/plugins/cc/ccproof.mli
@@ -6,6 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
+open API
open Ccalgo
open Term
diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml
index 201726d1e6..1ce1660b32 100644
--- a/plugins/cc/cctac.ml
+++ b/plugins/cc/cctac.ml
@@ -8,6 +8,7 @@
(* This file is the interface between the c-c algorithm and Coq *)
+open API
open Evd
open Names
open Inductiveops
@@ -26,7 +27,7 @@ open Proofview.Notations
module RelDecl = Context.Rel.Declaration
module NamedDecl = Context.Named.Declaration
-let reference dir s = lazy (Coqlib.gen_reference "CC" dir s)
+let reference dir s = lazy (Coqlib.coq_reference "CC" dir s)
let _f_equal = reference ["Init";"Logic"] "f_equal"
let _eq_rect = reference ["Init";"Logic"] "eq_rect"
@@ -65,7 +66,7 @@ let rec decompose_term env sigma t=
| 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_mind = MutInd.make1 (MutInd.canonical mind) in
let canon_ind = canon_mind,i_ind in
let (oib,_)=Global.lookup_inductive (canon_ind) in
let nargs=constructor_nallargs_env env (canon_ind,i_con) in
@@ -75,16 +76,16 @@ let rec decompose_term env sigma t=
| 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 (Constr.mkIndU (canon_ind,u)))
+ let canon_mind = MutInd.make1 (MutInd.canonical mind) in
+ let canon_ind = canon_mind,i_ind in (Symb (Term.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 (Constr.mkConstU (canon_const,u)))
+ let canon_const = Constant.make1 (Constant.canonical c) in
+ (Symb (Term.mkConstU (canon_const,u)))
| Proj (p, c) ->
- let canon_const kn = constant_of_kn (canonical_con kn) in
+ let canon_const kn = Constant.make1 (Constant.canonical kn) in
let p' = Projection.map canon_const p in
- (Appli (Symb (Constr.mkConst (Projection.constant p')), decompose_term env sigma c))
+ (Appli (Symb (Term.mkConst (Projection.constant p')), decompose_term env sigma c))
| _ ->
let t = Termops.strip_outer_cast sigma t in
if closed0 sigma t then Symb (EConstr.to_constr sigma t) else raise Not_found
@@ -197,7 +198,7 @@ let make_prb gls depth additionnal_terms =
(fun decl ->
let id = NamedDecl.get_id decl in
begin
- let cid=Constr.mkVar id in
+ let cid=Term.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
@@ -231,9 +232,9 @@ let make_prb gls depth additionnal_terms =
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 sigma, 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)
+ sigma, mkLambda(Name id,intype,body)
(* generate an adhoc tactic following the proof tree *)
@@ -241,24 +242,20 @@ let app_global f args k =
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 (sigma, ev) = Evarutil.new_evar env sigma u 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 ->
+ Proofview.Goal.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
+ Refine.refine begin fun sigma ->
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
@@ -266,32 +263,33 @@ let app_global_with_holes f args n =
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 }
+ (!evdref, ans)
+ end
+ end
let assert_before n c =
- Proofview.Goal.s_enter { s_enter = begin fun gl ->
+ Proofview.Goal.enter begin fun gl ->
let evm, _ = Tacmach.New.pf_apply type_of gl c in
- Sigma.Unsafe.of_pair (assert_before n c, evm)
- end }
+ Proofview.tclTHEN (Proofview.Unsafe.tclEVARS evm)
+ (assert_before n c)
+ 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.s_enter { s_enter = begin fun gl ->
+ Proofview.Goal.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
- Sigma.Unsafe.of_pair (k ty, evm)
- end }
+ Proofview.tclTHEN (Proofview.Unsafe.tclEVARS evm) (k ty)
+ end
let constr_of_term c = EConstr.of_constr (constr_of_term c)
let rec proof_tac p : unit Proofview.tactic =
- Proofview.Goal.enter { enter = begin fun gl ->
+ Proofview.Goal.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
@@ -346,17 +344,18 @@ 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 =
+ let sigma, proj =
build_projection intype cstr special default gl
in
let injt=
app_global_with_holes _f_equal [|intype;outtype;proj;ti;tj|] 1 in
- Tacticals.New.tclTHEN injt (proof_tac prf)))
+ Tacticals.New.tclTHEN (Proofview.Unsafe.tclEVARS sigma)
+ (Tacticals.New.tclTHEN injt (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.enter { enter = begin fun gl ->
+ Proofview.Goal.enter begin fun gl ->
let tt1=constr_of_term t1 and tt2=constr_of_term t2 in
let hid = Tacmach.New.pf_get_new_id (Id.of_string "Heq") gl in
let false_t=mkApp (c,[|mkVar hid|]) in
@@ -365,16 +364,16 @@ 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 =
- Proofview.Goal.s_enter { s_enter = begin fun gl ->
+ Proofview.Goal.enter begin fun gl ->
let evm, _ = Tacmach.New.pf_apply type_of gl c in
- Sigma.Unsafe.of_pair (exact_check c, evm)
- end }
+ Proofview.tclTHEN (Proofview.Unsafe.tclEVARS evm) (exact_check c)
+ end
let convert_to_goal_tac c t1 t2 p =
- Proofview.Goal.enter { enter = begin fun gl ->
+ Proofview.Goal.enter begin fun gl ->
let tt1=constr_of_term t1 and tt2=constr_of_term t2 in
let k sort =
let neweq= app_global _eq [|sort;tt1;tt2|] in
@@ -385,21 +384,21 @@ let convert_to_goal_tac c t1 t2 p =
Tacticals.New.tclTHENS (neweq (assert_before (Name e)))
[proof_tac p; 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.enter { enter = begin fun gl ->
+ Proofview.Goal.enter begin fun gl ->
let tt2=constr_of_term t2 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;
simplest_elim false_t]
- end }
+ end
(* Essentially [assert (Heq : lhs = rhs) by proof_tac p; discriminate Heq] *)
let discriminate_tac cstru p =
- Proofview.Goal.enter { enter = begin fun gl ->
+ Proofview.Goal.enter begin fun gl ->
let lhs=constr_of_term p.p_lhs and rhs=constr_of_term p.p_rhs in
let env = Proofview.Goal.env gl in
let evm = Tacmach.New.project gl in
@@ -409,7 +408,7 @@ let discriminate_tac cstru p =
Tacticals.New.tclTHEN (Proofview.Unsafe.tclEVARS evm)
(Tacticals.New.tclTHENS (neweq (assert_before (Name hid)))
[proof_tac p; Equality.discrHyp hid])
- end }
+ end
(* wrap everything *)
@@ -420,7 +419,7 @@ let build_term_to_complete uf pac =
(applist (mkConstructU (kn, EInstance.make u), real_args), pac.arity)
let cc_tactic depth additionnal_terms =
- Proofview.Goal.enter { enter = begin fun gl ->
+ Proofview.Goal.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
@@ -476,7 +475,7 @@ let cc_tactic depth additionnal_terms =
let ida = EConstr.of_constr ida in
let idb = EConstr.of_constr idb in
convert_to_hyp_tac ida ta idb tb p
- end }
+ end
let cc_fail =
Tacticals.New.tclZEROMSG (Pp.str "congruence failed.")
@@ -499,17 +498,17 @@ 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.s_enter { s_enter = begin fun gl ->
+ Proofview.Goal.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
- Sigma.Unsafe.of_pair (k term, evm)
- end }
+ Proofview.tclTHEN (Proofview.Unsafe.tclEVARS evm) (k term)
+ end
let f_equal =
- Proofview.Goal.enter { enter = begin fun gl ->
+ Proofview.Goal.enter begin fun gl ->
let concl = Proofview.Goal.concl gl in
let sigma = Tacmach.New.project gl in
let cut_eq c1 c2 =
@@ -536,4 +535,4 @@ let f_equal =
| Pretype_errors.PretypeError _ | Type_errors.TypeError _ -> Proofview.tclUNIT ()
| e -> Proofview.tclZERO ~info e
end
- end }
+ end
diff --git a/plugins/cc/cctac.mli b/plugins/cc/cctac.mli
index b4bb62be8e..ef32d2b83e 100644
--- a/plugins/cc/cctac.mli
+++ b/plugins/cc/cctac.mli
@@ -7,6 +7,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
+open API
open EConstr
val proof_tac: Ccproof.proof -> unit Proofview.tactic
diff --git a/plugins/cc/g_congruence.ml4 b/plugins/cc/g_congruence.ml4
index 7e76854b16..43b150c346 100644
--- a/plugins/cc/g_congruence.ml4
+++ b/plugins/cc/g_congruence.ml4
@@ -8,6 +8,7 @@
(*i camlp4deps: "grammar/grammar.cma" i*)
+open API
open Ltac_plugin
open Cctac
open Stdarg
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-29 14:31:11 +0000