| Copyright | (c) Kimiyuki Onaka 2020 |
|---|---|
| License | Apache License 2.0 |
| Maintainer | kimiyuki95@gmail.com |
| Stability | experimental |
| Portability | portable |
| Safe Haskell | None |
| Language | Haskell2010 |
Jikka.Core.Language.Expr
Description
Expr module has the basic data types for our core language.
They are similar to the GHC Core language.
Synopsis
- newtype VarName = VarName String
- unVarName :: VarName -> String
- newtype TypeName = TypeName String
- unTypeName :: TypeName -> String
- data Type
- data DataStructure
- data Semigroup'
- data Builtin
- = Negate
- | Plus
- | Minus
- | Mult
- | FloorDiv
- | FloorMod
- | CeilDiv
- | CeilMod
- | JustDiv
- | Pow
- | Abs
- | Gcd
- | Lcm
- | Min2
- | Max2
- | Iterate
- | Not
- | And
- | Or
- | Implies
- | If
- | BitNot
- | BitAnd
- | BitOr
- | BitXor
- | BitLeftShift
- | BitRightShift
- | MatAp Integer Integer
- | MatZero Integer Integer
- | MatOne Integer
- | MatAdd Integer Integer
- | MatMul Integer Integer Integer
- | MatPow Integer
- | VecFloorMod Integer
- | MatFloorMod Integer Integer
- | ModNegate
- | ModPlus
- | ModMinus
- | ModMult
- | ModInv
- | ModPow
- | ModMatAp Integer Integer
- | ModMatAdd Integer Integer
- | ModMatMul Integer Integer Integer
- | ModMatPow Integer
- | Cons
- | Snoc
- | Foldl
- | Scanl
- | Build
- | Len
- | Map
- | Filter
- | At
- | SetAt
- | Elem
- | Sum
- | Product
- | ModSum
- | ModProduct
- | Min1
- | Max1
- | ArgMin
- | ArgMax
- | Gcd1
- | Lcm1
- | All
- | Any
- | Sorted
- | Reversed
- | Range1
- | Range2
- | Range3
- | Tuple
- | Proj Integer
- | LessThan
- | LessEqual
- | GreaterThan
- | GreaterEqual
- | Equal
- | NotEqual
- | Fact
- | Choose
- | Permute
- | MultiChoose
- | ConvexHullTrickInit
- | ConvexHullTrickGetMin
- | ConvexHullTrickInsert
- | SegmentTreeInitList Semigroup'
- | SegmentTreeGetRange Semigroup'
- | SegmentTreeSetPoint Semigroup'
- data Literal
- data Expr
- pattern Fun2Ty :: Type -> Type -> Type -> Type
- pattern Fun3Ty :: Type -> Type -> Type -> Type -> Type
- pattern Fun1STy :: Type -> Type
- pattern Fun2STy :: Type -> Type
- pattern Fun3STy :: Type -> Type
- pattern FunLTy :: Type -> Type
- vectorTy :: Integer -> Type
- matrixTy :: Integer -> Integer -> Type
- pattern UnitTy :: Type
- pattern ConvexHullTrickTy :: Type
- pattern SegmentTreeTy :: Semigroup' -> Type
- pattern LitInt' :: Integer -> Expr
- pattern Lit0 :: Expr
- pattern Lit1 :: Expr
- pattern Lit2 :: Expr
- pattern LitMinus1 :: Expr
- pattern LitBool' :: Bool -> Expr
- pattern LitTrue :: Expr
- pattern LitFalse :: Expr
- pattern Builtin :: Builtin -> Expr
- pattern Builtin1 :: Builtin -> Type -> Expr
- pattern Builtin2 :: Builtin -> Type -> Type -> Expr
- pattern App2 :: Expr -> Expr -> Expr -> Expr
- pattern App3 :: Expr -> Expr -> Expr -> Expr -> Expr
- pattern App4 :: Expr -> Expr -> Expr -> Expr -> Expr -> Expr
- pattern AppBuiltin1 :: Builtin -> Expr -> Expr
- pattern AppBuiltin11 :: Builtin -> Type -> Expr -> Expr
- pattern AppBuiltin2 :: Builtin -> Expr -> Expr -> Expr
- pattern AppBuiltin12 :: Builtin -> Type -> Expr -> Expr -> Expr
- pattern AppBuiltin22 :: Builtin -> Type -> Type -> Expr -> Expr -> Expr
- pattern AppBuiltin3 :: Builtin -> Expr -> Expr -> Expr -> Expr
- pattern AppBuiltin13 :: Builtin -> Type -> Expr -> Expr -> Expr -> Expr
- pattern AppBuiltin23 :: Builtin -> Type -> Type -> Expr -> Expr -> Expr -> Expr
- pattern AppBuiltin14 :: Builtin -> Type -> Type -> Expr -> Expr -> Expr -> Expr
- pattern Lam2 :: VarName -> Type -> VarName -> Type -> Expr -> Expr
- pattern Lam3 :: VarName -> Type -> VarName -> Type -> VarName -> Type -> Expr -> Expr
- data ToplevelExpr
- type Program = ToplevelExpr
Documentation
Instances
| Eq VarName Source # | |
| Data VarName Source # | |
Defined in Jikka.Core.Language.Expr Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> VarName -> c VarName # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c VarName # toConstr :: VarName -> Constr # dataTypeOf :: VarName -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c VarName) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c VarName) # gmapT :: (forall b. Data b => b -> b) -> VarName -> VarName # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> VarName -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> VarName -> r # gmapQ :: (forall d. Data d => d -> u) -> VarName -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> VarName -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> VarName -> m VarName # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> VarName -> m VarName # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> VarName -> m VarName # | |
| Ord VarName Source # | |
Defined in Jikka.Core.Language.Expr | |
| Read VarName Source # | |
| Show VarName Source # | |
| IsString VarName Source # | |
Defined in Jikka.Core.Language.Expr Methods fromString :: String -> VarName # | |
Instances
| Eq TypeName Source # | |
| Data TypeName Source # | |
Defined in Jikka.Core.Language.Expr Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> TypeName -> c TypeName # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c TypeName # toConstr :: TypeName -> Constr # dataTypeOf :: TypeName -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c TypeName) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c TypeName) # gmapT :: (forall b. Data b => b -> b) -> TypeName -> TypeName # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> TypeName -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> TypeName -> r # gmapQ :: (forall d. Data d => d -> u) -> TypeName -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> TypeName -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> TypeName -> m TypeName # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> TypeName -> m TypeName # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> TypeName -> m TypeName # | |
| Ord TypeName Source # | |
Defined in Jikka.Core.Language.Expr | |
| Read TypeName Source # | |
| Show TypeName Source # | |
| IsString TypeName Source # | |
Defined in Jikka.Core.Language.Expr Methods fromString :: String -> TypeName # | |
unTypeName :: TypeName -> String Source #
Type represents the types of our core language. This is similar to the Type of GHC Core.
See also commentarycompilertype-type.
\[ \newcommand\int{\mathbf{int}} \newcommand\bool{\mathbf{bool}} \newcommand\list{\mathbf{list}} \begin{array}{rl} \tau ::= & \alpha \\ \vert & \int \\ \vert & \bool \\ \vert & \list(\tau) \\ \vert & \tau \times \tau \times \dots \times \tau \\ \vert & \tau \to \tau \\ \vert & \mathrm{data\_structure} \end{array} \]
Constructors
| VarTy TypeName | |
| IntTy | |
| BoolTy | |
| ListTy Type | |
| TupleTy [Type] | |
| FunTy Type Type | |
| DataStructureTy DataStructure |
Instances
| Eq Type Source # | |
| Data Type Source # | |
Defined in Jikka.Core.Language.Expr Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Type -> c Type # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Type # dataTypeOf :: Type -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Type) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Type) # gmapT :: (forall b. Data b => b -> b) -> Type -> Type # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Type -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Type -> r # gmapQ :: (forall d. Data d => d -> u) -> Type -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> Type -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> Type -> m Type # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Type -> m Type # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Type -> m Type # | |
| Ord Type Source # | |
| Read Type Source # | |
| Show Type Source # | |
data DataStructure Source #
Constructors
| ConvexHullTrick | |
| SegmentTree Semigroup' |
Instances
data Semigroup' Source #
Instances
Constructors
| Negate | \(: \int \to \int\) |
| Plus | \(: \int \to \int \to \int\) |
| Minus | \(: \int \to \int \to \int\) |
| Mult | \(: \int \to \int \to \int\) |
| FloorDiv | \(: \int \to \int \to \int\) |
| FloorMod | \(: \int \to \int \to \int\) |
| CeilDiv | \(: \int \to \int \to \int\) |
| CeilMod | \(: \int \to \int \to \int\) |
| JustDiv | divison which has no remainder \(: \int \to \int \to \int\) |
| Pow | \(: \int \to \int \to \int\) |
| Abs | \(: \int \to \int\) |
| Gcd | \(: \int \to \int \to \int\) |
| Lcm | \(: \int \to \int \to \int\) |
| Min2 | \(: \forall \alpha. \alpha \to \alpha \to \alpha\) |
| Max2 | \(: \forall \alpha. \alpha \to \alpha \to \alpha\) |
| Iterate | iterated application \((\lambda k f x. f^k(x)): \forall \alpha. \int \to (\alpha \to \alpha) \to \alpha \to \alpha\) |
| Not | \(: \bool \to \bool\) |
| And | \(: \bool \to \bool \to \bool\) |
| Or | \(: \bool \to \bool \to \bool\) |
| Implies | \(: \bool \to \bool \to \bool\) |
| If | \(: \forall \alpha. \bool \to \alpha \to \alpha \to \alpha\) |
| BitNot | \(: \int \to \int\) |
| BitAnd | \(: \int \to \int \to \int\) |
| BitOr | \(: \int \to \int \to \int\) |
| BitXor | \(: \int \to \int \to \int\) |
| BitLeftShift | \(: \int \to \int \to \int\) |
| BitRightShift | \(: \int \to \int \to \int\) |
| MatAp Integer Integer | matrix application \(: \int^{H \times W} \to \int^W \to \int^H\) |
| MatZero Integer Integer | zero matrix \(: \to \int^{h \times w}\) |
| MatOne Integer | unit matrix \(: \to \int^{n \times n}\) |
| MatAdd Integer Integer | matrix addition \(: \int^{H \times W} \to \int^{H \times W} \to \int^{H \times W}\) |
| MatMul Integer Integer Integer | matrix multiplication \(: \int^{H \times n} \to \int^{n \times W} \to \int^{H \times W}\) |
| MatPow Integer | matrix power \(: \int^{n \times n} \to \int \to \int^{n \times n}\) |
| VecFloorMod Integer | vector point-wise floor-mod \(: \int^{n} \to \int \to \int^{n}\) |
| MatFloorMod Integer Integer | matrix point-wise floor-mod \(: \int^{H \times W} \to \int \to \int^{H \times W}\) |
| ModNegate | \(: \int \to \int \to \int\) |
| ModPlus | \(: \int \to \int \to \int \to \int\) |
| ModMinus | \(: \int \to \int \to \int \to \int\) |
| ModMult | \(: \int \to \int \to \int \to \int\) |
| ModInv | \(: \int \to \int \to \int\) |
| ModPow | \(: \int \to \int \to \int \to \int\) |
| ModMatAp Integer Integer | matrix application \(: \int^{H \times W} \to \int^W \to \int \to \int^H\) |
| ModMatAdd Integer Integer | matrix addition \(: \int^{H \times W} \to \int^{H \times W} \to \int \to \int^{H \times W}\) |
| ModMatMul Integer Integer Integer | matrix multiplication \(: \int^{H \times n} \to \int^{n \times W} \to \int \to \int^{H \times W}\) |
| ModMatPow Integer | matrix power \(: \int^{n \times n} \to \int \to \int^{n \times n}\) |
| Cons | \(: \forall \alpha. \alpha \to \list(\alpha) \to \list(\alpha)\) |
| Snoc | \(: \forall \alpha. \list(alpha) \to \alpha \to \list(\alpha)\) |
| Foldl | \(: \forall \alpha \beta. (\beta \to \alpha \to \beta) \to \beta \to \list(\alpha) \to \beta\) |
| Scanl | \(: \forall \alpha \beta. (\beta \to \alpha \to \beta) \to \beta \to \list(\alpha) \to \list(\beta)\) |
| Build | \(\lambda f a n.\) repeat |
| Len | \(: \forall \alpha. \list(\alpha) \to \int\) |
| Map | \(: \forall \alpha \beta. (\alpha \to \beta) \to \list(\alpha) \to \list(\beta)\) |
| Filter | \(: \forall \alpha \beta. (\alpha \to \bool) \to \list(\alpha) \to \list(\beta)\) |
| At | \(: \forall \alpha. \list(\alpha) \to \int \to \alpha\) |
| SetAt | \(: \forall \alpha. \list(\alpha) \to \int \to \alpha \to \list(\alpha)\) |
| Elem | \(: \forall \alpha. \alpha \to \list(\alpha) \to \bool\) |
| Sum | \(: \list(\int) \to \int\) |
| Product | \(: \list(\int) \to \int\) |
| ModSum | \(: \list(\int) \to \int \to \int\) |
| ModProduct | \(: \list(\int) \to \int \to \int\) |
| Min1 | \(: \forall \alpha. \list(\alpha) \to \alpha\) |
| Max1 | \(: \forall \alpha. \list(\alpha) \to \alpha\) |
| ArgMin | \(: \forall \alpha. \list(\alpha) \to \int\) |
| ArgMax | \(: \forall \alpha. \list(\alpha) \to \int\) |
| Gcd1 | \(: \list(\int) \to \int\) |
| Lcm1 | \(: \list(\int) \to \int\) |
| All | \(: \list(\bool) \to \bool\) |
| Any | \(: \list(\bool) \to \bool\) |
| Sorted | \(: \forall \alpha. \list(\alpha) \to \list(\alpha)\) |
| Reversed | \(: \forall \alpha. \list(\alpha) \to \list(\alpha)\) |
| Range1 | \(: \int \to \list(\int)\) |
| Range2 | \(: \int \to \int \to \list(\int)\) |
| Range3 | \(: \int \to \int \to \int \to \list(\int)\) |
| Tuple | \(: \forall \alpha_0 \alpha_1 \dots \alpha _ {n - 1}. \alpha_0 \to \dots \to \alpha _ {n - 1} \to \alpha_0 \times \dots \times \alpha _ {n - 1}\) |
| Proj Integer | \(: \forall \alpha_0 \alpha_1 \dots \alpha _ {n - 1}. \alpha_0 \times \dots \times \alpha _ {n - 1} \to \alpha_i\)
|
| LessThan | \(: \forall \alpha. \alpha \to \alpha \to \bool\) |
| LessEqual | \(: \forall \alpha. \alpha \to \alpha \to \bool\) |
| GreaterThan | \(: \forall \alpha. \alpha \to \alpha \to \bool\) |
| GreaterEqual | \(: \forall \alpha. \alpha \to \alpha \to \bool\) |
| Equal | \(: \forall \alpha. \alpha \to \alpha \to \bool\) |
| NotEqual | \(: \forall \alpha. \alpha \to \alpha \to \bool\) |
| Fact | \(: \int \to \int\) |
| Choose | \(: \int \to \int \to \int\) |
| Permute | \(: \int \to \int \to \int\) |
| MultiChoose | \(: \int \to \int \to \int\) |
| ConvexHullTrickInit | \(: \mathrm{convex\_hull\_trick}\) |
| ConvexHullTrickGetMin | \(: \mathrm{convex\_hull\_trick} \to \int \to \int\) |
| ConvexHullTrickInsert | \(: \mathrm{convex\_hull\_trick} \to \int \to \int \to \mathrm{convex\_hull\_trick}\) |
| SegmentTreeInitList Semigroup' | \(: \list(S) \to \mathrm{segment\_tree}(S)\) for a semigroup (S) |
| SegmentTreeGetRange Semigroup' | \(: \mathrm{segment\_tree}(S) \to \int \to \int \to S\) for a semigroup (S) |
| SegmentTreeSetPoint Semigroup' | \(: \mathrm{segment\_tree}(S) \to \int \to S \to \mathrm{segment\_tree}(S)\) for a semigroup (S) |
Instances
| Eq Builtin Source # | |
| Data Builtin Source # | |
Defined in Jikka.Core.Language.Expr Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Builtin -> c Builtin # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Builtin # toConstr :: Builtin -> Constr # dataTypeOf :: Builtin -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Builtin) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Builtin) # gmapT :: (forall b. Data b => b -> b) -> Builtin -> Builtin # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Builtin -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Builtin -> r # gmapQ :: (forall d. Data d => d -> u) -> Builtin -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> Builtin -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> Builtin -> m Builtin # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Builtin -> m Builtin # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Builtin -> m Builtin # | |
| Ord Builtin Source # | |
Defined in Jikka.Core.Language.Expr | |
| Read Builtin Source # | |
| Show Builtin Source # | |
Constructors
| LitBuiltin Builtin [Type] | |
| LitInt Integer | \(: \forall \alpha. \int\) |
| LitBool Bool | \(: \forall \alpha. \bool\) |
| LitNil Type | \(: \forall \alpha. \list(\alpha)\) |
| LitBottom Type String | \(: \bot : \forall \alpha. \alpha\). The second argument is its error message. |
Instances
| Eq Literal Source # | |
| Data Literal Source # | |
Defined in Jikka.Core.Language.Expr Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Literal -> c Literal # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Literal # toConstr :: Literal -> Constr # dataTypeOf :: Literal -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Literal) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Literal) # gmapT :: (forall b. Data b => b -> b) -> Literal -> Literal # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Literal -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Literal -> r # gmapQ :: (forall d. Data d => d -> u) -> Literal -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> Literal -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> Literal -> m Literal # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Literal -> m Literal # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Literal -> m Literal # | |
| Ord Literal Source # | |
Defined in Jikka.Core.Language.Expr | |
| Read Literal Source # | |
| Show Literal Source # | |
Expr represents the exprs of our core language. This is similar to the Expr of GHC Core.
See also commentarycompilercore-syn-type.
\[ \begin{array}{rl} e ::= & x \\ \vert & \mathrm{literal}\ldots \\ \vert & e_0(e_1, e_2, \dots, e_n) \\ \vert & \lambda ~ x_0\colon \tau_0, x_1\colon \tau_1, \dots, x_{n-1}\colon \tau_{n-1}. ~ e \\ \vert & \mathbf{let} ~ x\colon \tau = e_1 ~ \mathbf{in} ~ e_2 \\ \vert & \mathbf{assert} ~ e_1 ~ \mathbf{in} ~ e_2 \end{array} \]
Constructors
| Var VarName | |
| Lit Literal | |
| App Expr Expr | |
| Lam VarName Type Expr | |
| Let VarName Type Expr Expr | This "let" is not recursive. |
| Assert Expr Expr |
Instances
| Eq Expr Source # | |
| Data Expr Source # | |
Defined in Jikka.Core.Language.Expr Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Expr -> c Expr # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Expr # dataTypeOf :: Expr -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Expr) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Expr) # gmapT :: (forall b. Data b => b -> b) -> Expr -> Expr # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Expr -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Expr -> r # gmapQ :: (forall d. Data d => d -> u) -> Expr -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> Expr -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> Expr -> m Expr # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Expr -> m Expr # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Expr -> m Expr # | |
| Ord Expr Source # | |
| Read Expr Source # | |
| Show Expr Source # | |
pattern ConvexHullTrickTy :: Type Source #
pattern SegmentTreeTy :: Semigroup' -> Type Source #
data ToplevelExpr Source #
ToplevelExpr is the toplevel exprs. In our core, "let rec" is allowed only on the toplevel.
\[ \begin{array}{rl} \mathrm{tle} ::= & e \\ \vert & \mathbf{let}~ x: \tau = e ~\mathbf{in}~ \mathrm{tle} \\ \vert & \mathbf{let~rec}~ x(x: \tau, x: \tau, \dots, x: \tau): \tau = e ~\mathbf{in}~ \mathrm{tle} \\ \vert & \mathbf{assert}~ e ~\mathbf{in}~ \mathrm{tle} \end{array} \]
Constructors
| ResultExpr Expr | |
| ToplevelLet VarName Type Expr ToplevelExpr | |
| ToplevelLetRec VarName [(VarName, Type)] Type Expr ToplevelExpr | |
| ToplevelAssert Expr ToplevelExpr |
Instances
type Program = ToplevelExpr Source #