src/HOL/Import/replay.ML
author Cezary Kaliszyk <kaliszyk@in.tum.de>
Wed Jul 20 10:11:08 2011 +0200 (2011-07-20)
changeset 43918 6ca79a354c51
parent 41522 42d13d00ccfb
child 46201 afdc69f5156e
permissions -rw-r--r--
HOL/Import reorganization/cleaning. Factor 9 speedup. Remove Import XML parser in favor of much faster of Isabelle's XML parser. Remove ImportRecording since we can use Isabelle images.
     1 (*  Title:      HOL/Import/replay.ML
     2     Author:     Sebastian Skalberg (TU Muenchen)
     3 *)
     4 
     5 structure Replay =  (* FIXME proper signature *)
     6 struct
     7 
     8 open ProofKernel
     9 
    10 exception REPLAY of string * string
    11 fun ERR f mesg = REPLAY (f,mesg)
    12 fun NY f = raise ERR f "NOT YET!"
    13 
    14 fun replay_proof int_thms thyname thmname prf thy =
    15     let
    16         fun rp (PRefl tm) thy = ProofKernel.REFL tm thy
    17           | rp (PInstT(p,lambda)) thy =
    18             let
    19                 val (thy',th) = rp' p thy
    20             in
    21                 ProofKernel.INST_TYPE lambda th thy'
    22             end
    23           | rp (PSubst(prfs,ctxt,prf)) thy =
    24             let
    25                 val (thy',ths) = fold_rev (fn p => fn (thy, ths) =>
    26                                            let
    27                                                val (thy',th) = rp' p thy
    28                                            in
    29                                                (thy',th::ths)
    30                                            end) prfs (thy,[])
    31                 val (thy'',th) = rp' prf thy'
    32             in
    33                 ProofKernel.SUBST ths ctxt th thy''
    34             end
    35           | rp (PAbs(prf,v)) thy =
    36             let
    37                 val (thy',th) = rp' prf thy
    38             in
    39                 ProofKernel.ABS v th thy'
    40             end
    41           | rp (PDisch(prf,tm)) thy =
    42             let
    43                 val (thy',th) = rp' prf thy
    44             in
    45                 ProofKernel.DISCH tm th thy'
    46             end
    47           | rp (PMp(prf1,prf2)) thy =
    48             let
    49                 val (thy1,th1) = rp' prf1 thy
    50                 val (thy2,th2) = rp' prf2 thy1
    51             in
    52                 ProofKernel.MP th1 th2 thy2
    53             end
    54           | rp (PHyp tm) thy = ProofKernel.ASSUME tm thy
    55           | rp (PDef(seg,name,rhs)) thy =
    56             (case ProofKernel.get_def seg name rhs thy of
    57                  (thy',SOME res) => (thy',res)
    58                | (thy',NONE) => 
    59                  if seg = thyname
    60                  then ProofKernel.new_definition seg name rhs thy'
    61                  else raise ERR "replay_proof" ("Too late for term definition: "^seg^" != "^thyname))
    62           | rp (POracle(tg,asl,c)) thy = (*ProofKernel.mk_oracle_thm tg (map be_contract asl,c)*) NY "ORACLE"
    63           | rp (PSpec(prf,tm)) thy =
    64             let
    65                 val (thy',th) = rp' prf thy
    66             in
    67                 ProofKernel.SPEC tm th thy'
    68             end
    69           | rp (PInst(prf,theta)) thy =
    70             let
    71                 val (thy',th) = rp' prf thy
    72             in
    73                 ProofKernel.INST theta th thy'
    74             end
    75           | rp (PGen(prf,v)) thy =
    76             let
    77                 val (thy',th) = rp' prf thy
    78                 val p = ProofKernel.GEN v th thy'
    79             in
    80                 p
    81             end
    82           | rp (PGenAbs(prf,opt,vl)) thy =
    83             let
    84                 val (thy',th) = rp' prf thy
    85             in
    86                 ProofKernel.GEN_ABS opt vl th thy'
    87             end
    88           | rp (PImpAS(prf1,prf2)) thy =
    89             let
    90                 val (thy1,th1) = rp' prf1 thy
    91                 val (thy2,th2) = rp' prf2 thy1
    92             in
    93                 ProofKernel.IMP_ANTISYM th1 th2 thy2
    94             end
    95           | rp (PSym prf) thy =
    96             let
    97                 val (thy1,th) = rp' prf thy
    98             in
    99                 ProofKernel.SYM th thy1
   100             end
   101           | rp (PTrans(prf1,prf2)) thy =
   102             let
   103                 val (thy1,th1) = rp' prf1 thy
   104                 val (thy2,th2) = rp' prf2 thy1
   105             in
   106                 ProofKernel.TRANS th1 th2 thy2
   107             end
   108           | rp (PComb(prf1,prf2)) thy =
   109             let
   110                 val (thy1,th1) = rp' prf1 thy
   111                 val (thy2,th2) = rp' prf2 thy1
   112             in
   113                 ProofKernel.COMB th1 th2 thy2
   114             end
   115           | rp (PEqMp(prf1,prf2)) thy =
   116             let
   117                 val (thy1,th1) = rp' prf1 thy
   118                 val (thy2,th2) = rp' prf2 thy1
   119             in
   120                 ProofKernel.EQ_MP th1 th2 thy2
   121             end
   122           | rp (PEqImp prf) thy =
   123             let
   124                 val (thy',th) = rp' prf thy
   125             in
   126                 ProofKernel.EQ_IMP_RULE th thy'
   127             end
   128           | rp (PExists(prf,ex,wit)) thy =
   129             let
   130                 val (thy',th) = rp' prf thy
   131             in
   132                 ProofKernel.EXISTS ex wit th thy'
   133             end
   134           | rp (PChoose(v,prf1,prf2)) thy =
   135             let
   136                 val (thy1,th1) = rp' prf1 thy
   137                 val (thy2,th2) = rp' prf2 thy1
   138             in
   139                 ProofKernel.CHOOSE v th1 th2 thy2
   140             end
   141           | rp (PConj(prf1,prf2)) thy =
   142             let
   143                 val (thy1,th1) = rp' prf1 thy
   144                 val (thy2,th2) = rp' prf2 thy1
   145             in
   146                 ProofKernel.CONJ th1 th2 thy2
   147             end
   148           | rp (PConjunct1 prf) thy =
   149             let
   150                 val (thy',th) = rp' prf thy
   151             in
   152                 ProofKernel.CONJUNCT1 th thy'
   153             end
   154           | rp (PConjunct2 prf) thy =
   155             let
   156                 val (thy',th) = rp' prf thy
   157             in
   158                 ProofKernel.CONJUNCT2 th thy'
   159             end
   160           | rp (PDisj1(prf,tm)) thy =
   161             let
   162                 val (thy',th) = rp' prf thy
   163             in
   164                 ProofKernel.DISJ1 th tm thy'
   165             end
   166           | rp (PDisj2(prf,tm)) thy =
   167             let
   168                 val (thy',th) = rp' prf thy
   169             in
   170                 ProofKernel.DISJ2 tm th thy'
   171             end
   172           | rp (PDisjCases(prf,prf1,prf2)) thy =
   173             let
   174                 val (thy',th)  = rp' prf  thy
   175                 val (thy1,th1) = rp' prf1 thy'
   176                 val (thy2,th2) = rp' prf2 thy1
   177             in
   178                 ProofKernel.DISJ_CASES th th1 th2 thy2
   179             end
   180           | rp (PNotI prf) thy =
   181             let
   182                 val (thy',th) = rp' prf thy
   183             in
   184                 ProofKernel.NOT_INTRO th thy'
   185             end
   186           | rp (PNotE prf) thy =
   187             let
   188                 val (thy',th) = rp' prf thy
   189             in
   190                 ProofKernel.NOT_ELIM th thy'
   191             end
   192           | rp (PContr(prf,tm)) thy =
   193             let
   194                 val (thy',th) = rp' prf thy
   195             in
   196                 ProofKernel.CCONTR tm th thy'
   197             end
   198           | rp (PTmSpec _) _ = raise ERR "rp" "Shouldn't reach here (PTmSpec)"
   199           | rp (PTyDef _) _ = raise ERR "rp" "Shouldn't reach here (PTyDef)"
   200           | rp (PTyIntro _) _ = raise ERR "rp" "Shouldn't reach here (PTyIntro)"
   201           | rp PDisk _ = raise ERR "rp" "Shouldn't reach here (PDisk)"
   202           | rp _ _ = raise ERR "rp" "What the hell is this? Which case did I forget?"
   203         and rp' p thy =
   204             let
   205                 val pc = content_of p
   206             in
   207                 case pc of
   208                     PDisk => (case disk_info_of p of
   209                                   SOME(thyname',thmname) =>
   210                                   (case Int.fromString thmname of
   211                                        SOME i =>
   212                                        if thyname' = thyname
   213                                        then
   214                                            (case Array.sub(int_thms,i-1) of
   215                                                 NONE =>
   216                                                 let
   217                                                     val (thy',th) = rp' (snd (import_proof thyname' thmname thy) thy) thy
   218                                                     val _ = Array.update(int_thms,i-1,SOME th)
   219                                                 in
   220                                                     (thy',th)
   221                                                 end
   222                                               | SOME th => (thy,th))
   223                                        else raise ERR "replay_proof" ("Library " ^ thyname' ^ " should be built before " ^ thyname ^ " (" ^ thmname ^ ")")
   224                                      | NONE => 
   225                                        (case ProofKernel.get_thm thyname' thmname thy of
   226                                             (thy',SOME res) => (thy',res)
   227                                           | (thy',NONE) => 
   228                                             if thyname' = thyname
   229                                             then
   230                                                 let
   231                                                     val _ = writeln ("Found no " ^ thmname ^ " theorem, replaying...")
   232                                                     val (f_opt,prf) = import_proof thyname' thmname thy'
   233                                                     val prf = prf thy'
   234                                                     val (thy',th) = replay_proof int_thms thyname' thmname prf thy'
   235                                                     val _ = writeln ("Successfully finished replaying "^thmname^" !")
   236                                                 in
   237                                                     case content_of prf of
   238                                                         PTmSpec _ => (thy',th)
   239                                                       | PTyDef  _ => (thy',th)
   240                                                       | PTyIntro _ => (thy',th)
   241                                                       | _ => ProofKernel.store_thm thyname' thmname th thy'
   242                                                 end
   243                                             else raise ERR "replay_proof" ("Library " ^ thyname' ^ " should be built before " ^ thyname ^ " (" ^ thmname ^ ")")))
   244                                 | NONE => raise ERR "rp'.PDisk" "Not enough information")
   245                   | PAxm(name,c) =>
   246                     (case ProofKernel.get_axiom thyname name thy of
   247                             (thy',SOME res) => (thy',res)
   248                           | (thy',NONE) => ProofKernel.new_axiom name c thy')
   249                   | PTmSpec(seg,names,prf') =>
   250                     let
   251                         val (thy',th) = rp' prf' thy
   252                     in
   253                         ProofKernel.new_specification seg thmname names th thy'
   254                     end
   255                   | PTyDef(seg,name,prf') =>
   256                     let
   257                         val (thy',th) = rp' prf' thy
   258                     in
   259                         ProofKernel.new_type_definition seg thmname name th thy'
   260                     end
   261                   | PTyIntro(seg,name,abs_name,rep_name,P,t,prf') =>
   262                     let
   263                         val (thy',th) = rp' prf' thy
   264                     in
   265                         ProofKernel.type_introduction seg thmname name abs_name rep_name (P,t) th thy'
   266                     end
   267                   | _ => rp pc thy
   268             end
   269     in
   270         rp' prf thy
   271     end
   272 
   273 fun setup_int_thms thyname thy =
   274     let
   275         val fname =
   276             case ProofKernel.get_proof_dir thyname thy of
   277                 SOME p => OS.Path.joinDirFile {dir=p,file=OS.Path.joinBaseExt{base = "facts",ext=SOME "lst"}}
   278               | NONE => error "Cannot find proof files"
   279         val is = TextIO.openIn fname
   280         val (num_int_thms,facts) =
   281             let
   282                 fun get_facts facts =
   283                     case TextIO.inputLine is of
   284                         NONE => (case facts of
   285                                    i::facts => (the (Int.fromString i),map ProofKernel.protect_factname (rev facts))
   286                                  | _ => raise ERR "replay_thm" "Bad facts.lst file")
   287                       | SOME fact => get_facts ((String.substring(fact,0,String.size fact -1 ))::facts)
   288             in
   289                 get_facts []
   290             end
   291         val _ = TextIO.closeIn is
   292         val int_thms = Array.array(num_int_thms,NONE:thm option)
   293     in
   294         (int_thms,facts)
   295     end
   296 
   297 fun import_single_thm thyname int_thms thmname thy =
   298     let
   299         fun replay_fact (thmname,thy) =
   300             let
   301                 val prf = mk_proof PDisk
   302                 val _ = set_disk_info_of prf thyname thmname
   303                 val _ = writeln ("Replaying "^thmname^" ...")
   304                 val p = fst (replay_proof int_thms thyname thmname prf thy)
   305             in
   306                 p
   307             end
   308     in
   309         replay_fact (thmname,thy)
   310     end
   311 
   312 fun import_thms thyname int_thms thmnames thy =
   313     let
   314         fun replay_fact thmname thy = 
   315             let
   316                 val prf = mk_proof PDisk        
   317                 val _ = set_disk_info_of prf thyname thmname
   318                 val _ = writeln ("Replaying "^thmname^" ...")
   319                 val p = fst (replay_proof int_thms thyname thmname prf thy)
   320             in
   321                 p
   322             end
   323         val res_thy = fold replay_fact thmnames thy
   324     in
   325         res_thy
   326     end
   327 
   328 fun import_thm thyname thmname thy =
   329     let
   330         val int_thms = fst (setup_int_thms thyname thy)
   331         fun replay_fact (thmname,thy) =
   332             let
   333                 val prf = mk_proof PDisk        
   334                 val _ = set_disk_info_of prf thyname thmname        
   335                 val _ = writeln ("Replaying "^thmname^" ...")
   336                 val p = fst (replay_proof int_thms thyname thmname prf thy)
   337             in 
   338                 p
   339             end
   340     in
   341         replay_fact (thmname,thy)
   342     end
   343 
   344 end