Source file db_parser.ml

type token =
  | IDENT of (
# 14 "src/datalog.prover/db_parser.mly"
        string
# 6 "src/datalog.prover/db_parser.ml"
)
  | INT of (
# 15 "src/datalog.prover/db_parser.mly"
        int
# 11 "src/datalog.prover/db_parser.ml"
)
  | LPAR
  | RPAR
  | COMMA
  | DOT
  | FROM
  | EOI
  | SLASH
  | QUESTION_MARK

open Parsing
let _ = parse_error;;
# 2 "src/datalog.prover/db_parser.mly"
  open UtilsLib
  open IdGenerator
  open Datalog_AbstractSyntax

  let check_arity pred_sym length = function
    | Some a when a<>length -> 
      let () = flush stdout in
      let () = Printf.fprintf stderr "The specified arity of predicate '%s/%d' does not match the actual number of arguments (%d)\n%!" pred_sym a length in
     raise Parsing.Parse_error
    | _ -> ()
# 35 "src/datalog.prover/db_parser.ml"
let yytransl_const = [|
  259 (* LPAR *);
  260 (* RPAR *);
  261 (* COMMA *);
  262 (* DOT *);
  263 (* FROM *);
  264 (* EOI *);
  265 (* SLASH *);
  266 (* QUESTION_MARK *);
    0|]

let yytransl_block = [|
  257 (* IDENT *);
  258 (* INT *);
    0|]

let yylhs = "\255\255\
\002\000\002\000\001\000\001\000\006\000\006\000\005\000\007\000\
\007\000\008\000\008\000\009\000\009\000\004\000\003\000\003\000\
\010\000\000\000\000\000\000\000\000\000"

let yylen = "\002\000\
\002\000\002\000\002\000\004\000\001\000\003\000\004\000\003\000\
\001\000\001\000\003\000\001\000\001\000\005\000\002\000\002\000\
\005\000\002\000\002\000\002\000\002\000"

let yydefred = "\000\000\
\000\000\000\000\000\000\000\000\000\000\000\000\018\000\000\000\
\000\000\000\000\019\000\020\000\000\000\000\000\021\000\000\000\
\000\000\003\000\000\000\000\000\001\000\002\000\000\000\015\000\
\016\000\000\000\008\000\000\000\000\000\013\000\012\000\000\000\
\000\000\000\000\000\000\000\000\004\000\007\000\000\000\000\000\
\000\000\006\000\011\000\017\000\014\000"

let yydgoto = "\005\000\
\010\000\011\000\012\000\015\000\008\000\029\000\009\000\032\000\
\033\000\014\000"

let yysindex = "\011\000\
\015\255\015\255\015\255\015\255\000\000\248\254\000\000\000\255\
\020\255\002\255\000\000\000\000\021\255\003\255\000\000\022\255\
\024\255\000\000\015\255\019\255\000\000\000\000\019\255\000\000\
\000\000\019\255\000\000\017\255\023\255\000\000\000\000\026\255\
\027\255\029\255\030\255\015\255\000\000\000\000\019\255\025\255\
\018\255\000\000\000\000\000\000\000\000"

let yyrindex = "\000\000\
\000\000\000\000\000\000\000\000\000\000\032\255\000\000\000\000\
\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
\000\000\000\000\000\000\031\255\000\000\000\000\000\000\000\000\
\034\255\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
\000\000\000\000\000\000\000\000\000\000"

let yygindex = "\000\000\
\026\000\029\000\022\000\000\000\237\255\004\000\005\000\235\255\
\000\000\000\000"

let yytablesize = 40
let yytable = "\028\000\
\017\000\034\000\006\000\006\000\035\000\018\000\019\000\013\000\
\016\000\021\000\024\000\001\000\002\000\003\000\004\000\006\000\
\028\000\043\000\013\000\030\000\031\000\036\000\020\000\023\000\
\026\000\027\000\007\000\045\000\037\000\038\000\044\000\039\000\
\040\000\041\000\009\000\025\000\005\000\010\000\022\000\042\000"

let yycheck = "\019\000\
\009\001\023\000\001\001\001\001\026\000\006\001\007\001\003\000\
\004\000\008\001\008\001\001\000\002\000\003\000\004\000\001\001\
\036\000\039\000\014\000\001\001\002\001\005\001\003\001\003\001\
\003\001\002\001\001\000\010\001\006\001\004\001\006\001\005\001\
\004\001\004\001\003\001\014\000\006\001\004\001\010\000\036\000"

let yynames_const = "\
  LPAR\000\
  RPAR\000\
  COMMA\000\
  DOT\000\
  FROM\000\
  EOI\000\
  SLASH\000\
  QUESTION_MARK\000\
  "

