src/HOL/Lazy_Sequence.thy
changeset 36513 70096cbdd4e0
parent 36176 3fe7e97ccca8
child 36516 8dac276ab10d
     1.1 --- a/src/HOL/Lazy_Sequence.thy	Wed Apr 28 15:42:10 2010 +0200
     1.2 +++ b/src/HOL/Lazy_Sequence.thy	Wed Apr 28 16:56:18 2010 +0200
     1.3 @@ -123,6 +123,13 @@
     1.4  
     1.5  subsection {* Code setup *}
     1.6  
     1.7 +code_reflect
     1.8 +  datatypes lazy_sequence = Lazy_Sequence
     1.9 +  functions "Lazy_Sequence.map" yield
    1.10 +  module_name Lazy_Sequence
    1.11 +
    1.12 +(* FIXME formulate yieldn in the logic with type code_numeral *)
    1.13 +
    1.14  ML {*
    1.15  signature LAZY_SEQUENCE =
    1.16  sig
    1.17 @@ -135,9 +142,9 @@
    1.18  structure Lazy_Sequence : LAZY_SEQUENCE =
    1.19  struct
    1.20  
    1.21 -@{code_datatype lazy_sequence = Lazy_Sequence}
    1.22 +open Lazy_Sequence;
    1.23  
    1.24 -val yield = @{code yield}
    1.25 +fun map f = mapa f;
    1.26  
    1.27  fun anamorph f k x = (if k = 0 then ([], x)
    1.28    else case f x
    1.29 @@ -148,17 +155,9 @@
    1.30  
    1.31  fun yieldn S = anamorph yield S;
    1.32  
    1.33 -val map = @{code map}
    1.34 -
    1.35  end;
    1.36  *}
    1.37  
    1.38 -code_reserved Eval Lazy_Sequence
    1.39 -
    1.40 -code_type lazy_sequence (Eval "_/ Lazy'_Sequence.lazy'_sequence")
    1.41 -
    1.42 -code_const Lazy_Sequence (Eval "Lazy'_Sequence.Lazy'_Sequence")
    1.43 -
    1.44  section {* With Hit Bound Value *}
    1.45  text {* assuming in negative context *}
    1.46