Now also handles FO problems
authorpaulson
Thu Jun 14 13:18:59 2007 +0200 (2007-06-14)
changeset 233869255c1a75ba9
parent 23385 0ef4f9fc0d09
child 23387 7cb8faa5d4d3
Now also handles FO problems
src/HOL/Tools/res_hol_clause.ML
     1.1 --- a/src/HOL/Tools/res_hol_clause.ML	Thu Jun 14 13:18:24 2007 +0200
     1.2 +++ b/src/HOL/Tools/res_hol_clause.ML	Thu Jun 14 13:18:59 2007 +0200
     1.3 @@ -59,10 +59,7 @@
     1.4  fun needs_hBOOL c = not (!minimize_applies) orelse !typ_level=T_PARTIAL orelse
     1.5                      getOpt (Symtab.lookup(!const_needs_hBOOL) c, false);
     1.6  
     1.7 -fun init thy = 
     1.8 -  (const_typargs := Sign.const_typargs thy; 
     1.9 -   const_min_arity := Symtab.empty; 
    1.10 -   const_needs_hBOOL := Symtab.empty);
    1.11 +fun init thy = (const_typargs := Sign.const_typargs thy);
    1.12  
    1.13  (**********************************************************************)
    1.14  (* convert a Term.term with lambdas into a Term.term with combinators *) 
    1.15 @@ -166,8 +163,7 @@
    1.16  type polarity = bool;
    1.17  type clause_id = int;
    1.18  
    1.19 -datatype combterm = CombConst of string * RC.fol_type * RC.fol_type list
    1.20 -		  | CombFree of string * RC.fol_type
    1.21 +datatype combterm = CombConst of string * RC.fol_type * RC.fol_type list (*Const and Free*)
    1.22  		  | CombVar of string * RC.fol_type
    1.23  		  | CombApp of combterm * combterm
    1.24  		  
    1.25 @@ -230,7 +226,7 @@
    1.26    | combterm_of (Free(v,t)) =
    1.27        let val (tp,ts) = type_of t
    1.28  	  val v' = if RC.isMeta v then CombVar(RC.make_schematic_var(v,0),tp)
    1.29 -		   else CombFree(RC.make_fixed_var v,tp)
    1.30 +		   else CombConst(RC.make_fixed_var v, tp, [])
    1.31        in  (v',ts)  end
    1.32    | combterm_of (Var(v,t)) =
    1.33        let val (tp,ts) = type_of t
    1.34 @@ -297,7 +293,6 @@
    1.35    | result_type _ = raise ERROR "result_type"
    1.36  
    1.37  fun type_of_combterm (CombConst(c,tp,_)) = tp
    1.38 -  | type_of_combterm (CombFree(v,tp)) = tp
    1.39    | type_of_combterm (CombVar(v,tp)) = tp
    1.40    | type_of_combterm (CombApp(t1,t2)) = result_type (type_of_combterm t1);
    1.41  
    1.42 @@ -323,7 +318,6 @@
    1.43  fun string_of_combterm1 (CombConst(c,tp,_)) = 
    1.44        let val c' = if c = "equal" then "c_fequal" else c
    1.45        in  wrap_type (c',tp)  end
    1.46 -  | string_of_combterm1 (CombFree(v,tp)) = wrap_type (v,tp)
    1.47    | string_of_combterm1 (CombVar(v,tp)) = wrap_type (v,tp)
    1.48    | string_of_combterm1 (CombApp(t1,t2)) =
    1.49        let val s1 = string_of_combterm1 t1
    1.50 @@ -355,7 +349,6 @@
    1.51        in
    1.52  	  string_apply (c ^ RC.paren_pack (args1@targs), args2)
    1.53        end
    1.54 -  | string_of_applic (CombFree(v,tp), args) = string_apply (v, args)
    1.55    | string_of_applic (CombVar(v,tp), args) = string_apply (v, args)
    1.56    | string_of_applic _ = raise ERROR "string_of_applic";
    1.57  
    1.58 @@ -438,7 +431,6 @@
    1.59    end; 
    1.60  
    1.61  fun get_uvars (CombConst _) vars = vars
    1.62 -  | get_uvars (CombFree _) vars = vars
    1.63    | get_uvars (CombVar(v,_)) vars = (v::vars)
    1.64    | get_uvars (CombApp(P,Q)) vars = get_uvars P (get_uvars Q vars);
    1.65  
    1.66 @@ -472,8 +464,6 @@
    1.67                     if needs_hBOOL c then (addtypes tvars (addit funcs), preds)
    1.68                     else (addtypes tvars funcs, addit preds)
    1.69                 end)
    1.70 -  | add_decls (CombFree(v,ctp), (funcs,preds)) = 
    1.71 -      (RC.add_foltype_funcs (ctp,Symtab.update (v,0) funcs), preds)
    1.72    | add_decls (CombVar(_,ctp), (funcs,preds)) = 
    1.73        (RC.add_foltype_funcs (ctp,funcs), preds)
    1.74    | add_decls (CombApp(P,Q),decls) = add_decls(P,add_decls (Q,decls));
    1.75 @@ -486,7 +476,7 @@
    1.76  
    1.77  fun decls_of_clauses clauses arity_clauses =
    1.78    let val happ_ar = case !typ_level of T_PARTIAL => 3 | _ => 2
    1.79 -      val init_functab = Symtab.update (type_wrapper,2) (Symtab.update ("hAPP",happ_ar) Symtab.empty)
    1.80 +      val init_functab = Symtab.update (type_wrapper,2) (Symtab.update ("hAPP",happ_ar) RC.init_functab)
    1.81        val init_predtab = Symtab.update ("hBOOL",1) Symtab.empty
    1.82        val (functab,predtab) = (foldl add_clause_decls (init_functab, init_predtab) clauses)
    1.83    in
    1.84 @@ -523,7 +513,6 @@
    1.85  fun count_combterm (CombConst(c,tp,_), ct) = 
    1.86       (case Symtab.lookup ct c of NONE => ct  (*no counter*)
    1.87                                 | SOME n => Symtab.update (c,n+1) ct)
    1.88 -  | count_combterm (CombFree(v,tp), ct) = ct
    1.89    | count_combterm (CombVar(v,tp), ct) = ct
    1.90    | count_combterm (CombApp(t1,t2), ct) = count_combterm(t1, count_combterm(t2, ct));
    1.91  
    1.92 @@ -537,7 +526,9 @@
    1.93  
    1.94  val cnf_helper_thms = ResAxioms.cnf_rules_pairs o (map ResAxioms.pairname)
    1.95  
    1.96 -fun get_helper_clauses (conjectures, axclauses, user_lemmas) =
    1.97 +fun get_helper_clauses isFO (conjectures, axclauses, user_lemmas) =
    1.98 +  if isFO then []  (*first-order*)
    1.99 +  else
   1.100      let val ct0 = foldl count_clause init_counters conjectures
   1.101          val ct = foldl (count_user_clause user_lemmas) ct0 axclauses
   1.102          fun needed c = valOf (Symtab.lookup ct c) > 0
   1.103 @@ -559,7 +550,7 @@
   1.104  	val other = cnf_helper_thms [ext,fequal_imp_equal,equal_imp_fequal]
   1.105      in
   1.106  	map #2 (make_axiom_clauses (other @ IK @ BC @ S @ B'C' @ S'))
   1.107 -    end
   1.108 +    end;
   1.109  
   1.110  (*Find the minimal arity of each function mentioned in the term. Also, note which uses
   1.111    are not at top level, to see if hBOOL is needed.*)
   1.112 @@ -590,7 +581,9 @@
   1.113  
   1.114  fun count_constants (conjectures, axclauses, helper_clauses) = 
   1.115    if !minimize_applies andalso !typ_level<>T_PARTIAL then
   1.116 -    (List.app count_constants_clause conjectures;
   1.117 +    (const_min_arity := Symtab.empty; 
   1.118 +     const_needs_hBOOL := Symtab.empty;
   1.119 +     List.app count_constants_clause conjectures;
   1.120       List.app count_constants_clause axclauses;
   1.121       List.app count_constants_clause helper_clauses;
   1.122       List.app display_arity (Symtab.dest (!const_min_arity)))
   1.123 @@ -599,10 +592,12 @@
   1.124  (* tptp format *)
   1.125  						  
   1.126  (* write TPTP format to a single file *)
   1.127 -fun tptp_write_file thms filename (ax_tuples,classrel_clauses,arity_clauses) user_lemmas =
   1.128 -    let val conjectures = make_conjecture_clauses thms
   1.129 +fun tptp_write_file isFO thms filename (ax_tuples,classrel_clauses,arity_clauses) user_lemmas =
   1.130 +    let val _ = Output.debug (fn () => ("Preparing to write the TPTP file " ^ filename))
   1.131 +        val _ = RC.dfg_format := false
   1.132 +        val conjectures = make_conjecture_clauses thms
   1.133          val (clnames,axclauses) = ListPair.unzip (make_axiom_clauses ax_tuples)
   1.134 -	val helper_clauses = get_helper_clauses (conjectures, axclauses, user_lemmas)
   1.135 +	val helper_clauses = get_helper_clauses isFO (conjectures, axclauses, user_lemmas)
   1.136  	val _ = count_constants (conjectures, axclauses, helper_clauses);
   1.137  	val (tptp_clss,tfree_litss) = ListPair.unzip (map clause2tptp conjectures)
   1.138  	val tfree_clss = map RC.tptp_tfree_clause (foldl (op union_string) [] tfree_litss)
   1.139 @@ -622,10 +617,12 @@
   1.140  
   1.141  (* dfg format *)
   1.142  
   1.143 -fun dfg_write_file  thms filename (ax_tuples,classrel_clauses,arity_clauses) user_lemmas =
   1.144 -    let val conjectures = make_conjecture_clauses thms
   1.145 +fun dfg_write_file isFO thms filename (ax_tuples,classrel_clauses,arity_clauses) user_lemmas =
   1.146 +    let val _ = Output.debug (fn () => ("Preparing to write the DFG file " ^ filename))
   1.147 +        val _ = RC.dfg_format := true
   1.148 +        val conjectures = make_conjecture_clauses thms
   1.149          val (clnames,axclauses) = ListPair.unzip (make_axiom_clauses ax_tuples)
   1.150 -	val helper_clauses = get_helper_clauses (conjectures, axclauses, user_lemmas)
   1.151 +	val helper_clauses = get_helper_clauses isFO (conjectures, axclauses, user_lemmas)
   1.152  	val _ = count_constants (conjectures, axclauses, helper_clauses);
   1.153  	val (dfg_clss,tfree_litss) = ListPair.unzip (map clause2dfg conjectures)
   1.154  	and probname = Path.implode (Path.base (Path.explode filename))