plugins/microc/mc_lexer.mli

   1 (********************************************************************)
   2 (*                                                                  *)
   3 (*  The Why3 Verification Platform   /   The Why3 Development Team  *)
   4 (*  Copyright 2010-2023 --  Inria - CNRS - Paris-Saclay University  *)
   5 (*                                                                  *)
   6 (*  This software is distributed under the terms of the GNU Lesser  *)
   7 (*  General Public License version 2.1, with the special exception  *)
   8 (*  on linking described in file LICENSE.                           *)
   9 (*                                                                  *)
  10 (********************************************************************)
  11
  12 val parse : string -> in_channel -> Mc_ast.file
  13 val parse_term : Lexing.lexbuf -> Why3.Ptree.term
  14 val parse_term_list : Lexing.lexbuf -> Why3.Ptree.term list
  15 val parse_list_ident : Lexing.lexbuf -> Why3.Ptree.ident list