| Copyright | (C) 2020 QBayLogic B.V. |
|---|---|
| License | BSD2 (see the file LICENSE) |
| Maintainer | QBayLogic B.V. <devops@qbaylogic.com> |
| Safe Haskell | None |
| Language | Haskell2010 |
Clash.Core.PartialEval.NormalForm
Description
Normal forms for the partial evaluator. These provide a restricted model of how terms can be constructed (compared to the more liberal Term type) which give a stronger guarantee that evaluation does not produce invalid results. This module is only needed to define new evaluators, for calling an existing evaluator see Clash.Core.PartialEval.
Synopsis
- type Arg a = Either a Type
- type Args a = [Arg a]
- data Neutral a
- data Value
- mkValueTicks :: Value -> [TickInfo] -> Value
- stripValue :: Value -> Value
- collectValueTicks :: Value -> (Value, [TickInfo])
- isUndefined :: Value -> Bool
- data Normal
- data LocalEnv = LocalEnv {
- lenvContext :: Id
- lenvTypes :: Map TyVar Type
- lenvValues :: Map Id Value
- lenvFuel :: Word
- lenvKeepLifted :: Bool
- data GlobalEnv = GlobalEnv {
- genvBindings :: VarEnv (Binding Value)
- genvTyConMap :: TyConMap
- genvInScope :: InScopeSet
- genvSupply :: Supply
- genvFuel :: Word
- genvHeap :: IntMap Value
- genvAddr :: Int
- genvWorkCache :: VarEnv Bool
- workFreeCache :: Lens' GlobalEnv (VarEnv Bool)
Documentation
Neutral terms cannot be reduced, as they represent things like variables which are unknown, partially applied functions, or case expressions where the subject cannot be inspected. Consider:
v Stuck if "v" is a free variable p x1 ... xn Stuck if "p" is a primitive that cannot be reduced x $ y Stuck if "x" is not known to be a lambda x @ A Stuck if "x" is not known to be a type lambda case x of ... Stuck if "x" is neutral (cannot choose an alternative)
Neutral terms can also be let expressions which preserve required bindings in the normal form representation. Examples of bindings that may be kept are bindings which perform work (and should not be copied) or bindings that are recursive and are still referred to by the body of the let expression.
let ... in ... Preserved bindings are needed by the body
Constructors
| NeVar !Id | |
| NePrim !PrimInfo !(Args a) | |
| NeApp !(Neutral a) !a | |
| NeTyApp !(Neutral a) !Type | |
| NeLetrec ![(Id, a)] !a | |
| NeCase !a !Type ![(Pat, a)] |
A term which has been potentially evaluated to WHNF. If evaluation has occurred, then there will be no redexes at the head of the Value, but sub-terms may still have redexes. Data constructors are only considered to be values when fully applied, if partially applied they should be eta-expanded during evaluation.
Thunks are included so that lazy evaluation can be modelled without needing to store Either Term Value in the environment. This makes the presentation simpler, with the caveat that values must be forced when they are required to not be thunks.
stripValue :: Value -> Value Source #
isUndefined :: Value -> Bool Source #
A term which is in beta-normal eta-long form (NF). This has no redexes, and all partially applied functions in sub-terms are eta-expanded.
While not strictly necessary, NLam includes the environment at the point the original term was evaluated. This makes it easier for the AsTerm instance for Normal to reintroduce let expressions before lambdas without accidentally floating a let using a lambda bound variable outwards.
Constructors
| LocalEnv | |
Fields
| |
Constructors
| GlobalEnv | |
Fields
| |