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