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_Type_Lift (Error_Type_Fun AST)
  61                    (Error_of_Type AST (Type_Root_of_Expr root))
  62  , Error_Expr_Lift (Error_Expr (Error_of_Type AST (Type_Root_of_Expr root))
  63                                (                   Type_Root_of_Expr root)
  64                                AST)
  65                    (Error_of_Expr AST root)
  66
  67  , Type_Unlift Type_Int (Type_of_Expr root)
  68
  69  , Root_of_Expr root ~ root
  70
  71  , Implicit_HBool (Is_Last_Expr (Expr_Int root) root)
  72  ) => Expr_from AST (Expr_Int root) where
  73         expr_from px_ex ctx ast k =
  74                 case ast of
  75                  AST "int" asts ->
  76                         case asts of
  77                          [AST ast_int []] ->
  78                                 case read_safe ast_int of
  79                                  Left err -> Left $ error_expr px_ex $ Error_Expr_Read err ast
  80                                  Right (i::Int) ->
  81                                         k type_int $ Forall_Repr_with_Context $
  82                                                 const $ int i
  83                          _ -> Left $ error_expr px_ex $
  84                                 Error_Expr_Wrong_number_of_arguments 3 ast
  85                  AST "neg" asts -> unary_from  asts neg
  86                  AST "add" asts -> binary_from asts add
  87                  _ -> Left $
  88                         case hbool :: HBool (Is_Last_Expr (Expr_Int root) root) of
  89                          HTrue  -> error_expr px_ex $ Error_Expr_Unsupported ast
  90                          HFalse -> error_expr px_ex $ Error_Expr_Unsupported_here ast
  91                 where
  92                 unary_from asts
  93                  (op::forall repr. Sym_Int repr
  94                     => repr Int -> repr Int) =
  95                         case asts of
  96                          [ast_x] ->
  97                                 expr_from (Proxy::Proxy root) ctx ast_x $ \ty_x (Forall_Repr_with_Context x) ->
  98                                 when_type_eq px_ex ast type_int ty_x $ \Refl ->
  99                                         k ty_x $ Forall_Repr_with_Context (op . x)
 100                          _ -> Left $ error_expr px_ex $
 101                                 Error_Expr_Wrong_number_of_arguments 1 ast
 102                 binary_from asts
 103                  (op::forall repr. Sym_Int repr
 104                     => repr Int -> repr Int -> repr Int) =
 105                         case asts of
 106                          [ast_x, ast_y] ->
 107                                 expr_from (Proxy::Proxy root) ctx ast_x $ \ty_x (Forall_Repr_with_Context x) ->
 108                                 expr_from (Proxy::Proxy root) ctx ast_y $ \ty_y (Forall_Repr_with_Context y) ->
 109                                 when_type_eq px_ex ast type_int ty_x $ \Refl ->
 110                                 when_type_eq px_ex ast type_int ty_y $ \Refl ->
 111                                         k ty_x $ Forall_Repr_with_Context $
 112                                          \c -> x c `op` y c
 113                          _ -> Left $ error_expr px_ex $
 114                                 Error_Expr_Wrong_number_of_arguments 2 ast
 115
 116 -- ** Type 'Expr_Lambda_Int'
 117 -- | Convenient alias.
 118 type Expr_Lambda_Int lam = Expr_Root (Expr_Alt (Expr_Lambda lam) Expr_Int)
 119
 120 -- | Convenient alias around 'expr_from'.
 121 expr_lambda_int_from
 122  :: forall lam ast.
 123  Expr_from ast (Expr_Lambda_Int lam)
 124  => Proxy lam
 125  -> ast
 126  -> Either (Error_of_Expr ast (Expr_Lambda_Int lam))
 127            (Exists_Type_and_Repr (Type_Root_of_Expr (Expr_Lambda_Int lam))
 128                                  (Forall_Repr (Expr_Lambda_Int lam)))
 129 expr_lambda_int_from _px_lam ast =
 130         expr_from
 131          (Proxy::Proxy (Expr_Lambda_Int lam))
 132          Context_Empty ast $ \ty (Forall_Repr_with_Context repr) ->
 133                 Right $ Exists_Type_and_Repr ty $
 134                         Forall_Repr $ repr Context_Empty