Additional haddock improvements

src/Cryptol/Eval.hs

@@ -53,9 +53,11 @@ type ReadEnv = EvalEnv
 
 -- Expression Evaluation -------------------------------------------------------
 
+-- | Extend the given evaluation environment with all the declarations
+--   contained in the given module.
 moduleEnv :: EvalPrims b w
-          => Module
-          -> GenEvalEnv b w
+          => Module         -- ^ Module containing declarations to evaluate
+          -> GenEvalEnv b w -- ^ Environment to extend
           -> Eval (GenEvalEnv b w)
 moduleEnv m env = evalDecls (mDecls m) =<< evalNewtypes (mNewtypes m) env
 
@@ -63,8 +65,8 @@ moduleEnv m env = evalDecls (mDecls m) =<< evalNewtypes (mNewtypes m) env
 --   by the `EvalPrims` class, which defines the behavior of bits and words, in
 --   addition to providing implementations for all the primitives.
 evalExpr :: EvalPrims b w
-         => GenEvalEnv b w
-         -> Expr
+         => GenEvalEnv b w     -- ^ Evaluation environment
+         -> Expr               -- ^ Expression to evaluate
          -> Eval (GenValue b w)
 evalExpr env expr = case expr of
 
@@ -182,9 +184,11 @@ evalNewtype nt = bindVar (ntName nt) (return (foldr tabs con (ntParams nt)))
 
 -- Declarations ----------------------------------------------------------------
 
+-- | Extend the given evaluation environment with the result of evaluating the
+--   given collection of declaration groups.
 evalDecls :: EvalPrims b w
-          => [DeclGroup]
-          -> GenEvalEnv b w
+          => [DeclGroup]         -- ^ Declaration groups to evaluate
+          -> GenEvalEnv b w      -- ^ Environment to extend
           -> Eval (GenEvalEnv b w)
 evalDecls dgs env = foldM evalDeclGroup env dgs
 

src/Cryptol/Eval/Env.hs

@@ -55,6 +55,7 @@ ppEnv opts env = brackets . fsep <$> mapM bind (Map.toList (envVars env))
    bind (k,v) = do vdoc <- ppValue opts =<< v
                    return (pp k <+> text "->" <+> vdoc)
 
+-- | Evaluation environment with no bindings
 emptyEnv :: GenEvalEnv b w
 emptyEnv  = mempty
 

src/Cryptol/Eval/Monad.hs

@@ -110,6 +110,7 @@ unDelay retry r x = do
       writeIORef r (Forced val)
       return val
 
+-- | Execute the given evaluation action.
 runEval :: Eval a -> IO a
 runEval (Ready a) = return a
 runEval (Thunk x) = x
@@ -121,7 +122,7 @@ evalBind (Thunk x) f  = Thunk (x >>= runEval . f)
 
 instance Functor Eval where
   fmap f (Ready x) = Ready (f x)
