git.iko.soy/Idris-dev
on master help sign in
Add Bool, Maybe, Either implementations for Quotable (#4367)
2184f50Joomy Korkut
libs/prelude/Language/Reflection.idr+33
compare with master
unifiedsplit
@@ -3,9 +3,12 @@ module Language.Reflection
3import Builtins
3import Builtins
4import Prelude.Applicative
4import Prelude.Applicative
5import Prelude.Basics
5import Prelude.Basics
6+import Prelude.Bool
7+import Prelude.Either
6import Prelude.Foldable
8import Prelude.Foldable
7import Prelude.Functor
9import Prelude.Functor
8import Prelude.List
10import Prelude.List
11+import Prelude.Maybe
9import Prelude.Nat
12import Prelude.Nat
10import Prelude.Traversable
13import Prelude.Traversable
11import Prelude.Uninhabited
14import Prelude.Uninhabited
@@ -803,6 +806,16 @@ implementation Quotable Nat Raw where
803 quote Z = `(Z)
806 quote Z = `(Z)
804 quote (S k) = `(S ~(quote k))
807 quote (S k) = `(S ~(quote k))
805
808
809+implementation Quotable Bool TT where
810+ quotedTy = `(Bool)
811+ quote True = `(True)
812+ quote False = `(False)
813+
814+implementation Quotable Bool Raw where
815+ quotedTy = `(Bool)
816+ quote True = `(True)
817+ quote False = `(False)
818+
806implementation Quotable Int TT where
819implementation Quotable Int TT where
807 quotedTy = `(Int)
820 quotedTy = `(Int)
808 quote x = TConst (I x)
821 quote x = TConst (I x)
@@ -885,6 +898,26 @@ implementation Quotable a Raw => Quotable (List a) Raw where
885 quote [] = `(List.Nil {elem=~(quotedTy {a})})
898 quote [] = `(List.Nil {elem=~(quotedTy {a})})
886 quote (x :: xs) = `(List.(::) {elem=~(quotedTy {a})} ~(quote x) ~(quote xs))
899 quote (x :: xs) = `(List.(::) {elem=~(quotedTy {a})} ~(quote x) ~(quote xs))
887
900
901+implementation Quotable a TT => Quotable (Maybe a) TT where
902+ quotedTy = `(Maybe ~(quotedTy {a}))
903+ quote (Just x) = `(Just {a=~(quotedTy {a})} ~(quote x))
904+ quote Nothing = `(Nothing {a=~(quotedTy {a})})
905+
906+implementation Quotable a Raw => Quotable (Maybe a) Raw where
907+ quotedTy = `(Maybe ~(quotedTy {a}))
908+ quote (Just x) = `(Just {a=~(quotedTy {a})} ~(quote x))
909+ quote Nothing = `(Nothing {a=~(quotedTy {a})})
910+
911+implementation (Quotable a TT, Quotable b TT) => Quotable (Either a b) TT where
912+ quotedTy = `(Either ~(quotedTy {a}) ~(quotedTy {a=b}))
913+ quote (Left x) = `(Left {a=~(quotedTy {a})} {b=~(quotedTy {a=b})} ~(quote x))
914+ quote (Right x) = `(Right {a=~(quotedTy {a})} {b=~(quotedTy {a=b})} ~(quote x))
915+
916+implementation (Quotable a Raw, Quotable b Raw) => Quotable (Either a b) Raw where
917+ quotedTy = `(Either ~(quotedTy {a}) ~(quotedTy {a=b}))
918+ quote (Left x) = `(Left {a=~(quotedTy {a})} {b=~(quotedTy {a=b})} ~(quote x))
919+ quote (Right x) = `(Right {a=~(quotedTy {a})} {b=~(quotedTy {a=b})} ~(quote x))
920+
888implementation Quotable () TT where
921implementation Quotable () TT where
889 quotedTy = `(Unit)
922 quotedTy = `(Unit)
890 quote () = `(MkUnit)
923 quote () = `(MkUnit)