mirror of
https://github.com/GaloisInc/cryptol.git
synced 2024-11-27 01:15:07 +03:00
Brian Huffman
parent
0a68d4e3a1
commit
d163e61c63
@ -105,7 +105,7 @@ infiniteSeqMap xs =
|
||||
-- TODO: use an int-trie?
|
||||
memoMap (IndexSeqMap $ \i -> genericIndex xs i)
|
||||
|
||||
-- | Create a finite list of length `n` of the values from [0..n-1] in
|
||||
-- | Create a finite list of length @n@ of the values from @[0..n-1]@ in
|
||||
-- the given the sequence emap.
|
||||
enumerateSeqMap :: (Integral n) => n -> SeqMap b w i -> [Eval (GenValue b w i)]
|
||||
enumerateSeqMap n m = [ lookupSeqMap m i | i <- [0 .. (toInteger n)-1] ]
|
||||
@ -124,7 +124,7 @@ updateSeqMap :: SeqMap b w i -> Integer -> Eval (GenValue b w i) -> SeqMap b w i
|
||||
updateSeqMap (UpdateSeqMap m sm) i x = UpdateSeqMap (Map.insert i x m) sm
|
||||
updateSeqMap (IndexSeqMap f) i x = UpdateSeqMap (Map.singleton i x) f
|
||||
|
||||
-- | Concatenate the first `n` values of the first sequence map onto the
|
||||
-- | Concatenate the first @n@ values of the first sequence map onto the
|
||||
-- beginning of the second sequence map.
|
||||
concatSeqMap :: Integer -> SeqMap b w i -> SeqMap b w i -> SeqMap b w i
|
||||
concatSeqMap n x y =
|
||||
@ -133,16 +133,16 @@ concatSeqMap n x y =
|
||||
then lookupSeqMap x i
|
||||
else lookupSeqMap y (i-n)
|
||||
|
||||
-- | Given a number `n` and a sequence map, return two new sequence maps:
|
||||
-- the first containing the values from `[0..n-1]` and the next containing
|
||||
-- the values from `n` onward.
|
||||
-- | Given a number @n@ and a sequence map, return two new sequence maps:
|
||||
-- the first containing the values from @[0..n-1]@ and the next containing
|
||||
-- the values from @n@ onward.
|
||||
splitSeqMap :: Integer -> SeqMap b w i -> (SeqMap b w i, SeqMap b w i)
|
||||
splitSeqMap n xs = (hd,tl)
|
||||
where
|
||||
hd = xs
|
||||
tl = IndexSeqMap $ \i -> lookupSeqMap xs (i+n)
|
||||
|
||||
-- | Drop the first @n@ elements of the given @SeqMap@.
|
||||
-- | Drop the first @n@ elements of the given 'SeqMap'.
|
||||
dropSeqMap :: Integer -> SeqMap b w i -> SeqMap b w i
|
||||
dropSeqMap 0 xs = xs
|
||||
dropSeqMap n xs = IndexSeqMap $ \i -> lookupSeqMap xs (i+n)
|
||||
@ -194,11 +194,11 @@ data WordValue b w i
|
||||
= WordVal !w -- ^ Packed word representation for bit sequences.
|
||||
| BitsVal !(Seq.Seq (Eval b)) -- ^ Sequence of thunks representing bits.
|
||||
| LargeBitsVal !Integer !(SeqMap b w i ) -- ^ A large bitvector sequence, represented as a
|
||||
-- @SeqMap@ of bits.
|
||||
-- 'SeqMap' of bits.
|
||||
deriving (Generic, NFData)
|
||||
|
||||
-- | An arbitrarily-chosen number of elements where we switch from a dense
|
||||
-- sequence representation of bit-level words to @SeqMap@ representation.
|
||||
-- sequence representation of bit-level words to 'SeqMap' representation.
|
||||
largeBitSize :: Integer
|
||||
largeBitSize = 1 `shiftL` 16
|
||||
|
||||
@ -256,7 +256,7 @@ indexWordValue (LargeBitsVal n xs) idx
|
||||
| idx < n = fromBit =<< lookupSeqMap xs idx
|
||||
| otherwise = invalidIndex idx
|
||||
|
||||
-- | Produce a new @WordValue@ from the one given by updating the @i@th bit with the
|
||||
-- | Produce a new 'WordValue' from the one given by updating the @i@th bit with the
|
||||
-- given bit value.
|
||||
updateWordValue :: BitWord b w i => WordValue b w i -> Integer -> Eval b -> Eval (WordValue b w i)
|
||||
updateWordValue (WordVal w) idx (Ready b)
|
||||
@ -275,9 +275,9 @@ updateWordValue (LargeBitsVal n xs) idx b
|
||||
-- | Generic value type, parameterized by bit and word types.
|
||||
--
|
||||
-- NOTE: we maintain an important invariant regarding sequence types.
|
||||
-- `VSeq` must never be used for finite sequences of bits.
|
||||
-- Always use the `VWord` constructor instead! Infinite sequences of bits
|
||||
-- are handled by the `VStream` constructor, just as for other types.
|
||||
-- 'VSeq' must never be used for finite sequences of bits.
|
||||
-- Always use the 'VWord' constructor instead! Infinite sequences of bits
|
||||
-- are handled by the 'VStream' constructor, just as for other types.
|
||||
data GenValue b w i
|
||||
= VRecord ![(Ident, Eval (GenValue b w i))] -- ^ @ { .. } @
|
||||
| VTuple ![Eval (GenValue b w i)] -- ^ @ ( .. ) @
|
||||
@ -433,7 +433,7 @@ class BitWord b w i | b -> w, w -> i, i -> b where
|
||||
-- | Pretty-print an integer value
|
||||
ppInteger :: PPOpts -> i -> Doc
|
||||
|
||||
-- | Attempt to render a word value as an ASCII character. Return `Nothing`
|
||||
-- | Attempt to render a word value as an ASCII character. Return 'Nothing'
|
||||
-- if the character value is unknown (e.g., for symbolic values).
|
||||
wordAsChar :: w -> Maybe Char
|
||||
|
||||
@ -491,9 +491,9 @@ class BitWord b w i | b -> w, w -> i, i -> b where
|
||||
-- The first integer argument is the number of bits in the
|
||||
-- resulting word. The second integer argument is the
|
||||
-- number of less-significant digits to discard. Stated another
|
||||
-- way, the operation `extractWord n i w` is equivalent to
|
||||
-- first shifting `w` right by `i` bits, and then truncating to
|
||||
-- `n` bits.
|
||||
-- way, the operation @extractWord n i w@ is equivalent to
|
||||
-- first shifting @w@ right by @i@ bits, and then truncating to
|
||||
-- @n@ bits.
|
||||
extractWord :: Integer -- ^ Number of bits to take
|
||||
-> Integer -- ^ starting bit
|
||||
-> w
|
||||
@ -641,11 +641,11 @@ lam = VFun
|
||||
wlam :: BitWord b w i => (w -> Eval (GenValue b w i)) -> GenValue b w i
|
||||
wlam f = VFun (\x -> x >>= fromVWord "wlam" >>= f)
|
||||
|
||||
-- | A type lambda that expects a @Type@.
|
||||
-- | A type lambda that expects a 'Type'.
|
||||
tlam :: (TValue -> GenValue b w i) -> GenValue b w i
|
||||
tlam f = VPoly (return . f)
|
||||
|
||||
-- | A type lambda that expects a @Type@ of kind #.
|
||||
-- | A type lambda that expects a 'Type' of kind #.
|
||||
nlam :: (Nat' -> GenValue b w i) -> GenValue b w i
|
||||
nlam f = VNumPoly (return . f)
|
||||
|
||||
@ -736,7 +736,7 @@ vWordLen val = case val of
|
||||
|
||||
-- | If the given list of values are all fully-evaluated thunks
|
||||
-- containing bits, return a packed word built from the same bits.
|
||||
-- However, if any value is not a fully-evaluated bit, return `Nothing`.
|
||||
-- However, if any value is not a fully-evaluated bit, return 'Nothing'.
|
||||
tryFromBits :: BitWord b w i => [Eval (GenValue b w i)] -> Maybe w
|
||||
tryFromBits = go id
|
||||
where
|
||||
|
||||
@ -30,8 +30,8 @@ type Gen g b w i = Integer -> g -> (GenValue b w i, g)
|
||||
|
||||
|
||||
{- | Apply a testable value to some randomly-generated arguments.
|
||||
Returns `Nothing` if the function returned `True`, or
|
||||
`Just counterexample` if it returned `False`.
|
||||
Returns @Nothing@ if the function returned @True@, or
|
||||
@Just counterexample@ if it returned @False@.
|
||||
|
||||
Please note that this function assumes that the generators match
|
||||
the supplied value, otherwise we'll panic.
|
||||
@ -87,7 +87,7 @@ returnTests g evo gens fun num = go gens g 0
|
||||
return ((inputs, output) : more)
|
||||
|
||||
{- | Given a (function) type, compute generators for the function's
|
||||
arguments. This is like @testableType@, but allows the result to be
|
||||
arguments. This is like 'testableType', but allows the result to be
|
||||
any finite type instead of just @Bit@. -}
|
||||
dumpableType :: forall g. RandomGen g => Type -> Maybe [Gen g Bool BV Integer]
|
||||
dumpableType ty =
|
||||
|
||||
@ -10,62 +10,62 @@
|
||||
-- slow down in some cases. What's the problem? Consider the following (common)
|
||||
-- patterns:
|
||||
--
|
||||
-- fibs = [0,1] # [ x + y | x <- fibs, y <- drop`{1} fibs ]
|
||||
-- > fibs = [0,1] # [ x + y | x <- fibs, y <- drop`{1} fibs ]
|
||||
--
|
||||
-- The type of `fibs` is:
|
||||
-- The type of @fibs@ is:
|
||||
--
|
||||
-- {a} (a >= 1, fin a) => [inf][a]
|
||||
-- > {a} (a >= 1, fin a) => [inf][a]
|
||||
--
|
||||
-- Here `a` is the number of bits to be used in the values computed by `fibs`.
|
||||
-- When we evaluate `fibs`, `a` becomes a parameter to `fibs`, which works
|
||||
-- except that now `fibs` is a function, and we don't get any of the memoization
|
||||
-- Here @a@ is the number of bits to be used in the values computed by @fibs@.
|
||||
-- When we evaluate @fibs@, @a@ becomes a parameter to @fibs@, which works
|
||||
-- except that now @fibs@ is a function, and we don't get any of the memoization
|
||||
-- we might expect! What looked like an efficient implementation has all
|
||||
-- of a sudden become exponential!
|
||||
--
|
||||
-- Note that this is only a problem for polymorphic values: if `fibs` was
|
||||
-- Note that this is only a problem for polymorphic values: if @fibs@ was
|
||||
-- already a function, it would not be that surprising that it does not
|
||||
-- get cached.
|
||||
--
|
||||
-- So, to avoid this, we try to spot recursive polymorphic values,
|
||||
-- where the recursive occurrences have the exact same type parameters
|
||||
-- as the definition. For example, this is the case in `fibs`: each
|
||||
-- recursive call to `fibs` is instantiated with exactly the same
|
||||
-- type parameter (i.e., `a`). The rewrite we do is as follows:
|
||||
-- as the definition. For example, this is the case in @fibs@: each
|
||||
-- recursive call to @fibs@ is instantiated with exactly the same
|
||||
-- type parameter (i.e., @a@). The rewrite we do is as follows:
|
||||
--
|
||||
-- fibs : {a} (a >= 1, fin a) => [inf][a]
|
||||
-- fibs = \{a} (a >= 1, fin a) -> fibs'
|
||||
-- where fibs' : [inf][a]
|
||||
-- fibs' = [0,1] # [ x + y | x <- fibs', y <- drop`{1} fibs' ]
|
||||
-- > fibs : {a} (a >= 1, fin a) => [inf][a]
|
||||
-- > fibs = \{a} (a >= 1, fin a) -> fibs'
|
||||
-- > where fibs' : [inf][a]
|
||||
-- > fibs' = [0,1] # [ x + y | x <- fibs', y <- drop`{1} fibs' ]
|
||||
--
|
||||
-- After the rewrite, the recursion is monomorphic (i.e., we are always using
|
||||
-- the same type). As a result, `fibs'` is an ordinary recursive value,
|
||||
-- the same type). As a result, @fibs'@ is an ordinary recursive value,
|
||||
-- where we get the benefit of caching.
|
||||
--
|
||||
-- The rewrite is a bit more complex, when there are multiple mutually
|
||||
-- recursive functions. Here is an example:
|
||||
--
|
||||
-- zig : {a} (a >= 2, fin a) => [inf][a]
|
||||
-- zig = [1] # zag
|
||||
--
|
||||
-- zag : {a} (a >= 2, fin a) => [inf][a]
|
||||
-- zag = [2] # zig
|
||||
-- > zig : {a} (a >= 2, fin a) => [inf][a]
|
||||
-- > zig = [1] # zag
|
||||
-- >
|
||||
-- > zag : {a} (a >= 2, fin a) => [inf][a]
|
||||
-- > zag = [2] # zig
|
||||
--
|
||||
-- This gets rewritten to:
|
||||
--
|
||||
-- newName : {a} (a >= 2, fin a) => ([inf][a], [inf][a])
|
||||
-- newName = \{a} (a >= 2, fin a) -> (zig', zag')
|
||||
-- where
|
||||
-- zig' : [inf][a]
|
||||
-- zig' = [1] # zag'
|
||||
--
|
||||
-- zag' : [inf][a]
|
||||
-- zag' = [2] # zig'
|
||||
--
|
||||
-- zig : {a} (a >= 2, fin a) => [inf][a]
|
||||
-- zig = \{a} (a >= 2, fin a) -> (newName a <> <> ).1
|
||||
--
|
||||
-- zag : {a} (a >= 2, fin a) => [inf][a]
|
||||
-- zag = \{a} (a >= 2, fin a) -> (newName a <> <> ).2
|
||||
-- > newName : {a} (a >= 2, fin a) => ([inf][a], [inf][a])
|
||||
-- > newName = \{a} (a >= 2, fin a) -> (zig', zag')
|
||||
-- > where
|
||||
-- > zig' : [inf][a]
|
||||
-- > zig' = [1] # zag'
|
||||
-- >
|
||||
-- > zag' : [inf][a]
|
||||
-- > zag' = [2] # zig'
|
||||
-- >
|
||||
-- > zig : {a} (a >= 2, fin a) => [inf][a]
|
||||
-- > zig = \{a} (a >= 2, fin a) -> (newName a <> <> ).1
|
||||
-- >
|
||||
-- > zag : {a} (a >= 2, fin a) => [inf][a]
|
||||
-- > zag = \{a} (a >= 2, fin a) -> (newName a <> <> ).2
|
||||
--
|
||||
-- NOTE: We are assuming that no capture would occur with binders.
|
||||
-- For values, this is because we replaces things with freshly chosen variables.
|
||||
@ -92,8 +92,8 @@ import MonadLib hiding (mapM)
|
||||
import Prelude ()
|
||||
import Prelude.Compat
|
||||
|
||||
{- (f,t,n) |--> x means that when we spot instantiations of `f` with `ts` and
|
||||
`n` proof argument, we should replace them with `Var x` -}
|
||||
{- (f,t,n) |--> x means that when we spot instantiations of @f@ with @ts@ and
|
||||
@n@ proof argument, we should replace them with @Var x@ -}
|
||||
newtype RewMap' a = RM (Map Name (TypesMap (Map Int a)))
|
||||
type RewMap = RewMap' Name
|
||||
|
||||
|
||||
@ -28,8 +28,8 @@ import Prelude.Compat
|
||||
|
||||
-- Specializer Monad -----------------------------------------------------------
|
||||
|
||||
-- | A Name should have an entry in the SpecCache iff it is
|
||||
-- specializable. Each Name starts out with an empty TypesMap.
|
||||
-- | A 'Name' should have an entry in the 'SpecCache' iff it is
|
||||
-- specializable. Each 'Name' starts out with an empty 'TypesMap'.
|
||||
type SpecCache = Map Name (Decl, TypesMap (Name, Maybe Decl))
|
||||
|
||||
-- | The specializer monad.
|
||||
@ -58,7 +58,7 @@ modify f = get >>= (set . f)
|
||||
|
||||
-- Specializer -----------------------------------------------------------------
|
||||
|
||||
-- | Add a `where` clause to the given expression containing
|
||||
-- | Add a @where@ clause to the given expression containing
|
||||
-- type-specialized versions of all functions called (transitively) by
|
||||
-- the body of the expression.
|
||||
specialize :: Expr -> M.ModuleCmd Expr
|
||||
@ -88,13 +88,13 @@ specializeExpr expr =
|
||||
e' <- specializeExpr e
|
||||
setSpecCache cache
|
||||
return (ETAbs t e')
|
||||
-- We need to make sure that after processing `e`, no specialized
|
||||
-- decls mentioning type variable `t` escape outside the
|
||||
-- `ETAbs`. To avoid this, we reset to an empty SpecCache while we
|
||||
-- run `specializeExpr e`, and restore it afterward: this
|
||||
-- We need to make sure that after processing @e@, no specialized
|
||||
-- decls mentioning type variable @t@ escape outside the
|
||||
-- 'ETAbs'. To avoid this, we reset to an empty 'SpecCache' while we
|
||||
-- run @'specializeExpr' e@, and restore it afterward: this
|
||||
-- effectively prevents the specializer from registering any type
|
||||
-- instantiations involving `t` for any decls bound outside the
|
||||
-- scope of `t`.
|
||||
-- instantiations involving @t@ for any decls bound outside the
|
||||
-- scope of @t@.
|
||||
ETApp {} -> specializeConst expr
|
||||
EApp e1 e2 -> EApp <$> specializeExpr e1 <*> specializeExpr e2
|
||||
EAbs qn t e -> EAbs qn t <$> specializeExpr e
|
||||
@ -144,9 +144,9 @@ withDeclGroups dgs action = do
|
||||
modifySpecCache (Map.union savedCache . flip Map.difference newCache)
|
||||
return (result, dgs', nameTable)
|
||||
|
||||
-- | Compute the specialization of `EWhere e dgs`. A decl within `dgs`
|
||||
-- | Compute the specialization of @'EWhere' e dgs@. A decl within @dgs@
|
||||
-- is replicated once for each monomorphic type instance at which it
|
||||
-- is used; decls not mentioned in `e` (even monomorphic ones) are
|
||||
-- is used; decls not mentioned in @e@ (even monomorphic ones) are
|
||||
-- simply dropped.
|
||||
specializeEWhere :: Expr -> [DeclGroup] -> SpecM Expr
|
||||
specializeEWhere e dgs = do
|
||||
@ -224,7 +224,7 @@ destETAbs = go []
|
||||
-- Any top-level declarations in the current module can be found in the
|
||||
-- ModuleEnv's LoadedModules, and so we can count of freshName to avoid
|
||||
-- collisions with them. Any generated name for a
|
||||
-- specialized function will be qualified with the current @ModName@, so genned
|
||||
-- specialized function will be qualified with the current 'ModName', so genned
|
||||
-- names will not collide with local decls either.
|
||||
-- freshName :: Name -> [Type] -> SpecM Name
|
||||
-- freshName n [] = return n
|
||||
@ -322,7 +322,7 @@ instantiateSchema ts n (Forall params props ty)
|
||||
| otherwise = return $ Forall [] [] (apSubst sub ty)
|
||||
where sub = listParamSubst (zip params ts)
|
||||
|
||||
-- | Reduce `length ts` outermost type abstractions and `n` proof abstractions.
|
||||
-- | Reduce @length ts@ outermost type abstractions and @n@ proof abstractions.
|
||||
instantiateExpr :: [Type] -> Int -> Expr -> SpecM Expr
|
||||
instantiateExpr [] 0 e = return e
|
||||
instantiateExpr [] n (EProofAbs _ e) = instantiateExpr [] (n - 1) e
|
||||
|
||||
@ -124,13 +124,13 @@ data Expr = EList [Expr] Type -- ^ List value (with type of elements)
|
||||
|
||||
{- | Proof abstraction. Because we don't keep proofs around
|
||||
we don't need to name the assumption, but we still need to
|
||||
record the assumption. The assumption is the `Type` term,
|
||||
which should be of kind `KProp`.
|
||||
record the assumption. The assumption is the 'Type' term,
|
||||
which should be of kind 'KProp'.
|
||||
-}
|
||||
| EProofAbs {- x -} Prop Expr
|
||||
|
||||
{- | If `e : p => t`, then `EProofApp e : t`,
|
||||
as long as we can prove `p`.
|
||||
{- | If @e : p => t@, then @EProofApp e : t@,
|
||||
as long as we can prove @p@.
|
||||
|
||||
We don't record the actual proofs, as they are not
|
||||
used for anything. It may be nice to keep them around
|
||||
@ -181,7 +181,7 @@ data DeclDef = DPrim
|
||||
ePrim :: PrimMap -> Ident -> Expr
|
||||
ePrim pm n = EVar (lookupPrimDecl n pm)
|
||||
|
||||
-- | Make an expression that is `error` pre-applied to a type and a message.
|
||||
-- | Make an expression that is @error@ pre-applied to a type and a message.
|
||||
eError :: PrimMap -> Type -> String -> Expr
|
||||
eError prims t str =
|
||||
EApp (ETApp (ETApp (ePrim prims (packIdent "error")) t)
|
||||
|
||||
@ -192,7 +192,7 @@ data RO = RO
|
||||
|
||||
{- NOTE: We assume no shadowing between these two, so it does not matter
|
||||
where we look first. Similarly, we assume no shadowing with
|
||||
the existential type variable (in RW). See `checkTShadowing`. -}
|
||||
the existential type variable (in RW). See 'checkTShadowing'. -}
|
||||
|
||||
, iTVars :: [TParam] -- ^ Type variable that are in scope
|
||||
, iTSyns :: Map Name (DefLoc, TySyn) -- ^ Type synonyms that are in scope
|
||||
@ -218,7 +218,7 @@ data RO = RO
|
||||
|
||||
, iSolvedHasLazy :: Map Int HasGoalSln
|
||||
-- ^ NOTE: This field is lazy in an important way! It is the
|
||||
-- final version of `iSolvedHas` in `RW`, and the two are tied
|
||||
-- final version of 'iSolvedHas' in 'RW', and the two are tied
|
||||
-- together through recursion. The field is here so that we can
|
||||
-- look thing up before they are defined, which is OK because we
|
||||
-- don't need to know the results until everything is done.
|
||||
@ -263,8 +263,8 @@ data RW = RW
|
||||
-- Constraints that need solving
|
||||
, iCts :: !Goals -- ^ Ordinary constraints
|
||||
, iHasCts :: ![HasGoal]
|
||||
{- ^ Tuple/record projection constraints. The `Int` is the "name"
|
||||
of the constraint, used so that we can name it solution properly. -}
|
||||
{- ^ Tuple/record projection constraints. The 'Int' is the "name"
|
||||
of the constraint, used so that we can name its solution properly. -}
|
||||
|
||||
, iSupply :: !Supply
|
||||
}
|
||||
@ -421,13 +421,13 @@ newHasGoal l ty f =
|
||||
addHasGoal :: HasGoal -> InferM ()
|
||||
addHasGoal g = IM $ sets_ $ \s -> s { iHasCts = g : iHasCts s }
|
||||
|
||||
-- | Get the `Has` constraints. Each of this should either be solved,
|
||||
-- or added back using `addHasGoal`.
|
||||
-- | Get the @Has@ constraints. Each of this should either be solved,
|
||||
-- or added back using 'addHasGoal'.
|
||||
getHasGoals :: InferM [HasGoal]
|
||||
getHasGoals = do gs <- IM $ sets $ \s -> (iHasCts s, s { iHasCts = [] })
|
||||
applySubst gs
|
||||
|
||||
-- | Specify the solution (`Expr -> Expr`) for the given constraint (`Int`).
|
||||
-- | Specify the solution (@Expr -> Expr@) for the given constraint ('Int').
|
||||
solveHasGoal :: Int -> HasGoalSln -> InferM ()
|
||||
solveHasGoal n e =
|
||||
IM $ sets_ $ \s -> s { iSolvedHas = Map.insert n e (iSolvedHas s) }
|
||||
@ -535,7 +535,7 @@ getSubst :: InferM Subst
|
||||
getSubst = IM $ fmap iSubst get
|
||||
|
||||
-- | Add to the accumulated substitution, checking that the datatype
|
||||
-- invariant for `Subst` is maintained.
|
||||
-- invariant for 'Subst' is maintained.
|
||||
extendSubst :: Subst -> InferM ()
|
||||
extendSubst su =
|
||||
do mapM_ check (substToList su)
|
||||
|
||||
@ -15,7 +15,7 @@ import Data.Maybe(listToMaybe)
|
||||
|
||||
|
||||
|
||||
-- | All ways to split a type in the form: `a + t1`, where `a` is a variable.
|
||||
-- | All ways to split a type in the form: @a + t1@, where @a@ is a variable.
|
||||
splitVarSummands :: Type -> [(TVar,Type)]
|
||||
splitVarSummands ty0 = [ (x,t1) | (x,t1) <- go ty0, tNum (0::Int) /= t1 ]
|
||||
where
|
||||
@ -32,12 +32,12 @@ splitVarSummands ty0 = [ (x,t1) | (x,t1) <- go ty0, tNum (0::Int) /= t1 ]
|
||||
TCon _ _ -> [] -- XXX: we could do some distributivity etc
|
||||
|
||||
|
||||
-- | Check if we can express a type in the form: `a + t1`.
|
||||
-- | Check if we can express a type in the form: @a + t1@.
|
||||
splitVarSummand :: TVar -> Type -> Maybe Type
|
||||
splitVarSummand a ty = listToMaybe [ t | (x,t) <- splitVarSummands ty, x == a ]
|
||||
|
||||
{- | Check if we can express a type in the form: `k + t1`,
|
||||
where `k` is a constant > 0.
|
||||
{- | Check if we can express a type in the form: @k + t1@,
|
||||
where @k@ is a constant > 0.
|
||||
This assumes that the type has been simplified already,
|
||||
so that constants are floated to the left. -}
|
||||
splitConstSummand :: Type -> Maybe (Integer, Type)
|
||||
@ -54,8 +54,8 @@ splitConstSummand ty =
|
||||
TCon (TC (TCNum k)) [] -> guard (k > 0) >> return (k, tNum (0::Int))
|
||||
TCon {} -> Nothing
|
||||
|
||||
{- | Check if we can express a type in the form: `k * t1`,
|
||||
where `k` is a constant > 1
|
||||
{- | Check if we can express a type in the form: @k * t1@,
|
||||
where @k@ is a constant > 1.
|
||||
This assumes that the type has been simplified already,
|
||||
so that constants are floated to the left. -}
|
||||
splitConstFactor :: Type -> Maybe (Integer, Type)
|
||||
|
||||
@ -99,8 +99,8 @@ data Type = TCon !TCon ![Type]
|
||||
{- ^ This is just a type annotation, for a type that
|
||||
was written as a type synonym. It is useful so that we
|
||||
can use it to report nicer errors.
|
||||
Example: `TUser T ts t` is really just the type `t` that
|
||||
was written as `T ts` by the user. -}
|
||||
Example: @TUser T ts t@ is really just the type @t@ that
|
||||
was written as @T ts@ by the user. -}
|
||||
|
||||
| TRec ![(Ident,Type)]
|
||||
-- ^ Record type
|
||||
@ -157,7 +157,7 @@ tvSourceName tvs =
|
||||
DefinitionOf x -> Just x
|
||||
_ -> Nothing
|
||||
|
||||
-- | The type is supposed to be of kind `KProp`
|
||||
-- | The type is supposed to be of kind 'KProp'.
|
||||
type Prop = Type
|
||||
|
||||
|
||||
@ -597,7 +597,7 @@ pLiteral x y = TCon (PC PLiteral) [x, y]
|
||||
(>==) :: Type -> Type -> Prop
|
||||
x >== y = TCon (PC PGeq) [x,y]
|
||||
|
||||
-- | A `Has` constraint, used for tuple and record selection.
|
||||
-- | A @Has@ constraint, used for tuple and record selection.
|
||||
pHas :: Selector -> Type -> Type -> Prop
|
||||
pHas l ty fi = TCon (PC (PHas l)) [ty,fi]
|
||||
|
||||
|
||||
Loading…
Reference in New Issue
Block a user