src/HOL/Tools/ATP/recon_parse.ML
author wenzelm
Wed, 13 Jul 2005 16:07:25 +0200
changeset 16804 3c339e1c069b
parent 16548 aa36ae6b955e
child 16840 3d5aad11bc24
permissions -rw-r--r--
open ReconPrelim ReconTranslateProof; removed second copy of exception ASSERTION;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
15789
4cb16144c81b added hearder lines and deleted some redundant material
paulson
parents: 15688
diff changeset
     1
(*  ID:         $Id$
4cb16144c81b added hearder lines and deleted some redundant material
paulson
parents: 15688
diff changeset
     2
    Author:     Claire Quigley
4cb16144c81b added hearder lines and deleted some redundant material
paulson
parents: 15688
diff changeset
     3
    Copyright   2004  University of Cambridge
4cb16144c81b added hearder lines and deleted some redundant material
paulson
parents: 15688
diff changeset
     4
*)
4cb16144c81b added hearder lines and deleted some redundant material
paulson
parents: 15688
diff changeset
     5
15642
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
     6
(*use "Translate_Proof";*)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
     7
(* Parsing functions *)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
     8
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
     9
(* Auxiliary functions *)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
    10
15684
5ec4d21889d6 Reconstruction code, now packaged to avoid name clashes
paulson
parents: 15642
diff changeset
    11
structure Recon_Parse =
5ec4d21889d6 Reconstruction code, now packaged to avoid name clashes
paulson
parents: 15642
diff changeset
    12
struct
5ec4d21889d6 Reconstruction code, now packaged to avoid name clashes
paulson
parents: 15642
diff changeset
    13
16804
3c339e1c069b open ReconPrelim ReconTranslateProof;
wenzelm
parents: 16548
diff changeset
    14
open ReconPrelim ReconTranslateProof;
15642
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
    15
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
    16
exception NOPARSE_WORD
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
    17
exception NOPARSE_NUM
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
    18
fun to_upper s = String.translate (Char.toString o Char.toUpper) s;
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
    19
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
    20
fun string2int s =
16804
3c339e1c069b open ReconPrelim ReconTranslateProof;
wenzelm
parents: 16548
diff changeset
    21
  (case Int.fromString s of SOME i => i
3c339e1c069b open ReconPrelim ReconTranslateProof;
wenzelm
parents: 16548
diff changeset
    22
  | NONE => raise ASSERTION "string -> int failed");
3c339e1c069b open ReconPrelim ReconTranslateProof;
wenzelm
parents: 16548
diff changeset
    23
15642
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
    24
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
    25
(* Parser combinators *)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
    26
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
    27
exception Noparse;
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
    28
exception SPASSError of string;
16478
d0a1f6231e2f Added VampCommunication.ML.
quigley
parents: 16418
diff changeset
    29
exception VampError of string;
d0a1f6231e2f Added VampCommunication.ML.
quigley
parents: 16418
diff changeset
    30
15642
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
    31
15688
adf0ba6353f3 fixed the syntax of infix declarations
paulson
parents: 15684
diff changeset
    32
fun (parser1 ++ parser2) input =
15642
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
    33
      let
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
    34
        val (result1, rest1) = parser1 input
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
    35
        val (result2, rest2) = parser2 rest1
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
    36
      in
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
    37
        ((result1, result2), rest2)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
    38
      end;
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
    39
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
    40
fun many parser input =
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
    41
      let   (* Tree * token list*)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
    42
        val (result, next) = parser input
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
    43
        val (results, rest) = many parser next
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
    44
      in
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
    45
        ((result::results), rest)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
    46
      end
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
    47
      handle Noparse => ([], input)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
    48
|            NOPARSE_WORD => ([], input)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
    49
|            NOPARSE_NUM  => ([], input);
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
    50
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
    51
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
    52
15688
adf0ba6353f3 fixed the syntax of infix declarations
paulson
parents: 15684
diff changeset
    53
fun (parser >> treatment) input =
15642
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
    54
      let
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
    55
        val (result, rest) = parser input
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
    56
      in
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
    57
        (treatment result, rest)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
    58
      end;
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
    59
15688
adf0ba6353f3 fixed the syntax of infix declarations
paulson
parents: 15684
diff changeset
    60
fun (parser1 || parser2) input = parser1 input
15642
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
    61
handle Noparse => parser2 input;
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
    62
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
    63
infixr 8 ++; infixr 7 >>; infixr 6 ||;
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
    64
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
    65
fun some p [] = raise Noparse
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
    66
  | some p (h::t) = if p h then (h, t) else raise Noparse;
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
    67
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
    68
fun a tok = some (fn item => item = tok);
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
    69
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
    70
fun finished input = if input = [] then (0, input) else raise Noparse;
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
    71
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
    72
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
    73
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
    74
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
    75
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
    76
  (* Parsing the output from gandalf *)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
    77
