]> Git — Sourcephile - haskell/symantic.git/blob - Language/Symantic/Compiling/If.hs
Add Compiling.Show.
[haskell/symantic.git] / Language / Symantic / Compiling / If.hs
1 {-# LANGUAGE UndecidableInstances #-}
2 {-# OPTIONS_GHC -fno-warn-orphans #-}
3 {-# OPTIONS_GHC -fconstraint-solver-iterations=5 #-}
4 -- | Symantic for @if@.
5 module Language.Symantic.Compiling.If where
6
7 import Data.Proxy
8 import Data.Text (Text)
9 import qualified Data.Text as Text
10 import Data.Type.Equality ((:~:)(Refl))
11
12 import Language.Symantic.Parsing
13 import Language.Symantic.Typing
14 import Language.Symantic.Compiling.Term
15 import Language.Symantic.Interpreting
16 import Language.Symantic.Transforming.Trans
17
18 -- * Class 'Sym_If'
19 class Sym_If term where
20 if_ :: term Bool -> term a -> term a -> term a
21 default if_ :: Trans t term => t term Bool -> t term a -> t term a -> t term a
22 if_ = trans_map3 if_
23
24 -- * Type 'If'
25 data If
26 type instance Sym_of_Iface (Proxy If) = Sym_If
27 type instance Consts_of_Iface (Proxy If) = Consts_imported_by If
28 type instance Consts_imported_by If = '[ Proxy Bool ]
29
30 instance Sym_If HostI where
31 if_ (HostI b) ok ko = if b then ok else ko
32 instance Sym_If TextI where
33 if_ (TextI cond) (TextI ok) (TextI ko) =
34 TextI $ \p v ->
35 let p' = Precedence 2 in
36 paren p p' $
37 Text.concat
38 [ "if ", cond p' v
39 , " then ", ok p' v
40 , " else ", ko p' v ]
41 instance (Sym_If r1, Sym_If r2) => Sym_If (DupI r1 r2) where
42 if_ = dupI3 (Proxy @Sym_If) if_
43
44 instance Const_from Text cs => Const_from Text (Proxy If ': cs) where
45 const_from s k = const_from s $ k . ConstS
46
47 instance Proj_ConC cs (Proxy If)
48 data instance TokenT meta (ts::[*]) (Proxy If)
49 = Token_Term_If_if (EToken meta ts) (EToken meta ts)
50 deriving instance Eq_Token meta ts => Eq (TokenT meta ts (Proxy If))
51 deriving instance Show_Token meta ts => Show (TokenT meta ts (Proxy If))
52 instance -- Term_fromI
53 ( Inj_Const (Consts_of_Ifaces is) Bool
54 , Inj_Const (Consts_of_Ifaces is) (->)
55 , Term_from is
56 ) => Term_fromI is (Proxy If) where
57 term_fromI tok ctx k =
58 case tok of
59 Token_Term_If_if tok_cond tok_ok ->
60 -- if :: Bool -> a -> a -> a
61 term_from tok_cond ctx $ \ty_cond (TermLC cond) ->
62 term_from tok_ok ctx $ \ty_ok (TermLC ok) ->
63 check_type
64 (At Nothing (ty @Bool))
65 (At (Just tok_cond) ty_cond) $ \Refl ->
66 k (ty_ok ~> ty_ok) $ TermLC $
67 \c -> lam $ if_ (cond c) (ok c)