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