src/Symantic/Syntaxes.hs

   1 {-# LANGUAGE AllowAmbiguousTypes #-}
   2 {-# LANGUAGE ConstraintKinds #-}
   3 {-# LANGUAGE DataKinds #-}
   4 {-# LANGUAGE PolyKinds #-}
   5 {-# LANGUAGE QuantifiedConstraints #-}
   6 {-# LANGUAGE RankNTypes #-}
   7 {-# LANGUAGE UndecidableInstances #-}
   8 {-# LANGUAGE UndecidableSuperClasses #-}
   9 {-# LANGUAGE ViewPatterns #-}
  10 {-# LANGUAGE NoMonomorphismRestriction #-}
  11 {-# OPTIONS_GHC -Wno-missing-signatures #-}
  12 {-# OPTIONS_GHC -Wno-orphans #-}
  13
  14 -- {-# OPTIONS_GHC -Wno-monomorphism-restriction #-}
  15
  16 module Symantic.Syntaxes where
  17
  18 import Data.Either (Either (..))
  19 import Data.Eq (Eq (..))
  20 import Data.Function (fix, ($))
  21 import Data.Int (Int)
  22 import Data.Kind (Type)
  23 import Data.Maybe (Maybe (..))
  24 import Data.Monoid (Monoid (..))
  25 import Data.Semigroup (Semigroup (..))
  26 import Data.Void (Void)
  27 import Text.Show (Show (..))
  28 import Type.Reflection (eqTypeRep, typeRep, (:~~:) (..))
  29 import Prelude (error)
  30
  31 import Symantic
  32 import Symantic.Typer ()
  33
  34 parse ::
  35   forall syns meta finalSyns.
  36   finalSyns ~ (UnAbstractable ': syns) =>
  37   Show meta =>
  38   Monoid meta =>
  39   FinalSyntax finalSyns (Semantics finalSyns) =>
  40   -- (forall sem. FinalSyntax finalSyns sem => Constable sem) =>
  41   Parsers finalSyns finalSyns meta =>
  42   TermAST meta ->
  43   Either ErrMsg (TermVT finalSyns meta '[])
  44 parse ast = unParser (fix parsersA ast) CtxTyZ
  45   where
  46     -- UnAbstractable is always needed
  47     parsersA final (BinTree2 fT aT) = Parser $ \ctx -> do
  48       let Parser fE = final fT
  49       TermVT fTy (f :: OTerm syn fVS a2b) <- fE ctx
  50       case fTy of
  51         -- FUN iTy bTy -> do
  52         TyApp
  53           { tyAppFun =
  54             TyApp
  55               { tyAppFun = TyConst{tyConst = Const{constType = eqTypeRep (typeRep @(->)) -> Just HRefl}}
  56               , tyAppArg = iTy
  57               }
  58           , tyAppArg = bTy
  59           } -> do
  60             let Parser aE = final aT
  61             TermVT aTy (a :: OTerm syn aVS a) <- aE ctx
  62             let (iTy', aTy') = appendVars iTy aTy
  63             case eqTy iTy' aTy' of
  64               Nothing -> Left "TypeError: UnAbstractable: eqTy"
  65               Just HRefl -> Right $ TermVT bTy $ f `appOTerm` a
  66         _ -> Left "TypeError: UnAbstractable: fTy is not a function"
  67     parsersA final (BinTree0 e) = parsers @finalSyns @finalSyns @meta final e
  68
  69 -- * Class 'Parsers'
  70 class Parsers syns finalSyns meta where
  71   parsers :: OpenParser finalSyns meta
  72 instance Parsers '[] finalSyns meta where
  73   parsers _final ast = Parser $ \_ctx -> Left $ "Invalid tree: " <> show ast
  74 instance
  75   ( ParserFor syn finalSyns meta
  76   , Parsers syns finalSyns meta
  77   ) =>
  78   Parsers (syn ': syns) finalSyns meta
  79   where
  80   parsers final = parserFor @syn @finalSyns (parsers @syns @finalSyns final) final
  81
  82 -- ** Type 'OpenParser'
  83 type OpenParser syn meta =
  84   Show meta =>
  85   Monoid meta =>
  86   {-final-} (TermAST meta -> Parser syn meta) ->
  87   TokenTerm meta ->
  88   Parser syn meta
  89
  90 -- ** Class 'ParserFor'
  91 class ParserFor syn finalSyn meta where
  92   parserFor ::
  93     {-next-} (TokenTerm meta -> Parser finalSyn meta) ->
  94     OpenParser finalSyn meta
  95 instance
  96   ( FinalSyntax finalSyn (Semantics finalSyn)
  97   ) =>
  98   ParserFor UnAbstractable finalSyn meta
  99   where
 100   parserFor next _final = next
 101 instance
 102   ( FinalSyntax finalSyn (Semantics finalSyn)
 103   , forall sem. FinalSyntax finalSyn sem => Constable sem
 104   , forall sem. FinalSyntax finalSyn sem => UnAbstractable sem
 105   ) =>
 106   ParserFor (Abstractable meta) finalSyn meta
 107   where
 108   parserFor _next _final (TokenTermVar vN) = Parser go
 109     where
 110       go :: forall vs. CtxTy meta vs Void -> Either ErrMsg (TermVT finalSyn meta vs)
 111       go CtxTyZ = Left $ "Error_Term_unknown: " <> vN
 112       go (CtxTyS n ty _) | n == vN = Right $ TermVT ty $ V
 113       go (CtxTyS _n _typ tys) = do
 114         TermVT ty ot <- go tys
 115         Right $ TermVT ty $ W ot
 116   parserFor _next final (TokenTermAbst argName (TyT (aTy :: Ty meta '[] a)) bT) =
 117     Parser $ \ctx ->
 118       case eqTy typeTy (kindOf aTy) of
 119         Nothing -> Left "TypeError: Abstractable: TokenTermAbst"
 120         Just HRefl -> do
 121           let Parser bE = final bT
 122           TermVT bTy (b :: OTerm syn bVS b) <- bE (CtxTyS argName aTy ctx)
 123           let aTy' = allocVarsR (lenVar bTy) aTy
 124           Right $
 125             TermVT (aTy' ~> bTy) $
 126               case b of
 127                 E d -> E (constK .@ d)
 128                 V -> E constI
 129                 W e -> E constK `appOTerm` e
 130                 N e -> e
 131     where
 132       typeTy = TyConst{tyConst = Const{constType = typeRep @Type, constMeta = mempty :: meta}, tyConstLen = LenZ}
 133   parserFor next _final e = next e
 134 instance
 135   ( FinalSyntax finalSyn (Semantics finalSyn)
 136   , forall sem. FinalSyntax finalSyn sem => Addable sem
 137   ) =>
 138   ParserFor Addable finalSyn meta
 139   where
 140   parserFor next _final = \case
 141     TokenTermAtom s
 142       | Right (i :: Int) <- safeRead s ->
 143           Parser $ \ctx -> Right $ TermVT (tyOf @Int (mempty :: meta) (lenVar ctx)) $ E $ Semantics @_ @Int $ lit i
 144     TokenTermAtom "neg" -> Parser $ \_ctx ->
 145       Right $ TermVT (tyOf (mempty :: meta) LenZ) $ E neg
 146     TokenTermAtom "add" -> Parser $ \_ctx ->
 147       Right $ TermVT (tyOf (mempty :: meta) LenZ) $ E add
 148     ast -> next ast
 149 instance
 150   () =>
 151   -- syn (Semantics syn)
 152   -- , forall sem. syn sem => Constable sem
 153   ParserFor Constable syns meta
 154   where
 155   parserFor next _final = next
 156
 157 --
 158 -- Parsing
 159 --
 160
 161 -- tree0Parser :: (forall sem. syn sem => Addable sem, syn (Semantics syn)) => Either ErrMsg (Semantics syn Int)
 162 -- tree0Parser = unParser $ parse tree0Print
 163
 164 -- parseMulable ::
 165 --  forall syn meta.
 166 --  ( forall sem. syn sem => Mulable sem
 167 --  , forall sem. syn sem => Addable sem
 168 --  , syn (Semantics syn)
 169 --  ) =>
 170 --  Monoid meta =>
 171 --  Show meta =>
 172 --  (TermAST meta -> Parser syn meta) ->
 173 --  TermAST meta -> Parser syn meta
 174 -- parseMulable final (BinTree2 (BinTree2 (BinTree0 (TokenTermAtom "mul")) aT) bT) =
 175 --  Parser $ \ctx -> do
 176 --    case (final aT, final bT) of
 177 --      (Parser aE, Parser bE) -> do
 178 --        TermVT aTy (Semantics a :: Semantics syn a) <- aE ctx
 179 --        case eqTy aTy TyConst{tyConst = Const{constType = typeRep @Int, constMeta = mempty::meta}, tyConstLen = lenVar aTy} of
 180 --          Nothing -> Left "TypeError: Mulable 1"
 181 --          Just HRefl -> do
 182 --            TermVT bTy (Semantics b :: Semantics syn b) <- bE ctx
 183 --            case eqTy bTy TyConst{tyConst = Const{constType = typeRep @Int, constMeta = mempty::meta}, tyConstLen = lenVar bTy} of
 184 --              Nothing -> Left "TypeError: Mulable 2"
 185 --              Just HRefl -> do
 186 --                Right $ TermVT aTy (Semantics @_ @a $ mul a b)
 187 -- parseMulable final t = parseAddable final t
 188
 189 --
 190 -- Printing
 191 --
 192
 193 printConst n = Printer (BinTree0 (TokenTermAtom n))
 194
 195 instance Constable (Printer meta) where
 196   constI = printConst "id"
 197   constK = printConst "const"
 198   constS = printConst "(<*>)"
 199   constB = printConst "(.)"
 200   constC = printConst "flip"
 201 instance Addable (Printer meta) where
 202   lit n = Printer $ BinTree0 (TokenTermAtom (show n))
 203   neg = printConst "neg"
 204   add = printConst "add"
 205 instance Mulable (Printer meta) where
 206   mul = print2 "mul"
 207 instance UnAbstractable (Printer meta) where
 208   Printer f .@ Printer a = Printer $ BinTree2 f a
 209 instance (Monoid meta) => Abstractable meta (Printer meta) where
 210   lam aTy (f :: Printer meta a -> Printer meta b) =
 211     Printer $
 212       BinTree0
 213         ( TokenTermAbst
 214             "x"
 215             (TyT aTy) -- (TyT (tyOf @a mempty LenZ))
 216             (unPrinter (f (Printer (BinTree0 (TokenTermVar "x")))))
 217         )
 218
 219 -- * Type 'Syntaxes'
 220 type Syntaxes meta = '[Abstractable meta, Addable, Constable]
 221
 222 -- tree0 = lit 0
 223 tree0 = add .@ lit 8 .@ (neg .@ (add .@ lit 1 .@ lit 2))
 224
 225 -- tree1 = mul (add (lit 8) (neg (add (lit 1) (lit 2)))) (lit 2)
 226 tree2 = lam (typeOf @()) (\(x :: sem Int) -> add .@ x .@ lit 0)
 227 tree3 = lam (typeOf @()) (\(x :: sem Int) -> add .@ x .@ x)
 228 tree0Print = print tree0
 229
 230 -- tree1Print = print tree1
 231 tree2Print = print tree2
 232 tree3Print = print tree3
 233
 234 tree0ParsePrint :: TermAST ()
 235 tree0ParsePrint = case parse @(Syntaxes ()) @() tree0Print of
 236   Left e -> error e
 237   Right (TermVT _ty (runOTerm -> Semantics sem)) -> print sem
 238
 239 -- tree1ParsePrint :: TermAST ()
 240 -- tree1ParsePrint = case parse @(FinalSyntaxes ()) @() tree1Print of
 241 --  Left e -> error e
 242 --  Right (TermVT _ty (runOTerm -> Semantics sem)) -> print sem
 243
 244 tree2ParsePrint :: TermAST ()
 245 tree2ParsePrint = case parse @(Syntaxes ()) @() tree2Print of
 246   Left e -> error e
 247   Right (TermVT _ty (runOTerm -> Semantics sem)) -> print sem
 248
 249 tree3ParsePrint :: TermAST ()
 250 tree3ParsePrint = case parse @(Syntaxes ()) @() tree3Print of
 251   Left e -> error e
 252   Right (TermVT _ty (runOTerm -> Semantics sem)) -> print sem