@@ -1,4 +1,4 @@
1−{-# LANGUAGE PatternGuards, ViewPatterns #-}
1+{-# LANGUAGE LambdaCase, PatternGuards, ViewPatterns #-}
2{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}
2{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}
3module Idris.ElabTerm where
3module Idris.ElabTerm where
@@ -37,6 +37,7 @@ import Debug.Trace
37data ElabMode = ETyDecl | ELHS | ERHS
37data ElabMode = ETyDecl | ELHS | ERHS
38 deriving Eq
38 deriving Eq
40data ElabResult =
41data ElabResult =
41 ElabResult { resultTerm :: Term -- ^ The term resulting from elaboration
42 ElabResult { resultTerm :: Term -- ^ The term resulting from elaboration
42 , resultMetavars :: [(Name, (Int, Maybe Name, Type))]
43 , resultMetavars :: [(Name, (Int, Maybe Name, Type))]
@@ -45,22 +46,23 @@ data ElabResult =
45 -- ^ Deferred declarations as the meaning of case blocks
46 -- ^ Deferred declarations as the meaning of case blocks
46 , resultContext :: Context
47 , resultContext :: Context
47 -- ^ The potentially extended context from new definitions
48 -- ^ The potentially extended context from new definitions
48− , resultTyDecls :: [(Name, FC, [PArg], Type)]
49+ , resultTyDecls :: [RDeclInstructions]
49 -- ^ Meta-info about the new type declarations
50 -- ^ Meta-info about the new type declarations
52−processTacticDecls :: [(Name, FC, [PArg], Type)] -> Idris ()
53+processTacticDecls :: [RDeclInstructions] -> Idris ()
53processTacticDecls info =
54processTacticDecls info =
54− forM_ info $ \(n, fc, impls, ty) ->
55+ forM_ info $ \case
56+ RTyDeclInstrs n fc impls ty ->
55− do logLvl 3 $ "Declaration from tactics: " ++ show n ++ " : " ++ show ty
57+ do logLvl 3 $ "Declaration from tactics: " ++ show n ++ " : " ++ show ty
56− logLvl 3 $ " It has impls " ++ show impls
58+ logLvl 3 $ " It has impls " ++ show impls
57− updateIState $ \i -> i { idris_implicits =
59+ updateIState $ \i -> i { idris_implicits =
58− addDef n impls (idris_implicits i) }
60+ addDef n impls (idris_implicits i) }
59− addIBC (IBCImp n)
61+ addIBC (IBCImp n)
60− ds <- checkDef fc [(n, (-1, Nothing, ty))]
62+ ds <- checkDef fc [(n, (-1, Nothing, ty))]
61− addIBC (IBCDef n)
63+ addIBC (IBCDef n)
62− let ds' = map (\(n, (i, top, t)) -> (n, (i, top, t, True))) ds
64+ let ds' = map (\(n, (i, top, t)) -> (n, (i, top, t, True))) ds
63− addDeferred ds'
65+ addDeferred ds'
66-- Using the elaborator, convert a term in raw syntax to a fully
68-- Using the elaborator, convert a term in raw syntax to a fully
@@ -1695,7 +1697,7 @@ runTactical fc env tm = do tm' <- eval tm
1695 let decl = TyDecl Ref checked
1697 let decl = TyDecl Ref checked
1696 ctxt' = addCtxtDef n decl ctxt
1698 ctxt' = addCtxtDef n decl ctxt
1697 set_context ctxt'
1699 set_context ctxt'
1698− updateAux $ \e -> e { new_tyDecls = (n, fc, map rArgToPArg args, checked) :
1700+ updateAux $ \e -> e { new_tyDecls = (RTyDeclInstrs n fc (map rArgToPArg args) checked) :
1699 new_tyDecls e }
1701 new_tyDecls e }
1700 aux <- getAux
1702 aux <- getAux
1701 returnUnit
1703 returnUnit