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
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
|
module Prelude.Tuple (
fstconstant `Prelude.Tuple.fst`
constant
type `('a, 'b) -> 'a`
executable,
sndconstant `Prelude.Tuple.snd`
constant
type `('a, 'b) -> 'b`
executable,
uncurryconstant `Prelude.Tuple.uncurry`
constant
type `('a -> 'b -> 'c) -> ('a, 'b) -> 'c`
executable,
curryconstant `Prelude.Tuple.curry`
constant
type `(('a, 'b) -> 'c) -> 'a -> 'b -> 'c`
executable,
Tuple2abbreviation-type `Prelude.Tuple.Tuple2`
kind `* -> *`
type `Tuple2 'a` abbreviates type `('a, 'a)`
executable(..)definition of abbreviation-type,
Tuple3abbreviation-type `Prelude.Tuple.Tuple3`
kind `* -> *`
type `Tuple3 'a` abbreviates type `('a, 'a, 'a)`
executable(..)definition of abbreviation-type,
Tuple4abbreviation-type `Prelude.Tuple.Tuple4`
kind `* -> *`
type `Tuple4 'a` abbreviates type `('a, 'a, 'a, 'a)`
executable(..)definition of abbreviation-type,
Tuple5abbreviation-type `Prelude.Tuple.Tuple5`
kind `* -> *`
type `Tuple5 'a` abbreviates type `('a, 'a, 'a, 'a, 'a)`
executable(..)definition of abbreviation-type,
Tuple6abbreviation-type `Prelude.Tuple.Tuple6`
kind `* -> *`
type `Tuple6 'a` abbreviates type `('a, 'a, 'a, 'a, 'a, 'a)`
executable(..)definition of abbreviation-type,
Tuple7abbreviation-type `Prelude.Tuple.Tuple7`
kind `* -> *`
type `Tuple7 'a` abbreviates type `('a, 'a, 'a, 'a, 'a, 'a, 'a)`
executable(..)definition of abbreviation-type,
Tuple8abbreviation-type `Prelude.Tuple.Tuple8`
kind `* -> *`
type `Tuple8 'a` abbreviates type `('a, 'a, 'a, 'a, 'a, 'a, 'a, 'a)`
executable(..)definition of abbreviation-type,
Tuple9abbreviation-type `Prelude.Tuple.Tuple9`
kind `* -> *`
type `Tuple9 'a` abbreviates type `('a, 'a, 'a, 'a, 'a, 'a, 'a, 'a, 'a)`
executable(..)definition of abbreviation-type
) where
{-# NoImplicitPrelude #-}
import Prelude.Bool
import Prelude.Eq
import Prelude.Ord
import Prelude.Function
import Prelude.Template
import Prelude.Functor
declare fstconstant `Prelude.Tuple.fst`
constant
type `('a, 'b) -> 'a`
executable :: ('atype-variable `'a`
kind `*`, 'btype-variable `'b`
kind `*`) -> 'atype-variable `'a`
kind `*`
define fstconstant `Prelude.Tuple.fst`
constant
type `('a, 'b) -> 'a`
executable (xvariable `x`
type `'a`, _) := xvariable `x`
type `'a`
declare sndconstant `Prelude.Tuple.snd`
constant
type `('a, 'b) -> 'b`
executable :: ('atype-variable `'a`
kind `*`, 'btype-variable `'b`
kind `*`) -> 'btype-variable `'b`
kind `*`
define sndconstant `Prelude.Tuple.snd`
constant
type `('a, 'b) -> 'b`
executable (_, yvariable `y`
type `'b`) := yvariable `y`
type `'b`
declare curryconstant `Prelude.Tuple.curry`
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 curryconstant `Prelude.Tuple.curry`
constant
type `(('a, 'b) -> 'c) -> 'a -> 'b -> 'c`
executable fvariable `f`
type `('a, 'b) -> 'c` xvariable `x`
type `'a` yvariable `y`
type `'b` := fvariable `f`
type `('a, 'b) -> 'c` (xvariable `x`
type `'a`, yvariable `y`
type `'b`)
declare uncurryconstant `Prelude.Tuple.uncurry`
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 uncurryconstant `Prelude.Tuple.uncurry`
constant
type `('a -> 'b -> 'c) -> ('a, 'b) -> 'c`
executable fvariable `f`
type `'a -> 'b -> 'c` (xvariable `x`
type `'a`, yvariable `y`
type `'b`) := fvariable `f`
type `'a -> 'b -> 'c` xvariable `x`
type `'a` yvariable `y`
type `'b`
template BuildTupleAbbrev (n :: Nat) :=
'''type Tuple{{= ntemplate-variable `n`
type Nat =}} \'a := {{=!BuildTupletemplate `Prelude.Template.BuildTuple`
argument-type: [String]
return-type: String
does not compute text(replicate(ntemplate-variable `n`
type Nat, "'a"))=}}'''
template BuildFunctorTupleInstance (n :: Nat) := '''
{{ name-scope {
var xstemplate-variable `xs`
type [String] := generateNames("x", ntemplate-variable `n`
type Nat)
}
var f_xstemplate-variable `f_xs`
type [String] := [] :: [String];
foreach var xtemplate-variable `x`
type String in xstemplate-variable `xs`
type [String] {
f_xstemplate-variable `f_xs`
type [String] := insertAtEnd("f " ++ xtemplate-variable `x`
type String, f_xstemplate-variable `f_xs`
type [String]);
}
}}
{{! BuildInstanceHeadertemplate `Prelude.Template.BuildInstanceHeader`
argument-types: ([String], String)
return-type: -([] :: [String], "Functor Tuple" ++ ntemplate-variable `n`
type Nat) !}}
define fmap f {{= !BuildTupletemplate `Prelude.Template.BuildTuple`
argument-type: [String]
return-type: String
does not compute text(xstemplate-variable `xs`
type [String]) =}} := {{= !BuildTupletemplate `Prelude.Template.BuildTuple`
argument-type: [String]
return-type: String
does not compute text(f_xstemplate-variable `f_xs`
type [String]) =}}
end-instance
'''
generate-codegenerated code:
type Tuple2 'a := ('a, 'a)
instance Functor Tuple2 where
define fmap f (x1, x2) := (f x1, f x2)
end-instance
type Tuple3 'a := ('a, 'a, 'a)
instance Functor Tuple3 where
define fmap f (x1, x2, x3) := (f x1, f x2, f x3)
end-instance
type Tuple4 'a := ('a, 'a, 'a, 'a)
instance Functor Tuple4 where
define fmap f (x1, x2, x3, x4) := (f x1, f x2, f x3, f x4)
end-instance
type Tuple5 'a := ('a, 'a, 'a, 'a, 'a)
instance Functor Tuple5 where
define fmap f (x1, x2, x3, x4, x5) := (f x1, f x2, f x3, f x4, f x5)
end-instance
type Tuple6 'a := ('a, 'a, 'a, 'a, 'a, 'a)
instance Functor Tuple6 where
define fmap f (x1, x2, x3, x4, x5, x6) := (f x1, f x2, f x3, f x4, f x5, f x6)
end-instance
type Tuple7 'a := ('a, 'a, 'a, 'a, 'a, 'a, 'a)
instance Functor Tuple7 where
define fmap f (x1, x2, x3, x4, x5, x6, x7) := (f x1, f x2, f x3, f x4, f x5, f x6, f x7)
end-instance
type Tuple8 'a := ('a, 'a, 'a, 'a, 'a, 'a, 'a, 'a)
instance Functor Tuple8 where
define fmap f (x1, x2, x3, x4, x5, x6, x7, x8) := (f x1, f x2, f x3, f x4, f x5, f x6, f x7, f x8)
end-instance
type Tuple9 'a := ('a, 'a, 'a, 'a, 'a, 'a, 'a, 'a, 'a)
instance Functor Tuple9 where
define fmap f (x1, x2, x3, x4, x5, x6, x7, x8, x9) := (f x1, f x2, f x3, f x4, f x5, f x6, f x7, f x8, f x9)
end-instance
'''
{{% for var itemplate-variable `i`
type Nat := 2 to 9 %}}
{{! BuildTupleAbbrevtemplate `Prelude.Tuple.BuildTupleAbbrev`
argument-type: Nat
return-type: -(itemplate-variable `i`
type Nat) !}}
{{! BuildFunctorTupleInstancetemplate `Prelude.Tuple.BuildFunctorTupleInstance`
argument-type: Nat
return-type: -(itemplate-variable `i`
type Nat) !}}
{{% end-for %}}
'''
template BuildTupleInstanceVars (className :: String, n :: Nat) :: ([String], [String], [String], String) :=
{{ name-scope {
var tyVarstemplate-variable `tyVars`
type [String] := !GetTypeVarstemplate `Prelude.Template.GetTypeVars`
argument-type: Nat
return-type: [String]
does not compute text(ntemplate-variable `n`
type Nat);
var xstemplate-variable `xs`
type [String] := generateNames("x", ntemplate-variable `n`
type Nat);
var ystemplate-variable `ys`
type [String] := generateNames("y", ntemplate-variable `n`
type Nat);
var supertemplate-variable `super`
type [String] := [] :: [String];
foreach var tyVtemplate-variable `tyV`
type String in tyVarstemplate-variable `tyVars`
type [String] {
supertemplate-variable `super`
type [String] := insertAtEnd(classNametemplate-variable `className`
type String ++ " " ++ tyVtemplate-variable `tyV`
type String, supertemplate-variable `super`
type [String]);
}
var insttemplate-variable `inst`
type String := classNametemplate-variable `className`
type String ++ " " ++ !BuildTupletemplate `Prelude.Template.BuildTuple`
argument-type: [String]
return-type: String
does not compute text(tyVarstemplate-variable `tyVars`
type [String]);
}
return (xstemplate-variable `xs`
type [String], ystemplate-variable `ys`
type [String], supertemplate-variable `super`
type [String], insttemplate-variable `inst`
type String);
}}
template BuildEqPTupleInstance (n :: Nat) := '''
{{ var (xstemplate-variable `xs`
type [String], ystemplate-variable `ys`
type [String], supertemplate-variable `super`
type [String], insttemplate-variable `inst`
type String) := !BuildTupleInstanceVarstemplate `Prelude.Tuple.BuildTupleInstanceVars`
argument-types: (String, Nat)
return-types: ([String], [String], [String], String)
does not compute text("EqP", ntemplate-variable `n`
type Nat);
var compstemplate-variable `comps`
type [String] := [] :: [String];
foreach var xytemplate-variable `xy`
type (String, String) in zip(xstemplate-variable `xs`
type [String], ystemplate-variable `ys`
type [String]) {
var eltemplate-variable `el`
type String := "(" ++ #1(xytemplate-variable `xy`
type (String, String)) ++ " === " ++ #2(xytemplate-variable `xy`
type (String, String)) ++ ")";
compstemplate-variable `comps`
type [String] := insertAtEnd(eltemplate-variable `el`
type String, compstemplate-variable `comps`
type [String]);
}
}}
{{! BuildInstanceHeadertemplate `Prelude.Template.BuildInstanceHeader`
argument-types: ([String], String)
return-type: -(supertemplate-variable `super`
type [String], insttemplate-variable `inst`
type String) !}}
define non-exec (===) {{= !BuildTupletemplate `Prelude.Template.BuildTuple`
argument-type: [String]
return-type: String
does not compute text(xstemplate-variable `xs`
type [String]) =}} {{= !BuildTupletemplate `Prelude.Template.BuildTuple`
argument-type: [String]
return-type: String
does not compute text(ystemplate-variable `ys`
type [String]) =}} :=
{{= !Intercalatetemplate `Prelude.Template.Intercalate`
argument-types: (String, [String])
return-type: String
does not compute text(" /\\\n", compstemplate-variable `comps`
type [String]) =}}
end-instance
'''
template BuildEqTupleInstance (n :: Nat) := '''
{{ var (xstemplate-variable `xs`
type [String], ystemplate-variable `ys`
type [String], supertemplate-variable `super`
type [String], insttemplate-variable `inst`
type String) := !BuildTupleInstanceVarstemplate `Prelude.Tuple.BuildTupleInstanceVars`
argument-types: (String, Nat)
return-types: ([String], [String], [String], String)
does not compute text("Eq", ntemplate-variable `n`
type Nat);
var compstemplate-variable `comps`
type [String] := [] :: [String];
foreach var xytemplate-variable `xy`
type (String, String) in zip(xstemplate-variable `xs`
type [String], ystemplate-variable `ys`
type [String]) {
var eltemplate-variable `el`
type String := "(" ++ #1(xytemplate-variable `xy`
type (String, String)) ++ " == " ++ #2(xytemplate-variable `xy`
type (String, String)) ++ ")";
compstemplate-variable `comps`
type [String] := insertAtEnd(eltemplate-variable `el`
type String, compstemplate-variable `comps`
type [String]);
}
}}
{{! BuildInstanceHeadertemplate `Prelude.Template.BuildInstanceHeader`
argument-types: ([String], String)
return-type: -(supertemplate-variable `super`
type [String], insttemplate-variable `inst`
type String) !}}
define (==) {{= !BuildTupletemplate `Prelude.Template.BuildTuple`
argument-type: [String]
return-type: String
does not compute text(xstemplate-variable `xs`
type [String]) =}} {{= !BuildTupletemplate `Prelude.Template.BuildTuple`
argument-type: [String]
return-type: String
does not compute text(ystemplate-variable `ys`
type [String]) =}} :=
{{= !Intercalatetemplate `Prelude.Template.Intercalate`
argument-types: (String, [String])
return-type: String
does not compute text(" &&\n", compstemplate-variable `comps`
type [String]) =}}
end-instance
'''
template BuildOrdTupleInstance (n :: Nat) := '''
{{ var (xstemplate-variable `xs`
type [String], ystemplate-variable `ys`
type [String], supertemplate-variable `super`
type [String], insttemplate-variable `inst`
type String) := !BuildTupleInstanceVarstemplate `Prelude.Tuple.BuildTupleInstanceVars`
argument-types: (String, Nat)
return-types: ([String], [String], [String], String)
does not compute text("Ord", ntemplate-variable `n`
type Nat);
var compstemplate-variable `comps`
type [String] := [] :: [String];
for var itemplate-variable `i`
type Nat := 0 to (ntemplate-variable `n`
type Nat - 2) {
var eltemplate-variable `el`
type String := "lexCompare " ++ xstemplate-variable `xs`
type [String][itemplate-variable `i`
type Nat] ++ " " ++ ystemplate-variable `ys`
type [String][itemplate-variable `i`
type Nat];
compstemplate-variable `comps`
type [String] := insertAtEnd(eltemplate-variable `el`
type String, compstemplate-variable `comps`
type [String]);
}
}}
{{! BuildInstanceHeadertemplate `Prelude.Template.BuildInstanceHeader`
argument-types: ([String], String)
return-type: -(supertemplate-variable `super`
type [String], insttemplate-variable `inst`
type String) !}}
define compare {{= !BuildTupletemplate `Prelude.Template.BuildTuple`
argument-type: [String]
return-type: String
does not compute text(xstemplate-variable `xs`
type [String]) =}} {{= !BuildTupletemplate `Prelude.Template.BuildTuple`
argument-type: [String]
return-type: String
does not compute text(ystemplate-variable `ys`
type [String]) =}} :=
{{= !Intercalatetemplate `Prelude.Template.Intercalate`
argument-types: (String, [String])
return-type: String
does not compute text(" $\n", compstemplate-variable `comps`
type [String]) =}} $
compare {{=xstemplate-variable `xs`
type [String][ntemplate-variable `n`
type Nat-1]=}} {{=ystemplate-variable `ys`
type [String][ntemplate-variable `n`
type Nat-1]=}}
end-instance
'''
generate-codegenerated code:
instance (EqP 'a, EqP 'b) => EqP ('a, 'b) where
define non-exec (===) (x1, x2) (y1, y2) :=
(x1 === y1) /\
(x2 === y2)
end-instance
instance (Eq 'a, Eq 'b) => Eq ('a, 'b) where
define (==) (x1, x2) (y1, y2) :=
(x1 == y1) &&
(x2 == y2)
end-instance
instance (Ord 'a, Ord 'b) => Ord ('a, 'b) where
define compare (x1, x2) (y1, y2) :=
lexCompare x1 y1 $
compare x2 y2
end-instance
instance (EqP 'a, EqP 'b, EqP 'c) => EqP ('a, 'b, 'c) where
define non-exec (===) (x1, x2, x3) (y1, y2, y3) :=
(x1 === y1) /\
(x2 === y2) /\
(x3 === y3)
end-instance
instance (Eq 'a, Eq 'b, Eq 'c) => Eq ('a, 'b, 'c) where
define (==) (x1, x2, x3) (y1, y2, y3) :=
(x1 == y1) &&
(x2 == y2) &&
(x3 == y3)
end-instance
instance (Ord 'a, Ord 'b, Ord 'c) => Ord ('a, 'b, 'c) where
define compare (x1, x2, x3) (y1, y2, y3) :=
lexCompare x1 y1 $
lexCompare x2 y2 $
compare x3 y3
end-instance
instance (EqP 'a, EqP 'b, EqP 'c, EqP 'd) => EqP ('a, 'b, 'c, 'd) where
define non-exec (===) (x1, x2, x3, x4) (y1, y2, y3, y4) :=
(x1 === y1) /\
(x2 === y2) /\
(x3 === y3) /\
(x4 === y4)
end-instance
instance (Eq 'a, Eq 'b, Eq 'c, Eq 'd) => Eq ('a, 'b, 'c, 'd) where
define (==) (x1, x2, x3, x4) (y1, y2, y3, y4) :=
(x1 == y1) &&
(x2 == y2) &&
(x3 == y3) &&
(x4 == y4)
end-instance
instance (Ord 'a, Ord 'b, Ord 'c, Ord 'd) => Ord ('a, 'b, 'c, 'd) where
define compare (x1, x2, x3, x4) (y1, y2, y3, y4) :=
lexCompare x1 y1 $
lexCompare x2 y2 $
lexCompare x3 y3 $
compare x4 y4
end-instance
instance (EqP 'a, EqP 'b, EqP 'c, EqP 'd, EqP 'e) => EqP ('a, 'b, 'c, 'd, 'e) where
define non-exec (===) (x1, x2, x3, x4, x5) (y1, y2, y3, y4, y5) :=
(x1 === y1) /\
(x2 === y2) /\
(x3 === y3) /\
(x4 === y4) /\
(x5 === y5)
end-instance
instance (Eq 'a, Eq 'b, Eq 'c, Eq 'd, Eq 'e) => Eq ('a, 'b, 'c, 'd, 'e) where
define (==) (x1, x2, x3, x4, x5) (y1, y2, y3, y4, y5) :=
(x1 == y1) &&
(x2 == y2) &&
(x3 == y3) &&
(x4 == y4) &&
(x5 == y5)
end-instance
instance (Ord 'a, Ord 'b, Ord 'c, Ord 'd, Ord 'e) => Ord ('a, 'b, 'c, 'd, 'e) where
define compare (x1, x2, x3, x4, x5) (y1, y2, y3, y4, y5) :=
lexCompare x1 y1 $
lexCompare x2 y2 $
lexCompare x3 y3 $
lexCompare x4 y4 $
compare x5 y5
end-instance
instance (EqP 'a, EqP 'b, EqP 'c, EqP 'd, EqP 'e, EqP 'f) => EqP ('a, 'b, 'c, 'd, 'e, 'f) where
define non-exec (===) (x1, x2, x3, x4, x5, x6) (y1, y2, y3, y4, y5, y6) :=
(x1 === y1) /\
(x2 === y2) /\
(x3 === y3) /\
(x4 === y4) /\
(x5 === y5) /\
(x6 === y6)
end-instance
instance (Eq 'a, Eq 'b, Eq 'c, Eq 'd, Eq 'e, Eq 'f) => Eq ('a, 'b, 'c, 'd, 'e, 'f) where
define (==) (x1, x2, x3, x4, x5, x6) (y1, y2, y3, y4, y5, y6) :=
(x1 == y1) &&
(x2 == y2) &&
(x3 == y3) &&
(x4 == y4) &&
(x5 == y5) &&
(x6 == y6)
end-instance
instance (Ord 'a, Ord 'b, Ord 'c, Ord 'd, Ord 'e, Ord 'f) => Ord ('a, 'b, 'c, 'd, 'e, 'f) where
define compare (x1, x2, x3, x4, x5, x6) (y1, y2, y3, y4, y5, y6) :=
lexCompare x1 y1 $
lexCompare x2 y2 $
lexCompare x3 y3 $
lexCompare x4 y4 $
lexCompare x5 y5 $
compare x6 y6
end-instance
instance (EqP 'a, EqP 'b, EqP 'c, EqP 'd, EqP 'e, EqP 'f, EqP 'g) => EqP ('a, 'b, 'c, 'd, 'e, 'f, 'g) where
define non-exec (===) (x1, x2, x3, x4, x5, x6, x7) (y1, y2, y3, y4, y5, y6, y7) :=
(x1 === y1) /\
(x2 === y2) /\
(x3 === y3) /\
(x4 === y4) /\
(x5 === y5) /\
(x6 === y6) /\
(x7 === y7)
end-instance
instance (Eq 'a, Eq 'b, Eq 'c, Eq 'd, Eq 'e, Eq 'f, Eq 'g) => Eq ('a, 'b, 'c, 'd, 'e, 'f, 'g) where
define (==) (x1, x2, x3, x4, x5, x6, x7) (y1, y2, y3, y4, y5, y6, y7) :=
(x1 == y1) &&
(x2 == y2) &&
(x3 == y3) &&
(x4 == y4) &&
(x5 == y5) &&
(x6 == y6) &&
(x7 == y7)
end-instance
instance (Ord 'a, Ord 'b, Ord 'c, Ord 'd, Ord 'e, Ord 'f, Ord 'g) => Ord ('a, 'b, 'c, 'd, 'e, 'f, 'g) where
define compare (x1, x2, x3, x4, x5, x6, x7) (y1, y2, y3, y4, y5, y6, y7) :=
lexCompare x1 y1 $
lexCompare x2 y2 $
lexCompare x3 y3 $
lexCompare x4 y4 $
lexCompare x5 y5 $
lexCompare x6 y6 $
compare x7 y7
end-instance
instance (EqP 'a, EqP 'b, EqP 'c, EqP 'd, EqP 'e, EqP 'f, EqP 'g, EqP 'h) => EqP ('a, 'b, 'c, 'd, 'e, 'f, 'g, 'h) where
define non-exec (===) (x1, x2, x3, x4, x5, x6, x7, x8) (y1, y2, y3, y4, y5, y6, y7, y8) :=
(x1 === y1) /\
(x2 === y2) /\
(x3 === y3) /\
(x4 === y4) /\
(x5 === y5) /\
(x6 === y6) /\
(x7 === y7) /\
(x8 === y8)
end-instance
instance (Eq 'a, Eq 'b, Eq 'c, Eq 'd, Eq 'e, Eq 'f, Eq 'g, Eq 'h) => Eq ('a, 'b, 'c, 'd, 'e, 'f, 'g, 'h) where
define (==) (x1, x2, x3, x4, x5, x6, x7, x8) (y1, y2, y3, y4, y5, y6, y7, y8) :=
(x1 == y1) &&
(x2 == y2) &&
(x3 == y3) &&
(x4 == y4) &&
(x5 == y5) &&
(x6 == y6) &&
(x7 == y7) &&
(x8 == y8)
end-instance
instance (Ord 'a, Ord 'b, Ord 'c, Ord 'd, Ord 'e, Ord 'f, Ord 'g, Ord 'h) => Ord ('a, 'b, 'c, 'd, 'e, 'f, 'g, 'h) where
define compare (x1, x2, x3, x4, x5, x6, x7, x8) (y1, y2, y3, y4, y5, y6, y7, y8) :=
lexCompare x1 y1 $
lexCompare x2 y2 $
lexCompare x3 y3 $
lexCompare x4 y4 $
lexCompare x5 y5 $
lexCompare x6 y6 $
lexCompare x7 y7 $
compare x8 y8
end-instance
instance (EqP 'a, EqP 'b, EqP 'c, EqP 'd, EqP 'e, EqP 'f, EqP 'g, EqP 'h, EqP 'i) => EqP ('a, 'b, 'c, 'd, 'e, 'f, 'g, 'h, 'i) where
define non-exec (===) (x1, x2, x3, x4, x5, x6, x7, x8, x9) (y1, y2, y3, y4, y5, y6, y7, y8, y9) :=
(x1 === y1) /\
(x2 === y2) /\
(x3 === y3) /\
(x4 === y4) /\
(x5 === y5) /\
(x6 === y6) /\
(x7 === y7) /\
(x8 === y8) /\
(x9 === y9)
end-instance
instance (Eq 'a, Eq 'b, Eq 'c, Eq 'd, Eq 'e, Eq 'f, Eq 'g, Eq 'h, Eq 'i) => Eq ('a, 'b, 'c, 'd, 'e, 'f, 'g, 'h, 'i) where
define (==) (x1, x2, x3, x4, x5, x6, x7, x8, x9) (y1, y2, y3, y4, y5, y6, y7, y8, y9) :=
(x1 == y1) &&
(x2 == y2) &&
(x3 == y3) &&
(x4 == y4) &&
(x5 == y5) &&
(x6 == y6) &&
(x7 == y7) &&
(x8 == y8) &&
(x9 == y9)
end-instance
instance (Ord 'a, Ord 'b, Ord 'c, Ord 'd, Ord 'e, Ord 'f, Ord 'g, Ord 'h, Ord 'i) => Ord ('a, 'b, 'c, 'd, 'e, 'f, 'g, 'h, 'i) where
define compare (x1, x2, x3, x4, x5, x6, x7, x8, x9) (y1, y2, y3, y4, y5, y6, y7, y8, y9) :=
lexCompare x1 y1 $
lexCompare x2 y2 $
lexCompare x3 y3 $
lexCompare x4 y4 $
lexCompare x5 y5 $
lexCompare x6 y6 $
lexCompare x7 y7 $
lexCompare x8 y8 $
compare x9 y9
end-instance
'''
{{% for var itemplate-variable `i`
type Nat := 2 to 9 %}}
{{! BuildEqPTupleInstancetemplate `Prelude.Tuple.BuildEqPTupleInstance`
argument-type: Nat
return-type: -(itemplate-variable `i`
type Nat) !}}
{{! BuildEqTupleInstancetemplate `Prelude.Tuple.BuildEqTupleInstance`
argument-type: Nat
return-type: -(itemplate-variable `i`
type Nat) !}}
{{! BuildOrdTupleInstancetemplate `Prelude.Tuple.BuildOrdTupleInstance`
argument-type: Nat
return-type: -(itemplate-variable `i`
type Nat) !}}
{{% end-for %}}
'''
end-moduleend of module Prelude.Tuple
|