Language/LOL/Symantic/Expr/Int.hs

   1 {-# LANGUAGE DefaultSignatures #-}
   2 {-# LANGUAGE FlexibleContexts #-}
   3 {-# LANGUAGE FlexibleInstances #-}
   4 {-# LANGUAGE GADTs #-}
   5 {-# LANGUAGE MultiParamTypeClasses #-}
   6 {-# LANGUAGE OverloadedStrings #-}
   7 {-# LANGUAGE Rank2Types #-}
   8 {-# LANGUAGE ScopedTypeVariables #-}
   9 {-# LANGUAGE TypeFamilies #-}
  10 {-# LANGUAGE UndecidableInstances #-}
  11 -- | Expression for 'Int'.
  12 module Language.LOL.Symantic.Expr.Int where
  13
  14 import Data.Proxy (Proxy(..))
  15 import Data.Type.Equality ((:~:)(Refl))
  16
  17 import Language.LOL.Symantic.AST
  18 import Language.LOL.Symantic.Type
  19 import Language.LOL.Symantic.Expr.Common
  20 import Language.LOL.Symantic.Expr.Lambda
  21 import Language.LOL.Symantic.Repr.Dup
  22 import Language.LOL.Symantic.Trans.Common
  23
  24 -- * Class 'Sym_Int'
  25
  26 -- | Symantic.
  27 class Sym_Int repr where
  28         int ::      Int -> repr Int
  29         neg :: repr Int -> repr Int
  30         add :: repr Int -> repr Int -> repr Int
  31
  32         default int :: Trans t repr =>        Int -> t repr Int
  33         default neg :: Trans t repr => t repr Int -> t repr Int
  34         default add :: Trans t repr => t repr Int -> t repr Int -> t repr Int
  35         int = trans_lift . int
  36         neg = trans_map1 neg
  37         add = trans_map2 add
  38
  39 instance -- Sym_Int Dup
  40  ( Sym_Int r1
  41  , Sym_Int r2
  42  ) => Sym_Int (Dup r1 r2) where
  43         int x = int x `Dup` int x
  44         neg (x1 `Dup` x2) = neg x1 `Dup` neg x2
  45         add (x1 `Dup` x2) (y1 `Dup` y2) = add x1 y1 `Dup` add x2 y2
  46
  47 -- * Type 'Expr_Int'
  48 -- | Expression.
  49 data Expr_Int (root:: *)
  50 type instance Root_of_Expr      (Expr_Int root)      = root
  51 type instance Type_of_Expr      (Expr_Int root)      = Type_Int
  52 type instance Sym_of_Expr       (Expr_Int root) repr = Sym_Int repr
  53 type instance Error_of_Expr ast (Expr_Int root)      = ()
  54
  55 instance -- Expr_from AST Expr_Int
  56  ( Type_from AST (Type_Root_of_Expr root)
  57  , Expr_from AST root
  58
  59  , Type_Root_Lift Type_Int (Type_Root_of_Expr root)
  60  , Error_Expr_Lift (Error_Expr (Error_of_Type AST (Type_Root_of_Expr root))
  61                                (                   Type_Root_of_Expr root)
  62                                AST)
  63                    (Error_of_Expr AST root)
  64
  65  , Type_Unlift Type_Int (Type_of_Expr root)
  66
  67  , Root_of_Expr root ~ root
  68
  69  , Implicit_HBool (Is_Last_Expr (Expr_Int root) root)
  70  ) => Expr_from AST (Expr_Int root) where
  71         expr_from px_ex ctx ast k =
  72                 case ast of
  73                  AST "int" asts ->
  74                         case asts of
  75                          [AST ast_int []] ->
  76                                 case read_safe ast_int of
  77                                  Left err -> Left $ error_expr px_ex $ Error_Expr_Read err ast
  78                                  Right (i::Int) ->
  79                                         k type_int $ Forall_Repr_with_Context $
  80                                                 const $ int i
  81                          _ -> Left $ error_expr px_ex $
  82                                 Error_Expr_Wrong_number_of_arguments ast 1
  83                  AST "neg" asts -> unary_from  asts neg
  84                  AST "add" asts -> binary_from asts add
  85                  _ -> Left $ error_expr_unsupported px_ex ast
  86                 where
  87                 unary_from asts
  88                  (op::forall repr. Sym_Int repr
  89                     => repr Int -> repr Int) =
  90                         case asts of
  91                          [ast_x] ->
  92                                 expr_from (Proxy::Proxy root) ctx ast_x $ \ty_x (Forall_Repr_with_Context x) ->
  93                                 when_type_eq px_ex ast type_int ty_x $ \Refl ->
  94                                         k ty_x $ Forall_Repr_with_Context (op . x)
  95                          _ -> Left $ error_expr px_ex $
  96                                 Error_Expr_Wrong_number_of_arguments ast 1
  97                 binary_from asts
  98                  (op::forall repr. Sym_Int repr
  99                     => repr Int -> repr Int -> repr Int) =
 100                         case asts of
 101                          [ast_x, ast_y] ->
 102                                 expr_from (Proxy::Proxy root) ctx ast_x $ \ty_x (Forall_Repr_with_Context x) ->
 103                                 expr_from (Proxy::Proxy root) ctx ast_y $ \ty_y (Forall_Repr_with_Context y) ->
 104                                 when_type_eq px_ex ast type_int ty_x $ \Refl ->
 105                                 when_type_eq px_ex ast type_int ty_y $ \Refl ->
 106                                         k ty_x $ Forall_Repr_with_Context $
 107                                          \c -> x c `op` y c
 108                          _ -> Left $ error_expr px_ex $
 109                                 Error_Expr_Wrong_number_of_arguments ast 2
 110
 111 -- ** Type 'Expr_Lambda_Int'
 112 -- | Convenient alias.
 113 type Expr_Lambda_Int lam = Expr_Root (Expr_Alt (Expr_Lambda lam) Expr_Int)
 114
 115 -- | Convenient alias around 'expr_from'.
 116 expr_lambda_int_from
 117  :: forall lam ast.
 118  Expr_from ast (Expr_Lambda_Int lam)
 119  => Proxy lam
 120  -> ast
 121  -> Either (Error_of_Expr ast (Expr_Lambda_Int lam))
 122            (Exists_Type_and_Repr (Type_Root_of_Expr (Expr_Lambda_Int lam))
 123                                  (Forall_Repr (Expr_Lambda_Int lam)))
 124 expr_lambda_int_from _px_lam ast =
 125         expr_from
 126          (Proxy::Proxy (Expr_Lambda_Int lam))
 127          Context_Empty ast $ \ty (Forall_Repr_with_Context repr) ->
 128                 Right $ Exists_Type_and_Repr ty $
 129                         Forall_Repr $ repr Context_Empty