1.1 --- a/src/HOL/Tools/Meson/meson.ML	Mon Jul 25 14:10:12 2011 +0200
     1.2 +++ b/src/HOL/Tools/Meson/meson.ML	Mon Jul 25 14:10:12 2011 +0200
     1.3 @@ -14,7 +14,9 @@
     1.4    val term_pair_of: indexname * (typ * 'a) -> term * 'a
     1.5    val size_of_subgoals: thm -> int
     1.6    val has_too_many_clauses: Proof.context -> term -> bool
     1.7 -  val make_cnf: thm list -> thm -> Proof.context -> thm list * Proof.context
     1.8 +  val make_cnf:
     1.9 +    thm list -> thm -> Proof.context
    1.10 +    -> Proof.context -> thm list * Proof.context
    1.11    val finish_cnf: thm list -> thm list
    1.12    val unfold_set_const_simps : Proof.context -> thm list
    1.13    val presimplified_consts : Proof.context -> string list
    1.14 @@ -26,8 +28,8 @@
    1.15    val extensionalize_conv : Proof.context -> conv
    1.16    val extensionalize_theorem : Proof.context -> thm -> thm
    1.17    val is_fol_term: theory -> term -> bool
    1.18 -  val make_clauses_unsorted: thm list -> thm list
    1.19 -  val make_clauses: thm list -> thm list
    1.20 +  val make_clauses_unsorted: Proof.context -> thm list -> thm list
    1.21 +  val make_clauses: Proof.context -> thm list -> thm list
    1.22    val make_horns: thm list -> thm list
    1.23    val best_prolog_tac: (thm -> int) -> thm list -> tactic
    1.24    val depth_prolog_tac: thm list -> tactic
    1.25 @@ -366,18 +368,18 @@
    1.26  (* Conjunctive normal form, adding clauses from th in front of ths (for foldr).
    1.27     Strips universal quantifiers and breaks up conjunctions.
    1.28     Eliminates existential quantifiers using Skolemization theorems. *)
    1.29 -fun cnf old_skolem_ths ctxt (th, ths) =
    1.30 -  let val ctxtr = Unsynchronized.ref ctxt   (* FIXME ??? *)
    1.31 +fun cnf old_skolem_ths ctxt ctxt0 (th, ths) =
    1.32 +  let val ctxt0r = Unsynchronized.ref ctxt0   (* FIXME ??? *)
    1.33        fun cnf_aux (th,ths) =
    1.34          if not (can HOLogic.dest_Trueprop (prop_of th)) then ths (*meta-level: ignore*)
    1.35          else if not (has_conns [@{const_name All}, @{const_name Ex}, @{const_name HOL.conj}] (prop_of th))
    1.36 -        then nodups ctxt th :: ths (*no work to do, terminate*)
    1.37 +        then nodups ctxt0 th :: ths (*no work to do, terminate*)
    1.38          else case head_of (HOLogic.dest_Trueprop (concl_of th)) of
    1.39              Const (@{const_name HOL.conj}, _) => (*conjunction*)
    1.40                  cnf_aux (th RS conjunct1, cnf_aux (th RS conjunct2, ths))
    1.41            | Const (@{const_name All}, _) => (*universal quantifier*)
    1.42 -                let val (th',ctxt') = freeze_spec th (!ctxtr)
    1.43 -                in  ctxtr := ctxt'; cnf_aux (th', ths) end
    1.44 +                let val (th',ctxt0') = freeze_spec th (!ctxt0r)
    1.45 +                in  ctxt0r := ctxt0'; cnf_aux (th', ths) end
    1.46            | Const (@{const_name Ex}, _) =>
    1.47                (*existential quantifier: Insert Skolem functions*)
    1.48                cnf_aux (apply_skolem_theorem (th, old_skolem_ths), ths)
    1.49 @@ -388,15 +390,17 @@
    1.50                    Misc_Legacy.METAHYPS (resop cnf_nil) 1 THEN
    1.51                     (fn st' => st' |> Misc_Legacy.METAHYPS (resop cnf_nil) 1)
    1.52                in  Seq.list_of (tac (th RS disj_forward)) @ ths  end
    1.53 -          | _ => nodups ctxt th :: ths  (*no work to do*)
    1.54 +          | _ => nodups ctxt0 th :: ths  (*no work to do*)
    1.55        and cnf_nil th = cnf_aux (th,[])
    1.56        val cls =
    1.57 -            if has_too_many_clauses ctxt (concl_of th)
    1.58 -            then (trace_msg ctxt (fn () => "cnf is ignoring: " ^ Display.string_of_thm ctxt th); ths)
    1.59 -            else cnf_aux (th,ths)
    1.60 -  in  (cls, !ctxtr)  end;
    1.61 -
    1.62 -fun make_cnf old_skolem_ths th ctxt = cnf old_skolem_ths ctxt (th, [])
    1.63 +        if has_too_many_clauses ctxt (concl_of th) then
    1.64 +          (trace_msg ctxt (fn () =>
    1.65 +               "cnf is ignoring: " ^ Display.string_of_thm ctxt0 th); ths)
    1.66 +        else
    1.67 +          cnf_aux (th, ths)
    1.68 +  in (cls, !ctxt0r) end
    1.69 +fun make_cnf old_skolem_ths th ctxt ctxt0 =
    1.70 +  cnf old_skolem_ths ctxt ctxt0 (th, [])
    1.71  
    1.72  (*Generalization, removal of redundant equalities, removal of tautologies.*)
    1.73  fun finish_cnf ths = filter (not o is_taut) (map refl_clause ths);
    1.74 @@ -657,15 +661,15 @@
    1.75                                            Display.string_of_thm ctxt th)
    1.76                                     | _ => ()))
    1.77  
    1.78 -fun add_clauses th cls =
    1.79 +fun add_clauses ctxt th cls =
    1.80    let val ctxt0 = Variable.global_thm_context th
    1.81 -      val (cnfs, ctxt) = make_cnf [] th ctxt0
    1.82 +      val (cnfs, ctxt) = make_cnf [] th ctxt ctxt0
    1.83    in Variable.export ctxt ctxt0 cnfs @ cls end;
    1.84  
    1.85  (*Make clauses from a list of theorems, previously Skolemized and put into nnf.
    1.86    The resulting clauses are HOL disjunctions.*)
    1.87 -fun make_clauses_unsorted ths = fold_rev add_clauses ths [];
    1.88 -val make_clauses = sort_clauses o make_clauses_unsorted;
    1.89 +fun make_clauses_unsorted ctxt ths = fold_rev (add_clauses ctxt) ths [];
    1.90 +val make_clauses = sort_clauses oo make_clauses_unsorted;
    1.91  
    1.92  (*Convert a list of clauses (disjunctions) to Horn clauses (contrapositives)*)
    1.93  fun make_horns ths =
    1.94 @@ -703,12 +707,13 @@
    1.95  (** Best-first search versions **)
    1.96  
    1.97  (*ths is a list of additional clauses (HOL disjunctions) to use.*)
    1.98 -fun best_meson_tac sizef =
    1.99 -  MESON all_tac make_clauses
   1.100 +fun best_meson_tac sizef ctxt =
   1.101 +  MESON all_tac (make_clauses ctxt)
   1.102      (fn cls =>
   1.103           THEN_BEST_FIRST (resolve_tac (gocls cls) 1)
   1.104                           (has_fewer_prems 1, sizef)
   1.105 -                         (prolog_step_tac (make_horns cls) 1));
   1.106 +                         (prolog_step_tac (make_horns cls) 1))
   1.107 +    ctxt
   1.108  
   1.109  (*First, breaks the goal into independent units*)
   1.110  fun safe_best_meson_tac ctxt =
   1.111 @@ -716,10 +721,10 @@
   1.112  
   1.113  (** Depth-first search version **)
   1.114  
   1.115 -val depth_meson_tac =
   1.116 -  MESON all_tac make_clauses
   1.117 -    (fn cls => EVERY [resolve_tac (gocls cls) 1, depth_prolog_tac (make_horns cls)]);
   1.118 -
   1.119 +fun depth_meson_tac ctxt =
   1.120 +  MESON all_tac (make_clauses ctxt)
   1.121 +    (fn cls => EVERY [resolve_tac (gocls cls) 1, depth_prolog_tac (make_horns cls)])
   1.122 +    ctxt
   1.123  
   1.124  (** Iterative deepening version **)
   1.125  
   1.126 @@ -737,7 +742,7 @@
   1.127  fun iter_deepen_prolog_tac horns =
   1.128      ITER_DEEPEN iter_deepen_limit (has_fewer_prems 1) (prolog_step_tac' horns);
   1.129  
   1.130 -fun iter_deepen_meson_tac ctxt ths = ctxt |> MESON all_tac make_clauses
   1.131 +fun iter_deepen_meson_tac ctxt ths = ctxt |> MESON all_tac (make_clauses ctxt)
   1.132    (fn cls =>
   1.133      (case (gocls (cls @ ths)) of
   1.134        [] => no_tac  (*no goal clauses*)

     2.1 --- a/src/HOL/Tools/Meson/meson_clausify.ML	Mon Jul 25 14:10:12 2011 +0200
     2.2 +++ b/src/HOL/Tools/Meson/meson_clausify.ML	Mon Jul 25 14:10:12 2011 +0200
     2.3 @@ -373,7 +373,7 @@
     2.4      fun clausify th =
     2.5        make_cnf (if new_skolemizer orelse null choice_ths then []
     2.6                  else map (old_skolem_theorem_from_def thy) (old_skolem_defs th))
     2.7 -               th ctxt
     2.8 +               th ctxt ctxt
     2.9      val (cnf_ths, ctxt) = clausify nnf_th
    2.10      fun intr_imp ct th =
    2.11        Thm.instantiate ([], map (pairself (cterm_of thy))

     3.1 --- a/src/HOL/Tools/Metis/metis_tactics.ML	Mon Jul 25 14:10:12 2011 +0200
     3.2 +++ b/src/HOL/Tools/Metis/metis_tactics.ML	Mon Jul 25 14:10:12 2011 +0200
     3.3 @@ -189,9 +189,9 @@
     3.4                   quote (method_call_for_type_enc fallback_type_syss) ^ "...");
     3.5              FOL_SOLVE fallback_type_syss ctxt cls ths0)
     3.6  
     3.7 -val neg_clausify =
     3.8 +fun neg_clausify ctxt =
     3.9    single
    3.10 -  #> Meson.make_clauses_unsorted
    3.11 +  #> Meson.make_clauses_unsorted ctxt
    3.12    #> map Meson_Clausify.introduce_combinators_in_theorem
    3.13    #> Meson.finish_cnf
    3.14  
    3.15 @@ -217,7 +217,7 @@
    3.16        verbose_warning ctxt "Proof state contains the universal sort {}"
    3.17      else
    3.18        ();
    3.19 -    Meson.MESON (preskolem_tac ctxt) (maps neg_clausify) tac ctxt i st0
    3.20 +    Meson.MESON (preskolem_tac ctxt) (maps (neg_clausify ctxt)) tac ctxt i st0
    3.21    end
    3.22  
    3.23  fun metis_tac [] = generic_metis_tac partial_type_syss