]> Git — Sourcephile - haskell/symantic.git/blob - Language/Symantic/Expr/If.hs
Repr_Dup helpers
[haskell/symantic.git] / Language / Symantic / Expr / If.hs
1 {-# LANGUAGE DefaultSignatures #-}
2 {-# LANGUAGE FlexibleContexts #-}
3 {-# LANGUAGE OverloadedStrings #-}
4 {-# LANGUAGE ScopedTypeVariables #-}
5 {-# LANGUAGE TypeFamilies #-}
6 {-# LANGUAGE TypeOperators #-}
7 -- | Expression for @if@.
8 module Language.Symantic.Expr.If where
9
10 import qualified Control.Monad as Monad
11 import Data.Monoid
12 import Data.Proxy (Proxy(..))
13 import Data.Type.Equality ((:~:)(Refl))
14
15 import Language.Symantic.Type
16 import Language.Symantic.Repr
17 import Language.Symantic.Expr.Root
18 import Language.Symantic.Expr.Error
19 import Language.Symantic.Expr.From
20 import Language.Symantic.Trans.Common
21
22 -- * Class 'Sym_If'
23 -- | Symantic.
24 class Sym_If repr where
25 if_ :: repr Bool -> repr a -> repr a -> repr a
26 default if_ :: Trans t repr => t repr Bool -> t repr a -> t repr a -> t repr a
27 if_ = trans_map3 if_
28 instance Sym_If Repr_Host where
29 if_ (Repr_Host b) ok ko = if b then ok else ko
30 instance Sym_If Repr_Text where
31 if_ (Repr_Text cond) (Repr_Text ok) (Repr_Text ko) =
32 Repr_Text $ \p v ->
33 let p' = Precedence 2 in
34 paren p p' $
35 "if " <> cond p' v <>
36 " then " <> ok p' v <>
37 " else " <> ko p' v
38
39 instance (Sym_If r1, Sym_If r2) => Sym_If (Repr_Dup r1 r2) where
40 if_ = repr_dup3 sym_If if_
41
42 sym_If :: Proxy Sym_If
43 sym_If = Proxy
44
45 -- * Class 'Sym_When'
46 -- | Symantic.
47 class Sym_When repr where
48 when :: repr Bool -> repr () -> repr ()
49 default when :: Trans t repr => t repr Bool -> t repr () -> t repr ()
50 when = trans_map2 when
51 instance Sym_When Repr_Host where
52 when (Repr_Host b) = Monad.when b
53 instance Sym_When Repr_Text where
54 when (Repr_Text cond) (Repr_Text ok) =
55 Repr_Text $ \p v ->
56 let p' = Precedence 2 in
57 paren p p' $
58 "when " <> cond p' v <>
59 " " <> ok p' v
60 instance (Sym_When r1, Sym_When r2) => Sym_When (Repr_Dup r1 r2) where
61 when = repr_dup2 sym_When when
62
63 sym_When :: Proxy Sym_When
64 sym_When = Proxy
65
66 -- * Type 'Expr_If'
67 -- | Expression.
68 data Expr_If (root:: *)
69 type instance Root_of_Expr (Expr_If root) = root
70 type instance Type_of_Expr (Expr_If root) = No_Type
71 type instance Sym_of_Expr (Expr_If root) repr = (Sym_If repr)
72 type instance Error_of_Expr ast (Expr_If root) = No_Error_Expr
73
74 if_from
75 :: forall root ty ast hs ret.
76 ( ty ~ Type_Root_of_Expr (Expr_If root)
77 , Type0_Eq ty
78 , Type0_Lift Type_Bool (Type_of_Expr root)
79 , Expr_From ast root
80 , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
81 (Error_of_Expr ast root)
82 , Root_of_Expr root ~ root
83 ) => ast -> ast -> ast
84 -> ExprFrom ast (Expr_If root) hs ret
85 if_from ast_cond ast_ok ast_ko ex ast ctx k =
86 expr_from (Proxy::Proxy root) ast_cond ctx $
87 \(ty_cond::ty h_n) (Forall_Repr_with_Context cond) ->
88 expr_from (Proxy::Proxy root) ast_ok ctx $
89 \(ty_ok::ty h_ok) (Forall_Repr_with_Context ok) ->
90 expr_from (Proxy::Proxy root) ast_ko ctx $
91 \(ty_ko::ty h_ko) (Forall_Repr_with_Context ko) ->
92 check_type0_eq ex ast type_bool ty_cond $ \Refl ->
93 check_type0_eq ex ast ty_ok ty_ko $ \Refl ->
94 k ty_ok $ Forall_Repr_with_Context $
95 \c -> if_ (cond c) (ok c) (ko c)
96
97 -- * Type 'Expr_When'
98 -- | Expression.
99 data Expr_When (root:: *)
100 type instance Root_of_Expr (Expr_When root) = root
101 type instance Type_of_Expr (Expr_When root) = No_Type
102 type instance Sym_of_Expr (Expr_When root) repr = (Sym_When repr)
103 type instance Error_of_Expr ast (Expr_When root) = No_Error_Expr
104
105 when_from
106 :: forall root ty ast hs ret.
107 ( ty ~ Type_Root_of_Expr (Expr_When root)
108 , Type0_Eq ty
109 , Type0_Lift Type_Bool (Type_of_Expr root)
110 , Type0_Lift Type_Unit (Type_of_Expr root)
111 , Expr_From ast root
112 , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
113 (Error_of_Expr ast root)
114 , Root_of_Expr root ~ root
115 ) => ast -> ast
116 -> ExprFrom ast (Expr_When root) hs ret
117 when_from ast_cond ast_ok ex ast ctx k =
118 expr_from (Proxy::Proxy root) ast_cond ctx $
119 \(ty_cond::ty h_n) (Forall_Repr_with_Context cond) ->
120 expr_from (Proxy::Proxy root) ast_ok ctx $
121 \(ty_ok::ty h_ok) (Forall_Repr_with_Context ok) ->
122 check_type0_eq ex ast type_bool ty_cond $ \Refl ->
123 check_type0_eq ex ast type_unit ty_ok $ \Refl ->
124 k ty_ok $ Forall_Repr_with_Context $
125 \c -> when (cond c) (ok c)