@@ -1,7 +1,7 @@
11{-# LANGUAGE PatternGuards #-}
22{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}
33
4−-- Reduction to Weak Head Normal Form
4+-- | Reduction to Weak Head Normal Form
55module Idris.Core.WHNF(whnf, WEnv) where
66
77import Idris.Core.TT
@@ -11,7 +11,7 @@ import qualified Idris.Core.Evaluate as Evaluate
1111
1212import Debug.Trace
1313
14−-- A stack entry consists of a term and the environment it is to be
14+-- | A stack entry consists of a term and the environment it is to be
1515-- evaluated in (i.e. it's a thunk)
1616type StackEntry = (Term, WEnv)
1717data WEnv = WEnv Int -- number of free variables
@@ -20,17 +20,17 @@ data WEnv = WEnv Int -- number of free variables
2020
2121type Stack = [StackEntry]
2222
23−-- A WHNF is a top level term evaluated in the empty environment. It is
23+-- | A WHNF is a top level term evaluated in the empty environment. It is
2424-- always headed by either an irreducible expression, i.e. a constructor,
2525-- a lambda, a constant, or a postulate
26−
26+--
2727-- Every 'Term' or 'Type' in this structure is associated with the
2828-- environment it was encountered in, so that when we quote back to a term
2929-- we get the substitutions right.
3030
31−data WHNF = WDCon Int Int Bool Name (Type, WEnv) -- data constructor
32− | WTCon Int Int Name (Type, WEnv) -- type constructor
33− | WPRef Name (Type, WEnv) -- irreducible global (e.g. a postulate)
31+data WHNF = WDCon Int Int Bool Name (Type, WEnv) -- ^ data constructor
32+ | WTCon Int Int Name (Type, WEnv) -- ^ type constructor
33+ | WPRef Name (Type, WEnv) -- ^irreducible global (e.g. a postulate)
3434 | WBind Name (Binder Term) (Term, WEnv)
3535 | WApp WHNF (Term, WEnv)
3636 | WConstant Const
@@ -40,7 +40,7 @@ data WHNF = WDCon Int Int Bool Name (Type, WEnv) -- data constructor
4040 | WErased
4141 | WImpossible
4242
43−-- Reduce a *closed* term to weak head normal form.
43+-- | Reduce a *closed* term to weak head normal form.
4444whnf :: Context -> Term -> Term
4545whnf ctxt tm = quote (do_whnf ctxt (WEnv 0 []) tm)
4646