Commit 60a0f681 authored by Simon Cruanes's avatar Simon Cruanes

uniformisation of module name (camlcase)

use of why AST in progress for tptp2why, but building a theory still does not work
parent 2c9c3ffb
......@@ -395,10 +395,10 @@ clean::
MENHIR=@MENHIR@
TPTPGENERATED = src/tptp2why/tptp_lexer.ml \
src/tptp2why/tptp_parser.ml src/tptp2why/tptp_parser.mli
TPTPGENERATED = src/tptp2why/tptpLexer.ml \
src/tptp2why/tptpParser.ml src/tptp2why/tptpParser.mli
TPTP_FILES = tptpTree tptp_parser tptp_lexer tptpTranslate tptp2why
TPTP_FILES = tptpTree tptpParser tptpLexer tptpTranslate tptp2why
TPTP_DIR=src/tptp2why/
TPTPMODULES = $(addprefix $(TPTP_DIR), $(TPTP_FILES))
......@@ -417,7 +417,7 @@ byte: bin/tptp2why.byte
opt: bin/tptp2why.opt
endif
src/tptp2why/tptp_parser.ml src/tptp2why/tptp_parser.mli: OCAMLYACC = $(MENHIR)
src/tptp2why/tptpParser.ml src/tptp2why/tptpParser.mli: OCAMLYACC = $(MENHIR)
bin/tptp2why.opt: src/why.cmxa $(TPTPCMX)
$(if $(QUIET), @echo 'Linking $@' &&) \
......
......@@ -19,7 +19,7 @@ end= struct
try
let filename = if first then filename else include_dir^"/"^filename in
let input = open_in filename in
let decls = Tptp_parser.tptp Tptp_lexer.token (Lexing.from_channel input) in
let decls = TptpParser.tptp TptpLexer.token (Lexing.from_channel input) in
let isInclude = function | Include _ -> true | _ -> false in
close_in input;
let (to_include, real_decl) = List.partition isInclude decls in
......
......@@ -2,7 +2,7 @@
{
open Format
open Lexing
open Tptp_parser
open TptpParser
let keywords = Hashtbl.create 97
let () =
......
......@@ -120,19 +120,21 @@ module Translate = struct
end)
module EnvFunctor = Scope(
struct
type key = (atom * Ty.ty list)
type key = (atom * Ty.ty list * Summary.indic)
type value = Term.lsymbol
let create (v,l) = Term.create_fsymbol (id_fresh (String.uncapitalize v)) l t
let create (v,l,ty) = match ty with
| Summary.Term -> Term.create_fsymbol (id_fresh (String.uncapitalize v)) l t
| Summary.Pred -> Term.create_psymbol (id_fresh (String.uncapitalize v)) l
end)
(** translation for terms *)
let rec term2term = function
| TAtom x -> Term.t_app (EnvFunctor.find (x, [])) [] t
| TConst x -> Term.t_app (EnvFunctor.find (x, [])) [] t
| TAtom x -> Term.t_app (EnvFunctor.find (x, [], Summary.Term)) [] t
| TConst x -> Term.t_app (EnvFunctor.find (x, [], Summary.Term)) [] t
| TVar x -> Term.t_var (EnvVar.find x)
| TFunctor (f, terms) ->
Term.t_app
(EnvFunctor.find (f, List.map (const t) terms))
(EnvFunctor.find (f, List.map (const t) terms, Summary.Term))
(List.map term2term terms)
t
......@@ -162,13 +164,13 @@ module Translate = struct
end
| FPred (p, terms) ->
Term.f_app
(EnvFunctor.find (p, List.map (const t) terms))
(EnvFunctor.find (p, List.map (const t) terms, Summary.Pred))
(List.map term2term terms)
| FTermBinop (op, t1, t2) ->
Term.f_app
( match op with
| Equal -> EnvFunctor.find ("=", [t;t])
| NotEqual -> EnvFunctor.find ("<>", [t;t]) )
| Equal -> EnvFunctor.find ("=", [t;t], Summary.Pred)
| NotEqual -> EnvFunctor.find ("<>", [t;t], Summary.Pred) )
[term2term t1; term2term t2]
let translatePropKind = function
......@@ -179,6 +181,7 @@ module Translate = struct
let addDecl theory = function
| Fof(name, ty, f) ->
let fmla = fmla2fmla f in
print_endline ("adds declaration of "^name);
Theory.add_prop_decl theory (translatePropKind ty)
(Decl.create_prsymbol (id_fresh name)) fmla
| Include _ -> assert false
......
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