Language/LOL/Symantic/Expr/Int.hs

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