src/HOL/Tools/ATP/recon_transfer_proof.ML
author quigley
Wed Jun 22 20:26:31 2005 +0200 (2005-06-22)
changeset 16548 aa36ae6b955e
parent 16520 7a9cda53bfa2
child 16803 014090d1e64b
permissions -rw-r--r--
Temporarily removed Rewrite from the translation code so that parsing with work on lists of numbers.
Will now signal if ATP has run out of time and then kill the watcher.
paulson@15789
     1
(*  ID:         $Id$
wenzelm@16259
     2
    Author:     Claire Quigley
wenzelm@16259
     3
    Copyright   2004  University of Cambridge
paulson@15789
     4
*)
paulson@15789
     5
quigley@15642
     6
(******************)
quigley@15642
     7
(* complete later *)
quigley@15642
     8
(******************)
quigley@15642
     9
paulson@15684
    10
structure Recon_Transfer =
paulson@15684
    11
struct
paulson@15684
    12
open Recon_Parse
paulson@15684
    13
infixr 8 ++; infixr 7 >>; infixr 6 ||;
paulson@15684
    14
quigley@15642
    15
fun not_newline ch = not (ch = "\n");
quigley@15642
    16
quigley@15642
    17
quigley@15642
    18
quigley@15919
    19
(*
quigley@15919
    20
fun fill_cls_array array n [] = ()
quigley@15919
    21
|   fill_cls_array array n (x::xs) = let val _ = Array.update (array, n,x)
quigley@15919
    22
                                     in
quigley@15919
    23
                                        fill_cls_array array (n+1) (xs)
quigley@15919
    24
                                     end;
quigley@15919
    25
quigley@15919
    26
quigley@15919
    27
quigley@15919
    28
fun memo_add_clauses ((name:string, (cls:Thm.thm list)), symtable)=
quigley@15919
    29
                        symtable := Symtab.update((name , cls), !symtable);
quigley@15919
    30
      	       
quigley@15919
    31
quigley@15919
    32
fun memo_add_all ([], symtable) = ()
quigley@15919
    33
|   memo_add_all ((x::xs),symtable) = let val _ = memo_add_clauses (x, symtable)
quigley@15919
    34
                           in
quigley@15919
    35
                               memo_add_all (xs, symtable)
quigley@15919
    36
                           end
quigley@15919
    37
quigley@15919
    38
fun memo_find_clause (name, (symtable: Thm.thm list Symtab.table ref)) = case Symtab.lookup (!symtable,name) of
quigley@15919
    39
      	        NONE =>  []
quigley@15919
    40
                |SOME cls  => cls ;
quigley@15919
    41
      	        	
quigley@15919
    42
quigley@15919
    43
fun retrieve_clause array symtable clausenum = let
quigley@15919
    44
                                                  val (name, clnum) = Array.sub(array, clausenum)
quigley@15919
    45
                                                  val clauses = memo_find_clause (name, symtable)
quigley@15919
    46
                                                  val clause = get_nth clnum clauses
quigley@15919
    47
                                               in
quigley@15919
    48
                                                  (name, clause)
quigley@15919
    49
                                               end
quigley@15919
    50
 *)                                             
quigley@15919
    51
quigley@15642
    52
(* Versions that include type information *)
quigley@15642
    53
 
paulson@16157
    54
fun string_of_thm thm =
paulson@16157
    55
  let val _ = set show_sorts
paulson@16157
    56
      val str = Display.string_of_thm thm
paulson@16157
    57
      val no_returns =List.filter not_newline (explode str)
paulson@16157
    58
      val _ = reset show_sorts
paulson@16157
    59
  in 
paulson@16157
    60
      implode no_returns
paulson@16157
    61
  end
quigley@15642
    62
quigley@15642
    63
quigley@15642
    64
(* check separate args in the watcher program for separating strings with a * or ; or something *)
quigley@15642
    65
quigley@15642
    66
fun clause_strs_to_string [] str = str
quigley@15642
    67
|   clause_strs_to_string (x::xs) str = clause_strs_to_string xs (str^x^"%")
quigley@15642
    68
quigley@15642
    69
fun thmvars_to_string [] str = str
quigley@15642
    70
|   thmvars_to_string (x::xs) str = thmvars_to_string xs (str^x^"%")
quigley@15642
    71
quigley@15642
    72
quigley@15642
    73
fun proofstep_to_string Axiom = "Axiom()"
paulson@16091
    74
|   proofstep_to_string  (Binary ((a,b), (c,d)))=
paulson@16091
    75
      "Binary(("^(string_of_int a)^","^(string_of_int b)^"),("^(string_of_int c)^","^(string_of_int d)^"))"
paulson@16091
    76
|   proofstep_to_string (Factor (a,b,c)) =
paulson@16091
    77
      "Factor("^(string_of_int a)^","^(string_of_int b)^","^(string_of_int c)^")"
paulson@16091
    78
|   proofstep_to_string  (Para ((a,b), (c,d)))= 
paulson@16091
    79
      "Para(("^(string_of_int a)^","^(string_of_int b)^"),("^(string_of_int c)^","^(string_of_int d)^"))"
paulson@16091
    80
|   proofstep_to_string  (MRR ((a,b), (c,d))) =
paulson@16091
    81
      "MRR(("^(string_of_int a)^","^(string_of_int b)^"),("^(string_of_int c)^","^(string_of_int d)^"))"
quigley@16548
    82
(*|   proofstep_to_string (Rewrite((a,b),(c,d))) =
quigley@16548
    83
      "Rewrite(("^(string_of_int a)^","^(string_of_int b)^"),("^(string_of_int c)^","^(string_of_int d)^"))"*)
quigley@15642
    84
quigley@15642
    85
fun list_to_string [] liststr = liststr
quigley@15642
    86
|   list_to_string (x::[]) liststr = liststr^(string_of_int x)
quigley@15642
    87
|   list_to_string (x::xs) liststr = list_to_string xs (liststr^(string_of_int x)^",")
quigley@15642
    88
quigley@15642
    89
paulson@16091
    90
fun proof_to_string (num,(step,clause_strs, thmvars)) = (string_of_int num)^(proofstep_to_string step)^"["^(clause_strs_to_string clause_strs "")^"]["^(thmvars_to_string thmvars "")^"]"
quigley@15642
    91
 
quigley@15642
    92
quigley@15642
    93
fun proofs_to_string [] str = str
quigley@15642
    94
|   proofs_to_string (x::xs) str = let val newstr = proof_to_string x 
quigley@15642
    95
                                   in
quigley@15642
    96
                                       proofs_to_string xs (str^newstr)
quigley@15642
    97
                                   end
quigley@15642
    98
quigley@15642
    99
quigley@15642
   100
quigley@15642
   101
fun init_proofstep_to_string (num, step, clause_strs) = (string_of_int num)^" "^(proofstep_to_string step)^" "^(clause_strs_to_string clause_strs "")^" "
quigley@15642
   102
quigley@15642
   103
fun init_proofsteps_to_string [] str = str
quigley@15642
   104
|   init_proofsteps_to_string (x::xs) str = let val newstr = init_proofstep_to_string x 
quigley@15642
   105
                                   in
quigley@15642
   106
                                       init_proofsteps_to_string xs (str^newstr)
quigley@15642
   107
                                   end
quigley@15642
   108
  
quigley@15642
   109
quigley@15642
   110
quigley@15642
   111
(*** get a string representing the Isabelle ordered axioms ***)
quigley@15642
   112
paulson@16061
   113
fun origAx_to_string (num,(meta,thmvars)) =
paulson@16061
   114
    let val clause_strs = ReconOrderClauses.get_meta_lits_bracket meta
paulson@16061
   115
    in
paulson@16091
   116
       (string_of_int num)^"OrigAxiom()["^
paulson@16091
   117
       (clause_strs_to_string clause_strs "")^"]["^
paulson@16061
   118
       (thmvars_to_string thmvars "")^"]"
paulson@16061
   119
    end
quigley@15642
   120
quigley@15642
   121
quigley@15642
   122
fun  origAxs_to_string [] str = str
quigley@15642
   123
|   origAxs_to_string (x::xs) str = let val newstr = origAx_to_string x 
quigley@15642
   124
                                   in
quigley@15642
   125
                                       origAxs_to_string xs (str^newstr)
quigley@15642
   126
                                   end
quigley@15642
   127
quigley@15642
   128
quigley@15642
   129
(*** get a string representing the Isabelle ordered axioms not used in the spass proof***)
quigley@15642
   130
paulson@16061
   131
fun extraAx_to_string (num, (meta,thmvars)) =
paulson@16061
   132
   let val clause_strs = ReconOrderClauses.get_meta_lits_bracket meta
paulson@16061
   133
   in
paulson@16091
   134
      (string_of_int num)^"ExtraAxiom()["^
paulson@16061
   135
      (clause_strs_to_string clause_strs "")^"]"^
paulson@16061
   136
      "["^(thmvars_to_string thmvars "")^"]"
paulson@16061
   137
   end;
quigley@15642
   138
