src/Symantic/Syntaxes.hs

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