0 | module TTImp.ProcessDecls

  2 | import Core.Directory

  3 | import Core.Env

  4 | import Core.Metadata

  5 | import Core.Termination

  6 | import Core.UnifyState

  8 | import Idris.Error

  9 | import Idris.Pretty

 10 | import Idris.REPL.Opts

 11 | import Idris.Syntax

 12 | import Parser.Source

 14 | import TTImp.BindImplicits

 15 | import TTImp.Elab.Check

 16 | import TTImp.Parser

 17 | import TTImp.ProcessBuiltin

 18 | import TTImp.ProcessData

 19 | import TTImp.ProcessDef

 20 | import TTImp.ProcessParams

 21 | import TTImp.ProcessRecord

 22 | import TTImp.ProcessRunElab

 23 | import TTImp.ProcessTransform

 24 | import TTImp.ProcessType

 25 | import TTImp.TTImp

 27 | import TTImp.ProcessDecls.Totality

 29 | import Libraries.Text.PrettyPrint.Prettyprinter.Doc

 31 | %default covering

 33 | processFailing :

 34 |   {vars : _} ->

 35 |   {auto c : Ref Ctxt Defs} ->

 36 |   {auto m : Ref MD Metadata} ->

 37 |   {auto u : Ref UST UState} ->

 38 |   {auto s : Ref Syn SyntaxInfo} ->

 39 |   {auto o : Ref ROpts REPLOpts} ->

 40 |   List ElabOpt ->

 41 |   NestedNames vars -> Env Term vars ->

 42 |   FC -> Maybe String ->  List ImpDecl -> Core ()

 43 | processFailing eopts nest env fc mmsg decls

 44 |     = do -- save the state: the content of a failing block should be discarded

 45 |          ust <- get UST

 46 |          syn <- get Syn

 47 |          md <- get MD

 49 |          -- We expect the block to fail and so the definitions introduced

 50 |          -- in it should be discarded once we leave the block.

 51 |          defs <- branch

 53 |          -- We're going to run the elaboration, and then return:

 54 |          -- * Nothing     if the block correctly failed

 55 |          -- * Just err    if it either did not fail or failed with an invalid error message

 56 |          result <- catch

 57 |                (do -- Run the elaborator

 58 |                    before <- getTotalityErrors

 59 |                    traverse_ (processDecl eopts nest env) decls

 60 |                    after <- getTotalityErrors

 61 |                    let errs = after \\ before

 62 |                    let (e :: es) = errs

 63 |                      | [] => do -- We better have unsolved holes

 64 |                                 -- checkUserHoles True -- do we need this one too?

 66 |                                  -- should we only look at the ones introduced in the block?

 67 |                                 Nothing <- checkDelayedHoles

 68 |                                   | Just err => throw err

 70 |                                 -- Or we have (unfortunately) succeeded

 71 |                                 pure (Just $ FailingDidNotFail fc)

 72 |                    let Just msg = mmsg

 73 |                      | _ => pure Nothing

 74 |                    log "elab.failing" 10 $ "Failing block based on \{show msg} failed with \{show errs}"

 75 |                    test <- anyM (checkError msg) errs

 76 |                    pure $ do -- Unless the error is the expected one

 77 |                              guard (not test)

 78 |                              -- We should complain we had the wrong one

 79 |                              pure (FailingWrongError fc msg (e ::: es)))

 80 |                (\err => do let Just msg = mmsg

 81 |                                  | _ => pure Nothing

 82 |                            log "elab.failing" 10 $ "Failing block based on \{show msg} failed with \{show err}"

 83 |                            test <- checkError msg err

 84 |                            pure $ do -- Unless the error is the expected one

 85 |                                      guard (not test)

 86 |                                      -- We should complain we had the wrong one

 87 |                                      pure (FailingWrongError fc msg (err ::: [])))

 88 |          md' <- get MD

 89 |          -- Reset the state

 90 |          put UST ust

 91 |          put Syn syn

 92 |          -- For metadata, we preserve the syntax highlithing information (but none

 93 |          -- of the things that may include code that's dropped like types, LHSs, etc.)

 94 |          put MD ({ semanticHighlighting := semanticHighlighting md'

 95 |                  , semanticAliases := semanticAliases md'

 96 |                  , semanticDefaults := semanticDefaults md'

 97 |                  } md)

 98 |          put Ctxt defs

 99 |          -- And fail if the block was successfully accepted

100 |          whenJust result throw

104 | process : {vars : _} ->

105 |           {auto c : Ref Ctxt Defs} ->

106 |           {auto m : Ref MD Metadata} ->

107 |           {auto u : Ref UST UState} ->

108 |           {auto s : Ref Syn SyntaxInfo} ->

109 |           {auto o : Ref ROpts REPLOpts} ->

110 |           List ElabOpt ->

111 |           NestedNames vars -> Env Term vars -> ImpDecl -> Core ()

112 | process eopts nest env (IClaim dat@(MkWithData fc (MkIClaimData rig vis opts ty)))

113 |     = processType eopts nest env dat.fc rig vis opts ty

114 | process eopts nest env (IData fc vis mbtot ddef)

115 |     = processData eopts nest env fc vis mbtot ddef

116 | process eopts nest env (IDef fc fname def)

117 |     = processDef eopts nest env fc fname def

118 | process eopts nest env (IParameters fc ps decls)

119 |     = processParams nest env fc (forget ps) decls

120 | process eopts nest env (IRecord fc ns vis mbtot rec)

121 |     = processRecord eopts nest env ns vis mbtot rec

122 | process eopts nest env (IFail fc msg decls)

123 |     = processFailing eopts nest env fc msg decls

124 | process eopts nest env (INamespace fc ns decls)

125 |     = withExtendedNS ns $

126 |          traverse_ (processDecl eopts nest env) decls

127 | process eopts nest env (ITransform fc n lhs rhs)

128 |     = processTransform eopts nest env fc n lhs rhs

129 | process eopts nest env (IRunElabDecl fc tm)

130 |     = processRunElab eopts nest env fc tm

131 | process eopts nest env (IPragma _ _ act)

132 |     = act nest env

133 | process eopts nest env (ILog lvl)

134 |     = addLogLevel (uncurry unsafeMkLogLevel <$> lvl)

135 | process eopts nest env (IBuiltin fc type name)

136 |     = processBuiltin nest env fc type name

138 | TTImp.Elab.Check.processDecl = process

141 | processDecls : {vars : _} ->

142 |                {auto c : Ref Ctxt Defs} ->

143 |                {auto m : Ref MD Metadata} ->

144 |                {auto u : Ref UST UState} ->

145 |                {auto s : Ref Syn SyntaxInfo} ->

146 |                {auto o : Ref ROpts REPLOpts} ->

147 |                NestedNames vars -> Env Term vars -> List ImpDecl -> Core Bool

148 | processDecls nest env decls

149 |     = do traverse_ (processDecl [] nest env) decls

150 |          pure True -- TODO: False on error

152 | processTTImpDecls : {vars : _} ->

153 |                     {auto c : Ref Ctxt Defs} ->

154 |                     {auto m : Ref MD Metadata} ->

155 |                     {auto u : Ref UST UState} ->

156 |                     {auto s : Ref Syn SyntaxInfo} ->

157 |                     {auto o : Ref ROpts REPLOpts} ->

158 |                     NestedNames vars -> Env Term vars -> List ImpDecl -> Core Bool

159 | processTTImpDecls {vars} nest env decls

160 |     = do traverse_ (\d => do d' <- bindNames d

161 |                              processDecl [] nest env d') decls

162 |          pure True -- TODO: False on error

163 |   where

164 |     bindConNames : ImpTy -> Core ImpTy

165 |     bindConNames ty

166 |         = traverse (bindTypeNames ty.fc [] (toList vars)) ty

168 |     bindDataNames : ImpData -> Core ImpData

169 |     bindDataNames (MkImpData fc n t opts cons)

170 |         = do t' <- traverseOpt (bindTypeNames fc [] (toList vars)) t

171 |              cons' <- traverse bindConNames cons

172 |              pure (MkImpData fc n t' opts cons')

173 |     bindDataNames (MkImpLater fc n t)

174 |         = do t' <- bindTypeNames fc [] (toList vars) t

175 |              pure (MkImpLater fc n t')

177 |     -- bind implicits to make raw TTImp source a bit friendlier

178 |     bindNames : ImpDecl -> Core ImpDecl

179 |     bindNames (IClaim dat@(MkWithData fc (MkIClaimData c vis opts ty)))

180 |         = do ty' <- bindTypeNames dat.fc [] (toList vars) ty.val

181 |              pure (IClaim (MkWithData fc (MkIClaimData c vis opts ({val := ty'} ty))))

182 |     bindNames (IData fc vis mbtot d)

183 |         = do d' <- bindDataNames d

184 |              pure (IData fc vis mbtot d')

185 |     bindNames d = pure d

188 | processTTImpFile : {auto c : Ref Ctxt Defs} ->

189 |                    {auto m : Ref MD Metadata} ->

190 |                    {auto u : Ref UST UState} ->

191 |                    {auto s : Ref Syn SyntaxInfo} ->

192 |                    {auto o : Ref ROpts REPLOpts} ->

193 |                    String -> Core Bool

194 | processTTImpFile fname

195 |     = do modIdent <- ctxtPathToNS fname

196 |          Right (ws, decor, tti) <- logTime 0 "Parsing" $

197 |                             coreLift $ parseFile fname (PhysicalIdrSrc modIdent)

198 |                             (do decls <- prog (PhysicalIdrSrc modIdent)

199 |                                 eoi

200 |                                 pure decls)

201 |                | Left err => do coreLift (putStrLn (show err))

202 |                                 pure False

203 |          traverse_ recordWarning ws

204 |          logTime 0 "Elaboration" $

205 |             catch (do ignore $ processTTImpDecls (MkNested []) Env.empty tti

206 |                       Nothing <- checkDelayedHoles

207 |                           | Just err => throw err

208 |                       pure True)

209 |                   (\err => do coreLift_ (printLn err)

210 |                               pure False)