paulson@16061
   139
fun extraAxs_to_string [] str = str
paulson@16061
   140
|   extraAxs_to_string (x::xs) str =
paulson@16061
   141
      let val newstr = extraAx_to_string x 
paulson@16061
   142
      in
paulson@16061
   143
	  extraAxs_to_string xs (str^newstr)
paulson@16061
   144
      end;
quigley@15642
   145
quigley@15642
   146
fun is_axiom ( num:int,Axiom, str) = true
quigley@15642
   147
|   is_axiom (num, _,_) = false
quigley@15642
   148
quigley@15642
   149
fun get_init_axioms xs = List.filter (is_axiom) ( xs)
quigley@15642
   150
quigley@15642
   151
fun get_step_nums [] nums = nums
quigley@15642
   152
|   get_step_nums (( num:int,Axiom, str)::xs) nums = get_step_nums xs (nums@[num])
quigley@15642
   153
paulson@15774
   154
exception Noassoc;
paulson@15774
   155
paulson@15774
   156
fun assoc_snd a [] = raise Noassoc
quigley@15642
   157
  | assoc_snd a ((x, y)::t) = if a = y then x else assoc_snd a t;
quigley@15642
   158
quigley@15642
   159
(* change to be something using check_order  instead of a = y --> returns true if ASSERTION not raised in checkorder, false otherwise *)
quigley@15642
   160
quigley@15642
   161
(*fun get_assoc_snds [] xs assocs= assocs
quigley@15642
   162
|   get_assoc_snds (x::xs) ys assocs = get_assoc_snds xs ys (assocs@[((assoc_snd x ys))])
quigley@15642
   163
*)
quigley@15642
   164
(*FIX - should this have vars in it? *)
paulson@16061
   165
fun there_out_of_order xs ys = (ReconOrderClauses.checkorder xs ys [] ([],[],[]); true) 
paulson@15774
   166
                               handle _ => false
quigley@15642
   167
paulson@15774
   168
fun assoc_out_of_order a [] = raise Noassoc
quigley@15642
   169
|   assoc_out_of_order a ((b,c)::t) = if there_out_of_order a c then b else assoc_out_of_order a t;
quigley@15642
   170
quigley@15642
   171
fun get_assoc_snds [] xs assocs= assocs
quigley@15642
   172
|   get_assoc_snds (x::xs) ys assocs = get_assoc_snds xs ys (assocs@[((assoc_out_of_order x ys))])
quigley@15642
   173
quigley@15642
   174
fun add_if_not_inlist [] xs newlist = newlist
paulson@16157
   175
|   add_if_not_inlist (y::ys) xs newlist = if (not (y mem xs)) then 
quigley@15642
   176
                                      add_if_not_inlist ys xs (y::newlist)
quigley@15642
   177
                                        else add_if_not_inlist ys xs (newlist)
quigley@15642
   178
paulson@15700
   179
(*Flattens a list of list of strings to one string*)
paulson@15700
   180
fun onestr ls = String.concat (map String.concat ls);
quigley@15642
   181
quigley@15642
   182
fun thmstrings [] str = str
quigley@15642
   183
|   thmstrings (x::xs) str = thmstrings xs (str^(string_of_thm x))
quigley@15642
   184
quigley@15919
   185
fun is_clasimp_ax clasimp_num n = n <=clasimp_num 
quigley@15642
   186
quigley@15919
   187
quigley@15919
   188
quigley@15919
   189
fun retrieve_axioms clause_arr  [] = []
quigley@15919
   190
|   retrieve_axioms clause_arr  (x::xs) =  [Array.sub(clause_arr, x)]@
quigley@15919
   191
 						     (retrieve_axioms clause_arr  xs)
quigley@15919
   192
quigley@16156
   193
fun subone x = x - 1
quigley@16156
   194
quigley@16156
   195
fun numstr [] = ""
quigley@16156
   196
|   numstr (x::xs) = (string_of_int x)^"%"^(numstr xs)
quigley@16156
   197
quigley@15919
   198
quigley@15919
   199
(* retrieve the axioms that were obtained from the clasimpset *)
quigley@15919
   200
quigley@15919
   201
fun get_clasimp_cls clause_arr clasimp_num step_nums = 
paulson@16157
   202
    let val realnums = map subone step_nums	
paulson@16157
   203
	val clasimp_nums = List.filter (is_clasimp_ax (clasimp_num - 1)) realnums
quigley@16478
   204
(*	val axnums = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "axnums")))     
paulson@16157
   205
	val _ = TextIO.output(axnums,(numstr clasimp_nums))
quigley@16478
   206
	val _ = TextIO.closeOut(axnums)*)
paulson@16157
   207
    in
paulson@16157
   208
	retrieve_axioms clause_arr  clasimp_nums
paulson@16157
   209
    end
quigley@15919
   210
quigley@16156
   211
quigley@16357
   212
quigley@16357
   213
(*****************************************************)
quigley@16357
   214
(* get names of clasimp axioms used                  *)
quigley@16357
   215
(*****************************************************)
quigley@16156
   216
paulson@16157
   217
 fun get_axiom_names proof_steps thms (clause_arr:(ResClause.clause * thm) Array.array) num_of_clauses  =
paulson@16157
   218
   let 
paulson@16157
   219
     (* not sure why this is necessary again, but seems to be *)
paulson@16157
   220
      val _ = (print_mode := (Library.gen_rems (op =) (! print_mode, ["xsymbols", "symbols"])))
paulson@16157
   221
      val axioms = get_init_axioms proof_steps
paulson@16157
   222
      val step_nums = get_step_nums axioms []
paulson@16157
   223
  
paulson@16157
   224
     (***********************************************)
paulson@16157
   225
     (* here need to add the clauses from clause_arr*)
paulson@16157
   226
     (***********************************************)
paulson@16157
   227
  
paulson@16157
   228
      val (clasimp_names_cls) = get_clasimp_cls clause_arr num_of_clauses step_nums 
paulson@16157
   229
      val clasimp_names = map (#1 o ResClause.clause_info o #1) clasimp_names_cls
paulson@16157
   230
  
paulson@16157
   231
      val _ = File.write (File.tmp_path (Path.basic "clasimp_names"))                                                               
paulson@16157
   232
                         (concat clasimp_names)
paulson@16157
   233
      val _ = (print_mode := (["xsymbols", "symbols"] @ ! print_mode))
paulson@16157
   234
   in
paulson@16157
   235
      clasimp_names
paulson@16157
   236
   end
quigley@16156
   237
    
quigley@16478
   238
 fun get_axiom_names_vamp proofstr thms (clause_arr:(ResClause.clause * thm) Array.array) num_of_clauses  =
quigley@16357
   239
   let 
quigley@16357
   240
     (* not sure why this is necessary again, but seems to be *)
quigley@16357
   241
      val _ = (print_mode := (Library.gen_rems (op =) (! print_mode, ["xsymbols", "symbols"])))
quigley@16478
   242
      val step_nums =get_linenums proofstr
quigley@16357
   243
  
quigley@16357
   244
     (***********************************************)
quigley@16357
   245
     (* here need to add the clauses from clause_arr*)
quigley@16357
   246
     (***********************************************)
quigley@16357
   247
  
quigley@16357
   248
      val (clasimp_names_cls) = get_clasimp_cls clause_arr num_of_clauses step_nums 
quigley@16357
   249
      val clasimp_names = map (#1 o ResClause.clause_info o #1) clasimp_names_cls
quigley@16357
   250
  
quigley@16357
   251
      val _ = File.write (File.tmp_path (Path.basic "clasimp_names"))                                                               
quigley@16357
   252
                         (concat clasimp_names)
quigley@16357
   253
      val _ = (print_mode := (["xsymbols", "symbols"] @ ! print_mode))
quigley@16357
   254
   in
quigley@16357
   255
      clasimp_names
quigley@16357
   256
   end
quigley@16357
   257
    
quigley@16357
   258
quigley@16357
   259
quigley@16357
   260
quigley@16357
   261
(***********************************************)
quigley@16357
   262
(* get axioms for reconstruction               *)
quigley@16357
   263
(***********************************************)
quigley@16156
   264
fun numclstr (vars, []) str = str
paulson@16157
   265
|   numclstr ( vars, ((num, thm)::rest)) str =
paulson@16157
   266
      let val newstr = str^(string_of_int num)^" "^(string_of_thm thm)^" "
paulson@16157
   267
      in
paulson@16157
   268
        numclstr  (vars,rest) newstr
paulson@16157
   269
      end
quigley@15919
   270
paulson@16157
   271
fun addvars c (a,b)  = (a,b,c)
quigley@15919
   272
quigley@15919
   273
 fun get_axioms_used proof_steps thms clause_arr num_of_clauses  =
paulson@16061
   274
     let 
wenzelm@16259
   275
	 (*val  outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "foo_ax_thmstr")))                                                                      
paulson@16061
   276
	 val _ = TextIO.output (outfile, thmstring)
paulson@16061
   277
	 
paulson@16061
   278
	 val _ =  TextIO.closeOut outfile*)
