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
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
|
module Prelude.Num (
NumPlustype-class `Prelude.Num.NumPlus`
arguments: ('a :: *)(..)class-constant `(+)`
,
NumMinustype-class `Prelude.Num.NumMinus`
arguments: ('a :: *)(..)class-constant `(-)`
,
NumMulttype-class `Prelude.Num.NumMult`
arguments: ('a :: *)(..)class-constant `(*)`
,
NumDivtype-class `Prelude.Num.NumDiv`
arguments: ('a :: *)(..)class-constant `(/)`
,
NumDivModtype-class `Prelude.Num.NumDivMod`
arguments: ('a :: *)(..)class-constant `div`
class-constant `divmod`
class-constant `mod`
,
Naturaldatatype `Prelude.Num.Natural`
kind `*`
executable(..)case-constant `caseNatural`
constructor `Zero`
constructor `Suc`
) where
{-# NoImplicitPrelude #-}
import Prelude.Bool
import Prelude.Default
import Prelude.Eq
import Prelude.Ord
import Prelude.Literal
import Prelude.Tuple
datatype rec Naturaldatatype `Prelude.Num.Natural`
kind `*`
executable :=
Zero
| Suc Naturaldatatype `Prelude.Num.Natural`
kind `*`
executable
instance Defaulttype-class `Prelude.Default.Default`
arguments: ('a :: *)
has default derive templates Naturaldatatype `Prelude.Num.Natural`
kind `*`
executable where
define defaultconstant `Prelude.Default.default`
constant of type-class instance `Default Natural`
type `Natural`
executable := Zeroconstant `Prelude.Num.Zero`
constructor of datatype `Natural`
type `Natural`
executable
{-# inline defaultconstant `Prelude.Default.default`
constant of type-class instance `Default Natural`
type `Natural`
executable #-}
end-instance
derive Naturaldatatype `Prelude.Num.Natural`
kind `*`
executable instances (EqPtype-class `Prelude.Eq.EqP`
arguments: ('a :: *)
has default derive templates
derive-template labels
- eq (only deriving)
- full
generated code:
instance EqP Natural where
define non-exec (===) x y := bool2prop (x == y)
end-instance
, Eqtype-class `Prelude.Eq.Eq`
arguments: ('a :: *)
super-class constraints:
- Prelude.Eq.EqP 'a
has default derive templates
generated code:
instance Eq Natural where
define rec (==) Zero Zero := True
| (==) (Suc x1) (Suc y1) := (x1 == y1)
| (==) _ _ := False
end-instance
, Ordtype-class `Prelude.Ord.Ord`
arguments: ('a :: *)
super-class constraints:
- Prelude.Eq.Eq 'a
has default derive templates
generated code:
instance Ord Natural where
define rec compare Zero Zero := EQ
| compare Zero _ := LT
| compare _ Zero := GT
| compare (Suc x1) (Suc y1) := compare x1 y1
end-instance
)
class NumPlus 'atype-variable `'a`
kind `*` where
declare (+)constant `Prelude.Num.(+)`
constant of type-class `NumPlus`
type `'a -> 'a -> 'a`
executable :: 'atype-variable `'a`
kind `*` -> 'atype-variable `'a`
kind `*` -> 'atype-variable `'a`
kind `*`
end-class
class NumMinus 'atype-variable `'a`
kind `*` where
declare (-)constant `Prelude.Num.(-)`
constant of type-class `NumMinus`
type `'a -> 'a -> 'a`
executable :: 'atype-variable `'a`
kind `*` -> 'atype-variable `'a`
kind `*` -> 'atype-variable `'a`
kind `*`
end-class
class NumMult 'atype-variable `'a`
kind `*` where
declare (*)constant `Prelude.Num.(*)`
constant of type-class `NumMult`
type `'a -> 'a -> 'a`
executable :: 'atype-variable `'a`
kind `*` -> 'atype-variable `'a`
kind `*` -> 'atype-variable `'a`
kind `*`
end-class
class NumDiv 'atype-variable `'a`
kind `*` where
declare (/)constant `Prelude.Num.(/)`
constant of type-class `NumDiv`
type `'a -> 'a -> 'a`
executable :: 'atype-variable `'a`
kind `*` -> 'atype-variable `'a`
kind `*` -> 'atype-variable `'a`
kind `*`
end-class
class NumDivMod 'atype-variable `'a`
kind `*` where
declare divmodconstant `Prelude.Num.divmod`
constant of type-class `NumDivMod`
type `'a -> 'a -> ('a, 'a)`
executable :: 'atype-variable `'a`
kind `*` -> 'atype-variable `'a`
kind `*` -> ('atype-variable `'a`
kind `*`, 'atype-variable `'a`
kind `*`)
declare divconstant `Prelude.Num.div`
constant of type-class `NumDivMod`
type `'a -> 'a -> 'a`
executable :: 'atype-variable `'a`
kind `*` -> 'atype-variable `'a`
kind `*` -> 'atype-variable `'a`
kind `*`
declare modconstant `Prelude.Num.mod`
constant of type-class `NumDivMod`
type `'a -> 'a -> 'a`
executable :: 'atype-variable `'a`
kind `*` -> 'atype-variable `'a`
kind `*` -> 'atype-variable `'a`
kind `*`
define divmodconstant `Prelude.Num.divmod`
default instance of type-class constant
type `('a -> 'a -> 'a) -> ('a -> 'a -> 'a) -> 'a -> 'a -> ('a, 'a)`
executable (xvariable `x`
type `'a` :: 'atype-variable `'a`
kind `*`) yvariable `y`
type `'a` := (xvariable `x`
type `'a` `div`constant `Prelude.Num.div`
constant of type-class `NumDivMod`
type `'a -> 'a -> 'a`
executable
same type-class instance yvariable `y`
type `'a`, xvariable `x`
type `'a` `mod`constant `Prelude.Num.mod`
constant of type-class `NumDivMod`
type `'a -> 'a -> 'a`
executable
same type-class instance yvariable `y`
type `'a`)
define divconstant `Prelude.Num.div`
default instance of type-class constant
type `('a -> 'a -> ('a, 'a)) -> 'a -> 'a -> 'a`
executable xvariable `x`
type `'a` yvariable `y`
type `'a` := fstconstant `Prelude.Tuple.fst`
constant
type `('a, 'b) -> 'a`
type in context `('a, 'a) -> 'a`
executable (divmodconstant `Prelude.Num.divmod`
constant of type-class `NumDivMod`
type `'a -> 'a -> ('a, 'a)`
executable
same type-class instance xvariable `x`
type `'a` yvariable `y`
type `'a`)
define modconstant `Prelude.Num.mod`
default instance of type-class constant
type `('a -> 'a -> ('a, 'a)) -> 'a -> 'a -> 'a`
executable xvariable `x`
type `'a` yvariable `y`
type `'a` := sndconstant `Prelude.Tuple.snd`
constant
type `('a, 'b) -> 'b`
type in context `('a, 'a) -> 'a`
executable (divmodconstant `Prelude.Num.divmod`
constant of type-class `NumDivMod`
type `'a -> 'a -> ('a, 'a)`
executable
same type-class instance xvariable `x`
type `'a` yvariable `y`
type `'a`)
end-class
instance LiteralNumtype-class `Prelude.Literal.LiteralNum`
arguments: ('a :: *)
super-class constraints:
- Prelude.Eq.Eq 'a
statically-resolved Naturaldatatype `Prelude.Num.Natural`
kind `*`
executable where
define mkLiteralNumconstant `Prelude.Literal.mkLiteralNum`
constant of type-class instance `LiteralNum Natural`
type `(Prelude.Literal.BuiltInNumRep, BuiltInNum) -> Natural`
executable _ := ???type `Natural`
end-instance
instance NumPlustype-class `Prelude.Num.NumPlus`
arguments: ('a :: *) Naturaldatatype `Prelude.Num.Natural`
kind `*`
executable where
define rec (+)constant `Prelude.Num.(+)`
constant of type-class instance `NumPlus Natural`
type `Natural -> Natural -> Natural`
executable nvariable `n`
type `Natural` Zeroconstant `Prelude.Num.Zero`
constructor of datatype `Natural`
type `Natural`
executable := nvariable `n`
type `Natural`
| (+)constant `Prelude.Num.(+)`
constant of type-class instance `NumPlus Natural`
type `Natural -> Natural -> Natural`
executable nvariable `n`
type `Natural` (Succonstant `Prelude.Num.Suc`
constructor of datatype `Natural`
type `Natural -> Natural`
executable mvariable `m`
type `Natural`) := (+)constant `Prelude.Num.(+)` (recursive usage)
constant of type-class `NumPlus`
type `'a -> 'a -> 'a`
type in context `Natural -> Natural -> Natural`
executable
same type-class instance (Succonstant `Prelude.Num.Suc`
constructor of datatype `Natural`
type `Natural -> Natural`
executable nvariable `n`
type `Natural`) mvariable `m`
type `Natural`
end-instance
instance NumMinustype-class `Prelude.Num.NumMinus`
arguments: ('a :: *) Naturaldatatype `Prelude.Num.Natural`
kind `*`
executable where
define rec (-)constant `Prelude.Num.(-)`
constant of type-class instance `NumMinus Natural`
type `Natural -> Natural -> Natural`
executable nvariable `n`
type `Natural` Zeroconstant `Prelude.Num.Zero`
constructor of datatype `Natural`
type `Natural`
executable := nvariable `n`
type `Natural`
| (-)constant `Prelude.Num.(-)`
constant of type-class instance `NumMinus Natural`
type `Natural -> Natural -> Natural`
executable Zeroconstant `Prelude.Num.Zero`
constructor of datatype `Natural`
type `Natural`
executable _ := Zeroconstant `Prelude.Num.Zero`
constructor of datatype `Natural`
type `Natural`
executable
| (-)constant `Prelude.Num.(-)`
constant of type-class instance `NumMinus Natural`
type `Natural -> Natural -> Natural`
executable (Succonstant `Prelude.Num.Suc`
constructor of datatype `Natural`
type `Natural -> Natural`
executable nvariable `n`
type `Natural`) (Succonstant `Prelude.Num.Suc`
constructor of datatype `Natural`
type `Natural -> Natural`
executable mvariable `m`
type `Natural`) := (-)constant `Prelude.Num.(-)` (recursive usage)
constant of type-class `NumMinus`
type `'a -> 'a -> 'a`
type in context `Natural -> Natural -> Natural`
executable
same type-class instance nvariable `n`
type `Natural` mvariable `m`
type `Natural`
end-instance
instance NumMulttype-class `Prelude.Num.NumMult`
arguments: ('a :: *) Naturaldatatype `Prelude.Num.Natural`
kind `*`
executable where
define rec (*)constant `Prelude.Num.(*)`
constant of type-class instance `NumMult Natural`
type `Natural -> Natural -> Natural`
executable _ Zeroconstant `Prelude.Num.Zero`
constructor of datatype `Natural`
type `Natural`
executable := Zeroconstant `Prelude.Num.Zero`
constructor of datatype `Natural`
type `Natural`
executable
| (*)constant `Prelude.Num.(*)`
constant of type-class instance `NumMult Natural`
type `Natural -> Natural -> Natural`
executable nvariable `n`
type `Natural` (Succonstant `Prelude.Num.Suc`
constructor of datatype `Natural`
type `Natural -> Natural`
executable mvariable `m`
type `Natural`) := (nvariable `n`
type `Natural` +constant `Prelude.Num.(+)`
constant of type-class `NumPlus`
type `'a -> 'a -> 'a`
type in context `Natural -> Natural -> Natural`
executable
statically resolved type-class instance (nvariable `n`
type `Natural` *constant `Prelude.Num.(*)` (recursive usage)
constant of type-class `NumMult`
type `'a -> 'a -> 'a`
type in context `Natural -> Natural -> Natural`
executable
same type-class instance mvariable `m`
type `Natural`))
end-instance
instance NumDivModtype-class `Prelude.Num.NumDivMod`
arguments: ('a :: *) Naturaldatatype `Prelude.Num.Natural`
kind `*`
executable where
define rec divmodconstant `Prelude.Num.divmod`
constant of type-class instance `NumDivMod Natural`
type `Natural -> Natural -> (Natural, Natural)`
executable _ Zeroconstant `Prelude.Num.Zero`
constructor of datatype `Natural`
type `Natural`
executable := ???type `(Natural, Natural)`
| divmodconstant `Prelude.Num.divmod`
constant of type-class instance `NumDivMod Natural`
type `Natural -> Natural -> (Natural, Natural)`
executable xvariable `x`
type `Natural` yvariable `y`
type `Natural` :=
if xvariable `x`
type `Natural` <constant `Prelude.Ord.(<)`
constant of type-class `Ord`
type `'a -> 'a -> Bool`
type in context `Natural -> Natural -> Bool`
executable
statically resolved type-class instance yvariable `y`
type `Natural` then
(0natural number literal
type `Natural`
decimal value: 0
hexadecimal value: 0x0
octal value: 0o0
binary value: 0b0, xvariable `x`
type `Natural`)
else
let
val (dvariable `d`
type `Natural`, mvariable `m`
type `Natural`) = divmodconstant `Prelude.Num.divmod` (recursive usage)
constant of type-class `NumDivMod`
type `'a -> 'a -> ('a, 'a)`
type in context `Natural -> Natural -> (Natural, Natural)`
executable
same type-class instance (xvariable `x`
type `Natural` -constant `Prelude.Num.(-)`
constant of type-class `NumMinus`
type `'a -> 'a -> 'a`
type in context `Natural -> Natural -> Natural`
executable
statically resolved type-class instance yvariable `y`
type `Natural`) yvariable `y`
type `Natural`
in (dvariable `d`
type `Natural`+constant `Prelude.Num.(+)`
constant of type-class `NumPlus`
type `'a -> 'a -> 'a`
type in context `Natural -> Natural -> Natural`
executable
statically resolved type-class instance1natural number literal
type `Natural`
decimal value: 1
hexadecimal value: 0x1
octal value: 0o1
binary value: 0b1, mvariable `m`
type `Natural`) end
end-instance
instance NumDivtype-class `Prelude.Num.NumDiv`
arguments: ('a :: *) Naturaldatatype `Prelude.Num.Natural`
kind `*`
executable where
define (/)constant `Prelude.Num.(/)`
constant of type-class instance `NumDiv Natural`
type `Natural -> Natural -> Natural`
executable := divconstant `Prelude.Num.div`
constant of type-class `NumDivMod`
type `'a -> 'a -> 'a`
type in context `Natural -> Natural -> Natural`
executable
statically resolved type-class instance
{-# inline (/)constant `Prelude.Num.(/)`
constant of type-class instance `NumDiv Natural`
type `Natural -> Natural -> Natural`
executable #-}
end-instance
instance LiteralNumtype-class `Prelude.Literal.LiteralNum`
arguments: ('a :: *)
super-class constraints:
- Prelude.Eq.Eq 'a
statically-resolved Booldatatype `Prelude.Bool.Bool`
kind `*`
executable where
define mkLiteralNumconstant `Prelude.Literal.mkLiteralNum`
constant of type-class instance `LiteralNum Bool`
type `(Prelude.Literal.BuiltInNumRep, BuiltInNum) -> Bool`
executable (_, 0natural number literal
type `BuiltInNum`
decimal value: 0
hexadecimal value: 0x0
octal value: 0o0
binary value: 0b0) := Falseconstant `Prelude.Bool.False`
constructor of datatype `Bool`
type `Bool`
executable
| mkLiteralNumconstant `Prelude.Literal.mkLiteralNum`
constant of type-class instance `LiteralNum Bool`
type `(Prelude.Literal.BuiltInNumRep, BuiltInNum) -> Bool`
executable (_, _) := Trueconstant `Prelude.Bool.True`
constructor of datatype `Bool`
type `Bool`
executable
{-# set-num-literal-boundaries 0 1 #-}
end-instance
end-moduleend of module Prelude.Num
|