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 -- | Parse 'compare'.
 105 compare_from
 106  :: forall root ty ast hs ret.
 107  ( ty ~ Type_Root_of_Expr (Expr_Ord root)
 108  , Type0_Eq ty
 109  , Expr_From ast root
 110  , Type0_Lift Type_Ordering (Type_of_Expr root)
 111  , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
 112                    (Error_of_Expr ast root)
 113  , Root_of_Expr root ~ root
 114  , Type0_Constraint Ord ty
 115  ) => ast -> ast
 116  -> ExprFrom ast (Expr_Ord root) hs ret
 117 compare_from ast_x ast_y ex ast ctx k =
 118         expr_from (Proxy::Proxy root) ast_x ctx $
 119          \(ty_x::ty h_x) (Forall_Repr_with_Context x) ->
 120         expr_from (Proxy::Proxy root) ast_y ctx $
 121          \(ty_y::ty h_y) (Forall_Repr_with_Context y) ->
 122         check_type0_eq ex ast ty_x ty_y $ \Refl ->
 123         check_type0_constraint ex (Proxy::Proxy Ord) ast ty_x $ \Dict ->
 124         k type_ordering $ Forall_Repr_with_Context $
 125          \c -> x c `compare` y c
 126
 127 -- | Parse 'compare', partially applied.
 128 compare_from1
 129  :: forall root ty ast hs ret.
 130  ( ty ~ Type_Root_of_Expr (Expr_Ord root)
 131  , Type0_Eq ty
 132  , Expr_From ast root
 133  , Type0_Lift Type_Ordering (Type_of_Expr root)
 134  , Type0_Lift Type_Fun      (Type_of_Expr root)
 135  , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
 136                    (Error_of_Expr ast root)
 137  , Root_of_Expr root ~ root
 138  , Type0_Constraint Ord ty
 139  ) => ast
 140  -> ExprFrom ast (Expr_Ord root) hs ret
 141 compare_from1 ast_x ex ast ctx k =
 142         expr_from (Proxy::Proxy root) ast_x ctx $
 143          \(ty_x::ty h_x) (Forall_Repr_with_Context x) ->
 144         check_type0_constraint ex (Proxy::Proxy Ord) ast ty_x $ \Dict ->
 145         k (type_fun ty_x type_ordering) $ Forall_Repr_with_Context $
 146          \c -> lam $ \y -> x c `compare` y
 147
 148 -- | Parse '<', '<=', '>', or '>='.
 149 ord_from
 150  :: forall root ty ast hs ret.
 151  ( ty ~ Type_Root_of_Expr (Expr_Ord root)
 152  , Type0_Lift Type_Bool (Type_of_Expr root)
 153  , Type0_Eq ty
 154  , Expr_From ast root
 155  , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
 156                    (Error_of_Expr ast root)
 157  , Root_of_Expr root ~ root
 158  , Type0_Constraint Ord ty
 159  ) => (forall repr a. (Sym_Ord repr, Ord a) => repr a -> repr a -> repr Bool)
 160  -> ast -> ast
 161  -> ExprFrom ast (Expr_Ord root) hs ret
 162 ord_from test ast_x ast_y ex ast ctx k =
 163         expr_from (Proxy::Proxy root) ast_x ctx $
 164          \(ty_x::ty h_x) (Forall_Repr_with_Context x) ->
 165         expr_from (Proxy::Proxy root) ast_y ctx $
 166          \(ty_y::ty h_y) (Forall_Repr_with_Context y) ->
 167         check_type0_eq ex ast ty_x ty_y $ \Refl ->
 168         check_type0_constraint ex (Proxy::Proxy Ord) ast ty_x $ \Dict ->
 169         k type_bool $ Forall_Repr_with_Context $
 170          \c -> x c `test` y c
 171
 172 -- | Parse '<', '<=', '>', or '>=', partially applied.
 173 ord_from1
 174  :: forall root ty ast hs ret.
 175  ( ty ~ Type_Root_of_Expr (Expr_Ord root)
 176  , Type0_Lift Type_Bool (Type_of_Expr root)
 177  , Type0_Lift Type_Fun  (Type_of_Expr root)
 178  , Type0_Eq ty
 179  , Expr_From ast root
 180  , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
 181                    (Error_of_Expr ast root)
 182  , Root_of_Expr root ~ root
 183  , Type0_Constraint Ord ty
 184  ) => (forall repr a. (Sym_Ord repr, Ord a) => repr a -> repr a -> repr Bool)
 185  -> ast
 186  -> ExprFrom ast (Expr_Ord root) hs ret
 187 ord_from1 test ast_x ex ast ctx k =
 188         expr_from (Proxy::Proxy root) ast_x ctx $
 189          \(ty_x::ty h_x) (Forall_Repr_with_Context x) ->
 190         check_type0_constraint ex (Proxy::Proxy Ord) ast ty_x $ \Dict ->
 191         k (type_fun ty_x type_bool) $ Forall_Repr_with_Context $
 192          \c -> lam $ \y -> x c `test` y