Skip to content

Commit

Permalink
unroll suffix terrace cells when remolding if they contain unmolded t…
Browse files Browse the repository at this point in the history
…okens in case they can be molded under new prefix (fix #93)
  • Loading branch information
dm0n3y committed Jan 17, 2025
1 parent db83b1c commit cf69e19
Showing 1 changed file with 15 additions and 0 deletions.
15 changes: 15 additions & 0 deletions src/core/parser/Molder.re
Original file line number Diff line number Diff line change
Expand Up @@ -174,6 +174,21 @@ and remold =
// P.show("rest", Stack.show(rest));
let connected = Stack.connect(t, grouted, rest) |> Stack.extend(tl_w);
let fill = Cell.mark_ends_dirty(hd.cell);
let (fill, r_tl) =
// unroll hd terrace cell if it contains an unmolded obligation,
// in case it can be molded by the new prefix
if (Path.Map.exists(
_ =>
fun
| Mtrl.Space(Space.T.Unmolded) => true
| _ => false,
fill.marks.obligs,
)) {
let (fill, unrolled) = Slope.Up.unroll(fill);
(fill, Stack.cat(unrolled, r_tl));
} else {
(fill, r_tl);
};
if (connected.bound == l.bound) {
remold(~fill, (connected, r_tl));
} else {
Expand Down

0 comments on commit cf69e19

Please sign in to comment.