1.1 --- a/src/HOL/Tools/ATP/atp_translate.ML Tue Jun 21 17:17:39 2011 +0200
1.2 +++ b/src/HOL/Tools/ATP/atp_translate.ML Tue Jun 21 17:17:39 2011 +0200
1.3 @@ -15,31 +15,6 @@
1.4 type formula_kind = ATP_Problem.formula_kind
1.5 type 'a problem = 'a ATP_Problem.problem
1.6
1.7 - type name = string * string
1.8 -
1.9 - datatype type_literal =
1.10 - TyLitVar of name * name |
1.11 - TyLitFree of name * name
1.12 -
1.13 - datatype arity_literal =
1.14 - TConsLit of name * name * name list |
1.15 - TVarLit of name * name
1.16 -
1.17 - type arity_clause =
1.18 - {name: string,
1.19 - prem_lits: arity_literal list,
1.20 - concl_lits: arity_literal}
1.21 -
1.22 - type class_rel_clause =
1.23 - {name: string,
1.24 - subclass: name,
1.25 - superclass: name}
1.26 -
1.27 - datatype combterm =
1.28 - CombConst of name * typ * typ list |
1.29 - CombVar of name * typ |
1.30 - CombApp of combterm * combterm
1.31 -
1.32 datatype locality =
1.33 General | Helper | Extensionality | Intro | Elim | Simp | Local | Assum |
1.34 Chained
1.35 @@ -56,13 +31,13 @@
1.36 Tags of polymorphism * type_level * type_heaviness
1.37
1.38 val bound_var_prefix : string
1.39 - val schematic_var_prefix: string
1.40 - val fixed_var_prefix: string
1.41 - val tvar_prefix: string
1.42 - val tfree_prefix: string
1.43 - val const_prefix: string
1.44 - val type_const_prefix: string
1.45 - val class_prefix: string
1.46 + val schematic_var_prefix : string
1.47 + val fixed_var_prefix : string
1.48 + val tvar_prefix : string
1.49 + val tfree_prefix : string
1.50 + val const_prefix : string
1.51 + val type_const_prefix : string
1.52 + val class_prefix : string
1.53 val skolem_const_prefix : string
1.54 val old_skolem_const_prefix : string
1.55 val new_skolem_const_prefix : string
1.56 @@ -87,34 +62,17 @@
1.57 val prefixed_predicator_name : string
1.58 val prefixed_app_op_name : string
1.59 val prefixed_type_tag_name : string
1.60 - val ascii_of: string -> string
1.61 - val unascii_of: string -> string
1.62 + val ascii_of : string -> string
1.63 + val unascii_of : string -> string
1.64 val strip_prefix_and_unascii : string -> string -> string option
1.65 val proxy_table : (string * (string * (thm * (string * string)))) list
1.66 val proxify_const : string -> (string * string) option
1.67 - val invert_const: string -> string
1.68 - val unproxify_const: string -> string
1.69 - val make_bound_var : string -> string
1.70 - val make_schematic_var : string * int -> string
1.71 - val make_fixed_var : string -> string
1.72 - val make_schematic_type_var : string * int -> string
1.73 - val make_fixed_type_var : string -> string
1.74 - val make_fixed_const : string -> string
1.75 - val make_fixed_type_const : string -> string
1.76 - val make_type_class : string -> string
1.77 + val invert_const : string -> string
1.78 + val unproxify_const : string -> string
1.79 val new_skolem_var_name_from_const : string -> string
1.80 val num_type_args : theory -> string -> int
1.81 val atp_irrelevant_consts : string list
1.82 val atp_schematic_consts_of : term -> typ list Symtab.table
1.83 - val make_arity_clauses :
1.84 - theory -> string list -> class list -> class list * arity_clause list
1.85 - val make_class_rel_clauses :
1.86 - theory -> class list -> class list -> class_rel_clause list
1.87 - val combtyp_of : combterm -> typ
1.88 - val strip_combterm_comb : combterm -> combterm * combterm list
1.89 - val atyps_of : typ -> typ list
1.90 - val combterm_from_term :
1.91 - theory -> (string * typ) list -> term -> combterm * typ list
1.92 val is_locality_global : locality -> bool
1.93 val type_sys_from_string : string -> type_sys
1.94 val polymorphism_of_type_sys : type_sys -> polymorphism
1.95 @@ -124,13 +82,9 @@
1.96 val choose_format : format list -> type_sys -> format * type_sys
1.97 val mk_aconns :
1.98 connective -> ('a, 'b, 'c) formula list -> ('a, 'b, 'c) formula
1.99 + val unmangled_const : string -> string * string fo_term list
1.100 val unmangled_const_name : string -> string
1.101 - val unmangled_const : string -> string * string fo_term list
1.102 val helper_table : ((string * bool) * thm list) list
1.103 - val should_specialize_helper : type_sys -> term -> bool
1.104 - val tfree_classes_of_terms : term list -> string list
1.105 - val tvar_classes_of_terms : term list -> string list
1.106 - val type_constrs_of_terms : theory -> term list -> string list
1.107 val prepare_atp_problem :
1.108 Proof.context -> format -> formula_kind -> formula_kind -> type_sys
1.109 -> bool -> bool -> bool -> term list -> term
1.110 @@ -237,16 +191,16 @@
1.111 fun un rcs [] = String.implode(rev rcs)
1.112 | un rcs [#"_"] = un (#"_" :: rcs) [] (* ERROR *)
1.113 (* Three types of _ escapes: __, _A to _P, _nnn *)
1.114 - | un rcs (#"_" :: #"_" :: cs) = un (#"_"::rcs) cs
1.115 + | un rcs (#"_" :: #"_" :: cs) = un (#"_" :: rcs) cs
1.116 | un rcs (#"_" :: c :: cs) =
1.117 if #"A" <= c andalso c<= #"P" then
1.118 (* translation of #" " to #"/" *)
1.119 un (Char.chr (Char.ord c - upper_a_minus_space) :: rcs) cs
1.120 else
1.121 - let val digits = List.take (c::cs, 3) handle General.Subscript => [] in
1.122 + let val digits = List.take (c :: cs, 3) handle General.Subscript => [] in
1.123 case Int.fromString (String.implode digits) of
1.124 SOME n => un (Char.chr n :: rcs) (List.drop (cs, 2))
1.125 - | NONE => un (c:: #"_"::rcs) cs (* ERROR *)
1.126 + | NONE => un (c :: #"_" :: rcs) cs (* ERROR *)
1.127 end
1.128 | un rcs (c :: cs) = un (c :: rcs) cs
1.129 in un [] o String.explode end
1.130 @@ -399,9 +353,9 @@
1.131 fold (fn s => s <> type_class ? cons (`make_type_class s, `I tvar))
1.132
1.133 type arity_clause =
1.134 - {name: string,
1.135 - prem_lits: arity_literal list,
1.136 - concl_lits: arity_literal}
1.137 + {name : string,
1.138 + prem_lits : arity_literal list,
1.139 + concl_lits : arity_literal}
1.140
1.141 (* Arity of type constructor "tcon :: (arg1, ..., argN) res" *)
1.142 fun make_axiom_arity_clause (tcons, name, (cls, args)) =
1.143 @@ -467,9 +421,9 @@
1.144 (** Isabelle class relations **)
1.145
1.146 type class_rel_clause =
1.147 - {name: string,
1.148 - subclass: name,
1.149 - superclass: name}
1.150 + {name : string,
1.151 + subclass : name,
1.152 + superclass : name}
1.153
1.154 (*Generate all pairs (sub,super) such that sub is a proper subclass of super in theory thy.*)
1.155 fun class_pairs _ [] _ = []
1.156 @@ -499,9 +453,10 @@
1.157
1.158 (*gets the head of a combinator application, along with the list of arguments*)
1.159 fun strip_combterm_comb u =
1.160 - let fun stripc (CombApp(t,u), ts) = stripc (t, u::ts)
1.161 - | stripc x = x
1.162 - in stripc(u,[]) end
1.163 + let
1.164 + fun stripc (CombApp (t, u), ts) = stripc (t, u :: ts)
1.165 + | stripc x = x
1.166 + in stripc (u, []) end
1.167
1.168 fun atyps_of T = fold_atyps (insert (op =)) T []
1.169
1.170 @@ -639,11 +594,11 @@
1.171 | format => (format, type_sys))
1.172
1.173 type translated_formula =
1.174 - {name: string,
1.175 - locality: locality,
1.176 - kind: formula_kind,
1.177 - combformula: (name, typ, combterm) formula,
1.178 - atomic_types: typ list}
1.179 + {name : string,
1.180 + locality : locality,
1.181 + kind : formula_kind,
1.182 + combformula : (name, typ, combterm) formula,
1.183 + atomic_types : typ list}
1.184
1.185 fun update_combformula f ({name, locality, kind, combformula, atomic_types}
1.186 : translated_formula) =