paulson@16061
   279
	(* not sure why this is necessary again, but seems to be *)
quigley@15782
   280
paulson@16061
   281
	val _=  (print_mode := (Library.gen_rems (op =) (! print_mode, ["xsymbols", "symbols"])))
paulson@16061
   282
	val axioms = get_init_axioms proof_steps
paulson@16061
   283
	val step_nums = get_step_nums axioms []
quigley@15919
   284
paulson@16061
   285
       (***********************************************)
paulson@16061
   286
       (* here need to add the clauses from clause_arr*)
paulson@16061
   287
       (***********************************************)
quigley@15919
   288
paulson@16061
   289
       (* val clasimp_names_cls = get_clasimp_cls clause_arr   num_of_clauses step_nums   
paulson@16061
   290
	val clasimp_names = map #1 clasimp_names_cls
paulson@16061
   291
	val clasimp_cls = map #2 clasimp_names_cls
wenzelm@16259
   292
	val  outfile = TextIO.openAppend(File.platform_path(File.tmp_path (Path.basic "clasimp_names")))                                                            val clasimp_namestr = concat clasimp_names                            
paulson@16061
   293
	 val _ = TextIO.output (outfile,clasimp_namestr)
paulson@16061
   294
	 
paulson@16061
   295
	 val _ =  TextIO.closeOut outfile
quigley@15919
   296
*)
quigley@15919
   297
paulson@16061
   298
	val clauses =(*(clasimp_cls)@*)( make_clauses thms)
paulson@16061
   299
	
paulson@16061
   300
	val vars = map thm_vars clauses
paulson@16061
   301
       
paulson@16061
   302
	val distvars = distinct (fold append vars [])
paulson@16061
   303
	val clause_terms = map prop_of clauses  
paulson@16061
   304
	val clause_frees = List.concat (map term_frees clause_terms)
quigley@15642
   305
paulson@16061
   306
	val frees = map lit_string_with_nums clause_frees;
quigley@15642
   307
paulson@16061
   308
	val distfrees = distinct frees
quigley@15642
   309
paulson@16061
   310
	val metas = map Meson.make_meta_clause clauses
paulson@16061
   311
	val ax_strs = map #3 axioms
quigley@15642
   312
paulson@16061
   313
	(* literals of -all- axioms, not just those used by spass *)
paulson@16061
   314
	val meta_strs = map ReconOrderClauses.get_meta_lits metas
paulson@16061
   315
       
paulson@16061
   316
	val metas_and_strs = ListPair.zip (metas,meta_strs)
wenzelm@16259
   317
	 val  outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "foo_clauses")));                                                                       
paulson@16061
   318
	 val _ = TextIO.output (outfile, onestr ax_strs)
paulson@16061
   319
	 
paulson@16061
   320
	 val _ =  TextIO.closeOut outfile
wenzelm@16259
   321
	 val  outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "foo_metastrs")));                                                                       
paulson@16061
   322
	 val _ = TextIO.output (outfile, onestr meta_strs)
paulson@16061
   323
	 val _ =  TextIO.closeOut outfile
quigley@15642
   324
paulson@16061
   325
	(* get list of axioms as thms with their variables *)
quigley@15642
   326
paulson@16061
   327
	val ax_metas = get_assoc_snds ax_strs metas_and_strs []
paulson@16061
   328
	val ax_vars = map thm_vars ax_metas
paulson@16061
   329
	val ax_with_vars = ListPair.zip (ax_metas,ax_vars)
quigley@15642
   330
paulson@16061
   331
	(* get list of extra axioms as thms with their variables *)
paulson@16061
   332
	val extra_metas = add_if_not_inlist metas ax_metas []
paulson@16061
   333
	val extra_vars = map thm_vars extra_metas
paulson@16061
   334
	val extra_with_vars = if (not (extra_metas = []) ) 
paulson@16061
   335
			      then
paulson@16061
   336
				     ListPair.zip (extra_metas,extra_vars)
paulson@16061
   337
			      else
paulson@16061
   338
				     []
quigley@15642
   339
paulson@16061
   340
       (* val _=  (print_mode := (Library.gen_rems (op =) (! print_mode, ["xsymbols", "symbols"])))
wenzelm@16259
   341
       val  outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "foo_metas")))
quigley@15642
   342
paulson@16061
   343
       val _ = TextIO.output (outfile, ((thmstrings ax_metas "")))
paulson@16061
   344
       val _ =  TextIO.closeOut outfile
wenzelm@16259
   345
      val foo_metas =  File.platform_path(File.tmp_path (Path.basic "foo_metas"))
wenzelm@16259
   346
      val foo_metas2 =   File.platform_path(File.tmp_path (Path.basic "foo_metas2"))
paulson@16061
   347
	val execperl = Unix.execute("/usr/bin/perl", ["remchars.pl", "  <", foo_metas, "  >", foo_metas2])
wenzelm@16259
   348
     val infile = TextIO.openIn(File.platform_path(File.tmp_path (Path.basic "foo_metas2")))
paulson@16061
   349
    val ax_metas_str = TextIO.inputLine (infile)
paulson@16061
   350
    val _ = TextIO.closeIn infile
paulson@16061
   351
       val _= (print_mode := (["xsymbols", "symbols"] @ ! print_mode))*)
paulson@16061
   352
       
paulson@16061
   353
     in
paulson@16061
   354
	(distfrees,distvars, extra_with_vars,ax_with_vars, (*clasimp_names*)(ListPair.zip (step_nums,ax_metas)))
paulson@16061
   355
     end
paulson@16061
   356
    
quigley@15642
   357
quigley@16156
   358
                                        
quigley@15642
   359
quigley@15642
   360
(*********************************************************************)
quigley@15642
   361
(* Pass in spass string of proof and string version of isabelle goal *)
quigley@15642
   362
(* Get out reconstruction steps as a string to be sent to Isabelle   *)
quigley@15642
   363
(*********************************************************************)
quigley@15642
   364
quigley@15642
   365
quigley@16156
   366
fun rules_to_string [] str = str
quigley@16156
   367
|   rules_to_string [x] str = str^x
quigley@16156
   368
|   rules_to_string (x::xs) str = rules_to_string xs (str^x^"   ")
quigley@16156
   369
                                  
quigley@15642
   370
quigley@16156
   371
val dummy_tac = PRIMITIVE(fn thm => thm );
quigley@15642
   372
quigley@15642
   373
quigley@16357
   374
(*val  proofstr = "1242[0:Inp] ||  -> equal(const_List_Orev(tconst_fun(tconst_List_Olist(U),tconst_List_Olist(U)),const_List_Olist_ONil),const_List_Olist_ONil)**.\
quigley@16357
   375
\1279[0:Inp] ||  -> equal(const_Nat_Osize(tconst_fun(tconst_List_Olist(U),tconst_nat),const_List_Olist_ONil),const_0)**.\
quigley@16357
   376
\1430[0:Inp] || equal(const_Nat_Osize(tconst_fun(tconst_List_Olist(typ__Ha),tconst_nat),const_List_Orev(tconst_fun(tconst_List_Olist(typ__Ha),tconst_List_Olist(typ__Ha)),const_List_Olist_ONil)),const_Nat_Osize(tconst_fun(tconst_List_Olist(typ__Ha),tconst_nat),const_List_Olist_ONil))** -> .\
quigley@16357
   377
\1453[0:Rew:1279.0,1430.0,1242.0,1430.0,1279.0,1430.0] || equal(const_0,const_0)* -> .\
quigley@16357
   378
\1454[0:Obv:1453.0] ||  -> .";*)
quigley@16357
   379
quigley@16357
   380
fun remove_linebreaks str = let val strlist = explode str
quigley@16357
   381
	                        val nonewlines = filter (not_equal "\n") strlist
quigley@16357
   382
	                    in
quigley@16357
   383
				implode nonewlines
quigley@16357
   384
			    end
quigley@16357
   385
quigley@16357
   386
quigley@16357
   387
fun subst_for a b [] = ""
quigley@16357
   388
|   subst_for a b (x::xs) = if (x = a)
quigley@16357
   389
				   then 
quigley@16357
   390
					(b^(subst_for a b  xs))
quigley@16357
   391
				   else
quigley@16357
   392
					x^(subst_for a b xs)
quigley@16357
   393
quigley@16156
   394
quigley@16357
   395
fun remove_linebreaks str = let val strlist = explode str
quigley@16357
   396
			    in
quigley@16357
   397
				subst_for "\n" "\t" strlist
quigley@16357
   398
			    end
quigley@16357
   399
quigley@16357
   400
fun restore_linebreaks str = let val strlist = explode str
quigley@16357
   401
			     in
quigley@16357
   402
				subst_for "\t" "\n" strlist
quigley@16357
   403
			     end
quigley@16357
   404
quigley@16357
   405
quigley@16357
   406
quigley@16357
   407
fun spassString_to_lemmaString proofstr thmstring goalstring toParent ppid thms clause_arr  num_of_clauses  = 
quigley@16357
   408
           let 	val  outfile = TextIO.openAppend( File.platform_path(File.tmp_path (Path.basic"thmstringfile")));          
quigley@16357
   409
		val _ = TextIO.output (outfile, ("thmstring is: "^thmstring^"\n proofstr is: "^proofstr^"\n goalstr is: "^goalstring^" \n  num of clauses is: "^(string_of_int num_of_clauses)))
quigley@16357
   410
quigley@16357
   411
              	val _ =  TextIO.closeOut outfile
quigley@16357
   412
quigley@16357
   413
                 (***********************************)
quigley@16357
   414
                 (* parse spass proof into datatype *)
quigley@16357
   415
                 (***********************************)
quigley@16156
   416
         
quigley@16357
   417
                  val tokens = #1(lex proofstr)
quigley@16357
   418
                  val proof_steps1 = parse tokens
quigley@16357
   419
                  val proof_steps = just_change_space proof_steps1
quigley@16357
   420
                  val  outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "foo_parse")));        val _ = TextIO.output (outfile, ("Did parsing on "^proofstr))
