Commit de7a7a6e authored by MARCHE Claude's avatar MARCHE Claude

TPTP parsing: added a load function that expands the includes

parent d36beb56
......@@ -9,4 +9,17 @@
(* *)
(********************************************************************)
val parse: in_channel -> Tptp_ast.tptp_file
exception FileNotFound of string
val load: string -> Tptp_ast.tptp_file
(** [load filename] loads and parses the file named [filename]. It
also expands other included files in that file. As specified by
the TPTP standard
(http://www.cs.miami.edu/~tptp/TPTP/TR/TPTPTR.shtml), files
included with relative path names are searched first under the
directory of the main file, and if not found there then searched
under the directory specified in the $TPTP environment variable.
If the file, or one of its included file, is not found in the
file system, then exception [FileNotFound s] is raised, where
[s] is the name of the file not found. *)
......@@ -238,13 +238,50 @@ and comment_line = parse
{
let parse c =
let lb = Lexing.from_channel c in Loc.with_location (tptp_file token) lb
let parse file c =
let lb = Lexing.from_channel c in
Loc.set_file file lb;
Loc.with_location (tptp_file token) lb
exception FileNotFound of string
let load file =
let dir = Filename.dirname file in
let tptplib =
try Some (Sys.getenv "TPTP")
with Not_found -> None
in
let rec aux file =
let ch,file =
try (open_in file, file)
with Sys_error _ ->
if not (Filename.is_relative file) then raise (FileNotFound file) else
try let f = Filename.concat dir file in (open_in f,f)
with Sys_error _ ->
match tptplib with
| None ->
raise (FileNotFound (file ^ " (warning: $TPTP was not set)"))
| Some d ->
try let f = Filename.concat d file in (open_in f,f)
with Sys_error _ -> raise (FileNotFound file)
in
let ast = parse file ch in
close_in ch;
let ast =
List.fold_left
(fun acc d ->
match d with
| Formula _ -> d::acc
| Include(file,_,_) ->
let fn = String.sub file 1 (String.length file - 2) in
let ast = aux fn in
List.rev_append ast acc)
[] ast
in List.rev ast
in aux file
let read_channel env path file c =
let lb = Lexing.from_channel c in
Loc.set_file file lb;
let ast = Loc.with_location (tptp_file token) lb in
let ast = parse file c in
Tptp_typing.typecheck env path ast
let () = Env.register_format Env.base_language "tptp" ["p";"ax"] read_channel
......
......@@ -67,31 +67,69 @@ let pr_decl fmt d =
let pr_file fmt a =
Pp.print_list Pp.newline pr_decl fmt a
let rec load file =
let ch = open_in file in
let ast = Tptp_lexer.parse ch in
close_in ch;
let ast =
List.fold_left
(fun acc d ->
match d with
| Formula _ -> d::acc
| Include(file,_,_) ->
let fn = String.sub file 1 (String.length file - 2) in
let ast = load fn in
List.rev_append ast acc)
[] ast
in List.rev ast
exception Unsupported of string
let unsupported s = raise (Unsupported s)
let check_op op =
match op with
| BOequ -> unsupported "BOequ"
| BOnequ -> unsupported "BOnequ"
| BOimp -> ()
| BOpmi -> unsupported "BOpmi"
| BOand -> ()
| BOor -> ()
| BOnand -> ()
| BOnor -> ()
let rec check_expr e = match e.e_node with
| Elet(e1,e2) -> unsupported "let"
| Eite(e1,e2,e3) -> unsupported "ite"
| Eqnt(q,vl,e) -> unsupported "qnt"
| Ebin(op,e1,e2) -> check_op op; check_expr e1; check_expr e2
| Enot e -> check_expr e
| Eequ(e1,e2) -> unsupported "equ"
| Eapp(w,el) -> List.iter check_expr el
| Edef(w,el) -> unsupported "def"
| Evar v -> ()
| Edob d -> unsupported "dob"
| Enum n -> unsupported "num"
let check_top_formula f =
match f with
| LogicFormula e -> check_expr e
| TypedAtom _ -> unsupported "TypedAtom"
| Sequent _ -> unsupported "Sequent"
let check_role _r = ()
let check_kind k =
match k with
| TFF -> unsupported "TFF"
| FOF -> ()
| CNF -> ()
let check_decl d =
match d with
| Include _ -> unsupported "Include"
| Formula(kind,_,role,top_formula,_) ->
check_kind kind; check_role role; check_top_formula top_formula
let check_file a = List.iter check_decl a
let () =
if Array.length Sys.argv <> 2 then
eprintf "Usage: %s <file>@." Sys.argv.(0)
else
let file = Sys.argv.(1) in
try
let ast = load Sys.argv.(1) in
let ast = Tptp_lexer.load file in
check_file ast;
printf "%a@." pr_file ast
with e ->
with
| Tptp_lexer.FileNotFound f -> eprintf "File not found: %s@." f
| Unsupported s -> eprintf "File %s: '%s' is not supported@." file s
| e ->
eprintf "Parsing error: %a@." Exn_printer.exn_printer e
(*
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment