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