src/HOL/Import/replay.ML
author wenzelm
Sat Mar 13 14:43:04 2010 +0100 (2010-03-13)
changeset 35742 eb8d2f668bfc
parent 33035 15eab423e573
child 35842 7c170d39a808
permissions -rw-r--r--
global typedef;
     1 (*  Title:      HOL/Import/replay.ML
     2     Author:     Sebastian Skalberg (TU Muenchen)
     3 *)
     4 
     5 structure Replay =
     6 struct
     7 
     8 structure P = ProofKernel
     9 
    10 open ProofKernel
    11 open ImportRecorder
    12 
    13 exception REPLAY of string * string
    14 fun ERR f mesg = REPLAY (f,mesg)
    15 fun NY f = raise ERR f "NOT YET!"
    16 
    17 fun replay_proof int_thms thyname thmname prf thy =
    18     let
    19         val _ = ImportRecorder.start_replay_proof thyname thmname 
    20         fun rp (PRefl tm) thy = P.REFL tm thy
    21           | rp (PInstT(p,lambda)) thy =
    22             let
    23                 val (thy',th) = rp' p thy
    24             in
    25                 P.INST_TYPE lambda th thy'
    26             end
    27           | rp (PSubst(prfs,ctxt,prf)) thy =
    28             let
    29                 val (thy',ths) = fold_rev (fn p => fn (thy, ths) =>
    30                                            let
    31                                                val (thy',th) = rp' p thy
    32                                            in
    33                                                (thy',th::ths)
    34                                            end) prfs (thy,[])
    35                 val (thy'',th) = rp' prf thy'
    36             in
    37                 P.SUBST ths ctxt th thy''
    38             end
    39           | rp (PAbs(prf,v)) thy =
    40             let
    41                 val (thy',th) = rp' prf thy
    42             in
    43                 P.ABS v th thy'
    44             end
    45           | rp (PDisch(prf,tm)) thy =
    46             let
    47                 val (thy',th) = rp' prf thy
    48             in
    49                 P.DISCH tm th thy'
    50             end
    51           | rp (PMp(prf1,prf2)) thy =
    52             let
    53                 val (thy1,th1) = rp' prf1 thy
    54                 val (thy2,th2) = rp' prf2 thy1
    55             in
    56                 P.MP th1 th2 thy2
    57             end
    58           | rp (PHyp tm) thy = P.ASSUME tm thy
    59           | rp (PDef(seg,name,rhs)) thy =
    60             (case P.get_def seg name rhs thy of
    61                  (thy',SOME res) => (thy',res)
    62                | (thy',NONE) => 
    63                  if seg = thyname
    64                  then P.new_definition seg name rhs thy'
    65                  else raise ERR "replay_proof" ("Too late for term definition: "^seg^" != "^thyname))
    66           | rp (POracle(tg,asl,c)) thy = (*P.mk_oracle_thm tg (map be_contract asl,c)*) NY "ORACLE"
    67           | rp (PSpec(prf,tm)) thy =
    68             let
    69                 val (thy',th) = rp' prf thy
    70             in
    71                 P.SPEC tm th thy'
    72             end
    73           | rp (PInst(prf,theta)) thy =
    74             let
    75                 val (thy',th) = rp' prf thy
    76             in
    77                 P.INST theta th thy'
    78             end
    79           | rp (PGen(prf,v)) thy =
    80             let
    81                 val (thy',th) = rp' prf thy
    82                 val p = P.GEN v th thy'
    83             in
    84                 p
    85             end
    86           | rp (PGenAbs(prf,opt,vl)) thy =
    87             let
    88                 val (thy',th) = rp' prf thy
    89             in
    90                 P.GEN_ABS opt vl th thy'
    91             end
    92           | rp (PImpAS(prf1,prf2)) thy =
    93             let
    94                 val (thy1,th1) = rp' prf1 thy
    95                 val (thy2,th2) = rp' prf2 thy1
    96             in
    97                 P.IMP_ANTISYM th1 th2 thy2
    98             end
    99           | rp (PSym prf) thy =
   100             let
   101                 val (thy1,th) = rp' prf thy
   102             in
   103                 P.SYM th thy1
   104             end
   105           | rp (PTrans(prf1,prf2)) thy =
   106             let
   107                 val (thy1,th1) = rp' prf1 thy
   108                 val (thy2,th2) = rp' prf2 thy1
   109             in
   110                 P.TRANS th1 th2 thy2
   111             end
   112           | rp (PComb(prf1,prf2)) thy =
   113             let
   114                 val (thy1,th1) = rp' prf1 thy
   115                 val (thy2,th2) = rp' prf2 thy1
   116             in
   117                 P.COMB th1 th2 thy2
   118             end
   119           | rp (PEqMp(prf1,prf2)) thy =
   120             let
   121                 val (thy1,th1) = rp' prf1 thy
   122                 val (thy2,th2) = rp' prf2 thy1
   123             in
   124                 P.EQ_MP th1 th2 thy2
   125             end
   126           | rp (PEqImp prf) thy =
   127             let
   128                 val (thy',th) = rp' prf thy
   129             in
   130                 P.EQ_IMP_RULE th thy'
   131             end
   132           | rp (PExists(prf,ex,wit)) thy =
   133             let
   134                 val (thy',th) = rp' prf thy
   135             in
   136                 P.EXISTS ex wit th thy'
   137             end
   138           | rp (PChoose(v,prf1,prf2)) thy =
   139             let
   140                 val (thy1,th1) = rp' prf1 thy
   141                 val (thy2,th2) = rp' prf2 thy1
   142             in
   143                 P.CHOOSE v th1 th2 thy2
   144             end
   145           | rp (PConj(prf1,prf2)) thy =
   146             let
   147                 val (thy1,th1) = rp' prf1 thy
   148                 val (thy2,th2) = rp' prf2 thy1
   149             in
   150                 P.CONJ th1 th2 thy2
   151             end
   152           | rp (PConjunct1 prf) thy =
   153             let
   154                 val (thy',th) = rp' prf thy
   155             in
   156                 P.CONJUNCT1 th thy'
   157             end
   158           | rp (PConjunct2 prf) thy =
   159             let
   160                 val (thy',th) = rp' prf thy
   161             in
   162                 P.CONJUNCT2 th thy'
   163             end
   164           | rp (PDisj1(prf,tm)) thy =
   165             let
   166                 val (thy',th) = rp' prf thy
   167             in
   168                 P.DISJ1 th tm thy'
   169             end
   170           | rp (PDisj2(prf,tm)) thy =
   171             let
   172                 val (thy',th) = rp' prf thy
   173             in
   174                 P.DISJ2 tm th thy'
   175             end
   176           | rp (PDisjCases(prf,prf1,prf2)) thy =
   177             let
   178                 val (thy',th)  = rp' prf  thy
   179                 val (thy1,th1) = rp' prf1 thy'
   180                 val (thy2,th2) = rp' prf2 thy1
   181             in
   182                 P.DISJ_CASES th th1 th2 thy2
   183             end
   184           | rp (PNotI prf) thy =
   185             let
   186                 val (thy',th) = rp' prf thy
   187             in
   188                 P.NOT_INTRO th thy'
   189             end
   190           | rp (PNotE prf) thy =
   191             let
   192                 val (thy',th) = rp' prf thy
   193             in
   194                 P.NOT_ELIM th thy'
   195             end
   196           | rp (PContr(prf,tm)) thy =
   197             let
   198                 val (thy',th) = rp' prf thy
   199             in
   200                 P.CCONTR tm th thy'
   201             end
   202           | rp (PTmSpec _) _ = raise ERR "rp" "Shouldn't reach here (PTmSpec)"
   203           | rp (PTyDef _) _ = raise ERR "rp" "Shouldn't reach here (PTyDef)"
   204           | rp (PTyIntro _) _ = raise ERR "rp" "Shouldn't reach here (PTyIntro)"
   205           | rp PDisk _ = raise ERR "rp" "Shouldn't reach here (PDisk)"
   206           | rp _ _ = raise ERR "rp" "What the hell is this? Which case did I forget?"
   207         and rp' p thy =
   208             let
   209                 val pc = content_of p
   210             in
   211                 case pc of
   212                     PDisk => (case disk_info_of p of
   213                                   SOME(thyname',thmname) =>
   214                                   (case Int.fromString thmname of
   215                                        SOME i =>
   216                                        if thyname' = thyname
   217                                        then
   218                                            (case Array.sub(int_thms,i-1) of
   219                                                 NONE =>
   220                                                 let
   221                                                     val (thy',th) = rp' (snd (import_proof thyname' thmname thy) thy) thy
   222                                                     val _ = Array.update(int_thms,i-1,SOME th)
   223                                                 in
   224                                                     (thy',th)
   225                                                 end
   226                                               | SOME th => (thy,th))
   227                                        else raise ERR "replay_proof" ("Library " ^ thyname' ^ " should be built before " ^ thyname ^ " (" ^ thmname ^ ")")
   228                                      | NONE => 
   229                                        (case P.get_thm thyname' thmname thy of
   230                                             (thy',SOME res) => (thy',res)
   231                                           | (thy',NONE) => 
   232                                             if thyname' = thyname
   233                                             then
   234                                                 let
   235                                                     val _ = writeln ("Found no " ^ thmname ^ " theorem, replaying...")
   236                                                     val (f_opt,prf) = import_proof thyname' thmname thy'
   237                                                     val prf = prf thy'
   238                                                     val (thy',th) = replay_proof int_thms thyname' thmname prf thy'
   239                                                     val _ = writeln ("Successfully finished replaying "^thmname^" !")
   240                                                 in
   241                                                     case content_of prf of
   242                                                         PTmSpec _ => (thy',th)
   243                                                       | PTyDef  _ => (thy',th)
   244                                                       | PTyIntro _ => (thy',th)
   245                                                       | _ => P.store_thm thyname' thmname th thy'
   246                                                 end
   247                                             else raise ERR "replay_proof" ("Library " ^ thyname' ^ " should be built before " ^ thyname ^ " (" ^ thmname ^ ")")))
   248                                 | NONE => raise ERR "rp'.PDisk" "Not enough information")
   249                   | PAxm(name,c) =>
   250                     (case P.get_axiom thyname name thy of
   251                             (thy',SOME res) => (thy',res)
   252                           | (thy',NONE) => P.new_axiom name c thy')
   253                   | PTmSpec(seg,names,prf') =>
   254                     let
   255                         val (thy',th) = rp' prf' thy
   256                     in
   257                         P.new_specification seg thmname names th thy'
   258                     end
   259                   | PTyDef(seg,name,prf') =>
   260                     let
   261                         val (thy',th) = rp' prf' thy
   262                     in
   263                         P.new_type_definition seg thmname name th thy'
   264                     end
   265                   | PTyIntro(seg,name,abs_name,rep_name,P,t,prf') =>
   266                     let
   267                         val (thy',th) = rp' prf' thy
   268                     in
   269                         P.type_introduction seg thmname name abs_name rep_name (P,t) th thy'
   270                     end
   271                   | _ => rp pc thy
   272             end
   273     in
   274         let
   275             val x = rp' prf thy handle e => (writeln "Exception in replay_proof"; OldGoals.print_exn e)
   276             val _ = ImportRecorder.stop_replay_proof thyname thmname
   277         in
   278             x
   279         end
   280     end handle x => (ImportRecorder.abort_replay_proof thyname thmname; raise x)
   281 
   282 fun setup_int_thms thyname thy =
   283     let
   284         val fname =
   285             case P.get_proof_dir thyname thy of
   286                 SOME p => OS.Path.joinDirFile {dir=p,file=OS.Path.joinBaseExt{base = "facts",ext=SOME "lst"}}
   287               | NONE => error "Cannot find proof files"
   288         val is = TextIO.openIn fname
   289         val (num_int_thms,facts) =
   290             let
   291                 fun get_facts facts =
   292                     case TextIO.inputLine is of
   293                         NONE => (case facts of
   294                                    i::facts => (the (Int.fromString i),map P.protect_factname (rev facts))
   295                                  | _ => raise ERR "replay_thm" "Bad facts.lst file")
   296                       | SOME fact => get_facts ((String.substring(fact,0,String.size fact -1 ))::facts)
   297             in
   298                 get_facts []
   299             end
   300         val _ = TextIO.closeIn is
   301         val int_thms = Array.array(num_int_thms,NONE:thm option)
   302     in
   303         (int_thms,facts)
   304     end
   305 
   306 fun import_single_thm thyname int_thms thmname thy =
   307     let
   308         fun replay_fact (thmname,thy) =
   309             let
   310                 val prf = mk_proof PDisk
   311                 val _ = set_disk_info_of prf thyname thmname
   312                 val _ = writeln ("Replaying "^thmname^" ...")
   313                 val p = fst (replay_proof int_thms thyname thmname prf thy)
   314             in
   315                 p
   316             end
   317     in
   318         replay_fact (thmname,thy)
   319     end
   320 
   321 fun replay_chached_thm int_thms thyname thmname =
   322     let
   323         fun th_of thy = Skip_Proof.make_thm thy
   324         fun err msg = raise ERR "replay_cached_thm" msg
   325         val _ = writeln ("Replaying (from cache) "^thmname^" ...")
   326         fun rps [] thy = thy
   327           | rps (t::ts) thy = rps ts (rp t thy)
   328         and rp (ThmEntry (thyname', thmname', aborted, History history)) thy = rps history thy      
   329           | rp (DeltaEntry ds) thy = fold delta ds thy
   330         and delta (Specification (names, th)) thy = 
   331             fst (Choice_Specification.add_specification NONE names (thy,th_of thy th))
   332           | delta (Hol_mapping (thyname, thmname, isaname)) thy = 
   333             add_hol4_mapping thyname thmname isaname thy
   334           | delta (Hol_pending (thyname, thmname, th)) thy = 
   335             add_hol4_pending thyname thmname ([], th_of thy th) thy
   336           | delta (Consts cs) thy = Sign.add_consts_i (map (fn (c, T, mx) => (Binding.name c, T, mx)) cs) thy
   337           | delta (Hol_const_mapping (thyname, constname, fullcname)) thy = 
   338             add_hol4_const_mapping thyname constname true fullcname thy
   339           | delta (Hol_move (fullname, moved_thmname)) thy = 
   340             add_hol4_move fullname moved_thmname thy
   341           | delta (Defs (thmname, eq)) thy =
   342             snd (PureThy.add_defs false [((Binding.name thmname, eq), [])] thy)
   343           | delta (Hol_theorem (thyname, thmname, th)) thy =
   344             add_hol4_theorem thyname thmname ([], th_of thy th) thy
   345           | delta (Typedef (thmname, (t, vs, mx), c, repabs, th)) thy = 
   346             snd (Typedef.add_typedef_global false (Option.map Binding.name thmname) (Binding.name t, vs, mx) c
   347         (Option.map (pairself Binding.name) repabs) (rtac (th_of thy th) 1) thy)
   348           | delta (Hol_type_mapping (thyname, tycname, fulltyname)) thy =  
   349             add_hol4_type_mapping thyname tycname true fulltyname thy
   350           | delta (Indexed_theorem (i, th)) thy = 
   351             (Array.update (int_thms,i-1,SOME (P.to_hol_thm (th_of thy th))); thy)                   
   352           | delta (Protect_varname (s,t)) thy = (P.replay_protect_varname s t; thy)
   353           | delta (Dump s) thy = P.replay_add_dump s thy
   354     in
   355         rps
   356     end
   357 
   358 fun import_thms thyname int_thms thmnames thy =
   359     let
   360         fun zip names [] = ([], names)
   361           | zip [] _ = ([], [])
   362           | zip (thmname::names) ((ThmEntry (entry as (thyname',thmname',aborted,History history)))::ys) = 
   363             if thyname = thyname' andalso thmname = thmname' then
   364                 (if aborted then ([], thmname::names) else 
   365                  let
   366                      val _ = writeln ("theorem is in-sync: "^thmname)
   367                      val (cached,normal) = zip names ys
   368                  in
   369                      (entry::cached, normal)
   370                  end)
   371             else
   372                 let
   373                     val _ = writeln ("cached theorems are not in-sync,  expected: "^thmname^", found: "^thmname')
   374                     val _ = writeln ("proceeding with next uncached theorem...")
   375                 in
   376                     ([], thmname::names)
   377                 end
   378         (*      raise ERR "import_thms" ("cached theorems are not in-sync, expected: "^thmname^", found: "^thmname')*)
   379           | zip (thmname::_) (DeltaEntry _ :: _) = 
   380             raise ERR "import_thms" ("expected theorem '"^thmname^"', but found a delta")
   381         fun zip' xs (History ys) = 
   382             let
   383                 val _ = writeln ("length of xs: "^(string_of_int (length xs)))
   384                 val _ = writeln ("length of history: "^(string_of_int (length ys)))
   385             in
   386                 zip xs ys
   387             end
   388         fun replay_fact thmname thy = 
   389             let
   390                 val prf = mk_proof PDisk        
   391                 val _ = set_disk_info_of prf thyname thmname
   392                 val _ = writeln ("Replaying "^thmname^" ...")
   393                 val p = fst (replay_proof int_thms thyname thmname prf thy)
   394             in
   395                 p
   396             end
   397         fun replay_cache (_,thmname, _, History history) thy = replay_chached_thm int_thms thyname thmname history thy
   398         val (cached, normal) = zip' thmnames (ImportRecorder.get_history ())
   399         val _ = ImportRecorder.set_history (History (map ThmEntry cached))
   400         val res_thy = fold replay_fact normal (fold replay_cache cached thy)
   401     in
   402         res_thy
   403     end
   404 
   405 fun import_thm thyname thmname thy =
   406     let
   407         val int_thms = fst (setup_int_thms thyname thy)
   408         fun replay_fact (thmname,thy) =
   409             let
   410                 val prf = mk_proof PDisk        
   411                 val _ = set_disk_info_of prf thyname thmname        
   412                 val _ = writeln ("Replaying "^thmname^" ...")
   413                 val p = fst (replay_proof int_thms thyname thmname prf thy)
   414             in 
   415                 p
   416             end
   417     in
   418         replay_fact (thmname,thy)
   419     end
   420 
   421 end