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

Renaming of built-in datatypes works finally

Browse Source
This commit is contained in:
Ahmad Salim Al-Sibahi 2014-09-23 10:46:06 +02:00
parent f0ed9e992f
commit 6faa1ab210
8 changed files with 26 additions and 44 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

7
libs/prelude/Builtins.idr
View File

@ -5,18 +5,19 @@
||| The canonical single-element type, also known as the trivially
||| true proposition.
data Unit =
%elim
data Unit =
||| The trivial constructor for `()`.
MkUnit
||| The non-dependent pair type, also known as conjunction.
||| @A the type of the left elements in the pair
||| @B the type of the left elements in the pair
data Pair : (A : Type) -> (B : Type) -> Type =
data Pair : (A : Type) -> (B : Type) -> Type where
||| A pair of elements
||| @a the left element of the pair
||| @b the right element of the pair
MkPair : (a : A) -> (b : B) -> Pair A B
MkPair : {A, B : Type} -> (a : A) -> (b : B) -> Pair A B
||| Dependent pairs, in their internal representation
||| @ a the type of the witness

2
libs/prelude/Prelude/Basics.idr
View File

@ -1,5 +1,7 @@
module Prelude.Basics
import Builtins
Not : Type -> Type
Not a = a -> _|_

2
libs/prelude/Prelude/Classes.idr
View File

@ -28,10 +28,8 @@ class Eq a where
x /= y = not (x == y)
x == y = not (x /= y)
%logging 5
instance Eq () where
() == () = True
%logging 0
instance Eq Int where
(==) = boolOp prim__eqInt

4
samples/reflection.idr
View File

