# HG changeset patch # User blanchet # Date 1481737937 -3600 # Node ID c48becd96398bb07d093372340235b2ddda9f5f1 # Parent abd9a9fd030b8e8005f1cccecc51eec39eaa3ff5 support THF1 parsing for 'tptp_...' commands (e.g. 'tptp_isabelle') -- useful for CASC, SystemOnTPTP, ... diff -r abd9a9fd030b -r c48becd96398 src/HOL/TPTP/TPTP_Parser/tptp_interpret.ML --- a/src/HOL/TPTP/TPTP_Parser/tptp_interpret.ML Wed Dec 14 09:19:50 2016 +0100 +++ b/src/HOL/TPTP/TPTP_Parser/tptp_interpret.ML Wed Dec 14 18:52:17 2016 +0100 @@ -215,7 +215,7 @@ fun declare_constant config const_name ty thy = if const_exists config thy const_name then raise MISINTERPRET_TERM - ("Const already declared", Term_Func (Uninterpreted const_name, [])) + ("Const already declared", Term_FuncG (Uninterpreted const_name, [], [])) else Theory.specify_const ((mk_binding config const_name, ty), NoSyn) thy @@ -224,10 +224,10 @@ (*Types in TFF/THF are encoded as formulas. These functions translate them to type form.*) -fun termtype_to_type (Term_Func (TypeSymbol typ, [])) = +fun termtype_to_type (Term_FuncG (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_FuncG (Uninterpreted str, tys, tms)) = + Atom_type (str, tys @ map termtype_to_type tms) | termtype_to_type (Term_Var str) = Var_type str (*FIXME possibly incomplete hack*) @@ -249,6 +249,9 @@ | fmlatype_to_type (Quant (Dep_Prod, _, fmla)) = fmlatype_to_type fmla | fmlatype_to_type (Pred (Interpreted_ExtraLogic Apply, [tm])) = termtype_to_type tm + | fmlatype_to_type (Fmla (Interpreted_ExtraLogic Apply, [tm1, tm2])) = + (case fmlatype_to_type tm1 of + Atom_type (str, tys) => Atom_type (str, tys @ [fmlatype_to_type tm2])) 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}) @@ -323,7 +326,7 @@ else raise MISINTERPRET_TERM ("Could not find the interpretation of this constant in the \ - \mapping to Isabelle/HOL", Term_Func (Uninterpreted str, []))) + \mapping to Isabelle/HOL", Term_FuncG (Uninterpreted str, [], []))) (*Eta-expands n-ary function. "str" is the name of an Isabelle/HOL constant*) @@ -448,7 +451,7 @@ interpret_type config thy type_map (Defined_type Type_Bool) else ind_type in case tptp_atom_value of - Atom_App (Term_Func (symb, tptp_ts)) => + Atom_App (Term_FuncG (symb, tptp_tys, tptp_ts)) => let val thy' = fold (fn t => type_atoms_to_thy config false type_map (Atom_App t)) tptp_ts thy @@ -456,7 +459,8 @@ case symb of Uninterpreted const_name => perhaps (try (snd o declare_constant config const_name - (mk_fun_type (replicate (length tptp_ts) ind_type) value_type I))) thy' + (mk_fun_type (replicate (length tptp_tys + length tptp_ts) ind_type) value_type I))) + thy' | _ => thy' end | Atom_App _ => thy @@ -499,6 +503,25 @@ | _ => false end +fun strip_applies_term (Term_FuncG (Interpreted_ExtraLogic Apply, [], [tm1, tm2])) = + strip_applies_term tm1 ||> (fn tms => tms @ [tm2]) + | strip_applies_term tm = (tm, []) + +fun termify_apply_fmla thy config (Fmla (Interpreted_ExtraLogic Apply, [fmla1, fmla2])) = + (case termify_apply_fmla thy config fmla1 of + SOME (Term_FuncG (symb, tys, tms)) => + let val typ_arity = type_arity_of_symbol thy config symb in + (case (null tms andalso length tys < typ_arity, try fmlatype_to_type fmla2) of + (true, SOME ty) => SOME (Term_FuncG (symb, tys @ [ty], [])) + | _ => + (case termify_apply_fmla thy config fmla2 of + SOME tm2 => SOME (Term_FuncG (symb, tys, tms @ [tm2])) + | NONE => NONE)) + end + | _ => NONE) + | termify_apply_fmla _ _ (Atom (THF_Atom_term tm)) = SOME tm + | termify_apply_fmla _ _ _ = NONE + (* Information needed to be carried around: - constant mapping: maps constant names to Isabelle terms with fully-qualified @@ -508,29 +531,33 @@ after each call of interpret_term since variables' cannot be bound across terms. *) -fun interpret_term formula_level config language const_map var_types type_map - tptp_t thy = +fun interpret_term formula_level config language const_map var_types type_map tptp_t thy = case tptp_t of - Term_Func (symb, tptp_ts) => + Term_FuncG (symb, tptp_tys, tptp_ts) => let val thy' = type_atoms_to_thy config formula_level type_map (Atom_App tptp_t) thy in case symb of Interpreted_ExtraLogic Apply => + (case strip_applies_term tptp_t of + (Term_FuncG (symb, tptp_tys, tptp_ts), extra_tptp_ts) => + interpret_term formula_level config language const_map var_types type_map + (Term_FuncG (symb, tptp_tys, tptp_ts @ extra_tptp_ts)) thy + | _ => (*apply the head of the argument list to the tail*) (mapply' (fold_map (interpret_term false config language const_map var_types type_map) (tl tptp_ts) thy') (interpret_term formula_level config language const_map - var_types type_map (hd tptp_ts))) - | _ => + var_types type_map (hd tptp_ts)))) + | _ => let val typ_arity = type_arity_of_symbol thy' config symb - val (tptp_type_args, tptp_term_args) = chop typ_arity tptp_ts + val (tptp_type_args, tptp_term_args) = chop (typ_arity - length tptp_tys) tptp_ts val tyargs = - map (interpret_type config thy' type_map o termtype_to_type) - tptp_type_args + map (interpret_type config thy' type_map) + (tptp_tys @ map termtype_to_type tptp_type_args) in (*apply symb to tptp_ts*) if is_prod_typed thy' config symb then @@ -604,38 +631,40 @@ and interpret_formula config language const_map var_types type_map tptp_fmla thy = case tptp_fmla of - Pred app => + Pred (symb, ts) => interpret_term true config language const_map - var_types type_map (Term_Func app) thy + var_types type_map (Term_FuncG (symb, [], ts)) thy | Fmla (symbol, tptp_formulas) => (case symbol of Interpreted_ExtraLogic Apply => + (case termify_apply_fmla thy config tptp_fmla of + SOME tptp_t => + interpret_term true config language const_map var_types type_map tptp_t thy + | NONE => mapply' (fold_map (interpret_formula config language const_map var_types type_map) (tl tptp_formulas) thy) (interpret_formula config language const_map - var_types type_map (hd tptp_formulas)) + var_types type_map (hd tptp_formulas))) | Uninterpreted const_name => let val (args, thy') = (fold_map (interpret_formula config language - const_map var_types type_map) tptp_formulas thy) + const_map var_types type_map) tptp_formulas thy) val thy' = type_atoms_to_thy config true type_map - (Atom_Arity (const_name, length tptp_formulas)) thy' + (Atom_Arity (const_name, length tptp_formulas)) thy' in (if is_prod_typed thy' config symbol then mtimes thy' args (interpret_symbol config const_map symbol [] thy') else - mapply args (interpret_symbol config const_map symbol [] thy'), + mapply args (interpret_symbol config const_map symbol [] thy'), thy') end | _ => let val (args, thy') = - fold_map - (interpret_formula config language - const_map var_types type_map) - tptp_formulas thy + fold_map (interpret_formula config language const_map var_types type_map) + tptp_formulas thy in (if is_prod_typed thy' config symbol then mtimes thy' args (interpret_symbol config const_map symbol [] thy') @@ -737,19 +766,20 @@ | _ => ([], 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 + | typeof_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 nameof_typing (THF_typing + ((Atom (THF_Atom_term (Term_FuncG (Uninterpreted str, [], [])))), _)) = str + | nameof_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) +fun dest_fn_type (Fn_type (ty1, ty2)) = + let val (tys2, ty3) = dest_fn_type ty2 in + (strip_prod_type ty1 @ tys2, ty3) + end | dest_fn_type ty = ([], ty) fun resolve_include_path path_prefixes path_suffix = @@ -758,11 +788,16 @@ SOME prefix => Path.append prefix path_suffix | NONE => error ("Cannot find include file " ^ Path.print 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 is_type_type (Fmla_type (Atom (THF_Atom_term (Term_FuncG (TypeSymbol Type_Type, [], []))))) = + true + | is_type_type (Defined_type Type_Type) = true + | is_type_type _ = false; + +(* Ideally, to be in sync with TFF1/THF1, 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 + (case filter_out (fn (_, SOME ty) => is_type_type ty | _ => false) varlist of [] => remove_leading_type_quantifiers tptp_fmla | varlist' => Quant (Forall, varlist', tptp_fmla)) | remove_leading_type_quantifiers tptp_fmla = tptp_fmla @@ -788,12 +823,8 @@ Role_Type => let 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*)) - else - (typeof_tff_typing tptp_formula, - nameof_tff_typing tptp_formula) + (typeof_typing tptp_formula (*assuming tptp_formula is a typing*), + nameof_typing tptp_formula (*and that the LHS is a (atom) name*)) in case dest_fn_type tptp_ty of (tptp_binders, Defined_type Type_Type) => (*add new type*) @@ -865,7 +896,7 @@ (*gather interpreted term, and the map of types occurring in that term*) val (t, thy') = interpret_formula config lang - const_map [] type_map (remove_leading_type_quantifiers 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.*) diff -r abd9a9fd030b -r c48becd96398 src/HOL/TPTP/TPTP_Parser/tptp_syntax.ML --- a/src/HOL/TPTP/TPTP_Parser/tptp_syntax.ML Wed Dec 14 09:19:50 2016 +0100 +++ b/src/HOL/TPTP/TPTP_Parser/tptp_syntax.ML Wed Dec 14 18:52:17 2016 +0100 @@ -81,7 +81,7 @@ | General_List of general_term list and tptp_term = - Term_Func of symbol * tptp_term list + Term_FuncG of symbol * tptp_type list (*special hack for TPTP_Interpret*) * tptp_term list | Term_Var of string | Term_Conditional of tptp_formula * tptp_term * tptp_term | Term_Num of number_kind * string @@ -118,6 +118,8 @@ | Fmla_type of tptp_formula | Subtype of symbol * symbol (*only THF*) + val Term_Func: symbol * tptp_term list -> tptp_term (*for Yacc parser*) + type general_list = general_term list type parent_details = general_list type useful_info = general_term list @@ -230,7 +232,7 @@ | General_List of general_term list and tptp_term = - Term_Func of symbol * tptp_term list + Term_FuncG of symbol * tptp_type list (*special hack for TPTP_Interpret*) * tptp_term list | Term_Var of string | Term_Conditional of tptp_formula * tptp_term * tptp_term | Term_Num of number_kind * string @@ -267,6 +269,8 @@ | Fmla_type of tptp_formula | Subtype of symbol * symbol +fun Term_Func (symb, ts) = Term_FuncG (symb, [], ts) + type general_list = general_term list type parent_details = general_list type useful_info = general_term list @@ -405,9 +409,10 @@ fun string_of_tptp_term x = case x of - Term_Func (symbol, tptp_term_list) => + Term_FuncG (symbol, tptp_type_list, tptp_term_list) => "(" ^ string_of_symbol symbol ^ " " ^ - space_implode " " (map string_of_tptp_term tptp_term_list) ^ ")" + space_implode " " (map string_of_tptp_type tptp_type_list + @ map string_of_tptp_term tptp_term_list) ^ ")" | Term_Var str => str | Term_Conditional (tptp_formula, tptp_term1, tptp_term2) => "" (*FIXME*) | Term_Num (_, str) => str @@ -531,22 +536,23 @@ (*infix symbols, including \subset, \cup, \cap*) fun latex_of_tptp_term x = case x of - Term_Func (Interpreted_Logic Equals, [tptp_t1, tptp_t2]) => + Term_FuncG (Interpreted_Logic Equals, [], [tptp_t1, tptp_t2]) => "(" ^ latex_of_tptp_term tptp_t1 ^ " = " ^ latex_of_tptp_term tptp_t2 ^ ")" - | Term_Func (Interpreted_Logic NEquals, [tptp_t1, tptp_t2]) => + | Term_FuncG (Interpreted_Logic NEquals, [], [tptp_t1, tptp_t2]) => "(" ^ latex_of_tptp_term tptp_t1 ^ " \\\\neq " ^ latex_of_tptp_term tptp_t2 ^ ")" - | Term_Func (Interpreted_Logic Or, [tptp_t1, tptp_t2]) => + | Term_FuncG (Interpreted_Logic Or, [], [tptp_t1, tptp_t2]) => "(" ^ latex_of_tptp_term tptp_t1 ^ " \\\\vee " ^ latex_of_tptp_term tptp_t2 ^ ")" - | Term_Func (Interpreted_Logic And, [tptp_t1, tptp_t2]) => + | Term_FuncG (Interpreted_Logic And, [], [tptp_t1, tptp_t2]) => "(" ^ latex_of_tptp_term tptp_t1 ^ " \\\\wedge " ^ latex_of_tptp_term tptp_t2 ^ ")" - | Term_Func (Interpreted_Logic Iff, [tptp_t1, tptp_t2]) => + | Term_FuncG (Interpreted_Logic Iff, [], [tptp_t1, tptp_t2]) => "(" ^ latex_of_tptp_term tptp_t1 ^ " \\\\longleftrightarrow " ^ latex_of_tptp_term tptp_t2 ^ ")" - | Term_Func (Interpreted_Logic If, [tptp_t1, tptp_t2]) => + | Term_FuncG (Interpreted_Logic If, [], [tptp_t1, tptp_t2]) => "(" ^ latex_of_tptp_term tptp_t1 ^ " \\\\longrightarrow " ^ latex_of_tptp_term tptp_t2 ^ ")" - | Term_Func (symbol, tptp_term_list) => + | Term_FuncG (symbol, tptp_type_list, tptp_term_list) => (*"(" ^*) latex_of_symbol symbol ^ "\\\\, " ^ - space_implode "\\\\, " (map latex_of_tptp_term tptp_term_list) (*^ ")"*) + space_implode "\\\\, " (map latex_of_tptp_type tptp_type_list + @ map latex_of_tptp_term tptp_term_list) (*^ ")"*) | Term_Var str => "\\\\mathrm{" ^ str ^ "}" | Term_Conditional (tptp_formula, tptp_term1, tptp_term2) => "" (*FIXME*) | Term_Num (_, str) => str @@ -647,10 +653,10 @@ latex_of_symbol symbol ^ space_implode "\\\\, " (map latex_of_tptp_term tptp_term_list) - | latex_of_tptp_formula (Fmla (Interpreted_ExtraLogic Apply, [Fmla (Interpreted_ExtraLogic Apply, [Atom (THF_Atom_term (Term_Func (Uninterpreted "union", []))), tptp_f1]), tptp_f2])) = + | latex_of_tptp_formula (Fmla (Interpreted_ExtraLogic Apply, [Fmla (Interpreted_ExtraLogic Apply, [Atom (THF_Atom_term (Term_FuncG (Uninterpreted "union", [], []))), tptp_f1]), tptp_f2])) = "(" ^ latex_of_tptp_formula tptp_f1 ^ " \\\\cup " ^ latex_of_tptp_formula tptp_f2 ^ ")" - | latex_of_tptp_formula (Fmla (Interpreted_ExtraLogic Apply, [Fmla (Interpreted_ExtraLogic Apply, [Atom (THF_Atom_term (Term_Func (Uninterpreted "subset", []))), tptp_f1]), tptp_f2])) = + | latex_of_tptp_formula (Fmla (Interpreted_ExtraLogic Apply, [Fmla (Interpreted_ExtraLogic Apply, [Atom (THF_Atom_term (Term_FuncG (Uninterpreted "subset", [], []))), tptp_f1]), tptp_f2])) = "(" ^ latex_of_tptp_formula tptp_f1 ^ " \\\\subset " ^ latex_of_tptp_formula tptp_f2 ^ ")" | latex_of_tptp_formula (Fmla (Interpreted_Logic Equals, [tptp_f1, tptp_f2])) = diff -r abd9a9fd030b -r c48becd96398 src/HOL/TPTP/TPTP_Parser/tptp_to_dot.ML --- a/src/HOL/TPTP/TPTP_Parser/tptp_to_dot.ML Wed Dec 14 09:19:50 2016 +0100 +++ b/src/HOL/TPTP/TPTP_Parser/tptp_to_dot.ML Wed Dec 14 18:52:17 2016 +0100 @@ -96,7 +96,7 @@ which we interpret to be the last line of the proof.*) fun is_last_line CNF (Pred (Interpreted_Logic False, [])) = true | is_last_line THF (Atom (THF_Atom_term - (Term_Func (Interpreted_Logic False, [])))) = true + (Term_Func (Interpreted_Logic False, [], [])))) = true | is_last_line _ _ = false fun tptp_dot_node with_label reverse_arrows