datatype token = Word of string
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
    78
               | Number of int
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
    79
               | Other of string
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
    80
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
    81
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
    82
      exception NOCUT
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
    83
      fun is_prefix [] l = true
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
    84
        | is_prefix (h::t) [] = false
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
    85
        | is_prefix (h::t) (h'::t') = (h = h') andalso is_prefix t t'
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
    86
      fun remove_prefix [] l = l
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
    87
        | remove_prefix (h::t) [] = raise (ASSERTION "can't remove prefix")
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
    88
        | remove_prefix (h::t) (h'::t') = remove_prefix t t'
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
    89
      fun ccut t [] = raise NOCUT
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
    90
        | ccut t s =
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
    91
            if is_prefix t s then ([], remove_prefix t s) else
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
    92
              let val (a, b) = ccut t (tl s) in ((hd s)::a, b) end
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
    93
      fun cut t s =
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
    94
        let
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
    95
          val t' = explode t
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
    96
          val s' = explode s
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
    97
          val (a, b) = ccut t' s'
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
    98
        in
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
    99
          (implode a, implode b)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   100
        end
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   101
    
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   102
      fun cut_exists t s
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   103
          = let val (a, b) = cut t s in true end handle NOCUT => false
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   104
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   105
      fun cut_before t s = let val (a, b) = cut t s in (a, t ^ b) end
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   106
      fun cut_after t s = let val (a, b) = cut t s in (a ^ t, b) end
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   107
    
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   108
15684
5ec4d21889d6 Reconstruction code, now packaged to avoid name clashes
paulson
parents: 15642
diff changeset
   109
    fun kill_lines 0 = Library.I
15642
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   110
      | kill_lines n = kill_lines (n - 1) o snd o cut_after "\n";
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   111
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   112
    (*fun extract_proof s
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   113
      = if cut_exists "EMPTY CLAUSE DERIVED" s then
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   114
          (kill_lines 6
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   115
           o snd o cut_after "EMPTY CLAUSE DERIVED"
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   116
           o fst o cut_after "contradiction.\n") s
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   117
        else
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   118
          raise (GandalfError "Couldn't find a proof.")
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   119
*)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   120
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   121
val proofstring =
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   122
"0:00:00.00 for the reduction.\
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   123
\\
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   124
\Here is a proof with depth 3, length 7 :\
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   125
\1[0:Inp] ||  -> P(xa)*.\
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   126
\2[0:Inp] ||  -> Q(xb)*.\
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   127
\3[0:Inp] || R(U)* -> .\
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   128
\4[0:Inp] || Q(U) P(V) -> R(x(V,U))*.\
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   129
\9[0:Res:4.2,3.0] || Q(U)*+ P(V)* -> .\
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   130
\11[0:Res:2.0,9.0] || P(U)* -> .\
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   131
\12[0:Res:1.0,11.0] ||  -> .\
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   132
\Formulae used in the proof :\
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   133
\\
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   134
\--------------------------SPASS-STOP------------------------------"
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   135
16418
5d0d24bd2c96 Multiple subgoals working.
quigley
parents: 16357
diff changeset
   136
fun extract_proof s
5d0d24bd2c96 Multiple subgoals working.
quigley
parents: 16357
diff changeset
   137
      = if cut_exists "Here is a proof with" s then
5d0d24bd2c96 Multiple subgoals working.
quigley
parents: 16357
diff changeset
   138
          (kill_lines 0
5d0d24bd2c96 Multiple subgoals working.
quigley
parents: 16357
diff changeset
   139
           o snd o cut_after ":"
5d0d24bd2c96 Multiple subgoals working.
quigley
parents: 16357
diff changeset
   140
           o snd o cut_after "Here is a proof with"
5d0d24bd2c96 Multiple subgoals working.
quigley
parents: 16357
diff changeset
   141
           o fst o cut_after " ||  -> .") s
5d0d24bd2c96 Multiple subgoals working.
quigley
parents: 16357
diff changeset
   142
        else if cut_exists "%================== Proof: ======================" s then
5d0d24bd2c96 Multiple subgoals working.
quigley
parents: 16357
diff changeset
   143
          (kill_lines 0
5d0d24bd2c96 Multiple subgoals working.
quigley
parents: 16357
diff changeset
   144
           o snd o cut_after "%================== Proof: ======================"
5d0d24bd2c96 Multiple subgoals working.
quigley
parents: 16357
diff changeset
   145
           o fst o cut_before "==============  End of proof. ==================") s
5d0d24bd2c96 Multiple subgoals working.
quigley
parents: 16357
diff changeset
   146
        else
5d0d24bd2c96 Multiple subgoals working.
quigley
parents: 16357
diff changeset
   147
          raise SPASSError "Couldn't find a proof."
15642
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   148
16418
5d0d24bd2c96 Multiple subgoals working.
quigley
parents: 16357
diff changeset
   149
(*fun extract_proof s
15642
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   150
      = if cut_exists "Here is a proof with" s then
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   151
          (kill_lines 0
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   152
           o snd o cut_after ":"
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   153
           o snd o cut_after "Here is a proof with"
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   154
           o fst o cut_after " ||  -> .") s
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   155
        else
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   156
          raise SPASSError "Couldn't find a proof."
16418
5d0d24bd2c96 Multiple subgoals working.
quigley
parents: 16357
diff changeset
   157
*)
15642
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   158
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   159
16478
d0a1f6231e2f Added VampCommunication.ML.
quigley
parents: 16418
diff changeset
   160
d0a1f6231e2f Added VampCommunication.ML.
quigley
parents: 16418
diff changeset
   161
d0a1f6231e2f Added VampCommunication.ML.
quigley
parents: 16418
diff changeset
   162
15642
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   163
fun several p = many (some p)
15684
5ec4d21889d6 Reconstruction code, now packaged to avoid name clashes
paulson
parents: 15642
diff changeset
   164
      fun collect (h, t) = h ^ (Utils.itlist (fn s1 => fn s2 => s1 ^ s2) t "")
15642
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   165
  
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   166
      fun lower_letter s = ("a" <= s) andalso (s <= "z")
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   167
      fun upper_letter s = ("A" <= s) andalso (s <= "Z")
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   168
      fun digit s = ("0" <= s) andalso (s <= "9")
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   169
      fun letter s = lower_letter s orelse upper_letter s
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   170
      fun alpha s = letter s orelse (s = "_")
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   171
      fun alphanum s = alpha s orelse digit s
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   172
      fun space s = (s = " ") orelse (s = "\n") orelse (s = "\t")
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   173
      (* FIX this is stopping it picking up numbers *)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   174
      val word = (some alpha ++ several alphanum) >> (Word o collect)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   175
      val number =
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   176
            (some digit ++ several digit) >> (Number o string2int o collect)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   177
      val other = some (K true) >> Other
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   178
      
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   179
      val token = (word || number || other) ++ several space >> fst
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   180
      val tokens = (several space ++ many token) >> snd
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   181
      val alltokens = (tokens ++ finished) >> fst
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   182
    
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   183
     (* val lex = fst ( alltokens ( (map str)  explode))*)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   184
     fun lex s =  alltokens  (explode s)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   185
16478
d0a1f6231e2f Added VampCommunication.ML.
quigley
parents: 16418
diff changeset
   186
d0a1f6231e2f Added VampCommunication.ML.
quigley
parents: 16418
diff changeset
   187
(*********************************************************)
d0a1f6231e2f Added VampCommunication.ML.
quigley
parents: 16418
diff changeset
   188
(*  Temporary code to "parse" Vampire proofs             *)
d0a1f6231e2f Added VampCommunication.ML.
quigley
parents: 16418
diff changeset
   189
(*********************************************************)
d0a1f6231e2f Added VampCommunication.ML.
quigley
parents: 16418
diff changeset
   190
d0a1f6231e2f Added VampCommunication.ML.
quigley
parents: 16418
diff changeset
   191
fun num_int (Number n) = n
d0a1f6231e2f Added VampCommunication.ML.
quigley
parents: 16418
diff changeset
   192
|   num_int _ = raise VampError "Not a number"
d0a1f6231e2f Added VampCommunication.ML.
quigley
parents: 16418
diff changeset
   193
d0a1f6231e2f Added VampCommunication.ML.
quigley
parents: 16418
diff changeset
   194
 fun takeUntil ch [] res  = (res, [])
d0a1f6231e2f Added VampCommunication.ML.
quigley
parents: 16418
diff changeset
   195
 |   takeUntil ch (x::xs) res = if   x = ch 
d0a1f6231e2f Added VampCommunication.ML.
quigley
parents: 16418
diff changeset
   196
                                then
d0a1f6231e2f Added VampCommunication.ML.
quigley
parents: 16418
diff changeset
   197
                                     (res, xs)
d0a1f6231e2f Added VampCommunication.ML.
quigley
parents: 16418
diff changeset
   198
                                else
d0a1f6231e2f Added VampCommunication.ML.
quigley
parents: 16418
diff changeset
   199
                                     takeUntil ch xs (res@[x])
d0a1f6231e2f Added VampCommunication.ML.
quigley
parents: 16418
diff changeset
   200
       
d0a1f6231e2f Added VampCommunication.ML.
quigley
parents: 16418
diff changeset
   201
fun linenums [] nums = nums
d0a1f6231e2f Added VampCommunication.ML.
quigley
parents: 16418
diff changeset
   202
|   linenums (x::xs) nums = let val (fst, rest ) = takeUntil (Other "%") (x::xs) []
d0a1f6231e2f Added VampCommunication.ML.
quigley
parents: 16418
diff changeset
   203
                                in 
d0a1f6231e2f Added VampCommunication.ML.
quigley
parents: 16418
diff changeset
   204
				  if rest = [] 
d0a1f6231e2f Added VampCommunication.ML.
quigley
parents: 16418
diff changeset
   205
				  then 
d0a1f6231e2f Added VampCommunication.ML.
quigley
parents: 16418
diff changeset
   206
				      nums
d0a1f6231e2f Added VampCommunication.ML.
quigley
parents: 16418
diff changeset
   207
				  else
16520
7a9cda53bfa2 Integrated vampire lemma code.
quigley
parents: 16478
diff changeset
   208
			          let val first = hd rest
7a9cda53bfa2 Integrated vampire lemma code.
quigley
parents: 16478
diff changeset
   209
				
16478
d0a1f6231e2f Added VampCommunication.ML.
quigley
parents: 16418
diff changeset
   210
			          in
16520
7a9cda53bfa2 Integrated vampire lemma code.
quigley
parents: 16478
diff changeset
   211
				    if (first = (Other "*") ) 
7a9cda53bfa2 Integrated vampire lemma code.
quigley
parents: 16478
diff changeset
   212
				    then 
7a9cda53bfa2 Integrated vampire lemma code.
quigley
parents: 16478
diff changeset
   213
					
7a9cda53bfa2 Integrated vampire lemma code.
quigley
parents: 16478
diff changeset
   214
					 linenums rest ((num_int (hd (tl rest)))::nums)
7a9cda53bfa2 Integrated vampire lemma code.
quigley
parents: 16478
diff changeset
   215
				     else
7a9cda53bfa2 Integrated vampire lemma code.
quigley
parents: 16478
diff changeset
   216
					  linenums rest ((num_int first)::nums)
16478
d0a1f6231e2f Added VampCommunication.ML.
quigley
parents: 16418
diff changeset
   217
			         end
d0a1f6231e2f Added VampCommunication.ML.
quigley
parents: 16418
diff changeset
   218
                                end
d0a1f6231e2f Added VampCommunication.ML.
quigley
parents: 16418
diff changeset
   219
16520
7a9cda53bfa2 Integrated vampire lemma code.
quigley
parents: 16478
diff changeset
   220
7a9cda53bfa2 Integrated vampire lemma code.
quigley
parents: 16478
diff changeset
   221
(* This relies on a Vampire proof line starting "% Number" or "% * Number"*)
7a9cda53bfa2 Integrated vampire lemma code.
quigley
parents: 16478
diff changeset
   222
(* Check this is right *)
7a9cda53bfa2 Integrated vampire lemma code.
quigley
parents: 16478
diff changeset
   223
7a9cda53bfa2 Integrated vampire lemma code.
quigley
parents: 16478
diff changeset
   224
fun get_linenums proofstr = let (*val s = extract_proof proofstr*)
7a9cda53bfa2 Integrated vampire lemma code.
quigley
parents: 16478
diff changeset
   225
                                val tokens = #1(lex proofstr)
16478
d0a1f6231e2f Added VampCommunication.ML.
quigley
parents: 16418
diff changeset
   226
	                 
d0a1f6231e2f Added VampCommunication.ML.
quigley
parents: 16418
diff changeset
   227
	                    in
d0a1f6231e2f Added VampCommunication.ML.
quigley
parents: 16418
diff changeset
   228
		                rev (linenums tokens [])
d0a1f6231e2f Added VampCommunication.ML.
quigley
parents: 16418
diff changeset
   229
		            end
d0a1f6231e2f Added VampCommunication.ML.
quigley
parents: 16418
diff changeset
   230
d0a1f6231e2f Added VampCommunication.ML.
quigley
parents: 16418
diff changeset
   231
(************************************************************)
d0a1f6231e2f Added VampCommunication.ML.
quigley
parents: 16418
diff changeset
   232
(************************************************************)
d0a1f6231e2f Added VampCommunication.ML.
quigley
parents: 16418
diff changeset
   233
d0a1f6231e2f Added VampCommunication.ML.
quigley
parents: 16418
diff changeset
   234
d0a1f6231e2f Added VampCommunication.ML.
quigley
parents: 16418
diff changeset
   235
(**************************************************)
d0a1f6231e2f Added VampCommunication.ML.
quigley
parents: 16418
diff changeset
   236
(* Code to parse SPASS proofs                     *)
d0a1f6231e2f Added VampCommunication.ML.
quigley
parents: 16418
diff changeset
   237
(**************************************************)
d0a1f6231e2f Added VampCommunication.ML.
quigley
parents: 16418
diff changeset
   238
15642
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   239
datatype Tree = Leaf of string
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   240
                | Branch of Tree * Tree
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   241
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   242
   
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   243
      fun number ((Number n)::rest) = (n, rest)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   244
        | number _ = raise NOPARSE_NUM
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   245
      fun word ((Word w)::rest) = (w, rest)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   246
        | word _ = raise NOPARSE_WORD
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   247
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   248
      fun other_char ( (Other p)::rest) = (p, rest)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   249
      | other_char _ =raise NOPARSE_WORD
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   250
     
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   251
      val number_list =
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   252
        (number ++ many number)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   253
        >> (fn (a, b) => (a::b))
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   254
     
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   255
      val term_num =
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   256
        (number ++ (a (Other ".")) ++ number) >> (fn (a, (_, c)) => (a, c))
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   257
16548
aa36ae6b955e Temporarily removed Rewrite from the translation code so that parsing with work on lists of numbers.
quigley
parents: 16520
diff changeset
   258
aa36ae6b955e Temporarily removed Rewrite from the translation code so that parsing with work on lists of numbers.
quigley
parents: 16520
diff changeset
   259
      val term_num_list = (term_num ++ many (a (Other ",") ++ term_num >> snd)
aa36ae6b955e Temporarily removed Rewrite from the translation code so that parsing with work on lists of numbers.
quigley
parents: 16520
diff changeset
   260
			   >> (fn (a, b) => (a::b)))
aa36ae6b955e Temporarily removed Rewrite from the translation code so that parsing with work on lists of numbers.
quigley
parents: 16520
diff changeset
   261
15642
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   262
      val axiom = (a (Word "Inp"))
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   263
            >> (fn (_) => Axiom)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   264
      
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   265
      
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   266
      val binary = (a (Word "Res")) ++ (a (Other ":"))
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   267
                   ++ term_num ++ (a (Other ","))
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   268
                   ++ term_num
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   269
            >> (fn (_, (_, (c, (_, e)))) => Binary (c, e))
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   270
      
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   271
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   272
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   273
      val factor = (a (Word "Fac")) ++ (a (Other ":")) 
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   274
                    ++ term_num ++ (a (Other ",")) 
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   275
                    ++ term_num
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   276
            >> (fn (_, (_, (c, (_, e)))) =>  Factor ((fst c), (snd c),(snd e)))
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   277
     
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   278
      val para  = (a (Word "SPm")) ++ (a (Other ":"))
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   279
                   ++ term_num ++ (a (Other ","))
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   280
                   ++ term_num
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   281
            >> (fn (_, (_, (c, (_, e)))) => Para (c, e))
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   282
      
16357
f1275d2a1dee All subgoals sent to the watcher at once now.
quigley
parents: 16061
diff changeset
   283
      val super_l  = (a (Word "SpL")) ++ (a (Other ":"))
f1275d2a1dee All subgoals sent to the watcher at once now.
quigley
parents: 16061
diff changeset
   284
                   ++ term_num ++ (a (Other ","))
f1275d2a1dee All subgoals sent to the watcher at once now.
quigley
parents: 16061
diff changeset
   285
                   ++ term_num
f1275d2a1dee All subgoals sent to the watcher at once now.
quigley
parents: 16061
diff changeset
   286
            >> (fn (_, (_, (c, (_, e)))) => Super_l (c, e))
f1275d2a1dee All subgoals sent to the watcher at once now.
quigley
parents: 16061
diff changeset
   287
f1275d2a1dee All subgoals sent to the watcher at once now.
quigley
parents: 16061
diff changeset
   288
f1275d2a1dee All subgoals sent to the watcher at once now.
quigley
parents: 16061
diff changeset
   289
      val super_r  = (a (Word "SpR")) ++ (a (Other ":"))
f1275d2a1dee All subgoals sent to the watcher at once now.
quigley
parents: 16061
diff changeset
   290
                   ++ term_num ++ (a (Other ","))
f1275d2a1dee All subgoals sent to the watcher at once now.
quigley
parents: 16061
diff changeset
   291
                   ++ term_num
f1275d2a1dee All subgoals sent to the watcher at once now.
quigley
parents: 16061
diff changeset
   292
            >> (fn (_, (_, (c, (_, e)))) => Super_r (c, e))
f1275d2a1dee All subgoals sent to the watcher at once now.
quigley
parents: 16061
diff changeset
   293
f1275d2a1dee All subgoals sent to the watcher at once now.
quigley
parents: 16061
diff changeset
   294
f1275d2a1dee All subgoals sent to the watcher at once now.
quigley
parents: 16061
diff changeset
   295
      val aed = (a (Word "AED")) ++ (a (Other ":")) ++ term_num
f1275d2a1dee All subgoals sent to the watcher at once now.
quigley
parents: 16061
diff changeset
   296
                 >> (fn (_, (_, c)) => Obvious ((fst c),(snd c)))
f1275d2a1dee All subgoals sent to the watcher at once now.
quigley
parents: 16061
diff changeset
   297
15642
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   298
      val rewrite = (a (Word "Rew")) ++ (a (Other ":")) 
16548
aa36ae6b955e Temporarily removed Rewrite from the translation code so that parsing with work on lists of numbers.
quigley
parents: 16520
diff changeset
   299
                    ++ term_num_list
aa36ae6b955e Temporarily removed Rewrite from the translation code so that parsing with work on lists of numbers.
quigley
parents: 16520
diff changeset
   300
            >> (fn (_, (_, (c))) =>  Rewrite (c))
15642
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   301
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   302
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   303
      val mrr = (a (Word "MRR")) ++ (a (Other ":"))
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   304
                   ++ term_num ++ (a (Other ","))
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   305
                   ++ term_num
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   306
            >> (fn (_, (_, (c, (_, e)))) => MRR (c, e))
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   307
16357
f1275d2a1dee All subgoals sent to the watcher at once now.
quigley
parents: 16061
diff changeset
   308
      val ssi = (a (Word "SSi")) ++ (a (Other ":"))
f1275d2a1dee All subgoals sent to the watcher at once now.
quigley
parents: 16061
diff changeset
   309
                   ++ term_num ++ (a (Other ","))
f1275d2a1dee All subgoals sent to the watcher at once now.
quigley
parents: 16061
diff changeset
   310
                   ++ term_num
f1275d2a1dee All subgoals sent to the watcher at once now.
quigley
parents: 16061
diff changeset
   311
            >> (fn (_, (_, (c, (_, e)))) => SortSimp (c, e))
f1275d2a1dee All subgoals sent to the watcher at once now.
quigley
parents: 16061
diff changeset
   312
f1275d2a1dee All subgoals sent to the watcher at once now.
quigley
parents: 16061
diff changeset
   313
    val unc = (a (Word "UnC")) ++ (a (Other ":"))
f1275d2a1dee All subgoals sent to the watcher at once now.
quigley
parents: 16061
diff changeset
   314
                   ++ term_num ++ (a (Other ","))
f1275d2a1dee All subgoals sent to the watcher at once now.
quigley
parents: 16061
diff changeset
   315
                   ++ term_num
f1275d2a1dee All subgoals sent to the watcher at once now.
quigley
parents: 16061
diff changeset
   316
            >> (fn (_, (_, (c, (_, e)))) => UnitConf (c, e))
f1275d2a1dee All subgoals sent to the watcher at once now.
quigley
parents: 16061
diff changeset
   317
f1275d2a1dee All subgoals sent to the watcher at once now.
quigley
parents: 16061
diff changeset
   318
15642
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   319
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   320
      val obv = (a (Word "Obv")) ++ (a (Other ":")) ++ term_num
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   321
                 >> (fn (_, (_, c)) => Obvious ((fst c),(snd c)))
16357
f1275d2a1dee All subgoals sent to the watcher at once now.
quigley
parents: 16061
diff changeset
   322
f1275d2a1dee All subgoals sent to the watcher at once now.
quigley
parents: 16061
diff changeset
   323
      val eqres = (a (Word "EqR")) ++ (a (Other ":")) ++ term_num
f1275d2a1dee All subgoals sent to the watcher at once now.
quigley
parents: 16061
diff changeset
   324
                 >> (fn (_, (_, c)) => EqualRes ((fst c),(snd c)))
f1275d2a1dee All subgoals sent to the watcher at once now.
quigley
parents: 16061
diff changeset
   325
   
f1275d2a1dee All subgoals sent to the watcher at once now.
quigley
parents: 16061
diff changeset
   326
      val con = (a (Word "Con")) ++ (a (Other ":")) ++ term_num
f1275d2a1dee All subgoals sent to the watcher at once now.
quigley
parents: 16061
diff changeset
   327
                 >> (fn (_, (_, c)) => Condense ((fst c),(snd c)))
f1275d2a1dee All subgoals sent to the watcher at once now.
quigley
parents: 16061
diff changeset
   328
15642
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   329
(*
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   330
      val hyper = a (Word "hyper")
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   331
                  ++ many ((a (Other ",") ++ number) >> snd)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   332
                  >> (Hyper o snd)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   333
*)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   334
     (* val method = axiom ||binary || factor || para || hyper*)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   335
16357
f1275d2a1dee All subgoals sent to the watcher at once now.
quigley
parents: 16061
diff changeset
   336
      val method = axiom || binary || factor || para ||super_l || super_r || rewrite || mrr || obv || aed || ssi || unc|| con
f1275d2a1dee All subgoals sent to the watcher at once now.
quigley
parents: 16061
diff changeset
   337
15642
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   338
      val binary_s = a (Word "binary_s") ++ a (Other ",") ++ term_num
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   339
            >> (fn (_, (_, a)) => Binary_s a)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   340
      val factor_s = a (Word "factor_s")
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   341
            >> (fn _ => Factor_s ())
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   342
      val demod_s = a (Word "demod")
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   343
                    ++ (many ((a (Other ",") ++ term_num) >> snd))
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   344
            >> (fn (_, a) => Demod_s a)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   345
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   346
      val hyper_s = a (Word "hyper_s")
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   347
                    ++ many ((a (Other ",") ++ number) >> snd)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   348
                    >> (Hyper_s o snd)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   349
      val simp_method = binary_s || factor_s || demod_s || hyper_s
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   350
      val simp = a (Other ",") ++ simp_method >> snd
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   351
      val simps = many simp
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   352
 
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   353
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   354
      val justification =
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   355
           a (Other "[") ++number ++ a (Other ":") ++ method ++ a (Other "]")
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   356
                 >> (fn (_,(_, (_,(b, _)))) => b)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   357
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   358
     
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   359
exception NOTERM
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   360
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   361
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   362
fun implode_with_space [] = implode []
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   363
|   implode_with_space [x] = implode [x]
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   364
|   implode_with_space (x::[y]) = x^" "^y
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   365
|   implode_with_space (x::xs) =  (x^" "^(implode_with_space xs))
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   366
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   367
(* FIX - should change the stars and pluses to many rather than explicit patterns *)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   368
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   369
(* FIX - add the other things later *)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   370
fun remove_typeinfo x  =  if (String.isPrefix "v_" x )
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   371
                            then 
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   372
                                 (String.substring (x,2, ((size x) - 2)))
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   373
                            else if (String.isPrefix "V_" x )
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   374
                                 then 
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   375
                                      (String.substring (x,2, ((size x) - 2)))
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   376
                                 else if (String.isPrefix "typ_" x )
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   377
                                      then 
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   378
                                          ""
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   379
                                      else if (String.isPrefix "Typ_" x )
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   380
                                           then 
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   381
                                                ""
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   382
                                           else  if (String.isPrefix "tconst_" x )
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   383
                                                 then 
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   384
                                                      ""
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   385
                                                 else  if (String.isPrefix "const_" x )
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   386
                                                       then 
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   387
                                                            (String.substring  (x,6, ((size x) - 6)))
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   388
                                                       else
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   389
                                                           x
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   390
                                               
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   391
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   392
fun term input = (  ntermlist ++ a (Other "-") ++ a (Other ">") ++ ptermlist >>(fn (a,(_,(_,b))) =>  (a@b))
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   393
                  ) input
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   394
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   395
(* pterms are terms from the rhs of the -> in the spass proof.  *)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   396
(* they should have a "~" in front of them so that they match with *)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   397
(* positive terms in the meta-clause *)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   398
(* nterm are terms from the lhs of the spass proof, and shouldn't *)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   399
(* "~"s added  word ++ a (Other "(") ++ arglist ++ a (Other ")") >> (fn (a,(_,(b,_ ))) =>  (a^" "^b)) *)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   400
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   401
and  pterm input = (
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   402
           peqterm >> (fn (a) => a)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   403
        
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   404
         || word ++ a (Other "(") ++ arglist ++  a (Other ")") ++ a (Other "*")++ a (Other "*") ++ a (Other "+")
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   405
           >> (fn (a, (_,(b, (_,(_,_))))) =>  ("~"^" "^(remove_typeinfo a)^" "^b))
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   406
         
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   407
        || word ++ a (Other "(") ++ arglist ++  a (Other ")") ++ a (Other "*") ++ a (Other "+")
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   408
           >> (fn ( a, (_,(b, (_,(_,_))))) =>  ("~"^" "^(remove_typeinfo a)^" "^b))
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   409
        
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   410
        || word ++ a (Other "(") ++ arglist ++ a (Other ")") ++ a (Other "*") ++ a (Other "*")
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   411
           >> (fn ( a, (_,(b, (_,(_,_))))) =>  ("~"^" "^(remove_typeinfo a)^" "^b))
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   412
        
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   413
	|| word ++ a (Other "(") ++ arglist ++ a (Other ")") ++ a (Other "*")
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   414
           >> (fn (a, (_,(b, (_,_)))) =>  ("~"^" "^(remove_typeinfo a)^" "^b))
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   415
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   416
        || word ++ a (Other "(") ++  arglist ++ a (Other ")") 
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   417
           >> (fn ( a, (_,(b,_ ))) => ("~"^" "^(remove_typeinfo a)^" "^b))
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   418
16357
f1275d2a1dee All subgoals sent to the watcher at once now.
quigley
parents: 16061
diff changeset
   419
        || word ++ a (Other "*") >> (fn (w,b) => "~"^" "^(remove_typeinfo w))
f1275d2a1dee All subgoals sent to the watcher at once now.
quigley
parents: 16061
diff changeset
   420
f1275d2a1dee All subgoals sent to the watcher at once now.
quigley
parents: 16061
diff changeset
   421
        || word                  >> (fn w => "~"^" "^(remove_typeinfo w))) input
15642
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   422
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   423
and  nterm input =
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   424
    
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   425
       (  
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   426
           neqterm >> (fn (a) => a)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   427
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   428
        || word ++ a (Other "(") ++ arglist ++ a (Other ")") ++ a (Other "*") ++ a (Other "*") ++ a (Other "+")
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   429
           >> (fn ( a, (_,(b, (_,(_,_))))) =>  ((remove_typeinfo a)^" "^b))
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   430
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   431
        || word ++ a (Other "(") ++ arglist ++ a (Other ")") ++ a (Other "*") ++ a (Other "+")
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   432
           >> (fn ( a, (_,(b, (_,(_,_))))) =>  ((remove_typeinfo a)^" "^b))
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   433
        
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   434
        || word ++ a (Other "(") ++ arglist ++ a (Other ")") ++ a (Other "*") ++ a (Other "*")
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   435
           >> (fn ( a, (_,(b, (_,(_,_))))) =>  ((remove_typeinfo a)^" "^b))
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   436
        
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   437
	|| word ++ a (Other "(") ++ arglist ++ a (Other ")") ++ a (Other "*")
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   438
           >> (fn ( a, (_,(b, (_,_)))) =>  ((remove_typeinfo a)^" "^b))
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   439
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   440
        || word ++ a (Other "(") ++ arglist ++ a (Other ")") 
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   441
           >> (fn (a, (_,(b,_ ))) => ((remove_typeinfo a)^" "^b))
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   442
16357
f1275d2a1dee All subgoals sent to the watcher at once now.
quigley
parents: 16061
diff changeset
   443
        || word ++ a (Other "*") >> (fn (w,b) =>  (remove_typeinfo w)) 
f1275d2a1dee All subgoals sent to the watcher at once now.
quigley
parents: 16061
diff changeset
   444
        || word                  >> (fn w =>  (remove_typeinfo w)) 
f1275d2a1dee All subgoals sent to the watcher at once now.
quigley
parents: 16061
diff changeset
   445
         ) input 
15642
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   446
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   447
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   448
and peqterm input =(
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   449
 
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   450
         a (Word "equal") ++  a (Other "(") ++ nterm ++ a (Other ",") ++ nterm ++ a (Other ")") 
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   451
         ++ a (Other "*") ++ a (Other "*") ++ a (Other "+")
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   452
            >> (fn (_,(_,(a,(_,(b,(_,(_,(_,_)))))))) => (a^" ~= "^b))
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   453
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   454
      || a (Word "equal") ++  a (Other "(") ++ nterm ++ a (Other ",") ++ nterm ++ a (Other ")") 
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   455
          ++ a (Other "*") ++ a (Other "+")
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   456
            >> (fn (_,(_,(a,(_,(b,(_,(_,_))))))) => (a^" ~= "^b))
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   457
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   458
      || a (Word "equal") ++  a (Other "(") ++ nterm ++ a (Other ",") ++ nterm ++ a (Other ")") 
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   459
         ++ a (Other "*") ++ a (Other "*")
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   460
            >> (fn (_,(_,(a,(_,(b,(_,(_,_))))))) => (a^" ~= "^b))
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   461
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   462
      || a (Word "equal") ++  a (Other "(") ++ nterm ++ a (Other ",") ++ nterm ++ a (Other ")") 
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   463
         ++ a (Other "*") 
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   464
            >> (fn (_,(_,(a,(_,(b,(_,_)))))) => (a^" ~= "^b))
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   465
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   466
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   467
       ||a (Word "equal") ++  a (Other "(") ++ nterm ++ a (Other ",") ++ nterm ++ a (Other ")") 
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   468
            >> (fn (_,(_,(a,(_,(b,_))))) => (a^" ~= "^b))) input
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   469
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   470
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   471
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   472
and neqterm input =(
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   473
 
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   474
         a (Word "equal") ++  a (Other "(") ++ nterm ++ a (Other ",") ++ nterm ++ a (Other ")") 
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   475
         ++ a (Other "*") ++ a (Other "*") ++ a (Other "+")
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   476
            >> (fn (_,(_,(a,(_,(b,(_,(_,(_,_)))))))) => (a^" = "^b))
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   477
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   478
      || a (Word "equal") ++  a (Other "(") ++ nterm ++ a (Other ",") ++ nterm ++ a (Other ")") 
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   479
          ++ a (Other "*") ++ a (Other "+")
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   480
            >> (fn (_,(_,(a,(_,(b,(_,(_,_))))))) => (a^" = "^b))
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   481
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   482
      || a (Word "equal") ++  a (Other "(") ++ nterm ++ a (Other ",") ++ nterm ++ a (Other ")") 
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   483
         ++ a (Other "*") ++ a (Other "*")
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   484
            >> (fn (_,(_,(a,(_,(b,(_,(_,_))))))) => (a^" = "^b))
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   485
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   486
      || a (Word "equal") ++  a (Other "(") ++ nterm ++ a (Other ",") ++ nterm ++ a (Other ")") 
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   487
         ++ a (Other "*") 
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   488
            >> (fn (_,(_,(a,(_,(b,(_,_)))))) => (a^" = "^b))
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   489
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   490
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   491
       ||a (Word "equal") ++  a (Other "(") ++ nterm ++ a (Other ",") ++ nterm ++ a (Other ")") 
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   492
            >> (fn (_,(_,(a,(_,(b,_))))) => (a^" = "^b))) input
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   493
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   494
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   495
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   496
and ptermlist input = (many  pterm
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   497
                      >> (fn (a) => (a))) input
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   498
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   499
and ntermlist input = (many  nterm
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   500
                      >> (fn (a) => (a))) input
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   501
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   502
(*and arglist input = (    nterm >> (fn (a) => (a))
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   503
                     ||  nterm ++ many (a (Other ",") ++ nterm >> snd)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   504
                      >> (fn (a, b) => (a^" "^(implode_with_space b)))) input*)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   505
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   506
and arglist input = (   nterm ++ many (a (Other ",") ++ nterm >> snd)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   507
                      >> (fn (a, b) => (a^" "^(implode_with_space b))) 
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   508
                      ||    nterm >> (fn (a) => (a)))input
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   509
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   510
 val clause =  term
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   511
15919
b30a35432f5a Replaced reference to SPASS with general one - set SPASS_HOME in settings file.
quigley
parents: 15789
diff changeset
   512
b30a35432f5a Replaced reference to SPASS with general one - set SPASS_HOME in settings file.
quigley
parents: 15789
diff changeset
   513
b30a35432f5a Replaced reference to SPASS with general one - set SPASS_HOME in settings file.
quigley
parents: 15789
diff changeset
   514
 (*val line = number ++ justification ++ a (Other "|") ++ 
15642
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   515
            a (Other "|") ++ clause ++ a (Other ".")
15919
b30a35432f5a Replaced reference to SPASS with general one - set SPASS_HOME in settings file.
quigley
parents: 15789
diff changeset
   516
          >> (fn (a, (z, (_,( _, (c, _))))) => (a, z, c))*)
b30a35432f5a Replaced reference to SPASS with general one - set SPASS_HOME in settings file.
quigley
parents: 15789
diff changeset
   517
b30a35432f5a Replaced reference to SPASS with general one - set SPASS_HOME in settings file.
quigley
parents: 15789
diff changeset
   518
b30a35432f5a Replaced reference to SPASS with general one - set SPASS_HOME in settings file.
quigley
parents: 15789
diff changeset
   519
(* not entirely sure nterm is right here, but I don't think you get negative things before the ||s *)
b30a35432f5a Replaced reference to SPASS with general one - set SPASS_HOME in settings file.
quigley
parents: 15789
diff changeset
   520
 val line = number ++ justification ++ many( nterm) ++ a (Other "|") ++ 
b30a35432f5a Replaced reference to SPASS with general one - set SPASS_HOME in settings file.
quigley
parents: 15789
diff changeset
   521
            a (Other "|") ++ clause ++ a (Other ".")
b30a35432f5a Replaced reference to SPASS with general one - set SPASS_HOME in settings file.
quigley
parents: 15789
diff changeset
   522
          >> (fn (a, (z, (w, (_,( _, (c, _)))))) => (a, z,(w@ c)))
b30a35432f5a Replaced reference to SPASS with general one - set SPASS_HOME in settings file.
quigley
parents: 15789
diff changeset
   523
       
b30a35432f5a Replaced reference to SPASS with general one - set SPASS_HOME in settings file.
quigley
parents: 15789
diff changeset
   524
b30a35432f5a Replaced reference to SPASS with general one - set SPASS_HOME in settings file.
quigley
parents: 15789
diff changeset
   525
15642
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   526
 val lines = many line
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   527
 val alllines = (lines ++ finished) >> fst
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   528
    
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   529
 val parse = fst o alllines
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   530
 val s = proofstring;
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   531
 
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   532
 
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   533
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   534
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   535
fun dropUntilNot ch []   = ( [])
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   536
 |   dropUntilNot ch (x::xs)  = if  not(x = ch )
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   537
                                then
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   538
                                     (x::xs)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   539
                                else
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   540
                                     dropUntilNot ch xs
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   541
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   542
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   543
fun remove_spaces str  []  = str
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   544
|   remove_spaces str (x::[]) = if x = " " 
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   545
                                then 
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   546
                                    str 
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   547
                                else 
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   548
                                    (str^x)
16061
8a139c1557bf A new structure and reduced indentation
paulson
parents: 15919
diff changeset
   549
|   remove_spaces str (x::xs) = 
8a139c1557bf A new structure and reduced indentation
paulson
parents: 15919
diff changeset
   550
      let val (first, rest) = ReconOrderClauses.takeUntil " " (x::xs) []
8a139c1557bf A new structure and reduced indentation
paulson
parents: 15919
diff changeset
   551
	  val (next) = dropUntilNot " " rest 
8a139c1557bf A new structure and reduced indentation
paulson
parents: 15919
diff changeset
   552
      in 
8a139c1557bf A new structure and reduced indentation
paulson
parents: 15919
diff changeset
   553
	  if next = []
8a139c1557bf A new structure and reduced indentation
paulson
parents: 15919
diff changeset
   554
	  then 
8a139c1557bf A new structure and reduced indentation
paulson
parents: 15919
diff changeset
   555
	       (str^(implode first)) 
8a139c1557bf A new structure and reduced indentation
paulson
parents: 15919
diff changeset
   556
	  else remove_spaces  (str^(implode first)^" ") next 
8a139c1557bf A new structure and reduced indentation
paulson
parents: 15919
diff changeset
   557
      end
15642
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   558
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   559
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   560
fun remove_space_strs clsstrs = map (remove_spaces "") (map explode clsstrs)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   561
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   562
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   563
fun all_spaces xs = List.filter  (not_equal " " ) xs
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   564
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   565
fun just_change_space []  = []
16061
8a139c1557bf A new structure and reduced indentation
paulson
parents: 15919
diff changeset
   566
|   just_change_space ((clausenum, step, strs)::xs) =
8a139c1557bf A new structure and reduced indentation
paulson
parents: 15919
diff changeset
   567
      let val newstrs = remove_space_strs strs
8a139c1557bf A new structure and reduced indentation
paulson
parents: 15919
diff changeset
   568
      in
8a139c1557bf A new structure and reduced indentation
paulson
parents: 15919
diff changeset
   569
	 if (all_spaces newstrs = [] ) (* all type_info *)
8a139c1557bf A new structure and reduced indentation
paulson
parents: 15919
diff changeset
   570
	 then    
8a139c1557bf A new structure and reduced indentation
paulson
parents: 15919
diff changeset
   571
	    (clausenum, step, newstrs)::(just_change_space xs)
8a139c1557bf A new structure and reduced indentation
paulson
parents: 15919
diff changeset
   572
	 else 
8a139c1557bf A new structure and reduced indentation
paulson
parents: 15919
diff changeset
   573
	     (clausenum, step, newstrs)::(just_change_space xs) 
8a139c1557bf A new structure and reduced indentation
paulson
parents: 15919
diff changeset
   574
      end;
15642
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   575
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   576
fun change_space []  = []
16061
8a139c1557bf A new structure and reduced indentation
paulson
parents: 15919
diff changeset
   577
|   change_space ((clausenum, step, strs)::xs) = 
8a139c1557bf A new structure and reduced indentation
paulson
parents: 15919
diff changeset
   578
      let val newstrs = remove_space_strs strs
8a139c1557bf A new structure and reduced indentation
paulson
parents: 15919
diff changeset
   579
      in
8a139c1557bf A new structure and reduced indentation
paulson
parents: 15919
diff changeset
   580
	 if (all_spaces newstrs = [] ) (* all type_info *)
8a139c1557bf A new structure and reduced indentation
paulson
parents: 15919
diff changeset
   581
	 then    
8a139c1557bf A new structure and reduced indentation
paulson
parents: 15919
diff changeset
   582
	    (clausenum, step, T_info, newstrs)::(change_space xs)
8a139c1557bf A new structure and reduced indentation
paulson
parents: 15919
diff changeset
   583
	 else 
8a139c1557bf A new structure and reduced indentation
paulson
parents: 15919
diff changeset
   584
	     (clausenum, step, P_info, newstrs)::(change_space xs) 
8a139c1557bf A new structure and reduced indentation
paulson
parents: 15919
diff changeset
   585
      end
15642
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   586
15684
5ec4d21889d6 Reconstruction code, now packaged to avoid name clashes
paulson
parents: 15642
diff changeset
   587
end;