git.iko.soy/Idris-dev
on master help sign in
Pair syntax for unique types

This works only if the elaborator is in a context where it is expecting a unique type (or a Type*) rather than a normal type. This is EXPERIMENTAL but should(!) not cause any issues in code which uses no unique types or Type*

commit4d1759e3942163a6cd8d4d8c20ad4d4250f2861e authorEdwin Brady <ecb10@st-andrews.ac.uk> dateThu 19 Feb 2015, 11:09 (12 years ago) parentfca8309
5 files changed+39−9
compare with master
unifiedsplit
libs/prelude/Builtins.idr+10 src/Idris/AbsSyntaxTree.hs+3 src/Idris/ElabTerm.hs+21−1 test/unique001/expected+1−1 test/unique001/unique001c.idr+4−7
libs/prelude/Builtins.idr+10
@@ -19,6 +19,16 @@ namespace Builtins
1919 ||| @b the right element of the pair
2020 MkPair : {A, B : Type} -> (a : A) -> (b : B) -> Pair A B
2121
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+
2232 ||| Dependent pairs
2333 |||
2434 ||| Dependent pairs represent existential quantification - they consist of a
src/Idris/AbsSyntaxTree.hs+3
@@ -1246,6 +1246,9 @@ falseTy = sUN "Void"
12461246pairTy = sNS (sUN "Pair") ["Builtins"]
12471247pairCon = sNS (sUN "MkPair") ["Builtins"]
12481248
1249+upairTy = sNS (sUN "UPair") ["Builtins"]
1250+upairCon = sNS (sUN "MkUPair") ["Builtins"]
1251+
12491252eqTy = sUN "="
12501253eqCon = sUN "Refl"
12511254eqDoc = fmap (const (Left $ Msg "")) . parseDocstring . T.pack $
src/Idris/ElabTerm.hs+21−1
@@ -318,6 +318,7 @@ elab ist info emode opts fn tm
318318 g <- goal
319319 case g of
320320 TType _ -> elab' ina (Just fc) (PRef fc unitTy)
321+ UType _ -> elab' ina (Just fc) (PRef fc unitTy)
321322 _ -> elab' ina (Just fc) (PRef fc unitCon)
322323 elab' ina fc (PResolveTC (FC "HACK" _ _)) -- for chasing parent classes
323324 = do g <- goal; resolveTC False 5 g fn ist
@@ -353,13 +354,32 @@ elab ist info emode opts fn tm
353354 elab' ina _ (PPair fc _ l r)
354355 = do hnf_compute
355356 g <- goal
357+ let (tc, _) = unApply g
356358 case g of
357359 TType _ -> elab' ina (Just fc) (PApp fc (PRef fc pairTy)
358360 [pexp l,pexp r])
359− _ -> elab' ina (Just fc) (PApp fc (PRef fc pairCon)
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
365+ -> elab' ina (Just fc) (PApp fc (PRef fc upairCon)
360366 [pimp (sUN "A") Placeholder False,
361367 pimp (sUN "B") Placeholder False,
362368 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+
363383 elab' ina _ (PDPair fc p l@(PRef _ n) t r)
364384 = case t of
365385 Placeholder ->
test/unique001/expected+1−1
@@ -15,6 +15,6 @@ unique001a.idr:55:12:Can't convert
1515with
1616 Int -> String
1717unique001b.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
1919unique001d.idr:3:7:Borrowed name x must not be used on RHS
2020unique001e.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
1111 ULeaf : UTree
1212 UNode : UTree -> Int -> UTree -> UTree
1313
14−data UPair : UniqueType -> UniqueType -> UniqueType where
15− MkUPair : {a,b:UniqueType} -> a -> b -> UPair a b
16−
1714dup : UTree -> UPair UTree UTree
18−dup ULeaf = MkUPair ULeaf ULeaf
19−dup (UNode l y r) = let MkUPair l1 l2 = dup l
20− MkUPair r1 r2 = dup r in
21− MkUPair (UNode l1 y r1) (UNode l2 y r2)
15+dup ULeaf = (ULeaf, ULeaf)
16+dup (UNode l y r) = let (l1, l2) = dup l
17+ (r1, r2) = dup r in
18+ (UNode l1 y r1, UNode l2 y r2)
2219
2320data Tree : Type where
2421 Leaf : Tree