Data/List.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.List (
  module Prelude.List,
  replicateconstant `Data.List.replicate`
   constant
   type `Natural -> 'a -> ['a]`
   executable,
  takeconstant `Data.List.take`
   constant
   type `Natural -> ['a] -> ['a]`
   executable,
  dropconstant `Data.List.drop`
   constant
   type `Natural -> ['a] -> ['a]`
   executable,
  splitAtconstant `Data.List.splitAt`
   constant
   type `Natural -> ['a] -> (['a], ['a])`
   executable,
  takeWhileconstant `Data.List.takeWhile`
   constant
   type `('a -> Bool) -> ['a] -> ['a]`
   executable,
  dropWhileconstant `Data.List.dropWhile`
   constant
   type `('a -> Bool) -> ['a] -> ['a]`
   executable,
  breakconstant `Data.List.break`
   constant
   type `('a -> Bool) -> ['a] -> (['a], ['a])`
   executable,
  spanconstant `Data.List.span`
   constant
   type `('a -> Bool) -> ['a] -> (['a], ['a])`
   executable,
  lookupconstant `Data.List.lookup`
   constant
   type `Eq 'k => 'k -> [('k, 'v)] -> Maybe 'v`
   executable,
  zipconstant `Data.List.zip`
   constant
   type `['a] -> ['b] -> [('a, 'b)]`
   executable,
  unzipconstant `Data.List.unzip`
   constant
   type `[('a, 'b)] -> (['a], ['b])`
   executable
) where

declare replicateconstant `Data.List.replicate`
   constant
   type `Natural -> 'a -> ['a]`
   executable :: Naturaldatatype `Prelude.Num.Natural`
   kind `*`
   executable -> 'atype-variable `'a`
   kind `*` -> ['atype-variable `'a`
   kind `*`]
define rec replicateconstant `Data.List.replicate`
   constant
   type `Natural -> 'a -> ['a]`
   executable 0natural number literal
   type `Natural`
   decimal value: 0
   hexadecimal value: 0x0
   octal value: 0o0
   binary value: 0b0 _ := []
         | replicateconstant `Data.List.replicate`
   constant
   type `Natural -> 'a -> ['a]`
   executable nvariable `n`
   type `Natural` avariable `a`
   type `'a` := avariable `a`
   type `'a` :constant `Prelude.List.(:)`
   constructor of datatype `List`
   type `'a -> ['a] -> ['a]`
   executable (replicateconstant `Data.List.replicate` (recursive usage)
   constant
   type `Natural -> 'a -> ['a]`
   executable (predconstant `Prelude.BasicClasses.pred`
   constant of type-class `Enum`
   type `'a -> 'a`
   type in context `Natural -> Natural`
   executable
   statically resolved type-class instance nvariable `n`
   type `Natural`) avariable `a`
   type `'a`)

declare takeconstant `Data.List.take`
   constant
   type `Natural -> ['a] -> ['a]`
   executable :: Naturaldatatype `Prelude.Num.Natural`
   kind `*`
   executable -> ['atype-variable `'a`
   kind `*`] -> ['atype-variable `'a`
   kind `*`]
define rec takeconstant `Data.List.take`
   constant
   type `Natural -> ['a] -> ['a]`
   executable 0natural number literal
   type `Natural`
   decimal value: 0
   hexadecimal value: 0x0
   octal value: 0o0
   binary value: 0b0 _ := []
         | takeconstant `Data.List.take`
   constant
   type `Natural -> ['a] -> ['a]`
   executable _ [] := []
         | takeconstant `Data.List.take`
   constant
   type `Natural -> ['a] -> ['a]`
   executable nvariable `n`
   type `Natural` (xvariable `x`
   type `'a`:constant `Prelude.List.(:)`
   constructor of datatype `List`
   type `'a -> ['a] -> ['a]`
   executablexsvariable `xs`
   type `['a]`) := xvariable `x`
   type `'a` :constant `Prelude.List.(:)`
   constructor of datatype `List`
   type `'a -> ['a] -> ['a]`
   executable (takeconstant `Data.List.take` (recursive usage)
   constant
   type `Natural -> ['a] -> ['a]`
   executable (predconstant `Prelude.BasicClasses.pred`
   constant of type-class `Enum`
   type `'a -> 'a`
   type in context `Natural -> Natural`
   executable
   statically resolved type-class instance nvariable `n`
   type `Natural`) xsvariable `xs`
   type `['a]`)

