Source file rgg.ml

open DatalogLib
module ASProg = Datalog_AbstractSyntax.AbstractSyntax.Program
module ASPred = Datalog_AbstractSyntax.AbstractSyntax.Predicate
module ASRule = Datalog_AbstractSyntax.AbstractSyntax.Rule

module Log = UtilsLib.Xlog.Make (struct
  let name = "Rgg"
end)

type rule_node = {
  rule : ASRule.rule;
  adorned_head : Adornment.status list;
  position : int;
  bound_vars : ASPred.TermSet.t;
  free_vars : ASPred.TermSet.t;
}

type vertex =
  | Goal of (ASPred.predicate * Adornment.status list)
  | Rule of rule_node  (**A node is either a Goal or a Rule *)

module Rg_node = struct
  type t = vertex

  let equal = ( = )

  let compare_node node1 node2 =
    match (node1, node2) with
    | Goal _g, Rule _r -> 1
    | Rule _r, Goal _g -> -1
    | Goal (p1, bf), Goal (p2, bf2) ->
      (* The comparison should not rely on arguments because we want
         to identify nodes with the same predicate symbol and the same
         bound/free adornment *)
      let id_comparison = ASPred.compare ~with_arguments:false p1 p2 in
      if id_comparison = 0 then
        (* Arity is already taken into account in the predicate comparison. *)
        Adornment.compare bf bf2
      else id_comparison
    | Rule r1, Rule r2 ->
      let rule_id_comp = ASRule.(r1.rule.id - r2.rule.id) in
      if rule_id_comp = 0 then
        let pos_comparison = r1.position - r2.position in
        if pos_comparison = 0 then
          Adornment.compare r1.adorned_head r2.adorned_head
        else pos_comparison
      else rule_id_comp
        
  let compare = compare_node
  let hash = Hashtbl.hash
end

module Rg_graph = Graph.Persistent.Digraph.ConcreteBidirectional (Rg_node)

let pp_node program fmt node =
  match node with
  | Goal (p, bfs) ->
      let predicate_name =
        ASPred.PredIdTable.find_sym_from_id p.ASPred.p_id
          program.ASProg.pred_table
      in
      Format.fprintf fmt "%s_%s" predicate_name (Adornment.to_string bfs)
  | Rule r ->
      let bfs = Adornment.to_string r.adorned_head in
      Format.fprintf fmt "Rule %d a position %d_%s" r.rule.ASRule.id r.position bfs
 


let node_to_dot node program =
  match node with
  | Goal (p, bfs) ->
      let predicate_name =
        ASPred.PredIdTable.find_sym_from_id p.ASPred.p_id
          program.ASProg.pred_table
      in
      let pred_without_slash =
        String.map
          (fun x -> if x = '/' || x = ',' || x = '(' || x = ')' then '_' else x)
          predicate_name
      in
      Printf.sprintf "\t%s_%s" pred_without_slash
        (Adornment.to_string bfs)
  | Rule r ->
      let bfs = Adornment.to_string r.adorned_head in
      Printf.sprintf "\tr%dp%d_%s" r.rule.ASRule.id r.position bfs

let edge_to_dot node1 node2 program =
  Printf.sprintf "%s -> %s"
    (node_to_dot node1 program)
    (node_to_dot node2 program)

let graph_to_dot rgg program filename =
  let oc = open_out filename in
  Printf.fprintf oc "digraph G {\n";
  Rg_graph.iter_vertex
    (fun x -> Printf.fprintf oc "%s;\n" (node_to_dot x program))
    rgg;
  Rg_graph.iter_edges
    (fun x y -> Printf.fprintf oc "%s;\n" (edge_to_dot x y program))
    rgg;
  Printf.fprintf oc "}";
  close_out oc

let rec make_bound_set_aux acc = function
  | [], [] -> acc
  | _, []
  | [], _ -> failwith "Bug: computing bound set of non compatible contents"
  | _ :: tl1, (ASPred.Const _) :: tl2 -> make_bound_set_aux acc (tl1, tl2)
  | binding :: tl1, _ :: tl2 when Adornment.Free = binding -> make_bound_set_aux acc (tl1, tl2)
  | _ :: tl1, var :: tl2 -> make_bound_set_aux (ASPred.TermSet.add var acc) (tl1, tl2)


let make_bound_set adornment head =
  (*We build for example [(true,x);(false,y);(false,z)] and we
    extract the bound variables*)
  make_bound_set_aux ASPred.TermSet.empty (adornment, head.ASPred.arguments)
    
let make_free_set rule bound_set =
  ASPred.TermSet.diff bound_set (ASRule.get_variables_in_rule rule)

(** Construction of a rule node at the position 0 *)
let build_init_rule_node adornment rule =
  let bound_vars = make_bound_set adornment rule.ASRule.lhs in
  let new_rule =
    Rule
      {
        rule;
        adorned_head = adornment;
        position = 0;
        bound_vars;
        free_vars = make_free_set rule bound_vars;
      }
  in
  new_rule

let build_succ_rule_node rule_node new_context =
  match rule_node with
  | Rule node ->
      let new_rule =
        Rule
          {
            rule = node.rule;
            adorned_head = node.adorned_head;
            position = node.position + 1;
            bound_vars = new_context;
            free_vars = make_free_set node.rule new_context;
          }
      in
      new_rule
  | _ -> rule_node

let new_nodes prog rgg_node =
  match rgg_node with
  (* Case where it's a predicate P with an adornment alpha *)
  | Goal (pred, bfs) ->
    if ASProg.is_in_idb pred prog then
      (*We search the rules which pred is the head of*)
      let matching_rules = ASProg.match_rules pred prog in
      (*We build the corresponding rule nodes at the position 0*)
      ASRule.Rules.fold
        (fun r acc ->
           let new_node =
             build_init_rule_node bfs r
           in
           (new_node :: acc))
        matching_rules
        []
        (* No new nodes when, it's an edb predicate*)
    else []
  (* Case where it's a rule *)
  | Rule r ->
    let rule = r.rule in
    let subgoal_number = rule.ASRule.rhs_num in
    (* Test : Rule with empty body like A(a,b,a,b).*)
    if subgoal_number = 0 then []
    else
      (*We retrieve the corresponding subgoal at the ith position*)
      let subgoal, _position = ASRule.get_subgoal rule r.position in
      let subgoal_adornment, new_context =
        Adornment.adornment ~bound_variables:r.bound_vars subgoal 
      in
      let goal_node =
        Goal
          ( subgoal,
            subgoal_adornment
             )
      in
      let result = [ goal_node ] in
      if r.position < subgoal_number - 1 then
        (*We can build a new rule node*)
        let succ_node = build_succ_rule_node rgg_node new_context in
        succ_node :: result
      else result
        
let rec build_graph prog graph rgg_node =
  (* From a node we build the immediate children *)
  let () =
    Log.debug (fun m -> m "Dealing with node %a" (pp_node prog) rgg_node)
  in
  let children =
    new_nodes prog rgg_node
  in
  List.fold_left
    (fun acc child ->
       if not (Rg_graph.mem_vertex acc child) then
         let acc' = Rg_graph.add_edge acc rgg_node child in
         build_graph prog acc' child
       else Rg_graph.add_edge acc rgg_node child)
    graph
    children
    
let build_rgg program query =
  let empty_rgg = Rg_graph.empty in
  let unit_rgg = Rg_graph.add_vertex empty_rgg (Goal query) in
  let result = build_graph program unit_rgg (Goal query) in
  result