src/HOL/Tools/res_hol_clause.ML
changeset 24937 340523598914
parent 24385 ab62948281a9
child 24940 8f9dea697b8d
     1.1 --- a/src/HOL/Tools/res_hol_clause.ML	Tue Oct 09 17:11:20 2007 +0200
     1.2 +++ b/src/HOL/Tools/res_hol_clause.ML	Tue Oct 09 18:14:00 2007 +0200
     1.3 @@ -97,9 +97,7 @@
     1.4                      th: thm,
     1.5                      kind: RC.kind,
     1.6                      literals: literal list,
     1.7 -                    ctypes_sorts: (RC.typ_var * Term.sort) list,
     1.8 -                    ctvar_type_literals: RC.type_literal list,
     1.9 -                    ctfree_type_literals: RC.type_literal list};
    1.10 +                    ctypes_sorts: (RC.typ_var * Term.sort) list};
    1.11  
    1.12  
    1.13  (*********************************************************************)
    1.14 @@ -177,15 +175,12 @@
    1.15  (* making axiom and conjecture clauses *)
    1.16  fun make_clause thy (clause_id,axiom_name,kind,th) =
    1.17      let val (lits,ctypes_sorts) = literals_of_term thy (prop_of th)
    1.18 -        val (ctvar_lits,ctfree_lits) = RC.add_typs_aux ctypes_sorts
    1.19      in
    1.20          if forall isFalse lits
    1.21          then error "Problem too trivial for resolution (empty clause)"
    1.22          else
    1.23              Clause {clause_id = clause_id, axiom_name = axiom_name, th = th, kind = kind,
    1.24 -                    literals = lits, ctypes_sorts = ctypes_sorts,
    1.25 -                    ctvar_type_literals = ctvar_lits,
    1.26 -                    ctfree_type_literals = ctfree_lits}
    1.27 +                    literals = lits, ctypes_sorts = ctypes_sorts}
    1.28      end;
    1.29  
    1.30  
    1.31 @@ -302,34 +297,24 @@
    1.32  
    1.33  (*Given a clause, returns its literals paired with a list of literals concerning TFrees;
    1.34    the latter should only occur in conjecture clauses.*)
    1.35 -fun tptp_type_lits (Clause cls) =
    1.36 -    let val lits = map tptp_literal (#literals cls)
    1.37 -        val ctvar_lits_strs = map RC.tptp_of_typeLit (#ctvar_type_literals cls)
    1.38 -        val ctfree_lits = map RC.tptp_of_typeLit (#ctfree_type_literals cls)
    1.39 -    in
    1.40 -        (ctvar_lits_strs @ lits, ctfree_lits)
    1.41 -    end;
    1.42 +fun tptp_type_lits pos (Clause{literals, ctypes_sorts, ...}) =
    1.43 +      (map tptp_literal literals, 
    1.44 +       map (RC.tptp_of_typeLit pos) (RC.add_typs ctypes_sorts));
    1.45  
    1.46  fun clause2tptp (cls as Clause{axiom_name,clause_id,kind,ctypes_sorts,...}) =
    1.47 -    let val (lits,ctfree_lits) = tptp_type_lits cls
    1.48 -        val cls_str = RC.gen_tptp_cls(clause_id,axiom_name,kind,lits)
    1.49 -    in
    1.50 -        (cls_str,ctfree_lits)
    1.51 -    end;
    1.52 +  let val (lits,tylits) = tptp_type_lits (kind = RC.Conjecture) cls
    1.53 +  in
    1.54 +      (RC.gen_tptp_cls(clause_id,axiom_name,kind,lits,tylits), tylits)
    1.55 +  end;
    1.56  
    1.57  
    1.58  (*** dfg format ***)
    1.59  
    1.60  fun dfg_literal (Literal(pol,pred)) = RC.dfg_sign pol (string_of_predicate pred);
    1.61  
    1.62 -fun dfg_clause_aux (Clause{literals, ctypes_sorts, ...}) =
    1.63 -  let val lits = map dfg_literal literals
    1.64 -      val (tvar_lits,tfree_lits) = RC.add_typs_aux ctypes_sorts
    1.65 -      val tvar_lits_strs = map RC.dfg_of_typeLit tvar_lits
    1.66 -      val tfree_lits = map RC.dfg_of_typeLit tfree_lits
    1.67 -  in
    1.68 -      (tvar_lits_strs @ lits, tfree_lits)
    1.69 -  end;
    1.70 +fun dfg_type_lits pos (Clause{literals, ctypes_sorts, ...}) =
    1.71 +      (map dfg_literal literals, 
    1.72 +       map (RC.dfg_of_typeLit pos) (RC.add_typs ctypes_sorts));
    1.73  
    1.74  fun get_uvars (CombConst _) vars = vars
    1.75    | get_uvars (CombVar(v,_)) vars = (v::vars)
    1.76 @@ -340,13 +325,13 @@
    1.77  fun dfg_vars (Clause {literals,...}) = RC.union_all (map get_uvars_l literals);
    1.78  
    1.79  fun clause2dfg (cls as Clause{axiom_name,clause_id,kind,ctypes_sorts,...}) =
    1.80 -    let val (lits,tfree_lits) = dfg_clause_aux cls
    1.81 -        val vars = dfg_vars cls
    1.82 -        val tvars = RC.get_tvar_strs ctypes_sorts
    1.83 -        val knd = RC.name_of_kind kind
    1.84 -        val lits_str = commas lits
    1.85 -        val cls_str = RC.gen_dfg_cls(clause_id, axiom_name, knd, lits_str, tvars@vars)
    1.86 -    in (cls_str, tfree_lits) end;
    1.87 +  let val (lits,tylits) = dfg_type_lits (kind = RC.Conjecture) cls
    1.88 +      val vars = dfg_vars cls
    1.89 +      val tvars = RC.get_tvar_strs ctypes_sorts
    1.90 +  in
    1.91 +      (RC.gen_dfg_cls(clause_id, axiom_name, kind, lits, tylits, tvars@vars), tylits)
    1.92 +  end;
    1.93 +
    1.94  
    1.95  (** For DFG format: accumulate function and predicate declarations **)
    1.96  
    1.97 @@ -509,7 +494,6 @@
    1.98      end;
    1.99  
   1.100  
   1.101 -
   1.102  (* dfg format *)
   1.103  
   1.104  fun dfg_write_file thy isFO thms filename (ax_tuples,classrel_clauses,arity_clauses) user_lemmas =