|
(************************************************************************)
(* * 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) *)
(************************************************************************)
(*s Utility functions for the scanners *)
{
open Printf
open Lexing
(* A list function we need *)
let rec take n ls =
if n = 0 then [] else
match ls with
| [] -> []
| (l :: ls) -> l :: (take (n-1) ls)
(* count the number of spaces at the beginning of a string *)
let count_spaces s =
let n = String.length s in
let rec count c i =
if i == n then c,i else match s.[i] with
| '\t' -> count (c + (8 - (c mod 8))) (i + 1)
| ' ' -> count (c + 1) (i + 1)
| _ -> c,i
in
count 0 0
let remove_newline s =
let n = String.length s in
let rec count i = if i == n || s.[i] <> '\n' then i else count (i + 1) in
let i = count 0 in
i, String.sub s i (n - i)
let count_dashes s =
let c = ref 0 in
for i = 0 to String.length s - 1 do if s.[i] = '-' then incr c done;
!c
let cut_head_tail_spaces s =
let n = String.length s in
let rec look_up i = if i == n || s.[i] <> ' ' then i else look_up (i+1) in
let rec look_dn i = if i == -1 || s.[i] <> ' ' then i else look_dn (i-1) in
let l = look_up 0 in
let r = look_dn (n-1) in
if l <= r then String.sub s l (r-l+1) else s
let sec_title s =
let rec count lev i =
if s.[i] = '*' then
count (succ lev) (succ i)
else
let t = String.sub s i (String.length s - i) in
lev, cut_head_tail_spaces t
in
count 0 (String.index s '*')
let strip_eol s =
let eol = s.[String.length s - 1] = '\n' in
(eol, if eol then String.sub s 1 (String.length s - 1) else s)
let formatted = ref false
let brackets = ref 0
let comment_level = ref 0
let in_proof = ref None
let in_env start stop =
let r = ref false in
let start_env () = r := true; start () in
let stop_env () = if !r then stop (); r := false in
(fun x -> !r), start_env, stop_env
let _, start_emph, stop_emph = in_env Output.start_emph Output.stop_emph
let in_quote, start_quote, stop_quote = in_env Output.start_quote Output.stop_quote
let url_buffer = Buffer.create 40
let url_name_buffer = Buffer.create 40
let backtrack lexbuf = lexbuf.lex_curr_pos <- lexbuf.lex_start_pos;
lexbuf.lex_curr_p <- lexbuf.lex_start_p
let backtrack_past_newline lexbuf =
let buf = lexeme lexbuf in
let splits = Str.bounded_split_delim (Str.regexp "['\n']") buf 2 in
match splits with
| [] -> ()
| (_ :: []) -> ()
| (s1 :: rest :: _) ->
let length_skip = 1 + String.length s1 in
lexbuf.lex_curr_pos <- lexbuf.lex_start_pos + length_skip
(* saving/restoring the PP state *)
type state = {
st_gallina : bool;
st_light : bool
}
let state_stack = Stack.create ()
let save_state () =
Stack.push { st_gallina = !Cdglobals.gallina; st_light = !Cdglobals.light } state_stack
let restore_state () =
let s = Stack.pop state_stack in
Cdglobals.gallina := s.st_gallina;
Cdglobals.light := s.st_light
let begin_show () = save_state (); Cdglobals.gallina := false; Cdglobals.light := false
let end_show () = restore_state ()
(* Reset the globals *)
let reset () =
formatted := false;
brackets := 0;
comment_level := 0
(* erasing of Section/End *)
let section_re = Str.regexp "[ \t]*Section"
let end_re = Str.regexp "[ \t]*End"
let is_section s = Str.string_match section_re s 0
let is_end s = Str.string_match end_re s 0
let sections_to_close = ref 0
let section_or_end s =
if is_section s then begin
incr sections_to_close; true
end else if is_end s then begin
if !sections_to_close > 0 then begin
decr sections_to_close; true
end else
false
end else
true
(* for item lists *)
type list_compare =
| Before
| StartLevel of int
| InLevel of int * bool
(* Before : we're before any levels
StartLevel : at the same column as the dash in a level
InLevel : after the dash of this level, but before any deeper dashes.
bool is true if this is the last level *)
let find_level levels cur_indent =
match levels with
| [] -> Before
| (l::ls) ->
if cur_indent < l then Before
else
(* cur_indent will never be less than the head of the list *)
let rec findind ls n =
match ls with
| [] -> InLevel (n,true)
| (l :: []) -> if cur_indent = l then StartLevel n
else InLevel (n,true)
| (l1 :: l2 :: ls) ->
if cur_indent = l1 then StartLevel n
else if cur_indent < l2 then InLevel (n,false)
else findind (l2 :: ls) (n+1)
in
findind (l::ls) 1
type is_start_list =
| Rule
| List of int
| Neither
let check_start_list str =
let n_dashes = count_dashes str in
let (n_spaces,_) = count_spaces str in
if n_dashes >= 4 && not !Cdglobals.plain_comments then
Rule
else
if n_dashes = 1 && not !Cdglobals.plain_comments then
List n_spaces
else
Neither
(* examine a string for subtitleness *)
let subtitle m s =
match Str.split_delim (Str.regexp ":") s with
| [] -> false
| (name::_) ->
if (cut_head_tail_spaces name) = m then
true
else
false
(* tokens pretty-print *)
let token_buffer = Buffer.create 1024
let token_re =
Str.regexp "[ \t]*(\\*\\*[ \t]+printing[ \t]+\\([^ \t]+\\)"
let printing_token_re =
Str.regexp
"[ \t]*\\(\\(%\\([^%]*\\)%\\)\\|\\(\\$[^$]*\\$\\)\\)?[ \t]*\\(#\\(\\(&#\\|[^#]\\)*\\)#\\)?"
let add_printing_token toks pps =
try
if Str.string_match token_re toks 0 then
let tok = Str.matched_group 1 toks in
if Str.string_match printing_token_re pps 0 then
let pp =
(try Some (Str.matched_group 3 pps) with _ ->
try Some (Str.matched_group 4 pps) with _ -> None),
(try Some (Str.matched_group 6 pps) with _ -> None)
in
Output.add_printing_token tok pp
with _ ->
()
let remove_token_re =
Str.regexp
"[ \t]*(\\*\\*[ \t]+remove[ \t]+printing[ \t]+\\([^ \t]+\\)[ \t]*\\*)"
let remove_printing_token toks =
try
if Str.string_match remove_token_re toks 0 then
let tok = Str.matched_group 1 toks in
Output.remove_printing_token tok
with _ ->
()
let output_indented_keyword s lexbuf =
let nbsp,isp = count_spaces s in
Output.indentation nbsp;
let s = String.sub s isp (String.length s - isp) in
Output.keyword s (lexeme_start lexbuf + isp)
let only_gallina () =
!Cdglobals.gallina && !in_proof <> None
let parse_comments () =
!Cdglobals.parse_comments && not (only_gallina ())
}
(*s Regular expressions *)
let space = [' ' '\t']
let space_nl = [' ' '\t' '\n' '\r']
let nl = "\r\n" | '\n'
let firstchar =
['A'-'Z' 'a'-'z' '_'] |
(* superscript 1 *)
'\194' '\185' |
(* utf-8 latin 1 supplement *)
'\195' ['\128'-'\150'] |
'\195' ['\152'-'\182'] |
'\195' ['\184'-'\191'] |
(* utf-8 letterlike symbols *)
'\206' (['\145'-'\161'] | ['\163'-'\191']) |
'\207' (['\145'-'\191']) |
'\226' ('\130' [ '\128'-'\137' ] (* subscripts *)
| '\129' [ '\176'-'\187' ] (* superscripts *)
| '\132' ['\128'-'\191'] | '\133' ['\128'-'\143'])
let identchar =
firstchar | ['\'' '0'-'9' '@' ]
let id = firstchar identchar*
let pfx_id = (id '.')*
let identifier =
id | pfx_id id
(* This misses unicode stuff, and it adds "[" and "]". It's only an
approximation of idents - used for detecting whether an underscore
is part of an identifier or meant to indicate emphasis *)
let nonidentchar = [^ 'A'-'Z' 'a'-'z' '_' '[' ']' '\'' '0'-'9' '@' ]
let printing_token = [^ ' ' '\t']*
let thm_token =
"Theorem"
| "Lemma"
| "Fact"
| "Remark"
| "Corollary"
| "Proposition"
| "Property"
| "Goal"
let prf_token =
"Next" space+ "Obligation"
| "Proof" (space* "." | space+ "with" | space+ "using")
let immediate_prf_token =
(* Approximation of a proof term, if not in the prf_token case *)
(* To be checked after prf_token *)
"Proof" space* [^ '.' 'w' 'u']
let def_token =
"Definition"
| "Let"
| "Class"
| "SubClass"
| "Example"
| "Fixpoint"
| "Function"
| "Boxed"
| "CoFixpoint"
| "Record"
| "Variant"
| "Structure"
| "Scheme"
| "Inductive"
| "CoInductive"
| "Equations"
| "Instance"
| "Declare" space+ "Instance"
| "Global" space+ "Instance"
| "Functional" space+ "Scheme"
let decl_token =
"Hypothesis"
| "Hypotheses"
| "Parameter" 's'?
| "Axiom" 's'?
| "Conjecture"
let gallina_ext =
"Module"
| "Include" space+ "Type"
| "Include"
| "Declare" space+ "Module"
| "Transparent"
| "Opaque"
| "Canonical"
| "Coercion"
| "Identity"
| "Implicit"
| "Tactic" space+ "Notation"
| "Section"
| "Context"
| "Variable" 's'?
| ("Hypothesis" | "Hypotheses")
| "End"
let notation_kw =
"Notation"
| "Infix"
| "Reserved" space+ "Notation"
let commands =
"Pwd"
| "Cd"
| "Drop"
| "ProtectedLoop"
| "Quit"
| "Restart"
| "Load"
| "Add"
| "Remove" space+ "Loadpath"
| "Print"
| "Inspect"
| "About"
| "SearchAbout"
| "SearchRewrite"
| "Search"
| "Locate"
| "Eval"
| "Reset"
| "Check"
| "Type"
| "Section"
| "Chapter"
| "Variable" 's'?
| ("Hypothesis" | "Hypotheses")
| "End"
let end_kw =
immediate_prf_token | "Qed" | "Defined" | "Save" | "Admitted" | "Abort"
let extraction =
"Extraction"
| "Recursive" space+ "Extraction"
| "Extract"
let gallina_kw = thm_token | def_token | decl_token | gallina_ext | commands | extraction
let prog_kw =
"Program" space+ gallina_kw
| "Obligation"
| "Obligations"
| "Solve"
let hint_kw =
"Extern" | "Rewrite" | "Resolve" | "Immediate" | "Transparent" | "Opaque" | "Unfold" | "Constructors"
let set_kw =
"Printing" space+ ("Coercions" | "Universes" | "All")
| "Implicit" space+ "Arguments"
let gallina_kw_to_hide =
"Implicit" space+ "Arguments"
| ("Local" space+)? "Ltac"
| "From"
| "Require"
| "Import"
| "Export"
| "Load"
| "Hint" space+ hint_kw
| "Open"
| "Close"
| "Delimit"
| "Transparent"
| "Opaque"
| ("Declare" space+ ("Morphism" | "Step") )
| ("Set" | "Unset") space+ set_kw
| "Declare" space+ ("Left" | "Right") space+ "Step"
| "Debug" space+ ("On" | "Off")
let section = "*" | "**" | "***" | "****"
let item_space = " "
let begin_hide = "(*" space* "begin" space+ "hide" space* "*)" space* nl
let end_hide = "(*" space* "end" space+ "hide" space* "*)" space* nl
let begin_show = "(*" space* "begin" space+ "show" space* "*)" space* nl
let end_show = "(*" space* "end" space+ "show" space* "*)" space* nl
(*
let begin_verb = "(*" space* "begin" space+ "verb" space* "*)
let end_verb = "(*" space* "end" space+ "verb" space* "*)"
*)
(*s Scanning Coq, at beginning of line *)
rule coq_bol = parse
| space* nl+
{ if not (!in_proof <> None && (!Cdglobals.gallina || !Cdglobals.light))
then Output.empty_line_of_code ();
coq_bol lexbuf }
| space* "(**" space_nl
{ Output.end_coq (); Output.start_doc ();
let eol = doc_bol lexbuf in
Output.end_doc (); Output.start_coq ();
if eol then coq_bol lexbuf else coq lexbuf }
| space* "Comments" space_nl
{ Output.end_coq (); Output.start_doc (); comments lexbuf; Output.end_doc ();
Output.start_coq (); coq lexbuf }
| space* begin_hide
{ skip_hide lexbuf; coq_bol lexbuf }
| space* begin_show
{ begin_show (); coq_bol lexbuf }
| space* end_show
{ end_show (); coq_bol lexbuf }
| space* (("Local"|"Global") space+)? gallina_kw_to_hide
{ let s = lexeme lexbuf in
if !Cdglobals.light && section_or_end s then
let eol = skip_to_dot lexbuf in
if eol then (coq_bol lexbuf) else coq lexbuf
else
begin
output_indented_keyword s lexbuf;
let eol = body lexbuf in
if eol then coq_bol lexbuf else coq lexbuf
end }
| space* thm_token
{ let s = lexeme lexbuf in
output_indented_keyword s lexbuf;
let eol = body lexbuf in
in_proof := Some eol;
if eol then coq_bol lexbuf else coq lexbuf }
| space* prf_token
{ in_proof := Some true;
let eol =
if not !Cdglobals.gallina then
begin backtrack lexbuf; body_bol lexbuf end
else
let s = lexeme lexbuf in
if s.[String.length s - 1] = '.' then false
else skip_to_dot lexbuf
in if eol then coq_bol lexbuf else coq lexbuf }
| space* end_kw {
let eol =
if not (only_gallina ()) then
begin backtrack lexbuf; body_bol lexbuf end
else skip_to_dot lexbuf
in
in_proof := None;
if eol then coq_bol lexbuf else coq lexbuf }
| space* gallina_kw
{
in_proof := None;
let s = lexeme lexbuf in
output_indented_keyword s lexbuf;
let eol= body lexbuf in
if eol then coq_bol lexbuf else coq lexbuf }
| space* prog_kw
{
in_proof := None;
let s = lexeme lexbuf in
output_indented_keyword s lexbuf;
let eol= body lexbuf in
if eol then coq_bol lexbuf else coq lexbuf }
| space* notation_kw
{ let s = lexeme lexbuf in
output_indented_keyword s lexbuf;
let eol= start_notation_string lexbuf in
if eol then coq_bol lexbuf else coq lexbuf }
| space* "(**" space+ "printing" space+ printing_token space+
{ let tok = lexeme lexbuf in
let s = printing_token_body lexbuf in
add_printing_token tok s;
coq_bol lexbuf }
| space* "(**" space+ "printing" space+
{ eprintf "warning: bad 'printing' command at character %d\n"
(lexeme_start lexbuf); flush stderr;
comment_level := 1;
ignore (comment lexbuf);
coq_bol lexbuf }
| space* "(**" space+ "remove" space+ "printing" space+
printing_token space* "*)"
{ remove_printing_token (lexeme lexbuf);
coq_bol lexbuf }
| space* "(**" space+ "remove" space+ "printing" space+
{ eprintf "warning: bad 'remove printing' command at character %d\n"
(lexeme_start lexbuf); flush stderr;
comment_level := 1;
ignore (comment lexbuf);
coq_bol lexbuf }
| space* "(*"
{ comment_level := 1;
let eol =
if parse_comments () then begin
let s = lexeme lexbuf in
let nbsp, isp = count_spaces s in
Output.indentation nbsp;
Output.start_comment ();
comment lexbuf
end else skipped_comment lexbuf in
if eol then coq_bol lexbuf else coq lexbuf }
| eof
{ () }
| _
{ let eol =
if not !Cdglobals.gallina then
begin backtrack lexbuf; body_bol lexbuf end
else
skip_to_dot_or_brace lexbuf
in
if eol then coq_bol lexbuf else coq lexbuf }
(*s Scanning Coq elsewhere *)
and coq = parse
| nl
{ if not (only_gallina ()) then Output.line_break(); coq_bol lexbuf }
| "(**" space_nl
{ Output.end_coq (); Output.start_doc ();
let eol = doc_bol lexbuf in
Output.end_doc (); Output.start_coq ();
if eol then coq_bol lexbuf else coq lexbuf }
| "(*"
{ comment_level := 1;
let eol =
if parse_comments () then begin
Output.start_comment ();
comment lexbuf
end else skipped_comment lexbuf in
if eol then coq_bol lexbuf else coq lexbuf }
| nl+ space* "]]"
{ if not !formatted then
begin
(* Isn't this an anomaly *)
let s = lexeme lexbuf in
let nlsp,s = remove_newline s in
let nbsp,isp = count_spaces s in
Output.indentation nbsp;
let loc = lexeme_start lexbuf + isp + nlsp in
Output.sublexer ']' loc;
Output.sublexer ']' (loc+1);
coq lexbuf
end }
| eof
{ () }
| (("Local"|"Global") space+)? gallina_kw_to_hide
{ let s = lexeme lexbuf in
if !Cdglobals.light && section_or_end s then
begin
let eol = skip_to_dot lexbuf in
if eol then coq_bol lexbuf else coq lexbuf
end
else
begin
Output.ident s None;
let eol=body lexbuf in
if eol then coq_bol lexbuf else coq lexbuf
end }
| prf_token
{ let eol =
if not !Cdglobals.gallina then
begin backtrack lexbuf; body lexbuf end
else
let s = lexeme lexbuf in
let eol =
if s.[String.length s - 1] = '.' then false
else skip_to_dot lexbuf
in
eol
in if eol then coq_bol lexbuf else coq lexbuf }
| end_kw {
let eol =
if not !Cdglobals.gallina then
begin backtrack lexbuf; body lexbuf end
else
let eol = skip_to_dot lexbuf in
if !in_proof <> Some true && eol then
Output.line_break ();
eol
in
in_proof := None;
if eol then coq_bol lexbuf else coq lexbuf }
| gallina_kw
{ let s = lexeme lexbuf in
Output.ident s None;
let eol = body lexbuf in
if eol then coq_bol lexbuf else coq lexbuf }
| notation_kw
{ let s = lexeme lexbuf in
Output.ident s None;
let eol= start_notation_string lexbuf in
if eol then coq_bol lexbuf else coq lexbuf }
| prog_kw
{ let s = lexeme lexbuf in
Output.ident s None;
let eol = body lexbuf in
if eol then coq_bol lexbuf else coq lexbuf }
| space+ { Output.char ' '; coq lexbuf }
| eof
{ () }
| _ { let eol =
if not !Cdglobals.gallina then
begin backtrack lexbuf; body lexbuf end
else
skip_to_dot_or_brace lexbuf
in
if eol then coq_bol lexbuf else coq lexbuf}
(*s Scanning documentation, at beginning of line *)
and doc_bol = parse
| space* section space+ ([^'\n' '*'] | '*'+ [^'\n' ')' '*'])* ('*'+ '\n')?
{ let eol, lex = strip_eol (lexeme lexbuf) in
let lev, s = sec_title lex in
if (!Cdglobals.lib_subtitles) &&
(subtitle (Output.get_module false) s) then
()
else
Output.section lev (fun () -> ignore (doc None (from_string s)));
if eol then doc_bol lexbuf else doc None lexbuf }
| space_nl* '-'+
{ let buf' = lexeme lexbuf in
let bufs = Str.split_delim (Str.regexp "['\n']") buf' in
let lines = (List.length bufs) - 1 in
let line =
match bufs with
| [] -> eprintf "Internal error bad_split1 - please report\n";
exit 1
| _ -> List.nth bufs lines
in
match check_start_list line with
| Neither -> backtrack_past_newline lexbuf; doc None lexbuf
| List n -> if lines > 0 then Output.paragraph ();
Output.item 1; doc (Some [n]) lexbuf
| Rule -> Output.rule (); doc None lexbuf
}
| space* nl+
{ Output.paragraph (); doc_bol lexbuf }
| "<<" space*
{ Output.start_verbatim false; verbatim 0 false lexbuf; doc_bol lexbuf }
| eof
{ true }
| '_'
{ if !Cdglobals.plain_comments then Output.char '_' else start_emph ();
doc None lexbuf }
| _
{ backtrack lexbuf; doc None lexbuf }
(*s Scanning lists - using whitespace *)
and doc_list_bol indents = parse
| space* '-'
{ let (n_spaces,_) = count_spaces (lexeme lexbuf) in
match find_level indents n_spaces with
| Before -> backtrack lexbuf; doc_bol lexbuf
| StartLevel n -> Output.item n; doc (Some (take n indents)) lexbuf
| InLevel (n,true) ->
let items = List.length indents in
Output.item (items+1);
doc (Some (List.append indents [n_spaces])) lexbuf
| InLevel (_,false) ->
backtrack lexbuf; doc_bol lexbuf
}
| "<<" space*
{ Output.start_verbatim false;
verbatim 0 false lexbuf;
doc_list_bol indents lexbuf }
| "[[" nl
{ formatted := true;
Output.start_inline_coq_block ();
ignore(body_bol lexbuf);
Output.end_inline_coq_block ();
formatted := false;
doc_list_bol indents lexbuf }
| "[[[" nl
{ inf_rules (Some indents) lexbuf }
| space* nl space* '-'
{ (* Like in the doc_bol production, these two productions
exist only to deal properly with whitespace *)
Output.paragraph ();
backtrack_past_newline lexbuf;
doc_list_bol indents lexbuf }
| space* nl space* _
{ let buf' = lexeme lexbuf in
let buf =
let bufs = Str.split_delim (Str.regexp "['\n']") buf' in
match bufs with
| (_ :: s :: []) -> s
| (_ :: _ :: s :: _) -> s
| _ -> eprintf "Internal error bad_split2 - please report\n";
exit 1
in
let (n_spaces,_) = count_spaces buf in
match find_level indents n_spaces with
| StartLevel 1 | Before ->
(* Here we were at the beginning of a line, and it was blank.
The next line started before any list items. So: insert
a paragraph for the empty line, rewind to whatever's just
after the newline, then toss over to doc_bol for whatever
comes next. *)
Output.stop_item ();
Output.paragraph ();
backtrack_past_newline lexbuf;
doc_bol lexbuf
| StartLevel _ | InLevel _ ->
Output.paragraph ();
backtrack_past_newline lexbuf;
doc_list_bol indents lexbuf
}
| space* _
{ let (n_spaces,_) = count_spaces (lexeme lexbuf) in
match find_level indents n_spaces with
| Before -> Output.stop_item (); backtrack lexbuf;
doc_bol lexbuf
| StartLevel n ->
Output.reach_item_level (n-1);
backtrack lexbuf;
doc (Some (take (n-1) indents)) lexbuf
| InLevel (n,_) ->
Output.reach_item_level n;
backtrack lexbuf;
doc (Some (take n indents)) lexbuf
}
(*s Scanning documentation elsewhere *)
and doc indents = parse
| nl
{ Output.char '\n';
match indents with
| Some ls -> doc_list_bol ls lexbuf
| None -> doc_bol lexbuf }
| "[[" nl
{ if !Cdglobals.plain_comments
then (Output.char '['; Output.char '['; doc indents lexbuf)
else (formatted := true;
Output.start_inline_coq_block ();
let eol = body_bol lexbuf in
Output.end_inline_coq_block (); formatted := false;
if eol then
match indents with
| Some ls -> doc_list_bol ls lexbuf
| None -> doc_bol lexbuf
else doc indents lexbuf)}
| "[[[" nl
{ inf_rules indents lexbuf }
| "[]"
{ Output.proofbox (); doc indents lexbuf }
| "{{" { url lexbuf; doc indents lexbuf }
| "["
{ if !Cdglobals.plain_comments then Output.char '['
else (brackets := 1; Output.start_inline_coq (); escaped_coq lexbuf;
Output.end_inline_coq ()); doc indents lexbuf }
| "(*"
{ backtrack lexbuf ;
let bol_parse = match indents with
| Some is -> doc_list_bol is
| None -> doc_bol
in
let eol =
if !Cdglobals.parse_comments then comment lexbuf
else skipped_comment lexbuf in
if eol then bol_parse lexbuf else doc indents lexbuf }
| '*'* "*)" space_nl* "(**"
{(match indents with
| Some _ -> Output.stop_item ()
| None -> ());
(* this says - if there is a blank line between the two comments,
insert one in the output too *)
let lines = List.length (Str.split_delim (Str.regexp "['\n']")
(lexeme lexbuf))
in
if lines > 2 then Output.paragraph ();
doc_bol lexbuf
}
| '*'* "*)" space* nl
{ true }
| '*'* "*)"
{ false }
| "$"
{ if !Cdglobals.plain_comments then Output.char '$'
else (Output.start_latex_math (); escaped_math_latex lexbuf);
doc indents lexbuf }
| "$$"
{ if !Cdglobals.plain_comments then Output.char '$';
Output.char '$'; doc indents lexbuf }
| "%"
{ if !Cdglobals.plain_comments then Output.char '%'
else escaped_latex lexbuf; doc indents lexbuf }
| "%%"
{ if !Cdglobals.plain_comments then Output.char '%';
Output.char '%'; doc indents lexbuf }
| "#"
{ if !Cdglobals.plain_comments then Output.char '#'
else escaped_html lexbuf; doc indents lexbuf }
| "##"
{ if !Cdglobals.plain_comments then Output.char '#';
Output.char '#'; doc indents lexbuf }
| nonidentchar '_' nonidentchar
{ List.iter (fun x -> Output.char (lexeme_char lexbuf x)) [0;1;2];
doc indents lexbuf}
| nonidentchar '_'
{ Output.char (lexeme_char lexbuf 0);
if !Cdglobals.plain_comments then Output.char '_' else start_emph () ;
doc indents lexbuf }
| '_' nonidentchar
{ if !Cdglobals.plain_comments then Output.char '_' else stop_emph () ;
Output.char (lexeme_char lexbuf 1);
doc indents lexbuf }
| "<<" space*
{ Output.start_verbatim true; verbatim 0 true lexbuf; doc_bol lexbuf }
| '"'
{ if !Cdglobals.plain_comments
then Output.char '"'
else if in_quote ()
then stop_quote ()
else start_quote ();
doc indents lexbuf }
| eof
{ false }
| _
{ Output.char (lexeme_char lexbuf 0); doc indents lexbuf }
(*s Various escapings *)
and escaped_math_latex = parse
| "$" { Output.stop_latex_math () }
| eof { Output.stop_latex_math () }
| "*)"
{ Output.stop_latex_math (); backtrack lexbuf }
| _ { Output.latex_char (lexeme_char lexbuf 0); escaped_math_latex lexbuf }
and escaped_latex = parse
| "%" { () }
| eof { () }
| "*)"
{ backtrack lexbuf }
| _ { Output.latex_char (lexeme_char lexbuf 0); escaped_latex lexbuf }
and escaped_html = parse
| "#" { () }
| "&#"
{ Output.html_char '&'; Output.html_char '#'; escaped_html lexbuf }
| "##"
{ Output.html_char '#'; escaped_html lexbuf }
| eof { () }
| "*)"
{ backtrack lexbuf }
| _ { Output.html_char (lexeme_char lexbuf 0); escaped_html lexbuf }
and verbatim depth inline = parse
| nl ">>" space* nl { Output.verbatim_char inline '\n'; Output.stop_verbatim inline }
| nl ">>" { Output.verbatim_char inline '\n'; Output.stop_verbatim inline }
| ">>" { Output.stop_verbatim inline }
| "(*" { Output.verbatim_char inline '(';
Output.verbatim_char inline '*';
verbatim (depth+1) inline lexbuf }
| "*)" { if (depth == 0)
then (Output.stop_verbatim inline; backtrack lexbuf)
else (Output.verbatim_char inline '*';
Output.verbatim_char inline ')';
verbatim (depth-1) inline lexbuf) }
| eof { Output.stop_verbatim inline }
| _ { Output.verbatim_char inline (lexeme_char lexbuf 0); verbatim depth inline lexbuf }
and url = parse
| "}}" { Output.url (Buffer.contents url_buffer) None; Buffer.clear url_buffer }
| "}" { url_name lexbuf }
| _ { Buffer.add_char url_buffer (lexeme_char lexbuf 0); url lexbuf }
and url_name = parse
| "}" { Output.url (Buffer.contents url_buffer) (Some (Buffer.contents url_name_buffer));
Buffer.clear url_buffer; Buffer.clear url_name_buffer }
| _ { Buffer.add_char url_name_buffer (lexeme_char lexbuf 0); url_name lexbuf }
(*s Coq, inside quotations *)
and escaped_coq = parse
| "]"
{ decr brackets;
if !brackets > 0 then
(Output.sublexer_in_doc ']'; escaped_coq lexbuf)
else Tokens.flush_sublexer () }
| "["
{ incr brackets;
Output.sublexer_in_doc '['; escaped_coq lexbuf }
| "(*"
{ Tokens.flush_sublexer (); comment_level := 1;
ignore (if !Cdglobals.parse_comments then comment lexbuf
else skipped_comment lexbuf);
escaped_coq lexbuf }
| "*)"
{ (* likely to be a syntax error: we escape *) backtrack lexbuf }
| eof
{ Tokens.flush_sublexer () }
| identifier
{ Tokens.flush_sublexer();
Output.ident (lexeme lexbuf) None;
escaped_coq lexbuf }
| space_nl*
{ let str = lexeme lexbuf in
Tokens.flush_sublexer();
(if !Cdglobals.inline_notmono then ()
else Output.end_inline_coq ());
String.iter Output.char str;
(if !Cdglobals.inline_notmono then ()
else Output.start_inline_coq ());
escaped_coq lexbuf }
| _
{ Output.sublexer_in_doc (lexeme_char lexbuf 0);
escaped_coq lexbuf }
(*s Coq "Comments" command. *)
and comments = parse
| space_nl+
{ Output.char ' '; comments lexbuf }
| '"' [^ '"']* '"'
{ let s = lexeme lexbuf in
let s = String.sub s 1 (String.length s - 2) in
ignore (doc None (from_string s)); comments lexbuf }
| ([^ '.' '"'] | '.' [^ ' ' '\t' '\n'])+
{ escaped_coq (from_string (lexeme lexbuf)); comments lexbuf }
| "." (space_nl | eof)
{ () }
| eof
{ () }
| _
{ Output.char (lexeme_char lexbuf 0); comments lexbuf }
and skipped_comment = parse
| "(*"
{ incr comment_level;
skipped_comment lexbuf }
| "*)" space* nl
{ decr comment_level;
if !comment_level > 0 then skipped_comment lexbuf else true }
| "*)"
{ decr comment_level;
if !comment_level > 0 then skipped_comment lexbuf else false }
| eof { false }
| _ { skipped_comment lexbuf }
and comment = parse
| "(*"
{ incr comment_level;
Output.start_comment ();
comment lexbuf }
| "*)" space* nl
{ Output.end_comment ();
Output.line_break ();
decr comment_level;
if !comment_level > 0 then comment lexbuf else true }
| "*)"
{ Output.end_comment ();
decr comment_level;
if !comment_level > 0 then comment lexbuf else false }
| "["
{ if !Cdglobals.plain_comments then Output.char '['
else (brackets := 1; Output.start_inline_coq ();
escaped_coq lexbuf; Output.end_inline_coq ());
comment lexbuf }
| "[[" nl
{ if !Cdglobals.plain_comments then (Output.char '['; Output.char '[')
else (formatted := true;
Output.start_inline_coq_block ();
let _ = body_bol lexbuf in
Output.end_inline_coq_block (); formatted := false);
comment lexbuf }
| "$"
{ if !Cdglobals.plain_comments then Output.char '$'
else (Output.start_latex_math (); escaped_math_latex lexbuf);
comment lexbuf }
| "$$"
{ if !Cdglobals.plain_comments then Output.char '$';
Output.char '$';
comment lexbuf }
| "%"
{ if !Cdglobals.plain_comments then Output.char '%'
else escaped_latex lexbuf;
comment lexbuf }
| "%%"
{ if !Cdglobals.plain_comments then Output.char '%';
Output.char '%';
comment lexbuf }
| "#"
{ if !Cdglobals.plain_comments then Output.char '#'
else escaped_html lexbuf;
comment lexbuf }
| "##"
{ if !Cdglobals.plain_comments then Output.char '#';
Output.char '#';
comment lexbuf }
| eof { false }
| space+
{ Output.indentation (fst (count_spaces (lexeme lexbuf)));
comment lexbuf }
| nl
{ Output.line_break ();
comment lexbuf }
| _ { Output.char (lexeme_char lexbuf 0);
comment lexbuf }
and skip_to_dot = parse
| '.' space* nl { true }
| eof | '.' space+ { false }
| "(*"
{ comment_level := 1;
ignore (skipped_comment lexbuf);
skip_to_dot lexbuf }
| _ { skip_to_dot lexbuf }
and skip_to_dot_or_brace = parse
| '.' space* nl { true }
| eof | '.' space+ { false }
| "(*"
{ comment_level := 1;
ignore (skipped_comment lexbuf);
skip_to_dot_or_brace lexbuf }
| "}" space* nl
{ true }
| "}"
{ false }
| space*
{ skip_to_dot_or_brace lexbuf }
| _ { skip_to_dot lexbuf }
and body_bol = parse
| space+
{ Output.indentation (fst (count_spaces (lexeme lexbuf))); body lexbuf }
| _ { backtrack lexbuf; Output.indentation 0; body lexbuf }
and body = parse
| nl {Tokens.flush_sublexer(); Output.line_break(); Lexing.new_line lexbuf; body_bol lexbuf}
| nl+ space* "]]" space* nl
{ Tokens.flush_sublexer();
if not !formatted then
begin
let s = lexeme lexbuf in
let nlsp,s = remove_newline s in
let _,isp = count_spaces s in
let loc = lexeme_start lexbuf + nlsp + isp in
Output.sublexer ']' loc;
Output.sublexer ']' (loc+1);
Tokens.flush_sublexer();
body lexbuf
end
else
begin
Output.paragraph ();
true
end }
| "]]" space* nl
{ Tokens.flush_sublexer();
if not !formatted then
begin
let loc = lexeme_start lexbuf in
Output.sublexer ']' loc;
Output.sublexer ']' (loc+1);
Tokens.flush_sublexer();
Output.line_break();
body lexbuf
end
else
begin
Output.paragraph ();
true
end }
| eof { Tokens.flush_sublexer(); false }
| '.' space* nl | '.' space* eof
{ Tokens.flush_sublexer(); Output.char '.'; Output.line_break();
if not !formatted then true else body_bol lexbuf }
| '.' space* nl "]]" space* nl
{ Tokens.flush_sublexer(); Output.char '.';
if not !formatted then
begin
eprintf "Error: stray ]] at %d\n" (lexeme_start lexbuf);
flush stderr;
exit 1
end
else
begin
Output.paragraph ();
true
end
}
| '.' space+
{ Tokens.flush_sublexer(); Output.char '.'; Output.char ' ';
if not !formatted then false else body lexbuf }
| "(**" space_nl
{ Tokens.flush_sublexer(); Output.end_coq (); Output.start_doc ();
let eol = doc_bol lexbuf in
Output.end_doc (); Output.start_coq ();
if eol then body_bol lexbuf else body lexbuf }
| "(*"
{ Tokens.flush_sublexer(); comment_level := 1;
let eol =
if parse_comments () then begin
Output.start_comment ();
comment lexbuf
end else begin
let eol = skipped_comment lexbuf in
if eol then Output.line_break();
eol
end in
if eol then body_bol lexbuf else body lexbuf }
| "where"
{ Tokens.flush_sublexer();
Output.ident (lexeme lexbuf) None;
start_notation_string lexbuf }
| identifier
{ Tokens.flush_sublexer();
Output.ident (lexeme lexbuf) (Some (lexeme_start lexbuf));
body lexbuf }
| ".."
{ Tokens.flush_sublexer(); Output.char '.'; Output.char '.';
body lexbuf }
| '"'
{ Tokens.flush_sublexer(); Output.char '"';
string lexbuf;
body lexbuf }
| space
{ Tokens.flush_sublexer(); Output.char (lexeme_char lexbuf 0);
body lexbuf }
| _ { let c = lexeme_char lexbuf 0 in
Output.sublexer c (lexeme_start lexbuf);
body lexbuf }
and start_notation_string = parse
| space { Tokens.flush_sublexer(); Output.char (lexeme_char lexbuf 0);
start_notation_string lexbuf }
| '"' (* a true notation *)
{ Output.sublexer '"' (lexeme_start lexbuf);
notation_string lexbuf;
body lexbuf }
| _ (* an abbreviation *)
{ backtrack lexbuf; body lexbuf }
and notation_string = parse
| "\"\""
{ Output.char '"'; Output.char '"'; (* Unlikely! *)
notation_string lexbuf }
| '"'
{ Tokens.flush_sublexer(); Output.char '"' }
| _ { let c = lexeme_char lexbuf 0 in
Output.sublexer c (lexeme_start lexbuf);
notation_string lexbuf }
and string = parse
| "\"\"" { Output.char '"'; Output.char '"'; string lexbuf }
| '"' { Output.char '"' }
| _ { let c = lexeme_char lexbuf 0 in Output.char c; string lexbuf }
and skip_hide = parse
| eof | end_hide { () }
| _ { skip_hide lexbuf }
(*s Reading token pretty-print *)
and printing_token_body = parse
| "*)" nl? | eof
{ let s = Buffer.contents token_buffer in
Buffer.clear token_buffer;
s }
| _ { Buffer.add_string token_buffer (lexeme lexbuf);
printing_token_body lexbuf }
(*s These handle inference rules, parsing the body segments of things
enclosed in [[[ ]]] brackets *)
and inf_rules indents = parse
| space* nl (* blank line, before or between definitions *)
{ inf_rules indents lexbuf }
| "]]]" nl (* end of the inference rules block *)
{ match indents with
| Some ls -> doc_list_bol ls lexbuf
| None -> doc_bol lexbuf }
| _
{ backtrack lexbuf; (* anything else must be the first line in a rule *)
inf_rules_assumptions indents [] lexbuf}
(* The inference rule parsing just collects the inference rule and then
calls the output function once, instead of doing things incrementally
like the rest of the lexer. If only there were a real parsing phase...
*)
and inf_rules_assumptions indents assumptions = parse
| space* "---" '-'* [^ '\n']* nl (* hit the horizontal line *)
{ let line = lexeme lexbuf in
let (spaces,_) = count_spaces line in
let dashes_and_name =
cut_head_tail_spaces (String.sub line 0 (String.length line - 1))
in
let ldn = String.length dashes_and_name in
let (dashes,name) =
try (let i = String.index dashes_and_name ' ' in
let d = String.sub dashes_and_name 0 i in
let n = cut_head_tail_spaces
(String.sub dashes_and_name (i+1) (ldn-i-1))
in
(d, Some n))
with _ -> (dashes_and_name, None)
in
inf_rules_conclusion indents (List.rev assumptions)
(spaces, dashes, name) [] lexbuf }
| [^ '\n']* nl (* if it's not the horizontal line, it's an assumption *)
{ let line = lexeme lexbuf in
let (spaces,_) = count_spaces line in
let assumption = cut_head_tail_spaces
(String.sub line 0 (String.length line - 1))
in
inf_rules_assumptions indents ((spaces,assumption)::assumptions)
lexbuf }
(*s The conclusion is required to come immediately after the
horizontal bar. It is allowed to contain multiple lines of
text, like the assumptions. The conclusion ends when we spot a
blank line or a ']]]'. *)
and inf_rules_conclusion indents assumptions middle conclusions = parse
| space* nl | space* "]]]" nl (* end of conclusions. *)
{ backtrack lexbuf;
Output.inf_rule assumptions middle (List.rev conclusions);
inf_rules indents lexbuf }
| space* [^ '\n']+ nl (* this is a line in the conclusion *)
{ let line = lexeme lexbuf in
let (spaces,_) = count_spaces line in
let conc = cut_head_tail_spaces (String.sub line 0
(String.length line - 1))
in
inf_rules_conclusion indents assumptions middle
((spaces,conc) :: conclusions) lexbuf
}
(*s A small scanner to support the chapter subtitle feature *)
and st_start m = parse
| "(*" "*"+ space+ "*" space+
{ st_modname m lexbuf }
| _
{ None }
and st_modname m = parse
| identifier space* ":" space*
{ if subtitle m (lexeme lexbuf) then
st_subtitle lexbuf
else
None
}
| _
{ None }
and st_subtitle = parse
| [^ '\n']* '\n'
{ let st = lexeme lexbuf in
let i = try Str.search_forward (Str.regexp "\\**)") st 0 with
Not_found ->
(eprintf "unterminated comment at beginning of file\n";
exit 1)
in
Some (cut_head_tail_spaces (String.sub st 0 i))
}
| _
{ None }
(*s Applying the scanners to files *)
{
let coq_file f m =
reset ();
let c = open_in f in
let lb = from_channel c in
(Index.current_library := m;
Output.initialize ();
Output.start_module ();
Output.start_coq (); coq_bol lb; Output.end_coq ();
close_in c)
let detect_subtitle f m =
let c = open_in f in
let lb = from_channel c in
let sub = st_start m lb in
close_in c;
sub
}
¤ Dauer der Verarbeitung: 0.166 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
