305 fun type_constraint_from_term ctxt (u as ATerm (a, us)) = |
305 fun type_constraint_from_term ctxt (u as ATerm (a, us)) = |
306 case (strip_prefix_and_unascii class_prefix a, map (typ_from_atp ctxt) us) of |
306 case (strip_prefix_and_unascii class_prefix a, map (typ_from_atp ctxt) us) of |
307 (SOME b, [T]) => (b, T) |
307 (SOME b, [T]) => (b, T) |
308 | _ => raise HO_TERM [u] |
308 | _ => raise HO_TERM [u] |
309 |
309 |
310 (** Accumulate type constraints in a formula: negative type literals **) |
310 (* Accumulate type constraints in a formula: negative type literals. *) |
311 fun add_var (key, z) = Vartab.map_default (key, []) (cons z) |
311 fun add_var (key, z) = Vartab.map_default (key, []) (cons z) |
312 fun add_type_constraint false (cl, TFree (a ,_)) = add_var ((a, ~1), cl) |
312 fun add_type_constraint false (cl, TFree (a ,_)) = add_var ((a, ~1), cl) |
313 | add_type_constraint false (cl, TVar (ix, _)) = add_var (ix, cl) |
313 | add_type_constraint false (cl, TVar (ix, _)) = add_var (ix, cl) |
314 | add_type_constraint _ _ = I |
314 | add_type_constraint _ _ = I |
315 |
315 |
327 | [s1, s2] => (case Int.fromString s2 of |
327 | [s1, s2] => (case Int.fromString s2 of |
328 SOME n => subscript_name s1 n |
328 SOME n => subscript_name s1 n |
329 | NONE => s) |
329 | NONE => s) |
330 | _ => s |
330 | _ => s |
331 end |
331 end |
|
332 |
|
333 (* The number of type arguments of a constant, zero if it's monomorphic. For |
|
334 (instances of) Skolem pseudoconstants, this information is encoded in the |
|
335 constant name. *) |
|
336 fun num_type_args thy s = |
|
337 if String.isPrefix skolem_const_prefix s then |
|
338 s |> space_explode Long_Name.separator |> List.last |> Int.fromString |> the |
|
339 else |
|
340 (s, Sign.the_const_type thy s) |> Sign.const_typargs thy |> length |
332 |
341 |
333 fun slack_fastype_of t = fastype_of t handle TERM _ => HOLogic.typeT |
342 fun slack_fastype_of t = fastype_of t handle TERM _ => HOLogic.typeT |
334 |
343 |
335 (* First-order translation. No types are known for variables. "HOLogic.typeT" |
344 (* First-order translation. No types are known for variables. "HOLogic.typeT" |
336 should allow them to be inferred. *) |
345 should allow them to be inferred. *) |
415 let |
424 let |
416 val ts = map (do_term [] NONE) us @ extra_ts |
425 val ts = map (do_term [] NONE) us @ extra_ts |
417 val T = map slack_fastype_of ts ---> HOLogic.typeT |
426 val T = map slack_fastype_of ts ---> HOLogic.typeT |
418 val t = |
427 val t = |
419 case strip_prefix_and_unascii fixed_var_prefix a of |
428 case strip_prefix_and_unascii fixed_var_prefix a of |
420 SOME b => Free (b, T) |
429 SOME b => |
|
430 (* FIXME: reconstruction of lambda-lifting *) |
|
431 Free (b, T) |
421 | NONE => |
432 | NONE => |
422 case strip_prefix_and_unascii schematic_var_prefix a of |
433 case strip_prefix_and_unascii schematic_var_prefix a of |
423 SOME b => Var ((b, var_index), T) |
434 SOME b => Var ((b, var_index), T) |
424 | NONE => |
435 | NONE => |
425 Var ((a |> textual ? repair_variable_name Char.toLower, |
436 Var ((a |> textual ? repair_variable_name Char.toLower, |