removed stateful init: operations take proper theory argument;
authorwenzelm
Sat Aug 18 13:32:25 2007 +0200 (2007-08-18)
changeset 243239aa7b5708eac
parent 24322 dc7336b8c54c
child 24324 9625e5bfa456
removed stateful init: operations take proper theory argument;
src/HOL/Tools/res_hol_clause.ML
     1.1 --- a/src/HOL/Tools/res_hol_clause.ML	Sat Aug 18 13:32:23 2007 +0200
     1.2 +++ b/src/HOL/Tools/res_hol_clause.ML	Sat Aug 18 13:32:25 2007 +0200
     1.3 @@ -19,7 +19,6 @@
     1.4    datatype type_level = T_FULL | T_PARTIAL | T_CONST
     1.5    val typ_level: type_level ref
     1.6    val minimize_applies: bool ref
     1.7 -  val init: theory -> unit
     1.8    type axiom_name = string
     1.9    type polarity = bool
    1.10    type clause_id = int
    1.11 @@ -29,11 +28,11 @@
    1.12      | CombApp of combterm * combterm
    1.13    datatype literal = Literal of polarity * combterm
    1.14    val strip_comb: combterm -> combterm * combterm list
    1.15 -  val literals_of_term: term -> literal list * (ResClause.typ_var * sort) list
    1.16 -  val tptp_write_file: bool -> thm list -> string ->
    1.17 +  val literals_of_term: theory -> term -> literal list * (ResClause.typ_var * sort) list
    1.18 +  val tptp_write_file: theory -> bool -> thm list -> string ->
    1.19      (thm * (axiom_name * clause_id)) list * ResClause.classrelClause list *
    1.20        ResClause.arityClause list -> string list -> axiom_name list
    1.21 -  val dfg_write_file: bool -> thm list -> string ->
    1.22 +  val dfg_write_file: theory -> bool -> thm list -> string ->
    1.23      (thm * (axiom_name * clause_id)) list * ResClause.classrelClause list *
    1.24        ResClause.arityClause list -> string list -> axiom_name list
    1.25  end
    1.26 @@ -71,8 +70,6 @@
    1.27    constant-typed translation, though it could be tried for the partially-typed one.*)
    1.28  val minimize_applies = ref true;
    1.29  
    1.30 -val const_typargs = ref (Library.K [] : (string*typ -> typ list));
    1.31 -
    1.32  val const_min_arity = ref (Symtab.empty : int Symtab.table);
    1.33  
    1.34  val const_needs_hBOOL = ref (Symtab.empty : bool Symtab.table);
    1.35 @@ -84,7 +81,6 @@
    1.36  fun needs_hBOOL c = not (!minimize_applies) orelse !typ_level=T_PARTIAL orelse
    1.37                      getOpt (Symtab.lookup(!const_needs_hBOOL) c, false);
    1.38  
    1.39 -fun init thy = (const_typargs := Sign.const_typargs thy);
    1.40  
    1.41  (**********************************************************************)
    1.42  (* convert a Term.term with lambdas into a Term.term with combinators *)
    1.43 @@ -212,46 +208,46 @@
    1.44    | simp_type_of (TVar (v,s)) = RC.AtomV(RC.make_schematic_type_var v);
    1.45  
    1.46  
    1.47 -fun const_type_of (c,t) =
    1.48 +fun const_type_of thy (c,t) =
    1.49        let val (tp,ts) = type_of t
    1.50 -      in  (tp, ts, map simp_type_of (!const_typargs(c,t))) end;
    1.51 +      in  (tp, ts, map simp_type_of (Sign.const_typargs thy (c,t))) end;
    1.52  
    1.53  (* convert a Term.term (with combinators) into a combterm, also accummulate sort info *)
    1.54 -fun combterm_of (Const(c,t)) =
    1.55 -      let val (tp,ts,tvar_list) = const_type_of (c,t)
    1.56 +fun combterm_of thy (Const(c,t)) =
    1.57 +      let val (tp,ts,tvar_list) = const_type_of thy (c,t)
    1.58            val c' = CombConst(RC.make_fixed_const c, tp, tvar_list)
    1.59        in  (c',ts)  end
    1.60 -  | combterm_of (Free(v,t)) =
    1.61 +  | combterm_of thy (Free(v,t)) =
    1.62        let val (tp,ts) = type_of t
    1.63            val v' = if RC.isMeta v then CombVar(RC.make_schematic_var(v,0),tp)
    1.64                     else CombConst(RC.make_fixed_var v, tp, [])
    1.65        in  (v',ts)  end
    1.66 -  | combterm_of (Var(v,t)) =
    1.67 +  | combterm_of thy (Var(v,t)) =
    1.68        let val (tp,ts) = type_of t
    1.69            val v' = CombVar(RC.make_schematic_var v,tp)
    1.70        in  (v',ts)  end
    1.71 -  | combterm_of (t as (P $ Q)) =
    1.72 -      let val (P',tsP) = combterm_of P
    1.73 -          val (Q',tsQ) = combterm_of Q
    1.74 +  | combterm_of thy (t as (P $ Q)) =
    1.75 +      let val (P',tsP) = combterm_of thy P
    1.76 +          val (Q',tsQ) = combterm_of thy Q
    1.77        in  (CombApp(P',Q'), tsP union tsQ)  end;
    1.78  
    1.79 -fun predicate_of ((Const("Not",_) $ P), polarity) = predicate_of (P, not polarity)
    1.80 -  | predicate_of (t,polarity) = (combterm_of t, polarity);
    1.81 +fun predicate_of thy ((Const("Not",_) $ P), polarity) = predicate_of thy (P, not polarity)
    1.82 +  | predicate_of thy (t,polarity) = (combterm_of thy t, polarity);
    1.83  
    1.84 -fun literals_of_term1 args (Const("Trueprop",_) $ P) = literals_of_term1 args P
    1.85 -  | literals_of_term1 args (Const("op |",_) $ P $ Q) =
    1.86 -      literals_of_term1 (literals_of_term1 args P) Q
    1.87 -  | literals_of_term1 (lits,ts) P =
    1.88 -      let val ((pred,ts'),pol) = predicate_of (P,true)
    1.89 +fun literals_of_term1 thy args (Const("Trueprop",_) $ P) = literals_of_term1 thy args P
    1.90 +  | literals_of_term1 thy args (Const("op |",_) $ P $ Q) =
    1.91 +      literals_of_term1 thy (literals_of_term1 thy args P) Q
    1.92 +  | literals_of_term1 thy (lits,ts) P =
    1.93 +      let val ((pred,ts'),pol) = predicate_of thy (P,true)
    1.94        in
    1.95            (Literal(pol,pred)::lits, ts union ts')
    1.96        end;
    1.97  
    1.98 -fun literals_of_term P = literals_of_term1 ([],[]) P;
    1.99 +fun literals_of_term thy P = literals_of_term1 thy ([],[]) P;
   1.100  
   1.101  (* making axiom and conjecture clauses *)
   1.102 -fun make_clause(clause_id,axiom_name,kind,th) =
   1.103 -    let val (lits,ctypes_sorts) = literals_of_term (to_comb (prop_of th) [])
   1.104 +fun make_clause thy (clause_id,axiom_name,kind,th) =
   1.105 +    let val (lits,ctypes_sorts) = literals_of_term thy (to_comb (prop_of th) [])
   1.106          val (ctvar_lits,ctfree_lits) = RC.add_typs_aux ctypes_sorts
   1.107      in
   1.108          if forall isFalse lits
   1.109 @@ -264,20 +260,20 @@
   1.110      end;
   1.111  
   1.112  
   1.113 -fun add_axiom_clause ((th,(name,id)), pairs) =
   1.114 -  let val cls = make_clause(id, name, RC.Axiom, th)
   1.115 +fun add_axiom_clause thy ((th,(name,id)), pairs) =
   1.116 +  let val cls = make_clause thy (id, name, RC.Axiom, th)
   1.117    in
   1.118        if isTaut cls then pairs else (name,cls)::pairs
   1.119    end;
   1.120  
   1.121 -val make_axiom_clauses = foldl add_axiom_clause [];
   1.122 +fun make_axiom_clauses thy = foldl (add_axiom_clause thy) [];
   1.123  
   1.124 -fun make_conjecture_clauses_aux _ [] = []
   1.125 -  | make_conjecture_clauses_aux n (th::ths) =
   1.126 -      make_clause(n,"conjecture", RC.Conjecture, th) ::
   1.127 -      make_conjecture_clauses_aux (n+1) ths;
   1.128 +fun make_conjecture_clauses_aux _ _ [] = []
   1.129 +  | make_conjecture_clauses_aux thy n (th::ths) =
   1.130 +      make_clause thy (n,"conjecture", RC.Conjecture, th) ::
   1.131 +      make_conjecture_clauses_aux thy (n+1) ths;
   1.132  
   1.133 -val make_conjecture_clauses = make_conjecture_clauses_aux 0;
   1.134 +fun make_conjecture_clauses thy = make_conjecture_clauses_aux thy 0;
   1.135  
   1.136  
   1.137  (**********************************************************************)
   1.138 @@ -524,7 +520,7 @@
   1.139  
   1.140  val cnf_helper_thms = ResAxioms.cnf_rules_pairs o (map ResAxioms.pairname)
   1.141  
   1.142 -fun get_helper_clauses isFO (conjectures, axclauses, user_lemmas) =
   1.143 +fun get_helper_clauses thy isFO (conjectures, axclauses, user_lemmas) =
   1.144    if isFO then []  (*first-order*)
   1.145    else
   1.146      let val ct0 = foldl count_clause init_counters conjectures
   1.147 @@ -547,7 +543,7 @@
   1.148                   else []
   1.149          val other = cnf_helper_thms [ext,fequal_imp_equal,equal_imp_fequal]
   1.150      in
   1.151 -        map #2 (make_axiom_clauses (other @ IK @ BC @ S @ B'C' @ S'))
   1.152 +        map #2 (make_axiom_clauses thy (other @ IK @ BC @ S @ B'C' @ S'))
   1.153      end;
   1.154  
   1.155  (*Find the minimal arity of each function mentioned in the term. Also, note which uses
   1.156 @@ -590,12 +586,12 @@
   1.157  (* tptp format *)
   1.158  
   1.159  (* write TPTP format to a single file *)
   1.160 -fun tptp_write_file isFO thms filename (ax_tuples,classrel_clauses,arity_clauses) user_lemmas =
   1.161 +fun tptp_write_file thy isFO thms filename (ax_tuples,classrel_clauses,arity_clauses) user_lemmas =
   1.162      let val _ = Output.debug (fn () => ("Preparing to write the TPTP file " ^ filename))
   1.163          val _ = RC.dfg_format := false
   1.164 -        val conjectures = make_conjecture_clauses thms
   1.165 -        val (clnames,axclauses) = ListPair.unzip (make_axiom_clauses ax_tuples)
   1.166 -        val helper_clauses = get_helper_clauses isFO (conjectures, axclauses, user_lemmas)
   1.167 +        val conjectures = make_conjecture_clauses thy thms
   1.168 +        val (clnames,axclauses) = ListPair.unzip (make_axiom_clauses thy ax_tuples)
   1.169 +        val helper_clauses = get_helper_clauses thy isFO (conjectures, axclauses, user_lemmas)
   1.170          val _ = count_constants (conjectures, axclauses, helper_clauses);
   1.171          val (tptp_clss,tfree_litss) = ListPair.unzip (map clause2tptp conjectures)
   1.172          val tfree_clss = map RC.tptp_tfree_clause (foldl (op union_string) [] tfree_litss)
   1.173 @@ -615,14 +611,14 @@
   1.174  
   1.175  (* dfg format *)
   1.176  
   1.177 -fun dfg_write_file isFO thms filename (ax_tuples,classrel_clauses,arity_clauses) user_lemmas =
   1.178 +fun dfg_write_file thy isFO thms filename (ax_tuples,classrel_clauses,arity_clauses) user_lemmas =
   1.179      let val _ = Output.debug (fn () => ("Preparing to write the DFG file " ^ filename))
   1.180          val _ = RC.dfg_format := true
   1.181 -        val conjectures = make_conjecture_clauses thms
   1.182 -        val (clnames,axclauses) = ListPair.unzip (make_axiom_clauses ax_tuples)
   1.183 -        val helper_clauses = get_helper_clauses isFO (conjectures, axclauses, user_lemmas)
   1.184 +        val conjectures = make_conjecture_clauses thy thms
   1.185 +        val (clnames,axclauses) = ListPair.unzip (make_axiom_clauses thy ax_tuples)
   1.186 +        val helper_clauses = get_helper_clauses thy isFO (conjectures, axclauses, user_lemmas)
   1.187          val _ = count_constants (conjectures, axclauses, helper_clauses);
   1.188 -        val (dfg_clss,tfree_litss) = ListPair.unzip (map clause2dfg conjectures)
   1.189 +        val (dfg_clss, tfree_litss) = ListPair.unzip (map clause2dfg conjectures)
   1.190          and probname = Path.implode (Path.base (Path.explode filename))
   1.191          val axstrs = map (#1 o clause2dfg) axclauses
   1.192          val tfree_clss = map RC.dfg_tfree_clause (RC.union_all tfree_litss)