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 -- * Type 'ReadTerm'
  15 -- | Convenient type alias for 'readTerm' and related functions.
  16 type ReadTerm src ss ts =
  17  Source src =>
  18  SourceInj (TypeVT src) src =>
  19  SourceInj (KindK src) src =>
  20  SourceInj (AST_Type src) src =>
  21  Constable (->) =>
  22  Imports NameTy ->
  23  ModulesTy src ->
  24  CtxTy src ts ->
  25  AST_Term src ss ->
  26  Either (Error_Term src) (TermVT src ss ts)
  27
  28 -- | Read a 'TermVT' from and 'AST_Term'.
  29 readTerm :: forall src ss ts. ReadTerm src ss ts
  30 readTerm impsTy modsTy ctxTy ast = do
  31         ts <- go ctxTy `traverse` ast
  32         errorInj `left` betaTerms ts
  33         where
  34         go ::
  35          forall ts'.
  36          CtxTy src ts' ->
  37          Token_Term src ss ->
  38          Either (Error_Term src) (TermVT src ss ts')
  39         go _ts (Token_Term (TermAVT te))  = Right $ TermVT te
  40         go _ts (Token_TermVT te)          = Right $ liftTermVT te
  41         go ts  (Token_Term_Var _src name) = teVar name ts
  42         go _ts (Token_Term_App _src)      = Right $ TermVT teApp
  43         go ts  (Token_Term_Abst _src name_arg ast_ty_arg ast_body) = do
  44                 TypeVT ty_arg <- errorInj `left` readType impsTy modsTy ast_ty_arg
  45                 when_EqKind (kindInj @K.Type) (kindOf ty_arg) $ \Refl ->
  46                         case lenVars ty_arg of
  47                          LenS{} -> Left $ Error_Term_polymorphic $ TypeVT ty_arg
  48                          LenZ | (TypeK qa, TypeK ta) <- unQualTy ty_arg -> do
  49                                 TermVT (Term qr tr (TeSym res)) <- readTerm impsTy modsTy (CtxTyS name_arg ta ts) ast_body
  50                                 let (qa', qr') = appendVars qa qr
  51                                 let (ta', tr') = appendVars ta tr
  52                                 Right $
  53                                         case (proveConstraint qa', proveConstraint qr') of
  54                                          -- NOTE: remove provable Constraints to keep those smaller.
  55                                          (Just Dict, Just Dict) -> TermVT $
  56                                                 Term (noConstraintLen (lenVars tr')) (ta' ~> tr') $
  57                                                 TeSym $ \c -> lam $ \arg -> res (arg `CtxTeS` c)
  58                                          (Just Dict, Nothing) -> TermVT $
  59                                                 Term qr' (ta' ~> tr') $
  60                                                 TeSym $ \c -> lam $ \arg -> res (arg `CtxTeS` c)
  61                                          (Nothing, Just Dict) -> TermVT $
  62                                                 Term qa' (ta' ~> tr') $
  63                                                 TeSym $ \c -> lam $ \arg -> res (arg `CtxTeS` c)
  64                                          (Nothing, Nothing) -> TermVT $
  65                                                 Term (qa' # qr') (ta' ~> tr') $
  66                                                 TeSym $ \c -> lam $ \arg -> res (arg `CtxTeS` c)
  67         go ts (Token_Term_Let _src name ast_arg ast_body) = do
  68                 TermVT (Term qa ta (TeSym arg)) <- readTerm impsTy modsTy ts ast_arg
  69                 case lenVars ta of
  70                  LenS{} -> Left $ Error_Term_polymorphic $ TypeVT (qa #> ta)
  71                  LenZ -> do
  72                         TermVT (Term qr tr (TeSym res)) <- readTerm impsTy modsTy (CtxTyS name ta ts) ast_body
  73                         let (qa', qr') = appendVars qa qr
  74                         let tr' = allocVarsL (lenVars ta) tr
  75                         Right $
  76                                 case (proveConstraint qa', proveConstraint qr') of
  77                                  -- NOTE: remove provable Constraints to keep those smaller.
  78                                  (Just Dict, Just Dict) -> TermVT $
  79                                         Term (noConstraintLen (lenVars tr')) tr' $
  80                                         TeSym $ \c -> let_ (arg c) $ \a -> res (a `CtxTeS` c)
  81                                  (Just Dict, Nothing) -> TermVT $
  82                                         Term qr' tr' $
  83                                         TeSym $ \c -> let_ (arg c) $ \a -> res (a `CtxTeS` c)
  84                                  (Nothing, Just Dict) -> TermVT $
  85                                         Term qa' tr' $
  86                                         TeSym $ \c -> let_ (arg c) $ \a -> res (a `CtxTeS` c)
  87                                  (Nothing, Nothing) -> TermVT $
  88                                         Term (qa' # qr') tr' $
  89                                         TeSym $ \c -> let_ (arg c) $ \a -> res (a `CtxTeS` c)
  90
  91 teVar ::
  92  forall ss src ts.
  93  Source src =>
  94  NameTe -> CtxTy src ts -> Either (Error_Term src) (TermVT src ss ts)
  95 teVar name CtxTyZ = Left $ Error_Term_unknown name
  96 teVar name (CtxTyS n ty _) | n == name =
  97         Right $ TermVT $ Term noConstraint ty $
  98                 TeSym $ \(te `CtxTeS` _) -> te
  99 teVar name (CtxTyS _n _typ ts') = do
 100         TermVT (Term q t (TeSym te)) <- teVar @ss name ts'
 101         Right $ TermVT $ Term q t $
 102                 TeSym $ \(_ `CtxTeS` ts) -> te ts
 103
 104 teApp ::
 105  Source src => Constable (->) =>
 106  Term src ss ts '[Proxy (a::K.Type), Proxy (b::K.Type)] (() #> ((a -> b) -> a -> b))
 107 teApp =
 108         Term noConstraint ((a ~> b) ~> a ~> b) $
 109         TeSym $ const apply
 110         where
 111         a :: Source src => Type src '[Proxy a, Proxy b] (a::K.Type)
 112         a = tyVar "a" $ varZ
 113         b :: Source src => Type src '[Proxy a, Proxy b] (b::K.Type)
 114         b = tyVar "b" $ VarS varZ
 115
 116 -- | Reduce number of 'Token_Term_App' in given 'AST_Term' by converting them into 'BinTree2'.
 117 --
 118 -- NOTE: 'Token_Term_App' exists only to handle unifix operators applied to arguments.
 119 reduceTeApp :: AST_Term src ss -> AST_Term src ss
 120 reduceTeApp (BinTree2 x y) =
 121         case reduceTeApp x of
 122          BinTree0 Token_Term_App{} `BinTree2` x' -> reduceTeApp x' `BinTree2` reduceTeApp y
 123          _ -> reduceTeApp x `BinTree2` reduceTeApp y
 124 reduceTeApp (BinTree0 (Token_Term_Abst src n ty te)) = BinTree0 $ Token_Term_Abst src n ty (reduceTeApp te)
 125 reduceTeApp (BinTree0 (Token_Term_Let  src n bo te)) = BinTree0 $ Token_Term_Let  src n (reduceTeApp bo) (reduceTeApp te)
 126 reduceTeApp x@BinTree0{} = x
 127
 128 -- ** Type 'ReadTermCF'
 129 -- | Like 'ReadTerm', but 'CtxTe'-free.
 130 --
 131 -- Useful in 'readTermWithCtx' to help GHC's type solver, which
 132 -- "Cannot instantiate unification variable with a type involving foralls".
 133 newtype ReadTermCF src ss
 134  =      ReadTermCF
 135  {    unReadTermCF :: forall ts. ReadTerm src ss ts }
 136
 137 -- | Like 'readTerm' but with given context, and no more.
 138 readTermWithCtx ::
 139  Foldable f =>
 140  Source src =>
 141  SourceInj (TypeVT src) src =>
 142  SourceInj (KindK src) src =>
 143  SourceInj (AST_Type src) src =>
 144  Constable (->) =>
 145  f (NameTe, TermT src ss '[] '[]) ->
 146  Imports NameTy ->
 147  ModulesTy src ->
 148  AST_Term src ss ->
 149  Either (Error_Term src) (TermVT src ss '[])
 150 readTermWithCtx env =
 151         readTermWithCtxClose $
 152         readTermWithCtxPush env readTerm
 153
 154 -- | Like 'readTerm' but with given context.
 155 readTermWithCtxPush ::
 156  Foldable f =>
 157  f (NameTe, TermT src ss '[] '[]) ->
 158  (forall ts'. ReadTerm src ss ts') ->
 159  ReadTerm src ss ts
 160 readTermWithCtxPush env readTe =
 161         unReadTermCF $ foldr
 162          (\t (ReadTermCF r) -> ReadTermCF $ readTermWithCtxPush1 t r)
 163          (ReadTermCF readTe) env
 164
 165 -- | Like 'readTerm' but with given 'TermT' pushed onto 'CtxTy' and 'CtxTe'.
 166 readTermWithCtxPush1 ::
 167  (NameTe, TermT src ss '[] '[]) ->
 168  (forall ts'. ReadTerm src ss ts') ->
 169  ReadTerm src ss ts
 170 readTermWithCtxPush1 (n, TermT (Term qn tn (TeSym te_n))) readTe impsTy modsTy ctxTy ast = do
 171         TermVT (Term q t (TeSym te)) <- readTe impsTy modsTy (CtxTyS n (qn #> tn) ctxTy) ast
 172         case proveConstraint qn of
 173          Nothing -> Left $ Error_Term_proofless $ TypeVT qn
 174          Just Dict ->
 175                 Right $ TermVT $ Term q t $ TeSym $ \c ->
 176                         let cte = qual qn $ te_n CtxTeZ in
 177                         te $ cte `CtxTeS` c
 178
 179 -- | Close a 'ReadTerm' context.
 180 readTermWithCtxClose ::
 181  (forall ts'. ReadTerm src ss ts') ->
 182  Source src =>
 183  SourceInj (TypeVT src) src =>
 184  SourceInj (KindK src) src =>
 185  SourceInj (AST_Type src) src =>
 186  Constable (->) =>
 187  Imports NameTy ->
 188  ModulesTy src ->
 189  AST_Term src ss ->
 190  Either (Error_Term src) (TermVT src ss '[])
 191 readTermWithCtxClose readTe impsTy modsTy = readTe impsTy modsTy CtxTyZ
 192
 193 -- * Type 'CtxTy'
 194 -- | /Typing context/
 195 -- accumulating at each /lambda abstraction/
 196 -- the 'Type' of the introduced variable.
 197 -- It is built top-down from the closest
 198 -- including /lambda abstraction/ to the farest.
 199 -- It determines the 'Type's of 'CtxTe'.
 200 data CtxTy src (ts::[K.Type]) where
 201         CtxTyZ :: CtxTy src '[]
 202         CtxTyS :: NameTe
 203                -> Type  src '[] t
 204                -> CtxTy src ts
 205                -> CtxTy src (t ': ts)
 206 infixr 5 `CtxTyS`
 207
 208 appendCtxTy ::
 209  CtxTy src ts0 ->
 210  CtxTy src ts1 ->
 211  CtxTy src (ts0 ++ ts1)
 212 appendCtxTy CtxTyZ c          = c
 213 appendCtxTy (CtxTyS n t c) c' = CtxTyS n t $ appendCtxTy c c'
 214
 215 -- * Type 'Error_Term'
 216 data Error_Term src
 217  =   Error_Term_unknown NameTe
 218  |   Error_Term_polymorphic (TypeVT src)
 219  |   Error_Term_qualified   (TypeVT src)
 220  |   Error_Term_proofless   (TypeVT src)
 221  |   Error_Term_Type (Error_Type src)
 222  |   Error_Term_Beta (Error_Beta src)
 223  {-   Error_Term_Con_Type (Con_Type src ss) -}
 224  {-   Error_Term_Con_Kind (Con_Kind src) -}
 225  deriving (Eq, Show)
 226 instance ErrorInj (Error_Type src) (Error_Term src) where
 227         errorInj = Error_Term_Type
 228 instance ErrorInj (Error_Beta src) (Error_Term src) where
 229         errorInj = Error_Term_Beta
 230 instance ErrorInj (Con_Kind src) (Error_Term src) where
 231         errorInj = Error_Term_Type . errorInj
 232
 233 -- * Type 'SrcTe'
 234 -- | A 'Source' usable when using 'readTerm'.
 235 data SrcTe inp ss
 236  =   SrcTe_Less
 237  |   SrcTe_Input    (Span inp)
 238  |   SrcTe_AST_Term (AST_Term (SrcTe inp ss) ss)
 239  |   SrcTe_AST_Type (AST_Type (SrcTe inp ss))
 240  |   SrcTe_Kind     (KindK    (SrcTe inp ss))
 241  |   SrcTe_Type     (TypeVT   (SrcTe inp ss))
 242  |   SrcTe_Term
 243  deriving (Eq, Show)
 244
 245 type instance Source_Input (SrcTe inp ss) = inp
 246
 247 instance Source (SrcTe inp ss) where
 248         noSource = SrcTe_Less
 249 instance SourceInj (Span inp) (SrcTe inp ss) where
 250         sourceInj = SrcTe_Input
 251 instance SourceInj (AST_Term (SrcTe inp ss) ss) (SrcTe inp ss) where
 252         sourceInj = SrcTe_AST_Term
 253 instance SourceInj (AST_Type (SrcTe inp ss)) (SrcTe inp ss) where
 254         sourceInj = SrcTe_AST_Type
 255 instance SourceInj (KindK (SrcTe inp ss)) (SrcTe inp ss) where
 256         sourceInj = SrcTe_Kind
 257 instance SourceInj (TypeVT (SrcTe inp ss)) (SrcTe inp ss) where
 258         sourceInj = SrcTe_Type