← Back to branch summary

~ubuntu-branches/ubuntu/wily/agda/wily-proposed

« back to all changes in this revision

Viewing changes to src/full/Agda/Auto/Typecheck.hs

  • Committer: Package Import Robot
  • Author(s): Iain Lane
  • Date: 2014-08-05 06:38:12 UTC
  • mfrom: (1.1.6)
  • Revision ID: package-import@ubuntu.com-20140805063812-io8e77niomivhd49
Tags: 2.4.0.2-1
* [6e140ac] Imported Upstream version 2.4.0.2
* [2049fc8] Update Build-Depends to match control
* [93dc4d4] Install the new primitives
* [e48f40f] Fix typo dev→doc

Show diffs side-by-side

added added

removed removed

Lines of Context:
src/full/Agda/Auto/Typecheck.hs
1
 
{-# LANGUAGE ExistentialQuantification, FlexibleContexts,
2
 
             ScopedTypeVariables, CPP #-}
 
1
{-# LANGUAGE CPP #-}
 
2
{-# LANGUAGE ExistentialQuantification #-}
 
3
{-# LANGUAGE FlexibleContexts #-}
 
4
{-# LANGUAGE ScopedTypeVariables #-}
3
5
 
4
6
module Agda.Auto.Typecheck where
5
7
 
6
 
import Agda.Utils.Impossible
7
 
#include "../undefined.h"
8
 
 
9
8
import Data.IORef
10
9
import Control.Monad (liftM)
11
10
 
13
12
import Agda.Auto.Syntax
14
13
import Agda.Auto.SearchControl
15
14
 
 
15
#include "../undefined.h"
 
16
import Agda.Utils.Impossible
16
17
 
17
18
-- ---------------------------------
18
19
 
 
20
-- | Typechecker drives the solution of metas.
 
21
 
19
22
tcExp :: Bool -> Ctx o -> CExp o -> MExp o -> EE (MyPB o)
20
23
tcExp isdep ctx typ@(TrBr typtrs ityp@(Clos _ itypexp)) trm =
21
24
  mbpcase prioTypeUnknown Nothing (hnn_checkstep ityp) $ \(hntyp, iotastepdone) ->
597
600
           Left _ -> return True
598
601
           Right e -> boringExp e
599
602
          ALCons{} -> return False
600
 
 
601
 
          ALProj{} -> __IMPOSSIBLE__
602
 
 
603
 
 
 
603
          ALProj{} -> return False
604
604
          ALConPar{} -> return False
605
605
 
606
606
       _ -> return False