idris-lang/Idris2
1
1
Fork 0
mirror of https://github.com/idris-lang/Idris2.git synced 2025-01-04 22:24:19 +03:00
Code Issues Projects Releases Wiki Activity

whitespace

Browse Source
This commit is contained in:
Mathew Polzin 2021-05-19 19:32:19 -07:00
parent d67e4fdebb
commit 11a1705674
1 changed files with 5 additions and 5 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

10
src/Core/CaseBuilder.idr
View File

@ -720,7 +720,7 @@ consScoreHeuristic scorePat (Scored xs ys) =
-- scoring the first column.
scoreFirstColumn : (nps : List (NamedPats ns (p' :: ps'))) -> (res : List (NamedPats ns ps') ** (LengthMatch nps res, Vect (length nps) Int))
scoreFirstColumn [] = ([] ** (NilMatch, []))
scoreFirstColumn ((w :: ws) :: nps) =
scoreFirstColumn ((w :: ws) :: nps) =
let (ws' ** (prf, scores)) = scoreFirstColumn nps
in (ws :: ws' ** (ConsMatch prf, scorePat (pat w) :: scores))
@ -757,10 +757,10 @@ heuristicB = consScoreHeuristic (headConsPenalty (\arity => if arity == 0 then 0
heuristicA : {ps : _} -> ScoredPats ns ps -> ScoredPats ns ps
heuristicA = consScoreHeuristic (headConsPenalty (negate . cast))
applyHeuristics : {p : _} ->
{ps : _} ->
ScoredPats ns (p :: ps) ->
List (ScoredPats ns (p :: ps) -> ScoredPats ns (p :: ps)) ->
applyHeuristics : {p : _} ->
{ps : _} ->
ScoredPats ns (p :: ps) ->
List (ScoredPats ns (p :: ps) -> ScoredPats ns (p :: ps)) ->
Maybe (n ** NVar n (p :: ps))
applyHeuristics x [] = highScoreIdx x
applyHeuristics x (f :: fs) = highScoreIdx x <|> applyHeuristics (f x) fs