fixed type interpretation;
authorsultana
Wed Apr 18 17:33:11 2012 +0100 (2012-04-18)
changeset 4754860849d8c457d
parent 47547 1a5dc8377b5c
child 47549 d19ce7f40d78
fixed type interpretation;
output now excludes parsed term;
tuned;
src/HOL/TPTP/TPTP_Interpret_Test.thy
src/HOL/TPTP/TPTP_Parser/tptp_interpret.ML
src/HOL/TPTP/TPTP_Parser_Example.thy
     1.1 --- a/src/HOL/TPTP/TPTP_Interpret_Test.thy	Wed Apr 18 17:33:11 2012 +0100
     1.2 +++ b/src/HOL/TPTP/TPTP_Interpret_Test.thy	Wed Apr 18 17:33:11 2012 +0100
     1.3 @@ -27,10 +27,7 @@
     1.4  
     1.5  text "... and display nicely."
     1.6  ML {*
     1.7 -  List.app (Pretty.writeln o (Syntax.pretty_term @{context}) o #4) fmlas;
     1.8 -
     1.9 -  (*Don't use TPTP_Syntax.string_of_tptp_formula, it's just for testing*)
    1.10 -  List.app (writeln o TPTP_Syntax.string_of_tptp_formula o #3) fmlas
    1.11 +  List.app (Pretty.writeln o (Syntax.pretty_term @{context}) o #3) fmlas;
    1.12  *}
    1.13  
    1.14  subsection "Multiple tests"
     2.1 --- a/src/HOL/TPTP/TPTP_Parser/tptp_interpret.ML	Wed Apr 18 17:33:11 2012 +0100
     2.2 +++ b/src/HOL/TPTP/TPTP_Parser/tptp_interpret.ML	Wed Apr 18 17:33:11 2012 +0100
     2.3 @@ -22,7 +22,7 @@
     2.4    the formula's label, its role, the TPTP formula, its Isabelle/HOL meaning, and
     2.5    inference info*)
     2.6    type tptp_formula_meaning =
     2.7 -    string * TPTP_Syntax.role * TPTP_Syntax.tptp_formula * term * inference_info
     2.8 +    string * TPTP_Syntax.role * term * inference_info
     2.9  
    2.10    (*In general, the meaning of a TPTP statement (which, through the Include
    2.11    directive, may include the meaning of an entire TPTP file, is a map from
    2.12 @@ -36,15 +36,7 @@
    2.13      problem_name = if given then it is used to qualify types & constants*)
    2.14    type config =
    2.15      {cautious : bool,
    2.16 -     problem_name : TPTP_Problem_Name.problem_name option
    2.17 -     (*FIXME future extensibility
    2.18 -     init_type_map : type_map with_origin,
    2.19 -     init_const_map : type_map with_origin,
    2.20 -     dont_build_maps : bool,
    2.21 -     extend_given_type_map : bool,
    2.22 -     extend_given_const_map : bool,
    2.23 -     generative_type_interpretation : bool,
    2.24 -     generative_const_interpretation : bool*)}
    2.25 +     problem_name : TPTP_Problem_Name.problem_name option}
    2.26  
    2.27    (*Generates a fresh Isabelle/HOL type for interpreting a TPTP type in a theory.*)
    2.28    val declare_type : config -> (TPTP_Syntax.tptp_type * string) -> type_map ->
    2.29 @@ -149,7 +141,7 @@
    2.30  type type_map = (TPTP_Syntax.tptp_type * typ) list
    2.31  type inference_info = (string * string list) option
    2.32  type tptp_formula_meaning =
    2.33 -  string * TPTP_Syntax.role * TPTP_Syntax.tptp_formula * term * inference_info
    2.34 +  string * TPTP_Syntax.role * term * inference_info
    2.35  type tptp_general_meaning =
    2.36    (type_map * const_map * tptp_formula_meaning list)
    2.37  
    2.38 @@ -165,9 +157,6 @@
    2.39  
    2.40  (** Adding types to a signature **)
    2.41  
    2.42 -fun type_exists thy ty_name =
    2.43 -  Sign.declared_tyname thy (Sign.full_bname thy ty_name)
    2.44 -
    2.45  (*transform quoted names into acceptable ASCII strings*)
    2.46  fun alphanumerate c =
    2.47    let
    2.48 @@ -197,11 +186,14 @@
    2.49           pre_binding
    2.50    end
    2.51  
    2.52 +fun type_exists config thy ty_name =
    2.53 +  Sign.declared_tyname thy (Sign.full_name thy (mk_binding config ty_name))
    2.54 +
    2.55  (*Returns updated theory and the name of the final type's name -- i.e. if the
    2.56  original name is already taken then the function looks for an available
    2.57  alternative. It also returns an updated type_map if one has been passed to it.*)
    2.58  fun declare_type (config : config) (thf_type, type_name) ty_map thy =
    2.59 -  if type_exists thy type_name then
    2.60 +  if type_exists config thy type_name then
    2.61      raise MISINTERPRET_TYPE ("Type already exists", Atom_type type_name)
    2.62    else
    2.63      let
    2.64 @@ -260,7 +252,7 @@
    2.65                 \mapping to Isabelle/HOL", thf_ty)
    2.66          | SOME ty => ty)
    2.67    in
    2.68 -    case thf_ty of (*FIXME make tail*)
    2.69 +    case thf_ty of
    2.70         Prod_type (thf_ty1, thf_ty2) =>
    2.71           Type ("Product_Type.prod",
    2.72            [interpret_type config thy type_map thf_ty1,
    2.73 @@ -744,7 +736,7 @@
    2.74                                   (analyse_type thy thf_ty1;
    2.75                                   analyse_type thy thf_ty2)
    2.76                               | Atom_type ty_name =>
    2.77 -                                 if type_exists thy ty_name then ()
    2.78 +                                 if type_exists config thy ty_name then ()
    2.79                                   else
    2.80                                    raise MISINTERPRET_TYPE
    2.81                                     ("Type (in signature of " ^
    2.82 @@ -781,13 +773,12 @@
    2.83                 there's no need to unify it with the type_map parameter.*)
    2.84               in
    2.85                ((type_map, const_map,
    2.86 -                [(label, role, tptp_formula,
    2.87 +                [(label, role,
    2.88                    Syntax.check_term (Proof_Context.init_global thy') t,
    2.89                    TPTP_Proof.extract_inference_info annotation_opt)]), thy')
    2.90               end
    2.91         else (*do nothing if we're not to includ this AF*)
    2.92           ((type_map, const_map, []), thy)
    2.93 -
    2.94  and interpret_problem config inc_list path_prefix lines type_map const_map thy =
    2.95    let
    2.96      val thy_name = Context.theory_name thy
     3.1 --- a/src/HOL/TPTP/TPTP_Parser_Example.thy	Wed Apr 18 17:33:11 2012 +0100
     3.2 +++ b/src/HOL/TPTP/TPTP_Parser_Example.thy	Wed Apr 18 17:33:11 2012 +0100
     3.3 @@ -9,8 +9,7 @@
     3.4  uses "~~/src/HOL/ex/sledgehammer_tactics.ML"
     3.5  begin
     3.6  
     3.7 -import_tptp "$TPTP_PROBLEMS_PATH/ALG/ALG001^5.p" (*FIXME multiple imports*)
     3.8 -(*import_tptp "$TPTP_PROBLEMS_PATH/NUM/NUM021^1.p"*)
     3.9 +import_tptp "$TPTP_PROBLEMS_PATH/ALG/ALG001^5.p"
    3.10  
    3.11  ML {*
    3.12  val an_fmlas =
    3.13 @@ -22,7 +21,7 @@
    3.14  
    3.15  (*Display nicely.*)
    3.16  ML {*
    3.17 -List.app (fn (n, role, _, fmla, _) =>
    3.18 +List.app (fn (n, role, fmla, _) =>
    3.19    Pretty.writeln
    3.20      (Pretty.block [Pretty.str ("\"" ^ n ^ "\"" ^ "(" ^
    3.21        TPTP_Syntax.role_to_string role  ^ "): "), Syntax.pretty_term @{context} fmla])
    3.22 @@ -35,9 +34,9 @@
    3.23  fun extract_terms roles : TPTP_Interpret.tptp_formula_meaning list ->
    3.24   (string * term) list =
    3.25     let
    3.26 -     fun role_predicate (_, role, _, _, _) =
    3.27 +     fun role_predicate (_, role, _, _) =
    3.28         fold (fn r1 => fn b => role = r1 orelse b) roles false
    3.29 -   in filter role_predicate #> map (fn (n, _, _, t, _) => (n, t)) end
    3.30 +   in filter role_predicate #> map (fn (n, _, t, _) => (n, t)) end
    3.31  *}
    3.32  
    3.33  ML {*