aboutsummaryrefslogtreecommitdiff
path: root/plugins/cc
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/cc')
-rw-r--r--plugins/cc/ccalgo.ml84
-rw-r--r--plugins/cc/ccalgo.mli19
-rw-r--r--plugins/cc/ccproof.ml13
-rw-r--r--plugins/cc/ccproof.mli13
-rw-r--r--plugins/cc/cctac.ml46
-rw-r--r--plugins/cc/cctac.mli12
-rw-r--r--plugins/cc/g_congruence.ml430
-rw-r--r--plugins/cc/g_congruence.mlg33
8 files changed, 121 insertions, 129 deletions
diff --git a/plugins/cc/ccalgo.ml b/plugins/cc/ccalgo.ml
index 3e4febf47c..ce620d5312 100644
--- a/plugins/cc/ccalgo.ml
+++ b/plugins/cc/ccalgo.ml
@@ -1,25 +1,26 @@
(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
+(* * The Coq Proof Assistant / The Coq Development Team *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* <O___,, * (see CREDITS file for the list of authors) *)
(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
(* This file implements the basic congruence-closure algorithm by *)
-(* Downey,Sethi and Tarjan. *)
+(* Downey, Sethi and Tarjan. *)
(* Plus some e-matching and constructor handling by P. Corbineau *)
-open API
open CErrors
-open Util
open Pp
-open Goptions
open Names
-open Term
+open Sorts
+open Constr
open Vars
+open Goptions
open Tacmach
-open Evd
+open Util
let init_size=5
@@ -129,8 +130,8 @@ type cinfo=
ci_nhyps: int} (* # projectable args *)
let family_eq f1 f2 = match f1, f2 with
- | Prop Pos, Prop Pos
- | Prop Null, Prop Null
+ | Set, Set
+ | Prop, Prop
| Type _, Type _ -> true
| _ -> false
@@ -155,7 +156,7 @@ let rec term_equal t1 t2 =
open Hashset.Combine
let rec hash_term = function
- | Symb c -> combine 1 (hash_constr c)
+ | Symb c -> combine 1 (Constr.hash c)
| 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)
@@ -216,7 +217,7 @@ type representative=
mutable lfathers:Int.Set.t;
mutable fathers:Int.Set.t;
mutable inductive_status: inductive_status;
- class_type : Term.types;
+ class_type : types;
mutable functions: Int.Set.t PafMap.t} (*pac -> term = app(constr,t) *)
type cl = Rep of representative| Eqto of int*equality
@@ -233,7 +234,7 @@ type node =
module Constrhash = Hashtbl.Make
(struct type t = constr
let equal = eq_constr_nounivs
- let hash = hash_constr
+ let hash = Constr.hash
end)
module Typehash = Constrhash
@@ -270,7 +271,8 @@ type state =
mutable rew_depth:int;
mutable changed:bool;
by_type: Int.Set.t Typehash.t;
- mutable gls:Goal.goal Evd.sigma}
+ mutable env:Environ.env;
+ sigma:Evd.evar_map}
let dummy_node =
{
@@ -305,7 +307,8 @@ let empty depth gls:state =
rew_depth=depth;
by_type=Constrhash.create init_size;
changed=false;
- gls=gls
+ env=pf_env gls;
+ sigma=project gls
}
let forest state = state.uf
@@ -424,7 +427,7 @@ let cc_product s1 s2 =
mkLambda(_B_,mkSort(s2),_body_))
let rec constr_of_term = function
- Symb s-> applist_projection s []
+ Symb s-> s
| Product(s1,s2) -> cc_product s1 s2
| Eps id -> mkVar id
| Constructor cinfo -> mkConstructU cinfo.ci_constr
@@ -432,30 +435,12 @@ let rec constr_of_term = function
make_app [(constr_of_term s2)] s1
and make_app l=function
Appli (s1,s2)->make_app ((constr_of_term s2)::l) s1
- | other ->
- applist_proj other l
-and applist_proj c l =
- match c with
- | Symb s -> applist_projection s l
- | _ -> applistc (constr_of_term c) l
-and applist_projection c l =
- match kind_of_term c with
- | Const c when Environ.is_projection (fst c) (Global.env()) ->
- let p = Projection.make (fst c) false in
- (match l with
- | [] -> (* Expand the projection *)
- let ty = Typeops.type_of_constant_in (Global.env ()) c in (* FIXME constraints *)
- let pb = Environ.lookup_projection p (Global.env()) in
- let ctx,_ = Term.decompose_prod_n_assum (pb.Declarations.proj_npars + 1) ty in
- it_mkLambda_or_LetIn (mkProj(p,mkRel 1)) ctx
- | hd :: tl ->
- applistc (mkProj (p, hd)) tl)
- | _ -> applistc c l
+ | other -> Term.applist (constr_of_term other,l)
let rec canonize_name sigma c =
let c = EConstr.Unsafe.to_constr c in
let func c = canonize_name sigma (EConstr.of_constr c) in
- match kind_of_term c with
+ match Constr.kind c with
| Const (kn,u) ->
let canon_const = Constant.make1 (Constant.canonical kn) in
(mkConstU (canon_const,u))
@@ -472,10 +457,10 @@ let rec canonize_name sigma c =
| LetIn (na,b,t,ct) ->
mkLetIn (na, func b,func t,func ct)
| App (ct,l) ->
- mkApp (func ct,Array.smartmap func l)
+ mkApp (func ct,Array.Smart.map func l)
| Proj(p,c) ->
let p' = Projection.map (fun kn ->
- Constant.make1 (Constant.canonical kn)) p in
+ MutInd.make1 (MutInd.canonical kn)) p in
(mkProj (p', func c))
| _ -> c
@@ -509,8 +494,8 @@ let rec add_term state t=
Not_found ->
let b=next uf in
let trm = constr_of_term t in
- let typ = pf_unsafe_type_of state.gls (EConstr.of_constr trm) in
- let typ = canonize_name (project state.gls) typ in
+ let typ = Typing.unsafe_type_of state.env state.sigma (EConstr.of_constr trm) in
+ let typ = canonize_name state.sigma typ in
let new_node=
match t with
Symb _ | Product (_,_) ->
@@ -818,11 +803,10 @@ let one_step state =
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 [Context.Named.Declaration.LocalAssum (id,typ)] in
- state.gls<- gls;
- id
+ 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;
+ id
let complete_one_class state i=
match (get_representative state.uf i).inductive_status with
@@ -830,15 +814,15 @@ let complete_one_class state i=
let rec app t typ n =
if n<=0 then t else
let _,etyp,rest= destProd typ in
- let id = new_state_var etyp state in
+ let id = new_state_var (EConstr.of_constr etyp) state in
app (Appli(t,Eps id)) (substl [mkVar id] rest) (n-1) in
- let _c = pf_unsafe_type_of state.gls
+ 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
let _args =
List.map (fun i -> constr_of_term (term state.uf i))
pac.args in
- let typ = prod_applist _c (List.rev _args) in
+ let typ = Term.prod_applist _c (List.rev _args) in
let ct = app (term state.uf i) typ pac.arity in
state.uf.epsilons <- pac :: state.uf.epsilons;
ignore (add_term state ct)
diff --git a/plugins/cc/ccalgo.mli b/plugins/cc/ccalgo.mli
index 1441e13fb3..4ebc6a135a 100644
--- a/plugins/cc/ccalgo.mli
+++ b/plugins/cc/ccalgo.mli
@@ -1,14 +1,15 @@
(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
+(* * The Coq Proof Assistant / The Coq Development Team *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* <O___,, * (see CREDITS file for the list of authors) *)
(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
-open API
open Util
-open Term
+open Constr
open Names
type pa_constructor =
@@ -86,7 +87,7 @@ type representative=
mutable lfathers:Int.Set.t;
mutable fathers:Int.Set.t;
mutable inductive_status: inductive_status;
- class_type : Term.types;
+ class_type : types;
mutable functions: Int.Set.t PafMap.t} (*pac -> term = app(constr,t) *)
type cl = Rep of representative| Eqto of int*equality
@@ -121,7 +122,7 @@ val term_equal : term -> term -> bool
val constr_of_term : term -> constr
-val debug : (unit -> Pp.std_ppcmds) -> unit
+val debug : (unit -> Pp.t) -> unit
val forest : state -> forest
@@ -170,7 +171,7 @@ val find_instances : state -> (quant_eq * int array) list
val execute : bool -> state -> explanation option
-val pr_idx_term : forest -> int -> Pp.std_ppcmds
+val pr_idx_term : forest -> int -> Pp.t
val empty_forest: unit -> forest
diff --git a/plugins/cc/ccproof.ml b/plugins/cc/ccproof.ml
index 4c9ebcfc4d..1f1fa9c99a 100644
--- a/plugins/cc/ccproof.ml
+++ b/plugins/cc/ccproof.ml
@@ -1,17 +1,18 @@
(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
+(* * The Coq Proof Assistant / The Coq Development Team *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* <O___,, * (see CREDITS file for the list of authors) *)
(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
(* 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 Constr
open Ccalgo
open Pp
diff --git a/plugins/cc/ccproof.mli b/plugins/cc/ccproof.mli
index 0488a5db7c..bebef241e1 100644
--- a/plugins/cc/ccproof.mli
+++ b/plugins/cc/ccproof.mli
@@ -1,14 +1,15 @@
(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
+(* * The Coq Proof Assistant / The Coq Development Team *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* <O___,, * (see CREDITS file for the list of authors) *)
(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
-open API
open Ccalgo
-open Term
+open Constr
type rule=
Ax of constr
diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml
index 4c5d85a5fd..2eaa6146e1 100644
--- a/plugins/cc/cctac.ml
+++ b/plugins/cc/cctac.ml
@@ -1,19 +1,20 @@
(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
+(* * The Coq Proof Assistant / The Coq Development Team *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* <O___,, * (see CREDITS file for the list of authors) *)
(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
(* This file is the interface between the c-c algorithm and Coq *)
-open API
open Evd
open Names
open Inductiveops
open Declarations
-open Term
+open Constr
open EConstr
open Vars
open Tactics
@@ -48,7 +49,7 @@ let whd_delta env sigma t =
(* decompose member of equality in an applicative format *)
(** FIXME: evar leak *)
-let sf_of env sigma c = e_sort_of env (ref sigma) c
+let sf_of env sigma c = snd (sort_of env sigma c)
let rec decompose_term env sigma t=
match EConstr.kind sigma (whd env sigma t) with
@@ -77,18 +78,19 @@ let rec decompose_term env sigma t=
let (mind,i_ind),u = c in
let u = EInstance.kind sigma u in
let canon_mind = MutInd.make1 (MutInd.canonical mind) in
- let canon_ind = canon_mind,i_ind in (Symb (Term.mkIndU (canon_ind,u)))
+ let canon_ind = canon_mind,i_ind in (Symb (Constr.mkIndU (canon_ind,u)))
| Const (c,u) ->
let u = EInstance.kind sigma u in
let canon_const = Constant.make1 (Constant.canonical c) in
- (Symb (Term.mkConstU (canon_const,u)))
+ (Symb (Constr.mkConstU (canon_const,u)))
| Proj (p, c) ->
- let canon_const kn = Constant.make1 (Constant.canonical kn) in
- let p' = Projection.map canon_const p in
- (Appli (Symb (Term.mkConst (Projection.constant p')), decompose_term env sigma c))
+ let canon_mind kn = MutInd.make1 (MutInd.canonical kn) in
+ let p' = Projection.map canon_mind p in
+ let c = Retyping.expand_projection env sigma p' c [] in
+ 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
+ if closed0 sigma t then Symb (EConstr.to_constr ~abort_on_undefined_evars:false sigma t) else raise Not_found
(* decompose equality in members and type *)
open Termops
@@ -187,7 +189,7 @@ let make_prb gls depth additionnal_terms =
let open Tacmach.New in
let env=pf_env gls in
let sigma=project gls in
- let state = empty depth {it = Proofview.Goal.goal (Proofview.Goal.assume gls); sigma } in
+ let state = empty depth {it = Proofview.Goal.goal gls; sigma } in
let pos_hyps = ref [] in
let neg_hyps =ref [] in
List.iter
@@ -198,7 +200,7 @@ let make_prb gls depth additionnal_terms =
(fun decl ->
let id = NamedDecl.get_id decl in
begin
- let cid=Term.mkVar id in
+ let cid=Constr.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
@@ -232,7 +234,8 @@ 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 sigma, body=Equality.build_selector (pf_env gls) (project gls) ci (mkRel 1) intype special default in
+ 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)
@@ -261,9 +264,8 @@ let app_global_with_holes f args n =
let ans = mkApp (fc, args) in
let (sigma, holes) = gen_holes env sigma t n [] in
let ans = applist (ans, holes) in
- let evdref = ref sigma in
- let () = Typing.e_check env evdref ans concl in
- (!evdref, ans)
+ let sigma = Typing.check env sigma ans concl in
+ (sigma, ans)
end
end
@@ -441,11 +443,11 @@ let cc_tactic depth additionnal_terms =
let open Glob_term in
let env = Proofview.Goal.env gl in
let terms_to_complete = List.map (build_term_to_complete uf) (epsilons uf) in
- let hole = CAst.make @@ GHole (Evar_kinds.InternalHole, Misctypes.IntroAnonymous, None) in
+ let hole = DAst.make @@ GHole (Evar_kinds.InternalHole, Namegen.IntroAnonymous, None) in
let pr_missing (c, missing) =
- let c = Detyping.detype ~lax:true false [] env sigma c in
+ let c = Detyping.detype Detyping.Now ~lax:true false Id.Set.empty env sigma c in
let holes = List.init missing (fun _ -> hole) in
- Printer.pr_glob_constr_env env (CAst.make @@ GApp (c, holes))
+ Printer.pr_glob_constr_env env (DAst.make @@ GApp (c, holes))
in
Feedback.msg_info
(Pp.str "Goal is solvable by congruence but some arguments are missing.");
diff --git a/plugins/cc/cctac.mli b/plugins/cc/cctac.mli
index ef32d2b83e..a1bbcbc0d6 100644
--- a/plugins/cc/cctac.mli
+++ b/plugins/cc/cctac.mli
@@ -1,13 +1,13 @@
-
(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *)
+(* * The Coq Proof Assistant / The Coq Development Team *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* <O___,, * (see CREDITS file for the list of authors) *)
(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
-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
deleted file mode 100644
index add3f90b1b..0000000000
--- a/plugins/cc/g_congruence.ml4
+++ /dev/null
@@ -1,30 +0,0 @@
-(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
-(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
-(************************************************************************)
-
-(*i camlp4deps: "grammar/grammar.cma" i*)
-
-open API
-open Ltac_plugin
-open Cctac
-open Stdarg
-
-DECLARE PLUGIN "cc_plugin"
-
-(* Tactic registration *)
-
-TACTIC EXTEND cc
- [ "congruence" ] -> [ congruence_tac 1000 [] ]
- |[ "congruence" integer(n) ] -> [ congruence_tac n [] ]
- |[ "congruence" "with" ne_constr_list(l) ] -> [ congruence_tac 1000 l ]
- |[ "congruence" integer(n) "with" ne_constr_list(l) ] ->
- [ congruence_tac n l ]
-END
-
-TACTIC EXTEND f_equal
- [ "f_equal" ] -> [ f_equal ]
-END
diff --git a/plugins/cc/g_congruence.mlg b/plugins/cc/g_congruence.mlg
new file mode 100644
index 0000000000..685059294f
--- /dev/null
+++ b/plugins/cc/g_congruence.mlg
@@ -0,0 +1,33 @@
+(************************************************************************)
+(* * The Coq Proof Assistant / The Coq Development Team *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* <O___,, * (see CREDITS file for the list of authors) *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(* * (see LICENSE file for the text of the license) *)
+(************************************************************************)
+
+{
+
+open Ltac_plugin
+open Cctac
+open Stdarg
+
+}
+
+DECLARE PLUGIN "cc_plugin"
+
+(* Tactic registration *)
+
+TACTIC EXTEND cc
+| [ "congruence" ] -> { congruence_tac 1000 [] }
+| [ "congruence" integer(n) ] -> { congruence_tac n [] }
+| [ "congruence" "with" ne_constr_list(l) ] -> { congruence_tac 1000 l }
+ |[ "congruence" integer(n) "with" ne_constr_list(l) ] ->
+ { congruence_tac n l }
+END
+
+TACTIC EXTEND f_equal
+| [ "f_equal" ] -> { f_equal }
+END
generated by cgit v1.2.3 (git 2.25.1) at 2026-06-07 02:38:34 +0000