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.Parsing.Grammar
  13 import Language.Symantic.Typing
  14 import Language.Symantic.Compiling
  15 import Language.Symantic.Interpreting
  16 import Language.Symantic.Transforming.Trans
  17 import Language.Symantic.Lib.Lambda
  18
  19 -- * Class 'Sym_If'
  20 class Sym_If term where
  21         if_ :: term Bool -> term a -> term a -> term a
  22         default if_ :: Trans t term => t term Bool -> t term a -> t term a -> t term a
  23         if_ = trans_map3 if_
  24
  25 -- * Type 'If'
  26 data If
  27 type instance Sym_of_Iface (Proxy If) = Sym_If
  28 type instance Consts_of_Iface (Proxy If) = Consts_imported_by If
  29 type instance Consts_imported_by If = '[ Proxy Bool ]
  30
  31 instance Sym_If HostI where
  32         if_ (HostI b) ok ko = if b then ok else ko
  33 instance Sym_If TextI where
  34         if_ (TextI cond) (TextI ok) (TextI ko) =
  35                 TextI $ \po v ->
  36                         infix_paren po op $
  37                         Text.concat
  38                          [ "if ", cond (op, L) v
  39                          , " then ", ok (op, L) v
  40                          , " else ", ko (op, L) v ]
  41                 where op = infixN 2
  42 instance (Sym_If r1, Sym_If r2) => Sym_If (DupI r1 r2) where
  43         if_  = dupI3 (Proxy @Sym_If) if_
  44
  45 instance
  46  ( Read_TypeNameR Type_Name cs rs
  47  ) => Read_TypeNameR Type_Name cs (Proxy If ': rs) where
  48         read_typenameR _rs = read_typenameR (Proxy @rs)
  49 instance Show_Const cs => Show_Const (Proxy If ': cs) where
  50         show_const ConstZ{} = "If"
  51         show_const (ConstS c) = show_const c
  52
  53 instance Proj_ConC cs (Proxy If)
  54 data instance TokenT meta (ts::[*]) (Proxy If)
  55  = Token_Term_If_if (EToken meta ts) (EToken meta ts)
  56 deriving instance Eq_Token meta ts => Eq (TokenT meta ts (Proxy If))
  57 deriving instance Show_Token meta ts => Show (TokenT meta ts (Proxy If))
  58 instance -- CompileI
  59  ( Inj_Const (Consts_of_Ifaces is) Bool
  60  , Inj_Const (Consts_of_Ifaces is) (->)
  61  , Compile is
  62  ) => CompileI is (Proxy If) where
  63         compileI tok ctx k =
  64                 case tok of
  65                  Token_Term_If_if tok_cond tok_ok ->
  66                         -- if :: Bool -> a -> a -> a
  67                         compileO tok_cond ctx $ \ty_cond (TermO cond) ->
  68                         compileO tok_ok   ctx $ \ty_ok   (TermO ok) ->
  69                         check_type
  70                          (At Nothing (ty @Bool))
  71                          (At (Just tok_cond) ty_cond) $ \Refl ->
  72                         k (ty_ok ~> ty_ok) $ TermO $
  73                          \c -> lam $ if_ (cond c) (ok c)
  74 instance -- TokenizeT
  75  -- Inj_Token meta ts If =>
  76  TokenizeT meta ts (Proxy If)
  77 instance Gram_Term_AtomsT meta ts (Proxy If) g -- TODO