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.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
  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 AST Expr_Bool
  51  ( Type_from AST (Type_Root_of_Expr root)
  52  , Sym_from AST root
  53
  54  , Type_Root_Lift Type_Bool (Type_Root_of_Expr root)
  55  , Error_Type_Lift (Error_Type_Fun AST)
  56                    (Error_of_Type AST (Type_Root_of_Expr root))
  57  , Error_Expr_Lift (Error_Expr_Lambda (Error_of_Type AST (Type_Root_of_Expr root))
  58                                       (                   Type_Root_of_Expr root)
  59                                       AST)
  60                    (Error_of_Expr AST root)
  61  , Error_Expr_Lift (Error_Expr_Read AST)
  62                    (Error_of_Expr AST root)
  63
  64  , Type_Unlift Type_Bool (Type_of_Expr root)
  65
  66  , Root_of_Expr root ~ root
  67  ) => Sym_from AST (Expr_Bool root) where
  68         sym_from _px_ex ctx raw k =
  69                 case raw of
  70                  AST "bool" raws ->
  71                         case raws of
  72                          [AST raw_bool []] ->
  73                                 case read_safe raw_bool of
  74                                  Left err -> Left $ Just $ error_expr_lift
  75                                         (Error_Expr_Read err raw :: Error_Expr_Read AST)
  76                                  Right (i::Bool) ->
  77                                         k type_bool $ Forall_Repr_with_Context $
  78                                                 const $ bool i
  79                          _ -> Left $ Just $ error_lambda_lift $
  80                                 Error_Expr_Fun_Wrong_number_of_arguments 3 raw
  81                  AST "not" raws -> unary_from  raws not
  82                  AST "and" raws -> binary_from raws and
  83                  AST "or"  raws -> binary_from raws or
  84                  AST "xor" raws -> binary_from raws xor
  85                  _ -> Left Nothing
  86                 where
  87                 unary_from raws
  88                  (op::forall repr. Sym_Bool repr
  89                     => repr Bool -> repr Bool) =
  90                         case raws of
  91                          [raw_x] ->
  92                                 sym_from (Proxy::Proxy root) ctx raw_x $
  93                                  \(ty_x::Type_Root_of_Expr root h_x) (Forall_Repr_with_Context x) ->
  94                                         case type_unlift $ unType_Root ty_x of
  95                                          Just (Type_Bool::Type_Bool (Type_Root_of_Expr root) h_x) ->
  96                                                 k ty_x $ Forall_Repr_with_Context (op . x)
  97                                          _ -> Left $ Just $ error_lambda_lift $
  98                                                 Error_Expr_Fun_Argument_mismatch
  99                                                  (Exists_Type type_bool)
 100                                                  (Exists_Type ty_x) raw
 101                          _ -> Left $ Just $ error_lambda_lift $
 102                                 Error_Expr_Fun_Wrong_number_of_arguments 1 raw
 103                 binary_from raws
 104                  (op::forall repr. Sym_Bool repr
 105                     => repr Bool -> repr Bool -> repr Bool) =
 106                         case raws of
 107                          [raw_x, raw_y] ->
 108                                 sym_from (Proxy::Proxy root) ctx raw_x $
 109                                  \(ty_x::Type_Root_of_Expr root h_x) (Forall_Repr_with_Context x) ->
 110                                 sym_from (Proxy::Proxy root) ctx raw_y $
 111                                  \(ty_y::Type_Root_of_Expr root h_y) (Forall_Repr_with_Context y) ->
 112                                         case type_unlift $ unType_Root ty_x of
 113                                          Just (Type_Bool::Type_Bool (Type_Root_of_Expr root) h_x) ->
 114                                                 case type_unlift $ unType_Root ty_y of
 115                                                  Just (Type_Bool::Type_Bool (Type_Root_of_Expr root) h_y) ->
 116                                                         k ty_x $ Forall_Repr_with_Context $
 117                                                          \c -> x c `op` y c
 118                                                  Nothing -> Left $ Just $ error_lambda_lift $
 119                                                         Error_Expr_Fun_Argument_mismatch
 120                                                          (Exists_Type type_bool)
 121                                                          (Exists_Type ty_y) raw
 122                                          Nothing -> Left $ Just $ error_lambda_lift $
 123                                                 Error_Expr_Fun_Argument_mismatch
 124                                                  (Exists_Type type_bool)
 125                                                  (Exists_Type ty_x) raw
 126                          _ -> Left $ Just $ error_lambda_lift $
 127                                 Error_Expr_Fun_Wrong_number_of_arguments 2 raw
 128                 error_lambda_lift
 129                  :: Error_Expr_Lambda (Error_of_Type AST (Type_Root_of_Expr root)) (Type_Root_of_Expr root) AST
 130                  -> Error_of_Expr AST root
 131                 error_lambda_lift = error_expr_lift
 132
 133 -- ** Type 'Expr_Lambda_Bool'
 134 -- | Convenient alias.
 135 type Expr_Lambda_Bool lam = Expr_Root (Expr_Cons (Expr_Lambda lam) Expr_Bool)
 136
 137 expr_lambda_bool_from
 138  :: forall lam raw.
 139  Sym_from raw (Expr_Lambda_Bool lam)
 140  => Proxy lam
 141  -> raw
 142  -> Either (Maybe (Error_of_Expr raw (Expr_Lambda_Bool lam)))
 143            (Exists_Type_and_Repr (Type_Root_of_Expr (Expr_Lambda_Bool lam))
 144                                  (Forall_Repr (Expr_Lambda_Bool lam)))
 145 expr_lambda_bool_from _px_lam raw =
 146         sym_from
 147          (Proxy::Proxy (Expr_Lambda_Bool lam))
 148          Context_Empty raw $ \ty (Forall_Repr_with_Context repr) ->
 149                 Right $ Exists_Type_and_Repr ty $
 150                         Forall_Repr $ repr Context_Empty
 151
 152 -- * Type 'Error_Expr_Bool'
 153 data Error_Expr_Bool raw
 154  =   Error_Expr_Bool
 155  deriving (Eq, Show)