summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
authorGravatar Benjamin Barenblat <bbaren@google.com>2019-02-13 20:40:51 -0500
committerGravatar Benjamin Barenblat <bbaren@google.com>2019-02-13 20:40:51 -0500
commit8018e923c75eb5504310864f821972f794b7d554 (patch)
tree88a55f7c23fcbbea0ff80e406555292049b48dec /src
parent76f9b4cdc5693a6313961e2f91b39ba311857e72 (diff)
New upstream version 8.8.0+1.gbp069dc3bupstream/8.8.0+1.gbp069dc3bupstream
Diffstat (limited to 'src')
-rw-r--r--src/aac.ml479
-rw-r--r--src/aac_plugin.mlpack8
-rw-r--r--src/aac_rewrite.ml425
-rw-r--r--src/aac_rewrite.mli24
-rw-r--r--src/coq.ml594
-rw-r--r--src/coq.mli232
-rw-r--r--src/helper.ml41
-rw-r--r--src/helper.mli33
-rw-r--r--src/matcher.ml1293
-rw-r--r--src/matcher.mli189
-rw-r--r--src/print.ml104
-rw-r--r--src/print.mli23
-rw-r--r--src/search_monad.ml70
-rw-r--r--src/search_monad.mli42
-rw-r--r--src/theory.ml1153
-rw-r--r--src/theory.mli197
16 files changed, 4507 insertions, 0 deletions
diff --git a/src/aac.ml4 b/src/aac.ml4
new file mode 100644
index 0000000..e879a69
--- /dev/null
+++ b/src/aac.ml4
@@ -0,0 +1,79 @@
+(***************************************************************************)
+(* 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 -- Reasoning modulo associativity and commutativity *)
+
+DECLARE PLUGIN "aac_plugin"
+
+
+open Ltac_plugin
+open Pcoq.Prim
+open Pcoq.Constr
+open Stdarg
+open Aac_rewrite
+open Extraargs
+open Genarg
+
+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 "<constr>"
+
+ARGUMENT EXTEND constro
+TYPED AS (constr option)
+PRINTED BY pr_constro
+| [ "[" constr(c) "]" ] -> [ Some c ]
+| [ ] -> [ None ]
+END
+
+TACTIC EXTEND _aac_reflexivity_
+| [ "aac_reflexivity" ] -> [ Proofview.V82.tactic aac_reflexivity ]
+END
+
+TACTIC EXTEND _aac_normalise_
+| [ "aac_normalise" ] -> [ Proofview.V82.tactic aac_normalise ]
+END
+
+TACTIC EXTEND _aac_rewrite_
+| [ "aac_rewrite" orient(l2r) constr(c) aac_args(args) constro(extra)] ->
+ [ Proofview.V82.tactic (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)] ->
+ [ Proofview.V82.tactic (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)] ->
+ [ Proofview.V82.tactic (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)] ->
+ [ Proofview.V82.tactic (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)] ->
+ [ Proofview.V82.tactic (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)] ->
+ [ Proofview.V82.tactic (fun gl -> aac_rewrite ?extra ~args ~l2r ~strict:false ~show:true c gl) ]
+END
diff --git a/src/aac_plugin.mlpack b/src/aac_plugin.mlpack
new file mode 100644
index 0000000..ae61b0d
--- /dev/null
+++ b/src/aac_plugin.mlpack
@@ -0,0 +1,8 @@
+Coq
+Helper
+Search_monad
+Matcher
+Theory
+Print
+Aac_rewrite
+Aac
diff --git a/src/aac_rewrite.ml b/src/aac_rewrite.ml
new file mode 100644
index 0000000..697c15c
--- /dev/null
+++ b/src/aac_rewrite.ml
@@ -0,0 +1,425 @@
+(***************************************************************************)
+(* 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 A or AC*)
+
+open Ltac_plugin
+
+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 ->
+ let env = Tacmach.pf_env gl in
+ let sigma = Tacmach.project gl in
+ pr_constr env sigma "last goal" (Tacmach.pf_concl gl);
+ exn msg e
+
+
+let retype = Coq.retype
+
+open EConstr
+open Names
+open Proof_type
+
+
+(** aac_lift : the ideal type beyond AAC_rewrite.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 : 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:(Pp.strbrk "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 = Proofview.V82.of_tactic (Tactics.convert_concl convert_to Constr.VMcast) in
+ let apply_tac = Proofview.V82.of_tactic (Tactics.apply decision_thm) in
+ (Tacticals.tclTHENLIST
+ [ retype decision_thm; retype convert_to;
+ convert ;
+ tac_or_exn apply_tac Coq.user_error (Pp.strbrk "unification failure");
+ tac_or_exn (time_tac "vm_norm" (Proofview.V82.of_tactic (Tactics.normalise_in_concl))) Coq.anomaly "vm_compute failure";
+ Tacticals.tclORELSE (Proofview.V82.of_tactic Tactics.reflexivity)
+ (Tacticals.tclFAIL 0 (Pp.str "Not an equality modulo A/AC"))
+ ])
+ )
+
+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 = Proofview.V82.of_tactic (Tactics.convert_concl convert_to Constr.VMcast) in
+ let apply_tac = Proofview.V82.of_tactic (Tactics.apply normalise_thm) in
+ (Tacticals.tclTHENLIST
+ [ retype normalise_thm; retype convert_to;
+ convert ;
+ apply_tac;
+ ])
+
+ )
+
+(** A handler tactic, that reifies the goal, and infer the liftings,
+ and then call its continuation *)
+let aac_conclude
+ (k : constr -> aac_lift -> Theory.Trans.ir -> Matcher.Terms.t -> Matcher.Terms.t -> Proof_type.tactic) = fun goal ->
+
+ let (equation : 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 @@ Pp.strbrk "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 env = Tacmach.pf_env goal in
+ let sigma = Tacmach.project goal in
+ let _ = pr_constr env sigma "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 @@ Pp.strbrk "No lifting from the goal's relation to an equivalence"
+
+open Tacexpr
+
+let aac_normalise = fun goal ->
+ let ids = Tacmach.pf_ids_of_hyps goal in
+ let mp = MPfile (DirPath.make (List.map Id.of_string ["AAC"; "AAC_tactics"])) in
+ let norm_tac = KerName.make2 mp (Label.make "internal_normalize") in
+ let norm_tac = Locus.ArgArg (None, norm_tac) in
+ Tacticals.tclTHENLIST
+ [
+ aac_conclude by_aac_normalise;
+ Proofview.V82.of_tactic (Tacinterp.eval_tactic (TacArg (None, TacCall (None, (norm_tac, [])))));
+ Proofview.V82.of_tactic (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:(Pp.strbrk "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
+
+ (Tacticals.tclTHEN (retype lift_reflexivity) (Proofview.V82.of_tactic (Tactics.apply lift_reflexivity)))
+ (fun goal ->
+ let concl = Tacmach.pf_concl goal in
+ let env = Tacmach.pf_env goal in
+ let sigma = Tacmach.project goal in
+ let _ = pr_constr env sigma "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 @@ Pp.strbrk "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
+ [ retype lift_transitivity;
+ Proofview.V82.of_tactic (Tactics.apply lift_transitivity)
+ ] goal
+
+
+(** The core tactic for aac_rewrite. Env and sigma are for the constr *)
+let core_aac_rewrite ?abort
+ rewinfo
+ subst
+ (by_aac_reflexivity : Matcher.Terms.t -> Matcher.Terms.t -> Proof_type.tactic)
+ env sigma (tr : constr) t left : tactic =
+ pr_constr env sigma "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_wrap ?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 : types) = Tacmach.pf_concl goal in
+ let (_,_,rlt) as concl =
+ match Coq.match_as_equation goal concl with
+ | None -> Coq.user_error @@ Pp.strbrk "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 (EConstr.to_constr (Tacmach.project goal) 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
+ let env = Tacmach.pf_env goal in
+ let sigma = Tacmach.project goal in
+ (* I'm not sure whether this is the right env/sigma for printing tr_step_raw *)
+ core_aac_rewrite ?abort rewinfo subst by_aac_reflexivity env sigma tr_step_raw tr_step subject
+
+ with
+ | NoSolutions ->
+ Tacticals.tclFAIL 0
+ (Pp.str (if occ_subterm = None && occ_sol = None
+ then "No matching occurrence modulo AC found"
+ else "No such solution"))
+ )
+ ) goal
+
+let get k l = try Some (List.assoc k l) with Not_found -> None
+
+let get_lhs l = try ignore (List.assoc "in_right" l); false with Not_found -> true
+
+let aac_rewrite ~args =
+ aac_rewrite_wrap ~occ_subterm:(get "at" args) ~occ_sol:(get "subst" args) ~in_left:(get_lhs args)
+
+
+
+let rec add k x = function
+ | [] -> [k,x]
+ | k',_ as ky::q ->
+ if k'=k then Coq.user_error @@ Pp.strbrk ("redondant argument ("^k^")")
+ else ky::add k x q
+
+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
+
diff --git a/src/aac_rewrite.mli b/src/aac_rewrite.mli
new file mode 100644
index 0000000..80134af
--- /dev/null
+++ b/src/aac_rewrite.mli
@@ -0,0 +1,24 @@
+(***************************************************************************)
+(* 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 A or AC*)
+
+val aac_reflexivity : Coq.goal_sigma -> Proof_type.goal list Evd.sigma
+val aac_normalise : Coq.goal_sigma -> Proof_type.goal list Evd.sigma
+
+val aac_rewrite :
+ args:(string * int) list ->
+ ?abort:bool ->
+ EConstr.constr ->
+ ?l2r:bool ->
+ ?show:bool ->
+ ?strict:bool -> ?extra:EConstr.t -> Proof_type.tactic
+
+val add : string -> 'a -> (string * 'a) list -> (string * 'a) list
+
+val pr_aac_args : 'a -> 'b -> 'c -> (string * int) list -> Pp.t
diff --git a/src/coq.ml b/src/coq.ml
new file mode 100644
index 0000000..ae1803a
--- /dev/null
+++ b/src/coq.ml
@@ -0,0 +1,594 @@
+(***************************************************************************)
+(* 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 *)
+
+open Constr
+open EConstr
+open Names
+open Context.Rel.Declaration
+
+(* 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 =
+ UnivGen.constr_of_global (Coqlib.find_reference contrib dir s)
+
+let init_constant_constr dir s = find_constant contrib_name dir s
+
+let init_constant dir s = EConstr.of_constr (find_constant contrib_name dir s)
+
+(* A clause specifying that the [let] should not try to fold anything
+ in the goal *)
+let nowhere =
+ { Locus.onhyps = Some [];
+ Locus.concl_occs = Locus.NoOccurrences
+ }
+
+let retype c gl =
+ let sigma, _ = Tacmach.pf_apply Typing.type_of gl c in
+ Refiner.tclEVARS sigma gl
+
+let cps_mk_letin
+ (name:string)
+ (c: constr)
+ (k : constr -> Proof_type.tactic)
+: Proof_type.tactic =
+ fun goal ->
+ let name = (Id.of_string name) in
+ let name = Tactics.fresh_id Id.Set.empty name goal in
+ let letin = (Proofview.V82.of_tactic (Tactics.letin_tac None (Name name) c None nowhere)) in
+ Tacticals.tclTHENLIST [retype c; letin; (k (mkVar name))] goal
+
+(** {1 General functions} *)
+
+type goal_sigma = Proof_type.goal Evd.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 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 cps_resolve_one_typeclass ?error : types -> (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 -> CErrors.anomaly (Pp.str "Cannot resolve a typeclass : please report")
+ | Some x -> CErrors.user_err x
+ end
+ in
+ Tacticals.tclTHENLIST [Refiner.tclEVARS em; k c] goal
+ ) goal
+
+
+let nf_evar goal c : constr=
+ let evar_map = Tacmach.project goal in
+ Evarutil.nf_evar evar_map c
+
+ (* TODO: refactor following similar functions*)
+
+let evar_unit (gl : goal_sigma) (x : constr) : constr * goal_sigma =
+ let env = Tacmach.pf_env gl in
+ let evar_map = Tacmach.project gl in
+ let (em,x) = Evarutil.new_evar env evar_map x in
+ x,(goal_update gl em)
+
+let evar_binary (gl: goal_sigma) (x : constr) =
+ let env = Tacmach.pf_env gl in
+ let evar_map = Tacmach.project gl in
+ let ty = mkArrow x (mkArrow x x) in
+ let (em,x) = Evarutil.new_evar env evar_map ty in
+ 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 Sorts.prop)) in
+ let (em,r) = Evarutil.new_evar env evar_map 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 Sorts.prop)) in
+ let (em, r) = Evarutil.new_evar env em ty in
+ Tacticals.tclTHENLIST [Refiner.tclEVARS em; k r] goal
+ ) goal
+
+let decomp_term sigma c = kind sigma (Termops.strip_outer_cast sigma 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" ; "Numbers"; "BinNums"]
+ 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"; "Init"; "Datatypes"]
+ 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 that the term
+ remains typable*)
+let match_as_equation ?(context = Context.Rel.empty) goal equation : (constr*constr* Std.Relation.t) option =
+ let env = Tacmach.pf_env goal in
+ let env = EConstr.push_rel_context context env in
+ let evar_map = Tacmach.project goal in
+ begin
+ match decomp_term evar_map 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.unsafe_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 _ = Feedback.msg_notice (Pp.str (Printf.sprintf "%s:%fs" msg (Sys.time ()-. u))) in
+ r
+
+let tclDEBUG msg tac = fun gl ->
+ let _ = Feedback.msg_debug (Pp.str msg) in
+ tac gl
+
+let tclPRINT tac = fun gl ->
+ let env = Tacmach.pf_env gl in
+ let sigma = Tacmach.project gl in
+ let _ = Feedback.msg_notice (Printer.pr_econstr_env env sigma (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 =
+ CErrors.anomaly ~label:"[aac_tactics]" (Pp.str msg)
+
+let user_error msg =
+ CErrors.user_err Pp.(str "[aac_tactics] " ++ msg)
+
+let warning msg =
+ Feedback.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 : constr; (** the actual constr corresponding to the hypothese *)
+ hyptype : constr; (** the type of the hypothesis *)
+ context : EConstr.rel_context; (** the quantifications of the hypothese *)
+ body : constr; (** the body of the type of the hypothesis*)
+ rel : Std.Relation.t; (** the relation *)
+ left : constr; (** left hand side *)
+ right : 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_unsafe_type_of goal c in
+ let evar_map = Tacmach.project goal in
+ let (rel_context, body_type) = decompose_prod_assum evar_map ctype in
+ let rec check f e =
+ match decomp_term evar_map e with
+ | Rel i -> f (get_type (Context.Rel.lookup i rel_context))
+ | _ -> fold evar_map (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 @@ Pp.strbrk "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 @@ Pp.strbrk "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 : rel_context)
+ (subst : (int * constr) list)
+ env
+ em
+ : Evd.evar_map * 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
+ | 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 ->
+ let (em, r) = Evarutil.new_evar env em (Vars.substl acc (get_type t)) in
+ (em, r)
+ in
+ (EConstr.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-instantiated variables. *)
+
+let recompose_prod'
+ (context : rel_context)
+ (subst : (int *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 = map_type Termops.pop 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 = 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 (Vars.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 = applist (c,List.rev app) in
+ let c = 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 *constr) list)
+ (k :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 *constr) list)
+ (k :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 = applist (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
+ Proofview.V82.of_tactic begin
+ Equality.general_rewrite_bindings
+ hypinfo.l2r
+ Locus.AllOccurrences
+ true (* tell if existing evars must be frozen for instantiation *)
+ false
+ (rew,Tactypes.NoBindings)
+ true
+ end
+ else
+ Tacticals.tclIDTAC
+ in k tac
+ )
+
+
+end
+
+include Std
diff --git a/src/coq.mli b/src/coq.mli
new file mode 100644
index 0000000..9cf0db7
--- /dev/null
+++ b/src/coq.mli
@@ -0,0 +1,232 @@
+(***************************************************************************)
+(* 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_constr : string list -> string -> Constr.t
+val init_constant : string list -> string -> EConstr.constr
+
+(** {2 General purpose functions} *)
+
+type goal_sigma = Proof_type.goal Evd.sigma
+val resolve_one_typeclass : Proof_type.goal Evd.sigma -> EConstr.types -> EConstr.constr * goal_sigma
+val cps_resolve_one_typeclass: ?error:Pp.t -> EConstr.types -> (EConstr.constr -> Proof_type.tactic) -> Proof_type.tactic
+val nf_evar : goal_sigma -> EConstr.constr -> EConstr.constr
+val evar_unit :goal_sigma ->EConstr.constr -> EConstr.constr* goal_sigma
+val evar_binary: goal_sigma -> EConstr.constr -> EConstr.constr* goal_sigma
+val evar_relation: goal_sigma -> EConstr.constr -> EConstr.constr* goal_sigma
+val cps_evar_relation : EConstr.constr -> (EConstr.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 -> EConstr.constr -> ( EConstr.constr -> Proof_type.tactic) -> Proof_type.tactic
+
+val retype : EConstr.constr -> Proof_type.tactic
+
+val decomp_term : Evd.evar_map -> EConstr.constr -> (EConstr.constr , EConstr.types, EConstr.ESorts.t, EConstr.EInstance.t) Constr.kind_of_term
+val lapp : EConstr.constr lazy_t -> EConstr.constr array -> EConstr.constr
+
+(** {2 Bindings with Coq' Standard Library} *)
+
+(** Coq lists *)
+module List:
+sig
+ (** [of_list ty l] *)
+ val of_list:EConstr.constr ->EConstr.constr list ->EConstr.constr
+
+ (** [type_of_list ty] *)
+ val type_of_list:EConstr.constr ->EConstr.constr
+end
+
+(** Coq pairs *)
+module Pair:
+sig
+ val typ:EConstr.constr lazy_t
+ val pair:EConstr.constr lazy_t
+ val of_pair : EConstr.constr -> EConstr.constr -> EConstr.constr * EConstr.constr -> EConstr.constr
+end
+
+module Bool : sig
+ val typ : EConstr.constr lazy_t
+ val of_bool : bool -> EConstr.constr
+end
+
+
+module Comparison : sig
+ val typ : EConstr.constr lazy_t
+ val eq : EConstr.constr lazy_t
+ val lt : EConstr.constr lazy_t
+ val gt : EConstr.constr lazy_t
+end
+
+module Leibniz : sig
+ val eq_refl : EConstr.types -> EConstr.constr -> EConstr.constr
+end
+
+module Option : sig
+ val typ : EConstr.constr lazy_t
+ val some : EConstr.constr -> EConstr.constr -> EConstr.constr
+ val none : EConstr.constr -> EConstr.constr
+ val of_option : EConstr.constr -> EConstr.constr option -> EConstr.constr
+end
+
+(** Coq positive numbers (pos) *)
+module Pos:
+sig
+ val typ:EConstr.constr lazy_t
+ val of_int: int ->EConstr.constr
+end
+
+(** Coq unary numbers (peano) *)
+module Nat:
+sig
+ val typ:EConstr.constr lazy_t
+ val of_int: int ->EConstr.constr
+end
+
+(** Coq typeclasses *)
+module Classes:
+sig
+ val mk_morphism: EConstr.constr -> EConstr.constr -> EConstr.constr -> EConstr.constr
+ val mk_equivalence: EConstr.constr -> EConstr.constr -> EConstr.constr
+ val mk_reflexive: EConstr.constr -> EConstr.constr -> EConstr.constr
+ val mk_transitive: EConstr.constr -> EConstr.constr -> EConstr.constr
+end
+
+module Relation : sig
+ type t = {carrier : EConstr.constr; r : EConstr.constr;}
+ val make : EConstr.constr -> EConstr.constr -> t
+ val split : t -> EConstr.constr * EConstr.constr
+end
+
+module Transitive : sig
+ type t =
+ {
+ carrier : EConstr.constr;
+ leq : EConstr.constr;
+ transitive : EConstr.constr;
+ }
+ val make : EConstr.constr -> EConstr.constr -> EConstr.constr -> t
+ val infer : goal_sigma -> EConstr.constr -> EConstr.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 : EConstr.constr;
+ eq : EConstr.constr;
+ equivalence : EConstr.constr;
+ }
+ val make : EConstr.constr -> EConstr.constr -> EConstr.constr -> t
+ val infer : goal_sigma -> EConstr.constr -> EConstr.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 -> EConstr.constr * EConstr.constr * EConstr.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:EConstr.rel_context -> goal_sigma -> EConstr.constr -> (EConstr.constr * EConstr.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 : Pp.t -> '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 : EConstr.constr; (** the actual constr corresponding to the hypothese *)
+ hyptype : EConstr.constr; (** the type of the hypothesis *)
+ context : EConstr.rel_context; (** the quantifications of the hypothese *)
+ body : EConstr.constr; (** the body of the hypothese*)
+ rel : Relation.t; (** the relation *)
+ left : EConstr.constr; (** left hand side *)
+ right : EConstr.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 :EConstr.constr -> l2r:bool -> ?check_type:(EConstr.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 * EConstr.constr) list -> (EConstr.constr -> Proof_type.tactic) -> Proof_type.tactic
+
+(** build the constr to rewrite, in CPS style, with evars *)
+val build_with_evar : hypinfo -> (int * EConstr.constr) list -> (EConstr.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 * EConstr.constr) list -> (Proof_type.tactic -> Proof_type.tactic) -> Proof_type.tactic
+end
diff --git a/src/helper.ml b/src/helper.ml
new file mode 100644
index 0000000..c1cae2a
--- /dev/null
+++ b/src/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 env evd msg constr =
+ if printing then
+ ( Feedback.msg_notice (Pp.str (Printf.sprintf "=====%s====" msg));
+ Feedback.msg_notice (Printer.pr_econstr_env env evd constr);
+ )
+
+
+ let debug_exception msg e =
+ debug (msg ^ (Printexc.to_string e))
+
+
+end
diff --git a/src/helper.mli b/src/helper.mli
new file mode 100644
index 0000000..400e847
--- /dev/null
+++ b/src/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 : Environ.env -> Evd.evar_map -> string -> EConstr.constr -> unit
+
+ end
diff --git a/src/matcher.ml b/src/matcher.ml
new file mode 100644
index 0000000..cc66961
--- /dev/null
+++ b/src/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 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 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 -> CErrors.user_err (Pp.strbrk "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
+ Feedback.msg_warning
+ (Pp.str
+ "[aac_tactics] This pattern can be instantiated 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 instantiated 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/src/matcher.mli b/src/matcher.mli
new file mode 100644
index 0000000..a6b6f46
--- /dev/null
+++ b/src/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/src/print.ml b/src/print.ml
new file mode 100644
index 0000000..6800200
--- /dev/null
+++ b/src/print.ml
@@ -0,0 +1,104 @@
+(***************************************************************************)
+(* 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
+open Context.Rel.Declaration
+open Names
+
+type named_env = (Name.t * Terms.t) list
+
+
+
+(** {pp_env} prints a substitution mapping names to terms, using the
+provided printer *)
+let pp_env pt : named_env -> Pp.t = fun env ->
+ List.fold_left
+ (fun acc (v,t) ->
+ begin match v with
+ | Names.Name s -> str (Printf.sprintf "%s: " (Id.to_string 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.t = 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.t = fun m ->
+ let _,s = Search_monad.fold
+ (fun (size,context,envm) (n,acc) ->
+ let s = str (Printf.sprintf "occurrence %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 : EConstr.rel_context) goal =
+ if Search_monad.count m = 0
+ then
+ (
+ Tacticals.tclFAIL 0 (Pp.str "No subterm modulo AC") goal
+ )
+ else
+ let _ = Feedback.msg_notice (Pp.str "All solutions:") in
+ let m = Search_monad.(>>) m
+ (fun (i,t,envm) ->
+ let envm = Search_monad.(>>) envm ( fun env ->
+ 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) ->
+ get_name (Context.Rel.lookup v context), 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 env = Tacmach.pf_env goal in
+ let sigma = Tacmach.project goal in
+ let _ = Feedback.msg_notice
+ (pp_all
+ (fun t -> Printer.pr_letype_env env sigma (Theory.Trans.raw_constr_of_t ir rlt context t)) m
+ )
+ in
+ Tacticals.tclIDTAC goal
+
diff --git a/src/print.mli b/src/print.mli
new file mode 100644
index 0000000..5ca6e27
--- /dev/null
+++ b/src/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 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 ->
+ EConstr.rel_context ->
+ Proof_type.tactic
+
diff --git a/src/search_monad.ml b/src/search_monad.ml
new file mode 100644
index 0000000..09a6455
--- /dev/null
+++ b/src/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/src/search_monad.mli b/src/search_monad.mli
new file mode 100644
index 0000000..7e2a910
--- /dev/null
+++ b/src/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 <http://spivey.oriel.ox.ac.uk/mike/search-jfp.pdf> 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/src/theory.ml b/src/theory.ml
new file mode 100644
index 0000000..7871fe4
--- /dev/null
+++ b/src/theory.ml
@@ -0,0 +1,1153 @@
+(***************************************************************************)
+(* 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_rewrite.v}, therefore, it should
+ be of little interest to most readers.
+*)
+open EConstr
+
+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} *)
+
+
+ (* TODO module HMap = Hashtbl, du coup ? *)
+module HMap = Hashtbl.Make(Constr)
+
+let ac_theory_path = ["AAC_tactics"; "AAC"]
+let ac_util_path = ["AAC_tactics"; "Utils"]
+
+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 : 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 : 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 : constr) (unit : 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_util_path
+ 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: Constr.t; value: Constr.t ; morph: Constr.t}
+ 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; EConstr.of_constr s.ar;EConstr.of_constr s.value;EConstr.of_constr 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 : Constr.t;
+ compat : Constr.t;
+ assoc : Constr.t;
+ comm : Constr.t 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 -> constr = fun (rlt) s ->
+ let (x,r) = Coq.Relation.split rlt in
+ let comm_ty = Classes.Commutative.ty rlt (EConstr.of_constr s.value) in
+ mkApp (Lazy.force mkPack , [| x ; r;
+ EConstr.of_constr s.value;
+ EConstr.of_constr s.compat ;
+ EConstr.of_constr s.assoc;
+ Coq.Option.of_option comm_ty (Option.map EConstr.of_constr 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 : Constr.t; (* u *)
+ uf_idx : Constr.t;
+ uf_desc : Constr.t; (* Unit R (e_bin uf_idx) u *)
+ }
+
+ type pack = {
+ u_value : 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;
+ EConstr.of_constr unit_of.uf_idx;
+ EConstr.of_constr unit_of.uf_desc
+ |])
+
+ let mk_pack rlt e_bin pack : 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 =
+ CErrors.anomaly ~label:"aac_tactics" (Pp.str msg)
+
+let user_error msg =
+ CErrors.user_err Pp.(strbrk "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.t (* to avoid confusion in bloom *)
+
+ module PackHash =
+ struct
+ open Hashset.Combine
+
+ type t = pack
+
+ let eq_sym_pack p1 p2 =
+ let open Sym in
+ Constr.equal p1.ar p2.ar &&
+ Constr.equal p1.value p2.value &&
+ Constr.equal p1.morph p2.morph
+
+ let hash_sym_pack p =
+ let open Sym in
+ combine3 (Constr.hash p.ar) (Constr.hash p.value) (Constr.hash p.morph)
+
+ let eq_bin_pack p1 p2 =
+ let open Bin in
+ Constr.equal p1.value p2.value &&
+ Constr.equal p1.compat p2.compat &&
+ Constr.equal p1.assoc p2.assoc &&
+ Option.equal Constr.equal p1.comm p2.comm
+
+ let hash_bin_pack p =
+ let open Bin in
+ combine4 (Constr.hash p.value) (Constr.hash p.compat)
+ (Constr.hash p.assoc) (Option.hash Constr.hash p.comm)
+
+ let eq_unit_of u1 u2 =
+ let open Unit in
+ Constr.equal u1.uf_u u2.uf_u &&
+ Constr.equal u1.uf_idx u2.uf_idx &&
+ Constr.equal u1.uf_desc u2.uf_desc
+
+ let hash_unit_of u =
+ let open Unit in
+ combine3 (Constr.hash u.uf_u) (Constr.hash u.uf_idx)
+ (Constr.hash u.uf_desc)
+
+ let equal p1 p2 = match p1, p2 with
+ | Bin (p1, o1), Bin (p2, o2) ->
+ eq_bin_pack p1 p2 && Option.equal eq_unit_of o1 o2
+ | Sym p1, Sym p2 -> eq_sym_pack p1 p2
+ | Unit c1, Unit c2 -> Constr.equal c1 c2
+ | _ -> false
+
+ let hash p = match p with
+ | Bin (p, o) ->
+ combinesmall 1 (combine (hash_bin_pack p) (Option.hash hash_unit_of o))
+ | Sym p ->
+ combinesmall 2 (hash_sym_pack p)
+ | Unit c ->
+ combinesmall 3 (Constr.hash c)
+
+ end
+
+ module PackTable = Hashtbl.Make(PackHash)
+
+ (** discr is a map from {!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 : int PackTable.t;
+ bloom_back : (int, pack ) Hashtbl.t;
+ bloom_next : int ref;
+ }
+
+ let empty_envs () =
+ {
+ discr = HMap.create 17;
+ bloom = PackTable.create 17;
+ bloom_back = Hashtbl.create 17;
+ bloom_next = ref 1;
+ }
+
+
+
+ let add_bloom envs pack =
+ if PackTable.mem envs.bloom pack
+ then ()
+ else
+ let x = ! (envs.bloom_next) in
+ PackTable.add envs.bloom pack x;
+ Hashtbl.add envs.bloom_back x pack;
+ incr (envs.bloom_next)
+
+ let find_bloom envs pack =
+ try PackTable.find envs.bloom pack
+ with Not_found -> assert false
+
+ (*********************************************)
+ (* (\* Gather the occurring 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 -> 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 = EConstr.to_constr (Tacmach.project goal) op;
+ Bin.compat = EConstr.to_constr (Tacmach.project goal) proper;
+ Bin.assoc = EConstr.to_constr (Tacmach.project goal) assoc;
+ Bin.comm = Option.map (EConstr.to_constr (Tacmach.project goal)) 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 = EConstr.to_constr (Tacmach.project goal) 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 = EConstr.to_constr (Tacmach.project goal) op;
+ Unit.uf_desc = EConstr.to_constr (Tacmach.project goal) 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 : 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 = EConstr.to_constr (Tacmach.project goal) (Coq.Nat.of_int ar);
+ Sym.value= EConstr.to_constr (Tacmach.project goal) papp;
+ Sym.morph= EConstr.to_constr (Tacmach.project goal) 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 = 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 = 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 (EConstr.to_constr (Tacmach.project goal) 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 (EConstr.to_constr (Tacmach.project goal) 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 (EConstr.to_constr (Tacmach.project goal) 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 (Tacmach.project goal) x with
+ | Constr.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 : 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 = EConstr.to_constr ~abort_on_undefined_evars:(false)(Tacmach.project goal) (Coq.Nat.of_int ar);
+ Sym.value= EConstr.to_constr ~abort_on_undefined_evars:(false)(Tacmach.project goal) papp;
+ Sym.morph= EConstr.to_constr ~abort_on_undefined_evars:(false)(Tacmach.project goal) 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 (EConstr.to_constr ~abort_on_undefined_evars:(false) (Tacmach.project goal) 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 (EConstr.to_constr ~abort_on_undefined_evars:(false) (Tacmach.project goal) 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 (EConstr.to_constr ~abort_on_undefined_evars:(false) (Tacmach.project goal) 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 (EConstr.to_constr ~abort_on_undefined_evars:(false) (Tacmach.project goal) (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 (Tacmach.project goal) x with
+ | Constr.App (t,ca) ->
+ discriminate goal envs rlt t ca
+ | _ -> discriminate goal envs rlt x [| |]
+ with
+ | NotReflexive -> user_error @@ Pp.strbrk "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 @@ Pp.strbrk "Cannot handle this kind of hypotheses (variables occurring 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 (Tacmach.project goal) x with
+ | Constr.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 (EConstr.of_constr (Constr.mkApp (l, [| Constr.mkRel 0;Constr.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 * 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.t) 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 = PackTable.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 Constr.equal (unit_of.Unit.uf_u) u
+ then
+ {unit_of with
+ Unit.uf_idx = EConstr.to_constr (Tacmach.project goal) (Coq.Pos.of_int nop)} :: acc
+ else
+ acc
+ )
+ [] bin
+ in
+ (n,{
+ Unit.u_value = EConstr.of_constr 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) : 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 (EConstr.of_constr 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 (EConstr.of_constr 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 (EConstr.of_constr s.Sym.value, Array.map aux t)
+ | _ -> assert false
+ end
+ | Matcher.Terms.Unit x ->
+ begin match Hashtbl.find ir.packer x with
+ | Unit s -> EConstr.of_constr 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 = Context.Rel.lookup t context in
+ cap (mkProd_or_LetIn i c) q
+ in
+ let t,indices = raw_constr_of_t_debruijn ir t in
+ 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 : constr;
+ env_bin : constr;
+ env_units : constr; (* the [idx -> X:constr] *)
+ }
+
+
+ type sigma_maps = {
+ sym_to_pos : int -> constr;
+ bin_to_pos : int -> constr;
+ units_to_pos : int -> 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 = EConstr.to_constr (Tacmach.project goal) op;
+ Bin.compat = EConstr.to_constr (Tacmach.project goal) compat;
+ Bin.assoc = EConstr.to_constr (Tacmach.project goal) assoc;
+ Bin.comm = None
+ }
+ with Not_found -> user_error @@ Pp.strbrk "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/src/theory.mli b/src/theory.mli
new file mode 100644
index 0000000..e7bfbfe
--- /dev/null
+++ b/src/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_rewrite.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_rewrite.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:EConstr.constr -> (EConstr.constr * int) list ->EConstr.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: EConstr.constr ->EConstr.constr ->EConstr.constr ->EConstr.constr ->EConstr.constr
+
+ (** [empty ty] create an empty map of type [ty] *)
+ val empty: EConstr.constr ->EConstr.constr
+
+ (** [of_list ty null l] translates an OCaml association list into a Coq one *)
+ val of_list: EConstr.constr -> EConstr.constr -> (int * EConstr.constr ) list -> EConstr.constr
+
+ (** [to_fun ty null map] converts a Coq association list into a Coq function (with default value [null]) *)
+ val to_fun: EConstr.constr ->EConstr.constr ->EConstr.constr ->EConstr.constr
+end
+
+
+(** Dynamically typed morphisms *)
+module Sym:
+sig
+ (** mimics the Coq record [Sym.pack] *)
+ type pack = {ar: Constr.t; value: Constr.t ; morph: Constr.t}
+
+ val typ: EConstr.constr lazy_t
+
+
+ (** [mk_pack rlt (ar,value,morph)] *)
+ val mk_pack: Coq.Relation.t -> pack -> EConstr.constr
+
+ (** [null] builds a dummy (identity) symbol, given an {!Coq.Relation.t} *)
+ val null: Coq.Relation.t -> EConstr.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 : EConstr.constr Lazy.t
+ val lift_proj_equivalence : EConstr.constr Lazy.t
+ val lift_transitivity_left : EConstr.constr Lazy.t
+ val lift_transitivity_right : EConstr.constr Lazy.t
+ val lift_reflexivity : EConstr.constr Lazy.t
+ (** The evaluation fonction, used to convert a reified coq term to a
+ raw coq term *)
+ val eval: EConstr.constr lazy_t
+
+ (** The main lemma of our theory, that is
+ [compare (norm u) (norm v) = Eq -> eval u == eval v] *)
+ val decide_thm:EConstr.constr lazy_t
+
+ val lift_normalise_thm : EConstr.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 -> (EConstr.constr * EConstr.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 -> Constr.t -> 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 -> EConstr.rel_context -> Matcher.Terms.t -> EConstr.constr
+
+ (** {2 Building reified terms} *)
+
+ (** The reification environments, as Coq constrs *)
+
+ type sigmas = {
+ env_sym : EConstr.constr;
+ env_bin : EConstr.constr;
+ env_units : EConstr.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 -> EConstr.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 -> EConstr.constr
+
+end
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-06 07:01:22 +0000