src/HOL/TPTP/TPTP_Parser/tptp_interpret.ML
author sultana
Tue Apr 24 13:55:02 2012 +0100 (2012-04-24)
changeset 47729 44d1f4e0a46e
parent 47692 3d76c81b5ed2
child 48829 6ed588c4f963
permissions -rw-r--r--
tuned;
     1 (*  Title:      HOL/TPTP/TPTP_Parser/tptp_interpret.ML
     2     Author:     Nik Sultana, Cambridge University Computer Laboratory
     3 
     4 Interprets TPTP problems in Isabelle/HOL.
     5 *)
     6 
     7 signature TPTP_INTERPRET =
     8 sig
     9   (*Signature extension: typing information for variables and constants*)
    10   type var_types = (string * typ option) list
    11   type const_map = (string * term) list
    12 
    13   (*Mapping from TPTP types to Isabelle/HOL types. This map works over all
    14   base types. The map must be total wrt TPTP types.*)
    15   type type_map = (TPTP_Syntax.tptp_type * typ) list
    16 
    17   (*Inference info, when available, consists of the name of the inference rule
    18   and the names of the inferences involved in the reasoning step.*)
    19   type inference_info = (string * string list) option
    20 
    21   (*A parsed annotated formula is represented as a 5-tuple consisting of
    22   the formula's label, its role, the TPTP formula, its Isabelle/HOL meaning, and
    23   inference info*)
    24   type tptp_formula_meaning =
    25     string * TPTP_Syntax.role * term * inference_info
    26 
    27   (*In general, the meaning of a TPTP statement (which, through the Include
    28   directive, may include the meaning of an entire TPTP file, is a map from
    29   TPTP to Isabelle/HOL types, a map from TPTP constants to their Isabelle/HOL
    30   counterparts and their types, and a list of interpreted annotated formulas.*)
    31   type tptp_general_meaning =
    32     (type_map * const_map * tptp_formula_meaning list)
    33 
    34   (*cautious = indicates whether additional checks are made to check
    35       that all used types have been declared.
    36     problem_name = if given then it is used to qualify types & constants*)
    37   type config =
    38     {cautious : bool,
    39      problem_name : TPTP_Problem_Name.problem_name option}
    40 
    41   (*Generates a fresh Isabelle/HOL type for interpreting a TPTP type in a theory.*)
    42   val declare_type : config -> (TPTP_Syntax.tptp_type * string) -> type_map ->
    43     theory -> type_map * theory
    44 
    45   (*Map TPTP types to Isabelle/HOL types*)
    46   val interpret_type : config -> theory -> type_map ->
    47     TPTP_Syntax.tptp_type -> typ
    48 
    49   (*Map TPTP terms to Isabelle/HOL terms*)
    50   val interpret_term : bool -> config -> TPTP_Syntax.language ->
    51     const_map -> var_types -> type_map -> TPTP_Syntax.tptp_term -> theory ->
    52     term * theory
    53 
    54   val interpret_formula : config -> TPTP_Syntax.language -> const_map ->
    55     var_types -> type_map -> TPTP_Syntax.tptp_formula -> theory ->
    56     term * theory
    57 
    58   (*Interpret a TPTP line: return a "tptp_general_meaning" for that line,
    59   as well as an updated Isabelle theory including any types & constants
    60   which were specified in that line.
    61   Note that type/constant declarations do not result in any formulas being
    62   returned. A typical TPTP line might update the theory, and/or return one or
    63   more formulas. For instance, the "include" directive may update the theory
    64   and also return a list of formulas from the included file.
    65   Arguments:
    66     config = (see above)
    67     inclusion list = names of annotated formulas to interpret (since "include"
    68       directive can be selective wrt to such names)
    69     type_map = mapping of TPTP-types to Isabelle/HOL types. This argument may be
    70       given to force a specific mapping: this is usually done for using an
    71       imported TPTP problem in Isar.
    72     const_map = as previous, but for constants.
    73     path_prefix = path where TPTP problems etc are located (to help the "include"
    74       directive find the files.
    75     line = parsed TPTP line
    76     thy = theory where interpreted info will be stored.
    77   *)
    78   val interpret_line : config -> string list -> type_map -> const_map ->
    79     Path.T -> TPTP_Syntax.tptp_line -> theory -> tptp_general_meaning * theory
    80 
    81   (*Like "interpret_line" above, but works over a whole parsed problem.
    82     Arguments:
    83       config = as previously
    84       inclusion list = as previously
    85       path_prefix = as previously
    86       lines = parsed TPTP syntax
    87       type_map = as previously
    88       const_map = as previously
    89       thy = as previously
    90   *)
    91   val interpret_problem : config -> string list -> Path.T ->
    92     TPTP_Syntax.tptp_line list -> type_map -> const_map -> theory ->
    93     tptp_general_meaning * theory
    94 
    95   (*Like "interpret_problem" above, but it is given a filename rather than
    96   a parsed problem.*)
    97   val interpret_file : bool -> Path.T -> Path.T -> type_map -> const_map ->
    98     theory -> tptp_general_meaning * theory
    99 
   100   type position = string * int * int
   101   exception MISINTERPRET of position list * exn
   102   exception MISINTERPRET_FORMULA of string * TPTP_Syntax.tptp_formula
   103   exception MISINTERPRET_SYMBOL of string * TPTP_Syntax.symbol
   104   exception MISINTERPRET_TERM of string * TPTP_Syntax.tptp_term
   105   exception MISINTERPRET_TYPE of string * TPTP_Syntax.tptp_type
   106 
   107   val import_file : bool -> Path.T -> Path.T -> type_map -> const_map ->
   108     theory -> theory
   109 
   110   (*Imported TPTP files are stored as "manifests" in the theory.*)
   111   type manifest = TPTP_Problem_Name.problem_name * tptp_general_meaning
   112   val get_manifests : theory -> manifest list
   113 end
   114 
   115 structure TPTP_Interpret : TPTP_INTERPRET =
   116 struct
   117 
   118 open TPTP_Syntax
   119 type position = string * int * int
   120 exception MISINTERPRET of position list * exn
   121 exception MISINTERPRET_FORMULA of string * TPTP_Syntax.tptp_formula
   122 exception MISINTERPRET_SYMBOL of string * TPTP_Syntax.symbol
   123 exception MISINTERPRET_TERM of string * TPTP_Syntax.tptp_term
   124 exception MISINTERPRET_TYPE of string * TPTP_Syntax.tptp_type
   125 
   126 
   127 (* General stuff *)
   128 
   129 type config =
   130   {cautious : bool,
   131    problem_name : TPTP_Problem_Name.problem_name option}
   132 
   133 
   134 (* Interpretation *)
   135 
   136 (** Signatures and other type abbrevations **)
   137 
   138 type const_map = (string * term) list
   139 type var_types = (string * typ option) list
   140 type type_map = (TPTP_Syntax.tptp_type * typ) list
   141 type inference_info = (string * string list) option
   142 type tptp_formula_meaning =
   143   string * TPTP_Syntax.role * term * inference_info
   144 type tptp_general_meaning =
   145   (type_map * const_map * tptp_formula_meaning list)
   146 
   147 type manifest = TPTP_Problem_Name.problem_name * tptp_general_meaning
   148 
   149 structure TPTP_Data = Theory_Data
   150 (
   151   type T = manifest list
   152   val empty = []
   153   val extend = I
   154   fun merge data : T = Library.merge (op =) data
   155 )
   156 val get_manifests = TPTP_Data.get
   157 
   158 
   159 (** Adding types to a signature **)
   160 
   161 (*transform quoted names into acceptable ASCII strings*)
   162 fun alphanumerate c =
   163   let
   164     val c' = ord c
   165     val out_of_range =
   166       ((c' > 64) andalso (c' < 91)) orelse ((c' > 96)
   167        andalso (c' < 123)) orelse ((c' > 47) andalso (c' < 58))
   168   in
   169     if (not out_of_range) andalso (not (c = "_")) then
   170       "_nom_" ^ Int.toString (ord c) ^ "_"
   171     else c
   172   end
   173 fun alphanumerated_name prefix name =
   174   prefix ^ (raw_explode #> map alphanumerate #> implode) name
   175 
   176 (*SMLNJ complains if type annotation not used below*)
   177 fun mk_binding (config : config) ident =
   178   let
   179     val pre_binding = Binding.name (alphanumerated_name "bnd_" ident)
   180   in
   181     case #problem_name config of
   182       NONE => pre_binding
   183     | SOME prob =>
   184         Binding.qualify
   185          false
   186          (TPTP_Problem_Name.mangle_problem_name prob)
   187          pre_binding
   188   end
   189 
   190 fun type_exists config thy ty_name =
   191   Sign.declared_tyname thy (Sign.full_name thy (mk_binding config ty_name))
   192 
   193 (*Returns updated theory and the name of the final type's name -- i.e. if the
   194 original name is already taken then the function looks for an available
   195 alternative. It also returns an updated type_map if one has been passed to it.*)
   196 fun declare_type (config : config) (thf_type, type_name) ty_map thy =
   197   if type_exists config thy type_name then
   198     raise MISINTERPRET_TYPE ("Type already exists", Atom_type type_name)
   199   else
   200     let
   201       val binding = mk_binding config type_name
   202       val final_fqn = Sign.full_name thy binding
   203       val thy' =
   204         Typedecl.typedecl_global (mk_binding config type_name, [], NoSyn) thy
   205         |> snd
   206       val typ_map_entry = (thf_type, (Type (final_fqn, [])))
   207       val ty_map' = typ_map_entry :: ty_map
   208     in (ty_map', thy') end
   209 
   210 
   211 (** Adding constants to signature **)
   212 
   213 fun full_name thy config const_name =
   214   Sign.full_name thy (mk_binding config const_name)
   215 
   216 fun const_exists config thy const_name =
   217   Sign.declared_const thy (full_name thy config const_name)
   218 
   219 fun declare_constant config const_name ty thy =
   220   if const_exists config thy const_name then
   221     raise MISINTERPRET_TERM
   222      ("Const already declared", Term_Func (Uninterpreted const_name, []))
   223   else
   224     Theory.specify_const
   225      ((mk_binding config const_name, ty), NoSyn) thy
   226 
   227 fun declare_const_ifnot config const_name ty thy =
   228   if const_exists config thy const_name then
   229     (Sign.mk_const thy ((Sign.full_name thy (mk_binding config const_name)), []), thy)
   230   else declare_constant config const_name ty thy
   231 
   232 
   233 (** Interpretation functions **)
   234 
   235 (*Types in THF are encoded as formulas. This function translates them to type form.*)
   236 (*FIXME possibly incomplete hack*)
   237 fun fmlatype_to_type (Atom (THF_Atom_term (Term_Func (TypeSymbol typ, [])))) =
   238       Defined_type typ
   239   | fmlatype_to_type (Atom (THF_Atom_term (Term_Func (Uninterpreted str, [])))) =
   240       Atom_type str
   241   | fmlatype_to_type (Type_fmla (Fn_type (ty1, ty2))) =
   242       let
   243         val ty1' = case ty1 of
   244             Fn_type _ => fmlatype_to_type (Type_fmla ty1)
   245           | Fmla_type ty1 => fmlatype_to_type ty1
   246         val ty2' = case ty2 of
   247             Fn_type _ => fmlatype_to_type (Type_fmla ty2)
   248           | Fmla_type ty2 => fmlatype_to_type ty2
   249       in Fn_type (ty1', ty2') end
   250 
   251 fun interpret_type config thy type_map thf_ty =
   252   let
   253     fun lookup_type ty_map thf_ty =
   254       (case AList.lookup (op =) ty_map thf_ty of
   255           NONE =>
   256             raise MISINTERPRET_TYPE
   257               ("Could not find the interpretation of this TPTP type in the \
   258                \mapping to Isabelle/HOL", thf_ty)
   259         | SOME ty => ty)
   260   in
   261     case thf_ty of
   262        Prod_type (thf_ty1, thf_ty2) =>
   263          Type ("Product_Type.prod",
   264           [interpret_type config thy type_map thf_ty1,
   265            interpret_type config thy type_map thf_ty2])
   266      | Fn_type (thf_ty1, thf_ty2) =>
   267          Type ("fun",
   268           [interpret_type config thy type_map thf_ty1,
   269            interpret_type config thy type_map thf_ty2])
   270      | Atom_type _ =>
   271          lookup_type type_map thf_ty
   272      | Defined_type tptp_base_type =>
   273          (case tptp_base_type of
   274             Type_Ind => @{typ ind}
   275           | Type_Bool => HOLogic.boolT
   276           | Type_Type => raise MISINTERPRET_TYPE ("No type interpretation", thf_ty)
   277          (*FIXME these types are currently unsupported, so they're treated as
   278          individuals*)
   279           | Type_Int =>
   280               interpret_type config thy type_map (Defined_type Type_Ind)
   281           | Type_Rat =>
   282               interpret_type config thy type_map (Defined_type Type_Ind)
   283           | Type_Real =>
   284               interpret_type config thy type_map (Defined_type Type_Ind)
   285           )
   286      | Sum_type _ =>
   287          raise MISINTERPRET_TYPE (*FIXME*)
   288           ("No type interpretation (sum type)", thf_ty)
   289      | Fmla_type tptp_ty =>
   290         fmlatype_to_type tptp_ty
   291         |> interpret_type config thy type_map
   292      | Subtype _ =>
   293          raise MISINTERPRET_TYPE (*FIXME*)
   294           ("No type interpretation (subtype)", thf_ty)
   295   end
   296 
   297 fun the_const config thy language const_map_payload str =
   298   if language = THF then
   299     (case AList.lookup (op =) const_map_payload str of
   300         NONE => raise MISINTERPRET_TERM
   301           ("Could not find the interpretation of this constant in the \
   302             \mapping to Isabelle/HOL", Term_Func (Uninterpreted str, []))
   303       | SOME t => t)
   304   else
   305     if const_exists config thy str then
   306        Sign.mk_const thy ((Sign.full_name thy (mk_binding config str)), [])
   307     else raise MISINTERPRET_TERM
   308           ("Could not find the interpretation of this constant in the \
   309             \mapping to Isabelle/HOL", Term_Func (Uninterpreted str, []))
   310 
   311 (*Eta-expands n-ary function.
   312  "str" is the name of an Isabelle/HOL constant*)
   313 fun mk_n_fun n str =
   314   let
   315     fun body 0 t = t
   316       | body n t = body (n - 1) (t  $ (Bound (n - 1)))
   317   in
   318     body n (Const (str, Term.dummyT))
   319     |> funpow n (Term.absdummy Term.dummyT)
   320   end
   321 fun mk_fun_type [] b acc = acc b
   322   | mk_fun_type (ty :: tys) b acc =
   323       mk_fun_type tys b (fn ty_rest => Type ("fun", [ty, acc ty_rest]))
   324 
   325 fun dummy_term () =
   326   HOLogic.choice_const Term.dummyT $ Term.absdummy Term.dummyT @{term "True"}
   327 
   328 (*These arities are not part of the TPTP spec*)
   329 fun arity_of interpreted_symbol = case interpreted_symbol of
   330     UMinus => 1
   331   | Sum => 2
   332   | Difference => 2
   333   | Product => 2
   334   | Quotient => 2
   335   | Quotient_E => 2
   336   | Quotient_T => 2
   337   | Quotient_F => 2
   338   | Remainder_E => 2
   339   | Remainder_T => 2
   340   | Remainder_F => 2
   341   | Floor => 1
   342   | Ceiling => 1
   343   | Truncate => 1
   344   | Round => 1
   345   | To_Int => 1
   346   | To_Rat => 1
   347   | To_Real => 1
   348   | Less => 2
   349   | LessEq => 2
   350   | Greater => 2
   351   | GreaterEq => 2
   352   | EvalEq => 2
   353   | Is_Int => 1
   354   | Is_Rat => 1
   355   | Distinct => 1
   356   | Apply=> 2
   357 
   358 fun interpret_symbol config language const_map symb thy =
   359   case symb of
   360      Uninterpreted n =>
   361        (*Constant would have been added to the map at the time of
   362        declaration*)
   363        the_const config thy language const_map n
   364    | Interpreted_ExtraLogic interpreted_symbol =>
   365        (*FIXME not interpreting*)
   366        Sign.mk_const thy ((Sign.full_name thy (mk_binding config
   367           (string_of_interpreted_symbol interpreted_symbol))), [])
   368    | Interpreted_Logic logic_symbol =>
   369        (case logic_symbol of
   370           Equals => HOLogic.eq_const Term.dummyT
   371         | NEquals =>
   372            HOLogic.mk_not (HOLogic.eq_const Term.dummyT $ Bound 1 $ Bound 0)
   373            |> (Term.absdummy Term.dummyT #> Term.absdummy Term.dummyT)
   374         | Or => HOLogic.disj
   375         | And => HOLogic.conj
   376         | Iff => HOLogic.eq_const HOLogic.boolT
   377         | If => HOLogic.imp
   378         | Fi => @{term "\<lambda> x. \<lambda> y. y \<longrightarrow> x"}
   379         | Xor =>
   380             @{term
   381               "\<lambda> x. \<lambda> y. \<not> (x \<longleftrightarrow> y)"}
   382         | Nor => @{term "\<lambda> x. \<lambda> y. \<not> (x \<or> y)"}
   383         | Nand => @{term "\<lambda> x. \<lambda> y. \<not> (x \<and> y)"}
   384         | Not => HOLogic.Not
   385         | Op_Forall => HOLogic.all_const Term.dummyT
   386         | Op_Exists => HOLogic.exists_const Term.dummyT
   387         | True => @{term "True"}
   388         | False => @{term "False"}
   389         )
   390    | TypeSymbol _ =>
   391        raise MISINTERPRET_SYMBOL
   392         ("Cannot have TypeSymbol in term", symb)
   393    | System str =>
   394        raise MISINTERPRET_SYMBOL
   395         ("Cannot interpret system symbol", symb)
   396 
   397 (*Apply a function to a list of arguments*)
   398 val mapply = fold (fn x => fn y => y $ x)
   399 
   400 fun mapply' (args, thy) f =
   401   let
   402     val (f', thy') = f thy
   403   in (mapply args f', thy') end
   404 
   405 (*As above, but for products*)
   406 fun mtimes thy =
   407   fold (fn x => fn y =>
   408     Sign.mk_const thy
   409     ("Product_Type.Pair", [Term.dummyT, Term.dummyT]) $ y $ x)
   410 
   411 fun mtimes' (args, thy) f =
   412   let
   413     val (f', thy') = f thy
   414   in (mtimes thy' args f', thy') end
   415 
   416 datatype tptp_atom_value =
   417     Atom_App of tptp_term
   418   | Atom_Arity of string * int (*FIXME instead of int could use type list*)
   419 
   420 (*Adds constants to signature when explicit type declaration isn't
   421 expected, e.g. FOL. "formula_level" means that the constants are to be interpreted
   422 as predicates, otherwise as functions over individuals.*)
   423 fun type_atoms_to_thy config formula_level type_map tptp_atom_value thy =
   424   let
   425     val ind_type = interpret_type config thy type_map (Defined_type Type_Ind)
   426     val value_type =
   427       if formula_level then
   428         interpret_type config thy type_map (Defined_type Type_Bool)
   429       else ind_type
   430   in case tptp_atom_value of
   431       Atom_App (Term_Func (symb, tptp_ts)) =>
   432         let
   433           val thy' = fold (fn t =>
   434             type_atoms_to_thy config false type_map (Atom_App t)) tptp_ts thy
   435         in
   436           case symb of
   437              Uninterpreted const_name =>
   438                declare_const_ifnot config const_name
   439                 (mk_fun_type (replicate (length tptp_ts) ind_type) value_type I) thy'
   440                |> snd
   441            | _ => thy'
   442         end
   443     | Atom_App _ => thy
   444     | Atom_Arity (const_name, n_args) =>
   445         declare_const_ifnot config const_name
   446          (mk_fun_type (replicate n_args ind_type) value_type I) thy
   447         |> snd
   448     | _ => thy
   449   end
   450 
   451 (*FIXME only used until interpretation is implemented*)
   452 fun add_interp_symbols_to_thy config type_map thy =
   453   let
   454     val ind_symbols = [UMinus, Sum, Difference, Product, Quotient, Quotient_E,
   455       Quotient_T, Quotient_F, Remainder_E, Remainder_T, Remainder_F, Floor,
   456       Ceiling, Truncate, Round, To_Int, To_Rat, To_Real, Distinct, Apply]
   457     val bool_symbols = [Less, LessEq, Greater, GreaterEq, EvalEq, Is_Int, Is_Rat]
   458     fun add_interp_symbol_to_thy formula_level symbol =
   459       type_atoms_to_thy config formula_level type_map
   460        (Atom_Arity (string_of_interpreted_symbol symbol, arity_of symbol))
   461   in
   462     fold (add_interp_symbol_to_thy false) ind_symbols thy
   463     |> fold (add_interp_symbol_to_thy true) bool_symbols
   464   end
   465 
   466 (*Next batch of functions give info about Isabelle/HOL types*)
   467 fun is_fun (Type ("fun", _)) = true
   468   | is_fun _ = false
   469 fun is_prod (Type ("Product_Type.prod", _)) = true
   470   | is_prod _ = false
   471 fun dom_type (Type ("fun", [ty1, _])) = ty1
   472 fun is_prod_typed thy config symb =
   473   let
   474     fun symb_type const_name =
   475       Sign.the_const_type thy (full_name thy config const_name)
   476   in
   477     case symb of
   478        Uninterpreted const_name =>
   479          if is_fun (symb_type const_name) then
   480            symb_type const_name |> dom_type |> is_prod
   481          else false
   482      | _ => false
   483    end
   484 
   485 (*
   486  Information needed to be carried around:
   487  - constant mapping: maps constant names to Isabelle terms with fully-qualified
   488     names. This is fixed, and it is determined by declaration lines earlier
   489     in the script (i.e. constants must be declared before appearing in terms.
   490  - type context: maps bound variables to their Isabelle type. This is discarded
   491     after each call of interpret_term since variables' cannot be bound across
   492     terms.
   493 *)
   494 fun interpret_term formula_level config language const_map var_types type_map
   495  tptp_t thy =
   496   case tptp_t of
   497     Term_Func (symb, tptp_ts) =>
   498        let
   499          val thy' =
   500            type_atoms_to_thy config formula_level type_map (Atom_App tptp_t) thy
   501          fun typeof_const const_name = Sign.the_const_type thy'
   502              (Sign.full_name thy' (mk_binding config const_name))
   503        in
   504          case symb of
   505            Interpreted_ExtraLogic Apply =>
   506              (*apply the head of the argument list to the tail*)
   507              (mapply'
   508                (fold_map (interpret_term false config language const_map
   509                 var_types type_map) (tl tptp_ts) thy')
   510                (interpret_term formula_level config language const_map
   511                 var_types type_map (hd tptp_ts)))
   512            | _ =>
   513               (*apply symb to tptp_ts*)
   514               if is_prod_typed thy' config symb then
   515                 let
   516                   val (t, thy'') =
   517                     mtimes'
   518                       (fold_map (interpret_term false config language const_map
   519                        var_types type_map) (tl tptp_ts) thy')
   520                       (interpret_term false config language const_map
   521                        var_types type_map (hd tptp_ts))
   522                 in (interpret_symbol config language const_map symb thy' $ t, thy'')
   523                 end
   524               else
   525                 (
   526                 mapply'
   527                   (fold_map (interpret_term false config language const_map
   528                    var_types type_map) tptp_ts thy')
   529                   (`(interpret_symbol config language const_map symb))
   530                 )
   531        end
   532   | Term_Var n =>
   533      (if language = THF orelse language = TFF then
   534         (case AList.lookup (op =) var_types n of
   535            SOME ty =>
   536              (case ty of
   537                 SOME ty => Free (n, ty)
   538               | NONE => Free (n, Term.dummyT) (*to infer the variable's type*)
   539              )
   540          | NONE =>
   541              raise MISINTERPRET_TERM ("Could not type variable", tptp_t))
   542       else (*variables range over individuals*)
   543         Free (n, interpret_type config thy type_map (Defined_type Type_Ind)),
   544       thy)
   545   | Term_Conditional (tptp_formula, tptp_t1, tptp_t2) =>
   546       let
   547         val (t_fmla, thy') =
   548           interpret_formula config language const_map var_types type_map tptp_formula thy
   549         val ([t1, t2], thy'') =
   550           fold_map (interpret_term formula_level config language const_map var_types type_map)
   551            [tptp_t1, tptp_t2] thy'
   552       in (mk_n_fun 3 @{const_name If} $ t_fmla $ t1 $ t2, thy'') end
   553   | Term_Num (number_kind, num) =>
   554       let
   555         (*FIXME hack*)
   556         val ind_type = interpret_type config thy type_map (Defined_type Type_Ind)
   557         val prefix = case number_kind of
   558             Int_num => "intn_"
   559           | Real_num => "realn_"
   560           | Rat_num => "ratn_"
   561       (*FIXME hack -- for Int_num should be
   562        HOLogic.mk_number @{typ "int"} (the (Int.fromString num))*)
   563       in declare_const_ifnot config (prefix ^ num) ind_type thy end
   564   | Term_Distinct_Object str =>
   565       declare_constant config ("do_" ^ str)
   566         (interpret_type config thy type_map (Defined_type Type_Ind)) thy
   567 
   568 and interpret_formula config language const_map var_types type_map tptp_fmla thy =
   569   case tptp_fmla of
   570       Pred app =>
   571         interpret_term true config language const_map
   572          var_types type_map (Term_Func app) thy
   573     | Fmla (symbol, tptp_formulas) =>
   574        (case symbol of
   575           Interpreted_ExtraLogic Apply =>
   576             mapply'
   577               (fold_map (interpret_formula config language const_map
   578                var_types type_map) (tl tptp_formulas) thy)
   579               (interpret_formula config language const_map
   580                var_types type_map (hd tptp_formulas))
   581         | Uninterpreted const_name =>
   582             let
   583               val (args, thy') = (fold_map (interpret_formula config language
   584                const_map var_types type_map) tptp_formulas thy)
   585               val thy' =
   586                 type_atoms_to_thy config true type_map
   587                  (Atom_Arity (const_name, length tptp_formulas)) thy'
   588             in
   589               (if is_prod_typed thy' config symbol then
   590                  mtimes thy' args (interpret_symbol config language
   591                   const_map symbol thy')
   592                else
   593                 mapply args
   594                  (interpret_symbol config language const_map symbol thy'),
   595               thy')
   596             end
   597         | _ =>
   598             let
   599               val (args, thy') =
   600                 fold_map
   601                  (interpret_formula config language
   602                   const_map var_types type_map)
   603                  tptp_formulas thy
   604             in
   605               (if is_prod_typed thy' config symbol then
   606                  mtimes thy' args (interpret_symbol config language
   607                   const_map symbol thy')
   608                else
   609                  mapply args
   610                   (interpret_symbol config language const_map symbol thy'),
   611                thy')
   612             end)
   613     | Sequent _ =>
   614         (*FIXME unsupported*)
   615         raise MISINTERPRET_FORMULA ("'Sequent' unsupported", tptp_fmla)
   616     | Quant (quantifier, bindings, tptp_formula) =>
   617         let
   618           val var_types' =
   619               ListPair.unzip bindings
   620            |> (apsnd ((map o Option.map) (interpret_type config thy type_map)))
   621            |> ListPair.zip
   622            |> List.rev
   623           fun fold_bind f =
   624             fold
   625               (fn (n, ty) => fn t =>
   626                  case ty of
   627                    NONE =>
   628                      f (n,
   629                         if language = THF then Term.dummyT
   630                         else
   631                           interpret_type config thy type_map
   632                            (Defined_type Type_Ind),
   633                         t)
   634                  | SOME ty => f (n, ty, t)
   635               )
   636               var_types'
   637         in case quantifier of
   638           Forall =>
   639             interpret_formula config language const_map (var_types' @ var_types)
   640              type_map tptp_formula thy
   641             |>> fold_bind HOLogic.mk_all
   642         | Exists =>
   643             interpret_formula config language const_map (var_types' @ var_types)
   644              type_map tptp_formula thy
   645             |>> fold_bind HOLogic.mk_exists
   646         | Lambda =>
   647             interpret_formula config language const_map (var_types' @ var_types)
   648              type_map tptp_formula thy
   649             |>> fold_bind (fn (n, ty, rest) => lambda (Free (n, ty)) rest)
   650         | Epsilon =>
   651             let val (t, thy') =
   652               interpret_formula config language const_map var_types type_map
   653                (Quant (Lambda, bindings, tptp_formula)) thy
   654             in ((HOLogic.choice_const Term.dummyT) $ t, thy') end
   655         | Iota =>
   656             let val (t, thy') =
   657               interpret_formula config language const_map var_types type_map
   658                (Quant (Lambda, bindings, tptp_formula)) thy
   659             in (Const (@{const_name The}, Term.dummyT) $ t, thy') end
   660         | Dep_Prod =>
   661             raise MISINTERPRET_FORMULA ("Unsupported", tptp_fmla)
   662         | Dep_Sum =>
   663             raise MISINTERPRET_FORMULA ("Unsupported", tptp_fmla)
   664         end
   665     | Conditional (fmla1, fmla2, fmla3) =>
   666         let
   667           val interp = interpret_formula config language const_map var_types type_map
   668           val (((fmla1', fmla2'), fmla3'), thy') =
   669             interp fmla1 thy
   670             ||>> interp fmla2
   671             ||>> interp fmla3
   672         in (HOLogic.mk_conj (HOLogic.mk_imp (fmla1', fmla2'),
   673                              HOLogic.mk_imp (HOLogic.mk_not fmla1', fmla3')),
   674             thy')
   675         end
   676     | Let (tptp_let_list, tptp_formula) => (*FIXME not yet implemented*)
   677         raise MISINTERPRET_FORMULA ("'Let' not yet implemented", tptp_fmla)
   678     | Atom tptp_atom =>
   679         (case tptp_atom of
   680           TFF_Typed_Atom (symbol, tptp_type_opt) =>
   681             (*FIXME ignoring type info*)
   682             (interpret_symbol config language const_map symbol thy, thy)
   683         | THF_Atom_term tptp_term =>
   684             interpret_term true config language const_map var_types
   685              type_map tptp_term thy
   686         | THF_Atom_conn_term symbol =>
   687             (interpret_symbol config language const_map symbol thy, thy))
   688     | Type_fmla _ =>
   689          raise MISINTERPRET_FORMULA
   690           ("Cannot interpret types as formulas", tptp_fmla)
   691     | THF_typing (tptp_formula, _) => (*FIXME ignoring type info*)
   692         interpret_formula config language
   693          const_map var_types type_map tptp_formula thy
   694 
   695 (*Extract the type from a typing*)
   696 local
   697   fun extract_type tptp_type =
   698     case tptp_type of
   699         Fmla_type typ => fmlatype_to_type typ
   700       | _ => tptp_type
   701 in
   702   fun typeof_typing (THF_typing (_, tptp_type)) = extract_type tptp_type
   703   fun typeof_tff_typing (Atom (TFF_Typed_Atom (_, SOME tptp_type))) =
   704     extract_type tptp_type
   705 end
   706 fun nameof_typing
   707   (THF_typing
   708      ((Atom (THF_Atom_term (Term_Func (Uninterpreted str, [])))), _)) = str
   709 fun nameof_tff_typing (Atom (TFF_Typed_Atom (Uninterpreted str, _))) = str
   710 
   711 fun interpret_line config inc_list type_map const_map path_prefix line thy =
   712   case line of
   713      Include (_, quoted_path, inc_list) =>
   714        interpret_file'
   715         config
   716         inc_list
   717         path_prefix
   718         (Path.append
   719           path_prefix
   720           (quoted_path
   721            |> unenclose
   722            |> Path.explode))
   723         type_map
   724         const_map
   725         thy
   726    | Annotated_Formula (_, lang, label, role, tptp_formula, annotation_opt) =>
   727        (*interpret a line only if "label" is in "inc_list", or if "inc_list" is
   728           empty (in which case interpret all lines)*)
   729        (*FIXME could work better if inc_list were sorted*)
   730        if null inc_list orelse is_some (List.find (fn x => x = label) inc_list) then
   731          case role of
   732            Role_Type =>
   733              let
   734                val thy_name = Context.theory_name thy
   735                val (tptp_ty, name) =
   736                  if lang = THF then
   737                    (typeof_typing tptp_formula (*assuming tptp_formula is a typing*),
   738                     nameof_typing tptp_formula (*and that the LHS is a (atom) name*))
   739                  else
   740                    (typeof_tff_typing tptp_formula,
   741                     nameof_tff_typing tptp_formula)
   742              in
   743                case tptp_ty of
   744                  Defined_type Type_Type => (*add new type*)
   745                    (*generate an Isabelle/HOL type to interpret this TPTP type,
   746                    and add it to both the Isabelle/HOL theory and to the type_map*)
   747                     let
   748                       val (type_map', thy') =
   749                         declare_type
   750                          config
   751                          (Atom_type name, name)
   752                          type_map
   753                          thy
   754                     in ((type_map',
   755                          const_map,
   756                          []),
   757                         thy')
   758                     end
   759 
   760                | _ => (*declaration of constant*)
   761                   (*Here we populate the map from constants to the Isabelle/HOL
   762                   terms they map to (which in turn contain their types).*)
   763                   let
   764                     val ty = interpret_type config thy type_map tptp_ty
   765                     (*make sure that the theory contains all the types appearing
   766                     in this constant's signature. Exception is thrown if encounter
   767                     an undeclared types.*)
   768                     val (t, thy') =
   769                       let
   770                         fun analyse_type thy thf_ty =
   771                            if #cautious config then
   772                             case thf_ty of
   773                                Fn_type (thf_ty1, thf_ty2) =>
   774                                  (analyse_type thy thf_ty1;
   775                                  analyse_type thy thf_ty2)
   776                              | Atom_type ty_name =>
   777                                  if type_exists config thy ty_name then ()
   778                                  else
   779                                   raise MISINTERPRET_TYPE
   780                                    ("Type (in signature of " ^
   781                                       name ^ ") has not been declared",
   782                                      Atom_type ty_name)
   783                              | _ => ()
   784                            else () (*skip test if we're not being cautious.*)
   785                       in
   786                         analyse_type thy tptp_ty;
   787                         declare_constant config name ty thy
   788                       end
   789                     (*register a mapping from name to t. Constants' type
   790                     declarations should occur at most once, so it's justified to
   791                     use "::". Note that here we use a constant's name rather
   792                     than the possibly- new one, since all references in the
   793                     theory will be to this name.*)
   794                     val const_map' = ((name, t) :: const_map)
   795                   in ((type_map,(*type_map unchanged, since a constant's
   796                                   declaration shouldn't include any new types.*)
   797                        const_map',(*typing table of constant was extended*)
   798                        []),(*no formulas were interpreted*)
   799                       thy')(*theory was extended with new constant*)
   800                   end
   801              end
   802 
   803          | _ => (*i.e. the AF is not a type declaration*)
   804              let
   805                (*gather interpreted term, and the map of types occurring in that term*)
   806                val (t, thy') =
   807                  interpret_formula config lang
   808                   const_map [] type_map tptp_formula thy
   809                  |>> HOLogic.mk_Trueprop
   810                (*type_maps grow monotonically, so return the newest value (type_mapped);
   811                there's no need to unify it with the type_map parameter.*)
   812              in
   813               ((type_map, const_map,
   814                 [(label, role,
   815                   Syntax.check_term (Proof_Context.init_global thy') t,
   816                   TPTP_Proof.extract_inference_info annotation_opt)]), thy')
   817              end
   818        else (*do nothing if we're not to includ this AF*)
   819          ((type_map, const_map, []), thy)
   820 
   821 and interpret_problem config inc_list path_prefix lines type_map const_map thy =
   822   let
   823     val thy_name = Context.theory_name thy
   824     val thy_with_symbols = add_interp_symbols_to_thy config type_map thy
   825   in
   826     fold (fn line =>
   827            fn ((type_map, const_map, lines), thy) =>
   828              let
   829                (*process the line, ignoring the type-context for variables*)
   830                val ((type_map', const_map', l'), thy') =
   831                  interpret_line config inc_list type_map const_map path_prefix line thy
   832                  (*FIXME
   833                    handle
   834                      (*package all exceptions to include position information,
   835                        even relating to multiple levels of "include"ed files*)
   836                        (*FIXME "exn" contents may appear garbled due to markup
   837                          FIXME this appears as ML source position *)
   838                        MISINTERPRET (pos_list, exn)  =>
   839                          raise MISINTERPRET
   840                            (TPTP_Syntax.pos_of_line line :: pos_list, exn)
   841                      | exn => raise MISINTERPRET
   842                          ([TPTP_Syntax.pos_of_line line], exn)
   843                   *)
   844              in
   845                ((type_map',
   846                  const_map',
   847                  l' @ lines),(*append is sufficient, union would be overkill*)
   848                 thy')
   849              end)
   850          lines (*lines of the problem file*)
   851          ((type_map, const_map, []), thy_with_symbols) (*initial values*)
   852   end
   853 
   854 and interpret_file' config inc_list path_prefix file_name =
   855   let
   856     val file_name' = Path.expand file_name
   857   in
   858     if Path.is_absolute file_name' then
   859       Path.implode file_name
   860       |> TPTP_Parser.parse_file
   861       |> interpret_problem config inc_list path_prefix
   862     else error "Could not determine absolute path to file"
   863   end
   864 
   865 and interpret_file cautious path_prefix file_name =
   866   let
   867     val config =
   868       {cautious = cautious,
   869        problem_name =
   870         SOME (TPTP_Problem_Name.parse_problem_name ((Path.base #> Path.implode)
   871          file_name))}
   872   in interpret_file' config [] path_prefix file_name end
   873 
   874 fun import_file cautious path_prefix file_name type_map const_map thy =
   875   let
   876     val prob_name =
   877       TPTP_Problem_Name.parse_problem_name (Path.implode (Path.base file_name))
   878     val (result, thy') =
   879       interpret_file cautious path_prefix file_name type_map const_map thy
   880   (*FIXME doesn't check if problem has already been interpreted*)
   881   in TPTP_Data.map (cons ((prob_name, result))) thy' end
   882 
   883 val _ =
   884   Outer_Syntax.improper_command @{command_spec "import_tptp"} "import TPTP problem"
   885     (Parse.path >> (fn path =>
   886       Toplevel.theory (fn thy =>
   887        (*NOTE: assumes include files are located at $TPTP/Axioms
   888          (which is how TPTP is organised)*)
   889        import_file true (Path.explode "$TPTP") path [] [] thy)))
   890 
   891 end