cryptol-3.0.0: Cryptol: The Language of Cryptography

Safe Haskell | Safe
Language | Haskell2010

Cryptol.TypeCheck.Default

Synopsis

- defaultLiterals :: [TVar] -> [Goal] -> ([TVar], Subst, [Warning])
- flitDefaultCandidates :: Goals -> Map TVar (Maybe ((TVar, Type), Warning))
- improveByDefaultingWithPure :: [TVar] -> [Goal] -> ([TVar], [Goal], Subst, [Error])
- defaultReplExpr' :: Solver -> [TParam] -> [Prop] -> IO (Maybe [(TParam, Type)])

# Documentation

defaultLiterals :: [TVar] -> [Goal] -> ([TVar], Subst, [Warning]) Source #

We default constraints of the form `Literal t a` and `FLiteral m n r a`.

For `Literal t a` we examine the context of constraints on the type `a` to decide how to default. If `Logic a` is required, we cannot do any defaulting. Otherwise, we default to either `Integer` or `Rational`. In particular, if we need to satisfy the `Field a`, constraint, we choose `Rational` and otherwise we choose `Integer`.

For `FLiteral t a` we always default to `Rational`.

flitDefaultCandidates :: Goals -> Map TVar (Maybe ((TVar, Type), Warning)) Source #

improveByDefaultingWithPure :: [TVar] -> [Goal] -> ([TVar], [Goal], Subst, [Error]) Source #

defaultReplExpr' :: Solver -> [TParam] -> [Prop] -> IO (Maybe [(TParam, Type)]) Source #

Try to pick a reasonable instantiation for an expression with the given type. This is useful when we do evaluation at the REPL. The resulting types should satisfy the constraints of the schema. The parameters should be all of numeric kind, and the props should als be numeric