aboutsummaryrefslogtreecommitdiff
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.ml61
-rw-r--r--plugins/cc/ccalgo.mli12
-rw-r--r--plugins/cc/ccproof.ml16
-rw-r--r--plugins/cc/ccproof.mli3
-rw-r--r--plugins/cc/cctac.ml253
-rw-r--r--plugins/cc/g_congruence.ml43
7 files changed, 175 insertions, 174 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 29bca8622b..bc53b113df 100644
--- a/plugins/cc/ccalgo.ml
+++ b/plugins/cc/ccalgo.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
@@ -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=
@@ -129,14 +129,14 @@ type cinfo=
ci_nhyps: int} (* # projectable args *)
let family_eq f1 f2 = match f1, f2 with
-| InProp, InProp
-| InSet, InSet
-| InType, InType -> true
-| _ -> false
+ | Prop Pos, Prop Pos
+ | Prop Null, Prop Null
+ | Type _, Type _ -> true
+ | _ -> false
type term=
Symb of constr
- | Product of sorts_family * sorts_family
+ | Product of sorts * sorts
| Eps of Id.t
| Appli of term*term
| Constructor of cinfo (* constructor arity + nhyps *)
@@ -154,14 +154,9 @@ 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 (hash_sorts_family s1) (hash_sorts_family s2)
+ | Product (s1, s2) -> combine3 2 (Sorts.hash s1) (Sorts.hash s2)
| Eps i -> combine 3 (Id.hash i)
| Appli (t1, t2) -> combine3 4 (hash_term t1) (hash_term t2)
| Constructor {ci_constr=(c,u); ci_arity=i; ci_nhyps=j} -> combine4 5 (constructor_hash c) i j
@@ -425,8 +420,8 @@ let _B_ = Name (Id.of_string "A")
let _body_ = mkProd(Anonymous,mkRel 2,mkRel 2)
let cc_product s1 s2 =
- mkLambda(_A_,mkSort(Universes.new_sort_in_family s1),
- mkLambda(_B_,mkSort(Universes.new_sort_in_family s2),_body_))
+ mkLambda(_A_,mkSort(s1),
+ mkLambda(_B_,mkSort(s2),_body_))
let rec constr_of_term = function
Symb s-> applist_projection s []
@@ -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
@@ -513,7 +508,7 @@ let rec add_term state t=
Not_found ->
let b=next uf in
let trm = constr_of_term t in
- let typ = pf_type_of state.gls trm in
+ let typ = pf_unsafe_type_of state.gls trm in
let typ = canonize_name typ in
let new_node=
match t with
@@ -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
@@ -836,7 +831,7 @@ let complete_one_class state i=
let _,etyp,rest= destProd typ in
let id = new_state_var etyp state in
app (Appli(t,Eps id)) (substl [mkVar id] rest) (n-1) in
- let _c = pf_type_of state.gls
+ let _c = pf_unsafe_type_of state.gls
(constr_of_term (term state.uf pac.cnode)) in
let _args =
List.map (fun i -> constr_of_term (term state.uf i))
@@ -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 c72843d55f..c7fa2f56fd 100644
--- a/plugins/cc/ccalgo.mli
+++ b/plugins/cc/ccalgo.mli
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
@@ -20,8 +20,8 @@ type pa_fun=
fnargs:int}
-module PafMap : Map.S with type key = pa_fun
-module PacMap : Map.S with type key = pa_constructor
+module PafMap : CSig.MapS with type key = pa_fun
+module PacMap : CSig.MapS with type key = pa_constructor
type cinfo =
{ci_constr: pconstructor; (* inductive type *)
@@ -30,7 +30,7 @@ type cinfo =
type term =
Symb of constr
- | Product of sorts_family * sorts_family
+ | Product of sorts * sorts
| Eps of Id.t
| Appli of term*term
| Constructor of cinfo (* constructor arity + nhyps *)
@@ -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
@@ -185,7 +185,7 @@ val empty_forest: unit -> forest
(*type pa_constructor
-module PacMap:Map.S with type key=pa_constructor
+module PacMap:CSig.MapS with type key=pa_constructor
type term =
Symb of Term.constr
diff --git a/plugins/cc/ccproof.ml b/plugins/cc/ccproof.ml
index 42c03234b2..f58847cafb 100644
--- a/plugins/cc/ccproof.ml
+++ b/plugins/cc/ccproof.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
@@ -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/ccproof.mli b/plugins/cc/ccproof.mli
index 0e0eb6d2a1..eacbfeac70 100644
--- a/plugins/cc/ccproof.mli
+++ b/plugins/cc/ccproof.mli
@@ -1,13 +1,12 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
open Ccalgo
-open Names
open Term
type rule=
diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml
index 7110e5b232..b5ca2f50fc 100644
--- a/plugins/cc/cctac.ml
+++ b/plugins/cc/cctac.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
@@ -20,10 +20,14 @@ open Typing
open Ccalgo
open Ccproof
open Pp
-open Errors
+open CErrors
open Util
+open Proofview.Notations
-let reference dir s = Coqlib.gen_reference "CC" dir s
+module RelDecl = Context.Rel.Declaration
+module NamedDecl = Context.Named.Declaration
+
+let reference dir s = lazy (Coqlib.gen_reference "CC" dir s)
let _f_equal = reference ["Init";"Logic"] "f_equal"
let _eq_rect = reference ["Init";"Logic"] "eq_rect"
@@ -36,17 +40,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 = family_of_sort (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 +84,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 = Termops.strip_outer_cast t in
+ if closed0 t then Symb t else raise Not_found
(* decompose equality in members and type *)
open Globnames
@@ -91,7 +97,7 @@ let atom_of_constr env sigma term =
let kot = kind_of_term wh in
match kot with
App (f,args)->
- if is_global _eq f && Int.equal (Array.length args) 3
+ if is_global (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))
@@ -126,7 +132,7 @@ 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 _eq f && Int.equal (Array.length args) 3
+ if is_global (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
@@ -147,11 +153,11 @@ let patterns_of_constr env sigma nrels term=
let rec quantified_atom_of_constr env sigma nrels term =
match kind_of_term (whd_delta env term) with
Prod (id,atom,ff) ->
- if is_global _False ff then
+ if is_global (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 (id,None,atom) env) sigma (succ nrels) ff
+ quantified_atom_of_constr (Environ.push_rel (RelDecl.LocalAssum (id,atom)) env) sigma (succ nrels) ff
| _ ->
let patts=patterns_of_constr env sigma nrels term in
`Rule patts
@@ -159,14 +165,14 @@ let rec quantified_atom_of_constr env sigma nrels term =
let litteral_of_constr env sigma term=
match kind_of_term (whd_delta env term) with
| Prod (id,atom,ff) ->
- if is_global _False ff then
+ if is_global (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 (id,None,atom) env) sigma 1 ff
+ quantified_atom_of_constr (Environ.push_rel (RelDecl.LocalAssum (id,atom)) env) sigma 1 ff
with Not_found ->
`Other (decompose_term env sigma term)
end
@@ -187,10 +193,11 @@ 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 = NamedDecl.get_id decl in
begin
let cid=mkVar id in
- match litteral_of_constr env sigma e with
+ 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
| `Other ph ->
@@ -220,24 +227,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,52 +237,66 @@ let build_projection intype outtype (cstr:pconstructor) special default gls=
let _M =mkMeta
-let app_global f args k =
- Tacticals.pf_constr_of_global f (fun fc -> k (mkApp (fc, args)))
+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 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)
+let assert_before n c =
+ 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 }
+
+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 ->
- let type_of t = Tacmach.New.pf_type_of gl t in
+ 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
Ax c -> exact_check c
| 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;
@@ -302,98 +308,91 @@ let rec proof_tac p : unit Proofview.tactic =
Tacticals.New.tclFIRST
[Tacticals.New.tclTHEN (Proofview.V82.tactic (lemma2 refine)) (proof_tac p2);
reflexivity;
- Proofview.tclZERO (UserError ("Congruence" ,
+ 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_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 e_type_of gl c in
+ 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_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_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 _I in
- (* let trivial=pf_type_of gls identity in *)
- let trivial = Universes.constr_of_global _True in
- let evm, outtype = Evd.new_sort_variable Evd.univ_flexible (Proofview.Goal.sigma gl) in
+ let identity = Universes.constr_of_global (Lazy.force _I) in
+ let trivial = Universes.constr_of_global (Lazy.force _True) 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 *)
@@ -405,18 +404,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
@@ -430,10 +429,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
@@ -456,10 +455,10 @@ 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.")
+ user_err ~hdr:"Congruence" (Pp.str "congruence failed.")
let congruence_tac depth l =
Tacticals.New.tclORELSE
@@ -477,23 +476,31 @@ let congruence_tac depth l =
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 { 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 })
+
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 type_of = Tacmach.New.pf_type_of gl in
let cut_eq c1 c2 =
try (* type_of can raise an exception *)
- let ty = (* Termops.refresh_universes *) (type_of c1) in
- if eq_constr_nounivs c1 c2 then Proofview.tclUNIT ()
- else
- Tacticals.New.tclTRY (Tacticals.New.tclTHEN
- ((new_app_global _eq [|ty; c1; c2|]) Tactics.cut)
- (Tacticals.New.tclTRY ((new_app_global _refl_equal [||]) apply)))
+ Tacticals.New.tclTHENS
+ (mk_eq _eq c1 c2 Tactics.cut)
+ [Proofview.tclUNIT ();Tacticals.New.tclTRY ((new_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 _eq r ->
+ | App (r,[|_;t;t'|]) when Globnames.is_global (Lazy.force _eq) r ->
begin match kind_of_term t, kind_of_term t' with
| App (f,v), App (f',v') when Int.equal (Array.length v) (Array.length v') ->
let rec cuts i =
@@ -508,4 +515,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 aa31c6f078..6f6811334d 100644
--- a/plugins/cc/g_congruence.ml4
+++ b/plugins/cc/g_congruence.ml4
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
@@ -9,6 +9,7 @@
(*i camlp4deps: "grammar/grammar.cma" i*)
open Cctac
+open Stdarg
DECLARE PLUGIN "cc_plugin"
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-30 21:11:45 +0000