1.1 --- a/src/HOL/TPTP/TPTP_Parser/tptp_interpret.ML Thu Apr 19 07:25:41 2012 +0100
1.2 +++ b/src/HOL/TPTP/TPTP_Parser/tptp_interpret.ML Thu Apr 19 07:25:44 2012 +0100
1.3 @@ -47,8 +47,8 @@
1.4 TPTP_Syntax.tptp_type -> typ
1.5
1.6 (*Map TPTP terms to Isabelle/HOL terms*)
1.7 - val interpret_term : bool -> config -> TPTP_Syntax.language -> theory ->
1.8 - const_map -> var_types -> type_map -> TPTP_Syntax.tptp_term ->
1.9 + val interpret_term : bool -> config -> TPTP_Syntax.language ->
1.10 + const_map -> var_types -> type_map -> TPTP_Syntax.tptp_term -> theory ->
1.11 term * theory
1.12
1.13 val interpret_formula : config -> TPTP_Syntax.language -> const_map ->
1.14 @@ -318,7 +318,7 @@
1.15 fun dummy_term () =
1.16 HOLogic.choice_const Term.dummyT $ Term.absdummy Term.dummyT @{term "True"}
1.17
1.18 -fun interpret_symbol config thy language const_map symb =
1.19 +fun interpret_symbol config language const_map symb thy =
1.20 case symb of
1.21 Uninterpreted n =>
1.22 (*Constant would have been added to the map at the time of
1.23 @@ -378,14 +378,27 @@
1.24
1.25 (*Apply a function to a list of arguments*)
1.26 val mapply = fold (fn x => fn y => y $ x)
1.27 +
1.28 +fun mapply' (args, thy) f =
1.29 + let
1.30 + val (f', thy') = f thy
1.31 + in (mapply args f', thy') end
1.32 +
1.33 (*As above, but for products*)
1.34 fun mtimes thy =
1.35 fold (fn x => fn y =>
1.36 Sign.mk_const thy
1.37 ("Product_Type.Pair",[Term.dummyT, Term.dummyT]) $ y $ x)
1.38
1.39 -(*Adds constants to signature in FOL. "formula_level" means that the constants
1.40 -are to be interpreted as predicates, otherwise as functions over individuals.*)
1.41 +fun mtimes' (args, thy) f =
1.42 + let
1.43 + val (f', thy') = f thy
1.44 + in (mtimes thy' args f', thy') end
1.45 +
1.46 +
1.47 +(*Adds constants to signature in FOL (since explicit type declaration isn't
1.48 +expected). "formula_level" means that the constants are to be interpreted as
1.49 +predicates, otherwise as functions over individuals.*)
1.50 fun FO_const_types config formula_level type_map tptp_t thy =
1.51 let
1.52 val ind_type = interpret_type config thy type_map (Defined_type Type_Ind)
1.53 @@ -457,8 +470,8 @@
1.54 after each call of interpret_term since variables' cannot be bound across
1.55 terms.
1.56 *)
1.57 -fun interpret_term formula_level config language thy const_map var_types type_map
1.58 - tptp_t =
1.59 +fun interpret_term formula_level config language const_map var_types type_map
1.60 + tptp_t thy =
1.61 case tptp_t of
1.62 Term_Func (symb, tptp_ts) =>
1.63 let
1.64 @@ -469,28 +482,30 @@
1.65 case symb of
1.66 Interpreted_ExtraLogic Apply =>
1.67 (*apply the head of the argument list to the tail*)
1.68 - (mapply
1.69 - (map (interpret_term false config language thy' const_map
1.70 - var_types type_map #> fst) (tl tptp_ts))
1.71 - (interpret_term formula_level config language thy' const_map
1.72 - var_types type_map (hd tptp_ts) |> fst),
1.73 - thy')
1.74 + (mapply'
1.75 + (fold_map (interpret_term false config language const_map
1.76 + var_types type_map) (tl tptp_ts) thy')
1.77 + (interpret_term formula_level config language const_map
1.78 + var_types type_map (hd tptp_ts)))
1.79 | _ =>
1.80 (*apply symb to tptp_ts*)
1.81 if is_prod_typed thy' config symb then
1.82 - (interpret_symbol config thy' language const_map symb $
1.83 - mtimes thy'
1.84 - (map (interpret_term false config language thy' const_map
1.85 - var_types type_map #> fst) (tl tptp_ts))
1.86 - ((interpret_term false config language thy' const_map
1.87 - var_types type_map #> fst) (hd tptp_ts)),
1.88 - thy')
1.89 + let
1.90 + val (t, thy'') =
1.91 + mtimes'
1.92 + (fold_map (interpret_term false config language const_map
1.93 + var_types type_map) (tl tptp_ts) thy')
1.94 + (interpret_term false config language const_map
1.95 + var_types type_map (hd tptp_ts))
1.96 + in (interpret_symbol config language const_map symb thy' $ t, thy'')
1.97 + end
1.98 else
1.99 - (mapply
1.100 - (map (interpret_term false config language thy' const_map
1.101 - var_types type_map #> fst) tptp_ts)
1.102 - (interpret_symbol config thy' language const_map symb),
1.103 - thy')
1.104 + (
1.105 + mapply'
1.106 + (fold_map (interpret_term false config language const_map
1.107 + var_types type_map) tptp_ts thy')
1.108 + (`(interpret_symbol config language const_map symb))
1.109 + )
1.110 end
1.111 | Term_Var n =>
1.112 (if language = THF orelse language = TFF then
1.113 @@ -515,7 +530,7 @@
1.114 else dummy_term () (*FIXME: not yet supporting rationals and reals*)
1.115 in (num_term, thy) end
1.116 | Term_Distinct_Object str =>
1.117 - declare_constant config (alphanumerated_name "ds_" str)
1.118 + declare_constant config ("do_" ^ str)
1.119 (interpret_type config thy type_map (Defined_type Type_Ind)) thy
1.120
1.121 (*Given a list of "'a option", then applies a function to each element if that
1.122 @@ -531,17 +546,16 @@
1.123 fun interpret_formula config language const_map var_types type_map tptp_fmla thy =
1.124 case tptp_fmla of
1.125 Pred app =>
1.126 - interpret_term true config language thy const_map
1.127 - var_types type_map (Term_Func app)
1.128 + interpret_term true config language const_map
1.129 + var_types type_map (Term_Func app) thy
1.130 | Fmla (symbol, tptp_formulas) =>
1.131 (case symbol of
1.132 Interpreted_ExtraLogic Apply =>
1.133 - let
1.134 - val (args, thy') = (fold_map (interpret_formula config language
1.135 - const_map var_types type_map) (tl tptp_formulas) thy)
1.136 - val (func, thy') = interpret_formula config language const_map
1.137 - var_types type_map (hd tptp_formulas) thy'
1.138 - in (mapply args func, thy') end
1.139 + mapply'
1.140 + (fold_map (interpret_formula config language const_map
1.141 + var_types type_map) (tl tptp_formulas) thy)
1.142 + (interpret_formula config language const_map
1.143 + var_types type_map (hd tptp_formulas))
1.144 | Uninterpreted const_name =>
1.145 let
1.146 val (args, thy') = (fold_map (interpret_formula config language
1.147 @@ -550,11 +564,11 @@
1.148 (length tptp_formulas) thy'
1.149 in
1.150 (if is_prod_typed thy' config symbol then
1.151 - mtimes thy' args (interpret_symbol config thy' language
1.152 - const_map symbol)
1.153 + mtimes thy' args (interpret_symbol config language
1.154 + const_map symbol thy')
1.155 else
1.156 mapply args
1.157 - (interpret_symbol config thy' language const_map symbol),
1.158 + (interpret_symbol config language const_map symbol thy'),
1.159 thy')
1.160 end
1.161 | _ =>
1.162 @@ -566,11 +580,11 @@
1.163 tptp_formulas thy
1.164 in
1.165 (if is_prod_typed thy' config symbol then
1.166 - mtimes thy' args (interpret_symbol config thy' language
1.167 - const_map symbol)
1.168 + mtimes thy' args (interpret_symbol config language
1.169 + const_map symbol thy')
1.170 else
1.171 mapply args
1.172 - (interpret_symbol config thy' language const_map symbol),
1.173 + (interpret_symbol config language const_map symbol thy'),
1.174 thy')
1.175 end)
1.176 | Sequent _ =>
1.177 @@ -645,12 +659,12 @@
1.178 (case tptp_atom of
1.179 TFF_Typed_Atom (symbol, tptp_type_opt) =>
1.180 (*FIXME ignoring type info*)
1.181 - (interpret_symbol config thy language const_map symbol, thy)
1.182 + (interpret_symbol config language const_map symbol thy, thy)
1.183 | THF_Atom_term tptp_term =>
1.184 - interpret_term true config language thy const_map var_types
1.185 - type_map tptp_term
1.186 + interpret_term true config language const_map var_types
1.187 + type_map tptp_term thy
1.188 | THF_Atom_conn_term symbol =>
1.189 - (interpret_symbol config thy language const_map symbol, thy))
1.190 + (interpret_symbol config language const_map symbol thy, thy))
1.191 | Type_fmla _ =>
1.192 raise MISINTERPRET_FORMULA
1.193 ("Cannot interpret types as formulas", tptp_fmla)