From 1117d2e4a00debfbfa0157cc3e780916df72c26b Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 27 Dec 2016 16:06:42 +0000 Subject: 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} *) -- cgit v1.2.3