quigley@16156
   421
                                                  val _ =  TextIO.closeOut outfile
quigley@16156
   422
                                                
wenzelm@16259
   423
                                                  val  outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "foo_thmstring_at_parse")));                                        val _ = TextIO.output (outfile, ("Parsing for thmstring: "^thmstring))
quigley@16156
   424
                                                  val _ =  TextIO.closeOut outfile
quigley@16156
   425
                                              (************************************)
quigley@16156
   426
                                              (* recreate original subgoal as thm *)
quigley@16156
   427
                                              (************************************)
quigley@16156
   428
                                                
quigley@16156
   429
                                                  (* get axioms as correctly numbered clauses w.r.t. the Spass proof *)
quigley@16156
   430
                                                  (* need to get prems_of thm, then get right one of the prems, relating to whichever*)
quigley@16156
   431
                                                  (* subgoal this is, and turn it into meta_clauses *)
quigley@16156
   432
                                                  (* should prob add array and table here, so that we can get axioms*)
quigley@16156
   433
                                                  (* produced from the clasimpset rather than the problem *)
quigley@16156
   434
quigley@16156
   435
                                                  val (axiom_names) = get_axiom_names proof_steps  thms clause_arr  num_of_clauses
quigley@16156
   436
                                                  val ax_str = "Rules from clasimpset used in proof found by SPASS: "^(rules_to_string axiom_names "")
wenzelm@16259
   437
                                                  val  outfile = TextIO.openAppend(File.platform_path(File.tmp_path (Path.basic "reconstrfile")));                                                     val _ = TextIO.output (outfile, ("reconstring is: "^ax_str^"  "^goalstring))
quigley@16156
   438
                                                  val _ =  TextIO.closeOut outfile
quigley@16156
   439
                                                   
quigley@16156
   440
                                              in 
quigley@16156
   441
                                                   TextIO.output (toParent, ax_str^"\n");
quigley@16156
   442
                                                   TextIO.flushOut toParent;
quigley@16156
   443
                                        	   TextIO.output (toParent, "goalstring: "^goalstring^"\n");
quigley@16156
   444
                                         	   TextIO.flushOut toParent;
quigley@16156
   445
                                         	   TextIO.output (toParent, "thmstring: "^thmstring^"\n");
quigley@16156
   446
                                         	   TextIO.flushOut toParent;
quigley@16156
   447
                                          
quigley@16156
   448
                                         	   Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
quigley@16156
   449
                                         	  (* Attempt to prevent several signals from turning up simultaneously *)
quigley@16156
   450
                                         	   Posix.Process.sleep(Time.fromSeconds 1) ; dummy_tac
quigley@16156
   451
                                              end
wenzelm@16259
   452
                                              handle _ => (let val  outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "foo_handler")));
quigley@16156
   453
quigley@16156
   454
                                                  val _ = TextIO.output (outfile, ("In exception handler"));
quigley@16156
   455
                                                  val _ =  TextIO.closeOut outfile
quigley@16156
   456
                                              in 
quigley@16478
   457
                                                 TextIO.output (toParent,"Proof found but parsing failed for resolution proof: "^(remove_linebreaks proofstr)^"\n" );
quigley@16478
   458
                                                  TextIO.flushOut toParent;
quigley@16478
   459
						   TextIO.output (toParent, (remove_linebreaks thmstring)^"\n");
quigley@16478
   460
                                         	   TextIO.flushOut toParent;
quigley@16478
   461
                                         	   TextIO.output (toParent, ( (remove_linebreaks goalstring)^"\n"));
quigley@16478
   462
                                         	   TextIO.flushOut toParent;
quigley@16478
   463
            					  Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
quigley@16478
   464
                                         	  (* Attempt to prevent several signals from turning up simultaneously *)
quigley@16478
   465
                                         	  Posix.Process.sleep(Time.fromSeconds 1) ;dummy_tac
quigley@16478
   466
                                              end)
quigley@16478
   467
quigley@16478
   468
quigley@16478
   469
fun vampString_to_lemmaString proofstr thmstring goalstring toParent ppid thms clause_arr  num_of_clauses  = 
quigley@16478
   470
           let val  outfile = TextIO.openAppend(File.platform_path(File.tmp_path (Path.basic "thmstringfile")));     						       val _ = TextIO.output (outfile, (" thmstring is: "^thmstring^"proofstr is: "^proofstr^"goalstr is: "^goalstring^" num of clauses is: "^(string_of_int num_of_clauses)))
quigley@16478
   471
                                               val _ =  TextIO.closeOut outfile
quigley@16478
   472
quigley@16478
   473
                                              (***********************************)
quigley@16478
   474
                                              (* get vampire axiom names         *)
quigley@16478
   475
                                              (***********************************)
quigley@16478
   476
         
quigley@16478
   477
                                               val (axiom_names) = get_axiom_names_vamp proofstr  thms clause_arr  num_of_clauses
quigley@16520
   478
                                               val ax_str = "Rules from clasimpset used in proof found by Vampire: "^(rules_to_string axiom_names "")
quigley@16478
   479
                                               val  outfile = TextIO.openAppend(File.platform_path(File.tmp_path (Path.basic "reconstrfile")));                                                    val _ = TextIO.output (outfile, ("reconstring is: "^ax_str^"  "^goalstring))
quigley@16478
   480
                                               val _ =  TextIO.closeOut outfile
quigley@16478
   481
                                                   
quigley@16478
   482
                                              in 
quigley@16478
   483
                                                   TextIO.output (toParent, ax_str^"\n");
quigley@16478
   484
                                                   TextIO.flushOut toParent;
quigley@16478
   485
                                        	   TextIO.output (toParent, "goalstring: "^goalstring^"\n");
quigley@16478
   486
                                         	   TextIO.flushOut toParent;
quigley@16478
   487
                                         	   TextIO.output (toParent, "thmstring: "^thmstring^"\n");
quigley@16478
   488
                                         	   TextIO.flushOut toParent;
quigley@16478
   489
                                          
quigley@16478
   490
                                         	   Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
quigley@16478
   491
                                         	  (* Attempt to prevent several signals from turning up simultaneously *)
quigley@16478
   492
                                         	   Posix.Process.sleep(Time.fromSeconds 1) ; dummy_tac
quigley@16478
   493
                                              end
quigley@16478
   494
                                              handle _ => (let val  outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "foo_handler")));
quigley@16478
   495
quigley@16478
   496
                                                  val _ = TextIO.output (outfile, ("In exception handler"));
quigley@16478
   497
                                                  val _ =  TextIO.closeOut outfile
quigley@16478
   498
                                              in 
quigley@16520
   499
                                                  TextIO.output (toParent,"Proof found by Vampire but translation failed for resolution proof: "^(remove_linebreaks proofstr) );
quigley@16156
   500
                                                  TextIO.flushOut toParent;
quigley@16156
   501
						   TextIO.output (toParent, thmstring^"\n");
quigley@16156
   502
                                         	   TextIO.flushOut toParent;
quigley@16156
   503
                                         	   TextIO.output (toParent, goalstring^"\n");
quigley@16156
   504
                                         	   TextIO.flushOut toParent;
quigley@16156
   505
            					  Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
quigley@16156
   506
                                         	  (* Attempt to prevent several signals from turning up simultaneously *)
quigley@16156
   507
                                         	  Posix.Process.sleep(Time.fromSeconds 1) ;dummy_tac
quigley@16156
   508
                                              end)
quigley@15642
   509
quigley@15642
   510
quigley@16357
   511
quigley@16357
   512
quigley@16357
   513
(* val proofstr = "1582[0:Inp] || -> v_P*.\
quigley@16357
   514
                 \1583[0:Inp] || v_P* -> .\
quigley@16357
   515
		 \1584[0:MRR:1583.0,1582.0] || -> ."; *)
quigley@15642
   516
quigley@15919
   517
fun spassString_to_reconString proofstr thmstring goalstring toParent ppid thms clause_arr  num_of_clauses  = 
wenzelm@16259
   518
      let val  outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "thmstringfile")));                                        
