From 8917ab003a9b7f2abf8e399b5e7ad013b31a2e0e Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Thu, 20 Sep 2012 09:41:14 +0200 Subject: Imported Upstream version 0.3 --- AAC.v | 4 +- AAC_coq.ml | 591 ----------------------- AAC_coq.mli | 231 --------- AAC_helper.ml | 41 -- AAC_helper.mli | 33 -- AAC_matcher.ml | 1293 -------------------------------------------------- AAC_matcher.mli | 189 -------- AAC_print.ml | 100 ---- AAC_print.mli | 23 - AAC_rewrite.ml | 524 -------------------- AAC_rewrite.mli | 9 - AAC_search_monad.ml | 70 --- AAC_search_monad.mli | 42 -- AAC_theory.ml | 1097 ------------------------------------------ AAC_theory.mli | 197 -------- CHANGELOG | 5 + Caveats.v | 2 - Instances.v | 22 +- Makefile | 326 +------------ README.txt | 7 +- Tutorial.v | 2 +- aac.mlpack | 7 + coq.ml | 592 +++++++++++++++++++++++ coq.mli | 231 +++++++++ helper.ml | 41 ++ helper.mli | 33 ++ magic.txt | 5 - make_makefile | 62 --- matcher.ml | 1293 ++++++++++++++++++++++++++++++++++++++++++++++++++ matcher.mli | 189 ++++++++ print.ml | 100 ++++ print.mli | 23 + rewrite.ml4 | 524 ++++++++++++++++++++ rewrite.mli | 9 + search_monad.ml | 70 +++ search_monad.mli | 42 ++ theory.ml | 1097 ++++++++++++++++++++++++++++++++++++++++++ theory.mli | 197 ++++++++ 38 files changed, 4488 insertions(+), 4835 deletions(-) delete mode 100644 AAC_coq.ml delete mode 100644 AAC_coq.mli delete mode 100644 AAC_helper.ml delete mode 100644 AAC_helper.mli delete mode 100644 AAC_matcher.ml delete mode 100644 AAC_matcher.mli delete mode 100644 AAC_print.ml delete mode 100644 AAC_print.mli delete mode 100644 AAC_rewrite.ml delete mode 100644 AAC_rewrite.mli delete mode 100644 AAC_search_monad.ml delete mode 100644 AAC_search_monad.mli delete mode 100644 AAC_theory.ml delete mode 100644 AAC_theory.mli create mode 100644 aac.mlpack create mode 100644 coq.ml create mode 100644 coq.mli create mode 100644 helper.ml create mode 100644 helper.mli delete mode 100644 magic.txt delete mode 100755 make_makefile create mode 100644 matcher.ml create mode 100644 matcher.mli create mode 100644 print.ml create mode 100644 print.mli create mode 100644 rewrite.ml4 create mode 100644 rewrite.mli create mode 100644 search_monad.ml create mode 100644 search_monad.mli create mode 100644 theory.ml create mode 100644 theory.mli diff --git a/AAC.v b/AAC.v index 0f5e85d..a16f1a0 100644 --- a/AAC.v +++ b/AAC.v @@ -82,7 +82,7 @@ Proof. Qed. Instance aac_lift_proper {X} {R : relation X} {E} {HE: Equivalence E} - {HR: Proper (E==>E==>iff) R}: AAC_lift R E | 4. + {HR: Proper (E==>E==>iff) R}: AAC_lift R E | 4 := {}. @@ -1132,4 +1132,4 @@ Section t. End t. -Declare ML Module "aac_tactics". +Declare ML Module "aac". diff --git a/AAC_coq.ml b/AAC_coq.ml deleted file mode 100644 index b3ee180..0000000 --- a/AAC_coq.ml +++ /dev/null @@ -1,591 +0,0 @@ -(***************************************************************************) -(* This is part of aac_tactics, it is distributed under the terms of the *) -(* GNU Lesser General Public License version 3 *) -(* (see file LICENSE for more details) *) -(* *) -(* Copyright 2009-2010: Thomas Braibant, Damien Pous. *) -(***************************************************************************) - -(** Interface with Coq *) -type constr = Term.constr - -open Term -open Names -open Coqlib - -(* The contrib name is used to locate errors when loading constrs *) -let contrib_name = "aac_tactics" - -(* 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 - -(* A clause specifying that the [let] should not try to fold anything - in the goal *) -let nowhere = - { Tacexpr.onhyps = Some []; - Tacexpr.concl_occs = Rawterm.no_occurrences_expr - } - -let cps_mk_letin - (name:string) - (c: constr) - (k : constr -> 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 (Name name) c None nowhere) in - Tacticals.tclTHEN letin (k (mkVar name)) goal - -(** {2 General functions} *) - -type goal_sigma = Proof_type.goal Tacmach.sigma -let goal_update (goal : goal_sigma) evar_map : goal_sigma= - let it = Tacmach.sig_it goal in - Tacmach.re_sig it evar_map - -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 evar_map env ty in - x,( goal_update goal em) - -let resolve_one_typeclass goal ty : constr*goal_sigma= - let env = Tacmach.pf_env goal in - let evar_map = Tacmach.project goal in - let em,c = Typeclasses.resolve_one_typeclass env evar_map ty in - c, (goal_update goal em) - -let general_error = - "Cannot resolve a typeclass : please report" - -let cps_resolve_one_typeclass ?error : Term.types -> (Term.constr -> Proof_type.tactic) -> Proof_type.tactic = fun t k goal -> - Tacmach.pf_apply - (fun env em -> let em ,c = - try Typeclasses.resolve_one_typeclass env em t - with Not_found -> - begin match error with - | None -> Util.anomaly "Cannot resolve a typeclass : please report" - | Some x -> Util.error x - end - in - Tacticals.tclTHENLIST [Refiner.tclEVARS em; k c] goal - ) goal - - -let nf_evar goal c : Term.constr= - let evar_map = Tacmach.project goal in - Evarutil.nf_evar evar_map c - -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 evar_map env x 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 evar_map env ty 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 evar_map env ty 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 em env ty in - Tacticals.tclTHENLIST [Refiner.tclEVARS em; k r] goal - ) goal - -(* decomp_term : constr -> (constr, types) kind_of_term *) -let decomp_term c = kind_of_term (strip_outer_cast c) - -let lapp c v = mkApp (Lazy.force c, v) - -(** {2 Bindings with Coq' Standard Library} *) -module Std = struct -(* Here we package the module to be able to use List, later *) - -module Pair = struct - - let path = ["Coq"; "Init"; "Datatypes"] - let typ = lazy (init_constant path "prod") - let pair = lazy (init_constant path "pair") - let of_pair t1 t2 (x,y) = - mkApp (Lazy.force pair, [| t1; t2; x ; y|] ) -end - -module Bool = struct - let path = ["Coq"; "Init"; "Datatypes"] - let typ = lazy (init_constant path "bool") - let ctrue = lazy (init_constant path "true") - let cfalse = lazy (init_constant path "false") - let of_bool b = - if b then Lazy.force ctrue else Lazy.force cfalse -end - -module Comparison = struct - let path = ["Coq"; "Init"; "Datatypes"] - let typ = lazy (init_constant path "comparison") - let eq = lazy (init_constant path "Eq") - let lt = lazy (init_constant path "Lt") - let gt = lazy (init_constant path "Gt") -end - -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|] -end - -module Option = struct - let path = ["Coq"; "Init"; "Datatypes"] - let typ = lazy (init_constant path "option") - let some = lazy (init_constant path "Some") - let none = lazy (init_constant path "None") - let some t x = mkApp (Lazy.force some, [| t ; x|]) - let none t = mkApp (Lazy.force none, [| t |]) - let of_option t x = match x with - | Some x -> some t x - | None -> none t -end - -module Pos = struct - - let path = ["Coq" ; "NArith"; "BinPos"] - let typ = lazy (init_constant path "positive") - let xI = lazy (init_constant path "xI") - let xO = lazy (init_constant path "xO") - let xH = lazy (init_constant path "xH") - - (* A coq positive from an int *) - let of_int n = - let rec aux n = - begin match n with - | n when n < 1 -> assert false - | 1 -> Lazy.force xH - | n -> mkApp - ( - (if n mod 2 = 0 - then Lazy.force xO - else Lazy.force xI - ), [| aux (n/2)|] - ) - end - in - aux n -end - -module Nat = struct - let path = ["Coq" ; "Init"; "Datatypes"] - let typ = lazy (init_constant path "nat") - let _S = lazy (init_constant path "S") - let _O = lazy (init_constant path "O") - (* A coq nat from an int *) - let of_int n = - let rec aux n = - begin match n with - | n when n < 0 -> assert false - | 0 -> Lazy.force _O - | n -> mkApp - ( - (Lazy.force _S - ), [| aux (n-1)|] - ) - end - in - aux n -end - -(** Lists from the standard library*) -module List = struct - let path = ["Coq"; "Lists"; "List"] - let typ = lazy (init_constant path "list") - let nil = lazy (init_constant path "nil") - let cons = lazy (init_constant path "cons") - let cons ty h t = - mkApp (Lazy.force cons, [| ty; h ; t |]) - let nil ty = - (mkApp (Lazy.force nil, [| ty |])) - let rec of_list ty = function - | [] -> nil ty - | t::q -> cons ty t (of_list ty q) - let type_of_list ty = - mkApp (Lazy.force typ, [|ty|]) -end - -(** Morphisms *) -module Classes = -struct - let classes_path = ["Coq";"Classes"; ] - let morphism = lazy (init_constant (classes_path@["Morphisms"]) "Proper") - let equivalence = lazy (init_constant (classes_path@ ["RelationClasses"]) "Equivalence") - let reflexive = lazy (init_constant (classes_path@ ["RelationClasses"]) "Reflexive") - let transitive = lazy (init_constant (classes_path@ ["RelationClasses"]) "Transitive") - - (** build the type [Equivalence ty rel] *) - let mk_equivalence ty rel = - mkApp (Lazy.force equivalence, [| ty; rel|]) - - - (** build the type [Reflexive ty rel] *) - let mk_reflexive ty rel = - mkApp (Lazy.force reflexive, [| ty; rel|]) - - (** build the type [Proper rel t] *) - let mk_morphism ty rel t = - mkApp (Lazy.force morphism, [| ty; rel; t|]) - - (** build the type [Transitive ty rel] *) - let mk_transitive ty rel = - mkApp (Lazy.force transitive, [| ty; rel|]) -end - -module Relation = struct - type t = - { - carrier : constr; - r : constr; - } - - let make ty r = {carrier = ty; r = r } - let split t = t.carrier, t.r -end - -module Transitive = struct - type t = - { - carrier : constr; - leq : constr; - transitive : constr; - } - let make ty leq transitive = {carrier = ty; leq = leq; transitive = transitive} - let infer goal ty leq = - let ask = Classes.mk_transitive ty leq in - let transitive , goal = resolve_one_typeclass goal ask in - make ty leq transitive, goal - let from_relation goal rlt = - infer goal (rlt.Relation.carrier) (rlt.Relation.r) - let cps_from_relation rlt k = - let ty =rlt.Relation.carrier in - let r = rlt.Relation.r in - let ask = Classes.mk_transitive ty r in - cps_resolve_one_typeclass ask - (fun trans -> k (make ty r trans) ) - let to_relation t = - {Relation.carrier = t.carrier; Relation.r = t.leq} - -end - -module Equivalence = struct - type t = - { - carrier : constr; - eq : constr; - equivalence : constr; - } - let make ty eq equivalence = {carrier = ty; eq = eq; equivalence = equivalence} - let infer goal ty eq = - let ask = Classes.mk_equivalence ty eq in - let equivalence , goal = resolve_one_typeclass goal ask in - make ty eq equivalence, goal - let from_relation goal rlt = - infer goal (rlt.Relation.carrier) (rlt.Relation.r) - let cps_from_relation rlt k = - let ty =rlt.Relation.carrier in - let r = rlt.Relation.r in - let ask = Classes.mk_equivalence ty r in - cps_resolve_one_typeclass ask (fun equiv -> k (make ty r equiv) ) - let to_relation t = - {Relation.carrier = t.carrier; Relation.r = t.eq} - let split t = - t.carrier, t.eq, t.equivalence -end -end -(**[ match_as_equation goal eqt] see [eqt] as an equation. An - optionnal rel_context can be provided to ensure taht the term - remains typable*) -let match_as_equation ?(context = Term.empty_rel_context) 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 - begin - match decomp_term equation with - | App(c,ca) when Array.length ca >= 2 -> - let n = Array.length ca in - let left = ca.(n-2) in - let right = ca.(n-1) in - let r = (mkApp (c, Array.sub ca 0 (n - 2))) in - let carrier = Typing.type_of env evar_map left in - let rlt =Std.Relation.make carrier r - in - Some (left, right, rlt ) - | _ -> None - end - - -(** {1 Tacticals} *) - -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 - r - -let tclDEBUG msg tac = fun gl -> - let _ = Pp.msgnl (Pp.str msg) in - tac gl - -let tclPRINT tac = fun gl -> - let _ = Pp.msgnl (Printer.pr_constr (Tacmach.pf_concl gl)) in - tac gl - - -(** {1 Error related mechanisms} *) -(* 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 = - Util.anomaly ("[aac_tactics] " ^ msg) - -let user_error msg = - Util.error ("[aac_tactics] " ^ msg) - -let warning msg = - Pp.msg_warning (Pp.str ("[aac_tactics]" ^ msg)) - - -(** {1 Rewriting tactics used in aac_rewrite} *) -module Rewrite = struct -(** Some informations about the hypothesis, with an (informal) - invariant: - - [typeof hyp = hyptype] - - [hyptype = forall context, body] - - [body = rel left right] - -*) - -type hypinfo = - { - hyp : Term.constr; (** the actual constr corresponding to the hypothese *) - hyptype : Term.constr; (** the type of the hypothesis *) - context : Term.rel_context; (** 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 *) - right : Term.constr; (** right hand side *) - l2r : bool; (** rewriting from left to right *) - } - -let get_hypinfo c ~l2r ?check_type (k : hypinfo -> Proof_type.tactic) : Proof_type.tactic = fun goal -> - let ctype = Tacmach.pf_type_of goal c in - 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 = Term.lookup_rel i rel_context - in f types - | _ -> 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"; - end; - begin - match match_as_equation ~context:rel_context goal body_type with - | None -> - user_error "The hypothesis is not an applied relation" - | Some (hleft,hright,hrlt) -> - k { - hyp = c; - hyptype = ctype; - body = body_type; - l2r = l2r; - context = rel_context; - rel = hrlt ; - left =hleft; - right = hright; - } - goal - end - - -(* The problem : Given a term to rewrite of type [H :forall xn ... x1, - t], we have to instanciate the subset of [xi] of type - [carrier]. [subst : (int * constr)] is the mapping the debruijn - indices in [t] to the [constrs]. We need to handle the rest of the - indexes. Two ways : - - - either using fresh evars and rewriting [H tn ?1 tn-2 ?2 ] - - either building a term like [fun 1 2 => H tn 1 tn-2 2] - - Both these terms have the same type. -*) - - -(* Fresh evars for everyone (should be the good way to do this - recompose in Coq v8.4) *) -let recompose_prod - (context : Term.rel_context) - (subst : (int * Term.constr) list) - env - em - : Evd.evar_map * Term.constr list = - (* the last index of rel relevant for the rewriting *) - let min_n = List.fold_left - (fun acc (x,_) -> min acc x) - (List.length context) subst in - let rec aux context acc em n = - let _ = Printf.printf "%i\n%!" n in - match context with - | [] -> - env, em, acc - | ((name,c,ty) as 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 em env (Term.substl acc ty) - in - (Environ.push_rel t env), em,x::acc - else - env,em,acc - in - let _,em,acc = aux context [] em 1 in - em, acc - -(* no fresh evars : instead, use a lambda abstraction around an - application to handle non-instanciated variables. *) - -let recompose_prod' - (context : Term.rel_context) - (subst : (int *Term.constr) list) - c - = - let rec popn pop n l = - if n <= 0 then l - else match l with - | [] -> [] - | t::q -> pop t :: (popn pop (n-1) q) - in - let pop_rel_decl (name,c,ty) = (name,c,Termops.pop ty) in - let rec aux sign n next app ctxt = - match sign with - | [] -> List.rev app, List.rev ctxt - | decl::sign -> - try let term = (List.assoc n subst) in - aux sign (n+1) next (term::app) (None :: ctxt) - with - | Not_found -> - let term = Term.mkRel next in - aux sign (n+1) (next+1) (term::app) (Some decl :: ctxt) - in - let app,ctxt = aux context 1 1 [] [] in - (* substitutes in the context *) - let rec update ctxt app = - match ctxt,app with - | [],_ -> [] - | _,[] -> [] - | None :: sign, _ :: app -> - None :: update sign (List.map (Termops.pop) app) - | Some decl :: sign, _ :: app -> - Some (Term.substl_decl app decl)::update sign (List.map (Termops.pop) app) - in - let ctxt = update ctxt app in - (* updates the rel accordingly, taking some care not to go to far - beyond: it is important not to lift indexes homogeneously, we - have to update *) - let rec update ctxt res n = - match ctxt with - | [] -> List.rev res - | None :: sign -> - (update (sign) (popn pop_rel_decl n res) 0) - | Some decl :: sign -> - update sign (decl :: res) (n+1) - in - let ctxt = update ctxt [] 0 in - let c = Term.applistc c (List.rev app) in - let c = Term.it_mkLambda_or_LetIn c (ctxt) in - c - -(* Version de Matthieu -let subst_rel_context k cstr ctx = - let (_, ctx') = - List.fold_left (fun (k, ctx') (id, b, t) -> (succ k, (id, Option.map - (Term.substnl [cstr] k) b, Term.substnl [cstr] k t) :: ctx')) (k, []) - ctx in List.rev ctx' - -let recompose_prod' context subst c = - let len = List.length context in - let rec aux sign n next app ctxt = - match sign with - | [] -> List.rev app, List.rev ctxt - | decl::sign -> - try let term = (List.assoc n subst) in - aux (subst_rel_context 0 term sign) (pred n) (succ next) - (term::List.map (Term.lift (-1)) app) ctxt - with Not_found -> - let term = Term.mkRel (len - next) in - aux sign (pred n) (succ next) (term::app) (decl :: ctxt) - in - let app,ctxt = aux (List.rev context) len 0 [] [] in - Term.it_mkLambda_or_LetIn (Term.applistc c(app)) (List.rev ctxt) -*) - -let build - (h : hypinfo) - (subst : (int *Term.constr) list) - (k :Term.constr -> Proof_type.tactic) - : Proof_type.tactic = fun goal -> - let c = recompose_prod' h.context subst h.hyp in - Tacticals.tclTHENLIST [k c] goal - -let build_with_evar - (h : hypinfo) - (subst : (int *Term.constr) list) - (k :Term.constr -> Proof_type.tactic) - : Proof_type.tactic - = fun goal -> - Tacmach.pf_apply - (fun env em -> - let evar_map, acc = recompose_prod h.context subst env em in - let c = Term.applistc h.hyp (List.rev acc) in - Tacticals.tclTHENLIST [Refiner.tclEVARS evar_map; k c] goal - ) goal - - -let rewrite ?(abort=false)hypinfo subst k = - build hypinfo subst - (fun rew -> - let tac = - if not abort then - Equality.general_rewrite_bindings - hypinfo.l2r - Termops.all_occurrences - false - (rew,Rawterm.NoBindings) - true - else - Tacticals.tclIDTAC - in k tac - ) - - -end - -include Std diff --git a/AAC_coq.mli b/AAC_coq.mli deleted file mode 100644 index a0f2ce0..0000000 --- a/AAC_coq.mli +++ /dev/null @@ -1,231 +0,0 @@ -(***************************************************************************) -(* This is part of aac_tactics, it is distributed under the terms of the *) -(* GNU Lesser General Public License version 3 *) -(* (see file LICENSE for more details) *) -(* *) -(* Copyright 2009-2010: Thomas Braibant, Damien Pous. *) -(***************************************************************************) - -(** Interface with Coq where we define some handlers for Coq's API, - and we import several definitions from Coq's standard library. - - This general purpose library could be reused by other plugins. - - Some salient points: - - we use Caml's module system to mimic Coq's one, and avoid cluttering - the namespace; - - we also provide several handlers for standard coq tactics, in - order to provide a unified setting (we replace functions that - modify the evar_map by functions that operate on the whole - goal, and repack the modified evar_map with it). - -*) - -(** {2 Getting Coq terms from the environment} *) - -val init_constant : string list -> string -> Term.constr - -(** {2 General purpose functions} *) - -type goal_sigma = Proof_type.goal Tacmach.sigma -val goal_update : goal_sigma -> Evd.evar_map -> goal_sigma -val resolve_one_typeclass : Proof_type.goal Tacmach.sigma -> Term.types -> Term.constr * goal_sigma -val cps_resolve_one_typeclass: ?error:string -> Term.types -> (Term.constr -> Proof_type.tactic) -> Proof_type.tactic -val nf_evar : goal_sigma -> Term.constr -> Term.constr -val fresh_evar :goal_sigma -> Term.types -> Term.constr* goal_sigma -val evar_unit :goal_sigma ->Term.constr -> Term.constr* goal_sigma -val evar_binary: goal_sigma -> Term.constr -> Term.constr* goal_sigma -val evar_relation: goal_sigma -> Term.constr -> Term.constr* goal_sigma -val cps_evar_relation : Term.constr -> (Term.constr -> Proof_type.tactic) -> Proof_type.tactic -(** [cps_mk_letin name v] binds the constr [v] using a letin tactic *) -val cps_mk_letin : string -> Term.constr -> ( Term.constr -> Proof_type.tactic) -> Proof_type.tactic - - -val decomp_term : Term.constr -> (Term.constr , Term.types) Term.kind_of_term -val lapp : Term.constr lazy_t -> Term.constr array -> Term.constr - -(** {2 Bindings with Coq' Standard Library} *) - -(** Coq lists *) -module List: -sig - (** [of_list ty l] *) - val of_list:Term.constr ->Term.constr list ->Term.constr - - (** [type_of_list ty] *) - val type_of_list:Term.constr ->Term.constr -end - -(** Coq pairs *) -module Pair: -sig - val typ:Term.constr lazy_t - val pair:Term.constr lazy_t - val of_pair : Term.constr -> Term.constr -> Term.constr * Term.constr -> Term.constr -end - -module Bool : sig - val typ : Term.constr lazy_t - val of_bool : bool -> Term.constr -end - - -module Comparison : sig - val typ : Term.constr lazy_t - val eq : Term.constr lazy_t - val lt : Term.constr lazy_t - val gt : Term.constr lazy_t -end - -module Leibniz : sig - val eq_refl : Term.types -> Term.constr -> Term.constr -end - -module Option : sig - val some : Term.constr -> Term.constr -> Term.constr - val none : Term.constr -> Term.constr - val of_option : Term.constr -> Term.constr option -> Term.constr -end - -(** Coq positive numbers (pos) *) -module Pos: -sig - val typ:Term.constr lazy_t - val of_int: int ->Term.constr -end - -(** Coq unary numbers (peano) *) -module Nat: -sig - val typ:Term.constr lazy_t - val of_int: int ->Term.constr -end - -(** Coq typeclasses *) -module Classes: -sig - val mk_morphism: Term.constr -> Term.constr -> Term.constr -> Term.constr - val mk_equivalence: Term.constr -> Term.constr -> Term.constr - val mk_reflexive: Term.constr -> Term.constr -> Term.constr - val mk_transitive: Term.constr -> Term.constr -> Term.constr -end - -module Relation : sig - type t = {carrier : Term.constr; r : Term.constr;} - val make : Term.constr -> Term.constr -> t - val split : t -> Term.constr * Term.constr -end - -module Transitive : sig - type t = - { - carrier : Term.constr; - leq : Term.constr; - transitive : Term.constr; - } - val make : Term.constr -> Term.constr -> Term.constr -> t - val infer : goal_sigma -> Term.constr -> Term.constr -> t * goal_sigma - val from_relation : goal_sigma -> Relation.t -> t * goal_sigma - val cps_from_relation : Relation.t -> (t -> Proof_type.tactic) -> Proof_type.tactic - val to_relation : t -> Relation.t -end - -module Equivalence : sig - type t = - { - carrier : Term.constr; - eq : Term.constr; - equivalence : Term.constr; - } - val make : Term.constr -> Term.constr -> Term.constr -> t - val infer : goal_sigma -> Term.constr -> Term.constr -> t * goal_sigma - val from_relation : goal_sigma -> Relation.t -> t * goal_sigma - val cps_from_relation : Relation.t -> (t -> Proof_type.tactic) -> Proof_type.tactic - val to_relation : t -> Relation.t - val split : t -> Term.constr * Term.constr * Term.constr -end - -(** [match_as_equation ?context goal c] try to decompose c as a - relation applied to two terms. An optionnal rel_context can be - provided to ensure that the term remains typable *) -val match_as_equation : ?context:Term.rel_context -> goal_sigma -> Term.constr -> (Term.constr * Term.constr * Relation.t) option - -(** {2 Some tacticials} *) - -(** time the execution of a tactic *) -val tclTIME : string -> Proof_type.tactic -> Proof_type.tactic - -(** emit debug messages to see which tactics are failing *) -val tclDEBUG : string -> Proof_type.tactic -> Proof_type.tactic - -(** print the current goal *) -val tclPRINT : Proof_type.tactic -> Proof_type.tactic - - -(** {2 Error related mechanisms} *) - -val anomaly : string -> 'a -val user_error : string -> 'a -val warning : string -> unit - - -(** {2 Rewriting tactics used in aac_rewrite} *) - -module Rewrite : sig - -(** The rewriting tactics used in aac_rewrite, build as handlers of the usual [setoid_rewrite]*) - - -(** {2 Datatypes} *) - -(** We keep some informations about the hypothesis, with an (informal) - invariant: - - [typeof hyp = typ] - - [typ = forall context, body] - - [body = rel left right] - -*) -type hypinfo = - { - hyp : Term.constr; (** the actual constr corresponding to the hypothese *) - hyptype : Term.constr; (** the type of the hypothesis *) - context : Term.rel_context; (** the quantifications of the hypothese *) - body : Term.constr; (** the body of the hypothese*) - rel : Relation.t; (** the relation *) - left : Term.constr; (** left hand side *) - right : Term.constr; (** right hand side *) - l2r : bool; (** rewriting from left to right *) - } - -(** [get_hypinfo H l2r ?check_type k] analyse the hypothesis H, and - build the related hypinfo, in CPS style. Moreover, an optionnal - function can be provided to check the type of every free - variable of the body of the hypothesis. *) -val get_hypinfo :Term.constr -> l2r:bool -> ?check_type:(Term.types -> bool) -> (hypinfo -> Proof_type.tactic) -> Proof_type.tactic - -(** {2 Rewriting with bindings} - - The problem : Given a term to rewrite of type [H :forall xn ... x1, - t], we have to instanciate the subset of [xi] of type - [carrier]. [subst : (int * constr)] is the mapping the De Bruijn - indices in [t] to the [constrs]. We need to handle the rest of the - indexes. Two ways : - - - either using fresh evars and rewriting [H tn ?1 tn-2 ?2 ] - - either building a term like [fun 1 2 => H tn 1 tn-2 2] - - Both these terms have the same type. -*) - -(** build the constr to rewrite, in CPS style, with lambda abstractions *) -val build : hypinfo -> (int * Term.constr) list -> (Term.constr -> Proof_type.tactic) -> Proof_type.tactic - -(** build the constr to rewrite, in CPS style, with evars *) -val build_with_evar : hypinfo -> (int * Term.constr) list -> (Term.constr -> Proof_type.tactic) -> Proof_type.tactic - -(** [rewrite ?abort hypinfo subst] builds the rewriting tactic - associated with the given [subst] and [hypinfo], and feeds it to - the given continuation. If [abort] is set to [true], we build - [tclIDTAC] instead. *) -val rewrite : ?abort:bool -> hypinfo -> (int * Term.constr) list -> (Proof_type.tactic -> Proof_type.tactic) -> Proof_type.tactic -end diff --git a/AAC_helper.ml b/AAC_helper.ml deleted file mode 100644 index 637def1..0000000 --- a/AAC_helper.ml +++ /dev/null @@ -1,41 +0,0 @@ -(***************************************************************************) -(* This is part of aac_tactics, it is distributed under the terms of the *) -(* GNU Lesser General Public License version 3 *) -(* (see file LICENSE for more details) *) -(* *) -(* Copyright 2009-2010: Thomas Braibant, Damien Pous. *) -(***************************************************************************) - -module type CONTROL = sig - val debug : bool - val time : bool - val printing : bool -end - -module Debug (X : CONTROL) = struct - open X - let debug x = - if debug then - Printf.printf "%s\n%!" x - - - let time f x fmt = - if time then - let t = Sys.time () in - let r = f x in - Printf.printf fmt (Sys.time () -. t); - r - else f x - - let pr_constr msg constr = - if printing then - ( Pp.msgnl (Pp.str (Printf.sprintf "=====%s====" msg)); - Pp.msgnl (Printer.pr_constr constr); - ) - - - let debug_exception msg e = - debug (msg ^ (Printexc.to_string e)) - - -end diff --git a/AAC_helper.mli b/AAC_helper.mli deleted file mode 100644 index f4e4454..0000000 --- a/AAC_helper.mli +++ /dev/null @@ -1,33 +0,0 @@ -(***************************************************************************) -(* This is part of aac_tactics, it is distributed under the terms of the *) -(* GNU Lesser General Public License version 3 *) -(* (see file LICENSE for more details) *) -(* *) -(* Copyright 2009-2010: Thomas Braibant, Damien Pous. *) -(***************************************************************************) - -(** Debugging functions, that can be triggered on a per-file base. *) - -module type CONTROL = -sig - val debug : bool - val time : bool - val printing : bool -end -module Debug : - functor (X : CONTROL) -> -sig - (** {!debug} prints the string and end it with a newline *) - val debug : string -> unit - val debug_exception : string -> exn -> unit - - (** {!time} computes the time spent in a function, and then - print it using the given format *) - val time : - ('a -> 'b) -> 'a -> (float -> unit, out_channel, unit) format -> 'b - - (** {!pr_constr} print a Coq constructor, that can be labelled - by a string *) - val pr_constr : string -> Term.constr -> unit - - end diff --git a/AAC_matcher.ml b/AAC_matcher.ml deleted file mode 100644 index 5d738e0..0000000 --- a/AAC_matcher.ml +++ /dev/null @@ -1,1293 +0,0 @@ -(***************************************************************************) -(* This is part of aac_tactics, it is distributed under the terms of the *) -(* GNU Lesser General Public License version 3 *) -(* (see file LICENSE for more details) *) -(* *) -(* Copyright 2009-2010: Thomas Braibant, Damien Pous. *) -(***************************************************************************) - -(** This module defines our matching functions, modulo associativity - and commutativity (AAC). - - The basic idea is to find a substitution [env] such that the - pattern [p] instantiated by [env] is equal to [t] modulo AAC. - - We proceed by structural decomposition of the pattern, and try all - possible non-deterministic split of the subject when needed. The - function {!matcher} is limited to top-level matching, that is, the - subject must make a perfect match against the pattern ([x+x] do - not match [a+a+b] ). We use a search monad {!Search} to perform - non-deterministic splits in an almost transparent way. We also - provide a function {!subterm} for finding a match that is a - subterm modulo AAC of the subject. Therefore, we are able to solve - the aforementioned case [x+x] against [a+b+a]. - - This file is structured as follows. First, we define the search - monad. Then,we define the two representations of terms (one - representing the AST, and one in normal form ), and environments - from variables to terms. Then, we use these parts to solve - matching problem. Finally, we wrap this function {!matcher} into - {!subterm} -*) - - -module Control = -struct - let debug = false - let time = false - let printing = false -end - -module Debug = AAC_helper.Debug (Control) -open Debug - -module Search = AAC_search_monad (* a handle *) - -type symbol = int -type var = int -type units = (symbol * symbol) list (* from AC/A symbols to the unit *) -type ext_units = - { - unit_for : units; - is_ac : (symbol * bool) list - } - -let print_units units= - List.iter (fun (op,unit) -> Printf.printf "%i %i\t" op unit) units; - Printf.printf "\n%!" - -exception NoUnit - -let get_unit units op = - try List.assoc op units - with - | Not_found -> raise NoUnit - -let is_unit units op unit = List.mem (op,unit) units - - -open Search - -type 'a mset = ('a * int) list -let linear p = - let rec ncons t l = function - | 0 -> l - | n -> t::ncons t l (n-1) - in - let rec aux = function - [ ] -> [] - | (t,n)::q -> let q = aux q in - ncons t q n - in aux p - - - -(** The module {!Terms} defines two different types for expressions. - - - a public type {!Terms.t} that represent abstract syntax trees of - expressions with binary associative (and commutative) operators - - - a private type {!Terms.nf_term} that represent an equivalence - class for terms that are equal modulo AAC. The constructions - functions on this type ensure the property that the term is in - normal form (that is, no sum can appear as a subterm of the same - sum, no trailing units, etc...). - -*) - -module Terms : sig - - (** {1 Abstract syntax tree of terms} - - Terms represented using this datatype are representation of the - AST of an expression. *) - - type t = - Dot of (symbol * t * t) - | Plus of (symbol * t * t) - | Sym of (symbol * t array) - | Var of var - | Unit of symbol - - val equal_aac : units -> t -> t -> bool - val size: t -> int - - (** {1 Terms in normal form} - - A term in normal form is the canonical representative of the - equivalence class of all the terms that are equal modulo - Associativity and Commutativity. Outside the {!AAC_matcher} module, - one does not need to access the actual representation of this - type. *) - - - type nf_term = private - | TAC of symbol * nf_term mset - | TA of symbol * nf_term list - | TSym of symbol * nf_term list - | TUnit of symbol - | TVar of var - - (** {2 Fresh variables: we provide some functions to pick some fresh variables with respect to a term} *) - val fresh_var_term : t -> int - val fresh_var_nfterm : nf_term -> int - - - (** {2 Constructors: we ensure that the terms are always - normalised - - braibant - Fri 27 Aug 2010, 15:11 - Moreover, we assure that we will not build empty sums or empty - products, leaving this task to the caller function. - } - *) - val mk_TAC : units -> symbol -> nf_term mset -> nf_term - val mk_TA : units -> symbol -> nf_term list -> nf_term - val mk_TSym : symbol -> nf_term list -> nf_term - val mk_TVar : var -> nf_term - val mk_TUnit : symbol -> nf_term - - (** {2 Comparisons} *) - val nf_term_compare : nf_term -> nf_term -> int - val nf_equal : nf_term -> nf_term -> bool - - (** {2 Printing function} *) - val sprint_nf_term : nf_term -> string - - (** {2 Conversion functions} *) - val term_of_t : units -> t -> nf_term - val t_of_term : nf_term -> t (* we could return the units here *) -end - = struct - - type t = - Dot of (symbol * t * t) - | Plus of (symbol * t * t) - | Sym of (symbol * t array) - | Var of var - | Unit of symbol - - let rec size = function - | Dot (_,x,y) - | Plus (_,x,y) -> size x+ size y + 1 - | Sym (_,v)-> Array.fold_left (fun acc x -> size x + acc) 1 v - | _ -> 1 - - - type nf_term = - | TAC of symbol * nf_term mset - | TA of symbol * nf_term list - | TSym of symbol * nf_term list - | TUnit of symbol - | TVar of var - - - (** {2 Picking fresh variables} *) - - (** [fresh_var_term] picks a fresh variable with respect to a term *) - let fresh_var_term t = - let rec aux = function - | Dot (_,t1,t2) - | Plus (_,t1,t2) -> max (aux t1) (aux t2) - | Sym (_,v) -> Array.fold_left (fun acc x -> max acc (aux x)) 0 v - | Var v -> assert (v >= 0); v - | Unit _ -> 0 - in - aux t - - (** [fresh_var_nfterm] picks a fresh_variable with respect to a term *) - let fresh_var_nfterm t = - let rec aux = function - | TAC (_,l) -> List.fold_left (fun acc (x,_) -> max acc (aux x)) 0 l - | TA (_,l) - | TSym (_,l) -> List.fold_left (fun acc x -> max acc (aux x)) 0 l - | TVar v -> assert (v >= 0); v - | TUnit _ -> 0 - in - aux t - - (** {2 Constructors: we ensure that the terms are always - normalised} *) - - (** {3 Pre constructors : These constructors ensure that sums and - products are not degenerated (no trailing units)} *) - let mk_TAC' units (s : symbol) l = match l with - | [] -> TUnit (get_unit units s ) - | [_,0] -> assert false - | [t,1] -> t - | _ -> TAC (s,l) - let mk_TA' units (s : symbol) l = match l with - | [] -> TUnit (get_unit units s ) - | [t] -> t - | _ -> TA (s,l) - - - (** {2 Comparison} *) - - let nf_term_compare = Pervasives.compare - let nf_equal a b = - a = b - - (** [merge_ac comp l1 l2] merges two lists of terms with coefficients - into one. Terms that are equal modulo the comparison function - [comp] will see their arities added. *) - - (* This function could be improved by the use of sorted msets *) - let merge_ac (compare : 'a -> 'a -> int) (l : 'a mset) (l' : 'a mset) : 'a mset = - let rec aux l l'= - match l,l' with - | [], _ -> l' - | _, [] -> l - | (t,tar)::q, (t',tar')::q' -> - begin match compare t t' with - | 0 -> ( t,tar+tar'):: aux q q' - | -1 -> (t, tar):: aux q l' - | _ -> (t', tar'):: aux l q' - end - in aux l l' - - (** [merge_map f l] uses the combinator [f] to combine the head of the - list [l] with the merge_maped tail of [l] *) - let rec merge_map (f : 'a -> 'b list -> 'b list) (l : 'a list) : 'b list = - match l with - | [] -> [] - | t::q -> f t (merge_map f q) - - - (** This function has to deal with the arities *) - let rec merge (l : nf_term mset) (l' : nf_term mset) : nf_term mset= - merge_ac nf_term_compare l l' - - let extract_A units s t = - match t with - | TA (s',l) when s' = s -> l - | TUnit u when is_unit units s u -> [] - | _ -> [t] - - let extract_AC units s (t,ar) : nf_term mset = - match t with - | TAC (s',l) when s' = s -> List.map (fun (x,y) -> (x,y*ar)) l - | TUnit u when is_unit units s u -> [] - | _ -> [t,ar] - - - (** {3 Constructors of {!nf_term}}*) - let mk_TAC units (s : symbol) (l : (nf_term *int) list) = - mk_TAC' units s - (merge_map (fun u l -> merge (extract_AC units s u) l) l) - let mk_TA units s l = - mk_TA' units s - (merge_map (fun u l -> (extract_A units s u) @ l) l) - let mk_TSym s l = TSym (s,l) - let mk_TVar v = TVar v - let mk_TUnit s = TUnit s - - - (** {2 Printing function} *) - let print_binary_list (single : 'a -> string) - (unit : string) - (binary : string -> string -> string) (l : 'a list) = - let rec aux l = - match l with - [] -> unit - | [t] -> single t - | t::q -> - let r = aux q in - Printf.sprintf "%s" (binary (single t) r) - in - aux l - - let print_symbol s = - match s with - | s, None -> Printf.sprintf "%i" s - | s , Some u -> Printf.sprintf "%i(unit %i)" s u - - let sprint_ac (single : 'a -> string) (l : 'a mset) = - (print_binary_list - (fun (x,t) -> - if t = 1 - then single x - else Printf.sprintf "%i*%s" t (single x) - ) - "0" - (fun x y -> x ^ " , " ^ y) - l - ) - - let print_symbol single s l = - match l with - [] -> Printf.sprintf "%i" s - | _ -> - Printf.sprintf "%i(%s)" - s - (print_binary_list single "" (fun x y -> x ^ "," ^ y) l) - - - let print_ac single s l = - Printf.sprintf "[%s:AC]{%s}" - (string_of_int s ) - (sprint_ac - single - l - ) - - let print_a single s l = - Printf.sprintf "[%s:A]{%s}" - (string_of_int s) - (print_binary_list single "1" (fun x y -> x ^ " , " ^ y) l) - - let rec sprint_nf_term = function - | TSym (s,l) -> print_symbol sprint_nf_term s l - | TAC (s,l) -> print_ac sprint_nf_term s l - | TA (s,l) -> print_a sprint_nf_term s l - | TVar v -> Printf.sprintf "x%i" v - | TUnit s -> Printf.sprintf "unit%i" s - - - - - (** {2 Conversion functions} *) - - (* rebuilds a tree out of a list, under the assumption that the list is not empty *) - let rec binary_of_list f comb l = - let l = List.rev l in - let rec aux = function - | [] -> assert false - | [t] -> f t - | t::q -> comb (aux q) (f t) - in - aux l - - let term_of_t units : t -> nf_term = - let rec term_of_t = function - | Dot (s,l,r) -> - let l = term_of_t l in - let r = term_of_t r in - mk_TA units s [l;r] - | Plus (s,l,r) -> - let l = term_of_t l in - let r = term_of_t r in - mk_TAC units s [l,1;r,1] - | Unit x -> - mk_TUnit x - | Sym (s,t) -> - let t = Array.to_list t in - let t = List.map term_of_t t in - mk_TSym s t - | Var i -> - mk_TVar ( i) - in - term_of_t - - let rec t_of_term : nf_term -> t = function - | TAC (s,l) -> - (binary_of_list - t_of_term - (fun l r -> Plus ( s,l,r)) - (linear l) - ) - | TA (s,l) -> - (binary_of_list - t_of_term - (fun l r -> Dot ( s,l,r)) - l - ) - | TSym (s,l) -> - let v = Array.of_list l in - let v = Array.map (t_of_term) v in - Sym ( s,v) - | TVar x -> Var x - | TUnit s -> Unit s - - - let equal_aac units x y = - nf_equal (term_of_t units x) (term_of_t units y) - end - - (** Terms environments defined as association lists from variables to - terms in normal form {! Terms.nf_term} *) - module Subst : sig - type t - - val find : t -> var -> Terms.nf_term option - val add : t -> var -> Terms.nf_term -> t - val empty : t - val instantiate : t -> Terms.t -> Terms.t - val sprint : t -> string - val to_list : t -> (var*Terms.t) list - end - = - struct - open Terms - - (** Terms environments, with nf_terms, to avoid costly conversions - of {!Terms.nf_terms} to {!Terms.t}, that will be mostly discarded*) - type t = (var * nf_term) list - - let find : t -> var -> nf_term option = fun t x -> - try Some (List.assoc x t) with | _ -> None - let add t x v = (x,v) :: t - let empty = [] - - let sprint (l : t) = - match l with - | [] -> Printf.sprintf "Empty environment\n" - | _ -> - let s = List.fold_left - (fun acc (x,y) -> - Printf.sprintf "%sX%i -> %s\n" - acc - x - (sprint_nf_term y) - ) - "" - (List.rev l) in - Printf.sprintf "%s\n%!" s - - - - (** [instantiate] is an homomorphism except for the variables*) - let instantiate (t: t) (x:Terms.t) : Terms.t = - let rec aux = function - | Unit _ as x -> x - | Sym (s,t) -> Sym (s,Array.map aux t) - | Plus (s,l,r) -> Plus (s, aux l, aux r) - | Dot (s,l,r) -> Dot (s, aux l, aux r) - | Var i -> - begin match find t i with - | None -> Util.error "aac_tactics: instantiate failure" - | Some x -> t_of_term x - end - in aux x - - let to_list t = List.map (fun (x,y) -> x,Terms.t_of_term y) t - end - - (******************) - (* MATCHING UTILS *) - (******************) - - open Terms - - (** Since most of the folowing functions require an extra parameter, - the units, we package them in a module. This functor will then be - applied to a module containing the units, in the exported - functions. *) - module M (X : sig - val units : units - val is_ac : (symbol * bool) list - val strict : bool (* variables cannot be instantiated with units *) - end) = struct - - open X - - let print_units ()= - List.iter (fun (op,unit) -> Printf.printf "%i %i\t" op unit) units; - Printf.printf "\n%!" - - let mk_TAC s l = mk_TAC units s l - let mk_TA s l = mk_TA units s l - let mk_TAC' s l = - try return( mk_TAC s l) - with _ -> fail () - let mk_TA' s l = - try return( mk_TA s l) - with _ -> fail () - - (** First, we need to be able to perform non-deterministic choice of - term splitting to satisfy a pattern. Indeed, we want to show that: - (x+a*b)*c <= a*b*c - *) - let a_nondet_split_raw t : ('a list * 'a list) m = - let rec aux l l' = - match l' with - | [] -> - return ( l,[]) - | t::q -> - return ( l,l' ) - >>| aux (l @ [t]) q - in - aux [] t - - (** Same as the previous [a_nondet_split], but split the list in 3 - parts *) - let a_nondet_middle t : ('a list * 'a list * 'a list) m = - a_nondet_split_raw t >> - (fun (left, right) -> - a_nondet_split_raw left >> - (fun (left, middle) -> return (left, middle, right)) - ) - - (** Non deterministic splits of ac lists *) - let dispatch f n = - let rec aux k = - if k = 0 then return (f n 0) - else return (f (n-k) k) >>| aux (k-1) - in - aux (n ) - - let add_with_arith x ar l = - if ar = 0 then l else (x,ar) ::l - - let ac_nondet_split_raw (l : 'a mset) : ('a mset * 'a mset) m = - let rec aux = function - | [] -> return ([],[]) - | (t,tar)::q -> - aux q - >> - (fun (left,right) -> - dispatch (fun arl arr -> - add_with_arith t arl left, - add_with_arith t arr right - ) - tar - ) - in - aux l - - let a_nondet_split current t : (nf_term * nf_term list) m= - a_nondet_split_raw t - >> - (fun (l,r) -> - if strict && (l=[]) - then fail() - else - mk_TA' current l >> - fun t -> return (t, r) - ) - - let ac_nondet_split current t : (nf_term * nf_term mset) m= - ac_nondet_split_raw t - >> - (fun (l,r) -> - if strict && (l=[]) - then fail() - else - mk_TAC' current l >> - fun t -> return (t, r) - ) - - - (** Try to affect the variable [x] to each left factor of [t]*) - let var_a_nondet_split env current x t = - a_nondet_split current t - >> - (fun (t,res) -> - return ((Subst.add env x t), res) - ) - - (** Try to affect variable [x] to _each_ subset of t. *) - let var_ac_nondet_split (current: symbol) env (x : var) (t : nf_term mset) : (Subst.t * (nf_term mset)) m = - ac_nondet_split current t - >> - (fun (t,res) -> - return ((Subst.add env x t), res) - ) - - (** See the term t as a given AC symbol. Unwrap the first constructor - if necessary *) - let get_AC (s : symbol) (t : nf_term) : (nf_term *int) list = - match t with - | TAC (s',l) when s' = s -> l - | TUnit u when is_unit units s u -> [] - | _ -> [t,1] - - (** See the term t as a given A symbol. Unwrap the first constructor - if necessary *) - let get_A (s : symbol) (t : nf_term) : nf_term list = - match t with - | TA (s',l) when s' = s -> l - | TUnit u when is_unit units s u -> [] - | _ -> [t] - - (** See the term [t] as an symbol [s]. Fail if it is not such - symbol. *) - let get_Sym s t = - match t with - | TSym (s',l) when s' = s -> return l - | _ -> fail () - - (*************) - (* A Removal *) - (*************) - - (** We remove the left factor v in a term list. This function runs - linearly with respect to the size of the first pattern symbol *) - - let left_factor current (v : nf_term) (t : nf_term list) = - let rec aux a b = - match a,b with - | t::q , t' :: q' when nf_equal t t' -> aux q q' - | [], q -> return q - | _, _ -> fail () - in - match v with - | TA (s,l) when s = current -> aux l t - | TUnit u when is_unit units current u -> return t - | _ -> - begin match t with - | [] -> fail () - | t::q -> - if nf_equal v t - then return q - else fail () - end - - - (**************) - (* AC Removal *) - (**************) - - (** {!pick_sym} gather all elements of a list that satisfies a - predicate, and combine them with the residual of the list. That - is, each element of the residual contains exactly one element less - than the original term. - - TODO : This function not as efficient as it could be, using a - proper data-structure *) - - let pick_sym (s : symbol) (t : nf_term mset ) = - let rec aux front back = - match back with - | [] -> fail () - | (t,tar)::q -> - begin match t with - | TSym (s',v') when s = s' -> - let back = - if tar > 1 - then (t,tar -1) ::q - else q - in - return (v' , List.rev_append front back ) - >>| aux ((t,tar)::front) q - | _ -> aux ((t,tar)::front) q - end - in - aux [] t - - - - (** We have to check if we are trying to remove a unit from a term. Could also be located in Terms*) - let is_unit_AC s t = - try nf_equal t (mk_TAC s []) - with | NoUnit -> false - - let is_same_AC s t : nf_term mset option= - match t with - TAC (s',l) when s = s' -> Some l - | _ -> None - - (** We want to remove the term [v] from the term list [t] under an AC - symbol *) - let single_AC_factor (s : symbol) (v : nf_term) v_ar (t : nf_term mset) : (nf_term mset) m = - let rec aux front back = - match back with - | [] -> fail () - | (t,tar)::q -> - begin - if nf_equal v t - then - match () with - | _ when tar < v_ar -> fail () - | _ when tar = v_ar -> return (List.rev_append front q) - | _ -> return (List.rev_append front ((t,tar-v_ar)::q)) - else - aux ((t,tar) :: front) q - end - in - if is_unit_AC s v - then - return t - else - aux [] t - - (* Remove a constant from a mset. If this constant is also a mset for - the same symbol, we remove every elements, one at a time (and we do - care of the arities) *) - let factor_AC (s : symbol) (v: nf_term) (t : nf_term mset) : ( nf_term mset ) m = - match is_same_AC s v with - | None -> single_AC_factor s v 1 t - | Some l -> - (* We are trying to remove an AC factor *) - List.fold_left (fun acc (v,v_ar) -> - acc >> (single_AC_factor s v v_ar) - ) - (return t) - l - - -(** [tri_fold f l acc] folds on the list [l] and give to f the - beginning of the list in reverse order, the considered element, and - the last part of the list - - as an exemple, on the list [1;2;3;4], we get the trace - f () [] 1 [2; 3; 4] - f () [1] 2 [3; 4] - f () [2;1] 3 [ 4] - f () [3;2;1] 4 [] - - it is the duty of the user to reverse the front if needed -*) - -let tri_fold f (l : 'a list) (acc : 'b)= match l with - [] -> acc - | _ -> - let _,_,acc = List.fold_left (fun acc (t : 'a) -> - let l,r,acc = acc in - let r = List.tl r in - t::l,r,f acc l t r - ) ([], l,acc) l - in acc - -(* let test = tri_fold (fun acc l t r -> (l,t,r) :: acc) [1;2;3;4] [] *) - - - - (*****************************) - (* ENUMERATION DES POSITIONS *) - (*****************************) - - -(** The pattern is a unit: we need to try to make it appear at each - position. We do not need to go further with a real matching, since - the match should be trivial. Hence, we proceed recursively to - enumerate all the positions. *) - -module Positions = struct - - - let ac (l: 'a mset) : ('a mset * 'a )m = - let rec aux = function - | [] -> assert false - | [t,1] -> return ([],t) - | [t,tar] -> return ([t,tar -1],t) - | (t,tar) as h :: q -> - (aux q >> (fun (c,x) -> return (h :: c,x))) - >>| (if tar > 1 then return ((t,tar-1) :: q,t) else return (q,t)) - in - aux l - - let ac' current (l: 'a mset) : ('a mset * 'a )m = - ac_nondet_split_raw l >> - (fun (l,r) -> - if l = [] || r = [] - then fail () - else - mk_TAC' current r >> - fun t -> return (l, t) - ) - - let a (l : 'a list) : ('a list * 'a * 'a list) m = - let rec aux left right : ('a list * 'a * 'a list) m = - match right with - | [] -> assert false - | [t] -> return (left,t,[]) - | t::q -> - aux (left@[t]) q - >>| return (left,t,q) - in - aux [] l -end - -let build_ac (current : symbol) (context : nf_term mset) (p : t) : t m= - if context = [] - then return p - else - mk_TAC' current context >> - fun t -> return (Plus (current,t_of_term t,p)) - -let build_a (current : symbol) - (left : nf_term list) (right : nf_term list) (p : t) : t m= - let right_pat p = - if right = [] - then return p - else - mk_TA' current right >> - fun t -> return (Dot (current,p,t_of_term t)) - in - let left_pat p= - if left = [] - then return p - else - mk_TA' current left >> - fun t -> return (Dot (current,t_of_term t,p)) - in - right_pat p >> left_pat >> (fun p -> return p) - - -let conts (hole : t) (l : symbol list) p : t m = - let p = t_of_term p in - (* - aller chercher les symboles ac et les symboles a - - construire pour chaque - * * + - / \ / \ / \ - 1 p p 1 p 1 - *) - let ac,a = List.partition (fun s -> List.assoc s is_ac) l in - let acc = fail () in - let acc = List.fold_left - (fun acc s -> - acc >>| return (Plus (s,p,hole)) - ) acc ac in - let acc = - List.fold_left - (fun acc s -> - acc >>| return (Dot (s,p,hole)) >>| return (Dot (s,hole,p)) - ) acc a - in acc - - -(** - Return the same thing as subterm : - - The size of the context - - The context - - A collection of substitutions (here == return Subst.empty) -*) -let unit_subterm (t : nf_term) (unit : symbol) (hole : t): (int * t * Subst.t m) m = - let symbols = List.fold_left - (fun acc (ac,u) -> if u = unit then ac :: acc else acc ) [] units - in - (* make a unit appear at each strict sub-position of the term*) - let rec positions (t : nf_term) : t m = - match t with - (* with a final unit at the end *) - | TAC (s,l) -> - let symbols' = List.filter (fun x -> x <> s) symbols in - ( - ac_nondet_split_raw l >> - (fun (l,r) -> if l = [] || r = [] then fail () else - ( - match r with - | [p,1] -> - positions p >>| conts hole symbols' p - | _ -> - mk_TAC' s r >> conts hole symbols' - ) >> build_ac s l )) - | TA (s,l) -> - let symbols' = List.filter (fun x -> x <> s) symbols in - ( - (* first the other symbols, and then the more simple case of - this particular symbol *) - a_nondet_middle l >> - (fun (l,m,r) -> - (* meant to break the symmetry *) - if (l = [] && r = []) - then fail () - else - ( - match m with - | [p] -> - positions p >>| conts hole symbols' p - | _ -> - mk_TA' s m >> conts hole symbols' - ) >> build_a s l r )) - >>| - ( - if List.mem s symbols then - begin match l with - | [a] -> assert false - | [a;b] -> build_a s [a] [b] (hole) - | _ -> - (* on ne construit que les elements interieurs, - d'ou la disymetrie *) - (Positions.a l >> - (fun (left,p,right) -> - if left = [] then fail () else - (build_a s left right (Dot (s,hole,t_of_term p))))) - end - else fail () - ) - - | TSym (s,l) -> - tri_fold (fun acc l t r -> - ((positions t) >> - (fun (p) -> - let l = List.map t_of_term l in - let r = List.map t_of_term r in - return (Sym (s, Array.of_list (List.rev_append l (p::r)))) )) - >>| - ( - conts hole symbols t >> - (fun (p) -> - let l = List.map t_of_term l in - let r = List.map t_of_term r in - return (Sym (s, Array.of_list (List.rev_append l (p::r)))) ) - ) - >>| acc - ) l (fail()) - | TVar x -> assert false - | TUnit x when x = unit -> return (hole) - | TUnit x as t -> conts hole symbols t - in - (positions t - >>| - (match t with - | TSym _ -> conts hole symbols t - | TAC (s,l) -> conts hole symbols t - | TA (s,l) -> conts hole symbols t - | _ -> fail()) - ) - >> fun (p) -> return (Terms.size p,p,return Subst.empty) - - - - - (************) - (* Matching *) - (************) - - - -(** {!matching} is the generic matching judgement. Each time a - non-deterministic split is made, we have to come back to this one. - - {!matchingSym} is used to match two applications that have the - same (free) head-symbol. - - {!matchingAC} is used to match two sums (with the subtlety that - [x+y] matches [f a] which is a function application or [a*b] which - is a product). - - {!matchingA} is used to match two products (with the subtlety that - [x*y] matches [f a] which is a function application, or [a+b] - which is a sum). - - -*) - -let matching : Subst.t -> nf_term -> nf_term -> Subst.t Search.m= - let rec matching env (p : nf_term) (t: nf_term) : Subst.t Search.m= - match p with - | TAC (s,l) -> - let l = linear l in - matchingAC env s l (get_AC s t) - | TA (s,l) -> - matchingA env s l (get_A s t) - | TSym (s,l) -> - (get_Sym s t) - >> (fun t -> matchingSym env l t) - | TVar x -> - begin match Subst.find env x with - | None -> return (Subst.add env x t) - | Some v -> if nf_equal v t then return env else fail () - end - | TUnit s -> - if nf_equal p t then return env else fail () - and - matchingAC (env : Subst.t) (current : symbol) (l : nf_term list) (t : (nf_term *int) list) = - match l with - | TSym (s,v):: q -> - pick_sym s t - >> (fun (v',t') -> - matchingSym env v v' - >> (fun env -> matchingAC env current q t')) - - | TAC (s,v)::q when s = current -> - assert false - | TVar x:: q -> (* This is an optimization *) - begin match Subst.find env x with - | None -> - (var_ac_nondet_split current env x t) - >> (fun (env,residual) -> matchingAC env current q residual) - | Some v -> - (factor_AC current v t) - >> (fun residual -> matchingAC env current q residual) - end - | TUnit s as v :: q -> (* this is an optimization *) - (factor_AC current v t) >> - (fun residual -> matchingAC env current q residual) - | h :: q ->(* PAC =/= curent or PA or unit for this symbol*) - (ac_nondet_split current t) - >> - (fun (t,right) -> - matching env h t - >> - ( - fun env -> - matchingAC env current q right - ) - ) - | [] -> if t = [] then return env else fail () - and - matchingA (env : Subst.t) (current : symbol) (l : nf_term list) (t : nf_term list) = - match l with - | TSym (s,v) :: l -> - begin match t with - | TSym (s',v') :: r when s = s' -> - (matchingSym env v v') - >> (fun env -> matchingA env current l r) - | _ -> fail () - end - | TA (s,v) :: l when s = current -> - assert false - | TVar x :: l -> - begin match Subst.find env x with - | None -> - debug (Printf.sprintf "var %i (%s)" x - (let b = Buffer.create 21 in List.iter (fun t -> Buffer.add_string b ( Terms.sprint_nf_term t)) t; Buffer.contents b )); - var_a_nondet_split env current x t - >> (fun (env,residual)-> debug (Printf.sprintf "pl %i %i" x(List.length residual)); matchingA env current l residual) - | Some v -> - (left_factor current v t) - >> (fun residual -> matchingA env current l residual) - end - | TUnit s as v :: q -> (* this is an optimization *) - (left_factor current v t) >> - (fun residual -> matchingA env current q residual) - | h :: l -> - a_nondet_split current t - >> (fun (t,r) -> - matching env h t - >> (fun env -> matchingA env current l r) - ) - | [] -> if t = [] then return env else fail () - and - matchingSym (env : Subst.t) (l : nf_term list) (t : nf_term list) = - List.fold_left2 - (fun acc p t -> acc >> (fun env -> matching env p t)) - (return env) - l - t - - in - fun env l r -> - let _ = debug (Printf.sprintf "pattern :%s\nterm :%s\n%!" (Terms.sprint_nf_term l) (Terms.sprint_nf_term r)) in - let m = matching env l r in - let _ = debug (Printf.sprintf "count %i" (Search.count m)) in - m - - -(** [unitifiable p : Subst.t m] *) -let unitifiable p : (symbol * Subst.t m) m = - let m = List.fold_left - (fun acc (_,unit) -> acc >>| - let m = matching Subst.empty p (mk_TUnit unit) in - if Search.is_empty m then - fail () - else - begin - return (unit,m) - end - ) (fail ()) units - in - m -;; - -let nullifiable p = - let nullable = not strict in - let has_unit s = - try let _ = get_unit units s in true - with NoUnit -> false - in - let rec aux = function - | TA (s,l) -> has_unit s && List.for_all (aux) l - | TAC (s,l) -> has_unit s && List.for_all (fun (x,n) -> aux x) l - | TSym _ -> false - | TVar _ -> nullable - | TUnit _ -> true - in aux p - -let unit_warning p ~nullif ~unitif = - assert ((Search.is_empty unitif) || nullif); - if not (Search.is_empty unitif) - then - begin - Pp.msg_warning - (Pp.str - "[aac_tactics] This pattern can be instanciated to match units, some solutions can be missing"); - end - -;; - - - - -(***********) -(* Subterm *) -(***********) - - - -(** [subterm] solves a sub-term pattern matching. - - This function is more high-level than {!matcher}, thus takes {!t} - as arguments rather than terms in normal form {!nf_term}. - - We use three mutually recursive functions {!subterm}, - {!subterm_AC}, {!subterm_A} to find the matching subterm, making - non-deterministic choices to split the term into a context and an - intersting sub-term. Intuitively, the only case in which we have to - go in depth is when we are left with a sub-term that is atomic. - - Indeed, rewriting [H: b = c |- a+b+a = a+a+c], we do not want to - find recursively the sub-terms of [a+b] and [b+a], since they will - overlap with the sub-terms of [a+b+a]. - - We rebuild the context on the fly, leaving the variables in the - pattern uninstantiated. We do so in order to allow interaction - with the user, to choose the env. - - Strange patterms like x*y*x can be instanciated by nothing, inside - a product. Therefore, we need to check that all the term is not - going into the context. With proper support for interaction with - the user, we should lift these tests. However, at the moment, they - serve as heuristics to return "interesting" matchings -*) - - let return_non_empty raw_p m = - if is_empty m - then - fail () - else - return (raw_p ,m) - - let subterm (raw_p:t) (raw_t:t): (int * t * Subst.t m) m= - let _ = debug (String.make 40 '=') in - let p = term_of_t units raw_p in - let t = term_of_t units raw_t in - let nullif = nullifiable p in - let unitif = unitifiable p in - let _ = unit_warning p ~nullif ~unitif in - let _ = debug (Printf.sprintf "%s" (Terms.sprint_nf_term p)) in - let _ = debug (Printf.sprintf "%s" (Terms.sprint_nf_term t)) in - let filter_right current right (p,m) = - if right = [] - then return (p,m) - else - mk_TAC' current right >> - fun t -> return (Plus (current,p,t_of_term t),m) - in - let filter_middle current left right (p,m) = - let right_pat p = - if right = [] - then return p - else - mk_TA' current right >> - fun t -> return (Dot (current,p,t_of_term t)) - in - let left_pat p= - if left = [] - then return p - else - mk_TA' current left >> - fun t -> return (Dot (current,t_of_term t,p)) - in - right_pat p >> left_pat >> (fun p -> return (p,m)) - in - let rec subterm (t:nf_term) : (t * Subst.t m) m= - match t with - | TAC (s,l) -> - ((ac_nondet_split_raw l) >> - (fun (left,right) -> - (subterm_AC s left) >> (filter_right s right) - )) - | TA (s,l) -> - (a_nondet_middle l) >> - (fun (left, middle, right) -> - (subterm_A s middle) >> - (filter_middle s left right) - ) - | TSym (s, l) -> - let init = - return_non_empty raw_p (matching Subst.empty p t) - in - tri_fold (fun acc l t r -> - ((subterm t) >> - (fun (p,m) -> - let l = List.map t_of_term l in - let r = List.map t_of_term r in - let p = Sym (s, Array.of_list (List.rev_append l (p::r))) in - return (p,m) - )) >>| acc - ) l init - | TVar x -> assert false - (* this case is superseded by the later disjunction *) - | TUnit s -> fail () - - and subterm_AC s tl = - match tl with - [x,1] -> subterm x - | _ -> - mk_TAC' s tl >> fun t -> - return_non_empty raw_p (matching Subst.empty p t) - and subterm_A s tl = - match tl with - [x] -> subterm x - | _ -> - mk_TA' s tl >> - fun t -> - return_non_empty raw_p (matching Subst.empty p t) - in - match p with - | TUnit unit -> unit_subterm t unit raw_p - | _ when not (Search.is_empty unitif) -> - let unit_matches = - Search.fold - (fun (unit,inst) acc -> - Search.fold - (fun subst acc' -> - let m = unit_subterm t unit (Subst.instantiate subst raw_p) - in - m>>| acc' - ) - inst - acc - ) - unitif - (fail ()) - in - let nullifies (t : Subst.t) = - List.for_all (fun (_,x) -> - List.exists (fun (_,y) -> Unit y = x ) units - ) (Subst.to_list t) - in - let nonunit_matches = - subterm t >> - ( - fun (p,m) -> - let m = Search.filter (fun subst -> not( nullifies subst)) m in - if Search.is_empty m - then fail () - else return (Terms.size p,p,m) - ) - in - unit_matches >>| nonunit_matches - - | _ -> (subterm t >> fun (p,m) -> return (Terms.size p,p,m)) - - - end - - -(* The functions we export, handlers for the previous ones. Some debug - information also *) -let subterm ?(strict = false) units raw t = - let module M = M (struct - let is_ac = units.is_ac - let units = units.unit_for - let strict = strict - end) in - let sols = time (M.subterm raw) t "%fs spent in subterm (including matching)\n" in - debug - (Printf.sprintf "%i possible solution(s)\n" - (Search.fold (fun (_,_,envm) acc -> count envm + acc) sols 0)); - sols - - -let matcher ?(strict = false) units p t = - let module M = M (struct - let is_ac = units.is_ac - let units = units.unit_for - let strict = false - end) in - let units = units.unit_for in - let sols = time - (fun (p,t) -> - let p = (Terms.term_of_t units p) in - let t = (Terms.term_of_t units t) in - M.matching Subst.empty p t) (p,t) - "%fs spent in the matcher\n" - in - debug (Printf.sprintf "%i solutions\n" (count sols)); - sols - diff --git a/AAC_matcher.mli b/AAC_matcher.mli deleted file mode 100644 index 896a2a9..0000000 --- a/AAC_matcher.mli +++ /dev/null @@ -1,189 +0,0 @@ -(***************************************************************************) -(* This is part of aac_tactics, it is distributed under the terms of the *) -(* GNU Lesser General Public License version 3 *) -(* (see file LICENSE for more details) *) -(* *) -(* Copyright 2009-2010: Thomas Braibant, Damien Pous. *) -(***************************************************************************) - -(** Standalone module containing the algorithm for matching modulo - associativity and associativity and commutativity - (AAC). Additionnaly, some A or AC operators can have units (U). - - This module could be reused outside of the Coq plugin. - - Matching a pattern [p] against a term [t] modulo AACU boils down - to finding a substitution [env] such that the pattern [p] - instantiated with [env] is equal to [t] modulo AACU. - - We proceed by structural decomposition of the pattern, trying all - possible non-deterministic splittings of the subject, when needed. The - function {!matcher} is limited to top-level matching, that is, the - subject must make a perfect match against the pattern ([x+x] does - not match [a+a+b] ). - - We use a search monad {!AAC_search_monad} to perform non-deterministic - choices in an almost transparent way. - - We also provide a function {!subterm} for finding a match that is - a subterm of the subject modulo AACU. In particular, this function - gives a solution to the aforementioned case ([x+x] against - [a+b+a]). - - On a slightly more involved level : - - it must be noted that we allow several AC/A operators to share - the same units, but that a given AC/A operator can have at most - one unit. - - - if the pattern does not contain "hard" symbols (like constants, - function symbols, AC or A symbols without units), there can be - infinitely many subterms such that the pattern matches: it is - possible to build "subterms" modulo AAC and U that make the size - of the term increase (by making neutral elements appear in a - layered fashion). Hence, in this case, a warning is issued, and - some solutions are omitted. - -*) - -(** {2 Utility functions} *) - -type symbol = int -type var = int - -(** Relationship between units and operators. This is a sparse - representation of a matrix of couples [(op,unit)] where [op] is - the index of the operation, and [unit] the index of the relevant - unit. We make the assumption that any operation has 0 or 1 unit, - and that operations can share a unit). *) - -type units =(symbol * symbol) list (* from AC/A symbols to the unit *) -type ext_units = - { - unit_for : units; (* from AC/A symbols to the unit *) - is_ac : (symbol * bool) list - } - - -(** The arguments of sums (or AC operators) are represented using finite multisets. - (Typically, [a+b+a] corresponds to [2.a+b], i.e. [Sum[a,2;b,1]]) *) -type 'a mset = ('a * int) list - -(** [linear] expands a multiset into a simple list *) -val linear : 'a mset -> 'a list - -(** Representations of expressions - - The module {!Terms} defines two different types for expressions. - - a public type {!Terms.t} that represents abstract syntax trees - of expressions with binary associative and commutative operators - - a private type {!Terms.nf_term}, corresponding to a canonical - representation for the above terms modulo AACU. The construction - functions on this type ensure that these terms are in normal form - (that is, no sum can appear as a subterm of the same sum, no - trailing units, lists corresponding to multisets are sorted, - etc...). - -*) -module Terms : -sig - - (** {2 Abstract syntax tree of terms and patterns} - - We represent both terms and patterns using the following datatype. - - Values of type [symbol] are used to index symbols. Typically, - given two associative operations [(^)] and [( * )], and two - morphisms [f] and [g], the term [f (a^b) (a*g b)] is represented - by the following value - [Sym(0,[| Dot(1, Sym(2,[||]), Sym(3,[||])); - Dot(4, Sym(2,[||]), Sym(5,[|Sym(3,[||])|])) |])] - where the implicit symbol environment associates - [f] to [0], [(^)] to [1], [a] to [2], [b] to [3], [( * )] to [4], and [g] to [5], - - Accordingly, the following value, that contains "variables" - [Sym(0,[| Dot(1, Var x, Unit (1); Dot(4, Var x, - Sym(5,[|Sym(3,[||])|])) |])] represents the pattern [forall x, f - (x^1) (x*g b)]. The relationship between [1] and [( * )] is only - mentionned in the units table. *) - - type t = - Dot of (symbol * t * t) - | Plus of (symbol * t * t) - | Sym of (symbol * t array) - | Var of var - | Unit of symbol - - (** Test for equality of terms modulo AACU (relies on the following - canonical representation of terms). Note than two different - units of a same operator are not considered equal. *) - val equal_aac : units -> t -> t -> bool - - - (** {2 Normalised terms (canonical representation) } - - A term in normal form is the canonical representative of the - equivalence class of all the terms that are equal modulo AACU. - This representation is only used internally; it is exported here - for the sake of completeness *) - - type nf_term - - (** {3 Comparisons} *) - - val nf_term_compare : nf_term -> nf_term -> int - val nf_equal : nf_term -> nf_term -> bool - - (** {3 Printing function} *) - - val sprint_nf_term : nf_term -> string - - (** {3 Conversion functions} *) - - (** we have the following property: [a] and [b] are equal modulo AACU - iif [nf_equal (term_of_t a) (term_of_t b) = true] *) - val term_of_t : units -> t -> nf_term - val t_of_term : nf_term -> t - -end - - -(** Substitutions (or environments) - - The module {!Subst} contains infrastructure to deal with - substitutions, i.e., functions from variables to terms. Only a - restricted subsets of these functions need to be exported. - - As expected, a particular substitution can be used to - instantiate a pattern. -*) -module Subst : -sig - type t - val sprint : t -> string - val instantiate : t -> Terms.t-> Terms.t - val to_list : t -> (var*Terms.t) list -end - - -(** {2 Main functions exported by this module} *) - -(** [matcher p t] computes the set of solutions to the given top-level - matching problem ([p] is the pattern, [t] is the term). If the - [strict] flag is set, solutions where units are used to - instantiate some variables are excluded, unless this unit appears - directly under a function symbol (e.g., f(x) still matches f(1), - while x+x+y does not match a+b+c, since this would require to - assign 1 to x). -*) -val matcher : ?strict:bool -> ext_units -> Terms.t -> Terms.t -> Subst.t AAC_search_monad.m - -(** [subterm p t] computes a set of solutions to the given - subterm-matching problem. - - Return a collection of possible solutions (each with the - associated depth, the context, and the solutions of the matching - problem). The context is actually a {!Terms.t} where the variables - are yet to be instantiated by one of the associated substitutions -*) -val subterm : ?strict:bool -> ext_units -> Terms.t -> Terms.t -> (int * Terms.t * Subst.t AAC_search_monad.m) AAC_search_monad.m - diff --git a/AAC_print.ml b/AAC_print.ml deleted file mode 100644 index 512efa3..0000000 --- a/AAC_print.ml +++ /dev/null @@ -1,100 +0,0 @@ -(***************************************************************************) -(* This is part of aac_tactics, it is distributed under the terms of the *) -(* GNU Lesser General Public License version 3 *) -(* (see file LICENSE for more details) *) -(* *) -(* Copyright 2009-2010: Thomas Braibant, Damien Pous. *) -(***************************************************************************) - -(* A very basic way to interact with the envs, to choose a possible - solution *) -open Pp -open AAC_matcher -type named_env = (Names.name * Terms.t) list - - - -(** {pp_env} prints a substitution mapping names to terms, using the -provided printer *) -let pp_env pt : named_env -> Pp.std_ppcmds = fun env -> - List.fold_left - (fun acc (v,t) -> - begin match v with - | Names.Name s -> str (Printf.sprintf "%s: " (Names.string_of_id s)) - | Names.Anonymous -> str ("_") - end - ++ pt t ++ str "; " ++ acc - ) - (str "") - env - -(** {pp_envm} prints a collection of possible environments, and number -them. This number must remain compatible with the parameters given to -{!aac_rewrite} *) -let pp_envm pt : named_env AAC_search_monad.m -> Pp.std_ppcmds = fun m -> - let _,s = - AAC_search_monad.fold - (fun env (n,acc) -> - n+1, h 0 (str (Printf.sprintf "%i:\t[" n) ++pp_env pt env ++ str "]") ++ fnl () :: acc - ) m (0,[]) - in - List.fold_left (fun acc s -> s ++ acc) (str "") (s) - -let trivial_substitution envm = - match AAC_search_monad.choose envm with - | None -> true (* assert false *) - | Some l -> l=[] - -(** {pp_all} prints a collection of possible contexts and related -possibles substitutions, giving a number to each. This number must -remain compatible with the parameters of {!aac_rewrite} *) -let pp_all pt : (int * Terms.t * named_env AAC_search_monad.m) AAC_search_monad.m -> Pp.std_ppcmds = fun m -> - let _,s = AAC_search_monad.fold - (fun (size,context,envm) (n,acc) -> - let s = str (Printf.sprintf "occurence %i: transitivity through " n) in - let s = s ++ pt context ++ str "\n" in - let s = if trivial_substitution envm then s else - s ++ str (Printf.sprintf "%i possible(s) substitution(s)" (AAC_search_monad.count envm) ) - ++ fnl () ++ pp_envm pt envm - in - n+1, s::acc - ) m (0,[]) in - List.fold_left (fun acc s -> s ++ str "\n" ++ acc) (str "") (s) - -(** The main printing function. {!print} uses the debruijn_env the -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 {!AAC_theory.Trans} module.*) -let print rlt ir m (context : Term.rel_context) goal = - if AAC_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 m = AAC_search_monad.(>>) m - (fun (i,t,envm) -> - let envm = AAC_search_monad.(>>) envm ( fun env -> - let l = AAC_matcher.Subst.to_list env in - let l = List.sort (fun (n,_) (n',_) -> Pervasives.compare n n') l in - let l = - List.map (fun (v,t) -> - let (name,body,types) = Term.lookup_rel v context in - (name,t) - ) l - in - AAC_search_monad.return l - ) - in - AAC_search_monad.return (i,t,envm) - ) - in - let m = AAC_search_monad.sort (fun (x,_,_) (y,_,_) -> x - y) m in - let _ = Pp.msgnl - (pp_all - (fun t -> Printer.pr_constr (AAC_theory.Trans.raw_constr_of_t ir rlt context t) ) m - ) - in - Tacticals.tclIDTAC goal - diff --git a/AAC_print.mli b/AAC_print.mli deleted file mode 100644 index bacd806..0000000 --- a/AAC_print.mli +++ /dev/null @@ -1,23 +0,0 @@ -(***************************************************************************) -(* This is part of aac_tactics, it is distributed under the terms of the *) -(* GNU Lesser General Public License version 3 *) -(* (see file LICENSE for more details) *) -(* *) -(* Copyright 2009-2010: Thomas Braibant, Damien Pous. *) -(***************************************************************************) - -(** Pretty printing functions we use for the aac_instances - tactic. *) - - -(** The main printing function. {!print} uses the [Term.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 {!AAC_theory.Trans} module.*) -val print : - AAC_coq.Relation.t -> - AAC_theory.Trans.ir -> - (int * AAC_matcher.Terms.t * AAC_matcher.Subst.t AAC_search_monad.m) AAC_search_monad.m -> - Term.rel_context -> - Proof_type.tactic - diff --git a/AAC_rewrite.ml b/AAC_rewrite.ml deleted file mode 100644 index be286f9..0000000 --- a/AAC_rewrite.ml +++ /dev/null @@ -1,524 +0,0 @@ -(***************************************************************************) -(* This is part of aac_tactics, it is distributed under the terms of the *) -(* GNU Lesser General Public License version 3 *) -(* (see file LICENSE for more details) *) -(* *) -(* Copyright 2009-2010: Thomas Braibant, Damien Pous. *) -(***************************************************************************) - -(** aac_rewrite -- rewriting modulo *) - - -module Control = struct - let debug = false - let printing = false - let time = false -end - -module Debug = AAC_helper.Debug (Control) -open Debug - -let time_tac msg tac = - if Control.time then AAC_coq.tclTIME msg tac else tac - -let tac_or_exn tac exn msg = fun gl -> - try tac gl with e -> - pr_constr "last goal" (Tacmach.pf_concl gl); - exn msg e - -(* 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 - | Util.Anomaly _ as e -> raise e - | _ -> AAC_coq.anomaly msg - -module M = AAC_matcher - -open Term -open Names -open Coqlib -open Proof_type - -(** The various kind of relation we can encounter, as a hierarchy *) -type rew_relation = - | Bare of AAC_coq.Relation.t - | Transitive of AAC_coq.Transitive.t - | Equivalence of AAC_coq.Equivalence.t - -(** {!promote try to go higher in the aforementionned hierarchy} *) -let promote (rlt : AAC_coq.Relation.t) (k : rew_relation -> Proof_type.tactic) = - try AAC_coq.Equivalence.cps_from_relation rlt - (fun e -> k (Equivalence e)) - with - | Not_found -> - begin - try AAC_coq.Transitive.cps_from_relation rlt - (fun trans -> k (Transitive trans)) - with - |Not_found -> k (Bare rlt) - end - - -(* - Various situations: - p == q |- left == right : rewrite <- -> - p <= q |- left <= right : rewrite -> - p <= q |- left == right : failure - p == q |- left <= right : rewrite <- -> - - Not handled - p <= q |- left >= right : failure -*) - -(** aac_lift : the ideal type beyond AAC.v/AAC_lift - - A base relation r, together with an equivalence relation, and the - proof that the former lifts to the later. Howver, we have to - ensure manually the invariant : r.carrier == e.carrier, and that - lift connects the two things *) -type aac_lift = - { - r : AAC_coq.Relation.t; - e : AAC_coq.Equivalence.t; - lift : Term.constr - } - -type rewinfo = - { - hypinfo : AAC_coq.Rewrite.hypinfo; - - in_left : bool; (** are we rewriting in the left hand-sie of the goal *) - pattern : constr; - subject : constr; - morph_rlt : AAC_coq.Relation.t; (** the relation we look for in morphism *) - eqt : AAC_coq.Equivalence.t; (** the equivalence we use as workbase *) - rlt : AAC_coq.Relation.t; (** the relation in the goal *) - lifting: aac_lift - } - -let infer_lifting (rlt: AAC_coq.Relation.t) (k : lift:aac_lift -> Proof_type.tactic) : Proof_type.tactic = - AAC_coq.cps_evar_relation rlt.AAC_coq.Relation.carrier (fun e -> - let lift_ty = - mkApp (Lazy.force AAC_theory.Stubs.lift, - [| - rlt.AAC_coq.Relation.carrier; - rlt.AAC_coq.Relation.r; - e - |] - ) in - AAC_coq.cps_resolve_one_typeclass ~error:"Cannot infer a lifting" - lift_ty (fun lift goal -> - let x = rlt.AAC_coq.Relation.carrier in - let r = rlt.AAC_coq.Relation.r in - let eq = (AAC_coq.nf_evar goal e) in - let equiv = AAC_coq.lapp AAC_theory.Stubs.lift_proj_equivalence [| x;r;eq; lift |] in - let lift = - { - r = rlt; - e = AAC_coq.Equivalence.make x eq equiv; - lift = lift; - } - in - k ~lift:lift goal - )) - -(** Builds a rewinfo, once and for all *) -let dispatch in_left (left,right,rlt) hypinfo (k: rewinfo -> Proof_type.tactic ) : Proof_type.tactic= - let l2r = hypinfo.AAC_coq.Rewrite.l2r in - infer_lifting rlt - (fun ~lift -> - let eq = lift.e in - k { - hypinfo = hypinfo; - in_left = in_left; - pattern = if l2r then hypinfo.AAC_coq.Rewrite.left else hypinfo.AAC_coq.Rewrite.right; - subject = if in_left then left else right; - morph_rlt = AAC_coq.Equivalence.to_relation eq; - eqt = eq; - lifting = lift; - rlt = rlt - } - ) - - - -(** {1 Tactics} *) - - -(** Build the reifiers, the reified terms, and the evaluation fonction *) -let handle eqt zero envs (t : AAC_matcher.Terms.t) (t' : AAC_matcher.Terms.t) k = - - let (x,r,_) = AAC_coq.Equivalence.split eqt in - AAC_theory.Trans.mk_reifier (AAC_coq.Equivalence.to_relation eqt) zero envs - (fun (maps, reifier) -> - (* fold through a term and reify *) - let t = AAC_theory.Trans.reif_constr_of_t reifier t in - let t' = AAC_theory.Trans.reif_constr_of_t reifier t' in - (* Some letins *) - let eval = (mkApp (Lazy.force AAC_theory.Stubs.eval, [|x;r; maps.AAC_theory.Trans.env_sym; maps.AAC_theory.Trans.env_bin; maps.AAC_theory.Trans.env_units|])) in - - AAC_coq.cps_mk_letin "eval" eval (fun eval -> - AAC_coq.cps_mk_letin "left" t (fun t -> - AAC_coq.cps_mk_letin "right" t' (fun t' -> - k maps eval t t')))) - -(** [by_aac_reflexivity] is a sub-tactic that closes a sub-goal that - is merely a proof of equality of two terms modulo AAC *) -let by_aac_reflexivity zero - eqt envs (t : AAC_matcher.Terms.t) (t' : AAC_matcher.Terms.t) : Proof_type.tactic = - handle eqt zero envs t t' - (fun maps eval t t' -> - let (x,r,e) = AAC_coq.Equivalence.split eqt in - let decision_thm = AAC_coq.lapp AAC_theory.Stubs.decide_thm - [|x;r;e; - maps.AAC_theory.Trans.env_sym; - maps.AAC_theory.Trans.env_bin; - maps.AAC_theory.Trans.env_units; - t;t'; - |] - in - (* This convert is required to deal with evars in a proper - way *) - let convert_to = mkApp (r, [| mkApp (eval,[| t |]); mkApp (eval, [|t'|])|]) in - let convert = Tactics.convert_concl convert_to Term.VMcast in - let apply_tac = Tactics.apply decision_thm in - (Tacticals.tclTHENLIST - [ - convert ; - tac_or_exn apply_tac AAC_coq.user_error "unification failure"; - tac_or_exn (time_tac "vm_norm" (Tactics.normalise_in_concl)) AAC_coq.anomaly "vm_compute failure"; - Tacticals.tclORELSE Tactics.reflexivity - (Tacticals.tclFAIL 0 (Pp.str "Not an equality modulo A/AC")) - ]) - ) - -let by_aac_normalise zero lift ir t t' = - let eqt = lift.e in - let rlt = lift.r in - handle eqt zero ir t t' - (fun maps eval t t' -> - let (x,r,e) = AAC_coq.Equivalence.split eqt in - let normalise_thm = AAC_coq.lapp AAC_theory.Stubs.lift_normalise_thm - [|x;r;e; - maps.AAC_theory.Trans.env_sym; - maps.AAC_theory.Trans.env_bin; - maps.AAC_theory.Trans.env_units; - rlt.AAC_coq.Relation.r; - lift.lift; - t;t'; - |] - in - (* This convert is required to deal with evars in a proper - way *) - let convert_to = mkApp (rlt.AAC_coq.Relation.r, [| mkApp (eval,[| t |]); mkApp (eval, [|t'|])|]) in - let convert = Tactics.convert_concl convert_to Term.VMcast in - let apply_tac = Tactics.apply normalise_thm in - (Tacticals.tclTHENLIST - [ - convert ; - apply_tac; - ]) - - ) - -(** A handler tactic, that reifies the goal, and infer the liftings, - and then call its continuation *) -let aac_conclude - (k : Term.constr -> aac_lift -> AAC_theory.Trans.ir -> AAC_matcher.Terms.t -> AAC_matcher.Terms.t -> Proof_type.tactic) = fun goal -> - - let (equation : Term.types) = Tacmach.pf_concl goal in - let envs = AAC_theory.Trans.empty_envs () in - let left, right,r = - match AAC_coq.match_as_equation goal equation with - | None -> AAC_coq.user_error "The goal is not an applied relation" - | Some x -> x in - try infer_lifting r - (fun ~lift goal -> - let eq = AAC_coq.Equivalence.to_relation lift.e in - let tleft,tright, goal = AAC_theory.Trans.t_of_constr goal eq envs (left,right) in - let goal, ir = AAC_theory.Trans.ir_of_envs goal eq envs in - let concl = Tacmach.pf_concl goal in - let _ = pr_constr "concl "concl in - let evar_map = Tacmach.project goal in - Tacticals.tclTHEN - (Refiner.tclEVARS evar_map) - (k left lift ir tleft tright) - goal - )goal - with - | Not_found -> AAC_coq.user_error "No lifting from the goal's relation to an equivalence" - -open Libnames -open Tacinterp - -let aac_normalise = fun goal -> - let ids = Tacmach.pf_ids_of_hyps goal in - Tacticals.tclTHENLIST - [ - aac_conclude by_aac_normalise; - 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 - >> - ); - Tactics.keep ids - ] goal - -let aac_reflexivity = fun goal -> - aac_conclude - (fun zero lift ir t t' -> - let x,r = AAC_coq.Relation.split (lift.r) in - let r_reflexive = (AAC_coq.Classes.mk_reflexive x r) in - AAC_coq.cps_resolve_one_typeclass ~error:"The goal's relation is not reflexive" - r_reflexive - (fun reflexive -> - let lift_reflexivity = - mkApp (Lazy.force (AAC_theory.Stubs.lift_reflexivity), - [| - x; - r; - lift.e.AAC_coq.Equivalence.eq; - lift.lift; - reflexive - |]) - in - Tacticals.tclTHEN - (Tactics.apply lift_reflexivity) - (fun goal -> - let concl = Tacmach.pf_concl goal in - let _ = pr_constr "concl "concl in - by_aac_reflexivity zero lift.e ir t t' goal) - ) - ) goal - -(** A sub-tactic to lift the rewriting using AAC_lift *) -let lift_transitivity in_left (step:constr) preorder lifting (using_eq : AAC_coq.Equivalence.t): tactic = - fun goal -> - (* catch the equation and the two members*) - let concl = Tacmach.pf_concl goal in - let (left, right, _ ) = match AAC_coq.match_as_equation goal concl with - | Some x -> x - | None -> AAC_coq.user_error "The goal is not an equation" - in - let lift_transitivity = - let thm = - if in_left - then - Lazy.force AAC_theory.Stubs.lift_transitivity_left - else - Lazy.force AAC_theory.Stubs.lift_transitivity_right - in - mkApp (thm, - [| - preorder.AAC_coq.Relation.carrier; - preorder.AAC_coq.Relation.r; - using_eq.AAC_coq.Equivalence.eq; - lifting; - step; - left; - right; - |]) - in - Tacticals.tclTHENLIST - [ - Tactics.apply lift_transitivity - ] goal - - -(** The core tactic for aac_rewrite *) -let core_aac_rewrite ?abort - rewinfo - subst - (by_aac_reflexivity : AAC_matcher.Terms.t -> AAC_matcher.Terms.t -> Proof_type.tactic) - (tr : constr) t left : tactic = - pr_constr "transitivity through" tr; - let tran_tac = - lift_transitivity rewinfo.in_left tr rewinfo.rlt rewinfo.lifting.lift rewinfo.eqt - in - AAC_coq.Rewrite.rewrite ?abort rewinfo.hypinfo subst (fun rew -> - Tacticals.tclTHENSV - (tac_or_exn (tran_tac) AAC_coq.anomaly "Unable to make the transitivity step") - ( - if rewinfo.in_left - then [| by_aac_reflexivity left t ; rew |] - else [| by_aac_reflexivity t left ; rew |] - ) - ) - -exception NoSolutions - - -(** Choose a substitution from a - [(int * Terms.t * Env.env AAC_search_monad.m) AAC_search_monad.m ] *) -(* WARNING: Beware, since the printing function can change the order of the - printed monad, this function has to be updated accordingly *) -let choose_subst subterm sol m= - try - let (depth,pat,envm) = match subterm with - | None -> (* first solution *) - List.nth ( List.rev (AAC_search_monad.to_list m)) 0 - | Some x -> - List.nth ( List.rev (AAC_search_monad.to_list m)) x - in - let env = match sol with - None -> - List.nth ( (AAC_search_monad.to_list envm)) 0 - | Some x -> List.nth ( (AAC_search_monad.to_list envm)) x - in - pat, env - with - | _ -> raise NoSolutions - -(** rewrite the constr modulo AC from left to right in the left member - of the goal *) -let aac_rewrite ?abort rew ?(l2r=true) ?(show = false) ?(in_left=true) ?strict ~occ_subterm ~occ_sol ?extra : Proof_type.tactic = fun goal -> - let envs = AAC_theory.Trans.empty_envs () in - let (concl : Term.types) = Tacmach.pf_concl goal in - let (_,_,rlt) as concl = - match AAC_coq.match_as_equation goal concl with - | None -> AAC_coq.user_error "The goal is not an applied relation" - | Some (left, right, rlt) -> left,right,rlt - in - let check_type x = - Tacmach.pf_conv_x goal x rlt.AAC_coq.Relation.carrier - in - AAC_coq.Rewrite.get_hypinfo rew ~l2r ?check_type:(Some check_type) - (fun hypinfo -> - dispatch in_left concl hypinfo - ( - fun rewinfo -> - let goal = - match extra with - | Some t -> AAC_theory.Trans.add_symbol goal rewinfo.morph_rlt envs t - | None -> goal - in - let pattern, subject, goal = - AAC_theory.Trans.t_of_constr goal rewinfo.morph_rlt envs - (rewinfo.pattern , rewinfo.subject) - in - let goal, ir = AAC_theory.Trans.ir_of_envs goal rewinfo.morph_rlt envs in - - let units = AAC_theory.Trans.ir_to_units ir in - let m = AAC_matcher.subterm ?strict units pattern subject in - (* We sort the monad in increasing size of contet *) - let m = AAC_search_monad.sort (fun (x,_,_) (y,_,_) -> x - y) m in - - if show - then - AAC_print.print rewinfo.morph_rlt ir m (hypinfo.AAC_coq.Rewrite.context) - - else - try - let pat,subst = choose_subst occ_subterm occ_sol m in - let tr_step = AAC_matcher.Subst.instantiate subst pat in - let tr_step_raw = AAC_theory.Trans.raw_constr_of_t ir rewinfo.morph_rlt [] tr_step in - - let conv = (AAC_theory.Trans.raw_constr_of_t ir rewinfo.morph_rlt (hypinfo.AAC_coq.Rewrite.context)) in - let subst = AAC_matcher.Subst.to_list subst in - let subst = List.map (fun (x,y) -> x, conv y) subst in - let by_aac_reflexivity = (by_aac_reflexivity rewinfo.subject rewinfo.eqt ir) in - core_aac_rewrite ?abort rewinfo subst by_aac_reflexivity tr_step_raw tr_step subject - - with - | NoSolutions -> - Tacticals.tclFAIL 0 - (Pp.str (if occ_subterm = None && occ_sol = None - then "No matching occurence modulo AC found" - else "No such solution")) - ) - ) goal - - -open Rewrite -open Tacmach -open Tacticals -open Tacexpr -open Tacinterp -open Extraargs -open Genarg - -let rec add k x = function - | [] -> [k,x] - | k',_ as ky::q -> - if k'=k then AAC_coq.user_error ("redondant argument ("^k^")") - else ky::add k x q - -let get k l = try Some (List.assoc k l) with Not_found -> None - -let get_lhs l = try List.assoc "in_right" l; false with Not_found -> true - -let aac_rewrite ~args = - aac_rewrite ~occ_subterm:(get "at" args) ~occ_sol:(get "subst" args) ~in_left:(get_lhs args) - - -let pr_aac_args _ _ _ l = - List.fold_left - (fun acc -> function - | ("in_right" as s,_) -> Pp.(++) (Pp.str s) acc - | (k,i) -> Pp.(++) (Pp.(++) (Pp.str k) (Pp.int i)) acc - ) (Pp.str "") l - -ARGUMENT EXTEND aac_args -TYPED AS ((string * int) list ) -PRINTED BY pr_aac_args -| [ "at" integer(n) aac_args(q) ] -> [ add "at" n q ] -| [ "subst" integer(n) aac_args(q) ] -> [ add "subst" n q ] -| [ "in_right" aac_args(q) ] -> [ add "in_right" 0 q ] -| [ ] -> [ [] ] -END - -let pr_constro _ _ _ = fun b -> - match b with - | None -> Pp.str "" - | Some o -> Pp.str "" - -ARGUMENT EXTEND constro -TYPED AS (constr option) -PRINTED BY pr_constro -| [ "[" constr(c) "]" ] -> [ Some c ] -| [ ] -> [ None ] -END - -TACTIC EXTEND _aac_reflexivity_ -| [ "aac_reflexivity" ] -> [ aac_reflexivity ] -END - -TACTIC EXTEND _aac_normalise_ -| [ "aac_normalise" ] -> [ aac_normalise ] -END - -TACTIC EXTEND _aac_rewrite_ -| [ "aac_rewrite" orient(l2r) constr(c) aac_args(args) constro(extra)] -> - [ fun gl -> aac_rewrite ?extra ~args ~l2r ~strict:true c gl ] -END - -TACTIC EXTEND _aac_pattern_ -| [ "aac_pattern" orient(l2r) constr(c) aac_args(args) constro(extra)] -> - [ fun gl -> aac_rewrite ?extra ~args ~l2r ~strict:true ~abort:true c gl ] -END - -TACTIC EXTEND _aac_instances_ -| [ "aac_instances" orient(l2r) constr(c) aac_args(args) constro(extra)] -> - [ fun gl -> aac_rewrite ?extra ~args ~l2r ~strict:true ~show:true c gl ] -END - -TACTIC EXTEND _aacu_rewrite_ -| [ "aacu_rewrite" orient(l2r) constr(c) aac_args(args) constro(extra)] -> - [ fun gl -> aac_rewrite ?extra ~args ~l2r ~strict:false c gl ] -END - -TACTIC EXTEND _aacu_pattern_ -| [ "aacu_pattern" orient(l2r) constr(c) aac_args(args) constro(extra)] -> - [ fun gl -> aac_rewrite ?extra ~args ~l2r ~strict:false ~abort:true c gl ] -END - -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 diff --git a/AAC_rewrite.mli b/AAC_rewrite.mli deleted file mode 100644 index d195075..0000000 --- a/AAC_rewrite.mli +++ /dev/null @@ -1,9 +0,0 @@ -(***************************************************************************) -(* This is part of aac_tactics, it is distributed under the terms of the *) -(* GNU Lesser General Public License version 3 *) -(* (see file LICENSE for more details) *) -(* *) -(* Copyright 2009-2010: Thomas Braibant, Damien Pous. *) -(***************************************************************************) - -(** Definition of the tactics, and corresponding Coq grammar entries.*) diff --git a/AAC_search_monad.ml b/AAC_search_monad.ml deleted file mode 100644 index 09a6455..0000000 --- a/AAC_search_monad.ml +++ /dev/null @@ -1,70 +0,0 @@ -(***************************************************************************) -(* This is part of aac_tactics, it is distributed under the terms of the *) -(* GNU Lesser General Public License version 3 *) -(* (see file LICENSE for more details) *) -(* *) -(* Copyright 2009-2010: Thomas Braibant, Damien Pous. *) -(***************************************************************************) - -type 'a m = | F of 'a - | N of 'a m list - -let fold (f : 'a -> 'b -> 'b) (m : 'a m) (acc : 'b) = - let rec aux acc = function - F x -> f x acc - | N l -> - (List.fold_left (fun acc x -> - match x with - | (N []) -> acc - | x -> aux acc x - ) acc l) - in - aux acc m - - -let rec (>>) : 'a m -> ('a -> 'b m) -> 'b m = - fun m f -> - match m with - | F x -> f x - | N l -> - N (List.fold_left (fun acc x -> - match x with - | (N []) -> acc - | x -> (x >> f)::acc - ) [] l) - -let (>>|) (m : 'a m) (n :'a m) : 'a m = match (m,n) with - | N [],_ -> n - | _,N [] -> m - | F x, N l -> N (F x::l) - | N l, F x -> N (F x::l) - | x,y -> N [x;y] - -let return : 'a -> 'a m = fun x -> F x -let fail : unit -> 'a m = fun () -> N [] - -let sprint f m = - fold (fun x acc -> Printf.sprintf "%s\n%s" acc (f x)) m "" -let rec count = function - | F _ -> 1 - | N l -> List.fold_left (fun acc x -> acc+count x) 0 l - -let opt_comb f x y = match x with None -> f y | _ -> x - -let rec choose = function - | F x -> Some x - | N l -> List.fold_left (fun acc x -> - opt_comb choose acc x - ) None l - -let is_empty = fun x -> choose x = None - -let to_list m = (fold (fun x acc -> x::acc) m []) - -let sort f m = - N (List.map (fun x -> F x) (List.sort f (to_list m))) - -(* preserve the structure of the heap *) -let filter f m = - fold (fun x acc -> (if f x then return x else fail ()) >>| acc) m (N []) - diff --git a/AAC_search_monad.mli b/AAC_search_monad.mli deleted file mode 100644 index 7e2a910..0000000 --- a/AAC_search_monad.mli +++ /dev/null @@ -1,42 +0,0 @@ -(***************************************************************************) -(* This is part of aac_tactics, it is distributed under the terms of the *) -(* GNU Lesser General Public License version 3 *) -(* (see file LICENSE for more details) *) -(* *) -(* Copyright 2009-2010: Thomas Braibant, Damien Pous. *) -(***************************************************************************) - -(** Search monad that allows to express non-deterministic algorithms - in a legible maner, or programs that solve combinatorial problems. - - @see the - inspiration of this module -*) - -(** A data type that represent a collection of ['a] *) -type 'a m - - (** {2 Monadic operations} *) - -(** bind and return *) -val ( >> ) : 'a m -> ('a -> 'b m) -> 'b m -val return : 'a -> 'a m - -(** non-deterministic choice *) -val ( >>| ) : 'a m -> 'a m -> 'a m - -(** failure *) -val fail : unit -> 'a m - -(** folding through the collection *) -val fold : ('a -> 'b -> 'b) -> 'a m -> 'b -> 'b - -(** {2 Derived facilities } *) - -val sprint : ('a -> string) -> 'a m -> string -val count : 'a m -> int -val choose : 'a m -> 'a option -val to_list : 'a m -> 'a list -val sort : ('a -> 'a -> int) -> 'a m -> 'a m -val is_empty: 'a m -> bool -val filter : ('a -> bool) -> 'a m -> 'a m diff --git a/AAC_theory.ml b/AAC_theory.ml deleted file mode 100644 index 55b9e21..0000000 --- a/AAC_theory.ml +++ /dev/null @@ -1,1097 +0,0 @@ -(***************************************************************************) -(* This is part of aac_tactics, it is distributed under the terms of the *) -(* GNU Lesser General Public License version 3 *) -(* (see file LICENSE for more details) *) -(* *) -(* Copyright 2009-2010: Thomas Braibant, Damien Pous. *) -(***************************************************************************) - -(** Constr from the theory of this particular development - - The inner-working of this module is highly correlated with the - particular structure of {b AAC.v}, therefore, it should - be of little interest to most readers. -*) -open Term - -module Control = struct - let printing = true - let debug = false - let time = false -end - -module Debug = AAC_helper.Debug (Control) -open Debug - -(** {1 HMap : Specialized Hashtables based on constr} *) - - -module Hashed_constr = -struct - type t = constr - let equal = (=) - let hash = Hashtbl.hash -end - - (* TODO module HMap = Hashtbl, du coup ? *) -module HMap = Hashtbl.Make(Hashed_constr) - -let ac_theory_path = ["AAC_tactics"; "AAC"] - -module Stubs = struct - let path = ac_theory_path@["Internal"] - - (** The constants from the inductive type *) - let _Tty = lazy (AAC_coq.init_constant path "T") - let vTty = lazy (AAC_coq.init_constant path "vT") - - let rsum = lazy (AAC_coq.init_constant path "sum") - let rprd = lazy (AAC_coq.init_constant path "prd") - let rsym = lazy (AAC_coq.init_constant path "sym") - let runit = lazy (AAC_coq.init_constant path "unit") - - let vnil = lazy (AAC_coq.init_constant path "vnil") - let vcons = lazy (AAC_coq.init_constant path "vcons") - let eval = lazy (AAC_coq.init_constant path "eval") - - - let decide_thm = lazy (AAC_coq.init_constant path "decide") - let lift_normalise_thm = lazy (AAC_coq.init_constant path "lift_normalise") - - let lift = - lazy (AAC_coq.init_constant ac_theory_path "AAC_lift") - let lift_proj_equivalence= - lazy (AAC_coq.init_constant ac_theory_path "aac_lift_equivalence") - let lift_transitivity_left = - lazy(AAC_coq.init_constant ac_theory_path "lift_transitivity_left") - let lift_transitivity_right = - lazy(AAC_coq.init_constant ac_theory_path "lift_transitivity_right") - let lift_reflexivity = - lazy(AAC_coq.init_constant ac_theory_path "lift_reflexivity") -end - -module Classes = struct - module Associative = struct - let path = ac_theory_path - let typ = lazy (AAC_coq.init_constant path "Associative") - let ty (rlt : AAC_coq.Relation.t) (value : Term.constr) = - mkApp (Lazy.force typ, [| rlt.AAC_coq.Relation.carrier; - rlt.AAC_coq.Relation.r; - value - |] ) - let infer goal rlt value = - let ty = ty rlt value in - AAC_coq.resolve_one_typeclass goal ty - end - - module Commutative = struct - let path = ac_theory_path - let typ = lazy (AAC_coq.init_constant path "Commutative") - let ty (rlt : AAC_coq.Relation.t) (value : Term.constr) = - mkApp (Lazy.force typ, [| rlt.AAC_coq.Relation.carrier; - rlt.AAC_coq.Relation.r; - value - |] ) - - end - - module Proper = struct - let path = ac_theory_path @ ["Internal";"Sym"] - let typeof = lazy (AAC_coq.init_constant path "type_of") - let relof = lazy (AAC_coq.init_constant path "rel_of") - let mk_typeof : AAC_coq.Relation.t -> int -> constr = fun rlt n -> - let x = rlt.AAC_coq.Relation.carrier in - mkApp (Lazy.force typeof, [| x ; AAC_coq.Nat.of_int n |]) - let mk_relof : AAC_coq.Relation.t -> int -> constr = fun rlt n -> - let (x,r) = AAC_coq.Relation.split rlt in - mkApp (Lazy.force relof, [| x;r ; AAC_coq.Nat.of_int n |]) - - let ty rlt op ar = - let typeof = mk_typeof rlt ar in - let relof = mk_relof rlt ar in - AAC_coq.Classes.mk_morphism typeof relof op - let infer goal rlt op ar = - let ty = ty rlt op ar in - AAC_coq.resolve_one_typeclass goal ty - end - - module Unit = struct - let path = ac_theory_path - let typ = lazy (AAC_coq.init_constant path "Unit") - let ty (rlt : AAC_coq.Relation.t) (value : Term.constr) (unit : Term.constr)= - mkApp (Lazy.force typ, [| rlt.AAC_coq.Relation.carrier; - rlt.AAC_coq.Relation.r; - value; - unit - |] ) - end - -end - -(* Non empty lists *) -module NEList = struct - let path = ac_theory_path @ ["Internal"] - let typ = lazy (AAC_coq.init_constant path "list") - let nil = lazy (AAC_coq.init_constant path "nil") - let cons = lazy (AAC_coq.init_constant path "cons") - let cons ty h t = - mkApp (Lazy.force cons, [| ty; h ; t |]) - let nil ty x = - (mkApp (Lazy.force nil, [| ty ; x|])) - let rec of_list ty = function - | [] -> invalid_arg "NELIST" - | [x] -> nil ty x - | t::q -> cons ty t (of_list ty q) - - let type_of_list ty = - mkApp (Lazy.force typ, [|ty|]) -end - -(** a [mset] is a ('a * pos) list *) -let mk_mset ty (l : (constr * int) list) = - let pos = Lazy.force AAC_coq.Pos.typ in - let pair (x : constr) (ar : int) = - AAC_coq.Pair.of_pair ty pos (x, AAC_coq.Pos.of_int ar) - in - let pair_ty = AAC_coq.lapp AAC_coq.Pair.typ [| ty ; pos|] in - let rec aux = function - | [ ] -> assert false - | [x,ar] -> NEList.nil pair_ty (pair x ar) - | (t,ar)::q -> NEList.cons pair_ty (pair t ar) (aux q) - in - aux l - -module Sigma = struct - let sigma = lazy (AAC_coq.init_constant ac_theory_path "sigma") - let sigma_empty = lazy (AAC_coq.init_constant ac_theory_path "sigma_empty") - let sigma_add = lazy (AAC_coq.init_constant ac_theory_path "sigma_add") - let sigma_get = lazy (AAC_coq.init_constant ac_theory_path "sigma_get") - - let add ty n x map = - mkApp (Lazy.force sigma_add,[|ty; n; x ; map|]) - let empty ty = - mkApp (Lazy.force sigma_empty,[|ty |]) - let typ ty = - mkApp (Lazy.force sigma, [|ty|]) - - let to_fun ty null map = - mkApp (Lazy.force sigma_get, [|ty;null;map|]) - - let of_list ty null l = - match l with - | (_,t)::q -> - let map = - List.fold_left - (fun acc (i,t) -> - assert (i > 0); - add ty (AAC_coq.Pos.of_int i) ( t) acc) - (empty ty) - q - in to_fun ty (t) map - | [] -> debug "of_list empty" ; to_fun ty (null) (empty ty) - - -end - - -module Sym = struct - type pack = {ar: Term.constr; value: Term.constr ; morph: Term.constr} - let path = ac_theory_path @ ["Internal";"Sym"] - let typ = lazy (AAC_coq.init_constant path "pack") - let mkPack = lazy (AAC_coq.init_constant path "mkPack") - let value = lazy (AAC_coq.init_constant path "value") - let null = lazy (AAC_coq.init_constant path "null") - let mk_pack (rlt: AAC_coq.Relation.t) s = - let (x,r) = AAC_coq.Relation.split rlt in - mkApp (Lazy.force mkPack, [|x;r; s.ar;s.value;s.morph|]) - let null rlt = - let x = rlt.AAC_coq.Relation.carrier in - let r = rlt.AAC_coq.Relation.r in - mkApp (Lazy.force null, [| x;r;|]) - - let mk_ty : AAC_coq.Relation.t -> constr = fun rlt -> - let (x,r) = AAC_coq.Relation.split rlt in - mkApp (Lazy.force typ, [| x; r|] ) -end - -module Bin =struct - type pack = {value : Term.constr; - compat : Term.constr; - assoc : Term.constr; - comm : Term.constr option; - } - - let path = ac_theory_path @ ["Internal";"Bin"] - let typ = lazy (AAC_coq.init_constant path "pack") - let mkPack = lazy (AAC_coq.init_constant path "mk_pack") - - let mk_pack: AAC_coq.Relation.t -> pack -> Term.constr = fun (rlt) s -> - let (x,r) = AAC_coq.Relation.split rlt in - let comm_ty = Classes.Commutative.ty rlt s.value in - mkApp (Lazy.force mkPack , [| x ; r; - s.value; - s.compat ; - s.assoc; - AAC_coq.Option.of_option comm_ty s.comm - |]) - let mk_ty : AAC_coq.Relation.t -> constr = fun rlt -> - let (x,r) = AAC_coq.Relation.split rlt in - mkApp (Lazy.force typ, [| x; r|] ) -end - -module Unit = struct - let path = ac_theory_path @ ["Internal"] - let unit_of_ty = lazy (AAC_coq.init_constant path "unit_of") - let unit_pack_ty = lazy (AAC_coq.init_constant path "unit_pack") - let mk_unit_of = lazy (AAC_coq.init_constant path "mk_unit_for") - let mk_unit_pack = lazy (AAC_coq.init_constant path "mk_unit_pack") - - type unit_of = - { - uf_u : Term.constr; (* u *) - uf_idx : Term.constr; - uf_desc : Term.constr; (* Unit R (e_bin uf_idx) u *) - } - - type pack = { - u_value : Term.constr; (* X *) - u_desc : (unit_of) list (* unit_of u_value *) - } - - let ty_unit_of rlt e_bin u = - let (x,r) = AAC_coq.Relation.split rlt in - mkApp ( Lazy.force unit_of_ty, [| x; r; e_bin; u |]) - - let ty_unit_pack rlt e_bin = - let (x,r) = AAC_coq.Relation.split rlt in - mkApp (Lazy.force unit_pack_ty, [| x; r; e_bin |]) - - let mk_unit_of rlt e_bin u unit_of = - let (x,r) = AAC_coq.Relation.split rlt in - mkApp (Lazy.force mk_unit_of , [| x; - r; - e_bin ; - u; - unit_of.uf_idx; - unit_of.uf_desc - |]) - - let mk_pack rlt e_bin pack : Term.constr = - let (x,r) = AAC_coq.Relation.split rlt in - let ty = ty_unit_of rlt e_bin pack.u_value in - let mk_unit_of = mk_unit_of rlt e_bin pack.u_value in - let u_desc =AAC_coq.List.of_list ( ty ) (List.map mk_unit_of pack.u_desc) in - mkApp (Lazy.force mk_unit_pack, [|x;r; - e_bin ; - pack.u_value; - u_desc - |]) - - let default x : pack = - { u_value = x; - u_desc = [] - } - -end - -let anomaly msg = - Util.anomaly ("aac_tactics: " ^ msg) - -let user_error msg = - Util.error ("aac_tactics: " ^ msg) - -module Trans = struct - - (** {1 From Coq to Abstract Syntax Trees (AST)} - - This module provides facilities to interpret a Coq term with - arbitrary operators as an abstract syntax tree. Considering an - application, we try to infer instances of our classes. - - We consider that [A] operators are coarser than [AC] operators, - which in turn are coarser than raw morphisms. That means that - [List.append], of type [(A : Type) -> list A -> list A -> list - A] can be understood as an [A] operator. - - During this reification, we gather some informations that will - be used to rebuild Coq terms from AST ( type {!envs}) - - We use a main hash-table from [constr] to [pack], in order to - discriminate the various constructors. All these are mixed in - order to improve on the number of comparisons in the tables *) - - (* 'a * (unit, op_unit) option *) - type 'a with_unit = 'a * (Unit.unit_of) option - type pack = - (* used to infer the AC/A structure in the first pass {!Gather} *) - | Bin of Bin.pack with_unit - (* will only be used in the second pass : {!Parse}*) - | Sym of Sym.pack - | Unit of constr (* to avoid confusion in bloom *) - - (** discr is a map from {!Term.constr} to {!pack}. - - [None] means that it is not possible to instantiate this partial - application to an interesting class. - - [Some x] means that we found something in the past. This means - in particular that a single [constr] cannot be two things at the - same time. - - The field [bloom] allows to give a unique number to each class we - found. *) - type envs = - { - discr : (pack option) HMap.t ; - bloom : (pack, int ) Hashtbl.t; - bloom_back : (int, pack ) Hashtbl.t; - bloom_next : int ref; - } - - let empty_envs () = - { - discr = HMap.create 17; - bloom = Hashtbl.create 17; - bloom_back = Hashtbl.create 17; - bloom_next = ref 1; - } - - - - let add_bloom envs pack = - if Hashtbl.mem envs.bloom pack - then () - else - let x = ! (envs.bloom_next) in - Hashtbl.add envs.bloom pack x; - Hashtbl.add envs.bloom_back x pack; - incr (envs.bloom_next) - - let find_bloom envs pack = - try Hashtbl.find envs.bloom pack - with Not_found -> assert false - - (********************************************) - (* (\* Gather the occuring AC/A symbols *\) *) - (********************************************) - - (** This modules exhibit a function that memoize in the environment - all the AC/A operators as well as the morphism that occur. This - staging process allows us to prefer AC/A operators over raw - morphisms. Moreover, for each AC/A operators, we need to try to - infer units. Otherwise, we do not have [x * y * x <= a * a] since 1 - does not occur. - - But, do we also need to check whether constants are - units. Otherwise, we do not have the ability to rewrite [0 = a + - a] in [a = ...]*) - module Gather : sig - val gather : AAC_coq.goal_sigma -> AAC_coq.Relation.t -> envs -> Term.constr -> AAC_coq.goal_sigma - end - = struct - - let memoize envs t pack : unit = - begin - HMap.add envs.discr t (Some pack); - add_bloom envs pack; - match pack with - | Bin (_, None) | Sym _ -> () - | Bin (_, Some (unit_of)) -> - let unit = unit_of.Unit.uf_u in - HMap.add envs.discr unit (Some (Unit unit)); - add_bloom envs (Unit unit); - | Unit _ -> assert false - end - - - let get_unit (rlt : AAC_coq.Relation.t) op goal : - (AAC_coq.goal_sigma * constr * constr ) option= - let x = (rlt.AAC_coq.Relation.carrier) in - let unit, goal = AAC_coq.evar_unit goal x in - let ty =Classes.Unit.ty rlt op unit in - let result = - try - let t,goal = AAC_coq.resolve_one_typeclass goal ty in - Some (goal,t,unit) - with Not_found -> None - in - match result with - | None -> None - | Some (goal,s,unit) -> - let unit = AAC_coq.nf_evar goal unit in - Some (goal, unit, s) - - - - (** gives back the class and the operator *) - let is_bin (rlt: AAC_coq.Relation.t) (op: constr) ( goal: AAC_coq.goal_sigma) - : (AAC_coq.goal_sigma * Bin.pack) option = - let assoc_ty = Classes.Associative.ty rlt op in - let comm_ty = Classes.Commutative.ty rlt op in - let proper_ty = Classes.Proper.ty rlt op 2 in - try - let proper , goal = AAC_coq.resolve_one_typeclass goal proper_ty in - let assoc, goal = AAC_coq.resolve_one_typeclass goal assoc_ty in - let comm , goal = - try - let comm, goal = AAC_coq.resolve_one_typeclass goal comm_ty in - Some comm, goal - with Not_found -> - None, goal - in - let bin = - {Bin.value = op; - Bin.compat = proper; - Bin.assoc = assoc; - Bin.comm = comm } - in - Some (goal,bin) - with |Not_found -> None - - let is_bin (rlt : AAC_coq.Relation.t) (op : constr) (goal : AAC_coq.goal_sigma)= - match is_bin rlt op goal with - | None -> None - | Some (goal, bin_pack) -> - match get_unit rlt op goal with - | None -> Some (goal, Bin (bin_pack, None)) - | Some (gl, unit,s) -> - let unit_of = - { - Unit.uf_u = unit; - (* TRICK : this term is not well-typed by itself, - but it is okay the way we use it in the other - functions *) - Unit.uf_idx = op; - Unit.uf_desc = s; - } - in Some (gl,Bin (bin_pack, Some (unit_of))) - - - (** {is_morphism} try to infer the kind of operator we are - dealing with *) - let is_morphism goal (rlt : AAC_coq.Relation.t) (papp : Term.constr) (ar : int) : (AAC_coq.goal_sigma * pack ) option = - let typeof = Classes.Proper.mk_typeof rlt ar in - let relof = Classes.Proper.mk_relof rlt ar in - let m = AAC_coq.Classes.mk_morphism typeof relof papp in - try - let m,goal = AAC_coq.resolve_one_typeclass goal m in - let pack = {Sym.ar = (AAC_coq.Nat.of_int ar); Sym.value= papp; Sym.morph= m} in - Some (goal, Sym pack) - with - | Not_found -> None - - - (* [crop_app f [| a_0 ; ... ; a_n |]] - returns Some (f a_0 ... a_(n-2), [|a_(n-1); a_n |] ) - *) - let crop_app t ca : (constr * constr array) option= - let n = Array.length ca in - if n <= 1 - then None - else - let papp = Term.mkApp (t, Array.sub ca 0 (n-2) ) in - let args = Array.sub ca (n-2) 2 in - Some (papp, args ) - - let fold goal (rlt : AAC_coq.Relation.t) envs t ca cont = - let fold_morphism t ca = - let nb_params = Array.length ca in - let rec aux n = - assert (n < nb_params && 0 < nb_params ); - let papp = Term.mkApp (t, Array.sub ca 0 n) in - match is_morphism goal rlt papp (nb_params - n) with - | None -> - (* here we have to memoize the failures *) - HMap.add envs.discr papp None; - if n < nb_params - 1 then aux (n+1) else goal - | Some (goal, pack) -> - let args = Array.sub ca (n) (nb_params -n)in - let goal = Array.fold_left cont goal args in - memoize envs papp pack; - goal - in - if nb_params = 0 then goal else aux 0 - in - let is_aac t = is_bin rlt t in - match crop_app t ca with - | None -> - fold_morphism t ca - | Some (papp, args) -> - begin match is_aac papp goal with - | None -> fold_morphism t ca - | Some (goal, pack) -> - memoize envs papp pack; - Array.fold_left cont goal args - end - - (* update in place the envs of known stuff, using memoization. We - have to memoize failures, here. *) - let gather goal (rlt : AAC_coq.Relation.t ) envs t : AAC_coq.goal_sigma = - let rec aux goal x = - match AAC_coq.decomp_term x with - | App (t,ca) -> - fold goal rlt envs t ca (aux ) - | _ -> goal - in - aux goal t - end - - (** We build a term out of a constr, updating in place the - environment if needed (the only kind of such updates are the - constants). *) - module Parse : - sig - val t_of_constr : AAC_coq.goal_sigma -> AAC_coq.Relation.t -> envs -> constr -> AAC_matcher.Terms.t * AAC_coq.goal_sigma - end - = struct - - (** [discriminates goal envs rlt t ca] infer : - - - its {! pack } (is it an AC operator, or an A operator, or a - Symbol ?), - - - the relevant partial application, - - - the vector of the remaining arguments - - We use an expansion to handle the special case of units, - before going back to the general discrimination - procedure. That means that a unit is more coarse than a raw - morphism - - This functions is prevented to go through [ar < 0] by the fact - that a constant is a morphism. But not an eva. *) - - let is_morphism goal (rlt : AAC_coq.Relation.t) (papp : Term.constr) (ar : int) : (AAC_coq.goal_sigma * pack ) option = - let typeof = Classes.Proper.mk_typeof rlt ar in - let relof = Classes.Proper.mk_relof rlt ar in - let m = AAC_coq.Classes.mk_morphism typeof relof papp in - try - let m,goal = AAC_coq.resolve_one_typeclass goal m in - let pack = {Sym.ar = (AAC_coq.Nat.of_int ar); Sym.value= papp; Sym.morph= m} in - Some (goal, Sym pack) - with - | e -> None - - exception NotReflexive - let discriminate goal envs (rlt : AAC_coq.Relation.t) t ca : AAC_coq.goal_sigma * pack * constr * constr array = - let nb_params = Array.length ca in - let rec fold goal ar :AAC_coq.goal_sigma * pack * constr * constr array = - begin - assert (0 <= ar && ar <= nb_params); - let p_app = mkApp (t, Array.sub ca 0 (nb_params - ar)) in - begin - try - begin match HMap.find envs.discr p_app with - | None -> - fold goal (ar-1) - | Some pack -> - (goal, pack, p_app, Array.sub ca (nb_params -ar ) ar) - end - with - Not_found -> (* Could not find this constr *) - memoize (is_morphism goal rlt p_app ar) p_app ar - end - end - and memoize (x) p_app ar = - assert (0 <= ar && ar <= nb_params); - match x with - | Some (goal, pack) -> - HMap.add envs.discr p_app (Some pack); - add_bloom envs pack; - (goal, pack, p_app, Array.sub ca (nb_params-ar) ar) - | None -> - - if ar = 0 then raise NotReflexive; - begin - (* to memoise the failures *) - HMap.add envs.discr p_app None; - (* will terminate, since [const] is capped, and it is - easy to find an instance of a constant *) - fold goal (ar-1) - end - in - try match HMap.find envs.discr (mkApp (t,ca))with - | None -> fold goal (nb_params) - | Some pack -> goal, pack, (mkApp (t,ca)), [| |] - with Not_found -> fold goal (nb_params) - - let discriminate goal envs rlt x = - try - match AAC_coq.decomp_term x with - | App (t,ca) -> - discriminate goal envs rlt t ca - | _ -> discriminate goal envs rlt x [| |] - with - | NotReflexive -> user_error "The relation to which the goal was lifted is not Reflexive" - (* TODO: is it the only source of invalid use that fall - into this catch_all ? *) - | e -> - user_error "Cannot handle this kind of hypotheses (variables occuring under a function symbol which is not a proper morphism)." - - (** [t_of_constr goal rlt envs cstr] builds the abstract syntax tree - of the term [cstr]. Doing so, it modifies the environment of - known stuff [envs], and eventually creates fresh - evars. Therefore, we give back the goal updated accordingly *) - let t_of_constr goal (rlt: AAC_coq.Relation.t ) envs : constr -> AAC_matcher.Terms.t * AAC_coq.goal_sigma = - let r_goal = ref (goal) in - let rec aux x = - match AAC_coq.decomp_term x with - | Rel i -> AAC_matcher.Terms.Var i - | _ -> - let goal, pack , p_app, ca = discriminate (!r_goal) envs rlt x in - r_goal := goal; - let k = find_bloom envs pack - in - match pack with - | Bin (pack,_) -> - begin match pack.Bin.comm with - | Some _ -> - assert (Array.length ca = 2); - AAC_matcher.Terms.Plus ( k, aux ca.(0), aux ca.(1)) - | None -> - assert (Array.length ca = 2); - AAC_matcher.Terms.Dot ( k, aux ca.(0), aux ca.(1)) - end - | Unit _ -> - assert (Array.length ca = 0); - AAC_matcher.Terms.Unit ( k) - | Sym _ -> - AAC_matcher.Terms.Sym ( k, Array.map aux ca) - in - ( - fun x -> let r = aux x in r, !r_goal - ) - - end (* Parse *) - - let add_symbol goal rlt envs l = - let goal = Gather.gather goal rlt envs (Term.mkApp (l, [| Term.mkRel 0;Term.mkRel 0|])) in - goal - - (* [t_of_constr] buils a the abstract syntax tree of a constr, - updating in place the environment. Doing so, we infer all the - morphisms and the AC/A operators. It is mandatory to do so both - for the pattern and the term, since AC symbols can occur in one - and not the other *) - let t_of_constr goal rlt envs (l,r) = - let goal = Gather.gather goal rlt envs l in - let goal = Gather.gather goal rlt envs r in - let l,goal = Parse.t_of_constr goal rlt envs l in - let r, goal = Parse.t_of_constr goal rlt envs r in - l, r, goal - - (* An intermediate representation of the environment, with association lists for AC/A operators, and also the raw [packer] information *) - - type ir = - { - packer : (int, pack) Hashtbl.t; (* = bloom_back *) - bin : (int * Bin.pack) list ; - units : (int * Unit.pack) list; - sym : (int * Term.constr) list ; - matcher_units : AAC_matcher.ext_units - } - - let ir_to_units ir = ir.matcher_units - - let ir_of_envs goal (rlt : AAC_coq.Relation.t) envs = - let add x y l = (x,y)::l in - let nil = [] in - let sym , - (bin : (int * Bin.pack with_unit) list), - (units : (int * constr) list) = - Hashtbl.fold - (fun int pack (sym,bin,units) -> - match pack with - | Bin s -> - sym, add (int) s bin, units - | Sym s -> - add (int) s sym, bin, units - | Unit s -> - sym, bin, add int s units - ) - envs.bloom_back - (nil,nil,nil) - in - let matcher_units = - let unit_for , is_ac = - List.fold_left - (fun ((unit_for,is_ac) as acc) (n,(bp,wu)) -> - match wu with - | None -> acc - | Some (unit_of) -> - let unit_n = Hashtbl.find envs.bloom - (Unit unit_of.Unit.uf_u) - in - ( n, unit_n)::unit_for, - (n, bp.Bin.comm <> None )::is_ac - - ) - ([],[]) bin - in - {AAC_matcher.unit_for = unit_for; AAC_matcher.is_ac = is_ac} - - in - let units : (int * Unit.pack) list = - List.fold_left - (fun acc (n,u) -> - (* first, gather all bins with this unit *) - let all_bin = - List.fold_left - ( fun acc (nop,(bp,wu)) -> - match wu with - | None -> acc - | Some unit_of -> - if unit_of.Unit.uf_u = u - then - {unit_of with - Unit.uf_idx = (AAC_coq.Pos.of_int nop)} :: acc - else - acc - ) - [] bin - in - (n,{ - Unit.u_value = u; - Unit.u_desc = all_bin - })::acc - ) - [] units - - in - goal, { - packer = envs.bloom_back; - bin = (List.map (fun (n,(s,_)) -> n, s) bin); - units = units; - sym = (List.map (fun (n,s) -> n,(Sym.mk_pack rlt s)) sym); - matcher_units = matcher_units - } - - - - (** {1 From AST back to Coq } - - The next functions allow one to map OCaml abstract syntax trees - to Coq terms *) - - (** {2 Building raw, natural, terms} *) - - (** [raw_constr_of_t_debruijn] rebuilds a term in the raw - representation, without products on top, and maybe escaping free - debruijn indices (in the case of a pattern for example). *) - let raw_constr_of_t_debruijn ir (t : AAC_matcher.Terms.t) : Term.constr * int list = - let add_set,get = - let r = ref [] in - let rec add x = function - [ ] -> [x] - | t::q when t = x -> t::q - | t::q -> t:: (add x q) - in - (fun x -> r := add x !r),(fun () -> !r) - in - (* Here, we rely on the invariant that the maps are well formed: - it is meanigless to fail to find a symbol in the maps, or to - find the wrong kind of pack in the maps *) - let rec aux t = - match t with - | AAC_matcher.Terms.Plus (s,l,r) -> - begin match Hashtbl.find ir.packer s with - | Bin (s,_) -> - mkApp (s.Bin.value , [|(aux l);(aux r)|]) - | _ -> Printf.printf "erreur:%i\n%!"s; - assert false - end - | AAC_matcher.Terms.Dot (s,l,r) -> - begin match Hashtbl.find ir.packer s with - | Bin (s,_) -> - mkApp (s.Bin.value, [|(aux l);(aux r)|]) - | _ -> assert false - end - | AAC_matcher.Terms.Sym (s,t) -> - begin match Hashtbl.find ir.packer s with - | Sym s -> - mkApp (s.Sym.value, Array.map aux t) - | _ -> assert false - end - | AAC_matcher.Terms.Unit x -> - begin match Hashtbl.find ir.packer x with - | Unit s -> s - | _ -> assert false - end - | AAC_matcher.Terms.Var i -> add_set i; - mkRel (i) - in - let t = aux t in - t , get ( ) - - (** [raw_constr_of_t] rebuilds a term in the raw representation *) - let raw_constr_of_t ir rlt (context:rel_context) t = - (** cap rebuilds the products in front of the constr *) - let rec cap c = function [] -> c - | t::q -> - let i = Term.lookup_rel t context in - cap (mkProd_or_LetIn i c) q - in - let t,indices = raw_constr_of_t_debruijn ir t in - cap t (List.sort (Pervasives.compare) indices) - - - (** {2 Building reified terms} *) - - (* Some informations to be able to build the maps *) - type reif_params = - { - bin_null : Bin.pack; (* the default A operator *) - sym_null : constr; - unit_null : Unit.pack; - sym_ty : constr; (* the type, as it appears in e_sym *) - bin_ty : constr - } - - - (** A record containing the environments that will be needed by the - decision procedure, as a Coq constr. Contains the functions - from the symbols (as ints) to indexes (as constr) *) - - type sigmas = { - env_sym : Term.constr; - env_bin : Term.constr; - env_units : Term.constr; (* the [idx -> X:constr] *) - } - - - type sigma_maps = { - sym_to_pos : int -> Term.constr; - bin_to_pos : int -> Term.constr; - units_to_pos : int -> Term.constr; - } - - - (** infers some stuff that will be required when we will build - environments (our environments need a default case, so we need - an Op_AC, an Op_A, and a symbol) *) - (* Note : this function can fail if the user is using the wrong - relation, like proving a = b, while the classes are defined with - another relation (==) *) - let build_reif_params goal (rlt : AAC_coq.Relation.t) (zero) : - reif_params * AAC_coq.goal_sigma = - let carrier = rlt.AAC_coq.Relation.carrier in - let bin_null = - try - let op,goal = AAC_coq.evar_binary goal carrier in - let assoc,goal = Classes.Associative.infer goal rlt op in - let compat,goal = Classes.Proper.infer goal rlt op 2 in - let op = AAC_coq.nf_evar goal op in - { - Bin.value = op; - Bin.compat = compat; - Bin.assoc = assoc; - Bin.comm = None - } - with Not_found -> user_error "Cannot infer a default A operator (required at least to be Proper and Associative)" - in - let zero, goal = - try - let evar_op,goal = AAC_coq.evar_binary goal carrier in - let evar_unit, goal = AAC_coq.evar_unit goal carrier in - let query = Classes.Unit.ty rlt evar_op evar_unit in - let _, goal = AAC_coq.resolve_one_typeclass goal query in - AAC_coq.nf_evar goal evar_unit, goal - with _ -> zero, goal in - let sym_null = Sym.null rlt in - let unit_null = Unit.default zero in - let record = - { - bin_null = bin_null; - sym_null = sym_null; - unit_null = unit_null; - sym_ty = Sym.mk_ty rlt ; - bin_ty = Bin.mk_ty rlt - } - in - record, goal - - (* We want to lift down the indexes of symbols. *) - let renumber (l: (int * 'a) list ) = - let _, l = List.fold_left (fun (next,acc) (glob,x) -> - (next+1, (next,glob,x)::acc) - ) (1,[]) l - in - let rec to_global loc = function - | [] -> assert false - | (local, global,x)::q when local = loc -> global - | _::q -> to_global loc q - in - let rec to_local glob = function - | [] -> assert false - | (local, global,x)::q when global = glob -> local - | _::q -> to_local glob q - in - let locals = List.map (fun (local,global,x) -> local,x) l in - locals, (fun x -> to_local x l) , (fun x -> to_global x l) - - (** [build_sigma_maps] given a envs and some reif_params, we are - able to build the sigmas *) - let build_sigma_maps (rlt : AAC_coq.Relation.t) zero ir (k : sigmas * sigma_maps -> Proof_type.tactic ) : Proof_type.tactic = fun goal -> - let rp,goal = build_reif_params goal rlt zero in - let renumbered_sym, to_local, to_global = renumber ir.sym in - let env_sym = Sigma.of_list - rp.sym_ty - (rp.sym_null) - renumbered_sym - in - AAC_coq.cps_mk_letin "env_sym" env_sym - (fun env_sym -> - let bin = (List.map ( fun (n,s) -> n, Bin.mk_pack rlt s) ir.bin) in - let env_bin = - Sigma.of_list - rp.bin_ty - (Bin.mk_pack rlt rp.bin_null) - bin - in - AAC_coq.cps_mk_letin "env_bin" env_bin - (fun env_bin -> - let units = (List.map (fun (n,s) -> n, Unit.mk_pack rlt env_bin s)ir.units) in - let env_units = - Sigma.of_list - (Unit.ty_unit_pack rlt env_bin) - (Unit.mk_pack rlt env_bin rp.unit_null ) - units - in - - AAC_coq.cps_mk_letin "env_units" env_units - (fun env_units -> - let sigmas = - { - env_sym = env_sym ; - env_bin = env_bin ; - env_units = env_units; - } in - let f = List.map (fun (x,_) -> (x,AAC_coq.Pos.of_int x)) in - let sigma_maps = - { - sym_to_pos = (let sym = f renumbered_sym in fun x -> (List.assoc (to_local x) sym)); - bin_to_pos = (let bin = f bin in fun x -> (List.assoc x bin)); - units_to_pos = (let units = f units in fun x -> (List.assoc x units)); - } - in - k (sigmas, sigma_maps ) - ) - ) - ) goal - - (** builders for the reification *) - type reif_builders = - { - rsum: constr -> constr -> constr -> constr; - rprd: constr -> constr -> constr -> constr; - rsym: constr -> constr array -> constr; - runit : constr -> constr - } - - (* donne moi une tactique, je rajoute ma part. Potentiellement, il - est possible d'utiliser la notation 'do' a la Haskell: - http://www.cas.mcmaster.ca/~carette/pa_monad/ *) - let (>>) : 'a * Proof_type.tactic -> ('a -> 'b * Proof_type.tactic) -> 'b * Proof_type.tactic = - fun (x,t) f -> - let b,t' = f x in - b, Tacticals.tclTHEN t t' - - let return x = x, Tacticals.tclIDTAC - - let mk_vect vnil vcons v = - let ar = Array.length v in - let rec aux = function - | 0 -> vnil - | n -> let n = n-1 in - mkApp( vcons, - [| - (AAC_coq.Nat.of_int n); - v.(ar - 1 - n); - (aux (n)) - |] - ) - in aux ar - - (* TODO: use a do notation *) - let mk_reif_builders (rlt: AAC_coq.Relation.t) (env_sym:constr) (k: reif_builders -> Proof_type.tactic) = - let x = (rlt.AAC_coq.Relation.carrier) in - let r = (rlt.AAC_coq.Relation.r) in - - let x_r_env = [|x;r;env_sym|] in - let tty = mkApp (Lazy.force Stubs._Tty, x_r_env) in - let rsum = mkApp (Lazy.force Stubs.rsum, x_r_env) in - let rprd = mkApp (Lazy.force Stubs.rprd, x_r_env) in - let rsym = mkApp (Lazy.force Stubs.rsym, x_r_env) in - let vnil = mkApp (Lazy.force Stubs.vnil, x_r_env) in - let vcons = mkApp (Lazy.force Stubs.vcons, x_r_env) in - AAC_coq.cps_mk_letin "tty" tty - (fun tty -> - AAC_coq.cps_mk_letin "rsum" rsum - (fun rsum -> - AAC_coq.cps_mk_letin "rprd" rprd - (fun rprd -> - AAC_coq.cps_mk_letin "rsym" rsym - (fun rsym -> - AAC_coq.cps_mk_letin "vnil" vnil - (fun vnil -> - AAC_coq.cps_mk_letin "vcons" vcons - (fun vcons -> - let r ={ - rsum = - begin fun idx l r -> - mkApp (rsum, [| idx ; mk_mset tty [l,1 ; r,1]|]) - end; - rprd = - begin fun idx l r -> - let lst = NEList.of_list tty [l;r] in - mkApp (rprd, [| idx; lst|]) - end; - rsym = - begin fun idx v -> - let vect = mk_vect vnil vcons v in - mkApp (rsym, [| idx; vect|]) - end; - runit = fun idx -> (* could benefit of a letin *) - mkApp (Lazy.force Stubs.runit , [|x;r;env_sym;idx; |]) - } - in k r - )))))) - - - - type reifier = sigma_maps * reif_builders - - - let mk_reifier rlt zero envs (k : sigmas *reifier -> Proof_type.tactic) = - build_sigma_maps rlt zero envs - (fun (s,sm) -> - mk_reif_builders rlt s.env_sym - (fun rb ->k (s,(sm,rb)) ) - - ) - - (** [reif_constr_of_t reifier t] rebuilds the term [t] in the - reified form. We use the [reifier] to minimise the size of the - terms (we make as much lets as possible)*) - let reif_constr_of_t (sm,rb) (t:AAC_matcher.Terms.t) : constr = - let rec aux = function - | AAC_matcher.Terms.Plus (s,l,r) -> - let idx = sm.bin_to_pos s in - rb.rsum idx (aux l) (aux r) - | AAC_matcher.Terms.Dot (s,l,r) -> - let idx = sm.bin_to_pos s in - rb.rprd idx (aux l) (aux r) - | AAC_matcher.Terms.Sym (s,t) -> - let idx = sm.sym_to_pos s in - rb.rsym idx (Array.map aux t) - | AAC_matcher.Terms.Unit s -> - let idx = sm.units_to_pos s in - rb.runit idx - | AAC_matcher.Terms.Var i -> - anomaly "call to reif_constr_of_t on a term with variables." - in aux t -end - - - diff --git a/AAC_theory.mli b/AAC_theory.mli deleted file mode 100644 index 2f57446..0000000 --- a/AAC_theory.mli +++ /dev/null @@ -1,197 +0,0 @@ -(***************************************************************************) -(* This is part of aac_tactics, it is distributed under the terms of the *) -(* GNU Lesser General Public License version 3 *) -(* (see file LICENSE for more details) *) -(* *) -(* Copyright 2009-2010: Thomas Braibant, Damien Pous. *) -(***************************************************************************) - -(** Bindings for Coq constants that are specific to the plugin; - reification and translation functions. - - Note: this module is highly correlated with the definitions of {i - AAC.v}. - - This module interfaces with the above Coq module; it provides - facilities to interpret a term with arbitrary operators as an - abstract syntax tree, and to convert an AST into a Coq term - (either using the Coq "raw" terms, as written in the starting - goal, or using the reified Coq datatypes we define in {i - AAC.v}). -*) - -(** Both in OCaml and Coq, we represent finite multisets using - weighted lists ([('a*int) list]), see {!AAC_matcher.mset}. - - [mk_mset ty l] constructs a Coq multiset from an OCaml multiset - [l] of Coq terms of type [ty] *) - -val mk_mset:Term.constr -> (Term.constr * int) list ->Term.constr - -(** {2 Packaging modules} *) - -(** Environments *) -module Sigma: -sig - (** [add ty n x map] adds the value [x] of type [ty] with key [n] in [map] *) - val add: Term.constr ->Term.constr ->Term.constr ->Term.constr ->Term.constr - - (** [empty ty] create an empty map of type [ty] *) - val empty: Term.constr ->Term.constr - - (** [of_list ty null l] translates an OCaml association list into a Coq one *) - val of_list: Term.constr -> Term.constr -> (int * Term.constr ) list -> Term.constr - - (** [to_fun ty null map] converts a Coq association list into a Coq function (with default value [null]) *) - val to_fun: Term.constr ->Term.constr ->Term.constr ->Term.constr -end - - -(** Dynamically typed morphisms *) -module Sym: -sig - (** mimics the Coq record [Sym.pack] *) - type pack = {ar: Term.constr; value: Term.constr ; morph: Term.constr} - - val typ: Term.constr lazy_t - - - (** [mk_pack rlt (ar,value,morph)] *) - val mk_pack: AAC_coq.Relation.t -> pack -> Term.constr - - (** [null] builds a dummy (identity) symbol, given an {!AAC_coq.Relation.t} *) - val null: AAC_coq.Relation.t -> Term.constr - -end - - -(** We need to export some Coq stubs out of this module. They are used - by the main tactic, see {!AAC_rewrite} *) -module Stubs : sig - val lift : Term.constr Lazy.t - val lift_proj_equivalence : Term.constr Lazy.t - val lift_transitivity_left : Term.constr Lazy.t - val lift_transitivity_right : Term.constr Lazy.t - val lift_reflexivity : Term.constr Lazy.t - (** The evaluation fonction, used to convert a reified coq term to a - raw coq term *) - val eval: Term.constr lazy_t - - (** The main lemma of our theory, that is - [compare (norm u) (norm v) = Eq -> eval u == eval v] *) - val decide_thm:Term.constr lazy_t - - val lift_normalise_thm : Term.constr lazy_t -end - -(** {2 Building reified terms} - - We define a bundle of functions to build reified versions of the - terms (those that will be given to the reflexive decision - procedure). In particular, each field takes as first argument the - index of the symbol rather than the symbol itself. *) - -(** Tranlations between Coq and OCaml *) -module Trans : sig - - (** This module provides facilities to interpret a term with - arbitrary operators as an instance of an abstract syntax tree - {!AAC_matcher.Terms.t}. - - For each Coq application [f x_1 ... x_n], this amounts to - deciding whether one of the partial applications [f x_1 - ... x_i], [i<=n] is a proper morphism, whether the partial - application with [i=n-2] yields an A or AC binary operator, and - whether the whole term is the unit for some A or AC operator. We - use typeclass resolution to test each of these possibilities. - - Note that there are ambiguous terms: - - a term like [f x y] might yield a unary morphism ([f x]) and a - binary one ([f]); we select the latter one (unless [f] is A or - AC, in which case we declare it accordingly); - - a term like [S O] can be considered as a morphism ([S]) - applied to a unit for [(+)], or as a unit for [( * )]; we - chose to give priority to units, so that the latter - interpretation is selected in this case; - - an element might be the unit for several operations - *) - - (** To achieve this reification, one need to record informations - about the collected operators (symbols, binary operators, - units). We use the following imperative internal data-structure to - this end. *) - - type envs - val empty_envs : unit -> envs - - - (** {2 Reification: from Coq terms to AST {!AAC_matcher.Terms.t} } *) - - - (** [t_of_constr goal rlt envs (left,right)] builds the abstract - syntax tree of the terms [left] and [right]. We rely on the [goal] - to perform typeclasses resolutions to find morphisms compatible - with the relation [rlt]. Doing so, it modifies the reification - environment [envs]. Moreover, we need to create fresh - evars; this is why we give back the [goal], accordingly - updated. *) - - val t_of_constr : AAC_coq.goal_sigma -> AAC_coq.Relation.t -> envs -> (Term.constr * Term.constr) -> AAC_matcher.Terms.t * AAC_matcher.Terms.t * AAC_coq.goal_sigma - - (** [add_symbol] adds a given binary symbol to the environment of - known stuff. *) - val add_symbol : AAC_coq.goal_sigma -> AAC_coq.Relation.t -> envs -> Term.constr -> AAC_coq.goal_sigma - - (** {2 Reconstruction: from AST back to Coq terms } - - The next functions allow one to map OCaml abstract syntax trees - to Coq terms. We need two functions to rebuild different kind of - terms: first, raw terms, like the one encountered by - {!t_of_constr}; second, reified Coq terms, that are required for - the reflexive decision procedure. *) - - type ir - val ir_of_envs : AAC_coq.goal_sigma -> AAC_coq.Relation.t -> envs -> AAC_coq.goal_sigma * ir - val ir_to_units : ir -> AAC_matcher.ext_units - - (** {2 Building raw, natural, terms} *) - - (** [raw_constr_of_t] rebuilds a term in the raw representation, and - 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 -> AAC_coq.Relation.t -> (Term.rel_context) ->AAC_matcher.Terms.t -> Term.constr - - (** {2 Building reified terms} *) - - (** The reification environments, as Coq constrs *) - - type sigmas = { - env_sym : Term.constr; - env_bin : Term.constr; - env_units : Term.constr; (* the [idx -> X:constr] *) - } - - - - (** We need to reify two terms (left and right members of a goal) - that share the same reification envirnoment. Therefore, we need - to add letins to the proof context in order to ensure some - sharing in the proof terms we produce. - - Moreover, in order to have as much sharing as possible, we also - add letins for various partial applications that are used - throughout the terms. - - To achieve this, we decompose the reconstruction function into - two steps: first, we build the reification environment and then - reify each term successively.*) - type reifier - - val mk_reifier : AAC_coq.Relation.t -> Term.constr -> ir -> (sigmas * reifier -> Proof_type.tactic) -> Proof_type.tactic - - (** [reif_constr_of_t reifier t] rebuilds the term [t] in the - reified form. *) - val reif_constr_of_t : reifier -> AAC_matcher.Terms.t -> Term.constr - -end diff --git a/CHANGELOG b/CHANGELOG index 84b2aae..13e9a02 100644 --- a/CHANGELOG +++ b/CHANGELOG @@ -1,3 +1,8 @@ + +AAC_tactics 0.3 : +----------------- +- New release for Coq 8.4 + AAC_tactics 0.2-pl2 : ----------------- diff --git a/Caveats.v b/Caveats.v index 0d0d5ca..a7967cc 100644 --- a/Caveats.v +++ b/Caveats.v @@ -13,8 +13,6 @@ with the path to the [aac_tactics] library *) -Add Rec LoadPath "." as AAC_tactics. -Add ML Path ".". Require Import AAC. Require Instances. diff --git a/Instances.v b/Instances.v index bb309fe..8ddf9e4 100644 --- a/Instances.v +++ b/Instances.v @@ -19,7 +19,7 @@ Proof. intros x y ->. reflexivity. Qed. (* At the moment, all the instances are exported even if they are packaged into modules. Even using LocalInstances in fact*) Module Peano. - Require Import Arith NArith Max. + Require Import Arith NArith Max Min. Instance aac_plus_Assoc : Associative eq plus := plus_assoc. Instance aac_plus_Comm : Commutative eq plus := plus_comm. @@ -82,7 +82,7 @@ End Lists. Module N. - Require Import NArith Nminmax. + Require Import NArith. Open Scope N_scope. Instance aac_Nplus_Assoc : Associative eq Nplus := Nplus_assoc. Instance aac_Nplus_Comm : Commutative eq Nplus := Nplus_comm. @@ -101,13 +101,13 @@ Module N. Instance aac_zero_max : Unit eq Nmax 0 := Build_Unit eq Nmax 0 N.max_0_l N.max_0_r. (* We also provide liftings from le to eq *) - Instance preorder_le : PreOrder Nle := Build_PreOrder _ Nle N.T.le_refl N.T.le_trans. + Instance preorder_le : PreOrder Nle := Build_PreOrder _ Nle N.le_refl N.le_trans. Instance lift_le_eq : AAC_lift Nle eq := Build_AAC_lift eq_equivalence _. End N. Module P. - Require Import NArith Pminmax. + Require Import NArith. Open Scope positive_scope. Instance aac_Pplus_Assoc : Associative eq Pplus := Pplus_assoc. Instance aac_Pplus_Comm : Commutative eq Pplus := Pplus_comm. @@ -115,18 +115,18 @@ Module P. Instance aac_Pmult_Comm : Commutative eq Pmult := Pmult_comm. Instance aac_Pmult_Assoc : Associative eq Pmult := Pmult_assoc. - Instance aac_Pmin_Comm : Commutative eq Pmin := P.min_comm. - Instance aac_Pmin_Assoc : Associative eq Pmin := P.min_assoc. + Instance aac_Pmin_Comm : Commutative eq Pmin := Pos.min_comm. + Instance aac_Pmin_Assoc : Associative eq Pmin := Pos.min_assoc. - Instance aac_Pmax_Comm : Commutative eq Pmax := P.max_comm. - Instance aac_Pmax_Assoc : Associative eq Pmax := P.max_assoc. + Instance aac_Pmax_Comm : Commutative eq Pmax := Pos.max_comm. + Instance aac_Pmax_Assoc : Associative eq Pmax := Pos.max_assoc. Instance aac_one : Unit eq Pmult 1 := Build_Unit eq Pmult 1 _ Pmult_1_r. intros; reflexivity. Qed. (* TODO : add this lemma in the stdlib *) - Instance aac_one_max : Unit eq Pmax 1 := Build_Unit eq Pmax 1 P.max_1_l P.max_1_r. + Instance aac_one_max : Unit eq Pmax 1 := Build_Unit eq Pmax 1 Pos.max_1_l Pos.max_1_r. (* We also provide liftings from le to eq *) - Instance preorder_le : PreOrder Ple := Build_PreOrder _ Ple P.T.le_refl P.T.le_trans. + Instance preorder_le : PreOrder Ple := Build_PreOrder _ Ple Pos.le_refl Pos.le_trans. Instance lift_le_eq : AAC_lift Ple eq := Build_AAC_lift eq_equivalence _. End P. @@ -148,7 +148,7 @@ Module Q. Instance aac_zero_Qplus : Unit Qeq Qplus 0 := Build_Unit Qeq Qplus 0 Qplus_0_l Qplus_0_r. (* We also provide liftings from le to eq *) - Instance preorder_le : PreOrder Qle := Build_PreOrder _ Qle Q.T.le_refl Q.T.le_trans. + Instance preorder_le : PreOrder Qle := Build_PreOrder _ Qle Qle_refl Qle_trans. Instance lift_le_eq : AAC_lift Qle Qeq := Build_AAC_lift QOrderedType.QOrder.TO.eq_equiv _. End Q. diff --git a/Makefile b/Makefile index a56d4b6..1043ce9 100644 --- a/Makefile +++ b/Makefile @@ -1,319 +1,29 @@ -############################################################################# -## v # The Coq Proof Assistant ## -## .depend - -#################### -# # -# Special targets. # -# # -#################### - -.PHONY: all opt byte archclean clean install depend html - -%.cmi: %.mli - $(CAMLC) $(ZDEBUG) $(ZFLAGS) $< - -%.cmo: %.ml - $(CAMLC) $(ZDEBUG) $(ZFLAGS) $(PP) $< - -%.cmx: %.ml - $(CAMLOPTC) $(ZDEBUG) $(ZFLAGS) $(PP) $< - -%.cmxs: %.ml - $(CAMLOPTLINK) $(ZDEBUG) $(ZFLAGS) -shared -o $@ $(PP) $< - -%.cmo: %.ml4 - $(CAMLC) $(ZDEBUG) $(ZFLAGS) $(PP) -impl $< - -%.cmx: %.ml4 - $(CAMLOPTC) $(ZDEBUG) $(ZFLAGS) $(PP) -impl $< - -%.cmxs: %.ml4 - $(CAMLOPTLINK) $(ZDEBUG) $(ZFLAGS) -shared -o $@ $(PP) -impl $< - -%.ml.d: %.ml - $(CAMLBIN)ocamldep -slash $(OCAMLLIBS) $(PP) "$<" > "$@" - -%.vo %.glob: %.v - $(COQC) $(COQDEBUG) $(COQFLAGS) $* - -%.vi: %.v - $(COQC) -i $(COQDEBUG) $(COQFLAGS) $* - -%.g: %.v - $(GALLINA) $< - -%.tex: %.v - $(COQDOC) -latex $< -o $@ - -%.html: %.v %.glob - $(COQDOC) -html $< -o $@ - -%.g.tex: %.v - $(COQDOC) -latex -g $< -o $@ - -%.g.html: %.v %.glob - $(COQDOC) -html -g $< -o $@ - -%.v.d: %.v - $(COQDEP) -slash $(COQLIBS) "$<" > "$@" || ( RV=$$?; rm -f "$@"; exit $${RV} ) - -byte: - $(MAKE) all "OPT:=-byte" - -opt: - $(MAKE) all "OPT:=-opt" - -install: - mkdir -p $(COQLIB)/user-contrib - (for i in $(VOFILES); do \ - install -d `dirname $(COQLIB)/user-contrib/AAC_tactics/$$i`; \ - install $$i $(COQLIB)/user-contrib/AAC_tactics/$$i; \ - done) - (for i in $(CMOFILES); do \ - install -d `dirname $(COQLIB)/user-contrib/AAC_tactics/$$i`; \ - install $$i $(COQLIB)/user-contrib/AAC_tactics/$$i; \ - done) - (for i in $(CMIFILES); do \ - install -d `dirname $(COQLIB)/user-contrib/AAC_tactics/$$i`; \ - install $$i $(COQLIB)/user-contrib/AAC_tactics/$$i; \ - done) - (for i in $(CMXSFILES); do \ - install -d `dirname $(COQLIB)/user-contrib/AAC_tactics/$$i`; \ - install $$i $(COQLIB)/user-contrib/AAC_tactics/$$i; \ - done) - -clean: - rm -f $(CMOFILES) $(CMIFILES) $(CMXFILES) $(CMXSFILES) $(OFILES) $(VOFILES) $(VIFILES) $(GFILES) $(MLFILES:.ml=.cmo) $(MLFILES:.ml=.cmx) *~ - rm -f all.ps all-gal.ps all.pdf all-gal.pdf all.glob $(VFILES:.v=.glob) $(HTMLFILES) $(GHTMLFILES) $(VFILES:.v=.tex) $(VFILES:.v=.g.tex) $(VFILES:.v=.v.d) - rm -f $(CMOFILES) $(MLFILES:.ml=.cmi) $(MLFILES:.ml=.ml.d) $(MLFILES:.ml=.cmx) $(MLFILES:.ml=.o) - - rm -rf html - - rm -rf doc - - rm -f aac_tactics.cmxs - - rm -f aac_tactics.cmxa - - rm -f aac_tactics.cma - - rm -f .depend - -archclean: - rm -f *.cmx *.o - - -printenv: - @echo CAMLC = $(CAMLC) - @echo CAMLOPTC = $(CAMLOPTC) - @echo CAMLP4LIB = $(CAMLP4LIB) - -.dummy: magic.txt - mv -f Makefile Makefile.bak - $(COQBIN)coq_makefile -f magic.txt -o Makefile - - --include $(VFILES:.v=.v.d) -.SECONDARY: $(VFILES:.v=.v.d) - --include $(MLFILES:.ml=.ml.d) -.SECONDARY: $(MLFILES:.ml=.ml.d) - -# WARNING -# -# This Makefile has been automagically generated -# Edit at your own risks ! -# -# END OF WARNING - - - -# override inadequate coq_makefile auto-regeneration -Makefile: make_makefile magic.txt files.txt - ./make_makefile - -# We want to keep the proofs in Caveats and the Tutorial -world: $(VOFILES) doc - - mkdir -p html - $(COQDOC) -toc -utf8 -html -g $(COQDOCLIBS) -d html $(VFILES) - $(COQDOC) --no-index --no-externals -s -utf8 -html $(COQDOCLIBS) -d html Tutorial.v - $(COQDOC) --no-index --no-externals -s -utf8 -html $(COQDOCLIBS) -d html Caveats.v - -# additional dependencies for AAC (since aac_tactics.cmxs/cma are not -# around the first time we run make, coqdep issues a warning and -# ignores this dependency) -# (one can safely select one of theses dependencies according to -# coq' compilation mode--bytecode or native) -AAC.vo: aac_tactics.cmxa aac_tactics.cmxs aac_tactics.cma - -# .depend contains dependencies for .mli files --include .depend -.SECONDARY: .depend +clean:: Makefile.coq + $(MAKE) -f Makefile.coq clean + rm -f Makefile.coq .depend diff --git a/README.txt b/README.txt index ae945cc..d308f70 100644 --- a/README.txt +++ b/README.txt @@ -18,11 +18,10 @@ equations, modulo associativity and commutativity of some operators. INSTALLATION ============ -This plugin should work with Coq v8.3, as released on the 14th of -October 2010. +This plugin should work with Coq v8.4 -- run [./make_makefile] in the top-level directory to generate a Makefile -- run [make world] to build the plugin and the documentation +- running [make] in the top-level directory will generate a Makefile + (using coq_makefile), and will build the plugin and its documentation Option 1 -------- diff --git a/Tutorial.v b/Tutorial.v index 8b4c753..76006ca 100644 --- a/Tutorial.v +++ b/Tutorial.v @@ -311,7 +311,7 @@ Section Peano. can specify which equivalence relation to use by declaring instances of the [AAC_lift] type class: *) - Instance lift_le_eq : AAC_lift le eq. + Instance lift_le_eq : AAC_lift le eq := {}. (** (This instance is automatically inferred because [eq] is always a valid candidate, here for [le].) *) diff --git a/aac.mlpack b/aac.mlpack new file mode 100644 index 0000000..0c12567 --- /dev/null +++ b/aac.mlpack @@ -0,0 +1,7 @@ +Coq +Helper +Search_monad +Matcher +Theory +Print +Rewrite diff --git a/coq.ml b/coq.ml new file mode 100644 index 0000000..7371913 --- /dev/null +++ b/coq.ml @@ -0,0 +1,592 @@ +(***************************************************************************) +(* This is part of aac_tactics, it is distributed under the terms of the *) +(* GNU Lesser General Public License version 3 *) +(* (see file LICENSE for more details) *) +(* *) +(* Copyright 2009-2010: Thomas Braibant, Damien Pous. *) +(***************************************************************************) + +(** Interface with Coq *) +type constr = Term.constr + +open Term +open Names +open Coqlib + +(* The contrib name is used to locate errors when loading constrs *) +let contrib_name = "aac_tactics" + +(* 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 + +(* A clause specifying that the [let] should not try to fold anything + in the goal *) +let nowhere = + { Tacexpr.onhyps = Some []; + Tacexpr.concl_occs = Glob_term.no_occurrences_expr + } + +let cps_mk_letin + (name:string) + (c: constr) + (k : constr -> 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 (Name name) c None nowhere) in + Tacticals.tclTHEN letin (k (mkVar name)) goal + +(** {2 General functions} *) + +type goal_sigma = Proof_type.goal Tacmach.sigma +let goal_update (goal : goal_sigma) evar_map : goal_sigma= + let it = Tacmach.sig_it goal in + Tacmach.re_sig it evar_map + +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 evar_map env ty in + x,( goal_update goal em) + +let resolve_one_typeclass goal ty : constr*goal_sigma= + let env = Tacmach.pf_env goal in + let evar_map = Tacmach.project goal in + let em,c = Typeclasses.resolve_one_typeclass env evar_map ty in + c, (goal_update goal em) + +let general_error = + "Cannot resolve a typeclass : please report" + +let cps_resolve_one_typeclass ?error : Term.types -> (Term.constr -> Proof_type.tactic) -> Proof_type.tactic = fun t k goal -> + Tacmach.pf_apply + (fun env em -> let em ,c = + try Typeclasses.resolve_one_typeclass env em t + with Not_found -> + begin match error with + | None -> Util.anomaly "Cannot resolve a typeclass : please report" + | Some x -> Util.error x + end + in + Tacticals.tclTHENLIST [Refiner.tclEVARS em; k c] goal + ) goal + + +let nf_evar goal c : Term.constr= + let evar_map = Tacmach.project goal in + Evarutil.nf_evar evar_map c + +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 evar_map env x 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 evar_map env ty 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 evar_map env ty 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 em env ty in + Tacticals.tclTHENLIST [Refiner.tclEVARS em; k r] goal + ) goal + +(* decomp_term : constr -> (constr, types) kind_of_term *) +let decomp_term c = kind_of_term (strip_outer_cast c) + +let lapp c v = mkApp (Lazy.force c, v) + +(** {2 Bindings with Coq' Standard Library} *) +module Std = struct +(* Here we package the module to be able to use List, later *) + +module Pair = struct + + let path = ["Coq"; "Init"; "Datatypes"] + let typ = lazy (init_constant path "prod") + let pair = lazy (init_constant path "pair") + let of_pair t1 t2 (x,y) = + mkApp (Lazy.force pair, [| t1; t2; x ; y|] ) +end + +module Bool = struct + let path = ["Coq"; "Init"; "Datatypes"] + let typ = lazy (init_constant path "bool") + let ctrue = lazy (init_constant path "true") + let cfalse = lazy (init_constant path "false") + let of_bool b = + if b then Lazy.force ctrue else Lazy.force cfalse +end + +module Comparison = struct + let path = ["Coq"; "Init"; "Datatypes"] + let typ = lazy (init_constant path "comparison") + let eq = lazy (init_constant path "Eq") + let lt = lazy (init_constant path "Lt") + let gt = lazy (init_constant path "Gt") +end + +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|] +end + +module Option = struct + let path = ["Coq"; "Init"; "Datatypes"] + let typ = lazy (init_constant path "option") + let some = lazy (init_constant path "Some") + let none = lazy (init_constant path "None") + let some t x = mkApp (Lazy.force some, [| t ; x|]) + let none t = mkApp (Lazy.force none, [| t |]) + let of_option t x = match x with + | Some x -> some t x + | None -> none t +end + +module Pos = struct + + let path = ["Coq" ; "PArith"; "BinPos"] + let typ = lazy (init_constant path "positive") + let xI = lazy (init_constant path "xI") + let xO = lazy (init_constant path "xO") + let xH = lazy (init_constant path "xH") + + (* A coq positive from an int *) + let of_int n = + let rec aux n = + begin match n with + | n when n < 1 -> assert false + | 1 -> Lazy.force xH + | n -> mkApp + ( + (if n mod 2 = 0 + then Lazy.force xO + else Lazy.force xI + ), [| aux (n/2)|] + ) + end + in + aux n +end + +module Nat = struct + let path = ["Coq" ; "Init"; "Datatypes"] + let typ = lazy (init_constant path "nat") + let _S = lazy (init_constant path "S") + let _O = lazy (init_constant path "O") + (* A coq nat from an int *) + let of_int n = + let rec aux n = + begin match n with + | n when n < 0 -> assert false + | 0 -> Lazy.force _O + | n -> mkApp + ( + (Lazy.force _S + ), [| aux (n-1)|] + ) + end + in + aux n +end + +(** Lists from the standard library*) +module List = struct + let path = ["Coq"; "Lists"; "List"] + let typ = lazy (init_constant path "list") + let nil = lazy (init_constant path "nil") + let cons = lazy (init_constant path "cons") + let cons ty h t = + mkApp (Lazy.force cons, [| ty; h ; t |]) + let nil ty = + (mkApp (Lazy.force nil, [| ty |])) + let rec of_list ty = function + | [] -> nil ty + | t::q -> cons ty t (of_list ty q) + let type_of_list ty = + mkApp (Lazy.force typ, [|ty|]) +end + +(** Morphisms *) +module Classes = +struct + let classes_path = ["Coq";"Classes"; ] + let morphism = lazy (init_constant (classes_path@["Morphisms"]) "Proper") + let equivalence = lazy (init_constant (classes_path@ ["RelationClasses"]) "Equivalence") + let reflexive = lazy (init_constant (classes_path@ ["RelationClasses"]) "Reflexive") + let transitive = lazy (init_constant (classes_path@ ["RelationClasses"]) "Transitive") + + (** build the type [Equivalence ty rel] *) + let mk_equivalence ty rel = + mkApp (Lazy.force equivalence, [| ty; rel|]) + + + (** build the type [Reflexive ty rel] *) + let mk_reflexive ty rel = + mkApp (Lazy.force reflexive, [| ty; rel|]) + + (** build the type [Proper rel t] *) + let mk_morphism ty rel t = + mkApp (Lazy.force morphism, [| ty; rel; t|]) + + (** build the type [Transitive ty rel] *) + let mk_transitive ty rel = + mkApp (Lazy.force transitive, [| ty; rel|]) +end + +module Relation = struct + type t = + { + carrier : constr; + r : constr; + } + + let make ty r = {carrier = ty; r = r } + let split t = t.carrier, t.r +end + +module Transitive = struct + type t = + { + carrier : constr; + leq : constr; + transitive : constr; + } + let make ty leq transitive = {carrier = ty; leq = leq; transitive = transitive} + let infer goal ty leq = + let ask = Classes.mk_transitive ty leq in + let transitive , goal = resolve_one_typeclass goal ask in + make ty leq transitive, goal + let from_relation goal rlt = + infer goal (rlt.Relation.carrier) (rlt.Relation.r) + let cps_from_relation rlt k = + let ty =rlt.Relation.carrier in + let r = rlt.Relation.r in + let ask = Classes.mk_transitive ty r in + cps_resolve_one_typeclass ask + (fun trans -> k (make ty r trans) ) + let to_relation t = + {Relation.carrier = t.carrier; Relation.r = t.leq} + +end + +module Equivalence = struct + type t = + { + carrier : constr; + eq : constr; + equivalence : constr; + } + let make ty eq equivalence = {carrier = ty; eq = eq; equivalence = equivalence} + let infer goal ty eq = + let ask = Classes.mk_equivalence ty eq in + let equivalence , goal = resolve_one_typeclass goal ask in + make ty eq equivalence, goal + let from_relation goal rlt = + infer goal (rlt.Relation.carrier) (rlt.Relation.r) + let cps_from_relation rlt k = + let ty =rlt.Relation.carrier in + let r = rlt.Relation.r in + let ask = Classes.mk_equivalence ty r in + cps_resolve_one_typeclass ask (fun equiv -> k (make ty r equiv) ) + let to_relation t = + {Relation.carrier = t.carrier; Relation.r = t.eq} + let split t = + t.carrier, t.eq, t.equivalence +end +end +(**[ match_as_equation goal eqt] see [eqt] as an equation. An + optionnal rel_context can be provided to ensure taht the term + remains typable*) +let match_as_equation ?(context = Term.empty_rel_context) 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 + begin + match decomp_term equation with + | App(c,ca) when Array.length ca >= 2 -> + let n = Array.length ca in + let left = ca.(n-2) in + let right = ca.(n-1) in + let r = (mkApp (c, Array.sub ca 0 (n - 2))) in + let carrier = Typing.type_of env evar_map left in + let rlt =Std.Relation.make carrier r + in + Some (left, right, rlt ) + | _ -> None + end + + +(** {1 Tacticals} *) + +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 + r + +let tclDEBUG msg tac = fun gl -> + let _ = Pp.msgnl (Pp.str msg) in + tac gl + +let tclPRINT tac = fun gl -> + let _ = Pp.msgnl (Printer.pr_constr (Tacmach.pf_concl gl)) in + tac gl + + +(** {1 Error related mechanisms} *) +(* 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 = + Util.anomaly ("[aac_tactics] " ^ msg) + +let user_error msg = + Util.error ("[aac_tactics] " ^ msg) + +let warning msg = + Pp.msg_warning (Pp.str ("[aac_tactics]" ^ msg)) + + +(** {1 Rewriting tactics used in aac_rewrite} *) +module Rewrite = struct +(** Some informations about the hypothesis, with an (informal) + invariant: + - [typeof hyp = hyptype] + - [hyptype = forall context, body] + - [body = rel left right] + +*) + +type hypinfo = + { + hyp : Term.constr; (** the actual constr corresponding to the hypothese *) + hyptype : Term.constr; (** the type of the hypothesis *) + context : Term.rel_context; (** 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 *) + right : Term.constr; (** right hand side *) + l2r : bool; (** rewriting from left to right *) + } + +let get_hypinfo c ~l2r ?check_type (k : hypinfo -> Proof_type.tactic) : Proof_type.tactic = fun goal -> + let ctype = Tacmach.pf_type_of goal c in + 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 = Term.lookup_rel i rel_context + in f types + | _ -> 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"; + end; + begin + match match_as_equation ~context:rel_context goal body_type with + | None -> + user_error "The hypothesis is not an applied relation" + | Some (hleft,hright,hrlt) -> + k { + hyp = c; + hyptype = ctype; + body = body_type; + l2r = l2r; + context = rel_context; + rel = hrlt ; + left =hleft; + right = hright; + } + goal + end + + +(* The problem : Given a term to rewrite of type [H :forall xn ... x1, + t], we have to instanciate the subset of [xi] of type + [carrier]. [subst : (int * constr)] is the mapping the debruijn + indices in [t] to the [constrs]. We need to handle the rest of the + indexes. Two ways : + + - either using fresh evars and rewriting [H tn ?1 tn-2 ?2 ] + - either building a term like [fun 1 2 => H tn 1 tn-2 2] + + Both these terms have the same type. +*) + + +(* Fresh evars for everyone (should be the good way to do this + recompose in Coq v8.4) *) +let recompose_prod + (context : Term.rel_context) + (subst : (int * Term.constr) list) + env + em + : Evd.evar_map * Term.constr list = + (* the last index of rel relevant for the rewriting *) + let min_n = List.fold_left + (fun acc (x,_) -> min acc x) + (List.length context) subst in + let rec aux context acc em n = + let _ = Printf.printf "%i\n%!" n in + match context with + | [] -> + env, em, acc + | ((name,c,ty) as 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 em env (Term.substl acc ty) + in + (Environ.push_rel t env), em,x::acc + else + env,em,acc + in + let _,em,acc = aux context [] em 1 in + em, acc + +(* no fresh evars : instead, use a lambda abstraction around an + application to handle non-instanciated variables. *) + +let recompose_prod' + (context : Term.rel_context) + (subst : (int *Term.constr) list) + c + = + let rec popn pop n l = + if n <= 0 then l + else match l with + | [] -> [] + | t::q -> pop t :: (popn pop (n-1) q) + in + let pop_rel_decl (name,c,ty) = (name,c,Termops.pop ty) in + let rec aux sign n next app ctxt = + match sign with + | [] -> List.rev app, List.rev ctxt + | decl::sign -> + try let term = (List.assoc n subst) in + aux sign (n+1) next (term::app) (None :: ctxt) + with + | Not_found -> + let term = Term.mkRel next in + aux sign (n+1) (next+1) (term::app) (Some decl :: ctxt) + in + let app,ctxt = aux context 1 1 [] [] in + (* substitutes in the context *) + let rec update ctxt app = + match ctxt,app with + | [],_ -> [] + | _,[] -> [] + | None :: sign, _ :: app -> + None :: update sign (List.map (Termops.pop) app) + | Some decl :: sign, _ :: app -> + Some (Term.substl_decl app decl)::update sign (List.map (Termops.pop) app) + in + let ctxt = update ctxt app in + (* updates the rel accordingly, taking some care not to go to far + beyond: it is important not to lift indexes homogeneously, we + have to update *) + let rec update ctxt res n = + match ctxt with + | [] -> List.rev res + | None :: sign -> + (update (sign) (popn pop_rel_decl n res) 0) + | Some decl :: sign -> + update sign (decl :: res) (n+1) + in + let ctxt = update ctxt [] 0 in + let c = Term.applistc c (List.rev app) in + let c = Term.it_mkLambda_or_LetIn c (ctxt) in + c + +(* Version de Matthieu +let subst_rel_context k cstr ctx = + let (_, ctx') = + List.fold_left (fun (k, ctx') (id, b, t) -> (succ k, (id, Option.map + (Term.substnl [cstr] k) b, Term.substnl [cstr] k t) :: ctx')) (k, []) + ctx in List.rev ctx' + +let recompose_prod' context subst c = + let len = List.length context in + let rec aux sign n next app ctxt = + match sign with + | [] -> List.rev app, List.rev ctxt + | decl::sign -> + try let term = (List.assoc n subst) in + aux (subst_rel_context 0 term sign) (pred n) (succ next) + (term::List.map (Term.lift (-1)) app) ctxt + with Not_found -> + let term = Term.mkRel (len - next) in + aux sign (pred n) (succ next) (term::app) (decl :: ctxt) + in + let app,ctxt = aux (List.rev context) len 0 [] [] in + Term.it_mkLambda_or_LetIn (Term.applistc c(app)) (List.rev ctxt) +*) + +let build + (h : hypinfo) + (subst : (int *Term.constr) list) + (k :Term.constr -> Proof_type.tactic) + : Proof_type.tactic = fun goal -> + let c = recompose_prod' h.context subst h.hyp in + Tacticals.tclTHENLIST [k c] goal + +let build_with_evar + (h : hypinfo) + (subst : (int *Term.constr) list) + (k :Term.constr -> Proof_type.tactic) + : Proof_type.tactic + = fun goal -> + Tacmach.pf_apply + (fun env em -> + let evar_map, acc = recompose_prod h.context subst env em in + let c = Term.applistc h.hyp (List.rev acc) in + Tacticals.tclTHENLIST [Refiner.tclEVARS evar_map; k c] goal + ) goal + + +let rewrite ?(abort=false)hypinfo subst k = + build hypinfo subst + (fun rew -> + let tac = + if not abort then + Equality.general_rewrite_bindings + hypinfo.l2r + Termops.all_occurrences + true (* tell if existing evars must be frozen for instantiation *) + false + (rew,Glob_term.NoBindings) + true + else + Tacticals.tclIDTAC + in k tac + ) + + +end + +include Std diff --git a/coq.mli b/coq.mli new file mode 100644 index 0000000..a0f2ce0 --- /dev/null +++ b/coq.mli @@ -0,0 +1,231 @@ +(***************************************************************************) +(* This is part of aac_tactics, it is distributed under the terms of the *) +(* GNU Lesser General Public License version 3 *) +(* (see file LICENSE for more details) *) +(* *) +(* Copyright 2009-2010: Thomas Braibant, Damien Pous. *) +(***************************************************************************) + +(** Interface with Coq where we define some handlers for Coq's API, + and we import several definitions from Coq's standard library. + + This general purpose library could be reused by other plugins. + + Some salient points: + - we use Caml's module system to mimic Coq's one, and avoid cluttering + the namespace; + - we also provide several handlers for standard coq tactics, in + order to provide a unified setting (we replace functions that + modify the evar_map by functions that operate on the whole + goal, and repack the modified evar_map with it). + +*) + +(** {2 Getting Coq terms from the environment} *) + +val init_constant : string list -> string -> Term.constr + +(** {2 General purpose functions} *) + +type goal_sigma = Proof_type.goal Tacmach.sigma +val goal_update : goal_sigma -> Evd.evar_map -> goal_sigma +val resolve_one_typeclass : Proof_type.goal Tacmach.sigma -> Term.types -> Term.constr * goal_sigma +val cps_resolve_one_typeclass: ?error:string -> Term.types -> (Term.constr -> Proof_type.tactic) -> Proof_type.tactic +val nf_evar : goal_sigma -> Term.constr -> Term.constr +val fresh_evar :goal_sigma -> Term.types -> Term.constr* goal_sigma +val evar_unit :goal_sigma ->Term.constr -> Term.constr* goal_sigma +val evar_binary: goal_sigma -> Term.constr -> Term.constr* goal_sigma +val evar_relation: goal_sigma -> Term.constr -> Term.constr* goal_sigma +val cps_evar_relation : Term.constr -> (Term.constr -> Proof_type.tactic) -> Proof_type.tactic +(** [cps_mk_letin name v] binds the constr [v] using a letin tactic *) +val cps_mk_letin : string -> Term.constr -> ( Term.constr -> Proof_type.tactic) -> Proof_type.tactic + + +val decomp_term : Term.constr -> (Term.constr , Term.types) Term.kind_of_term +val lapp : Term.constr lazy_t -> Term.constr array -> Term.constr + +(** {2 Bindings with Coq' Standard Library} *) + +(** Coq lists *) +module List: +sig + (** [of_list ty l] *) + val of_list:Term.constr ->Term.constr list ->Term.constr + + (** [type_of_list ty] *) + val type_of_list:Term.constr ->Term.constr +end + +(** Coq pairs *) +module Pair: +sig + val typ:Term.constr lazy_t + val pair:Term.constr lazy_t + val of_pair : Term.constr -> Term.constr -> Term.constr * Term.constr -> Term.constr +end + +module Bool : sig + val typ : Term.constr lazy_t + val of_bool : bool -> Term.constr +end + + +module Comparison : sig + val typ : Term.constr lazy_t + val eq : Term.constr lazy_t + val lt : Term.constr lazy_t + val gt : Term.constr lazy_t +end + +module Leibniz : sig + val eq_refl : Term.types -> Term.constr -> Term.constr +end + +module Option : sig + val some : Term.constr -> Term.constr -> Term.constr + val none : Term.constr -> Term.constr + val of_option : Term.constr -> Term.constr option -> Term.constr +end + +(** Coq positive numbers (pos) *) +module Pos: +sig + val typ:Term.constr lazy_t + val of_int: int ->Term.constr +end + +(** Coq unary numbers (peano) *) +module Nat: +sig + val typ:Term.constr lazy_t + val of_int: int ->Term.constr +end + +(** Coq typeclasses *) +module Classes: +sig + val mk_morphism: Term.constr -> Term.constr -> Term.constr -> Term.constr + val mk_equivalence: Term.constr -> Term.constr -> Term.constr + val mk_reflexive: Term.constr -> Term.constr -> Term.constr + val mk_transitive: Term.constr -> Term.constr -> Term.constr +end + +module Relation : sig + type t = {carrier : Term.constr; r : Term.constr;} + val make : Term.constr -> Term.constr -> t + val split : t -> Term.constr * Term.constr +end + +module Transitive : sig + type t = + { + carrier : Term.constr; + leq : Term.constr; + transitive : Term.constr; + } + val make : Term.constr -> Term.constr -> Term.constr -> t + val infer : goal_sigma -> Term.constr -> Term.constr -> t * goal_sigma + val from_relation : goal_sigma -> Relation.t -> t * goal_sigma + val cps_from_relation : Relation.t -> (t -> Proof_type.tactic) -> Proof_type.tactic + val to_relation : t -> Relation.t +end + +module Equivalence : sig + type t = + { + carrier : Term.constr; + eq : Term.constr; + equivalence : Term.constr; + } + val make : Term.constr -> Term.constr -> Term.constr -> t + val infer : goal_sigma -> Term.constr -> Term.constr -> t * goal_sigma + val from_relation : goal_sigma -> Relation.t -> t * goal_sigma + val cps_from_relation : Relation.t -> (t -> Proof_type.tactic) -> Proof_type.tactic + val to_relation : t -> Relation.t + val split : t -> Term.constr * Term.constr * Term.constr +end + +(** [match_as_equation ?context goal c] try to decompose c as a + relation applied to two terms. An optionnal rel_context can be + provided to ensure that the term remains typable *) +val match_as_equation : ?context:Term.rel_context -> goal_sigma -> Term.constr -> (Term.constr * Term.constr * Relation.t) option + +(** {2 Some tacticials} *) + +(** time the execution of a tactic *) +val tclTIME : string -> Proof_type.tactic -> Proof_type.tactic + +(** emit debug messages to see which tactics are failing *) +val tclDEBUG : string -> Proof_type.tactic -> Proof_type.tactic + +(** print the current goal *) +val tclPRINT : Proof_type.tactic -> Proof_type.tactic + + +(** {2 Error related mechanisms} *) + +val anomaly : string -> 'a +val user_error : string -> 'a +val warning : string -> unit + + +(** {2 Rewriting tactics used in aac_rewrite} *) + +module Rewrite : sig + +(** The rewriting tactics used in aac_rewrite, build as handlers of the usual [setoid_rewrite]*) + + +(** {2 Datatypes} *) + +(** We keep some informations about the hypothesis, with an (informal) + invariant: + - [typeof hyp = typ] + - [typ = forall context, body] + - [body = rel left right] + +*) +type hypinfo = + { + hyp : Term.constr; (** the actual constr corresponding to the hypothese *) + hyptype : Term.constr; (** the type of the hypothesis *) + context : Term.rel_context; (** the quantifications of the hypothese *) + body : Term.constr; (** the body of the hypothese*) + rel : Relation.t; (** the relation *) + left : Term.constr; (** left hand side *) + right : Term.constr; (** right hand side *) + l2r : bool; (** rewriting from left to right *) + } + +(** [get_hypinfo H l2r ?check_type k] analyse the hypothesis H, and + build the related hypinfo, in CPS style. Moreover, an optionnal + function can be provided to check the type of every free + variable of the body of the hypothesis. *) +val get_hypinfo :Term.constr -> l2r:bool -> ?check_type:(Term.types -> bool) -> (hypinfo -> Proof_type.tactic) -> Proof_type.tactic + +(** {2 Rewriting with bindings} + + The problem : Given a term to rewrite of type [H :forall xn ... x1, + t], we have to instanciate the subset of [xi] of type + [carrier]. [subst : (int * constr)] is the mapping the De Bruijn + indices in [t] to the [constrs]. We need to handle the rest of the + indexes. Two ways : + + - either using fresh evars and rewriting [H tn ?1 tn-2 ?2 ] + - either building a term like [fun 1 2 => H tn 1 tn-2 2] + + Both these terms have the same type. +*) + +(** build the constr to rewrite, in CPS style, with lambda abstractions *) +val build : hypinfo -> (int * Term.constr) list -> (Term.constr -> Proof_type.tactic) -> Proof_type.tactic + +(** build the constr to rewrite, in CPS style, with evars *) +val build_with_evar : hypinfo -> (int * Term.constr) list -> (Term.constr -> Proof_type.tactic) -> Proof_type.tactic + +(** [rewrite ?abort hypinfo subst] builds the rewriting tactic + associated with the given [subst] and [hypinfo], and feeds it to + the given continuation. If [abort] is set to [true], we build + [tclIDTAC] instead. *) +val rewrite : ?abort:bool -> hypinfo -> (int * Term.constr) list -> (Proof_type.tactic -> Proof_type.tactic) -> Proof_type.tactic +end diff --git a/helper.ml b/helper.ml new file mode 100644 index 0000000..637def1 --- /dev/null +++ b/helper.ml @@ -0,0 +1,41 @@ +(***************************************************************************) +(* This is part of aac_tactics, it is distributed under the terms of the *) +(* GNU Lesser General Public License version 3 *) +(* (see file LICENSE for more details) *) +(* *) +(* Copyright 2009-2010: Thomas Braibant, Damien Pous. *) +(***************************************************************************) + +module type CONTROL = sig + val debug : bool + val time : bool + val printing : bool +end + +module Debug (X : CONTROL) = struct + open X + let debug x = + if debug then + Printf.printf "%s\n%!" x + + + let time f x fmt = + if time then + let t = Sys.time () in + let r = f x in + Printf.printf fmt (Sys.time () -. t); + r + else f x + + let pr_constr msg constr = + if printing then + ( Pp.msgnl (Pp.str (Printf.sprintf "=====%s====" msg)); + Pp.msgnl (Printer.pr_constr constr); + ) + + + let debug_exception msg e = + debug (msg ^ (Printexc.to_string e)) + + +end diff --git a/helper.mli b/helper.mli new file mode 100644 index 0000000..f4e4454 --- /dev/null +++ b/helper.mli @@ -0,0 +1,33 @@ +(***************************************************************************) +(* This is part of aac_tactics, it is distributed under the terms of the *) +(* GNU Lesser General Public License version 3 *) +(* (see file LICENSE for more details) *) +(* *) +(* Copyright 2009-2010: Thomas Braibant, Damien Pous. *) +(***************************************************************************) + +(** Debugging functions, that can be triggered on a per-file base. *) + +module type CONTROL = +sig + val debug : bool + val time : bool + val printing : bool +end +module Debug : + functor (X : CONTROL) -> +sig + (** {!debug} prints the string and end it with a newline *) + val debug : string -> unit + val debug_exception : string -> exn -> unit + + (** {!time} computes the time spent in a function, and then + print it using the given format *) + val time : + ('a -> 'b) -> 'a -> (float -> unit, out_channel, unit) format -> 'b + + (** {!pr_constr} print a Coq constructor, that can be labelled + by a string *) + val pr_constr : string -> Term.constr -> unit + + end diff --git a/magic.txt b/magic.txt deleted file mode 100644 index d1c9191..0000000 --- a/magic.txt +++ /dev/null @@ -1,5 +0,0 @@ --custom "mkdir -p doc; $(CAMLBIN)ocamldoc -html -rectypes -d doc -m A $(ZDEBUG) $(ZFLAGS) $^ && touch doc" "$(MLIFILES)" doc --custom "$(CAMLOPTLINK) $(ZDEBUG) $(ZFLAGS) -shared -linkall -o aac_tactics.cmxs $(CMXFILES)" "$(CMXFILES)" aac_tactics.cmxs --custom "$(CAMLOPTLINK) -g -a -o aac_tactics.cmxa $(CMXFILES)" "$(CMXFILES)" aac_tactics.cmxa --custom "$(CAMLLINK) -g -a -o aac_tactics.cma $(CMOFILES)" "$(CMOFILES)" aac_tactics.cma --custom "$(CAMLBIN)ocamldep -slash $(OCAMLLIBS) $^ > .depend" "$(MLIFILES)" .depend diff --git a/make_makefile b/make_makefile deleted file mode 100755 index 1cef3d3..0000000 --- a/make_makefile +++ /dev/null @@ -1,62 +0,0 @@ -#!/bin/sh -# - set variable MLIFILES so that it can be used in custom targets to -# build documentation and dependencies for .mli files -# - remove useless ' -I . .../plugins/ ' lines so that we can read something in the compilation log -# - rename the rule for Makefile auto-regeneration, and replace it with an appropriate command -# - patch the rule for cleaning doc -# - include the .depend custom target, to take .mli dependencies into account -# - added some hackish settings of Variables, in order to be able to install the plugin in user-contrib (coq_makefile should define a "INSTALL" variables that we can modify, instead of copying 4 times the same code in install !) - -set -e - -if [ -f `ocamlc -where`/dynlink.cmxa ]; then - BEST=opt - CMXA=aac_tactics.cmxa - CMXS=aac_tactics.cmxs -else - BEST=byte - if which ocamlopt >/dev/null; then - CMXA=aac_tactics.cmxa - fi -fi - -( -coq_makefile -R . AAC_tactics -$BEST MLIFILES = '$(MLFILES:.ml=.mli)' $(cat files.txt) -f magic.txt \ - | sed 's|.*/plugins/.*||g;s|Makefile:|\.dummy:|g;s|rm -f doc|rm -rf doc|g;s|\.opt||g' -cat < Makefile - - - -# TOTHINK: coq_makefile est bête, [make all] compile systématiquement -# les .cmxs associés à chaque module, alors que ça ne sert à rien, -# seul aac_rewrite.cmxs compte - -# problemes lorsqu'un module porte un meme nom qu'un module predefini -# (matching par exemple), prendre garde si ce probleme s'etend a la -# confusion module/nom de librairie diff --git a/matcher.ml b/matcher.ml new file mode 100644 index 0000000..55a64b7 --- /dev/null +++ b/matcher.ml @@ -0,0 +1,1293 @@ +(***************************************************************************) +(* This is part of aac_tactics, it is distributed under the terms of the *) +(* GNU Lesser General Public License version 3 *) +(* (see file LICENSE for more details) *) +(* *) +(* Copyright 2009-2010: Thomas Braibant, Damien Pous. *) +(***************************************************************************) + +(** This module defines our matching functions, modulo associativity + and commutativity (AAC). + + The basic idea is to find a substitution [env] such that the + pattern [p] instantiated by [env] is equal to [t] modulo AAC. + + We proceed by structural decomposition of the pattern, and try all + possible non-deterministic split of the subject when needed. The + function {!matcher} is limited to top-level matching, that is, the + subject must make a perfect match against the pattern ([x+x] do + not match [a+a+b] ). We use a search monad {!Search} to perform + non-deterministic splits in an almost transparent way. We also + provide a function {!subterm} for finding a match that is a + subterm modulo AAC of the subject. Therefore, we are able to solve + the aforementioned case [x+x] against [a+b+a]. + + This file is structured as follows. First, we define the search + monad. Then,we define the two representations of terms (one + representing the AST, and one in normal form ), and environments + from variables to terms. Then, we use these parts to solve + matching problem. Finally, we wrap this function {!matcher} into + {!subterm} +*) + + +module Control = +struct + let debug = false + let time = false + let printing = false +end + +module Debug = Helper.Debug (Control) +open Debug + +module Search = Search_monad (* a handle *) + +type symbol = int +type var = int +type units = (symbol * symbol) list (* from AC/A symbols to the unit *) +type ext_units = + { + unit_for : units; + is_ac : (symbol * bool) list + } + +let print_units units= + List.iter (fun (op,unit) -> Printf.printf "%i %i\t" op unit) units; + Printf.printf "\n%!" + +exception NoUnit + +let get_unit units op = + try List.assoc op units + with + | Not_found -> raise NoUnit + +let is_unit units op unit = List.mem (op,unit) units + + +open Search + +type 'a mset = ('a * int) list +let linear p = + let rec ncons t l = function + | 0 -> l + | n -> t::ncons t l (n-1) + in + let rec aux = function + [ ] -> [] + | (t,n)::q -> let q = aux q in + ncons t q n + in aux p + + + +(** The module {!Terms} defines two different types for expressions. + + - a public type {!Terms.t} that represent abstract syntax trees of + expressions with binary associative (and commutative) operators + + - a private type {!Terms.nf_term} that represent an equivalence + class for terms that are equal modulo AAC. The constructions + functions on this type ensure the property that the term is in + normal form (that is, no sum can appear as a subterm of the same + sum, no trailing units, etc...). + +*) + +module Terms : sig + + (** {1 Abstract syntax tree of terms} + + Terms represented using this datatype are representation of the + AST of an expression. *) + + type t = + Dot of (symbol * t * t) + | Plus of (symbol * t * t) + | Sym of (symbol * t array) + | Var of var + | Unit of symbol + + val equal_aac : units -> t -> t -> bool + val size: t -> int + + (** {1 Terms in normal form} + + A term in normal form is the canonical representative of the + equivalence class of all the terms that are equal modulo + Associativity and Commutativity. Outside the {!Matcher} module, + one does not need to access the actual representation of this + type. *) + + + type nf_term = private + | TAC of symbol * nf_term mset + | TA of symbol * nf_term list + | TSym of symbol * nf_term list + | TUnit of symbol + | TVar of var + + (** {2 Fresh variables: we provide some functions to pick some fresh variables with respect to a term} *) + val fresh_var_term : t -> int + val fresh_var_nfterm : nf_term -> int + + + (** {2 Constructors: we ensure that the terms are always + normalised + + braibant - Fri 27 Aug 2010, 15:11 + Moreover, we assure that we will not build empty sums or empty + products, leaving this task to the caller function. + } + *) + val mk_TAC : units -> symbol -> nf_term mset -> nf_term + val mk_TA : units -> symbol -> nf_term list -> nf_term + val mk_TSym : symbol -> nf_term list -> nf_term + val mk_TVar : var -> nf_term + val mk_TUnit : symbol -> nf_term + + (** {2 Comparisons} *) + val nf_term_compare : nf_term -> nf_term -> int + val nf_equal : nf_term -> nf_term -> bool + + (** {2 Printing function} *) + val sprint_nf_term : nf_term -> string + + (** {2 Conversion functions} *) + val term_of_t : units -> t -> nf_term + val t_of_term : nf_term -> t (* we could return the units here *) +end + = struct + + type t = + Dot of (symbol * t * t) + | Plus of (symbol * t * t) + | Sym of (symbol * t array) + | Var of var + | Unit of symbol + + let rec size = function + | Dot (_,x,y) + | Plus (_,x,y) -> size x+ size y + 1 + | Sym (_,v)-> Array.fold_left (fun acc x -> size x + acc) 1 v + | _ -> 1 + + + type nf_term = + | TAC of symbol * nf_term mset + | TA of symbol * nf_term list + | TSym of symbol * nf_term list + | TUnit of symbol + | TVar of var + + + (** {2 Picking fresh variables} *) + + (** [fresh_var_term] picks a fresh variable with respect to a term *) + let fresh_var_term t = + let rec aux = function + | Dot (_,t1,t2) + | Plus (_,t1,t2) -> max (aux t1) (aux t2) + | Sym (_,v) -> Array.fold_left (fun acc x -> max acc (aux x)) 0 v + | Var v -> assert (v >= 0); v + | Unit _ -> 0 + in + aux t + + (** [fresh_var_nfterm] picks a fresh_variable with respect to a term *) + let fresh_var_nfterm t = + let rec aux = function + | TAC (_,l) -> List.fold_left (fun acc (x,_) -> max acc (aux x)) 0 l + | TA (_,l) + | TSym (_,l) -> List.fold_left (fun acc x -> max acc (aux x)) 0 l + | TVar v -> assert (v >= 0); v + | TUnit _ -> 0 + in + aux t + + (** {2 Constructors: we ensure that the terms are always + normalised} *) + + (** {3 Pre constructors : These constructors ensure that sums and + products are not degenerated (no trailing units)} *) + let mk_TAC' units (s : symbol) l = match l with + | [] -> TUnit (get_unit units s ) + | [_,0] -> assert false + | [t,1] -> t + | _ -> TAC (s,l) + let mk_TA' units (s : symbol) l = match l with + | [] -> TUnit (get_unit units s ) + | [t] -> t + | _ -> TA (s,l) + + + (** {2 Comparison} *) + + let nf_term_compare = Pervasives.compare + let nf_equal a b = + a = b + + (** [merge_ac comp l1 l2] merges two lists of terms with coefficients + into one. Terms that are equal modulo the comparison function + [comp] will see their arities added. *) + + (* This function could be improved by the use of sorted msets *) + let merge_ac (compare : 'a -> 'a -> int) (l : 'a mset) (l' : 'a mset) : 'a mset = + let rec aux l l'= + match l,l' with + | [], _ -> l' + | _, [] -> l + | (t,tar)::q, (t',tar')::q' -> + begin match compare t t' with + | 0 -> ( t,tar+tar'):: aux q q' + | -1 -> (t, tar):: aux q l' + | _ -> (t', tar'):: aux l q' + end + in aux l l' + + (** [merge_map f l] uses the combinator [f] to combine the head of the + list [l] with the merge_maped tail of [l] *) + let rec merge_map (f : 'a -> 'b list -> 'b list) (l : 'a list) : 'b list = + match l with + | [] -> [] + | t::q -> f t (merge_map f q) + + + (** This function has to deal with the arities *) + let rec merge (l : nf_term mset) (l' : nf_term mset) : nf_term mset= + merge_ac nf_term_compare l l' + + let extract_A units s t = + match t with + | TA (s',l) when s' = s -> l + | TUnit u when is_unit units s u -> [] + | _ -> [t] + + let extract_AC units s (t,ar) : nf_term mset = + match t with + | TAC (s',l) when s' = s -> List.map (fun (x,y) -> (x,y*ar)) l + | TUnit u when is_unit units s u -> [] + | _ -> [t,ar] + + + (** {3 Constructors of {!nf_term}}*) + let mk_TAC units (s : symbol) (l : (nf_term *int) list) = + mk_TAC' units s + (merge_map (fun u l -> merge (extract_AC units s u) l) l) + let mk_TA units s l = + mk_TA' units s + (merge_map (fun u l -> (extract_A units s u) @ l) l) + let mk_TSym s l = TSym (s,l) + let mk_TVar v = TVar v + let mk_TUnit s = TUnit s + + + (** {2 Printing function} *) + let print_binary_list (single : 'a -> string) + (unit : string) + (binary : string -> string -> string) (l : 'a list) = + let rec aux l = + match l with + [] -> unit + | [t] -> single t + | t::q -> + let r = aux q in + Printf.sprintf "%s" (binary (single t) r) + in + aux l + + let print_symbol s = + match s with + | s, None -> Printf.sprintf "%i" s + | s , Some u -> Printf.sprintf "%i(unit %i)" s u + + let sprint_ac (single : 'a -> string) (l : 'a mset) = + (print_binary_list + (fun (x,t) -> + if t = 1 + then single x + else Printf.sprintf "%i*%s" t (single x) + ) + "0" + (fun x y -> x ^ " , " ^ y) + l + ) + + let print_symbol single s l = + match l with + [] -> Printf.sprintf "%i" s + | _ -> + Printf.sprintf "%i(%s)" + s + (print_binary_list single "" (fun x y -> x ^ "," ^ y) l) + + + let print_ac single s l = + Printf.sprintf "[%s:AC]{%s}" + (string_of_int s ) + (sprint_ac + single + l + ) + + let print_a single s l = + Printf.sprintf "[%s:A]{%s}" + (string_of_int s) + (print_binary_list single "1" (fun x y -> x ^ " , " ^ y) l) + + let rec sprint_nf_term = function + | TSym (s,l) -> print_symbol sprint_nf_term s l + | TAC (s,l) -> print_ac sprint_nf_term s l + | TA (s,l) -> print_a sprint_nf_term s l + | TVar v -> Printf.sprintf "x%i" v + | TUnit s -> Printf.sprintf "unit%i" s + + + + + (** {2 Conversion functions} *) + + (* rebuilds a tree out of a list, under the assumption that the list is not empty *) + let rec binary_of_list f comb l = + let l = List.rev l in + let rec aux = function + | [] -> assert false + | [t] -> f t + | t::q -> comb (aux q) (f t) + in + aux l + + let term_of_t units : t -> nf_term = + let rec term_of_t = function + | Dot (s,l,r) -> + let l = term_of_t l in + let r = term_of_t r in + mk_TA units s [l;r] + | Plus (s,l,r) -> + let l = term_of_t l in + let r = term_of_t r in + mk_TAC units s [l,1;r,1] + | Unit x -> + mk_TUnit x + | Sym (s,t) -> + let t = Array.to_list t in + let t = List.map term_of_t t in + mk_TSym s t + | Var i -> + mk_TVar ( i) + in + term_of_t + + let rec t_of_term : nf_term -> t = function + | TAC (s,l) -> + (binary_of_list + t_of_term + (fun l r -> Plus ( s,l,r)) + (linear l) + ) + | TA (s,l) -> + (binary_of_list + t_of_term + (fun l r -> Dot ( s,l,r)) + l + ) + | TSym (s,l) -> + let v = Array.of_list l in + let v = Array.map (t_of_term) v in + Sym ( s,v) + | TVar x -> Var x + | TUnit s -> Unit s + + + let equal_aac units x y = + nf_equal (term_of_t units x) (term_of_t units y) + end + + (** Terms environments defined as association lists from variables to + terms in normal form {! Terms.nf_term} *) + module Subst : sig + type t + + val find : t -> var -> Terms.nf_term option + val add : t -> var -> Terms.nf_term -> t + val empty : t + val instantiate : t -> Terms.t -> Terms.t + val sprint : t -> string + val to_list : t -> (var*Terms.t) list + end + = + struct + open Terms + + (** Terms environments, with nf_terms, to avoid costly conversions + of {!Terms.nf_terms} to {!Terms.t}, that will be mostly discarded*) + type t = (var * nf_term) list + + let find : t -> var -> nf_term option = fun t x -> + try Some (List.assoc x t) with | _ -> None + let add t x v = (x,v) :: t + let empty = [] + + let sprint (l : t) = + match l with + | [] -> Printf.sprintf "Empty environment\n" + | _ -> + let s = List.fold_left + (fun acc (x,y) -> + Printf.sprintf "%sX%i -> %s\n" + acc + x + (sprint_nf_term y) + ) + "" + (List.rev l) in + Printf.sprintf "%s\n%!" s + + + + (** [instantiate] is an homomorphism except for the variables*) + let instantiate (t: t) (x:Terms.t) : Terms.t = + let rec aux = function + | Unit _ as x -> x + | Sym (s,t) -> Sym (s,Array.map aux t) + | Plus (s,l,r) -> Plus (s, aux l, aux r) + | Dot (s,l,r) -> Dot (s, aux l, aux r) + | Var i -> + begin match find t i with + | None -> Util.error "aac_tactics: instantiate failure" + | Some x -> t_of_term x + end + in aux x + + let to_list t = List.map (fun (x,y) -> x,Terms.t_of_term y) t + end + + (******************) + (* MATCHING UTILS *) + (******************) + + open Terms + + (** Since most of the folowing functions require an extra parameter, + the units, we package them in a module. This functor will then be + applied to a module containing the units, in the exported + functions. *) + module M (X : sig + val units : units + val is_ac : (symbol * bool) list + val strict : bool (* variables cannot be instantiated with units *) + end) = struct + + open X + + let print_units ()= + List.iter (fun (op,unit) -> Printf.printf "%i %i\t" op unit) units; + Printf.printf "\n%!" + + let mk_TAC s l = mk_TAC units s l + let mk_TA s l = mk_TA units s l + let mk_TAC' s l = + try return( mk_TAC s l) + with _ -> fail () + let mk_TA' s l = + try return( mk_TA s l) + with _ -> fail () + + (** First, we need to be able to perform non-deterministic choice of + term splitting to satisfy a pattern. Indeed, we want to show that: + (x+a*b)*c <= a*b*c + *) + let a_nondet_split_raw t : ('a list * 'a list) m = + let rec aux l l' = + match l' with + | [] -> + return ( l,[]) + | t::q -> + return ( l,l' ) + >>| aux (l @ [t]) q + in + aux [] t + + (** Same as the previous [a_nondet_split], but split the list in 3 + parts *) + let a_nondet_middle t : ('a list * 'a list * 'a list) m = + a_nondet_split_raw t >> + (fun (left, right) -> + a_nondet_split_raw left >> + (fun (left, middle) -> return (left, middle, right)) + ) + + (** Non deterministic splits of ac lists *) + let dispatch f n = + let rec aux k = + if k = 0 then return (f n 0) + else return (f (n-k) k) >>| aux (k-1) + in + aux (n ) + + let add_with_arith x ar l = + if ar = 0 then l else (x,ar) ::l + + let ac_nondet_split_raw (l : 'a mset) : ('a mset * 'a mset) m = + let rec aux = function + | [] -> return ([],[]) + | (t,tar)::q -> + aux q + >> + (fun (left,right) -> + dispatch (fun arl arr -> + add_with_arith t arl left, + add_with_arith t arr right + ) + tar + ) + in + aux l + + let a_nondet_split current t : (nf_term * nf_term list) m= + a_nondet_split_raw t + >> + (fun (l,r) -> + if strict && (l=[]) + then fail() + else + mk_TA' current l >> + fun t -> return (t, r) + ) + + let ac_nondet_split current t : (nf_term * nf_term mset) m= + ac_nondet_split_raw t + >> + (fun (l,r) -> + if strict && (l=[]) + then fail() + else + mk_TAC' current l >> + fun t -> return (t, r) + ) + + + (** Try to affect the variable [x] to each left factor of [t]*) + let var_a_nondet_split env current x t = + a_nondet_split current t + >> + (fun (t,res) -> + return ((Subst.add env x t), res) + ) + + (** Try to affect variable [x] to _each_ subset of t. *) + let var_ac_nondet_split (current: symbol) env (x : var) (t : nf_term mset) : (Subst.t * (nf_term mset)) m = + ac_nondet_split current t + >> + (fun (t,res) -> + return ((Subst.add env x t), res) + ) + + (** See the term t as a given AC symbol. Unwrap the first constructor + if necessary *) + let get_AC (s : symbol) (t : nf_term) : (nf_term *int) list = + match t with + | TAC (s',l) when s' = s -> l + | TUnit u when is_unit units s u -> [] + | _ -> [t,1] + + (** See the term t as a given A symbol. Unwrap the first constructor + if necessary *) + let get_A (s : symbol) (t : nf_term) : nf_term list = + match t with + | TA (s',l) when s' = s -> l + | TUnit u when is_unit units s u -> [] + | _ -> [t] + + (** See the term [t] as an symbol [s]. Fail if it is not such + symbol. *) + let get_Sym s t = + match t with + | TSym (s',l) when s' = s -> return l + | _ -> fail () + + (*************) + (* A Removal *) + (*************) + + (** We remove the left factor v in a term list. This function runs + linearly with respect to the size of the first pattern symbol *) + + let left_factor current (v : nf_term) (t : nf_term list) = + let rec aux a b = + match a,b with + | t::q , t' :: q' when nf_equal t t' -> aux q q' + | [], q -> return q + | _, _ -> fail () + in + match v with + | TA (s,l) when s = current -> aux l t + | TUnit u when is_unit units current u -> return t + | _ -> + begin match t with + | [] -> fail () + | t::q -> + if nf_equal v t + then return q + else fail () + end + + + (**************) + (* AC Removal *) + (**************) + + (** {!pick_sym} gather all elements of a list that satisfies a + predicate, and combine them with the residual of the list. That + is, each element of the residual contains exactly one element less + than the original term. + + TODO : This function not as efficient as it could be, using a + proper data-structure *) + + let pick_sym (s : symbol) (t : nf_term mset ) = + let rec aux front back = + match back with + | [] -> fail () + | (t,tar)::q -> + begin match t with + | TSym (s',v') when s = s' -> + let back = + if tar > 1 + then (t,tar -1) ::q + else q + in + return (v' , List.rev_append front back ) + >>| aux ((t,tar)::front) q + | _ -> aux ((t,tar)::front) q + end + in + aux [] t + + + + (** We have to check if we are trying to remove a unit from a term. Could also be located in Terms*) + let is_unit_AC s t = + try nf_equal t (mk_TAC s []) + with | NoUnit -> false + + let is_same_AC s t : nf_term mset option= + match t with + TAC (s',l) when s = s' -> Some l + | _ -> None + + (** We want to remove the term [v] from the term list [t] under an AC + symbol *) + let single_AC_factor (s : symbol) (v : nf_term) v_ar (t : nf_term mset) : (nf_term mset) m = + let rec aux front back = + match back with + | [] -> fail () + | (t,tar)::q -> + begin + if nf_equal v t + then + match () with + | _ when tar < v_ar -> fail () + | _ when tar = v_ar -> return (List.rev_append front q) + | _ -> return (List.rev_append front ((t,tar-v_ar)::q)) + else + aux ((t,tar) :: front) q + end + in + if is_unit_AC s v + then + return t + else + aux [] t + + (* Remove a constant from a mset. If this constant is also a mset for + the same symbol, we remove every elements, one at a time (and we do + care of the arities) *) + let factor_AC (s : symbol) (v: nf_term) (t : nf_term mset) : ( nf_term mset ) m = + match is_same_AC s v with + | None -> single_AC_factor s v 1 t + | Some l -> + (* We are trying to remove an AC factor *) + List.fold_left (fun acc (v,v_ar) -> + acc >> (single_AC_factor s v v_ar) + ) + (return t) + l + + +(** [tri_fold f l acc] folds on the list [l] and give to f the + beginning of the list in reverse order, the considered element, and + the last part of the list + + as an exemple, on the list [1;2;3;4], we get the trace + f () [] 1 [2; 3; 4] + f () [1] 2 [3; 4] + f () [2;1] 3 [ 4] + f () [3;2;1] 4 [] + + it is the duty of the user to reverse the front if needed +*) + +let tri_fold f (l : 'a list) (acc : 'b)= match l with + [] -> acc + | _ -> + let _,_,acc = List.fold_left (fun acc (t : 'a) -> + let l,r,acc = acc in + let r = List.tl r in + t::l,r,f acc l t r + ) ([], l,acc) l + in acc + +(* let test = tri_fold (fun acc l t r -> (l,t,r) :: acc) [1;2;3;4] [] *) + + + + (*****************************) + (* ENUMERATION DES POSITIONS *) + (*****************************) + + +(** The pattern is a unit: we need to try to make it appear at each + position. We do not need to go further with a real matching, since + the match should be trivial. Hence, we proceed recursively to + enumerate all the positions. *) + +module Positions = struct + + + let ac (l: 'a mset) : ('a mset * 'a )m = + let rec aux = function + | [] -> assert false + | [t,1] -> return ([],t) + | [t,tar] -> return ([t,tar -1],t) + | (t,tar) as h :: q -> + (aux q >> (fun (c,x) -> return (h :: c,x))) + >>| (if tar > 1 then return ((t,tar-1) :: q,t) else return (q,t)) + in + aux l + + let ac' current (l: 'a mset) : ('a mset * 'a )m = + ac_nondet_split_raw l >> + (fun (l,r) -> + if l = [] || r = [] + then fail () + else + mk_TAC' current r >> + fun t -> return (l, t) + ) + + let a (l : 'a list) : ('a list * 'a * 'a list) m = + let rec aux left right : ('a list * 'a * 'a list) m = + match right with + | [] -> assert false + | [t] -> return (left,t,[]) + | t::q -> + aux (left@[t]) q + >>| return (left,t,q) + in + aux [] l +end + +let build_ac (current : symbol) (context : nf_term mset) (p : t) : t m= + if context = [] + then return p + else + mk_TAC' current context >> + fun t -> return (Plus (current,t_of_term t,p)) + +let build_a (current : symbol) + (left : nf_term list) (right : nf_term list) (p : t) : t m= + let right_pat p = + if right = [] + then return p + else + mk_TA' current right >> + fun t -> return (Dot (current,p,t_of_term t)) + in + let left_pat p= + if left = [] + then return p + else + mk_TA' current left >> + fun t -> return (Dot (current,t_of_term t,p)) + in + right_pat p >> left_pat >> (fun p -> return p) + + +let conts (hole : t) (l : symbol list) p : t m = + let p = t_of_term p in + (* - aller chercher les symboles ac et les symboles a + - construire pour chaque + * * + + / \ / \ / \ + 1 p p 1 p 1 + *) + let ac,a = List.partition (fun s -> List.assoc s is_ac) l in + let acc = fail () in + let acc = List.fold_left + (fun acc s -> + acc >>| return (Plus (s,p,hole)) + ) acc ac in + let acc = + List.fold_left + (fun acc s -> + acc >>| return (Dot (s,p,hole)) >>| return (Dot (s,hole,p)) + ) acc a + in acc + + +(** + Return the same thing as subterm : + - The size of the context + - The context + - A collection of substitutions (here == return Subst.empty) +*) +let unit_subterm (t : nf_term) (unit : symbol) (hole : t): (int * t * Subst.t m) m = + let symbols = List.fold_left + (fun acc (ac,u) -> if u = unit then ac :: acc else acc ) [] units + in + (* make a unit appear at each strict sub-position of the term*) + let rec positions (t : nf_term) : t m = + match t with + (* with a final unit at the end *) + | TAC (s,l) -> + let symbols' = List.filter (fun x -> x <> s) symbols in + ( + ac_nondet_split_raw l >> + (fun (l,r) -> if l = [] || r = [] then fail () else + ( + match r with + | [p,1] -> + positions p >>| conts hole symbols' p + | _ -> + mk_TAC' s r >> conts hole symbols' + ) >> build_ac s l )) + | TA (s,l) -> + let symbols' = List.filter (fun x -> x <> s) symbols in + ( + (* first the other symbols, and then the more simple case of + this particular symbol *) + a_nondet_middle l >> + (fun (l,m,r) -> + (* meant to break the symmetry *) + if (l = [] && r = []) + then fail () + else + ( + match m with + | [p] -> + positions p >>| conts hole symbols' p + | _ -> + mk_TA' s m >> conts hole symbols' + ) >> build_a s l r )) + >>| + ( + if List.mem s symbols then + begin match l with + | [a] -> assert false + | [a;b] -> build_a s [a] [b] (hole) + | _ -> + (* on ne construit que les elements interieurs, + d'ou la disymetrie *) + (Positions.a l >> + (fun (left,p,right) -> + if left = [] then fail () else + (build_a s left right (Dot (s,hole,t_of_term p))))) + end + else fail () + ) + + | TSym (s,l) -> + tri_fold (fun acc l t r -> + ((positions t) >> + (fun (p) -> + let l = List.map t_of_term l in + let r = List.map t_of_term r in + return (Sym (s, Array.of_list (List.rev_append l (p::r)))) )) + >>| + ( + conts hole symbols t >> + (fun (p) -> + let l = List.map t_of_term l in + let r = List.map t_of_term r in + return (Sym (s, Array.of_list (List.rev_append l (p::r)))) ) + ) + >>| acc + ) l (fail()) + | TVar x -> assert false + | TUnit x when x = unit -> return (hole) + | TUnit x as t -> conts hole symbols t + in + (positions t + >>| + (match t with + | TSym _ -> conts hole symbols t + | TAC (s,l) -> conts hole symbols t + | TA (s,l) -> conts hole symbols t + | _ -> fail()) + ) + >> fun (p) -> return (Terms.size p,p,return Subst.empty) + + + + + (************) + (* Matching *) + (************) + + + +(** {!matching} is the generic matching judgement. Each time a + non-deterministic split is made, we have to come back to this one. + + {!matchingSym} is used to match two applications that have the + same (free) head-symbol. + + {!matchingAC} is used to match two sums (with the subtlety that + [x+y] matches [f a] which is a function application or [a*b] which + is a product). + + {!matchingA} is used to match two products (with the subtlety that + [x*y] matches [f a] which is a function application, or [a+b] + which is a sum). + + +*) + +let matching : Subst.t -> nf_term -> nf_term -> Subst.t Search.m= + let rec matching env (p : nf_term) (t: nf_term) : Subst.t Search.m= + match p with + | TAC (s,l) -> + let l = linear l in + matchingAC env s l (get_AC s t) + | TA (s,l) -> + matchingA env s l (get_A s t) + | TSym (s,l) -> + (get_Sym s t) + >> (fun t -> matchingSym env l t) + | TVar x -> + begin match Subst.find env x with + | None -> return (Subst.add env x t) + | Some v -> if nf_equal v t then return env else fail () + end + | TUnit s -> + if nf_equal p t then return env else fail () + and + matchingAC (env : Subst.t) (current : symbol) (l : nf_term list) (t : (nf_term *int) list) = + match l with + | TSym (s,v):: q -> + pick_sym s t + >> (fun (v',t') -> + matchingSym env v v' + >> (fun env -> matchingAC env current q t')) + + | TAC (s,v)::q when s = current -> + assert false + | TVar x:: q -> (* This is an optimization *) + begin match Subst.find env x with + | None -> + (var_ac_nondet_split current env x t) + >> (fun (env,residual) -> matchingAC env current q residual) + | Some v -> + (factor_AC current v t) + >> (fun residual -> matchingAC env current q residual) + end + | TUnit s as v :: q -> (* this is an optimization *) + (factor_AC current v t) >> + (fun residual -> matchingAC env current q residual) + | h :: q ->(* PAC =/= curent or PA or unit for this symbol*) + (ac_nondet_split current t) + >> + (fun (t,right) -> + matching env h t + >> + ( + fun env -> + matchingAC env current q right + ) + ) + | [] -> if t = [] then return env else fail () + and + matchingA (env : Subst.t) (current : symbol) (l : nf_term list) (t : nf_term list) = + match l with + | TSym (s,v) :: l -> + begin match t with + | TSym (s',v') :: r when s = s' -> + (matchingSym env v v') + >> (fun env -> matchingA env current l r) + | _ -> fail () + end + | TA (s,v) :: l when s = current -> + assert false + | TVar x :: l -> + begin match Subst.find env x with + | None -> + debug (Printf.sprintf "var %i (%s)" x + (let b = Buffer.create 21 in List.iter (fun t -> Buffer.add_string b ( Terms.sprint_nf_term t)) t; Buffer.contents b )); + var_a_nondet_split env current x t + >> (fun (env,residual)-> debug (Printf.sprintf "pl %i %i" x(List.length residual)); matchingA env current l residual) + | Some v -> + (left_factor current v t) + >> (fun residual -> matchingA env current l residual) + end + | TUnit s as v :: q -> (* this is an optimization *) + (left_factor current v t) >> + (fun residual -> matchingA env current q residual) + | h :: l -> + a_nondet_split current t + >> (fun (t,r) -> + matching env h t + >> (fun env -> matchingA env current l r) + ) + | [] -> if t = [] then return env else fail () + and + matchingSym (env : Subst.t) (l : nf_term list) (t : nf_term list) = + List.fold_left2 + (fun acc p t -> acc >> (fun env -> matching env p t)) + (return env) + l + t + + in + fun env l r -> + let _ = debug (Printf.sprintf "pattern :%s\nterm :%s\n%!" (Terms.sprint_nf_term l) (Terms.sprint_nf_term r)) in + let m = matching env l r in + let _ = debug (Printf.sprintf "count %i" (Search.count m)) in + m + + +(** [unitifiable p : Subst.t m] *) +let unitifiable p : (symbol * Subst.t m) m = + let m = List.fold_left + (fun acc (_,unit) -> acc >>| + let m = matching Subst.empty p (mk_TUnit unit) in + if Search.is_empty m then + fail () + else + begin + return (unit,m) + end + ) (fail ()) units + in + m +;; + +let nullifiable p = + let nullable = not strict in + let has_unit s = + try let _ = get_unit units s in true + with NoUnit -> false + in + let rec aux = function + | TA (s,l) -> has_unit s && List.for_all (aux) l + | TAC (s,l) -> has_unit s && List.for_all (fun (x,n) -> aux x) l + | TSym _ -> false + | TVar _ -> nullable + | TUnit _ -> true + in aux p + +let unit_warning p ~nullif ~unitif = + assert ((Search.is_empty unitif) || nullif); + if not (Search.is_empty unitif) + then + begin + Pp.msg_warning + (Pp.str + "[aac_tactics] This pattern can be instanciated to match units, some solutions can be missing"); + end + +;; + + + + +(***********) +(* Subterm *) +(***********) + + + +(** [subterm] solves a sub-term pattern matching. + + This function is more high-level than {!matcher}, thus takes {!t} + as arguments rather than terms in normal form {!nf_term}. + + We use three mutually recursive functions {!subterm}, + {!subterm_AC}, {!subterm_A} to find the matching subterm, making + non-deterministic choices to split the term into a context and an + intersting sub-term. Intuitively, the only case in which we have to + go in depth is when we are left with a sub-term that is atomic. + + Indeed, rewriting [H: b = c |- a+b+a = a+a+c], we do not want to + find recursively the sub-terms of [a+b] and [b+a], since they will + overlap with the sub-terms of [a+b+a]. + + We rebuild the context on the fly, leaving the variables in the + pattern uninstantiated. We do so in order to allow interaction + with the user, to choose the env. + + Strange patterms like x*y*x can be instanciated by nothing, inside + a product. Therefore, we need to check that all the term is not + going into the context. With proper support for interaction with + the user, we should lift these tests. However, at the moment, they + serve as heuristics to return "interesting" matchings +*) + + let return_non_empty raw_p m = + if is_empty m + then + fail () + else + return (raw_p ,m) + + let subterm (raw_p:t) (raw_t:t): (int * t * Subst.t m) m= + let _ = debug (String.make 40 '=') in + let p = term_of_t units raw_p in + let t = term_of_t units raw_t in + let nullif = nullifiable p in + let unitif = unitifiable p in + let _ = unit_warning p ~nullif ~unitif in + let _ = debug (Printf.sprintf "%s" (Terms.sprint_nf_term p)) in + let _ = debug (Printf.sprintf "%s" (Terms.sprint_nf_term t)) in + let filter_right current right (p,m) = + if right = [] + then return (p,m) + else + mk_TAC' current right >> + fun t -> return (Plus (current,p,t_of_term t),m) + in + let filter_middle current left right (p,m) = + let right_pat p = + if right = [] + then return p + else + mk_TA' current right >> + fun t -> return (Dot (current,p,t_of_term t)) + in + let left_pat p= + if left = [] + then return p + else + mk_TA' current left >> + fun t -> return (Dot (current,t_of_term t,p)) + in + right_pat p >> left_pat >> (fun p -> return (p,m)) + in + let rec subterm (t:nf_term) : (t * Subst.t m) m= + match t with + | TAC (s,l) -> + ((ac_nondet_split_raw l) >> + (fun (left,right) -> + (subterm_AC s left) >> (filter_right s right) + )) + | TA (s,l) -> + (a_nondet_middle l) >> + (fun (left, middle, right) -> + (subterm_A s middle) >> + (filter_middle s left right) + ) + | TSym (s, l) -> + let init = + return_non_empty raw_p (matching Subst.empty p t) + in + tri_fold (fun acc l t r -> + ((subterm t) >> + (fun (p,m) -> + let l = List.map t_of_term l in + let r = List.map t_of_term r in + let p = Sym (s, Array.of_list (List.rev_append l (p::r))) in + return (p,m) + )) >>| acc + ) l init + | TVar x -> assert false + (* this case is superseded by the later disjunction *) + | TUnit s -> fail () + + and subterm_AC s tl = + match tl with + [x,1] -> subterm x + | _ -> + mk_TAC' s tl >> fun t -> + return_non_empty raw_p (matching Subst.empty p t) + and subterm_A s tl = + match tl with + [x] -> subterm x + | _ -> + mk_TA' s tl >> + fun t -> + return_non_empty raw_p (matching Subst.empty p t) + in + match p with + | TUnit unit -> unit_subterm t unit raw_p + | _ when not (Search.is_empty unitif) -> + let unit_matches = + Search.fold + (fun (unit,inst) acc -> + Search.fold + (fun subst acc' -> + let m = unit_subterm t unit (Subst.instantiate subst raw_p) + in + m>>| acc' + ) + inst + acc + ) + unitif + (fail ()) + in + let nullifies (t : Subst.t) = + List.for_all (fun (_,x) -> + List.exists (fun (_,y) -> Unit y = x ) units + ) (Subst.to_list t) + in + let nonunit_matches = + subterm t >> + ( + fun (p,m) -> + let m = Search.filter (fun subst -> not( nullifies subst)) m in + if Search.is_empty m + then fail () + else return (Terms.size p,p,m) + ) + in + unit_matches >>| nonunit_matches + + | _ -> (subterm t >> fun (p,m) -> return (Terms.size p,p,m)) + + + end + + +(* The functions we export, handlers for the previous ones. Some debug + information also *) +let subterm ?(strict = false) units raw t = + let module M = M (struct + let is_ac = units.is_ac + let units = units.unit_for + let strict = strict + end) in + let sols = time (M.subterm raw) t "%fs spent in subterm (including matching)\n" in + debug + (Printf.sprintf "%i possible solution(s)\n" + (Search.fold (fun (_,_,envm) acc -> count envm + acc) sols 0)); + sols + + +let matcher ?(strict = false) units p t = + let module M = M (struct + let is_ac = units.is_ac + let units = units.unit_for + let strict = false + end) in + let units = units.unit_for in + let sols = time + (fun (p,t) -> + let p = (Terms.term_of_t units p) in + let t = (Terms.term_of_t units t) in + M.matching Subst.empty p t) (p,t) + "%fs spent in the matcher\n" + in + debug (Printf.sprintf "%i solutions\n" (count sols)); + sols + diff --git a/matcher.mli b/matcher.mli new file mode 100644 index 0000000..a6b6f46 --- /dev/null +++ b/matcher.mli @@ -0,0 +1,189 @@ +(***************************************************************************) +(* This is part of aac_tactics, it is distributed under the terms of the *) +(* GNU Lesser General Public License version 3 *) +(* (see file LICENSE for more details) *) +(* *) +(* Copyright 2009-2010: Thomas Braibant, Damien Pous. *) +(***************************************************************************) + +(** Standalone module containing the algorithm for matching modulo + associativity and associativity and commutativity + (AAC). Additionnaly, some A or AC operators can have units (U). + + This module could be reused outside of the Coq plugin. + + Matching a pattern [p] against a term [t] modulo AACU boils down + to finding a substitution [env] such that the pattern [p] + instantiated with [env] is equal to [t] modulo AACU. + + We proceed by structural decomposition of the pattern, trying all + possible non-deterministic splittings of the subject, when needed. The + function {!matcher} is limited to top-level matching, that is, the + subject must make a perfect match against the pattern ([x+x] does + not match [a+a+b] ). + + We use a search monad {!Search_monad} to perform non-deterministic + choices in an almost transparent way. + + We also provide a function {!subterm} for finding a match that is + a subterm of the subject modulo AACU. In particular, this function + gives a solution to the aforementioned case ([x+x] against + [a+b+a]). + + On a slightly more involved level : + - it must be noted that we allow several AC/A operators to share + the same units, but that a given AC/A operator can have at most + one unit. + + - if the pattern does not contain "hard" symbols (like constants, + function symbols, AC or A symbols without units), there can be + infinitely many subterms such that the pattern matches: it is + possible to build "subterms" modulo AAC and U that make the size + of the term increase (by making neutral elements appear in a + layered fashion). Hence, in this case, a warning is issued, and + some solutions are omitted. + +*) + +(** {2 Utility functions} *) + +type symbol = int +type var = int + +(** Relationship between units and operators. This is a sparse + representation of a matrix of couples [(op,unit)] where [op] is + the index of the operation, and [unit] the index of the relevant + unit. We make the assumption that any operation has 0 or 1 unit, + and that operations can share a unit). *) + +type units =(symbol * symbol) list (* from AC/A symbols to the unit *) +type ext_units = + { + unit_for : units; (* from AC/A symbols to the unit *) + is_ac : (symbol * bool) list + } + + +(** The arguments of sums (or AC operators) are represented using finite multisets. + (Typically, [a+b+a] corresponds to [2.a+b], i.e. [Sum[a,2;b,1]]) *) +type 'a mset = ('a * int) list + +(** [linear] expands a multiset into a simple list *) +val linear : 'a mset -> 'a list + +(** Representations of expressions + + The module {!Terms} defines two different types for expressions. + - a public type {!Terms.t} that represents abstract syntax trees + of expressions with binary associative and commutative operators + - a private type {!Terms.nf_term}, corresponding to a canonical + representation for the above terms modulo AACU. The construction + functions on this type ensure that these terms are in normal form + (that is, no sum can appear as a subterm of the same sum, no + trailing units, lists corresponding to multisets are sorted, + etc...). + +*) +module Terms : +sig + + (** {2 Abstract syntax tree of terms and patterns} + + We represent both terms and patterns using the following datatype. + + Values of type [symbol] are used to index symbols. Typically, + given two associative operations [(^)] and [( * )], and two + morphisms [f] and [g], the term [f (a^b) (a*g b)] is represented + by the following value + [Sym(0,[| Dot(1, Sym(2,[||]), Sym(3,[||])); + Dot(4, Sym(2,[||]), Sym(5,[|Sym(3,[||])|])) |])] + where the implicit symbol environment associates + [f] to [0], [(^)] to [1], [a] to [2], [b] to [3], [( * )] to [4], and [g] to [5], + + Accordingly, the following value, that contains "variables" + [Sym(0,[| Dot(1, Var x, Unit (1); Dot(4, Var x, + Sym(5,[|Sym(3,[||])|])) |])] represents the pattern [forall x, f + (x^1) (x*g b)]. The relationship between [1] and [( * )] is only + mentionned in the units table. *) + + type t = + Dot of (symbol * t * t) + | Plus of (symbol * t * t) + | Sym of (symbol * t array) + | Var of var + | Unit of symbol + + (** Test for equality of terms modulo AACU (relies on the following + canonical representation of terms). Note than two different + units of a same operator are not considered equal. *) + val equal_aac : units -> t -> t -> bool + + + (** {2 Normalised terms (canonical representation) } + + A term in normal form is the canonical representative of the + equivalence class of all the terms that are equal modulo AACU. + This representation is only used internally; it is exported here + for the sake of completeness *) + + type nf_term + + (** {3 Comparisons} *) + + val nf_term_compare : nf_term -> nf_term -> int + val nf_equal : nf_term -> nf_term -> bool + + (** {3 Printing function} *) + + val sprint_nf_term : nf_term -> string + + (** {3 Conversion functions} *) + + (** we have the following property: [a] and [b] are equal modulo AACU + iif [nf_equal (term_of_t a) (term_of_t b) = true] *) + val term_of_t : units -> t -> nf_term + val t_of_term : nf_term -> t + +end + + +(** Substitutions (or environments) + + The module {!Subst} contains infrastructure to deal with + substitutions, i.e., functions from variables to terms. Only a + restricted subsets of these functions need to be exported. + + As expected, a particular substitution can be used to + instantiate a pattern. +*) +module Subst : +sig + type t + val sprint : t -> string + val instantiate : t -> Terms.t-> Terms.t + val to_list : t -> (var*Terms.t) list +end + + +(** {2 Main functions exported by this module} *) + +(** [matcher p t] computes the set of solutions to the given top-level + matching problem ([p] is the pattern, [t] is the term). If the + [strict] flag is set, solutions where units are used to + instantiate some variables are excluded, unless this unit appears + directly under a function symbol (e.g., f(x) still matches f(1), + while x+x+y does not match a+b+c, since this would require to + assign 1 to x). +*) +val matcher : ?strict:bool -> ext_units -> Terms.t -> Terms.t -> Subst.t Search_monad.m + +(** [subterm p t] computes a set of solutions to the given + subterm-matching problem. + + Return a collection of possible solutions (each with the + associated depth, the context, and the solutions of the matching + problem). The context is actually a {!Terms.t} where the variables + are yet to be instantiated by one of the associated substitutions +*) +val subterm : ?strict:bool -> ext_units -> Terms.t -> Terms.t -> (int * Terms.t * Subst.t Search_monad.m) Search_monad.m + diff --git a/print.ml b/print.ml new file mode 100644 index 0000000..1ceb786 --- /dev/null +++ b/print.ml @@ -0,0 +1,100 @@ +(***************************************************************************) +(* This is part of aac_tactics, it is distributed under the terms of the *) +(* GNU Lesser General Public License version 3 *) +(* (see file LICENSE for more details) *) +(* *) +(* Copyright 2009-2010: Thomas Braibant, Damien Pous. *) +(***************************************************************************) + +(* A very basic way to interact with the envs, to choose a possible + solution *) +open Pp +open Matcher +type named_env = (Names.name * Terms.t) list + + + +(** {pp_env} prints a substitution mapping names to terms, using the +provided printer *) +let pp_env pt : named_env -> Pp.std_ppcmds = fun env -> + List.fold_left + (fun acc (v,t) -> + begin match v with + | Names.Name s -> str (Printf.sprintf "%s: " (Names.string_of_id s)) + | Names.Anonymous -> str ("_") + end + ++ pt t ++ str "; " ++ acc + ) + (str "") + env + +(** {pp_envm} prints a collection of possible environments, and number +them. This number must remain compatible with the parameters given to +{!aac_rewrite} *) +let pp_envm pt : named_env Search_monad.m -> Pp.std_ppcmds = fun m -> + let _,s = + Search_monad.fold + (fun env (n,acc) -> + n+1, h 0 (str (Printf.sprintf "%i:\t[" n) ++pp_env pt env ++ str "]") ++ fnl () :: acc + ) m (0,[]) + in + List.fold_left (fun acc s -> s ++ acc) (str "") (s) + +let trivial_substitution envm = + match Search_monad.choose envm with + | None -> true (* assert false *) + | Some l -> l=[] + +(** {pp_all} prints a collection of possible contexts and related +possibles substitutions, giving a number to each. This number must +remain compatible with the parameters of {!aac_rewrite} *) +let pp_all pt : (int * Terms.t * named_env Search_monad.m) Search_monad.m -> Pp.std_ppcmds = fun m -> + let _,s = Search_monad.fold + (fun (size,context,envm) (n,acc) -> + let s = str (Printf.sprintf "occurence %i: transitivity through " n) in + let s = s ++ pt context ++ str "\n" in + let s = if trivial_substitution envm then s else + s ++ str (Printf.sprintf "%i possible(s) substitution(s)" (Search_monad.count envm) ) + ++ fnl () ++ pp_envm pt envm + in + n+1, s::acc + ) m (0,[]) in + List.fold_left (fun acc s -> s ++ str "\n" ++ acc) (str "") (s) + +(** The main printing function. {!print} uses the debruijn_env the +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 : Term.rel_context) 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 m = Search_monad.(>>) m + (fun (i,t,envm) -> + let envm = Search_monad.(>>) envm ( fun env -> + let l = Matcher.Subst.to_list env in + let l = List.sort (fun (n,_) (n',_) -> Pervasives.compare n n') l in + let l = + List.map (fun (v,t) -> + let (name,body,types) = Term.lookup_rel v context in + (name,t) + ) l + in + Search_monad.return l + ) + in + Search_monad.return (i,t,envm) + ) + in + let m = Search_monad.sort (fun (x,_,_) (y,_,_) -> x - y) m in + let _ = Pp.msgnl + (pp_all + (fun t -> Printer.pr_constr (Theory.Trans.raw_constr_of_t ir rlt context t) ) m + ) + in + Tacticals.tclIDTAC goal + diff --git a/print.mli b/print.mli new file mode 100644 index 0000000..5b3dc15 --- /dev/null +++ b/print.mli @@ -0,0 +1,23 @@ +(***************************************************************************) +(* This is part of aac_tactics, it is distributed under the terms of the *) +(* GNU Lesser General Public License version 3 *) +(* (see file LICENSE for more details) *) +(* *) +(* Copyright 2009-2010: Thomas Braibant, Damien Pous. *) +(***************************************************************************) + +(** Pretty printing functions we use for the aac_instances + tactic. *) + + +(** The main printing function. {!print} uses the [Term.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.*) +val print : + Coq.Relation.t -> + Theory.Trans.ir -> + (int * Matcher.Terms.t * Matcher.Subst.t Search_monad.m) Search_monad.m -> + Term.rel_context -> + Proof_type.tactic + diff --git a/rewrite.ml4 b/rewrite.ml4 new file mode 100644 index 0000000..6229262 --- /dev/null +++ b/rewrite.ml4 @@ -0,0 +1,524 @@ +(***************************************************************************) +(* This is part of aac_tactics, it is distributed under the terms of the *) +(* GNU Lesser General Public License version 3 *) +(* (see file LICENSE for more details) *) +(* *) +(* Copyright 2009-2010: Thomas Braibant, Damien Pous. *) +(***************************************************************************) + +(** aac_rewrite -- rewriting modulo *) + + +module Control = struct + let debug = false + let printing = false + let time = false +end + +module Debug = Helper.Debug (Control) +open Debug + +let time_tac msg tac = + if Control.time then Coq.tclTIME msg tac else tac + +let tac_or_exn tac exn msg = fun gl -> + try tac gl with e -> + pr_constr "last goal" (Tacmach.pf_concl gl); + exn msg e + +(* 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 + | Util.Anomaly _ as e -> raise e + | _ -> Coq.anomaly msg + +module M = Matcher + +open Term +open Names +open Coqlib +open Proof_type + +(** The various kind of relation we can encounter, as a hierarchy *) +type rew_relation = + | Bare of Coq.Relation.t + | Transitive of Coq.Transitive.t + | Equivalence of Coq.Equivalence.t + +(** {!promote try to go higher in the aforementionned hierarchy} *) +let promote (rlt : Coq.Relation.t) (k : rew_relation -> Proof_type.tactic) = + try Coq.Equivalence.cps_from_relation rlt + (fun e -> k (Equivalence e)) + with + | Not_found -> + begin + try Coq.Transitive.cps_from_relation rlt + (fun trans -> k (Transitive trans)) + with + |Not_found -> k (Bare rlt) + end + + +(* + Various situations: + p == q |- left == right : rewrite <- -> + p <= q |- left <= right : rewrite -> + p <= q |- left == right : failure + p == q |- left <= right : rewrite <- -> + + Not handled + p <= q |- left >= right : failure +*) + +(** aac_lift : the ideal type beyond AAC.v/Lift + + A base relation r, together with an equivalence relation, and the + proof that the former lifts to the later. Howver, we have to + ensure manually the invariant : r.carrier == e.carrier, and that + lift connects the two things *) +type aac_lift = + { + r : Coq.Relation.t; + e : Coq.Equivalence.t; + lift : Term.constr + } + +type rewinfo = + { + hypinfo : Coq.Rewrite.hypinfo; + + in_left : bool; (** are we rewriting in the left hand-sie of the goal *) + pattern : constr; + subject : constr; + morph_rlt : Coq.Relation.t; (** the relation we look for in morphism *) + eqt : Coq.Equivalence.t; (** the equivalence we use as workbase *) + rlt : Coq.Relation.t; (** the relation in the goal *) + lifting: aac_lift + } + +let infer_lifting (rlt: Coq.Relation.t) (k : lift:aac_lift -> Proof_type.tactic) : Proof_type.tactic = + Coq.cps_evar_relation rlt.Coq.Relation.carrier (fun e -> + let lift_ty = + mkApp (Lazy.force Theory.Stubs.lift, + [| + rlt.Coq.Relation.carrier; + rlt.Coq.Relation.r; + e + |] + ) in + Coq.cps_resolve_one_typeclass ~error:"Cannot infer a lifting" + lift_ty (fun lift goal -> + let x = rlt.Coq.Relation.carrier in + let r = rlt.Coq.Relation.r in + let eq = (Coq.nf_evar goal e) in + let equiv = Coq.lapp Theory.Stubs.lift_proj_equivalence [| x;r;eq; lift |] in + let lift = + { + r = rlt; + e = Coq.Equivalence.make x eq equiv; + lift = lift; + } + in + k ~lift:lift goal + )) + +(** Builds a rewinfo, once and for all *) +let dispatch in_left (left,right,rlt) hypinfo (k: rewinfo -> Proof_type.tactic ) : Proof_type.tactic= + let l2r = hypinfo.Coq.Rewrite.l2r in + infer_lifting rlt + (fun ~lift -> + let eq = lift.e in + k { + hypinfo = hypinfo; + in_left = in_left; + pattern = if l2r then hypinfo.Coq.Rewrite.left else hypinfo.Coq.Rewrite.right; + subject = if in_left then left else right; + morph_rlt = Coq.Equivalence.to_relation eq; + eqt = eq; + lifting = lift; + rlt = rlt + } + ) + + + +(** {1 Tactics} *) + + +(** Build the reifiers, the reified terms, and the evaluation fonction *) +let handle eqt zero envs (t : Matcher.Terms.t) (t' : Matcher.Terms.t) k = + + let (x,r,_) = Coq.Equivalence.split eqt in + Theory.Trans.mk_reifier (Coq.Equivalence.to_relation eqt) zero envs + (fun (maps, reifier) -> + (* fold through a term and reify *) + let t = Theory.Trans.reif_constr_of_t reifier t in + let t' = Theory.Trans.reif_constr_of_t reifier t' in + (* Some letins *) + let eval = (mkApp (Lazy.force Theory.Stubs.eval, [|x;r; maps.Theory.Trans.env_sym; maps.Theory.Trans.env_bin; maps.Theory.Trans.env_units|])) in + + Coq.cps_mk_letin "eval" eval (fun eval -> + Coq.cps_mk_letin "left" t (fun t -> + Coq.cps_mk_letin "right" t' (fun t' -> + k maps eval t t')))) + +(** [by_aac_reflexivity] is a sub-tactic that closes a sub-goal that + is merely a proof of equality of two terms modulo AAC *) +let by_aac_reflexivity zero + eqt envs (t : Matcher.Terms.t) (t' : Matcher.Terms.t) : Proof_type.tactic = + handle eqt zero envs t t' + (fun maps eval t t' -> + let (x,r,e) = Coq.Equivalence.split eqt in + let decision_thm = Coq.lapp Theory.Stubs.decide_thm + [|x;r;e; + maps.Theory.Trans.env_sym; + maps.Theory.Trans.env_bin; + maps.Theory.Trans.env_units; + t;t'; + |] + in + (* This convert is required to deal with evars in a proper + way *) + let convert_to = mkApp (r, [| mkApp (eval,[| t |]); mkApp (eval, [|t'|])|]) in + let convert = Tactics.convert_concl convert_to Term.VMcast in + let apply_tac = Tactics.apply decision_thm in + (Tacticals.tclTHENLIST + [ + 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"; + Tacticals.tclORELSE Tactics.reflexivity + (Tacticals.tclFAIL 0 (Pp.str "Not an equality modulo A/AC")) + ]) + ) + +let by_aac_normalise zero lift ir t t' = + let eqt = lift.e in + let rlt = lift.r in + handle eqt zero ir t t' + (fun maps eval t t' -> + let (x,r,e) = Coq.Equivalence.split eqt in + let normalise_thm = Coq.lapp Theory.Stubs.lift_normalise_thm + [|x;r;e; + maps.Theory.Trans.env_sym; + maps.Theory.Trans.env_bin; + maps.Theory.Trans.env_units; + rlt.Coq.Relation.r; + lift.lift; + t;t'; + |] + in + (* This convert is required to deal with evars in a proper + way *) + let convert_to = mkApp (rlt.Coq.Relation.r, [| mkApp (eval,[| t |]); mkApp (eval, [|t'|])|]) in + let convert = Tactics.convert_concl convert_to Term.VMcast in + let apply_tac = Tactics.apply normalise_thm in + (Tacticals.tclTHENLIST + [ + convert ; + apply_tac; + ]) + + ) + +(** A handler tactic, that reifies the goal, and infer the liftings, + and then call its continuation *) +let aac_conclude + (k : Term.constr -> aac_lift -> Theory.Trans.ir -> Matcher.Terms.t -> Matcher.Terms.t -> Proof_type.tactic) = fun goal -> + + let (equation : Term.types) = Tacmach.pf_concl goal in + let envs = Theory.Trans.empty_envs () in + let left, right,r = + match Coq.match_as_equation goal equation with + | None -> Coq.user_error "The goal is not an applied relation" + | Some x -> x in + try infer_lifting r + (fun ~lift goal -> + let eq = Coq.Equivalence.to_relation lift.e in + let tleft,tright, goal = Theory.Trans.t_of_constr goal eq envs (left,right) in + let goal, ir = Theory.Trans.ir_of_envs goal eq envs in + let concl = Tacmach.pf_concl goal in + let _ = pr_constr "concl "concl in + let evar_map = Tacmach.project goal in + Tacticals.tclTHEN + (Refiner.tclEVARS evar_map) + (k left lift ir tleft tright) + goal + )goal + with + | Not_found -> Coq.user_error "No lifting from the goal's relation to an equivalence" + +open Libnames +open Tacinterp + +let aac_normalise = fun goal -> + let ids = Tacmach.pf_ids_of_hyps goal in + Tacticals.tclTHENLIST + [ + aac_conclude by_aac_normalise; + 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 + >> + ); + Tactics.keep ids + ] goal + +let aac_reflexivity = fun goal -> + aac_conclude + (fun zero lift ir t t' -> + let x,r = Coq.Relation.split (lift.r) in + let r_reflexive = (Coq.Classes.mk_reflexive x r) in + Coq.cps_resolve_one_typeclass ~error:"The goal's relation is not reflexive" + r_reflexive + (fun reflexive -> + let lift_reflexivity = + mkApp (Lazy.force (Theory.Stubs.lift_reflexivity), + [| + x; + r; + lift.e.Coq.Equivalence.eq; + lift.lift; + reflexive + |]) + in + Tacticals.tclTHEN + (Tactics.apply lift_reflexivity) + (fun goal -> + let concl = Tacmach.pf_concl goal in + let _ = pr_constr "concl "concl in + by_aac_reflexivity zero lift.e ir t t' goal) + ) + ) goal + +(** A sub-tactic to lift the rewriting using Lift *) +let lift_transitivity in_left (step:constr) preorder lifting (using_eq : Coq.Equivalence.t): tactic = + fun goal -> + (* catch the equation and the two members*) + let concl = Tacmach.pf_concl goal in + let (left, right, _ ) = match Coq.match_as_equation goal concl with + | Some x -> x + | None -> Coq.user_error "The goal is not an equation" + in + let lift_transitivity = + let thm = + if in_left + then + Lazy.force Theory.Stubs.lift_transitivity_left + else + Lazy.force Theory.Stubs.lift_transitivity_right + in + mkApp (thm, + [| + preorder.Coq.Relation.carrier; + preorder.Coq.Relation.r; + using_eq.Coq.Equivalence.eq; + lifting; + step; + left; + right; + |]) + in + Tacticals.tclTHENLIST + [ + Tactics.apply lift_transitivity + ] goal + + +(** The core tactic for aac_rewrite *) +let core_aac_rewrite ?abort + rewinfo + subst + (by_aac_reflexivity : Matcher.Terms.t -> Matcher.Terms.t -> Proof_type.tactic) + (tr : constr) t left : tactic = + pr_constr "transitivity through" tr; + let tran_tac = + lift_transitivity rewinfo.in_left tr rewinfo.rlt rewinfo.lifting.lift rewinfo.eqt + in + Coq.Rewrite.rewrite ?abort rewinfo.hypinfo subst (fun rew -> + Tacticals.tclTHENSV + (tac_or_exn (tran_tac) Coq.anomaly "Unable to make the transitivity step") + ( + if rewinfo.in_left + then [| by_aac_reflexivity left t ; rew |] + else [| by_aac_reflexivity t left ; rew |] + ) + ) + +exception NoSolutions + + +(** Choose a substitution from a + [(int * Terms.t * Env.env Search_monad.m) Search_monad.m ] *) +(* WARNING: Beware, since the printing function can change the order of the + printed monad, this function has to be updated accordingly *) +let choose_subst subterm sol m= + try + let (depth,pat,envm) = match subterm with + | None -> (* first solution *) + List.nth ( List.rev (Search_monad.to_list m)) 0 + | Some x -> + List.nth ( List.rev (Search_monad.to_list m)) x + in + let env = match sol with + None -> + List.nth ( (Search_monad.to_list envm)) 0 + | Some x -> List.nth ( (Search_monad.to_list envm)) x + in + pat, env + with + | _ -> raise NoSolutions + +(** rewrite the constr modulo AC from left to right in the left member + of the goal *) +let aac_rewrite ?abort rew ?(l2r=true) ?(show = false) ?(in_left=true) ?strict ~occ_subterm ~occ_sol ?extra : Proof_type.tactic = fun goal -> + let envs = Theory.Trans.empty_envs () in + let (concl : Term.types) = Tacmach.pf_concl goal in + let (_,_,rlt) as concl = + match Coq.match_as_equation goal concl with + | None -> Coq.user_error "The goal is not an applied relation" + | Some (left, right, rlt) -> left,right,rlt + in + let check_type x = + Tacmach.pf_conv_x goal x rlt.Coq.Relation.carrier + in + Coq.Rewrite.get_hypinfo rew ~l2r ?check_type:(Some check_type) + (fun hypinfo -> + dispatch in_left concl hypinfo + ( + fun rewinfo -> + let goal = + match extra with + | Some t -> Theory.Trans.add_symbol goal rewinfo.morph_rlt envs t + | None -> goal + in + let pattern, subject, goal = + Theory.Trans.t_of_constr goal rewinfo.morph_rlt envs + (rewinfo.pattern , rewinfo.subject) + in + let goal, ir = Theory.Trans.ir_of_envs goal rewinfo.morph_rlt envs in + + let units = Theory.Trans.ir_to_units ir in + let m = Matcher.subterm ?strict units pattern subject in + (* We sort the monad in increasing size of contet *) + let m = Search_monad.sort (fun (x,_,_) (y,_,_) -> x - y) m in + + if show + then + Print.print rewinfo.morph_rlt ir m (hypinfo.Coq.Rewrite.context) + + else + try + let pat,subst = choose_subst occ_subterm occ_sol m in + let tr_step = Matcher.Subst.instantiate subst pat in + let tr_step_raw = Theory.Trans.raw_constr_of_t ir rewinfo.morph_rlt [] tr_step in + + let conv = (Theory.Trans.raw_constr_of_t ir rewinfo.morph_rlt (hypinfo.Coq.Rewrite.context)) in + let subst = Matcher.Subst.to_list subst in + let subst = List.map (fun (x,y) -> x, conv y) subst in + let by_aac_reflexivity = (by_aac_reflexivity rewinfo.subject rewinfo.eqt ir) in + core_aac_rewrite ?abort rewinfo subst by_aac_reflexivity tr_step_raw tr_step subject + + with + | NoSolutions -> + Tacticals.tclFAIL 0 + (Pp.str (if occ_subterm = None && occ_sol = None + then "No matching occurence modulo AC found" + else "No such solution")) + ) + ) goal + + +open Coq.Rewrite +open Tacmach +open Tacticals +open Tacexpr +open Tacinterp +open Extraargs +open Genarg + +let rec add k x = function + | [] -> [k,x] + | k',_ as ky::q -> + if k'=k then Coq.user_error ("redondant argument ("^k^")") + else ky::add k x q + +let get k l = try Some (List.assoc k l) with Not_found -> None + +let get_lhs l = try List.assoc "in_right" l; false with Not_found -> true + +let aac_rewrite ~args = + aac_rewrite ~occ_subterm:(get "at" args) ~occ_sol:(get "subst" args) ~in_left:(get_lhs args) + + +let pr_aac_args _ _ _ l = + List.fold_left + (fun acc -> function + | ("in_right" as s,_) -> Pp.(++) (Pp.str s) acc + | (k,i) -> Pp.(++) (Pp.(++) (Pp.str k) (Pp.int i)) acc + ) (Pp.str "") l + +ARGUMENT EXTEND aac_args +TYPED AS ((string * int) list ) +PRINTED BY pr_aac_args +| [ "at" integer(n) aac_args(q) ] -> [ add "at" n q ] +| [ "subst" integer(n) aac_args(q) ] -> [ add "subst" n q ] +| [ "in_right" aac_args(q) ] -> [ add "in_right" 0 q ] +| [ ] -> [ [] ] +END + +let pr_constro _ _ _ = fun b -> + match b with + | None -> Pp.str "" + | Some o -> Pp.str "" + +ARGUMENT EXTEND constro +TYPED AS (constr option) +PRINTED BY pr_constro +| [ "[" constr(c) "]" ] -> [ Some c ] +| [ ] -> [ None ] +END + +TACTIC EXTEND _aac_reflexivity_ +| [ "aac_reflexivity" ] -> [ aac_reflexivity ] +END + +TACTIC EXTEND _aac_normalise_ +| [ "aac_normalise" ] -> [ aac_normalise ] +END + +TACTIC EXTEND _aac_rewrite_ +| [ "aac_rewrite" orient(l2r) constr(c) aac_args(args) constro(extra)] -> + [ fun gl -> aac_rewrite ?extra ~args ~l2r ~strict:true c gl ] +END + +TACTIC EXTEND _aac_pattern_ +| [ "aac_pattern" orient(l2r) constr(c) aac_args(args) constro(extra)] -> + [ fun gl -> aac_rewrite ?extra ~args ~l2r ~strict:true ~abort:true c gl ] +END + +TACTIC EXTEND _aac_instances_ +| [ "aac_instances" orient(l2r) constr(c) aac_args(args) constro(extra)] -> + [ fun gl -> aac_rewrite ?extra ~args ~l2r ~strict:true ~show:true c gl ] +END + +TACTIC EXTEND _aacu_rewrite_ +| [ "aacu_rewrite" orient(l2r) constr(c) aac_args(args) constro(extra)] -> + [ fun gl -> aac_rewrite ?extra ~args ~l2r ~strict:false c gl ] +END + +TACTIC EXTEND _aacu_pattern_ +| [ "aacu_pattern" orient(l2r) constr(c) aac_args(args) constro(extra)] -> + [ fun gl -> aac_rewrite ?extra ~args ~l2r ~strict:false ~abort:true c gl ] +END + +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 diff --git a/rewrite.mli b/rewrite.mli new file mode 100644 index 0000000..d195075 --- /dev/null +++ b/rewrite.mli @@ -0,0 +1,9 @@ +(***************************************************************************) +(* This is part of aac_tactics, it is distributed under the terms of the *) +(* GNU Lesser General Public License version 3 *) +(* (see file LICENSE for more details) *) +(* *) +(* Copyright 2009-2010: Thomas Braibant, Damien Pous. *) +(***************************************************************************) + +(** Definition of the tactics, and corresponding Coq grammar entries.*) diff --git a/search_monad.ml b/search_monad.ml new file mode 100644 index 0000000..09a6455 --- /dev/null +++ b/search_monad.ml @@ -0,0 +1,70 @@ +(***************************************************************************) +(* This is part of aac_tactics, it is distributed under the terms of the *) +(* GNU Lesser General Public License version 3 *) +(* (see file LICENSE for more details) *) +(* *) +(* Copyright 2009-2010: Thomas Braibant, Damien Pous. *) +(***************************************************************************) + +type 'a m = | F of 'a + | N of 'a m list + +let fold (f : 'a -> 'b -> 'b) (m : 'a m) (acc : 'b) = + let rec aux acc = function + F x -> f x acc + | N l -> + (List.fold_left (fun acc x -> + match x with + | (N []) -> acc + | x -> aux acc x + ) acc l) + in + aux acc m + + +let rec (>>) : 'a m -> ('a -> 'b m) -> 'b m = + fun m f -> + match m with + | F x -> f x + | N l -> + N (List.fold_left (fun acc x -> + match x with + | (N []) -> acc + | x -> (x >> f)::acc + ) [] l) + +let (>>|) (m : 'a m) (n :'a m) : 'a m = match (m,n) with + | N [],_ -> n + | _,N [] -> m + | F x, N l -> N (F x::l) + | N l, F x -> N (F x::l) + | x,y -> N [x;y] + +let return : 'a -> 'a m = fun x -> F x +let fail : unit -> 'a m = fun () -> N [] + +let sprint f m = + fold (fun x acc -> Printf.sprintf "%s\n%s" acc (f x)) m "" +let rec count = function + | F _ -> 1 + | N l -> List.fold_left (fun acc x -> acc+count x) 0 l + +let opt_comb f x y = match x with None -> f y | _ -> x + +let rec choose = function + | F x -> Some x + | N l -> List.fold_left (fun acc x -> + opt_comb choose acc x + ) None l + +let is_empty = fun x -> choose x = None + +let to_list m = (fold (fun x acc -> x::acc) m []) + +let sort f m = + N (List.map (fun x -> F x) (List.sort f (to_list m))) + +(* preserve the structure of the heap *) +let filter f m = + fold (fun x acc -> (if f x then return x else fail ()) >>| acc) m (N []) + diff --git a/search_monad.mli b/search_monad.mli new file mode 100644 index 0000000..7e2a910 --- /dev/null +++ b/search_monad.mli @@ -0,0 +1,42 @@ +(***************************************************************************) +(* This is part of aac_tactics, it is distributed under the terms of the *) +(* GNU Lesser General Public License version 3 *) +(* (see file LICENSE for more details) *) +(* *) +(* Copyright 2009-2010: Thomas Braibant, Damien Pous. *) +(***************************************************************************) + +(** Search monad that allows to express non-deterministic algorithms + in a legible maner, or programs that solve combinatorial problems. + + @see the + inspiration of this module +*) + +(** A data type that represent a collection of ['a] *) +type 'a m + + (** {2 Monadic operations} *) + +(** bind and return *) +val ( >> ) : 'a m -> ('a -> 'b m) -> 'b m +val return : 'a -> 'a m + +(** non-deterministic choice *) +val ( >>| ) : 'a m -> 'a m -> 'a m + +(** failure *) +val fail : unit -> 'a m + +(** folding through the collection *) +val fold : ('a -> 'b -> 'b) -> 'a m -> 'b -> 'b + +(** {2 Derived facilities } *) + +val sprint : ('a -> string) -> 'a m -> string +val count : 'a m -> int +val choose : 'a m -> 'a option +val to_list : 'a m -> 'a list +val sort : ('a -> 'a -> int) -> 'a m -> 'a m +val is_empty: 'a m -> bool +val filter : ('a -> bool) -> 'a m -> 'a m diff --git a/theory.ml b/theory.ml new file mode 100644 index 0000000..3fa35bf --- /dev/null +++ b/theory.ml @@ -0,0 +1,1097 @@ +(***************************************************************************) +(* This is part of aac_tactics, it is distributed under the terms of the *) +(* GNU Lesser General Public License version 3 *) +(* (see file LICENSE for more details) *) +(* *) +(* Copyright 2009-2010: Thomas Braibant, Damien Pous. *) +(***************************************************************************) + +(** Constr from the theory of this particular development + + The inner-working of this module is highly correlated with the + particular structure of {b AAC.v}, therefore, it should + be of little interest to most readers. +*) +open Term + +module Control = struct + let printing = true + let debug = false + let time = false +end + +module Debug = Helper.Debug (Control) +open Debug + +(** {1 HMap : Specialized Hashtables based on constr} *) + + +module Hashed_constr = +struct + type t = constr + let equal = (=) + let hash = Hashtbl.hash +end + + (* TODO module HMap = Hashtbl, du coup ? *) +module HMap = Hashtbl.Make(Hashed_constr) + +let ac_theory_path = ["AAC_tactics"; "AAC"] + +module Stubs = struct + let path = ac_theory_path@["Internal"] + + (** The constants from the inductive type *) + let _Tty = lazy (Coq.init_constant path "T") + let vTty = lazy (Coq.init_constant path "vT") + + let rsum = lazy (Coq.init_constant path "sum") + let rprd = lazy (Coq.init_constant path "prd") + let rsym = lazy (Coq.init_constant path "sym") + let runit = lazy (Coq.init_constant path "unit") + + let vnil = lazy (Coq.init_constant path "vnil") + let vcons = lazy (Coq.init_constant path "vcons") + let eval = lazy (Coq.init_constant path "eval") + + + let decide_thm = lazy (Coq.init_constant path "decide") + let lift_normalise_thm = lazy (Coq.init_constant path "lift_normalise") + + let lift = + lazy (Coq.init_constant ac_theory_path "AAC_lift") + let lift_proj_equivalence= + lazy (Coq.init_constant ac_theory_path "aac_lift_equivalence") + let lift_transitivity_left = + lazy(Coq.init_constant ac_theory_path "lift_transitivity_left") + let lift_transitivity_right = + lazy(Coq.init_constant ac_theory_path "lift_transitivity_right") + let lift_reflexivity = + lazy(Coq.init_constant ac_theory_path "lift_reflexivity") +end + +module Classes = struct + module Associative = struct + let path = ac_theory_path + let typ = lazy (Coq.init_constant path "Associative") + let ty (rlt : Coq.Relation.t) (value : Term.constr) = + mkApp (Lazy.force typ, [| rlt.Coq.Relation.carrier; + rlt.Coq.Relation.r; + value + |] ) + let infer goal rlt value = + let ty = ty rlt value in + Coq.resolve_one_typeclass goal ty + end + + module Commutative = struct + let path = ac_theory_path + let typ = lazy (Coq.init_constant path "Commutative") + let ty (rlt : Coq.Relation.t) (value : Term.constr) = + mkApp (Lazy.force typ, [| rlt.Coq.Relation.carrier; + rlt.Coq.Relation.r; + value + |] ) + + end + + module Proper = struct + let path = ac_theory_path @ ["Internal";"Sym"] + let typeof = lazy (Coq.init_constant path "type_of") + let relof = lazy (Coq.init_constant path "rel_of") + let mk_typeof : Coq.Relation.t -> int -> constr = fun rlt n -> + let x = rlt.Coq.Relation.carrier in + mkApp (Lazy.force typeof, [| x ; Coq.Nat.of_int n |]) + let mk_relof : Coq.Relation.t -> int -> constr = fun rlt n -> + let (x,r) = Coq.Relation.split rlt in + mkApp (Lazy.force relof, [| x;r ; Coq.Nat.of_int n |]) + + let ty rlt op ar = + let typeof = mk_typeof rlt ar in + let relof = mk_relof rlt ar in + Coq.Classes.mk_morphism typeof relof op + let infer goal rlt op ar = + let ty = ty rlt op ar in + Coq.resolve_one_typeclass goal ty + end + + module Unit = struct + let path = ac_theory_path + let typ = lazy (Coq.init_constant path "Unit") + let ty (rlt : Coq.Relation.t) (value : Term.constr) (unit : Term.constr)= + mkApp (Lazy.force typ, [| rlt.Coq.Relation.carrier; + rlt.Coq.Relation.r; + value; + unit + |] ) + end + +end + +(* Non empty lists *) +module NEList = struct + let path = ac_theory_path @ ["Internal"] + let typ = lazy (Coq.init_constant path "list") + let nil = lazy (Coq.init_constant path "nil") + let cons = lazy (Coq.init_constant path "cons") + let cons ty h t = + mkApp (Lazy.force cons, [| ty; h ; t |]) + let nil ty x = + (mkApp (Lazy.force nil, [| ty ; x|])) + let rec of_list ty = function + | [] -> invalid_arg "NELIST" + | [x] -> nil ty x + | t::q -> cons ty t (of_list ty q) + + let type_of_list ty = + mkApp (Lazy.force typ, [|ty|]) +end + +(** a [mset] is a ('a * pos) list *) +let mk_mset ty (l : (constr * int) list) = + let pos = Lazy.force Coq.Pos.typ in + let pair (x : constr) (ar : int) = + Coq.Pair.of_pair ty pos (x, Coq.Pos.of_int ar) + in + let pair_ty = Coq.lapp Coq.Pair.typ [| ty ; pos|] in + let rec aux = function + | [ ] -> assert false + | [x,ar] -> NEList.nil pair_ty (pair x ar) + | (t,ar)::q -> NEList.cons pair_ty (pair t ar) (aux q) + in + aux l + +module Sigma = struct + let sigma = lazy (Coq.init_constant ac_theory_path "sigma") + let sigma_empty = lazy (Coq.init_constant ac_theory_path "sigma_empty") + let sigma_add = lazy (Coq.init_constant ac_theory_path "sigma_add") + let sigma_get = lazy (Coq.init_constant ac_theory_path "sigma_get") + + let add ty n x map = + mkApp (Lazy.force sigma_add,[|ty; n; x ; map|]) + let empty ty = + mkApp (Lazy.force sigma_empty,[|ty |]) + let typ ty = + mkApp (Lazy.force sigma, [|ty|]) + + let to_fun ty null map = + mkApp (Lazy.force sigma_get, [|ty;null;map|]) + + let of_list ty null l = + match l with + | (_,t)::q -> + let map = + List.fold_left + (fun acc (i,t) -> + assert (i > 0); + add ty (Coq.Pos.of_int i) ( t) acc) + (empty ty) + q + in to_fun ty (t) map + | [] -> debug "of_list empty" ; to_fun ty (null) (empty ty) + + +end + + +module Sym = struct + type pack = {ar: Term.constr; value: Term.constr ; morph: Term.constr} + let path = ac_theory_path @ ["Internal";"Sym"] + let typ = lazy (Coq.init_constant path "pack") + let mkPack = lazy (Coq.init_constant path "mkPack") + let value = lazy (Coq.init_constant path "value") + let null = lazy (Coq.init_constant path "null") + let mk_pack (rlt: Coq.Relation.t) s = + let (x,r) = Coq.Relation.split rlt in + mkApp (Lazy.force mkPack, [|x;r; s.ar;s.value;s.morph|]) + let null rlt = + let x = rlt.Coq.Relation.carrier in + let r = rlt.Coq.Relation.r in + mkApp (Lazy.force null, [| x;r;|]) + + let mk_ty : Coq.Relation.t -> constr = fun rlt -> + let (x,r) = Coq.Relation.split rlt in + mkApp (Lazy.force typ, [| x; r|] ) +end + +module Bin =struct + type pack = {value : Term.constr; + compat : Term.constr; + assoc : Term.constr; + comm : Term.constr option; + } + + let path = ac_theory_path @ ["Internal";"Bin"] + let typ = lazy (Coq.init_constant path "pack") + let mkPack = lazy (Coq.init_constant path "mk_pack") + + let mk_pack: Coq.Relation.t -> pack -> Term.constr = fun (rlt) s -> + let (x,r) = Coq.Relation.split rlt in + let comm_ty = Classes.Commutative.ty rlt s.value in + mkApp (Lazy.force mkPack , [| x ; r; + s.value; + s.compat ; + s.assoc; + Coq.Option.of_option comm_ty s.comm + |]) + let mk_ty : Coq.Relation.t -> constr = fun rlt -> + let (x,r) = Coq.Relation.split rlt in + mkApp (Lazy.force typ, [| x; r|] ) +end + +module Unit = struct + let path = ac_theory_path @ ["Internal"] + let unit_of_ty = lazy (Coq.init_constant path "unit_of") + let unit_pack_ty = lazy (Coq.init_constant path "unit_pack") + let mk_unit_of = lazy (Coq.init_constant path "mk_unit_for") + let mk_unit_pack = lazy (Coq.init_constant path "mk_unit_pack") + + type unit_of = + { + uf_u : Term.constr; (* u *) + uf_idx : Term.constr; + uf_desc : Term.constr; (* Unit R (e_bin uf_idx) u *) + } + + type pack = { + u_value : Term.constr; (* X *) + u_desc : (unit_of) list (* unit_of u_value *) + } + + let ty_unit_of rlt e_bin u = + let (x,r) = Coq.Relation.split rlt in + mkApp ( Lazy.force unit_of_ty, [| x; r; e_bin; u |]) + + let ty_unit_pack rlt e_bin = + let (x,r) = Coq.Relation.split rlt in + mkApp (Lazy.force unit_pack_ty, [| x; r; e_bin |]) + + let mk_unit_of rlt e_bin u unit_of = + let (x,r) = Coq.Relation.split rlt in + mkApp (Lazy.force mk_unit_of , [| x; + r; + e_bin ; + u; + unit_of.uf_idx; + unit_of.uf_desc + |]) + + let mk_pack rlt e_bin pack : Term.constr = + let (x,r) = Coq.Relation.split rlt in + let ty = ty_unit_of rlt e_bin pack.u_value in + let mk_unit_of = mk_unit_of rlt e_bin pack.u_value in + let u_desc =Coq.List.of_list ( ty ) (List.map mk_unit_of pack.u_desc) in + mkApp (Lazy.force mk_unit_pack, [|x;r; + e_bin ; + pack.u_value; + u_desc + |]) + + let default x : pack = + { u_value = x; + u_desc = [] + } + +end + +let anomaly msg = + Util.anomaly ("aac_tactics: " ^ msg) + +let user_error msg = + Util.error ("aac_tactics: " ^ msg) + +module Trans = struct + + (** {1 From Coq to Abstract Syntax Trees (AST)} + + This module provides facilities to interpret a Coq term with + arbitrary operators as an abstract syntax tree. Considering an + application, we try to infer instances of our classes. + + We consider that [A] operators are coarser than [AC] operators, + which in turn are coarser than raw morphisms. That means that + [List.append], of type [(A : Type) -> list A -> list A -> list + A] can be understood as an [A] operator. + + During this reification, we gather some informations that will + be used to rebuild Coq terms from AST ( type {!envs}) + + We use a main hash-table from [constr] to [pack], in order to + discriminate the various constructors. All these are mixed in + order to improve on the number of comparisons in the tables *) + + (* 'a * (unit, op_unit) option *) + type 'a with_unit = 'a * (Unit.unit_of) option + type pack = + (* used to infer the AC/A structure in the first pass {!Gather} *) + | Bin of Bin.pack with_unit + (* will only be used in the second pass : {!Parse}*) + | Sym of Sym.pack + | Unit of constr (* to avoid confusion in bloom *) + + (** discr is a map from {!Term.constr} to {!pack}. + + [None] means that it is not possible to instantiate this partial + application to an interesting class. + + [Some x] means that we found something in the past. This means + in particular that a single [constr] cannot be two things at the + same time. + + The field [bloom] allows to give a unique number to each class we + found. *) + type envs = + { + discr : (pack option) HMap.t ; + bloom : (pack, int ) Hashtbl.t; + bloom_back : (int, pack ) Hashtbl.t; + bloom_next : int ref; + } + + let empty_envs () = + { + discr = HMap.create 17; + bloom = Hashtbl.create 17; + bloom_back = Hashtbl.create 17; + bloom_next = ref 1; + } + + + + let add_bloom envs pack = + if Hashtbl.mem envs.bloom pack + then () + else + let x = ! (envs.bloom_next) in + Hashtbl.add envs.bloom pack x; + Hashtbl.add envs.bloom_back x pack; + incr (envs.bloom_next) + + let find_bloom envs pack = + try Hashtbl.find envs.bloom pack + with Not_found -> assert false + + (********************************************) + (* (\* Gather the occuring AC/A symbols *\) *) + (********************************************) + + (** This modules exhibit a function that memoize in the environment + all the AC/A operators as well as the morphism that occur. This + staging process allows us to prefer AC/A operators over raw + morphisms. Moreover, for each AC/A operators, we need to try to + infer units. Otherwise, we do not have [x * y * x <= a * a] since 1 + does not occur. + + But, do we also need to check whether constants are + units. Otherwise, we do not have the ability to rewrite [0 = a + + a] in [a = ...]*) + module Gather : sig + val gather : Coq.goal_sigma -> Coq.Relation.t -> envs -> Term.constr -> Coq.goal_sigma + end + = struct + + let memoize envs t pack : unit = + begin + HMap.add envs.discr t (Some pack); + add_bloom envs pack; + match pack with + | Bin (_, None) | Sym _ -> () + | Bin (_, Some (unit_of)) -> + let unit = unit_of.Unit.uf_u in + HMap.add envs.discr unit (Some (Unit unit)); + add_bloom envs (Unit unit); + | Unit _ -> assert false + end + + + let get_unit (rlt : Coq.Relation.t) op goal : + (Coq.goal_sigma * constr * constr ) option= + let x = (rlt.Coq.Relation.carrier) in + let unit, goal = Coq.evar_unit goal x in + let ty =Classes.Unit.ty rlt op unit in + let result = + try + let t,goal = Coq.resolve_one_typeclass goal ty in + Some (goal,t,unit) + with Not_found -> None + in + match result with + | None -> None + | Some (goal,s,unit) -> + let unit = Coq.nf_evar goal unit in + Some (goal, unit, s) + + + + (** gives back the class and the operator *) + let is_bin (rlt: Coq.Relation.t) (op: constr) ( goal: Coq.goal_sigma) + : (Coq.goal_sigma * Bin.pack) option = + let assoc_ty = Classes.Associative.ty rlt op in + let comm_ty = Classes.Commutative.ty rlt op in + let proper_ty = Classes.Proper.ty rlt op 2 in + try + let proper , goal = Coq.resolve_one_typeclass goal proper_ty in + let assoc, goal = Coq.resolve_one_typeclass goal assoc_ty in + let comm , goal = + try + let comm, goal = Coq.resolve_one_typeclass goal comm_ty in + Some comm, goal + with Not_found -> + None, goal + in + let bin = + {Bin.value = op; + Bin.compat = proper; + Bin.assoc = assoc; + Bin.comm = comm } + in + Some (goal,bin) + with |Not_found -> None + + let is_bin (rlt : Coq.Relation.t) (op : constr) (goal : Coq.goal_sigma)= + match is_bin rlt op goal with + | None -> None + | Some (goal, bin_pack) -> + match get_unit rlt op goal with + | None -> Some (goal, Bin (bin_pack, None)) + | Some (gl, unit,s) -> + let unit_of = + { + Unit.uf_u = unit; + (* TRICK : this term is not well-typed by itself, + but it is okay the way we use it in the other + functions *) + Unit.uf_idx = op; + Unit.uf_desc = s; + } + in Some (gl,Bin (bin_pack, Some (unit_of))) + + + (** {is_morphism} try to infer the kind of operator we are + dealing with *) + let is_morphism goal (rlt : Coq.Relation.t) (papp : Term.constr) (ar : int) : (Coq.goal_sigma * pack ) option = + let typeof = Classes.Proper.mk_typeof rlt ar in + let relof = Classes.Proper.mk_relof rlt ar in + let m = Coq.Classes.mk_morphism typeof relof papp in + try + let m,goal = Coq.resolve_one_typeclass goal m in + let pack = {Sym.ar = (Coq.Nat.of_int ar); Sym.value= papp; Sym.morph= m} in + Some (goal, Sym pack) + with + | Not_found -> None + + + (* [crop_app f [| a_0 ; ... ; a_n |]] + returns Some (f a_0 ... a_(n-2), [|a_(n-1); a_n |] ) + *) + let crop_app t ca : (constr * constr array) option= + let n = Array.length ca in + if n <= 1 + then None + else + let papp = Term.mkApp (t, Array.sub ca 0 (n-2) ) in + let args = Array.sub ca (n-2) 2 in + Some (papp, args ) + + let fold goal (rlt : Coq.Relation.t) envs t ca cont = + let fold_morphism t ca = + let nb_params = Array.length ca in + let rec aux n = + assert (n < nb_params && 0 < nb_params ); + let papp = Term.mkApp (t, Array.sub ca 0 n) in + match is_morphism goal rlt papp (nb_params - n) with + | None -> + (* here we have to memoize the failures *) + HMap.add envs.discr papp None; + if n < nb_params - 1 then aux (n+1) else goal + | Some (goal, pack) -> + let args = Array.sub ca (n) (nb_params -n)in + let goal = Array.fold_left cont goal args in + memoize envs papp pack; + goal + in + if nb_params = 0 then goal else aux 0 + in + let is_aac t = is_bin rlt t in + match crop_app t ca with + | None -> + fold_morphism t ca + | Some (papp, args) -> + begin match is_aac papp goal with + | None -> fold_morphism t ca + | Some (goal, pack) -> + memoize envs papp pack; + Array.fold_left cont goal args + end + + (* update in place the envs of known stuff, using memoization. We + have to memoize failures, here. *) + let gather goal (rlt : Coq.Relation.t ) envs t : Coq.goal_sigma = + let rec aux goal x = + match Coq.decomp_term x with + | App (t,ca) -> + fold goal rlt envs t ca (aux ) + | _ -> goal + in + aux goal t + end + + (** We build a term out of a constr, updating in place the + environment if needed (the only kind of such updates are the + constants). *) + module Parse : + sig + val t_of_constr : Coq.goal_sigma -> Coq.Relation.t -> envs -> constr -> Matcher.Terms.t * Coq.goal_sigma + end + = struct + + (** [discriminates goal envs rlt t ca] infer : + + - its {! pack } (is it an AC operator, or an A operator, or a + Symbol ?), + + - the relevant partial application, + + - the vector of the remaining arguments + + We use an expansion to handle the special case of units, + before going back to the general discrimination + procedure. That means that a unit is more coarse than a raw + morphism + + This functions is prevented to go through [ar < 0] by the fact + that a constant is a morphism. But not an eva. *) + + let is_morphism goal (rlt : Coq.Relation.t) (papp : Term.constr) (ar : int) : (Coq.goal_sigma * pack ) option = + let typeof = Classes.Proper.mk_typeof rlt ar in + let relof = Classes.Proper.mk_relof rlt ar in + let m = Coq.Classes.mk_morphism typeof relof papp in + try + let m,goal = Coq.resolve_one_typeclass goal m in + let pack = {Sym.ar = (Coq.Nat.of_int ar); Sym.value= papp; Sym.morph= m} in + Some (goal, Sym pack) + with + | e -> None + + exception NotReflexive + let discriminate goal envs (rlt : Coq.Relation.t) t ca : Coq.goal_sigma * pack * constr * constr array = + let nb_params = Array.length ca in + let rec fold goal ar :Coq.goal_sigma * pack * constr * constr array = + begin + assert (0 <= ar && ar <= nb_params); + let p_app = mkApp (t, Array.sub ca 0 (nb_params - ar)) in + begin + try + begin match HMap.find envs.discr p_app with + | None -> + fold goal (ar-1) + | Some pack -> + (goal, pack, p_app, Array.sub ca (nb_params -ar ) ar) + end + with + Not_found -> (* Could not find this constr *) + memoize (is_morphism goal rlt p_app ar) p_app ar + end + end + and memoize (x) p_app ar = + assert (0 <= ar && ar <= nb_params); + match x with + | Some (goal, pack) -> + HMap.add envs.discr p_app (Some pack); + add_bloom envs pack; + (goal, pack, p_app, Array.sub ca (nb_params-ar) ar) + | None -> + + if ar = 0 then raise NotReflexive; + begin + (* to memoise the failures *) + HMap.add envs.discr p_app None; + (* will terminate, since [const] is capped, and it is + easy to find an instance of a constant *) + fold goal (ar-1) + end + in + try match HMap.find envs.discr (mkApp (t,ca))with + | None -> fold goal (nb_params) + | Some pack -> goal, pack, (mkApp (t,ca)), [| |] + with Not_found -> fold goal (nb_params) + + let discriminate goal envs rlt x = + try + match Coq.decomp_term x with + | App (t,ca) -> + discriminate goal envs rlt t ca + | _ -> discriminate goal envs rlt x [| |] + with + | NotReflexive -> user_error "The relation to which the goal was lifted is not Reflexive" + (* TODO: is it the only source of invalid use that fall + into this catch_all ? *) + | e -> + user_error "Cannot handle this kind of hypotheses (variables occuring under a function symbol which is not a proper morphism)." + + (** [t_of_constr goal rlt envs cstr] builds the abstract syntax tree + of the term [cstr]. Doing so, it modifies the environment of + known stuff [envs], and eventually creates fresh + evars. Therefore, we give back the goal updated accordingly *) + let t_of_constr goal (rlt: Coq.Relation.t ) envs : constr -> Matcher.Terms.t * Coq.goal_sigma = + let r_goal = ref (goal) in + let rec aux x = + match Coq.decomp_term x with + | Rel i -> Matcher.Terms.Var i + | _ -> + let goal, pack , p_app, ca = discriminate (!r_goal) envs rlt x in + r_goal := goal; + let k = find_bloom envs pack + in + match pack with + | Bin (pack,_) -> + begin match pack.Bin.comm with + | Some _ -> + assert (Array.length ca = 2); + Matcher.Terms.Plus ( k, aux ca.(0), aux ca.(1)) + | None -> + assert (Array.length ca = 2); + Matcher.Terms.Dot ( k, aux ca.(0), aux ca.(1)) + end + | Unit _ -> + assert (Array.length ca = 0); + Matcher.Terms.Unit ( k) + | Sym _ -> + Matcher.Terms.Sym ( k, Array.map aux ca) + in + ( + fun x -> let r = aux x in r, !r_goal + ) + + end (* Parse *) + + let add_symbol goal rlt envs l = + let goal = Gather.gather goal rlt envs (Term.mkApp (l, [| Term.mkRel 0;Term.mkRel 0|])) in + goal + + (* [t_of_constr] buils a the abstract syntax tree of a constr, + updating in place the environment. Doing so, we infer all the + morphisms and the AC/A operators. It is mandatory to do so both + for the pattern and the term, since AC symbols can occur in one + and not the other *) + let t_of_constr goal rlt envs (l,r) = + let goal = Gather.gather goal rlt envs l in + let goal = Gather.gather goal rlt envs r in + let l,goal = Parse.t_of_constr goal rlt envs l in + let r, goal = Parse.t_of_constr goal rlt envs r in + l, r, goal + + (* An intermediate representation of the environment, with association lists for AC/A operators, and also the raw [packer] information *) + + type ir = + { + packer : (int, pack) Hashtbl.t; (* = bloom_back *) + bin : (int * Bin.pack) list ; + units : (int * Unit.pack) list; + sym : (int * Term.constr) list ; + matcher_units : Matcher.ext_units + } + + let ir_to_units ir = ir.matcher_units + + let ir_of_envs goal (rlt : Coq.Relation.t) envs = + let add x y l = (x,y)::l in + let nil = [] in + let sym , + (bin : (int * Bin.pack with_unit) list), + (units : (int * constr) list) = + Hashtbl.fold + (fun int pack (sym,bin,units) -> + match pack with + | Bin s -> + sym, add (int) s bin, units + | Sym s -> + add (int) s sym, bin, units + | Unit s -> + sym, bin, add int s units + ) + envs.bloom_back + (nil,nil,nil) + in + let matcher_units = + let unit_for , is_ac = + List.fold_left + (fun ((unit_for,is_ac) as acc) (n,(bp,wu)) -> + match wu with + | None -> acc + | Some (unit_of) -> + let unit_n = Hashtbl.find envs.bloom + (Unit unit_of.Unit.uf_u) + in + ( n, unit_n)::unit_for, + (n, bp.Bin.comm <> None )::is_ac + + ) + ([],[]) bin + in + {Matcher.unit_for = unit_for; Matcher.is_ac = is_ac} + + in + let units : (int * Unit.pack) list = + List.fold_left + (fun acc (n,u) -> + (* first, gather all bins with this unit *) + let all_bin = + List.fold_left + ( fun acc (nop,(bp,wu)) -> + match wu with + | None -> acc + | Some unit_of -> + if unit_of.Unit.uf_u = u + then + {unit_of with + Unit.uf_idx = (Coq.Pos.of_int nop)} :: acc + else + acc + ) + [] bin + in + (n,{ + Unit.u_value = u; + Unit.u_desc = all_bin + })::acc + ) + [] units + + in + goal, { + packer = envs.bloom_back; + bin = (List.map (fun (n,(s,_)) -> n, s) bin); + units = units; + sym = (List.map (fun (n,s) -> n,(Sym.mk_pack rlt s)) sym); + matcher_units = matcher_units + } + + + + (** {1 From AST back to Coq } + + The next functions allow one to map OCaml abstract syntax trees + to Coq terms *) + + (** {2 Building raw, natural, terms} *) + + (** [raw_constr_of_t_debruijn] rebuilds a term in the raw + representation, without products on top, and maybe escaping free + debruijn indices (in the case of a pattern for example). *) + let raw_constr_of_t_debruijn ir (t : Matcher.Terms.t) : Term.constr * int list = + let add_set,get = + let r = ref [] in + let rec add x = function + [ ] -> [x] + | t::q when t = x -> t::q + | t::q -> t:: (add x q) + in + (fun x -> r := add x !r),(fun () -> !r) + in + (* Here, we rely on the invariant that the maps are well formed: + it is meanigless to fail to find a symbol in the maps, or to + find the wrong kind of pack in the maps *) + let rec aux t = + match t with + | Matcher.Terms.Plus (s,l,r) -> + begin match Hashtbl.find ir.packer s with + | Bin (s,_) -> + mkApp (s.Bin.value , [|(aux l);(aux r)|]) + | _ -> Printf.printf "erreur:%i\n%!"s; + assert false + end + | Matcher.Terms.Dot (s,l,r) -> + begin match Hashtbl.find ir.packer s with + | Bin (s,_) -> + mkApp (s.Bin.value, [|(aux l);(aux r)|]) + | _ -> assert false + end + | Matcher.Terms.Sym (s,t) -> + begin match Hashtbl.find ir.packer s with + | Sym s -> + mkApp (s.Sym.value, Array.map aux t) + | _ -> assert false + end + | Matcher.Terms.Unit x -> + begin match Hashtbl.find ir.packer x with + | Unit s -> s + | _ -> assert false + end + | Matcher.Terms.Var i -> add_set i; + mkRel (i) + in + let t = aux t in + t , get ( ) + + (** [raw_constr_of_t] rebuilds a term in the raw representation *) + let raw_constr_of_t ir rlt (context:rel_context) t = + (** cap rebuilds the products in front of the constr *) + let rec cap c = function [] -> c + | t::q -> + let i = Term.lookup_rel t context in + cap (mkProd_or_LetIn i c) q + in + let t,indices = raw_constr_of_t_debruijn ir t in + cap t (List.sort (Pervasives.compare) indices) + + + (** {2 Building reified terms} *) + + (* Some informations to be able to build the maps *) + type reif_params = + { + bin_null : Bin.pack; (* the default A operator *) + sym_null : constr; + unit_null : Unit.pack; + sym_ty : constr; (* the type, as it appears in e_sym *) + bin_ty : constr + } + + + (** A record containing the environments that will be needed by the + decision procedure, as a Coq constr. Contains the functions + from the symbols (as ints) to indexes (as constr) *) + + type sigmas = { + env_sym : Term.constr; + env_bin : Term.constr; + env_units : Term.constr; (* the [idx -> X:constr] *) + } + + + type sigma_maps = { + sym_to_pos : int -> Term.constr; + bin_to_pos : int -> Term.constr; + units_to_pos : int -> Term.constr; + } + + + (** infers some stuff that will be required when we will build + environments (our environments need a default case, so we need + an Op_AC, an Op_A, and a symbol) *) + (* Note : this function can fail if the user is using the wrong + relation, like proving a = b, while the classes are defined with + another relation (==) *) + let build_reif_params goal (rlt : Coq.Relation.t) (zero) : + reif_params * Coq.goal_sigma = + let carrier = rlt.Coq.Relation.carrier in + let bin_null = + try + let op,goal = Coq.evar_binary goal carrier in + let assoc,goal = Classes.Associative.infer goal rlt op in + let compat,goal = Classes.Proper.infer goal rlt op 2 in + let op = Coq.nf_evar goal op in + { + Bin.value = op; + Bin.compat = compat; + Bin.assoc = assoc; + Bin.comm = None + } + with Not_found -> user_error "Cannot infer a default A operator (required at least to be Proper and Associative)" + in + let zero, goal = + try + let evar_op,goal = Coq.evar_binary goal carrier in + let evar_unit, goal = Coq.evar_unit goal carrier in + let query = Classes.Unit.ty rlt evar_op evar_unit in + let _, goal = Coq.resolve_one_typeclass goal query in + Coq.nf_evar goal evar_unit, goal + with _ -> zero, goal in + let sym_null = Sym.null rlt in + let unit_null = Unit.default zero in + let record = + { + bin_null = bin_null; + sym_null = sym_null; + unit_null = unit_null; + sym_ty = Sym.mk_ty rlt ; + bin_ty = Bin.mk_ty rlt + } + in + record, goal + + (* We want to lift down the indexes of symbols. *) + let renumber (l: (int * 'a) list ) = + let _, l = List.fold_left (fun (next,acc) (glob,x) -> + (next+1, (next,glob,x)::acc) + ) (1,[]) l + in + let rec to_global loc = function + | [] -> assert false + | (local, global,x)::q when local = loc -> global + | _::q -> to_global loc q + in + let rec to_local glob = function + | [] -> assert false + | (local, global,x)::q when global = glob -> local + | _::q -> to_local glob q + in + let locals = List.map (fun (local,global,x) -> local,x) l in + locals, (fun x -> to_local x l) , (fun x -> to_global x l) + + (** [build_sigma_maps] given a envs and some reif_params, we are + able to build the sigmas *) + let build_sigma_maps (rlt : Coq.Relation.t) zero ir (k : sigmas * sigma_maps -> Proof_type.tactic ) : Proof_type.tactic = fun goal -> + let rp,goal = build_reif_params goal rlt zero in + let renumbered_sym, to_local, to_global = renumber ir.sym in + let env_sym = Sigma.of_list + rp.sym_ty + (rp.sym_null) + renumbered_sym + in + Coq.cps_mk_letin "env_sym" env_sym + (fun env_sym -> + let bin = (List.map ( fun (n,s) -> n, Bin.mk_pack rlt s) ir.bin) in + let env_bin = + Sigma.of_list + rp.bin_ty + (Bin.mk_pack rlt rp.bin_null) + bin + in + Coq.cps_mk_letin "env_bin" env_bin + (fun env_bin -> + let units = (List.map (fun (n,s) -> n, Unit.mk_pack rlt env_bin s)ir.units) in + let env_units = + Sigma.of_list + (Unit.ty_unit_pack rlt env_bin) + (Unit.mk_pack rlt env_bin rp.unit_null ) + units + in + + Coq.cps_mk_letin "env_units" env_units + (fun env_units -> + let sigmas = + { + env_sym = env_sym ; + env_bin = env_bin ; + env_units = env_units; + } in + let f = List.map (fun (x,_) -> (x,Coq.Pos.of_int x)) in + let sigma_maps = + { + sym_to_pos = (let sym = f renumbered_sym in fun x -> (List.assoc (to_local x) sym)); + bin_to_pos = (let bin = f bin in fun x -> (List.assoc x bin)); + units_to_pos = (let units = f units in fun x -> (List.assoc x units)); + } + in + k (sigmas, sigma_maps ) + ) + ) + ) goal + + (** builders for the reification *) + type reif_builders = + { + rsum: constr -> constr -> constr -> constr; + rprd: constr -> constr -> constr -> constr; + rsym: constr -> constr array -> constr; + runit : constr -> constr + } + + (* donne moi une tactique, je rajoute ma part. Potentiellement, il + est possible d'utiliser la notation 'do' a la Haskell: + http://www.cas.mcmaster.ca/~carette/pa_monad/ *) + let (>>) : 'a * Proof_type.tactic -> ('a -> 'b * Proof_type.tactic) -> 'b * Proof_type.tactic = + fun (x,t) f -> + let b,t' = f x in + b, Tacticals.tclTHEN t t' + + let return x = x, Tacticals.tclIDTAC + + let mk_vect vnil vcons v = + let ar = Array.length v in + let rec aux = function + | 0 -> vnil + | n -> let n = n-1 in + mkApp( vcons, + [| + (Coq.Nat.of_int n); + v.(ar - 1 - n); + (aux (n)) + |] + ) + in aux ar + + (* TODO: use a do notation *) + let mk_reif_builders (rlt: Coq.Relation.t) (env_sym:constr) (k: reif_builders -> Proof_type.tactic) = + let x = (rlt.Coq.Relation.carrier) in + let r = (rlt.Coq.Relation.r) in + + let x_r_env = [|x;r;env_sym|] in + let tty = mkApp (Lazy.force Stubs._Tty, x_r_env) in + let rsum = mkApp (Lazy.force Stubs.rsum, x_r_env) in + let rprd = mkApp (Lazy.force Stubs.rprd, x_r_env) in + let rsym = mkApp (Lazy.force Stubs.rsym, x_r_env) in + let vnil = mkApp (Lazy.force Stubs.vnil, x_r_env) in + let vcons = mkApp (Lazy.force Stubs.vcons, x_r_env) in + Coq.cps_mk_letin "tty" tty + (fun tty -> + Coq.cps_mk_letin "rsum" rsum + (fun rsum -> + Coq.cps_mk_letin "rprd" rprd + (fun rprd -> + Coq.cps_mk_letin "rsym" rsym + (fun rsym -> + Coq.cps_mk_letin "vnil" vnil + (fun vnil -> + Coq.cps_mk_letin "vcons" vcons + (fun vcons -> + let r ={ + rsum = + begin fun idx l r -> + mkApp (rsum, [| idx ; mk_mset tty [l,1 ; r,1]|]) + end; + rprd = + begin fun idx l r -> + let lst = NEList.of_list tty [l;r] in + mkApp (rprd, [| idx; lst|]) + end; + rsym = + begin fun idx v -> + let vect = mk_vect vnil vcons v in + mkApp (rsym, [| idx; vect|]) + end; + runit = fun idx -> (* could benefit of a letin *) + mkApp (Lazy.force Stubs.runit , [|x;r;env_sym;idx; |]) + } + in k r + )))))) + + + + type reifier = sigma_maps * reif_builders + + + let mk_reifier rlt zero envs (k : sigmas *reifier -> Proof_type.tactic) = + build_sigma_maps rlt zero envs + (fun (s,sm) -> + mk_reif_builders rlt s.env_sym + (fun rb ->k (s,(sm,rb)) ) + + ) + + (** [reif_constr_of_t reifier t] rebuilds the term [t] in the + reified form. We use the [reifier] to minimise the size of the + terms (we make as much lets as possible)*) + let reif_constr_of_t (sm,rb) (t:Matcher.Terms.t) : constr = + let rec aux = function + | Matcher.Terms.Plus (s,l,r) -> + let idx = sm.bin_to_pos s in + rb.rsum idx (aux l) (aux r) + | Matcher.Terms.Dot (s,l,r) -> + let idx = sm.bin_to_pos s in + rb.rprd idx (aux l) (aux r) + | Matcher.Terms.Sym (s,t) -> + let idx = sm.sym_to_pos s in + rb.rsym idx (Array.map aux t) + | Matcher.Terms.Unit s -> + let idx = sm.units_to_pos s in + rb.runit idx + | Matcher.Terms.Var i -> + anomaly "call to reif_constr_of_t on a term with variables." + in aux t +end + + + diff --git a/theory.mli b/theory.mli new file mode 100644 index 0000000..cc9a617 --- /dev/null +++ b/theory.mli @@ -0,0 +1,197 @@ +(***************************************************************************) +(* This is part of aac_tactics, it is distributed under the terms of the *) +(* GNU Lesser General Public License version 3 *) +(* (see file LICENSE for more details) *) +(* *) +(* Copyright 2009-2010: Thomas Braibant, Damien Pous. *) +(***************************************************************************) + +(** Bindings for Coq constants that are specific to the plugin; + reification and translation functions. + + Note: this module is highly correlated with the definitions of {i + AAC.v}. + + This module interfaces with the above Coq module; it provides + facilities to interpret a term with arbitrary operators as an + abstract syntax tree, and to convert an AST into a Coq term + (either using the Coq "raw" terms, as written in the starting + goal, or using the reified Coq datatypes we define in {i + AAC.v}). +*) + +(** Both in OCaml and Coq, we represent finite multisets using + weighted lists ([('a*int) list]), see {!Matcher.mset}. + + [mk_mset ty l] constructs a Coq multiset from an OCaml multiset + [l] of Coq terms of type [ty] *) + +val mk_mset:Term.constr -> (Term.constr * int) list ->Term.constr + +(** {2 Packaging modules} *) + +(** Environments *) +module Sigma: +sig + (** [add ty n x map] adds the value [x] of type [ty] with key [n] in [map] *) + val add: Term.constr ->Term.constr ->Term.constr ->Term.constr ->Term.constr + + (** [empty ty] create an empty map of type [ty] *) + val empty: Term.constr ->Term.constr + + (** [of_list ty null l] translates an OCaml association list into a Coq one *) + val of_list: Term.constr -> Term.constr -> (int * Term.constr ) list -> Term.constr + + (** [to_fun ty null map] converts a Coq association list into a Coq function (with default value [null]) *) + val to_fun: Term.constr ->Term.constr ->Term.constr ->Term.constr +end + + +(** Dynamically typed morphisms *) +module Sym: +sig + (** mimics the Coq record [Sym.pack] *) + type pack = {ar: Term.constr; value: Term.constr ; morph: Term.constr} + + val typ: Term.constr lazy_t + + + (** [mk_pack rlt (ar,value,morph)] *) + val mk_pack: Coq.Relation.t -> pack -> Term.constr + + (** [null] builds a dummy (identity) symbol, given an {!Coq.Relation.t} *) + val null: Coq.Relation.t -> Term.constr + +end + + +(** We need to export some Coq stubs out of this module. They are used + by the main tactic, see {!Rewrite} *) +module Stubs : sig + val lift : Term.constr Lazy.t + val lift_proj_equivalence : Term.constr Lazy.t + val lift_transitivity_left : Term.constr Lazy.t + val lift_transitivity_right : Term.constr Lazy.t + val lift_reflexivity : Term.constr Lazy.t + (** The evaluation fonction, used to convert a reified coq term to a + raw coq term *) + val eval: Term.constr lazy_t + + (** The main lemma of our theory, that is + [compare (norm u) (norm v) = Eq -> eval u == eval v] *) + val decide_thm:Term.constr lazy_t + + val lift_normalise_thm : Term.constr lazy_t +end + +(** {2 Building reified terms} + + We define a bundle of functions to build reified versions of the + terms (those that will be given to the reflexive decision + procedure). In particular, each field takes as first argument the + index of the symbol rather than the symbol itself. *) + +(** Tranlations between Coq and OCaml *) +module Trans : sig + + (** This module provides facilities to interpret a term with + arbitrary operators as an instance of an abstract syntax tree + {!Matcher.Terms.t}. + + For each Coq application [f x_1 ... x_n], this amounts to + deciding whether one of the partial applications [f x_1 + ... x_i], [i<=n] is a proper morphism, whether the partial + application with [i=n-2] yields an A or AC binary operator, and + whether the whole term is the unit for some A or AC operator. We + use typeclass resolution to test each of these possibilities. + + Note that there are ambiguous terms: + - a term like [f x y] might yield a unary morphism ([f x]) and a + binary one ([f]); we select the latter one (unless [f] is A or + AC, in which case we declare it accordingly); + - a term like [S O] can be considered as a morphism ([S]) + applied to a unit for [(+)], or as a unit for [( * )]; we + chose to give priority to units, so that the latter + interpretation is selected in this case; + - an element might be the unit for several operations + *) + + (** To achieve this reification, one need to record informations + about the collected operators (symbols, binary operators, + units). We use the following imperative internal data-structure to + this end. *) + + type envs + val empty_envs : unit -> envs + + + (** {2 Reification: from Coq terms to AST {!Matcher.Terms.t} } *) + + + (** [t_of_constr goal rlt envs (left,right)] builds the abstract + syntax tree of the terms [left] and [right]. We rely on the [goal] + to perform typeclasses resolutions to find morphisms compatible + with the relation [rlt]. Doing so, it modifies the reification + environment [envs]. Moreover, we need to create fresh + evars; this is why we give back the [goal], accordingly + updated. *) + + val t_of_constr : Coq.goal_sigma -> Coq.Relation.t -> envs -> (Term.constr * Term.constr) -> Matcher.Terms.t * Matcher.Terms.t * Coq.goal_sigma + + (** [add_symbol] adds a given binary symbol to the environment of + known stuff. *) + val add_symbol : Coq.goal_sigma -> Coq.Relation.t -> envs -> Term.constr -> Coq.goal_sigma + + (** {2 Reconstruction: from AST back to Coq terms } + + The next functions allow one to map OCaml abstract syntax trees + to Coq terms. We need two functions to rebuild different kind of + terms: first, raw terms, like the one encountered by + {!t_of_constr}; second, reified Coq terms, that are required for + the reflexive decision procedure. *) + + type ir + val ir_of_envs : Coq.goal_sigma -> Coq.Relation.t -> envs -> Coq.goal_sigma * ir + val ir_to_units : ir -> Matcher.ext_units + + (** {2 Building raw, natural, terms} *) + + (** [raw_constr_of_t] rebuilds a term in the raw representation, and + 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 -> (Term.rel_context) ->Matcher.Terms.t -> Term.constr + + (** {2 Building reified terms} *) + + (** The reification environments, as Coq constrs *) + + type sigmas = { + env_sym : Term.constr; + env_bin : Term.constr; + env_units : Term.constr; (* the [idx -> X:constr] *) + } + + + + (** We need to reify two terms (left and right members of a goal) + that share the same reification envirnoment. Therefore, we need + to add letins to the proof context in order to ensure some + sharing in the proof terms we produce. + + Moreover, in order to have as much sharing as possible, we also + add letins for various partial applications that are used + throughout the terms. + + To achieve this, we decompose the reconstruction function into + two steps: first, we build the reification environment and then + reify each term successively.*) + type reifier + + val mk_reifier : Coq.Relation.t -> Term.constr -> ir -> (sigmas * reifier -> Proof_type.tactic) -> Proof_type.tactic + + (** [reif_constr_of_t reifier t] rebuilds the term [t] in the + reified form. *) + val reif_constr_of_t : reifier -> Matcher.Terms.t -> Term.constr + +end -- cgit v1.2.3