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