1.1 --- a/src/HOL/Tools/Sledgehammer/metis_tactics.ML Mon May 17 10:16:54 2010 +0200
1.2 +++ b/src/HOL/Tools/Sledgehammer/metis_tactics.ML Mon May 17 10:18:14 2010 +0200
1.3 @@ -141,9 +141,10 @@
1.4 in
1.5 if is_conjecture then
1.6 (Metis.Thm.axiom (Metis.LiteralSet.fromList mlits),
1.7 - add_type_literals types_sorts)
1.8 + type_literals_for_types types_sorts)
1.9 else
1.10 - let val tylits = add_type_literals (filter (not o default_sort ctxt) types_sorts)
1.11 + let val tylits = filter_out (default_sort ctxt) types_sorts
1.12 + |> type_literals_for_types
1.13 val mtylits = if Config.get ctxt type_lits
1.14 then map (metis_of_type_literals false) tylits else []
1.15 in
1.16 @@ -599,9 +600,9 @@
1.17
1.18 (*Extract TFree constraints from context to include as conjecture clauses*)
1.19 fun init_tfrees ctxt =
1.20 - let fun add ((a,i),s) Ts = if i = ~1 then TFree(a,s) :: Ts else Ts
1.21 - in
1.22 - add_type_literals (Vartab.fold add (#2 (Variable.constraints_of ctxt)) [])
1.23 + let fun add ((a,i),s) Ts = if i = ~1 then TFree(a,s) :: Ts else Ts in
1.24 + Vartab.fold add (#2 (Variable.constraints_of ctxt)) []
1.25 + |> type_literals_for_types
1.26 end;
1.27
1.28 (*transform isabelle type / arity clause to metis clause *)
2.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fol_clause.ML Mon May 17 10:16:54 2010 +0200
2.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fol_clause.ML Mon May 17 10:18:14 2010 +0200
2.3 @@ -48,7 +48,7 @@
2.4 TyLitVar of string * name |
2.5 TyLitFree of string * name
2.6 exception CLAUSE of string * term
2.7 - val add_type_literals : typ list -> type_literal list
2.8 + val type_literals_for_types : typ list -> type_literal list
2.9 val get_tvar_strs: typ list -> string list
2.10 datatype arLit =
2.11 TConsLit of class * string * string list
2.12 @@ -331,7 +331,8 @@
2.13 | pred_of_sort (TyLitFree (s, _)) = (s, 1)
2.14
2.15 (*Given a list of sorted type variables, return a list of type literals.*)
2.16 -fun add_type_literals Ts = fold (union (op =)) (map sorts_on_typs Ts) []
2.17 +fun type_literals_for_types Ts =
2.18 + fold (union (op =)) (map sorts_on_typs Ts) []
2.19
2.20 (*The correct treatment of TFrees like 'a in lemmas (axiom clauses) is not clear.
2.21 * Ignoring them leads to unsound proofs, since we do nothing to ensure that 'a
2.22 @@ -520,7 +521,7 @@
2.23 dfg_forall vars ("or(" ^ commas lits ^ ")") ^ ",\n" ^
2.24 string_of_clausename (cls_id,ax_name) ^ ").\n\n";
2.25
2.26 -fun string_of_arity (name, num) = "(" ^ name ^ "," ^ Int.toString num ^ ")"
2.27 +fun string_of_arity (name, arity) = "(" ^ name ^ ", " ^ Int.toString arity ^ ")"
2.28
2.29 fun string_of_preds [] = ""
2.30 | string_of_preds preds = "predicates[" ^ commas(map string_of_arity preds) ^ "].\n";
3.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML Mon May 17 10:16:54 2010 +0200
3.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML Mon May 17 10:18:14 2010 +0200
3.3 @@ -300,7 +300,7 @@
3.4 let
3.5 val (lits, pool) = pool_map (tptp_literal params) literals pool
3.6 val (tylits, pool) = pool_map (tptp_of_type_literal pos)
3.7 - (add_type_literals ctypes_sorts) pool
3.8 + (type_literals_for_types ctypes_sorts) pool
3.9 in ((lits, tylits), pool) end
3.10
3.11 fun tptp_clause params (cls as HOLClause {axiom_name, clause_id, kind, ...})
3.12 @@ -320,7 +320,8 @@
3.13
3.14 fun dfg_type_literals params pos (HOLClause {literals, ctypes_sorts, ...}) =
3.15 pool_map (dfg_literal params) literals
3.16 - #>> rpair (map (dfg_of_type_literal pos) (add_type_literals ctypes_sorts))
3.17 + #>> rpair (map (dfg_of_type_literal pos)
3.18 + (type_literals_for_types ctypes_sorts))
3.19
3.20 fun get_uvars (CombConst _) vars pool = (vars, pool)
3.21 | get_uvars (CombVar (name, _)) vars pool =
3.22 @@ -531,6 +532,8 @@
3.23
3.24 (* DFG format *)
3.25
3.26 +fun dfg_tfree_predicate s = (first_field "(" s |> the |> fst, 1)
3.27 +
3.28 fun write_dfg_file full_types explicit_apply file clauses =
3.29 let
3.30 (* Some of the helper functions below are not name-pool-aware. However,
3.31 @@ -543,13 +546,16 @@
3.32 val params = (full_types, explicit_apply, cma, cnh)
3.33 val ((conjecture_clss, tfree_litss), pool) =
3.34 pool_map (dfg_clause params) conjectures pool |>> ListPair.unzip
3.35 - and problem_name = Path.implode (Path.base file)
3.36 + val tfree_lits = union_all tfree_litss
3.37 + val problem_name = Path.implode (Path.base file)
3.38 val (axstrs, pool) = pool_map (apfst fst oo dfg_clause params) axclauses pool
3.39 - val tfree_clss = map dfg_tfree_clause (union_all tfree_litss)
3.40 + val tfree_clss = map dfg_tfree_clause tfree_lits
3.41 + val tfree_preds = map dfg_tfree_predicate tfree_lits
3.42 val (helper_clauses_strs, pool) =
3.43 pool_map (apfst fst oo dfg_clause params) helper_clauses pool
3.44 val (funcs, cl_preds) = decls_of_clauses params (helper_clauses @ conjectures @ axclauses) arity_clauses
3.45 - and ty_preds = preds_of_clauses axclauses classrel_clauses arity_clauses
3.46 + val ty_preds = preds_of_clauses axclauses classrel_clauses arity_clauses
3.47 + val preds = tfree_preds @ cl_preds @ ty_preds
3.48 val conjecture_offset =
3.49 length axclauses + length classrel_clauses + length arity_clauses
3.50 + length helper_clauses
3.51 @@ -559,7 +565,7 @@
3.52 string_of_start problem_name ::
3.53 string_of_descrip problem_name ::
3.54 string_of_symbols (string_of_funcs funcs)
3.55 - (string_of_preds (cl_preds @ ty_preds)) ::
3.56 + (string_of_preds preds) ::
3.57 "list_of_clauses(axioms, cnf).\n" ::
3.58 axstrs @
3.59 map dfg_classrel_clause classrel_clauses @