https://github.com/EasyCrypt/easycrypt
Revision fe76f3396562618bbee795ea7032cdb29714100e authored by Benjamin Gregoire on 14 December 2017, 10:37:55 UTC, committed by Benjamin Gregoire on 14 December 2017, 10:37:55 UTC
1 parent 527d9ad
Raw File
Tip revision: fe76f3396562618bbee795ea7032cdb29714100e authored by Benjamin Gregoire on 14 December 2017, 10:37:55 UTC
more lemmas on FSet.oflist
Tip revision: fe76f33
ecIo.mli
(* --------------------------------------------------------------------
 * Copyright (c) - 2012--2016 - IMDEA Software Institute
 * Copyright (c) - 2012--2017 - Inria
 *
 * Distributed under the terms of the CeCILL-C-V1 license
 * -------------------------------------------------------------------- *)

(* -------------------------------------------------------------------- *)
type ecreader

(* -------------------------------------------------------------------- *)
val from_channel : name:string -> in_channel -> ecreader
val from_file    : string -> ecreader
val from_string  : string -> ecreader

(* -------------------------------------------------------------------- *)
val finalize : ecreader -> unit
val parse    : ecreader -> EcParsetree.prog
val parseall : ecreader -> EcParsetree.global list
val drain    : ecreader -> unit
val lexbuf   : ecreader -> Lexing.lexbuf

(* -------------------------------------------------------------------- *)
val lex_single_token : string -> EcParser.token option
val is_sym_ident : string -> bool
val is_mem_ident : string -> bool
val is_mod_ident : string -> bool

(* -------------------------------------------------------------------- *)
val is_binop     : string -> [`Yes | `No | `Invalid]
val is_uniop     : string -> [`Yes | `No | `Invalid]
back to top