paulson@16061
   519
	  (* val sign = sign_of_thm thm
paulson@16061
   520
	 val prems = prems_of thm
paulson@16061
   521
	 val prems_string =  concat_with_and (map (Sign.string_of_term sign) prems) "" 
paulson@16061
   522
	  val _ = warning ("thmstring is: "^thmstring);(*("thm in spassStrtoRec: "^(concat_with_and (map string_of_thm thms) "")^*)*)
paulson@16061
   523
	  val _ = TextIO.output (outfile, (" thmstring is: "^thmstring^"proofstr is: "^proofstr))
paulson@16061
   524
(*val _ = TextIO.output (outfile, (("in spassStrto Reconstr")));*)
paulson@16061
   525
	  val _ =  TextIO.closeOut outfile
quigley@15782
   526
paulson@16061
   527
	  val tokens = #1(lex proofstr)
quigley@15782
   528
paulson@16061
   529
	    
quigley@15919
   530
paulson@16061
   531
      (***********************************)
paulson@16061
   532
      (* parse spass proof into datatype *)
paulson@16061
   533
      (***********************************)
quigley@15642
   534
paulson@16061
   535
	  val proof_steps1 = parse tokens
paulson@16061
   536
	  val proof_steps = just_change_space proof_steps1
quigley@15642
   537
wenzelm@16259
   538
	  val  outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "foo_parse")));                                                                                          val _ = TextIO.output (outfile, ("Did parsing on "^proofstr))
paulson@16061
   539
	  val _ =  TextIO.closeOut outfile
paulson@16061
   540
	
wenzelm@16259
   541
	  val  outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "foo_thmstring_at_parse")));                                                                             val _ = TextIO.output (outfile, ("Parsing for thmstring: "^thmstring))
paulson@16061
   542
	  val _ =  TextIO.closeOut outfile
paulson@16061
   543
      (************************************)
paulson@16061
   544
      (* recreate original subgoal as thm *)
paulson@16061
   545
      (************************************)
paulson@16061
   546
	
paulson@16061
   547
	  (* get axioms as correctly numbered clauses w.r.t. the Spass proof *)
paulson@16061
   548
	  (* need to get prems_of thm, then get right one of the prems, relating to whichever*)
paulson@16061
   549
	  (* subgoal this is, and turn it into meta_clauses *)
paulson@16061
   550
	  (* should prob add array and table here, so that we can get axioms*)
paulson@16061
   551
	  (* produced from the clasimpset rather than the problem *)
paulson@16061
   552
	  val (frees,vars,extra_with_vars ,ax_with_vars,numcls) = get_axioms_used proof_steps  thms clause_arr  num_of_clauses
paulson@16061
   553
	  
paulson@16061
   554
	  (*val numcls_string = numclstr ( vars, numcls) ""*)
wenzelm@16259
   555
	  val  outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "foo_axiom")));                                                                            val _ = TextIO.output (outfile,"got axioms")
paulson@16061
   556
	  val _ =  TextIO.closeOut outfile
paulson@16061
   557
	    
paulson@16061
   558
      (************************************)
paulson@16061
   559
      (* translate proof                  *)
paulson@16061
   560
      (************************************)
wenzelm@16259
   561
	  val  outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "foo_steps")));                                                          val _ = TextIO.output (outfile, ("about to translate proof, steps: "^(init_proofsteps_to_string proof_steps "")))
paulson@16061
   562
	  val _ =  TextIO.closeOut outfile
paulson@16061
   563
	  val (newthm,proof) = translate_proof numcls  proof_steps vars
wenzelm@16259
   564
	  val  outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "foo_steps2")));                                                                         val _ = TextIO.output (outfile, ("translated proof, steps: "^(init_proofsteps_to_string proof_steps "")))
paulson@16061
   565
	  val _ =  TextIO.closeOut outfile
paulson@16061
   566
      (***************************************************)
paulson@16061
   567
      (* transfer necessary steps as strings to Isabelle *)
paulson@16061
   568
      (***************************************************)
paulson@16061
   569
	  (* turn the proof into a string *)
paulson@16061
   570
	  val reconProofStr = proofs_to_string proof ""
paulson@16061
   571
	  (* do the bit for the Isabelle ordered axioms at the top *)
paulson@16061
   572
	  val ax_nums = map #1 numcls
paulson@16061
   573
	  val ax_strs = map ReconOrderClauses.get_meta_lits_bracket (map #2 numcls)
paulson@16061
   574
	  val numcls_strs = ListPair.zip (ax_nums,ax_strs)
paulson@16061
   575
	  val num_cls_vars =  map (addvars vars) numcls_strs;
paulson@16061
   576
	  val reconIsaAxStr = origAxs_to_string (ListPair.zip (ax_nums,ax_with_vars)) ""
paulson@16061
   577
	  
paulson@16061
   578
	  val extra_nums = if (not (extra_with_vars = [])) then (1 upto (length extra_with_vars)) else []
paulson@16061
   579
	  val reconExtraAxStr = extraAxs_to_string ( ListPair.zip (extra_nums,extra_with_vars)) ""
paulson@16061
   580
	  val frees_str = "["^(thmvars_to_string frees "")^"]"
wenzelm@16259
   581
	  val  outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "reconstringfile")));
quigley@15642
   582
paulson@16061
   583
	  val _ = TextIO.output (outfile, (frees_str^reconExtraAxStr^reconIsaAxStr^reconProofStr))
paulson@16061
   584
	  val _ =  TextIO.closeOut outfile
paulson@16061
   585
	  val reconstr = (frees_str^reconExtraAxStr^reconIsaAxStr^reconProofStr)
paulson@16061
   586
      in 
paulson@16061
   587
	   TextIO.output (toParent, reconstr^"\n");
paulson@16061
   588
	   TextIO.flushOut toParent;
paulson@16061
   589
	   TextIO.output (toParent, thmstring^"\n");
paulson@16061
   590
	   TextIO.flushOut toParent;
paulson@16061
   591
	   TextIO.output (toParent, goalstring^"\n");
paulson@16061
   592
	   TextIO.flushOut toParent;
paulson@16061
   593
  
paulson@16061
   594
	   Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
paulson@16061
   595
	  (* Attempt to prevent several signals from turning up simultaneously *)
paulson@16061
   596
	   Posix.Process.sleep(Time.fromSeconds 1) ; dummy_tac
paulson@16061
   597
      end
wenzelm@16259
   598
      handle _ => (let val  outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "foo_handler")));
quigley@15642
   599
paulson@16061
   600
	  val _ = TextIO.output (outfile, ("In exception handler"));
paulson@16061
   601
	  val _ =  TextIO.closeOut outfile
paulson@16061
   602
      in 
quigley@16478
   603
	   TextIO.output (toParent,"Proof found but translation failed for resolution proof:"^(remove_linebreaks proofstr) ^"\n");
paulson@16061
   604
	  TextIO.flushOut toParent;
paulson@16061
   605
	TextIO.output (toParent, thmstring^"\n");
paulson@16061
   606
	   TextIO.flushOut toParent;
paulson@16061
   607
	   TextIO.output (toParent, goalstring^"\n");
paulson@16061
   608
	   TextIO.flushOut toParent;
paulson@16061
   609
	  Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
paulson@16061
   610
	  (* Attempt to prevent several signals from turning up simultaneously *)
paulson@16061
   611
	  Posix.Process.sleep(Time.fromSeconds 1) ;dummy_tac
paulson@16061
   612
      end)
quigley@15642
   613
quigley@15642
   614
quigley@15642
   615
quigley@15642
   616
quigley@15642
   617
quigley@15642
   618
(**********************************************************************************)
quigley@15642
   619
(* At other end, want to turn back into datatype so can apply reconstruct_proof.  *)
quigley@15642
   620
(* This will be done by the signal handler                                        *)
quigley@15642
   621
(**********************************************************************************)
quigley@15642
   622
quigley@15642
   623
(* Parse in the string version of the proof steps for reconstruction *)
quigley@15642
   624
(* Isar format: cl1 [BINARY 0 cl2 0];cl1 [PARAMOD 0 cl2 0]; cl1 [DEMOD 0 cl2];cl1 [FACTOR 1 2];*)
quigley@15642
   625
quigley@15642
   626
quigley@15642
   627
 val term_numstep =
quigley@15642
   628
        (number ++ (a (Other ",")) ++ number) >> (fn (a, (_, c)) => (a, c))
quigley@15642
   629
quigley@15642
   630
val extraaxiomstep = (a (Word "ExtraAxiom"))++ (a (Other "(")) ++(a (Other ")"))
quigley@15642
   631
            >> (fn (_) => ExtraAxiom)
quigley@15642
   632
quigley@15642
   633
quigley@15642
   634
quigley@15642
   635
val origaxiomstep = (a (Word "OrigAxiom"))++ (a (Other "(")) ++(a (Other ")"))
quigley@15642
   636
            >> (fn (_) => OrigAxiom)
quigley@15642
   637
quigley@15642
   638
