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's.
  12 module Language.LOL.Symantic.Expr.Int where
  13
  14 import Data.Proxy (Proxy(..))
  15
  16 import Language.LOL.Symantic.AST
  17 import Language.LOL.Symantic.Type
  18 import Language.LOL.Symantic.Expr.Common
  19 import Language.LOL.Symantic.Expr.Lambda
  20 import Language.LOL.Symantic.Repr.Dup
  21 import Language.LOL.Symantic.Trans.Common
  22
  23 -- * Class 'Sym_Int'
  24
  25 -- | Symantic.
  26 class Sym_Int repr where
  27         int ::      Int -> repr Int
  28         neg :: repr Int -> repr Int
  29         add :: repr Int -> repr Int -> repr Int
  30
  31         default int :: Trans t repr =>        Int -> t repr Int
  32         default neg :: Trans t repr => t repr Int -> t repr Int
  33         default add :: Trans t repr => t repr Int -> t repr Int -> t repr Int
  34         int = trans_lift . int
  35         neg = trans_map1 neg
  36         add = trans_map2 add
  37
  38 instance -- Sym_Int Dup
  39  ( Sym_Int r1
  40  , Sym_Int r2
  41  ) => Sym_Int (Dup r1 r2) where
  42         int x = int x `Dup` int x
  43         neg (x1 `Dup` x2) = neg x1 `Dup` neg x2
  44         add (x1 `Dup` x2) (y1 `Dup` y2) = add x1 y1 `Dup` add x2 y2
  45
  46 -- * Type 'Expr_Int'
  47 -- | Expression.
  48 data Expr_Int (root:: *)
  49 type instance Root_of_Expr (Expr_Int root) = root
  50 type instance Type_of_Expr (Expr_Int root) = Type_Int
  51 type instance Sym_of_Expr (Expr_Int root) repr = Sym_Int repr
  52 type instance Error_of_Expr ast (Expr_Int root) = Error_Expr_Int ast
  53
  54 instance -- Expr_from AST Expr_Int
  55  ( Type_from AST (Type_Root_of_Expr root)
  56  , Expr_from AST root
  57
  58  , Type_Root_Lift Type_Int (Type_Root_of_Expr root)
  59  , Error_Type_Lift (Error_Type_Fun AST)
  60                    (Error_of_Type AST (Type_Root_of_Expr root))
  61  , Error_Expr_Lift (Error_Expr_Lambda (Error_of_Type AST (Type_Root_of_Expr root))
  62                                       (                   Type_Root_of_Expr root)
  63                                       AST)
  64                    (Error_of_Expr AST root)
  65  , Error_Expr_Lift (Error_Expr AST) (Error_of_Expr AST root)
  66
  67  , Type_Unlift Type_Int (Type_of_Expr root)
  68
  69  , Root_of_Expr root ~ root
  70  -- , Root_of_Type (Type_Root_of_Expr root) ~ Type_Root_of_Expr root
  71
  72  , Implicit_HBool (Is_Last_Expr (Expr_Int root) root)
  73  ) => Expr_from AST (Expr_Int root) where
  74         expr_from _px_ex ctx ast k =
  75                 case ast of
  76                  AST "int" asts ->
  77                         case asts of
  78                          [AST ast_int []] ->
  79                                 case read_safe ast_int of
  80                                  Left err -> Left $ error_expr_lift $ Error_Expr_Read err ast
  81                                  Right (i::Int) ->
  82                                         k type_int $ Forall_Repr_with_Context $
  83                                                 const $ int i
  84                          _ -> Left $ error_lambda_lift $
  85                                 Error_Expr_Fun_Wrong_number_of_arguments 3 ast
  86                  AST "neg" asts -> unary_from  asts neg
  87                  AST "add" asts -> binary_from asts add
  88                  -- _ -> Left $ error_expr_lift $ Error_Expr_Unsupported_here ast
  89                  _ -> Left $
  90                         case hbool :: HBool (Is_Last_Expr (Expr_Int root) root) of
  91                          HTrue  -> error_expr_lift $ Error_Expr_Unsupported ast
  92                          HFalse -> error_expr_lift $ Error_Expr_Unsupported_here ast
  93                 where
  94                 unary_from asts
  95                  (op::forall repr. Sym_Int repr
  96                     => repr Int -> repr Int) =
  97                         case asts of
  98                          [ast_x] ->
  99                                 expr_from (Proxy::Proxy root) ctx ast_x $
 100                                  \(ty_x::Type_Root_of_Expr root h_x) (Forall_Repr_with_Context x) ->
 101                                         case type_unlift $ unType_Root ty_x of
 102                                          Just (Type_Int::Type_Int (Type_Root_of_Expr root) h_x) ->
 103                                                 k ty_x $ Forall_Repr_with_Context (op . x)
 104                                          _ -> Left $ error_lambda_lift $
 105                                                 Error_Expr_Fun_Argument_mismatch
 106                                                  (Exists_Type type_int)
 107                                                  (Exists_Type ty_x) ast
 108                          _ -> Left $ error_lambda_lift $
 109                                 Error_Expr_Fun_Wrong_number_of_arguments 1 ast
 110                 binary_from asts
 111                  (op::forall repr. Sym_Int repr
 112                     => repr Int -> repr Int -> repr Int) =
 113                         case asts of
 114                          [ast_x, ast_y] ->
 115                                 expr_from (Proxy::Proxy root) ctx ast_x $
 116                                  \(ty_x::Type_Root_of_Expr root h_x) (Forall_Repr_with_Context x) ->
 117                                 expr_from (Proxy::Proxy root) ctx ast_y $
 118                                  \(ty_y::Type_Root_of_Expr root h_y) (Forall_Repr_with_Context y) ->
 119                                         case type_unlift $ unType_Root ty_x of
 120                                          Just (Type_Int::Type_Int (Type_Root_of_Expr root) h_x) ->
 121                                                 case type_unlift $ unType_Root ty_y of
 122                                                  Just (Type_Int::Type_Int (Type_Root_of_Expr root) h_y) ->
 123                                                         k ty_x $ Forall_Repr_with_Context $
 124                                                          \c -> x c `op` y c
 125                                                  Nothing -> Left $ error_lambda_lift $
 126                                                         Error_Expr_Fun_Argument_mismatch
 127                                                          (Exists_Type type_int)
 128                                                          (Exists_Type ty_y) ast
 129                                          Nothing -> Left $ error_lambda_lift $
 130                                                 Error_Expr_Fun_Argument_mismatch
 131                                                  (Exists_Type type_int)
 132                                                  (Exists_Type ty_x) ast
 133                          _ -> Left $ error_lambda_lift $
 134                                 Error_Expr_Fun_Wrong_number_of_arguments 2 ast
 135                 error_lambda_lift
 136                  :: Error_Expr_Lambda (Error_of_Type AST (Type_Root_of_Expr root)) (Type_Root_of_Expr root) AST
 137                  -> Error_of_Expr AST root
 138                 error_lambda_lift = error_expr_lift
 139
 140 -- ** Type 'Expr_Lambda_Int'
 141 -- | Convenient alias.
 142 type Expr_Lambda_Int lam = Expr_Root (Expr_Alt (Expr_Lambda lam) Expr_Int)
 143
 144 expr_lambda_int_from
 145  :: forall lam ast.
 146  Expr_from ast (Expr_Lambda_Int lam)
 147  => Proxy lam
 148  -> ast
 149  -> Either (Error_of_Expr ast (Expr_Lambda_Int lam))
 150            (Exists_Type_and_Repr (Type_Root_of_Expr (Expr_Lambda_Int lam))
 151                                  (Forall_Repr (Expr_Lambda_Int lam)))
 152 expr_lambda_int_from _px_lam ast =
 153         expr_from
 154          (Proxy::Proxy (Expr_Lambda_Int lam))
 155          Context_Empty ast $ \ty (Forall_Repr_with_Context repr) ->
 156                 Right $ Exists_Type_and_Repr ty $
 157                         Forall_Repr $ repr Context_Empty
 158
 159 -- * Type 'Error_Expr_Int'
 160 data Error_Expr_Int ast
 161  =   Error_Expr_Int
 162  deriving (Eq, Show)
 163