src/HOL/Tools/metis_tools.ML
changeset 32955 4a78daeb012b
parent 32952 aeb1e44fbc19
child 32956 c39860141415
     1.1 --- a/src/HOL/Tools/metis_tools.ML	Fri Oct 16 00:26:19 2009 +0200
     1.2 +++ b/src/HOL/Tools/metis_tools.ML	Fri Oct 16 10:45:10 2009 +0200
     1.3 @@ -7,6 +7,7 @@
     1.4  
     1.5  signature METIS_TOOLS =
     1.6  sig
     1.7 +  val trace: bool Unsynchronized.ref
     1.8    val type_lits: bool Config.T
     1.9    val metis_tac: Proof.context -> thm list -> int -> tactic
    1.10    val metisF_tac: Proof.context -> thm list -> int -> tactic
    1.11 @@ -17,6 +18,9 @@
    1.12  structure MetisTools: METIS_TOOLS =
    1.13  struct
    1.14  
    1.15 +  val trace = Unsynchronized.ref false;
    1.16 +  fun trace_msg msg = if ! trace then tracing (msg ()) else ();
    1.17 +
    1.18    structure Recon = ResReconstruct;
    1.19  
    1.20    val (type_lits, type_lits_setup) = Attrib.config_bool "metis_type_lits" true;
    1.21 @@ -221,7 +225,7 @@
    1.22    (*Maps metis terms to isabelle terms*)
    1.23    fun fol_term_to_hol_RAW ctxt fol_tm =
    1.24      let val thy = ProofContext.theory_of ctxt
    1.25 -        val _ = Output.debug (fn () => "fol_term_to_hol: " ^ Metis.Term.toString fol_tm)
    1.26 +        val _ = trace_msg (fn () => "fol_term_to_hol: " ^ Metis.Term.toString fol_tm)
    1.27          fun tm_to_tt (Metis.Term.Var v) =
    1.28                 (case Recon.strip_prefix ResClause.tvar_prefix v of
    1.29                      SOME w => Type (Recon.make_tvar w)
    1.30 @@ -276,7 +280,7 @@
    1.31  
    1.32    (*Maps fully-typed metis terms to isabelle terms*)
    1.33    fun fol_term_to_hol_FT ctxt fol_tm =
    1.34 -    let val _ = Output.debug (fn () => "fol_term_to_hol_FT: " ^ Metis.Term.toString fol_tm)
    1.35 +    let val _ = trace_msg (fn () => "fol_term_to_hol_FT: " ^ Metis.Term.toString fol_tm)
    1.36          fun cvt (Metis.Term.Fn ("ti", [Metis.Term.Var v, ty])) =
    1.37                 (case Recon.strip_prefix ResClause.schematic_var_prefix v of
    1.38                      SOME w =>  mk_var(w, dummyT)
    1.39 @@ -303,8 +307,8 @@
    1.40                  | NONE => (*Not a constant. Is it a fixed variable??*)
    1.41                case Recon.strip_prefix ResClause.fixed_var_prefix x of
    1.42                    SOME v => Free (v, dummyT)
    1.43 -                | NONE =>  (Output.debug (fn () => "fol_term_to_hol_FT bad const: " ^ x); fol_term_to_hol_RAW ctxt t))
    1.44 -          | cvt t = (Output.debug (fn () => "fol_term_to_hol_FT bad term: " ^ Metis.Term.toString t); fol_term_to_hol_RAW ctxt t)
    1.45 +                | NONE =>  (trace_msg (fn () => "fol_term_to_hol_FT bad const: " ^ x); fol_term_to_hol_RAW ctxt t))
    1.46 +          | cvt t = (trace_msg (fn () => "fol_term_to_hol_FT bad term: " ^ Metis.Term.toString t); fol_term_to_hol_RAW ctxt t)
    1.47      in  cvt fol_tm   end;
    1.48  
    1.49    fun fol_term_to_hol ctxt FO = fol_term_to_hol_RAW ctxt
    1.50 @@ -313,10 +317,10 @@
    1.51  
    1.52    fun fol_terms_to_hol ctxt mode fol_tms =
    1.53      let val ts = map (fol_term_to_hol ctxt mode) fol_tms
    1.54 -        val _ = Output.debug (fn () => "  calling type inference:")
    1.55 -        val _ = app (fn t => Output.debug (fn () => Syntax.string_of_term ctxt t)) ts
    1.56 +        val _ = trace_msg (fn () => "  calling type inference:")
    1.57 +        val _ = app (fn t => trace_msg (fn () => Syntax.string_of_term ctxt t)) ts
    1.58          val ts' = infer_types ctxt ts;
    1.59 -        val _ = app (fn t => Output.debug
    1.60 +        val _ = app (fn t => trace_msg
    1.61                        (fn () => "  final term: " ^ Syntax.string_of_term ctxt t ^
    1.62                                  "  of type  " ^ Syntax.string_of_typ ctxt (type_of t)))
    1.63                      ts'
    1.64 @@ -333,9 +337,9 @@
    1.65  
    1.66    (*for debugging only*)
    1.67    fun print_thpair (fth,th) =
    1.68 -    (Output.debug (fn () => "=============================================");
    1.69 -     Output.debug (fn () => "Metis: " ^ Metis.Thm.toString fth);
    1.70 -     Output.debug (fn () => "Isabelle: " ^ Display.string_of_thm_without_context th));
    1.71 +    (trace_msg (fn () => "=============================================");
    1.72 +     trace_msg (fn () => "Metis: " ^ Metis.Thm.toString fth);
    1.73 +     trace_msg (fn () => "Isabelle: " ^ Display.string_of_thm_without_context th));
    1.74  
    1.75    fun lookth thpairs (fth : Metis.Thm.thm) =
    1.76      valOf (AList.lookup (uncurry Metis.Thm.equal) thpairs fth)
    1.77 @@ -374,7 +378,7 @@
    1.78                    val t = fol_term_to_hol ctxt mode y (*we call infer_types below*)
    1.79                in  SOME (cterm_of thy (Var v), t)  end
    1.80                handle Option =>
    1.81 -                  (Output.debug (fn() => "List.find failed for the variable " ^ x ^
    1.82 +                  (trace_msg (fn() => "List.find failed for the variable " ^ x ^
    1.83                                           " in " ^ Display.string_of_thm ctxt i_th);
    1.84                     NONE)
    1.85          fun remove_typeinst (a, t) =
    1.86 @@ -383,13 +387,13 @@
    1.87                  | NONE   => case Recon.strip_prefix ResClause.tvar_prefix a of
    1.88                    SOME _ => NONE          (*type instantiations are forbidden!*)
    1.89                  | NONE   => SOME (a,t)    (*internal Metis var?*)
    1.90 -        val _ = Output.debug (fn () => "  isa th: " ^ Display.string_of_thm ctxt i_th)
    1.91 +        val _ = trace_msg (fn () => "  isa th: " ^ Display.string_of_thm ctxt i_th)
    1.92          val substs = map_filter remove_typeinst (Metis.Subst.toList fsubst)
    1.93          val (vars,rawtms) = ListPair.unzip (map_filter subst_translation substs)
    1.94          val tms = infer_types ctxt rawtms;
    1.95          val ctm_of = cterm_incr_types thy (1 + Thm.maxidx_of i_th)
    1.96          val substs' = ListPair.zip (vars, map ctm_of tms)
    1.97 -        val _ = Output.debug (fn () =>
    1.98 +        val _ = trace_msg (fn () =>
    1.99            cat_lines ("subst_translations:" ::
   1.100              (substs' |> map (fn (x, y) =>
   1.101                Syntax.string_of_term ctxt (term_of x) ^ " |-> " ^
   1.102 @@ -416,23 +420,23 @@
   1.103      let
   1.104        val thy = ProofContext.theory_of ctxt
   1.105        val i_th1 = lookth thpairs th1 and i_th2 = lookth thpairs th2
   1.106 -      val _ = Output.debug (fn () => "  isa th1 (pos): " ^ Display.string_of_thm ctxt i_th1)
   1.107 -      val _ = Output.debug (fn () => "  isa th2 (neg): " ^ Display.string_of_thm ctxt i_th2)
   1.108 +      val _ = trace_msg (fn () => "  isa th1 (pos): " ^ Display.string_of_thm ctxt i_th1)
   1.109 +      val _ = trace_msg (fn () => "  isa th2 (neg): " ^ Display.string_of_thm ctxt i_th2)
   1.110      in
   1.111        if is_TrueI i_th1 then i_th2 (*Trivial cases where one operand is type info*)
   1.112        else if is_TrueI i_th2 then i_th1
   1.113        else
   1.114          let
   1.115            val i_atm = singleton (fol_terms_to_hol ctxt mode) (Metis.Term.Fn atm)
   1.116 -          val _ = Output.debug (fn () => "  atom: " ^ Syntax.string_of_term ctxt i_atm)
   1.117 +          val _ = trace_msg (fn () => "  atom: " ^ Syntax.string_of_term ctxt i_atm)
   1.118            val prems_th1 = prems_of i_th1
   1.119            val prems_th2 = prems_of i_th2
   1.120            val index_th1 = get_index (mk_not i_atm) prems_th1
   1.121                  handle Empty => error "Failed to find literal in th1"
   1.122 -          val _ = Output.debug (fn () => "  index_th1: " ^ Int.toString index_th1)
   1.123 +          val _ = trace_msg (fn () => "  index_th1: " ^ Int.toString index_th1)
   1.124            val index_th2 = get_index i_atm prems_th2
   1.125                  handle Empty => error "Failed to find literal in th2"
   1.126 -          val _ = Output.debug (fn () => "  index_th2: " ^ Int.toString index_th2)
   1.127 +          val _ = trace_msg (fn () => "  index_th2: " ^ Int.toString index_th2)
   1.128        in  resolve_inc_tyvars (Meson.select_literal index_th1 i_th1, index_th2, i_th2)  end
   1.129      end;
   1.130  
   1.131 @@ -443,7 +447,7 @@
   1.132    fun refl_inf ctxt mode t =
   1.133      let val thy = ProofContext.theory_of ctxt
   1.134          val i_t = singleton (fol_terms_to_hol ctxt mode) t
   1.135 -        val _ = Output.debug (fn () => "  term: " ^ Syntax.string_of_term ctxt i_t)
   1.136 +        val _ = trace_msg (fn () => "  term: " ^ Syntax.string_of_term ctxt i_t)
   1.137          val c_t = cterm_incr_types thy refl_idx i_t
   1.138      in  cterm_instantiate [(refl_x, c_t)] REFL_THM  end;
   1.139  
   1.140 @@ -456,7 +460,7 @@
   1.141      let val thy = ProofContext.theory_of ctxt
   1.142          val m_tm = Metis.Term.Fn atm
   1.143          val [i_atm,i_tm] = fol_terms_to_hol ctxt mode [m_tm, fr]
   1.144 -        val _ = Output.debug (fn () => "sign of the literal: " ^ Bool.toString pos)
   1.145 +        val _ = trace_msg (fn () => "sign of the literal: " ^ Bool.toString pos)
   1.146          fun replace_item_list lx 0 (l::ls) = lx::ls
   1.147            | replace_item_list lx i (l::ls) = l :: replace_item_list lx (i-1) ls
   1.148          fun path_finder_FO tm [] = (tm, Term.Bound 0)
   1.149 @@ -467,7 +471,7 @@
   1.150                    val tm_p = List.nth(args,p')
   1.151                      handle Subscript => error ("equality_inf: " ^ Int.toString p ^ " adj " ^
   1.152                        Int.toString adjustment  ^ " term " ^  Syntax.string_of_term ctxt tm)
   1.153 -                  val _ = Output.debug (fn () => "path_finder: " ^ Int.toString p ^
   1.154 +                  val _ = trace_msg (fn () => "path_finder: " ^ Int.toString p ^
   1.155                                          "  " ^ Syntax.string_of_term ctxt tm_p)
   1.156  		  val (r,t) = path_finder_FO tm_p ps
   1.157                in
   1.158 @@ -512,12 +516,12 @@
   1.159            | path_finder_lit tm_a idx = path_finder mode tm_a idx m_tm
   1.160          val (tm_subst, body) = path_finder_lit i_atm fp
   1.161          val tm_abs = Term.Abs("x", Term.type_of tm_subst, body)
   1.162 -        val _ = Output.debug (fn () => "abstraction: " ^ Syntax.string_of_term ctxt tm_abs)
   1.163 -        val _ = Output.debug (fn () => "i_tm: " ^ Syntax.string_of_term ctxt i_tm)
   1.164 -        val _ = Output.debug (fn () => "located term: " ^ Syntax.string_of_term ctxt tm_subst)
   1.165 +        val _ = trace_msg (fn () => "abstraction: " ^ Syntax.string_of_term ctxt tm_abs)
   1.166 +        val _ = trace_msg (fn () => "i_tm: " ^ Syntax.string_of_term ctxt i_tm)
   1.167 +        val _ = trace_msg (fn () => "located term: " ^ Syntax.string_of_term ctxt tm_subst)
   1.168          val imax = maxidx_of_term (i_tm $ tm_abs $ tm_subst)  (*ill typed but gives right max*)
   1.169          val subst' = incr_indexes (imax+1) (if pos then subst_em else ssubst_em)
   1.170 -        val _ = Output.debug (fn () => "subst' " ^ Display.string_of_thm ctxt subst')
   1.171 +        val _ = trace_msg (fn () => "subst' " ^ Display.string_of_thm ctxt subst')
   1.172          val eq_terms = map (pairself (cterm_of thy))
   1.173                             (ListPair.zip (OldTerm.term_vars (prop_of subst'), [tm_abs, tm_subst, i_tm]))
   1.174      in  cterm_instantiate eq_terms subst'  end;
   1.175 @@ -541,12 +545,12 @@
   1.176  
   1.177    fun translate mode _    thpairs [] = thpairs
   1.178      | translate mode ctxt thpairs ((fol_th, inf) :: infpairs) =
   1.179 -        let val _ = Output.debug (fn () => "=============================================")
   1.180 -            val _ = Output.debug (fn () => "METIS THM: " ^ Metis.Thm.toString fol_th)
   1.181 -            val _ = Output.debug (fn () => "INFERENCE: " ^ Metis.Proof.inferenceToString inf)
   1.182 +        let val _ = trace_msg (fn () => "=============================================")
   1.183 +            val _ = trace_msg (fn () => "METIS THM: " ^ Metis.Thm.toString fol_th)
   1.184 +            val _ = trace_msg (fn () => "INFERENCE: " ^ Metis.Proof.inferenceToString inf)
   1.185              val th = Meson.flexflex_first_order (step ctxt mode thpairs (fol_th, inf))
   1.186 -            val _ = Output.debug (fn () => "ISABELLE THM: " ^ Display.string_of_thm ctxt th)
   1.187 -            val _ = Output.debug (fn () => "=============================================")
   1.188 +            val _ = trace_msg (fn () => "ISABELLE THM: " ^ Display.string_of_thm ctxt th)
   1.189 +            val _ = trace_msg (fn () => "=============================================")
   1.190              val n_metis_lits = length (filter real_literal (Metis.LiteralSet.toList (Metis.Thm.clause fol_th)))
   1.191          in
   1.192              if nprems_of th = n_metis_lits then ()
   1.193 @@ -665,52 +669,52 @@
   1.194      let val thy = ProofContext.theory_of ctxt
   1.195          val th_cls_pairs = map (fn th => (Thm.get_name_hint th, ResAxioms.cnf_axiom thy th)) ths0
   1.196          val ths = maps #2 th_cls_pairs
   1.197 -        val _ = Output.debug (fn () => "FOL_SOLVE: CONJECTURE CLAUSES")
   1.198 -        val _ = app (fn th => Output.debug (fn () => Display.string_of_thm ctxt th)) cls
   1.199 -        val _ = Output.debug (fn () => "THEOREM CLAUSES")
   1.200 -        val _ = app (fn th => Output.debug (fn () => Display.string_of_thm ctxt th)) ths
   1.201 +        val _ = trace_msg (fn () => "FOL_SOLVE: CONJECTURE CLAUSES")
   1.202 +        val _ = app (fn th => trace_msg (fn () => Display.string_of_thm ctxt th)) cls
   1.203 +        val _ = trace_msg (fn () => "THEOREM CLAUSES")
   1.204 +        val _ = app (fn th => trace_msg (fn () => Display.string_of_thm ctxt th)) ths
   1.205          val (mode, {axioms,tfrees}) = build_map mode ctxt cls ths
   1.206          val _ = if null tfrees then ()
   1.207 -                else (Output.debug (fn () => "TFREE CLAUSES");
   1.208 -                      app (fn tf => Output.debug (fn _ => ResClause.tptp_of_typeLit true tf)) tfrees)
   1.209 -        val _ = Output.debug (fn () => "CLAUSES GIVEN TO METIS")
   1.210 +                else (trace_msg (fn () => "TFREE CLAUSES");
   1.211 +                      app (fn tf => trace_msg (fn _ => ResClause.tptp_of_typeLit true tf)) tfrees)
   1.212 +        val _ = trace_msg (fn () => "CLAUSES GIVEN TO METIS")
   1.213          val thms = map #1 axioms
   1.214 -        val _ = app (fn th => Output.debug (fn () => Metis.Thm.toString th)) thms
   1.215 -        val _ = Output.debug (fn () => "mode = " ^ string_of_mode mode)
   1.216 -        val _ = Output.debug (fn () => "START METIS PROVE PROCESS")
   1.217 +        val _ = app (fn th => trace_msg (fn () => Metis.Thm.toString th)) thms
   1.218 +        val _ = trace_msg (fn () => "mode = " ^ string_of_mode mode)
   1.219 +        val _ = trace_msg (fn () => "START METIS PROVE PROCESS")
   1.220      in
   1.221          case List.filter (is_false o prop_of) cls of
   1.222              false_th::_ => [false_th RS @{thm FalseE}]
   1.223            | [] =>
   1.224          case refute thms of
   1.225              Metis.Resolution.Contradiction mth =>
   1.226 -              let val _ = Output.debug (fn () => "METIS RECONSTRUCTION START: " ^
   1.227 +              let val _ = trace_msg (fn () => "METIS RECONSTRUCTION START: " ^
   1.228                              Metis.Thm.toString mth)
   1.229                    val ctxt' = fold Variable.declare_constraints (map prop_of cls) ctxt
   1.230                                 (*add constraints arising from converting goal to clause form*)
   1.231                    val proof = Metis.Proof.proof mth
   1.232                    val result = translate mode ctxt' axioms proof
   1.233                    and used = map_filter (used_axioms axioms) proof
   1.234 -                  val _ = Output.debug (fn () => "METIS COMPLETED...clauses actually used:")
   1.235 -	          val _ = app (fn th => Output.debug (fn () => Display.string_of_thm ctxt th)) used
   1.236 +                  val _ = trace_msg (fn () => "METIS COMPLETED...clauses actually used:")
   1.237 +	          val _ = app (fn th => trace_msg (fn () => Display.string_of_thm ctxt th)) used
   1.238  	          val unused = filter (fn (a,cls) => not (common_thm used cls)) th_cls_pairs
   1.239                in
   1.240                    if null unused then ()
   1.241                    else warning ("Metis: unused theorems " ^ commas_quote (map #1 unused));
   1.242                    case result of
   1.243                        (_,ith)::_ => 
   1.244 -                          (Output.debug (fn () => "success: " ^ Display.string_of_thm ctxt ith); 
   1.245 +                          (trace_msg (fn () => "success: " ^ Display.string_of_thm ctxt ith); 
   1.246                             [ith])
   1.247 -                    | _ => (Output.debug (fn () => "Metis: no result"); 
   1.248 +                    | _ => (trace_msg (fn () => "Metis: no result"); 
   1.249                              [])
   1.250                end
   1.251            | Metis.Resolution.Satisfiable _ => 
   1.252 -	      (Output.debug (fn () => "Metis: No first-order proof with the lemmas supplied"); 
   1.253 +	      (trace_msg (fn () => "Metis: No first-order proof with the lemmas supplied"); 
   1.254  	       [])
   1.255      end;
   1.256  
   1.257    fun metis_general_tac mode ctxt ths i st0 =
   1.258 -    let val _ = Output.debug (fn () =>
   1.259 +    let val _ = trace_msg (fn () =>
   1.260            "Metis called with theorems " ^ cat_lines (map (Display.string_of_thm ctxt) ths))
   1.261      in
   1.262         if exists_type ResAxioms.type_has_empty_sort (prop_of st0)