0 | module TTImp.TTImp.Functor
  1 |
  2 | import Core.TT
  3 | import Core.WithData
  4 | import TTImp.TTImp
  5 |
  6 | %default covering
  7 |
  8 | mutual
  9 |
 10 |   export
 11 |   Functor RawImp' where
 12 |     map f (IVar fc nm) = IVar fc (f nm)
 13 |     map f (IPi fc rig info nm a sc)
 14 |       = IPi fc rig (map (map f) info) nm (map f a) (map f sc)
 15 |     map f (ILam fc rig info nm a sc)
 16 |       = ILam fc rig (map (map f) info) nm (map f a) (map f sc)
 17 |     map f (ILet fc lhsFC rig nm ty val sc)
 18 |       = ILet fc lhsFC rig nm (map f ty) (map f val) (map f sc)
 19 |     map f (ICase fc opts sc ty cls)
 20 |       = ICase fc (map (map f) opts) (map f sc) (map f ty) (map (map f) cls)
 21 |     map f (ILocal fc ds sc)
 22 |       = ILocal fc (map (map f) ds) (map f sc)
 23 |     map f (ICaseLocal fc userN intN args sc)
 24 |       = ICaseLocal fc userN intN args (map f sc)
 25 |     map f (IUpdate fc upds rec)
 26 |       = IUpdate fc (map (map f) upds) (map f rec)
 27 |     map f (IApp fc fn t)
 28 |       = IApp fc (map f fn) (map f t)
 29 |     map f (IAutoApp fc fn t)
 30 |       = IAutoApp fc (map f fn) (map f t)
 31 |     map f (INamedApp fc fn nm t)
 32 |       = INamedApp fc (map f fn) nm (map f t)
 33 |     map f (IWithApp fc fn t)
 34 |       = IWithApp fc (map f fn) (map f t)
 35 |     map f (ISearch fc n)
 36 |       = ISearch fc n
 37 |     map f (IAlternative fc alt ts)
 38 |       = IAlternative fc (map f alt) (map (map f) ts)
 39 |     map f (IRewrite fc e t)
 40 |       = IRewrite fc (map f e) (map f t)
 41 |     map f (ICoerced fc e)
 42 |       = ICoerced fc (map f e)
 43 |     map f (IBindHere fc bd t)
 44 |       = IBindHere fc bd (map f t)
 45 |     map f (IBindVar fc str)
 46 |       = IBindVar fc str
 47 |     map f (IAs fc nmFC side nm t)
 48 |       = IAs fc nmFC side nm (map f t)
 49 |     map f (IMustUnify fc reason t)
 50 |       = IMustUnify fc reason (map f t)
 51 |     map f (IDelayed fc reason t)
 52 |       = IDelayed fc reason (map f t)
 53 |     map f (IDelay fc t)
 54 |       = IDelay fc (map f t)
 55 |     map f (IForce fc t)
 56 |       = IForce fc (map f t)
 57 |     map f (IQuote fc t)
 58 |       = IQuote fc (map f t)
 59 |     map f (IQuoteName fc nm)
 60 |       = IQuoteName fc nm
 61 |     map f (IQuoteDecl fc ds)
 62 |       = IQuoteDecl fc (map (map f) ds)
 63 |     map f (IUnquote fc t)
 64 |       = IUnquote fc (map f t)
 65 |     map f (IRunElab fc re t)
 66 |       = IRunElab fc re (map f t)
 67 |     map f (IPrimVal fc c)
 68 |       = IPrimVal fc c
 69 |     map f (IType fc)
 70 |       = IType fc
 71 |     map f (IHole fc str)
 72 |       = IHole fc str
 73 |     map f (IUnifyLog fc lvl t)
 74 |       = IUnifyLog fc lvl (map f t)
 75 |     map f (Implicit fc b)
 76 |       = Implicit fc b
 77 |     map f (IWithUnambigNames fc ns t)
 78 |       = IWithUnambigNames fc ns (map f t)
 79 |
 80 |   export
 81 |   Functor ImpClause' where
 82 |     map f (PatClause fc lhs rhs)
 83 |       = PatClause fc (map f lhs) (map f rhs)
 84 |     map f (WithClause fc lhs rig wval prf flags xs)
 85 |       = WithClause fc (map f lhs) rig (map f wval) prf flags (map (map f) xs)
 86 |     map f (ImpossibleClause fc lhs)
 87 |       = ImpossibleClause fc (map f lhs)
 88 |
 89 |   export
 90 |   Functor IClaimData where
 91 |     map f (MkIClaimData rig vis opts ty)
 92 |       = MkIClaimData rig vis (map (map f) opts) (map (map f) ty)
 93 |
 94 |   export
 95 |   Functor ImpDecl' where
 96 |     map f (IClaim c)
 97 |       = IClaim (map (map f) c)
 98 |     map f (IData fc vis mbtot dt)
 99 |       = IData fc vis mbtot (map f dt)
