src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML
changeset 36170 0cdb76723c88
parent 36169 27b1cc58715e
child 36186 bd246b00ef5a
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML	Fri Apr 16 14:48:34 2010 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML	Fri Apr 16 15:49:13 2010 +0200
     1.3 @@ -6,6 +6,7 @@
     1.4  
     1.5  signature SLEDGEHAMMER_HOL_CLAUSE =
     1.6  sig
     1.7 +  type name = Sledgehammer_FOL_Clause.name
     1.8    type kind = Sledgehammer_FOL_Clause.kind
     1.9    type fol_type = Sledgehammer_FOL_Clause.fol_type
    1.10    type classrel_clause = Sledgehammer_FOL_Clause.classrel_clause
    1.11 @@ -15,8 +16,8 @@
    1.12    type hol_clause_id = int
    1.13  
    1.14    datatype combterm =
    1.15 -    CombConst of string * fol_type * fol_type list (* Const and Free *) |
    1.16 -    CombVar of string * fol_type |
    1.17 +    CombConst of name * fol_type * fol_type list (* Const and Free *) |
    1.18 +    CombVar of name * fol_type |
    1.19      CombApp of combterm * combterm
    1.20    datatype literal = Literal of polarity * combterm
    1.21    datatype hol_clause =
    1.22 @@ -75,8 +76,8 @@
    1.23  type hol_clause_id = int;
    1.24  
    1.25  datatype combterm =
    1.26 -  CombConst of string * fol_type * fol_type list (* Const and Free *) |
    1.27 -  CombVar of string * fol_type |
    1.28 +  CombConst of name * fol_type * fol_type list (* Const and Free *) |
    1.29 +  CombVar of name * fol_type |
    1.30    CombApp of combterm * combterm
    1.31  
    1.32  datatype literal = Literal of polarity * combterm;
    1.33 @@ -90,11 +91,11 @@
    1.34  (* convert a clause with type Term.term to a clause with type clause *)
    1.35  (*********************************************************************)
    1.36  
    1.37 -fun isFalse (Literal(pol, CombConst(c,_,_))) =
    1.38 +fun isFalse (Literal (pol, CombConst ((c, _), _, _))) =
    1.39        (pol andalso c = "c_False") orelse (not pol andalso c = "c_True")
    1.40    | isFalse _ = false;
    1.41  
    1.42 -fun isTrue (Literal (pol, CombConst(c,_,_))) =
    1.43 +fun isTrue (Literal (pol, CombConst ((c, _), _, _))) =
    1.44        (pol andalso c = "c_True") orelse
    1.45        (not pol andalso c = "c_False")
    1.46    | isTrue _ = false;
    1.47 @@ -127,15 +128,15 @@
    1.48  (* convert a Term.term (with combinators) into a combterm, also accummulate sort info *)
    1.49  fun combterm_of dfg thy (Const(c,t)) =
    1.50        let val (tp,ts,tvar_list) = const_type_of dfg thy (c,t)
    1.51 -          val c' = CombConst(make_fixed_const dfg c, tp, tvar_list)
    1.52 +          val c' = CombConst (`(make_fixed_const dfg) c, tp, tvar_list)
    1.53        in  (c',ts)  end
    1.54    | combterm_of dfg _ (Free(v,t)) =
    1.55        let val (tp,ts) = type_of dfg t
    1.56 -          val v' = CombConst(make_fixed_var v, tp, [])
    1.57 +          val v' = CombConst (`make_fixed_var v, tp, [])
    1.58        in  (v',ts)  end
    1.59    | combterm_of dfg _ (Var(v,t)) =
    1.60        let val (tp,ts) = type_of dfg t
    1.61 -          val v' = CombVar(make_schematic_var v,tp)
    1.62 +          val v' = CombVar ((make_schematic_var v, string_of_indexname v), tp)
    1.63        in  (v',ts)  end
    1.64    | combterm_of dfg thy (P $ Q) =
    1.65        let val (P',tsP) = combterm_of dfg thy P
    1.66 @@ -211,11 +212,20 @@
    1.67  
    1.68  val type_wrapper = "ti";
    1.69  
    1.70 -fun head_needs_hBOOL const_needs_hBOOL (CombConst(c,_,_)) = needs_hBOOL const_needs_hBOOL c
    1.71 +fun head_needs_hBOOL const_needs_hBOOL (CombConst((c, _), _, _)) =
    1.72 +    needs_hBOOL const_needs_hBOOL c
    1.73    | head_needs_hBOOL _ _ = true;
    1.74  
    1.75 -fun wrap_type full_types (s, tp) =
    1.76 -  if full_types then type_wrapper ^ paren_pack [s, string_of_fol_type tp] else s;
    1.77 +fun wrap_type full_types (s, ty) pool =
    1.78 +  if full_types then
    1.79 +    let val (s', pool) = string_of_fol_type ty pool in
    1.80 +      (type_wrapper ^ paren_pack [s, s'], pool)
    1.81 +    end
    1.82 +  else
    1.83 +    (s, pool)
    1.84 +
    1.85 +fun wrap_type_if full_types cnh (head, s, tp) =
    1.86 +  if head_needs_hBOOL cnh head then wrap_type full_types (s, tp) else pair s
    1.87  
    1.88  fun apply ss = "hAPP" ^ paren_pack ss;
    1.89  
    1.90 @@ -224,105 +234,118 @@
    1.91  
    1.92  fun string_apply (v, args) = rev_apply (v, rev args);
    1.93  
    1.94 -(*Apply an operator to the argument strings, using either the "apply" operator or
    1.95 -  direct function application.*)
    1.96 -fun string_of_applic full_types cma (CombConst (c, _, tvars), args) =
    1.97 -      let val c = if c = "equal" then "c_fequal" else c
    1.98 -          val nargs = min_arity_of cma c
    1.99 -          val args1 = List.take(args, nargs)
   1.100 -            handle Subscript => error ("string_of_applic: " ^ c ^ " has arity " ^
   1.101 -                                         Int.toString nargs ^ " but is applied to " ^
   1.102 -                                         space_implode ", " args)
   1.103 -          val args2 = List.drop(args, nargs)
   1.104 -          val targs = if full_types then [] else map string_of_fol_type tvars
   1.105 -      in
   1.106 -          string_apply (c ^ paren_pack (args1@targs), args2)
   1.107 -      end
   1.108 -  | string_of_applic _ _ (CombVar (v, _), args) = string_apply (v, args)
   1.109 -  | string_of_applic _ _ _ = error "string_of_applic";
   1.110 +(* Apply an operator to the argument strings, using either the "apply" operator
   1.111 +   or direct function application. *)
   1.112 +fun string_of_application full_types cma (CombConst ((s, s'), _, tvars), args)
   1.113 +                          pool =
   1.114 +    let
   1.115 +      val s = if s = "equal" then "c_fequal" else s
   1.116 +      val nargs = min_arity_of cma s
   1.117 +      val args1 = List.take (args, nargs)
   1.118 +        handle Subscript =>
   1.119 +               raise Fail (quote s ^ " has arity " ^ Int.toString nargs ^
   1.120 +                           " but is applied to " ^ commas (map quote args))
   1.121 +      val args2 = List.drop (args, nargs)
   1.122 +      val (targs, pool) = if full_types then ([], pool)
   1.123 +                          else pool_map string_of_fol_type tvars pool
   1.124 +      val (s, pool) = nice_name (s, s') pool
   1.125 +    in (string_apply (s ^ paren_pack (args1 @ targs), args2), pool) end
   1.126 +  | string_of_application _ _ (CombVar (name, _), args) pool =
   1.127 +    nice_name name pool |>> (fn s => string_apply (s, args))
   1.128  
   1.129 -fun wrap_type_if full_types cnh (head, s, tp) =
   1.130 -  if head_needs_hBOOL cnh head then wrap_type full_types (s, tp) else s;
   1.131 -
   1.132 -fun string_of_combterm (params as (full_types, cma, cnh)) t =
   1.133 -  let val (head, args) = strip_combterm_comb t
   1.134 -  in  wrap_type_if full_types cnh (head,
   1.135 -          string_of_applic full_types cma
   1.136 -                           (head, map (string_of_combterm (params)) args),
   1.137 -          type_of_combterm t)
   1.138 -  end;
   1.139 +fun string_of_combterm (params as (full_types, cma, cnh)) t pool =
   1.140 +  let
   1.141 +    val (head, args) = strip_combterm_comb t
   1.142 +    val (ss, pool) = pool_map (string_of_combterm params) args pool
   1.143 +    val (s, pool) = string_of_application full_types cma (head, ss) pool
   1.144 +  in wrap_type_if full_types cnh (head, s, type_of_combterm t) pool end
   1.145  
   1.146  (*Boolean-valued terms are here converted to literals.*)
   1.147 -fun boolify params t =
   1.148 -  "hBOOL" ^ paren_pack [string_of_combterm params t];
   1.149 +fun boolify params c =
   1.150 +  string_of_combterm params c #>> prefix "hBOOL" o paren_pack o single
   1.151  
   1.152 -fun string_of_predicate (params as (_,_,cnh)) t =
   1.153 +fun string_of_predicate (params as (_, _, cnh)) t =
   1.154    case t of
   1.155 -      (CombApp(CombApp(CombConst("equal",_,_), t1), t2)) =>
   1.156 -          (*DFG only: new TPTP prefers infix equality*)
   1.157 -          ("equal" ^ paren_pack [string_of_combterm params t1, string_of_combterm params t2])
   1.158 -    | _ =>
   1.159 -          case #1 (strip_combterm_comb t) of
   1.160 -              CombConst(c,_,_) => if needs_hBOOL cnh c then boolify params t else string_of_combterm params t
   1.161 -            | _ => boolify params t;
   1.162 +    (CombApp (CombApp (CombConst (("equal", _), _, _), t1), t2)) =>
   1.163 +    (* DFG only: new TPTP prefers infix equality *)
   1.164 +    pool_map (string_of_combterm params) [t1, t2]
   1.165 +    #>> prefix "equal" o paren_pack
   1.166 +  | _ =>
   1.167 +    case #1 (strip_combterm_comb t) of
   1.168 +      CombConst ((s, _), _, _) =>
   1.169 +      (if needs_hBOOL cnh s then boolify else string_of_combterm) params t
   1.170 +    | _ => boolify params t
   1.171  
   1.172  
   1.173 -(*** tptp format ***)
   1.174 +(*** TPTP format ***)
   1.175  
   1.176 -fun tptp_of_equality params pol (t1,t2) =
   1.177 -  let val eqop = if pol then " = " else " != "
   1.178 -  in  string_of_combterm params t1 ^ eqop ^ string_of_combterm params t2  end;
   1.179 -
   1.180 -fun tptp_literal params (Literal(pol, CombApp(CombApp(CombConst("equal", _, _), t1), t2))) =
   1.181 -      tptp_of_equality params pol (t1,t2)
   1.182 -  | tptp_literal params (Literal(pol,pred)) =
   1.183 -      tptp_sign pol (string_of_predicate params pred);
   1.184 +fun tptp_of_equality params pos (t1, t2) =
   1.185 +  pool_map (string_of_combterm params) [t1, t2]
   1.186 +  #>> space_implode (if pos then " = " else " != ")
   1.187  
   1.188 -(*Given a clause, returns its literals paired with a list of literals concerning TFrees;
   1.189 -  the latter should only occur in conjecture clauses.*)
   1.190 -fun tptp_type_lits params pos (HOLClause {literals, ctypes_sorts, ...}) =
   1.191 -      (map (tptp_literal params) literals, 
   1.192 -       map (tptp_of_typeLit pos) (add_typs ctypes_sorts));
   1.193 +fun tptp_literal params
   1.194 +        (Literal (pos, CombApp (CombApp (CombConst (("equal", _), _, _), t1),
   1.195 +                                         t2))) =
   1.196 +    tptp_of_equality params pos (t1, t2)
   1.197 +  | tptp_literal params (Literal (pos, pred)) =
   1.198 +    string_of_predicate params pred #>> tptp_sign pos
   1.199 + 
   1.200 +(* Given a clause, returns its literals paired with a list of literals
   1.201 +   concerning TFrees; the latter should only occur in conjecture clauses. *)
   1.202 +fun tptp_type_literals params pos (HOLClause {literals, ctypes_sorts, ...}) =
   1.203 +  pool_map (tptp_literal params) literals
   1.204 +  #>> rpair (map (tptp_of_typeLit pos) (add_typs ctypes_sorts))
   1.205  
   1.206 -fun clause2tptp params (cls as HOLClause {axiom_name, clause_id, kind, ...}) =
   1.207 -  let val (lits,tylits) = tptp_type_lits params (kind = Conjecture) cls
   1.208 +fun tptp_clause params (cls as HOLClause {axiom_name, clause_id, kind, ...})
   1.209 +                pool =
   1.210 +let
   1.211 +    val ((lits, tylits), pool) =
   1.212 +      tptp_type_literals params (kind = Conjecture) cls pool
   1.213    in
   1.214 -      (gen_tptp_cls (clause_id, axiom_name, kind, lits, tylits), tylits)
   1.215 -  end;
   1.216 +    ((gen_tptp_cls (clause_id, axiom_name, kind, lits, tylits), tylits), pool)
   1.217 +  end
   1.218  
   1.219  
   1.220 -(*** dfg format ***)
   1.221 +(*** DFG format ***)
   1.222  
   1.223 -fun dfg_literal params (Literal(pol,pred)) = dfg_sign pol (string_of_predicate params pred);
   1.224 +fun dfg_literal params (Literal (pos, pred)) =
   1.225 +  string_of_predicate params pred #>> dfg_sign pos
   1.226  
   1.227 -fun dfg_type_lits params pos (HOLClause {literals, ctypes_sorts, ...}) =
   1.228 -      (map (dfg_literal params) literals, 
   1.229 -       map (dfg_of_typeLit pos) (add_typs ctypes_sorts));
   1.230 +fun dfg_type_literals params pos (HOLClause {literals, ctypes_sorts, ...}) =
   1.231 +  pool_map (dfg_literal params) literals
   1.232 +  #>> rpair (map (dfg_of_typeLit pos) (add_typs ctypes_sorts))
   1.233  
   1.234 -fun get_uvars (CombConst _) vars = vars
   1.235 -  | get_uvars (CombVar(v,_)) vars = (v::vars)
   1.236 -  | get_uvars (CombApp(P,Q)) vars = get_uvars P (get_uvars Q vars);
   1.237 +fun get_uvars (CombConst _) vars pool = (vars, pool)
   1.238 +  | get_uvars (CombVar (name, _)) vars pool =
   1.239 +    nice_name name pool |>> (fn var => var :: vars)
   1.240 +  | get_uvars (CombApp (P, Q)) vars pool =
   1.241 +    let val (vars, pool) = get_uvars P vars pool in get_uvars Q vars pool end
   1.242  
   1.243 -fun get_uvars_l (Literal(_,c)) = get_uvars c [];
   1.244 +fun get_uvars_l (Literal (_, c)) = get_uvars c [];
   1.245  
   1.246 -fun dfg_vars (HOLClause {literals,...}) = union_all (map get_uvars_l literals);
   1.247 +fun dfg_vars (HOLClause {literals, ...}) =
   1.248 +  pool_map get_uvars_l literals #>> union_all
   1.249  
   1.250 -fun clause2dfg params (cls as HOLClause {axiom_name, clause_id, kind,
   1.251 -                                         ctypes_sorts, ...}) =
   1.252 -  let val (lits,tylits) = dfg_type_lits params (kind = Conjecture) cls
   1.253 -      val vars = dfg_vars cls
   1.254 -      val tvars = get_tvar_strs ctypes_sorts
   1.255 +fun dfg_clause params (cls as HOLClause {axiom_name, clause_id, kind,
   1.256 +                                         ctypes_sorts, ...}) pool =
   1.257 +  let
   1.258 +    val ((lits, tylits), pool) =
   1.259 +      dfg_type_literals params (kind = Conjecture) cls pool
   1.260 +    val (vars, pool) = dfg_vars cls pool
   1.261 +    val tvars = get_tvar_strs ctypes_sorts
   1.262    in
   1.263 -      (gen_dfg_cls (clause_id, axiom_name, kind, lits, tylits, tvars@vars), tylits)
   1.264 -  end;
   1.265 +    ((gen_dfg_cls (clause_id, axiom_name, kind, lits, tylits, tvars @ vars),
   1.266 +      tylits), pool)
   1.267 +  end
   1.268  
   1.269  
   1.270  (** For DFG format: accumulate function and predicate declarations **)
   1.271  
   1.272  fun addtypes tvars tab = List.foldl add_foltype_funcs tab tvars;
   1.273  
   1.274 -fun add_decls (full_types, cma, cnh) (CombConst (c, _, tvars), (funcs, preds)) =
   1.275 -      if c = "equal" then (addtypes tvars funcs, preds)
   1.276 +fun add_decls (full_types, cma, cnh) (CombConst ((c, _), _, tvars), (funcs, preds)) =
   1.277 +      if c = "equal" then
   1.278 +        (addtypes tvars funcs, preds)
   1.279        else
   1.280          let val arity = min_arity_of cma c
   1.281              val ntys = if not full_types then length tvars else 0
   1.282 @@ -331,7 +354,7 @@
   1.283              if needs_hBOOL cnh c then (addtypes tvars (addit funcs), preds)
   1.284              else (addtypes tvars funcs, addit preds)
   1.285          end
   1.286 -  | add_decls _ (CombVar(_,ctp), (funcs,preds)) =
   1.287 +  | add_decls _ (CombVar (_,ctp), (funcs, preds)) =
   1.288        (add_foltype_funcs (ctp,funcs), preds)
   1.289    | add_decls params (CombApp(P,Q),decls) = add_decls params (P,add_decls params (Q,decls));
   1.290  
   1.291 @@ -372,7 +395,7 @@
   1.292    Symtab.make [("c_COMBI", 0), ("c_COMBK", 0), ("c_COMBB", 0), ("c_COMBC", 0),
   1.293                 ("c_COMBS", 0)];
   1.294  
   1.295 -fun count_combterm (CombConst (c, _, _), ct) =
   1.296 +fun count_combterm (CombConst ((c, _), _, _), ct) =
   1.297       (case Symtab.lookup ct c of NONE => ct  (*no counter*)
   1.298                                 | SOME n => Symtab.update (c,n+1) ct)
   1.299    | count_combterm (CombVar _, ct) = ct
   1.300 @@ -420,7 +443,7 @@
   1.301        val (const_min_arity, const_needs_hBOOL) = fold (count_constants_term false) args (const_min_arity, const_needs_hBOOL)
   1.302    in
   1.303        case head of
   1.304 -          CombConst (a,_,_) => (*predicate or function version of "equal"?*)
   1.305 +          CombConst ((a, _),_,_) => (*predicate or function version of "equal"?*)
   1.306              let val a = if a="equal" andalso not toplev then "c_fequal" else a
   1.307              val const_min_arity = Symtab.map_default (a, n) (Integer.min n) const_min_arity
   1.308              in
   1.309 @@ -459,25 +482,31 @@
   1.310    let
   1.311      fun section _ [] = []
   1.312        | section name ss = "\n% " ^ name ^ plural_s (length ss) ^ "\n" :: ss
   1.313 +    val pool = empty_name_pool debug
   1.314      val (conjectures, axclauses, _, helper_clauses,
   1.315        classrel_clauses, arity_clauses) = clauses
   1.316      val (cma, cnh) = count_constants clauses
   1.317      val params = (full_types, cma, cnh)
   1.318 -    val (tptp_clss,tfree_litss) = ListPair.unzip (map (clause2tptp params) conjectures)
   1.319 +    val ((conjecture_clss, tfree_litss), pool) =
   1.320 +      pool_map (tptp_clause params) conjectures pool |>> ListPair.unzip
   1.321      val tfree_clss = map tptp_tfree_clause (List.foldl (uncurry (union (op =))) [] tfree_litss)
   1.322 -    val timestamp = Date.fmt "%Y-%m-%d %H:%M:%S" (Date.fromTimeLocal (Time.now ()))
   1.323 +    val (ax_clss, pool) = pool_map (apfst fst oo tptp_clause params) axclauses
   1.324 +                                   pool
   1.325 +    val classrel_clss = map tptp_classrel_clause classrel_clauses
   1.326 +    val arity_clss = map tptp_arity_clause arity_clauses
   1.327 +    val (helper_clss, pool) = pool_map (apfst fst oo tptp_clause params)
   1.328 +                                       helper_clauses pool
   1.329      val _ =
   1.330        File.write_list file (
   1.331          "% This file was generated by Isabelle (most likely Sledgehammer)\n" ^
   1.332 -        "% " ^ timestamp ^ "\n" ::
   1.333 -        section "Relevant fact" (map (#1 o (clause2tptp params)) axclauses) @
   1.334 +        "% " ^ timestamp () ^ "\n" ::
   1.335 +        section "Relevant fact" ax_clss @
   1.336          section "Type variable" tfree_clss @
   1.337 -        section "Class relationship"
   1.338 -                (map tptp_classrel_clause classrel_clauses) @
   1.339 -        section "Arity declaration" (map tptp_arity_clause arity_clauses) @
   1.340 -        section "Helper fact" (map (#1 o (clause2tptp params)) helper_clauses) @
   1.341 -        section "Conjecture" tptp_clss)
   1.342 -    in (length axclauses + 1, length tfree_clss + length tptp_clss)
   1.343 +        section "Class relationship" classrel_clss @
   1.344 +        section "Arity declaration" arity_clss @
   1.345 +        section "Helper fact" helper_clss @
   1.346 +        section "Conjecture" conjecture_clss)
   1.347 +    in (length axclauses + 1, length tfree_clss + length conjecture_clss)
   1.348    end;
   1.349  
   1.350  
   1.351 @@ -485,15 +514,18 @@
   1.352  
   1.353  fun write_dfg_file debug full_types file clauses =
   1.354    let
   1.355 +    val pool = empty_name_pool debug
   1.356      val (conjectures, axclauses, _, helper_clauses,
   1.357        classrel_clauses, arity_clauses) = clauses
   1.358      val (cma, cnh) = count_constants clauses
   1.359      val params = (full_types, cma, cnh)
   1.360 -    val (dfg_clss, tfree_litss) = ListPair.unzip (map (clause2dfg params) conjectures)
   1.361 +    val ((conjecture_clss, tfree_litss), pool) =
   1.362 +      pool_map (dfg_clause params) conjectures pool |>> ListPair.unzip
   1.363      and probname = Path.implode (Path.base file)
   1.364 -    val axstrs = map (#1 o (clause2dfg params)) axclauses
   1.365 +    val (axstrs, pool) = pool_map (apfst fst oo dfg_clause params) axclauses pool
   1.366      val tfree_clss = map dfg_tfree_clause (union_all tfree_litss)
   1.367 -    val helper_clauses_strs = map (#1 o (clause2dfg params)) helper_clauses
   1.368 +    val (helper_clauses_strs, pool) =
   1.369 +      pool_map (apfst fst oo dfg_clause params) helper_clauses pool
   1.370      val (funcs,cl_preds) = decls_of_clauses params (helper_clauses @ conjectures @ axclauses) arity_clauses
   1.371      and ty_preds = preds_of_clauses axclauses classrel_clauses arity_clauses
   1.372      val _ =
   1.373 @@ -509,14 +541,15 @@
   1.374          helper_clauses_strs @
   1.375          ["end_of_list.\n\nlist_of_clauses(conjectures, cnf).\n"] @
   1.376          tfree_clss @
   1.377 -        dfg_clss @
   1.378 +        conjecture_clss @
   1.379          ["end_of_list.\n\n",
   1.380          (*VarWeight=3 helps the HO problems, probably by counteracting the presence of hAPP*)
   1.381           "list_of_settings(SPASS).\n{*\nset_flag(VarWeight, 3).\n*}\nend_of_list.\n\n",
   1.382           "end_problem.\n"])
   1.383  
   1.384 -    in (length axclauses + length classrel_clauses + length arity_clauses +
   1.385 -      length helper_clauses + 1, length tfree_clss + length dfg_clss)
   1.386 -  end;
   1.387 +  in
   1.388 +    (length axclauses + length classrel_clauses + length arity_clauses +
   1.389 +     length helper_clauses + 1, length tfree_clss + length conjecture_clss)
   1.390 +  end
   1.391  
   1.392  end;