Prelude/Ord.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
module Prelude.Ord (
  type Orderingdatatype `Prelude.Ord.Ordering`
   kind `*`
   executable(..)case-constant `caseOrdering`
constructor `LT`
constructor `EQ`
constructor `GT`
,
  class Ordtype-class `Prelude.Ord.Ord`
   arguments: ('a :: *)
   super-class constraints:
     - Prelude.Eq.Eq 'a
   has default derive templates(..)class-constant `(<)`
class-constant `(<=)`
class-constant `(>)`
class-constant `(>=)`
class-constant `compare`
class-constant `max`
class-constant `min`
,
  comparingconstant `Prelude.Ord.comparing`
   constant
   type `Ord 'a => ('b -> 'a) -> 'b -> 'b -> Ordering`
   executable,
  lexCompareconstant `Prelude.Ord.lexCompare`
   constant
   type `Ord 'a => 'a -> 'a -> Ordering -> Ordering`
   executable
) where

{-# NoImplicitPrelude #-}

import Prelude.Bool
import Prelude.Eq
import Prelude.Template
import Prelude.Default
import Prelude.Unit()

datatype Orderingdatatype `Prelude.Ord.Ordering`
   kind `*`
   executable :=
    LT
  | EQ
  | GT

derive Orderingdatatype `Prelude.Ord.Ordering`
   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 Ordering 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 Ordering where define (==) LT LT := True | (==) EQ EQ := True | (==) GT GT := True | (==) _ _ := False end-instance
)
instance Defaulttype-class `Prelude.Default.Default` arguments: ('a :: *) has default derive templates Orderingdatatype `Prelude.Ord.Ordering` kind `*` executable where define defaultconstant `Prelude.Default.default` constant of type-class instance `Default Ordering` type `Ordering` executable := EQconstant `Prelude.Ord.EQ` constructor of datatype `Ordering` type `Ordering` executable {-# inline defaultconstant `Prelude.Default.default` constant of type-class instance `Default Ordering` type `Ordering` executable #-} end-instance class Eqtype-class `Prelude.Eq.Eq` arguments: ('a :: *) super-class constraints: - Prelude.Eq.EqP 'a has default derive templates 'atype-variable `'a` kind `*` => Ord 'atype-variable `'a` kind `*` where declare compareconstant `Prelude.Ord.compare` constant of type-class `Ord` type `'a -> 'a -> Ordering` executable :: 'atype-variable `'a` kind `*` -> 'atype-variable `'a` kind `*` -> Orderingdatatype `Prelude.Ord.Ordering` kind `*` executable define compareconstant `Prelude.Ord.compare` default instance of type-class constant type `('a -> 'a -> Bool) -> 'a -> 'a -> Ordering` executable xvariable `x` type `'a` yvariable `y` type `'a` := cases (xvariable `x` type `'a` ==constant `Prelude.Eq.(==)` constant of type-class `Eq` type `'a -> 'a -> Bool` executable type-class instance from context yvariable `y` type `'a`) -> EQconstant `Prelude.Ord.EQ` constructor of datatype `Ordering` type `Ordering` executable | (xvariable `x` type `'a` <constant `Prelude.Ord.(<)` constant of type-class `Ord` type `'a -> 'a -> Bool` executable same type-class instance yvariable `y` type `'a`) -> LTconstant `Prelude.Ord.LT` constructor of datatype `Ordering` type `Ordering` executable | otherwise -> GTconstant `Prelude.Ord.GT` constructor of datatype `Ordering` type `Ordering` executable end declare (<)constant `Prelude.Ord.(<)` constant of type-class `Ord` type `'a -> 'a -> Bool` executable :: 'atype-variable `'a` kind `*` -> 'atype-variable `'a` kind `*` -> Booldatatype `Prelude.Bool.Bool` kind `*` executable declare (<=)constant `Prelude.Ord.(<=)` constant of type-class `Ord` type `'a -> 'a -> Bool` executable :: 'atype-variable `'a` kind `*` -> 'atype-variable `'a` kind `*` -> Booldatatype `Prelude.Bool.Bool` kind `*` executable declare (>)constant `Prelude.Ord.(>)` constant of type-class `Ord` type `'a -> 'a -> Bool` executable :: 'atype-variable `'a` kind `*` -> 'atype-variable `'a` kind `*` -> Booldatatype `Prelude.Bool.Bool` kind `*` executable declare (>=)constant `Prelude.Ord.(>=)` constant of type-class `Ord` type `'a -> 'a -> Bool` executable :: 'atype-variable `'a` kind `*` -> 'atype-variable `'a` kind `*` -> Booldatatype `Prelude.Bool.Bool` kind `*` executable declare minconstant `Prelude.Ord.min` constant of type-class `Ord` type `'a -> 'a -> 'a` executable :: 'atype-variable `'a` kind `*` -> 'atype-variable `'a` kind `*` -> 'atype-variable `'a` kind `*` declare maxconstant `Prelude.Ord.max` constant of type-class `Ord` type `'a -> 'a -> 'a` executable :: 'atype-variable `'a` kind `*` -> 'atype-variable `'a` kind `*` -> 'atype-variable `'a` kind `*` define (<=)constant `Prelude.Ord.(<=)` default instance of type-class constant type `('a -> 'a -> Ordering) -> 'a -> 'a -> Bool` executable xvariable `x` type `'a` yvariable `y` type `'a` := (compareconstant `Prelude.Ord.compare` constant of type-class `Ord` type `'a -> 'a -> Ordering` executable same type-class instance xvariable `x` type `'a` yvariable `y` type `'a` /=constant `Prelude.Eq.(/=)` constant of type-class `Eq` type `'a -> 'a -> Bool` type in context `Ordering -> Ordering -> Bool` executable statically resolved type-class instance GTconstant `Prelude.Ord.GT` constructor of datatype `Ordering` type `Ordering` executable) define (<)constant `Prelude.Ord.(<)` default instance of type-class constant type `('a -> 'a -> Ordering) -> 'a -> 'a -> Bool` executable xvariable `x` type `'a` yvariable `y` type `'a` := (compareconstant `Prelude.Ord.compare` constant of type-class `Ord` type `'a -> 'a -> Ordering` executable same type-class instance xvariable `x` type `'a` yvariable `y` type `'a` ==constant `Prelude.Eq.(==)` constant of type-class `Eq` type `'a -> 'a -> Bool` type in context `Ordering -> Ordering -> Bool` executable statically resolved type-class instance LTconstant `Prelude.Ord.LT` constructor of datatype `Ordering` type `Ordering` executable) define (>=)constant `Prelude.Ord.(>=)` default instance of type-class constant type `('a -> 'a -> Ordering) -> 'a -> 'a -> Bool` executable xvariable `x` type `'a` yvariable `y` type `'a` := (compareconstant `Prelude.Ord.compare` constant of type-class `Ord` type `'a -> 'a -> Ordering` executable same type-class instance xvariable `x` type `'a` yvariable `y` type `'a` /=constant `Prelude.Eq.(/=)` constant of type-class `Eq` type `'a -> 'a -> Bool` type in context `Ordering -> Ordering -> Bool` executable statically resolved type-class instance LTconstant `Prelude.Ord.LT` constructor of datatype `Ordering` type `Ordering` executable) define (>)constant `Prelude.Ord.(>)` default instance of type-class constant type `('a -> 'a -> Ordering) -> 'a -> 'a -> Bool` executable xvariable `x` type `'a` yvariable `y` type `'a` := (compareconstant `Prelude.Ord.compare` constant of type-class `Ord` type `'a -> 'a -> Ordering` executable same type-class instance xvariable `x` type `'a` yvariable `y` type `'a` ==constant `Prelude.Eq.(==)` constant of type-class `Eq` type `'a -> 'a -> Bool` type in context `Ordering -> Ordering -> Bool` executable statically resolved type-class instance GTconstant `Prelude.Ord.GT` constructor of datatype `Ordering` type `Ordering` executable) define maxconstant `Prelude.Ord.max` default instance of type-class constant type `('a -> 'a -> Bool) -> 'a -> 'a -> 'a` executable xvariable `x` type `'a` yvariable `y` type `'a` := if (xvariable `x` type `'a` <=constant `Prelude.Ord.(<=)` constant of type-class `Ord` type `'a -> 'a -> Bool` executable same type-class instance yvariable `y` type `'a`) then yvariable `y` type `'a` else xvariable `x` type `'a` define minconstant `Prelude.Ord.min` default instance of type-class constant type `('a -> 'a -> Bool) -> 'a -> 'a -> 'a` executable xvariable `x` type `'a` yvariable `y` type `'a` := if (xvariable `x` type `'a` <=constant `Prelude.Ord.(<=)` constant of type-class `Ord` type `'a -> 'a -> Bool` executable same type-class instance yvariable `y` type `'a`) then xvariable `x` type `'a` else yvariable `y` type `'a` test lt_alt_defsconstant `Prelude.Ord.lt_alt_defs` type-class test type `'a -> 'a -> Bool` executable (avariable `a` type `'a` :: 'atype-variable `'a` kind `*`) bvariable `b` type `'a` := ((avariable `a` type `'a` >constant `Prelude.Ord.(>)` constant of type-class `Ord` type `'a -> 'a -> Bool` executable same type-class instance bvariable `b` type `'a`) <->constant `Prelude.Bool.(<->)` constant type `Bool -> Bool -> Bool` executable (bvariable `b` type `'a` <constant `Prelude.Ord.(<)` constant of type-class `Ord` type `'a -> 'a -> Bool` executable same type-class instance avariable `a` type `'a`)) &&constant `Prelude.Bool.(&&)` constant type `Bool -> Bool -> Bool` executable ((avariable `a` type `'a` >=constant `Prelude.Ord.(>=)` constant of type-class `Ord` type `'a -> 'a -> Bool` executable same type-class instance bvariable `b` type `'a`) <->constant `Prelude.Bool.(<->)` constant type `Bool -> Bool -> Bool` executable (bvariable `b` type `'a` <=constant `Prelude.Ord.(<=)` constant of type-class `Ord` type `'a -> 'a -> Bool` executable same type-class instance avariable `a` type `'a`)) &&constant `Prelude.Bool.(&&)` constant type `Bool -> Bool -> Bool` executable ((avariable `a` type `'a` <=constant `Prelude.Ord.(<=)` constant of type-class `Ord` type `'a -> 'a -> Bool` executable same type-class instance bvariable `b` type `'a`) <->constant `Prelude.Bool.(<->)` constant type `Bool -> Bool -> Bool` executable ((avariable `a` type `'a` <constant `Prelude.Ord.(<)` constant of type-class `Ord` type `'a -> 'a -> Bool` executable same type-class instance bvariable `b` type `'a`) ||constant `Prelude.Bool.(||)` constant type `Bool -> Bool -> Bool` executable (avariable `a` type `'a` ==constant `Prelude.Eq.(==)` constant of type-class `Eq` type `'a -> 'a -> Bool` executable type-class instance from context bvariable `b` type `'a`))) test lt_irreflconstant `Prelude.Ord.lt_irrefl` type-class test type `'a -> Bool` executable (avariable `a` type `'a` :: 'atype-variable `'a` kind `*`) := notconstant `Prelude.Bool.not` constant type `Bool -> Bool` executable (avariable `a` type `'a` <constant `Prelude.Ord.(<)` constant of type-class `Ord` type `'a -> 'a -> Bool` executable same type-class instance avariable `a` type `'a`) test lt_transconstant `Prelude.Ord.lt_trans` type-class test type `'a -> 'a -> 'a -> Bool` executable (avariable `a` type `'a` :: 'atype-variable `'a` kind `*`) bvariable `b` type `'a` cvariable `c` type `'a` := ((avariable `a` type `'a` <constant `Prelude.Ord.(<)` constant of type-class `Ord` type `'a -> 'a -> Bool` executable same type-class instance bvariable `b` type `'a`) &&constant `Prelude.Bool.(&&)` constant type `Bool -> Bool -> Bool` executable (bvariable `b` type `'a` <constant `Prelude.Ord.(<)` constant of type-class `Ord` type `'a -> 'a -> Bool` executable same type-class instance cvariable `c` type `'a`)) -->constant `Prelude.Bool.(-->)` constant type `Bool -> Bool -> Bool` executable (avariable `a` type `'a` <constant `Prelude.Ord.(<)` constant of type-class `Ord` type `'a -> 'a -> Bool` executable same type-class instance cvariable `c` type `'a`) {-# minimal compare | (<) #-} end-class instance Ordtype-class `Prelude.Ord.Ord` arguments: ('a :: *) super-class constraints: - Prelude.Eq.Eq 'a has default derive templates () where define compareconstant `Prelude.Ord.compare` constant of type-class instance `Ord ()` type `() -> () -> Ordering` executable () () := EQconstant `Prelude.Ord.EQ` constructor of datatype `Ordering` type `Ordering` executable end-instance declare comparingconstant `Prelude.Ord.comparing` constant type `Ord 'a => ('b -> 'a) -> 'b -> 'b -> Ordering` executable :: Ordtype-class `Prelude.Ord.Ord` arguments: ('a :: *) super-class constraints: - Prelude.Eq.Eq 'a has default derive templates 'atype-variable `'a` kind `*` => ('btype-variable `'b` kind `*` -> 'atype-variable `'a` kind `*`) -> 'btype-variable `'b` kind `*` -> 'btype-variable `'b` kind `*` -> Orderingdatatype `Prelude.Ord.Ordering` kind `*` executable define comparingconstant `Prelude.Ord.comparing` constant type `Ord 'a => ('b -> 'a) -> 'b -> 'b -> Ordering` executable pvariable `p` type `'b -> 'a` xvariable `x` type `'b` yvariable `y` type `'b` := compareconstant `Prelude.Ord.compare` constant of type-class `Ord` type `'a -> 'a -> Ordering` executable type-class instance from argument (pvariable `p` type `'b -> 'a` xvariable `x` type `'b`) (pvariable `p` type `'b -> 'a` yvariable `y` type `'b`) declare lexCompareconstant `Prelude.Ord.lexCompare` constant type `Ord 'a => 'a -> 'a -> Ordering -> Ordering` executable :: Ordtype-class `Prelude.Ord.Ord` arguments: ('a :: *) super-class constraints: - Prelude.Eq.Eq 'a has default derive templates 'atype-variable `'a` kind `*` => 'atype-variable `'a` kind `*` -> 'atype-variable `'a` kind `*` -> Orderingdatatype `Prelude.Ord.Ordering` kind `*` executable -> Orderingdatatype `Prelude.Ord.Ordering` kind `*` executable define lexCompareconstant `Prelude.Ord.lexCompare` constant type `Ord 'a => 'a -> 'a -> Ordering -> Ordering` executable xvariable `x` type `'a` yvariable `y` type `'a` nextvariable `next` type `Ordering` := case (compareconstant `Prelude.Ord.compare` constant of type-class `Ord` type `'a -> 'a -> Ordering` executable type-class instance from argument xvariable `x` type `'a` yvariable `y` type `'a`) of EQconstant `Prelude.Ord.EQ` constructor of datatype `Ordering` type `Ordering` executable -> nextvariable `next` type `Ordering` | othervariable `other` type `Ordering` -> othervariable `other` type `Ordering` end {-# inline lexCompareconstant `Prelude.Ord.lexCompare` constant type `Ord 'a => 'a -> 'a -> Ordering -> Ordering` executable #-} template DeriveInstanceOrdBody (_ :: ClassID, ty :: TypeID, _ :: [String]) := ''' {{ var constrstemplate-variable `constrs` type [ConstID] := tytemplate-variable `ty` type TypeID.constructors; var clausestemplate-variable `clauses` type [String] := [] :: [String]; foreach var itemplate-variable `i` type Nat in constrstemplate-variable `constrs` type [ConstID].indices { name-scope { var (args1template-variable `args1` type [String], constr1template-variable `constr1` type String) := !ConstWithArgstemplate `Prelude.Template.ConstWithArgs` argument-types: (Bool, String, ConstID) return-types: ([String], String) does not compute text(True, "x", constrstemplate-variable `constrs` type [ConstID][itemplate-variable `i` type Nat]); var (args2template-variable `args2` type [String], constr2template-variable `constr2` type String) := !ConstWithArgstemplate `Prelude.Template.ConstWithArgs` argument-types: (Bool, String, ConstID) return-types: ([String], String) does not compute text(True, "y", constrstemplate-variable `constrs` type [ConstID][itemplate-variable `i` type Nat]); var cltemplate-variable `cl` type String := "compare " ++ constr1template-variable `constr1` type String ++ " " ++ constr2template-variable `constr2` type String ++ " := "; if (args1template-variable `args1` type [String].length > 0) { var rhstemplate-variable `rhs` type [String] := [] :: [String]; for var jtemplate-variable `j` type Nat := 1 to (args1template-variable `args1` type [String].length - 1) { var eltemplate-variable `el` type String := "lexCompare " ++ args1template-variable `args1` type [String][jtemplate-variable `j` type Nat-1] ++ " " ++ args2template-variable `args2` type [String][jtemplate-variable `j` type Nat-1]; rhstemplate-variable `rhs` type [String] := insertAtEnd(eltemplate-variable `el` type String, rhstemplate-variable `rhs` type [String]); } rhstemplate-variable `rhs` type [String] := insertAtEnd("compare "++ args1template-variable `args1` type [String][args1template-variable `args1` type [String].length - 1] ++ " " ++ args2template-variable `args2` type [String][args1template-variable `args1` type [String].length - 1], rhstemplate-variable `rhs` type [String]); cltemplate-variable `cl` type String := cltemplate-variable `cl` type String ++ !Intercalatetemplate `Prelude.Template.Intercalate` argument-types: (String, [String]) return-type: String does not compute text(" $ ", rhstemplate-variable `rhs` type [String]); } else { cltemplate-variable `cl` type String := cltemplate-variable `cl` type String ++ "EQ" } clausestemplate-variable `clauses` type [String] := insertAtEnd(cltemplate-variable `cl` type String, clausestemplate-variable `clauses` type [String]); var constrWctemplate-variable `constrWc` type String := !ConstWithWildcardArgstemplate `Prelude.Template.ConstWithWildcardArgs` argument-types: (Bool, ConstID) return-type: String does not compute text(True, constrstemplate-variable `constrs` type [ConstID][itemplate-variable `i` type Nat]); if (itemplate-variable `i` type Nat < constrstemplate-variable `constrs` type [ConstID].length - 1) { clausestemplate-variable `clauses` type [String] := insertAtEnd("compare " ++ constrWctemplate-variable `constrWc` type String ++ " _ := LT", clausestemplate-variable `clauses` type [String]); clausestemplate-variable `clauses` type [String] := insertAtEnd("compare _ " ++ constrWctemplate-variable `constrWc` type String ++ " := GT", clausestemplate-variable `clauses` type [String]); } } } var recDecltemplate-variable `recDecl` type String, indentRectemplate-variable `indentRec` type String := ""; if (tytemplate-variable `ty` type TypeID.isRec) { recDecltemplate-variable `recDecl` type String := "rec "; indentRectemplate-variable `indentRec` type String := " "; } }} {{= "define " ++ recDecltemplate-variable `recDecl` type String ++ !Intercalatetemplate `Prelude.Template.Intercalate` argument-types: (String, [String]) return-type: String does not compute text("\n "++indentRectemplate-variable `indentRec` type String++"| ", clausestemplate-variable `clauses` type [String]) =}} ''' register-derive-template Ordtype-class `Prelude.Ord.Ord` arguments: ('a :: *) super-class constraints: - Prelude.Eq.Eq 'a has default derive templates DeriveInstanceOrdBodytemplate `Prelude.Ord.DeriveInstanceOrdBody` argument-types: (ClassID, TypeID, [String]) return-type: - derive Orderingdatatype `Prelude.Ord.Ordering` kind `*` executable instances Ordtype-class `Prelude.Ord.Ord` arguments: ('a :: *) super-class constraints: - Prelude.Eq.Eq 'a has default derive templates
generated code: instance Ord Ordering where define compare LT LT := EQ | compare LT _ := LT | compare _ LT := GT | compare EQ EQ := EQ | compare EQ _ := LT | compare _ EQ := GT | compare GT GT := EQ end-instance
derive Booldatatype `Prelude.Bool.Bool` kind `*` executable instances Ordtype-class `Prelude.Ord.Ord` arguments: ('a :: *) super-class constraints: - Prelude.Eq.Eq 'a has default derive templates
generated code: instance Ord Bool where define compare False False := EQ | compare False _ := LT | compare _ False := GT | compare True True := EQ end-instance
end-moduleend of module Prelude.Ord