src/HOL/Tools/res_clause.ML
changeset 24937 340523598914
parent 24322 dc7336b8c54c
child 24940 8f9dea697b8d
     1.1 --- a/src/HOL/Tools/res_clause.ML	Tue Oct 09 17:11:20 2007 +0200
     1.2 +++ b/src/HOL/Tools/res_clause.ML	Tue Oct 09 18:14:00 2007 +0200
     1.3 @@ -32,7 +32,6 @@
     1.4    val make_fixed_type_const : string -> string
     1.5    val make_type_class : string -> string
     1.6    datatype kind = Axiom | Conjecture
     1.7 -  val name_of_kind : kind -> string
     1.8    type axiom_name = string
     1.9    datatype typ_var = FOLTVar of indexname | FOLTFree of string
    1.10    datatype fol_type =
    1.11 @@ -44,20 +43,15 @@
    1.12    val mk_typ_var_sort: typ -> typ_var * sort
    1.13    exception CLAUSE of string * term
    1.14    val isMeta : string -> bool
    1.15 -  val add_typs_aux : (typ_var * string list) list -> type_literal list * type_literal list
    1.16 +  val add_typs : (typ_var * string list) list -> type_literal list
    1.17    val get_tvar_strs: (typ_var * sort) list -> string list
    1.18    datatype arLit =
    1.19        TConsLit of class * string * string list
    1.20      | TVarLit of class * string
    1.21    datatype arityClause = ArityClause of
    1.22 -   {axiom_name: axiom_name,
    1.23 -    kind: kind,
    1.24 -    conclLit: arLit,
    1.25 -    premLits: arLit list}
    1.26 +   {axiom_name: axiom_name, conclLit: arLit, premLits: arLit list}
    1.27    datatype classrelClause = ClassrelClause of
    1.28 -   {axiom_name: axiom_name,
    1.29 -    subclass: class,
    1.30 -    superclass: class}
    1.31 +   {axiom_name: axiom_name, subclass: class, superclass: class}
    1.32    val make_classrel_clauses: theory -> class list -> class list -> classrelClause list
    1.33    val make_arity_clauses: theory -> string list -> class list -> class list * arityClause list
    1.34    val add_type_sort_preds: (typ_var * string list) * int Symtab.table -> int Symtab.table
    1.35 @@ -69,8 +63,8 @@
    1.36    val init_functab: int Symtab.table
    1.37    val writeln_strs: TextIO.outstream -> string list -> unit
    1.38    val dfg_sign: bool -> string -> string
    1.39 -  val dfg_of_typeLit: type_literal -> string
    1.40 -  val gen_dfg_cls: int * string * string * string * string list -> string
    1.41 +  val dfg_of_typeLit: bool -> type_literal -> string
    1.42 +  val gen_dfg_cls: int * string * kind * string list * string list * string list -> string
    1.43    val string_of_preds: (string * Int.int) list -> string
    1.44    val string_of_funcs: (string * int) list -> string
    1.45    val string_of_symbols: string -> string -> string
    1.46 @@ -80,8 +74,8 @@
    1.47    val dfg_classrelClause: classrelClause -> string
    1.48    val dfg_arity_clause: arityClause -> string
    1.49    val tptp_sign: bool -> string -> string
    1.50 -  val tptp_of_typeLit : type_literal -> string
    1.51 -  val gen_tptp_cls : int * string * kind * string list -> string
    1.52 +  val tptp_of_typeLit : bool -> type_literal -> string
    1.53 +  val gen_tptp_cls : int * string * kind * string list * string list -> string
    1.54    val tptp_tfree_clause : string -> string
    1.55    val tptp_arity_clause : arityClause -> string
    1.56    val tptp_classrelClause : classrelClause -> string
    1.57 @@ -236,9 +230,6 @@
    1.58  
    1.59  datatype kind = Axiom | Conjecture;
    1.60  
    1.61 -fun name_of_kind Axiom = "axiom"
    1.62 -  | name_of_kind Conjecture = "negated_conjecture";
    1.63 -
    1.64  type axiom_name = string;
    1.65  
    1.66  (**** Isabelle FOL clauses ****)
    1.67 @@ -296,18 +287,8 @@
    1.68  fun pred_of_sort (LTVar (s,ty)) = (s,1)
    1.69    | pred_of_sort (LTFree (s,ty)) = (s,1)
    1.70  
    1.71 -(*Given a list of sorted type variables, return two separate lists.
    1.72 -  The first is for TVars, the second for TFrees.*)
    1.73 -fun add_typs_aux [] = ([],[])
    1.74 -  | add_typs_aux ((FOLTVar indx, s) :: tss) =
    1.75 -      let val vs = sorts_on_typs (FOLTVar indx, s)
    1.76 -          val (vss,fss) = add_typs_aux tss
    1.77 -      in  (vs union vss, fss)  end
    1.78 -  | add_typs_aux ((FOLTFree x, s) :: tss) =
    1.79 -      let val fs = sorts_on_typs (FOLTFree x, s)
    1.80 -          val (vss,fss) = add_typs_aux tss
    1.81 -      in  (vss, fs union fss)  end;
    1.82 -
    1.83 +(*Given a list of sorted type variables, return a list of type literals.*)
    1.84 +fun add_typs tss = foldl (op union) [] (map sorts_on_typs tss);
    1.85  
    1.86  (** make axiom and conjecture clauses. **)
    1.87  
    1.88 @@ -327,7 +308,6 @@
    1.89  
    1.90  datatype arityClause =
    1.91           ArityClause of {axiom_name: axiom_name,
    1.92 -                         kind: kind,
    1.93                           conclLit: arLit,
    1.94                           premLits: arLit list};
    1.95  
    1.96 @@ -344,7 +324,7 @@
    1.97     let val tvars = gen_TVars (length args)
    1.98         val tvars_srts = ListPair.zip (tvars,args)
    1.99     in
   1.100 -      ArityClause {axiom_name = axiom_name, kind = Axiom,
   1.101 +      ArityClause {axiom_name = axiom_name, 
   1.102                     conclLit = TConsLit (cls, make_fixed_type_const tcons, tvars),
   1.103                     premLits = map TVarLit (union_all(map pack_sort tvars_srts))}
   1.104     end;
   1.105 @@ -478,17 +458,21 @@
   1.106  fun dfg_sign true s = s
   1.107    | dfg_sign false s = "not(" ^ s ^ ")"
   1.108  
   1.109 -fun dfg_of_typeLit (LTVar (s,ty)) = "not(" ^ s ^ "(" ^ ty ^ "))"
   1.110 -  | dfg_of_typeLit (LTFree (s,ty)) = s ^ "(" ^ ty ^ ")";
   1.111 +fun dfg_of_typeLit pos (LTVar (s,ty))  = dfg_sign pos (s ^ "(" ^ ty ^ ")")
   1.112 +  | dfg_of_typeLit pos (LTFree (s,ty)) = dfg_sign pos (s ^ "(" ^ ty ^ ")");
   1.113  
   1.114  (*Enclose the clause body by quantifiers, if necessary*)
   1.115  fun dfg_forall [] body = body
   1.116    | dfg_forall vars body = "forall([" ^ commas vars ^ "],\n" ^ body ^ ")"
   1.117  
   1.118 -fun gen_dfg_cls (cls_id, ax_name, knd, lits, vars) =
   1.119 -    "clause( %(" ^ knd ^ ")\n" ^
   1.120 -    dfg_forall vars ("or(" ^ lits ^ ")") ^ ",\n" ^
   1.121 -    string_of_clausename (cls_id,ax_name) ^  ").\n\n";
   1.122 +fun gen_dfg_cls (cls_id, ax_name, Axiom, lits, tylits, vars) =
   1.123 +      "clause( %(axiom)\n" ^
   1.124 +      dfg_forall vars ("or(" ^ commas (tylits@lits) ^ ")") ^ ",\n" ^
   1.125 +      string_of_clausename (cls_id,ax_name) ^  ").\n\n"
   1.126 +  | gen_dfg_cls (cls_id, ax_name, Conjecture, lits, _, vars) =
   1.127 +      "clause( %(negated_conjecture)\n" ^
   1.128 +      dfg_forall vars ("or(" ^ commas lits ^ ")") ^ ",\n" ^
   1.129 +      string_of_clausename (cls_id,ax_name) ^  ").\n\n";
   1.130  
   1.131  fun string_of_arity (name, num) =  "(" ^ name ^ "," ^ Int.toString num ^ ")"
   1.132  
   1.133 @@ -523,11 +507,11 @@
   1.134  
   1.135  fun string_of_ar axiom_name = arclause_prefix ^ ascii_of axiom_name;
   1.136  
   1.137 -fun dfg_arity_clause (ArityClause{axiom_name,kind,conclLit,premLits,...}) =
   1.138 +fun dfg_arity_clause (ArityClause{axiom_name,conclLit,premLits,...}) =
   1.139    let val TConsLit (_,_,tvars) = conclLit
   1.140        val lits = map dfg_of_arLit (conclLit :: premLits)
   1.141    in
   1.142 -      "clause( %(" ^ name_of_kind kind ^ ")\n" ^
   1.143 +      "clause( %(axiom)\n" ^
   1.144        dfg_forall tvars ("or( " ^ commas lits ^ ")") ^ ",\n" ^
   1.145        string_of_ar axiom_name ^ ").\n\n"
   1.146    end;
   1.147 @@ -539,12 +523,15 @@
   1.148  fun tptp_sign true s = s
   1.149    | tptp_sign false s = "~ " ^ s
   1.150  
   1.151 -fun tptp_of_typeLit (LTVar (s,ty))  = tptp_sign false (s ^ "(" ^ ty ^ ")")
   1.152 -  | tptp_of_typeLit (LTFree (s,ty)) = tptp_sign true  (s ^ "(" ^ ty ^ ")");
   1.153 +fun tptp_of_typeLit pos (LTVar (s,ty))  = tptp_sign pos (s ^ "(" ^ ty ^ ")")
   1.154 +  | tptp_of_typeLit pos (LTFree (s,ty)) = tptp_sign pos  (s ^ "(" ^ ty ^ ")");
   1.155  
   1.156 -fun gen_tptp_cls (cls_id,ax_name,knd,lits) =
   1.157 -    "cnf(" ^ string_of_clausename (cls_id,ax_name) ^ "," ^
   1.158 -    name_of_kind knd ^ "," ^ tptp_pack lits ^ ").\n";
   1.159 +fun gen_tptp_cls (cls_id,ax_name,Axiom,lits,tylits) =
   1.160 +      "cnf(" ^ string_of_clausename (cls_id,ax_name) ^ ",axiom," ^ 
   1.161 +               tptp_pack (tylits@lits) ^ ").\n"
   1.162 +  | gen_tptp_cls (cls_id,ax_name,Conjecture,lits,_) =
   1.163 +      "cnf(" ^ string_of_clausename (cls_id,ax_name) ^ ",negated_conjecture," ^ 
   1.164 +               tptp_pack lits ^ ").\n";
   1.165  
   1.166  fun tptp_tfree_clause tfree_lit =
   1.167      "cnf(" ^ "tfree_tcs," ^ "negated_conjecture" ^ "," ^ tptp_pack[tfree_lit] ^ ").\n";
   1.168 @@ -554,8 +541,8 @@
   1.169    | tptp_of_arLit (TVarLit (c,str)) =
   1.170        tptp_sign false (make_type_class c ^ "(" ^ str ^ ")")
   1.171  
   1.172 -fun tptp_arity_clause (ArityClause{axiom_name,kind,conclLit,premLits,...}) =
   1.173 -  "cnf(" ^ string_of_ar axiom_name ^ "," ^ name_of_kind kind ^ "," ^
   1.174 +fun tptp_arity_clause (ArityClause{axiom_name,conclLit,premLits,...}) =
   1.175 +  "cnf(" ^ string_of_ar axiom_name ^ ",axiom," ^
   1.176    tptp_pack (map tptp_of_arLit (conclLit :: premLits)) ^ ").\n";
   1.177  
   1.178  fun tptp_classrelLits sub sup =