1.1 --- a/src/HOL/TPTP/TPTP_Parser/tptp.yacc Wed Apr 04 16:29:16 2012 +0100
1.2 +++ b/src/HOL/TPTP/TPTP_Parser/tptp.yacc Wed Apr 04 16:29:17 2012 +0100
1.3 @@ -280,11 +280,11 @@
1.4 thf_logic_formula : thf_binary_formula (( thf_binary_formula ))
1.5 | thf_unitary_formula (( thf_unitary_formula ))
1.6 | thf_type_formula (( THF_typing thf_type_formula ))
1.7 - | thf_subtype (( THF_type thf_subtype ))
1.8 + | thf_subtype (( Type_fmla thf_subtype ))
1.9
1.10 thf_binary_formula : thf_binary_pair (( thf_binary_pair ))
1.11 | thf_binary_tuple (( thf_binary_tuple ))
1.12 - | thf_binary_type (( THF_type thf_binary_type ))
1.13 + | thf_binary_type (( Type_fmla thf_binary_type ))
1.14
1.15 thf_binary_pair : thf_unitary_formula thf_pair_connective thf_unitary_formula ((
1.16 Fmla (thf_pair_connective, [thf_unitary_formula1, thf_unitary_formula2])
1.17 @@ -468,7 +468,7 @@
1.18 | tff_quantified_type (( tff_quantified_type ))
1.19
1.20 tff_quantified_type : DEP_PROD LBRKT tff_variable_list RBRKT COLON tff_monotype ((
1.21 - Fmla_type (Quant (Dep_Prod, tff_variable_list, THF_type tff_monotype))
1.22 + Fmla_type (Quant (Dep_Prod, tff_variable_list, Type_fmla tff_monotype))
1.23 ))
1.24 | LPAREN tff_quantified_type RPAREN (( tff_quantified_type ))
1.25
1.26 @@ -480,7 +480,7 @@
1.27
1.28 tff_atomic_type : atomic_word (( Atom_type atomic_word ))
1.29 | defined_type (( Defined_type defined_type ))
1.30 - | atomic_word LPAREN tff_type_arguments RPAREN (( Fmla_type (Fmla (Uninterpreted atomic_word, (map THF_type tff_type_arguments))) ))
1.31 + | atomic_word LPAREN tff_type_arguments RPAREN (( Fmla_type (Fmla (Uninterpreted atomic_word, (map Type_fmla tff_type_arguments))) ))
1.32 | variable_ (( Fmla_type (Pred (Interpreted_ExtraLogic Apply, [Term_Var variable_])) ))
1.33
1.34 tff_type_arguments : tff_atomic_type (( [tff_atomic_type] ))
2.1 --- a/src/HOL/TPTP/TPTP_Parser/tptp_interpret.ML Wed Apr 04 16:29:16 2012 +0100
2.2 +++ b/src/HOL/TPTP/TPTP_Parser/tptp_interpret.ML Wed Apr 04 16:29:17 2012 +0100
2.3 @@ -13,9 +13,9 @@
2.4 type const_map = (string * term) list
2.5 type var_types = (string * typ option) list
2.6
2.7 - (*mapping from THF types to Isabelle/HOL types. This map works over all
2.8 - base types (i.e. THF functions must be interpreted as Isabelle/HOL functions).
2.9 - The map must be total wrt THF types. Later on there could be a configuration
2.10 + (*mapping from TPTP types to Isabelle/HOL types. This map works over all
2.11 + base types (i.e. TPTP functions must be interpreted as Isabelle/HOL functions).
2.12 + The map must be total wrt TPTP types. Later on there could be a configuration
2.13 option to make a map extensible.*)
2.14 type type_map = (TPTP_Syntax.tptp_type * typ) list
2.15
2.16 @@ -33,7 +33,7 @@
2.17 directive, may include the meaning of an entire TPTP file, is an extended
2.18 Isabelle/HOL theory, an explicit map from constants to their Isabelle/HOL
2.19 counterparts and their types, the meaning of any TPTP formulas encountered
2.20 - while interpreting that statement, and a map from THF to Isabelle/HOL types
2.21 + while interpreting that statement, and a map from TPTP to Isabelle/HOL types
2.22 (these types would have been added to the theory returned in the first position
2.23 of the tuple). The last value is NONE when the function which produced the
2.24 whole tptp_general_meaning value was given a type_map argument -- since
2.25 @@ -53,7 +53,7 @@
2.26 generative_type_interpretation : bool,
2.27 generative_const_interpretation : bool*)}
2.28
2.29 - (*map types form THF to Isabelle/HOL*)
2.30 + (*map types form TPTP to Isabelle/HOL*)
2.31 val interpret_type : config -> theory -> type_map ->
2.32 TPTP_Syntax.tptp_type -> typ
2.33
2.34 @@ -68,11 +68,11 @@
2.35 Arguments:
2.36 cautious = indicates whether additional checks are made to check
2.37 that all used types have been declared.
2.38 - type_map = mapping of THF-types to Isabelle/HOL types. This argument may be
2.39 + type_map = mapping of TPTP-types to Isabelle/HOL types. This argument may be
2.40 given to force a specific mapping: this is usually done for using an
2.41 - imported THF problem in Isar.
2.42 + imported TPTP problem in Isar.
2.43 const_map = as previous, but for constants.
2.44 - path_prefix = path where THF problems etc are located (to help the "include"
2.45 + path_prefix = path where TPTP problems etc are located (to help the "include"
2.46 directive find the files.
2.47 thy = theory where interpreted info will be stored.
2.48 *)
2.49 @@ -93,8 +93,8 @@
2.50 Arguments:
2.51 new_basic_types = indicates whether interpretations of $i and $o
2.52 types are to be added to the type map (unless it is Given).
2.53 - This is "true" if we are running this over a fresh THF problem, but
2.54 - "false" if we are calling this _during_ the interpretation of a THF file
2.55 + This is "true" if we are running this over a fresh TPTP problem, but
2.56 + "false" if we are calling this _during_ the interpretation of a TPTP file
2.57 (i.e. when interpreting an "include" directive.
2.58 config = config
2.59 path_prefix = " "
2.60 @@ -118,13 +118,13 @@
2.61 exception MISINTERPRET_TERM of string * TPTP_Syntax.tptp_term
2.62 exception MISINTERPRET_TYPE of string * TPTP_Syntax.tptp_type
2.63
2.64 - (*Generates a fresh Isabelle/HOL type for interpreting a THF type in a theory.*)
2.65 + (*Generates a fresh Isabelle/HOL type for interpreting a TPTP type in a theory.*)
2.66 val declare_type : config -> (TPTP_Syntax.tptp_type * string) -> type_map ->
2.67 theory -> type_map * theory
2.68
2.69 (*Returns the list of all files included in a directory and its
2.70 subdirectories. This is only used for testing the parser/interpreter against
2.71 - all THF problems.*)
2.72 + all TPTP problems.*)
2.73 val get_file_list : Path.T -> Path.T list
2.74
2.75 type manifest = TPTP_Problem_Name.problem_name * tptp_general_meaning
2.76 @@ -245,13 +245,13 @@
2.77 Defined_type typ
2.78 | fmlatype_to_type (Atom (THF_Atom_term (Term_Func (Uninterpreted str, [])))) =
2.79 Atom_type str
2.80 - | fmlatype_to_type (THF_type (Fn_type (ty1, ty2))) =
2.81 + | fmlatype_to_type (Type_fmla (Fn_type (ty1, ty2))) =
2.82 let
2.83 val ty1' = case ty1 of
2.84 - Fn_type _ => fmlatype_to_type (THF_type ty1)
2.85 + Fn_type _ => fmlatype_to_type (Type_fmla ty1)
2.86 | Fmla_type ty1 => fmlatype_to_type ty1
2.87 val ty2' = case ty2 of
2.88 - Fn_type _ => fmlatype_to_type (THF_type ty2)
2.89 + Fn_type _ => fmlatype_to_type (Type_fmla ty2)
2.90 | Fmla_type ty2 => fmlatype_to_type ty2
2.91 in Fn_type (ty1', ty2') end
2.92
2.93 @@ -327,7 +327,7 @@
2.94 (Const (str, Term.dummyT) $ Bound 0 $ Bound 1)
2.95 |> (Term.absdummy Term.dummyT #> Term.absdummy Term.dummyT)
2.96
2.97 -fun dummy_THF () =
2.98 +fun dummy_term () =
2.99 HOLogic.choice_const Term.dummyT $ Term.absdummy Term.dummyT @{term "True"}
2.100
2.101 fun interpret_symbol config thy language const_map symb =
2.102 @@ -357,7 +357,7 @@
2.103 | Remainder_F | Floor | Ceiling | Truncate | Round | To_Int | To_Rat
2.104 | To_Real | EvalEq | Is_Int | Is_Rat*)
2.105 | Apply => raise MISINTERPRET_SYMBOL ("Malformed term?", symb)
2.106 - | _ => dummy_THF ()
2.107 + | _ => dummy_term ()
2.108 )
2.109 | Interpreted_Logic logic_symbol =>
2.110 (case logic_symbol of
2.111 @@ -523,7 +523,7 @@
2.112 val num_term =
2.113 if number_kind = Int_num then
2.114 HOLogic.mk_number @{typ "int"} (the (Int.fromString num))
2.115 - else dummy_THF () (*FIXME: not yet supporting rationals and reals*)
2.116 + else dummy_term () (*FIXME: not yet supporting rationals and reals*)
2.117 in (num_term, thy) end
2.118 | Term_Distinct_Object str =>
2.119 let
2.120 @@ -674,7 +674,7 @@
2.121 type_map tptp_term
2.122 | THF_Atom_conn_term symbol =>
2.123 (interpret_symbol config thy language const_map symbol, thy))
2.124 - | THF_type _ => (*FIXME unsupported*)
2.125 + | Type_fmla _ => (*FIXME unsupported*)
2.126 raise MISINTERPRET_FORMULA
2.127 ("Cannot interpret types as formulas", tptp_fmla)
2.128 | THF_typing (tptp_formula, _) => (*FIXME ignoring type info*)
2.129 @@ -753,7 +753,7 @@
2.130 in
2.131 case tptp_ty of
2.132 Defined_type Type_Type => (*add new type*)
2.133 - (*generate an Isabelle/HOL type to interpret this THF type,
2.134 + (*generate an Isabelle/HOL type to interpret this TPTP type,
2.135 and add it to both the Isabelle/HOL theory and to the type_map*)
2.136 let
2.137 val (type_map', thy') =
3.1 --- a/src/HOL/TPTP/TPTP_Parser/tptp_lexyacc.ML Wed Apr 04 16:29:16 2012 +0100
3.2 +++ b/src/HOL/TPTP/TPTP_Parser/tptp_lexyacc.ML Wed Apr 04 16:29:17 2012 +0100
3.3 @@ -3880,7 +3880,7 @@
3.4 end
3.5 | ( 22, ( ( _, ( MlyValue.thf_subtype thf_subtype, thf_subtype1left,
3.6 thf_subtype1right)) :: rest671)) => let val result =
3.7 -MlyValue.thf_logic_formula (( THF_type thf_subtype ))
3.8 +MlyValue.thf_logic_formula (( Type_fmla thf_subtype ))
3.9 in ( LrTable.NT 124, ( result, thf_subtype1left, thf_subtype1right),
3.10 rest671)
3.11 end
3.12 @@ -3898,7 +3898,7 @@
3.13 end
3.14 | ( 25, ( ( _, ( MlyValue.thf_binary_type thf_binary_type,
3.15 thf_binary_type1left, thf_binary_type1right)) :: rest671)) => let val
3.16 - result = MlyValue.thf_binary_formula (( THF_type thf_binary_type ))
3.17 + result = MlyValue.thf_binary_formula (( Type_fmla thf_binary_type ))
3.18 in ( LrTable.NT 123, ( result, thf_binary_type1left,
3.19 thf_binary_type1right), rest671)
3.20 end
3.21 @@ -4619,7 +4619,7 @@
3.22 tff_variable_list, _, _)) :: _ :: ( _, ( _, DEP_PROD1left, _)) ::
3.23 rest671)) => let val result = MlyValue.tff_quantified_type (
3.24 (
3.25 - Fmla_type (Quant (Dep_Prod, tff_variable_list, THF_type tff_monotype))
3.26 + Fmla_type (Quant (Dep_Prod, tff_variable_list, Type_fmla tff_monotype))
3.27 )
3.28 )
3.29 in ( LrTable.NT 140, ( result, DEP_PROD1left, tff_monotype1right),
3.30 @@ -4674,7 +4674,7 @@
3.31 MlyValue.tff_type_arguments tff_type_arguments, _, _)) :: _ :: ( _, (
3.32 MlyValue.atomic_word atomic_word, atomic_word1left, _)) :: rest671))
3.33 => let val result = MlyValue.tff_atomic_type (
3.34 -( Fmla_type (Fmla (Uninterpreted atomic_word, (map THF_type tff_type_arguments))) )
3.35 +( Fmla_type (Fmla (Uninterpreted atomic_word, (map Type_fmla tff_type_arguments))) )
3.36 )
3.37 in ( LrTable.NT 79, ( result, atomic_word1left, RPAREN1right),
3.38 rest671)
4.1 --- a/src/HOL/TPTP/TPTP_Parser/tptp_syntax.ML Wed Apr 04 16:29:16 2012 +0100
4.2 +++ b/src/HOL/TPTP/TPTP_Parser/tptp_syntax.ML Wed Apr 04 16:29:17 2012 +0100
4.3 @@ -53,14 +53,13 @@
4.4 UMinus | Sum | Difference | Product | Quotient | Quotient_E |
4.5 Quotient_T | Quotient_F | Remainder_E | Remainder_T | Remainder_F |
4.6 Floor | Ceiling | Truncate | Round | To_Int | To_Rat | To_Real |
4.7 - (*these should be in defined_pred, but that's not being used in TPTP*)
4.8 + (*FIXME these should be in defined_pred, but that's not being used in TPTP*)
4.9 Less | LessEq | Greater | GreaterEq | EvalEq | Is_Int | Is_Rat |
4.10 - Distinct |
4.11 - Apply (*this is just a matter of convenience*)
4.12 + Distinct | Apply
4.13
4.14 and logic_symbol = Equals | NEquals | Or | And | Iff | If | Fi | Xor |
4.15 Nor | Nand | Not | Op_Forall | Op_Exists |
4.16 - (*these should be in defined_pred, but that's not being used in TPTP*)
4.17 + (*FIXME these should be in defined_pred, but that's not being used in TPTP*)
4.18 True | False
4.19
4.20 and quantifier = (*interpreted binders*)
4.21 @@ -102,7 +101,7 @@
4.22 | Conditional of tptp_formula * tptp_formula * tptp_formula
4.23 | Let of tptp_let list * tptp_formula (*FIXME remove list?*)
4.24 | Atom of tptp_atom
4.25 - | THF_type of tptp_type
4.26 + | Type_fmla of tptp_type
4.27 | THF_typing of tptp_formula * tptp_type (*only THF*)
4.28
4.29 and tptp_let =
4.30 @@ -130,7 +129,8 @@
4.31 type position = string * int * int
4.32
4.33 datatype tptp_line =
4.34 - Annotated_Formula of position * language * string * role * tptp_formula * annotation option
4.35 + Annotated_Formula of position * language * string * role *
4.36 + tptp_formula * annotation option
4.37 | Include of string * string list
4.38
4.39 type tptp_problem = tptp_line list
4.40 @@ -198,14 +198,12 @@
4.41 UMinus | Sum | Difference | Product | Quotient | Quotient_E |
4.42 Quotient_T | Quotient_F | Remainder_E | Remainder_T | Remainder_F |
4.43 Floor | Ceiling | Truncate | Round | To_Int | To_Rat | To_Real |
4.44 - (*these should be in defined_pred, but that's not being used in TPTP*)
4.45 Less | LessEq | Greater | GreaterEq | EvalEq | Is_Int | Is_Rat |
4.46 Distinct |
4.47 - Apply (*this is just a matter of convenience*)
4.48 + Apply
4.49
4.50 and logic_symbol = Equals | NEquals | Or | And | Iff | If | Fi | Xor |
4.51 Nor | Nand | Not | Op_Forall | Op_Exists |
4.52 - (*these should be in defined_pred, but that's not being used in TPTP*)
4.53 True | False
4.54
4.55 and quantifier = (*interpreted binders*)
4.56 @@ -247,21 +245,21 @@
4.57 | Conditional of tptp_formula * tptp_formula * tptp_formula
4.58 | Let of tptp_let list * tptp_formula
4.59 | Atom of tptp_atom
4.60 - | THF_type of tptp_type
4.61 + | Type_fmla of tptp_type
4.62 | THF_typing of tptp_formula * tptp_type
4.63
4.64 and tptp_let =
4.65 - Let_fmla of (string * tptp_type option) * tptp_formula (*both TFF and THF*)
4.66 - | Let_term of (string * tptp_type option) * tptp_term (*only TFF*)
4.67 + Let_fmla of (string * tptp_type option) * tptp_formula
4.68 + | Let_term of (string * tptp_type option) * tptp_term
4.69
4.70 and tptp_type =
4.71 Prod_type of tptp_type * tptp_type
4.72 | Fn_type of tptp_type * tptp_type
4.73 | Atom_type of string
4.74 | Defined_type of tptp_base_type
4.75 - | Sum_type of tptp_type * tptp_type (*only THF*)
4.76 - | Fmla_type of tptp_formula (*only THF*)
4.77 - | Subtype of symbol * symbol (*only THF*)
4.78 + | Sum_type of tptp_type * tptp_type
4.79 + | Fmla_type of tptp_formula
4.80 + | Subtype of symbol * symbol
4.81
4.82 type general_list = general_term list
4.83 type parent_details = general_list
4.84 @@ -273,13 +271,6 @@
4.85
4.86 exception DEQUOTE of string
4.87
4.88 -(*
4.89 -datatype defined_functor =
4.90 - ITE_T | UMINUS | SUM | DIFFERENCE | PRODUCT | QUOTIENT | QUOTIENT_E |
4.91 - QUOTIENT_T | QUOTIENT_F | REMAINDER_E | REMAINDER_T | REMAINDER_F |
4.92 - FLOOR | CEILING | TRUNCATE | ROUND | TO_INT | TO_RAT | TO_REAL
4.93 -*)
4.94 -
4.95 type position = string * int * int
4.96
4.97 datatype tptp_line =
4.98 @@ -474,7 +465,7 @@
4.99 | string_of_tptp_formula (Conditional _) = "" (*FIXME*)
4.100 | string_of_tptp_formula (Let _) = "" (*FIXME*)
4.101 | string_of_tptp_formula (Atom tptp_atom) = string_of_tptp_atom tptp_atom
4.102 - | string_of_tptp_formula (THF_type tptp_type) = string_of_tptp_type tptp_type
4.103 + | string_of_tptp_formula (Type_fmla tptp_type) = string_of_tptp_type tptp_type
4.104 | string_of_tptp_formula (THF_typing (tptp_formula, tptp_type)) =
4.105 string_of_tptp_formula tptp_formula ^ " : " ^ string_of_tptp_type tptp_type
4.106