src/Symantic/Syntaxes.hs

   1 {-# LANGUAGE ConstraintKinds #-}
   2 {-# LANGUAGE QuantifiedConstraints #-}
   3 {-# LANGUAGE RankNTypes #-}
   4 {-# LANGUAGE UndecidableInstances #-}
   5
   6 module Symantic.Syntaxes where
   7
   8 import Control.Applicative (Applicative (..))
   9 import Control.Monad (Monad (..))
  10 import Control.Monad.Trans.Except qualified as MT
  11 import Control.Monad.Trans.Reader qualified as MT
  12 import Control.Monad.Trans.State qualified as MT
  13 import Data.Bool (otherwise)
  14 import Data.Either (Either (..))
  15 import Data.Eq (Eq (..))
  16 import Data.Function (id, ($), (.))
  17 import Data.Functor (Functor (..), (<$>))
  18 import Data.Functor.Constant (Constant (..))
  19 import Data.Int (Int)
  20 import Data.Kind (Constraint, Type)
  21 import Data.Maybe (Maybe (..), isJust)
  22 import Data.Proxy (Proxy (..))
  23 import Data.Semigroup (Semigroup (..))
  24 import Data.String (String)
  25 import GHC.Types
  26 import Text.Read (Read (..), reads)
  27 import Text.Show (Show (..))
  28 import Type.Reflection (TypeRep, Typeable, eqTypeRep, typeRep, (:~~:) (..))
  29 import Unsafe.Coerce (unsafeCoerce)
  30 import Prelude (error)
  31 import Prelude qualified
  32
  33 import Symantic
  34 import Symantic.Typer
  35
  36 class Addable sem where
  37   lit :: Int -> sem Int
  38   neg :: sem Int -> sem Int
  39   add :: sem Int -> sem Int -> sem Int
  40 class Mulable sem where
  41   mul :: sem Int -> sem Int -> sem Int
  42 class Abstractable sem where
  43   -- | Lambda term abstraction, in HOAS (Higher-Order Abstract Syntax) style.
  44   lam :: Typeable a => (sem a -> sem b) -> sem (a -> b)
  45
  46   -- | Application, aka. unabstract.
  47   (.@) :: sem (a -> b) -> sem a -> sem b
  48
  49 instance (forall sem. syn sem => Addable sem) => Addable (ForallSem syn) where
  50   lit n = ForallSem (lit n)
  51   neg (ForallSem a) = ForallSem (neg a)
  52   add (ForallSem a) (ForallSem b) = ForallSem (add a b)
  53 instance (forall sem. syn sem => Mulable sem) => Mulable (ForallSem syn) where
  54   mul (ForallSem a) (ForallSem b) = ForallSem (mul a b)
  55 instance
  56   ( forall sem. syn sem => Abstractable sem
  57   -- , forall sem. syn sem => Typeable sem -- user instance not accepted
  58   -- , forall s1 s2. (syn s1, syn s2) => s1 ~ s2 -- crazy...
  59   ) =>
  60   Abstractable (ForallSem syn)
  61   where
  62   ForallSem a2b .@ ForallSem a = ForallSem (a2b .@ a)
  63   lam f = ForallSem (lam (\a -> let ForallSem b = f (forallSem a) in b))
  64     where
  65       -- Safe here because a :: sem a and b :: sem b share the same 'sem'.
  66       forallSem :: sem a -> ForallSem syn a
  67       forallSem a = ForallSem (unsafeCoerce a)
  68
  69 --
  70 -- Parsing
  71 --
  72
  73 parseAddable ::
  74   ( forall sem. syn sem => Addable sem
  75   , syn (ForallSem syn)
  76   ) =>
  77   (TermAST -> Parser syn) ->
  78   TermAST ->
  79   Parser syn
  80 parseAddable _final (BinTree0 (TokenTermAtom s))
  81   | Right (i :: Int) <- safeRead s =
  82       Parser $ Right $ TermVT TyConst{tyConst = Const{constType = typeRep, constMeta = ()}, tyConstLen = LenZ} $ ForallSem @_ @Int $ lit i
  83 parseAddable final (BinTree2 (BinTree0 (TokenTermAtom "Neg")) aT) = Parser $
  84   case final aT of
  85     Parser aE -> do
  86       TermVT aTy (ForallSem a :: ForallSem syn a) <- aE
  87       case eqTy aTy TyConst{tyConst = Const{constType = typeRep @Int, constMeta = ()}, tyConstLen = lenVar aTy} of
  88         Nothing -> Left "TypeError"
  89         Just HRefl -> do
  90           Right $ TermVT aTy $ neg a
  91 parseAddable final (BinTree2 (BinTree2 (BinTree0 (TokenTermAtom "Add")) aT) bT) =
  92   Parser $ do
  93     TermVT aTy (ForallSem a :: ForallSem syn a) <- unParser (final aT)
  94     case eqTy aTy TyConst{tyConst = Const{constType = typeRep @Int, constMeta = ()}, tyConstLen = lenVar aTy} of
  95       Nothing -> Left "TypeError"
  96       Just HRefl -> do
  97         TermVT bTy (ForallSem b :: ForallSem syn b) <- unParser (final bT)
  98         case eqTy bTy TyConst{tyConst = Const{constType = typeRep @Int, constMeta = ()}, tyConstLen = lenVar bTy} of
  99           Nothing -> Left "TypeError"
 100           Just HRefl -> do
 101             Right $ TermVT aTy $ ForallSem @_ @Int $ add a b
 102 parseAddable _final e = Parser $ Left $ "Invalid tree: " <> show e
 103
 104 -- tree0Parser :: (forall sem. syn sem => Addable sem, syn (ForallSem syn)) => Either ErrMsg (ForallSem syn Int)
 105 -- tree0Parser = unParser $ parse tree0Print
 106
 107 parseMulable ::
 108   ( forall sem. syn sem => Mulable sem
 109   , forall sem. syn sem => Addable sem
 110   , syn (ForallSem syn)
 111   ) =>
 112   (TermAST -> Parser syn) ->
 113   TermAST ->
 114   Parser syn
 115 parseMulable final (BinTree2 (BinTree2 (BinTree0 (TokenTermAtom "Mul")) aT) bT) =
 116   Parser $ do
 117     case (final aT, final bT) of
 118       (Parser aE, Parser bE) -> do
 119         TermVT aTy (ForallSem a :: ForallSem syn a) <- aE
 120         case eqTy aTy TyConst{tyConst = Const{constType = typeRep @Int, constMeta = ()}, tyConstLen = lenVar aTy} of
 121           Nothing -> Left "TypeError"
 122           Just HRefl -> do
 123             TermVT bTy (ForallSem b :: ForallSem syn b) <- bE
 124             case eqTy bTy TyConst{tyConst = Const{constType = typeRep @Int, constMeta = ()}, tyConstLen = lenVar bTy} of
 125               Nothing -> Left "TypeError"
 126               Just HRefl -> do
 127                 Right $ TermVT aTy (ForallSem @_ @a $ mul a b)
 128 parseMulable final t = parseAddable final t
 129
 130 parseAbstractable ::
 131   ( forall sem. syn sem => Mulable sem
 132   , forall sem. syn sem => Addable sem
 133   , forall sem. syn sem => Abstractable sem
 134   , syn (ForallSem syn)
 135   ) =>
 136   a ~ Int =>
 137   (TermAST -> Parser syn) ->
 138   TermAST ->
 139   Parser syn
 140 -- TODO: parse variables
 141 parseAbstractable final (BinTree0 (TokenTermAbst n (TyVT (aTy :: Ty meta vs a)) bT)) =
 142   Parser $
 143     case final bT of
 144       Parser bE -> do
 145         TermVT abTy (abF :: ForallSem syn ab) <- bE
 146         case eqTy TyConst{tyConst = Const{constType = typeRep @Type, constMeta = ()}, tyConstLen = lenVar aTy} aTy of
 147           Nothing -> Left "TypeError"
 148           Just HRefl -> do
 149             case abTy of
 150               FUN iTy bTy ->
 151                 case eqTy TyConst{tyConst = Const{constType = typeRep @Type, constMeta = ()}, tyConstLen = lenVar bTy} bTy of
 152                   Nothing -> Left "TypeError"
 153                   Just HRefl -> do
 154                     let (aTy', iTy') = appendVars aTy iTy
 155                     case eqTy aTy' iTy' of
 156                       Nothing -> Left "TypeError"
 157                       Just HRefl -> do
 158                         case abF of
 159                           ForallSem ab ->
 160                             Right $
 161                               TermVT abTy $
 162                                 ForallSem @_ @ab $
 163                                   -- FIXME: Tyable
 164                                   lam (ab .@)
 165               _ -> Left "TypeError"
 166 parseAbstractable final t = parseMulable final t
 167
 168 --
 169 -- Printing
 170 --
 171
 172 instance Addable Printer where
 173   lit n = Printer $ BinTree0 (TokenTermAtom (show n))
 174   neg (Printer aT) = Printer $ BinTree2 (BinTree0 (TokenTermAtom "Neg")) aT
 175   add = print2 "Add"
 176 instance Mulable Printer where
 177   mul = print2 "Mul"
 178 instance Abstractable Printer where
 179   Printer f .@ Printer a = Printer $ BinTree2 f a
 180   lam (f :: Printer a -> Printer b) =
 181     Printer $
 182       -- FIXME: Tyable? instead of Typeable?
 183       BinTree0
 184         ( TokenTermAbst
 185             "x"
 186             (TyVT TyConst{tyConst = Const{constType = typeRep @a, constMeta = ()}, tyConstLen = LenZ})
 187             (unPrinter (f (Printer (BinTree0 (TokenTermAtom "x")))))
 188         )
 189
 190 class (Addable sem, Mulable sem, Abstractable sem) => FinalSyntaxes sem
 191 instance (Addable sem, Mulable sem, Abstractable sem) => FinalSyntaxes sem
 192
 193 fix :: (a -> a) -> a
 194 fix f = f (fix f)
 195
 196 parse ::
 197   ( forall sem. syn sem => Addable sem
 198   , forall sem. syn sem => Mulable sem
 199   , forall sem. syn sem => Abstractable sem
 200   , syn (ForallSem syn)
 201   ) =>
 202   TermAST ->
 203   Parser syn
 204 parse = fix parseAbstractable
 205
 206 tree0 = add (lit 8) (neg (add (lit 1) (lit 2)))
 207 tree1 = mul (add (lit 8) (neg (add (lit 1) (lit 2)))) (lit 2)
 208 tree2 = lam (\(x :: sem Int) -> mul (lit 0) (add (lit 1) (lit 2)))
 209 tree0Print = print tree0
 210 tree1Print = print tree1
 211 tree2Print = print tree2
 212
 213 tree0ParsePrint :: TermAST
 214 tree0ParsePrint = case parse @FinalSyntaxes tree0Print of
 215   Parser (Left e) -> error e
 216   Parser (Right (TermVT _ty (ForallSem sem))) -> print sem
 217
 218 tree1ParsePrint :: TermAST
 219 tree1ParsePrint = case parse @FinalSyntaxes tree1Print of
 220   Parser (Left e) -> error e
 221   Parser (Right (TermVT _ty (ForallSem sem))) -> print sem
 222
 223 tree2ParsePrint :: TermAST
 224 tree2ParsePrint = case parse @FinalSyntaxes tree2Print of
 225   Parser (Left e) -> error e
 226   Parser (Right (TermVT _ty (ForallSem sem))) -> print sem