bulwahn@34948: 
bulwahn@34948: (* Author: Lukas Bulwahn, TU Muenchen *)
bulwahn@34948: 
bulwahn@34948: header {* Depth-Limited Sequences with failure element *}
bulwahn@34948: 
bulwahn@34948: theory DSequence
bulwahn@34948: imports Lazy_Sequence Code_Numeral
bulwahn@34948: begin
bulwahn@34948: 
bulwahn@34948: types 'a dseq = "code_numeral => bool => 'a Lazy_Sequence.lazy_sequence option"
bulwahn@34948: 
bulwahn@34948: definition empty :: "'a dseq"
bulwahn@34948: where
bulwahn@34948:   "empty = (%i pol. Some Lazy_Sequence.empty)"
bulwahn@34948: 
bulwahn@34948: definition single :: "'a => 'a dseq"
bulwahn@34948: where
bulwahn@34948:   "single x = (%i pol. Some (Lazy_Sequence.single x))"
bulwahn@34948: 
bulwahn@34948: fun eval :: "'a dseq => code_numeral => bool => 'a Lazy_Sequence.lazy_sequence option"
bulwahn@34948: where
bulwahn@34948:   "eval f i pol = f i pol"
bulwahn@34948: 
bulwahn@34948: definition yield :: "'a dseq => code_numeral => bool => ('a * 'a dseq) option" 
bulwahn@34948: where
bulwahn@34948:   "yield dseq i pol = (case eval dseq i pol of
bulwahn@34948:     None => None
bulwahn@34948:   | Some s => Option.map (apsnd (%r i pol. Some r)) (Lazy_Sequence.yield s))"
bulwahn@34948: 
bulwahn@34948: fun map_seq :: "('a => 'b dseq) => 'a Lazy_Sequence.lazy_sequence => 'b dseq"
bulwahn@34948: where
bulwahn@34948:   "map_seq f xq i pol = (case Lazy_Sequence.yield xq of
bulwahn@34948:     None => Some Lazy_Sequence.empty
bulwahn@34948:   | Some (x, xq') => (case eval (f x) i pol of
bulwahn@34948:       None => None
bulwahn@34948:     | Some yq => (case map_seq f xq' i pol of
bulwahn@34948:         None => None
bulwahn@34948:       | Some zq => Some (Lazy_Sequence.append yq zq))))"
bulwahn@34948: 
bulwahn@34953: definition bind :: "'a dseq => ('a => 'b dseq) => 'b dseq"
bulwahn@34948: where
bulwahn@34948:   "bind x f = (%i pol. 
bulwahn@34948:      if i = 0 then
bulwahn@34948:        (if pol then Some Lazy_Sequence.empty else None)
bulwahn@34948:      else
bulwahn@34948:        (case x (i - 1) pol of
bulwahn@34948:          None => None
bulwahn@34948:        | Some xq => map_seq f xq i pol))"
bulwahn@34948: 
bulwahn@34953: definition union :: "'a dseq => 'a dseq => 'a dseq"
bulwahn@34948: where
bulwahn@34948:   "union x y = (%i pol. case (x i pol, y i pol) of
bulwahn@34948:       (Some xq, Some yq) => Some (Lazy_Sequence.append xq yq)
bulwahn@34948:     | _ => None)"
bulwahn@34948: 
bulwahn@34948: definition if_seq :: "bool => unit dseq"
bulwahn@34948: where
bulwahn@34948:   "if_seq b = (if b then single () else empty)"
bulwahn@34948: 
bulwahn@34953: definition not_seq :: "unit dseq => unit dseq"
bulwahn@34948: where
bulwahn@34948:   "not_seq x = (%i pol. case x i (\<not>pol) of
bulwahn@34948:     None => Some Lazy_Sequence.empty
bulwahn@34948:   | Some xq => (case Lazy_Sequence.yield xq of
bulwahn@34948:       None => Some (Lazy_Sequence.single ())
bulwahn@34948:     | Some _ => Some (Lazy_Sequence.empty)))"
bulwahn@34948: 
bulwahn@34953: definition map :: "('a => 'b) => 'a dseq => 'b dseq"
bulwahn@34948: where
bulwahn@34948:   "map f g = (%i pol. case g i pol of
bulwahn@34948:      None => None
bulwahn@34948:    | Some xq => Some (Lazy_Sequence.map f xq))"
bulwahn@34948: 
bulwahn@34948: ML {*
bulwahn@34948: signature DSEQUENCE =
bulwahn@34948: sig
bulwahn@34948:   type 'a dseq = int -> bool -> 'a Lazy_Sequence.lazy_sequence option
bulwahn@34948:   val yield : 'a dseq -> int -> bool -> ('a * 'a dseq) option
bulwahn@34948:   val yieldn : int -> 'a dseq -> int -> bool -> 'a list * 'a dseq
bulwahn@34948:   val map : ('a -> 'b) -> 'a dseq -> 'b dseq
bulwahn@34948: end;
bulwahn@34948: 
bulwahn@34948: structure DSequence : DSEQUENCE =
bulwahn@34948: struct
bulwahn@34948: 
bulwahn@34948: type 'a dseq = int -> bool -> 'a Lazy_Sequence.lazy_sequence option
bulwahn@34948: 
bulwahn@34948: val yield = @{code yield}
bulwahn@36024: fun yieldn n s d pol = case s d pol of  
bulwahn@36024:     NONE => ([], fn d => fn pol => NONE)
bulwahn@36024:   | SOME s => let val (xs, s') = Lazy_Sequence.yieldn n s in (xs, fn d => fn pol => SOME s') end
bulwahn@36024: 
bulwahn@34948: val map = @{code map}
bulwahn@34948: 
bulwahn@34948: end;
bulwahn@34948: *}
bulwahn@34948: 
bulwahn@34948: code_reserved Eval DSequence
bulwahn@34948: (*
wenzelm@36176: hide_type Sequence.seq
bulwahn@34948: 
wenzelm@36176: hide_const Sequence.Seq Sequence.yield Sequence.yieldn Sequence.empty Sequence.single
bulwahn@34948:   Sequence.append Sequence.flat Sequence.map Sequence.bind Sequence.ifpred Sequence.not_seq
bulwahn@34948: *)
wenzelm@36176: hide_const (open) empty single eval map_seq bind union if_seq not_seq map
wenzelm@36176: hide_fact (open) empty_def single_def eval.simps map_seq.simps bind_def union_def
bulwahn@34953:   if_seq_def not_seq_def map_def
bulwahn@34948: 
bulwahn@34948: end