let yynames_block = "\
  IDENT\000\
  INT\000\
  "

let yyact = [|
  (fun _ -> failwith "parser")
; (fun __caml_parser_env ->
    let _1 = (Parsing.peek_val __caml_parser_env 1 :  Datalog_AbstractSyntax.AbstractSyntax.Proto_Program.t -> Datalog_AbstractSyntax.AbstractSyntax.Proto_Program.t ) in
    Obj.repr(
# 28 "src/datalog.prover/db_parser.mly"
            ( fun prog -> _1 prog )
# 132 "src/datalog.prover/db_parser.ml"
               :  Datalog_AbstractSyntax.AbstractSyntax.Proto_Program.t -> Datalog_AbstractSyntax.AbstractSyntax.Proto_Program.t ))
; (fun __caml_parser_env ->
    let _1 = (Parsing.peek_val __caml_parser_env 1 :  Datalog_AbstractSyntax.AbstractSyntax.Proto_Program.t -> Datalog_AbstractSyntax.AbstractSyntax.Proto_Program.t ) in
    let _2 = (Parsing.peek_val __caml_parser_env 0 :  Datalog_AbstractSyntax.AbstractSyntax.Proto_Program.t -> Datalog_AbstractSyntax.AbstractSyntax.Proto_Program.t ) in
    Obj.repr(
# 29 "src/datalog.prover/db_parser.mly"
                ( fun prog ->
   let new_prog = _1 prog in
   _2 new_prog)
# 142 "src/datalog.prover/db_parser.ml"
               :  Datalog_AbstractSyntax.AbstractSyntax.Proto_Program.t -> Datalog_AbstractSyntax.AbstractSyntax.Proto_Program.t ))
; (fun __caml_parser_env ->
    let _1 = (Parsing.peek_val __caml_parser_env 1 : 'predicate) in
    Obj.repr(
# 34 "src/datalog.prover/db_parser.mly"
                 ( fun prog -> 
   AbstractSyntax.Proto_Program.add_proto_rule (_1,fun t -> [],t) prog)
# 150 "src/datalog.prover/db_parser.ml"
               :  Datalog_AbstractSyntax.AbstractSyntax.Proto_Program.t -> Datalog_AbstractSyntax.AbstractSyntax.Proto_Program.t ))
; (fun __caml_parser_env ->
    let _1 = (Parsing.peek_val __caml_parser_env 3 : 'predicate) in
    let _3 = (Parsing.peek_val __caml_parser_env 1 : 'predicate_list) in
    Obj.repr(
# 37 "src/datalog.prover/db_parser.mly"
                                     ( fun prog -> 
   AbstractSyntax.Proto_Program.add_proto_rule (_1,_3) prog )
# 159 "src/datalog.prover/db_parser.ml"
               :  Datalog_AbstractSyntax.AbstractSyntax.Proto_Program.t -> Datalog_AbstractSyntax.AbstractSyntax.Proto_Program.t ))
; (fun __caml_parser_env ->
    let _1 = (Parsing.peek_val __caml_parser_env 0 : 'predicate) in
    Obj.repr(
# 41 "src/datalog.prover/db_parser.mly"
             (fun (pred_id_table,tables) -> 
   let predicate,(new_pred_id_table,new_tables)= _1 (pred_id_table,tables) in
   [predicate],(new_pred_id_table,new_tables) )
# 168 "src/datalog.prover/db_parser.ml"
               : 'predicate_list))
; (fun __caml_parser_env ->
    let _1 = (Parsing.peek_val __caml_parser_env 2 : 'predicate) in
    let _3 = (Parsing.peek_val __caml_parser_env 0 : 'predicate_list) in
    Obj.repr(
# 44 "src/datalog.prover/db_parser.mly"
                                  (fun (pred_id_table,tables) ->
   let predicate,(new_pred_id_table,new_tables)= _1 (pred_id_table,tables) in
   let remaining_pred,(new_pred_id_table',new_tables')=_3 (new_pred_id_table,new_tables) in
   predicate::remaining_pred,(new_pred_id_table',new_tables') )
# 179 "src/datalog.prover/db_parser.ml"
               : 'predicate_list))
; (fun __caml_parser_env ->
    let _1 = (Parsing.peek_val __caml_parser_env 3 : 'pred_id) in
    let _3 = (Parsing.peek_val __caml_parser_env 1 : 'parameters) in
    Obj.repr(
# 50 "src/datalog.prover/db_parser.mly"
                                (fun (pred_id_table,tables) ->
   let pred_sym,arity = _1 in
   let parameters,new_tables=_3 tables in
   let length=List.length parameters in
   let () = check_arity pred_sym length arity in
   let new_sym = Printf.sprintf "%s/%d" pred_sym (List.length parameters) in
   let pred_id,new_pred_id_table = AbstractSyntax.Predicate.PredIdTable.add_sym new_sym pred_id_table in
   {AbstractSyntax.Predicate.p_id=pred_id;
    AbstractSyntax.Predicate.arity=List.length parameters;
    AbstractSyntax.Predicate.arguments=parameters},(new_pred_id_table,new_tables) )
# 196 "src/datalog.prover/db_parser.ml"
               : 'predicate))
; (fun __caml_parser_env ->
    let _1 = (Parsing.peek_val __caml_parser_env 2 : string) in
    let _3 = (Parsing.peek_val __caml_parser_env 0 : int) in
    Obj.repr(
# 62 "src/datalog.prover/db_parser.mly"
                   (_1,Some _3)
# 204 "src/datalog.prover/db_parser.ml"
               : 'pred_id))
; (fun __caml_parser_env ->
    let _1 = (Parsing.peek_val __caml_parser_env 0 : string) in
    Obj.repr(
# 63 "src/datalog.prover/db_parser.mly"
         (_1,None)
# 211 "src/datalog.prover/db_parser.ml"
               : 'pred_id))
; (fun __caml_parser_env ->
    let _1 = (Parsing.peek_val __caml_parser_env 0 : 'parameter) in
    Obj.repr(
# 66 "src/datalog.prover/db_parser.mly"
             (fun tables ->
   let par,new_tables=_1 tables in
   [par],new_tables)
# 220 "src/datalog.prover/db_parser.ml"
               : 'parameters))
; (fun __caml_parser_env ->
    let _1 = (Parsing.peek_val __caml_parser_env 2 : 'parameter) in
    let _3 = (Parsing.peek_val __caml_parser_env 0 : 'parameters) in
    Obj.repr(
# 69 "src/datalog.prover/db_parser.mly"
                              (fun tables -> 
   let par,new_tables=_1 tables in
   let other_parameters,new_tables'=_3 new_tables in
   par::other_parameters,new_tables')
# 231 "src/datalog.prover/db_parser.ml"
               : 'parameters))
; (fun __caml_parser_env ->
    let _1 = (Parsing.peek_val __caml_parser_env 0 : int) in
    Obj.repr(
# 75 "src/datalog.prover/db_parser.mly"
       (fun (var_table,const_table) -> 
   let cst,new_const_table=ConstGen.Table.add_sym (string_of_int _1) const_table in
   AbstractSyntax.Predicate.Const cst,(var_table,new_const_table))
# 240 "src/datalog.prover/db_parser.ml"
               : 'parameter))
; (fun __caml_parser_env ->
    let _1 = (Parsing.peek_val __caml_parser_env 0 : string) in
    Obj.repr(
# 78 "src/datalog.prover/db_parser.mly"
         (fun (var_table,const_table) -> 
   let var,new_var_table=VarGen.Table.add_sym _1 var_table in
   AbstractSyntax.Predicate.Var var,(new_var_table,const_table))
# 249 "src/datalog.prover/db_parser.ml"
               : 'parameter))
; (fun __caml_parser_env ->
    let _1 = (Parsing.peek_val __caml_parser_env 4 : 'pred_id) in
    let _3 = (Parsing.peek_val __caml_parser_env 2 : 'parameters) in
    Obj.repr(
# 83 "src/datalog.prover/db_parser.mly"
                                               ( fun (pred_id_table,const_table) -> 
   let pred_sym,arity = _1 in
   let parameters,(_,new_const_table)=_3 (VarGen.Table.empty,const_table) in
   let length=List.length parameters in
   let () = check_arity pred_sym length arity in
   let new_sym = Printf.sprintf "%s/%d" pred_sym length in
   let pred_id,new_pred_id_table = AbstractSyntax.Predicate.PredIdTable.add_sym new_sym pred_id_table in
   {AbstractSyntax.Predicate.p_id=pred_id;
    AbstractSyntax.Predicate.arity=length;
    AbstractSyntax.Predicate.arguments=parameters},
   new_pred_id_table,new_const_table)
# 267 "src/datalog.prover/db_parser.ml"
               :  (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) ))
; (fun __caml_parser_env ->
    let _1 = (Parsing.peek_val __caml_parser_env 1 : 'extensional_fact) in
    Obj.repr(
# 101 "src/datalog.prover/db_parser.mly"
                        (fun param ->
   let r,new_cst_tble,new_gen = _1 param in
   [r],new_cst_tble,new_gen)
# 276 "src/datalog.prover/db_parser.ml"
               :  (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) ))
; (fun __caml_parser_env ->
    let _1 = (Parsing.peek_val __caml_parser_env 1 : 'extensional_fact) in
    let _2 = (Parsing.peek_val __caml_parser_env 0 :  (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) ) in
    Obj.repr(
# 104 "src/datalog.prover/db_parser.mly"
                                      (fun (pred_id_table,cst_table,gen) ->
   let r_lst,new_cst_tble,new_gen = _2 (pred_id_table,cst_table,gen) in
   let r,new_cst_tble',new_gen' = _1 (pred_id_table,new_cst_tble,new_gen) in
   r::r_lst,new_cst_tble',new_gen')
# 287 "src/datalog.prover/db_parser.ml"
               :  (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) ))
; (fun __caml_parser_env ->
    let _1 = (Parsing.peek_val __caml_parser_env 4 : 'pred_id) in
    let _3 = (Parsing.peek_val __caml_parser_env 2 : 'parameters) in
    Obj.repr(
# 110 "src/datalog.prover/db_parser.mly"
                                     ( fun (pred_id_table,const_table,rule_id_gen) -> 
   let pred_sym,arity = _1 in
   let parameters,(_,new_const_table)=_3 (VarGen.Table.empty,const_table) in
   let length=List.length parameters in
   let () = check_arity pred_sym length arity in
   let new_sym = Printf.sprintf "%s/%d" pred_sym length in
   try
     let pred_id = AbstractSyntax.Predicate.PredIdTable.find_id_of_sym new_sym pred_id_table in
     let rule_id,new_rule_id_gen=IntIdGen.get_fresh_id rule_id_gen in
     let lhs = {AbstractSyntax.Predicate.p_id=pred_id;
		AbstractSyntax.Predicate.arity=List.length parameters;
		AbstractSyntax.Predicate.arguments=parameters} in
     AbstractSyntax.Rule.({id=rule_id;
			   lhs=lhs;
			   e_rhs=[];
			   i_rhs=[];
			  i_rhs_num=0}),
     new_const_table,new_rule_id_gen
   with
   |  AbstractSyntax.Predicate.PredIdTable.Not_found -> 
     let () = flush stdout in
     let () = Printf.fprintf stderr "You try to add a fact about a predicate \"%s\" that is not a predicate of the program yet\n%!" new_sym in
     raise Parsing.Parse_error)
# 317 "src/datalog.prover/db_parser.ml"
               : 'extensional_fact))
(* Entry rule *)
; (fun __caml_parser_env -> raise (Parsing.YYexit (Parsing.peek_val __caml_parser_env 0)))
(* Entry program *)
; (fun __caml_parser_env -> raise (Parsing.YYexit (Parsing.peek_val __caml_parser_env 0)))
(* Entry extensional_facts *)
; (fun __caml_parser_env -> raise (Parsing.YYexit (Parsing.peek_val __caml_parser_env 0)))
(* Entry query *)
; (fun __caml_parser_env -> raise (Parsing.YYexit (Parsing.peek_val __caml_parser_env 0)))
|]
let yytables =
  { Parsing.actions=yyact;
    Parsing.transl_const=yytransl_const;
    Parsing.transl_block=yytransl_block;
    Parsing.lhs=yylhs;
    Parsing.len=yylen;
    Parsing.defred=yydefred;
    Parsing.dgoto=yydgoto;
    Parsing.sindex=yysindex;
    Parsing.rindex=yyrindex;
    Parsing.gindex=yygindex;
    Parsing.tablesize=yytablesize;
    Parsing.table=yytable;
    Parsing.check=yycheck;
    Parsing.error_function=parse_error;
    Parsing.names_const=yynames_const;
    Parsing.names_block=yynames_block }
let rule (lexfun : Lexing.lexbuf -> token) (lexbuf : Lexing.lexbuf) =
   (Parsing.yyparse yytables 1 lexfun lexbuf :  Datalog_AbstractSyntax.AbstractSyntax.Proto_Program.t -> Datalog_AbstractSyntax.AbstractSyntax.Proto_Program.t )
let program (lexfun : Lexing.lexbuf -> token) (lexbuf : Lexing.lexbuf) =
   (Parsing.yyparse yytables 2 lexfun lexbuf :  Datalog_AbstractSyntax.AbstractSyntax.Proto_Program.t -> Datalog_AbstractSyntax.AbstractSyntax.Proto_Program.t )
let extensional_facts (lexfun : Lexing.lexbuf -> token) (lexbuf : Lexing.lexbuf) =
   (Parsing.yyparse yytables 3 lexfun lexbuf :  (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) )
let query (lexfun : Lexing.lexbuf -> token) (lexbuf : Lexing.lexbuf) =
   (Parsing.yyparse yytables 4 lexfun lexbuf :  (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) )
;;