Deleted the partially-typed translation and the combinator code.
authorpaulson
Tue Aug 21 18:27:14 2007 +0200 (2007-08-21)
changeset 24385ab62948281a9
parent 24384 0002537695df
child 24386 7cbaf94aed08
Deleted the partially-typed translation and the combinator code.
Minimize_applies now uses the same translation code, which handles both cases anyway.
src/HOL/Tools/res_hol_clause.ML
     1.1 --- a/src/HOL/Tools/res_hol_clause.ML	Tue Aug 21 17:24:57 2007 +0200
     1.2 +++ b/src/HOL/Tools/res_hol_clause.ML	Tue Aug 21 18:27:14 2007 +0200
     1.3 @@ -16,7 +16,7 @@
     1.4    val comb_B: thm
     1.5    val comb_C: thm
     1.6    val comb_S: thm
     1.7 -  datatype type_level = T_FULL | T_PARTIAL | T_CONST
     1.8 +  datatype type_level = T_FULL | T_CONST
     1.9    val typ_level: type_level ref
    1.10    val minimize_applies: bool ref
    1.11    type axiom_name = string
    1.12 @@ -57,17 +57,12 @@
    1.13  
    1.14  
    1.15  (*The different translations of types*)
    1.16 -datatype type_level = T_FULL | T_PARTIAL | T_CONST;
    1.17 +datatype type_level = T_FULL | T_CONST;
    1.18  
    1.19  val typ_level = ref T_CONST;
    1.20  
    1.21 -fun full_types () = (typ_level:=T_FULL);
    1.22 -fun partial_types () = (typ_level:=T_PARTIAL);
    1.23 -fun const_types_only () = (typ_level:=T_CONST);
    1.24 -
    1.25  (*If true, each function will be directly applied to as many arguments as possible, avoiding
    1.26 -  use of the "apply" operator. Use of hBOOL is also minimized. It only works for the
    1.27 -  constant-typed translation, though it could be tried for the partially-typed one.*)
    1.28 +  use of the "apply" operator. Use of hBOOL is also minimized.*)
    1.29  val minimize_applies = ref true;
    1.30  
    1.31  val const_min_arity = ref (Symtab.empty : int Symtab.table);
    1.32 @@ -78,77 +73,10 @@
    1.33  
    1.34  (*True if the constant ever appears outside of the top-level position in literals.
    1.35    If false, the constant always receives all of its arguments and is used as a predicate.*)
    1.36 -fun needs_hBOOL c = not (!minimize_applies) orelse !typ_level=T_PARTIAL orelse
    1.37 +fun needs_hBOOL c = not (!minimize_applies) orelse
    1.38                      getOpt (Symtab.lookup(!const_needs_hBOOL) c, false);
    1.39  
    1.40  
    1.41 -(**********************************************************************)
    1.42 -(* convert a Term.term with lambdas into a Term.term with combinators *)
    1.43 -(**********************************************************************)
    1.44 -
    1.45 -fun is_free (Bound(a)) n = (a = n)
    1.46 -  | is_free (Abs(x,_,b)) n = (is_free b (n+1))
    1.47 -  | is_free (P $ Q) n = ((is_free P n) orelse (is_free Q n))
    1.48 -  | is_free _ _ = false;
    1.49 -
    1.50 -fun compact_comb t bnds = t;
    1.51 -
    1.52 -fun lam2comb (Abs(x,tp,Bound 0)) _ = Const("ATP_Linkup.COMBI",tp-->tp)
    1.53 -  | lam2comb (Abs(x,tp,Bound n)) bnds =
    1.54 -      let val tb = List.nth(bnds,n-1)
    1.55 -      in  Const("ATP_Linkup.COMBK", [tb,tp] ---> tb) $ Bound (n-1)  end
    1.56 -  | lam2comb (Abs(x,t1,Const(c,t2))) _ = Const("ATP_Linkup.COMBK",[t2,t1] ---> t2) $ Const(c,t2)
    1.57 -  | lam2comb (Abs(x,t1,Free(v,t2))) _ = Const("ATP_Linkup.COMBK",[t2,t1] ---> t2) $ Free(v,t2)
    1.58 -  | lam2comb (Abs(x,t1,Var(ind,t2))) _ = Const("ATP_Linkup.COMBK", [t2,t1] ---> t2) $ Var(ind,t2)
    1.59 -  | lam2comb (t as (Abs(x,t1,P$(Bound 0)))) bnds =
    1.60 -      if is_free P 0 then
    1.61 -          let val tI = [t1] ---> t1
    1.62 -              val P' = lam2comb (Abs(x,t1,P)) bnds
    1.63 -              val tp' = Term.type_of1(bnds,P')
    1.64 -              val tS = [tp',tI] ---> Term.type_of1(t1::bnds,P)
    1.65 -          in
    1.66 -              compact_comb (Const("ATP_Linkup.COMBS",tS) $ P' $
    1.67 -                             Const("ATP_Linkup.COMBI",tI)) bnds
    1.68 -          end
    1.69 -      else incr_boundvars ~1 P
    1.70 -  | lam2comb (t as (Abs(x,t1,P$Q))) bnds =
    1.71 -      let val nfreeP = not(is_free P 0)
    1.72 -          and nfreeQ = not(is_free Q 0)
    1.73 -          val tpq = Term.type_of1(t1::bnds, P$Q)
    1.74 -      in
    1.75 -          if nfreeP andalso nfreeQ
    1.76 -          then
    1.77 -            let val tK = [tpq,t1] ---> tpq
    1.78 -            in  Const("ATP_Linkup.COMBK",tK) $ incr_boundvars ~1 (P $ Q)  end
    1.79 -          else if nfreeP then
    1.80 -            let val Q' = lam2comb (Abs(x,t1,Q)) bnds
    1.81 -                val P' = incr_boundvars ~1 P
    1.82 -                val tp = Term.type_of1(bnds,P')
    1.83 -                val tq' = Term.type_of1(bnds, Q')
    1.84 -                val tB = [tp,tq',t1] ---> tpq
    1.85 -            in  compact_comb (Const("ATP_Linkup.COMBB",tB) $ P' $ Q') bnds  end
    1.86 -          else if nfreeQ then
    1.87 -            let val P' = lam2comb (Abs(x,t1,P)) bnds
    1.88 -                val Q' = incr_boundvars ~1 Q
    1.89 -                val tq = Term.type_of1(bnds,Q')
    1.90 -                val tp' = Term.type_of1(bnds, P')
    1.91 -                val tC = [tp',tq,t1] ---> tpq
    1.92 -            in  compact_comb (Const("ATP_Linkup.COMBC",tC) $ P' $ Q') bnds  end
    1.93 -          else
    1.94 -            let val P' = lam2comb (Abs(x,t1,P)) bnds
    1.95 -                val Q' = lam2comb (Abs(x,t1,Q)) bnds
    1.96 -                val tp' = Term.type_of1(bnds,P')
    1.97 -                val tq' = Term.type_of1(bnds,Q')
    1.98 -                val tS = [tp',tq',t1] ---> tpq
    1.99 -            in  compact_comb (Const("ATP_Linkup.COMBS",tS) $ P' $ Q') bnds  end
   1.100 -      end
   1.101 -  | lam2comb (t as (Abs(x,t1,_))) _ = raise RC.CLAUSE("HOL CLAUSE",t);
   1.102 -
   1.103 -fun to_comb (Abs(x,tp,b)) bnds = lam2comb (Abs(x, tp, to_comb b (tp::bnds))) bnds
   1.104 -  | to_comb (P $ Q) bnds = (to_comb P bnds) $ (to_comb Q bnds)
   1.105 -  | to_comb t _ = t;
   1.106 -
   1.107 -
   1.108  (******************************************************)
   1.109  (* data types for typed combinator expressions        *)
   1.110  (******************************************************)
   1.111 @@ -226,10 +154,11 @@
   1.112        let val (tp,ts) = type_of t
   1.113            val v' = CombVar(RC.make_schematic_var v,tp)
   1.114        in  (v',ts)  end
   1.115 -  | combterm_of thy (t as (P $ Q)) =
   1.116 +  | combterm_of thy (P $ Q) =
   1.117        let val (P',tsP) = combterm_of thy P
   1.118            val (Q',tsQ) = combterm_of thy Q
   1.119 -      in  (CombApp(P',Q'), tsP union tsQ)  end;
   1.120 +      in  (CombApp(P',Q'), tsP union tsQ)  end
   1.121 +  | combterm_of thy (t as Abs _) = raise RC.CLAUSE("HOL CLAUSE",t);
   1.122  
   1.123  fun predicate_of thy ((Const("Not",_) $ P), polarity) = predicate_of thy (P, not polarity)
   1.124    | predicate_of thy (t,polarity) = (combterm_of thy t, polarity);
   1.125 @@ -247,7 +176,7 @@
   1.126  
   1.127  (* making axiom and conjecture clauses *)
   1.128  fun make_clause thy (clause_id,axiom_name,kind,th) =
   1.129 -    let val (lits,ctypes_sorts) = literals_of_term thy (to_comb (prop_of th) [])
   1.130 +    let val (lits,ctypes_sorts) = literals_of_term thy (prop_of th)
   1.131          val (ctvar_lits,ctfree_lits) = RC.add_typs_aux ctypes_sorts
   1.132      in
   1.133          if forall isFalse lits
   1.134 @@ -308,21 +237,6 @@
   1.135  
   1.136  fun apply ss = "hAPP" ^ RC.paren_pack ss;
   1.137  
   1.138 -(*Full (non-optimized) and partial-typed transations*)
   1.139 -fun string_of_combterm1 (CombConst(c,tp,_)) =
   1.140 -      let val c' = if c = "equal" then "c_fequal" else c
   1.141 -      in  wrap_type (c',tp)  end
   1.142 -  | string_of_combterm1 (CombVar(v,tp)) = wrap_type (v,tp)
   1.143 -  | string_of_combterm1 (CombApp(t1,t2)) =
   1.144 -      let val s1 = string_of_combterm1 t1
   1.145 -          and s2 = string_of_combterm1 t2
   1.146 -      in
   1.147 -          case !typ_level of
   1.148 -              T_FULL => wrap_type (apply [s1,s2], result_type (type_of_combterm t1))
   1.149 -            | T_PARTIAL => apply [s1,s2, RC.string_of_fol_type (type_of_combterm t1)]
   1.150 -            | T_CONST => raise ERROR "string_of_combterm1"
   1.151 -      end;
   1.152 -
   1.153  fun rev_apply (v, []) = v
   1.154    | rev_apply (v, arg::args) = apply [rev_apply (v, args), arg];
   1.155  
   1.156 @@ -348,20 +262,13 @@
   1.157  
   1.158  fun wrap_type_if (head, s, tp) = if head_needs_hBOOL head then wrap_type (s, tp) else s;
   1.159  
   1.160 -(*Full (if optimized) and constant-typed transations*)
   1.161 -fun string_of_combterm2 t =
   1.162 +fun string_of_combterm t =
   1.163    let val (head, args) = strip_comb t
   1.164    in  wrap_type_if (head,
   1.165 -                    string_of_applic (head, map string_of_combterm2 args),
   1.166 +                    string_of_applic (head, map string_of_combterm args),
   1.167                      type_of_combterm t)
   1.168    end;
   1.169  
   1.170 -fun string_of_combterm t =
   1.171 -    case (!typ_level,!minimize_applies) of
   1.172 -         (T_PARTIAL, _) => string_of_combterm1 t
   1.173 -       | (T_FULL, false) => string_of_combterm1 t
   1.174 -       | _ => string_of_combterm2 t;
   1.175 -
   1.176  (*Boolean-valued terms are here converted to literals.*)
   1.177  fun boolify t = "hBOOL" ^ RC.paren_pack [string_of_combterm t];
   1.178  
   1.179 @@ -448,16 +355,13 @@
   1.180  fun add_decls (CombConst(c,tp,tvars), (funcs,preds)) =
   1.181        if c = "equal" then (addtypes tvars funcs, preds)
   1.182        else
   1.183 -        (case !typ_level of
   1.184 -            T_PARTIAL => (RC.add_foltype_funcs (tp, Symtab.update(c,0) funcs), preds)
   1.185 -          | _ =>
   1.186 -               let val arity = min_arity_of c
   1.187 -                   val ntys = if !typ_level = T_CONST then length tvars else 0
   1.188 -                   val addit = Symtab.update(c, arity+ntys)
   1.189 -               in
   1.190 -                   if needs_hBOOL c then (addtypes tvars (addit funcs), preds)
   1.191 -                   else (addtypes tvars funcs, addit preds)
   1.192 -               end)
   1.193 +	let val arity = min_arity_of c
   1.194 +	    val ntys = if !typ_level = T_CONST then length tvars else 0
   1.195 +	    val addit = Symtab.update(c, arity+ntys)
   1.196 +	in
   1.197 +	    if needs_hBOOL c then (addtypes tvars (addit funcs), preds)
   1.198 +	    else (addtypes tvars funcs, addit preds)
   1.199 +	end
   1.200    | add_decls (CombVar(_,ctp), (funcs,preds)) =
   1.201        (RC.add_foltype_funcs (ctp,funcs), preds)
   1.202    | add_decls (CombApp(P,Q),decls) = add_decls(P,add_decls (Q,decls));
   1.203 @@ -469,8 +373,7 @@
   1.204      handle Symtab.DUP a => raise ERROR ("function " ^ a ^ " has multiple arities")
   1.205  
   1.206  fun decls_of_clauses clauses arity_clauses =
   1.207 -  let val happ_ar = case !typ_level of T_PARTIAL => 3 | _ => 2
   1.208 -      val init_functab = Symtab.update (type_wrapper,2) (Symtab.update ("hAPP",happ_ar) RC.init_functab)
   1.209 +  let val init_functab = Symtab.update (type_wrapper,2) (Symtab.update ("hAPP",2) RC.init_functab)
   1.210        val init_predtab = Symtab.update ("hBOOL",1) Symtab.empty
   1.211        val (functab,predtab) = (foldl add_clause_decls (init_functab, init_predtab) clauses)
   1.212    in
   1.213 @@ -492,12 +395,10 @@
   1.214                 clsrel_clauses)
   1.215  
   1.216  
   1.217 -
   1.218  (**********************************************************************)
   1.219  (* write clauses to files                                             *)
   1.220  (**********************************************************************)
   1.221  
   1.222 -
   1.223  val init_counters =
   1.224      Symtab.make [("c_COMBI", 0), ("c_COMBK", 0),
   1.225                   ("c_COMBB", 0), ("c_COMBC", 0),
   1.226 @@ -574,7 +475,7 @@
   1.227                  (if needs_hBOOL c then " needs hBOOL" else ""));
   1.228  
   1.229  fun count_constants (conjectures, axclauses, helper_clauses) =
   1.230 -  if !minimize_applies andalso !typ_level<>T_PARTIAL then
   1.231 +  if !minimize_applies then
   1.232      (const_min_arity := Symtab.empty;
   1.233       const_needs_hBOOL := Symtab.empty;
   1.234       List.app count_constants_clause conjectures;