src/HOL/Tools/res_clause.ML
changeset 18869 00741f7280f7
parent 18868 7cfc21ee0370
child 18920 7635e0060cd4
     1.1 --- a/src/HOL/Tools/res_clause.ML	Tue Jan 31 16:37:06 2006 +0100
     1.2 +++ b/src/HOL/Tools/res_clause.ML	Tue Jan 31 17:48:28 2006 +0100
     1.3 @@ -45,7 +45,6 @@
     1.4    val make_type_class : string -> string
     1.5    val mk_fol_type: string * string * fol_type list -> fol_type
     1.6    val mk_typ_var_sort : Term.typ -> typ_var * sort
     1.7 -  val num_of_clauses : clause -> int
     1.8    val paren_pack : string list -> string
     1.9    val schematic_var_prefix : string
    1.10    val special_equal : bool ref
    1.11 @@ -190,7 +189,7 @@
    1.12  
    1.13  type polarity = bool;
    1.14  
    1.15 -(* "tag" is used for vampire specific syntax  *)
    1.16 +(* "tag" is used for vampire specific syntax FIXME REMOVE *)
    1.17  type tag = bool; 
    1.18  
    1.19  
    1.20 @@ -236,9 +235,9 @@
    1.21  		    axiom_name: axiom_name,
    1.22  		    kind: kind,
    1.23  		    literals: literal list,
    1.24 -		    types_sorts: (typ_var * sort) list, 
    1.25 -                    tvar_type_literals: type_literal list, 
    1.26 -                    tfree_type_literals: type_literal list};
    1.27 +		    types_sorts: (typ_var * sort) list};
    1.28 +
    1.29 +fun get_axiomName (Clause cls) = #axiom_name cls;
    1.30  
    1.31  exception CLAUSE of string * term;
    1.32  
    1.33 @@ -254,24 +253,12 @@
    1.34    
    1.35  fun isTaut (Clause {literals,...}) = exists isTrue literals;  
    1.36  
    1.37 -fun make_clause (clause_id,axiom_name,kind,literals,
    1.38 -                 types_sorts,tvar_type_literals,tfree_type_literals) =
    1.39 +fun make_clause (clause_id, axiom_name, kind, literals, types_sorts) =
    1.40    if forall isFalse literals 
    1.41    then error "Problem too trivial for resolution (empty clause)"
    1.42    else
    1.43       Clause {clause_id = clause_id, axiom_name = axiom_name, kind = kind, 
    1.44 -             literals = literals, types_sorts = types_sorts,
    1.45 -             tvar_type_literals = tvar_type_literals,
    1.46 -             tfree_type_literals = tfree_type_literals};
    1.47 -
    1.48 -
    1.49 -(** Some Clause destructor functions **)
    1.50 -
    1.51 -fun string_of_kind (Clause cls) = name_of_kind (#kind cls);
    1.52 -
    1.53 -fun get_axiomName (Clause cls) = #axiom_name cls;
    1.54 -
    1.55 -fun get_clause_id (Clause cls) = #clause_id cls;
    1.56 +             literals = literals, types_sorts = types_sorts};
    1.57  
    1.58  
    1.59  (*Declarations of the current theory--to allow suppressing types.*)
    1.60 @@ -588,10 +575,7 @@
    1.61        end;
    1.62  
    1.63  
    1.64 -fun add_typs (Clause cls) = add_typs_aux (#types_sorts cls)  
    1.65 -
    1.66 -
    1.67 -(** make axiom clauses, hypothesis clauses and conjecture clauses. **)
    1.68 +(** make axiom and conjecture clauses. **)
    1.69  
    1.70  fun get_tvar_strs [] = []
    1.71    | get_tvar_strs ((FOLTVar indx,s)::tss) = 
    1.72 @@ -603,23 +587,18 @@
    1.73  
    1.74  fun make_axiom_clause_thm thm (ax_name,cls_id) =
    1.75      let val (lits,types_sorts) = literals_of_term (prop_of thm)
    1.76 -	val lits' = sort_lits lits
    1.77 -	val (tvar_lits,tfree_lits) = add_typs_aux types_sorts  
    1.78      in 
    1.79 -	make_clause(cls_id,ax_name,Axiom,
    1.80 -	            lits',types_sorts,tvar_lits,tfree_lits)
    1.81 +	make_clause(cls_id, ax_name, Axiom, sort_lits lits, types_sorts)
    1.82      end;
    1.83  
    1.84  
    1.85 -(* check if a clause is FOL first*)
    1.86 +(* check if a clause is first-order before making a conjecture clause*)
    1.87  fun make_conjecture_clause n t =
    1.88      let val _ = check_is_fol_term t
    1.89  	    handle TERM("check_is_fol_term",_) => raise CLAUSE("Goal is not FOL",t)
    1.90  	val (lits,types_sorts) = literals_of_term t
    1.91 -	val (tvar_lits,tfree_lits) = add_typs_aux types_sorts 
    1.92      in
    1.93 -	make_clause(n,"conjecture",Conjecture,
    1.94 -	            lits,types_sorts,tvar_lits,tfree_lits)
    1.95 +	make_clause(n, "conjecture", Conjecture, lits, types_sorts)
    1.96      end;
    1.97      
    1.98  fun make_conjecture_clauses_aux _ [] = []
    1.99 @@ -635,10 +614,8 @@
   1.100  	    handle TERM("check_is_fol_term",_) => raise CLAUSE("Axiom is not FOL", term) 
   1.101  	val (lits,types_sorts) = literals_of_term term
   1.102  	val lits' = sort_lits lits
   1.103 -	val (tvar_lits,tfree_lits) = add_typs_aux types_sorts
   1.104      in 
   1.105 -	make_clause(cls_id,ax_name,Axiom,
   1.106 -	            lits',types_sorts,tvar_lits,tfree_lits)
   1.107 +	make_clause(cls_id, ax_name, Axiom, sort_lits lits, types_sorts)
   1.108      end;
   1.109  
   1.110  
   1.111 @@ -684,14 +661,6 @@
   1.112                     conclLit = make_TConsLit(true, (res,tcons,tvars)), 
   1.113                     premLits = map make_TVarLit false_tvars_srts'}
   1.114     end;
   1.115 -    
   1.116 -(*The number of clauses generated from cls, including type clauses. It's always 1
   1.117 -  except for conjecture clauses.*)
   1.118 -fun num_of_clauses (Clause cls) =
   1.119 -    let val num_tfree_lits = 
   1.120 -	      if !keep_types then length (#tfree_type_literals cls)
   1.121 -	      else 0
   1.122 -    in 	1 + num_tfree_lits  end;
   1.123  
   1.124  
   1.125  (**** Isabelle class relations ****)
   1.126 @@ -873,14 +842,13 @@
   1.127      dfg_forall vars ("or(" ^ lits ^ ")") ^ ",\n" ^ 
   1.128      string_of_clausename (cls_id,ax_name) ^  ").\n\n";
   1.129  
   1.130 -fun dfg_clause_aux (Clause{literals, tvar_type_literals, tfree_type_literals, ...}) = 
   1.131 +fun dfg_clause_aux (Clause{literals, types_sorts, ...}) = 
   1.132    let val lits = map dfg_literal literals
   1.133 +      val (tvar_lits,tfree_lits) = add_typs_aux types_sorts
   1.134        val tvar_lits_strs = 
   1.135 -	  if !keep_types then map dfg_of_typeLit tvar_type_literals
   1.136 -	  else []
   1.137 +	  if !keep_types then map dfg_of_typeLit tvar_lits else []
   1.138        val tfree_lits =
   1.139 -          if !keep_types then map dfg_of_typeLit tfree_type_literals
   1.140 -          else []
   1.141 +          if !keep_types then map dfg_of_typeLit tfree_lits else []
   1.142    in
   1.143        (tvar_lits_strs @ lits, tfree_lits)
   1.144    end; 
   1.145 @@ -985,10 +953,7 @@
   1.146    end;
   1.147  
   1.148  
   1.149 -(********************************)
   1.150 -(* code to produce TPTP files   *)
   1.151 -(********************************)
   1.152 -
   1.153 +(**** Produce TPTP files ****)
   1.154  
   1.155  (*Attach sign in TPTP syntax: false means negate.*)
   1.156  fun tptp_sign true s = "++" ^ s
   1.157 @@ -1006,7 +971,6 @@
   1.158  fun tptp_of_typeLit (LTVar (s,ty)) = "--" ^ s ^ "(" ^ ty ^ ")"
   1.159    | tptp_of_typeLit (LTFree (s,ty)) = "++" ^ s ^ "(" ^ ty ^ ")";
   1.160   
   1.161 -
   1.162  fun gen_tptp_cls (cls_id,ax_name,knd,lits) = 
   1.163      "input_clause(" ^ string_of_clausename (cls_id,ax_name) ^ "," ^ 
   1.164      knd ^ "," ^ lits ^ ").\n";
   1.165 @@ -1015,53 +979,29 @@
   1.166      "input_clause(" ^ string_of_type_clsname (cls_id,ax_name,idx) ^ "," ^ 
   1.167      knd ^ ",[" ^ tfree_lit ^ "]).\n";
   1.168  
   1.169 -fun tptp_type_lits (Clause cls) = 
   1.170 -    let val lits = map tptp_literal (#literals cls)
   1.171 -	val tvar_lits_strs =
   1.172 -	      if !keep_types 
   1.173 -	      then (map tptp_of_typeLit (#tvar_type_literals cls)) 
   1.174 -	      else []
   1.175 -	val tfree_lits = 
   1.176 -	      if !keep_types
   1.177 -	      then (map tptp_of_typeLit (#tfree_type_literals cls)) 
   1.178 -	      else []
   1.179 +fun tptp_type_lits (Clause {literals, types_sorts, ...}) = 
   1.180 +    let val lits = map tptp_literal literals
   1.181 +	val (tvar_lits,tfree_lits) = add_typs_aux types_sorts
   1.182 +        val tvar_lits_strs =
   1.183 +            if !keep_types then map tptp_of_typeLit tvar_lits else []
   1.184 +	val tfree_lits =
   1.185 +	    if !keep_types then map tptp_of_typeLit tfree_lits else []
   1.186      in
   1.187  	(tvar_lits_strs @ lits, tfree_lits)
   1.188      end; 
   1.189  
   1.190 -fun tptp_clause cls =
   1.191 +fun clause2tptp (cls as Clause {clause_id, axiom_name, kind, ...}) =
   1.192      let val (lits,tfree_lits) = tptp_type_lits cls 
   1.193              (*"lits" includes the typing assumptions (TVars)*)
   1.194 -	val cls_id = get_clause_id cls
   1.195 -	val ax_name = get_axiomName cls
   1.196 -	val knd = string_of_kind cls
   1.197 -	val lits_str = bracket_pack lits
   1.198 -	val cls_str = gen_tptp_cls(cls_id,ax_name,knd,lits_str) 			 
   1.199 -	fun typ_clss k [] = []
   1.200 -          | typ_clss k (tfree :: tfrees) = 
   1.201 -              gen_tptp_type_cls(cls_id,ax_name,knd,tfree,k) :: 
   1.202 -              typ_clss (k+1) tfrees
   1.203 -    in 
   1.204 -	cls_str :: (typ_clss 0 tfree_lits)
   1.205 -    end;
   1.206 -
   1.207 -fun clause2tptp cls =
   1.208 -    let val (lits,tfree_lits) = tptp_type_lits cls 
   1.209 -            (*"lits" includes the typing assumptions (TVars)*)
   1.210 -	val cls_id = get_clause_id cls
   1.211 -	val ax_name = get_axiomName cls
   1.212 -	val knd = string_of_kind cls
   1.213 -	val lits_str = bracket_pack lits
   1.214 -	val cls_str = gen_tptp_cls(cls_id,ax_name,knd,lits_str) 
   1.215 +	val knd = name_of_kind kind
   1.216 +	val cls_str = gen_tptp_cls(clause_id, axiom_name, knd, bracket_pack lits) 
   1.217      in
   1.218  	(cls_str,tfree_lits) 
   1.219      end;
   1.220  
   1.221 -
   1.222  fun tptp_tfree_clause tfree_lit =
   1.223      "input_clause(" ^ "tfree_tcs," ^ "conjecture" ^ ",[" ^ tfree_lit ^ "]).\n";
   1.224  
   1.225 -
   1.226  fun tptp_of_arLit (TConsLit(b,(c,t,args))) =
   1.227        tptp_sign b (c ^ "(" ^ t ^ paren_pack args ^ ")")
   1.228    | tptp_of_arLit (TVarLit(b,(c,str))) =
   1.229 @@ -1092,7 +1032,7 @@
   1.230      val tfree_clss = map tptp_tfree_clause (foldl (op union_string) [] tfree_litss)
   1.231      val out = TextIO.openOut filename
   1.232    in
   1.233 -    List.app (writeln_strs out o tptp_clause) axclauses;
   1.234 +    List.app (curry TextIO.output out o #1 o clause2tptp) axclauses;
   1.235      writeln_strs out tfree_clss;
   1.236      writeln_strs out tptp_clss;
   1.237      List.app (curry TextIO.output out o tptp_classrelClause) classrel_clauses;