Theory Misc_Types

theory Misc_Types
imports BNF_Nonuniform_Fixpoint FSet
(*
Miscellaneous nonuniform (co)datatype definitions.
*)

section ‹Miscellaneous Nonuniform Codatatype Definitions›

theory Misc_Types
imports "../code/BNF_Nonuniform_Fixpoint" "~~/src/HOL/Library/FSet"
begin

nonuniform_datatype 'a plist = PNil | PCons (phd: 'a) (ptl: "('a × 'a) plist")

nonuniform_datatype 'a ptree = Node 'a "'a pforest"
                and 'a pforest = Nil | Cons "'a ptree" "('a × 'a) pforest"

nonuniform_datatype 'a plist' = PNil | 
  PCons1 (phd: 'a) (ptl1: "'a plist'") |
  PCons2 (phd: 'a) (ptl2: "('a × 'a) plist'")
  
nonuniform_datatype ('a, 'b) tplist = PNil 'b | PCons 'a "('a × 'a, unit + 'b) tplist"

nonuniform_datatype 'a stree = Node 'a "'a fset stree fset"

nonuniform_codatatype 'a pstream = Cons (pshd: 'a) (pstl: "('a × 'a) pstream")
  
nonuniform_codatatype ('a, 'b) alter = C 'a "('b, 'a) alter" | D 'a "('b, 'a) alter"

(* doesn't work, since perfect witnesses not derived yet for codatatypes
nonuniform_datatype 'a fractal = F "('a, ('a, 'a) alter fractal) alter"
*)

nonuniform_datatype 'a lam = Var 'a | App "'a lam" "'a lam" | Abs "'a option lam"
  
datatype 'a node = Node2 'a 'a | Node3 'a 'a 'a
datatype 'a digit = One 'a | Two 'a 'a | Three 'a 'a 'a | Four 'a 'a 'a 'a
nonuniform_datatype 'a finger_tree =
    Empty
  | Single 'a
  | Depth "'a digit" "'a node finger_tree" "'a digit"
  
nonuniform_datatype 'a bootstrapped_queue =
    Empty
  | Queue (front: "'a list") (middle: "(unit ⇒ 'a list) bootstrapped_queue")
      (len_front_middle: "nat") (rear: "'a list") (len_rear: "nat")

datatype 'a zero_one = Zero | One 'a
datatype 'a one_two = One 'a | Two 'a 'a
nonuniform_datatype 'a implicit_queue =
    Shallow "'a zero_one"
  | Deep (front: "'a one_two") (middle: "unit ⇒ ('a × 'a) implicit_queue") (rear: "'a zero_one")
  
datatype 'a D = Zero | One 'a | Two 'a 'a | Three 'a 'a 'a
nonuniform_datatype 'a implicit_dequeue =
    Shallow "'a D"
  | Deep (front: "'a D") (middle: "unit ⇒ ('a × 'a) implicit_dequeue") (rear: "'a D")
  
nonuniform_datatype 'a simple_catenable_dequeue =
    Shallow "'a implicit_dequeue"
  | Deep (front: "'a implicit_dequeue") (middle: "unit ⇒ 'a implicit_dequeue simple_catenable_dequeue") (rear: "'a implicit_dequeue")

nonuniform_datatype ('a, 'b) cyclist = CNil | CCons (chd: 'a) (ctl: "('a, 'b option) cyclist") | Cycle 'b
nonuniform_codatatype 'a pllist = PLNil | PLCons (plhd: 'a) (pltl: "('a × 'a) pllist")

end