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
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
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 AST) (Error_of_Expr AST root)
67 , Type_Unlift Type_Int (Type_of_Expr root)
69 , Root_of_Expr root ~ root
70 -- , Root_of_Type (Type_Root_of_Expr root) ~ Type_Root_of_Expr root
71 ) => Expr_from AST (Expr_Int root) where
72 expr_from _px_ex ctx ast k =
77 case read_safe ast_int of
78 Left err -> Left $ error_expr_lift $ Error_Expr_Read err ast
80 k type_int $ Forall_Repr_with_Context $
82 _ -> Left $ error_lambda_lift $
83 Error_Expr_Fun_Wrong_number_of_arguments 3 ast
84 AST "neg" asts -> unary_from asts neg
85 AST "add" asts -> binary_from asts add
86 _ -> Left $ error_expr_lift $ Error_Expr_Unsupported ast
89 (op::forall repr. Sym_Int repr
90 => repr Int -> repr Int) =
93 expr_from (Proxy::Proxy root) ctx ast_x $
94 \(ty_x::Type_Root_of_Expr root h_x) (Forall_Repr_with_Context x) ->
95 case type_unlift $ unType_Root ty_x of
96 Just (Type_Int::Type_Int (Type_Root_of_Expr root) h_x) ->
97 k ty_x $ Forall_Repr_with_Context (op . x)
98 _ -> Left $ error_lambda_lift $
99 Error_Expr_Fun_Argument_mismatch
100 (Exists_Type type_int)
101 (Exists_Type ty_x) ast
102 _ -> Left $ error_lambda_lift $
103 Error_Expr_Fun_Wrong_number_of_arguments 1 ast
105 (op::forall repr. Sym_Int repr
106 => repr Int -> repr Int -> repr Int) =
109 expr_from (Proxy::Proxy root) ctx ast_x $
110 \(ty_x::Type_Root_of_Expr root h_x) (Forall_Repr_with_Context x) ->
111 expr_from (Proxy::Proxy root) ctx ast_y $
112 \(ty_y::Type_Root_of_Expr root h_y) (Forall_Repr_with_Context y) ->
113 case type_unlift $ unType_Root ty_x of
114 Just (Type_Int::Type_Int (Type_Root_of_Expr root) h_x) ->
115 case type_unlift $ unType_Root ty_y of
116 Just (Type_Int::Type_Int (Type_Root_of_Expr root) h_y) ->
117 k ty_x $ Forall_Repr_with_Context $
119 Nothing -> Left $ error_lambda_lift $
120 Error_Expr_Fun_Argument_mismatch
121 (Exists_Type type_int)
122 (Exists_Type ty_y) ast
123 Nothing -> Left $ error_lambda_lift $
124 Error_Expr_Fun_Argument_mismatch
125 (Exists_Type type_int)
126 (Exists_Type ty_x) ast
127 _ -> Left $ error_lambda_lift $
128 Error_Expr_Fun_Wrong_number_of_arguments 2 ast
130 :: Error_Expr_Lambda (Error_of_Type AST (Type_Root_of_Expr root)) (Type_Root_of_Expr root) AST
131 -> Error_of_Expr AST root
132 error_lambda_lift = error_expr_lift
134 -- ** Type 'Expr_Lambda_Int'
135 -- | Convenient alias.
136 type Expr_Lambda_Int lam = Expr_Root (Expr_Cons (Expr_Lambda lam) Expr_Int)
140 Expr_from ast (Expr_Lambda_Int lam)
143 -> Either (Error_of_Expr ast (Expr_Lambda_Int lam))
144 (Exists_Type_and_Repr (Type_Root_of_Expr (Expr_Lambda_Int lam))
145 (Forall_Repr (Expr_Lambda_Int lam)))
146 expr_lambda_int_from _px_lam ast =
148 (Proxy::Proxy (Expr_Lambda_Int lam))
149 Context_Empty ast $ \ty (Forall_Repr_with_Context repr) ->
150 Right $ Exists_Type_and_Repr ty $
151 Forall_Repr $ repr Context_Empty
153 -- * Type 'Error_Expr_Int'
154 data Error_Expr_Int ast