author  blanchet 
Thu, 12 May 2011 15:29:19 +0200  
changeset 42754  b9d7df8c51c8 
parent 42753  c9552e617acc 
child 42755  4603154a3018 
permissions  rwrr 
40114  1 
(* Title: HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML 
38282
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

2 
Author: Fabian Immler, TU Muenchen 
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

3 
Author: Makarius 
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

4 
Author: Jasmin Blanchette, TU Muenchen 
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

5 

39494
bf7dd4902321
rename "Metis_Clauses" to "Metis_Translate" for consistency with "Sledgehammer_Translate"
blanchet
parents:
39452
diff
changeset

6 
Translation of HOL to FOL for Sledgehammer. 
38282
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

7 
*) 
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

8 

40068  9 
signature SLEDGEHAMMER_ATP_TRANSLATE = 
38282
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

10 
sig 
42227
662b50b7126f
if "monomorphize" is enabled, mangle the type information in the names by default
blanchet
parents:
42180
diff
changeset

11 
type 'a fo_term = 'a ATP_Problem.fo_term 
42709
e7af132d48fe
allow each prover to specify its own formula kind for symbols occurring in the conjecture
blanchet
parents:
42701
diff
changeset

12 
type formula_kind = ATP_Problem.formula_kind 
38282
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

13 
type 'a problem = 'a ATP_Problem.problem 
42640
879d2d6b05ce
generate tags for simps, intros, and elims in TPTP poblems on demand
blanchet
parents:
42613
diff
changeset

14 
type locality = Sledgehammer_Filter.locality 
42613
23b13b1bd565
use strings to encode type systems in ATP module, to reduce the amount of outofplace information and also to make it easier to print the type system used
blanchet
parents:
42612
diff
changeset

15 

23b13b1bd565
use strings to encode type systems in ATP module, to reduce the amount of outofplace information and also to make it easier to print the type system used
blanchet
parents:
42612
diff
changeset

16 
datatype polymorphism = Polymorphic  Monomorphic  Mangled_Monomorphic 
23b13b1bd565
use strings to encode type systems in ATP module, to reduce the amount of outofplace information and also to make it easier to print the type system used
blanchet
parents:
42612
diff
changeset

17 
datatype type_level = 
23b13b1bd565
use strings to encode type systems in ATP module, to reduce the amount of outofplace information and also to make it easier to print the type system used
blanchet
parents:
42612
diff
changeset

18 
All_Types  Nonmonotonic_Types  Finite_Types  Const_Arg_Types  No_Types 
23b13b1bd565
use strings to encode type systems in ATP module, to reduce the amount of outofplace information and also to make it easier to print the type system used
blanchet
parents:
42612
diff
changeset

19 

23b13b1bd565
use strings to encode type systems in ATP module, to reduce the amount of outofplace information and also to make it easier to print the type system used
blanchet
parents:
42612
diff
changeset

20 
datatype type_system = 
42722  21 
Simple_Types of type_level  
42613
23b13b1bd565
use strings to encode type systems in ATP module, to reduce the amount of outofplace information and also to make it easier to print the type system used
blanchet
parents:
42612
diff
changeset

22 
Preds of polymorphism * type_level  
23b13b1bd565
use strings to encode type systems in ATP module, to reduce the amount of outofplace information and also to make it easier to print the type system used
blanchet
parents:
42612
diff
changeset

23 
Tags of polymorphism * type_level 
23b13b1bd565
use strings to encode type systems in ATP module, to reduce the amount of outofplace information and also to make it easier to print the type system used
blanchet
parents:
42612
diff
changeset

24 

40114  25 
type translated_formula 
38282
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

26 

42646
4781fcd53572
replaced some Unsynchronized.refs with Config.Ts
blanchet
parents:
42645
diff
changeset

27 
val readable_names : bool Config.T 
40204
da97d75e20e6
standardize on "fact" terminology (vs. "axiom" or "theorem") in Sledgehammer  but keep "Axiom" in the lowerlevel "ATP_Problem" module
blanchet
parents:
40145
diff
changeset

28 
val fact_prefix : string 
38282
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

29 
val conjecture_prefix : string 
42568
7b9801a34836
no needless "fequal" proxies if "explicit_apply" is set + always have readable names
blanchet
parents:
42566
diff
changeset

30 
val predicator_base : string 
42544
75cb06eee990
reimplemented the hAPP introduction code so that it's done earlier, when the types are still available
blanchet
parents:
42543
diff
changeset

31 
val explicit_app_base : string 
42549
b9754f26c7bc
handle special constants correctly in Isar proof reconstruction code, especially type predicates
blanchet
parents:
42548
diff
changeset

32 
val type_pred_base : string 
42562  33 
val tff_type_prefix : string 
42613
23b13b1bd565
use strings to encode type systems in ATP module, to reduce the amount of outofplace information and also to make it easier to print the type system used
blanchet
parents:
42612
diff
changeset

34 
val type_sys_from_string : string > type_system 
23b13b1bd565
use strings to encode type systems in ATP module, to reduce the amount of outofplace information and also to make it easier to print the type system used
blanchet
parents:
42612
diff
changeset

35 
val polymorphism_of_type_sys : type_system > polymorphism 
23b13b1bd565
use strings to encode type systems in ATP module, to reduce the amount of outofplace information and also to make it easier to print the type system used
blanchet
parents:
42612
diff
changeset

36 
val level_of_type_sys : type_system > type_level 
23b13b1bd565
use strings to encode type systems in ATP module, to reduce the amount of outofplace information and also to make it easier to print the type system used
blanchet
parents:
42612
diff
changeset

37 
val is_type_sys_virtually_sound : type_system > bool 
23b13b1bd565
use strings to encode type systems in ATP module, to reduce the amount of outofplace information and also to make it easier to print the type system used
blanchet
parents:
42612
diff
changeset

38 
val is_type_sys_fairly_sound : type_system > bool 
41136
30bedf58b177
implemented new type system encoding "overload_args", which is more lightweight than "const_args" (the unsound default) and hopefully almost as sound
blanchet
parents:
41134
diff
changeset

39 
val num_atp_type_args : theory > type_system > string > int 
42542
024920b65ce2
perform constant mangling and/or removal of its type args in an earlier phase, so that the rest of the code doesn't need to worry about it
blanchet
parents:
42541
diff
changeset

40 
val unmangled_const : string > string * string fo_term list 
41088  41 
val translate_atp_fact : 
42640
879d2d6b05ce
generate tags for simps, intros, and elims in TPTP poblems on demand
blanchet
parents:
42613
diff
changeset

42 
Proof.context > bool > (string * locality) * thm 
879d2d6b05ce
generate tags for simps, intros, and elims in TPTP poblems on demand
blanchet
parents:
42613
diff
changeset

43 
> translated_formula option * ((string * locality) * thm) 
40059
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39975
diff
changeset

44 
val prepare_atp_problem : 
42709
e7af132d48fe
allow each prover to specify its own formula kind for symbols occurring in the conjecture
blanchet
parents:
42701
diff
changeset

45 
Proof.context > formula_kind > formula_kind > type_system > bool 
e7af132d48fe
allow each prover to specify its own formula kind for symbols occurring in the conjecture
blanchet
parents:
42701
diff
changeset

46 
> term list > term 
41091
0afdf5cde874
implicitly call the minimizer for SMT solvers that don't return an unsat core
blanchet
parents:
41088
diff
changeset

