]> Git — Sourcephile - haskell/symantic.git/blob - Language/Symantic/Expr/Ord.hs
Repr_Dup helpers
[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 (Sym_Ord r1, Sym_Ord r2) => Sym_Ord (Repr_Dup r1 r2) where
78 compare = repr_dup2 sym_Ord compare
79 (<) = repr_dup2 sym_Ord (<)
80 (<=) = repr_dup2 sym_Ord (<=)
81 (>) = repr_dup2 sym_Ord (>)
82 (>=) = repr_dup2 sym_Ord (>=)
83 min = repr_dup2 sym_Ord min
84 max = repr_dup2 sym_Ord max
85
86 sym_Ord :: Proxy Sym_Ord
87 sym_Ord = Proxy
88
89 -- * Type 'Expr_Ord'
90 -- | Expression.
91 data Expr_Ord (root:: *)
92 type instance Root_of_Expr (Expr_Ord root) = root
93 type instance Type_of_Expr (Expr_Ord root) = Type_Ordering
94 type instance Sym_of_Expr (Expr_Ord root) repr = (Sym_Ord repr)
95 type instance Error_of_Expr ast (Expr_Ord root) = No_Error_Expr
96
97 -- | Parse 'compare'.
98 compare_from
99 :: forall root ty ast hs ret.
100 ( ty ~ Type_Root_of_Expr (Expr_Ord root)
101 , Type0_Eq ty
102 , Expr_From ast root
103 , Type0_Lift Type_Ordering (Type_of_Expr root)
104 , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
105 (Error_of_Expr ast root)
106 , Root_of_Expr root ~ root
107 , Type0_Constraint Ord ty
108 ) => ast -> ast
109 -> ExprFrom ast (Expr_Ord root) hs ret
110 compare_from ast_x ast_y ex ast ctx k =
111 expr_from (Proxy::Proxy root) ast_x ctx $
112 \(ty_x::ty h_x) (Forall_Repr_with_Context x) ->
113 expr_from (Proxy::Proxy root) ast_y ctx $
114 \(ty_y::ty h_y) (Forall_Repr_with_Context y) ->
115 check_type0_eq ex ast ty_x ty_y $ \Refl ->
116 check_type0_constraint ex (Proxy::Proxy Ord) ast ty_x $ \Dict ->
117 k type_ordering $ Forall_Repr_with_Context $
118 \c -> x c `compare` y c
119
120 -- | Parse 'compare', partially applied.
121 compare_from1
122 :: forall root ty ast hs ret.
123 ( ty ~ Type_Root_of_Expr (Expr_Ord root)
124 , Type0_Eq ty
125 , Expr_From ast root
126 , Type0_Lift Type_Ordering (Type_of_Expr root)
127 , Type0_Lift Type_Fun (Type_of_Expr root)
128 , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
129 (Error_of_Expr ast root)
130 , Root_of_Expr root ~ root
131 , Type0_Constraint Ord ty
132 ) => ast
133 -> ExprFrom ast (Expr_Ord root) hs ret
134 compare_from1 ast_x ex ast ctx k =
135 expr_from (Proxy::Proxy root) ast_x ctx $
136 \(ty_x::ty h_x) (Forall_Repr_with_Context x) ->
137 check_type0_constraint ex (Proxy::Proxy Ord) ast ty_x $ \Dict ->
138 k (type_fun ty_x type_ordering) $ Forall_Repr_with_Context $
139 \c -> lam $ \y -> x c `compare` y
140
141 -- | Parse '<', '<=', '>', or '>='.
142 ord_from
143 :: forall root ty ast hs ret.
144 ( ty ~ Type_Root_of_Expr (Expr_Ord root)
145 , Type0_Lift Type_Bool (Type_of_Expr root)
146 , Type0_Eq ty
147 , Expr_From ast root
148 , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
149 (Error_of_Expr ast root)
150 , Root_of_Expr root ~ root
151 , Type0_Constraint Ord ty
152 ) => (forall repr a. (Sym_Ord repr, Ord a) => repr a -> repr a -> repr Bool)
153 -> ast -> ast
154 -> ExprFrom ast (Expr_Ord root) hs ret
155 ord_from test ast_x ast_y ex ast ctx k =
156 expr_from (Proxy::Proxy root) ast_x ctx $
157 \(ty_x::ty h_x) (Forall_Repr_with_Context x) ->
158 expr_from (Proxy::Proxy root) ast_y ctx $
159 \(ty_y::ty h_y) (Forall_Repr_with_Context y) ->
160 check_type0_eq ex ast ty_x ty_y $ \Refl ->
161 check_type0_constraint ex (Proxy::Proxy Ord) ast ty_x $ \Dict ->
162 k type_bool $ Forall_Repr_with_Context $
163 \c -> x c `test` y c
164
165 -- | Parse '<', '<=', '>', or '>=', partially applied.
166 ord_from1
167 :: forall root ty ast hs ret.
168 ( ty ~ Type_Root_of_Expr (Expr_Ord root)
169 , Type0_Lift Type_Bool (Type_of_Expr root)
170 , Type0_Lift Type_Fun (Type_of_Expr root)
171 , Type0_Eq ty
172 , Expr_From ast root
173 , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
174 (Error_of_Expr ast root)
175 , Root_of_Expr root ~ root
176 , Type0_Constraint Ord ty
177 ) => (forall repr a. (Sym_Ord repr, Ord a) => repr a -> repr a -> repr Bool)
178 -> ast
179 -> ExprFrom ast (Expr_Ord root) hs ret
180 ord_from1 test ast_x ex ast ctx k =
181 expr_from (Proxy::Proxy root) ast_x ctx $
182 \(ty_x::ty h_x) (Forall_Repr_with_Context x) ->
183 check_type0_constraint ex (Proxy::Proxy Ord) ast ty_x $ \Dict ->
184 k (type_fun ty_x type_bool) $ Forall_Repr_with_Context $
185 \c -> lam $ \y -> x c `test` y