0 | module TTImp.TTImp.Traversals
8 | parameters (f : RawImp' nm -> RawImp' nm)
11 | mapTTImp : RawImp' nm -> RawImp' nm
14 | mapPiInfo : PiInfo (RawImp' nm) -> PiInfo (RawImp' nm)
15 | mapPiInfo Implicit = Implicit
16 | mapPiInfo Explicit = Explicit
17 | mapPiInfo AutoImplicit = AutoImplicit
18 | mapPiInfo (DefImplicit t) = DefImplicit (mapTTImp t)
21 | mapImpClause : ImpClause' nm -> ImpClause' nm
22 | mapImpClause (PatClause fc lhs rhs) = PatClause fc (mapTTImp lhs) (mapTTImp rhs)
23 | mapImpClause (WithClause fc lhs rig wval prf flags cls)
24 | = WithClause fc (mapTTImp lhs) rig (mapTTImp wval) prf flags (assert_total $
map mapImpClause cls)
25 | mapImpClause (ImpossibleClause fc lhs) = ImpossibleClause fc (mapTTImp lhs)
28 | mapFnOpt : FnOpt' nm -> FnOpt' nm
29 | mapFnOpt Unsafe = Unsafe
30 | mapFnOpt Inline = Inline
31 | mapFnOpt NoInline = NoInline
32 | mapFnOpt Deprecate = Deprecate
33 | mapFnOpt TCInline = TCInline
34 | mapFnOpt (Hint b) = Hint b
35 | mapFnOpt (GlobalHint b) = GlobalHint b
36 | mapFnOpt ExternFn = ExternFn
37 | mapFnOpt (ForeignFn ts) = ForeignFn (map mapTTImp ts)
38 | mapFnOpt (ForeignExport ts) = ForeignExport (map mapTTImp ts)
39 | mapFnOpt Invertible = Invertible
40 | mapFnOpt (Totality treq) = Totality treq
41 | mapFnOpt Macro = Macro
42 | mapFnOpt (SpecArgs ns) = SpecArgs ns
45 | mapImpData : ImpData' nm -> ImpData' nm
46 | mapImpData (MkImpData fc n tycon opts datacons)
47 | = MkImpData fc n (map mapTTImp tycon) opts (map (map mapTTImp) datacons)
48 | mapImpData (MkImpLater fc n tycon) = MkImpLater fc n (mapTTImp tycon)
51 | mapImpRecord : ImpRecordData nm -> ImpRecordData nm
52 | mapImpRecord (MkImpRecord header body)
53 | = MkImpRecord (map (map (map (map mapTTImp))) header)
54 | (map (map (map (map mapTTImp))) body)
57 | mapImpDecl : ImpDecl' nm -> ImpDecl' nm
58 | mapImpDecl (IClaim (MkWithData fc (MkIClaimData rig vis opts ty)))
59 | = IClaim (MkWithData fc (MkIClaimData rig vis (map mapFnOpt opts) (map mapTTImp ty)))
60 | mapImpDecl (IData fc vis mtreq dat) = IData fc vis mtreq (mapImpData dat)
61 | mapImpDecl (IDef fc n cls) = IDef fc n (map mapImpClause cls)
62 | mapImpDecl (IParameters fc params xs) = IParameters fc params (assert_total $
map mapImpDecl xs)
63 | mapImpDecl (IRecord fc mstr x y rec) = IRecord fc mstr x y (map mapImpRecord rec)
64 | mapImpDecl (IFail fc mstr xs) = IFail fc mstr (assert_total $
map mapImpDecl xs)
65 | mapImpDecl (INamespace fc mi xs) = INamespace fc mi (assert_total $
map mapImpDecl xs)
66 | mapImpDecl (ITransform fc n t u) = ITransform fc n (mapTTImp t) (mapTTImp u)
67 | mapImpDecl (IRunElabDecl fc t) = IRunElabDecl fc (mapTTImp t)
68 | mapImpDecl (IPragma fc ns g) = IPragma fc ns g
69 | mapImpDecl (ILog x) = ILog x
70 | mapImpDecl (IBuiltin fc x n) = IBuiltin fc x n
73 | mapIFieldUpdate : IFieldUpdate' nm -> IFieldUpdate' nm
74 | mapIFieldUpdate (ISetField path t) = ISetField path (mapTTImp t)
75 | mapIFieldUpdate (ISetFieldApp path t) = ISetFieldApp path (mapTTImp t)
78 | mapAltType : AltType' nm -> AltType' nm
79 | mapAltType FirstSuccess = FirstSuccess
80 | mapAltType Unique = Unique
81 | mapAltType (UniqueDefault t) = UniqueDefault (mapTTImp t)
83 | mapTTImp t@(IVar {}) = f t
84 | mapTTImp (IPi fc rig pinfo x argTy retTy)
85 | = f $
IPi fc rig (mapPiInfo pinfo) x (mapTTImp argTy) (mapTTImp retTy)
86 | mapTTImp (ILam fc rig pinfo x argTy lamTy)
87 | = f $
ILam fc rig (mapPiInfo pinfo) x (mapTTImp argTy) (mapTTImp lamTy)
88 | mapTTImp (ILet fc lhsFC rig n nTy nVal scope)
89 | = f $
ILet fc lhsFC rig n (mapTTImp nTy) (mapTTImp nVal) (mapTTImp scope)
90 | mapTTImp (ICase fc opts t ty cls)
91 | = f $
ICase fc opts (mapTTImp t) (mapTTImp ty) (assert_total $
map mapImpClause cls)
92 | mapTTImp (ILocal fc xs t)
93 | = f $
ILocal fc (assert_total $
map mapImpDecl xs) (mapTTImp t)
94 | mapTTImp (ICaseLocal fc unm inm args t) = f $
ICaseLocal fc unm inm args (mapTTImp t)
95 | mapTTImp (IUpdate fc upds t) = f $
IUpdate fc (assert_total map mapIFieldUpdate upds) (mapTTImp t)
96 | mapTTImp (IApp fc t u) = f $
IApp fc (mapTTImp t) (mapTTImp u)
97 | mapTTImp (IAutoApp fc t u) = f $
IAutoApp fc (mapTTImp t) (mapTTImp u)
98 | mapTTImp (INamedApp fc t n u) = f $
INamedApp fc (mapTTImp t) n (mapTTImp u)
99 | mapTTImp (IWithApp fc t u) = f $
IWithApp fc (mapTTImp t) (mapTTImp u)
100 | mapTTImp (ISearch fc depth) = f $
ISearch fc depth
101 | mapTTImp (IAlternative fc alt ts) = f $
IAlternative fc (mapAltType alt) (assert_total map mapTTImp ts)
102 | mapTTImp (IRewrite fc t u) = f $
IRewrite fc (mapTTImp t) (mapTTImp u)
103 | mapTTImp (ICoerced fc t) = f $
ICoerced fc (mapTTImp t)
104 | mapTTImp (IBindHere fc bm t) = f $
IBindHere fc bm (mapTTImp t)
105 | mapTTImp (IBindVar fc str) = f $
IBindVar fc str
106 | mapTTImp (IAs fc nameFC side n t) = f $
IAs fc nameFC side n (mapTTImp t)
107 | mapTTImp (IMustUnify fc x t) = f $
IMustUnify fc x (mapTTImp t)
108 | mapTTImp (IDelayed fc lz t) = f $
IDelayed fc lz (mapTTImp t)
109 | mapTTImp (IDelay fc t) = f $
IDelay fc (mapTTImp t)
110 | mapTTImp (IForce fc t) = f $
IForce fc (mapTTImp t)
111 | mapTTImp (IQuote fc t) = f $
IQuote fc (mapTTImp t)
112 | mapTTImp (IQuoteName fc n) = f $
IQuoteName fc n
113 | mapTTImp (IQuoteDecl fc xs) = f $
IQuoteDecl fc (assert_total $
map mapImpDecl xs)
114 | mapTTImp (IUnquote fc t) = f $
IUnquote fc (mapTTImp t)
115 | mapTTImp (IRunElab fc re t) = f $
IRunElab fc re (mapTTImp t)
116 | mapTTImp (IPrimVal fc c) = f $
IPrimVal fc c
117 | mapTTImp (IType fc) = f $
IType fc
118 | mapTTImp (IHole fc str) = f $
IHole fc str
119 | mapTTImp (IUnifyLog fc x t) = f $
IUnifyLog fc x (mapTTImp t)
120 | mapTTImp (Implicit fc bindIfUnsolved) = f $
Implicit fc bindIfUnsolved
121 | mapTTImp (IWithUnambigNames fc xs t) = f $
IWithUnambigNames fc xs (mapTTImp t)