src/Sequents/prover.ML
changeset 55228 901a6696cdd8
parent 38500 d5477ee35820
child 56491 a8ccf3d6a6e4
--- a/src/Sequents/prover.ML	Sat Feb 01 00:32:32 2014 +0000
+++ b/src/Sequents/prover.ML	Sat Feb 01 17:56:03 2014 +0100
@@ -5,54 +5,114 @@
 Simple classical reasoner for the sequent calculus, based on "theorem packs".
 *)
 
+signature CLA =
+sig
+  type pack
+  val empty_pack: pack
+  val get_pack: Proof.context -> pack
+  val put_pack: pack -> Proof.context -> Proof.context
+  val pretty_pack: Proof.context -> Pretty.T
+  val add_safe: thm -> Proof.context -> Proof.context
+  val add_unsafe: thm -> Proof.context -> Proof.context
+  val safe_add: attribute
+  val unsafe_add: attribute
+  val method: (Proof.context -> int -> tactic) -> (Proof.context -> Proof.method) context_parser
+  val trace: bool Config.T
+  val forms_of_seq: term -> term list
+  val safe_tac: Proof.context -> int -> tactic
+  val step_tac: Proof.context -> int -> tactic
+  val pc_tac: Proof.context -> int -> tactic
+  val fast_tac: Proof.context -> int -> tactic
+  val best_tac: Proof.context -> int -> tactic
+end;
 
-(*Higher precedence than := facilitates use of references*)
-infix 4 add_safes add_unsafes;
-
-structure Cla =
+structure Cla: CLA =
 struct
 
-datatype pack = Pack of thm list * thm list;
-
-val trace = Unsynchronized.ref false;
+(** rule declarations **)
 
 (*A theorem pack has the form  (safe rules, unsafe rules)
   An unsafe rule is incomplete or introduces variables in subgoals,
   and is tried only when the safe rules are not applicable.  *)
 
-fun less (rl1,rl2) = (nprems_of rl1) < (nprems_of rl2);
+fun less (rl1, rl2) = Thm.nprems_of rl1 < Thm.nprems_of rl2;
+val sort_rules = sort (make_ord less);
 
-val empty_pack = Pack([],[]);
+datatype pack = Pack of thm list * thm list;
+
+val empty_pack = Pack ([], []);
 
