# HG changeset patch # User blanchet # Date 1434984963 -7200 # Node ID a62655f925c85fd31c14d36aa9043c8c14e2c296 # Parent dcb0b9b42fcb1ee816bbf26d68ad8627bbb9d5b5 reverted some too aggressive TPTP interpreter changes diff -r dcb0b9b42fcb -r a62655f925c8 src/HOL/TPTP/TPTP_Parser/tptp_interpret.ML --- a/src/HOL/TPTP/TPTP_Parser/tptp_interpret.ML Mon Jun 22 16:56:03 2015 +0200 +++ b/src/HOL/TPTP/TPTP_Parser/tptp_interpret.ML Mon Jun 22 16:56:03 2015 +0200 @@ -288,9 +288,19 @@ Type_Ind => @{typ ind} | Type_Bool => HOLogic.boolT | Type_Type => raise MISINTERPRET_TYPE ("No type interpretation", thf_ty) + (*FIXME these types are currently unsupported, so they're treated as + individuals*) + (* | Type_Int => @{typ int} | Type_Rat => @{typ rat} | Type_Real => @{typ real} + *) + | Type_Int => + interpret_type config thy type_map (Defined_type Type_Ind) + | Type_Rat => + interpret_type config thy type_map (Defined_type Type_Ind) + | Type_Real => + interpret_type config thy type_map (Defined_type Type_Ind) | Type_Dummy => dummyT) | Sum_type _ => raise MISINTERPRET_TYPE (*FIXME*) @@ -305,13 +315,17 @@ fun permute_type_args perm Ts = map (nth Ts) perm -fun the_const thy const_map str tyargs = +fun the_const config 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, []))) + | _ => + 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, []))) (*Eta-expands n-ary function. "str" is the name of an Isabelle/HOL constant*) @@ -360,6 +374,7 @@ 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)) + handle TYPE _ => 0 end | type_arity_of_symbol _ _ _ = 0 @@ -368,7 +383,7 @@ Uninterpreted n => (*Constant would have been added to the map at the time of declaration*) - the_const thy const_map n tyargs + the_const config thy const_map n tyargs | Interpreted_ExtraLogic interpreted_symbol => (*FIXME not interpreting*) Sign.mk_const thy ((Sign.full_name thy (mk_binding config @@ -513,10 +528,10 @@ var_types type_map (hd tptp_ts))) | _ => let - val typ_arity = type_arity_of_symbol thy config symb + 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) + map (interpret_type config thy' type_map o termtype_to_type) tptp_type_args in (*apply symb to tptp_ts*) @@ -564,12 +579,27 @@ | Term_Num (number_kind, num) => let (*FIXME hack*) + (* 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 + *) + + 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_" + val const_name = prefix ^ num + in + 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 ind_type thy + end | Term_Distinct_Object str => declare_constant config ("do_" ^ str) (interpret_type config thy type_map (Defined_type Type_Ind)) thy