@@ -62,7 +62,7 @@ elabType info syn doc fc opts n ty' = {- let ty' = piBind (params info) ty_in
6262 (errAt "type of " n (erun fc (build i info False n ty)))
6363 ds <- checkDef fc defer
6464 addDeferred ds
65− mapM_ (elabCaseBlock info) is
65+ mapM_ (elabCaseBlock info opts) is
6666 ctxt <- getContext
6767 logLvl 5 $ "Rechecking"
6868 logLvl 6 $ show tyT
@@ -128,7 +128,7 @@ elabData info syn doc fc codata (PLaterdecl n t_in)
128128 (erun fc (build i info False n t))
129129 def' <- checkDef fc defer
130130 addDeferredTyCon def'
131− mapM_ (elabCaseBlock info) is
131+ mapM_ (elabCaseBlock info []) is
132132 (cty, _) <- recheckC fc [] t'
133133 logLvl 2 $ "---> " ++ show cty
134134 updateContext (addTyDecl n (TCon 0 0) cty) -- temporary, to check cons
@@ -145,7 +145,7 @@ elabData info syn doc fc codata (PDatadecl n t_in dcons)
145145 (errAt "data declaration " n (erun fc (build i info False n t)))
146146 def' <- checkDef fc defer
147147 addDeferredTyCon def'
148− mapM_ (elabCaseBlock info) is
148+ mapM_ (elabCaseBlock info []) is
149149 (cty, _) <- recheckC fc [] t'
150150 logLvl 2 $ "---> " ++ show cty
151151 -- temporary, to check cons
@@ -492,7 +492,7 @@ elabCon info syn tn codata (doc, n, t_in, fc)
492492 logLvl 2 $ "Rechecking " ++ show t'
493493 def' <- checkDef fc defer
494494 addDeferred def'
495− mapM_ (elabCaseBlock info) is
495+ mapM_ (elabCaseBlock info []) is
496496 ctxt <- getContext
497497 (cty, _) <- recheckC fc [] t'
498498 let cty' = normaliseC ctxt [] cty
@@ -528,7 +528,7 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in
528528 -- question: CAFs in where blocks?
529529 tclift $ tfail $ At fc (NoTypeDecl n)
530530 [ty] -> return ty
531− pats_in <- mapM (elabClause info (Dictionary `elem` opts))
531+ pats_in <- mapM (elabClause info opts)
532532 (zip [0..] cs)
533533 logLvl 3 $ "Elaborated patterns:\n" ++ show pats_in
534534
@@ -748,7 +748,7 @@ elabVal info aspat tm_in
748748 (build i info aspat (MN 0 "val") (infTerm tm)))
749749 def' <- checkDef (FC "(input)" 0) defer
750750 addDeferred def'
751− mapM_ (elabCaseBlock info) is
751+ mapM_ (elabCaseBlock info []) is
752752
753753 logLvl 3 ("Value: " ++ show tm')
754754 recheckC (FC "(input)" 0) [] tm'
@@ -778,16 +778,18 @@ checkPossible info fc tcgen fname lhs_in
778778-- trace (show (delab' i lhs_tm True) ++ "\n" ++ show lhs) $ return (not b)
779779 err@(Error _) -> return False
780780
781−elabClause :: ElabInfo -> Bool -> (Int, PClause) ->
781+elabClause :: ElabInfo -> FnOpts -> (Int, PClause) ->
782782 Idris (Either Term (Term, Term))
783−elabClause info tcgen (_, PClause fc fname lhs_in [] PImpossible [])
784− = do b <- checkPossible info fc tcgen fname lhs_in
783+elabClause info opts (_, PClause fc fname lhs_in [] PImpossible [])
784+ = do let tcgen = Dictionary `elem` opts
785+ b <- checkPossible info fc tcgen fname lhs_in
785786 case b of
786787 True -> fail $ show fc ++ ":" ++ show lhs_in ++ " is a possible case"
787788 False -> do ptm <- mkPatTm lhs_in
788789 return (Left ptm)
789−elabClause info tcgen (cnum, PClause fc fname lhs_in withs rhs_in whereblock)
790− = do ctxt <- getContext
790+elabClause info opts (cnum, PClause fc fname lhs_in withs rhs_in whereblock)
791+ = do let tcgen = Dictionary `elem` opts
792+ ctxt <- getContext
791793 -- Build the LHS as an "Infer", and pull out its type and
792794 -- pattern bindings
793795 i <- getIState
@@ -857,7 +859,7 @@ elabClause info tcgen (cnum, PClause fc fname lhs_in withs rhs_in whereblock)
857859 -- from the where block
858860
859861 mapM_ (elabDecl' EAll info) wafter
860− mapM_ (elabCaseBlock info) is
862+ mapM_ (elabCaseBlock info opts) is
861863
862864 ctxt <- getContext
863865 logLvl 5 $ "Rechecking"
@@ -937,8 +939,9 @@ elabClause info tcgen (cnum, PClause fc fname lhs_in withs rhs_in whereblock)
937939 = PApp fc (PRef fc n) (map (\x -> pimp x (PRef fc x)) ps)
938940 propagateParams ps x = x
939941
940−elabClause info tcgen (_, PWith fc fname lhs_in withs wval_in withblock)
941− = do ctxt <- getContext
942+elabClause info opts (_, PWith fc fname lhs_in withs wval_in withblock)
943+ = do let tcgen = Dictionary `elem` opts
944+ ctxt <- getContext
942945 -- Build the LHS as an "Infer", and pull out its type and
943946 -- pattern bindings
944947 i <- getIState
@@ -970,7 +973,7 @@ elabClause info tcgen (_, PWith fc fname lhs_in withs wval_in withblock)
970973 return (tt, d, is))
971974 def' <- checkDef fc defer
972975 addDeferred def'
973− mapM_ (elabCaseBlock info) is
976+ mapM_ (elabCaseBlock info opts) is
974977 (cwval, cwvalty) <- recheckC fc [] (getInferTerm wval')
975978 let cwvaltyN = explicitNames cwvalty
976979 let cwvalN = explicitNames cwval
@@ -1026,7 +1029,7 @@ elabClause info tcgen (_, PWith fc fname lhs_in withs wval_in withblock)
10261029 return (tt, d, is))
10271030 def' <- checkDef fc defer
10281031 addDeferred def'
1029− mapM_ (elabCaseBlock info) is
1032+ mapM_ (elabCaseBlock info opts) is
10301033 logLvl 5 ("Checked RHS " ++ show rhs')
10311034 (crhs, crhsty) <- recheckC fc [] rhs'
10321035 return $ Right (clhs, crhs)
@@ -1549,10 +1552,10 @@ elabDecl' what info (PTransform fc safety old new)
15491552 = elabTransform info fc safety old new
15501553elabDecl' _ _ _ = return () -- skipped this time
15511554
1552−elabCaseBlock info d@(PClauses f o n ps)
1555+elabCaseBlock info opts d@(PClauses f o n ps)
15531556 = do addIBC (IBCDef n)
15541557 logLvl 6 $ "CASE BLOCK: " ++ show (n, d)
1555− elabDecl' EAll info d
1558+ elabDecl' EAll info (PClauses f (nub (o ++ opts)) n ps )
15561559
15571560-- elabDecl' info (PImport i) = loadModule i
15581561