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   exception MISINTERPRET_FORMULA of string * TPTP_Syntax.tptp_formula

   101   exception MISINTERPRET_SYMBOL of string * TPTP_Syntax.symbol

   102   exception MISINTERPRET_TERM of string * TPTP_Syntax.tptp_term

   103   exception MISINTERPRET_TYPE of string * TPTP_Syntax.tptp_type

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

   106     theory -> theory

   108   (*Imported TPTP files are stored as "manifests" in the theory.*)

   109   type manifest = TPTP_Problem_Name.problem_name * tptp_general_meaning

   110   val get_manifests : theory -> manifest list

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

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

   114   all TPTP problems.*)

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

   116 end

   118 structure TPTP_Interpret : TPTP_INTERPRET =

   119 struct

   121 open TPTP_Syntax

   122 exception MISINTERPRET_FORMULA of string * TPTP_Syntax.tptp_formula

   123 exception MISINTERPRET_SYMBOL of string * TPTP_Syntax.symbol

   124 exception MISINTERPRET_TERM of string * TPTP_Syntax.tptp_term

   125 exception MISINTERPRET_TYPE of string * TPTP_Syntax.tptp_type

   128 (* General stuff *)

   130 type config =

   131   {cautious : bool,

   132    problem_name : TPTP_Problem_Name.problem_name option}

   135 (* Interpretation *)

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

   139 type const_map = (string * term) list

   140 type var_types = (string * typ option) list

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

   142 type inference_info = (string * string list) option

   143 type tptp_formula_meaning =

   144   string * TPTP_Syntax.role * term * inference_info

   145 type tptp_general_meaning =

   146   (type_map * const_map * tptp_formula_meaning list)

   148 type manifest = TPTP_Problem_Name.problem_name * tptp_general_meaning

   149 structure TPTP_Data = Theory_Data

   150   (type T = manifest list

   151    val empty = []

   152    val extend = I

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

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

   155 val get_manifests = TPTP_Data.get

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

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

   161 fun alphanumerate c =

   162   let

   163     val c' = ord c

   164     val out_of_range =

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

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

   167   in

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

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

   170     else c

   171   end

   172 fun alphanumerated_name prefix name =

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

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

   176 fun mk_binding (config : config) ident =

   177   let

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

   179   in

   180     case #problem_name config of

   181       NONE => pre_binding

   182     | SOME prob =>

   183         Binding.qualify

   184          false

   185          (TPTP_Problem_Name.mangle_problem_name prob)

   186          pre_binding

   187   end

   189 fun type_exists config thy ty_name =

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

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

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

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

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

   196   if type_exists config thy type_name then

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

   198   else

   199     let

   200       val binding = mk_binding config type_name

   201       val final_fqn = Sign.full_name thy binding

   202       val thy' =

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

   204         |> snd

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

   206       val ty_map' = typ_map_entry :: ty_map

   207     in (ty_map', thy') end

   210 (** Adding constants to signature **)

   212 fun full_name thy config const_name =

   213   Sign.full_name thy (mk_binding config const_name)

   215 fun const_exists config thy const_name =

   216   Sign.declared_const thy (full_name thy config const_name)

   218 fun declare_constant config const_name ty thy =

   219   if const_exists config thy const_name then

   220     raise MISINTERPRET_TERM

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

   222   else

   223     Theory.specify_const

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

   227 (** Interpretation functions **)

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

   230 (*FIXME possibly incomplete hack*)

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

   232       Defined_type typ

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

   234       Atom_type str

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

   236       let

   237         val ty1' = case ty1 of

   238             Fn_type _ => fmlatype_to_type (Type_fmla ty1)

   239           | Fmla_type ty1 => fmlatype_to_type ty1

   240         val ty2' = case ty2 of

   241             Fn_type _ => fmlatype_to_type (Type_fmla ty2)

   242           | Fmla_type ty2 => fmlatype_to_type ty2

   243       in Fn_type (ty1', ty2') end

   245 fun interpret_type config thy type_map thf_ty =

   246   let

   247     fun lookup_type ty_map thf_ty =

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

   249           NONE =>

   250             raise MISINTERPRET_TYPE

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

   252                \mapping to Isabelle/HOL", thf_ty)

   253         | SOME ty => ty)

   254   in

   255     case thf_ty of

   256        Prod_type (thf_ty1, thf_ty2) =>

   257          Type ("Product_Type.prod",

   258           [interpret_type config thy type_map thf_ty1,

   259            interpret_type config thy type_map thf_ty2])

   260      | Fn_type (thf_ty1, thf_ty2) =>

   261          Type ("fun",

   262           [interpret_type config thy type_map thf_ty1,

   263            interpret_type config thy type_map thf_ty2])

   264      | Atom_type _ =>

   265          lookup_type type_map thf_ty

   266      | Defined_type tptp_base_type =>

   267          (case tptp_base_type of

   268             Type_Ind => @{typ ind}

   269           | Type_Bool => HOLogic.boolT

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

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

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

   273          individuals*)

   274           | Type_Rat =>

   275               interpret_type config thy type_map (Defined_type Type_Ind)

   276           | Type_Real =>

   277               interpret_type config thy type_map (Defined_type Type_Ind)

   278           )

   279      | Sum_type _ =>

   280          raise MISINTERPRET_TYPE (*FIXME*)

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

   282      | Fmla_type tptp_ty =>

   283         fmlatype_to_type tptp_ty

   284         |> interpret_type config thy type_map

   285      | Subtype _ =>

   286          raise MISINTERPRET_TYPE (*FIXME*)

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

   288   end

   290 fun the_const config thy language const_map_payload str =

   291   if language = THF then

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

   293         NONE => raise MISINTERPRET_TERM

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

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

   296       | SOME t => t)

   297   else

   298     if const_exists config thy str then

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

   300     else raise MISINTERPRET_TERM

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

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

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

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

   306 fun mk_fun str =

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

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

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

   310 fun mk_swapped_fun str =

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

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

   314 fun dummy_term () =

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

   317 fun interpret_symbol config thy language const_map symb =

   318   case symb of

   319      Uninterpreted n =>

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

   321        declaration*)

   322        the_const config thy language const_map n

   323    | Interpreted_ExtraLogic interpreted_symbol =>

   324        (case interpreted_symbol of (*FIXME incomplete,

   325                                      and doesn't work with $i*)

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

   327         | UMinus =>

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

   329              |> Term.absdummy Term.dummyT

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

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

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

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

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

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

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

   337             and "greater_eq" abbreviations*)

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

   339         (* FIXME todo

   340         | Quotient_E | Quotient_T | Quotient_F | Remainder_E | Remainder_T

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

   342         | To_Real | EvalEq | Is_Int | Is_Rat*)

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

   344         | _ => dummy_term ()

   345         )

   346    | Interpreted_Logic logic_symbol =>

   347        (case logic_symbol of

   348           Equals => HOLogic.eq_const Term.dummyT

   349         | NEquals =>

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

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

   352         | Or => HOLogic.disj

   353         | And => HOLogic.conj

   354         | Iff => HOLogic.eq_const HOLogic.boolT

   355         | If => HOLogic.imp

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

   357         | Xor =>

   358             @{term

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

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

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

   362         | Not => HOLogic.Not

   363         | Op_Forall => HOLogic.all_const Term.dummyT

   364         | Op_Exists => HOLogic.exists_const Term.dummyT

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

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

   367         )

   368    | TypeSymbol _ =>

   369        raise MISINTERPRET_SYMBOL

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

   371    | System str =>

   372        raise MISINTERPRET_SYMBOL

   373         ("Cannot interpret system symbol", symb)

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

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

   377 (*As above, but for products*)

   378 fun mtimes thy =

   379   fold (fn x => fn y =>

   380     Sign.mk_const thy

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

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

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

   385 fun FO_const_types config formula_level type_map tptp_t thy =

   386   let

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

   388     val value_type =

   389       if formula_level then

   390         interpret_type config thy type_map (Defined_type Type_Bool)

   391       else ind_type

   392   in case tptp_t of

   393       Term_Func (symb, tptp_ts) =>

   394         let

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

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

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

   398         in

   399           case symb of

   400              Uninterpreted const_name =>

   401                  if const_exists config thy' const_name then thy'

   402                  else snd (declare_constant config const_name ty thy')

   403            | _ => thy'

   404         end

   405      | _ => thy

   406   end

   408 (*like FO_const_types but works over symbols*)

   409 fun symb_const_types config type_map formula_level const_name n_args thy =

   410   let

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

   412     val value_type =

   413       if formula_level then

   414         interpret_type config thy type_map (Defined_type Type_Bool)

   415       else interpret_type config thy type_map (Defined_type Type_Ind)

   416     fun mk_i_fun b n acc =

   417       if n = 0 then acc b

   418       else

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

   420   in

   421     if const_exists config thy const_name then thy

   422     else

   423       snd (declare_constant config const_name

   424            (mk_i_fun value_type n_args I) thy)

   425   end

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

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

   429   | is_fun _ = false

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

   431   | is_prod _ = false

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

   433 fun is_prod_typed thy config symb =

   434   let

   435     fun symb_type const_name =

   436       Sign.the_const_type thy (full_name thy config const_name)

   437   in

   438     case symb of

   439        Uninterpreted const_name =>

   440          if is_fun (symb_type const_name) then

   441            symb_type const_name |> dom_type |> is_prod

   442          else false

   443      | _ => false

   444    end

   447 (*

   448  Information needed to be carried around:

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

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

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

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

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

   454     terms.

   455 *)

   456 fun interpret_term formula_level config language thy const_map var_types type_map

   457  tptp_t =

   458   case tptp_t of

   459     Term_Func (symb, tptp_ts) =>

   460        let

   461          val thy' = FO_const_types config formula_level type_map tptp_t thy

   462          fun typeof_const const_name = Sign.the_const_type thy'

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

   464        in

   465          case symb of

   466            Interpreted_ExtraLogic Apply =>

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

   468              (mapply

   469                (map (interpret_term false config language thy' const_map

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

   471                (interpret_term formula_level config language thy' const_map

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

   473               thy')

   474            | _ =>

   475               (*apply symb to tptp_ts*)

   476               if is_prod_typed thy' config symb then

   477                 (interpret_symbol config thy' language const_map symb $

   478                   mtimes thy'

   479                   (map (interpret_term false config language thy' const_map

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

   481                   ((interpret_term false config language thy' const_map

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

   483                  thy')

   484               else

   485                 (mapply

   486                   (map (interpret_term false config language thy' const_map

   487                    var_types type_map #> fst) tptp_ts)

   488                   (interpret_symbol config thy' language const_map symb),

   489                  thy')

   490        end

   491   | Term_Var n =>

   492      (if language = THF orelse language = TFF then

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

   494            SOME ty =>

   495              (case ty of

   496                 SOME ty => Free (n, ty)

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

   498              )

   499          | NONE =>

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

   501       else (*variables range over individuals*)

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

   503       thy)

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

   505       (mk_fun @{const_name If}, thy)

   506   | Term_Num (number_kind, num) =>

   507       let

   508         val num_term =

   509           if number_kind = Int_num then

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

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

   512       in (num_term, thy) end

   513   | Term_Distinct_Object str =>

   514       declare_constant config (alphanumerated_name "ds_" str)

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

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

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

   519 fun map_opt f xs =

   520   fold

   521   (fn x => fn y =>

   522     (if Option.isSome x then

   523        SOME (f (Option.valOf x))

   524      else NONE) :: y

   525   ) xs []

   527 fun interpret_formula config language const_map var_types type_map tptp_fmla thy =

   528   case tptp_fmla of

   529       Pred app =>

   530         interpret_term true config language thy const_map

   531          var_types type_map (Term_Func app)

   532     | Fmla (symbol, tptp_formulas) =>

   533        (case symbol of

   534           Interpreted_ExtraLogic Apply =>

   535             let

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

   537                const_map var_types type_map) (tl tptp_formulas) thy)

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

   539                var_types type_map (hd tptp_formulas) thy'

   540             in (mapply args func, thy') end

   541         | Uninterpreted const_name =>

   542             let

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

   544                const_map var_types type_map) tptp_formulas thy)

   545               val thy' = symb_const_types config type_map true const_name

   546                (length tptp_formulas) thy'

   547             in

   548               (if is_prod_typed thy' config symbol then

   549                  mtimes thy' args (interpret_symbol config thy' language

   550                   const_map symbol)

   551                else

   552                 mapply args

   553                  (interpret_symbol config thy' language const_map symbol),

   554               thy')

   555             end

   556         | _ =>

   557             let

   558               val (args, thy') =

   559                 fold_map

   560                  (interpret_formula config language

   561                   const_map var_types type_map)

   562                  tptp_formulas thy

   563             in

   564               (if is_prod_typed thy' config symbol then

   565                  mtimes thy' args (interpret_symbol config thy' language

   566                   const_map symbol)

   567                else

   568                  mapply args

   569                   (interpret_symbol config thy' language const_map symbol),

   570                thy')

   571             end)

   572     | Sequent _ =>

   573         (*FIXME unsupported*)

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

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

   576         let

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

   578           val bound_var_types' : typ option list =

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

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

   581             (interpret_type config thy type_map) bound_var_types

   582           val var_types' =

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

   584             |> List.rev

   585           fun fold_bind f =

   586             fold

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

   588                  case ty of

   589                    NONE =>

   590                      f (n,

   591                         if language = THF then Term.dummyT

   592                         else

   593                           interpret_type config thy type_map

   594                            (Defined_type Type_Ind),

   595                         t)

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

   597               )

   598               var_types'

   599         in case quantifier of

   600           Forall =>

   601             interpret_formula config language const_map (var_types' @ var_types)

   602              type_map tptp_formula thy

   603             |>> fold_bind HOLogic.mk_all

   604         | Exists =>

   605             interpret_formula config language const_map (var_types' @ var_types)

   606              type_map tptp_formula thy

   607             |>> fold_bind HOLogic.mk_exists

   608         | Lambda =>

   609             interpret_formula config language const_map (var_types' @ var_types)

   610              type_map tptp_formula thy

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

   612         | Epsilon =>

   613             let val (t, thy') =

   614               interpret_formula config language const_map var_types type_map

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

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

   617         | Iota =>

   618             let val (t, thy') =

   619               interpret_formula config language const_map var_types type_map

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

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

   622         | Dep_Prod =>

   623             raise MISINTERPRET_FORMULA ("Unsupported", tptp_fmla)

   624         | Dep_Sum =>

   625             raise MISINTERPRET_FORMULA ("Unsupported", tptp_fmla)

   626         end

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

   628         let

   629           val interp = interpret_formula config language const_map var_types type_map

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

   631             interp fmla1 thy

   632             ||>> interp fmla2

   633             ||>> interp fmla3

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

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

   636             thy')

   637         end

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

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

   640     | Atom tptp_atom =>

   641         (case tptp_atom of

   642           TFF_Typed_Atom (symbol, tptp_type_opt) =>

   643             (*FIXME ignoring type info*)

   644             (interpret_symbol config thy language const_map symbol, thy)

   645         | THF_Atom_term tptp_term =>

   646             interpret_term true config language thy const_map var_types

   647              type_map tptp_term

   648         | THF_Atom_conn_term symbol =>

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

   650     | Type_fmla _ =>

   651          raise MISINTERPRET_FORMULA

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

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

   654         interpret_formula config language

   655          const_map var_types type_map tptp_formula thy

   657 (*Extract the type from a typing*)

   658 local

   659   fun extract_type tptp_type =

   660     case tptp_type of

   661         Fmla_type typ => fmlatype_to_type typ

   662       | _ => tptp_type

   663 in

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

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

   666     extract_type tptp_type

   667 end

   668 fun nameof_typing

   669   (THF_typing

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

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

   673 fun interpret_line config inc_list type_map const_map path_prefix line thy =

   674   case line of

   675      Include (quoted_path, inc_list) =>

   676        interpret_file'

   677         config

   678         inc_list

   679         path_prefix

   680         (Path.append

   681           path_prefix

   682           (quoted_path

   683            |> unenclose

   684            |> Path.explode))

   685         type_map

   686         const_map

   687         thy

   688    | Annotated_Formula (pos, lang, label, role, tptp_formula, annotation_opt) =>

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

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

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

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

   693          case role of

   694            Role_Type =>

   695              let

   696                val thy_name = Context.theory_name thy

   697                val (tptp_ty, name) =

   698                  if lang = THF then

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

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

   701                  else

   702                    (typeof_tff_typing tptp_formula,

   703                     nameof_tff_typing tptp_formula)

   704              in

   705                case tptp_ty of

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

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

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

   709                     let

   710                       val (type_map', thy') =

   711                         declare_type

   712                          config

   713                          (Atom_type name, name)

   714                          type_map

   715                          thy

   716                     in ((type_map',

   717                          const_map,

   718                          []),

   719                         thy')

   720                     end

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

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

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

   725                   let

   726                     val ty = interpret_type config thy type_map tptp_ty

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

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

   729                     an undeclared types.*)

   730                     val (t, thy') =

   731                       let

   732                         fun analyse_type thy thf_ty =

   733                            if #cautious config then

   734                             case thf_ty of

   735                                Fn_type (thf_ty1, thf_ty2) =>

   736                                  (analyse_type thy thf_ty1;

   737                                  analyse_type thy thf_ty2)

   738                              | Atom_type ty_name =>

   739                                  if type_exists config thy ty_name then ()

   740                                  else

   741                                   raise MISINTERPRET_TYPE

   742                                    ("Type (in signature of " ^

   743                                       name ^ ") has not been declared",

   744                                      Atom_type ty_name)

   745                              | _ => ()

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

   747                       in

   748                         analyse_type thy tptp_ty;

   749                         declare_constant config name ty thy

   750                       end

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

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

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

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

   755                     theory will be to this name.*)

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

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

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

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

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

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

   762                   end

   763              end

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

   766              let

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

   768                val (t, thy') =

   769                  interpret_formula config lang

   770                   const_map [] type_map tptp_formula thy

   771                  |>> HOLogic.mk_Trueprop

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

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

   774              in

   775               ((type_map, const_map,

   776                 [(label, role,

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

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

   779              end

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

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

   782 and interpret_problem config inc_list path_prefix lines type_map const_map thy =

   783   let

   784     val thy_name = Context.theory_name thy

   785   in

   786     fold (fn line =>

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

   788              let

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

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

   791                  interpret_line config inc_list type_map const_map path_prefix line thy

   792              in

   793                ((type_map',

   794                  const_map',

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

   796                 thy')

   797              end)

   798          lines (*lines of the problem file*)

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

   800   end

   802 and interpret_file' config inc_list path_prefix file_name =

   803   let

   804     val file_name' = Path.expand file_name

   805   in

   806     if Path.is_absolute file_name' then

   807       Path.implode file_name

   808       |> TPTP_Parser.parse_file

   809       |> interpret_problem config inc_list path_prefix

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

   811   end

   813 and interpret_file cautious path_prefix file_name =

   814   let

   815     val config =

   816       {cautious = cautious,

   817        problem_name =

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

   819          file_name))}

   820   in interpret_file' config [] path_prefix file_name end

   822 fun import_file cautious path_prefix file_name type_map const_map thy =

   823   let

   824     val prob_name =

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

   826     val (result, thy') =

   827       interpret_file cautious path_prefix file_name type_map const_map thy

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

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

   831 val _ =

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

   833     (Parse.path >> (fn path =>

   834       Toplevel.theory (fn thy =>

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

   836          (which is how TPTP is organised)*)

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

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

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

   842 fun get_file_list path =

   843   let

   844     fun check_file_entry f rest =

   845       let

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

   847         val f_str = Path.implode f

   848       in

   849         if File.is_dir f then

   850           rest (*filter out directories*)

   851         else if OS.FileSys.isLink f_str then

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

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

   854         else f :: rest

   855       end

   856   in

   857     File.read_dir path

   858     |> map

   859         (Path.explode

   860         #> Path.append path)

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

   862   end

   864 end

author	blanchet
	Wed, 18 Apr 2012 22:39:35 +0200
changeset 48429	55b42f9af99d
parent 48414	60849d8c457d
child 48440	fce9d97a3258
permissions	-rw-r--r--