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