quigley@15642
   639
 val axiomstep = (a (Word "Axiom"))++ (a (Other "(")) ++(a (Other ")"))
quigley@15642
   640
            >> (fn (_) => Axiom)
quigley@15642
   641
     
quigley@15642
   642
quigley@15642
   643
quigley@15642
   644
      
quigley@15642
   645
 val binarystep = (a (Word "Binary")) ++ (a (Other "(")) ++ (a (Other "(")) 
quigley@15642
   646
                   ++ term_numstep  ++ (a (Other ")")) ++ (a (Other ","))
quigley@15642
   647
                   ++ (a (Other "(")) ++ term_numstep ++ (a (Other ")")) ++ (a (Other ")"))
quigley@15642
   648
            >> (fn (_, (_, (_, (c, (_,(_,(_, (e,(_,_))))))))) => Binary (c,e))
quigley@15642
   649
      
quigley@15642
   650
quigley@15642
   651
 val parastep = (a (Word "Para")) ++ (a (Other "(")) ++ (a (Other "(")) 
quigley@15642
   652
                   ++ term_numstep  ++ (a (Other ")")) ++ (a (Other ","))
quigley@15642
   653
                   ++ (a (Other "(")) ++ term_numstep ++ (a (Other ")")) ++ (a (Other ")"))
quigley@15642
   654
            >> (fn (_, (_, (_, (c, (_,(_,(_, (e,(_,_))))))))) => Para(c, e))
quigley@15642
   655
      
quigley@15642
   656
 val mrrstep = (a (Word "MRR")) ++ (a (Other "(")) ++ (a (Other "(")) 
quigley@15642
   657
                   ++ term_numstep  ++ (a (Other ")")) ++ (a (Other ","))
quigley@15642
   658
                   ++ (a (Other "(")) ++ term_numstep ++ (a (Other ")")) ++ (a (Other ")"))
quigley@15642
   659
            >> (fn (_, (_, (_, (c, (_,(_,(_, (e,(_,_))))))))) => MRR(c, e))
quigley@15642
   660
      
quigley@15642
   661
quigley@15642
   662
 val factorstep = (a (Word "Factor")) ++ (a (Other "("))
quigley@15642
   663
                    ++ number ++ (a (Other ","))
quigley@15642
   664
                       ++ number ++ (a (Other ","))
quigley@15642
   665
                       ++ number ++  (a (Other ")"))
quigley@15642
   666
                   
quigley@15642
   667
            >> (fn (_, (_, (c, (_, (e,(_,(f,_))))))) =>  Factor (c,e,f))
quigley@15642
   668
quigley@15642
   669
quigley@16548
   670
(*val rewritestep = (a (Word "Rewrite"))  ++ (a (Other "(")) ++ (a (Other "(")) 
quigley@15642
   671
                   ++ term_numstep  ++ (a (Other ")")) ++ (a (Other ","))
quigley@15642
   672
                   ++ (a (Other "(")) ++ term_numstep ++ (a (Other ")")) ++ (a (Other ")"))
quigley@16548
   673
            >> (fn (_, (_, (_, (c, (_,(_,(_, (e,(_,_))))))))) => Rewrite (c,e))*)
quigley@15642
   674
quigley@15642
   675
val obviousstep = (a (Word "Obvious")) ++ (a (Other "(")) 
quigley@15642
   676
                   ++ term_numstep  ++ (a (Other ")")) 
quigley@15642
   677
            >> (fn (_, (_, (c,_))) => Obvious (c))
quigley@15642
   678
quigley@16548
   679
 val methodstep = extraaxiomstep || origaxiomstep || axiomstep ||binarystep || factorstep|| parastep || mrrstep || (*rewritestep ||*) obviousstep
quigley@15642
   680
quigley@15642
   681
quigley@15642
   682
 val number_list_step =
