new tool Code_Lazy
authorAndreas Lochbihler
Sat May 12 11:24:11 2018 +0200 (12 months ago)
changeset 681558b50f29a1992
parent 68154 42d63ea39161
child 68156 7da3af31ca4d
new tool Code_Lazy
src/HOL/Codegenerator_Test/Code_Lazy_Test.thy
src/HOL/Codegenerator_Test/Code_Test_GHC.thy
src/HOL/Codegenerator_Test/Code_Test_MLton.thy
src/HOL/Codegenerator_Test/Code_Test_OCaml.thy
src/HOL/Codegenerator_Test/Code_Test_PolyML.thy
src/HOL/Codegenerator_Test/Code_Test_SMLNJ.thy
src/HOL/Codegenerator_Test/Code_Test_Scala.thy
src/HOL/Library/Code_Lazy.thy
src/HOL/Library/Library.thy
src/HOL/Library/case_converter.ML
src/HOL/Library/code_lazy.ML
src/HOL/Library/document/root.bib
src/HOL/ROOT
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Codegenerator_Test/Code_Lazy_Test.thy	Sat May 12 11:24:11 2018 +0200
     1.3 @@ -0,0 +1,192 @@
     1.4 +(* Author: Andreas Lochbihler, Digital Asset *)
     1.5 +
     1.6 +section \<open>Laziness tests\<close>
     1.7 +
     1.8 +theory Code_Lazy_Test imports
     1.9 +  "HOL-Library.Code_Lazy"
    1.10 +  "HOL-Library.Stream" 
    1.11 +  "HOL-Library.Code_Test"
    1.12 +  "HOL-Library.BNF_Corec"
    1.13 +begin
    1.14 +
    1.15 +subsection \<open>Linear codatatype\<close>
    1.16 +
    1.17 +code_lazy_type stream
    1.18 +
    1.19 +value [code] "cycle ''ab''"
    1.20 +value [code] "let x = cycle ''ab''; y = snth x 10 in x"
    1.21 +
    1.22 +datatype 'a llist = LNil ("\<^bold>[\<^bold>]") | LCons (lhd: 'a) (ltl: "'a llist") (infixr "\<^bold>#" 65)
    1.23 +
    1.24 +subsection \<open>Finite lazy lists\<close>
    1.25 +
    1.26 +code_lazy_type llist
    1.27 +
    1.28 +no_notation lazy_llist ("_")
    1.29 +syntax "_llist" :: "args => 'a list"    ("\<^bold>[(_)\<^bold>]")
    1.30 +translations
    1.31 +  "\<^bold>[x, xs\<^bold>]" == "x\<^bold>#\<^bold>[xs\<^bold>]"
    1.32 +  "\<^bold>[x\<^bold>]" == "x\<^bold>#\<^bold>[\<^bold>]"
    1.33 +  "\<^bold>[x\<^bold>]" == "CONST lazy_llist x"
    1.34 +
    1.35 +definition llist :: "nat llist" where
    1.36 +  "llist = \<^bold>[1, 2, 3, hd [], 4\<^bold>]"
    1.37 +
    1.38 +fun lnth :: "nat \<Rightarrow> 'a llist \<Rightarrow> 'a" where
    1.39 +  "lnth 0 (x \<^bold># xs) = x"
    1.40 +| "lnth (Suc n) (x \<^bold># xs) = lnth n xs"
    1.41 +
    1.42 +value [code] "llist"
    1.43 +value [code] "let x = lnth 2 llist in (x, llist)"
    1.44 +value [code] "llist"
    1.45 +
    1.46 +fun lfilter :: "('a \<Rightarrow> bool) \<Rightarrow> 'a llist \<Rightarrow> 'a llist" where
    1.47 +  "lfilter P \<^bold>[\<^bold>] = \<^bold>[\<^bold>]"
    1.48 +| "lfilter P (x \<^bold># xs) = (if P x then x \<^bold># lfilter P xs else lfilter P xs)"
    1.49 +
    1.50 +value [code] "lhd (lfilter odd llist)"
    1.51 +
    1.52 +definition lfilter_test :: "nat llist \<Rightarrow> _" where "lfilter_test xs = lhd (lfilter even xs)"
    1.53 +  \<comment> \<open>Filtering @{term llist} for @{term even} fails because only the datatype is lazy, not the
    1.54 +  filter function itself.\<close>
    1.55 +ML_val \<open> (@{code lfilter_test} @{code llist}; raise Fail "Failure expected") handle Match => () \<close>
    1.56 +
    1.57 +subsection \<open>Records as free type\<close>
    1.58 +
    1.59 +record ('a, 'b) rec = 
    1.60 +  rec1 :: 'a
    1.61 +  rec2 :: 'b
    1.62 +
    1.63 +free_constructors rec_ext for rec.rec_ext
    1.64 +  subgoal by(rule rec.cases_scheme)
    1.65 +  subgoal by(rule rec.ext_inject)
    1.66 +  done
    1.67 +
    1.68 +code_lazy_type rec_ext
    1.69 +
    1.70 +definition rec_test1 where "rec_test1 = rec1 (\<lparr>rec1 = Suc 5, rec2 = True\<rparr>\<lparr>rec1 := 0\<rparr>)"
    1.71 +definition rec_test2 :: "(bool, bool) rec" where "rec_test2 = \<lparr>rec1 = hd [], rec2 = True\<rparr>"
    1.72 +test_code "rec_test1 = 0" in PolyML Scala
    1.73 +value [code] "rec_test2"
    1.74 +
    1.75 +subsection \<open>Branching codatatypes\<close>
    1.76 +
    1.77 +codatatype tree = L | Node tree tree (infix "\<triangle>" 900)
    1.78 +
    1.79 +code_lazy_type tree
    1.80 +
    1.81 +fun mk_tree :: "nat \<Rightarrow> tree" where
    1.82 +  mk_tree_0: "mk_tree 0 = L"
    1.83 +|            "mk_tree (Suc n) = (let t = mk_tree n in t \<triangle> t)"
    1.84 +
    1.85 +function subtree :: "bool list \<Rightarrow> tree \<Rightarrow> tree" where
    1.86 +  "subtree [] t = t"
    1.87 +| "subtree (True # p) (l \<triangle> r) = subtree p l"
    1.88 +| "subtree (False # p) (l \<triangle> r) = subtree p r"
    1.89 +| "subtree _ L = L"
    1.90 +  by pat_completeness auto
    1.91 +termination by lexicographic_order
    1.92 +
    1.93 +value [code] "mk_tree 10"
    1.94 +value [code] "let t = mk_tree 10; _ = subtree [True, True, False, False] t in t"
    1.95 +
    1.96 +lemma mk_tree_Suc: "mk_tree (Suc n) = mk_tree n \<triangle> mk_tree n"
    1.97 +  by(simp add: Let_def)
    1.98 +lemmas [code] = mk_tree_0 mk_tree_Suc
    1.99 +value [code] "let t = mk_tree 10; _ = subtree [True, True, False, False] t in t"
   1.100 +value [code] "let t = mk_tree 4; _ = subtree [True, True, False, False] t in t"
   1.101 +
   1.102 +subsection \<open>Corecursion\<close>
   1.103 +
   1.104 +corec (friend) plus :: "'a :: plus stream \<Rightarrow> 'a stream \<Rightarrow> 'a stream" where
   1.105 +  "plus xs ys = (shd xs + shd ys) ## plus (stl xs) (stl ys)"
   1.106 +
   1.107 +corec (friend) times :: "'a :: {plus, times} stream \<Rightarrow> 'a stream \<Rightarrow> 'a stream" where
   1.108 +  "times xs ys = (shd xs * shd ys) ## plus (times (stl xs) ys) (times xs (stl ys))"
   1.109 +
   1.110 +subsection \<open>Pattern-matching tests\<close>
   1.111 +
   1.112 +definition f1 :: "bool \<Rightarrow> bool \<Rightarrow> bool \<Rightarrow> nat llist \<Rightarrow> unit" where
   1.113 +  "f1 _ _ _ _ = ()"
   1.114 +
   1.115 +declare [[code drop: f1]]
   1.116 +lemma f1_code1 [code]: 
   1.117 +  "f1 b c d    ns     = Code.abort (STR ''4'') (\<lambda>_. ())" 
   1.118 +  "f1 b c True \<^bold>[n, m\<^bold>] = Code.abort (STR ''3'') (\<lambda>_. ())" 
   1.119 +  "f1 b True d \<^bold>[n\<^bold>]    = Code.abort (STR ''2'') (\<lambda>_. ())" 
   1.120 +  "f1 True c d \<^bold>[\<^bold>]     = ()"
   1.121 +  by(simp_all add: f1_def)
   1.122 +
   1.123 +value [code] "f1 True False False \<^bold>[\<^bold>]"
   1.124 +deactivate_lazy_type llist
   1.125 +value [code] "f1 True False False \<^bold>[\<^bold>]"
   1.126 +declare f1_code1(1) [code del]
   1.127 +value [code] "f1 True False False \<^bold>[\<^bold>]"
   1.128 +activate_lazy_type llist
   1.129 +value [code] "f1 True False False \<^bold>[\<^bold>]"
   1.130 +
   1.131 +declare [[code drop: f1]]
   1.132 +lemma f1_code2 [code]: 
   1.133 +  "f1 b c d    ns     = Code.abort (STR ''4'') (\<lambda>_. ())" 
   1.134 +  "f1 b c True \<^bold>[n, m\<^bold>] = Code.abort (STR ''3'') (\<lambda>_. ())" 
   1.135 +  "f1 b True d \<^bold>[n\<^bold>]    = ()"
   1.136 +  "f1 True c d \<^bold>[\<^bold>]     = Code.abort (STR ''1'') (\<lambda>_. ())"
   1.137 +  by(simp_all add: f1_def)
   1.138 +
   1.139 +value [code] "f1 True True True \<^bold>[0\<^bold>]"
   1.140 +declare f1_code2(1)[code del]
   1.141 +value [code] "f1 True True True \<^bold>[0\<^bold>]"
   1.142 +
   1.143 +declare [[code drop: f1]]
   1.144 +lemma f1_code3 [code]:
   1.145 +  "f1 b c d    ns     = Code.abort (STR ''4'') (\<lambda>_. ())"
   1.146 +  "f1 b c True \<^bold>[n, m\<^bold>] = ()" 
   1.147 +  "f1 b True d \<^bold>[n\<^bold>]    = Code.abort (STR ''2'') (\<lambda>_. ())"
   1.148 +  "f1 True c d \<^bold>[\<^bold>]     = Code.abort (STR ''1'') (\<lambda>_. ())"
   1.149 +  by(simp_all add: f1_def)
   1.150 +
   1.151 +value [code] "f1 True True True \<^bold>[0, 1\<^bold>]"
   1.152 +declare f1_code3(1)[code del]
   1.153 +value [code] "f1 True True True \<^bold>[0, 1\<^bold>]"
   1.154 +
   1.155 +declare [[code drop: f1]]
   1.156 +lemma f1_code4 [code]:
   1.157 +  "f1 b c d    ns     = ()" 
   1.158 +  "f1 b c True \<^bold>[n, m\<^bold>] = Code.abort (STR ''3'') (\<lambda>_. ())"
   1.159 +  "f1 b True d \<^bold>[n\<^bold>]    = Code.abort (STR ''2'') (\<lambda>_. ())" 
   1.160 +  "f1 True c d \<^bold>[\<^bold>]     = Code.abort (STR ''1'') (\<lambda>_. ())"
   1.161 +  by(simp_all add: f1_def)
   1.162 +
   1.163 +value [code] "f1 True True True \<^bold>[0, 1, 2\<^bold>]"
   1.164 +value [code] "f1 True True False \<^bold>[0, 1\<^bold>]"
   1.165 +value [code] "f1 True False True \<^bold>[0\<^bold>]"
   1.166 +value [code] "f1 False True True \<^bold>[\<^bold>]"
   1.167 +
   1.168 +definition f2 :: "nat llist llist list \<Rightarrow> unit" where "f2 _ = ()"
   1.169 +
   1.170 +declare [[code drop: f2]]
   1.171 +lemma f2_code1 [code]:
   1.172 +  "f2 xs = Code.abort (STR ''a'') (\<lambda>_. ())"
   1.173 +  "f2 [\<^bold>[\<^bold>[\<^bold>]\<^bold>]] = ()"
   1.174 +  "f2 [\<^bold>[\<^bold>[Suc n\<^bold>]\<^bold>]] = ()"
   1.175 +  "f2 [\<^bold>[\<^bold>[0, Suc n\<^bold>]\<^bold>]] = ()"
   1.176 +  by(simp_all add: f2_def)
   1.177 +
   1.178 +value [code] "f2 [\<^bold>[\<^bold>[\<^bold>]\<^bold>]]"
   1.179 +value [code] "f2 [\<^bold>[\<^bold>[4\<^bold>]\<^bold>]]"
   1.180 +value [code] "f2 [\<^bold>[\<^bold>[0, 1\<^bold>]\<^bold>]]"
   1.181 +ML_val \<open> (@{code f2} []; error "Fail expected") handle Fail _ => () \<close>
   1.182 +
   1.183 +definition f3 :: "nat set llist \<Rightarrow> unit" where "f3 _ = ()"
   1.184 +
   1.185 +declare [[code drop: f3]]
   1.186 +lemma f3_code1 [code]:
   1.187 +  "f3 \<^bold>[\<^bold>] = ()"
   1.188 +  "f3 \<^bold>[A\<^bold>] = ()"
   1.189 +  by(simp_all add: f3_def)
   1.190 +
   1.191 +value [code] "f3 \<^bold>[\<^bold>]"
   1.192 +value [code] "f3 \<^bold>[{}\<^bold>]"
   1.193 +value [code] "f3 \<^bold>[UNIV\<^bold>]"
   1.194 +
   1.195 +end
   1.196 \ No newline at end of file
     2.1 --- a/src/HOL/Codegenerator_Test/Code_Test_GHC.thy	Fri May 11 22:59:00 2018 +0200
     2.2 +++ b/src/HOL/Codegenerator_Test/Code_Test_GHC.thy	Sat May 12 11:24:11 2018 +0200
     2.3 @@ -4,7 +4,7 @@
     2.4  Test case for test_code on GHC
     2.5  *)
     2.6  
     2.7 -theory Code_Test_GHC imports "HOL-Library.Code_Test" begin
     2.8 +theory Code_Test_GHC imports "HOL-Library.Code_Test" Code_Lazy_Test begin
     2.9  
    2.10  test_code "(14 + 7 * -12 :: integer) = 140 div -2" in GHC
    2.11  
    2.12 @@ -20,4 +20,6 @@
    2.13    "gcd 0 0 = (0 :: integer)"
    2.14  in GHC
    2.15  
    2.16 +test_code "stake 10 (cycle ''ab'') = ''ababababab''" in GHC
    2.17 +
    2.18  end
     3.1 --- a/src/HOL/Codegenerator_Test/Code_Test_MLton.thy	Fri May 11 22:59:00 2018 +0200
     3.2 +++ b/src/HOL/Codegenerator_Test/Code_Test_MLton.thy	Sat May 12 11:24:11 2018 +0200
     3.3 @@ -4,10 +4,12 @@
     3.4  Test case for test_code on MLton
     3.5  *)
     3.6  
     3.7 -theory Code_Test_MLton imports  "HOL-Library.Code_Test" begin
     3.8 +theory Code_Test_MLton imports  "HOL-Library.Code_Test" Code_Lazy_Test begin
     3.9  
    3.10  test_code "14 + 7 * -12 = (140 div -2 :: integer)" in MLton
    3.11  
    3.12  value [MLton] "14 + 7 * -12 :: integer"
    3.13  
    3.14 +test_code "stake 10 (cycle ''ab'') = ''ababababab''" in MLton
    3.15 +
    3.16  end
     4.1 --- a/src/HOL/Codegenerator_Test/Code_Test_OCaml.thy	Fri May 11 22:59:00 2018 +0200
     4.2 +++ b/src/HOL/Codegenerator_Test/Code_Test_OCaml.thy	Sat May 12 11:24:11 2018 +0200
     4.3 @@ -4,7 +4,7 @@
     4.4  Test case for test_code on OCaml
     4.5  *)
     4.6  
     4.7 -theory Code_Test_OCaml imports  "HOL-Library.Code_Test" begin
     4.8 +theory Code_Test_OCaml imports  "HOL-Library.Code_Test" Code_Lazy_Test begin
     4.9  
    4.10  test_code "14 + 7 * -12 = (140 div -2 :: integer)" in OCaml
    4.11  
    4.12 @@ -20,4 +20,6 @@
    4.13    "gcd 0 0 = (0 :: integer)"
    4.14  in OCaml
    4.15  
    4.16 +test_code "stake 10 (cycle ''ab'') = ''ababababab''" in OCaml
    4.17 +
    4.18  end
     5.1 --- a/src/HOL/Codegenerator_Test/Code_Test_PolyML.thy	Fri May 11 22:59:00 2018 +0200
     5.2 +++ b/src/HOL/Codegenerator_Test/Code_Test_PolyML.thy	Sat May 12 11:24:11 2018 +0200
     5.3 @@ -4,10 +4,12 @@
     5.4  Test case for test_code on PolyML
     5.5  *)
     5.6  
     5.7 -theory Code_Test_PolyML imports  "HOL-Library.Code_Test" begin
     5.8 +theory Code_Test_PolyML imports  "HOL-Library.Code_Test" Code_Lazy_Test begin
     5.9  
    5.10  test_code "14 + 7 * -12 = (140 div -2 :: integer)" in PolyML
    5.11  
    5.12  value [PolyML] "14 + 7 * -12 :: integer"
    5.13  
    5.14 +test_code "stake 10 (cycle ''ab'') = ''ababababab''" in PolyML
    5.15 +
    5.16  end
     6.1 --- a/src/HOL/Codegenerator_Test/Code_Test_SMLNJ.thy	Fri May 11 22:59:00 2018 +0200
     6.2 +++ b/src/HOL/Codegenerator_Test/Code_Test_SMLNJ.thy	Sat May 12 11:24:11 2018 +0200
     6.3 @@ -4,10 +4,12 @@
     6.4  Test case for test_code on SMLNJ
     6.5  *)
     6.6  
     6.7 -theory Code_Test_SMLNJ imports  "HOL-Library.Code_Test" begin
     6.8 +theory Code_Test_SMLNJ imports  "HOL-Library.Code_Test" Code_Lazy_Test begin
     6.9  
    6.10  test_code "14 + 7 * -12 = (140 div -2 :: integer)" in SMLNJ
    6.11  
    6.12  value [SMLNJ] "14 + 7 * -12 :: integer"
    6.13  
    6.14 +test_code "stake 10 (cycle ''ab'') = ''ababababab''" in SMLNJ
    6.15 +
    6.16  end
     7.1 --- a/src/HOL/Codegenerator_Test/Code_Test_Scala.thy	Fri May 11 22:59:00 2018 +0200
     7.2 +++ b/src/HOL/Codegenerator_Test/Code_Test_Scala.thy	Sat May 12 11:24:11 2018 +0200
     7.3 @@ -4,7 +4,7 @@
     7.4  Test case for test_code on Scala
     7.5  *)
     7.6  
     7.7 -theory Code_Test_Scala imports  "HOL-Library.Code_Test" begin
     7.8 +theory Code_Test_Scala imports  "HOL-Library.Code_Test" Code_Lazy_Test begin
     7.9  
    7.10  test_code "14 + 7 * -12 = (140 div -2 :: integer)" in Scala
    7.11  
    7.12 @@ -20,4 +20,6 @@
    7.13    "gcd 0 0 = (0 :: integer)"
    7.14  in Scala
    7.15  
    7.16 +test_code "stake 10 (cycle ''ab'') = ''ababababab''" in Scala
    7.17 +
    7.18  end
     8.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     8.2 +++ b/src/HOL/Library/Code_Lazy.thy	Sat May 12 11:24:11 2018 +0200
     8.3 @@ -0,0 +1,251 @@
     8.4 +(* Author: Pascal Stoop, ETH Zurich
     8.5 +   Author: Andreas Lochbihler, Digital Asset *)
     8.6 +
     8.7 +section \<open>Lazy types in generated code\<close>
     8.8 +
     8.9 +theory Code_Lazy
    8.10 +imports Main
    8.11 +keywords
    8.12 +  "code_lazy_type"
    8.13 +  "activate_lazy_type"
    8.14 +  "deactivate_lazy_type"
    8.15 +  "activate_lazy_types"
    8.16 +  "deactivate_lazy_types"
    8.17 +  "print_lazy_types" :: thy_decl
    8.18 +begin
    8.19 +
    8.20 +text \<open>
    8.21 +  This theory and the CodeLazy tool described in @{cite "LochbihlerStoop2018"}.
    8.22 +
    8.23 +  It hooks into Isabelle’s code generator such that the generated code evaluates a user-specified
    8.24 +  set of type constructors lazily, even in target languages with eager evaluation.
    8.25 +  The lazy type must be algebraic, i.e., values must be built from constructors and a
    8.26 +  corresponding case operator decomposes them. Every datatype and codatatype is algebraic
    8.27 +  and thus eligible for lazification.
    8.28 +\<close>
    8.29 +
    8.30 +subsection \<open>Eliminating pattern matches\<close>
    8.31 +
    8.32 +definition missing_pattern_match :: "String.literal \<Rightarrow> (unit \<Rightarrow> 'a) \<Rightarrow> 'a" where
    8.33 +  [code del]: "missing_pattern_match m f = f ()"
    8.34 +
    8.35 +lemma missing_pattern_match_cong [cong]:
    8.36 +  "m = m' \<Longrightarrow> missing_pattern_match m f = missing_pattern_match m' f"
    8.37 +  by(rule arg_cong)
    8.38 +
    8.39 +lemma missing_pattern_match_code [code_unfold]:
    8.40 +  "missing_pattern_match = Code.abort"
    8.41 +  unfolding missing_pattern_match_def Code.abort_def ..
    8.42 +
    8.43 +ML_file "case_converter.ML"
    8.44 +
    8.45 +subsection \<open>The type @{text lazy}\<close>
    8.46 +
    8.47 +typedef 'a lazy = "UNIV :: 'a set" ..
    8.48 +setup_lifting type_definition_lazy
    8.49 +lift_definition delay :: "(unit \<Rightarrow> 'a) \<Rightarrow> 'a lazy"  is "\<lambda>f. f ()" .
    8.50 +lift_definition force :: "'a lazy \<Rightarrow> 'a" is "\<lambda>x. x" .
    8.51 +
    8.52 +code_datatype delay
    8.53 +lemma force_delay [code]: "force (delay f) = f ()" by transfer(rule refl)
    8.54 +lemma delay_force: "delay (\<lambda>_. force s) = s" by transfer(rule refl)
    8.55 +
    8.56 +text \<open>The implementations of @{typ "_ lazy"} using language primitives cache forced values.\<close>
    8.57 +
    8.58 +code_printing code_module Lazy \<rightharpoonup> (SML)
    8.59 +\<open>signature LAZY =
    8.60 +sig
    8.61 +  type 'a lazy;
    8.62 +  val lazy : (unit -> 'a) -> 'a lazy;
    8.63 +  val force : 'a lazy -> 'a;
    8.64 +  val peek : 'a lazy -> 'a option
    8.65 +  val termify_lazy : 
    8.66 +   (string -> 'typerep -> 'term) -> 
    8.67 +   ('term -> 'term -> 'term) -> 
    8.68 +   (string -> 'typerep -> 'term -> 'term) ->
    8.69 +   'typerep -> ('typerep -> 'typerep -> 'typerep) -> ('typerep -> 'typerep) ->
    8.70 +   ('a -> 'term) -> 'typerep -> 'a lazy -> 'term -> 'term;
    8.71 +end;
    8.72 +
    8.73 +structure Lazy : LAZY = 
    8.74 +struct
    8.75 +
    8.76 +datatype 'a content =
    8.77 +   Delay of unit -> 'a
    8.78 + | Value of 'a 
    8.79 + | Exn of exn;
    8.80 +
    8.81 +datatype 'a lazy = Lazy of 'a content ref;
    8.82 +
    8.83 +fun lazy f = Lazy (ref (Delay f));
    8.84 +
    8.85 +fun force (Lazy x) = case !x of
    8.86 +   Delay f => (
    8.87 +     let val res = f (); val _ = x := Value res; in res end
    8.88 +     handle exn => (x := Exn exn; raise exn))
    8.89 +  | Value x => x
    8.90 +  | Exn exn => raise exn;
    8.91 +
    8.92 +fun peek (Lazy x) = case !x of
    8.93 +    Value x => SOME x
    8.94 +  | _ => NONE;
    8.95 +
    8.96 +fun termify_lazy const app abs unitT funT lazyT term_of T x _ =
    8.97 +  app (const "Code_Lazy.delay" (funT (funT unitT T) (lazyT T))) 
    8.98 +    (case peek x of SOME y => abs "_" unitT (term_of y)
    8.99 +     | _ => const "Pure.dummy_pattern" (funT unitT T));
   8.100 +
   8.101 +end;\<close>
   8.102 +code_reserved SML Lazy
   8.103 +
   8.104 +code_printing
   8.105 +  type_constructor lazy \<rightharpoonup> (SML) "_ Lazy.lazy"
   8.106 +| constant delay \<rightharpoonup> (SML) "Lazy.lazy"
   8.107 +| constant force \<rightharpoonup> (SML) "Lazy.force"
   8.108 +
   8.109 +code_printing \<comment> \<open>For code generation within the Isabelle environment, we reuse the thread-safe
   8.110 +  implementation of lazy from @{file "~~/src/Pure/Concurrent/lazy.ML"}\<close>
   8.111 +  code_module Lazy \<rightharpoonup> (Eval) \<open>\<close>
   8.112 +| type_constructor lazy \<rightharpoonup> (Eval) "_ Lazy.lazy"
   8.113 +| constant delay \<rightharpoonup> (Eval) "Lazy.lazy"
   8.114 +| constant force \<rightharpoonup> (Eval) "Lazy.force"
   8.115 +
   8.116 +code_printing
   8.117 +  code_module Lazy \<rightharpoonup> (Haskell) 
   8.118 +\<open>newtype Lazy a = Lazy a;
   8.119 +delay f = Lazy (f ());
   8.120 +force (Lazy x) = x;\<close>
   8.121 +| type_constructor lazy \<rightharpoonup> (Haskell) "Lazy.Lazy _"
   8.122 +| constant delay \<rightharpoonup> (Haskell) "Lazy.delay"
   8.123 +| constant force \<rightharpoonup> (Haskell) "Lazy.force"
   8.124 +code_reserved Haskell Lazy
   8.125 +
   8.126 +code_printing
   8.127 +  code_module Lazy \<rightharpoonup> (Scala) 
   8.128 +\<open>object Lazy {
   8.129 +  final class Lazy[A] (f: Unit => A) {
   8.130 +    var evaluated = false;
   8.131 +    lazy val x: A = f ()
   8.132 +
   8.133 +    def get() : A = {
   8.134 +      evaluated = true;
   8.135 +      return x
   8.136 +    }
   8.137 +  }
   8.138 +
   8.139 +  def force[A] (x: Lazy[A]) : A = {
   8.140 +    return x.get()
   8.141 +  }
   8.142 +
   8.143 +  def delay[A] (f: Unit => A) : Lazy[A] = {
   8.144 +    return new Lazy[A] (f)
   8.145 +  }
   8.146 +
   8.147 +  def termify_lazy[Typerep, Term, A] (
   8.148 +    const: String => Typerep => Term,
   8.149 +    app: Term => Term => Term,
   8.150 +    abs: String => Typerep => Term => Term,
   8.151 +    unitT: Typerep,
   8.152 +    funT: Typerep => Typerep => Typerep,
   8.153 +    lazyT: Typerep => Typerep,
   8.154 +    term_of: A => Term,
   8.155 +    ty: Typerep,
   8.156 +    x: Lazy[A],
   8.157 +    dummy: Term) : Term = {
   8.158 +    if (x.evaluated)
   8.159 +      app(const("Code_Lazy.delay")(funT(funT(unitT)(ty))(lazyT(ty))))(abs("_")(unitT)(term_of(x.get)))
   8.160 +    else
   8.161 +      app(const("Code_Lazy.delay")(funT(funT(unitT)(ty))(lazyT(ty))))(const("Pure.dummy_pattern")(funT(unitT)(ty)))
   8.162 +  }
   8.163 +}\<close>
   8.164 +| type_constructor lazy \<rightharpoonup> (Scala) "Lazy.Lazy[_]"
   8.165 +| constant delay \<rightharpoonup> (Scala) "Lazy.delay"
   8.166 +| constant force \<rightharpoonup> (Scala) "Lazy.force"
   8.167 +code_reserved Scala Lazy termify_lazy
   8.168 +
   8.169 +code_printing
   8.170 +  type_constructor lazy \<rightharpoonup> (OCaml) "_ Lazy.t"
   8.171 +| constant delay \<rightharpoonup> (OCaml) "Lazy.from'_fun"
   8.172 +| constant force \<rightharpoonup> (OCaml) "Lazy.force"
   8.173 +code_reserved OCaml Lazy
   8.174 +
   8.175 +text \<open>
   8.176 +  Term reconstruction for lazy looks into the lazy value and reconstructs it to the depth it has been evaluated.
   8.177 +  This is not done for Haskell and Scala as we do not know of any portable way to inspect whether a lazy value
   8.178 +  has been evaluated to or not.
   8.179 +\<close>
   8.180 +code_printing code_module Termify_Lazy \<rightharpoonup> (Eval) 
   8.181 +\<open>structure Termify_Lazy = struct
   8.182 +fun termify_lazy 
   8.183 +  (_: string -> typ -> term) (_: term -> term -> term)  (_: string -> typ -> term -> term)
   8.184 +  (_: typ) (_: typ -> typ -> typ) (_: typ -> typ)
   8.185 +  (term_of: 'a -> term) (T: typ) (x: 'a Lazy.lazy) (_: term) =
   8.186 +  Const ("Code_Lazy.delay", (HOLogic.unitT --> T) --> Type ("Code_Lazy.lazy", [T])) $ 
   8.187 +  (case Lazy.peek x of
   8.188 +    SOME (Exn.Res x) => absdummy HOLogic.unitT (term_of x)
   8.189 +  | _ => Const ("Pure.dummy_pattern", HOLogic.unitT --> T));
   8.190 +end;\<close>
   8.191 +code_reserved Eval Termify_Lazy TERMIFY_LAZY termify_lazy
   8.192 +
   8.193 +code_printing code_module Termify_Lazy \<rightharpoonup> (OCaml) 
   8.194 +\<open>module Termify_Lazy : sig
   8.195 +  val termify_lazy :
   8.196 +   (string -> 'typerep -> 'term) -> 
   8.197 +   ('term -> 'term -> 'term) -> 
   8.198 +   (string -> 'typerep -> 'term -> 'term) ->
   8.199 +   'typerep -> ('typerep -> 'typerep -> 'typerep) -> ('typerep -> 'typerep) ->
   8.200 +   ('a -> 'term) -> 'typerep -> 'a Lazy.t -> 'term -> 'term
   8.201 +end = struct
   8.202 +
   8.203 +let termify_lazy const app abs unitT funT lazyT term_of ty x _ =
   8.204 +  app (const "Code_Lazy.delay" (funT (funT unitT ty) (lazyT ty))) 
   8.205 +    (if Lazy.is_val x then abs "_" unitT (term_of (Lazy.force x))
   8.206 +     else const "Pure.dummy_pattern" (funT unitT ty));;
   8.207 +
   8.208 +end;;\<close>
   8.209 +code_reserved OCaml Termify_Lazy termify_lazy
   8.210 +
   8.211 +definition termify_lazy2 :: "'a :: typerep lazy \<Rightarrow> term"
   8.212 +where "termify_lazy2 x =
   8.213 +  Code_Evaluation.App (Code_Evaluation.Const (STR ''Code_Lazy.delay'') (TYPEREP((unit \<Rightarrow> 'a) \<Rightarrow> 'a lazy)))
   8.214 +    (Code_Evaluation.Const (STR ''Pure.dummy_pattern'') (TYPEREP((unit \<Rightarrow> 'a))))"
   8.215 +
   8.216 +definition termify_lazy :: 
   8.217 +  "(String.literal \<Rightarrow> 'typerep \<Rightarrow> 'term) \<Rightarrow> 
   8.218 +   ('term \<Rightarrow> 'term \<Rightarrow> 'term) \<Rightarrow> 
   8.219 +   (String.literal \<Rightarrow> 'typerep \<Rightarrow> 'term \<Rightarrow> 'term) \<Rightarrow>
   8.220 +   'typerep \<Rightarrow> ('typerep \<Rightarrow> 'typerep \<Rightarrow> 'typerep) \<Rightarrow> ('typerep \<Rightarrow> 'typerep) \<Rightarrow>
   8.221 +   ('a \<Rightarrow> 'term) \<Rightarrow> 'typerep \<Rightarrow> 'a :: typerep lazy \<Rightarrow> 'term \<Rightarrow> term"
   8.222 +where "termify_lazy _ _ _ _ _ _ _ _ x _ = termify_lazy2 x"
   8.223 +
   8.224 +declare [[code drop: "Code_Evaluation.term_of :: _ lazy \<Rightarrow> _"]]
   8.225 +
   8.226 +lemma term_of_lazy_code [code]:
   8.227 +  "Code_Evaluation.term_of x \<equiv> 
   8.228 +   termify_lazy 
   8.229 +     Code_Evaluation.Const Code_Evaluation.App Code_Evaluation.Abs 
   8.230 +     TYPEREP(unit) (\<lambda>T U. typerep.Typerep (STR ''fun'') [T, U]) (\<lambda>T. typerep.Typerep (STR ''Code_Lazy.lazy'') [T])
   8.231 +     Code_Evaluation.term_of TYPEREP('a) x (Code_Evaluation.Const (STR '''') (TYPEREP(unit)))"
   8.232 +  for x :: "'a :: {typerep, term_of} lazy"
   8.233 +by(rule term_of_anything)
   8.234 +
   8.235 +code_printing constant termify_lazy
   8.236 +  \<rightharpoonup> (SML) "Lazy.termify'_lazy" 
   8.237 +  and (Eval) "Termify'_Lazy.termify'_lazy"
   8.238 +  and (OCaml) "Termify'_Lazy.termify'_lazy"
   8.239 +  and (Scala) "Lazy.termify'_lazy"
   8.240 +  
   8.241 +text \<open>Make evaluation with the simplifier respect @{term delay}s.\<close>
   8.242 +
   8.243 +lemma delay_lazy_cong: "delay f = delay f" by simp
   8.244 +setup \<open>Code_Simp.map_ss (Simplifier.add_cong @{thm delay_lazy_cong})\<close>        
   8.245 +
   8.246 +subsection \<open>Implementation\<close>
   8.247 +
   8.248 +ML_file "code_lazy.ML"
   8.249 +
   8.250 +setup \<open>
   8.251 +  Code_Preproc.add_functrans ("lazy_datatype", Code_Lazy.transform_code_eqs);
   8.252 +\<close>
   8.253 +
   8.254 +end
     9.1 --- a/src/HOL/Library/Library.thy	Fri May 11 22:59:00 2018 +0200
     9.2 +++ b/src/HOL/Library/Library.thy	Sat May 12 11:24:11 2018 +0200
     9.3 @@ -10,6 +10,7 @@
     9.4    Boolean_Algebra
     9.5    Bourbaki_Witt_Fixpoint
     9.6    Char_ord
     9.7 +  Code_Lazy
     9.8    Code_Test
     9.9    Combine_PER
    9.10    Complete_Partial_Order2
    10.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    10.2 +++ b/src/HOL/Library/case_converter.ML	Sat May 12 11:24:11 2018 +0200
    10.3 @@ -0,0 +1,549 @@
    10.4 +(* Author: Pascal Stoop, ETH Zurich
    10.5 +   Author: Andreas Lochbihler, Digital Asset *)
    10.6 +
    10.7 +signature CASE_CONVERTER =
    10.8 +sig
    10.9 +  val to_case: Proof.context -> (string * string -> bool) -> (string * typ -> int) ->
   10.10 +    thm list -> thm list option
   10.11 +end;
   10.12 +
   10.13 +structure Case_Converter : CASE_CONVERTER =
   10.14 +struct
   10.15 +
   10.16 +fun lookup_remove _ _ [] = (NONE, [])
   10.17 +  | lookup_remove eq k ((k', v) :: kvs) =
   10.18 +    if eq (k, k') then (SOME (k', v), kvs)
   10.19 +    else apsnd (cons (k', v)) (lookup_remove eq k kvs)
   10.20 +
   10.21 +fun map_option _ NONE = NONE
   10.22 +  | map_option f (SOME x) = SOME (f x)
   10.23 +
   10.24 +fun mk_abort msg t =
   10.25 +  let 
   10.26 +    val T = fastype_of t
   10.27 +    val abort = Const (@{const_name missing_pattern_match}, HOLogic.literalT --> (HOLogic.unitT --> T) --> T)
   10.28 +  in
   10.29 +    abort $ HOLogic.mk_literal msg $ absdummy HOLogic.unitT t
   10.30 +  end
   10.31 +
   10.32 +(* fold_term : (string * typ -> 'a) ->
   10.33 +               (string * typ -> 'a) ->
   10.34 +               (indexname * typ -> 'a) ->
   10.35 +               (int -> 'a) ->
   10.36 +               (string * typ * 'a -> 'a) ->
   10.37 +               ('a * 'a -> 'a) ->
   10.38 +               term ->
   10.39 +               'a *)
   10.40 +fun fold_term const_fun free_fun var_fun bound_fun abs_fun dollar_fun term =
   10.41 +  let
   10.42 +    fun go x = case x of
   10.43 +      Const (s, T) => const_fun (s, T)
   10.44 +      | Free (s, T) => free_fun (s, T)
   10.45 +      | Var (i, T) => var_fun (i, T)
   10.46 +      | Bound n => bound_fun n
   10.47 +      | Abs (s, T, term) => abs_fun (s, T, go term)
   10.48 +      | term1 $ term2 => dollar_fun (go term1, go term2)
   10.49 +  in
   10.50 +    go term
   10.51 +  end;
   10.52 +
   10.53 +datatype term_coordinate = End of typ
   10.54 +  | Coordinate of (string * (int * term_coordinate)) list;
   10.55 +
   10.56 +fun term_coordinate_merge (End T) _ = End T
   10.57 +  | term_coordinate_merge _ (End T) = End T
   10.58 +  | term_coordinate_merge (Coordinate xs) (Coordinate ys) =
   10.59 +  let
   10.60 +    fun merge_consts xs [] = xs
   10.61 +      | merge_consts xs ((s1, (n, y)) :: ys) = 
   10.62 +        case List.partition (fn (s2, (m, _)) => s1 = s2 andalso n = m) xs of
   10.63 +            ([], xs') => (s1, (n, y)) :: (merge_consts xs' ys)
   10.64 +          | ((_, (_, x)) :: _, xs') => (s1, (n, term_coordinate_merge x y)) :: (merge_consts xs' ys)
   10.65 +  in
   10.66 +    Coordinate (merge_consts xs ys)
   10.67 +  end;
   10.68 +
   10.69 +fun term_to_coordinates P term = 
   10.70 +  let
   10.71 +    val (ctr, args) = strip_comb term
   10.72 +  in
   10.73 +    case ctr of Const (s, T) =>
   10.74 +      if P (body_type T |> dest_Type |> fst, s)
   10.75 +      then SOME (End (body_type T))
   10.76 +      else
   10.77 +        let
   10.78 +          fun f (i, t) = term_to_coordinates P t |> map_option (pair i)
   10.79 +          val tcos = map_filter I (map_index f args)
   10.80 +        in
   10.81 +          if null tcos then NONE
   10.82 +          else SOME (Coordinate (map (pair s) tcos))
   10.83 +        end
   10.84 +    | _ => NONE
   10.85 +  end;
   10.86 +
   10.87 +fun coordinates_to_list (End x) = [(x, [])]
   10.88 +  | coordinates_to_list (Coordinate xs) = 
   10.89 +  let
   10.90 +    fun f (s, (n, xss)) = map (fn (T, xs) => (T, (s, n) :: xs)) (coordinates_to_list xss)
   10.91 +  in flat (map f xs) end;
   10.92 +
   10.93 +
   10.94 +(* AL: TODO: change from term to const_name *)
   10.95 +fun find_ctr ctr1 xs =
   10.96 +  let
   10.97 +    val const_name = fst o dest_Const
   10.98 +    fun const_equal (ctr1, ctr2) = const_name ctr1 = const_name ctr2
   10.99 +  in
  10.100 +    lookup_remove const_equal ctr1 xs
  10.101 +  end;
  10.102 +
  10.103 +datatype pattern 
  10.104 +  = Wildcard
  10.105 +  | Value
  10.106 +  | Split of int * (term * pattern) list * pattern;
  10.107 +
  10.108 +fun pattern_merge Wildcard pat' = pat'
  10.109 +  | pattern_merge Value _ = Value
  10.110 +  | pattern_merge (Split (n, xs, pat)) Wildcard =
  10.111 +    Split (n, map (apsnd (fn pat'' => pattern_merge pat'' Wildcard)) xs, pattern_merge pat Wildcard)
  10.112 +  | pattern_merge (Split _) Value = Value
  10.113 +  | pattern_merge (Split (n, xs, pat)) (Split (m, ys, pat'')) =
  10.114 +    let 
  10.115 +      fun merge_consts xs [] = map (apsnd (fn pat => pattern_merge pat Wildcard)) xs
  10.116 +        | merge_consts xs ((ctr, y) :: ys) =
  10.117 +          (case find_ctr ctr xs of
  10.118 +              (SOME (ctr, x), xs) => (ctr, pattern_merge x y) :: merge_consts xs ys
  10.119 +            | (NONE, xs) => (ctr, y) :: merge_consts xs ys
  10.120 +          )
  10.121 +     in
  10.122 +       Split (if n <= 0 then m else n, merge_consts xs ys, pattern_merge pat pat'')
  10.123 +     end
  10.124 +     
  10.125 +fun pattern_intersect Wildcard _ = Wildcard
  10.126 +  | pattern_intersect Value pat2 = pat2
  10.127 +  | pattern_intersect (Split _) Wildcard = Wildcard
  10.128 +  | pattern_intersect (Split (n, xs', pat1)) Value =
  10.129 +    Split (n,
  10.130 +      map (apsnd (fn pat1 => pattern_intersect pat1 Value)) xs',
  10.131 +      pattern_intersect pat1 Value)
  10.132 +  | pattern_intersect (Split (n, xs', pat1)) (Split (m, ys, pat2)) =
  10.133 +    Split (if n <= 0 then m else n, 
  10.134 +      intersect_consts xs' ys pat1 pat2,
  10.135 +      pattern_intersect pat1 pat2)
  10.136 +and
  10.137 +    intersect_consts xs [] _ default2 = map (apsnd (fn pat => pattern_intersect pat default2)) xs
  10.138 +  | intersect_consts xs ((ctr, pat2) :: ys) default1 default2 = case find_ctr ctr xs of
  10.139 +    (SOME (ctr, pat1), xs') => 
  10.140 +      (ctr, pattern_merge (pattern_merge (pattern_intersect pat1 pat2) (pattern_intersect default1 pat2))
  10.141 +              (pattern_intersect pat1 default2)) ::
  10.142 +      intersect_consts xs' ys default1 default2
  10.143 +    | (NONE, xs') => (ctr, pattern_intersect default1 pat2) :: (intersect_consts xs' ys default1 default2)
  10.144 +        
  10.145 +fun pattern_lookup _ Wildcard = Wildcard
  10.146 +  | pattern_lookup _ Value = Value
  10.147 +  | pattern_lookup [] (Split (n, xs, pat)) = 
  10.148 +    Split (n, map (apsnd (pattern_lookup [])) xs, pattern_lookup [] pat)
  10.149 +  | pattern_lookup (term :: terms) (Split (n, xs, pat)) =
  10.150 +  let
  10.151 +    val (ctr, args) = strip_comb term
  10.152 +    fun map_ctr (term, pat) =
  10.153 +      let
  10.154 +        val args = term |> dest_Const |> snd |> binder_types |> map (fn T => Free ("x", T))
  10.155 +      in
  10.156 +        pattern_lookup args pat
  10.157 +      end
  10.158 +  in
  10.159 +    if is_Const ctr then
  10.160 +       case find_ctr ctr xs of (SOME (_, pat'), _) => 
  10.161 +           pattern_lookup terms (pattern_merge (pattern_lookup args pat') (pattern_lookup [] pat))
  10.162 +         | (NONE, _) => pattern_lookup terms pat
  10.163 +    else if length xs < n orelse n <= 0 then
  10.164 +      pattern_lookup terms pat
  10.165 +    else pattern_lookup terms
  10.166 +      (pattern_merge
  10.167 +        (fold pattern_intersect (map map_ctr (tl xs)) (map_ctr (hd xs)))
  10.168 +        (pattern_lookup [] pat))
  10.169 +  end;
  10.170 +
  10.171 +fun pattern_contains terms pat = case pattern_lookup terms pat of
  10.172 +    Wildcard => false
  10.173 +  | Value => true
  10.174 +  | Split _ => raise Match;
  10.175 +
  10.176 +fun pattern_create _ [] = Wildcard
  10.177 +  | pattern_create ctr_count (term :: terms) = 
  10.178 +    let
  10.179 +      val (ctr, args) = strip_comb term
  10.180 +    in
  10.181 +      if is_Const ctr then
  10.182 +        Split (ctr_count ctr, [(ctr, pattern_create ctr_count (args @ terms))], Wildcard)
  10.183 +      else Split (0, [], pattern_create ctr_count terms)
  10.184 +    end;
  10.185 +
  10.186 +fun pattern_insert ctr_count terms pat =
  10.187 +  let
  10.188 +    fun new_pattern terms = pattern_insert ctr_count terms (pattern_create ctr_count terms)
  10.189 +    fun aux _ false Wildcard = Wildcard
  10.190 +      | aux terms true Wildcard = if null terms then Value else new_pattern terms
  10.191 +      | aux _ _ Value = Value
  10.192 +      | aux terms modify (Split (n, xs', pat)) =
  10.193 +      let
  10.194 +        val unmodified = (n, map (apsnd (aux [] false)) xs', aux [] false pat)
  10.195 +      in case terms of [] => Split unmodified
  10.196 +        | term :: terms =>
  10.197 +        let
  10.198 +          val (ctr, args) = strip_comb term
  10.199 +          val (m, ys, pat') = unmodified
  10.200 +        in
  10.201 +          if is_Const ctr
  10.202 +            then case find_ctr ctr xs' of
  10.203 +              (SOME (ctr, pat''), xs) =>
  10.204 +                Split (m, (ctr, aux (args @ terms) modify pat'') :: map (apsnd (aux [] false)) xs, pat')
  10.205 +              | (NONE, _) => if modify
  10.206 +                then if m <= 0
  10.207 +                  then Split (ctr_count ctr, (ctr, new_pattern (args @ terms)) :: ys, pat')
  10.208 +                  else Split (m, (ctr, new_pattern (args @ terms)) :: ys, pat')
  10.209 +                else Split unmodified
  10.210 +            else Split (m, ys, aux terms modify pat)
  10.211 +        end
  10.212 +      end
  10.213 +  in
  10.214 +    aux terms true pat
  10.215 +  end;
  10.216 +
  10.217 +val pattern_empty = Wildcard;
  10.218 +
  10.219 +fun replace_frees lhss rhss typ_list ctxt =
  10.220 +  let
  10.221 +    fun replace_frees_once (lhs, rhs) ctxt =
  10.222 +      let
  10.223 +        val add_frees_list = fold_rev Term.add_frees
  10.224 +        val frees = add_frees_list lhs []
  10.225 +        val (new_frees, ctxt1) = (Ctr_Sugar_Util.mk_Frees "x" (map snd frees) ctxt)
  10.226 +        val (new_frees1, ctxt2) =
  10.227 +          let
  10.228 +            val (dest_frees, types) = split_list (map dest_Free new_frees)
  10.229 +            val (new_frees, ctxt2) = Variable.variant_fixes dest_frees ctxt1
  10.230 +          in
  10.231 +            (map Free (new_frees ~~ types), ctxt2)
  10.232 +          end
  10.233 +        val dict = frees ~~ new_frees1
  10.234 +        fun free_map_fun (s, T) =
  10.235 +          case AList.lookup (op =) dict (s, T) of
  10.236 +              NONE => Free (s, T)
  10.237 +            | SOME x => x
  10.238 +        val map_fun = fold_term Const free_map_fun Var Bound Abs (op $)
  10.239 +      in
  10.240 +        ((map map_fun lhs, map_fun rhs), ctxt2)
  10.241 +      end
  10.242 +
  10.243 +    fun variant_fixes (def_frees, ctxt) =
  10.244 +      let
  10.245 +        val (dest_frees, types) = split_list (map dest_Free def_frees)
  10.246 +        val (def_frees, ctxt1) = Variable.variant_fixes dest_frees ctxt
  10.247 +      in
  10.248 +        (map Free (def_frees ~~ types), ctxt1)
  10.249 +      end
  10.250 +    val (def_frees, ctxt1) = variant_fixes (Ctr_Sugar_Util.mk_Frees "x" typ_list ctxt)
  10.251 +    val (rhs_frees, ctxt2) = variant_fixes (Ctr_Sugar_Util.mk_Frees "x" typ_list ctxt1)
  10.252 +    val (case_args, ctxt3) = variant_fixes (Ctr_Sugar_Util.mk_Frees "x"
  10.253 +      (map fastype_of (hd lhss)) ctxt2)
  10.254 +    val (new_terms1, ctxt4) = fold_map replace_frees_once (lhss ~~ rhss) ctxt3
  10.255 +    val (lhss1, rhss1) = split_list new_terms1
  10.256 +  in
  10.257 +    (lhss1, rhss1, def_frees ~~ rhs_frees, case_args, ctxt4)
  10.258 +  end;
  10.259 +
  10.260 +fun add_names_in_type (Type (name, Ts)) = 
  10.261 +    List.foldr (op o) (Symtab.update (name, ())) (map add_names_in_type Ts)
  10.262 +  | add_names_in_type (TFree _) = I
  10.263 +  | add_names_in_type (TVar _) = I
  10.264 +
  10.265 +fun add_names_in_term (Const (_, T)) = add_names_in_type T
  10.266 +  | add_names_in_term (Free (_, T)) = add_names_in_type T
  10.267 +  | add_names_in_term (Var (_, T)) = add_names_in_type T
  10.268 +  | add_names_in_term (Bound _) = I
  10.269 +  | add_names_in_term (Abs (_, T, body)) =
  10.270 +    add_names_in_type T o add_names_in_term body
  10.271 +  | add_names_in_term (t1 $ t2) = add_names_in_term t1 o add_names_in_term t2
  10.272 +
  10.273 +fun add_type_names terms =
  10.274 +  fold (fn term => fn f => add_names_in_term term o f) terms I
  10.275 +
  10.276 +fun get_split_theorems ctxt =
  10.277 +  Symtab.keys
  10.278 +  #> map_filter (Ctr_Sugar.ctr_sugar_of ctxt)
  10.279 +  #> map #split;
  10.280 +
  10.281 +fun match (Const (s1, _)) (Const (s2, _)) = if s1 = s2 then SOME I else NONE
  10.282 +  | match (Free y) x = SOME (fn z => if z = Free y then x else z)
  10.283 +  | match (pat1 $ pattern2) (t1 $ t2) =
  10.284 +    (case (match pat1 t1, match pattern2 t2) of
  10.285 +       (SOME f, SOME g) => SOME (f o g)
  10.286 +       | _ => NONE
  10.287 +     )
  10.288 +  | match _ _ = NONE;
  10.289 +
  10.290 +fun match_all patterns terms =
  10.291 +  let
  10.292 +    fun combine _ NONE = NONE
  10.293 +      | combine (f_opt, f_opt') (SOME g) = 
  10.294 +        case match f_opt f_opt' of SOME f => SOME (f o g) | _ => NONE
  10.295 +  in
  10.296 +    fold_rev combine (patterns ~~ terms) (SOME I)
  10.297 +  end
  10.298 +
  10.299 +fun matches (Const (s1, _)) (Const (s2, _)) = s1 = s2
  10.300 +  | matches (Free _) _ = true 
  10.301 +  | matches (pat1 $ pat2) (t1 $ t2) = matches pat1 t1 andalso matches pat2 t2
  10.302 +  | matches _ _ = false;
  10.303 +fun matches_all patterns terms = forall (uncurry matches) (patterns ~~ terms)
  10.304 +
  10.305 +fun terms_to_case_at ctr_count ctxt (fun_t : term) (default_lhs : term list)
  10.306 +    (pos, (lazy_case_arg, rhs_free))
  10.307 +    ((lhss : term list list), (rhss : term list), type_name_fun) =
  10.308 +  let
  10.309 +    fun abort t =
  10.310 +      let
  10.311 +        val fun_name = head_of t |> dest_Const |> fst
  10.312 +        val msg = "Missing pattern in " ^ fun_name ^ "."
  10.313 +      in
  10.314 +        mk_abort msg t
  10.315 +      end;
  10.316 +
  10.317 +    (* Step 1 : Eliminate lazy pattern *)
  10.318 +    fun replace_pat_at (n, tcos) pat pats =
  10.319 +      let
  10.320 +        fun map_at _ _ [] = raise Empty
  10.321 +          | map_at n f (x :: xs) = if n > 0
  10.322 +            then apfst (cons x) (map_at (n - 1) f xs)
  10.323 +            else apfst (fn x => x :: xs) (f x)
  10.324 +        fun replace [] pat term = (pat, term)
  10.325 +          | replace ((s1, n) :: tcos) pat term =
  10.326 +            let
  10.327 +              val (ctr, args) = strip_comb term
  10.328 +            in
  10.329 +              case ctr of Const (s2, _) =>
  10.330 +                  if s1 = s2
  10.331 +                  then apfst (pair ctr #> list_comb) (map_at n (replace tcos pat) args)
  10.332 +                  else (term, rhs_free)
  10.333 +                | _ => (term, rhs_free)
  10.334 +            end
  10.335 +        val (part1, (old_pat, part2)) = chop n pats ||> (fn xs => (hd xs, tl xs))
  10.336 +        val (new_pat, old_pat1) = replace tcos pat old_pat
  10.337 +      in
  10.338 +        (part1 @ [new_pat] @ part2, old_pat1)
  10.339 +      end                               
  10.340 +    val (lhss1, lazy_pats) = map (replace_pat_at pos lazy_case_arg) lhss
  10.341 +      |> split_list
  10.342 +
  10.343 +    (* Step 2 : Split patterns *)
  10.344 +    fun split equs =
  10.345 +      let
  10.346 +        fun merge_pattern (Const (s1, T1), Const (s2, _)) =
  10.347 +            if s1 = s2 then SOME (Const (s1, T1)) else NONE
  10.348 +          | merge_pattern (t, Free _) = SOME t
  10.349 +          | merge_pattern (Free _, t) = SOME t
  10.350 +          | merge_pattern (t1l $ t1r, t2l $ t2r) =
  10.351 +            (case (merge_pattern (t1l, t2l), merge_pattern (t1r, t2r)) of
  10.352 +              (SOME t1, SOME t2) => SOME (t1 $ t2)
  10.353 +              | _ => NONE)
  10.354 +          | merge_pattern _ = NONE
  10.355 +        fun merge_patterns pats1 pats2 = case (pats1, pats2) of
  10.356 +          ([], []) => SOME []
  10.357 +          | (x :: xs, y :: ys) =>
  10.358 +            (case (merge_pattern (x, y), merge_patterns xs ys) of
  10.359 +              (SOME x, SOME xs) => SOME (x :: xs)
  10.360 +              | _ => NONE
  10.361 +            )
  10.362 +          | _ => raise Match
  10.363 +        fun merge_insert ((lhs1, case_pat), _) [] =
  10.364 +            [(lhs1, pattern_empty |> pattern_insert ctr_count [case_pat])]
  10.365 +          | merge_insert ((lhs1, case_pat), rhs) ((lhs2, pat) :: pats) =
  10.366 +            let
  10.367 +              val pats = merge_insert ((lhs1, case_pat), rhs) pats
  10.368 +              val (first_equ_needed, new_lhs) = case merge_patterns lhs1 lhs2 of
  10.369 +                SOME new_lhs => (not (pattern_contains [case_pat] pat), new_lhs)
  10.370 +                | NONE => (false, lhs2)
  10.371 +              val second_equ_needed = not (matches_all lhs1 lhs2)
  10.372 +                orelse not first_equ_needed
  10.373 +              val first_equ = if first_equ_needed
  10.374 +                then [(new_lhs, pattern_insert ctr_count [case_pat] pat)]
  10.375 +                else []
  10.376 +              val second_equ = if second_equ_needed
  10.377 +                then [(lhs2, pat)]
  10.378 +                else []
  10.379 +            in
  10.380 +              first_equ @ second_equ @ pats
  10.381 +            end
  10.382 +        in
  10.383 +          (fold merge_insert equs []
  10.384 +            |> split_list
  10.385 +            |> fst) @ [default_lhs]
  10.386 +        end
  10.387 +    val lhss2 = split ((lhss1 ~~ lazy_pats) ~~ rhss)
  10.388 +
  10.389 +    (* Step 3 : Remove redundant patterns *)
  10.390 +    fun remove_redundant_lhs lhss =
  10.391 +      let
  10.392 +        fun f lhs pat = if pattern_contains lhs pat
  10.393 +          then ((lhs, false), pat)
  10.394 +          else ((lhs, true), pattern_insert ctr_count lhs pat)
  10.395 +      in
  10.396 +        fold_map f lhss pattern_empty
  10.397 +        |> fst
  10.398 +        |> filter snd
  10.399 +        |> map fst
  10.400 +      end
  10.401 +    fun remove_redundant_rhs rhss =
  10.402 +      let
  10.403 +        fun f (lhs, rhs) pat = if pattern_contains [lhs] pat
  10.404 +          then (((lhs, rhs), false), pat)
  10.405 +          else (((lhs, rhs), true), pattern_insert ctr_count [lhs] pat)
  10.406 +      in
  10.407 +        map fst (filter snd (fold_map f rhss pattern_empty |> fst))
  10.408 +      end
  10.409 +    val lhss3 = remove_redundant_lhs lhss2
  10.410 +
  10.411 +    (* Step 4 : Compute right hand side *)
  10.412 +    fun subs_fun f = fold_term
  10.413 +      Const
  10.414 +      (f o Free)
  10.415 +      Var
  10.416 +      Bound
  10.417 +      Abs
  10.418 +      (fn (x, y) => f x $ f y)
  10.419 +    fun find_rhss lhs =
  10.420 +      let
  10.421 +        fun f (lhs1, (pat, rhs)) = 
  10.422 +          case match_all lhs1 lhs of NONE => NONE
  10.423 +          | SOME f => SOME (pat, subs_fun f rhs)
  10.424 +      in
  10.425 +        remove_redundant_rhs
  10.426 +          (map_filter f (lhss1 ~~ (lazy_pats ~~ rhss)) @
  10.427 +            [(lazy_case_arg, list_comb (fun_t, lhs) |> abort)]
  10.428 +          )
  10.429 +      end
  10.430 +
  10.431 +    (* Step 5 : make_case of right hand side *)
  10.432 +    fun make_case ctxt case_arg cases = case cases of
  10.433 +      [(Free x, rhs)] => subs_fun (fn y => if y = Free x then case_arg else y) rhs
  10.434 +      | _ => Case_Translation.make_case
  10.435 +        ctxt
  10.436 +        Case_Translation.Warning
  10.437 +        Name.context
  10.438 +        case_arg
  10.439 +        cases
  10.440 +    val type_name_fun = add_type_names lazy_pats o type_name_fun
  10.441 +    val rhss3 = map ((make_case ctxt lazy_case_arg) o find_rhss) lhss3
  10.442 +  in
  10.443 +    (lhss3, rhss3, type_name_fun)
  10.444 +  end;
  10.445 +
  10.446 +fun terms_to_case ctxt ctr_count (head : term) (lhss : term list list)
  10.447 +    (rhss : term list) (typ_list : typ list) (poss : (int * (string * int) list) list) =
  10.448 +  let
  10.449 +    val (lhss1, rhss1, def_frees, case_args, ctxt1) = replace_frees lhss rhss typ_list ctxt
  10.450 +    val exec_list = poss ~~ def_frees
  10.451 +    val (lhss2, rhss2, type_name_fun) = fold_rev
  10.452 +      (terms_to_case_at ctr_count ctxt1 head case_args) exec_list (lhss1, rhss1, I)
  10.453 +    fun make_eq_term (lhss, rhs) = (list_comb (head, lhss), rhs)
  10.454 +      |> HOLogic.mk_eq
  10.455 +      |> HOLogic.mk_Trueprop
  10.456 +  in
  10.457 +    (map make_eq_term (lhss2 ~~ rhss2),
  10.458 +      get_split_theorems ctxt1 (type_name_fun Symtab.empty),
  10.459 +      ctxt1)
  10.460 +  end;
  10.461 +
  10.462 +fun build_case_t replace_ctr ctr_count head lhss rhss ctxt =
  10.463 +  let
  10.464 +    val num_eqs = length lhss
  10.465 +    val _ = if length rhss = num_eqs andalso num_eqs > 0 then ()
  10.466 +      else raise Fail
  10.467 +        ("expected same number of left-hand sides as right-hand sides\n"
  10.468 +          ^ "and at least one equation")
  10.469 +    val n = length (hd lhss)
  10.470 +    val _ = if forall (fn m => length m = n) lhss then ()
  10.471 +      else raise Fail "expected equal number of arguments"
  10.472 +
  10.473 +    fun to_coordinates (n, ts) = case map_filter (term_to_coordinates replace_ctr) ts of
  10.474 +        [] => NONE
  10.475 +      | (tco :: tcos) => SOME (n, fold term_coordinate_merge tcos tco |> coordinates_to_list)
  10.476 +    fun add_T (n, xss) = map (fn (T, xs) => (T, (n, xs))) xss
  10.477 +    val (typ_list, poss) = lhss
  10.478 +      |> Ctr_Sugar_Util.transpose
  10.479 +      |> map_index to_coordinates
  10.480 +      |> map_filter (map_option add_T)
  10.481 +      |> flat
  10.482 +      |> split_list 
  10.483 +  in
  10.484 +    if null poss then ([], [], ctxt)
  10.485 +    else terms_to_case ctxt (dest_Const #> ctr_count) head lhss rhss typ_list poss
  10.486 +  end;
  10.487 +
  10.488 +fun tac ctxt {splits, intros, defs} =
  10.489 +  let
  10.490 +    val split_and_subst = 
  10.491 +      split_tac ctxt splits 
  10.492 +      THEN' REPEAT_ALL_NEW (
  10.493 +        resolve_tac ctxt [@{thm conjI}, @{thm allI}]
  10.494 +        ORELSE'
  10.495 +        (resolve_tac ctxt [@{thm impI}] THEN' hyp_subst_tac_thin true ctxt))
  10.496 +  in
  10.497 +    (REPEAT_ALL_NEW split_and_subst ORELSE' K all_tac)
  10.498 +    THEN' (K (Local_Defs.unfold_tac ctxt [@{thm missing_pattern_match_def}]))
  10.499 +    THEN' (K (Local_Defs.unfold_tac ctxt defs))
  10.500 +    THEN_ALL_NEW (SOLVED' (resolve_tac ctxt (@{thm refl} :: intros)))
  10.501 +  end;
  10.502 +
  10.503 +fun to_case _ _ _ [] = NONE
  10.504 +  | to_case ctxt replace_ctr ctr_count ths =
  10.505 +    let
  10.506 +      val strip_eq = Thm.prop_of #> HOLogic.dest_Trueprop #> HOLogic.dest_eq
  10.507 +      fun import [] ctxt = ([], ctxt)
  10.508 +        | import (thm :: thms) ctxt =
  10.509 +          let
  10.510 +            val fun_ct = strip_eq #> fst #> head_of #> Logic.mk_term #> Thm.cterm_of ctxt
  10.511 +            val ct = fun_ct thm
  10.512 +            val cts = map fun_ct thms
  10.513 +            val pairs = map (fn s => (s,ct)) cts
  10.514 +            val thms' = map (fn (th,p) => Thm.instantiate (Thm.match p) th) (thms ~~ pairs)
  10.515 +          in
  10.516 +            Variable.import true (thm :: thms') ctxt |> apfst snd
  10.517 +          end
  10.518 +
  10.519 +      val (iths, ctxt') = import ths ctxt
  10.520 +      val head = hd iths |> strip_eq |> fst |> head_of
  10.521 +      val eqs = map (strip_eq #> apfst (snd o strip_comb)) iths
  10.522 +
  10.523 +      fun hide_rhs ((pat, rhs), name) lthy =
  10.524 +        let
  10.525 +          val frees = fold Term.add_frees pat []
  10.526 +          val abs_rhs = fold absfree frees rhs
  10.527 +          val (f, def, lthy') = case lthy
  10.528 +            |> Local_Defs.define [((Binding.name name, NoSyn), (Binding.empty_atts, abs_rhs))] of
  10.529 +              ([(f, (_, def))], lthy') => (f, def, lthy')
  10.530 +              | _ => raise Match
  10.531 +        in
  10.532 +          ((list_comb (f, map Free (rev frees)), def), lthy')
  10.533 +        end
  10.534 +
  10.535 +      val rhs_names = Name.invent (Variable.names_of ctxt') "rhs" (length eqs)
  10.536 +      val ((def_ts, def_thms), ctxt2) =
  10.537 +        fold_map hide_rhs (eqs ~~ rhs_names) ctxt' |> apfst split_list
  10.538 +      val (ts, split_thms, ctxt3) = build_case_t replace_ctr ctr_count head
  10.539 +        (map fst eqs) def_ts ctxt2
  10.540 +      fun mk_thm t = Goal.prove ctxt3 [] [] t
  10.541 +          (fn {context=ctxt, ...} => tac ctxt {splits=split_thms, intros=ths, defs=def_thms} 1)
  10.542 +    in
  10.543 +      if null ts then NONE
  10.544 +      else
  10.545 +        ts
  10.546 +        |> map mk_thm
  10.547 +        |> Proof_Context.export ctxt3 ctxt
  10.548 +        |> map (Goal.norm_result ctxt)
  10.549 +        |> SOME
  10.550 +    end;
  10.551 +
  10.552 +end
    11.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    11.2 +++ b/src/HOL/Library/code_lazy.ML	Sat May 12 11:24:11 2018 +0200
    11.3 @@ -0,0 +1,655 @@
    11.4 +(* Author: Pascal Stoop, ETH Zurich
    11.5 +   Author: Andreas Lochbihler, Digital Asset *)
    11.6 +
    11.7 +signature CODE_LAZY =
    11.8 +sig
    11.9 +  type lazy_info =
   11.10 +    {eagerT: typ,
   11.11 +     lazyT: typ,
   11.12 +     ctr: term,
   11.13 +     destr: term,
   11.14 +     lazy_ctrs: term list,
   11.15 +     case_lazy: term,
   11.16 +     active: bool,
   11.17 +     activate: theory -> theory,
   11.18 +     deactivate: theory -> theory};
   11.19 +  val code_lazy_type: string -> theory -> theory
   11.20 +  val activate_lazy_type: string -> theory -> theory
   11.21 +  val deactivate_lazy_type: string -> theory -> theory
   11.22 +  val activate_lazy_types: theory -> theory
   11.23 +  val deactivate_lazy_types: theory -> theory
   11.24 +
   11.25 +  val get_lazy_types: theory -> (string * lazy_info) list
   11.26 +
   11.27 +  val print_lazy_types: theory -> unit
   11.28 +
   11.29 +  val transform_code_eqs: Proof.context -> (thm * bool) list -> (thm * bool) list option
   11.30 +end;
   11.31 +
   11.32 +structure Code_Lazy : CODE_LAZY =
   11.33 +struct
   11.34 +
   11.35 +type lazy_info =
   11.36 +  {eagerT: typ,
   11.37 +   lazyT: typ,
   11.38 +   ctr: term,
   11.39 +   destr: term,
   11.40 +   lazy_ctrs: term list,
   11.41 +   case_lazy: term,
   11.42 +   active: bool,
   11.43 +   activate: theory -> theory,
   11.44 +   deactivate: theory -> theory};
   11.45 +
   11.46 +fun map_active f {eagerT, lazyT, ctr, destr, lazy_ctrs, case_lazy, active, activate, deactivate} =
   11.47 +  { eagerT = eagerT, 
   11.48 +    lazyT = lazyT,
   11.49 +    ctr = ctr,
   11.50 +    destr = destr,
   11.51 +    lazy_ctrs = lazy_ctrs,
   11.52 +    case_lazy = case_lazy,
   11.53 +    active = f active,
   11.54 +    activate = activate,
   11.55 +    deactivate = deactivate
   11.56 +  }
   11.57 +
   11.58 +structure Laziness_Data = Theory_Data(
   11.59 +  type T = lazy_info Symtab.table;
   11.60 +  val empty = Symtab.empty;
   11.61 +  val merge = Symtab.join (fn _ => fn (_, record) => record);
   11.62 +  val extend = I;
   11.63 +);
   11.64 +
   11.65 +fun fold_type type' tfree tvar typ =
   11.66 +  let
   11.67 +    fun go (Type (s, Ts)) = type' (s, map go Ts)
   11.68 +      | go (TFree T) = tfree T
   11.69 +      | go (TVar T) = tvar T
   11.70 +  in
   11.71 +    go typ
   11.72 +  end;
   11.73 +
   11.74 +fun read_typ lthy name =
   11.75 +  let
   11.76 +    val (s, Ts) = Proof_Context.read_type_name {proper = true, strict = true} lthy name |> dest_Type
   11.77 +    val (Ts', _) = Ctr_Sugar_Util.mk_TFrees (length Ts) lthy
   11.78 +  in 
   11.79 +    Type (s, Ts')
   11.80 +  end
   11.81 +
   11.82 +fun mk_name prefix suffix name ctxt =
   11.83 +  Ctr_Sugar_Util.mk_fresh_names ctxt 1 (prefix ^ name ^ suffix) |>> hd;
   11.84 +fun generate_typedef_name name ctxt = mk_name "" "_lazy" name ctxt;
   11.85 +
   11.86 +fun add_syntax_definition short_type_name eagerT lazyT lazy_ctr lthy = 
   11.87 +  let
   11.88 +    val (name, _) = mk_name "lazy_" "" short_type_name lthy
   11.89 +    val freeT = HOLogic.unitT --> lazyT
   11.90 +    val lazyT' = Type (@{type_name lazy}, [lazyT])
   11.91 +    val def = Logic.all_const freeT $ absdummy freeT (Logic.mk_equals (
   11.92 +      Free (name, (freeT --> eagerT)) $ Bound 0,
   11.93 +      lazy_ctr $ (Const (@{const_name delay}, (freeT --> lazyT')) $ Bound 0)))
   11.94 +    val (_, lthy') = Local_Theory.open_target lthy
   11.95 +    val ((t, (_, thm)), lthy') = Specification.definition NONE [] [] 
   11.96 +      ((Thm.def_binding (Binding.name name), []), def) lthy'
   11.97 +    val lthy' = Specification.notation true ("", false) [(t, Mixfix.mixfix "_")] lthy'
   11.98 +    val lthy = Local_Theory.close_target lthy'
   11.99 +    val def_thm = singleton (Proof_Context.export lthy' lthy) thm
  11.100 +  in
  11.101 +    (def_thm, lthy)
  11.102 +  end;
  11.103 +
  11.104 +fun add_ctr_code raw_ctrs case_thms thy =
  11.105 +  let
  11.106 +    fun mk_case_certificate ctxt raw_thms =
  11.107 +      let
  11.108 +        val thms = raw_thms
  11.109 +          |> Conjunction.intr_balanced
  11.110 +          |> Thm.unvarify_global (Proof_Context.theory_of ctxt)
  11.111 +          |> Conjunction.elim_balanced (length raw_thms)
  11.112 +          |> map Simpdata.mk_meta_eq
  11.113 +          |> map Drule.zero_var_indexes
  11.114 +        val thm1 = case thms of
  11.115 +          thm :: _ => thm
  11.116 +          | _ => raise Empty
  11.117 +        val params = Term.add_free_names (Thm.prop_of thm1) [];
  11.118 +        val rhs = thm1
  11.119 +          |> Thm.prop_of |> Logic.dest_equals |> fst |> strip_comb
  11.120 +          ||> fst o split_last |> list_comb
  11.121 +        val lhs = Free (singleton (Name.variant_list params) "case", fastype_of rhs);
  11.122 +        val assum = Thm.cterm_of ctxt (Logic.mk_equals (lhs, rhs))
  11.123 +      in
  11.124 +        thms
  11.125 +        |> Conjunction.intr_balanced
  11.126 +        |> rewrite_rule ctxt [Thm.symmetric (Thm.assume assum)]
  11.127 +        |> Thm.implies_intr assum
  11.128 +        |> Thm.generalize ([], params) 0
  11.129 +        |> Axclass.unoverload ctxt
  11.130 +        |> Thm.varifyT_global
  11.131 +      end
  11.132 +    val ctrs = map (apsnd (perhaps (try Logic.unvarifyT_global))) raw_ctrs
  11.133 +    val unover_ctrs = map (fn ctr as (_, fcT) => (Axclass.unoverload_const thy ctr, fcT)) ctrs
  11.134 +  in
  11.135 +    if can (Code.constrset_of_consts thy) unover_ctrs then
  11.136 +      thy
  11.137 +      |> Code.declare_datatype_global ctrs
  11.138 +      |> fold_rev (Code.add_eqn_global o rpair true) case_thms
  11.139 +      |> Code.declare_case_global (mk_case_certificate (Proof_Context.init_global thy) case_thms)
  11.140 +    else
  11.141 +      thy
  11.142 +  end;
  11.143 +
  11.144 +fun not_found s = error (s ^ " has not been added as lazy type");
  11.145 +
  11.146 +fun validate_type_name thy type_name =
  11.147 +  let
  11.148 +    val lthy = Named_Target.theory_init thy
  11.149 +    val eager_type = read_typ lthy type_name
  11.150 +    val type_name = case eager_type of
  11.151 +      Type (s, _) => s
  11.152 +      | _ => raise Match
  11.153 +  in
  11.154 +    type_name
  11.155 +  end;
  11.156 +
  11.157 +fun set_active_lazy_type value eager_type_string thy =
  11.158 +  let
  11.159 +    val type_name = validate_type_name thy eager_type_string
  11.160 +    val x =
  11.161 +      case Symtab.lookup (Laziness_Data.get thy) type_name of
  11.162 +        NONE => not_found type_name
  11.163 +        | SOME x => x
  11.164 +    val new_x = map_active (K value) x
  11.165 +    val thy1 = if value = #active x
  11.166 +      then thy
  11.167 +      else if value
  11.168 +        then #activate x thy
  11.169 +        else #deactivate x thy
  11.170 +  in
  11.171 +    Laziness_Data.map (Symtab.update (type_name, new_x)) thy1
  11.172 +  end;
  11.173 +
  11.174 +fun set_active_lazy_types value thy =
  11.175 +  let
  11.176 +    val lazy_type_names = Symtab.keys (Laziness_Data.get thy)
  11.177 +    fun fold_fun value type_name thy =
  11.178 +      let
  11.179 +        val x =
  11.180 +          case Symtab.lookup (Laziness_Data.get thy) type_name of
  11.181 +            SOME x => x
  11.182 +            | NONE => raise Match
  11.183 +        val new_x = map_active (K value) x
  11.184 +        val thy1 = if value = #active x
  11.185 +          then thy
  11.186 +          else if value
  11.187 +            then #activate x thy
  11.188 +            else #deactivate x thy
  11.189 +      in
  11.190 +        Laziness_Data.map (Symtab.update (type_name, new_x)) thy1
  11.191 +      end
  11.192 +  in
  11.193 +    fold (fold_fun value) lazy_type_names thy
  11.194 +  end;
  11.195 +
  11.196 +(* code_lazy_type : string -> theory -> theory *)
  11.197 +fun code_lazy_type eager_type_string thy =
  11.198 +  let
  11.199 +    val lthy = Named_Target.theory_init thy
  11.200 +    val eagerT = read_typ lthy eager_type_string
  11.201 +    val (type_name, type_args) = dest_Type eagerT
  11.202 +    val short_type_name = Long_Name.base_name type_name
  11.203 +    val _ = if Symtab.defined (Laziness_Data.get thy) type_name
  11.204 +      then error (type_name ^ " has already been added as lazy type.")
  11.205 +      else ()
  11.206 +    val {case_thms, casex, ctrs, ...} = case Ctr_Sugar.ctr_sugar_of lthy type_name of
  11.207 +        SOME x => x
  11.208 +      | _ => error (type_name ^ " is not registered with free constructors.")
  11.209 +
  11.210 +    fun substitute_ctr (old_T, new_T) ctr_T lthy =
  11.211 +      let
  11.212 +        val old_ctr_vars = map TVar (Term.add_tvarsT ctr_T [])
  11.213 +        val old_ctr_Ts = map TFree (Term.add_tfreesT ctr_T []) @ old_ctr_vars
  11.214 +        val (new_ctr_Ts, lthy') = Ctr_Sugar_Util.mk_TFrees (length old_ctr_Ts) lthy
  11.215 +
  11.216 +        fun double_type_fold Ts = case Ts of
  11.217 +          (Type (_, Ts1), Type (_, Ts2)) => flat (map double_type_fold (Ts1 ~~ Ts2))
  11.218 +          | (Type _, _) => raise Match
  11.219 +          | (_, Type _) => raise Match
  11.220 +          | Ts => [Ts]
  11.221 +        fun map_fun1 f = List.foldr
  11.222 +          (fn ((T1, T2), f) => fn T => if T = T1 then T2 else f T)
  11.223 +          f
  11.224 +          (double_type_fold (old_T, new_T))
  11.225 +        val map_fun2 = AList.lookup (op =) (old_ctr_Ts ~~ new_ctr_Ts) #> the
  11.226 +        val map_fun = map_fun1 map_fun2
  11.227 +
  11.228 +        val new_ctr_type = fold_type Type (map_fun o TFree) (map_fun o TVar) ctr_T
  11.229 +      in
  11.230 +        (new_ctr_type, lthy')
  11.231 +      end
  11.232 +
  11.233 +    val (short_lazy_type_name, lthy1) = generate_typedef_name short_type_name lthy
  11.234 +
  11.235 +    fun mk_lazy_typedef (name, eager_type) lthy =
  11.236 +      let
  11.237 +        val binding = Binding.name name
  11.238 +        val (result, lthy1) = (Typedef.add_typedef
  11.239 +            { overloaded=false }
  11.240 +            (binding, rev (Term.add_tfreesT eager_type []), Mixfix.NoSyn)
  11.241 +            (Const (@{const_name "top"}, Type (@{type_name set}, [eager_type])))
  11.242 +            NONE
  11.243 +            (fn ctxt => resolve_tac ctxt [@{thm UNIV_witness}] 1)
  11.244 +          o (Local_Theory.open_target #> snd)) lthy
  11.245 +      in
  11.246 +         (binding, result, Local_Theory.close_target lthy1)
  11.247 +      end;
  11.248 +
  11.249 +    val (typedef_binding, (_, info), lthy2) = mk_lazy_typedef (short_lazy_type_name, eagerT) lthy1
  11.250 +
  11.251 +    val lazy_type = Type (Local_Theory.full_name lthy2 typedef_binding, type_args)
  11.252 +    val (Abs_lazy, Rep_lazy) =
  11.253 +      let
  11.254 +        val info = fst info
  11.255 +        val Abs_name = #Abs_name info
  11.256 +        val Rep_name = #Rep_name info
  11.257 +        val Abs_type = eagerT --> lazy_type
  11.258 +        val Rep_type = lazy_type --> eagerT
  11.259 +      in
  11.260 +        (Const (Abs_name, Abs_type), Const (Rep_name, Rep_type))
  11.261 +      end
  11.262 +    val Abs_inverse = #Abs_inverse (snd info)
  11.263 +    val Rep_inverse = #Rep_inverse (snd info)
  11.264 +
  11.265 +    val (ctrs', lthy3) = List.foldr
  11.266 +      (fn (Const (s, T), (ctrs, lthy)) => let
  11.267 +            val (T', lthy') = substitute_ctr (body_type T, eagerT) T lthy
  11.268 +          in
  11.269 +            ((Const (s, T')) :: ctrs, lthy')
  11.270 +          end
  11.271 +      )
  11.272 +      ([], lthy2)
  11.273 +      ctrs
  11.274 +
  11.275 +    fun to_destr_eagerT typ = case typ of
  11.276 +          Type (@{type_name "fun"}, [_, Type (@{type_name "fun"}, Ts)]) => 
  11.277 +          to_destr_eagerT (Type (@{type_name "fun"}, Ts))
  11.278 +        | Type (@{type_name "fun"}, [T, _]) => T
  11.279 +        | _ => raise Match
  11.280 +    val (case', lthy4) = 
  11.281 +      let
  11.282 +        val (eager_case, caseT) = dest_Const casex
  11.283 +        val (caseT', lthy') = substitute_ctr (to_destr_eagerT caseT, eagerT) caseT lthy3
  11.284 +      in (Const (eager_case, caseT'), lthy') end
  11.285 +
  11.286 +    val ctr_names = map (Long_Name.base_name o fst o dest_Const) ctrs
  11.287 +    val ((((lazy_ctr_name, lazy_sel_name), lazy_ctrs_name), lazy_case_name), ctxt) = lthy4
  11.288 +      |> mk_name "Lazy_" "" short_type_name
  11.289 +      ||>> mk_name "unlazy_" "" short_type_name
  11.290 +      ||>> fold_map (mk_name "" "_Lazy") ctr_names
  11.291 +      ||>> mk_name "case_" "_lazy" short_type_name
  11.292 +
  11.293 +    fun mk_def (name, T, rhs) lthy =
  11.294 +      let
  11.295 +        val binding = Binding.name name
  11.296 +        val ((_, (_, thm)), lthy1) = 
  11.297 +          Local_Theory.open_target lthy |> snd
  11.298 +          |> Specification.definition NONE [] [] ((Thm.def_binding binding, []), rhs)
  11.299 +        val lthy2 = Local_Theory.close_target lthy1
  11.300 +        val def_thm = hd (Proof_Context.export lthy1 lthy2 [thm])
  11.301 +      in
  11.302 +        ({binding = binding, const = Const (Local_Theory.full_name lthy2 binding, T), thm = def_thm}, lthy2)
  11.303 +      end;
  11.304 +    
  11.305 +    val lazy_datatype = Type (@{type_name lazy}, [lazy_type])
  11.306 +    val Lazy_type = lazy_datatype --> eagerT
  11.307 +    val unstr_type = eagerT --> lazy_datatype
  11.308 +    
  11.309 +    fun apply_bounds i n term =
  11.310 +      if n > i then apply_bounds i (n-1) (term $ Bound (n-1))
  11.311 +      else term
  11.312 +    fun all_abs Ts t = Logic.list_all (map (pair Name.uu) Ts, t)
  11.313 +    fun mk_force t = Const (@{const_name force}, lazy_datatype --> lazy_type) $ t
  11.314 +    fun mk_delay t = Const (@{const_name delay}, (@{typ unit} --> lazy_type) --> lazy_datatype) $ t
  11.315 +
  11.316 +    val lazy_ctr = all_abs [lazy_datatype]
  11.317 +      (Logic.mk_equals (Free (lazy_ctr_name, Lazy_type) $ Bound 0, Rep_lazy $ mk_force (Bound 0)))
  11.318 +    val (lazy_ctr_def, lthy5) = mk_def (lazy_ctr_name, Lazy_type, lazy_ctr) lthy4
  11.319 +
  11.320 +    val lazy_sel = all_abs [eagerT]
  11.321 +      (Logic.mk_equals (Free (lazy_sel_name, unstr_type) $ Bound 0, 
  11.322 +        mk_delay (Abs (Name.uu, @{typ unit}, Abs_lazy $ Bound 1))))
  11.323 +    val (lazy_sel_def, lthy6) = mk_def (lazy_sel_name, unstr_type, lazy_sel) lthy5
  11.324 +
  11.325 +    fun mk_lazy_ctr (name, eager_ctr) =
  11.326 +      let
  11.327 +        val (_, ctrT) = dest_Const eager_ctr
  11.328 +        fun to_lazy_ctrT (Type (@{type_name fun}, [T1, T2])) = T1 --> to_lazy_ctrT T2
  11.329 +          | to_lazy_ctrT T = if T = eagerT then lazy_type else raise Match
  11.330 +        val lazy_ctrT = to_lazy_ctrT ctrT
  11.331 +        val argsT = binder_types ctrT
  11.332 +        val lhs = apply_bounds 0 (length argsT) (Free (name, lazy_ctrT))
  11.333 +        val rhs = Abs_lazy $ apply_bounds 0 (length argsT) eager_ctr
  11.334 +      in
  11.335 +        mk_def (name, lazy_ctrT, all_abs argsT (Logic.mk_equals (lhs, rhs)))
  11.336 +      end
  11.337 +    val (lazy_ctrs_def, lthy7) = fold_map mk_lazy_ctr (lazy_ctrs_name ~~ ctrs') lthy6
  11.338 +
  11.339 +    val (lazy_case_def, lthy8) =
  11.340 +      let
  11.341 +        val (_, caseT) = dest_Const case'
  11.342 +        fun to_lazy_caseT (Type (@{type_name fun}, [T1, T2])) =
  11.343 +            if T1 = eagerT then lazy_type --> T2 else T1 --> to_lazy_caseT T2
  11.344 +        val lazy_caseT = to_lazy_caseT caseT
  11.345 +        val argsT = binder_types lazy_caseT
  11.346 +        val n = length argsT
  11.347 +        val lhs = apply_bounds 0 n (Free (lazy_case_name, lazy_caseT)) 
  11.348 +        val rhs = apply_bounds 1 n case' $ (Rep_lazy $ Bound 0)
  11.349 +      in
  11.350 +        mk_def (lazy_case_name, lazy_caseT, all_abs argsT (Logic.mk_equals (lhs, rhs))) lthy7
  11.351 +      end
  11.352 +
  11.353 +    fun mk_thm ((name, term), thms) lthy =
  11.354 +      let
  11.355 +        val binding = Binding.name name
  11.356 +        fun tac {context, ...} = Simplifier.simp_tac
  11.357 +          (put_simpset HOL_basic_ss context addsimps thms)
  11.358 +          1
  11.359 +        val thm = Goal.prove lthy [] [] term tac
  11.360 +        val (_, lthy1) = lthy
  11.361 +          |> Local_Theory.open_target |> snd
  11.362 +          |> Local_Theory.note ((binding, []), [thm])
  11.363 +      in
  11.364 +        (thm, Local_Theory.close_target lthy1)
  11.365 +      end
  11.366 +    fun mk_thms exec_list lthy = fold_map mk_thm exec_list lthy
  11.367 +
  11.368 +    val mk_eq = HOLogic.mk_Trueprop o HOLogic.mk_eq
  11.369 +
  11.370 +    val lazy_ctrs = map #const lazy_ctrs_def
  11.371 +    val eager_lazy_ctrs = ctrs' ~~ lazy_ctrs
  11.372 +
  11.373 +    val (((((((Lazy_delay_eq_name, Rep_ctr_names), ctrs_lazy_names), force_sel_name), case_lazy_name),
  11.374 +      sel_lazy_name), case_ctrs_name), _) = lthy5
  11.375 +      |> mk_name "Lazy_" "_delay" short_type_name
  11.376 +      ||>> fold_map (mk_name "Rep_" "_Lazy") ctr_names
  11.377 +      ||>> fold_map (mk_name "" "_conv_lazy") ctr_names
  11.378 +      ||>> mk_name "force_unlazy_" "" short_type_name
  11.379 +      ||>> mk_name "case_" "_conv_lazy" short_type_name
  11.380 +      ||>> mk_name "Lazy_" "_inverse" short_type_name
  11.381 +      ||>> fold_map (mk_name ("case_" ^ short_type_name ^ "_lazy_") "") ctr_names
  11.382 +
  11.383 +    val mk_Lazy_delay_eq =
  11.384 +      (#const lazy_ctr_def $ mk_delay (Bound 0), Rep_lazy $ (Bound 0 $ @{const Unity}))
  11.385 +      |> mk_eq |> all_abs [@{typ unit} --> lazy_type]
  11.386 +    val (Lazy_delay_thm, lthy8a) = mk_thm 
  11.387 +      ((Lazy_delay_eq_name, mk_Lazy_delay_eq), [#thm lazy_ctr_def, @{thm force_delay}])
  11.388 +      lthy8
  11.389 +
  11.390 +    fun mk_lazy_ctr_eq (eager_ctr, lazy_ctr) =
  11.391 +      let
  11.392 +        val (_, ctrT) = dest_Const eager_ctr
  11.393 +        val argsT = binder_types ctrT
  11.394 +        val args = length argsT
  11.395 +      in
  11.396 +        (Rep_lazy $ apply_bounds 0 args lazy_ctr, apply_bounds 0 args eager_ctr)
  11.397 +        |> mk_eq |> all_abs argsT
  11.398 +      end
  11.399 +    val Rep_ctr_eqs = map mk_lazy_ctr_eq eager_lazy_ctrs
  11.400 +    val (Rep_ctr_thms, lthy8b) = mk_thms
  11.401 +        ((Rep_ctr_names ~~ Rep_ctr_eqs) ~~
  11.402 +          (map (fn def => [#thm def, Abs_inverse, @{thm UNIV_I}]) lazy_ctrs_def)
  11.403 +        )
  11.404 +        lthy8a
  11.405 +
  11.406 +    fun mk_ctrs_lazy_eq (eager_ctr, lazy_ctr) =
  11.407 +      let
  11.408 +        val argsT = dest_Const eager_ctr |> snd |> binder_types
  11.409 +        val n = length argsT
  11.410 +        val lhs = apply_bounds 0 n eager_ctr
  11.411 +        val rhs = #const lazy_ctr_def $ 
  11.412 +          (mk_delay (Abs (Name.uu, @{typ unit}, apply_bounds 1 (n + 1) lazy_ctr)))
  11.413 +      in
  11.414 +        (lhs, rhs) |> mk_eq |> all_abs argsT
  11.415 +      end
  11.416 +    val ctrs_lazy_eq = map mk_ctrs_lazy_eq eager_lazy_ctrs 
  11.417 +    val (ctrs_lazy_thms, lthy8c) = mk_thms
  11.418 +      ((ctrs_lazy_names ~~ ctrs_lazy_eq) ~~ map (fn thm => [Lazy_delay_thm, thm]) Rep_ctr_thms)
  11.419 +      lthy8b
  11.420 +
  11.421 +    val force_sel_eq = 
  11.422 +      (mk_force (#const lazy_sel_def $ Bound 0), Abs_lazy $ Bound 0)
  11.423 +      |> mk_eq |> all_abs [eagerT]
  11.424 +    val (force_sel_thm, lthy8d) = mk_thm
  11.425 +        ((force_sel_name, force_sel_eq), [#thm lazy_sel_def, @{thm force_delay}])
  11.426 +        lthy8c
  11.427 +
  11.428 +    val case_lazy_eq = 
  11.429 +      let
  11.430 +        val (_, caseT) = case' |> dest_Const
  11.431 +        val argsT = binder_types caseT
  11.432 +        val n = length argsT
  11.433 +        val lhs = apply_bounds 0 n case'
  11.434 +        val rhs = apply_bounds 1 n (#const lazy_case_def) $ (mk_force (#const lazy_sel_def $ Bound 0))
  11.435 +      in
  11.436 +        (lhs, rhs) |> mk_eq |> all_abs argsT
  11.437 +      end
  11.438 +    val (case_lazy_thm, lthy8e) = mk_thm
  11.439 +        ((case_lazy_name, case_lazy_eq), 
  11.440 +        [#thm lazy_case_def, force_sel_thm, Abs_inverse, @{thm UNIV_I}])
  11.441 +        lthy8d
  11.442 +
  11.443 +    val sel_lazy_eq =
  11.444 +      (#const lazy_sel_def $ (#const lazy_ctr_def $ Bound 0), Bound 0)
  11.445 +      |> mk_eq |> all_abs [lazy_datatype]
  11.446 +    val (sel_lazy_thm, lthy8f) = mk_thm
  11.447 +      ((sel_lazy_name, sel_lazy_eq),
  11.448 +      [#thm lazy_sel_def, #thm lazy_ctr_def, Rep_inverse, @{thm delay_force}])
  11.449 +      lthy8e
  11.450 +
  11.451 +    fun mk_case_ctrs_eq (i, lazy_ctr) =
  11.452 +      let
  11.453 +        val lazy_case = #const lazy_case_def
  11.454 +        val (_, ctrT) = dest_Const lazy_ctr
  11.455 +        val ctr_argsT = binder_types ctrT
  11.456 +        val ctr_args_n = length ctr_argsT
  11.457 +        val (_, caseT) = dest_Const lazy_case
  11.458 +        val case_argsT = binder_types caseT
  11.459 +
  11.460 +        fun n_bounds_from m n t =
  11.461 +          if n > 0 then n_bounds_from (m - 1) (n - 1) (t $ Bound (m - 1)) else t
  11.462 +
  11.463 +        val case_argsT' = take (length case_argsT - 1) case_argsT
  11.464 +        val Ts = case_argsT' @ ctr_argsT
  11.465 +        val num_abs_types = length Ts
  11.466 +        val lhs = n_bounds_from num_abs_types (length case_argsT') lazy_case $
  11.467 +          apply_bounds 0 ctr_args_n lazy_ctr
  11.468 +        val rhs = apply_bounds 0 ctr_args_n (Bound (num_abs_types - i - 1))
  11.469 +      in
  11.470 +        (lhs, rhs) |> mk_eq |> all_abs Ts
  11.471 +      end
  11.472 +    val case_ctrs_eq = map_index mk_case_ctrs_eq lazy_ctrs
  11.473 +    val (case_ctrs_thms, lthy9) = mk_thms
  11.474 +        ((case_ctrs_name ~~ case_ctrs_eq) ~~
  11.475 +         map2 (fn thm1 => fn thm2 => [#thm lazy_case_def, thm1, thm2]) Rep_ctr_thms case_thms
  11.476 +        )
  11.477 +        lthy8f
  11.478 +
  11.479 +    val (pat_def_thm, lthy10) = 
  11.480 +      add_syntax_definition short_type_name eagerT lazy_type (#const lazy_ctr_def) lthy9
  11.481 +
  11.482 +    val add_lazy_ctrs =
  11.483 +      Code.declare_datatype_global [dest_Const (#const lazy_ctr_def)]
  11.484 +    val eager_ctrs = map (apsnd (perhaps (try Logic.unvarifyT_global)) o dest_Const) ctrs
  11.485 +    val add_eager_ctrs =
  11.486 +      fold Code.del_eqn_global ctrs_lazy_thms
  11.487 +      #> Code.declare_datatype_global eager_ctrs
  11.488 +    val add_code_eqs = fold (Code.add_eqn_global o rpair true) 
  11.489 +      ([case_lazy_thm, sel_lazy_thm])
  11.490 +    val add_lazy_ctr_thms = fold (Code.add_eqn_global o rpair true) ctrs_lazy_thms
  11.491 +    val add_lazy_case_thms =
  11.492 +      fold Code.del_eqn_global case_thms
  11.493 +      #> Code.add_eqn_global (case_lazy_thm, false)
  11.494 +    val add_eager_case_thms = Code.del_eqn_global case_lazy_thm
  11.495 +      #> fold (Code.add_eqn_global o rpair false) case_thms
  11.496 +
  11.497 +    val delay_dummy_thm = (pat_def_thm RS @{thm symmetric})
  11.498 +      |> Drule.infer_instantiate' lthy10
  11.499 +         [SOME (Thm.cterm_of lthy10 (Const (@{const_name "Pure.dummy_pattern"}, HOLogic.unitT --> lazy_type)))]
  11.500 +      |> Thm.generalize (map (fst o dest_TFree) type_args, []) (Variable.maxidx_of lthy10 + 1);
  11.501 +
  11.502 +    val ctr_post = delay_dummy_thm :: map (fn thm => thm RS @{thm sym}) ctrs_lazy_thms
  11.503 +    val ctr_thms_abs = map (fn thm => Drule.abs_def (thm RS @{thm eq_reflection})) ctrs_lazy_thms
  11.504 +    val case_thm_abs = Drule.abs_def (case_lazy_thm RS @{thm eq_reflection})
  11.505 +    val add_simps = Code_Preproc.map_pre
  11.506 +      (fn ctxt => ctxt addsimps (case_thm_abs :: ctr_thms_abs))
  11.507 +    val del_simps = Code_Preproc.map_pre
  11.508 +      (fn ctxt => ctxt delsimps (case_thm_abs :: ctr_thms_abs))
  11.509 +    val add_post = Code_Preproc.map_post
  11.510 +      (fn ctxt => ctxt addsimps ctr_post)
  11.511 +    val del_post = Code_Preproc.map_post
  11.512 +      (fn ctxt => ctxt delsimps ctr_post)
  11.513 +  in
  11.514 +    Local_Theory.exit_global lthy10
  11.515 +    |> Laziness_Data.map (Symtab.update (type_name,
  11.516 +      {eagerT = eagerT, 
  11.517 +       lazyT = lazy_type,
  11.518 +       ctr = #const lazy_ctr_def,
  11.519 +       destr = #const lazy_sel_def,
  11.520 +       lazy_ctrs = map #const lazy_ctrs_def,
  11.521 +       case_lazy = #const lazy_case_def,
  11.522 +       active = true,
  11.523 +       activate = add_lazy_ctrs #> add_lazy_ctr_thms #> add_lazy_case_thms #> add_simps #> add_post,
  11.524 +       deactivate = add_eager_ctrs #> add_eager_case_thms #> del_simps #> del_post}))
  11.525 +    |> add_lazy_ctrs
  11.526 +    |> add_ctr_code (map (dest_Const o #const) lazy_ctrs_def) case_ctrs_thms
  11.527 +    |> add_code_eqs
  11.528 +    |> add_lazy_ctr_thms
  11.529 +    |> add_simps
  11.530 +    |> add_post
  11.531 +  end;
  11.532 +
  11.533 +fun transform_code_eqs _ [] = NONE
  11.534 +  | transform_code_eqs ctxt eqs =
  11.535 +    let
  11.536 +      val thy = Proof_Context.theory_of ctxt
  11.537 +      val table = Laziness_Data.get thy
  11.538 +      fun eliminate (s1, s2) = case Symtab.lookup table s1 of
  11.539 +          NONE => false
  11.540 +        | SOME x => #active x andalso s2 <> (#ctr x |> dest_Const |> fst)
  11.541 +      fun num_consts_fun (_, T) =
  11.542 +        let
  11.543 +          val s = body_type T |> dest_Type |> fst
  11.544 +        in
  11.545 +          if Symtab.defined table s
  11.546 +            then Ctr_Sugar.ctr_sugar_of ctxt s |> the |> #ctrs |> length
  11.547 +            else Code.get_type thy s |> fst |> snd |> length
  11.548 +        end
  11.549 +      val eqs = map (apfst (Thm.transfer thy)) eqs;
  11.550 +
  11.551 +      val ((code_eqs, nbe_eqs), pure) =
  11.552 +        ((case hd eqs |> fst |> Thm.prop_of of
  11.553 +            Const (@{const_name Pure.eq}, _) $ _ $ _ =>
  11.554 +              (map (apfst (fn x => x RS @{thm meta_eq_to_obj_eq})) eqs, true)
  11.555 +         | _ => (eqs, false))
  11.556 +        |> apfst (List.partition snd))
  11.557 +        handle THM _ => (([], eqs), false)
  11.558 +      val to_original_eq = if pure then map (apfst (fn x => x RS @{thm eq_reflection})) else I
  11.559 +    in
  11.560 +      case Case_Converter.to_case ctxt eliminate num_consts_fun (map fst code_eqs) of
  11.561 +          NONE => NONE
  11.562 +        | SOME thms => SOME (nbe_eqs @ map (rpair true) thms |> to_original_eq)
  11.563 +    end handle THM ex => (Output.writeln (@{make_string} eqs); raise THM ex);
  11.564 +
  11.565 +val activate_lazy_type = set_active_lazy_type true;
  11.566 +val deactivate_lazy_type = set_active_lazy_type false;
  11.567 +val activate_lazy_types = set_active_lazy_types true;
  11.568 +val deactivate_lazy_types = set_active_lazy_types false;
  11.569 +
  11.570 +fun get_lazy_types thy = Symtab.dest (Laziness_Data.get thy) 
  11.571 +
  11.572 +fun print_lazy_type thy (name, info : lazy_info) = 
  11.573 +  let
  11.574 +    val ctxt = Proof_Context.init_global thy
  11.575 +    fun pretty_ctr ctr = 
  11.576 +      let
  11.577 +        val argsT = dest_Const ctr |> snd |> binder_types
  11.578 +      in
  11.579 +        Pretty.block [
  11.580 +          Syntax.pretty_term ctxt ctr,
  11.581 +          Pretty.brk 1,
  11.582 +          Pretty.block (Pretty.separate "" (map (Pretty.quote o Syntax.pretty_typ ctxt) argsT))
  11.583 +        ]
  11.584 +      end
  11.585 +  in
  11.586 +    Pretty.block [
  11.587 +      Pretty.str (name ^ (if #active info then "" else " (inactive)") ^ ":"),
  11.588 +      Pretty.brk 1,
  11.589 +      Pretty.block [
  11.590 +        Syntax.pretty_typ ctxt (#eagerT info),
  11.591 +        Pretty.brk 1,
  11.592 +        Pretty.str "=",
  11.593 +        Pretty.brk 1,
  11.594 +        Syntax.pretty_term ctxt (#ctr info),
  11.595 +        Pretty.brk 1,
  11.596 +        Pretty.block [
  11.597 +          Pretty.str "(",
  11.598 +          Syntax.pretty_term ctxt (#destr info),
  11.599 +          Pretty.str ":",
  11.600 +          Pretty.brk 1,
  11.601 +          Syntax.pretty_typ ctxt (Type (@{type_name lazy}, [#lazyT info])),
  11.602 +          Pretty.str ")"
  11.603 +        ]
  11.604 +      ],
  11.605 +      Pretty.fbrk,
  11.606 +      Pretty.keyword2 "and",
  11.607 +      Pretty.brk 1,
  11.608 +      Pretty.block ([
  11.609 +        Syntax.pretty_typ ctxt (#lazyT info),
  11.610 +        Pretty.brk 1,
  11.611 +        Pretty.str "=",
  11.612 +        Pretty.brk 1] @
  11.613 +        Pretty.separate " |" (map pretty_ctr (#lazy_ctrs info)) @ [
  11.614 +        Pretty.fbrk,
  11.615 +        Pretty.keyword2 "for",
  11.616 +        Pretty.brk 1, 
  11.617 +        Pretty.str "case:",
  11.618 +        Pretty.brk 1,
  11.619 +        Syntax.pretty_term ctxt (#case_lazy info)
  11.620 +      ])
  11.621 +    ]
  11.622 +  end;
  11.623 +
  11.624 +fun print_lazy_types thy = 
  11.625 +  let
  11.626 +    fun cmp ((name1, _), (name2, _)) = string_ord (name1, name2)
  11.627 +    val infos = Laziness_Data.get thy |> Symtab.dest |> map (apfst Long_Name.base_name) |> sort cmp
  11.628 +  in
  11.629 +    Pretty.writeln_chunks (map (print_lazy_type thy) infos)
  11.630 +  end;
  11.631 +
  11.632 +
  11.633 +val _ =
  11.634 +  Outer_Syntax.command @{command_keyword code_lazy_type}
  11.635 +    "make a lazy copy of the datatype and activate substitution"
  11.636 +    (Parse.binding >> (fn b => Toplevel.theory (Binding.name_of b |> code_lazy_type)));
  11.637 +val _ =
  11.638 +  Outer_Syntax.command @{command_keyword activate_lazy_type}
  11.639 +    "activate substitution on a specific (lazy) type"
  11.640 +    (Parse.binding >> (fn b => Toplevel.theory (Binding.name_of b |> activate_lazy_type)));
  11.641 +val _ =
  11.642 +  Outer_Syntax.command @{command_keyword deactivate_lazy_type}
  11.643 +    "deactivate substitution on a specific (lazy) type"
  11.644 +    (Parse.binding >> (fn b => Toplevel.theory (Binding.name_of b |> deactivate_lazy_type)));
  11.645 +val _ =
  11.646 +  Outer_Syntax.command @{command_keyword activate_lazy_types}
  11.647 +    "activate substitution on all (lazy) types"
  11.648 +    (pair (Toplevel.theory activate_lazy_types));
  11.649 +val _ =
  11.650 +  Outer_Syntax.command @{command_keyword deactivate_lazy_types}
  11.651 +    "deactivate substitution on all (lazy) type"
  11.652 +    (pair (Toplevel.theory deactivate_lazy_types));
  11.653 +val _ =
  11.654 +  Outer_Syntax.command @{command_keyword print_lazy_types}
  11.655 +    "print the types that have been declared as lazy and their substitution state"
  11.656 +    (pair (Toplevel.theory (tap print_lazy_types)));
  11.657 +
  11.658 +end
  11.659 \ No newline at end of file
    12.1 --- a/src/HOL/Library/document/root.bib	Fri May 11 22:59:00 2018 +0200
    12.2 +++ b/src/HOL/Library/document/root.bib	Sat May 12 11:24:11 2018 +0200
    12.3 @@ -52,3 +52,10 @@
    12.4    year		= 1993,
    12.5    publisher	= {Springer},
    12.6    series	= {LNCS 664}}
    12.7 +
    12.8 +@InProceedings{LochbihlerStoop2018,
    12.9 +  author = {Andreas Lochbihler and Pascal Stoop},
   12.10 +  title = {Lazy Algebraic Types in {Isabelle/HOL}},
   12.11 +  booktitle = {Isabelle Workshop 2018},
   12.12 +  year = 2018,
   12.13 +}
   12.14 \ No newline at end of file
    13.1 --- a/src/HOL/ROOT	Fri May 11 22:59:00 2018 +0200
    13.2 +++ b/src/HOL/ROOT	Sat May 12 11:24:11 2018 +0200
    13.3 @@ -247,6 +247,7 @@
    13.4      Generate_Binary_Nat
    13.5      Generate_Target_Nat
    13.6      Generate_Efficient_Datastructures
    13.7 +    Code_Lazy_Test
    13.8      Code_Test_PolyML
    13.9      Code_Test_Scala
   13.10    theories [condition = ISABELLE_GHC]