Language/Symantic/Compiling/Ord.hs

   1 {-# LANGUAGE DataKinds #-}
   2 {-# LANGUAGE DefaultSignatures #-}
   3 {-# LANGUAGE FlexibleContexts #-}
   4 {-# LANGUAGE FlexibleInstances #-}
   5 {-# LANGUAGE InstanceSigs #-}
   6 {-# LANGUAGE MultiParamTypeClasses #-}
   7 {-# LANGUAGE OverloadedStrings #-}
   8 {-# LANGUAGE Rank2Types #-}
   9 {-# LANGUAGE ScopedTypeVariables #-}
  10 {-# LANGUAGE TypeFamilies #-}
  11 {-# LANGUAGE TypeOperators #-}
  12 {-# LANGUAGE UndecidableInstances #-}
  13 {-# OPTIONS_GHC -fno-warn-orphans #-}
  14 -- | Symantic for 'Ord'.
  15 module Language.Symantic.Compiling.Ord where
  16
  17 import Control.Monad
  18 import Data.Ord (Ord)
  19 import qualified Data.Ord as Ord
  20 import Data.Proxy (Proxy(..))
  21 import Data.String (IsString)
  22 import Data.Text (Text)
  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 :: forall ctx ls rs ret. Term_fromIT ast ctx ret is ls (Proxy Ord ': rs)
 113         term_fromI ast ctx k =
 114                 case ast_lexem ast of
 115                  "compare" -> test2_from compare tyOrdering
 116                  "<="      -> test2_from (<=)    tyBool
 117                  "<"       -> test2_from (<)     tyBool
 118                  ">="      -> test2_from (>=)    tyBool
 119                  ">"       -> test2_from (>)     tyBool
 120                  "min"     -> op2_from min
 121                  "max"     -> op2_from max
 122                  _ -> Left $ Error_Term_unsupported
 123                 where
 124                 test2_from
 125                  :: (forall term a. (Sym_Ord term, Ord a) => term a -> term a -> term res)
 126                  -> Type (Consts_of_Ifaces is) (res::Kind.Type)
 127                  -> Either (Error_Term is ast) ret
 128                 test2_from op ty_res =
 129                         from_ast1 ast $ \ast_x as ->
 130                         term_from ast_x ctx $ \ty_x (TermLC x) ->
 131                         check_constraint (At (Just ast_x) (tyOrd :$ ty_x)) $ \Con ->
 132                         k as (ty_x ~> ty_res) $ TermLC $
 133                          \c -> lam $ op (x c)
 134                 op2_from
 135                  :: (forall term a. (Sym_Ord term, Ord a) => term a -> term a -> term a)
 136                  -> Either (Error_Term is ast) ret
 137                 op2_from op =
 138                         from_ast1 ast $ \ast_x as ->
 139                         term_from ast_x ctx $ \ty_x (TermLC x) ->
 140                         check_constraint (At (Just ast_x) (tyOrd :$ ty_x)) $ \Con ->
 141                         k as (ty_x ~> ty_x) $ TermLC $
 142                          \c -> lam $ op (x c)
 143
 144 -- | The 'Ord' 'Type'
 145 tyOrd :: Inj_Const cs Ord => Type cs Ord
 146 tyOrd = TyConst inj_const
 147
 148 -- | The 'Ordering' 'Type'
 149 tyOrdering :: Inj_Const cs Ordering => Type cs Ordering
 150 tyOrdering = TyConst inj_const
 151
 152 sym_Ord :: Proxy Sym_Ord
 153 sym_Ord = Proxy
 154
 155 syOrd :: IsString a => [Syntax a] -> Syntax a
 156 syOrd = Syntax "Ord"