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