src/HOL/Import/replay.ML
changeset 43918 6ca79a354c51
parent 41522 42d13d00ccfb
child 46201 afdc69f5156e
     1.1 --- a/src/HOL/Import/replay.ML	Wed Jul 20 08:46:17 2011 +0200
     1.2 +++ b/src/HOL/Import/replay.ML	Wed Jul 20 10:11:08 2011 +0200
     1.3 @@ -6,7 +6,6 @@
     1.4  struct
     1.5  
     1.6  open ProofKernel
     1.7 -open ImportRecorder
     1.8  
     1.9  exception REPLAY of string * string
    1.10  fun ERR f mesg = REPLAY (f,mesg)
    1.11 @@ -14,7 +13,6 @@
    1.12  
    1.13  fun replay_proof int_thms thyname thmname prf thy =
    1.14      let
    1.15 -        val _ = ImportRecorder.start_replay_proof thyname thmname 
    1.16          fun rp (PRefl tm) thy = ProofKernel.REFL tm thy
    1.17            | rp (PInstT(p,lambda)) thy =
    1.18              let
    1.19 @@ -269,13 +267,8 @@
    1.20                    | _ => rp pc thy
    1.21              end
    1.22      in
    1.23 -        let
    1.24 -            val x = rp' prf thy
    1.25 -            val _ = ImportRecorder.stop_replay_proof thyname thmname
    1.26 -        in
    1.27 -            x
    1.28 -        end
    1.29 -    end handle x => (ImportRecorder.abort_replay_proof thyname thmname; reraise x)  (* FIXME avoid handle x ?? *)
    1.30 +        rp' prf thy
    1.31 +    end
    1.32  
    1.33  fun setup_int_thms thyname thy =
    1.34      let
    1.35 @@ -316,74 +309,8 @@
    1.36          replay_fact (thmname,thy)
    1.37      end
    1.38  
    1.39 -fun replay_chached_thm int_thms thyname thmname =
    1.40 -    let
    1.41 -        fun th_of thy = Skip_Proof.make_thm thy
    1.42 -        fun err msg = raise ERR "replay_cached_thm" msg
    1.43 -        val _ = writeln ("Replaying (from cache) "^thmname^" ...")
    1.44 -        fun rps [] thy = thy
    1.45 -          | rps (t::ts) thy = rps ts (rp t thy)
    1.46 -        and rp (ThmEntry (thyname', thmname', aborted, History history)) thy = rps history thy      
    1.47 -          | rp (DeltaEntry ds) thy = fold delta ds thy
    1.48 -        and delta (Specification (names, th)) thy = 
    1.49 -            fst (Choice_Specification.add_specification NONE names (thy,th_of thy th))
    1.50 -          | delta (Hol_mapping (thyname, thmname, isaname)) thy = 
    1.51 -            add_hol4_mapping thyname thmname isaname thy
    1.52 -          | delta (Hol_pending (thyname, thmname, th)) thy = 
    1.53 -            add_hol4_pending thyname thmname ([], th_of thy th) thy
    1.54 -          | delta (Consts cs) thy = Sign.add_consts_i (map (fn (c, T, mx) => (Binding.name c, T, mx)) cs) thy
    1.55 -          | delta (Hol_const_mapping (thyname, constname, fullcname)) thy = 
    1.56 -            add_hol4_const_mapping thyname constname true fullcname thy
    1.57 -          | delta (Hol_move (fullname, moved_thmname)) thy = 
    1.58 -            add_hol4_move fullname moved_thmname thy
    1.59 -          | delta (Defs (thmname, eq)) thy =
    1.60 -            snd (Global_Theory.add_defs false [((Binding.name thmname, eq), [])] thy)
    1.61 -          | delta (Hol_theorem (thyname, thmname, th)) thy =
    1.62 -            add_hol4_theorem thyname thmname ([], th_of thy th) thy
    1.63 -          | delta (Typedef (thmname, (t, vs, mx), c, repabs, th)) thy = 
    1.64 -            snd (Typedef.add_typedef_global false (Option.map Binding.name thmname)
    1.65 -              (Binding.name t, map (rpair dummyS) vs, mx) c
    1.66 -        (Option.map (pairself Binding.name) repabs) (rtac (th_of thy th) 1) thy)
    1.67 -          | delta (Hol_type_mapping (thyname, tycname, fulltyname)) thy =  
    1.68 -            add_hol4_type_mapping thyname tycname true fulltyname thy
    1.69 -          | delta (Indexed_theorem (i, th)) thy = 
    1.70 -            (Array.update (int_thms,i-1,SOME (ProofKernel.to_hol_thm (th_of thy th))); thy)                   
    1.71 -          | delta (Protect_varname (s,t)) thy = (ProofKernel.replay_protect_varname s t; thy)
    1.72 -          | delta (Dump s) thy = ProofKernel.replay_add_dump s thy
    1.73 -    in
    1.74 -        rps
    1.75 -    end
    1.76 -
    1.77  fun import_thms thyname int_thms thmnames thy =
    1.78      let
    1.79 -        fun zip names [] = ([], names)
    1.80 -          | zip [] _ = ([], [])
    1.81 -          | zip (thmname::names) ((ThmEntry (entry as (thyname',thmname',aborted,History history)))::ys) = 
    1.82 -            if thyname = thyname' andalso thmname = thmname' then
    1.83 -                (if aborted then ([], thmname::names) else 
    1.84 -                 let
    1.85 -                     val _ = writeln ("theorem is in-sync: "^thmname)
    1.86 -                     val (cached,normal) = zip names ys
    1.87 -                 in
    1.88 -                     (entry::cached, normal)
    1.89 -                 end)
    1.90 -            else
    1.91 -                let
    1.92 -                    val _ = writeln ("cached theorems are not in-sync,  expected: "^thmname^", found: "^thmname')
    1.93 -                    val _ = writeln ("proceeding with next uncached theorem...")
    1.94 -                in
    1.95 -                    ([], thmname::names)
    1.96 -                end
    1.97 -        (*      raise ERR "import_thms" ("cached theorems are not in-sync, expected: "^thmname^", found: "^thmname')*)
    1.98 -          | zip (thmname::_) (DeltaEntry _ :: _) = 
    1.99 -            raise ERR "import_thms" ("expected theorem '"^thmname^"', but found a delta")
   1.100 -        fun zip' xs (History ys) = 
   1.101 -            let
   1.102 -                val _ = writeln ("length of xs: "^(string_of_int (length xs)))
   1.103 -                val _ = writeln ("length of history: "^(string_of_int (length ys)))
   1.104 -            in
   1.105 -                zip xs ys
   1.106 -            end
   1.107          fun replay_fact thmname thy = 
   1.108              let
   1.109                  val prf = mk_proof PDisk        
   1.110 @@ -393,10 +320,7 @@
   1.111              in
   1.112                  p
   1.113              end
   1.114 -        fun replay_cache (_,thmname, _, History history) thy = replay_chached_thm int_thms thyname thmname history thy
   1.115 -        val (cached, normal) = zip' thmnames (ImportRecorder.get_history ())
   1.116 -        val _ = ImportRecorder.set_history (History (map ThmEntry cached))
   1.117 -        val res_thy = fold replay_fact normal (fold replay_cache cached thy)
   1.118 +        val res_thy = fold replay_fact thmnames thy
   1.119      in
   1.120          res_thy
   1.121      end