package dolmen
A parser library for automated deduction
Install
Dune Dependency
Authors
Maintainers
Sources
dolmen-0.8.1.tbz
sha256=80fc33ae81817a79c6e6b2f6c01c4cfcc0af02bfe4d2d1b87cf70b84cdde3928
sha512=3a44a99bce871161bc70cf909c813e9e6c91c590873cbc163c69b2ec90ab5be65bf0bf45430bc8d00d85d75cf0af004b06b8f5f1c9d4d47c8a30ab9f28762c04
doc/src/dolmen.std/transformer.ml.html
Source file transformer.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
(* This file is free software, part of dolmen. See file "LICENSE" formore information *) module Make (Loc : Loc.S) (Ty : sig type token type statement val env : string list val incremental : bool val error : int -> string end) (Lex : Dolmen_intf.Lex.S with type token := Ty.token) (Parse : Dolmen_intf.Parse.S with type token := Ty.token and type statement := Ty.statement) = struct (* Module Includes --------------- *) include Ty module Lexer = Lex module Parser = Parse (* Finding include files --------------------- *) let rec find_env file = function | [] -> None | var :: r -> begin match Sys.getenv var with | dir -> let f = Filename.concat dir file in if Sys.file_exists f then Some f else find_env file r | exception Not_found -> find_env file r end let find ?(dir="") file = if Filename.is_relative file then begin let f = Filename.concat dir file in if Sys.file_exists f then Some f else find_env file Ty.env end else if Sys.file_exists file then Some file else None (* Menhir state & checkpoint manipulations --------------------------------------- *) let error_message token s = match token with | None -> `Regular (Format.dprintf "Syntax error@ with@ missing@ token@ read,@ \ please@ report upstream,@ ^^") | Some tok -> let tok_descr = Lexer.descr tok in begin match String.trim (Ty.error s) with | exception Not_found -> `Regular (Format.dprintf "Missing@ syntax@ error@ message@ \ (state %d),@ please@ report@ \ upstream,@ ^^" s) | "<YOUR SYNTAX ERROR MESSAGE HERE>" -> `Regular (Format.dprintf "Syntax error (state %d)@ \ while reading %a." s Tok.print tok_descr) | msg -> begin match Misc.split_on_char '\n' msg with | error_ref :: production :: l -> let prod = Format.dprintf "%s" production in let lexed = Format.dprintf "%a" Tok.print tok_descr in let expected = Format.dprintf "%a" Format.pp_print_text (String.concat " " l) in `Advanced (error_ref, prod, lexed, expected) | _ -> `Regular (Format.dprintf "Syntax error (state %d)." s) end end (* Parsing loop ------------ *) let parse_aux ~k_exn newline sync lexbuf parser_fun = (* Token supplier *) let last_token = ref None in let lexer lexbuf = let token = Lexer.token newline lexbuf in last_token := Some token; token in (* Run the loop *) let aux () = begin match parser_fun lexer lexbuf with | res -> let () = sync lexbuf in res | exception (((Loc.Syntax_error _) | (Loc.Lexing_error _)) as e) -> let () = sync lexbuf in let () = k_exn () in raise e | exception Lexer.Error -> let pos = Loc.of_lexbuf lexbuf in let err = Lexing.lexeme lexbuf in let () = sync lexbuf in let () = k_exn () in raise (Loc.Lexing_error (pos, err)) | exception Parser.Error state -> let pos = Loc.of_lexbuf lexbuf in let msg = error_message !last_token state in let () = sync lexbuf in let () = k_exn () in raise (Loc.Syntax_error (pos, msg)) | exception e -> let bt = Printexc.get_raw_backtrace () in let pos = Loc.of_lexbuf lexbuf in let () = sync lexbuf in let () = k_exn () in raise (Loc.Uncaught (pos, e, bt)) end in aux (* Instantiations of the parsing loop ---------------------------------- *) let parse_file file = let lexbuf, cleanup = Misc.mk_lexbuf (`File file) in let locfile = Loc.mk_file file in let newline = Loc.newline locfile in let sync = Loc.update_size locfile in let k_exn () = cleanup () in let res = parse_aux ~k_exn newline sync lexbuf Parser.file () in let () = cleanup () in locfile, res let parse_file_lazy file = let lexbuf, cleanup = Misc.mk_lexbuf (`File file) in let locfile = Loc.mk_file file in let newline = Loc.newline locfile in let sync = Loc.update_size locfile in let k_exn () = cleanup () in let res = lazy ( let res = parse_aux ~k_exn newline sync lexbuf Parser.file () in let () = cleanup () in res ) in locfile, res let parse_raw_lazy ~filename contents = let lexbuf, cleanup = Misc.mk_lexbuf (`Contents (filename, contents)) in let locfile = Loc.mk_file filename in let newline = Loc.newline locfile in let sync = Loc.update_size locfile in let k_exn () = cleanup () in let res = lazy ( let res = parse_aux ~k_exn newline sync lexbuf Parser.file () in let () = cleanup () in res ) in locfile, res let parse_input i = let lexbuf, cleanup = Misc.mk_lexbuf i in let locfile = Loc.mk_file (Misc.filename_of_input i) in let newline = Loc.newline locfile in let sync = Loc.update_size locfile in if not Ty.incremental then begin (* If incremental mode is not supported, raise an error rather than do weird things. *) let msg = Format.dprintf ": @[<hov>%a@]" Format.pp_print_text "Input format does not support incremental parsing" in raise (Loc.Syntax_error (Loc.of_lexbuf lexbuf, `Regular msg)) end; let k_exn () = Dolmen_line.consume ~newline ~sync lexbuf in let aux = parse_aux ~k_exn newline sync lexbuf Parser.input in locfile, aux, cleanup end
sectionYPositions = computeSectionYPositions($el), 10)"
x-init="setTimeout(() => sectionYPositions = computeSectionYPositions($el), 10)"
>