aboutsummaryrefslogtreecommitdiff
path: root/plugins/cc
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/cc')
-rw-r--r--plugins/cc/ccalgo.ml65
-rw-r--r--plugins/cc/ccalgo.mli6
-rw-r--r--plugins/cc/ccproof.ml54
-rw-r--r--plugins/cc/ccproof.mli12
-rw-r--r--plugins/cc/cctac.ml20
5 files changed, 75 insertions, 82 deletions
diff --git a/plugins/cc/ccalgo.ml b/plugins/cc/ccalgo.ml
index f26ec0f401..048ec56dee 100644
--- a/plugins/cc/ccalgo.ml
+++ b/plugins/cc/ccalgo.ml
@@ -17,6 +17,7 @@ open Pp
open Names
open Sorts
open Constr
+open Context
open Vars
open Goptions
open Tacmach
@@ -26,14 +27,10 @@ let init_size=5
let cc_verbose=ref false
-let print_constr t =
- let sigma, env = Pfedit.get_current_context () in
- Printer.pr_econstr_env env sigma t
-
let debug x =
if !cc_verbose then Feedback.msg_debug (x ())
-let _=
+let () =
let gdopt=
{ optdepr=false;
optname="Congruence Verbose";
@@ -61,7 +58,7 @@ module ST=struct
type t = {toterm: int IntPairTable.t;
tosign: (int * int) IntTable.t}
- let empty ()=
+ let empty () =
{toterm=IntPairTable.create init_size;
tosign=IntTable.create init_size}
@@ -321,7 +318,7 @@ let compress_path uf i j = uf.map.(j).cpath<-i
let rec find_aux uf visited i=
let j = uf.map.(i).cpath in
- if j<0 then let _ = List.iter (compress_path uf i) visited in i else
+ if j<0 then let () = List.iter (compress_path uf i) visited in i else
find_aux uf (i::visited) j
let find uf i= find_aux uf [] i
@@ -333,9 +330,6 @@ let get_representative uf i=
let get_constructors uf i= uf.map.(i).constructors
-let find_pac uf i pac =
- PacMap.find pac (get_constructors uf i)
-
let rec find_oldest_pac uf i pac=
try PacMap.find pac (get_constructors uf i) with
Not_found ->
@@ -424,11 +418,11 @@ let new_representative typ =
let _A_ = Name (Id.of_string "A")
let _B_ = Name (Id.of_string "A")
-let _body_ = mkProd(Anonymous,mkRel 2,mkRel 2)
+let _body_ = mkProd(make_annot Anonymous Sorts.Relevant,mkRel 2,mkRel 2)
let cc_product s1 s2 =
- mkLambda(_A_,mkSort(s1),
- mkLambda(_B_,mkSort(s2),_body_))
+ mkLambda(make_annot _A_ Sorts.Relevant,mkSort(s1),
+ mkLambda(make_annot _B_ Sorts.Relevant,mkSort(s2),_body_))
let rec constr_of_term = function
Symb s-> s
@@ -455,11 +449,11 @@ let rec canonize_name sigma c =
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)
+ mkProd (na,func t, func ct)
| Lambda (na,t,ct) ->
- mkLambda (na, func t,func ct)
+ mkLambda (na, func t,func ct)
| LetIn (na,b,t,ct) ->
- mkLetIn (na, func b,func t,func ct)
+ mkLetIn (na, func b,func t,func ct)
| App (ct,l) ->
mkApp (func ct,Array.Smart.map func l)
| Proj(p,c) ->
@@ -486,11 +480,11 @@ let rec inst_pattern subst = function
(fun spat f -> Appli (f,inst_pattern subst spat))
args t
-let pr_idx_term uf i = str "[" ++ int i ++ str ":=" ++
- print_constr (EConstr.of_constr (constr_of_term (term uf i))) ++ str "]"
+let pr_idx_term env sigma uf i = str "[" ++ int i ++ str ":=" ++
+ Printer.pr_econstr_env env sigma (EConstr.of_constr (constr_of_term (term uf i))) ++ str "]"
-let pr_term t = str "[" ++
- print_constr (EConstr.of_constr (constr_of_term t)) ++ str "]"
+let pr_term env sigma t = str "[" ++
+ Printer.pr_econstr_env env sigma (EConstr.of_constr (constr_of_term t)) ++ str "]"
let rec add_term state t=
let uf=state.uf in
@@ -605,16 +599,16 @@ let add_inst state (inst,int_subst) =
begin
debug (fun () ->
(str "Adding new equality, depth="++ int state.rew_depth) ++ fnl () ++
- (str " [" ++ print_constr (EConstr.of_constr prf) ++ str " : " ++
- pr_term s ++ str " == " ++ pr_term t ++ str "]"));
+ (str " [" ++ Printer.pr_econstr_env state.env state.sigma (EConstr.of_constr prf) ++ str " : " ++
+ pr_term state.env state.sigma s ++ str " == " ++ pr_term state.env state.sigma t ++ str "]"));
add_equality state prf s t
end
else
begin
debug (fun () ->
(str "Adding new disequality, depth="++ int state.rew_depth) ++ fnl () ++
- (str " [" ++ print_constr (EConstr.of_constr prf) ++ str " : " ++
- pr_term s ++ str " <> " ++ pr_term t ++ str "]"));
+ (str " [" ++ Printer.pr_econstr_env state.env state.sigma (EConstr.of_constr prf) ++ str " : " ++
+ pr_term state.env state.sigma s ++ str " <> " ++ pr_term state.env state.sigma t ++ str "]"));
add_disequality state (Hyp prf) s t
end
end
@@ -642,8 +636,8 @@ let join_path uf i j=
min_path (down_path uf i [],down_path uf j [])
let union state i1 i2 eq=
- debug (fun () -> str "Linking " ++ pr_idx_term state.uf i1 ++
- str " and " ++ pr_idx_term state.uf i2 ++ str ".");
+ debug (fun () -> str "Linking " ++ pr_idx_term state.env state.sigma state.uf i1 ++
+ str " and " ++ pr_idx_term state.env state.sigma state.uf i2 ++ str ".");
let r1= get_representative state.uf i1
and r2= get_representative state.uf i2 in
link state.uf i1 i2 eq;
@@ -683,8 +677,8 @@ let union state i1 i2 eq=
let merge eq state = (* merge and no-merge *)
debug
- (fun () -> str "Merging " ++ pr_idx_term state.uf eq.lhs ++
- str " and " ++ pr_idx_term state.uf eq.rhs ++ str ".");
+ (fun () -> str "Merging " ++ pr_idx_term state.env state.sigma state.uf eq.lhs ++
+ str " and " ++ pr_idx_term state.env state.sigma state.uf eq.rhs ++ str ".");
let uf=state.uf in
let i=find uf eq.lhs
and j=find uf eq.rhs in
@@ -696,7 +690,7 @@ let merge eq state = (* merge and no-merge *)
let update t state = (* update 1 and 2 *)
debug
- (fun () -> str "Updating term " ++ pr_idx_term state.uf t ++ str ".");
+ (fun () -> str "Updating term " ++ pr_idx_term state.env state.sigma 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
@@ -758,7 +752,7 @@ let process_constructor_mark t i rep pac state =
let process_mark t m state =
debug
- (fun () -> str "Processing mark for term " ++ pr_idx_term state.uf t ++ str ".");
+ (fun () -> str "Processing mark for term " ++ pr_idx_term state.env state.sigma state.uf t ++ str ".");
let i=find state.uf t in
let rep=get_representative state.uf i in
match m with
@@ -779,8 +773,8 @@ let check_disequalities state =
else (str "No", check_aux q)
in
let _ = debug
- (fun () -> str "Checking if " ++ pr_idx_term state.uf dis.lhs ++ str " = " ++
- pr_idx_term state.uf dis.rhs ++ str " ... " ++ info) in
+ (fun () -> str "Checking if " ++ pr_idx_term state.env state.sigma state.uf dis.lhs ++ str " = " ++
+ pr_idx_term state.env state.sigma state.uf dis.rhs ++ str " ... " ++ info) in
ans
| [] -> None
in
@@ -809,7 +803,8 @@ let __eps__ = Id.of_string "_eps_"
let new_state_var typ state =
let ids = Environ.ids_of_named_context_val (Environ.named_context_val state.env) in
let id = Namegen.next_ident_away __eps__ ids in
- state.env<- EConstr.push_named (Context.Named.Declaration.LocalAssum (id,typ)) state.env;
+ let r = Sorts.Relevant in (* TODO relevance *)
+ state.env<- EConstr.push_named (Context.Named.Declaration.LocalAssum (make_annot id r,typ)) state.env;
id
let complete_one_class state i=
@@ -817,9 +812,9 @@ let complete_one_class state i=
Partial pac ->
let rec app t typ n =
if n<=0 then t else
- let _,etyp,rest= destProd typ in
+ let _,etyp,rest= destProd typ in
let id = new_state_var (EConstr.of_constr etyp) state in
- app (Appli(t,Eps id)) (substl [mkVar id] rest) (n-1) in
+ app (Appli(t,Eps id)) (substl [mkVar id] rest) (n-1) in
let _c = Typing.unsafe_type_of state.env state.sigma
(EConstr.of_constr (constr_of_term (term state.uf pac.cnode))) in
let _c = EConstr.Unsafe.to_constr _c in
diff --git a/plugins/cc/ccalgo.mli b/plugins/cc/ccalgo.mli
index 4ebc6a135a..5066c3931d 100644
--- a/plugins/cc/ccalgo.mli
+++ b/plugins/cc/ccalgo.mli
@@ -145,8 +145,6 @@ val tail_pac : pa_constructor -> pa_constructor
val find : forest -> int -> int
-val find_pac : forest -> int -> pa_constructor -> int
-
val find_oldest_pac : forest -> int -> pa_constructor -> int
val term : forest -> int -> term
@@ -171,7 +169,7 @@ val find_instances : state -> (quant_eq * int array) list
val execute : bool -> state -> explanation option
-val pr_idx_term : forest -> int -> Pp.t
+val pr_idx_term : Environ.env -> Evd.evar_map -> forest -> int -> Pp.t
val empty_forest: unit -> forest
@@ -257,5 +255,3 @@ val find_contradiction : UF.t ->
(Names.Id.t * (int * int)) list ->
(Names.Id.t * (int * int))
*)
-
-
diff --git a/plugins/cc/ccproof.ml b/plugins/cc/ccproof.ml
index 1f1fa9c99a..4f46f8327a 100644
--- a/plugins/cc/ccproof.ml
+++ b/plugins/cc/ccproof.ml
@@ -94,65 +94,65 @@ let pinject p c n a =
p_rhs=nth_arg p.p_rhs (n-a);
p_rule=Inject(p,c,n,a)}
-let rec equal_proof uf i j=
- debug (fun () -> str "equal_proof " ++ pr_idx_term uf i ++ brk (1,20) ++ pr_idx_term uf j);
+let rec equal_proof env sigma uf i j=
+ debug (fun () -> str "equal_proof " ++ pr_idx_term env sigma uf i ++ brk (1,20) ++ pr_idx_term env sigma 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))
+ ptrans (path_proof env sigma uf i li) (psym (path_proof env sigma uf j lj))
-and edge_proof uf ((i,j),eq)=
- 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
+and edge_proof env sigma uf ((i,j),eq)=
+ debug (fun () -> str "edge_proof " ++ pr_idx_term env sigma uf i ++ brk (1,20) ++ pr_idx_term env sigma uf j);
+ let pi=equal_proof env sigma uf i eq.lhs in
+ let pj=psym (equal_proof env sigma uf j eq.rhs) in
let pij=
match eq.rule with
Axiom (s,reversed)->
if reversed then psymax (axioms uf) s
else pax (axioms uf) s
- | Congruence ->congr_proof uf eq.lhs eq.rhs
+ | Congruence ->congr_proof env sigma uf eq.lhs eq.rhs
| Injection (ti,ipac,tj,jpac,k) -> (* pi_k ipac = p_k jpac *)
- let p=ind_proof uf ti ipac tj jpac in
+ let p=ind_proof env sigma uf ti ipac tj jpac in
let cinfo= get_constructor_info uf ipac.cnode in
pinject p cinfo.ci_constr cinfo.ci_nhyps k in
ptrans (ptrans pi pij) pj
-and constr_proof uf i ipac=
- debug (fun () -> str "constr_proof " ++ pr_idx_term uf i ++ brk (1,20));
+and constr_proof env sigma uf i ipac=
+ debug (fun () -> str "constr_proof " ++ pr_idx_term env sigma uf i ++ brk (1,20));
let t=find_oldest_pac uf i ipac in
- let eq_it=equal_proof uf i t in
+ let eq_it=equal_proof env sigma uf i t in
if ipac.args=[] then
eq_it
else
let fipac=tail_pac ipac in
let (fi,arg)=subterms uf t in
let targ=term uf arg in
- let p=constr_proof uf fi fipac in
+ let p=constr_proof env sigma uf fi fipac in
ptrans eq_it (pcongr p (prefl targ))
-and path_proof uf i l=
- debug (fun () -> str "path_proof " ++ pr_idx_term uf i ++ brk (1,20) ++ str "{" ++
+and path_proof env sigma uf i l=
+ debug (fun () -> str "path_proof " ++ pr_idx_term env sigma 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)
+ | x::q->ptrans (path_proof env sigma uf (snd (fst x)) q) (edge_proof env sigma uf x)
-and congr_proof uf i j=
- debug (fun () -> str "congr_proof " ++ pr_idx_term uf i ++ brk (1,20) ++ pr_idx_term uf j);
+and congr_proof env sigma uf i j=
+ debug (fun () -> str "congr_proof " ++ pr_idx_term env sigma uf i ++ brk (1,20) ++ pr_idx_term env sigma 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)
+ pcongr (equal_proof env sigma uf i1 j1) (equal_proof env sigma uf i2 j2)
-and ind_proof uf i ipac j jpac=
- 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
+and ind_proof env sigma uf i ipac j jpac=
+ debug (fun () -> str "ind_proof " ++ pr_idx_term env sigma uf i ++ brk (1,20) ++ pr_idx_term env sigma uf j);
+ let p=equal_proof env sigma uf i j
+ and p1=constr_proof env sigma uf i ipac
+ and p2=constr_proof env sigma uf j jpac in
ptrans (psym p1) (ptrans p p2)
-let build_proof uf=
+let build_proof env sigma uf=
function
- | `Prove (i,j) -> equal_proof uf i j
- | `Discr (i,ci,j,cj)-> ind_proof uf i ci j cj
+ | `Prove (i,j) -> equal_proof env sigma uf i j
+ | `Discr (i,ci,j,cj)-> ind_proof env sigma uf i ci j cj
diff --git a/plugins/cc/ccproof.mli b/plugins/cc/ccproof.mli
index bebef241e1..9ea31259c1 100644
--- a/plugins/cc/ccproof.mli
+++ b/plugins/cc/ccproof.mli
@@ -41,20 +41,20 @@ val pinject : proof -> pconstructor -> int -> int -> proof
(** Proof building functions *)
-val equal_proof : forest -> int -> int -> proof
+val equal_proof : Environ.env -> Evd.evar_map -> forest -> int -> int -> proof
-val edge_proof : forest -> (int*int)*equality -> proof
+val edge_proof : Environ.env -> Evd.evar_map -> forest -> (int*int)*equality -> proof
-val path_proof : forest -> int -> ((int*int)*equality) list -> proof
+val path_proof : Environ.env -> Evd.evar_map -> forest -> int -> ((int*int)*equality) list -> proof
-val congr_proof : forest -> int -> int -> proof
+val congr_proof : Environ.env -> Evd.evar_map -> forest -> int -> int -> proof
-val ind_proof : forest -> int -> pa_constructor -> int -> pa_constructor -> proof
+val ind_proof : Environ.env -> Evd.evar_map -> forest -> int -> pa_constructor -> int -> pa_constructor -> proof
(** Main proof building function *)
val build_proof :
- forest ->
+ Environ.env -> Evd.evar_map -> forest ->
[ `Discr of int * pa_constructor * int * pa_constructor
| `Prove of int * int ] -> proof
diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml
index 055d36747d..50fc2448fc 100644
--- a/plugins/cc/cctac.ml
+++ b/plugins/cc/cctac.ml
@@ -15,6 +15,7 @@ open Names
open Inductiveops
open Declarations
open Constr
+open Context
open EConstr
open Vars
open Tactics
@@ -151,19 +152,19 @@ let patterns_of_constr env sigma nrels term=
let rec quantified_atom_of_constr env sigma nrels term =
match EConstr.kind sigma (whd_delta env sigma term) with
- Prod (id,atom,ff) ->
+ Prod (id,atom,ff) ->
if is_global sigma (Lazy.force _False) ff then
let patts=patterns_of_constr env sigma nrels atom in
`Nrule patts
else
- quantified_atom_of_constr (EConstr.push_rel (RelDecl.LocalAssum (id,atom)) env) sigma (succ nrels) ff
+ quantified_atom_of_constr (EConstr.push_rel (RelDecl.LocalAssum (id,atom)) env) sigma (succ nrels) ff
| _ ->
let patts=patterns_of_constr env sigma nrels term in
`Rule patts
let litteral_of_constr env sigma term=
match EConstr.kind sigma (whd_delta env sigma term) with
- | Prod (id,atom,ff) ->
+ | Prod (id,atom,ff) ->
if is_global sigma (Lazy.force _False) ff then
match (atom_of_constr env sigma atom) with
`Eq(t,a,b) -> `Neq(t,a,b)
@@ -171,7 +172,7 @@ let litteral_of_constr env sigma term=
else
begin
try
- quantified_atom_of_constr (EConstr.push_rel (RelDecl.LocalAssum (id,atom)) env) sigma 1 ff
+ quantified_atom_of_constr (EConstr.push_rel (RelDecl.LocalAssum (id,atom)) env) sigma 1 ff
with Not_found ->
`Other (decompose_term env sigma term)
end
@@ -233,7 +234,7 @@ let build_projection intype (cstr:pconstructor) special default gls=
let sigma = project gls in
let body=Equality.build_selector (pf_env gls) sigma ci (mkRel 1) intype special default in
let id=pf_get_new_id (Id.of_string "t") gls in
- sigma, mkLambda(Name id,intype,body)
+ sigma, mkLambda(make_annot (Name id) Sorts.Relevant,intype,body)
(* generate an adhoc tactic following the proof tree *)
@@ -318,7 +319,7 @@ let rec proof_tac p : unit Proofview.tactic =
refresh_universes (type_of tx1) (fun typx ->
refresh_universes (type_of (mkApp (tf1,[|tx1|]))) (fun typfx ->
let id = Tacmach.New.pf_get_new_id (Id.of_string "f") gl in
- let appx1 = mkLambda(Name id,typf,mkApp(mkRel 1,[|tx1|])) in
+ let appx1 = mkLambda(make_annot (Name id) Sorts.Relevant,typf,mkApp(mkRel 1,[|tx1|])) in
let lemma1 = app_global_with_holes _f_equal [|typf;typfx;appx1;tf1;tf2|] 1 in
let lemma2 = app_global_with_holes _f_equal [|typx;typfx;tf2;tx1;tx2|] 1 in
let prf =
@@ -377,7 +378,7 @@ let convert_to_goal_tac c t1 t2 p =
let neweq= app_global _eq [|sort;tt1;tt2|] in
let e = Tacmach.New.pf_get_new_id (Id.of_string "e") gl in
let x = Tacmach.New.pf_get_new_id (Id.of_string "X") gl in
- let identity=mkLambda (Name x,sort,mkRel 1) in
+ let identity=mkLambda (make_annot (Name x) Sorts.Relevant,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; endt refine_exact_check]
@@ -432,7 +433,7 @@ let cc_tactic depth additionnal_terms =
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
+ let p=build_proof (Tacmach.New.pf_env gl) sigma uf (`Discr (i,ipac,j,jpac)) in
let cstr=(get_constructor_info uf ipac.cnode).ci_constr in
discriminate_tac cstr p
| Incomplete ->
@@ -461,7 +462,8 @@ let cc_tactic depth additionnal_terms =
Pp.str " replacing metavariables by arbitrary terms.");
Tacticals.New.tclFAIL 0 (str "Incomplete")
| Contradiction dis ->
- let p=build_proof uf (`Prove (dis.lhs,dis.rhs)) in
+ let env = Proofview.Goal.env gl in
+ let p=build_proof env sigma uf (`Prove (dis.lhs,dis.rhs)) in
let ta=term uf dis.lhs and tb=term uf dis.rhs in
match dis.rule with
Goal -> proof_tac p
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-02 12:51:42 +0000