symantic/Language/Symantic/Compiling/Read.hs

   1 {-# LANGUAGE GADTs #-}
   2 module Language.Symantic.Compiling.Read where
   3
   4 import Control.Arrow (left)
   5 import qualified Data.Kind as K
   6
   7 import Language.Symantic.Grammar
   8 import Language.Symantic.Typing
   9
  10 import Language.Symantic.Compiling.Term
  11 import Language.Symantic.Compiling.Module
  12 import Language.Symantic.Compiling.Beta
  13
  14 -- | Read a 'TermVT' from and 'AST_Term'.
  15 readTerm ::
  16  forall src ss ts.
  17  Source src =>
  18  Inj_Source (TypeVT src) src =>
  19  Inj_Source (KindK src) src =>
  20  Inj_Source (AST_Type src) src =>
  21  Constable (->) =>
  22  Name2Type src ->
  23  CtxTy src ts ->
  24  AST_Term src ss ->
  25  Either (Error_Term src) (TermVT src ss ts)
  26 readTerm cs ctxTe ast = do
  27         ts <- go ctxTe `traverse` ast
  28         inj_Error `left` betaTerms ts
  29         where
  30         go ::
  31          forall ts'.
  32          CtxTy src ts' ->
  33          Token_Term src ss ->
  34          Either (Error_Term src) (TermVT src ss ts')
  35         go _ts (Token_Term (TermVT_CF te)) = Right $ TermVT te
  36         go ts  (Token_Term_Var _src name)  = teVar name ts
  37         go _ts (Token_Term_App _src)       = Right $ TermVT teApp
  38         go ts  (Token_Term_Abst _src name_arg ast_ty_arg ast_body) = do
  39                 TypeVT ty_arg <- inj_Error `left` readType cs ast_ty_arg
  40                 when_EqKind (inj_Kind @K.Type) (kindOf ty_arg) $ \Refl ->
  41                         case lenVars ty_arg of
  42                          LenS{} -> Left $ Error_Term_polymorphic $ TypeVT ty_arg
  43                          LenZ | (TypeK qa, TypeK ta) <- unQualTy ty_arg -> do
  44                                 TermVT (Term qr tr (TeSym res)) <- readTerm cs (CtxTyS name_arg ta ts) ast_body
  45                                 let (qa', qr') = appendVars qa qr
  46                                 let (ta', tr') = appendVars ta tr
  47                                 Right $ TermVT $ Term @_ @_ @_ @_ @(_ #> _) (qa' # qr') (ta' ~> tr') $
  48                                         TeSym $ \c -> lam $ \arg -> res (arg `CtxTeS` c)
  49         go ts (Token_Term_Let _src name ast_arg ast_body) = do
  50                 TermVT (Term qa ta (TeSym arg)) <- readTerm cs ts ast_arg
  51                 case lenVars ta of
  52                  LenS{} -> Left $ Error_Term_polymorphic $ TypeVT (qa #> ta)
  53                  LenZ -> do
  54                         TermVT (Term qr tr (TeSym res)) <- readTerm cs (CtxTyS name ta ts) ast_body
  55                         let (qa', qr') = appendVars qa qr
  56                         let tr' = allocVarsL (lenVars ta) tr
  57                         Right $ TermVT $ Term @_ @_ @_ @_ @(_ #> _) (qa' # qr') tr' $
  58                                 TeSym $ \c -> let_ (arg c) $ \a -> res (a `CtxTeS` c)
  59
  60 teVar ::
  61  forall ss src ts.
  62  Source src =>
  63  NameTe -> CtxTy src ts -> Either (Error_Term src) (TermVT src ss ts)
  64 teVar name CtxTyZ = Left $ Error_Term_unknown name
  65 teVar name (CtxTyS n ty _) | n == name =
  66         Right $ TermVT $ Term @_ @_ @_ @_ @(_ #> _) noConstraint ty $
  67                 TeSym $ \(te `CtxTeS` _) -> te
  68 teVar name (CtxTyS _n _typ ts') = do
  69         TermVT (Term q t (TeSym te)) <- teVar @ss name ts'
  70         Right $ TermVT $ Term @_ @_ @_ @_ @(_ #> _) q t $
  71                 TeSym $ \(_ `CtxTeS` ts) -> te ts
  72
  73 teApp ::
  74  Source src => Constable (->) =>
  75  Term src ss ts '[Proxy (a::K.Type), Proxy (b::K.Type)] ((a -> b) -> a -> b)
  76 teApp =
  77         Term noConstraint ((a ~> b) ~> a ~> b) $
  78         TeSym $ const apply
  79         where
  80         a :: Source src => Type src '[Proxy a, Proxy b] (a::K.Type)
  81         a = tyVar "a" $ varZ
  82         b :: Source src => Type src '[Proxy a, Proxy b] (b::K.Type)
  83         b = tyVar "b" $ VarS varZ
  84
  85 -- | Reduce number of 'Token_Term_App' in given 'AST_Term' by converting them into 'BinTree2'.
  86 --
  87 -- NOTE: 'Token_Term_App' exists only to handle unifix operators applied to arguments.
  88 reduceTeApp :: AST_Term src ss -> AST_Term src ss
  89 reduceTeApp (BinTree2 x y) =
  90         case reduceTeApp x of
  91          BinTree0 Token_Term_App{} `BinTree2` x' -> reduceTeApp x' `BinTree2` reduceTeApp y
  92          _ -> reduceTeApp x `BinTree2` reduceTeApp y
  93 reduceTeApp (BinTree0 (Token_Term_Abst src n ty te)) = BinTree0 $ Token_Term_Abst src n ty (reduceTeApp te)
  94 reduceTeApp (BinTree0 (Token_Term_Let  src n bo te)) = BinTree0 $ Token_Term_Let  src n (reduceTeApp bo) (reduceTeApp te)
  95 reduceTeApp x@BinTree0{} = x
  96
  97 -- * Type 'CtxTy'
  98 -- | /Typing context/
  99 -- accumulating at each /lambda abstraction/
 100 -- the 'Type' of the introduced variable.
 101 -- It is built top-down from the closest
 102 -- including /lambda abstraction/ to the farest.
 103 data CtxTy src (ts::[K.Type]) where
 104         CtxTyZ :: CtxTy src '[]
 105         CtxTyS :: NameTe
 106                -> Type  src '[] t
 107                -> CtxTy src ts
 108                -> CtxTy src (t ': ts)
 109 infixr 5 `CtxTyS`
 110
 111 appendCtxTy
 112  :: CtxTy src ts0
 113  -> CtxTy src ts1
 114  -> CtxTy src (ts0 ++ ts1)
 115 appendCtxTy CtxTyZ c          = c
 116 appendCtxTy (CtxTyS n t c) c' = CtxTyS n t $ appendCtxTy c c'
 117
 118 -- * Type 'Error_Term'
 119 data Error_Term src
 120  =   Error_Term_unknown NameTe
 121  |   Error_Term_polymorphic (TypeVT src)
 122  |   Error_Term_qualified (TypeVT src)
 123  |   Error_Term_Type (Error_Type src)
 124  |   Error_Term_Beta (Error_Beta src)
 125  {-   Error_Term_Con_Type (Con_Type src ss) -}
 126  {-   Error_Term_Con_Kind (Con_Kind src) -}
 127  deriving (Eq, Show)
 128 instance Inj_Error (Error_Type src) (Error_Term src) where
 129         inj_Error = Error_Term_Type
 130 instance Inj_Error (Error_Beta src) (Error_Term src) where
 131         inj_Error = Error_Term_Beta
 132 instance Inj_Error (Con_Kind src) (Error_Term src) where
 133         inj_Error = Error_Term_Type . inj_Error
 134
 135 -- * Type 'SrcTe'
 136 data SrcTe inp ss
 137  =   SrcTe_Less
 138  |   SrcTe_Input    (Span inp)
 139  |   SrcTe_AST_Term (AST_Term (SrcTe inp ss) ss)
 140  |   SrcTe_AST_Type (AST_Type (SrcTe inp ss))
 141  |   SrcTe_Kind     (KindK    (SrcTe inp ss))
 142  |   SrcTe_Type     (TypeVT   (SrcTe inp ss))
 143  |   SrcTe_Term
 144  deriving (Eq, Show)
 145
 146 type instance Source_Input (SrcTe inp ss) = inp
 147
 148 instance Source (SrcTe inp ss) where
 149         noSource = SrcTe_Less
 150 instance Inj_Source (Span inp) (SrcTe inp ss) where
 151         inj_Source = SrcTe_Input
 152 instance Inj_Source (AST_Term (SrcTe inp ss) ss) (SrcTe inp ss) where
 153         inj_Source = SrcTe_AST_Term
 154 instance Inj_Source (AST_Type (SrcTe inp ss)) (SrcTe inp ss) where
 155         inj_Source = SrcTe_AST_Type
 156 instance Inj_Source (KindK (SrcTe inp ss)) (SrcTe inp ss) where
 157         inj_Source = SrcTe_Kind
 158 instance Inj_Source (TypeVT (SrcTe inp ss)) (SrcTe inp ss) where
 159         inj_Source = SrcTe_Type