]> 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'.
12 module Language.LOL.Symantic.Expr.Int where
13
14 import Data.Proxy (Proxy(..))
15 import Data.Type.Equality ((:~:)(Refl))
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_Int'
25
26 -- | Symantic.
27 class Sym_Int repr where
28 int :: Int -> repr Int
29 neg :: repr Int -> repr Int
30 add :: repr Int -> repr Int -> repr Int
31
32 default int :: Trans t repr => Int -> t repr Int
33 default neg :: Trans t repr => t repr Int -> t repr Int
34 default add :: Trans t repr => t repr Int -> t repr Int -> t repr Int
35 int = trans_lift . int
36 neg = trans_map1 neg
37 add = trans_map2 add
38
39 instance -- Sym_Int Dup
40 ( Sym_Int r1
41 , Sym_Int r2
42 ) => Sym_Int (Dup r1 r2) where
43 int x = int x `Dup` int x
44 neg (x1 `Dup` x2) = neg x1 `Dup` neg x2
45 add (x1 `Dup` x2) (y1 `Dup` y2) = add x1 y1 `Dup` add x2 y2
46
47 -- * Type 'Expr_Int'
48 -- | Expression.
49 data Expr_Int (root:: *)
50 type instance Root_of_Expr (Expr_Int root) = root
51 type instance Type_of_Expr (Expr_Int root) = Type_Int
52 type instance Sym_of_Expr (Expr_Int root) repr = Sym_Int repr
53 type instance Error_of_Expr ast (Expr_Int root) = No_Error_Expr
54
55 instance -- Expr_from AST Expr_Int
56 ( Type_from AST (Type_Root_of_Expr root)
57 , Expr_from AST root
58
59 , Type_Root_Lift Type_Int (Type_Root_of_Expr root)
60 , Error_Expr_Lift (Error_Expr (Error_of_Type AST (Type_Root_of_Expr root))
61 ( Type_Root_of_Expr root)
62 AST)
63 (Error_of_Expr AST root)
64
65 , Type_Unlift Type_Int (Type_of_Expr root)
66
67 , Root_of_Expr root ~ root
68
69 , Implicit_HBool (Is_Last_Expr (Expr_Int root) root)
70 ) => Expr_from AST (Expr_Int root) where
71 expr_from px_ex ctx ast k =
72 case ast of
73 AST "int" asts ->
74 case asts of
75 [AST ast_int []] ->
76 case read_safe ast_int of
77 Left err -> Left $ error_expr px_ex $ Error_Expr_Read err ast
78 Right (i::Int) ->
79 k type_int $ Forall_Repr_with_Context $
80 const $ int i
81 _ -> Left $ error_expr px_ex $
82 Error_Expr_Wrong_number_of_arguments ast 1
83 AST "neg" asts -> unary_from asts neg
84 AST "add" asts -> binary_from asts add
85 _ -> Left $ error_expr_unsupported px_ex ast
86 where
87 unary_from asts
88 (op::forall repr. Sym_Int repr
89 => repr Int -> repr Int) =
90 case asts of
91 [ast_x] ->
92 expr_from (Proxy::Proxy root) ctx ast_x $ \ty_x (Forall_Repr_with_Context x) ->
93 when_type_eq px_ex ast type_int ty_x $ \Refl ->
94 k ty_x $ Forall_Repr_with_Context (op . x)
95 _ -> Left $ error_expr px_ex $
96 Error_Expr_Wrong_number_of_arguments ast 1
97 binary_from asts
98 (op::forall repr. Sym_Int repr
99 => repr Int -> repr Int -> repr Int) =
100 case asts of
101 [ast_x, ast_y] ->
102 expr_from (Proxy::Proxy root) ctx ast_x $ \ty_x (Forall_Repr_with_Context x) ->
103 expr_from (Proxy::Proxy root) ctx ast_y $ \ty_y (Forall_Repr_with_Context y) ->
104 when_type_eq px_ex ast type_int ty_x $ \Refl ->
105 when_type_eq px_ex ast type_int ty_y $ \Refl ->
106 k ty_x $ Forall_Repr_with_Context $
107 \c -> x c `op` y c
108 _ -> Left $ error_expr px_ex $
109 Error_Expr_Wrong_number_of_arguments ast 2
110
111 -- ** Type 'Expr_Lambda_Int'
112 -- | Convenient alias.
113 type Expr_Lambda_Int lam = Expr_Root (Expr_Alt (Expr_Lambda lam) Expr_Int)
114
115 -- | Convenient alias around 'expr_from'.
116 expr_lambda_int_from
117 :: forall lam ast.
118 Expr_from ast (Expr_Lambda_Int lam)
119 => Proxy lam
120 -> ast
121 -> Either (Error_of_Expr ast (Expr_Lambda_Int lam))
122 (Exists_Type_and_Repr (Type_Root_of_Expr (Expr_Lambda_Int lam))
123 (Forall_Repr (Expr_Lambda_Int lam)))
124 expr_lambda_int_from _px_lam ast =
125 expr_from
126 (Proxy::Proxy (Expr_Lambda_Int lam))
127 Context_Empty ast $ \ty (Forall_Repr_with_Context repr) ->
128 Right $ Exists_Type_and_Repr ty $
129 Forall_Repr $ repr Context_Empty