Language/Symantic/Compiling/Eq.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 {-# LANGUAGE UndecidableInstances #-}
  11 {-# OPTIONS_GHC -fno-warn-orphans #-}
  12 -- | Symantic for 'Eq'.
  13 module Language.Symantic.Compiling.Eq where
  14
  15 import Control.Monad
  16 import qualified Data.Eq as Eq
  17 import Data.Proxy (Proxy(..))
  18 import Data.Type.Equality ((:~:)(Refl))
  19 import Prelude hiding ((==), (/=))
  20
  21 import Language.Symantic.Typing
  22 import Language.Symantic.Compiling.Term
  23 import Language.Symantic.Interpreting
  24 import Language.Symantic.Transforming.Trans
  25
  26 -- * Class 'Sym_Eq'
  27 -- | Symantic.
  28 class Sym_Eq term where
  29         (==) :: Eq a => term a -> term a -> term Bool
  30         (/=) :: Eq a => term a -> term a -> term Bool
  31
  32         default (==) :: (Trans t term, Eq a) => t term a -> t term a -> t term Bool
  33         default (/=) :: (Trans t term, Eq a) => t term a -> t term a -> t term Bool
  34
  35         (==) = trans_map2 (==)
  36         (/=) = trans_map2 (/=)
  37
  38 infix 4 ==
  39 infix 4 /=
  40
  41 type instance Sym_of_Iface (Proxy Eq) = Sym_Eq
  42
  43 instance Sym_Eq HostI where
  44         (==) = liftM2 (Eq.==)
  45         (/=) = liftM2 (Eq./=)
  46 instance Sym_Eq TextI where
  47         (==) = textI_infix "==" (Precedence 4)
  48         (/=) = textI_infix "/=" (Precedence 4)
  49 instance (Sym_Eq r1, Sym_Eq r2) => Sym_Eq (DupI r1 r2) where
  50         (==) = dupI2 sym_Eq (==)
  51         (/=) = dupI2 sym_Eq (/=)
  52
  53 sym_Eq :: Proxy Sym_Eq
  54 sym_Eq = Proxy
  55
  56 instance -- Term_fromI
  57  ( AST ast
  58  , Lexem ast ~ LamVarName
  59  , Inj_Const (Consts_of_Ifaces is) Bool
  60  , Inj_Const (Consts_of_Ifaces is) (->)
  61  , Inj_Const (Consts_of_Ifaces is) Eq
  62  , Proj_Con (Consts_of_Ifaces is)
  63  , Term_from is ast
  64  ) => Term_fromI is (Proxy Eq) ast where
  65         term_fromI ast ctx k =
  66                 case ast_lexem ast of
  67                  "=="  -> op2_from (==)
  68                  "/="  -> op2_from (/=)
  69                  _ -> Left $ Error_Term_unsupported
  70                 where
  71                 op2_from (op::forall term a. (Sym_Eq term, Eq a) => term a -> term a -> term Bool) =
  72                         case ast_nodes ast of
  73                          [] -> Left $ Error_Term_Syntax $
  74                                 Error_Syntax_more_arguments_needed $ At (Just ast) 1
  75                          [ast_x] ->
  76                                 term_from ast_x ctx $ \ty_x (Term_of_LamCtx x) ->
  77                                 check_constraint (At (Just ast_x) (tyEq :$ ty_x)) $ \Con ->
  78                                 k (ty_x ~> tyBool) $ Term_of_LamCtx $
  79                                  \c -> lam $ op (x c)
  80                          [ast_x, ast_y] ->
  81                                 term_from ast_x ctx $ \ty_x (Term_of_LamCtx x) ->
  82                                 check_constraint (At (Just ast_x) (tyEq :$ ty_x)) $ \Con ->
  83                                 term_from ast_y ctx $ \ty_y (Term_of_LamCtx y) ->
  84                                 check_type (At (Just ast_x) ty_x) (At (Just ast_y) ty_y) $ \Refl ->
  85                                 k tyBool $ Term_of_LamCtx $
  86                                  \c -> op (x c) (y c)
  87                          _ -> Left $ Error_Term_Syntax $
  88                                 Error_Syntax_too_many_arguments $ At (Just ast) 2
  89