src/Symantic/Syntaxes.hs

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