src/HOL/Library/code_lazy.ML
author haftmann
Wed Jul 18 20:51:21 2018 +0200 (11 months ago)
changeset 68658 16cc1161ad7f
parent 68549 bbc742358156
child 69568 de09a7261120
permissions -rw-r--r--
tuned equation
     1 (* Author: Pascal Stoop, ETH Zurich
     2    Author: Andreas Lochbihler, Digital Asset *)
     3 
     4 signature CODE_LAZY =
     5 sig
     6   type lazy_info =
     7     {eagerT: typ,
     8      lazyT: typ,
     9      ctr: term,
    10      destr: term,
    11      lazy_ctrs: term list,
    12      case_lazy: term,
    13      active: bool,
    14      activate: theory -> theory,
    15      deactivate: theory -> theory};
    16   val code_lazy_type: string -> theory -> theory
    17   val activate_lazy_type: string -> theory -> theory
    18   val deactivate_lazy_type: string -> theory -> theory
    19   val activate_lazy_types: theory -> theory
    20   val deactivate_lazy_types: theory -> theory
    21 
    22   val get_lazy_types: theory -> (string * lazy_info) list
    23 
    24   val print_lazy_types: theory -> unit
    25 
    26   val transform_code_eqs: Proof.context -> (thm * bool) list -> (thm * bool) list option
    27 end;
    28 
    29 structure Code_Lazy : CODE_LAZY =
    30 struct
    31 
    32 type lazy_info =
    33   {eagerT: typ,
    34    lazyT: typ,
    35    ctr: term,
    36    destr: term,
    37    lazy_ctrs: term list,
    38    case_lazy: term,
    39    active: bool,
    40    activate: theory -> theory,
    41    deactivate: theory -> theory};
    42 
    43 fun map_active f {eagerT, lazyT, ctr, destr, lazy_ctrs, case_lazy, active, activate, deactivate} =
    44   { eagerT = eagerT, 
    45     lazyT = lazyT,
    46     ctr = ctr,
    47     destr = destr,
    48     lazy_ctrs = lazy_ctrs,
    49     case_lazy = case_lazy,
    50     active = f active,
    51     activate = activate,
    52     deactivate = deactivate
    53   }
    54 
    55 structure Laziness_Data = Theory_Data(
    56   type T = lazy_info Symtab.table;
    57   val empty = Symtab.empty;
    58   val merge = Symtab.join (fn _ => fn (_, record) => record);
    59   val extend = I;
    60 );
    61 
    62 fun fold_type type' tfree tvar typ =
    63   let
    64     fun go (Type (s, Ts)) = type' (s, map go Ts)
    65       | go (TFree T) = tfree T
    66       | go (TVar T) = tvar T
    67   in
    68     go typ
    69   end;
    70 
    71 fun read_typ lthy name =
    72   let
    73     val (s, Ts) = Proof_Context.read_type_name {proper = true, strict = true} lthy name |> dest_Type
    74     val (Ts', _) = Ctr_Sugar_Util.mk_TFrees (length Ts) lthy
    75   in 
    76     Type (s, Ts')
    77   end
    78 
    79 fun mk_name prefix suffix name ctxt =
    80   Ctr_Sugar_Util.mk_fresh_names ctxt 1 (prefix ^ name ^ suffix) |>> hd;
    81 fun generate_typedef_name name ctxt = mk_name "" "_lazy" name ctxt;
    82 
    83 fun add_syntax_definition short_type_name eagerT lazyT lazy_ctr lthy = 
    84   let
    85     val (name, _) = mk_name "lazy_" "" short_type_name lthy
    86     val freeT = HOLogic.unitT --> lazyT
    87     val lazyT' = Type (@{type_name lazy}, [lazyT])
    88     val def = Logic.all_const freeT $ absdummy freeT (Logic.mk_equals (
    89       Free (name, (freeT --> eagerT)) $ Bound 0,
    90       lazy_ctr $ (Const (@{const_name delay}, (freeT --> lazyT')) $ Bound 0)))
    91     val (_, lthy') = Local_Theory.open_target lthy
    92     val ((t, (_, thm)), lthy') = Specification.definition NONE [] [] 
    93       ((Thm.def_binding (Binding.name name), []), def) lthy'
    94     val lthy' = Specification.notation true ("", false) [(t, Mixfix.mixfix "_")] lthy'
    95     val lthy = Local_Theory.close_target lthy'
    96     val def_thm = singleton (Proof_Context.export lthy' lthy) thm
    97   in
    98     (def_thm, lthy)
    99   end;
   100 
   101 fun add_ctr_code raw_ctrs case_thms thy =
   102   let
   103     fun mk_case_certificate ctxt raw_thms =
   104       let
   105         val thms = raw_thms
   106           |> Conjunction.intr_balanced
   107           |> Thm.unvarify_global (Proof_Context.theory_of ctxt)
   108           |> Conjunction.elim_balanced (length raw_thms)
   109           |> map Simpdata.mk_meta_eq
   110           |> map Drule.zero_var_indexes
   111         val thm1 = case thms of
   112           thm :: _ => thm
   113           | _ => raise Empty
   114         val params = Term.add_free_names (Thm.prop_of thm1) [];
   115         val rhs = thm1
   116           |> Thm.prop_of |> Logic.dest_equals |> fst |> strip_comb
   117           ||> fst o split_last |> list_comb
   118         val lhs = Free (singleton (Name.variant_list params) "case", fastype_of rhs);
   119         val assum = Thm.cterm_of ctxt (Logic.mk_equals (lhs, rhs))
   120       in
   121         thms
   122         |> Conjunction.intr_balanced
   123         |> rewrite_rule ctxt [Thm.symmetric (Thm.assume assum)]
   124         |> Thm.implies_intr assum
   125         |> Thm.generalize ([], params) 0
   126         |> Axclass.unoverload ctxt
   127         |> Thm.varifyT_global
   128       end
   129     val ctrs = map (apsnd (perhaps (try Logic.unvarifyT_global))) raw_ctrs
   130     val unover_ctrs = map (fn ctr as (_, fcT) => (Axclass.unoverload_const thy ctr, fcT)) ctrs
   131   in
   132     if can (Code.constrset_of_consts thy) unover_ctrs then
   133       thy
   134       |> Code.declare_datatype_global ctrs
   135       |> fold_rev (Code.add_eqn_global o rpair true) case_thms
   136       |> Code.declare_case_global (mk_case_certificate (Proof_Context.init_global thy) case_thms)
   137     else
   138       thy
   139   end;
   140 
   141 fun not_found s = error (s ^ " has not been added as lazy type");
   142 
   143 fun validate_type_name thy type_name =
   144   let
   145     val lthy = Named_Target.theory_init thy
   146     val eager_type = read_typ lthy type_name
   147     val type_name = case eager_type of
   148       Type (s, _) => s
   149       | _ => raise Match
   150   in
   151     type_name
   152   end;
   153 
   154 fun set_active_lazy_type value eager_type_string thy =
   155   let
   156     val type_name = validate_type_name thy eager_type_string
   157     val x =
   158       case Symtab.lookup (Laziness_Data.get thy) type_name of
   159         NONE => not_found type_name
   160         | SOME x => x
   161     val new_x = map_active (K value) x
   162     val thy1 = if value = #active x
   163       then thy
   164       else if value
   165         then #activate x thy
   166         else #deactivate x thy
   167   in
   168     Laziness_Data.map (Symtab.update (type_name, new_x)) thy1
   169   end;
   170 
   171 fun set_active_lazy_types value thy =
   172   let
   173     val lazy_type_names = Symtab.keys (Laziness_Data.get thy)
   174     fun fold_fun value type_name thy =
   175       let
   176         val x =
   177           case Symtab.lookup (Laziness_Data.get thy) type_name of
   178             SOME x => x
   179             | NONE => raise Match
   180         val new_x = map_active (K value) x
   181         val thy1 = if value = #active x
   182           then thy
   183           else if value
   184             then #activate x thy
   185             else #deactivate x thy
   186       in
   187         Laziness_Data.map (Symtab.update (type_name, new_x)) thy1
   188       end
   189   in
   190     fold (fold_fun value) lazy_type_names thy
   191   end;
   192 
   193 (* code_lazy_type : string -> theory -> theory *)
   194 fun code_lazy_type eager_type_string thy =
   195   let
   196     val lthy = Named_Target.theory_init thy
   197     val eagerT = read_typ lthy eager_type_string
   198     val (type_name, type_args) = dest_Type eagerT
   199     val short_type_name = Long_Name.base_name type_name
   200     val _ = if Symtab.defined (Laziness_Data.get thy) type_name
   201       then error (type_name ^ " has already been added as lazy type.")
   202       else ()
   203     val {case_thms, casex, ctrs, ...} = case Ctr_Sugar.ctr_sugar_of lthy type_name of
   204         SOME x => x
   205       | _ => error (type_name ^ " is not registered with free constructors.")
   206 
   207     fun substitute_ctr (old_T, new_T) ctr_T lthy =
   208       let
   209         val old_ctr_vars = map TVar (Term.add_tvarsT ctr_T [])
   210         val old_ctr_Ts = map TFree (Term.add_tfreesT ctr_T []) @ old_ctr_vars
   211         val (new_ctr_Ts, lthy') = Ctr_Sugar_Util.mk_TFrees (length old_ctr_Ts) lthy
   212 
   213         fun double_type_fold Ts = case Ts of
   214           (Type (_, Ts1), Type (_, Ts2)) => flat (map double_type_fold (Ts1 ~~ Ts2))
   215           | (Type _, _) => raise Match
   216           | (_, Type _) => raise Match
   217           | Ts => [Ts]
   218         fun map_fun1 f = List.foldr
   219           (fn ((T1, T2), f) => fn T => if T = T1 then T2 else f T)
   220           f
   221           (double_type_fold (old_T, new_T))
   222         val map_fun2 = AList.lookup (op =) (old_ctr_Ts ~~ new_ctr_Ts) #> the
   223         val map_fun = map_fun1 map_fun2
   224 
   225         val new_ctr_type = fold_type Type (map_fun o TFree) (map_fun o TVar) ctr_T
   226       in
   227         (new_ctr_type, lthy')
   228       end
   229 
   230     val (short_lazy_type_name, lthy1) = generate_typedef_name short_type_name lthy
   231 
   232     fun mk_lazy_typedef (name, eager_type) lthy =
   233       let
   234         val binding = Binding.name name
   235         val (result, lthy1) = (Typedef.add_typedef
   236             { overloaded=false }
   237             (binding, rev (Term.add_tfreesT eager_type []), Mixfix.NoSyn)
   238             (Const (@{const_name "top"}, Type (@{type_name set}, [eager_type])))
   239             NONE
   240             (fn ctxt => resolve_tac ctxt [@{thm UNIV_witness}] 1)
   241           o (Local_Theory.open_target #> snd)) lthy
   242       in
   243          (binding, result, Local_Theory.close_target lthy1)
   244       end;
   245 
   246     val (typedef_binding, (_, info), lthy2) = mk_lazy_typedef (short_lazy_type_name, eagerT) lthy1
   247 
   248     val lazy_type = Type (Local_Theory.full_name lthy2 typedef_binding, type_args)
   249     val (Abs_lazy, Rep_lazy) =
   250       let
   251         val info = fst info
   252         val Abs_name = #Abs_name info
   253         val Rep_name = #Rep_name info
   254         val Abs_type = eagerT --> lazy_type
   255         val Rep_type = lazy_type --> eagerT
   256       in
   257         (Const (Abs_name, Abs_type), Const (Rep_name, Rep_type))
   258       end
   259     val Abs_inverse = #Abs_inverse (snd info)
   260     val Rep_inverse = #Rep_inverse (snd info)
   261 
   262     val (ctrs', lthy3) = List.foldr
   263       (fn (Const (s, T), (ctrs, lthy)) => let
   264             val (T', lthy') = substitute_ctr (body_type T, eagerT) T lthy
   265           in
   266             ((Const (s, T')) :: ctrs, lthy')
   267           end
   268       )
   269       ([], lthy2)
   270       ctrs
   271 
   272     fun to_destr_eagerT typ = case typ of
   273           Type (@{type_name "fun"}, [_, Type (@{type_name "fun"}, Ts)]) => 
   274           to_destr_eagerT (Type (@{type_name "fun"}, Ts))
   275         | Type (@{type_name "fun"}, [T, _]) => T
   276         | _ => raise Match
   277     val (case', lthy4) = 
   278       let
   279         val (eager_case, caseT) = dest_Const casex
   280         val (caseT', lthy') = substitute_ctr (to_destr_eagerT caseT, eagerT) caseT lthy3
   281       in (Const (eager_case, caseT'), lthy') end
   282 
   283     val ctr_names = map (Long_Name.base_name o fst o dest_Const) ctrs
   284     val ((((lazy_ctr_name, lazy_sel_name), lazy_ctrs_name), lazy_case_name), ctxt) = lthy4
   285       |> mk_name "Lazy_" "" short_type_name
   286       ||>> mk_name "unlazy_" "" short_type_name
   287       ||>> fold_map (mk_name "" "_Lazy") ctr_names
   288       ||>> mk_name "case_" "_lazy" short_type_name
   289 
   290     fun mk_def (name, T, rhs) lthy =
   291       let
   292         val binding = Binding.name name
   293         val ((_, (_, thm)), lthy1) = 
   294           Local_Theory.open_target lthy |> snd
   295           |> Specification.definition NONE [] [] ((Thm.def_binding binding, []), rhs)
   296         val lthy2 = Local_Theory.close_target lthy1
   297         val def_thm = hd (Proof_Context.export lthy1 lthy2 [thm])
   298       in
   299         ({binding = binding, const = Const (Local_Theory.full_name lthy2 binding, T), thm = def_thm}, lthy2)
   300       end;
   301     
   302     val lazy_datatype = Type (@{type_name lazy}, [lazy_type])
   303     val Lazy_type = lazy_datatype --> eagerT
   304     val unstr_type = eagerT --> lazy_datatype
   305     
   306     fun apply_bounds i n term =
   307       if n > i then apply_bounds i (n-1) (term $ Bound (n-1))
   308       else term
   309     fun all_abs Ts t = Logic.list_all (map (pair Name.uu) Ts, t)
   310     fun mk_force t = Const (@{const_name force}, lazy_datatype --> lazy_type) $ t
   311     fun mk_delay t = Const (@{const_name delay}, (@{typ unit} --> lazy_type) --> lazy_datatype) $ t
   312 
   313     val lazy_ctr = all_abs [lazy_datatype]
   314       (Logic.mk_equals (Free (lazy_ctr_name, Lazy_type) $ Bound 0, Rep_lazy $ mk_force (Bound 0)))
   315     val (lazy_ctr_def, lthy5) = mk_def (lazy_ctr_name, Lazy_type, lazy_ctr) lthy4
   316 
   317     val lazy_sel = all_abs [eagerT]
   318       (Logic.mk_equals (Free (lazy_sel_name, unstr_type) $ Bound 0, 
   319         mk_delay (Abs (Name.uu, @{typ unit}, Abs_lazy $ Bound 1))))
   320     val (lazy_sel_def, lthy6) = mk_def (lazy_sel_name, unstr_type, lazy_sel) lthy5
   321 
   322     fun mk_lazy_ctr (name, eager_ctr) =
   323       let
   324         val (_, ctrT) = dest_Const eager_ctr
   325         fun to_lazy_ctrT (Type (@{type_name fun}, [T1, T2])) = T1 --> to_lazy_ctrT T2
   326           | to_lazy_ctrT T = if T = eagerT then lazy_type else raise Match
   327         val lazy_ctrT = to_lazy_ctrT ctrT
   328         val argsT = binder_types ctrT
   329         val lhs = apply_bounds 0 (length argsT) (Free (name, lazy_ctrT))
   330         val rhs = Abs_lazy $ apply_bounds 0 (length argsT) eager_ctr
   331       in
   332         mk_def (name, lazy_ctrT, all_abs argsT (Logic.mk_equals (lhs, rhs)))
   333       end
   334     val (lazy_ctrs_def, lthy7) = fold_map mk_lazy_ctr (lazy_ctrs_name ~~ ctrs') lthy6
   335 
   336     val (lazy_case_def, lthy8) =
   337       let
   338         val (_, caseT) = dest_Const case'
   339         fun to_lazy_caseT (Type (@{type_name fun}, [T1, T2])) =
   340             if T1 = eagerT then lazy_type --> T2 else T1 --> to_lazy_caseT T2
   341         val lazy_caseT = to_lazy_caseT caseT
   342         val argsT = binder_types lazy_caseT
   343         val n = length argsT
   344         val lhs = apply_bounds 0 n (Free (lazy_case_name, lazy_caseT)) 
   345         val rhs = apply_bounds 1 n case' $ (Rep_lazy $ Bound 0)
   346       in
   347         mk_def (lazy_case_name, lazy_caseT, all_abs argsT (Logic.mk_equals (lhs, rhs))) lthy7
   348       end
   349 
   350     fun mk_thm ((name, term), thms) lthy =
   351       let
   352         val binding = Binding.name name
   353         fun tac {context, ...} = Simplifier.simp_tac
   354           (put_simpset HOL_basic_ss context addsimps thms)
   355           1
   356         val thm = Goal.prove lthy [] [] term tac
   357         val (_, lthy1) = lthy
   358           |> Local_Theory.open_target |> snd
   359           |> Local_Theory.note ((binding, []), [thm])
   360       in
   361         (thm, Local_Theory.close_target lthy1)
   362       end
   363     fun mk_thms exec_list lthy = fold_map mk_thm exec_list lthy
   364 
   365     val mk_eq = HOLogic.mk_Trueprop o HOLogic.mk_eq
   366 
   367     val lazy_ctrs = map #const lazy_ctrs_def
   368     val eager_lazy_ctrs = ctrs' ~~ lazy_ctrs
   369 
   370     val (((((((Lazy_delay_eq_name, Rep_ctr_names), ctrs_lazy_names), force_sel_name), case_lazy_name),
   371       sel_lazy_name), case_ctrs_name), _) = lthy5
   372       |> mk_name "Lazy_" "_delay" short_type_name
   373       ||>> fold_map (mk_name "Rep_" "_Lazy") ctr_names
   374       ||>> fold_map (mk_name "" "_conv_lazy") ctr_names
   375       ||>> mk_name "force_unlazy_" "" short_type_name
   376       ||>> mk_name "case_" "_conv_lazy" short_type_name
   377       ||>> mk_name "Lazy_" "_inverse" short_type_name
   378       ||>> fold_map (mk_name ("case_" ^ short_type_name ^ "_lazy_") "") ctr_names
   379 
   380     val mk_Lazy_delay_eq =
   381       (#const lazy_ctr_def $ mk_delay (Bound 0), Rep_lazy $ (Bound 0 $ @{const Unity}))
   382       |> mk_eq |> all_abs [@{typ unit} --> lazy_type]
   383     val (Lazy_delay_thm, lthy8a) = mk_thm 
   384       ((Lazy_delay_eq_name, mk_Lazy_delay_eq), [#thm lazy_ctr_def, @{thm force_delay}])
   385       lthy8
   386 
   387     fun mk_lazy_ctr_eq (eager_ctr, lazy_ctr) =
   388       let
   389         val (_, ctrT) = dest_Const eager_ctr
   390         val argsT = binder_types ctrT
   391         val args = length argsT
   392       in
   393         (Rep_lazy $ apply_bounds 0 args lazy_ctr, apply_bounds 0 args eager_ctr)
   394         |> mk_eq |> all_abs argsT
   395       end
   396     val Rep_ctr_eqs = map mk_lazy_ctr_eq eager_lazy_ctrs
   397     val (Rep_ctr_thms, lthy8b) = mk_thms
   398         ((Rep_ctr_names ~~ Rep_ctr_eqs) ~~
   399           (map (fn def => [#thm def, Abs_inverse, @{thm UNIV_I}]) lazy_ctrs_def)
   400         )
   401         lthy8a
   402 
   403     fun mk_ctrs_lazy_eq (eager_ctr, lazy_ctr) =
   404       let
   405         val argsT = dest_Const eager_ctr |> snd |> binder_types
   406         val n = length argsT
   407         val lhs = apply_bounds 0 n eager_ctr
   408         val rhs = #const lazy_ctr_def $ 
   409           (mk_delay (Abs (Name.uu, @{typ unit}, apply_bounds 1 (n + 1) lazy_ctr)))
   410       in
   411         (lhs, rhs) |> mk_eq |> all_abs argsT
   412       end
   413     val ctrs_lazy_eq = map mk_ctrs_lazy_eq eager_lazy_ctrs 
   414     val (ctrs_lazy_thms, lthy8c) = mk_thms
   415       ((ctrs_lazy_names ~~ ctrs_lazy_eq) ~~ map (fn thm => [Lazy_delay_thm, thm]) Rep_ctr_thms)
   416       lthy8b
   417 
   418     val force_sel_eq = 
   419       (mk_force (#const lazy_sel_def $ Bound 0), Abs_lazy $ Bound 0)
   420       |> mk_eq |> all_abs [eagerT]
   421     val (force_sel_thm, lthy8d) = mk_thm
   422         ((force_sel_name, force_sel_eq), [#thm lazy_sel_def, @{thm force_delay}])
   423         lthy8c
   424 
   425     val case_lazy_eq = 
   426       let
   427         val (_, caseT) = case' |> dest_Const
   428         val argsT = binder_types caseT
   429         val n = length argsT
   430         val lhs = apply_bounds 0 n case'
   431         val rhs = apply_bounds 1 n (#const lazy_case_def) $ (mk_force (#const lazy_sel_def $ Bound 0))
   432       in
   433         (lhs, rhs) |> mk_eq |> all_abs argsT
   434       end
   435     val (case_lazy_thm, lthy8e) = mk_thm
   436         ((case_lazy_name, case_lazy_eq), 
   437         [#thm lazy_case_def, force_sel_thm, Abs_inverse, @{thm UNIV_I}])
   438         lthy8d
   439 
   440     val sel_lazy_eq =
   441       (#const lazy_sel_def $ (#const lazy_ctr_def $ Bound 0), Bound 0)
   442       |> mk_eq |> all_abs [lazy_datatype]
   443     val (sel_lazy_thm, lthy8f) = mk_thm
   444       ((sel_lazy_name, sel_lazy_eq),
   445       [#thm lazy_sel_def, #thm lazy_ctr_def, Rep_inverse, @{thm delay_force}])
   446       lthy8e
   447 
   448     fun mk_case_ctrs_eq (i, lazy_ctr) =
   449       let
   450         val lazy_case = #const lazy_case_def
   451         val (_, ctrT) = dest_Const lazy_ctr
   452         val ctr_argsT = binder_types ctrT
   453         val ctr_args_n = length ctr_argsT
   454         val (_, caseT) = dest_Const lazy_case
   455         val case_argsT = binder_types caseT
   456 
   457         fun n_bounds_from m n t =
   458           if n > 0 then n_bounds_from (m - 1) (n - 1) (t $ Bound (m - 1)) else t
   459 
   460         val case_argsT' = take (length case_argsT - 1) case_argsT
   461         val Ts = case_argsT' @ ctr_argsT
   462         val num_abs_types = length Ts
   463         val lhs = n_bounds_from num_abs_types (length case_argsT') lazy_case $
   464           apply_bounds 0 ctr_args_n lazy_ctr
   465         val rhs = apply_bounds 0 ctr_args_n (Bound (num_abs_types - i - 1))
   466       in
   467         (lhs, rhs) |> mk_eq |> all_abs Ts
   468       end
   469     val case_ctrs_eq = map_index mk_case_ctrs_eq lazy_ctrs
   470     val (case_ctrs_thms, lthy9) = mk_thms
   471         ((case_ctrs_name ~~ case_ctrs_eq) ~~
   472          map2 (fn thm1 => fn thm2 => [#thm lazy_case_def, thm1, thm2]) Rep_ctr_thms case_thms
   473         )
   474         lthy8f
   475 
   476     val (pat_def_thm, lthy10) = 
   477       add_syntax_definition short_type_name eagerT lazy_type (#const lazy_ctr_def) lthy9
   478 
   479     val add_lazy_ctrs =
   480       Code.declare_datatype_global [dest_Const (#const lazy_ctr_def)]
   481     val eager_ctrs = map (apsnd (perhaps (try Logic.unvarifyT_global)) o dest_Const) ctrs
   482     val add_eager_ctrs =
   483       fold Code.del_eqn_global ctrs_lazy_thms
   484       #> Code.declare_datatype_global eager_ctrs
   485     val add_code_eqs = fold (Code.add_eqn_global o rpair true) 
   486       ([case_lazy_thm, sel_lazy_thm])
   487     val add_lazy_ctr_thms = fold (Code.add_eqn_global o rpair true) ctrs_lazy_thms
   488     val add_lazy_case_thms =
   489       fold Code.del_eqn_global case_thms
   490       #> Code.add_eqn_global (case_lazy_thm, true)
   491     val add_eager_case_thms = Code.del_eqn_global case_lazy_thm
   492       #> fold (Code.add_eqn_global o rpair true) case_thms
   493 
   494     val delay_dummy_thm = (pat_def_thm RS @{thm symmetric})
   495       |> Drule.infer_instantiate' lthy10
   496          [SOME (Thm.cterm_of lthy10 (Const (@{const_name "Pure.dummy_pattern"}, HOLogic.unitT --> lazy_type)))]
   497       |> Thm.generalize (map (fst o dest_TFree) type_args, []) (Variable.maxidx_of lthy10 + 1);
   498 
   499     val ctr_post = delay_dummy_thm :: map (fn thm => thm RS @{thm sym}) ctrs_lazy_thms
   500     val ctr_thms_abs = map (fn thm => Drule.abs_def (thm RS @{thm eq_reflection})) ctrs_lazy_thms
   501     val case_thm_abs = Drule.abs_def (case_lazy_thm RS @{thm eq_reflection})
   502     val add_simps = Code_Preproc.map_pre
   503       (fn ctxt => ctxt addsimps (case_thm_abs :: ctr_thms_abs))
   504     val del_simps = Code_Preproc.map_pre
   505       (fn ctxt => ctxt delsimps (case_thm_abs :: ctr_thms_abs))
   506     val add_post = Code_Preproc.map_post
   507       (fn ctxt => ctxt addsimps ctr_post)
   508     val del_post = Code_Preproc.map_post
   509       (fn ctxt => ctxt delsimps ctr_post)
   510   in
   511     Local_Theory.exit_global lthy10
   512     |> Laziness_Data.map (Symtab.update (type_name,
   513       {eagerT = eagerT, 
   514        lazyT = lazy_type,
   515        ctr = #const lazy_ctr_def,
   516        destr = #const lazy_sel_def,
   517        lazy_ctrs = map #const lazy_ctrs_def,
   518        case_lazy = #const lazy_case_def,
   519        active = true,
   520        activate = add_lazy_ctrs #> add_lazy_ctr_thms #> add_lazy_case_thms #> add_simps #> add_post,
   521        deactivate = add_eager_ctrs #> add_eager_case_thms #> del_simps #> del_post}))
   522     |> add_lazy_ctrs
   523     |> add_ctr_code (map (dest_Const o #const) lazy_ctrs_def) case_ctrs_thms
   524     |> add_code_eqs
   525     |> add_lazy_ctr_thms
   526     |> add_simps
   527     |> add_post
   528   end;
   529 
   530 fun transform_code_eqs _ [] = NONE
   531   | transform_code_eqs ctxt eqs =
   532     let
   533       val thy = Proof_Context.theory_of ctxt
   534       val table = Laziness_Data.get thy
   535       fun eliminate (s1, s2) = case Symtab.lookup table s1 of
   536           NONE => false
   537         | SOME x => #active x andalso s2 <> (#ctr x |> dest_Const |> fst)
   538       fun num_consts_fun (_, T) =
   539         let
   540           val s = body_type T |> dest_Type |> fst
   541         in
   542           if Symtab.defined table s
   543             then Ctr_Sugar.ctr_sugar_of ctxt s |> the |> #ctrs |> length
   544             else Code.get_type thy s |> fst |> snd |> length
   545         end
   546       val eqs = map (apfst (Thm.transfer thy)) eqs;
   547 
   548       val ((code_eqs, nbe_eqs), pure) =
   549         ((case hd eqs |> fst |> Thm.prop_of of
   550             Const (@{const_name Pure.eq}, _) $ _ $ _ =>
   551               (map (apfst (fn x => x RS @{thm meta_eq_to_obj_eq})) eqs, true)
   552          | _ => (eqs, false))
   553         |> apfst (List.partition snd))
   554         handle THM _ => (([], eqs), false)
   555       val to_original_eq = if pure then map (apfst (fn x => x RS @{thm eq_reflection})) else I
   556     in
   557       case Case_Converter.to_case ctxt eliminate num_consts_fun (map fst code_eqs) of
   558           NONE => NONE
   559         | SOME thms => SOME (nbe_eqs @ map (rpair true) thms |> to_original_eq)
   560     end handle THM ex => (Output.writeln (@{make_string} eqs); raise THM ex);
   561 
   562 val activate_lazy_type = set_active_lazy_type true;
   563 val deactivate_lazy_type = set_active_lazy_type false;
   564 val activate_lazy_types = set_active_lazy_types true;
   565 val deactivate_lazy_types = set_active_lazy_types false;
   566 
   567 fun get_lazy_types thy = Symtab.dest (Laziness_Data.get thy) 
   568 
   569 fun print_lazy_type thy (name, info : lazy_info) = 
   570   let
   571     val ctxt = Proof_Context.init_global thy
   572     fun pretty_ctr ctr = 
   573       let
   574         val argsT = dest_Const ctr |> snd |> binder_types
   575       in
   576         Pretty.block [
   577           Syntax.pretty_term ctxt ctr,
   578           Pretty.brk 1,
   579           Pretty.block (Pretty.separate "" (map (Pretty.quote o Syntax.pretty_typ ctxt) argsT))
   580         ]
   581       end
   582   in
   583     Pretty.block [
   584       Pretty.str (name ^ (if #active info then "" else " (inactive)") ^ ":"),
   585       Pretty.brk 1,
   586       Pretty.block [
   587         Syntax.pretty_typ ctxt (#eagerT info),
   588         Pretty.brk 1,
   589         Pretty.str "=",
   590         Pretty.brk 1,
   591         Syntax.pretty_term ctxt (#ctr info),
   592         Pretty.brk 1,
   593         Pretty.block [
   594           Pretty.str "(",
   595           Syntax.pretty_term ctxt (#destr info),
   596           Pretty.str ":",
   597           Pretty.brk 1,
   598           Syntax.pretty_typ ctxt (Type (@{type_name lazy}, [#lazyT info])),
   599           Pretty.str ")"
   600         ]
   601       ],
   602       Pretty.fbrk,
   603       Pretty.keyword2 "and",
   604       Pretty.brk 1,
   605       Pretty.block ([
   606         Syntax.pretty_typ ctxt (#lazyT info),
   607         Pretty.brk 1,
   608         Pretty.str "=",
   609         Pretty.brk 1] @
   610         Pretty.separate " |" (map pretty_ctr (#lazy_ctrs info)) @ [
   611         Pretty.fbrk,
   612         Pretty.keyword2 "for",
   613         Pretty.brk 1, 
   614         Pretty.str "case:",
   615         Pretty.brk 1,
   616         Syntax.pretty_term ctxt (#case_lazy info)
   617       ])
   618     ]
   619   end;
   620 
   621 fun print_lazy_types thy = 
   622   let
   623     fun cmp ((name1, _), (name2, _)) = string_ord (name1, name2)
   624     val infos = Laziness_Data.get thy |> Symtab.dest |> map (apfst Long_Name.base_name) |> sort cmp
   625   in
   626     Pretty.writeln_chunks (map (print_lazy_type thy) infos)
   627   end;
   628 
   629 
   630 val _ =
   631   Outer_Syntax.command @{command_keyword code_lazy_type}
   632     "make a lazy copy of the datatype and activate substitution"
   633     (Parse.binding >> (fn b => Toplevel.theory (Binding.name_of b |> code_lazy_type)));
   634 val _ =
   635   Outer_Syntax.command @{command_keyword activate_lazy_type}
   636     "activate substitution on a specific (lazy) type"
   637     (Parse.binding >> (fn b => Toplevel.theory (Binding.name_of b |> activate_lazy_type)));
   638 val _ =
   639   Outer_Syntax.command @{command_keyword deactivate_lazy_type}
   640     "deactivate substitution on a specific (lazy) type"
   641     (Parse.binding >> (fn b => Toplevel.theory (Binding.name_of b |> deactivate_lazy_type)));
   642 val _ =
   643   Outer_Syntax.command @{command_keyword activate_lazy_types}
   644     "activate substitution on all (lazy) types"
   645     (pair (Toplevel.theory activate_lazy_types));
   646 val _ =
   647   Outer_Syntax.command @{command_keyword deactivate_lazy_types}
   648     "deactivate substitution on all (lazy) type"
   649     (pair (Toplevel.theory deactivate_lazy_types));
   650 val _ =
   651   Outer_Syntax.command @{command_keyword print_lazy_types}
   652     "print the types that have been declared as lazy and their substitution state"
   653     (pair (Toplevel.theory (tap print_lazy_types)));
   654 
   655 end