]> Git — Sourcephile - haskell/symantic.git/blob - Language/LOL/Symantic/Expr/If.hs
init
[haskell/symantic.git] / Language / LOL / Symantic / Expr / If.hs
1 {-# LANGUAGE DefaultSignatures #-}
2 {-# LANGUAGE FlexibleContexts #-}
3 {-# LANGUAGE ScopedTypeVariables #-}
4 {-# LANGUAGE TypeFamilies #-}
5 module Language.LOL.Symantic.Expr.If where
6
7 import Data.Proxy (Proxy(..))
8 import Data.Type.Equality ((:~:)(Refl))
9 import Language.LOL.Symantic.Expr.Bool
10 import Language.LOL.Symantic.Expr.Common
11 import Language.LOL.Symantic.Expr.Lambda
12 import Language.LOL.Symantic.Repr.Dup
13 import Language.LOL.Symantic.Trans.Common
14 import Language.LOL.Symantic.Type
15
16 -- * Class 'Sym_If'
17
18 class Sym_If repr where
19 if_ :: repr Bool -> repr a -> repr a -> repr a
20 default if_ :: Trans t repr => t repr Bool -> t repr a -> t repr a -> t repr a
21 if_ = trans_map3 if_
22 class Sym_When repr where
23 when :: repr Bool -> repr () -> repr ()
24 default when :: Trans t repr => t repr Bool -> t repr () -> t repr ()
25 when = trans_map2 when
26
27 instance -- Sym_If Dup
28 ( Sym_If r1
29 , Sym_If r2
30 ) => Sym_If (Dup r1 r2) where
31 if_ (c1 `Dup` c2) (ok1 `Dup` ok2) (ko1 `Dup` ko2) =
32 if_ c1 ok1 ko1 `Dup`
33 if_ c2 ok2 ko2
34 instance -- Sym_When Dup
35 ( Sym_When r1
36 , Sym_When r2
37 ) => Sym_When (Dup r1 r2) where
38 when (c1 `Dup` c2) (ok1 `Dup` ok2) =
39 when c1 ok1 `Dup`
40 when c2 ok2
41
42 -- * Type 'Expr_If'
43 -- | Expression.
44 data Expr_If (root:: *)
45 type instance Root_of_Expr (Expr_If root) = root
46 type instance Type_of_Expr (Expr_If root) = No_Type
47 type instance Sym_of_Expr (Expr_If root) repr = (Sym_If repr)
48 type instance Error_of_Expr ast (Expr_If root) = No_Error_Expr
49
50 if_from
51 :: forall root ty ast hs ret.
52 ( ty ~ Type_Root_of_Expr (Expr_If root)
53 , Type_Root_Lift Type_Bool (Type_Root_of_Expr root)
54 , Type_Eq (Type_Root_of_Expr root)
55 , Expr_from ast root
56 , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
57 (Error_of_Expr ast root)
58 , Root_of_Expr root ~ root
59 ) => ast -> ast -> ast
60 -> Expr_From ast (Expr_If root) hs ret
61 if_from ast_cond ast_ok ast_ko ex ast ctx k =
62 expr_from (Proxy::Proxy root) ast_cond ctx $
63 \(ty_cond::Type_Root_of_Expr root h_n) (Forall_Repr_with_Context cond) ->
64 expr_from (Proxy::Proxy root) ast_ok ctx $
65 \(ty_ok::Type_Root_of_Expr root h_ok) (Forall_Repr_with_Context ok) ->
66 expr_from (Proxy::Proxy root) ast_ko ctx $
67 \(ty_ko::Type_Root_of_Expr root h_ko) (Forall_Repr_with_Context ko) ->
68 when_type_eq ex ast type_bool ty_cond $ \Refl ->
69 when_type_eq ex ast ty_ok ty_ko $ \Refl ->
70 k ty_ok $ Forall_Repr_with_Context $
71 \c -> if_ (cond c) (ok c) (ko c)
72
73 -- * Type 'Expr_When'
74 -- | Expression.
75 data Expr_When (root:: *)
76 type instance Root_of_Expr (Expr_When root) = root
77 type instance Type_of_Expr (Expr_When root) = No_Type
78 type instance Sym_of_Expr (Expr_When root) repr = (Sym_When repr)
79 type instance Error_of_Expr ast (Expr_When root) = No_Error_Expr
80
81 when_from
82 :: forall root ty ast hs ret.
83 ( ty ~ Type_Root_of_Expr (Expr_When root)
84 , Type_Root_Lift Type_Bool (Type_Root_of_Expr root)
85 , Type_Root_Lift Type_Unit (Type_Root_of_Expr root)
86 , Type_Eq (Type_Root_of_Expr root)
87 , Expr_from ast root
88 , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
89 (Error_of_Expr ast root)
90 , Root_of_Expr root ~ root
91 ) => ast -> ast
92 -> Expr_From ast (Expr_When root) hs ret
93 when_from ast_cond ast_ok ex ast ctx k =
94 expr_from (Proxy::Proxy root) ast_cond ctx $
95 \(ty_cond::Type_Root_of_Expr root h_n) (Forall_Repr_with_Context cond) ->
96 expr_from (Proxy::Proxy root) ast_ok ctx $
97 \(ty_ok::Type_Root_of_Expr root h_ok) (Forall_Repr_with_Context ok) ->
98 when_type_eq ex ast type_bool ty_cond $ \Refl ->
99 when_type_eq ex ast type_unit ty_ok $ \Refl ->
100 k ty_ok $ Forall_Repr_with_Context $
101 \c -> when (cond c) (ok c)
102
103 -- ** Type 'Expr_Lambda_Bool_If'
104 -- | Convenient alias.
105 type Expr_Lambda_If_Bool lam
106 = Expr_Root (Expr_Alt (Expr_Lambda lam)
107 (Expr_Alt Expr_If
108 Expr_Bool))
109
110 -- | Convenient alias around 'expr_from'.
111 expr_lambda_if_bool_from
112 :: forall lam ast root.
113 ( Expr_from ast (Expr_Lambda_If_Bool lam)
114 , root ~ Expr_Lambda_If_Bool lam
115 ) => Proxy lam
116 -> ast
117 -> Either (Error_of_Expr ast root)
118 (Exists_Type_and_Repr (Type_Root_of_Expr root)
119 (Forall_Repr root))
120 expr_lambda_if_bool_from _px_lam ast =
121 expr_from (Proxy::Proxy root) ast
122 Context_Empty $ \ty (Forall_Repr_with_Context repr) ->
123 Right $ Exists_Type_and_Repr ty $
124 Forall_Repr $ repr Context_Empty