author paulson Fri, 09 Mar 2007 13:10:22 +0100 changeset 22428 1755e6381b2c parent 22427 69ce2cb9e3e5 child 22429 09e794384323
First stab at reconstructing HO problems
```--- a/src/HOL/Tools/res_reconstruct.ML	Fri Mar 09 08:45:59 2007 +0100
+++ b/src/HOL/Tools/res_reconstruct.ML	Fri Mar 09 13:10:22 2007 +0100
@@ -199,19 +199,23 @@

(*First-order translation. No types are known for variables. HOLogic.typeT should allow
them to be inferred.*)
-fun term_of_stree thy t =
+fun term_of_stree args thy t =
case t of
Int _ => raise STREE t
+    | Br ("hBOOL",[t]) => term_of_stree [] thy t  (*ignore hBOOL*)
+    | Br ("hAPP",[t,u]) => term_of_stree (u::args) thy t
| Br (a,ts) =>
case strip_prefix ResClause.const_prefix a of
SOME "equal" =>
if length ts = 2 then
-                list_comb(Const ("op =", HOLogic.typeT), List.map (term_of_stree thy) ts)
+                list_comb(Const ("op =", HOLogic.typeT), List.map (term_of_stree [] thy) ts)
else raise STREE t  (*equality needs two arguments*)
| SOME b =>
let val c = invert_const b
val nterms = length ts - num_typargs thy c
-                  val us = List.map (term_of_stree thy) (List.take(ts,nterms))
+                  val us = List.map (term_of_stree [] thy) (List.take(ts,nterms) @ args)
+                  (*Extra args from hAPP come AFTER any arguments given directly to the
+                    constant.*)
val Ts = List.map type_of_stree (List.drop(ts,nterms))
in  list_comb(const_of thy (c, Ts), us)  end
| NONE => (*a variable, not a constant*)
@@ -223,7 +227,7 @@
case strip_prefix ResClause.schematic_var_prefix a of
SOME b => make_var (b,T)
| NONE => make_var (a,T)    (*Variable from the ATP, say X1*)
-              in  list_comb (opr, List.map (term_of_stree thy) ts)  end;
+              in  list_comb (opr, List.map (term_of_stree [] thy) (args@ts))  end;

(*Type class literal applied to a type. Returns triple of polarity, class, type.*)
fun constraint_of_stree pol (Br("c_Not",[t])) = constraint_of_stree (not pol) t
@@ -250,7 +254,7 @@
| lits_of_strees ctxt (vt, lits) (t::ts) =
lits_of_strees ctxt (add_constraint (constraint_of_stree true t, vt), lits) ts
handle STREE _ =>
-      lits_of_strees ctxt (vt, term_of_stree (ProofContext.theory_of ctxt) t :: lits) ts;
+      lits_of_strees ctxt (vt, term_of_stree [] (ProofContext.theory_of ctxt) t :: lits) ts;

(*Update TVars/TFrees with detected sort constraints.*)
fun fix_sorts vt =```