Commit e6e7ac6b authored by POGODALLA Sylvain's avatar POGODALLA Sylvain

Possibly fixed the bug when duplicated interpretations are provided in...

Possibly fixed the bug when duplicated interpretations are provided in lexicons for which a datalog program is generated (i.e. with 2nd order abstract language and almost linear interpretations)
parent ce3fe260
......@@ -2,6 +2,32 @@
* Général
** BUG:
+ [ ] si 2 déclarations d'interprétations de la même constante dans un lexique, plusieurs solutions de parsing. Minmal example:
signature abs =
o:type;
a:o->o;
HASH:o;
end
signature strings =
o:type;
a:o->o;
epsilon = lambda x.x:o->o;
end
lexicon form(abs):strings=
o:= o->o;
a := lambda s. lambda z. a (s z);
a := lambda s. lambda z. a (s z);
HASH := epsilon;
end
# load o essai2.acgo;
# form parse a:o;
-> 2 analyses.
** TODO Avant Prochaine release
+ [X] merge avec trunk
+ [X] remplacer tous les gforge.loria en gforge.inria
......
......@@ -25,3 +25,4 @@ homepage: "http://acg.gforge.inria.fr/"
license: "CeCILL"
authors: ["Sylvain Pogodalla"]
bug-reports: "sylvain.pogodalla@inria.fr"
dev-repo: ""
......@@ -52,6 +52,10 @@ struct
module RuleToCstMap=Utils.IntMap
type datalog_correspondance = {prog:Datalog.Program.program;
rule_to_cst: Lambda.term RuleToCstMap.t;
cst_to_rule: int Utils.IntMap.t}
type 'a build =
| Interpret of (Sg.t*Sg.t)
| Compose of ('a*'a)
......@@ -62,9 +66,10 @@ struct
non_linear_interpretation:bool;
abstract_sig:Sg.t;
object_sig:Sg.t;
datalog_prog:(Datalog.Program.program * Lambda.term RuleToCstMap.t) option;
build:t build;
timestamp:float}
(* datalog_prog:(Datalog.Program.program * Lambda.term RuleToCstMap.t) option; *)
datalog_prog: datalog_correspondance option;
build:t build;
timestamp:float}
type dependency =
......@@ -90,7 +95,10 @@ struct
let prog =
(* if (Sg.is_2nd_order abs) && (not non_linear) then *)
if (Sg.is_2nd_order abs) then
Some (Datalog.Program.empty,RuleToCstMap.empty)
(* Some (Datalog.Program.empty,RuleToCstMap.empty) *)
Some {prog=Datalog.Program.empty;
rule_to_cst=RuleToCstMap.empty;
cst_to_rule=Utils.IntMap.empty}
else
None in
{name=name;
......@@ -156,7 +164,8 @@ struct
module Reduction=Reduction.Make(Sg)
let add_rule_for_cst_in_prog name abs_type interpreted_term lex (prog,rule_to_cst) =
(* let add_rule_for_cst_in_prog name abs_type interpreted_term lex (prog,rule_to_cst) = *)
let add_rule_for_cst_in_prog name duplicated abs_type interpreted_term lex {prog;rule_to_cst;cst_to_rule} =
let interpreted_type = (interpret_type abs_type lex) in
let eta_long_term =
Sg.eta_long_form
......@@ -182,47 +191,61 @@ struct
~abs_sig:lex.abstract_sig
~obj_sig:lex.object_sig in
let cst_id,_ = Sg.find_term name lex.abstract_sig in
new_prog,RuleToCstMap.add rule.Datalog_AbstractSyntax.AbstractSyntax.Rule.id cst_id rule_to_cst
let cst_id_as_int =
match cst_id with
| Lambda.Const i -> i
| _ -> failwith "Bug: Trying to add a rule that does not correspond to a constant" in
let new_prog'=
if duplicated then
Datalog.Program.remove_rule (Utils.IntMap.find cst_id_as_int cst_to_rule) rule.Datalog_AbstractSyntax.AbstractSyntax.Rule.lhs.Datalog_AbstractSyntax.AbstractSyntax.Predicate.p_id new_prog
else
new_prog in
(* new_prog,RuleToCstMap.add rule.Datalog_AbstractSyntax.AbstractSyntax.Rule.id cst_id rule_to_cst *)
{prog=new_prog';
rule_to_cst=RuleToCstMap.add rule.Datalog_AbstractSyntax.AbstractSyntax.Rule.id cst_id rule_to_cst;
cst_to_rule=Utils.IntMap.add cst_id_as_int rule.Datalog_AbstractSyntax.AbstractSyntax.Rule.id cst_to_rule
}
let insert e ({dico=d} as lex) = match e with
| Abstract_syntax.Type (id,loc,ty) ->
let interpreted_type = Sg.convert_type ty lex.object_sig in
let interpreted_type =
if lex.non_linear_interpretation then
Lambda.unlinearize_type interpreted_type
else
interpreted_type in
{lex with dico=Dico.add id (Type (loc,interpreted_type)) d}
let interpreted_type = Sg.convert_type ty lex.object_sig in
let interpreted_type =
if lex.non_linear_interpretation then
Lambda.unlinearize_type interpreted_type
else
interpreted_type in
{lex with dico=Dico.add id (Type (loc,interpreted_type)) d}
| Abstract_syntax.Constant (id,loc,t) ->
let abs_type=Sg.expand_type (Sg.type_of_constant id lex.abstract_sig) lex.abstract_sig in
let interpreted_type =
if lex.non_linear_interpretation then
interpret_type (Lambda.unlinearize_type abs_type) lex
else
interpret_type abs_type lex in
let t =
if lex.non_linear_interpretation then
Abstract_syntax.unlinearize_term t
else
t in
let unfold i =
if lex.non_linear_interpretation then
Lambda.unlinearize_term (Sg.unfold_term_definition i lex.object_sig)
else
Sg.unfold_term_definition i lex.object_sig in
let interpreted_term =
Lambda.normalize
~id_to_term:unfold
(Sg.typecheck t interpreted_type lex.object_sig) in
let prog = match lex.datalog_prog with
| None -> None
| Some p ->
let new_prog= add_rule_for_cst_in_prog id abs_type (Signature.expand_term interpreted_term lex.object_sig) lex p in
Some new_prog in
{lex with
dico=Dico.add id (Constant (loc,interpreted_term)) d;
datalog_prog =prog}
let abs_type=Sg.expand_type (Sg.type_of_constant id lex.abstract_sig) lex.abstract_sig in
let interpreted_type =
if lex.non_linear_interpretation then
interpret_type (Lambda.unlinearize_type abs_type) lex
else
interpret_type abs_type lex in
let t =
if lex.non_linear_interpretation then
Abstract_syntax.unlinearize_term t
else
t in
let unfold i =
if lex.non_linear_interpretation then
Lambda.unlinearize_term (Sg.unfold_term_definition i lex.object_sig)
else
Sg.unfold_term_definition i lex.object_sig in
let interpreted_term =
Lambda.normalize
~id_to_term:unfold
(Sg.typecheck t interpreted_type lex.object_sig) in
let prog = match lex.datalog_prog with
| None -> None
| Some p ->
let duplicate_entry = Dico.mem id d in
let new_prog= add_rule_for_cst_in_prog id duplicate_entry abs_type (Signature.expand_term interpreted_term lex.object_sig) lex p in
Some new_prog in
{lex with
dico=Dico.add id (Constant (loc,interpreted_term)) d;
datalog_prog =prog}
let rebuild_prog lex =
match lex.datalog_prog with
......@@ -236,12 +259,14 @@ struct
| Constant (l,t) ->
add_rule_for_cst_in_prog
key
false (* When rebuilding, no risk of dublicated interpretations *)
(Sg.expand_type (Sg.type_of_constant key lex.abstract_sig) lex.abstract_sig)
t
lex
acc)
lex.dico
(Datalog.Program.empty,RuleToCstMap.empty) in
(* (Datalog.Program.empty,RuleToCstMap.empty) in *)
{prog=Datalog.Program.empty;rule_to_cst=RuleToCstMap.empty;cst_to_rule=Utils.IntMap.empty} in
{lex with datalog_prog=Some new_prog}
......@@ -250,7 +275,8 @@ struct
| None,_ ->
let () = Printf.printf "Parsing is not implemented for non 2nd order ACG\n!" in
SharedForest.SharedForest.empty
| Some (prog,_), (Lambda.Atom _ as dist_type) ->
(* | Some (prog,_), (Lambda.Atom _ as dist_type) -> *)
| Some {prog}, (Lambda.Atom _ as dist_type) ->
let buff=Buffer.create 80 in
let () = Buffer.add_buffer buff (Datalog_AbstractSyntax.AbstractSyntax.Program.to_buffer (Datalog.Program.to_abstract prog)) in
LOG "Before parsing. Program is currently:" LEVEL DEBUG;
......@@ -307,7 +333,8 @@ struct
LOG "Trying to get some analysis" LEVEL DEBUG;
match lex.datalog_prog with
| None -> let () = Printf.printf "Parsing is not yet implemented for non atomic distinguished type\n%!" in None,resume
| Some (_,rule_id_to_cst) ->
(* | Some (_,rule_id_to_cst) -> *)
| Some {rule_to_cst=rule_id_to_cst} ->
match SharedForest.SharedForest.resumption resume with
| None,resume -> None,resume
| Some t,resume ->
......@@ -339,7 +366,9 @@ struct
let () = Printf.bprintf buff "\n************************\n" in
let () = match lex.datalog_prog with
| None -> Printf.bprintf buff "This lexicon was not recognized as having a 2nd order abstract signature\n"
| Some (p,_) -> let () = Printf.bprintf buff "This lexicon recognized as having a 2nd order abstract signature. The associated datalog program is:\n" in
(* | Some (p,_) -> *)
| Some {prog=p} ->
let () = Printf.bprintf buff "This lexicon recognized as having a 2nd order abstract signature. The associated datalog program is:\n" in
Buffer.add_buffer buff (Datalog_AbstractSyntax.AbstractSyntax.Program.to_buffer (Datalog.Program.to_abstract p)) in
Buffer.contents buff
......@@ -370,7 +399,8 @@ struct
let prog =
(* if (Sg.is_2nd_order lex.abstract_sig) && (not lex.non_linear_interpretation) then *)
if (Sg.is_2nd_order lex.abstract_sig) then
Some (Datalog.Program.empty,RuleToCstMap.empty)
(* Some (Datalog.Program.empty,RuleToCstMap.empty) *)
Some {prog=Datalog.Program.empty;rule_to_cst=RuleToCstMap.empty;cst_to_rule=Utils.IntMap.empty}
else
None in
let new_lex =
......@@ -407,7 +437,8 @@ struct
let buff=Buffer.create 80 in
let () = match lex.datalog_prog with
| None -> Printf.bprintf buff "This lexicon was not recognized as having a 2nd order abstract signature\n"
| Some (p,_) ->
(* | Some (p,_) -> *)
| Some {prog=p} ->
let () = Printf.bprintf buff "This lexicon recognized as having a 2nd order abstract signature. The associated datalog program is:\n" in
Buffer.add_buffer buff (Datalog_AbstractSyntax.AbstractSyntax.Program.to_buffer (Datalog.Program.to_abstract p)) in
buff
......@@ -420,7 +451,8 @@ struct
let buff=Buffer.create 80 in
let () = Printf.bprintf buff "Parsing is not implemented for non 2nd order ACG\n!" in
buff
| Some (prog,_), (Lambda.Atom _ as dist_type) ->
(* | Some (prog,_), (Lambda.Atom _ as dist_type) -> *)
| Some {prog}, (Lambda.Atom _ as dist_type) ->
let dist_type_image = interpret_type dist_type lex in
let obj_term=
Sg.eta_long_form
......
......@@ -76,7 +76,8 @@ sig
module Program :
sig
type program = {
rules : Rule.rule list Predicate.PredMap.t;
(* rules : Rule.rule list Predicate.PredMap.t; *)
rules : Rule.Rules.t Predicate.PredMap.t;
edb : ASPred.pred_id list;
edb_facts:Predicate.FactSet.t Predicate.PredMap.t;
idb : ASPred.pred_id list;
......@@ -116,8 +117,18 @@ sig
should be empty.*)
val add_rule : intensional:bool -> ASRule.rule -> program -> program
(** [remove_rule id p] returns the program [p] from which the rule
with id [id] has been removed.
IMPORTANT: This function only deals with rules introducing
intensional predicate, because it is used when a constant is
given several interpretations in a lexicon.
*)
val remove_rule : int -> ASPred.pred_id -> program -> program
val get_fresh_rule_id : program -> (int * program)
val get_fresh_cst_id : string -> program -> (Datalog_AbstractSyntax.ConstGen.id * program)
val add_pred_sym : string -> program -> (ASPred.pred_id*program)
......@@ -128,23 +139,23 @@ sig
val edb_to_buffer : program -> Buffer.t
end
end
end
end
module Make (S:UnionFind.Store) =
struct
exception Fails
module UF= UnionFind.Make(S)
module Make (S:UnionFind.Store) =
struct
exception Fails
module UF= UnionFind.Make(S)
module Predicate =
struct
module Predicate =
struct
(** For the type of the predicates, we use the same identifiers as
for the predicates of the datalog abstract syntax {!
Datalog_AbstractSyntax.AbstractSyntax.Predicate} *)
for the predicates of the datalog abstract syntax {!
Datalog_AbstractSyntax.AbstractSyntax.Predicate} *)
type predicate={p_id:ASPred.pred_id;
arity:int;
}
......@@ -678,9 +689,13 @@ struct
module Program =
struct
type program = {rules:Rule.rule list Predicate.PredMap.t;
type program = {
(* rules : Rule.rule list Predicate.PredMap.t; *)
(* the list of the rules of the program indexed by
the id of the lhs predicate *)
rules : Rule.Rules.t Predicate.PredMap.t;
(* the set of the rules of the program indexed by
the id of the lhs predicate *)
edb:ASPred.pred_id list;
(* the list of the ids of the extensional
predicates *)
......@@ -730,6 +745,15 @@ struct
with
| Not_found -> Predicate.PredMap.add k [v] map_list
let extend_map_to_rule_set k v map_to_set =
let current_set =
try
Predicate.PredMap.find k map_to_set
with
| Not_found -> Rule.Rules.empty in
Predicate.PredMap.add k (Rule.Rules.add v current_set) map_to_set
let extend_map_to_set k v map_to_set =
let current_set =
try
......@@ -751,7 +775,8 @@ struct
extend_map_to_set lhs.ASPred.p_id lhs e_facts
else
e_facts in
extend_map_to_list lhs.ASPred.p_id new_rule acc,updated_e_facts,ASRule.RuleMap.add r new_rule r_to_r)
(* extend_map_to_list lhs.ASPred.p_id new_rule acc,updated_e_facts,ASRule.RuleMap.add r new_rule r_to_r *)
extend_map_to_rule_set lhs.ASPred.p_id new_rule acc,updated_e_facts,ASRule.RuleMap.add r new_rule r_to_r)
r
(Predicate.PredMap.empty,Predicate.PredMap.empty,ASRule.RuleMap.empty) in
LOG "All rules done." LEVEL TRACE;
......@@ -788,7 +813,7 @@ struct
let to_abstract {rules=r;idb=idb;pred_table=pred_table;const_table=cst_table;rule_id_gen;edb_facts(*e_pred_to_rules*)} =
LOG "Transforming internal rules into abastract ones..." LEVEL TRACE;
let rules =
(* let rules =
Predicate.PredMap.fold
(fun _ rules acc ->
List.fold_left
......@@ -797,6 +822,16 @@ struct
acc
rules)
r
ASRule.Rules.empty in *)
let rules =
Predicate.PredMap.fold
(fun _ rules acc ->
Rule.Rules.fold
(fun rule acc' ->
ASRule.Rules.add (Rule.to_abstract rule rule.Rule.content pred_table) acc')
rules
acc)
r
ASRule.Rules.empty in
LOG "Done." LEVEL TRACE;
LOG "Transforming facts into rules" LEVEL TRACE;
......@@ -959,7 +994,7 @@ struct
http://webdam.inria.fr/Alice/pdfs/Chapter-13.pdf} Chap. 13 of
"Foundations of Databases", Abiteboul, Hull, and Vianu} *)
let p_semantics_for_predicate s_id prog e_facts previous_step_facts facts delta_facts derivations =
List.fold_left
(* List.fold_left
(fun acc r ->
temp_facts
r
......@@ -978,7 +1013,27 @@ struct
prog.pred_table
prog.const_table)
(Predicate.FactSet.empty,derivations)
(Predicate.PredMap.find s_id prog.rules) *)
Rule.Rules.fold
(fun r acc ->
temp_facts
r
e_facts
previous_step_facts
facts
delta_facts
(fun (new_fact,from_premises) r (new_fact_set,new_fact_derivations) ->
(Predicate.conditionnal_add
new_fact
new_fact_set
(custom_find r.Rule.lhs.Predicate.p_id previous_step_facts)
(custom_find r.Rule.lhs.Predicate.p_id delta_facts),
Predicate.add_to_map_to_set new_fact (from_premises,r.Rule.id,r.Rule.i_rhs_num) new_fact_derivations))
acc
prog.pred_table
prog.const_table)
(Predicate.PredMap.find s_id prog.rules)
(Predicate.FactSet.empty,derivations)
let seminaive prog =
(** [seminaive_aux facts delta_facts] returns [(S]{^
......@@ -1069,10 +1124,12 @@ struct
try
Predicate.PredMap.add
lhs.Predicate.p_id
(rule::(List.filter Rule.(fun r -> r.id=rule.id) (Predicate.PredMap.find lhs.Predicate.p_id acc)))
(* (rule::(List.filter Rule.(fun r -> r.id=rule.id) (Predicate.PredMap.find lhs.Predicate.p_id acc))) *)
Rule.(Rules.add rule (Rules.filter (fun r -> r.id=rule.id) (Predicate.PredMap.find lhs.Predicate.p_id acc)))
acc
with
| Not_found -> Predicate.PredMap.add lhs.Predicate.p_id [rule] acc)
(* | Not_found -> Predicate.PredMap.add lhs.Predicate.p_id [rule] acc) *)
| Not_found -> Predicate.PredMap.add lhs.Predicate.p_id Rule.Rules.(add rule empty) acc)
internal_modified_rules
prog.rules in
{rules=updated_rules;
......@@ -1179,12 +1236,27 @@ struct
| false,_,_ -> failwith "Bug: addition of a rule for an extensional predicate with non empty rhs"
| true,_,_ -> prog.edb_facts,prog.edb,list_extension lhs_pred prog.idb in
{prog with
rules=extend_map_to_list lhs_pred new_rule prog.rules;
(* rules=extend_map_to_list lhs_pred new_rule prog.rules; *)
rules=extend_map_to_rule_set lhs_pred new_rule prog.rules;
edb_facts=new_e_facts;
edb=new_edb;
idb=new_idb}
let remove_rule id pred prog =
try
(* create a fake rule with the relevant id since the set of
rules only look at the ids to compare elements *)
let fake_lhs = Predicate.{p_id=ASPred.fake_pred_id;arity= -1} in
let fake_rule = Rule.{id=id;lhs=fake_lhs;e_rhs=[];i_rhs=[];i_rhs_num=0;content=UF.create []} in
let new_rules_for_pred = Rule.Rules.remove fake_rule (Predicate.PredMap.find pred prog.rules) in
let new_rules = Predicate.PredMap.add pred new_rules_for_pred prog.rules in
if new_rules_for_pred = Rule.Rules.empty then
{prog with rules=new_rules;idb=List.filter (fun i -> not (i=pred)) prog.idb}
else
{prog with rules=new_rules}
with
| Not_found -> failwith "Bug: should not try to remove a rule with a lhs predicate that has no rule"
let get_fresh_rule_id ({rule_id_gen} as prog) =
let new_id,rule_id_gen=IdGenerator.IntIdGen.get_fresh_id rule_id_gen in
......
......@@ -77,7 +77,8 @@ sig
module Program :
sig
type program = {
rules : Rule.rule list Predicate.PredMap.t;
(* rules : Rule.rule list Predicate.PredMap.t; *)
rules : Rule.Rules.t Predicate.PredMap.t;
edb : ASPred.pred_id list;
edb_facts:Predicate.FactSet.t Predicate.PredMap.t;
idb : ASPred.pred_id list;
......@@ -117,7 +118,17 @@ sig
should be empty.*)
val add_rule : intensional:bool -> ASRule.rule -> program -> program
(** [remove_rule id p] returns the program [p] from which the rule
with id [id] has been removed.
IMPORTANT: This function only deals with rules introducing
intensional predicate, because it is used when a constant is
given several interpretations in a lexicon.
*)
val remove_rule : int -> ASPred.pred_id -> program -> program
val get_fresh_rule_id : program -> (int * program)
val get_fresh_cst_id : string -> program -> (Datalog_AbstractSyntax.ConstGen.id * program)
......
......@@ -111,6 +111,8 @@ struct
res
else
term_compare l1 l2
let fake_pred_id = -1
module PredIds=Utils.IntSet
......
......@@ -30,7 +30,8 @@ sig
val to_string : predicate -> PredIdTable.table -> ConstGen.Table.table -> string
val compare : predicate -> predicate -> int
val fake_pred_id : pred_id
end
......
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