packages feed

c-expr-dsl (empty) → 0.1.0.0

raw patch · 39 files changed

+7282/−0 lines, 39 filesdep +basedep +bytestringdep +c-expr-dsl

Dependencies added: base, bytestring, c-expr-dsl, c-expr-runtime, containers, debruijn, filepath, fin, indexed-traversable, libclang-bindings, mtl, parsec, scientific, some, tasty, tasty-golden, tasty-hunit, text, vec

Files

+ CHANGELOG.md view
@@ -0,0 +1,78 @@+# Revision history for `c-expr-dsl`++## 0.1.0.0 -- 2026-07-14++### Breaking changes++* `CheckedMacroTypeExpr` is renamed to `TypecheckedMacroTypeExpr` and gains+  `Foldable` and `Traversable` instances.+* `CheckedMacroValueExpr` is renamed to `TypecheckedMacroValueExpr` and gains+  `Functor`, `Foldable`, and `Traversable` instances.+* `TypeSource` is renamed to `CTypeSource`; its constructors `TypeSourceTypedef`+  and `TypeSourceMacroType` are renamed to `FromTypedef` and `FromMacroType`.+* Re-export parse-related symbols from `C.Expr.Parse`; demote lower-level+  modules to `other-modules`.+* Re-export typecheck-related symbols from `C.Expr.Typecheck`; demote+  `C.Expr.Typecheck.Expr` to `other-modules`; `C.Expr.Typecheck.Type` is still+  an exposed module.+* `Expr` and `Term` gain a `ctx :: Ctx` type index (from `debruijn`) for+  the local macro parameter scope. `Macro.macroArgs :: [Name]` is replaced+  by an existential `macroParams :: Vec ctx Name`; `macroExpr` becomes+  `Expr ctx Ps`. `sameMacro` compares macros structurally, ignoring location.+* `TypeTagged !TagKind !Name` is now a separate `Literal` constructor+  instead of a `TypeLit` variant.+* Some macros that were previously erroneously parsed as function-like are now+  parsed as object-like. See [PR #1990][pr-1990].+* Remove the `sameMacro` function. See [PR #1983][pr-1983].+* `CharLiteral.charLiteralValue` is now `CChar`; multi-character constants and+  numeric escapes wider than a single byte are rejected during parsing.+* `StringLiteral.stringLiteralValue` is now a strict `ByteString` holding the+  UTF-8 execution-encoding bytes (previously `[CharValue]`, then `ByteArray`).+* Rename `C.Expr.Syntax.Literals` to `C.Expr.Syntax.Literal`.+* Rename `Name` to `Identifier` (module `C.Expr.Syntax.Identifier`). The new+  `Name` (module `C.Expr.Syntax.Name`) distinguishes ordinary names+  (`NameOrdinary`) from tagged-type names (`NameTagged Identifier TagKind`).+  Tagged types now parse as `Var` nodes rather than `TypeTagged` literals.+* The `Ps` pass gains an annotation type parameter (`Ps ann`); `XVar (Ps ann)`+  carries a per-variable annotation. The `Tc` pass fixes its annotation to+  `Maybe QuantTy`.+* `tcMacros` no longer takes a typedef set or the `injectType`, `injectValue`,+  and `injectTaggedType` callbacks. It now takes a single+  `ann -> Maybe QuantTy` projection mapping each variable's parse annotation to+  its type (`Nothing` falls back to previously-typechecked macros). Accordingly,+  `CTypeSource`, `buildTypedefEnv`, and the `MacroTcInjectError` result+  constructor are removed.++### New features++* Parse macro types in addition to expressions; defer the type-vs-value+  distinction to the typechecking phase. See [PR #1862][pr-1862].+* Add test suite covering the parser (token-based and real-world libclang+  tests) and the typechecker. See [PR #1862][pr-1862].+* Local macro parameters in function-like macros are resolved to de Bruijn+  indices (`LocalParam (Idx ctx)`) at parse time, distinguishing them from+  free variables (`Var`).+* `tcMacro` now rejects type-like macros that expand to an incomplete type+  (`void` or `const void` at the top level) with a new `TcIncompleteTypeMacro`+  error. Pointer-to-incomplete types (e.g. `void *`) are still accepted.+* Support multi-line macro definitions. See [PR #1993][pr-1993].++### Minor changes++* New unit test suite `Test.CExpr.Parse.Literal` covering all character and+  string literal forms, escape sequences, and rejection cases.++### Bug fixes++* In accordance with the C reference, parse macros only as function-like when+  there is no whitespace between the macro name and the opening parenthesis of+  the parameter list. See [PR #1990][pr-1990].++[pr-1862]: https://github.com/well-typed/hs-bindgen/pull/1862+[pr-1983]: https://github.com/well-typed/hs-bindgen/pull/1983+[pr-1990]: https://github.com/well-typed/hs-bindgen/pull/1990+[pr-1993]: https://github.com/well-typed/hs-bindgen/pull/1993++## 0.1.0-alpha -- 2026-02-06++* Release candidate.
+ LICENSE view
@@ -0,0 +1,29 @@+Copyright (c) 2024-2026, Well-Typed LLP and Anduril Industries Inc.+++Redistribution and use in source and binary forms, with or without+modification, are permitted provided that the following conditions are met:++    * Redistributions of source code must retain the above copyright+      notice, this list of conditions and the following disclaimer.++    * Redistributions in binary form must reproduce the above+      copyright notice, this list of conditions and the following+      disclaimer in the documentation and/or other materials provided+      with the distribution.++    * Neither the name of the copyright holder nor the names of its+      contributors may be used to endorse or promote products derived+      from this software without specific prior written permission.++THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS+"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT+LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR+A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT+HOLDER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,+SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT+LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,+DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY+THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT+(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE+OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+ README.md view
@@ -0,0 +1,22 @@+# `c-expr-dsl`++`c-expr-dsl` is a [Haskell][] library providing a DSL for the C expression and+type language implemented by [`c-expr-runtime`][]: a [Parsec][]-based parser+turning [LLVM/Clang][] `libclang` macro tokens into a syntax tree, and a+bidirectional typechecker. It supports the [`hs-bindgen`][] project but can be+used independently.++`c-expr-dsl` requires an LLVM/Clang installation, as it parses macros via+`libclang`; see [`libclang-bindings`][] for setup details.++See the [main README][] for more information, and the [changelog][] for+release notes.++[Haskell]: <https://www.haskell.org/>+[Parsec]: <https://hackage.haskell.org/package/parsec>+[LLVM/Clang]: <https://github.com/llvm/llvm-project>+[`c-expr-runtime`]: <https://github.com/well-typed/c-expr/tree/main/c-expr-runtime>+[`hs-bindgen`]: <https://github.com/well-typed/hs-bindgen>+[`libclang-bindings`]: <https://github.com/well-typed/libclang-bindings/blob/main/manual/README.md>+[main README]: <https://github.com/well-typed/c-expr#readme>+[changelog]: <https://github.com/well-typed/c-expr/blob/main/c-expr-dsl/CHANGELOG.md>
+ c-expr-dsl.cabal view
@@ -0,0 +1,152 @@+cabal-version:   3.0+name:            c-expr-dsl+version:         0.1.0.0+license:         BSD-3-Clause+license-file:    LICENSE+author:          Well-Typed LLP+maintainer:      info@well-typed.com+category:        System+build-type:      Simple+extra-doc-files:+  CHANGELOG.md+  README.md++synopsis:        DSL for the language support by c-expr-runtime+tested-with:+  GHC ==9.2.8+   || ==9.4.8+   || ==9.6.7+   || ==9.8.4+   || ==9.10.3+   || ==9.12.2+   || ==9.14.1++description:+  This library provides the front end for the c-expr DSL: a Parsec-based parser+  that turns libclang macro tokens into a syntax tree, and a typechecker that+  assigns types to macro expressions according to the rules implemented in+  c-expr-runtime.++data-files:      *.golden+data-dir:        test/fixtures++source-repository head+  type:     git+  location: https://github.com/well-typed/c-expr.git+  subdir:   c-expr-dsl++source-repository this+  type:     git+  location: https://github.com/well-typed/c-expr.git+  subdir:   c-expr-dsl+  tag:      release-0.1.0.0++common lang+  build-depends:      base >=4.16 && <4.23+  default-language:   GHC2021+  default-extensions:+    DataKinds+    DeriveAnyClass+    DerivingStrategies+    LambdaCase+    MultiWayIf+    OverloadedStrings+    PatternSynonyms+    QuantifiedConstraints+    TypeFamilies+    UndecidableInstances++  other-extensions:+    CPP+    MagicHash++  ghc-options:+    -Wall -Wunused-packages -Wno-unticked-promoted-constructors+    -Wprepositive-qualified-module++library+  import:          lang+  hs-source-dirs:  src+  exposed-modules:+    C.Expr.Parse+    C.Expr.Syntax+    C.Expr.Typecheck+    C.Expr.Typecheck.Interface.Type+    C.Expr.Typecheck.Interface.Value+    C.Expr.Typecheck.Type+    C.Expr.Util.Panic++  other-modules:+    C.Expr.Parse.Expr+    C.Expr.Parse.Identifier+    C.Expr.Parse.Infra+    C.Expr.Parse.Literal+    C.Expr.Syntax.Expr+    C.Expr.Syntax.Identifier+    C.Expr.Syntax.Literal+    C.Expr.Syntax.Name+    C.Expr.Syntax.TTG+    C.Expr.Syntax.TTG.Parse+    C.Expr.Syntax.TTG.Typecheck+    C.Expr.Syntax.Type+    C.Expr.Typecheck.Expr+    C.Expr.Util.Parsec+    C.Expr.Util.TestEquality++  -- internal dependencies+  build-depends:   c-expr-runtime >=0.1.0.0 && <0.2++  -- external dependencies+  build-depends:+    , bytestring           >=0.10  && <0.13+    , containers           >=0.6   && <0.9+    , debruijn             >=0.3.1 && <0.4+    , fin                  >=0.3.2 && <0.4+    , indexed-traversable  >=0.1.4 && <0.2+    , libclang-bindings    >=0.1   && <0.2+    , mtl                  >=2.2   && <2.4+    , parsec               >=3.1   && <3.2+    , scientific           >=0.3.7 && <0.4+    , some                 >=1.0.6 && <1.1+    , text                 >=1.2   && <2.2+    , vec                  >=0.5   && <0.6++test-suite test-c-expr-dsl+  import:          lang+  type:            exitcode-stdio-1.0+  main-is:         Main.hs+  hs-source-dirs:  test+  other-modules:+    Paths_c_expr_dsl+    Test.CExpr.Parse+    Test.CExpr.Parse.Golden+    Test.CExpr.Parse.Infra+    Test.CExpr.Parse.Literal+    Test.CExpr.Parse.Macro+    Test.CExpr.Parse.Type+    Test.CExpr.Typecheck+    Test.CExpr.Typecheck.Classify+    Test.CExpr.Typecheck.Infra+    Test.CExpr.Util++  autogen-modules: Paths_c_expr_dsl++  -- internal dependencies+  build-depends:+    , c-expr-dsl+    , c-expr-runtime++  -- external dependencies+  build-depends:+    , bytestring         >=0.10  && <0.13+    , containers         >=0.6   && <0.9+    , debruijn           >=0.3.1 && <0.4+    , filepath           >=1.4   && <1.6+    , fin                >=0.3.2 && <0.4+    , libclang-bindings  >=0.1   && <0.2+    , parsec             >=3.1   && <3.2+    , tasty              >=1.4   && <1.6+    , tasty-golden       >=2.3   && <2.4+    , tasty-hunit        >=0.10  && <0.11+    , text               >=1.2   && <2.2+    , vec                >=0.5   && <0.6
+ src/C/Expr/Parse.hs view
@@ -0,0 +1,12 @@+module C.Expr.Parse (+    -- * Parsing macros+    parseMacro+  , parseMacroType+    -- * Parser infrastructure+  , Parser+  , runParser+  , MacroParseError(..)+  ) where++import C.Expr.Parse.Expr (parseMacro, parseMacroType)+import C.Expr.Parse.Infra (MacroParseError (..), Parser, runParser)
+ src/C/Expr/Parse/Expr.hs view
@@ -0,0 +1,513 @@+{-# LANGUAGE OverloadedRecordDot #-}++module C.Expr.Parse.Expr (parseMacro, parseMacroType) where++import Control.Monad+import Data.Foldable qualified as Foldable+import Data.Functor.Identity+import Data.Text (Text)+import Data.Type.Nat+import Data.Vec.Lazy (Vec (..))+import Data.Vec.Lazy qualified as Vec+import DeBruijn (Idx (..))+import Text.Parsec hiding (parseTest, token)+import Text.Parsec.Expr++import C.Expr.Parse.Identifier+import C.Expr.Parse.Infra+import C.Expr.Parse.Literal+import C.Expr.Syntax++import Clang.CStandard+import Clang.Enum.Simple+import Clang.HighLevel.Types+import Clang.LowLevel.Core++{-------------------------------------------------------------------------------+  Top-level++  Some useful references:++  - Section 6.10 "Preprocessing directives" of the C standard+    <https://fog.misty.com/perry/osp/standard/preproc.pdf>+  - Section 3 "Macros" of the @cpp@ documentation+    <https://gcc.gnu.org/onlinedocs/cpp/Macros.html>+  - "C operator precedence"+    <https://en.cppreference.com/w/c/language/operator_precedence>+-------------------------------------------------------------------------------}++-- | Parse a macro definition (type or value expression)+--+-- Tries to parse the body as a type expression first. A valid type token+-- sequence always produces @'Term' ('Type' …)@; everything else parses as an+-- expression. Only when typechecking macros, we can fully discriminate type and+-- value expressions.+parseMacro :: ClangCStandard -> Parser (Macro ())+parseMacro cStd = do+    (macroLocRange, macroName) <- parseLocIdentifier+    let+        macroLoc :: MultiLoc+        macroLoc = macroLocRange.rangeStart++        functionLike :: Parser (Macro ())+        functionLike = do+          noWhitespace macroLocRange+          paramNames <- formalParams+          Vec.reifyList (reverse paramNames) $ \macroParams -> do+            macroExpr <- bodyExpr macroParams+            pure $ Macro macroLoc macroName (Vec.reverse macroParams) macroExpr++        objectLike :: Parser (Macro ())+        objectLike = do+          macroExpr <- bodyExpr VNil+          pure $ Macro macroLoc macroName VNil macroExpr+    m <- choice [try functionLike, objectLike]+    eof+    return m+  where+    -- Try the body as a type expression first. The @'eof'@ inside the @'try'@+    -- is essential: if @'parseMacroType'@ succeeds on a prefix (e.g. the bare+    -- identifier in @size_t + 1@) but leaves tokens unconsumed, the whole+    -- attempt is abandoned and we fall back to the expression parser.+    bodyExpr :: Vec ctx Identifier -> Parser (Expr ctx (Ps ()))+    bodyExpr macroParams = do+      rejectPragma+      try (parseMacroType cStd macroParams <* eof) <|> exprTuple cStd macroParams++-- | Reject macro bodies that begin with the @_Pragma@ operator+--+-- @_Pragma@ is the C99 preprocessor operator (C standard §6.10.9), equivalent+-- to @#pragma@. A macro whose body uses it, such as+--+-- > #define PACK_START _Pragma("pack(1)")+--+-- expands to a preprocessing directive, not a C value or type expression. We+-- reject such macros here rather than misparsing @_Pragma@ as a reference to a+-- variable of that name, which would otherwise survive parsing and only fail+-- later (during name resolution or typechecking) with a misleading message.+rejectPragma :: Parser ()+rejectPragma =+    notFollowedBy (token isPragma) <?> "C expression (not a _Pragma operator)"+  where+    isPragma :: Token TokenSpelling -> Maybe ()+    isPragma t+      | getTokenSpelling (tokenSpelling t) == "_Pragma" = Just ()+      | otherwise                                       = Nothing++formalParams :: Parser [Identifier]+formalParams = parens $ parseIdentifier `sepBy` comma++lookupParam :: Identifier -> Vec ctx Identifier -> Maybe (Idx ctx)+lookupParam _ VNil    = Nothing+lookupParam n (m ::: vec)+  | n == m    = Just IZ+  | otherwise = IS <$> lookupParam n vec++-- | Check that there is no whitespace between the previous token and the current+-- token+--+-- Function-like macros are only function-like if there is /no/ whitespace+-- between the macro name and the opening parenthesis of the parameter list.+--+-- We used to not check whitespace, which was the source of a bug. See issue+-- #1903: <https://github.com/well-typed/hs-bindgen/issues/1903>+noWhitespace ::+     -- | Source range for the previous token+     Range MultiLoc+  -> Parser ()+noWhitespace prevRange = lookAhead $ do+    tok <- anyToken+    let prev    = prevRange.rangeEnd.multiLocExpansion+        current = tok.tokenExtent.rangeStart.multiLocExpansion+        p       = prev.singleLocPath   == current.singleLocPath &&+                  prev.singleLocLine   == current.singleLocLine &&+                  prev.singleLocColumn == current.singleLocColumn+    unless p $+      parserFail "unexpected whitespace"++{-------------------------------------------------------------------------------+  Types++-------------------------------------------------------------------------------}++-- | Parse a macro body as a C type expression+--+-- Recognizes the following grammar (informally):+--+-- @+--   type           ::= const? type_base const? pointer_layers?+--+--   type_base      ::= sign_specifier? int_size_keyword? 'int'?+--                    | sign_specifier? 'char'+--                    | 'float' | 'double'+--                    | 'void'+--                    | '_Bool' | 'bool'+--                    | ('struct' | 'union' | 'enum') identifier+--                    | identifier+--+--   pointer_layers ::= ('*' const?)++-- @+--+-- Returns an @'Expr' ctx ('Ps' ())@ where:+--+-- * A keyword base type becomes @'Term' ('Literal' ('TypeLit' …))@.+-- * A tagged base type (e.g. @struct Foo@) becomes @'Term' ('Var' …)@ with a+--   'NameTagged' name; the typechecker resolves it.+-- * A bare identifier that is a local macro parameter becomes @'Term' ('LocalParam' …)@.+-- * A bare identifier that is a free variable becomes @'Term' ('Var' …)@;+--   the typechecker decides whether it names a type or a value.+-- * Each @const@ qualifier wraps the expression in @'TyApp' 'Const'@.+-- * Each @*@ pointer layer wraps the expression in @'TyApp' 'Pointer'@.+parseMacroType :: ClangCStandard -> Vec ctx Identifier -> Parser (Expr ctx (Ps ()))+parseMacroType cStd macroParams = do+    constBefore <- option False (True <$ keyword "const")+    base        <- typeBase cStd macroParams+    constAfter  <- option False (True <$ keyword "const")+    ptrs        <- pointerLayers+    -- In C, @const@ is idempotent: @const int const@ is valid but equivalent+    -- to @const int@. We therefore wrap with at most one 'Const' layer,+    -- regardless of whether the qualifier appeared before or after the base.+    let withConst+          | constBefore || constAfter = TyApp Const (base ::: VNil)+          | otherwise                 = base+    return (Foldable.foldl' apPtr withConst ptrs)+  where+    apPtr acc ptrConst =+      let withPtr = TyApp Pointer (acc ::: VNil)+      in if ptrConst then TyApp Const (withPtr ::: VNil) else withPtr++-- | Base of a type expression (without const/pointer layers)+--+-- Returns:+--+-- * @'Term' ('Literal' ('TypeLit' …))@ for keyword base types.+-- * @'Term' ('Var' …)@ with a 'NameTagged' name for a tagged base type (e.g. @struct Foo@).+-- * @'Term' ('LocalParam' …)@ for a bare identifier that is a local macro parameter.+-- * @'Term' ('Var' …)@ for any other bare identifier; the typechecker decides+--   whether it names a type or a value.+typeBase :: forall ctx. ClangCStandard -> Vec ctx Identifier -> Parser (Expr ctx (Ps ()))+typeBase cStd macroParams =+    choice [+        -- Type literal.+        Term . Literal . TypeLit <$> typeLiteral cStd+        -- Tagged type (e.g., @struct Foo@)+      , Term . mkTagged <$> taggedTypeLit+        -- The bare identifier (typedef name, type macro, or expression+        -- variable) is needed to parse pointer-qualified typedef references+        -- such as @size_t *@: without it, @parseMacroType@ would reject the+        -- identifier base and the expression parser would then fail on @*@ (a+        -- binary operator without a right-hand side). Attempting to detangle+        -- the two by restricting @parseMacroType@ to keyword\/tagged bases only+        -- does not help (both paths produce the same @'Var'@ node) while+        -- adding backtracking overhead.+      , Term . mkVar <$> parseIdentifier+      ]+  where+    mkTagged :: (TagKind, Identifier) -> Term ctx (Ps ())+    mkTagged (tag, ident) = Var (XVarPs ()) (NameTagged ident tag) []++    mkVar :: Identifier -> Term ctx (Ps ())+    mkVar n = case lookupParam n macroParams of+      Just i  -> LocalParam i+      Nothing -> Var (XVarPs ()) (NameOrdinary n) []++-- | Parse a sequence of type-literal keywords and combine them+--+-- C type literal keywords can appear in various orders:+--+-- @+--   unsigned long int+--   long unsigned int+--   int long unsigned+-- @+--+-- are all the same type.+typeLiteral :: ClangCStandard -> Parser TypeLit+typeLiteral cStd = do+    kws <- many1 (typeKeyword cStd)+    case interpretKeywords kws of+      Just lit -> return lit+      Nothing  -> fail "unrecognised type literal"++-- | Parse an elaborated type literal+--+-- @+--   struct tag+--   union  tag+--   enum   tag+-- @+taggedTypeLit :: Parser (TagKind, Identifier)+taggedTypeLit = do+    tag <- choice [+        TagStruct <$ keyword "struct"+      , TagUnion  <$ keyword "union"+      , TagEnum   <$ keyword "enum"+      ]+    name <- parseIdentifier+    return (tag, name)++data TypeKeyword =+    KwSigned | KwUnsigned+  | KwShort | KwInt | KwLong | KwChar+  | KwFloat | KwDouble+  | KwVoid | KwBool+  deriving stock (Eq)++typeKeyword :: ClangCStandard -> Parser TypeKeyword+typeKeyword cStd = choice $+      [ KwSigned   <$ keyword "signed"+      , KwUnsigned <$ keyword "unsigned"+      , KwShort    <$ keyword "short"+      , KwInt      <$ keyword "int"+      , KwLong     <$ keyword "long"+      , KwChar     <$ keyword "char"+      , KwFloat    <$ keyword "float"+      , KwDouble   <$ keyword "double"+      , KwVoid     <$ keyword "void"+      , KwBool     <$ keyword "_Bool"+      ]+      +++      -- @bool@ is a keyword in C23 and later.+      case cStd of+        ClangCStandard std _ | std >= C23 -> [bool]+        _                                 -> []+  where+    bool = KwBool <$ keyword "bool"++-- | Combine a list of type keywords into a type literal+--+-- Returns 'Nothing' if the combination is invalid.+--+-- Duplicate keywords (e.g. @signed signed int@) are accepted, since input+-- tokens come from libclang-validated C source and such constructs are+-- rejected by the C compiler long before we see them.+interpretKeywords :: [TypeKeyword] -> Maybe TypeLit+interpretKeywords kws+  -- void+  | kws == [KwVoid]+  = Just TypeVoid++  -- _Bool / bool+  | kws == [KwBool]+  = Just TypeBool++  -- float+  | kws == [KwFloat]+  = Just $ TypeFloat SizeFloat++  -- double+  | kws == [KwDouble]+  = Just $ TypeFloat SizeDouble++  -- char with optional sign+  | KwChar `elem` kws+  , let sign = extractSign kws+  , all (\k -> k `elem` [KwChar, KwSigned, KwUnsigned]) kws+  = Just $ TypeChar sign++  -- integral types: combinations of sign, size, and int+  | all (\k -> k `elem` [KwSigned, KwUnsigned, KwShort, KwInt, KwLong]) kws+  = Just $ TypeInt (extractSign kws) (extractIntSize kws)++  | otherwise+  = Nothing++extractSign :: [TypeKeyword] -> Maybe Sign+extractSign kws+  | KwSigned   `elem` kws = Just Signed+  | KwUnsigned `elem` kws = Just Unsigned+  | otherwise              = Nothing++extractIntSize :: [TypeKeyword] -> Maybe IntSize+extractIntSize kws+  | KwShort `elem` kws                   = Just SizeShort+  | length (filter (== KwLong) kws) >= 2 = Just SizeLongLong+  | KwLong `elem` kws                    = Just SizeLong+  | KwInt `elem` kws                     = Just SizeInt+  | otherwise                            = Nothing+  -- NB: @signed@ alone (no size keyword, no @int@) means @signed int@.+  -- We return Nothing here; the caller interprets (Just sign, Nothing) as int.++-- | Parse zero or more pointer indirections, optionally followed by @const@+pointerLayers :: Parser [Bool]+pointerLayers = many pointerLayer++-- | Parse a pointer indirection, optionally followed by @const@+pointerLayer :: Parser Bool+pointerLayer = do+    punctuation "*"+    option False (True <$ keyword "const")++-- | Match a keyword token with the given spelling+keyword :: Text -> Parser ()+keyword expected = token $ \t ->+    if fromSimpleEnum (tokenKind t) == Right CXToken_Keyword+       && getTokenSpelling (tokenSpelling t) == expected+      then Just ()+      else Nothing++{-------------------------------------------------------------------------------+  Simple expressions+-------------------------------------------------------------------------------}++term :: forall ctx. ClangCStandard -> Vec ctx Identifier -> Parser (Term ctx (Ps ()))+term cStd macroParams =+    buildExpressionParser ops trm <?> "simple expression"+  where+    trm :: Parser (Term ctx (Ps ()))+    trm = choice [+        Literal <$> lit+      , localParamOrVar+      ]++    localParamOrVar :: Parser (Term ctx (Ps ()))+    localParamOrVar = do+      varName <- parseIdentifier+      case lookupParam varName macroParams of+        Just i ->+          pure $ LocalParam i+        Nothing ->+          Var (XVarPs ()) (NameOrdinary varName) <$>+            option [] (actualArgs cStd macroParams)++    lit :: Parser Literal+    lit = ValueLit <$> choice [+        ValueInt    <$> literalInteger+      , ValueFloat  <$> literalFloat+      , ValueChar   <$> literalChar+      , ValueString <$> literalString+      ]++    ops :: OperatorTable [Token TokenSpelling] () Identity (Term ctx (Ps ()))+    ops = []+++-- | Parse integer literal+literalInteger :: Parser IntegerLiteral+literalInteger = do+  (val, ty) <- parseTokenOfKind CXToken_Literal parseLiteralInteger+  return $+    IntegerLiteral+      { integerLiteralType  = ty+      , integerLiteralValue = val+      }++-- | Parse floating point literal+literalFloat :: Parser FloatingLiteral+literalFloat = do+  (fltVal, dblVal, ty) <- parseTokenOfKind CXToken_Literal parseLiteralFloating+  return $+    FloatingLiteral+      { floatingLiteralType = ty+      , floatingLiteralFloatValue = fltVal+      , floatingLiteralDoubleValue = dblVal+      }++-- | Parse character literal+literalChar :: Parser CharLiteral+literalChar = do+  val <- parseTokenOfKind CXToken_Literal parseLiteralChar+  return $ CharLiteral val++-- | Parse string literal+literalString :: Parser StringLiteral+literalString = do+  val <- parseTokenOfKind CXToken_Literal parseLiteralString+  return $ StringLiteral val++actualArgs :: ClangCStandard -> Vec ctx Identifier -> Parser [Expr ctx (Ps ())]+actualArgs cStd macroParams = parens $ expr cStd macroParams `sepBy` comma++{-------------------------------------------------------------------------------+  Expressions++  This is currently only a subset of the operators described in+  <https://en.cppreference.com/w/c/language/operator_precedence>, but we do+  follow the same structure.+-------------------------------------------------------------------------------}++exprTuple :: ClangCStandard -> Vec ctx Identifier -> Parser (Expr ctx (Ps ()))+exprTuple cStd macroParams = try tuple <|> expr cStd macroParams+  where+    tuple = do+      openParen <- optionMaybe $ punctuation "("+      (e1, e2, es) <- expr cStd macroParams `sepBy2` comma+      case openParen of+        Nothing -> return ()+        Just {} -> punctuation ")"+      return $+        Vec.reifyList es $ \es' ->+           VaApp NoXApp MTuple ( e1 ::: e2 ::: es' )++expr :: forall ctx. ClangCStandard -> Vec ctx Identifier -> Parser (Expr ctx (Ps ()))+expr cStd macroParams = buildExpressionParser ops trm <?> "expression"+  where++    trm :: Parser (Expr ctx (Ps ()))+    trm = choice [+          parens (expr cStd macroParams)+        , Term <$> term cStd macroParams+        ]++    -- 'OperatorTable' expects the list in descending precedence+    ops = [+        -- Precedence 1 (all left-to-right)+        []++        -- Precedence 2 (all right-to-left)+      , [ Prefix (ap1 MUnaryPlus  <$ punctuation "+")+        , Prefix (ap1 MUnaryMinus <$ punctuation "-")+        , Prefix (ap1 MLogicalNot <$ punctuation "!")+        , Prefix (ap1 MBitwiseNot <$ punctuation "~")+        ]++        -- Precedence 3 (precedence 3 .. 12 are all left-to-right)+      , [ Infix (ap2 MMult <$ punctuation "*") AssocLeft+        , Infix (ap2 MDiv  <$ punctuation "/") AssocLeft+        , Infix (ap2 MRem  <$ punctuation "%") AssocLeft+        ]++        -- Precedence 4+      , [ Infix (ap2 MAdd <$ punctuation "+") AssocLeft+        , Infix (ap2 MSub <$ punctuation "-") AssocLeft+        ]++        -- Precedence 5+      , [ Infix (ap2 MShiftLeft  <$ punctuation "<<") AssocLeft+        , Infix (ap2 MShiftRight <$ punctuation ">>") AssocLeft+        ]++        -- Precedence 6+      , [ Infix (ap2 MRelLT <$ punctuation "<")  AssocLeft+        , Infix (ap2 MRelLE <$ punctuation "<=") AssocLeft+        , Infix (ap2 MRelGT <$ punctuation ">")  AssocLeft+        , Infix (ap2 MRelGE <$ punctuation ">=") AssocLeft+        ]++        -- Precedence 7+      , [ Infix (ap2 MRelEQ <$ punctuation "==") AssocLeft+        , Infix (ap2 MRelNE <$ punctuation "!=") AssocLeft+        ]++        -- Precedence 8 .. 12+      , [ Infix (ap2 MBitwiseAnd <$ punctuation "&")  AssocLeft ]+      , [ Infix (ap2 MBitwiseXor <$ punctuation "^")  AssocLeft ]+      , [ Infix (ap2 MBitwiseOr  <$ punctuation "|")  AssocLeft ]+      , [ Infix (ap2 MLogicalAnd <$ punctuation "&&") AssocLeft ]+      , [ Infix (ap2 MLogicalOr  <$ punctuation "||") AssocLeft ]+      ]++    ap1 :: VaFun (S Z) -> Expr ctx (Ps ()) -> Expr ctx (Ps ())+    ap1 op arg = VaApp NoXApp op ( arg ::: VNil )++    ap2 :: VaFun (S (S Z)) -> Expr ctx (Ps ()) -> Expr ctx (Ps ()) -> Expr ctx (Ps ())+    ap2 op arg1 arg2 = VaApp NoXApp op ( arg1 ::: arg2 ::: VNil )++sepBy2 :: ParsecT s u m a -> ParsecT s u m sep -> ParsecT s u m (a, a, [a])+{-# INLINEABLE sepBy2 #-}+sepBy2 p sep = do+  x1 <- p+  void sep+  x2 <- p+  xs <- many $ sep >> p+  return (x1, x2, xs)
+ src/C/Expr/Parse/Identifier.hs view
@@ -0,0 +1,45 @@+-- | Parsing C identifiers+module C.Expr.Parse.Identifier (+    parseIdentifier+  , parseLocIdentifier+  ) where++import Control.Monad++import C.Expr.Parse.Infra+import C.Expr.Syntax.Identifier++import Clang.Enum.Simple+import Clang.HighLevel.Types+import Clang.LowLevel.Core++{-------------------------------------------------------------------------------+  Identifiers+-------------------------------------------------------------------------------}++-- | Parse an identifier+--+-- Does not accept C keywords. Use 'parseLocIdentifier' when the token may be a+-- keyword (e.g. for macro names, where @#define bool int@ is valid C).+parseIdentifier :: Parser Identifier+parseIdentifier = token $ \t -> do+    let spelling = getTokenSpelling (tokenSpelling t)+    let ki = fromSimpleEnum (tokenKind t)+    guard $ ki == Right CXToken_Identifier+    return $ Identifier spelling++-- | Parse an identifier together with its source location+--+-- Accepts both identifiers and keywords. In later LLVMs (not in 14, surely in+-- 16), @bool@ is classified as a keyword rather than an identifier. We accept+-- keywords here so that macros such as @#define bool int@ can be parsed. Even+-- in C23 the meaning of @bool@ can be overwritten (the macro takes precedence).+parseLocIdentifier :: Parser (Range MultiLoc, Identifier)+parseLocIdentifier = token $ \t -> do+    let spelling = getTokenSpelling (tokenSpelling t)+    let ki = fromSimpleEnum (tokenKind t)+    guard $ ki == Right CXToken_Identifier || ki == Right CXToken_Keyword+    return (+        tokenExtent t+      , Identifier spelling+      )
+ src/C/Expr/Parse/Infra.hs view
@@ -0,0 +1,156 @@+-- | Infrastructure for parsing+module C.Expr.Parse.Infra (+    -- * Parser type+    Parser+  , runParser+    -- * Parse errors+  , MacroParseError(..)+    -- * Dealing with individual tokens+  , token+    -- * Punctuation+  , punctuation+  , parens+  , comma+    -- * Parse tokens+  , TokenParser+  , parseTokenOfKind+  ) where++import Control.Exception+import Control.Monad+import Data.Bifunctor+import Data.Text (Text)+import Data.Text qualified as Text+import GHC.Generics+import GHC.Stack+import Text.Parsec hiding (runParser, token, tokens)+import Text.Parsec qualified as Parsec+import Text.Parsec.Pos++import C.Expr.Util.Panic++import Clang.Enum.Simple+import Clang.HighLevel.Types+import Clang.LowLevel.Core+import Clang.Paths++{-------------------------------------------------------------------------------+  Parser type+-------------------------------------------------------------------------------}++type Parser = Parsec [Token TokenSpelling] ()++runParser ::+     HasCallStack+  => Parser a+  -> [Token TokenSpelling]+  -> Either MacroParseError a+runParser p tokens =+    first unrecognized $ Parsec.runParser p () sourcePath tokens+  where+    sourcePath :: FilePath+    sourcePath =+        case tokens of+          []  -> panicPure "runParser: empty list"+          t:_ -> getSourcePath $ singleLocPath start+            where+              start :: SingleLoc+              start = rangeStart $ multiLocExpansion <$> tokenExtent t++    unrecognized :: ParseError -> MacroParseError+    unrecognized err = MacroParseError{+          parseError       = show err+        , parseErrorTokens = tokens+        }++{-------------------------------------------------------------------------------+  Parse errors+-------------------------------------------------------------------------------}++data MacroParseError = MacroParseError {+      parseError       :: String+    , parseErrorTokens :: [Token TokenSpelling]+    }+  deriving stock (Show, Eq, Generic)+  deriving anyclass (Exception)++{-------------------------------------------------------------------------------+  Dealing with individual tokens+-------------------------------------------------------------------------------}++token :: (Token TokenSpelling -> Maybe a) -> Parser a+token = Parsec.token tokenPretty tokenSourcePos+  where+    tokenPretty :: Token TokenSpelling -> String+    tokenPretty Token{tokenKind, tokenSpelling} = concat [+          show $ Text.unpack (getTokenSpelling tokenSpelling)+        , " ("+        , show tokenKind+        ,  ")"+        ]++    tokenSourcePos :: Token a -> SourcePos+    tokenSourcePos t =+        newPos+          (getSourcePath $ singleLocPath start)+          (singleLocLine start)+          (singleLocColumn start)+      where+        start :: SingleLoc+        start = rangeStart $ multiLocExpansion <$> tokenExtent t++tokenOfKind :: CXTokenKind -> (Text -> Maybe a) -> Parser a+tokenOfKind kind f = token $ \t ->+    if fromSimpleEnum (tokenKind t) == Right kind+      then f $ getTokenSpelling (tokenSpelling t)+      else Nothing++tokenOfKind' :: CXTokenKind -> (Text -> Bool) -> Parser ()+tokenOfKind' kind cmp = tokenOfKind kind (\actual -> guard $ cmp actual)++{-------------------------------------------------------------------------------+  Punctuation+-------------------------------------------------------------------------------}++punctuation :: Text -> Parser ()+punctuation expected = tokenOfKind' CXToken_Punctuation $+    \actual -> Text.unpack expected == removeMultilines (Text.unpack actual)++parens :: Parser a -> Parser a+parens p = punctuation "(" *> p <* punctuation ")"++comma :: Parser ()+comma = punctuation ","+++-- | Remove multiline characters from the string+--+-- Multiline characters are a pair of characters of the form "\\\n". These+-- characters are sometimes included in (punctuation) tokens. In other cases+-- @libclang@ handles multiline characters for us and does not report them. We+-- should remove multiline characters before comparing against a target string.+-- For example, we want @punctuation "("@ to match with a token that has+-- spelling "\\\n(".+--+-- >>> removeMultilines "a\\\ngbe\\\n"+-- "agbe"+--+removeMultilines :: String -> String+removeMultilines = \case+    []     -> []+    (c:cs) -> go c cs+  where+    go prev []        = [prev]+    go '\\' ('\n':cs) = removeMultilines cs+    go prev (c   :cs) = prev : go c cs++{-------------------------------------------------------------------------------+  Parse individual tokens+-------------------------------------------------------------------------------}++type TokenParser = Parsec Text ()++parseTokenOfKind :: CXTokenKind -> TokenParser a -> Parser a+parseTokenOfKind kind p = tokenOfKind kind $ \str ->+    either (const Nothing) Just $+      Parsec.parse (p <* Parsec.eof) "" str
+ src/C/Expr/Parse/Literal.hs view
@@ -0,0 +1,479 @@+module C.Expr.Parse.Literal (+    IntSuffix(..)+  , parseLiteralInteger+  , parseLiteralFloating+  , parseLiteralChar+  , parseLiteralString+  ) where++import Control.Applicative (asum)+import Control.Monad (replicateM, void)+import Data.Bits (shiftR, (.&.))+import Data.ByteString (ByteString)+import Data.ByteString qualified as BS+import Data.ByteString.Builder qualified as Builder+import Data.ByteString.Lazy qualified as BSL+import Data.Char (chr, ord, toLower)+import Data.List (unfoldr)+import Data.Maybe (catMaybes, fromMaybe, mapMaybe)+import Data.Scientific qualified as Scientific+import Data.Word (Word8)+import Foreign.C (CChar)+import GHC.Generics (Generic)+import Numeric.Natural (Natural)+import Text.Parsec (ParsecT, Stream, char, choice, many, many1, option,+                    optionMaybe, satisfy, tokenPrim, try, unexpected)+import Text.Parsec.Pos (updatePosChar)++import C.Type qualified as Runtime++import C.Expr.Parse.Infra (TokenParser)+import C.Expr.Util.Parsec (caseInsensitive', satisfyWith)++{-------------------------------------------------------------------------------+  Parser for integer literals++  Reference: <https://en.cppreference.com/w/cpp/language/integer_literal>+-------------------------------------------------------------------------------}++data IntSuffix =+    IntSuffixUnsigned+  | IntSuffixLong+  | IntSuffixLongLong+  | IntSuffixSize+  deriving stock (Eq, Show, Generic)++intSuffix :: TokenParser IntSuffix+intSuffix = choice [+      IntSuffixUnsigned <$ caseInsensitive' "u"+    , IntSuffixLongLong <$ caseInsensitive' "ll"+    , IntSuffixLong     <$ caseInsensitive' "l"+    , IntSuffixSize     <$ caseInsensitive' "z"+    ]++parseLiteralInteger :: TokenParser (Integer, Runtime.IntLikeType)+parseLiteralInteger = do+    (b, ds, suffixes) <- aux++    let val = readInBase b ds++        ty = case suffixes of+          [] -> Runtime.Int Runtime.Signed+          _  ->+            let sign = if any ( == IntSuffixUnsigned ) suffixes+                       then Runtime.Unsigned+                       else Runtime.Signed+                long     = any ( == IntSuffixLong ) suffixes+                longlong = any ( == IntSuffixLongLong ) suffixes+             in+                if | longlong+                   -> Runtime.LongLong sign+                   | long+                   -> Runtime.Long sign+                   | otherwise+                   -> Runtime.Int sign++    return (fromIntegral val, ty)+  where+    aux :: TokenParser (Base, [Digit], [IntSuffix])+    aux = asum [+          try $ do+            b  <- base+            ds <- many1 $ digitInBase True b+            ss <- many intSuffix+            return (b, ds, ss)+        , do+            let b = BaseDec+            ds <- many1 $ digitInBase True b+            ss <- many intSuffix+            return (b, ds, ss)+        ]++readInBase :: Base -> [Digit] -> Natural+readInBase b ds =+  let+    multipliers = iterate (* baseToNat b) 1+  in+    sum $ zipWith (*) (reverse $ mapMaybe getDigit ds) multipliers++{-------------------------------------------------------------------------------+  Parser for floating-point literals++  Reference: <https://en.cppreference.com/w/cpp/language/floating_literal>+-------------------------------------------------------------------------------}++parseLiteralFloating :: TokenParser (Float, Double, Runtime.FloatingType)+parseLiteralFloating = do++  b     <- option BaseDec (BaseHex <$ caseInsensitive' "0x")+  as    <- many (digitInBase True b)+  mbXs  <- optionMaybe $ do { void (char '.') ; many (digitInBase True b) }+  mbExp <-+    case b of+      -- Exponent is non-optional with hexadecimal base+      BaseHex -> Just <$> parseExponent b+      _       -> optionMaybe (parseExponent b)++  if+    | Nothing <- mbXs+    , Nothing <- mbExp+    -> unexpected $ "cannot parse floating-point value: expected either '.' or '" ++ exponentText b ++ "'"+    | null as+    , case mbXs of { Nothing -> True; Just [] -> True; _ -> False }+    -> unexpected $ "cannot parse floating-point value without any digits"+    | otherwise+    -> do ty <- choice+            [ Runtime.FloatType <$ caseInsensitive' "f"+            , do { void $ caseInsensitive' "l"+                 ; unexpected "no support for long double literals"+                 }+            , pure Runtime.DoubleType+            ]+          let m :: Natural+              m = readInBase b (as ++ fromMaybe [] mbXs)+              e :: Int+              e = fromMaybe 0 mbExp - maybe 0 length mbXs+          return (fromScientific m e, fromScientific m e, ty)++fromScientific :: forall a. RealFloat a => Natural -> Int -> a+fromScientific m e =+  Scientific.toRealFloat $ Scientific.scientific (fromIntegral m) e++parseExponent :: Base -> TokenParser Int+parseExponent b = do+  void (caseInsensitive' $ exponentText b)+  s <- parseSign+  ds <- many (digitInBase True BaseDec)+  return $ applySign s (fromIntegral $ readInBase BaseDec ds)++exponentText :: Base -> String+exponentText BaseHex = "p"+exponentText _ = "e"++data Sign = Neg | Pos+  deriving stock ( Eq, Ord, Show )++parseSign :: TokenParser Sign+parseSign = choice+  [ Pos <$ char '+'+  , Neg <$ char '-'+  , return Pos+  ]++applySign :: Num a => Sign -> a -> a+applySign Neg x = negate x+applySign Pos x = x++{-------------------------------------------------------------------------------+  Auxiliary: integer representations in different bases+-------------------------------------------------------------------------------}++data Base =+    BaseDec+  | BaseOct+  | BaseHex+  | BaseBin+  deriving stock (Show)++baseToNat :: Base -> Natural+baseToNat BaseDec = 10+baseToNat BaseOct = 8+baseToNat BaseBin = 2+baseToNat BaseHex = 16++-- | Digit in a given base+data Digit = Digit Natural | Separator+  deriving stock (Show)++getDigit :: Digit -> Maybe Natural+getDigit (Digit i) = Just i+getDigit Separator = Nothing++base :: TokenParser Base+base = choice [+      BaseHex <$ caseInsensitive' "0x"+    , BaseBin <$ caseInsensitive' "0b"+    , BaseOct <$ caseInsensitive' "0"+    ]++-- | Parse digit in the given base+--+-- Returns the value of the digit, of 'Nothing' for single quotes+-- (which are allowed as a separator between digits).+digitInBase :: Bool -> Base -> TokenParser Digit+digitInBase allowSeparator = satisfyWith . (. toLower) . aux+  where+    aux :: Base -> Char -> Maybe Digit+    aux BaseDec c+      | c >= '0' && c <= '9' = Just . Digit $ c `relativeTo` '0'+    aux BaseBin c+      | c >= '0' && c <= '1' = Just . Digit $ c `relativeTo` '0'+    aux BaseOct c+      | c >= '0' && c <= '7' = Just . Digit $ c `relativeTo` '0'+    aux BaseHex c+      | c >= '0' && c <= '9' = Just . Digit $ c `relativeTo` '0'+      | c >= 'a' && c <= 'f' = Just . Digit $ c `relativeTo` 'a' + 10++    aux _ '\''+      | allowSeparator+      = Just $ Separator+    aux _ _+      = Nothing++    relativeTo :: Char -> Char -> Natural+    relativeTo c r = fromIntegral $ ord c - ord r++digitChar :: Digit -> Maybe Char+digitChar (Digit i)+  | i < 0+  = Nothing+  | i <= 9+  = Just $ chr (ord '0' + fromIntegral i)+  | i <= 35+  = Just $ chr (ord 'A' + fromIntegral i - 10)+  | otherwise+  = Nothing+digitChar Separator = Nothing++{-------------------------------------------------------------------------------+  Parser for character literals++  Reference: <https://en.cppreference.com/w/c/language/character_constant>+-------------------------------------------------------------------------------}++-- | Re-parse a character literal into a single byte.+--+-- Only single-byte character literals are supported: the result is the byte+-- value that a C compiler would assign to the literal.  This is the value+-- embedded in the generated Haskell binding, which may be passed directly to+-- C code expecting that same byte.+--+-- The libclang token text is a 'String' of Unicode code points (UTF-8-decoded).+-- We parse the C escape syntax and verify the resulting code point fits in one+-- byte (see 'parseLiteralString' for the analogous three-layer approach).+--+-- Note that, in C, character literals have type @int@, **not** @char@!+--+-- We reject wide literals (@L@\/@u@\/@U@\/@u8@ prefix), multi-character+-- constants, code points above @0xFF@, and numeric escapes that overflow a byte.+parseLiteralChar :: TokenParser CChar+parseLiteralChar = do+  prefix <- parseCharPrefix+  case prefix of+    Just {} ->+      -- TODO <https://github.com/well-typed/c-expr/issues/2>+      -- Support prefixed character literals.+      unexpected "wide character literals are not supported"+    Nothing -> do+      void $ char '\''+      chars <- many1 $ choice [nonEscapedChar ['\''], escapedChar]+      void $ char '\''+      case chars of+        [c] ->+          if ord c <= 0xFF+            then return (fromIntegral (ord c))+            else unexpected "character literal value does not fit in a byte"+        _ ->+          unexpected "multi-character literal"++-- | Parse a single unescaped source character.+nonEscapedChar :: [Char] -> TokenParser Char+nonEscapedChar forbidden =+  satisfy ( not . ( `elem` '\n' : '\\' : forbidden ) )++data CharPrefix = Prefix_u8 | Prefix_u | Prefix_U | Prefix_L++parseCharPrefix :: TokenParser ( Maybe CharPrefix )+parseCharPrefix = choice+  [ do { c 'u' ; c '8'; return (Just Prefix_u8) }+  , do { c 'u';         return (Just Prefix_u) }+  , do { c 'U';         return (Just Prefix_U) }+  , do { c 'L';         return (Just Prefix_L) }+  , return Nothing+  ]+  where+    c = void . char++-- | Parse a single escaped character.+--+-- Numeric escapes that do not fit in a single byte are rejected, as they have+-- an implementation-defined value in C (see 'parseLiteralChar').+escapedChar :: TokenParser Char+escapedChar = do+  void $ char '\\'+  choice+    [ basicEscapedChar+    , numericCodeUnit hexCodeUnit+    , numericCodeUnit octalCodeUnit+    , chr . fromIntegral <$> universalCodePoint+    ]+  where+    numericCodeUnit p = do+      codeUnit <- p+      if codeUnit <= 0xFF+        then return $ chr ( fromIntegral codeUnit )+        else unexpected "character literal with implementation-defined value"++basicEscapedChar :: TokenParser Char+basicEscapedChar =+  satisfyM ( `lookup` ( basicSourceEscapedChars ++ executionEscapedChars ) )++-- | Like 'Text.Parsec.satisfy' but takes a @Char -> Maybe a@ predicate.+satisfyM :: Stream s m Char => (Char -> Maybe a) -> ParsecT s u m a+{-# INLINABLE satisfyM #-}+satisfyM f = tokenPrim+  (\c -> show [c])+  (\pos c _cs -> updatePosChar pos c)+  (\c -> f c)++-- | Escape sequences of basic (source) characters.+--+-- See https://en.cppreference.com/w/c/language/charset.+basicSourceEscapedChars :: [(Char, Char)]+basicSourceEscapedChars =+  [ ( '\'', '\'' )  -- single quote+  , ( '\"', '\"' )  -- double quote+  , ( '?' , '?'  )  -- question mark+  , ( '\\', '\\' )  -- backslash+  , ( 'f' , '\f'  ) -- form feed - new page+  , ( 't' , '\t'  ) -- horizontal tab+  , ( 'v' , '\v'  ) -- vertical tab+  ]++-- | Escape sequences of execution characters.+--+-- See https://en.cppreference.com/w/c/language/charset.+--+-- Note: @\\0@ is NOT listed here. It is an octal escape (value 0) and is+-- handled by 'octalCodeUnit'. Listing it here would cause @\\00@ / @\\000@+-- to be mis-parsed: the named escape would consume only the first @0@, leaving+-- the remaining digits to be interpreted as ordinary characters.+executionEscapedChars :: [(Char, Char)]+executionEscapedChars =+  [ ( 'a', '\a'   ) -- audible bell+  , ( 'b', '\b'   ) -- backspace+  , ( 'n', '\n'   ) -- line feed - new line+  , ( 'r', '\r'   ) -- carriage return+  ]++-- | Parse the value of a hexadecimal escape sequence (@\\xH...@).+hexCodeUnit :: TokenParser Natural+hexCodeUnit = do+  void $ char 'x'+  digs <- many1 (digitInBase False BaseHex)+  return $ readInBase BaseHex digs++-- | Parse the value of an octal escape sequence (@\\N@, @\\NN@ or @\\NNN@).+octalCodeUnit :: TokenParser Natural+octalCodeUnit = do+  -- NB (https://en.cppreference.com/w/c/language/escape):+  --+  -- Octal escape sequences have a length limit of three octal digits,+  -- but terminate at the first character that is not a valid octal digit+  -- if encountered sooner.+  dig1 <- digitInBase False BaseOct+  dig2 <- option Nothing (Just <$> digitInBase False BaseOct)+  dig3 <- option Nothing (Just <$> digitInBase False BaseOct)+  let+    digs :: [Digit]+    digs = dig1 : catMaybes [dig2, dig3]+  return $ readInBase BaseOct digs++-- | Parse and validate a universal character name (@\\uHHHH@ or+-- @\\UHHHHHHHH@), returning its Unicode code point.+universalCodePoint :: TokenParser Natural+universalCodePoint = do+  nbChars <- choice [4 <$ char 'u', 8 <$ char 'U']+  digs <- replicateM nbChars (digitInBase False BaseHex)+  let codePoint = readInBase BaseHex digs+      showCodePoint = mapMaybe digitChar digs++  -- See 'Range of universal character names' in https://en.cppreference.com/w/c/language/escape+  if | codePoint < 0xA0 && not (codePoint `elem` [0x24, 0x40, 0x60]) -- '$', '@', '`'+     -> unexpected $ "universal character names cannot refer to basic characters (" ++ showCodePoint ++ ")"+     | codePoint >= 0xD800 && codePoint < 0xDFFF+     -> unexpected $ "universal character names cannot refer to surrogate code points (" ++ showCodePoint ++ ")"+     | codePoint >= 0x10FFFF+     -> unexpected $ "universal character name is not a valid Unicode code point (" ++ showCodePoint ++ ")"+     | otherwise+     -> return codePoint++{-------------------------------------------------------------------------------+  Parser for string literals++  Reference: <https://en.cppreference.com/w/c/language/string_literal>+-------------------------------------------------------------------------------}++-- | Re-parse a string literal into its execution-encoding bytes.+--+-- The result is /bit-for-bit accurate/: the returned 'ByteString' contains+-- exactly the bytes that a C compiler targeting a UTF-8 execution charset would+-- store for this literal.  This matters because the generated Haskell bindings+-- may be passed directly to C functions that expect that same byte sequence.+--+-- The libclang token text is a 'String' of Unicode code points (UTF-8-decoded).+-- We apply a three-layer translation, e.g. for @\"你\\x41\"@:+--+--   1. /C source/ (UTF-8): raw byte sequence from the source file.+--   2. /Decoded/ ('String'): @['你', '\\\\', 'x', '4', '1']@ between the quotes.+--   3. /Execution encoding/ ('ByteString'): @[\<UTF-8 for 你\>, 0x41]@+--+-- Plain code points (including @\\uXXXX@) are UTF-8-encoded.  Numeric escapes+-- (@\\xNN@, @\\NNN@) contribute their raw code-unit bytes directly — they are+-- /not/ re-encoded as UTF-8.  This is what makes the output bit-for-bit+-- accurate: @\"\\xE3\\x81\\x82\"@ and @\"あ\"@ both yield the same three+-- bytes @[0xE3, 0x81, 0x82]@.+parseLiteralString :: TokenParser ByteString+parseLiteralString = do+  prefix <- parseCharPrefix+  case prefix of+    Just {} ->+      -- TODO <https://github.com/well-typed/c-expr/issues/2>+      -- Support prefixed string literals.+      unexpected "unsupported string literal prefix"+    Nothing -> do+      void $ char '\"'+      cs <- many $ choice [nonEscapedByte ['\"'], escapedByte]+      void $ char '\"'+      return $ BS.pack $ concat cs++-- | Parse a single unescaped source character, as its UTF-8 bytes.+nonEscapedByte :: [Char] -> TokenParser [Word8]+nonEscapedByte forbidden = utf8EncodeChar <$> nonEscapedChar forbidden++-- | Parse a single escaped character, as its UTF-8 bytes.+escapedByte :: TokenParser [Word8]+escapedByte = do+  void $ char '\\'+  choice+    [ utf8EncodeChar      <$> basicEscapedChar+    , codeUnitBytes       <$> hexCodeUnit+    , codeUnitBytes       <$> octalCodeUnit+    , utf8EncodeCodePoint <$> universalCodePoint+    ]++{-------------------------------------------------------------------------------+  Character encoding+-------------------------------------------------------------------------------}++-- | UTF-8-encode a 'Char'.+utf8EncodeChar :: Char -> [Word8]+utf8EncodeChar = BSL.unpack . Builder.toLazyByteString . Builder.charUtf8++-- | UTF-8-encode a Unicode code point.+--+-- The code point must be valid (@<= 0x10FFFF@); 'universalCodePoint' is the+-- only producer and validates this.+utf8EncodeCodePoint :: Natural -> [Word8]+utf8EncodeCodePoint = utf8EncodeChar . chr . fromIntegral++-- | The big-endian bytes of a numeric code unit value, e.g. the value of+-- @\\1\\2\\3\\4@ is @0x01020304@. The zero value produces a single null byte.+--+-- This is C numeric-escape semantics, not a UTF-8 encoding.+codeUnitBytes :: Natural -> [Word8]+codeUnitBytes 0 = [0]+codeUnitBytes n = reverse . unfoldr step $ n+  where+    step 0 = Nothing+    step x = Just (fromIntegral (x .&. 0xFF), x `shiftR` 8)
+ src/C/Expr/Syntax.hs view
@@ -0,0 +1,89 @@+{-# LANGUAGE CPP #-}++#if __GLASGOW_HASKELL__ >=908+{-# LANGUAGE TypeAbstractions #-}+#endif++-- | The syntax for macros recognized+--+-- Intended for unqualified import.+module C.Expr.Syntax (+    -- * Definition+    Macro(..)+    -- ** Type syntax+  , TypeLit(..)+  , Sign(..)+  , IntSize(..)+  , FloatSize(..)+    -- ** Expressions+  , Identifier(..)+  , TagKind(..)+  , Name(..)+  , Expr(..)+  , TyQual(..)+  , VaFun(..)+  , ValueLit(..)+  , Literal(..)+  , Term(..)+    -- ** Literals+  , IntegerLiteral(..)+  , FloatingLiteral(..)+  , CharLiteral(..)+  , StringLiteral(..)+  , canBeRepresentedAsRational+    -- ** Annotations+  , Pass+  , Ps+  , XVar(..)+  , XApp(..)+  , fmapExpr+  , annotateMacro+  , annotateExpr+  ) where++import Control.Monad.Identity (Identity (runIdentity))+import Data.Kind qualified as Hs+import Data.Type.Equality ((:~:) (..))+import Data.Type.Nat qualified as Nat+import Data.Vec.Lazy (Vec, withDict)+import DeBruijn (Ctx)++import C.Expr.Syntax.Expr+import C.Expr.Syntax.Identifier+import C.Expr.Syntax.Literal+import C.Expr.Syntax.Name+import C.Expr.Syntax.TTG+import C.Expr.Syntax.TTG.Parse+import C.Expr.Syntax.Type++import Clang.HighLevel.Types++type Macro :: Hs.Type -> Hs.Type+data Macro ann = forall (ctx :: Ctx). Macro {+      macroLoc    :: MultiLoc+    , macroName   :: Identifier+    , macroParams :: Vec ctx Identifier+    , macroExpr   :: Expr ctx (Ps ann)+    }++instance Eq ann => Eq (Macro ann) where+  (Macro @_ @c1 loc1 n1 p1 e1) == (Macro @_ @c2 loc2 n2 p2 e2) =+      loc1 == loc2 && n1   == n2 && eqBody+    where+      eqBody = withDict p1 $ withDict p2 $+        case Nat.eqNat @c1 @c2 of+          Just Refl -> p1 == p2 && e1 == e2+          Nothing   -> False++deriving stock instance (Show ann) => Show (Macro ann)++instance Functor Macro where+  fmap f = runIdentity . annotateMacro (\_name -> pure . f)++annotateMacro ::+     Applicative m+  => (Name -> ann -> m ann')+  -> Macro ann+  -> m (Macro ann')+annotateMacro f Macro{macroLoc, macroName, macroParams, macroExpr} =+    Macro macroLoc macroName macroParams <$> annotateExpr f macroExpr
+ src/C/Expr/Syntax/Expr.hs view
@@ -0,0 +1,282 @@+{-# LANGUAGE CPP #-}++#if __GLASGOW_HASKELL__ >=908+{-# LANGUAGE TypeAbstractions #-}+#endif++module C.Expr.Syntax.Expr (+    -- * Expressions+    Expr(..)+  , TyQual(..)+  , VaFun(..)+  , ValueLit(..)+  , Literal(..)+  , Term(..)+    -- * Annotations+  , fmapExpr+  , annotateExpr+  ) where++import Control.Monad.Identity+import Data.GADT.Compare (GEq (geq))+import Data.Kind+import Data.Nat (Nat (..))+import Data.Proxy+import Data.Type.Equality (type (:~:) (..))+import Data.Type.Nat (SNatI)+import Data.Type.Nat qualified as Nat+import Data.Vec.Lazy (Vec (..))+import Data.Vec.Lazy qualified as Vec+import DeBruijn (Ctx, Idx)+import GHC.Generics (Generic)++import C.Expr.Syntax.Literal+import C.Expr.Syntax.Name+import C.Expr.Syntax.TTG+import C.Expr.Syntax.TTG.Parse+import C.Expr.Syntax.Type+import C.Expr.Util.TestEquality++{-------------------------------------------------------------------------------+  Expressions+-------------------------------------------------------------------------------}++-- | Macro expression+--+-- For examples, see the extensive test suite "Test.CExpr.Parse".+type Expr :: Ctx -> Pass -> Type+data Expr ctx p+  -- | A term that is not a function application.+  = Term ( Term ctx p )+  -- | Exactly saturated non-nullary type-level function application.+  --+  -- We don't need an extension point here, because we do not need to evaluate+  -- type functions in Haskell. 'XApp' may be unnecessary if we can remove+  -- 'C.Expr.Typecheck.Type.FunValue'.+  | forall n. TyApp             ( TyQual ( S n ) ) ( Vec ( S n ) ( Expr ctx p ) )+  -- | Exactly saturated non-nullary function application.+  | forall n. VaApp !( XApp p ) ( VaFun ( S n ) ) ( Vec ( S n ) ( Expr ctx p ) )+deriving stock instance ( Show ( XVar p ), Show ( XApp p ) ) => Show ( Expr ctx p )++instance ( Eq ( XApp p ), Eq ( XVar p ) ) => Eq ( Expr ctx p ) where+  Term m1 == Term m2 = m1 == m2+  TyApp f1 args1 == TyApp f2 args2+    | Just Refl <- f1 `equals1` f2+    = args1 == args2+    | otherwise+    = False+  VaApp x1 f1 args1 == VaApp x2 f2 args2+    | Just Refl <- f1 `equals1` f2+    = x1 == x2 && args1 == args2+    | otherwise+    = False+  _ == _ = False++instance ( Ord ( XApp p ), Ord ( XVar p ) ) => Ord ( Expr ctx p ) where+  compare ( Term m1 ) ( Term m2 ) = compare m1 m2+  compare ( TyApp @_ @_ @n1 f1 args1 ) ( TyApp @_ @_ @n2 f2 args2 ) =+    Vec.withDict args1 $ Vec.withDict args2 $+    case Nat.eqNat @( S n1 ) @( S n2 ) of+      Just Refl -> compare f1 f2 <> compare args1 args2+      Nothing ->+        compare ( Nat.reflect @( S n1 ) Proxy ) ( Nat.reflect @( S n2 ) Proxy )+  compare ( VaApp @_ @_ @n1 x1 f1 args1 ) ( VaApp @_ @_ @n2 x2 f2 args2 ) =+    Vec.withDict args1 $ Vec.withDict args2 $+    case Nat.eqNat @( S n1 ) @( S n2 ) of+      Just Refl -> compare f1 f2 <> compare x1 x2 <> compare args1 args2+      Nothing ->+        compare ( Nat.reflect @( S n1 ) Proxy ) ( Nat.reflect @( S n2 ) Proxy )+  compare (Term {}) (TyApp {}) = LT+  compare (Term {}) (VaApp {}) = LT+  compare (TyApp {}) (Term {}) = GT+  compare (VaApp {}) (Term {}) = GT+  compare (TyApp {}) (VaApp {}) = LT+  compare (VaApp {}) (TyApp {}) = GT++{-------------------------------------------------------------------------------+  Functions+-------------------------------------------------------------------------------}++-- | Type qualifier+data TyQual arity where+  -- | Pointer+  Pointer :: TyQual ( S Z )+  -- | Const+  Const   :: TyQual ( S Z )++  -- NB: make sure to update 'instance GEq TyFun'+  -- when adding a new constructor.++deriving stock instance Show ( TyQual arity )+deriving stock instance Eq   ( TyQual arity )+deriving stock instance Ord  ( TyQual arity )++instance GEq TyQual where+  geq Pointer Pointer = Just Refl+  geq Const   Const   = Just Refl+  geq _        _        = Nothing++data VaFun arity where+  -- | @+@+  MUnaryPlus  :: VaFun ( S Z )+  -- | @-@+  MUnaryMinus :: VaFun ( S Z )+  -- | @!@+  MLogicalNot :: VaFun ( S Z )+  -- | @~@+  MBitwiseNot :: VaFun ( S Z )+  -- | @*@+  MMult       :: VaFun ( S ( S Z ) )+  -- | @/@+  MDiv        :: VaFun ( S ( S Z ) )+  -- | @%@+  MRem        :: VaFun ( S ( S Z ) )+  -- | @+@+  MAdd        :: VaFun ( S ( S Z ) )+  -- | @-@+  MSub        :: VaFun ( S ( S Z ) )+  -- | @<<@+  MShiftLeft  :: VaFun ( S ( S Z ) )+  -- | @>>@+  MShiftRight :: VaFun ( S ( S Z ) )+  -- | @<@+  MRelLT      :: VaFun ( S ( S Z ) )+  -- | @<=@+  MRelLE      :: VaFun ( S ( S Z ) )+  -- | @>@+  MRelGT      :: VaFun ( S ( S Z ) )+  -- | @>=@+  MRelGE      :: VaFun ( S ( S Z ) )+  -- | @==@+  MRelEQ      :: VaFun ( S ( S Z ) )+  -- | @!=@+  MRelNE      :: VaFun ( S ( S Z ) )+  -- | @&@+  MBitwiseAnd :: VaFun ( S ( S Z ) )+  -- | @^@+  MBitwiseXor :: VaFun ( S ( S Z ) )+  -- | @|@+  MBitwiseOr  :: VaFun ( S ( S Z ) )+  -- | @&&@+  MLogicalAnd :: VaFun ( S ( S Z ) )+  -- | @||@+  MLogicalOr  :: VaFun ( S ( S Z ) )+  -- | Tuples+  MTuple      :: SNatI n => VaFun ( S ( S n ) )++  -- NB: make sure to update 'instance GEq TyFun'+  -- when adding a new constructor.++deriving stock instance Show ( VaFun arity )+deriving stock instance Eq   ( VaFun arity )+deriving stock instance Ord  ( VaFun arity )++instance GEq VaFun where+  geq MUnaryPlus  MUnaryPlus  = Just Refl+  geq MUnaryMinus MUnaryMinus = Just Refl+  geq MLogicalNot MLogicalNot = Just Refl+  geq MBitwiseNot MBitwiseNot = Just Refl+  geq MMult       MMult       = Just Refl+  geq MDiv        MDiv        = Just Refl+  geq MRem        MRem        = Just Refl+  geq MAdd        MAdd        = Just Refl+  geq MSub        MSub        = Just Refl+  geq MShiftLeft  MShiftLeft  = Just Refl+  geq MShiftRight MShiftRight = Just Refl+  geq MRelLT      MRelLT      = Just Refl+  geq MRelLE      MRelLE      = Just Refl+  geq MRelGT      MRelGT      = Just Refl+  geq MRelGE      MRelGE      = Just Refl+  geq MRelEQ      MRelEQ      = Just Refl+  geq MRelNE      MRelNE      = Just Refl+  geq MBitwiseAnd MBitwiseAnd = Just Refl+  geq MBitwiseXor MBitwiseXor = Just Refl+  geq MBitwiseOr  MBitwiseOr  = Just Refl+  geq MLogicalAnd MLogicalAnd = Just Refl+  geq MLogicalOr  MLogicalOr  = Just Refl+  geq (MTuple @i) (MTuple @j)+    | Just Refl <- Nat.eqNat @i @j+    = Just Refl+  geq _           _           = Nothing++{-------------------------------------------------------------------------------+  Terms+-------------------------------------------------------------------------------}++-- | Value literal+data ValueLit =+    ValueInt    IntegerLiteral+  | ValueFloat  FloatingLiteral+  | ValueChar   CharLiteral+  | ValueString StringLiteral+  deriving stock (Eq, Ord, Show)++type Literal :: Type+data Literal =+    TypeLit  TypeLit++  | ValueLit ValueLit+  deriving stock (Eq, Ord, Show)++type Term :: Ctx -> Pass -> Type+data Term ctx p =+    -- | Literal (i.e., constant) type or value+    Literal Literal++    -- | Reference to a function parameter+    --+    -- The De Bruijn index of a parameter of the enclosing function-like+    -- macro. For example, the second @X@ in @#define F(X) X + 1@, with index 0.+    --+    -- The language defined in @c-expr-dsl@ is a first-order language, so there+    -- is no need for arguments. For example, we do not support+    -- @#define MACRO(F,X) F(X)@.+  | LocalParam (Idx ctx)++    -- | Free variable: another macro or typedef+  | Var ( XVar p ) Name [Expr ctx p]+  deriving stock Generic+deriving stock instance ( Eq   ( XApp p ), Eq   ( XVar p ) ) => Eq   ( Term ctx p )+deriving stock instance ( Ord  ( XApp p ), Ord  ( XVar p ) ) => Ord  ( Term ctx p )+deriving stock instance ( Show ( XApp p ), Show ( XVar p ) ) => Show ( Term ctx p )++{-------------------------------------------------------------------------------+  Annotations+-------------------------------------------------------------------------------}++fmapExpr :: (ann -> ann') -> Expr ctx (Ps ann) -> Expr ctx (Ps ann')+fmapExpr f = runIdentity . annotateExpr (\_name -> pure . f)++annotateExpr ::+     forall m ctx ann ann'.+     Applicative m+  => (Name -> ann -> m ann')+  -> Expr ctx (Ps ann)+  -> m (Expr ctx (Ps ann'))+annotateExpr f = \case+    Term t           -> Term              <$> annotateTerm f t+    TyApp qual args  -> TyApp qual        <$> traverse (annotateExpr f) args+    VaApp x fun args -> VaApp (aux x) fun <$> traverse (annotateExpr f) args+  where+    aux :: XApp (Ps ann) -> XApp (Ps ann')+    aux NoXApp = NoXApp++annotateTerm ::+     forall m ctx ann ann'.+     Applicative m+  => (Name -> ann -> m ann')+  -> Term ctx (Ps ann)+  -> m (Term ctx (Ps ann'))+annotateTerm f = \case+    Literal lit ->+      pure $ Literal lit+    LocalParam param ->+      pure $ LocalParam param+    Var ann nm args  ->+      pure Var+        <*> aux nm ann+        <*> pure nm+        <*> traverse (annotateExpr f) args+  where+    aux :: Name -> XVar (Ps ann) -> m (XVar (Ps ann'))+    aux nm' (XVarPs ann) = XVarPs <$> f nm' ann
+ src/C/Expr/Syntax/Identifier.hs view
@@ -0,0 +1,22 @@+module C.Expr.Syntax.Identifier (+    Identifier(..)+  ) where++import Data.String+import Data.Text (Text)+import GHC.Generics (Generic)++{-------------------------------------------------------------------------------+  Definition+-------------------------------------------------------------------------------}++-- | A C identifier+--+-- Used for any name in macro source: macro parameters, free variables, typedef+-- names, and the identifier part of a tagged type (e.g. the @Foo@ in+-- @struct Foo@).+newtype Identifier = Identifier {+      getIdentifier :: Text+    }+  deriving newtype (Show, Eq, Ord, IsString, Semigroup)+  deriving stock (Generic)
+ src/C/Expr/Syntax/Literal.hs view
@@ -0,0 +1,82 @@+module C.Expr.Syntax.Literal (+    IntegerLiteral(..)+  , FloatingLiteral(..)+  , CharLiteral(..)+  , StringLiteral(..)+    -- * Auxiliary+  , canBeRepresentedAsRational+  ) where++import Data.ByteString (ByteString)+import Foreign.C (CChar)+import GHC.Generics (Generic)++import C.Type qualified as Runtime++{-------------------------------------------------------------------------------+  Definition+-------------------------------------------------------------------------------}++-- | Integer literal+data IntegerLiteral =+  IntegerLiteral {+      -- | The type of the integer literal, as determined from suffixes.+      integerLiteralType  :: Runtime.IntLikeType++      -- | The (parsed) value of the literal+    , integerLiteralValue :: Integer+    }+  deriving stock ( Eq, Ord, Show, Generic )++-- | Floating-point literal+data FloatingLiteral =+  FloatingLiteral {+      -- | The type of the floating-point literal, as determined from suffixes.+      floatingLiteralType  :: Runtime.FloatingType++      -- | The (parsed) value of the literal, when parsed as a single precision+      -- floating-point value.+    , floatingLiteralFloatValue :: Float++      -- | The (parsed) value of the literal, when parsed as a double precision+      -- floating-point value.+    , floatingLiteralDoubleValue :: Double+    }+  deriving stock ( Eq, Ord, Show, Generic )++-- | A C character literal.+--+-- The value is represented as a 'CChar'. Wide character literals (prefixed+-- with @L@, @u@, @U@, or @u8@) and characters whose value does not fit in a+-- single byte are rejected during parsing (see+-- 'C.Expr.Parse.Literal.parseLiteralChar').+newtype CharLiteral = CharLiteral { charLiteralValue :: CChar }+  deriving stock ( Eq, Ord, Show, Generic )++-- | A C string literal.+--+-- 'stringLiteralValue' holds the /execution-encoding bytes/ of the literal,+-- assuming a UTF-8 execution character set.  The representation is+-- /bit-for-bit accurate/: the bytes are exactly what a C compiler targeting a+-- UTF-8 execution charset would embed in the object file.  This property is+-- required because the generated Haskell bindings may be passed directly to C+-- functions that expect the same byte sequence (see+-- 'C.Expr.Parse.Literal.parseLiteralString' for the encoding rules).+newtype StringLiteral = StringLiteral { stringLiteralValue :: ByteString }+  deriving stock ( Eq, Ord, Show, Generic )++{-------------------------------------------------------------------------------+  Auxiliary functions+-------------------------------------------------------------------------------}++{-# SPECIALISE canBeRepresentedAsRational :: Float  -> Bool #-}+{-# SPECIALISE canBeRepresentedAsRational :: Double -> Bool #-}++-- | Can this floating-point value be represented (losslessly) as a 'Rational'?+canBeRepresentedAsRational :: RealFloat a => a -> Bool+canBeRepresentedAsRational f = not $ or+  [ isNaN f+  , isInfinite f+  , isNegativeZero f+  , isDenormalized f -- not strictly necessary, but let's be conservative+  ]
+ src/C/Expr/Syntax/Name.hs view
@@ -0,0 +1,15 @@+module C.Expr.Syntax.Name (+    TagKind(..)+  , Name(..)+  ) where++import C.Expr.Syntax.Identifier++-- | Tag kind for elaborated types+data TagKind = TagStruct | TagUnion | TagEnum+  deriving stock (Eq, Ord, Show)++data Name =+    NameOrdinary Identifier+  | NameTagged   Identifier TagKind+  deriving stock (Eq, Ord, Show)
+ src/C/Expr/Syntax/TTG.hs view
@@ -0,0 +1,33 @@+module C.Expr.Syntax.TTG (+    Pass+    -- * TTG-style type families+  , XApp+  , XVar+  ) where++import Data.Kind++{-------------------------------------------------------------------------------+  Definition+-------------------------------------------------------------------------------}++-- | Kind of passes+--+-- Example:+--+-- > type Ps :: Pass+-- > data Ps a+type Pass = PassSimulatedOpenKind -> Type++-- | Internal type used only to simulate an open kind. Not exported.+data PassSimulatedOpenKind++{-------------------------------------------------------------------------------+  TTG-style type families+-------------------------------------------------------------------------------}++type XApp :: Pass -> Type+type XVar :: Pass -> Type++data family XApp p+data family XVar p
+ src/C/Expr/Syntax/TTG/Parse.hs view
@@ -0,0 +1,32 @@+module C.Expr.Syntax.TTG.Parse (+    Ps+  , XApp(..)+  , XVar(..)+  ) where++import Data.Kind qualified as Hs+import GHC.Generics (Generic)++import C.Expr.Syntax.TTG++{-------------------------------------------------------------------------------+  Definition+-------------------------------------------------------------------------------}++-- | The parse pass.+--+-- 'Ps' is parameterised by an annotation type @ann@ (attached to each 'XVar'),+-- so the embedding application can thread its own per-variable data through the+-- parsed tree.+type Ps :: Hs.Type -> Pass+data Ps ann a++{-------------------------------------------------------------------------------+  Pass-indexed type families+-------------------------------------------------------------------------------}++data instance XApp (Ps ann) = NoXApp deriving stock ( Eq, Ord, Show, Generic )+data instance XVar (Ps ann) = XVarPs {+    psAnn :: ann+  }+  deriving stock ( Eq, Ord, Show, Generic )
+ src/C/Expr/Syntax/TTG/Typecheck.hs view
@@ -0,0 +1,2 @@+module C.Expr.Syntax.TTG.Typecheck (+  ) where
+ src/C/Expr/Syntax/Type.hs view
@@ -0,0 +1,72 @@+-- | AST for C types as they appear in macro definitions+--+-- This covers the minimum amount of C type syntax needed for @hs-bindgen@:+-- primitive types with sign/size specifiers and references to named types+-- (typedefs / other macro types). Const qualifiers and pointer indirection+-- are represented as 'C.Expr.Syntax.Expr.TyApp' nodes in the expression tree+-- using 'C.Expr.Syntax.Expr.Const' and 'C.Expr.Syntax.Expr.Pointer'.+module C.Expr.Syntax.Type (+    TypeLit(..)+  , Sign(..)+  , IntSize(..)+  , FloatSize(..)+  ) where++import GHC.Generics++{-------------------------------------------------------------------------------+  Definition+-------------------------------------------------------------------------------}++-- | A C type literal as it appears in a macro definition body.+--+-- This is the base type, without const qualifiers or pointer indirections.+-- Those are represented by 'C.Expr.Syntax.Expr.TyApp' nodes wrapping this+-- term in the expression tree.+--+-- Examples:+--+-- > int           => TypeInt Nothing (Just SizeInt)+-- > unsigned long => TypeInt (Just Unsigned) (Just SizeLong)+--+-- Named types (typedefs, type macros) and tagged types (@struct@\/@union@\/@enum@)+-- are not represented here; both parse as 'C.Expr.Syntax.Expr.Var' nodes in+-- the expression layer, and the typechecker decides what they denote.+data TypeLit =+    -- | An integral type: @[signed|unsigned] [short|int|long|long long]@+    --+    -- Both sign and size can be omitted:+    --+    --   * @signed@ alone means @signed int@+    --   * @unsigned@ alone means @unsigned int@+    --   * @short@ alone means @signed short int@+    --   * etc.+    TypeInt !(Maybe Sign) !(Maybe IntSize)++    -- | @[signed|unsigned] char@+  | TypeChar !(Maybe Sign)++    -- | A floating-point type: @float@ or @double@+  | TypeFloat !FloatSize++    -- | @void@+  | TypeVoid++    -- | @_Bool@ or @bool@ (C23)+  | TypeBool+  deriving stock (Eq, Ord, Show, Generic)++data Sign = Signed | Unsigned+  deriving stock (Eq, Ord, Show, Generic)++data IntSize =+    SizeShort      -- ^ @short [int]@+  | SizeInt        -- ^ @int@+  | SizeLong       -- ^ @long [int]@+  | SizeLongLong   -- ^ @long long [int]@+  deriving stock (Eq, Ord, Show, Generic)++data FloatSize =+    SizeFloat    -- ^ @float@+  | SizeDouble   -- ^ @double@+  deriving stock (Eq, Ord, Show, Generic)
+ src/C/Expr/Typecheck.hs view
@@ -0,0 +1,153 @@+{-# LANGUAGE CPP #-}++#if __GLASGOW_HASKELL__ >=908+{-# LANGUAGE TypeAbstractions #-}+#endif++-- | Public entry point for typechecking macros.+module C.Expr.Typecheck (+    tcMacros+  , TypecheckedMacroTypeExpr(..)+  , TypecheckedMacroValueExpr(..)+  , MacroTcResult(..)++    -- * Errors+  , MacroTcError(..)+  , pprMacroTcError+  ) where++import Data.Foldable qualified as Foldable+import Data.Map (Map)+import Data.Map.Strict qualified as Map+import Data.Type.Equality ((:~:) (..))+import Data.Type.Nat qualified as Nat+import Data.Vec.Lazy (Vec)+import Data.Vec.Lazy qualified as Vec+import GHC.Generics++import C.Expr.Syntax+import C.Expr.Typecheck.Expr+import C.Expr.Typecheck.Interface.Type qualified as T+import C.Expr.Typecheck.Interface.Value qualified as V+import C.Expr.Typecheck.Type++-- | Batch-typecheck a sequence of macros+--+-- The macros are processed in order. Each successful macro is added to the+-- internal 'TypeEnv' so that subsequent macros can reference it. A macro that+-- fails to typecheck is /not/ added to the environment; later macros that+-- reference it will fail with an unbound-variable error.+--+-- @typeOfAnn@ projects each variable's parse annotation to its type, if known+-- (e.g. for @typedef@ names the embedder supplies); 'Nothing' falls back to the+-- internal 'TypeEnv' of previously-typechecked macros.+tcMacros ::+     forall ann.+     (ann -> Maybe QuantTy)+     -- ^ See the documentation of 'C.Expr.Typecheck.Type.Tc'.+  -> [Macro ann]+  -> Map Identifier (MacroTcResult ann)+tcMacros typeOfAnn macros =+    let (_, tcRs) = Foldable.foldl' step (Map.empty, Map.empty) macros+    in  tcRs+  where+    step ::+         (TypeEnv, Map Identifier (MacroTcResult ann))+      -> Macro ann+      -> (TypeEnv, Map Identifier (MacroTcResult ann))+    step (env, acc) (Macro _loc name params body) =+      let result :: MacroTcResult ann+          result = tcMacroOne typeOfAnn env name params body+          env' = case result of+            MacroTcTypeExpr cmt ->+              Map.insert name (macroTypeType  cmt) env+            MacroTcValueExpr cmv ->+              Map.insert name (macroValueType cmv) env+            MacroTcError _ ->+              env+      in  (env', Map.insert name result acc)++{-------------------------------------------------------------------------------+  Types+-------------------------------------------------------------------------------}++-- | The macro is a C type expression (e.g., @#define FOO int@).+data TypecheckedMacroTypeExpr ann = TypecheckedMacroTypeExpr{+      macroTypeBody :: T.Expr ann+    , macroTypeType :: QuantTy+    }+  deriving stock (Eq, Show, Generic, Functor, Foldable, Traversable)++-- | The macro is a value expression (e.g., @#define BAR 1@).+data TypecheckedMacroValueExpr ann = forall ctx. TypecheckedMacroValueExpr{+      macroValueParams :: Vec ctx Identifier+    , macroValueBody   :: V.Expr ctx ann+    , macroValueType   :: QuantTy+    }+instance Eq ann => Eq (TypecheckedMacroValueExpr ann) where+  (TypecheckedMacroValueExpr @_ @c1 p1 b1 t1) == (TypecheckedMacroValueExpr @_ @c2 p2 b2 t2) =+    t1 == t2 && (+      Vec.withDict p1 $ Vec.withDict p2 $+        case Nat.eqNat @c1 @c2 of+          Just Refl -> p1 == p2 && b1 == b2+          Nothing   -> False+    )+deriving stock instance Show ann => Show (TypecheckedMacroValueExpr ann)+deriving stock instance Functor     TypecheckedMacroValueExpr+deriving stock instance Foldable    TypecheckedMacroValueExpr+deriving stock instance Traversable TypecheckedMacroValueExpr++-- | The result of typechecking a single macro.+data MacroTcResult ann =+    MacroTcTypeExpr    (TypecheckedMacroTypeExpr  ann)+  | MacroTcValueExpr   (TypecheckedMacroValueExpr ann)+  -- | The @c-expr-dsl@ typechecker rejected the macro.+  | MacroTcError       MacroTcError++deriving stock instance (Show ann) => Show (MacroTcResult ann)+deriving stock instance (Eq   ann) => Eq   (MacroTcResult ann)++{-------------------------------------------------------------------------------+  Internal: typecheck a single macro against a given 'TypeEnv'.+-------------------------------------------------------------------------------}++-- | Typecheck a single macro against a given 'TypeEnv'.+tcMacroOne ::+     forall ctx ann.+     (ann -> Maybe QuantTy)+  -> TypeEnv+  -> Identifier+  -> Vec ctx Identifier+  -> Expr ctx (Ps ann)+  -> MacroTcResult ann+tcMacroOne typeOfAnn tyEnv name params expr =+    case tcExpr tyEnv name params (fmapExpr typeOfAnn expr) of+      Left  err -> MacroTcError err+      Right res -> classify res+  where+    classify :: (Type Ty, Quant (FunValue, Type Ty)) -> MacroTcResult ann+    classify = \case+      (MacroTypeTy, quant)+        | not (Vec.null params) ->+          MacroTcError $+            TcUnsupportedTypeWithLocalParameters name (Vec.toList params)+        | otherwise ->+            let texpr :: T.Expr ann+                texpr = T.fromExpr expr+            in if isIncompleteType texpr then+                 MacroTcError $ TcIncompleteTypeMacro name+               else+                 MacroTcTypeExpr $ TypecheckedMacroTypeExpr texpr quant+      (_, quant) ->+        (\vexpr -> MacroTcValueExpr $+          TypecheckedMacroValueExpr params vexpr quant) $+            V.fromExpr expr++    -- | An incomplete type at the top level of a type-like macro: 'void' or+    -- 'const'-wrapped 'void'. Pointer indirection makes the type complete, so+    -- 'void *' (and 'const void *') are not flagged.+    isIncompleteType :: T.Expr var -> Bool+    isIncompleteType = \case+        T.TypeLit TypeVoid -> True+        T.App T.Const e    -> isIncompleteType e+        _                  -> False
+ src/C/Expr/Typecheck/Expr.hs view
@@ -0,0 +1,2088 @@+{-# LANGUAGE BlockArguments #-}+{-# LANGUAGE CPP #-}+{-# LANGUAGE MagicHash #-}+{-# LANGUAGE ParallelListComp #-}++#if __GLASGOW_HASKELL__ >=908+{-# LANGUAGE TypeAbstractions #-}+#endif++-- | Type inference for simple function-like C macros.+module C.Expr.Typecheck.Expr+  (+    -- * Typechecking macros+    tcExpr+  , MacroTcError(..)+  , pprMacroTcError++    -- ** Macro type-system+  , Type(..), Kind(..)+  , TyCon(..), GenerativeTyCon(..), DataTyCon(..), ClassTyCon(..)+  , FamilyTyCon(..)+  , IntegralType(..)+  , Quant(..), QuantTyBody(..)+  , tyVarName, tyVarNames, mkQuantTyBody++    -- ** Macro typechecking errors+  , TcError(..), CtOrigin(..), MetaOrigin(..), CouldNotUnifyReason(..)+  , pprTcError, pprCtOrigin, pprMetaOrigin, pprCouldNotUnifyReason++    -- * Evaluating macros+  , naturalMaybe+  )+  where++import Control.Applicative qualified as Applicative+import Control.Monad+import Control.Monad.Except (ExceptT)+import Control.Monad.Except qualified as Except+import Control.Monad.ST (ST, runST)+import Control.Monad.State.Strict (State, StateT (..))+import Control.Monad.State.Strict qualified as State+import Control.Monad.Trans (lift)+import Control.Monad.Writer (WriterT)+import Control.Monad.Writer qualified as Writer+import Data.Bifunctor+import Data.Either (partitionEithers)+import Data.Fin qualified as Fin+import Data.Foldable qualified as Foldable+import Data.Functor ((<&>))+import Data.IntMap (IntMap)+import Data.IntMap.Strict qualified as IntMap+import Data.IntSet (IntSet)+import Data.IntSet qualified as IntSet+import Data.Kind qualified as Hs+import Data.List (intercalate)+import Data.List.NonEmpty qualified as NE+import Data.Map (Map)+import Data.Map.Strict qualified as Map+import Data.Maybe (fromMaybe, mapMaybe)+import Data.Monoid (Endo (..))+import Data.Nat (Nat (..))+import Data.Proxy+import Data.STRef (newSTRef, readSTRef)+import Data.Text (Text)+import Data.Text qualified as Text+import Data.Traversable (for)+import Data.Traversable.WithIndex (ifor)+import Data.Type.Equality (type (:~:) (..))+import Data.Type.Nat qualified as Nat+import Data.Typeable (Typeable, eqT)+import Data.Vec.Lazy (Vec (..))+import Data.Vec.Lazy qualified as Vec+import DeBruijn (Idx, idxToInt)+import Debug.Trace (traceM)+import Foreign.C.Types+import GHC.Exts (Int (I#), dataToTag#)+import GHC.Generics (Generic)+import GHC.Stack+import Numeric.Natural++import C.Expr.HostPlatform qualified as Runtime+import C.Type qualified as Runtime++import C.Expr.Syntax+import C.Expr.Typecheck.Type+import C.Expr.Util.Panic+import C.Expr.Util.TestEquality++import C.Operators qualified as Runtime++{-------------------------------------------------------------------------------+  Free type variables and substitution+-------------------------------------------------------------------------------}++data FVs where+  FVs+    :: { boundTvs       :: IntSet+       , seenTvs        :: IntSet+       , seenTvsRevList :: [ TyVar ]+       }+    -> FVs++insertFV :: TyVar -> FVs -> FVs+insertFV tv fvs@( FVs { boundTvs = bound, seenTvs = seen, seenTvsRevList = revTvs } )+  | u `IntSet.member` bound || u `IntSet.member` seen+  = fvs+  | otherwise+  = fvs+      { seenTvs        = IntSet.insert u seen+      , seenTvsRevList = tv : revTvs+      }+  where+    u = uniqueInt $ tyVarUnique tv++getFVs :: IntSet -> State FVs () -> FVs+getFVs bound = ( `State.execState` ( FVs bound IntSet.empty [] ) )++noBoundVars :: IntSet+noBoundVars = IntSet.empty++freeTyVarsOfType :: Type ki -> State FVs ()+freeTyVarsOfType = \case+  TyVarTy tv -> State.modify' $ insertFV tv+  FunTy args res -> goFunTy args res+  TyConAppTy _tc tys -> freeTyVarsOfTypes tys+  NomEqPred a b -> freeTyVarsOfTypes ( a ::: b ::: VNil )++  where+    goFunTy :: NE.NonEmpty ( Type Ty ) -> Type Ty -> State FVs ()+    goFunTy (argTy NE.:| mbArgTys) resTy = do+      freeTyVarsOfType argTy+      case NE.nonEmpty mbArgTys of+        Nothing     -> freeTyVarsOfType        resTy+        Just argTys -> goFunTy          argTys resTy++freeTyVarsOfTypes :: Traversable t => t ( Type ki ) -> State FVs ()+freeTyVarsOfTypes = Foldable.traverse_ freeTyVarsOfType+{-# INLINEABLE freeTyVarsOfType #-}++newtype Subst tv = Subst ( IntMap ( tv, Type Ty ) )+instance Functor Subst where+  fmap f ( Subst s ) = Subst $ fmap ( first f ) s++-- | Combine two substitutions, applying the first substitution over+-- the range of the second:+--+-- @applySubst s1 ( applySubst s2 ty ) == applySubst ( s1 <> s2 ) ty@+instance Show tv => Semigroup ( Subst tv ) where+  sub1@( Subst s1 ) <> ( Subst s2 ) =+    Subst $ IntMap.unionWithKey ( substClashErr "Semigroup Subst" ) s1+              ( IntMap.map ( \ ( nm, ty ) -> ( nm, applySubst sub1 ty ) ) s2 )+instance Show tv => Monoid ( Subst tv ) where+  mempty = Subst IntMap.empty+instance Show tv => Show ( Subst tv ) where+  show ( Subst s ) = "{ " ++ intercalate ", " ( map f $ IntMap.elems s ) ++ " }"+    where+      f ( tv, ty ) = show tv ++ " |-> " ++ show ty++isEmptySubst :: Subst tv -> Bool+isEmptySubst ( Subst s ) = IntMap.null s++domain :: Subst tv -> IntSet+domain ( Subst s ) = IntMap.keysSet s++addOneToSubst :: HasCallStack => TyVar -> Type Ty -> Subst TyVar -> Subst TyVar+addOneToSubst tv ty s = mkSubst [ ( tv, ty ) ] <> s++mkSubst :: HasCallStack => [ ( TyVar, Type Ty ) ] -> Subst TyVar+mkSubst = Subst+        . IntMap.fromListWithKey ( substClashErr "mkSubst" )+        . map ( \ ( tv, ty ) -> ( uniqueInt ( tyVarUnique tv ), ( tv, ty ) ) )++substClashErr :: ( Show a, HasCallStack ) => String -> Int -> a -> a -> a+substClashErr str i ty1 ty2 =+  panicPure $+    unlines+      [ str ++ ": incoherent substitution"+      , "TyVar with unique " ++ show ( Unique i ) ++ " mapped to two different types"+      , "ty1: " ++ show ty1+      , "ty2: " ++ show ty2+      ]++lookupSubst :: TyVar -> Subst tv -> Maybe ( Type Ty )+lookupSubst tv ( Subst s ) =+  fmap snd $ IntMap.lookup ( uniqueInt $ tyVarUnique tv ) s++applySubst :: forall ki tv. Subst tv -> Type ki -> Type ki+applySubst subst = goTy+  where+    goTy :: forall ki'. Type ki' -> Type ki'+    goTy = \case+      ty@( TyVarTy tv ) ->+        case lookupSubst tv subst of+          Nothing  -> ty+          Just ty' -> ty'+      FunTy args res ->+        FunTy ( fmap goTy args ) ( goTy res )+      TyConAppTy tc tys ->+        TyConAppTy tc $ fmap goTy tys+      NomEqPred a b ->+        NomEqPred ( goTy a ) ( goTy b )++-- | Are all the types in the range of the substitution atomic?+--+-- See 'isAtomicType'.+isAtomicSubst :: Subst tv -> Bool+isAtomicSubst ( Subst s ) = all ( isAtomicType . snd ) s++-- | Is this type atomic, i.e. does it have a counterpart in source Haskell?+--+-- The only reason a type would not be atomic is that in the macro typechecker+-- language, @IntLike@ and @FloatLike@ essentially behave like data families,+-- whereas in Haskell one instead has separate datatypes such as @data Int = ...@,+-- @data Word = ...@.+-- This means there is no Haskell equivalent of the type @IntLike alpha@ for+-- an unfilled metavariable @alpha@; it really corresponds to a family of types.+--+-- One might wonder why the macro type system departs from Haskell in this way;+-- the foundational reason is that it allows one to easily write families of+-- typeclass instances which cover all int-like types (see 'classInstancesWithDefaults').+isAtomicType :: Type ki -> Bool+isAtomicType = \case+  Data IntLikeTyCon args+    -- A well-kinded argument must be of one of the following two forms:+    --+    --   1. TyVarTy {}.+    --      This means we have a type like 'IntLike a' for a type variable a,+    --      precisely what we want to rule out as there is no Haskell counterpart+    --      for such a type.+    --   2. TyConApp (PrimIntInfoTyCon inty) VNil+    --      This means we have a concrete integral type in hand, which is fine.+    | TyVarTy {} ::: VNil <- args+    -> False+    | otherwise+    -> True+  Data FloatLikeTyCon args+    -- Similar comment as for the IntLikeTyCon case above.+    | TyVarTy {} ::: VNil <- args+    -> False+    | otherwise+    -> True+  TyConAppTy _tc args ->+    all isAtomicType args+  FunTy args res ->+    all isAtomicType args && isAtomicType res+  TyVarTy {} ->+    True+  NomEqPred a b+    -> isAtomicType a && isAtomicType b++{-------------------------------------------------------------------------------+  Constraints & errors+-------------------------------------------------------------------------------}++data Fun ctx =+    FunLocal ( Idx ctx )+  | FunVar   Identifier (Maybe QuantTy)+  | forall arity. FunVaFun ( VaFun arity )++funName :: Fun ctx -> FunName+funName = \case+    FunLocal i -> Text.pack ( "local_param_" ++ show i )+    FunVar n _ann -> getIdentifier n+    FunVaFun mf -> Text.pack ( show mf )++typFunName :: TyQual n -> FunName+typFunName = \case+    Pointer -> "pointer (*)"+    Const   -> "const qualifier (const)"++data TcError+  = UnificationError !UnificationError+  | UnboundVariable  !Identifier+  | TaggedNameWithArguments Identifier+  deriving stock Show++data UnificationError+  = forall k. Typeable k => CouldNotUnify !CouldNotUnifyReason !CtOrigin !( Type k ) !( Type k )+deriving stock instance Show UnificationError++pprTcError :: TcError -> Text+pprTcError = \case+  UnificationError err ->+    pprUnificationError err+  UnboundVariable ( Identifier nm ) ->+    "Unbound variable: '" <> nm <> "'"+  TaggedNameWithArguments name ->+    "Tagged name with arguments: " <> getIdentifier name++pprUnificationError :: UnificationError -> Text+pprUnificationError = \case+  CouldNotUnify rea orig ty1 ty2 ->+    Text.unlines+      [ "Could not unify:"+      , "  - " <> Text.pack ( show ty1 )+      , "  - " <> Text.pack ( show ty2 )+      , "because " <> pprCouldNotUnifyReason rea <> "."+      , pprCtOrigin orig ]++data CouldNotUnifyReason+  -- | Trying to unify incompatible types.+  = IncompatibleTypes+  -- | Trying to unify two TyConApps of different lengths.+  | TyConAppUnequalLength+  -- | Trying to unify two TyConApps with different head TyCons.+  | TyConAppDifferentTyCon+  -- | Trying to unify a type variable with a type mentiong this type variable.+  | OccursCheck !TyVar+  -- | Trying to unify a skolem variable with another type.+  | RigidSkolem !SkolemTyVar+  deriving stock ( Generic, Show )++pprCouldNotUnifyReason :: CouldNotUnifyReason -> Text+pprCouldNotUnifyReason = \case+  IncompatibleTypes ->+    "the types are incompatible"+  TyConAppUnequalLength ->+    "the type constructors are applied to different numbers of arguments"+  TyConAppDifferentTyCon ->+    "the type constructors are different"+  OccursCheck tv ->+    "of an occurs-check in the variable '" <> tyVarName tv <> "'"+  RigidSkolem sk ->+    "'" <> skolemTyVarName sk <> "' is a rigid skolem variable"++{-------------------------------------------------------------------------------+  Typechecking macros: typechecker environment+-------------------------------------------------------------------------------}++data TcEnv s =+  TcEnv+    { tcGblEnv :: !( TcGblEnv s )+    , tcLclEnv :: !TcLclEnv+    }++data TcGblEnv s+  = TcGblEnv+      { tcTypeEnv  :: !TypeEnv+      , tcPlatform :: !Runtime.Platform+      }++-- TODO <https://github.com/well-typed/c-expr/issues/23>+--+-- Implement source span to improve error reporting of macro typechecker errors.+data SrcSpan = SrcSpan+  deriving stock ( Eq, Ord, Generic )+instance Show SrcSpan where+  show _ = "<<noSrcSpan>>"++data TcLclEnv+  = TcLclEnv+      { tcSrcSpan   :: !SrcSpan+      , tcLclParams :: !ParamEnv+      }++newtype TcPureM a = TcPureM ( forall s. TcEnv s -> ST s a )+instance Functor TcPureM where+  fmap f ( TcPureM g ) = TcPureM ( fmap f . g )+instance Applicative TcPureM where+  pure f = TcPureM \ _ -> pure f+  (<*>) = ap+instance Monad TcPureM where+  TcPureM ma >>= f = TcPureM \ env -> do+    !a <- ma env+    case f a of+      TcPureM g -> g env++runTcM :: Runtime.Platform -> TypeEnv -> TcPureM a -> ( a, [ ( TcError, SrcSpan ) ] )+runTcM plat initTyEnv ( TcPureM f ) = runST do+  tcErrs    <- newSTRef []+  let+    tcGblEnv = TcGblEnv { tcTypeEnv = initTyEnv, tcPlatform = plat }+    tcLclEnv = TcLclEnv { tcSrcSpan = SrcSpan, tcLclParams = IntMap.empty }+  res <- f ( TcEnv { tcGblEnv, tcLclEnv } )+  errs <- readSTRef tcErrs+  return ( res, errs )++getSrcSpan :: TcPureM SrcSpan+getSrcSpan =+  TcPureM \ ( TcEnv _gbl ( TcLclEnv { tcSrcSpan } ) ) ->+    return tcSrcSpan++getPlatform :: TcPureM Runtime.Platform+getPlatform =+  TcPureM \ ( TcEnv ( TcGblEnv { tcPlatform = plat } ) _ ) ->+    pure plat++lookupTyEnv :: Identifier -> TcPureM (Maybe QuantTy)+lookupTyEnv varNm = TcPureM \ ( TcEnv ( TcGblEnv { tcTypeEnv } ) _ ) ->+  return $ Map.lookup varNm tcTypeEnv++declareLocalParams :: Vec ctx (Type Ty ) -> TcPureM a -> TcPureM a+declareLocalParams tys ( TcPureM f ) = TcPureM \ ( TcEnv gbl lcl ) ->+    f $+      TcEnv+        gbl+        lcl { tcLclParams = IntMap.fromList $ zip [0..] $ reverse (Vec.toList tys) }++lookupLocalParam :: forall ctx. Idx ctx -> TcPureM ( Type Ty )+lookupLocalParam i = TcPureM \ ( TcEnv _ lcl ) ->+    case IntMap.lookup (idxToInt i) ( tcLclParams lcl ) of+      Nothing -> panicPure "impossible: lookupLocalParam: index out of bounds"+      Just ty -> pure ty++{-------------------------------------------------------------------------------+  Typechecking macros: constraint generation monad+-------------------------------------------------------------------------------}++-- | Monad for unique generation.+type TcUniqueM = StateT Unique TcPureM++-- | Monad for unification.+type TcUnifyM = WriterT UnifyResult ( StateT ( Subst TyVar ) TcPureM )++-- | A collection of constraints (with their origin).+type Cts = [ ( Type Ct, CtOrigin ) ]++-- | Monad for generating constraints.+type TcGenM = WriterT ( Cts, [ ( TcError, SrcSpan ) ] ) ( StateT ( Subst TyVar ) TcUniqueM )++liftTcPureM :: TcPureM a -> TcGenM a+liftTcPureM = lift . lift . lift++newUnique :: Monoid w => WriterT w ( StateT s TcUniqueM ) Unique+newUnique = lift $ do+  u <- lift State.get+  let !u' = succ u+  lift $ State.put u'+  return u'+{-# INLINEABLE newUnique #-}++newMetaTyVarTy :: MetaOrigin -> VarName -> TcGenM ( Type Ty )+newMetaTyVarTy metaOrigin metaTyVarName = do+  metaTyVarUnique <- newUnique+  return $+    TyVarTy $+      MetaTv $+        MetaTyVar+          { metaTyVarUnique+          , metaTyVarName+          , metaOrigin+          }++-- | 'Control.Monad.Trans.Control.liftBaseWith' for t'TcPureM' and 'TcGenM'.+liftBaseTcM :: ( forall x. TcPureM x -> TcPureM x ) -> TcGenM a -> TcGenM a+liftBaseTcM morph g = do+  s0 <- lift State.get+  u  <- lift $ lift $ State.get+  ( ( ( a, ctsErrs ), subst ), u' ) <-+    liftTcPureM+      $ morph+      $ ( `State.runStateT` u )+      $ ( `State.runStateT` s0 )+      $ Writer.runWriterT g+  lift $ State.put subst+  lift $ lift $ State.put u'+  Writer.tell ctsErrs+  return a++liftUnifyM :: TcUnifyM a -> TcGenM a+liftUnifyM = Writer.mapWriterT ( fmap ( second deferredEqs ) . State.mapStateT lift )+  where+    deferredEqs :: UnifyResult -> ( Cts, [ ( TcError, SrcSpan ) ] )+    deferredEqs ( UnifyResult { deferredEqualities = eqs, unifyErrors = errs } ) =+      ( eqs, map ( first UnificationError ) errs )++addErrTcGenM :: TcError -> TcGenM ()+addErrTcGenM err = do+  srcSpan <- liftTcPureM getSrcSpan+  Writer.tell ( [], [ ( err, srcSpan ) ] )++runTcGenMTcM :: TcGenM a -> TcUniqueM ( ( a, ( Cts, [ ( TcError, SrcSpan ) ] ) ), Subst TyVar )+runTcGenMTcM = aux . Writer.runWriterT+  where+    aux :: StateT ( Subst TyVar ) TcUniqueM x -> TcUniqueM ( x, Subst TyVar )+    aux ( State.StateT f ) =+      State.StateT \ u ->+        ( `State.runStateT` u ) $ f mempty++-- | Run a 'TcUnifyM' action and retrieve the underlying t'Subst'+-- when unification succeeded without deferring any equalities.+runTcUnifyMSubst :: forall a. Subst TyVar -> TcUnifyM a -> TcPureM ( Maybe ( a, Subst TyVar ) )+runTcUnifyMSubst subst0 =+  fmap unifySuccess . ( `State.runStateT` subst0 ) . Writer.runWriterT+    where+      unifySuccess ( ( a, UnifyResult { deferredEqualities = eqs, unifyErrors = errs } ), subst )+        | null eqs && null errs+        = Just ( a, subst )+        | otherwise+        = Nothing++-- | Run a 'TcGenM' action and retrieve the underlying t'Subst'+-- when there were no errors.+runTcGenMSubst :: TcGenM a -> TcUniqueM ( Maybe ( ( Cts, Subst TyVar ), a ) )+runTcGenMSubst = fmap noErrs . runTcGenMTcM+  where+    noErrs ( ( a, ( cts, mbErrs ) ), subst ) =+      if null mbErrs+      then Just ( ( cts, subst ), a )+      else Nothing++{-------------------------------------------------------------------------------+  Typechecking macros: unification+-------------------------------------------------------------------------------}++data UnifyResult =+  UnifyResult+    { deferredEqualities :: [ ( Type Ct, CtOrigin ) ]+    , unifyErrors        :: [ ( UnificationError, SrcSpan ) ] }+  deriving stock Show+instance Semigroup UnifyResult where+  UnifyResult d1 e1 <> UnifyResult d2 e2 =+    UnifyResult ( d1 ++ d2 ) ( e1 ++ e2 )+instance Monoid UnifyResult where+  mempty = UnifyResult [] []++data SwapFlag = NotSwapped | Swapped+  deriving stock ( Eq, Ord, Show )++swap :: SwapFlag -> SwapFlag+swap = \case+  NotSwapped -> Swapped+  Swapped -> NotSwapped++unifyType :: CtOrigin -> SwapFlag -> Type Ty -> Type Ty -> TcUnifyM ()+unifyType orig swapped ty1 ty2+  | TyVarTy tv1 <- ty1+  = unifyTyVar orig swapped tv1 ty2+  | TyVarTy tv2 <- ty2+  = unifyTyVar orig ( swap swapped ) tv2 ty1+  | FunTy args1 res1 <- ty1+  , FunTy args2 res2 <- ty2+  = unifyFunTys orig swapped args1 res1 args2 res2+  | FamApp {} <- ty1+  = defer+  | FamApp {} <- ty2+  = defer+  | TyConAppTy ( GenerativeTyCon tc1 ) as1 <- ty1+  , TyConAppTy ( GenerativeTyCon tc2 ) as2 <- ty2+  = unifyTyConApp orig swapped ( tc1, as1 ) ( tc2, as2 )+  | otherwise+  = couldNotUnify IncompatibleTypes orig swapped ty1 ty2+  where+    eq :: Type Ct+    eq = case swapped of+      NotSwapped -> NomEqPred ty1 ty2+      Swapped    -> NomEqPred ty2 ty1+    defer :: TcUnifyM ()+    defer =+      Writer.tell $+        UnifyResult+          { deferredEqualities = [ ( eq, orig ) ]+          , unifyErrors = []+          }++unifyTyConApp+  :: forall nbArgs1 nbArgs2 resKi+  .  Typeable resKi+  => CtOrigin+  -> SwapFlag+  -> ( GenerativeTyCon nbArgs1 resKi, Vec nbArgs1 ( Type Ty ) )+  -> ( GenerativeTyCon nbArgs2 resKi, Vec nbArgs2 ( Type Ty ) )+  -> TcUnifyM ()+unifyTyConApp orig swapped ( tc1, args1 ) ( tc2, args2 )+  | Just Refl <- tcOK+  = unifyTypes orig swapped args1 args2+  | otherwise+  = couldNotUnify TyConAppDifferentTyCon orig swapped+      ( TyConAppTy ( GenerativeTyCon tc1 ) args1 )+      ( TyConAppTy ( GenerativeTyCon tc2 ) args2 )+  where+    tcOK :: Maybe ( nbArgs1 :~: nbArgs2 )+    tcOK = fmap ( \ Refl -> Refl ) $ tc1 `equals2` tc2++unifyTypes :: CtOrigin -> SwapFlag -> Vec n ( Type Ty ) -> Vec n ( Type Ty ) -> TcUnifyM ()+unifyTypes orig swapped as bs = sequence_ $ Vec.zipWith ( unifyType orig swapped ) as bs+{-# INLINEABLE unifyTypes #-}++unifyTyVar :: CtOrigin -> SwapFlag -> TyVar -> Type Ty -> TcUnifyM ()+unifyTyVar _ _ tv1 ( TyVarTy tv2 )+  | tyVarUnique tv1 == tyVarUnique tv2+  = return ()+unifyTyVar orig swapped tv1 ty2' = do+  plat <- lift $ lift $ getPlatform+  subst <- State.get+  let ty2 = normaliseType plat $ applySubst subst ty2'+  case lookupSubst tv1 subst of+    Just ty1 ->+      unifyType orig swapped ty1 ty2+    Nothing+      | TyVarTy tv2 <- ty2+      , tyVarUnique tv1 == tyVarUnique tv2+      -> return ()+      | SkolemTv {} <- tv1+      , TyVarTy ( tv2@( MetaTv {} ) ) <- ty2+      -> unifyTyVar orig ( swap swapped ) tv2 ( TyVarTy tv1 )+      | IntSet.member ( uniqueInt $ tyVarUnique tv1 ) $ seenTvs $ getFVs noBoundVars $ freeTyVarsOfType ty2+      -> couldNotUnify ( OccursCheck tv1 ) orig swapped ( TyVarTy tv1 ) ty2+      | otherwise+      -> case tv1 of+          MetaTv tau1 ->+            State.put $ addOneToSubst ( MetaTv tau1 ) ty2 subst+          SkolemTv sk1 ->+            couldNotUnify ( RigidSkolem sk1 ) orig swapped ( TyVarTy tv1 ) ty2++unifyFunTys :: CtOrigin -> SwapFlag -> NE.NonEmpty ( Type Ty ) -> Type Ty -> NE.NonEmpty ( Type Ty )  -> Type Ty -> TcUnifyM ()+unifyFunTys orig swapped ( arg1 NE.:| args1 ) res1 ( arg2 NE.:| args2 ) res2 = do+  unifyType orig swapped arg1 arg2+  if | argTy1 : rest1 <- args1+     , argTy2 : rest2 <- args2+     -> unifyFunTys orig swapped ( argTy1 NE.:| rest1 ) res1 ( argTy2 NE.:| rest2 ) res2+     | argTy1 : rest1 <- args1+     -> unifyType orig swapped ( FunTy ( argTy1 NE.:| rest1 ) res1 ) res2+     | argTy2 : rest2 <- args2+     -> unifyType orig swapped res1 ( FunTy ( argTy2 NE.:| rest2 ) res2 )+     | otherwise+     -> unifyType orig swapped res1 res2++couldNotUnify :: Typeable ki => CouldNotUnifyReason -> CtOrigin -> SwapFlag -> Type ki -> Type ki -> TcUnifyM ()+couldNotUnify rea orig swapped ty1 ty2 = do+  srcSpan <- lift $ lift getSrcSpan+  let+    oneErrorHere :: UnificationError -> UnifyResult+    oneErrorHere err = UnifyResult [] [ ( err, srcSpan ) ]+  Writer.tell $ oneErrorHere $+    case swapped of+      NotSwapped -> CouldNotUnify rea orig ty1 ty2+      Swapped    -> CouldNotUnify rea orig ty2 ty1++{-------------------------------------------------------------------------------+  Typechecking macros: normalisation+-------------------------------------------------------------------------------}++-- | Normalise a type by reducing reducible type-family applications.+normaliseType :: Runtime.Platform -> Type ki -> Type ki+normaliseType plat ty =+  case ty of+    TyVarTy {} -> ty+    FunTy args res ->+      FunTy ( fmap ( normaliseType plat ) args ) ( normaliseType plat res )+    NomEqPred lhs rhs ->+      NomEqPred ( normaliseType plat lhs ) ( normaliseType plat rhs )+    TyConAppTy tc args ->+      let+        args'  = fmap ( normaliseType plat ) args+        tcApp' = TyConAppTy tc args'+      in+        case tc of+          FamilyTyCon fam ->+            fromMaybe tcApp' $ reduceTyFamApp plat fam args'+          GenerativeTyCon {} ->+            tcApp'++reduceTyFamApp :: Runtime.Platform -> FamilyTyCon n -> Vec n ( Type Ty ) -> Maybe ( Type Ty )+reduceTyFamApp platform = \case+  PlusResTyCon       -> adapt $ Runtime.opResType platform $ Runtime.UnaryOp  Runtime.UnaryPlus+  MinusResTyCon      -> adapt $ Runtime.opResType platform $ Runtime.UnaryOp  Runtime.UnaryMinus+  AddResTyCon        -> adapt $ Runtime.opResType platform $ Runtime.BinaryOp Runtime.Add+  SubResTyCon        -> adapt $ Runtime.opResType platform $ Runtime.BinaryOp Runtime.Sub+  MultResTyCon       -> adapt $ Runtime.opResType platform $ Runtime.BinaryOp Runtime.Mult+  DivResTyCon        -> adapt $ Runtime.opResType platform $ Runtime.BinaryOp Runtime.Div+  RemResTyCon        -> adapt $ Runtime.opResType platform $ Runtime.BinaryOp Runtime.Rem+  ComplementResTyCon -> adapt $ Runtime.opResType platform $ Runtime.UnaryOp  Runtime.BitwiseNot+  BitsResTyCon       -> adapt $ Runtime.opResType platform $ Runtime.BinaryOp Runtime.BitwiseAnd+  ShiftResTyCon      -> adapt $ \ ( ty ::: VNil ) ->+                          -- NB: need to adapt to the fact that bit shift operators+                          -- are binary, but the result type family only cases on+                          -- the first argument (the shiftee) and not the+                          -- second argument (the shift amount).+                                Runtime.opResType platform ( Runtime.BinaryOp Runtime.ShiftLeft )+                                  ( ty ::: cIntTy ::: VNil )++  where+    cIntTy :: Runtime.Type CType+    cIntTy = Runtime.Arithmetic ( Runtime.Integral $ Runtime.IntLike $ Runtime.Int Runtime.Signed )+    adapt :: ( Vec n ( Runtime.Type CType ) -> Maybe ( Runtime.Type CType ) )+          -> Vec n ( Type Ty ) -> Maybe ( Type Ty )+    adapt f args = do+      args' <- traverse fromMacroType args+      res   <- f args'+      toMacroType res++-- | A recursive newtype, which instantiates the v'Runtime.Ptr' constructor of+-- t'Runtime.Type' to t'Runtime.Type' itself.+newtype CType = CType ( Runtime.Type CType )+  deriving stock Eq++toMacroType :: Runtime.Type CType -> Maybe ( Type Ty )+toMacroType = \case+  -- See https://github.com/well-typed/hs-bindgen/issues/441. Explicit casts+  -- would be one way to introduce `void`, but they don't work (yet).+  Runtime.Void          -> panicPure "C macro typechecker does not support 'void' (yet)"+  Runtime.Arithmetic a  ->+    case a of+      Runtime.Integral  i -> Just $ IntLike   $ PrimIntInfoTy   $ CIntegralType i+      Runtime.FloatLike f -> Just $ FloatLike $ PrimFloatInfoTy f+  Runtime.Ptr ( CType a ) -> Ptr <$> toMacroType a++fromMacroType :: Type Ty -> Maybe ( Runtime.Type CType )+fromMacroType = \case+  TyVarTy {} -> Nothing+  FunTy {} -> Nothing+  TyConAppTy tc args ->+    case tc of+      FamilyTyCon {} -> Nothing+      GenerativeTyCon ( DataTyCon dat ) ->+        case dat of+          TupleTyCon {} -> Nothing+          VoidTyCon -> Just $ Runtime.Void+          MacroTypeTyCon -> Nothing+          CharLitTyCon -> Nothing+          IntLikeTyCon ->+            case args of+              ( a ::: VNil ) ->+                case a of+                  PrimIntInfoTy (CIntegralType inty) ->+                    Just $ Runtime.Arithmetic $ Runtime.Integral inty+                  _ -> Nothing+          FloatLikeTyCon ->+            case args of+              ( a ::: VNil ) ->+                case a of+                  PrimFloatInfoTy floaty ->+                    Just $ Runtime.Arithmetic $ Runtime.FloatLike floaty+                  _ -> Nothing+          PtrTyCon       ->+            case args of+              ( a ::: VNil ) ->+                Runtime.Ptr . CType <$> fromMacroType a++          PrimIntInfoTyCon {} -> panicPure "fromMacroType: 'PrimIntInfoTyCon'"+          PrimFloatInfoTyCon {} -> panicPure "fromMacroType: 'PrimFloatInfoTyCon'"++applySubstNormalise :: Runtime.Platform -> Subst tv -> Type ki -> Type ki+applySubstNormalise plat subst = normaliseType plat . applySubst subst++{-------------------------------------------------------------------------------+  Typechecking macros: instantiation+-------------------------------------------------------------------------------}++instantiate+  :: forall nbBinders body+  .  Nat.SNatI nbBinders+  => CtOrigin -> InstOrigin+  -> ( Vec nbBinders ( Type Ty ) -> QuantTyBody body )+  -> TcGenM ( Vec nbBinders ( Type Ty ), body )+instantiate ctOrig instOrig body = do+  tvs <-+    for ( tyVarNames @nbBinders ) \ ( i, tvName ) ->+      newMetaTyVarTy ( Inst { instOrigin = instOrig, instPos = i } ) tvName+  let QuantTyBody cts bodyTy = body tvs+  Writer.tell $ ( map (, ctOrig ) cts, mempty )+  return ( tvs, bodyTy )++{-------------------------------------------------------------------------------+  Typechecking macros: type inference+-------------------------------------------------------------------------------}++-- | Infer the type of a macro declaration (before constraint solving and generalisation).+inferTop :: Identifier -> Vec ctx Identifier -> Expr ctx (Ps (Maybe QuantTy))+         -> TcUniqueM ( ( ( Expr ctx Tc, ( Vec ctx ( Type Ty ), Type Ty ) ), Cts )+                      , [ ( TcError, SrcSpan ) ] )+inferTop funNm params body = do+  plat <- lift getPlatform+  ( ( ( tcBody, ( paramTys, bodyTy ) ), ( cts, mbErrs ) ), subst ) <- runTcGenMTcM ( inferLam funNm params body )+  let paramTys' = fmap ( applySubstNormalise plat subst ) paramTys+      bodyTy' = applySubstNormalise plat subst bodyTy+      cts' = map ( first ( applySubstNormalise plat subst ) ) cts+  debugTraceM $ unlines+    [ "inferTop " ++ show funNm+    , "paramTys: " ++ show paramTys'+    , "bodyTy: " ++ show bodyTy'+    , "cts: " ++ show cts'+    , "final subst: " ++ show subst+    ]+  return ( ( ( tcBody, ( paramTys', bodyTy' ) ), cts' ), mbErrs )++inferExpr :: Expr ctx (Ps (Maybe QuantTy)) -> TcGenM ( Type Ty, Expr ctx Tc )+inferExpr = \case+  Term tm -> second Term <$> inferTerm tm+  TyApp fun args -> do+    ( args', resTy ) <- inferTyApp fun args+    pure ( resTy, TyApp fun args' )+  VaApp NoXApp fun args -> do+    ( funVal, ( args', resTy ) ) <- inferVaApp ( FunVaFun fun ) args+    return ( resTy, VaApp ( XAppTc funVal ) fun args' )++inferTerm :: Term ctx (Ps (Maybe QuantTy)) -> TcGenM ( Type Ty, Term ctx Tc )+inferTerm = \case+  Literal x ->+    pure (inferLit x, Literal x)+  LocalParam i ->+    do resTy <- liftTcPureM $ lookupLocalParam i+       return ( resTy, LocalParam i )+  Var (XVarPs ann) (NameOrdinary fun) argsList -> Vec.reifyList argsList $ \ args ->+    do ( funVal, ( args', resTy ) ) <- inferVaApp ( FunVar fun ann ) args+       return ( resTy, Var ( XVarTc funVal ann ) (NameOrdinary fun) ( Vec.toList args' ) )+  Var (XVarPs ann) (NameTagged name tag) argsList -> do+    case argsList of+      [] -> pure ()+      _  -> addErrTcGenM $ TaggedNameWithArguments name+    pure (MacroTypeTy, Var (XVarTc NoFunValue ann) (NameTagged name tag) [])++inferLit :: Literal -> Type Ty+inferLit = \case+  TypeLit{}        -> MacroTypeTy+  ValueLit vaLit -> case vaLit of+    ValueInt ( IntegerLiteral { integerLiteralType = intyTy } ) ->+      IntLike $ PrimIntInfoTy $ CIntegralType $ Runtime.IntLike intyTy+    ValueFloat ( FloatingLiteral { floatingLiteralType = floatyTy }) ->+      FloatLike $ PrimFloatInfoTy floatyTy+    ValueChar{} ->+      CharLitTy+    ValueString{} ->+      String++inferTyApp ::+     TyQual n+  -> Vec nbArgs ( Expr ctx (Ps (Maybe QuantTy)) )+  -> TcGenM ( Vec nbArgs ( Expr ctx Tc ), Type Ty )+inferTyApp fun args = do+  let funTy = inferTyFun fun+  -- The handling of arguments is duplicated in 'inferVaApp'.+  case args of+    VNil ->+      pure (VNil, funTy)+    _ ::: _ -> do+      args' <- traverse inferExpr args+      let ( argTys', argExprs ) = ( Vec.toNonEmpty $ fmap fst args', fmap snd args' )+      resTy <- newMetaTyVarTy ( ExpectedFunTyResTy $ funNm ) "r"+      let actualTy = FunTy argTys' resTy+      liftUnifyM $ unifyType ( AppOrigin $ funNm ) NotSwapped actualTy funTy+      pure ( argExprs, resTy )+  where+    funNm = typFunName fun++-- | Infer the type of an application of a function to arguments.+--+-- Also returns a 'FunValue', which allows evaluating the instantiated function.+inferVaApp ::+     Fun ctx+  -> Vec nbArgs ( Expr ctx (Ps (Maybe QuantTy)) )+  -> TcGenM ( FunValue, ( Vec nbArgs ( Expr ctx Tc ), Type Ty ) )+inferVaApp fun args = do+  ( funVal, funTy ) <- inferFun fun+  -- The handling of arguments is duplicated in 'inferTyApp'.+  ( funVal , ) <$> case args of+    VNil ->+      return ( VNil, funTy )+    _ ::: _ -> do+      args' <- traverse inferExpr args+      let ( argTys', argExprs ) = ( Vec.toNonEmpty $ fmap fst args', fmap snd args' )+      resTy <- newMetaTyVarTy ( ExpectedFunTyResTy $ funName fun ) "r"+      let actualTy = FunTy argTys' resTy+      liftUnifyM $ unifyType ( AppOrigin $ funName fun ) NotSwapped actualTy funTy+      return ( argExprs, resTy )++-- | Infer the type of an occurrence of a variable or function,+-- instantiating if necessary.+inferFun :: Fun ctx -> TcGenM ( FunValue, Type Ty )+inferFun f = case f of+    FunLocal idx -> do+      paramTy <- liftTcPureM $ lookupLocalParam idx+      pure+        -- The value is not consulted, see 'evaluateTerm'.+        ( FunValue @Z funNm $ const NoValue+        , paramTy )+    FunVar varNm ann -> do+      mbQTy <- case ann of+        Nothing -> liftTcPureM $ lookupTyEnv varNm+        Just x  -> pure $ Just x+      case mbQTy of+        Just ( Quant funQTy ) ->+          snd <$>+            instantiate ( FunInstOrigin funNm ) ( FunInstMetaOrigin funNm ) funQTy+        Nothing -> do+          addErrTcGenM $ UnboundVariable varNm+          alpha <- newMetaTyVarTy ( ExpectedVarTy varNm ) ( funNm <> "_ty" )+          return ( FunValue @Z funNm $ const NoValue, alpha )+    FunVaFun mFun  ->+      case inferVaFun mFun of+        Quant funQTy -> do+          snd <$>+            instantiate ( FunInstOrigin funNm ) ( FunInstMetaOrigin funNm ) funQTy+  where+    funNm :: FunName+    funNm = funName f++-- | Infer the type of a lambda expression.+inferLam :: forall ctx+         .  Identifier                    -- ^ name of the function (for error messages)+         -> Vec ctx Identifier            -- ^ local parameters+         -> Expr ctx (Ps (Maybe QuantTy)) -- ^ function body+         -> TcGenM ( Expr ctx Tc, ( Vec ctx ( Type Ty ), Type Ty ) )+inferLam _ VNil body = do+  ( bodyTy, body' ) <- inferExpr body+  return ( body', ( VNil, bodyTy) )+inferLam funNm params body = do+  paramTys <-+    ifor params \ i param  ->+      newMetaTyVarTy+        ( FunParam funNm ( param, Fin.toNatural i ) )+        ( "ty_" <> getIdentifier param )+  liftBaseTcM ( declareLocalParams paramTys ) $ do+    ( bodyTy, body' ) <- inferExpr body+    return ( body', ( paramTys, bodyTy ) )++-- Unlike value functions, functions on the type level are always monomorphic,+-- so we don't need a 'Quant'.+inferTyFun :: TyQual n -> Type Ty+inferTyFun fun = case fun of+    -- Pointer: MacroType -> MacroType+    Pointer -> mkFunTy [MacroTypeTy] MacroTypeTy+    -- Const qualifier: MacroType -> MacroType+    Const   -> mkFunTy [MacroTypeTy] MacroTypeTy++-- | Infer the type of a 'VaFun', together with a 'C.Expr.Typecheck.Type.FunValue'+-- used to evaluate this function.+inferVaFun :: VaFun arity -> Quant ( FunValue, Type Ty )+inferVaFun fun = case fun of++  -- Tuple+  MTuple @n -> Quant @( S ( S n ) ) \ as ->+    QuantTyBody []+      ( let arity :: Int+            arity = 2 + n+            tupNm = "Tuple" <> Text.pack ( show arity )+        in+          -- NB: we don't support evaluation of tuples currently, because:+          --+          --  1. C has no notion of tuples, and emulating tuples using structs+          --     passed by value brings in a lot of complexity (e.g. alignment+          --     considerations).+          --  2. We would need to add tuples to the value type system ('ValType').+          FunValue @( S ( S n ) ) tupNm $ const NoValue+      , mkFunTy as $ Tuple (Nat.snat @(S (S n))) as+      )+      where+        n :: Int+        n = Nat.reflectToNum @n Proxy+++  -- Logical operators+  MLogicalNot -> q1 \ a   -> QuantTyBody [Not  a]      ( unaryFun  $ \ ty      f -> f (Runtime.singNot ty)     , mkFunTy [a]   IntTy )+  MLogicalAnd -> q2 \ a b -> QuantTyBody [Logical a b] ( binaryFun $ \ ty1 ty2 f -> f (Runtime.singAnd ty1 ty2), mkFunTy [a,b] IntTy )+  MLogicalOr  -> q2 \ a b -> QuantTyBody [Logical a b] ( binaryFun $ \ ty1 ty2 f -> f (Runtime.singOr  ty1 ty2), mkFunTy [a,b] IntTy )++  -- Comparison operators+  MRelEQ      -> q2 \ a b -> QuantTyBody [RelEq a b]    ( binaryFun $ \ ty1 ty2 f -> f (Runtime.singEq  ty1 ty2), mkFunTy [a,b] IntTy )+  MRelNE      -> q2 \ a b -> QuantTyBody [RelEq a b]    ( binaryFun $ \ ty1 ty2 f -> f (Runtime.singNEq ty1 ty2), mkFunTy [a,b] IntTy )+  MRelLT      -> q2 \ a b -> QuantTyBody [RelOrd a b]   ( binaryFun $ \ ty1 ty2 f -> f (Runtime.singLT  ty1 ty2), mkFunTy [a,b] IntTy )+  MRelLE      -> q2 \ a b -> QuantTyBody [RelOrd a b]   ( binaryFun $ \ ty1 ty2 f -> f (Runtime.singLTE ty1 ty2), mkFunTy [a,b] IntTy )+  MRelGT      -> q2 \ a b -> QuantTyBody [RelOrd a b]   ( binaryFun $ \ ty1 ty2 f -> f (Runtime.singGT  ty1 ty2), mkFunTy [a,b] IntTy )+  MRelGE      -> q2 \ a b -> QuantTyBody [RelOrd a b]   ( binaryFun $ \ ty1 ty2 f -> f (Runtime.singGTE ty1 ty2), mkFunTy [a,b] IntTy )++  -- Arithmetic operators++    -- Unary+  MUnaryPlus  -> q1 \ a   -> QuantTyBody [Plus  a] ( unaryFun  $ \ ty      f -> f (Runtime.singPlus   ty), mkFunTy [a] ( PlusRes a ) )+  MUnaryMinus -> q1 \ a   -> QuantTyBody [Minus a] ( unaryFun  $ \ ty      f -> f (Runtime.singNegate ty), mkFunTy [a] ( MinusRes a ) )++    -- Additive+  MAdd        -> q2 \ a b -> QuantTyBody [Add a b] ( binaryFun $ \ ty1 ty2 f -> f (Runtime.singAdd ty1 ty2), mkFunTy [a,b] ( AddRes a b ) )+  MSub        -> q2 \ a b -> QuantTyBody [Sub a b] ( binaryFun $ \ ty1 ty2 f -> f (Runtime.singSub ty1 ty2), mkFunTy [a,b] ( SubRes a b ) )++    -- Multiplicative+  MMult       -> q2 \ a b -> QuantTyBody [Mult a b] ( binaryFun $ \ ty1 ty2 f -> f (Runtime.singMult ty1 ty2), mkFunTy [a,b] ( MultRes a b ) )+  MDiv        -> q2 \ a b -> QuantTyBody [Div  a b] ( binaryFun $ \ ty1 ty2 f -> f (Runtime.singDiv  ty1 ty2), mkFunTy [a,b] ( DivRes  a b ) )+  MRem        -> q2 \ a b -> QuantTyBody [Rem  a b] ( binaryFun $ \ ty1 ty2 f -> f (Runtime.singRem  ty1 ty2),  mkFunTy [a,b] ( RemRes  a b ) )++    -- Bitwise logical operators+  MBitwiseNot -> q1 \ a   -> QuantTyBody [Complement a] ( unaryFun  $ \ ty      f -> f (Runtime.singComplement ty) , mkFunTy [a]   ( ComplementRes a ) )+  MBitwiseAnd -> q2 \ a b -> QuantTyBody [Bitwise a b]  ( binaryFun $ \ ty1 ty2 f -> f (Runtime.singBitAnd ty1 ty2), mkFunTy [a,b] ( BitsRes a b ) )+  MBitwiseXor -> q2 \ a b -> QuantTyBody [Bitwise a b]  ( binaryFun $ \ ty1 ty2 f -> f (Runtime.singBitXor ty1 ty2), mkFunTy [a,b] ( BitsRes a b ) )+  MBitwiseOr  -> q2 \ a b -> QuantTyBody [Bitwise a b]  ( binaryFun $ \ ty1 ty2 f -> f (Runtime.singBitOr  ty1 ty2), mkFunTy [a,b] ( BitsRes a b ) )++    -- Bit shift+  MShiftLeft  -> q2 \ a i -> QuantTyBody [Shift a i] ( binaryFun $ \ ty1 ty2 f -> f (Runtime.singShiftL ty1 ty2), mkFunTy [a,i] ( ShiftRes a ) )+  MShiftRight -> q2 \ a i -> QuantTyBody [Shift a i] ( binaryFun $ \ ty1 ty2 f -> f (Runtime.singShiftR ty1 ty2), mkFunTy [a,i] ( ShiftRes a ) )+  where+    q1 body = Quant @( S Z )       \ (a ::: VNil) -> body a+    q2 body = Quant @( S ( S Z ) ) \ (a ::: i ::: VNil) -> body a i++    -- For explanation of this type signature see Note [Abstracting over instance lookup functions].+    unaryFun :: ( forall ty r. Runtime.SType ValSType ty+                  -> ( forall res. ( Runtime.SType ValSType res, ty -> res ) -> r ) -> r )+             -> FunValue+    unaryFun proveFn =+      FunValue @( S Z ) ( Text.pack ( show fun ) ) $ \ ( a ::: VNil ) ->+        if | Value ( ValSType ty ) x <- a+           -> proveFn ty $ \ ( resTy, fn ) ->+                Value ( ValSType resTy ) ( fn x )+           | otherwise+           -> NoValue++    -- For explanation of this type signature see Note [Abstracting over instance lookup functions].+    binaryFun :: ( forall ty1 ty2 r. Runtime.SType ValSType ty1 -> Runtime.SType ValSType ty2+                   -> ( forall res. ( Runtime.SType ValSType res, ty1 -> ty2 -> res ) -> r ) -> r )+               -> FunValue+    binaryFun proveFn =+      FunValue @( S ( S Z ) ) ( Text.pack ( show fun ) ) $ \ ( a ::: b ::: VNil ) ->+        if | Value ( ValSType ty1 ) x <- a+           , Value ( ValSType ty2 ) y <- b+           -> proveFn ty1 ty2 $ \ ( resTy, fn ) ->+                Value ( ValSType resTy ) ( fn x y )+           | otherwise+           -> NoValue++{- Note [Abstracting over instance lookup functions]+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~+We are trying to quantify over the different singleton types such as:++ singAdd   :: SType ty1 -> SType ty2 -> (SType ( AddRes ty1 ty2), ty1 -> ty2 ->  AddRes ty1 ty2)+ singMult  :: SType ty1 -> SType ty2 -> (SType (MultRes ty1 ty2), ty1 -> ty2 -> MultRes ty1 ty2)+ ...++We could try:++   binaryFun :: forall res. (forall ty1 ty2. SType ty1 -> SType ty2 -> (SType res, ty1 -> ty2 -> res)) -> FunValue++but this doesn't work because we would need to instantiate res to a type that+mentions the inner type variables ty1, ty2.++We also can't do:++ binaryFun :: (forall ty1 ty2 res. SType ty1 -> SType ty2 -> (SType res, ty1 -> ty2 -> res)) -> FunValue++because then the type of 'singAdd'/'singMult' would be insufficiently polymorphic.++Neither can we do:++ binaryFun :: (forall ty1 ty2 tf. SType ty1 -> SType ty2 -> (SType (tf ty1 ty2), ty1 -> ty2 -> tf ty1 ty2)) -> FunValue++because GHC interprets `tf` in such a position to be a matchable type constructor+(such as Maybe). We would not be able to instantiate it to e.g. 'AddRes', because+'AddRes' is not valid partially applied (we would need e.g. -XUnsaturatedTypeFamilies).++What we really want is an existential type:++ binaryFun :: (forall ty1 ty2. SType ty1 -> SType ty2 -> exists res. (SType res, ty1 -> ty2 -> res) -> FunValue++which we encode using continuation-passing style in 'unaryFun'/'binaryFun'.+-}++{-------------------------------------------------------------------------------+  Typechecking macros: classes+--------------------------------------------------------------------------------++The following pieces of information determine how class constraints are solved:++  1. The superclass implication structure, as specified by the function+     'classSuperclasses'.++  2. Class instances, as specified by the function+     'classInstancesWithDefaults'.+-}++-- | The type constructor tag of a 'C.Expr.Typecheck.Type.DataTyCon' or 'C.Expr.Typecheck.Type.ClassTyCon'.+type TyConTag :: Kind -> Hs.Type+newtype TyConTag ki = TyConTag Int+  deriving stock ( Eq, Ord, Show )++-- | The type constructor tag of a 'C.Expr.Typecheck.Type.DataTyCon'.+type DataTyConTag  = TyConTag Ty+-- | The type constructor tag of a 'C.Expr.Typecheck.Type.ClassTyCon'.+type ClassTyConTag = TyConTag Ct++-- | What heads this type?+--+-- Used for class instance matching.+data TypeHead+  -- | The type is headed by the function type constructor.+  = FunTyHead+  -- | The type is headed by the type constructor with the given 'DataTyConTag'.+  | TyConHead !DataTyConTag+  deriving stock ( Eq, Ord, Show )++-- | A defaulting proposal, returning a collection of additional equalities+-- between the input types.+type DefaultingProposal nbBinders =+  Vec nbBinders ( Type Ty ) -> NE.NonEmpty ( Type Ty, Type Ty )++-- | An instance for a class constraint, corresponding to the quantified+-- type at the head of the instance.+--+-- For example, the instance+--+-- @instance forall x y. ( x ~ y ) => Cls x y Int@+--+-- is represented by the quantified type+--+-- @forall x y. ( x ~ y ) => Cls x y Int@.+data Instance where+  Instance+    :: forall nbBinders nbArgs+    .  ( Nat.SNatI nbBinders, Nat.SNatI nbArgs )+    => { instanceQuantTy  :: !( Vec nbBinders ( Type Ty ) -> QuantTyBody ( Vec nbArgs ( Type Ty ) ) )+       , instanceDefaults :: !( [ DefaultingProposal nbBinders ] )+       }+    -> Instance++-- | A trie, used to look up class instances.+data TrieMap k a =+  Trie+    { value    :: [ a ]+    , children :: Map ( Maybe k ) ( TrieMap k a )+    }+  deriving stock ( Eq, Show, Functor, Foldable, Traversable )++instance Ord k => Semigroup ( TrieMap k a ) where+  Trie v1 c1 <> Trie v2 c2 = Trie ( v1 ++ v2 ) ( c1 <> c2 )+instance Ord k => Monoid ( TrieMap k a ) where+  mempty = Trie [] Map.empty++insertTrie :: Ord k => [ Maybe k ] -> a -> TrieMap k a -> TrieMap k a+insertTrie []         v ( Trie vs cs ) = Trie ( v : vs ) cs+insertTrie ( p : ps ) v ( Trie vs cs ) =+  Trie vs $+    let child = Map.findWithDefault mempty p cs+        newChild = insertTrie ps v child+     in Map.insert p newChild cs++lookupTrie :: Ord k => [ Maybe k ] -> TrieMap k a -> [ a ]+lookupTrie []         ( Trie vs _ ) = vs+lookupTrie ( p : ps ) ( Trie _ cs ) =+  case p of+   Nothing ->+     concatMap   ( lookupTrie ps ) ( Map.elems cs )+   _         ->+        maybe [] ( lookupTrie ps ) ( Map.lookup p       cs )+     ++ maybe [] ( lookupTrie ps ) ( Map.lookup Nothing cs )++isEmptyTrie :: TrieMap k a -> Bool+isEmptyTrie ( Trie vs cs ) = null vs && null cs++trieFromList :: Ord k => [ ( [ Maybe k ], v ) ] -> TrieMap k v+trieFromList = Foldable.foldl' ( \ t ( k, v ) -> insertTrie k v t ) mempty++mapMaybeATrie :: ( Ord k, Applicative f ) => ( a -> f ( Maybe b ) ) -> TrieMap k a -> f ( TrieMap k b )+mapMaybeATrie f ( Trie vs cs ) =+  Trie+    <$> mapMaybeA f vs+    <*> ( `Map.traverseMaybeWithKey` cs )+         ( \ _key -> fmap ( guarded ( not . isEmptyTrie ) ) . mapMaybeATrie f )++type InstanceKey = [ Maybe TypeHead ]++instanceKey :: Instance -> InstanceKey+instanceKey ( Instance { instanceQuantTy = qty } ) =+  map typeHead $ Vec.toList $ quantTyBody ( mkQuantTyBody ( Quant qty ) )++argsTypeHeads :: Vec n ( Type Ty ) -> [ Maybe TypeHead ]+argsTypeHeads = Vec.toList . fmap typeHead++typeHead :: Type Ty -> Maybe TypeHead+typeHead = \case+  FunTy {} ->+    Just FunTyHead+  TyConAppTy tc _args ->+    case tc of+      GenerativeTyCon ( DataTyCon dc ) ->+        Just $ TyConHead $ dataTyConTag dc+      FamilyTyCon {} ->+        Nothing+  TyVarTy {} ->+    Nothing++-- | An instance environment.+type InstEnv = forall nbArgs. ClassTyCon nbArgs -> TrieMap TypeHead Instance++-- | The superclass structure of built-in classes.+classSuperclasses :: forall nbArgs. ClassTyCon nbArgs -> ( Vec nbArgs ( Type Ty ) -> [ Type Ct ] )+classSuperclasses cls =+  case cls of+    NotTyCon        -> noSCs+    LogicalTyCon    -> noSCs+    RelEqTyCon      -> noSCs+    RelOrdTyCon     -> \ ( a ::: b ::: VNil ) -> [ RelEq a b ]+    PlusTyCon       -> noSCs+    MinusTyCon      -> noSCs+    AddTyCon        -> noSCs+    SubTyCon        -> noSCs+    MultTyCon       -> noSCs+    DivTyCon        -> noSCs+    RemTyCon        -> noSCs+    ComplementTyCon -> noSCs+    BitwiseTyCon    -> noSCs+    ShiftTyCon      -> noSCs+  where+    noSCs = const []++-- | Built-in top-level class instances, with associated defaulting assignments.+classInstancesWithDefaults :: forall nbClsArgs. ClassTyCon nbClsArgs -> TrieMap TypeHead Instance+classInstancesWithDefaults cls =+  trieFromList . map ( \ i -> ( instanceKey i, i ) ) $+    case cls of+      NotTyCon        -> [i1]+      LogicalTyCon    -> [ii2]+      RelEqTyCon      -> [ii2, ff2, if2, fi2, str2]+      RelOrdTyCon     -> [ii2, ff2, if2, fi2, str2]+      PlusTyCon       -> [i1, f1]+      MinusTyCon      -> [i1, f1]+      -- TODO <https://github.com/well-typed/c-expr/issues/24>+      --+      -- Support pointer arithmetic.+      AddTyCon        -> [ii2, ff2, if2, fi2]+      SubTyCon        -> [ii2, ff2, if2, fi2]+      MultTyCon       -> [ii2, ff2, if2, fi2]+      DivTyCon        -> [ii2, ff2, if2, fi2]+      RemTyCon        -> [ii2]+      ComplementTyCon -> [i1]+      BitwiseTyCon    -> [ii2]+      -- TODO <https://github.com/well-typed/c-expr/issues/25>+      --+      -- Improve defaulting of shift operands.+      ShiftTyCon      -> [ii2]+  where++    primIntTy    = PrimIntInfoTy $ CIntegralType $ Runtime.IntLike $ Runtime.Int Runtime.Signed+    primDoubleTy = PrimFloatInfoTy Runtime.DoubleType++    dfltToInt, dfltToDouble :: DefaultingProposal ( S Z )+    dfltToInt    ( a ::: VNil ) = NE.singleton ( a, primIntTy    )+    dfltToDouble ( a ::: VNil ) = NE.singleton ( a, primDoubleTy )++    dfltToEqual :: DefaultingProposal ( S ( S Z ) )+    dfltToEqual ( a ::: b ::: VNil ) = NE.singleton ( a, b )++    i1, f1, ii2, ff2, if2, fi2, str2 :: Instance+    i1   = mkNAry [ dfltToInt    ] ( IntLike   ::: VNil )+    f1   = mkNAry [ dfltToDouble ] ( FloatLike ::: VNil )+    ii2  = mkNAry [ dfltToEqual ] ( IntLike   ::: IntLike   ::: VNil )+    ff2  = mkNAry [ dfltToEqual ] ( FloatLike ::: FloatLike ::: VNil )+    if2  = mkNAry [ ] ( IntLike   ::: FloatLike ::: VNil )+    fi2  = mkNAry [ ] ( FloatLike ::: IntLike   ::: VNil )+    str2 = mkNAryNoForall ( String ::: String ::: VNil )++    mkNAryNoForall :: forall nbArgs. Vec nbArgs ( Type Ty ) -> Instance+    mkNAryNoForall tys =+      let qty :: Vec Z ( Type Ty ) -> QuantTyBody ( Vec nbArgs ( Type Ty ) )+          qty _ = QuantTyBody [] tys+      in+        Vec.withDict tys $+          Instance+            { instanceQuantTy  = qty+            , instanceDefaults = []+            }++    mkNAry :: [ DefaultingProposal nbArgs ] -> Vec nbArgs ( Type Ty -> Type Ty ) -> Instance+    mkNAry dflts tcs =+      Vec.withDict tcs $+        Instance+          { instanceQuantTy  = \ args -> QuantTyBody [] ( Vec.zipWith ($) tcs args )+          , instanceDefaults = dflts+          }++-- | Get the 'DataTyConTag' associated with a type constructor.+dataTyConTag :: DataTyCon args -> DataTyConTag+dataTyConTag tc = TyConTag $ I# ( dataToTag# tc )++-- | Get the 'ClassTyConTag' associated with a class.+classTyConTag :: ClassTyCon args -> ClassTyConTag+classTyConTag cls = TyConTag $ I# ( dataToTag# cls )++{-------------------------------------------------------------------------------+  Typechecking macros: constraint solving monad+-------------------------------------------------------------------------------}++data Solubility+  = Soluble+  | Insoluble+  deriving stock ( Eq, Ord, Show )+data InertSet =+  InertSet+    { inertDicts :: !( Map ClassTyConTag ( TrieMap TypeHead ( ( Type Ct, CtOrigin ), Solubility ) ) )+    , inertEqs   :: ![ ( ( Type Ct, CtOrigin ), Solubility ) ]+    }+  deriving stock Show++emptyInertSet :: InertSet+emptyInertSet =+  InertSet { inertDicts = Map.empty, inertEqs = [] }++modifyingInerts :: ( InertSet -> InertSet ) -> TcSolveM ()+modifyingInerts f =+  State.modify' $+    \ st@( SolverState { solverInerts = inerts } ) ->+       st { solverInerts = f inerts }++inertCts :: InertSet -> ( Cts, Cts )+inertCts ( InertSet { inertDicts = dicts, inertEqs = eqs } ) =+  partitionEithers ( concatMap ( fmap classify . Foldable.toList ) $ dicts )+    <>+  partitionEithers ( map classify eqs )+  where+    classify ( a, sol ) =+      case sol of+        Soluble   -> Right a+        Insoluble -> Left a++mapMaybeInerts :: ( Type Ct -> Maybe ( Type Ct ) ) -> InertSet -> ( InertSet, Cts )+mapMaybeInerts f inerts@( InertSet { inertDicts = dicts, inertEqs = eqs } ) =+  let kick :: ( ( Type Ct, CtOrigin ), Solubility ) -> Writer.Writer Cts ( Maybe ( ( Type Ct, CtOrigin ), Solubility ) )+      kick ct@( ( ctPred, ctOrig ), _ ) =+        case f ctPred of+          Just ctPred' -> do+            Writer.tell [ ( ctPred', ctOrig ) ]+            return Nothing+          Nothing ->+            return $ Just ct+      ( keptDicts, kickedDicts ) =+        Writer.runWriter $+          ( `Map.traverseMaybeWithKey` dicts ) \ _key ->+            fmap ( guarded ( not . isEmptyTrie ) ) . mapMaybeATrie kick+      ( keptEqs  , kickedEqs   ) = Writer.runWriter $ mapMaybeA kick eqs+   in ( inerts { inertDicts = keptDicts, inertEqs = keptEqs }+      , kickedDicts ++ kickedEqs+      )++-- | State for the 'TcSolveM' constraint solving monad.+data SolverState+  = SolverState+  { solverSubst    :: !( Subst TyVar )+  , solverInerts   :: !InertSet+  , solverWorkList :: !Cts+  }+  deriving stock Show++-- | Monad for solving constraints.+type TcSolveM = StateT SolverState TcUniqueM++initSolverState :: Cts -> SolverState+initSolverState cts0 =+  SolverState+    { solverSubst    = mempty+    , solverInerts   = emptyInertSet+    , solverWorkList = cts0+    }++emitWork :: Subst TyVar -> Cts -> TcSolveM ()+emitWork subst newCts = do+  unless ( null newCts ) $+    debugTraceM $+      unlines $+        "emitting new work" : map ( ( " - " ++ ) . show ) newCts+  State.modify' $+    \ st@( SolverState+          { solverSubst    = subst0+          , solverWorkList = wl0 } ) ->+        st+          { solverSubst    = subst0 <> subst+          , solverWorkList = wl0 ++ newCts+          }+  kickOut subst++addInertDict :: Solubility+             -> ( ( ClassTyCon nbArgs, Vec nbArgs ( Type Ty ) ), CtOrigin )+             -> InertSet -> InertSet+addInertDict sol ( ( cls, args ), ctOrig ) inerts@( InertSet { inertDicts = dicts } ) =+  inerts { inertDicts = Map.alter doInsert ( classTyConTag cls ) dicts }+    where+      ct = Class cls args+      key = argsTypeHeads args+      doInsert = Just . insertTrie key ( ( ct, ctOrig ), sol ) . fromMaybe mempty++addInertEq :: Solubility -> ( Type Ct, CtOrigin ) -> InertSet -> InertSet+addInertEq sol eq@( NomEqPred lhs rhs, _ ) inerts@( InertSet { inertEqs = eqs } )+  | not $ any seen eqs+  = inerts { inertEqs = eqs ++ [ ( eq, sol ) ] }+  where+    seen ( ( NomEqPred lhs' rhs', _ ), _ )+      =  ( lhs `eqType` lhs' && rhs `eqType` rhs' )+      || ( lhs `eqType` rhs' && rhs `eqType` lhs' )+    seen _ = False+addInertEq _ _ inerts = inerts++nextWorkItem :: TcSolveM ( Maybe ( Type Ct, CtOrigin ) )+nextWorkItem = do+  st@( SolverState { solverSubst = subst, solverWorkList = wl } ) <- State.get+  case wl of+    [] -> return Nothing+    ( ctPred, ctOrig ) : others -> do+      State.put $ st { solverWorkList = others }+      return $ Just ( applySubst subst ctPred, ctOrig )++solvingLoop :: ( ( Type Ct, CtOrigin ) -> TcSolveM () ) -> TcSolveM ()+solvingLoop solveOne = loop 1+  where+    loop :: Int -> TcSolveM ()+    loop !iter = do+      mbWorkItem <- nextWorkItem+      Foldable.for_ mbWorkItem \ workItem -> do+        debugTraceM $+          unlines+            [ "solvingLoop: iteration #" ++ show iter+            , "work item: " ++ show workItem+            ]+        solveOne workItem+        loop ( iter + 1 )++runTcSolveM :: Cts -> TcSolveM a -> TcUniqueM ( a, ( Subst TyVar, ( Cts, Cts ) ) )+runTcSolveM cts ( State.StateT f ) =+  fmap aux $ f ( initSolverState cts )++  where+    aux :: ( a, SolverState ) -> ( a, ( Subst TyVar, ( Cts, Cts ) ) )+    aux ( a, st ) =+      ( a, ( solverSubst st , inertCts ( solverInerts st ) ) )++{-------------------------------------------------------------------------------+  Typechecking macros: constraint solving+-------------------------------------------------------------------------------}++-- | Solve a constraint.+solveCt :: Defaulting -> InstEnv -> ( Type Ct, CtOrigin ) -> TcSolveM ()+solveCt defaulting instEnv ( ct, ctOrig ) =+  case ct of+    NomEqPred a b ->+      -- NB: we don't do any defaulting in equality constraints.+      --+      -- The reasoning is that, with the current type system, every equality+      -- constraint arises from a class constraint, e.g. if we have+      --   AddRes a b ~ c+      -- we necessarily have an 'AddRes a b' class constraint as well.+      --+      -- Hence defaulting of equality constraints happens as a by-product of+      -- defaulting of class constraints.+      solveEqCt ctOrig a b+    Class cls args ->+      solveDictCt defaulting ctOrig cls ( instEnv cls ) args++-- | Solve an equality constraint.+solveEqCt :: CtOrigin -> Type Ty -> Type Ty -> TcSolveM ()+solveEqCt ctOrig lhs rhs = do+  ( ( (), UnifyResult eqs errs ), innerSubst ) <-+    lift $ lift $ ( `State.runStateT` mempty ) $ Writer.runWriterT $+      unifyType ctOrig NotSwapped lhs rhs+  let+    sameOld other =+      case other of+        NomEqPred lhs' rhs'+          |  lhs `eqType` lhs' && rhs `eqType` rhs'+          || lhs `eqType` rhs' && rhs `eqType` lhs'+          -> Left ()+        _ -> Right other+    ( noProgress, progress ) =+      partitionEithers $+        map+          ( \ ( ct, orig ) -> ( , orig ) <$> sameOld ct )+          eqs+    mkInsol :: UnificationError -> Maybe ( Type Ct, CtOrigin )+    mkInsol ( CouldNotUnify @ki _rea ctOrig' lhs' rhs' ) =+      ( eqT @ki @Ty ) <&> \ Refl ->+        ( NomEqPred lhs' rhs', ctOrig' )++  modifyingInerts $+      ( appEndo $ foldMap ( Endo . addInertEq Insoluble ) $ mapMaybe ( mkInsol . fst ) errs )+    . ( if null noProgress then id else addInertEq Soluble ( NomEqPred lhs rhs, ctOrig ) )+  emitWork innerSubst progress++-- | Look up a constraint in the inert set of the solver.+lookupCt :: Type Ct -> TcSolveM ( Maybe Bool )+lookupCt ct = do+  SolverState { solverInerts = inerts } <- State.get+  return $+    case ct of+      Class cls args -> do+        dicts <- Map.lookup ( classTyConTag cls ) $ inertDicts inerts+        finish $ mapMaybe ( matchWithSCs . first fst )+               $ lookupTrie ( argsTypeHeads args ) dicts+      NomEqPred {} ->+        finish $ mapMaybe ( matchEq . first fst )+               $ inertEqs inerts+  where+    finish :: [ Solubility ] -> Maybe Bool+    finish []   = Nothing+    finish sols = Just $ any ( == Soluble ) sols+    matchEq :: ( Type Ct, Solubility ) -> Maybe Solubility+    matchEq ( pty, sol ) =+      case pty of+        TyConAppTy {} -> Nothing+        NomEqPred lhs rhs -> do+          guard $+            any ( eqType ct ) [ pty, NomEqPred rhs lhs ]+          return sol+    matchWithSCs :: ( Type Ct, Solubility ) -> Maybe Solubility+    matchWithSCs ( pty, sol ) =+      case pty of+        NomEqPred {} -> Nothing+        Class cls' args' -> do+          guard $+            any ( eqType ct ) ( pty : classSuperclasses cls' args' )+          return sol++-- | Kick out constraints which mention variables from the domain of the+-- new substitution.+kickOut :: Subst TyVar -> TcSolveM ()+kickOut subst =+  unless ( isEmptySubst subst ) do+    plat <- lift $ lift getPlatform+    st@( SolverState { solverInerts = inerts, solverWorkList = wl0 } ) <- State.get+    let ( okInerts, kickedInerts ) = mapMaybeInerts ( mbKickOut plat ) inerts+    unless ( null kickedInerts ) do+      debugTraceM $ unlines+        [ "kickOut"+        , "subst: " ++ show subst+        , "inerts kicked out: " ++ show kickedInerts+        ]+      State.put $+        st { solverInerts = okInerts, solverWorkList = wl0 ++ kickedInerts }+  where+    mbKickOut :: Runtime.Platform -> Type Ct -> Maybe ( Type Ct )+    mbKickOut plat ct =+      let+        ctFVs = getFVs noBoundVars $ freeTyVarsOfType ct+      in+        if IntSet.null $ seenTvs ctFVs `IntSet.intersection` domain subst+        then+          Nothing+        else+          Just $ applySubstNormalise plat subst ct++-- | Whether to do defaulting or not.+data Defaulting+  = DefaultTyVarsExcept !IntSet+  | Don'tDefault+  deriving stock ( Eq, Show )++-- | Solve a class constraint by looking up in the provided instance environment+-- for this class.+solveDictCt+  :: Defaulting+      -- ^ Do defaulting as well (if possible)?+  -> CtOrigin+  -> ClassTyCon nbArgs+  -> TrieMap TypeHead Instance+  -> Vec nbArgs ( Type Ty )+  -> TcSolveM ()+solveDictCt doDefault ctOrig cls instEnv args = do+  matchingDict <- lookupCt ct+  case matchingDict of+    Just {} -> do+      debugTraceM $ unlines+        [ "solveDictCt: constraint discharged (matching inert)"+        , "ct: " ++ show ct ]+      return ()+    Nothing -> do+      matches <- lift $ mapMaybeA matcher $ lookupTrie ( argsTypeHeads args ) instEnv+      case matches of+        [] -> do+          debugTraceM $ unlines+            [ "solveDictCt: insoluble; adding constraint to inert set"+            , "ct: " ++ show ct ]+          modifyingInerts $+            addInertDict Insoluble ( ( cls, args ), ctOrig )+        ( newCts, subst ) : rest+          | null rest+          , isAtomicSubst subst+          , all ( isAtomicType . fst ) newCts+            -- Non-atomicity means we are dealing with a family of instances,+            -- e.g. @instance forall a. C (IntLike a)@, which really stands+            -- for a family of instances in Haskell-land.+            --+            -- NB: this is the only place where we could possibly introduce+            -- non-atomic types.+          -> do+            debugTraceM $ unlines+              [ "solveDictCt: solved constraint"+              , "ct: " ++ show ct+              , "context: " ++ show newCts+              , "subst: " ++ show subst ]+            emitWork subst newCts+        _ -> do+          debugTraceM $ unlines+            [ "solveDictCt: multiple solutions; adding constraint to inert set"+            , "ct: " ++ show ct ]+          modifyingInerts $+            addInertDict Soluble ( ( cls, args ), ctOrig )+    where+      ct = Class cls args+      matcher :: Instance -> TcUniqueM ( Maybe ( Cts, Subst TyVar ) )+      matcher inst = do+        matchRes <- matchOneInst ctOrig cls inst args+        case matchRes of+          Nothing ->+            do debugTraceM $+                 unlines+                    [ "solveDictCt: matchOne FAILURE"+                    , "ct: " ++ show ct+                    ]+               return Nothing+          Just ( ( newCts, matchSubst ), dfltCands ) -> do+            case doDefault of+              Don'tDefault -> do+                debugTraceM $+                  unlines+                    [ "solveDictCt: matchOne SUCCESS (not defaulting)"+                    , "ct: " ++ show ct+                    , "subst: " ++ show matchSubst+                    ]+                return $ Just ( newCts, matchSubst )+              DefaultTyVarsExcept qtvs -> do+                candSubsts <- lift dfltCands+                  -- Only do defaulting when no candidate type variables+                  -- for quantification are involved.+                  -- (Alternatively we could choose to default only+                  -- a subset of the type variables, but we don't do so for now.)+                case filter ( doesNotRefine qtvs matchSubst ) candSubsts of+                  [] -> do+                    debugTraceM $+                      unlines+                        [ "solveDictCt: matchOne SUCCESS (no defaulting)"+                        , "qtvs: " ++ show qtvs+                        , "ct: " ++ show ct+                        , "subst: " ++ show matchSubst+                        ]+                    return $ Just ( newCts, matchSubst )+                  -- TODO <https://github.com/well-typed/c-expr/issues/26>+                  --+                  -- Instead of picking the first one, we should accumulate all+                  -- candidate defaulting substitutions for all constraints and+                  -- try to find a consistent set of defaulting assignments.+                  dfltSubst1 : _ -> do+                    debugTraceM $+                      unlines+                        [ "solveDictCt: matchOne SUCCESS (defaulting)"+                        , "qtvs: " ++ show qtvs+                        , "ct: " ++ show ct+                        , "matchSubst: " ++ show matchSubst+                        , "dfltSubst: " ++ show dfltSubst1+                        ]+                    return $ Just ( newCts, dfltSubst1 )++-- | Check that the second substitution does not "further substitute" the+-- given set of type variables.+--+-- Assumes that the second substitution refines the first one, i.e. that one+-- can arrive at the second substitution by adding more substitutions to the+-- first.+--+-- Example: @qtvs = {α}@, @subst1 = {α ↦ IntLike β}@.+--+--  1. @subst2 = {α ↦ IntLike β}@.+--     OK: @α@ maps to the same thing in both substitutions.+--  2. @subst2 = {α ↦ IntLike (Int Signed), β ↦ Int Signed }@+--     Not OK: @α@ is further substituted.+doesNotRefine :: IntSet -> Subst tv -> Subst tv -> Bool+doesNotRefine qtvs ( Subst matchSubst ) ( Subst dfltSubst ) =+  all noRefinement $ IntSet.toList qtvs+    where+      noRefinement tv =+        case IntMap.lookup tv dfltSubst of+          Nothing -> True+          Just ( _, dfltTy ) ->+            case IntMap.lookup tv matchSubst of+              Nothing -> False+              Just ( _, matchTy ) ->+                matchTy `eqType` dfltTy++-- | Match a constraint against an instance.+--+-- The returned first substitution does the matching, if that was possible.+-- The second substitution is an optional defaulting substitution.+matchOneInst+  :: forall nbArgs+  .  CtOrigin+  -> ClassTyCon nbArgs+  -> Instance+  -> Vec nbArgs ( Type Ty )+  -> TcUniqueM ( Maybe ( ( Cts, Subst TyVar ), TcPureM [ Subst TyVar ] ) )+matchOneInst ctOrig cls+  ( Instance+    { instanceQuantTy = ( iqty :: Vec nbBinders ( Type Ty ) -> QuantTyBody ( Vec instNbArgs ( Type Ty ) ) )+    , instanceDefaults = mbDflt }+    ) args+    | Just Refl <- Vec.withDict args $ Nat.eqNat @nbArgs @instNbArgs+    =+  runTcGenMSubst do+    let orig = ClassInstMetaOrigin $ Quant $ fmap ( fmap ( Class cls ) ) iqty+    ( instBndrs, instArgTys ) <- instantiate ctOrig orig iqty+    liftUnifyM $+      unifyTypes ctOrig NotSwapped instArgTys args+    matchSubst <- State.get+    return $+      mapMaybeA ( tryDefault ctOrig matchSubst . ( $ instBndrs ) ) mbDflt+  | otherwise+  = panicPure $ unlines+      [ "matchOneInst: incorrect class arity"+      , "class: " ++ show cls+      ]++tryDefault :: CtOrigin -> Subst TyVar -> NE.NonEmpty ( Type Ty, Type Ty ) -> TcPureM ( Maybe ( Subst TyVar ) )+tryDefault ctOrig matchSubst dfltEqs =+  fmap ( fmap snd ) $ runTcUnifyMSubst matchSubst $+    traverse ( uncurry $ unifyType ( DefaultingOrigin ctOrig ) NotSwapped ) dfltEqs++{-------------------------------------------------------------------------------+  Typechecking macros: top-level entry point to constraint solving+-------------------------------------------------------------------------------}++-- | Top-level type-checking monad.+type TcTopM = ExceptT MacroTcError TcUniqueM++simplifyAndDefault :: IntSet -> Cts -> TcTopM ( Subst TyVar, Cts )+simplifyAndDefault quantTvs cts =+  do+    ( (), ( subst, ( insols, inerts ) ) ) <- lift $ runTcSolveM cts $ solvingLoop solveOne+    Foldable.for_ ( NE.nonEmpty insols ) \ errs ->+      Except.throwError ( TcInconsistentConstraints $ NE.singleton ( NE.toList errs ) )+    return ( subst, inerts )++  where+    solveOne = solveCt ( DefaultTyVarsExcept quantTvs ) classInstancesWithDefaults++{-------------------------------------------------------------------------------+  Evaluation+--------------------------------------------------------------------------------++We sometimes need to be able to evaluate macros, in particular when a macro+appears as the size of an array:++  #define N 16+  #define M(X) 2 * X+  void foo(int arr[M(N) + N]);++To evaluate macros, we use the 'Value' existential data type++  data Value = forall ty. Value { valueType :: SType ty, value :: ty }++That is, a value is a dependent pair, consisting of a (singleton for a) type+and a value of that type.++Evaluation proceeds as follows:++  (1) Constants.++    The constant 16 in the definition of N is really++      IntegerLiteral+        { integerLiteralText = "16"+        , integerLiteralType = Int Signed+        , integerLiteralValue = 16 :: Integer+        }++    We turn this into a value by using 'promoteIntLikeType' from c-expr.+    This gives us a type singleton with a witness that the type satisfies+    the 'Integral' typeclass. So we can thus construct the value:++      Value+        { valueType = ( ... :: SType CInt )+        , value     = fromInteger 16 :: CInt+        }++    See e.g. the ValueInt case of 'evaluateTerm'.++  (2) MFun: built-in functions.++    Recall that we desugar built-in functions to custom typeclasses.+    For example, (+) corresponds to:++      class Add a b where+        type AddRes a b+        (+) :: a -> b -> AddRes a b++    This means that, to evaluate any particular instantiation of (+), we+    need to know the types we are instantiating (+) at . Once we have these, we+    can use the following function provided by the c-expr library++      singAdd :: SType a -> SType b -> ( SType ( AddRes a b ), a -> b -> AddRes a b )++    whose implementation looks like a giant case match:++      singAdd SInt   SInt    = ( SInt   , (+) :: CInt -> CInt -> CInt )+      singAdd SFloat SDouble = ( SDouble, (+) :: CFloat -> CDouble -> CDouble )+      ...++    This function behaves like a lookup function which, given a pair of types,+    returns the 'Add' instance at that type.++    The function 'inferVFun' thus does two things:++      1. As its name indicates, it infers the instantiated type of a function.+      2. It also returns the appropriate lookup function, such as 'singAdd' for+         (+), and stores it in the typechecked macro AST. Once we are done+         with typechecking, we will have elaborated all the types and will thus+         be able to pass specific argument types to this lookup function in+         order to evaluate the 'MFun'.++  (3) Macro functions: evaluating macro arguments, and calling other macros.++    After typechecking each macro, we also compute a function which allows+    evaluating this macro; see the call to 'evaluateExpr' in 'tcMacro'.+    This is a function that takes a vector of argument values, and returns the+    result of evaluating the macro on these arguments (see 'C.Expr.Typecheck.Type.FunValue').++    To do this, we create a new value environment (using 'Map Name Value'),+    and then call 'evaluateExpr'.+    When we get to a macro argument (in the 'Var' case of 'evaluateTerm'),+    we simply look up in the map to obtain the value.++    In this way, after typechecking each macro, we can produce a function of+    type 'Vec n Value -> Value' which takes a collection of argument values,+    with their types, and evaluates the macro.++    This "macro evaluation function" is then stored in the macro environment,+    so that if we come across a macro function application we can evaluate it,+    in the same way as the 'MFun' case in (2).++One final observation. Suppose we see the expression "x + y". During typechecking,+the approach outlined above stores the 'singAdd' function in the AST, of type:++  SType a -> SType b -> (SType (AddRes a b), a -> b -> AddRes a b)++You might wonder: if we know the types of the arguments, we should be able to+pass them at that point. However:++  - we haven't yet done constraint solving (which happens at the end), so+    the types might be metavariables,+  - we might have polymorphic types, such as "#define Add(x,y) x + y".++So the simplest thing to do to implement the evaluator is to:++  - store the types alongside the values,+  - use the types to look up the relevant instance for evaluation.++This is easier than erasing the types and dealing with typeclass specialisation,+which is what GHC does.+-}++evaluateExpr :: IntMap Value -> TypeEnv -> Expr ctx Tc -> Value+evaluateExpr argVals tyEnv = \case+  Term tm  -> evaluateTerm argVals tyEnv tm+  TyApp{}  -> NoValue+  VaApp ( XAppTc  NoFunValue               ) _funName _args ->+    NoValue+  VaApp @_ @_ @m (XAppTc (FunValue @n _ fn)) _funName  args ->+    -- We have stored the function that performs evaluation in the XAppTc+    -- field of the AST. For example, for addition, we have wrapped+    --+    --   singAdd :: SType ty1 -> SType ty2 -> ( SType (AddRes ty1 ty2), ty1 -> ty2 -> AddRes ty1 ty2 )+    --+    -- to obtain the function ( fn :: Vec 2 Value -> Value ).+    Vec.withDict args $+      case Nat.eqNat @( S m ) @n of+        Just Refl ->+          fn $ fmap ( evaluateExpr argVals tyEnv ) args+        Nothing ->+          NoValue++evaluateTerm :: IntMap Value -> TypeEnv -> Term ctx Tc -> Value+evaluateTerm argVals tyEnv = \case+  Literal x -> evaluateLit x+  -- Local macro parameter, e.g. @X@ in @#define AddOne(X) X+1@.+  LocalParam i -> fromMaybe NoValue $ IntMap.lookup (idxToInt i) argVals+  Var ( XVarTc   NoFunValue         _ ) _nm _args -> NoValue+  Var ( XVarTc ( FunValue @n _ fn ) _ ) nm args+    -> Vec.reifyList args $ \ ( argsVec :: Vec m ( Expr ctx Tc ) ) ->+        case Nat.eqNat @n @m of+          Nothing ->+            panicPure $ unlines+              [ "Mismatched arity in evaluation of macro function call"+              , "function: " ++ show nm+              , "expected number of arguments: " ++ show ( Nat.reflectToNum @n Proxy :: Int )+              , "arguments: " ++ show args+              ]+          Just Refl ->+            -- This is a macro call; evaluate the argument and apply the+            -- evaluator function. See also the 'MApp' case in 'evaluateExpr'.+            fn $ fmap ( evaluateExpr argVals tyEnv ) argsVec++-- Evaluation of integer and floating literals; useful, for example, when+-- calculating the length for arrays.+evaluateLit :: Literal -> Value+evaluateLit = \case+  ValueLit vaLit -> case vaLit of+    ValueInt lit ->+      let i = integerLiteralValue lit+          ty = integerLiteralType lit+      in+        Runtime.promoteIntLikeType ty $ \ sTy ->+          Value+            ( ValSType $ Runtime.SArithmetic $ Runtime.SIntegral $ Runtime.SIntLike sTy )+            ( fromInteger i )+    ValueFloat lit ->+      let ty = floatingLiteralType lit+      in+        Runtime.promoteFloatingType ty $ \ case+          sTy@Runtime.SFloatType ->+            Value+              ( ValSType $ Runtime.SArithmetic $ Runtime.SFloatLike sTy )+              ( CFloat  $ floatingLiteralFloatValue  lit )+          sTy@Runtime.SDoubleType ->+            Value+              ( ValSType $ Runtime.SArithmetic $ Runtime.SFloatLike sTy )+              ( CDouble $ floatingLiteralDoubleValue lit )+    -- We do not evaluate character and string functions.+    ValueChar   {} -> NoValue+    ValueString {} -> NoValue+  -- We do not evaluate type functions.+  TypeLit    {} -> NoValue++naturalMaybe :: ValSType ty -> ty -> Maybe Natural+naturalMaybe ( ValSType ty ) i =+  case ty of+    Runtime.SArithmetic ( Runtime.SIntegral iTy ) ->+      Runtime.witnessIntegralType @Integral iTy $+        let j = toInteger i+        in if j < 0+           then Nothing+           else Just $ fromInteger j+    _ -> Nothing++{-------------------------------------------------------------------------------+  Typechecking macros: generalisation (internal)+-------------------------------------------------------------------------------}++-- | Typecheck a macro expression body (internal).+--+-- Also returns the body type (post-inference, pre-quantification) so the+-- caller can tell whether the macro denotes a type or a value.+tcExpr ::+     forall ctx.+     TypeEnv+  -> Identifier                    -- ^ name of the macro+  -> Vec ctx Identifier            -- ^ macro arguments+  -> Expr ctx (Ps (Maybe QuantTy)) -- ^ macro body+  -> Either MacroTcError ( Type Ty, Quant ( FunValue, Type Ty ) )+tcExpr tyEnv macroNm args body =+  let plat = Runtime.hostPlatform in+  throwErrors $ runTcM plat tyEnv $ ( `State.evalStateT` Unique 0 ) $ Except.runExceptT do++    -- Step 1: infer the type.+    ( ( ( body', ( argTys, bodyTy ) ), ctsOrigs ), mbErrs ) <- lift $ inferTop macroNm args body+    Foldable.traverse_ ( Except.throwError . TcErrors ) ( NE.nonEmpty mbErrs )++    -- Step 2: compute the set of metavariables that are candidates for quantification.+    let+      freeTvs =+        seenTvs $ getFVs noBoundVars $+          freeTyVarsOfTypes ( bodyTy : Vec.toList argTys )++    -- Step 3: simplify and default constraints.+    ( ctSubst, simpleCts ) <- simplifyAndDefault freeTvs ctsOrigs++    -- Step 4: generalise.+    let+      qtvsFVs =+        getFVs noBoundVars $+          freeTyVarsOfTypes $+            fmap ( applySubstNormalise plat ctSubst ) $+              Vec.toList argTys ++ [ bodyTy ]+      qtvsList = reverse $ seenTvsRevList qtvsFVs+      ctTvs =+        seenTvs $ getFVs noBoundVars $+          freeTyVarsOfTypes (applySubstNormalise plat ctSubst <$> map fst simpleCts)+      ambigs = ctTvs IntSet.\\ seenTvs qtvsFVs++    debugTraceM $+      unlines+        [ "tcExpr"+        , "argTys: " ++ show argTys+        , "bodyTy: " ++ show bodyTy+        , "freeTvs: " ++ show freeTvs+        , "ctSubst: " ++ show ctSubst+        , "simpleCts: " ++ show simpleCts+        , "qtvs: " ++ show qtvsList+        , "ambigs: " ++ show ambigs+        ]++    -- Panic if there are metavariables in the constraints that are not+    -- in the argument/result type, i.e. ambiguous type variables.+    -- These should have been defaulted away.+    unless (IntSet.null ambigs) $+      panicPure $+        unlines+          [ "tcExpr: ambiguous type variables"+          , "ambigs: " ++ show ambigs+          , "qtvs: " ++ show qtvsList+          , "cts: " ++ show simpleCts+          , "argTys: " ++ show argTys+          , "bodyTy: " ++ show bodyTy+          ]++    -- Panic if there are any non-atomic types, which don't have natural+    -- counterparts in Haskell-land. See 'isAtomicType'.+    let allAtomic = and [ all isAtomicType argTys+                        , isAtomicType bodyTy+                        , all ( isAtomicType . fst ) simpleCts+                        ]++    unless allAtomic $+      panicPure $+        unlines+          [ "tcExpr computed a non-atomic type"+          , "qtvs: " ++ show qtvsList+          , "cts: " ++ show simpleCts+          , "argTys: " ++ show argTys+          , "bodyTy: " ++ show bodyTy+          ]++    return $+      ( bodyTy+      , Vec.reifyList qtvsList \ qtvs ->+          Quant \ tys ->+            let quantSubst = mkSubst $ Vec.toList $ Vec.zipWith (,) qtvs tys+                finalSubst = quantSubst <> ctSubst+                norm :: Type ki -> Type ki+                norm = applySubstNormalise plat finalSubst+                evalFun =+                  Vec.withDict args $+                    FunValue ( getIdentifier macroNm ) $ \ (argVals :: Vec ctx Value) ->+                      evaluateExpr+                        ( IntMap.fromList $ zip [0..] $ Vec.toList argVals )+                        tyEnv+                        body'+            in QuantTyBody+                { quantTyQuant = map norm ( fmap fst simpleCts )+                , quantTyBody  = ( evalFun, mkFunTy ( fmap norm ( argTys ) ) ( norm bodyTy ) )+                }+      )+  where+    throwErrors ( _, ( err : errs ) ) = Left $ TcErrors ( err NE.:| errs )+    throwErrors ( res, [] ) = res++data MacroTcError+  -- | Errors in the constraint-generation phase,+  -- e.g. we failed to unify some types.+  = TcErrors !( NE.NonEmpty ( TcError, SrcSpan ) )+  -- | A collection of class constraints was inconsistent.+  | TcInconsistentConstraints !( NE.NonEmpty Cts )+  | TcUnsupportedTypeWithLocalParameters Identifier [Identifier]+  -- | A type-like macro reduces to an incomplete type (e.g. @void@,+  -- @const void@) at the top level. Such a type cannot be used to declare+  -- a value, so the macro cannot be translated to a usable Haskell binding.+  -- Pointer-to-incomplete (e.g. @void *@) is fine and is not rejected here.+  | TcIncompleteTypeMacro Identifier+  deriving stock ( Show, Generic )++instance Eq MacroTcError where+  _ == _ = True++pprMacroTcError :: MacroTcError -> Text+pprMacroTcError tcMacroErr =+  Text.intercalate "\n" $+    case tcMacroErr of+      TcErrors errs ->+        map ( \ ( err, _srcSpan ) -> pprTcError err ) ( NE.toList errs )+      TcInconsistentConstraints ctss ->+        "Constraints are inconsistent:"+        : concat+          [ ( "  - " <> Text.pack ( show i ) <> ":" )+          : map ( \ ( ct, _orig ) -> "    '" <> Text.pack ( show ct ) <> "'" ) cts+          | cts <- NE.toList ctss+          | i <- [ ( 1 :: Int ) .. ]+          ]+      TcUnsupportedTypeWithLocalParameters nm ps -> [+          "Unsupported type-like macro expression with local parameters:"+        , getIdentifier nm <> " with parameters " <> Text.pack (show ps)+        ]+      TcIncompleteTypeMacro nm -> [+          "Type-like macro " <> getIdentifier nm <> " expands to an incomplete type"+        , "(such as 'void' or 'const void') at the top level."+        ]++mapMaybeA :: Applicative m => ( a -> m ( Maybe b ) ) -> [ a ] -> m [ b ]+mapMaybeA f =+  foldr ( Applicative.liftA2 ( maybe id (:) ) . f ) ( pure [] )+{-# INLINEABLE mapMaybeA #-}++guarded :: ( m -> Bool ) -> m -> Maybe m+guarded cond m = do+  guard $ cond m+  return m++{-------------------------------------------------------------------------------+  Quick & dirty testing framework+-------------------------------------------------------------------------------}++debugTraceM :: Applicative f => String -> f ()+debugTraceM+  | debug+  = traceM+  | otherwise+  = const $ pure ()+{-# INLINE debugTraceM #-}++debug :: Bool+debug = False
+ src/C/Expr/Typecheck/Interface/Type.hs view
@@ -0,0 +1,90 @@+-- | Interface for typechecked macro type expressions+--+-- Intended for qualified import+--+-- @+-- import C.Expr.Typecheck.Interface.Type qualified as T+-- @+module C.Expr.Typecheck.Interface.Type (+    Expr(..)+  , Qual(..)+  , fromExpr+  )+  where++import Control.Exception (Exception)+import Data.Nat (Nat (..))+import Data.Vec.Lazy (Vec (..))+import DeBruijn (idxToInt)++import C.Expr.Syntax qualified as M+import C.Expr.Syntax.TTG.Parse+import C.Expr.Util.Panic++data Expr var =+    TypeLit M.TypeLit+  | Var var+  | App Qual (Expr var)++deriving stock instance Eq   var => Eq         (Expr var)+deriving stock instance Show var => Show       (Expr var)+deriving stock instance             Functor     Expr+deriving stock instance             Foldable    Expr+deriving stock instance             Traversable Expr++-- | Type qualifier+--+-- This is a straight-forward representation of the C syntax. For a detailed+-- discussion of @const@, see+-- https://github.com/well-typed/hs-bindgen/issues/1521.+data Qual =+    Pointer+  | Const+  deriving stock (Eq, Show)++data ConversionError =+    -- | Unexpected value literal (e.g., the integer @42@)+    UnexpectedValueLiteralInType String+    -- | Unexpected local parameter in type+  | UnexpectedLocalParameterInType Int+    -- | A unary type function received multiple arguments+  | UnexpectedMultipleArgumentsToUnaryTypeFunction+    -- | Unexpected function application on a value (not a type)+  | UnexpectedValueFunctionApplicationInType String+  deriving stock (Show)++instance Exception ConversionError++-- | Translate into the typechecked AST assuming the expression is a type.+--+-- For variables, we don't use their name but their annotations.+fromExpr :: forall ctx ann. M.Expr ctx (Ps ann) -> Expr ann+fromExpr = go+  where+    go :: M.Expr ctx (Ps ann) -> Expr ann+    go = \case+      M.Term (M.Literal x) ->+        fromLit x+      M.Term (M.LocalParam i) ->+        panicPure $ show $ UnexpectedLocalParameterInType (idxToInt i)+      M.Term (M.Var (XVarPs{psAnn}) _nm _args) ->+        Var psAnn+      M.TyApp fun args -> do+        let arg = myHead args+        case fun of+          M.Pointer -> App Pointer $ go arg+          M.Const   -> App Const   $ go arg+      M.VaApp _ fun _ ->+        panicPure $ show $ UnexpectedValueFunctionApplicationInType (show fun)++    fromLit :: M.Literal -> Expr ann+    fromLit = \case+      M.TypeLit x         -> TypeLit x+      M.ValueLit x        -> panicPure $ show $ UnexpectedValueLiteralInType (show x)++    myHead :: Vec ('S n) a -> a+    myHead = \case+      (x ::: VNil) ->+        x+      (_ ::: _ ::: _) ->+        panicPure $ show UnexpectedMultipleArgumentsToUnaryTypeFunction
+ src/C/Expr/Typecheck/Interface/Value.hs view
@@ -0,0 +1,85 @@+-- | Interface for typechecked macro value expressions+--+-- Intended for qualified import+--+-- @+-- import C.Expr.Typecheck.Interface.Value qualified as V+-- @+module C.Expr.Typecheck.Interface.Value (+    Expr(..)+  , fromExpr+  )+  where++import Control.Exception (Exception)+import Data.GADT.Compare (GEq (..))+import Data.Nat (Nat (..))+import Data.Type.Equality ((:~:) (..))+import Data.Vec.Lazy (Vec)+import DeBruijn (Idx)++import C.Expr.Syntax qualified as M+import C.Expr.Syntax.TTG.Parse+import C.Expr.Util.Panic++data Expr ctx var =+    Literal M.ValueLit+  | LocalParam (Idx ctx)+  | Var var [Expr ctx var]+  | forall n . App (M.VaFun (S n)) (Vec (S n) (Expr ctx var))++deriving stock instance (Show var) => Show        (Expr ctx var)+deriving stock instance               Functor     (Expr ctx)+deriving stock instance               Foldable    (Expr ctx)+deriving stock instance               Traversable (Expr ctx)++instance Eq var => Eq (Expr ctx var) where+  Literal l1    == Literal l2    = l1 == l2+  LocalParam n1 == LocalParam n2 = n1 == n2+  Var v1 as1    == Var v2 as2    = v1 == v2 && as1 == as2+  App f1 xs1    == App f2 xs2    =+    case f1 `geq` f2 of+      Just Refl -> xs1 == xs2+      Nothing   -> False+  _ == _ = False++data ConversionError =+    -- | Unexpected type in a value expression (e.g., @int@)+    UnexpectedTypeInValue String+    -- | Unexpected function application on a type (not a value)+  | UnexpectedTypeFunctionApplicationInValue String+  deriving stock (Show)++instance Exception ConversionError++-- | Translate into the typechecked AST assuming the expression is a value.+--+-- For variables, we don't use their name but their annotations.+fromExpr ::+     forall ctx ann.+     M.Expr ctx (Ps ann)+  -> Expr ctx ann+fromExpr = go+  where+    go :: M.Expr ctx (Ps ann) -> Expr ctx ann+    go = \case+      M.Term (M.Literal x) ->+        fromLit x+      M.Term (M.LocalParam i) ->+        LocalParam i+      M.Term (M.Var XVarPs{psAnn} _nm args) ->+        Var psAnn (map go args)+      M.TyApp fun _ ->+        panicPure $ show $ UnexpectedTypeFunctionApplicationInValue (show fun)+      M.VaApp _ fun args ->+        App fun $ fmap go args++    fromLit :: M.Literal -> Expr ctx ann+    fromLit = \case+      M.TypeLit x ->+        panicPure $ show $ UnexpectedTypeInValue (show x)+      M.ValueLit x -> Literal $ case x of+        M.ValueInt y    -> M.ValueInt y+        M.ValueFloat y  -> M.ValueFloat y+        M.ValueChar y   -> M.ValueChar y+        M.ValueString y -> M.ValueString y
+ src/C/Expr/Typecheck/Type.hs view
@@ -0,0 +1,751 @@+{-# LANGUAGE CPP #-}++#if __GLASGOW_HASKELL__ >=908+{-# LANGUAGE TypeAbstractions #-}+#endif++-- | Macro types: the types that we infer for macros.+module C.Expr.Typecheck.Type (+    -- * Names+    VarName+  , FunName+    -- * Annotations+  , XVar(..)+  , XApp(..)+    -- * Pass+  , Tc+    -- * Type inference+  , QuantTy+  , simpleType+  , TypeEnv+  , ParamEnv+    -- ** Type system+  , Type(..)+  , IntegralType(..)+  , Kind(Ty, Ct)+  , Quant(..)+  , QuantTyBody(..)+  , mkQuantTyBody+  , mkFunTy+    -- ** Type variables+  , MetaTyVar(..)+  , MetaOrigin(..)+  , InstOrigin(..)+  , TyVar(..)+  , SkolemTyVar(..)+  , Unique(..)+    -- ** Type constructors+  , TyCon(..)+  , GenerativeTyCon(..)+  , FamilyTyCon(..)+  , DataTyCon(..)+    -- ** Constraints+  , ClassTyCon(..)+  , CtOrigin(..)+    -- ** Pattern synonyms for types+  , pattern Class+  , pattern Data+  , pattern FamApp+  , pattern Not+  , pattern Plus+  , pattern Minus+  , pattern Complement+  , pattern Logical+  , pattern RelEq+  , pattern RelOrd+  , pattern Add+  , pattern Sub+  , pattern Mult+  , pattern Div+  , pattern Rem+  , pattern Bitwise+  , pattern Shift+  , pattern PrimIntInfoTy+  , pattern PrimFloatInfoTy+  , pattern IntLike+  , pattern FloatLike+  , pattern String+  , pattern Ptr+  , pattern Tuple+  , pattern PlusRes+  , pattern MinusRes+  , pattern AddRes+  , pattern SubRes+  , pattern MultRes+  , pattern DivRes+  , pattern RemRes+  , pattern ComplementRes+  , pattern BitsRes+  , pattern ShiftRes+  , pattern IntTy+  , pattern HsIntTy+  , pattern CharTy+  , pattern CharLitTy+  , pattern MacroTypeTy+    -- ** Query+  , tyVarName+  , tyVarNames+  , tyVarUnique+  , eqType+    -- ** Pretty-printing+  , pprCtOrigin+  , pprMetaOrigin+    -- * Evaluation+  , ValSType(..)+  , Value(..)+  , FunValue(..)+  ) where++import Data.Foldable qualified as Foldable+import Data.GADT.Compare+import Data.IntMap (IntMap)+import Data.Kind qualified as Hs+import Data.List.NonEmpty qualified as NE+import Data.Map (Map)+import Data.Maybe (fromJust)+import Data.Nat (Nat (..))+import Data.Proxy+import Data.Text (Text)+import Data.Text qualified as Text+import Data.Type.Equality+import Data.Type.Nat (SNat (..), SNatI)+import Data.Type.Nat qualified as Nat+import Data.Vec.Lazy (Vec (..))+import Data.Vec.Lazy qualified as Vec+import Foreign.C.Types+import Foreign.Ptr qualified as Foreign+import GHC.Generics (Generic)+import GHC.Show (showSpace)+import Numeric.Natural++import C.Type qualified as Runtime++import C.Expr.Syntax+import C.Expr.Util.TestEquality++{-------------------------------------------------------------------------------+  Type system for macros+-------------------------------------------------------------------------------}++type VarName = Text+newtype Unique = Unique { uniqueInt :: Int }+  deriving newtype ( Enum, Eq, Show )+  deriving stock Generic++data Kind+  -- | The kind of types.+  = Ty+  -- | The kind of constraints.+  | Ct+  deriving stock ( Eq, Ord, Show )++type Type :: Kind -> Hs.Type+data Type ki where+  -- | A type variable.+  TyVarTy :: !TyVar -> Type Ty+  -- | A function type.+  FunTy :: !( NE.NonEmpty ( Type Ty ) ) -> !( Type Ty ) -> Type Ty+  -- | An (exactly saturated) application of a 'TyCon' to arguments.+  TyConAppTy :: !( TyCon nbArgs res ) -> !( Vec nbArgs ( Type Ty ) ) -> Type res+  -- | Nominal equality.+  NomEqPred :: !( Type Ty ) -> !( Type Ty ) -> Type Ct++mkFunTy :: Foldable f => f ( Type Ty ) -> Type Ty -> Type Ty+mkFunTy args = case Foldable.toList args of+  [] -> id+  ( a : as ) -> \ res -> FunTy ( a NE.:| as ) res++-- | A qualified quantified type @forall tys. cts => args -> res@.+type Quant :: Hs.Type -> Hs.Type+data Quant res where+  Quant+    :: forall nbBinders res+    .  ( SNatI nbBinders )+    => { quantTyBodyFn :: !( Vec nbBinders ( Type Ty ) -> QuantTyBody res ) }+    -> Quant res+deriving stock instance Functor Quant++instance Eq (QuantTyBody body) => Eq ( Quant body ) where+  qty1@( Quant @n1 _ ) == qty2@( Quant @n2 _ ) =+    case Nat.eqNat @n1 @n2 of+      Nothing   -> False+      Just Refl -> mkQuantTyBody qty1 == mkQuantTyBody qty2++-- | The body of a quantified type (what's under the forall).+type QuantTyBody :: Hs.Type -> Hs.Type+data QuantTyBody body+  = QuantTyBody+  { quantTyQuant :: ![ Type Ct ]+  , quantTyBody  :: !body+  }+  deriving stock ( Show, Generic, Functor, Foldable, Traversable )++instance Eq ( QuantTyBody ( Type ki ) ) where+  QuantTyBody cts1 body1 == QuantTyBody cts2 body2 =+    and [ length cts1 == length cts2+        , all ( uncurry eqType ) ( zip cts1 cts2 )+        , eqType body1 body2+        ]+instance Eq ( QuantTyBody ( FunValue, Type ki ) ) where+  QuantTyBody cts1 (funVal1, body1) == QuantTyBody cts2 (funVal2, body2) =+    and [ length cts1 == length cts2+        , all ( uncurry eqType ) ( zip cts1 cts2 )+        , eqType body1 body2+        , funVal1 == funVal2+        ]++instance Eq ( QuantTyBody ( Vec n ( Type ki ) ) ) where+  QuantTyBody cts1 body1 == QuantTyBody cts2 body2 =+    and [ length cts1 == length cts2+        , all ( uncurry eqType ) ( zip cts1 cts2 )+        , eqTypes body1 body2+        ]++instance Show ( Type ki ) where+  showsPrec p = \case+    TyVarTy tv -> showString ( show tv )+    TyConAppTy tc tys ->+      showParen (p >= 10 && not (null tys)) $+          showsPrec ( if null tys then p else 11 ) tc+        . foldr ( \ a acc -> showSpace . showsPrec 11 a . acc ) id tys+    FunTy as r ->+      showParen (p >= 0) $+        foldr ( \ a acc -> showsPrec 0 a . showString " -> " . acc ) id as . showsPrec 0 r+    NomEqPred a b ->+      showParen (p >= 5) $+        showsPrec 5 a . showString " ~ " . showsPrec 5 b++instance Show body => Show ( Quant body ) where+  showsPrec p0 quantTy@( Quant @nbBinders _ ) =+    showParen ( p0 >= 0 && not ( null qtvs && null cts ) ) $+        ( if null qtvs+          then id else+            showString "forall"+          . foldr ( \ ( _, tv ) acc -> showSpace . showString ( Text.unpack tv ) . acc ) id qtvs+          . showString ". "+        )+      . foldr ( \ a acc -> showsPrec 0 a . showString " => " . acc ) id cts+      . showsPrec 0 body+    where+      qtvs :: [ ( Int, Text ) ]+      qtvs = Foldable.toList $ tyVarNames @nbBinders+      QuantTyBody cts body = mkQuantTyBody quantTy++tyVarNames :: forall nbVars. SNatI nbVars => Vec nbVars ( Int, Text )+tyVarNames = fromJust $ Vec.fromListPrefix nms+  where+    n = Nat.reflectToNum @nbVars Proxy+    nms+      | n > 3+      = map ( \ i -> ( i, "a" <> Text.pack ( show i ) ) ) [ 1 .. n ]+      | otherwise+      = take n [ ( 1, "a" ), ( 2, "b" ), ( 3, "c" ) ]++mkQuantTyBody :: Quant body -> QuantTyBody body+mkQuantTyBody ( Quant @nbBinders body ) =+  body $ fmap ( uncurry mkSkol ) $ tyVarNames @nbBinders+  where+    mkSkol :: Int -> VarName -> Type Ty+    mkSkol i tv = TyVarTy $ SkolemTv $ SkolemTyVar tv ( Unique i )++data TyVar+  = SkolemTv {-# UNPACK #-} !SkolemTyVar+  | MetaTv   {-# UNPACK #-} !MetaTyVar+  deriving stock Generic++tyVarName :: TyVar -> VarName+tyVarName = \case+  SkolemTv sk  -> skolemTyVarName sk+  MetaTv   tau -> metaTyVarName tau++tyVarUnique :: TyVar -> Unique+tyVarUnique = \case+  SkolemTv sk  -> skolemTyVarUnique sk+  MetaTv   tau -> metaTyVarUnique   tau++instance Show TyVar where+  show tv =+    concat+      [ Text.unpack ( tyVarName tv )+      ++ case tv of+          MetaTv {} -> "_" ++ show u ++ "[tau]"+          SkolemTv {} -> "" -- assumes there is never shadowing in skolems+      ]+      where Unique u = tyVarUnique tv++data SkolemTyVar+  = SkolemTyVar+    { skolemTyVarName   :: !VarName+    , skolemTyVarUnique :: !Unique+    }+  deriving stock Generic+instance Show SkolemTyVar where+  show sk = show ( SkolemTv sk )+instance Show MetaTyVar where+  show tau = show ( MetaTv tau )++data MetaTyVar+  = MetaTyVar+    { metaTyVarName   :: !VarName+    , metaTyVarUnique :: !Unique+    , metaOrigin      :: !MetaOrigin+    }+  deriving stock Generic++type TyCon :: Nat -> Kind -> Hs.Type+data TyCon nbArgs res where+  GenerativeTyCon :: !( GenerativeTyCon nbArgs ki ) -> TyCon nbArgs ki+  FamilyTyCon     :: !( FamilyTyCon     nbArgs    ) -> TyCon nbArgs Ty+deriving stock instance Eq ( TyCon nbArgs res )++type GenerativeTyCon :: Nat -> Kind -> Hs.Type+data GenerativeTyCon nbArgs res where+  DataTyCon      :: !( DataTyCon   nbArgs ) -> GenerativeTyCon nbArgs Ty+  ClassTyCon     :: !( ClassTyCon  nbArgs ) -> GenerativeTyCon nbArgs Ct+deriving stock instance Eq ( GenerativeTyCon nbArgs res )++type DataTyCon :: Nat -> Hs.Type+data DataTyCon nbArgs where+  -- TODO <https://github.com/well-typed/c-expr/issues/6>+  --+  -- Split the type language into types of types, and types of values.+  -- | Type of types+  MacroTypeTyCon :: DataTyCon Z++  -- | Type constructor for @Void@+  VoidTyCon      :: DataTyCon Z+  -- | Type constructor for character literals (different from the C @char@+  -- integral type)+  CharLitTyCon   :: DataTyCon Z+  -- | Unary type constructor for integral types, such as @Int@ or @UShort@.+  IntLikeTyCon   :: DataTyCon ( S Z )+  -- | Unary type constructor for floating-point types, such as 'Float' or 'Double'+  FloatLikeTyCon :: DataTyCon ( S Z )+  -- | Type constructor for pointers+  PtrTyCon       :: DataTyCon ( S Z )++  -- | Tuple type constructors+  TupleTyCon     :: !(SNat (S (S n))) -> DataTyCon ( S ( S n ) )+    -- Invariant: the stored 'SNat' matches the arity of the tuple++  -- | Family of nullary type constructors for arguments to 'IntLikeTyCon'.+  PrimIntInfoTyCon   :: !IntegralType -> DataTyCon Z+  -- | Family of nullary type constructors for arguments to 'FloatLikeTyCon'.+  PrimFloatInfoTyCon :: !Runtime.FloatingType -> DataTyCon Z++data IntegralType+  = CIntegralType !Runtime.IntegralType+  | HsIntType+  deriving stock ( Eq, Ord, Show, Generic )++deriving stock instance Eq  ( DataTyCon nbArgs )+deriving stock instance Ord ( DataTyCon nbArgs )++type FamilyTyCon :: Nat -> Hs.Type+data FamilyTyCon nbArgs where+  -- | Return type of unary addition.+  PlusResTyCon       :: FamilyTyCon ( S Z )+  -- | Return type of unary negation.+  MinusResTyCon      :: FamilyTyCon ( S Z )+  -- | Return type of binary addition.+  AddResTyCon        :: FamilyTyCon ( S ( S Z ) )+  -- | Return type of binary subtraction.+  SubResTyCon        :: FamilyTyCon ( S ( S Z ) )+  -- | Return type of binary multiplication.+  MultResTyCon       :: FamilyTyCon ( S ( S Z ) )+  -- | Return type of binary division/quotient.+  DivResTyCon        :: FamilyTyCon ( S ( S Z ) )+  -- | Return type of unary bitwise negation.+  ComplementResTyCon :: FamilyTyCon ( S Z )+  -- | Return type of binary remainder operation.+  RemResTyCon        :: FamilyTyCon ( S ( S Z ) )+  -- | Return type of binary bitwise logical operations.+  BitsResTyCon       :: FamilyTyCon ( S ( S Z ) )+  -- | Return type of binary bitwise shift operations,+  -- as a function of the type of the argument being shifted.+  ShiftResTyCon      :: FamilyTyCon ( S Z )++deriving stock instance Eq  ( FamilyTyCon nbArgs )+deriving stock instance Ord ( FamilyTyCon nbArgs )++type ClassTyCon :: Nat -> Hs.Type+data ClassTyCon nbArgs where+  -- | Class type constructor for @Not@+  NotTyCon        :: ClassTyCon ( S Z )+  -- | Class type constructor for @Logical@+  LogicalTyCon    :: ClassTyCon ( S ( S Z ) )+  -- | Class type constructor for @RelEq@+  RelEqTyCon      :: ClassTyCon ( S ( S Z ) )+  -- | Class type constructor for @RelOrd@+  RelOrdTyCon     :: ClassTyCon ( S ( S Z ) )+  -- | Class type constructor for @Plus@ (unary plus)+  PlusTyCon       :: ClassTyCon ( S Z )+  -- | Class type constructor for @Minus@ (unary minus)+  MinusTyCon      :: ClassTyCon ( S Z )+  -- | Class type constructor for @Add@+  AddTyCon        :: ClassTyCon ( S ( S Z ) )+  -- | Class type constructor for @Sub@+  SubTyCon        :: ClassTyCon ( S ( S Z ) )+  -- | Class type constructor for @Mult@+  MultTyCon       :: ClassTyCon ( S ( S Z ) )+  -- | Class type constructor for @Div@+  DivTyCon        :: ClassTyCon ( S ( S Z ) )+  -- | Class type constructor for @Rem@+  RemTyCon        :: ClassTyCon ( S ( S Z ) )+  -- | Class type constructor for @Complement@+  ComplementTyCon :: ClassTyCon ( S Z )+  -- | Class type constructor for @Bitwise@+  BitwiseTyCon    :: ClassTyCon ( S ( S Z ) )+  -- | Class type constructor for @Shift@+  ShiftTyCon      :: ClassTyCon ( S ( S Z ) )++deriving stock instance Eq  ( ClassTyCon nbArgs )+deriving stock instance Ord ( ClassTyCon nbArgs )++instance Show ( TyCon n ki ) where+  showsPrec p = \case+    GenerativeTyCon tc -> showsPrec p tc+    FamilyTyCon     tc -> showsPrec p tc++instance Show ( GenerativeTyCon n ki ) where+  showsPrec p = \case+    DataTyCon   tc -> showsPrec p tc+    ClassTyCon  tc -> showsPrec p tc++instance Show ( DataTyCon n ) where+  showsPrec p = \case+    VoidTyCon                 -> showString "Void"+    MacroTypeTyCon            -> showString "Type"+    PtrTyCon                  -> showString "Ptr"+    CharLitTyCon              -> showString "CharLit"+    IntLikeTyCon              -> showString "IntLike"+    FloatLikeTyCon            -> showString "FloatLike"+    PrimIntInfoTyCon   inty   -> showsPrec p inty+    PrimFloatInfoTyCon floaty -> showsPrec p floaty+    TupleTyCon i              -> showString $ "Tuple" ++ show (Nat.snatToNatural i)+instance Show ( FamilyTyCon n ) where+  show = \case+    PlusResTyCon       -> "PlusRes"+    MinusResTyCon      -> "MinusRes"+    AddResTyCon        -> "AddRes"+    SubResTyCon        -> "SubRes"+    MultResTyCon       -> "MultRes"+    DivResTyCon        -> "DivRes"+    RemResTyCon        -> "RemRes"+    ComplementResTyCon -> "ComplementRes"+    BitsResTyCon       -> "BitsRes"+    ShiftResTyCon      -> "ShiftRes"++instance Show ( ClassTyCon n ) where+  show = \case+    NotTyCon        -> "Not"+    LogicalTyCon    -> "Logical"+    RelEqTyCon      -> "RelEq"+    RelOrdTyCon     -> "RelOrd"+    PlusTyCon       -> "Plus"+    MinusTyCon      -> "Minus"+    AddTyCon        -> "Add"+    SubTyCon        -> "Sub"+    MultTyCon       -> "Mult"+    DivTyCon        -> "Div"+    RemTyCon        -> "Rem"+    ComplementTyCon -> "Complement"+    BitwiseTyCon    -> "Bitwise"+    ShiftTyCon      -> "Shift"++{-------------------------------------------------------------------------------+  Type environment+-------------------------------------------------------------------------------}++type QuantTy = Quant (FunValue, Type Ty)+-- | The typing environment: every in-scope typechecked macro mapped to its+--   quantified type.+--+-- For @typedef@s we assume that the annotation informs us about the type.+type TypeEnv = Map Identifier QuantTy+-- | De Bruijn indexed environment of parameters /local to the macro+-- definition/.+type ParamEnv = IntMap   ( Type Ty )++{-------------------------------------------------------------------------------+  Pass definition+-------------------------------------------------------------------------------}++-- | The typecheck pass.+--+-- Unlike the parse pass 'C.Expr.Syntax.TTG.Parse.Ps', 'Tc' takes no annotation+-- parameter.+--+-- 1. The parse pass allows arbitrary user annotations.+--+-- 2. The typechecker 'C.Expr.Typecheck.tcMacros' gives the user the option of+-- specifying a type given an annotation (i.e., @typeOfAnn@).+--+-- 3. If the user gives such a type, it is stored in 'tcUserType'.+type Tc :: Pass+data Tc a++newtype instance XApp Tc = XAppTc FunValue+  deriving stock ( Eq, Show, Generic )++data instance XVar Tc = XVarTc {+      tcFunValue :: FunValue+      -- | If a variable refers to a type that is unavailable to the+      -- typechecker, the user must provide a type. For example, when a macro+      -- refers to a @typedef@, it must be labeled as a 'simpleType'.+    , tcUserType :: Maybe QuantTy+    }+  deriving stock ( Eq, Show, Generic )++-- | The type of simple, unparameterised types such as @typedef@s.+simpleType :: Quant (FunValue, Type Ty)+simpleType =+    Quant @Z $ \VNil ->+      QuantTyBody [] (NoFunValue , MacroTypeTy)++-- | A singleton for the type of a value, for use in evaluation of macros.+newtype ValSType ty = ValSType ( Runtime.SType ValSType ty )+  -- NB: this type ties the recursive knot of the open Runtime.SType type.+  --+  -- This type is defined here because it is tied to macro evaluation.+  -- In particular, if we decide to add support for evaluation macro tuples,+  -- we would need to add a constructor here to account for that.+ deriving newtype GEq+deriving stock instance Show ( ValSType ty )+instance Eq ( ValSType ty ) where+  ValSType ty1 == ValSType ty2 = defaultEq ty1 ty2+data Value where+  NoValue :: Value+  Value :: ValSType ty -> ty -> Value+instance Eq Value where+  NoValue == NoValue = True+  NoValue == Value {} = False+  Value {} == NoValue = False+  Value ty1 v1 == Value ty2 v2 =+    case geq ty1 ty2 of+      Nothing -> False+      Just Refl ->+        witnessValSType @Eq ty1 (v1 == v2)++-- | Produce class dictionaries for a class by matching on the singleton+-- for the type.+witnessValSType+  :: forall c ty r+  . ( forall x. c ( Foreign.Ptr x )+    , c CChar, c CSChar, c CUChar, c CShort, c CUShort, c CInt+    , c CUInt, c CLong, c CULong, c CLLong, c CULLong, c CPtrdiff+    , c CSize, c CBool, c CFloat, c CDouble, c () )+  => ValSType ty -> ( c ty => r ) -> r+witnessValSType ( ValSType ty ) f =+  Runtime.witnessType @c ( witnessValSType @c ) ty f++-- | A Haskell function that evaluates a macro function.+--+-- We sometimes need to be able to evaluate macros, in particular when a macro+-- appears as the size of an array:+--+-- @+--   #define N 16+--   #define M(X) 2 * X+--   void foo(int arr[M(N) + N]);+-- @+data FunValue where+  NoFunValue :: FunValue+  FunValue   :: SNatI n => FunName -> ( Vec n Value -> Value ) -> FunValue+instance Eq FunValue where+  NoFunValue    == NoFunValue    = True+  FunValue f1 _ == FunValue f2 _ = f1 == f2+  _             == _             = False++instance Show FunValue where+  show   NoFunValue      = "NoFunValue"+  show ( FunValue nm _ ) = Text.unpack nm++{-------------------------------------------------------------------------------+  Constraints & errors+-------------------------------------------------------------------------------}++-- | The textual name of a macro function.+type FunName = Text++-- | Why did we emit a constraint?+data CtOrigin+  = AppOrigin !FunName+  | FunInstOrigin !FunName+  | ClassInstOrigin !( Quant ( Type Ct ) ) !CtOrigin+  | DefaultingOrigin !CtOrigin+  deriving stock ( Generic, Show )++pprCtOrigin :: CtOrigin -> Text+pprCtOrigin = \case+  AppOrigin fun ->+    "In an application of '" <> fun <> "'."+  FunInstOrigin fun ->+    "In the instantiation of '" <> fun <> "'."+  ClassInstOrigin qty orig ->+    Text.unlines+      [ "From the context of the class instance '" <> Text.pack ( show qty ) <> "'."+      , pprCtOrigin orig ]+  DefaultingOrigin ct ->+    Text.unlines+      [ "When defaulting a constraint."+      , pprCtOrigin ct+      ]++-- | Why did we create a new metavariable?+data MetaOrigin+  = ExpectedFunTyResTy !FunName+  | ExpectedVarTy !Identifier+  | Inst { instOrigin :: !InstOrigin, instPos :: !Int }+  | FunParam !Identifier !( Identifier, Natural )+  | IntLitMeta !IntegerLiteral+  | FloatLitMeta !FloatingLiteral++deriving stock instance Show MetaOrigin++data InstOrigin+  = FunInstMetaOrigin !FunName+  | ClassInstMetaOrigin !( Quant ( Type Ct ) )+  deriving stock ( Generic, Show )++pprMetaOrigin :: MetaOrigin -> Text+pprMetaOrigin = \case+  ExpectedFunTyResTy funNm ->+    "the result type of '" <> Text.pack ( show funNm ) <> "'"+  ExpectedVarTy ( Identifier varNm ) ->+    "the type of the identifier '" <> varNm <> "'"+  Inst funNm i ->+    "the " <> speakNth i <> " type argument in the instantiation of '" <> Text.pack ( show funNm ) <> "'"+  FunParam ( Identifier funNm ) ( param, i ) ->+    "the type of the " <> speakNth (fromIntegral i) <> " parameter of '" <> funNm <> "' with name '" <> getIdentifier param <> "'"+  IntLitMeta i ->+    "the type of the integer literal '" <> Text.pack ( show i ) <> "'"+  FloatLitMeta f ->+    "the type of the floating-point literal '" <> Text.pack ( show f ) <> "'"++speakNth :: Int -> Text+speakNth n = Text.pack ( show n ) <> suffix+  where+    suffix+      | n >= 11 && n <= 13 = "th" -- 11, 12, 13 are non-standard+      | lastDigit == 1     = "st"+      | lastDigit == 2     = "nd"+      | lastDigit == 3     = "rd"+      | otherwise          = "th"+    lastDigit = n `rem` 10++{-------------------------------------------------------------------------------+  Syntactic type equality+-------------------------------------------------------------------------------}++-- | On-the-nose type equality.+eqType :: Type ki -> Type ki -> Bool+eqType ( TyVarTy tv1 ) ( TyVarTy tv2 ) = tyVarUnique tv1 == tyVarUnique tv2+eqType ( TyConAppTy tc1 args1 ) ( TyConAppTy tc2 args2 ) =+  case tc1 `equals2` tc2 of+    Nothing -> False+    Just Refl ->+      eqTypes args1 args2+eqType ( FunTy args1 res1 ) ( FunTy args2 res2 )+  =  length args1 == length args2+  && all ( uncurry eqType ) ( NE.zip args1 args2 )+  && eqType res1 res2+eqType _ _ = False++-- | 'eqType' for a vector of types.+eqTypes :: Vec n ( Type ki ) -> Vec n ( Type ki ) -> Bool+eqTypes = ( and . ) . Vec.zipWith eqType++{-------------------------------------------------------------------------------+  Pattern synonyms for types+-------------------------------------------------------------------------------}++pattern Class :: ClassTyCon nbArgs -> Vec nbArgs ( Type Ty ) -> Type Ct+pattern Class cls args = TyConAppTy ( GenerativeTyCon ( ClassTyCon cls ) ) args+{-# COMPLETE Class, NomEqPred #-}++pattern Data :: () => ki ~ Ty => DataTyCon nbArgs -> Vec nbArgs ( Type Ty ) -> Type ki+pattern Data tc args = TyConAppTy ( GenerativeTyCon ( DataTyCon tc ) ) args+pattern FamApp :: () => ki ~ Ty => FamilyTyCon nbArgs -> Vec nbArgs ( Type Ty ) -> Type ki+pattern FamApp tc args = TyConAppTy ( FamilyTyCon tc ) args++pattern Not :: Type Ty -> Type Ct+pattern Not a = Class NotTyCon ( a ::: VNil )+pattern Plus :: Type Ty -> Type Ct+pattern Plus a = Class PlusTyCon ( a ::: VNil )+pattern Minus :: Type Ty -> Type Ct+pattern Minus a = Class MinusTyCon ( a ::: VNil )+pattern Complement :: Type Ty -> Type Ct+pattern Complement a = Class ComplementTyCon ( a ::: VNil )++pattern Logical :: Type Ty -> Type Ty -> Type Ct+pattern Logical a b = Class LogicalTyCon ( a ::: b ::: VNil )+pattern RelEq :: Type Ty -> Type Ty -> Type Ct+pattern RelEq a b = Class RelEqTyCon ( a ::: b ::: VNil )+pattern RelOrd :: Type Ty -> Type Ty -> Type Ct+pattern RelOrd a b = Class RelOrdTyCon ( a ::: b ::: VNil )+pattern Add :: Type Ty -> Type Ty -> Type Ct+pattern Add a b = Class AddTyCon ( a ::: b ::: VNil )+pattern Sub :: Type Ty -> Type Ty -> Type Ct+pattern Sub a b = Class SubTyCon ( a ::: b ::: VNil )+pattern Mult :: Type Ty -> Type Ty -> Type Ct+pattern Mult a b = Class MultTyCon ( a ::: b ::: VNil )+pattern Div :: Type Ty -> Type Ty -> Type Ct+pattern Div a b = Class DivTyCon ( a ::: b ::: VNil )+pattern Rem :: Type Ty -> Type Ty -> Type Ct+pattern Rem a b = Class RemTyCon ( a ::: b ::: VNil )+pattern Bitwise :: Type Ty -> Type Ty -> Type Ct+pattern Bitwise a b = Class BitwiseTyCon ( a ::: b ::: VNil )+pattern Shift :: Type Ty -> Type Ty -> Type Ct+pattern Shift a b = Class ShiftTyCon ( a ::: b ::: VNil )++pattern PrimIntInfoTy :: IntegralType -> Type Ty+pattern PrimIntInfoTy inty = Data (PrimIntInfoTyCon inty) VNil+pattern PrimFloatInfoTy :: Runtime.FloatingType -> Type Ty+pattern PrimFloatInfoTy floaty = Data (PrimFloatInfoTyCon floaty) VNil+pattern IntLike :: Type Ty -> Type Ty+pattern IntLike intLike = Data IntLikeTyCon (intLike ::: VNil)+pattern FloatLike :: Type Ty -> Type Ty+pattern FloatLike floatLike = Data FloatLikeTyCon (floatLike ::: VNil)+pattern String :: Type Ty+pattern String = Tuple (SS' (SS' SZ)) (Ptr CharTy ::: HsIntTy ::: VNil)+pattern Ptr :: Type Ty -> Type Ty+pattern Ptr ty = Data PtrTyCon (ty ::: VNil)++pattern Tuple :: () => ( nbArgs ~ S (S n) ) => SNat (S (S n)) -> Vec nbArgs (Type Ty) -> Type Ty+pattern Tuple l as = Data ( TupleTyCon l ) as++pattern PlusRes :: Type Ty -> Type Ty+pattern PlusRes a = FamApp PlusResTyCon ( a ::: VNil )+pattern MinusRes :: Type Ty -> Type Ty+pattern MinusRes a = FamApp MinusResTyCon ( a ::: VNil )+pattern AddRes :: Type Ty -> Type Ty -> Type Ty+pattern AddRes a b = FamApp AddResTyCon ( a ::: b ::: VNil )+pattern SubRes :: Type Ty -> Type Ty -> Type Ty+pattern SubRes a b = FamApp SubResTyCon ( a ::: b ::: VNil )+pattern MultRes :: Type Ty -> Type Ty -> Type Ty+pattern MultRes a b = FamApp MultResTyCon ( a ::: b ::: VNil )+pattern DivRes :: Type Ty -> Type Ty -> Type Ty+pattern DivRes a b = FamApp DivResTyCon ( a ::: b ::: VNil )+pattern RemRes :: Type Ty -> Type Ty -> Type Ty+pattern RemRes a b = FamApp RemResTyCon ( a ::: b ::: VNil )+pattern ComplementRes :: Type Ty -> Type Ty+pattern ComplementRes a = FamApp ComplementResTyCon ( a ::: VNil )+pattern BitsRes :: Type Ty -> Type Ty -> Type Ty+pattern BitsRes a b = FamApp BitsResTyCon ( a ::: b ::: VNil )+pattern ShiftRes :: Type Ty -> Type Ty+pattern ShiftRes a = FamApp ShiftResTyCon ( a ::: VNil )+++pattern IntTy :: Type Ty+pattern IntTy = IntLike ( PrimIntInfoTy ( CIntegralType ( Runtime.IntLike ( Runtime.Int Runtime.Signed ) ) ) )+pattern HsIntTy :: Type Ty+pattern HsIntTy = IntLike ( PrimIntInfoTy HsIntType )+pattern CharTy :: Type Ty+pattern CharTy = IntLike ( PrimIntInfoTy ( CIntegralType ( Runtime.CharLike Runtime.Char ) ) )++pattern CharLitTy :: Type Ty+pattern CharLitTy = Data CharLitTyCon VNil++pattern MacroTypeTy :: Type Ty+pattern MacroTypeTy = Data MacroTypeTyCon VNil
+ src/C/Expr/Util/Panic.hs view
@@ -0,0 +1,31 @@+module C.Expr.Util.Panic (+    panicPure+  , panicIO+  ) where++import Control.Exception+import Control.Monad.IO.Class+import GHC.Stack++-- | Unexpected (e.g. invariant violation) conditions.+data PanicException = PanicException !CallStack !String+  deriving Show++instance Exception PanicException where+    displayException (PanicException cs  msg) = unlines+        [ "PANIC!: the impossible happened"+        , pleaseReport+        , msg+        , prettyCallStack cs+        ]++pleaseReport :: String+pleaseReport = "Please report this as a bug at https://github.com/well-typed/c-expr/issues/"++-- | Panic in pure context+panicPure :: HasCallStack => String -> a+panicPure msg = throw (PanicException callStack msg)++-- | Panic in IO+panicIO :: (HasCallStack, MonadIO m) => String -> m a+panicIO msg = liftIO (throwIO (PanicException callStack msg))
+ src/C/Expr/Util/Parsec.hs view
@@ -0,0 +1,120 @@+module C.Expr.Util.Parsec (+    -- * Character streams+    caseInsensitive'+  , foldCharTokens+  , satisfyWith+    -- * General purpose+  , Consumer(..)+  , foldTokens+  ) where++import Control.Monad (guard)+import Data.Char (toLower)+import Text.Parsec (Consumed (..), ParseError, ParsecT, Reply (..), SourcePos,+                    State (..), Stream (..), mkPT, tokenPrim, unknownError,+                    (<?>))+import Text.Parsec.Error (Message (..), newErrorMessage)+import Text.Parsec.Pos (updatePosChar, updatePosString)++{-------------------------------------------------------------------------------+  Character streams+-------------------------------------------------------------------------------}++-- | Case-insensitive version of 'Text.Parsec.string''+--+-- Returns the parsed string (which may be different from the argument string).+caseInsensitive' :: Stream s m Char => String -> ParsecT s u m String+caseInsensitive' = \expected ->+    foldCharTokens (go [] expected) <?> expected+  where+    go :: String -> String -> Consumer Char String+    go acc []     = Done (reverse acc)+    go acc (x:xs) = Look { onEof   = Nothing+                         , onToken = \y -> do+                             guard (toLower x == toLower y)+                             return $ go (y:acc) xs+                         }++-- | Specialization of 'foldTokens' to streams of characters+foldCharTokens :: Stream s m Char => Consumer Char a -> ParsecT s u m a+foldCharTokens = foldTokens show updatePosString++-- | Generalization of 'Text.Parsec.satisfy' that returns evidence+satisfyWith :: Stream s m Char => (Char -> Maybe a) -> ParsecT s u m a+satisfyWith =+    tokenPrim show updatePos+  where+    updatePos :: SourcePos -> Char -> s -> SourcePos+    updatePos pos c _ = updatePosChar pos c++{-------------------------------------------------------------------------------+  General purpose+-------------------------------------------------------------------------------}++data Consumer t a =+    Done a+  | Look {+        onEof   :: Maybe a+      , onToken :: t -> Maybe (Consumer t a)+      }++-- | Fold a sequence of tokens; no input is consumed on failure.+--+-- This is a generalization of 'Text.Parsec.tokens'', which can be defined in terms of+-- 'foldTokens' as follows:+--+-- > tokens' showTokens updatePos expected =+-- >     foldTokens showTokens updatePos (go expected) <?> showTokens expected+-- >   where+-- >     go :: [t] -> Consumer t [t]+-- >     go []     = Done expected+-- >     go (t:ts) = Look { onEof   = Nothing+-- >                      , onToken = \t' -> guard (t == t') >> return (go ts)+-- >                      }+foldTokens :: forall s u m t a.+     Stream s m t+  => ([t] -> String)+  -> (SourcePos -> [t] -> SourcePos)+  -> Consumer t a+  -> ParsecT s u m a+foldTokens showTokens updatePos = \f ->+    mkPT $ \st -> aux st f+  where+    aux :: State s u -> Consumer t a -> m (Consumed (m (Reply s u a)))+    aux initState =+        walk [] (stateInput initState)+      where+        walk :: [t] -> s -> Consumer t a -> m (Consumed (m (Reply s u a)))+        walk acc rs (Done a)             = ok acc rs a+        walk acc rs Look{onEof, onToken} = do+            mNextToken <- uncons rs+            case mNextToken of+              Nothing       -> case onEof of+                                 Nothing -> err errEof+                                 Just a  -> ok acc rs a+              Just (t, rs') -> case onToken t of+                                 Nothing -> err (errUnexpected t)+                                 Just k  -> walk (t:acc) rs' k++        ok :: [t] -> s -> a -> m (Consumed (m (Reply s u a)))+        ok acc rs a = return $+            (if null acc then Empty else Consumed) $+              return $ Ok a finalState (unknownError finalState)+          where+           finalState :: State s u+           finalState = State{+                 statePos   = updatePos (statePos initState) (reverse acc)+               , stateUser  = stateUser initState+               , stateInput = rs+               }++        err :: ParseError -> m (Consumed (m (Reply s u a)))+        err e = return $ Empty $ return $ Error $ e++        errEof :: ParseError+        errEof =+            newErrorMessage (SysUnExpect "") (statePos initState)++        errUnexpected :: t -> ParseError+        errUnexpected t =+           newErrorMessage (SysUnExpect $ showTokens [t]) (statePos initState)
+ src/C/Expr/Util/TestEquality.hs view
@@ -0,0 +1,104 @@+{-# LANGUAGE CPP       #-}+{-# LANGUAGE MagicHash #-}++-- | Utilities for writing 'Eq' instances for GADTs+module C.Expr.Util.TestEquality (+    equals1+  , equals2+  ) where++import Data.GADT.Compare+import Data.Kind+import Data.Type.Equality+import GHC.Exts+import Unsafe.Coerce (unsafeCoerce)++-- $setup+-- >>> :seti -XDataKinds -XGADTs++{-------------------------------------------------------------------------------+  Utilities for writing 'Eq' instances for GADTs+-------------------------------------------------------------------------------}++infixr 4 `equals1`+infixr 4 `equals2`++-- | Check whether two GADT values of type @k ->Type@ are equal.+--+-- If so, also return a proof that the tags were equal.+--+-- NB: this is stricter than 'testEquality', as 'testEquality' is supposed+-- to return @Just Refl@ whenever the tags are equal, even when the values+-- themselves are different.+--+-- NB: Doesn't work for types with type indices not-directly implied by+-- constructor "tags":+--+-- >>> data SBool (b :: Bool) where STrue :: SBool True; SFalse :: SBool False+-- >>> instance Eq (SBool b) where STrue == STrue = True; SFalse == SFalse = False+-- >>> data Foo b = Foo1 (SBool b) | Foo2 (SBool b) deriving Eq+-- >>>  equals1 (Foo1 STrue) (Foo1 SFalse)+-- *** Exception: ...Non-exhaustive patterns in function ==+-- ...+--+-- The GHC generated Eq instance for SBool would have default case, so this example *could* work.+-- If you want to be safe, use 'Data.GADT.Compare.geq' from @some@ package.+--+equals1 :: forall a tag1 tag2.+  ( forall tag. Eq ( a tag )+#if MIN_VERSION_base(4,20,0)+  , forall tag. DataToTag ( a tag )+#endif+  ) => a tag1 -> a tag2 -> Maybe ( tag1 :~: tag2 )+equals1 k1 k2+  | -- Fail-fast: comparing the tag first.+    isTrue# ( dataToTag# k1 ==# dataToTag# k2 )+    -- Assume the types are the same; this allows us to use the 'Eq' instance.+  , Refl <- ( unsafeCoerce Refl :: tag1 :~: tag2 )+  , k1 == k2+  -- The values are equal (according to the 'Eq' instance): this justifies the+  -- unsafe coercion above, assuming that the 'Eq' instance is lawful.+  = Just $ unsafeCoerce Refl+  | otherwise+  = Nothing++-- | Check whether two GADT values of type @k -> l ->Type@ are equal.+--+-- If so, also return a proof that the tags were equal.+--+-- NB: this is stricter than 'testEquality', as 'testEquality' is supposed+-- to return @Just Refl@ whenever the tags are equal, even when the values+-- themselves are different.+equals2 :: forall a k1 k2 l1 l2.+  ( forall k l. Eq ( a k l)+#if MIN_VERSION_base(4,20,0)+  , forall k l. DataToTag ( a k l )+#endif+  ) => a k1 l1 -> a k2 l2 -> Maybe ( '( k1, l1 ) :~: '( k2, l2 ) )+equals2 k1 k2+  | -- Fail-fast: comparing the tag first.+    isTrue# ( dataToTag# k1 ==# dataToTag# k2 )+    -- Assume the types are the same; this allows us to use the 'Eq' instance.+  , Refl <- ( unsafeCoerce Refl :: '( k1, l1 ) :~: '( k2, l2 ) )+  , k1 == k2+  -- The values are equal (according to the 'Eq' instance): this justifies the+  -- unsafe coercion above, assuming that the 'Eq' instance is lawful.+  = Just $ unsafeCoerce Refl+  | otherwise+  = Nothing++{-------------------------------------------------------------------------------+  Internal auxiliary+-------------------------------------------------------------------------------}++-- | Wrapper that provides a 'GEq' instance definition using 'equals1'+type ApEq :: ( k -> Type ) -> k -> Type+newtype ApEq f a = ApEq ( f a )++instance forall f.+  ( forall tag. Eq ( f tag )+#if MIN_VERSION_base(4,20,0)+  , forall tag. DataToTag (f tag )+#endif+  ) => GEq ( ApEq f ) where+  geq ( ApEq k1 ) ( ApEq k2 ) = equals1 k1 k2
+ test/Main.hs view
@@ -0,0 +1,12 @@+module Main (main) where++import Test.Tasty++import Test.CExpr.Parse qualified as Parse+import Test.CExpr.Typecheck qualified as Typecheck++main :: IO ()+main = defaultMain $ testGroup "c-expr-dsl" [+      Parse.tests+    , Typecheck.tests+    ]
+ test/Test/CExpr/Parse.hs view
@@ -0,0 +1,18 @@+module Test.CExpr.Parse (+    tests+  ) where++import Test.Tasty++import Test.CExpr.Parse.Golden qualified as Golden+import Test.CExpr.Parse.Literal qualified as Literal+import Test.CExpr.Parse.Macro qualified as Macro+import Test.CExpr.Parse.Type qualified as Type++tests :: TestTree+tests = testGroup "parse" [+      Type.tests+    , Macro.tests+    , Literal.tests+    , Golden.tests+    ]
+ test/Test/CExpr/Parse/Golden.hs view
@@ -0,0 +1,147 @@+-- | Golden integration tests for 'C.Expr.Parse.Expr.parseMacro'+--+-- These tests use @libclang@ to tokenise the macros defined in+-- @test/fixtures/macros.h@, feed the token streams to 'parseMacro', and+-- compare the results against the golden file @test/fixtures/macros.golden@.+--+-- Golden file can be regenerated using the @--accept@ CLI option.+module Test.CExpr.Parse.Golden (tests) where++import Data.Bifunctor (Bifunctor (..))+import Data.ByteString.Lazy.Char8 qualified as LBS+import Data.Text (Text)+import Data.Text qualified as Text+import System.FilePath ((</>))+import System.IO.Unsafe (unsafePerformIO)+import Test.Tasty (TestName, TestTree, testGroup)+import Test.Tasty.Golden (goldenVsString)++import C.Expr.Parse+import C.Expr.Syntax++import Clang.Args+import Clang.CStandard+import Clang.Enum.Bitfield+import Clang.Enum.Simple+import Clang.HighLevel qualified as HighLevel+import Clang.HighLevel.Types+import Clang.LowLevel.Core+import Clang.Paths+import Clang.Version++import Paths_c_expr_dsl (getDataDir)++{-------------------------------------------------------------------------------+  Top-level+-------------------------------------------------------------------------------}++data TestCStandard = CExprC17 | CExprC23++testCStandardToCStandard :: TestCStandard -> CStandard+testCStandardToCStandard = \case+    CExprC17 -> C17+    CExprC23 -> C23++testCStandardToClangArg :: TestCStandard -> String+testCStandardToClangArg = \case+    CExprC17 -> "-std=c17"+    CExprC23 -> "-std=c2x"++tests :: TestTree+tests = testGroup "Parse.Golden" $ [goldenWith CExprC17] ++ mbC23+  where+    mbC23 =+      case runtimeClangVersion of+        ClangVersion x | x >= (15,0,0) -> [goldenWith CExprC23]+        _                              -> []++goldenWith :: TestCStandard -> TestTree+goldenWith testCStd =+    goldenDynamic ("macros-" <> show cStd)+      (datadir </> "macros." <> show cStd <> ".golden")+      (parseMacrosFixture testCStd (datadir </> "macros.h"))+  where+    cStd = testCStandardToCStandard testCStd++{-# NOINLINE datadir #-}+datadir :: FilePath+datadir = unsafePerformIO getDataDir++-- | Minimal golden test using an 'IO' action to resolve the golden file path.+--+-- If the golden file does not yet exist it is created and the test fails so+-- that the developer can inspect and commit it. If it does exist the actual+-- output is compared byte-for-byte; on a mismatch the test fails with a hint+-- about how to regenerate the file.+goldenDynamic ::+     TestName+  -> FilePath           -- ^ path to the golden file+  -> IO LBS.ByteString  -- ^ action producing the actual output+  -> TestTree+goldenDynamic name goldenPath getActual = goldenVsString name goldenPath getActual++{-------------------------------------------------------------------------------+  Run the parser on all macros in the fixture file+-------------------------------------------------------------------------------}++parseMacrosFixture :: TestCStandard -> FilePath -> IO LBS.ByteString+parseMacrosFixture testCStd fixturePath = do+    macroTokens <- collectMacroTokens testCStd fixturePath+    return $ LBS.pack $ unlines $+      map (formatEntry . second (runParser $ parseMacro cStd)) macroTokens+  where+    cStd :: ClangCStandard+    cStd = ClangCStandard (testCStandardToCStandard testCStd) DisableGnu++    formatEntry ::+         Show ann+      => (Text, Either MacroParseError (Macro ann))+      -> String+    formatEntry (name, result) =+        Text.unpack name ++ ": " ++ formatResult result++    formatResult :: Show ann => Either MacroParseError (Macro ann) -> String+    formatResult (Right (Macro{macroExpr})) = "Right " ++ show macroExpr+    formatResult (Left _)                   = "Left <parse error>"++{-------------------------------------------------------------------------------+  Collect macro definitions from a C header file via libclang+-------------------------------------------------------------------------------}++collectMacroTokens ::+     TestCStandard+  -> FilePath+  -> IO [(Text, [Token TokenSpelling])]+collectMacroTokens testCStd path =+    HighLevel.withIndex DontDisplayDiagnostics $ \index ->+      HighLevel.withTranslationUnit index src noArgs [] flags $ \unit -> do+        root    <- clang_getTranslationUnitCursor unit+        HighLevel.clang_visitChildren root (macroFold unit)+  where+    src :: Maybe SourcePath+    src = Just $ SourcePath $ Text.pack path++    noArgs :: ClangArgs+    noArgs = ClangArgs [testCStandardToClangArg testCStd]++    flags :: BitfieldEnum CXTranslationUnit_Flags+    flags = bitfieldEnum [CXTranslationUnit_DetailedPreprocessingRecord]++macroFold ::+     CXTranslationUnit+  -> Fold IO (Text, [Token TokenSpelling])+macroFold unit = simpleFold $ \cursor -> do+    loc    <- clang_getCursorLocation cursor+    inMain <- clang_Location_isFromMainFile loc+    if not inMain+      then foldContinue+      else do+        kind <- fromSimpleEnum <$> clang_getCursorKind cursor+        case kind of+          Right CXCursor_MacroDefinition -> do+              name   <- clang_getCursorSpelling cursor+              range  <- HighLevel.clang_getCursorExtent cursor+              tokens <- HighLevel.clang_tokenize unit (multiLocExpansion <$> range)+              foldContinueWith (name, tokens)+          _ ->+              foldContinue
+ test/Test/CExpr/Parse/Infra.hs view
@@ -0,0 +1,99 @@+-- | Test infrastructure for the c-expr-dsl parser tests+module Test.CExpr.Parse.Infra (+    -- * Token constructors+    kw+  , ident+  , punc+  , lit+    -- * Running parsers+  , checkType+  , checkMacro+  , parseTestWith+    -- * Results+  , tyLit+  ) where++import Data.Nat (Nat (..))+import Data.Text (Text)+import Data.Vec.Lazy (Vec (..))+import Text.Parsec (eof)++import C.Expr.Parse+import C.Expr.Syntax++import Clang.CStandard+import Clang.Enum.Simple+import Clang.HighLevel.Types+import Clang.LowLevel.Core++import Test.CExpr.Util++{-------------------------------------------------------------------------------+  Token constructors+-------------------------------------------------------------------------------}++-- | Construct a keyword token+kw :: Text -> Token TokenSpelling+kw = mkToken CXToken_Keyword++-- | Construct an identifier token+ident :: Text -> Token TokenSpelling+ident = mkToken CXToken_Identifier++-- | Construct a punctuation token+punc :: Text -> Token TokenSpelling+punc = mkToken CXToken_Punctuation++-- | Construct a literal token+lit :: Text -> Token TokenSpelling+lit = mkToken CXToken_Literal++mkToken :: CXTokenKind -> Text -> Token TokenSpelling+mkToken kind spelling = Token{+      tokenKind       = simpleEnum kind+    , tokenSpelling   = TokenSpelling spelling+    , tokenExtent     = Range fakeLoc fakeLoc+    , tokenCursorKind = simpleEnum CXCursor_UnexposedDecl+    }++{-------------------------------------------------------------------------------+  Running parsers+-------------------------------------------------------------------------------}++-- | Run the type parser on a sequence of tokens+--+-- Adds 'eof' so that trailing tokens are rejected as parse failures.+checkType ::+     ClangCStandard+  -> [Token TokenSpelling]+  -> Either MacroParseError (Expr Z (Ps ()))+checkType cStd = runParser (parseMacroType cStd VNil <* eof)++-- | Run the macro parser on a complete token sequence+--+-- The first token must be the macro name (an identifier).  'parseMacro'+-- itself calls 'eof', so no trailing tokens are allowed.+checkMacro ::+     ClangCStandard+  -> [Token TokenSpelling]+  -> Either MacroParseError (Macro ())+checkMacro cStd = runParser (parseMacro cStd)++-- | Run a parser on a list of (kind, spelling) pairs and print the result.+--+-- Useful for interactive debugging in GHCi:+--+-- > parseTestWith (parseMacro C17) [(CXToken_Identifier, "M"), (CXToken_Literal, "1")]+parseTestWith ::+     Show a+  => Parser a+  -> [(CXTokenKind, Text)]+  -> IO ()+parseTestWith p pairs = print $ runParser p (map (uncurry mkToken) pairs)++{-------------------------------------------------------------------------------+  Results+-------------------------------------------------------------------------------}++tyLit :: TypeLit -> Expr ctx (Ps ())+tyLit = Term . Literal . TypeLit
+ test/Test/CExpr/Parse/Literal.hs view
@@ -0,0 +1,385 @@+-- | Unit tests for character and string literal parsing+--+-- These exercise 'C.Expr.Parse.Literal.parseLiteralChar' and+-- 'C.Expr.Parse.Literal.parseLiteralString' through the public macro parser+-- ('C.Expr.Parse.parseMacro'): a @CXToken_Literal@ token whose spelling is the+-- full literal (quotes included) is fed to the parser, and the resulting+-- 'CharLiteral' / 'StringLiteral' is inspected.+--+-- The aim is to cover every kind of character and string literal we accept (and+-- to pin down those we reject).+--+-- References:+--+--  * <https://en.cppreference.com/w/c/language/character_constant>+--  * <https://en.cppreference.com/w/c/language/string_literal>+--  * <https://en.cppreference.com/w/c/language/escape>+module Test.CExpr.Parse.Literal (tests) where++import Data.ByteString (ByteString)+import Data.Either (isLeft)+import Data.Text (Text)+import Data.Text qualified as Text+import Foreign.C (CChar)+import Test.Tasty+import Test.Tasty.HUnit++import C.Expr.Syntax++import Clang.CStandard+import Clang.HighLevel.Types++import Test.CExpr.Parse.Infra++{-------------------------------------------------------------------------------+  Top-level+-------------------------------------------------------------------------------}++tests :: TestTree+tests = testGroup "Parse.Literal" [+      testWithCStd cStd | cStd <- [minBound .. maxBound :: CStandard]+    ]++testWithCStd :: CStandard -> TestTree+testWithCStd cStd = testGroup (show cStd) [+      testGroup "char: ordinary"          $ tests_charOrdinary   std+    , testGroup "char: simple escapes"    $ tests_charEscapes    std+    , testGroup "char: numeric escapes"   $ tests_charNumeric    std+    , testGroup "char: universal names"   $ tests_charUniversal  std+    , testGroup "char: rejected"          $ tests_charRejected   std+    , testGroup "char: digit quirk"       $ tests_charDigitQuirk std+    , testGroup "string: ordinary"        $ tests_strOrdinary    std+    , testGroup "string: simple escapes"  $ tests_strEscapes     std+    , testGroup "string: numeric escapes" $ tests_strNumeric     std+    , testGroup "string: universal names" $ tests_strUniversal   std+    , testGroup "string: embedded NUL"    $ tests_strEmbeddedNul std+    , testGroup "string: rejected"        $ tests_strRejected    std+    , testGroup "prefixes: rejected"      $ tests_prefixes       std+    ]+  where+    std = ClangCStandard cStd DisableGnu++{-------------------------------------------------------------------------------+  Helpers+-------------------------------------------------------------------------------}++-- | A fixed macro name token used in all tests.+macroNameTok :: Token TokenSpelling+macroNameTok = ident "FOO"++-- | Extract a character literal from a parsed object-like macro body.+getCharLit :: Either e (Macro ann) -> Maybe CharLiteral+getCharLit (Right Macro{macroExpr}) = case macroExpr of+    Term (Literal (ValueLit (ValueChar c))) -> Just c+    _                                        -> Nothing+getCharLit _ = Nothing++-- | Extract a string literal from a parsed object-like macro body.+getStrLit :: Either e (Macro ann) -> Maybe StringLiteral+getStrLit (Right Macro{macroExpr}) = case macroExpr of+    Term (Literal (ValueLit (ValueString s))) -> Just s+    _                                          -> Nothing+getStrLit _ = Nothing++-- | Extract an integer value from a parsed object-like macro body.+getIntVal :: Either e (Macro ann) -> Maybe Integer+getIntVal (Right Macro{macroExpr}) = case macroExpr of+    Term (Literal (ValueLit (ValueInt i))) -> Just (integerLiteralValue i)+    _                                       -> Nothing+getIntVal _ = Nothing++-- | A successful character literal: the spelling parses to the given value,+-- and the original source text is preserved.+charCase :: ClangCStandard -> Text -> CChar -> TestTree+charCase cStd spelling val =+    testCase (Text.unpack spelling) $+      getCharLit (checkMacro cStd [macroNameTok, lit spelling])+        @?= Just (CharLiteral val)++-- | A successful string literal: the spelling parses to the given decoded+-- value, and the original source text is preserved.+strCase :: ClangCStandard -> Text -> ByteString -> TestTree+strCase cStd spelling val =+    testCase (Text.unpack spelling) $+      getStrLit (checkMacro cStd [macroNameTok, lit spelling])+        @?= Just (StringLiteral val)++-- | A literal spelling we reject (the whole macro fails to parse).+failCase :: ClangCStandard -> Text -> TestTree+failCase cStd spelling =+    testCase (Text.unpack spelling) $+      assertBool "expected parse failure" $+        isLeft (checkMacro cStd [macroNameTok, lit spelling])++{-------------------------------------------------------------------------------+  Characters: ordinary (unescaped) source characters+-------------------------------------------------------------------------------}++tests_charOrdinary :: ClangCStandard -> [TestTree]+tests_charOrdinary cStd = [+      charCase cStd "'a'" 97+    , charCase cStd "'Z'" 90+    , charCase cStd "' '" 32+      -- NB: a digit character such as @'0'@ is *not* here: it is currently+      -- mis-parsed as an integer literal (see "char: digit quirk" below).+      -- A double quote needs no escaping inside a character literal.+    , charCase cStd "'\"'" 34+    ]++{-------------------------------------------------------------------------------+  Characters: simple (named) escape sequences+-------------------------------------------------------------------------------}++tests_charEscapes :: ClangCStandard -> [TestTree]+tests_charEscapes cStd = [+      -- Basic source escapes.+      charCase cStd "'\\t'"  9    -- '\t'+    , charCase cStd "'\\v'"  11   -- '\v'+    , charCase cStd "'\\f'"  12   -- '\f'+    , charCase cStd "'\\''"  39   -- '\''+    , charCase cStd "'\\\"'" 34   -- '"'+    , charCase cStd "'\\?'"  63   -- '?'+    , charCase cStd "'\\\\'" 92   -- '\\'+      -- Execution escapes.+    , charCase cStd "'\\0'"  0    -- '\NUL' (octal escape; also in "char: numeric escapes")+    , charCase cStd "'\\a'"  7    -- '\a'+    , charCase cStd "'\\b'"  8    -- '\b'+    , charCase cStd "'\\n'"  10   -- '\n'+    , charCase cStd "'\\r'"  13   -- '\r'+    ]++{-------------------------------------------------------------------------------+  Characters: numeric (octal / hex) escape sequences+-------------------------------------------------------------------------------}++tests_charNumeric :: ClangCStandard -> [TestTree]+tests_charNumeric cStd = [+      -- Octal: \123 == 0o123 == 83 == 'S'.+      charCase cStd "'\\123'" 83+      -- Octal terminates at three digits / first non-octal digit.+    , charCase cStd "'\\0'"   0+      -- Octal at the single-byte boundary: \377 == 255.+    , charCase cStd "'\\377'" 255+      -- Hex: \x53 == 83 == 'S'.+    , charCase cStd "'\\x53'" 83+      -- Hex at the single-byte boundary: \xFF == 255.+    , charCase cStd "'\\xFF'" 255+    ]++{-------------------------------------------------------------------------------+  Characters: universal character names+-------------------------------------------------------------------------------}++tests_charUniversal :: ClangCStandard -> [TestTree]+tests_charUniversal cStd = [+      -- 4-digit \u form: code point > 0xFF, rejected.+      failCase cStd "'\\u3042'"      -- 'あ' (U+3042)+      -- 8-digit \U form outside the BMP, rejected.+    , failCase cStd "'\\U0001F600'" -- '😀' (U+1F600)+      -- The three basic characters explicitly allowed as universal names;+      -- their code points fit in a byte.+    , charCase cStd "'\\u0024'" 36  -- '$'+    , charCase cStd "'\\u0040'" 64  -- '@'+    , charCase cStd "'\\u0060'" 96  -- '`'+    ]++{-------------------------------------------------------------------------------+  Characters: rejected+-------------------------------------------------------------------------------}++tests_charRejected :: ClangCStandard -> [TestTree]+tests_charRejected cStd = [+      -- Multi-character constants have an implementation-defined value.+      failCase cStd "'ab'"+      -- A sequence of single-byte numeric escapes is still multi-character.+    , failCase cStd "'\\xE3\\x81\\x82'"+      -- Numeric escapes that do not fit in a single byte.+    , failCase cStd "'\\777'"   -- octal 511+    , failCase cStd "'\\xABC'"  -- hex 0xABC+      -- A raw multi-byte source character whose code point exceeds a byte.+    , failCase cStd "'\12354'"  -- 'あ' (U+3042)+      -- NB: the empty character literal @''@ is *not* rejected here: it is+      -- currently mis-parsed as the integer 0 (see "char: digit quirk" below).+      -- Universal names may not denote basic characters...+    , failCase cStd "'\\u0041'" -- 'A'+      -- ...nor surrogate code points.+    , failCase cStd "'\\uD800'"+      -- Unknown escape letters are not valid in standard C.+    , failCase cStd "'\\j'"    -- unrecognised escape+    , failCase cStd "'\\e'"    -- GCC extension for ESC, not standard C+      -- \x with no following hex digit is malformed.+    , failCase cStd "'\\x'"+      -- The digits 8 and 9 are not valid octal digits; \8 and \9 are not+      -- named escapes either.+    , failCase cStd "'\\8'"+    , failCase cStd "'\\9'"+      -- \u requires exactly 4 hex digits; \U requires exactly 8.+    , failCase cStd "'\\u004'"     -- only 3 digits+    , failCase cStd "'\\U01F600'"  -- only 6 digits+      -- UCN control characters below U+00A0 (other than U+0024/0040/0060) are+      -- forbidden.+    , failCase cStd "'\\u0001'"+    ]++-- TODO <https://github.com/well-typed/c-expr/issues/28>+--+-- Characters: digit quirk (known parser limitation/bug)+--+-- A character literal whose content looks like a number is currently *not*+-- parsed as a character at all: it is swallowed by the integer-literal parser.+-- Two things conspire:+--+--  * 'C.Expr.Parse.Literal.digitInBase' accepts the single quote @'@ as a C+--    digit separator in *any* position (including leading and trailing),+--    whereas C only permits separators *between* digits.+--  * In 'C.Expr.Parse.Expr' the integer alternative is tried before the+--    character alternative, so a @CXToken_Literal@ spelled @'<digits>'@ is+--    consumed by the integer parser, the surrounding quotes treated as+--    separators.+--+-- As a result @'0'@ yields the integer 0 (not the character whose value is 48),+-- and invalid forms such as @''@, @'12'@ and @'1'2'@ parse successfully instead+-- of being rejected.+--+-- These tests pin the current (incorrect) behaviour so that a future fix is+-- forced to revisit them; the expectations below should then move into+-- 'tests_charOrdinary' / 'tests_charRejected'.+tests_charDigitQuirk :: ClangCStandard -> [TestTree]+tests_charDigitQuirk cStd = [+      -- Should be the character '0' (value 48); currently the integer 0.+      quirk "'0'"   0+      -- Should be the character '5' (value 53); currently the integer 5.+    , quirk "'5'"   5+      -- Should be rejected (multi-character); currently the integer 12.+    , quirk "'12'"  12+      -- Should be rejected (garbage); currently the integer 12.+    , quirk "'1'2'" 12+      -- Should be rejected (empty); currently the integer 0.+    , quirk "''"    0+    ]+  where+    quirk :: Text -> Integer -> TestTree+    quirk spelling val =+      testCase (Text.unpack spelling) $+        getIntVal (checkMacro cStd [macroNameTok, lit spelling]) @?= Just val++{-------------------------------------------------------------------------------+  Strings: ordinary (unescaped) source characters+-------------------------------------------------------------------------------}++tests_strOrdinary :: ClangCStandard -> [TestTree]+tests_strOrdinary cStd = [+      strCase cStd "\"a\""           "a"+    , strCase cStd "\"abc\""         "abc"+    , strCase cStd "\"hello world\"" "hello world"+      -- The empty string is a valid (zero-length) literal.+    , strCase cStd "\"\""            ""+      -- A single quote needs no escaping inside a string literal.+    , strCase cStd "\"'\""           "'"+      -- A raw multi-byte source character decodes to that Unicode code point.+    , strCase cStd "\"\12354\""      "\xE3\x81\x82"  -- "あ" (U+3042, UTF-8)+    ]++{-------------------------------------------------------------------------------+  Strings: simple (named) escape sequences+-------------------------------------------------------------------------------}++tests_strEscapes :: ClangCStandard -> [TestTree]+tests_strEscapes cStd = [+      strCase cStd "\"\\t\""  "\t"+    , strCase cStd "\"\\n\""  "\n"+    , strCase cStd "\"\\r\""  "\r"+    , strCase cStd "\"\\v\""  "\v"+    , strCase cStd "\"\\f\""  "\f"+    , strCase cStd "\"\\a\""  "\a"   -- BEL (0x07)+    , strCase cStd "\"\\b\""  "\b"   -- BS  (0x08)+    , strCase cStd "\"\\'\""  "'"+    , strCase cStd "\"\\\"\"" "\""+    , strCase cStd "\"\\?\""  "?"+    , strCase cStd "\"\\\\\"" "\\"+    ]++{-------------------------------------------------------------------------------+  Strings: numeric (octal / hex) escape sequences+-------------------------------------------------------------------------------}++tests_strNumeric :: ClangCStandard -> [TestTree]+tests_strNumeric cStd = [+      -- Octal / hex single bytes.+      strCase cStd "\"\\123\"" "S"  -- 0x53+    , strCase cStd "\"\\x53\"" "S"+      -- A run of single-byte numeric escapes (all < 0x80, valid UTF-8).+    , strCase cStd "\"\\1\\2\\3\\4\\5\\6\"" "\1\2\3\4\5\6"+      -- Hex escapes of UTF-8 bytes: together they decode to one code point.+    , strCase cStd "\"\\xE3\\x81\\x82\"" "\xE3\x81\x82"  -- "あ" (U+3042, UTF-8)+      -- \777 == 0o777 == 0x01FF: two raw bytes [0x01, 0xFF]. These are not+      -- valid UTF-8, but ByteString accepts arbitrary bytes.+    , strCase cStd "\"\\777\"" "\x01\xFF"+      -- Zero-value numeric escapes must each produce a single null byte.+    , strCase cStd "\"\\0\""   "\NUL"    -- single-digit octal zero+    , strCase cStd "\"\\00\""  "\NUL"    -- two-digit octal zero+    , strCase cStd "\"\\000\"" "\NUL"    -- three-digit octal zero+    , strCase cStd "\"\\x0\""  "\NUL"    -- single-digit hex zero+    , strCase cStd "\"\\x00\"" "\NUL"    -- two-digit hex zero+      -- An oversized hex escape contributes its value as big-endian bytes.+      -- \xABC == 0xABC == 2748, big-endian: [0x0A, 0xBC].+    , strCase cStd "\"\\xABC\"" "\x0A\xBC"+    ]++{-------------------------------------------------------------------------------+  Strings: universal character names+-------------------------------------------------------------------------------}++tests_strUniversal :: ClangCStandard -> [TestTree]+tests_strUniversal cStd = [+      -- Universal names decode to their Unicode code point (UTF-8 encoded).+      strCase cStd "\"\\u3042\""     "\xE3\x81\x82"        -- "あ" (U+3042)+    , strCase cStd "\"\\U0001F600\"" "\xF0\x9F\x98\x80"    -- "😀" (U+1F600)+      -- Same basic-character / surrogate restrictions as character literals.+    , failCase cStd "\"\\u0041\""    -- 'A'+    , failCase cStd "\"\\uD800\""    -- surrogate+    ]++{-------------------------------------------------------------------------------+  Strings: rejected+-------------------------------------------------------------------------------}++tests_strRejected :: ClangCStandard -> [TestTree]+tests_strRejected cStd = [+      -- Unknown escape letters are not valid in standard C.+      failCase cStd "\"\\j\""+    , failCase cStd "\"\\e\""   -- GCC extension for ESC, not standard C+      -- \x with no following hex digit is malformed.+    , failCase cStd "\"\\x\""+      -- UCN control characters below U+00A0 (other than U+0024/0040/0060) are+      -- forbidden.+    , failCase cStd "\"\\u0001\""+    ]++{-------------------------------------------------------------------------------+  Strings: embedded NUL bytes+-------------------------------------------------------------------------------}++tests_strEmbeddedNul :: ClangCStandard -> [TestTree]+tests_strEmbeddedNul cStd = [+      strCase cStd "\"hij\\0\""       "hij\NUL"+    , strCase cStd "\"abc\\0def\\0g\"" "abc\NULdef\NULg"+    ]++{-------------------------------------------------------------------------------+  Prefixes: currently unsupported (rejected) for both characters and strings+-------------------------------------------------------------------------------}++tests_prefixes :: ClangCStandard -> [TestTree]+tests_prefixes cStd = [+      -- Character literal prefixes.+      failCase cStd "L'a'"+    , failCase cStd "u'a'"+    , failCase cStd "U'a'"+    , failCase cStd "u8'a'"+      -- String literal prefixes.+    , failCase cStd "L\"a\""+    , failCase cStd "u\"a\""+    , failCase cStd "U\"a\""+    , failCase cStd "u8\"a\""+    ]
+ test/Test/CExpr/Parse/Macro.hs view
@@ -0,0 +1,255 @@+{-# LANGUAGE CPP #-}++#if __GLASGOW_HASKELL__ >=908+{-# LANGUAGE TypeAbstractions #-}+#endif++-- | Unit tests for 'C.Expr.Parse.Expr.parseMacro'+--+-- Tests the full macro parser, focusing on:+--+-- * Type bodies vs expression bodies (disambiguation)+-- * Object-like and function-like expression macros+module Test.CExpr.Parse.Macro (tests) where++import Data.Either (isLeft, isRight)+import Data.Nat (Nat (..))+import Data.Type.Equality ((:~:) (..))+import Data.Type.Nat qualified as Nat+import Data.Vec.Lazy (Vec (..))+import Data.Vec.Lazy qualified as Vec+import DeBruijn (Idx (..))+import Test.Tasty+import Test.Tasty.HUnit++import C.Expr.Syntax++import Clang.CStandard+import Clang.HighLevel.Types++import Test.CExpr.Parse.Infra+import Test.CExpr.Typecheck.Infra (mtagged, mvar)++{-------------------------------------------------------------------------------+  Top-level+-------------------------------------------------------------------------------}++tests :: TestTree+tests = testGroup "Parse.Macro" [+      testsWithCStd cStd | cStd <- [minBound .. maxBound :: CStandard]+    ]++testsWithCStd :: CStandard -> TestTree+testsWithCStd cStd = testGroup (show cStd) [+      testGroup "type bodies"               $ tests_typeBody         std+    , testGroup "function-like type bodies" $ tests_funcLikeTypeBody std+    , testGroup "expression bodies"         $ tests_exprBody         std+    , testGroup "disambiguation"            $ tests_disambiguation   std+    ]+  where+    std = ClangCStandard cStd DisableGnu++{-------------------------------------------------------------------------------+  Helpers+-------------------------------------------------------------------------------}++-- | A fixed macro name token used in all tests+macroNameTok :: Token TokenSpelling+macroNameTok = ident "FOO"++-- | True when the macro expression looks like a type: it has an 'Type' or+-- 'TyApp' at its core (bare identifier cases are intentionally excluded+-- because a bare name is structurally identical in both type and expression+-- position after the refactor).+isTypeBody :: Either e (Macro ann) -> Bool+isTypeBody (Right Macro{macroExpr}) = case macroExpr of+    Term (Literal (TypeLit _)) -> True+    TyApp {}       -> True+    _               -> False+isTypeBody _ = False++-- | True when the macro expression is unambiguously an expression (a literal+-- or an operator application), not a type.+isExprBody :: Either e (Macro ann) -> Bool+isExprBody (Right Macro{macroExpr}) = case macroExpr of+    Term (Literal (ValueLit (ValueInt _)))    -> True+    Term (Literal (ValueLit (ValueFloat _)))  -> True+    Term (Literal (ValueLit (ValueChar _)))   -> True+    Term (Literal (ValueLit (ValueString _))) -> True+    VaApp {}         -> True+    _                 -> False+isExprBody _ = False++getMacroExpr ::+     forall e ctx ann. Nat.SNatI ctx+  => Either e (Macro ann)+  -> Maybe (Expr ctx (Ps ann))+getMacroExpr (Right (Macro @_ @ctx1 _ _ macroParams macroExpr)) =+    Vec.withDict macroParams $+      case Nat.eqNat @ctx @ctx1 of+        Just Refl -> Just macroExpr+        Nothing   -> Nothing+getMacroExpr _ =+    Nothing++-- | Extract the expression body from an object-like (0-arg) macro.+getObjExpr :: forall e ann. Either e (Macro ann) -> Maybe (Expr Z (Ps ann))+getObjExpr = getMacroExpr++-- | Extract the expression body from a function-like macro with one parameter.+getFn1Expr :: forall e ann. Either e (Macro ann) -> Maybe (Expr (S Z) (Ps ann))+getFn1Expr = getMacroExpr++{-------------------------------------------------------------------------------+  Type bodies+-------------------------------------------------------------------------------}++tests_typeBody :: ClangCStandard -> [TestTree]+tests_typeBody cStd = [+      testCase "int" $+        -- #define FOO int+        getObjExpr (checkMacro cStd [macroNameTok, kw "int"])+          @?= Just (tyLit (TypeInt Nothing (Just SizeInt)))+    , testCase "unsigned long" $+        -- #define FOO unsigned long+        getObjExpr (checkMacro cStd [macroNameTok, kw "unsigned", kw "long"])+          @?= Just (tyLit (TypeInt (Just Unsigned) (Just SizeLong)))+    , testCase "const int*" $+        -- #define FOO const int *+        getObjExpr (checkMacro cStd [macroNameTok, kw "const", kw "int", punc "*"])+          @?= Just (TyApp Pointer (TyApp Const (tyLit (TypeInt Nothing (Just SizeInt)) ::: VNil) ::: VNil))+    , testCase "void*" $+        -- #define FOO void *+        getObjExpr (checkMacro cStd [macroNameTok, kw "void", punc "*"])+          @?= Just (TyApp Pointer (tyLit TypeVoid ::: VNil))+    , testCase "struct Foo" $+        -- #define FOO struct Foo+        getObjExpr (checkMacro cStd [macroNameTok, kw "struct", ident "Foo"])+          @?= Just (mtagged "Foo" TagStruct)+    , testCase "size_t" $+        -- #define FOO size_t (bare identifier; typechecker decides it's a type)+        getObjExpr (checkMacro cStd [macroNameTok, ident "size_t"])+          @?= Just (mvar "size_t")+    , testCase "_Bool" $+        -- #define FOO _Bool+        getObjExpr (checkMacro cStd [macroNameTok, kw "_Bool"])+          @?= Just (tyLit TypeBool)+    , testCase "_Bool" $+        -- #define FOO size_t const * const+        getObjExpr (checkMacro cStd [macroNameTok, ident "size_t", kw "const", punc "*", kw "const" ])+          @?= Just (TyApp Const (TyApp Pointer (TyApp Const (mvar "size_t" ::: VNil) ::: VNil) ::: VNil))+    ]++{-------------------------------------------------------------------------------+  Function-like type bodies (local args)+-------------------------------------------------------------------------------}++tests_funcLikeTypeBody :: ClangCStandard -> [TestTree]+tests_funcLikeTypeBody cStd = [+      testCase "PTR(T) = T*" $+        -- #define PTR(T) T*+        -- T is a local arg; the body is a pointer type parameterised by T.+        getFn1Expr (checkMacro cStd+            [ macroNameTok, punc "(", ident "T", punc ")"+            , ident "T", punc "*"+            ])+          @?= Just (TyApp Pointer (Term (LocalParam IZ) ::: VNil))+    , testCase "CONST_PTR(T) = const T*" $+        -- #define CONST_PTR(T) const T*+        getFn1Expr (checkMacro cStd+            [ macroNameTok, punc "(", ident "T", punc ")"+            , kw "const", ident "T", punc "*"+            ])+          @?= Just (TyApp Pointer (TyApp Const (Term (LocalParam IZ) ::: VNil) ::: VNil))+    , testCase "free var is not a local arg" $+        -- #define PTR(T) size_t*+        -- size_t is not a formal parameter, so it stays as Var, not LocalParam.+        getFn1Expr (checkMacro cStd+            [ macroNameTok, punc "(", ident "T", punc ")"+            , ident "size_t", punc "*"+            ])+          @?= Just (TyApp Pointer (mvar "size_t" ::: VNil))+    ]++{-------------------------------------------------------------------------------+  Expression bodies+-------------------------------------------------------------------------------}++tests_exprBody :: ClangCStandard -> [TestTree]+tests_exprBody cStd = [+      -- Object-like macros+      testCase "integer literal" $+        -- #define FOO 42+        assertBool "expected expression body" $+          isExprBody (checkMacro cStd [macroNameTok, lit "42"])+    , testCase "negative literal" $+        -- #define FOO -1+        assertBool "expected expression body" $+          isExprBody (checkMacro cStd [macroNameTok, punc "-", lit "1"])+    , testCase "arithmetic expression" $+        -- #define FOO 1 + 2+        assertBool "expected expression body" $+          isExprBody (checkMacro cStd [macroNameTok, lit "1", punc "+", lit "2"])+      -- Function-like macros+      -- A bare identifier body (e.g. x) is structurally identical for type and+      -- expression positions after the Expr unification; we just check it parses.+    , testCase "identity function" $+        -- #define FOO(x) x+        assertBool "expected parse success" $+          isRight $+            checkMacro cStd [+                macroNameTok, punc "(", ident "x", punc ")"+              , ident "x"+              ]+    , testCase "two-argument function" $+        -- #define FOO(a, b) a + b+        assertBool "expected expression body" $+          isExprBody $+            checkMacro cStd [+                macroNameTok+              , punc "(", ident "a", punc ",", ident "b", punc ")"+              , ident "a", punc "+", ident "b"+              ]+      -- Zero-argument function-like macro (#define FOO() 0) is+      -- parsed as objectLike since empty parens are not valid formalArgs;+      -- the result is still an expression body+    ]++{-------------------------------------------------------------------------------+  Disambiguation: types vs. expressions+-------------------------------------------------------------------------------}++tests_disambiguation :: ClangCStandard -> [TestTree]+tests_disambiguation cStd = [+      -- A bare identifier like 'size_t' is now structurally identical whether+      -- it came from the type parser or the expression parser (both produce+      -- Term (Var ...)).  We just verify that parsing succeeds.+      testCase "bare name parses successfully" $+        -- #define FOO size_t+        assertBool "expected parse success" $+          isRight (checkMacro cStd [macroNameTok, ident "size_t"])+    , testCase "void is a type body, not an identifier expression" $+        -- #define FOO void+        assertBool "expected type body" $+          isTypeBody (checkMacro cStd [macroNameTok, kw "void"])+      -- An integer literal cannot be a type, so it falls through to expression.+    , testCase "literal falls through to expression" $+        -- #define FOO 0+        assertBool "expected expression body" $+          isExprBody (checkMacro cStd [macroNameTok, lit "0"])+      -- An expression that starts with parenthesised identifiers could look+      -- like formal arguments.+    , testCase "parenthesised expression is not a type" $+        -- #define FOO (1)+        assertBool "expected expression body" $+          isExprBody (checkMacro cStd [macroNameTok, punc "(", lit "1", punc ")"])+      -- Completely unparseable input+    , testCase "bare comma fails" $+        -- #define FOO ,+        assertBool "expected failure" $+          isLeft (checkMacro cStd [macroNameTok, punc ","])+    , testCase "empty body fails" $+        -- #define FOO+        assertBool "expected failure" $+          isLeft (checkMacro cStd [macroNameTok])+    ]
+ test/Test/CExpr/Parse/Type.hs view
@@ -0,0 +1,348 @@+-- | Unit tests for 'C.Expr.Parse.Type.parseMacroType'+module Test.CExpr.Parse.Type (tests) where++import Data.Either (isLeft)+import Data.Vec.Lazy (Vec (..))+import Test.Tasty+import Test.Tasty.HUnit++import C.Expr.Syntax++import Clang.CStandard++import Test.CExpr.Parse.Infra+import Test.CExpr.Typecheck.Infra (mtagged, mvar)++{-------------------------------------------------------------------------------+  Top-level+-------------------------------------------------------------------------------}++tests :: TestTree+tests = testGroup "Parse.Type" [+      testWithCStd cStd | cStd <- [minBound .. maxBound :: CStandard]+    ]++testWithCStd :: CStandard -> TestTree+testWithCStd cStd = testGroup (show cStd) [+      testGroup "void and bool"       $ tests_voidBool     std+    , testGroup "integer types"       $ tests_int          std+    , testGroup "char"                $ tests_char         std+    , testGroup "float and double"    $ tests_float        std+    , testGroup "named types"         $ tests_named        std+    , testGroup "tagged types"        $ tests_tagged       std+    , testGroup "const qualifier"     $ tests_const        std+    , testGroup "pointer indirection" $ tests_pointer      std+    , testGroup "combined"            $ tests_combined     std+    , testGroup "keyword order"       $ tests_keywordOrder std+    , testGroup "failures"            $ tests_failures     std+    ]+  where+    std = ClangCStandard cStd DisableGnu++{-------------------------------------------------------------------------------+  void and bool+-------------------------------------------------------------------------------}++tests_voidBool :: ClangCStandard -> [TestTree]+tests_voidBool cStd = [+      testCase "void" $+        -- void+        checkType cStd [kw "void"]+          @?= Right (tyLit TypeVoid)+    , testCase "_Bool" $+        -- _Bool+        checkType cStd [kw "_Bool"]+          @?= Right (tyLit TypeBool)+      -- 'bool' as CXToken_Keyword (Clang >= 16)+    , testCase "bool (keyword)" $+        -- bool+        let res = checkType cStd [kw "bool"]+        in  case cStd of+              ClangCStandard std _ | std >= C23 ->+                res @?= Right (tyLit TypeBool)+              _ ->+                assertBool "bool not a kw" $ isLeft res+      -- 'bool' as CXToken_Identifier (older Clang): treated as a named type+    , testCase "bool (identifier)" $+        -- bool+        checkType cStd [ident "bool"]+          @?= Right (mvar "bool")+    ]++{-------------------------------------------------------------------------------+  Integer types+-------------------------------------------------------------------------------}++tests_int :: ClangCStandard -> [TestTree]+tests_int cStd = [+      testCase "int" $+        -- int+        checkType cStd  [kw "int"]+          @?= Right (tyLit (TypeInt Nothing (Just SizeInt)))+    , testCase "signed" $+        -- signed+        checkType cStd [kw "signed"]+          @?= Right (tyLit (TypeInt (Just Signed) Nothing))+    , testCase "unsigned" $+        -- unsigned+        checkType cStd [kw "unsigned"]+          @?= Right (tyLit (TypeInt (Just Unsigned) Nothing))+    , testCase "short" $+        -- short+        checkType cStd [kw "short"]+          @?= Right (tyLit (TypeInt Nothing (Just SizeShort)))+    , testCase "long" $+        -- long+        checkType cStd [kw "long"]+          @?= Right (tyLit (TypeInt Nothing (Just SizeLong)))+    , testCase "long long" $+        -- long long+        checkType cStd [kw "long", kw "long"]+          @?= Right (tyLit (TypeInt Nothing (Just SizeLongLong)))+    , testCase "unsigned int" $+        -- unsigned int+        checkType cStd [kw "unsigned", kw "int"]+          @?= Right (tyLit (TypeInt (Just Unsigned) (Just SizeInt)))+    , testCase "signed int" $+        -- signed int+        checkType cStd [kw "signed", kw "int"]+          @?= Right (tyLit (TypeInt (Just Signed) (Just SizeInt)))+    , testCase "unsigned short" $+        -- unsigned short+        checkType cStd [kw "unsigned", kw "short"]+          @?= Right (tyLit (TypeInt (Just Unsigned) (Just SizeShort)))+    , testCase "unsigned long" $+        -- unsigned long+        checkType cStd [kw "unsigned", kw "long"]+          @?= Right (tyLit (TypeInt (Just Unsigned) (Just SizeLong)))+    , testCase "unsigned long long" $+        -- unsigned long long+        checkType cStd [kw "unsigned", kw "long", kw "long"]+          @?= Right (tyLit (TypeInt (Just Unsigned) (Just SizeLongLong)))+    , testCase "long long int" $+        -- long long int+        checkType cStd [kw "long", kw "long", kw "int"]+          @?= Right (tyLit (TypeInt Nothing (Just SizeLongLong)))+    ]++{-------------------------------------------------------------------------------+  Char+-------------------------------------------------------------------------------}++tests_char :: ClangCStandard -> [TestTree]+tests_char cStd = [+      testCase "char" $+        -- char+        checkType cStd [kw "char"]+          @?= Right (tyLit (TypeChar Nothing))+    , testCase "signed char" $+        -- signed char+        checkType cStd [kw "signed", kw "char"]+          @?= Right (tyLit (TypeChar (Just Signed)))+    , testCase "unsigned char" $+        -- unsigned char+        checkType cStd [kw "unsigned", kw "char"]+          @?= Right (tyLit (TypeChar (Just Unsigned)))+    ]++{-------------------------------------------------------------------------------+  Float and double+-------------------------------------------------------------------------------}++tests_float :: ClangCStandard -> [TestTree]+tests_float cStd = [+      testCase "float" $+        -- float+        checkType cStd [kw "float"]+          @?= Right (tyLit (TypeFloat SizeFloat))+    , testCase "double" $+        -- double+        checkType cStd [kw "double"]+          @?= Right (tyLit (TypeFloat SizeDouble))+    ]++{-------------------------------------------------------------------------------+  Named types (identifiers)+-------------------------------------------------------------------------------}++-- After parsing, we cannot tell if these are types or value expressions.+-- However, they are parsed by the type branch of the parser ('parseMacroType').++tests_named :: ClangCStandard -> [TestTree]+tests_named cStd = [+      testCase "size_t" $+        -- size_t+        checkType cStd [ident "size_t"]+          @?= Right (mvar "size_t")+    , testCase "uint32_t" $+        -- uint32_t+        checkType cStd [ident "uint32_t"]+          @?= Right (mvar "uint32_t")+      -- An identifier token spelled "int" is treated as a named type,+      -- not as the built-in int keyword (libclang always tokenizes keywords+      -- as CXToken_Keyword, so this case is mainly for documentation)+    , testCase "int as identifier" $+        -- int  (tokenised as CXToken_Identifier, not CXToken_Keyword)+        checkType cStd [ident "int"]+          @?= Right (mvar "int")+    ]++{-------------------------------------------------------------------------------+  Tagged types+-------------------------------------------------------------------------------}++tests_tagged :: ClangCStandard -> [TestTree]+tests_tagged cStd = [+      testCase "struct Foo" $+        -- struct Foo+        checkType cStd [kw "struct", ident "Foo"]+          @?= Right (mtagged "Foo" TagStruct)+    , testCase "union Bar" $+        -- union Bar+        checkType cStd [kw "union", ident "Bar"]+          @?= Right (mtagged "Bar" TagUnion)+    , testCase "enum Baz" $+        -- enum Baz+        checkType cStd [kw "enum", ident "Baz"]+          @?= Right (mtagged "Baz" TagEnum)+    ]++{-------------------------------------------------------------------------------+  Const qualifier+-------------------------------------------------------------------------------}++tests_const :: ClangCStandard -> [TestTree]+tests_const cStd = [+      testCase "const int (leading)" $+        -- const int+        checkType cStd [kw "const", kw "int"]+          @?= Right (TyApp Const (tyLit (TypeInt Nothing (Just SizeInt)) ::: VNil))+    , testCase "int const (trailing)" $+        -- int const+        checkType cStd [kw "int", kw "const"]+          @?= Right (TyApp Const (tyLit (TypeInt Nothing (Just SizeInt)) ::: VNil))+    , testCase "const void" $+        -- const void+        checkType cStd [kw "const", kw "void"]+          @?= Right (TyApp Const (tyLit TypeVoid ::: VNil))+    , testCase "const size_t" $+        -- const size_t+        checkType cStd [kw "const", ident "size_t"]+          @?= Right (TyApp Const (mvar "size_t" ::: VNil))+    , testCase "const struct Foo" $+        -- const struct Foo+        checkType cStd [kw "const", kw "struct", ident "Foo"]+          @?= Right (TyApp Const (mtagged "Foo" TagStruct ::: VNil))+    ]++{-------------------------------------------------------------------------------+  Pointer indirection+-------------------------------------------------------------------------------}++tests_pointer :: ClangCStandard -> [TestTree]+tests_pointer cStd = [+      testCase "int*" $+        -- int *+        checkType cStd [kw "int", punc "*"]+          @?= Right (TyApp Pointer (tyLit (TypeInt Nothing (Just SizeInt)) ::: VNil))+    , testCase "int**" $+        -- int **+        checkType cStd [kw "int", punc "*", punc "*"]+          @?= Right (TyApp Pointer (TyApp Pointer (tyLit (TypeInt Nothing (Just SizeInt)) ::: VNil) ::: VNil))+    , testCase "void*" $+        -- void *+        checkType cStd [kw "void", punc "*"]+          @?= Right (TyApp Pointer (tyLit TypeVoid ::: VNil))+    , testCase "size_t*" $+        -- size_t *+        checkType cStd [ident "size_t", punc "*"]+          @?= Right (TyApp Pointer (mvar "size_t" ::: VNil))+    , testCase "struct Foo*" $+        -- struct Foo *+        checkType cStd [kw "struct", ident "Foo", punc "*"]+          @?= Right (TyApp Pointer (mtagged "Foo" TagStruct ::: VNil))+    ]++{-------------------------------------------------------------------------------+  Combined complex types+-------------------------------------------------------------------------------}++tests_combined :: ClangCStandard -> [TestTree]+tests_combined cStd = [+      testCase "const int * (pointer to const int, const left-hand side)" $+        checkType cStd [kw "const", kw "int", punc "*"]+          @?= Right (TyApp Pointer (TyApp Const (tyLit (TypeInt Nothing (Just SizeInt)) ::: VNil) ::: VNil))+    , testCase "int const * (pointer to const int, const right-hand side)" $+        checkType cStd [kw "int", kw "const", punc "*"]+          @?= Right (TyApp Pointer (TyApp Const (tyLit (TypeInt Nothing (Just SizeInt)) ::: VNil) ::: VNil))+    , testCase "int * const (const pointer to int)" $+        checkType cStd [kw "int", punc "*", kw "const"]+          @?= Right (TyApp Const (TyApp Pointer (tyLit (TypeInt Nothing (Just SizeInt)) ::: VNil) ::: VNil))+    , testCase "const int * const (const pointer to const int, const left-hand side)" $+        checkType cStd [kw "const", kw "int", punc "*", kw "const"]+          @?= Right (TyApp Const (TyApp Pointer (TyApp Const (tyLit (TypeInt Nothing (Just SizeInt)) ::: VNil) ::: VNil) ::: VNil))+    , testCase "int const * const (const pointer to const int, const right-hand side)" $+        checkType cStd [kw "int", kw "const", punc "*", kw "const"]+          @?= Right (TyApp Const (TyApp Pointer (TyApp Const (tyLit (TypeInt Nothing (Just SizeInt)) ::: VNil) ::: VNil) ::: VNil))+    , testCase "const unsigned long*" $+        -- const unsigned long *+        checkType cStd [kw "const", kw "unsigned", kw "long", punc "*"]+          @?= Right (TyApp Pointer (TyApp Const (tyLit (TypeInt (Just Unsigned) (Just SizeLong)) ::: VNil) ::: VNil))+    , testCase "const struct Foo**" $+        -- const struct Foo **+        checkType cStd [kw "const", kw "struct", ident "Foo", punc "*", punc "*"]+          @?= Right (TyApp Pointer (TyApp Pointer (TyApp Const (mtagged "Foo" TagStruct ::: VNil) ::: VNil) ::: VNil))+    , testCase "unsigned long long int" $+        -- unsigned long long int+        checkType cStd [kw "unsigned", kw "long", kw "long", kw "int"]+          @?= Right (tyLit (TypeInt (Just Unsigned) (Just SizeLongLong)))+    ]++{-------------------------------------------------------------------------------+  Keyword order independence+-------------------------------------------------------------------------------}++tests_keywordOrder :: ClangCStandard -> [TestTree]+tests_keywordOrder cStd = [+      -- C allows type specifier keywords in any order+      testCase "long unsigned == unsigned long" $+        checkType cStd [kw "long", kw "unsigned"]+          @?= checkType cStd [kw "unsigned", kw "long"]+    , testCase "int unsigned == unsigned int" $+        checkType cStd [kw "int", kw "unsigned"]+          @?= checkType cStd [kw "unsigned", kw "int"]+    , testCase "int long unsigned == unsigned long int" $+        checkType cStd [kw "int", kw "long", kw "unsigned"]+          @?= checkType cStd [kw "unsigned", kw "long", kw "int"]+    ]++{-------------------------------------------------------------------------------+  Failure cases+-------------------------------------------------------------------------------}++tests_failures :: ClangCStandard -> [TestTree]+tests_failures cStd = [+      testCase "bare punctuation" $+        -- *  (no preceding type specifier)+        assertBool "expected failure" $ isLeft (checkType cStd [punc "*"])+    , testCase "struct without name" $+        -- struct  (tag keyword not followed by a name)+        assertBool "expected failure" $ isLeft (checkType cStd [kw "struct"])+    , testCase "void void" $+        -- void void  (duplicate specifier)+        assertBool "expected failure" $ isLeft (checkType cStd [kw "void", kw "void"])+    , testCase "float double" $+        -- float double  (conflicting float specifiers)+        assertBool "expected failure" $ isLeft (checkType cStd [kw "float", kw "double"])+    , testCase "int char" $+        -- int char  (conflicting specifiers)+        assertBool "expected failure" $ isLeft (checkType cStd [kw "int", kw "char"])+    , testCase "literal token" $+        -- 42  (integer literal is not a type token)+        assertBool "expected failure" $ isLeft (checkType cStd [lit "42"])+    , testCase "trailing tokens rejected" $+        -- int * extra  (parseMacroType alone would succeed on [int, *], but+        -- checkType adds eof so the trailing identifier causes failure)+        assertBool "expected failure" $+          isLeft (checkType cStd [kw "int", punc "*", ident "extra"])+    ]
+ test/Test/CExpr/Typecheck.hs view
@@ -0,0 +1,12 @@+module Test.CExpr.Typecheck (+    tests+  ) where++import Test.Tasty++import Test.CExpr.Typecheck.Classify qualified as Classify++tests :: TestTree+tests = testGroup "typecheck" [+      Classify.tests+    ]
+ test/Test/CExpr/Typecheck/Classify.hs view
@@ -0,0 +1,157 @@+module Test.CExpr.Typecheck.Classify (+    tests+  ) where++import Data.Map qualified as Map+import Data.Maybe+import Data.Vec.Lazy (Vec (..))+import DeBruijn (Idx (..), pattern I1)+import Test.Tasty+import Test.Tasty.HUnit++import C.Expr.Syntax+import C.Expr.Typecheck++import Test.CExpr.Typecheck.Infra++tests :: TestTree+tests = testGroup "classify" [+      tests_keywordTypes+    , tests_typeApp+    , tests_intLiterals+    , tests_arithmetic+    , tests_functionLike+    , tests_typeEnvChain+    , tests_errors+    ]++{-------------------------------------------------------------------------------+  Group 1: keyword type bodies+-------------------------------------------------------------------------------}++tests_keywordTypes :: TestTree+tests_keywordTypes = testGroup "keyword type bodies" [+      testCase "int"        $ assertTypeMacro $ classifyOne "M" VNil (tyLit (TypeInt Nothing (Just SizeInt)))+    , testCase "unsigned"   $ assertTypeMacro $ classifyOne "M" VNil (tyLit (TypeInt (Just Unsigned) Nothing))+    , testCase "float"      $ assertTypeMacro $ classifyOne "M" VNil (tyLit (TypeFloat SizeFloat))+    , testCase "double"     $ assertTypeMacro $ classifyOne "M" VNil (tyLit (TypeFloat SizeDouble))+    , testCase "_Bool"      $ assertTypeMacro $ classifyOne "M" VNil (tyLit TypeBool)+    , testCase "char"       $ assertTypeMacro $ classifyOne "M" VNil (tyLit (TypeChar Nothing))+    , testCase "struct Foo" $ assertTypeMacro $ classifyOne "M" VNil (mtagged "Foo" TagStruct)+    , testCase "union Bar"  $ assertTypeMacro $ classifyOne "M" VNil (mtagged "Bar" TagUnion)+    , testCase "enum Baz"   $ assertTypeMacro $ classifyOne "M" VNil (mtagged "Baz" TagEnum)+    ]++{-------------------------------------------------------------------------------+  Group 2: type application bodies+-------------------------------------------------------------------------------}++tests_typeApp :: TestTree+tests_typeApp = testGroup "type application bodies" [+      testCase "int *"        $ assertTypeMacro $ classifyOne "M" VNil (ptrOf (tyLit intTy))+    , testCase "const int"    $ assertTypeMacro $ classifyOne "M" VNil (constOf (tyLit intTy))+    , testCase "const int *"  $ assertTypeMacro $ classifyOne "M" VNil (ptrOf (constOf (tyLit intTy)))+    , testCase "int * const"  $ assertTypeMacro $ classifyOne "M" VNil (constOf (ptrOf (tyLit intTy)))+    , testCase "void *"       $ assertTypeMacro $ classifyOne "M" VNil (ptrOf (tyLit TypeVoid))+    , testCase "struct Foo *" $ assertTypeMacro $ classifyOne "M" VNil (ptrOf (mtagged "Foo" TagStruct))+    ]++{-------------------------------------------------------------------------------+  Group 3: integer literal bodies+-------------------------------------------------------------------------------}++tests_intLiterals :: TestTree+tests_intLiterals = testGroup "integer literal bodies" [+      testCase "0"   $ assertValueMacro $ classifyOne "M" VNil (intLit 0)+    , testCase "1"   $ assertValueMacro $ classifyOne "M" VNil (intLit 1)+    , testCase "42"  $ assertValueMacro $ classifyOne "M" VNil (intLit 42)+    , testCase "-1"  $ assertValueMacro $ classifyOne "M" VNil (intLit (-1))+    ]++{-------------------------------------------------------------------------------+  Group 4: arithmetic expression bodies+-------------------------------------------------------------------------------}++tests_arithmetic :: TestTree+tests_arithmetic = testGroup "arithmetic expression bodies" [+      testCase "1 + 2"   $ assertValueMacro $ classifyOne "M" VNil (add (intLit 1) (intLit 2))+    , testCase "1 << 4"  $ assertValueMacro $ classifyOne "M" VNil (shiftLeft (intLit 1) (intLit 4))+    ]++{-------------------------------------------------------------------------------+  Group 5: function-like macro bodies (with formal parameters)+-------------------------------------------------------------------------------}++tests_functionLike :: TestTree+tests_functionLike = testGroup "function-like macro bodies" [+      testCase "identity: \\x -> x" $+        assertValueMacro $+          classifyOne "IDENTITY" ("x" ::: VNil) (mlocal IZ)+    , testCase "add: \\a b -> a + b" $+        assertValueMacro $+          classifyOne "ADD" ("a" ::: "b" ::: VNil) (add (mlocal I1) (mlocal IZ))+    ]++{-------------------------------------------------------------------------------+  Group 6: TypeEnv chain — value macro references+-------------------------------------------------------------------------------}++tests_typeEnvChain :: TestTree+tests_typeEnvChain = testGroup "TypeEnv chain (value macro references)" [+      testCase "B references A (both value macros)" $ do+        let results = runTcSeq+              [ ("A", intLit 1)+              , ("B", mvar "A")+              ]+        mapM_ assertValueMacro results++    , testCase "C references B which references A" $ do+        let results = runTcSeq+              [ ("A", intLit 42)+              , ("B", mvar "A")+              , ("C", add (mvar "B") (intLit 1))+              ]+        assertValueMacro $ fromJust $ Map.lookup "C" results+    ]++{-------------------------------------------------------------------------------+  Group 7: error cases+-------------------------------------------------------------------------------}++tests_errors :: TestTree+tests_errors = testGroup "error cases" [+      testCase "unbound variable" $+        -- A bare identifier not in TypeEnv and not a macro argument is an+        -- unbound variable.  'tcMacros' reports it as 'MacroTcError'.+        assertCheckError $ classifyOne "M" VNil (mvar "unknown")++    , testCase "value macro referencing unknown name" $+        -- Even inside arithmetic, an unbound reference fails.+        assertCheckError $+          classifyOne "M" VNil (add (intLit 1) (mvar "UNDEFINED"))++    , testCase "type macro with unused parameter" $+        assertCheckError $+          classifyOne "M" ("X" ::: VNil) ((tyLit (TypeInt Nothing Nothing)))++    , testCase "bare void type macro is rejected" $+        assertCheckError $ classifyOne "M" VNil (tyLit TypeVoid)++    , testCase "const void type macro is rejected" $+        assertCheckError $ classifyOne "M" VNil (constOf (tyLit TypeVoid))+    ]+  where+    assertCheckError :: (Show a) => MacroTcResult a -> Assertion+    assertCheckError = \case+      MacroTcError _ ->+        pure ()+      r ->+        assertFailure $ "expected MacroTcError; got: " ++ show r++{-------------------------------------------------------------------------------+  Helpers+-------------------------------------------------------------------------------}++-- | Signed int literal, used in multiple test groups.+intTy :: TypeLit+intTy = TypeInt (Just Signed) (Just SizeInt)
+ test/Test/CExpr/Typecheck/Infra.hs view
@@ -0,0 +1,126 @@+module Test.CExpr.Typecheck.Infra (+    -- * Macro definitions+    MacDef+  , runTcSeq+  , classifyOne+    -- * Classification predicates+  , isTypeMacro+  , isValueMacro+    -- * Assertion helpers+  , assertTypeMacro+  , assertValueMacro+    -- * Expression helpers+  , tyLit+  , constOf+  , ptrOf+  , intLit+  , add+  , shiftLeft+  , mlocal+  , mvar+  , mtagged+  ) where++import Data.Functor.Identity (Identity (runIdentity))+import Data.Map (Map)+import Data.Map qualified as Map+import Data.Nat (Nat (..))+import Data.Vec.Lazy (Vec (..))+import DeBruijn (Idx (..))+import Test.Tasty.HUnit++import C.Type qualified as Runtime++import C.Expr.Syntax+import C.Expr.Typecheck+import C.Expr.Util.Panic++import Test.CExpr.Util++type MacDef = (Identifier, Expr Z (Ps ()))++-- | Run 'tcMacros' on a single macro+--+-- Convenience for tests that exercise one macro in isolation; threads no+-- typedef context.+classifyOne ::+     forall ctx.+     Identifier+  -> Vec ctx Identifier+  -> Expr ctx (Ps ())+  -> MacroTcResult Name+classifyOne name params body =+    case Map.toList (runTcMacros [Macro fakeLoc name params body']) of+      ((_, x):_) -> x+      []         -> panicPure "classifyOne: unexpected empty typecheck result"+  where+    body' :: Expr ctx (Ps Name)+    body' = identityResolutionPass body++-- | Typecheck a sequence of nullary macros in order, threading each successful+-- result into the typing environment for later macros to reference.+runTcSeq :: [MacDef] -> Map Identifier (MacroTcResult Name)+runTcSeq defs =+    runTcMacros [Macro fakeLoc nm VNil (identityResolutionPass body) | (nm, body) <- defs]++-- | Shared 'tcMacros' driver for the test helpers: every annotation projects to+-- 'Nothing', so all variable types resolve through the internal 'TypeEnv'.+runTcMacros :: Show ann => [Macro ann] -> Map Identifier (MacroTcResult ann)+runTcMacros macros = tcMacros (const Nothing) macros++isTypeMacro :: MacroTcResult a -> Bool+isTypeMacro (MacroTcTypeExpr _) = True+isTypeMacro _                   = False++isValueMacro :: MacroTcResult a -> Bool+isValueMacro (MacroTcValueExpr _) = True+isValueMacro _                    = False++assertTypeMacro :: (Show a) => MacroTcResult a -> Assertion+assertTypeMacro r =+    assertBool ("expected MacroTcTypeExpr, got: " ++ show r) (isTypeMacro r)++assertValueMacro :: (Show a) => MacroTcResult a -> Assertion+assertValueMacro r =+    assertBool ("expected MacroTcValueExpr, got: " ++ show r) (isValueMacro r)++tyLit :: TypeLit -> Expr ctx (Ps ())+tyLit = Term . Literal . TypeLit++constOf :: Expr ctx (Ps ()) -> Expr ctx (Ps ())+constOf e = TyApp Const (e ::: VNil)++ptrOf :: Expr ctx (Ps ()) -> Expr ctx (Ps ())+ptrOf e = TyApp Pointer (e ::: VNil)++-- | Construct an integer literal expression with a 'signed int' type hint.+-- Suitable for tests where the exact inferred integer type is not the subject+-- under test.+intLit :: Integer -> Expr ctx (Ps ())+intLit n = Term $ Literal $ ValueLit $ ValueInt $+    IntegerLiteral+      (Runtime.Int Runtime.Signed)+      n++add :: Expr ctx (Ps ()) -> Expr ctx (Ps ()) -> Expr ctx (Ps ())+add a b = VaApp NoXApp MAdd (a ::: b ::: VNil)++shiftLeft :: Expr ctx (Ps ()) -> Expr ctx (Ps ()) -> Expr ctx (Ps ())+shiftLeft a b = VaApp NoXApp MShiftLeft (a ::: b ::: VNil)++mlocal :: Idx ctx -> Expr ctx (Ps ())+mlocal i = Term $ LocalParam i++mvar :: Identifier -> Expr ctx (Ps ())+mvar n = Term $ Var (XVarPs ()) (NameOrdinary n) []++mtagged :: Identifier -> TagKind -> Expr ctx (Ps ())+mtagged n t = Term $ Var (XVarPs ()) (NameTagged n t) []++{-------------------------------------------------------------------------------+  Auxiliary+-------------------------------------------------------------------------------}++-- | Resolve 'Name's to themselves, faking a tiny name resolution pass.+identityResolutionPass :: Expr ctx (Ps a) -> Expr ctx (Ps Name)+identityResolutionPass body = runIdentity $ annotateExpr (\n _ -> pure n) body
+ test/Test/CExpr/Util.hs view
@@ -0,0 +1,22 @@+-- | Shared helpers for the c-expr-dsl test suite.+module Test.CExpr.Util (+    fakeLoc+  ) where++import Clang.HighLevel.Types++-- | A synthetic source location used to satisfy constructors that carry a+-- 'MultiLoc' (notably 'C.Expr.Syntax.Macro' and 'Token') in tests where the+-- actual location is irrelevant.+fakeLoc :: MultiLoc+fakeLoc = MultiLoc{+      multiLocExpansion = SingleLoc{+          singleLocPath   = "<test>"+        , singleLocLine   = 1+        , singleLocColumn = 1+        , singleLocOffset = 1+        }+    , multiLocPresumed  = Nothing+    , multiLocSpelling  = Nothing+    , multiLocFile      = Nothing+    }
+ test/fixtures/macros.C17.golden view
@@ -0,0 +1,82 @@+TY_VOID: Right Term (Literal (TypeLit TypeVoid))+TY_BOOL: Right Term (Literal (TypeLit TypeBool))+TY_BOOL_C23: Right Term (Var (XVarPs {psAnn = ()}) (NameOrdinary "bool") [])+TY_INT: Right Term (Literal (TypeLit (TypeInt Nothing (Just SizeInt))))+TY_SIGNED: Right Term (Literal (TypeLit (TypeInt (Just Signed) Nothing)))+TY_UNSIGNED: Right Term (Literal (TypeLit (TypeInt (Just Unsigned) Nothing)))+TY_SHORT: Right Term (Literal (TypeLit (TypeInt Nothing (Just SizeShort))))+TY_LONG: Right Term (Literal (TypeLit (TypeInt Nothing (Just SizeLong))))+TY_LONG_LONG: Right Term (Literal (TypeLit (TypeInt Nothing (Just SizeLongLong))))+TY_UNSIGNED_INT: Right Term (Literal (TypeLit (TypeInt (Just Unsigned) (Just SizeInt))))+TY_SIGNED_INT: Right Term (Literal (TypeLit (TypeInt (Just Signed) (Just SizeInt))))+TY_UNSIGNED_SHORT: Right Term (Literal (TypeLit (TypeInt (Just Unsigned) (Just SizeShort))))+TY_UNSIGNED_LONG: Right Term (Literal (TypeLit (TypeInt (Just Unsigned) (Just SizeLong))))+TY_UNSIGNED_LONG_LONG: Right Term (Literal (TypeLit (TypeInt (Just Unsigned) (Just SizeLongLong))))+TY_LONG_LONG_INT: Right Term (Literal (TypeLit (TypeInt Nothing (Just SizeLongLong))))+TY_CHAR: Right Term (Literal (TypeLit (TypeChar Nothing)))+TY_SIGNED_CHAR: Right Term (Literal (TypeLit (TypeChar (Just Signed))))+TY_UNSIGNED_CHAR: Right Term (Literal (TypeLit (TypeChar (Just Unsigned))))+TY_FLOAT: Right Term (Literal (TypeLit (TypeFloat SizeFloat)))+TY_DOUBLE: Right Term (Literal (TypeLit (TypeFloat SizeDouble)))+TY_CONST_INT: Right TyApp Const (Term (Literal (TypeLit (TypeInt Nothing (Just SizeInt)))) ::: VNil)+TY_INT_CONST: Right TyApp Const (Term (Literal (TypeLit (TypeInt Nothing (Just SizeInt)))) ::: VNil)+TY_CONST_VOID: Right TyApp Const (Term (Literal (TypeLit TypeVoid)) ::: VNil)+TY_INT_PTR: Right TyApp Pointer (Term (Literal (TypeLit (TypeInt Nothing (Just SizeInt)))) ::: VNil)+TY_INT_PTR_PTR: Right TyApp Pointer (TyApp Pointer (Term (Literal (TypeLit (TypeInt Nothing (Just SizeInt)))) ::: VNil) ::: VNil)+TY_VOID_PTR: Right TyApp Pointer (Term (Literal (TypeLit TypeVoid)) ::: VNil)+TY_CONST_INT_PTR: Right TyApp Pointer (TyApp Const (Term (Literal (TypeLit (TypeInt Nothing (Just SizeInt)))) ::: VNil) ::: VNil)+TY_INT_PTR_CONST: Right TyApp Const (TyApp Pointer (Term (Literal (TypeLit (TypeInt Nothing (Just SizeInt)))) ::: VNil) ::: VNil)+PTR_TO_CONST_L: Right TyApp Pointer (TyApp Const (Term (Literal (TypeLit (TypeInt Nothing (Just SizeInt)))) ::: VNil) ::: VNil)+PTR_TO_CONST_R: Right TyApp Pointer (TyApp Const (Term (Literal (TypeLit (TypeInt Nothing (Just SizeInt)))) ::: VNil) ::: VNil)+CONST_PTR: Right TyApp Const (TyApp Pointer (Term (Literal (TypeLit (TypeInt Nothing (Just SizeInt)))) ::: VNil) ::: VNil)+CONST_PTR_TO_CONST_L: Right TyApp Const (TyApp Pointer (TyApp Const (Term (Literal (TypeLit (TypeInt Nothing (Just SizeInt)))) ::: VNil) ::: VNil) ::: VNil)+CONST_PTR_TO_CONST_R: Right TyApp Const (TyApp Pointer (TyApp Const (Term (Literal (TypeLit (TypeInt Nothing (Just SizeInt)))) ::: VNil) ::: VNil) ::: VNil)+CONST_PTR_CHAIN_1: Right TyApp Pointer (TyApp Const (TyApp Pointer (TyApp Const (TyApp Pointer (TyApp Const (Term (Literal (TypeLit (TypeInt Nothing (Just SizeInt)))) ::: VNil) ::: VNil) ::: VNil) ::: VNil) ::: VNil) ::: VNil)+CONST_PTR_CHAIN_2: Right TyApp Const (TyApp Pointer (TyApp Const (TyApp Pointer (TyApp Const (TyApp Pointer (TyApp Const (Term (Literal (TypeLit (TypeInt Nothing (Just SizeInt)))) ::: VNil) ::: VNil) ::: VNil) ::: VNil) ::: VNil) ::: VNil) ::: VNil)+CONST_PTR_CHAIN_3: Right TyApp Const (TyApp Pointer (TyApp Const (TyApp Pointer (TyApp Pointer (TyApp Const (TyApp Pointer (TyApp Const (Term (Literal (TypeLit (TypeInt Nothing (Just SizeInt)))) ::: VNil) ::: VNil) ::: VNil) ::: VNil) ::: VNil) ::: VNil) ::: VNil) ::: VNil)+CONST_PTR_CHAIN_4: Right TyApp Pointer (TyApp Const (TyApp Pointer (TyApp Const (TyApp Pointer (TyApp Const (Term (Literal (TypeLit (TypeInt Nothing (Just SizeInt)))) ::: VNil) ::: VNil) ::: VNil) ::: VNil) ::: VNil) ::: VNil)+CONST_PTR_CHAIN_5: Right TyApp Const (TyApp Pointer (TyApp Const (TyApp Pointer (TyApp Const (TyApp Pointer (TyApp Const (Term (Literal (TypeLit (TypeInt Nothing (Just SizeInt)))) ::: VNil) ::: VNil) ::: VNil) ::: VNil) ::: VNil) ::: VNil) ::: VNil)+CONST_PTR_CHAIN_6: Right TyApp Const (TyApp Pointer (TyApp Const (TyApp Pointer (TyApp Pointer (TyApp Const (TyApp Pointer (TyApp Const (Term (Literal (TypeLit (TypeInt Nothing (Just SizeInt)))) ::: VNil) ::: VNil) ::: VNil) ::: VNil) ::: VNil) ::: VNil) ::: VNil) ::: VNil)+CONST_PTR_CHAIN_7: Right TyApp Const (TyApp Pointer (TyApp Pointer (TyApp Pointer (TyApp Pointer (TyApp Const (Term (Literal (TypeLit (TypeInt Nothing (Just SizeInt)))) ::: VNil) ::: VNil) ::: VNil) ::: VNil) ::: VNil) ::: VNil)+CONST_PTR_CHAIN_8: Right TyApp Const (TyApp Pointer (TyApp Pointer (TyApp Pointer (TyApp Pointer (TyApp Const (Term (Literal (TypeLit (TypeInt Nothing (Just SizeInt)))) ::: VNil) ::: VNil) ::: VNil) ::: VNil) ::: VNil) ::: VNil)+CONST_PTR_CHAIN_9: Right TyApp Pointer (TyApp Const (TyApp Pointer (TyApp Pointer (TyApp Pointer (TyApp Pointer (Term (Literal (TypeLit (TypeInt Nothing (Just SizeInt)))) ::: VNil) ::: VNil) ::: VNil) ::: VNil) ::: VNil) ::: VNil)+TY_STRUCT_FOO: Right Term (Var (XVarPs {psAnn = ()}) (NameTagged "Foo" TagStruct) [])+TY_UNION_BAR: Right Term (Var (XVarPs {psAnn = ()}) (NameTagged "Bar" TagUnion) [])+TY_ENUM_BAZ: Right Term (Var (XVarPs {psAnn = ()}) (NameTagged "Baz" TagEnum) [])+TY_STRUCT_FOO_PTR: Right TyApp Pointer (Term (Var (XVarPs {psAnn = ()}) (NameTagged "Foo" TagStruct) []) ::: VNil)+TY_SIZE_T: Right Term (Var (XVarPs {psAnn = ()}) (NameOrdinary "size_t") [])+TY_UINT32_T: Right Term (Var (XVarPs {psAnn = ()}) (NameOrdinary "uint32_t") [])+TY_CONST_SIZE_T: Right TyApp Const (Term (Var (XVarPs {psAnn = ()}) (NameOrdinary "size_t") []) ::: VNil)+TY_SIZE_T_PTR: Right TyApp Pointer (Term (Var (XVarPs {psAnn = ()}) (NameOrdinary "size_t") []) ::: VNil)+TY_MACRO_REF: Right Term (Var (XVarPs {psAnn = ()}) (NameOrdinary "EXPR_FORTY_TWO") [])+EXPR_ZERO: Right Term (Literal (ValueLit (ValueInt (IntegerLiteral {integerLiteralType = Int Signed, integerLiteralValue = 0}))))+EXPR_ONE: Right Term (Literal (ValueLit (ValueInt (IntegerLiteral {integerLiteralType = Int Signed, integerLiteralValue = 1}))))+EXPR_FORTY_TWO: Right Term (Literal (ValueLit (ValueInt (IntegerLiteral {integerLiteralType = Int Signed, integerLiteralValue = 42}))))+EXPR_HEX: Right Term (Literal (ValueLit (ValueInt (IntegerLiteral {integerLiteralType = Int Signed, integerLiteralValue = 255}))))+EXPR_NEG: Right VaApp NoXApp MUnaryMinus (Term (Literal (ValueLit (ValueInt (IntegerLiteral {integerLiteralType = Int Signed, integerLiteralValue = 1})))) ::: VNil)+EXPR_ADD: Right VaApp NoXApp MAdd (Term (Literal (ValueLit (ValueInt (IntegerLiteral {integerLiteralType = Int Signed, integerLiteralValue = 1})))) ::: Term (Literal (ValueLit (ValueInt (IntegerLiteral {integerLiteralType = Int Signed, integerLiteralValue = 2})))) ::: VNil)+EXPR_SUB: Right VaApp NoXApp MSub (Term (Literal (ValueLit (ValueInt (IntegerLiteral {integerLiteralType = Int Signed, integerLiteralValue = 10})))) ::: Term (Literal (ValueLit (ValueInt (IntegerLiteral {integerLiteralType = Int Signed, integerLiteralValue = 3})))) ::: VNil)+EXPR_MUL: Right VaApp NoXApp MMult (Term (Literal (ValueLit (ValueInt (IntegerLiteral {integerLiteralType = Int Signed, integerLiteralValue = 4})))) ::: Term (Literal (ValueLit (ValueInt (IntegerLiteral {integerLiteralType = Int Signed, integerLiteralValue = 5})))) ::: VNil)+EXPR_DIV: Right VaApp NoXApp MDiv (Term (Literal (ValueLit (ValueInt (IntegerLiteral {integerLiteralType = Int Signed, integerLiteralValue = 8})))) ::: Term (Literal (ValueLit (ValueInt (IntegerLiteral {integerLiteralType = Int Signed, integerLiteralValue = 2})))) ::: VNil)+EXPR_SHIFT_LEFT: Right VaApp NoXApp MShiftLeft (Term (Literal (ValueLit (ValueInt (IntegerLiteral {integerLiteralType = Int Signed, integerLiteralValue = 1})))) ::: Term (Literal (ValueLit (ValueInt (IntegerLiteral {integerLiteralType = Int Signed, integerLiteralValue = 4})))) ::: VNil)+EXPR_BITWISE_OR: Right VaApp NoXApp MBitwiseOr (Term (Literal (ValueLit (ValueInt (IntegerLiteral {integerLiteralType = Int Signed, integerLiteralValue = 15})))) ::: Term (Literal (ValueLit (ValueInt (IntegerLiteral {integerLiteralType = Int Signed, integerLiteralValue = 240})))) ::: VNil)+EXPR_PARENS: Right Term (Literal (ValueLit (ValueInt (IntegerLiteral {integerLiteralType = Int Signed, integerLiteralValue = 42}))))+EXPR_COMPOUND: Right VaApp NoXApp MMult (VaApp NoXApp MAdd (Term (Literal (ValueLit (ValueInt (IntegerLiteral {integerLiteralType = Int Signed, integerLiteralValue = 1})))) ::: Term (Literal (ValueLit (ValueInt (IntegerLiteral {integerLiteralType = Int Signed, integerLiteralValue = 2})))) ::: VNil) ::: Term (Literal (ValueLit (ValueInt (IntegerLiteral {integerLiteralType = Int Signed, integerLiteralValue = 3})))) ::: VNil)+FUNC_IDENTITY: Right Term (LocalParam 0)+FUNC_ADD: Right VaApp NoXApp MAdd (Term (LocalParam 1) ::: Term (LocalParam 0) ::: VNil)+FUNC_NEG: Right VaApp NoXApp MUnaryMinus (Term (LocalParam 0) ::: VNil)+FUNC_MULTIPLE_LOCAL_PARAMS: Right VaApp NoXApp MAdd (Term (LocalParam 3) ::: VaApp NoXApp MSub (Term (LocalParam 2) ::: VaApp NoXApp MAdd (Term (LocalParam 1) ::: Term (LocalParam 0) ::: VNil) ::: VNil) ::: VNil)+FUNC_SINGLELINE: Right VaApp NoXApp MMult (Term (LocalParam 1) ::: Term (LocalParam 0) ::: VNil)+FUNC_MULTILINE: Right VaApp NoXApp MMult (Term (LocalParam 1) ::: Term (LocalParam 0) ::: VNil)+EXPR_REF_ADD: Right VaApp NoXApp MAdd (Term (Var (XVarPs {psAnn = ()}) (NameOrdinary "EXPR_ONE") []) ::: Term (Var (XVarPs {psAnn = ()}) (NameOrdinary "EXPR_FORTY_TWO") []) ::: VNil)+EXPR_CALL_ADD: Right Term (Var (XVarPs {psAnn = ()}) (NameOrdinary "FUNC_ADD") [Term (Literal (ValueLit (ValueInt (IntegerLiteral {integerLiteralType = Int Signed, integerLiteralValue = 1})))),Term (Literal (ValueLit (ValueInt (IntegerLiteral {integerLiteralType = Int Signed, integerLiteralValue = 2}))))])+EXPR_CALL_NESTED: Right VaApp NoXApp MAdd (Term (Var (XVarPs {psAnn = ()}) (NameOrdinary "FUNC_ADD") [Term (Var (XVarPs {psAnn = ()}) (NameOrdinary "EXPR_ONE") []),Term (Var (XVarPs {psAnn = ()}) (NameOrdinary "EXPR_FORTY_TWO") [])]) ::: Term (Literal (ValueLit (ValueInt (IntegerLiteral {integerLiteralType = Int Signed, integerLiteralValue = 1})))) ::: VNil)+CAST_SINGLE_NOKW: Left <parse error>+CAST_SINGLE_KW: Left <parse error>+CAST_MULTI_KW: Left <parse error>+BAD_KEYWORD_AS_PARAM: Left <parse error>+TYPE_FUN_WITH_PARAM: Right Term (Literal (TypeLit (TypeInt Nothing (Just SizeInt))))+BAD_TERNARY: Left <parse error>+BAD_LONG_DOUBLE: Left <parse error>+PACK_START: Left <parse error>+PACK_FINISH: Left <parse error>
+ test/fixtures/macros.C23.golden view
@@ -0,0 +1,82 @@+TY_VOID: Right Term (Literal (TypeLit TypeVoid))+TY_BOOL: Right Term (Literal (TypeLit TypeBool))+TY_BOOL_C23: Right Term (Literal (TypeLit TypeBool))+TY_INT: Right Term (Literal (TypeLit (TypeInt Nothing (Just SizeInt))))+TY_SIGNED: Right Term (Literal (TypeLit (TypeInt (Just Signed) Nothing)))+TY_UNSIGNED: Right Term (Literal (TypeLit (TypeInt (Just Unsigned) Nothing)))+TY_SHORT: Right Term (Literal (TypeLit (TypeInt Nothing (Just SizeShort))))+TY_LONG: Right Term (Literal (TypeLit (TypeInt Nothing (Just SizeLong))))+TY_LONG_LONG: Right Term (Literal (TypeLit (TypeInt Nothing (Just SizeLongLong))))+TY_UNSIGNED_INT: Right Term (Literal (TypeLit (TypeInt (Just Unsigned) (Just SizeInt))))+TY_SIGNED_INT: Right Term (Literal (TypeLit (TypeInt (Just Signed) (Just SizeInt))))+TY_UNSIGNED_SHORT: Right Term (Literal (TypeLit (TypeInt (Just Unsigned) (Just SizeShort))))+TY_UNSIGNED_LONG: Right Term (Literal (TypeLit (TypeInt (Just Unsigned) (Just SizeLong))))+TY_UNSIGNED_LONG_LONG: Right Term (Literal (TypeLit (TypeInt (Just Unsigned) (Just SizeLongLong))))+TY_LONG_LONG_INT: Right Term (Literal (TypeLit (TypeInt Nothing (Just SizeLongLong))))+TY_CHAR: Right Term (Literal (TypeLit (TypeChar Nothing)))+TY_SIGNED_CHAR: Right Term (Literal (TypeLit (TypeChar (Just Signed))))+TY_UNSIGNED_CHAR: Right Term (Literal (TypeLit (TypeChar (Just Unsigned))))+TY_FLOAT: Right Term (Literal (TypeLit (TypeFloat SizeFloat)))+TY_DOUBLE: Right Term (Literal (TypeLit (TypeFloat SizeDouble)))+TY_CONST_INT: Right TyApp Const (Term (Literal (TypeLit (TypeInt Nothing (Just SizeInt)))) ::: VNil)+TY_INT_CONST: Right TyApp Const (Term (Literal (TypeLit (TypeInt Nothing (Just SizeInt)))) ::: VNil)+TY_CONST_VOID: Right TyApp Const (Term (Literal (TypeLit TypeVoid)) ::: VNil)+TY_INT_PTR: Right TyApp Pointer (Term (Literal (TypeLit (TypeInt Nothing (Just SizeInt)))) ::: VNil)+TY_INT_PTR_PTR: Right TyApp Pointer (TyApp Pointer (Term (Literal (TypeLit (TypeInt Nothing (Just SizeInt)))) ::: VNil) ::: VNil)+TY_VOID_PTR: Right TyApp Pointer (Term (Literal (TypeLit TypeVoid)) ::: VNil)+TY_CONST_INT_PTR: Right TyApp Pointer (TyApp Const (Term (Literal (TypeLit (TypeInt Nothing (Just SizeInt)))) ::: VNil) ::: VNil)+TY_INT_PTR_CONST: Right TyApp Const (TyApp Pointer (Term (Literal (TypeLit (TypeInt Nothing (Just SizeInt)))) ::: VNil) ::: VNil)+PTR_TO_CONST_L: Right TyApp Pointer (TyApp Const (Term (Literal (TypeLit (TypeInt Nothing (Just SizeInt)))) ::: VNil) ::: VNil)+PTR_TO_CONST_R: Right TyApp Pointer (TyApp Const (Term (Literal (TypeLit (TypeInt Nothing (Just SizeInt)))) ::: VNil) ::: VNil)+CONST_PTR: Right TyApp Const (TyApp Pointer (Term (Literal (TypeLit (TypeInt Nothing (Just SizeInt)))) ::: VNil) ::: VNil)+CONST_PTR_TO_CONST_L: Right TyApp Const (TyApp Pointer (TyApp Const (Term (Literal (TypeLit (TypeInt Nothing (Just SizeInt)))) ::: VNil) ::: VNil) ::: VNil)+CONST_PTR_TO_CONST_R: Right TyApp Const (TyApp Pointer (TyApp Const (Term (Literal (TypeLit (TypeInt Nothing (Just SizeInt)))) ::: VNil) ::: VNil) ::: VNil)+CONST_PTR_CHAIN_1: Right TyApp Pointer (TyApp Const (TyApp Pointer (TyApp Const (TyApp Pointer (TyApp Const (Term (Literal (TypeLit (TypeInt Nothing (Just SizeInt)))) ::: VNil) ::: VNil) ::: VNil) ::: VNil) ::: VNil) ::: VNil)+CONST_PTR_CHAIN_2: Right TyApp Const (TyApp Pointer (TyApp Const (TyApp Pointer (TyApp Const (TyApp Pointer (TyApp Const (Term (Literal (TypeLit (TypeInt Nothing (Just SizeInt)))) ::: VNil) ::: VNil) ::: VNil) ::: VNil) ::: VNil) ::: VNil) ::: VNil)+CONST_PTR_CHAIN_3: Right TyApp Const (TyApp Pointer (TyApp Const (TyApp Pointer (TyApp Pointer (TyApp Const (TyApp Pointer (TyApp Const (Term (Literal (TypeLit (TypeInt Nothing (Just SizeInt)))) ::: VNil) ::: VNil) ::: VNil) ::: VNil) ::: VNil) ::: VNil) ::: VNil) ::: VNil)+CONST_PTR_CHAIN_4: Right TyApp Pointer (TyApp Const (TyApp Pointer (TyApp Const (TyApp Pointer (TyApp Const (Term (Literal (TypeLit (TypeInt Nothing (Just SizeInt)))) ::: VNil) ::: VNil) ::: VNil) ::: VNil) ::: VNil) ::: VNil)+CONST_PTR_CHAIN_5: Right TyApp Const (TyApp Pointer (TyApp Const (TyApp Pointer (TyApp Const (TyApp Pointer (TyApp Const (Term (Literal (TypeLit (TypeInt Nothing (Just SizeInt)))) ::: VNil) ::: VNil) ::: VNil) ::: VNil) ::: VNil) ::: VNil) ::: VNil)+CONST_PTR_CHAIN_6: Right TyApp Const (TyApp Pointer (TyApp Const (TyApp Pointer (TyApp Pointer (TyApp Const (TyApp Pointer (TyApp Const (Term (Literal (TypeLit (TypeInt Nothing (Just SizeInt)))) ::: VNil) ::: VNil) ::: VNil) ::: VNil) ::: VNil) ::: VNil) ::: VNil) ::: VNil)+CONST_PTR_CHAIN_7: Right TyApp Const (TyApp Pointer (TyApp Pointer (TyApp Pointer (TyApp Pointer (TyApp Const (Term (Literal (TypeLit (TypeInt Nothing (Just SizeInt)))) ::: VNil) ::: VNil) ::: VNil) ::: VNil) ::: VNil) ::: VNil)+CONST_PTR_CHAIN_8: Right TyApp Const (TyApp Pointer (TyApp Pointer (TyApp Pointer (TyApp Pointer (TyApp Const (Term (Literal (TypeLit (TypeInt Nothing (Just SizeInt)))) ::: VNil) ::: VNil) ::: VNil) ::: VNil) ::: VNil) ::: VNil)+CONST_PTR_CHAIN_9: Right TyApp Pointer (TyApp Const (TyApp Pointer (TyApp Pointer (TyApp Pointer (TyApp Pointer (Term (Literal (TypeLit (TypeInt Nothing (Just SizeInt)))) ::: VNil) ::: VNil) ::: VNil) ::: VNil) ::: VNil) ::: VNil)+TY_STRUCT_FOO: Right Term (Var (XVarPs {psAnn = ()}) (NameTagged "Foo" TagStruct) [])+TY_UNION_BAR: Right Term (Var (XVarPs {psAnn = ()}) (NameTagged "Bar" TagUnion) [])+TY_ENUM_BAZ: Right Term (Var (XVarPs {psAnn = ()}) (NameTagged "Baz" TagEnum) [])+TY_STRUCT_FOO_PTR: Right TyApp Pointer (Term (Var (XVarPs {psAnn = ()}) (NameTagged "Foo" TagStruct) []) ::: VNil)+TY_SIZE_T: Right Term (Var (XVarPs {psAnn = ()}) (NameOrdinary "size_t") [])+TY_UINT32_T: Right Term (Var (XVarPs {psAnn = ()}) (NameOrdinary "uint32_t") [])+TY_CONST_SIZE_T: Right TyApp Const (Term (Var (XVarPs {psAnn = ()}) (NameOrdinary "size_t") []) ::: VNil)+TY_SIZE_T_PTR: Right TyApp Pointer (Term (Var (XVarPs {psAnn = ()}) (NameOrdinary "size_t") []) ::: VNil)+TY_MACRO_REF: Right Term (Var (XVarPs {psAnn = ()}) (NameOrdinary "EXPR_FORTY_TWO") [])+EXPR_ZERO: Right Term (Literal (ValueLit (ValueInt (IntegerLiteral {integerLiteralType = Int Signed, integerLiteralValue = 0}))))+EXPR_ONE: Right Term (Literal (ValueLit (ValueInt (IntegerLiteral {integerLiteralType = Int Signed, integerLiteralValue = 1}))))+EXPR_FORTY_TWO: Right Term (Literal (ValueLit (ValueInt (IntegerLiteral {integerLiteralType = Int Signed, integerLiteralValue = 42}))))+EXPR_HEX: Right Term (Literal (ValueLit (ValueInt (IntegerLiteral {integerLiteralType = Int Signed, integerLiteralValue = 255}))))+EXPR_NEG: Right VaApp NoXApp MUnaryMinus (Term (Literal (ValueLit (ValueInt (IntegerLiteral {integerLiteralType = Int Signed, integerLiteralValue = 1})))) ::: VNil)+EXPR_ADD: Right VaApp NoXApp MAdd (Term (Literal (ValueLit (ValueInt (IntegerLiteral {integerLiteralType = Int Signed, integerLiteralValue = 1})))) ::: Term (Literal (ValueLit (ValueInt (IntegerLiteral {integerLiteralType = Int Signed, integerLiteralValue = 2})))) ::: VNil)+EXPR_SUB: Right VaApp NoXApp MSub (Term (Literal (ValueLit (ValueInt (IntegerLiteral {integerLiteralType = Int Signed, integerLiteralValue = 10})))) ::: Term (Literal (ValueLit (ValueInt (IntegerLiteral {integerLiteralType = Int Signed, integerLiteralValue = 3})))) ::: VNil)+EXPR_MUL: Right VaApp NoXApp MMult (Term (Literal (ValueLit (ValueInt (IntegerLiteral {integerLiteralType = Int Signed, integerLiteralValue = 4})))) ::: Term (Literal (ValueLit (ValueInt (IntegerLiteral {integerLiteralType = Int Signed, integerLiteralValue = 5})))) ::: VNil)+EXPR_DIV: Right VaApp NoXApp MDiv (Term (Literal (ValueLit (ValueInt (IntegerLiteral {integerLiteralType = Int Signed, integerLiteralValue = 8})))) ::: Term (Literal (ValueLit (ValueInt (IntegerLiteral {integerLiteralType = Int Signed, integerLiteralValue = 2})))) ::: VNil)+EXPR_SHIFT_LEFT: Right VaApp NoXApp MShiftLeft (Term (Literal (ValueLit (ValueInt (IntegerLiteral {integerLiteralType = Int Signed, integerLiteralValue = 1})))) ::: Term (Literal (ValueLit (ValueInt (IntegerLiteral {integerLiteralType = Int Signed, integerLiteralValue = 4})))) ::: VNil)+EXPR_BITWISE_OR: Right VaApp NoXApp MBitwiseOr (Term (Literal (ValueLit (ValueInt (IntegerLiteral {integerLiteralType = Int Signed, integerLiteralValue = 15})))) ::: Term (Literal (ValueLit (ValueInt (IntegerLiteral {integerLiteralType = Int Signed, integerLiteralValue = 240})))) ::: VNil)+EXPR_PARENS: Right Term (Literal (ValueLit (ValueInt (IntegerLiteral {integerLiteralType = Int Signed, integerLiteralValue = 42}))))+EXPR_COMPOUND: Right VaApp NoXApp MMult (VaApp NoXApp MAdd (Term (Literal (ValueLit (ValueInt (IntegerLiteral {integerLiteralType = Int Signed, integerLiteralValue = 1})))) ::: Term (Literal (ValueLit (ValueInt (IntegerLiteral {integerLiteralType = Int Signed, integerLiteralValue = 2})))) ::: VNil) ::: Term (Literal (ValueLit (ValueInt (IntegerLiteral {integerLiteralType = Int Signed, integerLiteralValue = 3})))) ::: VNil)+FUNC_IDENTITY: Right Term (LocalParam 0)+FUNC_ADD: Right VaApp NoXApp MAdd (Term (LocalParam 1) ::: Term (LocalParam 0) ::: VNil)+FUNC_NEG: Right VaApp NoXApp MUnaryMinus (Term (LocalParam 0) ::: VNil)+FUNC_MULTIPLE_LOCAL_PARAMS: Right VaApp NoXApp MAdd (Term (LocalParam 3) ::: VaApp NoXApp MSub (Term (LocalParam 2) ::: VaApp NoXApp MAdd (Term (LocalParam 1) ::: Term (LocalParam 0) ::: VNil) ::: VNil) ::: VNil)+FUNC_SINGLELINE: Right VaApp NoXApp MMult (Term (LocalParam 1) ::: Term (LocalParam 0) ::: VNil)+FUNC_MULTILINE: Right VaApp NoXApp MMult (Term (LocalParam 1) ::: Term (LocalParam 0) ::: VNil)+EXPR_REF_ADD: Right VaApp NoXApp MAdd (Term (Var (XVarPs {psAnn = ()}) (NameOrdinary "EXPR_ONE") []) ::: Term (Var (XVarPs {psAnn = ()}) (NameOrdinary "EXPR_FORTY_TWO") []) ::: VNil)+EXPR_CALL_ADD: Right Term (Var (XVarPs {psAnn = ()}) (NameOrdinary "FUNC_ADD") [Term (Literal (ValueLit (ValueInt (IntegerLiteral {integerLiteralType = Int Signed, integerLiteralValue = 1})))),Term (Literal (ValueLit (ValueInt (IntegerLiteral {integerLiteralType = Int Signed, integerLiteralValue = 2}))))])+EXPR_CALL_NESTED: Right VaApp NoXApp MAdd (Term (Var (XVarPs {psAnn = ()}) (NameOrdinary "FUNC_ADD") [Term (Var (XVarPs {psAnn = ()}) (NameOrdinary "EXPR_ONE") []),Term (Var (XVarPs {psAnn = ()}) (NameOrdinary "EXPR_FORTY_TWO") [])]) ::: Term (Literal (ValueLit (ValueInt (IntegerLiteral {integerLiteralType = Int Signed, integerLiteralValue = 1})))) ::: VNil)+CAST_SINGLE_NOKW: Left <parse error>+CAST_SINGLE_KW: Left <parse error>+CAST_MULTI_KW: Left <parse error>+BAD_KEYWORD_AS_PARAM: Left <parse error>+TYPE_FUN_WITH_PARAM: Right Term (Literal (TypeLit (TypeInt Nothing (Just SizeInt))))+BAD_TERNARY: Left <parse error>+BAD_LONG_DOUBLE: Left <parse error>+PACK_START: Left <parse error>+PACK_FINISH: Left <parse error>