src/Symantic/Syntaxes.hs

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