Prelude/Tuple.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
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