← Back to branch summary

~ubuntu-branches/ubuntu/raring/agda/raring-proposed

« back to all changes in this revision

Viewing changes to src/full/Agda/Syntax/Translation/ConcreteToAbstract.hs

  • Committer: Bazaar Package Importer
  • Author(s): Iain Lane
  • Date: 2010-01-05 23:43:20 UTC
  • mfrom: (1.1.1 upstream)
  • Revision ID: james.westby@ubuntu.com-20100105234320-6ksc0sdsfhtweknu
Tags: 2.2.6-1
http://bugs.debian.org/559197
* New upstream release 2.2.6, for headlines please see:
  http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Main.Version-2-2-6
* debian/control
  + Bump standards-version to 3.8.3, no changes
  + Fix Vcs-Git to point to correct URL
  + Update build-depends for new upstream release
  + Undo arch/indep split per current pkg-haskell practice
  + Add Homepage field
* debian/copyright: Fix encoding to UTF-8 (thanks Lintian) 
* debian/README.source: Remove, no repacking so not necessary any more 
* debian/50agda.el:
  + Only load file if it exists, prevents a non-intrusive emacs warning
    where 50agda.el is left on system when package is removed. 
    (Closes: #559197). 
  + Do not load file on XEmacs — agda-mode is not compatible with XEmacs.

Show diffs side-by-side

added added

removed removed

Lines of Context:
src/full/Agda/Syntax/Translation/ConcreteToAbstract.hs
30
30
import Data.List ((\\), nub)
31
31
import qualified Data.Map as Map
32
32
 
33
 
import Agda.Syntax.Concrete as C
 
33
import Agda.Syntax.Concrete as C hiding (topLevelModuleName)
34
34
import Agda.Syntax.Abstract as A
35
35
import Agda.Syntax.Position
36
36
import Agda.Syntax.Common
42
42
import Agda.Syntax.Scope.Monad
43
43
import Agda.Syntax.Strict
44
44
 
45
 
import Agda.TypeChecking.Monad.Base (TypeError(..), Call(..), typeError, TCErr(..))
 
45
import Agda.TypeChecking.Monad.Base (TypeError(..), Call(..), typeError,
 
46
                                     TCErr(..), TCErr'(..))
46
47
import Agda.TypeChecking.Monad.Trace (traceCall, traceCallCPS, setCurrentRange)
47
48
import Agda.TypeChecking.Monad.State
48
49
import Agda.TypeChecking.Monad.Options
119
120
  return $ ScopedExpr s e
120
121
 
121
122
expandEllipsis :: C.Pattern -> [C.Pattern] -> C.Clause -> C.Clause
122
 
expandEllipsis _ _ c@(C.Clause _ (C.LHS _ _ _) _ _ _) = c
123
 
expandEllipsis p ps (C.Clause x (C.Ellipsis _ ps' es) rhs wh wcs) =
124
 
  C.Clause x (C.LHS p (ps ++ ps') es) rhs wh wcs
 
123
expandEllipsis _ _ c@(C.Clause _ C.LHS{} _ _ _) = c
 
124
expandEllipsis p ps (C.Clause x (C.Ellipsis _ ps' eqs es) rhs wh wcs) =
 
125
  C.Clause x (C.LHS p (ps ++ ps') eqs es) rhs wh wcs
125
126
 
126
127
-- | Make sure that each variable occurs only once.
127
128
checkPatternLinearity :: [A.Pattern' e] -> ScopeM ()
151
152
    notField NiceField{} = False
152
153
    notField _           = True
153
154
 
154
 
    build (NiceField r f _ _ x e : fs) = C.Pi [C.TypedBindings r NotHidden
155
 
                                                [C.TBind r [BName x f] e]
156
 
                                              ] $ build fs
 
155
    build (NiceField r f _ _ h x e : fs) = C.Pi [C.TypedBindings r h
 
156
                                                  [C.TBind r [BName x f] e]
 
157
                                                ] $ build fs
157
158
      where r = getRange x
158
159
    build (d : fs)                     = C.Let noRange (notSoNiceDeclarations [d]) $ build fs
159
160
    build []                           = C.Prop noRange
318
319
      (DefinedName d, C.QName x) | DefName == anameKind d -> return $ Left x
319
320
      (UnknownName,   C.QName x)                          -> return $ Left x
320
321
      (ConstructorName ds, _)                             -> return $ Right ds
321
 
      _                                                   -> fail $ "not a constructor: " ++ show x -- TODO
 
322
      _                                                   ->
 
323
        typeError $ GenericError $
 
324
          "Cannot pattern match on " ++ show x ++ ", because it is not a constructor"
322
325
    case z of
323
326
      Left x  -> do
324
327
        reportSLn "scope.pat" 10 $ "it was a var: " ++ show x
548
551
 
549
552
niceDecls :: [C.Declaration] -> ScopeM [NiceDeclaration]
550
553
niceDecls ds = case runNice $ niceDeclarations ds of
551
 
  Left e   -> throwError $ Exception (getRange e) (show e)
 
554
  Left e   -> throwError $ TCErr Nothing $ Exception (getRange e) (show e)
552
555
  Right ds -> return ds
553
556
 
554
557
instance ToAbstract [C.Declaration] [A.Declaration] where
588
591
 
589
592
            _   -> notAValidLetBinding d
590
593
        where
591
 
            letToAbstract (C.Clause top clhs@(C.LHS p [] []) (C.RHS rhs) NoWhere []) = do
 
594
            letToAbstract (C.Clause top clhs@(C.LHS p [] [] []) (C.RHS rhs) NoWhere []) = do
592
595
                p    <- parseLHS (Just top) p
593
596
                localToAbstract (snd $ lhsArgs p) $ \args ->
594
597
                    do  rhs <- toAbstract rhs
628
631
    toAbstract (C.BuiltinPragma _ b e) = do
629
632
        e <- toAbstract e
630
633
        return [ A.BuiltinPragma b e ]
631
 
    toAbstract (C.LinePragma _ _ _) = return []
632
634
    toAbstract (C.ImportPragma _ i) = do
633
635
      addHaskellImport i
634
636
      return []
 
637
    toAbstract (C.ImpossiblePragma _) = __IMPOSSIBLE__
635
638
 
636
639
-- Only constructor names are bound by definitions.
637
640
instance ToAbstract NiceDefinition Definition where
667
670
          conName _ = __IMPOSSIBLE__
668
671
 
669
672
    -- Record definitions (mucho interesting)
670
 
      C.RecDef r f p a x pars fields ->
 
673
      C.RecDef r f p a x c pars fields ->
671
674
        traceCall (ScopeCheckDefinition d) $
672
675
        withLocalVars $ do
673
676
          pars   <- toAbstract pars
686
689
          -- popScope p
687
690
          bindModule p x m
688
691
          printScope "rec" 15 "record complete"
689
 
          return $ A.RecDef (mkDefInfo x f p a r) x' pars contel afields
 
692
          c' <- mapM (toAbstract . Constr) c
 
693
          return $ A.RecDef (mkDefInfo x f p a r) x' c' pars contel afields
690
694
 
691
695
-- The only reason why we return a list is that open declarations disappears.
692
696
-- For every other declaration we get a singleton list.
704
708
      return [ A.Axiom (mkDefInfo x f p a r) y t' ]
705
709
 
706
710
  -- Fields
707
 
    C.NiceField r f p a x t -> do
 
711
    C.NiceField r f p a h x t -> do
708
712
      t' <- toAbstractCtx TopCtx t
709
713
      y  <- freshAbstractQName f x
710
714
      bindName p DefName x y
711
 
      return [ A.Field (mkDefInfo x f p a r) y t' ]
 
715
      return [ A.Field (mkDefInfo x f p a r) h y t' ]
712
716
 
713
717
  -- Primitive function
714
718
    PrimitiveFunction r f p a x t -> do
816
820
    toAbstract _ = __IMPOSSIBLE__    -- a constructor is always an axiom
817
821
 
818
822
instance ToAbstract C.Clause A.Clause where
819
 
    toAbstract (C.Clause top (C.Ellipsis _ _ _) _ _ _) = fail "bad '...'" -- TODO: errors message
820
 
    toAbstract (C.Clause top lhs@(C.LHS p wps with) rhs wh wcs) = withLocalVars $ do
 
823
    toAbstract (C.Clause top C.Ellipsis{} _ _ _) = fail "bad '...'" -- TODO: errors message
 
824
    toAbstract (C.Clause top lhs@(C.LHS p wps eqs with) rhs wh wcs) = withLocalVars $ do
821
825
      let wcs' = map (expandEllipsis p wps) wcs
822
826
      lhs' <- toAbstract (LeftHandSide top p wps)
823
827
      printLocals 10 "after lhs:"
825
829
            NoWhere        -> (Nothing, [])
826
830
            AnyWhere ds    -> (Nothing, ds)
827
831
            SomeWhere m ds -> (Just m, ds)
828
 
      case whds of
829
 
        [] -> do
830
 
          rhs <- toAbstract =<< toAbstractCtx TopCtx (RightHandSide with wcs' rhs)
 
832
      if not (null eqs)
 
833
        then do
 
834
          rhs <- toAbstract =<< toAbstractCtx TopCtx (RightHandSide eqs with wcs' rhs whds)
831
835
          return $ A.Clause lhs' rhs []
832
 
        _       -> do
833
 
          m <- maybe (nameConcrete <$> freshNoName noRange) return whname
834
 
          let acc = maybe PrivateAccess (const PublicAccess) whname  -- unnamed where's are private
835
 
          let tel = []
836
 
          old <- getCurrentModule
837
 
          am  <- toAbstract (NewModuleName m)
838
 
          (scope, ds) <- scopeCheckModule (getRange wh) (C.QName m) am tel whds
839
 
          setScope scope
 
836
        else do
840
837
          -- the right hand side is checked inside the module of the local definitions
841
 
          rhs <- toAbstractCtx TopCtx (RightHandSide with wcs' rhs)
842
 
          setCurrentModule old
843
 
          bindModule acc m am
 
838
          (rhs, ds) <- whereToAbstract (getRange wh) whname whds $
 
839
                        toAbstractCtx TopCtx (RightHandSide eqs with wcs' rhs [])
844
840
          rhs <- toAbstract rhs
845
841
          return $ A.Clause lhs' rhs ds
846
842
 
847
 
data RightHandSide = RightHandSide [C.Expr] [C.Clause] C.RHS
 
843
whereToAbstract :: Range -> Maybe C.Name -> [C.Declaration] -> ScopeM a -> ScopeM (a, [A.Declaration])
 
844
whereToAbstract _ _ [] inner = do
 
845
  x <- inner
 
846
  return (x, [])
 
847
whereToAbstract r whname whds inner = do
 
848
  m <- maybe (nameConcrete <$> freshNoName noRange) return whname
 
849
  let acc = maybe PrivateAccess (const PublicAccess) whname  -- unnamed where's are private
 
850
  let tel = []
 
851
  old <- getCurrentModule
 
852
  am  <- toAbstract (NewModuleName m)
 
853
  (scope, ds) <- scopeCheckModule r (C.QName m) am tel whds
 
854
  setScope scope
 
855
  x <- inner
 
856
  setCurrentModule old
 
857
  bindModule acc m am
 
858
  return (x, ds)
 
859
 
 
860
data RightHandSide = RightHandSide [C.Expr] [C.Expr] [C.Clause] C.RHS [C.Declaration]
848
861
data AbstractRHS = AbsurdRHS'
849
862
                 | WithRHS' [A.Expr] [C.Clause]  -- ^ The with clauses haven't been translated yet
850
863
                 | RHS' A.Expr
 
864
                 | RewriteRHS' [A.Expr] AbstractRHS [A.Declaration]
 
865
 
 
866
withFunctionName :: String -> ScopeM A.QName
 
867
withFunctionName s = do
 
868
  m <- getCurrentModule
 
869
  NameId i _ <- fresh
 
870
  A.qualify m <$> freshName_ (s ++ show i)
851
871
 
852
872
instance ToAbstract AbstractRHS A.RHS where
853
 
  toAbstract AbsurdRHS'       = return A.AbsurdRHS
854
 
  toAbstract (RHS' e)         = return $ A.RHS e
 
873
  toAbstract AbsurdRHS'            = return A.AbsurdRHS
 
874
  toAbstract (RHS' e)              = return $ A.RHS e
 
875
  toAbstract (RewriteRHS' eqs rhs wh) = do
 
876
    auxs <- replicateM (length eqs) $ withFunctionName "rewrite-"
 
877
    rhs  <- toAbstract rhs
 
878
    return $ RewriteRHS auxs eqs rhs wh
855
879
  toAbstract (WithRHS' es cs) = do
856
 
    m   <- getCurrentModule
857
 
    -- Hack
858
 
    NameId i _ <- fresh
859
 
    aux <- A.qualify m <$> freshName_ ("aux" ++ show i)
 
880
    aux <- withFunctionName "with-"
860
881
    A.WithRHS aux es <$> toAbstract cs
861
882
 
862
883
instance ToAbstract RightHandSide AbstractRHS where
863
 
  toAbstract (RightHandSide [] (_ : _) _)        = __IMPOSSIBLE__
864
 
  toAbstract (RightHandSide (_ : _) _ (C.RHS _)) = typeError $ BothWithAndRHS
865
 
  toAbstract (RightHandSide [] [] rhs)           = toAbstract rhs
866
 
  toAbstract (RightHandSide es cs C.AbsurdRHS)   = do
 
884
  toAbstract (RightHandSide eqs@(_:_) es cs rhs wh) = do
 
885
    eqs <- toAbstractCtx TopCtx eqs
 
886
                 -- TODO: remember named where
 
887
    (rhs, ds) <- whereToAbstract (getRange wh) Nothing wh $
 
888
                  toAbstract (RightHandSide [] es cs rhs [])
 
889
    return $ RewriteRHS' eqs rhs ds
 
890
  toAbstract (RightHandSide [] [] (_ : _) _ _)        = __IMPOSSIBLE__
 
891
  toAbstract (RightHandSide [] (_ : _) _ (C.RHS _) _) = typeError $ BothWithAndRHS
 
892
  toAbstract (RightHandSide [] [] [] rhs [])          = toAbstract rhs
 
893
  toAbstract (RightHandSide [] es cs C.AbsurdRHS [])  = do
867
894
    es <- toAbstractCtx TopCtx es
868
895
    return $ WithRHS' es cs
 
896
  -- TODO: some of these might be possible
 
897
  toAbstract (RightHandSide [] (_ : _) _ C.AbsurdRHS (_ : _)) = __IMPOSSIBLE__
 
898
  toAbstract (RightHandSide [] [] [] (C.RHS _) (_ : _))       = __IMPOSSIBLE__
 
899
  toAbstract (RightHandSide [] [] [] C.AbsurdRHS (_ : _))     = __IMPOSSIBLE__
869
900
 
870
901
instance ToAbstract C.RHS AbstractRHS where
871
902
    toAbstract C.AbsurdRHS = return $ AbsurdRHS'