paulson@15739
   683
        ( number ++ many ((a (Other ",") ++ number)>> #2))
quigley@15642
   684
        >> (fn (a,b) => (a::b))
quigley@15642
   685
        
quigley@15642
   686
 val numberlist_step = a (Other "[")  ++ a (Other "]")
quigley@15642
   687
                        >>(fn (_,_) => ([]:int list))
quigley@15642
   688
                       || a (Other "[") ++ number_list_step ++ a (Other "]")
quigley@15642
   689
                        >>(fn (_,(a,_)) => a)
quigley@15642
   690
                    
quigley@15642
   691
quigley@15642
   692
quigley@15642
   693
(** change this to allow P (x U) *)
quigley@15642
   694
 fun arglist_step input = ( word ++ many  word >> (fn (a, b) => (a^" "^(implode_with_space b)))
quigley@15642
   695
                           ||word >> (fn (a) => (a)))input
quigley@15642
   696
                
quigley@15642
   697
quigley@15642
   698
fun literal_step input = (word ++ a (Other "(") ++ arglist_step ++  a (Other ")")
quigley@15642
   699
                                          >>(fn (a, (b, (c,d))) => (a^" ("^(c)^")"))
quigley@15642
   700
                        || arglist_step >> (fn (a) => (a)))input
quigley@15642
   701
                           
quigley@15642
   702
quigley@15642
   703
quigley@15642
   704
(* fun term_step input = (a (Other "~") ++ arglist_step ++ a (Other "%")>> (fn (a,(b,c)) => ("~ "^b))
quigley@15642
   705
                     ||  arglist_step ++ a (Other "%")>> (fn (a,b) => a ))input
quigley@15642
   706
*)
quigley@15642
   707
quigley@15642
   708
quigley@15642
   709
 fun term_step input = (a (Other "~") ++ literal_step ++ a (Other "%")>> (fn (a,(b,c)) => ("~ "^b))
quigley@15642
   710
                     ||  literal_step ++ a (Other "%")>> (fn (a,b) => a ))input
quigley@15642
   711
quigley@15642
   712
quigley@15642
   713
         
quigley@15642
   714
quigley@15642
   715
 val term_list_step =
quigley@15642
   716
        (  term_step ++ many ( term_step))
quigley@15642
   717
        >> (fn (a,b) => (a::b))
quigley@15642
   718
        
quigley@15642
   719
 
quigley@15642
   720
val term_lists_step = a (Other "[")  ++ a (Other "]")
quigley@15642
   721
                        >>(fn (_,_) => ([]:string list))
quigley@15642
   722
                       || a (Other "[") ++ term_list_step ++ a (Other "]")
quigley@15642
   723
                        >>(fn (_,(a,_)) => a)
quigley@15642
   724
                     
quigley@15642
   725
quigley@15642
   726
quigley@15642
   727
quigley@15642
   728
fun anytoken_step input  = (word>> (fn (a) => a)  ) input
quigley@15642
   729
                       handle NOPARSE_WORD => (number>> (fn (a) => string_of_int a)  ) input
quigley@15642
   730
                      handle NOPARSE_NUMBER => (other_char >> (fn(a) => a)) input
quigley@15642
   731
quigley@15642
   732
quigley@15642
   733
quigley@15642
   734
fun goalstring_step input= (anytoken_step ++ many (anytoken_step )
quigley@15642
   735
                  >> (fn (a,b) =>  (a^" "^(implode b)))) input
quigley@15642
   736
quigley@15642
   737
quigley@15642
   738
quigley@15642
   739
 val linestep = number ++ methodstep ++ term_lists_step ++ term_lists_step
quigley@15642
   740
                >> (fn (a, (b, (c,d))) => (a,(b,c,d)))
quigley@15642
   741
    
quigley@15642
   742
 val lines_step = many linestep
quigley@15642
   743
paulson@15739
   744
 val alllines_step = (term_lists_step ++ lines_step ) ++ finished >> #1
quigley@15642
   745
    
paulson@15739
   746
 val parse_step = #1 o alllines_step
quigley@15642
   747
quigley@15642
   748
quigley@15642
   749
 (*
quigley@15642
   750
val reconstr ="[P%x%xa%xb%]1OrigAxiom()[P x%~ P U%][U%]3OrigAxiom()[P U%~ P x%][U%]5OrigAxiom()[~ P xa%~ P U%][U%]7OrigAxiom()[P U%P xb%][U%]1Axiom()[P x%~ P U%][U%]3Axiom()[P U%~ P x%][U%]5Axiom()[~ P U%~ P xa%][U%]7Axiom()[P U%P xb%][U%]9Factor(5,0,1)[~ P xa%][]10Binary((9,0),(3,0))[~ P x%][]11Binary((10,0),(1,0))[~ P U%][U%]12Factor(7,0,1)[P xb%][]14Binary((11,0),(12,0))[][]%(EX x::'a::type. ALL y::'a::type. (P::'a::type => bool) x = P y) -->(EX x::'a::type. P x) = (ALL y::'a::type. P y)"
quigley@15642
   751
*)
quigley@15642
   752
quigley@15642
   753
(************************************************************)
quigley@15642
   754
(* Construct an Isar style proof from a list of proof steps *)
quigley@15642
   755
(************************************************************)
quigley@15642
   756
(* want to assume all axioms, then do haves for the other clauses*)
quigley@15642
   757
(* then show for the last step *)
quigley@15642
   758
quigley@15642
   759
(* replace ~ by not here *)
quigley@15642
   760
fun change_nots [] = []
quigley@15642
   761
|   change_nots (x::xs) = if x = "~" 
quigley@15642
   762
                          then 
quigley@15642
   763
                             ["\\", "<", "n", "o", "t", ">"]@(change_nots xs)
quigley@15642
   764
                          else (x::(change_nots xs))
quigley@15642
   765
quigley@15642
   766
(*
quigley@15642
   767
fun clstrs_to_string [] str = str
quigley@15642
   768
|   clstrs_to_string (x::[]) str = str^x
quigley@15642
   769
|   clstrs_to_string (x::xs) str = clstrs_to_string xs (str^(x^"; "))
quigley@15642
   770
*)
quigley@15642
   771
fun clstrs_to_string [] str = implode (change_nots (explode str))
quigley@15642
   772
|   clstrs_to_string (x::[]) str = implode (change_nots (explode (str^x)))
quigley@15642
   773
|   clstrs_to_string (x::xs) str = implode (change_nots (explode (clstrs_to_string xs (str^(x^"; ")))))
quigley@15642
   774
quigley@15642
   775
quigley@15642
   776
quigley@15642
   777
fun thmvars_to_quantstring [] str = str
quigley@15642
   778
|   thmvars_to_quantstring (x::[]) str =str^x^". "
quigley@15642
   779
|   thmvars_to_quantstring (x::xs) str = thmvars_to_quantstring xs (str^(x^" "))
quigley@15642
   780
quigley@15642
   781
paulson@16091
   782
fun clause_strs_to_isar clstrs [] =  "\"\\<lbrakk>"^(clstrs_to_string clstrs "")^"\\<rbrakk> \\<Longrightarrow> False\""
paulson@16091
   783
|   clause_strs_to_isar clstrs thmvars = "\"\\<And>"^(thmvars_to_quantstring thmvars "")^"\\<lbrakk>"^(clstrs_to_string clstrs "")^"\\<rbrakk> \\<Longrightarrow> False\""
quigley@15642
   784
quigley@15642
   785
fun frees_to_string [] str = implode (change_nots (explode str))
quigley@15642
   786
|   frees_to_string (x::[]) str = implode (change_nots (explode (str^x)))
quigley@15642
   787
|   frees_to_string  (x::xs) str = implode (change_nots (explode (frees_to_string xs (str^(x^" ")))))
quigley@15642
   788
quigley@15642
   789
fun frees_to_isar_str [] =  ""
quigley@15642
   790
|   frees_to_isar_str  clstrs = (frees_to_string clstrs "")
quigley@15642
   791
quigley@15642
   792
quigley@15642
   793
(***********************************************************************)
quigley@15642
   794
(* functions for producing assumptions for the Isabelle ordered axioms *)
quigley@15642
   795
(***********************************************************************)
quigley@15642
   796
(*val str = "[P%x%xa%xb%]1OrigAxiom()[P x%~ P U%][U%]3OrigAxiom()[P U%~ P x%][U%]5OrigAxiom()[~ P xa%~ P U%][U%]7OrigAxiom()[P U%P xb%][U%]1Axiom()[P x%~ P U%][U%]3Axiom()[P U%~ P x%][U%]5Axiom()[~ P U%~ P xa%][U%]7Axiom()[P U%P xb%][U%]9Factor(5,0,1)[~ P xa%][]10Binary((9,0),(3,0))[~ P x%][]11Binary((10,0),(1,0))[~ P U%][U%]12Factor(7,0,1)[P xb%][]14Binary((11,0),(12,0))[][]";       
quigley@15642
   797
num, rule, clausestrs, vars*)
quigley@15642
   798
quigley@15642
   799
quigley@15642
   800
(* assume the extra clauses - not used in Spass proof *)
quigley@15642
   801
quigley@15642
   802
fun is_extraaxiom_step ( num:int,(ExtraAxiom, str, tstr)) = true
quigley@15642
   803
|   is_extraaxiom_step (num, _) = false
quigley@15642
   804
quigley@15642
   805
fun get_extraaxioms xs = List.filter (is_extraaxiom_step) ( xs)
quigley@15642
   806
quigley@15642
   807
fun assume_isar_extraaxiom [] str  = str
quigley@15642
   808
|   assume_isar_extraaxiom ((numb,(step, clstr, thmvars))::xs) str  = assume_isar_extraaxiom xs (str^"and cl"^(string_of_int numb)^"': "^(clause_strs_to_isar clstr thmvars)^"\n " )
quigley@15642
   809
quigley@15642
   810
quigley@15642
   811
quigley@15642
   812
fun assume_isar_extraaxioms  [] = ""
quigley@15642
   813
|assume_isar_extraaxioms ((numb,(step, clstrs, thmstrs))::xs) = let val str = "assume cl"^(string_of_int numb)^"': "^(clause_strs_to_isar clstrs thmstrs)^"\n" 
quigley@15642
   814
                                         in
quigley@15642
   815
                                             assume_isar_extraaxiom xs str
quigley@15642
   816
                                         end
quigley@15642
   817
quigley@15642
   818
(* assume the Isabelle ordered clauses *)
quigley@15642
   819
quigley@15642
   820
fun is_origaxiom_step ( num:int,(OrigAxiom, str, tstr)) = true
quigley@15642
   821
|   is_origaxiom_step (num, _) = false
quigley@15642
   822
quigley@15642
   823
fun get_origaxioms xs = List.filter (is_origaxiom_step) ( xs)
quigley@15642
   824
quigley@15642
   825
fun assume_isar_origaxiom [] str  = str
quigley@15642
   826
|   assume_isar_origaxiom ((numb,(step, clstr, thmvars))::xs) str  = assume_isar_origaxiom xs (str^"and cl"^(string_of_int numb)^"': "^(clause_strs_to_isar clstr thmvars)^"\n " )
quigley@15642
   827
quigley@15642
   828
quigley@15642
   829
quigley@15642
   830
fun assume_isar_origaxioms ((numb,(step, clstrs, thmstrs))::xs) = let val str = "assume cl"^(string_of_int numb)^"': "^(clause_strs_to_isar clstrs thmstrs)^"\n" 
quigley@15642
   831
                                         in
quigley@15642
   832
                                             assume_isar_origaxiom xs str
quigley@15642
   833
                                         end
quigley@15642
   834
quigley@15642
   835
quigley@15642
   836
quigley@15642
   837
fun is_axiom_step ( num:int,(Axiom, str, tstr)) = true
quigley@15642
   838
|   is_axiom_step (num, _) = false
quigley@15642
   839
quigley@15642
   840
fun get_axioms xs = List.filter  (is_axiom_step) ( xs)
quigley@15642
   841
quigley@15642
   842
fun have_isar_axiomline (numb,(step, clstrs, thmstrs))="have cl"^(string_of_int numb)^": "^(clause_strs_to_isar clstrs thmstrs)^"\n"
quigley@15642
   843
quigley@15642
   844
fun  by_isar_axiomline (numb,(step, clstrs, thmstrs))="by (rule cl"^ (string_of_int numb)^"') \n"
quigley@15642
   845
quigley@15642
   846
quigley@15642
   847
fun isar_axiomline (numb, (step, clstrs, thmstrs))  = (have_isar_axiomline (numb,(step,clstrs, thmstrs )))^( by_isar_axiomline(numb,(step,clstrs, thmstrs )) )
quigley@15642
   848
quigley@15642
   849
quigley@15642
   850
fun isar_axiomlines [] str = str
quigley@15642
   851
|   isar_axiomlines (x::xs) str = isar_axiomlines xs (str^(isar_axiomline x))
quigley@15642
   852
quigley@15642
   853
quigley@15642
   854
fun have_isar_line (numb,(step, clstrs, thmstrs))="have cl"^(string_of_int numb)^": "^(clause_strs_to_isar clstrs thmstrs)^"\n"
quigley@16357
   855
(*FIX: ask Larry to add and mrr attribute *)
quigley@15642
   856
paulson@16091
   857
fun by_isar_line ((Binary ((a,b), (c,d)))) = 
paulson@16091
   858
    "by(rule cl"^
paulson@16091
   859
		(string_of_int a)^" [binary "^(string_of_int b)^" cl"^
paulson@16091
   860
		(string_of_int c)^" "^(string_of_int d)^"])\n"
quigley@16357
   861
|by_isar_line ((MRR ((a,b), (c,d)))) = 
quigley@16357
   862
    "by(rule cl"^
quigley@16357
   863
		(string_of_int a)^" [binary "^(string_of_int b)^" cl"^
quigley@16357
   864
		(string_of_int c)^" "^(string_of_int d)^"])\n"
paulson@16091
   865
|   by_isar_line ( (Para ((a,b), (c,d)))) =
paulson@16091
   866
    "by (rule cl"^
paulson@16091
   867
		(string_of_int a)^" [paramod "^(string_of_int b)^" cl"^
paulson@16091
   868
		(string_of_int c)^" "^(string_of_int d)^"])\n"
paulson@16091
   869
|   by_isar_line ((Factor ((a,b,c)))) = 
paulson@16091
   870
    "by (rule cl"^(string_of_int a)^" [factor "^(string_of_int b)^" "^
paulson@16091
   871
		(string_of_int c)^" ])\n"
quigley@16548
   872
(*|   by_isar_line ( (Rewrite ((a,b),(c,d)))) =
paulson@16091
   873
    "by (rule cl"^(string_of_int a)^" [demod "^(string_of_int b)^" "^
quigley@16548
   874
		(string_of_int c)^" "^(string_of_int d)^" ])\n"*)
paulson@16091
   875
|   by_isar_line ( (Obvious ((a,b)))) =
paulson@16091
   876
    "by (rule cl"^(string_of_int a)^" [obvious "^(string_of_int b)^" ])\n"
quigley@15642
   877
quigley@15642
   878
fun isar_line (numb, (step, clstrs, thmstrs))  = (have_isar_line (numb,(step,clstrs, thmstrs )))^( by_isar_line step)
quigley@15642
   879
quigley@15642
   880
quigley@15642
   881
fun isar_lines [] str = str
quigley@15642
   882
|   isar_lines (x::xs) str = isar_lines xs (str^(isar_line x))
quigley@15642
   883
quigley@15642
   884
fun last_isar_line (numb,( step, clstrs,thmstrs)) = "show \"False\"\n"^(by_isar_line step)
quigley@15642
   885
quigley@15642
   886
paulson@16091
   887
fun to_isar_proof (frees, xs, goalstring) =
paulson@16091
   888
    let val extraaxioms = get_extraaxioms xs
paulson@16091
   889
	val extraax_num = length extraaxioms
paulson@16091
   890
	val origaxioms_and_steps = Library.drop (extraax_num, xs)  
paulson@16091
   891
	
paulson@16091
   892
	val origaxioms = get_origaxioms origaxioms_and_steps
paulson@16091
   893
	val origax_num = length origaxioms
paulson@16091
   894
	val axioms_and_steps = Library.drop (origax_num + extraax_num, xs)  
paulson@16091
   895
	val axioms = get_axioms axioms_and_steps
paulson@16091
   896
	
paulson@16091
   897
	val steps = Library.drop (origax_num, axioms_and_steps)
paulson@16091
   898
	val firststeps = ReconOrderClauses.butlast steps
paulson@16091
   899
	val laststep = ReconOrderClauses.last steps
paulson@16091
   900
	val goalstring = implode(ReconOrderClauses.butlast(explode goalstring))
paulson@16091
   901
	
paulson@16091
   902
	val isar_proof = 
paulson@16091
   903
		("show \""^goalstring^"\"\n")^
paulson@16091
   904
		("proof (rule ccontr,skolemize, make_clauses) \n")^
paulson@16091
   905
		("fix "^(frees_to_isar_str frees)^"\n")^
paulson@16091
   906
		(assume_isar_extraaxioms extraaxioms)^
paulson@16091
   907
		(assume_isar_origaxioms origaxioms)^
paulson@16091
   908
		(isar_axiomlines axioms "")^
paulson@16091
   909
		(isar_lines firststeps "")^
paulson@16091
   910
		(last_isar_line laststep)^
paulson@16091
   911
		("qed")
wenzelm@16259
   912
	val  outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "isar_proof_file")));
