99 val make_fixed_const : string -> string |
99 val make_fixed_const : string -> string |
100 val make_fixed_type_const : string -> string |
100 val make_fixed_type_const : string -> string |
101 val make_type_class : string -> string |
101 val make_type_class : string -> string |
102 val new_skolem_var_name_from_const : string -> string |
102 val new_skolem_var_name_from_const : string -> string |
103 val num_type_args : theory -> string -> int |
103 val num_type_args : theory -> string -> int |
|
104 val atp_irrelevant_consts : string list |
|
105 val atp_schematic_consts_of : term -> typ list Symtab.table |
104 val make_arity_clauses : |
106 val make_arity_clauses : |
105 theory -> string list -> class list -> class list * arity_clause list |
107 theory -> string list -> class list -> class list * arity_clause list |
106 val make_class_rel_clauses : |
108 val make_class_rel_clauses : |
107 theory -> class list -> class list -> class_rel_clause list |
109 theory -> class list -> class list -> class_rel_clause list |
108 val combtyp_of : combterm -> typ |
110 val combtyp_of : combterm -> typ |
348 fun num_type_args thy s = |
350 fun num_type_args thy s = |
349 if String.isPrefix skolem_const_prefix s then |
351 if String.isPrefix skolem_const_prefix s then |
350 s |> space_explode Long_Name.separator |> List.last |> Int.fromString |> the |
352 s |> space_explode Long_Name.separator |> List.last |> Int.fromString |> the |
351 else |
353 else |
352 (s, Sign.the_const_type thy s) |> Sign.const_typargs thy |> length |
354 (s, Sign.the_const_type thy s) |> Sign.const_typargs thy |> length |
|
355 |
|
356 (* These are either simplified away by "Meson.presimplify" (most of the time) or |
|
357 handled specially via "fFalse", "fTrue", ..., "fequal". *) |
|
358 val atp_irrelevant_consts = |
|
359 [@{const_name False}, @{const_name True}, @{const_name Not}, |
|
360 @{const_name conj}, @{const_name disj}, @{const_name implies}, |
|
361 @{const_name HOL.eq}, @{const_name If}, @{const_name Let}] |
|
362 |
|
363 val atp_monomorph_bad_consts = |
|
364 atp_irrelevant_consts @ |
|
365 (* These are ignored anyway by the relevance filter (unless they appear in |
|
366 higher-order places) but not by the monomorphizer. *) |
|
367 [@{const_name all}, @{const_name "==>"}, @{const_name "=="}, |
|
368 @{const_name Trueprop}, @{const_name All}, @{const_name Ex}, |
|
369 @{const_name Ex1}, @{const_name Ball}, @{const_name Bex}] |
|
370 |
|
371 val atp_schematic_consts_of = |
|
372 Monomorph.all_schematic_consts_of |
|
373 #> Symtab.map (fn s => fn Ts => |
|
374 if member (op =) atp_monomorph_bad_consts s then [] else Ts) |
353 |
375 |
354 (** Definitions and functions for FOL clauses and formulas for TPTP **) |
376 (** Definitions and functions for FOL clauses and formulas for TPTP **) |
355 |
377 |
356 (* The first component is the type class; the second is a "TVar" or "TFree". *) |
378 (* The first component is the type class; the second is a "TVar" or "TFree". *) |
357 datatype type_literal = |
379 datatype type_literal = |