src/Pure/Isar/code.ML
changeset 28673 d746a8c12c43
parent 28672 0baf1d9c6780
child 28695 f7a06d7284c8
     1.1 --- a/src/Pure/Isar/code.ML	Thu Oct 23 13:52:28 2008 +0200
     1.2 +++ b/src/Pure/Isar/code.ML	Thu Oct 23 14:22:16 2008 +0200
     1.3 @@ -15,7 +15,7 @@
     1.4    val add_default_eqn_attr: Attrib.src
     1.5    val del_eqn: thm -> theory -> theory
     1.6    val del_eqns: string -> theory -> theory
     1.7 -  val add_eqnl: string * (thm * bool) list Susp.T -> theory -> theory
     1.8 +  val add_eqnl: string * (thm * bool) list Lazy.T -> theory -> theory
     1.9    val map_pre: (MetaSimplifier.simpset -> MetaSimplifier.simpset) -> theory -> theory
    1.10    val map_post: (MetaSimplifier.simpset -> MetaSimplifier.simpset) -> theory -> theory
    1.11    val add_inline: thm -> theory -> theory
    1.12 @@ -117,16 +117,16 @@
    1.13  
    1.14  (* defining equations with linear flag, default flag and lazy theorems *)
    1.15  
    1.16 -fun pretty_lthms ctxt r = case Susp.peek r
    1.17 +fun pretty_lthms ctxt r = case Lazy.peek r
    1.18   of SOME thms => map (ProofContext.pretty_thm ctxt o fst) (Exn.release thms)
    1.19    | NONE => [Pretty.str "[...]"];
    1.20  
    1.21  fun certificate thy f r =
    1.22 -  case Susp.peek r
    1.23 -   of SOME thms => (Susp.value o f thy) (Exn.release thms)
    1.24 +  case Lazy.peek r
    1.25 +   of SOME thms => (Lazy.value o f thy) (Exn.release thms)
    1.26      | NONE => let
    1.27          val thy_ref = Theory.check_thy thy;
    1.28 -      in Susp.delay (fn () => (f (Theory.deref thy_ref) o Susp.force) r) end;
    1.29 +      in Lazy.lazy (fn () => (f (Theory.deref thy_ref) o Lazy.force) r) end;
    1.30  
    1.31  fun add_drop_redundant thy (thm, linear) thms =
    1.32    let
    1.33 @@ -141,13 +141,13 @@
    1.34        else false;
    1.35    in (thm, linear) :: filter_out drop thms end;
    1.36  
    1.37 -fun add_thm thy _ thm (false, thms) = (false, Susp.map_force (add_drop_redundant thy thm) thms)
    1.38 -  | add_thm thy true thm (true, thms) = (true, Susp.map_force (fn thms => thms @ [thm]) thms)
    1.39 -  | add_thm thy false thm (true, thms) = (false, Susp.value [thm]);
    1.40 +fun add_thm thy _ thm (false, thms) = (false, Lazy.map_force (add_drop_redundant thy thm) thms)
    1.41 +  | add_thm thy true thm (true, thms) = (true, Lazy.map_force (fn thms => thms @ [thm]) thms)
    1.42 +  | add_thm thy false thm (true, thms) = (false, Lazy.value [thm]);
    1.43  
    1.44  fun add_lthms lthms _ = (false, lthms);
    1.45  
    1.46 -fun del_thm thm = (apsnd o Susp.map_force) (remove (eq_fst Thm.eq_thm_prop) (thm, true));
    1.47 +fun del_thm thm = (apsnd o Lazy.map_force) (remove (eq_fst Thm.eq_thm_prop) (thm, true));
    1.48  
    1.49  fun merge_defthms ((true, _), defthms2) = defthms2
    1.50    | merge_defthms (defthms1 as (false, _), (true, _)) = defthms1
    1.51 @@ -171,7 +171,7 @@
    1.52  (* specification data *)
    1.53  
    1.54  datatype spec = Spec of {
    1.55 -  eqns: (bool * (thm * bool) list Susp.T) Symtab.table,
    1.56 +  eqns: (bool * (thm * bool) list Lazy.T) Symtab.table,
    1.57    dtyps: ((string * sort) list * (string * typ list) list) Symtab.table,
    1.58    cases: (int * string list) Symtab.table * unit Symtab.table
    1.59  };
    1.60 @@ -471,7 +471,7 @@
    1.61        |> maps (map fst o these o try (#params o AxClass.get_info thy))
    1.62        |> map_filter (fn c => try (AxClass.param_of_inst thy) (c, tyco))
    1.63        |> map (Symtab.lookup ((the_eqns o the_exec) thy))
    1.64 -      |> (map o Option.map) (map fst o Susp.force o snd)
    1.65 +      |> (map o Option.map) (map fst o Lazy.force o snd)
    1.66        |> maps these
    1.67        |> map (map (snd o dest_TVar) o Sign.const_typargs thy o Code_Unit.const_typ_eqn);
    1.68      val inter_sorts = map2 (curry (Sorts.inter_sort algebra));
    1.69 @@ -544,7 +544,7 @@
    1.70              else ();
    1.71          in
    1.72            (map_exec_purge (SOME [c]) o map_eqns) (Symtab.map_default
    1.73 -            (c, (true, Susp.value [])) (add_thm thy default (thm, linear))) thy
    1.74 +            (c, (true, Lazy.value [])) (add_thm thy default (thm, linear))) thy
    1.75          end
    1.76      | NONE => thy;
    1.77  
    1.78 @@ -559,7 +559,7 @@
    1.79    | NONE => thy;
    1.80  
    1.81  fun del_eqns c = map_exec_purge (SOME [c])
    1.82 -  (map_eqns (Symtab.map_entry c (K (false, Susp.value []))));
    1.83 +  (map_eqns (Symtab.map_entry c (K (false, Lazy.value []))));
    1.84  
    1.85  fun add_eqnl (c, lthms) thy =
    1.86    let
    1.87 @@ -567,7 +567,7 @@
    1.88        (fn thy => map (Code_Unit.assert_linear) o certify_const thy c) lthms;
    1.89    in
    1.90      map_exec_purge (SOME [c])
    1.91 -      (map_eqns (Symtab.map_default (c, (true, Susp.value []))
    1.92 +      (map_eqns (Symtab.map_default (c, (true, Lazy.value []))
    1.93          (add_lthms lthms'))) thy
    1.94    end;
    1.95  
    1.96 @@ -648,7 +648,7 @@
    1.97  
    1.98  fun get_eqns thy c =
    1.99    Symtab.lookup ((the_eqns o the_exec) thy) c
   1.100 -  |> Option.map (Susp.force o snd)
   1.101 +  |> Option.map (Lazy.force o snd)
   1.102    |> these
   1.103    |> (map o apfst) (Thm.transfer thy);
   1.104