author  blanchet 
Tue, 20 Mar 2012 13:53:09 +0100  
changeset 47045  631adf003bb0 
parent 47039  1b36a05a070d 
child 47047  10bece4ac87e 
permissions  rwrr 
44651
5d6a11e166cf
renamed "Metis_Tactics" to "Metis_Tactic", now that there is only one Metis tactic ("metisFT" is legacy)
blanchet
parents:
44634
diff
changeset

1 
(* Title: HOL/Tools/Metis/metis_tactic.ML 
38027  2 
Author: Kong W. Susanto, Cambridge University Computer Laboratory 
3 
Author: Lawrence C. Paulson, Cambridge University Computer Laboratory 

4 
Author: Jasmin Blanchette, TU Muenchen 

23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

5 
Copyright Cambridge University 2007 
23447  6 

29266  7 
HOL setup for the Metis prover. 
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

8 
*) 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

9 

44651
5d6a11e166cf
renamed "Metis_Tactics" to "Metis_Tactic", now that there is only one Metis tactic ("metisFT" is legacy)
blanchet
parents:
44634
diff
changeset

10 
signature METIS_TACTIC = 
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

11 
sig 
39979
b13515940b53
added "trace_meson" configuration option, replacing oldfashioned reference
blanchet
parents:
39978
diff
changeset

12 
val trace : bool Config.T 
40665
1a65f0c74827
added "verbose" option to Metis to shut up its warnings if necessary
blanchet
parents:
40262
diff
changeset

