git.iko.soy/Idris-dev
on master help sign in
Merge pull request #1490 from edwinb/master
008cdb6Edwin Brady
CHANGELOG+1
compare with master
unifiedsplit
@@ -11,6 +11,7 @@ New in 0.9.15:
11 solved automatically.
11 solved automatically.
12* More efficient representation of proof state, leading to faster elaboration
12* More efficient representation of proof state, leading to faster elaboration
13 of large expressions.
13 of large expressions.
14+* EXPERIMENTAL Implementation of uniqueness types
14
15
15New in 0.9.14:
16New in 0.9.14:
16--------------
17--------------
src/Idris/Core/CaseTree.hs+7−1
@@ -350,10 +350,16 @@ toPats reflect tc f = reverse (toPat reflect tc (getArgs f)) where
350toPat :: Bool -> Bool -> [Term] -> [Pat]
350toPat :: Bool -> Bool -> [Term] -> [Pat]
351toPat reflect tc = map $ toPat' []
351toPat reflect tc = map $ toPat' []
352 where
352 where
353− toPat' [_,_,arg](P (DCon t a uniq) nm@(UN n) _)
353+ toPat' [_,_,arg] (P (DCon t a uniq) nm@(UN n) _)
354 | n == txt "Delay"
354 | n == txt "Delay"
355 = PCon uniq nm t [PAny, PAny, toPat' [] arg]
355 = PCon uniq nm t [PAny, PAny, toPat' [] arg]
356
356
357+ toPat' args (P (DCon t a uniq) nm@(NS (UN n) [own]) _)
358+ | n == txt "Read" && own == txt "Ownership"
359+ = PCon False nm t (map shareCons (map (toPat' []) args))
360+ where shareCons (PCon _ n i ps) = PCon False n i (map shareCons ps)
361+ shareCons p = p
362+
357 toPat' args (P (DCon t a uniq) n _)
363 toPat' args (P (DCon t a uniq) n _)
358 = PCon uniq n t $ map (toPat' []) args
364 = PCon uniq n t $ map (toPat' []) args
359
365