ilyakooo0/Idris-dev
1
0
Fork 0
mirror of https://github.com/ilyakooo0/Idris-dev.git synced 2024-11-11 14:57:30 +03:00
Code Issues Projects Releases Wiki Activity

Implement accessible+inaccessible splitting.

Browse Source
This commit is contained in:
Matus Tejiscak 2014-07-05 20:57:07 +01:00
parent 1e3734863c
commit 2490a15c1c
1 changed files with 14 additions and 3 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

17
src/Idris/Core/CaseTree.hs
View File

@ -549,8 +549,10 @@ argsToAlt _ [] = return ([], [], [], [])
argsToAlt inacc rs@((r, m) : rest) = do
newVars <- getNewVars r
return $ case inacc of
[] -> (newVars, newVars, [], addRs rs) -- no inaccessible arguments
_ -> error "inaccessible data ctor args not implemented"
[] -> (newVars, newVars, [], addRs rs) -- no inaccessible arguments, simple.
_ | (accVars, inaccVars) <- partitionAcc newVars
-> (newVars, accVars, inaccVars, addRs rs)
where
-- Create names for new variables arising from the given patterns.
getNewVars :: [Pat] -> CaseBuilder [Name]
@ -575,8 +577,17 @@ argsToAlt inacc rs@((r, m) : rest) = do
getNewVars (PTyPat : ns) = (:) <$> getVar "t" <*> getNewVars ns
getNewVars (_ : ns) = (:) <$> getVar "e" <*> getNewVars ns
-- Partition a list of things into (accessible, inaccessible) things,
-- according to the list of inaccessible indices.
partitionAcc xs =
( [x | (i,x) <- zip [0..] xs, i `notElem` inacc]
, [x | (i,x) <- zip [0..] xs, i `elem` inacc]
)
addRs [] = []
addRs ((r, (ps, res)) : rs) = ((r++ps, res) : addRs rs)
addRs ((r, (ps, res)) : rs) = ((acc++ps++inacc, res) : addRs rs)
where
(acc, inacc) = partitionAcc r
uniq i (UN n) = MN i n
uniq i n = n