src/Symantic/Syntaxes.hs

   1 {-# LANGUAGE AllowAmbiguousTypes #-}
   2 {-# LANGUAGE ConstraintKinds #-}
   3 {-# LANGUAGE DataKinds #-}
   4 {-# LANGUAGE PolyKinds #-}
   5 {-# LANGUAGE QuantifiedConstraints #-}
   6 {-# LANGUAGE RankNTypes #-}
   7 {-# LANGUAGE UndecidableInstances #-}
   8 {-# LANGUAGE UndecidableSuperClasses #-}
   9 {-# LANGUAGE ViewPatterns #-}
  10 {-# LANGUAGE NoMonomorphismRestriction #-}
  11 {-# OPTIONS_GHC -Wno-missing-signatures #-}
  12 {-# OPTIONS_GHC -Wno-orphans #-}
  13
  14 -- {-# OPTIONS_GHC -Wno-monomorphism-restriction #-}
  15
  16 module Symantic.Syntaxes where
  17
  18 import Control.Arrow (left)
  19 import Data.Either (Either (..))
  20 import Data.Eq (Eq (..))
  21 import Data.Function (fix, ($))
  22 import Data.Int (Int)
  23 import Data.Maybe (Maybe (..))
  24 import Data.Monoid (Monoid (..))
  25 import Data.Semigroup (Semigroup (..))
  26 import Data.Void (Void)
  27 import Symantic.Syntaxes.Classes (Unabstractable (..))
  28 import Text.Show (Show (..))
  29 import Type.Reflection (eqTypeRep, typeRep, (:~~:) (..))
  30 import Prelude (error)
  31
  32 import Symantic
  33 import Symantic.Typer ()
  34
  35 parse ::
  36   forall syns meta finalSyns.
  37   finalSyns ~ (Unabstractable ': Constable ': syns) =>
  38   Show meta =>
  39   Monoid meta =>
  40   Syntaxes finalSyns (ForallSemantic finalSyns) =>
  41   Parsers finalSyns finalSyns meta =>
  42   TermAST meta ->
  43   Either ErrMsg (TermVT finalSyns meta '[])
  44 parse ast = unParser (fix parsersA ast) CtxTyZ
  45   where
  46     -- Unabstractable and Constable are always required.
  47     parsersA final (BinTree2 fT aT) = Parser $ \ctx -> do
  48       let Parser fE = final fT
  49       TermVT fTy (f :: OpenTerm finalSyns fVS a2b) <- fE ctx
  50       let Parser aE = final aT
  51       TermVT aTy (a :: OpenTerm finalSyns aVS a) <- aE ctx
  52       let (fTy', aTy') = appendVars fTy aTy
  53       case fTy' of
  54         -- FUN faTy bTy -> do
  55         TyApp
  56           { tyAppFun =
  57             TyApp
  58               { tyAppFun = TyConst{tyConst = Const{constType = eqTypeRep (typeRep @(->)) -> Just HRefl}}
  59               , tyAppArg = faTy
  60               }
  61           , tyAppArg = bTy
  62           } -> do
  63             mgu <- show `left` unifyType mempty faTy aTy'
  64             let faTy' = subst @Ty mgu faTy
  65             let aTy'' = subst @Ty mgu aTy'
  66             case eqTy faTy' aTy'' of
  67               Nothing ->
  68                 Left $
  69                   "TypeError: Unabstractable: eqTy: "
  70                     <> "\n faTy'="
  71                     <> show faTy
  72                     <> "\n aTy'="
  73                     <> show aTy''
  74               Just HRefl -> Right $ TermVT bTy $ f .@ a
  75         _ -> Left "TypeError: Unabstractable: fTy is not a function"
  76     parsersA final (BinTree0 e) = parsers @finalSyns @finalSyns @meta final e
  77
  78 -- * Class 'Parsers'
  79 class Parsers syns finalSyns meta where
  80   parsers :: OpenParser finalSyns meta
  81 instance Parsers '[] finalSyns meta where
  82   parsers _final ast = Parser $ \_ctx -> Left $ "Invalid tree: " <> show ast
  83 instance
  84   ( TokenParser syn finalSyns meta
  85   , Parsers syns finalSyns meta
  86   ) =>
  87   Parsers (syn ': syns) finalSyns meta
  88   where
  89   parsers final = tokenParser @syn @finalSyns (parsers @syns @finalSyns final) final
  90
  91 -- ** Type 'OpenParser'
  92 type OpenParser syns meta =
  93   Show meta =>
  94   Monoid meta =>
  95   {-final-} (TermAST meta -> Parser syns meta) ->
  96   TokenTerm meta ->
  97   Parser syns meta
  98
  99 -- ** Class 'TokenParser'
 100 class TokenParser syn finalSyn meta where
 101   tokenParser ::
 102     {-next-} (TokenTerm meta -> Parser finalSyn meta) ->
 103     OpenParser finalSyn meta
 104 instance
 105   ( Syntaxes finalSyn (ForallSemantic finalSyn)
 106   ) =>
 107   TokenParser Unabstractable finalSyn meta
 108   where
 109   tokenParser next _final = next
 110 instance
 111   ( Syntaxes finalSyn (ForallSemantic finalSyn)
 112   , forall sem. Syntaxes finalSyn sem => Constable sem
 113   , forall sem. Syntaxes finalSyn sem => Unabstractable sem
 114   ) =>
 115   TokenParser (Abstractable meta) finalSyn meta
 116   where
 117   tokenParser _next _final (TokenTermVar vN) = Parser go
 118     where
 119       go :: forall vs. CtxTy meta vs Void -> Either ErrMsg (TermVT finalSyn meta vs)
 120       go CtxTyZ = Left $ "Error_Term_unknown: " <> vN
 121       go (CtxTyS n ty _) | n == vN = Right $ TermVT ty $ V
 122       go (CtxTyS _n _typ tys) = do
 123         TermVT ty ot <- go tys
 124         Right $ TermVT ty $ W ot
 125   tokenParser _next final (TokenTermAbst argName (TyT (aTy :: Ty meta '[] a)) bT) =
 126     Parser $ \ctx ->
 127       case eqTy (typeTy @meta) (kindOf aTy) of
 128         Nothing -> Left "TypeError: Abstractable: TokenTermAbst"
 129         Just HRefl -> do
 130           let Parser bE = final bT
 131           TermVT bTy (b :: OpenTerm syn bVS b) <- bE (CtxTyS argName aTy ctx)
 132           let aTy' = allocVarsR (lenVar bTy) aTy
 133           Right $
 134             TermVT (aTy' ~> bTy) $
 135               case b of
 136                 E d -> E (constK .@ d)
 137                 V -> E constI
 138                 W e -> E constK `appOpenTerm` e
 139                 N e -> e
 140   tokenParser next _final e = next e
 141 instance
 142   ( Syntaxes finalSyn (ForallSemantic finalSyn)
 143   , forall sem. Syntaxes finalSyn sem => Addable sem
 144   ) =>
 145   TokenParser Addable finalSyn meta
 146   where
 147   tokenParser next _final = \case
 148     TokenTermAtom s
 149       | Right (i :: Int) <- safeRead s ->
 150           Parser $ \ctx -> Right $ TermVT (inferTy @_ @Int (mempty :: meta) (lenVar ctx)) $ E $ ForallSemantic @_ @Int $ lit i
 151     TokenTermAtom "neg" -> Parser $ \_ctx ->
 152       Right $ TermVT (intTy ~> intTy) $ E neg
 153     TokenTermAtom "add" -> Parser $ \_ctx ->
 154       Right $ TermVT (intTy ~> intTy ~> intTy) $ E add
 155     ast -> next ast
 156 instance
 157   ( Syntaxes syns (ForallSemantic syns)
 158   , forall sem. Syntaxes syns sem => Constable sem
 159   ) =>
 160   TokenParser Constable syns meta
 161   where
 162   tokenParser next _final = \case
 163     TokenTermAtom "id" -> Parser $ \_ctx ->
 164       Right
 165         $ TermVT
 166           (a ~> a)
 167         $ E constI
 168       where
 169         a = TyVar{tyVar = VarZ{varZKind = typeTy, varZNext = LenZ, varZMeta = (mempty :: meta)}, tyVarName = "a"}
 170     TokenTermAtom "(<*>)" -> Parser $ \_ctx ->
 171       Right
 172         $ TermVT
 173           ((a ~> b ~> c) ~> (a ~> b) ~> a ~> c)
 174         $ E constS
 175       where
 176         a = TyVar{tyVar = VarZ{varZKind = typeTy, varZNext = LenS $ LenS $ LenZ, varZMeta = (mempty :: meta)}, tyVarName = "a"}
 177         b = TyVar{tyVar = VarS $ VarZ{varZKind = typeTy, varZNext = LenS $ LenZ, varZMeta = (mempty :: meta)}, tyVarName = "b"}
 178         c = TyVar{tyVar = VarS $ VarS $ VarZ{varZKind = typeTy, varZNext = LenZ, varZMeta = (mempty :: meta)}, tyVarName = "c"}
 179     tok -> next tok
 180
 181 intTy :: Monoid meta => Ty meta '[] Int
 182 intTy = TyConst{tyConst = Const{constType = typeRep @Int, constMeta = mempty}, tyConstLen = LenZ}
 183
 184 class Addable sem where
 185   lit :: Int -> sem Int
 186   neg :: sem (Int -> Int)
 187   add :: sem (Int -> Int -> Int)
 188
 189 class Mulable sem where
 190   mul :: sem Int -> sem Int -> sem Int
 191 instance (forall sem. Syntaxes syn sem => Addable sem) => Addable (ForallSemantic syn) where
 192   lit n = ForallSemantic (lit n)
 193   neg = ForallSemantic neg
 194   add = ForallSemantic add
 195 instance (forall sem. Syntaxes syn sem => Mulable sem) => Mulable (ForallSemantic syn) where
 196   mul (ForallSemantic a) (ForallSemantic b) = ForallSemantic (mul a b)
 197
 198 --
 199 -- Parsing
 200 --
 201
 202 -- tree0Parser :: (forall sem. syn sem => Addable sem, syn (ForallSemantic syn)) => Either ErrMsg (ForallSemantic syn Int)
 203 -- tree0Parser = unParser $ parse tree0Print
 204
 205 -- parseMulable ::
 206 --  forall syn meta.
 207 --  ( forall sem. syn sem => Mulable sem
 208 --  , forall sem. syn sem => Addable sem
 209 --  , syn (ForallSemantic syn)
 210 --  ) =>
 211 --  Monoid meta =>
 212 --  Show meta =>
 213 --  (TermAST meta -> Parser syn meta) ->
 214 --  TermAST meta -> Parser syn meta
 215 -- parseMulable final (BinTree2 (BinTree2 (BinTree0 (TokenTermAtom "mul")) aT) bT) =
 216 --  Parser $ \ctx -> do
 217 --    case (final aT, final bT) of
 218 --      (Parser aE, Parser bE) -> do
 219 --        TermVT aTy (ForallSemantic a :: ForallSemantic syn a) <- aE ctx
 220 --        case eqTy aTy TyConst{tyConst = Const{constType = typeRep @Int, constMeta = mempty::meta}, tyConstLen = lenVar aTy} of
 221 --          Nothing -> Left "TypeError: Mulable 1"
 222 --          Just HRefl -> do
 223 --            TermVT bTy (ForallSemantic b :: ForallSemantic syn b) <- bE ctx
 224 --            case eqTy bTy TyConst{tyConst = Const{constType = typeRep @Int, constMeta = mempty::meta}, tyConstLen = lenVar bTy} of
 225 --              Nothing -> Left "TypeError: Mulable 2"
 226 --              Just HRefl -> do
 227 --                Right $ TermVT aTy (ForallSemantic @_ @a $ mul a b)
 228 -- parseMulable final t = parseAddable final t
 229
 230 --
 231 -- Printing
 232 --
 233
 234 printConst n = Printer (BinTree0 (TokenTermAtom n))
 235
 236 instance Constable (Printer meta) where
 237   constI = printConst "id"
 238   constK = printConst "const"
 239   constS = printConst "(<*>)"
 240   constB = printConst "(.)"
 241   constC = printConst "flip"
 242 instance Addable (Printer meta) where
 243   lit n = Printer $ BinTree0 (TokenTermAtom (show n))
 244   neg = printConst "neg"
 245   add = printConst "add"
 246 instance Mulable (Printer meta) where
 247   mul = print2 "mul"
 248 instance Unabstractable (Printer meta) where
 249   Printer f .@ Printer a = Printer $ BinTree2 f a
 250 instance (Monoid meta) => Abstractable meta (Printer meta) where
 251   lam aTy (f :: Printer meta a -> Printer meta b) =
 252     Printer $
 253       BinTree0
 254         ( TokenTermAbst
 255             "x"
 256             (TyT aTy) -- (TyT (inferTy @a mempty LenZ))
 257             (unPrinter (f (Printer (BinTree0 (TokenTermVar "x")))))
 258         )
 259
 260 -- * Type 'FinalSyntaxes'
 261 type FinalSyntaxes meta = '[Abstractable meta, Addable]
 262
 263 -- tree0 = lit 0
 264 tree0 = add .@ lit 8 .@ (neg .@ (add .@ lit 1 .@ lit 2))
 265
 266 -- tree1 = mul (add (lit 8) (neg (add (lit 1) (lit 2)))) (lit 2)
 267 tree2 = lam (typeOf @()) (\(x :: sem Int) -> add .@ x .@ lit 0)
 268 tree3 = lam (typeOf @()) (\(x :: sem Int) -> add .@ x .@ x)
 269 tree4 = constS .@ add .@ constI
 270 tree0Print = print tree0
 271
 272 -- tree1Print = print tree1
 273 tree2Print = print tree2
 274 tree3Print = print tree3
 275 tree4Print = print tree4
 276
 277 tree0ParsePrint :: TermAST ()
 278 tree0ParsePrint = case parse @(FinalSyntaxes ()) @() tree0Print of
 279   Left e -> error e
 280   Right (TermVT _ty (runOpenTerm -> ForallSemantic sem)) -> print sem
 281
 282 -- tree1ParsePrint :: TermAST ()
 283 -- tree1ParsePrint = case parse @(FinalSyntaxes ()) @() tree1Print of
 284 --  Left e -> error e
 285 --  Right (TermVT _ty (runOpenTerm -> ForallSemantic sem)) -> print sem
 286
 287 tree2ParsePrint :: TermAST ()
 288 tree2ParsePrint = case parse @(FinalSyntaxes ()) @() tree2Print of
 289   Left e -> error e
 290   Right (TermVT _ty (runOpenTerm -> ForallSemantic sem)) -> print sem
 291
 292 tree3ParsePrint :: TermAST ()
 293 tree3ParsePrint = case parse @(FinalSyntaxes ()) @() tree3Print of
 294   Left e -> error e
 295   Right (TermVT _ty (runOpenTerm -> ForallSemantic sem)) -> print sem
 296
 297 tree3ParsePrint' :: TermAST ()
 298 tree3ParsePrint' = case parse @(FinalSyntaxes ()) @() tree3ParsePrint of
 299   Left e -> error e
 300   Right (TermVT _ty (runOpenTerm -> ForallSemantic sem)) -> print sem
 301
 302 tree4ParsePrint :: TermAST ()
 303 tree4ParsePrint = case parse @(FinalSyntaxes ()) @() tree4Print of
 304   Left e -> error e
 305   Right (TermVT _ty (runOpenTerm -> ForallSemantic sem)) -> print sem