197 (*Generates a constant, given its type arguments*) |
197 (*Generates a constant, given its type arguments*) |
198 fun const_of thy (a,Ts) = Const(a, Sign.const_instance thy (a,Ts)); |
198 fun const_of thy (a,Ts) = Const(a, Sign.const_instance thy (a,Ts)); |
199 |
199 |
200 (*First-order translation. No types are known for variables. HOLogic.typeT should allow |
200 (*First-order translation. No types are known for variables. HOLogic.typeT should allow |
201 them to be inferred.*) |
201 them to be inferred.*) |
202 fun term_of_stree thy t = |
202 fun term_of_stree args thy t = |
203 case t of |
203 case t of |
204 Int _ => raise STREE t |
204 Int _ => raise STREE t |
|
205 | Br ("hBOOL",[t]) => term_of_stree [] thy t (*ignore hBOOL*) |
|
206 | Br ("hAPP",[t,u]) => term_of_stree (u::args) thy t |
205 | Br (a,ts) => |
207 | Br (a,ts) => |
206 case strip_prefix ResClause.const_prefix a of |
208 case strip_prefix ResClause.const_prefix a of |
207 SOME "equal" => |
209 SOME "equal" => |
208 if length ts = 2 then |
210 if length ts = 2 then |
209 list_comb(Const ("op =", HOLogic.typeT), List.map (term_of_stree thy) ts) |
211 list_comb(Const ("op =", HOLogic.typeT), List.map (term_of_stree [] thy) ts) |
210 else raise STREE t (*equality needs two arguments*) |
212 else raise STREE t (*equality needs two arguments*) |
211 | SOME b => |
213 | SOME b => |
212 let val c = invert_const b |
214 let val c = invert_const b |
213 val nterms = length ts - num_typargs thy c |
215 val nterms = length ts - num_typargs thy c |
214 val us = List.map (term_of_stree thy) (List.take(ts,nterms)) |
216 val us = List.map (term_of_stree [] thy) (List.take(ts,nterms) @ args) |
|
217 (*Extra args from hAPP come AFTER any arguments given directly to the |
|
218 constant.*) |
215 val Ts = List.map type_of_stree (List.drop(ts,nterms)) |
219 val Ts = List.map type_of_stree (List.drop(ts,nterms)) |
216 in list_comb(const_of thy (c, Ts), us) end |
220 in list_comb(const_of thy (c, Ts), us) end |
217 | NONE => (*a variable, not a constant*) |
221 | NONE => (*a variable, not a constant*) |
218 let val T = HOLogic.typeT |
222 let val T = HOLogic.typeT |
219 val opr = (*a Free variable is typically a Skolem function*) |
223 val opr = (*a Free variable is typically a Skolem function*) |
221 SOME b => Free(b,T) |
225 SOME b => Free(b,T) |
222 | NONE => |
226 | NONE => |
223 case strip_prefix ResClause.schematic_var_prefix a of |
227 case strip_prefix ResClause.schematic_var_prefix a of |
224 SOME b => make_var (b,T) |
228 SOME b => make_var (b,T) |
225 | NONE => make_var (a,T) (*Variable from the ATP, say X1*) |
229 | NONE => make_var (a,T) (*Variable from the ATP, say X1*) |
226 in list_comb (opr, List.map (term_of_stree thy) ts) end; |
230 in list_comb (opr, List.map (term_of_stree [] thy) (args@ts)) end; |
227 |
231 |
228 (*Type class literal applied to a type. Returns triple of polarity, class, type.*) |
232 (*Type class literal applied to a type. Returns triple of polarity, class, type.*) |
229 fun constraint_of_stree pol (Br("c_Not",[t])) = constraint_of_stree (not pol) t |
233 fun constraint_of_stree pol (Br("c_Not",[t])) = constraint_of_stree (not pol) t |
230 | constraint_of_stree pol t = case t of |
234 | constraint_of_stree pol t = case t of |
231 Int _ => raise STREE t |
235 Int _ => raise STREE t |
248 (*Accumulate sort constraints in vt, with "real" literals in lits.*) |
252 (*Accumulate sort constraints in vt, with "real" literals in lits.*) |
249 fun lits_of_strees ctxt (vt, lits) [] = (vt, rev (nofalses lits)) |
253 fun lits_of_strees ctxt (vt, lits) [] = (vt, rev (nofalses lits)) |
250 | lits_of_strees ctxt (vt, lits) (t::ts) = |
254 | lits_of_strees ctxt (vt, lits) (t::ts) = |
251 lits_of_strees ctxt (add_constraint (constraint_of_stree true t, vt), lits) ts |
255 lits_of_strees ctxt (add_constraint (constraint_of_stree true t, vt), lits) ts |
252 handle STREE _ => |
256 handle STREE _ => |
253 lits_of_strees ctxt (vt, term_of_stree (ProofContext.theory_of ctxt) t :: lits) ts; |
257 lits_of_strees ctxt (vt, term_of_stree [] (ProofContext.theory_of ctxt) t :: lits) ts; |
254 |
258 |
255 (*Update TVars/TFrees with detected sort constraints.*) |
259 (*Update TVars/TFrees with detected sort constraints.*) |
256 fun fix_sorts vt = |
260 fun fix_sorts vt = |
257 let fun tysubst (Type (a, Ts)) = Type (a, map tysubst Ts) |
261 let fun tysubst (Type (a, Ts)) = Type (a, map tysubst Ts) |
258 | tysubst (TVar (xi, s)) = TVar (xi, getOpt (Vartab.lookup vt xi, s)) |
262 | tysubst (TVar (xi, s)) = TVar (xi, getOpt (Vartab.lookup vt xi, s)) |