# HG changeset patch # User paulson # Date 1126775752 -7200 # Node ID d16c3a62c396f5dc58214f48be9edaadbdd22074 # Parent de60322ff13a4c8cd06ec60ede0b820cf057d11c the experimental tagging system, and the usual tidying diff -r de60322ff13a -r d16c3a62c396 src/HOL/HOL.thy --- a/src/HOL/HOL.thy Thu Sep 15 10:33:35 2005 +0200 +++ b/src/HOL/HOL.thy Thu Sep 15 11:15:52 2005 +0200 @@ -1282,6 +1282,28 @@ setup InductMethod.setup +subsubsection{*Tags, for the ATP Linkup*} + +constdefs + tag :: "bool => bool" + "tag P == P" + +text{*These label the distinguished literals of introduction and elimination +rules.*} + +lemma tagI: "P ==> tag P" +by (simp add: tag_def) + +lemma tagD: "tag P ==> P" +by (simp add: tag_def) + +text{*Applications of "tag" to True and False must go!*} + +lemma tag_True: "tag True = True" +by (simp add: tag_def) + +lemma tag_False: "tag False = False" +by (simp add: tag_def) end diff -r de60322ff13a -r d16c3a62c396 src/HOL/Tools/meson.ML --- a/src/HOL/Tools/meson.ML Thu Sep 15 10:33:35 2005 +0200 +++ b/src/HOL/Tools/meson.ML Thu Sep 15 11:15:52 2005 +0200 @@ -225,7 +225,7 @@ incomplete, since when actually called, the only connectives likely to remain are & | Not.*) fun is_conn c = c mem_string - ["Trueprop", "op &", "op |", "op -->", "op =", "Not", + ["Trueprop", "HOL.tag", "op &", "op |", "op -->", "op =", "Not", "All", "Ex", "Ball", "Bex"]; (*True if the term contains a function where the type of any argument contains @@ -329,8 +329,11 @@ (tryres(th, [conj_forward,disj_forward,all_forward,ex_forward])) handle THM _ => th; -(*The simplification removes defined quantifiers and occurrences of True and False.*) -val nnf_ss = HOL_basic_ss addsimps Ex1_def::Ball_def::Bex_def::simp_thms; +(*The simplification removes defined quantifiers and occurrences of True and False, as well as tags applied to True and False.*) +val tag_True = thm "tag_True"; +val tag_False = thm "tag_False"; +val nnf_simps = [Ex1_def,Ball_def,Bex_def,tag_True,tag_False] +val nnf_ss = HOL_basic_ss addsimps nnf_simps@simp_thms; fun make_nnf th = th |> simplify nnf_ss |> check_is_fol |> make_nnf1 diff -r de60322ff13a -r d16c3a62c396 src/HOL/Tools/res_atp.ML --- a/src/HOL/Tools/res_atp.ML Thu Sep 15 10:33:35 2005 +0200 +++ b/src/HOL/Tools/res_atp.ML Thu Sep 15 11:15:52 2005 +0200 @@ -22,7 +22,7 @@ fun debug_tac tac = (debug "testing"; tac); -val prover = ref "spass"; (* use spass as default prover *) +val prover = ref "E"; (* use E as the default prover *) val custom_spass = (*specialized options for SPASS*) ref ["Auto=0","-FullRed=0","-IORe","-IOFc","-RTaut","-RFSub","-RBSub", "-DocProof","-TimeLimit=60"]; diff -r de60322ff13a -r d16c3a62c396 src/HOL/Tools/res_axioms.ML --- a/src/HOL/Tools/res_axioms.ML Thu Sep 15 10:33:35 2005 +0200 +++ b/src/HOL/Tools/res_axioms.ML Thu Sep 15 11:15:52 2005 +0200 @@ -8,18 +8,17 @@ signature RES_AXIOMS = sig exception ELIMR2FOL of string + val tagging_enabled : bool val elimRule_tac : thm -> Tactical.tactic val elimR2Fol : thm -> term val transform_elim : thm -> thm val clausify_axiom_pairs : (string*thm) -> (ResClause.clause*thm) list val cnf_axiom : (string * thm) -> thm list val meta_cnf_axiom : thm -> thm list - val cnf_rule : thm -> thm list - val cnf_rules : (string*thm) list -> thm list -> thm list list * thm list val rm_Eps : (term * term) list -> thm list -> term list val claset_rules_of_thy : theory -> (string * thm) list val simpset_rules_of_thy : theory -> (string * thm) list - val clausify_rules_pairs : (string * thm) list -> thm list -> (ResClause.clause * thm) list list * thm list + val clausify_rules_pairs : (string*thm) list -> thm list -> (ResClause.clause*thm) list list * thm list val clause_setup : (theory -> theory) list val meson_method_setup : (theory -> theory) list end; @@ -28,6 +27,8 @@ struct +val tagging_enabled = false (*compile_time option*) + (**** Transformation of Elimination Rules into First-Order Formulas****) (* a tactic used to prove an elim-rule. *) @@ -133,8 +134,6 @@ (**** Transformation of Clasets and Simpsets into First-Order Axioms ****) -(* to be fixed: cnf_intro, cnf_rule, is_introR *) - (* repeated resolution *) fun repeat_RS thm1 thm2 = let val thm1' = thm1 RS thm2 handle THM _ => thm1 @@ -182,7 +181,7 @@ (*Traverse a term, accumulating Skolem function definitions.*) fun declare_skofuns s t thy = - let fun dec_sko (Const ("Ex",_) $ (xtp as Abs(_,T,p))) (n, thy) = + let fun dec_sko (Const ("Ex",_) $ (xtp as Abs(_,T,p))) (n, (thy, axs)) = (*Existential: declare a Skolem function, then insert into body and continue*) let val cname = s ^ "_" ^ Int.toString n val args = term_frees xtp (*get the formal parameter list*) @@ -194,20 +193,25 @@ val def = equals cT $ c $ rhs val thy' = Theory.add_consts_i [(cname, cT, NoSyn)] thy (*Theory is augmented with the constant, then its def*) - val thy'' = Theory.add_defs_i false [(cname ^ "_def", def)] thy' - in dec_sko (subst_bound (list_comb(c,args), p)) (n+1, thy'') end - | dec_sko (Const ("All",_) $ (xtp as Abs(a,T,p))) (n, thy) = + val cdef = cname ^ "_def" + val thy'' = Theory.add_defs_i false [(cdef, def)] thy' + in dec_sko (subst_bound (list_comb(c,args), p)) + (n+1, (thy'', get_axiom thy'' cdef :: axs)) + end + | dec_sko (Const ("All",_) $ (xtp as Abs(a,T,p))) (n, thx) = (*Universal quant: insert a free variable into body and continue*) let val fname = variant (add_term_names (p,[])) a - in dec_sko (subst_bound (Free(fname,T), p)) (n, thy) end + in dec_sko (subst_bound (Free(fname,T), p)) (n, thx) end | dec_sko (Const ("op &", _) $ p $ q) nthy = dec_sko q (dec_sko p nthy) | dec_sko (Const ("op |", _) $ p $ q) nthy = dec_sko q (dec_sko p nthy) + | dec_sko (Const ("HOL.tag", _) $ p) nthy = + dec_sko p nthy | dec_sko (Const ("Trueprop", _) $ p) nthy = dec_sko p nthy - | dec_sko t (n,thy) = (n,thy) (*Do nothing otherwise*) - in #2 (dec_sko t (1,thy)) end; + | dec_sko t nthx = nthx (*Do nothing otherwise*) + in #2 (dec_sko t (1, (thy,[]))) end; (*cterms are used throughout for efficiency*) val cTrueprop = Thm.cterm_of (Theory.sign_of HOL.thy) HOLogic.Trueprop; @@ -251,8 +255,8 @@ (*Declare Skolem functions for a theorem, supplied in nnf and with its name*) fun skolem thy (name,th) = let val cname = (case name of "" => gensym "sko" | s => Sign.base_name s) - val thy' = declare_skofuns cname (#prop (rep_thm th)) thy - in (map (skolem_of_def o #2) (axioms_of thy'), thy') end; + val (thy',axs) = declare_skofuns cname (#prop (rep_thm th)) thy + in (map skolem_of_def axs, thy') end; (*Populate the clause cache using the supplied theorems*) fun skolemlist [] thy = thy @@ -313,18 +317,15 @@ (sk_term,(t,sk_term)::epss) end; - +(*FIXME: use a-list lookup!!*) fun sk_lookup [] t = NONE | sk_lookup ((tm,sk_tm)::tms) t = if (t = tm) then SOME (sk_tm) else (sk_lookup tms t); - - (* get the proper skolem term to replace epsilon term *) fun get_skolem epss t = case (sk_lookup epss t) of NONE => get_new_skolem epss t | SOME sk => (sk,epss); - fun rm_Eps_cls_aux epss (t as (Const ("Hilbert_Choice.Eps",_) $ Abs(_,_,_))) = get_skolem epss t | rm_Eps_cls_aux epss (P $ Q) = @@ -333,11 +334,9 @@ in (P' $ Q',epss'') end | rm_Eps_cls_aux epss t = (t,epss); - fun rm_Eps_cls epss th = rm_Eps_cls_aux epss (prop_of th); - -(* remove the epsilon terms in a formula, by skolem terms. *) +(* replace the epsilon terms in a formula by skolem terms. *) fun rm_Eps _ [] = [] | rm_Eps epss (th::thms) = let val (th',epss') = rm_Eps_cls epss th @@ -347,15 +346,26 @@ (**** Extract and Clausify theorems from a theory's claset and simpset ****) +(*Preserve the name of "th" after the transformation "f"*) +fun preserve_name f th = Thm.name_thm (Thm.name_of_thm th, f th); + +(*Tags identify the major premise or conclusion, as hints to resolution provers. + However, they don't appear to help in recent tests, and they complicate the code.*) +val tagI = thm "tagI"; +val tagD = thm "tagD"; + +val tag_intro = preserve_name (fn th => th RS tagI); +val tag_elim = preserve_name (fn th => tagD RS th); + fun claset_rules_of_thy thy = - let val clsset = rep_cs (claset_of thy) - val safeEs = #safeEs clsset - val safeIs = #safeIs clsset - val hazEs = #hazEs clsset - val hazIs = #hazIs clsset - in - map pairname (safeEs @ safeIs @ hazEs @ hazIs) - end; + let val cs = rep_cs (claset_of thy) + val intros = (#safeIs cs) @ (#hazIs cs) + val elims = (#safeEs cs) @ (#hazEs cs) + in + if tagging_enabled + then map pairname (map tag_intro intros @ map tag_elim elims) + else map pairname (intros @ elims) + end; fun simpset_rules_of_thy thy = let val rules = #rules (fst (rep_ss (simpset_of thy))) @@ -368,31 +378,40 @@ fun cnf_rules [] err_list = ([],err_list) | cnf_rules ((name,th) :: thms) err_list = let val (ts,es) = cnf_rules thms err_list - in (cnf_axiom (name,th) :: ts,es) handle _ => (ts, (th::es)) end; (* FIXME avoid handle _ *) + in (cnf_axiom (name,th) :: ts,es) handle _ => (ts, (th::es)) end; (**** Convert all theorems of a claset/simpset into clauses (ResClause.clause) ****) +fun addclause (c,th) l = + if ResClause.isTaut c then l else (c,th) :: l; + (* outputs a list of (clause,thm) pairs *) fun clausify_axiom_pairs (thm_name,thm) = - let val isa_clauses = cnf_axiom (thm_name,thm) (*"isa_clauses" are already "standard"ed. *) + let val isa_clauses = cnf_axiom (thm_name,thm) val isa_clauses' = rm_Eps [] isa_clauses val clauses_n = length isa_clauses - val thy = theory_of_thm thm fun make_axiom_clauses _ [] []= [] | make_axiom_clauses i (cls::clss) (cls'::clss') = - (ResClause.make_axiom_clause cls (thm_name,i), cls') :: - make_axiom_clauses (i+1) clss clss' + addclause (ResClause.make_axiom_clause cls (thm_name,i), cls') + (make_axiom_clauses (i+1) clss clss') in make_axiom_clauses 0 isa_clauses' isa_clauses - end; + end fun clausify_rules_pairs [] err_list = ([],err_list) | clausify_rules_pairs ((name,thm)::thms) err_list = let val (ts,es) = clausify_rules_pairs thms err_list in ((clausify_axiom_pairs (name,thm))::ts, es) - handle _ => (ts, (thm::es)) (* FIXME avoid handle _ *) + handle THM (msg,_,_) => + (debug ("Cannot clausify " ^ name ^ ": " ^ msg); + (ts, (thm::es))) + | ResClause.CLAUSE (msg,t) => + (debug ("Cannot clausify " ^ name ^ ": " ^ msg ^ + ": " ^ TermLib.string_of_term t); + (ts, (thm::es))) + end; diff -r de60322ff13a -r d16c3a62c396 src/HOL/Tools/res_clause.ML --- a/src/HOL/Tools/res_clause.ML Thu Sep 15 10:33:35 2005 +0200 +++ b/src/HOL/Tools/res_clause.ML Thu Sep 15 11:15:52 2005 +0200 @@ -10,49 +10,49 @@ (* works for writeoutclasimp on typed *) signature RES_CLAUSE = sig - exception ARCLAUSE of string - exception CLAUSE of string - type arityClause - type classrelClause - val classrelClauses_of : string * string list -> classrelClause list - type clause - val init : theory -> unit - val keep_types : bool ref - val make_axiom_arity_clause : - string * (string * string list list) -> arityClause - val make_axiom_classrelClause : - string * string option -> classrelClause - val make_axiom_clause : Term.term -> string * int -> clause - val make_conjecture_clause : Term.term -> clause - val make_conjecture_clause_thm : Thm.thm -> clause - val make_hypothesis_clause : Term.term -> clause - val special_equal : bool ref - val get_axiomName : clause -> string - val typed : unit -> unit - val untyped : unit -> unit - val num_of_clauses : clause -> int + val keep_types : bool ref + val special_equal : bool ref + val tagged : bool ref + + exception ARCLAUSE of string + exception CLAUSE of string * term + type arityClause + type classrelClause + val classrelClauses_of : string * string list -> classrelClause list + type clause + val init : theory -> unit + val make_axiom_arity_clause : + string * (string * string list list) -> arityClause + val make_axiom_classrelClause : string * string option -> classrelClause + val make_axiom_clause : Term.term -> string * int -> clause + val make_conjecture_clause : Term.term -> clause + val make_conjecture_clause_thm : Thm.thm -> clause + val make_hypothesis_clause : Term.term -> clause + val get_axiomName : clause -> string + val isTaut : clause -> bool + val num_of_clauses : clause -> int - val dfg_clauses2str : string list -> string - val clause2dfg : clause -> string * string list - val clauses2dfg : clause list -> string -> clause list -> clause list -> - (string * int) list -> (string * int) list -> string list -> string - val tfree_dfg_clause : string -> string + val dfg_clauses2str : string list -> string + val clause2dfg : clause -> string * string list + val clauses2dfg : clause list -> string -> clause list -> clause list -> + (string * int) list -> (string * int) list -> string list -> string + val tfree_dfg_clause : string -> string - val tptp_arity_clause : arityClause -> string - val tptp_classrelClause : classrelClause -> string - val tptp_clause : clause -> string list - val tptp_clauses2str : string list -> string - val clause2tptp : clause -> string * string list - val tfree_clause : string -> string - val schematic_var_prefix : string - val fixed_var_prefix : string - val tvar_prefix : string - val tfree_prefix : string - val clause_prefix : string - val arclause_prefix : string - val const_prefix : string - val tconst_prefix : string - val class_prefix : string + val tptp_arity_clause : arityClause -> string + val tptp_classrelClause : classrelClause -> string + val tptp_clause : clause -> string list + val tptp_clauses2str : string list -> string + val clause2tptp : clause -> string * string list + val tfree_clause : string -> string + val schematic_var_prefix : string + val fixed_var_prefix : string + val tvar_prefix : string + val tfree_prefix : string + val clause_prefix : string + val arclause_prefix : string + val const_prefix : string + val tconst_prefix : string + val class_prefix : string end; structure ResClause: RES_CLAUSE = @@ -157,9 +157,6 @@ (***** definitions and functions for FOL clauses, prepared for conversion into TPTP format or SPASS format. *****) val keep_types = ref true; -fun untyped () = (keep_types := false); -fun typed () = (keep_types := true); - datatype kind = Axiom | Hypothesis | Conjecture; fun name_of_kind Axiom = "axiom" @@ -189,7 +186,6 @@ (**** Isabelle FOL clauses ****) -(* by default it is false *) val tagged = ref false; type pred_name = string; @@ -223,7 +219,7 @@ functions: (string*int) list}; -exception CLAUSE of string; +exception CLAUSE of string * term; (*** make clauses ***) @@ -233,6 +229,13 @@ (not pol andalso a = "c_True") | isFalse _ = false; +fun isTrue (Literal (pol,Predicate(a,_,[]),_)) = + (pol andalso a = "c_True") orelse + (not pol andalso a = "c_False") + | isTrue _ = false; + +fun isTaut (Clause {literals,...}) = exists isTrue literals; + fun make_clause (clause_id,axiom_name,kind,literals, types_sorts,tvar_type_literals, tfree_type_literals,tvars, predicates, functions) = @@ -303,10 +306,10 @@ let val (typof,(folTyps,funcs)) = maybe_type_of c T in (make_fixed_const c, (typof,folTyps), funcs) end | pred_name_type (Free(x,T)) = - if isMeta x then raise CLAUSE("Predicate Not First Order") + if isMeta x then raise CLAUSE("Predicate Not First Order 1", Free(x,T)) else (make_fixed_var x, ("",[]), []) - | pred_name_type (Var(_,_)) = raise CLAUSE("Predicate Not First Order") - | pred_name_type _ = raise CLAUSE("Predicate input unexpected"); + | pred_name_type (v as Var _) = raise CLAUSE("Predicate Not First Order 2", v) + | pred_name_type t = raise CLAUSE("Predicate input unexpected", t); (* For type equality *) @@ -330,7 +333,7 @@ in (t, ("",[]), [(t, length args)]) end - | fun_name_type _ args = raise CLAUSE("Function Not First Order"); + | fun_name_type f args = raise CLAUSE("Function Not First Order 1", f); fun term_of (Var(ind_nm,T)) = @@ -339,17 +342,19 @@ (UVar(make_schematic_var ind_nm, folType), (ts, funcs)) end | term_of (Free(x,T)) = - let val (folType,(ts, funcs)) = type_of T + let val (folType, (ts,funcs)) = type_of T in if isMeta x then (UVar(make_schematic_var(x,0),folType), (ts, ((make_schematic_var(x,0)),0)::funcs)) else - (Fun(make_fixed_var x,folType,[]), (ts, ((make_fixed_var x),0)::funcs)) + (Fun(make_fixed_var x, folType, []), + (ts, ((make_fixed_var x),0)::funcs)) end | term_of (Const(c,T)) = (* impossible to be equality *) let val (folType,(ts,funcs)) = type_of T - in - (Fun(make_fixed_const c,folType,[]),(ts, ((make_fixed_const c),0)::funcs)) + in + (Fun(make_fixed_const c, folType, []), + (ts, ((make_fixed_const c),0)::funcs)) end | term_of (app as (t $ a)) = let val (f,args) = strip_comb app @@ -360,7 +365,7 @@ val ts3 = ResLib.flat_noDup (ts1::ts2) val funcs'' = ResLib.flat_noDup((funcs::funcs')) in - (Fun(funName,funType,args'),(ts3,funcs'')) + (Fun(funName,funType,args'), (ts3,funcs'')) end fun term_of_eq ((Const ("op =", typ)),args) = let val arg_typ = eq_arg_type typ @@ -370,60 +375,58 @@ in (Fun(equal_name,arg_typ,args'), (ResLib.flat_noDup ts, - (((make_fixed_var equal_name),2):: ResLib.flat_noDup funcs))) + (make_fixed_var equal_name, 2):: ResLib.flat_noDup funcs)) end in - case f of Const ("op =", typ) => term_of_eq (f,args) - | Const(_,_) => term_of_aux () - | Free(s,_) => if isMeta s - then raise CLAUSE("Function Not First Order") - else term_of_aux() - | _ => raise CLAUSE("Function Not First Order") + case f of Const ("op =", typ) => term_of_eq (f,args) + | Const(_,_) => term_of_aux () + | Free(s,_) => + if isMeta s + then raise CLAUSE("Function Not First Order 2", f) + else term_of_aux() + | _ => raise CLAUSE("Function Not First Order 3", f) end - | term_of _ = raise CLAUSE("Function Not First Order"); + | term_of t = raise CLAUSE("Function Not First Order 4", t); -fun pred_of_eq ((Const ("op =", typ)),args) = - let val arg_typ = eq_arg_type typ - val (args',ts_funcs) = ListPair.unzip (map term_of args) - val (ts,funcs) = ListPair.unzip ts_funcs - val equal_name = make_fixed_const "op =" - in - (Predicate(equal_name,arg_typ,args'), - ResLib.flat_noDup ts, - [((make_fixed_var equal_name), 2)], - (ResLib.flat_noDup funcs)) - end; - -(* The input "pred" cannot be an equality *) -fun pred_of_nonEq (pred,args) = - let val (predName,(predType,ts1), pfuncs) = pred_name_type pred - val (args',ts_funcs) = ListPair.unzip (map term_of args) - val (ts2,ffuncs) = ListPair.unzip ts_funcs - val ts3 = ResLib.flat_noDup (ts1::ts2) - val ffuncs' = (ResLib.flat_noDup ffuncs) - val newfuncs = distinct (pfuncs@ffuncs') - val arity = - case pred of - Const (c,_) => - if !keep_types andalso not (no_types_needed c) - then 1 + length args - else length args - | _ => length args - in - (Predicate(predName,predType,args'), ts3, - [(predName, arity)], newfuncs) - end; +fun pred_of (Const("op =", typ), args) = + let val arg_typ = eq_arg_type typ + val (args',ts_funcs) = ListPair.unzip (map term_of args) + val (ts,funcs) = ListPair.unzip ts_funcs + val equal_name = make_fixed_const "op =" + in + (Predicate(equal_name,arg_typ,args'), + ResLib.flat_noDup ts, + [((make_fixed_var equal_name), 2)], + (ResLib.flat_noDup funcs)) + end + | pred_of (pred,args) = + let val (predName,(predType,ts1), pfuncs) = pred_name_type pred + val (args',ts_funcs) = ListPair.unzip (map term_of args) + val (ts2,ffuncs) = ListPair.unzip ts_funcs + val ts3 = ResLib.flat_noDup (ts1::ts2) + val ffuncs' = (ResLib.flat_noDup ffuncs) + val newfuncs = distinct (pfuncs@ffuncs') + val arity = + case pred of + Const (c,_) => + if !keep_types andalso not (no_types_needed c) + then 1 + length args + else length args + | _ => length args + in + (Predicate(predName,predType,args'), ts3, + [(predName, arity)], newfuncs) + end; -(* Changed for typed equality *) -(* First check if the predicate is an equality or not, then call different functions for equality and non-equalities *) -fun predicate_of term = - let val (pred,args) = strip_comb term - in - case pred of (Const ("op =", _)) => pred_of_eq (pred,args) - | _ => pred_of_nonEq (pred,args) - end; +(*Treatment of literals, possibly negated or tagged*) +fun predicate_of ((Const("Not",_) $ P), polarity, tag) = + predicate_of (P, not polarity, tag) + | predicate_of ((Const("HOL.tag",_) $ P), polarity, tag) = + predicate_of (P, polarity, true) + | predicate_of (term,polarity,tag) = + (pred_of (strip_comb term), polarity, tag); fun literals_of_term ((Const("Trueprop",_) $ P),lits_ts, preds, funcs) = literals_of_term(P,lits_ts, preds, funcs) @@ -434,16 +437,10 @@ literals_of_term(Q, (lits',ts'), distinct(preds'@preds), distinct(funcs'@funcs)) end - | literals_of_term ((Const("Not",_) $ P),(lits,ts), preds, funcs) = - let val (pred,ts', preds', funcs') = predicate_of P - val lits' = Literal(false,pred,false) :: lits - val ts'' = ResLib.no_rep_app ts ts' - in - (lits',ts'', distinct(preds'@preds), distinct(funcs'@funcs)) - end | literals_of_term (P,(lits,ts), preds, funcs) = - let val (pred,ts', preds', funcs') = predicate_of P - val lits' = Literal(true,pred,false) :: lits + let val ((pred,ts', preds', funcs'), pol, tag) = + predicate_of (P,true,false) + val lits' = Literal(pol,pred,tag) :: lits val ts'' = ResLib.no_rep_app ts ts' in (lits',ts'', distinct(preds'@preds), distinct(funcs'@funcs)) @@ -759,27 +756,24 @@ end -fun get_uvars (UVar(str,typ)) = [str] -| get_uvars (Fun (str,typ,tlist)) = ResLib.flat_noDup(map get_uvars tlist) - - -fun is_uvar (UVar(str,typ)) = true -| is_uvar (Fun (str,typ,tlist)) = false; - -fun uvar_name (UVar(str,typ)) = str -| uvar_name _ = (raise CLAUSE("Not a variable")); +fun get_uvars (UVar(a,typ)) = [a] +| get_uvars (Fun (_,typ,tlist)) = ResLib.flat_noDup(map get_uvars tlist) +fun is_uvar (UVar _) = true +| is_uvar (Fun _) = false; + +fun uvar_name (UVar(a,_)) = a +| uvar_name (Fun (a,_,_)) = raise CLAUSE("Not a variable", Const(a,dummyT)); + fun mergelist [] = [] -| mergelist (x::xs ) = x@(mergelist xs) - +| mergelist (x::xs ) = x @ mergelist xs fun dfg_vars (Clause cls) = - let val lits = (#literals cls) + let val lits = #literals cls val folterms = mergelist(map dfg_folterms lits) - val vars = ResLib.flat_noDup(map get_uvars folterms) in - vars + ResLib.flat_noDup(map get_uvars folterms) end