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