Language/LOL/Symantic/Expr/Int.hs

   1 {-# LANGUAGE FlexibleContexts #-}
   2 {-# LANGUAGE FlexibleInstances #-}
   3 {-# LANGUAGE GADTs #-}
   4 {-# LANGUAGE MultiParamTypeClasses #-}
   5 {-# LANGUAGE OverloadedStrings #-}
   6 {-# LANGUAGE Rank2Types #-}
   7 {-# LANGUAGE ScopedTypeVariables #-}
   8 {-# LANGUAGE TypeFamilies #-}
   9 {-# LANGUAGE UndecidableInstances #-}
  10 {-# OPTIONS_GHC -fno-warn-orphans #-}
  11 module Language.LOL.Symantic.Expr.Int where
  12
  13 import Data.Proxy (Proxy(..))
  14
  15 import Language.LOL.Symantic.Raw
  16 import Language.LOL.Symantic.Type
  17 import Language.LOL.Symantic.Expr.Common
  18 import Language.LOL.Symantic.Expr.Lambda
  19 import Language.LOL.Symantic.Expr.Bool ()
  20 import Language.LOL.Symantic.Repr.Dup
  21
  22 -- * Class 'Sym_Int'
  23
  24 -- | Symantics acting on 'Int's.
  25 class Sym_Int repr where
  26         int :: Int -> repr Int
  27         neg :: repr Int -> repr Int
  28         add :: repr Int -> repr Int -> repr Int
  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
  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 raw (Expr_Int root) = Error_Expr_Int raw
  45
  46 instance -- Sym_from Raw Expr_Int
  47  ( Type_from Raw (Type_Root_of_Expr root)
  48  , Sym_from Raw root
  49
  50  , Type_Root_Lift Type_Int (Type_Root_of_Expr root)
  51  , Error_Type_Lift (Error_Type_Fun Raw)
  52                    (Error_of_Type Raw (Type_Root_of_Expr root))
  53  , Error_Expr_Lift (Error_Expr_Lambda (Error_of_Type Raw (Type_Root_of_Expr root))
  54                                      (Type_Root_of_Expr root)
  55                                      Raw)
  56                   (Error_of_Expr Raw root)
  57  , Error_Expr_Lift (Error_Expr_Read Raw)
  58                   (Error_of_Expr Raw root)
  59
  60  , Expr_Cons_Unlift (Type_Int (Type_Root_of_Expr root)) (Type_Root_of_Expr root)
  61
  62  , Root_of_Expr root ~ root
  63  -- , Root_of_Type (Type_Root_of_Expr root) ~ Type_Root_of_Expr root
  64  ) => Sym_from Raw (Expr_Int root) where
  65         sym_from _px_ex ctx raw k =
  66                 case raw of
  67                  Raw "int" raws ->
  68                         case raws of
  69                          [Raw raw_int []] ->
  70                                 case read_safe raw_int of
  71                                  Left err -> Left $ Just $ error_expr_lift
  72                                         (Error_Expr_Read err raw :: Error_Expr_Read Raw)
  73                                  Right (i::Int) ->
  74                                         k type_int $ Forall_Repr_with_Context $
  75                                                 const $ int i
  76                          _ -> Left $ Just $ error_lambda_lift $
  77                                 Error_Expr_Fun_Wrong_number_of_arguments 3 raw
  78                  Raw "neg" raws -> unary_from  raws neg
  79                  Raw "add" raws -> binary_from raws add
  80                  _ -> Left Nothing
  81                 where
  82                 unary_from raws
  83                  (op::forall repr. Sym_Int repr
  84                     => repr Int -> repr Int) =
  85                         case raws of
  86                          [raw_x] ->
  87                                 sym_from (Proxy::Proxy root) ctx raw_x $
  88                                  \(ty_x::Type_Root_of_Expr root h_x) (Forall_Repr_with_Context x) ->
  89                                         case expr_cons_unlift ty_x of
  90                                          Just (Type_Int::Type_Int (Type_Root_of_Expr root) h_x) ->
  91                                                 k ty_x $ Forall_Repr_with_Context (op . x)
  92                                          _ -> Left $ Just $ error_lambda_lift $
  93                                                 Error_Expr_Fun_Argument_mismatch
  94                                                  (Exists_Type type_int)
  95                                                  (Exists_Type ty_x) raw
  96                          _ -> Left $ Just $ error_lambda_lift $
  97                                 Error_Expr_Fun_Wrong_number_of_arguments 1 raw
  98                 binary_from raws
  99                  (op::forall repr. Sym_Int repr
 100                     => repr Int -> repr Int -> repr Int) =
 101                         case raws of
 102                          [raw_x, raw_y] ->
 103                                 sym_from (Proxy::Proxy root) ctx raw_x $
 104                                  \(ty_x::Type_Root_of_Expr root h_x) (Forall_Repr_with_Context x) ->
 105                                 sym_from (Proxy::Proxy root) ctx raw_y $
 106                                  \(ty_y::Type_Root_of_Expr root h_y) (Forall_Repr_with_Context y) ->
 107                                         case expr_cons_unlift ty_x of
 108                                          Just (Type_Int::Type_Int (Type_Root_of_Expr root) h_x) ->
 109                                                 case expr_cons_unlift ty_y of
 110                                                  Just (Type_Int::Type_Int (Type_Root_of_Expr root) h_y) ->
 111                                                         k ty_x $ Forall_Repr_with_Context $
 112                                                          \c -> x c `op` y c
 113                                                  Nothing -> Left $ Just $ error_lambda_lift $
 114                                                         Error_Expr_Fun_Argument_mismatch
 115                                                          (Exists_Type type_int)
 116                                                          (Exists_Type ty_y) raw
 117                                          Nothing -> Left $ Just $ error_lambda_lift $
 118                                                 Error_Expr_Fun_Argument_mismatch
 119                                                  (Exists_Type type_int)
 120                                                  (Exists_Type ty_x) raw
 121                          _ -> Left $ Just $ error_lambda_lift $
 122                                 Error_Expr_Fun_Wrong_number_of_arguments 2 raw
 123                 error_lambda_lift
 124                  :: Error_Expr_Lambda (Error_of_Type Raw (Type_Root_of_Expr root)) (Type_Root_of_Expr root) Raw
 125                  -> Error_of_Expr Raw root
 126                 error_lambda_lift = error_expr_lift
 127
 128 -- ** Type 'Expr_Lambda_Int'
 129 -- | Convenient alias.
 130 type Expr_Lambda_Int lam = Expr_Root (Expr_Cons (Expr_Lambda lam) Expr_Int)
 131
 132 expr_lambda_int_from
 133  :: forall lam raw.
 134  Sym_from raw (Expr_Lambda_Int lam)
 135  => Proxy lam
 136  -> raw
 137  -> Either (Maybe (Error_of_Expr raw (Expr_Lambda_Int lam)))
 138            (Exists_Type_and_Repr (Type_Root_of_Expr (Expr_Lambda_Int lam))
 139                                  (Forall_Repr (Expr_Lambda_Int lam)))
 140 expr_lambda_int_from _px_lam raw =
 141         sym_from
 142          (Proxy::Proxy (Expr_Lambda_Int lam))
 143          Context_Empty raw $ \ty (Forall_Repr_with_Context repr) ->
 144                 Right $ Exists_Type_and_Repr ty $
 145                         Forall_Repr $ repr Context_Empty
 146
 147 -- * Type 'Error_Expr_Int'
 148 data Error_Expr_Int raw
 149  =   Error_Expr_Int
 150  deriving (Eq, Show)
 151