added first-order TPTP version of Nitpick to Isabelle, so that its sources stay in sync with Isabelle and it is easier to install new versions for SystemOnTPTP and CASC -- the tool is called "isabelle nitrox" but is deliberately omitted from the tool list unless the component is explicitly enabled, to avoid clutter
authorblanchet
Tue Mar 22 19:04:32 2011 +0100 (2011-03-22)
changeset 42064f4e53c8630c0
parent 42063 a2a69b32d899
child 42065 2b98b4c2e2f1
added first-order TPTP version of Nitpick to Isabelle, so that its sources stay in sync with Isabelle and it is easier to install new versions for SystemOnTPTP and CASC -- the tool is called "isabelle nitrox" but is deliberately omitted from the tool list unless the component is explicitly enabled, to avoid clutter
src/HOL/IsaMakefile
src/HOL/Nitpick.thy
src/HOL/Tools/Nitpick/etc/settings
src/HOL/Tools/Nitpick/lib/Tools/nitrox
src/HOL/Tools/Nitpick/nitrox.ML
     1.1 --- a/src/HOL/IsaMakefile	Tue Mar 22 18:38:29 2011 +0100
     1.2 +++ b/src/HOL/IsaMakefile	Tue Mar 22 19:04:32 2011 +0100
     1.3 @@ -319,6 +319,7 @@
     1.4    Tools/Nitpick/nitpick_scope.ML \
     1.5    Tools/Nitpick/nitpick_tests.ML \
     1.6    Tools/Nitpick/nitpick_util.ML \
     1.7 +  Tools/Nitpick/nitrox.ML \
     1.8    Tools/numeral.ML \
     1.9    Tools/numeral_simprocs.ML \
    1.10    Tools/numeral_syntax.ML \
     2.1 --- a/src/HOL/Nitpick.thy	Tue Mar 22 18:38:29 2011 +0100
     2.2 +++ b/src/HOL/Nitpick.thy	Tue Mar 22 19:04:32 2011 +0100
     2.3 @@ -24,8 +24,10 @@
     2.4       ("Tools/Nitpick/nitpick.ML")
     2.5       ("Tools/Nitpick/nitpick_isar.ML")
     2.6       ("Tools/Nitpick/nitpick_tests.ML")
     2.7 +     ("Tools/Nitpick/nitrox.ML")
     2.8  begin
     2.9  
    2.10 +typedecl iota (* for Nitrox *)
    2.11  typedecl bisim_iterator
    2.12  
    2.13  axiomatization unknown :: 'a
    2.14 @@ -231,6 +233,7 @@
    2.15  use "Tools/Nitpick/nitpick.ML"
    2.16  use "Tools/Nitpick/nitpick_isar.ML"
    2.17  use "Tools/Nitpick/nitpick_tests.ML"
    2.18 +use "Tools/Nitpick/nitrox.ML"
    2.19  
    2.20  setup {* Nitpick_Isar.setup *}
    2.21  
    2.22 @@ -239,7 +242,8 @@
    2.23      fold_graph' nat_gcd nat_lcm int_gcd int_lcm Frac Abs_Frac Rep_Frac zero_frac
    2.24      one_frac num denom norm_frac frac plus_frac times_frac uminus_frac
    2.25      number_of_frac inverse_frac less_frac less_eq_frac of_frac
    2.26 -hide_type (open) bisim_iterator fun_box pair_box unsigned_bit signed_bit word
    2.27 +hide_type (open) iota bisim_iterator fun_box pair_box unsigned_bit signed_bit
    2.28 +    word
    2.29  hide_fact (open) Ex1_unfold rtrancl_unfold rtranclp_unfold tranclp_unfold
    2.30      prod_def refl'_def wf'_def wf_wfrec'_def wfrec'_def card'_def setsum'_def
    2.31      fold_graph'_def The_psimp Eps_psimp unit_case_unfold nat_case_unfold
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/HOL/Tools/Nitpick/etc/settings	Tue Mar 22 19:04:32 2011 +0100
     3.3 @@ -0,0 +1,1 @@
     3.4 +ISABELLE_TOOLS="$ISABELLE_TOOLS:$COMPONENT/lib/Tools"
     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/src/HOL/Tools/Nitpick/lib/Tools/nitrox	Tue Mar 22 19:04:32 2011 +0100
     4.3 @@ -0,0 +1,24 @@
     4.4 +#!/usr/bin/env bash
     4.5 +#
     4.6 +# Author: Jasmin Blanchette
     4.7 +#
     4.8 +# DESCRIPTION: TPTP FOF version of Nitpick
     4.9 +
    4.10 +
    4.11 +PRG="$(basename "$0")"
    4.12 +
    4.13 +function usage() {
    4.14 +  echo
    4.15 +  echo "Usage: isabelle $PRG FILES"
    4.16 +  echo
    4.17 +  echo "  Runs Nitrox on a FOF or CNF TPTP problem."
    4.18 +  echo
    4.19 +  exit 1
    4.20 +}
    4.21 +
    4.22 +for FILE in "$@"
    4.23 +do
    4.24 +  (echo "theory Nitrox_Run imports Main begin" &&
    4.25 +   echo "ML {* Nitrox.pick_nits_in_fof_file \"$FILE\" *}" &&
    4.26 +   echo "end;") | isabelle tty
    4.27 +done
     5.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.2 +++ b/src/HOL/Tools/Nitpick/nitrox.ML	Tue Mar 22 19:04:32 2011 +0100
     5.3 @@ -0,0 +1,210 @@
     5.4 +(*  Title:      HOL/Tools/Nitpick/nitrox.ML
     5.5 +    Author:     Jasmin Blanchette, TU Muenchen
     5.6 +    Copyright   2010, 2011
     5.7 +
     5.8 +Finite model generation for TPTP first-order formulas via Nitpick.
     5.9 +*)
    5.10 +
    5.11 +signature NITROX =
    5.12 +sig
    5.13 +  val pick_nits_in_fof_file : string -> string
    5.14 +end;
    5.15 +
    5.16 +structure Nitrox : NITROX =
    5.17 +struct
    5.18 +
    5.19 +datatype 'a fo_term = ATerm of 'a * 'a fo_term list
    5.20 +datatype quantifier = AForall | AExists
    5.21 +datatype connective = ANot | AAnd | AOr | AImplies | AIf | AIff | ANotIff
    5.22 +datatype 'a formula =
    5.23 +  AQuant of quantifier * 'a list * 'a formula |
    5.24 +  AConn of connective * 'a formula list |
    5.25 +  APred of 'a fo_term
    5.26 +
    5.27 +exception SYNTAX of string
    5.28 +
    5.29 +fun is_ident_char c = Char.isAlphaNum c orelse c = #"_"
    5.30 +
    5.31 +fun takewhile _ [] = []
    5.32 +  | takewhile p (x :: xs) = if p x then x :: takewhile p xs else []
    5.33 +
    5.34 +fun dropwhile _ [] = []
    5.35 +  | dropwhile p (x :: xs) =  if p x then dropwhile p xs else x :: xs
    5.36 +
    5.37 +fun strip_c_style_comment [] = ""
    5.38 +  | strip_c_style_comment (#"*" :: #"/" :: cs) = strip_spaces_in_list cs
    5.39 +  | strip_c_style_comment (_ :: cs) = strip_c_style_comment cs
    5.40 +and strip_spaces_in_list [] = ""
    5.41 +  | strip_spaces_in_list (#"%" :: cs) =
    5.42 +    strip_spaces_in_list (dropwhile (not_equal #"\n") cs)
    5.43 +  | strip_spaces_in_list (#"/" :: #"*" :: cs) = strip_c_style_comment cs
    5.44 +  | strip_spaces_in_list [c1] = if Char.isSpace c1 then "" else str c1
    5.45 +  | strip_spaces_in_list [c1, c2] =
    5.46 +    strip_spaces_in_list [c1] ^ strip_spaces_in_list [c2]
    5.47 +  | strip_spaces_in_list (c1 :: c2 :: c3 :: cs) =
    5.48 +    if Char.isSpace c1 then
    5.49 +      strip_spaces_in_list (c2 :: c3 :: cs)
    5.50 +    else if Char.isSpace c2 then
    5.51 +      if Char.isSpace c3 then
    5.52 +        strip_spaces_in_list (c1 :: c3 :: cs)
    5.53 +      else
    5.54 +        str c1 ^ (if forall is_ident_char [c1, c3] then " " else "") ^
    5.55 +        strip_spaces_in_list (c3 :: cs)
    5.56 +    else
    5.57 +      str c1 ^ strip_spaces_in_list (c2 :: c3 :: cs)
    5.58 +val strip_spaces = strip_spaces_in_list o String.explode
    5.59 +
    5.60 +val parse_keyword = Scan.this_string
    5.61 +
    5.62 +fun parse_file_path ("'" :: ss) =
    5.63 +    (takewhile (not_equal "'") ss |> implode,
    5.64 +     List.drop (dropwhile (not_equal "'") ss, 1))
    5.65 +  | parse_file_path ("\"" :: ss) =
    5.66 +    (takewhile (not_equal "\"") ss |> implode,
    5.67 +     List.drop (dropwhile (not_equal "\"") ss, 1))
    5.68 +  | parse_file_path _ = raise SYNTAX "invalid file path"
    5.69 +
    5.70 +fun parse_include x =
    5.71 +  let
    5.72 +    val (file_name, rest) =
    5.73 +      (parse_keyword "include" |-- $$ "(" |-- parse_file_path --| $$ ")"
    5.74 +       --| $$ ".") x
    5.75 +  in
    5.76 +    ((), raw_explode (strip_spaces (File.read (Path.explode file_name))) @ rest)
    5.77 +  end
    5.78 +
    5.79 +fun mk_anot phi = AConn (ANot, [phi])
    5.80 +fun mk_aconn c (phi1, phi2) = AConn (c, [phi1, phi2])
    5.81 +
    5.82 +val parse_dollar_name =
    5.83 +  Scan.repeat ($$ "$") -- Symbol.scan_id >> (fn (ss, s) => implode ss ^ s)
    5.84 +
    5.85 +fun parse_term x =
    5.86 +  (parse_dollar_name
    5.87 +   -- Scan.optional ($$ "(" |-- parse_terms --| $$ ")") [] >> ATerm) x
    5.88 +and parse_terms x = (parse_term ::: Scan.repeat ($$ "," |-- parse_term)) x
    5.89 +
    5.90 +(* Apply equal or not-equal to a term. *)
    5.91 +val parse_predicate_term =
    5.92 +  parse_term -- Scan.option (Scan.option ($$ "!") --| $$ "=" -- parse_term)
    5.93 +  >> (fn (u, NONE) => APred u
    5.94 +       | (u1, SOME (NONE, u2)) => APred (ATerm ("=", [u1, u2]))
    5.95 +       | (u1, SOME (SOME _, u2)) => mk_anot (APred (ATerm ("=", [u1, u2]))))
    5.96 +
    5.97 +fun fo_term_head (ATerm (s, _)) = s
    5.98 +
    5.99 +fun parse_formula x =
   5.100 +  (($$ "(" |-- parse_formula --| $$ ")"
   5.101 +    || ($$ "!" >> K AForall || $$ "?" >> K AExists)
   5.102 +       --| $$ "[" -- parse_terms --| $$ "]" --| $$ ":" -- parse_formula
   5.103 +       >> (fn ((q, ts), phi) => AQuant (q, map fo_term_head ts, phi))
   5.104 +    || $$ "~" |-- parse_formula >> mk_anot
   5.105 +    || parse_predicate_term)
   5.106 +   -- Scan.option ((Scan.this_string "=>" >> K AImplies
   5.107 +                    || Scan.this_string "<=>" >> K AIff
   5.108 +                    || Scan.this_string "<~>" >> K ANotIff
   5.109 +                    || Scan.this_string "<=" >> K AIf
   5.110 +                    || $$ "|" >> K AOr || $$ "&" >> K AAnd) -- parse_formula)
   5.111 +   >> (fn (phi1, NONE) => phi1
   5.112 +        | (phi1, SOME (c, phi2)) => mk_aconn c (phi1, phi2))) x
   5.113 +
   5.114 +val parse_fof_or_cnf =
   5.115 +  (parse_keyword "fof" || parse_keyword "cnf") |-- $$ "(" |--
   5.116 +  Scan.many (not_equal ",") |-- $$ "," |--
   5.117 +  (parse_keyword "axiom" || parse_keyword "definition"
   5.118 +   || parse_keyword "theorem" || parse_keyword "lemma"
   5.119 +   || parse_keyword "hypothesis" || parse_keyword "conjecture"
   5.120 +   || parse_keyword "negated_conjecture") --| $$ "," -- parse_formula
   5.121 +      --| $$ ")" --| $$ "."
   5.122 +  >> (fn ("conjecture", phi) => AConn (ANot, [phi]) | (_, phi) => phi)
   5.123 +
   5.124 +val parse_problem =
   5.125 +  Scan.repeat parse_include
   5.126 +  |-- Scan.repeat (parse_fof_or_cnf --| Scan.repeat parse_include)
   5.127 +
   5.128 +val parse_tptp_problem =
   5.129 +  Scan.finite Symbol.stopper
   5.130 +      (Scan.error (!! (fn _ => raise SYNTAX "malformed TPTP input")
   5.131 +                  parse_problem))
   5.132 +  o raw_explode o strip_spaces
   5.133 +
   5.134 +val boolT = @{typ bool}
   5.135 +val iotaT = @{typ iota}
   5.136 +val quantT = (iotaT --> boolT) --> boolT
   5.137 +
   5.138 +fun is_variable s = Char.isUpper (String.sub (s, 0))
   5.139 +
   5.140 +fun hol_term_from_fo_term res_T (ATerm (x, us)) =
   5.141 +  let val ts = map (hol_term_from_fo_term iotaT) us in
   5.142 +    list_comb ((case x of
   5.143 +                  "$true" => @{const_name True}
   5.144 +                | "$false" => @{const_name False}
   5.145 +                | "=" => @{const_name HOL.eq}
   5.146 +                | _ => x, map fastype_of ts ---> res_T)
   5.147 +               |> (if is_variable x then Free else Const), ts)
   5.148 +  end
   5.149 +
   5.150 +fun hol_prop_from_formula phi =
   5.151 +  case phi of
   5.152 +    AQuant (_, [], phi') => hol_prop_from_formula phi'
   5.153 +  | AQuant (q, x :: xs, phi') =>
   5.154 +    Const (case q of AForall => @{const_name All} | AExists => @{const_name Ex},
   5.155 +           quantT)
   5.156 +    $ lambda (Free (x, iotaT)) (hol_prop_from_formula (AQuant (q, xs, phi')))
   5.157 +  | AConn (ANot, [u']) => HOLogic.mk_not (hol_prop_from_formula u')
   5.158 +  | AConn (c, [u1, u2]) =>
   5.159 +    pairself hol_prop_from_formula (u1, u2)
   5.160 +    |> (case c of
   5.161 +          AAnd => HOLogic.mk_conj
   5.162 +        | AOr => HOLogic.mk_disj
   5.163 +        | AImplies => HOLogic.mk_imp
   5.164 +        | AIf => HOLogic.mk_imp o swap
   5.165 +        | AIff => HOLogic.mk_eq
   5.166 +        | ANotIff => HOLogic.mk_not o HOLogic.mk_eq
   5.167 +        | ANot => raise Fail "binary \"ANot\"")
   5.168 +  | AConn _ => raise Fail "malformed AConn"
   5.169 +  | APred u => hol_term_from_fo_term boolT u
   5.170 +
   5.171 +fun mk_all x t = Const (@{const_name All}, quantT) $ lambda x t
   5.172 +
   5.173 +fun close_hol_prop t = fold (mk_all o Free) (Term.add_frees t []) t
   5.174 +
   5.175 +fun pick_nits_in_fof_file file_name =
   5.176 +  case parse_tptp_problem (File.read (Path.explode file_name)) of
   5.177 +    (_, s :: ss) => raise SYNTAX ("cannot parse " ^ quote (implode (s :: ss)))
   5.178 +  | (phis, []) =>
   5.179 +    let
   5.180 +      val ts = map (HOLogic.mk_Trueprop o close_hol_prop
   5.181 +                    o hol_prop_from_formula) phis
   5.182 +(*
   5.183 +      val _ = warning (PolyML.makestring phis)
   5.184 +      val _ = app (warning o Syntax.string_of_term @{context}) ts
   5.185 +*)
   5.186 +      val state = Proof.init @{context}
   5.187 +      val params =
   5.188 +        [("card iota", "1\<midarrow>100"),
   5.189 +         ("card", "1\<midarrow>8"),
   5.190 +         ("box", "false"),
   5.191 +         ("sat_solver", "smart"),
   5.192 +         ("max_threads", "1"),
   5.193 +         ("batch_size", "10"),
   5.194 +         (* ("debug", "true"), *)
   5.195 +         ("verbose", "true"),
   5.196 +         (* ("overlord", "true"), *)
   5.197 +         ("show_consts", "true"),
   5.198 +         ("format", "1000"),
   5.199 +         ("max_potential", "0"),
   5.200 +         (* ("timeout", "240 s"), *)
   5.201 +         ("expect", "genuine")]
   5.202 +        |> Nitpick_Isar.default_params @{theory}
   5.203 +      val auto = false
   5.204 +      val i = 1
   5.205 +      val n = 1
   5.206 +      val step = 0
   5.207 +      val subst = []
   5.208 +    in
   5.209 +      Nitpick.pick_nits_in_term state params auto i n step subst ts
   5.210 +                                @{prop False} |> fst
   5.211 +    end
   5.212 +
   5.213 +end;