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