@@ -1,4 +1,4 @@
1−{-# LANGUAGE PatternGuards, ViewPatterns #-}
1+{-# LANGUAGE LambdaCase, PatternGuards, ViewPatterns #-}
22{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}
33module Idris.ElabTerm where
44
@@ -37,6 +37,7 @@ import Debug.Trace
3737data ElabMode = ETyDecl | ELHS | ERHS
3838 deriving Eq
3939
40+
4041data ElabResult =
4142 ElabResult { resultTerm :: Term -- ^ The term resulting from elaboration
4243 , resultMetavars :: [(Name, (Int, Maybe Name, Type))]
@@ -45,22 +46,23 @@ data ElabResult =
4546 -- ^ Deferred declarations as the meaning of case blocks
4647 , resultContext :: Context
4748 -- ^ The potentially extended context from new definitions
48− , resultTyDecls :: [(Name, FC, [PArg], Type)]
49+ , resultTyDecls :: [RDeclInstructions]
4950 -- ^ Meta-info about the new type declarations
5051 }
5152
52−processTacticDecls :: [(Name, FC, [PArg], Type)] -> Idris ()
53+processTacticDecls :: [RDeclInstructions] -> Idris ()
5354processTacticDecls info =
54− forM_ info $ \(n, fc, impls, ty) ->
55− do logLvl 3 $ "Declaration from tactics: " ++ show n ++ " : " ++ show ty
56− logLvl 3 $ " It has impls " ++ show impls
57− updateIState $ \i -> i { idris_implicits =
58− addDef n impls (idris_implicits i) }
59− addIBC (IBCImp n)
60− ds <- checkDef fc [(n, (-1, Nothing, ty))]
61− addIBC (IBCDef n)
62− let ds' = map (\(n, (i, top, t)) -> (n, (i, top, t, True))) ds
63− addDeferred ds'
55+ forM_ info $ \case
56+ RTyDeclInstrs n fc impls ty ->
57+ do logLvl 3 $ "Declaration from tactics: " ++ show n ++ " : " ++ show ty
58+ logLvl 3 $ " It has impls " ++ show impls
59+ updateIState $ \i -> i { idris_implicits =
60+ addDef n impls (idris_implicits i) }
61+ addIBC (IBCImp n)
62+ ds <- checkDef fc [(n, (-1, Nothing, ty))]
63+ addIBC (IBCDef n)
64+ let ds' = map (\(n, (i, top, t)) -> (n, (i, top, t, True))) ds
65+ addDeferred ds'
6466
6567
6668-- Using the elaborator, convert a term in raw syntax to a fully
@@ -1695,7 +1697,7 @@ runTactical fc env tm = do tm' <- eval tm
16951697 let decl = TyDecl Ref checked
16961698 ctxt' = addCtxtDef n decl ctxt
16971699 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) :
16991701 new_tyDecls e }
17001702 aux <- getAux
17011703 returnUnit