]> Git — Sourcephile - haskell/symantic.git/blob - symantic-lib/Language/Symantic/Lib/If.hs
Fix comment typo.
[haskell/symantic.git] / symantic-lib / Language / Symantic / Lib / 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.Lib.If where
6
7 import Data.Proxy
8 import qualified Data.Text as Text
9 import Data.Type.Equality ((:~:)(Refl))
10
11 import Language.Symantic.Parsing
12 import Language.Symantic.Typing
13 import Language.Symantic.Compiling
14 import Language.Symantic.Interpreting
15 import Language.Symantic.Transforming
16 import Language.Symantic.Lib.Lambda
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 TyConsts_of_Iface (Proxy If) = TyConsts_imported_by If
28 type instance TyConsts_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 $ \po v ->
35 infix_paren po op $
36 Text.concat
37 [ "if ", cond (op, L) v
38 , " then ", ok (op, L) v
39 , " else ", ko (op, L) v ]
40 where op = infixN 2
41 instance (Sym_If r1, Sym_If r2) => Sym_If (DupI r1 r2) where
42 if_ = dupI3 @Sym_If if_
43
44 instance
45 ( Read_TyNameR TyName cs rs
46 ) => Read_TyNameR TyName cs (Proxy If ': rs) where
47 read_TyNameR _rs = read_TyNameR (Proxy @rs)
48 instance Show_TyConst cs => Show_TyConst (Proxy If ': cs) where
49 show_TyConst TyConstZ{} = "If"
50 show_TyConst (TyConstS c) = show_TyConst c
51
52 instance Proj_TyConC cs (Proxy If)
53 data instance TokenT meta (ts::[*]) (Proxy If)
54 = Token_Term_If_if (EToken meta ts) (EToken meta ts)
55 deriving instance Eq_Token meta ts => Eq (TokenT meta ts (Proxy If))
56 deriving instance Show_Token meta ts => Show (TokenT meta ts (Proxy If))
57 instance -- CompileI
58 ( Inj_TyConst (TyConsts_of_Ifaces is) Bool
59 , Inj_TyConst (TyConsts_of_Ifaces is) (->)
60 , Compile is
61 ) => CompileI is (Proxy If) where
62 compileI tok ctx k =
63 case tok of
64 Token_Term_If_if tok_cond tok_ok ->
65 -- if :: Bool -> a -> a -> a
66 compileO tok_cond ctx $ \ty_cond (TermO cond) ->
67 compileO tok_ok ctx $ \ty_ok (TermO ok) ->
68 check_TyEq
69 (At Nothing (ty @Bool))
70 (At (Just tok_cond) ty_cond) $ \Refl ->
71 k (ty_ok ~> ty_ok) $ TermO $
72 \c -> lam $ if_ (cond c) (ok c)
73 instance -- TokenizeT
74 -- Inj_Token meta ts If =>
75 TokenizeT meta ts (Proxy If)
76 instance Gram_Term_AtomsT meta ts (Proxy If) g -- TODO