@@ -176,6 +176,35 @@ class Desugarer(val elaborator: Elaborator)(using UnderCtx)
176
176
nominate(ctx, term(coda)(using ctx)):
177
177
expandMatch(_, pat, sequel)(fallback)
178
178
expandMatch(scrutSymbol, headPattern, tailSplit)(fallback)
179
+
180
+ def termSplit (trees : Ls [Tree ], finish : Term => Term ): Split => Sequel =
181
+ trees.foldRight(default): (t, elabFallback) =>
182
+ t match
183
+ case LetLike (`let`, ident @ Ident (_), N , N ) => ???
184
+ case LetLike (`let`, ident @ Ident (_), S (termTree), N ) => fallback => ctx => trace(
185
+ pre = s " termSplit: let ${ident.name} = $termTree" ,
186
+ post = (res : Split ) => s " termSplit: let >>> $res"
187
+ ):
188
+ val sym = VarSymbol (ident)
189
+ val fallbackCtx = ctx + (ident.name -> sym)
190
+ Split .Let (sym, term(termTree)(using ctx), elabFallback(fallback)(fallbackCtx)).withLocOf(t)
191
+ case Modified (Keyword .`do`, doLoc, computation) => fallback => ctx => trace(
192
+ pre = s " termSplit: do $computation" ,
193
+ post = (res : Split ) => s " termSplit: else >>> $res"
194
+ ):
195
+ val sym = TempSymbol (N , " doTemp" )
196
+ Split .Let (sym, term(computation)(using ctx), elabFallback(fallback)(ctx)).withLocOf(t)
197
+ case Modified (Keyword .`else`, elsLoc, default) => fallback => ctx => trace(
198
+ pre = s " termSplit: else $default" ,
199
+ post = (res : Split ) => s " termSplit: else >>> $res"
200
+ ):
201
+ // TODO: report `rest` as unreachable
202
+ Split .default(term(default)(using ctx)).withLocOf(t)
203
+ case branch => fallback => ctx => trace(
204
+ pre = s " termSplit: $branch" ,
205
+ post = (res : Split ) => s " termSplit >>> $res"
206
+ ):
207
+ termSplit(branch, finish)(elabFallback(fallback)(ctx))(ctx)
179
208
180
209
/** Desugar a _term split_ (TS) into a _split_ of core abstract syntax.
181
210
* @param tree the tree representing the term split.
@@ -187,34 +216,7 @@ class Desugarer(val elaborator: Elaborator)(using UnderCtx)
187
216
def termSplit (tree : Tree , finish : Term => Term ): Split => Sequel =
188
217
log(s " termSplit: $tree" )
189
218
tree match
190
- case blk : Block =>
191
- blk.desugStmts.foldRight(default): (t, elabFallback) =>
192
- t match
193
- case LetLike (`let`, ident @ Ident (_), N , N ) => ???
194
- case LetLike (`let`, ident @ Ident (_), S (termTree), N ) => fallback => ctx => trace(
195
- pre = s " termSplit: let ${ident.name} = $termTree" ,
196
- post = (res : Split ) => s " termSplit: let >>> $res"
197
- ):
198
- val sym = VarSymbol (ident)
199
- val fallbackCtx = ctx + (ident.name -> sym)
200
- Split .Let (sym, term(termTree)(using ctx), elabFallback(fallback)(fallbackCtx)).withLocOf(t)
201
- case Modified (Keyword .`do`, doLoc, computation) => fallback => ctx => trace(
202
- pre = s " termSplit: do $computation" ,
203
- post = (res : Split ) => s " termSplit: else >>> $res"
204
- ):
205
- val sym = TempSymbol (N , " doTemp" )
206
- Split .Let (sym, term(computation)(using ctx), elabFallback(fallback)(ctx)).withLocOf(t)
207
- case Modified (Keyword .`else`, elsLoc, default) => fallback => ctx => trace(
208
- pre = s " termSplit: else $default" ,
209
- post = (res : Split ) => s " termSplit: else >>> $res"
210
- ):
211
- // TODO: report `rest` as unreachable
212
- Split .default(term(default)(using ctx)).withLocOf(t)
213
- case branch => fallback => ctx => trace(
214
- pre = s " termSplit: $branch" ,
215
- post = (res : Split ) => s " termSplit >>> $res"
216
- ):
217
- termSplit(branch, finish)(elabFallback(fallback)(ctx))(ctx).withLocOf(t)
219
+ case blk : Block => termSplit(blk.desugStmts, finish)
218
220
case coda is rhs => fallback => ctx =>
219
221
nominate(ctx, finish(term(coda)(using ctx))):
220
222
patternSplit(rhs, _)(fallback)
@@ -246,6 +248,7 @@ class Desugarer(val elaborator: Elaborator)(using UnderCtx)
246
248
):
247
249
nominate(ctx, finish(term(headCoda)(using ctx))):
248
250
expandMatch(_, headPattern, tailSplit)(fallback)
251
+ // Handle binary operators.
249
252
case tree @ OpApp (lhs, opIdent @ Ident (opName), rhss) => fallback => ctx => trace(
250
253
pre = s " termSplit: after op <<< $opName" ,
251
254
post = (res : Split ) => s " termSplit: after op >>> $res"
@@ -261,35 +264,10 @@ class Desugarer(val elaborator: Elaborator)(using UnderCtx)
261
264
val arguments = Term .Tup (first :: second :: Nil )(Tree .DummyTup )
262
265
val joint = FlowSymbol (" ‹applied-result›" )
263
266
Term .App (opRef, arguments)(Tree .DummyApp , N , joint)
264
- rhss match
265
- case rhs :: Nil => termSplit(rhs, finishInner)(fallback)
266
- case _ => ???
267
- case tree @ App (opIdent @ Ident (opName), rawTup @ Tup (lhs :: rhs :: Nil )) => fallback => ctx => trace(
268
- pre = s " termSplit: after op <<< $opName" ,
269
- post = (res : Split ) => s " termSplit: after op >>> $res"
270
- ):
271
- // Resolve the operator.
272
- val opRef = term(opIdent)
273
- // Elaborate and finish the LHS. Nominate the LHS if necessary.
274
- nominate(ctx, finish(term(lhs)(using ctx))): lhsSymbol =>
275
- // Compose a function that takes the RHS and finishes the application.
276
- val finishInner = (rhsTerm : Term ) =>
277
- val first = Fld (FldFlags .empty, lhsSymbol.ref(/* FIXME ident? */ ), N )
278
- val second = Fld (FldFlags .empty, rhsTerm, N )
279
- val arguments = Term .Tup (first :: second :: Nil )(rawTup)
280
- val joint = FlowSymbol (" ‹applied-result›" )
281
- Term .App (opRef, arguments)(tree, N , joint)
282
- termSplit(rhs, finishInner)(fallback)
267
+ termSplit(rhss, finishInner)(fallback)
283
268
// Handle operator splits.
284
269
case tree @ OpSplit (lhs, rhss) => fallback => ctx =>
285
270
nominate(ctx, finish(term(lhs)(using ctx))): vs =>
286
- val mkInnerFinish = (op : Term ) => (rhsTerm : Term ) =>
287
- val first = Fld (FldFlags .empty, vs.ref(/* FIXME ident? */ ), N )
288
- val second = Fld (FldFlags .empty, rhsTerm, N )
289
- val rawTup = Tup (lhs :: Nil ): Tup // <-- loc might be wrong
290
- val arguments = Term .Tup (first :: second :: Nil )(rawTup)
291
- val joint = FlowSymbol (" ‹applied-result›" )
292
- Term .App (op, arguments)(Tree .DummyApp , N , joint)
293
271
rhss.foldRight(Function .const(fallback): Sequel ): (branch, elabFallback) =>
294
272
branch match
295
273
case LetLike (`let`, pat, termTree, N ) => ctx =>
0 commit comments