summaryrefslogtreecommitdiff
path: root/src/full/Agda/Compiler/MAlonzo/Compiler.hs
diff options
context:
space:
mode:
Diffstat (limited to 'src/full/Agda/Compiler/MAlonzo/Compiler.hs')
-rw-r--r--src/full/Agda/Compiler/MAlonzo/Compiler.hs65
1 files changed, 27 insertions, 38 deletions
diff --git a/src/full/Agda/Compiler/MAlonzo/Compiler.hs b/src/full/Agda/Compiler/MAlonzo/Compiler.hs
index 335499b..7398c73 100644
--- a/src/full/Agda/Compiler/MAlonzo/Compiler.hs
+++ b/src/full/Agda/Compiler/MAlonzo/Compiler.hs
@@ -1,6 +1,6 @@
-{-# LANGUAGE CPP #-}
+{-# LANGUAGE CPP #-}
{-# LANGUAGE FlexibleContexts #-}
-{-# LANGUAGE PatternGuards #-}
+{-# LANGUAGE PatternGuards #-}
module Agda.Compiler.MAlonzo.Compiler where
@@ -111,11 +111,8 @@ imports = (++) <$> hsImps <*> imps where
((++) <$> importsForPrim <*> (List.map mazMod <$> mnames))
decl :: HS.ModuleName -> HS.ImportDecl
-#if MIN_VERSION_haskell_src_exts(1,16,0)
decl m = HS.ImportDecl dummy m True False False Nothing Nothing Nothing
-#else
- decl m = HS.ImportDecl dummy m True False Nothing Nothing Nothing
-#endif
+
mnames :: TCM [ModuleName]
mnames = (++) <$> (Set.elems <$> use stImportedModules)
<*> (List.map fst . iImportedModules <$> curIF)
@@ -149,7 +146,7 @@ definitions defs = do
definition :: Maybe CoinductionKit -> Definition -> TCM [HS.Decl]
-- ignore irrelevant definitions
{- Andreas, 2012-10-02: Invariant no longer holds
-definition kit (Defn Forced _ _ _ _ _ _ _ _) = __IMPOSSIBLE__
+definition kit (Defn Forced{} _ _ _ _ _ _ _ _) = __IMPOSSIBLE__
definition kit (Defn UnusedArg _ _ _ _ _ _ _ _) = __IMPOSSIBLE__
definition kit (Defn NonStrict _ _ _ _ _ _ _ _) = __IMPOSSIBLE__
-}
@@ -282,11 +279,8 @@ checkCover q ty n cs = do
(a, _) <- conArityAndPars c
Just (HsDefn _ hsc) <- compiledHaskell . defCompiledRep <$> getConstInfo c
let pat = HS.PApp (HS.UnQual $ HS.Ident hsc) $ genericReplicate a HS.PWildCard
-#if MIN_VERSION_haskell_src_exts(1,16,0)
return $ HS.Alt dummy pat (HS.UnGuardedRhs $ HS.unit_con) (HS.BDecls [])
-#else
- return $ HS.Alt dummy pat (HS.UnGuardedAlt $ HS.unit_con) (HS.BDecls [])
-#endif
+
cs <- mapM makeClause cs
let rhs = case cs of
[] -> fakeExp "()" -- There is no empty case statement in Haskell
@@ -336,11 +330,9 @@ argpatts ps0 bvs = evalStateT (mapM pat' ps0) bvs
pat (ProjP _ ) = lift $ typeError $ NotImplemented $ "Compilation of copatterns"
pat (VarP _ ) = do v <- gets head; modify tail; return v
pat (DotP _ ) = pat (VarP dummy) -- WHY NOT: return HS.PWildCard -- SEE ABOVE
-#if MIN_VERSION_haskell_src_exts(1,16,0)
+ pat (LitP (LitQName _ x)) = return $ litqnamepat x
pat (LitP l ) = return $ HS.PLit HS.Signless $ hslit l
-#else
- pat (LitP l ) = return $ HS.PLit $ hslit l
-#endif
+
pat p@(ConP c _ ps) = do
-- Note that irr is applied once for every subpattern, so in the
-- worst case it is quadratic in the size of the pattern. I
@@ -431,7 +423,7 @@ literal l = case l of
LitInt _ _ -> do toN <- bltQual "NATURAL" mazIntegerToNat
return $ HS.Var toN `HS.App` typed "Integer"
LitFloat _ _ -> return $ typed "Double"
- LitQName _ x -> litqname x
+ LitQName _ x -> return $ litqname x
_ -> return $ l'
where l' = HS.Lit $ hslit l
typed = HS.ExpTypeSig dummy l' . HS.TyCon . rtmQual
@@ -443,13 +435,25 @@ hslit l = case l of LitInt _ x -> HS.Int x
LitChar _ x -> HS.Char x
LitQName _ x -> __IMPOSSIBLE__
-litqname :: QName -> TCM HS.Exp
-litqname x = return $
+litqname :: QName -> HS.Exp
+litqname x =
HS.Con (HS.Qual mazRTE $ HS.Ident "QName") `HS.App`
HS.Lit (HS.Int n) `HS.App`
HS.Lit (HS.Int m) `HS.App`
(rtmError "primQNameType: not implemented") `HS.App`
- (rtmError "primQNameDefinition: not implemented")
+ (rtmError "primQNameDefinition: not implemented") `HS.App`
+ HS.Lit (HS.String $ show x )
+ where
+ NameId n m = nameId $ qnameName x
+
+litqnamepat :: QName -> HS.Pat
+litqnamepat x =
+ HS.PApp (HS.Qual mazRTE $ HS.Ident "QName")
+ [ HS.PLit HS.Signless (HS.Int n)
+ , HS.PLit HS.Signless (HS.Int m)
+ , HS.PWildCard
+ , HS.PWildCard
+ , HS.PWildCard]
where
NameId n m = nameId $ qnameName x
@@ -460,11 +464,7 @@ condecl q = do
cdecl :: QName -> Nat -> HS.ConDecl
cdecl q n = HS.ConDecl (unqhname "C" q)
-#if MIN_VERSION_haskell_src_exts(1,16,0)
[ HS.TyVar $ ihname "a" i | i <- [0 .. n - 1] ]
-#else
- [ HS.UnBangedTy $ HS.TyVar $ ihname "a" i | i <- [0 .. n - 1] ]
-#endif
tvaldecl :: QName
-> Induction
@@ -548,9 +548,9 @@ rteModule = ok $ parse $ unlines
, "{-# RULES \"coerce-id\" forall (x :: a) . mazCoerce x = x #-}"
, ""
, "-- Builtin QNames, the third field is for the type."
- , "data QName a b = QName { nameId, moduleId :: Integer, qnameType :: a, qnameDefinition :: b }"
+ , "data QName a b = QName { nameId, moduleId :: Integer, qnameType :: a, qnameDefinition :: b, qnameString :: String}"
, "instance Eq (QName a b) where"
- , " QName a b _ _ == QName c d _ _ = (a, b) == (c, d)"
+ , " QName a b _ _ _ == QName c d _ _ _ = (a, b) == (c, d)"
, ""
, "mazIncompleteMatch :: String -> a"
, "mazIncompleteMatch s = error (\"MAlonzo Runtime Error: incomplete pattern matching: \" ++ s)"
@@ -558,24 +558,13 @@ rteModule = ok $ parse $ unlines
where
parse :: String -> HS.ParseResult HS.Module
parse = HS.parseModuleWithMode
- HS.defaultParseMode{HS.extensions = [explicitForAll]}
+ HS.defaultParseMode
+ { HS.extensions = [ HS.EnableExtension HS.ExplicitForAll ] }
ok :: HS.ParseResult HS.Module -> HS.Module
ok (HS.ParseOk d) = d
ok HS.ParseFailed{} = __IMPOSSIBLE__
-explicitForAll :: HS.Extension
-explicitForAll =
--- GHC 7.0.1 cannot parse the following CPP conditional
--- error: missing binary operator before token "("
-#if MIN_VERSION_haskell_src_exts(1,14,0)
- HS.EnableExtension HS.ExplicitForAll
-#elif MIN_VERSION_haskell_src_exts(1,12,0)
- HS.ExplicitForAll
-#else
- HS.ExplicitForall
-#endif
-
compileDir :: TCM FilePath
compileDir = do
mdir <- optCompileDir <$> commandLineOptions