on master help sign in
Implement accessible+inaccessible splitting.
commit2490a15c1c5189439a85caff1e3d7a7d094168ef authorMatus Tejiscak <ziman@functor.sk> dateSat 5 Jul 2014, 20:57 (12 years ago) parent1e37348
1 file changed+14−3
src/Idris/Core/CaseTree.hs+14−3
src/Idris/Core/CaseTree.hs+14−3
@@ -549,8 +549,10 @@ argsToAlt _ [] = return ([], [], [], [])
549549argsToAlt inacc rs@((r, m) : rest) = do
550550 newVars <- getNewVars r
551551 return $ case inacc of
552− [] -> (newVars, newVars, [], addRs rs) -- no inaccessible arguments
553− _ -> error "inaccessible data ctor args not implemented"
552+ [] -> (newVars, newVars, [], addRs rs) -- no inaccessible arguments, simple.
553+
554+ _ | (accVars, inaccVars) <- partitionAcc newVars
555+ -> (newVars, accVars, inaccVars, addRs rs)
554556 where
555557 -- Create names for new variables arising from the given patterns.
556558 getNewVars :: [Pat] -> CaseBuilder [Name]
@@ -575,8 +577,17 @@ argsToAlt inacc rs@((r, m) : rest) = do
575577 getNewVars (PTyPat : ns) = (:) <$> getVar "t" <*> getNewVars ns
576578 getNewVars (_ : ns) = (:) <$> getVar "e" <*> getNewVars ns
577579
580+ -- Partition a list of things into (accessible, inaccessible) things,
581+ -- according to the list of inaccessible indices.
582+ partitionAcc xs =
583+ ( [x | (i,x) <- zip [0..] xs, i `notElem` inacc]
584+ , [x | (i,x) <- zip [0..] xs, i `elem` inacc]
585+ )
586+
578587 addRs [] = []
579− addRs ((r, (ps, res)) : rs) = ((r++ps, res) : addRs rs)
588+ addRs ((r, (ps, res)) : rs) = ((acc++ps++inacc, res) : addRs rs)
589+ where
590+ (acc, inacc) = partitionAcc r
580591
581592 uniq i (UN n) = MN i n
582593 uniq i n = n