]> Git — Sourcephile - haskell/symantic.git/blob - Language/Symantic/Expr/Ord.hs
polish names
[haskell/symantic.git] / Language / Symantic / Expr / Ord.hs
1 {-# LANGUAGE DefaultSignatures #-}
2 {-# LANGUAGE FlexibleContexts #-}
3 {-# LANGUAGE FlexibleInstances #-}
4 {-# LANGUAGE MultiParamTypeClasses #-}
5 {-# LANGUAGE OverloadedStrings #-}
6 {-# LANGUAGE Rank2Types #-}
7 {-# LANGUAGE ScopedTypeVariables #-}
8 {-# LANGUAGE TypeFamilies #-}
9 {-# LANGUAGE TypeOperators #-}
10 {-# OPTIONS_GHC -fno-warn-orphans #-}
11 -- | Expression for 'Ord'.
12 module Language.Symantic.Expr.Ord where
13
14 import Control.Monad
15 import qualified Data.Ord as Ord
16 import Data.Proxy (Proxy(..))
17 import Data.Type.Equality ((:~:)(Refl))
18 import Data.Ord (Ord)
19 import Prelude hiding (Ord(..))
20
21 import Language.Symantic.Type
22 import Language.Symantic.Repr
23 import Language.Symantic.Expr.Root
24 import Language.Symantic.Expr.Error
25 import Language.Symantic.Expr.From
26 import Language.Symantic.Expr.Eq
27 import Language.Symantic.Trans.Common
28
29 -- * Class 'Sym_Ord'
30 -- | Symantic.
31 class Sym_Eq repr => Sym_Ord repr where
32 compare :: Ord a => repr a -> repr a -> repr Ordering
33 (<) :: Ord a => repr a -> repr a -> repr Bool
34 (<=) :: Ord a => repr a -> repr a -> repr Bool
35 (>) :: Ord a => repr a -> repr a -> repr Bool
36 (>=) :: Ord a => repr a -> repr a -> repr Bool
37 max :: Ord a => repr a -> repr a -> repr a
38 min :: Ord a => repr a -> repr a -> repr a
39
40 default compare :: (Trans t repr, Ord a) => t repr a -> t repr a -> t repr Ordering
41 default (<) :: (Trans t repr, Ord a) => t repr a -> t repr a -> t repr Bool
42 default (<=) :: (Trans t repr, Ord a) => t repr a -> t repr a -> t repr Bool
43 default (>) :: (Trans t repr, Ord a) => t repr a -> t repr a -> t repr Bool
44 default (>=) :: (Trans t repr, Ord a) => t repr a -> t repr a -> t repr Bool
45 default max :: (Trans t repr, Ord a) => t repr a -> t repr a -> t repr a
46 default min :: (Trans t repr, Ord a) => t repr a -> t repr a -> t repr a
47
48 compare = trans_map2 compare
49 (<) = trans_map2 (<)
50 (<=) = trans_map2 (<=)
51 (>) = trans_map2 (>)
52 (>=) = trans_map2 (>=)
53 min = trans_map2 min
54 max = trans_map2 max
55
56 infix 4 <
57 infix 4 <=
58 infix 4 >
59 infix 4 >=
60
61 instance Sym_Ord Repr_Host where
62 compare = liftM2 Ord.compare
63 (<) = liftM2 (Ord.<)
64 (<=) = liftM2 (Ord.<=)
65 (>) = liftM2 (Ord.>)
66 (>=) = liftM2 (Ord.>=)
67 min = liftM2 Ord.min
68 max = liftM2 Ord.max
69 instance Sym_Ord Repr_Text where
70 compare = repr_text_app2 "compare"
71 (<) = repr_text_infix "<" (Precedence 4)
72 (<=) = repr_text_infix "<=" (Precedence 4)
73 (>) = repr_text_infix ">" (Precedence 4)
74 (>=) = repr_text_infix ">=" (Precedence 4)
75 min = repr_text_app2 "min"
76 max = repr_text_app2 "max"
77 instance
78 ( Sym_Ord r1
79 , Sym_Ord r2
80 ) => Sym_Ord (Repr_Dup r1 r2) where
81 compare (x1 `Repr_Dup` x2) (y1 `Repr_Dup` y2) =
82 compare x1 y1 `Repr_Dup` compare x2 y2
83 (<) (x1 `Repr_Dup` x2) (y1 `Repr_Dup` y2) =
84 (<) x1 y1 `Repr_Dup` (<) x2 y2
85 (<=) (x1 `Repr_Dup` x2) (y1 `Repr_Dup` y2) =
86 (<=) x1 y1 `Repr_Dup` (<=) x2 y2
87 (>) (x1 `Repr_Dup` x2) (y1 `Repr_Dup` y2) =
88 (>) x1 y1 `Repr_Dup` (>) x2 y2
89 (>=) (x1 `Repr_Dup` x2) (y1 `Repr_Dup` y2) =
90 (>=) x1 y1 `Repr_Dup` (>=) x2 y2
91 min (x1 `Repr_Dup` x2) (y1 `Repr_Dup` y2) =
92 min x1 y1 `Repr_Dup` min x2 y2
93 max (x1 `Repr_Dup` x2) (y1 `Repr_Dup` y2) =
94 max x1 y1 `Repr_Dup` max x2 y2
95
96 -- * Type 'Expr_Ord'
97 -- | Expression.
98 data Expr_Ord (root:: *)
99 type instance Root_of_Expr (Expr_Ord root) = root
100 type instance Type_of_Expr (Expr_Ord root) = Type_Ordering
101 type instance Sym_of_Expr (Expr_Ord root) repr = (Sym_Ord repr)
102 type instance Error_of_Expr ast (Expr_Ord root) = No_Error_Expr
103
104 compare_from
105 :: forall root ty ast hs ret.
106 ( ty ~ Type_Root_of_Expr (Expr_Ord root)
107 , Type0_Eq ty
108 , Expr_From ast root
109 , Type0_Lift Type_Ordering (Type_of_Expr root)
110 , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
111 (Error_of_Expr ast root)
112 , Root_of_Expr root ~ root
113 , Type0_Constraint Ord ty
114 ) => ast -> ast
115 -> ExprFrom ast (Expr_Ord root) hs ret
116 compare_from ast_x ast_y ex ast ctx k =
117 expr_from (Proxy::Proxy root) ast_x ctx $
118 \(ty_x::ty h_x) (Forall_Repr_with_Context x) ->
119 expr_from (Proxy::Proxy root) ast_y ctx $
120 \(ty_y::ty h_y) (Forall_Repr_with_Context y) ->
121 check_type0_eq ex ast ty_x ty_y $ \Refl ->
122 check_type0_constraint ex (Proxy::Proxy Ord) ast ty_x $ \Dict ->
123 k type_ordering $ Forall_Repr_with_Context $
124 \c -> x c `compare` y c
125
126 ord_from
127 :: forall root ty ast hs ret.
128 ( ty ~ Type_Root_of_Expr (Expr_Ord root)
129 , Type0_Lift Type_Bool (Type_of_Expr root)
130 , Type0_Eq ty
131 , Expr_From ast root
132 , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
133 (Error_of_Expr ast root)
134 , Root_of_Expr root ~ root
135 , Type0_Constraint Ord ty
136 ) => (forall repr a. (Sym_Ord repr, Ord a) => repr a -> repr a -> repr Bool)
137 -> ast -> ast
138 -> ExprFrom ast (Expr_Ord root) hs ret
139 ord_from test ast_x ast_y ex ast ctx k =
140 expr_from (Proxy::Proxy root) ast_x ctx $
141 \(ty_x::ty h_x) (Forall_Repr_with_Context x) ->
142 expr_from (Proxy::Proxy root) ast_y ctx $
143 \(ty_y::ty h_y) (Forall_Repr_with_Context y) ->
144 check_type0_eq ex ast ty_x ty_y $ \Refl ->
145 check_type0_constraint ex (Proxy::Proxy Ord) ast ty_x $ \Dict ->
146 k type_bool $ Forall_Repr_with_Context $
147 \c -> x c `test` y c