TFHOE/Expr/Int.hs

   1 {-# LANGUAGE FlexibleContexts #-}
   2 {-# LANGUAGE FlexibleInstances #-}
   3 {-# LANGUAGE GADTs #-}
   4 {-# LANGUAGE MultiParamTypeClasses #-}
   5 {-# LANGUAGE Rank2Types #-}
   6 {-# LANGUAGE ScopedTypeVariables #-}
   7 {-# LANGUAGE TypeFamilies #-}
   8 {-# OPTIONS_GHC -fno-warn-orphans #-}
   9 module TFHOE.Expr.Int where
  10
  11 import Data.Proxy (Proxy(..))
  12
  13 import TFHOE.Raw
  14 import TFHOE.Type
  15 import TFHOE.Expr.Common
  16 import TFHOE.Expr.Fun ()
  17 import TFHOE.Expr.Bool ()
  18 import TFHOE.Repr.Dup
  19
  20 -- * Class 'Expr_Int'
  21
  22 -- | Symantics combinable with 'Type_Int'.
  23 class Expr_Int repr where
  24         int :: Int -> repr Int
  25         add :: repr Int -> repr Int -> repr Int
  26
  27 type instance Expr_from_Type (Type_Int next) repr
  28  = ( Expr_Int repr
  29    , Expr_from_Type next repr )
  30
  31 instance -- Expr_Int Dup
  32  ( Expr_Int r1
  33  , Expr_Int r2
  34  ) => Expr_Int (Dup r1 r2) where
  35         int x = int x `Dup` int x
  36         add (x1 `Dup` x2) (y1 `Dup` y2) = add x1 y1 `Dup` add x2 y2
  37 instance -- Expr_from Raw
  38  ( Type_from Raw next
  39  , Expr_from Raw next (Type_Fun_Bool_Int fun next)
  40  ) => Expr_from Raw (Type_Int next)
  41                     (Type_Fun_Bool_Int fun next) where
  42         expr_from _px_ty _px_ty_end _ctx (Raw "int" [Raw raw_int []]) k = do
  43                 (i::Int) <- read_safe raw_int
  44                 k (Type_Fun_Next $ Type_Bool_Next Type_Int) $ Forall_Repr_with_Context $
  45                  \_c -> int i
  46         expr_from _px_ty px_ty_end ctx (Raw "add" [raw_x, raw_y]) k =
  47                 expr_from px_ty_end px_ty_end ctx raw_x $ \ty_x (Forall_Repr_with_Context x) ->
  48                 expr_from px_ty_end px_ty_end ctx raw_y $ \ty_y (Forall_Repr_with_Context y) ->
  49                         case (ty_x, ty_y) of
  50                          (  Type_Fun_Next (Type_Bool_Next Type_Int)
  51                           , Type_Fun_Next (Type_Bool_Next Type_Int) ) ->
  52                                 k ty_x $ Forall_Repr_with_Context $
  53                                  \c -> x c `add` y c
  54                          _ -> Left "Error: add: at least one operand is not an Int"
  55         expr_from _px_ty px_ty_end ctx raw k =
  56                 expr_from (Proxy::Proxy next) px_ty_end ctx raw k
  57 instance Expr_from Raw Type_End (Type_Fun_Bool_Int repr Type_End) where
  58         expr_from _px_ty _px_ty_end _ctx raw _k =
  59                 Left $ "Error: invalid Type_Fun_Bool_Int: " ++ show raw
  60
  61 expr_fun_bool_int_from
  62  :: forall fun raw next.
  63  ( Expr_from raw (Type_Fun_Bool_Int fun next)
  64                  (Type_Fun_Bool_Int fun next)
  65  )
  66  => Proxy fun
  67  -> Proxy next
  68  -> raw
  69  -> Either Error_Type
  70            (Exists_Type_and_Repr
  71             (Type_Fun_Bool_Int fun next)
  72             (Forall_Repr (Type_Fun_Bool_Int fun next)))
  73 expr_fun_bool_int_from _px_call _px_next raw =
  74         expr_from
  75          (Proxy::Proxy (Type_Fun_Bool_Int fun next))
  76          (Proxy::Proxy (Type_Fun_Bool_Int fun next))
  77          Context_Empty raw $ \ty (Forall_Repr_with_Context repr) ->
  78                 Right $ Exists_Type_and_Repr ty $
  79                         Forall_Repr $ repr Context_Empty