Initial changes for a dependently (?) typed parser through gadt's

src/Expr.hs

@@ -1,5 +1,6 @@
 module Expr
   ( Size (..)
+  , SizedProof (..)
   , Register (..)
   , Label
   , Statement (..)
@@ -12,6 +13,7 @@ module Expr
   , rewrapSized
   , validate8
   , validate16
+  , haveCompatibleSizes
   )
 where
 
@@ -120,36 +122,47 @@ data Operand (s :: Size)
 -- TODO: proper memory addresses
 -- deriving (Show, Eq)
 
+data SizedProof (s :: Size) where
+  SP8 :: SizedProof SW8
+  SP16 :: SizedProof SW16
+  SPS :: SizedProof s
+
 data SomeSized (sized :: Size -> Type) where
-  SZ8 :: sized SW8 -> SomeSized sized
-  SZ16 :: sized SW16 -> SomeSized sized
-  SZS :: sized s -> SomeSized sized
+  SS :: SizedProof s -> sized s -> SomeSized sized
 
 rewrapSized
   :: forall sized sized2
    . (forall (y :: Size). sized y -> sized2 y)
   -> SomeSized sized
   -> SomeSized sized2
-rewrapSized con s = case s of
-  SZ8 x -> SZ8 (con x)
-  SZ16 x -> SZ16 (con x)
-  SZS x -> SZS (con x)
+rewrapSized con (SS s x) = SS s (con x)
+
+haveCompatibleSizes
+  :: SomeSized sized
+  -> SomeSized sized
+  -> (forall s1 s2. sized s1 -> sized s2 -> r)
+  -> r
+  -> r
+haveCompatibleSizes (SS s1 x) (SS s2 y) f e = case (s1, s2) of
+  (SP8, SP16) -> e
+  (SP16, SP8) -> e
+  _ -> f x y
 
 validate8
   :: (forall s. sized s -> Maybe (sized SW8)) -> SomeSized sized -> Maybe (sized SW8)
-validate8 fun = \case
-  SZ8 x -> Just x
-  SZ16 x -> Nothing
-  SZS x -> fun x
+validate8 fun (SS s x) = case s of
+  SP8 -> Just x
+  SP16 -> Nothing
+  SPS -> fun x
 
 validate16
   :: (forall s. sized s -> Maybe (sized SW16))
   -> SomeSized sized
   -> Maybe (sized SW16)
-validate16 fun = \case
-  SZ8 x -> Nothing
-  SZ16 x -> Just x
-  SZS x -> fun x
+validate16 fun (SS s x) = case s of
+  SP8 -> Nothing
+  SP16 -> Just x
+  SPS -> fun x
 
 instance Display (Operand s) where
   {-# INLINE displayBuilder #-}

src/Parser.hs

@@ -105,25 +105,24 @@ parseVarOrLabelName = do
     match (letterChar >> takeWhileP Nothing (\c -> isAlphaNum c || c == '_'))
   pure t
 
-type OpPair (s :: Size) = (Operand s, Operand s)
-
 -- Parser for operands
-parseOperand :: Maybe (SomeSized Operand) -> Parser (SomeSized OpPair)
-parseOperand op = label "Instruction operand" $ do
-  partialres <-
-    choice
-      [ try $ rewrapSized RegOp <$> parseRegister
-      , try $ rewrapSized ImmOp <$> parseImmediate
-      , SZS . MemOp <$> parseMemory
-      ]
-  case op of
-    Nothing -> pure partialres
-    Just o -> do
-      case (o, partialres) of
-        (SZ8 _, SZ8 _) -> pure partialres
-        (SZ16 _, SZ16 _) -> pure partialres
-        (SZS _, _) -> pure partialres
-        _ -> fail " "
+parseOperand :: Parser (SomeSized Operand)
+parseOperand = label "Instruction operand" $ do
+  choice
+    [ try $ rewrapSized RegOp <$> parseRegister
+    , try $ rewrapSized ImmOp <$> parseImmediate
+    , SS SPS . MemOp <$> parseMemory
+    ]
+
+parseSecondOperand :: SizedProof s -> Parser (Operand s)
+parseSecondOperand s1 = label "Instruction operand" $ do
+  (SS s2 o) <- parseOperand
+  case (s1, s2) of
+    (SP8, SP16) -> fail ""
+    (SP16, SP8) -> fail ""
+    (SP8, SP8) -> pure o
+    (SP16, SP16) -> pure o
+    (SPS, SP16) -> pure o
 
 -- Parser for instructions
 parseInstruction :: Parser Instruction
@@ -147,14 +146,16 @@ parseInstruction =
     singleP constr txt arg =
       constr <$> do
         L.symbol' hspace1 txt *> arg
+    binaryP
+      :: (forall s. Operand s -> Operand s -> Instruction) -> Text -> Parser Instruction
     binaryP constr txt = do
       L.symbol' hspace1 txt
       op1 <- label "op1" (L.lexeme hspace (parseOperand Nothing))
       op2 <-
         label
           "op2"
           (char ',' *> hidden hspace *> L.lexeme hspace (parseOperand (Just op1)))
-      pure $ constr
+      pure $ constr op1 op2
 
 parseDirective :: Parser Directive
 parseDirective =