# HG changeset patch
# User haftmann
# Date 1546075710 0
# Node ID 9d0e492e3229eed4b800c27a8f06c0e1d22c3eb0
# Parent  3626ccf644e1899514a803c3d1f8b5245033538f
explicit dependencies for includes

diff -r 3626ccf644e1 -r 9d0e492e3229 src/HOL/Library/Code_Lazy.thy
--- a/src/HOL/Library/Code_Lazy.thy	Sat Dec 29 09:28:28 2018 +0000
+++ b/src/HOL/Library/Code_Lazy.thy	Sat Dec 29 09:28:30 2018 +0000
@@ -39,6 +39,7 @@
 
 ML_file "case_converter.ML"
 
+
 subsection \<open>The type \<open>lazy\<close>\<close>
 
 typedef 'a lazy = "UNIV :: 'a set" ..
@@ -47,10 +48,40 @@
 lift_definition force :: "'a lazy \<Rightarrow> 'a" is "\<lambda>x. x" .
 
 code_datatype delay
-lemma force_delay [code]: "force (delay f) = f ()" by transfer(rule refl)
-lemma delay_force: "delay (\<lambda>_. force s) = s" by transfer(rule refl)
+lemma force_delay [code]: "force (delay f) = f ()" by transfer (rule refl)
+lemma delay_force: "delay (\<lambda>_. force s) = s" by transfer (rule refl)
+
+definition termify_lazy2 :: "'a :: typerep lazy \<Rightarrow> term"
+  where "termify_lazy2 x =
+  Code_Evaluation.App (Code_Evaluation.Const (STR ''Code_Lazy.delay'') (TYPEREP((unit \<Rightarrow> 'a) \<Rightarrow> 'a lazy)))
+    (Code_Evaluation.Const (STR ''Pure.dummy_pattern'') (TYPEREP((unit \<Rightarrow> 'a))))"
+
+definition termify_lazy ::
+  "(String.literal \<Rightarrow> 'typerep \<Rightarrow> 'term) \<Rightarrow>
+   ('term \<Rightarrow> 'term \<Rightarrow> 'term) \<Rightarrow>
+   (String.literal \<Rightarrow> 'typerep \<Rightarrow> 'term \<Rightarrow> 'term) \<Rightarrow>
+   'typerep \<Rightarrow> ('typerep \<Rightarrow> 'typerep \<Rightarrow> 'typerep) \<Rightarrow> ('typerep \<Rightarrow> 'typerep) \<Rightarrow>
+   ('a \<Rightarrow> 'term) \<Rightarrow> 'typerep \<Rightarrow> 'a :: typerep lazy \<Rightarrow> 'term \<Rightarrow> term"
+  where "termify_lazy _ _ _ _ _ _ _ _ x _ = termify_lazy2 x"
 
-text \<open>The implementations of @{typ "_ lazy"} using language primitives cache forced values.\<close>
+declare [[code drop: "Code_Evaluation.term_of :: _ lazy \<Rightarrow> _"]]
+
+lemma term_of_lazy_code [code]:
+  "Code_Evaluation.term_of x \<equiv>
+   termify_lazy
+     Code_Evaluation.Const Code_Evaluation.App Code_Evaluation.Abs
+     TYPEREP(unit) (\<lambda>T U. typerep.Typerep (STR ''fun'') [T, U]) (\<lambda>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)
+
+text \<open>
+  The implementations of @{typ "_ lazy"} using language primitives cache forced values.
+
+  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 as we do not know of any portable way to inspect whether a lazy value
+  has been evaluated to or not.
+\<close>
 
 code_printing code_module Lazy \<rightharpoonup> (SML)
 \<open>signature LAZY =
@@ -95,29 +126,69 @@
     (case peek x of SOME y => abs "_" unitT (term_of y)
      | _ => const "Pure.dummy_pattern" (funT unitT T));
 
-end;\<close>
-code_reserved SML Lazy
-
-code_printing
-  type_constructor lazy \<rightharpoonup> (SML) "_ Lazy.lazy"
+end;\<close> for type_constructor lazy constant delay force termify_lazy
+| type_constructor lazy \<rightharpoonup> (SML) "_ Lazy.lazy"
 | constant delay \<rightharpoonup> (SML) "Lazy.lazy"
 | constant force \<rightharpoonup> (SML) "Lazy.force"
+| constant termify_lazy \<rightharpoonup> (SML) "Lazy.termify'_lazy"
+
+code_reserved SML Lazy
 
 code_printing \<comment> \<open>For code generation within the Isabelle environment, we reuse the thread-safe
   implementation of lazy from @{file "~~/src/Pure/Concurrent/lazy.ML"}\<close>
-  code_module Lazy \<rightharpoonup> (Eval) \<open>\<close>
+  code_module Lazy \<rightharpoonup> (Eval) \<open>\<close> for constant undefined
 | type_constructor lazy \<rightharpoonup> (Eval) "_ Lazy.lazy"
 | constant delay \<rightharpoonup> (Eval) "Lazy.lazy"
 | constant force \<rightharpoonup> (Eval) "Lazy.force"
+| code_module Termify_Lazy \<rightharpoonup> (Eval)
+\<open>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;\<close> for constant termify_lazy
+| constant termify_lazy \<rightharpoonup> (Eval) "Termify'_Lazy.termify'_lazy"
+
+code_reserved Eval Termify_Lazy
+
+code_printing
+  type_constructor lazy \<rightharpoonup> (OCaml) "_ Lazy.t"
+| constant delay \<rightharpoonup> (OCaml) "Lazy.from'_fun"
+| constant force \<rightharpoonup> (OCaml) "Lazy.force"
+| code_module Termify_Lazy \<rightharpoonup> (OCaml)
+\<open>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;;\<close> for constant termify_lazy
+| constant termify_lazy \<rightharpoonup> (OCaml) "Termify'_Lazy.termify'_lazy"
+
+code_reserved OCaml Lazy Termify_Lazy
+
 
 code_printing
   code_module Lazy \<rightharpoonup> (Haskell) 
 \<open>newtype Lazy a = Lazy a;
 delay f = Lazy (f ());
-force (Lazy x) = x;\<close>
+force (Lazy x) = x;\<close> for type_constructor lazy constant delay force
 | type_constructor lazy \<rightharpoonup> (Haskell) "Lazy.Lazy _"
 | constant delay \<rightharpoonup> (Haskell) "Lazy.delay"
 | constant force \<rightharpoonup> (Haskell) "Lazy.force"
+
 code_reserved Haskell Lazy
 
 code_printing
@@ -157,84 +228,14 @@
     else
       app(const("Code_Lazy.delay")(funT(funT(unitT)(ty))(lazyT(ty))))(const("Pure.dummy_pattern")(funT(unitT)(ty)))
   }
-}\<close>
+}\<close> for type_constructor lazy constant delay force termify_lazy
 | type_constructor lazy \<rightharpoonup> (Scala) "Lazy.Lazy[_]"
 | constant delay \<rightharpoonup> (Scala) "Lazy.delay"
 | constant force \<rightharpoonup> (Scala) "Lazy.force"
-code_reserved Scala Lazy termify_lazy
-
-code_printing
-  type_constructor lazy \<rightharpoonup> (OCaml) "_ Lazy.t"
-| constant delay \<rightharpoonup> (OCaml) "Lazy.from'_fun"
-| constant force \<rightharpoonup> (OCaml) "Lazy.force"
-code_reserved OCaml Lazy
-
-text \<open>
-  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.
-\<close>
-code_printing code_module Termify_Lazy \<rightharpoonup> (Eval) 
-\<open>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;\<close>
-code_reserved Eval Termify_Lazy TERMIFY_LAZY termify_lazy
-
-code_printing code_module Termify_Lazy \<rightharpoonup> (OCaml) 
-\<open>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
+| constant termify_lazy \<rightharpoonup> (Scala) "Lazy.termify'_lazy"
 
-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;;\<close>
-code_reserved OCaml Termify_Lazy termify_lazy
-
-definition termify_lazy2 :: "'a :: typerep lazy \<Rightarrow> term"
-where "termify_lazy2 x =
-  Code_Evaluation.App (Code_Evaluation.Const (STR ''Code_Lazy.delay'') (TYPEREP((unit \<Rightarrow> 'a) \<Rightarrow> 'a lazy)))
-    (Code_Evaluation.Const (STR ''Pure.dummy_pattern'') (TYPEREP((unit \<Rightarrow> 'a))))"
+code_reserved Scala Lazy
 
-definition termify_lazy :: 
-  "(String.literal \<Rightarrow> 'typerep \<Rightarrow> 'term) \<Rightarrow> 
-   ('term \<Rightarrow> 'term \<Rightarrow> 'term) \<Rightarrow> 
-   (String.literal \<Rightarrow> 'typerep \<Rightarrow> 'term \<Rightarrow> 'term) \<Rightarrow>
-   'typerep \<Rightarrow> ('typerep \<Rightarrow> 'typerep \<Rightarrow> 'typerep) \<Rightarrow> ('typerep \<Rightarrow> 'typerep) \<Rightarrow>
-   ('a \<Rightarrow> 'term) \<Rightarrow> 'typerep \<Rightarrow> 'a :: typerep lazy \<Rightarrow> 'term \<Rightarrow> term"
-where "termify_lazy _ _ _ _ _ _ _ _ x _ = termify_lazy2 x"
-
-declare [[code drop: "Code_Evaluation.term_of :: _ lazy \<Rightarrow> _"]]
-
-lemma term_of_lazy_code [code]:
-  "Code_Evaluation.term_of x \<equiv> 
-   termify_lazy 
-     Code_Evaluation.Const Code_Evaluation.App Code_Evaluation.Abs 
-     TYPEREP(unit) (\<lambda>T U. typerep.Typerep (STR ''fun'') [T, U]) (\<lambda>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
-  \<rightharpoonup> (SML) "Lazy.termify'_lazy" 
-  and (Eval) "Termify'_Lazy.termify'_lazy"
-  and (OCaml) "Termify'_Lazy.termify'_lazy"
-  and (Scala) "Lazy.termify'_lazy"
-  
 text \<open>Make evaluation with the simplifier respect @{term delay}s.\<close>
 
 lemma delay_lazy_cong: "delay f = delay f" by simp
diff -r 3626ccf644e1 -r 9d0e492e3229 src/HOL/Library/IArray.thy
--- a/src/HOL/Library/IArray.thy	Sat Dec 29 09:28:28 2018 +0000
+++ b/src/HOL/Library/IArray.thy	Sat Dec 29 09:28:30 2018 +0000
@@ -214,6 +214,7 @@
 
   length :: IArray e -> Integer;
   length (IArray v) = toInteger (Data.Ix.rangeSize (Data.Array.IArray.bounds v));\<close>
+  for type_constructor iarray constant IArray IArray.tabulate IArray.sub' IArray.length'
 
 code_reserved Haskell IArray_Impl
 
diff -r 3626ccf644e1 -r 9d0e492e3229 src/HOL/Quickcheck_Narrowing.thy
--- a/src/HOL/Quickcheck_Narrowing.thy	Sat Dec 29 09:28:28 2018 +0000
+++ b/src/HOL/Quickcheck_Narrowing.thy	Sat Dec 29 09:28:30 2018 +0000
@@ -16,15 +16,15 @@
 code_printing
   code_module Typerep \<rightharpoonup> (Haskell_Quickcheck) \<open>
 data Typerep = Typerep String [Typerep]
-\<close>
+\<close> for type_constructor typerep constant Typerep.Typerep
 | type_constructor typerep \<rightharpoonup> (Haskell_Quickcheck) "Typerep.Typerep"
 | constant Typerep.Typerep \<rightharpoonup> (Haskell_Quickcheck) "Typerep.Typerep"
-| type_constructor integer \<rightharpoonup> (Haskell_Quickcheck) "Prelude.Int"
 
 code_reserved Haskell_Quickcheck Typerep
 
 code_printing
-  constant "0::integer" \<rightharpoonup>
+  type_constructor integer \<rightharpoonup> (Haskell_Quickcheck) "Prelude.Int"
+| constant "0::integer" \<rightharpoonup>
     (Haskell_Quickcheck) "!(0/ ::/ Prelude.Int)"
 
 setup \<open>