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