Language/Symantic/Typing/Syntax.hs

   1 {-# LANGUAGE DataKinds #-}
   2 {-# LANGUAGE PolyKinds #-}
   3 {-# LANGUAGE ConstraintKinds #-}
   4 {-# LANGUAGE FlexibleContexts #-}
   5 {-# LANGUAGE FlexibleInstances #-}
   6 {-# LANGUAGE GADTs #-}
   7 {-# LANGUAGE NoMonomorphismRestriction #-}
   8 {-# LANGUAGE MultiParamTypeClasses #-}
   9 {-# LANGUAGE OverloadedStrings #-}
  10 {-# LANGUAGE Rank2Types #-}
  11 {-# LANGUAGE ScopedTypeVariables #-}
  12 {-# LANGUAGE StandaloneDeriving #-}
  13 {-# LANGUAGE TypeFamilies #-}
  14 {-# LANGUAGE UndecidableInstances #-}
  15 module Language.Symantic.Typing.Syntax where
  16
  17 import qualified Data.List as List
  18 import Data.Maybe
  19 import Data.Type.Equality
  20 import Data.String (IsString(..))
  21
  22 import Language.Symantic.Typing.Kind
  23 import Language.Symantic.Typing.Constant
  24 import Language.Symantic.Typing.Type
  25 import Language.Symantic.Typing.Constraint
  26
  27 -- * Class 'AST'
  28 class AST node where
  29         type Lexem node
  30         ast_lexem :: node -> Lexem node
  31         ast_nodes :: node -> [node]
  32
  33 instance AST (Syntax a) where
  34         type Lexem (Syntax a) = a
  35         ast_lexem (Syntax x _)  = x
  36         ast_nodes (Syntax _ ns) = ns
  37
  38 -- * Type 'At'
  39 -- | Attach a location.
  40 data At ast a
  41  =   At ast a
  42  deriving (Eq, Show)
  43 instance Functor (At ast) where
  44         fmap f (At ast a) = At ast (f a)
  45
  46 -- * Type 'Syntax'
  47 data Syntax a
  48  =   Syntax a [Syntax a]
  49  deriving (Eq)
  50
  51 -- | Custom 'Show' instance a little bit more readable
  52 -- than the automatically derived one.
  53 instance Show (Syntax String) where
  54         showsPrec p ast@(Syntax n args) =
  55                 case ast of
  56                  Syntax _ [] -> showString n
  57                  Syntax "(->)" [a] ->
  58                         showParen (p <= prec_arrow) $
  59                         showString (""++n++" ") .
  60                         showsPrec prec_arrow a
  61                  Syntax "(->)" [a, b] ->
  62                         showParen (p <= prec_arrow) $
  63                         showsPrec prec_arrow a .
  64                         showString (" -> ") .
  65                         showsPrec (prec_arrow + 1) b
  66                  Syntax "\\" [var, ty, body] ->
  67                         showParen (p <= prec_lambda) $
  68                         showString ("\\(") .
  69                         showsPrec prec_lambda var .
  70                         showString (":") .
  71                         showsPrec prec_lambda ty .
  72                         showString (") -> ") .
  73                         showsPrec prec_lambda body
  74                  Syntax "$" [fun, arg] ->
  75                         showParen (p <= prec_dollar) $
  76                         showsPrec prec_dollar fun .
  77                         showString (" $ ") .
  78                         showsPrec prec_dollar arg
  79                  _ ->
  80                         showParen (p <= prec_app) $
  81                         showString n .
  82                         showString " " .
  83                         showString (List.unwords $ show <$> args)
  84                 where
  85                 prec_arrow  = 1
  86                 prec_lambda = 1
  87                 prec_dollar = 1
  88                 prec_app    = 10
  89
  90 -- * Type 'Error_Type'
  91 data Error_Type cs ast
  92  =   Error_Type_Constant_unknown    (At ast ())
  93  |   Error_Type_Kind_mismatch       (At ast EKind) (At ast EKind)
  94  |   Error_Type_Kind_not_applicable (At ast EKind)
  95 deriving instance (Eq ast, Eq (Lexem ast)) => Eq (Error_Type cs ast)
  96 deriving instance (Show ast, Show (Lexem ast), Show_Const cs) => Show (Error_Type cs ast)
  97
  98 -- * Class 'Type_from'
  99 -- | Try to build a 'Type' from raw data.
 100 class Type_from ast cs where
 101         type_from
 102          :: ast
 103          -> (forall ki_h h. Type cs ki_h h -> Either (Error_Type cs ast) ret)
 104          -> Either (Error_Type cs ast) ret
 105
 106 instance
 107  ( Proj_Con cs
 108  , Const_from (Lexem ast) cs
 109  , AST ast
 110  ) => Type_from ast cs where
 111         type_from ast kk =
 112                 fromMaybe (Left $ Error_Type_Constant_unknown $ At ast ()) $
 113                 const_from (ast_lexem ast) $ \c -> Just $
 114                 go (ast_nodes ast) (TyConst c) kk
 115                 where
 116                 go :: forall ki h ret. [ast]
 117                  -> Type cs ki h
 118                  -> (forall ki' h'. Type cs ki' h' -> Either (Error_Type cs ast) ret)
 119                  -> Either (Error_Type cs ast) ret
 120                 go [] ty k = k ty
 121                 go (ast_x:ast_xs) ty_f k =
 122                         type_from ast_x $ \ty_x ->
 123                         case kind_of ty_f of
 124                          ki_f_a `SKiArrow` _ki_f_b ->
 125                                 let ki_x = kind_of ty_x in
 126                                 case testEquality ki_f_a ki_x of
 127                                  Just Refl -> go ast_xs (ty_f :$ ty_x) k
 128                                  Nothing -> Left $ Error_Type_Kind_mismatch
 129                                          (At ast $ EKind ki_f_a)
 130                                          (At ast_x $ EKind ki_x)
 131                          ki -> Left $ Error_Type_Kind_not_applicable $ At ast (EKind ki)
 132
 133 syBool :: IsString a => Syntax a
 134 syBool = Syntax "Bool" []
 135 syEq :: IsString a => [Syntax a] -> Syntax a
 136 syEq = Syntax "Eq"
 137 syFun :: IsString a => [Syntax a] -> Syntax a
 138 syFun = Syntax "(->)"
 139 syInt :: IsString a => Syntax a
 140 syInt = Syntax "Int" []
 141 syIO :: IsString a => [Syntax a] -> Syntax a
 142 syIO = Syntax "IO"
 143 syTraversable :: IsString a => [Syntax a] -> Syntax a
 144 syTraversable = Syntax "Traversable"
 145 syMonad :: IsString a => [Syntax a] -> Syntax a
 146 syMonad = Syntax "Monad"
 147 (.>) :: IsString a => Syntax a -> Syntax a -> Syntax a
 148 a .> b = syFun [a, b]
 149 infixr 3 .>