File: toplevel.ml

package info (click to toggle)
coq-doc 8.2pl1-1
  • links: PTS, VCS
  • area: non-free
  • in suites: squeeze
  • size: 19,240 kB
  • ctags: 22,737
  • sloc: ml: 132,933; ansic: 1,960; sh: 1,366; lisp: 456; makefile: 327
file content (386 lines) | stat: -rw-r--r-- 12,911 bytes parent folder | download
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
(************************************************************************)
(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
(*   \VV/  **************************************************************)
(*    //   *      This file is distributed under the terms of the       *)
(*         *       GNU Lesser General Public License Version 2.1        *)
(************************************************************************)

(* $Id: toplevel.ml 11784 2009-01-14 11:36:32Z herbelin $ *)

open Pp
open Util
open Flags
open Cerrors
open Vernac
open Vernacexpr
open Pcoq
open Protectedtoplevel

(* A buffer for the character read from a channel. We store the command
 * entered to be able to report errors without pretty-printing. *)

type input_buffer = { 
  mutable prompt : unit -> string;
  mutable str : string; (* buffer of already read characters *)
  mutable len : int;    (* number of chars in the buffer *)
  mutable bols : int list; (* offsets in str of begining of lines *)
  mutable tokens : Gram.parsable; (* stream of tokens *)
  mutable start : int } (* stream count of the first char of the buffer *)

(* Double the size of the buffer. *)

let resize_buffer ibuf =
  let nstr = String.create (2 * String.length ibuf.str + 1) in
  String.blit ibuf.str 0 nstr 0 (String.length ibuf.str);
  ibuf.str <- nstr

(* Delete all irrelevent lines of the input buffer. Keep the last line
   in the buffer (useful when there are several commands on the same line. *)

let resynch_buffer ibuf =
  match ibuf.bols with
    | ll::_ ->
        let new_len = ibuf.len - ll in
        String.blit ibuf.str ll ibuf.str 0 new_len;
        ibuf.len <- new_len;
        ibuf.bols <- [];
        ibuf.start <- ibuf.start + ll
    | _ -> ()


(* emacs special character for prompt end (fast) detection. Prefer
   (Char.chr 6) since it does not interfere with utf8. For
    compatibility we let (Char.chr 249) as default for a while. *)

let emacs_prompt_startstring() = Printer.emacs_str "" "<prompt>"

let emacs_prompt_endstring() = Printer.emacs_str (String.make 1 (Char.chr 249)) "</prompt>"

(* Read a char in an input channel, displaying a prompt at every
   beginning of line. *)
let prompt_char ic ibuf count =
  let bol = match ibuf.bols with
    | ll::_ -> ibuf.len == ll
    | [] -> ibuf.len == 0
  in
  if bol && not !print_emacs then msgerr (str (ibuf.prompt()));
  try
    let c = input_char ic in
    if c == '\n' then ibuf.bols <- (ibuf.len+1) :: ibuf.bols;
    if ibuf.len == String.length ibuf.str then resize_buffer ibuf;
    ibuf.str.[ibuf.len] <- c;
    ibuf.len <- ibuf.len + 1;
    Some c
  with End_of_file -> 
    None

(* Reinitialize the char stream (after a Drop) *)

let reset_input_buffer ic ibuf =
  ibuf.str <- "";
  ibuf.len <- 0;
  ibuf.bols <- [];
  ibuf.tokens <- Gram.parsable (Stream.from (prompt_char ic ibuf));
  ibuf.start <- 0

(* Functions to print underlined locations from an input buffer. *)

(* Given a location, returns the list of locations of each line. The last
   line is returned separately. It also checks the location bounds. *)

let get_bols_of_loc ibuf (bp,ep) =
  let add_line (b,e) lines =
    if b < 0 or e < b then anomaly "Bad location";
    match lines with
      | ([],None) -> ([], Some (b,e))
      | (fl,oe) -> ((b,e)::fl, oe) 
  in
  let rec lines_rec ba after = function
    | []                  -> add_line (0,ba) after
    | ll::_ when ll <= bp -> add_line (ll,ba) after
    | ll::fl              ->
        let nafter = if ll < ep then add_line (ll,ba) after else after in
        lines_rec ll nafter fl 
  in
  let (fl,ll) = lines_rec ibuf.len ([],None) ibuf.bols in
  (fl,Option.get ll)

let dotted_location (b,e) =
  if e-b < 3 then 
    ("", String.make (e-b) ' ')
  else 
    (String.make (e-b-1) '.', " ")

let print_highlight_location ib loc =
  let (bp,ep) = unloc loc in
  let bp = bp - ib.start 
  and ep = ep - ib.start in
  let highlight_lines =
    match get_bols_of_loc ib (bp,ep) with
      | ([],(bl,el)) ->  
	  (str"> " ++ str(String.sub ib.str bl (el-bl-1)) ++ fnl () ++
             str"> " ++ str(String.make (bp-bl) ' ') ++
             str(String.make (ep-bp) '^'))
      | ((b1,e1)::ml,(bn,en)) ->
          let (d1,s1) = dotted_location (b1,bp) in
          let (dn,sn) = dotted_location (ep,en) in
          let l1 = (str"> " ++ str d1 ++ str s1 ++
                      str(String.sub ib.str bp (e1-bp))) in
          let li =
            prlist (fun (bi,ei) ->
                      (str"> " ++ str(String.sub ib.str bi (ei-bi)))) ml in
          let ln = (str"> " ++ str(String.sub ib.str bn (ep-bn)) ++
                      str sn ++ str dn) in 
	  (l1 ++ li ++ ln)
  in 
  let loc = make_loc (bp,ep) in
  (str"Toplevel input, characters " ++ Cerrors.print_loc loc ++ str":" ++ fnl () ++
     highlight_lines ++ fnl ())

(* Functions to report located errors in a file. *)

let print_location_in_file s inlibrary fname loc =
  let errstrm = str"Error while reading " ++ str s in
  if loc = dummy_loc then
    hov 1 (errstrm ++ spc() ++ str" (unknown location):") ++ fnl ()
  else
    let errstrm =
      if s = fname then mt() else errstrm ++ str":" ++ fnl() in
    if inlibrary then
      hov 0 (errstrm ++ str"Module " ++ str ("\""^fname^"\"") ++ spc() ++
             str"characters " ++ Cerrors.print_loc loc) ++ fnl ()
    else
    let (bp,ep) = unloc loc in
    let ic = open_in fname in
    let rec line_of_pos lin bol cnt =
      if cnt < bp then
        if input_char ic == '\n'
        then line_of_pos (lin + 1) (cnt +1) (cnt+1)
        else line_of_pos lin bol (cnt+1)
      else (lin, bol)
    in
    try
      let (line, bol) = line_of_pos 1 0 0 in
      close_in ic;
      hov 0
        (errstrm ++ str"File " ++ str ("\""^fname^"\"") ++ str"," ++ spc() ++
         hov 0 (str"line " ++ int line ++ str"," ++ spc() ++
                str"characters " ++
                Cerrors.print_loc (make_loc (bp-bol,ep-bol))) ++ str":") ++
      fnl ()
    with e ->
      (close_in ic;
       hov 1 (errstrm ++ spc() ++ str"(invalid location):") ++ fnl ())
	
let print_command_location ib dloc =
  match dloc with
    | Some (bp,ep) ->
        (str"Error during interpretation of command:" ++ fnl () ++
           str(String.sub ib.str (bp-ib.start) (ep-bp)) ++ fnl ())
    | None -> (mt ())

let valid_loc dloc loc =
  loc <> dummy_loc
  & match dloc with
    | Some dloc ->
	let (bd,ed) = unloc dloc in let (b,e) = unloc loc in bd<=b & e<=ed
    | _ -> true
	  
let valid_buffer_loc ib dloc loc =
  valid_loc dloc loc & 
  let (b,e) = unloc loc in b-ib.start >= 0 & e-ib.start < ib.len & b<=e 

(*s The Coq prompt is the name of the focused proof, if any, and "Coq"
    otherwise. We trap all exceptions to prevent the error message printing
    from cycling. *)
let make_prompt () =
  try
    (Names.string_of_id (Pfedit.get_current_proof_name ())) ^ " < "
  with _ -> 
    "Coq < "

(*let build_pending_list l = 
  let pl = ref ">" in
  let l' = ref l in
  let res = 
    while List.length !l' > 1 do 
      pl := !pl ^ "|" Names.string_of_id x;
      l':=List.tl !l'
    done in
  let last = try List.hd !l' with _ ->   in
  "<"^l'
*)    

(* the coq prompt added to the default one when in emacs mode
   The prompt contains the current state label [n] (for global
   backtracking) and the current proof state [p] (for proof
   backtracking) plus the list of open (nested) proofs (for proof
   aborting when backtracking). It looks like:
   
   "n |lem1|lem2|lem3| p < "
*)
let make_emacs_prompt() =
  let statnum = string_of_int (Lib.current_command_label ()) in
  let dpth = Pfedit.current_proof_depth() in
  let pending = Pfedit.get_all_proof_names() in
  let pendingprompt = 
    List.fold_left 
      (fun acc x -> acc ^ (if acc <> "" then "|" else "") ^ Names.string_of_id x)
      "" pending in
  let proof_info = if dpth >= 0 then string_of_int dpth else "0" in
  if !Flags.print_emacs then statnum ^ " |" ^ pendingprompt ^ "| " ^ proof_info ^ " < "
  else ""

(* A buffer to store the current command read on stdin. It is
 * initialized when a vernac command is immediately followed by "\n",
 * or after a Drop. *)
let top_buffer =
  let pr() = 
    emacs_prompt_startstring() 
    ^ make_prompt() 
    ^ make_emacs_prompt()
    ^ emacs_prompt_endstring()
  in
  { prompt = pr;
    str = "";
    len = 0;
    bols = [];
    tokens = Gram.parsable (Stream.of_list []);
    start = 0 }

let set_prompt prompt =
  top_buffer.prompt
  <- (fun () -> 
    emacs_prompt_startstring()
    ^ prompt ()
    ^ emacs_prompt_endstring())

(* Removes and prints the location of the error. The following exceptions
   need not be located. *)
let rec is_pervasive_exn = function
  | Out_of_memory | Stack_overflow | Sys.Break -> true
  | Error_in_file (_,_,e) -> is_pervasive_exn e
  | Stdpp.Exc_located (_,e) -> is_pervasive_exn e
  | DuringCommandInterp (_,e) -> is_pervasive_exn e
  | DuringSyntaxChecking e -> is_pervasive_exn e
  | _ -> false

(* Toplevel error explanation, dealing with locations, Drop, Ctrl-D
   May raise only the following exceptions: Drop and End_of_input,
   meaning we get out of the Coq loop *)
let print_toplevel_error exc =
  let (dloc,exc) =
    match exc with
      | DuringCommandInterp (loc,ie)
      | Stdpp.Exc_located (loc, DuringSyntaxChecking ie) ->
          if loc = dummy_loc then (None,ie) else (Some loc, ie)
      | _ -> (None, exc) 
  in
  let (locstrm,exc) =
    match exc with
      | Stdpp.Exc_located (loc, ie) ->
          if valid_buffer_loc top_buffer dloc loc then
            (print_highlight_location top_buffer loc, ie)
          else 
	    ((mt ()) (* print_command_location top_buffer dloc *), ie)
      | Error_in_file (s, (inlibrary, fname, loc), ie) ->
          (print_location_in_file s inlibrary fname loc, ie)
      | _ -> 
	  ((mt ()) (* print_command_location top_buffer dloc *), exc)
  in
  match exc with
    | End_of_input -> 
	msgerrnl (mt ()); pp_flush(); exit 0
    | Vernacexpr.Drop ->  (* Last chance *)
        if Mltop.is_ocaml_top() then raise Vernacexpr.Drop;
        (str"Error: There is no ML toplevel." ++ fnl ())
    | Vernacexpr.ProtectedLoop ->
	raise Vernacexpr.ProtectedLoop
    | Vernacexpr.Quit -> 
	raise Vernacexpr.Quit
    | _ -> 
	(if is_pervasive_exn exc then (mt ()) else locstrm) ++
        Cerrors.explain_exn exc

(* Read the input stream until a dot is encountered *)
let parse_to_dot =
  let rec dot st = match Stream.next st with
    | ("", ".") -> ()
    | ("EOI", "") -> raise End_of_input
    | _ -> dot st
  in 
  Gram.Entry.of_parser "Coqtoplevel.dot" dot
    
(* We assume that when a lexer error occurs, at least one char was eaten *)
let rec discard_to_dot () =
  try 
    Gram.Entry.parse parse_to_dot top_buffer.tokens
  with Stdpp.Exc_located(_,Token.Error _) -> 
    discard_to_dot()


(* If the error occured while parsing, we read the input until a dot token
 * in encountered. *)

let process_error = function
  | DuringCommandInterp _ 
  | Stdpp.Exc_located (_,DuringSyntaxChecking _) as e -> e
  | e ->
      if is_pervasive_exn e then 
	e
      else 
        try 
	  discard_to_dot (); e 
	with
          | End_of_input -> End_of_input
          | de -> if is_pervasive_exn de then de else e

(* do_vernac reads and executes a toplevel phrase, and print error
   messages when an exception is raised, except for the following:
     Drop: kill the Coq toplevel, going down to the Caml toplevel if it exists.
           Otherwise, exit.
     End_of_input: Ctrl-D was typed in, we will quit *)
let do_vernac () =
  msgerrnl (mt ());
  if !print_emacs then msgerr (str (top_buffer.prompt()));
  resynch_buffer top_buffer;
  begin 
    try 
      raw_do_vernac top_buffer.tokens
    with e -> 
      msgnl (print_toplevel_error (process_error e)) 
  end;
  flush_all()

(* coq and go read vernacular expressions until Drop is entered.
 * Ctrl-C will raise the exception Break instead of aborting Coq.
 * Here we catch the exceptions terminating the Coq loop, and decide
 * if we really must quit.
 * The boolean value is used to choose between a protected loop, which
 * we think is more suited for communication with other programs, or
 * plain communication. *)

let rec coq_switch b =
  Sys.catch_break true;
  (* ensure we have a command separator object (DOT) so that the first
     command can be reseted. *)
  Lib.mark_end_of_command();
  try
    if b then begin
      reset_input_buffer stdin top_buffer;
      while true do do_vernac() done
    end else
      protected_loop stdin
  with
    | Vernacexpr.Drop -> ()
    | Vernacexpr.ProtectedLoop -> 
	Lib.declare_initial_state();
	coq_switch false
    | End_of_input -> msgerrnl (mt ()); pp_flush(); exit 0
    | Vernacexpr.Quit -> exit 0
    | e ->
	msgerrnl (str"Anomaly. Please report.");
	coq_switch b

let loop () = coq_switch true