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