paulson@16091
   913
	
paulson@16091
   914
	val _ = TextIO.output (outfile, isar_proof)
paulson@16091
   915
	val _ =  TextIO.closeOut outfile
paulson@16091
   916
    in
paulson@16091
   917
	isar_proof
paulson@16091
   918
    end;
quigley@15642
   919
quigley@15642
   920
(* get fix vars from axioms - all Frees *)
quigley@15642
   921
(* check each clause for meta-vars and /\ over them at each step*)
quigley@15642
   922
quigley@15642
   923
(*******************************************************)
quigley@15642
   924
(* This assumes the thm list  "numcls" is still there  *)
quigley@15642
   925
(* In reality, should probably label it with an        *)
quigley@15642
   926
(* ID number identifying the subgoal.  This could      *)
quigley@15642
   927
(* be passed over to the watcher, e.g.  numcls25       *)
quigley@15642
   928
(*******************************************************)
quigley@15642
   929
quigley@15642
   930
(* val str = "[S%x%P%R%Q%]1ExtraAxiom()[~ Q U%~ R U%][U%]2ExtraAxiom()[~ Q U%~ P U%][U%]3ExtraAxiom()[Q U%R U%][U%]1OrigAxiom()[S x%][]2OrigAxiom()[P U%R U%][U%]6OrigAxiom()[~ S U%~ P U%][U%]7OrigAxiom()[~ S U%~ R U%][U%]1Axiom()[S x%][]2Axiom()[R U%P U%][U%]6Axiom()[~ P U%~ S U%][U%]7Axiom()[~ R U%~ S U%][U%]8Binary((6,1),(1,0))[~ P x%][]9Binary((7,1),(1,0))[~ R x%][]19Binary((9,0),(2,0))[P x%][]25Binary((8,0),(19,0))[][]";
quigley@15642
   931
quigley@15642
   932
val str = "[P%x%xa%xb%]1OrigAxiom()[P x%~ P U%][U%]3OrigAxiom()[P U%~ P x%][U%]5OrigAxiom()[~ P xa%~ P U%][U%]7OrigAxiom()[P U%P xb%][U%]1Axiom()[P x%~ P U%][U%]3Axiom()[P U%~ P x%][U%]5Axiom()[~ P U%~ P xa%][U%]7Axiom()[P U%P xb%][U%]9Factor(5,0,1)[~ P xa%][]10Binary((9,0),(3,0))[~ P x%][]11Binary((10,0),(1,0))[~ P U%][U%]12Factor(7,0,1)[P xb%][]14Binary((11,0),(12,0))[][]";
quigley@15642
   933
quigley@15642
   934
val reconstr = "[P%Q%x%xa%]1OrigAxiom()[~ P U%][U%]3OrigAxiom()[Q U%][U%]5OrigAxiom()[P (x U)%~ Q (xa U)%][U%]9Binary((7,0),(3,0))[][]7Binary((1,0),(5,0))[~ Q (xa U)%][U%]5Axiom()[P (x U)%~ Q (xa U)%][U%]3Axiom()[Q U%][U%]1Axiom()[~ P U%][U%](ALL xb::'a::type.   (~ (P::'a::type => bool) ((x::'a::type => 'a::type) xb) |    (Q::'a::type => bool) ((xa::'a::type => 'a::type) xb)) &   P xb & ~ Q xb)";
quigley@15642
   935
quigley@15642
   936
quigley@15642
   937
val reconstr = "[P%x%xa%xb%]1OrigAxiom()[P x%~ P U%][U%]3OrigAxiom()[P U%~ P x%][U%]5OrigAxiom()[~ P xa%~ P U%][U%]7OrigAxiom()[P U%P xb%][U%]1Axiom()[P x%~ P U%][U%]3Axiom()[P U%~ P x%][U%]5Axiom()[~ P U%~ P xa%][U%]7Axiom()[P U%P xb%][U%]9Factor(5,0,1)[~ P xa%][]10Binary((9,0),(3,0))[~ P x%][]11Binary((10,0),(1,0))[~ P U%][U%]12Factor(7,0,1)[P xb%][]14Binary((11,0),(12,0))[][]";
quigley@15642
   938
quigley@15642
   939
val thmstring = " (ALL xa::'a::type.   (~ (P::'a::type => bool) (x::'a::type) | P xa) & (~ P xa | P x)) & (((P::'a::type => bool) (xa::'a::type) | (ALL x::'a::type. P x)) &((ALL x::'a::type. ~ P x) | ~ P (xb::'a::type)))";
quigley@15642
   940
*)
quigley@15642
   941
paulson@15739
   942
fun apply_res_thm str goalstring  = let val tokens = #1 (lex str);
quigley@16357
   943
				val _ = File.append (File.tmp_path (Path.basic "applyres")) 
quigley@16357
   944
			           ("str is: "^str^" goalstr is: "^goalstring^"\n")	
quigley@15642
   945
                                   val (frees,recon_steps) = parse_step tokens 
quigley@15642
   946
                                   val isar_str = to_isar_proof (frees, recon_steps, goalstring)
wenzelm@16259
   947
                                   val foo =   TextIO.openOut (File.platform_path(File.tmp_path (Path.basic "foobar")));
quigley@15642
   948
                               in 
quigley@15642
   949
                                  TextIO.output(foo,(isar_str));TextIO.closeOut foo;Pretty.writeln(Pretty.str  isar_str); () 
quigley@15642
   950
                               end 
quigley@15642
   951
quigley@15642
   952
quigley@16357
   953
(* val reconstr = reconstr^"[P%]51Axiom()[~P%]52Axiom[P%][]53MRR((52,0),(51,0))[][]";
quigley@16357
   954
*)
paulson@15684
   955
end;