@@ -3,9 +3,12 @@ module Language.Reflection
33import Builtins
44import Prelude.Applicative
55import Prelude.Basics
6+import Prelude.Bool
7+import Prelude.Either
68import Prelude.Foldable
79import Prelude.Functor
810import Prelude.List
11+import Prelude.Maybe
912import Prelude.Nat
1013import Prelude.Traversable
1114import Prelude.Uninhabited
@@ -803,6 +806,16 @@ implementation Quotable Nat Raw where
803806 quote Z = `(Z)
804807 quote (S k) = `(S ~(quote k))
805808
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+
806819implementation Quotable Int TT where
807820 quotedTy = `(Int)
808821 quote x = TConst (I x)
@@ -885,6 +898,26 @@ implementation Quotable a Raw => Quotable (List a) Raw where
885898 quote [] = `(List.Nil {elem=~(quotedTy {a})})
886899 quote (x :: xs) = `(List.(::) {elem=~(quotedTy {a})} ~(quote x) ~(quote xs))
887900
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+
888921implementation Quotable () TT where
889922 quotedTy = `(Unit)
890923 quote () = `(MkUnit)