lambdacube-compiler (empty) → 0.4.0.0
raw patch · 15 files changed
+6458/−0 lines, 15 filesdep +QuickCheckdep +aesondep +asyncsetup-changed
Dependencies added: QuickCheck, aeson, async, base, bytestring, containers, deepseq, directory, exceptions, filepath, indentation, lambdacube-compiler, lambdacube-ir, monad-control, mtl, optparse-applicative, parsec, pretty-compact, tasty, tasty-quickcheck, text, time, vector
Files
- LICENSE +30/−0
- Setup.hs +2/−0
- lambdacube-compiler.cabal +201/−0
- lc/Builtins.lc +572/−0
- lc/Internals.lc +133/−0
- lc/Prelude.lc +364/−0
- src/LambdaCube/Compiler.hs +209/−0
- src/LambdaCube/Compiler/CoreToIR.hs +1116/−0
- src/LambdaCube/Compiler/Infer.hs +1458/−0
- src/LambdaCube/Compiler/Lexer.hs +614/−0
- src/LambdaCube/Compiler/Parser.hs +1192/−0
- src/LambdaCube/Compiler/Pretty.hs +146/−0
- test/UnitTests.hs +135/−0
- test/runTests.hs +248/−0
- tool/Compiler.hs +38/−0
+ LICENSE view
@@ -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.
+ Setup.hs view
@@ -0,0 +1,2 @@+import Distribution.Simple+main = defaultMain
+ lambdacube-compiler.cabal view
@@ -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+
+ lc/Builtins.lc view
@@ -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`+
+ lc/Internals.lc view
@@ -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 :++
+ lc/Prelude.lc view
@@ -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)++
+ src/LambdaCube/Compiler.hs view
@@ -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+
+ src/LambdaCube/Compiler/CoreToIR.hs view
@@ -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+
+ src/LambdaCube/Compiler/Infer.hs view
@@ -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 -- <<e>> 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 -- __ <i := x>+ 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 "<<HERE>>"++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++
+ src/LambdaCube/Compiler/Lexer.hs view
@@ -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"+
+ src/LambdaCube/Compiler/Parser.hs view
@@ -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+
+ src/LambdaCube/Compiler/Pretty.hs view
@@ -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+
+ test/UnitTests.hs view
@@ -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))
+ test/runTests.hs view
@@ -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+
+ tool/Compiler.hs view
@@ -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