plugins/tptp/tptp_lexer.mli

   1 (********************************************************************)
   2 (*                                                                  *)
   3 (*  The Why3 Verification Platform   /   The Why3 Development Team  *)
   4 (*  Copyright 2010-2024 --  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 exception FileNotFound of string
  13
  14 val load: string -> Tptp_ast.tptp_file
  15 (** [load filename] loads and parses the file named [filename]. It
  16     also expands other included files in that file. As specified by
  17     the TPTP standard
  18     (http://www.cs.miami.edu/~tptp/TPTP/TR/TPTPTR.shtml), files
  19     included with relative path names are searched first under the
  20     directory of the main file, and if not found there then searched
  21     under the directory specified in the $TPTP environment variable.
  22
  23     If the file, or one of its included file, is not found in the
  24     file system, then exception [FileNotFound s] is raised, where
  25     [s] is the name of the file not found.  *)