src/HOL/Tools/res_atp.ML
changeset 19227 d15f2baa7ecc
parent 19205 4ec788c69f82
child 19352 1a07f6cf1e6c
     1.1 --- a/src/HOL/Tools/res_atp.ML	Wed Mar 08 21:40:46 2006 +0100
     1.2 +++ b/src/HOL/Tools/res_atp.ML	Thu Mar 09 06:05:01 2006 +0100
     1.3 @@ -34,6 +34,14 @@
     1.4    val hol_typ_level: unit -> ResHolClause.type_level
     1.5    val run_relevance_filter: bool ref
     1.6    val invoke_atp_ml : ProofContext.context * thm -> unit
     1.7 +  val add_claset : unit -> unit
     1.8 +  val add_simpset : unit -> unit
     1.9 +  val add_clasimp : unit -> unit
    1.10 +  val add_atpset : unit -> unit
    1.11 +  val rm_claset : unit -> unit
    1.12 +  val rm_simpset : unit -> unit
    1.13 +  val rm_atpset : unit -> unit
    1.14 +  val rm_clasimp : unit -> unit
    1.15  end;
    1.16  
    1.17  structure ResAtp : RES_ATP =
    1.18 @@ -117,11 +125,11 @@
    1.19  val include_atpset = ref true;
    1.20  val add_simpset = (fn () => include_simpset:=true);
    1.21  val add_claset = (fn () => include_claset:=true);
    1.22 -val add_clasimp = (fn () => include_simpset:=true;include_claset:=true);
    1.23 +val add_clasimp = (fn () => (include_simpset:=true;include_claset:=true));
    1.24  val add_atpset = (fn () => include_atpset:=true);
    1.25  val rm_simpset = (fn () => include_simpset:=false);
    1.26  val rm_claset = (fn () => include_claset:=false);
    1.27 -val rm_clasimp = (fn () => include_simpset:=false;include_claset:=false);
    1.28 +val rm_clasimp = (fn () => (include_simpset:=false;include_claset:=false));
    1.29  val rm_atpset = (fn () => include_atpset:=false);
    1.30  
    1.31  (*** paths for HOL helper files ***)
    1.32 @@ -268,39 +276,41 @@
    1.33      let val (pred,args) = strip_comb P
    1.34  	val (lg',seen') = if pred mem seen then (lg,seen) 
    1.35  			  else pred_lg pred (lg,seen)
    1.36 +	val _ = if is_fol_logic lg' then () else warning ("Found a HOL predicate: " ^ (Term.str_of_term pred))
    1.37      in
    1.38  	term_lg args (lg',seen')
    1.39      end;
    1.40  
    1.41  fun lits_lg [] (lg,seen) = (lg,seen)
    1.42    | lits_lg (lit::lits) (FOL,seen) =
    1.43 -    lits_lg lits (lit_lg lit (FOL,seen))
    1.44 +    let val (lg,seen') = lit_lg lit (FOL,seen)
    1.45 +	val _ =  if is_fol_logic lg then () else warning ("Found a HOL literal: " ^ (Term.str_of_term lit))
    1.46 +    in
    1.47 +	lits_lg lits (lg,seen')
    1.48 +    end
    1.49    | lits_lg lits (lg,seen) = (lg,seen);
    1.50  
    1.51  
    1.52 +fun dest_disj_aux (Const ("op |", _) $ t $ t') disjs = 
    1.53 +    dest_disj_aux t (dest_disj_aux t' disjs)
    1.54 +  | dest_disj_aux t disjs = t::disjs;
    1.55 +
    1.56 +fun dest_disj t = dest_disj_aux t [];
    1.57 +
    1.58  fun logic_of_clause tm (lg,seen) =
    1.59      let val tm' = HOLogic.dest_Trueprop tm
    1.60 -	val disjs = HOLogic.dest_disj tm'
    1.61 -    in
    1.62 -	lits_lg disjs (lg,seen)
    1.63 -    end;
    1.64 -
    1.65 -fun lits_lg [] (lg,seen) = (lg,seen)
    1.66 -  | lits_lg (lit::lits) (FOL,seen) =
    1.67 -    lits_lg lits (lit_lg lit (FOL,seen))
    1.68 -  | lits_lg lits (lg,seen) = (lg,seen);
    1.69 -
    1.70 -
    1.71 -fun logic_of_clause tm (lg,seen) =
    1.72 -    let val tm' = HOLogic.dest_Trueprop tm
    1.73 -	val disjs = HOLogic.dest_disj tm'
    1.74 +	val disjs = dest_disj tm'
    1.75      in
    1.76  	lits_lg disjs (lg,seen)
    1.77      end;
    1.78  
    1.79  fun logic_of_clauses [] (lg,seen) = (lg,seen)
    1.80    | logic_of_clauses (cls::clss) (FOL,seen) =
    1.81 -    logic_of_clauses clss (logic_of_clause cls (FOL,seen))
    1.82 +    let val (lg,seen') = logic_of_clause cls (FOL,seen)
    1.83 +	val _ = if is_fol_logic lg then () else warning ("Found a HOL clause: " ^ (Term.str_of_term cls))
    1.84 +    in
    1.85 +	logic_of_clauses clss (lg,seen')
    1.86 +    end
    1.87    | logic_of_clauses (cls::clss) (lg,seen) = (lg,seen);
    1.88  
    1.89  fun logic_of_nclauses [] (lg,seen) = (lg,seen)