declare dropconstant `Data.List.drop`
   constant
   type `Natural -> ['a] -> ['a]`
   executable :: Naturaldatatype `Prelude.Num.Natural`
   kind `*`
   executable -> ['atype-variable `'a`
   kind `*`] -> ['atype-variable `'a`
   kind `*`]
define rec dropconstant `Data.List.drop`
   constant
   type `Natural -> ['a] -> ['a]`
   executable 0natural number literal
   type `Natural`
   decimal value: 0
   hexadecimal value: 0x0
   octal value: 0o0
   binary value: 0b0 lvariable `l`
   type `['a]` := lvariable `l`
   type `['a]`
         | dropconstant `Data.List.drop`
   constant
   type `Natural -> ['a] -> ['a]`
   executable _ [] := []
         | dropconstant `Data.List.drop`
   constant
   type `Natural -> ['a] -> ['a]`
   executable nvariable `n`
   type `Natural` (_:constant `Prelude.List.(:)`
   constructor of datatype `List`
   type `'a -> ['a] -> ['a]`
   executablexsvariable `xs`
   type `['a]`) := dropconstant `Data.List.drop` (recursive usage)
   constant
   type `Natural -> ['a] -> ['a]`
   executable (predconstant `Prelude.BasicClasses.pred`
   constant of type-class `Enum`
   type `'a -> 'a`
   type in context `Natural -> Natural`
   executable
   statically resolved type-class instance nvariable `n`
   type `Natural`) xsvariable `xs`
   type `['a]`

