Revision e12e2c2f2d80489ea5981a51f4362c947b05079d authored by Pierre-Yves Strub on 14 October 2019, 08:38:48 UTC, committed by Pierre-Yves Strub on 14 October 2019, 08:39:46 UTC
- call by value reduction strategy. - user defined reduction rules. Co-authored-by: Pierre-Yves Strub <pierre-yves@strub.nu> Co-authored-by: Benjamin Gregoire <benjamin.gregoire@inria.fr>
1 parent 651df3f
ecIo.ml
(* --------------------------------------------------------------------
* Copyright (c) - 2012--2016 - IMDEA Software Institute
* Copyright (c) - 2012--2018 - Inria
* Copyright (c) - 2012--2018 - Ecole Polytechnique
*
* Distributed under the terms of the CeCILL-C-V1 license
* -------------------------------------------------------------------- *)
(* -------------------------------------------------------------------- *)
open EcUtils
module P = EcParser
module L = Lexing
(* -------------------------------------------------------------------- *)
let lexbuf_from_channel = fun name channel ->
let lexbuf = Lexing.from_channel channel in
lexbuf.Lexing.lex_curr_p <- {
Lexing.pos_fname = name;
Lexing.pos_lnum = 1;
Lexing.pos_bol = 0;
Lexing.pos_cnum = 0
};
lexbuf
(* -------------------------------------------------------------------- *)
let parserfun = fun () ->
MenhirLib.Convert.Simplified.traditional2revised EcParser.prog
type 'a parser_t =
(P.token * L.position * L.position, 'a) MenhirLib.Convert.revised
(* -------------------------------------------------------------------- *)
let isbinop_fun = fun () ->
MenhirLib.Convert.Simplified.traditional2revised EcParser.is_binop
let isuniop_fun = fun () ->
MenhirLib.Convert.Simplified.traditional2revised EcParser.is_uniop
(* -------------------------------------------------------------------- *)
type 'a ecreader_gr = {
(*---*) ecr_lexbuf : Lexing.lexbuf;
(*---*) ecr_parser : 'a parser_t;
mutable ecr_tokens : EcParser.token list;
mutable ecr_atstart : bool;
}
type 'a ecreader_g = 'a ecreader_gr Disposable.t
type ecreader = EcParsetree.prog ecreader_g
(* -------------------------------------------------------------------- *)
let lexbuf (reader : 'a ecreader_g) =
(Disposable.get reader).ecr_lexbuf
(* -------------------------------------------------------------------- *)
let from_channel ~name channel =
let lexbuf = lexbuf_from_channel name channel in
Disposable.create
{ ecr_lexbuf = lexbuf;
ecr_parser = parserfun ();
ecr_atstart = true;
ecr_tokens = []; }
(* -------------------------------------------------------------------- *)
let from_file filename =
let channel = open_in filename in
try
let lexbuf = lexbuf_from_channel filename channel in
Disposable.create ~cb:(fun _ -> close_in channel)
{ ecr_lexbuf = lexbuf;
ecr_parser = parserfun ();
ecr_atstart = true;
ecr_tokens = []; }
with
| e ->
(try close_in channel with _ -> ());
raise e
(* -------------------------------------------------------------------- *)
let from_string data =
let lexbuf = Lexing.from_string data in
Disposable.create
{ ecr_lexbuf = lexbuf;
ecr_parser = parserfun ();
ecr_atstart = true;
ecr_tokens = []; }
(* -------------------------------------------------------------------- *)
let finalize (ecreader : 'a ecreader_g) =
Disposable.dispose ecreader
(* -------------------------------------------------------------------- *)
let lexer = fun ecreader ->
let lexbuf = ecreader.ecr_lexbuf in
if ecreader.ecr_tokens = [] then
ecreader.ecr_tokens <- EcLexer.main lexbuf;
match ecreader.ecr_tokens with
| [] ->
failwith "short-read-from-lexer"
| token :: queue -> begin
ecreader.ecr_tokens <- queue;
ecreader.ecr_atstart <- (token = EcParser.FINAL);
(token, Lexing.lexeme_start_p lexbuf, Lexing.lexeme_end_p lexbuf)
end
(* -------------------------------------------------------------------- *)
let drain (ecreader : 'a ecreader_g) =
let ecreader = Disposable.get ecreader in
let rec drain () =
try
match lexer ecreader with
| (EcParser.FINAL, _, _) -> ()
| _ -> drain ()
with EcLexer.LexicalError _ -> drain ()
in
if not ecreader.ecr_atstart then
drain ()
(* -------------------------------------------------------------------- *)
let parse (ecreader : 'a ecreader_g) =
let ecreader = Disposable.get ecreader in
ecreader.ecr_parser (fun () -> lexer ecreader)
(* -------------------------------------------------------------------- *)
let parseall (ecreader : 'a ecreader_g) =
let rec aux acc =
match EcLocation.unloc (parse ecreader) with
| EcParsetree.P_Prog (commands, terminate) ->
let acc = List.rev_append commands acc in
if terminate then List.rev acc else aux acc
| EcParsetree.P_Undo _ ->
assert false (* FIXME *)
in
aux []
(* -------------------------------------------------------------------- *)
let lex_single_token name =
try
let ecr =
{ ecr_lexbuf = Lexing.from_string name;
ecr_parser = parserfun ();
ecr_atstart = true;
ecr_tokens = []; } in
let (token, _, _) = lexer ecr in
match lexer ecr with
| (EcParser.EOF, _, _) -> Some token
| _ -> None
with EcLexer.LexicalError _ -> None
(* -------------------------------------------------------------------- *)
let is_sym_ident x =
match lex_single_token x with
| Some (EcParser.LIDENT _) -> true
| Some (EcParser.UIDENT _) -> true
| _ -> false
let is_op_ident x =
match lex_single_token x with
| Some (EcParser.LIDENT _) -> true
| Some (EcParser.UIDENT _) -> true
| Some (EcParser.NOP _) -> true
| _ -> false
let is_mem_ident x =
match lex_single_token x with
| Some (EcParser.MIDENT _) -> true
| _ -> false
let is_mod_ident x =
match lex_single_token x with
| Some (EcParser.UIDENT _) -> true
| _ -> false
(* -------------------------------------------------------------------- *)
type lexer1 = {
(*---*) l1_lexbuf : Lexing.lexbuf;
mutable l1_buffer : EcParser.token list;
}
let lexer1_of_lexbuf (lexbuf : Lexing.lexbuf) =
{ l1_lexbuf = lexbuf; l1_buffer = []; }
let lexer1 (lexbuf : lexer1) =
if lexbuf.l1_buffer = [] then
lexbuf.l1_buffer <- EcLexer.main lexbuf.l1_lexbuf;
match lexbuf.l1_buffer with
| [] ->
failwith "short-read-from-lexer"
| token :: queue ->
lexbuf.l1_buffer <- queue;
(token,
Lexing.lexeme_start_p lexbuf.l1_lexbuf,
Lexing.lexeme_end_p lexbuf.l1_lexbuf)
(* -------------------------------------------------------------------- *)
let is_uniop (x : string) =
match lex_single_token x with
| Some (EcParser.PUNIOP x) -> begin
try
let x =
EcRegexp.exec (`S "^\\[(.+)\\]$") x
|> omap (fun m -> oget (EcRegexp.Match.group m 1))
|> odfl x
in
let parse = isuniop_fun () in
let lexbuf = lexer1_of_lexbuf (Lexing.from_string x) in
parse (fun () -> lexer1 lexbuf); `Yes
with EcLexer.LexicalError _ | EcParser.Error -> `Invalid
end
| _ -> `No
(* -------------------------------------------------------------------- *)
let is_binop (x : string) =
match lex_single_token x with
| Some (EcParser.PBINOP x) -> begin
try
let parse = isbinop_fun () in
let lexbuf = lexer1_of_lexbuf (Lexing.from_string x) in
parse (fun () -> lexer1 lexbuf); `Yes
with EcLexer.LexicalError _ | EcParser.Error -> `Invalid
end
| _ -> `No
![swh spinner](/static/img/swh-spinner.gif)
Computing file changes ...