@@ -80,10 +80,11 @@ elabClauses info' fc opts n_in cs =
8080 let atys = map snd (getArgTys fty)
8181 cs_elab <- mapM (elabClause info opts)
8282 (zip [0..] cs)
83+ ctxt <- getContext
8384 -- pats_raw is the version we'll work with at compile time:
8485 -- no simplification or PE
8586 let (pats_in, cs_full) = unzip cs_elab
86− let pats_raw = map (simple_lhs (tt_ctxt ist)) pats_in
87+ let pats_raw = map (simple_lhs ctxt) pats_in
8788 logElab 3 $ "Elaborated patterns:\n" ++ show pats_raw
8889
8990 solveDeferred n
@@ -93,6 +94,7 @@ elabClauses info' fc opts n_in cs =
9394 addIBC (IBCOpt n)
9495
9596 ist <- getIState
97+ ctxt <- getContext
9698 -- Don't apply rules if this is a partial evaluation definition,
9799 -- or we'll make something that just runs itself!
98100 let tpats = case specNames opts of
@@ -103,7 +105,7 @@ elabClauses info' fc opts n_in cs =
103105 -- RHS
104106 pe_tm <- doPartialEval ist tpats
105107 let pats_pe = if petrans
106− then map (simple_lhs (tt_ctxt ist)) pe_tm
108+ then map (simple_lhs ctxt) pe_tm
107109 else pats_raw
108110
109111 let tcase = opt_typecase (idris_options ist)
@@ -183,7 +185,8 @@ elabClauses info' fc opts n_in cs =
183185 -- pdef' is the version that gets compiled for run-time,
184186 -- so we start from the partially evaluated version
185187 pdef_in' <- applyOpts $ map (\(ns, lhs, rhs) -> (map fst ns, lhs, rhs)) pdef_pe
186− let pdef' = map (simple_rt (tt_ctxt ist)) pdef_in'
188+ ctxt <- getContext
189+ let pdef' = map (simple_rt ctxt) pdef_in'
187190
188191 logElab 5 $ "After data structure transformations:\n" ++ show pdef'
189192
@@ -247,7 +250,8 @@ elabClauses info' fc opts n_in cs =
247250 defer_totcheck (fc, n)
248251 when (tot /= Unchecked) $ addIBC (IBCTotal n tot)
249252 i <- getIState
250− case lookupDef n (tt_ctxt i) of
253+ ctxt <- getContext
254+ case lookupDef n ctxt of
251255 (CaseOp _ _ _ _ _ cd : _) ->
252256 let (scargs, sc) = cases_compiletime cd in
253257 do let calls = map fst $ findCalls sc scargs
@@ -349,11 +353,12 @@ elabPE info fc caller r =
349353 mkSpecialised :: (Name, [(PEArgType, Term)]) -> Idris [(Term, Term)]
350354 mkSpecialised specapp_in = do
351355 ist <- getIState
356+ ctxt <- getContext
352357 let (specTy, specapp) = getSpecTy ist specapp_in
353358 let (n, newnm, specdecl) = getSpecClause ist specapp
354359 let lhs = pe_app specdecl
355360 let rhs = pe_def specdecl
356− let undef = case lookupDefExact newnm (tt_ctxt ist) of
361+ let undef = case lookupDefExact newnm ctxt of
357362 Nothing -> True
358363 _ -> False
359364 logElab 5 $ show (newnm, undef, map (concreteArg ist) (snd specapp))
@@ -366,7 +371,7 @@ elabPE info fc caller r =
366371 let cgns' = filter (\x -> x /= n &&
367372 notStatic ist x) cgns
368373 -- set small reduction limit on partial/productive things
369− let maxred = case lookupTotal n (tt_ctxt ist) of
374+ let maxred = case lookupTotal n ctxt of
370375 [Total _] -> 65536
371376 [Productive] -> 16
372377 _ -> 1
@@ -481,7 +486,7 @@ checkPossible info fc tcgen fname lhs_in
481486 processTacticDecls info newDecls
482487 sendHighlighting highlights
483488 let lhs_tm = orderPats (getInferTerm lhs')
484− case recheck ctxt [] (forget lhs_tm) lhs_tm of
489+ case recheck ctxt' [] (forget lhs_tm) lhs_tm of
485490 OK _ -> return True
486491 err -> return False
487492 -- if it's a recoverable error, the case may become possible
@@ -554,7 +559,7 @@ elabClause info opts (cnum, PClause fc fname lhs_in_as withs rhs_in_as wherebloc
554559 (Msg "unexpected patterns outside of \"with\" block")))
555560
556561 -- get the parameters first, to pass through to any where block
557− let fn_ty = case lookupTy fname (tt_ctxt i) of
562+ let fn_ty = case lookupTy fname ctxt of
558563 [t] -> t
559564 _ -> error "Can't happen (elabClause function type)"
560565 let fn_is = case lookupCtxt fname (idris_implicits i) of
@@ -598,6 +603,7 @@ elabClause info opts (cnum, PClause fc fname lhs_in_as withs rhs_in_as wherebloc
598603
599604 -- If we're inferring metavariables in the type, don't recheck,
600605 -- because we're only doing this to try to work out those metavariables
606+ ctxt <- getContext
601607 (clhs_c, clhsty) <- if not inf
602608 then recheckC_borrowing False (PEGenerated `notElem` opts)
603609 [] fc id [] lhs_tm
@@ -623,6 +629,8 @@ elabClause info opts (cnum, PClause fc fname lhs_in_as withs rhs_in_as wherebloc
623629 logElab 5 ("Checked " ++ show clhs ++ "\n" ++ show clhsty)
624630 -- Elaborate where block
625631 ist <- getIState
632+ ctxt <- getContext
633+
626634 windex <- getName
627635 let decls = nub (concatMap declared whereblock)
628636 let defs = nub (decls ++ concatMap defined whereblock)
@@ -631,7 +639,7 @@ elabClause info opts (cnum, PClause fc fname lhs_in_as withs rhs_in_as wherebloc
631639 -- Unique arguments must be passed to the where block explicitly
632640 -- (since we can't control "usage" easlily otherwise). Remove them
633641 -- from newargs here
634− let uniqargs = findUnique (tt_ctxt ist) [] lhs_tm
642+ let uniqargs = findUnique ctxt [] lhs_tm
635643 let newargs = filter (\(n,_) -> n `notElem` uniqargs) newargs_all
636644
637645 let winfo = (pinfo info newargs defs windex) { elabFC = Just fc }
@@ -794,7 +802,7 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in pn_in withblock)
794802 -- pattern bindings
795803 i <- getIState
796804 -- get the parameters first, to pass through to any where block
797− let fn_ty = case lookupTy fname (tt_ctxt i) of
805+ let fn_ty = case lookupTy fname ctxt of
798806 [t] -> t
799807 _ -> error "Can't happen (elabClause function type)"
800808 let fn_is = case lookupCtxt fname (idris_implicits i) of
@@ -815,6 +823,7 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in pn_in withblock)
815823 processTacticDecls info newDecls
816824 sendHighlighting highlights
817825
826+ ctxt <- getContext
818827 let lhs_tm = orderPats (getInferTerm lhs')
819828 let lhs_ty = getInferType lhs'
820829 let ret_ty = getRetTy (explicitNames (normalise ctxt [] lhs_ty))
@@ -848,6 +857,8 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in pn_in withblock)
848857 addDeferred def''
849858 mapM_ (elabCaseBlock info opts) is
850859 logElab 5 ("Checked wval " ++ show wval')
860+
861+ ctxt <- getContext
851862 (cwval, cwvalty) <- recheckC fc id [] (getInferTerm wval')
852863 let cwvaltyN = explicitNames (normalise ctxt [] cwvalty)
853864 let cwvalN = explicitNames (normalise ctxt [] cwval)