47 
> (translated_formula option * ((string * 'a) * thm)) list 
42541
8938507b2054
move type declarations to the front, for TFFcompliance
blanchet
parents:
42540
diff
changeset

48 
> string problem * string Symtab.table * int * int 
8938507b2054
move type declarations to the front, for TFFcompliance
blanchet
parents:
42540
diff
changeset

49 
* (string * 'a) list vector 
41313
a96ac4d180b7
optionally supply constant weights to E  turned off by default until properly parameterized
blanchet
parents:
41211
diff
changeset

50 
val atp_problem_weights : string problem > (string * real) list 
38282
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

51 
end; 
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

52 

41140
9c68004b8c9d
added Sledgehammer support for higherorder propositional reasoning
blanchet
parents:
41138
diff
changeset

53 
structure Sledgehammer_ATP_Translate : SLEDGEHAMMER_ATP_TRANSLATE = 
38282
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

54 
struct 
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

55 

319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

56 
open ATP_Problem 
39494
bf7dd4902321
rename "Metis_Clauses" to "Metis_Translate" for consistency with "Sledgehammer_Translate"
blanchet
parents:
39452
diff
changeset

57 
open Metis_Translate 
38282
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

58 
open Sledgehammer_Util 
42640
879d2d6b05ce
generate tags for simps, intros, and elims in TPTP poblems on demand
blanchet
parents:
42613
diff
changeset

59 
open Sledgehammer_Filter 
879d2d6b05ce
generate tags for simps, intros, and elims in TPTP poblems on demand
blanchet
parents:
42613
diff
changeset

60 

879d2d6b05ce
generate tags for simps, intros, and elims in TPTP poblems on demand
blanchet
parents:
42613
diff
changeset

61 
(* experimental *) 
879d2d6b05ce
generate tags for simps, intros, and elims in TPTP poblems on demand
blanchet
parents:
42613
diff
changeset

62 
val generate_useful_info = false 
38282
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

63 

42568
7b9801a34836
no needless "fequal" proxies if "explicit_apply" is set + always have readable names
blanchet
parents:
42566
diff
changeset

64 
(* Readable names are often much shorter, especially if types are mangled in 
42589
9f7c48463645
restructured type systems some more  the old naming schemes had "argshg diff less" and "tagshg diff less" as equivalent and didn't support a monomorphic version of "tags"
blanchet
parents:
42586
diff
changeset

65 
names. Also, the logic for generating legal SNARK sort names is only 
9f7c48463645
restructured type systems some more  the old naming schemes had "argshg diff less" and "tagshg diff less" as equivalent and didn't support a monomorphic version of "tags"
blanchet
parents:
42586
diff
changeset

66 
implemented for readable names. Finally, readable names are, well, more 
9f7c48463645
restructured type systems some more  the old naming schemes had "argshg diff less" and "tagshg diff less" as equivalent and didn't support a monomorphic version of "tags"
blanchet
parents:
42586
diff
changeset

67 
readable. For these reason, they are enabled by default. *) 
42646
4781fcd53572
replaced some Unsynchronized.refs with Config.Ts
blanchet
parents:
42645
diff
changeset

68 
val readable_names = 
4781fcd53572
replaced some Unsynchronized.refs with Config.Ts
blanchet
parents:
42645
diff
changeset

69 
Attrib.setup_config_bool @{binding sledgehammer_atp_readable_names} (K true) 
42568
7b9801a34836
no needless "fequal" proxies if "explicit_apply" is set + always have readable names
blanchet
parents:
42566
diff
changeset

70 

42543
f9d402d144d4
declare TFF types so that SNARK can be used with types
blanchet
parents:
42542
diff
changeset

71 
val type_decl_prefix = "type_" 
f9d402d144d4
declare TFF types so that SNARK can be used with types
blanchet
parents:
42542
diff
changeset

72 
val sym_decl_prefix = "sym_" 
40204
da97d75e20e6
standardize on "fact" terminology (vs. "axiom" or "theorem") in Sledgehammer  but keep "Axiom" in the lowerlevel "ATP_Problem" module
blanchet
parents:
40145
diff
changeset

73 
val fact_prefix = "fact_" 
38282
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

74 
val conjecture_prefix = "conj_" 
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

75 
val helper_prefix = "help_" 
42543
f9d402d144d4
declare TFF types so that SNARK can be used with types
blanchet
parents:
42542
diff
changeset

76 
val class_rel_clause_prefix = "crel_"; 
38282
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

77 
val arity_clause_prefix = "arity_" 
39975
7c50d5ca5c04
avoid generating several formulas with the same name ("tfrees")
blanchet
parents:
39954
diff
changeset

78 
val tfree_prefix = "tfree_" 
38282
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

79 

42568
7b9801a34836
no needless "fequal" proxies if "explicit_apply" is set + always have readable names
blanchet
parents:
42566
diff
changeset

80 
val predicator_base = "hBOOL" 
42544
75cb06eee990
reimplemented the hAPP introduction code so that it's done earlier, when the types are still available
blanchet
parents:
42543
diff
changeset

81 
val explicit_app_base = "hAPP" 
42542
024920b65ce2
perform constant mangling and/or removal of its type args in an earlier phase, so that the rest of the code doesn't need to worry about it
blanchet
parents:
42541
diff
changeset

82 
val type_pred_base = "is" 
42562  83 
val tff_type_prefix = "ty_" 
42531
a462dbaa584f
added more rudimentary type support to Sledgehammer's ATP encoding
blanchet
parents:
42530
diff
changeset

84 

42562  85 
fun make_tff_type s = tff_type_prefix ^ ascii_of s 
42531
a462dbaa584f
added more rudimentary type support to Sledgehammer's ATP encoding
blanchet
parents:
42530
diff
changeset

86 

38282
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

87 
(* Freshness almost guaranteed! *) 
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

88 
val sledgehammer_weak_prefix = "Sledgehammer:" 
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

89 

42613
23b13b1bd565
use strings to encode type systems in ATP module, to reduce the amount of outofplace information and also to make it easier to print the type system used
blanchet
parents:
42612
diff
changeset

90 
datatype polymorphism = Polymorphic  Monomorphic  Mangled_Monomorphic 
23b13b1bd565
use strings to encode type systems in ATP module, to reduce the amount of outofplace information and also to make it easier to print the type system used
blanchet
parents:
42612
diff
changeset

91 
datatype type_level = 
23b13b1bd565
use strings to encode type systems in ATP module, to reduce the amount of outofplace information and also to make it easier to print the type system used
blanchet
parents:
42612
diff
changeset

92 
All_Types  Nonmonotonic_Types  Finite_Types  Const_Arg_Types  No_Types 
23b13b1bd565
use strings to encode type systems in ATP module, to reduce the amount of outofplace information and also to make it easier to print the type system used
blanchet
parents:
42612
diff
changeset

93 

23b13b1bd565
use strings to encode type systems in ATP module, to reduce the amount of outofplace information and also to make it easier to print the type system used
blanchet
parents:
42612
diff
changeset

94 
datatype type_system = 
42722  95 
Simple_Types of type_level  
42613
23b13b1bd565
use strings to encode type systems in ATP module, to reduce the amount of outofplace information and also to make it easier to print the type system used
blanchet
parents:
42612
diff
changeset

96 
Preds of polymorphism * type_level  
23b13b1bd565
use strings to encode type systems in ATP module, to reduce the amount of outofplace information and also to make it easier to print the type system used
blanchet
parents:
42612
diff
changeset

97 
Tags of polymorphism * type_level 
23b13b1bd565
use strings to encode type systems in ATP module, to reduce the amount of outofplace information and also to make it easier to print the type system used
blanchet
parents:
42612
diff
changeset

98 

42689
e38590764c34
versions of ! and ? for the ASCIIchallenged Mirabelle
blanchet
parents:
42688
diff
changeset

99 
fun try_unsuffixes ss s = 
e38590764c34
versions of ! and ? for the ASCIIchallenged Mirabelle
blanchet
parents:
42688
diff
changeset

100 
fold (fn s' => fn NONE => try (unsuffix s') s  some => some) ss NONE 
e38590764c34
versions of ! and ? for the ASCIIchallenged Mirabelle
blanchet
parents:
42688
diff
changeset

101 

42613
23b13b1bd565
use strings to encode type systems in ATP module, to reduce the amount of outofplace information and also to make it easier to print the type system used
blanchet
parents:
42612
diff
changeset

102 
fun type_sys_from_string s = 
42722  103 
(case try (unprefix "poly_") s of 
104 
SOME s => (SOME Polymorphic, s) 

42613
23b13b1bd565
use strings to encode type systems in ATP module, to reduce the amount of outofplace information and also to make it easier to print the type system used
blanchet
parents:
42612
diff
changeset

105 
 NONE => 
23b13b1bd565
use strings to encode type systems in ATP module, to reduce the amount of outofplace information and also to make it easier to print the type system used
blanchet
parents:
42612
diff
changeset

106 
case try (unprefix "mono_") s of 
42722  107 
SOME s => (SOME Monomorphic, s) 
108 
 NONE => 

109 
case try (unprefix "mangled_") s of 

110 
SOME s => (SOME Mangled_Monomorphic, s) 

111 
 NONE => (NONE, s)) 

42613
23b13b1bd565
use strings to encode type systems in ATP module, to reduce the amount of outofplace information and also to make it easier to print the type system used
blanchet
parents:
42612
diff
changeset

112 
> (fn s => 
42689
e38590764c34
versions of ! and ? for the ASCIIchallenged Mirabelle
blanchet
parents:
42688
diff
changeset

113 
(* "_query" and "_bang" are for the ASCIIchallenged Mirabelle. *) 
e38590764c34
versions of ! and ? for the ASCIIchallenged Mirabelle
blanchet
parents:
42688
diff
changeset

114 
case try_unsuffixes ["?", "_query"] s of 
42613
23b13b1bd565
use strings to encode type systems in ATP module, to reduce the amount of outofplace information and also to make it easier to print the type system used
blanchet
parents:
42612
diff
changeset

115 
SOME s => (Nonmonotonic_Types, s) 
23b13b1bd565
use strings to encode type systems in ATP module, to reduce the amount of outofplace information and also to make it easier to print the type system used
blanchet
parents:
42612
diff
changeset

116 
 NONE => 
42689
e38590764c34
versions of ! and ? for the ASCIIchallenged Mirabelle
blanchet
parents:
42688
diff
changeset

117 
case try_unsuffixes ["!", "_bang"] s of 
42613
23b13b1bd565
use strings to encode type systems in ATP module, to reduce the amount of outofplace information and also to make it easier to print the type system used
blanchet
parents:
42612
diff
changeset

118 
SOME s => (Finite_Types, s) 
23b13b1bd565
use strings to encode type systems in ATP module, to reduce the amount of outofplace information and also to make it easier to print the type system used
blanchet
parents:
42612
diff
changeset

119 
 NONE => (All_Types, s)) 
42722  120 
> (fn (poly, (level, core)) => 
121 
case (core, (poly, level)) of 

122 
("simple_types", (NONE, level)) => Simple_Types level 

42753
c9552e617acc
drop some type arguments to constants in unsound type systems + remove a few type systems that make no sense from the circulation
blanchet
parents:
42750
diff
changeset

123 
 ("preds", (SOME Polymorphic, level)) => 
c9552e617acc
drop some type arguments to constants in unsound type systems + remove a few type systems that make no sense from the circulation
blanchet
parents:
42750
diff
changeset

124 
if level = All_Types then Preds (Polymorphic, level) 
c9552e617acc
drop some type arguments to constants in unsound type systems + remove a few type systems that make no sense from the circulation
blanchet
parents:
42750
diff
changeset

125 
else raise Same.SAME 
42722  126 
 ("preds", (SOME poly, level)) => Preds (poly, level) 
42753
c9552e617acc
drop some type arguments to constants in unsound type systems + remove a few type systems that make no sense from the circulation
blanchet
parents:
42750
diff
changeset

127 
 ("tags", (SOME Polymorphic, level)) => 
c9552e617acc
drop some type arguments to constants in unsound type systems + remove a few type systems that make no sense from the circulation
blanchet
parents:
42750
diff
changeset

128 
if level = All_Types orelse level = Finite_Types then 
c9552e617acc
drop some type arguments to constants in unsound type systems + remove a few type systems that make no sense from the circulation
blanchet
parents:
42750
diff
changeset

129 
Tags (Polymorphic, level) 
c9552e617acc
drop some type arguments to constants in unsound type systems + remove a few type systems that make no sense from the circulation
blanchet
parents:
42750
diff
changeset

130 
else 
c9552e617acc
drop some type arguments to constants in unsound type systems + remove a few type systems that make no sense from the circulation
blanchet
parents:
42750
diff
changeset

131 
raise Same.SAME 
42722  132 
 ("tags", (SOME poly, level)) => Tags (poly, level) 
133 
 ("args", (SOME poly, All_Types (* naja *))) => 

134 
Preds (poly, Const_Arg_Types) 

135 
 ("erased", (NONE, All_Types (* naja *))) => 

136 
Preds (Polymorphic, No_Types) 

42753
c9552e617acc
drop some type arguments to constants in unsound type systems + remove a few type systems that make no sense from the circulation
blanchet
parents:
42750
diff
changeset

137 
 _ => raise Same.SAME) 
c9552e617acc
drop some type arguments to constants in unsound type systems + remove a few type systems that make no sense from the circulation
blanchet
parents:
42750
diff
changeset

138 
handle Same.SAME => error ("Unknown type system: " ^ quote s ^ ".") 
42613
23b13b1bd565
use strings to encode type systems in ATP module, to reduce the amount of outofplace information and also to make it easier to print the type system used
blanchet
parents:
42612
diff
changeset

139 

42722  140 
fun polymorphism_of_type_sys (Simple_Types _) = Mangled_Monomorphic 
42613
23b13b1bd565
use strings to encode type systems in ATP module, to reduce the amount of outofplace information and also to make it easier to print the type system used
blanchet
parents:
42612
diff
changeset

141 
 polymorphism_of_type_sys (Preds (poly, _)) = poly 
23b13b1bd565
use strings to encode type systems in ATP module, to reduce the amount of outofplace information and also to make it easier to print the type system used
blanchet
parents:
42612
diff
changeset

142 
 polymorphism_of_type_sys (Tags (poly, _)) = poly 
23b13b1bd565
use strings to encode type systems in ATP module, to reduce the amount of outofplace information and also to make it easier to print the type system used
blanchet
parents:
42612
diff
changeset

143 

42722  144 
fun level_of_type_sys (Simple_Types level) = level 
42613
23b13b1bd565
use strings to encode type systems in ATP module, to reduce the amount of outofplace information and also to make it easier to print the type system used
blanchet
parents:
42612
diff
changeset

145 
 level_of_type_sys (Preds (_, level)) = level 
23b13b1bd565
use strings to encode type systems in ATP module, to reduce the amount of outofplace information and also to make it easier to print the type system used
blanchet
parents:
42612
diff
changeset

146 
 level_of_type_sys (Tags (_, level)) = level 
23b13b1bd565
use strings to encode type systems in ATP module, to reduce the amount of outofplace information and also to make it easier to print the type system used
blanchet
parents:
42612
diff
changeset

147 

42687  148 
fun is_type_level_virtually_sound level = 
149 
level = All_Types orelse level = Nonmonotonic_Types 

42613
23b13b1bd565
use strings to encode type systems in ATP module, to reduce the amount of outofplace information and also to make it easier to print the type system used
blanchet
parents:
42612
diff
changeset

150 
val is_type_sys_virtually_sound = 
23b13b1bd565
use strings to encode type systems in ATP module, to reduce the amount of outofplace information and also to make it easier to print the type system used
blanchet
parents:
42612
diff
changeset

151 
is_type_level_virtually_sound o level_of_type_sys 
23b13b1bd565
use strings to encode type systems in ATP module, to reduce the amount of outofplace information and also to make it easier to print the type system used
blanchet
parents:
42612
diff
changeset

152 

23b13b1bd565
use strings to encode type systems in ATP module, to reduce the amount of outofplace information and also to make it easier to print the type system used
blanchet
parents:
42612
diff
changeset

153 
fun is_type_level_fairly_sound level = 
23b13b1bd565
use strings to encode type systems in ATP module, to reduce the amount of outofplace information and also to make it easier to print the type system used
blanchet
parents:
42612
diff
changeset

154 
is_type_level_virtually_sound level orelse level = Finite_Types 
23b13b1bd565
use strings to encode type systems in ATP module, to reduce the amount of outofplace information and also to make it easier to print the type system used
blanchet
parents:
42612
diff
changeset

155 
val is_type_sys_fairly_sound = is_type_level_fairly_sound o level_of_type_sys 
23b13b1bd565
use strings to encode type systems in ATP module, to reduce the amount of outofplace information and also to make it easier to print the type system used
blanchet
parents:
42612
diff
changeset

156 

42687  157 
fun is_type_level_partial level = 
158 
level = Nonmonotonic_Types orelse level = Finite_Types 

159 

42573
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

160 
fun formula_map f (AQuant (q, xs, phi)) = AQuant (q, xs, formula_map f phi) 
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

161 
 formula_map f (AConn (c, phis)) = AConn (c, map (formula_map f) phis) 
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

162 
 formula_map f (AAtom tm) = AAtom (f tm) 
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

163 

42680  164 
fun formula_fold pos f = 
42677
25496cd3c199
monotonic type inference in ATP Sledgehammer problems  based on Claessen & al.'s CADE 2011 paper, Sect. 2.3.
blanchet
parents:
42675
diff
changeset

165 
let 
25496cd3c199
monotonic type inference in ATP Sledgehammer problems  based on Claessen & al.'s CADE 2011 paper, Sect. 2.3.
blanchet
parents:
42675
diff
changeset

166 
fun aux pos (AQuant (_, _, phi)) = aux pos phi 
42680  167 
 aux pos (AConn (ANot, [phi])) = aux (Option.map not pos) phi 
42677
25496cd3c199
monotonic type inference in ATP Sledgehammer problems  based on Claessen & al.'s CADE 2011 paper, Sect. 2.3.
blanchet
parents:
42675
diff
changeset

168 
 aux pos (AConn (AImplies, [phi1, phi2])) = 
42680  169 
aux (Option.map not pos) phi1 #> aux pos phi2 
170 
 aux pos (AConn (AAnd, phis)) = fold (aux pos) phis 

171 
 aux pos (AConn (AOr, phis)) = fold (aux pos) phis 

172 
 aux _ (AConn (_, phis)) = fold (aux NONE) phis 

42677
25496cd3c199
monotonic type inference in ATP Sledgehammer problems  based on Claessen & al.'s CADE 2011 paper, Sect. 2.3.
blanchet
parents:
42675
diff
changeset

173 
 aux pos (AAtom tm) = f pos tm 
42680  174 
in aux (SOME pos) end 
42573
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

175 

40114  176 
type translated_formula = 
38752
6628adcae4a7
consider "locality" when assigning weights to facts
blanchet
parents:
38748
diff
changeset

177 
{name: string, 
42640
879d2d6b05ce
generate tags for simps, intros, and elims in TPTP poblems on demand
blanchet
parents:
42613
diff
changeset

178 
locality: locality, 
42525
7a506b0b644f
distinguish FOF and TFF (typed firstorder) in ATP abstract syntax tree
blanchet
parents:
42524
diff
changeset

179 
kind: formula_kind, 
42562  180 
combformula: (name, typ, combterm) formula, 
181 
atomic_types: typ list} 

38282
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

182 

42640
879d2d6b05ce
generate tags for simps, intros, and elims in TPTP poblems on demand
blanchet
parents:
42613
diff
changeset

183 
fun update_combformula f ({name, locality, kind, combformula, atomic_types} 
879d2d6b05ce
generate tags for simps, intros, and elims in TPTP poblems on demand
blanchet
parents:
42613
diff
changeset

184 
: translated_formula) = 
879d2d6b05ce
generate tags for simps, intros, and elims in TPTP poblems on demand
blanchet
parents:
42613
diff
changeset

185 
{name = name, locality = locality, kind = kind, combformula = f combformula, 
42562  186 
atomic_types = atomic_types} : translated_formula 
42542
024920b65ce2
perform constant mangling and/or removal of its type args in an earlier phase, so that the rest of the code doesn't need to worry about it
blanchet
parents:
42541
diff
changeset

187 

42558
3d9930cb6770
cleaned up "explicit_apply" so that it shares most of its code path with the default mode of operation
blanchet
parents:
42557
diff
changeset

188 
fun fact_lift f ({combformula, ...} : translated_formula) = f combformula 
3d9930cb6770
cleaned up "explicit_apply" so that it shares most of its code path with the default mode of operation
blanchet
parents:
42557
diff
changeset

189 

42572
0c9a947b43fc
drop "fequal" type args for unmangled type systems
blanchet
parents:
42570
diff
changeset

190 
val boring_consts = [explicit_app_base, @{const_name Metis.fequal}] 
0c9a947b43fc
drop "fequal" type args for unmangled type systems
blanchet
parents:
42570
diff
changeset

191 

0c9a947b43fc
drop "fequal" type args for unmangled type systems
blanchet
parents:
42570
diff
changeset

192 
fun should_omit_type_args type_sys s = 
42589
9f7c48463645
restructured type systems some more  the old naming schemes had "argshg diff less" and "tagshg diff less" as equivalent and didn't support a monomorphic version of "tags"
blanchet
parents:
42586
diff
changeset

193 
s <> type_pred_base andalso s <> type_tag_name andalso 
9f7c48463645
restructured type systems some more  the old naming schemes had "argshg diff less" and "tagshg diff less" as equivalent and didn't support a monomorphic version of "tags"
blanchet
parents:
42586
diff
changeset

194 
(s = @{const_name HOL.eq} orelse level_of_type_sys type_sys = No_Types orelse 
9f7c48463645
restructured type systems some more  the old naming schemes had "argshg diff less" and "tagshg diff less" as equivalent and didn't support a monomorphic version of "tags"
blanchet
parents:
42586
diff
changeset

195 
(case type_sys of 
9f7c48463645
restructured type systems some more  the old naming schemes had "argshg diff less" and "tagshg diff less" as equivalent and didn't support a monomorphic version of "tags"
blanchet
parents:
42586
diff
changeset

196 
Tags (_, All_Types) => true 
9f7c48463645
restructured type systems some more  the old naming schemes had "argshg diff less" and "tagshg diff less" as equivalent and didn't support a monomorphic version of "tags"
blanchet
parents:
42586
diff
changeset

197 
 _ => polymorphism_of_type_sys type_sys <> Mangled_Monomorphic andalso 
9f7c48463645
restructured type systems some more  the old naming schemes had "argshg diff less" and "tagshg diff less" as equivalent and didn't support a monomorphic version of "tags"
blanchet
parents:
42586
diff
changeset

198 
member (op =) boring_consts s)) 
42677
25496cd3c199
monotonic type inference in ATP Sledgehammer problems  based on Claessen & al.'s CADE 2011 paper, Sect. 2.3.
blanchet
parents:
42675
diff
changeset

199 

42753
c9552e617acc
drop some type arguments to constants in unsound type systems + remove a few type systems that make no sense from the circulation
blanchet
parents:
42750
diff
changeset

200 
(* The Booleans indicate whether all type arguments should be kept. *) 
c9552e617acc
drop some type arguments to constants in unsound type systems + remove a few type systems that make no sense from the circulation
blanchet
parents:
42750
diff
changeset

201 
datatype type_arg_policy = 
c9552e617acc
drop some type arguments to constants in unsound type systems + remove a few type systems that make no sense from the circulation
blanchet
parents:
42750
diff
changeset

202 
Explicit_Type_Args of bool  
c9552e617acc
drop some type arguments to constants in unsound type systems + remove a few type systems that make no sense from the circulation
blanchet
parents:
42750
diff
changeset

203 
Mangled_Type_Args of bool  
c9552e617acc
drop some type arguments to constants in unsound type systems + remove a few type systems that make no sense from the circulation
blanchet
parents:
42750
diff
changeset

204 
No_Type_Args 
41136
30bedf58b177
implemented new type system encoding "overload_args", which is more lightweight than "const_args" (the unsound default) and hopefully almost as sound
blanchet
parents:
41134
diff
changeset

205 

42753
c9552e617acc
drop some type arguments to constants in unsound type systems + remove a few type systems that make no sense from the circulation
blanchet
parents:
42750
diff
changeset

206 
(* FIXME: Find out whether and when erasing the nonresult type arguments is 
c9552e617acc
drop some type arguments to constants in unsound type systems + remove a few type systems that make no sense from the circulation
blanchet
parents:
42750
diff
changeset

207 
sound. *) 
42589
9f7c48463645
restructured type systems some more  the old naming schemes had "argshg diff less" and "tagshg diff less" as equivalent and didn't support a monomorphic version of "tags"
blanchet
parents:
42586
diff
changeset

208 
fun general_type_arg_policy type_sys = 
9f7c48463645
restructured type systems some more  the old naming schemes had "argshg diff less" and "tagshg diff less" as equivalent and didn't support a monomorphic version of "tags"
blanchet
parents:
42586
diff
changeset

209 
if level_of_type_sys type_sys = No_Types then 
9f7c48463645
restructured type systems some more  the old naming schemes had "argshg diff less" and "tagshg diff less" as equivalent and didn't support a monomorphic version of "tags"
blanchet
parents:
42586
diff
changeset

210 
No_Type_Args 
9f7c48463645
restructured type systems some more  the old naming schemes had "argshg diff less" and "tagshg diff less" as equivalent and didn't support a monomorphic version of "tags"
blanchet
parents:
42586
diff
changeset

211 
else if polymorphism_of_type_sys type_sys = Mangled_Monomorphic then 
42753
c9552e617acc
drop some type arguments to constants in unsound type systems + remove a few type systems that make no sense from the circulation
blanchet
parents:
42750
diff
changeset

212 
Mangled_Type_Args (is_type_sys_virtually_sound type_sys) 
42589
9f7c48463645
restructured type systems some more  the old naming schemes had "argshg diff less" and "tagshg diff less" as equivalent and didn't support a monomorphic version of "tags"
blanchet
parents:
42586
diff
changeset

213 
else 
42753
c9552e617acc
drop some type arguments to constants in unsound type systems + remove a few type systems that make no sense from the circulation
blanchet
parents:
42750
diff
changeset

214 
Explicit_Type_Args (is_type_sys_virtually_sound type_sys) 
42563  215 

42524  216 
fun type_arg_policy type_sys s = 
42572
0c9a947b43fc
drop "fequal" type args for unmangled type systems
blanchet
parents:
42570
diff
changeset

217 
if should_omit_type_args type_sys s then No_Type_Args 
42563  218 
else general_type_arg_policy type_sys 
42227
662b50b7126f
if "monomorphize" is enabled, mangle the type information in the names by default
blanchet
parents:
42180
diff
changeset

219 

41136
30bedf58b177
implemented new type system encoding "overload_args", which is more lightweight than "const_args" (the unsound default) and hopefully almost as sound
blanchet
parents:
41134
diff
changeset

220 
fun num_atp_type_args thy type_sys s = 
42753
c9552e617acc
drop some type arguments to constants in unsound type systems + remove a few type systems that make no sense from the circulation
blanchet
parents:
42750
diff
changeset

221 
case type_arg_policy type_sys s of 
c9552e617acc
drop some type arguments to constants in unsound type systems + remove a few type systems that make no sense from the circulation
blanchet
parents:
42750
diff
changeset

222 
Explicit_Type_Args keep_all => 
c9552e617acc
drop some type arguments to constants in unsound type systems + remove a few type systems that make no sense from the circulation
blanchet
parents:
42750
diff
changeset

223 
if keep_all then num_type_args thy s 
c9552e617acc
drop some type arguments to constants in unsound type systems + remove a few type systems that make no sense from the circulation
blanchet
parents:
42750
diff
changeset

224 
else error "not implemented yet" (* FIXME *) 
c9552e617acc
drop some type arguments to constants in unsound type systems + remove a few type systems that make no sense from the circulation
blanchet
parents:
42750
diff
changeset

225 
 _ => 0 
41136
30bedf58b177
implemented new type system encoding "overload_args", which is more lightweight than "const_args" (the unsound default) and hopefully almost as sound
blanchet
parents:
41134
diff
changeset

226 

42353
7797efa897a1
correctly handle TFrees that occur in (local) facts  Metis did the right thing here but Sledgehammer was incorrectly generating spurious preconditions such as "dense_linorder(t_a)"
blanchet
parents:
42237
diff
changeset

227 
fun atp_type_literals_for_types type_sys kind Ts = 
42589
9f7c48463645
restructured type systems some more  the old naming schemes had "argshg diff less" and "tagshg diff less" as equivalent and didn't support a monomorphic version of "tags"
blanchet
parents:
42586
diff
changeset

228 
if level_of_type_sys type_sys = No_Types then 
42353
7797efa897a1
correctly handle TFrees that occur in (local) facts  Metis did the right thing here but Sledgehammer was incorrectly generating spurious preconditions such as "dense_linorder(t_a)"
blanchet
parents:
42237
diff
changeset

229 
[] 
7797efa897a1
correctly handle TFrees that occur in (local) facts  Metis did the right thing here but Sledgehammer was incorrectly generating spurious preconditions such as "dense_linorder(t_a)"
blanchet
parents:
42237
diff
changeset

230 
else 
7797efa897a1
correctly handle TFrees that occur in (local) facts  Metis did the right thing here but Sledgehammer was incorrectly generating spurious preconditions such as "dense_linorder(t_a)"
blanchet
parents:
42237
diff
changeset

231 
Ts > type_literals_for_types 
7797efa897a1
correctly handle TFrees that occur in (local) facts  Metis did the right thing here but Sledgehammer was incorrectly generating spurious preconditions such as "dense_linorder(t_a)"
blanchet
parents:
42237
diff
changeset

232 
> filter (fn TyLitVar _ => kind <> Conjecture 
7797efa897a1
correctly handle TFrees that occur in (local) facts  Metis did the right thing here but Sledgehammer was incorrectly generating spurious preconditions such as "dense_linorder(t_a)"
blanchet
parents:
42237
diff
changeset

233 
 TyLitFree _ => kind = Conjecture) 
41137
8b634031b2a5
implemented "no_types" encoding, which is too unsound to be useful but can come in handy for evaluations
blanchet
parents:
41136
diff
changeset

234 

42709
e7af132d48fe
allow each prover to specify its own formula kind for symbols occurring in the conjecture
blanchet
parents:
42701
diff
changeset

235 
fun mk_anot phi = AConn (ANot, [phi]) 
38282
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

236 
fun mk_aconn c phi1 phi2 = AConn (c, [phi1, phi2]) 
42534
46e690db16b8
fake type declarations for fulltype args and mangled type encodings, so that type assumptions can be discharged
blanchet
parents:
42533
diff
changeset

237 
fun mk_aconns c phis = 
46e690db16b8
fake type declarations for fulltype args and mangled type encodings, so that type assumptions can be discharged
blanchet
parents:
42533
diff
changeset

238 
let val (phis', phi') = split_last phis in 
46e690db16b8
fake type declarations for fulltype args and mangled type encodings, so that type assumptions can be discharged
blanchet
parents:
42533
diff
changeset

239 
fold_rev (mk_aconn c) phis' phi' 
46e690db16b8
fake type declarations for fulltype args and mangled type encodings, so that type assumptions can be discharged
blanchet
parents:
42533
diff
changeset

240 
end 
38282
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

241 
fun mk_ahorn [] phi = phi 
42534
46e690db16b8
fake type declarations for fulltype args and mangled type encodings, so that type assumptions can be discharged
blanchet
parents:
42533
diff
changeset

242 
 mk_ahorn phis psi = AConn (AImplies, [mk_aconns AAnd phis, psi]) 
42522
413b56894f82
close ATP formulas universally earlier, so that we can add type predicates
blanchet
parents:
42521
diff
changeset

243 
fun mk_aquant _ [] phi = phi 
413b56894f82
close ATP formulas universally earlier, so that we can add type predicates
blanchet
parents:
42521
diff
changeset

244 
 mk_aquant q xs (phi as AQuant (q', xs', phi')) = 
413b56894f82
close ATP formulas universally earlier, so that we can add type predicates
blanchet
parents:
42521
diff
changeset

245 
if q = q' then AQuant (q, xs @ xs', phi') else AQuant (q, xs, phi) 
413b56894f82
close ATP formulas universally earlier, so that we can add type predicates
blanchet
parents:
42521
diff
changeset

246 
 mk_aquant q xs phi = AQuant (q, xs, phi) 
38282
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

247 

42522
413b56894f82
close ATP formulas universally earlier, so that we can add type predicates
blanchet
parents:
42521
diff
changeset

248 
fun close_universally atom_vars phi = 
41145
a5ee3b8e5a90
improve partially tagged encoding by adding a helper fact that coalesces consecutive "ti" tags
blanchet
parents:
41140
diff
changeset

249 
let 
a5ee3b8e5a90
improve partially tagged encoding by adding a helper fact that coalesces consecutive "ti" tags
blanchet
parents:
41140
diff
changeset

250 
fun formula_vars bounds (AQuant (_, xs, phi)) = 
42526  251 
formula_vars (map fst xs @ bounds) phi 
41145
a5ee3b8e5a90
improve partially tagged encoding by adding a helper fact that coalesces consecutive "ti" tags
blanchet
parents:
41140
diff
changeset

252 
 formula_vars bounds (AConn (_, phis)) = fold (formula_vars bounds) phis 
42522
413b56894f82
close ATP formulas universally earlier, so that we can add type predicates
blanchet
parents:
42521
diff
changeset

253 
 formula_vars bounds (AAtom tm) = 
42526  254 
union (op =) (atom_vars tm [] 
255 
> filter_out (member (op =) bounds o fst)) 

42522
413b56894f82
close ATP formulas universally earlier, so that we can add type predicates
blanchet
parents:
42521
diff
changeset

256 
in mk_aquant AForall (formula_vars [] phi []) phi end 
413b56894f82
close ATP formulas universally earlier, so that we can add type predicates
blanchet
parents:
42521
diff
changeset

257 

42531
a462dbaa584f
added more rudimentary type support to Sledgehammer's ATP encoding
blanchet
parents:
42530
diff
changeset

258 
fun combterm_vars (CombApp (tm1, tm2)) = fold combterm_vars [tm1, tm2] 
42522
413b56894f82
close ATP formulas universally earlier, so that we can add type predicates
blanchet
parents:
42521
diff
changeset

259 
 combterm_vars (CombConst _) = I 
42574  260 
 combterm_vars (CombVar (name, T)) = insert (op =) (name, SOME T) 
42674  261 
fun close_combformula_universally phi = close_universally combterm_vars phi 
42522
413b56894f82
close ATP formulas universally earlier, so that we can add type predicates
blanchet
parents:
42521
diff
changeset

262 

413b56894f82
close ATP formulas universally earlier, so that we can add type predicates
blanchet
parents:
42521
diff
changeset

263 
fun term_vars (ATerm (name as (s, _), tms)) = 
42531
a462dbaa584f
added more rudimentary type support to Sledgehammer's ATP encoding
blanchet
parents:
42530
diff
changeset

264 
is_atp_variable s ? insert (op =) (name, NONE) 
42526  265 
#> fold term_vars tms 
42674  266 
fun close_formula_universally phi = close_universally term_vars phi 
41145
a5ee3b8e5a90
improve partially tagged encoding by adding a helper fact that coalesces consecutive "ti" tags
blanchet
parents:
41140
diff
changeset

267 

42562  268 
fun fo_term_from_typ (Type (s, Ts)) = 
269 
ATerm (`make_fixed_type_const s, map fo_term_from_typ Ts) 

270 
 fo_term_from_typ (TFree (s, _)) = 

271 
ATerm (`make_fixed_type_var s, []) 

272 
 fo_term_from_typ (TVar ((x as (s, _)), _)) = 

273 
ATerm ((make_schematic_type_var x, s), []) 

274 

275 
(* This shouldn't clash with anything else. *) 

42542
024920b65ce2
perform constant mangling and/or removal of its type args in an earlier phase, so that the rest of the code doesn't need to worry about it
blanchet
parents:
42541
diff
changeset

276 
val mangled_type_sep = "\000" 
024920b65ce2
perform constant mangling and/or removal of its type args in an earlier phase, so that the rest of the code doesn't need to worry about it
blanchet
parents:
42541
diff
changeset

277 

42562  278 
fun generic_mangled_type_name f (ATerm (name, [])) = f name 
279 
 generic_mangled_type_name f (ATerm (name, tys)) = 

280 
f name ^ "(" ^ commas (map (generic_mangled_type_name f) tys) ^ ")" 

281 
val mangled_type_name = 

282 
fo_term_from_typ 

283 
#> (fn ty => (make_tff_type (generic_mangled_type_name fst ty), 

284 
generic_mangled_type_name snd ty)) 

42542
024920b65ce2
perform constant mangling and/or removal of its type args in an earlier phase, so that the rest of the code doesn't need to worry about it
blanchet
parents:
42541
diff
changeset

285 

42574  286 
fun generic_mangled_type_suffix f g Ts = 
42542
024920b65ce2
perform constant mangling and/or removal of its type args in an earlier phase, so that the rest of the code doesn't need to worry about it
blanchet
parents:
42541
diff
changeset

287 
fold_rev (curry (op ^) o g o prefix mangled_type_sep 
42574  288 
o generic_mangled_type_name f) Ts "" 
42562  289 
fun mangled_const_name T_args (s, s') = 
290 
let val ty_args = map fo_term_from_typ T_args in 

291 
(s ^ generic_mangled_type_suffix fst ascii_of ty_args, 

292 
s' ^ generic_mangled_type_suffix snd I ty_args) 

293 
end 

42542
024920b65ce2
perform constant mangling and/or removal of its type args in an earlier phase, so that the rest of the code doesn't need to worry about it
blanchet
parents:
42541
diff
changeset

294 

024920b65ce2
perform constant mangling and/or removal of its type args in an earlier phase, so that the rest of the code doesn't need to worry about it
blanchet
parents:
42541
diff
changeset

295 
val parse_mangled_ident = 
024920b65ce2
perform constant mangling and/or removal of its type args in an earlier phase, so that the rest of the code doesn't need to worry about it
blanchet
parents:
42541
diff
changeset

296 
Scan.many1 (not o member (op =) ["(", ")", ","]) >> implode 
024920b65ce2
perform constant mangling and/or removal of its type args in an earlier phase, so that the rest of the code doesn't need to worry about it
blanchet
parents:
42541
diff
changeset

297 

024920b65ce2
perform constant mangling and/or removal of its type args in an earlier phase, so that the rest of the code doesn't need to worry about it
blanchet
parents:
42541
diff
changeset

298 
fun parse_mangled_type x = 
024920b65ce2
perform constant mangling and/or removal of its type args in an earlier phase, so that the rest of the code doesn't need to worry about it
blanchet
parents:
42541
diff
changeset

299 
(parse_mangled_ident 
024920b65ce2
perform constant mangling and/or removal of its type args in an earlier phase, so that the rest of the code doesn't need to worry about it
blanchet
parents:
42541
diff
changeset

300 
 Scan.optional ($$ "("  Scan.optional parse_mangled_types []  $$ ")") 
024920b65ce2
perform constant mangling and/or removal of its type args in an earlier phase, so that the rest of the code doesn't need to worry about it
blanchet
parents:
42541
diff
changeset

301 
[] >> ATerm) x 
024920b65ce2
perform constant mangling and/or removal of its type args in an earlier phase, so that the rest of the code doesn't need to worry about it
blanchet
parents:
42541
diff
changeset

302 
and parse_mangled_types x = 
024920b65ce2
perform constant mangling and/or removal of its type args in an earlier phase, so that the rest of the code doesn't need to worry about it
blanchet
parents:
42541
diff
changeset

303 
(parse_mangled_type ::: Scan.repeat ($$ ","  parse_mangled_type)) x 
024920b65ce2
perform constant mangling and/or removal of its type args in an earlier phase, so that the rest of the code doesn't need to worry about it
blanchet
parents:
42541
diff
changeset

304 

024920b65ce2
perform constant mangling and/or removal of its type args in an earlier phase, so that the rest of the code doesn't need to worry about it
blanchet
parents:
42541
diff
changeset

305 
fun unmangled_type s = 
024920b65ce2
perform constant mangling and/or removal of its type args in an earlier phase, so that the rest of the code doesn't need to worry about it
blanchet
parents:
42541
diff
changeset

306 
s > suffix ")" > raw_explode 
024920b65ce2
perform constant mangling and/or removal of its type args in an earlier phase, so that the rest of the code doesn't need to worry about it
blanchet
parents:
42541
diff
changeset

307 
> Scan.finite Symbol.stopper 
024920b65ce2
perform constant mangling and/or removal of its type args in an earlier phase, so that the rest of the code doesn't need to worry about it
blanchet
parents:
42541
diff
changeset

308 
(Scan.error (!! (fn _ => raise Fail ("unrecognized mangled type " ^ 
024920b65ce2
perform constant mangling and/or removal of its type args in an earlier phase, so that the rest of the code doesn't need to worry about it
blanchet
parents:
42541
diff
changeset

309 
quote s)) parse_mangled_type)) 
024920b65ce2
perform constant mangling and/or removal of its type args in an earlier phase, so that the rest of the code doesn't need to worry about it
blanchet
parents:
42541
diff
changeset

310 
> fst 
024920b65ce2
perform constant mangling and/or removal of its type args in an earlier phase, so that the rest of the code doesn't need to worry about it
blanchet
parents:
42541
diff
changeset

311 

42561
23ddc4e3d19c
have properly typeinstantiated helper facts (combinators and If)
blanchet
parents:
42560
diff
changeset

312 
val unmangled_const_name = space_explode mangled_type_sep #> hd 
42542
024920b65ce2
perform constant mangling and/or removal of its type args in an earlier phase, so that the rest of the code doesn't need to worry about it
blanchet
parents:
42541
diff
changeset

313 
fun unmangled_const s = 
024920b65ce2
perform constant mangling and/or removal of its type args in an earlier phase, so that the rest of the code doesn't need to worry about it
blanchet
parents:
42541
diff
changeset

314 
let val ss = space_explode mangled_type_sep s in 
024920b65ce2
perform constant mangling and/or removal of its type args in an earlier phase, so that the rest of the code doesn't need to worry about it
blanchet
parents:
42541
diff
changeset

315 
(hd ss, map unmangled_type (tl ss)) 
024920b65ce2
perform constant mangling and/or removal of its type args in an earlier phase, so that the rest of the code doesn't need to worry about it
blanchet
parents:
42541
diff
changeset

316 
end 
024920b65ce2
perform constant mangling and/or removal of its type args in an earlier phase, so that the rest of the code doesn't need to worry about it
blanchet
parents:
42541
diff
changeset

317 

42674  318 
fun introduce_proxies tm = 
42568
7b9801a34836
no needless "fequal" proxies if "explicit_apply" is set + always have readable names
blanchet
parents:
42566
diff
changeset

319 
let 
7b9801a34836
no needless "fequal" proxies if "explicit_apply" is set + always have readable names
blanchet
parents:
42566
diff
changeset

320 
fun aux top_level (CombApp (tm1, tm2)) = 
7b9801a34836
no needless "fequal" proxies if "explicit_apply" is set + always have readable names
blanchet
parents:
42566
diff
changeset

321 
CombApp (aux top_level tm1, aux false tm2) 
42574  322 
 aux top_level (CombConst (name as (s, s'), T, T_args)) = 
42570
77f94ac04f32
cleanup proxification/unproxification and make sure that "num_atp_type_args" is called on the proxy in the reconstruction code, since "c_fequal" has one type arg but the unproxified equal has 0
blanchet
parents:
42569
diff
changeset

323 
(case proxify_const s of 
42568
7b9801a34836
no needless "fequal" proxies if "explicit_apply" is set + always have readable names
blanchet
parents:
42566
diff
changeset

324 
SOME proxy_base => 
7b9801a34836
no needless "fequal" proxies if "explicit_apply" is set + always have readable names
blanchet
parents:
42566
diff
changeset

325 
if top_level then 
7b9801a34836
no needless "fequal" proxies if "explicit_apply" is set + always have readable names
blanchet
parents:
42566
diff
changeset

326 
(case s of 
7b9801a34836
no needless "fequal" proxies if "explicit_apply" is set + always have readable names
blanchet
parents:
42566
diff
changeset

327 
"c_False" => (tptp_false, s') 
7b9801a34836
no needless "fequal" proxies if "explicit_apply" is set + always have readable names
blanchet
parents:
42566
diff
changeset

328 
 "c_True" => (tptp_true, s') 
7b9801a34836
no needless "fequal" proxies if "explicit_apply" is set + always have readable names
blanchet
parents:
42566
diff
changeset

329 
 _ => name, []) 
42569
5737947e4c77
make sure that fequal keeps its type arguments for mangled type systems
blanchet
parents:
42568
diff
changeset

330 
else 
42574  331 
(proxy_base >> prefix const_prefix, T_args) 
332 
 NONE => (name, T_args)) 

333 
> (fn (name, T_args) => CombConst (name, T, T_args)) 

42568
7b9801a34836
no needless "fequal" proxies if "explicit_apply" is set + always have readable names
blanchet
parents:
42566
diff
changeset

334 
 aux _ tm = tm 
42674  335 
in aux true tm end 
42568
7b9801a34836
no needless "fequal" proxies if "explicit_apply" is set + always have readable names
blanchet
parents:
42566
diff
changeset

336 

42562  337 
fun combformula_from_prop thy eq_as_iff = 
38282
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

338 
let 
42568
7b9801a34836
no needless "fequal" proxies if "explicit_apply" is set + always have readable names
blanchet
parents:
42566
diff
changeset

339 
fun do_term bs t atomic_types = 
41140
9c68004b8c9d
added Sledgehammer support for higherorder propositional reasoning
blanchet
parents:
41138
diff
changeset

340 
combterm_from_term thy bs (Envir.eta_contract t) 
42568
7b9801a34836
no needless "fequal" proxies if "explicit_apply" is set + always have readable names
blanchet
parents:
42566
diff
changeset

341 
>> (introduce_proxies #> AAtom) 
7b9801a34836
no needless "fequal" proxies if "explicit_apply" is set + always have readable names
blanchet
parents:
42566
diff
changeset

342 
> union (op =) atomic_types 
38282
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

343 
fun do_quant bs q s T t' = 
38518
54727b44e277
handle bound name conflicts gracefully in FOF translation
blanchet
parents:
38496
diff
changeset

344 
let val s = Name.variant (map fst bs) s in 
54727b44e277
handle bound name conflicts gracefully in FOF translation
blanchet
parents:
38496
diff
changeset

345 
do_formula ((s, T) :: bs) t' 
42562  346 
#>> mk_aquant q [(`make_bound_var s, SOME T)] 
38518
54727b44e277
handle bound name conflicts gracefully in FOF translation
blanchet
parents:
38496
diff
changeset

347 
end 
38282
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

348 
and do_conn bs c t1 t2 = 
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

349 
do_formula bs t1 ##>> do_formula bs t2 
42531
a462dbaa584f
added more rudimentary type support to Sledgehammer's ATP encoding
blanchet
parents:
42530
diff
changeset

350 
#>> uncurry (mk_aconn c) 
38282
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

351 
and do_formula bs t = 
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

352 
case t of 
42531
a462dbaa584f
added more rudimentary type support to Sledgehammer's ATP encoding
blanchet
parents:
42530
diff
changeset

353 
@{const Not} $ t1 => do_formula bs t1 #>> mk_anot 
38282
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

354 
 Const (@{const_name All}, _) $ Abs (s, T, t') => 
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

355 
do_quant bs AForall s T t' 
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

356 
 Const (@{const_name Ex}, _) $ Abs (s, T, t') => 
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

357 
do_quant bs AExists s T t' 
38795
848be46708dc
formerly unnamed infix conjunction and disjunction now named HOL.conj and HOL.disj
haftmann
parents:
38786
diff
changeset

358 
 @{const HOL.conj} $ t1 $ t2 => do_conn bs AAnd t1 t2 
848be46708dc
formerly unnamed infix conjunction and disjunction now named HOL.conj and HOL.disj
haftmann
parents:
38786
diff
changeset

359 
 @{const HOL.disj} $ t1 $ t2 => do_conn bs AOr t1 t2 
38786
e46e7a9cb622
formerly unnamed infix impliciation now named HOL.implies
haftmann
parents:
38752
diff
changeset

360 
 @{const HOL.implies} $ t1 $ t2 => do_conn bs AImplies t1 t2 
38864
4abe644fcea5
formerly unnamed infix equality now named HOL.eq
haftmann
parents:
38829
diff
changeset

361 
 Const (@{const_name HOL.eq}, Type (_, [@{typ bool}, _])) $ t1 $ t2 => 
41140
9c68004b8c9d
added Sledgehammer support for higherorder propositional reasoning
blanchet
parents:
41138
diff
changeset

362 
if eq_as_iff then do_conn bs AIff t1 t2 else do_term bs t 
9c68004b8c9d
added Sledgehammer support for higherorder propositional reasoning
blanchet
parents:
41138
diff
changeset

363 
 _ => do_term bs t 
38282
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

364 
in do_formula [] end 
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

365 

42750
c8b1d9ee3758
ensure Set.member isn't introduced by Meson's preprocessing if it's supposed to be unfolded
blanchet
parents:
42747
diff
changeset

366 
fun presimplify_term ctxt = 
c8b1d9ee3758
ensure Set.member isn't introduced by Meson's preprocessing if it's supposed to be unfolded
blanchet
parents:
42747
diff
changeset

367 
Skip_Proof.make_thm (Proof_Context.theory_of ctxt) 
c8b1d9ee3758
ensure Set.member isn't introduced by Meson's preprocessing if it's supposed to be unfolded
blanchet
parents:
42747
diff
changeset

368 
#> Meson.presimplify ctxt 
c8b1d9ee3758
ensure Set.member isn't introduced by Meson's preprocessing if it's supposed to be unfolded
blanchet
parents:
42747
diff
changeset

369 
#> prop_of 
38282
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

370 

41491  371 
fun concealed_bound_name j = sledgehammer_weak_prefix ^ string_of_int j 
38282
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

372 
fun conceal_bounds Ts t = 
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

373 
subst_bounds (map (Free o apfst concealed_bound_name) 
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

374 
(0 upto length Ts  1 ~~ Ts), t) 
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

375 
fun reveal_bounds Ts = 
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

376 
subst_atomic (map (fn (j, T) => (Free (concealed_bound_name j, T), Bound j)) 
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

377 
(0 upto length Ts  1 ~~ Ts)) 
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

378 

42747
f132d13fcf75
use the same code for extensionalization in Metis and Sledgehammer and generalize that code so that it gracefully handles negations (e.g. negated conjecture), formulas of the form (%x. t) = u, etc.
blanchet
parents:
42742
diff
changeset

379 
fun extensionalize_term ctxt t = 
f132d13fcf75
use the same code for extensionalization in Metis and Sledgehammer and generalize that code so that it gracefully handles negations (e.g. negated conjecture), formulas of the form (%x. t) = u, etc.
blanchet
parents:
42742
diff
changeset

380 
let val thy = Proof_Context.theory_of ctxt in 
f132d13fcf75
use the same code for extensionalization in Metis and Sledgehammer and generalize that code so that it gracefully handles negations (e.g. negated conjecture), formulas of the form (%x. t) = u, etc.
blanchet
parents:
42742
diff
changeset

381 
t > cterm_of thy > Meson.extensionalize_conv ctxt 
f132d13fcf75
use the same code for extensionalization in Metis and Sledgehammer and generalize that code so that it gracefully handles negations (e.g. negated conjecture), formulas of the form (%x. t) = u, etc.
blanchet
parents:
42742
diff
changeset

382 
> prop_of > Logic.dest_equals > snd 
f132d13fcf75
use the same code for extensionalization in Metis and Sledgehammer and generalize that code so that it gracefully handles negations (e.g. negated conjecture), formulas of the form (%x. t) = u, etc.
blanchet
parents:
42742
diff
changeset

383 
end 
38608
01ed56c46259
beta eta contract the Sledgehammer conjecture (and also the axioms, although this might not be needed), just like Metis does (implicitly);
blanchet
parents:
38606
diff
changeset

384 

38282
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

385 
fun introduce_combinators_in_term ctxt kind t = 
42361  386 
let val thy = Proof_Context.theory_of ctxt in 
38491
f7e51d981a9f
invoke Variable.export/import_term on the entire formula, to make sure that schematic variables don't get different indices in different subterms;
blanchet
parents:
38282
diff
changeset

387 
if Meson.is_fol_term thy t then 
f7e51d981a9f
invoke Variable.export/import_term on the entire formula, to make sure that schematic variables don't get different indices in different subterms;
blanchet
parents:
38282
diff
changeset

388 
t 
f7e51d981a9f
invoke Variable.export/import_term on the entire formula, to make sure that schematic variables don't get different indices in different subterms;
blanchet
parents:
38282
diff
changeset

389 
else 
f7e51d981a9f
invoke Variable.export/import_term on the entire formula, to make sure that schematic variables don't get different indices in different subterms;
blanchet
parents:
38282
diff
changeset

390 
let 
f7e51d981a9f
invoke Variable.export/import_term on the entire formula, to make sure that schematic variables don't get different indices in different subterms;
blanchet
parents:
38282
diff
changeset

391 
fun aux Ts t = 
f7e51d981a9f
invoke Variable.export/import_term on the entire formula, to make sure that schematic variables don't get different indices in different subterms;
blanchet
parents:
38282
diff
changeset

392 
case t of 
f7e51d981a9f
invoke Variable.export/import_term on the entire formula, to make sure that schematic variables don't get different indices in different subterms;
blanchet
parents:
38282
diff
changeset

393 
@{const Not} $ t1 => @{const Not} $ aux Ts t1 
f7e51d981a9f
invoke Variable.export/import_term on the entire formula, to make sure that schematic variables don't get different indices in different subterms;
blanchet
parents:
38282
diff
changeset

394 
 (t0 as Const (@{const_name All}, _)) $ Abs (s, T, t') => 
f7e51d981a9f
invoke Variable.export/import_term on the entire formula, to make sure that schematic variables don't get different indices in different subterms;
blanchet
parents:
38282
diff
changeset

395 
t0 $ Abs (s, T, aux (T :: Ts) t') 
38652
e063be321438
perform etaexpansion of quantifier bodies in Sledgehammer translation when needed + transform elim rules later;
blanchet
parents:
38618
diff
changeset

396 
 (t0 as Const (@{const_name All}, _)) $ t1 => 
e063be321438
perform etaexpansion of quantifier bodies in Sledgehammer translation when needed + transform elim rules later;
blanchet
parents:
38618
diff
changeset

397 
aux Ts (t0 $ eta_expand Ts t1 1) 
38491
f7e51d981a9f
invoke Variable.export/import_term on the entire formula, to make sure that schematic variables don't get different indices in different subterms;
blanchet
parents:
38282
diff
changeset

398 
 (t0 as Const (@{const_name Ex}, _)) $ Abs (s, T, t') => 
f7e51d981a9f
invoke Variable.export/import_term on the entire formula, to make sure that schematic variables don't get different indices in different subterms;
blanchet
parents:
38282
diff
changeset

399 
t0 $ Abs (s, T, aux (T :: Ts) t') 
38652
e063be321438
perform etaexpansion of quantifier bodies in Sledgehammer translation when needed + transform elim rules later;
blanchet
parents:
38618
diff
changeset

400 
 (t0 as Const (@{const_name Ex}, _)) $ t1 => 
e063be321438
perform etaexpansion of quantifier bodies in Sledgehammer translation when needed + transform elim rules later;
blanchet
parents:
38618
diff
changeset

401 
aux Ts (t0 $ eta_expand Ts t1 1) 
38795
848be46708dc
formerly unnamed infix conjunction and disjunction now named HOL.conj and HOL.disj
haftmann
parents:
38786
diff
changeset

402 
 (t0 as @{const HOL.conj}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2 
848be46708dc
formerly unnamed infix conjunction and disjunction now named HOL.conj and HOL.disj
haftmann
parents:
38786
diff
changeset

403 
 (t0 as @{const HOL.disj}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2 
38786
e46e7a9cb622
formerly unnamed infix impliciation now named HOL.implies
haftmann
parents:
38752
diff
changeset

404 
 (t0 as @{const HOL.implies}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2 
38864
4abe644fcea5
formerly unnamed infix equality now named HOL.eq
haftmann
parents:
38829
diff
changeset

405 
 (t0 as Const (@{const_name HOL.eq}, Type (_, [@{typ bool}, _]))) 
38491
f7e51d981a9f
invoke Variable.export/import_term on the entire formula, to make sure that schematic variables don't get different indices in different subterms;
blanchet
parents:
38282
diff
changeset

406 
$ t1 $ t2 => 
f7e51d981a9f
invoke Variable.export/import_term on the entire formula, to make sure that schematic variables don't get different indices in different subterms;
blanchet
parents:
38282
diff
changeset

407 
t0 $ aux Ts t1 $ aux Ts t2 
f7e51d981a9f
invoke Variable.export/import_term on the entire formula, to make sure that schematic variables don't get different indices in different subterms;
blanchet
parents:
38282
diff
changeset

408 
 _ => if not (exists_subterm (fn Abs _ => true  _ => false) t) then 
f7e51d981a9f
invoke Variable.export/import_term on the entire formula, to make sure that schematic variables don't get different indices in different subterms;
blanchet
parents:
38282
diff
changeset

409 
t 
f7e51d981a9f
invoke Variable.export/import_term on the entire formula, to make sure that schematic variables don't get different indices in different subterms;
blanchet
parents:
38282
diff
changeset

410 
else 
f7e51d981a9f
invoke Variable.export/import_term on the entire formula, to make sure that schematic variables don't get different indices in different subterms;
blanchet
parents:
38282
diff
changeset

411 
t > conceal_bounds Ts 
f7e51d981a9f
invoke Variable.export/import_term on the entire formula, to make sure that schematic variables don't get different indices in different subterms;
blanchet
parents:
38282
diff
changeset

412 
> Envir.eta_contract 
f7e51d981a9f
invoke Variable.export/import_term on the entire formula, to make sure that schematic variables don't get different indices in different subterms;
blanchet
parents:
38282
diff
changeset

413 
> cterm_of thy 
39890  414 
> Meson_Clausify.introduce_combinators_in_cterm 
38491
f7e51d981a9f
invoke Variable.export/import_term on the entire formula, to make sure that schematic variables don't get different indices in different subterms;
blanchet
parents:
38282
diff
changeset

415 
> prop_of > Logic.dest_equals > snd 
f7e51d981a9f
invoke Variable.export/import_term on the entire formula, to make sure that schematic variables don't get different indices in different subterms;
blanchet
parents:
38282
diff
changeset

416 
> reveal_bounds Ts 
39370
f8292d3020db
use same hack as in "Async_Manager" to work around Proof General bug
blanchet
parents:
39005
diff
changeset

417 
val (t, ctxt') = Variable.import_terms true [t] ctxt >> the_single 
38491
f7e51d981a9f
invoke Variable.export/import_term on the entire formula, to make sure that schematic variables don't get different indices in different subterms;
blanchet
parents:
38282
diff
changeset

418 
in t > aux [] > singleton (Variable.export_terms ctxt' ctxt) end 
f7e51d981a9f
invoke Variable.export/import_term on the entire formula, to make sure that schematic variables don't get different indices in different subterms;
blanchet
parents:
38282
diff
changeset

419 
handle THM _ => 
f7e51d981a9f
invoke Variable.export/import_term on the entire formula, to make sure that schematic variables don't get different indices in different subterms;
blanchet
parents:
38282
diff
changeset

420 
(* A type variable of sort "{}" will make abstraction fail. *) 
38613
4ca2cae2653f
use "hypothesis" rather than "conjecture" for hypotheses in TPTP format;
blanchet
parents:
38610
diff
changeset

421 
if kind = Conjecture then HOLogic.false_const 
4ca2cae2653f
use "hypothesis" rather than "conjecture" for hypotheses in TPTP format;
blanchet
parents:
38610
diff
changeset

422 
else HOLogic.true_const 
38491
f7e51d981a9f
invoke Variable.export/import_term on the entire formula, to make sure that schematic variables don't get different indices in different subterms;
blanchet
parents:
38282
diff
changeset

423 
end 
38282
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

424 

319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

425 
(* Metis's use of "resolve_tac" freezes the schematic variables. We simulate the 
42353
7797efa897a1
correctly handle TFrees that occur in (local) facts  Metis did the right thing here but Sledgehammer was incorrectly generating spurious preconditions such as "dense_linorder(t_a)"
blanchet
parents:
42237
diff
changeset

426 
same in Sledgehammer to prevent the discovery of unreplayable proofs. *) 
38282
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

427 
fun freeze_term t = 
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

428 
let 
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

429 
fun aux (t $ u) = aux t $ aux u 
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

430 
 aux (Abs (s, T, t)) = Abs (s, T, aux t) 
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

431 
 aux (Var ((s, i), T)) = 
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

432 
Free (sledgehammer_weak_prefix ^ s ^ "_" ^ string_of_int i, T) 
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

433 
 aux t = t 
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

434 
in t > exists_subterm is_Var t ? aux end 
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

435 

40204
da97d75e20e6
standardize on "fact" terminology (vs. "axiom" or "theorem") in Sledgehammer  but keep "Axiom" in the lowerlevel "ATP_Problem" module
blanchet
parents:
40145
diff
changeset

436 
(* making fact and conjecture formulas *) 
42640
879d2d6b05ce
generate tags for simps, intros, and elims in TPTP poblems on demand
blanchet
parents:
42613
diff
changeset

437 
fun make_formula ctxt eq_as_iff presimp name loc kind t = 
38282
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

438 
let 
42361  439 
val thy = Proof_Context.theory_of ctxt 
38608
01ed56c46259
beta eta contract the Sledgehammer conjecture (and also the axioms, although this might not be needed), just like Metis does (implicitly);
blanchet
parents:
38606
diff
changeset

440 
val t = t > Envir.beta_eta_contract 
38652
e063be321438
perform etaexpansion of quantifier bodies in Sledgehammer translation when needed + transform elim rules later;
blanchet
parents:
38618
diff
changeset

441 
> transform_elim_term 
41211
1e2e16bc0077
no need to do a superduper atomization if Metis fails afterwards anyway
blanchet
parents:
41199
diff
changeset

442 
> Object_Logic.atomize_term thy 
42563  443 
val need_trueprop = (fastype_of t = @{typ bool}) 
38652
e063be321438
perform etaexpansion of quantifier bodies in Sledgehammer translation when needed + transform elim rules later;
blanchet
parents:
38618
diff
changeset

444 
val t = t > need_trueprop ? HOLogic.mk_Trueprop 
42742
369dfc819056
unfold set constants in Sledgehammer/ATP as well if Metis does it too
blanchet
parents:
42734
diff
changeset

445 
> Raw_Simplifier.rewrite_term thy 
369dfc819056
unfold set constants in Sledgehammer/ATP as well if Metis does it too
blanchet
parents:
42734
diff
changeset

446 
(Meson.unfold_set_const_simps ctxt) [] 
42747
f132d13fcf75
use the same code for extensionalization in Metis and Sledgehammer and generalize that code so that it gracefully handles negations (e.g. negated conjecture), formulas of the form (%x. t) = u, etc.
blanchet
parents:
42742
diff
changeset

447 
> extensionalize_term ctxt 
42750
c8b1d9ee3758
ensure Set.member isn't introduced by Meson's preprocessing if it's supposed to be unfolded
blanchet
parents:
42747
diff
changeset

448 
> presimp ? presimplify_term ctxt 
38282
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

449 
> perhaps (try (HOLogic.dest_Trueprop)) 
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

450 
> introduce_combinators_in_term ctxt kind 
38613
4ca2cae2653f
use "hypothesis" rather than "conjecture" for hypotheses in TPTP format;
blanchet
parents:
38610
diff
changeset

451 
> kind <> Axiom ? freeze_term 
42562  452 
val (combformula, atomic_types) = 
453 
combformula_from_prop thy eq_as_iff t [] 

38282
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

454 
in 
42640
879d2d6b05ce
generate tags for simps, intros, and elims in TPTP poblems on demand
blanchet
parents:
42613
diff
changeset

455 
{name = name, locality = loc, kind = kind, combformula = combformula, 
42562  456 
atomic_types = atomic_types} 
38282
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

457 
end 
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

458 

42640
879d2d6b05ce
generate tags for simps, intros, and elims in TPTP poblems on demand
blanchet
parents:
42613
diff
changeset

459 
fun make_fact ctxt keep_trivial eq_as_iff presimp ((name, loc), t) = 
879d2d6b05ce
generate tags for simps, intros, and elims in TPTP poblems on demand
blanchet
parents:
42613
diff
changeset

460 
case (keep_trivial, make_formula ctxt eq_as_iff presimp name loc Axiom t) of 
41990
7f2793d51efc
add option to function to keep trivial ATP formulas, needed for some experiments
blanchet
parents:
41770
diff
changeset

461 
(false, {combformula = AAtom (CombConst (("c_True", _), _, _)), ...}) => 
7f2793d51efc
add option to function to keep trivial ATP formulas, needed for some experiments
blanchet
parents:
41770
diff
changeset

462 
NONE 
7f2793d51efc
add option to function to keep trivial ATP formulas, needed for some experiments
blanchet
parents:
41770
diff
changeset

463 
 (_, formula) => SOME formula 
42561
23ddc4e3d19c
have properly typeinstantiated helper facts (combinators and If)
blanchet
parents:
42560
diff
changeset

464 

42709
e7af132d48fe
allow each prover to specify its own formula kind for symbols occurring in the conjecture
blanchet
parents:
42701
diff
changeset

465 
fun make_conjecture ctxt prem_kind ts = 
38613
4ca2cae2653f
use "hypothesis" rather than "conjecture" for hypotheses in TPTP format;
blanchet
parents:
38610
diff
changeset

466 
let val last = length ts  1 in 
42709
e7af132d48fe
allow each prover to specify its own formula kind for symbols occurring in the conjecture
blanchet
parents:
42701
diff
changeset

467 
map2 (fn j => fn t => 
e7af132d48fe
allow each prover to specify its own formula kind for symbols occurring in the conjecture
blanchet
parents:
42701
diff
changeset

468 
let 
e7af132d48fe
allow each prover to specify its own formula kind for symbols occurring in the conjecture
blanchet
parents:
42701
diff
changeset

469 
val (kind, maybe_negate) = 
e7af132d48fe
allow each prover to specify its own formula kind for symbols occurring in the conjecture
blanchet
parents:
42701
diff
changeset

470 
if j = last then 
e7af132d48fe
allow each prover to specify its own formula kind for symbols occurring in the conjecture
blanchet
parents:
42701
diff
changeset

471 
(Conjecture, I) 
e7af132d48fe
allow each prover to specify its own formula kind for symbols occurring in the conjecture
blanchet
parents:
42701
diff
changeset

472 
else 
e7af132d48fe
allow each prover to specify its own formula kind for symbols occurring in the conjecture
blanchet
parents:
42701
diff
changeset

473 
(prem_kind, 
e7af132d48fe
allow each prover to specify its own formula kind for symbols occurring in the conjecture
blanchet
parents:
42701
diff
changeset

474 
if prem_kind = Conjecture then update_combformula mk_anot 
e7af132d48fe
allow each prover to specify its own formula kind for symbols occurring in the conjecture
blanchet
parents:
42701
diff
changeset

475 
else I) 
e7af132d48fe
allow each prover to specify its own formula kind for symbols occurring in the conjecture
blanchet
parents:
42701
diff
changeset

476 
in 
e7af132d48fe
allow each prover to specify its own formula kind for symbols occurring in the conjecture
blanchet
parents:
42701
diff
changeset

477 
make_formula ctxt true true (string_of_int j) Chained kind t 
e7af132d48fe
allow each prover to specify its own formula kind for symbols occurring in the conjecture
blanchet
parents:
42701
diff
changeset

478 
> maybe_negate 
e7af132d48fe
allow each prover to specify its own formula kind for symbols occurring in the conjecture
blanchet
parents:
42701
diff
changeset

479 
end) 
38613
4ca2cae2653f
use "hypothesis" rather than "conjecture" for hypotheses in TPTP format;
blanchet
parents:
38610
diff
changeset

480 
(0 upto last) ts 
4ca2cae2653f
use "hypothesis" rather than "conjecture" for hypotheses in TPTP format;
blanchet
parents:
38610
diff
changeset

481 
end 
38282
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

482 

42682
562046fd8e0c
added type homogenization, whereby all (isomorphic) infinite types are mapped to the same type (to reduce the number of different predicates/TFFtypes)
blanchet
parents:
42680
diff
changeset

483 
(** Finite and infinite type inference **) 
562046fd8e0c
added type homogenization, whereby all (isomorphic) infinite types are mapped to the same type (to reduce the number of different predicates/TFFtypes)
blanchet
parents:
42680
diff
changeset

484 

562046fd8e0c
added type homogenization, whereby all (isomorphic) infinite types are mapped to the same type (to reduce the number of different predicates/TFFtypes)
blanchet
parents:
42680
diff
changeset

485 
(* Finite types such as "unit", "bool", "bool * bool", and "bool => bool" are 
562046fd8e0c
added type homogenization, whereby all (isomorphic) infinite types are mapped to the same type (to reduce the number of different predicates/TFFtypes)
blanchet
parents:
42680
diff
changeset

486 
dangerous because their "exhaust" properties can easily lead to unsound ATP 
562046fd8e0c
added type homogenization, whereby all (isomorphic) infinite types are mapped to the same type (to reduce the number of different predicates/TFFtypes)
blanchet
parents:
42680
diff
changeset

487 
proofs. On the other hand, all HOL infinite types can be given the same 
562046fd8e0c
added type homogenization, whereby all (isomorphic) infinite types are mapped to the same type (to reduce the number of different predicates/TFFtypes)
blanchet
parents:
42680
diff
changeset

488 
models in firstorder logic (via LÃ¶wenheimSkolem). *) 
562046fd8e0c
added type homogenization, whereby all (isomorphic) infinite types are mapped to the same type (to reduce the number of different predicates/TFFtypes)
blanchet
parents:
42680
diff
changeset

489 

562046fd8e0c
added type homogenization, whereby all (isomorphic) infinite types are mapped to the same type (to reduce the number of different predicates/TFFtypes)
blanchet
parents:
42680
diff
changeset

490 
fun should_encode_type _ _ All_Types _ = true 
562046fd8e0c
added type homogenization, whereby all (isomorphic) infinite types are mapped to the same type (to reduce the number of different predicates/TFFtypes)
blanchet
parents:
42680
diff
changeset

491 
 should_encode_type ctxt _ Finite_Types T = is_type_surely_finite ctxt T 
562046fd8e0c
added type homogenization, whereby all (isomorphic) infinite types are mapped to the same type (to reduce the number of different predicates/TFFtypes)
blanchet
parents:
42680
diff
changeset

492 
 should_encode_type _ nonmono_Ts Nonmonotonic_Types T = 
562046fd8e0c
added type homogenization, whereby all (isomorphic) infinite types are mapped to the same type (to reduce the number of different predicates/TFFtypes)
blanchet
parents:
42680
diff
changeset

493 
exists (curry Type.raw_instance T) nonmono_Ts 
562046fd8e0c
added type homogenization, whereby all (isomorphic) infinite types are mapped to the same type (to reduce the number of different predicates/TFFtypes)
blanchet
parents:
42680
diff
changeset

494 
 should_encode_type _ _ _ _ = false 
562046fd8e0c
added type homogenization, whereby all (isomorphic) infinite types are mapped to the same type (to reduce the number of different predicates/TFFtypes)
blanchet
parents:
42680
diff
changeset

495 

562046fd8e0c
added type homogenization, whereby all (isomorphic) infinite types are mapped to the same type (to reduce the number of different predicates/TFFtypes)
blanchet
parents:
42680
diff
changeset

496 
fun should_predicate_on_type ctxt nonmono_Ts (Preds (_, level)) T = 
562046fd8e0c
added type homogenization, whereby all (isomorphic) infinite types are mapped to the same type (to reduce the number of different predicates/TFFtypes)
blanchet
parents:
42680
diff
changeset

497 
should_encode_type ctxt nonmono_Ts level T 
562046fd8e0c
added type homogenization, whereby all (isomorphic) infinite types are mapped to the same type (to reduce the number of different predicates/TFFtypes)
blanchet
parents:
42680
diff
changeset

498 
 should_predicate_on_type _ _ _ _ = false 
562046fd8e0c
added type homogenization, whereby all (isomorphic) infinite types are mapped to the same type (to reduce the number of different predicates/TFFtypes)
blanchet
parents:
42680
diff
changeset

499 

562046fd8e0c
added type homogenization, whereby all (isomorphic) infinite types are mapped to the same type (to reduce the number of different predicates/TFFtypes)
blanchet
parents:
42680
diff
changeset

500 
fun should_tag_with_type ctxt nonmono_Ts (Tags (_, level)) T = 
562046fd8e0c
added type homogenization, whereby all (isomorphic) infinite types are mapped to the same type (to reduce the number of different predicates/TFFtypes)
blanchet
parents:
42680
diff
changeset

501 
should_encode_type ctxt nonmono_Ts level T 
562046fd8e0c
added type homogenization, whereby all (isomorphic) infinite types are mapped to the same type (to reduce the number of different predicates/TFFtypes)
blanchet
parents:
42680
diff
changeset

502 
 should_tag_with_type _ _ _ _ = false 
562046fd8e0c
added type homogenization, whereby all (isomorphic) infinite types are mapped to the same type (to reduce the number of different predicates/TFFtypes)
blanchet
parents:
42680
diff
changeset

503 

562046fd8e0c
added type homogenization, whereby all (isomorphic) infinite types are mapped to the same type (to reduce the number of different predicates/TFFtypes)
blanchet
parents:
42680
diff
changeset

504 
val homo_infinite_T = @{typ ind} (* any infinite type *) 
562046fd8e0c
added type homogenization, whereby all (isomorphic) infinite types are mapped to the same type (to reduce the number of different predicates/TFFtypes)
blanchet
parents:
42680
diff
changeset

505 

562046fd8e0c
added type homogenization, whereby all (isomorphic) infinite types are mapped to the same type (to reduce the number of different predicates/TFFtypes)
blanchet
parents:
42680
diff
changeset

506 
fun homogenized_type ctxt nonmono_Ts level T = 
562046fd8e0c
added type homogenization, whereby all (isomorphic) infinite types are mapped to the same type (to reduce the number of different predicates/TFFtypes)
blanchet
parents:
42680
diff
changeset

507 
if should_encode_type ctxt nonmono_Ts level T then T else homo_infinite_T 
562046fd8e0c
added type homogenization, whereby all (isomorphic) infinite types are mapped to the same type (to reduce the number of different predicates/TFFtypes)
blanchet
parents:
42680
diff
changeset

508 

42573
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

509 
(** "hBOOL" and "hAPP" **) 
41313
a96ac4d180b7
optionally supply constant weights to E  turned off by default until properly parameterized
blanchet
parents:
41211
diff
changeset

510 

42574  511 
type sym_info = 
42563  512 
{pred_sym : bool, min_ary : int, max_ary : int, typ : typ option} 
513 

42574  514 
fun add_combterm_syms_to_table explicit_apply = 
42558
3d9930cb6770
cleaned up "explicit_apply" so that it shares most of its code path with the default mode of operation
blanchet
parents:
42557
diff
changeset

515 
let 
3d9930cb6770
cleaned up "explicit_apply" so that it shares most of its code path with the default mode of operation
blanchet
parents:
42557
diff
changeset

516 
fun aux top_level tm = 
3d9930cb6770
cleaned up "explicit_apply" so that it shares most of its code path with the default mode of operation
blanchet
parents:
42557
diff
changeset

517 
let val (head, args) = strip_combterm_comb tm in 
3d9930cb6770
cleaned up "explicit_apply" so that it shares most of its code path with the default mode of operation
blanchet
parents:
42557
diff
changeset

518 
(case head of 
42563  519 
CombConst ((s, _), T, _) => 
42558
3d9930cb6770
cleaned up "explicit_apply" so that it shares most of its code path with the default mode of operation
blanchet
parents:
42557
diff
changeset

520 
if String.isPrefix bound_var_prefix s then 
3d9930cb6770
cleaned up "explicit_apply" so that it shares most of its code path with the default mode of operation
blanchet
parents:
42557
diff
changeset

521 
I 
3d9930cb6770
cleaned up "explicit_apply" so that it shares most of its code path with the default mode of operation
blanchet
parents:
42557
diff
changeset

522 
else 
42563  523 
let val ary = length args in 
42558
3d9930cb6770
cleaned up "explicit_apply" so that it shares most of its code path with the default mode of operation
blanchet
parents:
42557
diff
changeset

524 
Symtab.map_default 
3d9930cb6770
cleaned up "explicit_apply" so that it shares most of its code path with the default mode of operation
blanchet
parents:
42557
diff
changeset

525 
(s, {pred_sym = true, 
42563  526 
min_ary = if explicit_apply then 0 else ary, 
527 
max_ary = 0, typ = SOME T}) 

528 
(fn {pred_sym, min_ary, max_ary, typ} => 

42558
3d9930cb6770
cleaned up "explicit_apply" so that it shares most of its code path with the default mode of operation
blanchet
parents:
42557
diff
changeset

529 
{pred_sym = pred_sym andalso top_level, 
42563  530 
min_ary = Int.min (ary, min_ary), 
531 
max_ary = Int.max (ary, max_ary), 

532 
typ = if typ = SOME T then typ else NONE}) 

42558
3d9930cb6770
cleaned up "explicit_apply" so that it shares most of its code path with the default mode of operation
blanchet
parents:
42557
diff
changeset

533 
end 
3d9930cb6770
cleaned up "explicit_apply" so that it shares most of its code path with the default mode of operation
blanchet
parents:
42557
diff
changeset

534 
 _ => I) 
3d9930cb6770
cleaned up "explicit_apply" so that it shares most of its code path with the default mode of operation
blanchet
parents:
42557
diff
changeset

535 
#> fold (aux false) args 
3d9930cb6770
cleaned up "explicit_apply" so that it shares most of its code path with the default mode of operation
blanchet
parents:
42557
diff
changeset

536 
end 
3d9930cb6770
cleaned up "explicit_apply" so that it shares most of its code path with the default mode of operation
blanchet
parents:
42557
diff
changeset

537 
in aux true end 
42674  538 
fun add_fact_syms_to_table explicit_apply = 
42680  539 
fact_lift (formula_fold true (K (add_combterm_syms_to_table explicit_apply))) 
38282
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

540 

42675  541 
val default_sym_table_entries : (string * sym_info) list = 
42563  542 
[("equal", {pred_sym = true, min_ary = 2, max_ary = 2, typ = NONE}), 
42568
7b9801a34836
no needless "fequal" proxies if "explicit_apply" is set + always have readable names
blanchet
parents:
42566
diff
changeset

543 
(make_fixed_const predicator_base, 
42563  544 
{pred_sym = true, min_ary = 1, max_ary = 1, typ = NONE})] @ 
42568
7b9801a34836
no needless "fequal" proxies if "explicit_apply" is set + always have readable names
blanchet
parents:
42566
diff
changeset

545 
([tptp_false, tptp_true] 
42563  546 
> map (rpair {pred_sym = true, min_ary = 0, max_ary = 0, typ = NONE})) 
41140
9c68004b8c9d
added Sledgehammer support for higherorder propositional reasoning
blanchet
parents:
41138
diff
changeset

547 

42544
75cb06eee990
reimplemented the hAPP introduction code so that it's done earlier, when the types are still available
blanchet
parents:
42543
diff
changeset

548 
fun sym_table_for_facts explicit_apply facts = 
42568
7b9801a34836
no needless "fequal" proxies if "explicit_apply" is set + always have readable names
blanchet
parents:
42566
diff
changeset

549 
Symtab.empty > fold Symtab.default default_sym_table_entries 
42574  550 
> fold (add_fact_syms_to_table explicit_apply) facts 
38282
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

551 

42558
3d9930cb6770
cleaned up "explicit_apply" so that it shares most of its code path with the default mode of operation
blanchet
parents:
42557
diff
changeset

552 
fun min_arity_of sym_tab s = 
3d9930cb6770
cleaned up "explicit_apply" so that it shares most of its code path with the default mode of operation
blanchet
parents:
42557
diff
changeset

553 
case Symtab.lookup sym_tab s of 
42574  554 
SOME ({min_ary, ...} : sym_info) => min_ary 
42558
3d9930cb6770
cleaned up "explicit_apply" so that it shares most of its code path with the default mode of operation
blanchet
parents:
42557
diff
changeset

555 
 NONE => 
3d9930cb6770
cleaned up "explicit_apply" so that it shares most of its code path with the default mode of operation
blanchet
parents:
42557
diff
changeset

556 
case strip_prefix_and_unascii const_prefix s of 
42547
b5eec0c99528
fixed arity of special constants if "explicit_apply" is set
blanchet
parents:
42546
diff
changeset

557 
SOME s => 
42570
77f94ac04f32
cleanup proxification/unproxification and make sure that "num_atp_type_args" is called on the proxy in the reconstruction code, since "c_fequal" has one type arg but the unproxified equal has 0
blanchet
parents:
42569
diff
changeset

558 
let val s = s > unmangled_const_name > invert_const in 
42568
7b9801a34836
no needless "fequal" proxies if "explicit_apply" is set + always have readable names
blanchet
parents:
42566
diff
changeset

559 
if s = predicator_base then 1 
42547
b5eec0c99528
fixed arity of special constants if "explicit_apply" is set
blanchet
parents:
42546
diff
changeset

560 
else if s = explicit_app_base then 2 
b5eec0c99528
fixed arity of special constants if "explicit_apply" is set
blanchet
parents:
42546
diff
changeset

561 
else if s = type_pred_base then 1 
42557
ae0deb39a254
fixed minarity computation when "explicit_apply" is specified
blanchet
parents:
42556
diff
changeset

562 
else 0 
42547
b5eec0c99528
fixed arity of special constants if "explicit_apply" is set
blanchet
parents:
42546
diff
changeset

563 
end 
42544
75cb06eee990
reimplemented the hAPP introduction code so that it's done earlier, when the types are still available
blanchet
parents:
42543
diff
changeset

564 
 NONE => 0 
38282
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

565 

319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

566 
(* True if the constant ever appears outside of the toplevel position in 
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

567 
literals, or if it appears with different arities (e.g., because of different 
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

568 
type instantiations). If false, the constant always receives all of its 
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

569 
arguments and is used as a predicate. *) 
42558
3d9930cb6770
cleaned up "explicit_apply" so that it shares most of its code path with the default mode of operation
blanchet
parents:
42557
diff
changeset

570 
fun is_pred_sym sym_tab s = 
3d9930cb6770
cleaned up "explicit_apply" so that it shares most of its code path with the default mode of operation
blanchet
parents:
42557
diff
changeset

571 
case Symtab.lookup sym_tab s of 
42574  572 
SOME ({pred_sym, min_ary, max_ary, ...} : sym_info) => 
573 
pred_sym andalso min_ary = max_ary 

42558
3d9930cb6770
cleaned up "explicit_apply" so that it shares most of its code path with the default mode of operation
blanchet
parents:
42557
diff
changeset

574 
 NONE => false 
38282
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

575 

42568
7b9801a34836
no needless "fequal" proxies if "explicit_apply" is set + always have readable names
blanchet
parents:
42566
diff
changeset

576 
val predicator_combconst = 
7b9801a34836
no needless "fequal" proxies if "explicit_apply" is set + always have readable names
blanchet
parents:
42566
diff
changeset

577 
CombConst (`make_fixed_const predicator_base, @{typ "bool => bool"}, []) 
7b9801a34836
no needless "fequal" proxies if "explicit_apply" is set + always have readable names
blanchet
parents:
42566
diff
changeset

578 
fun predicator tm = CombApp (predicator_combconst, tm) 
42542
024920b65ce2
perform constant mangling and/or removal of its type args in an earlier phase, so that the rest of the code doesn't need to worry about it
blanchet
parents:
42541
diff
changeset

579 

42568
7b9801a34836
no needless "fequal" proxies if "explicit_apply" is set + always have readable names
blanchet
parents:
42566
diff
changeset

580 
fun introduce_predicators_in_combterm sym_tab tm = 
42542
024920b65ce2
perform constant mangling and/or removal of its type args in an earlier phase, so that the rest of the code doesn't need to worry about it
blanchet
parents:
42541
diff
changeset

581 
case strip_combterm_comb tm of 
024920b65ce2
perform constant mangling and/or removal of its type args in an earlier phase, so that the rest of the code doesn't need to worry about it
blanchet
parents:
42541
diff
changeset

582 
(CombConst ((s, _), _, _), _) => 
42568
7b9801a34836
no needless "fequal" proxies if "explicit_apply" is set + always have readable names
blanchet
parents:
42566
diff
changeset

583 
if is_pred_sym sym_tab s then tm else predicator tm 
7b9801a34836
no needless "fequal" proxies if "explicit_apply" is set + always have readable names
blanchet
parents:
42566
diff
changeset

584 
 _ => predicator tm 
42542
024920b65ce2
perform constant mangling and/or removal of its type args in an earlier phase, so that the rest of the code doesn't need to worry about it
blanchet
parents:
42541
diff
changeset

585 

42544
75cb06eee990
reimplemented the hAPP introduction code so that it's done earlier, when the types are still available
blanchet
parents:
42543
diff
changeset

586 
fun list_app head args = fold (curry (CombApp o swap)) args head 
75cb06eee990
reimplemented the hAPP introduction code so that it's done earlier, when the types are still available
blanchet
parents:
42543
diff
changeset

587 

75cb06eee990
reimplemented the hAPP introduction code so that it's done earlier, when the types are still available
blanchet
parents:
42543
diff
changeset

588 
fun explicit_app arg head = 
75cb06eee990
reimplemented the hAPP introduction code so that it's done earlier, when the types are still available
blanchet
parents:
42543
diff
changeset

589 
let 
42562  590 
val head_T = combtyp_of head 
42693
3c2baf9b3c61
reverted 6efda6167e5d because unsound  Vampire found a counterexample
blanchet
parents:
42691
diff
changeset

591 
val (arg_T, res_T) = dest_funT head_T 
42544
75cb06eee990
reimplemented the hAPP introduction code so that it's done earlier, when the types are still available
blanchet
parents:
42543
diff
changeset

592 
val explicit_app = 
42562  593 
CombConst (`make_fixed_const explicit_app_base, head_T > head_T, 
42693
3c2baf9b3c61
reverted 6efda6167e5d because unsound  Vampire found a counterexample
blanchet
parents:
42691
diff
changeset

594 
[arg_T, res_T]) 
42544
75cb06eee990
reimplemented the hAPP introduction code so that it's done earlier, when the types are still available
blanchet
parents:
42543
diff
changeset

595 
in list_app explicit_app [head, arg] end 
75cb06eee990
reimplemented the hAPP introduction code so that it's done earlier, when the types are still available
blanchet
parents:
42543
diff
changeset

596 
fun list_explicit_app head args = fold explicit_app args head 
38282
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

597 

42565
93f58e6a6f3e
proper handling of partially applied proxy symbols
blanchet
parents:
42564
diff
changeset

598 
fun introduce_explicit_apps_in_combterm sym_tab = 
42544
75cb06eee990
reimplemented the hAPP introduction code so that it's done earlier, when the types are still available
blanchet
parents:
42543
diff
changeset

599 
let 
75cb06eee990
reimplemented the hAPP introduction code so that it's done earlier, when the types are still available
blanchet
parents:
42543
diff
changeset

600 
fun aux tm = 
75cb06eee990
reimplemented the hAPP introduction code so that it's done earlier, when the types are still available
blanchet
parents:
42543
diff
changeset

601 
case strip_combterm_comb tm of 
75cb06eee990
reimplemented the hAPP introduction code so that it's done earlier, when the types are still available
blanchet
parents:
42543
diff
changeset

602 
(head as CombConst ((s, _), _, _), args) => 
75cb06eee990
reimplemented the hAPP introduction code so that it's done earlier, when the types are still available
blanchet
parents:
42543
diff
changeset

603 
args > map aux 
42557
ae0deb39a254
fixed minarity computation when "explicit_apply" is specified
blanchet
parents:
42556
diff
changeset

604 
> chop (min_arity_of sym_tab s) 
42544
75cb06eee990
reimplemented the hAPP introduction code so that it's done earlier, when the types are still available
blanchet
parents:
42543
diff
changeset

605 
>> list_app head 
75cb06eee990
reimplemented the hAPP introduction code so that it's done earlier, when the types are still available
blanchet
parents:
42543
diff
changeset

606 
> list_explicit_app 
75cb06eee990
reimplemented the hAPP introduction code so that it's done earlier, when the types are still available
blanchet
parents:
42543
diff
changeset

607 
 (head, args) => list_explicit_app head (map aux args) 
75cb06eee990
reimplemented the hAPP introduction code so that it's done earlier, when the types are still available
blanchet
parents:
42543
diff
changeset

608 
in aux end 
38282
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

609 

42753
c9552e617acc
drop some type arguments to constants in unsound type systems + remove a few type systems that make no sense from the circulation
blanchet
parents:
42750
diff
changeset

610 
fun chop_fun 0 T = ([], T) 
c9552e617acc
drop some type arguments to constants in unsound type systems + remove a few type systems that make no sense from the circulation
blanchet
parents:
42750
diff
changeset

611 
 chop_fun n (Type (@{type_name fun}, [dom_T, ran_T])) = 
c9552e617acc
drop some type arguments to constants in unsound type systems + remove a few type systems that make no sense from the circulation
blanchet
parents:
42750
diff
changeset

612 
chop_fun (n  1) ran_T >> cons dom_T 
c9552e617acc
drop some type arguments to constants in unsound type systems + remove a few type systems that make no sense from the circulation
blanchet
parents:
42750
diff
changeset

613 
 chop_fun _ _ = raise Fail "unexpected nonfunction" 
c9552e617acc
drop some type arguments to constants in unsound type systems + remove a few type systems that make no sense from the circulation
blanchet
parents:
42750
diff
changeset

614 

c9552e617acc
drop some type arguments to constants in unsound type systems + remove a few type systems that make no sense from the circulation
blanchet
parents:
42750
diff
changeset

615 
fun filter_type_args thy s arity T_args = 
42573
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

616 
let 
42753
c9552e617acc
drop some type arguments to constants in unsound type systems + remove a few type systems that make no sense from the circulation
blanchet
parents:
42750
diff
changeset

617 
val U = s > Sign.the_const_type thy (* may throw "TYPE" *) 
c9552e617acc
drop some type arguments to constants in unsound type systems + remove a few type systems that make no sense from the circulation
blanchet
parents:
42750
diff
changeset

618 
val res_U = U > chop_fun arity > snd 
c9552e617acc
drop some type arguments to constants in unsound type systems + remove a few type systems that make no sense from the circulation
blanchet
parents:
42750
diff
changeset

619 
val res_U_vars = Term.add_tvarsT res_U [] 
c9552e617acc
drop some type arguments to constants in unsound type systems + remove a few type systems that make no sense from the circulation
blanchet
parents:
42750
diff
changeset

620 
val U_args = (s, U) > Sign.const_typargs thy 
c9552e617acc
drop some type arguments to constants in unsound type systems + remove a few type systems that make no sense from the circulation
blanchet
parents:
42750
diff
changeset

621 
in 
c9552e617acc
drop some type arguments to constants in unsound type systems + remove a few type systems that make no sense from the circulation
blanchet
parents:
42750
diff
changeset

622 
U_args ~~ T_args 
c9552e617acc
drop some type arguments to constants in unsound type systems + remove a few type systems that make no sense from the circulation
blanchet
parents:
42750
diff
changeset

623 
> map_filter (fn (U, T) => 
c9552e617acc
drop some type arguments to constants in unsound type systems + remove a few type systems that make no sense from the circulation
blanchet
parents:
42750
diff
changeset

624 
if member (op =) res_U_vars (dest_TVar U) then SOME T 
c9552e617acc
drop some type arguments to constants in unsound type systems + remove a few type systems that make no sense from the circulation
blanchet
parents:
42750
diff
changeset

625 
else NONE) 
c9552e617acc
drop some type arguments to constants in unsound type systems + remove a few type systems that make no sense from the circulation
blanchet
parents:
42750
diff
changeset

626 
end 
c9552e617acc
drop some type arguments to constants in unsound type systems + remove a few type systems that make no sense from the circulation
blanchet
parents:
42750
diff
changeset

627 
handle TYPE _ => T_args 
c9552e617acc
drop some type arguments to constants in unsound type systems + remove a few type systems that make no sense from the circulation
blanchet
parents:
42750
diff
changeset

628 

c9552e617acc
drop some type arguments to constants in unsound type systems + remove a few type systems that make no sense from the circulation
blanchet
parents:
42750
diff
changeset

629 
fun enforce_type_arg_policy_in_combterm ctxt nonmono_Ts type_sys = 
c9552e617acc
drop some type arguments to constants in unsound type systems + remove a few type systems that make no sense from the circulation
blanchet
parents:
42750
diff
changeset

630 
let 
c9552e617acc
drop some type arguments to constants in unsound type systems + remove a few type systems that make no sense from the circulation
blanchet
parents:
42750
diff
changeset

631 
val thy = Proof_Context.theory_of ctxt 
c9552e617acc
drop some type arguments to constants in unsound type systems + remove a few type systems that make no sense from the circulation
blanchet
parents:
42750
diff
changeset

632 
fun aux arity (CombApp (tm1, tm2)) = 
c9552e617acc
drop some type arguments to constants in unsound type systems + remove a few type systems that make no sense from the circulation
blanchet
parents:
42750
diff
changeset

633 
CombApp (aux (arity + 1) tm1, aux 0 tm2) 
c9552e617acc
drop some type arguments to constants in unsound type systems + remove a few type systems that make no sense from the circulation
blanchet
parents:
42750
diff
changeset

634 
 aux arity (CombConst (name as (s, _), T, T_args)) = 
42701
500e4a88675e
reintroduce unsoundnesses taken out in 4d29b4785f43 and 3c2baf9b3c61 but only for unsound type systems
blanchet
parents:
42700
diff
changeset

635 
let 
500e4a88675e
reintroduce unsoundnesses taken out in 4d29b4785f43 and 3c2baf9b3c61 but only for unsound type systems
blanchet
parents:
42700
diff
changeset

636 
val level = level_of_type_sys type_sys 
500e4a88675e
reintroduce unsoundnesses taken out in 4d29b4785f43 and 3c2baf9b3c61 but only for unsound type systems
blanchet
parents:
42700
diff
changeset

637 
val (T, T_args) = 
500e4a88675e
reintroduce unsoundnesses taken out in 4d29b4785f43 and 3c2baf9b3c61 but only for unsound type systems
blanchet
parents:
42700
diff
changeset

638 
(* Aggressively merge most "hAPPs" if the type system is unsound 
500e4a88675e
reintroduce unsoundnesses taken out in 4d29b4785f43 and 3c2baf9b3c61 but only for unsound type systems
blanchet
parents:
42700
diff
changeset

639 
anyway, by distinguishing overloads only on the homogenized 
500e4a88675e
reintroduce unsoundnesses taken out in 4d29b4785f43 and 3c2baf9b3c61 but only for unsound type systems
blanchet
parents:
42700
diff
changeset

640 
result type. *) 
500e4a88675e
reintroduce unsoundnesses taken out in 4d29b4785f43 and 3c2baf9b3c61 but only for unsound type systems
blanchet
parents:
42700
diff
changeset

641 
if s = const_prefix ^ explicit_app_base andalso 
42726
70fc448a1815
avoid "Empty" exception by making sure that a certain optimization only is attempted when it makes sense
blanchet
parents:
42722
diff
changeset

642 
length T_args = 2 andalso 
42701
500e4a88675e
reintroduce unsoundnesses taken out in 4d29b4785f43 and 3c2baf9b3c61 but only for unsound type systems
blanchet
parents:
42700
diff
changeset

643 
not (is_type_sys_virtually_sound type_sys) then 
500e4a88675e
reintroduce unsoundnesses taken out in 4d29b4785f43 and 3c2baf9b3c61 but only for unsound type systems
blanchet
parents:
42700
diff
changeset

644 
T_args > map (homogenized_type ctxt nonmono_Ts level) 
500e4a88675e
reintroduce unsoundnesses taken out in 4d29b4785f43 and 3c2baf9b3c61 but only for unsound type systems
blanchet
parents:
42700
diff
changeset

645 
> (fn Ts => let val T = hd Ts > nth Ts 1 in 
42753
c9552e617acc
drop some type arguments to constants in unsound type systems + remove a few type systems that make no sense from the circulation
blanchet
parents:
42750
diff
changeset

646 
(T > T, tl Ts) (* ### FIXME: need tl? *) 
42701
500e4a88675e
reintroduce unsoundnesses taken out in 4d29b4785f43 and 3c2baf9b3c61 but only for unsound type systems
blanchet
parents:
42700
diff
changeset

647 
end) 
500e4a88675e
reintroduce unsoundnesses taken out in 4d29b4785f43 and 3c2baf9b3c61 but only for unsound type systems
blanchet
parents:
42700
diff
changeset

648 
else 
500e4a88675e
reintroduce unsoundnesses taken out in 4d29b4785f43 and 3c2baf9b3c61 but only for unsound type systems
blanchet
parents:
42700
diff
changeset

649 
(T, T_args) 
500e4a88675e
reintroduce unsoundnesses taken out in 4d29b4785f43 and 3c2baf9b3c61 but only for unsound type systems
blanchet
parents:
42700
diff
changeset

650 
in 
500e4a88675e
reintroduce unsoundnesses taken out in 4d29b4785f43 and 3c2baf9b3c61 but only for unsound type systems
blanchet
parents:
42700
diff
changeset

651 
(case strip_prefix_and_unascii const_prefix s of 
500e4a88675e
reintroduce unsoundnesses taken out in 4d29b4785f43 and 3c2baf9b3c61 but only for unsound type systems
blanchet
parents:
42700
diff
changeset

652 
NONE => (name, T_args) 
500e4a88675e
reintroduce unsoundnesses taken out in 4d29b4785f43 and 3c2baf9b3c61 but only for unsound type systems
blanchet
parents:
42700
diff
changeset

653 
 SOME s'' => 
42753
c9552e617acc
drop some type arguments to constants in unsound type systems + remove a few type systems that make no sense from the circulation
blanchet
parents:
42750
diff
changeset

654 
let 
c9552e617acc
drop some type arguments to constants in unsound type systems + remove a few type systems that make no sense from the circulation
blanchet
parents:
42750
diff
changeset

655 
val s'' = invert_const s'' 
c9552e617acc
drop some type arguments to constants in unsound type systems + remove a few type systems that make no sense from the circulation
blanchet
parents:
42750
diff
changeset

656 
fun filtered_T_args true = T_args 
c9552e617acc
drop some type arguments to constants in unsound type systems + remove a few type systems that make no sense from the circulation
blanchet
parents:
42750
diff
changeset

657 
 filtered_T_args false = filter_type_args thy s'' arity T_args 
c9552e617acc
drop some type arguments to constants in unsound type systems + remove a few type systems that make no sense from the circulation
blanchet
parents:
42750
diff
changeset

658 
in 
42701
500e4a88675e
reintroduce unsoundnesses taken out in 4d29b4785f43 and 3c2baf9b3c61 but only for unsound type systems
blanchet
parents:
42700
diff
changeset

659 
case type_arg_policy type_sys s'' of 
42753
c9552e617acc
drop some type arguments to constants in unsound type systems + remove a few type systems that make no sense from the circulation
blanchet
parents:
42750
diff
changeset

660 
Explicit_Type_Args keep_all => (name, filtered_T_args keep_all) 
c9552e617acc
drop some type arguments to constants in unsound type systems + remove a few type systems that make no sense from the circulation
blanchet
parents:
42750
diff
changeset

661 
 Mangled_Type_Args keep_all => 
c9552e617acc
drop some type arguments to constants in unsound type systems + remove a few type systems that make no sense from the circulation
blanchet
parents:
42750
diff
changeset

662 
(mangled_const_name (filtered_T_args keep_all) name, []) 
c9552e617acc
drop some type arguments to constants in unsound type systems + remove a few type systems that make no sense from the circulation
blanchet
parents:
42750
diff
changeset

663 
 No_Type_Args => (name, []) 
42701
500e4a88675e
reintroduce unsoundnesses taken out in 4d29b4785f43 and 3c2baf9b3c61 but only for unsound type systems
blanchet
parents:
42700
diff
changeset

664 
end) 
500e4a88675e
reintroduce unsoundnesses taken out in 4d29b4785f43 and 3c2baf9b3c61 but only for unsound type systems
blanchet
parents:
42700
diff
changeset

665 
> (fn (name, T_args) => CombConst (name, T, T_args)) 
500e4a88675e
reintroduce unsoundnesses taken out in 4d29b4785f43 and 3c2baf9b3c61 but only for unsound type systems
blanchet
parents:
42700
diff
changeset

666 
end 
42753
c9552e617acc
drop some type arguments to constants in unsound type systems + remove a few type systems that make no sense from the circulation
blanchet
parents:
42750
diff
changeset

667 
 aux _ tm = tm 
c9552e617acc
drop some type arguments to constants in unsound type systems + remove a few type systems that make no sense from the circulation
blanchet
parents:
42750
diff
changeset

668 
in aux 0 end 
42573
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

669 

42701
500e4a88675e
reintroduce unsoundnesses taken out in 4d29b4785f43 and 3c2baf9b3c61 but only for unsound type systems
blanchet
parents:
42700
diff
changeset

670 
fun repair_combterm ctxt nonmono_Ts type_sys sym_tab = 
42565
93f58e6a6f3e
proper handling of partially applied proxy symbols
blanchet
parents:
42564
diff
changeset

671 
introduce_explicit_apps_in_combterm sym_tab 
42568
7b9801a34836
no needless "fequal" proxies if "explicit_apply" is set + always have readable names
blanchet
parents:
42566
diff
changeset

672 
#> introduce_predicators_in_combterm sym_tab 
42753
c9552e617acc
drop some type arguments to constants in unsound type systems + remove a few type systems that make no sense from the circulation
blanchet
parents:
42750
diff
changeset

673 
#> enforce_type_arg_policy_in_combterm ctxt nonmono_Ts type_sys 
42701
500e4a88675e
reintroduce unsoundnesses taken out in 4d29b4785f43 and 3c2baf9b3c61 but only for unsound type systems
blanchet
parents:
42700
diff
changeset

674 
fun repair_fact ctxt nonmono_Ts type_sys sym_tab = 
500e4a88675e
reintroduce unsoundnesses taken out in 4d29b4785f43 and 3c2baf9b3c61 but only for unsound type systems
blanchet
parents:
42700
diff
changeset

675 
update_combformula (formula_map 
500e4a88675e
reintroduce unsoundnesses taken out in 4d29b4785f43 and 3c2baf9b3c61 but only for unsound type systems
blanchet
parents:
42700
diff
changeset

676 
(repair_combterm ctxt nonmono_Ts type_sys sym_tab)) 
42573
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

677 

744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

678 
(** Helper facts **) 
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

679 

744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

680 
fun ti_ti_helper_fact () = 
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

681 
let 
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

682 
fun var s = ATerm (`I s, []) 
42589
9f7c48463645
restructured type systems some more  the old naming schemes had "argshg diff less" and "tagshg diff less" as equivalent and didn't support a monomorphic version of "tags"
blanchet
parents:
42586
diff
changeset

683 
fun tag tm = ATerm (`make_fixed_const type_tag_name, [var "X", tm]) 
42573
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

684 
in 
42612  685 
Formula (helper_prefix ^ "ti_ti", Axiom, 
42573
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

686 
AAtom (ATerm (`I "equal", [tag (tag (var "Y")), tag (var "Y")])) 
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

687 
> close_formula_universally, NONE, NONE) 
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

688 
end 
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

689 

42574  690 
fun helper_facts_for_sym ctxt type_sys (s, {typ, ...} : sym_info) = 
42573
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

691 
case strip_prefix_and_unascii const_prefix s of 
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

692 
SOME mangled_s => 
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

693 
let 
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

694 
val thy = Proof_Context.theory_of ctxt 
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

695 
val unmangled_s = mangled_s > unmangled_const_name 
42579
2552c09b1a72
implement the new ATP type system in Sledgehammer
blanchet
parents:
42577
diff
changeset

696 
fun dub_and_inst c needs_some_types (th, j) = 
2552c09b1a72
implement the new ATP type system in Sledgehammer
blanchet
parents:
42577
diff
changeset

697 
((c ^ "_" ^ string_of_int j ^ (if needs_some_types then "T" else ""), 
42640
879d2d6b05ce
generate tags for simps, intros, and elims in TPTP poblems on demand
blanchet
parents:
42613
diff
changeset

698 
Chained), 
42573
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

699 
let val t = th > prop_of in 
42753
c9552e617acc
drop some type arguments to constants in unsound type systems + remove a few type systems that make no sense from the circulation
blanchet
parents:
42750
diff
changeset

700 
t > ((case general_type_arg_policy type_sys of 
c9552e617acc
drop some type arguments to constants in unsound type systems + remove a few type systems that make no sense from the circulation
blanchet
parents:
42750
diff
changeset

701 
Mangled_Type_Args _ => true 
c9552e617acc
drop some type arguments to constants in unsound type systems + remove a few type systems that make no sense from the circulation
blanchet
parents:
42750
diff
changeset

702 
 _ => false) andalso 
42573
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

703 
not (null (Term.hidden_polymorphism t))) 
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

704 
? (case typ of 
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

705 
SOME T => specialize_type thy (invert_const unmangled_s, T) 
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

706 
 NONE => I) 
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

707 
end) 
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

708 
fun make_facts eq_as_iff = 
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

709 
map_filter (make_fact ctxt false eq_as_iff false) 
42589
9f7c48463645
restructured type systems some more  the old naming schemes had "argshg diff less" and "tagshg diff less" as equivalent and didn't support a monomorphic version of "tags"
blanchet
parents:
42586
diff
changeset

710 
val has_some_types = is_type_sys_fairly_sound type_sys 
42573
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

711 
in 
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

712 
metis_helpers 
42579
2552c09b1a72
implement the new ATP type system in Sledgehammer
blanchet
parents:
42577
diff
changeset

713 
> maps (fn (metis_s, (needs_some_types, ths)) => 
42573
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

714 
if metis_s <> unmangled_s orelse 
42589
9f7c48463645
restructured type systems some more  the old naming schemes had "argshg diff less" and "tagshg diff less" as equivalent and didn't support a monomorphic version of "tags"
blanchet
parents:
42586
diff
changeset

715 
(needs_some_types andalso not has_some_types) then 
42573
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

716 
[] 
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

717 
else 
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

718 
ths ~~ (1 upto length ths) 
42579
2552c09b1a72
implement the new ATP type system in Sledgehammer
blanchet
parents:
42577
diff
changeset

719 
> map (dub_and_inst mangled_s needs_some_types) 
2552c09b1a72
implement the new ATP type system in Sledgehammer
blanchet
parents:
42577
diff
changeset

720 
> make_facts (not needs_some_types)) 
42573
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

721 
end 
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

722 
 NONE => [] 
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

723 
fun helper_facts_for_sym_table ctxt type_sys sym_tab = 
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

724 
Symtab.fold_rev (append o helper_facts_for_sym ctxt type_sys) sym_tab [] 
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

725 

744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

726 
fun translate_atp_fact ctxt keep_trivial = 
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

727 
`(make_fact ctxt keep_trivial true true o apsnd prop_of) 
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

728 

42709
e7af132d48fe
allow each prover to specify its own formula kind for symbols occurring in the conjecture
blanchet
parents:
42701
diff
changeset

729 
fun translate_formulas ctxt prem_kind type_sys hyp_ts concl_t rich_facts = 
42573
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

730 
let 
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

731 
val thy = Proof_Context.theory_of ctxt 
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

732 
val fact_ts = map (prop_of o snd o snd) rich_facts 
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

733 
val (facts, fact_names) = 
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

734 
rich_facts 
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

735 
> map_filter (fn (NONE, _) => NONE 
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

736 
 (SOME fact, (name, _)) => SOME (fact, name)) 
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

737 
> ListPair.unzip 
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

738 
(* Remove existing facts from the conjecture, as this can dramatically 
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

739 
boost an ATP's performance (for some reason). *) 
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

740 
val hyp_ts = hyp_ts > filter_out (member (op aconv) fact_ts) 
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

741 
val goal_t = Logic.list_implies (hyp_ts, concl_t) 
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

742 
val all_ts = goal_t :: fact_ts 
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

743 
val subs = tfree_classes_of_terms all_ts 
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

744 
val supers = tvar_classes_of_terms all_ts 
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

745 
val tycons = type_consts_of_terms thy all_ts 
42709
e7af132d48fe
allow each prover to specify its own formula kind for symbols occurring in the conjecture
blanchet
parents:
42701
diff
changeset

746 
val conjs = make_conjecture ctxt prem_kind (hyp_ts @ [concl_t]) 
42573
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

747 
val (supers', arity_clauses) = 
42589
9f7c48463645
restructured type systems some more  the old naming schemes had "argshg diff less" and "tagshg diff less" as equivalent and didn't support a monomorphic version of "tags"
blanchet
parents:
42586
diff
changeset

748 
if level_of_type_sys type_sys = No_Types then ([], []) 
42573
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

749 
else make_arity_clauses thy tycons supers 
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

750 
val class_rel_clauses = make_class_rel_clauses thy subs supers' 
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

751 
in 
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

752 
(fact_names > map single, (conjs, facts, class_rel_clauses, arity_clauses)) 
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

753 
end 
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

754 

744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

755 
fun fo_literal_from_type_literal (TyLitVar (class, name)) = 
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

756 
(true, ATerm (class, [ATerm (name, [])])) 
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

757 
 fo_literal_from_type_literal (TyLitFree (class, name)) = 
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

758 
(true, ATerm (class, [ATerm (name, [])])) 
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

759 

744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

760 
fun formula_from_fo_literal (pos, t) = AAtom t > not pos ? mk_anot 
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

761 

42701
500e4a88675e
reintroduce unsoundnesses taken out in 4d29b4785f43 and 3c2baf9b3c61 but only for unsound type systems
blanchet
parents:
42700
diff
changeset

762 
fun type_pred_combatom ctxt nonmono_Ts type_sys T tm = 
42573
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

763 
CombApp (CombConst (`make_fixed_const type_pred_base, T > @{typ bool}, [T]), 
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

764 
tm) 
42753
c9552e617acc
drop some type arguments to constants in unsound type systems + remove a few type systems that make no sense from the circulation
blanchet
parents:
42750
diff
changeset

765 
> enforce_type_arg_policy_in_combterm ctxt nonmono_Ts type_sys 
42573
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

766 
> AAtom 
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

767 

42680  768 
fun formula_from_combformula ctxt nonmono_Ts type_sys = 
42573
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

769 
let 
42589
9f7c48463645
restructured type systems some more  the old naming schemes had "argshg diff less" and "tagshg diff less" as equivalent and didn't support a monomorphic version of "tags"
blanchet
parents:
42586
diff
changeset

770 
fun tag_with_type type_sys T tm = 
9f7c48463645
restructured type systems some more  the old naming schemes had "argshg diff less" and "tagshg diff less" as equivalent and didn't support a monomorphic version of "tags"
blanchet
parents:
42586
diff
changeset

771 
CombConst (`make_fixed_const type_tag_name, T > T, [T]) 
42753
c9552e617acc
drop some type arguments to constants in unsound type systems + remove a few type systems that make no sense from the circulation
blanchet
parents:
42750
diff
changeset

772 
> enforce_type_arg_policy_in_combterm ctxt nonmono_Ts type_sys 
42589
9f7c48463645
restructured type systems some more  the old naming schemes had "argshg diff less" and "tagshg diff less" as equivalent and didn't support a monomorphic version of "tags"
blanchet
parents:
42586
diff
changeset

773 
> do_term true 
9f7c48463645
restructured type systems some more  the old naming schemes had "argshg diff less" and "tagshg diff less" as equivalent and didn't support a monomorphic version of "tags"
blanchet
parents:
42586
diff
changeset

774 
> (fn ATerm (s, tms) => ATerm (s, tms @ [tm])) 
9f7c48463645
restructured type systems some more  the old naming schemes had "argshg diff less" and "tagshg diff less" as equivalent and didn't support a monomorphic version of "tags"
blanchet
parents:
42586
diff
changeset

775 
and do_term top_level u = 
42573
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

776 
let 
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

777 
val (head, args) = strip_combterm_comb u 
42574  778 
val (x, T_args) = 
42573
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

779 
case head of 
42574  780 
CombConst (name, _, T_args) => (name, T_args) 
42573
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

781 
 CombVar (name, _) => (name, []) 
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

782 
 CombApp _ => raise Fail "impossible \"CombApp\"" 
42574  783 
val t = ATerm (x, map fo_term_from_typ T_args @ 
42573
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

784 
map (do_term false) args) 
42574  785 
val T = combtyp_of u 
42573
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

786 
in 
42680  787 
t > (if not top_level andalso 
788 
should_tag_with_type ctxt nonmono_Ts type_sys T then 

42589
9f7c48463645
restructured type systems some more  the old naming schemes had "argshg diff less" and "tagshg diff less" as equivalent and didn't support a monomorphic version of "tags"
blanchet
parents:
42586
diff
changeset

789 
tag_with_type type_sys T 
42573
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

790 
else 
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

791 
I) 
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

792 
end 
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

793 
val do_bound_type = 
42682
562046fd8e0c
added type homogenization, whereby all (isomorphic) infinite types are mapped to the same type (to reduce the number of different predicates/TFFtypes)
blanchet
parents:
42680
diff
changeset

794 
case type_sys of 
42722  795 
Simple_Types level => 
42682
562046fd8e0c
added type homogenization, whereby all (isomorphic) infinite types are mapped to the same type (to reduce the number of different predicates/TFFtypes)
blanchet
parents:
42680
diff
changeset

796 
SOME o mangled_type_name o homogenized_type ctxt nonmono_Ts level 
562046fd8e0c
added type homogenization, whereby all (isomorphic) infinite types are mapped to the same type (to reduce the number of different predicates/TFFtypes)
blanchet
parents:
42680
diff
changeset

797 
 _ => K NONE 
42573
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

798 
fun do_out_of_bound_type (s, T) = 
42680  799 
if should_predicate_on_type ctxt nonmono_Ts type_sys T then 
42701
500e4a88675e
reintroduce unsoundnesses taken out in 4d29b4785f43 and 3c2baf9b3c61 but only for unsound type systems
blanchet
parents:
42700
diff
changeset

800 
type_pred_combatom ctxt nonmono_Ts type_sys T (CombVar (s, T)) 
42573
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

801 
> do_formula > SOME 
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

802 
else 
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

803 
NONE 
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

804 
and do_formula (AQuant (q, xs, phi)) = 
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

805 
AQuant (q, xs > map (apsnd (fn NONE => NONE 
42574  806 
 SOME T => do_bound_type T)), 
42573
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

807 
(if q = AForall then mk_ahorn else fold_rev (mk_aconn AAnd)) 
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

808 
(map_filter 
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

809 
(fn (_, NONE) => NONE 
42574  810 
 (s, SOME T) => do_out_of_bound_type (s, T)) xs) 
42573
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

811 
(do_formula phi)) 
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

812 
 do_formula (AConn (c, phis)) = AConn (c, map do_formula phis) 
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

813 
 do_formula (AAtom tm) = AAtom (do_term true tm) 
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

814 
in do_formula end 
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

815 

42727
f365f5138771
ensure type class predicates are generated in symbol declarations (for "poly_preds" and similar)
blanchet
parents:
42726
diff
changeset

816 
fun bound_atomic_types type_sys Ts = 
f365f5138771
ensure type class predicates are generated in symbol declarations (for "poly_preds" and similar)
blanchet
parents:
42726
diff
changeset

817 
mk_ahorn (map (formula_from_fo_literal o fo_literal_from_type_literal) 
f365f5138771
ensure type class predicates are generated in symbol declarations (for "poly_preds" and similar)
blanchet
parents:
42726
diff
changeset

818 
(atp_type_literals_for_types type_sys Axiom Ts)) 
f365f5138771
ensure type class predicates are generated in symbol declarations (for "poly_preds" and similar)
blanchet
parents:
42726
diff
changeset

819 

42680  820 
fun formula_for_fact ctxt nonmono_Ts type_sys 
42573
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

821 
({combformula, atomic_types, ...} : translated_formula) = 
42727
f365f5138771
ensure type class predicates are generated in symbol declarations (for "poly_preds" and similar)
blanchet
parents:
42726
diff
changeset

822 
combformula 
f365f5138771
ensure type class predicates are generated in symbol declarations (for "poly_preds" and similar)
blanchet
parents:
42726
diff
changeset

823 
> close_combformula_universally 
f365f5138771
ensure type class predicates are generated in symbol declarations (for "poly_preds" and similar)
blanchet
parents:
42726
diff
changeset

824 
> formula_from_combformula ctxt nonmono_Ts type_sys 
f365f5138771
ensure type class predicates are generated in symbol declarations (for "poly_preds" and similar)
blanchet
parents:
42726
diff
changeset

825 
> bound_atomic_types type_sys atomic_types 
42573
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

826 
> close_formula_universally 
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

827 

42640
879d2d6b05ce
generate tags for simps, intros, and elims in TPTP poblems on demand
blanchet
parents:
42613
diff
changeset

828 
fun useful_isabelle_info s = SOME (ATerm ("[]", [ATerm ("isabelle_" ^ s, [])])) 
879d2d6b05ce
generate tags for simps, intros, and elims in TPTP poblems on demand
blanchet
parents:
42613
diff
changeset

829 

42573
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

830 
(* Each fact is given a unique fact number to avoid name clashes (e.g., because 
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

831 
of monomorphization). The TPTP explicitly forbids name clashes, and some of 
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

832 
the remote provers might care. *) 
42680  833 
fun formula_line_for_fact ctxt prefix nonmono_Ts type_sys 
42640
879d2d6b05ce
generate tags for simps, intros, and elims in TPTP poblems on demand
blanchet
parents:
42613
diff
changeset

834 
(j, formula as {name, locality, kind, ...}) = 
42680  835 
Formula (prefix ^ (if polymorphism_of_type_sys type_sys = Polymorphic then "" 
836 
else string_of_int j ^ "_") ^ 

42647
59142dbfa3ba
no need to generate fact numbers for polymorphic type systems  this confuses the TPTP exporter
blanchet
parents:
42646
diff
changeset

837 
ascii_of name, 
42680  838 
kind, formula_for_fact ctxt nonmono_Ts type_sys formula, NONE, 
42640
879d2d6b05ce
generate tags for simps, intros, and elims in TPTP poblems on demand
blanchet
parents:
42613
diff
changeset

839 
if generate_useful_info then 
879d2d6b05ce
generate tags for simps, intros, and elims in TPTP poblems on demand
blanchet
parents:
42613
diff
changeset

840 
case locality of 
879d2d6b05ce
generate tags for simps, intros, and elims in TPTP poblems on demand
blanchet
parents:
42613
diff
changeset

841 
Intro => useful_isabelle_info "intro" 
879d2d6b05ce
generate tags for simps, intros, and elims in TPTP poblems on demand
blanchet
parents:
42613
diff
changeset

842 
 Elim => useful_isabelle_info "elim" 
879d2d6b05ce
generate tags for simps, intros, and elims in TPTP poblems on demand
blanchet
parents:
42613
diff
changeset

843 
 Simp => useful_isabelle_info "simp" 
879d2d6b05ce
generate tags for simps, intros, and elims in TPTP poblems on demand
blanchet
parents:
42613
diff
changeset

844 
 _ => NONE 
879d2d6b05ce
generate tags for simps, intros, and elims in TPTP poblems on demand
blanchet
parents:
42613
diff
changeset

845 
else 
879d2d6b05ce
generate tags for simps, intros, and elims in TPTP poblems on demand
blanchet
parents:
42613
diff
changeset

846 
NONE) 
42573
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

847 

744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

848 
fun formula_line_for_class_rel_clause (ClassRelClause {name, subclass, 
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

849 
superclass, ...}) = 
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

850 
let val ty_arg = ATerm (`I "T", []) in 
42577
78414ec6fa4e
made the format (TFF or FOF) of the TPTP problem a global argument of the problem again and have the ATPs report which formats they support
blanchet
parents:
42576
diff
changeset

851 
Formula (class_rel_clause_prefix ^ ascii_of name, Axiom, 
42573
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

852 
AConn (AImplies, [AAtom (ATerm (subclass, [ty_arg])), 
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

853 
AAtom (ATerm (superclass, [ty_arg]))]) 
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

854 
> close_formula_universally, NONE, NONE) 
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

855 
end 
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

856 

744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

857 
fun fo_literal_from_arity_literal (TConsLit (c, t, args)) = 
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

858 
(true, ATerm (c, [ATerm (t, map (fn arg => ATerm (arg, [])) args)])) 
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

859 
 fo_literal_from_arity_literal (TVarLit (c, sort)) = 
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

860 
(false, ATerm (c, [ATerm (sort, [])])) 
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

861 

744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

862 
fun formula_line_for_arity_clause (ArityClause {name, conclLit, premLits, 
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

863 
...}) = 
42577
78414ec6fa4e
made the format (TFF or FOF) of the TPTP problem a global argument of the problem again and have the ATPs report which formats they support
blanchet
parents:
42576
diff
changeset

864 
Formula (arity_clause_prefix ^ ascii_of name, Axiom, 
42573
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

865 
mk_ahorn (map (formula_from_fo_literal o apfst not 
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

866 
o fo_literal_from_arity_literal) premLits) 
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

867 
(formula_from_fo_literal 
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

868 
(fo_literal_from_arity_literal conclLit)) 
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

869 
> close_formula_universally, NONE, NONE) 
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

870 

42680  871 
fun formula_line_for_conjecture ctxt nonmono_Ts type_sys 
42573
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

872 
({name, kind, combformula, ...} : translated_formula) = 
42577
78414ec6fa4e
made the format (TFF or FOF) of the TPTP problem a global argument of the problem again and have the ATPs report which formats they support
blanchet
parents:
42576
diff
changeset

873 
Formula (conjecture_prefix ^ name, kind, 
42680  874 
formula_from_combformula ctxt nonmono_Ts type_sys 
42573
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

875 
(close_combformula_universally combformula) 
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

876 
> close_formula_universally, NONE, NONE) 
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

877 

744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

878 
fun free_type_literals type_sys ({atomic_types, ...} : translated_formula) = 
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

879 
atomic_types > atp_type_literals_for_types type_sys Conjecture 
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

880 
> map fo_literal_from_type_literal 
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

881 

744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

882 
fun formula_line_for_free_type j lit = 
42577
78414ec6fa4e
made the format (TFF or FOF) of the TPTP problem a global argument of the problem again and have the ATPs report which formats they support
blanchet
parents:
42576
diff
changeset

883 
Formula (tfree_prefix ^ string_of_int j, Hypothesis, 
42573
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

884 
formula_from_fo_literal lit, NONE, NONE) 
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

885 
fun formula_lines_for_free_types type_sys facts = 
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

886 
let 
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

887 
val litss = map (free_type_literals type_sys) facts 
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

888 
val lits = fold (union (op =)) litss [] 
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

889 
in map2 formula_line_for_free_type (0 upto length lits  1) lits end 
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

890 

744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

891 
(** Symbol declarations **) 
42544
75cb06eee990
reimplemented the hAPP introduction code so that it's done earlier, when the types are still available
blanchet
parents:
42543
diff
changeset

892 

42677
25496cd3c199
monotonic type inference in ATP Sledgehammer problems  based on Claessen & al.'s CADE 2011 paper, Sect. 2.3.
blanchet
parents:
42675
diff
changeset

893 
fun insert_type get_T x xs = 
25496cd3c199
monotonic type inference in ATP Sledgehammer problems  based on Claessen & al.'s CADE 2011 paper, Sect. 2.3.
blanchet
parents:
42675
diff
changeset

894 
let val T = get_T x in 
25496cd3c199
monotonic type inference in ATP Sledgehammer problems  based on Claessen & al.'s CADE 2011 paper, Sect. 2.3.
blanchet
parents:
42675
diff
changeset

895 
if exists (curry Type.raw_instance T o get_T) xs then xs 
25496cd3c199
monotonic type inference in ATP Sledgehammer problems  based on Claessen & al.'s CADE 2011 paper, Sect. 2.3.
blanchet
parents:
42675
diff
changeset

896 
else x :: filter_out ((fn T' => Type.raw_instance (T', T)) o get_T) xs 
25496cd3c199
monotonic type inference in ATP Sledgehammer problems  based on Claessen & al.'s CADE 2011 paper, Sect. 2.3.
blanchet
parents:
42675
diff
changeset

897 
end 
25496cd3c199
monotonic type inference in ATP Sledgehammer problems  based on Claessen & al.'s CADE 2011 paper, Sect. 2.3.
blanchet
parents:
42675
diff
changeset

898 

42574  899 
fun should_declare_sym type_sys pred_sym s = 
42542
024920b65ce2
perform constant mangling and/or removal of its type args in an earlier phase, so that the rest of the code doesn't need to worry about it
blanchet
parents:
42541
diff
changeset

900 
not (String.isPrefix bound_var_prefix s) andalso s <> "equal" andalso 
42753
c9552e617acc
drop some type arguments to constants in unsound type systems + remove a few type systems that make no sense from the circulation
blanchet
parents:
42750
diff
changeset

901 
not (String.isPrefix tptp_special_prefix s) andalso 
42722  902 
((case type_sys of Simple_Types _ => true  _ => false) orelse not pred_sym) 
38282
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

903 

42698
ffd1ae4ff5c6
help SOS by ensuring that typing information is marked as part of the conjecture + be more precise w.r.t. typedefs in monotonicity check
blanchet
parents:
42697
diff
changeset

904 
fun sym_decl_table_for_facts type_sys repaired_sym_tab (conjs, facts) = 
42574  905 
let 
42698
ffd1ae4ff5c6
help SOS by ensuring that typing information is marked as part of the conjecture + be more precise w.r.t. typedefs in monotonicity check
blanchet
parents:
42697
diff
changeset

906 
fun add_combterm in_conj tm = 
42574  907 
let val (head, args) = strip_combterm_comb tm in 
908 
(case head of 

909 
CombConst ((s, s'), T, T_args) => 

910 
let val pred_sym = is_pred_sym repaired_sym_tab s in 

911 
if should_declare_sym type_sys pred_sym s then 

42576
a8a80a2a34be
merge symbol declarations that are typeinstances of each other  useful for type system "Args true" with monomorphization turned off
blanchet
parents:
42575
diff
changeset

912 
Symtab.map_default (s, []) 
42698
ffd1ae4ff5c6
help SOS by ensuring that typing information is marked as part of the conjecture + be more precise w.r.t. typedefs in monotonicity check
blanchet
parents:
42697
diff
changeset

913 
(insert_type #3 (s', T_args, T, pred_sym, length args, 
ffd1ae4ff5c6
help SOS by ensuring that typing information is marked as part of the conjecture + be more precise w.r.t. typedefs in monotonicity check
blanchet
parents:
42697
diff
changeset

914 
in_conj)) 
42574  915 
else 
916 
I 

917 
end 

918 
 _ => I) 

42698
ffd1ae4ff5c6
help SOS by ensuring that typing information is marked as part of the conjecture + be more precise w.r.t. typedefs in monotonicity check
blanchet
parents:
42697
diff
changeset

919 
#> fold (add_combterm in_conj) args 
42574  920 
end 
42698
ffd1ae4ff5c6
help SOS by ensuring that typing information is marked as part of the conjecture + be more precise w.r.t. typedefs in monotonicity check
blanchet
parents:
42697
diff
changeset

921 
fun add_fact in_conj = 
ffd1ae4ff5c6
help SOS by ensuring that typing information is marked as part of the conjecture + be more precise w.r.t. typedefs in monotonicity check
blanchet
parents:
42697
diff
changeset

922 
fact_lift (formula_fold true (K (add_combterm in_conj))) 
ffd1ae4ff5c6
help SOS by ensuring that typing information is marked as part of the conjecture + be more precise w.r.t. typedefs in monotonicity check
blanchet
parents:
42697
diff
changeset

923 
in 
ffd1ae4ff5c6
help SOS by ensuring that typing information is marked as part of the conjecture + be more precise w.r.t. typedefs in monotonicity check
blanchet
parents:
42697
diff
changeset

924 
Symtab.empty 
ffd1ae4ff5c6
help SOS by ensuring that typing information is marked as part of the conjecture + be more precise w.r.t. typedefs in monotonicity check
blanchet
parents:
42697
diff
changeset

925 
> is_type_sys_fairly_sound type_sys 
ffd1ae4ff5c6
help SOS by ensuring that typing information is marked as part of the conjecture + be more precise w.r.t. typedefs in monotonicity check
blanchet
parents:
42697
diff
changeset

926 
? (fold (add_fact true) conjs #> fold (add_fact false) facts) 
ffd1ae4ff5c6
help SOS by ensuring that typing information is marked as part of the conjecture + be more precise w.r.t. typedefs in monotonicity check
blanchet
parents:
42697
diff
changeset

927 
end 
42533  928 

42677
25496cd3c199
monotonic type inference in ATP Sledgehammer problems  based on Claessen & al.'s CADE 2011 paper, Sect. 2.3.
blanchet
parents:
42675
diff
changeset

929 
fun is_var_or_bound_var (CombConst ((s, _), _, _)) = 
25496cd3c199
monotonic type inference in ATP Sledgehammer problems  based on Claessen & al.'s CADE 2011 paper, Sect. 2.3.
blanchet
parents:
42675
diff
changeset

930 
String.isPrefix bound_var_prefix s 
25496cd3c199
monotonic type inference in ATP Sledgehammer problems  based on Claessen & al.'s CADE 2011 paper, Sect. 2.3.
blanchet
parents:
42675
diff
changeset

931 
 is_var_or_bound_var (CombVar _) = true 
25496cd3c199
monotonic type inference in ATP Sledgehammer problems  based on Claessen & al.'s CADE 2011 paper, Sect. 2.3.
blanchet
parents:
42675
diff
changeset

932 
 is_var_or_bound_var _ = false 
25496cd3c199
monotonic type inference in ATP Sledgehammer problems  based on Claessen & al.'s CADE 2011 paper, Sect. 2.3.
blanchet
parents:
42675
diff
changeset

933 

42685  934 
(* This inference is described in section 2.3 of Claessen et al.'s "Sorting it 
935 
out with monotonicity" paper presented at CADE 2011. *) 

42680  936 
fun add_combterm_nonmonotonic_types _ (SOME false) _ = I 
937 
 add_combterm_nonmonotonic_types ctxt _ 

938 
(CombApp (CombApp (CombConst (("equal", _), Type (_, [T, _]), _), tm1), 

939 
tm2)) = 

940 
(exists is_var_or_bound_var [tm1, tm2] andalso 

941 
not (is_type_surely_infinite ctxt T)) ? insert_type I T 

942 
 add_combterm_nonmonotonic_types _ _ _ = I 

943 
fun add_fact_nonmonotonic_types ctxt ({kind, combformula, ...} 

944 
: translated_formula) = 

945 
formula_fold (kind <> Conjecture) (add_combterm_nonmonotonic_types ctxt) 

946 
combformula 

947 
fun add_nonmonotonic_types_for_facts ctxt type_sys facts = 

948 
level_of_type_sys type_sys = Nonmonotonic_Types 

42731
2490e5e2f3f5
gracefully declare fTrue and fFalse proxies' types if the constants only appear in the helpers
blanchet
parents:
42730
diff
changeset

949 
? (fold (add_fact_nonmonotonic_types ctxt) facts 
2490e5e2f3f5
gracefully declare fTrue and fFalse proxies' types if the constants only appear in the helpers
blanchet
parents:
42730
diff
changeset

950 
(* in case helper "True_or_False" is included *) 
2490e5e2f3f5
gracefully declare fTrue and fFalse proxies' types if the constants only appear in the helpers
blanchet
parents:
42730
diff
changeset

951 
#> insert_type I @{typ bool}) 
42677
25496cd3c199
monotonic type inference in ATP Sledgehammer problems  based on Claessen & al.'s CADE 2011 paper, Sect. 2.3.
blanchet
parents:
42675
diff
changeset

952 

42753
c9552e617acc
drop some type arguments to constants in unsound type systems + remove a few type systems that make no sense from the circulation
blanchet
parents:
42750
diff
changeset

953 
fun result_type_of_decl (_, _, T, _, ary, _) = chop_fun ary T > snd 
42579
2552c09b1a72
implement the new ATP type system in Sledgehammer
blanchet
parents:
42577
diff
changeset

954 

42754
b9d7df8c51c8
make sure "simple_types_query" and "simple_types_bang" symbols are declared with the proper types
blanchet
parents:
42753
diff
changeset

955 
fun decl_line_for_sym ctxt nonmono_Ts level s (s', _, T, pred_sym, ary, _) = 
b9d7df8c51c8
make sure "simple_types_query" and "simple_types_bang" symbols are declared with the proper types
blanchet
parents:
42753
diff
changeset

956 
let 
b9d7df8c51c8
make sure "simple_types_query" and "simple_types_bang" symbols are declared with the proper types
blanchet
parents:
42753
diff
changeset

957 
val translate_type = 
b9d7df8c51c8
make sure "simple_types_query" and "simple_types_bang" symbols are declared with the proper types
blanchet
parents:
42753
diff
changeset

958 
mangled_type_name o homogenized_type ctxt nonmono_Ts level 
b9d7df8c51c8
make sure "simple_types_query" and "simple_types_bang" symbols are declared with the proper types
blanchet
parents:
42753
diff
changeset

959 
val (arg_tys, res_ty) = 
b9d7df8c51c8
make sure "simple_types_query" and "simple_types_bang" symbols are declared with the proper types
blanchet
parents:
42753
diff
changeset

960 
T > chop_fun ary >> map translate_type > translate_type 
b9d7df8c51c8
make sure "simple_types_query" and "simple_types_bang" symbols are declared with the proper types
blanchet
parents:
42753
diff
changeset

961 
in 
b9d7df8c51c8
make sure "simple_types_query" and "simple_types_bang" symbols are declared with the proper types
blanchet
parents:
42753
diff
changeset

962 
Decl (sym_decl_prefix ^ s, (s, s'), arg_tys, 
b9d7df8c51c8
make sure "simple_types_query" and "simple_types_bang" symbols are declared with the proper types
blanchet
parents:
42753
diff
changeset

963 
if pred_sym then `I tptp_tff_bool_type else res_ty) 
42579
2552c09b1a72
implement the new ATP type system in Sledgehammer
blanchet
parents:
42577
diff
changeset

964 
end 
2552c09b1a72
implement the new ATP type system in Sledgehammer
blanchet
parents:
42577
diff
changeset

965 

42592
fa2cf11d6351
beware of polymorphic types in typed translation symbol declarations  match alphaequivalent types and, more importantly, prevent unsoundnesses by generating type constraints on the arguments of a polymorphic symbols (otherwise "hAPP" can be given any result type)
blanchet
parents:
42589
diff
changeset

966 
fun is_polymorphic_type T = fold_atyps (fn TVar _ => K true  _ => I) T false 
fa2cf11d6351
beware of polymorphic types in typed translation symbol declarations  match alphaequivalent types and, more importantly, prevent unsoundnesses by generating type constraints on the arguments of a polymorphic symbols (otherwise "hAPP" can be given any result type)
blanchet
parents:
42589
diff
changeset

967 

42709
e7af132d48fe
allow each prover to specify its own formula kind for symbols occurring in the conjecture
blanchet
parents:
42701
diff
changeset

968 
fun formula_line_for_sym_decl ctxt conj_sym_kind nonmono_Ts type_sys n s j 
42698
ffd1ae4ff5c6
help SOS by ensuring that typing information is marked as part of the conjecture + be more precise w.r.t. typedefs in monotonicity check
blanchet
parents:
42697
diff
changeset

969 
(s', T_args, T, _, ary, in_conj) = 
42579
2552c09b1a72
implement the new ATP type system in Sledgehammer
blanchet
parents:
42577
diff
changeset

970 
let 
42709
e7af132d48fe
allow each prover to specify its own formula kind for symbols occurring in the conjecture
blanchet
parents:
42701
diff
changeset

971 
val (kind, maybe_negate) = 
e7af132d48fe
allow each prover to specify its own formula kind for symbols occurring in the conjecture
blanchet
parents:
42701
diff
changeset

972 
if in_conj then (conj_sym_kind, conj_sym_kind = Conjecture ? mk_anot) 
e7af132d48fe
allow each prover to specify its own formula kind for symbols occurring in the conjecture
blanchet
parents:
42701
diff
changeset

973 
else (Axiom, I) 
42753
c9552e617acc
drop some type arguments to constants in unsound type systems + remove a few type systems that make no sense from the circulation
blanchet
parents:
42750
diff
changeset

974 
val (arg_Ts, res_T) = chop_fun ary T 
42579
2552c09b1a72
implement the new ATP type system in Sledgehammer
blanchet
parents:
42577
diff
changeset

975 
val bound_names = 
2552c09b1a72
implement the new ATP type system in Sledgehammer
blanchet
parents:
42577
diff
changeset

976 
1 upto length arg_Ts > map (`I o make_bound_var o string_of_int) 
2552c09b1a72
implement the new ATP type system in Sledgehammer
blanchet
parents:
42577
diff
changeset

977 
val bound_tms = 
2552c09b1a72
implement the new ATP type system in Sledgehammer
blanchet
parents:
42577
diff
changeset

978 
bound_names ~~ arg_Ts > map (fn (name, T) => CombConst (name, T, [])) 
2552c09b1a72
implement the new ATP type system in Sledgehammer
blanchet
parents:
42577
diff
changeset

979 
val bound_Ts = 
42592
fa2cf11d6351
beware of polymorphic types in typed translation symbol declarations  match alphaequivalent types and, more importantly, prevent unsoundnesses by generating type constraints on the arguments of a polymorphic symbols (otherwise "hAPP" can be given any result type)
blanchet
parents:
42589
diff
changeset

980 
arg_Ts > map (fn T => if n > 1 orelse is_polymorphic_type T then SOME T 
fa2cf11d6351
beware of polymorphic types in typed translation symbol declarations  match alphaequivalent types and, more importantly, prevent unsoundnesses by generating type constraints on the arguments of a polymorphic symbols (otherwise "hAPP" can be given any result type)
blanchet
parents:
42589
diff
changeset

981 
else NONE) 
42579
2552c09b1a72
implement the new ATP type system in Sledgehammer
blanchet
parents:
42577
diff
changeset

982 
in 
42612  983 
Formula (sym_decl_prefix ^ s ^ 
42709
e7af132d48fe
allow each prover to specify its own formula kind for symbols occurring in the conjecture
blanchet
parents:
42701
diff
changeset

984 
(if n > 1 then "_" ^ string_of_int j else ""), kind, 
42579
2552c09b1a72
implement the new ATP type system in Sledgehammer
blanchet
parents:
42577
diff
changeset

985 
CombConst ((s, s'), T, T_args) 
2552c09b1a72
implement the new ATP type system in Sledgehammer
blanchet
parents:
42577
diff
changeset

986 
> fold (curry (CombApp o swap)) bound_tms 
42701
500e4a88675e
reintroduce unsoundnesses taken out in 4d29b4785f43 and 3c2baf9b3c61 but only for unsound type systems
blanchet
parents:
42700
diff
changeset

987 
> type_pred_combatom ctxt nonmono_Ts type_sys res_T 
42579
2552c09b1a72
implement the new ATP type system in Sledgehammer
blanchet
parents:
42577
diff
changeset

988 
> mk_aquant AForall (bound_names ~~ bound_Ts) 
42680  989 
> formula_from_combformula ctxt nonmono_Ts type_sys 
42727
f365f5138771
ensure type class predicates are generated in symbol declarations (for "poly_preds" and similar)
blanchet
parents:
42726
diff
changeset

990 
> n > 1 ? bound_atomic_types type_sys (atyps_of T) 
42709
e7af132d48fe
allow each prover to specify its own formula kind for symbols occurring in the conjecture
blanchet
parents:
42701
diff
changeset

991 
> close_formula_universally 
e7af132d48fe
allow each prover to specify its own formula kind for symbols occurring in the conjecture
blanchet
parents:
42701
diff
changeset

992 
> maybe_negate, 
42579
2552c09b1a72
implement the new ATP type system in Sledgehammer
blanchet
parents:
42577
diff
changeset

993 
NONE, NONE) 
2552c09b1a72
implement the new ATP type system in Sledgehammer
blanchet
parents:
42577
diff
changeset

994 
end 
2552c09b1a72
implement the new ATP type system in Sledgehammer
blanchet
parents:
42577
diff
changeset

995 

42709
e7af132d48fe
allow each prover to specify its own formula kind for symbols occurring in the conjecture
blanchet
parents:
42701
diff
changeset

996 
fun problem_lines_for_sym_decls ctxt conj_sym_kind nonmono_Ts type_sys 
e7af132d48fe
allow each prover to specify its own formula kind for symbols occurring in the conjecture
blanchet
parents:
42701
diff
changeset

997 
(s, decls) = 
42682
562046fd8e0c
added type homogenization, whereby all (isomorphic) infinite types are mapped to the same type (to reduce the number of different predicates/TFFtypes)
blanchet
parents:
42680
diff
changeset

998 
case type_sys of 
42754
b9d7df8c51c8
make sure "simple_types_query" and "simple_types_bang" symbols are declared with the proper types
blanchet
parents:
42753
diff
changeset

999 
Simple_Types level => map (decl_line_for_sym ctxt nonmono_Ts level s) decls 
42682
562046fd8e0c
added type homogenization, whereby all (isomorphic) infinite types are mapped to the same type (to reduce the number of different predicates/TFFtypes)
blanchet
parents:
42680
diff
changeset

1000 
 _ => 
42574  1001 
let 
42579
2552c09b1a72
implement the new ATP type system in Sledgehammer
blanchet
parents:
42577
diff
changeset

1002 
val decls = 
2552c09b1a72
implement the new ATP type system in Sledgehammer
blanchet
parents:
42577
diff
changeset

1003 
case decls of 
2552c09b1a72
implement the new ATP type system in Sledgehammer
blanchet
parents:
42577
diff
changeset

1004 
decl :: (decls' as _ :: _) => 
42592
fa2cf11d6351
beware of polymorphic types in typed translation symbol declarations  match alphaequivalent types and, more importantly, prevent unsoundnesses by generating type constraints on the arguments of a polymorphic symbols (otherwise "hAPP" can be given any result type)
blanchet
parents:
42589
diff
changeset

1005 
let val T = result_type_of_decl decl in 
fa2cf11d6351
beware of polymorphic types in typed translation symbol declarations  match alphaequivalent types and, more importantly, prevent unsoundnesses by generating type constraints on the arguments of a polymorphic symbols (otherwise "hAPP" can be given any result type)
blanchet
parents:
42589
diff
changeset

1006 
if forall ((fn T' => Type.raw_instance (T', T)) 
fa2cf11d6351
beware of polymorphic types in typed translation symbol declarations  match alphaequivalent types and, more importantly, prevent unsoundnesses by generating type constraints on the arguments of a polymorphic symbols (otherwise "hAPP" can be given any result type)
blanchet
parents:
42589
diff
changeset

1007 
o result_type_of_decl) decls' then 
fa2cf11d6351
beware of polymorphic types in typed translation symbol declarations  match alphaequivalent types and, more importantly, prevent unsoundnesses by generating type constraints on the arguments of a polymorphic symbols (otherwise "hAPP" can be given any result type)
blanchet
parents:
42589
diff
changeset

1008 
[decl] 
fa2cf11d6351
beware of polymorphic types in typed translation symbol declarations  match alphaequivalent types and, more importantly, prevent unsoundnesses by generating type constraints on the arguments of a polymorphic symbols (otherwise "hAPP" can be given any result type)
blanchet
parents:
42589
diff
changeset

1009 
else 
fa2cf11d6351
beware of polymorphic types in typed translation symbol declarations  match alphaequivalent types and, more importantly, prevent unsoundnesses by generating type constraints on the arguments of a polymorphic symbols (otherwise "hAPP" can be given any result type)
blanchet
parents:
42589
diff
changeset

1010 
decls 
fa2cf11d6351
beware of polymorphic types in typed translation symbol declarations  match alphaequivalent types and, more importantly, prevent unsoundnesses by generating type constraints on the arguments of a polymorphic symbols (otherwise "hAPP" can be given any result type)
blanchet
parents:
42589
diff
changeset

1011 
end 
42579
2552c09b1a72
implement the new ATP type system in Sledgehammer
blanchet
parents:
42577
diff
changeset

1012 
 _ => decls 
2552c09b1a72
implement the new ATP type system in Sledgehammer
blanchet
parents:
42577
diff
changeset

1013 
val n = length decls 
2552c09b1a72
implement the new ATP type system in Sledgehammer
blanchet
parents:
42577
diff
changeset

1014 
val decls = 
42680  1015 
decls > filter (should_predicate_on_type ctxt nonmono_Ts type_sys 
42579
2552c09b1a72
implement the new ATP type system in Sledgehammer
blanchet
parents:
42577
diff
changeset

1016 
o result_type_of_decl) 
42574  1017 
in 
42709
e7af132d48fe
allow each prover to specify its own formula kind for symbols occurring in the conjecture
blanchet
parents:
42701
diff
changeset

1018 
(0 upto length decls  1, decls) 
e7af132d48fe
allow each prover to specify its own formula kind for symbols occurring in the conjecture
blanchet
parents:
42701
diff
changeset

1019 
> map2 (formula_line_for_sym_decl ctxt conj_sym_kind nonmono_Ts type_sys 
e7af132d48fe
allow each prover to specify its own formula kind for symbols occurring in the conjecture
blanchet
parents:
42701
diff
changeset

1020 
n s) 
42574  1021 
end 
42579
2552c09b1a72
implement the new ATP type system in Sledgehammer
blanchet
parents:
42577
diff
changeset

1022 

42709
e7af132d48fe
allow each prover to specify its own formula kind for symbols occurring in the conjecture
blanchet
parents:
42701
diff
changeset

1023 
fun problem_lines_for_sym_decl_table ctxt conj_sym_kind nonmono_Ts type_sys 
e7af132d48fe
allow each prover to specify its own formula kind for symbols occurring in the conjecture
blanchet
parents:
42701
diff
changeset

1024 
sym_decl_tab = 
e7af132d48fe
allow each prover to specify its own formula kind for symbols occurring in the conjecture
blanchet
parents:
42701
diff
changeset

1025 
Symtab.fold_rev (append o problem_lines_for_sym_decls ctxt conj_sym_kind 
e7af132d48fe
allow each prover to specify its own formula kind for symbols occurring in the conjecture
blanchet
parents:
42701
diff
changeset

1026 
nonmono_Ts type_sys) 
42574  1027 
sym_decl_tab [] 
42543
f9d402d144d4
declare TFF types so that SNARK can be used with types
blanchet
parents:
42542
diff
changeset

1028 

f9d402d144d4
declare TFF types so that SNARK can be used with types
blanchet
parents:
42542
diff
changeset

1029 
fun add_tff_types_in_formula (AQuant (_, xs, phi)) = 
f9d402d144d4
declare TFF types so that SNARK can be used with types
blanchet
parents:
42542
diff
changeset

1030 
union (op =) (map_filter snd xs) #> add_tff_types_in_formula phi 
f9d402d144d4
declare TFF types so that SNARK can be used with types
blanchet
parents:
42542
diff
changeset

1031 
 add_tff_types_in_formula (AConn (_, phis)) = 
f9d402d144d4
declare TFF types so that SNARK can be used with types
blanchet
parents:
42542
diff
changeset

1032 
fold add_tff_types_in_formula phis 
f9d402d144d4
declare TFF types so that SNARK can be used with types
blanchet
parents:
42542
diff
changeset

1033 
 add_tff_types_in_formula (AAtom _) = I 
42539
f6ba908b8b27
generate typing for "hBOOL" in "Many_Typed" mode + tuning
blanchet
parents:
42538
diff
changeset

1034 

42562  1035 
fun add_tff_types_in_problem_line (Decl (_, _, arg_Ts, res_T)) = 
1036 
union (op =) (res_T :: arg_Ts) 

42577
78414ec6fa4e
made the format (TFF or FOF) of the TPTP problem a global argument of the problem again and have the ATPs report which formats they support
blanchet
parents:
42576
diff
changeset

1037 
 add_tff_types_in_problem_line (Formula (_, _, phi, _, _)) = 
42543
f9d402d144d4
declare TFF types so that SNARK can be used with types
blanchet
parents:
42542
diff
changeset

1038 
add_tff_types_in_formula phi 
f9d402d144d4
declare TFF types so that SNARK can be used with types
blanchet
parents:
42542
diff
changeset

1039 

f9d402d144d4
declare TFF types so that SNARK can be used with types
blanchet
parents:
42542
diff
changeset

1040 
fun tff_types_in_problem problem = 
f9d402d144d4
declare TFF types so that SNARK can be used with types
blanchet
parents:
42542
diff
changeset

1041 
fold (fold add_tff_types_in_problem_line o snd) problem [] 
f9d402d144d4
declare TFF types so that SNARK can be used with types
blanchet
parents:
42542
diff
changeset

1042 

42545  1043 
fun decl_line_for_tff_type (s, s') = 
42568
7b9801a34836
no needless "fequal" proxies if "explicit_apply" is set + always have readable names
blanchet
parents:
42566
diff
changeset

1044 
Decl (type_decl_prefix ^ ascii_of s, (s, s'), [], `I tptp_tff_type_of_types) 
42543
f9d402d144d4
declare TFF types so that SNARK can be used with types
blanchet
parents:
42542
diff
changeset

1045 

f9d402d144d4
declare TFF types so that SNARK can be used with types
blanchet
parents:
42542
diff
changeset

1046 
val type_declsN = "Types" 
42544
75cb06eee990
reimplemented the hAPP introduction code so that it's done earlier, when the types are still available
blanchet
parents:
42543
diff
changeset

1047 
val sym_declsN = "Symbol types" 
41157  1048 
val factsN = "Relevant facts" 
1049 
val class_relsN = "Class relationships" 

42543
f9d402d144d4
declare TFF types so that SNARK can be used with types
blanchet
parents:
42542
diff
changeset

1050 
val aritiesN = "Arities" 
41157  1051 
val helpersN = "Helper facts" 
1052 
val conjsN = "Conjectures" 

41313
a96ac4d180b7
optionally supply constant weights to E  turned off by default until properly parameterized
blanchet
parents:
41211
diff
changeset

1053 
val free_typesN = "Type variables" 
41157  1054 

1055 
fun offset_of_heading_in_problem _ [] j = j 

1056 
 offset_of_heading_in_problem needle ((heading, lines) :: problem) j = 

1057 
if heading = needle then j 

1058 
else offset_of_heading_in_problem needle problem (j + length lines) 
