git.iko.soy/Idris-dev
on master help sign in
Renaming of built-in datatypes works finally
6faa1abAhmad Salim Al-Sibahi
libs/prelude/Builtins.idr+4−3
compare with master
unifiedsplit
@@ -5,18 +5,19 @@
5
5
6||| The canonical single-element type, also known as the trivially
6||| The canonical single-element type, also known as the trivially
7||| true proposition.
7||| true proposition.
8+%elim
8−data Unit =
9+ data Unit =
9 ||| The trivial constructor for `()`.
10 ||| The trivial constructor for `()`.
10 MkUnit
11 MkUnit
11
12
12||| The non-dependent pair type, also known as conjunction.
13||| The non-dependent pair type, also known as conjunction.
13||| @A the type of the left elements in the pair
14||| @A the type of the left elements in the pair
14||| @B the type of the left elements in the pair
15||| @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
16 ||| A pair of elements
17 ||| A pair of elements
17 ||| @a the left element of the pair
18 ||| @a the left element of the pair
18 ||| @b the right element of the pair
19 ||| @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
20
21
21||| Dependent pairs, in their internal representation
22||| Dependent pairs, in their internal representation
22||| @ a the type of the witness
23||| @ a the type of the witness
libs/prelude/Prelude/Basics.idr+2
@@ -1,5 +1,7 @@
1module Prelude.Basics
1module Prelude.Basics
2
2
3+import Builtins
4+
3Not : Type -> Type
5Not : Type -> Type
4Not a = a -> _|_
6Not a = a -> _|_
5
7
libs/prelude/Prelude/Classes.idr−2
@@ -28,10 +28,8 @@ class Eq a where
28 x /= y = not (x == y)
28 x /= y = not (x == y)
29 x == y = not (x /= y)
29 x == y = not (x /= y)
30
30
31−%logging 5
32instance Eq () where
31instance Eq () where
33 () == () = True
32 () == () = True
34−%logging 0
35
33
36instance Eq Int where
34instance Eq Int where
37 (==) = boolOp prim__eqInt
35 (==) = boolOp prim__eqInt
samples/reflection.idr+2−2
@@ -32,13 +32,13 @@ envList = ?envListPrf
32
32
33||| Reflected raw rep. for the type (TTName, TT)
33||| Reflected raw rep. for the type (TTName, TT)
34tupleType : Raw
34tupleType : Raw
35−tupleType = RApp (RApp (Var (MN 0 "__Pair"))
35+tupleType = RApp (RApp (Var (UN "Pair"))
36 (Var (NS (UN "TTName") ["Reflection", "Language"])))
36 (Var (NS (UN "TTName") ["Reflection", "Language"])))
37 (Var (NS (UN "TT") ["Reflection", "Language"]))
37 (Var (NS (UN "TT") ["Reflection", "Language"]))
38
38
39||| Reflected raw rep for the type List (TTName, TT)
39||| Reflected raw rep for the type List (TTName, TT)
40mkTuple : Raw
40mkTuple : Raw
41−mkTuple = RApp (RApp (Var (MN 0 "__MkPair"))
41+mkTuple = RApp (RApp (Var (UN "MkPair"))
42 (Var (NS (UN "TTName") ["Reflection", "Language"])))
42 (Var (NS (UN "TTName") ["Reflection", "Language"])))
43 (Var (NS (UN "TT") ["Reflection", "Language"]))
43 (Var (NS (UN "TT") ["Reflection", "Language"]))
44
44
src/Idris/AbsSyntaxTree.hs+1−24
@@ -1065,16 +1065,10 @@ getInferType (App (App _ ty) _) = ty
1065
1065
1066-- Handy primitives: Unit, False, Pair, MkPair, =, mkForeign
1066-- Handy primitives: Unit, False, Pair, MkPair, =, mkForeign
1067
1067
1068−primNames = [unitTy, unitCon,
1069− falseTy, pairTy, pairCon,
1070− eqTy, eqCon, inferTy, inferCon]
1068+primNames = [falseTy, eqTy, eqCon, inferTy, inferCon]
1071
1069
1072−unitDoc = parseDocstring . T.pack $ "The canonical single-element type, also known as the trivially true proposition."
1073unitTy = sUN "Unit"
1070unitTy = sUN "Unit"
1074unitCon = sUN "MkUnit"
1071unitCon = sUN "MkUnit"
1075−unitDecl = PDatadecl unitTy PType
1076− [(parseDocstring . T.pack $ "The trivial constructor for `()`. ", [], unitCon, PRef bi unitTy, bi, [])]
1077−unitOpts = [DefaultEliminator]
1078
1072
1079falseDoc = parseDocstring . T.pack $
1073falseDoc = parseDocstring . T.pack $
1080 "The empty type, also known as the trivially false proposition." ++
1074 "The empty type, also known as the trivially false proposition." ++
@@ -1085,25 +1079,8 @@ falseTy = sMN 0 "__False"
1085falseDecl = PDatadecl falseTy PType []
1079falseDecl = PDatadecl falseTy PType []
1086falseOpts = []
1080falseOpts = []
1087
1081
1088−pairDoc = parseDocstring . T.pack $ "The non-dependent pair type, also known as conjunction."
1089pairTy = sUN "Pair"
1082pairTy = sUN "Pair"
1090pairCon = sUN "MkPair"
1083pairCon = 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
1107
1084
1108eqTy = sUN "="
1085eqTy = sUN "="
1109eqCon = sUN "Refl"
1086eqCon = sUN "Refl"
src/Idris/ElabDecls.hs+4−4
@@ -76,10 +76,10 @@ elabPrims :: Idris ()
76elabPrims = do mapM_ (elabDecl' EAll recinfo)
76elabPrims = do mapM_ (elabDecl' EAll recinfo)
77 (map (\(opt, decl, docs, argdocs) -> PData docs argdocs defaultSyntax (fileFC "builtin") opt decl)
77 (map (\(opt, decl, docs, argdocs) -> PData docs argdocs defaultSyntax (fileFC "builtin") opt decl)
78 (zip4
78 (zip4
79− [inferOpts, unitOpts, falseOpts, pairOpts, eqOpts]
79+ [inferOpts, falseOpts, eqOpts]
80− [inferDecl, unitDecl, falseDecl, pairDecl, eqDecl]
80+ [inferDecl, falseDecl, eqDecl]
81− [emptyDocstring, unitDoc, falseDoc, pairDoc, eqDoc]
81+ [emptyDocstring, falseDoc, eqDoc]
82− [[], [], [], pairParamDoc, eqParamDoc]))
82+ [[], [], eqParamDoc]))
83 addNameHint eqTy (sUN "prf")
83 addNameHint eqTy (sUN "prf")
84 mapM_ elabPrim primitives
84 mapM_ elabPrim primitives
85 -- Special case prim__believe_me because it doesn't work on just constants
85 -- 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
245-- = lift $ tfail (Msg "Typecase is not allowed")
245-- = lift $ tfail (Msg "Typecase is not allowed")
246 elab' ina (PConstant c) = do apply (RConstant c) []; solve
246 elab' ina (PConstant c) = do apply (RConstant c) []; solve
247 elab' ina (PQuote r) = do fill r; solve
247 elab' ina (PQuote r) = do fill r; solve
248− elab' ina (PTrue fc _) = try (elab' ina (PRef fc unitCon))
248+ elab' ina (PTrue fc _) =
249+ do hnf_compute
250+ g <- goal
251+ case g of
249− (elab' ina (PRef fc unitTy))
252+ TType _ -> elab' ina (PRef fc unitTy)
253+ _ -> elab' ina (PRef fc unitCon)
250 elab' ina (PFalse fc) = elab' ina (PRef fc falseTy)
254 elab' ina (PFalse fc) = elab' ina (PRef fc falseTy)
251 elab' ina (PResolveTC (FC "HACK" _ _)) -- for chasing parent classes
255 elab' ina (PResolveTC (FC "HACK" _ _)) -- for chasing parent classes
252 = do g <- goal; resolveTC False 5 g fn ist
256 = do g <- goal; resolveTC False 5 g fn ist
@@ -283,11 +287,11 @@ elab ist info emode opts fn tm
283 = do hnf_compute
287 = do hnf_compute
284 g <- goal
288 g <- goal
285 case g of
289 case g of
286− TType _ -> elabE (True, a,inty, qq) (PApp fc (PRef fc pairTy)
290+ TType _ -> elab' ina (PApp fc (PRef fc pairTy)
287 [pexp l,pexp r])
291 [pexp l,pexp r])
288− _ -> elabE (True, a, inty, qq) (PApp fc (PRef fc pairCon)
292+ _ -> elab' ina (PApp fc (PRef fc pairCon)
289− [pimp (sMN 0 "A") Placeholder True,
293+ [pimp (sUN "A") Placeholder False,
290− pimp (sMN 0 "B") Placeholder True,
294+ pimp (sUN "B") Placeholder False,
291 pexp l, pexp r])
295 pexp l, pexp r])
292 elab' ina (PDPair fc p l@(PRef _ n) t r)
296 elab' ina (PDPair fc p l@(PRef _ n) t r)
293 = case t of
297 = 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))))))
2--------------
2--------------
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)))))
4--------------
4--------------
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))))