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