Source file doc.ml
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
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
863
864
865
866
867
868
869
870
871
872
873
874
875
876
877
878
879
880
881
882
883
884
885
886
887
888
889
890
891
892
893
894
895
896
897
898
899
900
901
902
903
904
905
906
907
908
909
910
911
912
913
914
915
916
917
918
919
920
921
922
923
924
925
926
927
928
929
930
931
932
933
934
935
936
937
938
939
940
941
942
943
944
945
946
947
948
949
950
951
952
953
954
955
956
957
958
959
960
961
962
963
964
965
966
967
968
969
970
971
972
973
974
975
976
977
978
979
980
981
982
983
984
985
986
987
988
989
990
991
992
993
994
995
996
997
998
999
1000
1001
1002
1003
1004
1005
1006
1007
1008
1009
1010
1011
1012
1013
1014
1015
1016
1017
1018
1019
1020
1021
1022
1023
1024
1025
1026
1027
1028
1029
1030
1031
1032
1033
1034
1035
1036
1037
1038
1039
1040
1041
1042
1043
1044
1045
1046
1047
1048
1049
1050
1051
1052
1053
1054
1055
1056
1057
1058
1059
1060
1061
1062
1063
1064
1065
1066
1067
1068
1069
1070
1071
1072
1073
1074
1075
1076
1077
1078
1079
1080
1081
1082
1083
1084
1085
1086
1087
1088
1089
1090
1091
1092
1093
1094
1095
1096
1097
1098
1099
1100
1101
1102
1103
1104
1105
1106
1107
1108
1109
1110
1111
1112
1113
1114
1115
1116
1117
1118
1119
1120
1121
1122
module Util = struct
let hd_opt l =
match l with
| [] -> None
| h :: _ -> Some h
let rec last l =
match l with
| [] -> None
| [ x ] -> Some x
| _ :: xs -> last xs
let build_span start_loc end_loc =
Loc.
{ start_loc with
line_nb_last = end_loc.line_nb_last
; bol_pos_last = end_loc.bol_pos_last
; ep = end_loc.ep
}
let print_stats () =
(if !Config.v.mem_stats then
let size = Memo.all_size () in
Io.Log.trace "stats" "%d" size);
let stats = Stats.Global.dump () in
Io.Log.trace "cache" "%s" (Stats.Global.to_string stats);
Io.Log.trace "cache" "%s" (Memo.GlobalCacheStats.stats ());
Memo.GlobalCacheStats.reset ();
Stats.reset ()
let safe_sub s pos len =
if pos < 0 || len < 0 || pos > String.length s - len then (
let s = String.sub s 0 (Stdlib.min 20 String.(length s - 1)) in
Io.Log.trace "string_sub" "error for pos: %d len: %d str: %s" pos len s;
None)
else Some (String.sub s pos len)
end
module DDebug = struct
let parsed_sentence ~ast =
let loc = Coq.Ast.loc ast |> Option.get in
let line = loc.Loc.line_nb - 1 in
Io.Log.trace "coq" "parsed sentence: [l: %d] | %a" line Pp.pp_with
(Coq.Ast.print ast)
let resume (last_tok : Lang.Range.t) version =
Io.Log.trace "check" "resuming [v: %d], from: %d l: %d" version
last_tok.end_.offset last_tok.end_.line
end
module Node = struct
module Ast = struct
type t =
{ v : Coq.Ast.t
; ast_info : Lang.Ast.Info.t list option
}
let to_coq { v; _ } = Coq.Ast.to_coq v
end
module Info = struct
type t =
{ parsing_time : float
; stats : Memo.Stats.t option
; global_stats : Stats.Global.t (** Info about cumulative stats *)
}
let make ~parsing_time ?stats ~global_stats () =
{ parsing_time; stats; global_stats }
let pp_cache_hit fmt = function
| None -> Format.fprintf fmt "N/A"
| Some hit -> Format.fprintf fmt "%b" hit
let pp_time fmt = function
| None -> Format.fprintf fmt "N/A"
| Some time -> Format.fprintf fmt "%.3f" time
let pp_words fmt = function
| None -> Format.fprintf fmt "N/A"
| Some memory -> Stats.pp_words fmt memory
let osplit = function
| None -> (None, None, None)
| Some (x, y, z) -> (Some x, Some y, Some z)
let print { parsing_time; stats; global_stats } =
let cptime = Stats.Global.get_f global_stats ~kind:Stats.Kind.Parsing in
let cetime = Stats.Global.get_f global_stats ~kind:Stats.Kind.Exec in
let cache_hit, time, memory =
Option.map
(fun (s : Memo.Stats.t) ->
(s.cache_hit, s.stats.time, s.stats.memory))
stats
|> osplit
in
Format.asprintf
"Cached: %a | P: %.3f / %.2f | E: %a / %.2f | Mem-Diff: %a" pp_cache_hit
cache_hit parsing_time cptime.time pp_time time cetime.time pp_words
memory
end
module Message = struct
type t = Lang.Range.t Coq.Message.t
let feedback_to_message ~lines message =
let f = Coq.Utils.to_range ~lines in
Coq.Message.map ~f message
end
type t =
{ range : Lang.Range.t
; prev : t option
; ast : Ast.t option (** Ast of node *)
; state : Coq.State.t (** (Full) State of node *)
; diags : Lang.Diagnostic.t list
; messages : Message.t list
; info : Info.t
}
let range { range; _ } = range
let ast { ast; _ } = ast
let state { state; _ } = state
let diags { diags; _ } = diags
let messages { messages; _ } = messages
let info { info; _ } = info
end
(** Diagnostics helper module *)
module Diags : sig
val err : Lang.Diagnostic.Severity.t
(** Build simple diagnostic *)
val make :
?data:Lang.Diagnostic.Data.t
-> Lang.Range.t
-> Lang.Diagnostic.Severity.t
-> Pp.t
-> Lang.Diagnostic.t
(** Build advanced diagnostic with AST analysis *)
val error :
err_range:Lang.Range.t
-> quickFix:Lang.Range.t Lang.Qf.t list option
-> msg:Pp.t
-> stm_range:Lang.Range.t
-> ?ast:Node.Ast.t
-> unit
-> Lang.Diagnostic.t
(** [of_messages drange msgs] process feedback messages, and convert some to
diagnostics based on user-config. Default range [drange] is used for
messages that have no range, usually this is set to the full node range. *)
val of_messages :
drange:Lang.Range.t
-> Node.Message.t list
-> Lang.Diagnostic.t list * Node.Message.t list
end = struct
let err = Lang.Diagnostic.Severity.error
let make ?data range severity message =
Lang.Diagnostic.{ range; severity; message; data }
let extra_diagnostics_of_ast quickFix stm_range ast =
let sentenceRange = Some stm_range in
let failedRequire =
match
Option.bind ast (fun (ast : Node.Ast.t) ->
Coq.Ast.Require.extract ast.v)
with
| Some { Coq.Ast.Require.from; mods; _ } ->
let refs = List.map fst mods in
Some [ { Lang.Diagnostic.FailedRequire.prefix = from; refs } ]
| _ -> None
in
Some { Lang.Diagnostic.Data.sentenceRange; failedRequire; quickFix }
let qf stm_range ast =
if !Config.v.send_diags_extra_data then
extra_diagnostics_of_ast qf stm_range ast
else
Option.map
(fun qf ->
let sentenceRange, failedRequire, quickFix = (None, None, Some qf) in
{ Lang.Diagnostic.Data.sentenceRange; failedRequire; quickFix })
qf
let error ~err_range ~quickFix ~msg ~stm_range ?ast () =
let data = extra_diagnostics_of_ast quickFix stm_range ast in
make ?data err_range Lang.Diagnostic.Severity.error msg
let of_feed ~drange (severity, payload) =
let { Coq.Message.Payload.range; quickFix; msg } = payload in
let range = Option.default drange range in
let data =
Option.map
(fun qf ->
let sentenceRange, failedRequire, quickFix = (None, None, Some qf) in
Lang.Diagnostic.Data.{ sentenceRange; failedRequire; quickFix })
quickFix
in
make ?data range severity msg
type partition_kind =
| Left
| Both
| Right
let partition ~f l =
let rec part l r = function
| [] -> (List.rev l, List.rev r)
| x :: xs -> (
match f x with
| Left -> part (x :: l) r xs
| Both -> part (x :: l) (x :: l) xs
| Right -> part l (x :: r) xs)
in
part [] [] l
let of_messages ~drange fbs =
let cutoff =
if !Config.v.show_coq_info_messages then 5
else if !Config.v.show_notices_as_diagnostics then 4
else 3
in
let f (lvl, _) =
if lvl = Lang.Diagnostic.Severity.warning then Both
else if lvl < cutoff then Left
else Right
in
let diags, messages = partition ~f fbs in
(List.map (of_feed ~drange) diags, messages)
end
module Completion = struct
type t =
| Yes of Lang.Range.t (** Location of the last token in the document *)
| Stopped of Lang.Range.t (** Location of the last valid token *)
| Failed of Lang.Range.t (** Critical failure, like an anomaly *)
let range = function
| Yes range | Stopped range | Failed range -> range
let to_string = function
| Yes _ -> "fully checked"
| Stopped _ -> "stopped"
| Failed _ -> "failed"
let is_completed = function
| Yes _ | Failed _ -> true
| _ -> false
end
(** Enviroment external to the document, this includes for now the [init] Coq
state and the [workspace], which are used to build the first state of the
document, usually by importing the prelude and other libs implicitly. *)
module Env = struct
type t =
{ init : Coq.State.t
; workspace : Coq.Workspace.t
; files : Coq.Files.t
}
let make ~init ~workspace ~files = { init; workspace; files }
let inject_requires ~ { init; workspace; files } =
let workspace = Coq.Workspace.inject_requires ~extra_requires workspace in
{ init; workspace; files }
end
(** A Flèche document is basically a [node list], which is a crude form of a
meta-data map [Range.t -> data], where for now [data] is the contents of
[Node.t]. *)
type t =
{ uri : Lang.LUri.File.t (** [uri] of the document *)
; version : int (** [version] of the document *)
; contents : Contents.t (** [contents] of the document *)
; nodes : Node.t list (** List of document nodes *)
; completed : Completion.t
(** Status of the document, usually either completed, suspended, or
waiting for some IO / external event *)
; toc : Node.t CString.Map.t (** table of contents *)
; env : Env.t (** External document enviroment *)
; root : Coq.State.t
(** [root] contains the first state document state, obtained by applying
a workspace to Coq's initial state *)
; diags_dirty : bool (** internal field *)
}
let asts doc = List.filter_map Node.ast doc.nodes
let diags doc = List.concat_map Node.diags doc.nodes
let lines doc = doc.contents.lines
let rec add_toc_info node toc { Lang.Ast.Info.name; children; _ } =
let toc =
match name.v with
| None -> toc
| Some id -> CString.Map.add id node toc
in
Option.cata (List.fold_left (add_toc_info node) toc) toc children
let update_toc_info toc ast_info node =
List.fold_left (add_toc_info node) toc ast_info
let update_toc_node toc node =
match Node.ast node with
| None -> toc
| Some { Node.Ast.ast_info = None; _ } -> toc
| Some { Node.Ast.ast_info = Some ast_info; _ } ->
update_toc_info toc ast_info node
let rebuild_toc nodes = List.fold_left update_toc_node CString.Map.empty nodes
let init_fname ~uri =
let file = Lang.LUri.File.to_string_file uri in
Loc.InFile { dirpath = None; file }
let init_loc ~uri = Loc.initial (init_fname ~uri)
let drange ~lines =
let open Lang in
let llen = if Array.length lines > 0 then String.length lines.(0) else 1 in
let start = Point.{ line = 0; character = 0; offset = 0 } in
let end_ = Point.{ line = 0; character = llen; offset = llen } in
Range.{ start; end_ }
let process_init_feedback ~lines ~stats ~global_stats state feedback =
let messages = List.map (Node.Message.feedback_to_message ~lines) feedback in
if not (CList.is_empty messages) then
let drange = drange ~lines in
let diags, messages = Diags.of_messages ~drange messages in
let parsing_time = 0.0 in
let info = Node.Info.make ~parsing_time ?stats ~global_stats () in
let range = drange in
let prev = None in
[ { Node.range; prev; ast = None; state; diags; messages; info } ]
else []
let mk_doc ~token ~env ~uri =
Memo.Init.evalS ~token (env.Env.init, env.workspace, uri)
let empty_doc ~uri ~contents ~version ~env ~root ~nodes ~completed =
let lines = contents.Contents.lines in
let init_loc = init_loc ~uri in
let init_range = Coq.Utils.to_range ~lines init_loc in
let toc = CString.Map.empty in
let diags_dirty = not (CList.is_empty nodes) in
let completed = completed init_range in
{ uri; contents; toc; version; env; root; nodes; diags_dirty; completed }
let error_doc ~range ~message ~uri ~contents ~version ~env =
let payload = Coq.Message.Payload.make ?range (Pp.str message) in
let feedback = [ (Diags.err, payload) ] in
let root = env.Env.init in
let nodes = [] in
let completed range = Completion.Failed range in
(empty_doc ~uri ~version ~contents ~env ~root ~nodes ~completed, feedback)
let conv_error_doc ~raw ~uri ~version ~env ~root err =
let contents = Contents.make_raw ~raw in
let lines = contents.lines in
let err =
let msg = Pp.(str "Error in document conversion: " ++ str err) in
(Diags.err, Coq.Message.Payload.make msg)
in
let stats = None in
let global_stats = Stats.Global.dump () in
let nodes = process_init_feedback ~lines ~stats ~global_stats root [ err ] in
let completed range = Completion.Failed range in
empty_doc ~uri ~version ~env ~root ~nodes ~completed ~contents
let create ~token ~env ~uri ~version ~contents =
let () = Stats.reset () in
let root, stats = mk_doc ~token ~env ~uri in
( Coq.Protect.E.map root ~f:(fun root ->
let nodes = [] in
let completed range = Completion.Stopped range in
empty_doc ~uri ~contents ~version ~env ~root ~nodes ~completed)
, stats )
(** Try to create a doc, if Coq execution fails, create a failed doc with the
corresponding errors; for now we refine the contents step as to better setup
the initial document. *)
let handle_doc_creation_exec ~token ~env ~uri ~version ~contents =
let { Coq.Protect.E.r; feedback }, stats =
create ~token ~env ~uri ~version ~contents
in
let doc, =
match r with
| Interrupted ->
let message = "Document Creation Interrupted!" in
let range = None in
error_doc ~range ~message ~uri ~version ~contents ~env
| Completed (Error (User { range; msg = err_msg; quickFix = _ }))
| Completed (Error (Anomaly { range; msg = err_msg; quickFix = _ })) ->
let message =
Format.asprintf "Doc.create, internal error: @[%a@]" Pp.pp_with err_msg
in
error_doc ~range ~message ~uri ~version ~contents ~env
| Completed (Ok doc) -> (doc, [])
in
let state = doc.root in
let stats = Some stats in
let global_stats = Stats.Global.dump () in
let nodes =
let lines = contents.Contents.lines in
process_init_feedback ~lines ~stats ~global_stats state
(feedback @ extra_feedback)
@ doc.nodes
in
let diags_dirty = not (CList.is_empty nodes) in
{ doc with nodes; diags_dirty }
let handle_contents_creation ~env ~uri ~version ~raw f =
match Contents.make ~uri ~raw with
| Contents.R.Error err ->
let root = env.Env.init in
conv_error_doc ~raw ~uri ~version ~env ~root err
| Contents.R.Ok contents -> f ~env ~uri ~version ~contents
let create ~token ~env ~uri ~version ~raw =
handle_contents_creation ~env ~uri ~version ~raw
(handle_doc_creation_exec ~token)
let recreate ~token ~doc ~version ~contents =
let env, uri = (doc.env, doc.uri) in
handle_doc_creation_exec ~token ~env ~uri ~version ~contents
let recover_up_to_offset ~init_range doc offset =
Io.Log.trace "prefix" "common prefix offset found at %d" offset;
let rec find acc_nodes acc_range nodes =
match nodes with
| [] -> (List.rev acc_nodes, acc_range)
| n :: ns ->
if Debug.scan then
Io.Log.trace "scan" "consider node at %a" Lang.Range.pp n.Node.range;
if n.range.end_.offset >= offset then (List.rev acc_nodes, acc_range)
else find (n :: acc_nodes) n.range ns
in
find [] init_range doc.nodes
let compute_common_prefix ~init_range ~contents (prev : t) =
let s1 = prev.contents.raw in
let l1 = prev.contents.last.offset in
let s2 = contents.Contents.raw in
let l2 = contents.last.offset in
let rec match_or_stop i =
if i = l1 || i = l2 then i
else if Char.equal s1.[i] s2.[i] then match_or_stop (i + 1)
else i
in
let common_idx = match_or_stop 0 in
let nodes, range = recover_up_to_offset ~init_range prev common_idx in
let toc = rebuild_toc nodes in
Io.Log.trace "prefix" "resuming from %a" Lang.Range.pp range;
let completed = Completion.Stopped range in
(nodes, completed, toc)
let bump_version ~init_range ~version ~contents doc =
let nodes, completed, toc = compute_common_prefix ~init_range ~contents doc in
let uri = doc.uri in
let root = doc.root in
let env = doc.env in
{ uri
; version
; root
; nodes
; contents
; toc
; diags_dirty = true
; completed
; env
}
let bump_version ~token ~version ~(contents : Contents.t) doc =
let init_loc = init_loc ~uri:doc.uri in
let init_range = Coq.Utils.to_range ~lines:contents.lines init_loc in
match doc.completed with
| Failed _ ->
recreate ~token ~doc ~version ~contents
| Stopped _ | Yes _ -> bump_version ~init_range ~version ~contents doc
let bump_version ~token ~version ~raw doc =
let uri = doc.uri in
match Contents.make ~uri ~raw with
| Contents.R.Error e ->
conv_error_doc ~raw ~uri ~version ~env:doc.env ~root:doc.root e
| Contents.R.Ok contents -> bump_version ~token ~version ~contents doc
let add_node ~node doc =
let diags_dirty = if node.Node.diags <> [] then true else doc.diags_dirty in
let toc = update_toc_node doc.toc node in
{ doc with nodes = node :: doc.nodes; toc; diags_dirty }
let send_eager_diagnostics ~io ~uri ~version ~doc =
if doc.diags_dirty && !Config.v.eager_diagnostics then (
let diags = diags doc in
Io.Report.diagnostics ~io ~uri ~version diags;
{ doc with diags_dirty = false })
else doc
let set_completion ~completed doc = { doc with completed }
let compute_progress end_ (last_done : Lang.Range.t) =
let start = last_done.end_ in
let range = Lang.Range.{ start; end_ } in
{ Progress.Info.range; kind = 1 }
let report_progress ~io ~doc (last_tok : Lang.Range.t) =
let progress = compute_progress doc.contents.last last_tok in
Io.Report.fileProgress ~io ~uri:doc.uri ~version:doc.version [ progress ]
let parse_stm ~token ~st ps =
let f ps = Coq.Parsing.parse ~token ~st ps in
Stats.record ~kind:Stats.Kind.Parsing ~f ps
module Recovery_context = struct
type t =
{ contents : Contents.t
(** Contents of the document (for syntax-based recovery) *)
; last_tok : Lang.Range.t (** Position of the last token parsed *)
; nodes : Node.t list
(** All nodes of the document (to be replaced by the structural
solution *)
; ast : Coq.Ast.t option
(** Ast of the sentence that failed, if available *)
}
let make ~contents ~last_tok ~nodes ?ast () =
{ contents; last_tok; nodes; ast }
end
module Recovery : sig
(** [find_proof_start nodes] returns [Some (node, pnode)] where [node] is the
node that contains the start of the proof, and [pnode] is the previous
node, if exists. [nodes] is the list of document nodes, in _reverse
order_. *)
val find_proof_start : Node.t list -> (Node.t * Node.t option) option
val handle :
token:Coq.Limits.Token.t
-> context:Recovery_context.t
-> st:Coq.State.t
-> Coq.State.t
end = struct
let rec find_proof_start nodes =
match nodes with
| [] -> None
| { Node.ast = None; _ } :: ns -> find_proof_start ns
| ({ ast = Some ast; _ } as n) :: ns -> (
match (Node.Ast.to_coq ast).CAst.v.Vernacexpr.expr with
| Vernacexpr.VernacSynPure (VernacStartTheoremProof _)
| VernacSynPure (VernacDefinition (_, _, ProveBody _)) ->
Some (n, Util.hd_opt ns)
| _ -> find_proof_start ns)
let recovery_for_failed_qed ~token ~default nodes =
match find_proof_start nodes with
| None -> Coq.Protect.E.ok (default, None)
| Some ({ range; state; _ }, prev) -> (
if !Config.v.admit_on_bad_qed then
Memo.Admit.eval ~token state
|> Coq.Protect.E.map ~f:(fun state -> (state, Some range))
else
match prev with
| None -> Coq.Protect.E.ok (default, None)
| Some { state; range; _ } -> Coq.Protect.E.ok (state, Some range))
let log_qed_recovery v =
Coq.Protect.E.map ~f:(fun (st, range) ->
let loc_msg = Option.cata Lang.Range.to_string "no loc" range in
Io.Log.trace "recovery" "success %s %s" loc_msg
(Memo.Interp.input_info (st, v));
st)
let Lang.Range.{ end_; _ } { Contents.lines; _ } size =
let Lang.Point.{ line; character; _ } = end_ in
let line = Array.get lines line in
if character > size && String.length line > size then
let coff = character - (size + 1) in
Some (String.init size (fun idx -> line.[idx + coff]))
else None
let lex_recovery_heuristic ~token last_tok contents nodes st =
let et = extract_token last_tok contents in
match (et 3, et 7, et 8) with
| Some ("Qed" as txt), _, _
| _, Some ("Defined" as txt), _
| _, _, Some ("Admitted" as txt) ->
Io.Log.trace "lex recovery" "%s detected" txt;
recovery_for_failed_qed ~token ~default:st nodes
|> Coq.Protect.E.map ~f:fst
| _, _, _ -> Coq.Protect.E.ok st
let ast_recovery_heuristic ~token last_tok contents nodes st v =
match (Coq.Ast.to_coq v).CAst.v.Vernacexpr.expr with
| Vernacexpr.VernacSynPure (VernacEndProof _) ->
Io.Log.trace "recovery" "qed";
recovery_for_failed_qed ~token ~default:st nodes |> log_qed_recovery v
| Vernacexpr.VernacSynPure (VernacBullet _ | Vernacexpr.VernacEndSubproof)
->
Io.Log.trace "recovery" "bullet";
Coq.State.admit_goal ~token ~st
|> Coq.Protect.E.bind ~f:(fun st ->
let intern = Vernacinterp.fs_intern in
Coq.Interp.interp ~token ~intern ~st v)
| _ ->
lex_recovery_heuristic ~token last_tok contents nodes st
let handle ~token ~context ~st =
let { Recovery_context.contents; last_tok; nodes; ast } = context in
let { Coq.Protect.E.r; feedback } =
match ast with
| None -> lex_recovery_heuristic ~token last_tok contents nodes st
| Some ast -> ast_recovery_heuristic ~token last_tok contents nodes st ast
in
Io.Log.feedback "Recovery_context.handle" feedback;
match r with
| Interrupted -> st
| Completed (Ok st) -> st
| Completed (Error _) -> st
end
let interp_and_info ~token ~st ~files ast =
match Coq.Ast.Require.extract ast with
| None -> Memo.Interp.evalS ~token (st, ast)
| Some ast -> Memo.Require.evalS ~token (st, files, ast)
let search_node ~command ~doc ~st =
let nstats (node : Node.t option) =
Option.cata
(fun (node : Node.t) -> Option.default Memo.Stats.zero node.info.stats)
Memo.Stats.zero node
in
let back_overflow num =
let ll = List.length doc.nodes in
Pp.(
str "not enough nodes: [" ++ int num ++ str " > " ++ int ll
++ str "] available document nodes")
in
match command with
| Coq.Ast.Meta.Command.Back num -> (
match Base.List.nth doc.nodes num with
| None ->
let message = back_overflow num in
(Coq.Protect.E.error message, nstats None)
| Some node -> (Coq.Protect.E.ok node.state, nstats (Some node)))
| Restart -> (
match Recovery.find_proof_start doc.nodes with
| None ->
(Coq.Protect.E.error Pp.(str "no proof to restart"), Memo.Stats.zero)
| Some (node, _) -> (Coq.Protect.E.ok node.state, nstats None))
| ResetName id -> (
let toc = doc.toc in
let id = Names.Id.to_string id.v in
match CString.Map.find_opt id toc with
| None ->
( Coq.Protect.E.error Pp.(str "identifier " ++ str id ++ str " not found")
, Memo.Stats.zero )
| Some node ->
let node = Option.default node node.prev in
(Coq.Protect.E.ok node.state, nstats (Some node)))
| ResetInitial -> (Coq.Protect.E.ok doc.root, nstats None)
| AbortAll ->
let st = Coq.State.drop_all_proofs ~st in
(Coq.Protect.E.ok st, nstats None)
let interp_and_info ~token ~st ~files ~doc ast =
match Coq.Ast.Meta.extract ast with
| None -> interp_and_info ~token ~st ~files ast
| Some { command; loc = _; attrs = _; control = _ } ->
search_node ~command ~doc ~st
let interp_and_info ~token ~parsing_time ~st ~files ~doc ast =
let res, stats = interp_and_info ~token ~st ~files ~doc ast in
let global_stats = Stats.Global.dump () in
let info = Node.Info.make ~parsing_time ~stats ~global_stats () in
(res, info)
type parse_action =
| EOF of Completion.t
| Skip of
Lang.Range.t
* Lang.Range.t
| Process of Coq.Ast.t
let parse_action ~token ~lines ~st last_tok doc_handle =
let start_loc = Coq.Parsing.Parsable.loc doc_handle |> CLexer.after in
let parse_res, stats = parse_stm ~token ~st doc_handle in
let f = Coq.Utils.to_range ~lines in
let { Coq.Protect.E.r; feedback } = Coq.Protect.E.map_loc ~f parse_res in
let { Stats.time; memory = _ } = stats in
match r with
| Coq.Protect.R.Interrupted -> (EOF (Stopped last_tok), [], feedback, time)
| Coq.Protect.R.Completed res -> (
match res with
| Ok None ->
let last_tok = Coq.Parsing.Parsable.loc doc_handle in
let last_tok = Coq.Utils.to_range ~lines last_tok in
(EOF (Yes last_tok), [], feedback, time)
| Ok (Some ast) ->
let () = if Debug.parsing then DDebug.parsed_sentence ~ast in
(Process ast, [], feedback, time)
| Error (Anomaly { range = _; quickFix; msg })
| Error (User { range = None; quickFix; msg }) ->
let err_range = last_tok in
let parse_diags =
[ Diags.error ~err_range ~quickFix ~msg ~stm_range:err_range () ]
in
(EOF (Failed last_tok), parse_diags, feedback, time)
| Error (User { range = Some err_range; quickFix; msg }) ->
Coq.Parsing.discard_to_dot doc_handle;
let last_tok = Coq.Parsing.Parsable.loc doc_handle in
let last_tok_range = Coq.Utils.to_range ~lines last_tok in
let span_loc = Util.build_span start_loc last_tok in
let span_range = Coq.Utils.to_range ~lines span_loc in
let parse_diags =
[ Diags.error ~err_range ~quickFix ~msg ~stm_range:span_range () ]
in
(Skip (span_range, last_tok_range), parse_diags, feedback, time))
type document_action =
| Stop of Completion.t * Node.t
| Continue of
{ state : Coq.State.t
; last_tok : Lang.Range.t
; node : Node.t
}
| Interrupted of Lang.Range.t
let unparseable_node ~range ~prev ~parsing_diags ~parsing_feedback ~state
~parsing_time =
let fb_diags, messages = Diags.of_messages ~drange:range parsing_feedback in
let diags = fb_diags @ parsing_diags in
let stats = None in
let global_stats = Stats.Global.dump () in
let info = Node.Info.make ~parsing_time ?stats ~global_stats () in
{ Node.range; prev; ast = None; diags; messages; state; info }
let assemble_diags ~range ~parsing_diags ~parsing_feedback ~diags ~feedback =
let parsing_fb_diags, parsing_messages =
Diags.of_messages ~drange:range parsing_feedback
in
let fb_diags, fb_messages = Diags.of_messages ~drange:range feedback in
let diags = parsing_diags @ parsing_fb_diags @ fb_diags @ diags in
let messages = parsing_messages @ fb_messages in
(diags, messages)
let parsed_node ~range ~prev ~ast ~state ~parsing_diags ~parsing_feedback ~diags
~feedback ~info =
let diags, messages =
assemble_diags ~range ~parsing_diags ~parsing_feedback ~diags ~feedback
in
{ Node.range; prev; ast = Some ast; diags; messages; state; info }
let strategy_of_coq_err ~node ~state ~last_tok = function
| Coq.Protect.Error.Anomaly _ -> Stop (Failed last_tok, node)
| User _ -> Continue { state; last_tok; node }
let node_of_coq_result ~token ~doc ~range ~prev ~ast ~st ~parsing_diags
~parsing_feedback ~feedback ~info last_tok res =
match res with
| Ok state ->
let node =
parsed_node ~range ~prev ~ast ~state ~parsing_diags ~parsing_feedback
~diags:[] ~feedback ~info
in
Continue { state; last_tok; node }
| Error
(Coq.Protect.Error.Anomaly { range = err_range; quickFix; msg } as coq_err)
| Error (User { range = err_range; quickFix; msg } as coq_err) ->
let err_range = Option.default range err_range in
let err_diags =
[ Diags.error ~err_range ~quickFix ~msg ~stm_range:range ~ast () ]
in
let contents, nodes = (doc.contents, doc.nodes) in
let context =
Recovery_context.make ~contents ~last_tok ~nodes ~ast:ast.v ()
in
let recovery_st = Recovery.handle ~token ~context ~st in
let node =
parsed_node ~range ~prev ~ast ~state:recovery_st ~parsing_diags
~parsing_feedback ~diags:err_diags ~feedback ~info
in
strategy_of_coq_err ~node ~state:recovery_st ~last_tok coq_err
let document_action ~token ~st ~parsing_diags ~parsing_feedback ~parsing_time
~prev ~doc last_tok doc_handle action =
match action with
| EOF completed ->
let range = Completion.range completed in
let node =
unparseable_node ~range ~prev ~parsing_diags ~parsing_feedback ~state:st
~parsing_time
in
Stop (completed, node)
| Skip (span_range, last_tok) ->
let context =
Recovery_context.make ~contents:doc.contents ~last_tok ~nodes:doc.nodes ()
in
let st = Recovery.handle ~token ~context ~st in
let node =
unparseable_node ~range:span_range ~prev ~parsing_diags ~parsing_feedback
~state:st ~parsing_time
in
Continue { state = st; last_tok; node }
| Process ast -> (
let lines, files = (doc.contents.lines, doc.env.files) in
let process_res, info =
interp_and_info ~token ~parsing_time ~st ~files ~doc ast
in
let f = Coq.Utils.to_range ~lines in
let { Coq.Protect.E.r; feedback } = Coq.Protect.E.map_loc ~f process_res in
match r with
| Coq.Protect.R.Interrupted ->
Interrupted last_tok
| Coq.Protect.R.Completed res ->
let ast_loc = Coq.Ast.loc ast |> Option.get in
let ast_range = Coq.Utils.to_range ~lines ast_loc in
let ast =
Node.Ast.{ v = ast; ast_info = Coq.Ast.make_info ~lines ~st ast }
in
let last_tok_new = Coq.Parsing.Parsable.loc doc_handle in
let last_tok_new = Coq.Utils.to_range ~lines last_tok_new in
node_of_coq_result ~token ~doc ~range:ast_range ~prev ~ast ~st
~parsing_diags ~parsing_feedback ~feedback ~info last_tok_new res)
module Target = struct
type t =
| End
| Position of int * int
let pp fmt = function
| End -> Format.fprintf fmt "{target: end}"
| Position (l, c) -> Format.fprintf fmt "{target: l: %02d | c: %02d}" l c
let reached ~(range : Lang.Range.t) (line, col) =
let reached_line = range.end_.line in
let reached_col = range.end_.character in
line < reached_line || (line = reached_line && col <= reached_col)
end
let beyond_target (range : Lang.Range.t) target =
match target with
| Target.End -> false
| Position (cut_line, cut_col) -> Target.reached ~range (cut_line, cut_col)
let log_beyond_target last_tok target =
Io.Log.trace "beyond_target" "target reached %a" Lang.Range.pp last_tok;
Io.Log.trace "beyond_target" "target is %a" Target.pp target
let max_errors_node ~state ~range ~prev =
let msg = Pp.str "Maximum number of errors reached" in
let parsing_diags = [ Diags.make range Diags.err msg ] in
unparseable_node ~range ~prev ~parsing_diags ~parsing_feedback:[] ~state
~parsing_time:0.0
module Stop_cond = struct
type t =
| Target
| Max_errors
| Continue
let should_stop acc_errors last_tok target =
if acc_errors > !Config.v.max_errors then Max_errors
else if beyond_target last_tok target then Target
else Continue
end
let process_and_parse ~io ~token ~target ~uri ~version doc last_tok doc_handle =
let rec stm doc st (last_tok : Lang.Range.t) prev acc_errors =
let doc = send_eager_diagnostics ~io ~uri ~version ~doc in
report_progress ~io ~doc last_tok;
match Stop_cond.should_stop acc_errors last_tok target with
| Max_errors ->
let completed = Completion.Failed last_tok in
let node = max_errors_node ~state:st ~range:last_tok ~prev in
let doc = add_node ~node doc in
set_completion ~completed doc
| Target ->
let () = log_beyond_target last_tok target in
let completed =
if last_tok.end_.offset >= doc.contents.last.offset then
Completion.Yes last_tok
else Completion.Stopped last_tok
in
set_completion ~completed doc
| Continue -> (
if Debug.parsing then Io.Log.trace "coq" "parsing sentence";
let lines = doc.contents.lines in
let action, parsing_diags, parsing_feedback, parsing_time =
parse_action ~token ~lines ~st last_tok doc_handle
in
let action =
document_action ~token ~st ~parsing_diags ~parsing_feedback
~parsing_time ~prev ~doc last_tok doc_handle action
in
match action with
| Interrupted last_tok -> set_completion ~completed:(Stopped last_tok) doc
| Stop (completed, node) ->
let doc = add_node ~node doc in
report_progress ~io ~doc (Completion.range completed);
set_completion ~completed doc
| Continue { state; last_tok; node } ->
let n_errors = CList.count Lang.Diagnostic.is_error node.Node.diags in
let doc = add_node ~node doc in
stm doc state last_tok (Some node) (acc_errors + n_errors))
in
let doc = { doc with nodes = List.rev doc.nodes } in
let last_node, st, stats =
match Util.hd_opt doc.nodes with
| None -> (None, doc.root, Stats.Global.zero ())
| Some { Node.state; range; info = { global_stats; _ }; _ } as last_node ->
Io.Log.trace "resume / process_and_parse" "last node: %a" Lang.Range.pp
range;
(last_node, state, global_stats)
in
Stats.Global.restore stats;
let doc = stm doc st last_tok last_node 0 in
let doc = { doc with nodes = List.rev doc.nodes } in
doc
let log_doc_completion (completed : Completion.t) =
let timestamp = Unix.gettimeofday () in
let range = Completion.range completed in
let status = Completion.to_string completed in
Io.Log.trace "check" "done [%.2f]: document %s with pos %a" timestamp status
Lang.Range.pp range
let debug_loc_after line (r : Lang.Range.t) =
if Debug.unicode then
Io.Log.trace "loc_after" "str: '%s' | char: %d" line r.end_.character
let loc_after ~lines ~uri (r : Lang.Range.t) =
let line_nb_last = r.end_.line + 1 in
let end_index =
let line = Array.get lines r.end_.line in
debug_loc_after line r;
Lang.Utf.utf8_offset_of_utf16_offset ~line ~offset:r.end_.character
in
let bol_pos_last = r.end_.offset - end_index in
{ Loc.fname = init_fname ~uri
; line_nb = line_nb_last
; bol_pos = bol_pos_last
; line_nb_last
; bol_pos_last
; bp = r.end_.offset
; ep = r.end_.offset
}
(** Setup parser and call the main routine *)
let resume_check ~io ~token ~(last_tok : Lang.Range.t) ~doc ~target =
let uri, version, contents = (doc.uri, doc.version, doc.contents) in
let lines = doc.contents.lines in
let resume_loc = loc_after ~lines ~uri last_tok in
let offset = resume_loc.Loc.bp in
let pcontent_len = contents.last.offset in
match Util.safe_sub contents.text offset (pcontent_len - offset) with
| None ->
let completed = Completion.Failed last_tok in
set_completion ~completed doc
| Some processed_content ->
let handle =
Coq.Parsing.Parsable.make ~loc:resume_loc
Gramlib.Stream.(of_string ~offset processed_content)
in
process_and_parse ~io ~token ~target ~uri ~version doc last_tok handle
(** Check a document, if it was not completed already *)
let check ~io ~token ~target ~doc () =
match doc.completed with
| Yes _ ->
Io.Log.trace "check" "resuming, completed=yes, nothing to do";
doc
| Failed _ ->
Io.Log.trace "check" "can't resume, failed=yes, nothing to do";
doc
| Stopped last_tok ->
DDebug.resume last_tok doc.version;
let doc = resume_check ~io ~token ~last_tok ~doc ~target in
log_doc_completion doc.completed;
Util.print_stats ();
doc
let save ~token ~doc =
match doc.completed with
| Yes _ ->
let st = Util.last doc.nodes |> Option.cata Node.state doc.root in
let uri = doc.uri in
let ldir = Coq.Workspace.dirpath_of_uri ~uri in
let in_file = Lang.LUri.File.to_string_file uri in
Coq.State.in_stateM ~token ~st
~f:(fun () -> Coq.Save.save_vo ~token ~st ~ldir ~in_file)
()
| _ ->
let error = Pp.(str "Can't save document that failed to check") in
Coq.Protect.E.error error
let eval_no_memo ~token (st, cmd) =
Coq.Interp.interp ~token ~intern:Vernacinterp.fs_intern ~st cmd
let rec parse_execute_loop ~token ~memo pa st =
let open Coq.Protect.E.O in
let eval = if memo then Memo.Interp.eval else eval_no_memo in
let* ast = Coq.Parsing.parse ~token ~st pa in
match ast with
| Some ast ->
let* st = eval ~token (st, ast) in
parse_execute_loop ~token ~memo pa st
| None -> Coq.Protect.E.ok st
let parse_and_execute_in ~token ~loc tac st =
let str = Gramlib.Stream.of_string tac in
let pa = Coq.Parsing.Parsable.make ?loc str in
parse_execute_loop ~token pa st
let run ~token ?loc ?(memo = true) ~st cmds =
Coq.State.in_stateM ~token ~st
~f:(parse_and_execute_in ~token ~loc ~memo cmds)
st