Commit f1ca2031 authored by SALVATI Sylvain's avatar SALVATI Sylvain

Adding the datalog parsing component

parent 10b6f434
This diff is collapsed.
module Datalog_solver =
struct
open Program
type item = It of (int*int list)
type eval_rule = ER of (predicate* predicate * predicate list * int Int_map.t ) (* the first predicate is the conclusion, the second is the next that need to be identified, the list contains the predicates that need to be proved and the int_map is the substitution that has been computed so far.*)
type result = RER of eval_rule | RIt of item
exception Not_unifiable
let get_eval_rule (Cl(lhs,rhs)) =
(match rhs with
[] -> failwith "get_eval_rule: rule with an empty right hand side?"
| pred::rhs_tl -> ER (lhs, pred, rhs_tl, Int_map.empty)
)
let instanciate (Pred(k,args)) subst =
It(k,
List.fold_right
(function arg ->
function l ->
(Int_map.find arg subst)::l
)
args
[]
)
let rec eliminate_eq_neq predicates eq neq subst =
(match predicates with
Pred(k,[arg1;arg2])::predicates_tl ->
if k=eq
then
(try
let k1 = Int_map.find arg1 subst in
(try
let k2 = Int_map.find arg2 subst in
if k1 = k2
then eliminate_eq_neq predicates_tl eq neq subst
else raise Not_unifiable
with
Not_found ->
eliminate_eq_neq predicates_tl eq neq
(Int_map.add arg2 k1 subst)
)
with Not_found ->
(try
let k2 = Int_map.find arg2 subst in
eliminate_eq_neq predicates_tl eq neq
(Int_map.add arg1 k2 subst)
with
Not_found ->
raise Not_unifiable
)
)
else
(if k=neq
then
(try
let k1 = Int_map.find arg1 subst in
(try
let k2 = Int_map.find arg2 subst in
if k1 != k2
then eliminate_eq_neq predicates_tl eq neq subst
else raise Not_unifiable
with
Not_found ->
raise Not_unifiable
)
with
Not_found ->
raise Not_unifiable
)
else
(subst,predicates)
)
|_ -> (subst,predicates)
)
module Ordered_items =
struct
type t = item
let compare k1 k2 = Pervasives.compare k1 k2
end
module Ordered_eval_rules =
struct
type t = eval_rule
let compare k1 k2 = Pervasives.compare k1 k2
end
module Item_set = Set.Make(Ordered_items)
module Item_map = Map.Make(Ordered_items)
module ER_set = Set.Make(Ordered_eval_rules)
type chart =(int Item_map.t) array (*array whose ith address contains the function f whose domain contains the lists args such that the ith predicate holds for the list args and that this fact has been added at the kth step of the algo wher k = f(args)*)
type eval_rules = (ER_set.t) array (*array whose ith address contains the eval_rules that can be completed by an instance of the ith predicate *)
type agenda = Item_set.t (*set containing pairs (predicate identifier, arg instanciation)*)
type memory = M of (Signature.signature*chart*eval_rules*agenda*(item list)*int*int*int)
exception No_more_step
let get_predicates_in_chart k (M(_,chart,_,_,_,_,_,_)) = (Array.get chart k)
let add_mem (It(k,_) as item) (M(sign,chart,ev_rules,agenda,facts,step,eq,neq) as mem) =
if Item_map.mem item (get_predicates_in_chart k mem)
then mem
else
let agenda = Item_set.add item agenda in
M(sign,chart,ev_rules,agenda,facts,step,eq,neq)
let ev_rule_known (ER(_,Pred(k,_),_,_)as ev_rule) (M(_,_,ev_rules,_,_,_,_,_)) =
ER_set.mem ev_rule (Array.get ev_rules k)
let add_ev_rule (ER(_,Pred(k,_),_,_)as ev_rule) (M(sign,chart,ev_rules,agenda,facts,step,eq,neq)) =
Array.set ev_rules k (ER_set.add ev_rule (Array.get ev_rules k));
M(sign,chart,ev_rules,agenda,facts,step,eq,neq)
let rec extend_eval_rule
(ER(res,Pred(k,args_pred),predicates,subst))
(It(l,args_item))
(M(_,_,_,_,_,_,eq,neq) as mem)
=
(if k=l
then
(try
let subst =
List.fold_left2
(function subst ->
function arg_pred->
function arg_item->
(try
let k = Int_map.find arg_pred subst in
if k = arg_item
then subst
else raise Not_unifiable
with
Not_found ->
(Int_map.add arg_pred arg_item subst)
)
)
subst
args_pred
args_item
in
(match eliminate_eq_neq predicates eq neq subst with
(subst,[]) ->
(try
add_mem (instanciate res subst) mem
with Not_found ->
(match res with Pred(k,_) -> failwith ("PB: pred "^(string_of_int k))))
| (subst,(Pred(k,_) as pred)::predicates) ->
let ev_rule = (ER(res,pred,predicates,subst)) in
if ev_rule_known ev_rule mem
then mem
else
let mem = add_ev_rule ev_rule mem in
Item_map.fold
(function item ->
function _ ->
function mem ->
extend_eval_rule
ev_rule
item
mem
)
(get_predicates_in_chart k mem)
mem
)
with
Not_unifiable -> mem
)
else failwith "extend_eval_rule: trying to extend a rule with a rong item.")
let rec process_item (It(pred,_) as item) (M(_,_,ev_rules,_,_,_,_,_) as mem) =
let pred_ev_rules = Array.get ev_rules pred in
let (M(sign,chart,ev_rules,agenda,facts,step,eq,neq)) =
ER_set.fold
(function ev_rule ->
function mem ->
extend_eval_rule ev_rule item mem
)
pred_ev_rules
mem
in
let agenda = Item_set.remove item agenda in
let _ = Array.set
chart
pred
(Item_map.add item step (Array.get chart pred))
in
M(sign,chart,ev_rules,agenda,facts,step,eq,neq)
let next_step (M(sign,chart,ev_rules,agenda,facts,step,eq,neq)) =
(match facts with
[] -> raise No_more_step
| fact::remaining_facts ->
let _ = print_string ("Make step: "^(string_of_int (step+1))^".\n") in
M(sign,chart,ev_rules,Item_set.add fact agenda,remaining_facts,step+1,eq,neq)
)
let rec naive_solve (M(sign,chart,ev_rules,agenda,facts,step,eq,neq) as mem)=
if(Item_set.is_empty agenda)
then
(if facts=[]
then mem
else naive_solve(next_step mem))
else
naive_solve(process_item (Item_set.choose agenda) mem)
let init_solver program facts =
match program with
Prog(sign,clauses) ->
let n = Signature.fresh sign in
let chart = Array.make n (Item_map.empty) in
let ev_rules = Array.make n (ER_set.empty) in
let agenda = Item_set.empty in
let step = -1 in
let (eq,sign) = Signature.add_eq_get_id sign in
let (neq,sign) = Signature.add_neq_get_id sign in
let _ =
List.fold_left
(function () ->
function Cl(pred,(Pred(k,args) as fst)::rem) ->
let ev_rule = ER(pred,fst,rem,Int_map.empty) in
Array.set ev_rules k (ER_set.add ev_rule (Array.get ev_rules k))
|_ -> failwith "init_solver: the program contains a clause with no rhs."
)
()
clauses
in
M(sign,chart,ev_rules,agenda,facts,step,eq,neq)
let init_solver2 program list magic =
let Prog(sign,_) = program in
let (_,facts) =
List.fold_left
(function (n,l) ->
function string ->
try
let (_,pred) = Signature.find_pred_of_name string sign in
(n+1,It(pred,[n;n+1])::l)
with
Not_found ->
failwith ("init_solver2: predicate '"^string^"' is not defined.")
)
(0,[])
list
in
init_solver
program
(It(magic,[0])::(List.rev facts))
let solve program facts = naive_solve(init_solver program facts)
let solve2 program list magic = naive_solve(init_solver2 program list magic)
let print_chart (M(sign,chart,_,_,_,step,_,_)) =
let res = Array.make (step+1) [] in
let _ =
Array.fold_right
(function set ->
function () ->
Item_map.fold
(function It(k,args)->
function step0 ->
function () ->
Array.set
res
step0
((Signature.get_name k sign,args)::(Array.get res step0))
)
set
()
)
chart
()
in
res
end
module Datalog_syn =
struct
(*
The grammar:
RULES -> Ident LHS_ARGS | EMPTY
LHS_ARGS -> LPAR LHS_ARGS_LIST
LHS_ARGS_LIST -> Ident LHS_ARGS_STRUCT
LHS_ARGS_STRUCT -> RPAR RHS | COMMA LHS_ARGS_LIST
RHS -> SEP PREMISSES
PREMISSES -> Ident PRED_OR_EQ | EQ EQ_ARGS | NEQ EQ_ARGS
PRED_OR_EQ -> LPAR RHS_ARGS_LIST | EQ EQ_STRUCT | NEQ EQ_STRUCT
EQ_STRUCT -> Ident PREMISSES_STRUCT
EQ_ARGS -> LPAR RHS_ARGS_LIST
PREMISSES_STRUCT -> COMMA PREMISSES | PERIOD RULES
RHS_ARGS_LIST -> Ident RHS_ARGS_STRUCT
RHS_ARGS_STRUCT -> RPAR PREMISSES_STRUCT | COMMA RHAS_ARGS_LIST
*)
open Lexicalizer
type parse_context =
{
mutable sign: Signature.signature; (*signature under construction*)
mutable pos_before_token : pos; (*position right befor the present token*)
mutable pos: pos; (*position in the stream*)
mutable variables: ((int*bool) String_map.t); (*variables of a rule, it associates to the name its identifer and a boolean which specifies whether the variable has an occurrence in the right hand side of a clause*)
mutable lhs: Program.predicate option; (*possible current lhs*)
mutable rhs: Program.predicate list; (*rhs of the current rule*)
mutable current_pred_name: string; (*name of the current predicate*)
mutable arguments: int list; (*list of arguments of the current predicate*)
mutable arity: int; (*number of arguments of the current predicate*)
mutable fresh: int; (*the next fresh identifier for variables*)
mutable clauses: Program.clause list
}
let empty_parse_context () =
{
sign = Signature.empty;
pos_before_token = first_pos;
pos = first_pos;
variables = String_map.empty;
lhs = None;
rhs = [];
current_pred_name = "";
arguments = [];
arity = 0;
fresh = 0;
clauses=[]
}
let parse_error parse_context message =
let P(line,col) = parse_context.pos in
let P(line_b,col_b) = parse_context.pos_before_token in
let col_string =
if col >col_b
then
(string_of_int col_b)^"-"^(string_of_int col)
else string_of_int col
in failwith ("Line: "^string_of_int(line)^", Col: "^col_string^". "^message)
let get_predicate_id parse_context =
let name = parse_context.current_pred_name in
(try
let (ar,id) = Signature.find_pred_of_name name parse_context.sign in
if ar = parse_context.arity
then id
else parse_error parse_context
("The predicate "^name^" should have arity "^string_of_int (ar)^" but is used with arity "^string_of_int(parse_context.arity)^".")
with Not_found->
let (id,sign) = Signature.add_pred_get_id parse_context.arity name parse_context.sign in
parse_context.sign <- sign;
id
)
let set_current_pred name parse_context =
parse_context.current_pred_name <- name
let make_lhs parse_context =
(let id = get_predicate_id parse_context in
parse_context.lhs <- Some(Program.Pred(id,List.rev parse_context.arguments));
parse_context.arguments <- [];
parse_context.arity <- 0
)
let add_lhs_arg var_name parse_context =
(try
let (id,_) = String_map.find var_name parse_context.variables in
parse_context.arity <- parse_context.arity+1;
parse_context.arguments <- (id::parse_context.arguments)
with
Not_found ->
let fresh = parse_context.fresh in
parse_context.variables <- (String_map.add var_name (fresh,false) parse_context.variables);
parse_context.arguments <- (fresh::parse_context.arguments);
parse_context.arity <- parse_context.arity+1;
parse_context.fresh <- fresh+1
)
let add_rhs_arg var_name parse_context =
(try
let (id,right) = String_map.find var_name parse_context.variables in
parse_context.arguments <- (id::parse_context.arguments);
parse_context.arity <- parse_context.arity+1;
(if right
then ()
else
parse_context.variables <- (String_map.add var_name (id,true) parse_context.variables)
)
with
Not_found ->
let fresh = parse_context.fresh in
parse_context.variables <- (String_map.add var_name (fresh,true) parse_context.variables);
parse_context.arguments <- (fresh::parse_context.arguments);
parse_context.arity <- parse_context.arity+1;
parse_context.fresh <- fresh+1
)
let make_rhs_pred parse_context =
let id = get_predicate_id parse_context in
parse_context.rhs <- ((Program.Pred(id, List.rev parse_context.arguments))::parse_context.rhs);
parse_context.arguments <- [];
parse_context.arity <- 0
let make_clause parse_context =
match parse_context.lhs with
Some pred ->
parse_context.clauses <- ((Program.Cl(pred,List.rev parse_context.rhs))::parse_context.clauses);
parse_context.variables <- String_map.empty;
parse_context.lhs <- None;
parse_context.rhs <- [];
parse_context.current_pred_name <- "";
parse_context.fresh <- 0;
| None -> failwith "make_clause: no lhs for clause"
let make_program parse_context =
Program.Prog(parse_context.sign,List.rev parse_context.clauses)
let parse stream =
let parse_context = empty_parse_context() in
let get_token ()=
let tk = next_token stream parse_context.pos in
(match tk with
Some(Ident(_,pb) as res,p)
| Some(Str(_,pb) as res,p)
| Some(INIT(pb) as res,p)
| Some(EQ(pb) as res,p)
| Some(NEQ(pb) as res,p)
| Some(SEP(pb) as res,p)
| Some(LPAR(pb) as res,p)
| Some(RPAR(pb) as res,p)
| Some(COMMA(pb) as res,p)
| Some(PERIOD(pb) as res,p)
| Some(SEMICOL(pb) as res,p) ->
parse_context.pos_before_token <- pb;
parse_context.pos <- p;
Some res
| None ->
parse_context.pos_before_token <-parse_context.pos;
None
);
in
let rec rules ()=
(match get_token () with
Some(Ident(name,_)) ->
set_current_pred name parse_context;
lhs_args ()
| None -> make_program parse_context
|_ -> parse_error parse_context "Identifier expected."
)
and lhs_args () =
(match get_token () with
Some(LPAR(_)) -> lhs_args_list()
| _ -> parse_error parse_context "'(' expected."
)
and lhs_args_list () =
(match get_token () with
Some(Ident(name,_)) ->
add_lhs_arg name parse_context;
lhs_args_struct()
|_ -> parse_error parse_context "Identifier expected."
)
and lhs_args_struct () =
(match get_token() with
Some(RPAR(_)) ->
make_lhs parse_context;
rhs()
| Some(COMMA(_)) ->
lhs_args_list()
|_ -> parse_error parse_context "',' or ')' expected."
)
and rhs () =
(match get_token() with
Some(SEP(_)) -> premisses()
|_ -> parse_error parse_context "':-' expected."
)
and premisses ()=
(match get_token() with
Some(Ident(name,_)) -> pred_or_eq name
| Some(EQ(_)) ->
set_current_pred "=" parse_context;
parse_context.sign <- (Signature.add_eq parse_context.sign);
eq_args ()
| Some(NEQ(_)) ->
set_current_pred "~=" parse_context;
parse_context.sign <- (Signature.add_neq parse_context.sign);
eq_args ()
|_ -> parse_error parse_context "Identifier, '=', or '~=' expected."
)
and pred_or_eq name =
(match get_token() with
Some(LPAR(_)) ->
set_current_pred name parse_context;
rhs_args_list()
| Some(EQ(_)) ->
set_current_pred "=" parse_context;
parse_context.sign <- (Signature.add_eq parse_context.sign);
add_rhs_arg name parse_context;
eq_struct()
| Some(NEQ(_)) ->
set_current_pred "~=" parse_context;
parse_context.sign <- (Signature.add_neq parse_context.sign);
eq_struct()
|_ -> parse_error parse_context "'(' or '=' expected."
)
and eq_struct () =
(match get_token() with
Some(Ident(name,_)) ->
add_rhs_arg name parse_context;
make_rhs_pred parse_context;
premisses_struct()
|_ -> parse_error parse_context "Identifier expected."
)
and eq_args () =
(match get_token() with
Some(LPAR(_)) -> rhs_args_list()
|_ -> parse_error parse_context "'(' expected."
)
and premisses_struct ()=
(match get_token() with
Some(COMMA(_)) -> premisses ()
| Some(PERIOD(_)) ->
make_clause parse_context;
rules ()
|_ -> parse_error parse_context "',' or ',' expected."
)
and rhs_args_list () =
(match get_token() with
Some(Ident(name,_)) ->
add_rhs_arg name parse_context;
rhs_args_struct()
|_ -> parse_error parse_context "Identifier expected."
)
and rhs_args_struct () =
(match get_token() with
Some(RPAR(_)) ->
make_rhs_pred parse_context;
premisses_struct();
| Some(COMMA(_)) ->
rhs_args_list()
|_ -> parse_error parse_context "')' or ',' expected."
)
in rules ()
end
init = s;
s("");
s(x1 x3) :- p(x1,x2,x3);
p("a" x1 x2 x2, "a" x2, "b" x3) :- p(x1,x2,x3);
p("a","a","b");
\ No newline at end of file
module Int_map = Map.Make(
struct
type t=int
let compare = Pervasives.compare
end
)
module Int_set = Set.Make (struct type t=int let compare=compare end)
init = s;
s(x1 y1 x2 y2) :- p(x1,x2) q(y1,y2);
p("a1" "a2", "a3" "a4");
p("a1" x1 "a2","a3" x2 "a4") :- p(x1,x2);
q("b1" "b2", "b3" "b4");
q("b1" y1 "b2","b3" y2 "b4") :- q(y1,y2);
module Kanazawa_transform =
struct
let is_impermissible n=
let rec check adornment =
match adornment with
[] -> false
| false::true::_ -> true
| _::_::adornment -> check adornment
| _::[] -> false
in
function Adornment.AdP(k,adornment) ->
k<n && (check adornment)
let is_impermissible2 n=
let rec check has_bound_var adornment =
match adornment with
[] -> has_bound_var
| false::true::_ -> true
| true::_::adornment -> check true adornment
| false::false::adornment -> check has_bound_var adornment
| _::[] -> true
in
function Adornment.AdP(k,adornment) ->
k<n && (check false adornment)
(*let is_impermissible3 =
let rec check adornment =
match adornment with
[] -> false
| false::true::_ -> true
| false::false::_ -> true