Language/Symantic/Compiling/Ord.hs

   1 {-# LANGUAGE DataKinds #-}
   2 {-# LANGUAGE DefaultSignatures #-}
   3 {-# LANGUAGE FlexibleContexts #-}
   4 {-# LANGUAGE FlexibleInstances #-}
   5 {-# LANGUAGE MultiParamTypeClasses #-}
   6 {-# LANGUAGE OverloadedStrings #-}
   7 {-# LANGUAGE Rank2Types #-}
   8 {-# LANGUAGE ScopedTypeVariables #-}
   9 {-# LANGUAGE TypeFamilies #-}
  10 {-# LANGUAGE TypeOperators #-}
  11 {-# LANGUAGE UndecidableInstances #-}
  12 {-# OPTIONS_GHC -fno-warn-orphans #-}
  13 -- | Symantic for 'Ord'.
  14 module Language.Symantic.Compiling.Ord where
  15
  16 import Control.Monad
  17 import Data.Ord (Ord)
  18 import qualified Data.Ord as Ord
  19 import Data.Proxy (Proxy(..))
  20 import Data.String (IsString)
  21 import Data.Text (Text)
  22 import Data.Type.Equality ((:~:)(Refl))
  23 import qualified Data.Kind as Kind
  24 import Prelude hiding (Ord(..))
  25
  26 import Language.Symantic.Typing
  27 import Language.Symantic.Compiling.Term
  28 import Language.Symantic.Compiling.Bool
  29 import Language.Symantic.Compiling.Eq
  30 import Language.Symantic.Interpreting
  31 import Language.Symantic.Transforming.Trans
  32
  33 -- * Class 'Sym_Ord'
  34 class Sym_Eq term => Sym_Ord term where
  35         compare :: Ord a => term a -> term a -> term Ordering
  36         (<)     :: Ord a => term a -> term a -> term Bool
  37         (<=)    :: Ord a => term a -> term a -> term Bool
  38         (>)     :: Ord a => term a -> term a -> term Bool
  39         (>=)    :: Ord a => term a -> term a -> term Bool
  40         max     :: Ord a => term a -> term a -> term a
  41         min     :: Ord a => term a -> term a -> term a
  42
  43         default compare :: (Trans t term, Ord a) => t term a -> t term a -> t term Ordering
  44         default (<)     :: (Trans t term, Ord a) => t term a -> t term a -> t term Bool
  45         default (<=)    :: (Trans t term, Ord a) => t term a -> t term a -> t term Bool
  46         default (>)     :: (Trans t term, Ord a) => t term a -> t term a -> t term Bool
  47         default (>=)    :: (Trans t term, Ord a) => t term a -> t term a -> t term Bool
  48         default max     :: (Trans t term, Ord a) => t term a -> t term a -> t term a
  49         default min     :: (Trans t term, Ord a) => t term a -> t term a -> t term a
  50
  51         compare  = trans_map2 compare
  52         (<)      = trans_map2 (<)
  53         (<=)     = trans_map2 (<=)
  54         (>)      = trans_map2 (>)
  55         (>=)     = trans_map2 (>=)
  56         min      = trans_map2 min
  57         max      = trans_map2 max
  58
  59 infix 4 <
  60 infix 4 <=
  61 infix 4 >
  62 infix 4 >=
  63
  64 type instance Sym_of_Iface (Proxy Ord) = Sym_Ord
  65 type instance Consts_of_Iface (Proxy Ord) = Proxy Ord ': Consts_imported_by Ord
  66 type instance Consts_imported_by Ord = '[]
  67
  68 instance Sym_Ord HostI where
  69         compare = liftM2 Ord.compare
  70         (<)     = liftM2 (Ord.<)
  71         (<=)    = liftM2 (Ord.<=)
  72         (>)     = liftM2 (Ord.>)
  73         (>=)    = liftM2 (Ord.>=)
  74         min     = liftM2 Ord.min
  75         max     = liftM2 Ord.max
  76 instance Sym_Ord TextI where
  77         compare = textI_app2  "compare"
  78         (<)     = textI_infix "<"  (Precedence 4)
  79         (<=)    = textI_infix "<=" (Precedence 4)
  80         (>)     = textI_infix ">"  (Precedence 4)
  81         (>=)    = textI_infix ">=" (Precedence 4)
  82         min     = textI_app2  "min"
  83         max     = textI_app2  "max"
  84 instance (Sym_Ord r1, Sym_Ord r2) => Sym_Ord (DupI r1 r2) where
  85         compare = dupI2 sym_Ord compare
  86         (<)     = dupI2 sym_Ord (<)
  87         (<=)    = dupI2 sym_Ord (<=)
  88         (>)     = dupI2 sym_Ord (>)
  89         (>=)    = dupI2 sym_Ord (>=)
  90         min     = dupI2 sym_Ord min
  91         max     = dupI2 sym_Ord max
  92
  93 instance Const_from Text cs => Const_from Text (Proxy Ord ': cs) where
  94         const_from "Ord" k = k (ConstZ kind)
  95         const_from s k = const_from s $ k . ConstS
  96 instance Show_Const cs => Show_Const (Proxy Ord ': cs) where
  97         show_const ConstZ{} = "Ord"
  98         show_const (ConstS c) = show_const c
  99
 100 instance -- Proj_ConC
 101  Proj_ConC cs (Proxy Ord)
 102 instance -- Term_fromI
 103  ( AST ast
 104  , Lexem ast ~ LamVarName
 105  , Inj_Const (Consts_of_Ifaces is) Bool
 106  , Inj_Const (Consts_of_Ifaces is) (->)
 107  , Inj_Const (Consts_of_Ifaces is) Ord
 108  , Inj_Const (Consts_of_Ifaces is) Ordering
 109  , Proj_Con (Consts_of_Ifaces is)
 110  , Term_from is ast
 111  ) => Term_fromI is (Proxy Ord) ast where
 112         term_fromI ast =
 113                 case ast_lexem ast of
 114                  "compare" -> test2_from compare tyOrdering
 115                  "<="      -> test2_from (<=)    tyBool
 116                  "<"       -> test2_from (<)     tyBool
 117                  ">="      -> test2_from (>=)    tyBool
 118                  ">"       -> test2_from (>)     tyBool
 119                  "min"     -> op2_from min
 120                  "max"     -> op2_from max
 121                  _ -> \_ctx _k -> Left $ Error_Term_unsupported
 122                 where
 123                 test2_from
 124                  :: (forall term a. (Sym_Ord term, Ord a) => term a -> term a -> term res)
 125                  -> Type (Consts_of_Ifaces is) (res::Kind.Type)
 126                  -> LamCtx_Type is (Lexem ast) ctx
 127                  -> ( forall h. Type (Consts_of_Ifaces is) (h::Kind.Type)
 128                              -> TermLC ctx h is ls (Proxy Ord ': rs)
 129                              -> Either (Error_Term is ast) ret )
 130                  -> Either (Error_Term is ast) ret
 131                 test2_from op ty_res ctx k =
 132                         case ast_nodes ast of
 133                          [] -> Left $ Error_Term_Syntax $
 134                                 Error_Syntax_more_arguments_needed $ At (Just ast) 1
 135                          [ast_x] ->
 136                                 term_from ast_x ctx $ \ty_x (TermLC x) ->
 137                                 check_constraint (At (Just ast_x) (tyOrd :$ ty_x)) $ \Con ->
 138                                 k (ty_x ~> ty_res) $ TermLC $
 139                                  \c -> lam $ op (x c)
 140                          [ast_x, ast_y] ->
 141                                 term_from ast_x ctx $ \ty_x (TermLC x) ->
 142                                 term_from ast_y ctx $ \ty_y (TermLC y) ->
 143                                 check_type (At (Just ast_x) ty_x) (At (Just ast_y) ty_y) $ \Refl ->
 144                                 check_constraint (At (Just ast_x) (tyOrd :$ ty_x)) $ \Con ->
 145                                 k ty_res $ TermLC $
 146                                  \c -> x c `op` y c
 147                          _ -> Left $ Error_Term_Syntax $
 148                                 Error_Syntax_too_many_arguments $ At (Just ast) 2
 149                 op2_from
 150                  :: (forall term a. (Sym_Ord term, Ord a) => term a -> term a -> term a)
 151                  -> LamCtx_Type is (Lexem ast) ctx
 152                  -> ( forall h. Type (Consts_of_Ifaces is) (h::Kind.Type)
 153                              -> TermLC ctx h is ls (Proxy Ord ': rs)
 154                              -> Either (Error_Term is ast) ret )
 155                  -> Either (Error_Term is ast) ret
 156                 op2_from op ctx k =
 157                         case ast_nodes ast of
 158                          [] -> Left $ Error_Term_Syntax $
 159                                 Error_Syntax_more_arguments_needed $ At (Just ast) 1
 160                          [ast_x] ->
 161                                 term_from ast_x ctx $ \ty_x (TermLC x) ->
 162                                 check_constraint (At (Just ast_x) (tyOrd :$ ty_x)) $ \Con ->
 163                                 k (ty_x ~> ty_x) $ TermLC $
 164                                  \c -> lam $ op (x c)
 165                          [ast_x, ast_y] ->
 166                                 term_from ast_x ctx $ \ty_x (TermLC x) ->
 167                                 term_from ast_y ctx $ \ty_y (TermLC y) ->
 168                                 check_type (At (Just ast_x) ty_x) (At (Just ast_y) ty_y) $ \Refl ->
 169                                 check_constraint (At (Just ast_x) (tyOrd :$ ty_x)) $ \Con ->
 170                                 k ty_x $ TermLC $
 171                                  \c -> x c `op` y c
 172                          _ -> Left $ Error_Term_Syntax $
 173                                 Error_Syntax_too_many_arguments $ At (Just ast) 2
 174
 175 -- | The 'Ord' 'Type'
 176 tyOrd :: Inj_Const cs Ord => Type cs Ord
 177 tyOrd = TyConst inj_const
 178
 179 -- | The 'Ordering' 'Type'
 180 tyOrdering :: Inj_Const cs Ordering => Type cs Ordering
 181 tyOrdering = TyConst inj_const
 182
 183 sym_Ord :: Proxy Sym_Ord
 184 sym_Ord = Proxy
 185
 186 syOrd :: IsString a => [Syntax a] -> Syntax a
 187 syOrd = Syntax "Ord"