diff --git a/LICENSE b/LICENSE new file mode 100644 --- /dev/null +++ b/LICENSE @@ -0,0 +1,30 @@ +Copyright (c) 2015, Csaba Hruska, Péter Diviánszky, Dániel Pék, Andor Pénzes + +All rights reserved. + +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 Csaba Hruska, Peter Divianszky nor the names of other + 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 +OWNER 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/Setup.hs b/Setup.hs new file mode 100644 --- /dev/null +++ b/Setup.hs @@ -0,0 +1,2 @@ +import Distribution.Simple +main = defaultMain diff --git a/lambdacube-compiler.cabal b/lambdacube-compiler.cabal new file mode 100644 --- /dev/null +++ b/lambdacube-compiler.cabal @@ -0,0 +1,201 @@ +-- Initial lambdacube-dsl.cabal generated by cabal init. For further +-- documentation, see http://haskell.org/cabal/users-guide/ + +name: lambdacube-compiler +version: 0.4.0.0 +homepage: http://lambdacube3d.com +synopsis: LambdaCube 3D is a DSL to program GPUs +description: LambdaCube 3D is a domain specific language and library that makes it + possible to program GPUs in a purely functional style. +license: BSD3 +license-file: LICENSE +author: Csaba Hruska, Péter Diviánszky, Dániel Pék, Andor Pénzes +maintainer: csaba.hruska@gmail.com +category: Graphics, Compiler +build-type: Simple +cabal-version: >=1.10 + +Data-Files: + lc/Builtins.lc + lc/Internals.lc + lc/Prelude.lc + +Flag onlytestsuite + Description: Only compiles the library and testsuit + Default: False + +Flag profiling + Description: Enable profiling + Default: False + +Flag coverage + Description: Enable coverage reporting + Default: False + +source-repository head + type: git + location: https://github.com/lambdacube3d/lambdacube-compiler + +library + other-modules: + Paths_lambdacube_compiler + exposed-modules: + -- Compiler + LambdaCube.Compiler + LambdaCube.Compiler.Pretty + LambdaCube.Compiler.Lexer + LambdaCube.Compiler.Parser + LambdaCube.Compiler.Infer + LambdaCube.Compiler.CoreToIR + other-extensions: + LambdaCase + PatternSynonyms + ViewPatterns + TypeSynonymInstances + FlexibleInstances + NoMonomorphismRestriction + TypeFamilies + RecordWildCards + DeriveFunctor + DeriveFoldable + DeriveTraversable + GeneralizedNewtypeDeriving + OverloadedStrings + TupleSections + MonadComprehensions + ExistentialQuantification + ScopedTypeVariables + ParallelListComp + + -- CAUTION: When the build-depends change, please bump the git submodule in lambdacube-docker repository + build-depends: + aeson >= 0.9 && <1, + base >=4.7 && <4.9, + containers >=0.5 && <0.6, + deepseq, + directory, + exceptions >= 0.8 && <0.9, + filepath, + mtl >=2.2 && <2.3, + parsec >= 3.1.9 && <3.2, +-- megaparsec >= 4.3.0 && <4.4, + indentation >= 0.2 && <0.3, + pretty-compact >=1.0 && <1.1, + text >= 1.2 && <1.3, + lambdacube-ir == 0.2.*, + vector >= 0.11 && <0.12 + + hs-source-dirs: src + default-language: Haskell2010 + + if flag(profiling) + GHC-Options: -fprof-auto -rtsopts + + +executable lambdacube-compiler-unit-tests + hs-source-dirs: test + main-is: UnitTests.hs + default-language: Haskell2010 + + -- CAUTION: When the build-depends change, please bump the git submodule in lambdacube-docker repository + build-depends: + base < 4.9, + containers >=0.5 && <0.6, + lambdacube-compiler, + parsec >= 3.1.9 && <3.2, + QuickCheck >= 2.8.2 && <2.9, + tasty >= 0.11 && <0.12, + tasty-quickcheck >=0.8 && <0.9 + + if flag(onlytestsuite) + Buildable: False + else + Buildable: True + +executable lambdacube-compiler-test-suite + hs-source-dirs: test + main-is: runTests.hs + default-language: Haskell2010 + + -- CAUTION: When the build-depends change, please bump the git submodule in lambdacube-docker repository + build-depends: + aeson >= 0.9 && <1, + async >= 2.0 && <2.1, + base < 4.9, + containers >=0.5 && <0.6, + deepseq, + directory, + exceptions >= 0.8 && <0.9, + filepath, + lambdacube-compiler, + mtl >=2.2 && <2.3, + monad-control >= 1.0 && <1.1, + optparse-applicative == 0.12.*, + parsec >= 3.1.9 && <3.2, + indentation >= 0.2 && <0.3, + pretty-compact >=1.0 && <1.1, + text >= 1.2 && <1.3, + time >= 1.5 && <1.6, + lambdacube-ir == 0.2.*, + vector >= 0.11 && <0.12 + + if flag(profiling) + GHC-Options: -fprof-auto -rtsopts + + +executable lc + hs-source-dirs: tool + main-is: Compiler.hs + default-language: Haskell2010 + + -- CAUTION: When the build-depends change, please bump the git submodule in lambdacube-docker repository + build-depends: + base < 4.9, + lambdacube-compiler, + optparse-applicative == 0.12.*, + aeson >= 0.9 && < 0.11, + bytestring == 0.10.*, + filepath == 1.4.* + + if flag(onlytestsuite) + Buildable: False + else + Buildable: True + + +executable lambdacube-compiler-coverage-test-suite + hs-source-dirs: src, test + main-is: runTests.hs + default-language: Haskell2010 + + if flag(coverage) + Buildable: True + else + Buildable: False + + if flag(profiling) + GHC-Options: -fhpc -hpcdir dist/hpc/lambdacube-compiler -fprof-auto -rtsopts + else + GHC-Options: -fhpc -hpcdir dist/hpc/lambdacube-compiler + + -- CAUTION: When the build-depends change, please bump the git submodule in lambdacube-docker repository + build-depends: + aeson >= 0.9 && <1, + async >= 2.0 && <2.1, + base < 4.9, + containers >=0.5 && <0.6, + deepseq, + directory, + exceptions >= 0.8 && <0.9, + filepath, + lambdacube-ir == 0.2.*, + mtl >=2.2 && <2.3, + monad-control >= 1.0 && <1.1, + optparse-applicative == 0.12.*, + parsec >= 3.1.9 && <3.2, + indentation >= 0.2 && <0.3, + pretty-compact >=1.0 && <1.1, + text >= 1.2 && <1.3, + time >= 1.5 && <1.6, + vector >= 0.11 && <0.12 + diff --git a/lc/Builtins.lc b/lc/Builtins.lc new file mode 100644 --- /dev/null +++ b/lc/Builtins.lc @@ -0,0 +1,572 @@ +{-# LANGUAGE NoImplicitPrelude #-} +module Builtins + ( module Internals + , module Builtins + ) where + +import Internals + +id x = x + +--------------------------------------- + +class AttributeTuple a +instance AttributeTuple a -- TODO +class ValidOutput a +instance ValidOutput a -- TODO +class ValidFrameBuffer a +instance ValidFrameBuffer a -- TODO + +data VecS (a :: Type) :: Nat -> Type where + V2 :: a -> a -> VecS a 2 + V3 :: a -> a -> a -> VecS a 3 + V4 :: a -> a -> a -> a -> VecS a 4 + +type family Vec (n :: Nat) t where Vec n t = VecS t n + +type family VecScalar (n :: Nat) a where + VecScalar 1 a = a + VecScalar ('Succ ('Succ n)) a = Vec ('Succ ('Succ n)) a + +-- may be a data family? +type family TFVec (n :: Nat) a where + TFVec n a = Vec n a -- TODO: check range: n = 2,3,4; a is Float, Int, Word, Bool + +-- todo: use less constructors with more parameters +data Mat :: Nat -> Nat -> Type -> Type where + M22F :: Vec 2 Float -> Vec 2 Float -> Mat 2 2 Float + M32F :: Vec 3 Float -> Vec 3 Float -> Mat 3 2 Float + M42F :: Vec 4 Float -> Vec 4 Float -> Mat 4 2 Float + M23F :: Vec 2 Float -> Vec 2 Float -> Vec 2 Float -> Mat 2 3 Float + M33F :: Vec 3 Float -> Vec 3 Float -> Vec 3 Float -> Mat 3 3 Float + M43F :: Vec 4 Float -> Vec 4 Float -> Vec 4 Float -> Mat 4 3 Float + M24F :: Vec 2 Float -> Vec 2 Float -> Vec 2 Float -> Vec 2 Float -> Mat 2 4 Float + M34F :: Vec 3 Float -> Vec 3 Float -> Vec 3 Float -> Vec 3 Float -> Mat 3 4 Float + M44F :: Vec 4 Float -> Vec 4 Float -> Vec 4 Float -> Vec 4 Float -> Mat 4 4 Float + +type family MatVecScalarElem a where + MatVecScalarElem Float = Float + MatVecScalarElem Bool = Bool + MatVecScalarElem Int = Int + MatVecScalarElem (VecS a n) = a + MatVecScalarElem (Mat i j a) = a + +--------------------------------------- swizzling + +data Swizz = Sx | Sy | Sz | Sw + +-- todo: use pattern matching +mapVec :: forall a b m . (a -> b) -> Vec m a -> Vec m b +mapVec @a @b @m f v = 'VecSCase (\m _ -> 'Vec m b) + (\x y -> V2 (f x) (f y)) + (\x y z -> V3 (f x) (f y) (f z)) + (\x y z w -> V4 (f x) (f y) (f z) (f w)) + @m + v + +-- todo: make it more type safe +swizzscalar :: forall n . Vec n a -> Swizz -> a +swizzscalar (V2 x y) Sx = x +swizzscalar (V2 x y) Sy = y +swizzscalar (V3 x y z) Sx = x +swizzscalar (V3 x y z) Sy = y +swizzscalar (V3 x y z) Sz = z +swizzscalar (V4 x y z w) Sx = x +swizzscalar (V4 x y z w) Sy = y +swizzscalar (V4 x y z w) Sz = z +swizzscalar (V4 x y z w) Sw = w + +-- used to prevent unfolding of swizzvector on variables (behind GPU lambda) +definedVec :: forall a m . Vec m a -> Bool +definedVec (V2 _ _) = True +definedVec (V3 _ _ _) = True +definedVec (V4 _ _ _ _) = True + +swizzvector :: forall n . forall m . Vec n a -> Vec m Swizz -> Vec m a +swizzvector v w | definedVec v = mapVec (swizzscalar v) w + + +--------------------------------------- type classes + +class Signed a + +instance Signed Int +instance Signed Float + +class Component a where + zeroComp :: a + oneComp :: a + +instance Component Int where + zeroComp = 0 :: Int + oneComp = 1 :: Int +instance Component Word where + zeroComp = 0 :: Word + oneComp = 1 :: Word +instance Component Float where + zeroComp = 0.0 + oneComp = 1.0 +instance Component (VecS Float 2) where + zeroComp = V2 0.0 0.0 + oneComp = V2 1.0 1.0 +instance Component (VecS Float 3) where + zeroComp = V3 0.0 0.0 0.0 + oneComp = V3 1.0 1.0 1.0 +instance Component (VecS Float 4) where + zeroComp = V4 0.0 0.0 0.0 0.0 + oneComp = V4 1.0 1.0 1.0 1.0 +instance Component Bool where + zeroComp = False + oneComp = True +instance Component (VecS Bool 2) where + zeroComp = V2 False False + oneComp = V2 True True +instance Component (VecS Bool 3) where + zeroComp = V3 False False False + oneComp = V3 True True True +instance Component (VecS Bool 4) where + zeroComp = V4 False False False False + oneComp = V4 True True True True + +class Integral a + +instance Integral Int +instance Integral Word + +class Floating a + +instance Floating Float +instance Floating (VecS Float 2) -- todo: use Vec +instance Floating (VecS Float 3) +instance Floating (VecS Float 4) +instance Floating (Mat 2 2 Float) +instance Floating (Mat 2 3 Float) +instance Floating (Mat 2 4 Float) +instance Floating (Mat 3 2 Float) +instance Floating (Mat 3 3 Float) +instance Floating (Mat 3 4 Float) +instance Floating (Mat 4 2 Float) +instance Floating (Mat 4 3 Float) +instance Floating (Mat 4 4 Float) + +data BlendingFactor + = Zero' --- FIXME: modified + | One + | SrcColor + | OneMinusSrcColor + | DstColor + | OneMinusDstColor + | SrcAlpha + | OneMinusSrcAlpha + | DstAlpha + | OneMinusDstAlpha + | ConstantColor + | OneMinusConstantColor + | ConstantAlpha + | OneMinusConstantAlpha + | SrcAlphaSaturate + +data BlendEquation + = FuncAdd + | FuncSubtract + | FuncReverseSubtract + | Min + | Max + +data LogicOperation + = Clear + | And + | AndReverse + | Copy + | AndInverted + | Noop + | Xor + | Or + | Nor + | Equiv + | Invert + | OrReverse + | CopyInverted + | OrInverted + | Nand + | Set + +data StencilOperation + = OpZero + | OpKeep + | OpReplace + | OpIncr + | OpIncrWrap + | OpDecr + | OpDecrWrap + | OpInvert + +data ComparisonFunction + = Never + | Less + | Equal + | Lequal + | Greater + | Notequal + | Gequal + | Always + +data ProvokingVertex + = LastVertex + | FirstVertex + +data CullMode + = CullFront + | CullBack + | CullNone + +data PointSize a + = PointSize Float + | ProgramPointSize (a -> Float) + +data PolygonMode a + = PolygonFill + | PolygonPoint (PointSize a) + | PolygonLine Float + +data PolygonOffset + = NoOffset + | Offset Float Float + +data PointSpriteCoordOrigin + = LowerLeft + | UpperLeft + + +data Depth a where +data Stencil a where +data Color a where + +data PrimitiveType + = Triangle + | Line + | Point + | TriangleAdjacency + | LineAdjacency + +-- builtin +primTexture :: () -> Vec 2 Float -> Vec 4 Float + +-- builtins +Uniform :: String -> t +Attribute :: String -> t + +data RasterContext a :: PrimitiveType -> Type where + TriangleCtx :: CullMode -> PolygonMode a -> PolygonOffset -> ProvokingVertex -> RasterContext a Triangle + PointCtx :: PointSize a -> Float -> PointSpriteCoordOrigin -> RasterContext a Point + LineCtx :: Float -> ProvokingVertex -> RasterContext a Line + +type family FTRepr' a where + -- TODO + FTRepr' [a] = a + FTRepr' ([a], [b]) = (a, b) + +data Blending :: Type -> Type where + NoBlending :: Blending t + BlendLogicOp :: (Integral t) => LogicOperation -> Blending t + Blend :: (BlendEquation, BlendEquation) + -> ((BlendingFactor, BlendingFactor), (BlendingFactor, BlendingFactor)) + -> Vec 4 Float -> Blending Float + +{- TODO: more precise kinds + FragmentOperation :: Semantic -> * + FragmentOut :: Semantic -> * +-} + +data StencilTests +data StencilOps +data Int32 + +data FragmentOperation :: Type -> Type where + ColorOp :: (mask ~ VecScalar d Bool, color ~ VecScalar d c, Num c) => Blending c -> mask + -> FragmentOperation (Color color) + DepthOp :: ComparisonFunction -> Bool -> FragmentOperation (Depth Float) + StencilOp :: StencilTests -> StencilOps -> StencilOps -> FragmentOperation (Stencil Int32) +{- +type family FragOps a where + FragOps (FragmentOperation t) = t + FragOps (FragmentOperation t1, FragmentOperation t2) = (t1, t2) + FragOps (FragmentOperation t1, FragmentOperation t2, FragmentOperation t3) = (t1, t2, t3) + FragOps (FragmentOperation t1, FragmentOperation t2, FragmentOperation t3, FragmentOperation t4) = (t1, t2, t3, t4) + FragOps (FragmentOperation t1, FragmentOperation t2, FragmentOperation t3, FragmentOperation t4, FragmentOperation t5) = (t1, t2, t3, t4, t5) +-} +type family FragOps a where + FragOps (t1, t2) = (FragmentOperation t1, FragmentOperation t2) + FragOps (t1, t2, t3) = (FragmentOperation t1, FragmentOperation t2, FragmentOperation t3) + FragOps (t1, t2, t3, t4) = (FragmentOperation t1, FragmentOperation t2, FragmentOperation t3, FragmentOperation t4) + FragOps (t1, t2, t3, t4, t5) = (FragmentOperation t1, FragmentOperation t2, FragmentOperation t3, FragmentOperation t4, FragmentOperation t5) + FragOps t = (FragmentOperation t) + +[] ++ ys = ys +x:xs ++ ys = x : xs ++ ys + +foldr f e [] = e +foldr f e (x: xs) = f x (foldr f e xs) + +concat = foldr (++) [] + +map _ [] = [] +map f (x:xs) = f x : map f xs + +concatMap :: (a -> [b]) -> [a] -> [b] +concatMap f x = concat (map f x) + +data Primitive a :: PrimitiveType -> Type where + PrimPoint :: a -> Primitive a Point + PrimLine :: a -> a -> Primitive a Line + PrimTriangle :: a -> a -> a -> Primitive a Triangle + +type PrimitiveStream a t = [Primitive t a] + +mapPrimitive :: (a -> b) -> Primitive a p -> Primitive b p +{- todo +mapPrimitive f (PrimPoint a) = PrimPoint (f a) +mapPrimitive f (PrimLine a b) = PrimLine (f a) (f b) +mapPrimitive f (PrimTriangle a b c) = PrimTriangle (f a) (f b) (f c) +-} + +fetch_ :: forall a t . (AttributeTuple t) => String -> t -> PrimitiveStream a t +fetchArrays_ :: forall a t t' . (AttributeTuple t, t ~ FTRepr' t') => t' -> PrimitiveStream a t + +mapPrimitives :: (a -> b) -> PrimitiveStream p a -> PrimitiveStream p b +mapPrimitives f = map (mapPrimitive f) + +fetch s a t = fetch_ @a s t +fetchArrays a t = fetchArrays_ @a t + +type family RemSemantics a where + RemSemantics () = () + RemSemantics (Color a) = a + RemSemantics (Color a, Color b) = (a, b) + RemSemantics (Color a, Color b, Color c) = (a, b, c) + RemSemantics (Color a, Color b, Color c, Color d) = (a, b, c, d) + RemSemantics (Color a, Color b, Color c, Color d, Color e) = (a, b, c, d, e) + RemSemantics (Depth Float) = () + RemSemantics (Depth Float, Color a) = a + RemSemantics (Depth Float, Color a, Color b) = (a, b) + RemSemantics (Depth Float, Color a, Color b, Color c) = (a, b, c) + RemSemantics (Depth Float, Color a, Color b, Color c, Color d) = (a, b, c, d) + +------------------- + +data Maybe a + = Nothing + | Just a +-- deriving (Eq, Ord, Show) + +data Vector (n :: Nat) t + +type Fragment n t = Vector n (Maybe (SimpleFragment t)) + +data SimpleFragment t = SimpleFragment + { sFragmentCoords :: Vec 3 Float + , sFragmentValue :: t + } + +type FragmentStream n t = [Fragment n t] + +customizeDepth :: (a -> Float) -> Fragment n a -> Fragment n a + +customizeDepths :: (a -> Float) -> FragmentStream n a -> FragmentStream n a +customizeDepths f = map (customizeDepth f) + +filterFragment :: (a -> Bool) -> Fragment n a -> Fragment n a + +filterFragments :: (a -> Bool) -> FragmentStream n a -> FragmentStream n a +filterFragments p = map (filterFragment p) + +mapFragment :: (a -> b) -> Fragment n a -> Fragment n b + +mapFragments :: (a -> b) -> FragmentStream n a -> FragmentStream n b +mapFragments f = map (mapFragment f) + + +data Interpolated t where + Smooth, NoPerspective + :: (Floating t) => Interpolated t + Flat :: Interpolated t + +type family InterpolatedType a where + InterpolatedType () = () + InterpolatedType (Interpolated a) = a + InterpolatedType (Interpolated a, Interpolated b) = (a, b) + InterpolatedType (Interpolated a, Interpolated b, Interpolated c) = (a, b, c) + +rasterizePrimitive + :: ( b ~ InterpolatedType interpolation + , a ~ JoinTupleType (Vec 4 Float) b ) + => interpolation -- tuple of Smooth & Flat + -> RasterContext a x + -> Primitive a x + -> FragmentStream 1 b + +rasterizePrimitives ctx is s = concat (map (rasterizePrimitive is ctx) s) + +data Image :: Nat -> Type -> Type + +ColorImage :: forall a d t color . (Num t, color ~ VecScalar d t) + => color -> Image a (Color color) +DepthImage :: forall a . Float -> Image a (Depth Float) +StencilImage :: forall a . Int -> Image a (Stencil Int) + +type family SameLayerCounts a where + SameLayerCounts (Image n1 t1) = Unit + SameLayerCounts (Image n1 t1, Image n2 t2) = EqCT Nat n1 n2 + SameLayerCounts (Image n1 t1, Image n2 t2, Image n3 t3) = T2 (EqCT Nat n1 n2) (EqCT Nat n1 n3) + +class DefaultFragOp a where defaultFragOp :: FragmentOperation a +instance DefaultFragOp (Color (VecS Float 4)) where defaultFragOp = ColorOp NoBlending (V4 True True True True) +instance DefaultFragOp (Depth Float) where defaultFragOp = DepthOp Less True +{- +class DefaultFragOps a where defaultFragOps :: a +instance (DefaultFragOp a, DefaultFragOp b) => DefaultFragOps (FragmentOperation a, FragmentOperation b) where + defaultFragOps = -- (undefined @(), undefined) + (defaultFragOp @a @_, defaultFragOp @b @_) +-} +data FrameBuffer (n :: Nat) t +Accumulate :: FragOps b -> FragmentStream n (RemSemantics b) -> FrameBuffer n b -> FrameBuffer n b + +type family TFFrameBuffer a where + TFFrameBuffer (Image n1 t1) = FrameBuffer n1 t1 + TFFrameBuffer (Image n1 t1, Image n2 t2) = FrameBuffer n1 (t1, t2) + TFFrameBuffer (Image n1 t1, Image n2 t2, Image n3 t3) = FrameBuffer n1 (t1, t2, t3) + +FrameBuffer :: (ValidFrameBuffer b, SameLayerCounts a, FrameBuffer n b ~ TFFrameBuffer a) => a -> FrameBuffer n b + +accumulate ctx fshader fstr fb = Accumulate ctx (mapFragments fshader fstr) fb + +accumulationContext x = x + +-- texture support +PrjImage :: FrameBuffer 1 a -> Image 1 a +PrjImageColor :: FrameBuffer 1 (Depth Float, Color (Vec 4 Float)) -> Image 1 (Color (Vec 4 Float)) + +data Output where + ScreenOut :: FrameBuffer a b -> Output + +------------------------------------------------------------------- +-- * Builtin Primitive Functions * +-- Arithmetic Functions (componentwise) + +PrimAdd, PrimSub, PrimMul :: Num (MatVecScalarElem a) => a -> a -> a +PrimAddS, PrimSubS, PrimMulS :: (t ~ MatVecScalarElem a, Num t) => a -> t -> a +PrimDiv, PrimMod :: (Num t, a ~ VecScalar d t) => a -> a -> a +PrimDivS, PrimModS :: (Num t, a ~ VecScalar d t) => a -> t -> a +PrimNeg :: Signed (MatVecScalarElem a) => a -> a +-- Bit-wise Functions +PrimBAnd, PrimBOr, PrimBXor :: (Integral t, a ~ VecScalar d t) => a -> a -> a +PrimBAndS, PrimBOrS, PrimBXorS:: (Integral t, a ~ VecScalar d t) => a -> t -> a +PrimBNot :: (Integral t, a ~ VecScalar d t) => a -> a +PrimBShiftL, PrimBShiftR :: (Integral t, a ~ VecScalar d t, b ~ VecScalar d Word) => a -> b -> a +PrimBShiftLS, PrimBShiftRS :: (Integral t, a ~ VecScalar d t) => a -> Word -> a +-- Logic Functions +PrimAnd, PrimOr, PrimXor :: Bool -> Bool -> Bool +PrimNot :: (a ~ VecScalar d Bool) => a -> a +PrimAny, PrimAll :: VecScalar d Bool -> Bool + +-- Angle, Trigonometry and Exponential Functions +PrimACos, PrimACosH, PrimASin, PrimASinH, PrimATan, PrimATanH, PrimCos, PrimCosH, PrimDegrees, PrimRadians, PrimSin, PrimSinH, PrimTan, PrimTanH, PrimExp, PrimLog, PrimExp2, PrimLog2, PrimSqrt, PrimInvSqrt + :: (a ~ VecScalar d Float) => a -> a +PrimPow, PrimATan2 :: (a ~ VecScalar d Float) => a -> a -> a +-- Common Functions +PrimFloor, PrimTrunc, PrimRound, PrimRoundEven, PrimCeil, PrimFract + :: (a ~ VecScalar d Float) => a -> a +PrimMin, PrimMax :: (Num t, a ~ VecScalar d t) => a -> a -> a +PrimMinS, PrimMaxS :: (Num t, a ~ VecScalar d t) => a -> t -> a +PrimIsNan, PrimIsInf :: (a ~ VecScalar d Float, b ~ VecScalar d Bool) => a -> b +PrimAbs, PrimSign :: (Signed t, a ~ VecScalar d t) => a -> a +PrimModF :: (a ~ VecScalar d Float) => a -> (a, a) +PrimClamp :: (Num t, a ~ VecScalar d t) => a -> a -> a -> a +PrimClampS :: (Num t, a ~ VecScalar d t) => a -> t -> t -> a +PrimMix :: (a ~ VecScalar d Float) => a -> a -> a -> a +PrimMixS :: (a ~ VecScalar d Float) => a -> a -> Float -> a +PrimMixB :: (a ~ VecScalar d Float, b ~ VecScalar d Bool) => a -> a -> b -> a +PrimStep :: (a ~ TFVec d Float) => a -> a -> a +PrimStepS :: (a ~ VecScalar d Float) => Float -> a -> a +PrimSmoothStep :: (a ~ TFVec d Float) => a -> a -> a -> a +PrimSmoothStepS :: (a ~ VecScalar d Float) => Float -> Float -> a -> a + +-- Integer/Floatonversion Functions +PrimFloatBitsToInt :: VecScalar d Float -> VecScalar d Int +PrimFloatBitsToUInt :: VecScalar d Float -> VecScalar d Word +PrimIntBitsToFloat :: VecScalar d Int -> VecScalar d Float +PrimUIntBitsToFloat :: VecScalar d Word -> VecScalar d Float +-- Geometric Functions +PrimLength :: (a ~ VecScalar d Float) => a -> Float +PrimDistance, PrimDot :: (a ~ VecScalar d Float) => a -> a -> Float +PrimCross :: (a ~ VecScalar 3 Float) => a -> a -> a +PrimNormalize :: (a ~ VecScalar d Float) => a -> a +PrimFaceForward, PrimRefract :: (a ~ VecScalar d Float) => a -> a -> a -> a +PrimReflect :: (a ~ VecScalar d Float) => a -> a -> a +-- Matrix Functions +PrimTranspose :: Mat h w a -> Mat w h a +PrimDeterminant :: Mat s s a -> Float +PrimInverse :: Mat s s a -> Mat s s a +PrimOuterProduct :: Vec w a -> Vec h a -> Mat h w a +PrimMulMatVec :: Mat h w a -> Vec w a -> Vec h a +PrimMulVecMat :: Vec h a -> Mat h w a -> Vec w a +PrimMulMatMat :: Mat i j a -> Mat j k a -> Mat i k a +-- Vector and Scalar Relational Functions +PrimLessThan, PrimLessThanEqual, PrimGreaterThan, PrimGreaterThanEqual, PrimEqualV, PrimNotEqualV + :: (Num t, a ~ VecScalar d t, b ~ VecScalar d Bool) => a -> a -> b +PrimEqual, PrimNotEqual :: (t ~ MatVecScalarElem a) => a -> a -> Bool +-- Fragment Processing Functions +PrimDFdx, PrimDFdy, PrimFWidth + :: (a ~ VecScalar d Float) => a -> a +-- Noise Functions +PrimNoise1 :: VecScalar d Float -> Float +PrimNoise2 :: VecScalar d Float -> Vec 2 Float +PrimNoise3 :: VecScalar d Float -> Vec 3 Float +PrimNoise4 :: VecScalar d Float -> Vec 4 Float + +{- +-- Vec/Mat (de)construction +PrimTupToV2 :: Component a => PrimFun stage ((a,a) -> V2 a) +PrimTupToV3 :: Component a => PrimFun stage ((a,a,a) -> V3 a) +PrimTupToV4 :: Component a => PrimFun stage ((a,a,a,a) -> V4 a) +PrimV2ToTup :: Component a => PrimFun stage (V2 a -> (a,a)) +PrimV3ToTup :: Component a => PrimFun stage (V3 a -> (a,a,a)) +PrimV4ToTup :: Component a => PrimFun stage (V4 a -> (a,a,a,a)) +-} + +-------------------- +-- * Texture support +-- FIXME: currently only Float RGBA 2D texture is supported + +data Texture where + Texture2DSlot :: String -- texture slot name + -> Texture + + Texture2D :: Vec 2 Int -- FIXME: use Word here + -> Image 1 (Color (Vec 4 Float)) + -> Texture + +data Filter + = PointFilter + | LinearFilter + +data EdgeMode + = Repeat + | MirroredRepeat + | ClampToEdge + +data Sampler = Sampler Filter EdgeMode Texture + +-- builtin +texture2D :: Sampler -> Vec 2 Float -> Vec 4 Float + + +accumulateWith ctx x = (ctx, x) +overlay cl (ctx, str) = Accumulate ctx str cl +renderFrame = ScreenOut +imageFrame = FrameBuffer +emptyDepthImage = DepthImage @1 +emptyColorImage = ColorImage @1 + +infixl 0 `overlay` + diff --git a/lc/Internals.lc b/lc/Internals.lc new file mode 100644 --- /dev/null +++ b/lc/Internals.lc @@ -0,0 +1,133 @@ +{-# LANGUAGE NoImplicitPrelude #-} +-- declarations of builtin functions and data types used by the compiler +module Internals where + +-- used for type annotations +typeAnn x = x + +undefined :: forall (a :: Type) . a + +primFix :: forall (a :: Type) . (a -> a) -> a + +data Unit = TT +data String +data Empty (a :: String) + +-- TODO: generate? +data Tuple0 = Tuple0 +data Tuple1 a = Tuple1 a +data Tuple2 a b = Tuple2 a b +data Tuple3 a b c = Tuple3 a b c +data Tuple4 a b c d = Tuple4 a b c d +data Tuple5 a b c d e = Tuple5 a b c d e + +-- ... TODO + +-- builtin used for overlapping instances +parEval :: forall a -> a -> a -> a + +type family JoinTupleType t1 t2 where + -- TODO + JoinTupleType a () = a + JoinTupleType a (b, c) = (a, b, c) + JoinTupleType a (b, c, d) = (a, b, c, d) + JoinTupleType a (b, c, d, e) = (a, b, c, d, e) + JoinTupleType a b = (a, b) + +-- conjuction of constraints +type family T2 a b + +-- equality constraints +type family EqCT (t :: Type) (a :: t) (b :: t) + +type EqCTt = EqCT Type + +--type instance EqCT t (a, b) (JoinTupleType a' b') = T2 (EqCT Type a a') (EqCT Type b b') + +-- builtin conjuction of constraint witnesses +t2C :: Unit -> Unit -> Unit + +-- builtin type constructors +data Int +data Word +data Float +data Char + +data Bool = False | True + +data Ordering = LT | EQ | GT + +data Nat = Zero | Succ Nat + +-- builtin primitives +primIntToWord :: Int -> Word +primIntToFloat :: Int -> Float +primIntToNat :: Int -> Nat +primCompareInt :: Int -> Int -> Ordering +primCompareWord :: Word -> Word -> Ordering +primCompareFloat :: Float -> Float -> Ordering +primCompareChar :: Char -> Char -> Ordering +primCompareString :: String -> String -> Ordering +primNegateInt :: Int -> Int +primNegateWord :: Word -> Word +primNegateFloat :: Float -> Float +primAddInt :: Int -> Int -> Int +primSubInt :: Int -> Int -> Int +primModInt :: Int -> Int -> Int +primSqrtFloat :: Float -> Float +primRound :: Float -> Int + + +primIfThenElse :: Bool -> a -> a -> a +primIfThenElse True a b = a +primIfThenElse False a b = b + +isEQ EQ = True +isEQ _ = False + +-- fromInt is needed for integer literal +class Num a where + fromInt :: Int -> a + compare :: a -> a -> Ordering + negate :: a -> a + +instance Num Int where + fromInt = \x -> x + compare = primCompareInt + negate = primNegateInt +instance Num Word where + fromInt = primIntToWord + compare = primCompareWord + negate = primNegateWord +instance Num Float where + fromInt = primIntToFloat + compare = primCompareFloat + negate = primNegateFloat +instance Num Nat where + fromInt = primIntToNat --if isEQ (primCompareInt n zero') then Zero else Succ (fromInt (primSubInt n one')) + compare = undefined + negate = undefined + +class Eq a where + (==) :: a -> a -> Bool -- todo: use (==) sign + +infix 4 == + +instance Eq String where a == b = isEQ (primCompareString a b) +instance Eq Char where a == b = isEQ (primCompareChar a b) +instance Eq Int where a == b = isEQ (primCompareInt a b) +instance Eq Float where a == b = isEQ (primCompareFloat a b) +instance Eq Bool where + True == True = True + False == False = True + _ == _ = False +instance Eq Nat where + Zero == Zero = True + Succ a == Succ b = a == b + _ == _ = False + +data List a = Nil | Cons a (List a) + +infixr 5 : + + diff --git a/lc/Prelude.lc b/lc/Prelude.lc new file mode 100644 --- /dev/null +++ b/lc/Prelude.lc @@ -0,0 +1,364 @@ +{-# LANGUAGE NoImplicitPrelude #-} +module Prelude + ( module Prelude + , module Builtins + ) where + +import Builtins + +infixr 9 . +infixl 7 `PrimMulMatVec`, `PrimDot` +infixr 5 ++ +infixr 3 *** +infixr 0 $ +--infixl 0 & + +const x y = x + +otherwise = True + +x & f = f x + +($) = \f x -> f x +(.) = \f g x -> f (g x) + +uncurry f (x, y) = f x y + +(***) f g (x, y) = (f x, g y) + +pi = 3.14 + +zip :: [a] -> [b] -> [(a,b)] +zip [] xs = [] +zip xs [] = [] +zip (a: as) (b: bs) = (a,b): zip as bs + +unzip :: [(a,b)] -> ([a],[b]) +unzip [] = ([],[]) +unzip ((a,b):xs) = (a:as,b:bs) + where (as,bs) = unzip xs + +filter pred [] = [] +filter pred (x:xs) = case pred x of + True -> (x : filter pred xs) + False -> (filter pred xs) + +head :: [a] -> a +head (a: _) = a + +tail :: [a] -> [a] +tail (_: xs) = xs + +pairs :: [a] -> [(a, a)] +pairs v = zip v (tail v) + +foldl' f e [] = e +foldl' f e (x: xs) = foldl' f (f e x) xs + +foldr1 f (x: xs) = foldr f x xs + +split [] = ([], []) +split (x: xs) = (x: bs, as) where (as, bs) = split xs + +mergeBy f (x:xs) (y:ys) = case f x y of + LT -> x: mergeBy f xs (y:ys) + _ -> y: mergeBy f (x:xs) ys +mergeBy f [] xs = xs +mergeBy f xs [] = xs + +sortBy f [] = [] +sortBy f [x] = [x] +sortBy f xs = uncurry (mergeBy f) ((sortBy f *** sortBy f) (split xs)) + +iterate :: (a -> a) -> a -> [a] +iterate f x = x : iterate f (f x) + +fst (a, b) = a +snd (a, b) = b + +tuptype :: [Type] -> Type +tuptype [] = '() +tuptype (x:xs) = '(x, tuptype xs) + +data RecordC (xs :: [(String, Type)]) + = RecordCons (tuptype (map snd xs)) + +False ||| x = x +True ||| x = True + +infixr 2 ||| + +True &&& x = x +False &&& x = False + +infixr 3 &&& + +------------------------------------ Row polymorphism +-- todo: sorted field names (more efficient & easier to use) + +{- +isKey _ [] = False +isKey s ((s', _): ss) = s == s' ||| isKey s ss + +subList [] _ = [] +subList ((s, t): xs) ys = if isKey s ys then subList xs ys else (s, t): subList xs ys + +addList [] ys = ys +addList ((s, t): xs) ys = if isKey s ys then addList xs ys else (s, t): addList xs ys + +findEq x [] = 'Unit +findEq (s, t) ((s', t'):xs) = if s == s' then 'T2 (t ~ t') (findEq (s, t) xs) else findEq (s, t) xs + +sameEq [] _ = 'Unit +sameEq (x: xs) ys = 'T2 (findEq x ys) (sameEq xs ys) + +defined [] = True +defined (x: xs) = defined xs + +type family Split a b c +type instance Split (RecordC xs) (RecordC ys) z | defined xs &&& defined ys = T2 (sameEq xs ys) (z ~ RecordC (subList xs ys)) +type instance Split (RecordC xs) z (RecordC ys) | defined xs &&& defined ys = T2 (sameEq xs ys) (z ~ RecordC (subList xs ys)) +type instance Split z (RecordC xs) (RecordC ys) | defined xs &&& defined ys = T2 (sameEq xs ys) (z ~ RecordC (addList xs ys)) + +-- builtin +-- TODO +record :: [(String, Type)] -> Type +--record xs = RecordCons ({- TODO: sortBy fst-} xs) +-} +-- builtin +unsafeCoerce :: forall a b . a -> b + +isKeyC _ _ [] = 'Empty "" +isKeyC s t ((s', t'): ss) = if s == s' then t ~ t' else isKeyC s t ss + +-- todo: don't use unsafeCoerce +project :: forall a (xs :: [(String, Type)]) . forall (s :: String) -> 'isKeyC s a xs => RecordC xs -> a +project @a @((s', a'): xs) s @_ (RecordCons ts) | s == s' = fst (unsafeCoerce @_ @(a, tuptype (map snd xs)) ts) +project @a @((s', a'): xs) s @_ (RecordCons ts) = project @a @xs s @(undefined @(isKeyC s a xs)) (RecordCons (snd (unsafeCoerce @_ @(a, tuptype (map snd xs)) ts))) + +--------------------------------------- HTML colors + +rgb r g b = V4 r g b 1.0 + +black = rgb 0.0 0.0 0.0 +gray = rgb 0.5 0.5 0.5 +silver = rgb 0.75 0.75 0.75 +white = rgb 1.0 1.0 1.0 +maroon = rgb 0.5 0.0 0.0 +red = rgb 1.0 0.0 0.0 +olive = rgb 0.5 0.5 0.0 +yellow = rgb 1.0 1.0 0.0 +green = rgb 0.0 0.5 0.0 +lime = rgb 0.0 1.0 0.0 +teal = rgb 0.0 0.5 0.5 +aqua = rgb 0.0 1.0 1.0 +navy = rgb 0.0 0.0 0.5 +blue = rgb 0.0 0.0 1.0 +purple = rgb 0.5 0.0 0.5 +fuchsia = rgb 1.0 0.0 1.0 + +colorImage1 = ColorImage @1 +colorImage2 = ColorImage @2 + +depthImage1 = DepthImage @1 + +v3FToV4F :: Vec 3 Float -> Vec 4 Float +v3FToV4F v = V4 v%x v%y v%z 1 + +------------ +-- * WebGL 1 +------------ + +-- angle and trigonometric +radians = PrimRadians +degrees = PrimDegrees +sin = PrimSin +cos = PrimCos +tan = PrimTan +sinh = PrimSinH +cosh = PrimCosH +tanh = PrimTanH +asin = PrimASin +asinh = PrimASinH +acos = PrimACos +acosh = PrimACosH +atan = PrimATan +atanh = PrimATanH +atan2 = PrimATan2 + +-- exponential functions +pow = PrimPow +exp = PrimExp +log = PrimLog +exp2 = PrimExp2 +log2 = PrimLog2 +sqrt = PrimSqrt +inversesqrt = PrimInvSqrt + +-- common functions +abs = PrimAbs +sign = PrimSign +floor = PrimFloor +trunc = PrimTrunc +round = PrimRound +roundEven = PrimRoundEven +ceil = PrimCeil +fract = PrimFract +mod = PrimMod +min = PrimMin +max = PrimMax +modF = PrimModF +clamp = PrimClamp +clampS = PrimClampS +mix = PrimMix +mixS = PrimMixS +mixB = PrimMixB +step = PrimStep +stepS = PrimStepS +smoothstep = PrimSmoothStep +smoothstepS = PrimSmoothStepS +isNan = PrimIsNan +isInf = PrimIsInf + +dFdx = PrimDFdx +dFdy = PrimDFdy +fWidth = PrimFWidth + +noise1 = PrimNoise1 +noise2 = PrimNoise2 +noise3 = PrimNoise3 +noise4 = PrimNoise4 + +-- geometric functions +length = PrimLength +distance = PrimDistance +dot = PrimDot +cross = PrimCross +normalize = PrimNormalize +faceforward = PrimFaceForward +reflect = PrimReflect +refract = PrimRefract + +transpose = PrimTranspose +det = PrimDeterminant +inv = PrimInverse +outer = PrimOuterProduct + +-- operators +infixl 7 *, /, % +infixl 6 +, - +infix 4 /=, <, <=, >=, > + +infixr 3 && +infixr 2 || + +infix 7 `dot` -- dot +infix 7 `cross` -- cross + +infixr 7 *. -- mulmv +infixl 7 .* -- mulvm +infixl 7 .*. -- mulmm + +-- arithemtic +a + b = PrimAdd a b +a - b = PrimSub a b +a * b = PrimMul a b +a / b = PrimDiv a b +a % b = PrimMod a b + +neg a = PrimNeg a + +-- comparison +--a == b = PrimEqual a b +a /= b = PrimNotEqual a b +a < b = PrimLessThan a b +a <= b = PrimLessThanEqual a b +a >= b = PrimGreaterThanEqual a b +a > b = PrimGreaterThan a b + +-- logical +a && b = PrimAnd a b +a || b = PrimOr a b +xor = PrimXor +not a = PrimNot a +any a = PrimAny a +all a = PrimAll a + +-- matrix functions +a .*. b = PrimMulMatMat a b +a *. b = PrimMulMatVec a b +a .* b = PrimMulVecMat a b + +-- temp hack for vector <---> scalar operators +infixl 7 *!, /!, %! +infixl 6 +!, -! + +-- arithemtic +a +! b = PrimAddS a b +a -! b = PrimSubS a b +a *! b = PrimMulS a b +a /! b = PrimDivS a b +a %! b = PrimModS a b + +------------------ +-- common matrices +------------------ +{- +-- | Perspective transformation matrix in row major order. +perspective :: Float -- ^ Near plane clipping distance (always positive). + -> Float -- ^ Far plane clipping distance (always positive). + -> Float -- ^ Field of view of the y axis, in radians. + -> Float -- ^ Aspect ratio, i.e. screen's width\/height. + -> Mat 4 4 Float +perspective n f fovy aspect = --transpose $ + M44F (V4F (2*n/(r-l)) 0 (-(r+l)/(r-l)) 0) + (V4F 0 (2*n/(t-b)) ((t+b)/(t-b)) 0) + (V4F 0 0 (-(f+n)/(f-n)) (-2*f*n/(f-n))) + (V4F 0 0 (-1) 0) + where + t = n*tan(fovy/2) + b = -t + r = aspect*t + l = -r +-} +rotMatrixZ a = M44F (V4 c s 0 0) (V4 (-s) c 0 0) (V4 0 0 1 0) (V4 0 0 0 1) + where + c = cos a + s = sin a + +rotMatrixY a = M44F (V4 c 0 (-s) 0) (V4 0 1 0 0) (V4 s 0 c 0) (V4 0 0 0 1) + where + c = cos a + s = sin a + +rotMatrixX a = M44F (V4 1 0 0 0) (V4 0 c s 0) (V4 0 (-s) c 0) (V4 0 0 0 1) + where + c = cos a + s = sin a + +rotationEuler a b c = rotMatrixY a .*. rotMatrixX b .*. rotMatrixZ c + +{- +-- | Camera transformation matrix. +lookat :: Vec 3 Float -- ^ Camera position. + -> Vec 3 Float -- ^ Target position. + -> Vec 3 Float -- ^ Upward direction. + -> M44F +lookat pos target up = translateBefore4 (neg pos) (orthogonal $ toOrthoUnsafe r) + where + w = normalize $ pos - target + u = normalize $ up `cross` w + v = w `cross` u + r = transpose $ Mat3 u v w +-} + +scale t v = v * V4 t t t 1.0 + +fromTo :: Float -> Float -> [Float] +fromTo a b = if a > b then [] else a: fromTo (a +! 1.0) b + +(!!) :: [a] -> Int -> a +(x : _) !! 0 = x +(_ : xs) !! n = xs !! (n-1) + + diff --git a/src/LambdaCube/Compiler.hs b/src/LambdaCube/Compiler.hs new file mode 100644 --- /dev/null +++ b/src/LambdaCube/Compiler.hs @@ -0,0 +1,209 @@ +{-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE PatternSynonyms #-} +{-# LANGUAGE ViewPatterns #-} +{-# LANGUAGE LambdaCase #-} +{-# LANGUAGE GeneralizedNewtypeDeriving #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# OPTIONS_GHC -fno-warn-orphans #-} -- instance MonadMask m => MonadMask (ExceptT e m) +module LambdaCube.Compiler + ( Backend(..) + , Pipeline + , Infos, listInfos, Range(..) + , ErrorMsg(..) + , Exp, outputType, boolType, trueExp + + , MMT, runMMT, mapMMT + , MM, runMM + , Err + , catchMM, catchErr + , ioFetch + , getDef, compileMain, preCompile + , removeFromCache + + , compilePipeline + , ppShow + ) where + +import Data.Char +import Data.List +import Data.Map (Map) +import qualified Data.Map as Map +import Control.Monad.State +import Control.Monad.Reader +import Control.Monad.Writer +import Control.Monad.Except +import Control.Monad.Identity +import Control.DeepSeq +import Control.Monad.Catch +import Control.Exception hiding (catch, bracket, finally, mask) +import Control.Arrow hiding ((<+>)) +import System.Directory +import System.FilePath +--import Debug.Trace +import qualified Data.Text as T +import qualified Data.Text.IO as TIO + +import LambdaCube.IR as IR +import LambdaCube.Compiler.Pretty hiding (()) +import LambdaCube.Compiler.Infer (Infos, listInfos, ErrorMsg(..), PolyEnv(..), Export(..), Module(..), ErrorT, throwErrorTCM, parseLC, joinPolyEnvs, filterPolyEnv, inference_, ImportItems (..), Range(..), Exp, outputType, boolType, trueExp) +import LambdaCube.Compiler.CoreToIR + +-- inlcude path for: Builtins, Internals and Prelude +import Paths_lambdacube_compiler (getDataDir) + +type EName = String +type MName = String + +type Modules = Map FilePath (Either Doc PolyEnv) +type ModuleFetcher m = Maybe FilePath -> MName -> m (FilePath, String) + +newtype MMT m a = MMT { runMMT :: ReaderT (ModuleFetcher (MMT m)) (ErrorT (StateT Modules (WriterT Infos m))) a } + deriving (Functor, Applicative, Monad, MonadReader (ModuleFetcher (MMT m)), MonadState Modules, MonadError ErrorMsg, MonadIO, MonadThrow, MonadCatch, MonadMask) +type MM = MMT IO + +instance MonadMask m => MonadMask (ExceptT e m) where + mask f = ExceptT $ mask $ \u -> runExceptT $ f (mapExceptT u) + uninterruptibleMask = error "not implemented: uninterruptibleMask for ExcpetT" + +mapMMT f (MMT m) = MMT $ f m + +type Err a = (Either ErrorMsg a, Infos) + +runMM :: Monad m => ModuleFetcher (MMT m) -> MMT m a -> m (Err a) +runMM fetcher + = runWriterT + . flip evalStateT mempty + . runExceptT + . flip runReaderT fetcher + . runMMT + +catchErr :: (MonadCatch m, NFData a, MonadIO m) => (String -> m a) -> m a -> m a +catchErr er m = (force <$> m >>= liftIO . evaluate) `catch` getErr `catch` getPMatchFail + where + getErr (e :: ErrorCall) = catchErr er $ er $ show e + getPMatchFail (e :: PatternMatchFail) = catchErr er $ er $ show e + +catchMM :: Monad m => MMT m a -> (ErrorMsg -> MMT m a) -> MMT m a +catchMM m e = mapMMT (mapReaderT $ lift . runExceptT) m >>= either e return + +-- TODO: remove dependent modules from cache too +removeFromCache :: Monad m => FilePath -> MMT m () +removeFromCache f = modify $ Map.delete f + +readFileStrict :: FilePath -> IO String +readFileStrict = fmap T.unpack . TIO.readFile + +readFile' :: FilePath -> IO (Maybe String) +readFile' fname = do + b <- doesFileExist fname + if b then Just <$> readFileStrict fname else return Nothing + +ioFetch :: MonadIO m => [FilePath] -> ModuleFetcher (MMT m) +ioFetch paths imp n = do + preludePath <- ( "lc") <$> liftIO getDataDir + let + f [] = throwErrorTCM $ "can't find module" <+> hsep (map text fnames) + f (x:xs) = liftIO (readFile' x) >>= \case + Nothing -> f xs + Just src -> do + --liftIO $ putStrLn $ "loading " ++ x + return (x, src) + fnames = map normalise . concatMap lcModuleFile $ nub $ preludePath : paths + lcModuleFile path = (++ ".lc") <$> g imp + where + g Nothing = [path n] + g (Just fn) = [path hn, fst (splitMPath fn) hn] + + hn = h [] n + h acc [] = reverse acc + h acc ('.':cs) = reverse acc h [] cs + h acc (c: cs) = h (c: acc) cs + f fnames + +splitMPath fn = (joinPath as, intercalate "." $ bs ++ [y]) + where + (as, bs) = span (\x -> null x || x == "." || x == "/" || isLower (head x)) xs + (xs, y) = map takeDirectory . splitPath *** id $ splitFileName $ dropExtension fn + + +loadModule :: MonadMask m => Maybe FilePath -> MName -> MMT m (FilePath, PolyEnv) +loadModule imp mname = do + fetch <- ask + (fname, src) <- fetch imp mname + c <- gets $ Map.lookup fname + case c of + Just (Right m) -> return (fname, m) + Just (Left e) -> throwErrorTCM $ "cycles in module imports:" <+> pShow mname <+> e + _ -> do + e <- MMT $ lift $ mapExceptT (lift . lift) $ parseLC fname src + modify $ Map.insert fname $ Left $ pShow $ map fst $ moduleImports e + let + loadModuleImports (m, is) = do + filterPolyEnv (filterImports is) . snd <$> loadModule (Just fname) m + do + ms <- mapM loadModuleImports $ moduleImports e + x' <- {-trace ("loading " ++ fname) $-} do + env <- joinPolyEnvs False ms + x <- MMT $ lift $ mapExceptT (lift . mapWriterT (return . runIdentity)) $ inference_ env e + case moduleExports e of + Nothing -> return x + Just es -> joinPolyEnvs False $ flip map es $ \exp -> case exp of + ExportId d -> case Map.lookup d $ getPolyEnv x of + Just def -> PolyEnv (Map.singleton d def) mempty + Nothing -> error $ d ++ " is not defined" + ExportModule m | m == snd (splitMPath mname) -> x + ExportModule m -> case [ ms + | ((m', is), ms) <- zip (moduleImports e) ms, m' == m] of + [PolyEnv x infos] -> PolyEnv x mempty -- TODO + [] -> error "empty export list" + _ -> error "export list: internal error" + modify $ Map.insert fname $ Right x' + return (fname, x') +-- `finally` modify (Map.delete fname) + `catchMM` (\e -> modify (Map.delete fname) >> throwError e) + +filterImports (ImportAllBut ns) = not . (`elem` ns) +filterImports (ImportJust ns) = (`elem` ns) + +-- used in runTests +getDef :: MonadMask m => MName -> EName -> Maybe Exp -> MMT m (FilePath, Either String (Exp, Exp), Infos) +getDef m d ty = do + (fname, pe) <- loadModule Nothing m + return + ( fname + , case Map.lookup d $ getPolyEnv pe of + Just (e, thy, si) + | Just False <- (== thy) <$> ty -> Left $ "type of " ++ d ++ " should be " ++ show ty ++ " instead of " ++ ppShow thy -- TODO: better type comparison + | otherwise -> Right (e, thy) + Nothing -> Left $ d ++ " is not found" + , infos pe + ) + +parseAndToCoreMain m = either (throwErrorTCM . text) return . (\(_, e, i) -> flip (,) i <$> e) =<< getDef m "main" (Just outputType) + +-- | most commonly used interface for end users +compileMain :: [FilePath] -> IR.Backend -> MName -> IO (Either String IR.Pipeline) +compileMain path backend fname + = fmap ((show +++ fst) . fst) $ runMM (ioFetch path) $ first (compilePipeline backend) <$> parseAndToCoreMain fname + +-- | Removes the escaping characters from the error message +removeEscapes = first ((\(ErrorMsg e) -> ErrorMsg (removeEscs e)) +++ id) + +-- used by the compiler-service of the online editor +preCompile :: (MonadMask m, MonadIO m) => [FilePath] -> [FilePath] -> Backend -> String -> IO (String -> m (Err (IR.Pipeline, Infos))) +preCompile paths paths' backend mod = do + res <- runMM (ioFetch paths) $ loadModule Nothing mod + case res of + (Left err, i) -> error $ "Prelude could not compiled: " ++ show err + (Right (_, prelude), _) -> return compile + where + compile src = fmap removeEscapes . runMM fetch $ do + modify $ Map.insert ("." "Prelude.lc") $ Right prelude + first (compilePipeline backend) <$> parseAndToCoreMain "Main" + where + fetch imp = \case + "Prelude" -> return ("./Prelude.lc", undefined) + "Main" -> return ("./Main.lc", src) + n -> ioFetch paths' imp n + diff --git a/src/LambdaCube/Compiler/CoreToIR.hs b/src/LambdaCube/Compiler/CoreToIR.hs new file mode 100644 --- /dev/null +++ b/src/LambdaCube/Compiler/CoreToIR.hs @@ -0,0 +1,1116 @@ +{-# LANGUAGE PatternSynonyms #-} +{-# LANGUAGE ViewPatterns #-} +{-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE LambdaCase #-} +{-# LANGUAGE PackageImports #-} +{-# LANGUAGE DeriveFunctor #-} +{-# LANGUAGE DeriveFoldable #-} +{-# LANGUAGE DeriveTraversable #-} +{-# OPTIONS_GHC -fno-warn-unused-binds #-} -- TODO: remove +module LambdaCube.Compiler.CoreToIR + ( compilePipeline + ) where + +import Data.Char +import Data.List +import Data.Maybe +import Data.Monoid +import Data.Set (Set) +import qualified Data.Set as Set +import Data.Map (Map) +import qualified Data.Map as Map +import Data.Vector ((!)) +import qualified Data.Vector as Vector +--import Control.Applicative +import Control.Arrow hiding ((<+>)) +import Control.Monad.Writer +import Control.Monad.State +import Control.Monad.Reader +--import Control.Monad.Except +--import Control.Monad.Identity +--import Text.Parsec.Pos +--import Debug.Trace + +import LambdaCube.IR(Backend(..)) +import qualified LambdaCube.IR as IR +import qualified LambdaCube.Linear as IR + +import LambdaCube.Compiler.Pretty hiding (parens) +import qualified LambdaCube.Compiler.Infer as I +import LambdaCube.Compiler.Infer (SName, Lit(..), Visibility(..)) + +-------------------------------------------------------------------------- + +type CG = State IR.Pipeline + +pattern TFrameBuffer a b <- A2 "FrameBuffer" a b + +emptyPipeline b = IR.Pipeline b mempty mempty mempty mempty mempty mempty mempty +update i x xs = xs Vector.// [(i,x)] + +newTexture :: Int -> Int -> IR.ImageSemantic -> CG IR.TextureName +newTexture width height semantic = do + let sampleDescriptor = IR.SamplerDescriptor + { IR.samplerWrapS = IR.Repeat + , IR.samplerWrapT = Nothing + , IR.samplerWrapR = Nothing + , IR.samplerMinFilter = IR.Linear + , IR.samplerMagFilter = IR.Linear + , IR.samplerBorderColor = IR.VV4F (IR.V4 0 0 0 1) + , IR.samplerMinLod = Nothing + , IR.samplerMaxLod = Nothing + , IR.samplerLodBias = 0 + , IR.samplerCompareFunc = Nothing + } + + textureDescriptor = IR.TextureDescriptor + { IR.textureType = IR.Texture2D (if semantic == IR.Color then IR.FloatT IR.RGBA else IR.FloatT IR.Red) 1 + , IR.textureSize = IR.VV2U $ IR.V2 (fromIntegral width) (fromIntegral height) + , IR.textureSemantic = semantic + , IR.textureSampler = sampleDescriptor + , IR.textureBaseLevel = 0 + , IR.textureMaxLevel = 0 + } + tv <- gets IR.textures + modify (\s -> s {IR.textures = tv <> pure textureDescriptor}) + return $ length tv + +newFrameBufferTarget :: Ty -> CG IR.RenderTargetName +newFrameBufferTarget (TFrameBuffer _ a) = do + let t = IR.RenderTarget $ Vector.fromList [IR.TargetItem s (Just (IR.Framebuffer s)) | s <- compSemantic a] + tv <- gets IR.targets + modify (\s -> s {IR.targets = tv <> pure t}) + return $ length tv +newFrameBufferTarget x = error $ "newFrameBufferTarget illegal target type: " ++ ppShow x + +newTextureTarget :: Int -> Int -> Ty -> CG IR.RenderTargetName +newTextureTarget w h (TFrameBuffer _ a) = do + tl <- forM (compSemantic a) $ \s -> do + texture <- newTexture w h s + return $ IR.TargetItem s (Just (IR.TextureImage texture 0 Nothing)) + tv <- gets IR.targets + modify (\s -> s {IR.targets = tv <> pure (IR.RenderTarget $ Vector.fromList tl)}) + return $ Vector.length tv +newTextureTarget _ _ x = error $ "newTextureTarget illegal target type: " ++ ppShow x + +compilePipeline :: IR.Backend -> I.ExpType -> IR.Pipeline +compilePipeline b e = flip execState (emptyPipeline b) $ do + (subCmds,cmds) <- getCommands $ toExp e + modify (\s -> s {IR.commands = Vector.fromList subCmds <> Vector.fromList cmds}) + +mergeSlot a b = a + { IR.slotUniforms = IR.slotUniforms a <> IR.slotUniforms b + , IR.slotStreams = IR.slotStreams a <> IR.slotStreams b + , IR.slotPrograms = IR.slotPrograms a <> IR.slotPrograms b + } + +getSlot :: Exp -> CG (IR.Command,[(String,IR.InputType)]) +getSlot e@(Prim2 "fetch_" (EString slotName) attrs) = do + let input = compAttribute attrs + slot = IR.Slot + { IR.slotName = slotName + , IR.slotUniforms = mempty + , IR.slotStreams = Map.fromList input + , IR.slotPrimitive = compFetchPrimitive $ getPrim $ tyOf e + , IR.slotPrograms = mempty + } + sv <- gets IR.slots + case Vector.findIndex ((slotName ==) . IR.slotName) sv of + Nothing -> do + modify (\s -> s {IR.slots = sv <> pure slot}) + return (IR.RenderSlot $ length sv,input) + Just i -> do + modify (\s -> s {IR.slots = update i (mergeSlot (sv ! i) slot) sv}) + return (IR.RenderSlot i,input) +getSlot e@(Prim1 "fetchArrays_" attrs) = do + let (input,values) = unzip [((name,ty),(name,value)) | (i,(ty,value)) <- zip [0..] (compAttributeValue attrs), let name = "attribute_" ++ show i] + stream = IR.StreamData + { IR.streamData = Map.fromList values + , IR.streamType = Map.fromList input + , IR.streamPrimitive = compFetchPrimitive $ getPrim $ tyOf e + , IR.streamPrograms = mempty + } + sv <- gets IR.streams + modify (\s -> s {IR.streams = sv <> pure stream}) + return (IR.RenderStream $ length sv,input) +getSlot x = error $ "getSlot: " ++ ppShow x + +getPrim (A1 "List" (A2 "Primitive" _ p)) = p +getPrim' (A1 "List" (A2 "Primitive" a _)) = a +getPrim'' (A1 "List" (A2 "Vector" _ (A1 "Maybe" (A1 "SimpleFragment" a)))) = a +getPrim'' x = error $ "getPrim'':" ++ ppShow x + +addProgramToSlot :: IR.ProgramName -> IR.Command -> CG () +addProgramToSlot prgName (IR.RenderSlot slotName) = do + sv <- gets IR.slots + pv <- gets IR.programs + let slot = sv ! slotName + prg = pv ! prgName + slot' = slot + { IR.slotUniforms = IR.slotUniforms slot <> IR.programUniforms prg + , IR.slotPrograms = IR.slotPrograms slot <> pure prgName + } + modify (\s -> s {IR.slots = update slotName slot' sv}) +addProgramToSlot prgName (IR.RenderStream streamName) = do + sv <- gets IR.streams + pv <- gets IR.programs + let stream = sv ! streamName + prg = pv ! prgName + stream' = stream + { IR.streamPrograms = IR.streamPrograms stream <> pure prgName + } + modify (\s -> s {IR.streams = update streamName stream' sv}) + +getProgram :: [(String,IR.InputType)] -> IR.Command -> Exp -> Exp -> Exp -> Exp -> Maybe Exp -> CG IR.ProgramName +getProgram input slot rp is vert frag ffilter = do + backend <- gets IR.backend + let ((vertexInput,vertOut),vertSrc) = genVertexGLSL backend rp is vert + fragSrc = genFragmentGLSL backend pUniforms vertOut frag ffilter + pUniforms = Map.fromList $ Set.toList $ getUniforms vert <> getUniforms rp <> getUniforms frag <> maybe mempty getUniforms ffilter + prg = IR.Program + { IR.programUniforms = pUniforms + , IR.programStreams = Map.fromList $ zip vertexInput $ map (uncurry IR.Parameter) input + , IR.programInTextures = Map.fromList $ Set.toList $ getSamplerUniforms vert <> getSamplerUniforms rp <> getSamplerUniforms frag <> maybe mempty getSamplerUniforms ffilter + , IR.programOutput = pure $ IR.Parameter "f0" IR.V4F -- TODO + , IR.vertexShader = vertSrc + , IR.geometryShader = mempty -- TODO + , IR.fragmentShader = fragSrc + } + pv <- gets IR.programs + modify (\s -> s {IR.programs = pv <> pure prg}) + let prgName = length pv + addProgramToSlot prgName slot + return prgName + +getRenderTextures :: Exp -> [Exp] +getRenderTextures e = case e of + ELet (PVar (A0 "Sampler") _) (A3 "Sampler" _ _ (A2 "Texture2D" _ _)) _ -> [e] + Exp e -> foldMap getRenderTextures e + +type SamplerBinding = (IR.UniformName,IR.ImageRef) + +getRenderTextureCommands :: Exp -> CG ([SamplerBinding],[IR.Command]) +getRenderTextureCommands e = foldM (\(a,b) x -> f x >>= (\(c,d) -> return (c:a,d ++ b))) mempty (getRenderTextures e) + where + f = \case + ELet (PVar t n) (A3 "Sampler" _ _ (A2 "Texture2D" (A2 "V2" (EInt w) (EInt h)) (Prim1 "PrjImageColor" a))) _ -> do + rt <- newTextureTarget (fromIntegral w) (fromIntegral h) (tyOf a) + tv <- gets IR.targets + let IR.RenderTarget (Vector.toList -> [_,IR.TargetItem IR.Color (Just (IR.TextureImage texture _ _))]) = tv ! rt + (subCmds,cmds) <- getCommands a + return ((n,IR.TextureImage texture 0 Nothing), subCmds <> (IR.SetRenderTarget rt:cmds)) + ELet (PVar t n) (A3 "Sampler" _ _ (A2 "Texture2D" (A2 "V2" (EInt w) (EInt h)) (Prim1 "PrjImage" a))) _ -> do + rt <- newTextureTarget (fromIntegral w) (fromIntegral h) (tyOf a) + tv <- gets IR.targets + let IR.RenderTarget (Vector.toList -> [IR.TargetItem IR.Color (Just (IR.TextureImage texture _ _))]) = tv ! rt + (subCmds,cmds) <- getCommands a + return ((n,IR.TextureImage texture 0 Nothing), subCmds <> (IR.SetRenderTarget rt:cmds)) + x -> error $ "getRenderTextureCommands: not supported render texture exp: " ++ ppShow x + +getFragFilter (Prim2 "map" (EtaPrim2 "filterFragment" p) x) = (Just p, x) +getFragFilter x = (Nothing, x) + +getVertexShader (Prim2 "map" (EtaPrim2 "mapPrimitive" f) x) = (f, x) +getVertexShader x = (idFun $ getPrim' $ tyOf x, x) + +getFragmentShader (Prim2 "map" (EtaPrim2 "mapFragment" f) x) = (f, x) +getFragmentShader x = (idFun $ getPrim'' $ tyOf x, x) + +removeDepthHandler (Prim2 "map" (EtaPrim1 "noDepth") x) = x +removeDepthHandler x = x + +getCommands :: Exp -> CG ([IR.Command],[IR.Command]) +getCommands e = case e of + A1 "ScreenOut" a -> do + rt <- newFrameBufferTarget (tyOf a) + (subCmds,cmds) <- getCommands a + return (subCmds,IR.SetRenderTarget rt : cmds) + Prim3 "Accumulate" actx (getFragmentShader . removeDepthHandler -> (frag, getFragFilter -> (ffilter, Prim3 "foldr" (EtaPrim2_2 "++") (A0 "Nil") (Prim2 "map" (EtaPrim3 "rasterizePrimitive" is rctx) (getVertexShader -> (vert, input)))))) fbuf -> do + let rp = compRC' rctx + (smpBindingsV,vertCmds) <- getRenderTextureCommands vert + (smpBindingsR,rastCmds) <- maybe (return mempty) getRenderTextureCommands ffilter + (smpBindingsP,raspCmds) <- getRenderTextureCommands rp + (smpBindingsF,fragCmds) <- getRenderTextureCommands frag + (renderCommand,input) <- getSlot input + prog <- getProgram input renderCommand rp is vert frag ffilter + (subFbufCmds, fbufCommands) <- getCommands fbuf + programs <- gets IR.programs + let textureUniforms = [IR.SetSamplerUniform n textureUnit | ((n,IR.FTexture2D),textureUnit) <- zip (Map.toList $ IR.programUniforms $ programs ! prog) [0..]] + cmds = + [ IR.SetProgram prog ] <> + textureUniforms <> + concat -- TODO: generate IR.SetSamplerUniform commands for texture slots + [ [ IR.SetTexture textureUnit texture + , IR.SetSamplerUniform name textureUnit + ] | (textureUnit,(name,IR.TextureImage texture _ _)) <- zip [length textureUniforms..] (smpBindingsV <> smpBindingsP <> smpBindingsR <> smpBindingsF) + ] <> + [ IR.SetRasterContext (compRC rctx) + , IR.SetAccumulationContext (compAC actx) + , renderCommand + ] + return (subFbufCmds <> vertCmds <> raspCmds <> rastCmds <> fragCmds, fbufCommands <> cmds) + Prim1 "FrameBuffer" a -> return ([],[IR.ClearRenderTarget (Vector.fromList $ map (uncurry IR.ClearImage) $ compFrameBuffer a)]) + x -> error $ "getCommands " ++ ppShow x + +getSamplerUniforms :: Exp -> Set (String,IR.InputType) +getSamplerUniforms e = case e of + ELet (PVar _ _) (A3 "Sampler" _ _ (A1 "Texture2DSlot" (EString s))) _ -> Set.singleton (s, IR.FTexture2D{-compInputType $ tyOf e-}) -- TODO + ELet (PVar _ n) (A3 "Sampler" _ _ (A2 "Texture2D" _ _)) _ -> Set.singleton (n, IR.FTexture2D) + Exp e -> foldMap getSamplerUniforms e + +getUniforms :: Exp -> Set (String,IR.InputType) +getUniforms e = case e of + Uniform s -> Set.singleton (s, compInputType $ tyOf e) + ELet (PVar _ _) (A3 "Sampler" _ _ (A1 "Texture2DSlot" (EString s))) _ -> Set.singleton (s, IR.FTexture2D{-compInputType $ tyOf e-}) -- TODO + ELet (PVar _ _) (A3 "Sampler" _ _ (A2 "Texture2D" _ _)) _ -> mempty + Exp e -> foldMap getUniforms e + +compFrameBuffer x = case x of + ETuple a -> concatMap compFrameBuffer a + Prim1 "DepthImage" a -> [(IR.Depth, compValue a)] + Prim1 "ColorImage" a -> [(IR.Color, compValue a)] + x -> error $ "compFrameBuffer " ++ ppShow x + +compSemantic x = case x of + TTuple t -> concatMap compSemantic t + A1 "Depth" _ -> return IR.Depth + A1 "Stencil" _ -> return IR.Stencil + A1 "Color" _ -> return IR.Color + x -> error $ "compSemantic " ++ ppShow x + +compAC x = IR.AccumulationContext Nothing $ map compFrag $ case x of + ETuple a -> a + a -> [a] + +compBlending x = case x of + A0 "NoBlending" -> IR.NoBlending + A1 "BlendLogicOp" a -> IR.BlendLogicOp (compLO a) + A3 "Blend" (ETuple [a,b]) (ETuple [ETuple [c,d],ETuple [e,f]]) (compValue -> IR.VV4F g) -> IR.Blend (compBE a) (compBE b) (compBF c) (compBF d) (compBF e) (compBF f) g + x -> error $ "compBlending " ++ ppShow x + +compBF x = case x of + A0 "Zero'" -> IR.Zero + A0 "One" -> IR.One + A0 "SrcColor" -> IR.SrcColor + A0 "OneMinusSrcColor" -> IR.OneMinusSrcColor + A0 "DstColor" -> IR.DstColor + A0 "OneMinusDstColor" -> IR.OneMinusDstColor + A0 "SrcAlpha" -> IR.SrcAlpha + A0 "OneMinusSrcAlpha" -> IR.OneMinusSrcAlpha + A0 "DstAlpha" -> IR.DstAlpha + A0 "OneMinusDstAlpha" -> IR.OneMinusDstAlpha + A0 "ConstantColor" -> IR.ConstantColor + A0 "OneMinusConstantColor" -> IR.OneMinusConstantColor + A0 "ConstantAlpha" -> IR.ConstantAlpha + A0 "OneMinusConstantAlpha" -> IR.OneMinusConstantAlpha + A0 "SrcAlphaSaturate" -> IR.SrcAlphaSaturate + x -> error $ "compBF " ++ ppShow x + +compBE x = case x of + A0 "FuncAdd" -> IR.FuncAdd + A0 "FuncSubtract" -> IR.FuncSubtract + A0 "FuncReverseSubtract" -> IR.FuncReverseSubtract + A0 "Min" -> IR.Min + A0 "Max" -> IR.Max + x -> error $ "compBE " ++ ppShow x + +compLO x = case x of + A0 "Clear" -> IR.Clear + A0 "And" -> IR.And + A0 "AndReverse" -> IR.AndReverse + A0 "Copy" -> IR.Copy + A0 "AndInverted" -> IR.AndInverted + A0 "Noop" -> IR.Noop + A0 "Xor" -> IR.Xor + A0 "Or" -> IR.Or + A0 "Nor" -> IR.Nor + A0 "Equiv" -> IR.Equiv + A0 "Invert" -> IR.Invert + A0 "OrReverse" -> IR.OrReverse + A0 "CopyInverted" -> IR.CopyInverted + A0 "OrInverted" -> IR.OrInverted + A0 "Nand" -> IR.Nand + A0 "Set" -> IR.Set + x -> error $ "compLO " ++ ppShow x + +compComparisonFunction x = case x of + A0 "Never" -> IR.Never + A0 "Less" -> IR.Less + A0 "Equal" -> IR.Equal + A0 "Lequal" -> IR.Lequal + A0 "Greater" -> IR.Greater + A0 "Notequal" -> IR.Notequal + A0 "Gequal" -> IR.Gequal + A0 "Always" -> IR.Always + x -> error $ "compComparisonFunction " ++ ppShow x + +pattern EBool a <- (compBool -> Just a) + +compBool x = case x of + A0 "True" -> Just True + A0 "False" -> Just False + x -> Nothing + +compFrag x = case x of + A2 "DepthOp" (compComparisonFunction -> a) (EBool b) -> IR.DepthOp a b + A2 "ColorOp" (compBlending -> b) (compValue -> v) -> IR.ColorOp b v + x -> error $ "compFrag " ++ ppShow x + +compInputType x = case x of + TFloat -> IR.Float + TVec 2 TFloat -> IR.V2F + TVec 3 TFloat -> IR.V3F + TVec 4 TFloat -> IR.V4F + TBool -> IR.Bool + TVec 2 TBool -> IR.V2B + TVec 3 TBool -> IR.V3B + TVec 4 TBool -> IR.V4B + TInt -> IR.Int + TVec 2 TInt -> IR.V2I + TVec 3 TInt -> IR.V3I + TVec 4 TInt -> IR.V4I + TWord -> IR.Word + TVec 2 TWord -> IR.V2U + TVec 3 TWord -> IR.V3U + TVec 4 TWord -> IR.V4U + TMat 2 2 TFloat -> IR.M22F + TMat 2 3 TFloat -> IR.M23F + TMat 2 4 TFloat -> IR.M24F + TMat 3 2 TFloat -> IR.M32F + TMat 3 3 TFloat -> IR.M33F + TMat 3 4 TFloat -> IR.M34F + TMat 4 2 TFloat -> IR.M42F + TMat 4 3 TFloat -> IR.M43F + TMat 4 4 TFloat -> IR.M44F + x -> error $ "compInputType " ++ ppShow x + +compAttribute x = case x of + ETuple a -> concatMap compAttribute a + Prim1 "Attribute" (EString s) -> [(s, compInputType $ tyOf x)] + x -> error $ "compAttribute " ++ ppShow x + +compAttributeValue :: Exp -> [(IR.InputType,IR.ArrayValue)] +compAttributeValue x = let + compList (A2 "Cons" a x) = compValue a : compList x + compList (A0 "Nil") = [] + compList x = error $ "compList: " ++ ppShow x + emptyArray t | t `elem` [IR.Float,IR.V2F,IR.V3F,IR.V4F,IR.M22F,IR.M23F,IR.M24F,IR.M32F,IR.M33F,IR.M34F,IR.M42F,IR.M43F,IR.M44F] = IR.VFloatArray mempty + emptyArray t | t `elem` [IR.Int,IR.V2I,IR.V3I,IR.V4I] = IR.VIntArray mempty + emptyArray t | t `elem` [IR.Word,IR.V2U,IR.V3U,IR.V4U] = IR.VWordArray mempty + emptyArray t | t `elem` [IR.Bool,IR.V2B,IR.V3B,IR.V4B] = IR.VBoolArray mempty + emptyArray _ = error "compAttributeValue - emptyArray" + flatten IR.Float (IR.VFloat x) (IR.VFloatArray l) = IR.VFloatArray $ pure x <> l + flatten IR.V2F (IR.VV2F (IR.V2 x y)) (IR.VFloatArray l) = IR.VFloatArray $ pure x <> pure y <> l + flatten IR.V3F (IR.VV3F (IR.V3 x y z)) (IR.VFloatArray l) = IR.VFloatArray $ pure x <> pure y <> pure z <> l + flatten IR.V4F (IR.VV4F (IR.V4 x y z w)) (IR.VFloatArray l) = IR.VFloatArray $ pure x <> pure y <> pure z <> pure w <> l + flatten _ _ _ = error "compAttributeValue" + checkLength l@((a,_):_) = case all (\(i,_) -> i == a) l of + True -> snd $ unzip l + False -> error "FetchArrays array length mismatch!" + go = \case + ETuple a -> concatMap go a + a -> let A1 "List" (compInputType -> t) = tyOf a + values = compList a + in + [(length values,(t,foldr (flatten t) (emptyArray t) values))] + in checkLength $ go x + +compFetchPrimitive x = case x of + A0 "Point" -> IR.Points + A0 "Line" -> IR.Lines + A0 "Triangle" -> IR.Triangles + A0 "LineAdjacency" -> IR.LinesAdjacency + A0 "TriangleAdjacency" -> IR.TrianglesAdjacency + x -> error $ "compFetchPrimitive " ++ ppShow x + +compValue x = case x of + EFloat a -> IR.VFloat $ realToFrac a + EInt a -> IR.VInt $ fromIntegral a + A2 "V2" (EFloat a) (EFloat b) -> IR.VV2F $ IR.V2 (realToFrac a) (realToFrac b) + A3 "V3" (EFloat a) (EFloat b) (EFloat c) -> IR.VV3F $ IR.V3 (realToFrac a) (realToFrac b) (realToFrac c) + A4 "V4" (EFloat a) (EFloat b) (EFloat c) (EFloat d) -> IR.VV4F $ IR.V4 (realToFrac a) (realToFrac b) (realToFrac c) (realToFrac d) + A2 "V2" (EBool a) (EBool b) -> IR.VV2B $ IR.V2 a b + A3 "V3" (EBool a) (EBool b) (EBool c) -> IR.VV3B $ IR.V3 a b c + A4 "V4" (EBool a) (EBool b) (EBool c) (EBool d) -> IR.VV4B $ IR.V4 a b c d + x -> error $ "compValue " ++ ppShow x + +compRC x = case x of + A3 "PointCtx" a (EFloat b) c -> IR.PointCtx (compPS a) (realToFrac b) (compPSCO c) + A2 "LineCtx" (EFloat a) b -> IR.LineCtx (realToFrac a) (compPV b) + A4 "TriangleCtx" a b c d -> IR.TriangleCtx (compCM a) (compPM b) (compPO c) (compPV d) + x -> error $ "compRC " ++ ppShow x + +compRC' x = case x of + A3 "PointCtx" a _ _ -> compPS' a + A4 "TriangleCtx" _ b _ _ -> compPM' b + x -> defaultPointSizeFun $ case tyOf x of A2 "RasterContext" t _ -> t + +compPSCO x = case x of + A0 "LowerLeft" -> IR.LowerLeft + A0 "UpperLeft" -> IR.UpperLeft + x -> error $ "compPSCO " ++ ppShow x + +compCM x = case x of + A0 "CullNone" -> IR.CullNone + A0 "CullFront" -> IR.CullFront IR.CCW + A0 "CullBack" -> IR.CullBack IR.CCW + x -> error $ "compCM " ++ ppShow x + +compPM x = case x of + A0 "PolygonFill" -> IR.PolygonFill + A1 "PolygonLine" (EFloat a) -> IR.PolygonLine $ realToFrac a + A1 "PolygonPoint" a -> IR.PolygonPoint $ compPS a + x -> error $ "compPM " ++ ppShow x + +compPM' x = case x of + A1 "PolygonPoint" a -> compPS' a + x -> defaultPointSizeFun $ case tyOf x of A1 "PolygonMode" t -> t + +compPS x = case x of + A1 "PointSize" (EFloat a) -> IR.PointSize $ realToFrac a + A1 "ProgramPointSize" _ -> IR.ProgramPointSize + x -> error $ "compPS " ++ ppShow x + +compPS' x = case x of + A1 "ProgramPointSize" x -> x + x -> defaultPointSizeFun $ case tyOf x of A1 "PointSize" t -> t + +compPO x = case x of + A2 "Offset" (EFloat a) (EFloat b) -> IR.Offset (realToFrac a) (realToFrac b) + A0 "NoOffset" -> IR.NoOffset + x -> error $ "compPO " ++ ppShow x + +compPV x = case x of + A0 "FirstVertex" -> IR.FirstVertex + A0 "LastVertex" -> IR.LastVertex + x -> error $ "compPV " ++ ppShow x + +--------------------------------------------------------------- GLSL generation + +{- +mangleIdent :: String -> String +mangleIdent n = '_': concatMap encodeChar n + where + encodeChar = \case + c | isAlphaNum c -> [c] + '_' -> "__" + '.' -> "_dot" + '$' -> "_dollar" + '~' -> "_tilde" + '=' -> "_eq" + '<' -> "_less" + '>' -> "_greater" + '!' -> "_bang" + '#' -> "_hash" + '%' -> "_percent" + '^' -> "_up" + '&' -> "_amp" + '|' -> "_bar" + '*' -> "_times" + '/' -> "_div" + '+' -> "_plus" + '-' -> "_minus" + ':' -> "_colon" + '\\' -> "_bslash" + '?' -> "_qmark" + '@' -> "_at" + '\'' -> "_prime" + c -> '$' : show (ord c) +-} + +genUniforms :: Exp -> Set [String] +genUniforms e = case e of + Uniform s -> Set.singleton [unwords ["uniform",toGLSLType "1" $ tyOf e,s,";"]] + ELet (PVar _ _) (A3 "Sampler" _ _ (A1 "Texture2DSlot" (EString n))) _ -> Set.singleton [unwords ["uniform","sampler2D",n,";"]] + ELet (PVar _ n) (A3 "Sampler" _ _ (A2 "Texture2D" _ _)) _ -> Set.singleton [unwords ["uniform","sampler2D",n,";"]] + Exp e -> foldMap genUniforms e + +type GLSL = Writer [String] + +genStreamInput :: Backend -> Pat -> GLSL [String] +genStreamInput backend i = fmap concat $ mapM input $ case i of + PTuple l -> l + x -> [x] + where + input (PVar t n) = tell [unwords [inputDef,toGLSLType (n ++ " " ++ "\n") t,n,";"]] >> return [n] + input a = error $ "genStreamInput " ++ ppShow a + inputDef = case backend of + OpenGL33 -> "in" + WebGL1 -> "attribute" + +streamInput :: Pat -> [String] +streamInput i = concatMap input $ case i of + PTuple l -> l + x -> [x] + where + input (PVar t n) = [n] + input a = error $ "streamInput " ++ ppShow a + +genStreamOutput :: Backend -> Exp -> [Exp] -> GLSL [(String, String, String)] +genStreamOutput backend (eTuple -> is) l = fmap concat $ zipWithM go (map (("vv" ++) . show) [0..]) $ zip is l + where + go var (A0 (f -> i), toGLSLType "3" . tyOf -> t) = do + tell $ case backend of + WebGL1 -> [unwords ["varying",t,var,";"]] + OpenGL33 -> [unwords [i,"out",t,var,";"]] + return [(i,t,var)] + f "Smooth" = "smooth" + f "Flat" = "flat" + f "NoPerspective" = "noperspective" + +eTuple (ETuple l) = l +eTuple x = [x] + +genFragmentInput :: Backend -> [(String, String, String)] -> GLSL () +genFragmentInput OpenGL33 s = tell [unwords [i,"in",t,n,";"] | (i,t,n) <- s] +genFragmentInput WebGL1 s = tell [unwords ["varying",t,n,";"] | (i,t,n) <- s] +genFragmentOutput backend (tyOf -> a@(toGLSLType "4" -> t)) = case a of + TUnit -> return False + _ -> case backend of + OpenGL33 -> tell [unwords ["out",t,"f0",";"]] >> return True + WebGL1 -> return True + +shaderHeader = \case + OpenGL33 -> do + tell ["#version 330 core"] + tell ["vec4 texture2D(sampler2D s, vec2 uv){return texture(s,uv);}"] + WebGL1 -> do + tell ["#version 100"] + tell ["precision highp float;"] + tell ["precision highp int;"] + +defaultPointSizeFun t = ELam (PVar t "dps") $ EFloat 1 + +genVertexGLSL :: Backend -> Exp -> Exp -> Exp -> (([String],[(String,String,String)]),String) +genVertexGLSL backend rp@(etaRed -> ELam is s) ints e@(etaRed -> ELam i o) = second unlines $ runWriter $ do + shaderHeader backend + mapM_ tell $ foldMap genUniforms [e, rp] + input <- genStreamInput backend i + out <- genStreamOutput backend ints $ tail $ eTuple o + tell ["void main() {"] + unless (null out) $ sequence_ [tell [var <> " = " <> genGLSL x <> ";"] | ((_,_,var),x) <- zip out $ tail $ eTuple o] + tell ["gl_Position = " <> genGLSL (head $ eTuple o) <> ";"] + tell ["gl_PointSize = " <> show (genGLSLSubst (Map.fromList $ zip (streamInput is) $ map (\(_,_,var) -> var) out) s) <> ";"] + tell ["}"] + return (input,out) +genVertexGLSL _ _ _ e = error $ "genVertexGLSL: " ++ ppShow e + +genGLSL :: Exp -> String +genGLSL e = show $ genGLSLSubst mempty e + +genFragmentGLSL :: Backend -> Map String IR.InputType -> [(String,String,String)] -> Exp -> Maybe Exp -> String +genFragmentGLSL backend unifs s e@(etaRed -> ELam i o) ffilter = unlines $ execWriter $ do + shaderHeader backend + mapM_ tell $ foldMap genUniforms $ maybe [e] ((e:) . (:[])) ffilter -- todo: use unifs? + genFragmentInput backend s + hasOutput <- genFragmentOutput backend o + tell ["void main() {"] + case ffilter of + Nothing -> return () + Just (etaRed -> ELam i o) -> tell ["if (!(" <> show (genGLSLSubst (makeSubst i s) o) <> ")) discard;"] + when hasOutput $ case backend of + OpenGL33 -> tell ["f0 = " <> show (genGLSLSubst (makeSubst i s) o) <> ";"] + WebGL1 -> tell ["gl_FragColor = " <> show (genGLSLSubst (makeSubst i s) o) <> ";"] + tell ["}"] + +genFragmentGLSL _ _ _ e ff = error $ "genFragmentGLSL: " ++ ppShow e ++ ppShow ff + +makeSubst (PVar _ x) [(_,_,n)] = Map.singleton x n +makeSubst (PTuple l) x = Map.fromList $ go l x where + go [] [] = [] + go (PVar _ x: al) ((_,_,n):bl) = (x,n) : go al bl + go i s = error $ "makeSubst illegal input " ++ ppShow i ++ " " ++ show s + +parens a = "(" <+> a <+> ")" + +-- todo: (on hold) name mangling to prevent name collisions +-- todo: reader monad +genGLSLSubst :: Map String String -> Exp -> Doc +genGLSLSubst s e = case e of + ELit a -> text $ show a + EVar a -> text $ Map.findWithDefault a a s + Uniform s -> text s + -- texturing + A3 "Sampler" _ _ _ -> error "sampler GLSL codegen is not supported" + PrimN "texture2D" xs -> functionCall "texture2D" xs + + -- temp builtins FIXME: get rid of these + Prim1 "primIntToWord" a -> error $ "WebGL 1 does not support uint types: " ++ ppShow e + Prim1 "primIntToFloat" a -> gen a -- FIXME: does GLSL support implicit int to float cast??? + Prim2 "primCompareInt" a b -> error $ "GLSL codegen does not support: " ++ ppShow e + Prim2 "primCompareWord" a b -> error $ "GLSL codegen does not support: " ++ ppShow e + Prim2 "primCompareFloat" a b -> error $ "GLSL codegen does not support: " ++ ppShow e + Prim1 "primNegateInt" a -> text "-" <+> parens (gen a) + Prim1 "primNegateWord" a -> error $ "WebGL 1 does not support uint types: " ++ ppShow e + Prim1 "primNegateFloat" a -> text "-" <+> parens (gen a) + + -- vectors + AN n xs | n `elem` ["V2", "V3", "V4"], Just s <- vecConName $ tyOf e -> functionCall s xs + -- bool + A0 "True" -> text "true" + A0 "False" -> text "false" + -- matrices + AN "M22F" xs -> functionCall "mat2" xs + AN "M23F" xs -> error "WebGL 1 does not support matrices with this dimension" + AN "M24F" xs -> error "WebGL 1 does not support matrices with this dimension" + AN "M32F" xs -> error "WebGL 1 does not support matrices with this dimension" + AN "M33F" xs -> functionCall "mat3" xs + AN "M34F" xs -> error "WebGL 1 does not support matrices with this dimension" + AN "M42F" xs -> error "WebGL 1 does not support matrices with this dimension" + AN "M43F" xs -> error "WebGL 1 does not support matrices with this dimension" + AN "M44F" xs -> functionCall "mat4" xs -- where gen = gen + + Prim3 "primIfThenElse" a b c -> gen a <+> "?" <+> gen b <+> ":" <+> gen c + -- TODO: Texture Lookup Functions + SwizzProj a x -> "(" <+> gen a <+> (")." <> text x) + ELam _ _ -> error "GLSL codegen for lambda function is not supported yet" + ELet (PVar _ _) (A3 "Sampler" _ _ (A1 "Texture2DSlot" (EString n))) _ -> text n + ELet (PVar _ n) (A3 "Sampler" _ _ (A2 "Texture2D" _ _)) _ -> text n + ELet{} -> error "GLSL codegen for let is not supported yet" + ETuple _ -> error "GLSL codegen for tuple is not supported yet" + + -- Primitive Functions + PrimN "==" xs -> binOp "==" xs + PrimN ('P':'r':'i':'m':n) xs | n'@(_:_) <- trName (dropS n) -> case n' of + (c:_) | isAlpha c -> functionCall n' xs + [op, '_'] -> prefixOp [op] xs + n' -> binOp n' xs + where + ifType p a b = if all (p . tyOf) xs then a else b + + dropS n + | last n == 'S' && init n `elem` ["Add", "Sub", "Div", "Mod", "BAnd", "BOr", "BXor", "BShiftL", "BShiftR", "Min", "Max", "Clamp", "Mix", "Step", "SmoothStep"] = init n + | otherwise = n + + trName = \case + + -- Arithmetic Functions + "Add" -> "+" + "Sub" -> "-" + "Neg" -> "-_" + "Mul" -> ifType isMatrix "matrixCompMult" "*" + "MulS" -> "*" + "Div" -> "/" + "Mod" -> ifType isIntegral "%" "mod" + + -- Bit-wise Functions + "BAnd" -> "&" + "BOr" -> "|" + "BXor" -> "^" + "BNot" -> "~_" + "BShiftL" -> "<<" + "BShiftR" -> ">>" + + -- Logic Functions + "And" -> "&&" + "Or" -> "||" + "Xor" -> "^" + "Not" -> ifType isScalar "!_" "not" + + -- Integer/Float Conversion Functions + "FloatBitsToInt" -> "floatBitsToInt" + "FloatBitsToUInt" -> "floatBitsToUint" + "IntBitsToFloat" -> "intBitsToFloat" + "UIntBitsToFloat" -> "uintBitsToFloat" + + -- Matrix Functions + "OuterProduct" -> "outerProduct" + "MulMatVec" -> "*" + "MulVecMat" -> "*" + "MulMatMat" -> "*" + + -- Fragment Processing Functions + "DFdx" -> "dFdx" + "DFdy" -> "dFdy" + + -- Vector and Scalar Relational Functions + "LessThan" -> ifType isScalarNum "<" "lessThan" + "LessThanEqual" -> ifType isScalarNum "<=" "lessThanEqual" + "GreaterThan" -> ifType isScalarNum ">" "greaterThan" + "GreaterThanEqual" -> ifType isScalarNum ">=" "greaterThanEqual" + "Equal" -> "==" + "EqualV" -> ifType isScalar "==" "equal" + "NotEqual" -> "!=" + "NotEqualV" -> ifType isScalar "!=" "notEqual" + + -- Angle and Trigonometry Functions + "ATan2" -> "atan" + -- Exponential Functions + "InvSqrt" -> "inversesqrt" + -- Common Functions + "RoundEven" -> "roundEven" + "ModF" -> error "PrimModF is not implemented yet!" -- TODO + "MixB" -> "mix" + + n | n `elem` + -- Logic Functions + [ "Any", "All" + -- Angle and Trigonometry Functions + , "ACos", "ACosH", "ASin", "ASinH", "ATan", "ATanH", "Cos", "CosH", "Degrees", "Radians", "Sin", "SinH", "Tan", "TanH" + -- Exponential Functions + , "Pow", "Exp", "Exp2", "Log2", "Sqrt" + -- Common Functions + , "IsNan", "IsInf", "Abs", "Sign", "Floor", "Trunc", "Round", "Ceil", "Fract", "Min", "Max", "Mix", "Step", "SmoothStep" + -- Geometric Functions + , "Length", "Distance", "Dot", "Cross", "Normalize", "FaceForward", "Reflect", "Refract" + -- Matrix Functions + , "Transpose", "Determinant", "Inverse" + -- Fragment Processing Functions + , "FWidth" + -- Noise Functions + , "Noise1", "Noise2", "Noise3", "Noise4" + ] -> map toLower n + + _ -> "" + + x -> error $ "GLSL codegen - unsupported expression: " ++ ppShow x + where + prefixOp o [a] = text o <+> parens (gen a) + binOp o [a, b] = parens (gen a) <+> text o <+> parens (gen b) + functionCall f a = text f <+> parens (hcat $ intersperse "," $ map gen a) + + gen = genGLSLSubst s + +isMatrix :: Ty -> Bool +isMatrix TMat{} = True +isMatrix _ = False + +isIntegral :: Ty -> Bool +isIntegral TWord = True +isIntegral TInt = True +isIntegral (TVec _ TWord) = True +isIntegral (TVec _ TInt) = True +isIntegral _ = False + +isScalarNum :: Ty -> Bool +isScalarNum = \case + TInt -> True + TWord -> True + TFloat -> True + _ -> False + +isScalar :: Ty -> Bool +isScalar = isJust . scalarType + +scalarType = \case + TBool -> Just "b" + TWord -> Just "u" + TInt -> Just "i" + TFloat -> Just "" + _ -> Nothing + +vecConName = \case + TVec n t | is234 n, Just s <- scalarType t -> Just $ s ++ "vec" ++ show n + t -> Nothing + +toGLSLType msg = \case + TBool -> "bool" + TWord -> "uint" + TInt -> "int" + TFloat -> "float" + x@(TVec n t) | Just s <- vecConName x -> s + TMat i j TFloat | is234 i && is234 j -> "mat" ++ if i == j then show i else show i ++ "x" ++ show j + TTuple [] -> "void" + t -> error $ "toGLSLType: " ++ msg ++ " " ++ ppShow t + +is234 = (`elem` [2,3,4]) + + +-------------------------------------------------------------------------------- + +data Exp_ a + = Pi_ Visibility SName a a + | Lam_ Visibility Pat a a + | Con_ SName a [a] + | ELit_ Lit + | Fun_ SName a [a] + | App_ a a + | Var_ SName a + | TType_ + | Let_ Pat a a + deriving (Show, Eq, Functor, Foldable, Traversable) + +instance PShow Exp where + pShowPrec p = \case + Var n t -> text n + TType -> "Type" + ELit a -> text $ show a + Con n t ps -> pApps p (text n) ps + Fun n t ps -> pApps p (text n) ps + EApp a b -> pApp p a b + Lam h n t e -> pParens True $ "\\" <> showVis h <> pShow n "->" <+> pShow e + Pi h n t e -> pParens True $ showVis h <> pShow n "->" <+> pShow e + ELet pat x e -> pParens (p > 0) $ "let" <+> pShow pat "=" <+> pShow x "in" <+> pShow e + where + showVis Visible = "" + showVis Hidden = "@" + +pattern Pi h n a b = Exp (Pi_ h n a b) +pattern Lam h n a b = Exp (Lam_ h n a b) +pattern Con n a b = Exp (Con_ (UntickName n) a b) +pattern ELit a = Exp (ELit_ a) +pattern Fun n a b = Exp (Fun_ (UntickName n) a b) +pattern EApp a b = Exp (App_ a b) +pattern Var a b = Exp (Var_ a b) +pattern TType = Exp TType_ +pattern ELet a b c = Exp (Let_ a b c) + +pattern UntickName n <- (untick -> n) where UntickName = untick + +pattern EString s = ELit (LString s) +pattern EFloat s = ELit (LFloat s) +pattern EInt s = ELit (LInt s) + +newtype Exp = Exp (Exp_ Exp) + deriving (Show, Eq) + +makeTE [] = I.EGlobal (error "makeTE - no source") I.initEnv $ error "makeTE" +makeTE ((_, t): vs) = I.EBind2 (I.BLam Visible) t $ makeTE vs + +toExp :: I.ExpType -> Exp +toExp = flip runReader [] . flip evalStateT freshTypeVars . f_ + where + freshTypeVars = flip (:) <$> map show [0..] <*> ['a'..'z'] + newName = gets head <* modify tail + f_ (e, et) + | isSampler et = newName >>= \n -> do + t <- f_ (et, I.TType) + ELet (PVar t n) <$> f__ (e, et) <*> pure (Var n t) + | otherwise = f__ (e, et) + f__ (e, et) = case e of + I.Var i -> asks $ fst . (!!! i) + I.Pi b x (I.down 0 -> Just y) -> Pi b "" <$> f_ (x, I.TType) <*> f_ (y, I.TType) + I.Pi b x y -> newName >>= \n -> do + t <- f_ (x, I.TType) + Pi b n t <$> local ((Var n t, x):) (f_ (y, I.TType)) + I.Lam y -> case et of + I.Pi b x yt -> newName >>= \n -> do + t <- f_ (x, I.TType) + Lam b (PVar t n) t <$> local ((Var n t, x):) (f_ (y, yt)) + I.Con s n xs -> Con (show s) <$> f_ (I.nType s, I.TType) <*> chain [] (I.nType s) (I.mkConPars n et ++ xs) + I.TyCon s xs -> Con (show s) <$> f_ (I.nType s, I.TType) <*> chain [] (I.nType s) xs + I.Fun s xs -> Fun (show s) <$> f_ (I.nType s, I.TType) <*> chain [] (I.nType s) xs + I.CaseFun s xs n -> asks makeTE >>= \te -> Fun (show s) <$> f_ (I.nType s, I.TType) <*> chain [] (I.nType s) (I.makeCaseFunPars te n ++ xs ++ [I.Neut n]) + I.Neut (I.App_ a b) -> asks makeTE >>= \te -> do + let t = I.neutType te a + app' <$> f_ (I.Neut a, t) <*> (head <$> chain [] t [b]) + I.ELit l -> pure $ ELit l + I.TType -> pure TType + x@I.PMLabel{} -> f_ (I.unpmlabel x, et) + I.FixLabel _ x -> f_ (x, et) +-- I.LabelEnd x -> f x -- not possible + z -> error $ "toExp: " ++ show z + + chain acc t [] = return $ reverse acc + chain acc t@(I.Pi b at y) (a: as) = do + a' <- f_ (a, at) + chain (a': acc) (I.appTy t a) as + + xs !!! i | i < 0 || i >= length xs = error $ show xs ++ " !! " ++ show i + xs !!! i = xs !! i + +isSampler (I.TyCon n _) = show n == "'Sampler" +isSampler _ = False + +untick ('\'': s) = s +untick s = s + +freeVars :: Exp -> Set.Set SName +freeVars = \case + Var n _ -> Set.singleton n + Con _ _ xs -> mconcat $ map freeVars xs + ELit _ -> mempty + Fun _ _ xs -> mconcat $ map freeVars xs + EApp a b -> freeVars a <> freeVars b + Pi _ n a b -> freeVars a <> Set.delete n (freeVars b) + Lam _ n a b -> freeVars a <> foldr Set.delete (freeVars b) (patVars n) + TType -> mempty + ELet n a b -> freeVars a <> foldr Set.delete (freeVars b) (patVars n) + +type Ty = Exp + +tyOf :: Exp -> Ty +tyOf = \case + Lam h (PVar _ n) t x -> Pi h n t $ tyOf x + EApp f x -> app (tyOf f) x + Var _ t -> t + Pi{} -> TType + Con _ t xs -> foldl app t xs + Fun _ t xs -> foldl app t xs + ELit l -> toExp (I.litType l, I.TType) + TType -> TType + ELet a b c -> tyOf $ EApp (ELam a c) b + x -> error $ "tyOf: " ++ ppShow x + where + app (Pi _ n a b) x = substE n x b + +substE n x = \case + z@(Var n' _) | n' == n -> x + | otherwise -> z + Pi h n' a b | n == n' -> Pi h n' (substE n x a) b + Pi h n' a b -> Pi h n' (substE n x a) (substE n x b) + Lam h n' a b -> Lam h n' (substE n x a) $ if n `elem` patVars n' then b else substE n x b + Con n' cn xs -> Con n' cn (map (substE n x) xs) + Fun n' cn xs -> Fun n' cn (map (substE n x) xs) + TType -> TType + EApp a b -> app' (substE n x a) (substE n x b) + x@ELit{} -> x + z -> error $ "substE: " ++ ppShow z + +app' (Lam _ (PVar _ n) _ x) b = substE n b x +app' a b = EApp a b + +-------------------------------------------------------------------------------- Exp conversion -- TODO: remove + +data Pat + = PVar Exp SName + | PTuple [Pat] + deriving (Eq, Show) + +instance PShow Pat where + pShowPrec p = \case + PVar t n -> text n + PTuple ps -> tupled $ map pShow ps + +patVars (PVar _ n) = [n] +patVars (PTuple ps) = concatMap patVars ps + +patTy (PVar t _) = t +patTy (PTuple ps) = Con ("Tuple" ++ show (length ps)) (tupTy $ length ps) $ map patTy ps + +tupTy n = foldr (:~>) TType $ replicate n TType + +-- workaround for backward compatibility +etaRed (ELam (PVar _ n) (EApp f (EVar n'))) | n == n' && n `Set.notMember` freeVars f = f +etaRed (ELam (PVar _ n) (Prim3 (tupCaseName -> Just k) _ x (EVar n'))) | n == n' && n `Set.notMember` freeVars x = uncurry (\ps e -> ELam (PTuple ps) e) $ getPats k x +etaRed x = x + +pattern EtaPrim1 s <- (getEtaPrim -> Just (s, [])) +pattern EtaPrim2 s x <- (getEtaPrim -> Just (s, [x])) +pattern EtaPrim3 s x1 x2 <- (getEtaPrim -> Just (s, [x1, x2])) +pattern EtaPrim4 s x1 x2 x3 <- (getEtaPrim -> Just (s, [x1, x2, x3])) +pattern EtaPrim5 s x1 x2 x3 x4 <- (getEtaPrim -> Just (s, [x1, x2, x3, x4])) +pattern EtaPrim2_2 s <- (getEtaPrim2 -> Just (s, [])) + +getEtaPrim (ELam (PVar _ n) (PrimN s (initLast -> Just (xs, EVar n')))) | n == n' && all (Set.notMember n . freeVars) xs = Just (s, xs) +getEtaPrim _ = Nothing + +getEtaPrim2 (ELam (PVar _ n) (ELam (PVar _ n2) (PrimN s (initLast -> Just (initLast -> Just (xs, EVar n'), EVar n2'))))) | n == n' && n2 == n2' && all (Set.notMember n . freeVars) xs = Just (s, xs) +getEtaPrim2 _ = Nothing + +initLast [] = Nothing +initLast xs = Just (init xs, last xs) + +tupCaseName "Tuple2Case" = Just 2 +tupCaseName "Tuple3Case" = Just 3 +tupCaseName "Tuple4Case" = Just 4 +tupCaseName "Tuple5Case" = Just 5 +tupCaseName "Tuple6Case" = Just 6 +tupCaseName "Tuple7Case" = Just 7 +tupCaseName _ = Nothing + +getPats 0 e = ([], e) +getPats i (ELam p e) = first (p:) $ getPats (i-1) e + +------------- + +pattern EVar n <- Var n _ + +pattern ELam n b <- Lam Visible n _ b where ELam n b = Lam Visible n (patTy n) b + +idFun t = Lam Visible (PVar t n) t (Var n t) where n = "id" + +pattern a :~> b = Pi Visible "" a b +infixr 1 :~> + +pattern PrimN n xs <- Fun n t (filterRelevant (n, 0) t -> xs) where PrimN n xs = Fun n (builtinType n) xs +pattern Prim1 n a = PrimN n [a] +pattern Prim2 n a b = PrimN n [a, b] +pattern Prim3 n a b c <- PrimN n [a, b, c] +pattern Prim4 n a b c d <- PrimN n [a, b, c, d] +pattern Prim5 n a b c d e <- PrimN n [a, b, c, d, e] + +builtinType = \case + "Output" -> TType + "Bool" -> TType + "Float" -> TType + "Nat" -> TType + "Zero" -> TNat + "Succ" -> TNat :~> TNat + "String" -> TType + "Sampler" -> TType + "VecS" -> TType :~> TNat :~> TType + n -> error $ "type of " ++ ppShow n + +filterRelevant _ _ [] = [] +filterRelevant i (Pi h n t t') (x: xs) = (if h == Visible then (x:) else id) $ filterRelevant (second (+1) i) (substE n x t') xs + +pattern AN n xs <- Con n t (filterRelevant (n, 0) t -> xs) where AN n xs = Con n (builtinType n) xs +pattern A0 n = AN n [] +pattern A1 n a = AN n [a] +pattern A2 n a b = AN n [a, b] +pattern A3 n a b c <- AN n [a, b, c] +pattern A4 n a b c d <- AN n [a, b, c, d] +pattern A5 n a b c d e <- AN n [a, b, c, d, e] + +pattern TCon0 n = A0 n +pattern TCon t n = Con n t [] + +pattern TUnit <- A0 "Tuple0" +pattern TBool = A0 "Bool" +pattern TWord <- A0 "Word" +pattern TInt <- A0 "Int" +pattern TNat = A0 "Nat" +pattern TFloat = A0 "Float" +pattern TString = A0 "String" + +pattern Uniform n <- Prim1 "Uniform" (EString n) + +pattern Zero = A0 "Zero" +pattern Succ n = A1 "Succ" n + +pattern TVec n a = A2 "VecS" a (Nat n) +pattern TMat i j a <- A3 "Mat" (Nat i) (Nat j) a + +pattern Nat n <- (fromNat -> Just n) where Nat = toNat + +toNat :: Int -> Exp +toNat 0 = Zero +toNat n = Succ (toNat $ n-1) + +fromNat :: Exp -> Maybe Int +fromNat Zero = Just 0 +fromNat (Succ n) = (1 +) <$> fromNat n +fromNat _ = Nothing + +pattern TTuple xs <- (getTuple -> Just xs) +pattern ETuple xs <- (getTuple -> Just xs) + +getTuple (AN (tupName -> Just n) xs) | length xs == n = Just xs +getTuple _ = Nothing + +tupName = \case + "Tuple0" -> Just 0 + "Tuple2" -> Just 2 + "Tuple3" -> Just 3 + "Tuple4" -> Just 4 + "Tuple5" -> Just 5 + "Tuple6" -> Just 6 + "Tuple7" -> Just 7 + _ -> Nothing + +pattern SwizzProj a b <- (getSwizzProj -> Just (a, b)) + +getSwizzProj = \case + Prim2 "swizzscalar" e (getSwizzChar -> Just s) -> Just (e, [s]) + Prim2 "swizzvector" e (AN ((`elem` ["V2","V3","V4"]) -> True) (traverse getSwizzChar -> Just s)) -> Just (e, s) + _ -> Nothing + +getSwizzChar = \case + A0 "Sx" -> Just 'x' + A0 "Sy" -> Just 'y' + A0 "Sz" -> Just 'z' + A0 "Sw" -> Just 'w' + _ -> Nothing + diff --git a/src/LambdaCube/Compiler/Infer.hs b/src/LambdaCube/Compiler/Infer.hs new file mode 100644 --- /dev/null +++ b/src/LambdaCube/Compiler/Infer.hs @@ -0,0 +1,1458 @@ +{-# LANGUAGE LambdaCase #-} +{-# LANGUAGE ViewPatterns #-} +{-# LANGUAGE PatternSynonyms #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE NoMonomorphismRestriction #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE RecursiveDo #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE UndecidableInstances #-} +{-# LANGUAGE GeneralizedNewtypeDeriving #-} +{-# LANGUAGE DeriveFunctor #-} +{-# OPTIONS_GHC -fno-warn-overlapping-patterns #-} -- TODO: remove +{-# OPTIONS_GHC -fno-warn-unused-binds #-} -- TODO: remove +-- {-# OPTIONS_GHC -O0 #-} +module LambdaCube.Compiler.Infer + ( Binder (..), SName, Lit(..), Visibility(..), Export(..), Module(..) + , Exp (..), ExpType, GlobalEnv + , pattern Var, pattern Fun, pattern CaseFun, pattern TyCaseFun, pattern App_, pattern PMLabel, pattern FixLabel + , pattern Con, pattern TyCon, pattern Pi, pattern Lam + , outputType, boolType, trueExp + , down + , litType + , initEnv, Env(..), pattern EBind2 + , Infos(..), listInfos, ErrorMsg(..), PolyEnv(..), ErrorT, throwErrorTCM, parseLC, joinPolyEnvs, filterPolyEnv, inference_ + , ImportItems (..) + , SI(..), Range(..) + , nType, neutType, appTy, mkConPars, makeCaseFunPars, unpmlabel + , MaxDB(..) + ) where +import Data.Monoid +import Data.Maybe +import qualified Data.Set as Set +import qualified Data.Map as Map + +import Control.Monad.Except +import Control.Monad.Reader +import Control.Monad.Writer +import Control.Monad.State +import Control.Monad.Identity +import Control.Arrow hiding ((<+>)) +import Control.DeepSeq + +import LambdaCube.Compiler.Pretty hiding (Doc, braces, parens) +import LambdaCube.Compiler.Lexer +import LambdaCube.Compiler.Parser + +-------------------------------------------------------------------------------- core expression representation + +data Exp + = TType + | ELit Lit + | Con_ MaxDB ConName !Int [Exp] + | TyCon_ MaxDB TyConName [Exp] + | Pi_ MaxDB Visibility Exp Exp + | Lam_ MaxDB Exp + | Neut Neutral + | Label LabelKind Exp{-folded expression-} Exp{-unfolded expression-} + | LabelEnd_ LEKind Exp + deriving (Show) + +data Neutral + = Fun__ MaxDB FunName [Exp] + | CaseFun__ MaxDB CaseFunName [Exp] Neutral + | TyCaseFun__ MaxDB TyCaseFunName [Exp] Neutral + | App__ MaxDB Neutral Exp + | Var_ !Int -- De Bruijn variable + | PMLabel_ FunName !Int [Exp] Exp{-unfolded expression-} + deriving (Show) + +data ConName = ConName SName MFixity Int{-ordinal number, e.g. Zero:0, Succ:1-} TyConName Type + +data TyConName = TyConName SName MFixity Int{-num of indices-} Type [ConName]{-constructors-} CaseFunName + +data FunName = FunName_ SName ([Exp] -> Exp) MFixity Type +pattern FunName a b c <- FunName_ a _ b c where FunName a b c = funName a b c + +funName a b c = n where n = FunName_ a (getFunDef n) b c + +data CaseFunName = CaseFunName SName Type Int{-num of parameters-} + +data TyCaseFunName = TyCaseFunName SName Type + +type Type = Exp +type ExpType = (Exp, Type) +type SExp2 = SExp' ExpType + +instance Show ConName where show (ConName n _ _ _ _) = n +instance Eq ConName where ConName _ _ n _ _ == ConName _ _ n' _ _ = n == n' +instance Show TyConName where show (TyConName n _ _ _ _ _) = n +instance Eq TyConName where TyConName n _ _ _ _ _ == TyConName n' _ _ _ _ _ = n == n' +instance Show FunName where show (FunName n _ _) = n +instance Eq FunName where FunName n _ _ == FunName n' _ _ = n == n' +instance Show CaseFunName where show (CaseFunName n _ _) = caseName n +instance Eq CaseFunName where CaseFunName n _ _ == CaseFunName n' _ _ = n == n' +instance Show TyCaseFunName where show (TyCaseFunName n _) = MatchName n +instance Eq TyCaseFunName where TyCaseFunName n _ == TyCaseFunName n' _ = n == n' + +-------------------------------------------------------------------------------- auxiliary functions and patterns + +infixl 2 `App`, `app_` +infixr 1 :~> + +pattern Fun_ a b <- Fun__ _ a b where Fun_ a b = Fun__ (foldMap maxDB_ b) a b +pattern CaseFun_ a b c <- CaseFun__ _ a b c where CaseFun_ a b c = CaseFun__ (foldMap maxDB_ b <> maxDB_ c) a b c +pattern TyCaseFun_ a b c <- TyCaseFun__ _ a b c where TyCaseFun_ a b c = TyCaseFun__ (foldMap maxDB_ b <> maxDB_ c) a b c +pattern App_ a b <- App__ _ a b where App_ a b = App__ (maxDB_ a <> maxDB_ b) a b +pattern Fun a b = Neut (Fun_ a b) +pattern CaseFun a b c = Neut (CaseFun_ a b c) +pattern TyCaseFun a b c = Neut (TyCaseFun_ a b c) +pattern App a b <- Neut (App_ (Neut -> a) b) +pattern Var a = Neut (Var_ a) + +conParams (conTypeName -> TyConName _ _ _ _ _ (CaseFunName _ _ pars)) = pars +mkConPars n (snd . getParams -> TyCon (TyConName _ _ _ _ _ (CaseFunName _ _ pars)) xs) = take (min n pars) xs +mkConPars n x = error $ "mkConPars: " ++ ppShow x +conName a b c d = ConName a b c (get $ snd $ getParams d) d + where + get (TyCon s _) = s + +makeCaseFunPars te n = case neutType te n of + TyCon (TyConName _ _ _ _ _ (CaseFunName _ _ pars)) xs -> take pars xs + +pattern Closed :: () => Up a => a -> a +pattern Closed a <- a where Closed a = closedExp a + +pattern Con x n y <- Con_ _ x n y where Con x n y = Con_ (foldMap maxDB_ y) x n y +pattern ConN s a <- Con (ConName s _ _ _ _) _ a +tCon s i t a = Con (conName s Nothing i t) 0 a +pattern TyCon x y <- TyCon_ _ x y where TyCon x y = TyCon_ (foldMap maxDB_ y) x y +pattern Lam y <- Lam_ _ y where Lam y = Lam_ (lowerDB (maxDB_ y)) y +pattern Pi v x y <- Pi_ _ v x y where Pi v x y = Pi_ (maxDB_ x <> lowerDB (maxDB_ y)) v x y +pattern FunN a b <- Fun (FunName a _ _) b +pattern TFun a t b <- Fun (FunName a _ t) b where TFun a t b = Fun (FunName a Nothing t) b +pattern TFun' a t b <- Fun_ (FunName a _ t) b where TFun' a t b = Fun_ (FunName a Nothing t) b +pattern TyConN s a <- TyCon (TyConName s _ _ _ _ _) a +pattern TTyCon s t a <- TyCon (TyConName s _ _ t _ _) a where TTyCon s t a = TyCon (TyConName s Nothing (error "todo: inum") t (error "todo: tcn cons 2") $ CaseFunName (error "TTyCon-A") (error "TTyCon-B") $ length a) a +pattern TTyCon0 s <- TyCon (TyConName s _ _ TType _ _) [] where TTyCon0 s = Closed $ TyCon (TyConName s Nothing 0 TType (error "todo: tcn cons 3") $ CaseFunName (error "TTyCon0-A") (error "TTyCon0-B") 0) [] +pattern a :~> b = Pi Visible a b + +pattern Unit = TTyCon0 "'Unit" +pattern TInt = TTyCon0 "'Int" +pattern TNat = TTyCon0 "'Nat" +pattern TBool = TTyCon0 "'Bool" +pattern TFloat = TTyCon0 "'Float" +pattern TString = TTyCon0 "'String" +pattern TChar = TTyCon0 "'Char" +pattern TOrdering = TTyCon0 "'Ordering" +pattern TTuple2 a b = TTyCon "'Tuple2" (TType :~> TType :~> TType) [a, b] +pattern TVec a b = TTyCon "'VecS" (TType :~> TNat :~> TType) [b, a] +pattern Empty s <- TyCon (TyConName "'Empty" _ _ _ _ _) [EString s] where + Empty s = TyCon (TyConName "'Empty" Nothing (error "todo: inum2_") (TString :~> TType) (error "todo: tcn cons 3_") $ error "Empty") [EString s] + +pattern TT <- ConN "TT" _ where TT = Closed (tCon "TT" 0 Unit []) +pattern Zero <- ConN "Zero" _ where Zero = Closed (tCon "Zero" 0 TNat []) +pattern Succ n <- ConN "Succ" (n:_) where Succ n = tCon "Succ" 1 (TNat :~> TNat) [n] + +pattern CstrT t a b = TFun "'EqCT" (TType :~> Var 0 :~> Var 1 :~> TType) [t, a, b] +pattern CstrT' t a b = TFun' "'EqCT" (TType :~> Var 0 :~> Var 1 :~> TType) [t, a, b] +pattern ReflCstr x = TFun "reflCstr" (TType :~> CstrT TType (Var 0) (Var 0)) [x] +pattern Coe a b w x = TFun "coe" (TType :~> TType :~> CstrT TType (Var 1) (Var 0) :~> Var 2 :~> Var 2) [a,b,w,x] +pattern ParEval t a b = TFun "parEval" (TType :~> Var 0 :~> Var 1 :~> Var 2) [t, a, b] +pattern Undef t = TFun "undefined" (Pi Hidden TType (Var 0)) [t] +pattern T2 a b = TFun "'T2" (TType :~> TType :~> TType) [a, b] +pattern T2C a b = TFun "t2C" (Unit :~> Unit :~> Unit) [a, b] +pattern CSplit a b c <- FunN "'Split" [a, b, c] + +pattern EInt a = ELit (LInt a) +pattern EFloat a = ELit (LFloat a) +pattern EChar a = ELit (LChar a) +pattern EString a = ELit (LString a) +pattern EBool a <- (getEBool -> Just a) where EBool = mkBool +pattern ENat n <- (fromNatE -> Just n) where ENat = toNatE + +pattern LCon <- (isCon -> True) +pattern CFun <- (isCaseFun -> True) +pattern NoTup <- (noTup -> True) + +--pattern Sigma a b <- TyConN "Sigma" [a, Lam b] where Sigma a b = TTyCon "Sigma" (error "sigmatype") [a, Lam Visible a{-todo: don't duplicate-} b] +--pattern TVec a b = TTyCon "'Vec" (TNat :~> TType :~> TType) [a, b] +--pattern Tuple2 a b c d = tCon "Tuple2" 0 Tuple2Type [a, b, c, d] +--pattern Tuple0 = tCon "Tuple0" 0 TTuple0 [] +--pattern TTuple0 :: Exp +--pattern TTuple0 <- _ where TTuple0 = TTyCon0 "'Tuple0" +--pattern Tuple2Type :: Exp +--pattern Tuple2Type <- _ where Tuple2Type = Pi Hidden TType $ Pi Hidden TType $ Var 1 :~> Var 1 :~> TTuple2 (Var 3) (Var 2) +--tTuple3 a b c = TTyCon "'Tuple3" (TType :~> TType :~> TType :~> TType) [a, b, c] + +toNatE :: Int -> Exp +toNatE 0 = Closed Zero +toNatE n | n > 0 = Closed (Succ (toNatE (n - 1))) + +fromNatE :: Exp -> Maybe Int +fromNatE Zero = Just 0 +fromNatE (Succ n) = (1 +) <$> fromNatE n +fromNatE _ = Nothing + +mkBool False = Closed $ tCon "False" 0 TBool [] +mkBool True = Closed $ tCon "True" 1 TBool [] + +getEBool (ConN "False" _) = Just False +getEBool (ConN "True" _) = Just True +getEBool _ = Nothing + +isCaseFun Fun{} = True +isCaseFun CaseFun{} = True +isCaseFun TyCaseFun{} = True +isCaseFun _ = False + +isCon = \case + TType{} -> True + Con{} -> True + TyCon{} -> True + ELit{} -> True + _ -> False + +mkOrdering x = Closed $ case x of + LT -> tCon "LT" 0 TOrdering [] + EQ -> tCon "EQ" 1 TOrdering [] + GT -> tCon "GT" 2 TOrdering [] + +noTup (TyConN s _) = take 6 s /= "'Tuple" -- todo +noTup _ = False + +conTypeName :: ConName -> TyConName +conTypeName (ConName _ _ _ t _) = t + +outputType = TTyCon0 "'Output" +boolType = TBool +trueExp = EBool True + +-------------------------------------------------------------------------------- label handling + +data LabelKind + = {-LabelPM -- pattern match label + | -}LabelFix -- fix unfold label + deriving (Show) + +pattern PMLabel f i x y = Neut (PMLabel_ f i x y) +pattern FixLabel x y = Label LabelFix x y + +data LEKind + = LEPM + | LEClosed + deriving (Show, Eq) + +pattern LabelEnd x = LabelEnd_ LEPM x +--pattern ClosedExp x = LabelEnd_ LEClosed x + +label LabelFix x y = FixLabel x y +pmLabel :: FunName -> Int -> [Exp] -> Exp -> Exp +pmLabel _ _ _ (unlabel'' -> LabelEnd y) = y +pmLabel f i xs y@Neut{} = PMLabel f i xs y +pmLabel f i xs y@Lam{} = PMLabel f i xs y +pmLabel f i xs y = error $ "pmLabel: " ++ show y + +pattern UL a <- (unlabel -> a) where UL = unlabel + +unpmlabel (PMLabel f i a _) + | i >= 0 = iterateN i Lam $ Fun f $ a ++ downTo 0 i + | otherwise = foldl app_ (Fun f $ reverse $ drop (-i) $ reverse a) (reverse $ take (-i) $ reverse a) + +unlabel x@PMLabel{} = unlabel (unpmlabel x) +unlabel (FixLabel _ a) = unlabel a +--unlabel (LabelEnd_ _ a) = unlabel a +unlabel a = a + +unlabel'' (FixLabel _ a) = unlabel'' a +unlabel'' a = a + +pattern UL' a <- (unlabel' -> a) where UL' = unlabel' + +--unlabel (PMLabel a _) = unlabel a +--unlabel (FixLabel _ a) = unlabel a +unlabel' (LabelEnd_ _ a) = unlabel' a +unlabel' a = a + + +-------------------------------------------------------------------------------- low-level toolbox + +class Up a => Subst b a where + subst :: Int -> b -> a -> a + +down :: (Subst Exp a) => Int -> a -> Maybe a +down t x | used t x = Nothing + | otherwise = Just $ subst t (error "impossible: down" :: Exp) x + +instance Eq Exp where + FixLabel a _ == FixLabel a' _ = a == a' + FixLabel _ a == a' = a == a' + a == FixLabel _ a' = a == a' + LabelEnd_ k a == a' = a == a' + a == LabelEnd_ k' a' = a == a' + Lam a == Lam a' = a == a' + Pi a b c == Pi a' b' c' = (a, b, c) == (a', b', c') + Con a n b == Con a' n' b' = (a, n, b) == (a', n', b') + TyCon a b == TyCon a' b' = (a, b) == (a', b') + TType == TType = True + ELit l == ELit l' = l == l' + Neut a == Neut a' = a == a' + _ == _ = False + +instance Eq Neutral where + PMLabel_ f i a _ == PMLabel_ f' i' a' _ = (f, i, a) == (f', i', a') + Fun_ a b == Fun_ a' b' = (a, b) == (a', b') + CaseFun_ a b c == CaseFun_ a' b' c' = (a, b, c) == (a', b', c') + TyCaseFun_ a b c == TyCaseFun_ a' b' c' = (a, b, c) == (a', b', c') + App_ a b == App_ a' b' = (a, b) == (a', b') + Var_ a == Var_ a' = a == a' + _ == _ = False + +isClosed (maxDB_ -> MaxDB x) = isNothing x + +-- 0 means that no free variable is used +-- 1 means that only var 0 is used +maxDB = max 0 . fromMaybe 0 . getMaxDB . maxDB_ +upDB n (MaxDB i) = MaxDB $ (\x -> if x == 0 then x else x+n) <$> i + +free x | isClosed x = mempty +free x = fold (\i k -> Set.fromList [k - i | k >= i]) 0 x + +instance Up Exp where + up_ 0 = \_ e -> e + up_ n = f where + f i e | isClosed e = e + f i e = case e of + Lam_ md b -> Lam_ (upDB n md) (f (i+1) b) + Pi_ md h a b -> Pi_ (upDB n md) h (f i a) (f (i+1) b) + Con_ md s pn as -> Con_ (upDB n md) s pn $ map (f i) as + TyCon_ md s as -> TyCon_ (upDB n md) s $ map (f i) as + Neut x -> Neut $ up_ n i x + Label lk x y -> Label lk (f i x) $ f i y + LabelEnd_ k x -> LabelEnd_ k $ f i x + + used i e + | i >= maxDB e = False + | otherwise = ((getAny .) . fold ((Any .) . (==))) i e + + fold f i = \case + FixLabel _ x -> fold f i x + Lam b -> {-fold f i t <> todo: explain why this is not needed -} fold f (i+1) b + Pi _ a b -> fold f i a <> fold f (i+1) b + Con _ _ as -> foldMap (fold f i) as + TyCon _ as -> foldMap (fold f i) as + TType -> mempty + ELit _ -> mempty + LabelEnd_ _ x -> fold f i x + Neut x -> fold f i x + + maxDB_ = \case + Lam_ c _ -> c + Pi_ c _ _ _ -> c + Con_ c _ _ _ -> c + TyCon_ c _ _ -> c + + Neut x -> maxDB_ x + FixLabel x y -> maxDB_ x <> maxDB_ y + TType -> mempty + ELit _ -> mempty + LabelEnd_ _ x -> maxDB_ x + + closedExp = \case + Lam_ _ c -> Lam_ mempty c + Pi_ _ a b c -> Pi_ mempty a b c + Con_ _ a b c -> Con_ mempty a b c + TyCon_ _ a b -> TyCon_ mempty a b + Neut a -> Neut $ closedExp a + Label lk a b -> Label lk (closedExp a) (closedExp b) + LabelEnd a -> LabelEnd (closedExp a) + e -> e + +instance Subst Exp Exp where + subst i0 x = f i0 + where + f i (Neut n) = substNeut n + where + substNeut e | isClosed e = Neut e + substNeut e = case e of + Var_ k -> case compare k i of GT -> Var $ k - 1; LT -> Var k; EQ -> up (i - i0) x + Fun_ s as -> evalFun s $ f i <$> as + CaseFun_ s as n -> evalCaseFun s (f i <$> as) (substNeut n) + TyCaseFun_ s as n -> evalTyCaseFun s (f i <$> as) (substNeut n) + App_ a b -> app_ (substNeut a) (f i b) + PMLabel_ fn c xs v -> pmLabel fn c (f i <$> xs) $ f i v + f i e | {-i >= maxDB e-} isClosed e = e + f i e = case e of + Label lk z v -> label lk (f i z) $ f i v + Lam b -> Lam (f (i+1) b) + Con s n as -> Con s n $ f i <$> as + Pi h a b -> Pi h (f i a) (f (i+1) b) + TyCon s as -> TyCon s $ f i <$> as + LabelEnd_ k a -> LabelEnd_ k $ f i a + +instance Up Neutral where + + up_ 0 = \_ e -> e + up_ n = f where + f i e | isClosed e = e + f i e = case e of + Var_ k -> Var_ $ if k >= i then k+n else k + Fun__ md s as -> Fun__ (upDB n md) s $ map (up_ n i) as + CaseFun__ md s as ne -> CaseFun__ (upDB n md) s (up_ n i <$> as) (up_ n i ne) + TyCaseFun__ md s as ne -> TyCaseFun__ (upDB n md) s (up_ n i <$> as) (up_ n i ne) + App__ md a b -> App__ (upDB n md) (up_ n i a) (up_ n i b) + PMLabel_ fn c x y -> PMLabel_ fn c (up_ n i <$> x) $ up_ n i y + + used i e + | i >= maxDB e = False + | otherwise = ((getAny .) . fold ((Any .) . (==))) i e + + fold f i = \case + Var_ k -> f i k + Fun_ _ as -> foldMap (fold f i) as + CaseFun_ _ as n -> foldMap (fold f i) as <> fold f i n + TyCaseFun_ _ as n -> foldMap (fold f i) as <> fold f i n + App_ a b -> fold f i a <> fold f i b + PMLabel_ _ _ x _ -> foldMap (fold f i) x + + maxDB_ = \case + Var_ k -> varDB k + Fun__ c _ _ -> c + CaseFun__ c _ _ _ -> c + TyCaseFun__ c _ _ _ -> c + App__ c a b -> c + PMLabel_ _ _ x _ -> foldMap maxDB_ x + + closedExp = \case + x@Var_{} -> error "impossible" + Fun__ _ a as -> Fun__ mempty a as + CaseFun__ _ a as n -> CaseFun__ mempty a as n + TyCaseFun__ _ a as n -> TyCaseFun__ mempty a as n + App__ _ a b -> App__ mempty a b + PMLabel_ f i x y -> PMLabel_ f i (map closedExp x) (closedExp y) + +instance (Subst x a, Subst x b) => Subst x (a, b) where + subst i x (a, b) = (subst i x a, subst i x b) + +varType :: String -> Int -> Env -> (Binder, Exp) +varType err n_ env = f n_ env where + f n (EAssign i (x, _) es) = second (subst i x) $ f (if n < i then n else n+1) es + f n (EBind2 b t es) = if n == 0 then (b, up 1 t) else second (up 1) $ f (n-1) es + f n (ELet2 _ (x, t) es) = if n == 0 then (BLam Visible{-??-}, up 1 t) else second (up 1) $ f (n-1) es + f n e = either (error $ "varType: " ++ err ++ "\n" ++ show n_ ++ "\n" ++ ppShow env) (f n) $ parent e + +-------------------------------------------------------------------------------- reduction + +evalCaseFun a ps (Con (ConName _ _ i _ _) _ vs) + | i /= (-1) = foldl app_ (ps !! (i + 1)) vs + | otherwise = error "evcf" +evalCaseFun a b (Neut c) = CaseFun a b c +evalCaseFun a b (FixLabel _ c) = evalCaseFun a b c + +evalTyCaseFun a b (Neut c) = TyCaseFun a b c +evalTyCaseFun a b (FixLabel _ c) = evalTyCaseFun a b c +evalTyCaseFun (TyCaseFunName n ty) [_, t, f] (TyCon (TyConName n' _ _ _ _ _) vs) | n == n' = foldl app_ t vs +evalTyCaseFun (TyCaseFunName n ty) [_, t, f] _ = f + +evalCoe a b TT d = d +evalCoe a b t d = Coe a b t d + +{- todo: generate + Fun n@(FunName "natElim" _ _) [a, z, s, Succ x] -> let -- todo: replace let with better abstraction + sx = s `app_` x + in sx `app_` eval (Fun n [a, z, s, x]) + MT "natElim" [_, z, s, Zero] -> z + Fun na@(FunName "finElim" _ _) [m, z, s, n, ConN "FSucc" [i, x]] -> let six = s `app_` i `app_` x-- todo: replace let with better abstraction + in six `app_` eval (Fun na [m, z, s, i, x]) + MT "finElim" [m, z, s, n, ConN "FZero" [i]] -> z `app_` i +-} + +evalFun s@(FunName_ _ f _ _) = f + +getFunDef s = case show s of + "unsafeCoerce" -> \case [_, _, x@LCon] -> x; xs -> f xs + "'EqCT" -> \case [t, a, b] -> cstrT'' t a b + "reflCstr" -> \case [a] -> reflCstr a + "coe" -> \case [a, b, t, d] -> evalCoe a b t d + "'T2" -> \case [a, b] -> t2 a b + "t2C" -> \case [a, b] -> t2C a b + "parEval" -> \case [t, a, b] -> parEval t a b + where + parEval _ (LabelEnd x) _ = LabelEnd x + parEval _ _ (LabelEnd x) = LabelEnd x + parEval t a b = ParEval t a b + + -- general compiler primitives + "primAddInt" -> \case [EInt i, EInt j] -> EInt (i + j); xs -> f xs + "primSubInt" -> \case [EInt i, EInt j] -> EInt (i - j); xs -> f xs + "primModInt" -> \case [EInt i, EInt j] -> EInt (i `mod` j); xs -> f xs + "primSqrtFloat" -> \case [EFloat i] -> EFloat $ sqrt i; xs -> f xs + "primRound" -> \case [EFloat i] -> EInt $ round i; xs -> f xs + "primIntToFloat" -> \case [EInt i] -> EFloat $ fromIntegral i; xs -> f xs + "primIntToNat" -> \case [EInt i] -> ENat $ fromIntegral i; xs -> f xs + "primCompareInt" -> \case [EInt x, EInt y] -> mkOrdering $ x `compare` y; xs -> f xs + "primCompareFloat" -> \case [EFloat x, EFloat y] -> mkOrdering $ x `compare` y; xs -> f xs + "primCompareChar" -> \case [EChar x, EChar y] -> mkOrdering $ x `compare` y; xs -> f xs + "primCompareString" -> \case [EString x, EString y] -> mkOrdering $ x `compare` y; xs -> f xs + + -- LambdaCube 3D specific primitives + "PrimGreaterThan" -> \case [_, _, _, _, _, _, _, x, y] | Just r <- twoOpBool (>) x y -> r; xs -> f xs + "PrimGreaterThanEqual" -> \case [_, _, _, _, _, _, _, x, y] | Just r <- twoOpBool (>=) x y -> r; xs -> f xs + "PrimLessThan" -> \case [_, _, _, _, _, _, _, x, y] | Just r <- twoOpBool (<) x y -> r; xs -> f xs + "PrimLessThanEqual" -> \case [_, _, _, _, _, _, _, x, y] | Just r <- twoOpBool (<=) x y -> r; xs -> f xs + "PrimEqualV" -> \case [_, _, _, _, _, _, _, x, y] | Just r <- twoOpBool (==) x y -> r; xs -> f xs + "PrimNotEqualV" -> \case [_, _, _, _, _, _, _, x, y] | Just r <- twoOpBool (/=) x y -> r; xs -> f xs + "PrimEqual" -> \case [_, _, _, x, y] | Just r <- twoOpBool (==) x y -> r; xs -> f xs + "PrimNotEqual" -> \case [_, _, _, x, y] | Just r <- twoOpBool (/=) x y -> r; xs -> f xs + "PrimSubS" -> \case [_, _, _, _, x, y] | Just r <- twoOp (-) x y -> r; xs -> f xs + "PrimSub" -> \case [_, _, x, y] | Just r <- twoOp (-) x y -> r; xs -> f xs + "PrimAddS" -> \case [_, _, _, _, x, y] | Just r <- twoOp (+) x y -> r; xs -> f xs + "PrimAdd" -> \case [_, _, x, y] | Just r <- twoOp (+) x y -> r; xs -> f xs + "PrimMulS" -> \case [_, _, _, _, x, y] | Just r <- twoOp (*) x y -> r; xs -> f xs + "PrimMul" -> \case [_, _, x, y] | Just r <- twoOp (*) x y -> r; xs -> f xs + "PrimDivS" -> \case [_, _, _, _, _, x, y] | Just r <- twoOp_ (/) div x y -> r; xs -> f xs + "PrimDiv" -> \case [_, _, _, _, _, x, y] | Just r <- twoOp_ (/) div x y -> r; xs -> f xs + "PrimModS" -> \case [_, _, _, _, _, x, y] | Just r <- twoOp_ modF mod x y -> r; xs -> f xs + "PrimMod" -> \case [_, _, _, _, _, x, y] | Just r <- twoOp_ modF mod x y -> r; xs -> f xs + "PrimNeg" -> \case [_, x] | Just r <- oneOp negate x -> r; xs -> f xs + "PrimAnd" -> \case [EBool x, EBool y] -> EBool (x && y); xs -> f xs + "PrimOr" -> \case [EBool x, EBool y] -> EBool (x || y); xs -> f xs + "PrimXor" -> \case [EBool x, EBool y] -> EBool (x /= y); xs -> f xs + "PrimNot" -> \case [_, _, _, EBool x] -> EBool $ not x; xs -> f xs + + _ -> f + where + f = Fun s + +cstrT'' TType = cstrT_ TType +cstrT'' t = cstrT t + +cstr = cstrT_ TType + + +cstrT t (UL a) (UL a') | a == a' = Unit +cstrT TNat (ConN "Succ" [a]) (ConN "Succ" [a']) = cstrT TNat a a' +cstrT t (FixLabel _ a) a' = cstrT t a a' +cstrT t a (FixLabel _ a') = cstrT t a a' +cstrT t a a' = CstrT t a a' + +-- todo: use typ +cstrT_ typ = cstr__ [] + where + cstr__ = cstr_ + + cstr_ [] (UL a) (UL a') | a == a' = Unit + cstr_ ns (LabelEnd_ k a) a' = cstr_ ns a a' + cstr_ ns a (LabelEnd_ k a') = cstr_ ns a a' + cstr_ ns (FixLabel _ a) a' = cstr_ ns a a' + cstr_ ns a (FixLabel _ a') = cstr_ ns a a' +-- cstr_ ns (PMLabel a _) a' = cstr_ ns a a' +-- cstr_ ns a (PMLabel a' _) = cstr_ ns a a' +-- cstr_ ns TType TType = Unit + cstr_ ns (Con a n xs) (Con a' n' xs') | a == a' && n == n' = foldr t2 Unit $ zipWith (cstr__ ns) xs xs' + cstr_ [] (TyConN "'FrameBuffer" [a, b]) (TyConN "'FrameBuffer" [a', b']) = t2 (cstrT TNat a a') (cstr__ [] b b') -- todo: elim + cstr_ ns (TyCon a xs) (TyCon a' xs') | a == a' = foldr t2 Unit $ zipWith (cstr__ ns) xs xs' +-- cstr_ ns (TyCon a []) (TyCon a' []) | a == a' = Unit + cstr_ ns (Var i) (Var i') | i == i', i < length ns = Unit + cstr_ (_: ns) (down 0 -> Just a) (down 0 -> Just a') = cstr__ ns a a' +-- cstr_ ((t, t'): ns) (UApp (down 0 -> Just a) (Var 0)) (UApp (down 0 -> Just a') (Var 0)) = traceInj2 (a, "V0") (a', "V0") $ cstr__ ns a a' +-- cstr_ ((t, t'): ns) a (UApp (down 0 -> Just a') (Var 0)) = traceInj (a', "V0") a $ cstr__ ns (Lam Visible t a) a' +-- cstr_ ((t, t'): ns) (UApp (down 0 -> Just a) (Var 0)) a' = traceInj (a, "V0") a' $ cstr__ ns a (Lam Visible t' a') +-- cstr_ ns (Lam b) (Lam b') = cstr__ ((a, a'): ns) b b' -- todo + cstr_ ns (Pi h a b) (Pi h' a' b') | h == h' = t2 (cstr__ ns a a') (cstr__ ((a, a'): ns) b b') +-- cstr_ ns (Meta a b) (Meta a' b') = t2 (cstr__ ns a a') (cstr__ ((a, a'): ns) b b') +-- cstr_ [] t (Meta a b) = Meta a $ cstr_ [] (up 1 t) b +-- cstr_ [] (Meta a b) t = Meta a $ cstr_ [] b (up 1 t) +-- cstr_ ns (unApp -> Just (a, b)) (unApp -> Just (a', b')) = traceInj2 (a, show b) (a', show b') $ t2 (cstr__ ns a a') (cstr__ ns b b') +-- cstr_ ns (unApp -> Just (a, b)) (unApp -> Just (a', b')) = traceInj2 (a, show b) (a', show b') $ t2 (cstr__ ns a a') (cstr__ ns b b') +-- cstr_ ns (Label f xs _) (Label f' xs' _) | f == f' = foldr1 T2 $ zipWith (cstr__ ns) xs xs' + + cstr_ [] (UL (FunN "'VecScalar" [a, b])) (TVec a' b') = t2 (cstrT TNat a a') (cstr__ [] b b') + cstr_ [] (UL (FunN "'VecScalar" [a, b])) (UL (FunN "'VecScalar" [a', b'])) = t2 (cstrT TNat a a') (cstr__ [] b b') + cstr_ [] (UL (FunN "'VecScalar" [a, b])) t@(TTyCon0 n) | isElemTy n = t2 (cstrT TNat a (ENat 1)) (cstr__ [] b t) + cstr_ [] t@(TTyCon0 n) (UL (FunN "'VecScalar" [a, b])) | isElemTy n = t2 (cstrT TNat a (ENat 1)) (cstr__ [] b t) + + cstr_ ns@[] (UL (FunN "'FragOps" [a])) (TyConN "'FragmentOperation" [x]) = cstr__ ns a x + cstr_ ns@[] (UL (FunN "'FragOps" [a])) (TyConN "'Tuple2" [TyConN "'FragmentOperation" [x], TyConN "'FragmentOperation" [y]]) = cstr__ ns a $ TTuple2 x y + + cstr_ ns@[] (TyConN "'Tuple2" [x, y]) (UL (FunN "'JoinTupleType" [x', y'])) = t2 (cstr__ ns x x') (cstr__ ns y y') + cstr_ ns@[] (UL (FunN "'JoinTupleType" [x', y'])) (TyConN "'Tuple2" [x, y]) = t2 (cstr__ ns x' x) (cstr__ ns y' y) + cstr_ ns@[] (UL (FunN "'JoinTupleType" [x', y'])) x@NoTup = t2 (cstr__ ns x' x) (cstr__ ns y' $ TTyCon0 "'Tuple0") + + cstr_ ns@[] (x@NoTup) (UL (FunN "'InterpolatedType" [x'])) = cstr__ ns (TTyCon "'Interpolated" (TType :~> TType) [x]) x' + +-- cstr_ [] (TyConN "'FrameBuffer" [a, b]) (UL (FunN "'TFFrameBuffer" [TyConN "'Image" [a', b']])) = T2 (cstrT TNat a a') (cstr__ [] b b') + + cstr_ [] a@App{} a'@App{} = CstrT TType a a' + cstr_ [] a@CFun a'@CFun = CstrT TType a a' + cstr_ [] a@LCon a'@CFun = CstrT TType a a' + cstr_ [] a@LCon a'@App{} = CstrT TType a a' + cstr_ [] a@CFun a'@LCon = CstrT TType a a' + cstr_ [] a@App{} a'@LCon = CstrT TType a a' + cstr_ [] a@PMLabel{} a' = CstrT TType a a' + cstr_ [] a a'@PMLabel{} = CstrT TType a a' + cstr_ [] a a' | isVar a || isVar a' = CstrT TType a a' + cstr_ ns a a' = Empty $ unlines [ "can not unify" + , ppShow a + , "with" + , ppShow a' + ] +{- +-- unApp (UApp a b) | isInjective a = Just (a, b) -- TODO: injectivity check + unApp (Con a xs@(_:_)) = Just (Con a (init xs), last xs) + unApp (TyCon a xs@(_:_)) = Just (TyCon a (init xs), last xs) + unApp _ = Nothing +-} + isInjective _ = True--False + + isVar Var{} = True + isVar (App a b) = isVar a + isVar _ = False + + traceInj2 (a, a') (b, b') c | debug && (susp a || susp b) = trace_ (" inj'? " ++ show a ++ " : " ++ a' ++ " ---- " ++ show b ++ " : " ++ b') c + traceInj2 _ _ c = c + traceInj (x, y) z a | debug && susp x = trace_ (" inj? " ++ show x ++ " : " ++ y ++ " ---- " ++ show z) a + traceInj _ _ a = a + + susp Con{} = False + susp TyCon{} = False + susp _ = True + + isElemTy n = n `elem` ["'Bool", "'Float", "'Int"] + +reflCstr = \case +{- + Unit -> TT + TType -> TT -- ? + Con n xs -> foldl (t2C te{-todo: more precise env-}) TT $ map (reflCstr te{-todo: more precise env-}) xs + TyCon n xs -> foldl (t2C te{-todo: more precise env-}) TT $ map (reflCstr te{-todo: more precise env-}) xs + x -> {-error $ "reflCstr: " ++ show x-} ReflCstr x +-} + x -> TT + +t2C TT TT = TT +t2C a b = T2C a b + +t2 Unit a = a +t2 a Unit = a +t2 (Empty a) (Empty b) = Empty (a <> b) +t2 (Empty s) _ = Empty s +t2 _ (Empty s) = Empty s +t2 a b = T2 a b + +oneOp :: (forall a . Num a => a -> a) -> Exp -> Maybe Exp +oneOp f = oneOp_ f f + +oneOp_ f _ (EFloat x) = Just $ EFloat $ f x +oneOp_ _ f (EInt x) = Just $ EInt $ f x +oneOp_ _ _ _ = Nothing + +twoOp :: (forall a . Num a => a -> a -> a) -> Exp -> Exp -> Maybe Exp +twoOp f = twoOp_ f f + +twoOp_ f _ (EFloat x) (EFloat y) = Just $ EFloat $ f x y +twoOp_ _ f (EInt x) (EInt y) = Just $ EInt $ f x y +twoOp_ _ _ _ _ = Nothing + +modF x y = x - fromIntegral (floor (x / y)) * y + +twoOpBool :: (forall a . Ord a => a -> a -> Bool) -> Exp -> Exp -> Maybe Exp +twoOpBool f (EFloat x) (EFloat y) = Just $ EBool $ f x y +twoOpBool f (EInt x) (EInt y) = Just $ EBool $ f x y +twoOpBool f (EString x) (EString y) = Just $ EBool $ f x y +twoOpBool f (EChar x) (EChar y) = Just $ EBool $ f x y +twoOpBool f (ENat x) (ENat y) = Just $ EBool $ f x y +twoOpBool _ _ _ = Nothing + +app_ :: Exp -> Exp -> Exp +app_ (Lam x) a = subst 0 a x +app_ (Con s n xs) a = if n < conParams s then Con s (n+1) xs else Con s n (xs ++ [a]) +app_ (TyCon s xs) a = TyCon s (xs ++ [a]) +app_ (Label lk x e) a = label lk (app_ x a) $ app_ e a +app_ (LabelEnd_ k x) a = LabelEnd_ k (app_ x a) -- ??? +app_ (Neut f) a = neutApp f a + +neutApp (PMLabel_ f i xs e) a + = pmLabel f (i-1) (xs ++ [a]) (app_ e a) +-- | i == 0 = app_ (pmLabel f i xs e) a +neutApp f a = Neut $ App_ f a + +-------------------------------------------------------------------------------- constraints env + +data CEnv a + = MEnd a + | Meta Exp (CEnv a) + | Assign !Int ExpType (CEnv a) -- De Bruijn index decreasing assign reservedOp, only for metavariables (non-recursive) + deriving (Show, Functor) + +instance (Subst Exp a) => Up (CEnv a) where + up1_ i = \case + MEnd a -> MEnd $ up1_ i a + Meta a b -> Meta (up1_ i a) (up1_ (i+1) b) + Assign j a b -> handleLet i j $ \i' j' -> assign j' (up1_ i' a) (up1_ i' b) + where + handleLet i j f + | i > j = f (i-1) j + | i <= j = f i (j+1) + + used i a = error "used @(CEnv _)" + + fold _ _ _ = error "fold @(CEnv _)" + + maxDB_ _ = error "maxDB_ @(CEnv _)" + +instance (Subst Exp a) => Subst Exp (CEnv a) where + subst i x = \case + MEnd a -> MEnd $ subst i x a + Meta a b -> Meta (subst i x a) (subst (i+1) (up 1 x) b) + Assign j a b + | j > i, Just a' <- down i a -> assign (j-1) a' (subst i (subst (j-1) (fst a') x) b) + | j > i, Just x' <- down (j-1) x -> assign (j-1) (subst i x' a) (subst i x' b) + | j < i, Just a' <- down (i-1) a -> assign j a' (subst (i-1) (subst j (fst a') x) b) + | j < i, Just x' <- down j x -> assign j (subst (i-1) x' a) (subst (i-1) x' b) + | j == i -> Meta (cstrT'' (snd a) x $ fst a) $ up1_ 0 b + +--assign :: (Int -> Exp -> CEnv Exp -> a) -> (Int -> Exp -> CEnv Exp -> a) -> Int -> Exp -> CEnv Exp -> a +swapAssign _ clet i (Var j, t) b | i > j = clet j (Var (i-1), t) $ subst j (Var (i-1)) $ up1_ i b +swapAssign clet _ i a b = clet i a b + +assign = swapAssign Assign Assign + + +-------------------------------------------------------------------------------- environments + +-- SExp + Exp zipper +data Env + = EBind1 SI Binder Env SExp2 -- zoom into first parameter of SBind + | EBind2_ SI Binder Type Env -- zoom into second parameter of SBind + | EApp1 SI Visibility Env SExp2 + | EApp2 SI Visibility ExpType Env + | ELet1 LI Env SExp2 + | ELet2 LI ExpType Env + | EGlobal String{-full source of current module-} GlobalEnv [Stmt] + | ELabelEnd Env + + | EAssign Int ExpType Env + | CheckType_ SI Type Env + | CheckIType SExp2 Env +-- | CheckSame Exp Env + | CheckAppType SI Visibility Type Env SExp2 --pattern CheckAppType _ h t te b = EApp1 _ h (CheckType t te) b + deriving Show + +pattern EBind2 b e env <- EBind2_ _ b e env where EBind2 b e env = EBind2_ (debugSI "6") b e env +pattern CheckType e env <- CheckType_ _ e env where CheckType e env = CheckType_ (debugSI "7") e env + +parent = \case + EAssign _ _ x -> Right x + EBind2 _ _ x -> Right x + EBind1 _ _ x _ -> Right x + EApp1 _ _ x _ -> Right x + EApp2 _ _ _ x -> Right x + ELet1 _ x _ -> Right x + ELet2 _ _ x -> Right x + CheckType _ x -> Right x + CheckIType _ x -> Right x +-- CheckSame _ x -> Right x + CheckAppType _ _ _ x _ -> Right x + ELabelEnd x -> Right x + EGlobal s x _ -> Left (s, x) + +-------------------------------------------------------------------------------- simple typing + +litType = \case + LInt _ -> TInt + LFloat _ -> TFloat + LString _ -> TString + LChar _ -> TChar + +class NType a where nType :: a -> Type + +instance NType FunName where nType (FunName _ _ t) = t +instance NType ConName where nType (ConName _ _ _ _ t) = t +instance NType TyConName where nType (TyConName _ _ _ t _ _) = t +instance NType CaseFunName where nType (CaseFunName _ t _) = t +instance NType TyCaseFunName where nType (TyCaseFunName _ t) = t + +neutType te = \case + App_ f x -> appTy (neutType te f) x + Var_ i -> snd $ varType "C" i te + Fun_ s ts -> foldl appTy (nType s) ts + CaseFun_ s ts n -> appTy (foldl appTy (nType s) $ makeCaseFunPars te n ++ ts) (Neut n) + TyCaseFun_ s [m, t, f] n -> foldl appTy (nType s) [m, t, Neut n, f] + PMLabel_ s _ a _ -> foldl appTy (nType s) a + +appTy (Pi _ a b) x = subst 0 x b +appTy t x = error $ "appTy: " ++ show t + +-------------------------------------------------------------------------------- inference + +type TCM m = ExceptT String (WriterT Infos m) + +--runTCM = either error id . runExcept + +expAndType s (e, t, si) = (e, t) + +-- todo: do only if NoTypeNamespace extension is not on +lookupName s@('\'':s') m = expAndType s <$> (Map.lookup s m `mplus` Map.lookup s' m) +lookupName s m = expAndType s <$> Map.lookup s m +--elemIndex' s@('\'':s') m = elemIndex s m `mplus` elemIndex s' m +--elemIndex' s m = elemIndex s m + +getDef te si s = maybe (throwError $ "can't find: " ++ s ++ " in " ++ showSI te si {- ++ "\nitems:\n" ++ intercalate ", " (take' "..." 10 $ Map.keys $ snd $ extractEnv te)-}) return (lookupName s $ snd $ extractEnv te) +{- +take' e n xs = case splitAt n xs of + (as, []) -> as + (as, _) -> as ++ [e] +-} +showSI :: Env -> SI -> String +showSI e = showSI_ (fst $ extractEnv e) + +type ExpType' = CEnv ExpType + +inferN :: forall m . Monad m => TraceLevel -> Env -> SExp2 -> TCM m ExpType' +inferN tracelevel = infer where + + infer :: Env -> SExp2 -> TCM m ExpType' + infer te exp = (if tracelevel >= 1 then trace_ ("infer: " ++ showEnvSExp te exp) else id) $ (if debug then fmap (fmap{-todo-} $ recheck' "infer" te) else id) $ case exp of + SAnn x t -> checkN (CheckIType x te) t TType + SLabelEnd x -> infer (ELabelEnd te) x + SVar (si, _) i -> focus_' te exp (Var i, snd $ varType "C2" i te) + SLit si l -> focus_' te exp (ELit l, litType l) + STyped si et -> focus_' te exp et + SGlobal (si, s) -> focus_' te exp =<< getDef te si s + SApp si h a b -> infer (EApp1 (si `validate` [sourceInfo a, sourceInfo b]) h te b) a + SLet le a b -> infer (ELet1 le te b{-in-}) a{-let-} -- infer te SLamV b `SAppV` a) + SBind si h _ a b -> infer ((if h /= BMeta then CheckType_ (sourceInfo exp) TType else id) $ EBind1 si h te $ (if isPi h then TyType else id) b) a + + checkN :: Env -> SExp2 -> Exp -> TCM m ExpType' + checkN te x t = (if tracelevel >= 1 then trace_ $ "check: " ++ showEnvSExpType te x t else id) $ checkN_ te x t + + checkN_ te e t + -- temporal hack + | x@(SGlobal (si, MatchName n)) `SAppV` SLamV (Wildcard_ siw _) `SAppV` a `SAppV` SVar siv v `SAppV` b <- e + = infer te $ x `SAppV` SLam Visible SType (STyped mempty (subst (v+1) (Var 0) $ up 1 t, TType)) `SAppV` a `SAppV` SVar siv v `SAppV` b + -- temporal hack + | x@(SGlobal (si, "'NatCase")) `SAppV` SLamV (Wildcard_ siw _) `SAppV` a `SAppV` b `SAppV` SVar siv v <- e + = infer te $ x `SAppV` STyped mempty (Lam $ subst (v+1) (Var 0) $ up 1 t, TNat :~> TType) `SAppV` a `SAppV` b `SAppV` SVar siv v +{- + -- temporal hack + | x@(SGlobal "'VecSCase") `SAppV` SLamV (SLamV (Wildcard _)) `SAppV` a `SAppV` b `SAppV` c `SAppV` SVar v <- e + = infer te $ x `SAppV` (SLamV (SLamV (STyped (subst (v+1) (Var 0) $ up 2 t, TType)))) `SAppV` a `SAppV` b `SAppV` c `SAppV` SVar v +-} + -- temporal hack + | SGlobal (si, "undefined") <- e = focus_' te e (Undef t, t) + | SLabelEnd x <- e = checkN (ELabelEnd te) x t + | SApp si h a b <- e = infer (CheckAppType si h t te b) a + | SLam h a b <- e, Pi h' x y <- t, h == h' = do + tellType te e t + let same = checkSame te a x + if same then checkN (EBind2 (BLam h) x te) b y else error $ "checkSame:\n" ++ show a ++ "\nwith\n" ++ showEnvExp te (x, TType) + | Pi Hidden a b <- t, notHiddenLam e = checkN (EBind2 (BLam Hidden) a te) (up1 e) b + | otherwise = infer (CheckType_ (sourceInfo e) t te) e + where + -- todo + notHiddenLam = \case + SLam Visible _ _ -> True + SGlobal (si,s) | (Lam _, Pi Hidden _ _) <- fromMaybe (error $ "infer: can't find: " ++ s) $ lookupName s $ snd $ extractEnv te -> False + | otherwise -> True + _ -> False +{- + -- todo + checkSame te (Wildcard _) a = return (te, True) + checkSame te x y = do + (ex, _) <- checkN te x TType + return $ ex == y +-} + checkSame te (Wildcard _) a = True + checkSame te (SGlobal (_,"'Type")) TType = True + checkSame te SType TType = True + checkSame te (SBind _ BMeta _ SType (STyped _ (Var 0, _))) a = True + checkSame te a b = error $ "checkSame: " ++ show (a, b) + + hArgs (Pi Hidden _ b) = 1 + hArgs b + hArgs _ = 0 + + focus_' env si eet = tellType env si (snd eet) >> focus_ env eet + + focus_ :: Env -> ExpType -> TCM m ExpType' + focus_ env eet@(e, et) = (if tracelevel >= 1 then trace_ $ "focus: " ++ showEnvExp env eet else id) $ (if debug then fmap (fmap{-todo-} $ recheck' "focus" env) else id) $ case env of + ELabelEnd te -> focus_ te (LabelEnd e, et) +-- CheckSame x te -> focus_ (EBind2_ (debugSI "focus_ CheckSame") BMeta (cstr x e) te) $ up 1 eet + CheckAppType si h t te b -- App1 h (CheckType t te) b + | Pi h' x (down 0 -> Just y) <- et, h == h' -> case t of + Pi Hidden t1 t2 | h == Visible -> focus_ (EApp1 si h (CheckType_ (sourceInfo b) t te) b) eet -- <> b : {t1} -> {t2} + _ -> focus_ (EBind2_ (sourceInfo b) BMeta (cstr t y) $ EApp1 si h te b) $ up 1 eet + | otherwise -> focus_ (EApp1 si h (CheckType_ (sourceInfo b) t te) b) eet + EApp1 si h te b + | Pi h' x y <- et, h == h' -> checkN (EApp2 si h eet te) b x + | Pi Hidden x y <- et, h == Visible -> focus_ (EApp1 mempty Hidden env $ Wildcard $ Wildcard SType) eet -- e b --> e _ b +-- | CheckType (Pi Hidden _ _) te' <- te -> error "ok" +-- | CheckAppType Hidden _ te' _ <- te -> error "ok" + | otherwise -> infer (CheckType_ (sourceInfo b) (Var 2) $ cstr' h (up 2 et) (Pi Visible (Var 1) (Var 1)) (up 2 e) $ EBind2_ (sourceInfo b) BMeta TType $ EBind2_ (sourceInfo b) BMeta TType te) (up 3 b) + where + cstr' h x y e = EApp2 mempty h (evalCoe (up 1 x) (up 1 y) (Var 0) (up 1 e), up 1 y) . EBind2_ (sourceInfo b) BMeta (cstr x y) + ELet2 le (x{-let-}, xt) te -> focus_ te $ subst 0 (mkELet le x xt){-let-} eet{-in-} + CheckIType x te -> checkN te x e + CheckType_ si t te + | hArgs et > hArgs t + -> focus_ (EApp1 mempty Hidden (CheckType_ si t te) $ Wildcard $ Wildcard SType) eet + | hArgs et < hArgs t, Pi Hidden t1 t2 <- t + -> focus_ (CheckType_ si t2 $ EBind2 (BLam Hidden) t1 te) eet + | otherwise -> focus_ (EBind2_ si BMeta (cstr t et) te) $ up 1 eet + EApp2 si h (a, at) te -> focus_' te si (app_ a e, appTy at e) -- h?? + EBind1 si h te b -> infer (EBind2_ (sourceInfo b) h e te) b + EBind2_ si (BLam h) a te -> focus_ te $ lamPi h a eet + EBind2_ si (BPi h) a te -> focus_' te si (Pi h a e, TType) + _ -> focus2 env $ MEnd eet + + focus2 :: Env -> CEnv ExpType -> TCM m ExpType' + focus2 env eet = case env of + ELet1 le te b{-in-} -> infer (ELet2 le (replaceMetas' eet{-let-}) te) b{-in-} + EBind2_ si BMeta tt te + | Unit <- tt -> refocus te $ subst 0 TT eet + | Empty msg <- tt -> throwError $ "type error: " ++ msg ++ "\nin " ++ showSI te si ++ "\n"-- todo: better error msg + | T2 x y <- tt, let te' = EBind2_ si BMeta (up 1 y) $ EBind2_ si BMeta x te + -> refocus te' $ subst 2 (t2C (Var 1) (Var 0)) $ up 2 eet + | CstrT t a b <- tt, a == b -> refocus te $ subst 0 TT eet + | CstrT t a b <- tt, Just r <- cst (a, t) b -> r + | CstrT t a b <- tt, Just r <- cst (b, t) a -> r + | isCstr tt, EBind2 h x te' <- te{-, h /= BMeta todo: remove-}, Just x' <- down 0 tt, x == x' + -> refocus te $ subst 1 (Var 0) eet + | EBind2 h x te' <- te, h /= BMeta, Just b' <- down 0 tt + -> refocus (EBind2_ si h (up 1 x) $ EBind2_ si BMeta b' te') $ subst 2 (Var 0) $ up 1 eet + | ELet2 le (x, xt) te' <- te, Just b' <- down 0 tt + -> refocus (ELet2 le (up 1 x, up 1 xt) $ EBind2_ si BMeta b' te') $ subst 2 (Var 0) $ up 1 eet + | EBind1 si h te' x <- te -> refocus (EBind1 si h (EBind2_ si BMeta tt te') $ up1_ 1 x) eet + | ELet1 le te' x <- te, floatLetMeta $ snd $ replaceMetas' $ Meta tt $ eet + -> refocus (ELet1 le (EBind2_ si BMeta tt te') $ up1_ 1 x) eet + | CheckAppType si h t te' x <- te -> refocus (CheckAppType si h (up 1 t) (EBind2_ si BMeta tt te') $ up1 x) eet + | EApp1 si h te' x <- te -> refocus (EApp1 si h (EBind2_ si BMeta tt te') $ up1 x) eet + | EApp2 si h x te' <- te -> refocus (EApp2 si h (up 1 x) $ EBind2_ si BMeta tt te') eet + | CheckType_ si t te' <- te -> refocus (CheckType_ si (up 1 t) $ EBind2_ si BMeta tt te') eet +-- | CheckIType x te' <- te -> refocus (CheckType_ si (up 1 t) $ EBind2_ si BMeta tt te') eet + | ELabelEnd te' <- te -> refocus (ELabelEnd $ EBind2_ si BMeta tt te') eet + | otherwise -> focus2 te $ Meta tt eet + where + refocus = refocus_ focus2 + cst :: ExpType -> Exp -> Maybe (TCM m ExpType') + cst x = \case + Var i | fst (varType "X" i te) == BMeta + , Just y <- down i x + -> Just $ join swapAssign (\i x -> refocus $ EAssign i x te) i y $ subst 0 {-ReflCstr y-}TT $ subst (i+1) (fst $ up 1 y) eet + _ -> Nothing + + EAssign i b te -> case te of + EBind2_ si h x te' | i > 0, Just b' <- down 0 b + -> refocus' (EBind2_ si h (subst (i-1) (fst b') x) (EAssign (i-1) b' te')) eet + ELet2 le (x, xt) te' | i > 0, Just b' <- down 0 b + -> refocus' (ELet2 le (subst (i-1) (fst b') x, subst (i-1) (fst b') xt) (EAssign (i-1) b' te')) eet + ELet1 le te' x -> refocus' (ELet1 le (EAssign i b te') $ substS (i+1) (up 1 b) x) eet + EBind1 si h te' x -> refocus' (EBind1 si h (EAssign i b te') $ substS (i+1) (up 1 b) x) eet + CheckAppType si h t te' x -> refocus' (CheckAppType si h (subst i (fst b) t) (EAssign i b te') $ substS i b x) eet + EApp1 si h te' x -> refocus' (EApp1 si h (EAssign i b te') $ substS i b x) eet + EApp2 si h x te' -> refocus' (EApp2 si h (subst i (fst b) x) $ EAssign i b te') eet + CheckType_ si t te' -> refocus' (CheckType_ si (subst i (fst b) t) $ EAssign i b te') eet + ELabelEnd te' -> refocus' (ELabelEnd $ EAssign i b te') eet + EAssign j a te' | i < j + -> refocus' (EAssign (j-1) (subst i (fst b) a) $ EAssign i (up1_ (j-1) b) te') eet + t | Just te' <- pull i te -> refocus' te' eet + | otherwise -> swapAssign (\i x -> focus2 te . Assign i x) (\i x -> refocus' $ EAssign i x te) i b eet + -- todo: CheckSame Exp Env + where + refocus' = fix refocus_ + pull i = \case + EBind2 BMeta _ te | i == 0 -> Just te + EBind2_ si h x te -> EBind2_ si h <$> down (i-1) x <*> pull (i-1) te + EAssign j b te -> EAssign (if j <= i then j else j-1) <$> down i b <*> pull (if j <= i then i+1 else i) te + _ -> Nothing + + EGlobal{} -> return eet + _ -> case eet of + MEnd x -> throwError_ $ "focus todo: " ++ ppShow x + _ -> throwError_ $ "focus checkMetas: " ++ ppShow env ++ "\n" ++ ppShow (fst <$> eet) + where + refocus_ :: (Env -> CEnv ExpType -> TCM m ExpType') -> Env -> CEnv ExpType -> TCM m ExpType' + refocus_ _ e (MEnd at) = focus_ e at + refocus_ f e (Meta x at) = f (EBind2 BMeta x e) at + refocus_ _ e (Assign i x at) = focus2 (EAssign i x e) at + + replaceMetas' = replaceMetas $ lamPi Hidden + +lamPi h = (***) <$> (\a b -> Lam b) <*> Pi h + +replaceMetas bind = \case + Meta a t -> bind a $ replaceMetas bind t + Assign i x t | x' <- up1_ i x -> bind (cstrT'' (snd x') (Var i) $ fst x') . up 1 . up1_ i $ replaceMetas bind t + MEnd t -> t + + +isCstr CstrT{} = True +isCstr (UL (FunN s _)) = s `elem` ["'Eq", "'Ord", "'Num", "'CNum", "'Signed", "'Component", "'Integral", "'NumComponent", "'Floating"] -- todo: use Constraint type to decide this +isCstr (UL c) = {- trace_ (ppShow c ++ show c) $ -} False + +-------------------------------------------------------------------------------- re-checking + +type Message = String + +recheck :: Message -> Env -> ExpType -> ExpType +recheck msg e = recheck' msg e + +-- todo: check type also +recheck' :: Message -> Env -> ExpType -> ExpType +recheck' msg' e (x, xt) = (recheck_ "main" (checkEnv e) (x, xt), xt) + where + checkEnv = \case + e@EGlobal{} -> e + EBind1 si h e b -> EBind1 si h (checkEnv e) b + EBind2_ si h t e -> EBind2_ si h (checkType e t) $ checkEnv e -- E [\(x :: t) -> e] -> check E [t] + ELet1 le e b -> ELet1 le (checkEnv e) b + ELet2 le x e -> ELet2 le (recheck'' "env" e x) $ checkEnv e + EApp1 si h e b -> EApp1 si h (checkEnv e) b + EApp2 si h a e -> EApp2 si h (recheck'' "env" e a) $ checkEnv e -- E [a x] -> check + EAssign i x e -> EAssign i (recheck'' "env" e $ up1_ i x) $ checkEnv e -- __ + CheckType_ si x e -> CheckType_ si (checkType e x) $ checkEnv e +-- CheckSame x e -> CheckSame (recheck'' "env" e x) $ checkEnv e + CheckAppType si h x e y -> CheckAppType si h (checkType e x) (checkEnv e) y + + recheck'' msg te a@(x, xt) = (recheck_ msg te a, xt) + checkType te e = recheck_ "check" te (e, TType) + + recheck_ msg te = \case + (Var k, zt) -> Var k -- todo: check var type + (Lam b, Pi h a bt) -> Lam $ recheck_ "9" (EBind2 (BLam h) a te) (b, bt) + (Pi h a b, TType) -> Pi h (checkType te a) $ checkType (EBind2 (BPi h) a te) b + (ELit l, zt) -> ELit l -- todo: check literal type + (TType, TType) -> TType + (Neut (App_ a b), zt) + | (Neut a', at) <- recheck'' "app1" te (Neut a, neutType te a) + -> checkApps [] zt (Neut . App_ a' . head) te at [b] + (Con s n as, zt) -> checkApps [] zt (Con s n . drop (conParams s)) te (nType s) $ mkConPars n zt ++ as + (TyCon s as, zt) -> checkApps [] zt (TyCon s) te (nType s) as + (Fun s as, zt) -> checkApps [] zt (Fun s) te (nType s) as + (CaseFun s@(CaseFunName _ t pars) as n, zt) -> checkApps [] zt (\xs -> evalCaseFun s (init $ drop pars xs) (last xs)) te (nType s) (makeCaseFunPars te n ++ as ++ [Neut n]) + (TyCaseFun s [m, t, f] n, zt) -> checkApps [] zt (\[m, t, n, f] -> evalTyCaseFun s [m, t, f] n) te (nType s) [m, t, Neut n, f] + (Label lk a x, zt) -> Label lk (recheck_ msg te (a, zt)) x + (PMLabel f i a x, zt) -> checkApps [] zt (\xs -> PMLabel f i xs x) te (nType f) a + (LabelEnd_ k x, zt) -> LabelEnd_ k $ recheck_ msg te (x, zt) + where + checkApps acc zt f _ t [] | t == zt = f $ reverse acc + checkApps acc zt f te t@(Pi h x y) (b_: xs) = checkApps (b: acc) zt f te (appTy t b) xs where b = recheck_ "checkApps" te (b_, x) + checkApps acc zt f te t _ = error_ $ "checkApps " ++ msg ++ "\n" ++ showEnvExp te{-todo-} (t, TType) ++ "\n\n" ++ showEnvExp e (x, xt) + + getNeut (Neut a) = a + +-- Ambiguous: (Int ~ F a) => Int +-- Not ambiguous: (Show a, a ~ F b) => b +ambiguityCheck :: String -> Exp -> Maybe String +ambiguityCheck s ty = case ambigVars ty of + [] -> Nothing + err -> Just $ s ++ " has ambiguous type:\n" ++ ppShow ty ++ "\nproblematic vars:\n" ++ show err + +ambigVars :: Exp -> [(Int, Exp)] +ambigVars ty = [(n, c) | (n, c) <- hid, not $ any (`Set.member` defined) $ Set.insert n $ free c] + where + (defined, hid, i) = compDefined False ty + +floatLetMeta :: Exp -> Bool +floatLetMeta ty = (i-1) `Set.member` defined + where + (defined, hid, i) = compDefined True ty + +compDefined b ty = (defined, hid, i) + where + defined = dependentVars hid $ Set.map (if b then (+i) else id) $ free ty + + i = length hid_ + hid = zipWith (\k t -> (k, up (k+1) t)) (reverse [0..i-1]) hid_ + (hid_, ty') = hiddenVars ty + +hiddenVars (Pi Hidden a b) = first (a:) $ hiddenVars b +hiddenVars t = ([], t) + +-- compute dependent type vars in constraints +-- Example: dependentVars [(a, b) ~ F b c, d ~ F e] [c] == [a,b,c] +dependentVars :: [(Int, Exp)] -> Set.Set Int -> Set.Set Int +dependentVars ie = cycle mempty + where + freeVars = free + + cycle acc s + | Set.null s = acc + | otherwise = cycle (acc <> s) (grow s Set.\\ acc) + + grow = flip foldMap ie $ \case + (n, t) -> (Set.singleton n <-> freeVars t) <> case t of + CstrT _{-todo-} ty f -> freeVars ty <-> freeVars f + CSplit a b c -> freeVars a <-> (freeVars b <> freeVars c) + _ -> mempty + where + a --> b = \s -> if Set.null $ a `Set.intersection` s then mempty else b + a <-> b = (a --> b) <> (b --> a) + + +-------------------------------------------------------------------------------- global env + +type GlobalEnv = Map.Map SName (Exp, Type, SI) + +-- monad used during elaborating statments -- TODO: use zippers instead +type ElabStmtM m = ReaderT (Extensions, String{-full source-}) (StateT GlobalEnv (ExceptT String (WriterT Infos m))) + +extractEnv :: Env -> (String, GlobalEnv) +extractEnv = either id extractEnv . parent + +initEnv :: GlobalEnv +initEnv = Map.fromList + [ (,) "'Type" (TType, TType, debugSI "source-of-Type") + ] + +extractDesugarInfo :: GlobalEnv -> DesugarInfo +extractDesugarInfo ge = + ( Map.fromList + [ (n, f) | (n, (d, _, si)) <- Map.toList ge, f <- maybeToList $ case UL' d of + Con (ConName _ f _ _ _) 0 [] -> f + TyCon (TyConName _ f _ _ _ _) [] -> f + (getLams -> UL (getLams -> Fun (FunName _ f _) _)) -> f + Fun (FunName _ f _) [] -> f + _ -> Nothing + ] + , Map.fromList $ + [ (n, Left ((t, inum), map f cons)) + | (n, (UL' (Con cn 0 []), _, si)) <- Map.toList ge, let TyConName t _ inum _ cons _ = conTypeName cn + ] ++ + [ (n, Right $ pars t) + | (n, (UL' (TyCon (TyConName _ _ _ t _ _) []), _, _)) <- Map.toList ge + ] + ) + where + f (ConName n _ _ _ ct) = (n, pars ct) + pars = length . filter ((==Visible) . fst) . fst . getParams + +-------------------------------------------------------------------------------- infos + +newtype Infos = Infos (Map.Map Range (Set.Set String)) + deriving (NFData) + +instance Monoid Infos where + mempty = Infos mempty + Infos x `mappend` Infos y = Infos $ Map.unionWith mappend x y + +mkInfoItem (RangeSI r) i = Infos $ Map.singleton r $ Set.singleton i +mkInfoItem _ _ = mempty + +listInfos (Infos m) = [(r, Set.toList i) | (r, i) <- Map.toList m] + +-------------------------------------------------------------------------------- inference for statements + +handleStmt :: MonadFix m => [Stmt] -> Stmt -> ElabStmtM m () +handleStmt defs = \case + Primitive n mf (trSExp' -> t_) -> do + t <- inferType tr =<< ($ t_) <$> addF + tellStmtType (fst n) t + addToEnv n $ flip (,) t $ lamify t $ Fun (FunName (snd n) mf t) + Let n mf mt ar t_ -> do + af <- addF + let t__ = maybe id (flip SAnn . af) mt t_ + (x, t) <- inferTerm (snd n) tr id $ trSExp' $ if usedS n t__ then SBuiltin "primFix" `SAppV` SLamV (substSG0 n t__) else t__ + tellStmtType (fst n) t + addToEnv n (mkELet (True, n, SData mf, ar) x t, t) + PrecDef{} -> return () + Data s (map (second trSExp') -> ps) (trSExp' -> t_) addfa (map (second trSExp') -> cs) -> do + exs <- asks fst + af <- if addfa then gets $ addForalls exs . (snd s:) . defined' else return id + vty <- inferType tr $ addParamsS ps t_ + tellStmtType (fst s) vty + let + pnum' = length $ filter ((== Visible) . fst) ps + inum = arity vty - length ps + + mkConstr j (cn, af -> ct) + | c == SGlobal s && take pnum' xs == downToS (length . fst . getParamsS $ ct) pnum' + = do + cty <- removeHiddenUnit <$> inferType tr (addParamsS [(Hidden, x) | (Visible, x) <- ps] ct) + tellStmtType (fst cn) cty + let pars = zipWith (\x -> second $ STyped (debugSI "mkConstr1") . flip (,) TType . up_ (1+j) x) [0..] $ drop (length ps) $ fst $ getParams cty + act = length . fst . getParams $ cty + acts = map fst . fst . getParams $ cty + conn = conName (snd cn) (listToMaybe [f | PrecDef n f <- defs, n == cn]) j cty + addToEnv cn (Con conn 0 [], cty) + return ( conn + , addParamsS pars + $ foldl SAppV (SVar (debugSI "22", ".cs") $ j + length pars) $ drop pnum' xs ++ [apps' (SGlobal cn) (zip acts $ downToS (j+1+length pars) (length ps) ++ downToS 0 (act- length ps))] + ) + | otherwise = throwError "illegal data definition (parameters are not uniform)" -- ++ show (c, cn, take pnum' xs, act) + where + (c, map snd -> xs) = getApps $ snd $ getParamsS ct + + motive = addParamsS (replicate inum (Visible, Wildcard SType)) $ + SPi Visible (apps' (SGlobal s) $ zip (map fst ps) (downToS inum $ length ps) ++ zip (map fst $ fst $ getParamsS t_) (downToS 0 inum)) SType + + mdo + let tcn = TyConName (snd s) Nothing inum vty (map fst cons) cfn + let cfn = CaseFunName (snd s) ct $ length ps + addToEnv s (TyCon tcn [], vty) + cons <- zipWithM mkConstr [0..] cs + ct <- inferType tr + ( (\x -> traceD ("type of case-elim before elaboration: " ++ ppShow x) x) $ addParamsS + ( [(Hidden, x) | (_, x) <- ps] + ++ (Visible, motive) + : map ((,) Visible . snd) cons + ++ replicate inum (Hidden, Wildcard SType) + ++ [(Visible, apps' (SGlobal s) $ zip (map fst ps) (downToS (inum + length cs + 1) $ length ps) ++ zip (map fst $ fst $ getParamsS t_) (downToS 0 inum))] + ) + $ foldl SAppV (SVar (debugSI "23", ".ct") $ length cs + inum + 1) $ downToS 1 inum ++ [SVar (debugSI "24", ".24") 0] + ) + addToEnv (fst s, caseName (snd s)) (lamify ct $ \xs -> evalCaseFun cfn (init $ drop (length ps) xs) (last xs), ct) + let ps' = fst $ getParams vty + t = (TType :~> TType) + :~> addParams ps' (Var (length ps') `app_` TyCon tcn (downTo 0 $ length ps')) + :~> TType + :~> Var 2 `app_` Var 0 + :~> Var 3 `app_` Var 1 + addToEnv (fst s, MatchName (snd s)) (lamify t $ \[m, tr, n, f] -> evalTyCaseFun (TyCaseFunName (snd s) t) [m, tr, f] n, t) + + stmt -> error $ "handleStmt: " ++ show stmt + +mkELet (False, n, mf, ar) x xt = x +mkELet (True, n, SData mf, ar) x t{-type of x-} = term + where + term = pmLabel (FunName (snd n) mf t) (addLams'' ar t) [] $ par ar t x 0 + + addLams'' [] _ = 0 + addLams'' (h: ar) (Pi h' d t) | h == h' = 1 + addLams'' ar t + addLams'' ar@(Visible: _) (Pi h@Hidden d t) = 1 + addLams'' ar t + + addLams' [] _ i = Fun (FunName (snd n) mf t) $ downTo 0 i + addLams' (h: ar) (Pi h' d t) i | h == h' = Lam $ addLams' ar t (i+1) + addLams' ar@(Visible: _) (Pi h@Hidden d t) i = Lam $ addLams' ar t (i+1) + + par ar tt (FunN "primFix" [_, f]) i = f `app_` label LabelFix (addLams' ar tt i) (foldl app_ term $ downTo 0 i) + par ar (Pi Hidden k tt) (Lam z) i = Lam $ par (dropHidden ar) tt z (i+1) + where + dropHidden (Hidden: ar) = ar + dropHidden ar = ar + par ar t x _ = x + +removeHiddenUnit (Pi Hidden Unit (down 0 -> Just t)) = removeHiddenUnit t +removeHiddenUnit (Pi h a b) = Pi h a $ removeHiddenUnit b +removeHiddenUnit t = t + +addParams ps t = foldr (uncurry Pi) t ps + +addLams ps t = foldr (uncurry $ \h a b -> Lam b) t ps + +lamify t x = addLams (fst $ getParams t) $ x $ downTo 0 $ arity t + +{- +getApps' = second reverse . run where + run (App a b) = second (b:) $ run a + run x = (x, []) +-} +arity :: Exp -> Int +arity = length . fst . getParams + +getParams :: Exp -> ([(Visibility, Exp)], Exp) +getParams (UL' (Pi h a b)) = first ((h, a):) $ getParams b +getParams x = ([], x) + +getLams (Lam b) = getLams b +getLams x = x + +getGEnv f = do + (exs, src) <- ask + gets (\ge -> EGlobal src ge mempty) >>= f +inferTerm msg tr f t = asks fst >>= \exs -> getGEnv $ \env -> let env' = f env in smartTrace exs $ \tr -> + fmap (recheck msg env' . replaceMetas (lamPi Hidden)) $ lift (lift $ inferN (if tr then traceLevel exs else 0) env' t) +inferType tr t = asks fst >>= \exs -> getGEnv $ \env -> fmap (fst . recheck "inferType" env . flip (,) TType . replaceMetas (Pi Hidden) . fmap fst) $ lift (lift $ inferN (if tr then traceLevel exs else 0) (CheckType_ (debugSI "inferType CheckType_") TType env) t) + +addToEnv :: Monad m => SIName -> (Exp, Exp) -> ElabStmtM m () +addToEnv (si, s) (x, t) = do +-- maybe (pure ()) throwError_ $ ambiguityCheck s t -- TODO + exs <- asks fst + when (trLight exs) $ mtrace (s ++ " :: " ++ ppShow t) + v <- gets $ Map.lookup s + case v of + Nothing -> modify $ Map.insert s (closedExp x, closedExp t, si) + Just (_, _, si') + | sameSource si si' -> getGEnv $ \ge -> throwError $ "already defined " ++ s ++ " at " ++ showSI ge si ++ "\n and at " ++ showSI ge si' + | otherwise -> getGEnv $ \ge -> throwError $ "already defined " ++ s ++ " at " ++ showSI ge si ++ "\n and at " ++ showSourcePosSI si' + +downTo n m = map Var [n+m-1, n+m-2..n] + +defined' = Map.keys + +addF = asks fst >>= \exs -> gets $ addForalls exs . defined' + +tellType te si t = tell $ mkInfoItem (sourceInfo si) $ removeEscs $ showDoc $ mkDoc True (t, TType) +tellStmtType si t = getGEnv $ \te -> tellType te si t + + +-------------------------------------------------------------------------------- inference output + +data PolyEnv = PolyEnv + { getPolyEnv :: GlobalEnv + , infos :: Infos + } + +filterPolyEnv p pe = pe { getPolyEnv = Map.filterWithKey (\k _ -> p k) $ getPolyEnv pe } + +joinPolyEnvs :: MonadError ErrorMsg m => Bool -> [PolyEnv] -> m PolyEnv +joinPolyEnvs _ = return . foldr mappend' mempty' -- todo + where + mempty' = PolyEnv mempty mempty + PolyEnv a b `mappend'` PolyEnv a' b' = PolyEnv (a `mappend` a') (b `mappend` b') + +-------------------------------------------------------------------------------- pretty print +-- todo: do this via conversion to SExp + +instance PShow Exp where + pShowPrec _ = showDoc_ . mkDoc False + +instance PShow (CEnv Exp) where + pShowPrec _ = showDoc_ . mkDoc False + +instance PShow Env where + pShowPrec _ e = showDoc_ $ envDoc e $ pure $ shAtom $ underlined "<>" + +showEnvExp :: Env -> ExpType -> String +showEnvExp e c = showDoc $ envDoc e $ epar <$> mkDoc False c + +showEnvSExp :: Up a => Env -> SExp' a -> String +showEnvSExp e c = showDoc $ envDoc e $ epar <$> sExpDoc c + +showEnvSExpType :: Up a => Env -> SExp' a -> Exp -> String +showEnvSExpType e c t = showDoc $ envDoc e $ epar <$> (shAnn "::" False <$> sExpDoc c <**> mkDoc False (t, TType)) + where + infixl 4 <**> + (<**>) :: NameDB (a -> b) -> NameDB a -> NameDB b + a <**> b = get >>= \s -> lift $ evalStateT a s <*> evalStateT b s + +{- +expToSExp :: Exp -> SExp +expToSExp = \case + PMLabel x _ -> expToSExp x + FixLabel _ x -> expToSExp x +-- Var k -> shAtom <$> shVar k + App a b -> SApp Visible{-todo-} (expToSExp a) (expToSExp b) +{- + Lam h a b -> join $ shLam (used 0 b) (BLam h) <$> f a <*> pure (f b) + Bind h a b -> join $ shLam (used 0 b) h <$> f a <*> pure (f b) + Cstr a b -> shCstr <$> f a <*> f b + MT s xs -> foldl (shApp Visible) (shAtom s) <$> mapM f xs + CaseFun s xs -> foldl (shApp Visible) (shAtom $ show s) <$> mapM f xs + TyCaseFun s xs -> foldl (shApp Visible) (shAtom $ show s) <$> mapM f xs + ConN s xs -> foldl (shApp Visible) (shAtom s) <$> mapM f xs + TyConN s xs -> foldl (shApp Visible) (shAtom s) <$> mapM f xs +-- TType -> pure $ shAtom "Type" + ELit l -> pure $ shAtom $ show l + Assign i x e -> shLet i (f x) (f e) + LabelEnd x -> shApp Visible (shAtom "labend") <$> f x +-} +nameSExp :: SExp -> NameDB SExp +nameSExp = \case + SGlobal s -> pure $ SGlobal s + SApp h a b -> SApp h <$> nameSExp a <*> nameSExp b + SBind h a b -> newName >>= \n -> SBind h <$> nameSExp a <*> local (n:) (nameSExp b) + SLet a b -> newName >>= \n -> SLet <$> nameSExp a <*> local (n:) (nameSExp b) + STyped_ x (e, _) -> nameSExp $ expToSExp e -- todo: mark boundary + SVar i -> SGlobal <$> shVar i +-} +envDoc :: Env -> Doc -> Doc +envDoc x m = case x of + EGlobal{} -> m + EBind1 _ h ts b -> envDoc ts $ join $ shLam (used 0 b) h <$> m <*> pure (sExpDoc b) + EBind2 h a ts -> envDoc ts $ join $ shLam True h <$> mkDoc ts' (a, TType) <*> pure m + EApp1 _ h ts b -> envDoc ts $ shApp h <$> m <*> sExpDoc b + EApp2 _ h (Lam (Var 0), Pi Visible TType _) ts -> envDoc ts $ shApp h (shAtom "tyType") <$> m + EApp2 _ h a ts -> envDoc ts $ shApp h <$> mkDoc ts' a <*> m + ELet1 _ ts b -> envDoc ts $ shLet_ m (sExpDoc b) + ELet2 _ x ts -> envDoc ts $ shLet_ (mkDoc ts' x) m + EAssign i x ts -> envDoc ts $ shLet i (mkDoc ts' x) m + CheckType t ts -> envDoc ts $ shAnn ":" False <$> m <*> mkDoc ts' (t, TType) +-- CheckSame t ts -> envDoc ts $ shCstr <$> m <*> mkDoc ts' t + CheckAppType si h t te b -> envDoc (EApp1 si h (CheckType_ (sourceInfo b) t te) b) m + ELabelEnd ts -> envDoc ts $ shApp Visible (shAtom "labEnd") <$> m + where + ts' = False + +class MkDoc a where + mkDoc :: Bool -> a -> Doc + +instance MkDoc ExpType where + mkDoc ts e = mkDoc ts $ fst e + +instance MkDoc Exp where + mkDoc ts e = fmap inGreen <$> f e + where + f = \case + FixLabel _ x -> f x + Neut x -> mkDoc ts x +-- Lam h a b -> join $ shLam (used 0 b) (BLam h) <$> f a <*> pure (f b) + Lam b -> join $ shLam True (BLam Visible) <$> f TType{-todo-} <*> pure (f b) + Pi h a b -> join $ shLam (used 0 b) (BPi h) <$> f a <*> pure (f b) + ENat n -> pure $ shAtom $ show n + Con s _ xs -> foldl (shApp Visible) (shAtom_ $ show s) <$> mapM f xs + TyConN s xs -> foldl (shApp Visible) (shAtom_ s) <$> mapM f xs + TType -> pure $ shAtom "Type" + ELit l -> pure $ shAtom $ show l + LabelEnd_ k x -> shApp Visible (shAtom $ "labend" ++ show k) <$> f x + + shAtom_ = shAtom . if ts then switchTick else id + +instance MkDoc Neutral where + mkDoc ts e = fmap inGreen <$> f e + where + g = mkDoc ts + f = \case + PMLabel_ s i xs _ -> foldl (shApp Visible) (shAtom_ $ show s) <$> mapM g xs + Var_ k -> shAtom <$> shVar k + App_ a b -> shApp Visible <$> g a <*> g b + CstrT' TType a b -> shCstr <$> g a <*> g b + Fun_ s xs -> foldl (shApp Visible) (shAtom_ $ show s) <$> mapM g xs + CaseFun_ s xs n -> foldl (shApp Visible) (shAtom_ $ show s) <$> mapM g (xs ++ [Neut n]) + TyCaseFun_ s [m, t, f] n -> foldl (shApp Visible) (shAtom_ $ show s) <$> mapM g [m, t, Neut n, f] + + shAtom_ = shAtom . if ts then switchTick else id + +instance MkDoc (CEnv Exp) where + mkDoc ts e = fmap inGreen <$> f e + where + f :: CEnv Exp -> Doc + f = \case + MEnd a -> mkDoc ts a + Meta a b -> join $ shLam True BMeta <$> mkDoc ts a <*> pure (f b) + Assign i (x, _) e -> shLet i (mkDoc ts x) (f e) + +-------------------------------------------------------------------------------- main + +smartTrace :: MonadError String m => Extensions -> (Bool -> m a) -> m a +smartTrace exs f | traceLevel exs >= 2 = f True +smartTrace exs f | traceLevel exs == 0 = f False +smartTrace exs f = catchError (f False) $ \err -> + trace_ (unlines + [ "---------------------------------" + , err + , "try again with trace" + , "---------------------------------" + ]) $ f True + +type TraceLevel = Int +traceLevel exs = if TraceTypeCheck `elem` exs then 1 else 0 :: TraceLevel -- 0: no trace +tr = False --traceLevel >= 2 +trLight exs = traceLevel exs >= 1 + +inference_ :: PolyEnv -> Module -> ErrorT (WriterT Infos Identity) PolyEnv +inference_ (PolyEnv pe is) m = ff $ runWriter $ runExceptT $ mdo + let (x, dns) = definitions m ds + ds = mkDesugarInfo defs `joinDesugarInfo` extractDesugarInfo pe + defs <- either (throwError . ErrorMsg) return x + mapM_ (maybe (return ()) (throwErrorTCM . text)) dns + mapExceptT (fmap $ ErrorMsg +++ snd) . flip runStateT (initEnv <> pe) . flip runReaderT (extensions m, sourceCode m) . mapM_ (handleStmt defs) $ sortDefs ds defs + where + ff (Left e, is) = throwError e + ff (Right ge, is) = do + tell is + return $ PolyEnv ge is + + diff --git a/src/LambdaCube/Compiler/Lexer.hs b/src/LambdaCube/Compiler/Lexer.hs new file mode 100644 --- /dev/null +++ b/src/LambdaCube/Compiler/Lexer.hs @@ -0,0 +1,614 @@ +-- contains modified Haskell source code copied from Text.Parsec.Token, see below +{-# LANGUAGE LambdaCase #-} +{-# LANGUAGE ViewPatterns #-} +{-# LANGUAGE PatternSynonyms #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE NoMonomorphismRestriction #-} +{-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# OPTIONS_GHC -fno-warn-orphans #-} -- instance NFData SourcePos +{-# OPTIONS -fno-warn-unused-do-bind -fno-warn-name-shadowing #-} +module LambdaCube.Compiler.Lexer + ( module LambdaCube.Compiler.Lexer + , module Pr + ) where + +import Data.Monoid +import Data.Maybe +import Data.List +import Data.Char +import qualified Data.Set as Set +import qualified Data.Map as Map + +import Control.Monad.Except +import Control.Monad.Reader +import Control.Monad.Writer +import Control.Arrow hiding ((<+>)) +import Control.Applicative +import Control.DeepSeq + +import LambdaCube.Compiler.Pretty hiding (Doc, braces, parens) + +--------------------- parsec specific code begins here +import Text.Parsec hiding ((<|>), many) +import Text.Parsec as Pr hiding (label, Empty, State, (<|>), many, try) +import qualified Text.Parsec as Pa +import Text.Parsec.Indentation as Pa +import Text.Parsec.Indentation.Char +import Text.Parsec.Pos + +skipSome = skipMany1 + +type P = ParsecT (IndentStream (CharIndentStream String)) SourcePos InnerP + +indent s p = reserved s *> localIndentation Ge (localAbsoluteIndentation p) +indented = localIndentation Gt +indentMany s p = indent s $ many p +indentSome s p = indent s $ some p +indentMany' = many + +whiteSpace = ignoreAbsoluteIndentation (localTokenMode (const Pa.Any) whiteSpace') + +lexeme p + = p <* (getPosition >>= setState >> whiteSpace) + +mkStream = mkIndentStream 0 infIndentation True Ge . mkCharIndentStream + +runPT' p st --u name s + = do res <- runParsecT p st -- (Pa.State s (initialPos name) u) + r <- parserReply res + case r of + Ok x _ _ -> return (Right x) + Error err -> return (Left err) + where + parserReply res + = case res of + Consumed r -> r + Pa.Empty r -> r + +runParserT'' p f = runParserT p (initialPos f) f +--------------------- parsec specific code ends here +{- +--------------------- megaparsec specific code begins here +import Control.Monad.State +import Text.Megaparsec +import Text.Megaparsec.Lexer hiding (lexeme, symbol, space, negate) +import Text.Megaparsec as Pr hiding (try, label, Message) +import Text.Megaparsec.Pos + +optionMaybe = optional +runParserT'' p f = flip evalStateT (initialPos f, 0) . runParserT p f + +runPT' p st = snd <$> flip evalStateT (initialPos ".....", 0) (runParserT' p st) +mkStream = id +hexDigit = hexDigitChar +octDigit = octDigitChar +digit = digitChar +getState = fst <$> get + +type P = ParsecT String (StateT (SourcePos, Int) InnerP) + +indentMany' p = --many p-- + indentBlock whiteSpace' $ whiteSpace' >> return (IndentMany Nothing return p) +indentMany s p = indentBlock whiteSpace' $ try (reserved s) *> return (IndentMany Nothing return p) +indentSome s p = indentBlock whiteSpace' $ try (reserved s) *> return (IndentSome Nothing return p) +indented p = do + i <- indentLevel + modify $ second $ const i + --p <* indentGuard whiteSpace' (>= i) + p + +lexeme p = do + i <- indentLevel + i' <- snd <$> get +-- when (i < i') $ fail "indent level" + p <* (getPosition >>= \p -> modify (first $ const p) >> whiteSpace) + +whiteSpace = whiteSpace' +--------------------- megaparsec specific code ends here +-} +-------------------------------------------------------------------------------- parser utils + +-- see http://blog.ezyang.com/2014/05/parsec-try-a-or-b-considered-harmful/comment-page-1/#comment-6602 +try_ s m = try m s + +manyNM a b _ | b < a || b < 0 || a < 0 = mzero +manyNM 0 0 _ = pure [] +manyNM 0 n p = option [] $ (:) <$> p <*> manyNM 0 (n-1) p +manyNM k n p = (:) <$> p <*> manyNM (k-1) (n-1) p + +-------------------------------------------------------------------------------- parser type + +type InnerP = WriterT [PostponedCheck] (Reader (DesugarInfo, Namespace)) + +type PostponedCheck = Maybe String + +type DesugarInfo = (FixityMap, ConsMap) + +type ConsMap = Map.Map SName{-constructor name-} + (Either ((SName{-type name-}, Int{-num of indices-}), [(SName, Int)]{-constructors with arities-}) + Int{-arity-}) + +dsInfo :: P DesugarInfo +dsInfo = asks fst + +namespace :: P Namespace +namespace = asks snd + + +-------------------------------------------------------------------------------- literals + +data Lit + = LInt Integer + | LChar Char + | LFloat Double + | LString String + deriving (Eq) + +instance Show Lit where + show = \case + LFloat x -> show x + LString x -> show x + LInt x -> show x + LChar x -> show x + +-------------------------------------------------------------------------------- names + +type SName = String + +caseName (c:cs) = toLower c: cs ++ "Case" + +pattern MatchName cs <- (getMatchName -> Just cs) where MatchName = matchName + +matchName cs = "match" ++ cs +getMatchName ('m':'a':'t':'c':'h':cs) = Just cs +getMatchName _ = Nothing + + +-------------------------------------------------------------------------------- source infos + +instance NFData SourcePos where + rnf x = x `seq` () + +data Range = Range SourcePos SourcePos + deriving (Eq, Ord) + +instance NFData Range where + rnf (Range a b) = rnf a `seq` rnf b `seq` () + +instance PShow Range where + pShowPrec _ (Range b e) | sourceName b == sourceName e = text (sourceName b) <+> f b <> "-" <> f e + where + f x = pShow (sourceLine x) <> ":" <> pShow (sourceColumn x) + +joinRange :: Range -> Range -> Range +joinRange (Range b e) (Range b' e') = Range (min b b') (max e e') + +data SI + = NoSI (Set.Set String) -- no source info, attached debug info + | RangeSI Range + +instance Show SI where show _ = "SI" +instance Eq SI where _ == _ = True +instance Ord SI where _ `compare` _ = EQ + +instance Monoid SI where + mempty = NoSI Set.empty + mappend (RangeSI r1) (RangeSI r2) = RangeSI (joinRange r1 r2) + mappend (NoSI ds1) (NoSI ds2) = NoSI (ds1 `Set.union` ds2) + mappend r@RangeSI{} _ = r + mappend _ r@RangeSI{} = r + +instance PShow SI where + pShowPrec _ (NoSI ds) = hsep $ map pShow $ Set.toList ds + pShowPrec _ (RangeSI r) = pShow r + +showSI_ _ (NoSI ds) = unwords $ Set.toList ds +showSI_ source (RangeSI (Range s e)) = show str + where + startLine = sourceLine s - 1 + endline = sourceLine e - if sourceColumn e == 1 then 1 else 0 + len = endline - startLine + str = vcat $ text (show s <> ":"){- <+> "-" <+> text (show e)-}: + map text (take len $ drop startLine $ lines source) + ++ [text $ replicate (sourceColumn s - 1) ' ' ++ replicate (sourceColumn e - sourceColumn s) '^' | len == 1] + +showSourcePosSI (NoSI ds) = unwords $ Set.toList ds +showSourcePosSI (RangeSI (Range s _)) = show s + +-- TODO: remove +validSI RangeSI{} = True +validSI _ = False + +debugSI a = NoSI (Set.singleton a) + +si@(RangeSI r) `validate` xs | all validSI xs && r `notElem` [r | RangeSI r <- xs] = si +_ `validate` _ = mempty + +sourceNameSI (RangeSI (Range a _)) = sourceName a + +sameSource r@(RangeSI {}) q@(RangeSI {}) = sourceNameSI r == sourceNameSI q +sameSource _ _ = True + +class SourceInfo si where + sourceInfo :: si -> SI + +instance SourceInfo SI where + sourceInfo = id + +instance SourceInfo si => SourceInfo [si] where + sourceInfo = foldMap sourceInfo + +class SetSourceInfo a where + setSI :: SI -> a -> a + +appRange :: P (SI -> a) -> P a +appRange p = (\p1 a p2 -> a $ RangeSI $ Range p1 p2) <$> getPosition <*> p <*> getState + +withRange :: (SI -> a -> b) -> P a -> P b +withRange f p = appRange $ flip f <$> p + +infix 9 `withRange` + +type SIName = (SI, SName) + +parseSIName :: P String -> P SIName +parseSIName = withRange (,) + +-------------------------------------------------------------------------------- namespace handling + +data Level = TypeLevel | ExpLevel + deriving (Eq, Show) + +data Namespace = Namespace + { namespaceLevel :: Maybe Level + , constructorNamespace :: Bool -- True means that the case of the first letter of identifiers matters + } + deriving (Show) + +tick = (\case TypeLevel -> switchTick; _ -> id) . fromMaybe ExpLevel . namespaceLevel + +tick' c = (`tick` c) <$> namespace + +switchTick ('\'': n) = n +switchTick n = '\'': n + +modifyLevel f = local $ second $ \(Namespace l p) -> Namespace (f <$> l) p + +typeNS, expNS, switchNS :: P a -> P a +typeNS = modifyLevel $ const TypeLevel +expNS = modifyLevel $ const ExpLevel +switchNS = modifyLevel $ \case ExpLevel -> TypeLevel; TypeLevel -> ExpLevel + +ifNoCNamespace p = namespace >>= \ns -> if constructorNamespace ns then mzero else p + +-------------------------------------------------------------------------------- identifiers + +lcIdentStart = satisfy $ \c -> isLower c || c == '_' +identStart = satisfy $ \c -> isLetter c || c == '_' +identLetter = satisfy $ \c -> isAlphaNum c || c == '_' || c == '\'' || c == '#' +lowercaseOpLetter = oneOf "!#$%&*+./<=>?@\\^|-~" +opLetter = oneOf ":!#$%&*+./<=>?@\\^|-~" + +maybeStartWith p i = i <|> (:) <$> satisfy p <*> i + +lowerLetter = lcIdentStart <|> ifNoCNamespace identStart +upperLetter = satisfy isUpper <|> ifNoCNamespace identStart + +upperCase, lowerCase, symbols, colonSymbols, backquotedIdent :: P SName + +upperCase = identifier (tick' =<< maybeStartWith (=='\'') ((:) <$> upperLetter <*> many identLetter)) "uppercase ident" +lowerCase = identifier ((:) <$> lowerLetter <*> many identLetter) "lowercase ident" +backquotedIdent = identifier ((:) <$ char '`' <*> identStart <*> many identLetter <* char '`') "backquoted ident" +symbols = operator (some opLetter) "symbols" +lcSymbols = operator ((:) <$> lowercaseOpLetter <*> many opLetter) "symbols" +colonSymbols = operator ((:) <$> satisfy (== ':') <*> many opLetter) "op symbols" +moduleName = identifier (intercalate "." <$> sepBy1 ((:) <$> upperLetter <*> many identLetter) (char '.')) "module name" + +patVar = f <$> lowerCase where + f "_" = "" + f x = x +lhsOperator = lcSymbols <|> backquotedIdent +rhsOperator = symbols <|> backquotedIdent +varId = lowerCase <|> parens rhsOperator +upperLower = lowerCase <|> upperCase <|> parens rhsOperator + +--qIdent = {-qualified_ todo-} (lowerCase <|> upperCase) + +-------------------------------------------------------------------------------- fixity handling + +data FixityDef = Infix | InfixL | InfixR deriving (Show) +type Fixity = (FixityDef, Int) +type MFixity = Maybe Fixity +type FixityMap = Map.Map SName Fixity + +calcPrec + :: (Show e, Show f) + => (f -> e -> e -> e) + -> (f -> Fixity) + -> e + -> [(f, e)] + -> e +calcPrec app getFixity e = compileOps [((Infix, -1000), error "calcPrec", e)] + where + compileOps [(_, _, e)] [] = e + compileOps acc [] = compileOps (shrink acc) [] + compileOps acc@((p, g, e1): ee) es_@((op, e'): es) = case compareFixity (pr, op) (p, g) of + Right GT -> compileOps ((pr, op, e'): acc) es + Right LT -> compileOps (shrink acc) es_ + Left err -> error err + where + pr = getFixity op + + shrink ((_, op, e): (pr, op', e'): es) = (pr, op', app op e' e): es + + compareFixity ((dir, i), op) ((dir', i'), op') + | i > i' = Right GT + | i < i' = Right LT + | otherwise = case (dir, dir') of + (InfixL, InfixL) -> Right LT + (InfixR, InfixR) -> Right GT + _ -> Left $ "fixity error:" ++ show (op, op') + +parseFixityDecl :: P [(SIName, Fixity)] +parseFixityDecl = do + dir <- Infix <$ reserved "infix" + <|> InfixL <$ reserved "infixl" + <|> InfixR <$ reserved "infixr" + indented $ do + LInt n <- parseLit + let i = fromIntegral n + ns <- commaSep1 (parseSIName rhsOperator) + return $ (,) <$> ns <*> pure (dir, i) + +getFixity :: DesugarInfo -> SName -> Fixity +getFixity (fm, _) n = fromMaybe (InfixL, 9) $ Map.lookup n fm + + +---------------------------------------------------------------------- +---------------------------------------------------------------------- +-- modified version of +-- +-- Module : Text.Parsec.Token +-- Copyright : (c) Daan Leijen 1999-2001, (c) Paolo Martini 2007 +-- License : BSD-style + +----------------------------------------------------------- +-- Bracketing +----------------------------------------------------------- +parens p = between (symbol "(") (symbol ")") p +braces p = between (symbol "{") (symbol "}") p +angles p = between (symbol "<") (symbol ">") p +brackets p = between (symbol "[") (symbol "]") p + +commaSep p = sepBy p $ symbol "," +commaSep1 p = sepBy1 p $ symbol "," + +----------------------------------------------------------- + +parseLit = lexeme $ charLiteral <|> stringLiteral <|> natFloat + where + ----------------------------------------------------------- + -- Chars & Strings + ----------------------------------------------------------- + charLiteral = LChar <$> between (char '\'') + (char '\'' "end of character") + characterChar + "character" + + characterChar = charLetter <|> charEscape + "literal character" + + charEscape = do{ char '\\'; escapeCode } + charLetter = satisfy (\c -> (c /= '\'') && (c /= '\\') && (c > '\026')) + + + + stringLiteral = LString <$> + do{ str <- between (char '"') + (char '"' "end of string") + (many stringChar) + ; return (foldr (maybe id (:)) "" str) + } + "literal string" + + stringChar = do{ c <- stringLetter; return (Just c) } + <|> stringEscape + "string character" + + stringLetter = satisfy (\c -> (c /= '"') && (c /= '\\') && (c > '\026')) + + stringEscape = do{ char '\\' + ; do{ escapeGap ; return Nothing } + <|> do{ escapeEmpty; return Nothing } + <|> do{ esc <- escapeCode; return (Just esc) } + } + + escapeEmpty = char '&' + escapeGap = do{ some space + ; char '\\' "end of string gap" + } + + + + -- escape codes + escapeCode = charEsc <|> charNum <|> charAscii <|> charControl + "escape code" + + charControl = do{ char '^' + ; code <- satisfy isUpper "uppercase letter" + ; return (toEnum (fromEnum code - fromEnum 'A')) + } + + charNum = do{ code <- decimal + <|> do{ char 'o'; number 8 octDigit } + <|> do{ char 'x'; number 16 hexDigit } + ; return (toEnum (fromInteger code)) + } + + charEsc = choice (map parseEsc escMap) + where + parseEsc (c,code) = do{ char c; return code } + + charAscii = choice (map parseAscii asciiMap) + where + parseAscii (asc,code) = try (do{ string asc; return code }) + + + -- escape code tables + escMap = zip ("abfnrtv\\\"\'") ("\a\b\f\n\r\t\v\\\"\'") + asciiMap = zip (ascii3codes ++ ascii2codes) (ascii3 ++ ascii2) + + ascii2codes = ["BS","HT","LF","VT","FF","CR","SO","SI","EM", + "FS","GS","RS","US","SP"] + ascii3codes = ["NUL","SOH","STX","ETX","EOT","ENQ","ACK","BEL", + "DLE","DC1","DC2","DC3","DC4","NAK","SYN","ETB", + "CAN","SUB","ESC","DEL"] + + ascii2 = ['\BS','\HT','\LF','\VT','\FF','\CR','\SO','\SI', + '\EM','\FS','\GS','\RS','\US','\SP'] + ascii3 = ['\NUL','\SOH','\STX','\ETX','\EOT','\ENQ','\ACK', + '\BEL','\DLE','\DC1','\DC2','\DC3','\DC4','\NAK', + '\SYN','\ETB','\CAN','\SUB','\ESC','\DEL'] + + + ----------------------------------------------------------- + -- Numbers + ----------------------------------------------------------- + + -- floats + natFloat = do{ char '0' + ; zeroNumFloat + } + <|> decimalFloat + + zeroNumFloat = do{ n <- hexadecimal <|> octal + ; return (LInt n) + } + <|> decimalFloat + <|> fractFloat 0 + <|> return (LInt 0) + + decimalFloat = do{ n <- decimal + ; option (LInt n) + (fractFloat n) + } + + fractFloat n = do{ f <- fractExponent n + ; return (LFloat f) + } + + fractExponent n = do{ fract <- fraction + ; expo <- option 1.0 exponent' + ; return ((fromInteger n + fract)*expo) + } + <|> + do{ expo <- exponent' + ; return ((fromInteger n)*expo) + } + + fraction = do{ char '.' + ; digits <- some digit "fraction" + ; return (foldr op 0.0 digits) + } + "fraction" + where + op d f = (f + fromIntegral (digitToInt d))/10.0 + + exponent' = do{ oneOf "eE" + ; f <- sign + ; e <- decimal "exponent" + ; return (power (f e)) + } + "exponent" + where + power e | e < 0 = 1.0/power(-e) + | otherwise = fromInteger (10^e) + + + -- integers and naturals + sign = (char '-' >> return negate) + <|> (char '+' >> return id) + <|> return id + + decimal = number 10 digit + hexadecimal = do{ oneOf "xX"; number 16 hexDigit } + octal = do{ oneOf "oO"; number 8 octDigit } + + number base baseDigit + = do{ digits <- some baseDigit + ; let n = foldl' (\x d -> base*x + toInteger (digitToInt d)) 0 digits + ; seq n (return n) + } + +----------------------------------------------------------- +-- Operators & reserved ops +----------------------------------------------------------- +reservedOp name = + lexeme $ try $ + do{ string name + ; notFollowedBy opLetter ("end of " ++ show name) + } + +operator oper = + lexeme $ try $ trCons <$> expect "reserved operator" (`Set.member` theReservedOpNames) oper + where + trCons ":" = "Cons" + trCons x = x + +theReservedOpNames = Set.fromList ["::","..","=","\\","|","<-","->","@","~","=>"] + +expect msg p i = i >>= \n -> if (p n) then unexpected (msg ++ " " ++ show n) else return n + +----------------------------------------------------------- +-- Identifiers & Reserved words +----------------------------------------------------------- +reserved name = + lexeme $ try $ + do{ string name + ; notFollowedBy identLetter ("end of " ++ show name) + } + +identifier ident = + lexeme $ try $ expect "reserved word" (`Set.member` theReservedNames) ident + +theReservedNames = Set.fromList $ + ["let","in","case","of","if","then","else" + ,"data","type" + ,"class","default","deriving","do","import" + ,"infix","infixl","infixr","instance","module" + ,"newtype","where" + ,"primitive" + -- "as","qualified","hiding" + ] ++ + ["foreign","import","export","primitive" + ,"_ccall_","_casm_" + ,"forall" + ] + +----------------------------------------------------------- +-- White space & symbols +----------------------------------------------------------- + +symbol name + = lexeme (string name) + +whiteSpace' = skipMany (simpleSpace <|> oneLineComment <|> multiLineComment "") + +simpleSpace + = skipSome (satisfy isSpace) + +oneLineComment + = try (string "--" >> many (char '-') >> notFollowedBy opLetter) + >> skipMany (satisfy (/= '\n')) + +multiLineComment = try (string "{-") *> inCommentMulti + +inCommentMulti + = try (() <$ string "-}") + <|> multiLineComment *> inCommentMulti + <|> skipSome (noneOf "{}-") *> inCommentMulti + <|> oneOf "{}-" *> inCommentMulti + "end of comment" + diff --git a/src/LambdaCube/Compiler/Parser.hs b/src/LambdaCube/Compiler/Parser.hs new file mode 100644 --- /dev/null +++ b/src/LambdaCube/Compiler/Parser.hs @@ -0,0 +1,1192 @@ +{-# LANGUAGE LambdaCase #-} +{-# LANGUAGE ViewPatterns #-} +{-# LANGUAGE PatternSynonyms #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE NoMonomorphismRestriction #-} +{-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE DeriveFunctor #-} +{-# LANGUAGE ScopedTypeVariables #-} +module LambdaCube.Compiler.Parser + ( SData(..) + , NameDB, caseName, pattern MatchName + , sourceInfo, SI(..), debugSI + , Module(..), Visibility(..), Binder(..), SExp'(..), Extension(..), Extensions + , pattern SVar, pattern SType, pattern Wildcard, pattern SAppV, pattern SLamV, pattern SAnn + , pattern SBuiltin, pattern SPi, pattern Primitive, pattern SLabelEnd, pattern SLam + , pattern TyType, pattern Wildcard_ + , debug, LI, isPi, varDB, lowerDB, MaxDB (..), iterateN, traceD, parseLC + , getParamsS, addParamsS, getApps, apps', downToS, addForalls + , mkDesugarInfo, joinDesugarInfo + , throwErrorTCM, ErrorMsg(..), ErrorT + , Up (..), up1, up + , Doc, shLam, shApp, shLet, shLet_, shAtom, shAnn, shVar, epar, showDoc, showDoc_, sExpDoc, shCstr + , mtrace, sortDefs + , trSExp', usedS, substSG0, substS + , Stmt (..), Export (..), ImportItems (..) + ) where + +import Data.Monoid +import Data.Maybe +import Data.List +import Data.Char +import Data.String +import qualified Data.Map as Map +import qualified Data.Set as Set + +import Control.Monad.Except +import Control.Monad.Reader +import Control.Monad.Writer +import Control.Monad.State +import Control.Arrow hiding ((<+>)) +import Control.Applicative + +import qualified LambdaCube.Compiler.Pretty as P +import LambdaCube.Compiler.Pretty hiding (Doc, braces, parens) +import LambdaCube.Compiler.Lexer + +-------------------------------------------------------------------------------- utils + +(<&>) = flip (<$>) + +dropNth i xs = take i xs ++ drop (i+1) xs +iterateN n f e = iterate f e !! n +mtrace s = trace_ s $ return () + +-- supplementary data: data with no semantic relevance +newtype SData a = SData a +instance Show (SData a) where show _ = "SData" +instance Eq (SData a) where _ == _ = True +instance Ord (SData a) where _ `compare` _ = EQ + +newtype ErrorMsg = ErrorMsg String +instance Show ErrorMsg where show (ErrorMsg s) = s + +type ErrorT = ExceptT ErrorMsg + +throwErrorTCM :: MonadError ErrorMsg m => P.Doc -> m a +throwErrorTCM d = throwError $ ErrorMsg $ show d + +traceD x = if debug then trace_ x else id + +debug = False--True--tr + +try = try_ + +-------------------------------------------------------------------------------- builtin precedences + +data Prec + = PrecAtom -- ( _ ) ... + | PrecAtom' + | PrecProj -- _ ._ {left} + | PrecSwiz -- _%_ {left} + | PrecApp -- _ _ {left} + | PrecOp + | PrecArr -- _ -> _ {right} + | PrecEq -- _ ~ _ + | PrecAnn -- _ :: _ {right} + | PrecLet -- _ := _ + | PrecLam -- \ _ -> _ {right} {accum} + deriving (Eq, Ord) + +-------------------------------------------------------------------------------- expression representation + +type SExp = SExp' Void + +data Void + +instance Show Void where show _ = error "show @Void" +instance Eq Void where _ == _ = error "(==) @Void" + +data SExp' a + = SGlobal SIName + | SBind SI Binder (SData SIName{-parameter's name-}) (SExp' a) (SExp' a) + | SApp SI Visibility (SExp' a) (SExp' a) + | SLet LI (SExp' a) (SExp' a) -- let x = e in f --> SLet e f{-x is Var 0-} + | SVar_ (SData SIName) !Int + | SLit SI Lit + | STyped SI a + deriving (Eq, Show) + +-- let info +type LI = (Bool, SIName, SData (Maybe Fixity), [Visibility]) + +pattern SVar a b = SVar_ (SData a) b + +data Binder + = BPi Visibility + | BLam Visibility + | BMeta -- a metavariable is like a floating hidden lambda + deriving (Eq, Show) + +data Visibility = Hidden | Visible + deriving (Eq, Show) + +sLit = SLit mempty +pattern SPi h a b <- SBind _ (BPi h) _ a b where SPi h a b = sBind (BPi h) (SData (debugSI "patternSPi2", "pattern_spi_name")) a b +pattern SLam h a b <- SBind _ (BLam h) _ a b where SLam h a b = sBind (BLam h) (SData (debugSI "patternSLam2", "pattern_slam_name")) a b +pattern Wildcard t <- SBind _ BMeta _ t (SVar _ 0) where Wildcard t = sBind BMeta (SData (debugSI "pattern Wildcard2", "pattern_wildcard_name")) t (SVar (debugSI "pattern Wildcard2", ".wc") 0) +pattern Wildcard_ si t <- SBind _ BMeta _ t (SVar (si, _) 0) +pattern SLamV a = SLam Visible (Wildcard SType) a + +pattern SApp' h a b <- SApp _ h a b where SApp' h a b = sApp h a b +pattern SAppH a b = SApp' Hidden a b +pattern SAppV a b = SApp' Visible a b +pattern SAppV2 f a b = f `SAppV` a `SAppV` b + +pattern SType = SBuiltin "'Type" +pattern SAnn a t = SBuiltin "typeAnn" `SAppH` t `SAppV` a +pattern TyType a = SAnn a SType +pattern SLabelEnd a = SBuiltin "labelend" `SAppV` a + +pattern SBuiltin s <- SGlobal (_, s) where SBuiltin s = SGlobal (debugSI $ "builtin " ++ s, s) + +pattern Section e = SBuiltin "^section" `SAppV` e + +sApp v a b = SApp (sourceInfo a <> sourceInfo b) v a b +sBind v x a b = SBind (sourceInfo a <> sourceInfo b) v x a b + +isPi (BPi _) = True +isPi _ = False + +infixl 2 `SAppV`, `SAppH` + +addParamsS ps t = foldr (uncurry SPi) t ps + +getParamsS (SPi h t x) = first ((h, t):) $ getParamsS x +getParamsS x = ([], x) + +apps' = foldl $ \a (v, b) -> sApp v a b + +getApps = second reverse . run where + run (SApp _ h a b) = second ((h, b):) $ run a + run x = (x, []) + +downToS n m = map (SVar (debugSI "20", ".ds")) [n+m-1, n+m-2..n] + +xSLabelEnd = id --SLabelEnd + +instance SourceInfo (SExp' a) where + sourceInfo = \case + SGlobal (si, _) -> si + SBind si _ _ e1 e2 -> si + SApp si _ e1 e2 -> si + SLet _ e1 e2 -> sourceInfo e1 <> sourceInfo e2 + SVar (si, _) _ -> si + STyped si _ -> si + SLit si _ -> si + +instance SetSourceInfo (SExp' a) where + setSI si = \case + SBind _ a b c d -> SBind si a b c d + SApp _ a b c -> SApp si a b c + SLet le a b -> SLet le a b + SVar (_, n) i -> SVar (si, n) i + STyped _ t -> STyped si t + SGlobal (_, n) -> SGlobal (si, n) + SLit _ l -> SLit si l + +-------------------------------------------------------------------------------- low-level toolbox + +newtype MaxDB = MaxDB {getMaxDB :: Maybe Int} + +instance Monoid MaxDB where + mempty = MaxDB Nothing + MaxDB a `mappend` MaxDB a' = MaxDB $ Just $ max (fromMaybe 0 a) (fromMaybe 0 a') + +instance Show MaxDB where show _ = "MaxDB" + +varDB i = MaxDB $ Just $ i + 1 + +lowerDB (MaxDB i) = MaxDB $ (+ (- 1)) <$> i +--lowerDB' l (MaxDB i) = MaxDB $ Just $ 1 + max l (fromMaybe 0 i) + +class Up a where + up_ :: Int -> Int -> a -> a + up_ n i = iterateN n $ up1_ i + up1_ :: Int -> a -> a + up1_ = up_ 1 + + fold :: Monoid e => (Int -> Int -> e) -> Int -> a -> e + + used :: Int -> a -> Bool + used = (getAny .) . fold ((Any .) . (==)) + + maxDB_ :: a -> MaxDB + + closedExp :: a -> a + closedExp a = a + +instance (Up a, Up b) => Up (a, b) where + up_ n i (a, b) = (up_ n i a, up_ n i b) + used i (a, b) = used i a || used i b + fold _ _ _ = error "fold @(_,_)" + maxDB_ (a, b) = maxDB_ a <> maxDB_ b + closedExp (a, b) = (closedExp a, closedExp b) + +up n = up_ n 0 +up1 = up1_ 0 + +substS j x = mapS' f2 ((+1) *** up 1) (j, x) + where + f2 sn i (j, x) = case compare i j of + GT -> SVar sn $ i - 1 + LT -> SVar sn i + EQ -> STyped (fst sn) x + +foldS h g f = fs + where + fs i = \case + SApp _ _ a b -> fs i a <> fs i b + SLet _ a b -> fs i a <> fs (i+1) b + SBind _ _ _ a b -> fs i a <> fs (i+1) b + STyped si x -> h i si x + SVar sn j -> f sn j i + SGlobal sn -> g sn i + x@SLit{} -> mempty + +freeS = nub . foldS (\_ _ _ -> error "freeS") (\sn _ -> [sn]) mempty 0 + +usedS n = getAny . foldS (\_ _ _ -> error "usedS") (\sn _ -> Any $ n == sn) mempty 0 + +mapS' = mapS__ (\_ _ _ -> error "mapS'") (const . SGlobal) +mapS__ hh gg f2 h = g where + g i = \case + SApp si v a b -> SApp si v (g i a) (g i b) + SLet x a b -> SLet x (g i a) (g (h i) b) + SBind si k si' a b -> SBind si k si' (g i a) (g (h i) b) + SVar sn j -> f2 sn j i + SGlobal sn -> gg sn i + STyped si x -> hh i si x + x@SLit{} -> x + +rearrangeS :: (Int -> Int) -> SExp -> SExp +rearrangeS f = mapS' (\sn j i -> SVar sn $ if j < i then j else i + f (j - i)) (+1) 0 +{- +substS'' :: Int -> Int -> SExp' a -> SExp' a +substS'' j' x = mapS' f2 (+1) j' + where + f2 sn j i + | j < i = SVar sn j + | j == i = SVar sn $ x + (j - j') + | j > i = SVar sn $ j - 1 +-} +substSG j = mapS__ (\_ _ _ -> error "substSG") (\sn x -> if sn == j then SVar sn x else SGlobal sn) (\sn j -> const $ SVar sn j) (+1) +substSG0 n = substSG n 0 . up1 + +instance Up Void where + up_ n i = error "up_ @Void" + fold _ = error "fold_ @Void" + maxDB_ _ = error "maxDB @Void" + +instance Up a => Up (SExp' a) where + up_ n i = mapS' (\sn j i -> SVar sn $ if j < i then j else j+n) (+1) i + fold f = foldS (\_ _ _ -> error "fold @SExp") mempty $ \sn j i -> f j i + maxDB_ _ = error "maxDB @SExp" + +dbf' = dbf_ 0 +dbf_ j xs e = foldl (\e (i, sn) -> substSG sn i e) e $ zip [j..] xs + +dbff :: DBNames -> SExp -> SExp +dbff ns e = foldr substSG0 e ns + +trSExp' = trSExp elimVoid + +elimVoid :: Void -> a +elimVoid _ = error "impossible" + +trSExp :: (a -> b) -> SExp' a -> SExp' b +trSExp f = g where + g = \case + SApp si v a b -> SApp si v (g a) (g b) + SLet x a b -> SLet x (g a) (g b) + SBind si k si' a b -> SBind si k si' (g a) (g b) + SVar sn j -> SVar sn j + SGlobal sn -> SGlobal sn + SLit si l -> SLit si l + STyped si a -> STyped si $ f a + +-------------------------------------------------------------------------------- expression parsing + +parseType mb = maybe id option mb (reservedOp "::" *> parseTTerm PrecLam) +typedIds mb = (,) <$> commaSep1 (parseSIName upperLower) <*> indented {-TODO-} (parseType mb) + +hiddenTerm p q = (,) Hidden <$ reservedOp "@" <*> p <|> (,) Visible <$> q + +telescope mb = fmap dbfi $ many $ hiddenTerm + (typedId <|> maybe empty (tvar . pure) mb) + (try "::" typedId <|> maybe ((,) <$> parseSIName (pure "") <*> parseTTerm PrecAtom) (tvar . pure) mb) + where + tvar x = (,) <$> parseSIName patVar <*> x + typedId = parens $ tvar $ indented {-TODO-} (parseType mb) + +dbfi = first reverse . unzip . go [] + where + go _ [] = [] + go vs ((v, (n, e)): ts) = (n, (v, dbf' vs e)): go (n: vs) ts + +sVar = withRange $ curry SGlobal + +parseTTerm = typeNS . parseTerm +parseETerm = expNS . parseTerm + +indentation p q = p >> indented q + +parseTerm :: Prec -> P SExp +parseTerm prec = withRange setSI $ case prec of + PrecLam -> + do level PrecAnn $ \t -> mkPi <$> (Visible <$ reservedOp "->" <|> Hidden <$ reservedOp "=>") <*> pure t <*> parseTTerm PrecLam + <|> mkIf <$ reserved "if" <*> parseTerm PrecLam <* reserved "then" <*> parseTerm PrecLam <* reserved "else" <*> parseTerm PrecLam + <|> do reserved "forall" + (fe, ts) <- telescope (Just $ Wildcard SType) + f <- SPi . const Hidden <$ reservedOp "." <|> SPi . const Visible <$ reservedOp "->" + t' <- dbf' fe <$> parseTTerm PrecLam + return $ foldr (uncurry f) t' ts + <|> do expNS $ do + (fe, ts) <- reservedOp "\\" *> telescopePat <* reservedOp "->" + checkPattern fe + t' <- dbf' fe <$> parseTerm PrecLam + ge <- dsInfo + return $ foldr (uncurry (patLam id ge)) t' ts + <|> compileCase <$ reserved "case" <*> dsInfo <*> parseETerm PrecLam <*> do + indentSome "of" $ do + (fe, p) <- longPattern + (,) p <$> parseRHS (dbf' fe) "->" +-- <|> compileGuardTree id id <$> dsInfo <*> (Alts <$> parseSomeGuards (const True)) + PrecAnn -> level PrecOp $ \t -> SAnn t <$> parseType Nothing + PrecOp -> (notOp False <|> notExp) >>= \xs -> join $ calculatePrecs <$> dsInfo <*> pure xs where + notExp = (++) <$> ope <*> notOp True + notOp x = (++) <$> try "expression" ((++) <$> ex PrecApp <*> option [] ope) <*> notOp True + <|> if x then option [] (try "lambda" $ ex PrecLam) else mzero + ope = pure . Left <$> parseSIName (rhsOperator <|> "'EqCTt" <$ reservedOp "~") + ex pr = pure . Right <$> parseTerm pr + PrecApp -> + apps' <$> try "record" (sVar upperCase <* reservedOp "{") <*> (commaSep $ lowerCase *> reservedOp "=" *> ((,) Visible <$> parseTerm PrecLam)) <* reservedOp "}" + <|> apps' <$> parseTerm PrecSwiz <*> many (hiddenTerm (parseTTerm PrecSwiz) $ parseTerm PrecSwiz) + PrecSwiz -> level PrecProj $ \t -> mkSwizzling t <$> lexeme (try "swizzling" $ char '%' *> manyNM 1 4 (satisfy (`elem` ("xyzwrgba" :: String)))) + PrecProj -> level PrecAtom $ \t -> try "projection" $ mkProjection t <$ char '.' <*> sepBy1 (sLit . LString <$> lowerCase) (char '.') + PrecAtom -> + mkLit <$> try "literal" parseLit + <|> Wildcard (Wildcard SType) <$ reserved "_" + <|> char '\'' *> switchNS (parseTerm PrecAtom) + <|> sVar (try "identifier" upperLower) + <|> brackets ( (parseTerm PrecLam >>= \e -> + mkDotDot e <$ reservedOp ".." <*> parseTerm PrecLam + <|> foldr ($) (SBuiltin "Cons" `SAppV` e `SAppV` SBuiltin "Nil") <$ reservedOp "|" <*> commaSep (generator <|> letdecl <|> boolExpression) + <|> mkList <$> namespace <*> ((e:) <$> option [] (symbol "," *> commaSep1 (parseTerm PrecLam))) + ) <|> mkList <$> namespace <*> pure []) + <|> mkTuple <$> namespace <*> parens (commaSep $ parseTerm PrecLam) + <|> mkRecord <$> braces (commaSep $ (,) <$> lowerCase <* symbol ":" <*> parseTerm PrecLam) + <|> mkLets True <$> dsInfo <*> parseDefs xSLabelEnd (indentMany "let") <* reserved "in" <*> parseTerm PrecLam + where + level pr f = parseTerm pr >>= \t -> option t $ f t + + mkSwizzling term = swizzcall + where + sc c = SBuiltin ['S',c] + swizzcall [x] = SBuiltin "swizzscalar" `SAppV` term `SAppV` (sc . synonym) x + swizzcall xs = SBuiltin "swizzvector" `SAppV` term `SAppV` swizzparam xs + swizzparam xs = foldl SAppV (vec xs) $ map (sc . synonym) xs + vec xs = SBuiltin $ case length xs of + 0 -> error "impossible: swizzling parsing returned empty pattern" + 1 -> error "impossible: swizzling went to vector for one scalar" + n -> "V" ++ show n + synonym 'r' = 'x' + synonym 'g' = 'y' + synonym 'b' = 'z' + synonym 'a' = 'w' + synonym c = c + + mkProjection = foldl $ \exp field -> SBuiltin "project" `SAppV` field `SAppV` exp + + -- Creates: RecordCons @[("x", _), ("y", _), ("z", _)] (1.0, (2.0, (3.0, ()))) + mkRecord xs = SBuiltin "RecordCons" `SAppH` names `SAppV` values + where + (names, values) = mkNames *** mkValues $ unzip xs + + mkNameTuple v = SBuiltin "Tuple2" `SAppV` sLit (LString v) `SAppV` Wildcard SType + mkNames = foldr (\n ns -> SBuiltin "Cons" `SAppV` mkNameTuple n `SAppV` ns) + (SBuiltin "Nil") + + mkValues = foldr (\x xs -> SBuiltin "Tuple2" `SAppV` x `SAppV` xs) + (SBuiltin "Tuple0") + + mkTuple _ [Section e] = e + mkTuple _ [x] = x + mkTuple (Namespace level _) xs = foldl SAppV (SBuiltin (tuple ++ show (length xs))) xs + where tuple = case level of + Just TypeLevel -> "'Tuple" + Just ExpLevel -> "Tuple" + _ -> error "mkTuple" + + mkList (Namespace (Just TypeLevel) _) [x] = SBuiltin "'List" `SAppV` x + mkList (Namespace (Just ExpLevel) _) xs = foldr (\x l -> SBuiltin "Cons" `SAppV` x `SAppV` l) (SBuiltin "Nil") xs + mkList _ xs = error "mkList" + + mkLit n@LInt{} = SBuiltin "fromInt" `SAppV` sLit n + mkLit l = sLit l + + mkIf b t f = SBuiltin "primIfThenElse" `SAppV` b `SAppV` t `SAppV` f + + mkDotDot e f = SBuiltin "fromTo" `SAppV` e `SAppV` f + + calculatePrecs :: DesugarInfo -> [Either SIName SExp] -> P SExp + calculatePrecs dcls = either fail return . f where + f [] = error "impossible" + f (Right t: xs) = either (\(op, xs) -> Section $ SLamV $ SGlobal op `SAppV` up1 (calcPrec' t xs) `SAppV` SVar (mempty, ".rs") 0) (calcPrec' t) <$> cont xs + f xs@(Left op@(_, "-"): _) = f $ Right (mkLit $ LInt 0): xs + f (Left op: xs) = g op xs >>= either (const $ Left "TODO: better error message @476") + (\((op, e): oe) -> return $ Section $ SLamV $ SGlobal op `SAppV` SVar (mempty, ".ls") 0 `SAppV` up1 (calcPrec' e oe)) + g op (Right t: xs) = (second ((op, t):) +++ ((op, t):)) <$> cont xs + g op [] = return $ Left (op, []) + g op _ = Left "two operator is not allowed next to each-other" + cont (Left op: xs) = g op xs + cont [] = return $ Right [] + cont _ = error "impossible" + + calcPrec' = calcPrec (\op x y -> SGlobal op `SAppV` x `SAppV` y) (getFixity dcls . snd) + + generator, letdecl, boolExpression :: P (SExp -> SExp) + generator = do + ge <- dsInfo + (dbs, pat) <- try "generator" $ longPattern <* reservedOp "<-" + checkPattern dbs + exp <- parseTerm PrecLam + return $ \e -> + SBuiltin "concatMap" + `SAppV` SLamV (compileGuardTree id id ge $ Alts + [ compilePatts [(pat, 0)] $ Right $ dbff dbs e + , GuardLeaf $ SBuiltin "Nil" + ]) + `SAppV` exp + + letdecl = mkLets False <$ reserved "let" <*> dsInfo <*> (compileFunAlts' id =<< valueDef) + + boolExpression = (\pred e -> SBuiltin "primIfThenElse" `SAppV` pred `SAppV` e `SAppV` SBuiltin "Nil") <$> parseTerm PrecLam + + + mkPi Hidden (getTTuple' -> xs) b = foldr (sNonDepPi Hidden) b xs + mkPi h a b = sNonDepPi h a b + + sNonDepPi h a b = SPi h a $ up1 b + +getTTuple' (getTTuple -> Just (n, xs)) | n == length xs = xs +getTTuple' x = [x] + +getTTuple (SAppV (getTTuple -> Just (n, xs)) z) = Just (n, xs ++ [z]{-todo: eff-}) +getTTuple (SGlobal (si, s@(splitAt 6 -> ("'Tuple", reads -> [(n, "")])))) = Just (n :: Int, []) +getTTuple _ = Nothing + +patLam :: (SExp -> SExp) -> DesugarInfo -> (Visibility, SExp) -> Pat -> SExp -> SExp +patLam f ge (v, t) p e = SLam v t $ compileGuardTree f f ge $ compilePatts [(p, 0)] $ Right e + +-------------------------------------------------------------------------------- pattern representation + +data Pat + = PVar SIName -- Int + | PCon SIName [ParPat] + | ViewPat SExp ParPat + | PatType ParPat SExp + deriving Show + +-- parallel patterns like v@(f -> [])@(Just x) +newtype ParPat = ParPat [Pat] + deriving Show + +mapPP f = \case + ParPat ps -> ParPat (mapP f <$> ps) + +mapP :: (SExp -> SExp) -> Pat -> Pat +mapP f = \case + PVar n -> PVar n + PCon n pp -> PCon n (mapPP f <$> pp) + ViewPat e pp -> ViewPat (f e) (mapPP f pp) + PatType pp e -> PatType (mapPP f pp) (f e) + +--upP i j = mapP (up_ j i) + +varPP = length . getPPVars_ +varP = length . getPVars_ + +type DBNames = [SIName] -- De Bruijn variable names + +getPVars :: Pat -> DBNames +getPVars = reverse . getPVars_ + +getPPVars = reverse . getPPVars_ + +getPVars_ = \case + PVar n -> [n] + PCon _ pp -> foldMap getPPVars_ pp + ViewPat e pp -> getPPVars_ pp + PatType pp e -> getPPVars_ pp + +getPPVars_ = \case + ParPat pp -> foldMap getPVars_ pp + +instance SourceInfo ParPat where + sourceInfo (ParPat ps) = sourceInfo ps + +instance SourceInfo Pat where + sourceInfo = \case + PVar (si,_) -> si + PCon (si,_) ps -> si <> sourceInfo ps + ViewPat e ps -> sourceInfo e <> sourceInfo ps + PatType ps e -> sourceInfo ps <> sourceInfo e + +-------------------------------------------------------------------------------- pattern parsing + +parsePat :: Prec -> P Pat +parsePat = \case + PrecAnn -> + patType <$> parsePat PrecOp <*> parseType (Just $ Wildcard SType) + PrecOp -> + calculatePatPrecs <$> dsInfo <*> p_ + where + p_ = (,) <$> parsePat PrecApp <*> option [] (parseSIName colonSymbols >>= p) + p op = do (exp, op') <- try "pattern" ((,) <$> parsePat PrecApp <*> parseSIName colonSymbols) + ((op, exp):) <$> p op' + <|> pure . (,) op <$> parsePat PrecAnn + PrecApp -> + PCon <$> parseSIName upperCase <*> many (ParPat . pure <$> parsePat PrecAtom) + <|> parsePat PrecAtom + PrecAtom -> + mkLit <$> namespace <*> try "literal" parseLit + <|> flip PCon [] <$> parseSIName upperCase + <|> char '\'' *> switchNS (parsePat PrecAtom) + <|> PVar <$> parseSIName patVar + <|> (\ns -> pConSI . mkListPat ns) <$> namespace <*> brackets patlist + <|> (\ns -> pConSI . mkTupPat ns) <$> namespace <*> parens patlist + where + litP = flip ViewPat (ParPat [PCon (mempty, "True") []]) . SAppV (SBuiltin "==") + + mkLit (Namespace (Just TypeLevel) _) (LInt n) = toNatP n -- todo: elim this alternative + mkLit _ n@LInt{} = litP (SBuiltin "fromInt" `SAppV` sLit n) + mkLit _ n = litP (sLit n) + + toNatP = run where + run 0 = PCon (mempty, "Zero") [] + run n | n > 0 = PCon (mempty, "Succ") [ParPat [run $ n-1]] + + pConSI (PCon (_, n) ps) = PCon (sourceInfo ps, n) ps + pConSI p = p + + patlist = commaSep $ parsePat PrecAnn + + mkListPat ns [p] | namespaceLevel ns == Just TypeLevel = PCon (debugSI "mkListPat4", "'List") [ParPat [p]] + mkListPat ns (p: ps) = PCon (debugSI "mkListPat2", "Cons") $ map (ParPat . (:[])) [p, mkListPat ns ps] + mkListPat _ [] = PCon (debugSI "mkListPat3", "Nil") [] + + --mkTupPat :: [Pat] -> Pat + mkTupPat ns [x] = x + mkTupPat ns ps = PCon (debugSI "", tick ns $ "Tuple" ++ show (length ps)) (ParPat . (:[]) <$> ps) + + patType p (Wildcard SType) = p + patType p t = PatType (ParPat [p]) t + + calculatePatPrecs dcls (e, xs) = calcPrec (\op x y -> PCon op $ ParPat . (:[]) <$> [x, y]) (getFixity dcls . snd) e xs + +longPattern = parsePat PrecAnn <&> (getPVars &&& id) +--patternAtom = parsePat PrecAtom <&> (getPVars &&& id) + +telescopePat = fmap (getPPVars . ParPat . map snd &&& id) $ many $ uncurry f <$> hiddenTerm (parsePat PrecAtom) (parsePat PrecAtom) + where + f h (PatType (ParPat [p]) t) = ((h, t), p) + f h p = ((h, Wildcard SType), p) + +checkPattern :: DBNames -> P () +checkPattern ns = lift $ tell $ pure $ + case [ns' | ns' <- group . sort . filter (not . null . snd) $ ns + , not . null . tail $ ns'] of + [] -> Nothing + xs -> Just $ "multiple pattern vars:\n" ++ unlines [n ++ " is defined at " ++ ppShow si | ns <- xs, (si, n) <- ns] + + +-------------------------------------------------------------------------------- pattern match compilation + +data GuardTree + = GuardNode SExp SName [ParPat] GuardTree -- _ <- _ + | Alts [GuardTree] -- _ | _ + | GuardLeaf SExp -- _ -> e + deriving Show + +alts (Alts xs) = concatMap alts xs +alts x = [x] + +mapGT k i = \case + GuardNode e c pps gt -> GuardNode (i k e) c {-todo: up-}pps $ mapGT (k + sum (map varPP pps)) i gt + Alts gts -> Alts $ map (mapGT k i) gts + GuardLeaf e -> GuardLeaf $ i k e + +upGT k i = mapGT k $ \k -> up_ i k + +substGT i j = mapGT 0 $ \k -> rearrangeS $ \r -> if r == k + i then k + j else if r > k + i then r - 1 else r +{- +dbfGT :: DBNames -> GuardTree -> GuardTree +dbfGT v = mapGT 0 $ \k -> dbf_ k v +-} +-- todo: clenup +compilePatts :: [(Pat, Int)] -> Either [(SExp, SExp)] SExp -> GuardTree +compilePatts ps gu = cp [] ps + where + cp ps' [] = case gu of + Right e -> GuardLeaf $ rearrangeS (f $ reverse ps') e + Left gs -> Alts + [ GuardNode (rearrangeS (f $ reverse ps') ge) "True" [] $ GuardLeaf $ rearrangeS (f $ reverse ps') e + | (ge, e) <- gs + ] + cp ps' ((p@PVar{}, i): xs) = cp (p: ps') xs + cp ps' ((p@(PCon (si, n) ps), i): xs) = GuardNode (SVar (si, n) $ i + sum (map (fromMaybe 0 . ff) ps')) n ps $ cp (p: ps') xs + cp ps' ((p@(ViewPat f (ParPat [PCon (si, n) ps])), i): xs) + = GuardNode (SAppV f $ SVar (si, n) $ i + sum (map (fromMaybe 0 . ff) ps')) n ps $ cp (p: ps') xs + + m = length ps + + ff PVar{} = Nothing + ff p = Just $ varP p + + f ps i + | i >= s = i - s + m + sum vs' + | i < s = case vs_ !! n of + Nothing -> m + sum vs' - 1 - n + Just _ -> m + sum vs' - 1 - (m + sum (take n vs') + j) + where + i' = s - 1 - i + (n, j) = concat (zipWith (\k j -> zip (repeat j) [0..k-1]) vs [0..]) !! i' + + vs_ = map ff ps + vs = map (fromMaybe 1) vs_ + vs' = map (fromMaybe 0) vs_ + s = sum vs + +compileGuardTrees False ulend lend ge alts = compileGuardTree ulend lend ge $ Alts alts +compileGuardTrees True ulend lend ge alts = foldr1 (SAppV2 $ SBuiltin "parEval" `SAppV` Wildcard SType) $ compileGuardTree ulend lend ge <$> alts + +compileGuardTree :: (SExp -> SExp) -> (SExp -> SExp) -> DesugarInfo -> GuardTree -> SExp +compileGuardTree ulend lend adts t = (\x -> traceD (" ! :" ++ ppShow x) x) $ guardTreeToCases t + where + guardTreeToCases :: GuardTree -> SExp + guardTreeToCases t = case alts t of + [] -> ulend $ SBuiltin "undefined" + GuardLeaf e: _ -> lend e + ts@(GuardNode f s _ _: _) -> case Map.lookup s (snd adts) of + Nothing -> error $ "Constructor is not defined: " ++ s + Just (Left ((t, inum), cns)) -> + foldl SAppV (SGlobal (debugSI "compileGuardTree2", caseName t) `SAppV` iterateN (1 + inum) SLamV (Wildcard SType)) + [ iterateN n SLamV $ guardTreeToCases $ Alts $ map (filterGuardTree (up n f) cn 0 n . upGT 0 n) ts + | (cn, n) <- cns + ] + `SAppV` f + Just (Right n) -> SGlobal (debugSI "compileGuardTree3", MatchName s) + `SAppV` SLamV (Wildcard SType) + `SAppV` iterateN n SLamV (guardTreeToCases $ Alts $ map (filterGuardTree (up n f) s 0 n . upGT 0 n) ts) + `SAppV` f + `SAppV` guardTreeToCases (Alts $ map (filterGuardTree' f s) ts) + + filterGuardTree :: SExp -> SName{-constr.-} -> Int -> Int{-number of constr. params-} -> GuardTree -> GuardTree + filterGuardTree f s k ns = \case + GuardLeaf e -> GuardLeaf e + Alts ts -> Alts $ map (filterGuardTree f s k ns) ts + GuardNode f' s' ps gs + | f /= f' -> GuardNode f' s' ps $ filterGuardTree (up su f) s (su + k) ns gs + | s == s' -> filterGuardTree f s k ns $ guardNodes (zips [k+ns-1, k+ns-2..] ps) gs + | otherwise -> Alts [] + where + zips is ps = zip (map (SVar (debugSI "30", ".30")) $ zipWith (+) is $ sums $ map varPP ps) ps + su = sum $ map varPP ps + sums = scanl (+) 0 + + filterGuardTree' :: SExp -> SName{-constr.-} -> GuardTree -> GuardTree + filterGuardTree' f s = \case + GuardLeaf e -> GuardLeaf e + Alts ts -> Alts $ map (filterGuardTree' f s) ts + GuardNode f' s' ps gs + | f /= f' || s /= s' -> GuardNode f' s' ps $ filterGuardTree' (up su f) s gs + | otherwise -> Alts [] + where + su = sum $ map varPP ps + + guardNodes :: [(SExp, ParPat)] -> GuardTree -> GuardTree + guardNodes [] l = l + guardNodes ((v, ParPat ws): vs) e = guardNode v ws $ guardNodes vs e + + guardNode :: SExp -> [Pat] -> GuardTree -> GuardTree + guardNode v [] e = e + guardNode v [w] e = case w of + PVar _ -> {-todo guardNode v (subst x v ws) $ -} varGuardNode 0 v e + ViewPat f (ParPat p) -> guardNode (f `SAppV` v) p {- $ guardNode v ws -} e + PCon (_, s) ps' -> GuardNode v s ps' {- $ guardNode v ws -} e + + varGuardNode v (SVar _ e) = substGT v e + +compileCase ge x cs + = SLamV (compileGuardTree id id ge $ Alts [compilePatts [(p, 0)] e | (p, e) <- cs]) `SAppV` x + + +-------------------------------------------------------------------------------- declaration representation + +data Stmt + = Let SIName MFixity (Maybe SExp) [Visibility]{-source arity-} SExp + | Data SIName [(Visibility, SExp)]{-parameters-} SExp{-type-} Bool{-True:add foralls-} [(SIName, SExp)]{-constructor names and types-} + | PrecDef SIName Fixity + + -- eliminated during parsing + | TypeFamily SIName [(Visibility, SExp)]{-parameters-} SExp{-type-} + | Class SIName [SExp]{-parameters-} [(SIName, SExp)]{-method names and types-} + | Instance SIName [Pat]{-parameter patterns-} [SExp]{-constraints-} [Stmt]{-method definitions-} + | TypeAnn SIName SExp -- intermediate + | FunAlt SIName [((Visibility, SExp), Pat)] (Either [(SExp, SExp)]{-guards-} SExp{-no guards-}) + deriving (Show) + +pattern Primitive n mf t <- Let n mf (Just t) _ (SBuiltin "undefined") where Primitive n mf t = Let n mf (Just t) (map fst $ fst $ getParamsS t) $ SBuiltin "undefined" + +-------------------------------------------------------------------------------- declaration parsing + +parseDef :: P [Stmt] +parseDef = + do indentation (reserved "data") $ do + x <- typeNS $ parseSIName upperCase + (npsd, ts) <- telescope (Just SType) + t <- dbf' npsd <$> parseType (Just SType) + let mkConTy mk (nps', ts') = + ( if mk then Just nps' else Nothing + , foldr (uncurry SPi) (foldl SAppV (SGlobal x) $ downToS (length ts') $ length ts) ts') + (af, cs) <- option (True, []) $ + do fmap ((,) True) $ indentMany "where" $ second ((,) Nothing . dbf' npsd) <$> typedIds Nothing + <|> (,) False <$ reservedOp "=" <*> + sepBy1 ((,) <$> (pure <$> parseSIName upperCase) + <*> do do braces $ mkConTy True . second (zipWith (\i (v, e) -> (v, dbf_ i npsd e)) [0..]) + <$> telescopeDataFields + <|> mkConTy False . second (zipWith (\i (v, e) -> (v, dbf_ i npsd e)) [0..]) + <$> telescope Nothing + ) + (reservedOp "|") + mkData <$> dsInfo <*> pure x <*> pure ts <*> pure t <*> pure af <*> pure (concatMap (\(vs, t) -> (,) <$> vs <*> pure t) cs) + <|> do indentation (reserved "class") $ do + x <- parseSIName $ typeNS upperCase + (nps, ts) <- telescope (Just SType) + cs <- option [] $ indentMany "where" $ typedIds Nothing + return $ pure $ Class x (map snd ts) (concatMap (\(vs, t) -> (,) <$> vs <*> pure (dbf' nps t)) cs) + <|> do indentation (reserved "instance") $ typeNS $ do + constraints <- option [] $ try "constraint" $ getTTuple' <$> parseTerm PrecOp <* reservedOp "=>" + x <- parseSIName upperCase + (nps, args) <- telescopePat + checkPattern nps + cs <- expNS $ option [] $ indentSome "where" $ dbFunAlt nps <$> funAltDef varId + pure . Instance x ({-todo-}map snd args) (dbff (nps <> [x]) <$> constraints) <$> compileFunAlts' id{-TODO-} cs + <|> do indentation (try "type family" $ reserved "type" >> reserved "family") $ typeNS $ do + x <- parseSIName upperCase + (nps, ts) <- telescope (Just SType) + t <- dbf' nps <$> parseType (Just SType) + option {-open type family-}[TypeFamily x ts t] $ do + cs <- indentMany "where" $ funAltDef $ mfilter (== snd x) upperCase + -- closed type family desugared here + compileFunAlts False id SLabelEnd [TypeAnn x $ addParamsS ts t] cs + <|> do indentation (try "type instance" $ reserved "type" >> reserved "instance") $ typeNS $ pure <$> funAltDef upperCase + <|> do indentation (reserved "type") $ typeNS $ do + x <- parseSIName upperCase + (nps, ts) <- telescope $ Just (Wildcard SType) + rhs <- dbf' nps <$ reservedOp "=" <*> parseTerm PrecLam + compileFunAlts False id SLabelEnd + [{-TypeAnn x $ addParamsS ts $ SType-}{-todo-}] + [FunAlt x (zip ts $ map PVar $ reverse nps) $ Right rhs] + <|> do try "typed ident" $ (\(vs, t) -> TypeAnn <$> vs <*> pure t) <$> typedIds Nothing + <|> map (uncurry PrecDef) <$> parseFixityDecl + <|> pure <$> funAltDef varId + <|> valueDef + where + telescopeDataFields :: P ([SIName], [(Visibility, SExp)]) + telescopeDataFields = dbfi <$> commaSep ((,) Visible <$> ((,) <$> parseSIName lowerCase <*> parseType Nothing)) + + mkData ge x ts t af cs = Data x ts t af (second snd <$> cs): concatMap mkProj (nub $ concat [fs | (_, (Just fs, _)) <- cs]) + where + mkProj fn + = [ FunAlt fn [((Visible, Wildcard SType), PCon cn $ replicate (length fs) $ ParPat [PVar (mempty, "generated_name1")])] $ Right $ SVar (mempty, ".proj") i + | (cn, (Just fs, _)) <- cs, (i, fn') <- zip [0..] fs, fn' == fn + ] + + +parseRHS fe tok = fmap (fmap (fe *** fe) +++ fe) $ indented $ do + fmap Left . some $ (,) <$ reservedOp "|" <*> parseTerm PrecOp <* reservedOp tok <*> parseTerm PrecLam + <|> do + reservedOp tok + rhs <- parseTerm PrecLam + f <- option id $ mkLets True <$> dsInfo <*> parseDefs xSLabelEnd (indentMany "where") + return $ Right $ f rhs + +parseDefs lend p = p parseDef >>= compileFunAlts' lend . concat + +funAltDef parseName = do -- todo: use ns to determine parseName + (n, (fee, tss)) <- + do try "operator definition" $ do + (e', a1) <- longPattern + indented $ do + n <- parseSIName lhsOperator + (e'', a2) <- longPattern + lookAhead $ reservedOp "=" <|> reservedOp "|" + return (n, (e'' <> e', (,) (Visible, Wildcard SType) <$> [a1, mapP (dbf' e') a2])) + <|> do try "lhs" $ do + n <- parseSIName parseName + indented $ (,) n <$> telescopePat <* lookAhead (reservedOp "=" <|> reservedOp "|") + checkPattern fee + FunAlt n tss <$> parseRHS (dbf' fee) "=" + +valueDef :: P [Stmt] +valueDef = do + (dns, p) <- try "pattern" $ longPattern <* reservedOp "=" + checkPattern dns + e <- indented $ parseETerm PrecLam + ds <- dsInfo + return $ desugarValueDef ds p e + +desugarValueDef ds p e + = FunAlt n [] (Right e) + : [ FunAlt x [] $ Right $ compileCase ds (SGlobal n) [(p, Right $ SVar x i)] + | (i, x) <- zip [0..] dns + ] + where + dns = getPVars p + n = mangleNames dns + +mangleNames xs = (foldMap fst xs, "_" ++ intercalate "_" (map snd xs)) +{- +parseSomeGuards f = do + pos <- sourceColumn <$> getPosition <* reservedOp "|" + guard $ f pos + (e', f) <- + do (e', PCon (_, p) vs) <- try "pattern" $ longPattern <* reservedOp "<-" + checkPattern e' + x <- parseETerm PrecOp + return (e', \gs' gs -> GuardNode x p vs (Alts gs'): gs) + <|> do x <- parseETerm PrecOp + return (mempty, \gs' gs -> [GuardNode x "True" [] $ Alts gs', GuardNode x "False" [] $ Alts gs]) + f <$> ((map (dbfGT e') <$> parseSomeGuards (> pos)) <|> (:[]) . GuardLeaf <$ reservedOp "->" <*> (dbf' e' <$> parseETerm PrecLam)) + <*> option [] (parseSomeGuards (== pos)) +-} +mkLets :: Bool -> DesugarInfo -> [Stmt]{-where block-} -> SExp{-main expression-} -> SExp{-big let with lambdas; replaces global names with de bruijn indices-} +mkLets a ds = mkLets' a ds . sortDefs ds where + mkLets' _ _ [] e = e + mkLets' False ge (Let n _ mt ar x: ds) e | not $ usedS n x + = SLet (False, n, SData Nothing, ar) (maybe id (flip SAnn . addForalls {-todo-}[] []) mt x) (substSG0 n $ mkLets' False ge ds e) + mkLets' True ge (Let n _ mt ar x: ds) e | not $ usedS n x + = SLet (False, n, SData Nothing, ar) (maybe id (flip SAnn . addForalls {-todo-}[] []) mt x) (substSG0 n $ mkLets' True ge ds e) + mkLets' _ _ (x: ds) e = error $ "mkLets: " ++ show x + +addForalls :: Up a => Extensions -> [SName] -> SExp' a -> SExp' a +addForalls exs defined x = foldl f x [v | v@(_, vh:_) <- reverse $ freeS x, snd v `notElem'` ("fromInt"{-todo: remove-}: defined), isLower vh || NoConstructorNamespace `elem` exs] + where + f e v = SPi Hidden (Wildcard SType) $ substSG0 v e + + notElem' s@('\'':s') m = notElem s m && notElem s' m + notElem' s m = s `notElem` m +{- +defined defs = ("'Type":) $ flip foldMap defs $ \case + TypeAnn (_, x) _ -> [x] + Let (_, x) _ _ _ _ -> [x] + Data (_, x) _ _ _ cs -> x: map (snd . fst) cs + Class (_, x) _ cs -> x: map (snd . fst) cs + TypeFamily (_, x) _ _ -> [x] + x -> error $ unwords ["defined: Impossible", show x, "cann't be here"] +-} + +-------------------------------------------------------------------------------- declaration desugaring + +sortDefs ds xs = concatMap (desugarMutual ds) $ topSort mempty mempty mempty nodes + where + nodes = zip (zip [0..] xs) $ map (def &&& need) xs + need = \case + PrecDef{} -> mempty + Let _ _ mt _ e -> foldMap freeS' mt <> freeS' e + Data _ ps t _ cs -> foldMap (freeS' . snd) ps <> freeS' t <> foldMap (freeS' . snd) cs + def = \case + PrecDef{} -> mempty + Let n _ _ _ _ -> Set.singleton n + Data n _ _ _ cs -> Set.singleton n <> Set.fromList (map fst cs) + freeS' = Set.fromList . freeS + topSort acc@(_:_) defs vs xs | Set.null vs = reverse acc: topSort mempty defs vs xs + topSort [] _ vs [] | Set.null vs = [] + topSort acc defs vs (x@((i, v), (d, u)): ns) + | i `elem` vs || all (`elem` defs) u = topSort (v: acc) (d <> defs) (Set.delete i vs) ns + | otherwise = topSort acc defs (Set.insert i vs) $ let + (ns1, ns2) = span (\(_, (d, _)) -> not $ Set.null $ d `Set.intersection` u) ns + in ns1 ++ x: ns2 + +desugarMutual _ [x] = [x] +desugarMutual ds xs = xs +{- + = FunAlt n [] (Right e) + : [ FunAlt x [] $ Right $ compileCase ds (SGlobal n) [(p, Right $ SVar x i)] + | (i, x) <- zip [0..] dns + ] + where + dns = getPVars p + n = mangleNames dns + (ps, es) = unzip [(n, e) | Let n ~Nothing ~Nothing [] e <- xs] + tup = "Tuple" ++ show (length xs) + e = dbf' ps $ foldl SAppV (SBuiltin tup) es + p = PCon (mempty, tup) $ map (ParPat . pure . PVar) ps +-} + + +compileFunAlts' lend ds = fmap concat . sequence $ map (compileFunAlts False lend lend ds) $ groupBy h ds where + h (FunAlt n _ _) (FunAlt m _ _) = m == n + h _ _ = False + +--compileFunAlts :: forall m . Monad m => Bool -> (SExp -> SExp) -> (SExp -> SExp) -> DesugarInfo -> [Stmt] -> [Stmt] -> m [Stmt] +compileFunAlts par ulend lend ds xs = dsInfo >>= \ge -> case xs of + [Instance{}] -> return [] + [Class n ps ms] -> compileFunAlts' SLabelEnd $ + [ TypeAnn n $ foldr (SPi Visible) SType ps ] + ++ [ FunAlt n (map noTA ps) $ Right $ foldr (SAppV2 $ SBuiltin "'T2") (SBuiltin "'Unit") cstrs | Instance n' ps cstrs _ <- ds, n == n' ] + ++ [ FunAlt n (replicate (length ps) (noTA $ PVar (debugSI "compileFunAlts1", "generated_name0"))) $ Right $ SBuiltin "'Empty" `SAppV` sLit (LString $ "no instance of " ++ snd n ++ " on ???")] + ++ concat + [ TypeAnn m (addParamsS (map ((,) Hidden) ps) $ SPi Hidden (foldl SAppV (SGlobal n) $ downToS 0 $ length ps) $ up1 t) + : [ FunAlt m p $ Right {- $ SLam Hidden (Wildcard SType) $ up1 -} e + | Instance n' i cstrs alts <- ds, n' == n + , Let m' ~Nothing ~Nothing ar e <- alts, m' == m + , let p = zip ((,) Hidden <$> ps) i -- ++ ((Hidden, Wildcard SType), PVar): [] +-- , let ic = sum $ map varP i + ] + | (m, t) <- ms +-- , let ts = fst $ getParamsS $ up1 t + ] + [TypeAnn n t] -> return [Primitive n Nothing t | snd n `notElem` [n' | FunAlt (_, n') _ _ <- ds]] + tf@[TypeFamily n ps t] -> case [d | d@(FunAlt n' _ _) <- ds, n' == n] of + [] -> return [Primitive n Nothing $ addParamsS ps t] + alts -> compileFunAlts True id SLabelEnd [TypeAnn n $ addParamsS ps t] alts + [p@PrecDef{}] -> return [p] + fs@(FunAlt n vs _: _) -> case map head $ group [length vs | FunAlt _ vs _ <- fs] of + [num] + | num == 0 && length fs > 1 -> fail $ "redefined " ++ snd n ++ " at " ++ ppShow (fst n) + | n `elem` [n' | TypeFamily n' _ _ <- ds] -> return [] + | otherwise -> return + [ Let n + (listToMaybe [t | PrecDef n' t <- ds, n' == n]) + (listToMaybe [t | TypeAnn n' t <- ds, n' == n]) + (map (fst . fst) vs) + (foldr (uncurry SLam . fst) (compileGuardTrees par ulend lend ge + [ compilePatts (zip (map snd vs) $ reverse [0.. num - 1]) gsx + | FunAlt _ vs gsx <- fs + ]) vs) + ] + _ -> fail $ "different number of arguments of " ++ snd n ++ " at " ++ ppShow (fst n) + x -> return x + where + noTA x = ((Visible, Wildcard SType), x) + +dbFunAlt v (FunAlt n ts gue) = FunAlt n (map (second $ mapP (dbf' v)) ts) $ fmap (dbf' v *** dbf' v) +++ dbf' v $ gue + + +-------------------------------------------------------------------------------- desugar info + +mkDesugarInfo :: [Stmt] -> DesugarInfo +mkDesugarInfo ss = + ( Map.fromList $ ("'EqCTt", (Infix, -1)): [(s, f) | PrecDef (_, s) f <- ss] + , Map.fromList $ + [(cn, Left ((t, pars ty), (snd *** pars) <$> cs)) | Data (_, t) ps ty _ cs <- ss, ((_, cn), ct) <- cs] + ++ [(t, Right $ pars $ addParamsS ps ty) | Data (_, t) ps ty _ cs <- ss] + ) + where + pars ty = length $ filter ((== Visible) . fst) $ fst $ getParamsS ty -- todo + +joinDesugarInfo (fm, cm) (fm', cm') = (Map.union fm fm', Map.union cm cm') + + +-------------------------------------------------------------------------------- module exports + +data Export = ExportModule SName | ExportId SName + +parseExport :: Namespace -> P Export +parseExport ns = + ExportModule <$ reserved "module" <*> moduleName + <|> ExportId <$> varId + +-------------------------------------------------------------------------------- module imports + +data ImportItems + = ImportAllBut [SName] + | ImportJust [SName] + +importlist = parens $ commaSep upperLower + +-------------------------------------------------------------------------------- language pragmas + +type Extensions = [Extension] + +data Extension + = NoImplicitPrelude + | NoTypeNamespace + | NoConstructorNamespace + | TraceTypeCheck + deriving (Enum, Eq, Ord, Show) + +extensionMap :: Map.Map String Extension +extensionMap = Map.fromList $ map (show &&& id) [toEnum 0 .. ] + +parseExtensions :: P [Extension] +parseExtensions + = try "pragma" (symbol "{-#") *> symbol "LANGUAGE" *> commaSep (lexeme ext) <* symbol "#-}" + where + ext = do + s <- some $ satisfy isAlphaNum + maybe + (fail $ "language extension expected instead of " ++ s) + return + (Map.lookup s extensionMap) + +-------------------------------------------------------------------------------- modules + +data Module + = Module + { extensions :: Extensions + , moduleImports :: [(SName, ImportItems)] + , moduleExports :: Maybe [Export] + , definitions :: DesugarInfo -> (Either String [Stmt], [PostponedCheck]) + , sourceCode :: String + } + +parseModule :: FilePath -> String -> P Module +parseModule f str = do + exts <- concat <$> many parseExtensions + let ns = Namespace (if NoTypeNamespace `elem` exts then Nothing else Just ExpLevel) (NoConstructorNamespace `notElem` exts) + whiteSpace + header <- optionMaybe $ do + modn <- reserved "module" *> moduleName + exps <- optionMaybe (parens $ commaSep $ parseExport ns) + reserved "where" + return (modn, exps) + let mkIDef _ n i h _ = (n, f i h) + where + f Nothing Nothing = ImportAllBut [] + f (Just h) Nothing = ImportAllBut h + f Nothing (Just i) = ImportJust i + idefs <- many $ + mkIDef <$ reserved "import" + <*> optionMaybe (reserved "qualified") + <*> moduleName + <*> optionMaybe (reserved "hiding" *> importlist) + <*> optionMaybe importlist + <*> optionMaybe (reserved "as" *> moduleName) + st <- getParserState + return Module + { extensions = exts + , moduleImports = [("Prelude", ImportAllBut []) | NoImplicitPrelude `notElem` exts] ++ idefs + , moduleExports = join $ snd <$> header + , definitions = \ge -> first (show +++ id) $ flip runReader (ge, ns) . runWriterT $ runPT' (parseDefs SLabelEnd indentMany' <* eof) st + , sourceCode = str + } + +parseLC :: MonadError ErrorMsg m => FilePath -> String -> m Module +parseLC f str + = either (throwError . ErrorMsg . show) return + . flip runReader (error "globalenv used", Namespace (Just ExpLevel) True) + . fmap fst . runWriterT + . runParserT'' (parseModule f str) f + . mkStream + $ str + +-------------------------------------------------------------------------------- pretty print + +instance Up a => PShow (SExp' a) where + pShowPrec _ = showDoc_ . sExpDoc + +type Doc = NameDB PrecString + +-- name De Bruijn indices +type NameDB a = StateT [String] (Reader [String]) a + +showDoc :: Doc -> String +showDoc = str . flip runReader [] . flip evalStateT (flip (:) <$> iterate ('\'':) "" <*> ['a'..'z']) + +showDoc_ :: Doc -> P.Doc +showDoc_ = text . str . flip runReader [] . flip evalStateT (flip (:) <$> iterate ('\'':) "" <*> ['a'..'z']) + +sExpDoc :: Up a => SExp' a -> Doc +sExpDoc = \case + SGlobal (_,s) -> pure $ shAtom s + SAnn a b -> shAnn ":" False <$> sExpDoc a <*> sExpDoc b + TyType a -> shApp Visible (shAtom "tyType") <$> sExpDoc a + SApp _ h a b -> shApp h <$> sExpDoc a <*> sExpDoc b + Wildcard t -> shAnn ":" True (shAtom "_") <$> sExpDoc t + SBind _ h _ a b -> join $ shLam (used 0 b) h <$> sExpDoc a <*> pure (sExpDoc b) + SLet _ a b -> shLet_ (sExpDoc a) (sExpDoc b) + STyped _ _{-(e,t)-} -> pure $ shAtom "<<>>" -- todo: expDoc e + SVar _ i -> shAtom <$> shVar i + SLit _ l -> pure $ shAtom $ show l + +shVar i = asks lookupVarName where + lookupVarName xs | i < length xs && i >= 0 = xs !! i + lookupVarName _ = "V" ++ show i + +newName = gets head <* modify tail + +shLet i a b = shAtom <$> shVar i >>= \i' -> local (dropNth i) $ shLam' <$> (cpar . shLet' (fmap inBlue i') <$> a) <*> b +shLet_ a b = newName >>= \i -> shLam' <$> (cpar . shLet' (shAtom i) <$> a) <*> local (i:) b +shLam used h a b = newName >>= \i -> + let lam = case h of + BPi _ -> shArr + _ -> shLam' + p = case h of + BMeta -> cpar . shAnn ":" True (shAtom $ inBlue i) + BLam h -> vpar h + BPi h -> vpar h + vpar Hidden = brace . shAnn ":" True (shAtom $ inGreen i) + vpar Visible = ann (shAtom $ inGreen i) + ann | used = shAnn ":" False + | otherwise = const id + in lam (p a) <$> local (i:) b + +----------------------------------------- + +data PS a = PS Prec a deriving (Functor) +type PrecString = PS String + +getPrec (PS p _) = p +prec i s = PS i (s i) +str (PS _ s) = s + +lpar, rpar :: PrecString -> Prec -> String +lpar (PS i s) j = par (i >. j) s where + PrecLam >. i = i > PrecAtom' + i >. PrecLam = i >= PrecArr + PrecApp >. PrecApp = False + i >. j = i >= j +rpar (PS i s) j = par (i >. j) s where + PrecLam >. PrecLam = False + PrecLam >. i = i > PrecAtom' + PrecArr >. PrecArr = False + PrecAnn >. PrecAnn = False + i >. j = i >= j + +par True s = "(" ++ s ++ ")" +par False s = s + +isAtom = (==PrecAtom) . getPrec +isAtom' = (<=PrecAtom') . getPrec + +shAtom = PS PrecAtom +shAtom' = PS PrecAtom' +shAnn _ True x y | str y `elem` ["Type", inGreen "Type"] = x +shAnn s simp x y | isAtom x && isAtom y = shAtom' $ str x <> s <> str y +shAnn s simp x y = prec PrecAnn $ lpar x <> " " <> const s <> " " <> rpar y +shApp Hidden x y = prec PrecApp $ lpar x <> " " <> const (str $ brace y) +shApp h x y = prec PrecApp $ lpar x <> " " <> rpar y +shArr x y | isAtom x && isAtom y = shAtom' $ str x <> "->" <> str y +shArr x y = prec PrecArr $ lpar x <> " -> " <> rpar y +shCstr x y | isAtom x && isAtom y = shAtom' $ str x <> "~" <> str y +shCstr x y = prec PrecEq $ lpar x <> " ~ " <> rpar y +shLet' x y | isAtom x && isAtom y = shAtom' $ str x <> ":=" <> str y +shLet' x y = prec PrecLet $ lpar x <> " := " <> rpar y +shLam' x y | PrecLam <- getPrec y = prec PrecLam $ "\\" <> lpar x <> " " <> pure (dropC $ str y) + where + dropC (ESC s (dropC -> x)) = ESC s x + dropC (x: xs) = xs +shLam' x y | isAtom x && isAtom y = shAtom' $ "\\" <> str x <> "->" <> str y +shLam' x y = prec PrecLam $ "\\" <> lpar x <> " -> " <> rpar y +brace s = shAtom $ "{" <> str s <> "}" +cpar s | isAtom' s = s -- TODO: replace with lpar, rpar +cpar s = shAtom $ par True $ str s +epar = fmap underlined + +instance IsString (Prec -> String) where fromString = const + diff --git a/src/LambdaCube/Compiler/Pretty.hs b/src/LambdaCube/Compiler/Pretty.hs new file mode 100644 --- /dev/null +++ b/src/LambdaCube/Compiler/Pretty.hs @@ -0,0 +1,146 @@ +{-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE NoMonomorphismRestriction #-} +{-# LANGUAGE LambdaCase #-} +{-# LANGUAGE PatternSynonyms #-} +{-# LANGUAGE ViewPatterns #-} +{-# LANGUAGE FlexibleContexts #-} +module LambdaCube.Compiler.Pretty + ( module LambdaCube.Compiler.Pretty + , Doc + , (<+>), (), (<$$>) + , hsep, hcat, vcat + , punctuate + , tupled, braces, parens + , text + ) where + +import Data.Set (Set) +import qualified Data.Set as Set +import Data.Map (Map) +import qualified Data.Map as Map +import Control.Monad.Except +import Debug.Trace + +import Text.PrettyPrint.Compact + +-------------------------------------------------------------------------------- + +--instance IsString Doc where fromString = text + +class PShow a where + pShowPrec :: Int -> a -> Doc + +pShow = pShowPrec (-2) +ppShow = show . pShow + +ppShow' = show + + +{- +prec 0: no outer parens needed +prec 10: argument of a function + + +f x (g y) + + +-} + +-------------------------------------------------------------------------------- + +pParens p x + | p = tupled [x] + | otherwise = x + +pOp i j k sep p a b = pParens (p >= i) $ pShowPrec j a <+> sep <+> pShowPrec k b +pOp' i j k sep p a b = pParens (p >= i) $ pShowPrec j a sep <+> pShowPrec k b + +pInfixl i = pOp i (i-1) i +pInfixr i = pOp i i (i-1) +pInfixr' i = pOp' i i (i-1) +pInfix i = pOp i i i + +pTyApp = pInfixl 10 "@" +pApps p x [] = pShowPrec p x +pApps p x xs = pParens (p > 9) $ hsep $ pShowPrec 9 x: map (pShowPrec 10) xs +pApp p a b = pApps p a [b] + +showRecord = braces . hsep . punctuate (pShow ',') . map (\(a, b) -> pShow a <> ":" <+> pShow b) + +-------------------------------------------------------------------------------- + +instance PShow Bool where + pShowPrec p b = if b then "True" else "False" + +instance (PShow a, PShow b) => PShow (a, b) where + pShowPrec p (a, b) = tupled [pShow a, pShow b] + +instance (PShow a, PShow b, PShow c) => PShow (a, b, c) where + pShowPrec p (a, b, c) = tupled [pShow a, pShow b, pShow c] + +instance PShow a => PShow [a] where + pShowPrec p = brackets . sep . punctuate comma . map pShow + +instance PShow a => PShow (Maybe a) where + pShowPrec p = \case + Nothing -> "Nothing" + Just x -> "Just" <+> pShow x + +instance PShow a => PShow (Set a) where + pShowPrec p = pShowPrec p . Set.toList + +instance (PShow s, PShow a) => PShow (Map s a) where + pShowPrec p = braces . vcat . map (\(k, t) -> pShow k <> colon <+> pShow t) . Map.toList + +instance (PShow a, PShow b) => PShow (Either a b) where + pShowPrec p = either (("Left" <+>) . pShow) (("Right" <+>) . pShow) + +instance PShow Doc where + pShowPrec p x = x + +instance PShow Int where pShowPrec _ = int +instance PShow Integer where pShowPrec _ = integer +instance PShow Double where pShowPrec _ = double +instance PShow Char where pShowPrec _ = char +instance PShow () where pShowPrec _ _ = "()" + + +-------------------------------------------------------------------------------- ANSI terminal colors + +pattern ESC a b <- (splitESC -> Just (a, b)) where ESC a b | 'm' `notElem` a = "\ESC[" ++ a ++ "m" ++ b + +splitESC ('\ESC':'[': (span (/='m') -> (a, c: b))) | c == 'm' = Just (a, b) +splitESC _ = Nothing + +withEsc i s = ESC (show i) $ s ++ ESC "" "" + +inGreen = withEsc 32 +inBlue = withEsc 34 +inRed = withEsc 31 +underlined = withEsc 47 + +removeEscs :: String -> String +removeEscs (ESC _ cs) = removeEscs cs +removeEscs (c: cs) = c: removeEscs cs +removeEscs [] = [] + +correctEscs :: String -> String +correctEscs = (++ "\ESC[K") . f ["39","49"] where + f acc (ESC i@(_:_) cs) = esc (i /= head acc) i $ f (i: acc) cs + f (a: acc) (ESC "" cs) = esc (a /= head acc) (compOld (cType a) acc) $ f acc cs + f acc (c: cs) = c: f acc cs + f acc [] = [] + + esc b i = if b then ESC i else id + compOld x xs = head $ filter ((== x) . cType) xs + + cType n + | "30" <= n && n <= "39" = 0 + | "40" <= n && n <= "49" = 1 + | otherwise = 2 + +putStrLn_ = putStrLn . correctEscs +error_ = error . correctEscs +trace_ = trace . correctEscs +throwError_ = throwError . correctEscs + diff --git a/test/UnitTests.hs b/test/UnitTests.hs new file mode 100644 --- /dev/null +++ b/test/UnitTests.hs @@ -0,0 +1,135 @@ +{-# LANGUAGE StandaloneDeriving #-} +module Main where + +import Data.Monoid +import Text.Parsec.Pos (SourcePos(..), newPos, sourceName, sourceLine, sourceColumn) +import qualified Data.Map as Map +import qualified Data.Set as Set + +import Test.QuickCheck +import Test.QuickCheck.Property +import Test.Tasty +import Test.Tasty.QuickCheck + +import LambdaCube.Compiler.Infer + +----------------------------------------------------------------- Main + +-- Usage: ":main --quickcheck-max-size 30 --quickcheck-tests 100" +main = defaultMain $ testGroup "Compiler" + [ testGroup "Infer" $ concat [ + monoidTestProperties "SI" (arbitrary :: Gen SI) + , monoidTestProperties "Infos" (arbitrary :: Gen Infos) + , monoidTestProperties "MaxDB" (arbitrary :: Gen MaxDB) + ] + ] + +----------------------------------------------------------------- Arbitraries + +-- SourcePos + +instance Arbitrary SourcePos where + arbitrary = newPos <$> arbitrary <*> arbitrary <*> arbitrary + shrink pos + | n <- sourceName pos, l <- sourceLine pos, c <- sourceColumn pos + = [newPos n' l' c' | n' <- shrink n, l' <- shrink l, c' <- shrink c] + -- TODO: Diagonalize shrink + +-- Range + +instance Arbitrary Range where + arbitrary = Range <$> arbitrary <*> arbitrary + shrink (Range a b) = Range <$> shrink a <*> shrink b + +deriving instance Show Range + +-- SI + +instance Arbitrary SI where + arbitrary = oneof [NoSI . Set.fromList <$> arbitrary, RangeSI <$> arbitrary] + shrink (NoSI ds) = [] + shrink (RangeSI r) = mempty: map RangeSI (shrink r) + +instance MonoidEq SI where + NoSI a =::= NoSI b = a == b + RangeSI a =::= RangeSI b = a == b + +instance TestShow SI where + testShow (NoSI a) = "NoSI " ++ show a + testShow (RangeSI a) = "RangeSI " ++ show a + +-- Infos + +instance Arbitrary Infos where + arbitrary = Infos . Map.fromList <$> arbitrary + shrink (Infos m) = map (Infos . Map.fromList . shrink) $ Map.toList m + +deriving instance Eq Infos + +instance MonoidEq Infos where + (=::=) = (==) + +instance TestShow Infos where + testShow (Infos i) = "Infos " ++ show i + +-- MaxDB + +instance Arbitrary MaxDB where + arbitrary = MaxDB <$> fmap (fmap abs) arbitrary + shrink (MaxDB m) = map MaxDB $ shrink m + +instance MonoidEq MaxDB where + MaxDB (Just n) =::= MaxDB (Just m) = n == m + MaxDB Nothing =::= MaxDB Nothing = True + MaxDB (Just 0) =::= MaxDB Nothing = True + MaxDB Nothing =::= MaxDB (Just 0) = True + _ =::= _ = False + +instance TestShow MaxDB where + testShow (MaxDB a) = "MaxDB " ++ show a + +----------------------------------------------------------------- Test building blocks + +class Monoid m => MonoidEq m where + (=::=) :: m -> m -> Bool + +infix 4 =::= + +monoidTestProperties name gen = + [ testProperty (name ++ " monoid left identity") (propMonoidLeftIdentity gen) + , testProperty (name ++ " monoid right identity") (propMonoidRightIdentity gen) + , testProperty (name ++ " monoid associativity") (propMonoidAssociativity gen) + ] + +----------------------------------------------------------------- Properties + +-- * Monoid + +propMonoidLeftIdentity :: (MonoidEq m, TestShow m) => Gen m -> Property +propMonoidLeftIdentity gen = forAll' gen (\x -> x =*= mempty <> x) + +propMonoidRightIdentity :: (MonoidEq m, TestShow m) => Gen m -> Property +propMonoidRightIdentity gen = forAll' gen (\x -> x =*= x <> mempty) + +propMonoidAssociativity :: (Arbitrary m, MonoidEq m, TestShow m) => Gen m -> Property +propMonoidAssociativity gen = + forAll' gen $ \x -> forAll' gen $ \y -> forAll' gen $ \z -> + (x <> y) <> z =*= x <> (y <> z) + +----------------------------------------------------------------- Tools + +class TestShow t where + testShow :: t -> String + +-- | Like '=::=', but prints a counterexample when it fails. +infix 4 =*= +(=*=) :: (MonoidEq a, TestShow a) => a -> a -> Property +x =*= y = + counterexample (testShow x ++ " /= " ++ testShow y) (x =::= y) + +forAll' :: (TestShow a, Testable prop) + => Gen a -> (a -> prop) -> Property +forAll' gen pf = + MkProperty $ + gen >>= \x -> + unProperty (counterexample (testShow x) (pf x)) diff --git a/test/runTests.hs b/test/runTests.hs new file mode 100644 --- /dev/null +++ b/test/runTests.hs @@ -0,0 +1,248 @@ +{-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE LambdaCase #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE RecordWildCards #-} +module Main where + +import Data.List +import Data.Time.Clock +import Control.Applicative +import Control.Concurrent +import Control.Concurrent.Async +import Control.Monad +import Control.Monad.Reader +import Control.Exception hiding (catch) +import Control.Monad.Trans.Control +import Control.DeepSeq +import System.Exit +import System.Directory +import System.FilePath +import System.IO +import Options.Applicative + +import qualified Data.Text as T +import qualified Data.Text.IO as TIO +import Text.Printf + +import LambdaCube.Compiler + +------------------------------------------ utils + +readFileStrict :: FilePath -> IO String +readFileStrict = fmap T.unpack . TIO.readFile + +getDirectoryContentsRecursive path = do + l <- map (path ) . filter (`notElem` [".",".."]) <$> getDirectoryContents path + -- ignore sub directories that name include .ignore + (++) + <$> (filter ((".lc" ==) . takeExtension) <$> filterM doesFileExist l) + <*> (fmap concat . mapM getDirectoryContentsRecursive . filter ((".ignore" `notElem`) . takeExtensions') =<< filterM doesDirectoryExist l) + +takeExtensions' :: FilePath -> [String] +takeExtensions' fn = case splitExtension fn of + (_, "") -> [] + (fn', ext) -> ext: takeExtensions' fn' + +getYNChar = do + c <- getChar + case c of + _ | c `elem` ("yY\n" :: String) -> putChar '\n' >> return True + | c `elem` ("nN\n" :: String) -> putChar '\n' >> return False + | otherwise -> getYNChar + +showTime delta + | t > 1e-1 = printf "%.3fs" t + | t > 1e-3 = printf "%.1fms" (t/1e-3) + | otherwise = printf "%.0fus" (t/1e-6) + where + t = realToFrac delta :: Double + +timeOut :: MonadBaseControl IO m => NominalDiffTime -> a -> m a -> m (NominalDiffTime, a) +timeOut dt d m = + control $ \runInIO -> + race' (runInIO $ timeDiff m) + (runInIO $ timeDiff $ liftIO (threadDelay $ round $ dt * 1000000) >> return d) + where + liftIO = liftBaseWith . const + race' a b = either id id <$> race a b + timeDiff m = (\s x e -> (diffUTCTime e s, x)) + <$> liftIO getCurrentTime + <*> m + <*> liftIO getCurrentTime + +------------------------------------------ + +testDataPath = "./testdata" + +data Config + = Config + { cfgVerbose :: Bool + , cfgReject :: Bool + , cfgTimeout :: NominalDiffTime + , cfgIgnore :: [String] + } deriving Show + +arguments :: Parser (Config, [String]) +arguments = + (,) <$> (Config <$> switch (short 'v' <> long "verbose" <> help "Verbose output during test runs") + <*> switch (short 'r' <> long "reject" <> help "Reject test cases with missing, new or different .out files") + <*> option (realToFrac <$> (auto :: ReadM Double)) (value 60 <> short 't' <> long "timeout" <> help "Timeout for tests in seconds") + <*> option ((:[]) <$> eitherReader Right) (value [] <> short 'i' <> long "ignore" <> help "Ignore test") + ) + <*> many (strArgument idm) + +data Res = Passed | Accepted | New | TimedOut | Rejected | Failed | ErrorCatched + deriving (Eq, Ord, Show) + +showRes = \case + ErrorCatched -> "crashed test" + Failed -> "failed test" + Rejected -> "rejected result" + TimedOut -> "timed out test" + New -> "new result" + Accepted -> "accepted result" + Passed -> "passed test" + +instance NFData Res where + rnf a = a `seq` () + +erroneous = (>= TimedOut) + +isWip = (".wip" `elem`) . takeExtensions' +isReject = (".reject" `elem`) . takeExtensions' + +main :: IO () +main = do + hSetBuffering stdout NoBuffering + hSetBuffering stdin NoBuffering + (cfg@Config{..}, samplesToTest) <- execParser $ + info (helper <*> arguments) + (fullDesc <> header "LambdaCube 3D compiler test suite") + + testData <- getDirectoryContentsRecursive testDataPath + -- select test set: all test or user selected + let (ignoredTests, testSet) + = partition (\d -> any (`isInfixOf` d) cfgIgnore) + . map head . group . sort + $ [d | d <- testData, s <- if null samplesToTest then [""] else samplesToTest, s `isInfixOf` d] + + unless (null ignoredTests) $ do + putStrLn $ "------------------------------------ Ignoring " ++ show (length ignoredTests) ++ " tests" + forM_ ignoredTests putStrLn + + when (null testSet) $ do + putStrLn $ "test files not found: " ++ show samplesToTest + exitFailure + + putStrLn $ "------------------------------------ Running " ++ show (length testSet) ++ " tests" + + (Right resultDiffs, _) + <- runMM (ioFetch [".", testDataPath]) + $ forM (zip [1..] testSet) $ doTest cfg + + let sh :: (FilePath -> Res -> Bool) -> String -> [String] + sh p b = [ (if any (\(ty, s) -> erroneous ty && not (isWip s)) ss then "!" else "") + ++ show noOfResult ++ " " + ++ pad 10 (b ++ plural ++ ": ") ++ "\n" + ++ unlines (map snd ss) + | not $ null ss ] + where + ss = [(ty, s) | ((_, ty), s) <- zip resultDiffs testSet, p s ty] + noOfResult = length ss + plural = ['s' | noOfResult > 1] + + putStrLn "------------------------------------ Summary" + putStrLn $ unlines $ reverse $ + concat [ sh (\s ty -> ty == x && p s) (w ++ showRes x) + | (w, p) <- [("", not . isWip), ("wip ", isWip)] + , x <- [ErrorCatched, Failed, Rejected, TimedOut, New, Accepted] + ] + ++ sh (\s ty -> ty == Passed && isWip s) "wip passed test" + + putStrLn $ "Overall time: " ++ showTime (sum $ map fst resultDiffs) + + when (or [erroneous r | ((_, r), f) <- zip resultDiffs testSet, not $ isWip f]) exitFailure + putStrLn "All OK" + when (or [erroneous r | ((_, r), f) <- zip resultDiffs testSet, isWip f]) $ + putStrLn "Only work in progress test cases are failing." + +doTest Config{..} (i, fn) = do + liftIO $ putStr $ fn ++ " " + (runtime, res) <- mapMMT (timeOut cfgTimeout $ Left ("!Timed Out", TimedOut)) + $ catchErr (\e -> return $ Left (tab "!Crashed" e, ErrorCatched)) + $ liftIO . evaluate =<< (force <$> action) + liftIO $ putStr $ "(" ++ showTime runtime ++ ")" ++ " " + (msg, result) <- case res of + Left x -> return x + Right (op, x) -> liftIO $ compareResult (pad 15 op) (dropExtension fn ++ ".out") x + liftIO $ putStrLn msg + return (runtime, result) + where + n = dropExtension fn + + action = f <$> (Right <$> getDef n "main" Nothing) `catchMM` (return . Left . show) + + f | not $ isReject fn = \case + Left e -> Left (tab "!Failed" e, Failed) + Right (fname, Left e, i) + -> Right ("typechecked module" + , unlines $ e: "tooltips:": [ ppShow r ++ " " ++ intercalate " | " m + | (r, m) <- listInfos i]) + Right (fname, Right (e, te), i) + | True <- i `deepseq` False -> error "impossible" + | te == outputType -> Right ("compiled pipeline", show $ compilePipeline OpenGL33 (e, te)) + | e == trueExp -> Right ("reducted main", ppShow e) + | te == boolType -> Left (tab "!Failed" $ "main should be True but it is \n" ++ ppShow e, Failed) + | otherwise -> Right ("reduced main " ++ ppShow te, ppShow e) + | otherwise = \case + Left e -> Right ("error message", e) + Right _ -> Left (tab "!Failed" "failed to catch error", Failed) + + tab msg + | isWip fn && cfgReject = const msg + | otherwise = ((msg ++ "\n") ++) . unlines . map (" " ++) . lines + + compareResult msg ef e = doesFileExist ef >>= \b -> case b of + False + | cfgReject -> return ("!Missing .out file", Rejected) + | otherwise -> writeFile ef e >> return ("New .out file", New) + True -> do + e' <- readFileStrict ef + case map fst $ filter snd $ zip [0..] $ zipWith (/=) e e' ++ replicate (abs $ length e - length e') True of + [] -> return ("OK", Passed) + rs | cfgReject-> return ("!Different .out file", Rejected) + | otherwise -> do + printOldNew msg (showRanges ef rs e') (showRanges ef rs e) + putStrLn $ ef ++ " has changed." + putStr $ "Accept new " ++ msg ++ " (y/n)? " + c <- length e' `seq` getYNChar + if c + then writeFile ef e >> return ("Accepted .out file", Accepted) + else return ("!Rejected .out file", Rejected) + +printOldNew msg old new = do + putStrLn $ msg ++ " has changed." + putStrLn "------------------------------------------- Old" + putStrLn old + putStrLn "------------------------------------------- New" + putStrLn new + putStrLn "-------------------------------------------" + +pad n s = s ++ replicate (n - length s) ' ' + +limit :: String -> Int -> String -> String +limit msg n s = take n s ++ if null (drop n s) then "" else msg + +showRanges :: String -> [Int] -> String -> String +showRanges fname is e = (if head rs == 0 then "" else "...\n") + ++ limit ("\n... (see " ++ fname ++ " for more differences)") 140000 (intercalate "\n...\n" $ f (zipWith (-) rs (0:rs)) e) + where + f :: [Int] -> String -> [String] + f (i:is) e = g is $ drop i e + f [] "" = [] + f [] _ = ["\n..."] + g (i:is) e = take i e: f is (drop i e) + rs = (head is - x) : concat [[a + x, b - x] | (a, b) <- zip is (tail is), a + y < b] ++ [last is + x] + x = 100000 + y = 3*x + diff --git a/tool/Compiler.hs b/tool/Compiler.hs new file mode 100644 --- /dev/null +++ b/tool/Compiler.hs @@ -0,0 +1,38 @@ +{-# LANGUAGE RecordWildCards #-} +import Options.Applicative +import Data.Aeson +import qualified Data.ByteString.Lazy as B +import System.FilePath + +import LambdaCube.Compiler + +data Config + = Config + { srcName :: String + , backend :: Backend + , includePaths :: [FilePath] + } + +sample :: Parser Config +sample = Config + <$> argument str (metavar "SOURCE_FILE") + <*> flag OpenGL33 WebGL1 (long "webgl" <> help "generate WebGL 1.0 pipeline" ) + <*> pure ["."] + +main :: IO () +main = compile =<< execParser opts + where + opts = info (helper <*> sample) + ( fullDesc + <> progDesc "compiles LambdaCube graphics pipeline source to JSON IR" + <> header "LambdaCube 3D compiler" ) + +compile :: Config -> IO () +compile Config{..} = do + let dropExt n | takeExtension n == ".lc" = dropExtension n + dropExt n = n + baseName = dropExt srcName + pplRes <- compileMain includePaths backend baseName + case pplRes of + Left err -> putStrLn err + Right ppl -> B.writeFile (baseName <> ".json") $ encode ppl