packages feed

c-expr-runtime (empty) → 0.1.0.0

raw patch · 17 files changed

+3017/−0 lines, 17 filesdep +basedep +c-expr-runtimedep +containers

Dependencies added: base, c-expr-runtime, containers, data-array-byte, data-default, fin, libclang-bindings, some, template-haskell, text, vec

Files

+ CHANGELOG.md view
@@ -0,0 +1,10 @@+# Revision history for `c-expr`++## 0.1.0.0 -- 2026-07-14++* Remove the `C.Char` module; UTF-8 encoding of character and string literals+  now lives in `c-expr-dsl`'s parser.++## 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,20 @@+# `c-expr-runtime`++`c-expr-runtime` is a [Haskell][] library providing the runtime support for+[`c-expr-dsl`][]: a type-level universe of C types and a class-per-operator+hierarchy whose associated type families encode the C standard's+integral-promotion and arithmetic-conversion rules. It supports the+[`hs-bindgen`][] project but can be used independently.++Its test suite cross-checks operator result types against a real C compiler,+and so requires an [LLVM/Clang][] installation.++See the [main README][] for more information, and the [changelog][] for+release notes.++[Haskell]: <https://www.haskell.org/>+[LLVM/Clang]: <https://github.com/llvm/llvm-project>+[`c-expr-dsl`]: <https://github.com/well-typed/c-expr/tree/main/c-expr-dsl>+[`hs-bindgen`]: <https://github.com/well-typed/hs-bindgen>+[main README]: <https://github.com/well-typed/c-expr#readme>+[changelog]: <https://github.com/well-typed/c-expr/blob/main/c-expr-runtime/CHANGELOG.md>
+ c-expr-runtime.cabal view
@@ -0,0 +1,136 @@+cabal-version:   3.0+name:            c-expr-runtime+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:        Haskell DSL for simple C arithmetic expressions+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 a Haskell DSL for simple C arithmetic expressions,+  implementing the arithmetic conversion and integral promotion rules of the+  C standard.++  For example, addition is defined with the following type class:++  @++  infixl 2 ++  type Add :: Type -> Type -> Constraint+  class Add a b where+    type family AddRes a b :: Type+    (+) :: a -> b -> AddRes a b++  @++  That is, we can add arguments of different types, e.g. an integer and a+  floating-point number, in which case the integer will first get converted to+  the floating-point format before performing the addition.++source-repository head+  type:     git+  location: https://github.com/well-typed/c-expr.git+  subdir:   c-expr-runtime++source-repository this+  type:     git+  location: https://github.com/well-typed/c-expr.git+  subdir:   c-expr-runtime+  tag:      release-0.1.0.0++common common+  ghc-options:+    -Wall -Wunused-packages -Wno-unticked-promoted-constructors++  default-extensions:+    DataKinds+    DeriveGeneric+    DeriveTraversable+    DerivingStrategies+    FlexibleInstances+    GADTs+    ImportQualifiedPost+    LambdaCase+    MagicHash+    MultiParamTypeClasses+    ParallelListComp+    StandaloneKindSignatures+    TupleSections+    TypeApplications+    TypeFamilies+    TypeOperators++  build-depends:      base >=4.16 && <4.23+  default-language:   Haskell2010++-- C arithmetic DSL+--+-- Note: C.Operator.Classes is exposed only so its associated type families+-- (e.g. AddRes) are usable in signatures. Its classes have no instances of+-- their own; import C.Expr.HostPlatform (or a Posix32/Posix64/Win64 variant)+-- to get a platform's instances.+library+  import:          common+  hs-source-dirs:  core lib+  exposed-modules:+    C.Expr.HostPlatform+    C.Operator.Classes+    C.Operator.GenInstances+    C.Operators+    C.Type+    C.Type.Internal.Universe++  other-modules:+    C.Expr.Posix32+    C.Expr.Posix64+    C.Expr.Win64+    C.Operator.Internal+    C.Operator.TH++  -- External dependencies+  build-depends:+    , containers        >=0.5   && <0.9+    , fin               >=0.3.2 && <0.4+    , some              >=1.0.6 && <1.1+    , template-haskell  >=2.18  && <2.25+    , vec               >=0.5   && <0.6++  if impl(ghc <9.4)+    build-depends: data-array-byte >=0.1.0.1 && <0.2++test-suite tests+  import:         common+  hs-source-dirs: test+  main-is:        Main.hs+  type:           exitcode-stdio-1.0+  other-modules:  CallClang++  -- Internal dependencies+  build-depends:+    , c-expr-runtime+    , libclang-bindings++  -- Inherited dependencies+  build-depends:+    , containers+    , data-default+    , fin+    , vec++  -- External dependencies+  build-depends:  text >=1.2 && <2.2
+ core/C/Operator/Classes.hs view
@@ -0,0 +1,184 @@+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TemplateHaskell #-}+{-# LANGUAGE UndecidableInstances #-}++module C.Operator.Classes+  ( -- * Logical operators+    Not(..)+  , Logical(..)+    -- * Equality and comparison+  , RelEq(..), RelOrd(..)+  , NotNull(..)+    -- * Arithmetic+    -- ** Unary+  , Plus(..)+  , Minus(..)+    -- ** Binary+  , Add(..)+  , Sub(..)+  , Mult(..)+  , Div(..)+  , Rem(..)+    -- * Bitwise+    -- ** Unary+  , Complement(..)+    -- ** Binary+  , Bitwise(..)+  , Shift(..)+  ) where++import Prelude (Bool (..), Eq (..), Num (..))++import Data.Kind (Constraint, Type)+import Foreign (Ptr, nullPtr)+import Foreign.C++--------------------------------------------------------------------------------++-- | Class to compare whether a value is zero/null.+type NotNull :: Type -> Constraint+class NotNull a where+  notNull :: a -> Bool+instance ( Eq a, Num a ) => NotNull a where+  notNull = ( /= 0 )+instance {-# OVERLAPPING #-} NotNull ( Ptr a ) where+  notNull = ( /= nullPtr )++--------------------------------------------------------------------------------++infixr 0 `not`+-- | Class for the C logical negation operator.+type Not :: Type -> Constraint+class Not a where+  -- | C logical negation operator.+  not :: a -> CInt++infixl 7 &&+infixl 8 ||+-- | Class for C boolean logical operators (conjunction and disjunction).+type Logical :: Type -> Type -> Constraint+class Logical a b where+  (&&), (||) :: a -> b -> CInt++--------------------------------------------------------------------------------++infixl 5 ==+infixl 5 !=+-- | Class for C equality and inequality operators.+type RelEq :: Type -> Type -> Constraint+class RelEq a b where+  (==), (!=) :: a -> b -> CInt++infixl 4 >=+infixl 4 <+infixl 4 <=+infixl 4 >+-- | Class for C relative comparison operators (less than, greater than or equal, etc).+type RelOrd :: Type -> Type -> Constraint+class RelOrd a b where+  (<=), (<), (>=), (>) :: a -> b -> CInt++--------------------------------------------------------------------------------++infixr 0 `plus`+-- | Class for the C unary plus operator.+type Plus :: Type -> Constraint+class Plus a where+  -- | Result type family of the C unary plus operator.+  type family PlusRes a :: Type+  -- | C unary plus operator.+  plus :: a -> PlusRes a++infixr 0 `negate`+-- | Class for the C unary minus operator.+type Minus :: Type -> Constraint+class Minus a where+  -- | Result type family of the C unary minus operator.+  type family MinusRes a :: Type+  -- | C unary minus operator.+  negate :: a -> MinusRes a++infixl 2 ++-- | Class for the C binary addition operator.+type Add :: Type -> Type -> Constraint+class Add a b where+  -- | Result type family of the C binary addition operator.+  type family AddRes a b :: Type+  -- | C binary addition operator.+  (+) :: a -> b -> AddRes a b++infixl 2 -+-- | Class for the C binary subtraction operator.+type Sub :: Type -> Type -> Constraint+class Sub a b where+  -- | Result type family of the C binary subtraction operator.+  type family SubRes a b :: Type+  -- | C binary subtraction operator.+  (-) :: a -> b -> SubRes a b++infixl 1 *+-- | Class for the C binary multiplication operator.+type Mult :: Type -> Type -> Constraint+class Mult a b where+  -- | Result type family of the C binary multiplication operator.+  type family MultRes a b :: Type+  -- | C binary multiplication operator.+  (*) :: a -> b -> MultRes a b++infixl 1 /+-- | Class for the C binary division operator.+type Div :: Type -> Type -> Constraint+class Div a b where+  -- | Result type family of the C binary division operator.+  type family DivRes a b :: Type+  -- | C binary division operator.+  (/) :: a -> b -> DivRes a b++infixl 1 %+-- | Class for the C binary remainder operator.+type Rem :: Type -> Type -> Constraint+class Rem a b where+  -- | Result type family of the C binary remainder operator.+  type family RemRes a b :: Type+  -- | C binary remainder operator.+  (%) :: a -> b -> RemRes a b++--------------------------------------------------------------------------------++infixr 0 .~+-- | Class for the C unary bitwise complement operator.+type Complement :: Type -> Constraint+class Complement a where+  -- | Result type family of the C unary bitwise complement operator.+  type family ComplementRes a :: Type+  -- | C unary bitwise complement operator.+  (.~) :: a -> ComplementRes a++infixl 7 .&.+infixl 8 .|.+infixl 6 .^.+-- | Class for C binary bitwise logical operators.+type Bitwise :: Type -> Type -> Constraint+class Bitwise a b where+  -- | Result type family of C binary bitwise logical operators.+  type family BitsRes a b :: Type+  -- | C binary bitwise /and/ operator.+  (.&.) :: a -> b -> BitsRes a b+  -- | C binary bitwise /or/ operator.+  (.|.) :: a -> b -> BitsRes a b+  -- | C binary bitwise /xor/ operator.+  (.^.) :: a -> b -> BitsRes a b++infixl 3 <<+infixl 3 >>+-- | Class for the C binary bit-shift operators.+type Shift :: Type -> Type -> Constraint+class Shift a i where+  -- | Result type family of C binary bit-shift operators.+  type family ShiftRes a :: Type+  -- | C binary left-shift operator.+  (<<) :: a -> i -> ShiftRes a+  -- | C binary right-shift operator.+  (>>) :: a -> i -> ShiftRes a++--------------------------------------------------------------------------------
+ core/C/Operator/GenInstances.hs view
@@ -0,0 +1,218 @@+{-# LANGUAGE TemplateHaskellQuotes #-}++module C.Operator.GenInstances+  ( cExprInstances ) where++import Prelude hiding (Fractional (..), Integral (..), Num (..))+import Prelude qualified++import Control.Monad (guard)+import Data.Bits qualified as Bits+import Foreign.C.Types+import Language.Haskell.TH qualified as TH++import C.Type qualified as C++import C.Operator.Classes qualified as C+import C.Operator.Internal qualified as C+import C.Operator.TH++--------------------------------------------------------------------------------++-- | All instances for arithmetic classes on standard types, for the given+-- 'C.Platform'.+cExprInstances :: C.Platform -> TH.Q [ TH.Dec ]+cExprInstances platform = do+  concat <$> sequence [++    ----------------------------------------------------------------------------+    -- Not, Logical++    do impl <- [| \ i -> if C.notNull i then 0 else 1 |]+       withInstanceProofs+         [ genUnaryInstances ''C.Not ( Left $ TH.ConT ''CInt ) ( C.unaryLogicalType platform )+           [ ClassMethod 'C.not "singNot" 1 impl ]+         ]+    ,++    do impl1 <- [| \ i j -> if C.notNull i Prelude.&& C.notNull j then 1 else 0 |]+       impl2 <- [| \ i j -> if C.notNull i Prelude.|| C.notNull j then 1 else 0 |]+       withInstanceProofs+         [ genBinaryInstances ''C.Logical ( Left $ TH.ConT ''CInt ) ( C.binaryLogicalType platform )+           [ ClassMethod '(C.&&) "singAnd" 2 impl1+           , ClassMethod '(C.||) "singOr"  2 impl2+           ]+         ]+    ,++    ----------------------------------------------------------------------------+    -- RelEq, RelOrd++    do impl1 <- [| \ a b -> if a Prelude.== b then 1 else 0 |]+       impl2 <- [| \ a b -> if a Prelude./= b then 1 else 0 |]+       withInstanceProofs+         [ genBinaryInstances ''C.RelEq ( Left $ TH.ConT ''CInt ) ( C.binaryEqType platform )+           [ ClassMethod '(C.==) "singEq"  2 impl1+           , ClassMethod '(C.!=) "singNEq" 2 impl2+           ]+         ]+    ,++    do impl1 <- [| \ a b -> if a Prelude.>  b then 1 else 0 |]+       impl2 <- [| \ a b -> if a Prelude.>= b then 1 else 0 |]+       impl3 <- [| \ a b -> if a Prelude.<  b then 1 else 0 |]+       impl4 <- [| \ a b -> if a Prelude.<= b then 1 else 0 |]+       withInstanceProofs+         [ genBinaryInstances ''C.RelOrd ( Left $ TH.ConT ''CInt ) ( C.binaryRelType platform )+           [ ClassMethod '(C.>)  "singGT" 2 impl1+           , ClassMethod '(C.>=) "singGTE" 2 impl2+           , ClassMethod '(C.<)  "singLT" 2 impl3+           , ClassMethod '(C.<=) "singLTE" 2 impl4+           ]+         ]+    ,++    ----------------------------------------------------------------------------+    -- Plus, Minus++    withInstanceProofs+      [ genUnaryInstances ''C.Plus ( withAssoc "PlusRes" "PlusResImpl" SameArgs )+        ( C.unaryPlusType platform )+        [ ClassMethod 'C.plus "singPlus" 1 ( TH.VarE 'Prelude.id ) ]+      ]+    ,++    genUnaryTyFam platform ( TH.mkName "PlusResImpl" ) C.unaryPlusType+    ,++    withInstanceProofs+      [ genUnaryInstances ''C.Minus ( withAssoc "MinusRes" "MinusResImpl" SameArgs )+        ( C.unaryMinusType platform )+        [ ClassMethod 'C.negate "singNegate" 1 ( TH.VarE 'Prelude.negate ) ]+      ]+    ,++    genUnaryTyFam platform ( TH.mkName "MinusResImpl" ) C.unaryMinusType+    ,++    ----------------------------------------------------------------------------+    -- Add, Sub, Mult, Div, Rem++    withInstanceProofs+      [ genBinaryInstances ''C.Add ( withAssoc "AddRes" "AddResImpl" SameArgs )+        ( C.binaryAddType platform )+        [ ClassMethod '(C.+) "singAdd" 2 ( TH.VarE '(Prelude.+) ) ]+      ]+    ,++    genBinaryTyFam platform ( TH.mkName "AddResImpl" ) C.binaryAddType+    ,++    withInstanceProofs+      [ genBinaryInstances ''C.Sub ( withAssoc "SubRes" "SubResImpl" SameArgs )+        ( C.binarySubType platform )+        [ ClassMethod '(C.-) "singSub" 2 ( TH.VarE '(Prelude.-) ) ]+      ]+    ,++    genBinaryTyFam platform ( TH.mkName "SubResImpl" ) C.binarySubType+    ,++    withInstanceProofs+      [ genBinaryInstances ''C.Mult ( withAssoc "MultRes" "MultResImpl" SameArgs )+        ( C.binaryMultiplicativeType platform )+        [ ClassMethod '(C.*) "singMult" 2 ( TH.VarE '(Prelude.*) ) ]+      ]+    ,++    genBinaryTyFam platform ( TH.mkName "MultResImpl" ) C.binaryMultiplicativeType+    ,++    -- NB: this is the key usage of 'withInstanceProofs' with a non-singleton list+    withInstanceProofs+        -- division for integral types+      [ genBinaryInstances ''C.Div ( withAssoc "DivRes" "MultResImpl" SameArgs ) -- NB: re-use 'MultResImpl'+          ( \ a b ->+            do op@( resTy, _ ) <- C.integralBinaryType platform a b+               guard ( case resTy of C.Arithmetic ( C.FloatLike {} ) -> False; _ -> True )+               return op+          )+          [ ClassMethod '(C./) "singDiv" 2 ( TH.VarE 'Prelude.div ) ]+        -- division for floating-point types+      , genBinaryInstances ''C.Div ( withAssoc "DivRes" "MultResImpl" SameArgs ) -- NB: re-use 'MultResImpl'+          ( \ a b ->+            do op@( resTy, _ ) <- C.binaryMultiplicativeType platform a b+               guard ( case resTy of C.Arithmetic ( C.FloatLike {} ) -> True; _ -> False )+               return op+          )+          [ ClassMethod '(C./) "singDiv" 2 ( TH.VarE '(Prelude./) ) ]+      ]+    ,++    withInstanceProofs+      [ genBinaryInstances ''C.Rem ( withAssoc "RemRes" "BinResImpl" SameArgs ) -- NB: use 'BinResImpl'+        ( C.integralBinaryType platform )+        [ ClassMethod '(C.%) "singRem" 2 ( TH.VarE 'Prelude.rem ) ]+      ]+    ,++    genBinaryTyFam platform ( TH.mkName "BinResImpl" ) C.integralBinaryType+    ,++    ----------------------------------------------------------------------------+    -- Complement, Bitwise, Shift++    withInstanceProofs+      [ genUnaryInstances ''C.Complement ( withAssoc "ComplementRes" "ComplementResImpl" SameArgs )+        ( C.integralUnaryType platform )+        [ ClassMethod '(C..~) "singComplement" 1 ( TH.VarE 'Bits.complement ) ]+      ]+    ,++    genUnaryTyFam platform ( TH.mkName "ComplementResImpl" ) C.integralUnaryType+    ,++    withInstanceProofs+      [ genBinaryInstances ''C.Bitwise ( withAssoc "BitsRes" "BinResImpl" SameArgs ) -- NB: use 'BinResImpl'+        ( C.integralBinaryType platform )+          [ ClassMethod '(C..&.) "singBitAnd" 2 ( TH.VarE '(Bits..&.) )+          , ClassMethod '(C..|.) "singBitOr" 2 ( TH.VarE '(Bits..|.) )+          , ClassMethod '(C..^.) "singBitXor" 2 ( TH.VarE 'Bits.xor )+          ]+      ]+    ,++    do impl1 <- [| \ a i -> Bits.shiftL a ( Prelude.fromIntegral i ) |]+       impl2 <- [| \ a i -> Bits.shiftR a ( Prelude.fromIntegral i ) |]+       withInstanceProofs+         [ genBinaryInstances ''C.Shift ( withAssoc "ShiftRes" "ShiftResImpl" FirstArgOnly )+              -- NB: use 'FirstArgOnly', because the result type only depends on the+              -- first argument.+             ( C.shiftType platform )+             [ ClassMethod '(C.<<) "singShiftL" 2 impl1+             , ClassMethod '(C.>>) "singShiftR" 2 impl2+             ]+         ]+    ,++    genUnaryTyFam platform ( TH.mkName "ShiftResImpl" ) $+      -- The associated type family for Shift is unary, as the result type+      -- only depends on the shiftee type, not the type of the shift amount,+      -- which undergoes an independent arithmetic promotion.+      \ plat ty -> C.shiftType plat ty ( C.Arithmetic $ C.Integral $ C.IntLike $ C.Int C.Signed )+++    ]++--------------------------------------------------------------------------------++-- | Utility function to construct a 'C.Operator.TH.AssocTyFam' argument to pass+-- to 'genUnaryInstances' or 'genBinaryInstances'.+withAssoc :: String -> String -> AssocTyFamArgs -> Either TH.Type AssocTyFam+withAssoc famName implName args =+  Right $+    AssocTyFam+      { assocTyFamName     = TH.mkName famName+      , assocTyFamImplName = TH.mkName implName+      , assocTyFamArgs     = args+      }
+ core/C/Operator/Internal.hs view
@@ -0,0 +1,462 @@+{-# LANGUAGE ScopedTypeVariables #-}++module C.Operator.Internal where++import Control.Arrow (first, second, (***))+import Control.Exception (assert)+import Data.Kind qualified as Hs+import Data.Nat (Nat (..))+import Data.Vec.Lazy (Vec (..))+import Data.Void qualified as Absurd+import GHC.Generics (Generic)++import C.Type++--------------------------------------------------------------------------------++-- | __Internal implementation detail__+--+-- How is a C operator, when instantiated at a particular type, implemented?+type OpImpl :: Nat -> Hs.Type+data OpImpl n+  -- | Convert arguments with the given conversions and then apply+  -- the implied function (e.g. addition for the 'C.Operator.Classes.Add'+  -- class) at the resulting type.+  = ConvertThenOp+  { argumentConversions :: !( Vec n [ Conversion ] ) }+  -- | Add an integral value and a pointer.+  | AddIntegralAndPtr+  -- | Add a pointer and an integral value.+  | AddPtrAndIntegral+  -- | Get the difference between two pointers.+  | SubPtrAndPtr+  -- | Subtract an integral value from a pointer.+  | SubPtrAndIntegral+  deriving stock ( Show, Generic )++data Conversion+  = FromIntegralTo { fromIntegralTo :: !( Type Absurd.Void ) }+  | RealToFracTo   { realToFracTo   :: !( Type Absurd.Void ) }+  | PtrToInt+  deriving stock ( Show, Generic )++--------------------------------------------------------------------------------++type Op :: Nat -> Hs.Type+data Op arity where+  UnaryOp  :: UnaryOp -> Op ( S Z )+  BinaryOp :: BinaryOp -> Op ( S ( S Z ) )++data UnaryOp+  -- | @+@+  = UnaryPlus+  -- | @-@+  | UnaryMinus+  -- | @!@+  | LogicalNot+  -- | @~@+  | BitwiseNot+  deriving stock ( Eq, Ord, Show, Enum, Bounded )++data BinaryOp+  -- | @*@+  = Mult+  -- | @/@+  | Div+  -- | @%@+  | Rem+  -- | @+@+  | Add+  -- | @-@+  | Sub+  -- | @<<@+  | ShiftLeft+  -- | @>>@+  | ShiftRight+  -- | @<@+  | RelLT+  -- | @<=@+  | RelLE+  -- | @>@+  | RelGT+  -- | @>=@+  | RelGE+  -- | @==@+  | RelEQ+  -- | @!=@+  | RelNE+  -- | @&@+  | BitwiseAnd+  -- | @^@+  | BitwiseXor+  -- | @|@+  | BitwiseOr+  -- | @&&@+  | LogicalAnd+  -- | @||@+  | LogicalOr+  deriving stock ( Eq, Ord, Show, Enum, Bounded )++pprOp :: Op arity -> String+pprOp = \case+  UnaryOp op ->+    case op of+      UnaryPlus  -> "+"+      UnaryMinus -> "-"+      LogicalNot -> "!"+      BitwiseNot -> "~"+  BinaryOp op ->+    case op of+      Mult       -> "*"+      Div        -> "/"+      Rem        -> "%"+      Add        -> "+"+      Sub        -> "-"+      ShiftLeft  -> "<<"+      ShiftRight -> ">>"+      RelLT      -> "<"+      RelLE      -> "<="+      RelGT      -> ">"+      RelGE      -> ">="+      RelEQ      -> "=="+      RelNE      -> "!="+      BitwiseAnd -> "&"+      BitwiseXor -> "^"+      BitwiseOr  -> "|"+      LogicalAnd -> "&&"+      LogicalOr  -> "||"++pprOpApp :: forall arity. Op arity -> Vec arity String -> String+pprOpApp op args =+  case op of+    UnaryOp  {} -> unary+    BinaryOp {} -> binary+  where+    unary :: arity ~ S Z => String+    unary =+      case args of+        a ::: VNil ->+          pprOp op ++ a+    binary :: arity ~ S ( S Z ) => String+    binary =+      case args of+        a ::: b ::: VNil ->+          a ++ pprOp op ++ b++--------------------------------------------------------------------------------++opResTypeAndImpl :: forall arity a. Eq a => Platform -> Op arity -> Vec arity ( Type a ) -> Maybe ( Type a, OpImpl arity )+opResTypeAndImpl plat op args =+  case op of+    UnaryOp o ->+      case o of+        UnaryPlus  -> unary unaryPlusType+        UnaryMinus -> unary unaryMinusType+        LogicalNot -> unary unaryLogicalType+        BitwiseNot -> unary integralUnaryType+    BinaryOp o ->+      case o of+        Mult       -> binary binaryMultiplicativeType+        Div        -> binary binaryMultiplicativeType+        Rem        -> binary integralBinaryType+        Add        -> binary binaryAddType+        Sub        -> binary binarySubType+        ShiftLeft  -> binary shiftType+        ShiftRight -> binary shiftType+        RelLT      -> binary binaryRelType+        RelLE      -> binary binaryRelType+        RelGT      -> binary binaryRelType+        RelGE      -> binary binaryRelType+        RelEQ      -> binary binaryEqType+        RelNE      -> binary binaryEqType+        BitwiseAnd -> binary integralBinaryType+        BitwiseXor -> binary integralBinaryType+        BitwiseOr  -> binary integralBinaryType+        LogicalAnd -> binary binaryLogicalType+        LogicalOr  -> binary binaryLogicalType+  where+    unary :: arity ~ S Z => ( Platform -> Type a -> Maybe r ) -> Maybe r+    unary f =+      case args of+        a ::: VNil ->+          f plat a+    binary :: arity ~ S ( S Z ) => ( Platform -> Type a -> Type a -> Maybe r ) -> Maybe r+    binary f =+      case args of+        a ::: b ::: VNil ->+          f plat a b++--------------------------------------------------------------------------------++-- | Result type of unary @+@+unaryPlusType :: Platform -> Type a -> Maybe ( Type a, OpImpl ( S Z ) )+unaryPlusType plat = \case+  Arithmetic ty ->+    Just $ mkArithConv1 $ arithmeticPromotion plat ty+  Ptr {} ->+    -- The C++ standard allows unary plus on pointers, but the C standard doesn't.+    Nothing+  Void -> Nothing++-- | Result type of unary @-@+unaryMinusType :: Platform -> Type a -> Maybe ( Type a, OpImpl ( S Z ) )+unaryMinusType plat = \case+  Arithmetic ty ->+    Just $ mkArithConv1 $ arithmeticPromotion plat ty+  Ptr {} -> Nothing+  Void   -> Nothing++-- | Result type of binary @+@+binaryAddType :: Platform -> Type a -> Type a -> Maybe ( Type a, OpImpl ( S ( S Z ) ) )+binaryAddType plat ( Arithmetic a1 ) ( Arithmetic a2 )+  = Just $ mkArithConv2 $ arithmeticConversion plat a1 a2+binaryAddType _ ( Arithmetic ( Integral {} ) ) ptr@( Ptr {} )+  = Just ( ptr, AddIntegralAndPtr )+binaryAddType _ ptr@( Ptr {} ) ( Arithmetic ( Integral {} ) )+  = Just ( ptr, AddPtrAndIntegral )+binaryAddType _ _ _+  = Nothing++-- | Result type of binary @-@+binarySubType :: Eq a => Platform -> Type a -> Type a -> Maybe ( Type a, OpImpl ( S ( S Z ) ) )+binarySubType plat ( Arithmetic a1 ) ( Arithmetic a2 )+  = Just $ mkArithConv2 $ arithmeticConversion plat a1 a2+binarySubType _ ptr@( Ptr {} ) ( Arithmetic ( Integral {} ) )+  = Just ( ptr, SubPtrAndIntegral )+binarySubType _ ( Ptr ty1 ) ( Ptr ty2 )+  | ty1 == ty2+  -- TODO <https://github.com/well-typed/c-expr/issues/31>+  --+  -- Do we want to be more lenient in allowing subtraction of pointers with+  -- different pointee types, e.g. allow @(x :: Ptr Void) - (y :: Ptr Int)@?+  = Just ( Arithmetic $ Integral $ IntLike PtrDiff, SubPtrAndPtr )+binarySubType _ _ _+  = Nothing+++-- | Result type for multiplication and division (integral and floating-point)+binaryMultiplicativeType :: Platform -> Type a -> Type a -> Maybe ( Type a, OpImpl ( S ( S Z ) ) )+binaryMultiplicativeType plat ( Arithmetic a1 ) ( Arithmetic a2 )+  = Just $ mkArithConv2 $ arithmeticConversion plat a1 a2+binaryMultiplicativeType _ _ _ = Nothing++-- | Result type for bitwise not operator+integralUnaryType :: Platform -> Type a -> Maybe ( Type a, OpImpl ( S Z ) )+integralUnaryType plat ( Arithmetic a1 )+  | Integral {} <- a1+  = Just $ mkArithConv1 $ arithmeticPromotion plat a1+integralUnaryType _ _ = Nothing++-- | Type for integral remainder and binary bitwise logic operators+integralBinaryType :: Platform -> Type a -> Type a -> Maybe ( Type a, OpImpl ( S ( S Z ) ) )+integralBinaryType plat ( Arithmetic a1 ) ( Arithmetic a2 )+  | Integral {} <- a1+  , Integral {} <- a2+  = Just $ mkArithConv2 $ arithmeticConversion plat a1 a2+integralBinaryType _ _ _ = Nothing++-- | Type for binary shift operators+shiftType :: Platform+          -> Type a -- ^ type of the value being shifted+          -> Type a -- ^ type of the shift amount+          -> Maybe ( Type a, OpImpl ( S ( S Z ) ) )+shiftType plat ( Arithmetic a1@( Integral {} ) ) ( Arithmetic a2@( Integral {} ) )+  = let ( i1, c1 ) = arithmeticPromotion plat a1+        ( _ , c2 ) = arithmeticPromotion plat a2+    in Just ( Arithmetic i1, ConvertThenOp ( c1 ::: c2 ::: VNil ) )+shiftType _ _ _+  = Nothing++intType, uintType :: Type a+intType  = Arithmetic $ Integral $ IntLike $ Int Signed+uintType = Arithmetic $ Integral $ IntLike $ Int Unsigned++convertToInt :: Platform -> Type a -> Maybe [ Conversion ]+convertToInt _ = \case+  Arithmetic a -> Just $ case a of+    Integral i ->+      case i of+        IntLike ( Int Signed ) -> []+        _ -> [ FromIntegralTo intType ]+    FloatLike {} ->+      [ RealToFracTo intType ]+  Ptr {}        ->+    Just [ PtrToInt ]+  _             ->+    Nothing++-- | Type for logical not operation @!@.+unaryLogicalType :: Platform -> Type a -> Maybe ( Type a, OpImpl ( S Z ) )+unaryLogicalType plat a = do+  _conv <- convertToInt plat a+  return $ ( intType, ConvertThenOp ( [] ::: VNil ) )++-- | Type for binary equality operators @==@ and @!=@.+binaryEqType :: Eq a => Platform -> Type a -> Type a -> Maybe ( Type a, OpImpl ( S ( S Z ) ) )+binaryEqType plat ( Arithmetic a1 ) ( Arithmetic a2 )+  = Just $ mkArithConv2 ( Integral $ IntLike $ Int Signed, snd $ arithmeticConversion plat a1 a2 )+binaryEqType _ ( Ptr ty1 ) ( Ptr ty2 )+  | ty1 == ty2+  -- TODO <https://github.com/well-typed/c-expr/issues/29>+  --+  -- The C Standard is more permissive than we are.+  = Just ( intType, ConvertThenOp ( [] ::: [] ::: VNil ) )+binaryEqType _ _ _ = Nothing++-- | Type for binary logical operators @&&@ and @||@.+binaryLogicalType :: Platform -> Type a -> Type a -> Maybe ( Type a, OpImpl ( S ( S Z ) ) )+binaryLogicalType plat a1 a2 = do+  _c1 <- convertToInt plat a1+  _c2 <- convertToInt plat a2+  return ( intType, ConvertThenOp ( [] ::: [] ::: VNil ) )++-- | Type for binary comparison operators @<@, @<=@, @>@, @>=@.+binaryRelType :: Eq a => Platform -> Type a -> Type a -> Maybe ( Type a, OpImpl ( S ( S Z ) ) )+binaryRelType plat ( Arithmetic a1 ) ( Arithmetic a2 )+  = Just $ mkArithConv2 ( Integral $ IntLike $ Int Signed, snd $ arithmeticConversion plat a1 a2 )+binaryRelType _ ( Ptr ty1 ) ( Ptr ty2 )+  | ty1 == ty2+  -- TODO <https://github.com/well-typed/c-expr/issues/30>+  --+  -- C is a bit more lenient than requiring the inner types to match exactly.+  = Just ( intType, ConvertThenOp ( [] ::: [] ::: VNil ) )+binaryRelType _ _ _ = Nothing++mkArithConv1 :: ( ArithmeticType, [ Conversion ] ) -> ( Type a, OpImpl ( S Z ) )+mkArithConv1 =+  ( Arithmetic *** ( \ a -> ConvertThenOp ( a ::: VNil ) ) )++mkArithConv2 :: ( ArithmeticType, ( [ Conversion ], [ Conversion ] ) ) -> ( Type a, OpImpl ( S ( S Z ) ) )+mkArithConv2 =+  ( Arithmetic *** ( \ ( a, b ) -> ConvertThenOp ( a ::: b ::: VNil ) ) )++--------------------------------------------------------------------------------++arithmeticPromotion :: Platform -> ArithmeticType -> ( ArithmeticType, [ Conversion ] )+arithmeticPromotion _ f@( FloatLike {} ) =+  ( f, [] )+arithmeticPromotion plat ( Integral i ) =+  first ( Integral . IntLike ) $ integralPromotion plat i++integralPromotion :: Platform -> IntegralType -> ( IntLikeType, [ Conversion ] )+  -- C standard: Promotion from integral types (non bit-field case).+  --+  -- If the integer conversion rank of T is lower than that of int:+  --+  --   1. promote T to int if int can represent all the values of T,+  --   2. otherwise promote T to unsigned int+integralPromotion plat ( IntLike i )+  | intLikeTypeConversionRank plat i < intLikeTypeConversionRank plat ( Int Signed )+  = if intLikeTypeFitsInInt plat i+    then ( Int Signed  , [ FromIntegralTo intType  ] )+    else ( Int Unsigned, [ FromIntegralTo uintType ] )+  | otherwise+  = ( i, [ ] )+integralPromotion plat ( CharLike c )+  = assert ( charLikeTypeSizeInBits plat c < intLikeTypeSizeInBits plat ( Int Signed ) )+    ( Int Signed, [ FromIntegralTo intType ] )+integralPromotion _ Bool+  = ( Int Signed, [ FromIntegralTo intType ] )++--------------------------------------------------------------------------------+-- Arithmetic conversion++arithmeticConversion :: Platform -> ArithmeticType -> ArithmeticType -> ( ArithmeticType, ( [ Conversion ], [ Conversion ] ) )+arithmeticConversion plat ( Integral i1 ) ( Integral i2 )+  -- Both arguments are integral: do integral promotion then integral conversion.+  = let+      ( j1, c1 ) = integralPromotion plat i1+      ( j2, c2 ) = integralPromotion plat i2+      ( r, ( d1, d2 ) ) = integralArithmeticConversion plat j1 j2+    in ( Integral $ IntLike r, ( c1 ++ d1, c2 ++ d2 ) )++-- At least one of the arguments is of floating-point type:+-- pick the largest floating-point type.+arithmeticConversion _ ( FloatLike f1 )  ( FloatLike f2 ) =+  ( FloatLike ( max f1 f2 ), ( if f2 > f1 then [ rf f2 ] else [], if f1 > f2 then [ rf f1 ] else [] ) )+    where+      rf f = RealToFracTo $ Arithmetic $ FloatLike f+arithmeticConversion _ f@( FloatLike {} ) ( Integral {} ) =+  ( f, ( [], [ FromIntegralTo ( Arithmetic f ) ] ) )+arithmeticConversion _ ( Integral {} ) f@( FloatLike {} ) =+  ( f, ( [ FromIntegralTo ( Arithmetic f ) ], [] ) )++integralArithmeticConversion :: Platform -> IntLikeType -> IntLikeType -> ( IntLikeType, ( [ Conversion ], [ Conversion ] ) )+integralArithmeticConversion plat t1 t2+  -- The following rules are applied to determine the arithmetic conversion result type 'C':+  --+  --   1. If 'T1' and 'T2' are the same type, 'C' is that type.+  | t1 == t2+  = ( t1, ( [], [] ) )+  --   2. If T1 and T2 are both signed integer types or both unsigned integer types,+  --      C is the type of greater integer conversion rank.+  | s1 == s2+  = if rk1 >= rk2+    then ( t1, ( [], [ FromIntegralTo ( Arithmetic $ Integral $ IntLike t1 ) ] ) )+    else ( t2, ( [ FromIntegralTo ( Arithmetic $ Integral $ IntLike t2 ) ], [] ) )+  | otherwise+  --   3. Otherwise, the types are of different signs.+  --      Implement the logic in 'integralArithmeticConversion_differentSigns'.+  = case s1 of+      Signed ->+        integralArithmeticConversion_differentSigns plat ( t1, rk1 ) ( t2, rk2 )+      Unsigned ->+        second ( \ ( c1, c2 ) -> ( c2, c1 ) ) $+          integralArithmeticConversion_differentSigns plat ( t2, rk2 ) ( t1, rk1 )+  where+    s1, s2 :: Sign+    s1 = intLikeTypeSign t1+    s2 = intLikeTypeSign t2+    rk1, rk2 :: IntegerConversionRank+    rk1 = intLikeTypeConversionRank plat t1+    rk2 = intLikeTypeConversionRank plat t2+++integralArithmeticConversion_differentSigns+  :: Platform+  -> ( IntLikeType, IntegerConversionRank ) -- ^ the signed type+  -> ( IntLikeType, IntegerConversionRank ) -- ^ the unsigned type+  -> ( IntLikeType, ( [ Conversion ], [ Conversion ] ) )+integralArithmeticConversion_differentSigns plat s@( t_s, rk_s ) u@( t_u, rk_u )+  -- Implement the following rules to determine the arithmetic conversion+  -- result type C for signed type S and unsigned type U:+  --+  --   1. If the rank of U is greater than or equal to the rank of S, C is U.+  | rk_u >= rk_s+  = ( t_u, ( [ FromIntegralTo ( Arithmetic $ Integral $ IntLike t_u ) ], [] ) )+  -- Otherwise, S has (strictly) greater rank than U.+  --+  --   2. If S can represent all of the values of U, C is S.+  | unsignedFitsInSigned plat t_u t_s+  = ( t_s, ( [], [ FromIntegralTo ( Arithmetic $ Integral $ IntLike t_s ) ] ) )+  --   3. Otherwise, C is the unsigned integer type corresponding to S.+  | otherwise+  = ( \ iTy ->+      let ty = Arithmetic $ Integral $ IntLike iTy+      in ( iTy , ( [ FromIntegralTo ty ], [ FromIntegralTo ty ] ) )+    ) $+     case t_s of+      Short    {} -> Short    Unsigned+      Int      {} -> Int      Unsigned+      Long     {} -> Long     Unsigned+      LongLong {} -> LongLong Unsigned+      _ ->+        -- Should never happen, because any unsigned type of rank strictly+        -- less than that of ptrdiff_t fits into ptrdiff_t.+        error $ unlines+          [ "integralArithmeticConversion_differentSigns: extended type"+          , "ty: " ++ show t_s+          , "s: " ++ show s+          , "u: " ++ show u+          ]++-- | Does the given unsigned type fit into the given signed type?+unsignedFitsInSigned+  :: Platform+  -> IntLikeType -- ^ the unsigned type+  -> IntLikeType -- ^ the signed type+  -> Bool+unsignedFitsInSigned plat u s =+  intLikeTypeSizeInBits plat s > intLikeTypeSizeInBits plat u++--------------------------------------------------------------------------------
+ core/C/Operator/TH.hs view
@@ -0,0 +1,614 @@+{-# LANGUAGE CPP #-}++{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TemplateHaskellQuotes #-}+{-# LANGUAGE ViewPatterns #-}++{-# LANGUAGE BangPatterns #-}++module C.Operator.TH+  (++  -- * Generating type family declarations+    genTyFam, genUnaryTyFam, genBinaryTyFam++  -- * Generating class instances+  , ClassMethod(..)+  , genUnaryInstances, genBinaryInstances+  , genClassInstances, genInstance+  , AssocTyFam(..), AssocTyFamArgs(..)++  -- * Generating proofs+  , withInstanceProofs++  ) where++-- base+import Data.Foldable+  ( toList+#if !MIN_VERSION_base(4,20,0)+  , foldl'+#endif+  )+import Data.Function+  ( on )+import Data.Kind qualified as Hs+import Data.List+  ( sortOn )+import Data.List.NonEmpty+  ( groupBy )++import qualified Data.List.NonEmpty as NE+import Data.Maybe+  ( fromJust, maybeToList, mapMaybe )+import Data.Proxy+  ( Proxy(..) )+import Data.Type.Equality+  ( type (:~:)(Refl) )+import Data.Void+  ( absurd )+import Foreign+  ( Ptr, plusPtr, minusPtr )+import Foreign.C+import qualified GHC.Exts as Foreign.C+  ( Ptr(Ptr) )+import GHC.Exts+  ( Int(I#), addr2Int# )++-- containers+import Data.Map.Strict qualified as Map++-- fin+import Data.Type.Nat qualified as Fin+import Data.Type.Nat+  ( Nat(..) )++-- some+import Data.GADT.Compare+  ( GEq(geq) )++-- template-haskell+import Language.Haskell.TH qualified as TH++-- vec+import Data.Vec.Lazy+  ( Vec(..) )+import Data.Vec.Lazy qualified as Vec++-- c-expr+import C.Type+import C.Type.Internal.Universe+import C.Operator.Internal+  ( OpImpl(..), Conversion(..) )++--------------------------------------------------------------------------------+-- Type families++-- | Generate a unary closed type family with the equations ranging over+-- all types, with the RHS being given by the given function.+--+-- If the function returns 'Nothing', that particular type family equation+-- is omitted.+genUnaryTyFam+  :: Platform+  -> TH.Name -- ^ type family name+  -> ( Platform -> Type TH.Name -> Maybe ( Type TH.Name, details ) )+      -- ^ function implementing the type family reduction rules+  -> TH.Q [ TH.Dec ]+genUnaryTyFam platform fam f = genTyFam @( S Z ) platform fam g+  where+    g :: Platform -> Vec ( S Z ) ( Type TH.Name ) -> Maybe ( Type TH.Name )+    g p ( a ::: VNil ) = fst <$> f p a++-- | Generate a binary closed type family with the equations ranging over+-- all pairs of types, with the RHS being given by the given function.+--+-- If the function returns 'Nothing', that particular type family equation+-- is omitted.+genBinaryTyFam+  :: Platform+  -> TH.Name -- ^ type family name+  -> ( Platform -> Type TH.Name -> Type TH.Name -> Maybe ( Type TH.Name, details ) )+      -- ^ function implementing the type family reduction rules+  -> TH.Q [ TH.Dec ]+genBinaryTyFam platform fam f = genTyFam @( S ( S Z ) ) platform fam g+  where+    g :: Platform -> Vec ( S ( S Z ) ) ( Type TH.Name ) -> Maybe ( Type TH.Name )+    g p ( a ::: b ::: VNil ) = fst <$> f p a b++-- | Generate a closed type family with the equations ranging over+-- all @n@-tuples of types, with the RHS being given by the given function.+--+-- If the function returns 'Nothing', that particular type family equation+-- is omitted.+genTyFam+  :: forall n+  .  Fin.SNatI n+  => Platform+  -> TH.Name -- ^ type family name+  -> ( Platform -> Vec n ( Type TH.Name ) -> Maybe ( Type TH.Name ) )+      -- ^ function implementing the type family reduction rules+  -> TH.Q [ TH.Dec ]+genTyFam platform famName impl = do+  let hsTy :: TH.Type+      hsTy = TH.ConT ''Hs.Type+      n :: Int+      n = Fin.reflectToNum @n Proxy+      args = fmap TH.mkName $ fromJust $ Vec.fromListPrefix @n [ "t" ++ show i | i <- [(1 :: Int)..]]++      kiSig, famDecl :: TH.Dec+      kiSig =+        TH.KiSigD famName ( foldr ( \ arg acc -> TH.AppT ( TH.AppT TH.ArrowT arg ) acc ) hsTy ( replicate n hsTy ) )+      famDecl =+        TH.ClosedTypeFamilyD+          ( TH.TypeFamilyHead famName+              [ TH.PlainTV+                  a+#if MIN_VERSION_template_haskell(2,21,0)+                  TH.BndrReq+#else+                  ()+#endif+              | a <- toList args+              ]+              TH.NoSig+              Nothing+          )+          ( mkTyFamEqs famName ( impl platform ) )++  return+    [ kiSig, famDecl ]++-- | Generate the equations of a closed type family, with the RHS of each+-- equation being given by the given function.+--+-- If the function returns 'Nothing', that particular type family equation+-- is omitted.+mkTyFamEqs+  :: forall n+  .  Fin.SNatI n+  => TH.Name -- ^ type family name+  -> ( Vec n ( Type TH.Name ) -> Maybe ( Type TH.Name ) )+      -- ^ function implementing the type family reduction rules+  -> [ TH.TySynEqn ]+mkTyFamEqs fam impl =+  [ TH.TySynEqn Nothing ( foldl' TH.AppT ( TH.ConT fam ) ( fmap mkType args ) ) ( mkType res )+  | ( args :: Vec n ( Type a ) ) <- map mkNames $ enumerateTypeTuples @n+  , res <- maybeToList $ impl args+  ]++--------------------------------------------------------------------------------+-- Class instances++-- | Information needed to generate a class instance (of the form we need+-- for the @c-expr@ library) with Template Haskell.+data ClassInstance+  = ClassInstance+  { className      :: !TH.Name+  , instanceTys    :: ![ TH.Type ]+  , classMethods   :: ![ ClassMethod ]+  }+  deriving stock Show++-- | Information needed to generate the methods in a class instance for the+-- @c-expr@ library, using Template Haskell.+data ClassMethod+  = ClassMethod+  { methodName   :: !TH.Name+  , proveName    :: !String+  , methodNbArgs :: !Int+  , methodFn     :: !TH.Exp+  }+  deriving stock Show++-- | Information needed to generate associated type family instances for+-- the @c-expr@ library, using Template Haskell.+data AssocTyFam+  = AssocTyFam+      { assocTyFamName :: !TH.Name+      , assocTyFamArgs :: !AssocTyFamArgs+      , assocTyFamImplName :: !TH.Name+      }++-- | Information about the arity/arguments of an associated type family.+data AssocTyFamArgs+  -- | The associated type family has the same arguments as the class.+  = SameArgs+  -- | The associated type family has a single argument, which is the same+  -- as the first argument of the class.+  | FirstArgOnly+++-- | Generate TH declarations for a collection of instances of a unary class,+-- where the argument ranges over all supported types.+genUnaryInstances+  :: TH.Name+     -- ^ class name+  -> Either TH.Type AssocTyFam+     -- ^ result type (either constant, or given by an associated type family)+  -> ( Type TH.Name -> Maybe ( Type TH.Name, OpImpl ( S Z ) ) )+     -- ^ function computing the result type and implementation strategy+  -> [ ClassMethod ]+     -- ^ class methods+  -> TH.Q ( [ TH.Dec ], [ ( TH.Name, ( TH.Type, TH.Clause ) ) ] )+genUnaryInstances cls fam f = genClassInstances @( S Z ) cls fam ( \ ( a ::: VNil ) -> f a )++-- | Generate TH declarations for a collection of instances of a binary class,+-- where the arguments range over pairs of supported types.+genBinaryInstances+  :: TH.Name+     -- ^ class name+  -> Either TH.Type AssocTyFam+     -- ^ result type (either constant, or given by an associated type family)+  -> ( Type TH.Name -> Type TH.Name -> Maybe ( Type TH.Name, OpImpl ( S ( S Z ) ) ) )+     -- ^ function computing the result type and implementation strategy+  -> [ ClassMethod ]+     -- ^ class methods+  -> TH.Q ( [ TH.Dec ], [ ( TH.Name, ( TH.Type, TH.Clause ) ) ] )+genBinaryInstances cls fam f =+  genClassInstances @( S ( S Z ) ) cls fam ( \ ( a ::: b ::: VNil ) -> f a b )++-- | Generate TH declarations for a collection of instances of a class,+-- where the arguments range over all @n@-tuples of supported types.+genClassInstances+  :: forall n+  .  Fin.SNatI n+  => TH.Name+     -- ^ class name+  -> Either TH.Type AssocTyFam+     -- ^ result type (either constant, or given by an associated type family)+  -> ( Vec n ( Type TH.Name ) -> Maybe ( Type TH.Name, OpImpl n ) )+     -- ^ function computing the result type and implementation strategy+  -> [ ClassMethod ]+     -- ^ class methods+  -> TH.Q ( [ TH.Dec ], [ ( TH.Name, ( TH.Type, TH.Clause ) ) ] )+genClassInstances cls fam resTyFn meths = do+  instDecs0 <-+    sequence+      [ ( argTys , ) <$> genInstance cls ( case fam of { Left {} -> Nothing; Right tf -> Just tf } ) argTys resTy opImpl meths+      | argTys <- map mkNames $ enumerateTypeTuples @n+      , ( resTy, opImpl ) <- maybeToList $ resTyFn argTys+      ]+  let instDecs = discardSubsumed instDecs0+      ( insts, singFuns ) = unzip instDecs+  return+    ( insts, map ( \ ( nm, c ) -> ( nm, ( proveType ( Fin.reflectToNum @n Proxy ) fam, c ) ) ) ( concat singFuns ) )++-- | Generate singletons that prove the availability of instances.+--+-- Example: @singAdd :: SType ty1 -> SType ty2 -> (SType (AddRes ty1 ty2), ty1 -> ty2 -> AddRes ty1 ty2)@.+withInstanceProofs :: [ TH.Q ( [ TH.Dec ], [ ( TH.Name, ( TH.Type, TH.Clause ) ) ] ) ] -> TH.Q [ TH.Dec ]+withInstanceProofs inner = do+  ( decs, singFuns ) <- unzip <$> sequence inner+  return $+    concat decs ++ concatMap funDecl ( groupBy ( (==) `on` fst ) $ sortOn fst $ concat singFuns )+  where+    funDecl :: NE.NonEmpty ( TH.Name, ( TH.Type, TH.Clause ) ) -> [ TH.Dec ]+    funDecl ( ( nm, ( ty, c ) ) NE.:| cs ) =+      [ TH.SigD nm ty+      , TH.FunD nm ( c : map ( snd . snd ) cs )+      ]++-- | Discard instances that are subsumed by more general instances, to avoid+-- overlapping instances.+--+-- Example: @instance Add (Ptr ty1) (Ptr ty2)@ is more general+-- than @instance Add (Ptr ty) (Ptr ty)@; discard the latter.+discardSubsumed :: forall n b. Fin.SNatI n => [ ( Vec n ( Type TH.Name ), b ) ] -> [ b ]+discardSubsumed insts = Map.elems $ Map.filterWithKey keepInst allInsts+  where+    allInsts = Map.fromList insts+    keepInst :: Vec n ( Type TH.Name ) -> b -> Bool+    keepInst k _+      -- NB: for simplicity we only handle the n=2 case,+      -- as we don't have any ternary instances.+      | Just Refl <- Fin.eqNat @n @( S ( S Z ) )+      , Ptr ty1 ::: Ptr ty2 ::: VNil <- k+      , ty1 == ty2+      , Map.member ( Ptr ( TH.mkName "ty_1" ) ::: Ptr ( TH.mkName "ty_2" ) ::: VNil ) allInsts+      = False+      | otherwise+      = True++-- | The type of one of the "prove" functions.+--+-- Example:+--+-- @singAdd :: SType rec ty1 -> SType rec ty2 -> ( SType rec ( AddRes ty1 ty2 ), ty1 -> ty2 -> AddRes ty1 ty2 )@+proveType :: Int -> Either TH.Type AssocTyFam -> TH.Type+proveType nbArgs resFam =+  TH.ForallT+    ( map mkTv ( TH.mkName "rec" : tvs ) )+    [ TH.ConT ''GEq `TH.AppT` TH.VarT ( TH.mkName "rec" ) ] $ go 1+  where+    tvs = [ TH.mkName $ "ty_" ++ show j | j <- [ 1 .. nbArgs ] ]+    mkTv tv = TH.PlainTV tv TH.SpecifiedSpec++    mkFunTy [] res = res+    mkFunTy (a:as) res = TH.ArrowT `TH.AppT` a `TH.AppT` (mkFunTy as res)++    resTy =+      case resFam of+        Left ty -> ty+        Right AssocTyFam+          { assocTyFamName = famNm+          , assocTyFamArgs = famArgs+          } -> case famArgs of+            SameArgs     -> foldl' TH.AppT ( TH.ConT famNm ) ( map TH.VarT tvs )+            FirstArgOnly -> ( TH.ConT famNm ) `TH.AppT` ( TH.VarT $ TH.mkName "ty_1" )++    go i+      | i > nbArgs+      = TH.TupleT 2 `TH.AppT` mkSingTy resTy `TH.AppT` ( mkFunTy ( map TH.VarT tvs ) resTy )+      | otherwise+      = TH.ArrowT `TH.AppT` ( mkSingTy $ TH.VarT ( TH.mkName $ "ty_" ++ show i ) ) `TH.AppT` go ( i + 1 )++-- | Generate one TH declaration for a class instance.+genInstance+  :: forall n+  .  TH.Name+     -- ^ class name+  -> Maybe AssocTyFam+     -- ^ optional associated type family definition+  -> Vec n ( Type TH.Name )+     -- ^ class instance argument types+  -> Type TH.Name+     -- ^ result type+  -> OpImpl n+     -- ^ class instance implementation strategy+  -> [ ClassMethod ]+     -- ^ class methods+  -> TH.Q ( TH.Dec, [ ( TH.Name, TH.Clause ) ] )+genInstance cls fam argTys resTy methImpl meths = do+  let clsTy :: TH.Type+      clsTy = mkTcApp cls argTys+      famDecs :: [ TH.Dec ]+      famDecs =+        [ TH.TySynInstD $+            TH.TySynEqn Nothing ( mkTcApp famName args ) ( mkTcApp famImplName args )+        | AssocTyFam+           { assocTyFamName     = famName+           , assocTyFamImplName = famImplName+           , assocTyFamArgs     = assocArgs+           } <- maybeToList fam+        , let args :: [ Type TH.Name ]+              args =+               case assocArgs of+                  SameArgs -> toList argTys+                  FirstArgOnly ->+                    case argTys of+                      VNil -> []+                      ( a ::: _ ) -> [ a ]++        ]+      methDecs :: [ TH.Dec ]+      proveDecs :: [ ( TH.Name, TH.Clause ) ]+      ( methDecs, proveDecs ) = unzip+        -- NB: use scoped type variables in the function, because Template Haskell+        -- doesn't support generating instances with explicit quantification+        -- (https://gitlab.haskell.org/ghc/ghc/-/issues/21794).+        --+        -- We would want:+        --+        -- instance forall ty1 ty2. Sub (Ptr ty1) (Ptr ty2) where+        --   (-) x y = ... @(SubRes (Ptr ty1) (Ptr ty2))+        --+        -- but we instead generate:+        --+        -- instance Sub (Ptr ty1) (Ptr ty2) where+        --   (-) (x :: Ptr ty1) (y :: Ptr ty2) = ... @(SubRes (Ptr ty1) (Ptr ty2))+        [ ( TH.FunD meth [ TH.Clause ( map ( \ ( arg, ty ) -> TH.SigP ( TH.VarP arg ) ( mkType ty ) ) args ) ( TH.NormalB body ) [ ] ]+          , ( proveNm,+                TH.Clause provePats+                  ( case mbProveGuard of+                      Nothing -> TH.NormalB proveRes+                      Just g -> TH.GuardedB [ ( g, proveRes ) ]+                  )+                  []+            )+          )+        | ClassMethod+            { methodName   = meth+            , proveName    = proveStr+            , methodNbArgs = nbArgs+            , methodFn     = fn+            } <- meths+        , let argNms :: [ TH.Name ]+              argNms = map ( TH.mkName . ( "a" ++ ) . show ) [ 1 .. nbArgs ]+              args :: [ ( TH.Name, Type TH.Name ) ]+              args = zip argNms ( toList argTys )++              proveNm = TH.mkName proveStr+              ( provePats, mbProveGuard ) = mkSingPats ( toList argTys )+              proveRes = TH.TupE [ Just ( mkSingExp resTy ), Just $ TH.VarE meth ]++              mkConversions :: [ Conversion ] -> TH.Exp -> TH.Exp+              mkConversions [] e = e+              mkConversions (c1 : cs) e = mkConversions cs ( mkConversion c1 e )+              mkConversion :: Conversion -> TH.Exp -> TH.Exp+              mkConversion c e = ( `TH.AppE` e ) $ case c of+                FromIntegralTo { fromIntegralTo = to } ->+                  TH.VarE 'Prelude.fromIntegral `TH.AppTypeE` TH.WildCardT `TH.AppTypeE` mkType (fmap absurd to)+                RealToFracTo   { realToFracTo   = to } ->+                  TH.VarE 'Prelude.realToFrac `TH.AppTypeE` TH.WildCardT `TH.AppTypeE` mkType (fmap absurd to)+                PtrToInt ->+                  TH.LamE [ TH.ConP 'Foreign.C.Ptr [] [ TH.VarP ( TH.mkName "ptr" ) ] ]+                      ( TH.AppE ( TH.ConE 'I# ) $+                        TH.AppE ( TH.VarE 'addr2Int# ) ( TH.VarE $ TH.mkName "ptr" ) )+              body =+                case methImpl of+                  ConvertThenOp convs ->+                    foldl' TH.AppE fn $+                      zipWith mkConversions ( toList convs ) ( map TH.VarE argNms )+                  AddIntegralAndPtr ->+                    case argNms of+                      [ i, p ] ->+                        TH.VarE 'plusPtr+                            `TH.AppE`+                          ( TH.VarE p )+                            `TH.AppE`+                          ( TH.VarE 'fromIntegral `TH.AppE` TH.VarE i )+                      _ -> error $ "genInstance AddIntegralAndPtr: expected 2 arguments, but got: " ++ show args+                  AddPtrAndIntegral ->+                    case argNms of+                      [ p, i ] ->+                        TH.VarE 'plusPtr+                            `TH.AppE`+                          ( TH.VarE p )+                            `TH.AppE`+                          ( TH.VarE 'fromIntegral `TH.AppE` TH.VarE i )+                      _ -> error $ "genInstance AddPtrAndIntegral: expected 2 arguments, but got: " ++ show args+                  SubPtrAndPtr ->+                    case argNms of+                      [ p1, p2 ] ->+                        ( TH.VarE 'fromIntegral `TH.AppTypeE` TH.WildCardT `TH.AppTypeE` TH.ConT ''CPtrdiff )+                            `TH.AppE`+                          ( TH.VarE 'minusPtr `TH.AppE` TH.VarE p1 `TH.AppE` TH.VarE p2 )+                      _ -> error $ "genInstance SubPtrAndPtr: expected 2 arguments, but got: " ++ show args+                  SubPtrAndIntegral ->+                    case argNms of+                      [ p, i ] ->+                        TH.VarE 'plusPtr+                            `TH.AppE`+                          ( TH.VarE p )+                            `TH.AppE`+                          ( TH.VarE 'fromIntegral `TH.AppE` ( TH.VarE 'Prelude.negate `TH.AppE` TH.VarE i ) )+                      _ -> error $ "genInstance SubPtrAndIntegral: expected 2 arguments, but got: " ++ show args+        ]+      overlap :: Maybe TH.Overlap+      overlap = Nothing+      ctxt :: [ TH.Type ]+      ctxt = [ ]+  return $+    ( TH.InstanceD overlap ctxt clsTy ( famDecs ++ methDecs )+    , proveDecs+    )++--------------------------------------------------------------------------------+-- Util++mkNames :: Vec n ( Type OpaqueTy ) -> Vec n ( Type TH.Name )+mkNames = fmap $ fmap $ \ ( OpaqueTy i ) -> TH.mkName ( "ty_" ++ show i )++mkTcApp :: Foldable f => TH.Name -> f ( Type TH.Name ) -> TH.Type+mkTcApp tc args =+  foldl' ( \ a t -> TH.AppT a ( mkType t ) ) ( TH.ConT tc ) args++mkType :: Type TH.Name -> TH.Type+mkType = \case+  Void -> TH.ConT ''()+  Ptr ty -> TH.AppT ( TH.ConT ''Ptr ) ( TH.VarT ty )+  Arithmetic a ->+    mkArithmeticType a++mkSingTy :: TH.Type -> TH.Type+mkSingTy ty = ( TH.ConT ''SType ) `TH.AppT` TH.VarT ( TH.mkName "rec" ) `TH.AppT` ty++mkSingPats :: [ Type TH.Name ] -> ( [ TH.Pat ], Maybe TH.Guard )+mkSingPats tys = ( map ( mkSingPat . mkOne ) tickedTys, if null guards then Nothing else Just $ TH.PatG guards )+  where+    tickedTys = mkTicked 0 tys+    mkTicked :: Int -> [ Type TH.Name ] -> [ Either ( TH.Name, Int ) ( Type TH.Name ) ]+    mkTicked _ [] = []+    mkTicked i ( Ptr nm : rest ) = Left ( nm, i ) : mkTicked ( i + 1 )rest+    mkTicked i ( ty : rest ) = Right ty : mkTicked i rest+    mkOne ( Left ( nm, i ) ) = Ptr $ mkTickedName nm i+    mkOne ( Right ty ) = ty+    guards = concat $ mapMaybe mkGroup $ groupBy ( (==) `on` fst ) $ mapMaybe oneGuard tickedTys+    mkGroup :: NE.NonEmpty ( TH.Name, Int ) -> Maybe [ TH.Stmt ]+    mkGroup ( _ NE.:| [] ) = Nothing+    mkGroup ( ( nm, i ) NE.:| ( fmap snd -> js ) ) =+      Just+        [ TH.BindS+           ( TH.ConP 'Just [] [ TH.ConP 'Refl [] [] ] )+           ( TH.VarE 'geq `TH.AppE` TH.VarE ( mkTickedName nm i ) `TH.AppE` TH.VarE ( mkTickedName nm j ) )+        | j <- js ]+    mkTickedName nm i = TH.mkName $ show nm ++ replicate i '\''+    oneGuard ( Left ( nm, i ) ) = Just ( nm, i )+    oneGuard _                  = Nothing++mkSingPat :: Type TH.Name -> TH.Pat+mkSingExp :: Type TH.Name -> TH.Exp+( mkSingPat, mkSingExp ) =+  ( go_type TH.VarP ( \ c -> TH.ConP c [] [] ) ( \ c a -> TH.ConP c [] [a] )+  , go_type TH.VarE TH.ConE ( \ c e -> TH.AppE ( TH.ConE c ) e )+  )+  where+    go_type var con conapp = \case+      Void -> con 'SVoid+      Ptr ty -> conapp 'SPtr ( var ty )+      Arithmetic a -> conapp 'SArithmetic $ go_arith a++        where++        go_arith = \case+          Integral i -> conapp 'SIntegral $ go_integral i+          FloatLike f -> conapp 'SFloatLike $ go_floatlike f+        go_integral = \case+          Bool -> con 'SBool+          CharLike c -> conapp 'SCharLike $ go_charlike c+          IntLike i -> conapp 'SIntLike $ go_intlike i+        go_floatlike = \case+          FloatType -> con 'SFloatType+          DoubleType -> con 'SDoubleType+        go_charlike = \case+          Char -> con 'S_Char+          SChar -> con 'S_SChar+          UChar -> con 'S_UChar+        go_intlike = \case+          Short s ->+            case s of+              Signed -> con 'SShort+              Unsigned -> con 'SUShort+          Int s ->+            case s of+              Signed -> con 'SInt+              Unsigned -> con 'SUInt+          Long s ->+            case s of+              Signed -> con 'SLong+              Unsigned -> con 'SULong+          LongLong s ->+            case s of+              Signed -> con 'SLongLong+              Unsigned -> con 'SULongLong+          PtrDiff -> con 'SPtrDiff++mkArithmeticType :: ArithmeticType -> TH.Type+mkArithmeticType ( Integral i ) = mkIntegralType i+mkArithmeticType ( FloatLike f ) =+  TH.ConT $+    case f of+      FloatType  -> ''CFloat+      DoubleType -> ''CDouble++mkIntegralType :: IntegralType -> TH.Type+mkIntegralType = \case+  Bool -> TH.ConT ''CBool+  CharLike c -> TH.ConT $+    case c of+      Char  -> ''CChar+      SChar -> ''CSChar+      UChar -> ''CUChar+  IntLike i ->+    mkIntLikeType i++mkIntLikeType :: IntLikeType -> TH.Type+mkIntLikeType = TH.ConT . \case+  Short    s ->+    case s of+      Signed   -> ''CShort+      Unsigned -> ''CUShort+  Int      s ->+    case s of+      Signed   -> ''CInt+      Unsigned -> ''CUInt+  Long     s ->+    case s of+      Signed   -> ''CLong+      Unsigned -> ''CULong+  LongLong s ->+    case s of+      Signed   -> ''CLLong+      Unsigned -> ''CULLong+  PtrDiff -> ''CPtrdiff
+ core/C/Operators.hs view
@@ -0,0 +1,26 @@+module C.Operators+  ( -- * C operators and their types+    Op(..), UnaryOp(..), BinaryOp(..)+  , pprOp, pprOpApp+  , opResType++  ) where++import Data.Vec.Lazy++import C.Type++import C.Operator.Internal+++--------------------------------------------------------------------------------++-- | Compute the result type of a C operator applied to+-- arguments of the given types.+opResType :: Eq a+          => Platform+          -> Op arity             -- ^ C operator+          -> Vec arity ( Type a ) -- ^ types of its arguments+          -> Maybe ( Type a )+opResType plat op args =+  fst <$> opResTypeAndImpl plat op args
+ core/C/Type.hs view
@@ -0,0 +1,540 @@+{-# LANGUAGE ConstraintKinds #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE PartialTypeSignatures #-}+{-# LANGUAGE QuantifiedConstraints #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE StandaloneDeriving #-}++module C.Type+  ( -- * C types+    Type(..)+  , ArithmeticType(..)+  , IntegralType(..)+  , CharLikeType(..)+  , IntLikeType(..)+  , Sign(..)+  , FloatingType(..)+  , IntegerConversionRank(..)+  , intLikeTypeSign+  , charLikeTypeSizeInBits+  , intLikeTypeSizeInBits+  , intLikeTypeConversionRank+  , intLikeTypeFitsInInt+  , showTypeAsCType++  -- * Platform+  , Platform(..), WordWidth(..), OS(..)+  , hostPlatform++  -- * Singletons for C types+  , SType(..)+  , SArithmeticType(..)+  , SIntegralType(..)+  , SCharLikeType(..)+  , SIntLikeType(..)+  , SFloatingType(..)++  -- ** Promotion+  , promoteType+  , promoteArithmeticType+  , promoteIntegralType+  , promoteCharLikeType+  , promoteIntLikeType+  , promoteFloatingType++  -- ** Demotion+  , demoteType+  , demoteArithmeticType+  , demoteIntegralType+  , demoteCharLikeType+  , demoteIntLikeType+  , demoteFloatingType++  -- ** Utilities+  , witnessType+  , witnessArithmeticType+  , witnessFloatingType+  , witnessIntegralType+  , witnessCharLike+  , witnessIntLike++  ) where++import Data.GADT.Compare+import Data.Kind qualified as Hs+import Data.Semigroup (Arg (..))+import Data.Type.Equality+import Foreign.C.Types+import Foreign.Ptr qualified as Foreign (Ptr)+import Foreign.Storable (sizeOf)+import GHC.Generics (Generic)+import System.Info qualified (os)++--------------------------------------------------------------------------------++data Type a+  = Void+  | Arithmetic !ArithmeticType+  | Ptr        !a+  deriving stock ( Eq, Ord, Show, Functor, Foldable, Traversable, Generic )++data ArithmeticType+  = Integral  !IntegralType+  | FloatLike !FloatingType+  deriving stock ( Eq, Ord, Show, Generic )++data FloatingType = FloatType | DoubleType+  deriving stock ( Eq, Ord, Show, Generic )++data IntegralType+  = Bool+  | CharLike !CharLikeType+  | IntLike  !IntLikeType+  deriving stock ( Eq, Ord, Show, Generic )++data CharLikeType = Char | SChar | UChar+  deriving stock ( Eq, Ord, Show, Generic )++data Sign = Signed | Unsigned+  deriving stock ( Eq, Ord, Show, Generic )++data IntLikeType+  = Short    !Sign+  | Int      !Sign+  | Long     !Sign+  | LongLong !Sign+  | PtrDiff+  deriving stock ( Eq, Ord, Show, Generic )++--------------------------------------------------------------------------------++data WordWidth = WordWidth32 | WordWidth64+  deriving stock ( Eq, Ord, Show, Generic )++wordWidthInBits :: WordWidth -> Word+wordWidthInBits = \case+  WordWidth32 -> 32+  WordWidth64 -> 64++data OS = Windows | Posix+  deriving stock ( Eq, Ord, Show, Generic )++data Platform = Platform { platformWordWidth :: !WordWidth+                         , platformOS        :: !OS }+  deriving stock ( Eq, Show, Generic )++hostPlatform :: Platform+hostPlatform =+  Platform+    { platformWordWidth =+        case sizeOf @( Foreign.Ptr () ) undefined of+          4 -> WordWidth32+          8 -> WordWidth64+          w -> error $ "hostPlatform: unsupported word width (" ++ show (8 * w) ++ " bits)"+    , platformOS =+        case System.Info.os of+          "mingw32" -> Windows+          _         -> Posix+    }++newtype IntegerConversionRank = IntegerConversionRank Rational+  deriving stock ( Eq, Ord, Show, Generic )++intLikeTypeSign :: IntLikeType -> Sign+intLikeTypeSign = \case+  Short     s -> s+  Int       s -> s+  Long      s -> s+  LongLong  s -> s+  PtrDiff     -> Signed++charLikeTypeSizeInBits :: Platform -> CharLikeType -> Word+charLikeTypeSizeInBits _ = \case+  -- NB: this would need to change if we wanted to support+  -- platforms on which char is not 8 bits wide.+  Char  -> 8+  SChar -> 8+  UChar -> 8++intLikeTypeSizeInBits :: Platform -> IntLikeType -> Word+intLikeTypeSizeInBits plat i =+  case platformWordWidth plat of+    WordWidth32 ->+      case i of+        Short    {} -> 16+        Int      {} -> 32+        Long     {} -> 32+        LongLong {} -> 64+        PtrDiff     -> 32+    WordWidth64 ->+      case i of+        Short    {} -> 16+        Int      {} -> 32+        Long     {} ->+          case platformOS plat of+            Windows -> 32+            Posix   -> 64+        LongLong {} -> 64+        PtrDiff     -> 64++intLikeTypeConversionRank :: Platform -> IntLikeType -> IntegerConversionRank+intLikeTypeConversionRank plat = IntegerConversionRank . \case+  -- Rules for integer conversion ranks:+  --+  --  1. No two signed integer types other than char and signed char (if char is signed)+  --     have the same rank, even if they have the same representation.+  --  2. The rank of a signed integer type is greater than the rank of any+  --     signed integer type with a smaller width.+  --  3. The ranks of char/short/int/long/long long increase in order.+  --  4. The rank of any unsigned integer type equals the rank of the+  --     corresponding signed integer type.+  --  5. The rank of any standard integer type is greater than the rank of+  --     any extended integer type with the same width.+  --  6. The rank of bool is less than the rank of all standard integer types.+  --  7. The rank of any extended signed integer type relative to another extended+  --     signed integer type with the same width is implementation-defined.++  -- Standard integer types.+  -- Implement (3), ignoring sign as per (4).+  Short     {} -> 3+  Int       {} -> 4+  Long      {} -> 5+  LongLong  {} -> 6++  -- Extended types.+  _extended_ty ->+    -- The following logic comes from (1) and (5), which dictate that the+    -- integer conversion rank of ptrdiff_t and size_t must be:+    --+    --  (a) strictly greater than the integer conversion rank of any+    --      standard integer type whose size is less than the word width,+    --  (b) strictly less than the integer conversion rank of any standard+    --      integer type whose size is greater than or equal to the word width.+    case minimum [ Arg rk ty+                 | ty <- [ Short Signed, Int Signed, Long Signed, LongLong Signed ]+                 , let sz = intLikeTypeSizeInBits plat ty+                       rk = intLikeTypeConversionRank plat ty+                 , sz >= wordWidthInBits ( platformWordWidth plat )+                 ] of+      Arg ( IntegerConversionRank rk ) _ ->+        rk - 0.5+          -- 0.5 is an arbitrary value in the open interval ]0,1[+          --+          -- This assumes that the standard integer types are given+          -- integral integer conversion ranks.++-- | Does the given 'IntLikeType' fit inside the (signed) @int@ type+-- on this platform?+intLikeTypeFitsInInt :: Platform -> IntLikeType -> Bool+intLikeTypeFitsInInt plat ty =+  -- TODO <https://github.com/well-typed/c-expr/issues/27>+  --+  -- This logic is questionable, as in theory I think we could have an 'IntLike'+  -- type of a small size but of an entirely distinct range, e.g. an 8-bit+  -- unsigned integer type that can store values in the range [2^32,+  -- 2^32+2^8-1].+  case intLikeTypeSign ty of+    Signed ->+      sz <= intSz+    Unsigned ->+      sz < intSz+  where+    sz, intSz :: Word+    sz = intLikeTypeSizeInBits plat ty+    intSz = intLikeTypeSizeInBits plat (Int Signed)++--------------------------------------------------------------------------------++showTypeAsCType :: Show a => Type a -> String -> String+showTypeAsCType ty s =+  case ty of+    Void         -> "void" +++ s+    Arithmetic a -> showArithmeticTypeAsCType a +++ s+    Ptr a        -> addStar (show a) ++ s+  where+    x +++ "" = x+    x +++ y = x ++ " " ++ y+    addStar x@(_:_)+      | last x == '*'+      = x ++ "*"+    addStar x+      = x ++ " *"++showArithmeticTypeAsCType :: ArithmeticType -> String+showArithmeticTypeAsCType = \case+  Integral i ->+    showIntegralTypeAsCType i+  FloatLike f ->+    case f of+      FloatType  -> "float"+      DoubleType -> "double"++showIntegralTypeAsCType :: IntegralType -> String+showIntegralTypeAsCType = \case+  Bool -> "bool"+  CharLike c ->+    case c of+      Char -> "char"+      SChar -> "signed char"+      UChar -> "unsigned char"+  IntLike i ->+    showIntLikeTypeAsCType i++showIntLikeTypeAsCType :: IntLikeType -> String+showIntLikeTypeAsCType = \case+  Short    s -> withSign s "short"+  Int      s -> withSign s "int"+  Long     s -> withSign s "long"+  LongLong s -> withSign s "long long"+  PtrDiff -> "ptrdiff_t"+  where+    withSign s = case s of+      Signed   -> id+      Unsigned -> ( "unsigned " ++ )++--------------------------------------------------------------------------------+-- Singletons++type SType :: ( Hs.Type -> Hs.Type ) -> Hs.Type -> Hs.Type+data SType rec a where+  SVoid :: SType rec ()+  SArithmetic :: !( SArithmeticType ty ) -> SType rec ty+  SPtr :: rec ty -> SType rec ( Foreign.Ptr ty )+deriving stock instance ( forall x. Show ( rec x ) ) => Show ( SType rec a )++data SArithmeticType ty where+  SIntegral  :: !( SIntegralType ty ) -> SArithmeticType ty+  SFloatLike :: !( SFloatingType ty ) -> SArithmeticType ty+deriving stock instance Show ( SArithmeticType ty )++data SFloatingType ty where+  SFloatType  :: SFloatingType CFloat+  SDoubleType :: SFloatingType CDouble+deriving stock instance Show ( SFloatingType ty )++data SIntegralType ty where+  SBool :: SIntegralType CBool+  SCharLike :: !( SCharLikeType ty ) -> SIntegralType ty+  SIntLike :: !( SIntLikeType ty ) -> SIntegralType ty+deriving stock instance Show ( SIntegralType ty )++data SCharLikeType ty where+  S_Char  :: SCharLikeType CChar+  S_SChar :: SCharLikeType CSChar+  S_UChar :: SCharLikeType CUChar+deriving stock instance Show ( SCharLikeType ty )++data SIntLikeType ty where+  SShort     :: SIntLikeType CShort+  SUShort    :: SIntLikeType CUShort+  SInt       :: SIntLikeType CInt+  SUInt      :: SIntLikeType CUInt+  SLong      :: SIntLikeType CLong+  SULong     :: SIntLikeType CULong+  SLongLong  :: SIntLikeType CLLong+  SULongLong :: SIntLikeType CULLong+  SPtrDiff   :: SIntLikeType CPtrdiff+  -- NB: make sure to update 'GEq SIntLikeType' when updating this datatype+deriving stock instance Show ( SIntLikeType ty )++instance GEq rec => GEq ( SType rec ) where+  geq SVoid SVoid = Just Refl+  geq (SArithmetic a) (SArithmetic b) = geq a b+  geq (SPtr a) (SPtr b) =+    case geq a b of+      Just Refl -> Just Refl+      Nothing   -> Nothing+  geq _ _ = Nothing+instance GEq SArithmeticType where+  geq (SIntegral a) (SIntegral b) = geq a b+  geq (SFloatLike a) (SFloatLike b) = geq a b+  geq _ _ = Nothing++instance GEq SFloatingType where+  geq SFloatType  SFloatType  = Just Refl+  geq SDoubleType SDoubleType = Just Refl+  geq _ _ = Nothing+instance GEq SCharLikeType where+  geq S_Char  S_Char  = Just Refl+  geq S_SChar S_SChar = Just Refl+  geq S_UChar S_UChar = Just Refl+  geq _       _       = Nothing++instance GEq SIntegralType where+  geq SBool          SBool        = Just Refl+  geq (SCharLike a) (SCharLike b) = geq a b+  geq (SIntLike  a) (SIntLike  b) = geq a b+  geq _ _ = Nothing++instance GEq SIntLikeType where+  geq SShort     SShort     = Just Refl+  geq SUShort    SUShort    = Just Refl+  geq SInt       SInt       = Just Refl+  geq SUInt      SUInt      = Just Refl+  geq SLong      SLong      = Just Refl+  geq SULong     SULong     = Just Refl+  geq SLongLong  SLongLong  = Just Refl+  geq SULongLong SULongLong = Just Refl+  geq SPtrDiff   SPtrDiff   = Just Refl+  geq _ _ = Nothing++promoteType :: ( a -> ( forall ty. rec ty -> r ) -> r ) -> Type a -> ( forall ty. ( Ord ty, Show ty ) => SType rec ty -> r ) -> r+promoteType recur ty f = case ty of+  Void -> f SVoid+  Arithmetic i -> promoteArithmeticType i ( f . SArithmetic )+  Ptr p -> recur p ( f . SPtr )++promoteArithmeticType :: ArithmeticType -> ( forall ty. ( Ord ty, Show ty ) => SArithmeticType ty -> r ) -> r+promoteArithmeticType ty f = case ty of+  Integral  t -> promoteIntegralType t ( f . SIntegral )+  FloatLike t -> promoteFloatingType t ( f . SFloatLike )++promoteFloatingType :: FloatingType -> ( forall ty. ( Ord ty, Show ty ) => SFloatingType ty -> r ) -> r+promoteFloatingType ty f = case ty of+  FloatType  -> f SFloatType+  DoubleType -> f SDoubleType++promoteIntegralType :: IntegralType -> ( forall ty. ( Show ty, Integral ty ) => SIntegralType ty -> r ) -> r+promoteIntegralType ty f = case ty of+  Bool -> f SBool+  CharLike c -> promoteCharLikeType c ( f . SCharLike )+  IntLike i  -> promoteIntLikeType  i ( f . SIntLike )++promoteCharLikeType :: CharLikeType -> ( forall ty. ( Show ty, Integral ty ) => SCharLikeType ty -> r ) -> r+promoteCharLikeType ty f = case ty of+  Char  -> f S_Char+  UChar -> f S_UChar+  SChar -> f S_SChar++promoteIntLikeType :: IntLikeType -> ( forall ty. ( Show ty, Integral ty ) => SIntLikeType ty -> r ) -> r+promoteIntLikeType ty f = case ty of+  Short s ->+    case s of+      Signed   -> f SShort+      Unsigned -> f SUShort+  Int s ->+    case s of+      Signed   -> f SInt+      Unsigned -> f SUInt+  Long s ->+    case s of+      Signed   -> f SLong+      Unsigned -> f SULong+  LongLong s ->+    case s of+      Signed   -> f SLongLong+      Unsigned -> f SULongLong+  PtrDiff -> f SPtrDiff++demoteType :: ( forall ty'. rec ty' -> a ) -> SType rec ty -> Type a+demoteType recur = \case+  SVoid -> Void+  SArithmetic a -> Arithmetic $ demoteArithmeticType a+  SPtr a -> Ptr $ recur a++demoteArithmeticType :: SArithmeticType ty -> ArithmeticType+demoteArithmeticType = \case+  SIntegral  i -> Integral  $ demoteIntegralType i+  SFloatLike f -> FloatLike $ demoteFloatingType f++demoteIntegralType :: SIntegralType ty -> IntegralType+demoteIntegralType = \case+  SBool -> Bool+  SCharLike c -> CharLike $ demoteCharLikeType c+  SIntLike i  -> IntLike  $ demoteIntLikeType  i++demoteFloatingType :: SFloatingType ty -> FloatingType+demoteFloatingType = \case+  SFloatType  -> FloatType+  SDoubleType -> DoubleType++demoteCharLikeType :: SCharLikeType ty -> CharLikeType+demoteCharLikeType = \case+  S_Char  -> Char+  S_UChar -> UChar+  S_SChar -> SChar++demoteIntLikeType :: SIntLikeType ty -> IntLikeType+demoteIntLikeType = \case+  SShort     -> Short Signed+  SUShort    -> Short Unsigned+  SInt       -> Int Signed+  SUInt      -> Int Unsigned+  SLong      -> Long Signed+  SULong     -> Long Unsigned+  SLongLong  -> LongLong Signed+  SULongLong -> LongLong Unsigned+  SPtrDiff   -> PtrDiff++witnessType+  :: forall c ty rec 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 () )+  => ( forall ty'. rec ty' -> ( c ty' => r ) -> r )+  -> SType rec ty -> ( c ty => r ) -> r+witnessType recur ty f =+  case ty of+    SVoid  -> f+    SArithmetic i -> witnessArithmeticType @c i f+    SPtr p -> recur p f++witnessArithmeticType+  :: forall c ty r+  . ( 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 )+  => SArithmeticType ty -> ( c ty => r ) -> r+witnessArithmeticType ty f =+  case ty of+    SIntegral i -> witnessIntegralType @c i f+    SFloatLike k -> witnessFloatingType @c k f++witnessFloatingType+  :: forall c ty r+  . ( c CFloat, c CDouble )+  => SFloatingType ty -> ( c ty => r ) -> r+witnessFloatingType ty f =+  case ty of+    SFloatType -> f+    SDoubleType -> f++witnessIntegralType+  :: forall c ty r+  . ( 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 )+  => SIntegralType ty -> ( c ty => r ) -> r+witnessIntegralType ty f =+  case ty of+    SBool       -> f+    SCharLike c -> witnessCharLike @c c f+    SIntLike  i -> witnessIntLike @c i f++witnessCharLike+  :: forall c ty r+  .  ( c CChar, c CSChar, c CUChar )+  => SCharLikeType ty -> ( c ty => r ) -> r+witnessCharLike ty f =+  case ty of+    S_Char -> f+    S_SChar -> f+    S_UChar -> f++witnessIntLike+  :: forall c ty r+  . ( c CShort, c CUShort, c CInt, c CUInt, c CLong, c CULong+    , c CLLong, c CULLong, c CPtrdiff, c CSize )+  => SIntLikeType ty -> ( c ty => r ) -> r+witnessIntLike ty f =+  case ty of+    SShort     -> f+    SUShort    -> f+    SInt       -> f+    SUInt      -> f+    SLong      -> f+    SULong     -> f+    SLongLong  -> f+    SULongLong -> f+    SPtrDiff   -> f
+ core/C/Type/Internal/Universe.hs view
@@ -0,0 +1,77 @@+{-# LANGUAGE ScopedTypeVariables #-}++-- | __Internal__ module listing out all n-tuples of types+-- for the purposes of generating code with Template Haskell+-- and for testing.+module C.Type.Internal.Universe+  ( OpaqueTy(..)+  , enumerateTypeTuples+  , allArithmeticTypes, allIntegralTypes, allIntLikeTypes+  ) where++import Data.Functor ((<&>))+import Data.Type.Nat qualified as Fin+import Data.Vec.Lazy (Vec (..))+import Data.Vec.Lazy qualified as Vec (snoc)+import GHC.Generics (Generic)++import C.Type++--------------------------------------------------------------------------------++-- | Helper type to use 'Fin.induction' on.+newtype F n = F { unF :: [ ( Vec n ( Type OpaqueTy ), Maybe Int ) ] }++-- | An opaque named type with a unique identifier.+newtype OpaqueTy = OpaqueTy Int+  deriving stock ( Eq, Ord, Show, Generic )++-- | Enumerate all tuples of types.+--+-- For example, for @n = 2@, this will list out pairs of types.+-- This list will include all pairwise combination of primitive types,+-- and also two pairs of pointer types:+--+--  - @( Ptr ty_1, Ptr ty_2 )@ – pointers to different types,+--  - @( Ptr ty_1, Ptr ty_1 )@ – pointers to the same type.+--+-- This is used for generating type family and class instances.+enumerateTypeTuples :: forall n. Fin.SNatI n => [ Vec n ( Type OpaqueTy ) ]+enumerateTypeTuples = fmap fst $ unF $+  Fin.induction+    ( F [ ( VNil, Nothing ) ] )+    ( \ ( ( F prev ) :: F m ) -> F $ do+      ( tys, mbLastUsedTyVarNumber ) <- prev+      let m = case mbLastUsedTyVarNumber of+                Nothing -> 1+                Just i  -> i + 1+      ( ty, mbNextUsedTyVar ) <- allTypes m+      let mbUsedTv = maxMaybe mbLastUsedTyVarNumber mbNextUsedTyVar+      return ( Vec.snoc tys ty, mbUsedTv )+    )++maxMaybe :: Ord i => Maybe i -> Maybe i -> Maybe i+maxMaybe ( Just i ) ( Just j ) = Just $ max i j+maxMaybe j@( Just {} ) Nothing = j+maxMaybe Nothing r = r++allTypes :: Int -> [ ( Type OpaqueTy, Maybe Int ) ]+allTypes n =+  fmap ( ( , Nothing ) . Arithmetic ) allArithmeticTypes ++ ( Void, Nothing ) :+    [ ( Ptr ( OpaqueTy i ), Just i ) | i <- [ 1 .. n ] ]+  -- For unary functions, just have a single pointer type "Ptr a".+  -- For binary functions, the first argument has "Ptr a1",+  -- while the second argument has both "Ptr a1" and "Ptr a2".+  -- etc++allArithmeticTypes :: [ ArithmeticType ]+allArithmeticTypes = fmap FloatLike [ FloatType, DoubleType ]+                  ++ fmap Integral  allIntegralTypes++allIntegralTypes :: [ IntegralType ]+allIntegralTypes = Bool : fmap CharLike [ Char, SChar, UChar ] ++ fmap IntLike allIntLikeTypes++allIntLikeTypes :: [ IntLikeType ]+allIntLikeTypes =+  concatMap ( [ Signed, Unsigned ] <&> ) [ Short, Int, Long, LongLong ]+    ++ [ PtrDiff ]
+ lib/C/Expr/HostPlatform.hs view
@@ -0,0 +1,54 @@+{-# LANGUAGE CPP #-}++#include <MachDeps.h>++-- Confusingly, mingw32_HOST_OS is also defined on 64-bit Windows+#ifdef mingw32_HOST_OS+#  if WORD_SIZE_IN_BITS == 64+#    define CExprPlatform C.Expr.Win64+#  else+#    error "C.Expr: Windows: word size must be 64 bits"+#  endif+#else+#  if WORD_SIZE_IN_BITS == 32+#    define CExprPlatform C.Expr.Posix32+#  elif WORD_SIZE_IN_BITS == 64+#    define CExprPlatform C.Expr.Posix64+#  else+#    error "C.Expr: POSIX: word size must be 32 or 64 bits"+#  endif+#endif++module C.Expr.HostPlatform+  ( -- explicit re-exports of everything in C.Operator.Classes+    -- (we don't re-export the module, for better haddocks)++    -- * Logical operators+    Not(..)+  , Logical(..)+    -- * Equality and comparison+  , RelEq(..), RelOrd(..)+  , NotNull(..)+    -- * Arithmetic+    -- ** Unary+  , Plus(..)+  , Minus(..)+    -- ** Binary+  , Add(..)+  , Sub(..)+  , Mult(..)+  , Div(..)+  , Rem(..)+    -- * Bitwise+    -- ** Unary+  , Complement(..)+    -- ** Binary+  , Bitwise(..)+  , Shift(..)++    -- instances+  , module CExprPlatform+  ) where++import C.Operator.Classes+import CExprPlatform
+ lib/C/Expr/Posix32.hs view
@@ -0,0 +1,28 @@+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TemplateHaskell #-}+{-# LANGUAGE UndecidableInstances #-}++{-# OPTIONS_GHC -Wno-orphans -Wno-unused-matches #-}++-- Some options to make this module faster to compile+{-# OPTIONS_GHC -O0 -fmax-pmcheck-models=1 #-}++module C.Expr.Posix32+  ( module C.Operator.Classes+  , module C.Expr.Posix32+  ) where++-- c-expr+import C.Type (OS (..), Platform (..), WordWidth (..))++import C.Operator.Classes+import C.Operator.GenInstances (cExprInstances)++--------------------------------------------------------------------------------++$( cExprInstances+    ( Platform+        { platformWordWidth = WordWidth32+        , platformOS        = Posix+        }+    ) )
+ lib/C/Expr/Posix64.hs view
@@ -0,0 +1,27 @@+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TemplateHaskell #-}+{-# LANGUAGE UndecidableInstances #-}++{-# OPTIONS_GHC -Wno-orphans -Wno-unused-matches #-}++-- Some options to make this module faster to compile+{-# OPTIONS_GHC -O0 -fmax-pmcheck-models=1 #-}++module C.Expr.Posix64+  ( module C.Operator.Classes+  , module C.Expr.Posix64+  ) where++import C.Type (OS (..), Platform (..), WordWidth (..))++import C.Operator.Classes+import C.Operator.GenInstances (cExprInstances)++--------------------------------------------------------------------------------++$( cExprInstances+    ( Platform+        { platformWordWidth = WordWidth64+        , platformOS        = Posix+        }+    ) )
+ lib/C/Expr/Win64.hs view
@@ -0,0 +1,27 @@+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TemplateHaskell #-}+{-# LANGUAGE UndecidableInstances #-}++{-# OPTIONS_GHC -Wno-orphans -Wno-unused-matches #-}++-- Some options to make this module faster to compile+{-# OPTIONS_GHC -O0 -fmax-pmcheck-models=1 #-}++module C.Expr.Win64+  ( module C.Operator.Classes+  , module C.Expr.Win64+  ) where++import C.Type (OS (..), Platform (..), WordWidth (..))++import C.Operator.Classes+import C.Operator.GenInstances (cExprInstances)++--------------------------------------------------------------------------------++$( cExprInstances+    ( Platform+        { platformWordWidth = WordWidth64+        , platformOS        = Windows+        }+    ) )
+ test/CallClang.hs view
@@ -0,0 +1,368 @@+{-# LANGUAGE OverloadedStrings #-}+{-# LANGUAGE ScopedTypeVariables #-}++module CallClang+  ( CType(..)+  , queryClangForResultType+  , getExpansionTypeMapping+  , queryClangBuildTargetTriple+  )+  where++import Control.Exception (bracket)+import Control.Monad.IO.Class (MonadIO (liftIO))+import Data.Default (Default (def))+import Data.Foldable (toList)+import Data.IntMap.Strict (IntMap)+import Data.IntMap.Strict qualified as IntMap+import Data.List (intercalate, partition)+import Data.Map.Strict (Map)+import Data.Map.Strict qualified as Map+import Data.Maybe (listToMaybe)+import Data.Text (Text)+import Data.Text qualified as Text+import Data.Vec.Lazy (Vec (..))+import Data.Vec.Lazy qualified as Vec+import Text.Read (readMaybe)++import C.Type++import Clang.Args qualified as Clang+import Clang.Enum.Bitfield qualified as Clang (BitfieldEnum, bitfieldEnum)+import Clang.Enum.Simple qualified as Clang (fromSimpleEnum)+import Clang.HighLevel qualified as Clang hiding (clang_getCursorLocation)+import Clang.HighLevel.Types qualified as Clang+import Clang.LowLevel.Core qualified as Clang hiding (clang_visitChildren)+import Clang.Paths qualified as Paths++--------------------------------------------------------------------------------++-- | A C type, extended with typedefs for use with Clang.+data CType+  = TypeDef !Text+  | CType !(Type CType)+  deriving stock ( Eq, Ord )+instance Show CType where+  show (TypeDef ty) = Text.unpack ty+  show (CType ty) = showTypeAsCType ty ""++showCType :: CType -> String -> String+showCType (TypeDef ty) s = Text.unpack ty ++ " " ++ s+showCType (CType ty) s = showTypeAsCType ty s+++-- | Parse a 'CXType' into a 'Type'.+parseClangType :: Clang.CXType -> IO ( Maybe CType )+parseClangType cxTy = do+  ty <- Clang.clang_getTypeSpelling cxTy+  case Clang.fromSimpleEnum $ Clang.cxtKind cxTy of+    Left {} -> return $ Nothing+    Right ki -> do+      case ki of+        Clang.CXType_Invalid             -> return Nothing+        -- LLVM/Clang 22 reports the predefined sugar types '__ptrdiff_t',+        -- '__size_t', and '__signed_size_t' as 'CXType_Unexposed' (see+        -- upstream https://github.com/llvm/llvm-project/issues/192268).+        -- Fall back to the canonical type to recover the underlying kind.+        Clang.CXType_Unexposed           -> do { canTy <- Clang.clang_getCanonicalType cxTy+                                               ; case Clang.fromSimpleEnum $ Clang.cxtKind canTy of+                                                   Right Clang.CXType_Unexposed -> return Nothing+                                                   _otherKind                   -> parseClangType canTy+                                               }+        Clang.CXType_Void                -> return $ Just $ CType Void+        Clang.CXType_Bool                -> return $ Just $ CType $ Arithmetic $ Integral $ Bool+        Clang.CXType_Char_U              -> return $ Just $ CType $ Arithmetic $ Integral $ CharLike UChar+        Clang.CXType_UChar               -> return $ Just $ CType $ Arithmetic $ Integral $ CharLike UChar+        Clang.CXType_Char16              -> return Nothing+        Clang.CXType_Char32              -> return Nothing+        Clang.CXType_UShort              -> return $ Just $ CType $ Arithmetic $ Integral $ IntLike $ Short    Unsigned+        Clang.CXType_UInt                -> return $ Just $ CType $ Arithmetic $ Integral $ IntLike $ Int      Unsigned+        Clang.CXType_ULong               -> return $ Just $ CType $ Arithmetic $ Integral $ IntLike $ Long     Unsigned+        Clang.CXType_ULongLong           -> return $ Just $ CType $ Arithmetic $ Integral $ IntLike $ LongLong Unsigned+        Clang.CXType_UInt128             -> return Nothing+        Clang.CXType_Char_S              -> return $ Just $ CType $ Arithmetic $ Integral $ CharLike Char+        Clang.CXType_SChar               -> return $ Just $ CType $ Arithmetic $ Integral $ CharLike SChar+        Clang.CXType_WChar               -> return Nothing+        Clang.CXType_Short               -> return $ Just $ CType $ Arithmetic $ Integral $ IntLike $ Short    Signed+        Clang.CXType_Int                 -> return $ Just $ CType $ Arithmetic $ Integral $ IntLike $ Int      Signed+        Clang.CXType_Long                -> return $ Just $ CType $ Arithmetic $ Integral $ IntLike $ Long     Signed+        Clang.CXType_LongLong            -> return $ Just $ CType $ Arithmetic $ Integral $ IntLike $ LongLong Signed+        Clang.CXType_Int128              -> return Nothing+        Clang.CXType_Float               -> return $ Just $ CType $ Arithmetic $ FloatLike FloatType+        Clang.CXType_Double              -> return $ Just $ CType $ Arithmetic $ FloatLike DoubleType+        Clang.CXType_LongDouble          -> return Nothing+        Clang.CXType_NullPtr             -> return Nothing+        Clang.CXType_Overload            -> return Nothing+        Clang.CXType_Dependent           -> return Nothing+        Clang.CXType_ObjCId              -> return Nothing+        Clang.CXType_ObjCClass           -> return Nothing+        Clang.CXType_ObjCSel             -> return Nothing+        Clang.CXType_Float128            -> return Nothing+        Clang.CXType_Half                -> return Nothing+        Clang.CXType_Float16             -> return Nothing+        Clang.CXType_ShortAccum          -> return Nothing+        Clang.CXType_Accum               -> return Nothing+        Clang.CXType_LongAccum           -> return Nothing+        Clang.CXType_UShortAccum         -> return Nothing+        Clang.CXType_UAccum              -> return Nothing+        Clang.CXType_ULongAccum          -> return Nothing+        Clang.CXType_BFloat16            -> return Nothing+        Clang.CXType_Ibm128              -> return Nothing+        Clang.CXType_Complex             -> return Nothing+        Clang.CXType_Pointer             -> fmap ( CType . Ptr ) <$> ( parseClangType =<< Clang.clang_getPointeeType cxTy )+        Clang.CXType_BlockPointer        -> return Nothing+        Clang.CXType_LValueReference     -> return Nothing+        Clang.CXType_RValueReference     -> return Nothing+        Clang.CXType_Record              -> return $ Just $ TypeDef ty+        Clang.CXType_Enum                -> do { tyDecl <- Clang.clang_getTypeDeclaration cxTy+                                               ; enumTy <- Clang.clang_getEnumDeclIntegerType tyDecl+                                               ; parseClangType enumTy }+        Clang.CXType_Typedef             -> do { canTy <- Clang.clang_getCanonicalType cxTy+                                               ; parseClangType canTy }+        Clang.CXType_ObjCInterface       -> return Nothing+        Clang.CXType_ObjCObjectPointer   -> return Nothing+        Clang.CXType_FunctionNoProto     -> return Nothing+        Clang.CXType_FunctionProto       -> return Nothing+        Clang.CXType_ConstantArray       -> return Nothing+        Clang.CXType_Vector              -> return Nothing+        Clang.CXType_IncompleteArray     -> return Nothing+        Clang.CXType_VariableArray       -> return Nothing+        Clang.CXType_DependentSizedArray -> return Nothing+        Clang.CXType_MemberPointer       -> return Nothing+        Clang.CXType_Auto                -> do { canTy <- Clang.clang_getCanonicalType cxTy+                                               ; parseClangType canTy }+        Clang.CXType_Elaborated          -> do { namedTy <- Clang.clang_Type_getNamedType cxTy+                                               ; parseClangType namedTy }+        Clang.CXType_ObjCObject          -> return Nothing+        Clang.CXType_ObjCTypeParam       -> return Nothing+        Clang.CXType_Attributed          -> return Nothing+        Clang.CXType_ExtVector           -> return Nothing+        Clang.CXType_Atomic              -> return Nothing++-- | Query @clang@ for canonical names for types.+getExpansionTypeMapping :: Clang.ClangArgs -> [ CType ] -> IO ( Map CType CType )+getExpansionTypeMapping clangArgs tys =+  clangVisitChildren clangArgs sourceProgram ( getCanonicalType Nothing ) $+    \ _severe ->+        traverse ( \ cxTy -> expectJust cxTy =<< parseClangType cxTy )+      . Map.fromList++  where++    getCanonicalType :: Maybe Int -> Clang.Fold IO ( CType, Clang.CXType )+    getCanonicalType inTestFunDecl = Clang.simpleFold $ \cursor -> do+      loc <- liftIO $ Clang.clang_getCursorLocation cursor+      inMain <- liftIO $ Clang.clang_Location_isFromMainFile loc+      if not inMain+      then+        Clang.foldContinue+      else do+        cursorKind <- liftIO $ Clang.fromSimpleEnum <$> Clang.clang_getCursorKind cursor+        case cursorKind of+          Right kind+            | Clang.CXCursor_FunctionDecl <- kind+            -> do+              funNm <- liftIO $ Clang.clang_getCursorSpelling cursor+              let ( nm, nb ) = Text.splitAt 6 funNm+              case readMaybe ( Text.unpack nb ) of+                Just i | nm == "testFn" ->+                  Clang.foldRecursePureOpt ( getCanonicalType ( Just i ) ) listToMaybe+                _otherwise ->+                  Clang.foldContinue+            | Just nb <- inTestFunDecl+            , Clang.CXCursor_DeclRefExpr <- kind+            -> do+              cxTy  <- liftIO $ Clang.clang_getCursorType    cursor+              mbRhsTy <- parseClangType cxTy+              let lhsTy = tyPairs IntMap.! nb+                  res+                    | Just rhsTy <- mbRhsTy+                    , lhsTy /= rhsTy+                    -- Don't bother when a type is mapped to itself.+                    = Just ( lhsTy, cxTy )+                    | otherwise+                    = Nothing+              Clang.foldContinueOpt res+          _ -> Clang.foldRecursePureOpt ( getCanonicalType inTestFunDecl ) listToMaybe++    tyPairs :: IntMap CType+    tyPairs = IntMap.fromList [ (i, ty) | i <- [ (1 :: Int) .. ] | ty <- tys ]++    sourceProgram :: String+    sourceProgram = unlines $ concat+      [ [ "#include <stddef.h>" ]+      , [ unlines+            [ "static " ++ showTy "testFn" ++ show i ++ "(" ++ showTy "x" ++ ") {"+            , "  return x;"+            , "}"+            ]+        | ( i, ty ) <- IntMap.assocs tyPairs+        , let showTy = showCType ty+        ]+      ]++    expectJust :: Clang.CXType -> Maybe a -> IO a+    expectJust cxTy =+      \case+        Nothing -> do+          tyNm <- Clang.clang_getTypeSpelling cxTy+          error $ unlines+            [ "getExpansionTypeMapping: could not parse CXType " ++ show cxTy+            , Text.unpack tyNm ]+        Just ty -> return ty++-- | Query @clang@ for the result type of an operator application.+--+-- Returns the extracted type (if any) together with the formatted text of any+-- severe diagnostics @clang@ emitted. A severe diagnostic discards the whole+-- translation unit, so the type is then 'Nothing'; returning the diagnostics+-- lets the caller report /why/ the result is unavailable (e.g. a builtin header+-- such as @stddef.h@ could not be found) instead of a bare @<n/a>@.+queryClangForResultType ::+     forall n. Clang.ClangArgs+  -> Vec n CType+  -> ( Vec n String -> String )+  -> IO ( Maybe CType, [ Text ] )+queryClangForResultType clangArgs tys op =+  clangVisitChildren clangArgs sourceProgram ( extractType ( False, False ) ) $+    \ severe results ->+      return ( listToMaybe results, map Clang.diagnosticFormatted severe )+  where+    n :: Int+    n = length tys++    args, typedArgs :: Vec n String+    args = Vec.imap (\ i _ -> "x_" ++ show i) tys+    typedArgs = Vec.imap ( \i ty -> showCType ty ( "x_" ++ show i ) ) tys++    sourceProgram :: String+    sourceProgram = unlines $ concat $+      [ [ "// #include <stdio.h>"+        , "#include <stddef.h>"+        , "#define bool _Bool"+        , ""+        ]+      , [ "typedef struct { void **unused; } " ++ s ++ ";"+        | i <- [ 1 .. n ]+        , let s = "ty_" ++ show i+        ]+      , [ ""+        , "static int testFunction (" ++ intercalate ", " (toList typedArgs) ++ ") {"+        , "  (void)(" ++ op args ++ ");"+        , "  return 0;"+        , "}"+        ]+      ]++    extractType :: ( Bool, Bool ) -> Clang.Fold IO CType+    extractType ( inTestFunDecl, inCast ) = Clang.simpleFold $ \cursor -> do+      loc <- Clang.clang_getCursorLocation cursor+      inMain <- Clang.clang_Location_isFromMainFile loc+      if not inMain+      then+        Clang.foldContinue+      else do+        cursorKind <- Clang.fromSimpleEnum <$> Clang.clang_getCursorKind cursor+        case cursorKind of+          Right kind+            | Clang.CXCursor_CStyleCastExpr <- kind+            -> Clang.foldRecursePureOpt ( extractType ( inTestFunDecl, True ) ) listToMaybe+            | Clang.CXCursor_FunctionDecl <- kind+            -> do+              funNm <- Clang.clang_getCursorSpelling cursor+              if funNm == "testFunction"+              then+                Clang.foldRecursePureOpt ( extractType ( True, False ) ) listToMaybe+              else+                Clang.foldContinue+            | inTestFunDecl+            , inCast+            , kind == Clang.CXCursor_UnaryOperator || kind == Clang.CXCursor_BinaryOperator+            -> do+              cxTy <- Clang.clang_getCursorType cursor+              mbTy <- parseClangType cxTy+              Clang.foldBreakOpt mbTy+          _ -> Clang.foldRecursePureOpt ( extractType ( inTestFunDecl, inCast ) ) listToMaybe++clangWithTranslationUnit ::+     Clang.ClangArgs+  -> String+  -> (Clang.CXTranslationUnit -> IO a)+  -> IO a+clangWithTranslationUnit userClangArgs srcContents k =+  Clang.withIndex Clang.DontDisplayDiagnostics $ \index ->+    Clang.withUnsavedFile headerName srcContents $ \unsavedFile ->+      Clang.withTranslationUnit index (Just src) args [unsavedFile] opts k+  where+    headerName :: FilePath+    headerName = "src.c"++    src :: Paths.SourcePath+    src = Paths.SourcePath $ Text.pack headerName++    args :: Clang.ClangArgs+    args = Clang.ClangArgs $+      Clang.unClangArgs userClangArgs+        +++        [ "-Werror=pointer-integer-compare"+        , "-Werror=compare-distinct-pointer-types"+        ]++    opts :: Clang.BitfieldEnum Clang.CXTranslationUnit_Flags+    opts = Clang.bitfieldEnum+      [ Clang.CXTranslationUnit_DetailedPreprocessingRecord+      , Clang.CXTranslationUnit_IncludeAttributedTypes+      , Clang.CXTranslationUnit_VisitImplicitAttributes+      ]++-- NB: This is implemented using a continuation so that all @libclang@ values+-- are processed before the file content, translation unit, and index are freed.+-- | The continuation receives the severe diagnostics (empty unless the+-- translation unit failed to compile) and the folded results. When there are+-- severe diagnostics the translation unit is discarded, so the results are+-- empty and the diagnostics explain why.+clangVisitChildren ::+     Clang.ClangArgs+  -> String+  -> Clang.Fold IO a+  -> ([Clang.Diagnostic] -> [a] -> IO b)+  -> IO b+clangVisitChildren args srcContents f k =+    clangWithTranslationUnit args srcContents $ \unit -> do+      diags <- Clang.clang_getDiagnostics unit Nothing+      let (errors, _warnings) = partition diagnosticIsSevere diags+      if null errors+      then do+        rootCursor <- Clang.clang_getTranslationUnitCursor unit+        k errors =<< Clang.clang_visitChildren rootCursor f+      else+        k errors []++diagnosticIsSevere :: Clang.Diagnostic -> Bool+diagnosticIsSevere diag =+  Clang.diagnosticIsError diag ||+    diagTextIsSevere ( Clang.diagnosticSpelling diag )+  where+    diagTextIsSevere :: Text -> Bool+    diagTextIsSevere diagTxt =+      or+        -- Turn warnings about comparison between e.g. 'char *' and 'int'+        -- into errors.+        --+        -- NB: for some reason, -Werror=pointer-integer-compare isn't sufficient+        -- to achieve this.+        [ Text.isPrefixOf "ordered comparison between pointer and integer" diagTxt+        ]++-------------------------------------------------------------------------------++-- | Get the target triple of the build system, as reported by Clang.+queryClangBuildTargetTriple :: IO Text+queryClangBuildTargetTriple =+  clangWithTranslationUnit def "" getTriple+  where+    getTriple unit =+      bracket+          ( Clang.clang_getTranslationUnitTargetInfo unit )+          Clang.clang_TargetInfo_dispose+          Clang.clang_TargetInfo_getTriple
+ test/Main.hs view
@@ -0,0 +1,197 @@+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE DerivingStrategies #-}+{-# LANGUAGE LambdaCase #-}+{-# LANGUAGE NamedFieldPuns #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE TupleSections #-}+{-# LANGUAGE TypeApplications #-}++module Main where++import Control.Arrow (first)+import Data.Map.Strict (Map)+import Data.Map.Strict qualified as Map+import Data.Maybe (catMaybes)+import Data.Text (Text)+import Data.Text qualified as Text+import Data.Traversable (for)+import Data.Type.Nat+import Data.Vec.Lazy (Vec (..))+import System.Exit+import System.Info qualified as Info++import C.Type+import C.Type.Internal.Universe++import Clang.Args qualified as Clang+import Clang.Discover qualified as Clang++import C.Operators (BinaryOp (..), Op (..), UnaryOp (..), opResType, pprOp,+                    pprOpApp)+import CallClang (CType (..), getExpansionTypeMapping, queryClangForResultType)++--------------------------------------------------------------------------------++main :: IO ()+main = do+  resourceDirArgs <- clangResourceDirArgs+  let stdClangArg = "-std=c17"  -- C23 arg depends on libclang version+      targetArgs = case platformOS hostPlatform of+        Windows -> [ "-target", "x86_64-unknown-mingw32" ]+        Posix+          -- On macOS, test against the native target and the system SDK headers+          -- rather than cross-compiling to Linux (for which the headers are+          -- absent). Linux uses an explicit target for reproducibility.+          | Info.os == "darwin" -> []+          | otherwise           -> [ "-target", "x86_64-pc-linux" ]+      clangArgs = Clang.ClangArgs $ stdClangArg : targetArgs ++ resourceDirArgs+      extendedInts = [ PtrDiff ]+  canonTys <-+    getExpansionTypeMapping clangArgs+      [ CType $ Arithmetic $ Integral $ IntLike extInt+      | extInt <- extendedInts+      ]++{-+  -- Quick debugging+  putStrLn $ "Canonical type mapping: " ++ show canonTys+  let intTy  = Arithmetic $ Integral $ IntLike $ Int Signed+      ptrTy1 = Ptr $ Arithmetic $ Integral $ IntLike $ Int Signed+  testRes <- queryClangForResultType ( ptrTy1 ::: intTy ::: VNil ) ( pprOpApp ( BinaryOp MRelEQ ) )+  putStrLn $ "Result of ty_1* == int: " ++ show testRes+-}++  putStrLn "Unary operators"+  unaries <- unaryTests hostPlatform clangArgs canonTys+  badUnary <-+    fmap catMaybes <$> for unaries $ \ ( op, tests ) -> do+      putStrLn $ pprOp ( UnaryOp op )+      let ( ok, bad ) = partitionTests tests+      if null bad+      then do+        putStrLn $ "   PASSED (" ++ show (length ok) ++ " tests)"+        pure Nothing+      else do+        putStrLn $ unlines $+          ( "   FAILED:" )+          : map ( showFailure . first show ) bad+        pure $ Just bad+  putStrLn "Binary operators"+  binaries <- binaryTests hostPlatform clangArgs canonTys+  badBinary <-+    fmap catMaybes <$> for binaries $ \ ( op, tests ) -> do+      putStrLn $ pprOp ( BinaryOp op )+      let ( ok, bad ) = partitionTests tests+      if null bad+      then do+        putStrLn $ "   PASSED (" ++ show (length ok) ++ " tests)"+        pure Nothing+      else do+        putStrLn $ unlines $+            "   FAILED:"+          : map ( showFailure . first show ) bad+        pure $ Just bad+  if null badUnary && null badBinary+  then exitSuccess+  else exitFailure+++clangResourceDirArgs :: IO [ String ]+clangResourceDirArgs = do+  let noTrace _ _ = pure ()+  paths <- Clang.getPaths noTrace Clang.BuiltinIncDirClang+  case Clang.pBuiltinIncDir paths of+    Just dir -> do+      putStrLn $ "Clang builtin include directory is: " ++ dir+      pure [ "-isystem", dir ]+    _ -> do+      putStrLn $ unlines [+          "WARNING: could not determine Clang's builtin include directory, falling back to libclang's own resolution."+        , "Builtin headers (stddef.h, ...) may not be found."+        ]+      pure []++showFailure :: ( String, ( Maybe CType, Maybe CType, [ Text ] ) ) -> String+showFailure ( input, ( mbOurs, mbClang, diags ) ) =+  unlines $+       [ "   " ++ input+       , "     - computed type: " ++ showMaybeType mbOurs+       , "     -  Clang's type: " ++ showMaybeType mbClang+       ]+    ++ [ "     - Clang's diagnostics:"+       | not ( null diags ) ]+    ++ [ "         " ++ l+       | d <- diags+       , l <- lines ( Text.unpack d ) ]+  where+    showMaybeType Nothing     = "<n/a>"+    showMaybeType ( Just ty ) = show ty++data TestResult a+  = TestOK !a+  | TestFailed {+        ours       :: !a+      , clang's    :: !a+      , clangDiags :: ![ Text ]+      }+  deriving stock Show++partitionTests ::+     [ ( x, TestResult a ) ]+  -> ( [ ( x, a ) ], [ ( x, ( a, a, [ Text ] ) ) ] )+partitionTests = foldMap $ \case+  ( x, TestOK a )            -> ( [ ( x, a ) ], []                        )+  ( x, TestFailed b1 b2 ds ) -> ( []          , [ ( x, ( b1, b2, ds ) ) ] )++eqTypeUpToExpansion :: Map CType CType -> Maybe CType -> Maybe CType -> Bool+eqTypeUpToExpansion canonTys ourTy clangTy = go ourTy+  where+    go mbTy+      | mbTy == clangTy+      = True+      | Just ty <- mbTy+      , Just ty' <- Map.lookup ty canonTys+      = go ( Just ty' )+      | otherwise+      = False++unaryTests :: Platform -> Clang.ClangArgs -> Map CType CType -> IO [ ( UnaryOp, [ ( CType, TestResult ( Maybe CType ) ) ] ) ]+unaryTests platform clangArgs canonTys =+  sequence+    [ ( op, ) <$> sequence+         [ do let ours = CType <$> opResType platform ( UnaryOp op ) ( ty ::: VNil )+              ( clang's, clangDiags ) <-+                queryClangForResultType+                  clangArgs+                  ( CType ty ::: VNil )+                  ( pprOpApp ( UnaryOp op ) )+              pure $ ( CType ty , ) $+                if eqTypeUpToExpansion canonTys ours clang's+                then TestOK ours+                else TestFailed { ours, clang's, clangDiags }+         | ( ty ::: VNil ) <- mkCTypes <$> enumerateTypeTuples @( S Z )+         ]+    | op <- [ ( minBound :: UnaryOp ) .. maxBound ] ]+++binaryTests :: Platform -> Clang.ClangArgs -> Map CType CType -> IO [ ( BinaryOp, [ ( ( CType, CType ), TestResult ( Maybe CType ) ) ] ) ]+binaryTests platform clangArgs canonTys =+  sequence+    [ ( op, ) <$>+      sequence+        [ do let ours = CType <$> opResType platform ( BinaryOp op ) ( ty1 ::: ty2 ::: VNil )+             ( clang's, clangDiags ) <-+               queryClangForResultType+                 clangArgs+                 ( CType ty1 ::: CType ty2 ::: VNil )+                 ( pprOpApp ( BinaryOp op ) )+             pure $ ( ( CType ty1, CType ty2 ), ) $+               if eqTypeUpToExpansion canonTys ours clang's+               then TestOK ours+               else TestFailed { ours, clang's, clangDiags }+        | ( ty1 ::: ty2 ::: VNil ) <- mkCTypes <$> enumerateTypeTuples @( S ( S Z ) )+        ]+    | op <- [ ( minBound :: BinaryOp ) .. maxBound ] ]++mkCTypes :: Vec n ( Type OpaqueTy ) -> Vec n ( Type CType )+mkCTypes = fmap $ fmap $ \ ( OpaqueTy i ) -> TypeDef $ Text.pack ( "ty_" ++ show i )