68c519e · Idris-dev · git.iko.soy

1{-# LANGUAGE PatternGuards #-}

2{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}

3

4−-- Reduction to Weak Head Normal Form

4+-- | Reduction to Weak Head Normal Form

5module Idris.Core.WHNF(whnf, WEnv) where

6

7import Idris.Core.TT

11

12import Debug.Trace

13

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

15-- evaluated in (i.e. it's a thunk)

16type StackEntry = (Term, WEnv)

17data WEnv = WEnv Int -- number of free variables

20

21type Stack = [StackEntry]

22

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

24-- always headed by either an irreducible expression, i.e. a constructor,

25-- a lambda, a constant, or a postulate

26−

26+--

27-- Every 'Term' or 'Type' in this structure is associated with the

28-- environment it was encountered in, so that when we quote back to a term

29-- we get the substitutions right.

30

31−data WHNF = WDCon Int Int Bool Name (Type, WEnv) -- data constructor

31+data WHNF = WDCon Int Int Bool Name (Type, WEnv) -- ^ data constructor

32− | WTCon Int Int Name (Type, WEnv) -- type constructor

32+ | WTCon Int Int Name (Type, WEnv) -- ^ type constructor

33− | WPRef Name (Type, WEnv) -- irreducible global (e.g. a postulate)

33+ | WPRef Name (Type, WEnv) -- ^irreducible global (e.g. a postulate)

34 | WBind Name (Binder Term) (Term, WEnv)

35 | WApp WHNF (Term, WEnv)

36 | WConstant Const

40 | WErased

41 | WImpossible

42

43−-- Reduce a *closed* term to weak head normal form.

43+-- | Reduce a *closed* term to weak head normal form.

44whnf :: Context -> Term -> Term

45whnf ctxt tm = quote (do_whnf ctxt (WEnv 0 []) tm)

46