]> Git — Sourcephile - haskell/symantic.git/blob - Language/LOL/Symantic/Expr/Bool.hs
init
[haskell/symantic.git] / Language / LOL / Symantic / Expr / Bool.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 'Bool's.
12 module Language.LOL.Symantic.Expr.Bool where
13
14 import Data.Proxy (Proxy(..))
15 import Prelude hiding (and, not, or)
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_Bool'
25
26 -- | Symantic.
27 class Sym_Bool repr where
28 bool :: Bool -> repr Bool
29 not :: repr Bool -> repr Bool
30 and :: repr Bool -> repr Bool -> repr Bool
31 or :: repr Bool -> repr Bool -> repr Bool
32 xor :: repr Bool -> repr Bool -> repr Bool
33 xor x y = (x `or` y) `and` not (x `and` y)
34
35 default bool :: Trans t repr => Bool -> t repr Bool
36 default not :: Trans t repr => t repr Bool -> t repr Bool
37 default and :: Trans t repr => t repr Bool -> t repr Bool -> t repr Bool
38 default or :: Trans t repr => t repr Bool -> t repr Bool -> t repr Bool
39 bool = trans_lift . bool
40 not = trans_map1 not
41 and = trans_map2 and
42 or = trans_map2 or
43
44 instance -- Sym_Bool Dup
45 ( Sym_Bool r1
46 , Sym_Bool r2
47 ) => Sym_Bool (Dup r1 r2) where
48 bool x = bool x `Dup` bool x
49 not (x1 `Dup` x2) = not x1 `Dup` not x2
50 and (x1 `Dup` x2) (y1 `Dup` y2) = and x1 y1 `Dup` and x2 y2
51 or (x1 `Dup` x2) (y1 `Dup` y2) = or x1 y1 `Dup` or x2 y2
52 xor (x1 `Dup` x2) (y1 `Dup` y2) = xor x1 y1 `Dup` xor x2 y2
53
54 -- * Type 'Expr_Bool'
55 -- | Expression.
56 data Expr_Bool (root:: *)
57 type instance Root_of_Expr (Expr_Bool root) = root
58 type instance Type_of_Expr (Expr_Bool root) = Type_Bool
59 type instance Sym_of_Expr (Expr_Bool root) repr = Sym_Bool repr
60 type instance Error_of_Expr ast (Expr_Bool root) = Error_Expr_Bool ast
61
62 instance -- Expr_from AST Expr_Bool
63 ( Type_from AST (Type_Root_of_Expr root)
64 , Expr_from AST root
65
66 , Type_Root_Lift Type_Bool (Type_Root_of_Expr root)
67 , Error_Type_Lift (Error_Type_Fun AST)
68 (Error_of_Type AST (Type_Root_of_Expr root))
69 , Error_Expr_Lift (Error_Expr (Error_of_Type AST (Type_Root_of_Expr root))
70 ( Type_Root_of_Expr root)
71 AST)
72 (Error_of_Expr AST root)
73
74 , Type_Unlift Type_Bool (Type_of_Expr root)
75
76 , Root_of_Expr root ~ root
77
78 , Implicit_HBool (Is_Last_Expr (Expr_Bool root) root)
79 ) => Expr_from AST (Expr_Bool root) where
80 expr_from px_ex ctx ast k =
81 case ast of
82 AST "bool" asts ->
83 case asts of
84 [AST ast_bool []] ->
85 case read_safe ast_bool of
86 Left err -> Left $ error_expr px_ex $ Error_Expr_Read err ast
87 Right (i::Bool) ->
88 k type_bool $ Forall_Repr_with_Context $
89 const $ bool i
90 _ -> Left $ error_expr px_ex $
91 Error_Expr_Wrong_number_of_arguments 3 ast
92 AST "not" asts -> unary_from asts not
93 AST "and" asts -> binary_from asts and
94 AST "or" asts -> binary_from asts or
95 AST "xor" asts -> binary_from asts xor
96 _ -> Left $
97 case hbool :: HBool (Is_Last_Expr (Expr_Bool root) root) of
98 HTrue -> error_expr px_ex $ Error_Expr_Unsupported ast
99 HFalse -> error_expr px_ex $ Error_Expr_Unsupported_here ast
100 where
101 unary_from asts
102 (op::forall repr. Sym_Bool repr
103 => repr Bool -> repr Bool) =
104 case asts of
105 [ast_x] ->
106 expr_from (Proxy::Proxy root) ctx ast_x $
107 \(ty_x::Type_Root_of_Expr root h_x) (Forall_Repr_with_Context x) ->
108 case type_unlift $ unType_Root ty_x of
109 Just (Type_Bool::Type_Bool (Type_Root_of_Expr root) h_x) ->
110 k ty_x $ Forall_Repr_with_Context (op . x)
111 _ -> Left $ error_expr px_ex $
112 Error_Expr_Argument_mismatch
113 (Exists_Type type_bool)
114 (Exists_Type ty_x) ast
115 _ -> Left $ error_expr px_ex $
116 Error_Expr_Wrong_number_of_arguments 1 ast
117 binary_from asts
118 (op::forall repr. Sym_Bool repr
119 => repr Bool -> repr Bool -> repr Bool) =
120 case asts of
121 [ast_x, ast_y] ->
122 expr_from (Proxy::Proxy root) ctx ast_x $
123 \(ty_x::Type_Root_of_Expr root h_x) (Forall_Repr_with_Context x) ->
124 expr_from (Proxy::Proxy root) ctx ast_y $
125 \(ty_y::Type_Root_of_Expr root h_y) (Forall_Repr_with_Context y) ->
126 case type_unlift $ unType_Root ty_x of
127 Just (Type_Bool::Type_Bool (Type_Root_of_Expr root) h_x) ->
128 case type_unlift $ unType_Root ty_y of
129 Just (Type_Bool::Type_Bool (Type_Root_of_Expr root) h_y) ->
130 k ty_x $ Forall_Repr_with_Context $
131 \c -> x c `op` y c
132 Nothing -> Left $ error_expr px_ex $
133 Error_Expr_Argument_mismatch
134 (Exists_Type type_bool)
135 (Exists_Type ty_y) ast
136 Nothing -> Left $ error_expr px_ex $
137 Error_Expr_Argument_mismatch
138 (Exists_Type type_bool)
139 (Exists_Type ty_x) ast
140 _ -> Left $ error_expr px_ex $
141 Error_Expr_Wrong_number_of_arguments 2 ast
142
143 -- ** Type 'Expr_Lambda_Bool'
144 -- | Convenient alias.
145 type Expr_Lambda_Bool lam = Expr_Root (Expr_Alt (Expr_Lambda lam) Expr_Bool)
146
147 expr_lambda_bool_from
148 :: forall lam ast.
149 Expr_from ast (Expr_Lambda_Bool lam)
150 => Proxy lam
151 -> ast
152 -> Either (Error_of_Expr ast (Expr_Lambda_Bool lam))
153 (Exists_Type_and_Repr (Type_Root_of_Expr (Expr_Lambda_Bool lam))
154 (Forall_Repr (Expr_Lambda_Bool lam)))
155 expr_lambda_bool_from _px_lam ast =
156 expr_from
157 (Proxy::Proxy (Expr_Lambda_Bool lam))
158 Context_Empty ast $ \ty (Forall_Repr_with_Context repr) ->
159 Right $ Exists_Type_and_Repr ty $
160 Forall_Repr $ repr Context_Empty
161
162 -- * Type 'Error_Expr_Bool'
163 data Error_Expr_Bool ast
164 = Error_Expr_Bool
165 deriving (Eq, Show)