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 =
  29  '[ Proxy Bool
  30  ]
  31
  32 instance Sym_If HostI where
  33         if_ (HostI b) ok ko = if b then ok else ko
  34 instance Sym_If TextI where
  35         if_ (TextI cond) (TextI ok) (TextI ko) =
  36                 TextI $ \p v ->
  37                         let p' = Precedence 2 in
  38                         paren p p' $
  39                         Text.concat
  40                          [ "if ", cond p' v
  41                          , " then ", ok p' v
  42                          , " else ", ko p' v ]
  43 instance (Sym_If r1, Sym_If r2) => Sym_If (DupI r1 r2) where
  44         if_  = dupI3 (Proxy @Sym_If) if_
  45
  46 instance Const_from Text cs => Const_from Text (Proxy If ': cs) where
  47         const_from s k = const_from s $ k . ConstS
  48
  49 instance Proj_ConC cs (Proxy If)
  50 data instance TokenT meta (ts::[*]) (Proxy If)
  51  = Token_Term_If_if (EToken meta ts) (EToken meta ts)
  52 deriving instance Eq_Token meta ts => Eq (TokenT meta ts (Proxy If))
  53 deriving instance Show_Token meta ts => Show (TokenT meta ts (Proxy If))
  54 instance -- Term_fromI
  55  ( Inj_Const (Consts_of_Ifaces is) Bool
  56  , Inj_Const (Consts_of_Ifaces is) (->)
  57  , Term_from is
  58  ) => Term_fromI is (Proxy If) where
  59         term_fromI tok ctx k =
  60                 case tok of
  61                  Token_Term_If_if tok_cond tok_ok ->
  62                         -- if :: Bool -> a -> a -> a
  63                         term_from tok_cond ctx $ \ty_cond (TermLC cond) ->
  64                         term_from tok_ok   ctx $ \ty_ok   (TermLC ok) ->
  65                         check_type
  66                          (At Nothing (ty @Bool))
  67                          (At (Just tok_cond) ty_cond) $ \Refl ->
  68                         k (ty_ok ~> ty_ok) $ TermLC $
  69                          \c -> lam $ if_ (cond c) (ok c)