@@ -35,10 +35,10 @@ toplevel = EInfo [] emptyContext id Nothing
3535
3636-- Also find deferred names in the term and their types
3737
38−build :: IState -> ElabInfo -> Bool -> Name -> PTerm ->
38+build :: IState -> ElabInfo -> Bool -> FnOpts -> Name -> PTerm ->
3939 ElabD (Term, [(Name, (Int, Maybe Name, Type))], [PDecl])
40−build ist info pattern fn tm
41− = do elab ist info pattern False fn tm
40+build ist info pattern opts fn tm
41+ = do elab ist info pattern opts fn tm
4242 ivs <- get_instances
4343 hs <- get_holes
4444 ptm <- get_term
@@ -75,10 +75,10 @@ build ist info pattern fn tm
7575-- (Separate, so we don't go overboard resolving things that we don't
7676-- know about yet on the LHS of a pattern def)
7777
78−buildTC :: IState -> ElabInfo -> Bool -> Bool -> Name -> PTerm ->
78+buildTC :: IState -> ElabInfo -> Bool -> FnOpts -> Name -> PTerm ->
7979 ElabD (Term, [(Name, (Int, Maybe Name, Type))], [PDecl])
80−buildTC ist info pattern tcgen fn tm
81− = do elab ist info pattern tcgen fn tm
80+buildTC ist info pattern opts fn tm
81+ = do elab ist info pattern opts fn tm
8282 probs <- get_probs
8383 tm <- get_term
8484 case probs of
@@ -94,19 +94,22 @@ buildTC ist info pattern tcgen fn tm
9494-- Returns the set of declarations we need to add to complete the definition
9595-- (most likely case blocks to elaborate)
9696
97−elab :: IState -> ElabInfo -> Bool -> Bool -> Name -> PTerm ->
97+elab :: IState -> ElabInfo -> Bool -> FnOpts -> Name -> PTerm ->
9898 ElabD ()
99−elab ist info pattern tcgen fn tm
99+elab ist info pattern opts fn tm
100100 = do let loglvl = opt_logLevel (idris_options ist)
101101 when (loglvl > 5) $ unifyLog True
102102 compute -- expand type synonyms, etc
103− elabE (False, False) tm -- (in argument, guarded)
103+ elabE (False, False, False) tm -- (in argument, guarded, in type)
104104 end_unify
105105 when pattern -- convert remaining holes to pattern vars
106106 (do update_term orderPats
107107 tm <- get_term
108108 mkPat)
109109 where
110+ tcgen = Dictionary `elem` opts
111+ reflect = Reflection `elem` opts
112+
110113 isph arg = case getTm arg of
111114 Placeholder -> (True, priority arg)
112115 _ -> (False, priority arg)
@@ -125,6 +128,7 @@ elab ist info pattern tcgen fn tm
125128 (h: hs) -> do patvar h; mkPat
126129 [] -> return ()
127130
131+ elabE :: (Bool, Bool, Bool) -> PTerm -> ElabD ()
128132 elabE ina t = {- do g <- goal
129133 tm <- get_term
130134 trace ("Elaborating " ++ show t ++ " : " ++ show g ++ "\n\tin " ++ show tm)
@@ -144,9 +148,18 @@ elab ist info pattern tcgen fn tm
144148
145149 local f = do e <- get_env
146150 return (f `elem` map fst e)
151+
152+ constType (AType _) = True
153+ constType StrType = True
154+ constType PtrType = True
155+ constType VoidType = True
156+ constType _ = False
147157
148158 elab' ina (PNoImplicits t) = elab' ina t -- skip elabE step
149159 elab' ina PType = do apply RType []; solve
160+ elab' (_,_,inty) (PConstant c)
161+ | constType c && pattern && not reflect && not inty
162+ = lift $ tfail (Msg "Typecase is not allowed")
150163 elab' ina (PConstant c) = do apply (RConstant c) []; solve
151164 elab' ina (PQuote r) = do fill r; solve
152165 elab' ina (PTrue fc) = try (elab' ina (PRef fc unitCon))
@@ -168,13 +181,13 @@ elab ist info pattern tcgen fn tm
168181 [pimp (MN 0 "a") Placeholder True,
169182 pimp (MN 0 "b") Placeholder False,
170183 pexp l, pexp r])
171− elab' ina@(_, a) (PPair fc l r)
184+ elab' ina@(_, a, inty) (PPair fc l r)
172185 = do hnf_compute
173186 g <- goal
174187 case g of
175− TType _ -> elabE (True, a) (PApp fc (PRef fc pairTy)
176− [pexp l,pexp r])
177− _ -> elabE (True, a) (PApp fc (PRef fc pairCon)
188+ TType _ -> elabE (True, a,inty) (PApp fc (PRef fc pairTy)
189+ [pexp l,pexp r])
190+ _ -> elabE (True, a, inty) (PApp fc (PRef fc pairCon)
178191 [pimp (MN 0 "A") Placeholder True,
179192 pimp (MN 0 "B") Placeholder True,
180193 pexp l, pexp r])
@@ -222,7 +235,10 @@ elab ist info pattern tcgen fn tm
222235 trySeq' deferr (x : xs)
223236 = try' (elab' ina x) (trySeq' deferr xs) True
224237 elab' ina (PPatvar fc n) | pattern = patvar n
225− elab' (ina, guarded) (PRef fc n) | pattern && not (inparamBlock n)
238+ elab' (_, _, inty) (PRef fc f)
239+ | isTConName f (tt_ctxt ist) && pattern && not reflect && not inty
240+ = lift $ tfail (Msg "Typecase is not allowed")
241+ elab' (ina, guarded, inty) (PRef fc n) | pattern && not (inparamBlock n)
226242 = do ctxt <- get_context
227243 let defined = case lookupTy n ctxt of
228244 [] -> False
@@ -239,7 +255,7 @@ elab ist info pattern tcgen fn tm
239255 _ -> True
240256 elab' ina f@(PInferRef fc n) = elab' ina (PApp fc f [])
241257 elab' ina (PRef fc n) = erun fc $ do apply (Var n) []; solve
242− elab' ina@(_, a) (PLam n Placeholder sc)
258+ elab' ina@(_, a, inty) (PLam n Placeholder sc)
243259 = do -- n' <- unique_hole n
244260 -- let sc' = mapPT (repN n n') sc
245261 ptm <- get_term
@@ -247,10 +263,10 @@ elab ist info pattern tcgen fn tm
247263 checkPiGoal n
248264 attack; intro (Just n);
249265 -- trace ("------ intro " ++ show n ++ " ---- \n" ++ show ptm)
250− elabE (True, a) sc; solve
266+ elabE (True, a, inty) sc; solve
251267 where repN n n' (PRef fc x) | x == n' = PRef fc n'
252268 repN _ _ t = t
253− elab' ina@(_, a) (PLam n ty sc)
269+ elab' ina@(_, a, inty) (PLam n ty sc)
254270 = do hsin <- get_holes
255271 ptmin <- get_term
256272 tyn <- unique_hole (MN 0 "lamty")
@@ -265,12 +281,12 @@ elab ist info pattern tcgen fn tm
265281 introTy (Var tyn) (Just n)
266282 -- end_unify
267283 focus tyn
268− elabE (True, a) ty
269− elabE (True, a) sc
284+ elabE (True, a, True) ty
285+ elabE (True, a, inty) sc
270286 solve
271− elab' ina@(_,a) (PPi _ n Placeholder sc)
272− = do attack; arg n (MN 0 "ty"); elabE (True, a) sc; solve
273− elab' ina@(_,a) (PPi _ n ty sc)
287+ elab' ina@(_, a, _) (PPi _ n Placeholder sc)
288+ = do attack; arg n (MN 0 "ty"); elabE (True, a, True) sc; solve
289+ elab' ina@(_, a, _) (PPi _ n ty sc)
274290 = do attack; tyn <- unique_hole (MN 0 "ty")
275291 claim tyn RType
276292 n' <- case n of
@@ -278,10 +294,10 @@ elab ist info pattern tcgen fn tm
278294 _ -> return n
279295 forall n' (Var tyn)
280296 focus tyn
281− elabE (True, a) ty
282− elabE (True, a) sc
297+ elabE (True, a, True) ty
298+ elabE (True, a, True) sc
283299 solve
284− elab' ina@(_,a) (PLet n ty val sc)
300+ elab' ina@(_, a, inty) (PLet n ty val sc)
285301 = do attack;
286302 tyn <- unique_hole (MN 0 "letty")
287303 claim tyn RType
@@ -293,17 +309,17 @@ elab ist info pattern tcgen fn tm
293309 Placeholder -> return ()
294310 _ -> do focus tyn
295311 explicit tyn
296− elabE (True, a) ty
312+ elabE (True, a, True) ty
297313 focus valn
298− elabE (True, a) val
314+ elabE (True, a, True) val
299315 env <- get_env
300− elabE (True, a) sc
316+ elabE (True, a, inty) sc
301317 -- HACK: If the name leaks into its type, it may leak out of
302318 -- scope outside, so substitute in the outer scope.
303319 expandLet n (case lookup n env of
304320 Just (Let t v) -> v)
305321 solve
306− elab' ina@(_,a) (PGoal fc r n sc) = do
322+ elab' ina@(_, a, inty) (PGoal fc r n sc) = do
307323 rty <- goal
308324 attack
309325 tyn <- unique_hole (MN 0 "letty")
@@ -312,10 +328,10 @@ elab ist info pattern tcgen fn tm
312328 claim valn (Var tyn)
313329 letbind n (Var tyn) (Var valn)
314330 focus valn
315− elabE (True, a) (PApp fc r [pexp (delab ist rty)])
331+ elabE (True, a, True) (PApp fc r [pexp (delab ist rty)])
316332 env <- get_env
317333 computeLet n
318− elabE (True, a) sc
334+ elabE (True, a, inty) sc
319335 solve
320336-- elab' ina (PLet n Placeholder
321337-- (PApp fc r [pexp (delab ist rty)]) sc)
@@ -365,14 +381,17 @@ elab ist info pattern tcgen fn tm
365381 Just xs@(_:_) -> NS n xs
366382 _ -> n
367383
368− elab' (ina, g) (PMatchApp fc fn)
384+ elab' ina (PMatchApp fc fn)
369385 = do (fn', imps) <- case lookupCtxtName fn (idris_implicits ist) of
370386 [(n, args)] -> return (n, map (const True) args)
371387 _ -> lift $ tfail (NoSuchVariable fn)
372388 ns <- match_apply (Var fn') (map (\x -> (x,0)) imps)
373389 solve
390+ elab' (_, _, inty) (PApp fc (PRef _ f) args')
391+ | isTConName f (tt_ctxt ist) && pattern && not reflect && not inty
392+ = lift $ tfail (Msg "Typecase is not allowed")
374393 -- if f is local, just do a simple_app
375− elab' (ina, g) tm@(PApp fc (PRef _ f) args')
394+ elab' (ina, g, inty) tm@(PApp fc (PRef _ f) args')
376395 = do let args = {- case lookupCtxt f (inblock info) of
377396 Just ps -> (map (pexp . (PRef fc)) ps ++ args')
378397 _ -> -} args'
@@ -380,8 +399,8 @@ elab ist info pattern tcgen fn tm
380399 env <- get_env
381400 if (f `elem` map fst env && length args' == 1)
382401 then -- simple app, as below
383− do simple_app (elabE (ina, g) (PRef fc f))
384− (elabE (True, g) (getTm (head args')))
402+ do simple_app (elabE (ina, g, inty) (PRef fc f))
403+ (elabE (True, g, inty) (getTm (head args')))
385404 (show tm)
386405 solve
387406 else
@@ -405,7 +424,7 @@ elab ist info pattern tcgen fn tm
405424 sortBy (\(_,x) (_,y) ->
406425 compare (priority x) (priority y))
407426 (zip ns args)
408− elabArgs (ina || not isinf, guarded)
427+ elabArgs (ina || not isinf, guarded, inty)
409428 [] fc False ns' (map (\x -> (lazyarg x, getTm x)) eargs)
410429 mkSpecialised ist fc f (map getTm args') tm
411430 solve
@@ -436,9 +455,9 @@ elab ist info pattern tcgen fn tm
436455 setInjective (PApp _ (PRef _ n) _) = setinj n
437456 setInjective _ = return ()
438457
439− elab' ina@(_, a) tm@(PApp fc f [arg])
458+ elab' ina@(_, a, inty) tm@(PApp fc f [arg])
440459 = erun fc $
441− do simple_app (elabE ina f) (elabE (True, a) (getTm arg))
460+ do simple_app (elabE ina f) (elabE (True, a, inty) (getTm arg))
442461 (show tm)
443462 solve
444463 elab' ina Placeholder = do (h : hs) <- get_holes
@@ -487,7 +506,7 @@ elab ist info pattern tcgen fn tm
487506 elab' ina sc
488507 elab' ina (PRef fc letn)
489508 solve
490− elab' ina@(_, a) c@(PCase fc scr opts)
509+ elab' ina@(_, a, inty) c@(PCase fc scr opts)
491510 = do attack
492511 tyn <- unique_hole (MN 0 "scty")
493512 claim tyn RType
@@ -496,7 +515,7 @@ elab ist info pattern tcgen fn tm
496515 claim valn (Var tyn)
497516 letbind scvn (Var tyn) (Var valn)
498517 focus valn
499− elabE (True, a) scr
518+ elabE (True, a, inty) scr
500519 args <- get_env
501520 cname <- unique_hole' True (mkCaseName fn)
502521 let cname' = mkN cname
@@ -679,9 +698,9 @@ findInstances ist t
679698 | otherwise = []
680699
681700trivial' ist
682− = trivial (elab ist toplevel False False (MN 0 "tac")) ist
701+ = trivial (elab ist toplevel False [] (MN 0 "tac")) ist
683702proofSearch' ist top n hints
684− = proofSearch (elab ist toplevel False False (MN 0 "tac")) top n hints ist
703+ = proofSearch (elab ist toplevel False [] (MN 0 "tac")) top n hints ist
685704
686705
687706resolveTC :: Int -> Term -> Name -> IState -> ElabD ()
@@ -810,7 +829,7 @@ runTac autoSolve ist tac
810829 where
811830 bname (Bind n _ _) = Just n
812831 bname _ = Nothing
813− runT (Exact tm) = do elab ist toplevel False False (MN 0 "tac") tm
832+ runT (Exact tm) = do elab ist toplevel False [] (MN 0 "tac") tm
814833 when autoSolve solveAll
815834 runT (MatchRefine fn)
816835 = do fnimps <-
@@ -857,7 +876,7 @@ runTac autoSolve ist tac
857876 letn <- unique_hole (MN 0 "equiv_val")
858877 letbind letn (Var tyn) (Var valn)
859878 focus tyn
860− elab ist toplevel False False (MN 0 "tac") tm
879+ elab ist toplevel False [] (MN 0 "tac") tm
861880 focus valn
862881 when autoSolve solveAll
863882 runT (Rewrite tm) -- to elaborate tm, let bind it, then rewrite by that
@@ -870,7 +889,7 @@ runTac autoSolve ist tac
870889 letn <- unique_hole (MN 0 "rewrite_rule")
871890 letbind letn (Var tyn) (Var valn)
872891 focus valn
873− elab ist toplevel False False (MN 0 "tac") tm
892+ elab ist toplevel False [] (MN 0 "tac") tm
874893 rewrite (Var letn)
875894 when autoSolve solveAll
876895 runT (Induction nm)
@@ -885,7 +904,7 @@ runTac autoSolve ist tac
885904 letn <- unique_hole n
886905 letbind letn (Var tyn) (Var valn)
887906 focus valn
888− elab ist toplevel False False (MN 0 "tac") tm
907+ elab ist toplevel False [] (MN 0 "tac") tm
889908 when autoSolve solveAll
890909 runT (LetTacTy n ty tm)
891910 = do attack
@@ -896,9 +915,9 @@ runTac autoSolve ist tac
896915 letn <- unique_hole n
897916 letbind letn (Var tyn) (Var valn)
898917 focus tyn
899− elab ist toplevel False False (MN 0 "tac") ty
918+ elab ist toplevel False [] (MN 0 "tac") ty
900919 focus valn
901− elab ist toplevel False False (MN 0 "tac") tm
920+ elab ist toplevel False [] (MN 0 "tac") tm
902921 when autoSolve solveAll
903922 runT Compute = compute
904923 runT Trivial = do trivial' ist; when autoSolve solveAll
@@ -916,7 +935,7 @@ runTac autoSolve ist tac
916935 scriptvar <- unique_hole (MN 0 "scriptvar" )
917936 letbind scriptvar scriptTy (Var script)
918937 focus script
919− elab ist toplevel False False (MN 0 "tac") tm
938+ elab ist toplevel False [] (MN 0 "tac") tm
920939 (script', _) <- get_type_val (Var scriptvar)
921940 -- now that we have the script apply
922941 -- it to the reflected goal and context
@@ -949,7 +968,7 @@ runTac autoSolve ist tac
949968 letbind scriptvar scriptTy (Var script)
950969 focus script
951970 ptm <- get_term
952− elab ist toplevel False False (MN 0 "tac")
971+ elab ist toplevel False [] (MN 0 "tac")
953972 (PApp emptyFC tm [pexp (delabTy' ist [] tgoal True True)])
954973 (script', _) <- get_type_val (Var scriptvar)
955974 -- now that we have the script apply
@@ -977,7 +996,7 @@ runTac autoSolve ist tac
977996 letn <- unique_hole (MN 0 "letvar")
978997 letbind letn (Var tyn) (Var valn)
979998 focus valn
980− elab ist toplevel False False (MN 0 "tac") v
999+ elab ist toplevel False [] (MN 0 "tac") v
9811000 (value, _) <- get_type_val (Var letn)
9821001 ctxt <- get_context
9831002 env <- get_env
@@ -991,7 +1010,7 @@ runTac autoSolve ist tac
9911010 letn <- unique_hole (MN 0 "letvar")
9921011 letbind letn (Var tyn) (Var valn)
9931012 focus valn
994− elab ist toplevel False False (MN 0 "tac") v
1013+ elab ist toplevel False [] (MN 0 "tac") v
9951014 (value, _) <- get_type_val (Var letn)
9961015 ctxt <- get_context
9971016 env <- get_env