Skip to content

Commit ccc5f15

Browse files
rtetleyrtetley
authored
Merge pull request rocq-prover#1059 from coq/sections-in-outline
feat: adding sections and modules in outlines
2 parents 54562da + e56b54f commit ccc5f15

File tree

3 files changed

+84
-28
lines changed

3 files changed

+84
-28
lines changed

‎language-server/dm/document.ml‎

Lines changed: 20 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -23,9 +23,12 @@ module LM = Map.Make (Int)
2323
module SM = Map.Make (Stateid)
2424

2525
type proof_block_type =
26-
| TheoremKind of Decls.theorem_kind
27-
| DefinitionType of Decls.definition_object_kind
28-
| InductiveType of Vernacexpr.inductive_kind
26+
| TheoremKind
27+
| DefinitionType
28+
| InductiveType
29+
| BeginSection
30+
| BeginModule
31+
| End
2932
| Other
3033

3134
type proof_step = {
@@ -188,10 +191,10 @@ let record_outline document id (ast : Synterp.vernac_control_entry) classif (out
188191
| VernacSynterp _ -> None
189192
| VernacSynPure pure ->
190193
match pure with
191-
| Vernacexpr.VernacStartTheoremProof (kind, _) -> Some (TheoremKind kind)
192-
| Vernacexpr.VernacDefinition ((_, def), _, _) -> Some (DefinitionType def)
193-
| Vernacexpr.VernacFixpoint (_, _) -> Some (DefinitionType Decls.Fixpoint)
194-
| Vernacexpr.VernacCoFixpoint (_, _) -> Some (DefinitionType Decls.CoFixpoint)
194+
| Vernacexpr.VernacStartTheoremProof _ -> Some TheoremKind
195+
| Vernacexpr.VernacDefinition _ -> Some DefinitionType
196+
| Vernacexpr.VernacFixpoint _ -> Some DefinitionType
197+
| Vernacexpr.VernacCoFixpoint _ -> Some DefinitionType
195198
| _ -> None
196199
in
197200
let name = match names with
@@ -210,14 +213,19 @@ let record_outline document id (ast : Synterp.vernac_control_entry) classif (out
210213
let vernac_gen_expr = ast.v.expr in
211214
let type_, statement = match vernac_gen_expr with
212215
| VernacSynterp (Synterp.EVernacExtend _) when names <> [] -> Some Other, "external"
216+
| VernacSynterp (Synterp.EVernacBeginSection _) -> log (fun () -> Format.sprintf "BEGIN SECTION %s" (string_of_id document id)); Some BeginSection, ""
217+
| VernacSynterp (Synterp.EVernacDeclareModuleType _) -> log (fun () -> Format.sprintf "BEGIN MODULE %s" (string_of_id document id)); Some BeginModule, ""
218+
| VernacSynterp (Synterp.EVernacDefineModule _) -> log (fun () -> Format.sprintf "BEGIN MODULE %s" (string_of_id document id)); Some BeginModule, ""
219+
| VernacSynterp (Synterp.EVernacDeclareModule _) -> log (fun () -> Format.sprintf "BEGIN MODULE %s" (string_of_id document id)); Some BeginModule, ""
220+
| VernacSynterp (Synterp.EVernacEndSegment _) -> log (fun () -> Format.sprintf "END SEGMENT"); Some End, ""
213221
| VernacSynterp _ -> None, ""
214222
| VernacSynPure pure ->
215223
match pure with
216-
| Vernacexpr.VernacStartTheoremProof (kind, _) -> Some (TheoremKind kind), string_of_id document id
217-
| Vernacexpr.VernacDefinition ((_, def), _, _) -> Some (DefinitionType def), string_of_id document id
218-
| Vernacexpr.VernacInductive (kind, _) -> Some (InductiveType kind), string_of_id document id
219-
| Vernacexpr.VernacFixpoint (_, _) -> Some (DefinitionType Decls.Fixpoint), string_of_id document id
220-
| Vernacexpr.VernacCoFixpoint (_, _) -> Some (DefinitionType Decls.CoFixpoint), string_of_id document id
224+
| Vernacexpr.VernacStartTheoremProof _ -> Some TheoremKind, string_of_id document id
225+
| Vernacexpr.VernacDefinition _ -> Some DefinitionType, string_of_id document id
226+
| Vernacexpr.VernacInductive _ -> Some InductiveType, string_of_id document id
227+
| Vernacexpr.VernacFixpoint _ -> Some DefinitionType, string_of_id document id
228+
| Vernacexpr.VernacCoFixpoint _ -> Some DefinitionType, string_of_id document id
221229
| _ -> None, ""
222230
in
223231
let name = match names with

‎language-server/dm/document.mli‎

Lines changed: 6 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -23,9 +23,12 @@ open Lsp.Types
2323
type document
2424

2525
type proof_block_type =
26-
| TheoremKind of Decls.theorem_kind
27-
| DefinitionType of Decls.definition_object_kind
28-
| InductiveType of Vernacexpr.inductive_kind
26+
| TheoremKind
27+
| DefinitionType
28+
| InductiveType
29+
| BeginSection
30+
| BeginModule
31+
| End
2932
| Other
3033

3134
type proof_step = {

‎language-server/dm/documentManager.ml‎

Lines changed: 58 additions & 13 deletions
Original file line numberDiff line numberDiff line change
@@ -336,7 +336,7 @@ let get_document_proofs st =
336336
let outline = Document.outline st.document in
337337
let is_theorem Document.{ type_ } =
338338
match type_ with
339-
| TheoremKind _ -> true
339+
| TheoremKind -> true
340340
| _ -> false
341341
in
342342
let mk_proof_block Document.{statement; proof; range } =
@@ -351,19 +351,64 @@ let get_document_proofs st =
351351
let proofs, _ = List.partition is_theorem outline in
352352
List.map mk_proof_block proofs
353353

354-
let get_document_symbols st =
355-
let outline = Document.outline st.document in
356-
let to_document_symbol elem =
357-
let Document.{name; statement; range; type_} = elem in
358-
let kind = begin match type_ with
359-
| TheoremKind _ -> SymbolKind.Function
360-
| DefinitionType _ -> SymbolKind.Variable
361-
| InductiveType _ -> SymbolKind.Struct
362-
| Other -> SymbolKind.Null
363-
end in
364-
DocumentSymbol.{name; detail=(Some statement); kind; range; selectionRange=range; children=None; deprecated=None; tags=None;}
354+
let to_document_symbol elem =
355+
let Document.{name; statement; range; type_} = elem in
356+
let kind = begin match type_ with
357+
| TheoremKind -> SymbolKind.Function
358+
| DefinitionType -> SymbolKind.Variable
359+
| InductiveType -> SymbolKind.Struct
360+
| Other -> SymbolKind.Null
361+
| BeginSection | BeginModule -> SymbolKind.Class
362+
| End -> SymbolKind.Null
363+
end in
364+
DocumentSymbol.{name; detail=(Some statement); kind; range; selectionRange=range; children=None; deprecated=None; tags=None;}
365+
366+
let rec get_document_symbols outline (sec_or_m: DocumentSymbol.t list) symbols =
367+
let add_child (s_father: DocumentSymbol.t) s_child =
368+
let children = match s_father.children with
369+
| None -> Some [s_child]
370+
| Some l -> Some (l @ [s_child])
371+
in
372+
{s_father with children}
373+
in
374+
let record_in_outline outline symbol sec_or_m =
375+
match sec_or_m with
376+
| [] ->
377+
let symbols = symbols @ [symbol] in
378+
get_document_symbols outline sec_or_m symbols
379+
| s :: l ->
380+
let s = add_child s symbol in
381+
get_document_symbols outline (s::l) symbols
365382
in
366-
List.map to_document_symbol outline
383+
match outline with
384+
| [] -> symbols
385+
| e :: l ->
386+
let Document.{type_} = e in
387+
match type_ with
388+
| TheoremKind | DefinitionType | InductiveType | Other ->
389+
let symbol = to_document_symbol e in
390+
record_in_outline l symbol sec_or_m
391+
| BeginSection ->
392+
let symbol = to_document_symbol e in
393+
get_document_symbols l (symbol :: sec_or_m) symbols
394+
| BeginModule ->
395+
let symbol = to_document_symbol e in
396+
get_document_symbols l (symbol :: sec_or_m) symbols
397+
| End ->
398+
match sec_or_m with
399+
| [] -> log(fun () -> "Trying to end a module or section with no begin"); get_document_symbols l [] symbols
400+
| symbol :: s_l ->
401+
match s_l with
402+
| [] ->
403+
get_document_symbols l s_l (symbols @ [symbol])
404+
| s_parent :: s_l ->
405+
let s = add_child s_parent symbol in
406+
get_document_symbols l (s :: s_l) symbols
407+
408+
409+
let get_document_symbols st =
410+
let outline = List.rev @@ Document.outline st.document in
411+
get_document_symbols outline [] []
367412

368413
let interpret_to st id check_mode =
369414
let observe_id = (Id id) in

0 commit comments

Comments
 (0)