git.iko.soy/Idris-dev
on master help sign in
Pair syntax for unique types
4d1759eEdwin Brady
libs/prelude/Builtins.idr+10
compare with master
unifiedsplit
@@ -19,6 +19,16 @@ namespace Builtins
19 ||| @b the right element of the pair
19 ||| @b the right element of the pair
20 MkPair : {A, B : Type} -> (a : A) -> (b : B) -> Pair A B
20 MkPair : {A, B : Type} -> (a : A) -> (b : B) -> Pair A B
21
21
22+ ||| The non-dependent pair type, also known as conjunction, usable with
23+ ||| UniqueTypes.
24+ ||| @A the type of the left elements in the pair
25+ ||| @B the type of the left elements in the pair
26+ data UPair : (A : Type*) -> (B : Type*) -> Type where
27+ ||| A pair of elements
28+ ||| @a the left element of the pair
29+ ||| @b the right element of the pair
30+ MkUPair : {A, B : Type*} -> (a : A) -> (b : B) -> UPair A B
31+
22 ||| Dependent pairs
32 ||| Dependent pairs
23 |||
33 |||
24 ||| Dependent pairs represent existential quantification - they consist of a
34 ||| Dependent pairs represent existential quantification - they consist of a
src/Idris/AbsSyntaxTree.hs+3
@@ -1246,6 +1246,9 @@ falseTy = sUN "Void"
1246pairTy = sNS (sUN "Pair") ["Builtins"]
1246pairTy = sNS (sUN "Pair") ["Builtins"]
1247pairCon = sNS (sUN "MkPair") ["Builtins"]
1247pairCon = sNS (sUN "MkPair") ["Builtins"]
1248
1248
1249+upairTy = sNS (sUN "UPair") ["Builtins"]
1250+upairCon = sNS (sUN "MkUPair") ["Builtins"]
1251+
1249eqTy = sUN "="
1252eqTy = sUN "="
1250eqCon = sUN "Refl"
1253eqCon = sUN "Refl"
1251eqDoc = fmap (const (Left $ Msg "")) . parseDocstring . T.pack $
1254eqDoc = fmap (const (Left $ Msg "")) . parseDocstring . T.pack $
src/Idris/ElabTerm.hs+21−1
@@ -318,6 +318,7 @@ elab ist info emode opts fn tm
318 g <- goal
318 g <- goal
319 case g of
319 case g of
320 TType _ -> elab' ina (Just fc) (PRef fc unitTy)
320 TType _ -> elab' ina (Just fc) (PRef fc unitTy)
321+ UType _ -> elab' ina (Just fc) (PRef fc unitTy)
321 _ -> elab' ina (Just fc) (PRef fc unitCon)
322 _ -> elab' ina (Just fc) (PRef fc unitCon)
322 elab' ina fc (PResolveTC (FC "HACK" _ _)) -- for chasing parent classes
323 elab' ina fc (PResolveTC (FC "HACK" _ _)) -- for chasing parent classes
323 = do g <- goal; resolveTC False 5 g fn ist
324 = do g <- goal; resolveTC False 5 g fn ist
@@ -353,13 +354,32 @@ elab ist info emode opts fn tm
353 elab' ina _ (PPair fc _ l r)
354 elab' ina _ (PPair fc _ l r)
354 = do hnf_compute
355 = do hnf_compute
355 g <- goal
356 g <- goal
357+ let (tc, _) = unApply g
356 case g of
358 case g of
357 TType _ -> elab' ina (Just fc) (PApp fc (PRef fc pairTy)
359 TType _ -> elab' ina (Just fc) (PApp fc (PRef fc pairTy)
358 [pexp l,pexp r])
360 [pexp l,pexp r])
361+ UType _ -> elab' ina (Just fc) (PApp fc (PRef fc upairTy)
362+ [pexp l,pexp r])
363+ _ -> case tc of
364+ P _ n _ | n == upairTy
359− _ -> elab' ina (Just fc) (PApp fc (PRef fc pairCon)
365+ -> elab' ina (Just fc) (PApp fc (PRef fc upairCon)
360 [pimp (sUN "A") Placeholder False,
366 [pimp (sUN "A") Placeholder False,
361 pimp (sUN "B") Placeholder False,
367 pimp (sUN "B") Placeholder False,
362 pexp l, pexp r])
368 pexp l, pexp r])
369+ _ -> elab' ina (Just fc) (PApp fc (PRef fc pairCon)
370+ [pimp (sUN "A") Placeholder False,
371+ pimp (sUN "B") Placeholder False,
372+ pexp l, pexp r])
373+-- _ -> try' (elab' ina (Just fc) (PApp fc (PRef fc pairCon)
374+-- [pimp (sUN "A") Placeholder False,
375+-- pimp (sUN "B") Placeholder False,
376+-- pexp l, pexp r]))
377+-- (elab' ina (Just fc) (PApp fc (PRef fc upairCon)
378+-- [pimp (sUN "A") Placeholder False,
379+-- pimp (sUN "B") Placeholder False,
380+-- pexp l, pexp r]))
381+-- True
382+
363 elab' ina _ (PDPair fc p l@(PRef _ n) t r)
383 elab' ina _ (PDPair fc p l@(PRef _ n) t r)
364 = case t of
384 = case t of
365 Placeholder ->
385 Placeholder ->
test/unique001/expected+1−1
@@ -15,6 +15,6 @@ unique001a.idr:55:12:Can't convert
15with
15with
16 Int -> String
16 Int -> String
17unique001b.idr:16:7:Borrowed name xs must not be used on RHS
17unique001b.idr:16:7:Borrowed name xs must not be used on RHS
18−unique001c.idr:49:6:Unique name f is used more than once
18+unique001c.idr:46:6:Unique name f is used more than once
19unique001d.idr:3:7:Borrowed name x must not be used on RHS
19unique001d.idr:3:7:Borrowed name x must not be used on RHS
20unique001e.idr:4:11:Constructor Main.:: has a UniqueType, but the data type does not
20unique001e.idr:4:11:Constructor Main.:: has a UniqueType, but the data type does not
test/unique001/unique001c.idr+4−7
@@ -11,14 +11,11 @@ data UTree : UniqueType where
11 ULeaf : UTree
11 ULeaf : UTree
12 UNode : UTree -> Int -> UTree -> UTree
12 UNode : UTree -> Int -> UTree -> UTree
13
13
14−data UPair : UniqueType -> UniqueType -> UniqueType where
15− MkUPair : {a,b:UniqueType} -> a -> b -> UPair a b
16−
17dup : UTree -> UPair UTree UTree
14dup : UTree -> UPair UTree UTree
18−dup ULeaf = MkUPair ULeaf ULeaf
15+dup ULeaf = (ULeaf, ULeaf)
19−dup (UNode l y r) = let MkUPair l1 l2 = dup l
16+dup (UNode l y r) = let (l1, l2) = dup l
20− MkUPair r1 r2 = dup r in
17+ (r1, r2) = dup r in
21− MkUPair (UNode l1 y r1) (UNode l2 y r2)
18+ (UNode l1 y r1, UNode l2 y r2)
22
19
23data Tree : Type where
20data Tree : Type where
24 Leaf : Tree
21 Leaf : Tree