symantic/Language/Symantic/Typing/Read.hs

   1 {-# LANGUAGE AllowAmbiguousTypes #-}
   2 {-# LANGUAGE PolyKinds #-}
   3 module Language.Symantic.Typing.Read where
   4
   5 import Language.Symantic.Grammar
   6 import Language.Symantic.Typing.Kind
   7 import Language.Symantic.Typing.Type
   8 import Language.Symantic.Typing.Show ()
   9 import Language.Symantic.Typing.Grammar
  10 import Language.Symantic.Typing.Variable
  11
  12 -- | Read a 'Type' from an 'AST_Type', given its 'Vars'.
  13 readType ::
  14  SourceInj (KindK src) src =>
  15  SourceInj (TypeVT src) src =>
  16  SourceInj (AST_Type src) src =>
  17  AST_Type src ->
  18  Either (Error_Type src) (TypeVT src)
  19 readType ast | EVars vs <- readVars (EVars VarsZ) ast = do
  20         TypeT ty <- readTyVars vs ast
  21         Right $ TypeVT ty
  22
  23 -- | Read a 'Type' from an 'AST_Type', given its 'Vars'.
  24 readTyVars ::
  25  forall vs src.
  26  SourceInj (KindK src) src =>
  27  SourceInj (TypeVT src) src =>
  28  SourceInj (AST_Type src) src =>
  29  Vars src vs ->
  30  AST_Type src ->
  31  Either (Error_Type src) (TypeT src vs)
  32 readTyVars vs (BinTree0 (Token_Type_Const (TypeTLen t))) =
  33         Right $ t (lenVars vs)
  34         -- readTyName is ms (sourceInj ast) (lenVars vs) name
  35 readTyVars vs (BinTree0 (Token_Type_Var (At src name))) =
  36         case lookupVars name vs of
  37          Just (EVar v) -> Right $ TypeT $ TyVar src name v
  38          Nothing -> error "[BUG] readTyVars: lookupVars failed"
  39 readTyVars vs ast@(ast_x `BinTree2` ast_y) = do
  40         TypeT ty_x <- readTyVars vs ast_x
  41         TypeT ty_y <- readTyVars vs ast_y
  42         when_KiFun (kindOf ty_x) $ \Refl ki_x_a _ki_x_b ->
  43                 when_EqKind ki_x_a (kindOf ty_y) $ \Refl ->
  44                         Right $ TypeT $ TyApp (sourceInj ast) ty_x ty_y
  45
  46 -- | Return the given 'EVars' augmented by the ones used in given 'AST_Type'.
  47 readVars :: Source src => EVars src -> AST_Type src -> EVars src
  48 readVars evs@(EVars vs) (BinTree0 (Token_Type_Var (At _src name))) =
  49         case lookupVars name vs of
  50          Just{} -> evs
  51          Nothing -> do
  52                 let kv = KiType noSource
  53                 let vs' = VarsS name kv vs
  54                 EVars vs'
  55 readVars evs BinTree0{} = evs
  56 readVars evs (BinTree2 x y) =
  57         readVars (readVars evs x) y