Language/Symantic/Compiling/Eq.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 'Eq'.
  14 module Language.Symantic.Compiling.Eq where
  15
  16 import Control.Monad
  17 import qualified Data.Eq as Eq
  18 import Data.Proxy (Proxy(..))
  19 import Data.String (IsString)
  20 import Data.Text (Text)
  21 import Data.Type.Equality ((:~:)(Refl))
  22 import Prelude hiding ((==), (/=))
  23
  24 import Language.Symantic.Typing
  25 import Language.Symantic.Compiling.Term
  26 import Language.Symantic.Compiling.Bool
  27 import Language.Symantic.Interpreting
  28 import Language.Symantic.Transforming.Trans
  29
  30 -- * Class 'Sym_Eq'
  31 class Sym_Eq term where
  32         (==) :: Eq a => term a -> term a -> term Bool
  33         (/=) :: Eq a => term a -> term a -> term Bool
  34
  35         default (==) :: (Trans t term, Eq a) => t term a -> t term a -> t term Bool
  36         default (/=) :: (Trans t term, Eq a) => t term a -> t term a -> t term Bool
  37
  38         (==) = trans_map2 (==)
  39         (/=) = trans_map2 (/=)
  40
  41 infix 4 ==
  42 infix 4 /=
  43
  44 type instance Sym_of_Iface (Proxy Eq) = Sym_Eq
  45 type instance Consts_of_Iface (Proxy Eq) = Proxy Eq ': Consts_imported_by Eq
  46 type instance Consts_imported_by Eq = '[]
  47
  48 instance Sym_Eq HostI where
  49         (==) = liftM2 (Eq.==)
  50         (/=) = liftM2 (Eq./=)
  51 instance Sym_Eq TextI where
  52         (==) = textI_infix "==" (Precedence 4)
  53         (/=) = textI_infix "/=" (Precedence 4)
  54 instance (Sym_Eq r1, Sym_Eq r2) => Sym_Eq (DupI r1 r2) where
  55         (==) = dupI2 sym_Eq (==)
  56         (/=) = dupI2 sym_Eq (/=)
  57
  58 instance Const_from Text cs => Const_from Text (Proxy Eq ': cs) where
  59         const_from "Eq" k = k (ConstZ kind)
  60         const_from s k = const_from s $ k . ConstS
  61 instance Show_Const cs => Show_Const (Proxy Eq ': cs) where
  62         show_const ConstZ{} = "Eq"
  63         show_const (ConstS c) = show_const c
  64
  65 instance -- Proj_ConC
  66  Proj_ConC cs (Proxy Eq)
  67 instance -- Term_fromI
  68  ( AST ast
  69  , Lexem ast ~ LamVarName
  70  , Inj_Const (Consts_of_Ifaces is) Bool
  71  , Inj_Const (Consts_of_Ifaces is) (->)
  72  , Inj_Const (Consts_of_Ifaces is) Eq
  73  , Proj_Con (Consts_of_Ifaces is)
  74  , Term_from is ast
  75  ) => Term_fromI is (Proxy Eq) ast where
  76         term_fromI ast ctx k =
  77                 case ast_lexem ast of
  78                  "=="  -> op2_from (==)
  79                  "/="  -> op2_from (/=)
  80                  _ -> Left $ Error_Term_unsupported
  81                 where
  82                 op2_from (op::forall term a. (Sym_Eq term, Eq a) => term a -> term a -> term Bool) =
  83                         case ast_nodes ast of
  84                          [] -> Left $ Error_Term_Syntax $
  85                                 Error_Syntax_more_arguments_needed $ At (Just ast) 1
  86                          [ast_x] ->
  87                                 term_from ast_x ctx $ \ty_x (TermLC x) ->
  88                                 check_constraint (At (Just ast_x) (tyEq :$ ty_x)) $ \Con ->
  89                                 k (ty_x ~> tyBool) $ TermLC $
  90                                  \c -> lam $ op (x c)
  91                          [ast_x, ast_y] ->
  92                                 term_from ast_x ctx $ \ty_x (TermLC x) ->
  93                                 check_constraint (At (Just ast_x) (tyEq :$ ty_x)) $ \Con ->
  94                                 term_from ast_y ctx $ \ty_y (TermLC y) ->
  95                                 check_type (At (Just ast_x) ty_x) (At (Just ast_y) ty_y) $ \Refl ->
  96                                 k tyBool $ TermLC $
  97                                  \c -> op (x c) (y c)
  98                          _ -> Left $ Error_Term_Syntax $
  99                                 Error_Syntax_too_many_arguments $ At (Just ast) 2
 100
 101 -- | The 'Eq' 'Type'
 102 tyEq :: Inj_Const cs Eq => Type cs Eq
 103 tyEq = TyConst inj_const
 104
 105 sym_Eq :: Proxy Sym_Eq
 106 sym_Eq = Proxy
 107
 108 syEq :: IsString a => [Syntax a] -> Syntax a
 109 syEq = Syntax "Eq"