# HG changeset patch # User Andreas Lochbihler # Date 1526117051 -7200 # Node ID 8b50f29a1992566b9503b2740f40e3d6a05edb9c # Parent 42d63ea3916165c657c30b8b2f7a43b1b09d6e1c new tool Code_Lazy diff -r 42d63ea39161 -r 8b50f29a1992 src/HOL/Codegenerator_Test/Code_Lazy_Test.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Codegenerator_Test/Code_Lazy_Test.thy Sat May 12 11:24:11 2018 +0200 @@ -0,0 +1,192 @@ +(* Author: Andreas Lochbihler, Digital Asset *) + +section \Laziness tests\ + +theory Code_Lazy_Test imports + "HOL-Library.Code_Lazy" + "HOL-Library.Stream" + "HOL-Library.Code_Test" + "HOL-Library.BNF_Corec" +begin + +subsection \Linear codatatype\ + +code_lazy_type stream + +value [code] "cycle ''ab''" +value [code] "let x = cycle ''ab''; y = snth x 10 in x" + +datatype 'a llist = LNil ("\<^bold>[\<^bold>]") | LCons (lhd: 'a) (ltl: "'a llist") (infixr "\<^bold>#" 65) + +subsection \Finite lazy lists\ + +code_lazy_type llist + +no_notation lazy_llist ("_") +syntax "_llist" :: "args => 'a list" ("\<^bold>[(_)\<^bold>]") +translations + "\<^bold>[x, xs\<^bold>]" == "x\<^bold>#\<^bold>[xs\<^bold>]" + "\<^bold>[x\<^bold>]" == "x\<^bold>#\<^bold>[\<^bold>]" + "\<^bold>[x\<^bold>]" == "CONST lazy_llist x" + +definition llist :: "nat llist" where + "llist = \<^bold>[1, 2, 3, hd [], 4\<^bold>]" + +fun lnth :: "nat \ 'a llist \ 'a" where + "lnth 0 (x \<^bold># xs) = x" +| "lnth (Suc n) (x \<^bold># xs) = lnth n xs" + +value [code] "llist" +value [code] "let x = lnth 2 llist in (x, llist)" +value [code] "llist" + +fun lfilter :: "('a \ bool) \ 'a llist \ 'a llist" where + "lfilter P \<^bold>[\<^bold>] = \<^bold>[\<^bold>]" +| "lfilter P (x \<^bold># xs) = (if P x then x \<^bold># lfilter P xs else lfilter P xs)" + +value [code] "lhd (lfilter odd llist)" + +definition lfilter_test :: "nat llist \ _" where "lfilter_test xs = lhd (lfilter even xs)" + \ \Filtering @{term llist} for @{term even} fails because only the datatype is lazy, not the + filter function itself.\ +ML_val \ (@{code lfilter_test} @{code llist}; raise Fail "Failure expected") handle Match => () \ + +subsection \Records as free type\ + +record ('a, 'b) rec = + rec1 :: 'a + rec2 :: 'b + +free_constructors rec_ext for rec.rec_ext + subgoal by(rule rec.cases_scheme) + subgoal by(rule rec.ext_inject) + done + +code_lazy_type rec_ext + +definition rec_test1 where "rec_test1 = rec1 (\rec1 = Suc 5, rec2 = True\\rec1 := 0\)" +definition rec_test2 :: "(bool, bool) rec" where "rec_test2 = \rec1 = hd [], rec2 = True\" +test_code "rec_test1 = 0" in PolyML Scala +value [code] "rec_test2" + +subsection \Branching codatatypes\ + +codatatype tree = L | Node tree tree (infix "\" 900) + +code_lazy_type tree + +fun mk_tree :: "nat \ tree" where + mk_tree_0: "mk_tree 0 = L" +| "mk_tree (Suc n) = (let t = mk_tree n in t \ t)" + +function subtree :: "bool list \ tree \ tree" where + "subtree [] t = t" +| "subtree (True # p) (l \ r) = subtree p l" +| "subtree (False # p) (l \ r) = subtree p r" +| "subtree _ L = L" + by pat_completeness auto +termination by lexicographic_order + +value [code] "mk_tree 10" +value [code] "let t = mk_tree 10; _ = subtree [True, True, False, False] t in t" + +lemma mk_tree_Suc: "mk_tree (Suc n) = mk_tree n \ mk_tree n" + by(simp add: Let_def) +lemmas [code] = mk_tree_0 mk_tree_Suc +value [code] "let t = mk_tree 10; _ = subtree [True, True, False, False] t in t" +value [code] "let t = mk_tree 4; _ = subtree [True, True, False, False] t in t" + +subsection \Corecursion\ + +corec (friend) plus :: "'a :: plus stream \ 'a stream \ 'a stream" where + "plus xs ys = (shd xs + shd ys) ## plus (stl xs) (stl ys)" + +corec (friend) times :: "'a :: {plus, times} stream \ 'a stream \ 'a stream" where + "times xs ys = (shd xs * shd ys) ## plus (times (stl xs) ys) (times xs (stl ys))" + +subsection \Pattern-matching tests\ + +definition f1 :: "bool \ bool \ bool \ nat llist \ unit" where + "f1 _ _ _ _ = ()" + +declare [[code drop: f1]] +lemma f1_code1 [code]: + "f1 b c d ns = Code.abort (STR ''4'') (\_. ())" + "f1 b c True \<^bold>[n, m\<^bold>] = Code.abort (STR ''3'') (\_. ())" + "f1 b True d \<^bold>[n\<^bold>] = Code.abort (STR ''2'') (\_. ())" + "f1 True c d \<^bold>[\<^bold>] = ()" + by(simp_all add: f1_def) + +value [code] "f1 True False False \<^bold>[\<^bold>]" +deactivate_lazy_type llist +value [code] "f1 True False False \<^bold>[\<^bold>]" +declare f1_code1(1) [code del] +value [code] "f1 True False False \<^bold>[\<^bold>]" +activate_lazy_type llist +value [code] "f1 True False False \<^bold>[\<^bold>]" + +declare [[code drop: f1]] +lemma f1_code2 [code]: + "f1 b c d ns = Code.abort (STR ''4'') (\_. ())" + "f1 b c True \<^bold>[n, m\<^bold>] = Code.abort (STR ''3'') (\_. ())" + "f1 b True d \<^bold>[n\<^bold>] = ()" + "f1 True c d \<^bold>[\<^bold>] = Code.abort (STR ''1'') (\_. ())" + by(simp_all add: f1_def) + +value [code] "f1 True True True \<^bold>[0\<^bold>]" +declare f1_code2(1)[code del] +value [code] "f1 True True True \<^bold>[0\<^bold>]" + +declare [[code drop: f1]] +lemma f1_code3 [code]: + "f1 b c d ns = Code.abort (STR ''4'') (\_. ())" + "f1 b c True \<^bold>[n, m\<^bold>] = ()" + "f1 b True d \<^bold>[n\<^bold>] = Code.abort (STR ''2'') (\_. ())" + "f1 True c d \<^bold>[\<^bold>] = Code.abort (STR ''1'') (\_. ())" + by(simp_all add: f1_def) + +value [code] "f1 True True True \<^bold>[0, 1\<^bold>]" +declare f1_code3(1)[code del] +value [code] "f1 True True True \<^bold>[0, 1\<^bold>]" + +declare [[code drop: f1]] +lemma f1_code4 [code]: + "f1 b c d ns = ()" + "f1 b c True \<^bold>[n, m\<^bold>] = Code.abort (STR ''3'') (\_. ())" + "f1 b True d \<^bold>[n\<^bold>] = Code.abort (STR ''2'') (\_. ())" + "f1 True c d \<^bold>[\<^bold>] = Code.abort (STR ''1'') (\_. ())" + by(simp_all add: f1_def) + +value [code] "f1 True True True \<^bold>[0, 1, 2\<^bold>]" +value [code] "f1 True True False \<^bold>[0, 1\<^bold>]" +value [code] "f1 True False True \<^bold>[0\<^bold>]" +value [code] "f1 False True True \<^bold>[\<^bold>]" + +definition f2 :: "nat llist llist list \ unit" where "f2 _ = ()" + +declare [[code drop: f2]] +lemma f2_code1 [code]: + "f2 xs = Code.abort (STR ''a'') (\_. ())" + "f2 [\<^bold>[\<^bold>[\<^bold>]\<^bold>]] = ()" + "f2 [\<^bold>[\<^bold>[Suc n\<^bold>]\<^bold>]] = ()" + "f2 [\<^bold>[\<^bold>[0, Suc n\<^bold>]\<^bold>]] = ()" + by(simp_all add: f2_def) + +value [code] "f2 [\<^bold>[\<^bold>[\<^bold>]\<^bold>]]" +value [code] "f2 [\<^bold>[\<^bold>[4\<^bold>]\<^bold>]]" +value [code] "f2 [\<^bold>[\<^bold>[0, 1\<^bold>]\<^bold>]]" +ML_val \ (@{code f2} []; error "Fail expected") handle Fail _ => () \ + +definition f3 :: "nat set llist \ unit" where "f3 _ = ()" + +declare [[code drop: f3]] +lemma f3_code1 [code]: + "f3 \<^bold>[\<^bold>] = ()" + "f3 \<^bold>[A\<^bold>] = ()" + by(simp_all add: f3_def) + +value [code] "f3 \<^bold>[\<^bold>]" +value [code] "f3 \<^bold>[{}\<^bold>]" +value [code] "f3 \<^bold>[UNIV\<^bold>]" + +end \ No newline at end of file diff -r 42d63ea39161 -r 8b50f29a1992 src/HOL/Codegenerator_Test/Code_Test_GHC.thy --- a/src/HOL/Codegenerator_Test/Code_Test_GHC.thy Fri May 11 22:59:00 2018 +0200 +++ b/src/HOL/Codegenerator_Test/Code_Test_GHC.thy Sat May 12 11:24:11 2018 +0200 @@ -4,7 +4,7 @@ Test case for test_code on GHC *) -theory Code_Test_GHC imports "HOL-Library.Code_Test" begin +theory Code_Test_GHC imports "HOL-Library.Code_Test" Code_Lazy_Test begin test_code "(14 + 7 * -12 :: integer) = 140 div -2" in GHC @@ -20,4 +20,6 @@ "gcd 0 0 = (0 :: integer)" in GHC +test_code "stake 10 (cycle ''ab'') = ''ababababab''" in GHC + end diff -r 42d63ea39161 -r 8b50f29a1992 src/HOL/Codegenerator_Test/Code_Test_MLton.thy --- a/src/HOL/Codegenerator_Test/Code_Test_MLton.thy Fri May 11 22:59:00 2018 +0200 +++ b/src/HOL/Codegenerator_Test/Code_Test_MLton.thy Sat May 12 11:24:11 2018 +0200 @@ -4,10 +4,12 @@ Test case for test_code on MLton *) -theory Code_Test_MLton imports "HOL-Library.Code_Test" begin +theory Code_Test_MLton imports "HOL-Library.Code_Test" Code_Lazy_Test begin test_code "14 + 7 * -12 = (140 div -2 :: integer)" in MLton value [MLton] "14 + 7 * -12 :: integer" +test_code "stake 10 (cycle ''ab'') = ''ababababab''" in MLton + end diff -r 42d63ea39161 -r 8b50f29a1992 src/HOL/Codegenerator_Test/Code_Test_OCaml.thy --- a/src/HOL/Codegenerator_Test/Code_Test_OCaml.thy Fri May 11 22:59:00 2018 +0200 +++ b/src/HOL/Codegenerator_Test/Code_Test_OCaml.thy Sat May 12 11:24:11 2018 +0200 @@ -4,7 +4,7 @@ Test case for test_code on OCaml *) -theory Code_Test_OCaml imports "HOL-Library.Code_Test" begin +theory Code_Test_OCaml imports "HOL-Library.Code_Test" Code_Lazy_Test begin test_code "14 + 7 * -12 = (140 div -2 :: integer)" in OCaml @@ -20,4 +20,6 @@ "gcd 0 0 = (0 :: integer)" in OCaml +test_code "stake 10 (cycle ''ab'') = ''ababababab''" in OCaml + end diff -r 42d63ea39161 -r 8b50f29a1992 src/HOL/Codegenerator_Test/Code_Test_PolyML.thy --- a/src/HOL/Codegenerator_Test/Code_Test_PolyML.thy Fri May 11 22:59:00 2018 +0200 +++ b/src/HOL/Codegenerator_Test/Code_Test_PolyML.thy Sat May 12 11:24:11 2018 +0200 @@ -4,10 +4,12 @@ Test case for test_code on PolyML *) -theory Code_Test_PolyML imports "HOL-Library.Code_Test" begin +theory Code_Test_PolyML imports "HOL-Library.Code_Test" Code_Lazy_Test begin test_code "14 + 7 * -12 = (140 div -2 :: integer)" in PolyML value [PolyML] "14 + 7 * -12 :: integer" +test_code "stake 10 (cycle ''ab'') = ''ababababab''" in PolyML + end diff -r 42d63ea39161 -r 8b50f29a1992 src/HOL/Codegenerator_Test/Code_Test_SMLNJ.thy --- a/src/HOL/Codegenerator_Test/Code_Test_SMLNJ.thy Fri May 11 22:59:00 2018 +0200 +++ b/src/HOL/Codegenerator_Test/Code_Test_SMLNJ.thy Sat May 12 11:24:11 2018 +0200 @@ -4,10 +4,12 @@ Test case for test_code on SMLNJ *) -theory Code_Test_SMLNJ imports "HOL-Library.Code_Test" begin +theory Code_Test_SMLNJ imports "HOL-Library.Code_Test" Code_Lazy_Test begin test_code "14 + 7 * -12 = (140 div -2 :: integer)" in SMLNJ value [SMLNJ] "14 + 7 * -12 :: integer" +test_code "stake 10 (cycle ''ab'') = ''ababababab''" in SMLNJ + end diff -r 42d63ea39161 -r 8b50f29a1992 src/HOL/Codegenerator_Test/Code_Test_Scala.thy --- a/src/HOL/Codegenerator_Test/Code_Test_Scala.thy Fri May 11 22:59:00 2018 +0200 +++ b/src/HOL/Codegenerator_Test/Code_Test_Scala.thy Sat May 12 11:24:11 2018 +0200 @@ -4,7 +4,7 @@ Test case for test_code on Scala *) -theory Code_Test_Scala imports "HOL-Library.Code_Test" begin +theory Code_Test_Scala imports "HOL-Library.Code_Test" Code_Lazy_Test begin test_code "14 + 7 * -12 = (140 div -2 :: integer)" in Scala @@ -20,4 +20,6 @@ "gcd 0 0 = (0 :: integer)" in Scala +test_code "stake 10 (cycle ''ab'') = ''ababababab''" in Scala + end diff -r 42d63ea39161 -r 8b50f29a1992 src/HOL/Library/Code_Lazy.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Library/Code_Lazy.thy Sat May 12 11:24:11 2018 +0200 @@ -0,0 +1,251 @@ +(* Author: Pascal Stoop, ETH Zurich + Author: Andreas Lochbihler, Digital Asset *) + +section \Lazy types in generated code\ + +theory Code_Lazy +imports Main +keywords + "code_lazy_type" + "activate_lazy_type" + "deactivate_lazy_type" + "activate_lazy_types" + "deactivate_lazy_types" + "print_lazy_types" :: thy_decl +begin + +text \ + This theory and the CodeLazy tool described in @{cite "LochbihlerStoop2018"}. + + It hooks into Isabelle’s code generator such that the generated code evaluates a user-specified + set of type constructors lazily, even in target languages with eager evaluation. + The lazy type must be algebraic, i.e., values must be built from constructors and a + corresponding case operator decomposes them. Every datatype and codatatype is algebraic + and thus eligible for lazification. +\ + +subsection \Eliminating pattern matches\ + +definition missing_pattern_match :: "String.literal \ (unit \ 'a) \ 'a" where + [code del]: "missing_pattern_match m f = f ()" + +lemma missing_pattern_match_cong [cong]: + "m = m' \ missing_pattern_match m f = missing_pattern_match m' f" + by(rule arg_cong) + +lemma missing_pattern_match_code [code_unfold]: + "missing_pattern_match = Code.abort" + unfolding missing_pattern_match_def Code.abort_def .. + +ML_file "case_converter.ML" + +subsection \The type @{text lazy}\ + +typedef 'a lazy = "UNIV :: 'a set" .. +setup_lifting type_definition_lazy +lift_definition delay :: "(unit \ 'a) \ 'a lazy" is "\f. f ()" . +lift_definition force :: "'a lazy \ 'a" is "\x. x" . + +code_datatype delay +lemma force_delay [code]: "force (delay f) = f ()" by transfer(rule refl) +lemma delay_force: "delay (\_. force s) = s" by transfer(rule refl) + +text \The implementations of @{typ "_ lazy"} using language primitives cache forced values.\ + +code_printing code_module Lazy \ (SML) +\signature LAZY = +sig + type 'a lazy; + val lazy : (unit -> 'a) -> 'a lazy; + val force : 'a lazy -> 'a; + val peek : 'a lazy -> 'a option + val termify_lazy : + (string -> 'typerep -> 'term) -> + ('term -> 'term -> 'term) -> + (string -> 'typerep -> 'term -> 'term) -> + 'typerep -> ('typerep -> 'typerep -> 'typerep) -> ('typerep -> 'typerep) -> + ('a -> 'term) -> 'typerep -> 'a lazy -> 'term -> 'term; +end; + +structure Lazy : LAZY = +struct + +datatype 'a content = + Delay of unit -> 'a + | Value of 'a + | Exn of exn; + +datatype 'a lazy = Lazy of 'a content ref; + +fun lazy f = Lazy (ref (Delay f)); + +fun force (Lazy x) = case !x of + Delay f => ( + let val res = f (); val _ = x := Value res; in res end + handle exn => (x := Exn exn; raise exn)) + | Value x => x + | Exn exn => raise exn; + +fun peek (Lazy x) = case !x of + Value x => SOME x + | _ => NONE; + +fun termify_lazy const app abs unitT funT lazyT term_of T x _ = + app (const "Code_Lazy.delay" (funT (funT unitT T) (lazyT T))) + (case peek x of SOME y => abs "_" unitT (term_of y) + | _ => const "Pure.dummy_pattern" (funT unitT T)); + +end;\ +code_reserved SML Lazy + +code_printing + type_constructor lazy \ (SML) "_ Lazy.lazy" +| constant delay \ (SML) "Lazy.lazy" +| constant force \ (SML) "Lazy.force" + +code_printing \ \For code generation within the Isabelle environment, we reuse the thread-safe + implementation of lazy from @{file "~~/src/Pure/Concurrent/lazy.ML"}\ + code_module Lazy \ (Eval) \\ +| type_constructor lazy \ (Eval) "_ Lazy.lazy" +| constant delay \ (Eval) "Lazy.lazy" +| constant force \ (Eval) "Lazy.force" + +code_printing + code_module Lazy \ (Haskell) +\newtype Lazy a = Lazy a; +delay f = Lazy (f ()); +force (Lazy x) = x;\ +| type_constructor lazy \ (Haskell) "Lazy.Lazy _" +| constant delay \ (Haskell) "Lazy.delay" +| constant force \ (Haskell) "Lazy.force" +code_reserved Haskell Lazy + +code_printing + code_module Lazy \ (Scala) +\object Lazy { + final class Lazy[A] (f: Unit => A) { + var evaluated = false; + lazy val x: A = f () + + def get() : A = { + evaluated = true; + return x + } + } + + def force[A] (x: Lazy[A]) : A = { + return x.get() + } + + def delay[A] (f: Unit => A) : Lazy[A] = { + return new Lazy[A] (f) + } + + def termify_lazy[Typerep, Term, A] ( + const: String => Typerep => Term, + app: Term => Term => Term, + abs: String => Typerep => Term => Term, + unitT: Typerep, + funT: Typerep => Typerep => Typerep, + lazyT: Typerep => Typerep, + term_of: A => Term, + ty: Typerep, + x: Lazy[A], + dummy: Term) : Term = { + if (x.evaluated) + app(const("Code_Lazy.delay")(funT(funT(unitT)(ty))(lazyT(ty))))(abs("_")(unitT)(term_of(x.get))) + else + app(const("Code_Lazy.delay")(funT(funT(unitT)(ty))(lazyT(ty))))(const("Pure.dummy_pattern")(funT(unitT)(ty))) + } +}\ +| type_constructor lazy \ (Scala) "Lazy.Lazy[_]" +| constant delay \ (Scala) "Lazy.delay" +| constant force \ (Scala) "Lazy.force" +code_reserved Scala Lazy termify_lazy + +code_printing + type_constructor lazy \ (OCaml) "_ Lazy.t" +| constant delay \ (OCaml) "Lazy.from'_fun" +| constant force \ (OCaml) "Lazy.force" +code_reserved OCaml Lazy + +text \ + Term reconstruction for lazy looks into the lazy value and reconstructs it to the depth it has been evaluated. + This is not done for Haskell and Scala as we do not know of any portable way to inspect whether a lazy value + has been evaluated to or not. +\ +code_printing code_module Termify_Lazy \ (Eval) +\structure Termify_Lazy = struct +fun termify_lazy + (_: string -> typ -> term) (_: term -> term -> term) (_: string -> typ -> term -> term) + (_: typ) (_: typ -> typ -> typ) (_: typ -> typ) + (term_of: 'a -> term) (T: typ) (x: 'a Lazy.lazy) (_: term) = + Const ("Code_Lazy.delay", (HOLogic.unitT --> T) --> Type ("Code_Lazy.lazy", [T])) $ + (case Lazy.peek x of + SOME (Exn.Res x) => absdummy HOLogic.unitT (term_of x) + | _ => Const ("Pure.dummy_pattern", HOLogic.unitT --> T)); +end;\ +code_reserved Eval Termify_Lazy TERMIFY_LAZY termify_lazy + +code_printing code_module Termify_Lazy \ (OCaml) +\module Termify_Lazy : sig + val termify_lazy : + (string -> 'typerep -> 'term) -> + ('term -> 'term -> 'term) -> + (string -> 'typerep -> 'term -> 'term) -> + 'typerep -> ('typerep -> 'typerep -> 'typerep) -> ('typerep -> 'typerep) -> + ('a -> 'term) -> 'typerep -> 'a Lazy.t -> 'term -> 'term +end = struct + +let termify_lazy const app abs unitT funT lazyT term_of ty x _ = + app (const "Code_Lazy.delay" (funT (funT unitT ty) (lazyT ty))) + (if Lazy.is_val x then abs "_" unitT (term_of (Lazy.force x)) + else const "Pure.dummy_pattern" (funT unitT ty));; + +end;;\ +code_reserved OCaml Termify_Lazy termify_lazy + +definition termify_lazy2 :: "'a :: typerep lazy \ term" +where "termify_lazy2 x = + Code_Evaluation.App (Code_Evaluation.Const (STR ''Code_Lazy.delay'') (TYPEREP((unit \ 'a) \ 'a lazy))) + (Code_Evaluation.Const (STR ''Pure.dummy_pattern'') (TYPEREP((unit \ 'a))))" + +definition termify_lazy :: + "(String.literal \ 'typerep \ 'term) \ + ('term \ 'term \ 'term) \ + (String.literal \ 'typerep \ 'term \ 'term) \ + 'typerep \ ('typerep \ 'typerep \ 'typerep) \ ('typerep \ 'typerep) \ + ('a \ 'term) \ 'typerep \ 'a :: typerep lazy \ 'term \ term" +where "termify_lazy _ _ _ _ _ _ _ _ x _ = termify_lazy2 x" + +declare [[code drop: "Code_Evaluation.term_of :: _ lazy \ _"]] + +lemma term_of_lazy_code [code]: + "Code_Evaluation.term_of x \ + termify_lazy + Code_Evaluation.Const Code_Evaluation.App Code_Evaluation.Abs + TYPEREP(unit) (\T U. typerep.Typerep (STR ''fun'') [T, U]) (\T. typerep.Typerep (STR ''Code_Lazy.lazy'') [T]) + Code_Evaluation.term_of TYPEREP('a) x (Code_Evaluation.Const (STR '''') (TYPEREP(unit)))" + for x :: "'a :: {typerep, term_of} lazy" +by(rule term_of_anything) + +code_printing constant termify_lazy + \ (SML) "Lazy.termify'_lazy" + and (Eval) "Termify'_Lazy.termify'_lazy" + and (OCaml) "Termify'_Lazy.termify'_lazy" + and (Scala) "Lazy.termify'_lazy" + +text \Make evaluation with the simplifier respect @{term delay}s.\ + +lemma delay_lazy_cong: "delay f = delay f" by simp +setup \Code_Simp.map_ss (Simplifier.add_cong @{thm delay_lazy_cong})\ + +subsection \Implementation\ + +ML_file "code_lazy.ML" + +setup \ + Code_Preproc.add_functrans ("lazy_datatype", Code_Lazy.transform_code_eqs); +\ + +end diff -r 42d63ea39161 -r 8b50f29a1992 src/HOL/Library/Library.thy --- a/src/HOL/Library/Library.thy Fri May 11 22:59:00 2018 +0200 +++ b/src/HOL/Library/Library.thy Sat May 12 11:24:11 2018 +0200 @@ -10,6 +10,7 @@ Boolean_Algebra Bourbaki_Witt_Fixpoint Char_ord + Code_Lazy Code_Test Combine_PER Complete_Partial_Order2 diff -r 42d63ea39161 -r 8b50f29a1992 src/HOL/Library/case_converter.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Library/case_converter.ML Sat May 12 11:24:11 2018 +0200 @@ -0,0 +1,549 @@ +(* Author: Pascal Stoop, ETH Zurich + Author: Andreas Lochbihler, Digital Asset *) + +signature CASE_CONVERTER = +sig + val to_case: Proof.context -> (string * string -> bool) -> (string * typ -> int) -> + thm list -> thm list option +end; + +structure Case_Converter : CASE_CONVERTER = +struct + +fun lookup_remove _ _ [] = (NONE, []) + | lookup_remove eq k ((k', v) :: kvs) = + if eq (k, k') then (SOME (k', v), kvs) + else apsnd (cons (k', v)) (lookup_remove eq k kvs) + +fun map_option _ NONE = NONE + | map_option f (SOME x) = SOME (f x) + +fun mk_abort msg t = + let + val T = fastype_of t + val abort = Const (@{const_name missing_pattern_match}, HOLogic.literalT --> (HOLogic.unitT --> T) --> T) + in + abort $ HOLogic.mk_literal msg $ absdummy HOLogic.unitT t + end + +(* fold_term : (string * typ -> 'a) -> + (string * typ -> 'a) -> + (indexname * typ -> 'a) -> + (int -> 'a) -> + (string * typ * 'a -> 'a) -> + ('a * 'a -> 'a) -> + term -> + 'a *) +fun fold_term const_fun free_fun var_fun bound_fun abs_fun dollar_fun term = + let + fun go x = case x of + Const (s, T) => const_fun (s, T) + | Free (s, T) => free_fun (s, T) + | Var (i, T) => var_fun (i, T) + | Bound n => bound_fun n + | Abs (s, T, term) => abs_fun (s, T, go term) + | term1 $ term2 => dollar_fun (go term1, go term2) + in + go term + end; + +datatype term_coordinate = End of typ + | Coordinate of (string * (int * term_coordinate)) list; + +fun term_coordinate_merge (End T) _ = End T + | term_coordinate_merge _ (End T) = End T + | term_coordinate_merge (Coordinate xs) (Coordinate ys) = + let + fun merge_consts xs [] = xs + | merge_consts xs ((s1, (n, y)) :: ys) = + case List.partition (fn (s2, (m, _)) => s1 = s2 andalso n = m) xs of + ([], xs') => (s1, (n, y)) :: (merge_consts xs' ys) + | ((_, (_, x)) :: _, xs') => (s1, (n, term_coordinate_merge x y)) :: (merge_consts xs' ys) + in + Coordinate (merge_consts xs ys) + end; + +fun term_to_coordinates P term = + let + val (ctr, args) = strip_comb term + in + case ctr of Const (s, T) => + if P (body_type T |> dest_Type |> fst, s) + then SOME (End (body_type T)) + else + let + fun f (i, t) = term_to_coordinates P t |> map_option (pair i) + val tcos = map_filter I (map_index f args) + in + if null tcos then NONE + else SOME (Coordinate (map (pair s) tcos)) + end + | _ => NONE + end; + +fun coordinates_to_list (End x) = [(x, [])] + | coordinates_to_list (Coordinate xs) = + let + fun f (s, (n, xss)) = map (fn (T, xs) => (T, (s, n) :: xs)) (coordinates_to_list xss) + in flat (map f xs) end; + + +(* AL: TODO: change from term to const_name *) +fun find_ctr ctr1 xs = + let + val const_name = fst o dest_Const + fun const_equal (ctr1, ctr2) = const_name ctr1 = const_name ctr2 + in + lookup_remove const_equal ctr1 xs + end; + +datatype pattern + = Wildcard + | Value + | Split of int * (term * pattern) list * pattern; + +fun pattern_merge Wildcard pat' = pat' + | pattern_merge Value _ = Value + | pattern_merge (Split (n, xs, pat)) Wildcard = + Split (n, map (apsnd (fn pat'' => pattern_merge pat'' Wildcard)) xs, pattern_merge pat Wildcard) + | pattern_merge (Split _) Value = Value + | pattern_merge (Split (n, xs, pat)) (Split (m, ys, pat'')) = + let + fun merge_consts xs [] = map (apsnd (fn pat => pattern_merge pat Wildcard)) xs + | merge_consts xs ((ctr, y) :: ys) = + (case find_ctr ctr xs of + (SOME (ctr, x), xs) => (ctr, pattern_merge x y) :: merge_consts xs ys + | (NONE, xs) => (ctr, y) :: merge_consts xs ys + ) + in + Split (if n <= 0 then m else n, merge_consts xs ys, pattern_merge pat pat'') + end + +fun pattern_intersect Wildcard _ = Wildcard + | pattern_intersect Value pat2 = pat2 + | pattern_intersect (Split _) Wildcard = Wildcard + | pattern_intersect (Split (n, xs', pat1)) Value = + Split (n, + map (apsnd (fn pat1 => pattern_intersect pat1 Value)) xs', + pattern_intersect pat1 Value) + | pattern_intersect (Split (n, xs', pat1)) (Split (m, ys, pat2)) = + Split (if n <= 0 then m else n, + intersect_consts xs' ys pat1 pat2, + pattern_intersect pat1 pat2) +and + intersect_consts xs [] _ default2 = map (apsnd (fn pat => pattern_intersect pat default2)) xs + | intersect_consts xs ((ctr, pat2) :: ys) default1 default2 = case find_ctr ctr xs of + (SOME (ctr, pat1), xs') => + (ctr, pattern_merge (pattern_merge (pattern_intersect pat1 pat2) (pattern_intersect default1 pat2)) + (pattern_intersect pat1 default2)) :: + intersect_consts xs' ys default1 default2 + | (NONE, xs') => (ctr, pattern_intersect default1 pat2) :: (intersect_consts xs' ys default1 default2) + +fun pattern_lookup _ Wildcard = Wildcard + | pattern_lookup _ Value = Value + | pattern_lookup [] (Split (n, xs, pat)) = + Split (n, map (apsnd (pattern_lookup [])) xs, pattern_lookup [] pat) + | pattern_lookup (term :: terms) (Split (n, xs, pat)) = + let + val (ctr, args) = strip_comb term + fun map_ctr (term, pat) = + let + val args = term |> dest_Const |> snd |> binder_types |> map (fn T => Free ("x", T)) + in + pattern_lookup args pat + end + in + if is_Const ctr then + case find_ctr ctr xs of (SOME (_, pat'), _) => + pattern_lookup terms (pattern_merge (pattern_lookup args pat') (pattern_lookup [] pat)) + | (NONE, _) => pattern_lookup terms pat + else if length xs < n orelse n <= 0 then + pattern_lookup terms pat + else pattern_lookup terms + (pattern_merge + (fold pattern_intersect (map map_ctr (tl xs)) (map_ctr (hd xs))) + (pattern_lookup [] pat)) + end; + +fun pattern_contains terms pat = case pattern_lookup terms pat of + Wildcard => false + | Value => true + | Split _ => raise Match; + +fun pattern_create _ [] = Wildcard + | pattern_create ctr_count (term :: terms) = + let + val (ctr, args) = strip_comb term + in + if is_Const ctr then + Split (ctr_count ctr, [(ctr, pattern_create ctr_count (args @ terms))], Wildcard) + else Split (0, [], pattern_create ctr_count terms) + end; + +fun pattern_insert ctr_count terms pat = + let + fun new_pattern terms = pattern_insert ctr_count terms (pattern_create ctr_count terms) + fun aux _ false Wildcard = Wildcard + | aux terms true Wildcard = if null terms then Value else new_pattern terms + | aux _ _ Value = Value + | aux terms modify (Split (n, xs', pat)) = + let + val unmodified = (n, map (apsnd (aux [] false)) xs', aux [] false pat) + in case terms of [] => Split unmodified + | term :: terms => + let + val (ctr, args) = strip_comb term + val (m, ys, pat') = unmodified + in + if is_Const ctr + then case find_ctr ctr xs' of + (SOME (ctr, pat''), xs) => + Split (m, (ctr, aux (args @ terms) modify pat'') :: map (apsnd (aux [] false)) xs, pat') + | (NONE, _) => if modify + then if m <= 0 + then Split (ctr_count ctr, (ctr, new_pattern (args @ terms)) :: ys, pat') + else Split (m, (ctr, new_pattern (args @ terms)) :: ys, pat') + else Split unmodified + else Split (m, ys, aux terms modify pat) + end + end + in + aux terms true pat + end; + +val pattern_empty = Wildcard; + +fun replace_frees lhss rhss typ_list ctxt = + let + fun replace_frees_once (lhs, rhs) ctxt = + let + val add_frees_list = fold_rev Term.add_frees + val frees = add_frees_list lhs [] + val (new_frees, ctxt1) = (Ctr_Sugar_Util.mk_Frees "x" (map snd frees) ctxt) + val (new_frees1, ctxt2) = + let + val (dest_frees, types) = split_list (map dest_Free new_frees) + val (new_frees, ctxt2) = Variable.variant_fixes dest_frees ctxt1 + in + (map Free (new_frees ~~ types), ctxt2) + end + val dict = frees ~~ new_frees1 + fun free_map_fun (s, T) = + case AList.lookup (op =) dict (s, T) of + NONE => Free (s, T) + | SOME x => x + val map_fun = fold_term Const free_map_fun Var Bound Abs (op $) + in + ((map map_fun lhs, map_fun rhs), ctxt2) + end + + fun variant_fixes (def_frees, ctxt) = + let + val (dest_frees, types) = split_list (map dest_Free def_frees) + val (def_frees, ctxt1) = Variable.variant_fixes dest_frees ctxt + in + (map Free (def_frees ~~ types), ctxt1) + end + val (def_frees, ctxt1) = variant_fixes (Ctr_Sugar_Util.mk_Frees "x" typ_list ctxt) + val (rhs_frees, ctxt2) = variant_fixes (Ctr_Sugar_Util.mk_Frees "x" typ_list ctxt1) + val (case_args, ctxt3) = variant_fixes (Ctr_Sugar_Util.mk_Frees "x" + (map fastype_of (hd lhss)) ctxt2) + val (new_terms1, ctxt4) = fold_map replace_frees_once (lhss ~~ rhss) ctxt3 + val (lhss1, rhss1) = split_list new_terms1 + in + (lhss1, rhss1, def_frees ~~ rhs_frees, case_args, ctxt4) + end; + +fun add_names_in_type (Type (name, Ts)) = + List.foldr (op o) (Symtab.update (name, ())) (map add_names_in_type Ts) + | add_names_in_type (TFree _) = I + | add_names_in_type (TVar _) = I + +fun add_names_in_term (Const (_, T)) = add_names_in_type T + | add_names_in_term (Free (_, T)) = add_names_in_type T + | add_names_in_term (Var (_, T)) = add_names_in_type T + | add_names_in_term (Bound _) = I + | add_names_in_term (Abs (_, T, body)) = + add_names_in_type T o add_names_in_term body + | add_names_in_term (t1 $ t2) = add_names_in_term t1 o add_names_in_term t2 + +fun add_type_names terms = + fold (fn term => fn f => add_names_in_term term o f) terms I + +fun get_split_theorems ctxt = + Symtab.keys + #> map_filter (Ctr_Sugar.ctr_sugar_of ctxt) + #> map #split; + +fun match (Const (s1, _)) (Const (s2, _)) = if s1 = s2 then SOME I else NONE + | match (Free y) x = SOME (fn z => if z = Free y then x else z) + | match (pat1 $ pattern2) (t1 $ t2) = + (case (match pat1 t1, match pattern2 t2) of + (SOME f, SOME g) => SOME (f o g) + | _ => NONE + ) + | match _ _ = NONE; + +fun match_all patterns terms = + let + fun combine _ NONE = NONE + | combine (f_opt, f_opt') (SOME g) = + case match f_opt f_opt' of SOME f => SOME (f o g) | _ => NONE + in + fold_rev combine (patterns ~~ terms) (SOME I) + end + +fun matches (Const (s1, _)) (Const (s2, _)) = s1 = s2 + | matches (Free _) _ = true + | matches (pat1 $ pat2) (t1 $ t2) = matches pat1 t1 andalso matches pat2 t2 + | matches _ _ = false; +fun matches_all patterns terms = forall (uncurry matches) (patterns ~~ terms) + +fun terms_to_case_at ctr_count ctxt (fun_t : term) (default_lhs : term list) + (pos, (lazy_case_arg, rhs_free)) + ((lhss : term list list), (rhss : term list), type_name_fun) = + let + fun abort t = + let + val fun_name = head_of t |> dest_Const |> fst + val msg = "Missing pattern in " ^ fun_name ^ "." + in + mk_abort msg t + end; + + (* Step 1 : Eliminate lazy pattern *) + fun replace_pat_at (n, tcos) pat pats = + let + fun map_at _ _ [] = raise Empty + | map_at n f (x :: xs) = if n > 0 + then apfst (cons x) (map_at (n - 1) f xs) + else apfst (fn x => x :: xs) (f x) + fun replace [] pat term = (pat, term) + | replace ((s1, n) :: tcos) pat term = + let + val (ctr, args) = strip_comb term + in + case ctr of Const (s2, _) => + if s1 = s2 + then apfst (pair ctr #> list_comb) (map_at n (replace tcos pat) args) + else (term, rhs_free) + | _ => (term, rhs_free) + end + val (part1, (old_pat, part2)) = chop n pats ||> (fn xs => (hd xs, tl xs)) + val (new_pat, old_pat1) = replace tcos pat old_pat + in + (part1 @ [new_pat] @ part2, old_pat1) + end + val (lhss1, lazy_pats) = map (replace_pat_at pos lazy_case_arg) lhss + |> split_list + + (* Step 2 : Split patterns *) + fun split equs = + let + fun merge_pattern (Const (s1, T1), Const (s2, _)) = + if s1 = s2 then SOME (Const (s1, T1)) else NONE + | merge_pattern (t, Free _) = SOME t + | merge_pattern (Free _, t) = SOME t + | merge_pattern (t1l $ t1r, t2l $ t2r) = + (case (merge_pattern (t1l, t2l), merge_pattern (t1r, t2r)) of + (SOME t1, SOME t2) => SOME (t1 $ t2) + | _ => NONE) + | merge_pattern _ = NONE + fun merge_patterns pats1 pats2 = case (pats1, pats2) of + ([], []) => SOME [] + | (x :: xs, y :: ys) => + (case (merge_pattern (x, y), merge_patterns xs ys) of + (SOME x, SOME xs) => SOME (x :: xs) + | _ => NONE + ) + | _ => raise Match + fun merge_insert ((lhs1, case_pat), _) [] = + [(lhs1, pattern_empty |> pattern_insert ctr_count [case_pat])] + | merge_insert ((lhs1, case_pat), rhs) ((lhs2, pat) :: pats) = + let + val pats = merge_insert ((lhs1, case_pat), rhs) pats + val (first_equ_needed, new_lhs) = case merge_patterns lhs1 lhs2 of + SOME new_lhs => (not (pattern_contains [case_pat] pat), new_lhs) + | NONE => (false, lhs2) + val second_equ_needed = not (matches_all lhs1 lhs2) + orelse not first_equ_needed + val first_equ = if first_equ_needed + then [(new_lhs, pattern_insert ctr_count [case_pat] pat)] + else [] + val second_equ = if second_equ_needed + then [(lhs2, pat)] + else [] + in + first_equ @ second_equ @ pats + end + in + (fold merge_insert equs [] + |> split_list + |> fst) @ [default_lhs] + end + val lhss2 = split ((lhss1 ~~ lazy_pats) ~~ rhss) + + (* Step 3 : Remove redundant patterns *) + fun remove_redundant_lhs lhss = + let + fun f lhs pat = if pattern_contains lhs pat + then ((lhs, false), pat) + else ((lhs, true), pattern_insert ctr_count lhs pat) + in + fold_map f lhss pattern_empty + |> fst + |> filter snd + |> map fst + end + fun remove_redundant_rhs rhss = + let + fun f (lhs, rhs) pat = if pattern_contains [lhs] pat + then (((lhs, rhs), false), pat) + else (((lhs, rhs), true), pattern_insert ctr_count [lhs] pat) + in + map fst (filter snd (fold_map f rhss pattern_empty |> fst)) + end + val lhss3 = remove_redundant_lhs lhss2 + + (* Step 4 : Compute right hand side *) + fun subs_fun f = fold_term + Const + (f o Free) + Var + Bound + Abs + (fn (x, y) => f x $ f y) + fun find_rhss lhs = + let + fun f (lhs1, (pat, rhs)) = + case match_all lhs1 lhs of NONE => NONE + | SOME f => SOME (pat, subs_fun f rhs) + in + remove_redundant_rhs + (map_filter f (lhss1 ~~ (lazy_pats ~~ rhss)) @ + [(lazy_case_arg, list_comb (fun_t, lhs) |> abort)] + ) + end + + (* Step 5 : make_case of right hand side *) + fun make_case ctxt case_arg cases = case cases of + [(Free x, rhs)] => subs_fun (fn y => if y = Free x then case_arg else y) rhs + | _ => Case_Translation.make_case + ctxt + Case_Translation.Warning + Name.context + case_arg + cases + val type_name_fun = add_type_names lazy_pats o type_name_fun + val rhss3 = map ((make_case ctxt lazy_case_arg) o find_rhss) lhss3 + in + (lhss3, rhss3, type_name_fun) + end; + +fun terms_to_case ctxt ctr_count (head : term) (lhss : term list list) + (rhss : term list) (typ_list : typ list) (poss : (int * (string * int) list) list) = + let + val (lhss1, rhss1, def_frees, case_args, ctxt1) = replace_frees lhss rhss typ_list ctxt + val exec_list = poss ~~ def_frees + val (lhss2, rhss2, type_name_fun) = fold_rev + (terms_to_case_at ctr_count ctxt1 head case_args) exec_list (lhss1, rhss1, I) + fun make_eq_term (lhss, rhs) = (list_comb (head, lhss), rhs) + |> HOLogic.mk_eq + |> HOLogic.mk_Trueprop + in + (map make_eq_term (lhss2 ~~ rhss2), + get_split_theorems ctxt1 (type_name_fun Symtab.empty), + ctxt1) + end; + +fun build_case_t replace_ctr ctr_count head lhss rhss ctxt = + let + val num_eqs = length lhss + val _ = if length rhss = num_eqs andalso num_eqs > 0 then () + else raise Fail + ("expected same number of left-hand sides as right-hand sides\n" + ^ "and at least one equation") + val n = length (hd lhss) + val _ = if forall (fn m => length m = n) lhss then () + else raise Fail "expected equal number of arguments" + + fun to_coordinates (n, ts) = case map_filter (term_to_coordinates replace_ctr) ts of + [] => NONE + | (tco :: tcos) => SOME (n, fold term_coordinate_merge tcos tco |> coordinates_to_list) + fun add_T (n, xss) = map (fn (T, xs) => (T, (n, xs))) xss + val (typ_list, poss) = lhss + |> Ctr_Sugar_Util.transpose + |> map_index to_coordinates + |> map_filter (map_option add_T) + |> flat + |> split_list + in + if null poss then ([], [], ctxt) + else terms_to_case ctxt (dest_Const #> ctr_count) head lhss rhss typ_list poss + end; + +fun tac ctxt {splits, intros, defs} = + let + val split_and_subst = + split_tac ctxt splits + THEN' REPEAT_ALL_NEW ( + resolve_tac ctxt [@{thm conjI}, @{thm allI}] + ORELSE' + (resolve_tac ctxt [@{thm impI}] THEN' hyp_subst_tac_thin true ctxt)) + in + (REPEAT_ALL_NEW split_and_subst ORELSE' K all_tac) + THEN' (K (Local_Defs.unfold_tac ctxt [@{thm missing_pattern_match_def}])) + THEN' (K (Local_Defs.unfold_tac ctxt defs)) + THEN_ALL_NEW (SOLVED' (resolve_tac ctxt (@{thm refl} :: intros))) + end; + +fun to_case _ _ _ [] = NONE + | to_case ctxt replace_ctr ctr_count ths = + let + val strip_eq = Thm.prop_of #> HOLogic.dest_Trueprop #> HOLogic.dest_eq + fun import [] ctxt = ([], ctxt) + | import (thm :: thms) ctxt = + let + val fun_ct = strip_eq #> fst #> head_of #> Logic.mk_term #> Thm.cterm_of ctxt + val ct = fun_ct thm + val cts = map fun_ct thms + val pairs = map (fn s => (s,ct)) cts + val thms' = map (fn (th,p) => Thm.instantiate (Thm.match p) th) (thms ~~ pairs) + in + Variable.import true (thm :: thms') ctxt |> apfst snd + end + + val (iths, ctxt') = import ths ctxt + val head = hd iths |> strip_eq |> fst |> head_of + val eqs = map (strip_eq #> apfst (snd o strip_comb)) iths + + fun hide_rhs ((pat, rhs), name) lthy = + let + val frees = fold Term.add_frees pat [] + val abs_rhs = fold absfree frees rhs + val (f, def, lthy') = case lthy + |> Local_Defs.define [((Binding.name name, NoSyn), (Binding.empty_atts, abs_rhs))] of + ([(f, (_, def))], lthy') => (f, def, lthy') + | _ => raise Match + in + ((list_comb (f, map Free (rev frees)), def), lthy') + end + + val rhs_names = Name.invent (Variable.names_of ctxt') "rhs" (length eqs) + val ((def_ts, def_thms), ctxt2) = + fold_map hide_rhs (eqs ~~ rhs_names) ctxt' |> apfst split_list + val (ts, split_thms, ctxt3) = build_case_t replace_ctr ctr_count head + (map fst eqs) def_ts ctxt2 + fun mk_thm t = Goal.prove ctxt3 [] [] t + (fn {context=ctxt, ...} => tac ctxt {splits=split_thms, intros=ths, defs=def_thms} 1) + in + if null ts then NONE + else + ts + |> map mk_thm + |> Proof_Context.export ctxt3 ctxt + |> map (Goal.norm_result ctxt) + |> SOME + end; + +end diff -r 42d63ea39161 -r 8b50f29a1992 src/HOL/Library/code_lazy.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Library/code_lazy.ML Sat May 12 11:24:11 2018 +0200 @@ -0,0 +1,655 @@ +(* Author: Pascal Stoop, ETH Zurich + Author: Andreas Lochbihler, Digital Asset *) + +signature CODE_LAZY = +sig + type lazy_info = + {eagerT: typ, + lazyT: typ, + ctr: term, + destr: term, + lazy_ctrs: term list, + case_lazy: term, + active: bool, + activate: theory -> theory, + deactivate: theory -> theory}; + val code_lazy_type: string -> theory -> theory + val activate_lazy_type: string -> theory -> theory + val deactivate_lazy_type: string -> theory -> theory + val activate_lazy_types: theory -> theory + val deactivate_lazy_types: theory -> theory + + val get_lazy_types: theory -> (string * lazy_info) list + + val print_lazy_types: theory -> unit + + val transform_code_eqs: Proof.context -> (thm * bool) list -> (thm * bool) list option +end; + +structure Code_Lazy : CODE_LAZY = +struct + +type lazy_info = + {eagerT: typ, + lazyT: typ, + ctr: term, + destr: term, + lazy_ctrs: term list, + case_lazy: term, + active: bool, + activate: theory -> theory, + deactivate: theory -> theory}; + +fun map_active f {eagerT, lazyT, ctr, destr, lazy_ctrs, case_lazy, active, activate, deactivate} = + { eagerT = eagerT, + lazyT = lazyT, + ctr = ctr, + destr = destr, + lazy_ctrs = lazy_ctrs, + case_lazy = case_lazy, + active = f active, + activate = activate, + deactivate = deactivate + } + +structure Laziness_Data = Theory_Data( + type T = lazy_info Symtab.table; + val empty = Symtab.empty; + val merge = Symtab.join (fn _ => fn (_, record) => record); + val extend = I; +); + +fun fold_type type' tfree tvar typ = + let + fun go (Type (s, Ts)) = type' (s, map go Ts) + | go (TFree T) = tfree T + | go (TVar T) = tvar T + in + go typ + end; + +fun read_typ lthy name = + let + val (s, Ts) = Proof_Context.read_type_name {proper = true, strict = true} lthy name |> dest_Type + val (Ts', _) = Ctr_Sugar_Util.mk_TFrees (length Ts) lthy + in + Type (s, Ts') + end + +fun mk_name prefix suffix name ctxt = + Ctr_Sugar_Util.mk_fresh_names ctxt 1 (prefix ^ name ^ suffix) |>> hd; +fun generate_typedef_name name ctxt = mk_name "" "_lazy" name ctxt; + +fun add_syntax_definition short_type_name eagerT lazyT lazy_ctr lthy = + let + val (name, _) = mk_name "lazy_" "" short_type_name lthy + val freeT = HOLogic.unitT --> lazyT + val lazyT' = Type (@{type_name lazy}, [lazyT]) + val def = Logic.all_const freeT $ absdummy freeT (Logic.mk_equals ( + Free (name, (freeT --> eagerT)) $ Bound 0, + lazy_ctr $ (Const (@{const_name delay}, (freeT --> lazyT')) $ Bound 0))) + val (_, lthy') = Local_Theory.open_target lthy + val ((t, (_, thm)), lthy') = Specification.definition NONE [] [] + ((Thm.def_binding (Binding.name name), []), def) lthy' + val lthy' = Specification.notation true ("", false) [(t, Mixfix.mixfix "_")] lthy' + val lthy = Local_Theory.close_target lthy' + val def_thm = singleton (Proof_Context.export lthy' lthy) thm + in + (def_thm, lthy) + end; + +fun add_ctr_code raw_ctrs case_thms thy = + let + fun mk_case_certificate ctxt raw_thms = + let + val thms = raw_thms + |> Conjunction.intr_balanced + |> Thm.unvarify_global (Proof_Context.theory_of ctxt) + |> Conjunction.elim_balanced (length raw_thms) + |> map Simpdata.mk_meta_eq + |> map Drule.zero_var_indexes + val thm1 = case thms of + thm :: _ => thm + | _ => raise Empty + val params = Term.add_free_names (Thm.prop_of thm1) []; + val rhs = thm1 + |> Thm.prop_of |> Logic.dest_equals |> fst |> strip_comb + ||> fst o split_last |> list_comb + val lhs = Free (singleton (Name.variant_list params) "case", fastype_of rhs); + val assum = Thm.cterm_of ctxt (Logic.mk_equals (lhs, rhs)) + in + thms + |> Conjunction.intr_balanced + |> rewrite_rule ctxt [Thm.symmetric (Thm.assume assum)] + |> Thm.implies_intr assum + |> Thm.generalize ([], params) 0 + |> Axclass.unoverload ctxt + |> Thm.varifyT_global + end + val ctrs = map (apsnd (perhaps (try Logic.unvarifyT_global))) raw_ctrs + val unover_ctrs = map (fn ctr as (_, fcT) => (Axclass.unoverload_const thy ctr, fcT)) ctrs + in + if can (Code.constrset_of_consts thy) unover_ctrs then + thy + |> Code.declare_datatype_global ctrs + |> fold_rev (Code.add_eqn_global o rpair true) case_thms + |> Code.declare_case_global (mk_case_certificate (Proof_Context.init_global thy) case_thms) + else + thy + end; + +fun not_found s = error (s ^ " has not been added as lazy type"); + +fun validate_type_name thy type_name = + let + val lthy = Named_Target.theory_init thy + val eager_type = read_typ lthy type_name + val type_name = case eager_type of + Type (s, _) => s + | _ => raise Match + in + type_name + end; + +fun set_active_lazy_type value eager_type_string thy = + let + val type_name = validate_type_name thy eager_type_string + val x = + case Symtab.lookup (Laziness_Data.get thy) type_name of + NONE => not_found type_name + | SOME x => x + val new_x = map_active (K value) x + val thy1 = if value = #active x + then thy + else if value + then #activate x thy + else #deactivate x thy + in + Laziness_Data.map (Symtab.update (type_name, new_x)) thy1 + end; + +fun set_active_lazy_types value thy = + let + val lazy_type_names = Symtab.keys (Laziness_Data.get thy) + fun fold_fun value type_name thy = + let + val x = + case Symtab.lookup (Laziness_Data.get thy) type_name of + SOME x => x + | NONE => raise Match + val new_x = map_active (K value) x + val thy1 = if value = #active x + then thy + else if value + then #activate x thy + else #deactivate x thy + in + Laziness_Data.map (Symtab.update (type_name, new_x)) thy1 + end + in + fold (fold_fun value) lazy_type_names thy + end; + +(* code_lazy_type : string -> theory -> theory *) +fun code_lazy_type eager_type_string thy = + let + val lthy = Named_Target.theory_init thy + val eagerT = read_typ lthy eager_type_string + val (type_name, type_args) = dest_Type eagerT + val short_type_name = Long_Name.base_name type_name + val _ = if Symtab.defined (Laziness_Data.get thy) type_name + then error (type_name ^ " has already been added as lazy type.") + else () + val {case_thms, casex, ctrs, ...} = case Ctr_Sugar.ctr_sugar_of lthy type_name of + SOME x => x + | _ => error (type_name ^ " is not registered with free constructors.") + + fun substitute_ctr (old_T, new_T) ctr_T lthy = + let + val old_ctr_vars = map TVar (Term.add_tvarsT ctr_T []) + val old_ctr_Ts = map TFree (Term.add_tfreesT ctr_T []) @ old_ctr_vars + val (new_ctr_Ts, lthy') = Ctr_Sugar_Util.mk_TFrees (length old_ctr_Ts) lthy + + fun double_type_fold Ts = case Ts of + (Type (_, Ts1), Type (_, Ts2)) => flat (map double_type_fold (Ts1 ~~ Ts2)) + | (Type _, _) => raise Match + | (_, Type _) => raise Match + | Ts => [Ts] + fun map_fun1 f = List.foldr + (fn ((T1, T2), f) => fn T => if T = T1 then T2 else f T) + f + (double_type_fold (old_T, new_T)) + val map_fun2 = AList.lookup (op =) (old_ctr_Ts ~~ new_ctr_Ts) #> the + val map_fun = map_fun1 map_fun2 + + val new_ctr_type = fold_type Type (map_fun o TFree) (map_fun o TVar) ctr_T + in + (new_ctr_type, lthy') + end + + val (short_lazy_type_name, lthy1) = generate_typedef_name short_type_name lthy + + fun mk_lazy_typedef (name, eager_type) lthy = + let + val binding = Binding.name name + val (result, lthy1) = (Typedef.add_typedef + { overloaded=false } + (binding, rev (Term.add_tfreesT eager_type []), Mixfix.NoSyn) + (Const (@{const_name "top"}, Type (@{type_name set}, [eager_type]))) + NONE + (fn ctxt => resolve_tac ctxt [@{thm UNIV_witness}] 1) + o (Local_Theory.open_target #> snd)) lthy + in + (binding, result, Local_Theory.close_target lthy1) + end; + + val (typedef_binding, (_, info), lthy2) = mk_lazy_typedef (short_lazy_type_name, eagerT) lthy1 + + val lazy_type = Type (Local_Theory.full_name lthy2 typedef_binding, type_args) + val (Abs_lazy, Rep_lazy) = + let + val info = fst info + val Abs_name = #Abs_name info + val Rep_name = #Rep_name info + val Abs_type = eagerT --> lazy_type + val Rep_type = lazy_type --> eagerT + in + (Const (Abs_name, Abs_type), Const (Rep_name, Rep_type)) + end + val Abs_inverse = #Abs_inverse (snd info) + val Rep_inverse = #Rep_inverse (snd info) + + val (ctrs', lthy3) = List.foldr + (fn (Const (s, T), (ctrs, lthy)) => let + val (T', lthy') = substitute_ctr (body_type T, eagerT) T lthy + in + ((Const (s, T')) :: ctrs, lthy') + end + ) + ([], lthy2) + ctrs + + fun to_destr_eagerT typ = case typ of + Type (@{type_name "fun"}, [_, Type (@{type_name "fun"}, Ts)]) => + to_destr_eagerT (Type (@{type_name "fun"}, Ts)) + | Type (@{type_name "fun"}, [T, _]) => T + | _ => raise Match + val (case', lthy4) = + let + val (eager_case, caseT) = dest_Const casex + val (caseT', lthy') = substitute_ctr (to_destr_eagerT caseT, eagerT) caseT lthy3 + in (Const (eager_case, caseT'), lthy') end + + val ctr_names = map (Long_Name.base_name o fst o dest_Const) ctrs + val ((((lazy_ctr_name, lazy_sel_name), lazy_ctrs_name), lazy_case_name), ctxt) = lthy4 + |> mk_name "Lazy_" "" short_type_name + ||>> mk_name "unlazy_" "" short_type_name + ||>> fold_map (mk_name "" "_Lazy") ctr_names + ||>> mk_name "case_" "_lazy" short_type_name + + fun mk_def (name, T, rhs) lthy = + let + val binding = Binding.name name + val ((_, (_, thm)), lthy1) = + Local_Theory.open_target lthy |> snd + |> Specification.definition NONE [] [] ((Thm.def_binding binding, []), rhs) + val lthy2 = Local_Theory.close_target lthy1 + val def_thm = hd (Proof_Context.export lthy1 lthy2 [thm]) + in + ({binding = binding, const = Const (Local_Theory.full_name lthy2 binding, T), thm = def_thm}, lthy2) + end; + + val lazy_datatype = Type (@{type_name lazy}, [lazy_type]) + val Lazy_type = lazy_datatype --> eagerT + val unstr_type = eagerT --> lazy_datatype + + fun apply_bounds i n term = + if n > i then apply_bounds i (n-1) (term $ Bound (n-1)) + else term + fun all_abs Ts t = Logic.list_all (map (pair Name.uu) Ts, t) + fun mk_force t = Const (@{const_name force}, lazy_datatype --> lazy_type) $ t + fun mk_delay t = Const (@{const_name delay}, (@{typ unit} --> lazy_type) --> lazy_datatype) $ t + + val lazy_ctr = all_abs [lazy_datatype] + (Logic.mk_equals (Free (lazy_ctr_name, Lazy_type) $ Bound 0, Rep_lazy $ mk_force (Bound 0))) + val (lazy_ctr_def, lthy5) = mk_def (lazy_ctr_name, Lazy_type, lazy_ctr) lthy4 + + val lazy_sel = all_abs [eagerT] + (Logic.mk_equals (Free (lazy_sel_name, unstr_type) $ Bound 0, + mk_delay (Abs (Name.uu, @{typ unit}, Abs_lazy $ Bound 1)))) + val (lazy_sel_def, lthy6) = mk_def (lazy_sel_name, unstr_type, lazy_sel) lthy5 + + fun mk_lazy_ctr (name, eager_ctr) = + let + val (_, ctrT) = dest_Const eager_ctr + fun to_lazy_ctrT (Type (@{type_name fun}, [T1, T2])) = T1 --> to_lazy_ctrT T2 + | to_lazy_ctrT T = if T = eagerT then lazy_type else raise Match + val lazy_ctrT = to_lazy_ctrT ctrT + val argsT = binder_types ctrT + val lhs = apply_bounds 0 (length argsT) (Free (name, lazy_ctrT)) + val rhs = Abs_lazy $ apply_bounds 0 (length argsT) eager_ctr + in + mk_def (name, lazy_ctrT, all_abs argsT (Logic.mk_equals (lhs, rhs))) + end + val (lazy_ctrs_def, lthy7) = fold_map mk_lazy_ctr (lazy_ctrs_name ~~ ctrs') lthy6 + + val (lazy_case_def, lthy8) = + let + val (_, caseT) = dest_Const case' + fun to_lazy_caseT (Type (@{type_name fun}, [T1, T2])) = + if T1 = eagerT then lazy_type --> T2 else T1 --> to_lazy_caseT T2 + val lazy_caseT = to_lazy_caseT caseT + val argsT = binder_types lazy_caseT + val n = length argsT + val lhs = apply_bounds 0 n (Free (lazy_case_name, lazy_caseT)) + val rhs = apply_bounds 1 n case' $ (Rep_lazy $ Bound 0) + in + mk_def (lazy_case_name, lazy_caseT, all_abs argsT (Logic.mk_equals (lhs, rhs))) lthy7 + end + + fun mk_thm ((name, term), thms) lthy = + let + val binding = Binding.name name + fun tac {context, ...} = Simplifier.simp_tac + (put_simpset HOL_basic_ss context addsimps thms) + 1 + val thm = Goal.prove lthy [] [] term tac + val (_, lthy1) = lthy + |> Local_Theory.open_target |> snd + |> Local_Theory.note ((binding, []), [thm]) + in + (thm, Local_Theory.close_target lthy1) + end + fun mk_thms exec_list lthy = fold_map mk_thm exec_list lthy + + val mk_eq = HOLogic.mk_Trueprop o HOLogic.mk_eq + + val lazy_ctrs = map #const lazy_ctrs_def + val eager_lazy_ctrs = ctrs' ~~ lazy_ctrs + + val (((((((Lazy_delay_eq_name, Rep_ctr_names), ctrs_lazy_names), force_sel_name), case_lazy_name), + sel_lazy_name), case_ctrs_name), _) = lthy5 + |> mk_name "Lazy_" "_delay" short_type_name + ||>> fold_map (mk_name "Rep_" "_Lazy") ctr_names + ||>> fold_map (mk_name "" "_conv_lazy") ctr_names + ||>> mk_name "force_unlazy_" "" short_type_name + ||>> mk_name "case_" "_conv_lazy" short_type_name + ||>> mk_name "Lazy_" "_inverse" short_type_name + ||>> fold_map (mk_name ("case_" ^ short_type_name ^ "_lazy_") "") ctr_names + + val mk_Lazy_delay_eq = + (#const lazy_ctr_def $ mk_delay (Bound 0), Rep_lazy $ (Bound 0 $ @{const Unity})) + |> mk_eq |> all_abs [@{typ unit} --> lazy_type] + val (Lazy_delay_thm, lthy8a) = mk_thm + ((Lazy_delay_eq_name, mk_Lazy_delay_eq), [#thm lazy_ctr_def, @{thm force_delay}]) + lthy8 + + fun mk_lazy_ctr_eq (eager_ctr, lazy_ctr) = + let + val (_, ctrT) = dest_Const eager_ctr + val argsT = binder_types ctrT + val args = length argsT + in + (Rep_lazy $ apply_bounds 0 args lazy_ctr, apply_bounds 0 args eager_ctr) + |> mk_eq |> all_abs argsT + end + val Rep_ctr_eqs = map mk_lazy_ctr_eq eager_lazy_ctrs + val (Rep_ctr_thms, lthy8b) = mk_thms + ((Rep_ctr_names ~~ Rep_ctr_eqs) ~~ + (map (fn def => [#thm def, Abs_inverse, @{thm UNIV_I}]) lazy_ctrs_def) + ) + lthy8a + + fun mk_ctrs_lazy_eq (eager_ctr, lazy_ctr) = + let + val argsT = dest_Const eager_ctr |> snd |> binder_types + val n = length argsT + val lhs = apply_bounds 0 n eager_ctr + val rhs = #const lazy_ctr_def $ + (mk_delay (Abs (Name.uu, @{typ unit}, apply_bounds 1 (n + 1) lazy_ctr))) + in + (lhs, rhs) |> mk_eq |> all_abs argsT + end + val ctrs_lazy_eq = map mk_ctrs_lazy_eq eager_lazy_ctrs + val (ctrs_lazy_thms, lthy8c) = mk_thms + ((ctrs_lazy_names ~~ ctrs_lazy_eq) ~~ map (fn thm => [Lazy_delay_thm, thm]) Rep_ctr_thms) + lthy8b + + val force_sel_eq = + (mk_force (#const lazy_sel_def $ Bound 0), Abs_lazy $ Bound 0) + |> mk_eq |> all_abs [eagerT] + val (force_sel_thm, lthy8d) = mk_thm + ((force_sel_name, force_sel_eq), [#thm lazy_sel_def, @{thm force_delay}]) + lthy8c + + val case_lazy_eq = + let + val (_, caseT) = case' |> dest_Const + val argsT = binder_types caseT + val n = length argsT + val lhs = apply_bounds 0 n case' + val rhs = apply_bounds 1 n (#const lazy_case_def) $ (mk_force (#const lazy_sel_def $ Bound 0)) + in + (lhs, rhs) |> mk_eq |> all_abs argsT + end + val (case_lazy_thm, lthy8e) = mk_thm + ((case_lazy_name, case_lazy_eq), + [#thm lazy_case_def, force_sel_thm, Abs_inverse, @{thm UNIV_I}]) + lthy8d + + val sel_lazy_eq = + (#const lazy_sel_def $ (#const lazy_ctr_def $ Bound 0), Bound 0) + |> mk_eq |> all_abs [lazy_datatype] + val (sel_lazy_thm, lthy8f) = mk_thm + ((sel_lazy_name, sel_lazy_eq), + [#thm lazy_sel_def, #thm lazy_ctr_def, Rep_inverse, @{thm delay_force}]) + lthy8e + + fun mk_case_ctrs_eq (i, lazy_ctr) = + let + val lazy_case = #const lazy_case_def + val (_, ctrT) = dest_Const lazy_ctr + val ctr_argsT = binder_types ctrT + val ctr_args_n = length ctr_argsT + val (_, caseT) = dest_Const lazy_case + val case_argsT = binder_types caseT + + fun n_bounds_from m n t = + if n > 0 then n_bounds_from (m - 1) (n - 1) (t $ Bound (m - 1)) else t + + val case_argsT' = take (length case_argsT - 1) case_argsT + val Ts = case_argsT' @ ctr_argsT + val num_abs_types = length Ts + val lhs = n_bounds_from num_abs_types (length case_argsT') lazy_case $ + apply_bounds 0 ctr_args_n lazy_ctr + val rhs = apply_bounds 0 ctr_args_n (Bound (num_abs_types - i - 1)) + in + (lhs, rhs) |> mk_eq |> all_abs Ts + end + val case_ctrs_eq = map_index mk_case_ctrs_eq lazy_ctrs + val (case_ctrs_thms, lthy9) = mk_thms + ((case_ctrs_name ~~ case_ctrs_eq) ~~ + map2 (fn thm1 => fn thm2 => [#thm lazy_case_def, thm1, thm2]) Rep_ctr_thms case_thms + ) + lthy8f + + val (pat_def_thm, lthy10) = + add_syntax_definition short_type_name eagerT lazy_type (#const lazy_ctr_def) lthy9 + + val add_lazy_ctrs = + Code.declare_datatype_global [dest_Const (#const lazy_ctr_def)] + val eager_ctrs = map (apsnd (perhaps (try Logic.unvarifyT_global)) o dest_Const) ctrs + val add_eager_ctrs = + fold Code.del_eqn_global ctrs_lazy_thms + #> Code.declare_datatype_global eager_ctrs + val add_code_eqs = fold (Code.add_eqn_global o rpair true) + ([case_lazy_thm, sel_lazy_thm]) + val add_lazy_ctr_thms = fold (Code.add_eqn_global o rpair true) ctrs_lazy_thms + val add_lazy_case_thms = + fold Code.del_eqn_global case_thms + #> Code.add_eqn_global (case_lazy_thm, false) + val add_eager_case_thms = Code.del_eqn_global case_lazy_thm + #> fold (Code.add_eqn_global o rpair false) case_thms + + val delay_dummy_thm = (pat_def_thm RS @{thm symmetric}) + |> Drule.infer_instantiate' lthy10 + [SOME (Thm.cterm_of lthy10 (Const (@{const_name "Pure.dummy_pattern"}, HOLogic.unitT --> lazy_type)))] + |> Thm.generalize (map (fst o dest_TFree) type_args, []) (Variable.maxidx_of lthy10 + 1); + + val ctr_post = delay_dummy_thm :: map (fn thm => thm RS @{thm sym}) ctrs_lazy_thms + val ctr_thms_abs = map (fn thm => Drule.abs_def (thm RS @{thm eq_reflection})) ctrs_lazy_thms + val case_thm_abs = Drule.abs_def (case_lazy_thm RS @{thm eq_reflection}) + val add_simps = Code_Preproc.map_pre + (fn ctxt => ctxt addsimps (case_thm_abs :: ctr_thms_abs)) + val del_simps = Code_Preproc.map_pre + (fn ctxt => ctxt delsimps (case_thm_abs :: ctr_thms_abs)) + val add_post = Code_Preproc.map_post + (fn ctxt => ctxt addsimps ctr_post) + val del_post = Code_Preproc.map_post + (fn ctxt => ctxt delsimps ctr_post) + in + Local_Theory.exit_global lthy10 + |> Laziness_Data.map (Symtab.update (type_name, + {eagerT = eagerT, + lazyT = lazy_type, + ctr = #const lazy_ctr_def, + destr = #const lazy_sel_def, + lazy_ctrs = map #const lazy_ctrs_def, + case_lazy = #const lazy_case_def, + active = true, + activate = add_lazy_ctrs #> add_lazy_ctr_thms #> add_lazy_case_thms #> add_simps #> add_post, + deactivate = add_eager_ctrs #> add_eager_case_thms #> del_simps #> del_post})) + |> add_lazy_ctrs + |> add_ctr_code (map (dest_Const o #const) lazy_ctrs_def) case_ctrs_thms + |> add_code_eqs + |> add_lazy_ctr_thms + |> add_simps + |> add_post + end; + +fun transform_code_eqs _ [] = NONE + | transform_code_eqs ctxt eqs = + let + val thy = Proof_Context.theory_of ctxt + val table = Laziness_Data.get thy + fun eliminate (s1, s2) = case Symtab.lookup table s1 of + NONE => false + | SOME x => #active x andalso s2 <> (#ctr x |> dest_Const |> fst) + fun num_consts_fun (_, T) = + let + val s = body_type T |> dest_Type |> fst + in + if Symtab.defined table s + then Ctr_Sugar.ctr_sugar_of ctxt s |> the |> #ctrs |> length + else Code.get_type thy s |> fst |> snd |> length + end + val eqs = map (apfst (Thm.transfer thy)) eqs; + + val ((code_eqs, nbe_eqs), pure) = + ((case hd eqs |> fst |> Thm.prop_of of + Const (@{const_name Pure.eq}, _) $ _ $ _ => + (map (apfst (fn x => x RS @{thm meta_eq_to_obj_eq})) eqs, true) + | _ => (eqs, false)) + |> apfst (List.partition snd)) + handle THM _ => (([], eqs), false) + val to_original_eq = if pure then map (apfst (fn x => x RS @{thm eq_reflection})) else I + in + case Case_Converter.to_case ctxt eliminate num_consts_fun (map fst code_eqs) of + NONE => NONE + | SOME thms => SOME (nbe_eqs @ map (rpair true) thms |> to_original_eq) + end handle THM ex => (Output.writeln (@{make_string} eqs); raise THM ex); + +val activate_lazy_type = set_active_lazy_type true; +val deactivate_lazy_type = set_active_lazy_type false; +val activate_lazy_types = set_active_lazy_types true; +val deactivate_lazy_types = set_active_lazy_types false; + +fun get_lazy_types thy = Symtab.dest (Laziness_Data.get thy) + +fun print_lazy_type thy (name, info : lazy_info) = + let + val ctxt = Proof_Context.init_global thy + fun pretty_ctr ctr = + let + val argsT = dest_Const ctr |> snd |> binder_types + in + Pretty.block [ + Syntax.pretty_term ctxt ctr, + Pretty.brk 1, + Pretty.block (Pretty.separate "" (map (Pretty.quote o Syntax.pretty_typ ctxt) argsT)) + ] + end + in + Pretty.block [ + Pretty.str (name ^ (if #active info then "" else " (inactive)") ^ ":"), + Pretty.brk 1, + Pretty.block [ + Syntax.pretty_typ ctxt (#eagerT info), + Pretty.brk 1, + Pretty.str "=", + Pretty.brk 1, + Syntax.pretty_term ctxt (#ctr info), + Pretty.brk 1, + Pretty.block [ + Pretty.str "(", + Syntax.pretty_term ctxt (#destr info), + Pretty.str ":", + Pretty.brk 1, + Syntax.pretty_typ ctxt (Type (@{type_name lazy}, [#lazyT info])), + Pretty.str ")" + ] + ], + Pretty.fbrk, + Pretty.keyword2 "and", + Pretty.brk 1, + Pretty.block ([ + Syntax.pretty_typ ctxt (#lazyT info), + Pretty.brk 1, + Pretty.str "=", + Pretty.brk 1] @ + Pretty.separate " |" (map pretty_ctr (#lazy_ctrs info)) @ [ + Pretty.fbrk, + Pretty.keyword2 "for", + Pretty.brk 1, + Pretty.str "case:", + Pretty.brk 1, + Syntax.pretty_term ctxt (#case_lazy info) + ]) + ] + end; + +fun print_lazy_types thy = + let + fun cmp ((name1, _), (name2, _)) = string_ord (name1, name2) + val infos = Laziness_Data.get thy |> Symtab.dest |> map (apfst Long_Name.base_name) |> sort cmp + in + Pretty.writeln_chunks (map (print_lazy_type thy) infos) + end; + + +val _ = + Outer_Syntax.command @{command_keyword code_lazy_type} + "make a lazy copy of the datatype and activate substitution" + (Parse.binding >> (fn b => Toplevel.theory (Binding.name_of b |> code_lazy_type))); +val _ = + Outer_Syntax.command @{command_keyword activate_lazy_type} + "activate substitution on a specific (lazy) type" + (Parse.binding >> (fn b => Toplevel.theory (Binding.name_of b |> activate_lazy_type))); +val _ = + Outer_Syntax.command @{command_keyword deactivate_lazy_type} + "deactivate substitution on a specific (lazy) type" + (Parse.binding >> (fn b => Toplevel.theory (Binding.name_of b |> deactivate_lazy_type))); +val _ = + Outer_Syntax.command @{command_keyword activate_lazy_types} + "activate substitution on all (lazy) types" + (pair (Toplevel.theory activate_lazy_types)); +val _ = + Outer_Syntax.command @{command_keyword deactivate_lazy_types} + "deactivate substitution on all (lazy) type" + (pair (Toplevel.theory deactivate_lazy_types)); +val _ = + Outer_Syntax.command @{command_keyword print_lazy_types} + "print the types that have been declared as lazy and their substitution state" + (pair (Toplevel.theory (tap print_lazy_types))); + +end \ No newline at end of file diff -r 42d63ea39161 -r 8b50f29a1992 src/HOL/Library/document/root.bib --- a/src/HOL/Library/document/root.bib Fri May 11 22:59:00 2018 +0200 +++ b/src/HOL/Library/document/root.bib Sat May 12 11:24:11 2018 +0200 @@ -52,3 +52,10 @@ year = 1993, publisher = {Springer}, series = {LNCS 664}} + +@InProceedings{LochbihlerStoop2018, + author = {Andreas Lochbihler and Pascal Stoop}, + title = {Lazy Algebraic Types in {Isabelle/HOL}}, + booktitle = {Isabelle Workshop 2018}, + year = 2018, +} \ No newline at end of file diff -r 42d63ea39161 -r 8b50f29a1992 src/HOL/ROOT --- a/src/HOL/ROOT Fri May 11 22:59:00 2018 +0200 +++ b/src/HOL/ROOT Sat May 12 11:24:11 2018 +0200 @@ -247,6 +247,7 @@ Generate_Binary_Nat Generate_Target_Nat Generate_Efficient_Datastructures + Code_Lazy_Test Code_Test_PolyML Code_Test_Scala theories [condition = ISABELLE_GHC]