Source file reduction.ml

open Logic.Lambda
open UtilsLib.Utils
open DatalogLib.Datalog_AbstractSyntax
open DatalogLib.Datalog

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

module Make (Sg : module type of Signature.Data_Signature) = struct
  let rec sequentialize_rev stype sequence =
    match stype with
    | Lambda.Atom i -> i :: sequence
    | Lambda.DAtom _ -> failwith "Bug: type definition should be unfolded"
    | Lambda.LFun (alpha, beta) | Lambda.Fun (alpha, beta) ->
        sequentialize_rev beta (sequentialize_rev alpha sequence)
    | _ -> failwith "Bug: Not a 2nd order type"

  let sequentialize stype = List.rev (sequentialize_rev stype [])

  (** [map_types abs_type obj_type sg] returns a list of triple
      [(id_n,name_n,image_n);...;(id_2,name_2,image_2);(id_1,name_1,image_1)]
      where [abst_type=Atom(id_1) -> Atom(id_2) -> ... Atom(id_n)] and
      is defined as [name_1 -> name_2 -> ... -> name_n] and
      [obj_type=image_1 -> image_2 -> ... -> image_n]. Note that the
      list is in the {em reverse order} and that [abs_type] should be
      2nd order. *)

  let map_types abs_type obj_type sg =
    let log_type ?raw_type_info msg pp_type t =
      let raw_type =
        match raw_type_info with
        | None -> ""
        | Some (f, t) -> Printf.sprintf " (%s)" (f t)
      in
      Log.debug (fun m -> m "%s%a%s" msg pp_type t raw_type)
    in
    let rec map_types_aux abs_type obj_type lst =
      log_type "Mapping (aux) type:" (Sg.pp_type sg) abs_type;
      log_type "On (aux):          "
        (fun fmt ty -> Format.fprintf fmt "%s" (Lambda.raw_type_to_string ty))
        obj_type;
      match (abs_type, obj_type) with
      | Lambda.Atom i, _ -> (i, snd (Sg.id_to_string sg i), obj_type) :: lst
      | Lambda.DAtom _, _ ->
          failwith
            (Format.asprintf
               "Bug: type definition in \"%a\" as \"%s\" should be unfolded"
               (Sg.pp_type sg) abs_type
               (Lambda.raw_type_to_string abs_type))
      | Lambda.LFun (Lambda.Atom i, beta), Lambda.Fun (alpha', beta')
      | Lambda.Fun (Lambda.Atom i, beta), Lambda.Fun (alpha', beta') ->
          map_types_aux beta beta'
            ((i, snd (Sg.id_to_string sg i), alpha') :: lst)
      | Lambda.LFun _, Lambda.Fun _ | Lambda.Fun _, Lambda.Fun _ ->
          failwith "Bug: should be 2nd order type for abstract constant"
      | _, _ ->
          failwith
            "Bug: Not a 2nd order type or not corresponding abstract and \
             object type"
    in
    log_type
      ~raw_type_info:(Lambda.raw_type_to_string, abs_type)
      "Mapping type:" (Sg.pp_type sg) abs_type;
    log_type "On:          "
      (fun fmt ty -> Format.fprintf fmt "%s" (Lambda.raw_type_to_string ty))
      obj_type;
    map_types_aux abs_type obj_type []

  let log_pred name o_type atom_seq =
    Log.debug (fun m ->
        m "Build predicate from %s: %s   ([%s])" name
          (Lambda.raw_type_to_string o_type)
          (string_of_list ";" string_of_int atom_seq))

  (** [build_predicate_w_var_args (name,obj_type)
      (prog,var_gen,type_to_var_map)] returns [(prog',var_gen',type_to_var_map')] where:
      
      - [name] is the name of an abstract type of some ACG that
      has to be turned into a predicate of the associated datalog
      program
      
      - [ob_type] is the principal type of its realisation by this ACG
      
      - [prog] is the current associated datalog program
      
      - [var_gen] is a variable generator that records the variable
      associated with this predicate (according to the principal type
      [obj_type] of its image). It can be updated to [var_gen'] if
      some new variables are needed
      
      - [type_to_var_map] records to which variable each atomic type
      of the principal type is associated with. It can be updated to
      [type_to_var_map'] if some new variables were needed.
      
      - [prog'] is [prog] where the new predicate has been added
  *)
  let build_predicate_w_var_args (name, obj_type)
      (prog, var_gen, type_to_var_map) =
    let atom_sequence = sequentialize_rev obj_type [] in
    log_pred name obj_type atom_sequence;
    let var_sequence, var_gen, type_to_var_map =
      List.fold_left
        (fun (l_var_seq, l_var_gen, l_type_to_var_map) i ->
          let var, l_var_gen, l_type_to_var_map =
            try (IntMap.find i l_type_to_var_map, l_var_gen, l_type_to_var_map)
            with Not_found ->
              let var, l_var_gen = VarGen.get_fresh_id l_var_gen in
              (var, l_var_gen, IntMap.add i var l_type_to_var_map)
          in
          ( AbstractSyntax.Predicate.Var var :: l_var_seq,
            l_var_gen,
            l_type_to_var_map ))
        ([], var_gen, type_to_var_map)
        atom_sequence
    in
    let () =
      Log.debug (fun m ->
          match
            AbstractSyntax.Predicate.PredIdTable.find_id_of_sym_opt name
              prog.Datalog.Program.pred_table
          with
          | None ->
              m "The predicate '%s' was not already present in the program" name
          | Some _ ->
              m "The predicate '%s' was indeed already present in the program"
                name)
    in
    (* Except for variables and constants, the program [prog] is unchanged *)
    let p_id, prog = Datalog.Program.add_pred_sym name prog in
    ( AbstractSyntax.Predicate.
        { p_id; arity = List.length var_sequence; arguments = var_sequence },
      (prog, var_gen, type_to_var_map) )

  (** [build_predicate_w_cst_args (name,obj_type) prog] returns a pair
     [pred,prog'] where [pred] is a fully instantiated predicate
     where:

      - [name] is the name of an abstract type of some ACG that has to
     be turned into a the querying predicate for the associated
     datalog program

      - [ob_type] is the principal type of its realisation by this ACG
     that is interpreted as Datalog constants

      - [prog] is the current associated datalog program.

      [prog'] differs from [prog] only by keeping track of the
     constants added (and possibly the predicate, although it should
     already be present *)

  let build_predicate_w_cst_args ?(check_no_new_pred = true) (name, obj_type)
      prog =
    let atom_sequence = sequentialize obj_type in
    log_pred name obj_type atom_sequence;
    let const_sequence, prog =
      List.fold_left
        (fun (l_const_seq, l_prog) i ->
          let const_id, l_prog =
            (* l_prog output differs from l_prog input only by the
               association between (string_of_int i) and const_id *)
            Datalog.Program.get_fresh_cst_id (string_of_int i) l_prog
          in
          (AbstractSyntax.Predicate.Const const_id :: l_const_seq, l_prog))
        ([], prog) atom_sequence
    in
    let () =
      if check_no_new_pred then
        Log.debug (fun m ->
            let () =
              assert (
                match
                  AbstractSyntax.Predicate.PredIdTable.find_id_of_sym_opt name
                    prog.Datalog.Program.pred_table
                with
                | None -> false
                | Some _ -> true)
            in
            m "The predicate '%s' was indeed already present in the program"
              name)
        (* Except for variables and constants, the program [prog] is unchanged *)
        (* prog as input differs from prog as output only with the
           association between [name] and [p_id].*)
      else ()
    in
    let p_id, prog = Datalog.Program.add_pred_sym name prog in
    ( AbstractSyntax.Predicate.
        {
          p_id;
          arity = List.length const_sequence;
          arguments = List.rev const_sequence;
        },
      prog )

  let get_constant_id = function
    | Lambda.Const i -> i
    | _ ->
        failwith "Bug: Predicates should be build only for declared constants"

  (** [generate_and_add_rule ~abs_cst ~obj_princ_type ~obj_typing_env
      prog abs_sig obj_sig] returns a pair [(r,prog')] where:
      - [r] is the generated rule
      - [prog'] is [prog] where the rule [r] has been added
      - [abs_cst] is the abstract constant from the abstract signature
      [abs_sig] that triggers the rule generation
      - [obj_princ_type] is the principal type of the image by the
      lexicon of [abs_cst]
      - [obj_typing_env] is its typing environment. The latter maps
      the position of the object constants in the realisation of
      [abs_cst] to a pair [(t,ty)] where [t] is the object constant
      itself, and [ty] the type associated by the principal typing
      environment.
      - [prog] is the current datalog program
      - [abs_sig] and [obj_sig] are the abstract signature and the
      object signature of some ACG. *)

  let generate_and_add_rule ~abs_cst:(_, abs_t_type)
      ~obj_princ_type:principle_type ~obj_typing_env:env ~abs_sig ~obj_sig
      ~update_fct ~syms prog =
    let rule_id, prog = Datalog.Program.get_fresh_rule_id prog in
    let type_lst = map_types abs_t_type principle_type abs_sig in
    match type_lst with
    | [] -> failwith "Bug: there should be a type correspondance"
    | (_, name, image) :: tl ->
        let lhs, (prog, var_gen, type_to_var_map) =
          build_predicate_w_var_args (name, image)
            (prog, VarGen.init (), IntMap.empty)
        in
        (* intensional predicates come before extensional ones*)
        let e_rhs, e_rhs_length, (prog, var_gen, type_to_var_map), new_syms =
          IntMap.fold
            (fun _ (cst, cst_type) (rhs, l_length, l_tables, l_syms) ->
              let () =
                assert (
                  let e_pred_name_candidate =
                    Format.asprintf "%a" (Sg.pp_term obj_sig) cst
                  in
                  match Sg.is_constant e_pred_name_candidate obj_sig with
                  | true, Some (_, false, _) -> true
                  | _ -> false)
              in
              let const_name, l_syms' = update_fct cst l_syms in
              let new_pred, new_tables =
                build_predicate_w_var_args (const_name, cst_type) l_tables
              in
              let l_length = l_length + 1 in
              ((new_pred, l_length) :: rhs, l_length, new_tables, l_syms'))
            env
            ([], 0, (prog, var_gen, type_to_var_map), syms)
        in
        let i_rhs, length, (prog, _, _) =
          List.fold_left
            (fun (rhs, l_length, l_tables) (_, l_name, l_image) ->
              let new_pred, new_tables =
                build_predicate_w_var_args (l_name, l_image) l_tables
              in
              let l_length = l_length + 1 in
              ((new_pred, l_length) :: rhs, l_length, new_tables))
            ([], e_rhs_length, (prog, var_gen, type_to_var_map))
            tl
        in
        let new_rule =
          AbstractSyntax.Rule.
            {
              id = rule_id;
              lhs;
              e_rhs;
              i_rhs;
              i_rhs_num = length - e_rhs_length;
              rhs_num = length;
            }
        in
        let () =
          Log.debug (fun m ->
              m "The following rule was generated: %a"
                (AbstractSyntax.Rule.pp ~with_position:true
                   prog.Datalog.Program.pred_table
                   prog.Datalog.Program.const_table)
                new_rule)
        in
        ( new_rule,
          Datalog.Program.add_rule ~intensional:true new_rule prog,
          new_syms )

  (** [edb_and_query ~obj_term ~obj_type ~obj_typing_env ~dist_type
      prog ~abs_sig ~obj_sig] returns a pair [(q,prog')] where:
      - [q] is the predicate corresponding to the query generated by
      the object term [obj_term] to parse
      - [prog'] is [prog] where the extensional database resulting
      from the reduction of the object term [obj_term]
      - [obj_type] is the principal type of [obj_term]
      - [obj_typing_env] is its typing environment. The latter maps
      the position of the object constants in the realisation of
      [abs_cst] to a pair [(t,ty)] where [t] is the object constant
      itself, and [ty] the type associated by the principal typing
      environment.
      - [dist_type] is the distinguished type of the ACG
      - [prog] is the current datalog program
      - [abs_sig] and [obj_sig] are the abstract signature and the
      object signature of some ACG. *)
  let edb_and_query ~obj_term ~obj_type ~obj_typing_env ~dist_type ?adornment
      prog ~abs_sig ~obj_sig ~syms:(syms, _) =
    (* It makes the assumption that no constant has been
       previously defined or used in the program *)
    let type_lst = map_types dist_type obj_type abs_sig in
    match type_lst with
    | [] -> failwith "Bug: there should be a type correspondance"
    | [ (_, name, image) ] ->
        let e_facts, prog =
          IntMap.fold
            (fun _ (cst, cst_type) (l_facts, l_prog) ->
              let cst_id = get_constant_id cst in
              let () =
                assert (
                  let const_name =
                    Format.asprintf "%a" (Sg.pp_term obj_sig) cst
                  in
                  match Sg.is_constant const_name obj_sig with
                  | true, Some (_, false, _) -> true
                  | _ -> false)
              in
              let const_name =
                match UtilsLib.Utils.IntMap.find_opt cst_id syms with
                | None -> Format.asprintf "%a" (Sg.pp_term obj_sig) cst
                | Some name -> name
              in
              let new_pred, l_prog =
                build_predicate_w_cst_args (const_name, cst_type) l_prog
              in
              let rule_id, l_prog = Datalog.Program.get_fresh_rule_id l_prog in
              let new_fact =
                AbstractSyntax.Rule.
                  {
                    id = rule_id;
                    lhs = new_pred;
                    e_rhs = [];
                    i_rhs = [];
                    i_rhs_num = 0;
                    rhs_num = 0;
                  }
              in
              (new_fact :: l_facts, l_prog))
            obj_typing_env ([], prog)
        in
        let () = Log.debug (fun m -> m "Done (query in reduction)") in
        let prog =
          Datalog.Program.add_e_facts prog
            ( e_facts,
              prog.Datalog.Program.const_table,
              prog.Datalog.Program.rule_id_gen )
        in
        (* if there is an adornment, adds it to the name *)
        let name =
          match adornment with
          | None -> name
          | Some ad ->
              Printf.sprintf "%s_%s" name
                (MagicRewriting.Adornment.to_string ad)
        in
        build_predicate_w_cst_args (name, image) prog
    | (_, _, _) :: tl ->
        failwith "Bug: querying non atomic types is not yet implemented"
    [@@warning "-27"]

  let only_edb_and_query ~obj_term ~obj_type ~obj_typing_env ~dist_type prog
      ~abs_sig ~obj_sig ~syms:(syms, _) =
    (* It makes the assumption that no constant has been previously
       defined or used in the program *)
    let type_lst = map_types dist_type obj_type abs_sig in
    match type_lst with
    | [] -> failwith "Bug: there should be a type correspondance"
    | [ (_, name, image) ] ->
        let e_facts, prog =
          IntMap.fold
            (fun _ (cst, cst_type) (l_facts, l_prog) ->
              let cst_id = get_constant_id cst in
              let () =
                assert (
                  let const_name =
                    Format.asprintf "%a" (Sg.pp_term obj_sig) cst
                  in
                  match Sg.is_constant const_name obj_sig with
                  | true, Some (_, false, _) -> true
                  | _ -> false)
              in
              let const_name =
                match UtilsLib.Utils.IntMap.find_opt cst_id syms with
                | None -> Format.asprintf "%a" (Sg.pp_term obj_sig) cst
                | Some name -> name
              in
              let new_pred, l_prog =
                build_predicate_w_cst_args (const_name, cst_type) l_prog
              in
              (* only constants are added to the program. No rule *)
              (new_pred :: l_facts, l_prog))
            obj_typing_env ([], prog)
        in
        let () = Log.debug (fun m -> m "Done (query in reduction)") in
        (* [new_ prog] only differs from [prog] by vars/constants. No new rule is added *)
        let query, new_prog = build_predicate_w_cst_args (name, image) prog in
        (query, e_facts, new_prog)
    | (_, _, _) :: tl ->
        failwith "Bug: querying non atomic types is not yet implemented"
    [@@warning "-27"]
end