From a77bca84565b26aeedec3b210d761240d9d261f4 Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Thu, 5 Dec 2013 07:55:11 +0100 Subject: Imported Upstream version 0.4 --- Caveats.v | 3 + Makefile | 11 ++- Tutorial.v | 33 +++++++++ aac.mlpack | 1 + coq.ml | 2 + coq.mli | 1 + evm_compute.ml | 221 ++++++++++++++++++++++++++++++++++++++++++++++++++++++++ evm_compute.mli | 11 +++ rewrite.ml4 | 47 ++++++++++++ 9 files changed, 327 insertions(+), 3 deletions(-) create mode 100644 evm_compute.ml create mode 100644 evm_compute.mli diff --git a/Caveats.v b/Caveats.v index a7967cc..d0ec37a 100644 --- a/Caveats.v +++ b/Caveats.v @@ -13,6 +13,7 @@ with the path to the [aac_tactics] library *) +Add Rec LoadPath "." as AAC_tactics. Require Import AAC. Require Instances. @@ -370,3 +371,5 @@ to investigate on this in the future *) End Z. + + diff --git a/Makefile b/Makefile index 1043ce9..03775bc 100644 --- a/Makefile +++ b/Makefile @@ -1,24 +1,29 @@ -FILES := coq.mli helper.mli search_monad.mli matcher.mli theory.mli print.mli rewrite.mli \ - coq.ml helper.ml search_monad.ml matcher.ml theory.ml print.ml rewrite.ml4 \ +FILES := coq.mli helper.mli search_monad.mli matcher.mli theory.mli print.mli \ + evm_compute.mli evm_compute.ml \ + coq.ml helper.ml search_monad.ml matcher.ml theory.ml print.ml rewrite.ml4 \ aac.mlpack \ AAC.v Instances.v Tutorial.v Caveats.v ARGS := -R . AAC_tactics -.PHONY: coq clean +.PHONY: coq clean doc world: all doc all: Makefile.coq $(MAKE) -f Makefile.coq all +install: Makefile.coq + $(MAKE) -f Makefile.coq install + coq: Makefile.coq $(MAKE) -f Makefile.coq doc: Makefile.coq $(MAKE) -f Makefile.coq html + $(MAKE) -f Makefile.coq mlihtml Makefile.coq: Makefile $(VS) coq_makefile $(ARGS) $(FILES) -o Makefile.coq diff --git a/Tutorial.v b/Tutorial.v index 76006ca..6356a10 100644 --- a/Tutorial.v +++ b/Tutorial.v @@ -397,3 +397,36 @@ Section Examples. End Examples. +Section Match. + (* The following example is inspired by a question by Francois + Pottier, wokring in the context of separation logic. *) + + Variable T : Type. + Variable star : T -> T -> T. + Hypothesis P : T -> Prop. + + Context (starA : Associative eq star). + Context (starC : Commutative eq star). + + Hypothesis P_hereditary_left : forall a b, P (star a b) -> P a. + Hypothesis P_hereditary_right : forall a b, P (star a b) -> P b. + + Notation "a * b" := (star a b). + + Ltac crush := + match goal with + H: P ?R' |- P ?R => + let h := fresh in + aac_match (fun x => x * R) R' h; + rewrite <- h in H; + try eauto using P_hereditary_right + end. + + Goal forall a b c, P (c * a * c * b) -> P (b * a). + Proof. intros. crush. Qed. + + Goal forall a b c, exists d, P (d * a * c * b) -> P (b * d) /\ b = d. + Proof. intros. eexists. intros. split. crush. reflexivity. Qed. + +End Match. + diff --git a/aac.mlpack b/aac.mlpack index 0c12567..60d5298 100644 --- a/aac.mlpack +++ b/aac.mlpack @@ -4,4 +4,5 @@ Search_monad Matcher Theory Print +Evm_compute Rewrite diff --git a/coq.ml b/coq.ml index 7371913..132fbf7 100644 --- a/coq.ml +++ b/coq.ml @@ -148,6 +148,8 @@ module Leibniz = struct let path = ["Coq"; "Init"; "Logic"] let eq_refl = lazy (init_constant path "eq_refl") let eq_refl ty x = lapp eq_refl [| ty;x|] + let eq ty = Term.mkApp (init_constant path "eq", [| ty |]) + end module Option = struct diff --git a/coq.mli b/coq.mli index a0f2ce0..53d42eb 100644 --- a/coq.mli +++ b/coq.mli @@ -79,6 +79,7 @@ end module Leibniz : sig val eq_refl : Term.types -> Term.constr -> Term.constr + val eq : Term.types -> Term.constr end module Option : sig diff --git a/evm_compute.ml b/evm_compute.ml new file mode 100644 index 0000000..b10a9cd --- /dev/null +++ b/evm_compute.ml @@ -0,0 +1,221 @@ +(*i camlp4deps: "parsing/grammar.cma" i*) +(*i camlp4use: "pa_extend.cmp" i*) + + +let pp_constr fmt x = Pp.pp_with fmt (Printer.pr_constr x) +let pp_list pp fmt l = List.iter (fun x -> Format.fprintf fmt "%a; " pp x) l +let pp_list_nl pp fmt l = List.iter (fun x -> Format.fprintf fmt "%a;\n" pp x) l +let pp_constrs fmt l = (pp_list pp_constr) fmt l + +type constr = Term.constr + +module Replace (X : sig val eq: Term.constr -> Term.constr -> bool + val subst : (Term.constr * Term.constr) list end) = + struct + + (* assumes that [c] and [t] have no outer casts, and all + applications have been flattened *) + let rec find l (t: constr) = + match l with + | [] -> None + | (c,c') :: q -> + begin + match Term.kind_of_term c, Term.kind_of_term t with + | Term.App (f1,args1), Term.App (f2, args2) -> + let l1 = Array.length args1 in + let l2 = Array.length args2 in + if l1 <= l2 && X.eq c (Term.mkApp (f2, Array.sub args2 0 l1)) + then + (* we must return the array of arguments, to make the + substitution in them too *) + Some (c',Array.sub args2 l1 (l2 - l1)) + else + find q t + | _, _ -> + if X.eq c t + then Some (c', [| |]) + else find q t + end + + + let replace_terms t = + let rec aux (k:int) t = + match find X.subst t with + | Some (t',v) -> + let v' = Array.map (Term.map_constr_with_binders (succ) aux k) v in + Term.mkApp (Term.lift k t', v') + | None -> + Term.map_constr_with_binders succ aux k t + in aux 0 t + + end + +let nowhere = + { Tacexpr.onhyps = Some []; + Tacexpr.concl_occs = Glob_term.no_occurrences_expr + } + +let mk_letin + (name:string) + (c: constr) + (k : Names .identifier -> Proof_type.tactic) +: Proof_type.tactic = + fun goal -> + let name = (Names.id_of_string name) in + let name = Tactics.fresh_id [] name goal in + let letin = (Tactics.letin_tac None (Names.Name name) c None nowhere) in + Tacticals.tclTHEN letin (k name) goal + +let assert_tac + (name:string) + (c: constr) + (by:Proof_type.tactic) + (k : Names.identifier -> Proof_type.tactic) +: Proof_type.tactic = + fun goal -> + let name = (Names.id_of_string name) in + let name = Tactics.fresh_id [] name goal in + let t = (Tactics.assert_tac (Names.Name name) c) in + Tacticals.tclTHENS t [by; (k name)] goal + + +(* The contrib name is used to locate errors when loading constrs *) +let contrib_name = "evm_compute" + +(* Getting constrs (primitive Coq terms) from existing Coq + libraries. *) +let find_constant contrib dir s = + Libnames.constr_of_global (Coqlib.find_reference contrib dir s) + +let init_constant dir s = find_constant contrib_name dir s + +module Leibniz = struct + let path = ["Coq"; "Init"; "Logic"] + + let eq_refl t x= + Term.mkApp (init_constant path "eq_refl", [| t; x|]) + + let eq t x y = + Term.mkApp (init_constant path "eq", [| t; x ; y|]) + + let eq_ind_r ty x p px y yx = + Term.mkApp (init_constant path "eq_ind_r", [|ty;x;p;px;y;yx|]) +end + +let mk_vm_cast t c = Term.mkCast (c,Term.VMcast,t) + +let mk_let + (name:Names.identifier) + (c: constr) + (t: constr) + (k : Names.identifier -> constr) = + Term.mkNamedLetIn name c t (Term.subst_vars [name] (k name)) + +let mk_fun + (name:Names.identifier) + (t: constr) + (k : Names.identifier -> constr) = + Term.mkNamedLambda name t (Term.subst_vars [name] (k name)) + +let rec has_evar x = + match Term.kind_of_term x with + | Term.Evar _ -> true + | Term.Rel _ | Term.Var _ | Term.Meta _ | Term.Sort _ | Term.Const _ | Term.Ind _ | Term.Construct _ -> + false + | Term.Cast (t1, _, t2) | Term.Prod (_, t1, t2) | Term.Lambda (_, t1, t2) -> + has_evar t1 || has_evar t2 + | Term.LetIn (_, t1, t2, t3) -> + has_evar t1 || has_evar t2 || has_evar t3 + | Term.App (t1, ts) -> + has_evar t1 || has_evar_array ts + | Term.Case (_, t1, t2, ts) -> + has_evar t1 || has_evar t2 || has_evar_array ts + | Term.Fix ((_, tr)) | Term.CoFix ((_, tr)) -> + has_evar_prec tr +and has_evar_array x = + Util.array_exists has_evar x +and has_evar_prec (_, ts1, ts2) = + Util.array_exists has_evar ts1 || Util.array_exists has_evar ts2 + +let evm_compute eq blacklist = fun gl -> + (* the type of the conclusion of the goal is [concl] *) + let concl = Tacmach.pf_concl gl in + + let extra = + List.fold_left (fun acc (id,body,ty) -> + match body with + | None -> acc + | Some body -> if has_evar body then (Term.mkVar id :: acc) else acc) + [] (Tacmach.pf_hyps gl) in + + (* the set of evars that appear in the goal *) + let evars = Evd.evar_list (Tacmach.project gl) concl in + + (* the arguments of the function are: the constr that are blacklisted, then the evars *) + let args = extra @ blacklist @ (List.map (fun x -> Term.mkEvar x) evars) in + + let argsv = Array.of_list args in + + let context = (Termops.rel_list 0 (List.length args)) in + + (* we associate to each argument the proper de bruijn index *) + let (subst: (Term.constr * Term.constr) list) = List.combine args context in + + let module R = Replace(struct let eq = eq let subst = subst end) in + + let t = R.replace_terms concl in + + (* we have to retype both the blacklist and the evars to know how to build the final product *) + let rel_context = List.map (fun x -> Names.Anonymous, None, Tacmach.pf_type_of gl x) args in + + (* the abstraction *) + let t = Term.it_mkLambda_or_LetIn t (List.rev rel_context) in + + let typeof_t = (Tacmach.pf_type_of gl t) in + + (* the normal form of the head function *) + let nft = Vnorm.cbv_vm (Tacmach.pf_env gl) t typeof_t in + + + let (!!) x = Tactics.fresh_id [] ((Names.id_of_string x)) gl in + + (* p = [fun x => x a_i] which corresponds to the type of the goal when applied to [t] *) + let p = mk_fun (!! "x") typeof_t (fun x -> Term.mkApp (Term.mkVar x,argsv)) in + + let proof_term pnft = begin + mk_let (!! "nft") nft typeof_t (fun nft -> let nft' = Term.mkVar nft in + mk_let (!! "t") t typeof_t (fun t -> let t' = Term.mkVar t in + mk_let (!! "H") (mk_vm_cast (Leibniz.eq typeof_t t' nft') (Leibniz.eq_refl typeof_t nft')) (Leibniz.eq typeof_t t' nft') + (fun h -> + (* typeof_t -> Prop *) + let body = Leibniz.eq_ind_r typeof_t + nft' p pnft t' (Term.mkVar h) + in + Term.mkCast (body, Term.DEFAULTcast, Term.mkApp (t', argsv)) + ))) + end in + + try + assert_tac "subgoal" (Term.mkApp (p,[| nft |])) + Tacticals.tclIDTAC + (fun subgoal -> + (* We use the tactic [exact_no_check]. It has two consequences: + - first, it means that in theory we could produce ill typed proof terms, that fail to type check at Qed; + - second, it means that we are able to use vm_compute and vm_compute casts, that will be checkable at Qed time when all evars have been instantiated. + *) + Tactics.exact_no_check (proof_term (Term.mkVar subgoal)) + ) gl + with + | e -> + Tacticals.tclFAIL 0 (Pp.str (Printf.sprintf "evm_compute failed with an exception %s" (Printexc.to_string e))) gl + +;; + +let evm_compute_in eq blacklist h = fun gl -> + let concl = Tacmach.pf_concl gl in + Tacticals.tclTHENLIST + [Tactics.revert [h]; + evm_compute eq (concl :: blacklist); + Tactics.introduction h + ] + gl diff --git a/evm_compute.mli b/evm_compute.mli new file mode 100644 index 0000000..f50c0db --- /dev/null +++ b/evm_compute.mli @@ -0,0 +1,11 @@ + + +(** [evm_compute eq blacklist] performs a vm_compute step with the + following provisos: evars can appear in the goal; terms that are + equal (modulo eq) to terms in the blacklist are abstracted + before-hand. *) +val evm_compute : (Term.constr -> Term.constr -> bool) -> Term.constr list -> Proof_type.tactic + + +(** [evm_compute eq blacklist h] performs an evm_compute step in the hypothesis h *) +val evm_compute_in : (Term.constr -> Term.constr -> bool) -> Term.constr list -> Names.identifier -> Proof_type.tactic diff --git a/rewrite.ml4 b/rewrite.ml4 index 6229262..383d706 100644 --- a/rewrite.ml4 +++ b/rewrite.ml4 @@ -32,6 +32,10 @@ let push_anomaly msg = function | Util.Anomaly _ as e -> raise e | _ -> Coq.anomaly msg + + + + module M = Matcher open Term @@ -435,6 +439,41 @@ let aac_rewrite ?abort rew ?(l2r=true) ?(show = false) ?(in_left=true) ?strict ) goal +(** [aac_match eq (fun x1 ... xn => p) t H] match the term [t] against + the pattern, and introduces an hypothesis H of type p = t. (Note + that we have performed the substitution in p). +*) + +let aac_match ~eq pattern term h = fun gl -> + let env = Tacmach.pf_env gl in + let evar_map = Tacmach.project gl in + let carrier = Typing.type_of env evar_map term in + let rel = Coq.Relation.make carrier eq in + let equiv,gl = Coq.Equivalence.from_relation gl rel in + (* first, we decompose the pattern as an arity. *) + let x_args, pat = Term.decompose_lam pattern in + (* then, we reify the pattern and the term, using the provided equality *) + let envs = Theory.Trans.empty_envs () in + let left, right,gl = Theory.Trans.t_of_constr gl rel envs (pat,term) in + let gl,ir = Theory.Trans.ir_of_envs gl rel envs in + let solutions = Matcher.matcher (Theory.Trans.ir_to_units ir) left right in + (* then, we pick the first solution to the matching problem *) + let sigma = match Search_monad.choose solutions with + | None -> Coq.user_error "no solution to the matching problem" + | Some sigma -> sigma + in + let p_sigma = Matcher.Subst.instantiate sigma left in + let args = List.map (fun (x,t) -> x,Theory.Trans.raw_constr_of_t ir rel [] t) (Matcher.Subst.to_list sigma) in + (* Then, we have to assert the fact that p_sigma is equal to term *) + let equation = mkApp (eq, [| Theory.Trans.raw_constr_of_t ir rel [] p_sigma ; term |]) in + let evar_map = Tacmach.project gl in + Tacticals.tclTHENLIST + [ + Refiner.tclEVARS evar_map; + Tactics.assert_by h equation (by_aac_reflexivity term equiv ir p_sigma right); + ] gl + + open Coq.Rewrite open Tacmach open Tacticals @@ -522,3 +561,11 @@ TACTIC EXTEND _aacu_instances_ | [ "aacu_instances" orient(l2r) constr(c) aac_args(args) constro(extra)] -> [ fun gl -> aac_rewrite ?extra ~args ~l2r ~strict:false ~show:true c gl ] END + +TACTIC EXTEND _aac_match_ +| [ "aac_match" constr(p) constr(t) ident(h)] -> + [ fun gl -> + let ty = Tacmach.pf_type_of gl t in + let eq = Coq.Leibniz.eq ty in + aac_match ~eq p t (Names.Name h) gl] +END -- cgit v1.2.3