13 
val verbose : bool Config.T 
39891
8e12f1956fcd
"meson_new_skolemizer" > "metis_new_skolemizer" option (since Meson doesn't support the new skolemizer (yet))
blanchet
parents:
39890
diff
changeset

14 
val new_skolemizer : bool Config.T 
47039
1b36a05a070d
added "metis_advisory_simp" option to orient as many equations as possible in Metis the right way (cf. "More SPASS with Isabelle")
blanchet
parents:
47015
diff
changeset

15 
val advisory_simp : bool Config.T 
44934  16 
val type_has_top_sort : typ > bool 
45514  17 
val metis_tac : 
18 
string list > string > Proof.context > thm list > int > tactic 

45521  19 
val metis_lam_transs : string list 
45519
cd6e78cb6ee8
make metis reconstruction handling more flexible
blanchet
parents:
45514
diff
changeset

20 
val parse_metis_options : (string list option * string option) parser 
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset

21 
val setup : theory > theory 
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

22 
end 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

23 

44651
5d6a11e166cf
renamed "Metis_Tactics" to "Metis_Tactic", now that there is only one Metis tactic ("metisFT" is legacy)
blanchet
parents:
44634
diff
changeset

24 
structure Metis_Tactic : METIS_TACTIC = 
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

25 
struct 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

26 

46320  27 
open ATP_Problem_Generate 
28 
open ATP_Proof_Reconstruct 

29 
open Metis_Generate 

39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset

30 
open Metis_Reconstruct 
35826  31 

43089  32 
val new_skolemizer = 
33 
Attrib.setup_config_bool @{binding metis_new_skolemizer} (K false) 

47039
1b36a05a070d
added "metis_advisory_simp" option to orient as many equations as possible in Metis the right way (cf. "More SPASS with Isabelle")
blanchet
parents:
47015
diff
changeset

34 
val advisory_simp = 
47045  35 
Attrib.setup_config_bool @{binding metis_advisory_simp} (K true) 
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

36 

43134
0c82e00ba63e
make sure no warnings are given for polymorphic facts where we use a monomorphic instance
blanchet
parents:
43133
diff
changeset

37 
(* Designed to work also with monomorphic instances of polymorphic theorems. *) 
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset

38 
fun have_common_thm ths1 ths2 = 
43301
8d7fc4a5b502
removed needless function that duplicated standard functionality, with a little unnecessary twist
blanchet
parents:
43299
diff
changeset

39 
exists (member (Term.aconv_untyped o pairself prop_of) ths1) 
43134
0c82e00ba63e
make sure no warnings are given for polymorphic facts where we use a monomorphic instance
blanchet
parents:
43133
diff
changeset

40 
(map Meson.make_meta_clause ths2) 
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

41 

32956  42 
(*Determining which axiom clauses are actually used*) 
39419
c9accfd621a5
"Metis." > "Metis_" to reflect change in "metis.ML"
blanchet
parents:
39376
diff
changeset

43 
fun used_axioms axioms (th, Metis_Proof.Axiom _) = SOME (lookth axioms th) 
43128  44 
 used_axioms _ _ = NONE 
24855  45 

43129  46 
(* Lightweight predicate type information comes in two flavors, "t = t'" and 
47 
"t => t'", where "t" and "t'" are the same term modulo type tags. 

48 
In Isabelle, type tags are stripped away, so we are left with "t = t" or 

43159
29b55f292e0b
added support for helpers in new Metis, so far only for polymorphic type encodings
blanchet
parents:
43136
diff
changeset

49 
"t => t". Type tag idempotence is also handled this way. *) 
45508  50 
fun reflexive_or_trivial_from_metis ctxt type_enc sym_tab concealed mth = 
43136
cf5cda219058
handle lightweight tags sym theorems gracefully in the presence of TVars with interesting type classes
blanchet
parents:
43135
diff
changeset

51 
let val thy = Proof_Context.theory_of ctxt in 
45508  52 
case hol_clause_from_metis ctxt type_enc sym_tab concealed mth of 
43136
cf5cda219058
handle lightweight tags sym theorems gracefully in the presence of TVars with interesting type classes
blanchet
parents:
43135
diff
changeset

53 
Const (@{const_name HOL.eq}, _) $ _ $ t => 
44408
30ea62ab4f16
made reconstruction of type tag equalities "\?x = \?x" reliable
blanchet
parents:
44402
diff
changeset

54 
let 
30ea62ab4f16
made reconstruction of type tag equalities "\?x = \?x" reliable
blanchet
parents:
44402
diff
changeset

55 
val ct = cterm_of thy t 
30ea62ab4f16
made reconstruction of type tag equalities "\?x = \?x" reliable
blanchet
parents:
44402
diff
changeset

56 
val cT = ctyp_of_term ct 
30ea62ab4f16
made reconstruction of type tag equalities "\?x = \?x" reliable
blanchet
parents:
44402
diff
changeset

57 
in refl > Drule.instantiate' [SOME cT] [SOME ct] end 
43136
cf5cda219058
handle lightweight tags sym theorems gracefully in the presence of TVars with interesting type classes
blanchet
parents:
43135
diff
changeset

58 
 Const (@{const_name disj}, _) $ t1 $ t2 => 
cf5cda219058
handle lightweight tags sym theorems gracefully in the presence of TVars with interesting type classes
blanchet
parents:
43135
diff
changeset

59 
(if can HOLogic.dest_not t1 then t2 else t1) 
cf5cda219058
handle lightweight tags sym theorems gracefully in the presence of TVars with interesting type classes
blanchet
parents:
43135
diff
changeset

60 
> HOLogic.mk_Trueprop > cterm_of thy > Thm.trivial 
45511
9b0f8ca4388e
continued implementation of lambdalifting in Metis
blanchet
parents:
45508
diff
changeset

61 
 _ => raise Fail "expected reflexive or trivial clause" 
43136
cf5cda219058
handle lightweight tags sym theorems gracefully in the presence of TVars with interesting type classes
blanchet
parents:
43135
diff
changeset

62 
end 
43129  63 
> Meson.make_meta_clause 
64 

45569
eb30a5490543
wrap lambdas earlier, to get more control over beta/eta
blanchet
parents:
45568
diff
changeset

65 
fun lam_lifted_from_metis ctxt type_enc sym_tab concealed mth = 
45511
9b0f8ca4388e
continued implementation of lambdalifting in Metis
blanchet
parents:
45508
diff
changeset

66 
let 
9b0f8ca4388e
continued implementation of lambdalifting in Metis
blanchet
parents:
45508
diff
changeset

67 
val thy = Proof_Context.theory_of ctxt 
46904  68 
val tac = rewrite_goals_tac @{thms lambda_def [abs_def]} THEN rtac refl 1 
45511
9b0f8ca4388e
continued implementation of lambdalifting in Metis
blanchet
parents:
45508
diff
changeset

69 
val t = hol_clause_from_metis ctxt type_enc sym_tab concealed mth 
9b0f8ca4388e
continued implementation of lambdalifting in Metis
blanchet
parents:
45508
diff
changeset

70 
val ct = cterm_of thy (HOLogic.mk_Trueprop t) 
9b0f8ca4388e
continued implementation of lambdalifting in Metis
blanchet
parents:
45508
diff
changeset

71 
in Goal.prove_internal [] ct (K tac) > Meson.make_meta_clause end 
9b0f8ca4388e
continued implementation of lambdalifting in Metis
blanchet
parents:
45508
diff
changeset

72 

45570
6d95a66cce00
pull variables (Var) out of lambdas, so that the Isabelle theorems closely mirror the Metis lambdalifted ones
blanchet
parents:
45569
diff
changeset

73 
fun add_vars_and_frees (t $ u) = fold (add_vars_and_frees) [t, u] 
6d95a66cce00
pull variables (Var) out of lambdas, so that the Isabelle theorems closely mirror the Metis lambdalifted ones
blanchet
parents:
45569
diff
changeset

74 
 add_vars_and_frees (Abs (_, _, t)) = add_vars_and_frees t 
6d95a66cce00
pull variables (Var) out of lambdas, so that the Isabelle theorems closely mirror the Metis lambdalifted ones
blanchet
parents:
45569
diff
changeset

75 
 add_vars_and_frees (t as Var _) = insert (op =) t 
6d95a66cce00
pull variables (Var) out of lambdas, so that the Isabelle theorems closely mirror the Metis lambdalifted ones
blanchet
parents:
45569
diff
changeset

76 
 add_vars_and_frees (t as Free _) = insert (op =) t 
6d95a66cce00
pull variables (Var) out of lambdas, so that the Isabelle theorems closely mirror the Metis lambdalifted ones
blanchet
parents:
45569
diff
changeset

77 
 add_vars_and_frees _ = I 
6d95a66cce00
pull variables (Var) out of lambdas, so that the Isabelle theorems closely mirror the Metis lambdalifted ones
blanchet
parents:
45569
diff
changeset

78 

45569
eb30a5490543
wrap lambdas earlier, to get more control over beta/eta
blanchet
parents:
45568
diff
changeset

79 
fun introduce_lam_wrappers ctxt th = 
45511
9b0f8ca4388e
continued implementation of lambdalifting in Metis
blanchet
parents:
45508
diff
changeset

80 
if Meson_Clausify.is_quasi_lambda_free (prop_of th) then 
9b0f8ca4388e
continued implementation of lambdalifting in Metis
blanchet
parents:
45508
diff
changeset

81 
th 
9b0f8ca4388e
continued implementation of lambdalifting in Metis
blanchet
parents:
45508
diff
changeset

82 
else 
9b0f8ca4388e
continued implementation of lambdalifting in Metis
blanchet
parents:
45508
diff
changeset

83 
let 
45570
6d95a66cce00
pull variables (Var) out of lambdas, so that the Isabelle theorems closely mirror the Metis lambdalifted ones
blanchet
parents:
45569
diff
changeset

84 
val thy = Proof_Context.theory_of ctxt 
6d95a66cce00
pull variables (Var) out of lambdas, so that the Isabelle theorems closely mirror the Metis lambdalifted ones
blanchet
parents:
45569
diff
changeset

85 
fun conv first ctxt ct = 
45511
9b0f8ca4388e
continued implementation of lambdalifting in Metis
blanchet
parents:
45508
diff
changeset

86 
if Meson_Clausify.is_quasi_lambda_free (term_of ct) then 
9b0f8ca4388e
continued implementation of lambdalifting in Metis
blanchet
parents:
45508
diff
changeset

87 
Thm.reflexive ct 
9b0f8ca4388e
continued implementation of lambdalifting in Metis
blanchet
parents:
45508
diff
changeset

88 
else case term_of ct of 
45883  89 
Abs (_, _, u) => 
45570
6d95a66cce00
pull variables (Var) out of lambdas, so that the Isabelle theorems closely mirror the Metis lambdalifted ones
blanchet
parents:
45569
diff
changeset

90 
if first then 
6d95a66cce00
pull variables (Var) out of lambdas, so that the Isabelle theorems closely mirror the Metis lambdalifted ones
blanchet
parents:
45569
diff
changeset

91 
case add_vars_and_frees u [] of 
6d95a66cce00
pull variables (Var) out of lambdas, so that the Isabelle theorems closely mirror the Metis lambdalifted ones
blanchet
parents:
45569
diff
changeset

92 
[] => 
6d95a66cce00
pull variables (Var) out of lambdas, so that the Isabelle theorems closely mirror the Metis lambdalifted ones
blanchet
parents:
45569
diff
changeset

93 
Conv.abs_conv (conv false o snd) ctxt ct 
6d95a66cce00
pull variables (Var) out of lambdas, so that the Isabelle theorems closely mirror the Metis lambdalifted ones
blanchet
parents:
45569
diff
changeset

94 
> (fn th => Meson.first_order_resolve th @{thm Metis.eq_lambdaI}) 
6d95a66cce00
pull variables (Var) out of lambdas, so that the Isabelle theorems closely mirror the Metis lambdalifted ones
blanchet
parents:
45569
diff
changeset

95 
 v :: _ => 
6d95a66cce00
pull variables (Var) out of lambdas, so that the Isabelle theorems closely mirror the Metis lambdalifted ones
blanchet
parents:
45569
diff
changeset

96 
Abs (Name.uu, fastype_of v, abstract_over (v, term_of ct)) $ v 
6d95a66cce00
pull variables (Var) out of lambdas, so that the Isabelle theorems closely mirror the Metis lambdalifted ones
blanchet
parents:
45569
diff
changeset

97 
> cterm_of thy 
6d95a66cce00
pull variables (Var) out of lambdas, so that the Isabelle theorems closely mirror the Metis lambdalifted ones
blanchet
parents:
45569
diff
changeset

98 
> Conv.comb_conv (conv true ctxt) 
6d95a66cce00
pull variables (Var) out of lambdas, so that the Isabelle theorems closely mirror the Metis lambdalifted ones
blanchet
parents:
45569
diff
changeset

99 
else 
6d95a66cce00
pull variables (Var) out of lambdas, so that the Isabelle theorems closely mirror the Metis lambdalifted ones
blanchet
parents:
45569
diff
changeset

100 
Conv.abs_conv (conv false o snd) ctxt ct 
6d95a66cce00
pull variables (Var) out of lambdas, so that the Isabelle theorems closely mirror the Metis lambdalifted ones
blanchet
parents:
45569
diff
changeset

101 
 Const (@{const_name Meson.skolem}, _) $ _ => Thm.reflexive ct 
45511
9b0f8ca4388e
continued implementation of lambdalifting in Metis
blanchet
parents:
45508
diff
changeset

102 
 _ => Conv.comb_conv (conv true ctxt) ct 
45570
6d95a66cce00
pull variables (Var) out of lambdas, so that the Isabelle theorems closely mirror the Metis lambdalifted ones
blanchet
parents:
45569
diff
changeset

103 
val eq_th = conv true ctxt (cprop_of th) 
6d95a66cce00
pull variables (Var) out of lambdas, so that the Isabelle theorems closely mirror the Metis lambdalifted ones
blanchet
parents:
45569
diff
changeset

104 
(* We replace the equation's lefthand side with a betaequivalent term 
6d95a66cce00
pull variables (Var) out of lambdas, so that the Isabelle theorems closely mirror the Metis lambdalifted ones
blanchet
parents:
45569
diff
changeset

105 
so that "Thm.equal_elim" works below. *) 
6d95a66cce00
pull variables (Var) out of lambdas, so that the Isabelle theorems closely mirror the Metis lambdalifted ones
blanchet
parents:
45569
diff
changeset

106 
val t0 $ _ $ t2 = prop_of eq_th 
6d95a66cce00
pull variables (Var) out of lambdas, so that the Isabelle theorems closely mirror the Metis lambdalifted ones
blanchet
parents:
45569
diff
changeset

107 
val eq_ct = t0 $ prop_of th $ t2 > cterm_of thy 
6d95a66cce00
pull variables (Var) out of lambdas, so that the Isabelle theorems closely mirror the Metis lambdalifted ones
blanchet
parents:
45569
diff
changeset

108 
val eq_th' = Goal.prove_internal [] eq_ct (K (Tactic.rtac eq_th 1)) 
6d95a66cce00
pull variables (Var) out of lambdas, so that the Isabelle theorems closely mirror the Metis lambdalifted ones
blanchet
parents:
45569
diff
changeset

109 
in Thm.equal_elim eq_th' th end 
45511
9b0f8ca4388e
continued implementation of lambdalifting in Metis
blanchet
parents:
45508
diff
changeset

110 

47039
1b36a05a070d
added "metis_advisory_simp" option to orient as many equations as possible in Metis the right way (cf. "More SPASS with Isabelle")
blanchet
parents:
47015
diff
changeset

111 
fun clause_params ordering = 
1b36a05a070d
added "metis_advisory_simp" option to orient as many equations as possible in Metis the right way (cf. "More SPASS with Isabelle")
blanchet
parents:
47015
diff
changeset

112 
{ordering = ordering, 
44492
a330c0608da8
avoid using ":" for anything but systematic type tag annotations, because Hurd's Metis gives it that special semantics
blanchet
parents:
44411
diff
changeset

113 
orderLiterals = Metis_Clause.UnsignedLiteralOrder, 
39450
7e9879fbb7c5
supply the Metis parameter defaults as argument, instead of patching the Metis sources;
blanchet
parents:
39419
diff
changeset

114 
orderTerms = true} 
47039
1b36a05a070d
added "metis_advisory_simp" option to orient as many equations as possible in Metis the right way (cf. "More SPASS with Isabelle")
blanchet
parents:
47015
diff
changeset

115 
fun active_params ordering = 
1b36a05a070d
added "metis_advisory_simp" option to orient as many equations as possible in Metis the right way (cf. "More SPASS with Isabelle")
blanchet
parents:
47015
diff
changeset

116 
{clause = clause_params ordering, 
39450
7e9879fbb7c5
supply the Metis parameter defaults as argument, instead of patching the Metis sources;
blanchet
parents:
39419
diff
changeset

117 
prefactor = #prefactor Metis_Active.default, 
7e9879fbb7c5
supply the Metis parameter defaults as argument, instead of patching the Metis sources;
blanchet
parents:
39419
diff
changeset

118 
postfactor = #postfactor Metis_Active.default} 
7e9879fbb7c5
supply the Metis parameter defaults as argument, instead of patching the Metis sources;
blanchet
parents:
39419
diff
changeset

119 
val waiting_params = 
7e9879fbb7c5
supply the Metis parameter defaults as argument, instead of patching the Metis sources;
blanchet
parents:
39419
diff
changeset

120 
{symbolsWeight = 1.0, 
47015
7e2c4da9ac7d
better defaults for Metis, that seem to make it less likely to loop seemingly forever  0 coefficients might very well make it incomplete
blanchet
parents:
46949
diff
changeset

121 
variablesWeight = 0.5, 
7e2c4da9ac7d
better defaults for Metis, that seem to make it less likely to loop seemingly forever  0 coefficients might very well make it incomplete
blanchet
parents:
46949
diff
changeset

122 
literalsWeight = 0.1, 
39450
7e9879fbb7c5
supply the Metis parameter defaults as argument, instead of patching the Metis sources;
blanchet
parents:
39419
diff
changeset

123 
models = []} 
47039
1b36a05a070d
added "metis_advisory_simp" option to orient as many equations as possible in Metis the right way (cf. "More SPASS with Isabelle")
blanchet
parents:
47015
diff
changeset

124 
fun resolution_params ordering = 
1b36a05a070d
added "metis_advisory_simp" option to orient as many equations as possible in Metis the right way (cf. "More SPASS with Isabelle")
blanchet
parents:
47015
diff
changeset

125 
{active = active_params ordering, waiting = waiting_params} 
1b36a05a070d
added "metis_advisory_simp" option to orient as many equations as possible in Metis the right way (cf. "More SPASS with Isabelle")
blanchet
parents:
47015
diff
changeset

126 

1b36a05a070d
added "metis_advisory_simp" option to orient as many equations as possible in Metis the right way (cf. "More SPASS with Isabelle")
blanchet
parents:
47015
diff
changeset

127 
fun kbo_advisory_simp_ordering ord_info = 
1b36a05a070d
added "metis_advisory_simp" option to orient as many equations as possible in Metis the right way (cf. "More SPASS with Isabelle")
blanchet
parents:
47015
diff
changeset

128 
let 
1b36a05a070d
added "metis_advisory_simp" option to orient as many equations as possible in Metis the right way (cf. "More SPASS with Isabelle")
blanchet
parents:
47015
diff
changeset

129 
fun weight (m, _) = 
1b36a05a070d
added "metis_advisory_simp" option to orient as many equations as possible in Metis the right way (cf. "More SPASS with Isabelle")
blanchet
parents:
47015
diff
changeset

130 
AList.lookup (op =) ord_info (Metis_Name.toString m) > the_default 1 
1b36a05a070d
added "metis_advisory_simp" option to orient as many equations as possible in Metis the right way (cf. "More SPASS with Isabelle")
blanchet
parents:
47015
diff
changeset

131 
fun precedence p = 
1b36a05a070d
added "metis_advisory_simp" option to orient as many equations as possible in Metis the right way (cf. "More SPASS with Isabelle")
blanchet
parents:
47015
diff
changeset

132 
case int_ord (pairself weight p) of 
1b36a05a070d
added "metis_advisory_simp" option to orient as many equations as possible in Metis the right way (cf. "More SPASS with Isabelle")
blanchet
parents:
47015
diff
changeset

133 
EQUAL => #precedence Metis_KnuthBendixOrder.default p 
1b36a05a070d
added "metis_advisory_simp" option to orient as many equations as possible in Metis the right way (cf. "More SPASS with Isabelle")
blanchet
parents:
47015
diff
changeset

134 
 ord => ord 
1b36a05a070d
added "metis_advisory_simp" option to orient as many equations as possible in Metis the right way (cf. "More SPASS with Isabelle")
blanchet
parents:
47015
diff
changeset

135 
in {weight = weight, precedence = precedence} end 
37573  136 

37516
c81c86bfc18a
have "metis" method and "metis_tac" fall back on "metisFT" upon failure, following a suggestion by Larry
blanchet
parents:
37509
diff
changeset

137 
(* Main function to start Metis proof and reconstruction *) 
45519
cd6e78cb6ee8
make metis reconstruction handling more flexible
blanchet
parents:
45514
diff
changeset

138 
fun FOL_SOLVE (type_enc :: fallback_type_encs) lam_trans ctxt cls ths0 = 
42361  139 
let val thy = Proof_Context.theory_of ctxt 
39901
75d792edf634
make "cnf_axiom" work (after a fashion) in the absence of the axiom of choice
blanchet
parents:
39899
diff
changeset

140 
val new_skolemizer = 
39950  141 
Config.get ctxt new_skolemizer orelse null (Meson.choice_theorems thy) 
46365  142 
val do_lams = 
143 
(lam_trans = liftingN orelse lam_trans = lam_liftingN) 

144 
? introduce_lam_wrappers ctxt 

35826  145 
val th_cls_pairs = 
39894
35ae5cf8c96a
encode number of skolem assumptions in them, for more efficient retrieval later
blanchet
parents:
39892
diff
changeset

146 
map2 (fn j => fn th => 
35ae5cf8c96a
encode number of skolem assumptions in them, for more efficient retrieval later
blanchet
parents:
39892
diff
changeset

147 
(Thm.get_name_hint th, 
45570
6d95a66cce00
pull variables (Var) out of lambdas, so that the Isabelle theorems closely mirror the Metis lambdalifted ones
blanchet
parents:
45569
diff
changeset

148 
th > Drule.eta_contraction_rule 
6d95a66cce00
pull variables (Var) out of lambdas, so that the Isabelle theorems closely mirror the Metis lambdalifted ones
blanchet
parents:
45569
diff
changeset

149 
> Meson_Clausify.cnf_axiom ctxt new_skolemizer 
46365  150 
(lam_trans = combsN) j 
45570
6d95a66cce00
pull variables (Var) out of lambdas, so that the Isabelle theorems closely mirror the Metis lambdalifted ones
blanchet
parents:
45569
diff
changeset

151 
> map do_lams)) 
39894
35ae5cf8c96a
encode number of skolem assumptions in them, for more efficient retrieval later
blanchet
parents:
39892
diff
changeset

152 
(0 upto length ths0  1) ths0 
43092
93ec303e1917
more work on new metis that exploits the powerful new type encodings
blanchet
parents:
43091
diff
changeset

153 
val ths = maps (snd o snd) th_cls_pairs 
39938
0a2091f86eb4
fixed two bugs in new skolemizer: instantiations now take types into consideration, and rotate_tac is given the proper offset
blanchet
parents:
39937
diff
changeset

154 
val dischargers = map (fst o snd) th_cls_pairs 
45570
6d95a66cce00
pull variables (Var) out of lambdas, so that the Isabelle theorems closely mirror the Metis lambdalifted ones
blanchet
parents:
45569
diff
changeset

155 
val cls = cls > map (Drule.eta_contraction_rule #> do_lams) 
39978
11bfb7e7cc86
added "trace_metis" configuration option, replacing oldfashioned references
blanchet
parents:
39964
diff
changeset

156 
val _ = trace_msg ctxt (fn () => "FOL_SOLVE: CONJECTURE CLAUSES") 
11bfb7e7cc86
added "trace_metis" configuration option, replacing oldfashioned references
blanchet
parents:
39964
diff
changeset

157 
val _ = app (fn th => trace_msg ctxt (fn () => Display.string_of_thm ctxt th)) cls 
44411
e3629929b171
change Metis's default settings if type information axioms are generated
blanchet
parents:
44408
diff
changeset

158 
val _ = trace_msg ctxt (fn () => "type_enc = " ^ type_enc) 
46301  159 
val type_enc = type_enc_from_string Strict type_enc 
47039
1b36a05a070d
added "metis_advisory_simp" option to orient as many equations as possible in Metis the right way (cf. "More SPASS with Isabelle")
blanchet
parents:
47015
diff
changeset

160 
val (sym_tab, axioms, ord_info, concealed) = 
45514  161 
prepare_metis_problem ctxt type_enc lam_trans cls ths 
43159
29b55f292e0b
added support for helpers in new Metis, so far only for polymorphic type encodings
blanchet
parents:
43136
diff
changeset

162 
fun get_isa_thm mth Isa_Reflexive_or_Trivial = 
45508  163 
reflexive_or_trivial_from_metis ctxt type_enc sym_tab concealed mth 
45511
9b0f8ca4388e
continued implementation of lambdalifting in Metis
blanchet
parents:
45508
diff
changeset

164 
 get_isa_thm mth Isa_Lambda_Lifted = 
45569
eb30a5490543
wrap lambdas earlier, to get more control over beta/eta
blanchet
parents:
45568
diff
changeset

165 
lam_lifted_from_metis ctxt type_enc sym_tab concealed mth 
eb30a5490543
wrap lambdas earlier, to get more control over beta/eta
blanchet
parents:
45568
diff
changeset

166 
 get_isa_thm _ (Isa_Raw ith) = ith 
eb30a5490543
wrap lambdas earlier, to get more control over beta/eta
blanchet
parents:
45568
diff
changeset

167 
val axioms = axioms > map (fn (mth, ith) => (mth, get_isa_thm mth ith)) 
45559  168 
val _ = trace_msg ctxt (fn () => "ISABELLE CLAUSES") 
169 
val _ = app (fn (_, ith) => trace_msg ctxt (fn () => Display.string_of_thm ctxt ith)) axioms 

170 
val _ = trace_msg ctxt (fn () => "METIS CLAUSES") 

171 
val _ = app (fn (mth, _) => trace_msg ctxt (fn () => Metis_Thm.toString mth)) axioms 

39978
11bfb7e7cc86
added "trace_metis" configuration option, replacing oldfashioned references
blanchet
parents:
39964
diff
changeset

172 
val _ = trace_msg ctxt (fn () => "START METIS PROVE PROCESS") 
47039
1b36a05a070d
added "metis_advisory_simp" option to orient as many equations as possible in Metis the right way (cf. "More SPASS with Isabelle")
blanchet
parents:
47015
diff
changeset

173 
val ordering = 
1b36a05a070d
added "metis_advisory_simp" option to orient as many equations as possible in Metis the right way (cf. "More SPASS with Isabelle")
blanchet
parents:
47015
diff
changeset

174 
if Config.get ctxt advisory_simp then 
1b36a05a070d
added "metis_advisory_simp" option to orient as many equations as possible in Metis the right way (cf. "More SPASS with Isabelle")
blanchet
parents:
47015
diff
changeset

175 
kbo_advisory_simp_ordering (ord_info ()) 
1b36a05a070d
added "metis_advisory_simp" option to orient as many equations as possible in Metis the right way (cf. "More SPASS with Isabelle")
blanchet
parents:
47015
diff
changeset

176 
else 
1b36a05a070d
added "metis_advisory_simp" option to orient as many equations as possible in Metis the right way (cf. "More SPASS with Isabelle")
blanchet
parents:
47015
diff
changeset

177 
Metis_KnuthBendixOrder.default 
32956  178 
in 
43159
29b55f292e0b
added support for helpers in new Metis, so far only for polymorphic type encodings
blanchet
parents:
43136
diff
changeset

179 
case filter (fn t => prop_of t aconv @{prop False}) cls of 
29b55f292e0b
added support for helpers in new Metis, so far only for polymorphic type encodings
blanchet
parents:
43136
diff
changeset

180 
false_th :: _ => [false_th RS @{thm FalseE}] 
32956  181 
 [] => 
47039
1b36a05a070d
added "metis_advisory_simp" option to orient as many equations as possible in Metis the right way (cf. "More SPASS with Isabelle")
blanchet
parents:
47015
diff
changeset

182 
case Metis_Resolution.new (resolution_params ordering) 
45559  183 
{axioms = axioms > map fst, conjecture = []} 
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset

184 
> Metis_Resolution.loop of 
39419
c9accfd621a5
"Metis." > "Metis_" to reflect change in "metis.ML"
blanchet
parents:
39376
diff
changeset

185 
Metis_Resolution.Contradiction mth => 
39978
11bfb7e7cc86
added "trace_metis" configuration option, replacing oldfashioned references
blanchet
parents:
39964
diff
changeset

186 
let val _ = trace_msg ctxt (fn () => "METIS RECONSTRUCTION START: " ^ 
39419
c9accfd621a5
"Metis." > "Metis_" to reflect change in "metis.ML"
blanchet
parents:
39376
diff
changeset

187 
Metis_Thm.toString mth) 
32956  188 
val ctxt' = fold Variable.declare_constraints (map prop_of cls) ctxt 
189 
(*add constraints arising from converting goal to clause form*) 

39419
c9accfd621a5
"Metis." > "Metis_" to reflect change in "metis.ML"
blanchet
parents:
39376
diff
changeset

190 
val proof = Metis_Proof.proof mth 
43094  191 
val result = 
43212  192 
axioms 
45508  193 
> fold (replay_one_inference ctxt' type_enc concealed sym_tab) proof 
45569
eb30a5490543
wrap lambdas earlier, to get more control over beta/eta
blanchet
parents:
45568
diff
changeset

194 
val used = proof > map_filter (used_axioms axioms) 
39978
11bfb7e7cc86
added "trace_metis" configuration option, replacing oldfashioned references
blanchet
parents:
39964
diff
changeset

195 
val _ = trace_msg ctxt (fn () => "METIS COMPLETED...clauses actually used:") 
11bfb7e7cc86
added "trace_metis" configuration option, replacing oldfashioned references
blanchet
parents:
39964
diff
changeset

196 
val _ = app (fn th => trace_msg ctxt (fn () => Display.string_of_thm ctxt th)) used 
43134
0c82e00ba63e
make sure no warnings are given for polymorphic facts where we use a monomorphic instance
blanchet
parents:
43133
diff
changeset

197 
val names = th_cls_pairs > map fst 
0c82e00ba63e
make sure no warnings are given for polymorphic facts where we use a monomorphic instance
blanchet
parents:
43133
diff
changeset

198 
val used_names = 
0c82e00ba63e
make sure no warnings are given for polymorphic facts where we use a monomorphic instance
blanchet
parents:
43133
diff
changeset

199 
th_cls_pairs 
0c82e00ba63e
make sure no warnings are given for polymorphic facts where we use a monomorphic instance
blanchet
parents:
43133
diff
changeset

200 
> map_filter (fn (name, (_, cls)) => 
0c82e00ba63e
make sure no warnings are given for polymorphic facts where we use a monomorphic instance
blanchet
parents:
43133
diff
changeset

201 
if have_common_thm used cls then SOME name 
0c82e00ba63e
make sure no warnings are given for polymorphic facts where we use a monomorphic instance
blanchet
parents:
43133
diff
changeset

202 
else NONE) 
0c82e00ba63e
make sure no warnings are given for polymorphic facts where we use a monomorphic instance
blanchet
parents:
43133
diff
changeset

203 
val unused_names = names > subtract (op =) used_names 
32956  204 
in 
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset

205 
if not (null cls) andalso not (have_common_thm used cls) then 
42650
552eae49f97d
reintroduce this idea of running "metisFT" after a failed "metis"  I took it out in e85ce10cef1a because I couldn't think of a reasonable use case, but now that ATPs use sound encodings and include dangerous facts (e.g. True_or_False) it makes more sense than ever to run "metisFT" after "metis"
blanchet
parents:
42616
diff
changeset

206 
verbose_warning ctxt "The assumptions are inconsistent" 
36383  207 
else 
208 
(); 

43134
0c82e00ba63e
make sure no warnings are given for polymorphic facts where we use a monomorphic instance
blanchet
parents:
43133
diff
changeset

209 
if not (null unused_names) then 
0c82e00ba63e
make sure no warnings are given for polymorphic facts where we use a monomorphic instance
blanchet
parents:
43133
diff
changeset

210 
"Unused theorems: " ^ commas_quote unused_names 
0c82e00ba63e
make sure no warnings are given for polymorphic facts where we use a monomorphic instance
blanchet
parents:
43133
diff
changeset

211 
> verbose_warning ctxt 
36230
43d10a494c91
added warning about inconsistent context to Metis;
blanchet
parents:
36170
diff
changeset

212 
else 
43d10a494c91
added warning about inconsistent context to Metis;
blanchet
parents:
36170
diff
changeset

213 
(); 
32956  214 
case result of 
215 
(_,ith)::_ => 

39978
11bfb7e7cc86
added "trace_metis" configuration option, replacing oldfashioned references
blanchet
parents:
39964
diff
changeset

216 
(trace_msg ctxt (fn () => "Success: " ^ Display.string_of_thm ctxt ith); 
39887
74939e2afb95
second step in introducing the new Skolemizer  notably, added procedure for discharging Skolem assumptions
blanchet
parents:
39886
diff
changeset

217 
[discharge_skolem_premises ctxt dischargers ith]) 
39978
11bfb7e7cc86
added "trace_metis" configuration option, replacing oldfashioned references
blanchet
parents:
39964
diff
changeset

218 
 _ => (trace_msg ctxt (fn () => "Metis: No result"); []) 
32956  219 
end 
39419
c9accfd621a5
"Metis." > "Metis_" to reflect change in "metis.ML"
blanchet
parents:
39376
diff
changeset

220 
 Metis_Resolution.Satisfiable _ => 
39978
11bfb7e7cc86
added "trace_metis" configuration option, replacing oldfashioned references
blanchet
parents:
39964
diff
changeset

221 
(trace_msg ctxt (fn () => "Metis: No firstorder proof with the lemmas supplied"); 
45519
cd6e78cb6ee8
make metis reconstruction handling more flexible
blanchet
parents:
45514
diff
changeset

222 
if null fallback_type_encs then 
43034
18259246abb5
try both "metis" and (on failure) "metisFT" in replay
blanchet
parents:
42847
diff
changeset

223 
() 
18259246abb5
try both "metis" and (on failure) "metisFT" in replay
blanchet
parents:
42847
diff
changeset

224 
else 
42650
552eae49f97d
reintroduce this idea of running "metisFT" after a failed "metis"  I took it out in e85ce10cef1a because I couldn't think of a reasonable use case, but now that ATPs use sound encodings and include dangerous facts (e.g. True_or_False) it makes more sense than ever to run "metisFT" after "metis"
blanchet
parents:
42616
diff
changeset

225 
raise METIS ("FOL_SOLVE", 
43034
18259246abb5
try both "metis" and (on failure) "metisFT" in replay
blanchet
parents:
42847
diff
changeset

226 
"No firstorder proof with the lemmas supplied"); 
38097
5e4ad2df09f3
revert exception throwing in FOL_SOLVE, since they're not caught anyway
blanchet
parents:
38028
diff
changeset

227 
[]) 
42733
01ef1c3d9cfd
more robust exception handling in Metis (also works if there are several subgoals)
blanchet
parents:
42650
diff
changeset

228 
end 
01ef1c3d9cfd
more robust exception handling in Metis (also works if there are several subgoals)
blanchet
parents:
42650
diff
changeset

229 
handle METIS (loc, msg) => 
45519
cd6e78cb6ee8
make metis reconstruction handling more flexible
blanchet
parents:
45514
diff
changeset

230 
case fallback_type_encs of 
43034
18259246abb5
try both "metis" and (on failure) "metisFT" in replay
blanchet
parents:
42847
diff
changeset

231 
[] => error ("Failed to replay Metis proof in Isabelle." ^ 
18259246abb5
try both "metis" and (on failure) "metisFT" in replay
blanchet
parents:
42847
diff
changeset

232 
(if Config.get ctxt verbose then "\n" ^ loc ^ ": " ^ msg 
18259246abb5
try both "metis" and (on failure) "metisFT" in replay
blanchet
parents:
42847
diff
changeset

233 
else "")) 
45519
cd6e78cb6ee8
make metis reconstruction handling more flexible
blanchet
parents:
45514
diff
changeset

234 
 first_fallback :: _ => 
43228
2ed2f092e990
obsoleted "metisFT", and added "no_types" version of Metis as fallback to Sledgehammer after noticing how useful it can be
blanchet
parents:
43212
diff
changeset

235 
(verbose_warning ctxt 
2ed2f092e990
obsoleted "metisFT", and added "no_types" version of Metis as fallback to Sledgehammer after noticing how useful it can be
blanchet
parents:
43212
diff
changeset

236 
("Falling back on " ^ 
45519
cd6e78cb6ee8
make metis reconstruction handling more flexible
blanchet
parents:
45514
diff
changeset

237 
quote (metis_call first_fallback lam_trans) ^ "..."); 
cd6e78cb6ee8
make metis reconstruction handling more flexible
blanchet
parents:
45514
diff
changeset

238 
FOL_SOLVE fallback_type_encs lam_trans ctxt cls ths0) 
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

239 

45508  240 
fun neg_clausify ctxt combinators = 
38028  241 
single 
43964
9338aa218f09
thread proper context through, to make sure that "using [[meson_max_clauses = 200]]" is not ignored when clausifying the conjecture
blanchet
parents:
43963
diff
changeset

242 
#> Meson.make_clauses_unsorted ctxt 
45508  243 
#> combinators ? map Meson_Clausify.introduce_combinators_in_theorem 
38028  244 
#> Meson.finish_cnf 
245 

39269
c2795d8a2461
use definitional CNF for the goal if at least one of the premisses would lead to too many clauses in Meson
blanchet
parents:
39267
diff
changeset

246 
fun preskolem_tac ctxt st0 = 
c2795d8a2461
use definitional CNF for the goal if at least one of the premisses would lead to too many clauses in Meson
blanchet
parents:
39267
diff
changeset

247 
(if exists (Meson.has_too_many_clauses ctxt) 
c2795d8a2461
use definitional CNF for the goal if at least one of the premisses would lead to too many clauses in Meson
blanchet
parents:
39267
diff
changeset

248 
(Logic.prems_of_goal (prop_of st0) 1) then 
42336
d63d43e85879
improve definitional CNF on goal by moving "not" past the quantifiers
blanchet
parents:
40665
diff
changeset

249 
Simplifier.full_simp_tac (Meson_Clausify.ss_only @{thms not_all not_ex}) 1 
d63d43e85879
improve definitional CNF on goal by moving "not" past the quantifiers
blanchet
parents:
40665
diff
changeset

250 
THEN cnf.cnfx_rewrite_tac ctxt 1 
39269
c2795d8a2461
use definitional CNF for the goal if at least one of the premisses would lead to too many clauses in Meson
blanchet
parents:
39267
diff
changeset

251 
else 
c2795d8a2461
use definitional CNF for the goal if at least one of the premisses would lead to too many clauses in Meson
blanchet
parents:
39267
diff
changeset

252 
all_tac) st0 
c2795d8a2461
use definitional CNF for the goal if at least one of the premisses would lead to too many clauses in Meson
blanchet
parents:
39267
diff
changeset

253 

38652
e063be321438
perform etaexpansion of quantifier bodies in Sledgehammer translation when needed + transform elim rules later;
blanchet
parents:
38632
diff
changeset

254 
val type_has_top_sort = 
e063be321438
perform etaexpansion of quantifier bodies in Sledgehammer translation when needed + transform elim rules later;
blanchet
parents:
38632
diff
changeset

255 
exists_subtype (fn TFree (_, []) => true  TVar (_, []) => true  _ => false) 
e063be321438
perform etaexpansion of quantifier bodies in Sledgehammer translation when needed + transform elim rules later;
blanchet
parents:
38632
diff
changeset

256 

45519
cd6e78cb6ee8
make metis reconstruction handling more flexible
blanchet
parents:
45514
diff
changeset

257 
fun generic_metis_tac type_encs lam_trans ctxt ths i st0 = 
37926
e6ff246c0cdb
renamings + only need second component of name pool to reconstruct proofs
blanchet
parents:
37925
diff
changeset

258 
let 
39978
11bfb7e7cc86
added "trace_metis" configuration option, replacing oldfashioned references
blanchet
parents:
39964
diff
changeset

259 
val _ = trace_msg ctxt (fn () => 
43194  260 
"Metis called with theorems\n" ^ 
43034
18259246abb5
try both "metis" and (on failure) "metisFT" in replay
blanchet
parents:
42847
diff
changeset

261 
cat_lines (map (Display.string_of_thm ctxt) ths)) 
45519
cd6e78cb6ee8
make metis reconstruction handling more flexible
blanchet
parents:
45514
diff
changeset

262 
val type_encs = type_encs > maps unalias_type_enc 
45508  263 
fun tac clause = 
45519
cd6e78cb6ee8
make metis reconstruction handling more flexible
blanchet
parents:
45514
diff
changeset

264 
resolve_tac (FOL_SOLVE type_encs lam_trans ctxt clause ths) 1 
32956  265 
in 
37626
1146291fe718
move blacklisting completely out of the clausifier;
blanchet
parents:
37625
diff
changeset

266 
if exists_type type_has_top_sort (prop_of st0) then 
43299
f78d5f0818a0
be a bit more liberal with respect to the universal sort  it sometimes help
blanchet
parents:
43298
diff
changeset

267 
verbose_warning ctxt "Proof state contains the universal sort {}" 
35568
8fbbfc39508f
renamed type_has_empty_sort to type_has_topsort  {} is the full universal sort;
wenzelm
parents:
34087
diff
changeset

268 
else 
43299
f78d5f0818a0
be a bit more liberal with respect to the universal sort  it sometimes help
blanchet
parents:
43298
diff
changeset

269 
(); 
45508  270 
Meson.MESON (preskolem_tac ctxt) 
46365  271 
(maps (neg_clausify ctxt (lam_trans = combsN))) tac ctxt i st0 
32956  272 
end 
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

273 

45519
cd6e78cb6ee8
make metis reconstruction handling more flexible
blanchet
parents:
45514
diff
changeset

274 
fun metis_tac [] = generic_metis_tac partial_type_encs 
cd6e78cb6ee8
make metis reconstruction handling more flexible
blanchet
parents:
45514
diff
changeset

275 
 metis_tac type_encs = generic_metis_tac type_encs 
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

276 

38632
9cde57cdd0e3
treat "using X by metis" (more or less) the same as "by (metis X)"
blanchet
parents:
38614
diff
changeset

277 
(* Whenever "X" has schematic type variables, we treat "using X by metis" as 
43100  278 
"by (metis X)" to prevent "Subgoal.FOCUS" from freezing the type variables. 
38632
9cde57cdd0e3
treat "using X by metis" (more or less) the same as "by (metis X)"
blanchet
parents:
38614
diff
changeset

279 
We don't do it for nonschematic facts "X" because this breaks a few proofs 
9cde57cdd0e3
treat "using X by metis" (more or less) the same as "by (metis X)"
blanchet
parents:
38614
diff
changeset

280 
(in the rare and subtle case where a proof relied on extensionality not being 
38994  281 
applied) and brings few benefits. *) 
38632
9cde57cdd0e3
treat "using X by metis" (more or less) the same as "by (metis X)"
blanchet
parents:
38614
diff
changeset

282 
val has_tvar = 
9cde57cdd0e3
treat "using X by metis" (more or less) the same as "by (metis X)"
blanchet
parents:
38614
diff
changeset

283 
exists_type (exists_subtype (fn TVar _ => true  _ => false)) o prop_of 
43034
18259246abb5
try both "metis" and (on failure) "metisFT" in replay
blanchet
parents:
42847
diff
changeset

284 

45519
cd6e78cb6ee8
make metis reconstruction handling more flexible
blanchet
parents:
45514
diff
changeset

285 
fun method default_type_encs ((override_type_encs, lam_trans), ths) ctxt facts = 
43100  286 
let 
43228
2ed2f092e990
obsoleted "metisFT", and added "no_types" version of Metis as fallback to Sledgehammer after noticing how useful it can be
blanchet
parents:
43212
diff
changeset

287 
val _ = 
45519
cd6e78cb6ee8
make metis reconstruction handling more flexible
blanchet
parents:
45514
diff
changeset

288 
if default_type_encs = full_type_encs then 
44052  289 
legacy_feature "Old \"metisFT\" method  use \"metis (full_types)\" instead" 
43228
2ed2f092e990
obsoleted "metisFT", and added "no_types" version of Metis as fallback to Sledgehammer after noticing how useful it can be
blanchet
parents:
43212
diff
changeset

290 
else 
2ed2f092e990
obsoleted "metisFT", and added "no_types" version of Metis as fallback to Sledgehammer after noticing how useful it can be
blanchet
parents:
43212
diff
changeset

291 
() 
43100  292 
val (schem_facts, nonschem_facts) = List.partition has_tvar facts 
45519
cd6e78cb6ee8
make metis reconstruction handling more flexible
blanchet
parents:
45514
diff
changeset

293 
val type_encs = override_type_encs > the_default default_type_encs 
cd6e78cb6ee8
make metis reconstruction handling more flexible
blanchet
parents:
45514
diff
changeset

294 
val lam_trans = lam_trans > the_default metis_default_lam_trans 
43100  295 
in 
43099  296 
HEADGOAL (Method.insert_tac nonschem_facts THEN' 
45519
cd6e78cb6ee8
make metis reconstruction handling more flexible
blanchet
parents:
45514
diff
changeset

297 
CHANGED_PROP o generic_metis_tac type_encs lam_trans ctxt 
45514  298 
(schem_facts @ ths)) 
43099  299 
end 
43100  300 

46365  301 
val metis_lam_transs = [hide_lamsN, liftingN, combsN] 
45519
cd6e78cb6ee8
make metis reconstruction handling more flexible
blanchet
parents:
45514
diff
changeset

302 

45578  303 
fun set_opt _ x NONE = SOME x 
304 
 set_opt get x (SOME x0) = 

305 
error ("Cannot specify both " ^ quote (get x0) ^ " and " ^ quote (get x) ^ 

306 
".") 

45519
cd6e78cb6ee8
make metis reconstruction handling more flexible
blanchet
parents:
45514
diff
changeset

307 
fun consider_opt s = 
45578  308 
if member (op =) metis_lam_transs s then apsnd (set_opt I s) 
309 
else apfst (set_opt hd [s]) 

45514  310 

45519
cd6e78cb6ee8
make metis reconstruction handling more flexible
blanchet
parents:
45514
diff
changeset

311 
val parse_metis_options = 
cd6e78cb6ee8
make metis reconstruction handling more flexible
blanchet
parents:
45514
diff
changeset

312 
Scan.optional 
cd6e78cb6ee8
make metis reconstruction handling more flexible
blanchet
parents:
45514
diff
changeset

313 
(Args.parens (Parse.short_ident 
46949  314 
 Scan.option (@{keyword ","}  Parse.short_ident)) 
45519
cd6e78cb6ee8
make metis reconstruction handling more flexible
blanchet
parents:
45514
diff
changeset

315 
>> (fn (s, s') => 
cd6e78cb6ee8
make metis reconstruction handling more flexible
blanchet
parents:
45514
diff
changeset

316 
(NONE, NONE) > consider_opt s 
cd6e78cb6ee8
make metis reconstruction handling more flexible
blanchet
parents:
45514
diff
changeset

317 
> (case s' of SOME s' => consider_opt s'  _ => I))) 
cd6e78cb6ee8
make metis reconstruction handling more flexible
blanchet
parents:
45514
diff
changeset

318 
(NONE, NONE) 
cd6e78cb6ee8
make metis reconstruction handling more flexible
blanchet
parents:
45514
diff
changeset

319 

cd6e78cb6ee8
make metis reconstruction handling more flexible
blanchet
parents:
45514
diff
changeset

320 
fun setup_method (binding, type_encs) = 
cd6e78cb6ee8
make metis reconstruction handling more flexible
blanchet
parents:
45514
diff
changeset

321 
Scan.lift parse_metis_options  Attrib.thms >> (METHOD oo method type_encs) 
43228
2ed2f092e990
obsoleted "metisFT", and added "no_types" version of Metis as fallback to Sledgehammer after noticing how useful it can be
blanchet
parents:
43212
diff
changeset

322 
> Method.setup binding 
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

323 

32956  324 
val setup = 
45519
cd6e78cb6ee8
make metis reconstruction handling more flexible
blanchet
parents:
45514
diff
changeset

325 
[((@{binding metis}, partial_type_encs), 
43228
2ed2f092e990
obsoleted "metisFT", and added "no_types" version of Metis as fallback to Sledgehammer after noticing how useful it can be
blanchet
parents:
43212
diff
changeset

326 
"Metis for FOL and HOL problems"), 
45519
cd6e78cb6ee8
make metis reconstruction handling more flexible
blanchet
parents:
45514
diff
changeset

327 
((@{binding metisFT}, full_type_encs), 
43212  328 
"Metis for FOL/HOL problems with fullytyped translation")] 
43034
18259246abb5
try both "metis" and (on failure) "metisFT" in replay
blanchet
parents:
42847
diff
changeset

329 
> fold (uncurry setup_method) 
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

330 

028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

331 
end; 