From fedecee9c4b10a2469c10fe09ec091d2dc6fc56a Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 7 Apr 2010 13:34:29 +0000 Subject: [PATCH] THF parser for TPTP From: tassi --- helm/software/components/tptp_grafite/.depend | 7 + .../software/components/tptp_grafite/Makefile | 20 ++- .../components/tptp_grafite/astTHF.ml | 22 +++ .../components/tptp_grafite/lexerTHF.mll | 74 ++++++++ .../components/tptp_grafite/mainTHF.ml | 32 ++++ .../components/tptp_grafite/parserTHF.mly | 165 ++++++++++++++++++ 6 files changed, 312 insertions(+), 8 deletions(-) create mode 100644 helm/software/components/tptp_grafite/astTHF.ml create mode 100644 helm/software/components/tptp_grafite/lexerTHF.mll create mode 100644 helm/software/components/tptp_grafite/mainTHF.ml create mode 100644 helm/software/components/tptp_grafite/parserTHF.mly diff --git a/helm/software/components/tptp_grafite/.depend b/helm/software/components/tptp_grafite/.depend index a8972f4cf..bf1f2d73e 100644 --- a/helm/software/components/tptp_grafite/.depend +++ b/helm/software/components/tptp_grafite/.depend @@ -1,10 +1,17 @@ parser.cmi: ast.cmo +parserTHF.cmi: astTHF.cmo tptp2grafite.cmi: ast.cmo: ast.cmx: lexer.cmo: parser.cmi lexer.cmx: parser.cmx +astTHF.cmo: +astTHF.cmx: +lexerTHF.cmo: parserTHF.cmi +lexerTHF.cmx: parserTHF.cmx parser.cmo: ast.cmo parser.cmi parser.cmx: ast.cmx parser.cmi +parserTHF.cmo: astTHF.cmo parserTHF.cmi +parserTHF.cmx: astTHF.cmx parserTHF.cmi tptp2grafite.cmo: parser.cmi lexer.cmo ast.cmo tptp2grafite.cmi tptp2grafite.cmx: parser.cmx lexer.cmx ast.cmx tptp2grafite.cmi diff --git a/helm/software/components/tptp_grafite/Makefile b/helm/software/components/tptp_grafite/Makefile index c196dd609..1e2398373 100644 --- a/helm/software/components/tptp_grafite/Makefile +++ b/helm/software/components/tptp_grafite/Makefile @@ -1,31 +1,35 @@ PACKAGE = tptp_grafite PREDICATES = -INTERFACE_FILES= parser.mli tptp2grafite.mli +INTERFACE_FILES= parser.mli parserTHF.mli tptp2grafite.mli -IMPLEMENTATION_FILES = ast.ml lexer.ml $(INTERFACE_FILES:%.mli=%.ml) +IMPLEMENTATION_FILES = ast.ml lexer.ml astTHF.ml lexerTHF.ml $(INTERFACE_FILES:%.mli=%.ml) EXTRA_OBJECTS_TO_INSTALL = EXTRA_OBJECTS_TO_CLEAN = TPTPDIR= /home/$(USER)/work-area/TPTP-v3.2.0/ -all: tptp2grafite +all: tptp2grafite mainTHF clean: clean_tests clean_tests: rm -f tptp2grafite -parser.mli parser.ml:parser.mly - ocamlyacc parser.mly -lexer.ml: - ocamllex lexer.mll +%.mli %.ml: %.mly + ocamlyacc $*.mly +%.ml:%.mll + ocamllex $*.mll LOCAL_LINKOPTS = -package helm-$(PACKAGE) -linkpkg tptp2grafite: main.ml tptp_grafite.cma @echo " OCAMLC $<" @$(OCAMLC) $(LOCAL_LINKOPTS) -o $@ $< -test: tptp2grafite +mainTHF: mainTHF.ml tptp_grafite.cma + @echo " OCAMLC $<" + @$(OCAMLC) $(LOCAL_LINKOPTS) -o $@ $< + +test: tptp2grafite mainTHF testall: tptp2grafite for X in `cat unit_equality_problems`; do\ diff --git a/helm/software/components/tptp_grafite/astTHF.ml b/helm/software/components/tptp_grafite/astTHF.ml new file mode 100644 index 000000000..541cf98e1 --- /dev/null +++ b/helm/software/components/tptp_grafite/astTHF.ml @@ -0,0 +1,22 @@ +type role = + Axiom +| Hypothesis +| Definition +| Assumption +| Lemma +| Theorem +| Conjecture +| Negated_conjecture +| Lemma_conjecture +| Plain +| Fi_domain +| Fi_functors +| Fi_predicates +| Type +| Unknown + + +type ast = + | Formula of string * role * CicNotationPt.term + | Comment of string + | Inclusion of string * (string list) diff --git a/helm/software/components/tptp_grafite/lexerTHF.mll b/helm/software/components/tptp_grafite/lexerTHF.mll new file mode 100644 index 000000000..6dc1d5795 --- /dev/null +++ b/helm/software/components/tptp_grafite/lexerTHF.mll @@ -0,0 +1,74 @@ +{ + open ParserTHF + exception BadToken of string + + let incr_linenum lexbuf = + let pos = lexbuf.Lexing.lex_curr_p in + lexbuf.Lexing.lex_curr_p <- { pos with + Lexing.pos_lnum = pos.Lexing.pos_lnum + 1; + Lexing.pos_bol = pos.Lexing.pos_cnum; + } + ;; + +} + +let dust = ' ' | '\t' +let comment = '%' [^ '\n' ] * '\n' +let lname = + ['a'-'z'] ['a'-'z''A'-'Z''0'-'9''_']* +let uname = + ['A'-'Z'] ['a'-'z''A'-'Z''0'-'9''_']* +let qstring = ''' [^ ''' ]+ ''' +let type_ = + "axiom" | "hypothesis" | "definition" | "lemma" | "theorem" | + "conjecture" | "lemma_conjecture" | "negated_conjecture" | + "plain" | "unknown" | "type" + +let ieq = "=" +let peq = "equal" +let nieq = "!=" + +rule yylex = parse + | dust { yylex lexbuf } + | '\n' { incr_linenum lexbuf; yylex lexbuf } + | comment { incr_linenum lexbuf; COMMENT (Lexing.lexeme lexbuf) } + | "include" { INCLUSION } + | type_ { TYPE (Lexing.lexeme lexbuf) } + | "thf" { THF } + | "$true" { TRUE } + | "$false" { FALSE } + | "equal" { PEQ } + + | "$i" { TYPE_I } + | "$o" { TYPE_O } + | "$tType" { TYPE_U } + | ">" { TO } + + | lname { LNAME (Lexing.lexeme lexbuf) } + | uname { UNAME (Lexing.lexeme lexbuf) } + + | ['0' - '9']+ { NUM (int_of_string (Lexing.lexeme lexbuf)) } + | ',' { COMMA } + | '.' { DOT } + | '(' { LPAREN } + | ')' { RPAREN } + | '|' { IOR } + | '&' { IAND } + | '~' { NOT } + | '=' { IEQ } + | "=>" { IMPLY } + | "!=" { NIEQ } + | "!" { FORALL } + | "?" { EXISTS } + | "!" { FORALL } + | "^" { LAMBDA } + | "[" { BEGINVARLIST } + | "]" { ENDVARLIST } + | ":" { COLON } + | "," { COMMA } + | "@" { APPLY } + | qstring { QSTRING (Lexing.lexeme lexbuf) } + | eof { EOF } + | _ { raise (BadToken (Lexing.lexeme lexbuf)) } + +{ (* trailer *) } diff --git a/helm/software/components/tptp_grafite/mainTHF.ml b/helm/software/components/tptp_grafite/mainTHF.ml new file mode 100644 index 000000000..b3eca0141 --- /dev/null +++ b/helm/software/components/tptp_grafite/mainTHF.ml @@ -0,0 +1,32 @@ +(* OPTIONS *) +let tptppath = ref "./";; +let ng = ref false;; +let spec = [ + ("-ng",Arg.Set ng,"Matita ng syntax"); + ("-tptppath", + Arg.String (fun x -> tptppath := x), + "Where to find the Axioms/ and Problems/ directory") +] + +(* MAIN *) +let _ = + let usage = "Usage: tptpTHF2grafite [options] file" in + let inputfile = ref "" in + Arg.parse spec (fun s -> inputfile := s) usage; + if !inputfile = "" then + begin + prerr_endline usage; + exit 1 + end; + let lexbuf = Lexing.from_channel (open_in !inputfile) in + List.iter + (function + | AstTHF.Comment _ -> () + | AstTHF.Inclusion _ -> () + | AstTHF.Formula(name,role,term) -> + prerr_endline (name ^ "===" ^ CicNotationPp.pp_term term) + + ) + (ParserTHF.main LexerTHF.yylex lexbuf); + exit 0 + diff --git a/helm/software/components/tptp_grafite/parserTHF.mly b/helm/software/components/tptp_grafite/parserTHF.mly new file mode 100644 index 000000000..35bc870cc --- /dev/null +++ b/helm/software/components/tptp_grafite/parserTHF.mly @@ -0,0 +1,165 @@ +%{ + (* header *) + open AstTHF + open Parsing + open Lexing + module T = CicNotationPt + + let parse_error s = Printf.eprintf "%s: " s ;; + let rm_q s = String.sub s 1 (String.length s - 2) ;; + +%} + %token TYPE + %token COMMENT + %token NUM + %token LNAME + %token UNAME + %token QSTRING + %token COMMA + %token INCLUSION + %token LPAREN + %token RPAREN + %token CNF + %token TRUE + %token FALSE + %token NOT + %token IAND + %token IOR + %token NIEQ + %token IEQ + %token IMPLY + %token PEQ + %token DOT + %token EOF + %token FORALL + %token EXISTS + %token LAMBDA + %token COLON + %token BEGINVARLIST + %token ENDVARLIST + %token APPLY + %token TYPE_I + %token TYPE_O + %token TYPE_U + %token TO + %token THF + + %left IOR + %left IAND + %nonassoc NOT + %right TO + %left APPLY + + %type main + %start main +%% + main: + | tptp_input EOF {[$1]} + | tptp_input main {$1::$2} + | error { + let start_pos = rhs_start_pos 1 in + let end_pos = rhs_end_pos 1 in + Printf.eprintf "from line %d char %d to line %d char %d\n" + start_pos.pos_lnum (start_pos.pos_cnum - start_pos.pos_bol) + end_pos.pos_lnum (end_pos.pos_cnum - end_pos.pos_bol); + exit 1 + } + ; + + tptp_input: + | annot_formula {$1} + | include_ {$1} + | comment {$1} + ; + + formula_source_and_infos: + | { () } + | COMMA { assert false } + ; + + annot_formula: + | THF LPAREN + name COMMA formula_type COMMA term formula_source_and_infos + RPAREN DOT { + Formula($3,$5,$7) + } + ; + + formula_type: + | TYPE { + match $1 with + | "axiom" -> Axiom + | "hypothesis" -> Hypothesis + | "definition" -> Definition + | "lemma" -> Lemma + | "theorem" -> Theorem + | "conjecture" -> Conjecture + | "lemma_conjecture" -> Lemma_conjecture + | "negated_conjecture" -> Negated_conjecture + | "plain" -> Plain + | "unknown" -> Unknown + | "type" -> Type + | _ -> assert false + } + ; + + quantifier : + | FORALL {`Forall} + | EXISTS {`Exists} + | LAMBDA {`Lambda} + + vardecl : + | UNAME { T.Implicit `JustOne,Some (T.Ident($1,None)) } + | UNAME COLON term { $3,Some (T.Ident($1,None)) } + + varlist : + | vardecl { [$1] } + | vardecl COMMA varlist { $1 :: $3 } + + term: + | quantifier BEGINVARLIST varlist ENDVARLIST COLON term { + List.fold_right (fun v t -> T.Binder($1,v,t)) $3 $6 + } + | term IMPLY term { + match $1 with + | T.Appl l -> T.Appl (l @ [$3]) + | x -> T.Appl ([$1; $3]) + } + | term APPLY term { + match $1 with + | T.Appl l -> T.Appl (l @ [$3]) + | x -> T.Appl ([$1; $3]) + } + | LPAREN term COLON term RPAREN { T.Cast ($2,$4) } + | term TO term { T.Binder (`Pi,($1,None),$3) } + | term IEQ term { T.Appl [T.Symbol("'eq",0);$1;$3] } + | term IAND term { T.Appl [T.Symbol("'and",0);$1;$3] } + | term IOR term { T.Appl [T.Symbol("'or",0);$1;$3] } + | NOT term { T.Appl [T.Symbol("'not",0);$2] } + | LPAREN term RPAREN {$2} + | LNAME { T.Ident($1,None) } + | UNAME { T.Ident($1,None) } + | TYPE_I { T.Symbol("'i",0) } + | TYPE_O { T.Symbol("'o",0) } + | TYPE_U { T.Sort `Set } + | FALSE { T.Symbol("'false",0)} + | TRUE { T.Symbol("'true",0)} + ; + + include_: + | INCLUSION LPAREN QSTRING selection_of_formulae RPAREN DOT { + let fname = rm_q $3 in + Inclusion (fname,$4) + } + ; + + selection_of_formulae: + | { [] } + | COMMA name selection_of_formulae { $2::$3 } + ; + + comment: COMMENT {Comment $1} ; + + name: NUM { string_of_int $1} | LNAME { $1 } | UNAME { $1 } ; +%% + (* trailer *) -- 2.39.2