← Back to branch summary

~ubuntu-branches/ubuntu/trusty/agda/trusty

« back to all changes in this revision

Viewing changes to src/full/Agda/Compiler/Epic/ForceConstrs.hs

  • Committer: Package Import Robot
  • Author(s): Iain Lane
  • Date: 2011-11-23 10:12:59 UTC
  • mfrom: (12.1.3 sid)
  • Revision ID: package-import@ubuntu.com-20111123101259-zhs3e4ynpck20hmu
Tags: 2.3.0-1
* [c0e4746] Imported Upstream version 2.3.0. New/changed features include:
  + New more liberal syntax for mutually recursive definitions
  + Pattern matching on lambdas
  + New syntax for updating (some fields of) records
  + Universe polymorphism is now enabled by default
  + New type of hidden function argument: instance arguments
  + Dependent irrelevant function types and records with irrelevant fields
  + See http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Main.Version-2-3-0
    for a full list
* [369ed3a] Update BDs in line with cabal requirements in new upstream
* [3798aee] Remove all patches. They are all now upstream.

Show diffs side-by-side

added added

removed removed

Lines of Context:
src/full/Agda/Compiler/Epic/ForceConstrs.hs
 
1
-- | Remove forced arguments from constructors.
 
2
{-# LANGUAGE CPP #-}
 
3
module Agda.Compiler.Epic.ForceConstrs where
 
4
 
 
5
import Control.Applicative
 
6
import Control.Monad.Trans
 
7
 
 
8
import Agda.Compiler.Epic.AuxAST
 
9
import Agda.Compiler.Epic.CompileState
 
10
import Agda.Compiler.Epic.Interface
 
11
 
 
12
import qualified Agda.Syntax.Common   as S
 
13
import qualified Agda.Syntax.Internal as T
 
14
import Agda.TypeChecking.Monad (TCM, reportSDoc)
 
15
import Agda.TypeChecking.Pretty
 
16
 
 
17
#include "../../undefined.h"
 
18
import Agda.Utils.Impossible
 
19
 
 
20
-- | Check which arguments are forced
 
21
makeForcedArgs :: T.Type -> ForcedArgs
 
22
makeForcedArgs (T.El _ term) = case term of
 
23
    T.Pi  arg ab  -> isRel arg : makeForcedArgs (T.unAbs ab)
 
24
    _ -> []
 
25
  where
 
26
    isRel :: S.Arg T.Type -> Forced
 
27
    isRel arg = case S.argRelevance arg of
 
28
      S.Relevant   -> NotForced
 
29
      S.Irrelevant -> Forced
 
30
      S.NonStrict  -> Forced -- can never be executed
 
31
      S.Forced     -> Forced -- It can be inferred
 
32
 
 
33
-- | Remove forced arguments from constructors and branches
 
34
forceConstrs :: [Fun] -> Compile TCM [Fun]
 
35
forceConstrs fs = mapM forceFun fs
 
36
 
 
37
forceFun :: Fun -> Compile TCM Fun
 
38
forceFun e@(EpicFun{}) = return e
 
39
forceFun (Fun inline name qname comment args expr) =
 
40
    Fun inline name qname comment args <$> forceExpr expr
 
41
  where
 
42
    -- | Remove all arguments to constructors that we don't need to store in an
 
43
    --   expression.
 
44
    forceExpr :: Expr -> Compile TCM Expr
 
45
    forceExpr expr = case expr of
 
46
        Var v        -> return $ Var v
 
47
        Lit l        -> return $ Lit l
 
48
        Lam v e      -> Lam v <$> forceExpr e
 
49
        Con tag q es -> do
 
50
            -- We only need to apply the non-forced arguments
 
51
            forcArgs <- getForcedArgs q
 
52
            return $ Con tag q $ notForced forcArgs es
 
53
        App v es     -> App v <$> mapM forceExpr es
 
54
        Case e bs    -> Case <$> forceExpr e <*> mapM forceBranch bs
 
55
        Let v e e'   -> lett v <$> forceExpr e <*> forceExpr e'
 
56
        If a b c     -> If <$> forceExpr a <*> forceExpr b <*> forceExpr c
 
57
        Lazy e       -> Lazy <$> forceExpr e
 
58
        UNIT         -> return expr
 
59
        IMPOSSIBLE   -> return expr
 
60
 
 
61
    -- | Remove all the arguments that don't need to be stored in the constructor
 
62
    --   For the branch
 
63
    forceBranch :: Branch -> Compile TCM Branch
 
64
    forceBranch br = case br of
 
65
        Branch  tag name vars e -> do
 
66
            ir <- getForcedArgs name
 
67
            let vs = notForced ir vars
 
68
                subs = forced ir vars
 
69
 
 
70
            e'' <- if all (`notElem` fv e) subs
 
71
                  then return e
 
72
                  else __IMPOSSIBLE__ -- If so, the removal of forced args has gone wrong
 
73
            Branch tag name vs <$> forceExpr e''
 
74
        BrInt i e -> BrInt i <$> forceExpr e
 
75
        Default e -> Default <$> forceExpr e