-  fmap f (Thunk m) = Thunk (f <$> m) 
+  fmap f (Thunk m) = Thunk (f <$> m)
   {-# INLINE fmap #-}
 
 instance Applicative Eval where
@@ -159,13 +160,14 @@ evalPanic :: String -> [String] -> a
 evalPanic cxt = panic ("[Eval] " ++ cxt)
 
 
+-- | Data type describing errors that can occur during evaluation
 data EvalError
-  = InvalidIndex Integer
-  | TypeCannotBeDemoted Type
-  | DivideByZero
-  | WordTooWide Integer
-  | UserError String
-  | LoopError String
+  = InvalidIndex Integer          -- ^ Out-of-bounds index
+  | TypeCannotBeDemoted Type      -- ^ Non-numeric type passed to demote function
+  | DivideByZero                  -- ^ Division or modulus by 0
+  | WordTooWide Integer           -- ^ Bitvector too large
+  | UserError String              -- ^ Call to the Cryptol 'error' primitive
+  | LoopError String              -- ^ Detectable nontermination
     deriving (Typeable,Show)
 
 instance PP EvalError where

src/Cryptol/Eval/Type.hs

@@ -25,14 +25,15 @@ import Control.DeepSeq
 -- | An evaluated type of kind *.
 -- These types do not contain type variables, type synonyms, or type functions.
 data TValue
-  = TVBit
-  | TVSeq Integer TValue
-  | TVStream TValue -- ^ [inf]t
-  | TVTuple [TValue]
-  | TVRec [(Ident, TValue)]
-  | TVFun TValue TValue
+  = TVBit                    -- ^ @ Bit @
+  | TVSeq Integer TValue     -- ^ @ [n]a @
+  | TVStream TValue          -- ^ @ [inf]t @
+  | TVTuple [TValue]         -- ^ @ (a, b, c )@
+  | TVRec [(Ident, TValue)]  -- ^ @ { x : a, y : b, z : c } @
+  | TVFun TValue TValue      -- ^ @ a -> b @
     deriving (Generic, NFData)
 
+-- | Convert a type value back into a regular type
 tValTy :: TValue -> Type
 tValTy tv =
   case tv of
@@ -49,14 +50,18 @@ instance Show TValue where
 
 -- Utilities -------------------------------------------------------------------
 
+-- | True if the evaluated value is @Bit@
 isTBit :: TValue -> Bool
 isTBit TVBit = True
 isTBit _ = False
 
+-- | Produce a sequence type value
 tvSeq :: Nat' -> TValue -> TValue
 tvSeq (Nat n) t = TVSeq n t
 tvSeq Inf     t = TVStream t
 
+-- | Coerce an extended natural into an integer,
+--   for values known to be finite
 finNat' :: Nat' -> Integer
 finNat' n' =
   case n' of
@@ -103,6 +108,7 @@ evalValType env ty =
     Left _ -> evalPanic "evalValType" ["expected value type, found numeric type"]
     Right t -> t
 
+-- | Evaluation for number types (kind #).
 evalNumType :: TypeEnv -> Type -> Nat'
 evalNumType env ty =
   case evalType env ty of

src/Cryptol/Eval/Value.hs

@@ -195,17 +195,17 @@ indexWordValue (BitsVal bs) idx = Seq.index bs (fromInteger idx)
 --   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
-  = VRecord ![(Ident, Eval (GenValue b w))] -- @ { .. } @
-  | VTuple ![Eval (GenValue b w)]           -- @ ( .. ) @
-  | VBit !b                                 -- @ Bit    @
-  | VSeq !Integer !(SeqMap b w)             -- @ [n]a   @
-                                            -- Invariant: VSeq is never a sequence of bits
-  | VWord !Integer !(Eval (WordValue b w))  -- @ [n]Bit @
-  | VStream !(SeqMap b w)                   -- @ [inf]a @
-  | VFun (Eval (GenValue b w) -> Eval (GenValue b w)) -- functions
-  | VPoly (TValue -> Eval (GenValue b w))   -- polymorphic values (kind *)
-  | VNumPoly (Nat' -> Eval (GenValue b w))  -- polymorphic values (kind #)
-  deriving (Generic, NFData)
+  = VRecord ![(Ident, Eval (GenValue b w))] -- ^ @ { .. } @
+  | VTuple ![Eval (GenValue b w)]           -- ^ @ ( .. ) @
+  | VBit !b                                 -- ^ @ Bit    @
+  | VSeq !Integer !(SeqMap b w)             -- ^ @ [n]a   @
+                                            --   Invariant: VSeq is never a sequence of bits
+  | VWord !Integer !(Eval (WordValue b w))  -- ^ @ [n]Bit @
+  | VStream !(SeqMap b w)                   -- ^ @ [inf]a @
+  | VFun (Eval (GenValue b w) -> Eval (GenValue b w)) -- ^ functions
+  | VPoly (TValue -> Eval (GenValue b w))   -- ^ polymorphic values (kind *)
+  | VNumPoly (Nat' -> Eval (GenValue b w))  -- ^ polymorphic values (kind #)
+ deriving (Generic, NFData)
 
 
 -- | Force the evaluation of a word value

src/Cryptol/Prims/Eval.hs

@@ -367,13 +367,6 @@ arithBinary op = loop
       return $ VRecord [ (f, loop' fty (lookupRecord f l) (lookupRecord f r))
                        | (f,fty) <- fs ]
 
-    -- | otherwise = do
-    --       ldoc <- ppValue defaultPPOpts l
-    --       rdoc <- ppValue defaultPPOpts r
-    --       evalPanic "arithBinop" ["Invalid arguments", show ty
-    --                              , show ldoc, show rdoc]
-
-
 type UnaryArith w = Integer -> w -> w
 
 liftUnaryArith :: (Integer -> Integer) -> UnaryArith BV