@ -32,13 +32,13 @@ envList = ?envListPrf
||| Reflected raw rep. for the type (TTName, TT)
tupleType : Raw
tupleType = RApp (RApp (Var (MN 0 "__Pair"))
tupleType = RApp (RApp (Var (UN "Pair"))
(Var (NS (UN "TTName") ["Reflection", "Language"])))
(Var (NS (UN "TT") ["Reflection", "Language"]))
||| Reflected raw rep for the type List (TTName, TT)
mkTuple : Raw
mkTuple = RApp (RApp (Var (MN 0 "__MkPair"))
mkTuple = RApp (RApp (Var (UN "MkPair"))
(Var (NS (UN "TTName") ["Reflection", "Language"])))
(Var (NS (UN "TT") ["Reflection", "Language"]))

25
src/Idris/AbsSyntaxTree.hs
View File

@ -1065,16 +1065,10 @@ getInferType (App (App _ ty) _) = ty
-- Handy primitives: Unit, False, Pair, MkPair, =, mkForeign
primNames = [unitTy, unitCon,
falseTy, pairTy, pairCon,
eqTy, eqCon, inferTy, inferCon]
primNames = [falseTy, eqTy, eqCon, inferTy, inferCon]
unitDoc = parseDocstring . T.pack $ "The canonical single-element type, also known as the trivially true proposition."
unitTy = sUN "Unit"
unitCon = sUN "MkUnit"
unitDecl = PDatadecl unitTy PType
[(parseDocstring . T.pack $ "The trivial constructor for `()`. ", [], unitCon, PRef bi unitTy, bi, [])]
unitOpts = [DefaultEliminator]
falseDoc = parseDocstring . T.pack $
"The empty type, also known as the trivially false proposition." ++
@ -1085,25 +1079,8 @@ falseTy = sMN 0 "__False"
falseDecl = PDatadecl falseTy PType []
falseOpts = []
pairDoc = parseDocstring . T.pack $ "The non-dependent pair type, also known as conjunction."
pairTy = sUN "Pair"
pairCon = sUN "MkPair"
pairDecl = PDatadecl pairTy (piBind [(n "A", PType), (n "B", PType)] PType)
[(pairConDoc, pairConParamDoc,
pairCon, PPi impl (n "A") PType (
PPi impl (n "B") PType (
PPi expl (n "a") (PRef bi (n "A")) (
PPi expl (n "b") (PRef bi (n "B"))
(PApp bi (PRef bi pairTy) [pexp (PRef bi (n "A")),
pexp (PRef bi (n "B"))])))), bi, [])]
where n a = sMN 0 a
pairConDoc = parseDocstring . T.pack $ "A pair of elements"
pairConParamDoc = [(n "a", parseDocstring . T.pack $ "the left element of the pair"),
(n "b", parseDocstring . T.pack $ "the right element of the pair")]
pairOpts = []
pairParamDoc = [(n "A", parseDocstring . T.pack $ "the type of the left elements in the pair"),
(n "B", parseDocstring . T.pack $ "the type of the left elements in the pair")]
where n a = sMN 0 a
eqTy = sUN "="
eqCon = sUN "Refl"

8
src/Idris/ElabDecls.hs
View File

@ -76,10 +76,10 @@ elabPrims :: Idris ()
elabPrims = do mapM_ (elabDecl' EAll recinfo)
(map (\(opt, decl, docs, argdocs) -> PData docs argdocs defaultSyntax (fileFC "builtin") opt decl)
(zip4
[inferOpts, unitOpts, falseOpts, pairOpts, eqOpts]
[inferDecl, unitDecl, falseDecl, pairDecl, eqDecl]
[emptyDocstring, unitDoc, falseDoc, pairDoc, eqDoc]
[[], [], [], pairParamDoc, eqParamDoc]))
[inferOpts, falseOpts, eqOpts]
[inferDecl, falseDecl, eqDecl]
[emptyDocstring, falseDoc, eqDoc]
[[], [], eqParamDoc]))
addNameHint eqTy (sUN "prf")
mapM_ elabPrim primitives
-- Special case prim__believe_me because it doesn't work on just constants

16
src/Idris/ElabTerm.hs
View File

@ -245,8 +245,12 @@ elab ist info emode opts fn tm
-- = lift $ tfail (Msg "Typecase is not allowed")
elab' ina (PConstant c) = do apply (RConstant c) []; solve
elab' ina (PQuote r) = do fill r; solve
elab' ina (PTrue fc _) = try (elab' ina (PRef fc unitCon))
(elab' ina (PRef fc unitTy))
elab' ina (PTrue fc _) =
do hnf_compute
g <- goal
case g of
TType _ -> elab' ina (PRef fc unitTy)
_ -> elab' ina (PRef fc unitCon)
elab' ina (PFalse fc) = elab' ina (PRef fc falseTy)
elab' ina (PResolveTC (FC "HACK" _ _)) -- for chasing parent classes
= do g <- goal; resolveTC False 5 g fn ist
@ -283,11 +287,11 @@ elab ist info emode opts fn tm
= do hnf_compute
g <- goal
case g of
TType _ -> elabE (True, a,inty, qq) (PApp fc (PRef fc pairTy)
TType _ -> elab' ina (PApp fc (PRef fc pairTy)
[pexp l,pexp r])
_ -> elabE (True, a, inty, qq) (PApp fc (PRef fc pairCon)
[pimp (sMN 0 "A") Placeholder True,
pimp (sMN 0 "B") Placeholder True,
_ -> elab' ina (PApp fc (PRef fc pairCon)
[pimp (sUN "A") Placeholder False,
pimp (sUN "B") Placeholder False,
pexp l, pexp r])
elab' ina (PDPair fc p l@(PRef _ n) t r)
= case t of

6
test/quasiquote001/expected
View File

@ -1,5 +1,5 @@
(App (App (App (P (DCon 1 3) (NS (UN ::) ["List", "Prelude"]) (Bind (UN a) (Pi (TType (UVar -1))) (Bind (MN 0 "_t") (Pi (V 0)) (Bind (MN 2 "_t") (Pi (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 1))) (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 2)))))) (P (TCon 7 0) (MN 0 "__Unit") (TType (UVar 10)))) (P (DCon 0 0) (MN 0 "__II") (P (TCon 0 0) (MN 0 "__Unit") (TType (UVar 10))))) (App (App (App (P (DCon 1 3) (NS (UN ::) ["List", "Prelude"]) (Bind (UN a) (Pi (TType (UVar -1))) (Bind (MN 0 "_t") (Pi (V 0)) (Bind (MN 2 "_t") (Pi (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 1))) (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 2)))))) (P (TCon 7 0) (MN 0 "__Unit") (TType (UVar 10)))) (P (DCon 0 0) (MN 0 "__II") (P (TCon 0 0) (MN 0 "__Unit") (TType (UVar 10))))) (App (P (DCon 0 1) (NS (UN Nil) ["List", "Prelude"]) (Bind (UN a) (Pi (TType (UVar -1))) (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 0)))) (P (TCon 7 0) (MN 0 "__Unit") (TType (UVar 10))))))
(App (App (App (P (DCon 1 3) (NS (UN ::) ["List", "Prelude"]) (Bind (UN a) (Pi (TType (UVar -1))) (Bind (MN 0 "_t") (Pi (V 0)) (Bind (MN 2 "_t") (Pi (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 1))) (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 2)))))) (P (TCon 9 0) (UN Unit) (TType (UVar -1)))) (P (DCon 0 0) (UN MkUnit) (P (TCon 0 0) (UN Unit) Erased))) (App (App (App (P (DCon 1 3) (NS (UN ::) ["List", "Prelude"]) (Bind (UN a) (Pi (TType (UVar -1))) (Bind (MN 0 "_t") (Pi (V 0)) (Bind (MN 2 "_t") (Pi (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 1))) (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 2)))))) (P (TCon 9 0) (UN Unit) (TType (UVar -1)))) (P (DCon 0 0) (UN MkUnit) (P (TCon 0 0) (UN Unit) Erased))) (App (P (DCon 0 1) (NS (UN Nil) ["List", "Prelude"]) (Bind (UN a) (Pi (TType (UVar -1))) (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 0)))) (P (TCon 9 0) (UN Unit) (TType (UVar -1))))))
--------------
(App (App (App (P (DCon 1 3) (NS (UN ::) ["List", "Prelude"]) (Bind (UN a) (Pi (TType (UVar -1))) (Bind (MN 0 "_t") (Pi (V 0)) (Bind (MN 2 "_t") (Pi (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 1))) (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 2)))))) (TType (UVar 190))) (TType (UVar 192))) (App (App (App (P (DCon 1 3) (NS (UN ::) ["List", "Prelude"]) (Bind (UN a) (Pi (TType (UVar -1))) (Bind (MN 0 "_t") (Pi (V 0)) (Bind (MN 2 "_t") (Pi (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 1))) (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 2)))))) (TType (UVar 194))) (App (App (App (App (P (DCon 0 4) (MN 0 "__MkPair") (Bind (MN 0 "A") (Pi (TType (UVar 64))) (Bind (MN 0 "B") (Pi (TType (UVar 68))) (Bind (MN 0 "a") (Pi (V 1)) (Bind (MN 0 "b") (Pi (V 1)) (App (App (P (TCon 0 0) (MN 0 "__Pair") (Bind (MN 1 "A") (Pi (TType (UVar 52))) (Bind (MN 1 "B") (Pi (TType (UVar 56))) (TType (UVar 60))))) (V 3)) (V 2))))))) (TType (UVar 184))) (TType (UVar 186))) (P (TCon 15 0) (NS (UN Nat) ["Nat", "Prelude"]) (TType (UVar -1)))) (P (TCon 15 0) (NS (UN Nat) ["Nat", "Prelude"]) (TType (UVar -1))))) (App (P (DCon 0 1) (NS (UN Nil) ["List", "Prelude"]) (Bind (UN a) (Pi (TType (UVar -1))) (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 0)))) (TType (UVar 196)))))
(App (App (App (P (DCon 1 3) (NS (UN ::) ["List", "Prelude"]) (Bind (UN a) (Pi (TType (UVar -1))) (Bind (MN 0 "_t") (Pi (V 0)) (Bind (MN 2 "_t") (Pi (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 1))) (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 2)))))) (TType (UVar 50))) (TType (UVar 52))) (App (App (App (P (DCon 1 3) (NS (UN ::) ["List", "Prelude"]) (Bind (UN a) (Pi (TType (UVar -1))) (Bind (MN 0 "_t") (Pi (V 0)) (Bind (MN 2 "_t") (Pi (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 1))) (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 2)))))) (TType (UVar 54))) (App (App (App (App (P (DCon 0 4) (UN MkPair) (Bind (UN A) (Pi (TType (UVar -1))) (Bind (UN B) (Pi (TType (UVar -1))) (Bind (UN a) (Pi (V 1)) (Bind (UN b) (Pi (V 1)) (App (App (P (TCon 0 0) (UN Pair) Erased) (V 3)) (V 2))))))) (TType (UVar 44))) (TType (UVar 46))) (P (TCon 9 0) (NS (UN Nat) ["Nat", "Prelude"]) (TType (UVar -1)))) (P (TCon 9 0) (NS (UN Nat) ["Nat", "Prelude"]) (TType (UVar -1))))) (App (P (DCon 0 1) (NS (UN Nil) ["List", "Prelude"]) (Bind (UN a) (Pi (TType (UVar -1))) (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 0)))) (TType (UVar 56)))))
--------------
(App (App (App (App (P (DCon 0 4) (MN 0 "__MkPair") (Bind (MN 0 "A") (Pi (TType (UVar 64))) (Bind (MN 0 "B") (Pi (TType (UVar 68))) (Bind (MN 0 "a") (Pi (V 1)) (Bind (MN 0 "b") (Pi (V 1)) (App (App (P (TCon 0 0) (MN 0 "__Pair") (Bind (MN 1 "A") (Pi (TType (UVar 52))) (Bind (MN 1 "B") (Pi (TType (UVar 56))) (TType (UVar 60))))) (V 3)) (V 2))))))) (TType (UVar 184))) (TType (UVar 186))) (App (App (App (App (P (DCon 0 4) (MN 0 "__MkPair") (Bind (MN 0 "A") (Pi (TType (UVar 64))) (Bind (MN 0 "B") (Pi (TType (UVar 68))) (Bind (MN 0 "a") (Pi (V 1)) (Bind (MN 0 "b") (Pi (V 1)) (App (App (P (TCon 0 0) (MN 0 "__Pair") (Bind (MN 1 "A") (Pi (TType (UVar 52))) (Bind (MN 1 "B") (Pi (TType (UVar 56))) (TType (UVar 60))))) (V 3)) (V 2))))))) (TType (UVar 184))) (TType (UVar 186))) (TType (UVar 190))) (TType (UVar 190)))) (App (App (App (App (P (DCon 0 4) (MN 0 "__MkPair") (Bind (MN 0 "A") (Pi (TType (UVar 64))) (Bind (MN 0 "B") (Pi (TType (UVar 68))) (Bind (MN 0 "a") (Pi (V 1)) (Bind (MN 0 "b") (Pi (V 1)) (App (App (P (TCon 0 0) (MN 0 "__Pair") (Bind (MN 1 "A") (Pi (TType (UVar 52))) (Bind (MN 1 "B") (Pi (TType (UVar 56))) (TType (UVar 60))))) (V 3)) (V 2))))))) (TType (UVar 184))) (TType (UVar 186))) (TType (UVar 190))) (TType (UVar 190))))
(App (App (App (App (P (DCon 0 4) (UN MkPair) (Bind (UN A) (Pi (TType (UVar -1))) (Bind (UN B) (Pi (TType (UVar -1))) (Bind (UN a) (Pi (V 1)) (Bind (UN b) (Pi (V 1)) (App (App (P (TCon 0 0) (UN Pair) Erased) (V 3)) (V 2))))))) (TType (UVar 44))) (TType (UVar 46))) (App (App (App (App (P (DCon 0 4) (UN MkPair) (Bind (UN A) (Pi (TType (UVar -1))) (Bind (UN B) (Pi (TType (UVar -1))) (Bind (UN a) (Pi (V 1)) (Bind (UN b) (Pi (V 1)) (App (App (P (TCon 0 0) (UN Pair) Erased) (V 3)) (V 2))))))) (TType (UVar 44))) (TType (UVar 46))) (TType (UVar 50))) (TType (UVar 50)))) (App (App (App (App (P (DCon 0 4) (UN MkPair) (Bind (UN A) (Pi (TType (UVar -1))) (Bind (UN B) (Pi (TType (UVar -1))) (Bind (UN a) (Pi (V 1)) (Bind (UN b) (Pi (V 1)) (App (App (P (TCon 0 0) (UN Pair) Erased) (V 3)) (V 2))))))) (TType (UVar 44))) (TType (UVar 46))) (TType (UVar 50))) (TType (UVar 50))))