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