# HG changeset patch # User blanchet # Date 1305907306 -7200 # Node ID c8d9bce88f89d7ab6901e74576283ff34b5796d4 # Parent ce269ee43800e0e5878c254110f9428147b1b1d8 name tuning diff -r ce269ee43800 -r c8d9bce88f89 src/HOL/Tools/Metis/metis_translate.ML --- a/src/HOL/Tools/Metis/metis_translate.ML Fri May 20 17:16:13 2011 +0200 +++ b/src/HOL/Tools/Metis/metis_translate.ML Fri May 20 18:01:46 2011 +0200 @@ -14,11 +14,14 @@ datatype type_literal = TyLitVar of name * name | TyLitFree of name * name - datatype arLit = + datatype arity_literal = TConsLit of name * name * name list | TVarLit of name * name datatype arity_clause = - ArityClause of {name: string, conclLit: arLit, premLits: arLit list} + ArityClause of + {name: string, + prem_lits: arity_literal list, + concl_lits: arity_literal} datatype class_rel_clause = ClassRelClause of {name: string, subclass: name, superclass: name} datatype combterm = @@ -274,13 +277,15 @@ (**** Isabelle arities ****) -datatype arLit = +datatype arity_literal = TConsLit of name * name * name list | TVarLit of name * name datatype arity_clause = - ArityClause of {name: string, conclLit: arLit, premLits: arLit list} - + ArityClause of + {name: string, + prem_lits: arity_literal list, + concl_lits: arity_literal} fun gen_TVars 0 = [] | gen_TVars n = ("T_" ^ string_of_int n) :: gen_TVars (n-1); @@ -288,7 +293,7 @@ fun pack_sort(_,[]) = [] | pack_sort(tvar, "HOL.type"::srt) = pack_sort (tvar, srt) (*IGNORE sort "type"*) | pack_sort(tvar, cls::srt) = - (`make_type_class cls, (tvar, tvar)) :: pack_sort (tvar, srt) + (`make_type_class cls, `I tvar) :: pack_sort (tvar, srt) (*Arity of type constructor tcon :: (arg1,...,argN)res*) fun make_axiom_arity_clause (tcons, name, (cls,args)) = @@ -297,10 +302,10 @@ val tvars_srts = ListPair.zip (tvars, args) in ArityClause {name = name, - conclLit = TConsLit (`make_type_class cls, - `make_fixed_type_const tcons, - tvars ~~ tvars), - premLits = map TVarLit (union_all (map pack_sort tvars_srts))} + prem_lits = map TVarLit (union_all (map pack_sort tvars_srts)), + concl_lits = TConsLit (`make_type_class cls, + `make_fixed_type_const tcons, + tvars ~~ tvars)} end @@ -719,9 +724,10 @@ | m_arity_cls (TVarLit ((c, _), (s, _))) = metis_lit false c [Metis_Term.Var s] (*TrueI is returned as the Isabelle counterpart because there isn't any.*) -fun arity_cls (ArityClause {conclLit, premLits, ...}) = +fun arity_cls (ArityClause {prem_lits, concl_lits, ...}) = (TrueI, - Metis_Thm.axiom (Metis_LiteralSet.fromList (map m_arity_cls (conclLit :: premLits)))); + Metis_Thm.axiom (Metis_LiteralSet.fromList + (map m_arity_cls (concl_lits :: prem_lits)))); (* CLASSREL CLAUSE *) fun m_class_rel_cls (subclass, _) (superclass, _) = diff -r ce269ee43800 -r c8d9bce88f89 src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML Fri May 20 17:16:13 2011 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML Fri May 20 18:01:46 2011 +0200 @@ -922,13 +922,13 @@ | fo_literal_from_arity_literal (TVarLit (c, sort)) = (false, ATerm (c, [ATerm (sort, [])])) -fun formula_line_for_arity_clause (ArityClause {name, conclLit, premLits, +fun formula_line_for_arity_clause (ArityClause {name, prem_lits, concl_lits, ...}) = Formula (arity_clause_prefix ^ ascii_of name, Axiom, mk_ahorn (map (formula_from_fo_literal o apfst not - o fo_literal_from_arity_literal) premLits) + o fo_literal_from_arity_literal) prem_lits) (formula_from_fo_literal - (fo_literal_from_arity_literal conclLit)) + (fo_literal_from_arity_literal concl_lits)) |> close_formula_universally, intro_info, NONE) fun formula_line_for_conjecture ctxt nonmono_Ts type_sys