Data/Collection/Stack.ad

Outline

Content

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
module Data.Collection.Stack (
  Stackdatatype `Data.Collection.Stack.Stack`
   kind `* -> *`
   executable,
  emptyStackconstant `Data.Collection.Stack.emptyStack`
   constant
   type `Stack 'a`
   executable,
  pushconstant `Data.Collection.Stack.push`
   constant
   type `'a -> Stack 'a -> Stack 'a`
   executable,
  popconstant `Data.Collection.Stack.pop`
   constant
   type `Stack 'a -> Maybe ('a, Stack 'a)`
   executable
) where 

import qualified Data.List as List

datatype Stackdatatype `Data.Collection.Stack.Stack`
   kind `* -> *`
   executable 'atype-variable `'a`
   kind `*` := Stack ['atype-variable `'a`
   kind `*`] 

declare emptyStackconstant `Data.Collection.Stack.emptyStack`
   constant
   type `Stack 'a`
   executable :: Stackdatatype `Data.Collection.Stack.Stack`
   kind `* -> *`
   executable 'atype-variable `'a`
   kind `*`
define emptyStackconstant `Data.Collection.Stack.emptyStack`
   constant
   type `Stack 'a`
   executable := Stackconstant `Data.Collection.Stack.Stack`
   constructor of datatype `Stack`
   type `['a] -> Stack 'a`
   executable [] 

declare pushconstant `Data.Collection.Stack.push`
   constant
   type `'a -> Stack 'a -> Stack 'a`
   executable :: 'atype-variable `'a`
   kind `*` -> Stackdatatype `Data.Collection.Stack.Stack`
   kind `* -> *`
   executable 'atype-variable `'a`
   kind `*` -> Stackdatatype `Data.Collection.Stack.Stack`
   kind `* -> *`
   executable 'atype-variable `'a`
   kind `*`
define pushconstant `Data.Collection.Stack.push`
   constant
   type `'a -> Stack 'a -> Stack 'a`
   executable evariable `e`
   type `'a` (Stackconstant `Data.Collection.Stack.Stack`
   constructor of datatype `Stack`
   type `['a] -> Stack 'a`
   executable lvariable `l`
   type `['a]`) := Stackconstant `Data.Collection.Stack.Stack`
   constructor of datatype `Stack`
   type `['a] -> Stack 'a`
   executable (evariable `e`
   type `'a`:constant `Prelude.List.(:)`
   constructor of datatype `List`
   type `'a -> ['a] -> ['a]`
   executablelvariable `l`
   type `['a]`)

declare popconstant `Data.Collection.Stack.pop`
   constant
   type `Stack 'a -> Maybe ('a, Stack 'a)`
   executable :: Stackdatatype `Data.Collection.Stack.Stack`
   kind `* -> *`
   executable 'atype-variable `'a`
   kind `*` -> Maybedatatype `Prelude.Maybe.Maybe`
   kind `* -> *`
   executable ('atype-variable `'a`
   kind `*`, Stackdatatype `Data.Collection.Stack.Stack`
   kind `* -> *`
   executable 'atype-variable `'a`
   kind `*`)
define popconstant `Data.Collection.Stack.pop`
   constant
   type `Stack 'a -> Maybe ('a, Stack 'a)`
   executable (Stackconstant `Data.Collection.Stack.Stack`
   constructor of datatype `Stack`
   type `['a] -> Stack 'a`
   executable (evariable `e`
   type `'a`:constant `Prelude.List.(:)`
   constructor of datatype `List`
   type `'a -> ['a] -> ['a]`
   executablelvariable `l`
   type `['a]`)) := Justconstant `Prelude.Maybe.Just`
   constructor of datatype `Maybe`
   type `'a -> Maybe 'a`
   type in context `('a, Stack 'a) -> Maybe ('a, Stack 'a)`
   executable (evariable `e`
   type `'a`, Stackconstant `Data.Collection.Stack.Stack`
   constructor of datatype `Stack`
   type `['a] -> Stack 'a`
   executable lvariable `l`
   type `['a]`)
     | popconstant `Data.Collection.Stack.pop`
   constant
   type `Stack 'a -> Maybe ('a, Stack 'a)`
   executable (Stackconstant `Data.Collection.Stack.Stack`
   constructor of datatype `Stack`
   type `['a] -> Stack 'a`
   executable []) := Nothingconstant `Prelude.Maybe.Nothing`
   constructor of datatype `Maybe`
   type `Maybe 'a`
   type in context `Maybe ('a, Stack 'a)`
   executable 

