# HG changeset patch # User paulson # Date 1160487048 -7200 # Node ID 1ea394dc2a0fccdff52ce540c212a0b2f9fc8370 # Parent 070d176a8e2d5c95e472e7098e12a0483eb5c9c7 Combinators require the theory name; added settings for SPASS diff -r 070d176a8e2d -r 1ea394dc2a0f src/HOL/Tools/res_hol_clause.ML --- a/src/HOL/Tools/res_hol_clause.ML Tue Oct 10 13:59:16 2006 +0200 +++ b/src/HOL/Tools/res_hol_clause.ML Tue Oct 10 15:30:48 2006 +0200 @@ -48,12 +48,20 @@ exception DECRE_COMB of string; -fun decreB count_comb n = if count_comb then (if !combB_count >= n then combB_count := !combB_count - n else raise (DECRE_COMB "COMBB")) else (); +fun decreB count_comb n = + if count_comb then + if !combB_count >= n then combB_count := !combB_count - n else raise DECRE_COMB "COMBB" + else (); -fun decreC count_comb n = if count_comb then (if !combC_count >= n then combC_count := !combC_count - n else raise (DECRE_COMB "COMBC")) else (); +fun decreC count_comb n = + if count_comb then + if !combC_count >= n then combC_count := !combC_count - n else raise DECRE_COMB "COMBC" + else (); -fun decreS count_comb n = if count_comb then (if !combS_count >= n then combS_count := !combS_count - n else raise (DECRE_COMB "COMBS")) else (); - +fun decreS count_comb n = + if count_comb then + if !combS_count >= n then combS_count := !combS_count - n else raise DECRE_COMB "COMBS" + else (); val const_typargs = ref (Library.K [] : (string*typ -> typ list)); @@ -82,7 +90,7 @@ (*******************************************) -fun mk_compact_comb (tm as (Const("COMBB",_)$p) $ (Const("COMBB",_)$q$r)) Bnds count_comb = +fun mk_compact_comb (tm as (Const("Reconstruction.COMBB",_)$p) $ (Const("Reconstruction.COMBB",_)$q$r)) Bnds count_comb = let val tp_p = Term.type_of1(Bnds,p) val tp_q = Term.type_of1(Bnds,q) val tp_r = Term.type_of1(Bnds,r) @@ -91,9 +99,9 @@ val _ = increB' count_comb val _ = decreB count_comb 2 in - Const("COMBB_e",typ_B') $ p $ q $ r + Const("Reconstruction.COMBB'",typ_B') $ p $ q $ r end - | mk_compact_comb (tm as (Const("COMBC",_) $ (Const("COMBB",_)$p$q) $ r)) Bnds count_comb = + | mk_compact_comb (tm as (Const("Reconstruction.COMBC",_) $ (Const("Reconstruction.COMBB",_)$p$q) $ r)) Bnds count_comb = let val tp_p = Term.type_of1(Bnds,p) val tp_q = Term.type_of1(Bnds,q) val tp_r = Term.type_of1(Bnds,r) @@ -103,9 +111,9 @@ val _ = decreC count_comb 1 val _ = decreB count_comb 1 in - Const("COMBC_e",typ_C') $ p $ q $ r + Const("Reconstruction.COMBC'",typ_C') $ p $ q $ r end - | mk_compact_comb (tm as (Const("COMBS",_) $ (Const("COMBB",_)$p$q) $ r)) Bnds count_comb = + | mk_compact_comb (tm as (Const("Reconstruction.COMBS",_) $ (Const("Reconstruction.COMBB",_)$p$q) $ r)) Bnds count_comb = let val tp_p = Term.type_of1(Bnds,p) val tp_q = Term.type_of1(Bnds,q) val tp_r = Term.type_of1(Bnds,r) @@ -115,7 +123,7 @@ val _ = decreS count_comb 1 val _ = decreB count_comb 1 in - Const("COMBS_e",typ_S') $ p $ q $ r + Const("Reconstruction.COMBS'",typ_S') $ p $ q $ r end | mk_compact_comb tm _ _ = tm; @@ -125,7 +133,7 @@ let val tpI = Type("fun",[tp,tp]) val _ = increI count_comb in - Const("COMBI",tpI) + Const("Reconstruction.COMBI",tpI) end | lam2comb (Abs(x,tp,Bound n)) Bnds count_comb = let val (Bound n') = decre_bndVar (Bound n) @@ -133,25 +141,25 @@ val tK = Type("fun",[tb,Type("fun",[tp,tb])]) val _ = increK count_comb in - Const("COMBK",tK) $ (Bound n') + Const("Reconstruction.COMBK",tK) $ (Bound n') end | lam2comb (Abs(x,t1,Const(c,t2))) _ count_comb = let val tK = Type("fun",[t2,Type("fun",[t1,t2])]) val _ = increK count_comb in - Const("COMBK",tK) $ Const(c,t2) + Const("Reconstruction.COMBK",tK) $ Const(c,t2) end | lam2comb (Abs(x,t1,Free(v,t2))) _ count_comb = let val tK = Type("fun",[t2,Type("fun",[t1,t2])]) val _ = increK count_comb in - Const("COMBK",tK) $ Free(v,t2) + Const("Reconstruction.COMBK",tK) $ Free(v,t2) end | lam2comb (Abs(x,t1,Var(ind,t2))) _ count_comb = let val tK = Type("fun",[t2,Type("fun",[t1,t2])]) val _ = increK count_comb in - Const("COMBK",tK) $ Var(ind,t2) + Const("Reconstruction.COMBK",tK) $ Var(ind,t2) end | lam2comb (t as (Abs(x,t1,P$(Bound 0)))) Bnds count_comb = let val nfreeP = not(is_free P 0) @@ -166,7 +174,7 @@ val _ = increI count_comb val _ = increS count_comb in - compact_comb (Const("COMBS",tS) $ P' $ Const("COMBI",tI)) Bnds count_comb + compact_comb (Const("Reconstruction.COMBS",tS) $ P' $ Const("Reconstruction.COMBI",tI)) Bnds count_comb end) end @@ -179,7 +187,7 @@ val PQ' = decre_bndVar(P $ Q) val _ = increK count_comb in - Const("COMBK",tK) $ PQ' + Const("Reconstruction.COMBK",tK) $ PQ' end) else ( if nfreeP then ( @@ -190,7 +198,7 @@ val tB = Type("fun",[tp,Type("fun",[tq',Type("fun",[t1,tpq])])]) val _ = increB count_comb in - compact_comb (Const("COMBB",tB) $ P' $ Q') Bnds count_comb + compact_comb (Const("Reconstruction.COMBB",tB) $ P' $ Q') Bnds count_comb end) else ( if nfreeQ then ( @@ -201,7 +209,7 @@ val tC = Type("fun",[tp',Type("fun",[tq,Type("fun",[t1,tpq])])]) val _ = increC count_comb in - compact_comb (Const("COMBC",tC) $ P' $ Q') Bnds count_comb + compact_comb (Const("Reconstruction.COMBC",tC) $ P' $ Q') Bnds count_comb end) else( let val P' = lam2comb (Abs(x,t1,P)) Bnds count_comb @@ -211,7 +219,7 @@ val tS = Type("fun",[tp',Type("fun",[tq',Type("fun",[t1,tpq])])]) val _ = increS count_comb in - compact_comb (Const("COMBS",tS) $ P' $ Q') Bnds count_comb + compact_comb (Const("Reconstruction.COMBS",tS) $ P' $ Q') Bnds count_comb end))) end | lam2comb (t as (Abs(x,t1,_))) _ _ = raise ResClause.CLAUSE("HOL CLAUSE",t); @@ -795,7 +803,10 @@ TextIO.output (out, "end_of_list.\n\nlist_of_clauses(conjectures,cnf).\n"); ResClause.writeln_strs out tfree_clss; ResClause.writeln_strs out dfg_clss; - TextIO.output (out, "end_of_list.\n\nend_problem.\n"); + TextIO.output (out, "end_of_list.\n\n"); + (*VarWeight=3 helps the HO problems, probably by counteracting the presence of hAPP*) + TextIO.output (out, "list_of_settings(SPASS).\n{*\nset_flag(VarWeight,3).\n*}\nend_of_list.\n\n"); + TextIO.output (out, "end_problem.\n"); TextIO.closeOut out; clnames end;