Language/Symantic/Compiling/Bool.hs

   1 {-# LANGUAGE DefaultSignatures #-}
   2 {-# LANGUAGE FlexibleContexts #-}
   3 {-# LANGUAGE FlexibleInstances #-}
   4 {-# LANGUAGE MultiParamTypeClasses #-}
   5 {-# LANGUAGE OverloadedStrings #-}
   6 {-# LANGUAGE Rank2Types #-}
   7 {-# LANGUAGE ScopedTypeVariables #-}
   8 {-# LANGUAGE TypeFamilies #-}
   9 {-# LANGUAGE TypeOperators #-}
  10 {-# LANGUAGE UndecidableInstances #-}
  11 {-# OPTIONS_GHC -fno-warn-orphans #-}
  12 -- | Symantic for 'Bool'.
  13 module Language.Symantic.Compiling.Bool where
  14
  15 import Control.Monad
  16 import qualified Data.Bool as Bool
  17 import Data.Monoid
  18 import Data.Proxy
  19 import Data.Type.Equality ((:~:)(Refl))
  20 import qualified Data.Text as Text
  21 import Prelude hiding ((&&), not, (||))
  22
  23 import Language.Symantic.Typing
  24 import Language.Symantic.Compiling.Term
  25 import Language.Symantic.Interpreting
  26 import Language.Symantic.Transforming.Trans
  27
  28 -- * Class 'Sym_Bool'
  29 -- | Symantic.
  30 class Sym_Bool term where
  31         bool ::      Bool -> term Bool
  32         not  :: term Bool -> term Bool
  33         (&&) :: term Bool -> term Bool -> term Bool
  34         (||) :: term Bool -> term Bool -> term Bool
  35         xor  :: term Bool -> term Bool -> term Bool
  36         xor x y = (x || y) && not (x && y)
  37
  38         default bool :: Trans t term =>        Bool -> t term Bool
  39         default not  :: Trans t term => t term Bool -> t term Bool
  40         default (&&) :: Trans t term => t term Bool -> t term Bool -> t term Bool
  41         default (||) :: Trans t term => t term Bool -> t term Bool -> t term Bool
  42
  43         bool = trans_lift . bool
  44         not  = trans_map1 not
  45         (&&) = trans_map2 (&&)
  46         (||) = trans_map2 (||)
  47
  48 infixr 2 ||
  49 infixr 2 `xor`
  50 infixr 3 &&
  51
  52 type instance Sym_of_Iface (Proxy Bool) = Sym_Bool
  53
  54 instance Sym_Bool HostI where
  55         bool = HostI
  56         not  = liftM Bool.not
  57         (&&) = liftM2 (Bool.&&)
  58         (||) = liftM2 (Bool.||)
  59 instance Sym_Bool TextI where
  60         bool a = TextI $ \_p _v ->
  61                 Text.pack (show a)
  62         not (TextI x) =
  63                 TextI $ \p v ->
  64                         let p' = Precedence 9 in
  65                         paren p p' $ "not " <> x p' v
  66         (&&) = textI_infix "&&"    (Precedence 6)
  67         (||) = textI_infix "||"    (Precedence 5)
  68         xor  = textI_infix "`xor`" (Precedence 5)
  69 instance (Sym_Bool r1, Sym_Bool r2) => Sym_Bool (DupI r1 r2) where
  70         bool x = bool x `DupI` bool x
  71         not  = dupI1 sym_Bool not
  72         (&&) = dupI2 sym_Bool (&&)
  73         (||) = dupI2 sym_Bool (||)
  74         xor  = dupI2 sym_Bool xor
  75
  76 sym_Bool :: Proxy Sym_Bool
  77 sym_Bool = Proxy
  78
  79 instance -- Term_fromI
  80  ( AST ast
  81  , Lexem ast ~ LamVarName
  82  , Inj_Const (Consts_of_Ifaces is) Bool
  83  , Inj_Const (Consts_of_Ifaces is) (->)
  84  , Term_from is ast
  85  ) => Term_fromI is (Proxy Bool) ast where
  86         term_fromI ast ctx k =
  87                 case ast_lexem ast of
  88                  "True"  -> k tyBool $ Term_of_LamCtx $ \_c -> bool True
  89                  "False" -> k tyBool $ Term_of_LamCtx $ \_c -> bool False
  90                  "not" -> op1_from not
  91                  "&&"  -> op2_from (&&)
  92                  "||"  -> op2_from (||)
  93                  "xor" -> op2_from xor
  94                  _ -> Left $ Error_Term_unsupported
  95                 where
  96                 op1_from (op::forall term. Sym_Bool term => term Bool -> term Bool) =
  97                         case ast_nodes ast of
  98                          [] -> k (tyBool ~> tyBool) $ Term_of_LamCtx $
  99                                  \_c -> lam op
 100                          [ast_x] ->
 101                                 term_from ast_x ctx $ \ty_x (Term_of_LamCtx x) ->
 102                                 check_type (At Nothing tyBool) (At (Just ast_x) ty_x) $ \Refl ->
 103                                 k tyBool $ Term_of_LamCtx $
 104                                  \c -> op (x c)
 105                          _ -> Left $ Error_Term_Syntax $
 106                                 Error_Syntax_too_many_arguments $ At (Just ast) 1
 107                 op2_from (op::forall term. Sym_Bool term => term Bool -> term Bool -> term Bool) =
 108                         case ast_nodes ast of
 109                          [] -> k (tyBool ~> tyBool ~> tyBool) $ Term_of_LamCtx $
 110                                  \_c -> lam $ lam . op
 111                          [ast_x] ->
 112                                 term_from ast_x ctx $ \ty_x (Term_of_LamCtx x) ->
 113                                 check_type (At Nothing tyBool) (At (Just ast_x) ty_x) $ \Refl ->
 114                                 k (tyBool ~> tyBool) $ Term_of_LamCtx $
 115                                  \c -> lam $ op (x c)
 116                          [ast_x, ast_y] ->
 117                                 term_from ast_x ctx $ \ty_x (Term_of_LamCtx x) ->
 118                                 term_from ast_y ctx $ \ty_y (Term_of_LamCtx y) ->
 119                                 check_type (At Nothing tyBool) (At (Just ast_x) ty_x) $ \Refl ->
 120                                 check_type (At Nothing tyBool) (At (Just ast_y) ty_y) $ \Refl ->
 121                                 k tyBool $ Term_of_LamCtx $
 122                                  \c -> op (x c) (y c)
 123                          _ -> Left $ Error_Term_Syntax $
 124                                 Error_Syntax_too_many_arguments $ At (Just ast) 2