8df6b32 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

prim__believeMe needs to be considered total

The point of it being that it's believed to be total, even though it obviously isn't, so that things can reduce using it

commit8df6b326c6ab42f9bb42a9d447a7ba34415b728b authorEdwin Brady <ecb10@st-andrews.ac.uk> dateTue 29 Mar 2016, 17:34 (11 years ago) parentfaa58ad

2 files changed+9−7

compare with master

unifiedsplit

src/Idris/Core/Evaluate.hs+6−6 src/Idris/ElabDecls.hs+3−1

src/Idris/Core/Evaluate.hs+6−6

@@ -246,12 +246,11 @@ eval traceon ctxt ntimes genv tm opts = ev ntimes [] True [] tm where

246246 | not top && hnf = liftM (VP Ref n) (ev ntimes stk top env ty)

247247 | otherwise

248248 = 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)

250251 if red then

251252 do let val = lookupDefAcc n (spec || atRepl || runtime) ctxt

252253 case val of

253− [(Function _ tm, _)] | sUN "assert_total" `elem` stk ->

254− ev ntimes (n:stk) True env tm

255254 [(Function _ tm, Public)] ->

256255 ev ntimes (n:stk) True env tm

257256 [(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

371370 _ -> return $ unload env f args

372371 | otherwise

373372 = 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)

375375 if red then

376376 do let val = lookupDefAcc n (spec || atRepl || runtime) ctxt

377377 case val of

378378 [(CaseOp ci _ _ _ _ cd, acc)]

379− | acc == Public || acc == Hidden || sUN "assert_total" `elem` stk ->

379+ | acc == Public || acc == Hidden ->

380380 -- unoptimised version

381381 let (ns, tree) = getCases cd in

382382 if blockSimplify ci n stk

@@ -1094,7 +1094,7 @@ lookupTotalExact n ctxt = fmap mkt $ lookupCtxtExact n (definitions ctxt)

10941094-- are not reducible (so treated as a constant)

10951095tcReducible :: Name -> Context -> Bool

10961096tcReducible n ctxt = case lookupTotalExact n ctxt of

1097− Nothing -> False

1097+ Nothing -> True

10981098 Just (Partial _) -> False

10991099 _ -> True

11001100

src/Idris/ElabDecls.hs+3−1

@@ -111,7 +111,9 @@ elabPrims = do mapM_ (elabDecl' EAll recinfo)

111111 elabBelieveMe

112112 = do let prim__believe_me = sUN "prim__believe_me"

113113 updateContext (addOperator prim__believe_me believeTy 3 p_believeMe)

114− setTotality prim__believe_me (Partial NotCovering)

114+ -- The point is that it is believed to be total, even

115+ -- though it clearly isn't :)

116+ setTotality prim__believe_me (Total [])

115117 i <- getIState

116118 putIState i {

117119 idris_scprims = (prim__believe_me, (3, LNoOp)) : idris_scprims i