declare stackToListconstant `Data.Collection.Stack.stackToList`
   constant
   type `Stack 'a -> ['a]`
   executable :: Stackdatatype `Data.Collection.Stack.Stack`
   kind `* -> *`
   executable 'atype-variable `'a`
   kind `*` -> ['atype-variable `'a`
   kind `*`]
define stackToListconstant `Data.Collection.Stack.stackToList`
   constant
   type `Stack 'a -> ['a]`
   executable (Stackconstant `Data.Collection.Stack.Stack`
   constructor of datatype `Stack`
   type `['a] -> Stack 'a`
   executable lvariable `l`
   type `['a]`) := lvariable `l`
   type `['a]`

declare stackFromListconstant `Data.Collection.Stack.stackFromList`
   constant
   type `['a] -> Stack 'a`
   executable :: ['atype-variable `'a`
   kind `*`] -> Stackdatatype `Data.Collection.Stack.Stack`
   kind `* -> *`
   executable 'atype-variable `'a`
   kind `*`
define stackFromListconstant `Data.Collection.Stack.stackFromList`
   constant
   type `['a] -> Stack 'a`
   executable lvariable `l`
   type `['a]` := Stackconstant `Data.Collection.Stack.Stack`
   constructor of datatype `Stack`
   type `['a] -> Stack 'a`
   executable lvariable `l`
   type `['a]` 

instance Functortype-class `Prelude.Functor.Functor`
   arguments: ('F :: * -> *)
   reserved var-names: 'a, 'b
   statically-resolved Stackdatatype `Data.Collection.Stack.Stack`
   kind `* -> *`
   executable where 
  define fmapconstant `Prelude.Functor.fmap`
   constant of type-class instance `Functor Stack`
   type `('a -> 'b) -> Stack 'a -> Stack 'b`
   executable fvariable `f`
   type `'a -> 'b` (Stackconstant `Data.Collection.Stack.Stack`
   constructor of datatype `Stack`
   type `['a] -> Stack 'a`
   executable lvariable `l`
   type `['a]`) := Stackconstant `Data.Collection.Stack.Stack`
   constructor of datatype `Stack`
   type `['a] -> Stack 'a`
   type in context `['b] -> Stack 'b`
   executable (mapconstant `Prelude.List.map`
   constant
   type `('a -> 'b) -> ['a] -> ['b]`
   executable fvariable `f`
   type `'a -> 'b` lvariable `l`
   type `['a]`)
end-instance

instance EqPtype-class `Prelude.Eq.EqP`
   arguments: ('a :: *)
   has default derive templates
   derive-template labels
     - eq (only deriving)
     - full 'atype-variable `'a`
   kind `*` => EqPtype-class `Prelude.Eq.EqP`
   arguments: ('a :: *)
   has default derive templates
   derive-template labels
     - eq (only deriving)
     - full (Stackdatatype `Data.Collection.Stack.Stack`
   kind `* -> *`
   executable 'atype-variable `'a`
   kind `*`) where 
  define non-exec (===)constant `Prelude.Eq.(===)`
   constant of type-class instance `EqP 'a => EqP (Stack 'a)`
   type `Stack 'a -> Stack 'a -> Prop`
   non-executable q1variable `q1`
   type `Stack 'a` q2variable `q2`
   type `Stack 'a` := (stackToListconstant `Data.Collection.Stack.stackToList`
   constant
   type `Stack 'a -> ['a]`
   executable q1variable `q1`
   type `Stack 'a`) ===constant `Prelude.Eq.(===)`
   constant of type-class `EqP`
   type `'a -> 'a -> Prop`
   type in context `['a] -> ['a] -> Prop`
   non-executable
   statically resolved type-class instance (stackToListconstant `Data.Collection.Stack.stackToList`
   constant
   type `Stack 'a -> ['a]`
   executable q2variable `q2`
   type `Stack 'a`)
end-instance

instance Eqtype-class `Prelude.Eq.Eq`
   arguments: ('a :: *)
   super-class constraints:
     - Prelude.Eq.EqP 'a
   has default derive templates 'atype-variable `'a`
   kind `*` => Eqtype-class `Prelude.Eq.Eq`
   arguments: ('a :: *)
   super-class constraints:
     - Prelude.Eq.EqP 'a
   has default derive templates (Stackdatatype `Data.Collection.Stack.Stack`
   kind `* -> *`
   executable 'atype-variable `'a`
   kind `*`) where 
  define (==)constant `Prelude.Eq.(==)`
   constant of type-class instance `Eq 'a => Eq (Stack 'a)`
   type `Stack 'a -> Stack 'a -> Bool`
   executable q1variable `q1`
   type `Stack 'a` q2variable `q2`
   type `Stack 'a` := (stackToListconstant `Data.Collection.Stack.stackToList`
   constant
   type `Stack 'a -> ['a]`
   executable q1variable `q1`
   type `Stack 'a`) ==constant `Prelude.Eq.(==)`
   constant of type-class `Eq`
   type `'a -> 'a -> Bool`
   type in context `['a] -> ['a] -> Bool`
   executable
   statically resolved type-class instance (stackToListconstant `Data.Collection.Stack.stackToList`
   constant
   type `Stack 'a -> ['a]`
   executable q2variable `q2`
   type `Stack 'a`)
end-instance

instance Ordtype-class `Prelude.Ord.Ord`
   arguments: ('a :: *)
   super-class constraints:
     - Prelude.Eq.Eq 'a
   has default derive templates 'atype-variable `'a`
   kind `*` => Ordtype-class `Prelude.Ord.Ord`
   arguments: ('a :: *)
   super-class constraints:
     - Prelude.Eq.Eq 'a
   has default derive templates (Stackdatatype `Data.Collection.Stack.Stack`
   kind `* -> *`
   executable 'atype-variable `'a`
   kind `*`) where 
  define compareconstant `Prelude.Ord.compare`
   constant of type-class instance `Ord 'a => Ord (Stack 'a)`
   type `Stack 'a -> Stack 'a -> Ordering`
   executable q1variable `q1`
   type `Stack 'a` q2variable `q2`
   type `Stack 'a` := compareconstant `Prelude.Ord.compare`
   constant of type-class `Ord`
   type `'a -> 'a -> Ordering`
   type in context `['a] -> ['a] -> Ordering`
   executable
   statically resolved type-class instance (stackToListconstant `Data.Collection.Stack.stackToList`
   constant
   type `Stack 'a -> ['a]`
   executable q1variable `q1`
   type `Stack 'a`) (stackToListconstant `Data.Collection.Stack.stackToList`
   constant
   type `Stack 'a -> ['a]`
   executable q2variable `q2`
   type `Stack 'a`)
end-instance

instance Semigrouptype-class `Prelude.BasicClasses.Semigroup`
   arguments: ('a :: *) (Stackdatatype `Data.Collection.Stack.Stack`
   kind `* -> *`
   executable 'atype-variable `'a`
   kind `*`) where 
  define (<>)constant `Prelude.BasicClasses.(<>)`
   constant of type-class instance `Semigroup (Stack 'a)`
   type `Stack 'a -> Stack 'a -> Stack 'a`
   executable q1variable `q1`
   type `Stack 'a` q2variable `q2`
   type `Stack 'a` := stackFromListconstant `Data.Collection.Stack.stackFromList`
   constant
   type `['a] -> Stack 'a`
   executable ((stackToListconstant `Data.Collection.Stack.stackToList`
   constant
   type `Stack 'a -> ['a]`
   executable q1variable `q1`
   type `Stack 'a`) ++constant `Prelude.List.(++)`
   constant
   type `['a] -> ['a] -> ['a]`
   executable (stackToListconstant `Data.Collection.Stack.stackToList`
   constant
   type `Stack 'a -> ['a]`
   executable q2variable `q2`
   type `Stack 'a`))
end-instance

instance Monoidtype-class `Prelude.BasicClasses.Monoid`
   arguments: ('a :: *)
   super-class constraints:
     - Prelude.BasicClasses.Semigroup 'a (Stackdatatype `Data.Collection.Stack.Stack`
   kind `* -> *`
   executable 'atype-variable `'a`
   kind `*`) where 
  define memptyconstant `Prelude.BasicClasses.mempty`
   constant of type-class instance `Monoid (Stack 'a)`
   type `Stack 'a`
   executable := emptyStackconstant `Data.Collection.Stack.emptyStack`
   constant
   type `Stack 'a`
   executable
  {-# inline memptyconstant `Prelude.BasicClasses.mempty`
   constant of type-class instance `Monoid (Stack 'a)`
   type `Stack 'a`
   executable #-}
end-instance

instance CollectionWithEmptynessTesttype-class `Prelude.Collection.CollectionWithEmptynessTest`
   arguments: ('c :: *) ('e :: *)
   functional deps: 'c -> 'e
   super-class constraints:
     - Prelude.Collection.Collection 'c 'e (Stackdatatype `Data.Collection.Stack.Stack`
   kind `* -> *`
   executable 'etype-variable `'e`
   kind `*`) 'etype-variable `'e`
   kind `*` where
  define isEmptyconstant `Prelude.Collection.isEmpty`
   constant of type-class instance `CollectionWithEmptynessTest (Stack 'e) 'e`
   type `Stack 'e -> Bool`
   executable (Stackconstant `Data.Collection.Stack.Stack`
   constructor of datatype `Stack`
   type `['a] -> Stack 'a`
   type in context `['e] -> Stack 'e`
   executable lvariable `l`
   type `['e]`) := (nullconstant `Prelude.Foldable.null`
   constant of type-class `Foldable`
   type `'t -> Bool`
   type in context `['e] -> Bool`
   executable
   statically resolved type-class instance lvariable `l`
   type `['e]`)
end-instance

instance Collectiontype-class `Prelude.Collection.Collection`
   arguments: ('c :: *) ('e :: *)
   functional deps: 'c -> 'e
   super-class constraints:
     - Prelude.BasicClasses.Monoid 'c (Stackdatatype `Data.Collection.Stack.Stack`
   kind `* -> *`
   executable 'etype-variable `'e`
   kind `*`) 'etype-variable `'e`
   kind `*` where
  define insertconstant `Prelude.Collection.insert`
   constant of type-class instance `Collection (Stack 'e) 'e`
   type `'e -> Stack 'e -> Stack 'e`
   executable := pushconstant `Data.Collection.Stack.push`
   constant
   type `'a -> Stack 'a -> Stack 'a`
   type in context `'e -> Stack 'e -> Stack 'e`
   executable
  {-# inline insertconstant `Prelude.Collection.insert`
   constant of type-class instance `Collection (Stack 'e) 'e`
   type `'e -> Stack 'e -> Stack 'e`
   executable #-}

  define fromListconstant `Prelude.Collection.fromList`
   constant of type-class instance `Collection (Stack 'e) 'e`
   type `['e] -> Stack 'e`
   executable := stackFromListconstant `Data.Collection.Stack.stackFromList`
   constant
   type `['a] -> Stack 'a`
   type in context `['e] -> Stack 'e`
   executable
  {-# inline fromListconstant `Prelude.Collection.fromList`
   constant of type-class instance `Collection (Stack 'e) 'e`
   type `['e] -> Stack 'e`
   executable #-}

  define non-exec isEmptyPconstant `Prelude.Collection.isEmptyP`
   constant of type-class instance `Collection (Stack 'e) 'e`
   type `Stack 'e -> Prop`
   non-executable qvariable `q`
   type `Stack 'e` := bool2propconstant `Prelude.Bool.bool2prop`
   constant
   type `Bool -> Prop`
   non-executable (isEmptyconstant `Prelude.Collection.isEmpty`
   constant of type-class `CollectionWithEmptynessTest`
   type `'c -> Bool`
   type in context `Stack 'e -> Bool`
   executable
   statically resolved type-class instance qvariable `q`
   type `Stack 'e`)
  define non-exec memberPconstant `Prelude.Collection.memberP`
   constant of type-class instance `Collection (Stack 'e) 'e`
   type `EqP 'e => 'e -> Stack 'e -> Prop`
   non-executable evariable `e`
   type `'e` (Stackconstant `Data.Collection.Stack.Stack`
   constructor of datatype `Stack`
   type `['a] -> Stack 'a`
   type in context `['e] -> Stack 'e`
   executable lvariable `l`
   type `['e]`) := List.elemPconstant `Prelude.List.elemP`
   constant
   type `EqP 'a => 'a -> ['a] -> Prop`
   type in context `'e -> ['e] -> Prop`
   non-executable evariable `e`
   type `'e` lvariable `l`
   type `['e]`
end-instance

instance Foldabletype-class `Prelude.Foldable.Foldable`
   arguments: ('t :: *) ('e :: *)
   functional deps: 't -> 'e
   reserved var-names: 'acc (Stackdatatype `Data.Collection.Stack.Stack`
   kind `* -> *`
   executable 'etype-variable `'e`
   kind `*`) 'etype-variable `'e`
   kind `*` where
  define toListconstant `Prelude.Foldable.toList`
   constant of type-class instance `Foldable (Stack 'e) 'e`
   type `Stack 'e -> ['e]`
   executable := stackToListconstant `Data.Collection.Stack.stackToList`
   constant
   type `Stack 'a -> ['a]`
   type in context `Stack 'e -> ['e]`
   executable
  {-# inline toListconstant `Prelude.Foldable.toList`
   constant of type-class instance `Foldable (Stack 'e) 'e`
   type `Stack 'e -> ['e]`
   executable #-}
end-instance

instance Eqtype-class `Prelude.Eq.Eq`
   arguments: ('a :: *)
   super-class constraints:
     - Prelude.Eq.EqP 'a
   has default derive templates 'etype-variable `'e`
   kind `*` => CollectionWithMembershipTesttype-class `Prelude.Collection.CollectionWithMembershipTest`
   arguments: ('c :: *) ('e :: *)
   functional deps: 'c -> 'e
   super-class constraints:
     - Prelude.Collection.Collection 'c 'e (Stackdatatype `Data.Collection.Stack.Stack`
   kind `* -> *`
   executable 'etype-variable `'e`
   kind `*`) 'etype-variable `'e`
   kind `*` where
  define occurconstant `Prelude.Collection.occur`
   constant of type-class instance `Eq 'e => CollectionWithMembershipTest (Stack 'e) 'e`
   type `Eq 'e => 'e -> Stack 'e -> Natural`
   executable evariable `e`
   type `'e` (Stackconstant `Data.Collection.Stack.Stack`
   constructor of datatype `Stack`
   type `['a] -> Stack 'a`
   type in context `['e] -> Stack 'e`
   executable lvariable `l`
   type `['e]`) := countconstant `Prelude.List.count`
   constant
   type `Eq 'a => 'a -> ['a] -> Natural`
   type in context `'e -> ['e] -> Natural`
   executable evariable `e`
   type `'e` lvariable `l`
   type `['e]`
  define memberconstant `Prelude.Collection.member`
   constant of type-class instance `Eq 'e => CollectionWithMembershipTest (Stack 'e) 'e`
   type `Eq 'e => 'e -> Stack 'e -> Bool`
   executable := elemconstant `Prelude.Foldable.elem`
   constant of type-class `Foldable`
   type `Eq 'e => 'e -> 't -> Bool`
   type in context `'e -> Stack 'e -> Bool`
   executable
   statically resolved type-class instance
  {-# inline memberconstant `Prelude.Collection.member`
   constant of type-class instance `Eq 'e => CollectionWithMembershipTest (Stack 'e) 'e`
   type `Eq 'e => 'e -> Stack 'e -> Bool`
   executable #-}  
end-instance

instance Eqtype-class `Prelude.Eq.Eq`
   arguments: ('a :: *)
   super-class constraints:
     - Prelude.Eq.EqP 'a
   has default derive templates 'etype-variable `'e`
   kind `*` => FiniteCollectiontype-class `Prelude.Collection.FiniteCollection`
   arguments: ('c :: *) ('e :: *)
   functional deps: 'c -> 'e
   super-class constraints:
     - Prelude.Collection.CollectionWithMembershipTest 'c 'e
     - Prelude.Foldable.Foldable 'c 'e
     - Prelude.Collection.CollectionWithEmptynessTest 'c 'e (Stackdatatype `Data.Collection.Stack.Stack`
   kind `* -> *`
   executable 'etype-variable `'e`
   kind `*`) 'etype-variable `'e`
   kind `*` where
end-instance

end-moduleend of module Data.Collection.Stack