-fun warn_duplicates [] = []
-  | warn_duplicates dups =
-      (warning (cat_lines ("Ignoring duplicate theorems:" ::
-          map Display.string_of_thm_without_context dups));
-       dups);
+structure Pack = Generic_Data
+(
+  type T = pack;
+  val empty = empty_pack;
+  val extend = I;
+  fun merge (Pack (safes, unsafes), Pack (safes', unsafes')) =
+    Pack
+     (sort_rules (Thm.merge_thms (safes, safes')),
+      sort_rules (Thm.merge_thms (unsafes, unsafes')));
+);
 
-fun (Pack(safes,unsafes)) add_safes ths   = 
-    let val dups = warn_duplicates (inter Thm.eq_thm_prop ths safes)
-        val ths' = subtract Thm.eq_thm_prop dups ths
-    in
-        Pack(sort (make_ord less) (ths'@safes), unsafes)
-    end;
+val put_pack = Context.proof_map o Pack.put;
+val get_pack = Pack.get o Context.Proof;
+fun get_rules ctxt = let val Pack rules = get_pack ctxt in rules end;
+
+
+(* print pack *)
 
-fun (Pack(safes,unsafes)) add_unsafes ths = 
-    let val dups = warn_duplicates (inter Thm.eq_thm_prop unsafes ths)
-        val ths' = subtract Thm.eq_thm_prop dups ths
-    in
-        Pack(safes, sort (make_ord less) (ths'@unsafes))
-    end;
+fun pretty_pack ctxt =
+  let val (safes, unsafes) = get_rules ctxt in
+    Pretty.chunks
+     [Pretty.big_list "safe rules:" (map (Display.pretty_thm ctxt) safes),
+      Pretty.big_list "unsafe rules:" (map (Display.pretty_thm ctxt) unsafes)]
+  end;
 
-fun merge_pack (Pack(safes,unsafes), Pack(safes',unsafes')) =
-        Pack(sort (make_ord less) (safes@safes'), 
-             sort (make_ord less) (unsafes@unsafes'));
+val _ =
+  Outer_Syntax.command @{command_spec "print_pack"} "print pack of classical rules"
+    (Scan.succeed (Toplevel.keep (Pretty.writeln o pretty_pack o Toplevel.context_of)));
 
 
-fun print_pack (Pack(safes,unsafes)) =
-  writeln (cat_lines
-   (["Safe rules:"] @ map Display.string_of_thm_without_context safes @
-    ["Unsafe rules:"] @ map Display.string_of_thm_without_context unsafes));
+(* declare rules *)
+
+fun add_rule which th context = context |> Pack.map (fn Pack rules =>
+  Pack (rules |> which (fn ths =>
+    if member Thm.eq_thm_prop ths th then
+      let
+        val ctxt = Context.proof_of context;
+        val _ =
+          if Context_Position.is_visible ctxt then
+            warning ("Ignoring duplicate theorems:\n" ^ Display.string_of_thm ctxt th)
+          else ();
+      in ths end
+    else sort_rules (th :: ths))));
+
+val add_safe = Context.proof_map o add_rule apfst;
+val add_unsafe = Context.proof_map o add_rule apsnd;
+
+
+(* attributes *)
+
+val safe_add = Thm.declaration_attribute (add_rule apfst);
+val unsafe_add = Thm.declaration_attribute (add_rule apsnd);
+
+val _ = Theory.setup
+  (Attrib.setup @{binding safe} (Scan.succeed safe_add) "" #>
+   Attrib.setup @{binding unsafe} (Scan.succeed unsafe_add) "");
+
+
+(* proof method syntax *)
+
+fun method tac =
+  Method.sections
+   [Args.$$$ "add" -- Args.bang_colon >> K (I, safe_add),
+    Args.$$$ "add" -- Args.colon >> K (I, unsafe_add)]
+  >> K (SIMPLE_METHOD' o tac);
+
+
+(** tactics **)
+
+val trace = Attrib.setup_config_bool @{binding cla_trace} (K false);
+
 
 (*Returns the list of all formulas in the sequent*)
 fun forms_of_seq (Const(@{const_name "SeqO'"},_) $ P $ u) = P :: forms_of_seq u
@@ -65,11 +125,10 @@
   -- checks that each concl formula looks like some subgoal formula.
   It SHOULD check order as well, using recursion rather than forall/exists*)
 fun could_res (seqp,seqc) =
-      forall (fn Qc => exists (fn Qp => Term.could_unify (Qp,Qc)) 
+      forall (fn Qc => exists (fn Qp => Term.could_unify (Qp,Qc))
                               (forms_of_seq seqp))
              (forms_of_seq seqc);
 
-
 (*Tests whether two sequents or pairs of sequents could be resolved*)
 fun could_resolve_seq (prem,conc) =
   case (prem,conc) of
@@ -102,7 +161,7 @@
   The list of rules is partitioned into 0, 1, 2 premises.
   The resulting tactic, gtac, tries to resolve with rules.
   If successful, it recursively applies nextac to the new subgoals only.
-  Else fails.  (Treatment of goals due to Ph. de Groote) 
+  Else fails.  (Treatment of goals due to Ph. de Groote)
   Bind (RESOLVE_THEN rules) to a variable: it preprocesses the rules. *)
 
 (*Takes rule lists separated in to 0, 1, 2, >2 premises.
@@ -112,7 +171,7 @@
 fun RESOLVE_THEN rules =
   let val [rls0,rls1,rls2] = partition_list has_prems 0 2 rules;
       fun tac nextac i state = state |>
-             (filseq_resolve_tac rls0 9999 i 
+             (filseq_resolve_tac rls0 9999 i
               ORELSE
               (DETERM(filseq_resolve_tac rls1 9999 i) THEN  TRY(nextac i))
               ORELSE
@@ -123,50 +182,54 @@
 
 
 (*repeated resolution applied to the designated goal*)
-fun reresolve_tac rules = 
-  let val restac = RESOLVE_THEN rules;  (*preprocessing done now*)
-      fun gtac i = restac gtac i
-  in  gtac  end; 
+fun reresolve_tac rules =
+  let
+    val restac = RESOLVE_THEN rules;  (*preprocessing done now*)
+    fun gtac i = restac gtac i;
+  in gtac end;
 
 (*tries the safe rules repeatedly before the unsafe rules. *)
-fun repeat_goal_tac (Pack(safes,unsafes)) = 
-  let val restac  =    RESOLVE_THEN safes
-      and lastrestac = RESOLVE_THEN unsafes;
-      fun gtac i = restac gtac i  
-                   ORELSE  (if !trace then
-                                (print_tac "" THEN lastrestac gtac i)
-                            else lastrestac gtac i)
-  in  gtac  end; 
+fun repeat_goal_tac ctxt =
+  let
+    val (safes, unsafes) = get_rules ctxt;
+    val restac = RESOLVE_THEN safes;
+    val lastrestac = RESOLVE_THEN unsafes;
+    fun gtac i =
+      restac gtac i ORELSE
+       (if Config.get ctxt trace then print_tac "" THEN lastrestac gtac i
+        else lastrestac gtac i)
+  in gtac end;
 
 
 (*Tries safe rules only*)
-fun safe_tac (Pack(safes,unsafes)) = reresolve_tac safes;
-
-val safe_goal_tac = safe_tac;   (*backwards compatibility*)
+fun safe_tac ctxt = reresolve_tac (#1 (get_rules ctxt));
 
 (*Tries a safe rule or else a unsafe rule.  Single-step for tracing. *)
-fun step_tac (pack as Pack(safes,unsafes)) =
-    safe_tac pack  ORELSE'
-    filseq_resolve_tac unsafes 9999;
+fun step_tac ctxt =
+  safe_tac ctxt ORELSE' filseq_resolve_tac (#2 (get_rules ctxt)) 9999;
 
 
 (* Tactic for reducing a goal, using Predicate Calculus rules.
    A decision procedure for Propositional Calculus, it is incomplete
-   for Predicate-Calculus because of allL_thin and exR_thin.  
+   for Predicate-Calculus because of allL_thin and exR_thin.
    Fails if it can do nothing.      *)
-fun pc_tac pack = SELECT_GOAL (DEPTH_SOLVE (repeat_goal_tac pack 1));
+fun pc_tac ctxt = SELECT_GOAL (DEPTH_SOLVE (repeat_goal_tac ctxt 1));
 
 
-(*The following two tactics are analogous to those provided by 
+(*The following two tactics are analogous to those provided by
   Provers/classical.  In fact, pc_tac is usually FASTER than fast_tac!*)
-fun fast_tac pack =
-  SELECT_GOAL (DEPTH_SOLVE (step_tac pack 1));
+fun fast_tac ctxt =
+  SELECT_GOAL (DEPTH_SOLVE (step_tac ctxt 1));
+
+fun best_tac ctxt  =
+  SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, size_of_thm) (step_tac ctxt 1));
 
-fun best_tac pack  = 
-  SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, size_of_thm) 
-               (step_tac pack 1));
+val _ = Theory.setup
+  (Method.setup @{binding safe} (method safe_tac) "" #>
+   Method.setup @{binding step} (method step_tac) "" #>
+   Method.setup @{binding pc} (method pc_tac) "" #>
+   Method.setup @{binding fast} (method fast_tac) "" #>
+   Method.setup @{binding best} (method best_tac) "");
 
 end;
 
-
-open Cla;