Bump versions.

[haskell/symantic.git] / symantic-lib / Language / Symantic / Lib / If.hs

diff --git a/symantic-lib/Language/Symantic/Lib/If.hs b/symantic-lib/Language/Symantic/Lib/If.hs
index 6136eb8c76b787fdba3f95ff39b8d43f8c2c3ceb..62e1628f468f858f1c521c043ade2f8f2cfca477 100644 (file)
--- a/symantic-lib/Language/Symantic/Lib/If.hs
+++ b/symantic-lib/Language/Symantic/Lib/If.hs
@@ -1,76 +1,55 @@
 {-# LANGUAGE UndecidableInstances #-}
 {-# OPTIONS_GHC -fno-warn-orphans #-}
-{-# OPTIONS_GHC -fconstraint-solver-iterations=5 #-}
--- | Symantic for @if@.
+-- | Symantic for @If@.
 module Language.Symantic.Lib.If where
 
-import Data.Proxy
 import qualified Data.Text as Text
-import Data.Type.Equality ((:~:)(Refl))
 
-import Language.Symantic.Parsing
-import Language.Symantic.Typing
-import Language.Symantic.Compiling
-import Language.Symantic.Interpreting
-import Language.Symantic.Transforming
-import Language.Symantic.Lib.Lambda
+import Language.Symantic
+import Language.Symantic.Lib.Bool (tyBool)
+import Language.Symantic.Lib.Function (a0)
+
+-- * Type 'If'
+data If
 
 -- * Class 'Sym_If'
+type instance Sym If = Sym_If
 class Sym_If term where
        if_ :: term Bool -> term a -> term a -> term a
-       default if_ :: Trans t term => t term Bool -> t term a -> t term a -> t term a
-       if_ = trans_map3 if_
+       default if_ :: Sym_If (UnT term) => Trans term => term Bool -> term a -> term a -> term a
+       if_ = trans3 if_
 
--- * Type 'If'
-data If
-type instance Sym_of_Iface (Proxy If) = Sym_If
-type instance TyConsts_of_Iface (Proxy If) = TyConsts_imported_by If
-type instance TyConsts_imported_by If = '[ Proxy Bool ]
-
-instance Sym_If HostI where
-       if_ (HostI b) ok ko = if b then ok else ko
-instance Sym_If TextI where
-       if_ (TextI cond) (TextI ok) (TextI ko) =
-               TextI $ \po v ->
-                       infix_paren po op $
+-- Interpreting
+instance Sym_If Eval where
+       if_ (Eval b) ok ko = if b then ok else ko
+instance Sym_If View where
+       if_ (View cond) (View ok) (View ko) =
+               View $ \po v ->
+                       parenInfix po op $
                        Text.concat
-                        [ "if ", cond (op, L) v
-                        , " then ", ok (op, L) v
-                        , " else ", ko (op, L) v ]
+                        [ "if ", cond (op, SideL) v
+                        , " then ", ok (op, SideL) v
+                        , " else ", ko (op, SideL) v ]
                where op = infixN 2
-instance (Sym_If r1, Sym_If r2) => Sym_If (DupI r1 r2) where
-       if_  = dupI3 @Sym_If if_
+instance (Sym_If r1, Sym_If r2) => Sym_If (Dup r1 r2) where
+       if_  = dup3 @Sym_If if_
+
+-- Transforming
+instance (Sym_If term, Sym_Lambda term) => Sym_If (BetaT term)
+
+-- Typing
+instance NameTyOf If where
+       nameTyOf _c = ["If"] `Mod` "If"
+instance ClassInstancesFor If
+instance TypeInstancesFor If
+
+-- Compiling
+instance Gram_Term_AtomsFor src ss g If
+ -- TODO: some support for if-then-else or ternary (?:) operator
+instance ModuleFor src ss If
 
-instance
- ( Read_TyNameR TyName cs rs
- ) => Read_TyNameR TyName cs (Proxy If ': rs) where
-       read_TyNameR _rs = read_TyNameR (Proxy @rs)
-instance Show_TyConst cs => Show_TyConst (Proxy If ': cs) where
-       show_TyConst TyConstZ{} = "If"
-       show_TyConst (TyConstS c) = show_TyConst c
+-- ** 'Type's
 
-instance Proj_TyConC cs (Proxy If)
-data instance TokenT meta (ts::[*]) (Proxy If)
- = Token_Term_If_if (EToken meta ts) (EToken meta ts)
-deriving instance Eq_Token meta ts => Eq (TokenT meta ts (Proxy If))
-deriving instance Show_Token meta ts => Show (TokenT meta ts (Proxy If))
-instance -- CompileI
- ( Inj_TyConst (TyConsts_of_Ifaces is) Bool
- , Inj_TyConst (TyConsts_of_Ifaces is) (->)
- , Compile is
- ) => CompileI is (Proxy If) where
-       compileI tok ctx k =
-               case tok of
-                Token_Term_If_if tok_cond tok_ok ->
-                       -- if :: Bool -> a -> a -> a
-                       compileO tok_cond ctx $ \ty_cond (TermO cond) ->
-                       compileO tok_ok   ctx $ \ty_ok   (TermO ok) ->
-                       check_TyEq
-                        (At Nothing (ty @Bool))
-                        (At (Just tok_cond) ty_cond) $ \Refl ->
-                       k (ty_ok ~> ty_ok) $ TermO $
-                        \c -> lam $ if_ (cond c) (ok c)
-instance -- TokenizeT
- -- Inj_Token meta ts If =>
- TokenizeT meta ts (Proxy If)
-instance Gram_Term_AtomsT meta ts (Proxy If) g -- TODO
+-- ** 'Term's
+teIf_if :: TermDef If '[Proxy a] (() #> (Bool -> a -> a -> a))
+teIf_if = Term noConstraint (tyBool ~> a0 ~> a0 ~> a0) $ teSym @If $ lam3 if_