git.iko.soy/Idris-dev
on master help sign in
prim__believeMe needs to be considered total
8df6b32Edwin Brady
src/Idris/Core/Evaluate.hs+6−6
compare with master
unifiedsplit
@@ -246,12 +246,11 @@ eval traceon ctxt ntimes genv tm opts = ev ntimes [] True [] tm where
246 | not top && hnf = liftM (VP Ref n) (ev ntimes stk top env ty)
246 | not top && hnf = liftM (VP Ref n) (ev ntimes stk top env ty)
247 | otherwise
247 | otherwise
248 = do (u, ntimes) <- usable spec n ntimes_in
248 = do (u, ntimes) <- usable spec n ntimes_in
249− let red = u && (tcReducible n ctxt || spec || atRepl || runtime)
249+ let red = u && (tcReducible n ctxt || spec || atRepl || runtime
250+ || sUN "assert_total" `elem` stk)
250 if red then
251 if red then
251 do let val = lookupDefAcc n (spec || atRepl || runtime) ctxt
252 do let val = lookupDefAcc n (spec || atRepl || runtime) ctxt
252 case val of
253 case val of
253− [(Function _ tm, _)] | sUN "assert_total" `elem` stk ->
254− ev ntimes (n:stk) True env tm
255 [(Function _ tm, Public)] ->
254 [(Function _ tm, Public)] ->
256 ev ntimes (n:stk) True env tm
255 ev ntimes (n:stk) True env tm
257 [(TyDecl nt ty, _)] -> do vty <- ev ntimes stk True env ty
256 [(TyDecl nt ty, _)] -> do vty <- ev ntimes stk True env ty
@@ -371,12 +370,13 @@ eval traceon ctxt ntimes genv tm opts = ev ntimes [] True [] tm where
371 _ -> return $ unload env f args
370 _ -> return $ unload env f args
372 | otherwise
371 | otherwise
373 = do (u, ntimes) <- usable spec n ntimes_in
372 = do (u, ntimes) <- usable spec n ntimes_in
374− let red = u && (tcReducible n ctxt || spec || atRepl || runtime)
373+ let red = u && (tcReducible n ctxt || spec || atRepl || runtime
374+ || sUN "assert_total" `elem` stk)
375 if red then
375 if red then
376 do let val = lookupDefAcc n (spec || atRepl || runtime) ctxt
376 do let val = lookupDefAcc n (spec || atRepl || runtime) ctxt
377 case val of
377 case val of
378 [(CaseOp ci _ _ _ _ cd, acc)]
378 [(CaseOp ci _ _ _ _ cd, acc)]
379− | acc == Public || acc == Hidden || sUN "assert_total" `elem` stk ->
379+ | acc == Public || acc == Hidden ->
380 -- unoptimised version
380 -- unoptimised version
381 let (ns, tree) = getCases cd in
381 let (ns, tree) = getCases cd in
382 if blockSimplify ci n stk
382 if blockSimplify ci n stk
@@ -1094,7 +1094,7 @@ lookupTotalExact n ctxt = fmap mkt $ lookupCtxtExact n (definitions ctxt)
1094-- are not reducible (so treated as a constant)
1094-- are not reducible (so treated as a constant)
1095tcReducible :: Name -> Context -> Bool
1095tcReducible :: Name -> Context -> Bool
1096tcReducible n ctxt = case lookupTotalExact n ctxt of
1096tcReducible n ctxt = case lookupTotalExact n ctxt of
1097− Nothing -> False
1097+ Nothing -> True
1098 Just (Partial _) -> False
1098 Just (Partial _) -> False
1099 _ -> True
1099 _ -> True
1100
1100
src/Idris/ElabDecls.hs+3−1
@@ -111,7 +111,9 @@ elabPrims = do mapM_ (elabDecl' EAll recinfo)
111 elabBelieveMe
111 elabBelieveMe
112 = do let prim__believe_me = sUN "prim__believe_me"
112 = do let prim__believe_me = sUN "prim__believe_me"
113 updateContext (addOperator prim__believe_me believeTy 3 p_believeMe)
113 updateContext (addOperator prim__believe_me believeTy 3 p_believeMe)
114+ -- The point is that it is believed to be total, even
115+ -- though it clearly isn't :)
114− setTotality prim__believe_me (Partial NotCovering)
116+ setTotality prim__believe_me (Total [])
115 i <- getIState
117 i <- getIState
116 putIState i {
118 putIState i {
117 idris_scprims = (prim__believe_me, (3, LNoOp)) : idris_scprims i
119 idris_scprims = (prim__believe_me, (3, LNoOp)) : idris_scprims i