Une MAJ de sécurité est nécessaire sur notre version actuelle. Elle sera effectuée lundi 02/08 entre 12h30 et 13h. L'interruption de service devrait durer quelques minutes (probablement moins de 5 minutes).

Commit d9240dd6 authored by Andrei Paskevich's avatar Andrei Paskevich
Browse files

start TPTP typechecking

parent 18171354
......@@ -257,7 +257,7 @@ PLUGGENERATED = plugins/tptp/tptp_lexer.ml \
PLUG_PARSER = genequlin
PLUG_PRINTER = tptpfof
PLUG_TRANSFORM =
PLUG_TPTP = tptp_ast tptp_parser tptp_lexer
PLUG_TPTP = tptp_ast tptp_parser tptp_typing tptp_lexer
PLUGINS = genequlin tptpfof tptp
......
......@@ -94,8 +94,7 @@ type file = string
type role =
| Axiom | Hypothesis | Definition | Assumption
| Lemma | Theorem | Conjecture | Negated_conjecture
| Type | Unknown of string
| Lemma | Theorem | Conjecture | Negated_conjecture | Type
type input =
| Formula of kind * name * role * top_formula * loc
......
......@@ -22,7 +22,7 @@
open Lexing
open Tptp_ast
open Tptp_parser
(* open Tptp_typing *)
open Tptp_typing
open Why3
......@@ -250,8 +250,7 @@ and comment_line = parse
let lb = Lexing.from_channel c in
Loc.set_file file lb;
let ast = with_location (tptp_file token) lb in
(* tptp_typing env path ast *)
Util.Mstr.empty
Tptp_typing.typecheck env path ast
let () = Env.register_format "tptp" ["p";"ax"] read_channel
}
......
......@@ -325,8 +325,25 @@ number:
;
atomic_word:
| LWORD { $1 }
| SINGLE_QUOTED { $1 }
| LWORD { $1 }
| SINGLE_QUOTED { $1 }
| reserved_word { $1 }
;
reserved_word:
| ASSUMPTION { "assumption" }
| AXIOM { "axiom" }
| CNF { "cnf" }
| CONJECTURE { "conjecture" }
| DEFINITION { "definition" }
| FOF { "fof" }
| HYPOTHESIS { "hypothesis" }
| INCLUDE { "include" }
| LEMMA { "lemma" }
| NEGATED_CONJECTURE { "negated_conjecture" }
| TFF { "tff" }
| THEOREM { "theorem" }
| TYPE { "type" }
;
/* TODO: add support for annotations */
......
(**************************************************************************)
(* *)
(* Copyright (C) 2010-2011 *)
(* François Bobot *)
(* Jean-Christophe Filliâtre *)
(* Claude Marché *)
(* Andrei Paskevich *)
(* *)
(* This software is free software; you can redistribute it and/or *)
(* modify it under the terms of the GNU Library General Public *)
(* License version 2.1, with the special exception on linking *)
(* described in file LICENSE. *)
(* *)
(* This software is distributed in the hope that it will be useful, *)
(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. *)
(* *)
(**************************************************************************)
open Why3
open Util
open Ident
open Ty
open Term
open Decl
open Theory
type symbol =
| STVar of tvsymbol
| SVar of vsymbol
| SType of tysymbol
| SFunc of lsymbol
| SPred of lsymbol
| SletF of tvsymbol list * vsymbol list * term
| SletP of tvsymbol list * vsymbol list * term
type env = symbol Mstr.t
type implicit = (string,symbol) Hashtbl.t
let typecheck _env _path _ast = Mstr.empty
(**************************************************************************)
(* *)
(* Copyright (C) 2010-2011 *)
(* François Bobot *)
(* Jean-Christophe Filliâtre *)
(* Claude Marché *)
(* Andrei Paskevich *)
(* *)
(* This software is free software; you can redistribute it and/or *)
(* modify it under the terms of the GNU Library General Public *)
(* License version 2.1, with the special exception on linking *)
(* described in file LICENSE. *)
(* *)
(* This software is distributed in the hope that it will be useful, *)
(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. *)
(* *)
(**************************************************************************)
val typecheck : Why3.Env.env -> Why3.Env.pathname ->
Tptp_ast.tptp_file -> Why3.Theory.theory Why3.Util.Mstr.t
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