]> Git — Sourcephile - haskell/symantic.git/blob - symantic-lib/Language/Symantic/Lib/Ord.hs
Integrate types to the module system.
[haskell/symantic.git] / symantic-lib / Language / Symantic / Lib / Ord.hs
1 {-# LANGUAGE UndecidableInstances #-}
2 {-# OPTIONS_GHC -fno-warn-orphans #-}
3 -- | Symantic for 'Ord'.
4 module Language.Symantic.Lib.Ord where
5
6 import Data.Ord (Ord)
7 import Prelude hiding (Ord(..))
8 import qualified Data.Ord as Ord
9 import qualified Data.Text as Text
10
11 import Language.Symantic
12 import Language.Symantic.Lib.Bool (tyBool)
13 import Language.Symantic.Lib.Function (a0)
14 import Language.Symantic.Lib.Eq (Sym_Eq)
15
16 -- * Class 'Sym_Ordering'
17 type instance Sym Ordering = Sym_Ordering
18 class Sym_Eq term => Sym_Ordering term where
19 ordering :: Ordering -> term Ordering
20 default ordering :: Sym_Ordering (UnT term) => Trans term => Ordering -> term Ordering
21 ordering = trans . ordering
22
23 -- Interpreting
24 instance Sym_Ordering Eval where
25 ordering = Eval
26 instance Sym_Ordering View where
27 ordering o = View $ \_p _v ->
28 Text.pack (show o)
29 instance (Sym_Ordering r1, Sym_Ordering r2) => Sym_Ordering (Dup r1 r2) where
30 ordering o = ordering o `Dup` ordering o
31
32 -- Transforming
33 instance (Sym_Ordering term, Sym_Lambda term) => Sym_Ordering (BetaT term)
34
35 -- Typing
36 instance NameTyOf Ordering where
37 nameTyOf _c = ["Ord"] `Mod` "Ordering"
38 instance ClassInstancesFor Ordering
39 instance TypeInstancesFor Ordering
40
41 -- Compiling
42 instance Gram_Term_AtomsFor src ss g Ordering
43 instance (Source src, SymInj ss Ordering) => ModuleFor src ss Ordering where
44 moduleFor = [] `moduleWhere`
45 [ "LT" := teOrdering LT
46 , "EQ" := teOrdering EQ
47 , "GT" := teOrdering GT
48 ]
49
50 -- ** 'Type's
51 tyOrdering :: Source src => LenInj vs => Type src vs Ordering
52 tyOrdering = tyConst @(K Ordering) @Ordering
53
54 -- ** 'Term's
55 teOrdering :: Source src => SymInj ss Ordering => Ordering -> Term src ss ts '[] (() #> Ordering)
56 teOrdering o = Term noConstraint tyOrdering $ teSym @Ordering $ ordering o
57
58 -- * Class 'Sym_Ord'
59 type instance Sym Ord = Sym_Ord
60 class Sym_Eq term => Sym_Ord term where
61 compare :: Ord a => term a -> term a -> term Ordering
62 (<) :: Ord a => term a -> term a -> term Bool; infix 4 <
63 (<=) :: Ord a => term a -> term a -> term Bool; infix 4 <=
64 (>) :: Ord a => term a -> term a -> term Bool; infix 4 >
65 (>=) :: Ord a => term a -> term a -> term Bool; infix 4 >=
66 max :: Ord a => term a -> term a -> term a
67 min :: Ord a => term a -> term a -> term a
68
69 default compare :: Sym_Ord (UnT term) => Trans term => Ord a => term a -> term a -> term Ordering
70 default (<) :: Sym_Ord (UnT term) => Trans term => Ord a => term a -> term a -> term Bool
71 default (<=) :: Sym_Ord (UnT term) => Trans term => Ord a => term a -> term a -> term Bool
72 default (>) :: Sym_Ord (UnT term) => Trans term => Ord a => term a -> term a -> term Bool
73 default (>=) :: Sym_Ord (UnT term) => Trans term => Ord a => term a -> term a -> term Bool
74 default max :: Sym_Ord (UnT term) => Trans term => Ord a => term a -> term a -> term a
75 default min :: Sym_Ord (UnT term) => Trans term => Ord a => term a -> term a -> term a
76
77 compare = trans2 compare
78 (<) = trans2 (<)
79 (<=) = trans2 (<=)
80 (>) = trans2 (>)
81 (>=) = trans2 (>=)
82 min = trans2 min
83 max = trans2 max
84
85 -- Interpreting
86 instance Sym_Ord Eval where
87 compare = eval2 Ord.compare
88 (<) = eval2 (Ord.<)
89 (<=) = eval2 (Ord.<=)
90 (>) = eval2 (Ord.>)
91 (>=) = eval2 (Ord.>=)
92 min = eval2 Ord.min
93 max = eval2 Ord.max
94 instance Sym_Ord View where
95 compare = view2 "compare"
96 (<) = viewInfix "<" (infixN 4)
97 (<=) = viewInfix "<=" (infixN 4)
98 (>) = viewInfix ">" (infixN 4)
99 (>=) = viewInfix ">=" (infixN 4)
100 min = view2 "min"
101 max = view2 "max"
102 instance (Sym_Ord r1, Sym_Ord r2) => Sym_Ord (Dup r1 r2) where
103 compare = dup2 @Sym_Ord compare
104 (<) = dup2 @Sym_Ord (<)
105 (<=) = dup2 @Sym_Ord (<=)
106 (>) = dup2 @Sym_Ord (>)
107 (>=) = dup2 @Sym_Ord (>=)
108 min = dup2 @Sym_Ord min
109 max = dup2 @Sym_Ord max
110
111 -- Transforming
112 instance (Sym_Ord term, Sym_Lambda term) => Sym_Ord (BetaT term)
113
114 -- Typing
115 instance NameTyOf Ord where
116 nameTyOf _c = ["Ord"] `Mod` "Ord"
117 instance FixityOf Ord
118 instance ClassInstancesFor Ord where
119 proveConstraintFor _ (TyApp _ (TyConst _ _ q) z)
120 | Just HRefl <- proj_ConstKiTy @_ @Ordering z
121 = case () of
122 _ | Just Refl <- proj_Const @Bounded q -> Just Dict
123 | Just Refl <- proj_Const @Enum q -> Just Dict
124 | Just Refl <- proj_Const @Eq q -> Just Dict
125 | Just Refl <- proj_Const @Ord q -> Just Dict
126 | Just Refl <- proj_Const @Show q -> Just Dict
127 _ -> Nothing
128 proveConstraintFor _c _q = Nothing
129 instance TypeInstancesFor Ord
130
131 -- Compiling
132 instance Gram_Term_AtomsFor src ss g Ord
133 instance (Source src, SymInj ss Ord) => ModuleFor src ss Ord where
134 moduleFor = ["Ord"] `moduleWhere`
135 [ "compare" := teOrd_compare
136 , "<" `withInfixN` 4 := teOrd_lt
137 , "<=" `withInfixN` 4 := teOrd_le
138 , ">" `withInfixN` 4 := teOrd_gt
139 , ">=" `withInfixN` 4 := teOrd_ge
140 ]
141
142 -- ** 'Type's
143 tyOrd :: Source src => Type src vs a -> Type src vs (Ord a)
144 tyOrd a = tyConstLen @(K Ord) @Ord (lenVars a) `tyApp` a
145
146 -- ** 'Term's
147 teOrd_compare :: TermDef Ord '[Proxy a] (Ord a #> (a -> a -> Ordering))
148 teOrd_compare = Term (tyOrd a0) (a0 ~> a0 ~> tyOrdering) $ teSym @Ord $ lam2 compare
149
150 teOrd_le, teOrd_lt, teOrd_ge, teOrd_gt :: TermDef Ord '[Proxy a] (Ord a #> (a -> a -> Bool))
151 teOrd_le = Term (tyOrd a0) (a0 ~> a0 ~> tyBool) $ teSym @Ord $ lam2 (<=)
152 teOrd_lt = Term (tyOrd a0) (a0 ~> a0 ~> tyBool) $ teSym @Ord $ lam2 (<)
153 teOrd_ge = Term (tyOrd a0) (a0 ~> a0 ~> tyBool) $ teSym @Ord $ lam2 (>=)
154 teOrd_gt = Term (tyOrd a0) (a0 ~> a0 ~> tyBool) $ teSym @Ord $ lam2 (>)
155
156 teOrd_min, teOrd_max :: TermDef Ord '[Proxy a] (Ord a #> (a -> a -> a))
157 teOrd_min = Term (tyOrd a0) (a0 ~> a0 ~> a0) $ teSym @Ord $ lam2 min
158 teOrd_max = Term (tyOrd a0) (a0 ~> a0 ~> a0) $ teSym @Ord $ lam2 max