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