Language/LOL/Symantic/Expr/Bool.hs

   1 {-# LANGUAGE ExistentialQuantification #-}
   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 module Language.LOL.Symantic.Expr.Bool where
  12
  13 import Data.Proxy (Proxy(..))
  14 import Prelude hiding (and, not, or)
  15
  16 import Language.LOL.Symantic.Raw
  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
  22 -- * Class 'Sym_Bool'
  23
  24 -- | Symantics combinable with 'Type_Bool'.
  25 class Sym_Bool repr where
  26         bool :: Bool -> repr Bool
  27         not :: repr Bool -> repr Bool
  28         and :: repr Bool -> repr Bool -> repr Bool
  29         or  :: repr Bool -> repr Bool -> repr Bool
  30         xor :: repr Bool -> repr Bool -> repr Bool
  31         xor x y = (x `or` y) `and` not (x `and` y)
  32
  33 instance -- Sym_Bool Dup
  34  ( Sym_Bool r1
  35  , Sym_Bool r2
  36  ) => Sym_Bool (Dup r1 r2) where
  37         bool x = bool x `Dup` bool x
  38         not (x1 `Dup` x2)               = not x1    `Dup` not x2
  39         and (x1 `Dup` x2) (y1 `Dup` y2) = and x1 y1 `Dup` and x2 y2
  40         or  (x1 `Dup` x2) (y1 `Dup` y2) = or  x1 y1 `Dup` or  x2 y2
  41         xor (x1 `Dup` x2) (y1 `Dup` y2) = xor x1 y1 `Dup` xor x2 y2
  42
  43 -- * Type 'Expr_Bool'
  44 data Expr_Bool (root:: *)
  45 type instance Root_of_Expr (Expr_Bool root) = root
  46 type instance Type_of_Expr (Expr_Bool root) = Type_Bool
  47 type instance Sym_of_Expr (Expr_Bool root) repr = Sym_Bool repr
  48 type instance Error_of_Expr raw (Expr_Bool root) = Error_Expr_Bool raw
  49
  50 instance -- Sym_from Raw Expr_Bool
  51  ( Type_from Raw (Type_Root_of_Expr root)
  52  , Sym_from Raw root
  53
  54  , Type_Root_Lift Type_Bool (Type_Root_of_Expr root)
  55  , Error_Type_Lift (Error_Type_Fun Raw)
  56                    (Error_of_Type Raw (Type_Root_of_Expr root))
  57  , Error_Expr_Lift (Error_Expr_Lambda (Error_of_Type Raw (Type_Root_of_Expr root))
  58                                      (                   Type_Root_of_Expr root)
  59                                      Raw)
  60                   (Error_of_Expr Raw root)
  61  , Error_Expr_Lift (Error_Expr_Read Raw)
  62                   (Error_of_Expr Raw root)
  63
  64  , Type_Cons_Unlift Type_Bool (Type_of_Expr root)
  65
  66  , Root_of_Expr root ~ root
  67  -- , Root_of_Type (Type_Root_of_Expr root) ~ Type_Root_of_Expr root
  68  ) => Sym_from Raw (Expr_Bool root) where
  69         sym_from _px_ex ctx raw k =
  70                 case raw of
  71                  Raw "bool" raws ->
  72                         case raws of
  73                          [Raw raw_bool []] ->
  74                                 case read_safe raw_bool of
  75                                  Left err -> Left $ Just $ error_expr_lift
  76                                         (Error_Expr_Read err raw :: Error_Expr_Read Raw)
  77                                  Right (i::Bool) ->
  78                                         k type_bool $ Forall_Repr_with_Context $
  79                                                 const $ bool i
  80                          _ -> Left $ Just $ error_lambda_lift $
  81                                 Error_Expr_Fun_Wrong_number_of_arguments 3 raw
  82                  Raw "not" raws -> unary_from  raws not
  83                  Raw "and" raws -> binary_from raws and
  84                  Raw "or"  raws -> binary_from raws or
  85                  Raw "xor" raws -> binary_from raws xor
  86                  _ -> Left Nothing
  87                 where
  88                 unary_from raws
  89                  (op::forall repr. Sym_Bool repr
  90                     => repr Bool -> repr Bool) =
  91                         case raws of
  92                          [raw_x] ->
  93                                 sym_from (Proxy::Proxy root) ctx raw_x $
  94                                  \(ty_x::Type_Root_of_Expr root h_x) (Forall_Repr_with_Context x) ->
  95                                         case type_cons_unlift $ unType_Root ty_x of
  96                                          Just (Type_Bool::Type_Bool (Type_Root_of_Expr root) h_x) ->
  97                                                 k ty_x $ Forall_Repr_with_Context (op . x)
  98                                          _ -> Left $ Just $ error_lambda_lift $
  99                                                 Error_Expr_Fun_Argument_mismatch
 100                                                  (Exists_Type type_bool)
 101                                                  (Exists_Type ty_x) raw
 102                          _ -> Left $ Just $ error_lambda_lift $
 103                                 Error_Expr_Fun_Wrong_number_of_arguments 1 raw
 104                 binary_from raws
 105                  (op::forall repr. Sym_Bool repr
 106                     => repr Bool -> repr Bool -> repr Bool) =
 107                         case raws of
 108                          [raw_x, raw_y] ->
 109                                 sym_from (Proxy::Proxy root) ctx raw_x $
 110                                  \(ty_x::Type_Root_of_Expr root h_x) (Forall_Repr_with_Context x) ->
 111                                 sym_from (Proxy::Proxy root) ctx raw_y $
 112                                  \(ty_y::Type_Root_of_Expr root h_y) (Forall_Repr_with_Context y) ->
 113                                         case type_cons_unlift $ unType_Root ty_x of
 114                                          Just (Type_Bool::Type_Bool (Type_Root_of_Expr root) h_x) ->
 115                                                 case type_cons_unlift $ unType_Root ty_y of
 116                                                  Just (Type_Bool::Type_Bool (Type_Root_of_Expr root) h_y) ->
 117                                                         k ty_x $ Forall_Repr_with_Context $
 118                                                          \c -> x c `op` y c
 119                                                  Nothing -> Left $ Just $ error_lambda_lift $
 120                                                         Error_Expr_Fun_Argument_mismatch
 121                                                          (Exists_Type type_bool)
 122                                                          (Exists_Type ty_y) raw
 123                                          Nothing -> Left $ Just $ error_lambda_lift $
 124                                                 Error_Expr_Fun_Argument_mismatch
 125                                                  (Exists_Type type_bool)
 126                                                  (Exists_Type ty_x) raw
 127                          _ -> Left $ Just $ error_lambda_lift $
 128                                 Error_Expr_Fun_Wrong_number_of_arguments 2 raw
 129                 error_lambda_lift
 130                  :: Error_Expr_Lambda (Error_of_Type Raw (Type_Root_of_Expr root)) (Type_Root_of_Expr root) Raw
 131                  -> Error_of_Expr Raw root
 132                 error_lambda_lift = error_expr_lift
 133                 {-
 134                 error_bool_lift
 135                  :: Error_Expr_Bool Raw
 136                  -> Error_of_Expr Raw root
 137                 error_bool_lift = error_expr_lift
 138                 -}
 139
 140 -- ** Type 'Expr_Lambda_Bool'
 141 -- | Convenient alias.
 142 type Expr_Lambda_Bool lam = Expr_Root (Expr_Cons (Expr_Lambda lam) Expr_Bool)
 143
 144 expr_lambda_bool_from
 145  :: forall lam raw.
 146  Sym_from raw (Expr_Lambda_Bool lam)
 147  => Proxy lam
 148  -> raw
 149  -> Either (Maybe (Error_of_Expr raw (Expr_Lambda_Bool lam)))
 150            (Exists_Type_and_Repr (Type_Root_of_Expr (Expr_Lambda_Bool lam))
 151                                  (Forall_Repr (Expr_Lambda_Bool lam)))
 152 expr_lambda_bool_from _px_lam raw =
 153         sym_from
 154          (Proxy::Proxy (Expr_Lambda_Bool lam))
 155          Context_Empty raw $ \ty (Forall_Repr_with_Context repr) ->
 156                 Right $ Exists_Type_and_Repr ty $
 157                         Forall_Repr $ repr Context_Empty
 158
 159 -- * Type 'Error_Expr_Bool'
 160 data Error_Expr_Bool raw
 161  =   Error_Expr_Bool
 162  deriving (Eq, Show)