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 34b2a505 authored by POGODALLA Sylvain's avatar POGODALLA Sylvain
Browse files

Move to using menhir to parse datalog programs.

cherry-picking commit aec5c07.
parent d6e1d07b
This directory contains the datalog implementation.
The Datalog grammar that can be uses to test the prover is as follows:
+ identifers (for predicate symbols or variables occuring within an atom) are sequences that start with a letter (upper or lower case) and contains letters (upper or lower case) and the `_` symbol, and possibly ends with a sequence of `'` symbols, or a single symbol among `|` `!` `"` `#` `$` `%` `&` `\'` `*` `+` `-` `/` `<` `>` `?` `@` `\\` `^` ``` ` ``` `~`
+ constants are natural numbers
+ a predicate symbol consists of an idenditierds optionally followed by `/n` where `n` is the arity of the symbol
+ a program consists of a sequence of rules and facts
+ a rule consists of:
+ a head only: an atom followed by a `.`.
Ex:
```
A(1,2,j,k).
```
+ a head and a body: an atom followed by the `:-` symbol and a comma separated list of atoms ending with a `.`
Ex:
```
S(i,k) :- NP(i,j),VP(j,k).
```
+ a fact consists of a an atom whose paremeters are constants (i.e., natural numbers) followed by a `.`
Ex:
```
A(1,2,3).
```
```
......@@ -86,8 +86,8 @@ sig
val empty : t
(** [extension pred_table const_table id_gen] returns an almost
empty proto program. This almost empty proto program is mean to
serve as extension of an actual program *)
empty proto program. This almost empty proto program is meant
to serve as extension of an actual program *)
val extension : Predicate.PredIdTable.table -> ConstGen.Table.table -> IntIdGen.t -> t
val add_proto_rule : ((tables -> (Predicate.predicate*tables))*(tables -> ((Predicate.predicate list)*tables))) -> t -> t
......
open UtilsLib.IdGenerator
open DatalogLib.Datalog_AbstractSyntax
(*module Store = (*: UnionFind.Store with type 'a t ='a PersistentArray.PersistentArray.t *)
......@@ -47,9 +46,9 @@ let parse_file query edb filename =
Logs.app (fun m -> m "%s" sep);
let program =
match edb with
| None ->
| None ->
Logs.debug (fun m -> m "I didn't find an edb file to parse.");
program
program
| Some edb_filename ->
Logs.debug (fun m -> m "I found an edb file to parse.");
let edb_in_ch =
......@@ -59,24 +58,72 @@ let parse_file query edb filename =
Logs.app (fun m -> m "Parsing \"%s\"..." edb_filename);
let to_be_added=DatalogLib.Db_parser.extensional_facts DatalogLib.Db_lexer.lexer edb_lexbuf Datalog.Program.(program.pred_table,program.const_table,program.rule_id_gen) in
Logs.app (fun m -> m "Done.");
Datalog.Program.add_e_facts program to_be_added in
Datalog.Program.add_e_facts program to_be_added in
let derived_facts,derivations = Datalog.Program.seminaive program in
Logs.app (fun m -> m "I could derive the following facts:\n%s" (Datalog.Predicate.facts_to_string derived_facts program.Datalog.Program.pred_table program.Datalog.Program.const_table));
let buff = Buffer.create 80 in
let () = Datalog.Predicate.add_map_to_premises_to_buffer buff program.Datalog.Program.pred_table program.Datalog.Program.const_table derivations in
Logs.app (fun m -> m "With the following derivations:\n%s\n" (Buffer.contents buff));
let query,new_pred_table,new_cons_table =
let query,_new_pred_table,_new_cons_table =
match query with
| None ->
None,program.Datalog.Program.pred_table,program.Datalog.Program.const_table
None,program.Datalog.Program.pred_table,program.Datalog.Program.const_table
| Some s ->
let q,t1,t2=DatalogLib.Db_parser.query DatalogLib.Db_lexer.lexer (Lexing.from_string s) Datalog.Program.(program.pred_table,program.const_table) in
Some q,t1,t2 in
let q,t1,t2=DatalogLib.Db_parser.query DatalogLib.Db_lexer.lexer (Lexing.from_string s) Datalog.Program.(program.pred_table,program.const_table) in
Some q,t1,t2 in
let () = Datalog.Predicate.format_derivations2 ?query:query program.Datalog.Program.pred_table program.Datalog.Program.const_table derivations in
Logs.app (fun m -> m "%s" (Buffer.contents (Format.stdbuf)));
()
let main query edb filename =
match DatalogLib.Dl_parse_functions.parse_program filename with
| None -> ()
| Some p ->
let prog= p AbstractSyntax.Proto_Program.empty in
Logs.debug (fun m -> m "Current symbol tables:");
AbstractSyntax.Predicate.PredIdTable.log_content Logs.Debug prog.AbstractSyntax.Proto_Program.pred_table;
let sep=String.make 15 '*' in
Logs.app (fun m -> m "%s%!" sep);
Logs.app (fun m -> m "Create the abstract program and print it...");
let abs_program = AbstractSyntax.Program.make_program prog in
let () = Buffer.output_buffer stdout (AbstractSyntax.Program.to_buffer abs_program) in
Logs.app (fun m -> m "Done.");
Logs.app (fun m -> m "%s" sep);
Logs.app (fun m -> m "Create the internal program and print it...");
let program=Datalog.Program.make_program abs_program in
let () = Buffer.output_buffer stdout (AbstractSyntax.Program.to_buffer (Datalog.Program.to_abstract program)) in
Logs.app (fun m -> m "Done.");
Logs.app (fun m -> m "%s" sep);
let program =
match edb with
| None ->
let () = Logs.debug (fun m -> m "I didn't find an edb file to parse.") in
program
| Some edb_filename ->
let () = Logs.debug (fun m -> m "I found an edb file to parse.") in
let to_be_added=DatalogLib.Dl_parse_functions.parse_edb edb_filename in
match to_be_added with
| None -> program
| Some add -> Datalog.Program.add_e_facts program (add Datalog.Program.(program.pred_table,program.const_table,program.rule_id_gen)) in
let derived_facts,derivations = Datalog.Program.seminaive program in
Logs.app (fun m -> m "I could derive the following facts:\n%s" (Datalog.Predicate.facts_to_string derived_facts program.Datalog.Program.pred_table program.Datalog.Program.const_table));
let buff = Buffer.create 80 in
let () = Datalog.Predicate.add_map_to_premises_to_buffer buff program.Datalog.Program.pred_table program.Datalog.Program.const_table derivations in
Logs.app (fun m -> m "With the following derivations:\n%s\n" (Buffer.contents buff));
Logs.app (fun m -> m "%s" (Buffer.contents (Format.stdbuf)));
match query with
| None ->
Datalog.Predicate.format_derivations2 program.Datalog.Program.pred_table program.Datalog.Program.const_table derivations
| Some s ->
let as_q = DatalogLib.Dl_parse_functions.parse_query s in
match as_q with
| None -> ()
| Some pred ->
let () = Logs.app (fun m -> m "Facts (and their derivations) matching the query \"%s\":\n" s) in
let q,_t1,_t2= pred Datalog.Program.(program.pred_table,program.const_table) in
Datalog.Predicate.format_derivations2 ~query:q program.Datalog.Program.pred_table program.Datalog.Program.const_table derivations
let usage_msg="Usage: db_test [-edb edb_file] file"
let edb_file=ref None
......@@ -89,7 +136,9 @@ let options =
]
let () =
let () = UtilsLib.Log.set_level "db_test" Logs.App in
let () = UtilsLib.Log.set_level ~app:"db_test" Logs.Warning in
(* let () = UtilsLib.Log.set_level ~app:"db_test" Logs.Debug in *)
if Array.length (Sys.argv) > 1 then
Arg.parse options (fun s -> parse_file !query !edb_file s) usage_msg
else parse_file None None "/home/pogodall/work/dev/ACGtk/src/datalog.prover/Jean-regarde-telescope.dl"
(* Arg.parse options (fun s -> parse_file !query !edb_file s) usage_msg *)
Arg.parse options (fun s -> main !query !edb_file s) usage_msg
else parse_file None None "/home/pogodall/work/dev/ACGtk/src/datalog.prover/Jean-regarde-telescope.dl"
type err =
| BadArity of (string * int * int)
| ParseError of string
module E =
struct
type t = err
let to_string = function
| BadArity (sym,expected_a,written_a) -> Printf.sprintf "Predicate symbole \"%s\" is defined with arity %d while used with arity %d" sym expected_a written_a
| ParseError s -> s
end
module Error = UtilsLib.ErrorMg.Make(E)
type err =
| BadArity of (string * int * int)
| ParseError of string
module E : UtilsLib.ErrorMg.E with type t = err
module Error : UtilsLib.ErrorMg.ERROR with type t = E.t UtilsLib.ErrorMg.error
{
open Dl_parser
open UtilsLib
let loc lexbuf = Lexing.lexeme_start_p lexbuf,Lexing.lexeme_end_p lexbuf
}
let newline = ('\010' | '\013' | "\013\010")
let letter = ['a'-'z' 'A'-'Z' 'µ' 'À'-'Ö' 'Ø'-'Ý' 'ß'-'ö' 'ø'-'ÿ']
let digit = ['0'-'9']
let string = (letter|digit|'_')*'\''*
let symbol = ['|' '!' '"' '#' '$' '%' '&' '\'' '*' '+' '-' '/' '<' '>' '?' '@' '\\' '^' '`' '~' ]
rule lexer = parse
| [' ' '\t'] {lexer lexbuf}
| newline {let () = Lexing.new_line lexbuf in lexer lexbuf}
| "(*" {comment [loc lexbuf] lexbuf}
| "*)" {raise (DlError.Error.Error (ErrorMg.LexError ErrorMg.Unstarted_comment,loc lexbuf))}
| eof {EOI}
| "," {COMMA(loc lexbuf)}
| "." {DOT(loc lexbuf)}
| "(" {LPAR(loc lexbuf)}
| ")" {RPAR(loc lexbuf)}
| ":-" {FROM(loc lexbuf)}
| "/" {SLASH(loc lexbuf)}
| "?" {QUESTION_MARK(loc lexbuf)}
| letter string {IDENT (Lexing.lexeme lexbuf,loc lexbuf)}
| symbol {IDENT (Lexing.lexeme lexbuf,loc lexbuf)}
| '-'?digit+ {let s = Lexing.lexeme lexbuf in
INT ((int_of_string s),loc lexbuf)}
and comment depth = parse
| "*)" {match depth with
| [_] -> lexer lexbuf
| _::tl -> comment tl lexbuf
| [] -> raise (DlError.Error.Error (ErrorMg.LexError ErrorMg.Unstarted_comment,loc lexbuf))}
| "(*" {comment ((loc lexbuf)::depth) lexbuf}
| eof {raise (DlError.Error.Error (ErrorMg.LexError ErrorMg.Unclosed_comment, List.hd depth))}
| newline {let () = Lexing.new_line lexbuf in comment depth lexbuf}
| _ {comment depth lexbuf}
open UtilsLib
module I = Dl_parser.MenhirInterpreter
(* -------------------------------------------------------------------------- *)
let succeed data =
(* The parser has succeeded and produced a semantic value. *)
data
let fail lexbuf c =
(* The parser has suspended itself because of a syntax error. Stop. *)
match c with
| I.HandlingError env ->
let loc = Lexing.lexeme_start_p lexbuf,Lexing.lexeme_end_p lexbuf in
let current_state_num = I.current_state_number env in
raise (DlError.Error.Error (ErrorMg.SyntError (DlError.ParseError (Messages.message current_state_num)),loc))
| _ -> failwith "Should not happen. Always fails with a HandlingError"
let core_supplier lexbuf = I.lexer_lexbuf_to_supplier Dl_lexer.lexer lexbuf
let supplier = core_supplier
let dummy_loc = Lexing.(dummy_pos,dummy_pos)
type entry =
| File of string
| String of string
let generic_parse ~entry f =
let input =
match entry with
| File f -> f
| String _ -> "stdin" in
try
let lexbuf,from_file =
match entry with
| File filename ->
let in_ch =
let fullname = Utils.find_file filename [""] in
open_in fullname in
Lexing.from_channel in_ch,true
| String s -> Lexing.from_string s,false in
let () = if from_file then Logs.app (fun m -> m "Parsing \"%s\"..." input) else () in
let starting_parse_time = Sys.time () in
let e = I.loop_handle succeed (fail lexbuf) (supplier lexbuf) (f lexbuf.Lexing.lex_curr_p) in
let ending_parse_time = Sys.time () in
let () = if from_file then Logs.app (fun m -> m "Done (%.3f seconds).\n%!" (ending_parse_time -. starting_parse_time)) else () in
Some e
with
| Utils.No_file(f,msg) ->
let e = ErrorMg.SysError (Printf.sprintf "No such file \"%s\" in %s" f msg) in
let () = Logs.err (fun m -> m "%s" (DlError.Error.error_msg (e,dummy_loc) ~filename:f)) in
None
| Sys_error s ->
let e = ErrorMg.SysError s in
let () = Logs.err (fun m -> m "%s" (DlError.Error.error_msg (e,dummy_loc) ~filename:input)) in
None
| DlError.Error.Error e ->
let () = Logs.err (fun m -> m "%s" (DlError.Error.error_msg e ~filename:input)) in
None
let parse_program filename =
generic_parse ~entry:(File filename) Dl_parser.Incremental.program
let parse_edb filename =
generic_parse ~entry:(File filename) Dl_parser.Incremental.extensional_facts
let parse_query q =
generic_parse ~entry:(String q) Dl_parser.Incremental.query
open Datalog_AbstractSyntax
open AbstractSyntax
val parse_program : string -> (Proto_Program.t -> Proto_Program.t) option
val parse_edb : string -> ((Predicate.PredIdTable.table * ConstGen.Table.table * UtilsLib.IdGenerator.IntIdGen.t) -> (Rule.rule list * ConstGen.Table.table * UtilsLib.IdGenerator.IntIdGen.t)) option
val parse_query : string -> ((Predicate.PredIdTable.table * ConstGen.Table.table) -> (Predicate.predicate * Predicate.PredIdTable.table * Datalog_AbstractSyntax.ConstGen.Table.table)) option
rule: IDENT LPAR IDENT RPAR FROM SLASH
##
## Ends in an error in state: 49.
##
## rule -> atom FROM . separated_nonempty_list(COMMA,atom) DOT [ # ]
##
## The known suffix of the stack is as follows:
## atom FROM
##
rule: SLASH
##
## Ends in an error in state: 46.
##
## rule' -> . rule [ # ]
##
## The known suffix of the stack is as follows:
##
##
query: SLASH
##
## Ends in an error in state: 39.
##
## query' -> . query [ # ]
##
## The known suffix of the stack is as follows:
##
##
program: IDENT LPAR IDENT RPAR DOT SLASH
##
## Ends in an error in state: 22.
##
## nonempty_list(rule) -> rule . [ EOI ]
## nonempty_list(rule) -> rule . nonempty_list(rule) [ EOI ]
##
## The known suffix of the stack is as follows:
## rule
##
program: IDENT LPAR IDENT RPAR FROM IDENT LPAR IDENT RPAR COMMA SLASH
##
## Ends in an error in state: 33.
##
## separated_nonempty_list(COMMA,atom) -> atom COMMA . separated_nonempty_list(COMMA,atom) [ DOT ]
##
## The known suffix of the stack is as follows:
## atom COMMA
##
program: IDENT LPAR IDENT RPAR FROM SLASH
##
## Ends in an error in state: 29.
##
## rule -> atom FROM . separated_nonempty_list(COMMA,atom) DOT [ IDENT EOI ]
##
## The known suffix of the stack is as follows:
## atom FROM
##
program: SLASH
##
## Ends in an error in state: 21.
##
## program' -> . program [ # ]
##
## The known suffix of the stack is as follows:
##
##
extensional_facts: SLASH
##
## Ends in an error in state: 0.
##
## extensional_facts' -> . extensional_facts [ # ]
##
## The known suffix of the stack is as follows:
##
##
extensional_facts: IDENT LPAR IDENT RPAR DOT SLASH
##
## Ends in an error in state: 9.
##
## nonempty_list(extensional_fact) -> extensional_fact . [ EOI ]
## nonempty_list(extensional_fact) -> extensional_fact . nonempty_list(extensional_fact) [ EOI ]
##
## The known suffix of the stack is as follows:
## extensional_fact
##
A predicate symbol is expected.
rule: IDENT LPAR IDENT RPAR SLASH
##
## Ends in an error in state: 48.
##
## rule -> atom . DOT [ # ]
## rule -> atom . FROM separated_nonempty_list(COMMA,atom) DOT [ # ]
##
## The known suffix of the stack is as follows:
## atom
##
program: IDENT LPAR IDENT RPAR SLASH
##
## Ends in an error in state: 28.
##
## rule -> atom . DOT [ IDENT EOI ]
## rule -> atom . FROM separated_nonempty_list(COMMA,atom) DOT [ IDENT EOI ]
##
## The known suffix of the stack is as follows:
## atom
##
A "." or a ":-" is expected.
query: IDENT LPAR INT RPAR SLASH
##
## Ends in an error in state: 44.
##
## query -> atom_sym LPAR separated_nonempty_list(COMMA,parameter) RPAR . QUESTION_MARK [ # ]
##
## The known suffix of the stack is as follows:
## atom_sym LPAR separated_nonempty_list(COMMA,parameter) RPAR
##
A "?" is expected.
query: IDENT SLASH INT SLASH
##
## Ends in an error in state: 41.
##
## query -> atom_sym . LPAR separated_nonempty_list(COMMA,parameter) RPAR QUESTION_MARK [ # ]
##
## The known suffix of the stack is as follows:
## atom_sym
##
program: IDENT SLASH INT SLASH
##
## Ends in an error in state: 24.
##
## atom -> atom_sym . LPAR separated_nonempty_list(COMMA,parameter) RPAR [ FROM DOT COMMA ]
##
## The known suffix of the stack is as follows:
## atom_sym
##
A "(" is expected.
program: IDENT LPAR IDENT RPAR FROM IDENT LPAR IDENT RPAR SLASH
##
## Ends in an error in state: 32.
##
## separated_nonempty_list(COMMA,atom) -> atom . [ DOT ]
## separated_nonempty_list(COMMA,atom) -> atom . COMMA separated_nonempty_list(COMMA,atom) [ DOT ]
##
## The known suffix of the stack is as follows:
## atom
##
A "." or a "," is expected.
query: IDENT LPAR SLASH
##
## Ends in an error in state: 42.
##
## query -> atom_sym LPAR . separated_nonempty_list(COMMA,parameter) RPAR QUESTION_MARK [ # ]
##
## The known suffix of the stack is as follows:
## atom_sym LPAR
##
program: IDENT LPAR SLASH
##
## Ends in an error in state: 25.
##
## atom -> atom_sym LPAR . separated_nonempty_list(COMMA,parameter) RPAR [ FROM DOT COMMA ]
##
## The known suffix of the stack is as follows:
## atom_sym LPAR
##
extensional_facts: IDENT LPAR INT COMMA SLASH
##
## Ends in an error in state: 19.
##
## separated_nonempty_list(COMMA,parameter) -> parameter COMMA . separated_nonempty_list(COMMA,parameter) [ RPAR ]
##
## The known suffix of the stack is as follows:
## parameter COMMA
##
extensional_facts: IDENT LPAR SLASH
##
## Ends in an error in state: 12.
##
## extensional_fact -> atom_sym LPAR . separated_nonempty_list(COMMA,parameter) RPAR DOT [ IDENT EOI ]
##
## The known suffix of the stack is as follows:
## atom_sym LPAR
##
A variable or a constant (natural number) is expected.
extensional_facts: IDENT LPAR INT RPAR SLASH
##
## Ends in an error in state: 16.
##
## extensional_fact -> atom_sym LPAR separated_nonempty_list(COMMA,parameter) RPAR . DOT [ IDENT EOI ]
##
## The known suffix of the stack is as follows:
## atom_sym LPAR separated_nonempty_list(COMMA,parameter) RPAR
##
A "." or a "," is expected.
extensional_facts: IDENT LPAR INT SLASH
##
## Ends in an error in state: 18.
##
## separated_nonempty_list(COMMA,parameter) -> parameter . [ RPAR ]
## separated_nonempty_list(COMMA,parameter) -> parameter . COMMA separated_nonempty_list(COMMA,parameter) [ RPAR ]
##
## The known suffix of the stack is as follows:
## parameter
##
A "," or a ")" is expected.
extensional_facts: IDENT RPAR
##
## Ends in an error in state: 1.
##
## atom_sym -> IDENT . option(arity) [ LPAR ]
##
## The known suffix of the stack is as follows:
## IDENT
##
A "/" or a "(" is expected.
extensional_facts: IDENT SLASH INT SLASH
##
## Ends in an error in state: 11.
##
## extensional_fact -> atom_sym . LPAR separated_nonempty_list(COMMA,parameter) RPAR DOT [ IDENT EOI ]
##
## The known suffix of the stack is as follows:
## atom_sym
##
A "(" is expected.
extensional_facts: IDENT SLASH SLASH
##
## Ends in an error in state: 2.
##
## arity -> SLASH . INT [ LPAR ]
##
## The known suffix of the stack is as follows:
## SLASH
##
An integer is expected.
%{
open UtilsLib
open IdGenerator
open Datalog_AbstractSyntax
let check_arity (pred_sym,loc) length arity =
let () = Logs.info (fun m -> m "Checking symbol \"%s\". Parameter number is %d" pred_sym length) in
match arity with
| Some a when a<>length ->
let () = Logs.info (fun m -> m "Found arity %d" a) in
raise DlError.(Error.Error (ErrorMg.SyntError (BadArity (pred_sym,a,length)),loc))
| _ -> ()
%}
%token <string*UtilsLib.ErrorMg.location> IDENT
%token <int*UtilsLib.ErrorMg.location> INT
%token <UtilsLib.ErrorMg.location>LPAR RPAR COMMA DOT FROM SLASH QUESTION_MARK
%token EOI
%start rule program extensional_facts query
%type < Datalog_AbstractSyntax.AbstractSyntax.Proto_Program.t -> Datalog_AbstractSyntax.AbstractSyntax.Proto_Program.t > rule
%type < Datalog_AbstractSyntax.AbstractSyntax.Proto_Program.t -> Datalog_AbstractSyntax.AbstractSyntax.Proto_Program.t > program
%type < (Datalog_AbstractSyntax.AbstractSyntax.Predicate.PredIdTable.table * Datalog_AbstractSyntax.ConstGen.Table.table) -> (Datalog_AbstractSyntax.AbstractSyntax.Predicate.predicate * Datalog_AbstractSyntax.AbstractSyntax.Predicate.PredIdTable.table * Datalog_AbstractSyntax.ConstGen.Table.table) > query
%type < (Datalog_AbstractSyntax.AbstractSyntax.Predicate.PredIdTable.table * Datalog_AbstractSyntax.ConstGen.Table.table*UtilsLib.IdGenerator.IntIdGen.t) -> (Datalog_AbstractSyntax.AbstractSyntax.Rule.rule list*Datalog_AbstractSyntax.ConstGen.Table.table*UtilsLib.IdGenerator.IntIdGen.t) > extensional_facts
%%
let program :=
| rules=nonempty_list(rule) ; EOI ; { fun prog -> List.fold_left (fun acc r -> r acc) prog rules }
let rule :=
| a=atom ; DOT ; { fun prog ->
AbstractSyntax.Proto_Program.add_proto_rule (a,fun t -> [],t) prog}
| head=atom ; FROM ; body=separated_nonempty_list(COMMA,atom) ; DOT ;
{ fun prog ->
AbstractSyntax.Proto_Program.add_proto_rule
(head,
fun tables ->
let body_atoms,new_tables =
List.fold_left
<