on master help sign in
Set reduction limits on non-total functions in PE
7037cb0Edwin Brady
src/Idris/Elab/Clause.hs+6−1
@@ -338,10 +338,15 @@ elabPE info fc caller r =
338 -- want to be a PE version of those next)
338 -- want to be a PE version of those next)
339 let cgns' = filter (\x -> x /= n &&
339 let cgns' = filter (\x -> x /= n &&
340 notStatic ist x) cgns
340 notStatic ist x) cgns
341+ -- set small reduction limit on partial/productive things
342+ let maxred = case lookupTotal n (tt_ctxt ist) of
343+ [Total _] -> 65536
344+ [Productive] -> 16
345+ _ -> 1
341 let opts = [Specialise ((if pe_simple specdecl
346 let opts = [Specialise ((if pe_simple specdecl
342 then map (\x -> (x, Nothing)) cgns'
347 then map (\x -> (x, Nothing)) cgns'
343 else []) ++
348 else []) ++
344− (n, Just 65536) :
349+ (n, Just maxred) :
345 mapMaybe (specName (pe_simple specdecl))
350 mapMaybe (specName (pe_simple specdecl))
346 (snd specapp))]
351 (snd specapp))]
347 logLvl 3 $ "Specialising application: " ++ show specapp
352 logLvl 3 $ "Specialising application: " ++ show specapp