This is an automated email from the git hooks/post-receive script.
gareuselesinge pushed a commit to branch master
in repository aac-tactics.
commit 1117d2e4a00debfbfa0157cc3e780916df72c26b
Author: Enrico Tassi <gareuselesi...@debian.org>
Date: Tue Dec 27 16:06:42 2016 +0000
New upstream version 8.6
---
AAC.v | 5 +++++
Make | 2 ++
Makefile | 2 ++
coq.ml | 65 ++++++++++++++++++++++++++++++++++++-------------------------
coq.mli | 6 +++---
helper.ml | 4 ++--
matcher.ml | 4 ++--
print.ml | 11 ++++++-----
print.mli | 4 ++--
rewrite.ml4 | 27 +++++++++++++------------
theory.ml | 8 ++++----
theory.mli | 2 +-
12 files changed, 81 insertions(+), 59 deletions(-)
diff --git a/AAC.v b/AAC.v
index f6f382f..5feb0b6 100644
--- a/AAC.v
+++ b/AAC.v
@@ -1115,6 +1115,11 @@ Section s.
End s.
End Internal.
+Local Ltac internal_normalize :=
+ let x := fresh in let y := fresh in
+ intro x; intro y; vm_compute in x; vm_compute in y; unfold x; unfold y;
+ compute [Internal.eval Internal.fold_map Internal.copy Prect]; simpl.
+
(** * Lemmas for performing transitivity steps
given an instance of AAC_lift *)
diff --git a/Make b/Make
index 8caf805..ec45b23 100644
--- a/Make
+++ b/Make
@@ -1,5 +1,6 @@
-I .
-R . AAC_tactics
+
coq.mli
helper.mli
search_monad.mli
@@ -15,6 +16,7 @@ theory.ml
print.ml
rewrite.ml4
aac.mlpack
+
AAC.v
Instances.v
Tutorial.v
diff --git a/Makefile b/Makefile
index a9d5466..abf2ec6 100644
--- a/Makefile
+++ b/Makefile
@@ -8,6 +8,8 @@ clean: Makefile.coq
Makefile.coq: Make
$(COQBIN)coq_makefile -f Make -o Makefile.coq
+Make: ;
+
%: Makefile.coq
+make -f Makefile.coq $@
diff --git a/coq.ml b/coq.ml
index 97154e2..eb4b5f1 100755
--- a/coq.ml
+++ b/coq.ml
@@ -12,6 +12,8 @@ type constr = Term.constr
open Term
open Names
open Coqlib
+open Sigma.Notations
+open Context.Rel.Declaration
(* The contrib name is used to locate errors when loading constrs *)
let contrib_name = "aac_tactics"
@@ -55,7 +57,9 @@ let goal_update (goal : goal_sigma) evar_map : goal_sigma=
let fresh_evar goal ty : constr * goal_sigma =
let env = Tacmach.pf_env goal in
let evar_map = Tacmach.project goal in
- let (em,x) = Evarutil.new_evar env evar_map ty in
+ let evar_map = Sigma.Unsafe.of_evar_map evar_map in
+ let Sigma (x,em,_) = Evarutil.new_evar env evar_map ty in
+ let em = Sigma.to_evar_map em in
x,( goal_update goal em)
let resolve_one_typeclass goal ty : constr*goal_sigma=
@@ -73,8 +77,8 @@ let cps_resolve_one_typeclass ?error : Term.types ->
(Term.constr -> Proof_type
try Typeclasses.resolve_one_typeclass env em t
with Not_found ->
begin match error with
- | None -> Errors.anomaly (Pp.str "Cannot resolve a
typeclass : please report")
- | Some x -> Errors.error x
+ | None -> CErrors.anomaly (Pp.str "Cannot resolve a
typeclass : please report")
+ | Some x -> CErrors.error x
end
in
Tacticals.tclTHENLIST [Refiner.tclEVARS em; k c] goal
@@ -88,28 +92,36 @@ let nf_evar goal c : Term.constr=
let evar_unit (gl : goal_sigma) (x : constr) : constr * goal_sigma =
let env = Tacmach.pf_env gl in
let evar_map = Tacmach.project gl in
- let (em,x) = Evarutil.new_evar env evar_map x in
+ let evar_map = Sigma.Unsafe.of_evar_map evar_map in
+ let Sigma (x,em,_) = Evarutil.new_evar env evar_map x in
+ let em = Sigma.to_evar_map em in
x,(goal_update gl em)
let evar_binary (gl: goal_sigma) (x : constr) =
let env = Tacmach.pf_env gl in
let evar_map = Tacmach.project gl in
let ty = mkArrow x (mkArrow x x) in
- let (em,x) = Evarutil.new_evar env evar_map ty in
+ let evar_map = Sigma.Unsafe.of_evar_map evar_map in
+ let Sigma (x,em,_) = Evarutil.new_evar env evar_map ty in
+ let em = Sigma.to_evar_map em in
x,( goal_update gl em)
let evar_relation (gl: goal_sigma) (x: constr) =
let env = Tacmach.pf_env gl in
let evar_map = Tacmach.project gl in
let ty = mkArrow x (mkArrow x (mkSort prop_sort)) in
- let (em,r) = Evarutil.new_evar env evar_map ty in
+ let evar_map = Sigma.Unsafe.of_evar_map evar_map in
+ let Sigma (r, em, _) = Evarutil.new_evar env evar_map ty in
+ let em = Sigma.to_evar_map em in
r,( goal_update gl em)
let cps_evar_relation (x: constr) k = fun goal ->
Tacmach.pf_apply
(fun env em ->
let ty = mkArrow x (mkArrow x (mkSort prop_sort)) in
- let (em,r) = Evarutil.new_evar env em ty in
+ let em = Sigma.Unsafe.of_evar_map em in
+ let Sigma (r, em, _) = Evarutil.new_evar env em ty in
+ let em = Sigma.to_evar_map em in
Tacticals.tclTHENLIST [Refiner.tclEVARS em; k r] goal
) goal
@@ -319,9 +331,9 @@ module Equivalence = struct
end
end
(**[ match_as_equation goal eqt] see [eqt] as an equation. An
- optionnal rel_context can be provided to ensure taht the term
+ optionnal rel-context can be provided to ensure that the term
remains typable*)
-let match_as_equation ?(context = Context.empty_rel_context) goal equation :
(constr*constr* Std.Relation.t) option =
+let match_as_equation ?(context = Context.Rel.empty) goal equation :
(constr*constr* Std.Relation.t) option =
let env = Tacmach.pf_env goal in
let env = Environ.push_rel_context context env in
let evar_map = Tacmach.project goal in
@@ -345,15 +357,15 @@ let match_as_equation ?(context =
Context.empty_rel_context) goal equation : (co
let tclTIME msg tac = fun gl ->
let u = Sys.time () in
let r = tac gl in
- let _ = Pp.msgnl (Pp.str (Printf.sprintf "%s:%fs" msg (Sys.time ()-. u))) in
+ let _ = Feedback.msg_notice (Pp.str (Printf.sprintf "%s:%fs" msg (Sys.time
()-. u))) in
r
let tclDEBUG msg tac = fun gl ->
- let _ = Pp.msgnl (Pp.str msg) in
+ let _ = Feedback.msg_debug (Pp.str msg) in
tac gl
let tclPRINT tac = fun gl ->
- let _ = Pp.msgnl (Printer.pr_constr (Tacmach.pf_concl gl)) in
+ let _ = Feedback.msg_notice (Printer.pr_constr (Tacmach.pf_concl gl)) in
tac gl
@@ -361,13 +373,13 @@ let tclPRINT tac = fun gl ->
(* functions to handle the failures of our tactic. Some should be
reported [anomaly], some are on behalf of the user [user_error]*)
let anomaly msg =
- Errors.anomaly ~label:"[aac_tactics]" (Pp.str msg)
+ CErrors.anomaly ~label:"[aac_tactics]" (Pp.str msg)
let user_error msg =
- Errors.error ("[aac_tactics] " ^ msg)
+ CErrors.error ("[aac_tactics] " ^ msg)
let warning msg =
- Pp.msg_warning (Pp.str ("[aac_tactics]" ^ msg))
+ Feedback.msg_warning (Pp.str ("[aac_tactics]" ^ msg))
(** {1 Rewriting tactics used in aac_rewrite} *)
@@ -384,7 +396,7 @@ type hypinfo =
{
hyp : Term.constr; (** the actual constr corresponding
to the hypothese *)
hyptype : Term.constr; (** the type of the hypothesis *)
- context : Context.rel_context; (** the quantifications of the
hypothese *)
+ context : Context.Rel.t; (** the quantifications of the
hypothese *)
body : Term.constr; (** the body of the type of the
hypothesis*)
rel : Std.Relation.t; (** the relation *)
left : Term.constr; (** left hand side *)
@@ -397,16 +409,14 @@ let get_hypinfo c ~l2r ?check_type (k : hypinfo ->
Proof_type.tactic) : Proo
let (rel_context, body_type) = Term.decompose_prod_assum ctype in
let rec check f e =
match decomp_term e with
- | Term.Rel i ->
- let name, constr_option, types = Context.lookup_rel i rel_context
- in f types
+ | Term.Rel i -> f (get_type (Context.Rel.lookup i rel_context))
| _ -> Term.fold_constr (fun acc x -> acc && check f x) true e
in
begin match check_type with
| None -> ()
| Some f ->
- if not (check f body_type)
- then user_error "Unable to deal with higher-order or heterogeneous
patterns";
+ if not (check f body_type)
+ then user_error "Unable to deal with higher-order or heterogeneous
patterns";
end;
begin
match match_as_equation ~context:rel_context goal body_type with
@@ -443,7 +453,7 @@ let get_hypinfo c ~l2r ?check_type (k : hypinfo ->
Proof_type.tactic) : Proo
(* Fresh evars for everyone (should be the good way to do this
recompose in Coq v8.4) *)
let recompose_prod
- (context : Context.rel_context)
+ (context : Context.Rel.t)
(subst : (int * Term.constr) list)
env
em
@@ -457,14 +467,17 @@ let recompose_prod
match context with
| [] ->
env, em, acc
- | ((name,c,ty) as t)::q ->
+ | t::q ->
let env, em, acc = aux q acc em (n+1) in
if n >= min_n
then
let em,x =
try em, List.assoc n subst
with | Not_found ->
- Evarutil.new_evar env em (Vars.substl acc ty)
+ let em = Sigma.Unsafe.of_evar_map em in
+ let Sigma (r, em, _) = Evarutil.new_evar env em (Vars.substl acc
(get_type t)) in
+ let em = Sigma.to_evar_map em in
+ (em, r)
in
(Environ.push_rel t env), em,x::acc
else
@@ -477,7 +490,7 @@ let recompose_prod
application to handle non-instanciated variables. *)
let recompose_prod'
- (context : Context.rel_context)
+ (context : Context.Rel.t)
(subst : (int *Term.constr) list)
c
=
@@ -487,7 +500,7 @@ let recompose_prod'
| [] -> []
| t::q -> pop t :: (popn pop (n-1) q)
in
- let pop_rel_decl (name,c,ty) = (name,c,Termops.pop ty) in
+ let pop_rel_decl = map_type Termops.pop in
let rec aux sign n next app ctxt =
match sign with
| [] -> List.rev app, List.rev ctxt
diff --git a/coq.mli b/coq.mli
index 1004d2c..4d46c7d 100644
--- a/coq.mli
+++ b/coq.mli
@@ -147,9 +147,9 @@ module Equivalence : sig
end
(** [match_as_equation ?context goal c] try to decompose c as a
- relation applied to two terms. An optionnal rel_context can be
+ relation applied to two terms. An optionnal rel-context can be
provided to ensure that the term remains typable *)
-val match_as_equation : ?context:Context.rel_context -> goal_sigma ->
Term.constr -> (Term.constr * Term.constr * Relation.t) option
+val match_as_equation : ?context:Context.Rel.t -> goal_sigma -> Term.constr
-> (Term.constr * Term.constr * Relation.t) option
(** {2 Some tacticials} *)
@@ -190,7 +190,7 @@ type hypinfo =
{
hyp : Term.constr; (** the actual constr corresponding
to the hypothese *)
hyptype : Term.constr; (** the type of the hypothesis *)
- context : Context.rel_context; (** the quantifications of the
hypothese *)
+ context : Context.Rel.t; (** the quantifications of the
hypothese *)
body : Term.constr; (** the body of the hypothese*)
rel : Relation.t; (** the relation *)
left : Term.constr; (** left hand side *)
diff --git a/helper.ml b/helper.ml
index 637def1..636b17f 100644
--- a/helper.ml
+++ b/helper.ml
@@ -29,8 +29,8 @@ module Debug (X : CONTROL) = struct
let pr_constr msg constr =
if printing then
- ( Pp.msgnl (Pp.str (Printf.sprintf "=====%s====" msg));
- Pp.msgnl (Printer.pr_constr constr);
+ ( Feedback.msg_notice (Pp.str (Printf.sprintf "=====%s====" msg));
+ Feedback.msg_notice (Printer.pr_constr constr);
)
diff --git a/matcher.ml b/matcher.ml
index 2fd0517..1dcb1d2 100644
--- a/matcher.ml
+++ b/matcher.ml
@@ -455,7 +455,7 @@ end
| Dot (s,l,r) -> Dot (s, aux l, aux r)
| Var i ->
begin match find t i with
- | None -> Errors.error "aac_tactics: instantiate failure"
+ | None -> CErrors.error "aac_tactics: instantiate failure"
| Some x -> t_of_term x
end
in aux x
@@ -1092,7 +1092,7 @@ let unit_warning p ~nullif ~unitif =
if not (Search.is_empty unitif)
then
begin
- Pp.msg_warning
+ Feedback.msg_warning
(Pp.str
"[aac_tactics] This pattern can be instanciated to match units, some
solutions can be missing");
end
diff --git a/print.ml b/print.ml
index 0305158..427b6dc 100644
--- a/print.ml
+++ b/print.ml
@@ -10,6 +10,8 @@
solution *)
open Pp
open Matcher
+open Context.Rel.Declaration
+
type named_env = (Names.name * Terms.t) list
@@ -65,14 +67,14 @@ let pp_all pt : (int * Terms.t * named_env Search_monad.m)
Search_monad.m -> Pp.
rename the variables, and rebuilds raw Coq terms (for the context, and
the terms in the environment). In order to do so, it requires the
information gathered by the {!Theory.Trans} module.*)
-let print rlt ir m (context : Context.rel_context) goal =
+let print rlt ir m (context : Context.Rel.t) goal =
if Search_monad.count m = 0
then
(
Tacticals.tclFAIL 0 (Pp.str "No subterm modulo AC") goal
)
else
- let _ = Pp.msgnl (Pp.str "All solutions:") in
+ let _ = Feedback.msg_notice (Pp.str "All solutions:") in
let m = Search_monad.(>>) m
(fun (i,t,envm) ->
let envm = Search_monad.(>>) envm ( fun env ->
@@ -80,8 +82,7 @@ let print rlt ir m (context : Context.rel_context) goal =
let l = List.sort (fun (n,_) (n',_) -> Pervasives.compare n n') l in
let l =
List.map (fun (v,t) ->
- let (name,body,types) = Context.lookup_rel v context in
- (name,t)
+ get_name (Context.Rel.lookup v context), t
) l
in
Search_monad.return l
@@ -91,7 +92,7 @@ let print rlt ir m (context : Context.rel_context) goal =
)
in
let m = Search_monad.sort (fun (x,_,_) (y,_,_) -> x - y) m in
- let _ = Pp.msgnl
+ let _ = Feedback.msg_notice
(pp_all
(fun t -> Printer.pr_constr (Theory.Trans.raw_constr_of_t ir rlt
context t) ) m
)
diff --git a/print.mli b/print.mli
index 7fab3be..bbb9b20 100644
--- a/print.mli
+++ b/print.mli
@@ -10,7 +10,7 @@
tactic. *)
-(** The main printing function. {!print} uses the [Term.rel_context]
+(** The main printing function. {!print} uses the rel-context
to rename the variables, and rebuilds raw Coq terms (for the given
context, and the terms in the environment). In order to do so, it
requires the information gathered by the {!Theory.Trans} module.*)
@@ -18,6 +18,6 @@ val print :
Coq.Relation.t ->
Theory.Trans.ir ->
(int * Matcher.Terms.t * Matcher.Subst.t Search_monad.m) Search_monad.m ->
- Context.rel_context ->
+ Context.Rel.t ->
Proof_type.tactic
diff --git a/rewrite.ml4 b/rewrite.ml4
index b3e52e0..1f57c0b 100644
--- a/rewrite.ml4
+++ b/rewrite.ml4
@@ -8,6 +8,11 @@
(** aac_rewrite -- rewriting modulo *)
+open Pcoq.Prim
+open Pcoq.Constr
+open Stdarg
+open Constrarg
+
DECLARE PLUGIN "aac"
module Control = struct
@@ -33,7 +38,7 @@ let retype = Coq.retype
(* helper to be used with the previous function: raise a new anomaly
except if a another one was previously raised *)
let push_anomaly msg = function
- | e when Errors.is_anomaly e -> raise e
+ | e when CErrors.is_anomaly e -> raise e
| _ -> Coq.anomaly msg
module M = Matcher
@@ -190,7 +195,7 @@ let by_aac_reflexivity zero
[ retype decision_thm; retype convert_to;
convert ;
tac_or_exn apply_tac Coq.user_error "unification failure";
- tac_or_exn (time_tac "vm_norm" (Tactics.normalise_in_concl))
Coq.anomaly "vm_compute failure";
+ tac_or_exn (time_tac "vm_norm" (Proofview.V82.of_tactic
(Tactics.normalise_in_concl))) Coq.anomaly "vm_compute failure";
Tacticals.tclORELSE (Proofview.V82.of_tactic Tactics.reflexivity)
(Tacticals.tclFAIL 0 (Pp.str "Not an equality modulo A/AC"))
])
@@ -253,25 +258,19 @@ let aac_conclude
| Not_found -> Coq.user_error "No lifting from the goal's relation to an
equivalence"
open Libnames
+open Tacexpr
open Tacinterp
let aac_normalise = fun goal ->
let ids = Tacmach.pf_ids_of_hyps goal in
+ let loc = Loc.ghost in
+ let mp = MPfile (DirPath.make (List.map Id.of_string ["AAC";
"AAC_tactics"])) in
+ let norm_tac = KerName.make2 mp (Label.make "internal_normalize") in
+ let norm_tac = Misctypes.ArgArg (loc, norm_tac) in
Tacticals.tclTHENLIST
[
aac_conclude by_aac_normalise;
- Proofview.V82.of_tactic begin
- Tacinterp.interp (
- <:tactic<
- intro x;
- intro y;
- vm_compute in x;
- vm_compute in y;
- unfold x;
- unfold y;
- compute [Internal.eval Internal.fold_map Internal.copy Prect]; simpl
- >>
- )end;
+ Proofview.V82.of_tactic (Tacinterp.eval_tactic (TacArg (loc, TacCall
(loc, norm_tac, []))));
Proofview.V82.of_tactic (Tactics.keep ids)
] goal
diff --git a/theory.ml b/theory.ml
index a5229fa..20cb299 100644
--- a/theory.ml
+++ b/theory.ml
@@ -289,10 +289,10 @@ module Unit = struct
end
let anomaly msg =
- Errors.anomaly ~label:"aac_tactics" (Pp.str msg)
+ CErrors.anomaly ~label:"aac_tactics" (Pp.str msg)
let user_error msg =
- Errors.error ("aac_tactics: " ^ msg)
+ CErrors.error ("aac_tactics: " ^ msg)
module Trans = struct
@@ -877,11 +877,11 @@ module Trans = struct
t , get ( )
(** [raw_constr_of_t] rebuilds a term in the raw representation *)
- let raw_constr_of_t ir rlt (context:rel_context) t =
+ let raw_constr_of_t ir rlt (context:Context.Rel.t) t =
(** cap rebuilds the products in front of the constr *)
let rec cap c = function [] -> c
| t::q ->
- let i = Context.lookup_rel t context in
+ let i = Context.Rel.lookup t context in
cap (mkProd_or_LetIn i c) q
in
let t,indices = raw_constr_of_t_debruijn ir t in
diff --git a/theory.mli b/theory.mli
index 1dae57b..fe79a11 100644
--- a/theory.mli
+++ b/theory.mli
@@ -160,7 +160,7 @@ module Trans : sig
reconstruct the named products on top of it. In particular, this
allow us to print the context put around the left (or right)
hand side of a pattern. *)
- val raw_constr_of_t : ir -> Coq.Relation.t -> (Context.rel_context)
->Matcher.Terms.t -> Term.constr
+ val raw_constr_of_t : ir -> Coq.Relation.t -> (Context.Rel.t)
->Matcher.Terms.t -> Term.constr
(** {2 Building reified terms} *)
--
Alioth's /usr/local/bin/git-commit-notice on
/srv/git.debian.org/git/pkg-ocaml-maint/packages/aac-tactics.git
_______________________________________________
Pkg-ocaml-maint-commits mailing list
Pkg-ocaml-maint-commits@lists.alioth.debian.org
http://lists.alioth.debian.org/cgi-bin/mailman/listinfo/pkg-ocaml-maint-commits
