1.1 --- a/src/HOL/IsaMakefile Fri Sep 17 16:15:45 2010 +0200
1.2 +++ b/src/HOL/IsaMakefile Fri Sep 17 16:38:11 2010 +0200
1.3 @@ -317,7 +317,8 @@
1.4 Tools/semiring_normalizer.ML \
1.5 Tools/Sledgehammer/clausifier.ML \
1.6 Tools/Sledgehammer/meson_tactic.ML \
1.7 - Tools/Sledgehammer/metis_clauses.ML \
1.8 + Tools/Sledgehammer/metis_reconstruct.ML \
1.9 + Tools/Sledgehammer/metis_translate.ML \
1.10 Tools/Sledgehammer/metis_tactics.ML \
1.11 Tools/Sledgehammer/sledgehammer.ML \
1.12 Tools/Sledgehammer/sledgehammer_filter.ML \
2.1 --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Fri Sep 17 16:15:45 2010 +0200
2.2 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Fri Sep 17 16:38:11 2010 +0200
2.3 @@ -434,7 +434,7 @@
2.4
2.5 fun run_minimize args named_thms id ({pre=st, log, ...}: Mirabelle.run_args) =
2.6 let
2.7 - open Metis_Clauses
2.8 + open Metis_Translate
2.9 val thy = Proof.theory_of st
2.10 val n0 = length (these (!named_thms))
2.11 val (prover_name, _) = get_atp thy args
3.1 --- a/src/HOL/Sledgehammer.thy Fri Sep 17 16:15:45 2010 +0200
3.2 +++ b/src/HOL/Sledgehammer.thy Fri Sep 17 16:38:11 2010 +0200
3.3 @@ -16,7 +16,8 @@
3.4 ("~~/src/Tools/Metis/metis.ML")
3.5 ("Tools/Sledgehammer/clausifier.ML")
3.6 ("Tools/Sledgehammer/meson_tactic.ML")
3.7 - ("Tools/Sledgehammer/metis_clauses.ML")
3.8 + ("Tools/Sledgehammer/metis_translate.ML")
3.9 + ("Tools/Sledgehammer/metis_reconstruct.ML")
3.10 ("Tools/Sledgehammer/metis_tactics.ML")
3.11 ("Tools/Sledgehammer/sledgehammer_util.ML")
3.12 ("Tools/Sledgehammer/sledgehammer_filter.ML")
3.13 @@ -102,7 +103,8 @@
3.14 use "Tools/Sledgehammer/meson_tactic.ML"
3.15 setup Meson_Tactic.setup
3.16
3.17 -use "Tools/Sledgehammer/metis_clauses.ML"
3.18 +use "Tools/Sledgehammer/metis_translate.ML"
3.19 +use "Tools/Sledgehammer/metis_reconstruct.ML"
3.20 use "Tools/Sledgehammer/metis_tactics.ML"
3.21 setup Metis_Tactics.setup
3.22
4.1 --- a/src/HOL/Tools/ATP/atp_proof.ML Fri Sep 17 16:15:45 2010 +0200
4.2 +++ b/src/HOL/Tools/ATP/atp_proof.ML Fri Sep 17 16:38:11 2010 +0200
4.3 @@ -11,6 +11,12 @@
4.4 type 'a fo_term = 'a ATP_Problem.fo_term
4.5 type 'a uniform_formula = 'a ATP_Problem.uniform_formula
4.6
4.7 + datatype failure =
4.8 + Unprovable | IncompleteUnprovable | CantConnect | TimedOut |
4.9 + OutOfResources | SpassTooOld | VampireTooOld | NoPerl | NoLibwwwPerl |
4.10 + MalformedInput | MalformedOutput | Interrupted | InternalError |
4.11 + UnknownError
4.12 +
4.13 type step_name = string * string option
4.14
4.15 datatype 'a step =
4.16 @@ -20,6 +26,13 @@
4.17 type 'a proof = 'a uniform_formula step list
4.18
4.19 val strip_spaces : (char -> bool) -> string -> string
4.20 + val string_for_failure : failure -> string
4.21 + val extract_important_message : string -> string
4.22 + val extract_known_failure :
4.23 + (failure * string) list -> string -> failure option
4.24 + val extract_tstplike_proof_and_outcome :
4.25 + bool -> int -> (string * string) list -> (failure * string) list -> string
4.26 + -> string * failure option
4.27 val is_same_step : step_name * step_name -> bool
4.28 val atp_proof_from_tstplike_string : string -> string proof
4.29 val map_term_names_in_atp_proof :
4.30 @@ -30,6 +43,13 @@
4.31 structure ATP_Proof : ATP_PROOF =
4.32 struct
4.33
4.34 +open ATP_Problem
4.35 +
4.36 +datatype failure =
4.37 + Unprovable | IncompleteUnprovable | CantConnect | TimedOut | OutOfResources |
4.38 + SpassTooOld | VampireTooOld | NoPerl | NoLibwwwPerl | MalformedInput |
4.39 + MalformedOutput | Interrupted | InternalError | UnknownError
4.40 +
4.41 fun strip_spaces_in_list _ [] = []
4.42 | strip_spaces_in_list _ [c1] = if Char.isSpace c1 then [] else [str c1]
4.43 | strip_spaces_in_list is_evil [c1, c2] =
4.44 @@ -51,7 +71,85 @@
4.45 fun is_ident_char c = Char.isAlphaNum c orelse c = #"_"
4.46 val strip_spaces_except_between_ident_chars = strip_spaces is_ident_char
4.47
4.48 -open ATP_Problem
4.49 +val missing_message_tail =
4.50 + " appears to be missing. You will need to install it if you want to run \
4.51 + \ATPs remotely."
4.52 +
4.53 +fun string_for_failure Unprovable = "The ATP problem is unprovable."
4.54 + | string_for_failure IncompleteUnprovable =
4.55 + "The ATP cannot prove the problem."
4.56 + | string_for_failure CantConnect = "Can't connect to remote server."
4.57 + | string_for_failure TimedOut = "Timed out."
4.58 + | string_for_failure OutOfResources = "The ATP ran out of resources."
4.59 + | string_for_failure SpassTooOld =
4.60 + "Isabelle requires a more recent version of SPASS with support for the \
4.61 + \TPTP syntax. To install it, download and extract the package \
4.62 + \\"http://isabelle.in.tum.de/dist/contrib/spass-3.7.tar.gz\" and add the \
4.63 + \\"spass-3.7\" directory's absolute path to " ^
4.64 + quote (Path.implode (Path.expand (Path.appends
4.65 + (Path.variable "ISABELLE_HOME_USER" ::
4.66 + map Path.basic ["etc", "components"])))) ^
4.67 + " on a line of its own."
4.68 + | string_for_failure VampireTooOld =
4.69 + "Isabelle requires a more recent version of Vampire. To install it, follow \
4.70 + \the instructions from the Sledgehammer manual (\"isabelle doc\
4.71 + \ sledgehammer\")."
4.72 + | string_for_failure NoPerl = "Perl" ^ missing_message_tail
4.73 + | string_for_failure NoLibwwwPerl =
4.74 + "The Perl module \"libwww-perl\"" ^ missing_message_tail
4.75 + | string_for_failure MalformedInput =
4.76 + "The ATP problem is malformed. Please report this to the Isabelle \
4.77 + \developers."
4.78 + | string_for_failure MalformedOutput = "The ATP output is malformed."
4.79 + | string_for_failure Interrupted = "The ATP was interrupted."
4.80 + | string_for_failure InternalError = "An internal ATP error occurred."
4.81 + | string_for_failure UnknownError = "An unknown ATP error occurred."
4.82 +
4.83 +fun extract_delimited (begin_delim, end_delim) output =
4.84 + output |> first_field begin_delim |> the |> snd
4.85 + |> first_field end_delim |> the |> fst
4.86 + |> first_field "\n" |> the |> snd
4.87 + handle Option.Option => ""
4.88 +
4.89 +val tstp_important_message_delims =
4.90 + ("% SZS start RequiredInformation", "% SZS end RequiredInformation")
4.91 +
4.92 +fun extract_important_message output =
4.93 + case extract_delimited tstp_important_message_delims output of
4.94 + "" => ""
4.95 + | s => s |> space_explode "\n" |> filter_out (curry (op =) "")
4.96 + |> map (perhaps (try (unprefix "%")))
4.97 + |> map (perhaps (try (unprefix " ")))
4.98 + |> space_implode "\n " |> quote
4.99 +
4.100 +(* Splits by the first possible of a list of delimiters. *)
4.101 +fun extract_tstplike_proof delims output =
4.102 + case pairself (find_first (fn s => String.isSubstring s output))
4.103 + (ListPair.unzip delims) of
4.104 + (SOME begin_delim, SOME end_delim) =>
4.105 + extract_delimited (begin_delim, end_delim) output
4.106 + | _ => ""
4.107 +
4.108 +fun extract_known_failure known_failures output =
4.109 + known_failures
4.110 + |> find_first (fn (_, pattern) => String.isSubstring pattern output)
4.111 + |> Option.map fst
4.112 +
4.113 +fun extract_tstplike_proof_and_outcome complete res_code proof_delims
4.114 + known_failures output =
4.115 + case extract_known_failure known_failures output of
4.116 + NONE => (case extract_tstplike_proof proof_delims output of
4.117 + "" => ("", SOME (if res_code = 0 andalso output = "" then
4.118 + Interrupted
4.119 + else
4.120 + UnknownError))
4.121 + | tstplike_proof => if res_code = 0 then (tstplike_proof, NONE)
4.122 + else ("", SOME UnknownError))
4.123 + | SOME failure =>
4.124 + ("", SOME (if failure = IncompleteUnprovable andalso complete then
4.125 + Unprovable
4.126 + else
4.127 + failure))
4.128
4.129 fun mk_anot (AConn (ANot, [phi])) = phi
4.130 | mk_anot phi = AConn (ANot, [phi])
5.1 --- a/src/HOL/Tools/ATP/atp_systems.ML Fri Sep 17 16:15:45 2010 +0200
5.2 +++ b/src/HOL/Tools/ATP/atp_systems.ML Fri Sep 17 16:38:11 2010 +0200
5.3 @@ -7,11 +7,7 @@
5.4
5.5 signature ATP_SYSTEMS =
5.6 sig
5.7 - datatype failure =
5.8 - Unprovable | IncompleteUnprovable | CantConnect | TimedOut |
5.9 - OutOfResources | SpassTooOld | VampireTooOld | NoPerl | NoLibwwwPerl |
5.10 - MalformedInput | MalformedOutput | Interrupted | InternalError |
5.11 - UnknownError
5.12 + type failure = ATP_Proof.failure
5.13
5.14 type prover_config =
5.15 {exec: string * string,
5.16 @@ -24,9 +20,6 @@
5.17 explicit_forall: bool,
5.18 use_conjecture_for_hypotheses: bool}
5.19
5.20 - val string_for_failure : failure -> string
5.21 - val known_failure_in_output :
5.22 - string -> (failure * string) list -> failure option
5.23 val add_prover: string * prover_config -> theory -> theory
5.24 val get_prover: theory -> string -> prover_config
5.25 val available_atps: theory -> unit
5.26 @@ -38,13 +31,10 @@
5.27 structure ATP_Systems : ATP_SYSTEMS =
5.28 struct
5.29
5.30 +open ATP_Proof
5.31 +
5.32 (* prover configuration *)
5.33
5.34 -datatype failure =
5.35 - Unprovable | IncompleteUnprovable | CantConnect | TimedOut | OutOfResources |
5.36 - SpassTooOld | VampireTooOld | NoPerl | NoLibwwwPerl | MalformedInput |
5.37 - MalformedOutput | Interrupted | InternalError | UnknownError
5.38 -
5.39 type prover_config =
5.40 {exec: string * string,
5.41 required_execs: (string * string) list,
5.42 @@ -56,44 +46,6 @@
5.43 explicit_forall: bool,
5.44 use_conjecture_for_hypotheses: bool}
5.45
5.46 -val missing_message_tail =
5.47 - " appears to be missing. You will need to install it if you want to run \
5.48 - \ATPs remotely."
5.49 -
5.50 -fun string_for_failure Unprovable = "The ATP problem is unprovable."
5.51 - | string_for_failure IncompleteUnprovable =
5.52 - "The ATP cannot prove the problem."
5.53 - | string_for_failure CantConnect = "Can't connect to remote server."
5.54 - | string_for_failure TimedOut = "Timed out."
5.55 - | string_for_failure OutOfResources = "The ATP ran out of resources."
5.56 - | string_for_failure SpassTooOld =
5.57 - "Isabelle requires a more recent version of SPASS with support for the \
5.58 - \TPTP syntax. To install it, download and extract the package \
5.59 - \\"http://isabelle.in.tum.de/dist/contrib/spass-3.7.tar.gz\" and add the \
5.60 - \\"spass-3.7\" directory's absolute path to " ^
5.61 - quote (Path.implode (Path.expand (Path.appends
5.62 - (Path.variable "ISABELLE_HOME_USER" ::
5.63 - map Path.basic ["etc", "components"])))) ^
5.64 - " on a line of its own."
5.65 - | string_for_failure VampireTooOld =
5.66 - "Isabelle requires a more recent version of Vampire. To install it, follow \
5.67 - \the instructions from the Sledgehammer manual (\"isabelle doc\
5.68 - \ sledgehammer\")."
5.69 - | string_for_failure NoPerl = "Perl" ^ missing_message_tail
5.70 - | string_for_failure NoLibwwwPerl =
5.71 - "The Perl module \"libwww-perl\"" ^ missing_message_tail
5.72 - | string_for_failure MalformedInput =
5.73 - "The ATP problem is malformed. Please report this to the Isabelle \
5.74 - \developers."
5.75 - | string_for_failure MalformedOutput = "The ATP output is malformed."
5.76 - | string_for_failure Interrupted = "The ATP was interrupted."
5.77 - | string_for_failure InternalError = "An internal ATP error occurred."
5.78 - | string_for_failure UnknownError = "An unknown ATP error occurred."
5.79 -
5.80 -fun known_failure_in_output output =
5.81 - find_first (fn (_, pattern) => String.isSubstring pattern output)
5.82 - #> Option.map fst
5.83 -
5.84 val known_perl_failures =
5.85 [(CantConnect, "HTTP error"),
5.86 (NoPerl, "env: perl"),
5.87 @@ -124,6 +76,7 @@
5.88
5.89 fun to_secs bonus time = (Time.toMilliseconds time + bonus + 999) div 1000
5.90
5.91 +
5.92 (* E prover *)
5.93
5.94 (* Give older versions of E an extra second, because the "eproof" script wrongly
5.95 @@ -163,6 +116,8 @@
5.96 val e = ("e", e_config)
5.97
5.98
5.99 +(* SPASS *)
5.100 +
5.101 (* The "-VarWeight=3" option helps the higher-order problems, probably by
5.102 counteracting the presence of "hAPP". *)
5.103 val spass_config : prover_config =
5.104 @@ -226,11 +181,11 @@
5.105
5.106 fun get_systems () =
5.107 case bash_output "\"$ISABELLE_ATP/scripts/remote_atp\" -w 2>&1" of
5.108 - (answer, 0) => split_lines answer
5.109 - | (answer, _) =>
5.110 - error (case known_failure_in_output answer known_perl_failures of
5.111 + (output, 0) => split_lines output
5.112 + | (output, _) =>
5.113 + error (case extract_known_failure known_perl_failures output of
5.114 SOME failure => string_for_failure failure
5.115 - | NONE => perhaps (try (unsuffix "\n")) answer ^ ".")
5.116 + | NONE => perhaps (try (unsuffix "\n")) output ^ ".")
5.117
5.118 fun refresh_systems_on_tptp () =
5.119 Synchronized.change systems (fn _ => get_systems ())
6.1 --- a/src/HOL/Tools/Sledgehammer/metis_clauses.ML Fri Sep 17 16:15:45 2010 +0200
6.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
6.3 @@ -1,524 +0,0 @@
6.4 -(* Title: HOL/Tools/Sledgehammer/metis_clauses.ML
6.5 - Author: Jia Meng, Cambridge University Computer Laboratory and NICTA
6.6 - Author: Jasmin Blanchette, TU Muenchen
6.7 -
6.8 -Storing/printing FOL clauses and arity clauses. Typed equality is
6.9 -treated differently.
6.10 -*)
6.11 -
6.12 -signature METIS_CLAUSES =
6.13 -sig
6.14 - type name = string * string
6.15 - datatype type_literal =
6.16 - TyLitVar of name * name |
6.17 - TyLitFree of name * name
6.18 - datatype arLit =
6.19 - TConsLit of name * name * name list |
6.20 - TVarLit of name * name
6.21 - datatype arity_clause =
6.22 - ArityClause of {name: string, conclLit: arLit, premLits: arLit list}
6.23 - datatype class_rel_clause =
6.24 - ClassRelClause of {name: string, subclass: name, superclass: name}
6.25 - datatype combtyp =
6.26 - CombTVar of name |
6.27 - CombTFree of name |
6.28 - CombType of name * combtyp list
6.29 - datatype combterm =
6.30 - CombConst of name * combtyp * combtyp list (* Const and Free *) |
6.31 - CombVar of name * combtyp |
6.32 - CombApp of combterm * combterm
6.33 - datatype fol_literal = FOLLiteral of bool * combterm
6.34 -
6.35 - val type_wrapper_name : string
6.36 - val bound_var_prefix : string
6.37 - val schematic_var_prefix: string
6.38 - val fixed_var_prefix: string
6.39 - val tvar_prefix: string
6.40 - val tfree_prefix: string
6.41 - val const_prefix: string
6.42 - val type_const_prefix: string
6.43 - val class_prefix: string
6.44 - val invert_const: string -> string
6.45 - val ascii_of: string -> string
6.46 - val unascii_of: string -> string
6.47 - val strip_prefix_and_unascii: string -> string -> string option
6.48 - val make_bound_var : string -> string
6.49 - val make_schematic_var : string * int -> string
6.50 - val make_fixed_var : string -> string
6.51 - val make_schematic_type_var : string * int -> string
6.52 - val make_fixed_type_var : string -> string
6.53 - val make_fixed_const : string -> string
6.54 - val make_fixed_type_const : string -> string
6.55 - val make_type_class : string -> string
6.56 - val skolem_theory_name: string
6.57 - val skolem_prefix: string
6.58 - val skolem_infix: string
6.59 - val is_skolem_const_name: string -> bool
6.60 - val num_type_args: theory -> string -> int
6.61 - val type_literals_for_types : typ list -> type_literal list
6.62 - val make_class_rel_clauses: theory -> class list -> class list -> class_rel_clause list
6.63 - val make_arity_clauses: theory -> string list -> class list -> class list * arity_clause list
6.64 - val combtyp_of : combterm -> combtyp
6.65 - val strip_combterm_comb : combterm -> combterm * combterm list
6.66 - val combterm_from_term :
6.67 - theory -> (string * typ) list -> term -> combterm * typ list
6.68 - val literals_of_term : theory -> term -> fol_literal list * typ list
6.69 - val conceal_skolem_terms :
6.70 - int -> (string * term) list -> term -> (string * term) list * term
6.71 - val reveal_skolem_terms : (string * term) list -> term -> term
6.72 - val tfree_classes_of_terms : term list -> string list
6.73 - val tvar_classes_of_terms : term list -> string list
6.74 - val type_consts_of_terms : theory -> term list -> string list
6.75 -end
6.76 -
6.77 -structure Metis_Clauses : METIS_CLAUSES =
6.78 -struct
6.79 -
6.80 -val type_wrapper_name = "ti"
6.81 -
6.82 -val bound_var_prefix = "B_"
6.83 -val schematic_var_prefix = "V_"
6.84 -val fixed_var_prefix = "v_"
6.85 -
6.86 -val tvar_prefix = "T_";
6.87 -val tfree_prefix = "t_";
6.88 -
6.89 -val const_prefix = "c_";
6.90 -val type_const_prefix = "tc_";
6.91 -val class_prefix = "class_";
6.92 -
6.93 -fun union_all xss = fold (union (op =)) xss []
6.94 -
6.95 -(* Readable names for the more common symbolic functions. Do not mess with the
6.96 - last nine entries of the table unless you know what you are doing. *)
6.97 -val const_trans_table =
6.98 - Symtab.make [(@{type_name Product_Type.prod}, "prod"),
6.99 - (@{type_name Sum_Type.sum}, "sum"),
6.100 - (@{const_name HOL.eq}, "equal"),
6.101 - (@{const_name HOL.conj}, "and"),
6.102 - (@{const_name HOL.disj}, "or"),
6.103 - (@{const_name HOL.implies}, "implies"),
6.104 - (@{const_name Set.member}, "member"),
6.105 - (@{const_name fequal}, "fequal"),
6.106 - (@{const_name COMBI}, "COMBI"),
6.107 - (@{const_name COMBK}, "COMBK"),
6.108 - (@{const_name COMBB}, "COMBB"),
6.109 - (@{const_name COMBC}, "COMBC"),
6.110 - (@{const_name COMBS}, "COMBS"),
6.111 - (@{const_name True}, "True"),
6.112 - (@{const_name False}, "False"),
6.113 - (@{const_name If}, "If")]
6.114 -
6.115 -(* Invert the table of translations between Isabelle and ATPs. *)
6.116 -val const_trans_table_inv =
6.117 - Symtab.update ("fequal", @{const_name HOL.eq})
6.118 - (Symtab.make (map swap (Symtab.dest const_trans_table)))
6.119 -
6.120 -val invert_const = perhaps (Symtab.lookup const_trans_table_inv)
6.121 -
6.122 -(*Escaping of special characters.
6.123 - Alphanumeric characters are left unchanged.
6.124 - The character _ goes to __
6.125 - Characters in the range ASCII space to / go to _A to _P, respectively.
6.126 - Other characters go to _nnn where nnn is the decimal ASCII code.*)
6.127 -val A_minus_space = Char.ord #"A" - Char.ord #" ";
6.128 -
6.129 -fun stringN_of_int 0 _ = ""
6.130 - | stringN_of_int k n = stringN_of_int (k-1) (n div 10) ^ Int.toString (n mod 10);
6.131 -
6.132 -fun ascii_of_c c =
6.133 - if Char.isAlphaNum c then String.str c
6.134 - else if c = #"_" then "__"
6.135 - else if #" " <= c andalso c <= #"/"
6.136 - then "_" ^ String.str (Char.chr (Char.ord c + A_minus_space))
6.137 - else ("_" ^ stringN_of_int 3 (Char.ord c)) (*fixed width, in case more digits follow*)
6.138 -
6.139 -val ascii_of = String.translate ascii_of_c;
6.140 -
6.141 -(** Remove ASCII armouring from names in proof files **)
6.142 -
6.143 -(*We don't raise error exceptions because this code can run inside the watcher.
6.144 - Also, the errors are "impossible" (hah!)*)
6.145 -fun unascii_aux rcs [] = String.implode(rev rcs)
6.146 - | unascii_aux rcs [#"_"] = unascii_aux (#"_"::rcs) [] (*ERROR*)
6.147 - (*Three types of _ escapes: __, _A to _P, _nnn*)
6.148 - | unascii_aux rcs (#"_" :: #"_" :: cs) = unascii_aux (#"_"::rcs) cs
6.149 - | unascii_aux rcs (#"_" :: c :: cs) =
6.150 - if #"A" <= c andalso c<= #"P" (*translation of #" " to #"/"*)
6.151 - then unascii_aux (Char.chr(Char.ord c - A_minus_space) :: rcs) cs
6.152 - else
6.153 - let val digits = List.take (c::cs, 3) handle Subscript => []
6.154 - in
6.155 - case Int.fromString (String.implode digits) of
6.156 - NONE => unascii_aux (c:: #"_"::rcs) cs (*ERROR*)
6.157 - | SOME n => unascii_aux (Char.chr n :: rcs) (List.drop (cs, 2))
6.158 - end
6.159 - | unascii_aux rcs (c::cs) = unascii_aux (c::rcs) cs
6.160 -val unascii_of = unascii_aux [] o String.explode
6.161 -
6.162 -(* If string s has the prefix s1, return the result of deleting it,
6.163 - un-ASCII'd. *)
6.164 -fun strip_prefix_and_unascii s1 s =
6.165 - if String.isPrefix s1 s then
6.166 - SOME (unascii_of (String.extract (s, size s1, NONE)))
6.167 - else
6.168 - NONE
6.169 -
6.170 -(*Remove the initial ' character from a type variable, if it is present*)
6.171 -fun trim_type_var s =
6.172 - if s <> "" andalso String.sub(s,0) = #"'" then String.extract(s,1,NONE)
6.173 - else error ("trim_type: Malformed type variable encountered: " ^ s);
6.174 -
6.175 -fun ascii_of_indexname (v,0) = ascii_of v
6.176 - | ascii_of_indexname (v,i) = ascii_of v ^ "_" ^ Int.toString i;
6.177 -
6.178 -fun make_bound_var x = bound_var_prefix ^ ascii_of x
6.179 -fun make_schematic_var v = schematic_var_prefix ^ ascii_of_indexname v
6.180 -fun make_fixed_var x = fixed_var_prefix ^ ascii_of x
6.181 -
6.182 -fun make_schematic_type_var (x,i) =
6.183 - tvar_prefix ^ (ascii_of_indexname (trim_type_var x,i));
6.184 -fun make_fixed_type_var x = tfree_prefix ^ (ascii_of (trim_type_var x));
6.185 -
6.186 -fun lookup_const c =
6.187 - case Symtab.lookup const_trans_table c of
6.188 - SOME c' => c'
6.189 - | NONE => ascii_of c
6.190 -
6.191 -(* HOL.eq MUST BE "equal" because it's built into ATPs. *)
6.192 -fun make_fixed_const @{const_name HOL.eq} = "equal"
6.193 - | make_fixed_const c = const_prefix ^ lookup_const c
6.194 -
6.195 -fun make_fixed_type_const c = type_const_prefix ^ lookup_const c
6.196 -
6.197 -fun make_type_class clas = class_prefix ^ ascii_of clas;
6.198 -
6.199 -val skolem_theory_name = "Sledgehammer" ^ Long_Name.separator ^ "Sko"
6.200 -val skolem_prefix = "sko_"
6.201 -val skolem_infix = "$"
6.202 -
6.203 -(* Hack: Could return false positives (e.g., a user happens to declare a
6.204 - constant called "SomeTheory.sko_means_shoe_in_$wedish". *)
6.205 -val is_skolem_const_name =
6.206 - Long_Name.base_name
6.207 - #> String.isPrefix skolem_prefix andf String.isSubstring skolem_infix
6.208 -
6.209 -(* The number of type arguments of a constant, zero if it's monomorphic. For
6.210 - (instances of) Skolem pseudoconstants, this information is encoded in the
6.211 - constant name. *)
6.212 -fun num_type_args thy s =
6.213 - if String.isPrefix skolem_theory_name s then
6.214 - s |> unprefix skolem_theory_name
6.215 - |> space_explode skolem_infix |> hd
6.216 - |> space_explode "_" |> List.last |> Int.fromString |> the
6.217 - else
6.218 - (s, Sign.the_const_type thy s) |> Sign.const_typargs thy |> length
6.219 -
6.220 -(**** Definitions and functions for FOL clauses for TPTP format output ****)
6.221 -
6.222 -type name = string * string
6.223 -
6.224 -(**** Isabelle FOL clauses ****)
6.225 -
6.226 -(* The first component is the type class; the second is a TVar or TFree. *)
6.227 -datatype type_literal =
6.228 - TyLitVar of name * name |
6.229 - TyLitFree of name * name
6.230 -
6.231 -exception CLAUSE of string * term;
6.232 -
6.233 -(*Make literals for sorted type variables*)
6.234 -fun sorts_on_typs_aux (_, []) = []
6.235 - | sorts_on_typs_aux ((x,i), s::ss) =
6.236 - let val sorts = sorts_on_typs_aux ((x,i), ss)
6.237 - in
6.238 - if s = "HOL.type" then sorts
6.239 - else if i = ~1 then TyLitFree (`make_type_class s, `make_fixed_type_var x) :: sorts
6.240 - else TyLitVar (`make_type_class s, (make_schematic_type_var (x,i), x)) :: sorts
6.241 - end;
6.242 -
6.243 -fun sorts_on_typs (TFree (a,s)) = sorts_on_typs_aux ((a,~1),s)
6.244 - | sorts_on_typs (TVar (v,s)) = sorts_on_typs_aux (v,s);
6.245 -
6.246 -(*Given a list of sorted type variables, return a list of type literals.*)
6.247 -fun type_literals_for_types Ts =
6.248 - fold (union (op =)) (map sorts_on_typs Ts) []
6.249 -
6.250 -(** make axiom and conjecture clauses. **)
6.251 -
6.252 -(**** Isabelle arities ****)
6.253 -
6.254 -datatype arLit =
6.255 - TConsLit of name * name * name list |
6.256 - TVarLit of name * name
6.257 -
6.258 -datatype arity_clause =
6.259 - ArityClause of {name: string, conclLit: arLit, premLits: arLit list}
6.260 -
6.261 -
6.262 -fun gen_TVars 0 = []
6.263 - | gen_TVars n = ("T_" ^ Int.toString n) :: gen_TVars (n-1);
6.264 -
6.265 -fun pack_sort(_,[]) = []
6.266 - | pack_sort(tvar, "HOL.type"::srt) = pack_sort (tvar, srt) (*IGNORE sort "type"*)
6.267 - | pack_sort(tvar, cls::srt) =
6.268 - (`make_type_class cls, (tvar, tvar)) :: pack_sort (tvar, srt)
6.269 -
6.270 -(*Arity of type constructor tcon :: (arg1,...,argN)res*)
6.271 -fun make_axiom_arity_clause (tcons, name, (cls,args)) =
6.272 - let
6.273 - val tvars = gen_TVars (length args)
6.274 - val tvars_srts = ListPair.zip (tvars, args)
6.275 - in
6.276 - ArityClause {name = name,
6.277 - conclLit = TConsLit (`make_type_class cls,
6.278 - `make_fixed_type_const tcons,
6.279 - tvars ~~ tvars),
6.280 - premLits = map TVarLit (union_all (map pack_sort tvars_srts))}
6.281 - end
6.282 -
6.283 -
6.284 -(**** Isabelle class relations ****)
6.285 -
6.286 -datatype class_rel_clause =
6.287 - ClassRelClause of {name: string, subclass: name, superclass: name}
6.288 -
6.289 -(*Generate all pairs (sub,super) such that sub is a proper subclass of super in theory thy.*)
6.290 -fun class_pairs _ [] _ = []
6.291 - | class_pairs thy subs supers =
6.292 - let
6.293 - val class_less = Sorts.class_less (Sign.classes_of thy)
6.294 - fun add_super sub super = class_less (sub, super) ? cons (sub, super)
6.295 - fun add_supers sub = fold (add_super sub) supers
6.296 - in fold add_supers subs [] end
6.297 -
6.298 -fun make_class_rel_clause (sub,super) =
6.299 - ClassRelClause {name = sub ^ "_" ^ super,
6.300 - subclass = `make_type_class sub,
6.301 - superclass = `make_type_class super}
6.302 -
6.303 -fun make_class_rel_clauses thy subs supers =
6.304 - map make_class_rel_clause (class_pairs thy subs supers);
6.305 -
6.306 -
6.307 -(** Isabelle arities **)
6.308 -
6.309 -fun arity_clause _ _ (_, []) = []
6.310 - | arity_clause seen n (tcons, ("HOL.type",_)::ars) = (*ignore*)
6.311 - arity_clause seen n (tcons,ars)
6.312 - | arity_clause seen n (tcons, (ar as (class,_)) :: ars) =
6.313 - if member (op =) seen class then (*multiple arities for the same tycon, class pair*)
6.314 - make_axiom_arity_clause (tcons, lookup_const tcons ^ "_" ^ class ^ "_" ^ Int.toString n, ar) ::
6.315 - arity_clause seen (n+1) (tcons,ars)
6.316 - else
6.317 - make_axiom_arity_clause (tcons, lookup_const tcons ^ "_" ^ class, ar) ::
6.318 - arity_clause (class::seen) n (tcons,ars)
6.319 -
6.320 -fun multi_arity_clause [] = []
6.321 - | multi_arity_clause ((tcons, ars) :: tc_arlists) =
6.322 - arity_clause [] 1 (tcons, ars) @ multi_arity_clause tc_arlists
6.323 -
6.324 -(*Generate all pairs (tycon,class,sorts) such that tycon belongs to class in theory thy
6.325 - provided its arguments have the corresponding sorts.*)
6.326 -fun type_class_pairs thy tycons classes =
6.327 - let val alg = Sign.classes_of thy
6.328 - fun domain_sorts tycon = Sorts.mg_domain alg tycon o single
6.329 - fun add_class tycon class =
6.330 - cons (class, domain_sorts tycon class)
6.331 - handle Sorts.CLASS_ERROR _ => I
6.332 - fun try_classes tycon = (tycon, fold (add_class tycon) classes [])
6.333 - in map try_classes tycons end;
6.334 -
6.335 -(*Proving one (tycon, class) membership may require proving others, so iterate.*)
6.336 -fun iter_type_class_pairs _ _ [] = ([], [])
6.337 - | iter_type_class_pairs thy tycons classes =
6.338 - let val cpairs = type_class_pairs thy tycons classes
6.339 - val newclasses = union_all (union_all (union_all (map (map #2 o #2) cpairs)))
6.340 - |> subtract (op =) classes |> subtract (op =) HOLogic.typeS
6.341 - val (classes', cpairs') = iter_type_class_pairs thy tycons newclasses
6.342 - in (union (op =) classes' classes, union (op =) cpairs' cpairs) end;
6.343 -
6.344 -fun make_arity_clauses thy tycons classes =
6.345 - let val (classes', cpairs) = iter_type_class_pairs thy tycons classes
6.346 - in (classes', multi_arity_clause cpairs) end;
6.347 -
6.348 -datatype combtyp =
6.349 - CombTVar of name |
6.350 - CombTFree of name |
6.351 - CombType of name * combtyp list
6.352 -
6.353 -datatype combterm =
6.354 - CombConst of name * combtyp * combtyp list (* Const and Free *) |
6.355 - CombVar of name * combtyp |
6.356 - CombApp of combterm * combterm
6.357 -
6.358 -datatype fol_literal = FOLLiteral of bool * combterm
6.359 -
6.360 -(*********************************************************************)
6.361 -(* convert a clause with type Term.term to a clause with type clause *)
6.362 -(*********************************************************************)
6.363 -
6.364 -(*Result of a function type; no need to check that the argument type matches.*)
6.365 -fun result_type (CombType (_, [_, tp2])) = tp2
6.366 - | result_type _ = raise Fail "non-function type"
6.367 -
6.368 -fun combtyp_of (CombConst (_, tp, _)) = tp
6.369 - | combtyp_of (CombVar (_, tp)) = tp
6.370 - | combtyp_of (CombApp (t1, _)) = result_type (combtyp_of t1)
6.371 -
6.372 -(*gets the head of a combinator application, along with the list of arguments*)
6.373 -fun strip_combterm_comb u =
6.374 - let fun stripc (CombApp(t,u), ts) = stripc (t, u::ts)
6.375 - | stripc x = x
6.376 - in stripc(u,[]) end
6.377 -
6.378 -fun type_of (Type (a, Ts)) =
6.379 - let val (folTypes,ts) = types_of Ts in
6.380 - (CombType (`make_fixed_type_const a, folTypes), ts)
6.381 - end
6.382 - | type_of (tp as TFree (a, _)) = (CombTFree (`make_fixed_type_var a), [tp])
6.383 - | type_of (tp as TVar (x, _)) =
6.384 - (CombTVar (make_schematic_type_var x, string_of_indexname x), [tp])
6.385 -and types_of Ts =
6.386 - let val (folTyps, ts) = ListPair.unzip (map type_of Ts) in
6.387 - (folTyps, union_all ts)
6.388 - end
6.389 -
6.390 -(* same as above, but no gathering of sort information *)
6.391 -fun simp_type_of (Type (a, Ts)) =
6.392 - CombType (`make_fixed_type_const a, map simp_type_of Ts)
6.393 - | simp_type_of (TFree (a, _)) = CombTFree (`make_fixed_type_var a)
6.394 - | simp_type_of (TVar (x, _)) =
6.395 - CombTVar (make_schematic_type_var x, string_of_indexname x)
6.396 -
6.397 -(* Converts a term (with combinators) into a combterm. Also accummulates sort
6.398 - infomation. *)
6.399 -fun combterm_from_term thy bs (P $ Q) =
6.400 - let val (P', tsP) = combterm_from_term thy bs P
6.401 - val (Q', tsQ) = combterm_from_term thy bs Q
6.402 - in (CombApp (P', Q'), union (op =) tsP tsQ) end
6.403 - | combterm_from_term thy _ (Const (c, T)) =
6.404 - let
6.405 - val (tp, ts) = type_of T
6.406 - val tvar_list =
6.407 - (if String.isPrefix skolem_theory_name c then
6.408 - [] |> Term.add_tvarsT T |> map TVar
6.409 - else
6.410 - (c, T) |> Sign.const_typargs thy)
6.411 - |> map simp_type_of
6.412 - val c' = CombConst (`make_fixed_const c, tp, tvar_list)
6.413 - in (c',ts) end
6.414 - | combterm_from_term _ _ (Free (v, T)) =
6.415 - let val (tp,ts) = type_of T
6.416 - val v' = CombConst (`make_fixed_var v, tp, [])
6.417 - in (v',ts) end
6.418 - | combterm_from_term _ _ (Var (v, T)) =
6.419 - let val (tp,ts) = type_of T
6.420 - val v' = CombVar ((make_schematic_var v, string_of_indexname v), tp)
6.421 - in (v',ts) end
6.422 - | combterm_from_term _ bs (Bound j) =
6.423 - let
6.424 - val (s, T) = nth bs j
6.425 - val (tp, ts) = type_of T
6.426 - val v' = CombConst (`make_bound_var s, tp, [])
6.427 - in (v', ts) end
6.428 - | combterm_from_term _ _ (Abs _) = raise Fail "HOL clause: Abs"
6.429 -
6.430 -fun predicate_of thy ((@{const Not} $ P), pos) = predicate_of thy (P, not pos)
6.431 - | predicate_of thy (t, pos) =
6.432 - (combterm_from_term thy [] (Envir.eta_contract t), pos)
6.433 -
6.434 -fun literals_of_term1 args thy (@{const Trueprop} $ P) =
6.435 - literals_of_term1 args thy P
6.436 - | literals_of_term1 args thy (@{const HOL.disj} $ P $ Q) =
6.437 - literals_of_term1 (literals_of_term1 args thy P) thy Q
6.438 - | literals_of_term1 (lits, ts) thy P =
6.439 - let val ((pred, ts'), pol) = predicate_of thy (P, true) in
6.440 - (FOLLiteral (pol, pred) :: lits, union (op =) ts ts')
6.441 - end
6.442 -val literals_of_term = literals_of_term1 ([], [])
6.443 -
6.444 -fun skolem_name i j num_T_args =
6.445 - skolem_prefix ^ (space_implode "_" (map Int.toString [i, j, num_T_args])) ^
6.446 - skolem_infix ^ "g"
6.447 -
6.448 -fun conceal_skolem_terms i skolems t =
6.449 - if exists_Const (curry (op =) @{const_name skolem} o fst) t then
6.450 - let
6.451 - fun aux skolems
6.452 - (t as (Const (@{const_name skolem}, Type (_, [_, T])) $ _)) =
6.453 - let
6.454 - val (skolems, s) =
6.455 - if i = ~1 then
6.456 - (skolems, @{const_name undefined})
6.457 - else case AList.find (op aconv) skolems t of
6.458 - s :: _ => (skolems, s)
6.459 - | [] =>
6.460 - let
6.461 - val s = skolem_theory_name ^ "." ^
6.462 - skolem_name i (length skolems)
6.463 - (length (Term.add_tvarsT T []))
6.464 - in ((s, t) :: skolems, s) end
6.465 - in (skolems, Const (s, T)) end
6.466 - | aux skolems (t1 $ t2) =
6.467 - let
6.468 - val (skolems, t1) = aux skolems t1
6.469 - val (skolems, t2) = aux skolems t2
6.470 - in (skolems, t1 $ t2) end
6.471 - | aux skolems (Abs (s, T, t')) =
6.472 - let val (skolems, t') = aux skolems t' in
6.473 - (skolems, Abs (s, T, t'))
6.474 - end
6.475 - | aux skolems t = (skolems, t)
6.476 - in aux skolems t end
6.477 - else
6.478 - (skolems, t)
6.479 -
6.480 -fun reveal_skolem_terms skolems =
6.481 - map_aterms (fn t as Const (s, _) =>
6.482 - if String.isPrefix skolem_theory_name s then
6.483 - AList.lookup (op =) skolems s |> the
6.484 - |> map_types Type_Infer.paramify_vars
6.485 - else
6.486 - t
6.487 - | t => t)
6.488 -
6.489 -
6.490 -(***************************************************************)
6.491 -(* Type Classes Present in the Axiom or Conjecture Clauses *)
6.492 -(***************************************************************)
6.493 -
6.494 -fun set_insert (x, s) = Symtab.update (x, ()) s
6.495 -
6.496 -fun add_classes (sorts, cset) = List.foldl set_insert cset (flat sorts)
6.497 -
6.498 -(*Remove this trivial type class*)
6.499 -fun delete_type cset = Symtab.delete_safe (the_single @{sort HOL.type}) cset;
6.500 -
6.501 -fun tfree_classes_of_terms ts =
6.502 - let val sorts_list = map (map #2 o OldTerm.term_tfrees) ts
6.503 - in Symtab.keys (delete_type (List.foldl add_classes Symtab.empty sorts_list)) end;
6.504 -
6.505 -fun tvar_classes_of_terms ts =
6.506 - let val sorts_list = map (map #2 o OldTerm.term_tvars) ts
6.507 - in Symtab.keys (delete_type (List.foldl add_classes Symtab.empty sorts_list)) end;
6.508 -
6.509 -(*fold type constructors*)
6.510 -fun fold_type_consts f (Type (a, Ts)) x = fold (fold_type_consts f) Ts (f (a,x))
6.511 - | fold_type_consts _ _ x = x;
6.512 -
6.513 -(*Type constructors used to instantiate overloaded constants are the only ones needed.*)
6.514 -fun add_type_consts_in_term thy =
6.515 - let
6.516 - fun aux (Const x) =
6.517 - fold (fold_type_consts set_insert) (Sign.const_typargs thy x)
6.518 - | aux (Abs (_, _, u)) = aux u
6.519 - | aux (Const (@{const_name skolem}, _) $ _) = I
6.520 - | aux (t $ u) = aux t #> aux u
6.521 - | aux _ = I
6.522 - in aux end
6.523 -
6.524 -fun type_consts_of_terms thy ts =
6.525 - Symtab.keys (fold (add_type_consts_in_term thy) ts Symtab.empty);
6.526 -
6.527 -end;
7.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
7.2 +++ b/src/HOL/Tools/Sledgehammer/metis_reconstruct.ML Fri Sep 17 16:38:11 2010 +0200
7.3 @@ -0,0 +1,514 @@
7.4 +(* Title: HOL/Tools/Sledgehammer/metis_reconstruct.ML
7.5 + Author: Kong W. Susanto, Cambridge University Computer Laboratory
7.6 + Author: Lawrence C. Paulson, Cambridge University Computer Laboratory
7.7 + Author: Jasmin Blanchette, TU Muenchen
7.8 + Copyright Cambridge University 2007
7.9 +
7.10 +Proof reconstruction for Metis.
7.11 +*)
7.12 +
7.13 +signature METIS_RECONSTRUCT =
7.14 +sig
7.15 + type mode = Metis_Translate.mode
7.16 +
7.17 + val trace: bool Unsynchronized.ref
7.18 + val lookth : (Metis_Thm.thm * 'a) list -> Metis_Thm.thm -> 'a
7.19 + val replay_one_inference :
7.20 + Proof.context -> mode -> (string * term) list
7.21 + -> Metis_Thm.thm * Metis_Proof.inference -> (Metis_Thm.thm * thm) list
7.22 + -> (Metis_Thm.thm * thm) list
7.23 +end;
7.24 +
7.25 +structure Metis_Reconstruct : METIS_RECONSTRUCT =
7.26 +struct
7.27 +
7.28 +open Metis_Translate
7.29 +
7.30 +val trace = Unsynchronized.ref false
7.31 +fun trace_msg msg = if !trace then tracing (msg ()) else ()
7.32 +
7.33 +datatype term_or_type = SomeTerm of term | SomeType of typ
7.34 +
7.35 +fun terms_of [] = []
7.36 + | terms_of (SomeTerm t :: tts) = t :: terms_of tts
7.37 + | terms_of (SomeType _ :: tts) = terms_of tts;
7.38 +
7.39 +fun types_of [] = []
7.40 + | types_of (SomeTerm (Var ((a,idx), _)) :: tts) =
7.41 + if String.isPrefix "_" a then
7.42 + (*Variable generated by Metis, which might have been a type variable.*)
7.43 + TVar (("'" ^ a, idx), HOLogic.typeS) :: types_of tts
7.44 + else types_of tts
7.45 + | types_of (SomeTerm _ :: tts) = types_of tts
7.46 + | types_of (SomeType T :: tts) = T :: types_of tts;
7.47 +
7.48 +fun apply_list rator nargs rands =
7.49 + let val trands = terms_of rands
7.50 + in if length trands = nargs then SomeTerm (list_comb(rator, trands))
7.51 + else raise Fail
7.52 + ("apply_list: wrong number of arguments: " ^ Syntax.string_of_term_global Pure.thy rator ^
7.53 + " expected " ^ Int.toString nargs ^
7.54 + " received " ^ commas (map (Syntax.string_of_term_global Pure.thy) trands))
7.55 + end;
7.56 +
7.57 +fun infer_types ctxt =
7.58 + Syntax.check_terms (ProofContext.set_mode ProofContext.mode_pattern ctxt);
7.59 +
7.60 +(*We use 1 rather than 0 because variable references in clauses may otherwise conflict
7.61 + with variable constraints in the goal...at least, type inference often fails otherwise.
7.62 + SEE ALSO axiom_inf below.*)
7.63 +fun mk_var (w, T) = Var ((w, 1), T)
7.64 +
7.65 +(*include the default sort, if available*)
7.66 +fun mk_tfree ctxt w =
7.67 + let val ww = "'" ^ w
7.68 + in TFree(ww, the_default HOLogic.typeS (Variable.def_sort ctxt (ww, ~1))) end;
7.69 +
7.70 +(*Remove the "apply" operator from an HO term*)
7.71 +fun strip_happ args (Metis_Term.Fn(".",[t,u])) = strip_happ (u::args) t
7.72 + | strip_happ args x = (x, args);
7.73 +
7.74 +fun make_tvar s = TVar (("'" ^ s, 0), HOLogic.typeS)
7.75 +
7.76 +fun smart_invert_const "fequal" = @{const_name HOL.eq}
7.77 + | smart_invert_const s = invert_const s
7.78 +
7.79 +fun hol_type_from_metis_term _ (Metis_Term.Var v) =
7.80 + (case strip_prefix_and_unascii tvar_prefix v of
7.81 + SOME w => make_tvar w
7.82 + | NONE => make_tvar v)
7.83 + | hol_type_from_metis_term ctxt (Metis_Term.Fn(x, tys)) =
7.84 + (case strip_prefix_and_unascii type_const_prefix x of
7.85 + SOME tc => Type (smart_invert_const tc,
7.86 + map (hol_type_from_metis_term ctxt) tys)
7.87 + | NONE =>
7.88 + case strip_prefix_and_unascii tfree_prefix x of
7.89 + SOME tf => mk_tfree ctxt tf
7.90 + | NONE => raise Fail ("hol_type_from_metis_term: " ^ x));
7.91 +
7.92 +(*Maps metis terms to isabelle terms*)
7.93 +fun hol_term_from_metis_PT ctxt fol_tm =
7.94 + let val thy = ProofContext.theory_of ctxt
7.95 + val _ = trace_msg (fn () => "hol_term_from_metis_PT: " ^
7.96 + Metis_Term.toString fol_tm)
7.97 + fun tm_to_tt (Metis_Term.Var v) =
7.98 + (case strip_prefix_and_unascii tvar_prefix v of
7.99 + SOME w => SomeType (make_tvar w)
7.100 + | NONE =>
7.101 + case strip_prefix_and_unascii schematic_var_prefix v of
7.102 + SOME w => SomeTerm (mk_var (w, HOLogic.typeT))
7.103 + | NONE => SomeTerm (mk_var (v, HOLogic.typeT)) )
7.104 + (*Var from Metis with a name like _nnn; possibly a type variable*)
7.105 + | tm_to_tt (Metis_Term.Fn ("{}", [arg])) = tm_to_tt arg (*hBOOL*)
7.106 + | tm_to_tt (t as Metis_Term.Fn (".",_)) =
7.107 + let val (rator,rands) = strip_happ [] t
7.108 + in case rator of
7.109 + Metis_Term.Fn(fname,ts) => applic_to_tt (fname, ts @ rands)
7.110 + | _ => case tm_to_tt rator of
7.111 + SomeTerm t => SomeTerm (list_comb(t, terms_of (map tm_to_tt rands)))
7.112 + | _ => raise Fail "tm_to_tt: HO application"
7.113 + end
7.114 + | tm_to_tt (Metis_Term.Fn (fname, args)) = applic_to_tt (fname,args)
7.115 + and applic_to_tt ("=",ts) =
7.116 + SomeTerm (list_comb(Const (@{const_name HOL.eq}, HOLogic.typeT), terms_of (map tm_to_tt ts)))
7.117 + | applic_to_tt (a,ts) =
7.118 + case strip_prefix_and_unascii const_prefix a of
7.119 + SOME b =>
7.120 + let val c = smart_invert_const b
7.121 + val ntypes = num_type_args thy c
7.122 + val nterms = length ts - ntypes
7.123 + val tts = map tm_to_tt ts
7.124 + val tys = types_of (List.take(tts,ntypes))
7.125 + in if length tys = ntypes then
7.126 + apply_list (Const (c, dummyT)) nterms (List.drop(tts,ntypes))
7.127 + else
7.128 + raise Fail ("Constant " ^ c ^ " expects " ^ Int.toString ntypes ^
7.129 + " but gets " ^ Int.toString (length tys) ^
7.130 + " type arguments\n" ^
7.131 + cat_lines (map (Syntax.string_of_typ ctxt) tys) ^
7.132 + " the terms are \n" ^
7.133 + cat_lines (map (Syntax.string_of_term ctxt) (terms_of tts)))
7.134 + end
7.135 + | NONE => (*Not a constant. Is it a type constructor?*)
7.136 + case strip_prefix_and_unascii type_const_prefix a of
7.137 + SOME b =>
7.138 + SomeType (Type (smart_invert_const b, types_of (map tm_to_tt ts)))
7.139 + | NONE => (*Maybe a TFree. Should then check that ts=[].*)
7.140 + case strip_prefix_and_unascii tfree_prefix a of
7.141 + SOME b => SomeType (mk_tfree ctxt b)
7.142 + | NONE => (*a fixed variable? They are Skolem functions.*)
7.143 + case strip_prefix_and_unascii fixed_var_prefix a of
7.144 + SOME b =>
7.145 + let val opr = Free (b, HOLogic.typeT)
7.146 + in apply_list opr (length ts) (map tm_to_tt ts) end
7.147 + | NONE => raise Fail ("unexpected metis function: " ^ a)
7.148 + in
7.149 + case tm_to_tt fol_tm of
7.150 + SomeTerm t => t
7.151 + | SomeType T => raise TYPE ("fol_tm_to_tt: Term expected", [T], [])
7.152 + end
7.153 +
7.154 +(*Maps fully-typed metis terms to isabelle terms*)
7.155 +fun hol_term_from_metis_FT ctxt fol_tm =
7.156 + let val _ = trace_msg (fn () => "hol_term_from_metis_FT: " ^
7.157 + Metis_Term.toString fol_tm)
7.158 + fun cvt (Metis_Term.Fn ("ti", [Metis_Term.Var v, _])) =
7.159 + (case strip_prefix_and_unascii schematic_var_prefix v of
7.160 + SOME w => mk_var(w, dummyT)
7.161 + | NONE => mk_var(v, dummyT))
7.162 + | cvt (Metis_Term.Fn ("ti", [Metis_Term.Fn ("=",[]), _])) =
7.163 + Const (@{const_name HOL.eq}, HOLogic.typeT)
7.164 + | cvt (Metis_Term.Fn ("ti", [Metis_Term.Fn (x,[]), ty])) =
7.165 + (case strip_prefix_and_unascii const_prefix x of
7.166 + SOME c => Const (smart_invert_const c, dummyT)
7.167 + | NONE => (*Not a constant. Is it a fixed variable??*)
7.168 + case strip_prefix_and_unascii fixed_var_prefix x of
7.169 + SOME v => Free (v, hol_type_from_metis_term ctxt ty)
7.170 + | NONE => raise Fail ("hol_term_from_metis_FT bad constant: " ^ x))
7.171 + | cvt (Metis_Term.Fn ("ti", [Metis_Term.Fn (".",[tm1,tm2]), _])) =
7.172 + cvt tm1 $ cvt tm2
7.173 + | cvt (Metis_Term.Fn (".",[tm1,tm2])) = (*untyped application*)
7.174 + cvt tm1 $ cvt tm2
7.175 + | cvt (Metis_Term.Fn ("{}", [arg])) = cvt arg (*hBOOL*)
7.176 + | cvt (Metis_Term.Fn ("=", [tm1,tm2])) =
7.177 + list_comb(Const (@{const_name HOL.eq}, HOLogic.typeT), map cvt [tm1,tm2])
7.178 + | cvt (t as Metis_Term.Fn (x, [])) =
7.179 + (case strip_prefix_and_unascii const_prefix x of
7.180 + SOME c => Const (smart_invert_const c, dummyT)
7.181 + | NONE => (*Not a constant. Is it a fixed variable??*)
7.182 + case strip_prefix_and_unascii fixed_var_prefix x of
7.183 + SOME v => Free (v, dummyT)
7.184 + | NONE => (trace_msg (fn () => "hol_term_from_metis_FT bad const: " ^ x);
7.185 + hol_term_from_metis_PT ctxt t))
7.186 + | cvt t = (trace_msg (fn () => "hol_term_from_metis_FT bad term: " ^ Metis_Term.toString t);
7.187 + hol_term_from_metis_PT ctxt t)
7.188 + in fol_tm |> cvt end
7.189 +
7.190 +fun hol_term_from_metis FT = hol_term_from_metis_FT
7.191 + | hol_term_from_metis _ = hol_term_from_metis_PT
7.192 +
7.193 +fun hol_terms_from_fol ctxt mode skolems fol_tms =
7.194 + let val ts = map (hol_term_from_metis mode ctxt) fol_tms
7.195 + val _ = trace_msg (fn () => " calling type inference:")
7.196 + val _ = app (fn t => trace_msg (fn () => Syntax.string_of_term ctxt t)) ts
7.197 + val ts' = ts |> map (reveal_skolem_terms skolems) |> infer_types ctxt
7.198 + val _ = app (fn t => trace_msg
7.199 + (fn () => " final term: " ^ Syntax.string_of_term ctxt t ^
7.200 + " of type " ^ Syntax.string_of_typ ctxt (type_of t)))
7.201 + ts'
7.202 + in ts' end;
7.203 +
7.204 +(* ------------------------------------------------------------------------- *)
7.205 +(* FOL step Inference Rules *)
7.206 +(* ------------------------------------------------------------------------- *)
7.207 +
7.208 +(*for debugging only*)
7.209 +(*
7.210 +fun print_thpair (fth,th) =
7.211 + (trace_msg (fn () => "=============================================");
7.212 + trace_msg (fn () => "Metis: " ^ Metis_Thm.toString fth);
7.213 + trace_msg (fn () => "Isabelle: " ^ Display.string_of_thm_without_context th));
7.214 +*)
7.215 +
7.216 +fun lookth thpairs (fth : Metis_Thm.thm) =
7.217 + the (AList.lookup (uncurry Metis_Thm.equal) thpairs fth)
7.218 + handle Option.Option =>
7.219 + raise Fail ("Failed to find Metis theorem " ^ Metis_Thm.toString fth)
7.220 +
7.221 +fun cterm_incr_types thy idx = cterm_of thy o (map_types (Logic.incr_tvar idx));
7.222 +
7.223 +(* INFERENCE RULE: AXIOM *)
7.224 +
7.225 +fun axiom_inf thpairs th = Thm.incr_indexes 1 (lookth thpairs th);
7.226 + (*This causes variables to have an index of 1 by default. SEE ALSO mk_var above.*)
7.227 +
7.228 +(* INFERENCE RULE: ASSUME *)
7.229 +
7.230 +val EXCLUDED_MIDDLE = @{lemma "P ==> ~ P ==> False" by (rule notE)}
7.231 +
7.232 +fun inst_excluded_middle thy i_atm =
7.233 + let val th = EXCLUDED_MIDDLE
7.234 + val [vx] = Term.add_vars (prop_of th) []
7.235 + val substs = [(cterm_of thy (Var vx), cterm_of thy i_atm)]
7.236 + in cterm_instantiate substs th end;
7.237 +
7.238 +fun assume_inf ctxt mode skolems atm =
7.239 + inst_excluded_middle
7.240 + (ProofContext.theory_of ctxt)
7.241 + (singleton (hol_terms_from_fol ctxt mode skolems) (Metis_Term.Fn atm))
7.242 +
7.243 +(* INFERENCE RULE: INSTANTIATE (SUBST). Type instantiations are ignored. Trying
7.244 + to reconstruct them admits new possibilities of errors, e.g. concerning
7.245 + sorts. Instead we try to arrange that new TVars are distinct and that types
7.246 + can be inferred from terms. *)
7.247 +
7.248 +fun inst_inf ctxt mode skolems thpairs fsubst th =
7.249 + let val thy = ProofContext.theory_of ctxt
7.250 + val i_th = lookth thpairs th
7.251 + val i_th_vars = Term.add_vars (prop_of i_th) []
7.252 + fun find_var x = the (List.find (fn ((a,_),_) => a=x) i_th_vars)
7.253 + fun subst_translation (x,y) =
7.254 + let val v = find_var x
7.255 + (* We call "reveal_skolem_terms" and "infer_types" below. *)
7.256 + val t = hol_term_from_metis mode ctxt y
7.257 + in SOME (cterm_of thy (Var v), t) end
7.258 + handle Option.Option =>
7.259 + (trace_msg (fn () => "\"find_var\" failed for " ^ x ^
7.260 + " in " ^ Display.string_of_thm ctxt i_th);
7.261 + NONE)
7.262 + | TYPE _ =>
7.263 + (trace_msg (fn () => "\"hol_term_from_metis\" failed for " ^ x ^
7.264 + " in " ^ Display.string_of_thm ctxt i_th);
7.265 + NONE)
7.266 + fun remove_typeinst (a, t) =
7.267 + case strip_prefix_and_unascii schematic_var_prefix a of
7.268 + SOME b => SOME (b, t)
7.269 + | NONE => case strip_prefix_and_unascii tvar_prefix a of
7.270 + SOME _ => NONE (*type instantiations are forbidden!*)
7.271 + | NONE => SOME (a,t) (*internal Metis var?*)
7.272 + val _ = trace_msg (fn () => " isa th: " ^ Display.string_of_thm ctxt i_th)
7.273 + val substs = map_filter remove_typeinst (Metis_Subst.toList fsubst)
7.274 + val (vars,rawtms) = ListPair.unzip (map_filter subst_translation substs)
7.275 + val tms = rawtms |> map (reveal_skolem_terms skolems) |> infer_types ctxt
7.276 + val ctm_of = cterm_incr_types thy (1 + Thm.maxidx_of i_th)
7.277 + val substs' = ListPair.zip (vars, map ctm_of tms)
7.278 + val _ = trace_msg (fn () =>
7.279 + cat_lines ("subst_translations:" ::
7.280 + (substs' |> map (fn (x, y) =>
7.281 + Syntax.string_of_term ctxt (term_of x) ^ " |-> " ^
7.282 + Syntax.string_of_term ctxt (term_of y)))));
7.283 + in cterm_instantiate substs' i_th end
7.284 + handle THM (msg, _, _) =>
7.285 + error ("Cannot replay Metis proof in Isabelle:\n" ^ msg)
7.286 +
7.287 +(* INFERENCE RULE: RESOLVE *)
7.288 +
7.289 +(* Like RSN, but we rename apart only the type variables. Vars here typically
7.290 + have an index of 1, and the use of RSN would increase this typically to 3.
7.291 + Instantiations of those Vars could then fail. See comment on "mk_var". *)
7.292 +fun resolve_inc_tyvars thy tha i thb =
7.293 + let
7.294 + val tha = Drule.incr_type_indexes (1 + Thm.maxidx_of thb) tha
7.295 + fun aux tha thb =
7.296 + case Thm.bicompose false (false, tha, nprems_of tha) i thb
7.297 + |> Seq.list_of |> distinct Thm.eq_thm of
7.298 + [th] => th
7.299 + | _ => raise THM ("resolve_inc_tyvars: unique result expected", i,
7.300 + [tha, thb])
7.301 + in
7.302 + aux tha thb
7.303 + handle TERM z =>
7.304 + (* The unifier, which is invoked from "Thm.bicompose", will sometimes
7.305 + refuse to unify "?a::?'a" with "?a::?'b" or "?a::nat" and throw a
7.306 + "TERM" exception (with "add_ffpair" as first argument). We then
7.307 + perform unification of the types of variables by hand and try
7.308 + again. We could do this the first time around but this error
7.309 + occurs seldom and we don't want to break existing proofs in subtle
7.310 + ways or slow them down needlessly. *)
7.311 + case [] |> fold (Term.add_vars o prop_of) [tha, thb]
7.312 + |> AList.group (op =)
7.313 + |> maps (fn ((s, _), T :: Ts) =>
7.314 + map (fn T' => (Free (s, T), Free (s, T'))) Ts)
7.315 + |> rpair (Envir.empty ~1)
7.316 + |-> fold (Pattern.unify thy)
7.317 + |> Envir.type_env |> Vartab.dest
7.318 + |> map (fn (x, (S, T)) =>
7.319 + pairself (ctyp_of thy) (TVar (x, S), T)) of
7.320 + [] => raise TERM z
7.321 + | ps => aux (instantiate (ps, []) tha) (instantiate (ps, []) thb)
7.322 + end
7.323 +
7.324 +fun mk_not (Const (@{const_name Not}, _) $ b) = b
7.325 + | mk_not b = HOLogic.mk_not b
7.326 +
7.327 +(* Match untyped terms. *)
7.328 +fun untyped_aconv (Const (a, _)) (Const(b, _)) = (a = b)
7.329 + | untyped_aconv (Free (a, _)) (Free (b, _)) = (a = b)
7.330 + | untyped_aconv (Var ((a, _), _)) (Var ((b, _), _)) =
7.331 + (a = b) (* The index is ignored, for some reason. *)
7.332 + | untyped_aconv (Bound i) (Bound j) = (i = j)
7.333 + | untyped_aconv (Abs (_, _, t)) (Abs (_, _, u)) = untyped_aconv t u
7.334 + | untyped_aconv (t1 $ t2) (u1 $ u2) =
7.335 + untyped_aconv t1 u1 andalso untyped_aconv t2 u2
7.336 + | untyped_aconv _ _ = false
7.337 +
7.338 +(* Finding the relative location of an untyped term within a list of terms *)
7.339 +fun literal_index lit =
7.340 + let
7.341 + val lit = Envir.eta_contract lit
7.342 + fun get _ [] = raise Empty
7.343 + | get n (x :: xs) =
7.344 + if untyped_aconv lit (Envir.eta_contract (HOLogic.dest_Trueprop x)) then
7.345 + n
7.346 + else
7.347 + get (n+1) xs
7.348 + in get 1 end
7.349 +
7.350 +fun resolve_inf ctxt mode skolems thpairs atm th1 th2 =
7.351 + let
7.352 + val thy = ProofContext.theory_of ctxt
7.353 + val i_th1 = lookth thpairs th1 and i_th2 = lookth thpairs th2
7.354 + val _ = trace_msg (fn () => " isa th1 (pos): " ^ Display.string_of_thm ctxt i_th1)
7.355 + val _ = trace_msg (fn () => " isa th2 (neg): " ^ Display.string_of_thm ctxt i_th2)
7.356 + in
7.357 + (* Trivial cases where one operand is type info *)
7.358 + if Thm.eq_thm (TrueI, i_th1) then
7.359 + i_th2
7.360 + else if Thm.eq_thm (TrueI, i_th2) then
7.361 + i_th1
7.362 + else
7.363 + let
7.364 + val i_atm = singleton (hol_terms_from_fol ctxt mode skolems)
7.365 + (Metis_Term.Fn atm)
7.366 + val _ = trace_msg (fn () => " atom: " ^ Syntax.string_of_term ctxt i_atm)
7.367 + val prems_th1 = prems_of i_th1
7.368 + val prems_th2 = prems_of i_th2
7.369 + val index_th1 = literal_index (mk_not i_atm) prems_th1
7.370 + handle Empty => raise Fail "Failed to find literal in th1"
7.371 + val _ = trace_msg (fn () => " index_th1: " ^ Int.toString index_th1)
7.372 + val index_th2 = literal_index i_atm prems_th2
7.373 + handle Empty => raise Fail "Failed to find literal in th2"
7.374 + val _ = trace_msg (fn () => " index_th2: " ^ Int.toString index_th2)
7.375 + in
7.376 + resolve_inc_tyvars thy (Meson.select_literal index_th1 i_th1) index_th2
7.377 + i_th2
7.378 + end
7.379 + end;
7.380 +
7.381 +(* INFERENCE RULE: REFL *)
7.382 +
7.383 +val REFL_THM = Thm.incr_indexes 2 @{lemma "t ~= t ==> False" by simp}
7.384 +
7.385 +val refl_x = cterm_of @{theory} (Var (hd (Term.add_vars (prop_of REFL_THM) [])));
7.386 +val refl_idx = 1 + Thm.maxidx_of REFL_THM;
7.387 +
7.388 +fun refl_inf ctxt mode skolems t =
7.389 + let val thy = ProofContext.theory_of ctxt
7.390 + val i_t = singleton (hol_terms_from_fol ctxt mode skolems) t
7.391 + val _ = trace_msg (fn () => " term: " ^ Syntax.string_of_term ctxt i_t)
7.392 + val c_t = cterm_incr_types thy refl_idx i_t
7.393 + in cterm_instantiate [(refl_x, c_t)] REFL_THM end;
7.394 +
7.395 +(* INFERENCE RULE: EQUALITY *)
7.396 +
7.397 +val subst_em = @{lemma "s = t ==> P s ==> ~ P t ==> False" by simp}
7.398 +val ssubst_em = @{lemma "s = t ==> P t ==> ~ P s ==> False" by simp}
7.399 +
7.400 +val metis_eq = Metis_Term.Fn ("=", []);
7.401 +
7.402 +fun get_ty_arg_size _ (Const (@{const_name HOL.eq}, _)) = 0 (*equality has no type arguments*)
7.403 + | get_ty_arg_size thy (Const (c, _)) = (num_type_args thy c handle TYPE _ => 0)
7.404 + | get_ty_arg_size _ _ = 0;
7.405 +
7.406 +fun equality_inf ctxt mode skolems (pos, atm) fp fr =
7.407 + let val thy = ProofContext.theory_of ctxt
7.408 + val m_tm = Metis_Term.Fn atm
7.409 + val [i_atm,i_tm] = hol_terms_from_fol ctxt mode skolems [m_tm, fr]
7.410 + val _ = trace_msg (fn () => "sign of the literal: " ^ Bool.toString pos)
7.411 + fun replace_item_list lx 0 (_::ls) = lx::ls
7.412 + | replace_item_list lx i (l::ls) = l :: replace_item_list lx (i-1) ls
7.413 + fun path_finder_FO tm [] = (tm, Bound 0)
7.414 + | path_finder_FO tm (p::ps) =
7.415 + let val (tm1,args) = strip_comb tm
7.416 + val adjustment = get_ty_arg_size thy tm1
7.417 + val p' = if adjustment > p then p else p-adjustment
7.418 + val tm_p = List.nth(args,p')
7.419 + handle Subscript =>
7.420 + error ("Cannot replay Metis proof in Isabelle:\n" ^
7.421 + "equality_inf: " ^ Int.toString p ^ " adj " ^
7.422 + Int.toString adjustment ^ " term " ^
7.423 + Syntax.string_of_term ctxt tm)
7.424 + val _ = trace_msg (fn () => "path_finder: " ^ Int.toString p ^
7.425 + " " ^ Syntax.string_of_term ctxt tm_p)
7.426 + val (r,t) = path_finder_FO tm_p ps
7.427 + in
7.428 + (r, list_comb (tm1, replace_item_list t p' args))
7.429 + end
7.430 + fun path_finder_HO tm [] = (tm, Bound 0)
7.431 + | path_finder_HO (t$u) (0::ps) = (fn(x,y) => (x, y$u)) (path_finder_HO t ps)
7.432 + | path_finder_HO (t$u) (_::ps) = (fn(x,y) => (x, t$y)) (path_finder_HO u ps)
7.433 + | path_finder_HO tm ps =
7.434 + raise Fail ("Cannot replay Metis proof in Isabelle:\n" ^
7.435 + "equality_inf, path_finder_HO: path = " ^
7.436 + space_implode " " (map Int.toString ps) ^
7.437 + " isa-term: " ^ Syntax.string_of_term ctxt tm)
7.438 + fun path_finder_FT tm [] _ = (tm, Bound 0)
7.439 + | path_finder_FT tm (0::ps) (Metis_Term.Fn ("ti", [t1, _])) =
7.440 + path_finder_FT tm ps t1
7.441 + | path_finder_FT (t$u) (0::ps) (Metis_Term.Fn (".", [t1, _])) =
7.442 + (fn(x,y) => (x, y$u)) (path_finder_FT t ps t1)
7.443 + | path_finder_FT (t$u) (1::ps) (Metis_Term.Fn (".", [_, t2])) =
7.444 + (fn(x,y) => (x, t$y)) (path_finder_FT u ps t2)
7.445 + | path_finder_FT tm ps t =
7.446 + raise Fail ("Cannot replay Metis proof in Isabelle:\n" ^
7.447 + "equality_inf, path_finder_FT: path = " ^
7.448 + space_implode " " (map Int.toString ps) ^
7.449 + " isa-term: " ^ Syntax.string_of_term ctxt tm ^
7.450 + " fol-term: " ^ Metis_Term.toString t)
7.451 + fun path_finder FO tm ps _ = path_finder_FO tm ps
7.452 + | path_finder HO (tm as Const(@{const_name HOL.eq},_) $ _ $ _) (p::ps) _ =
7.453 + (*equality: not curried, as other predicates are*)
7.454 + if p=0 then path_finder_HO tm (0::1::ps) (*select first operand*)
7.455 + else path_finder_HO tm (p::ps) (*1 selects second operand*)
7.456 + | path_finder HO tm (_ :: ps) (Metis_Term.Fn ("{}", [_])) =
7.457 + path_finder_HO tm ps (*if not equality, ignore head to skip hBOOL*)
7.458 + | path_finder FT (tm as Const(@{const_name HOL.eq}, _) $ _ $ _) (p::ps)
7.459 + (Metis_Term.Fn ("=", [t1,t2])) =
7.460 + (*equality: not curried, as other predicates are*)
7.461 + if p=0 then path_finder_FT tm (0::1::ps)
7.462 + (Metis_Term.Fn (".", [Metis_Term.Fn (".", [metis_eq,t1]), t2]))
7.463 + (*select first operand*)
7.464 + else path_finder_FT tm (p::ps)
7.465 + (Metis_Term.Fn (".", [metis_eq,t2]))
7.466 + (*1 selects second operand*)
7.467 + | path_finder FT tm (_ :: ps) (Metis_Term.Fn ("{}", [t1])) = path_finder_FT tm ps t1
7.468 + (*if not equality, ignore head to skip the hBOOL predicate*)
7.469 + | path_finder FT tm ps t = path_finder_FT tm ps t (*really an error case!*)
7.470 + fun path_finder_lit ((nt as Const (@{const_name Not}, _)) $ tm_a) idx =
7.471 + let val (tm, tm_rslt) = path_finder mode tm_a idx m_tm
7.472 + in (tm, nt $ tm_rslt) end
7.473 + | path_finder_lit tm_a idx = path_finder mode tm_a idx m_tm
7.474 + val (tm_subst, body) = path_finder_lit i_atm fp
7.475 + val tm_abs = Abs ("x", type_of tm_subst, body)
7.476 + val _ = trace_msg (fn () => "abstraction: " ^ Syntax.string_of_term ctxt tm_abs)
7.477 + val _ = trace_msg (fn () => "i_tm: " ^ Syntax.string_of_term ctxt i_tm)
7.478 + val _ = trace_msg (fn () => "located term: " ^ Syntax.string_of_term ctxt tm_subst)
7.479 + val imax = maxidx_of_term (i_tm $ tm_abs $ tm_subst) (*ill typed but gives right max*)
7.480 + val subst' = Thm.incr_indexes (imax+1) (if pos then subst_em else ssubst_em)
7.481 + val _ = trace_msg (fn () => "subst' " ^ Display.string_of_thm ctxt subst')
7.482 + val eq_terms = map (pairself (cterm_of thy))
7.483 + (ListPair.zip (OldTerm.term_vars (prop_of subst'), [tm_abs, tm_subst, i_tm]))
7.484 + in cterm_instantiate eq_terms subst' end;
7.485 +
7.486 +val factor = Seq.hd o distinct_subgoals_tac;
7.487 +
7.488 +fun step ctxt mode skolems thpairs p =
7.489 + case p of
7.490 + (fol_th, Metis_Proof.Axiom _) => factor (axiom_inf thpairs fol_th)
7.491 + | (_, Metis_Proof.Assume f_atm) => assume_inf ctxt mode skolems f_atm
7.492 + | (_, Metis_Proof.Metis_Subst (f_subst, f_th1)) =>
7.493 + factor (inst_inf ctxt mode skolems thpairs f_subst f_th1)
7.494 + | (_, Metis_Proof.Resolve(f_atm, f_th1, f_th2)) =>
7.495 + factor (resolve_inf ctxt mode skolems thpairs f_atm f_th1 f_th2)
7.496 + | (_, Metis_Proof.Refl f_tm) => refl_inf ctxt mode skolems f_tm
7.497 + | (_, Metis_Proof.Equality (f_lit, f_p, f_r)) =>
7.498 + equality_inf ctxt mode skolems f_lit f_p f_r
7.499 +
7.500 +fun is_real_literal (_, (c, _)) = not (String.isPrefix class_prefix c)
7.501 +
7.502 +fun replay_one_inference ctxt mode skolems (fol_th, inf) thpairs =
7.503 + let
7.504 + val _ = trace_msg (fn () => "=============================================")
7.505 + val _ = trace_msg (fn () => "METIS THM: " ^ Metis_Thm.toString fol_th)
7.506 + val _ = trace_msg (fn () => "INFERENCE: " ^ Metis_Proof.inferenceToString inf)
7.507 + val th = Meson.flexflex_first_order (step ctxt mode skolems
7.508 + thpairs (fol_th, inf))
7.509 + val _ = trace_msg (fn () => "ISABELLE THM: " ^ Display.string_of_thm ctxt th)
7.510 + val _ = trace_msg (fn () => "=============================================")
7.511 + val n_metis_lits =
7.512 + length (filter is_real_literal (Metis_LiteralSet.toList (Metis_Thm.clause fol_th)))
7.513 + val _ = if nprems_of th = n_metis_lits then ()
7.514 + else error "Cannot replay Metis proof in Isabelle: Out of sync."
7.515 + in (fol_th, th) :: thpairs end
7.516 +
7.517 +end;
8.1 --- a/src/HOL/Tools/Sledgehammer/metis_tactics.ML Fri Sep 17 16:15:45 2010 +0200
8.2 +++ b/src/HOL/Tools/Sledgehammer/metis_tactics.ML Fri Sep 17 16:38:11 2010 +0200
8.3 @@ -9,733 +9,34 @@
8.4
8.5 signature METIS_TACTICS =
8.6 sig
8.7 - val trace: bool Unsynchronized.ref
8.8 - val type_lits: bool Config.T
8.9 - val metis_tac: Proof.context -> thm list -> int -> tactic
8.10 - val metisF_tac: Proof.context -> thm list -> int -> tactic
8.11 - val metisFT_tac: Proof.context -> thm list -> int -> tactic
8.12 - val setup: theory -> theory
8.13 + val trace : bool Unsynchronized.ref
8.14 + val type_lits : bool Config.T
8.15 + val metis_tac : Proof.context -> thm list -> int -> tactic
8.16 + val metisF_tac : Proof.context -> thm list -> int -> tactic
8.17 + val metisFT_tac : Proof.context -> thm list -> int -> tactic
8.18 + val setup : theory -> theory
8.19 end
8.20
8.21 structure Metis_Tactics : METIS_TACTICS =
8.22 struct
8.23
8.24 -open Metis_Clauses
8.25 +open Metis_Translate
8.26 +open Metis_Reconstruct
8.27
8.28 -val trace = Unsynchronized.ref false;
8.29 -fun trace_msg msg = if !trace then tracing (msg ()) else ();
8.30 +val trace = Unsynchronized.ref false
8.31 +fun trace_msg msg = if !trace then tracing (msg ()) else ()
8.32
8.33 val (type_lits, type_lits_setup) = Attrib.config_bool "metis_type_lits" (K true);
8.34
8.35 -datatype mode = FO | HO | FT (* first-order, higher-order, fully-typed *)
8.36 +fun is_false t = t aconv (HOLogic.mk_Trueprop HOLogic.false_const);
8.37
8.38 -(* ------------------------------------------------------------------------- *)
8.39 -(* Useful Theorems *)
8.40 -(* ------------------------------------------------------------------------- *)
8.41 -val EXCLUDED_MIDDLE = @{lemma "P ==> ~ P ==> False" by (rule notE)}
8.42 -val REFL_THM = Thm.incr_indexes 2 @{lemma "t ~= t ==> False" by simp}
8.43 -val subst_em = @{lemma "s = t ==> P s ==> ~ P t ==> False" by simp}
8.44 -val ssubst_em = @{lemma "s = t ==> P t ==> ~ P s ==> False" by simp}
8.45 -
8.46 -(* ------------------------------------------------------------------------- *)
8.47 -(* Useful Functions *)
8.48 -(* ------------------------------------------------------------------------- *)
8.49 -
8.50 -(* Match untyped terms. *)
8.51 -fun untyped_aconv (Const (a, _)) (Const(b, _)) = (a = b)
8.52 - | untyped_aconv (Free (a, _)) (Free (b, _)) = (a = b)
8.53 - | untyped_aconv (Var ((a, _), _)) (Var ((b, _), _)) =
8.54 - (a = b) (* The index is ignored, for some reason. *)
8.55 - | untyped_aconv (Bound i) (Bound j) = (i = j)
8.56 - | untyped_aconv (Abs (_, _, t)) (Abs (_, _, u)) = untyped_aconv t u
8.57 - | untyped_aconv (t1 $ t2) (u1 $ u2) =
8.58 - untyped_aconv t1 u1 andalso untyped_aconv t2 u2
8.59 - | untyped_aconv _ _ = false
8.60 -
8.61 -(* Finding the relative location of an untyped term within a list of terms *)
8.62 -fun get_index lit =
8.63 - let val lit = Envir.eta_contract lit
8.64 - fun get _ [] = raise Empty
8.65 - | get n (x::xs) = if untyped_aconv lit (Envir.eta_contract (HOLogic.dest_Trueprop x))
8.66 - then n else get (n+1) xs
8.67 - in get 1 end;
8.68 -
8.69 -(* ------------------------------------------------------------------------- *)
8.70 -(* HOL to FOL (Isabelle to Metis) *)
8.71 -(* ------------------------------------------------------------------------- *)
8.72 -
8.73 -fun fn_isa_to_met_sublevel "equal" = "=" (* FIXME: "c_fequal" *)
8.74 - | fn_isa_to_met_sublevel x = x
8.75 -fun fn_isa_to_met_toplevel "equal" = "="
8.76 - | fn_isa_to_met_toplevel x = x
8.77 -
8.78 -fun metis_lit b c args = (b, (c, args));
8.79 -
8.80 -fun metis_term_from_combtyp (CombTVar (s, _)) = Metis_Term.Var s
8.81 - | metis_term_from_combtyp (CombTFree (s, _)) = Metis_Term.Fn (s, [])
8.82 - | metis_term_from_combtyp (CombType ((s, _), tps)) =
8.83 - Metis_Term.Fn (s, map metis_term_from_combtyp tps);
8.84 -
8.85 -(*These two functions insert type literals before the real literals. That is the
8.86 - opposite order from TPTP linkup, but maybe OK.*)
8.87 -
8.88 -fun hol_term_to_fol_FO tm =
8.89 - case strip_combterm_comb tm of
8.90 - (CombConst ((c, _), _, tys), tms) =>
8.91 - let val tyargs = map metis_term_from_combtyp tys
8.92 - val args = map hol_term_to_fol_FO tms
8.93 - in Metis_Term.Fn (c, tyargs @ args) end
8.94 - | (CombVar ((v, _), _), []) => Metis_Term.Var v
8.95 - | _ => raise Fail "non-first-order combterm"
8.96 -
8.97 -fun hol_term_to_fol_HO (CombConst ((a, _), _, tylist)) =
8.98 - Metis_Term.Fn (fn_isa_to_met_sublevel a, map metis_term_from_combtyp tylist)
8.99 - | hol_term_to_fol_HO (CombVar ((s, _), _)) = Metis_Term.Var s
8.100 - | hol_term_to_fol_HO (CombApp (tm1, tm2)) =
8.101 - Metis_Term.Fn (".", map hol_term_to_fol_HO [tm1, tm2]);
8.102 -
8.103 -(*The fully-typed translation, to avoid type errors*)
8.104 -fun wrap_type (tm, ty) = Metis_Term.Fn("ti", [tm, metis_term_from_combtyp ty]);
8.105 -
8.106 -fun hol_term_to_fol_FT (CombVar ((s, _), ty)) = wrap_type (Metis_Term.Var s, ty)
8.107 - | hol_term_to_fol_FT (CombConst((a, _), ty, _)) =
8.108 - wrap_type (Metis_Term.Fn(fn_isa_to_met_sublevel a, []), ty)
8.109 - | hol_term_to_fol_FT (tm as CombApp(tm1,tm2)) =
8.110 - wrap_type (Metis_Term.Fn(".", map hol_term_to_fol_FT [tm1,tm2]),
8.111 - combtyp_of tm)
8.112 -
8.113 -fun hol_literal_to_fol FO (FOLLiteral (pos, tm)) =
8.114 - let val (CombConst((p, _), _, tys), tms) = strip_combterm_comb tm
8.115 - val tylits = if p = "equal" then [] else map metis_term_from_combtyp tys
8.116 - val lits = map hol_term_to_fol_FO tms
8.117 - in metis_lit pos (fn_isa_to_met_toplevel p) (tylits @ lits) end
8.118 - | hol_literal_to_fol HO (FOLLiteral (pos, tm)) =
8.119 - (case strip_combterm_comb tm of
8.120 - (CombConst(("equal", _), _, _), tms) =>
8.121 - metis_lit pos "=" (map hol_term_to_fol_HO tms)
8.122 - | _ => metis_lit pos "{}" [hol_term_to_fol_HO tm]) (*hBOOL*)
8.123 - | hol_literal_to_fol FT (FOLLiteral (pos, tm)) =
8.124 - (case strip_combterm_comb tm of
8.125 - (CombConst(("equal", _), _, _), tms) =>
8.126 - metis_lit pos "=" (map hol_term_to_fol_FT tms)
8.127 - | _ => metis_lit pos "{}" [hol_term_to_fol_FT tm]) (*hBOOL*);
8.128 -
8.129 -fun literals_of_hol_term thy mode t =
8.130 - let val (lits, types_sorts) = literals_of_term thy t
8.131 - in (map (hol_literal_to_fol mode) lits, types_sorts) end;
8.132 -
8.133 -(*Sign should be "true" for conjecture type constraints, "false" for type lits in clauses.*)
8.134 -fun metis_of_type_literals pos (TyLitVar ((s, _), (s', _))) =
8.135 - metis_lit pos s [Metis_Term.Var s']
8.136 - | metis_of_type_literals pos (TyLitFree ((s, _), (s', _))) =
8.137 - metis_lit pos s [Metis_Term.Fn (s',[])]
8.138 -
8.139 -fun default_sort _ (TVar _) = false
8.140 - | default_sort ctxt (TFree (x, s)) = (s = the_default [] (Variable.def_sort ctxt (x, ~1)));
8.141 -
8.142 -fun metis_of_tfree tf =
8.143 - Metis_Thm.axiom (Metis_LiteralSet.singleton (metis_of_type_literals true tf));
8.144 -
8.145 -fun hol_thm_to_fol is_conjecture ctxt mode j skolems th =
8.146 - let
8.147 - val thy = ProofContext.theory_of ctxt
8.148 - val (skolems, (mlits, types_sorts)) =
8.149 - th |> prop_of |> conceal_skolem_terms j skolems
8.150 - ||> (HOLogic.dest_Trueprop #> literals_of_hol_term thy mode)
8.151 - in
8.152 - if is_conjecture then
8.153 - (Metis_Thm.axiom (Metis_LiteralSet.fromList mlits),
8.154 - type_literals_for_types types_sorts, skolems)
8.155 - else
8.156 - let val tylits = filter_out (default_sort ctxt) types_sorts
8.157 - |> type_literals_for_types
8.158 - val mtylits = if Config.get ctxt type_lits
8.159 - then map (metis_of_type_literals false) tylits else []
8.160 - in
8.161 - (Metis_Thm.axiom (Metis_LiteralSet.fromList(mtylits @ mlits)), [],
8.162 - skolems)
8.163 - end
8.164 - end;
8.165 -
8.166 -(* ARITY CLAUSE *)
8.167 -
8.168 -fun m_arity_cls (TConsLit ((c, _), (t, _), args)) =
8.169 - metis_lit true c [Metis_Term.Fn(t, map (Metis_Term.Var o fst) args)]
8.170 - | m_arity_cls (TVarLit ((c, _), (s, _))) =
8.171 - metis_lit false c [Metis_Term.Var s]
8.172 -
8.173 -(*TrueI is returned as the Isabelle counterpart because there isn't any.*)
8.174 -fun arity_cls (ArityClause {conclLit, premLits, ...}) =
8.175 - (TrueI,
8.176 - Metis_Thm.axiom (Metis_LiteralSet.fromList (map m_arity_cls (conclLit :: premLits))));
8.177 -
8.178 -(* CLASSREL CLAUSE *)
8.179 -
8.180 -fun m_class_rel_cls (subclass, _) (superclass, _) =
8.181 - [metis_lit false subclass [Metis_Term.Var "T"], metis_lit true superclass [Metis_Term.Var "T"]];
8.182 -
8.183 -fun class_rel_cls (ClassRelClause {subclass, superclass, ...}) =
8.184 - (TrueI, Metis_Thm.axiom (Metis_LiteralSet.fromList (m_class_rel_cls subclass superclass)));
8.185 -
8.186 -(* ------------------------------------------------------------------------- *)
8.187 -(* FOL to HOL (Metis to Isabelle) *)
8.188 -(* ------------------------------------------------------------------------- *)
8.189 -
8.190 -datatype term_or_type = Term of Term.term | Type of Term.typ;
8.191 -
8.192 -fun terms_of [] = []
8.193 - | terms_of (Term t :: tts) = t :: terms_of tts
8.194 - | terms_of (Type _ :: tts) = terms_of tts;
8.195 -
8.196 -fun types_of [] = []
8.197 - | types_of (Term (Term.Var ((a,idx), _)) :: tts) =
8.198 - if String.isPrefix "_" a then
8.199 - (*Variable generated by Metis, which might have been a type variable.*)
8.200 - TVar (("'" ^ a, idx), HOLogic.typeS) :: types_of tts
8.201 - else types_of tts
8.202 - | types_of (Term _ :: tts) = types_of tts
8.203 - | types_of (Type T :: tts) = T :: types_of tts;
8.204 -
8.205 -fun apply_list rator nargs rands =
8.206 - let val trands = terms_of rands
8.207 - in if length trands = nargs then Term (list_comb(rator, trands))
8.208 - else raise Fail
8.209 - ("apply_list: wrong number of arguments: " ^ Syntax.string_of_term_global Pure.thy rator ^
8.210 - " expected " ^ Int.toString nargs ^
8.211 - " received " ^ commas (map (Syntax.string_of_term_global Pure.thy) trands))
8.212 - end;
8.213 -
8.214 -fun infer_types ctxt =
8.215 - Syntax.check_terms (ProofContext.set_mode ProofContext.mode_pattern ctxt);
8.216 -
8.217 -(*We use 1 rather than 0 because variable references in clauses may otherwise conflict
8.218 - with variable constraints in the goal...at least, type inference often fails otherwise.
8.219 - SEE ALSO axiom_inf below.*)
8.220 -fun mk_var (w,T) = Term.Var((w,1), T);
8.221 -
8.222 -(*include the default sort, if available*)
8.223 -fun mk_tfree ctxt w =
8.224 - let val ww = "'" ^ w
8.225 - in TFree(ww, the_default HOLogic.typeS (Variable.def_sort ctxt (ww, ~1))) end;
8.226 -
8.227 -(*Remove the "apply" operator from an HO term*)
8.228 -fun strip_happ args (Metis_Term.Fn(".",[t,u])) = strip_happ (u::args) t
8.229 - | strip_happ args x = (x, args);
8.230 -
8.231 -fun make_tvar s = TVar (("'" ^ s, 0), HOLogic.typeS)
8.232 -
8.233 -fun smart_invert_const "fequal" = @{const_name HOL.eq}
8.234 - | smart_invert_const s = invert_const s
8.235 -
8.236 -fun hol_type_from_metis_term _ (Metis_Term.Var v) =
8.237 - (case strip_prefix_and_unascii tvar_prefix v of
8.238 - SOME w => make_tvar w
8.239 - | NONE => make_tvar v)
8.240 - | hol_type_from_metis_term ctxt (Metis_Term.Fn(x, tys)) =
8.241 - (case strip_prefix_and_unascii type_const_prefix x of
8.242 - SOME tc => Term.Type (smart_invert_const tc,
8.243 - map (hol_type_from_metis_term ctxt) tys)
8.244 - | NONE =>
8.245 - case strip_prefix_and_unascii tfree_prefix x of
8.246 - SOME tf => mk_tfree ctxt tf
8.247 - | NONE => raise Fail ("hol_type_from_metis_term: " ^ x));
8.248 -
8.249 -(*Maps metis terms to isabelle terms*)
8.250 -fun hol_term_from_metis_PT ctxt fol_tm =
8.251 - let val thy = ProofContext.theory_of ctxt
8.252 - val _ = trace_msg (fn () => "hol_term_from_metis_PT: " ^
8.253 - Metis_Term.toString fol_tm)
8.254 - fun tm_to_tt (Metis_Term.Var v) =
8.255 - (case strip_prefix_and_unascii tvar_prefix v of
8.256 - SOME w => Type (make_tvar w)
8.257 - | NONE =>
8.258 - case strip_prefix_and_unascii schematic_var_prefix v of
8.259 - SOME w => Term (mk_var (w, HOLogic.typeT))
8.260 - | NONE => Term (mk_var (v, HOLogic.typeT)) )
8.261 - (*Var from Metis with a name like _nnn; possibly a type variable*)
8.262 - | tm_to_tt (Metis_Term.Fn ("{}", [arg])) = tm_to_tt arg (*hBOOL*)
8.263 - | tm_to_tt (t as Metis_Term.Fn (".",_)) =
8.264 - let val (rator,rands) = strip_happ [] t
8.265 - in case rator of
8.266 - Metis_Term.Fn(fname,ts) => applic_to_tt (fname, ts @ rands)
8.267 - | _ => case tm_to_tt rator of
8.268 - Term t => Term (list_comb(t, terms_of (map tm_to_tt rands)))
8.269 - | _ => raise Fail "tm_to_tt: HO application"
8.270 - end
8.271 - | tm_to_tt (Metis_Term.Fn (fname, args)) = applic_to_tt (fname,args)
8.272 - and applic_to_tt ("=",ts) =
8.273 - Term (list_comb(Const (@{const_name HOL.eq}, HOLogic.typeT), terms_of (map tm_to_tt ts)))
8.274 - | applic_to_tt (a,ts) =
8.275 - case strip_prefix_and_unascii const_prefix a of
8.276 - SOME b =>
8.277 - let val c = smart_invert_const b
8.278 - val ntypes = num_type_args thy c
8.279 - val nterms = length ts - ntypes
8.280 - val tts = map tm_to_tt ts
8.281 - val tys = types_of (List.take(tts,ntypes))
8.282 - in if length tys = ntypes then
8.283 - apply_list (Const (c, dummyT)) nterms (List.drop(tts,ntypes))
8.284 - else
8.285 - raise Fail ("Constant " ^ c ^ " expects " ^ Int.toString ntypes ^
8.286 - " but gets " ^ Int.toString (length tys) ^
8.287 - " type arguments\n" ^
8.288 - cat_lines (map (Syntax.string_of_typ ctxt) tys) ^
8.289 - " the terms are \n" ^
8.290 - cat_lines (map (Syntax.string_of_term ctxt) (terms_of tts)))
8.291 - end
8.292 - | NONE => (*Not a constant. Is it a type constructor?*)
8.293 - case strip_prefix_and_unascii type_const_prefix a of
8.294 - SOME b =>
8.295 - Type (Term.Type (smart_invert_const b, types_of (map tm_to_tt ts)))
8.296 - | NONE => (*Maybe a TFree. Should then check that ts=[].*)
8.297 - case strip_prefix_and_unascii tfree_prefix a of
8.298 - SOME b => Type (mk_tfree ctxt b)
8.299 - | NONE => (*a fixed variable? They are Skolem functions.*)
8.300 - case strip_prefix_and_unascii fixed_var_prefix a of
8.301 - SOME b =>
8.302 - let val opr = Term.Free(b, HOLogic.typeT)
8.303 - in apply_list opr (length ts) (map tm_to_tt ts) end
8.304 - | NONE => raise Fail ("unexpected metis function: " ^ a)
8.305 - in
8.306 - case tm_to_tt fol_tm of
8.307 - Term t => t
8.308 - | _ => raise Fail "fol_tm_to_tt: Term expected"
8.309 - end
8.310 -
8.311 -(*Maps fully-typed metis terms to isabelle terms*)
8.312 -fun hol_term_from_metis_FT ctxt fol_tm =
8.313 - let val _ = trace_msg (fn () => "hol_term_from_metis_FT: " ^
8.314 - Metis_Term.toString fol_tm)
8.315 - fun cvt (Metis_Term.Fn ("ti", [Metis_Term.Var v, _])) =
8.316 - (case strip_prefix_and_unascii schematic_var_prefix v of
8.317 - SOME w => mk_var(w, dummyT)
8.318 - | NONE => mk_var(v, dummyT))
8.319 - | cvt (Metis_Term.Fn ("ti", [Metis_Term.Fn ("=",[]), _])) =
8.320 - Const (@{const_name HOL.eq}, HOLogic.typeT)
8.321 - | cvt (Metis_Term.Fn ("ti", [Metis_Term.Fn (x,[]), ty])) =
8.322 - (case strip_prefix_and_unascii const_prefix x of
8.323 - SOME c => Const (smart_invert_const c, dummyT)
8.324 - | NONE => (*Not a constant. Is it a fixed variable??*)
8.325 - case strip_prefix_and_unascii fixed_var_prefix x of
8.326 - SOME v => Free (v, hol_type_from_metis_term ctxt ty)
8.327 - | NONE => raise Fail ("hol_term_from_metis_FT bad constant: " ^ x))
8.328 - | cvt (Metis_Term.Fn ("ti", [Metis_Term.Fn (".",[tm1,tm2]), _])) =
8.329 - cvt tm1 $ cvt tm2
8.330 - | cvt (Metis_Term.Fn (".",[tm1,tm2])) = (*untyped application*)
8.331 - cvt tm1 $ cvt tm2
8.332 - | cvt (Metis_Term.Fn ("{}", [arg])) = cvt arg (*hBOOL*)
8.333 - | cvt (Metis_Term.Fn ("=", [tm1,tm2])) =
8.334 - list_comb(Const (@{const_name HOL.eq}, HOLogic.typeT), map cvt [tm1,tm2])
8.335 - | cvt (t as Metis_Term.Fn (x, [])) =
8.336 - (case strip_prefix_and_unascii const_prefix x of
8.337 - SOME c => Const (smart_invert_const c, dummyT)
8.338 - | NONE => (*Not a constant. Is it a fixed variable??*)
8.339 - case strip_prefix_and_unascii fixed_var_prefix x of
8.340 - SOME v => Free (v, dummyT)
8.341 - | NONE => (trace_msg (fn () => "hol_term_from_metis_FT bad const: " ^ x);
8.342 - hol_term_from_metis_PT ctxt t))
8.343 - | cvt t = (trace_msg (fn () => "hol_term_from_metis_FT bad term: " ^ Metis_Term.toString t);
8.344 - hol_term_from_metis_PT ctxt t)
8.345 - in fol_tm |> cvt end
8.346 -
8.347 -fun hol_term_from_metis FT = hol_term_from_metis_FT
8.348 - | hol_term_from_metis _ = hol_term_from_metis_PT
8.349 -
8.350 -fun hol_terms_from_fol ctxt mode skolems fol_tms =
8.351 - let val ts = map (hol_term_from_metis mode ctxt) fol_tms
8.352 - val _ = trace_msg (fn () => " calling type inference:")
8.353 - val _ = app (fn t => trace_msg (fn () => Syntax.string_of_term ctxt t)) ts
8.354 - val ts' = ts |> map (reveal_skolem_terms skolems) |> infer_types ctxt
8.355 - val _ = app (fn t => trace_msg
8.356 - (fn () => " final term: " ^ Syntax.string_of_term ctxt t ^
8.357 - " of type " ^ Syntax.string_of_typ ctxt (type_of t)))
8.358 - ts'
8.359 - in ts' end;
8.360 -
8.361 -fun mk_not (Const (@{const_name Not}, _) $ b) = b
8.362 - | mk_not b = HOLogic.mk_not b;
8.363 -
8.364 -val metis_eq = Metis_Term.Fn ("=", []);
8.365 -
8.366 -(* ------------------------------------------------------------------------- *)
8.367 -(* FOL step Inference Rules *)
8.368 -(* ------------------------------------------------------------------------- *)
8.369 -
8.370 -(*for debugging only*)
8.371 -(*
8.372 -fun print_thpair (fth,th) =
8.373 - (trace_msg (fn () => "=============================================");
8.374 - trace_msg (fn () => "Metis: " ^ Metis_Thm.toString fth);
8.375 - trace_msg (fn () => "Isabelle: " ^ Display.string_of_thm_without_context th));
8.376 -*)
8.377 -
8.378 -fun lookth thpairs (fth : Metis_Thm.thm) =
8.379 - the (AList.lookup (uncurry Metis_Thm.equal) thpairs fth)
8.380 - handle Option =>
8.381 - raise Fail ("Failed to find a Metis theorem " ^ Metis_Thm.toString fth);
8.382 -
8.383 -fun is_TrueI th = Thm.eq_thm(TrueI,th);
8.384 -
8.385 -fun cterm_incr_types thy idx = cterm_of thy o (map_types (Logic.incr_tvar idx));
8.386 -
8.387 -fun inst_excluded_middle thy i_atm =
8.388 - let val th = EXCLUDED_MIDDLE
8.389 - val [vx] = Term.add_vars (prop_of th) []
8.390 - val substs = [(cterm_of thy (Var vx), cterm_of thy i_atm)]
8.391 - in cterm_instantiate substs th end;
8.392 -
8.393 -(* INFERENCE RULE: AXIOM *)
8.394 -fun axiom_inf thpairs th = Thm.incr_indexes 1 (lookth thpairs th);
8.395 - (*This causes variables to have an index of 1 by default. SEE ALSO mk_var above.*)
8.396 -
8.397 -(* INFERENCE RULE: ASSUME *)
8.398 -fun assume_inf ctxt mode skolems atm =
8.399 - inst_excluded_middle
8.400 - (ProofContext.theory_of ctxt)
8.401 - (singleton (hol_terms_from_fol ctxt mode skolems) (Metis_Term.Fn atm))
8.402 -
8.403 -(* INFERENCE RULE: INSTANTIATE (Subst). Type instantiations are ignored. Trying to reconstruct
8.404 - them admits new possibilities of errors, e.g. concerning sorts. Instead we try to arrange
8.405 - that new TVars are distinct and that types can be inferred from terms.*)
8.406 -fun inst_inf ctxt mode skolems thpairs fsubst th =
8.407 - let val thy = ProofContext.theory_of ctxt
8.408 - val i_th = lookth thpairs th
8.409 - val i_th_vars = Term.add_vars (prop_of i_th) []
8.410 - fun find_var x = the (List.find (fn ((a,_),_) => a=x) i_th_vars)
8.411 - fun subst_translation (x,y) =
8.412 - let val v = find_var x
8.413 - (* We call "reveal_skolem_terms" and "infer_types" below. *)
8.414 - val t = hol_term_from_metis mode ctxt y
8.415 - in SOME (cterm_of thy (Var v), t) end
8.416 - handle Option =>
8.417 - (trace_msg (fn() => "\"find_var\" failed for the variable " ^ x ^
8.418 - " in " ^ Display.string_of_thm ctxt i_th);
8.419 - NONE)
8.420 - fun remove_typeinst (a, t) =
8.421 - case strip_prefix_and_unascii schematic_var_prefix a of
8.422 - SOME b => SOME (b, t)
8.423 - | NONE => case strip_prefix_and_unascii tvar_prefix a of
8.424 - SOME _ => NONE (*type instantiations are forbidden!*)
8.425 - | NONE => SOME (a,t) (*internal Metis var?*)
8.426 - val _ = trace_msg (fn () => " isa th: " ^ Display.string_of_thm ctxt i_th)
8.427 - val substs = map_filter remove_typeinst (Metis_Subst.toList fsubst)
8.428 - val (vars,rawtms) = ListPair.unzip (map_filter subst_translation substs)
8.429 - val tms = rawtms |> map (reveal_skolem_terms skolems) |> infer_types ctxt
8.430 - val ctm_of = cterm_incr_types thy (1 + Thm.maxidx_of i_th)
8.431 - val substs' = ListPair.zip (vars, map ctm_of tms)
8.432 - val _ = trace_msg (fn () =>
8.433 - cat_lines ("subst_translations:" ::
8.434 - (substs' |> map (fn (x, y) =>
8.435 - Syntax.string_of_term ctxt (term_of x) ^ " |-> " ^
8.436 - Syntax.string_of_term ctxt (term_of y)))));
8.437 - in cterm_instantiate substs' i_th end
8.438 - handle THM (msg, _, _) =>
8.439 - error ("Cannot replay Metis proof in Isabelle:\n" ^ msg)
8.440 -
8.441 -(* INFERENCE RULE: RESOLVE *)
8.442 -
8.443 -(* Like RSN, but we rename apart only the type variables. Vars here typically
8.444 - have an index of 1, and the use of RSN would increase this typically to 3.
8.445 - Instantiations of those Vars could then fail. See comment on "mk_var". *)
8.446 -fun resolve_inc_tyvars thy tha i thb =
8.447 - let
8.448 - val tha = Drule.incr_type_indexes (1 + Thm.maxidx_of thb) tha
8.449 - fun aux tha thb =
8.450 - case Thm.bicompose false (false, tha, nprems_of tha) i thb
8.451 - |> Seq.list_of |> distinct Thm.eq_thm of
8.452 - [th] => th
8.453 - | _ => raise THM ("resolve_inc_tyvars: unique result expected", i,
8.454 - [tha, thb])
8.455 - in
8.456 - aux tha thb
8.457 - handle TERM z =>
8.458 - (* The unifier, which is invoked from "Thm.bicompose", will sometimes
8.459 - refuse to unify "?a::?'a" with "?a::?'b" or "?a::nat" and throw a
8.460 - "TERM" exception (with "add_ffpair" as first argument). We then
8.461 - perform unification of the types of variables by hand and try
8.462 - again. We could do this the first time around but this error
8.463 - occurs seldom and we don't want to break existing proofs in subtle
8.464 - ways or slow them down needlessly. *)
8.465 - case [] |> fold (Term.add_vars o prop_of) [tha, thb]
8.466 - |> AList.group (op =)
8.467 - |> maps (fn ((s, _), T :: Ts) =>
8.468 - map (fn T' => (Free (s, T), Free (s, T'))) Ts)
8.469 - |> rpair (Envir.empty ~1)
8.470 - |-> fold (Pattern.unify thy)
8.471 - |> Envir.type_env |> Vartab.dest
8.472 - |> map (fn (x, (S, T)) =>
8.473 - pairself (ctyp_of thy) (TVar (x, S), T)) of
8.474 - [] => raise TERM z
8.475 - | ps => aux (instantiate (ps, []) tha) (instantiate (ps, []) thb)
8.476 - end
8.477 -
8.478 -fun resolve_inf ctxt mode skolems thpairs atm th1 th2 =
8.479 - let
8.480 - val thy = ProofContext.theory_of ctxt
8.481 - val i_th1 = lookth thpairs th1 and i_th2 = lookth thpairs th2
8.482 - val _ = trace_msg (fn () => " isa th1 (pos): " ^ Display.string_of_thm ctxt i_th1)
8.483 - val _ = trace_msg (fn () => " isa th2 (neg): " ^ Display.string_of_thm ctxt i_th2)
8.484 - in
8.485 - if is_TrueI i_th1 then i_th2 (*Trivial cases where one operand is type info*)
8.486 - else if is_TrueI i_th2 then i_th1
8.487 - else
8.488 - let
8.489 - val i_atm = singleton (hol_terms_from_fol ctxt mode skolems)
8.490 - (Metis_Term.Fn atm)
8.491 - val _ = trace_msg (fn () => " atom: " ^ Syntax.string_of_term ctxt i_atm)
8.492 - val prems_th1 = prems_of i_th1
8.493 - val prems_th2 = prems_of i_th2
8.494 - val index_th1 = get_index (mk_not i_atm) prems_th1
8.495 - handle Empty => raise Fail "Failed to find literal in th1"
8.496 - val _ = trace_msg (fn () => " index_th1: " ^ Int.toString index_th1)
8.497 - val index_th2 = get_index i_atm prems_th2
8.498 - handle Empty => raise Fail "Failed to find literal in th2"
8.499 - val _ = trace_msg (fn () => " index_th2: " ^ Int.toString index_th2)
8.500 - in
8.501 - resolve_inc_tyvars thy (Meson.select_literal index_th1 i_th1) index_th2
8.502 - i_th2
8.503 - end
8.504 - end;
8.505 -
8.506 -(* INFERENCE RULE: REFL *)
8.507 -val refl_x = cterm_of @{theory} (Var (hd (Term.add_vars (prop_of REFL_THM) [])));
8.508 -val refl_idx = 1 + Thm.maxidx_of REFL_THM;
8.509 -
8.510 -fun refl_inf ctxt mode skolems t =
8.511 - let val thy = ProofContext.theory_of ctxt
8.512 - val i_t = singleton (hol_terms_from_fol ctxt mode skolems) t
8.513 - val _ = trace_msg (fn () => " term: " ^ Syntax.string_of_term ctxt i_t)
8.514 - val c_t = cterm_incr_types thy refl_idx i_t
8.515 - in cterm_instantiate [(refl_x, c_t)] REFL_THM end;
8.516 -
8.517 -fun get_ty_arg_size _ (Const (@{const_name HOL.eq}, _)) = 0 (*equality has no type arguments*)
8.518 - | get_ty_arg_size thy (Const (c, _)) = (num_type_args thy c handle TYPE _ => 0)
8.519 - | get_ty_arg_size _ _ = 0;
8.520 -
8.521 -(* INFERENCE RULE: EQUALITY *)
8.522 -fun equality_inf ctxt mode skolems (pos, atm) fp fr =
8.523 - let val thy = ProofContext.theory_of ctxt
8.524 - val m_tm = Metis_Term.Fn atm
8.525 - val [i_atm,i_tm] = hol_terms_from_fol ctxt mode skolems [m_tm, fr]
8.526 - val _ = trace_msg (fn () => "sign of the literal: " ^ Bool.toString pos)
8.527 - fun replace_item_list lx 0 (_::ls) = lx::ls
8.528 - | replace_item_list lx i (l::ls) = l :: replace_item_list lx (i-1) ls
8.529 - fun path_finder_FO tm [] = (tm, Term.Bound 0)
8.530 - | path_finder_FO tm (p::ps) =
8.531 - let val (tm1,args) = strip_comb tm
8.532 - val adjustment = get_ty_arg_size thy tm1
8.533 - val p' = if adjustment > p then p else p-adjustment
8.534 - val tm_p = List.nth(args,p')
8.535 - handle Subscript =>
8.536 - error ("Cannot replay Metis proof in Isabelle:\n" ^
8.537 - "equality_inf: " ^ Int.toString p ^ " adj " ^
8.538 - Int.toString adjustment ^ " term " ^
8.539 - Syntax.string_of_term ctxt tm)
8.540 - val _ = trace_msg (fn () => "path_finder: " ^ Int.toString p ^
8.541 - " " ^ Syntax.string_of_term ctxt tm_p)
8.542 - val (r,t) = path_finder_FO tm_p ps
8.543 - in
8.544 - (r, list_comb (tm1, replace_item_list t p' args))
8.545 - end
8.546 - fun path_finder_HO tm [] = (tm, Term.Bound 0)
8.547 - | path_finder_HO (t$u) (0::ps) = (fn(x,y) => (x, y$u)) (path_finder_HO t ps)
8.548 - | path_finder_HO (t$u) (_::ps) = (fn(x,y) => (x, t$y)) (path_finder_HO u ps)
8.549 - | path_finder_HO tm ps =
8.550 - raise Fail ("equality_inf, path_finder_HO: path = " ^
8.551 - space_implode " " (map Int.toString ps) ^
8.552 - " isa-term: " ^ Syntax.string_of_term ctxt tm)
8.553 - fun path_finder_FT tm [] _ = (tm, Term.Bound 0)
8.554 - | path_finder_FT tm (0::ps) (Metis_Term.Fn ("ti", [t1, _])) =
8.555 - path_finder_FT tm ps t1
8.556 - | path_finder_FT (t$u) (0::ps) (Metis_Term.Fn (".", [t1, _])) =
8.557 - (fn(x,y) => (x, y$u)) (path_finder_FT t ps t1)
8.558 - | path_finder_FT (t$u) (1::ps) (Metis_Term.Fn (".", [_, t2])) =
8.559 - (fn(x,y) => (x, t$y)) (path_finder_FT u ps t2)
8.560 - | path_finder_FT tm ps t =
8.561 - raise Fail ("equality_inf, path_finder_FT: path = " ^
8.562 - space_implode " " (map Int.toString ps) ^
8.563 - " isa-term: " ^ Syntax.string_of_term ctxt tm ^
8.564 - " fol-term: " ^ Metis_Term.toString t)
8.565 - fun path_finder FO tm ps _ = path_finder_FO tm ps
8.566 - | path_finder HO (tm as Const(@{const_name HOL.eq},_) $ _ $ _) (p::ps) _ =
8.567 - (*equality: not curried, as other predicates are*)
8.568 - if p=0 then path_finder_HO tm (0::1::ps) (*select first operand*)
8.569 - else path_finder_HO tm (p::ps) (*1 selects second operand*)
8.570 - | path_finder HO tm (_ :: ps) (Metis_Term.Fn ("{}", [_])) =
8.571 - path_finder_HO tm ps (*if not equality, ignore head to skip hBOOL*)
8.572 - | path_finder FT (tm as Const(@{const_name HOL.eq}, _) $ _ $ _) (p::ps)
8.573 - (Metis_Term.Fn ("=", [t1,t2])) =
8.574 - (*equality: not curried, as other predicates are*)
8.575 - if p=0 then path_finder_FT tm (0::1::ps)
8.576 - (Metis_Term.Fn (".", [Metis_Term.Fn (".", [metis_eq,t1]), t2]))
8.577 - (*select first operand*)
8.578 - else path_finder_FT tm (p::ps)
8.579 - (Metis_Term.Fn (".", [metis_eq,t2]))
8.580 - (*1 selects second operand*)
8.581 - | path_finder FT tm (_ :: ps) (Metis_Term.Fn ("{}", [t1])) = path_finder_FT tm ps t1
8.582 - (*if not equality, ignore head to skip the hBOOL predicate*)
8.583 - | path_finder FT tm ps t = path_finder_FT tm ps t (*really an error case!*)
8.584 - fun path_finder_lit ((nt as Const (@{const_name Not}, _)) $ tm_a) idx =
8.585 - let val (tm, tm_rslt) = path_finder mode tm_a idx m_tm
8.586 - in (tm, nt $ tm_rslt) end
8.587 - | path_finder_lit tm_a idx = path_finder mode tm_a idx m_tm
8.588 - val (tm_subst, body) = path_finder_lit i_atm fp
8.589 - val tm_abs = Term.Abs("x", Term.type_of tm_subst, body)
8.590 - val _ = trace_msg (fn () => "abstraction: " ^ Syntax.string_of_term ctxt tm_abs)
8.591 - val _ = trace_msg (fn () => "i_tm: " ^ Syntax.string_of_term ctxt i_tm)
8.592 - val _ = trace_msg (fn () => "located term: " ^ Syntax.string_of_term ctxt tm_subst)
8.593 - val imax = maxidx_of_term (i_tm $ tm_abs $ tm_subst) (*ill typed but gives right max*)
8.594 - val subst' = Thm.incr_indexes (imax+1) (if pos then subst_em else ssubst_em)
8.595 - val _ = trace_msg (fn () => "subst' " ^ Display.string_of_thm ctxt subst')
8.596 - val eq_terms = map (pairself (cterm_of thy))
8.597 - (ListPair.zip (OldTerm.term_vars (prop_of subst'), [tm_abs, tm_subst, i_tm]))
8.598 - in cterm_instantiate eq_terms subst' end;
8.599 -
8.600 -val factor = Seq.hd o distinct_subgoals_tac;
8.601 -
8.602 -fun step ctxt mode skolems thpairs p =
8.603 - case p of
8.604 - (fol_th, Metis_Proof.Axiom _) => factor (axiom_inf thpairs fol_th)
8.605 - | (_, Metis_Proof.Assume f_atm) => assume_inf ctxt mode skolems f_atm
8.606 - | (_, Metis_Proof.Metis_Subst (f_subst, f_th1)) =>
8.607 - factor (inst_inf ctxt mode skolems thpairs f_subst f_th1)
8.608 - | (_, Metis_Proof.Resolve(f_atm, f_th1, f_th2)) =>
8.609 - factor (resolve_inf ctxt mode skolems thpairs f_atm f_th1 f_th2)
8.610 - | (_, Metis_Proof.Refl f_tm) => refl_inf ctxt mode skolems f_tm
8.611 - | (_, Metis_Proof.Equality (f_lit, f_p, f_r)) =>
8.612 - equality_inf ctxt mode skolems f_lit f_p f_r
8.613 -
8.614 -fun real_literal (_, (c, _)) = not (String.isPrefix class_prefix c);
8.615 -
8.616 -fun translate_one ctxt mode skolems (fol_th, inf) thpairs =
8.617 - let
8.618 - val _ = trace_msg (fn () => "=============================================")
8.619 - val _ = trace_msg (fn () => "METIS THM: " ^ Metis_Thm.toString fol_th)
8.620 - val _ = trace_msg (fn () => "INFERENCE: " ^ Metis_Proof.inferenceToString inf)
8.621 - val th = Meson.flexflex_first_order (step ctxt mode skolems
8.622 - thpairs (fol_th, inf))
8.623 - val _ = trace_msg (fn () => "ISABELLE THM: " ^ Display.string_of_thm ctxt th)
8.624 - val _ = trace_msg (fn () => "=============================================")
8.625 - val n_metis_lits =
8.626 - length (filter real_literal (Metis_LiteralSet.toList (Metis_Thm.clause fol_th)))
8.627 - val _ = if nprems_of th = n_metis_lits then ()
8.628 - else error "Cannot replay Metis proof in Isabelle."
8.629 - in (fol_th, th) :: thpairs end
8.630 +fun have_common_thm ths1 ths2 =
8.631 + exists (member Thm.eq_thm ths1) (map Meson.make_meta_clause ths2)
8.632
8.633 (*Determining which axiom clauses are actually used*)
8.634 fun used_axioms axioms (th, Metis_Proof.Axiom _) = SOME (lookth axioms th)
8.635 | used_axioms _ _ = NONE;
8.636
8.637 -(* ------------------------------------------------------------------------- *)
8.638 -(* Translation of HO Clauses *)
8.639 -(* ------------------------------------------------------------------------- *)
8.640 -
8.641 -fun type_ext thy tms =
8.642 - let val subs = tfree_classes_of_terms tms
8.643 - val supers = tvar_classes_of_terms tms
8.644 - and tycons = type_consts_of_terms thy tms
8.645 - val (supers', arity_clauses) = make_arity_clauses thy tycons supers
8.646 - val class_rel_clauses = make_class_rel_clauses thy subs supers'
8.647 - in map class_rel_cls class_rel_clauses @ map arity_cls arity_clauses
8.648 - end;
8.649 -
8.650 -(* ------------------------------------------------------------------------- *)
8.651 -(* Logic maps manage the interface between HOL and first-order logic. *)
8.652 -(* ------------------------------------------------------------------------- *)
8.653 -
8.654 -type logic_map =
8.655 - {axioms: (Metis_Thm.thm * thm) list,
8.656 - tfrees: type_literal list,
8.657 - skolems: (string * term) list}
8.658 -
8.659 -fun const_in_metis c (pred, tm_list) =
8.660 - let
8.661 - fun in_mterm (Metis_Term.Var _) = false
8.662 - | in_mterm (Metis_Term.Fn (".", tm_list)) = exists in_mterm tm_list
8.663 - | in_mterm (Metis_Term.Fn (nm, tm_list)) = c=nm orelse exists in_mterm tm_list
8.664 - in c = pred orelse exists in_mterm tm_list end;
8.665 -
8.666 -(*Extract TFree constraints from context to include as conjecture clauses*)
8.667 -fun init_tfrees ctxt =
8.668 - let fun add ((a,i),s) Ts = if i = ~1 then TFree(a,s) :: Ts else Ts in
8.669 - Vartab.fold add (#2 (Variable.constraints_of ctxt)) []
8.670 - |> type_literals_for_types
8.671 - end;
8.672 -
8.673 -(*transform isabelle type / arity clause to metis clause *)
8.674 -fun add_type_thm [] lmap = lmap
8.675 - | add_type_thm ((ith, mth) :: cls) {axioms, tfrees, skolems} =
8.676 - add_type_thm cls {axioms = (mth, ith) :: axioms, tfrees = tfrees,
8.677 - skolems = skolems}
8.678 -
8.679 -(*Insert non-logical axioms corresponding to all accumulated TFrees*)
8.680 -fun add_tfrees {axioms, tfrees, skolems} : logic_map =
8.681 - {axioms = map (rpair TrueI o metis_of_tfree) (distinct (op =) tfrees) @
8.682 - axioms,
8.683 - tfrees = tfrees, skolems = skolems}
8.684 -
8.685 -fun string_of_mode FO = "FO"
8.686 - | string_of_mode HO = "HO"
8.687 - | string_of_mode FT = "FT"
8.688 -
8.689 -val helpers =
8.690 - [("c_COMBI", (false, map (`I) @{thms COMBI_def})),
8.691 - ("c_COMBK", (false, map (`I) @{thms COMBK_def})),
8.692 - ("c_COMBB", (false, map (`I) @{thms COMBB_def})),
8.693 - ("c_COMBC", (false, map (`I) @{thms COMBC_def})),
8.694 - ("c_COMBS", (false, map (`I) @{thms COMBS_def})),
8.695 - ("c_fequal", (false, map (rpair @{thm equal_imp_equal})
8.696 - @{thms fequal_imp_equal equal_imp_fequal})),
8.697 - ("c_True", (true, map (`I) @{thms True_or_False})),
8.698 - ("c_False", (true, map (`I) @{thms True_or_False})),
8.699 - ("c_If", (true, map (`I) @{thms if_True if_False True_or_False}))]
8.700 -
8.701 -fun is_quasi_fol_clause thy =
8.702 - Meson.is_fol_term thy o snd o conceal_skolem_terms ~1 [] o prop_of
8.703 -
8.704 -(* Function to generate metis clauses, including comb and type clauses *)
8.705 -fun build_map mode0 ctxt cls ths =
8.706 - let val thy = ProofContext.theory_of ctxt
8.707 - (*The modes FO and FT are sticky. HO can be downgraded to FO.*)
8.708 - fun set_mode FO = FO
8.709 - | set_mode HO =
8.710 - if forall (is_quasi_fol_clause thy) (cls @ ths) then FO else HO
8.711 - | set_mode FT = FT
8.712 - val mode = set_mode mode0
8.713 - (*transform isabelle clause to metis clause *)
8.714 - fun add_thm is_conjecture (metis_ith, isa_ith) {axioms, tfrees, skolems}
8.715 - : logic_map =
8.716 - let
8.717 - val (mth, tfree_lits, skolems) =
8.718 - hol_thm_to_fol is_conjecture ctxt mode (length axioms) skolems
8.719 - metis_ith
8.720 - in
8.721 - {axioms = (mth, Meson.make_meta_clause isa_ith) :: axioms,
8.722 - tfrees = union (op =) tfree_lits tfrees, skolems = skolems}
8.723 - end;
8.724 - val lmap = {axioms = [], tfrees = init_tfrees ctxt, skolems = []}
8.725 - |> fold (add_thm true o `I) cls
8.726 - |> add_tfrees
8.727 - |> fold (add_thm false o `I) ths
8.728 - val clause_lists = map (Metis_Thm.clause o #1) (#axioms lmap)
8.729 - fun is_used c =
8.730 - exists (Metis_LiteralSet.exists (const_in_metis c o #2)) clause_lists
8.731 - val lmap =
8.732 - if mode = FO then
8.733 - lmap
8.734 - else
8.735 - let
8.736 - val helper_ths =
8.737 - helpers |> filter (is_used o fst)
8.738 - |> maps (fn (c, (needs_full_types, thms)) =>
8.739 - if not (is_used c) orelse
8.740 - needs_full_types andalso mode <> FT then
8.741 - []
8.742 - else
8.743 - thms)
8.744 - in lmap |> fold (add_thm false) helper_ths end
8.745 - in (mode, add_type_thm (type_ext thy (map prop_of (cls @ ths))) lmap) end
8.746 -
8.747 val clause_params =
8.748 {ordering = Metis_KnuthBendixOrder.default,
8.749 orderLiterals = Metis_Clause.UnsignedLiteralOrder,
8.750 @@ -749,20 +50,12 @@
8.751 variablesWeight = 0.0,
8.752 literalsWeight = 0.0,
8.753 models = []}
8.754 -val refute_params = {active = active_params, waiting = waiting_params}
8.755 -
8.756 -fun refute cls =
8.757 - Metis_Resolution.new refute_params {axioms = cls, conjecture = []}
8.758 - |> Metis_Resolution.loop
8.759 -
8.760 -fun is_false t = t aconv (HOLogic.mk_Trueprop HOLogic.false_const);
8.761 -
8.762 -fun common_thm ths1 ths2 = exists (member Thm.eq_thm ths1) (map Meson.make_meta_clause ths2);
8.763 -
8.764 +val resolution_params = {active = active_params, waiting = waiting_params}
8.765
8.766 (* Main function to start Metis proof and reconstruction *)
8.767 fun FOL_SOLVE mode ctxt cls ths0 =
8.768 let val thy = ProofContext.theory_of ctxt
8.769 + val type_lits = Config.get ctxt type_lits
8.770 val th_cls_pairs =
8.771 map (fn th => (Thm.get_name_hint th, Clausifier.cnf_axiom thy th)) ths0
8.772 val ths = maps #2 th_cls_pairs
8.773 @@ -770,7 +63,8 @@
8.774 val _ = app (fn th => trace_msg (fn () => Display.string_of_thm ctxt th)) cls
8.775 val _ = trace_msg (fn () => "THEOREM CLAUSES")
8.776 val _ = app (fn th => trace_msg (fn () => Display.string_of_thm ctxt th)) ths
8.777 - val (mode, {axioms, tfrees, skolems}) = build_map mode ctxt cls ths
8.778 + val (mode, {axioms, tfrees, skolems}) =
8.779 + build_logic_map mode ctxt type_lits cls ths
8.780 val _ = if null tfrees then ()
8.781 else (trace_msg (fn () => "TFREE CLAUSES");
8.782 app (fn TyLitFree ((s, _), (s', _)) =>
8.783 @@ -784,21 +78,22 @@
8.784 case filter (is_false o prop_of) cls of
8.785 false_th::_ => [false_th RS @{thm FalseE}]
8.786 | [] =>
8.787 - case refute thms of
8.788 + case Metis_Resolution.new resolution_params {axioms = thms, conjecture = []}
8.789 + |> Metis_Resolution.loop of
8.790 Metis_Resolution.Contradiction mth =>
8.791 let val _ = trace_msg (fn () => "METIS RECONSTRUCTION START: " ^
8.792 Metis_Thm.toString mth)
8.793 val ctxt' = fold Variable.declare_constraints (map prop_of cls) ctxt
8.794 (*add constraints arising from converting goal to clause form*)
8.795 val proof = Metis_Proof.proof mth
8.796 - val result = fold (translate_one ctxt' mode skolems) proof axioms
8.797 + val result = fold (replay_one_inference ctxt' mode skolems) proof axioms
8.798 and used = map_filter (used_axioms axioms) proof
8.799 val _ = trace_msg (fn () => "METIS COMPLETED...clauses actually used:")
8.800 val _ = app (fn th => trace_msg (fn () => Display.string_of_thm ctxt th)) used
8.801 val unused = th_cls_pairs |> map_filter (fn (name, cls) =>
8.802 - if common_thm used cls then NONE else SOME name)
8.803 + if have_common_thm used cls then NONE else SOME name)
8.804 in
8.805 - if not (null cls) andalso not (common_thm used cls) then
8.806 + if not (null cls) andalso not (have_common_thm used cls) then
8.807 warning "Metis: The assumptions are inconsistent."
8.808 else
8.809 ();
9.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
9.2 +++ b/src/HOL/Tools/Sledgehammer/metis_translate.ML Fri Sep 17 16:38:11 2010 +0200
9.3 @@ -0,0 +1,738 @@
9.4 +(* Title: HOL/Tools/Sledgehammer/metis_translate.ML
9.5 + Author: Jia Meng, Cambridge University Computer Laboratory and NICTA
9.6 + Author: Kong W. Susanto, Cambridge University Computer Laboratory
9.7 + Author: Lawrence C. Paulson, Cambridge University Computer Laboratory
9.8 + Author: Jasmin Blanchette, TU Muenchen
9.9 +
9.10 +Translation of HOL to FOL for Metis.
9.11 +*)
9.12 +
9.13 +signature METIS_TRANSLATE =
9.14 +sig
9.15 + type name = string * string
9.16 + datatype type_literal =
9.17 + TyLitVar of name * name |
9.18 + TyLitFree of name * name
9.19 + datatype arLit =
9.20 + TConsLit of name * name * name list |
9.21 + TVarLit of name * name
9.22 + datatype arity_clause =
9.23 + ArityClause of {name: string, conclLit: arLit, premLits: arLit list}
9.24 + datatype class_rel_clause =
9.25 + ClassRelClause of {name: string, subclass: name, superclass: name}
9.26 + datatype combtyp =
9.27 + CombTVar of name |
9.28 + CombTFree of name |
9.29 + CombType of name * combtyp list
9.30 + datatype combterm =
9.31 + CombConst of name * combtyp * combtyp list (* Const and Free *) |
9.32 + CombVar of name * combtyp |
9.33 + CombApp of combterm * combterm
9.34 + datatype fol_literal = FOLLiteral of bool * combterm
9.35 +
9.36 + datatype mode = FO | HO | FT
9.37 + type logic_map =
9.38 + {axioms: (Metis_Thm.thm * thm) list,
9.39 + tfrees: type_literal list,
9.40 + skolems: (string * term) list}
9.41 +
9.42 + val type_wrapper_name : string
9.43 + val bound_var_prefix : string
9.44 + val schematic_var_prefix: string
9.45 + val fixed_var_prefix: string
9.46 + val tvar_prefix: string
9.47 + val tfree_prefix: string
9.48 + val const_prefix: string
9.49 + val type_const_prefix: string
9.50 + val class_prefix: string
9.51 + val invert_const: string -> string
9.52 + val ascii_of: string -> string
9.53 + val unascii_of: string -> string
9.54 + val strip_prefix_and_unascii: string -> string -> string option
9.55 + val make_bound_var : string -> string
9.56 + val make_schematic_var : string * int -> string
9.57 + val make_fixed_var : string -> string
9.58 + val make_schematic_type_var : string * int -> string
9.59 + val make_fixed_type_var : string -> string
9.60 + val make_fixed_const : string -> string
9.61 + val make_fixed_type_const : string -> string
9.62 + val make_type_class : string -> string
9.63 + val num_type_args: theory -> string -> int
9.64 + val type_literals_for_types : typ list -> type_literal list
9.65 + val make_class_rel_clauses :
9.66 + theory -> class list -> class list -> class_rel_clause list
9.67 + val make_arity_clauses :
9.68 + theory -> string list -> class list -> class list * arity_clause list
9.69 + val combtyp_of : combterm -> combtyp
9.70 + val strip_combterm_comb : combterm -> combterm * combterm list
9.71 + val combterm_from_term :
9.72 + theory -> (string * typ) list -> term -> combterm * typ list
9.73 + val reveal_skolem_terms : (string * term) list -> term -> term
9.74 + val tfree_classes_of_terms : term list -> string list
9.75 + val tvar_classes_of_terms : term list -> string list
9.76 + val type_consts_of_terms : theory -> term list -> string list
9.77 + val string_of_mode : mode -> string
9.78 + val build_logic_map :
9.79 + mode -> Proof.context -> bool -> thm list -> thm list -> mode * logic_map
9.80 +end
9.81 +
9.82 +structure Metis_Translate : METIS_TRANSLATE =
9.83 +struct
9.84 +
9.85 +val type_wrapper_name = "ti"
9.86 +
9.87 +val bound_var_prefix = "B_"
9.88 +val schematic_var_prefix = "V_"
9.89 +val fixed_var_prefix = "v_"
9.90 +
9.91 +val tvar_prefix = "T_";
9.92 +val tfree_prefix = "t_";
9.93 +
9.94 +val const_prefix = "c_";
9.95 +val type_const_prefix = "tc_";
9.96 +val class_prefix = "class_";
9.97 +
9.98 +fun union_all xss = fold (union (op =)) xss []
9.99 +
9.100 +(* Readable names for the more common symbolic functions. Do not mess with the
9.101 + last nine entries of the table unless you know what you are doing. *)
9.102 +val const_trans_table =
9.103 + Symtab.make [(@{type_name Product_Type.prod}, "prod"),
9.104 + (@{type_name Sum_Type.sum}, "sum"),
9.105 + (@{const_name HOL.eq}, "equal"),
9.106 + (@{const_name HOL.conj}, "and"),
9.107 + (@{const_name HOL.disj}, "or"),
9.108 + (@{const_name HOL.implies}, "implies"),
9.109 + (@{const_name Set.member}, "member"),
9.110 + (@{const_name fequal}, "fequal"),
9.111 + (@{const_name COMBI}, "COMBI"),
9.112 + (@{const_name COMBK}, "COMBK"),
9.113 + (@{const_name COMBB}, "COMBB"),
9.114 + (@{const_name COMBC}, "COMBC"),
9.115 + (@{const_name COMBS}, "COMBS"),
9.116 + (@{const_name True}, "True"),
9.117 + (@{const_name False}, "False"),
9.118 + (@{const_name If}, "If")]
9.119 +
9.120 +(* Invert the table of translations between Isabelle and ATPs. *)
9.121 +val const_trans_table_inv =
9.122 + Symtab.update ("fequal", @{const_name HOL.eq})
9.123 + (Symtab.make (map swap (Symtab.dest const_trans_table)))
9.124 +
9.125 +val invert_const = perhaps (Symtab.lookup const_trans_table_inv)
9.126 +
9.127 +(*Escaping of special characters.
9.128 + Alphanumeric characters are left unchanged.
9.129 + The character _ goes to __
9.130 + Characters in the range ASCII space to / go to _A to _P, respectively.
9.131 + Other characters go to _nnn where nnn is the decimal ASCII code.*)
9.132 +val A_minus_space = Char.ord #"A" - Char.ord #" ";
9.133 +
9.134 +fun stringN_of_int 0 _ = ""
9.135 + | stringN_of_int k n = stringN_of_int (k-1) (n div 10) ^ Int.toString (n mod 10);
9.136 +
9.137 +fun ascii_of_c c =
9.138 + if Char.isAlphaNum c then String.str c
9.139 + else if c = #"_" then "__"
9.140 + else if #" " <= c andalso c <= #"/"
9.141 + then "_" ^ String.str (Char.chr (Char.ord c + A_minus_space))
9.142 + else ("_" ^ stringN_of_int 3 (Char.ord c)) (*fixed width, in case more digits follow*)
9.143 +
9.144 +val ascii_of = String.translate ascii_of_c;
9.145 +
9.146 +(** Remove ASCII armouring from names in proof files **)
9.147 +
9.148 +(*We don't raise error exceptions because this code can run inside the watcher.
9.149 + Also, the errors are "impossible" (hah!)*)
9.150 +fun unascii_aux rcs [] = String.implode(rev rcs)
9.151 + | unascii_aux rcs [#"_"] = unascii_aux (#"_"::rcs) [] (*ERROR*)
9.152 + (*Three types of _ escapes: __, _A to _P, _nnn*)
9.153 + | unascii_aux rcs (#"_" :: #"_" :: cs) = unascii_aux (#"_"::rcs) cs
9.154 + | unascii_aux rcs (#"_" :: c :: cs) =
9.155 + if #"A" <= c andalso c<= #"P" (*translation of #" " to #"/"*)
9.156 + then unascii_aux (Char.chr(Char.ord c - A_minus_space) :: rcs) cs
9.157 + else
9.158 + let val digits = List.take (c::cs, 3) handle Subscript => []
9.159 + in
9.160 + case Int.fromString (String.implode digits) of
9.161 + NONE => unascii_aux (c:: #"_"::rcs) cs (*ERROR*)
9.162 + | SOME n => unascii_aux (Char.chr n :: rcs) (List.drop (cs, 2))
9.163 + end
9.164 + | unascii_aux rcs (c::cs) = unascii_aux (c::rcs) cs
9.165 +val unascii_of = unascii_aux [] o String.explode
9.166 +
9.167 +(* If string s has the prefix s1, return the result of deleting it,
9.168 + un-ASCII'd. *)
9.169 +fun strip_prefix_and_unascii s1 s =
9.170 + if String.isPrefix s1 s then
9.171 + SOME (unascii_of (String.extract (s, size s1, NONE)))
9.172 + else
9.173 + NONE
9.174 +
9.175 +(*Remove the initial ' character from a type variable, if it is present*)
9.176 +fun trim_type_var s =
9.177 + if s <> "" andalso String.sub(s,0) = #"'" then String.extract(s,1,NONE)
9.178 + else error ("trim_type: Malformed type variable encountered: " ^ s);
9.179 +
9.180 +fun ascii_of_indexname (v,0) = ascii_of v
9.181 + | ascii_of_indexname (v,i) = ascii_of v ^ "_" ^ Int.toString i;
9.182 +
9.183 +fun make_bound_var x = bound_var_prefix ^ ascii_of x
9.184 +fun make_schematic_var v = schematic_var_prefix ^ ascii_of_indexname v
9.185 +fun make_fixed_var x = fixed_var_prefix ^ ascii_of x
9.186 +
9.187 +fun make_schematic_type_var (x,i) =
9.188 + tvar_prefix ^ (ascii_of_indexname (trim_type_var x,i));
9.189 +fun make_fixed_type_var x = tfree_prefix ^ (ascii_of (trim_type_var x));
9.190 +
9.191 +fun lookup_const c =
9.192 + case Symtab.lookup const_trans_table c of
9.193 + SOME c' => c'
9.194 + | NONE => ascii_of c
9.195 +
9.196 +(* HOL.eq MUST BE "equal" because it's built into ATPs. *)
9.197 +fun make_fixed_const @{const_name HOL.eq} = "equal"
9.198 + | make_fixed_const c = const_prefix ^ lookup_const c
9.199 +
9.200 +fun make_fixed_type_const c = type_const_prefix ^ lookup_const c
9.201 +
9.202 +fun make_type_class clas = class_prefix ^ ascii_of clas;
9.203 +
9.204 +val skolem_prefix = "Sledgehammer" ^ Long_Name.separator ^ "Sko"
9.205 +
9.206 +(* The number of type arguments of a constant, zero if it's monomorphic. For
9.207 + (instances of) Skolem pseudoconstants, this information is encoded in the
9.208 + constant name. *)
9.209 +fun num_type_args thy s =
9.210 + if String.isPrefix skolem_prefix s then
9.211 + s |> space_explode Long_Name.separator |> List.last |> Int.fromString |> the
9.212 + else
9.213 + (s, Sign.the_const_type thy s) |> Sign.const_typargs thy |> length
9.214 +
9.215 +(**** Definitions and functions for FOL clauses for TPTP format output ****)
9.216 +
9.217 +type name = string * string
9.218 +
9.219 +(**** Isabelle FOL clauses ****)
9.220 +
9.221 +(* The first component is the type class; the second is a TVar or TFree. *)
9.222 +datatype type_literal =
9.223 + TyLitVar of name * name |
9.224 + TyLitFree of name * name
9.225 +
9.226 +(*Make literals for sorted type variables*)
9.227 +fun sorts_on_typs_aux (_, []) = []
9.228 + | sorts_on_typs_aux ((x,i), s::ss) =
9.229 + let val sorts = sorts_on_typs_aux ((x,i), ss)
9.230 + in
9.231 + if s = "HOL.type" then sorts
9.232 + else if i = ~1 then TyLitFree (`make_type_class s, `make_fixed_type_var x) :: sorts
9.233 + else TyLitVar (`make_type_class s, (make_schematic_type_var (x,i), x)) :: sorts
9.234 + end;
9.235 +
9.236 +fun sorts_on_typs (TFree (a,s)) = sorts_on_typs_aux ((a,~1),s)
9.237 + | sorts_on_typs (TVar (v,s)) = sorts_on_typs_aux (v,s);
9.238 +
9.239 +(*Given a list of sorted type variables, return a list of type literals.*)
9.240 +fun type_literals_for_types Ts =
9.241 + fold (union (op =)) (map sorts_on_typs Ts) []
9.242 +
9.243 +(** make axiom and conjecture clauses. **)
9.244 +
9.245 +(**** Isabelle arities ****)
9.246 +
9.247 +datatype arLit =
9.248 + TConsLit of name * name * name list |
9.249 + TVarLit of name * name
9.250 +
9.251 +datatype arity_clause =
9.252 + ArityClause of {name: string, conclLit: arLit, premLits: arLit list}
9.253 +
9.254 +
9.255 +fun gen_TVars 0 = []
9.256 + | gen_TVars n = ("T_" ^ Int.toString n) :: gen_TVars (n-1);
9.257 +
9.258 +fun pack_sort(_,[]) = []
9.259 + | pack_sort(tvar, "HOL.type"::srt) = pack_sort (tvar, srt) (*IGNORE sort "type"*)
9.260 + | pack_sort(tvar, cls::srt) =
9.261 + (`make_type_class cls, (tvar, tvar)) :: pack_sort (tvar, srt)
9.262 +
9.263 +(*Arity of type constructor tcon :: (arg1,...,argN)res*)
9.264 +fun make_axiom_arity_clause (tcons, name, (cls,args)) =
9.265 + let
9.266 + val tvars = gen_TVars (length args)
9.267 + val tvars_srts = ListPair.zip (tvars, args)
9.268 + in
9.269 + ArityClause {name = name,
9.270 + conclLit = TConsLit (`make_type_class cls,
9.271 + `make_fixed_type_const tcons,
9.272 + tvars ~~ tvars),
9.273 + premLits = map TVarLit (union_all (map pack_sort tvars_srts))}
9.274 + end
9.275 +
9.276 +
9.277 +(**** Isabelle class relations ****)
9.278 +
9.279 +datatype class_rel_clause =
9.280 + ClassRelClause of {name: string, subclass: name, superclass: name}
9.281 +
9.282 +(*Generate all pairs (sub,super) such that sub is a proper subclass of super in theory thy.*)
9.283 +fun class_pairs _ [] _ = []
9.284 + | class_pairs thy subs supers =
9.285 + let
9.286 + val class_less = Sorts.class_less (Sign.classes_of thy)
9.287 + fun add_super sub super = class_less (sub, super) ? cons (sub, super)
9.288 + fun add_supers sub = fold (add_super sub) supers
9.289 + in fold add_supers subs [] end
9.290 +
9.291 +fun make_class_rel_clause (sub,super) =
9.292 + ClassRelClause {name = sub ^ "_" ^ super,
9.293 + subclass = `make_type_class sub,
9.294 + superclass = `make_type_class super}
9.295 +
9.296 +fun make_class_rel_clauses thy subs supers =
9.297 + map make_class_rel_clause (class_pairs thy subs supers);
9.298 +
9.299 +
9.300 +(** Isabelle arities **)
9.301 +
9.302 +fun arity_clause _ _ (_, []) = []
9.303 + | arity_clause seen n (tcons, ("HOL.type",_)::ars) = (*ignore*)
9.304 + arity_clause seen n (tcons,ars)
9.305 + | arity_clause seen n (tcons, (ar as (class,_)) :: ars) =
9.306 + if member (op =) seen class then (*multiple arities for the same tycon, class pair*)
9.307 + make_axiom_arity_clause (tcons, lookup_const tcons ^ "_" ^ class ^ "_" ^ Int.toString n, ar) ::
9.308 + arity_clause seen (n+1) (tcons,ars)
9.309 + else
9.310 + make_axiom_arity_clause (tcons, lookup_const tcons ^ "_" ^ class, ar) ::
9.311 + arity_clause (class::seen) n (tcons,ars)
9.312 +
9.313 +fun multi_arity_clause [] = []
9.314 + | multi_arity_clause ((tcons, ars) :: tc_arlists) =
9.315 + arity_clause [] 1 (tcons, ars) @ multi_arity_clause tc_arlists
9.316 +
9.317 +(*Generate all pairs (tycon,class,sorts) such that tycon belongs to class in theory thy
9.318 + provided its arguments have the corresponding sorts.*)
9.319 +fun type_class_pairs thy tycons classes =
9.320 + let val alg = Sign.classes_of thy
9.321 + fun domain_sorts tycon = Sorts.mg_domain alg tycon o single
9.322 + fun add_class tycon class =
9.323 + cons (class, domain_sorts tycon class)
9.324 + handle Sorts.CLASS_ERROR _ => I
9.325 + fun try_classes tycon = (tycon, fold (add_class tycon) classes [])
9.326 + in map try_classes tycons end;
9.327 +
9.328 +(*Proving one (tycon, class) membership may require proving others, so iterate.*)
9.329 +fun iter_type_class_pairs _ _ [] = ([], [])
9.330 + | iter_type_class_pairs thy tycons classes =
9.331 + let val cpairs = type_class_pairs thy tycons classes
9.332 + val newclasses = union_all (union_all (union_all (map (map #2 o #2) cpairs)))
9.333 + |> subtract (op =) classes |> subtract (op =) HOLogic.typeS
9.334 + val (classes', cpairs') = iter_type_class_pairs thy tycons newclasses
9.335 + in (union (op =) classes' classes, union (op =) cpairs' cpairs) end;
9.336 +
9.337 +fun make_arity_clauses thy tycons classes =
9.338 + let val (classes', cpairs) = iter_type_class_pairs thy tycons classes
9.339 + in (classes', multi_arity_clause cpairs) end;
9.340 +
9.341 +datatype combtyp =
9.342 + CombTVar of name |
9.343 + CombTFree of name |
9.344 + CombType of name * combtyp list
9.345 +
9.346 +datatype combterm =
9.347 + CombConst of name * combtyp * combtyp list (* Const and Free *) |
9.348 + CombVar of name * combtyp |
9.349 + CombApp of combterm * combterm
9.350 +
9.351 +datatype fol_literal = FOLLiteral of bool * combterm
9.352 +
9.353 +(*********************************************************************)
9.354 +(* convert a clause with type Term.term to a clause with type clause *)
9.355 +(*********************************************************************)
9.356 +
9.357 +(*Result of a function type; no need to check that the argument type matches.*)
9.358 +fun result_type (CombType (_, [_, tp2])) = tp2
9.359 + | result_type _ = raise Fail "non-function type"
9.360 +
9.361 +fun combtyp_of (CombConst (_, tp, _)) = tp
9.362 + | combtyp_of (CombVar (_, tp)) = tp
9.363 + | combtyp_of (CombApp (t1, _)) = result_type (combtyp_of t1)
9.364 +
9.365 +(*gets the head of a combinator application, along with the list of arguments*)
9.366 +fun strip_combterm_comb u =
9.367 + let fun stripc (CombApp(t,u), ts) = stripc (t, u::ts)
9.368 + | stripc x = x
9.369 + in stripc(u,[]) end
9.370 +
9.371 +fun combtype_of (Type (a, Ts)) =
9.372 + let val (folTypes, ts) = combtypes_of Ts in
9.373 + (CombType (`make_fixed_type_const a, folTypes), ts)
9.374 + end
9.375 + | combtype_of (tp as TFree (a, _)) = (CombTFree (`make_fixed_type_var a), [tp])
9.376 + | combtype_of (tp as TVar (x, _)) =
9.377 + (CombTVar (make_schematic_type_var x, string_of_indexname x), [tp])
9.378 +and combtypes_of Ts =
9.379 + let val (folTyps, ts) = ListPair.unzip (map combtype_of Ts) in
9.380 + (folTyps, union_all ts)
9.381 + end
9.382 +
9.383 +(* same as above, but no gathering of sort information *)
9.384 +fun simple_combtype_of (Type (a, Ts)) =
9.385 + CombType (`make_fixed_type_const a, map simple_combtype_of Ts)
9.386 + | simple_combtype_of (TFree (a, _)) = CombTFree (`make_fixed_type_var a)
9.387 + | simple_combtype_of (TVar (x, _)) =
9.388 + CombTVar (make_schematic_type_var x, string_of_indexname x)
9.389 +
9.390 +(* Converts a term (with combinators) into a combterm. Also accummulates sort
9.391 + infomation. *)
9.392 +fun combterm_from_term thy bs (P $ Q) =
9.393 + let val (P', tsP) = combterm_from_term thy bs P
9.394 + val (Q', tsQ) = combterm_from_term thy bs Q
9.395 + in (CombApp (P', Q'), union (op =) tsP tsQ) end
9.396 + | combterm_from_term thy _ (Const (c, T)) =
9.397 + let
9.398 + val (tp, ts) = combtype_of T
9.399 + val tvar_list =
9.400 + (if String.isPrefix skolem_prefix c then
9.401 + [] |> Term.add_tvarsT T |> map TVar
9.402 + else
9.403 + (c, T) |> Sign.const_typargs thy)
9.404 + |> map simple_combtype_of
9.405 + val c' = CombConst (`make_fixed_const c, tp, tvar_list)
9.406 + in (c',ts) end
9.407 + | combterm_from_term _ _ (Free (v, T)) =
9.408 + let val (tp, ts) = combtype_of T
9.409 + val v' = CombConst (`make_fixed_var v, tp, [])
9.410 + in (v',ts) end
9.411 + | combterm_from_term _ _ (Var (v, T)) =
9.412 + let val (tp,ts) = combtype_of T
9.413 + val v' = CombVar ((make_schematic_var v, string_of_indexname v), tp)
9.414 + in (v',ts) end
9.415 + | combterm_from_term _ bs (Bound j) =
9.416 + let
9.417 + val (s, T) = nth bs j
9.418 + val (tp, ts) = combtype_of T
9.419 + val v' = CombConst (`make_bound_var s, tp, [])
9.420 + in (v', ts) end
9.421 + | combterm_from_term _ _ (Abs _) = raise Fail "HOL clause: Abs"
9.422 +
9.423 +fun predicate_of thy ((@{const Not} $ P), pos) = predicate_of thy (P, not pos)
9.424 + | predicate_of thy (t, pos) =
9.425 + (combterm_from_term thy [] (Envir.eta_contract t), pos)
9.426 +
9.427 +fun literals_of_term1 args thy (@{const Trueprop} $ P) =
9.428 + literals_of_term1 args thy P
9.429 + | literals_of_term1 args thy (@{const HOL.disj} $ P $ Q) =
9.430 + literals_of_term1 (literals_of_term1 args thy P) thy Q
9.431 + | literals_of_term1 (lits, ts) thy P =
9.432 + let val ((pred, ts'), pol) = predicate_of thy (P, true) in
9.433 + (FOLLiteral (pol, pred) :: lits, union (op =) ts ts')
9.434 + end
9.435 +val literals_of_term = literals_of_term1 ([], [])
9.436 +
9.437 +fun skolem_name i j num_T_args =
9.438 + skolem_prefix ^ Long_Name.separator ^
9.439 + (space_implode Long_Name.separator (map Int.toString [i, j, num_T_args]))
9.440 +
9.441 +fun conceal_skolem_terms i skolems t =
9.442 + if exists_Const (curry (op =) @{const_name skolem} o fst) t then
9.443 + let
9.444 + fun aux skolems
9.445 + (t as (Const (@{const_name skolem}, Type (_, [_, T])) $ _)) =
9.446 + let
9.447 + val (skolems, s) =
9.448 + if i = ~1 then
9.449 + (skolems, @{const_name undefined})
9.450 + else case AList.find (op aconv) skolems t of
9.451 + s :: _ => (skolems, s)
9.452 + | [] =>
9.453 + let
9.454 + val s = skolem_name i (length skolems)
9.455 + (length (Term.add_tvarsT T []))
9.456 + in ((s, t) :: skolems, s) end
9.457 + in (skolems, Const (s, T)) end
9.458 + | aux skolems (t1 $ t2) =
9.459 + let
9.460 + val (skolems, t1) = aux skolems t1
9.461 + val (skolems, t2) = aux skolems t2
9.462 + in (skolems, t1 $ t2) end
9.463 + | aux skolems (Abs (s, T, t')) =
9.464 + let val (skolems, t') = aux skolems t' in
9.465 + (skolems, Abs (s, T, t'))
9.466 + end
9.467 + | aux skolems t = (skolems, t)
9.468 + in aux skolems t end
9.469 + else
9.470 + (skolems, t)
9.471 +
9.472 +fun reveal_skolem_terms skolems =
9.473 + map_aterms (fn t as Const (s, _) =>
9.474 + if String.isPrefix skolem_prefix s then
9.475 + AList.lookup (op =) skolems s |> the
9.476 + |> map_types Type_Infer.paramify_vars
9.477 + else
9.478 + t
9.479 + | t => t)
9.480 +
9.481 +
9.482 +(***************************************************************)
9.483 +(* Type Classes Present in the Axiom or Conjecture Clauses *)
9.484 +(***************************************************************)
9.485 +
9.486 +fun set_insert (x, s) = Symtab.update (x, ()) s
9.487 +
9.488 +fun add_classes (sorts, cset) = List.foldl set_insert cset (flat sorts)
9.489 +
9.490 +(*Remove this trivial type class*)
9.491 +fun delete_type cset = Symtab.delete_safe (the_single @{sort HOL.type}) cset;
9.492 +
9.493 +fun tfree_classes_of_terms ts =
9.494 + let val sorts_list = map (map #2 o OldTerm.term_tfrees) ts
9.495 + in Symtab.keys (delete_type (List.foldl add_classes Symtab.empty sorts_list)) end;
9.496 +
9.497 +fun tvar_classes_of_terms ts =
9.498 + let val sorts_list = map (map #2 o OldTerm.term_tvars) ts
9.499 + in Symtab.keys (delete_type (List.foldl add_classes Symtab.empty sorts_list)) end;
9.500 +
9.501 +(*fold type constructors*)
9.502 +fun fold_type_consts f (Type (a, Ts)) x = fold (fold_type_consts f) Ts (f (a,x))
9.503 + | fold_type_consts _ _ x = x;
9.504 +
9.505 +(*Type constructors used to instantiate overloaded constants are the only ones needed.*)
9.506 +fun add_type_consts_in_term thy =
9.507 + let
9.508 + fun aux (Const x) =
9.509 + fold (fold_type_consts set_insert) (Sign.const_typargs thy x)
9.510 + | aux (Abs (_, _, u)) = aux u
9.511 + | aux (Const (@{const_name skolem}, _) $ _) = I
9.512 + | aux (t $ u) = aux t #> aux u
9.513 + | aux _ = I
9.514 + in aux end
9.515 +
9.516 +fun type_consts_of_terms thy ts =
9.517 + Symtab.keys (fold (add_type_consts_in_term thy) ts Symtab.empty);
9.518 +
9.519 +(* ------------------------------------------------------------------------- *)
9.520 +(* HOL to FOL (Isabelle to Metis) *)
9.521 +(* ------------------------------------------------------------------------- *)
9.522 +
9.523 +datatype mode = FO | HO | FT (* first-order, higher-order, fully-typed *)
9.524 +
9.525 +fun string_of_mode FO = "FO"
9.526 + | string_of_mode HO = "HO"
9.527 + | string_of_mode FT = "FT"
9.528 +
9.529 +fun fn_isa_to_met_sublevel "equal" = "=" (* FIXME: "c_fequal" *)
9.530 + | fn_isa_to_met_sublevel x = x
9.531 +fun fn_isa_to_met_toplevel "equal" = "="
9.532 + | fn_isa_to_met_toplevel x = x
9.533 +
9.534 +fun metis_lit b c args = (b, (c, args));
9.535 +
9.536 +fun metis_term_from_combtyp (CombTVar (s, _)) = Metis_Term.Var s
9.537 + | metis_term_from_combtyp (CombTFree (s, _)) = Metis_Term.Fn (s, [])
9.538 + | metis_term_from_combtyp (CombType ((s, _), tps)) =
9.539 + Metis_Term.Fn (s, map metis_term_from_combtyp tps);
9.540 +
9.541 +(*These two functions insert type literals before the real literals. That is the
9.542 + opposite order from TPTP linkup, but maybe OK.*)
9.543 +
9.544 +fun hol_term_to_fol_FO tm =
9.545 + case strip_combterm_comb tm of
9.546 + (CombConst ((c, _), _, tys), tms) =>
9.547 + let val tyargs = map metis_term_from_combtyp tys
9.548 + val args = map hol_term_to_fol_FO tms
9.549 + in Metis_Term.Fn (c, tyargs @ args) end
9.550 + | (CombVar ((v, _), _), []) => Metis_Term.Var v
9.551 + | _ => raise Fail "non-first-order combterm"
9.552 +
9.553 +fun hol_term_to_fol_HO (CombConst ((a, _), _, tylist)) =
9.554 + Metis_Term.Fn (fn_isa_to_met_sublevel a, map metis_term_from_combtyp tylist)
9.555 + | hol_term_to_fol_HO (CombVar ((s, _), _)) = Metis_Term.Var s
9.556 + | hol_term_to_fol_HO (CombApp (tm1, tm2)) =
9.557 + Metis_Term.Fn (".", map hol_term_to_fol_HO [tm1, tm2]);
9.558 +
9.559 +(*The fully-typed translation, to avoid type errors*)
9.560 +fun wrap_type (tm, ty) = Metis_Term.Fn("ti", [tm, metis_term_from_combtyp ty]);
9.561 +
9.562 +fun hol_term_to_fol_FT (CombVar ((s, _), ty)) = wrap_type (Metis_Term.Var s, ty)
9.563 + | hol_term_to_fol_FT (CombConst((a, _), ty, _)) =
9.564 + wrap_type (Metis_Term.Fn(fn_isa_to_met_sublevel a, []), ty)
9.565 + | hol_term_to_fol_FT (tm as CombApp(tm1,tm2)) =
9.566 + wrap_type (Metis_Term.Fn(".", map hol_term_to_fol_FT [tm1,tm2]),
9.567 + combtyp_of tm)
9.568 +
9.569 +fun hol_literal_to_fol FO (FOLLiteral (pos, tm)) =
9.570 + let val (CombConst((p, _), _, tys), tms) = strip_combterm_comb tm
9.571 + val tylits = if p = "equal" then [] else map metis_term_from_combtyp tys
9.572 + val lits = map hol_term_to_fol_FO tms
9.573 + in metis_lit pos (fn_isa_to_met_toplevel p) (tylits @ lits) end
9.574 + | hol_literal_to_fol HO (FOLLiteral (pos, tm)) =
9.575 + (case strip_combterm_comb tm of
9.576 + (CombConst(("equal", _), _, _), tms) =>
9.577 + metis_lit pos "=" (map hol_term_to_fol_HO tms)
9.578 + | _ => metis_lit pos "{}" [hol_term_to_fol_HO tm]) (*hBOOL*)
9.579 + | hol_literal_to_fol FT (FOLLiteral (pos, tm)) =
9.580 + (case strip_combterm_comb tm of
9.581 + (CombConst(("equal", _), _, _), tms) =>
9.582 + metis_lit pos "=" (map hol_term_to_fol_FT tms)
9.583 + | _ => metis_lit pos "{}" [hol_term_to_fol_FT tm]) (*hBOOL*);
9.584 +
9.585 +fun literals_of_hol_term thy mode t =
9.586 + let val (lits, types_sorts) = literals_of_term thy t
9.587 + in (map (hol_literal_to_fol mode) lits, types_sorts) end;
9.588 +
9.589 +(*Sign should be "true" for conjecture type constraints, "false" for type lits in clauses.*)
9.590 +fun metis_of_type_literals pos (TyLitVar ((s, _), (s', _))) =
9.591 + metis_lit pos s [Metis_Term.Var s']
9.592 + | metis_of_type_literals pos (TyLitFree ((s, _), (s', _))) =
9.593 + metis_lit pos s [Metis_Term.Fn (s',[])]
9.594 +
9.595 +fun default_sort _ (TVar _) = false
9.596 + | default_sort ctxt (TFree (x, s)) = (s = the_default [] (Variable.def_sort ctxt (x, ~1)));
9.597 +
9.598 +fun metis_of_tfree tf =
9.599 + Metis_Thm.axiom (Metis_LiteralSet.singleton (metis_of_type_literals true tf));
9.600 +
9.601 +fun hol_thm_to_fol is_conjecture ctxt type_lits mode j skolems th =
9.602 + let
9.603 + val thy = ProofContext.theory_of ctxt
9.604 + val (skolems, (mlits, types_sorts)) =
9.605 + th |> prop_of |> conceal_skolem_terms j skolems
9.606 + ||> (HOLogic.dest_Trueprop #> literals_of_hol_term thy mode)
9.607 + in
9.608 + if is_conjecture then
9.609 + (Metis_Thm.axiom (Metis_LiteralSet.fromList mlits),
9.610 + type_literals_for_types types_sorts, skolems)
9.611 + else
9.612 + let
9.613 + val tylits = filter_out (default_sort ctxt) types_sorts
9.614 + |> type_literals_for_types
9.615 + val mtylits =
9.616 + if type_lits then map (metis_of_type_literals false) tylits else []
9.617 + in
9.618 + (Metis_Thm.axiom (Metis_LiteralSet.fromList(mtylits @ mlits)), [],
9.619 + skolems)
9.620 + end
9.621 + end;
9.622 +
9.623 +val helpers =
9.624 + [("c_COMBI", (false, map (`I) @{thms COMBI_def})),
9.625 + ("c_COMBK", (false, map (`I) @{thms COMBK_def})),
9.626 + ("c_COMBB", (false, map (`I) @{thms COMBB_def})),
9.627 + ("c_COMBC", (false, map (`I) @{thms COMBC_def})),
9.628 + ("c_COMBS", (false, map (`I) @{thms COMBS_def})),
9.629 + ("c_fequal", (false, map (rpair @{thm equal_imp_equal})
9.630 + @{thms fequal_imp_equal equal_imp_fequal})),
9.631 + ("c_True", (true, map (`I) @{thms True_or_False})),
9.632 + ("c_False", (true, map (`I) @{thms True_or_False})),
9.633 + ("c_If", (true, map (`I) @{thms if_True if_False True_or_False}))]
9.634 +
9.635 +(* ------------------------------------------------------------------------- *)
9.636 +(* Logic maps manage the interface between HOL and first-order logic. *)
9.637 +(* ------------------------------------------------------------------------- *)
9.638 +
9.639 +type logic_map =
9.640 + {axioms: (Metis_Thm.thm * thm) list,
9.641 + tfrees: type_literal list,
9.642 + skolems: (string * term) list}
9.643 +
9.644 +fun is_quasi_fol_clause thy =
9.645 + Meson.is_fol_term thy o snd o conceal_skolem_terms ~1 [] o prop_of
9.646 +
9.647 +(*Extract TFree constraints from context to include as conjecture clauses*)
9.648 +fun init_tfrees ctxt =
9.649 + let fun add ((a,i),s) Ts = if i = ~1 then TFree(a,s) :: Ts else Ts in
9.650 + Vartab.fold add (#2 (Variable.constraints_of ctxt)) []
9.651 + |> type_literals_for_types
9.652 + end;
9.653 +
9.654 +(*Insert non-logical axioms corresponding to all accumulated TFrees*)
9.655 +fun add_tfrees {axioms, tfrees, skolems} : logic_map =
9.656 + {axioms = map (rpair TrueI o metis_of_tfree) (distinct (op =) tfrees) @
9.657 + axioms,
9.658 + tfrees = tfrees, skolems = skolems}
9.659 +
9.660 +(*transform isabelle type / arity clause to metis clause *)
9.661 +fun add_type_thm [] lmap = lmap
9.662 + | add_type_thm ((ith, mth) :: cls) {axioms, tfrees, skolems} =
9.663 + add_type_thm cls {axioms = (mth, ith) :: axioms, tfrees = tfrees,
9.664 + skolems = skolems}
9.665 +
9.666 +fun const_in_metis c (pred, tm_list) =
9.667 + let
9.668 + fun in_mterm (Metis_Term.Var _) = false
9.669 + | in_mterm (Metis_Term.Fn (".", tm_list)) = exists in_mterm tm_list
9.670 + | in_mterm (Metis_Term.Fn (nm, tm_list)) = c=nm orelse exists in_mterm tm_list
9.671 + in c = pred orelse exists in_mterm tm_list end;
9.672 +
9.673 +(* ARITY CLAUSE *)
9.674 +fun m_arity_cls (TConsLit ((c, _), (t, _), args)) =
9.675 + metis_lit true c [Metis_Term.Fn(t, map (Metis_Term.Var o fst) args)]
9.676 + | m_arity_cls (TVarLit ((c, _), (s, _))) =
9.677 + metis_lit false c [Metis_Term.Var s]
9.678 +(*TrueI is returned as the Isabelle counterpart because there isn't any.*)
9.679 +fun arity_cls (ArityClause {conclLit, premLits, ...}) =
9.680 + (TrueI,
9.681 + Metis_Thm.axiom (Metis_LiteralSet.fromList (map m_arity_cls (conclLit :: premLits))));
9.682 +
9.683 +(* CLASSREL CLAUSE *)
9.684 +fun m_class_rel_cls (subclass, _) (superclass, _) =
9.685 + [metis_lit false subclass [Metis_Term.Var "T"], metis_lit true superclass [Metis_Term.Var "T"]];
9.686 +fun class_rel_cls (ClassRelClause {subclass, superclass, ...}) =
9.687 + (TrueI, Metis_Thm.axiom (Metis_LiteralSet.fromList (m_class_rel_cls subclass superclass)));
9.688 +
9.689 +fun type_ext thy tms =
9.690 + let val subs = tfree_classes_of_terms tms
9.691 + val supers = tvar_classes_of_terms tms
9.692 + and tycons = type_consts_of_terms thy tms
9.693 + val (supers', arity_clauses) = make_arity_clauses thy tycons supers
9.694 + val class_rel_clauses = make_class_rel_clauses thy subs supers'
9.695 + in map class_rel_cls class_rel_clauses @ map arity_cls arity_clauses
9.696 + end;
9.697 +
9.698 +(* Function to generate metis clauses, including comb and type clauses *)
9.699 +fun build_logic_map mode0 ctxt type_lits cls ths =
9.700 + let val thy = ProofContext.theory_of ctxt
9.701 + (*The modes FO and FT are sticky. HO can be downgraded to FO.*)
9.702 + fun set_mode FO = FO
9.703 + | set_mode HO =
9.704 + if forall (is_quasi_fol_clause thy) (cls @ ths) then FO else HO
9.705 + | set_mode FT = FT
9.706 + val mode = set_mode mode0
9.707 + (*transform isabelle clause to metis clause *)
9.708 + fun add_thm is_conjecture (metis_ith, isa_ith) {axioms, tfrees, skolems}
9.709 + : logic_map =
9.710 + let
9.711 + val (mth, tfree_lits, skolems) =
9.712 + hol_thm_to_fol is_conjecture ctxt type_lits mode (length axioms)
9.713 + skolems metis_ith
9.714 + in
9.715 + {axioms = (mth, Meson.make_meta_clause isa_ith) :: axioms,
9.716 + tfrees = union (op =) tfree_lits tfrees, skolems = skolems}
9.717 + end;
9.718 + val lmap = {axioms = [], tfrees = init_tfrees ctxt, skolems = []}
9.719 + |> fold (add_thm true o `I) cls
9.720 + |> add_tfrees
9.721 + |> fold (add_thm false o `I) ths
9.722 + val clause_lists = map (Metis_Thm.clause o #1) (#axioms lmap)
9.723 + fun is_used c =
9.724 + exists (Metis_LiteralSet.exists (const_in_metis c o #2)) clause_lists
9.725 + val lmap =
9.726 + if mode = FO then
9.727 + lmap
9.728 + else
9.729 + let
9.730 + val helper_ths =
9.731 + helpers |> filter (is_used o fst)
9.732 + |> maps (fn (c, (needs_full_types, thms)) =>
9.733 + if not (is_used c) orelse
9.734 + needs_full_types andalso mode <> FT then
9.735 + []
9.736 + else
9.737 + thms)
9.738 + in lmap |> fold (add_thm false) helper_ths end
9.739 + in (mode, add_type_thm (type_ext thy (map prop_of (cls @ ths))) lmap) end
9.740 +
9.741 +end;
10.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML Fri Sep 17 16:15:45 2010 +0200
10.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML Fri Sep 17 16:38:11 2010 +0200
10.3 @@ -13,6 +13,7 @@
10.4 type relevance_override = Sledgehammer_Filter.relevance_override
10.5 type fol_formula = Sledgehammer_Translate.fol_formula
10.6 type minimize_command = Sledgehammer_Reconstruct.minimize_command
10.7 +
10.8 type params =
10.9 {blocking: bool,
10.10 debug: bool,
10.11 @@ -27,12 +28,14 @@
10.12 isar_shrink_factor: int,
10.13 timeout: Time.time,
10.14 expect: string}
10.15 +
10.16 type problem =
10.17 {state: Proof.state,
10.18 goal: thm,
10.19 subgoal: int,
10.20 axioms: (term * ((string * locality) * fol_formula) option) list,
10.21 only: bool}
10.22 +
10.23 type prover_result =
10.24 {outcome: failure option,
10.25 message: string,
10.26 @@ -43,6 +46,7 @@
10.27 tstplike_proof: string,
10.28 axiom_names: (string * locality) list vector,
10.29 conjecture_shape: int list list}
10.30 +
10.31 type prover = params -> minimize_command -> problem -> prover_result
10.32
10.33 val dest_dir : string Config.T
10.34 @@ -62,8 +66,9 @@
10.35 struct
10.36
10.37 open ATP_Problem
10.38 +open ATP_Proof
10.39 open ATP_Systems
10.40 -open Metis_Clauses
10.41 +open Metis_Translate
10.42 open Sledgehammer_Util
10.43 open Sledgehammer_Filter
10.44 open Sledgehammer_Translate
10.45 @@ -135,102 +140,11 @@
10.46 |> Exn.release
10.47 |> tap (after path)
10.48
10.49 -fun extract_delimited (begin_delim, end_delim) output =
10.50 - output |> first_field begin_delim |> the |> snd
10.51 - |> first_field end_delim |> the |> fst
10.52 - |> first_field "\n" |> the |> snd
10.53 - handle Option.Option => ""
10.54 +(* generic TPTP-based provers *)
10.55
10.56 -val tstp_important_message_delims =
10.57 - ("% SZS start RequiredInformation", "% SZS end RequiredInformation")
10.58 -
10.59 -fun extract_important_message output =
10.60 - case extract_delimited tstp_important_message_delims output of
10.61 - "" => ""
10.62 - | s => s |> space_explode "\n" |> filter_out (curry (op =) "")
10.63 - |> map (perhaps (try (unprefix "%")))
10.64 - |> map (perhaps (try (unprefix " ")))
10.65 - |> space_implode "\n " |> quote
10.66 -
10.67 -(* Splits by the first possible of a list of delimiters. *)
10.68 -fun extract_tstplike_proof delims output =
10.69 - case pairself (find_first (fn s => String.isSubstring s output))
10.70 - (ListPair.unzip delims) of
10.71 - (SOME begin_delim, SOME end_delim) =>
10.72 - extract_delimited (begin_delim, end_delim) output
10.73 - | _ => ""
10.74 -
10.75 -fun extract_tstplike_proof_and_outcome complete res_code proof_delims
10.76 - known_failures output =
10.77 - case known_failure_in_output output known_failures of
10.78 - NONE => (case extract_tstplike_proof proof_delims output of
10.79 - "" => ("", SOME (if res_code = 0 andalso output = "" then
10.80 - Interrupted
10.81 - else
10.82 - UnknownError))
10.83 - | tstplike_proof => if res_code = 0 then (tstplike_proof, NONE)
10.84 - else ("", SOME UnknownError))
10.85 - | SOME failure =>
10.86 - ("", SOME (if failure = IncompleteUnprovable andalso complete then
10.87 - Unprovable
10.88 - else
10.89 - failure))
10.90 -
10.91 -fun extract_clause_sequence output =
10.92 - let
10.93 - val tokens_of = String.tokens (not o Char.isAlphaNum)
10.94 - fun extract_num ("clause" :: (ss as _ :: _)) =
10.95 - Int.fromString (List.last ss)
10.96 - | extract_num _ = NONE
10.97 - in output |> split_lines |> map_filter (extract_num o tokens_of) end
10.98 -
10.99 -val set_ClauseFormulaRelationN = "set_ClauseFormulaRelation"
10.100 -
10.101 -val parse_clause_formula_pair =
10.102 - $$ "(" |-- scan_integer --| $$ ","
10.103 - -- (Symbol.scan_id ::: Scan.repeat ($$ "," |-- Symbol.scan_id)) --| $$ ")"
10.104 - --| Scan.option ($$ ",")
10.105 -val parse_clause_formula_relation =
10.106 - Scan.this_string set_ClauseFormulaRelationN |-- $$ "("
10.107 - |-- Scan.repeat parse_clause_formula_pair
10.108 -val extract_clause_formula_relation =
10.109 - Substring.full #> Substring.position set_ClauseFormulaRelationN
10.110 - #> snd #> Substring.position "." #> fst #> Substring.string
10.111 - #> explode #> filter_out Symbol.is_blank #> parse_clause_formula_relation
10.112 - #> fst
10.113 -
10.114 -(* TODO: move to "Sledgehammer_Reconstruct" *)
10.115 -fun repair_conjecture_shape_and_theorem_names output conjecture_shape
10.116 - axiom_names =
10.117 - if String.isSubstring set_ClauseFormulaRelationN output then
10.118 - (* This is a hack required for keeping track of axioms after they have been
10.119 - clausified by SPASS's Flotter tool. The "ATP/scripts/spass" script is
10.120 - also part of this hack. *)
10.121 - let
10.122 - val j0 = hd (hd conjecture_shape)
10.123 - val seq = extract_clause_sequence output
10.124 - val name_map = extract_clause_formula_relation output
10.125 - fun renumber_conjecture j =
10.126 - conjecture_prefix ^ string_of_int (j - j0)
10.127 - |> AList.find (fn (s, ss) => member (op =) ss s) name_map
10.128 - |> map (fn s => find_index (curry (op =) s) seq + 1)
10.129 - fun names_for_number j =
10.130 - j |> AList.lookup (op =) name_map |> these
10.131 - |> map_filter (try (unprefix axiom_prefix)) |> map unascii_of
10.132 - |> map (fn name =>
10.133 - (name, name |> find_first_in_list_vector axiom_names
10.134 - |> the)
10.135 - handle Option.Option =>
10.136 - error ("No such fact: " ^ quote name ^ "."))
10.137 - in
10.138 - (conjecture_shape |> map (maps renumber_conjecture),
10.139 - seq |> map names_for_number |> Vector.fromList)
10.140 - end
10.141 - else
10.142 - (conjecture_shape, axiom_names)
10.143 -
10.144 -
10.145 -(* generic TPTP-based provers *)
10.146 +(* Important messages are important but not so important that users want to see
10.147 + them each time. *)
10.148 +val important_message_keep_factor = 0.1
10.149
10.150 fun prover_fun auto atp_name
10.151 {exec, required_execs, arguments, has_incomplete_mode, proof_delims,
10.152 @@ -342,9 +256,13 @@
10.153 (output, msecs, tstplike_proof, outcome)) =
10.154 with_path cleanup export run_on problem_path_name
10.155 val (conjecture_shape, axiom_names) =
10.156 - repair_conjecture_shape_and_theorem_names output conjecture_shape
10.157 - axiom_names
10.158 - val important_message = extract_important_message output
10.159 + repair_conjecture_shape_and_axiom_names output conjecture_shape
10.160 + axiom_names
10.161 + val important_message =
10.162 + if random () <= important_message_keep_factor then
10.163 + extract_important_message output
10.164 + else
10.165 + ""
10.166 val banner = if auto then "Sledgehammer found a proof"
10.167 else "Try this command"
10.168 val (message, used_thm_names) =
11.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Fri Sep 17 16:15:45 2010 +0200
11.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Fri Sep 17 16:38:11 2010 +0200
11.3 @@ -20,7 +20,7 @@
11.4 structure Sledgehammer_Minimize : SLEDGEHAMMER_MINIMIZE =
11.5 struct
11.6
11.7 -open ATP_Systems
11.8 +open ATP_Proof
11.9 open Sledgehammer_Util
11.10 open Sledgehammer_Filter
11.11 open Sledgehammer_Translate
12.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Fri Sep 17 16:15:45 2010 +0200
12.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Fri Sep 17 16:38:11 2010 +0200
12.3 @@ -3,7 +3,7 @@
12.4 Author: Claire Quigley, Cambridge University Computer Laboratory
12.5 Author: Jasmin Blanchette, TU Muenchen
12.6
12.7 -Transfer of proofs from external provers.
12.8 +Proof reconstruction for Sledgehammer.
12.9 *)
12.10
12.11 signature SLEDGEHAMMER_RECONSTRUCT =
12.12 @@ -17,6 +17,9 @@
12.13 string Symtab.table * bool * int * Proof.context * int list list
12.14 type text_result = string * (string * locality) list
12.15
12.16 + val repair_conjecture_shape_and_axiom_names :
12.17 + string -> int list list -> (string * locality) list vector
12.18 + -> int list list * (string * locality) list vector
12.19 val metis_proof_text : metis_params -> text_result
12.20 val isar_proof_text : isar_params -> metis_params -> text_result
12.21 val proof_text : bool -> isar_params -> metis_params -> text_result
12.22 @@ -27,7 +30,7 @@
12.23
12.24 open ATP_Problem
12.25 open ATP_Proof
12.26 -open Metis_Clauses
12.27 +open Metis_Translate
12.28 open Sledgehammer_Util
12.29 open Sledgehammer_Filter
12.30 open Sledgehammer_Translate
12.31 @@ -40,6 +43,69 @@
12.32 string Symtab.table * bool * int * Proof.context * int list list
12.33 type text_result = string * (string * locality) list
12.34
12.35 +fun is_head_digit s = Char.isDigit (String.sub (s, 0))
12.36 +val scan_integer = Scan.many1 is_head_digit >> (the o Int.fromString o implode)
12.37 +
12.38 +fun find_first_in_list_vector vec key =
12.39 + Vector.foldl (fn (ps, NONE) => AList.lookup (op =) ps key
12.40 + | (_, value) => value) NONE vec
12.41 +
12.42 +
12.43 +(** SPASS's Flotter hack **)
12.44 +
12.45 +(* This is a hack required for keeping track of axioms after they have been
12.46 + clausified by SPASS's Flotter tool. The "ATP/scripts/spass" script is also
12.47 + part of this hack. *)
12.48 +
12.49 +val set_ClauseFormulaRelationN = "set_ClauseFormulaRelation"
12.50 +
12.51 +fun extract_clause_sequence output =
12.52 + let
12.53 + val tokens_of = String.tokens (not o Char.isAlphaNum)
12.54 + fun extract_num ("clause" :: (ss as _ :: _)) =
12.55 + Int.fromString (List.last ss)
12.56 + | extract_num _ = NONE
12.57 + in output |> split_lines |> map_filter (extract_num o tokens_of) end
12.58 +
12.59 +val parse_clause_formula_pair =
12.60 + $$ "(" |-- scan_integer --| $$ ","
12.61 + -- (Symbol.scan_id ::: Scan.repeat ($$ "," |-- Symbol.scan_id)) --| $$ ")"
12.62 + --| Scan.option ($$ ",")
12.63 +val parse_clause_formula_relation =
12.64 + Scan.this_string set_ClauseFormulaRelationN |-- $$ "("
12.65 + |-- Scan.repeat parse_clause_formula_pair
12.66 +val extract_clause_formula_relation =
12.67 + Substring.full #> Substring.position set_ClauseFormulaRelationN
12.68 + #> snd #> Substring.position "." #> fst #> Substring.string
12.69 + #> explode #> filter_out Symbol.is_blank #> parse_clause_formula_relation
12.70 + #> fst
12.71 +
12.72 +fun repair_conjecture_shape_and_axiom_names output conjecture_shape
12.73 + axiom_names =
12.74 + if String.isSubstring set_ClauseFormulaRelationN output then
12.75 + let
12.76 + val j0 = hd (hd conjecture_shape)
12.77 + val seq = extract_clause_sequence output
12.78 + val name_map = extract_clause_formula_relation output
12.79 + fun renumber_conjecture j =
12.80 + conjecture_prefix ^ string_of_int (j - j0)
12.81 + |> AList.find (fn (s, ss) => member (op =) ss s) name_map
12.82 + |> map (fn s => find_index (curry (op =) s) seq + 1)
12.83 + fun names_for_number j =
12.84 + j |> AList.lookup (op =) name_map |> these
12.85 + |> map_filter (try (unprefix axiom_prefix)) |> map unascii_of
12.86 + |> map (fn name =>
12.87 + (name, name |> find_first_in_list_vector axiom_names
12.88 + |> the)
12.89 + handle Option.Option =>
12.90 + error ("No such fact: " ^ quote name ^ "."))
12.91 + in
12.92 + (conjecture_shape |> map (maps renumber_conjecture),
12.93 + seq |> map names_for_number |> Vector.fromList)
12.94 + end
12.95 + else
12.96 + (conjecture_shape, axiom_names)
12.97 +
12.98
12.99 (** Soft-core proof reconstruction: Metis one-liner **)
12.100
13.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_translate.ML Fri Sep 17 16:15:45 2010 +0200
13.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_translate.ML Fri Sep 17 16:38:11 2010 +0200
13.3 @@ -3,7 +3,7 @@
13.4 Author: Makarius
13.5 Author: Jasmin Blanchette, TU Muenchen
13.6
13.7 -Translation of HOL to FOL.
13.8 +Translation of HOL to FOL for Sledgehammer.
13.9 *)
13.10
13.11 signature SLEDGEHAMMER_TRANSLATE =
13.12 @@ -30,7 +30,7 @@
13.13 struct
13.14
13.15 open ATP_Problem
13.16 -open Metis_Clauses
13.17 +open Metis_Translate
13.18 open Sledgehammer_Util
13.19
13.20 val axiom_prefix = "ax_"
14.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Fri Sep 17 16:15:45 2010 +0200
14.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Fri Sep 17 16:38:11 2010 +0200
14.3 @@ -6,13 +6,11 @@
14.4
14.5 signature SLEDGEHAMMER_UTIL =
14.6 sig
14.7 - val find_first_in_list_vector : (''a * 'b) list vector -> ''a -> 'b option
14.8 val plural_s : int -> string
14.9 val serial_commas : string -> string list -> string list
14.10 val simplify_spaces : string -> string
14.11 val parse_bool_option : bool -> string -> string -> bool option
14.12 val parse_time_option : string -> string -> Time.time option
14.13 - val scan_integer : string list -> int * string list
14.14 val nat_subscript : int -> string
14.15 val unyxml : string -> string
14.16 val maybe_quote : string -> string
14.17 @@ -28,10 +26,6 @@
14.18 structure Sledgehammer_Util : SLEDGEHAMMER_UTIL =
14.19 struct
14.20
14.21 -fun find_first_in_list_vector vec key =
14.22 - Vector.foldl (fn (ps, NONE) => AList.lookup (op =) ps key
14.23 - | (_, value) => value) NONE vec
14.24 -
14.25 fun plural_s n = if n = 1 then "" else "s"
14.26
14.27 fun serial_commas _ [] = ["??"]
14.28 @@ -72,9 +66,6 @@
14.29 SOME (Time.fromMilliseconds msecs)
14.30 end
14.31
14.32 -fun is_head_digit s = Char.isDigit (String.sub (s, 0))
14.33 -val scan_integer = Scan.many1 is_head_digit >> (the o Int.fromString o implode)
14.34 -
14.35 val subscript = implode o map (prefix "\<^isub>") o explode
14.36 fun nat_subscript n =
14.37 n |> string_of_int |> print_mode_active Symbol.xsymbolsN ? subscript
15.1 --- a/src/Tools/Metis/README Fri Sep 17 16:15:45 2010 +0200
15.2 +++ b/src/Tools/Metis/README Fri Sep 17 16:38:11 2010 +0200
15.3 @@ -8,7 +8,7 @@
15.4 1. The files "Makefile" and "script/mlpp" and the directory "src/"
15.5 were initially copied from Joe Hurd's official Metis package. The
15.6 package that was used when these notes where written was Metis 2.3
15.7 - (15 Sept. 2010).
15.8 + (16 Sept. 2010).
15.9
15.10 2. The license in each source file will probably not be something we
15.11 can use in Isabelle. The "fix_metis_license" script can be run to
15.12 @@ -20,11 +20,11 @@
15.13 as part of Isabelle, with the Metis code covered under the
15.14 Isabelle BSD license.
15.15
15.16 - 3. Some modifications have to be done manually to the source files.
15.17 - The ultimate way to track them down is to use Mercurial. The
15.18 - command
15.19 + 3. Some modifications might have to be done manually to the source
15.20 + files. The ultimate way to track them down is to use Mercurial.
15.21 + The command
15.22
15.23 - hg diff -rbeabb8443ee4: src
15.24 + hg diff -rcffceed8e7fa: src
15.25
15.26 should do the trick. You might need to specify a different
15.27 revision number if somebody updated the Metis sources without
15.28 @@ -55,4 +55,4 @@
15.29 Good luck!
15.30
15.31 Jasmin Blanchette
15.32 - 16 Sept. 2010
15.33 + 17 Sept. 2010
16.1 --- a/src/Tools/Metis/metis.ML Fri Sep 17 16:15:45 2010 +0200
16.2 +++ b/src/Tools/Metis/metis.ML Fri Sep 17 16:38:11 2010 +0200
16.3 @@ -967,49 +967,32 @@
16.4 end;
16.5
16.6 local
16.7 - fun calcPrimes ps n i =
16.8 - if List.exists (fn p => divides p i) ps then calcPrimes ps n (i + 1)
16.9 + fun calcPrimes mode ps i n =
16.10 + if n = 0 then ps
16.11 + else if List.exists (fn p => divides p i) ps then
16.12 + let
16.13 + val i = i + 1
16.14 + and n = if mode then n else n - 1
16.15 + in
16.16 + calcPrimes mode ps i n
16.17 + end
16.18 else
16.19 let
16.20 val ps = ps @ [i]
16.21 + and i = i + 1
16.22 and n = n - 1
16.23 in
16.24 - if n = 0 then ps else calcPrimes ps n (i + 1)
16.25 + calcPrimes mode ps i n
16.26 end;
16.27 -
16.28 - val primesList = Unsynchronized.ref [2];
16.29 -in
16.30 - fun primes n = Metis_Portable.critical (fn () =>
16.31 - let
16.32 - val Unsynchronized.ref ps = primesList
16.33 -
16.34 - val k = n - length ps
16.35 - in
16.36 - if k <= 0 then List.take (ps,n)
16.37 - else
16.38 - let
16.39 - val ps = calcPrimes ps k (List.last ps + 1)
16.40 -
16.41 - val () = primesList := ps
16.42 - in
16.43 - ps
16.44 - end
16.45 - end) ();
16.46 -end;
16.47 -
16.48 -fun primesUpTo n = Metis_Portable.critical (fn () =>
16.49 - let
16.50 - fun f k =
16.51 - let
16.52 - val l = primes k
16.53 -
16.54 - val p = List.last l
16.55 - in
16.56 - if p < n then f (2 * k) else takeWhile (fn j => j <= n) l
16.57 - end
16.58 - in
16.59 - f 8
16.60 - end) ();
16.61 +in
16.62 + fun primes n =
16.63 + if n <= 0 then []
16.64 + else calcPrimes true [2] 3 (n - 1);
16.65 +
16.66 + fun primesUpTo n =
16.67 + if n < 2 then []
16.68 + else calcPrimes false [2] 3 (n - 2);
16.69 +end;
16.70
16.71 (* ------------------------------------------------------------------------- *)
16.72 (* Strings. *)
16.73 @@ -1228,23 +1211,30 @@
16.74
16.75 local
16.76 val generator = Unsynchronized.ref 0
16.77 -in
16.78 - fun newInt () = Metis_Portable.critical (fn () =>
16.79 +
16.80 + fun newIntThunk () =
16.81 let
16.82 val n = !generator
16.83 +
16.84 val () = generator := n + 1
16.85 in
16.86 n
16.87 - end) ();
16.88 -
16.89 - fun newInts 0 = []
16.90 - | newInts k = Metis_Portable.critical (fn () =>
16.91 + end;
16.92 +
16.93 + fun newIntsThunk k () =
16.94 let
16.95 val n = !generator
16.96 +
16.97 val () = generator := n + k
16.98 in
16.99 interval n k
16.100 - end) ();
16.101 + end;
16.102 +in
16.103 + fun newInt () = Metis_Portable.critical newIntThunk ();
16.104 +
16.105 + fun newInts k =
16.106 + if k <= 0 then []
16.107 + else Metis_Portable.critical (newIntsThunk k) ();
16.108 end;
16.109
16.110 fun withRef (r,new) f x =
16.111 @@ -14197,24 +14187,23 @@
16.112 (* Basic conjunctive normal form. *)
16.113 (* ------------------------------------------------------------------------- *)
16.114
16.115 -val newSkolemFunction =
16.116 - let
16.117 - val counter : int Metis_StringMap.map Unsynchronized.ref = Unsynchronized.ref (Metis_StringMap.new ())
16.118 -
16.119 - fun new n () =
16.120 - let
16.121 - val Unsynchronized.ref m = counter
16.122 - val s = Metis_Name.toString n
16.123 - val i = Option.getOpt (Metis_StringMap.peek m s, 0)
16.124 - val () = counter := Metis_StringMap.insert m (s, i + 1)
16.125 - val i = if i = 0 then "" else "_" ^ Int.toString i
16.126 - val s = skolemPrefix ^ "_" ^ s ^ i
16.127 - in
16.128 - Metis_Name.fromString s
16.129 - end
16.130 - in
16.131 - fn n => Metis_Portable.critical (new n) ()
16.132 - end;
16.133 +local
16.134 + val counter : int Metis_StringMap.map Unsynchronized.ref = Unsynchronized.ref (Metis_StringMap.new ());
16.135 +
16.136 + fun new n () =
16.137 + let
16.138 + val Unsynchronized.ref m = counter
16.139 + val s = Metis_Name.toString n
16.140 + val i = Option.getOpt (Metis_StringMap.peek m s, 0)
16.141 + val () = counter := Metis_StringMap.insert m (s, i + 1)
16.142 + val i = if i = 0 then "" else "_" ^ Int.toString i
16.143 + val s = skolemPrefix ^ "_" ^ s ^ i
16.144 + in
16.145 + Metis_Name.fromString s
16.146 + end;
16.147 +in
16.148 + fun newSkolemFunction n = Metis_Portable.critical (new n) ();
16.149 +end;
16.150
16.151 fun skolemize fv bv fm =
16.152 let
16.153 @@ -14753,18 +14742,19 @@
16.154 (* Definitions. *)
16.155 (* ------------------------------------------------------------------------- *)
16.156
16.157 -val newDefinitionRelation =
16.158 - let
16.159 - val counter : int Unsynchronized.ref = Unsynchronized.ref 0
16.160 - in
16.161 - fn () => Metis_Portable.critical (fn () =>
16.162 - let
16.163 - val Unsynchronized.ref i = counter
16.164 - val () = counter := i + 1
16.165 - in
16.166 - definitionPrefix ^ "_" ^ Int.toString i
16.167 - end) ()
16.168 - end;
16.169 +local
16.170 + val counter : int Unsynchronized.ref = Unsynchronized.ref 0;
16.171 +
16.172 + fun new () =
16.173 + let
16.174 + val Unsynchronized.ref i = counter
16.175 + val () = counter := i + 1
16.176 + in
16.177 + definitionPrefix ^ "_" ^ Int.toString i
16.178 + end;
16.179 +in
16.180 + fun newDefinitionRelation () = Metis_Portable.critical new ();
16.181 +end;
16.182
16.183 fun newDefinition def =
16.184 let
17.1 --- a/src/Tools/Metis/src/Normalize.sml Fri Sep 17 16:15:45 2010 +0200
17.2 +++ b/src/Tools/Metis/src/Normalize.sml Fri Sep 17 16:38:11 2010 +0200
17.3 @@ -685,24 +685,23 @@
17.4 (* Basic conjunctive normal form. *)
17.5 (* ------------------------------------------------------------------------- *)
17.6
17.7 -val newSkolemFunction =
17.8 - let
17.9 - val counter : int StringMap.map ref = ref (StringMap.new ())
17.10 +local
17.11 + val counter : int StringMap.map ref = ref (StringMap.new ());
17.12
17.13 - fun new n () =
17.14 - let
17.15 - val ref m = counter
17.16 - val s = Name.toString n
17.17 - val i = Option.getOpt (StringMap.peek m s, 0)
17.18 - val () = counter := StringMap.insert m (s, i + 1)
17.19 - val i = if i = 0 then "" else "_" ^ Int.toString i
17.20 - val s = skolemPrefix ^ "_" ^ s ^ i
17.21 - in
17.22 - Name.fromString s
17.23 - end
17.24 - in
17.25 - fn n => Portable.critical (new n) ()
17.26 - end;
17.27 + fun new n () =
17.28 + let
17.29 + val ref m = counter
17.30 + val s = Name.toString n
17.31 + val i = Option.getOpt (StringMap.peek m s, 0)
17.32 + val () = counter := StringMap.insert m (s, i + 1)
17.33 + val i = if i = 0 then "" else "_" ^ Int.toString i
17.34 + val s = skolemPrefix ^ "_" ^ s ^ i
17.35 + in
17.36 + Name.fromString s
17.37 + end;
17.38 +in
17.39 + fun newSkolemFunction n = Portable.critical (new n) ();
17.40 +end;
17.41
17.42 fun skolemize fv bv fm =
17.43 let
17.44 @@ -1241,18 +1240,19 @@
17.45 (* Definitions. *)
17.46 (* ------------------------------------------------------------------------- *)
17.47
17.48 -val newDefinitionRelation =
17.49 - let
17.50 - val counter : int ref = ref 0
17.51 - in
17.52 - fn () => Portable.critical (fn () =>
17.53 - let
17.54 - val ref i = counter
17.55 - val () = counter := i + 1
17.56 - in
17.57 - definitionPrefix ^ "_" ^ Int.toString i
17.58 - end) ()
17.59 - end;
17.60 +local
17.61 + val counter : int ref = ref 0;
17.62 +
17.63 + fun new () =
17.64 + let
17.65 + val ref i = counter
17.66 + val () = counter := i + 1
17.67 + in
17.68 + definitionPrefix ^ "_" ^ Int.toString i
17.69 + end;
17.70 +in
17.71 + fun newDefinitionRelation () = Portable.critical new ();
17.72 +end;
17.73
17.74 fun newDefinition def =
17.75 let
18.1 --- a/src/Tools/Metis/src/Useful.sml Fri Sep 17 16:15:45 2010 +0200
18.2 +++ b/src/Tools/Metis/src/Useful.sml Fri Sep 17 16:38:11 2010 +0200
18.3 @@ -462,50 +462,33 @@
18.4 end;
18.5
18.6 local
18.7 - fun calcPrimes ps n i =
18.8 - if List.exists (fn p => divides p i) ps then calcPrimes ps n (i + 1)
18.9 + fun calcPrimes mode ps i n =
18.10 + if n = 0 then ps
18.11 + else if List.exists (fn p => divides p i) ps then
18.12 + let
18.13 + val i = i + 1
18.14 + and n = if mode then n else n - 1
18.15 + in
18.16 + calcPrimes mode ps i n
18.17 + end
18.18 else
18.19 let
18.20 val ps = ps @ [i]
18.21 + and i = i + 1
18.22 and n = n - 1
18.23 in
18.24 - if n = 0 then ps else calcPrimes ps n (i + 1)
18.25 + calcPrimes mode ps i n
18.26 end;
18.27 +in
18.28 + fun primes n =
18.29 + if n <= 0 then []
18.30 + else calcPrimes true [2] 3 (n - 1);
18.31
18.32 - val primesList = ref [2];
18.33 -in
18.34 - fun primes n = Portable.critical (fn () =>
18.35 - let
18.36 - val ref ps = primesList
18.37 -
18.38 - val k = n - length ps
18.39 - in
18.40 - if k <= 0 then List.take (ps,n)
18.41 - else
18.42 - let
18.43 - val ps = calcPrimes ps k (List.last ps + 1)
18.44 -
18.45 - val () = primesList := ps
18.46 - in
18.47 - ps
18.48 - end
18.49 - end) ();
18.50 + fun primesUpTo n =
18.51 + if n < 2 then []
18.52 + else calcPrimes false [2] 3 (n - 2);
18.53 end;
18.54
18.55 -fun primesUpTo n = Portable.critical (fn () =>
18.56 - let
18.57 - fun f k =
18.58 - let
18.59 - val l = primes k
18.60 -
18.61 - val p = List.last l
18.62 - in
18.63 - if p < n then f (2 * k) else takeWhile (fn j => j <= n) l
18.64 - end
18.65 - in
18.66 - f 8
18.67 - end) ();
18.68 -
18.69 (* ------------------------------------------------------------------------- *)
18.70 (* Strings. *)
18.71 (* ------------------------------------------------------------------------- *)
18.72 @@ -723,23 +706,30 @@
18.73
18.74 local
18.75 val generator = ref 0
18.76 -in
18.77 - fun newInt () = Portable.critical (fn () =>
18.78 +
18.79 + fun newIntThunk () =
18.80 let
18.81 val n = !generator
18.82 +
18.83 val () = generator := n + 1
18.84 in
18.85 n
18.86 - end) ();
18.87 + end;
18.88
18.89 - fun newInts 0 = []
18.90 - | newInts k = Portable.critical (fn () =>
18.91 + fun newIntsThunk k () =
18.92 let
18.93 val n = !generator
18.94 +
18.95 val () = generator := n + k
18.96 in
18.97 interval n k
18.98 - end) ();
18.99 + end;
18.100 +in
18.101 + fun newInt () = Portable.critical newIntThunk ();
18.102 +
18.103 + fun newInts k =
18.104 + if k <= 0 then []
18.105 + else Portable.critical (newIntsThunk k) ();
18.106 end;
18.107
18.108 fun withRef (r,new) f x =
19.1 --- a/src/Tools/Metis/src/metis.sml Fri Sep 17 16:15:45 2010 +0200
19.2 +++ b/src/Tools/Metis/src/metis.sml Fri Sep 17 16:38:11 2010 +0200
19.3 @@ -13,7 +13,7 @@
19.4
19.5 val VERSION = "2.3";
19.6
19.7 -val versionString = PROGRAM^" "^VERSION^" (release 20100915)"^"\n";
19.8 +val versionString = PROGRAM^" "^VERSION^" (release 20100916)"^"\n";
19.9
19.10 (* ------------------------------------------------------------------------- *)
19.11 (* Program options. *)