# HG changeset patch # User nipkow # Date 1245927632 -7200 # Node ID 477f2abf90a4940c67b704dc22ad0f2ec853fc0d # Parent 294b955d0e80c586bc9592232cccd9d10db15c2a Streamlined code diff -r 294b955d0e80 -r 477f2abf90a4 src/HOL/Tools/res_hol_clause.ML --- a/src/HOL/Tools/res_hol_clause.ML Thu Jun 25 07:34:30 2009 +0200 +++ b/src/HOL/Tools/res_hol_clause.ML Thu Jun 25 13:00:32 2009 +0200 @@ -12,8 +12,6 @@ val comb_B: thm val comb_C: thm val comb_S: thm - datatype type_level = T_FULL | T_CONST - val typ_level: type_level val minimize_applies: bool type axiom_name = string type polarity = bool @@ -59,10 +57,8 @@ val equal_imp_fequal = thm "ATP_Linkup.equal_imp_fequal"; -(*The different translations of types*) -datatype type_level = T_FULL | T_CONST; - -val typ_level = T_CONST; +(* Parameter t_full below indicates that full type information is to be +exported *) (*If true, each function will be directly applied to as many arguments as possible, avoiding use of the "apply" operator. Use of hBOOL is also minimized.*) @@ -260,26 +256,26 @@ fun wrap_type_if t_full cnh (head, s, tp) = if head_needs_hBOOL cnh head then wrap_type t_full (s, tp) else s; -fun string_of_combterm t_full cma cnh t = +fun string_of_combterm (params as (t_full, cma, cnh)) t = let val (head, args) = strip_comb t in wrap_type_if t_full cnh (head, - string_of_applic t_full cma (head, map (string_of_combterm t_full cma cnh) args), + string_of_applic t_full cma (head, map (string_of_combterm (params)) args), type_of_combterm t) end; (*Boolean-valued terms are here converted to literals.*) -fun boolify t_full cma cnh t = - "hBOOL" ^ RC.paren_pack [string_of_combterm t_full cma cnh t]; +fun boolify params t = + "hBOOL" ^ RC.paren_pack [string_of_combterm params t]; -fun string_of_predicate t_full cma cnh t = +fun string_of_predicate (params as (_,_,cnh)) t = case t of (CombApp(CombApp(CombConst("equal",_,_), t1), t2)) => (*DFG only: new TPTP prefers infix equality*) - ("equal" ^ RC.paren_pack [string_of_combterm t_full cma cnh t1, string_of_combterm t_full cma cnh t2]) + ("equal" ^ RC.paren_pack [string_of_combterm params t1, string_of_combterm params t2]) | _ => case #1 (strip_comb t) of - CombConst(c,_,_) => if needs_hBOOL cnh c then boolify t_full cma cnh t else string_of_combterm t_full cma cnh t - | _ => boolify t_full cma cnh t; + CombConst(c,_,_) => if needs_hBOOL cnh c then boolify params t else string_of_combterm params t + | _ => boolify params t; fun string_of_clausename (cls_id,ax_name) = RC.clause_prefix ^ RC.ascii_of ax_name ^ "_" ^ Int.toString cls_id; @@ -290,23 +286,23 @@ (*** tptp format ***) -fun tptp_of_equality t_full cma cnh pol (t1,t2) = +fun tptp_of_equality params pol (t1,t2) = let val eqop = if pol then " = " else " != " - in string_of_combterm t_full cma cnh t1 ^ eqop ^ string_of_combterm t_full cma cnh t2 end; + in string_of_combterm params t1 ^ eqop ^ string_of_combterm params t2 end; -fun tptp_literal t_full cma cnh (Literal(pol, CombApp(CombApp(CombConst("equal",_,_), t1), t2))) = - tptp_of_equality t_full cma cnh pol (t1,t2) - | tptp_literal t_full cma cnh (Literal(pol,pred)) = - RC.tptp_sign pol (string_of_predicate t_full cma cnh pred); +fun tptp_literal params (Literal(pol, CombApp(CombApp(CombConst("equal",_,_), t1), t2))) = + tptp_of_equality params pol (t1,t2) + | tptp_literal params (Literal(pol,pred)) = + RC.tptp_sign pol (string_of_predicate params pred); (*Given a clause, returns its literals paired with a list of literals concerning TFrees; the latter should only occur in conjecture clauses.*) -fun tptp_type_lits t_full cma cnh pos (Clause{literals, ctypes_sorts, ...}) = - (map (tptp_literal t_full cma cnh) literals, +fun tptp_type_lits params pos (Clause{literals, ctypes_sorts, ...}) = + (map (tptp_literal params) literals, map (RC.tptp_of_typeLit pos) (RC.add_typs ctypes_sorts)); -fun clause2tptp (t_full, cma, cnh) (cls as Clause{axiom_name,clause_id,kind,ctypes_sorts,...}) = - let val (lits,tylits) = tptp_type_lits t_full cma cnh (kind = RC.Conjecture) cls +fun clause2tptp params (cls as Clause{axiom_name,clause_id,kind,ctypes_sorts,...}) = + let val (lits,tylits) = tptp_type_lits params (kind = RC.Conjecture) cls in (RC.gen_tptp_cls(clause_id,axiom_name,kind,lits,tylits), tylits) end; @@ -314,10 +310,10 @@ (*** dfg format ***) -fun dfg_literal t_full cma cnh (Literal(pol,pred)) = RC.dfg_sign pol (string_of_predicate t_full cma cnh pred); +fun dfg_literal params (Literal(pol,pred)) = RC.dfg_sign pol (string_of_predicate params pred); -fun dfg_type_lits t_full cma cnh pos (Clause{literals, ctypes_sorts, ...}) = - (map (dfg_literal t_full cma cnh) literals, +fun dfg_type_lits params pos (Clause{literals, ctypes_sorts, ...}) = + (map (dfg_literal params) literals, map (RC.dfg_of_typeLit pos) (RC.add_typs ctypes_sorts)); fun get_uvars (CombConst _) vars = vars @@ -328,8 +324,8 @@ fun dfg_vars (Clause {literals,...}) = RC.union_all (map get_uvars_l literals); -fun clause2dfg (t_full, cma, cnh) (cls as Clause{axiom_name,clause_id,kind,ctypes_sorts,...}) = - let val (lits,tylits) = dfg_type_lits t_full cma cnh (kind = RC.Conjecture) cls +fun clause2dfg params (cls as Clause{axiom_name,clause_id,kind,ctypes_sorts,...}) = + let val (lits,tylits) = dfg_type_lits params (kind = RC.Conjecture) cls val vars = dfg_vars cls val tvars = RC.get_tvar_strs ctypes_sorts in @@ -341,7 +337,7 @@ fun addtypes tvars tab = List.foldl RC.add_foltype_funcs tab tvars; -fun add_decls t_full cma cnh (CombConst(c,tp,tvars), (funcs,preds)) = +fun add_decls (t_full, cma, cnh) (CombConst(c,tp,tvars), (funcs,preds)) = if c = "equal" then (addtypes tvars funcs, preds) else let val arity = min_arity_of cma c @@ -351,20 +347,20 @@ if needs_hBOOL cnh c then (addtypes tvars (addit funcs), preds) else (addtypes tvars funcs, addit preds) end - | add_decls _ _ _ (CombVar(_,ctp), (funcs,preds)) = + | add_decls _ (CombVar(_,ctp), (funcs,preds)) = (RC.add_foltype_funcs (ctp,funcs), preds) - | add_decls t_full cma cnh (CombApp(P,Q),decls) = add_decls t_full cma cnh (P,add_decls t_full cma cnh (Q,decls)); + | add_decls params (CombApp(P,Q),decls) = add_decls params (P,add_decls params (Q,decls)); -fun add_literal_decls t_full cma cnh (Literal(_,c), decls) = add_decls t_full cma cnh (c,decls); +fun add_literal_decls params (Literal(_,c), decls) = add_decls params (c,decls); -fun add_clause_decls t_full cma cnh (Clause {literals, ...}, decls) = - List.foldl (add_literal_decls t_full cma cnh) decls literals +fun add_clause_decls params (Clause {literals, ...}, decls) = + List.foldl (add_literal_decls params) decls literals handle Symtab.DUP a => error ("function " ^ a ^ " has multiple arities") -fun decls_of_clauses (t_full, cma, cnh) clauses arity_clauses = +fun decls_of_clauses params clauses arity_clauses = let val init_functab = Symtab.update (type_wrapper,2) (Symtab.update ("hAPP",2) RC.init_functab) val init_predtab = Symtab.update ("hBOOL",1) Symtab.empty - val (functab,predtab) = (List.foldl (add_clause_decls t_full cma cnh) (init_functab, init_predtab) clauses) + val (functab,predtab) = (List.foldl (add_clause_decls params) (init_functab, init_predtab) clauses) in (Symtab.dest (List.foldl RC.add_arityClause_funcs functab arity_clauses), Symtab.dest predtab)