declare splitAtconstant `Data.List.splitAt`
   constant
   type `Natural -> ['a] -> (['a], ['a])`
   executable :: Naturaldatatype `Prelude.Num.Natural`
   kind `*`
   executable -> ['atype-variable `'a`
   kind `*`] -> (['atype-variable `'a`
   kind `*`], ['atype-variable `'a`
   kind `*`])
define rec splitAtconstant `Data.List.splitAt`
   constant
   type `Natural -> ['a] -> (['a], ['a])`
   executable 0natural number literal
   type `Natural`
   decimal value: 0
   hexadecimal value: 0x0
   octal value: 0o0
   binary value: 0b0 lvariable `l`
   type `['a]` := ([], lvariable `l`
   type `['a]`)
         | splitAtconstant `Data.List.splitAt`
   constant
   type `Natural -> ['a] -> (['a], ['a])`
   executable _ [] := ([], [])
         | splitAtconstant `Data.List.splitAt`
   constant
   type `Natural -> ['a] -> (['a], ['a])`
   executable nvariable `n`
   type `Natural` (xvariable `x`
   type `'a`:constant `Prelude.List.(:)`
   constructor of datatype `List`
   type `'a -> ['a] -> ['a]`
   executablexsvariable `xs`
   type `['a]`) :=
             let
               val (ltvariable `lt`
   type `['a]`, ldvariable `ld`
   type `['a]`) = (splitAtconstant `Data.List.splitAt` (recursive usage)
   constant
   type `Natural -> ['a] -> (['a], ['a])`
   executable (predconstant `Prelude.BasicClasses.pred`
   constant of type-class `Enum`
   type `'a -> 'a`
   type in context `Natural -> Natural`
   executable
   statically resolved type-class instance nvariable `n`
   type `Natural`) xsvariable `xs`
   type `['a]`)
             in
               (xvariable `x`
   type `'a`:constant `Prelude.List.(:)`
   constructor of datatype `List`
   type `'a -> ['a] -> ['a]`
   executableltvariable `lt`
   type `['a]`, ldvariable `ld`
   type `['a]`)
             end

property EqPtype-class `Prelude.Eq.EqP`
   arguments: ('a :: *)
   has default derive templates
   derive-template labels
     - eq (only deriving)
     - full 'atype-variable `'a`
   kind `*` => splitAt_take_dropconstant `Data.List.splitAt_take_drop`
   property
   type `EqP 'a => Natural -> ['a] -> Prop`
   non-executable nvariable `n`
   type `Natural` (lvariable `l`
   type `['a]` :: ['atype-variable `'a`
   kind `*`]) := ((splitAtconstant `Data.List.splitAt`
   constant
   type `Natural -> ['a] -> (['a], ['a])`
   executable nvariable `n`
   type `Natural` lvariable `l`
   type `['a]`) ===constant `Prelude.Eq.(===)`
   constant of type-class `EqP`
   type `'a -> 'a -> Prop`
   type in context `(['a], ['a]) -> (['a], ['a]) -> Prop`
   non-executable
   statically resolved type-class instance (takeconstant `Data.List.take`
   constant
   type `Natural -> ['a] -> ['a]`
   executable nvariable `n`
   type `Natural` lvariable `l`
   type `['a]`, dropconstant `Data.List.drop`
   constant
   type `Natural -> ['a] -> ['a]`
   executable nvariable `n`
   type `Natural` lvariable `l`
   type `['a]`))


declare takeWhileconstant `Data.List.takeWhile`
   constant
   type `('a -> Bool) -> ['a] -> ['a]`
   executable :: ('atype-variable `'a`
   kind `*` -> Booldatatype `Prelude.Bool.Bool`
   kind `*`
   executable) -> ['atype-variable `'a`
   kind `*`] -> ['atype-variable `'a`
   kind `*`]
define rec takeWhileconstant `Data.List.takeWhile`
   constant
   type `('a -> Bool) -> ['a] -> ['a]`
   executable _ [] := []
         | takeWhileconstant `Data.List.takeWhile`
   constant
   type `('a -> Bool) -> ['a] -> ['a]`
   executable pvariable `p`
   type `'a -> Bool` (xvariable `x`
   type `'a`:constant `Prelude.List.(:)`
   constructor of datatype `List`
   type `'a -> ['a] -> ['a]`
   executablexsvariable `xs`
   type `['a]`) :=
             if (pvariable `p`
   type `'a -> Bool` xvariable `x`
   type `'a`) then xvariable `x`
   type `'a` :constant `Prelude.List.(:)`
   constructor of datatype `List`
   type `'a -> ['a] -> ['a]`
   executable (takeWhileconstant `Data.List.takeWhile` (recursive usage)
   constant
   type `('a -> Bool) -> ['a] -> ['a]`
   executable pvariable `p`
   type `'a -> Bool` xsvariable `xs`
   type `['a]`) else []

declare dropWhileconstant `Data.List.dropWhile`
   constant
   type `('a -> Bool) -> ['a] -> ['a]`
   executable :: ('atype-variable `'a`
   kind `*` -> Booldatatype `Prelude.Bool.Bool`
   kind `*`
   executable) -> ['atype-variable `'a`
   kind `*`] -> ['atype-variable `'a`
   kind `*`]
define rec dropWhileconstant `Data.List.dropWhile`
   constant
   type `('a -> Bool) -> ['a] -> ['a]`
   executable _ [] := []
         | dropWhileconstant `Data.List.dropWhile`
   constant
   type `('a -> Bool) -> ['a] -> ['a]`
   executable pvariable `p`
   type `'a -> Bool` (xvariable `x`
   type `'a`:constant `Prelude.List.(:)`
   constructor of datatype `List`
   type `'a -> ['a] -> ['a]`
   executablexsvariable `xs`
   type `['a]`) :=
             if (pvariable `p`
   type `'a -> Bool` xvariable `x`
   type `'a`) then (dropWhileconstant `Data.List.dropWhile` (recursive usage)
   constant
   type `('a -> Bool) -> ['a] -> ['a]`
   executable pvariable `p`
   type `'a -> Bool` xsvariable `xs`
   type `['a]`) else (xvariable `x`
   type `'a`:constant `Prelude.List.(:)`
   constructor of datatype `List`
   type `'a -> ['a] -> ['a]`
   executablexsvariable `xs`
   type `['a]`)

declare spanconstant `Data.List.span`
   constant
   type `('a -> Bool) -> ['a] -> (['a], ['a])`
   executable :: ('atype-variable `'a`
   kind `*` -> Booldatatype `Prelude.Bool.Bool`
   kind `*`
   executable) -> ['atype-variable `'a`
   kind `*`] -> (['atype-variable `'a`
   kind `*`], ['atype-variable `'a`
   kind `*`])
define rec spanconstant `Data.List.span`
   constant
   type `('a -> Bool) -> ['a] -> (['a], ['a])`
   executable _ [] := ([], [])
         | spanconstant `Data.List.span`
   constant
   type `('a -> Bool) -> ['a] -> (['a], ['a])`
   executable pvariable `p`
   type `'a -> Bool` (xvariable `x`
   type `'a`:constant `Prelude.List.(:)`
   constructor of datatype `List`
   type `'a -> ['a] -> ['a]`
   executablexsvariable `xs`
   type `['a]`) :=
             if (pvariable `p`
   type `'a -> Bool` xvariable `x`
   type `'a`) then
               let val (ysvariable `ys`
   type `['a]`, zsvariable `zs`
   type `['a]`) = spanconstant `Data.List.span` (recursive usage)
   constant
   type `('a -> Bool) -> ['a] -> (['a], ['a])`
   executable pvariable `p`
   type `'a -> Bool` xsvariable `xs`
   type `['a]` in
                  (xvariable `x`
   type `'a`:constant `Prelude.List.(:)`
   constructor of datatype `List`
   type `'a -> ['a] -> ['a]`
   executableysvariable `ys`
   type `['a]`, zsvariable `zs`
   type `['a]`)
               end
             else ([], xvariable `x`
   type `'a`:constant `Prelude.List.(:)`
   constructor of datatype `List`
   type `'a -> ['a] -> ['a]`
   executablexsvariable `xs`
   type `['a]`)

declare breakconstant `Data.List.break`
   constant
   type `('a -> Bool) -> ['a] -> (['a], ['a])`
   executable :: ('atype-variable `'a`
   kind `*` -> Booldatatype `Prelude.Bool.Bool`
   kind `*`
   executable) -> ['atype-variable `'a`
   kind `*`] -> (['atype-variable `'a`
   kind `*`], ['atype-variable `'a`
   kind `*`])
define breakconstant `Data.List.break`
   constant
   type `('a -> Bool) -> ['a] -> (['a], ['a])`
   executable pvariable `p`
   type `'a -> Bool` := spanconstant `Data.List.span`
   constant
   type `('a -> Bool) -> ['a] -> (['a], ['a])`
   executable (notconstant `Prelude.Bool.not`
   constant
   type `Bool -> Bool`
   executable .constant `Prelude.Function.(.)`
   constant of type-class `Dot`
   type `'a -> 'b -> 'c`
   type in context `(Bool -> Bool) -> ('a -> Bool) -> 'a -> Bool`
   executable
   statically resolved type-class instance pvariable `p`
   type `'a -> Bool`)


declare lookupconstant `Data.List.lookup`
   constant
   type `Eq 'k => 'k -> [('k, 'v)] -> Maybe 'v`
   executable :: Eqtype-class `Prelude.Eq.Eq`
   arguments: ('a :: *)
   super-class constraints:
     - Prelude.Eq.EqP 'a
   has default derive templates 'ktype-variable `'k`
   kind `*` => 'ktype-variable `'k`
   kind `*` -> [('ktype-variable `'k`
   kind `*`, 'vtype-variable `'v`
   kind `*`)] -> Maybedatatype `Prelude.Maybe.Maybe`
   kind `* -> *`
   executable 'vtype-variable `'v`
   kind `*`
define rec lookupconstant `Data.List.lookup`
   constant
   type `Eq 'k => 'k -> [('k, 'v)] -> Maybe 'v`
   executable _keyvariable `_key`
   type `'k` [] := Nothingconstant `Prelude.Maybe.Nothing`
   constructor of datatype `Maybe`
   type `Maybe 'a`
   type in context `Maybe 'v`
   executable
         | lookupconstant `Data.List.lookup`
   constant
   type `Eq 'k => 'k -> [('k, 'v)] -> Maybe 'v`
   executable keyvariable `key`
   type `'k` ((kvariable `k`
   type `'k`, vvariable `v`
   type `'v`):constant `Prelude.List.(:)`
   constructor of datatype `List`
   type `'a -> ['a] -> ['a]`
   type in context `('k, 'v) -> [('k, 'v)] -> [('k, 'v)]`
   executablekvsvariable `kvs`
   type `[('k, 'v)]`) :=
             if (keyvariable `key`
   type `'k` ==constant `Prelude.Eq.(==)`
   constant of type-class `Eq`
   type `'a -> 'a -> Bool`
   type in context `'k -> 'k -> Bool`
   executable
   type-class instance from argument kvariable `k`
   type `'k`) then Justconstant `Prelude.Maybe.Just`
   constructor of datatype `Maybe`
   type `'a -> Maybe 'a`
   type in context `'v -> Maybe 'v`
   executable vvariable `v`
   type `'v` else lookupconstant `Data.List.lookup` (recursive usage)
   constant
   type `Eq 'k => 'k -> [('k, 'v)] -> Maybe 'v`
   executable keyvariable `key`
   type `'k` kvsvariable `kvs`
   type `[('k, 'v)]`


declare zipWithconstant `Data.List.zipWith`
   constant
   type `('a -> 'b -> 'c) -> ['a] -> ['b] -> ['c]`
   executable :: ('atype-variable `'a`
   kind `*` -> 'btype-variable `'b`
   kind `*` -> 'ctype-variable `'c`
   kind `*`) -> ['atype-variable `'a`
   kind `*`] -> ['btype-variable `'b`
   kind `*`] -> ['ctype-variable `'c`
   kind `*`]
define rec zipWithconstant `Data.List.zipWith`
   constant
   type `('a -> 'b -> 'c) -> ['a] -> ['b] -> ['c]`
   executable fvariable `f`
   type `'a -> 'b -> 'c` (xvariable `x`
   type `'a`:constant `Prelude.List.(:)`
   constructor of datatype `List`
   type `'a -> ['a] -> ['a]`
   executablexsvariable `xs`
   type `['a]`) (yvariable `y`
   type `'b`:constant `Prelude.List.(:)`
   constructor of datatype `List`
   type `'a -> ['a] -> ['a]`
   type in context `'b -> ['b] -> ['b]`
   executableysvariable `ys`
   type `['b]`) := (fvariable `f`
   type `'a -> 'b -> 'c` xvariable `x`
   type `'a` yvariable `y`
   type `'b`):constant `Prelude.List.(:)`
   constructor of datatype `List`
   type `'a -> ['a] -> ['a]`
   type in context `'c -> ['c] -> ['c]`
   executable(zipWithconstant `Data.List.zipWith` (recursive usage)
   constant
   type `('a -> 'b -> 'c) -> ['a] -> ['b] -> ['c]`
   executable fvariable `f`
   type `'a -> 'b -> 'c` xsvariable `xs`
   type `['a]` ysvariable `ys`
   type `['b]`)
         | zipWithconstant `Data.List.zipWith`
   constant
   type `('a -> 'b -> 'c) -> ['a] -> ['b] -> ['c]`
   executable _ _ _ := undefinedconstant `Prelude.Default.undefined`
   constant of type-class `Default`
   type `'a`
   type in context `['c]`
   executable
   statically resolved type-class instance

declare zipconstant `Data.List.zip`
   constant
   type `['a] -> ['b] -> [('a, 'b)]`
   executable :: ['atype-variable `'a`
   kind `*`] -> ['btype-variable `'b`
   kind `*`] -> [('atype-variable `'a`
   kind `*`, 'btype-variable `'b`
   kind `*`)]
define zipconstant `Data.List.zip`
   constant
   type `['a] -> ['b] -> [('a, 'b)]`
   executable := zipWithconstant `Data.List.zipWith`
   constant
   type `('a -> 'b -> 'c) -> ['a] -> ['b] -> ['c]`
   type in context `('a -> 'b -> ('a, 'b)) -> ['a] -> ['b] -> [('a, 'b)]`
   executable (fntype `'a -> 'b -> ('a, 'b)` xvariable `x`
   type `'a` yvariable `y`
   type `'b` -> (xvariable `x`
   type `'a`, yvariable `y`
   type `'b`))

declare unzipconstant `Data.List.unzip`
   constant
   type `[('a, 'b)] -> (['a], ['b])`
   executable :: [('atype-variable `'a`
   kind `*`,'btype-variable `'b`
   kind `*`)] -> (['atype-variable `'a`
   kind `*`],['btype-variable `'b`
   kind `*`])
define unzipconstant `Data.List.unzip`
   constant
   type `[('a, 'b)] -> (['a], ['b])`
   executable :=  foldrconstant `Prelude.Foldable.foldr`
   statically resolved constant of type-class `Foldable`
   type `('e -> 'acc -> 'acc) -> 'acc -> 't -> 'acc`
   type in context `(('a, 'b) -> (['a], ['b]) -> (['a], ['b])) -> (['a], ['b]) -> [('a, 'b)] -> (['a], ['b])`
   executable
   statically resolved type-class instance (fntype `('a, 'b) -> (['a], ['b]) -> (['a], ['b])` (xvariable `x`
   type `'a`,yvariable `y`
   type `'b`) (xsvariable `xs`
   type `['a]`,ysvariable `ys`
   type `['b]`) -> (xvariable `x`
   type `'a`:constant `Prelude.List.(:)`
   constructor of datatype `List`
   type `'a -> ['a] -> ['a]`
   executablexsvariable `xs`
   type `['a]`,yvariable `y`
   type `'b`:constant `Prelude.List.(:)`
   constructor of datatype `List`
   type `'a -> ['a] -> ['a]`
   type in context `'b -> ['b] -> ['b]`
   executableysvariable `ys`
   type `['b]`)) ([],[])

end-moduleend of module Data.List