# HG changeset patch # User mengj # Date 1158753243 -7200 # Node ID ff938c7b15e8cd6914832f2c69655656ce327d60 # Parent 267f30cbe2cbaeb99b1a2aa343efb48c43362c95 Introduced combinators B', C' and S'. diff -r 267f30cbe2cb -r ff938c7b15e8 src/HOL/Tools/res_hol_clause.ML --- a/src/HOL/Tools/res_hol_clause.ML Wed Sep 20 13:53:03 2006 +0200 +++ b/src/HOL/Tools/res_hol_clause.ML Wed Sep 20 13:54:03 2006 +0200 @@ -9,17 +9,41 @@ struct +(* a flag to set if we use extra combinators B',C',S' *) +val use_combB'C'S' = ref true; -val include_combS = ref false; -val include_min_comb = ref false; +val combI_count = ref 0; +val combK_count = ref 0; +val combB_count = ref 0; +val combC_count = ref 0; +val combS_count = ref 0; + +val combB'_count = ref 0; +val combC'_count = ref 0; +val combS'_count = ref 0; + -fun in_min_comb count_comb = if count_comb then include_min_comb:=true else (); - -fun in_combS count_comb = if count_comb then include_combS:=true else (); +fun increI count_comb = if count_comb then combI_count := !combI_count + 1 else (); +fun increK count_comb = if count_comb then combK_count := !combK_count + 1 else (); +fun increB count_comb = if count_comb then combB_count := !combB_count + 1 else (); +fun increC count_comb = if count_comb then combC_count := !combC_count + 1 else (); +fun increS count_comb = if count_comb then combS_count := !combS_count + 1 else (); +fun increB' count_comb = if count_comb then combB'_count := !combB'_count + 1 else (); +fun increC' count_comb = if count_comb then combC'_count := !combC'_count + 1 else (); +fun increS' count_comb = if count_comb then combS'_count := !combS'_count + 1 else (); + + +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 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 (); + val const_typargs = ref (Library.K [] : (string*typ -> typ list)); -fun init thy = (include_combS:=false; include_min_comb:=false; +fun init thy = (combI_count:=0; combK_count:=0;combB_count:=0;combC_count:=0;combS_count:=0;combB'_count:=0;combC'_count:=0;combS'_count:=0; const_typargs := Sign.const_typargs thy); (**********************************************************************) @@ -46,9 +70,48 @@ (*******************************************) +fun mk_compact_comb (tm as (Const("COMBB",_)$p) $ (Const("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) + val typ = Term.type_of1(Bnds,tm) + val typ_B' = [tp_p,tp_q,tp_r] ---> typ + val _ = increB' count_comb + val _ = decreB count_comb 2 + in + Const("COMBB_e",typ_B') $ p $ q $ r + end + | mk_compact_comb (tm as (Const("COMBC",_) $ (Const("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) + val typ = Term.type_of1(Bnds,tm) + val typ_C' = [tp_p,tp_q,tp_r] ---> typ + val _ = increC' count_comb + val _ = decreC count_comb 1 + val _ = decreB count_comb 1 + in + Const("COMBC_e",typ_C') $ p $ q $ r + end + | mk_compact_comb (tm as (Const("COMBS",_) $ (Const("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) + val typ = Term.type_of1(Bnds,tm) + val typ_S' = [tp_p,tp_q,tp_r] ---> typ + val _ = increS' count_comb + val _ = decreS count_comb 1 + val _ = decreB count_comb 1 + in + Const("COMBS_e",typ_S') $ p $ q $ r + end + | mk_compact_comb tm _ _ = tm; + +fun compact_comb t Bnds count_comb = if !use_combB'C'S' then mk_compact_comb t Bnds count_comb else t; + fun lam2comb (Abs(x,tp,Bound 0)) _ count_comb = let val tpI = Type("fun",[tp,tp]) - val _ = in_min_comb count_comb + val _ = increI count_comb in Const("COMBI",tpI) end @@ -56,25 +119,25 @@ let val (Bound n') = decre_bndVar (Bound n) val tb = List.nth(Bnds,n') val tK = Type("fun",[tb,Type("fun",[tp,tb])]) - val _ = in_min_comb count_comb + val _ = increK count_comb in Const("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 _ = in_min_comb count_comb + val _ = increK count_comb in Const("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 _ = in_min_comb count_comb + val _ = increK count_comb in Const("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 _ = in_min_comb count_comb + val _ = increK count_comb in Const("COMBK",tK) $ Var(ind,t2) end @@ -88,10 +151,10 @@ val P' = lam2comb (Abs(x,t1,P)) Bnds count_comb val tp' = Term.type_of1(Bnds,P') val tS = Type("fun",[tp',Type("fun",[tI,tr])]) - val _ = in_min_comb count_comb - val _ = in_combS count_comb + val _ = increI count_comb + val _ = increS count_comb in - Const("COMBS",tS) $ P' $ Const("COMBI",tI) + compact_comb (Const("COMBS",tS) $ P' $ Const("COMBI",tI)) Bnds count_comb end) end @@ -102,7 +165,7 @@ if(nfreeP andalso nfreeQ) then ( let val tK = Type("fun",[tpq,Type("fun",[t1,tpq])]) val PQ' = decre_bndVar(P $ Q) - val _ = in_min_comb count_comb + val _ = increK count_comb in Const("COMBK",tK) $ PQ' end) @@ -113,9 +176,9 @@ val tp = Term.type_of1(Bnds,P') val tq' = Term.type_of1(Bnds, Q') val tB = Type("fun",[tp,Type("fun",[tq',Type("fun",[t1,tpq])])]) - val _ = in_min_comb count_comb + val _ = increB count_comb in - Const("COMBB",tB) $ P' $ Q' + compact_comb (Const("COMBB",tB) $ P' $ Q') Bnds count_comb end) else ( if nfreeQ then ( @@ -124,9 +187,9 @@ val tq = Term.type_of1(Bnds,Q') val tp' = Term.type_of1(Bnds, P') val tC = Type("fun",[tp',Type("fun",[tq,Type("fun",[t1,tpq])])]) - val _ = in_min_comb count_comb + val _ = increC count_comb in - Const("COMBC",tC) $ P' $ Q' + compact_comb (Const("COMBC",tC) $ P' $ Q') Bnds count_comb end) else( let val P' = lam2comb (Abs(x,t1,P)) Bnds count_comb @@ -134,10 +197,9 @@ val tp' = Term.type_of1(Bnds,P') val tq' = Term.type_of1(Bnds,Q') val tS = Type("fun",[tp',Type("fun",[tq',Type("fun",[t1,tpq])])]) - val _ = in_min_comb count_comb - val _ = in_combS count_comb + val _ = increS count_comb in - Const("COMBS",tS) $ P' $ Q' + compact_comb (Const("COMBS",tS) $ P' $ Q') Bnds count_comb end))) end | lam2comb (t as (Abs(x,t1,_))) _ _ = raise LAM2COMB (t); @@ -150,9 +212,9 @@ | to_comb (P $ Q) Bnds count_comb = ((to_comb P Bnds count_comb) $ (to_comb Q Bnds count_comb)) | to_comb t _ _ = t; - + fun comb_of t count_comb = to_comb t [] count_comb; - + (* print a term containing combinators, used for debugging *) exception TERM_COMB of term; @@ -313,6 +375,34 @@ val c = range_type (range_type t1) in map simp_type_of [a,b,c] + end + | comb_typ ("COMBB_e",t) = + let val t1 = domain_type t + val a = domain_type t1 + val b = range_type t1 + val t2 = domain_type (range_type(range_type t)) + val c = domain_type t2 + val d = range_type t2 + in + map simp_type_of [a,b,c,d] + end + | comb_typ ("COMBC_e",t) = + let val t1 = domain_type t + val a = domain_type t1 + val b = domain_type (range_type t1) + val c = range_type (range_type t1) + val d = domain_type (domain_type (range_type t)) + in + map simp_type_of [a,b,c,d] + end + | comb_typ ("COMBS_e",t) = + let val t1 = domain_type t + val a = domain_type t1 + val b = domain_type (range_type t1) + val c = range_type (range_type t1) + val d = domain_type (domain_type (range_type t)) + in + map simp_type_of [a,b,c,d] end; fun const_type_of ("COMBI",t) = @@ -345,6 +435,24 @@ in (tp,ts,C_var) end + | const_type_of ("COMBB_e",t) = + let val (tp,ts) = type_of t + val B'_var = comb_typ ("COMBB_e",t) + in + (tp,ts,B'_var) + end + | const_type_of ("COMBC_e",t) = + let val (tp,ts) = type_of t + val C'_var = comb_typ ("COMBC_e",t) + in + (tp,ts,C'_var) + end + | const_type_of ("COMBS_e",t) = + let val (tp,ts) = type_of t + val S'_var = comb_typ ("COMBS_e",t) + in + (tp,ts,S'_var) + end | const_type_of (c,t) = let val (tp,ts) = type_of t val tvars = !const_typargs(c,t) @@ -353,6 +461,7 @@ (tp,ts,tvars') end; + fun is_bool_type (Type("bool",[])) = true | is_bool_type _ = false; @@ -677,12 +786,15 @@ | "c_COMBI" => Symtab.update (comb,1) funcs | "c_COMBB" => Symtab.update (comb,3) funcs | "c_COMBC" => Symtab.update (comb,3) funcs + | "c_COMBB_e" => Symtab.update (comb,4) funcs + | "c_COMBC_e" => Symtab.update (comb,4) funcs + | "c_COMBS_e" => Symtab.update (comb,4) funcs | _ => funcs) | _ => Symtab.update (comb,0) funcs; fun init_funcs_tab funcs = let val tp = !typ_level - val funcs0 = foldl init_combs funcs ["c_COMBK","c_COMBS","c_COMBI","c_COMBB","c_COMBC"] + val funcs0 = foldl init_combs funcs ["c_COMBK","c_COMBS","c_COMBI","c_COMBB","c_COMBC","c_COMBB_e","c_COMBC_e","c_COMBS_e"] val funcs1 = case tp of T_PARTIAL => Symtab.update ("hAPP",3) funcs0 | _ => Symtab.update ("hAPP",2) funcs0 val funcs2 = case tp of T_FULL => Symtab.update ("typeinfo",2) funcs1 @@ -732,6 +844,17 @@ fun read_in fs = map (File.read o File.unpack_platform_path) fs; +fun get_helper_tptp () = + let val IK = if !combI_count > 0 orelse !combK_count > 0 then (Output.debug "Include combinator I K";["combIK.tptp"]) else [] + val BC = if !combB_count > 0 orelse !combC_count > 0 then (Output.debug "Include combinator B C";["combBC.tptp"]) else [] + val S = if !combS_count > 0 then (Output.debug "Include combinator S";["combS.tptp"]) else [] + val B'C' = if !combB'_count > 0 orelse !combC'_count > 0 then (Output.debug "Include combinator B' C'"; ["combBC_e.tptp"]) else [] + val S' = if !combS'_count > 0 then (Output.debug "Include combinator S'";["combS_e.tptp"]) else [] + in + ("helper1.tptp") :: (IK @ BC @ S @ B'C' @ S') + end; + + fun get_helper_clauses_tptp () = let val tlevel = case !typ_level of T_FULL => (Output.debug "Fully-typed HOL"; @@ -742,13 +865,7 @@ "~~/src/HOL/Tools/atp-inputs/const_") | T_NONE => (Output.debug "Untyped HOL"; "~~/src/HOL/Tools/atp-inputs/u_") - val helpers = if !include_combS - then (Output.debug "Include combinator S"; - ["helper1.tptp","comb_inclS.tptp"]) - else if !include_min_comb - then (Output.debug "Include min combinators"; - ["helper1.tptp","comb_noS.tptp"]) - else (Output.debug "No combinator is used"; ["helper1.tptp"]) + val helpers = get_helper_tptp () val t_helpers = map (curry (op ^) tlevel) helpers in read_in t_helpers @@ -776,6 +893,17 @@ end; +fun get_helper_dfg () = + let val IK = if !combI_count > 0 orelse !combK_count > 0 then (Output.debug "Include combinator I K";["combIK.dfg"]) else [] + val BC = if !combB_count > 0 orelse !combC_count > 0 then (Output.debug "Include combinator B C";["combBC.dfg"]) else [] + val S = if !combS_count > 0 then (Output.debug "Include combinator S";["combS.dfg"]) else [] + val B'C' = if !combB'_count > 0 orelse !combC'_count > 0 then (Output.debug "Include combinator B' C'"; ["combBC_e.dfg"]) else [] + val S' = if !combS'_count > 0 then (Output.debug "Include combinator S'";["combS_e.dfg"]) else [] + in + ("helper1.dfg") :: (IK @ BC @ S @ B'C' @ S') + end; + + (* dfg format *) fun get_helper_clauses_dfg () = let val tlevel = case !typ_level of @@ -787,13 +915,7 @@ "~~/src/HOL/Tools/atp-inputs/const_") | T_NONE => (Output.debug "Untyped HOL"; "~~/src/HOL/Tools/atp-inputs/u_") - val helpers = if !include_combS - then (Output.debug "Include combinator S"; - ["helper1.dfg","comb_inclS.dfg"]) else - if !include_min_comb - then (Output.debug "Include min combinators"; - ["helper1.dfg","comb_noS.dfg"]) - else (Output.debug "No combinator is used"; ["helper1.dfg"]) + val helpers = get_helper_dfg () val t_helpers = map (curry (op ^) tlevel) helpers in read_in t_helpers