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.Type.Equality ((:~:)(Refl))
  21 import Prelude hiding (Ord(..))
  22
  23 import Language.Symantic.Typing
  24 import Language.Symantic.Compiling.Term
  25 import Language.Symantic.Compiling.Eq
  26 import Language.Symantic.Interpreting
  27 import Language.Symantic.Transforming.Trans
  28
  29 -- * Class 'Sym_Ord'
  30 -- | Symantic.
  31 class Sym_Eq term => Sym_Ord term where
  32         compare :: Ord a => term a -> term a -> term Ordering
  33         (<)     :: Ord a => term a -> term a -> term Bool
  34         (<=)    :: Ord a => term a -> term a -> term Bool
  35         (>)     :: Ord a => term a -> term a -> term Bool
  36         (>=)    :: Ord a => term a -> term a -> term Bool
  37         max     :: Ord a => term a -> term a -> term a
  38         min     :: Ord a => term a -> term a -> term a
  39
  40         default compare :: (Trans t term, Ord a) => t term a -> t term a -> t term Ordering
  41         default (<)     :: (Trans t term, Ord a) => t term a -> t term a -> t term Bool
  42         default (<=)    :: (Trans t term, Ord a) => t term a -> t term a -> t term Bool
  43         default (>)     :: (Trans t term, Ord a) => t term a -> t term a -> t term Bool
  44         default (>=)    :: (Trans t term, Ord a) => t term a -> t term a -> t term Bool
  45         default max     :: (Trans t term, Ord a) => t term a -> t term a -> t term a
  46         default min     :: (Trans t term, Ord a) => t term a -> t term a -> t term 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 type instance Sym_of_Iface (Proxy Ord) = Sym_Ord
  62
  63 instance Sym_Ord HostI where
  64         compare = liftM2 Ord.compare
  65         (<)     = liftM2 (Ord.<)
  66         (<=)    = liftM2 (Ord.<=)
  67         (>)     = liftM2 (Ord.>)
  68         (>=)    = liftM2 (Ord.>=)
  69         min     = liftM2 Ord.min
  70         max     = liftM2 Ord.max
  71 instance Sym_Ord TextI where
  72         compare = textI_app2  "compare"
  73         (<)     = textI_infix "<"  (Precedence 4)
  74         (<=)    = textI_infix "<=" (Precedence 4)
  75         (>)     = textI_infix ">"  (Precedence 4)
  76         (>=)    = textI_infix ">=" (Precedence 4)
  77         min     = textI_app2  "min"
  78         max     = textI_app2  "max"
  79 instance (Sym_Ord r1, Sym_Ord r2) => Sym_Ord (DupI r1 r2) where
  80         compare = dupI2 sym_Ord compare
  81         (<)     = dupI2 sym_Ord (<)
  82         (<=)    = dupI2 sym_Ord (<=)
  83         (>)     = dupI2 sym_Ord (>)
  84         (>=)    = dupI2 sym_Ord (>=)
  85         min     = dupI2 sym_Ord min
  86         max     = dupI2 sym_Ord max
  87
  88 sym_Ord :: Proxy Sym_Ord
  89 sym_Ord = Proxy
  90
  91 instance -- Term_fromI
  92  ( AST ast
  93  , Lexem ast ~ LamVarName
  94  , Inj_Const (Consts_of_Ifaces is) Bool
  95  , Inj_Const (Consts_of_Ifaces is) (->)
  96  , Inj_Const (Consts_of_Ifaces is) Ord
  97  , Inj_Const (Consts_of_Ifaces is) Ordering
  98  , Proj_Con (Consts_of_Ifaces is)
  99  , Term_from is ast
 100  ) => Term_fromI is (Proxy Ord) ast where
 101         term_fromI ast =
 102                 case ast_lexem ast of
 103                  "compare" -> test2_from compare tyOrdering
 104                  "<="      -> test2_from (<=)    tyBool
 105                  "<"       -> test2_from (<)     tyBool
 106                  ">="      -> test2_from (>=)    tyBool
 107                  ">"       -> test2_from (>)     tyBool
 108                  "min"     -> op2_from min
 109                  "max"     -> op2_from max
 110                  _ -> \_ctx _k -> Left $ Error_Term_unsupported
 111                 where
 112                 test2_from
 113                  :: (forall term a. (Sym_Ord term, Ord a) => term a -> term a -> term (UnProxy res))
 114                  -> Type (Consts_of_Ifaces is) 'KiTerm res
 115                  -> LamCtx_Type is (Lexem ast) ctx
 116                  -> ( forall h. Type (Consts_of_Ifaces is) 'KiTerm h
 117                              -> Term_of_LamCtx ctx h is ls (Proxy Ord ': rs)
 118                              -> Either (Error_Term is ast) ret )
 119                  -> Either (Error_Term is ast) ret
 120                 test2_from op ty_res ctx k =
 121                         case ast_nodes ast of
 122                          [] -> Left $ Error_Term_Syntax $
 123                                 Error_Syntax_more_arguments_needed $ At (Just ast) 1
 124                          [ast_x] ->
 125                                 term_from ast_x ctx $ \ty_x (Term_of_LamCtx x) ->
 126                                 check_constraint (At (Just ast_x) (tyOrd :$ ty_x)) $ \Con ->
 127                                 k (ty_x ~> ty_res) $ Term_of_LamCtx $
 128                                  \c -> lam $ op (x c)
 129                          [ast_x, ast_y] ->
 130                                 term_from ast_x ctx $ \ty_x (Term_of_LamCtx x) ->
 131                                 term_from ast_y ctx $ \ty_y (Term_of_LamCtx y) ->
 132                                 check_type (At (Just ast_x) ty_x) (At (Just ast_y) ty_y) $ \Refl ->
 133                                 check_constraint (At (Just ast_x) (tyOrd :$ ty_x)) $ \Con ->
 134                                 k ty_res $ Term_of_LamCtx $
 135                                  \c -> x c `op` y c
 136                          _ -> Left $ Error_Term_Syntax $
 137                                 Error_Syntax_too_many_arguments $ At (Just ast) 2
 138                 op2_from
 139                  :: (forall term a. (Sym_Ord term, Ord a) => term a -> term a -> term a)
 140                  -> LamCtx_Type is (Lexem ast) ctx
 141                  -> ( forall h. Type (Consts_of_Ifaces is) 'KiTerm h
 142                              -> Term_of_LamCtx ctx h is ls (Proxy Ord ': rs)
 143                              -> Either (Error_Term is ast) ret )
 144                  -> Either (Error_Term is ast) ret
 145                 op2_from op ctx k =
 146                         case ast_nodes ast of
 147                          [] -> Left $ Error_Term_Syntax $
 148                                 Error_Syntax_more_arguments_needed $ At (Just ast) 1
 149                          [ast_x] ->
 150                                 term_from ast_x ctx $ \ty_x (Term_of_LamCtx x) ->
 151                                 check_constraint (At (Just ast_x) (tyOrd :$ ty_x)) $ \Con ->
 152                                 k (ty_x ~> ty_x) $ Term_of_LamCtx $
 153                                  \c -> lam $ op (x c)
 154                          [ast_x, ast_y] ->
 155                                 term_from ast_x ctx $ \ty_x (Term_of_LamCtx x) ->
 156                                 term_from ast_y ctx $ \ty_y (Term_of_LamCtx y) ->
 157                                 check_type (At (Just ast_x) ty_x) (At (Just ast_y) ty_y) $ \Refl ->
 158                                 check_constraint (At (Just ast_x) (tyOrd :$ ty_x)) $ \Con ->
 159                                 k ty_x $ Term_of_LamCtx $
 160                                  \c -> x c `op` y c
 161                          _ -> Left $ Error_Term_Syntax $
 162                                 Error_Syntax_too_many_arguments $ At (Just ast) 2