symantic/Language/Symantic/Typing/Read.hs

   1 {-# LANGUAGE AllowAmbiguousTypes #-}
   2 {-# LANGUAGE PolyKinds #-}
   3 module Language.Symantic.Typing.Read where
   4
   5 import Data.Maybe (fromMaybe)
   6 import Data.Typeable
   7 import qualified Data.Map.Strict as Map
   8
   9 import Language.Symantic.Grammar
  10 import Language.Symantic.Typing.List
  11 import Language.Symantic.Typing.Kind
  12 import Language.Symantic.Typing.Type
  13 import Language.Symantic.Typing.Show ()
  14 import Language.Symantic.Typing.Grammar
  15 import Language.Symantic.Typing.Variable
  16 import Language.Symantic.Typing.Module
  17
  18 -- | Read a 'Type' from an 'AST_Type', given its 'Vars'.
  19 readType ::
  20  SourceInj (KindK src) src =>
  21  SourceInj (TypeVT src) src =>
  22  SourceInj (AST_Type src) src =>
  23  Imports NameTy ->
  24  ModulesTy src ->
  25  AST_Type src ->
  26  Either (Error_Type src) (TypeVT src)
  27 readType is ms ast | EVars vs <- readVars (EVars VarsZ) ast = do
  28         TypeT ty <- readTyVars is ms vs ast
  29         Right $ TypeVT ty
  30
  31 -- | Read a 'Type' from an 'AST_Type', given its 'Vars'.
  32 readTyVars ::
  33  forall vs src.
  34  SourceInj (KindK src) src =>
  35  SourceInj (TypeVT src) src =>
  36  SourceInj (AST_Type src) src =>
  37  Imports NameTy ->
  38  ModulesTy src ->
  39  Vars src vs ->
  40  AST_Type src ->
  41  Either (Error_Type src) (TypeT src vs)
  42 readTyVars is ms vs ast@(BinTree0 (Token_Type_Const (At _src name))) =
  43         readTyName is ms (sourceInj ast) (lenVars vs) name
  44 readTyVars _is _ms vs ast@(BinTree0 (Token_Type_Var (At _src name))) =
  45         case lookupVars name vs of
  46          Just (EVar v) -> Right $ TypeT $ TyVar (sourceInj ast) name v
  47          Nothing -> error "[BUG] readTyVars: lookupVars failed"
  48 readTyVars is ms vs ast@(ast_x `BinTree2` ast_y) = do
  49         TypeT ty_x <- readTyVars is ms vs ast_x
  50         TypeT ty_y <- readTyVars is ms vs ast_y
  51         when_KiFun (kindOf ty_x) $ \Refl ki_x_a _ki_x_b ->
  52                 when_EqKind ki_x_a (kindOf ty_y) $ \Refl ->
  53                         Right $ TypeT $ TyApp (sourceInj ast) ty_x ty_y
  54
  55 -- | Lookup a 'TyConst' or 'Type' synonym
  56 -- associated with given 'NameTy' in given 'ModulesTy',
  57 -- building it for a @vs@ of given 'Len'.
  58 readTyName ::
  59  Source src =>
  60  Imports NameTy ->
  61  ModulesTy src -> src -> Len vs -> Mod NameTy ->
  62  Either (Error_Type src) (TypeT src vs)
  63 readTyName is ms src len name@(m `Mod` n) =
  64         let m' = fromMaybe m $ lookupImports FixyInfix name is in
  65         case Map.lookup (m' `Mod` n) ms of
  66          Just (TypeTLen t) -> Right $ t len
  67          Nothing -> Left $ Error_Type_Constant_unknown $ At src name
  68
  69 -- | Return the given 'EVars' augmented by the ones used in given 'AST_Type'.
  70 readVars :: Source src => EVars src -> AST_Type src -> EVars src
  71 readVars evs@(EVars vs) (BinTree0 (Token_Type_Var (At _src name))) =
  72         case lookupVars name vs of
  73          Just{} -> evs
  74          Nothing -> do
  75                 let kv = KiType noSource
  76                 let vs' = VarsS name kv vs
  77                 EVars vs'
  78 readVars evs BinTree0{} = evs
  79 readVars evs (BinTree2 x y) =
  80         readVars (readVars evs x) y
  81
  82 -- * Type 'Error_Type'
  83 data Error_Type src
  84  =   Error_Type_Constant_unknown (At src (Mod NameTy))
  85  |   Error_Type_Con_Kind         (Con_Kind src)
  86  deriving (Eq, Show)
  87 instance ErrorInj (Error_Type src) (Error_Type src) where
  88         errorInj = id
  89 instance ErrorInj (Con_Kind src) (Error_Type src) where
  90         errorInj = Error_Type_Con_Kind