1 {-# LANGUAGE DefaultSignatures #-}
2 {-# LANGUAGE FlexibleContexts #-}
3 {-# LANGUAGE FlexibleInstances #-}
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
14 import Data.Proxy (Proxy(..))
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
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
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
38 instance -- Sym_Int Dup
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
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
54 instance -- Expr_from AST Expr_Int
55 ( Type_from AST (Type_Root_of_Expr root)
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)
64 (Error_of_Expr AST root)
65 , Error_Expr_Lift (Error_Expr_Read AST)
66 (Error_of_Expr AST root)
68 , Type_Unlift Type_Int (Type_of_Expr root)
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 =
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)
82 k type_int $ Forall_Repr_with_Context $
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
91 (op::forall repr. Sym_Int repr
92 => repr Int -> repr Int) =
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
107 (op::forall repr. Sym_Int repr
108 => repr Int -> repr Int -> repr Int) =
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 $
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
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
136 -- ** Type 'Expr_Lambda_Int'
137 -- | Convenient alias.
138 type Expr_Lambda_Int lam = Expr_Root (Expr_Cons (Expr_Lambda lam) Expr_Int)
142 Expr_from ast (Expr_Lambda_Int lam)
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 =
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
155 -- * Type 'Error_Expr_Int'
156 data Error_Expr_Int ast