106 fun make_tfree ctxt w = |
106 fun make_tfree ctxt w = |
107 let val ww = "'" ^ w in |
107 let val ww = "'" ^ w in |
108 TFree (ww, the_default HOLogic.typeS (Variable.def_sort ctxt (ww, ~1))) |
108 TFree (ww, the_default HOLogic.typeS (Variable.def_sort ctxt (ww, ~1))) |
109 end |
109 end |
110 |
110 |
|
111 exception ATP_CLASS of string list |
111 exception ATP_TYPE of string atp_type list |
112 exception ATP_TYPE of string atp_type list |
112 exception ATP_TERM of (string, string atp_type) atp_term list |
113 exception ATP_TERM of (string, string atp_type) atp_term list |
113 exception ATP_FORMULA of |
114 exception ATP_FORMULA of |
114 (string, string, (string, string atp_type) atp_term, string) atp_formula list |
115 (string, string, (string, string atp_type) atp_term, string) atp_formula list |
115 exception SAME of unit |
116 exception SAME of unit |
116 |
117 |
|
118 fun class_of_atp_class cls = |
|
119 (case unprefix_and_unascii class_prefix cls of |
|
120 SOME s => s |
|
121 | NONE => raise ATP_CLASS [cls]) |
|
122 |
117 (* Type variables are given the basic sort "HOL.type". Some will later be constrained by information |
123 (* Type variables are given the basic sort "HOL.type". Some will later be constrained by information |
118 from type literals, or by type inference. *) |
124 from type literals, or by type inference. *) |
119 fun typ_of_atp_type ctxt (ty as AType (a, tys)) = |
125 fun typ_of_atp_type ctxt (ty as AType ((a, clss), tys)) = |
120 let val Ts = map (typ_of_atp_type ctxt) tys in |
126 let val Ts = map (typ_of_atp_type ctxt) tys in |
121 (case unprefix_and_unascii type_const_prefix a of |
127 (case unprefix_and_unascii type_const_prefix a of |
122 SOME b => Type (invert_const b, Ts) |
128 SOME b => Type (invert_const b, Ts) |
123 | NONE => |
129 | NONE => |
124 if not (null tys) then |
130 if not (null tys) then |
128 SOME b => make_tfree ctxt b |
134 SOME b => make_tfree ctxt b |
129 | NONE => |
135 | NONE => |
130 (* The term could be an Isabelle variable or a variable from the ATP, say "X1" or "_5018". |
136 (* The term could be an Isabelle variable or a variable from the ATP, say "X1" or "_5018". |
131 Sometimes variables from the ATP are indistinguishable from Isabelle variables, which |
137 Sometimes variables from the ATP are indistinguishable from Isabelle variables, which |
132 forces us to use a type parameter in all cases. *) |
138 forces us to use a type parameter in all cases. *) |
133 Type_Infer.param 0 (a |> perhaps (unprefix_and_unascii tvar_prefix), HOLogic.typeS))) |
139 Type_Infer.param 0 (a |> perhaps (unprefix_and_unascii tvar_prefix), |
|
140 (if null clss then HOLogic.typeS |
|
141 else map class_of_atp_class clss)))) |
134 end |
142 end |
135 |
143 |
136 fun atp_type_of_atp_term (ATerm ((s, _), us)) = AType (s, map atp_type_of_atp_term us) |
144 fun atp_type_of_atp_term (ATerm ((s, _), us)) = AType ((s, []), map atp_type_of_atp_term us) |
137 |
145 |
138 fun typ_of_atp_term ctxt = typ_of_atp_type ctxt o atp_type_of_atp_term |
146 fun typ_of_atp_term ctxt = typ_of_atp_type ctxt o atp_type_of_atp_term |
139 |
147 |
140 (* Type class literal applied to a type. Returns triple of polarity, class, type. *) |
148 (* Type class literal applied to a type. Returns triple of polarity, class, type. *) |
141 fun type_constraint_of_term ctxt (u as ATerm ((a, _), us)) = |
149 fun type_constraint_of_term ctxt (u as ATerm ((a, _), us)) = |