aboutsummaryrefslogtreecommitdiffhomepage
path: root/stm/proofBlockDelimiter.ml
blob: b8af2bcd56c0dabbbd1358a666df5139fda21167 (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
(************************************************************************)
(*         *   The Coq Proof Assistant / The Coq Development Team       *)
(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
(* <O___,, *       (see CREDITS file for the list of authors)           *)
(*   \VV/  **************************************************************)
(*    //   *    This file is distributed under the terms of the         *)
(*         *     GNU Lesser General Public License Version 2.1          *)
(*         *     (see LICENSE file for the text of the license)         *)
(************************************************************************)

open Stm

module Util : sig

val simple_goal : Evd.evar_map -> Goal.goal -> Goal.goal list -> bool
val is_focused_goal_simple : doc:Stm.doc -> Stateid.t -> [ `Simple of Goal.goal list | `Not ]

type 'a until = [ `Stop | `Found of static_block_declaration | `Cont of 'a ]

val crawl :
  document_view -> ?init:document_node option ->
  ('a -> document_node -> 'a until) -> 'a ->
    static_block_declaration option

val unit_val : Stm.DynBlockData.t
val of_bullet_val : Proof_bullet.t -> Stm.DynBlockData.t
val to_bullet_val : Stm.DynBlockData.t -> Proof_bullet.t
val of_vernac_control_val : Vernacexpr.vernac_control -> Stm.DynBlockData.t
val to_vernac_control_val : Stm.DynBlockData.t -> Vernacexpr.vernac_control

end = struct

let unit_tag = DynBlockData.create "unit"
let unit_val = DynBlockData.Easy.inj () unit_tag

let of_bullet_val, to_bullet_val = DynBlockData.Easy.make_dyn "bullet"
let of_vernac_control_val, to_vernac_control_val = DynBlockData.Easy.make_dyn "vernac_control"

let simple_goal sigma g gs =
  let open Evar in
  let open Evd in
  let open Evarutil in
  let evi = Evd.find sigma g in
  Set.is_empty (evars_of_term (EConstr.Unsafe.to_constr evi.evar_concl)) &&
  Set.is_empty (evars_of_filtered_evar_info (nf_evar_info sigma evi)) &&
  not (List.exists (Proofview.depends_on sigma g) gs)

let is_focused_goal_simple ~doc id =
  match state_of_id ~doc id with
  | `Expired | `Error _ | `Valid None -> `Not
  | `Valid (Some { Vernacstate.proof }) ->
       let proof = Proof_global.proof_of_state proof in
       let focused, r1, r2, r3, sigma = Proof.proof proof in
       let rest = List.(flatten (map (fun (x,y) -> x @ y) r1)) @ r2 @ r3 in
       if List.for_all (fun x -> simple_goal sigma x rest) focused
       then `Simple focused
       else `Not

type 'a until = [ `Stop | `Found of static_block_declaration | `Cont of 'a ]

let crawl { entry_point; prev_node } ?(init=Some entry_point) f acc =
  let rec crawl node acc =
    match node with
    | None -> None
    | Some node ->
        match f acc node with
        | `Stop -> None
        | `Found x -> Some x
        | `Cont acc -> crawl (prev_node node) acc in
  crawl init acc

end

include Util

(* ****************** - foo - bar - baz *********************************** *)

let static_bullet ({ entry_point; prev_node } as view) =
  assert (not (Vernacprop.has_Fail entry_point.ast));
  match Vernacprop.under_control entry_point.ast with
  | Vernacexpr.VernacBullet b ->
      let base = entry_point.indentation in
      let last_tac = prev_node entry_point in
      crawl view ~init:last_tac (fun prev node ->
        if node.indentation < base then `Stop else
        if node.indentation > base then `Cont node else
        if Vernacprop.has_Fail node.ast then `Stop
        else match Vernacprop.under_control node.ast with
        | Vernacexpr.VernacBullet b' when b = b' ->
          `Found { block_stop = entry_point.id; block_start = prev.id;
                   dynamic_switch = node.id; carry_on_data = of_bullet_val b }
        | _ -> `Stop) entry_point
  | _ -> assert false

let dynamic_bullet doc { dynamic_switch = id; carry_on_data = b } =
  match is_focused_goal_simple ~doc id with
  | `Simple focused ->
      `ValidBlock {
         base_state = id;
         goals_to_admit = focused;
         recovery_command = Some (Vernacexpr.VernacExpr([], Vernacexpr.VernacBullet (to_bullet_val b)))
      }
  | `Not -> `Leaks

let () = register_proof_block_delimiter
  "bullet" static_bullet dynamic_bullet

(* ******************** { block } ***************************************** *)
  
let static_curly_brace ({ entry_point; prev_node } as view) =
  assert(Vernacprop.under_control entry_point.ast = Vernacexpr.VernacEndSubproof);
  crawl view (fun (nesting,prev) node ->
    if Vernacprop.has_Fail node.ast then `Cont (nesting,node)
    else match Vernacprop.under_control node.ast with
    | Vernacexpr.VernacSubproof _ when nesting = 0 ->
      `Found { block_stop = entry_point.id; block_start = prev.id;
               dynamic_switch = node.id; carry_on_data = unit_val }
    | Vernacexpr.VernacSubproof _ ->
      `Cont (nesting - 1,node)
    | Vernacexpr.VernacEndSubproof ->
      `Cont (nesting + 1,node)
    | _ -> `Cont (nesting,node)) (-1, entry_point)

let dynamic_curly_brace doc { dynamic_switch = id } =
  match is_focused_goal_simple ~doc id with
  | `Simple focused ->
      `ValidBlock {
         base_state = id;
         goals_to_admit = focused;
         recovery_command = Some (Vernacexpr.VernacExpr ([], Vernacexpr.VernacEndSubproof))
      }
  | `Not -> `Leaks

let () = register_proof_block_delimiter
  "curly" static_curly_brace dynamic_curly_brace

(* ***************** par: ************************************************* *)

let static_par { entry_point; prev_node } =
  match prev_node entry_point with
  | None -> None
  | Some { id = pid } ->
      Some { block_stop = entry_point.id; block_start = pid;
             dynamic_switch = pid; carry_on_data = unit_val }

let dynamic_par doc { dynamic_switch = id } =
  match is_focused_goal_simple ~doc id with
  | `Simple focused ->
      `ValidBlock {
         base_state = id;
         goals_to_admit = focused;
         recovery_command = None;
      }
  | `Not -> `Leaks

let () = register_proof_block_delimiter "par" static_par dynamic_par

(* ***************** simple indentation *********************************** *)

let static_indent ({ entry_point; prev_node } as view) =
   Printf.eprintf "@%d\n" (Stateid.to_int entry_point.id);
   match prev_node entry_point with
   | None -> None
   | Some last_tac ->
      if last_tac.indentation <= entry_point.indentation then None
      else
        crawl view ~init:(Some last_tac) (fun prev node ->
        if node.indentation >= last_tac.indentation then `Cont node
        else 
          `Found { block_stop = entry_point.id; block_start = node.id;
                   dynamic_switch = node.id;
                   carry_on_data = of_vernac_control_val entry_point.ast }
        ) last_tac

let dynamic_indent doc { dynamic_switch = id; carry_on_data = e } =
  Printf.eprintf "%s\n" (Stateid.to_string id);
  match is_focused_goal_simple ~doc id with
  | `Simple [] -> `Leaks
  | `Simple focused ->
      let but_last = List.tl (List.rev focused) in 
      `ValidBlock {
         base_state = id;
         goals_to_admit = but_last;
         recovery_command = Some (to_vernac_control_val e);
      }
  | `Not -> `Leaks

let () = register_proof_block_delimiter "indent" static_indent dynamic_indent