# HG changeset patch # User blanchet # Date 1280136085 -7200 # Node ID 7911e78a7122325f6b30fdedeca2ac2f9f27e160 # Parent 3093ab32f1e79eefeea1b2d5a0d085190bdf3e15 renamed internal function diff -r 3093ab32f1e7 -r 7911e78a7122 src/HOL/Tools/Sledgehammer/metis_clauses.ML --- a/src/HOL/Tools/Sledgehammer/metis_clauses.ML Mon Jul 26 11:21:11 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/metis_clauses.ML Mon Jul 26 11:21:25 2010 +0200 @@ -45,7 +45,7 @@ val invert_const: string -> string val ascii_of: string -> string val undo_ascii_of: string -> string - val strip_prefix: string -> string -> string option + val strip_prefix_and_undo_ascii: string -> string -> string option val make_schematic_var : string * int -> string val make_fixed_var : string -> string val make_schematic_type_var : string * int -> string @@ -163,7 +163,7 @@ (* If string s has the prefix s1, return the result of deleting it, un-ASCII'd. *) -fun strip_prefix s1 s = +fun strip_prefix_and_undo_ascii s1 s = if String.isPrefix s1 s then SOME (undo_ascii_of (String.extract (s, size s1, NONE))) else diff -r 3093ab32f1e7 -r 7911e78a7122 src/HOL/Tools/Sledgehammer/metis_tactics.ML --- a/src/HOL/Tools/Sledgehammer/metis_tactics.ML Mon Jul 26 11:21:11 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/metis_tactics.ML Mon Jul 26 11:21:25 2010 +0200 @@ -223,15 +223,15 @@ fun make_tvar s = TVar (("'" ^ s, 0), HOLogic.typeS) fun hol_type_from_metis_term _ (Metis.Term.Var v) = - (case strip_prefix tvar_prefix v of + (case strip_prefix_and_undo_ascii tvar_prefix v of SOME w => make_tvar w | NONE => make_tvar v) | hol_type_from_metis_term ctxt (Metis.Term.Fn(x, tys)) = - (case strip_prefix type_const_prefix x of + (case strip_prefix_and_undo_ascii type_const_prefix x of SOME tc => Term.Type (invert_const tc, map (hol_type_from_metis_term ctxt) tys) | NONE => - case strip_prefix tfree_prefix x of + case strip_prefix_and_undo_ascii tfree_prefix x of SOME tf => mk_tfree ctxt tf | NONE => raise Fail ("hol_type_from_metis_term: " ^ x)); @@ -241,10 +241,10 @@ val _ = trace_msg (fn () => "hol_term_from_metis_PT: " ^ Metis.Term.toString fol_tm) fun tm_to_tt (Metis.Term.Var v) = - (case strip_prefix tvar_prefix v of + (case strip_prefix_and_undo_ascii tvar_prefix v of SOME w => Type (make_tvar w) | NONE => - case strip_prefix schematic_var_prefix v of + case strip_prefix_and_undo_ascii schematic_var_prefix v of SOME w => Term (mk_var (w, HOLogic.typeT)) | NONE => Term (mk_var (v, HOLogic.typeT)) ) (*Var from Metis with a name like _nnn; possibly a type variable*) @@ -261,7 +261,7 @@ and applic_to_tt ("=",ts) = Term (list_comb(Const (@{const_name "op ="}, HOLogic.typeT), terms_of (map tm_to_tt ts))) | applic_to_tt (a,ts) = - case strip_prefix const_prefix a of + case strip_prefix_and_undo_ascii const_prefix a of SOME b => let val c = invert_const b val ntypes = num_type_args thy c @@ -279,14 +279,14 @@ cat_lines (map (Syntax.string_of_term ctxt) (terms_of tts))) end | NONE => (*Not a constant. Is it a type constructor?*) - case strip_prefix type_const_prefix a of + case strip_prefix_and_undo_ascii type_const_prefix a of SOME b => Type (Term.Type (invert_const b, types_of (map tm_to_tt ts))) | NONE => (*Maybe a TFree. Should then check that ts=[].*) - case strip_prefix tfree_prefix a of + case strip_prefix_and_undo_ascii tfree_prefix a of SOME b => Type (mk_tfree ctxt b) | NONE => (*a fixed variable? They are Skolem functions.*) - case strip_prefix fixed_var_prefix a of + case strip_prefix_and_undo_ascii fixed_var_prefix a of SOME b => let val opr = Term.Free(b, HOLogic.typeT) in apply_list opr (length ts) (map tm_to_tt ts) end @@ -302,16 +302,16 @@ let val _ = trace_msg (fn () => "hol_term_from_metis_FT: " ^ Metis.Term.toString fol_tm) fun cvt (Metis.Term.Fn ("ti", [Metis.Term.Var v, _])) = - (case strip_prefix schematic_var_prefix v of + (case strip_prefix_and_undo_ascii schematic_var_prefix v of SOME w => mk_var(w, dummyT) | NONE => mk_var(v, dummyT)) | cvt (Metis.Term.Fn ("ti", [Metis.Term.Fn ("=",[]), _])) = Const ("op =", HOLogic.typeT) | cvt (Metis.Term.Fn ("ti", [Metis.Term.Fn (x,[]), ty])) = - (case strip_prefix const_prefix x of + (case strip_prefix_and_undo_ascii const_prefix x of SOME c => Const (invert_const c, dummyT) | NONE => (*Not a constant. Is it a fixed variable??*) - case strip_prefix fixed_var_prefix x of + case strip_prefix_and_undo_ascii fixed_var_prefix x of SOME v => Free (v, hol_type_from_metis_term ctxt ty) | NONE => raise Fail ("hol_term_from_metis_FT bad constant: " ^ x)) | cvt (Metis.Term.Fn ("ti", [Metis.Term.Fn (".",[tm1,tm2]), _])) = @@ -322,10 +322,10 @@ | cvt (Metis.Term.Fn ("=", [tm1,tm2])) = list_comb(Const (@{const_name "op ="}, HOLogic.typeT), map cvt [tm1,tm2]) | cvt (t as Metis.Term.Fn (x, [])) = - (case strip_prefix const_prefix x of + (case strip_prefix_and_undo_ascii const_prefix x of SOME c => Const (invert_const c, dummyT) | NONE => (*Not a constant. Is it a fixed variable??*) - case strip_prefix fixed_var_prefix x of + case strip_prefix_and_undo_ascii fixed_var_prefix x of SOME v => Free (v, dummyT) | NONE => (trace_msg (fn () => "hol_term_from_metis_FT bad const: " ^ x); hol_term_from_metis_PT ctxt t)) @@ -405,9 +405,9 @@ " in " ^ Display.string_of_thm ctxt i_th); NONE) fun remove_typeinst (a, t) = - case strip_prefix schematic_var_prefix a of + case strip_prefix_and_undo_ascii schematic_var_prefix a of SOME b => SOME (b, t) - | NONE => case strip_prefix tvar_prefix a of + | NONE => case strip_prefix_and_undo_ascii tvar_prefix a of SOME _ => NONE (*type instantiations are forbidden!*) | NONE => SOME (a,t) (*internal Metis var?*) val _ = trace_msg (fn () => " isa th: " ^ Display.string_of_thm ctxt i_th) diff -r 3093ab32f1e7 -r 7911e78a7122 src/HOL/Tools/Sledgehammer/sledgehammer_tptp_format.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_tptp_format.ML Mon Jul 26 11:21:11 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_tptp_format.ML Mon Jul 26 11:21:25 2010 +0200 @@ -11,7 +11,16 @@ type arity_clause = Metis_Clauses.arity_clause type fol_clause = Metis_Clauses.fol_clause + datatype 'a fo_term = ATerm of 'a * 'a fo_term list + datatype quantifier = AForall | AExists + datatype connective = ANot | AAnd | AOr | AImplies | AIf | AIff | ANotIff + datatype 'a formula = + AQuant of quantifier * 'a list * 'a formula | + AConn of connective * 'a formula list | + APred of 'a fo_term + val axiom_prefix : string + val conjecture_prefix : string val write_tptp_file : theory -> bool -> bool -> bool -> Path.T -> fol_clause list * fol_clause list * fol_clause list * fol_clause list @@ -30,7 +39,7 @@ datatype 'a fo_term = ATerm of 'a * 'a fo_term list datatype quantifier = AForall | AExists -datatype connective = ANot | AAnd | AOr | AImplies | AIff +datatype connective = ANot | AAnd | AOr | AImplies | AIf | AIff | ANotIff datatype 'a formula = AQuant of quantifier * 'a list * 'a formula | AConn of connective * 'a formula list | @@ -51,7 +60,9 @@ | string_for_connective AAnd = "&" | string_for_connective AOr = "|" | string_for_connective AImplies = "=>" + | string_for_connective AIf = "<=" | string_for_connective AIff = "<=>" + | string_for_connective ANotIff = "<~>" fun string_for_formula (AQuant (q, xs, phi)) = string_for_quantifier q ^ " [" ^ commas xs ^ "] : " ^ string_for_formula phi @@ -141,8 +152,6 @@ val conjecture_prefix = "conj_" val arity_clause_prefix = "clsarity_" -fun hol_ident prefix axiom_name = prefix ^ ascii_of axiom_name - fun wrap_type ty t = ATerm ((type_wrapper_name, type_wrapper_name), [ty, t]) fun fo_term_for_combtyp (CombTVar name) = ATerm (name, []) @@ -180,6 +189,7 @@ fun formula_for_fo_literal (pos, t) = APred t |> not pos ? mk_anot fun formula_for_fo_literals [] = APred (ATerm (("$false", "$false"), [])) + | formula_for_fo_literals [lit] = formula_for_fo_literal lit | formula_for_fo_literals (lit :: lits) = AConn (AOr, [formula_for_fo_literal lit, formula_for_fo_literals lits]) @@ -191,7 +201,7 @@ fun problem_line_for_axiom full_types (clause as FOLClause {axiom_name, kind, ...}) = - Fof (hol_ident axiom_prefix axiom_name, kind, + Fof (axiom_prefix ^ ascii_of axiom_name, kind, formula_for_axiom full_types clause) fun problem_line_for_class_rel_clause @@ -214,10 +224,10 @@ |> formula_for_fo_literals) fun problem_line_for_conjecture full_types - (clause as FOLClause {axiom_name, kind, literals, ...}) = - Fof (hol_ident conjecture_prefix axiom_name, kind, - map (fo_literal_for_literal full_types) literals - |> formula_for_fo_literals |> mk_anot) + (clause as FOLClause {clause_id, kind, literals, ...}) = + Fof (conjecture_prefix ^ Int.toString clause_id, + kind, map (fo_literal_for_literal full_types) literals + |> formula_for_fo_literals |> mk_anot) fun atp_free_type_literals_for_conjecture (FOLClause {ctypes_sorts, ...}) = map (fo_literal_for_type_literal true) (type_literals_for_types ctypes_sorts) @@ -269,7 +279,7 @@ 16383 (* large number *) else if full_types then 0 - else case strip_prefix const_prefix s of + else case strip_prefix_and_undo_ascii const_prefix s of SOME s' => num_type_args thy (invert_const s') | NONE => 0) | min_arity_of _ _ (SOME the_const_tab) s = @@ -364,7 +374,7 @@ (conjectures, axiom_clauses, extra_clauses, helper_clauses, class_rel_clauses, arity_clauses) = let - val explicit_forall = true (* FIXME *) + val explicit_forall = true (* ### FIXME *) val axiom_lines = map (problem_line_for_axiom full_types) axiom_clauses val class_rel_lines = map problem_line_for_class_rel_clause class_rel_clauses