100 |     map f (IDef fc nm cls)
101 |       = IDef fc nm (map (map f) cls)
102 |     map f (IParameters fc ps ds)
103 |       = IParameters fc (map (map (map (map f))) ps) (map (map f) ds)
104 |     map f (IRecord fc cs vis mbtot rec)
105 |       = IRecord fc cs vis mbtot (map (map f) rec)
106 |     map f (IFail fc msg ds)
107 |       = IFail fc msg (map (map f) ds)
108 |     map f (INamespace fc ns ds)
109 |       = INamespace fc ns (map (map f) ds)
110 |     map f (ITransform fc n lhs rhs)
111 |       = ITransform fc n (map f lhs) (map f rhs)
112 |     map f (IRunElabDecl fc t)
113 |       = IRunElabDecl fc (map f t)
114 |     map f (IPragma fc xs k) = IPragma fc xs k
115 |     map f (ILog x) = ILog x
116 |     map f (IBuiltin fc ty n) = IBuiltin fc ty n
117 |
118 |   export
119 |   Functor FnOpt' where
120 |     map f Unsafe = Unsafe
121 |     map f Inline = Inline
122 |     map f NoInline = NoInline
123 |     map f Deprecate = Deprecate
124 |     map f TCInline = TCInline
125 |     map f (Hint b) = Hint b
126 |     map f (GlobalHint b) = GlobalHint b
127 |     map f ExternFn = ExternFn
128 |     map f (ForeignFn ts) = ForeignFn (map (map f) ts)
129 |     map f (ForeignExport ts) = ForeignExport (map (map f) ts)
130 |     map f Invertible = Invertible
131 |     map f (Totality tot) = Totality tot
132 |     map f Macro = Macro
133 |     map f (SpecArgs ns) = SpecArgs ns
134 |
135 |   export
136 |   Functor ImpData' where
137 |     map f (MkImpData fc n tycon opts datacons)
138 |       = MkImpData fc n (map (map f) tycon) opts (map (map (map f)) datacons)
139 |     map f (MkImpLater fc n tycon)
140 |       = MkImpLater fc n (map f tycon)
141 |
142 |   export
143 |   Functor ImpRecordData where
144 |     map f (MkImpRecord header body)
145 |       = MkImpRecord (map (map (map (map (map f)))) header)
146 |                     (map (map (map (map (map f)))) body)
147 |
148 |   export
149 |   Functor IFieldUpdate' where
150 |     map f (ISetField path t) = ISetField path (map f t)
151 |     map f (ISetFieldApp path t) = ISetFieldApp path (map f t)
152 |
153 |   export
154 |   Functor AltType' where
155 |     map f FirstSuccess = FirstSuccess
156 |     map f Unique = Unique
157 |     map f (UniqueDefault t) = UniqueDefault (map f t)
158 |