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       go (CtxTyS n ty _) | n == varName = Right $ TermVT ty V
 139       go (CtxTyS _n _typ tys) = do
 140         TermVT ty ot <- go tys
 141         Right $ TermVT ty (W ot)
 142   tokenParser _next final (TokenTermAbst argName (TyT (argTy :: Ty prov '[] a)) bT) =
 143     Parser $ \ctx ->
 144       case eqTy (monoTy @Type @prov) (kindOf argTy) of
 145         Nothing -> Left $ perSyntax $ ErrorParserAbstractableNotAType (TyVT argTy)
 146         Just HRefl -> do
 147           TermVT resTy (res :: OpenTerm syn bVS res) <-
 148             unParser (final bT) (CtxTyS argName argTy ctx)
 149           let argTy' = allocVarsR (lenVar resTy) argTy
 150           Right $
 151             TermVT (argTy' ~> resTy) $
 152               case res of
 153                 E d -> E (Sym.const .@ d)
 154                 V -> E Sym.id
 155                 W e -> E Sym.const `appOpenTerm` e
 156                 N e -> e
 157   tokenParser next _final e = next e
 158 instance
 159   ( Syntaxes finalSyns (Forall finalSyns)
 160   , forall sem. Syntaxes finalSyns sem => Addable sem
 161   ) =>
 162   TokenParser Addable finalSyns prov
 163   where
 164   tokenParser next _final = \case
 165     TokenTermAtom s
 166       | Right (i :: Int) <- safeRead s ->
 167           Parser $ \ctx ->
 168             Right
 169               $ TermVT
 170                 (tyOfTypeRep (lenVar ctx) (typeRep @Int))
 171               $ E
 172               $ Forall @_ @Int
 173               $ lit i
 174     TokenTermAtom "neg" -> Parser $ \_ctx ->
 175       Right $ TermVT (monoTy @Int ~> monoTy @Int) $ E neg
 176     TokenTermAtom "add" -> Parser $ \_ctx ->
 177       Right $ TermVT (monoTy @Int ~> monoTy @Int ~> monoTy @Int) $ E add
 178     ast -> next ast
 179 instance
 180   ( Syntaxes syns (Forall syns)
 181   , forall sem. Syntaxes syns sem => Unabstractable sem
 182   ) =>
 183   TokenParser Unabstractable syns prov
 184   where
 185   tokenParser next _final = \case
 186     TokenTermAtom "id" -> Parser $ \_ctx ->
 187       Right $ TermVT (aTy @'[] ~> aTy) $ E Sym.id
 188     TokenTermAtom "(<*>)" -> Parser $ \_ctx ->
 189       Right $
 190         TermVT ((aTy ~> bTy ~> cTy @'[]) ~> (aTy ~> bTy) ~> aTy ~> cTy) $
 191           E Sym.ap
 192     TokenTermAtom "const" -> Parser $ \_ctx ->
 193       Right $ TermVT (aTy ~> bTy @'[] ~> aTy) $ E Sym.const
 194     TokenTermAtom "(.)" -> Parser $ \_ctx ->
 195       Right $ TermVT ((bTy ~> cTy @'[]) ~> (aTy ~> bTy) ~> aTy ~> cTy) $ E (Sym..)
 196     TokenTermAtom "flip" -> Parser $ \_ctx ->
 197       Right $ TermVT ((aTy ~> bTy ~> cTy @'[]) ~> bTy ~> aTy ~> cTy) $ E (Sym.flip)
 198     TokenTermAtom "($)" -> Parser $ \_ctx ->
 199       Right $ TermVT ((aTy ~> bTy @'[]) ~> aTy ~> bTy) $ E (Sym.$)
 200     tok -> next tok
 201
 202 -- * Class 'Addable'
 203 class Addable sem where
 204   lit :: Int -> sem Int
 205   neg :: sem (Int -> Int)
 206   add :: sem (Int -> Int -> Int)
 207 data instance ErrorParser prov Addable
 208   deriving (Show)
 209
 210 -- * Class 'Mulable'
 211 class Mulable sem where
 212   mul :: sem Int -> sem Int -> sem Int
 213 instance (forall sem. Syntaxes syn sem => Addable sem) => Addable (Forall syn) where
 214   lit n = Forall (lit n)
 215   neg = Forall neg
 216   add = Forall add
 217 instance (forall sem. Syntaxes syn sem => Mulable sem) => Mulable (Forall syn) where
 218   mul (Forall a) (Forall b) = Forall (mul a b)
 219
 220 --
 221 -- Parsing
 222 --
 223
 224 -- tree0Parser :: (forall sem. syn sem => Addable sem, syn (Forall syn)) => Either ErrMsg (Forall syn Int)
 225 -- tree0Parser = unParser $ parse tree0Print
 226
 227 -- parseMulable ::
 228 --  forall syn prov.
 229 --  ( forall sem. syn sem => Mulable sem
 230 --  , forall sem. syn sem => Addable sem
 231 --  , syn (Forall syn)
 232 --  ) =>
 233 --  Monoid prov =>
 234 --  Show prov =>
 235 --  (TermAST prov -> Parser syn prov) ->
 236 --  TermAST prov -> Parser syn prov
 237 -- parseMulable final (BinTree2 (BinTree2 (BinTree0 (TokenTermAtom "mul")) aT) bT) =
 238 --  Parser $ \ctx -> do
 239 --    case (final aT, final bT) of
 240 --      (Parser aE, Parser bE) -> do
 241 --        TermVT aTy (Forall a :: Forall syn a) <- aE ctx
 242 --        case eqTy aTy TyConst{tyConst = Const{constType = typeRep @Int, constMeta = mempty::prov}, tyConstLen = lenVar aTy} of
 243 --          Nothing -> Left "TypeError: Mulable 1"
 244 --          Just HRefl -> do
 245 --            TermVT bTy (Forall b :: Forall syn b) <- bE ctx
 246 --            case eqTy bTy TyConst{tyConst = Const{constType = typeRep @Int, constMeta = mempty::prov}, tyConstLen = lenVar bTy} of
 247 --              Nothing -> Left "TypeError: Mulable 2"
 248 --              Just HRefl -> do
 249 --                Right $ TermVT aTy (Forall @_ @a $ mul a b)
 250 -- parseMulable final t = parseAddable final t
 251
 252 --
 253 -- Printing
 254 --
 255
 256 printConst n = Printer (BinTree0 (TokenTermAtom n))
 257
 258 instance Sym.Unabstractable (Printer prov) where
 259   ap = printConst "(<*>)"
 260   const = printConst "const"
 261   id = printConst "id"
 262   (.) = printConst "(.)"
 263   flip = printConst "flip"
 264   ($) = printConst "($)"
 265 instance Addable (Printer prov) where
 266   lit n = Printer $ BinTree0 (TokenTermAtom (show n))
 267   neg = printConst "neg"
 268   add = printConst "add"
 269 instance Mulable (Printer prov) where
 270   mul = print2 "mul"
 271 instance Instantiable (Printer prov) where
 272   Printer f .@ Printer a = Printer $ BinTree2 f a
 273 instance (Monoid prov) => AbstractableTy (Ty prov '[]) (Printer prov) where
 274   lamTy xTy (f :: Printer prov a -> Printer prov b) =
 275     Printer $
 276       BinTree0
 277         ( TokenTermAbst
 278             "x"
 279             (TyT xTy)
 280             (unPrinter (f (Printer (BinTree0 (TokenTermVar "x")))))
 281         )
 282
 283 -- * Type 'FinalSyntaxes'
 284 type FinalSyntaxes prov = '[AbstractableTy (Ty prov '[]), Addable]
 285
 286 -- tree0 = lit 0
 287 tree0 = add .@ lit 8 .@ (neg .@ (add .@ lit 1 .@ lit 2))
 288
 289 -- tree1 = mul (add (lit 8) (neg (add (lit 1) (lit 2)))) (lit 2)
 290 tree2 = fun @() (\x -> add .@ x .@ lit 0)
 291 tree3 = fun @() (\x -> add .@ x .@ x)
 292 tree4 = Sym.ap .@ add .@ Sym.id
 293 tree0Print = print tree0
 294
 295 -- tree1Print = print tree1
 296 tree2Print = print tree2
 297 tree3Print = print tree3
 298 tree4Print = print tree4
 299
 300 tree0ParsePrint :: TermAST ()
 301 tree0ParsePrint = case parse @(FinalSyntaxes ()) @() tree0Print of
 302   Left e -> error $ show e
 303   Right (TermVT _ty (unE -> Forall sem)) -> print sem
 304
 305 -- tree1ParsePrint :: TermAST ()
 306 -- tree1ParsePrint = case parse @(FinalSyntaxes ()) @() tree1Print of
 307 --  Left e -> error e
 308 --  Right (TermVT _ty (unE -> Forall sem)) -> print sem
 309
 310 tree2ParsePrint :: TermAST ()
 311 tree2ParsePrint = case parse @(FinalSyntaxes ()) @() tree2Print of
 312   Left e -> error $ show e
 313   Right (TermVT _ty (unE -> Forall sem)) -> print sem
 314
 315 tree3ParsePrint :: TermAST ()
 316 tree3ParsePrint = case parse @(FinalSyntaxes ()) @() tree3Print of
 317   Left e -> error $ show e
 318   Right (TermVT _ty (unE -> Forall sem)) -> print sem
 319
 320 tree3ParsePrint' :: TermAST ()
 321 tree3ParsePrint' = case parse @(FinalSyntaxes ()) @() tree3ParsePrint of
 322   Left e -> error $ show e
 323   Right (TermVT _ty (unE -> Forall sem)) -> print sem
 324
 325 tree4ParsePrint :: TermAST ()
 326 tree4ParsePrint = case parse @(FinalSyntaxes ()) @() tree4Print of
 327   Left e -> error $ show e
 328   Right (TermVT _ty (unE -> Forall sem)) -> print sem