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

Pair syntax for unique types

Browse Source 
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*
This commit is contained in:
Edwin Brady 2015-02-19 11:09:15 +00:00
parent fca8309ee2
commit 4d1759e394
5 changed files with 39 additions and 9 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

10
libs/prelude/Builtins.idr
View File

@ -19,6 +19,16 @@ namespace Builtins
||| @b the right element of the pair
MkPair : {A, B : Type} -> (a : A) -> (b : B) -> Pair A B
||| The non-dependent pair type, also known as conjunction, usable with
||| UniqueTypes.
||| @A the type of the left elements in the pair
||| @B the type of the left elements in the pair
data UPair : (A : Type*) -> (B : Type*) -> Type where
||| A pair of elements
||| @a the left element of the pair
||| @b the right element of the pair
MkUPair : {A, B : Type*} -> (a : A) -> (b : B) -> UPair A B
||| Dependent pairs
|||
||| Dependent pairs represent existential quantification - they consist of a

3
src/Idris/AbsSyntaxTree.hs
View File

@ -1246,6 +1246,9 @@ falseTy = sUN "Void"
pairTy = sNS (sUN "Pair") ["Builtins"]
pairCon = sNS (sUN "MkPair") ["Builtins"]
upairTy = sNS (sUN "UPair") ["Builtins"]
upairCon = sNS (sUN "MkUPair") ["Builtins"]
eqTy = sUN "="
eqCon = sUN "Refl"
eqDoc = fmap (const (Left $ Msg "")) . parseDocstring . T.pack $

22
src/Idris/ElabTerm.hs
View File

@ -318,6 +318,7 @@ elab ist info emode opts fn tm
g <- goal
case g of
TType _ -> elab' ina (Just fc) (PRef fc unitTy)
UType _ -> elab' ina (Just fc) (PRef fc unitTy)
_ -> elab' ina (Just fc) (PRef fc unitCon)
elab' ina fc (PResolveTC (FC "HACK" _ _)) -- for chasing parent classes
= do g <- goal; resolveTC False 5 g fn ist
@ -353,13 +354,32 @@ elab ist info emode opts fn tm
elab' ina _ (PPair fc _ l r)
= do hnf_compute
g <- goal
let (tc, _) = unApply g
case g of
TType _ -> elab' ina (Just fc) (PApp fc (PRef fc pairTy)
[pexp l,pexp r])
_ -> elab' ina (Just fc) (PApp fc (PRef fc pairCon)
UType _ -> elab' ina (Just fc) (PApp fc (PRef fc upairTy)
[pexp l,pexp r])
_ -> case tc of
P _ n _ | n == upairTy
-> elab' ina (Just fc) (PApp fc (PRef fc upairCon)
[pimp (sUN "A") Placeholder False,
pimp (sUN "B") Placeholder False,
pexp l, pexp r])
_ -> elab' ina (Just fc) (PApp fc (PRef fc pairCon)
[pimp (sUN "A") Placeholder False,
pimp (sUN "B") Placeholder False,
pexp l, pexp r])
-- _ -> try' (elab' ina (Just fc) (PApp fc (PRef fc pairCon)
-- [pimp (sUN "A") Placeholder False,
-- pimp (sUN "B") Placeholder False,
-- pexp l, pexp r]))
-- (elab' ina (Just fc) (PApp fc (PRef fc upairCon)
-- [pimp (sUN "A") Placeholder False,
-- pimp (sUN "B") Placeholder False,
-- pexp l, pexp r]))
-- True
elab' ina _ (PDPair fc p l@(PRef _ n) t r)
= case t of
Placeholder ->

2
test/unique001/expected
View File

@ -15,6 +15,6 @@ unique001a.idr:55:12:Can't convert
with
Int -> String
unique001b.idr:16:7:Borrowed name xs must not be used on RHS
unique001c.idr:49:6:Unique name f is used more than once
unique001c.idr:46:6:Unique name f is used more than once
unique001d.idr:3:7:Borrowed name x must not be used on RHS
unique001e.idr:4:11:Constructor Main.:: has a UniqueType, but the data type does not

11
test/unique001/unique001c.idr
View File

@ -11,14 +11,11 @@ data UTree : UniqueType where
ULeaf : UTree
UNode : UTree -> Int -> UTree -> UTree
data UPair : UniqueType -> UniqueType -> UniqueType where
MkUPair : {a,b:UniqueType} -> a -> b -> UPair a b
dup : UTree -> UPair UTree UTree
dup ULeaf = MkUPair ULeaf ULeaf
dup (UNode l y r) = let MkUPair l1 l2 = dup l
MkUPair r1 r2 = dup r in
MkUPair (UNode l1 y r1) (UNode l2 y r2)
dup ULeaf = (ULeaf, ULeaf)
dup (UNode l y r) = let (l1, l2) = dup l
(r1, r2) = dup r in
(UNode l1 y r1, UNode l2 y r2)
data Tree : Type where
Leaf : Tree