wneuper/isa: src/HOL/TPTP/TPTP_Parser/tptp

     1 (*  Title:      HOL/TPTP/TPTP_Parser/tptp_interpret.ML

     2     Author:     Nik Sultana, Cambridge University Computer Laboratory

     4 Interprets TPTP problems in Isabelle/HOL.

     5 *)

     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

    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

    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

    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

    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)

    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}

    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

    45   (*Map TPTP types to Isabelle/HOL types*)

    46   val interpret_type : config -> theory -> type_map ->

    47     TPTP_Syntax.tptp_type -> typ

    49   (*Map TPTP terms to Isabelle/HOL terms*)

    50   val interpret_term : bool -> config -> TPTP_Syntax.language -> theory ->

    51     const_map -> var_types -> type_map -> TPTP_Syntax.tptp_term ->

    52     term * theory

    54   val interpret_formula : config -> TPTP_Syntax.language -> const_map ->

    55     var_types -> type_map -> TPTP_Syntax.tptp_formula -> theory ->

    56     term * theory

    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

    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

    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

   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

   107   val import_file : bool -> Path.T -> Path.T -> type_map -> const_map ->

   108     theory -> theory

   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

   114   (*Returns the list of all files included in a directory and its

   115   subdirectories. This is only used for testing the parser/interpreter against

   116   all TPTP problems.*)

   117   val get_file_list : Path.T -> Path.T list

   118 end

   120 structure TPTP_Interpret : TPTP_INTERPRET =

   121 struct

   123 open TPTP_Syntax

   124 type position = string * int * int

   125 exception MISINTERPRET of position list * exn

   126 exception MISINTERPRET_FORMULA of string * TPTP_Syntax.tptp_formula

   127 exception MISINTERPRET_SYMBOL of string * TPTP_Syntax.symbol

   128 exception MISINTERPRET_TERM of string * TPTP_Syntax.tptp_term

   129 exception MISINTERPRET_TYPE of string * TPTP_Syntax.tptp_type

   132 (* General stuff *)

   134 type config =

   135   {cautious : bool,

   136    problem_name : TPTP_Problem_Name.problem_name option}

   139 (* Interpretation *)

   141 (** Signatures and other type abbrevations **)

   143 type const_map = (string * term) list

   144 type var_types = (string * typ option) list

   145 type type_map = (TPTP_Syntax.tptp_type * typ) list

   146 type inference_info = (string * string list) option

   147 type tptp_formula_meaning =

   148   string * TPTP_Syntax.role * term * inference_info

   149 type tptp_general_meaning =

   150   (type_map * const_map * tptp_formula_meaning list)

   152 type manifest = TPTP_Problem_Name.problem_name * tptp_general_meaning

   153 structure TPTP_Data = Theory_Data

   154   (type T = manifest list

   155    val empty = []

   156    val extend = I

   157    (*SMLNJ complains if non-expanded form used below*)

   158    fun merge v = Library.merge (op =) v)

   159 val get_manifests = TPTP_Data.get

   162 (** Adding types to a signature **)

   164 (*transform quoted names into acceptable ASCII strings*)

   165 fun alphanumerate c =

   166   let

   167     val c' = ord c

   168     val out_of_range =

   169       ((c' > 64) andalso (c' < 91)) orelse ((c' > 96)

   170        andalso (c' < 123)) orelse ((c' > 47) andalso (c' < 58))

   171   in

   172     if (not out_of_range) andalso (not (c = "_")) then

   173       "_nom_" ^ Int.toString (ord c) ^ "_"

   174     else c

   175   end

   176 fun alphanumerated_name prefix name =

   177   prefix ^ (raw_explode #> map alphanumerate #> implode) name

   179 (*SMLNJ complains if type annotation not used below*)

   180 fun mk_binding (config : config) ident =

   181   let

   182     val pre_binding = Binding.name (alphanumerated_name "bnd_" ident)

   183   in

   184     case #problem_name config of

   185       NONE => pre_binding

   186     | SOME prob =>

   187         Binding.qualify

   188          false

   189          (TPTP_Problem_Name.mangle_problem_name prob)

   190          pre_binding

   191   end

   193 fun type_exists config thy ty_name =

   194   Sign.declared_tyname thy (Sign.full_name thy (mk_binding config ty_name))

   196 (*Returns updated theory and the name of the final type's name -- i.e. if the

   197 original name is already taken then the function looks for an available

   198 alternative. It also returns an updated type_map if one has been passed to it.*)

   199 fun declare_type (config : config) (thf_type, type_name) ty_map thy =

   200   if type_exists config thy type_name then

   201     raise MISINTERPRET_TYPE ("Type already exists", Atom_type type_name)

   202   else

   203     let

   204       val binding = mk_binding config type_name

   205       val final_fqn = Sign.full_name thy binding

   206       val thy' =

   207         Typedecl.typedecl_global (mk_binding config type_name, [], NoSyn) thy

   208         |> snd

   209       val typ_map_entry = (thf_type, (Type (final_fqn, [])))

   210       val ty_map' = typ_map_entry :: ty_map

   211     in (ty_map', thy') end

   214 (** Adding constants to signature **)

   216 fun full_name thy config const_name =

   217   Sign.full_name thy (mk_binding config const_name)

   219 fun const_exists config thy const_name =

   220   Sign.declared_const thy (full_name thy config const_name)

   222 fun declare_constant config const_name ty thy =

   223   if const_exists config thy const_name then

   224     raise MISINTERPRET_TERM

   225      ("Const already declared", Term_Func (Uninterpreted const_name, []))

   226   else

   227     Theory.specify_const

   228      ((mk_binding config const_name, ty), NoSyn) thy

   231 (** Interpretation functions **)

   233 (*Types in THF are encoded as formulas. This function translates them to type form.*)

   234 (*FIXME possibly incomplete hack*)

   235 fun fmlatype_to_type (Atom (THF_Atom_term (Term_Func (TypeSymbol typ, [])))) =

   236       Defined_type typ

   237   | fmlatype_to_type (Atom (THF_Atom_term (Term_Func (Uninterpreted str, [])))) =

   238       Atom_type str

   239   | fmlatype_to_type (Type_fmla (Fn_type (ty1, ty2))) =

   240       let

   241         val ty1' = case ty1 of

   242             Fn_type _ => fmlatype_to_type (Type_fmla ty1)

   243           | Fmla_type ty1 => fmlatype_to_type ty1

   244         val ty2' = case ty2 of

   245             Fn_type _ => fmlatype_to_type (Type_fmla ty2)

   246           | Fmla_type ty2 => fmlatype_to_type ty2

   247       in Fn_type (ty1', ty2') end

   249 fun interpret_type config thy type_map thf_ty =

   250   let

   251     fun lookup_type ty_map thf_ty =

   252       (case AList.lookup (op =) ty_map thf_ty of

   253           NONE =>

   254             raise MISINTERPRET_TYPE

   255               ("Could not find the interpretation of this TPTP type in the \

   256                \mapping to Isabelle/HOL", thf_ty)

   257         | SOME ty => ty)

   258   in

   259     case thf_ty of

   260        Prod_type (thf_ty1, thf_ty2) =>

   261          Type ("Product_Type.prod",

   262           [interpret_type config thy type_map thf_ty1,

   263            interpret_type config thy type_map thf_ty2])

   264      | Fn_type (thf_ty1, thf_ty2) =>

   265          Type ("fun",

   266           [interpret_type config thy type_map thf_ty1,

   267            interpret_type config thy type_map thf_ty2])

   268      | Atom_type _ =>

   269          lookup_type type_map thf_ty

   270      | Defined_type tptp_base_type =>

   271          (case tptp_base_type of

   272             Type_Ind => @{typ ind}

   273           | Type_Bool => HOLogic.boolT

   274           | Type_Type => raise MISINTERPRET_TYPE ("No type interpretation", thf_ty)

   275           | Type_Int => Type ("Int.int", [])

   276          (*FIXME these types are currently unsupported, so they're treated as

   277          individuals*)

   278           | Type_Rat =>

   279               interpret_type config thy type_map (Defined_type Type_Ind)

   280           | Type_Real =>

   281               interpret_type config thy type_map (Defined_type Type_Ind)

   282           )

   283      | Sum_type _ =>

   284          raise MISINTERPRET_TYPE (*FIXME*)

   285           ("No type interpretation (sum type)", thf_ty)

   286      | Fmla_type tptp_ty =>

   287         fmlatype_to_type tptp_ty

   288         |> interpret_type config thy type_map

   289      | Subtype _ =>

   290          raise MISINTERPRET_TYPE (*FIXME*)

   291           ("No type interpretation (subtype)", thf_ty)

   292   end

   294 fun the_const config thy language const_map_payload str =

   295   if language = THF then

   296     (case AList.lookup (op =) const_map_payload str of

   297         NONE => raise MISINTERPRET_TERM

   298           ("Could not find the interpretation of this constant in the \

   299             \mapping to Isabelle/HOL", Term_Func (Uninterpreted str, []))

   300       | SOME t => t)

   301   else

   302     if const_exists config thy str then

   303        Sign.mk_const thy ((Sign.full_name thy (mk_binding config str)), [])

   304     else raise MISINTERPRET_TERM

   305           ("Could not find the interpretation of this constant in the \

   306             \mapping to Isabelle/HOL", Term_Func (Uninterpreted str, []))

   308 (*Eta-expands Isabelle/HOL binary function.

   309  "str" is the name of a polymorphic constant in Isabelle/HOL*)

   310 fun mk_fun str =

   311   (Const (str, Term.dummyT) $ Bound 1 $ Bound 0)

   312    |> (Term.absdummy Term.dummyT #> Term.absdummy Term.dummyT)

   313 (*As above, but swaps the function's arguments*)

   314 fun mk_swapped_fun str =

   315   (Const (str, Term.dummyT) $ Bound 0 $ Bound 1)

   316    |> (Term.absdummy Term.dummyT #> Term.absdummy Term.dummyT)

   318 fun dummy_term () =

   319   HOLogic.choice_const Term.dummyT $ Term.absdummy Term.dummyT @{term "True"}

   321 fun interpret_symbol config thy language const_map symb =

   322   case symb of

   323      Uninterpreted n =>

   324        (*Constant would have been added to the map at the time of

   325        declaration*)

   326        the_const config thy language const_map n

   327    | Interpreted_ExtraLogic interpreted_symbol =>

   328        (case interpreted_symbol of (*FIXME incomplete,

   329                                      and doesn't work with $i*)

   330           Sum => mk_fun @{const_name Groups.plus}

   331         | UMinus =>

   332             (Const (@{const_name Groups.uminus}, Term.dummyT) $ Bound 0)

   333              |> Term.absdummy Term.dummyT

   334         | Difference => mk_fun @{const_name Groups.minus}

   335         | Product => mk_fun @{const_name Groups.times}

   336         | Quotient => mk_fun @{const_name Fields.divide}

   337         | Less => mk_fun @{const_name Orderings.less}

   338         | LessEq => mk_fun @{const_name Orderings.less_eq}

   339         | Greater => mk_swapped_fun @{const_name Orderings.less}

   340           (*FIXME would be nicer to expand "greater"

   341             and "greater_eq" abbreviations*)

   342         | GreaterEq => mk_swapped_fun @{const_name Orderings.less_eq}

   343         (* FIXME todo

   344         | Quotient_E | Quotient_T | Quotient_F | Remainder_E | Remainder_T

   345         | Remainder_F | Floor | Ceiling | Truncate | Round | To_Int | To_Rat

   346         | To_Real | EvalEq | Is_Int | Is_Rat*)

   347         | Apply => raise MISINTERPRET_SYMBOL ("Malformed term?", symb)

   348         | _ => dummy_term ()

   349         )

   350    | Interpreted_Logic logic_symbol =>

   351        (case logic_symbol of

   352           Equals => HOLogic.eq_const Term.dummyT

   353         | NEquals =>

   354            HOLogic.mk_not (HOLogic.eq_const Term.dummyT $ Bound 1 $ Bound 0)

   355            |> (Term.absdummy Term.dummyT #> Term.absdummy Term.dummyT)

   356         | Or => HOLogic.disj

   357         | And => HOLogic.conj

   358         | Iff => HOLogic.eq_const HOLogic.boolT

   359         | If => HOLogic.imp

   360         | Fi => @{term "\<lambda> x. \<lambda> y. y \<longrightarrow> x"}

   361         | Xor =>

   362             @{term

   363               "\<lambda> x. \<lambda> y. \<not> (x \<longleftrightarrow> y)"}

   364         | Nor => @{term "\<lambda> x. \<lambda> y. \<not> (x \<or> y)"}

   365         | Nand => @{term "\<lambda> x. \<lambda> y. \<not> (x \<and> y)"}

   366         | Not => HOLogic.Not

   367         | Op_Forall => HOLogic.all_const Term.dummyT

   368         | Op_Exists => HOLogic.exists_const Term.dummyT

   369         | True => @{term "True"}

   370         | False => @{term "False"}

   371         )

   372    | TypeSymbol _ =>

   373        raise MISINTERPRET_SYMBOL

   374         ("Cannot have TypeSymbol in term", symb)

   375    | System str =>

   376        raise MISINTERPRET_SYMBOL

   377         ("Cannot interpret system symbol", symb)

   379 (*Apply a function to a list of arguments*)

   380 val mapply = fold (fn x => fn y => y $ x)

   381 (*As above, but for products*)

   382 fun mtimes thy =

   383   fold (fn x => fn y =>

   384     Sign.mk_const thy

   385     ("Product_Type.Pair",[Term.dummyT, Term.dummyT]) $ y $ x)

   387 (*Adds constants to signature in FOL. "formula_level" means that the constants

   388 are to be interpreted as predicates, otherwise as functions over individuals.*)

   389 fun FO_const_types config formula_level type_map tptp_t thy =

   390   let

   391     val ind_type = interpret_type config thy type_map (Defined_type Type_Ind)

   392     val value_type =

   393       if formula_level then

   394         interpret_type config thy type_map (Defined_type Type_Bool)

   395       else ind_type

   396   in case tptp_t of

   397       Term_Func (symb, tptp_ts) =>

   398         let

   399           val thy' = fold (FO_const_types config false type_map) tptp_ts thy

   400           val ty = fold (fn ty1 => fn ty2 => Type ("fun", [ty1, ty2]))

   401             (map (fn _ => ind_type) tptp_ts) value_type

   402         in

   403           case symb of

   404              Uninterpreted const_name =>

   405                  if const_exists config thy' const_name then thy'

   406                  else snd (declare_constant config const_name ty thy')

   407            | _ => thy'

   408         end

   409      | _ => thy

   410   end

   412 (*like FO_const_types but works over symbols*)

   413 fun symb_const_types config type_map formula_level const_name n_args thy =

   414   let

   415     val ind_type = interpret_type config thy type_map (Defined_type Type_Ind)

   416     val value_type =

   417       if formula_level then

   418         interpret_type config thy type_map (Defined_type Type_Bool)

   419       else interpret_type config thy type_map (Defined_type Type_Ind)

   420     fun mk_i_fun b n acc =

   421       if n = 0 then acc b

   422       else

   423         mk_i_fun b (n - 1) (fn ty => Type ("fun", [ind_type, acc ty]))

   424   in

   425     if const_exists config thy const_name then thy

   426     else

   427       snd (declare_constant config const_name

   428            (mk_i_fun value_type n_args I) thy)

   429   end

   431 (*Next batch of functions give info about Isabelle/HOL types*)

   432 fun is_fun (Type ("fun", _)) = true

   433   | is_fun _ = false

   434 fun is_prod (Type ("Product_Type.prod", _)) = true

   435   | is_prod _ = false

   436 fun dom_type (Type ("fun", [ty1, _])) = ty1

   437 fun is_prod_typed thy config symb =

   438   let

   439     fun symb_type const_name =

   440       Sign.the_const_type thy (full_name thy config const_name)

   441   in

   442     case symb of

   443        Uninterpreted const_name =>

   444          if is_fun (symb_type const_name) then

   445            symb_type const_name |> dom_type |> is_prod

   446          else false

   447      | _ => false

   448    end

   451 (*

   452  Information needed to be carried around:

   453  - constant mapping: maps constant names to Isabelle terms with fully-qualified

   454     names. This is fixed, and it is determined by declaration lines earlier

   455     in the script (i.e. constants must be declared before appearing in terms.

   456  - type context: maps bound variables to their Isabelle type. This is discarded

   457     after each call of interpret_term since variables' cannot be bound across

   458     terms.

   459 *)

   460 fun interpret_term formula_level config language thy const_map var_types type_map

   461  tptp_t =

   462   case tptp_t of

   463     Term_Func (symb, tptp_ts) =>

   464        let

   465          val thy' = FO_const_types config formula_level type_map tptp_t thy

   466          fun typeof_const const_name = Sign.the_const_type thy'

   467              (Sign.full_name thy' (mk_binding config const_name))

   468        in

   469          case symb of

   470            Interpreted_ExtraLogic Apply =>

   471              (*apply the head of the argument list to the tail*)

   472              (mapply

   473                (map (interpret_term false config language thy' const_map

   474                 var_types type_map #> fst) (tl tptp_ts))

   475                (interpret_term formula_level config language thy' const_map

   476                 var_types type_map (hd tptp_ts) |> fst),

   477               thy')

   478            | _ =>

   479               (*apply symb to tptp_ts*)

   480               if is_prod_typed thy' config symb then

   481                 (interpret_symbol config thy' language const_map symb $

   482                   mtimes thy'

   483                   (map (interpret_term false config language thy' const_map

   484                    var_types type_map #> fst) (tl tptp_ts))

   485                   ((interpret_term false config language thy' const_map

   486                    var_types type_map #> fst) (hd tptp_ts)),

   487                  thy')

   488               else

   489                 (mapply

   490                   (map (interpret_term false config language thy' const_map

   491                    var_types type_map #> fst) tptp_ts)

   492                   (interpret_symbol config thy' language const_map symb),

   493                  thy')

   494        end

   495   | Term_Var n =>

   496      (if language = THF orelse language = TFF then

   497         (case AList.lookup (op =) var_types n of

   498            SOME ty =>

   499              (case ty of

   500                 SOME ty => Free (n, ty)

   501               | NONE => Free (n, Term.dummyT) (*to infer the variable's type*)

   502              )

   503          | NONE =>

   504              raise MISINTERPRET_TERM ("Could not type variable", tptp_t))

   505       else (*variables range over individuals*)

   506         Free (n, interpret_type config thy type_map (Defined_type Type_Ind)),

   507       thy)

   508   | Term_Conditional (tptp_formula, tptp_t1, tptp_t2) =>

   509       (mk_fun @{const_name If}, thy)

   510   | Term_Num (number_kind, num) =>

   511       let

   512         val num_term =

   513           if number_kind = Int_num then

   514             HOLogic.mk_number @{typ "int"} (the (Int.fromString num))

   515           else dummy_term () (*FIXME: not yet supporting rationals and reals*)

   516       in (num_term, thy) end

   517   | Term_Distinct_Object str =>

   518       declare_constant config (alphanumerated_name "ds_" str)

   519         (interpret_type config thy type_map (Defined_type Type_Ind)) thy

   521 (*Given a list of "'a option", then applies a function to each element if that

   522 element is SOME value, otherwise it leaves it as NONE.*)

   523 fun map_opt f xs =

   524   fold

   525   (fn x => fn y =>

   526     (if Option.isSome x then

   527        SOME (f (Option.valOf x))

   528      else NONE) :: y

   529   ) xs []

   531 fun interpret_formula config language const_map var_types type_map tptp_fmla thy =

   532   case tptp_fmla of

   533       Pred app =>

   534         interpret_term true config language thy const_map

   535          var_types type_map (Term_Func app)

   536     | Fmla (symbol, tptp_formulas) =>

   537        (case symbol of

   538           Interpreted_ExtraLogic Apply =>

   539             let

   540               val (args, thy') = (fold_map (interpret_formula config language

   541                const_map var_types type_map) (tl tptp_formulas) thy)

   542               val (func, thy') = interpret_formula config language const_map

   543                var_types type_map (hd tptp_formulas) thy'

   544             in (mapply args func, thy') end

   545         | Uninterpreted const_name =>

   546             let

   547               val (args, thy') = (fold_map (interpret_formula config language

   548                const_map var_types type_map) tptp_formulas thy)

   549               val thy' = symb_const_types config type_map true const_name

   550                (length tptp_formulas) thy'

   551             in

   552               (if is_prod_typed thy' config symbol then

   553                  mtimes thy' args (interpret_symbol config thy' language

   554                   const_map symbol)

   555                else

   556                 mapply args

   557                  (interpret_symbol config thy' language const_map symbol),

   558               thy')

   559             end

   560         | _ =>

   561             let

   562               val (args, thy') =

   563                 fold_map

   564                  (interpret_formula config language

   565                   const_map var_types type_map)

   566                  tptp_formulas thy

   567             in

   568               (if is_prod_typed thy' config symbol then

   569                  mtimes thy' args (interpret_symbol config thy' language

   570                   const_map symbol)

   571                else

   572                  mapply args

   573                   (interpret_symbol config thy' language const_map symbol),

   574                thy')

   575             end)

   576     | Sequent _ =>

   577         (*FIXME unsupported*)

   578         raise MISINTERPRET_FORMULA ("'Sequent' unsupported", tptp_fmla)

   579     | Quant (quantifier, bindings, tptp_formula) =>

   580         let

   581           val (bound_vars, bound_var_types) = ListPair.unzip bindings

   582           val bound_var_types' : typ option list =

   583             (map_opt : (tptp_type -> typ) ->

   584              (tptp_type option list) -> typ option list)

   585             (interpret_type config thy type_map) bound_var_types

   586           val var_types' =

   587             ListPair.zip (bound_vars, List.rev bound_var_types')

   588             |> List.rev

   589           fun fold_bind f =

   590             fold

   591               (fn (n, ty) => fn t =>

   592                  case ty of

   593                    NONE =>

   594                      f (n,

   595                         if language = THF then Term.dummyT

   596                         else

   597                           interpret_type config thy type_map

   598                            (Defined_type Type_Ind),

   599                         t)

   600                  | SOME ty => f (n, ty, t)

   601               )

   602               var_types'

   603         in case quantifier of

   604           Forall =>

   605             interpret_formula config language const_map (var_types' @ var_types)

   606              type_map tptp_formula thy

   607             |>> fold_bind HOLogic.mk_all

   608         | Exists =>

   609             interpret_formula config language const_map (var_types' @ var_types)

   610              type_map tptp_formula thy

   611             |>> fold_bind HOLogic.mk_exists

   612         | Lambda =>

   613             interpret_formula config language const_map (var_types' @ var_types)

   614              type_map tptp_formula thy

   615             |>> fold_bind (fn (n, ty, rest) => lambda (Free (n, ty)) rest)

   616         | Epsilon =>

   617             let val (t, thy') =

   618               interpret_formula config language const_map var_types type_map

   619                (Quant (Lambda, bindings, tptp_formula)) thy

   620             in ((HOLogic.choice_const Term.dummyT) $ t, thy') end

   621         | Iota =>

   622             let val (t, thy') =

   623               interpret_formula config language const_map var_types type_map

   624                (Quant (Lambda, bindings, tptp_formula)) thy

   625             in (Const (@{const_name The}, Term.dummyT) $ t, thy') end

   626         | Dep_Prod =>

   627             raise MISINTERPRET_FORMULA ("Unsupported", tptp_fmla)

   628         | Dep_Sum =>

   629             raise MISINTERPRET_FORMULA ("Unsupported", tptp_fmla)

   630         end

   631     | Conditional (fmla1, fmla2, fmla3) =>

   632         let

   633           val interp = interpret_formula config language const_map var_types type_map

   634           val (((fmla1', fmla2'), fmla3'), thy') =

   635             interp fmla1 thy

   636             ||>> interp fmla2

   637             ||>> interp fmla3

   638         in (HOLogic.mk_conj (HOLogic.mk_imp (fmla1', fmla2'),

   639                              HOLogic.mk_imp (HOLogic.mk_not fmla1', fmla3')),

   640             thy')

   641         end

   642     | Let (tptp_let_list, tptp_formula) => (*FIXME not yet implemented*)

   643         raise MISINTERPRET_FORMULA ("'Let' not yet implemented", tptp_fmla)

   644     | Atom tptp_atom =>

   645         (case tptp_atom of

   646           TFF_Typed_Atom (symbol, tptp_type_opt) =>

   647             (*FIXME ignoring type info*)

   648             (interpret_symbol config thy language const_map symbol, thy)

   649         | THF_Atom_term tptp_term =>

   650             interpret_term true config language thy const_map var_types

   651              type_map tptp_term

   652         | THF_Atom_conn_term symbol =>

   653             (interpret_symbol config thy language const_map symbol, thy))

   654     | Type_fmla _ =>

   655          raise MISINTERPRET_FORMULA

   656           ("Cannot interpret types as formulas", tptp_fmla)

   657     | THF_typing (tptp_formula, _) => (*FIXME ignoring type info*)

   658         interpret_formula config language

   659          const_map var_types type_map tptp_formula thy

   661 (*Extract the type from a typing*)

   662 local

   663   fun extract_type tptp_type =

   664     case tptp_type of

   665         Fmla_type typ => fmlatype_to_type typ

   666       | _ => tptp_type

   667 in

   668   fun typeof_typing (THF_typing (_, tptp_type)) = extract_type tptp_type

   669   fun typeof_tff_typing (Atom (TFF_Typed_Atom (_, SOME tptp_type))) =

   670     extract_type tptp_type

   671 end

   672 fun nameof_typing

   673   (THF_typing

   674      ((Atom (THF_Atom_term (Term_Func (Uninterpreted str, [])))), _)) = str

   675 fun nameof_tff_typing (Atom (TFF_Typed_Atom (Uninterpreted str, _))) = str

   677 fun interpret_line config inc_list type_map const_map path_prefix line thy =

   678   case line of

   679      Include (_, quoted_path, inc_list) =>

   680        interpret_file'

   681         config

   682         inc_list

   683         path_prefix

   684         (Path.append

   685           path_prefix

   686           (quoted_path

   687            |> unenclose

   688            |> Path.explode))

   689         type_map

   690         const_map

   691         thy

   692    | Annotated_Formula (_, lang, label, role, tptp_formula, annotation_opt) =>

   693        (*interpret a line only if "label" is in "inc_list", or if "inc_list" is

   694           empty (in which case interpret all lines)*)

   695        (*FIXME could work better if inc_list were sorted*)

   696        if null inc_list orelse is_some (List.find (fn x => x = label) inc_list) then

   697          case role of

   698            Role_Type =>

   699              let

   700                val thy_name = Context.theory_name thy

   701                val (tptp_ty, name) =

   702                  if lang = THF then

   703                    (typeof_typing tptp_formula (*assuming tptp_formula is a typing*),

   704                     nameof_typing tptp_formula (*and that the LHS is a (atom) name*))

   705                  else

   706                    (typeof_tff_typing tptp_formula,

   707                     nameof_tff_typing tptp_formula)

   708              in

   709                case tptp_ty of

   710                  Defined_type Type_Type => (*add new type*)

   711                    (*generate an Isabelle/HOL type to interpret this TPTP type,

   712                    and add it to both the Isabelle/HOL theory and to the type_map*)

   713                     let

   714                       val (type_map', thy') =

   715                         declare_type

   716                          config

   717                          (Atom_type name, name)

   718                          type_map

   719                          thy

   720                     in ((type_map',

   721                          const_map,

   722                          []),

   723                         thy')

   724                     end

   726                | _ => (*declaration of constant*)

   727                   (*Here we populate the map from constants to the Isabelle/HOL

   728                   terms they map to (which in turn contain their types).*)

   729                   let

   730                     val ty = interpret_type config thy type_map tptp_ty

   731                     (*make sure that the theory contains all the types appearing

   732                     in this constant's signature. Exception is thrown if encounter

   733                     an undeclared types.*)

   734                     val (t, thy') =

   735                       let

   736                         fun analyse_type thy thf_ty =

   737                            if #cautious config then

   738                             case thf_ty of

   739                                Fn_type (thf_ty1, thf_ty2) =>

   740                                  (analyse_type thy thf_ty1;

   741                                  analyse_type thy thf_ty2)

   742                              | Atom_type ty_name =>

   743                                  if type_exists config thy ty_name then ()

   744                                  else

   745                                   raise MISINTERPRET_TYPE

   746                                    ("Type (in signature of " ^

   747                                       name ^ ") has not been declared",

   748                                      Atom_type ty_name)

   749                              | _ => ()

   750                            else () (*skip test if we're not being cautious.*)

   751                       in

   752                         analyse_type thy tptp_ty;

   753                         declare_constant config name ty thy

   754                       end

   755                     (*register a mapping from name to t. Constants' type

   756                     declarations should occur at most once, so it's justified to

   757                     use "::". Note that here we use a constant's name rather

   758                     than the possibly- new one, since all references in the

   759                     theory will be to this name.*)

   760                     val const_map' = ((name, t) :: const_map)

   761                   in ((type_map,(*type_map unchanged, since a constant's

   762                                   declaration shouldn't include any new types.*)

   763                        const_map',(*typing table of constant was extended*)

   764                        []),(*no formulas were interpreted*)

   765                       thy')(*theory was extended with new constant*)

   766                   end

   767              end

   769          | _ => (*i.e. the AF is not a type declaration*)

   770              let

   771                (*gather interpreted term, and the map of types occurring in that term*)

   772                val (t, thy') =

   773                  interpret_formula config lang

   774                   const_map [] type_map tptp_formula thy

   775                  |>> HOLogic.mk_Trueprop

   776                (*type_maps grow monotonically, so return the newest value (type_mapped);

   777                there's no need to unify it with the type_map parameter.*)

   778              in

   779               ((type_map, const_map,

   780                 [(label, role,

   781                   Syntax.check_term (Proof_Context.init_global thy') t,

   782                   TPTP_Proof.extract_inference_info annotation_opt)]), thy')

   783              end

   784        else (*do nothing if we're not to includ this AF*)

   785          ((type_map, const_map, []), thy)

   787 and interpret_problem config inc_list path_prefix lines type_map const_map thy =

   788   let

   789     val thy_name = Context.theory_name thy

   790   in

   791     fold (fn line =>

   792            fn ((type_map, const_map, lines), thy) =>

   793              let

   794                (*process the line, ignoring the type-context for variables*)

   795                val ((type_map', const_map', l'), thy') =

   796                  interpret_line config inc_list type_map const_map path_prefix line thy

   797                    handle

   798                      (*package all exceptions to include position information,

   799                        even relating to multiple levels of "include"ed files*)

   800                        (*FIXME "exn" contents may appear garbled due to markup

   801                          FIXME this appears as ML source position *)

   802                        MISINTERPRET (pos_list, exn)  =>

   803                          raise MISINTERPRET

   804                            (TPTP_Syntax.pos_of_line line :: pos_list, exn)

   805                      | exn => raise MISINTERPRET

   806                          ([TPTP_Syntax.pos_of_line line], exn)

   807              in

   808                ((type_map',

   809                  const_map',

   810                  l' @ lines),(*append is sufficient, union would be overkill*)

   811                 thy')

   812              end)

   813          lines (*lines of the problem file*)

   814          ((type_map, const_map, []), thy) (*initial values*)

   815   end

   817 and interpret_file' config inc_list path_prefix file_name =

   818   let

   819     val file_name' = Path.expand file_name

   820   in

   821     if Path.is_absolute file_name' then

   822       Path.implode file_name

   823       |> TPTP_Parser.parse_file

   824       |> interpret_problem config inc_list path_prefix

   825     else error "Could not determine absolute path to file"

   826   end

   828 and interpret_file cautious path_prefix file_name =

   829   let

   830     val config =

   831       {cautious = cautious,

   832        problem_name =

   833         SOME (TPTP_Problem_Name.parse_problem_name ((Path.base #> Path.implode)

   834          file_name))}

   835   in interpret_file' config [] path_prefix file_name end

   837 fun import_file cautious path_prefix file_name type_map const_map thy =

   838   let

   839     val prob_name =

   840       TPTP_Problem_Name.parse_problem_name (Path.implode (Path.base file_name))

   841     val (result, thy') =

   842       interpret_file cautious path_prefix file_name type_map const_map thy

   843   (*FIXME doesn't check if problem has already been interpreted*)

   844   in TPTP_Data.map (cons ((prob_name, result))) thy' end

   846 val _ =

   847   Outer_Syntax.improper_command @{command_spec "import_tptp"} "import TPTP problem"

   848     (Parse.path >> (fn path =>

   849       Toplevel.theory (fn thy =>

   850        (*NOTE: assumes include files are located at $TPTP/Axioms

   851          (which is how TPTP is organised)*)

   852        import_file true (Path.explode "$TPTP") path [] [] thy)))

   855 (*Used for debugging. Returns all files contained within a directory or its

   856 subdirectories. Follows symbolic links, filters away directories.*)

   857 fun get_file_list path =

   858   let

   859     fun check_file_entry f rest =

   860       let

   861         (*NOTE needed since don't have File.is_link and File.read_link*)

   862         val f_str = Path.implode f

   863       in

   864         if File.is_dir f then

   865           rest (*filter out directories*)

   866         else if OS.FileSys.isLink f_str then

   867           (*follow links -- NOTE this breaks if links are relative paths*)

   868           check_file_entry (Path.explode (OS.FileSys.readLink f_str)) rest

   869         else f :: rest

   870       end

   871   in

   872     File.read_dir path

   873     |> map

   874         (Path.explode

   875         #> Path.append path)

   876     |> (fn l => fold check_file_entry l [])

   877   end

   879 end

author	sultana
	Thu, 19 Apr 2012 07:25:41 +0100
changeset 48440	fce9d97a3258
parent 48429	55b42f9af99d
child 48441	df3c9aa6c9dc
permissions	-rw-r--r--