--- a/src/HOL/TPTP/TPTP_Parser/tptp.lex Thu Aug 07 12:17:41 2014 +0200
+++ b/src/HOL/TPTP/TPTP_Parser/tptp.lex Thu Aug 07 12:17:41 2014 +0200
@@ -86,6 +86,7 @@
upper_word = {upper_alpha}{alpha_numeric}*;
dollar_dollar_word = {ddollar}{lower_word};
dollar_word = {dollar}{lower_word};
+dollar_underscore = {dollar}_;
distinct_object = {double_quote}{do_char}+{double_quote};
@@ -177,6 +178,7 @@
{lower_word} => (col:=yypos-(!eolpos); T.LOWER_WORD(yytext,!linep,!col));
{dollar_word} => (col:=yypos-(!eolpos); T.DOLLAR_WORD(yytext,!linep,!col));
+{dollar_underscore} => (col:=yypos-(!eolpos); T.DOLLAR_WORD(yytext,!linep,!col));
{dollar_dollar_word} => (col:=yypos-(!eolpos); T.DOLLAR_DOLLAR_WORD(yytext,!linep,!col));
"+" => (col:=yypos-(!eolpos); T.PLUS(!linep,!col));
--- a/src/HOL/TPTP/TPTP_Parser/tptp.yacc Thu Aug 07 12:17:41 2014 +0200
+++ b/src/HOL/TPTP/TPTP_Parser/tptp.yacc Thu Aug 07 12:17:41 2014 +0200
@@ -491,7 +491,7 @@
tff_unitary_type : tff_atomic_type (( tff_atomic_type ))
| LPAREN tff_xprod_type RPAREN (( tff_xprod_type ))
-tff_atomic_type : atomic_word (( Atom_type atomic_word ))
+tff_atomic_type : atomic_word (( Atom_type (atomic_word, []) ))
| defined_type (( Defined_type defined_type ))
| atomic_word LPAREN tff_type_arguments RPAREN (( Fmla_type (Fmla (Uninterpreted atomic_word, (map Type_fmla tff_type_arguments))) ))
| variable_ (( Fmla_type (Pred (Interpreted_ExtraLogic Apply, [Term_Var variable_])) ))
@@ -634,6 +634,7 @@
| "$real" => Type_Real
| "$rat" => Type_Rat
| "$int" => Type_Int
+ | "$_" => Type_Dummy
| thing => raise UNRECOGNISED_SYMBOL ("defined_type", thing)
))
@@ -747,6 +748,7 @@
| "$real" => TypeSymbol Type_Real
| "$rat" => TypeSymbol Type_Rat
| "$tType" => TypeSymbol Type_Type
+ | "$_" => TypeSymbol Type_Dummy
| "$true" => Interpreted_Logic True
| "$false" => Interpreted_Logic False
--- a/src/HOL/TPTP/TPTP_Parser/tptp_interpret.ML Thu Aug 07 12:17:41 2014 +0200
+++ b/src/HOL/TPTP/TPTP_Parser/tptp_interpret.ML Thu Aug 07 12:17:41 2014 +0200
@@ -8,11 +8,11 @@
sig
(*Signature extension: typing information for variables and constants*)
type var_types = (string * typ option) list
- type const_map = (string * term) list
+ type const_map = (string * (term * int list)) list
(*Mapping from TPTP types to Isabelle/HOL types. This map works over all
base types. The map must be total wrt TPTP types.*)
- type type_map = (TPTP_Syntax.tptp_type * typ) list
+ type type_map = (string * (string * int)) list
(*A parsed annotated formula is represented as a 5-tuple consisting of
the formula's label, its role, the TPTP formula, its Isabelle/HOL meaning, and
@@ -35,7 +35,7 @@
problem_name : TPTP_Problem_Name.problem_name option}
(*Generates a fresh Isabelle/HOL type for interpreting a TPTP type in a theory.*)
- val declare_type : config -> (TPTP_Syntax.tptp_type * string) -> type_map ->
+ val declare_type : config -> string * (string * int) -> type_map ->
theory -> type_map * theory
(*Map TPTP types to Isabelle/HOL types*)
@@ -132,9 +132,9 @@
(** Signatures and other type abbrevations **)
-type const_map = (string * term) list
+type const_map = (string * (term * int list)) list
type var_types = (string * typ option) list
-type type_map = (TPTP_Syntax.tptp_type * typ) list
+type type_map = (string * (string * int)) list
type tptp_formula_meaning =
string * TPTP_Syntax.role * term * TPTP_Proof.source_info option
type tptp_general_meaning =
@@ -189,17 +189,19 @@
(*Returns updated theory and the name of the final type's name -- i.e. if the
original name is already taken then the function looks for an available
alternative. It also returns an updated type_map if one has been passed to it.*)
-fun declare_type (config : config) (thf_type, type_name) ty_map thy =
+fun declare_type (config : config) (thf_type, (type_name, arity)) ty_map thy =
if type_exists config thy type_name then
- raise MISINTERPRET_TYPE ("Type already exists", Atom_type type_name)
+ raise MISINTERPRET_TYPE ("Type already exists", Atom_type (type_name, []))
else
let
val binding = mk_binding config type_name
val final_fqn = Sign.full_name thy binding
+ val tyargs =
+ List.tabulate (arity, rpair @{sort type} o prefix "'" o string_of_int)
val thy' =
- Typedecl.typedecl_global (mk_binding config type_name, [], NoSyn) thy
+ Typedecl.typedecl_global (mk_binding config type_name, tyargs, NoSyn) thy
|> snd
- val typ_map_entry = (thf_type, (Type (final_fqn, [])))
+ val typ_map_entry = (thf_type, (final_fqn, arity))
val ty_map' = typ_map_entry :: ty_map
in (ty_map', thy') end
@@ -217,42 +219,56 @@
raise MISINTERPRET_TERM
("Const already declared", Term_Func (Uninterpreted const_name, []))
else
- Theory.specify_const
- ((mk_binding config const_name, ty), NoSyn) thy
-
-fun declare_const_ifnot config const_name ty thy =
- if const_exists config thy const_name then
- (Sign.mk_const thy ((Sign.full_name thy (mk_binding config const_name)), []), thy)
- else declare_constant config const_name ty thy
+ Theory.specify_const ((mk_binding config const_name, ty), NoSyn) thy
(** Interpretation functions **)
-(*Types in THF are encoded as formulas. This function translates them to type form.*)
+(*Types in TFF/THF are encoded as formulas. These functions translate them to type form.*)
+
+fun termtype_to_type (Term_Func (TypeSymbol typ, [])) =
+ Defined_type typ
+ | termtype_to_type (Term_Func (Uninterpreted str, tms)) =
+ Atom_type (str, map termtype_to_type tms)
+ | termtype_to_type (Term_Var str) = Var_type str
+
(*FIXME possibly incomplete hack*)
-fun fmlatype_to_type (Atom (THF_Atom_term (Term_Func (TypeSymbol typ, [])))) =
- Defined_type typ
- | fmlatype_to_type (Atom (THF_Atom_term (Term_Func (Uninterpreted str, [])))) =
- Atom_type str
+fun fmlatype_to_type (Atom (THF_Atom_term tm)) = termtype_to_type tm
| fmlatype_to_type (Type_fmla (Fn_type (ty1, ty2))) =
let
val ty1' = case ty1 of
Fn_type _ => fmlatype_to_type (Type_fmla ty1)
| Fmla_type ty1 => fmlatype_to_type ty1
+ | _ => ty1
val ty2' = case ty2 of
Fn_type _ => fmlatype_to_type (Type_fmla ty2)
| Fmla_type ty2 => fmlatype_to_type ty2
+ | _ => ty2
in Fn_type (ty1', ty2') end
+ | fmlatype_to_type (Type_fmla ty) = ty
+ | fmlatype_to_type (Fmla (Uninterpreted str, fmla)) =
+ Atom_type (str, map fmlatype_to_type fmla)
+ | fmlatype_to_type (Quant (Dep_Prod, _, fmla)) = fmlatype_to_type fmla
+ | fmlatype_to_type (Pred (Interpreted_ExtraLogic Apply, [tm])) =
+ termtype_to_type tm
+
+fun tfree_name_of_var_type str = "'" ^ Name.desymbolize (SOME false) str
+fun tfree_of_var_type str = TFree (tfree_name_of_var_type str, @{sort type})
fun interpret_type config thy type_map thf_ty =
let
- fun lookup_type ty_map thf_ty =
- (case AList.lookup (op =) ty_map thf_ty of
+ fun lookup_type ty_map ary str =
+ (case AList.lookup (op =) ty_map str of
NONE =>
- raise MISINTERPRET_TYPE
+ raise MISINTERPRET_SYMBOL
("Could not find the interpretation of this TPTP type in the \
- \mapping to Isabelle/HOL", thf_ty)
- | SOME ty => ty)
+ \mapping to Isabelle/HOL", Uninterpreted str)
+ | SOME (str', ary') =>
+ if ary' = ary then
+ str'
+ else
+ raise MISINTERPRET_SYMBOL ("TPTP type used with wrong arity",
+ Uninterpreted str))
in
case thf_ty of
Prod_type (thf_ty1, thf_ty2) =>
@@ -263,8 +279,10 @@
Type (@{type_name fun},
[interpret_type config thy type_map thf_ty1,
interpret_type config thy type_map thf_ty2])
- | Atom_type _ =>
- lookup_type type_map thf_ty
+ | Atom_type (str, thf_tys) =>
+ Type (lookup_type type_map (length thf_tys) str,
+ map (interpret_type config thy type_map) thf_tys)
+ | Var_type str => tfree_of_var_type str
| Defined_type tptp_base_type =>
(case tptp_base_type of
Type_Ind => @{typ ind}
@@ -272,7 +290,8 @@
| Type_Type => raise MISINTERPRET_TYPE ("No type interpretation", thf_ty)
| Type_Int => @{typ int}
| Type_Rat => @{typ rat}
- | Type_Real => @{typ real})
+ | Type_Real => @{typ real}
+ | Type_Dummy => dummyT)
| Sum_type _ =>
raise MISINTERPRET_TYPE (*FIXME*)
("No type interpretation (sum type)", thf_ty)
@@ -284,19 +303,15 @@
("No type interpretation (subtype)", thf_ty)
end
-fun the_const config thy language const_map_payload str =
- if language = THF then
- (case AList.lookup (op =) const_map_payload str of
- NONE => raise MISINTERPRET_TERM
- ("Could not find the interpretation of this constant in the \
- \mapping to Isabelle/HOL", Term_Func (Uninterpreted str, []))
- | SOME t => t)
- else
- if const_exists config thy str then
- Sign.mk_const thy ((Sign.full_name thy (mk_binding config str)), [])
- else raise MISINTERPRET_TERM
- ("Could not find the interpretation of this constant in the \
- \mapping to Isabelle/HOL", Term_Func (Uninterpreted str, []))
+fun permute_type_args perm Ts = map (nth Ts) perm
+
+fun the_const thy const_map str tyargs =
+ (case AList.lookup (op =) const_map str of
+ SOME (Const (s, _), tyarg_perm) =>
+ Sign.mk_const thy (s, permute_type_args tyarg_perm tyargs)
+ | _ => raise MISINTERPRET_TERM
+ ("Could not find the interpretation of this constant in the \
+ \mapping to Isabelle/HOL", Term_Func (Uninterpreted str, [])))
(*Eta-expands n-ary function.
"str" is the name of an Isabelle/HOL constant*)
@@ -340,18 +355,24 @@
| Is_Int => 1
| Is_Rat => 1
| Distinct => 1
- | Apply=> 2
+ | Apply => 2
-fun interpret_symbol config language const_map symb thy =
+fun type_arity_of_symbol thy config (Uninterpreted n) =
+ let val s = full_name thy config n in
+ length (Sign.const_typargs thy (s, Sign.the_const_type thy s))
+ end
+ | type_arity_of_symbol _ _ _ = 0
+
+fun interpret_symbol config const_map symb tyargs thy =
case symb of
Uninterpreted n =>
(*Constant would have been added to the map at the time of
declaration*)
- the_const config thy language const_map n
+ the_const thy const_map n tyargs
| Interpreted_ExtraLogic interpreted_symbol =>
(*FIXME not interpreting*)
Sign.mk_const thy ((Sign.full_name thy (mk_binding config
- (string_of_interpreted_symbol interpreted_symbol))), [])
+ (string_of_interpreted_symbol interpreted_symbol))), tyargs)
| Interpreted_Logic logic_symbol =>
(case logic_symbol of
Equals => HOLogic.eq_const dummyT
@@ -421,16 +442,14 @@
in
case symb of
Uninterpreted const_name =>
- declare_const_ifnot config const_name
- (mk_fun_type (replicate (length tptp_ts) ind_type) value_type I) thy'
- |> snd
+ perhaps (try (snd o declare_constant config const_name
+ (mk_fun_type (replicate (length tptp_ts) ind_type) value_type I))) thy'
| _ => thy'
end
| Atom_App _ => thy
| Atom_Arity (const_name, n_args) =>
- declare_const_ifnot config const_name
- (mk_fun_type (replicate n_args ind_type) value_type I) thy
- |> snd
+ perhaps (try (snd o declare_constant config const_name
+ (mk_fun_type (replicate n_args ind_type) value_type I))) thy
end
(*FIXME only used until interpretation is implemented*)
@@ -493,24 +512,32 @@
(interpret_term formula_level config language const_map
var_types type_map (hd tptp_ts)))
| _ =>
- (*apply symb to tptp_ts*)
- if is_prod_typed thy' config symb then
- let
- val (t, thy'') =
- mtimes'
- (fold_map (interpret_term false config language const_map
- var_types type_map) (tl tptp_ts) thy')
- (interpret_term false config language const_map
- var_types type_map (hd tptp_ts))
- in (interpret_symbol config language const_map symb thy' $ t, thy'')
- end
- else
- (
- mapply'
- (fold_map (interpret_term false config language const_map
- var_types type_map) tptp_ts thy')
- (`(interpret_symbol config language const_map symb))
- )
+ let
+ val typ_arity = type_arity_of_symbol thy config symb
+ val (tptp_type_args, tptp_term_args) = chop typ_arity tptp_ts
+ val tyargs =
+ map (interpret_type config thy type_map o termtype_to_type)
+ tptp_type_args
+ in
+ (*apply symb to tptp_ts*)
+ if is_prod_typed thy' config symb then
+ let
+ val (t, thy'') =
+ mtimes'
+ (fold_map (interpret_term false config language const_map
+ var_types type_map) (tl tptp_term_args) thy')
+ (interpret_term false config language const_map
+ var_types type_map (hd tptp_term_args))
+ in (interpret_symbol config const_map symb tyargs thy' $ t, thy'')
+ end
+ else
+ (
+ mapply'
+ (fold_map (interpret_term false config language const_map
+ var_types type_map) tptp_term_args thy')
+ (`(interpret_symbol config const_map symb tyargs))
+ )
+ end
end
| Term_Var n =>
(if language = THF orelse language = TFF then
@@ -537,14 +564,12 @@
| Term_Num (number_kind, num) =>
let
(*FIXME hack*)
- val ind_type = interpret_type config thy type_map (Defined_type Type_Ind)
- val prefix = case number_kind of
- Int_num => "intn_"
- | Real_num => "realn_"
- | Rat_num => "ratn_"
- (*FIXME hack -- for Int_num should be
- HOLogic.mk_number @{typ "int"} (the (Int.fromString num))*)
- in declare_const_ifnot config (prefix ^ num) ind_type thy end
+ val tptp_type = case number_kind of
+ Int_num => Type_Int
+ | Real_num => Type_Real
+ | Rat_num => Type_Rat
+ val T = interpret_type config thy type_map (Defined_type tptp_type)
+ in (HOLogic.mk_number T (the (Int.fromString num)), thy) end
| Term_Distinct_Object str =>
declare_constant config ("do_" ^ str)
(interpret_type config thy type_map (Defined_type Type_Ind)) thy
@@ -571,11 +596,9 @@
(Atom_Arity (const_name, length tptp_formulas)) thy'
in
(if is_prod_typed thy' config symbol then
- mtimes thy' args (interpret_symbol config language
- const_map symbol thy')
+ mtimes thy' args (interpret_symbol config const_map symbol [] thy')
else
- mapply args
- (interpret_symbol config language const_map symbol thy'),
+ mapply args (interpret_symbol config const_map symbol [] thy'),
thy')
end
| _ =>
@@ -587,11 +610,9 @@
tptp_formulas thy
in
(if is_prod_typed thy' config symbol then
- mtimes thy' args (interpret_symbol config language
- const_map symbol thy')
+ mtimes thy' args (interpret_symbol config const_map symbol [] thy')
else
- mapply args
- (interpret_symbol config language const_map symbol thy'),
+ mapply args (interpret_symbol config const_map symbol [] thy'),
thy')
end)
| Sequent _ =>
@@ -663,12 +684,12 @@
(case tptp_atom of
TFF_Typed_Atom (symbol, tptp_type_opt) =>
(*FIXME ignoring type info*)
- (interpret_symbol config language const_map symbol thy, thy)
+ (interpret_symbol config const_map symbol [] thy, thy)
| THF_Atom_term tptp_term =>
interpret_term true config language const_map var_types
type_map tptp_term thy
| THF_Atom_conn_term symbol =>
- (interpret_symbol config language const_map symbol thy, thy))
+ (interpret_symbol config const_map symbol [] thy, thy))
| Type_fmla _ =>
raise MISINTERPRET_FORMULA
("Cannot interpret types as formulas", tptp_fmla)
@@ -678,20 +699,31 @@
(*Extract the type from a typing*)
local
+ fun type_vars_of_fmlatype (Quant (Dep_Prod, varlist, fmla)) =
+ map fst varlist @ type_vars_of_fmlatype fmla
+ | type_vars_of_fmlatype _ = []
+
fun extract_type tptp_type =
case tptp_type of
- Fmla_type typ => fmlatype_to_type typ
- | _ => tptp_type
+ Fmla_type fmla => (type_vars_of_fmlatype fmla, fmlatype_to_type fmla)
+ | _ => ([], tptp_type)
in
fun typeof_typing (THF_typing (_, tptp_type)) = extract_type tptp_type
fun typeof_tff_typing (Atom (TFF_Typed_Atom (_, SOME tptp_type))) =
extract_type tptp_type
end
+
fun nameof_typing
(THF_typing
((Atom (THF_Atom_term (Term_Func (Uninterpreted str, [])))), _)) = str
fun nameof_tff_typing (Atom (TFF_Typed_Atom (Uninterpreted str, _))) = str
+fun strip_prod_type (Prod_type (ty1, ty2)) = ty1 :: strip_prod_type ty2
+ | strip_prod_type ty = [ty]
+
+fun dest_fn_type (Fn_type (ty1, ty2)) = (strip_prod_type ty1, ty2)
+ | dest_fn_type ty = ([], ty)
+
fun resolve_include_path path_prefixes path_suffix =
case find_first (fn prefix => File.exists (Path.append prefix path_suffix))
path_prefixes of
@@ -699,6 +731,15 @@
| NONE =>
error ("Cannot find include file " ^ quote (Path.implode path_suffix))
+(* Ideally, to be in sync with TFF1, we should perform full type skolemization here.
+ But the problems originating from HOL systems are restricted to top-level
+ universal quantification for types. *)
+fun remove_leading_type_quantifiers (Quant (Forall, varlist, tptp_fmla)) =
+ (case filter_out (curry (op =) (SOME (Defined_type Type_Type)) o snd) varlist of
+ [] => remove_leading_type_quantifiers tptp_fmla
+ | varlist' => Quant (Forall, varlist', tptp_fmla))
+ | remove_leading_type_quantifiers tptp_fmla = tptp_fmla
+
fun interpret_line config inc_list type_map const_map path_prefixes line thy =
case line of
Include (_, quoted_path, inc_list) =>
@@ -719,7 +760,7 @@
case role of
Role_Type =>
let
- val (tptp_ty, name) =
+ val ((tptp_type_vars, tptp_ty), name) =
if lang = THF then
(typeof_typing tptp_formula (*assuming tptp_formula is a typing*),
nameof_typing tptp_formula (*and that the LHS is a (atom) name*))
@@ -727,22 +768,15 @@
(typeof_tff_typing tptp_formula,
nameof_tff_typing tptp_formula)
in
- case tptp_ty of
- Defined_type Type_Type => (*add new type*)
+ case dest_fn_type tptp_ty of
+ (tptp_binders, Defined_type Type_Type) => (*add new type*)
(*generate an Isabelle/HOL type to interpret this TPTP type,
and add it to both the Isabelle/HOL theory and to the type_map*)
let
val (type_map', thy') =
- declare_type
- config
- (Atom_type name, name)
- type_map
- thy
- in ((type_map',
- const_map,
- []),
- thy')
- end
+ declare_type config
+ (name, (name, length tptp_binders)) type_map thy
+ in ((type_map', const_map, []), thy') end
| _ => (*declaration of constant*)
(*Here we populate the map from constants to the Isabelle/HOL
@@ -752,7 +786,7 @@
(*make sure that the theory contains all the types appearing
in this constant's signature. Exception is thrown if encounter
an undeclared types.*)
- val (t, thy') =
+ val (t as Const (name', _), thy') =
let
fun analyse_type thy thf_ty =
if #cautious config then
@@ -760,13 +794,13 @@
Fn_type (thf_ty1, thf_ty2) =>
(analyse_type thy thf_ty1;
analyse_type thy thf_ty2)
- | Atom_type ty_name =>
+ | Atom_type (ty_name, _) =>
if type_exists config thy ty_name then ()
else
raise MISINTERPRET_TYPE
("Type (in signature of " ^
name ^ ") has not been declared",
- Atom_type ty_name)
+ Atom_type (ty_name, []))
| _ => ()
else () (*skip test if we're not being cautious.*)
in
@@ -778,7 +812,19 @@
use "::". Note that here we use a constant's name rather
than the possibly- new one, since all references in the
theory will be to this name.*)
- val const_map' = ((name, t) :: const_map)
+
+ val tf_tyargs = map tfree_of_var_type tptp_type_vars
+ val isa_tyargs = Sign.const_typargs thy' (name', ty)
+ val _ =
+ if length isa_tyargs < length tf_tyargs then
+ raise MISINTERPRET_SYMBOL
+ ("Cannot handle phantom types for constant",
+ Uninterpreted name)
+ else
+ ()
+ val tyarg_perm =
+ map (fn T => find_index (curry (op =) T) tf_tyargs) isa_tyargs
+ val const_map' = ((name, (t, tyarg_perm)) :: const_map)
in ((type_map,(*type_map unchanged, since a constant's
declaration shouldn't include any new types.*)
const_map',(*typing table of constant was extended*)
@@ -792,7 +838,7 @@
(*gather interpreted term, and the map of types occurring in that term*)
val (t, thy') =
interpret_formula config lang
- const_map [] type_map tptp_formula thy
+ const_map [] type_map (remove_leading_type_quantifiers tptp_formula) thy
|>> HOLogic.mk_Trueprop
(*type_maps grow monotonically, so return the newest value (type_mapped);
there's no need to unify it with the type_map parameter.*)
--- a/src/HOL/TPTP/TPTP_Parser/tptp_lexyacc.ML Thu Aug 07 12:17:41 2014 +0200
+++ b/src/HOL/TPTP/TPTP_Parser/tptp_lexyacc.ML Thu Aug 07 12:17:41 2014 +0200
@@ -174,9 +174,9 @@
\\000"
),
(1,
-"\000\000\000\000\000\000\000\000\000\142\144\000\000\143\000\000\
-\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
-\\142\138\133\000\101\089\088\083\082\081\080\078\077\072\070\057\
+"\000\000\000\000\000\000\000\000\000\143\145\000\000\144\000\000\
+\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
+\\143\139\134\000\101\089\088\083\082\081\080\078\077\072\070\057\
\\048\048\048\048\048\048\048\048\048\048\045\000\039\037\036\033\
\\030\029\029\029\029\029\029\029\029\029\029\029\029\029\029\029\
\\029\029\029\029\029\029\029\029\029\029\029\028\000\027\026\000\
@@ -847,10 +847,10 @@
(101,
"\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
-\\000\000\000\000\131\000\000\000\000\000\000\000\000\000\000\000\
-\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
-\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
-\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
+\\000\000\000\000\132\000\000\000\000\000\000\000\000\000\000\000\
+\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
+\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
+\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\131\
\\000\102\102\128\102\102\124\102\102\118\102\102\108\102\102\102\
\\102\102\102\102\103\102\102\102\102\102\102\000\000\000\000\000\
\\000"
@@ -1053,76 +1053,76 @@
\\102\102\102\102\102\102\102\102\102\102\102\000\000\000\000\000\
\\000"
),
- (131,
-"\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
-\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
-\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
-\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
-\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
-\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
-\\000\132\132\132\132\132\132\132\132\132\132\132\132\132\132\132\
-\\132\132\132\132\132\132\132\132\132\132\132\000\000\000\000\000\
-\\000"
-),
(132,
"\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
-\\132\132\132\132\132\132\132\132\132\132\000\000\000\000\000\000\
-\\000\132\132\132\132\132\132\132\132\132\132\132\132\132\132\132\
-\\132\132\132\132\132\132\132\132\132\132\132\000\000\000\000\132\
-\\000\132\132\132\132\132\132\132\132\132\132\132\132\132\132\132\
-\\132\132\132\132\132\132\132\132\132\132\132\000\000\000\000\000\
+\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
+\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
+\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
+\\000\133\133\133\133\133\133\133\133\133\133\133\133\133\133\133\
+\\133\133\133\133\133\133\133\133\133\133\133\000\000\000\000\000\
\\000"
),
(133,
-"\134\134\134\134\134\134\134\134\134\134\134\134\134\134\134\134\
-\\134\134\134\134\134\134\134\134\134\134\134\134\134\134\134\134\
-\\134\134\000\134\134\134\134\134\134\134\134\134\134\134\134\134\
-\\134\134\134\134\134\134\134\134\134\134\134\134\134\134\134\134\
-\\134\134\134\134\134\134\134\134\134\134\134\134\134\134\134\134\
-\\134\134\134\134\134\134\134\134\134\134\134\134\137\134\134\134\
-\\134\134\134\134\134\134\134\134\134\134\134\134\134\134\134\134\
-\\134\134\134\134\134\134\134\134\134\134\134\134\134\134\134\134\
-\\134"
+"\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
+\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
+\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
+\\133\133\133\133\133\133\133\133\133\133\000\000\000\000\000\000\
+\\000\133\133\133\133\133\133\133\133\133\133\133\133\133\133\133\
+\\133\133\133\133\133\133\133\133\133\133\133\000\000\000\000\133\
+\\000\133\133\133\133\133\133\133\133\133\133\133\133\133\133\133\
+\\133\133\133\133\133\133\133\133\133\133\133\000\000\000\000\000\
+\\000"
),
(134,
-"\134\134\134\134\134\134\134\134\134\134\134\134\134\134\134\134\
-\\134\134\134\134\134\134\134\134\134\134\134\134\134\134\134\134\
-\\134\134\136\134\134\134\134\134\134\134\134\134\134\134\134\134\
-\\134\134\134\134\134\134\134\134\134\134\134\134\134\134\134\134\
-\\134\134\134\134\134\134\134\134\134\134\134\134\134\134\134\134\
-\\134\134\134\134\134\134\134\134\134\134\134\134\135\134\134\134\
-\\134\134\134\134\134\134\134\134\134\134\134\134\134\134\134\134\
-\\134\134\134\134\134\134\134\134\134\134\134\134\134\134\134\134\
-\\134"
+"\135\135\135\135\135\135\135\135\135\135\135\135\135\135\135\135\
+\\135\135\135\135\135\135\135\135\135\135\135\135\135\135\135\135\
+\\135\135\000\135\135\135\135\135\135\135\135\135\135\135\135\135\
+\\135\135\135\135\135\135\135\135\135\135\135\135\135\135\135\135\
+\\135\135\135\135\135\135\135\135\135\135\135\135\135\135\135\135\
+\\135\135\135\135\135\135\135\135\135\135\135\135\138\135\135\135\
+\\135\135\135\135\135\135\135\135\135\135\135\135\135\135\135\135\
+\\135\135\135\135\135\135\135\135\135\135\135\135\135\135\135\135\
+\\135"
),
(135,
+"\135\135\135\135\135\135\135\135\135\135\135\135\135\135\135\135\
+\\135\135\135\135\135\135\135\135\135\135\135\135\135\135\135\135\
+\\135\135\137\135\135\135\135\135\135\135\135\135\135\135\135\135\
+\\135\135\135\135\135\135\135\135\135\135\135\135\135\135\135\135\
+\\135\135\135\135\135\135\135\135\135\135\135\135\135\135\135\135\
+\\135\135\135\135\135\135\135\135\135\135\135\135\136\135\135\135\
+\\135\135\135\135\135\135\135\135\135\135\135\135\135\135\135\135\
+\\135\135\135\135\135\135\135\135\135\135\135\135\135\135\135\135\
+\\135"
+),
+ (136,
"\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
-\\000\000\134\000\000\000\000\000\000\000\000\000\000\000\000\000\
-\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
-\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
-\\000\000\000\000\000\000\000\000\000\000\000\000\134\000\000\000\
+\\000\000\135\000\000\000\000\000\000\000\000\000\000\000\000\000\
+\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
+\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
+\\000\000\000\000\000\000\000\000\000\000\000\000\135\000\000\000\
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
\\000"
),
- (138,
+ (139,
"\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
-\\000\141\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
-\\000\000\000\000\000\000\000\000\000\000\000\000\000\140\139\000\
+\\000\142\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
+\\000\000\000\000\000\000\000\000\000\000\000\000\000\141\140\000\
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
\\000"
),
- (142,
-"\000\000\000\000\000\000\000\000\000\142\000\000\000\000\000\000\
-\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
-\\142\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
+ (143,
+"\000\000\000\000\000\000\000\000\000\143\000\000\000\000\000\000\
+\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
+\\143\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
@@ -1130,8 +1130,8 @@
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
\\000"
),
- (143,
-"\000\000\000\000\000\000\000\000\000\000\144\000\000\000\000\000\
+ (144,
+"\000\000\000\000\000\000\000\000\000\000\145\000\000\000\000\000\
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
@@ -1184,7 +1184,7 @@
{fin = [(N 12)], trans = 0},
{fin = [(N 78)], trans = 33},
{fin = [(N 21)], trans = 0},
-{fin = [(N 303)], trans = 0},
+{fin = [(N 306)], trans = 0},
{fin = [(N 38)], trans = 0},
{fin = [(N 31)], trans = 37},
{fin = [(N 48)], trans = 0},
@@ -1193,10 +1193,10 @@
{fin = [(N 68)], trans = 0},
{fin = [(N 41)], trans = 42},
{fin = [(N 45)], trans = 0},
-{fin = [(N 297)], trans = 0},
+{fin = [(N 300)], trans = 0},
{fin = [(N 27)], trans = 45},
{fin = [(N 36)], trans = 0},
-{fin = [(N 306)], trans = 0},
+{fin = [(N 309)], trans = 0},
{fin = [(N 126)], trans = 48},
{fin = [], trans = 49},
{fin = [(N 104)], trans = 49},
@@ -1225,11 +1225,11 @@
{fin = [(N 55)], trans = 0},
{fin = [(N 123)], trans = 74},
{fin = [(N 58)], trans = 75},
-{fin = [(N 294)], trans = 0},
+{fin = [(N 297)], trans = 0},
{fin = [(N 29)], trans = 0},
-{fin = [(N 288)], trans = 78},
+{fin = [(N 291)], trans = 78},
{fin = [(N 76)], trans = 0},
-{fin = [(N 290)], trans = 0},
+{fin = [(N 293)], trans = 0},
{fin = [(N 82)], trans = 0},
{fin = [(N 52)], trans = 0},
{fin = [], trans = 83},
@@ -1280,19 +1280,20 @@
{fin = [(N 278)], trans = 128},
{fin = [(N 278)], trans = 129},
{fin = [(N 209),(N 278)], trans = 102},
-{fin = [], trans = 131},
-{fin = [(N 286)], trans = 132},
-{fin = [], trans = 133},
+{fin = [(N 281)], trans = 0},
+{fin = [], trans = 132},
+{fin = [(N 289)], trans = 133},
{fin = [], trans = 134},
{fin = [], trans = 135},
+{fin = [], trans = 136},
{fin = [(N 95)], trans = 0},
-{fin = [], trans = 135},
-{fin = [(N 33)], trans = 138},
-{fin = [(N 300)], trans = 0},
+{fin = [], trans = 136},
+{fin = [(N 33)], trans = 139},
+{fin = [(N 303)], trans = 0},
{fin = [(N 64)], trans = 0},
{fin = [(N 18)], trans = 0},
-{fin = [(N 2)], trans = 142},
-{fin = [(N 7)], trans = 143},
+{fin = [(N 2)], trans = 143},
+{fin = [(N 7)], trans = 144},
{fin = [(N 7)], trans = 0}])
end
structure StartStates =
@@ -1369,15 +1370,16 @@
| 27 => (col:=yypos-(!eolpos); T.COLON(!linep,!col))
| 271 => let val yytext=yymktext() in col:=yypos-(!eolpos); T.LOWER_WORD(yytext,!linep,!col) end
| 278 => let val yytext=yymktext() in col:=yypos-(!eolpos); T.DOLLAR_WORD(yytext,!linep,!col) end
-| 286 => let val yytext=yymktext() in col:=yypos-(!eolpos); T.DOLLAR_DOLLAR_WORD(yytext,!linep,!col) end
-| 288 => (col:=yypos-(!eolpos); T.PLUS(!linep,!col))
+| 281 => let val yytext=yymktext() in col:=yypos-(!eolpos); T.DOLLAR_WORD(yytext,!linep,!col) end
+| 289 => let val yytext=yymktext() in col:=yypos-(!eolpos); T.DOLLAR_DOLLAR_WORD(yytext,!linep,!col) end
| 29 => (col:=yypos-(!eolpos); T.COMMA(!linep,!col))
-| 290 => (col:=yypos-(!eolpos); T.TIMES(!linep,!col))
-| 294 => (col:=yypos-(!eolpos); T.GENTZEN_ARROW(!linep,!col))
-| 297 => (col:=yypos-(!eolpos); T.SUBTYPE(!linep,!col))
-| 300 => (col:=yypos-(!eolpos); T.DEP_PROD(!linep,!col))
-| 303 => (col:=yypos-(!eolpos); T.DEP_SUM(!linep,!col))
-| 306 => (col:=yypos-(!eolpos); T.LET_TERM(!linep,!col))
+| 291 => (col:=yypos-(!eolpos); T.PLUS(!linep,!col))
+| 293 => (col:=yypos-(!eolpos); T.TIMES(!linep,!col))
+| 297 => (col:=yypos-(!eolpos); T.GENTZEN_ARROW(!linep,!col))
+| 300 => (col:=yypos-(!eolpos); T.SUBTYPE(!linep,!col))
+| 303 => (col:=yypos-(!eolpos); T.DEP_PROD(!linep,!col))
+| 306 => (col:=yypos-(!eolpos); T.DEP_SUM(!linep,!col))
+| 309 => (col:=yypos-(!eolpos); T.LET_TERM(!linep,!col))
| 31 => (col:=yypos-(!eolpos); T.EQUALS(!linep,!col))
| 33 => (col:=yypos-(!eolpos); T.EXCLAMATION(!linep,!col))
| 36 => (col:=yypos-(!eolpos); T.LET(!linep,!col))
@@ -4851,7 +4853,7 @@
end
| ( 135, ( ( _, ( MlyValue.atomic_word atomic_word, atomic_word1left,
atomic_word1right)) :: rest671)) => let val result =
-MlyValue.tff_atomic_type (( Atom_type atomic_word ))
+MlyValue.tff_atomic_type (( Atom_type (atomic_word, []) ))
in ( LrTable.NT 79, ( result, atomic_word1left, atomic_word1right),
rest671)
end
@@ -5316,6 +5318,7 @@
| "$real" => Type_Real
| "$rat" => Type_Rat
| "$int" => Type_Int
+ | "$_" => Type_Dummy
| thing => raise UNRECOGNISED_SYMBOL ("defined_type", thing)
)
)
@@ -5590,6 +5593,7 @@
| "$real" => TypeSymbol Type_Real
| "$rat" => TypeSymbol Type_Rat
| "$tType" => TypeSymbol Type_Type
+ | "$_" => TypeSymbol Type_Dummy
| "$true" => Interpreted_Logic True
| "$false" => Interpreted_Logic False
--- a/src/HOL/TPTP/TPTP_Parser/tptp_syntax.ML Thu Aug 07 12:17:41 2014 +0200
+++ b/src/HOL/TPTP/TPTP_Parser/tptp_syntax.ML Thu Aug 07 12:17:41 2014 +0200
@@ -66,7 +66,7 @@
Forall | Exists | Epsilon | Iota | Lambda | Dep_Prod | Dep_Sum
and tptp_base_type =
- Type_Ind | Type_Bool | Type_Type | Type_Int | Type_Rat | Type_Real
+ Type_Ind | Type_Bool | Type_Type | Type_Int | Type_Rat | Type_Real | Type_Dummy
and symbol =
Uninterpreted of string
@@ -111,7 +111,8 @@
and tptp_type =
Prod_type of tptp_type * tptp_type
| Fn_type of tptp_type * tptp_type
- | Atom_type of string
+ | Atom_type of string * tptp_type list
+ | Var_type of string
| Defined_type of tptp_base_type
| Sum_type of tptp_type * tptp_type (*only THF*)
| Fmla_type of tptp_formula
@@ -141,8 +142,6 @@
val status_to_string : status_value -> string
- val nameof_tff_atom_type : tptp_type -> string
-
val pos_of_line : tptp_line -> position
(*Returns the list of all files included in a directory and its
@@ -216,7 +215,7 @@
Forall | Exists | Epsilon | Iota | Lambda | Dep_Prod | Dep_Sum
and tptp_base_type =
- Type_Ind | Type_Bool | Type_Type | Type_Int | Type_Rat | Type_Real
+ Type_Ind | Type_Bool | Type_Type | Type_Int | Type_Rat | Type_Real | Type_Dummy
and symbol =
Uninterpreted of string
@@ -261,7 +260,8 @@
and tptp_type =
Prod_type of tptp_type * tptp_type
| Fn_type of tptp_type * tptp_type
- | Atom_type of string
+ | Atom_type of string * tptp_type list
+ | Var_type of string
| Defined_type of tptp_base_type
| Sum_type of tptp_type * tptp_type
| Fmla_type of tptp_formula
@@ -287,9 +287,6 @@
fun debug f x = if Options.default_bool @{system_option ML_exception_trace} then (f x; ()) else ()
-fun nameof_tff_atom_type (Atom_type str) = str
- | nameof_tff_atom_type _ = raise TPTP_SYNTAX "nameof_tff_atom_type called on non-atom type"
-
fun pos_of_line tptp_line =
case tptp_line of
Annotated_Formula (position, _, _, _, _, _) => position
@@ -428,6 +425,7 @@
| string_of_tptp_base_type Type_Int = "$int"
| string_of_tptp_base_type Type_Rat = "$rat"
| string_of_tptp_base_type Type_Real = "$real"
+ | string_of_tptp_base_type Type_Dummy = "$_"
and string_of_interpreted_symbol x =
case x of
@@ -517,7 +515,10 @@
string_of_tptp_type tptp_type1 ^ " * " ^ string_of_tptp_type tptp_type2
| string_of_tptp_type (Fn_type (tptp_type1, tptp_type2)) =
string_of_tptp_type tptp_type1 ^ " > " ^ string_of_tptp_type tptp_type2
- | string_of_tptp_type (Atom_type str) = str
+ | string_of_tptp_type (Atom_type (str, [])) = str
+ | string_of_tptp_type (Atom_type (str, tptp_types)) =
+ str ^ "(" ^ commas (map string_of_tptp_type tptp_types) ^ ")"
+ | string_of_tptp_type (Var_type str) = str
| string_of_tptp_type (Defined_type tptp_base_type) =
string_of_tptp_base_type tptp_base_type
| string_of_tptp_type (Sum_type (tptp_type1, tptp_type2)) = ""
@@ -565,6 +566,7 @@
| latex_of_tptp_base_type Type_Int = "\\\\mathsf{int} "
| latex_of_tptp_base_type Type_Rat = "\\\\mathsf{rat} "
| latex_of_tptp_base_type Type_Real = "\\\\mathsf{real} "
+ | latex_of_tptp_base_type Type_Dummy = "\\\\mathsf{\\\\_} "
and latex_of_interpreted_symbol x =
case x of
@@ -687,7 +689,10 @@
latex_of_tptp_type tptp_type1 ^ " \\\\times " ^ latex_of_tptp_type tptp_type2
| latex_of_tptp_type (Fn_type (tptp_type1, tptp_type2)) =
latex_of_tptp_type tptp_type1 ^ " \\\\to " ^ latex_of_tptp_type tptp_type2
- | latex_of_tptp_type (Atom_type str) = "\\\\mathrm{" ^ str ^ "}"
+ | latex_of_tptp_type (Atom_type (str, [])) = "\\\\mathrm{" ^ str ^ "}"
+ | latex_of_tptp_type (Atom_type (str, tptp_types)) =
+ "\\\\mathrm{" ^ str ^ "}(" ^ commas (map latex_of_tptp_type tptp_types) ^ ")"
+ | latex_of_tptp_type (Var_type str) = "\\\\mathrm{" ^ str ^ "}"
| latex_of_tptp_type (Defined_type tptp_base_type) =
latex_of_tptp_base_type tptp_base_type
| latex_of_tptp_type (Sum_type (tptp_type1, tptp_type2)) = ""