Language/Symantic/Expr/Int.hs

   1 {-# LANGUAGE DefaultSignatures #-}
   2 {-# LANGUAGE FlexibleContexts #-}
   3 {-# LANGUAGE ScopedTypeVariables #-}
   4 {-# LANGUAGE TypeFamilies #-}
   5 -- | Expression for 'Int'.
   6 module Language.Symantic.Expr.Int where
   7
   8 import Data.Proxy (Proxy(..))
   9
  10 import Language.Symantic.Type
  11 import Language.Symantic.Expr.Common
  12 import Language.Symantic.Expr.Lambda
  13 import Language.Symantic.Repr.Dup
  14 import Language.Symantic.Trans.Common
  15
  16 -- * Class 'Sym_Int'
  17 -- | Symantic.
  18 class Sym_Int repr where
  19         int ::      Int -> repr Int
  20         neg :: repr Int -> repr Int
  21         add :: repr Int -> repr Int -> repr Int
  22
  23         default int :: Trans t repr =>        Int -> t repr Int
  24         default neg :: Trans t repr => t repr Int -> t repr Int
  25         default add :: Trans t repr => t repr Int -> t repr Int -> t repr Int
  26         int = trans_lift . int
  27         neg = trans_map1 neg
  28         add = trans_map2 add
  29
  30 instance -- Sym_Int Dup
  31  ( Sym_Int r1
  32  , Sym_Int r2
  33  ) => Sym_Int (Dup r1 r2) where
  34         int x = int x `Dup` int x
  35         neg (x1 `Dup` x2) = neg x1 `Dup` neg x2
  36         add (x1 `Dup` x2) (y1 `Dup` y2) = add x1 y1 `Dup` add x2 y2
  37
  38 -- * Type 'Expr_Int'
  39 -- | Expression.
  40 data Expr_Int (root:: *)
  41 type instance Root_of_Expr      (Expr_Int root)      = root
  42 type instance Type_of_Expr      (Expr_Int root)      = Type_Int
  43 type instance Sym_of_Expr       (Expr_Int root) repr = Sym_Int repr
  44 type instance Error_of_Expr ast (Expr_Int root)      = No_Error_Expr
  45
  46 -- ** Type 'Expr_Lambda_Int'
  47 -- | Convenient alias.
  48 type Expr_Lambda_Int lam = Expr_Root (Expr_Alt (Expr_Lambda lam) Expr_Int)
  49
  50 -- | Convenient alias around 'expr_from'.
  51 expr_lambda_int_from
  52  :: forall lam ast.
  53  Expr_from ast (Expr_Lambda_Int lam)
  54  => Proxy lam
  55  -> ast
  56  -> Either (Error_of_Expr ast (Expr_Lambda_Int lam))
  57            (Exists_Type_and_Repr (Type_Root_of_Expr (Expr_Lambda_Int lam))
  58                                  (Forall_Repr (Expr_Lambda_Int lam)))
  59 expr_lambda_int_from _lam ast =
  60         expr_from (Proxy::Proxy (Expr_Lambda_Int lam)) ast
  61          Context_Empty $ \ty (Forall_Repr_with_Context repr) ->
  62                 Right $ Exists_Type_and_Repr ty $
  63                         Forall_Repr $ repr Context_Empty