diff --git a/CHANGELOG.md b/CHANGELOG.md new file mode 100644 --- /dev/null +++ b/CHANGELOG.md @@ -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. diff --git a/LICENSE b/LICENSE new file mode 100644 --- /dev/null +++ b/LICENSE @@ -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. diff --git a/README.md b/README.md new file mode 100644 --- /dev/null +++ b/README.md @@ -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]: +[LLVM/Clang]: +[`c-expr-dsl`]: +[`hs-bindgen`]: +[main README]: +[changelog]: diff --git a/c-expr-runtime.cabal b/c-expr-runtime.cabal new file mode 100644 --- /dev/null +++ b/c-expr-runtime.cabal @@ -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 diff --git a/core/C/Operator/Classes.hs b/core/C/Operator/Classes.hs new file mode 100644 --- /dev/null +++ b/core/C/Operator/Classes.hs @@ -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 + +-------------------------------------------------------------------------------- diff --git a/core/C/Operator/GenInstances.hs b/core/C/Operator/GenInstances.hs new file mode 100644 --- /dev/null +++ b/core/C/Operator/GenInstances.hs @@ -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 + } diff --git a/core/C/Operator/Internal.hs b/core/C/Operator/Internal.hs new file mode 100644 --- /dev/null +++ b/core/C/Operator/Internal.hs @@ -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 + -- + -- 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 + -- + -- 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 + -- + -- 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 + +-------------------------------------------------------------------------------- diff --git a/core/C/Operator/TH.hs b/core/C/Operator/TH.hs new file mode 100644 --- /dev/null +++ b/core/C/Operator/TH.hs @@ -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 diff --git a/core/C/Operators.hs b/core/C/Operators.hs new file mode 100644 --- /dev/null +++ b/core/C/Operators.hs @@ -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 diff --git a/core/C/Type.hs b/core/C/Type.hs new file mode 100644 --- /dev/null +++ b/core/C/Type.hs @@ -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 + -- + -- 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 diff --git a/core/C/Type/Internal/Universe.hs b/core/C/Type/Internal/Universe.hs new file mode 100644 --- /dev/null +++ b/core/C/Type/Internal/Universe.hs @@ -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 ] diff --git a/lib/C/Expr/HostPlatform.hs b/lib/C/Expr/HostPlatform.hs new file mode 100644 --- /dev/null +++ b/lib/C/Expr/HostPlatform.hs @@ -0,0 +1,54 @@ +{-# LANGUAGE CPP #-} + +#include + +-- 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 diff --git a/lib/C/Expr/Posix32.hs b/lib/C/Expr/Posix32.hs new file mode 100644 --- /dev/null +++ b/lib/C/Expr/Posix32.hs @@ -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 + } + ) ) diff --git a/lib/C/Expr/Posix64.hs b/lib/C/Expr/Posix64.hs new file mode 100644 --- /dev/null +++ b/lib/C/Expr/Posix64.hs @@ -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 + } + ) ) diff --git a/lib/C/Expr/Win64.hs b/lib/C/Expr/Win64.hs new file mode 100644 --- /dev/null +++ b/lib/C/Expr/Win64.hs @@ -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 + } + ) ) diff --git a/test/CallClang.hs b/test/CallClang.hs new file mode 100644 --- /dev/null +++ b/test/CallClang.hs @@ -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 " ] + , [ 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 @@. +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 " + , "#include " + , "#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 diff --git a/test/Main.hs b/test/Main.hs new file mode 100644 --- /dev/null +++ b/test/Main.hs @@ -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 = "" + 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 )