|
| 1 | +(* -------------------------------------------------------------------- *) |
| 2 | +open EcLocation |
| 3 | +open EcParsetree |
| 4 | + |
| 5 | +(* -------------------------------------------------------------------- *) |
| 6 | +type frame = { |
| 7 | + bf_bullet : bullet; |
| 8 | + bf_loc : EcLocation.t; |
| 9 | + bf_floor : int; |
| 10 | +} |
| 11 | + |
| 12 | +type stack = frame list |
| 13 | + |
| 14 | +type error = |
| 15 | + | UnbulletedSplit of { opened : int; level : [`Top | `Frame of frame] } |
| 16 | + | NoSubgoalToOpen of { bullet : bullet } |
| 17 | + | OuterSkipsInner of { bullet : bullet; outer : frame; inner : frame } |
| 18 | + | ReuseBeforeClosing of { bullet : bullet; frame : frame } |
| 19 | + |
| 20 | +exception BulletError of EcLocation.t option * error |
| 21 | + |
| 22 | +(* -------------------------------------------------------------------- *) |
| 23 | +let pp_bullet fmt (b : bullet) = |
| 24 | + let c = match b.b_kind with `Minus -> '-' | `Plus -> '+' | `Star -> '*' in |
| 25 | + for _ = 1 to b.b_count do Format.pp_print_char fmt c done |
| 26 | + |
| 27 | +let pp_error fmt = function |
| 28 | + | UnbulletedSplit { opened; level = `Top } -> |
| 29 | + Format.fprintf fmt |
| 30 | + "previous tactic left %d open subgoals at top level; the next \ |
| 31 | + phrase needs a bullet to focus one of them" opened |
| 32 | + | UnbulletedSplit { opened; level = `Frame f } -> |
| 33 | + Format.fprintf fmt |
| 34 | + "previous tactic left %d open subgoals at the bullet level \ |
| 35 | + opened by `%a' at %s; the next phrase needs a bullet to \ |
| 36 | + focus one of them" |
| 37 | + opened pp_bullet f.bf_bullet (EcLocation.tostring f.bf_loc) |
| 38 | + | NoSubgoalToOpen { bullet } -> |
| 39 | + Format.fprintf fmt |
| 40 | + "bullet `%a' opens a new subproof level but there are no \ |
| 41 | + remaining subgoals" pp_bullet bullet |
| 42 | + | OuterSkipsInner { bullet; outer; inner } -> |
| 43 | + Format.fprintf fmt |
| 44 | + "bullet `%a' (matches an outer level opened at %s) skips past \ |
| 45 | + inner bullet `%a' opened at %s whose subproof is not closed" |
| 46 | + pp_bullet bullet (EcLocation.tostring outer.bf_loc) |
| 47 | + pp_bullet inner.bf_bullet (EcLocation.tostring inner.bf_loc) |
| 48 | + | ReuseBeforeClosing { bullet; frame } -> |
| 49 | + Format.fprintf fmt |
| 50 | + "bullet `%a' reused but the previous subgoal (opened at %s) \ |
| 51 | + is not closed" |
| 52 | + pp_bullet bullet (EcLocation.tostring frame.bf_loc) |
| 53 | + |
| 54 | +(* -------------------------------------------------------------------- *) |
| 55 | +let n_open (juc : EcCoreGoal.proof) = |
| 56 | + List.length (EcCoreGoal.all_hd_opened juc) |
| 57 | + |
| 58 | +let raise_error ?loc err = raise (BulletError (loc, err)) |
| 59 | + |
| 60 | +(* -------------------------------------------------------------------- *) |
| 61 | +(* Validate the bullet against the current stack and return the |
| 62 | + pre-phrase stack. Each frame's [bf_floor] records the open-count |
| 63 | + that should remain once the frame's subproof is fully closed; the |
| 64 | + frame becomes poppable when [n_open <= bf_floor]. *) |
| 65 | +let open_phrase ~(bullet : bullet located option) |
| 66 | + (juc : EcCoreGoal.proof) (stack : stack) : stack = |
| 67 | + let opened = n_open juc in |
| 68 | + (* Top-of-stack floor, or 0 if the stack is empty (top-level: one |
| 69 | + focused goal allowed without a bullet). A phrase may run |
| 70 | + unbulleted iff [opened <= floor_top + 1]: the focused goal |
| 71 | + plus the goals "outside" the current level. *) |
| 72 | + let floor_top = |
| 73 | + match stack with [] -> 0 | f :: _ -> f.bf_floor in |
| 74 | + match bullet with |
| 75 | + | None -> |
| 76 | + if opened > floor_top + 1 then begin |
| 77 | + let level = |
| 78 | + match stack with [] -> `Top | f :: _ -> `Frame f in |
| 79 | + raise_error (UnbulletedSplit { opened; level }) |
| 80 | + end; |
| 81 | + stack |
| 82 | + | Some b -> |
| 83 | + let bul = unloc b in |
| 84 | + let loc = loc b in |
| 85 | + (* Search the stack from innermost outward for a frame matching |
| 86 | + [bul]. Inner frames not yet drained block the match. *) |
| 87 | + let rec scan acc = function |
| 88 | + | [] -> `Open |
| 89 | + | f :: rest when f.bf_bullet = bul -> `Match (List.rev acc, f, rest) |
| 90 | + | f :: rest -> scan (f :: acc) rest |
| 91 | + in |
| 92 | + match scan [] stack with |
| 93 | + | `Open -> |
| 94 | + if opened = 0 then |
| 95 | + raise_error ~loc (NoSubgoalToOpen { bullet = bul }); |
| 96 | + { bf_bullet = bul; bf_loc = loc; bf_floor = opened - 1 } :: stack |
| 97 | + | `Match (inner, frame, outer) -> |
| 98 | + (* Inner frames must already be drained. *) |
| 99 | + List.iter (fun (f : frame) -> |
| 100 | + if opened > f.bf_floor then |
| 101 | + raise_error ~loc |
| 102 | + (OuterSkipsInner { bullet = bul; outer = frame; inner = f })) |
| 103 | + inner; |
| 104 | + (* The matching frame's current slot must be closed. *) |
| 105 | + if opened > frame.bf_floor then |
| 106 | + raise_error ~loc (ReuseBeforeClosing { bullet = bul; frame }); |
| 107 | + { frame with bf_loc = loc } :: outer |
| 108 | + |
| 109 | +(* -------------------------------------------------------------------- *) |
| 110 | +(* After a phrase has run, pop frames whose subproof has fully |
| 111 | + closed. Cascades through nested last-sibling frames; this is what |
| 112 | + lets the last sibling at any level be addressed by an unbulleted |
| 113 | + phrase. *) |
| 114 | +let close_phrase (juc : EcCoreGoal.proof) (stack : stack) : stack = |
| 115 | + let opened = n_open juc in |
| 116 | + let rec pop = function |
| 117 | + | f :: rest when opened <= f.bf_floor -> pop rest |
| 118 | + | s -> s |
| 119 | + in |
| 120 | + pop stack |
| 121 | + |
| 122 | +(* -------------------------------------------------------------------- *) |
| 123 | +let pp_exn fmt = function |
| 124 | + | BulletError (_, err) -> pp_error fmt err |
| 125 | + | exn -> raise exn |
| 126 | + |
| 127 | +let () = EcPException.register pp_exn |
0 commit comments