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  |   Error_Type_Constraint_missing  (At ast (EType cs))
  96 deriving instance (Eq ast, Eq (Lexem ast)) => Eq (Error_Type cs ast)
  97 deriving instance (Show ast, Show (Lexem ast), Show_Const cs) => Show (Error_Type cs ast)
  98
  99 -- * Class 'Type_from'
 100 -- | Try to build a 'Type' from raw data.
 101 class Type_from ast cs where
 102         type_from
 103          :: ast
 104          -> (forall ki_h h. Type cs ki_h h -> Either (Error_Type cs ast) ret)
 105          -> Either (Error_Type cs ast) ret
 106
 107 instance
 108  ( Proj_Con cs
 109  , Const_from (Lexem ast) cs
 110  , AST ast
 111  ) => Type_from ast cs where
 112         type_from ast kk =
 113                 fromMaybe (Left $ Error_Type_Constant_unknown $ At ast ()) $
 114                 const_from (ast_lexem ast) $ \c -> Just $
 115                 go (ast_nodes ast) (TyConst c) kk
 116                 where
 117                 go :: forall ki h ret. [ast]
 118                  -> Type cs ki h
 119                  -> (forall ki' h'. Type cs ki' h' -> Either (Error_Type cs ast) ret)
 120                  -> Either (Error_Type cs ast) ret
 121                 go [] ty k = k ty
 122                 go (ast_x:ast_xs) ty_f k =
 123                         type_from ast_x $ \ty_x ->
 124                         let ki_x = kind_of ty_x in
 125                         case kind_of ty_f of
 126                          ki_f_a `SKiArrow` ki_f_b ->
 127                                 case testEquality ki_f_a ki_x of
 128                                  Nothing -> Left $ Error_Type_Kind_mismatch
 129                                          (At ast $ EKind ki_f_a)
 130                                          (At ast_x $ EKind ki_x)
 131                                  Just Refl ->
 132                                         let ty_fx = ty_f :$ ty_x in
 133                                         case ki_f_b of
 134                                          SKiCon ->
 135                                                 case proj_con ty_f ty_x of
 136                                                  Nothing -> Left $ Error_Type_Constraint_missing $ At ast (EType ty_fx)
 137                                                  Just Dict -> go ast_xs (ty_f :~ ty_x) k
 138                                          _ -> go ast_xs ty_fx k
 139                          ki -> Left $ Error_Type_Kind_not_applicable $ At ast (EKind ki)
 140
 141 syBool :: IsString a => Syntax a
 142 syBool = Syntax "Bool" []
 143 syEq :: IsString a => [Syntax a] -> Syntax a
 144 syEq = Syntax "Eq"
 145 syFun :: IsString a => [Syntax a] -> Syntax a
 146 syFun = Syntax "(->)"
 147 syInt :: IsString a => Syntax a
 148 syInt = Syntax "Int" []
 149 syIO :: IsString a => [Syntax a] -> Syntax a
 150 syIO = Syntax "IO"
 151 syTraversable :: IsString a => [Syntax a] -> Syntax a
 152 syTraversable = Syntax "Traversable"
 153 syMonad :: IsString a => [Syntax a] -> Syntax a
 154 syMonad = Syntax "Monad"
 155 (.>) :: IsString a => Syntax a -> Syntax a -> Syntax a
 156 a .> b = syFun [a, b]
 157 infixr 3 .>