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