src/HOL/Tools/Sledgehammer/metis_translate.ML
changeset 39886 8a9f0c97d550
parent 39720 0b93a954da4f
child 39887 74939e2afb95
     1.1 --- a/src/HOL/Tools/Sledgehammer/metis_translate.ML	Wed Sep 29 17:59:20 2010 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/metis_translate.ML	Wed Sep 29 22:23:27 2010 +0200
     1.3 @@ -34,7 +34,7 @@
     1.4    type logic_map =
     1.5      {axioms: (Metis_Thm.thm * thm) list,
     1.6       tfrees: type_literal list,
     1.7 -     skolems: (string * term) list}
     1.8 +     old_skolems: (string * term) list}
     1.9  
    1.10    val type_wrapper_name : string
    1.11    val bound_var_prefix : string
    1.12 @@ -45,6 +45,7 @@
    1.13    val const_prefix: string
    1.14    val type_const_prefix: string
    1.15    val class_prefix: string
    1.16 +  val new_skolem_prefix : string
    1.17    val invert_const: string -> string
    1.18    val ascii_of: string -> string
    1.19    val unascii_of: string -> string
    1.20 @@ -58,6 +59,7 @@
    1.21    val make_fixed_type_const : string -> string
    1.22    val make_type_class : string -> string
    1.23    val num_type_args: theory -> string -> int
    1.24 +  val new_skolem_var_from_const: string -> indexname
    1.25    val type_literals_for_types : typ list -> type_literal list
    1.26    val make_class_rel_clauses :
    1.27      theory -> class list -> class list -> class_rel_clause list
    1.28 @@ -66,14 +68,15 @@
    1.29    val combtyp_of : combterm -> combtyp
    1.30    val strip_combterm_comb : combterm -> combterm * combterm list
    1.31    val combterm_from_term :
    1.32 -    theory -> (string * typ) list -> term -> combterm * typ list
    1.33 -  val reveal_skolem_terms : (string * term) list -> term -> term
    1.34 +    theory -> int -> (string * typ) list -> term -> combterm * typ list
    1.35 +  val reveal_old_skolem_terms : (string * term) list -> term -> term
    1.36    val tfree_classes_of_terms : term list -> string list
    1.37    val tvar_classes_of_terms : term list -> string list
    1.38    val type_consts_of_terms : theory -> term list -> string list
    1.39    val string_of_mode : mode -> string
    1.40    val build_logic_map :
    1.41 -    mode -> Proof.context -> bool -> thm list -> thm list -> mode * logic_map
    1.42 +    mode -> Proof.context -> bool -> thm list -> thm list list
    1.43 +    -> mode * logic_map
    1.44  end
    1.45  
    1.46  structure Metis_Translate : METIS_TRANSLATE =
    1.47 @@ -92,6 +95,12 @@
    1.48  val type_const_prefix = "tc_";
    1.49  val class_prefix = "class_";
    1.50  
    1.51 +val new_skolem_var_prefix = "SK?" (* purposedly won't parse *)
    1.52 +
    1.53 +val skolem_prefix = "Sledgehammer" ^ Long_Name.separator ^ "Sko"
    1.54 +val old_skolem_prefix = skolem_prefix ^ "o"
    1.55 +val new_skolem_prefix = skolem_prefix ^ "n"
    1.56 +
    1.57  fun union_all xss = fold (union (op =)) xss []
    1.58  
    1.59  (* Readable names for the more common symbolic functions. Do not mess with the
    1.60 @@ -198,8 +207,6 @@
    1.61  
    1.62  fun make_type_class clas = class_prefix ^ ascii_of clas;
    1.63  
    1.64 -val skolem_prefix = "Sledgehammer" ^ Long_Name.separator ^ "Sko"
    1.65 -
    1.66  (* The number of type arguments of a constant, zero if it's monomorphic. For
    1.67     (instances of) Skolem pseudoconstants, this information is encoded in the
    1.68     constant name. *)
    1.69 @@ -209,6 +216,13 @@
    1.70    else
    1.71      (s, Sign.the_const_type thy s) |> Sign.const_typargs thy |> length
    1.72  
    1.73 +fun new_skolem_var_from_const s =
    1.74 +  let
    1.75 +    val ss = s |> space_explode Long_Name.separator
    1.76 +    val n = length ss
    1.77 +  in (nth ss (n - 2), nth ss (n - 3) |> Int.fromString |> the) end
    1.78 +
    1.79 +
    1.80  (**** Definitions and functions for FOL clauses for TPTP format output ****)
    1.81  
    1.82  type name = string * string
    1.83 @@ -384,92 +398,107 @@
    1.84    | simple_combtype_of (TVar (x, _)) =
    1.85      CombTVar (make_schematic_type_var x, string_of_indexname x)
    1.86  
    1.87 +fun new_skolem_name th_no s num_T_args =
    1.88 +  [new_skolem_prefix, string_of_int th_no, s, string_of_int num_T_args]
    1.89 +  |> space_implode Long_Name.separator
    1.90 +
    1.91  (* Converts a term (with combinators) into a combterm. Also accummulates sort
    1.92     infomation. *)
    1.93 -fun combterm_from_term thy bs (P $ Q) =
    1.94 -      let val (P', tsP) = combterm_from_term thy bs P
    1.95 -          val (Q', tsQ) = combterm_from_term thy bs Q
    1.96 +fun combterm_from_term thy th_no bs (P $ Q) =
    1.97 +      let val (P', tsP) = combterm_from_term thy th_no bs P
    1.98 +          val (Q', tsQ) = combterm_from_term thy th_no bs Q
    1.99        in  (CombApp (P', Q'), union (op =) tsP tsQ)  end
   1.100 -  | combterm_from_term thy _ (Const (c, T)) =
   1.101 +  | combterm_from_term thy _ _ (Const (c, T)) =
   1.102        let
   1.103          val (tp, ts) = combtype_of T
   1.104          val tvar_list =
   1.105 -          (if String.isPrefix skolem_prefix c then
   1.106 +          (if String.isPrefix old_skolem_prefix c then
   1.107               [] |> Term.add_tvarsT T |> map TVar
   1.108             else
   1.109               (c, T) |> Sign.const_typargs thy)
   1.110            |> map simple_combtype_of
   1.111          val c' = CombConst (`make_fixed_const c, tp, tvar_list)
   1.112        in  (c',ts)  end
   1.113 -  | combterm_from_term _ _ (Free (v, T)) =
   1.114 +  | combterm_from_term _ _ _ (Free (v, T)) =
   1.115        let val (tp, ts) = combtype_of T
   1.116            val v' = CombConst (`make_fixed_var v, tp, [])
   1.117        in  (v',ts)  end
   1.118 -  | combterm_from_term _ _ (Var (v, T)) =
   1.119 -      let val (tp,ts) = combtype_of T
   1.120 -          val v' = CombVar ((make_schematic_var v, string_of_indexname v), tp)
   1.121 -      in  (v',ts)  end
   1.122 -  | combterm_from_term _ bs (Bound j) =
   1.123 +  | combterm_from_term _ th_no _ (Var (v as (s, _), T)) =
   1.124 +    let
   1.125 +      val (tp, ts) = combtype_of T
   1.126 +      val v' =
   1.127 +        if String.isPrefix new_skolem_var_prefix s then
   1.128 +          let
   1.129 +            val tys = T |> strip_type |> swap |> op ::
   1.130 +            val s' = new_skolem_name th_no s (length tys)
   1.131 +          in
   1.132 +            CombConst (`make_fixed_const s', tp, map simple_combtype_of tys)
   1.133 +          end
   1.134 +        else
   1.135 +          CombVar ((make_schematic_var v, string_of_indexname v), tp)
   1.136 +    in (v', ts) end
   1.137 +  | combterm_from_term _ _ bs (Bound j) =
   1.138        let
   1.139          val (s, T) = nth bs j
   1.140          val (tp, ts) = combtype_of T
   1.141          val v' = CombConst (`make_bound_var s, tp, [])
   1.142        in (v', ts) end
   1.143 -  | combterm_from_term _ _ (Abs _) = raise Fail "HOL clause: Abs"
   1.144 +  | combterm_from_term _ _ _ (Abs _) = raise Fail "HOL clause: Abs"
   1.145  
   1.146 -fun predicate_of thy ((@{const Not} $ P), pos) = predicate_of thy (P, not pos)
   1.147 -  | predicate_of thy (t, pos) =
   1.148 -    (combterm_from_term thy [] (Envir.eta_contract t), pos)
   1.149 +fun predicate_of thy th_no ((@{const Not} $ P), pos) =
   1.150 +    predicate_of thy th_no (P, not pos)
   1.151 +  | predicate_of thy th_no (t, pos) =
   1.152 +    (combterm_from_term thy th_no [] (Envir.eta_contract t), pos)
   1.153  
   1.154 -fun literals_of_term1 args thy (@{const Trueprop} $ P) =
   1.155 -    literals_of_term1 args thy P
   1.156 -  | literals_of_term1 args thy (@{const HOL.disj} $ P $ Q) =
   1.157 -    literals_of_term1 (literals_of_term1 args thy P) thy Q
   1.158 -  | literals_of_term1 (lits, ts) thy P =
   1.159 -    let val ((pred, ts'), pol) = predicate_of thy (P, true) in
   1.160 +fun literals_of_term1 args thy th_no (@{const Trueprop} $ P) =
   1.161 +    literals_of_term1 args thy th_no P
   1.162 +  | literals_of_term1 args thy th_no (@{const HOL.disj} $ P $ Q) =
   1.163 +    literals_of_term1 (literals_of_term1 args thy th_no P) thy th_no Q
   1.164 +  | literals_of_term1 (lits, ts) thy th_no P =
   1.165 +    let val ((pred, ts'), pol) = predicate_of thy th_no (P, true) in
   1.166        (FOLLiteral (pol, pred) :: lits, union (op =) ts ts')
   1.167      end
   1.168  val literals_of_term = literals_of_term1 ([], [])
   1.169  
   1.170 -fun skolem_name i j num_T_args =
   1.171 -  skolem_prefix ^ Long_Name.separator ^
   1.172 +fun old_skolem_name i j num_T_args =
   1.173 +  old_skolem_prefix ^ Long_Name.separator ^
   1.174    (space_implode Long_Name.separator (map Int.toString [i, j, num_T_args]))
   1.175  
   1.176 -fun conceal_skolem_terms i skolems t =
   1.177 +fun conceal_old_skolem_terms i old_skolems t =
   1.178    if exists_Const (curry (op =) @{const_name skolem} o fst) t then
   1.179      let
   1.180 -      fun aux skolems
   1.181 +      fun aux old_skolems
   1.182                (t as (Const (@{const_name skolem}, Type (_, [_, T])) $ _)) =
   1.183            let
   1.184 -            val (skolems, s) =
   1.185 +            val (old_skolems, s) =
   1.186                if i = ~1 then
   1.187 -                (skolems, @{const_name undefined})
   1.188 -              else case AList.find (op aconv) skolems t of
   1.189 -                s :: _ => (skolems, s)
   1.190 +                (old_skolems, @{const_name undefined})
   1.191 +              else case AList.find (op aconv) old_skolems t of
   1.192 +                s :: _ => (old_skolems, s)
   1.193                | [] =>
   1.194                  let
   1.195 -                  val s = skolem_name i (length skolems)
   1.196 -                                      (length (Term.add_tvarsT T []))
   1.197 -                in ((s, t) :: skolems, s) end
   1.198 -          in (skolems, Const (s, T)) end
   1.199 -        | aux skolems (t1 $ t2) =
   1.200 +                  val s = old_skolem_name i (length old_skolems)
   1.201 +                                          (length (Term.add_tvarsT T []))
   1.202 +                in ((s, t) :: old_skolems, s) end
   1.203 +          in (old_skolems, Const (s, T)) end
   1.204 +        | aux old_skolems (t1 $ t2) =
   1.205            let
   1.206 -            val (skolems, t1) = aux skolems t1
   1.207 -            val (skolems, t2) = aux skolems t2
   1.208 -          in (skolems, t1 $ t2) end
   1.209 -        | aux skolems (Abs (s, T, t')) =
   1.210 -          let val (skolems, t') = aux skolems t' in
   1.211 -            (skolems, Abs (s, T, t'))
   1.212 +            val (old_skolems, t1) = aux old_skolems t1
   1.213 +            val (old_skolems, t2) = aux old_skolems t2
   1.214 +          in (old_skolems, t1 $ t2) end
   1.215 +        | aux old_skolems (Abs (s, T, t')) =
   1.216 +          let val (old_skolems, t') = aux old_skolems t' in
   1.217 +            (old_skolems, Abs (s, T, t'))
   1.218            end
   1.219 -        | aux skolems t = (skolems, t)
   1.220 -    in aux skolems t end
   1.221 +        | aux old_skolems t = (old_skolems, t)
   1.222 +    in aux old_skolems t end
   1.223    else
   1.224 -    (skolems, t)
   1.225 +    (old_skolems, t)
   1.226  
   1.227 -fun reveal_skolem_terms skolems =
   1.228 +fun reveal_old_skolem_terms old_skolems =
   1.229    map_aterms (fn t as Const (s, _) =>
   1.230 -                 if String.isPrefix skolem_prefix s then
   1.231 -                   AList.lookup (op =) skolems s |> the
   1.232 +                 if String.isPrefix old_skolem_prefix s then
   1.233 +                   AList.lookup (op =) old_skolems s |> the
   1.234                     |> map_types Type_Infer.paramify_vars
   1.235                   else
   1.236                     t
   1.237 @@ -580,8 +609,8 @@
   1.238              metis_lit pos "=" (map hol_term_to_fol_FT tms)
   1.239          | _ => metis_lit pos "{}" [hol_term_to_fol_FT tm])   (*hBOOL*);
   1.240  
   1.241 -fun literals_of_hol_term thy mode t =
   1.242 -      let val (lits, types_sorts) = literals_of_term thy t
   1.243 +fun literals_of_hol_term thy th_no mode t =
   1.244 +      let val (lits, types_sorts) = literals_of_term thy th_no t
   1.245        in  (map (hol_literal_to_fol mode) lits, types_sorts) end;
   1.246  
   1.247  (*Sign should be "true" for conjecture type constraints, "false" for type lits in clauses.*)
   1.248 @@ -596,16 +625,16 @@
   1.249  fun metis_of_tfree tf =
   1.250    Metis_Thm.axiom (Metis_LiteralSet.singleton (metis_of_type_literals true tf));
   1.251  
   1.252 -fun hol_thm_to_fol is_conjecture ctxt type_lits mode j skolems th =
   1.253 +fun hol_thm_to_fol is_conjecture th_no ctxt type_lits mode j old_skolems th =
   1.254    let
   1.255      val thy = ProofContext.theory_of ctxt
   1.256 -    val (skolems, (mlits, types_sorts)) =
   1.257 -     th |> prop_of |> conceal_skolem_terms j skolems
   1.258 -        ||> (HOLogic.dest_Trueprop #> literals_of_hol_term thy mode)
   1.259 +    val (old_skolems, (mlits, types_sorts)) =
   1.260 +     th |> prop_of |> conceal_old_skolem_terms j old_skolems
   1.261 +        ||> (HOLogic.dest_Trueprop #> literals_of_hol_term thy th_no mode)
   1.262    in
   1.263      if is_conjecture then
   1.264        (Metis_Thm.axiom (Metis_LiteralSet.fromList mlits),
   1.265 -       type_literals_for_types types_sorts, skolems)
   1.266 +       type_literals_for_types types_sorts, old_skolems)
   1.267      else
   1.268        let
   1.269          val tylits = filter_out (default_sort ctxt) types_sorts
   1.270 @@ -614,7 +643,7 @@
   1.271            if type_lits then map (metis_of_type_literals false) tylits else []
   1.272        in
   1.273          (Metis_Thm.axiom (Metis_LiteralSet.fromList(mtylits @ mlits)), [],
   1.274 -         skolems)
   1.275 +         old_skolems)
   1.276        end
   1.277    end;
   1.278  
   1.279 @@ -637,10 +666,10 @@
   1.280  type logic_map =
   1.281    {axioms: (Metis_Thm.thm * thm) list,
   1.282     tfrees: type_literal list,
   1.283 -   skolems: (string * term) list}
   1.284 +   old_skolems: (string * term) list}
   1.285  
   1.286  fun is_quasi_fol_clause thy =
   1.287 -  Meson.is_fol_term thy o snd o conceal_skolem_terms ~1 [] o prop_of
   1.288 +  Meson.is_fol_term thy o snd o conceal_old_skolem_terms ~1 [] o prop_of
   1.289  
   1.290  (*Extract TFree constraints from context to include as conjecture clauses*)
   1.291  fun init_tfrees ctxt =
   1.292 @@ -650,16 +679,16 @@
   1.293    end;
   1.294  
   1.295  (*Insert non-logical axioms corresponding to all accumulated TFrees*)
   1.296 -fun add_tfrees {axioms, tfrees, skolems} : logic_map =
   1.297 +fun add_tfrees {axioms, tfrees, old_skolems} : logic_map =
   1.298       {axioms = map (rpair TrueI o metis_of_tfree) (distinct (op =) tfrees) @
   1.299                 axioms,
   1.300 -      tfrees = tfrees, skolems = skolems}
   1.301 +      tfrees = tfrees, old_skolems = old_skolems}
   1.302  
   1.303  (*transform isabelle type / arity clause to metis clause *)
   1.304  fun add_type_thm [] lmap = lmap
   1.305 -  | add_type_thm ((ith, mth) :: cls) {axioms, tfrees, skolems} =
   1.306 +  | add_type_thm ((ith, mth) :: cls) {axioms, tfrees, old_skolems} =
   1.307        add_type_thm cls {axioms = (mth, ith) :: axioms, tfrees = tfrees,
   1.308 -                        skolems = skolems}
   1.309 +                        old_skolems = old_skolems}
   1.310  
   1.311  fun const_in_metis c (pred, tm_list) =
   1.312    let
   1.313 @@ -694,29 +723,31 @@
   1.314    end;
   1.315  
   1.316  (* Function to generate metis clauses, including comb and type clauses *)
   1.317 -fun build_logic_map mode0 ctxt type_lits cls ths =
   1.318 +fun build_logic_map mode0 ctxt type_lits cls thss =
   1.319    let val thy = ProofContext.theory_of ctxt
   1.320        (*The modes FO and FT are sticky. HO can be downgraded to FO.*)
   1.321        fun set_mode FO = FO
   1.322          | set_mode HO =
   1.323 -          if forall (is_quasi_fol_clause thy) (cls @ ths) then FO else HO
   1.324 +          if forall (forall (is_quasi_fol_clause thy)) (cls :: thss) then FO
   1.325 +          else HO
   1.326          | set_mode FT = FT
   1.327        val mode = set_mode mode0
   1.328        (*transform isabelle clause to metis clause *)
   1.329 -      fun add_thm is_conjecture (metis_ith, isa_ith) {axioms, tfrees, skolems}
   1.330 -                  : logic_map =
   1.331 +      fun add_thm th_no is_conjecture (metis_ith, isa_ith)
   1.332 +                  {axioms, tfrees, old_skolems} : logic_map =
   1.333          let
   1.334 -          val (mth, tfree_lits, skolems) =
   1.335 -            hol_thm_to_fol is_conjecture ctxt type_lits mode (length axioms)
   1.336 -                           skolems metis_ith
   1.337 +          val (mth, tfree_lits, old_skolems) =
   1.338 +            hol_thm_to_fol is_conjecture th_no ctxt type_lits mode (length axioms)
   1.339 +                           old_skolems metis_ith
   1.340          in
   1.341             {axioms = (mth, Meson.make_meta_clause isa_ith) :: axioms,
   1.342 -            tfrees = union (op =) tfree_lits tfrees, skolems = skolems}
   1.343 +            tfrees = union (op =) tfree_lits tfrees, old_skolems = old_skolems}
   1.344          end;
   1.345 -      val lmap = {axioms = [], tfrees = init_tfrees ctxt, skolems = []}
   1.346 -                 |> fold (add_thm true o `I) cls
   1.347 +      val lmap = {axioms = [], tfrees = init_tfrees ctxt, old_skolems = []}
   1.348 +                 |> fold (add_thm 0 true o `I) cls
   1.349                   |> add_tfrees
   1.350 -                 |> fold (add_thm false o `I) ths
   1.351 +                 |> fold (fn (th_no, ths) => fold (add_thm th_no false o `I) ths)
   1.352 +                         (1 upto length thss ~~ thss)
   1.353        val clause_lists = map (Metis_Thm.clause o #1) (#axioms lmap)
   1.354        fun is_used c =
   1.355          exists (Metis_LiteralSet.exists (const_in_metis c o #2)) clause_lists
   1.356 @@ -733,7 +764,9 @@
   1.357                                      []
   1.358                                    else
   1.359                                      thms)
   1.360 -          in lmap |> fold (add_thm false) helper_ths end
   1.361 -  in (mode, add_type_thm (type_ext thy (map prop_of (cls @ ths))) lmap) end
   1.362 +          in lmap |> fold (add_thm ~1 false) helper_ths end
   1.363 +  in
   1.364 +    (mode, add_type_thm (type_ext thy (maps (map prop_of) (cls :: thss))) lmap)
   1.365 +  end
   1.366  
   1.367  end;