git.iko.soy/Idris-dev
on master help sign in
Renaming of built-in datatypes works finally
commit6faa1ab210ed311236291acb538292d959cc4721 authorAhmad Salim Al-Sibahi <asal@itu.dk> dateTue 23 Sep 2014, 10:46 (12 years ago) parentf0ed9e9
8 files changed+26−44
compare with master
unifiedsplit
libs/prelude/Builtins.idr+4−3 libs/prelude/Prelude/Basics.idr+2 libs/prelude/Prelude/Classes.idr−2 samples/reflection.idr+2−2 src/Idris/AbsSyntaxTree.hs+1−24 src/Idris/ElabDecls.hs+4−4 src/Idris/ElabTerm.hs+10−6 test/quasiquote001/expected+3−3
libs/prelude/Builtins.idr+4−3
@@ -5,18 +5,19 @@
55
66||| The canonical single-element type, also known as the trivially
77||| true proposition.
8−data Unit =
8+%elim
9+ data Unit =
910 ||| The trivial constructor for `()`.
1011 MkUnit
1112
1213||| The non-dependent pair type, also known as conjunction.
1314||| @A the type of the left elements in the pair
1415||| @B the type of the left elements in the pair
15−data Pair : (A : Type) -> (B : Type) -> Type =
16+data Pair : (A : Type) -> (B : Type) -> Type where
1617 ||| A pair of elements
1718 ||| @a the left element of the pair
1819 ||| @b the right element of the pair
19− MkPair : (a : A) -> (b : B) -> Pair A B
20+ MkPair : {A, B : Type} -> (a : A) -> (b : B) -> Pair A B
2021
2122||| Dependent pairs, in their internal representation
2223||| @ a the type of the witness
libs/prelude/Prelude/Basics.idr+2
@@ -1,5 +1,7 @@
11module Prelude.Basics
22
3+import Builtins
4+
35Not : Type -> Type
46Not a = a -> _|_
57
libs/prelude/Prelude/Classes.idr−2
@@ -28,10 +28,8 @@ class Eq a where
2828 x /= y = not (x == y)
2929 x == y = not (x /= y)
3030
31−%logging 5
3231instance Eq () where
3332 () == () = True
34−%logging 0
3533
3634instance Eq Int where
3735 (==) = boolOp prim__eqInt
samples/reflection.idr+2−2
@@ -32,13 +32,13 @@ envList = ?envListPrf
3232
3333||| Reflected raw rep. for the type (TTName, TT)
3434tupleType : Raw
35−tupleType = RApp (RApp (Var (MN 0 "__Pair"))
35+tupleType = RApp (RApp (Var (UN "Pair"))
3636 (Var (NS (UN "TTName") ["Reflection", "Language"])))
3737 (Var (NS (UN "TT") ["Reflection", "Language"]))
3838
3939||| Reflected raw rep for the type List (TTName, TT)
4040mkTuple : Raw
41−mkTuple = RApp (RApp (Var (MN 0 "__MkPair"))
41+mkTuple = RApp (RApp (Var (UN "MkPair"))
4242 (Var (NS (UN "TTName") ["Reflection", "Language"])))
4343 (Var (NS (UN "TT") ["Reflection", "Language"]))
4444
src/Idris/AbsSyntaxTree.hs+1−24
@@ -1065,16 +1065,10 @@ getInferType (App (App _ ty) _) = ty
10651065
10661066-- Handy primitives: Unit, False, Pair, MkPair, =, mkForeign
10671067
1068−primNames = [unitTy, unitCon,
1069− falseTy, pairTy, pairCon,
1070− eqTy, eqCon, inferTy, inferCon]
1068+primNames = [falseTy, eqTy, eqCon, inferTy, inferCon]
10711069
1072−unitDoc = parseDocstring . T.pack $ "The canonical single-element type, also known as the trivially true proposition."
10731070unitTy = sUN "Unit"
10741071unitCon = sUN "MkUnit"
1075−unitDecl = PDatadecl unitTy PType
1076− [(parseDocstring . T.pack $ "The trivial constructor for `()`. ", [], unitCon, PRef bi unitTy, bi, [])]
1077−unitOpts = [DefaultEliminator]
10781072
10791073falseDoc = parseDocstring . T.pack $
10801074 "The empty type, also known as the trivially false proposition." ++
@@ -1085,25 +1079,8 @@ falseTy = sMN 0 "__False"
10851079falseDecl = PDatadecl falseTy PType []
10861080falseOpts = []
10871081
1088−pairDoc = parseDocstring . T.pack $ "The non-dependent pair type, also known as conjunction."
10891082pairTy = sUN "Pair"
10901083pairCon = sUN "MkPair"
1091−pairDecl = PDatadecl pairTy (piBind [(n "A", PType), (n "B", PType)] PType)
1092− [(pairConDoc, pairConParamDoc,
1093− pairCon, PPi impl (n "A") PType (
1094− PPi impl (n "B") PType (
1095− PPi expl (n "a") (PRef bi (n "A")) (
1096− PPi expl (n "b") (PRef bi (n "B"))
1097− (PApp bi (PRef bi pairTy) [pexp (PRef bi (n "A")),
1098− pexp (PRef bi (n "B"))])))), bi, [])]
1099− where n a = sMN 0 a
1100− pairConDoc = parseDocstring . T.pack $ "A pair of elements"
1101− pairConParamDoc = [(n "a", parseDocstring . T.pack $ "the left element of the pair"),
1102− (n "b", parseDocstring . T.pack $ "the right element of the pair")]
1103−pairOpts = []
1104−pairParamDoc = [(n "A", parseDocstring . T.pack $ "the type of the left elements in the pair"),
1105− (n "B", parseDocstring . T.pack $ "the type of the left elements in the pair")]
1106− where n a = sMN 0 a
11071084
11081085eqTy = sUN "="
11091086eqCon = sUN "Refl"
src/Idris/ElabDecls.hs+4−4
@@ -76,10 +76,10 @@ elabPrims :: Idris ()
7676elabPrims = do mapM_ (elabDecl' EAll recinfo)
7777 (map (\(opt, decl, docs, argdocs) -> PData docs argdocs defaultSyntax (fileFC "builtin") opt decl)
7878 (zip4
79− [inferOpts, unitOpts, falseOpts, pairOpts, eqOpts]
80− [inferDecl, unitDecl, falseDecl, pairDecl, eqDecl]
81− [emptyDocstring, unitDoc, falseDoc, pairDoc, eqDoc]
82− [[], [], [], pairParamDoc, eqParamDoc]))
79+ [inferOpts, falseOpts, eqOpts]
80+ [inferDecl, falseDecl, eqDecl]
81+ [emptyDocstring, falseDoc, eqDoc]
82+ [[], [], eqParamDoc]))
8383 addNameHint eqTy (sUN "prf")
8484 mapM_ elabPrim primitives
8585 -- Special case prim__believe_me because it doesn't work on just constants
src/Idris/ElabTerm.hs+10−6
@@ -245,8 +245,12 @@ elab ist info emode opts fn tm
245245-- = lift $ tfail (Msg "Typecase is not allowed")
246246 elab' ina (PConstant c) = do apply (RConstant c) []; solve
247247 elab' ina (PQuote r) = do fill r; solve
248− elab' ina (PTrue fc _) = try (elab' ina (PRef fc unitCon))
249− (elab' ina (PRef fc unitTy))
248+ elab' ina (PTrue fc _) =
249+ do hnf_compute
250+ g <- goal
251+ case g of
252+ TType _ -> elab' ina (PRef fc unitTy)
253+ _ -> elab' ina (PRef fc unitCon)
250254 elab' ina (PFalse fc) = elab' ina (PRef fc falseTy)
251255 elab' ina (PResolveTC (FC "HACK" _ _)) -- for chasing parent classes
252256 = do g <- goal; resolveTC False 5 g fn ist
@@ -283,11 +287,11 @@ elab ist info emode opts fn tm
283287 = do hnf_compute
284288 g <- goal
285289 case g of
286− TType _ -> elabE (True, a,inty, qq) (PApp fc (PRef fc pairTy)
290+ TType _ -> elab' ina (PApp fc (PRef fc pairTy)
287291 [pexp l,pexp r])
288− _ -> elabE (True, a, inty, qq) (PApp fc (PRef fc pairCon)
289− [pimp (sMN 0 "A") Placeholder True,
290− pimp (sMN 0 "B") Placeholder True,
292+ _ -> elab' ina (PApp fc (PRef fc pairCon)
293+ [pimp (sUN "A") Placeholder False,
294+ pimp (sUN "B") Placeholder False,
291295 pexp l, pexp r])
292296 elab' ina (PDPair fc p l@(PRef _ n) t r)
293297 = case t of
test/quasiquote001/expected+3−3
@@ -1,5 +1,5 @@
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)))))) (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))))))
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)))))) (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))))))
22--------------
3−(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)))))
3+(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)))))
44--------------
5−(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))))
5+(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))))