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_unsafe 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_unsafe 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 =
            match IntMap.find_opt i l_type_to_var_map with
            | Some v -> (v, l_var_gen, l_type_to_var_map)
            | None -> 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 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 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:(name, dist_type)
      ~interpretation:(o_term, o_type)
      prog
      abs_sig
      obj_sig] returns a pair [(r,prog')] where:
      {ul
      {- [r] is the generated rule}
      {- [prog'] is [prog] where the rule [r] has been added}
      {- [name] is the abstract constant name from the abstract
      signature [abs_sig] that triggers the rule generation, and
      [dist_type] is its type}
      {- [o_term] is the interpretation of [name] according to some
      lexicon}
      {- [o_type] is its type (and should be the image by the same
      lexicon of [abs_cst]}
      {- [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:(name, abs_t_type) ~interpretation:(o_term, o_type)
        ~abs_sig ~obj_sig
        ~update_fct ~syms prog =
    let eta_long_term =
      Signature.Data_Signature.eta_long_form o_term o_type obj_sig in
    let obj_princ_type, obj_typing_env =
      Logic.TypeInference.Type.inference eta_long_term
    in
    Log.info (fun m ->
        m "Interpreting \"%s\" as \"%a=%s\" with principle type: \"%s\"" name
          (Signature.Data_Signature.pp_term obj_sig)
          eta_long_term
          (Lambda.raw_to_caml eta_long_term)
          (Lambda.raw_type_to_string obj_princ_type));
    Log.info (fun m ->
        let pp_typing_env fmt env =
          IntMap.iter
            (fun k (t, ty) ->
              Format.fprintf fmt "@[%d --> %s : %s@]" k (Lambda.raw_to_string t)
                (Lambda.raw_type_to_string ty))
            env
        in
        m "In the context of:@,@[<v>  @[%a@]@]" pp_typing_env obj_typing_env);
    let rule_id, prog = Datalog.Program.get_fresh_rule_id prog in
    let type_lst = map_types abs_t_type obj_princ_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 = Sg.cst_to_string obj_sig cst
                  in
                  match Option.map (fun s -> Sg.is_constant s obj_sig) e_pred_name_candidate with
                  | Some (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'))
            obj_typing_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 ~dist_type
      prog ~abs_sig ~obj_sig] returns a pair [(q,prog')] where:
      {ul
      {- [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] has been added}
      {- [obj_type] is the type of [obj_term] (only used for debugging
      information)}
      {- [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 ~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 obj_princ_type, obj_typing_env =
      Logic.TypeInference.Type.inference obj_term in
    Log.debug (fun m ->
        m "Going to set a query for the distinguised type \"%a(%s)\""
          (Signature.Data_Signature.pp_type abs_sig)
          dist_type
          (Lambda.raw_type_to_string dist_type));
    Log.debug (fun m ->
        m "whose image is \"%a(%s)\""
          (Signature.Data_Signature.pp_type obj_sig)
          obj_type
          (Lambda.raw_type_to_string obj_type));
    Log.debug (fun m ->
        m "resulting int the principle type \"%s\""
          (Lambda.raw_type_to_string obj_princ_type));
    let type_lst = map_types dist_type obj_princ_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 = Sg.id_to_string_unsafe obj_sig cst_id
                  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 -> snd (Sg.id_to_string_unsafe obj_sig cst_id)
                | 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"

  let[@warning "-unused-value-declaration"] only_edb_and_query
       ~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 = Sg.id_to_string_unsafe obj_sig cst_id
                  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 -> snd (Sg.id_to_string_unsafe obj_sig cst_id)
                | 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"
end