git.iko.soy/Idris-dev
on master help sign in
Add some Quotable implementations (#3104)

This adds Quotable implementations for every public datatype in Language.Reflection and Language.Reflection.Elab and for a couple of additional types which are returned by primitive Elab actions (namely Pair and Unit).

commit8d78d3225fe2191e0b902cbd16859214082d13d9 authorMelvar Chen <Melvar.Chen@googlemail.com> dateSun 10 Apr 2016, 19:56 (11 years ago) parent3408098
4 files changed+243−29
compare with master
unifiedsplit
libs/prelude/Language/Reflection.idr+108−22 libs/prelude/Language/Reflection/Elab.idr+134 test/meta002/AgdaStyleReflection.idr−6 test/meta002/expected+1−1
libs/prelude/Language/Reflection.idr+108−22
@@ -942,20 +942,6 @@ implementation Quotable String Raw where
942942 quotedTy = `(String)
943943 quote x = RConstant (Str x)
944944
945−implementation Quotable NameType TT where
946− quotedTy = `(NameType)
947− quote Bound = `(Bound)
948− quote Ref = `(Ref)
949− quote (DCon x y) = `(DCon ~(quote x) ~(quote y))
950− quote (TCon x y) = `(TCon ~(quote x) ~(quote y))
951−
952−implementation Quotable NameType Raw where
953− quotedTy = `(NameType)
954− quote Bound = `(Bound)
955− quote Ref = `(Ref)
956− quote (DCon x y) = `(DCon ~(quote {t=Raw} x) ~(quote {t=Raw} y))
957− quote (TCon x y) = `(TCon ~(quote {t=Raw} x) ~(quote {t=Raw} y))
958−
959945implementation Quotable a TT => Quotable (List a) TT where
960946 quotedTy = `(List ~(quotedTy {a}))
961947 quote [] = `(List.Nil {elem=~(quotedTy {a})})
@@ -966,6 +952,22 @@ implementation Quotable a Raw => Quotable (List a) Raw where
966952 quote [] = `(List.Nil {elem=~(quotedTy {a})})
967953 quote (x :: xs) = `(List.(::) {elem=~(quotedTy {a})} ~(quote x) ~(quote xs))
968954
955+implementation Quotable () TT where
956+ quotedTy = `(Unit)
957+ quote () = `(MkUnit)
958+
959+implementation Quotable () Raw where
960+ quotedTy = `(Unit)
961+ quote () = `(MkUnit)
962+
963+implementation (Quotable a TT, Quotable b TT) => Quotable (a, b) TT where
964+ quotedTy = `(Pair ~(quotedTy {a=a}) ~(quotedTy {a=b}))
965+ quote (x, y) = `(MkPair {A=~(quotedTy {a=a})} {B=~(quotedTy {a=b})} ~(quote x) ~(quote y))
966+
967+implementation (Quotable a Raw, Quotable b Raw) => Quotable (a, b) Raw where
968+ quotedTy = `(Pair ~(quotedTy {a=a}) ~(quotedTy {a=b}))
969+ quote (x, y) = `(MkPair {A=~(quotedTy {a=a})} {B=~(quotedTy {a=b})} ~(quote x) ~(quote y))
970+
969971implementation Quotable SourceLocation TT where
970972 quotedTy = `(SourceLocation)
971973 quote (FileLoc fn (sl, sc) (el, ec)) =
@@ -1022,6 +1024,16 @@ mutual
10221024 quote (MetaN parent meta) = `(MetaN ~(quote parent) ~(quote meta))
10231025
10241026
1027+implementation Quotable TTUExp TT where
1028+ quotedTy = `(TTUExp)
1029+ quote (UVar x) = `(UVar ~(quote x))
1030+ quote (UVal x) = `(UVal ~(quote x))
1031+
1032+implementation Quotable TTUExp Raw where
1033+ quotedTy = `(TTUExp)
1034+ quote (UVar x) = `(UVar ~(quote {t=Raw} x))
1035+ quote (UVal x) = `(UVal ~(quote {t=Raw} x))
1036+
10251037implementation Quotable NativeTy TT where
10261038 quotedTy = `(NativeTy)
10271039 quote IT8 = `(Reflection.IT8)
@@ -1096,15 +1108,19 @@ implementation Quotable Const Raw where
10961108 quote WorldType = `(WorldType)
10971109 quote TheWorld = `(TheWorld)
10981110
1099−implementation Quotable TTUExp TT where
1100− quotedTy = `(TTUExp)
1101− quote (UVar x) = `(UVar ~(quote x))
1102− quote (UVal x) = `(UVal ~(quote x))
1111+implementation Quotable NameType TT where
1112+ quotedTy = `(NameType)
1113+ quote Bound = `(Bound)
1114+ quote Ref = `(Ref)
1115+ quote (DCon x y) = `(DCon ~(quote x) ~(quote y))
1116+ quote (TCon x y) = `(TCon ~(quote x) ~(quote y))
11031117
1104−implementation Quotable TTUExp Raw where
1105− quotedTy = `(TTUExp)
1106− quote (UVar x) = `(UVar ~(quote {t=Raw} x))
1107− quote (UVal x) = `(UVal ~(quote {t=Raw} x))
1118+implementation Quotable NameType Raw where
1119+ quotedTy = `(NameType)
1120+ quote Bound = `(Bound)
1121+ quote Ref = `(Ref)
1122+ quote (DCon x y) = `(DCon ~(quote {t=Raw} x) ~(quote {t=Raw} y))
1123+ quote (TCon x y) = `(TCon ~(quote {t=Raw} x) ~(quote {t=Raw} y))
11081124
11091125implementation Quotable Universe TT where
11101126 quotedTy = `(Universe)
@@ -1144,6 +1160,38 @@ mutual
11441160 quote (PVar x) = `(PVar {a=TT} ~(assert_total (quote x)))
11451161 quote (PVTy x) = `(PVTy {a=TT} ~(assert_total (quote x)))
11461162
1163+mutual
1164+ quoteTTRaw : TT -> Raw
1165+ quoteTTRaw (P nt n tm) = `(P ~(quote nt) ~(quote n) ~(quoteTTRaw tm))
1166+ quoteTTRaw (V x) = `(V ~(quote x))
1167+ quoteTTRaw (Bind n b tm) = `(Bind ~(quote n) ~(assert_total $ quoteTTBinderRaw b) ~(quoteTTRaw tm))
1168+ quoteTTRaw (App f x) = `(App ~(quoteTTRaw f) ~(quoteTTRaw x))
1169+ quoteTTRaw (TConst c) = `(TConst ~(quote c))
1170+ quoteTTRaw Erased = `(Erased)
1171+ quoteTTRaw (TType uexp) = `(TType ~(quote uexp))
1172+ quoteTTRaw (UType u) = `(UType ~(quote u))
1173+
1174+ quoteTTBinderRaw : Binder TT -> Raw
1175+ quoteTTBinderRaw (Lam x) = `(Lam {a=TT} ~(quoteTTRaw x))
1176+ quoteTTBinderRaw (Pi x k) = `(Pi {a=TT} ~(quoteTTRaw x)
1177+ ~(quoteTTRaw k))
1178+ quoteTTBinderRaw (Let x y) = `(Let {a=TT} ~(quoteTTRaw x)
1179+ ~(quoteTTRaw y))
1180+ quoteTTBinderRaw (Hole x) = `(Hole {a=TT} ~(quoteTTRaw x))
1181+ quoteTTBinderRaw (GHole x) = `(GHole {a=TT} ~(quoteTTRaw x))
1182+ quoteTTBinderRaw (Guess x y) = `(Guess {a=TT} ~(quoteTTRaw x)
1183+ ~(quoteTTRaw y))
1184+ quoteTTBinderRaw (PVar x) = `(PVar {a=TT} ~(quoteTTRaw x))
1185+ quoteTTBinderRaw (PVTy x) = `(PVTy {a=TT} ~(quoteTTRaw x))
1186+
1187+implementation Quotable TT Raw where
1188+ quotedTy = `(TT)
1189+ quote = quoteTTRaw
1190+
1191+implementation Quotable (Binder TT) Raw where
1192+ quotedTy = `(Binder TT)
1193+ quote = quoteTTBinderRaw
1194+
11471195mutual
11481196 quoteRawTT : Raw -> TT
11491197 quoteRawTT (Var n) = `(Var ~(quote n))
@@ -1206,6 +1254,14 @@ implementation Quotable ErrorReportPart TT where
12061254 quote (RawPart tm) = `(RawPart ~(quote tm))
12071255 quote (SubReport xs) = `(SubReport ~(assert_total $ quote xs))
12081256
1257+implementation Quotable ErrorReportPart Raw where
1258+ quotedTy = `(ErrorReportPart)
1259+ quote (TextPart x) = `(TextPart ~(quote x))
1260+ quote (NamePart n) = `(NamePart ~(quote n))
1261+ quote (TermPart tm) = `(TermPart ~(quote tm))
1262+ quote (RawPart tm) = `(RawPart ~(quote tm))
1263+ quote (SubReport xs) = `(SubReport ~(assert_total $ quote xs))
1264+
12091265implementation Quotable Tactic TT where
12101266 quotedTy = `(Tactic)
12111267 quote (Try tac tac') = `(Try ~(quote tac) ~(quote tac'))
@@ -1235,3 +1291,33 @@ implementation Quotable Tactic TT where
12351291 quote Skip = `(Skip)
12361292 quote (Fail xs) = `(Fail ~(quote xs))
12371293 quote SourceFC = `(SourceFC)
1294+
1295+implementation Quotable Tactic Raw where
1296+ quotedTy = `(Tactic)
1297+ quote (Try tac tac') = `(Try ~(quote tac) ~(quote tac'))
1298+ quote (GoalType x tac) = `(GoalType ~(quote x) ~(quote tac))
1299+ quote (Refine n) = `(Refine ~(quote n))
1300+ quote (Claim n ty) = `(Claim ~(quote n) ~(quote ty))
1301+ quote Unfocus = `(Unfocus)
1302+ quote (Seq tac tac') = `(Seq ~(quote tac) ~(quote tac'))
1303+ quote Trivial = `(Trivial)
1304+ quote (Search x) = `(Search ~(quote x))
1305+ quote Instance = `(Instance)
1306+ quote Solve = `(Solve)
1307+ quote Intros = `(Intros)
1308+ quote (Intro n) = `(Intro ~(quote n))
1309+ quote (ApplyTactic tm) = `(ApplyTactic ~(quote tm))
1310+ quote (Reflect tm) = `(Reflect ~(quote tm))
1311+ quote (ByReflection tm) = `(ByReflection ~(quote tm))
1312+ quote (Fill tm) = `(Fill ~(quote tm))
1313+ quote (Exact tm) = `(Exact ~(quote tm))
1314+ quote (Focus n) = `(Focus ~(quote n))
1315+ quote (Rewrite tm) = `(Rewrite ~(quote tm))
1316+ quote (Induction tm) = `(Induction ~(quote tm))
1317+ quote (Case tm) = `(Case ~(quote tm))
1318+ quote (LetTac n tm) = `(LetTac ~(quote n) ~(quote tm))
1319+ quote (LetTacTy n tm tm') = `(LetTacTy ~(quote n) ~(quote tm) ~(quote tm'))
1320+ quote Compute = `(Compute)
1321+ quote Skip = `(Skip)
1322+ quote (Fail xs) = `(Fail ~(quote xs))
1323+ quote SourceFC = `(SourceFC)
libs/prelude/Language/Reflection/Elab.idr+134
@@ -630,3 +630,137 @@ namespace Tactics
630630 runElab : Raw -> Elab () -> Elab (TT, TT)
631631 runElab goal script = Prim__RecursiveElab goal script
632632
633+---------------------------
634+-- Quotable Implementations
635+---------------------------
636+
637+implementation Quotable Fixity TT where
638+ quotedTy = `(Fixity)
639+ quote (Infixl k) = `(Infixl ~(quote k))
640+ quote (Infixr k) = `(Infixr ~(quote k))
641+ quote (Infix k) = `(Infix ~(quote k))
642+ quote (Prefix k) = `(Prefix ~(quote k))
643+
644+implementation Quotable Fixity Raw where
645+ quotedTy = `(Fixity)
646+ quote (Infixl k) = `(Infixl ~(quote k))
647+ quote (Infixr k) = `(Infixr ~(quote k))
648+ quote (Infix k) = `(Infix ~(quote k))
649+ quote (Prefix k) = `(Prefix ~(quote k))
650+
651+implementation Quotable Erasure TT where
652+ quotedTy = `(Erasure)
653+ quote Erased = `(Elab.Erased)
654+ quote NotErased = `(NotErased)
655+
656+implementation Quotable Erasure Raw where
657+ quotedTy = `(Erasure)
658+ quote Erased = `(Elab.Erased)
659+ quote NotErased = `(NotErased)
660+
661+implementation Quotable Plicity TT where
662+ quotedTy = `(Plicity)
663+ quote Explicit = `(Explicit)
664+ quote Implicit = `(Implicit)
665+ quote Constraint = `(Constraint)
666+
667+implementation Quotable Plicity Raw where
668+ quotedTy = `(Plicity)
669+ quote Explicit = `(Explicit)
670+ quote Implicit = `(Implicit)
671+ quote Constraint = `(Constraint)
672+
673+implementation Quotable FunArg TT where
674+ quotedTy = `(FunArg)
675+ quote (MkFunArg name type plicity erasure) =
676+ `(MkFunArg ~(quote name) ~(quote type) ~(quote plicity) ~(quote erasure))
677+
678+implementation Quotable FunArg Raw where
679+ quotedTy = `(FunArg)
680+ quote (MkFunArg name type plicity erasure) =
681+ `(MkFunArg ~(quote name) ~(quote type) ~(quote plicity) ~(quote erasure))
682+
683+implementation Quotable TyConArg TT where
684+ quotedTy = `(TyConArg)
685+ quote (TyConParameter arg) = `(TyConParameter ~(quote arg))
686+ quote (TyConIndex arg) = `(TyConIndex ~(quote arg))
687+
688+implementation Quotable TyConArg Raw where
689+ quotedTy = `(TyConArg)
690+ quote (TyConParameter arg) = `(TyConParameter ~(quote arg))
691+ quote (TyConIndex arg) = `(TyConIndex ~(quote arg))
692+
693+implementation Quotable TyDecl TT where
694+ quotedTy = `(TyDecl)
695+ quote (Declare name arguments returnType) =
696+ `(Declare ~(quote name) ~(quote arguments) ~(quote returnType))
697+
698+implementation Quotable TyDecl Raw where
699+ quotedTy = `(TyDecl)
700+ quote (Declare name arguments returnType) =
701+ `(Declare ~(quote name) ~(quote arguments) ~(quote returnType))
702+
703+implementation (Quotable a TT) => Quotable (FunClause a) TT where
704+ quotedTy = `(FunClause ~(quotedTy {a}))
705+ quote (MkFunClause lhs rhs) =
706+ `(MkFunClause {a = ~(quotedTy {a})} ~(quote lhs) ~(quote rhs))
707+ quote (MkImpossibleClause lhs) =
708+ `(MkImpossibleClause {a = ~(quotedTy {a})} ~(quote lhs))
709+
710+implementation (Quotable a Raw) => Quotable (FunClause a) Raw where
711+ quotedTy = `(FunClause ~(quotedTy {a}))
712+ quote (MkFunClause lhs rhs) =
713+ `(MkFunClause {a = ~(quotedTy {a})} ~(quote lhs) ~(quote rhs))
714+ quote (MkImpossibleClause lhs) =
715+ `(MkImpossibleClause {a = ~(quotedTy {a})} ~(quote lhs))
716+
717+implementation (Quotable a TT) => Quotable (FunDefn a) TT where
718+ quotedTy = `(FunDefn ~(quotedTy {a}))
719+ quote (DefineFun name clauses) =
720+ `(DefineFun {a = ~(quotedTy {a})} ~(quote name) ~(quote clauses))
721+
722+implementation (Quotable a Raw) => Quotable (FunDefn a) Raw where
723+ quotedTy = `(FunDefn ~(quotedTy {a}))
724+ quote (DefineFun name clauses) =
725+ `(DefineFun {a = ~(quotedTy {a})} ~(quote name) ~(quote clauses))
726+
727+implementation Quotable ConstructorDefn TT where
728+ quotedTy = `(ConstructorDefn)
729+ quote (Constructor name arguments returnType) =
730+ `(Constructor ~(quote name) ~(quote arguments) ~(quote returnType))
731+
732+implementation Quotable ConstructorDefn Raw where
733+ quotedTy = `(ConstructorDefn)
734+ quote (Constructor name arguments returnType) =
735+ `(Constructor ~(quote name) ~(quote arguments) ~(quote returnType))
736+
737+implementation Quotable DataDefn TT where
738+ quotedTy = `(DataDefn)
739+ quote (DefineDatatype name constructors) =
740+ `(DefineDatatype ~(quote name) ~(quote constructors))
741+
742+implementation Quotable DataDefn Raw where
743+ quotedTy = `(DataDefn)
744+ quote (DefineDatatype name constructors) =
745+ `(DefineDatatype ~(quote name) ~(quote constructors))
746+
747+implementation Quotable CtorArg TT where
748+ quotedTy = `(CtorArg)
749+ quote (CtorParameter arg) = `(CtorParameter ~(quote arg))
750+ quote (CtorField arg) = `(CtorField ~(quote arg))
751+
752+implementation Quotable CtorArg Raw where
753+ quotedTy = `(CtorArg)
754+ quote (CtorParameter arg) = `(CtorParameter ~(quote arg))
755+ quote (CtorField arg) = `(CtorField ~(quote arg))
756+
757+implementation Quotable Datatype TT where
758+ quotedTy = `(Datatype)
759+ quote (MkDatatype name tyConArgs tyConRes constructors) =
760+ `(MkDatatype ~(quote name) ~(quote tyConArgs) ~(quote tyConRes) ~(quote constructors))
761+
762+implementation Quotable Datatype Raw where
763+ quotedTy = `(Datatype)
764+ quote (MkDatatype name tyConArgs tyConRes constructors) =
765+ `(MkDatatype ~(quote name) ~(quote tyConArgs) ~(quote tyConRes) ~(quote constructors))
766+
test/meta002/AgdaStyleReflection.idr−6
@@ -40,12 +40,6 @@ data Term
4040 | Constant Const
4141 | Ty
4242
43−implementation Quotable Plicity Raw where
44− quotedTy = `(Plicity)
45− quote Explicit = `(Explicit)
46− quote Implicit = `(Implicit)
47− quote Constraint = `(Constraint)
48−
4943implementation (Quotable a Raw) => Quotable (Arg a) Raw where
5044 quotedTy = `(Arg ~(quotedTy {a=a}))
5145 quote (MkArg plicity argValue) =
test/meta002/expected+1−1
@@ -6,7 +6,7 @@ When checking right hand side of testElab3 with expected type
66 DPair Ty (Tm [])
77
88Unifying ty and ARR ty t would lead to infinite value
9−AgdaStyleReflection.idr:321:5:
9+AgdaStyleReflection.idr:315:5:
1010When checking right hand side of baz with expected type
1111 (Nat, Void)
1212