Something went wrong. Try again.
forked from gbury/dolmen
Something went wrong. Try again.
123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159160161162163164165166167168169170171172173174175176177178179180181182183184185186187188189190191192193194195196
(* This file is free software, part of dolmen. See file "LICENSE" for more information *)
module type S = sig
type file type statement exception Extension_not_found of string
type language = | Alt_ergo | Dimacs | ICNF | Smtlib2 of Dolmen_smtlib2.Script.version | Tptp of Dolmen_tptp.version | Zf
val enum : (string * language) list val string_of_language : language -> string
val find : ?language:language -> ?dir:string -> string -> string option val parse_all : ?language:language -> [< `File of string | `Stdin of language | `Raw of string * language * string ] -> language * file * statement list Lazy.t val parse_input : ?language:language -> [< `File of string | `Stdin of language | `Raw of string * language * string ] -> language * file * (unit -> statement option) * (unit -> unit)
module type S = Dolmen_intf.Language.S with type statement := statement and type file := file
val of_language : language -> language * string * (module S) val of_extension : string -> language * string * (module S) val of_filename : string -> language * string * (module S)
end
module Make (L : Dolmen_intf.Location.S) (I : Dolmen_intf.Id.Logic) (T : Dolmen_intf.Term.Logic with type location := L.t and type id := I.t) (S : Dolmen_intf.Stmt.Logic with type location := L.t and type id := I.t and type term := T.t) (E : Dolmen_intf.Ext.Logic with type location := L.t and type term := T.t and type statement := S.t) : S with type file := L.file and type statement := S.t= struct
exception Extension_not_found of string
module type S = Dolmen_intf.Language.S with type statement := S.t and type file := L.file
type language = | Alt_ergo | Dimacs | ICNF | Smtlib2 of Dolmen_smtlib2.Script.version | Tptp of Dolmen_tptp.version | Zf
let enum = [ "ae", Alt_ergo; "dimacs", Dimacs; "iCNF", ICNF; "smt2", Smtlib2 `Latest; "smt2.6", Smtlib2 `V2_6; "smt2.7", Smtlib2 `V2_7; "psmt2", Smtlib2 `Poly; "tptp", Tptp `Latest; "tptp-6.3.0", Tptp `V6_3_0; "zf", Zf; ]
let string_of_language l = fst (List.find (fun (_, l') -> l = l') enum)
let assoc = [
(* Alt-ergo format *) Alt_ergo, ".ae", (module Dolmen_ae.Make(L)(I)(T)(S) : S);
(* Dimacs *) Dimacs, ".cnf", (module Dolmen_dimacs.Make(L)(T)(S) : S);
(* iCNF *) ICNF, ".icnf", (module Dolmen_icnf.Make(L)(T)(S) : S);
(* Smtlib2 *) Smtlib2 `Latest, ".smt2", (module Dolmen_smtlib2.Script.Latest.Make(L)(I)(T)(S)(E.Smtlib2) : S); Smtlib2 `V2_6, ".smt2", (module Dolmen_smtlib2.Script.V2_6.Make(L)(I)(T)(S)(E.Smtlib2) : S); Smtlib2 `V2_7, ".smt2", (module Dolmen_smtlib2.Script.V2_7.Make(L)(I)(T)(S)(E.Smtlib2) : S); Smtlib2 `Poly, ".psmt2", (module Dolmen_smtlib2.Script.Poly.Make(L)(I)(T)(S)(E.Smtlib2) : S);
(* TPTP *) Tptp `Latest, ".p", (module Dolmen_tptp.Latest.Make(L)(I)(T)(S) : S); Tptp `V6_3_0, ".p", (module Dolmen_tptp.V6_3_0.Make(L)(I)(T)(S) : S);
(* Zipperposition format *) Zf, ".zf", (module Dolmen_zf.Make(L)(I)(T)(S) : S); ]
let of_language l = List.find (fun (l', _, _) -> l = l') assoc
let of_extension ext = try List.find (fun (_, ext', _) -> ext = ext') assoc with Not_found -> raise (Extension_not_found ext)
let of_filename s = of_extension (Dolmen_std.Misc.get_extension s)
let find ?language ?(dir="") file = match language with | None -> let f = if Filename.is_relative file then Filename.concat dir file else file in if Sys.file_exists f then Some f else None | Some l -> let _, _, (module P : S) = of_language l in P.find ~dir file
let parse_all ?language = function | `File file -> let l, _, (module P : S) = match language with | None -> of_filename file | Some l -> of_language l in let locfile, res = P.parse_all (`File file) in l, locfile, res | `Raw (filename, l, s) -> let l, _, (module P : S) = match language with | None -> of_language l | Some lang -> of_language lang in let locfile, res = P.parse_all (`Contents (filename, s)) in l, locfile, res | `Stdin l -> let l, _, (module P : S) = match language with | None -> of_language l | Some lang -> of_language lang in let locfile, res = P.parse_all `Stdin in l, locfile, res
let parse_input ?language = function | `File file -> let l, _, (module P : S) = match language with | Some l -> of_language l | None -> of_extension (Dolmen_std.Misc.get_extension file) in let locfile, gen, cl = P.parse_input (`File file) in l, locfile, gen, cl | `Stdin l -> let l, _, (module P : S) = of_language (match language with | Some l' -> l' | None -> l) in let locfile, gen, cl = P.parse_input `Stdin in l, locfile, gen, cl | `Raw (filename, l, s) -> let _, _, (module P : S) = of_language (match language with | Some l' -> l' | None -> l) in let locfile, gen, cl = P.parse_input (`Contents (filename, s)) in l, locfile, gen, cl
end