43 datatype polymorphism = Polymorphic | Monomorphic | Mangled_Monomorphic |
43 datatype polymorphism = Polymorphic | Monomorphic | Mangled_Monomorphic |
44 datatype type_level = |
44 datatype type_level = |
45 All_Types | Nonmonotonic_Types | Finite_Types | Const_Arg_Types | No_Types |
45 All_Types | Nonmonotonic_Types | Finite_Types | Const_Arg_Types | No_Types |
46 datatype type_heaviness = Heavy | Light |
46 datatype type_heaviness = Heavy | Light |
47 |
47 |
48 datatype type_system = |
48 datatype type_sys = |
49 Simple_Types of type_level | |
49 Simple_Types of type_level | |
50 Preds of polymorphism * type_level * type_heaviness | |
50 Preds of polymorphism * type_level * type_heaviness | |
51 Tags of polymorphism * type_level * type_heaviness |
51 Tags of polymorphism * type_level * type_heaviness |
52 |
52 |
53 type translated_formula |
53 type translated_formula |
96 val strip_combterm_comb : combterm -> combterm * combterm list |
96 val strip_combterm_comb : combterm -> combterm * combterm list |
97 val atyps_of : typ -> typ list |
97 val atyps_of : typ -> typ list |
98 val combterm_from_term : |
98 val combterm_from_term : |
99 theory -> (string * typ) list -> term -> combterm * typ list |
99 theory -> (string * typ) list -> term -> combterm * typ list |
100 val is_locality_global : locality -> bool |
100 val is_locality_global : locality -> bool |
101 val type_sys_from_string : string -> type_system |
101 val type_sys_from_string : string -> type_sys |
102 val polymorphism_of_type_sys : type_system -> polymorphism |
102 val polymorphism_of_type_sys : type_sys -> polymorphism |
103 val level_of_type_sys : type_system -> type_level |
103 val level_of_type_sys : type_sys -> type_level |
104 val is_type_sys_virtually_sound : type_system -> bool |
104 val is_type_sys_virtually_sound : type_sys -> bool |
105 val is_type_sys_fairly_sound : type_system -> bool |
105 val is_type_sys_fairly_sound : type_sys -> bool |
106 val choose_format : format list -> type_system -> format * type_system |
106 val choose_format : format list -> type_sys -> format * type_sys |
107 val raw_type_literals_for_types : typ list -> type_literal list |
107 val raw_type_literals_for_types : typ list -> type_literal list |
108 val unmangled_const : string -> string * string fo_term list |
108 val unmangled_const : string -> string * string fo_term list |
109 val translate_atp_fact : |
109 val translate_atp_fact : |
110 Proof.context -> format -> type_system -> bool -> (string * locality) * thm |
110 Proof.context -> format -> type_sys -> bool -> (string * locality) * thm |
111 -> translated_formula option * ((string * locality) * thm) |
111 -> translated_formula option * ((string * locality) * thm) |
112 val helper_table : (string * (bool * thm list)) list |
112 val helper_table : (string * (bool * thm list)) list |
113 val tfree_classes_of_terms : term list -> string list |
113 val tfree_classes_of_terms : term list -> string list |
114 val tvar_classes_of_terms : term list -> string list |
114 val tvar_classes_of_terms : term list -> string list |
115 val type_consts_of_terms : theory -> term list -> string list |
115 val type_consts_of_terms : theory -> term list -> string list |
116 val prepare_atp_problem : |
116 val prepare_atp_problem : |
117 Proof.context -> format -> formula_kind -> formula_kind -> type_system |
117 Proof.context -> format -> formula_kind -> formula_kind -> type_sys |
118 -> bool option -> bool -> bool -> term list -> term |
118 -> bool option -> bool -> bool -> term list -> term |
119 -> (translated_formula option * ((string * 'a) * thm)) list |
119 -> (translated_formula option * ((string * 'a) * thm)) list |
120 -> string problem * string Symtab.table * int * int |
120 -> string problem * string Symtab.table * int * int |
121 * (string * 'a) list vector * int list * int Symtab.table |
121 * (string * 'a) list vector * int list * int Symtab.table |
122 val atp_problem_weights : string problem -> (string * real) list |
122 val atp_problem_weights : string problem -> (string * real) list |
496 datatype polymorphism = Polymorphic | Monomorphic | Mangled_Monomorphic |
496 datatype polymorphism = Polymorphic | Monomorphic | Mangled_Monomorphic |
497 datatype type_level = |
497 datatype type_level = |
498 All_Types | Nonmonotonic_Types | Finite_Types | Const_Arg_Types | No_Types |
498 All_Types | Nonmonotonic_Types | Finite_Types | Const_Arg_Types | No_Types |
499 datatype type_heaviness = Heavy | Light |
499 datatype type_heaviness = Heavy | Light |
500 |
500 |
501 datatype type_system = |
501 datatype type_sys = |
502 Simple_Types of type_level | |
502 Simple_Types of type_level | |
503 Preds of polymorphism * type_level * type_heaviness | |
503 Preds of polymorphism * type_level * type_heaviness | |
504 Tags of polymorphism * type_level * type_heaviness |
504 Tags of polymorphism * type_level * type_heaviness |
505 |
505 |
506 fun try_unsuffixes ss s = |
506 fun try_unsuffixes ss s = |