@@ -191,66 +191,11 @@ ibc i (IBCDyLib n) f = return f {ibc_dynamic_libs = n : ibc_dynamic_libs f }
191191ibc i (IBCHeader tgt n) f = return f { ibc_hdrs = (tgt, n) : ibc_hdrs f }
192192ibc i (IBCDef n) f
193193 = do f' <- case lookupDefExact n (tt_ctxt i) of
194− Just v -> do -- (v', (f', _)) <- runStateT (updateDef v) (f, length (symbols f))
195− return f { ibc_defs = (n,v) : ibc_defs f }
194+ Just v -> return f { ibc_defs = (n,v) : ibc_defs f }
196195 _ -> ifail "IBC write failed"
197196 case lookupCtxtExact n (idris_patdefs i) of
198197 Just v -> return f' { ibc_patdefs = (n,v) : ibc_patdefs f }
199198 _ -> return f' -- Not a pattern definition
200− where
201− updateDef :: Def -> StateT (IBCFile, Int) Idris Def
202− updateDef (CaseOp c t args o s cd)
203− = do o' <- mapM updateOrig o
204− cd' <- updateCD cd
205− return (CaseOp c t args o' s cd')
206− updateDef t = return t
207−
208− updateOrig (Left t) = do t' <- update t
209− return (Left t')
210− updateOrig (Right (l,r)) = do l' <- update l
211− r' <- update r
212− return (Right (l', r'))
213−
214− updateCD (CaseDefs (ts, t) (cs, c) (is, i) (rs, r))
215− = do c' <- updateSC c; r' <- updateSC r
216− return (CaseDefs (ts, t) (cs, c') (is, i) (rs, r'))
217−
218− updateSC (Case up n alts) = do alts' <- mapM updateAlt alts
219− return (Case up n alts')
220− updateSC (ProjCase t alts) = do t' <- update t
221− alts' <- mapM updateAlt alts
222− return (ProjCase t' alts')
223− updateSC (STerm t) = do t' <- update t
224− return (STerm t')
225− updateSC t = return t
226−
227− updateAlt (ConCase n i a sc) = do sc' <- updateSC sc
228− return (ConCase n i a sc')
229− updateAlt (FnCase n a sc) = do sc' <- updateSC sc
230− return (FnCase n a sc')
231− updateAlt (ConstCase i sc) = do sc' <- updateSC sc
232− return (ConstCase i sc')
233− updateAlt (SucCase n sc) = do sc' <- updateSC sc
234− return (SucCase n sc')
235− updateAlt (DefaultCase sc) = do sc' <- updateSC sc
236− return (DefaultCase sc')
237−
238− update (P t n@(MN _ _) ty) = return (P t n ty)
239− update (P t n@(UN _) ty) = return (P t n ty)
240− update (P t n ty) = do (f, len) <- ST.get
241− (i, _) <- lift (addNameIdx n)
242− when (i >= len) $
243− ST.put (f { symbols = symbols f ++ [n] }, len+1)
244− return (P t (SymRef i) ty)
245− update (App f a) = do f' <- update f; a' <- update a
246− return (App f' a')
247− update (Bind n b sc) = do b' <- fmapMB update b
248− sc' <- update sc
249− return (Bind n b' sc')
250− update (Proj t i) = do t' <- update t
251− return (Proj t' i)
252− update t = return t
253−
254199
255200ibc i (IBCDoc n) f = case lookupCtxtExact n (idris_docstrings i) of
256201 Just v -> return f { ibc_docstrings = (n,v) : ibc_docstrings f }
@@ -470,7 +415,7 @@ pPatdefs ds
470415pDefs :: Bool -> [Name] -> [(Name, Def)] -> Idris ()
471416pDefs reexp syms ds
472417 = mapM_ (\ (n, d) ->
473− do let d' = force d -- (updateDef d)
418+ do d' <- updateDef d
474419 case d' of
475420 TyDecl _ _ -> return ()
476421 _ -> do iLOG $ "SOLVING " ++ show n
@@ -483,23 +428,55 @@ pDefs reexp syms ds
483428 else iLOG $ "Exporting " ++ show n) ds
484429 where
485430 updateDef (CaseOp c t args o s cd)
486− = CaseOp c t args (map updateOrig o) s (updateCD cd)
487− updateDef t = t
431+ = do o' <- mapM updateOrig o
432+ cd' <- updateCD cd
433+ return $ CaseOp c t args o' s cd'
434+ updateDef t = return t
488435
489− updateOrig (Left t) = Left (update t)
490− updateOrig (Right (l, r)) = Right (update l, update r)
436+ updateOrig (Left t) = liftM Left (update t)
437+ updateOrig (Right (l, r)) = do l' <- update l
438+ r' <- update r
439+ return $ Right (l', r')
491440
492441 updateCD (CaseDefs (ts, t) (cs, c) (is, i) (rs, r))
493− = CaseDefs (ts, fmap update t)
494− (cs, fmap update c)
495− (is, fmap update i)
496− (rs, fmap update r)
497−
498− update (P t (SymRef i) ty) = P t (syms!!i) ty
499− update (App f a) = App (update f) (update a)
500− update (Bind n b sc) = Bind n (fmap update b) (update sc)
501− update (Proj t i) = Proj (update t) i
502− update t = t
442+ = do t' <- updateSC t
443+ c' <- updateSC c
444+ i' <- updateSC i
445+ r' <- updateSC r
446+ return $ CaseDefs (ts, t') (cs, c') (is, i') (rs, r')
447+
448+ updateSC (Case t n alts) = do alts' <- mapM updateAlt alts
449+ return (Case t n alts')
450+ updateSC (ProjCase t alts) = do alts' <- mapM updateAlt alts
451+ return (ProjCase t alts')
452+ updateSC (STerm t) = do t' <- update t
453+ return (STerm t')
454+ updateSC c = return c
455+
456+ updateAlt (ConCase n i ns t) = do t' <- updateSC t
457+ return (ConCase n i ns t')
458+ updateAlt (FnCase n ns t) = do t' <- updateSC t
459+ return (FnCase n ns t')
460+ updateAlt (ConstCase c t) = do t' <- updateSC t
461+ return (ConstCase c t')
462+ updateAlt (SucCase n t) = do t' <- updateSC t
463+ return (SucCase n t')
464+ updateAlt (DefaultCase t) = do t' <- updateSC t
465+ return (DefaultCase t')
466+
467+ update (P t n ty) = do n' <- getSymbol n
468+ return $ P t n' ty
469+ update (App f a) = liftM2 App (update f) (update a)
470+ update (Bind n b sc) = do b' <- updateB b
471+ sc' <- update sc
472+ return $ Bind n b' sc'
473+ where
474+ updateB (Let t v) = liftM2 Let (update t) (update v)
475+ updateB b = do ty' <- update (binderTy b)
476+ return (b { binderTy = ty' })
477+ update (Proj t i) = do t' <- update t
478+ return $ Proj t' i
479+ update t = return t
503480
504481pDocs :: [(Name, (Docstring D.DocTerm, [(Name, Docstring D.DocTerm)]))] -> Idris ()
505482pDocs ds = mapM_ (\ (n, a) -> addDocStr n (fst a) (snd a)) ds