<commit_before>(**************************************************************************)
(*                                                                        *)
(*  Copyright (C) 2010-                                                   *)
(*    <NAME>                                                     *)
(*    <NAME>                                          *)
(*    <NAME>                                                      *)
(*    <NAME>                                                    *)
(*                                                                        *)
(*  This software is free software; you can redistribute it and/or        *)
(*  modify it under the terms of the GNU Library General Public           *)
(*  License version 2.1, with the special exception on linking            *)
(*  described in file LICENSE.                                            *)
(*                                                                        *)
(*  This software is distributed in the hope that it will be useful,      *)
(*  but WITHOUT ANY WARRANTY; without even the implied warranty of        *)
(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.                  *)
(*                                                                        *)
(**************************************************************************)

(** transformation from polymorphic logic to untyped logic. The polymorphic
logic must not have finite support types. *)


open Util
open Ident
open Ty
open Term
open Decl
open Task
open Libencoding

(** module with printing functions *)
module Debug = struct
  let print_mtv vprinter fmter m =
    Mtv.iter (fun key value -> Format.fprintf fmter "@[%a@] -> @[%a@]@."
      Pretty.print_tv key vprinter value) m

  (** utility to print a list of items *)
  let rec print_list printer fmter = function
    | [] -> Format.fprintf fmter ""
    | e::es -> if es = []
        then Format.fprintf fmter "@[%a@] %a" printer e (print_list printer) es
        else Format.fprintf fmter "@[%a@], %a" printer e
        (print_list printer) es

  let debug x = Format.eprintf "%s@." x
end

(** {2 module to separate utilities from important functions} *)

module Transform = struct

    (* really return the map that replace all the variable of ty1,
       If the same variable appear in ty1 and ty2 Ty.ty_match doesn't
       bind this variable
    *)
  let rec ty_match2 s ty1 ty2 =
    match ty1.ty_node, ty2.ty_node with
      | Tyvar n1, _ ->
        Mtv.change n1 (function
          | None -> Some ty2
          | Some ty1 as r when ty_equal ty1 ty2 -> r
          | _ -> assert false) s
      | Tyapp (f1, l1), Tyapp (f2, l2) when ts_equal f1 f2 ->
        List.fold_left2 ty_match2 s l1 l2
      | _ -> assert false


  let fs_type =
    let alpha = ty_var (create_tvsymbol (id_fresh "a")) in
    create_fsymbol (id_fresh "type_of") [alpha] ty_type

  let app_type t = t_app fs_type [t] ty_type

  (** creates a new logic symbol, with a different type if the
  given symbol was polymorphic *)
  let findL = Wls.memoize 63 (fun lsymbol ->
    if ls_equal lsymbol ps_equ || lsymbol.ls_value = None then lsymbol else
    let new_ty = ty_freevars Stv.empty (of_option lsymbol.ls_value) in
    (* as many t as type vars *)
    if Stv.is_empty new_ty then lsymbol (* same type *) else
      let add _ acc = ty_type :: acc in
      let args = Stv.fold add new_ty lsymbol.ls_args in
      (* creates a new lsymbol with the same name but a different type *)
      Term.create_lsymbol (id_clone lsymbol.ls_name) args lsymbol.ls_value)

  (** {1 transformations} *)

  (** translation of terms *)
  let rec term_transform kept varM t =
    match t.t_node with
    | Tapp(f, terms) ->
      let terms = args_transform kept varM (of_option f.ls_value)
        terms t.t_ty in
      t_app (findL f) terms t.t_ty
    | _ -> (* default case : traverse *)
      t_map (term_transform kept varM) (fmla_transform kept varM) t

  (** translation of formulae *)
  and fmla_transform kept varM f =
    match f.f_node with
      (* first case : predicate are not translated *)
    | Fapp(p,terms) ->
      let terms = List.map (term_transform kept varM) terms in
      f_app (findL p) terms
    | Fquant(q,b) ->
      let vsl,trl,fmla,cb = f_open_quant_cb b in
        (* TODO : how to modify the triggers? *)
      let guard fmla vs =
        if Sty.mem vs.vs_ty kept then fmla else
          let g = f_equ (app_type (t_var vs)) (term_of_ty varM vs.vs_ty) in
          f_implies g fmla in
      let fmla2 = List.fold_left guard (fmla_transform kept varM fmla) vsl in
      let trl = tr_map (term_transform kept varM)
        (fmla_transform kept varM) trl in
      f_quant q (cb vsl trl fmla2)
    | _ -> (* otherwise : just traverse and translate *)
      f_map (term_transform kept varM) (fmla_transform kept varM) f(*  in *)
    (* Format.eprintf "fmla_to : %a@." Pretty.print_fmla f;f *)

  and args_transform kept varM fs_value args ty =
    (* Debug.print_list Pretty.print_ty Format.std_formatter type_vars; *)
    let tv_to_ty = ty_match2 Mtv.empty fs_value ty in
    (* Debug.print_mtv Pretty.print_ty Format.err_formatter tv_to_ty; *)
    let args = List.map (term_transform kept varM) args in
    (* fresh args to be added at the beginning of the list of arguments *)
    let add _ ty acc = term_of_ty varM ty :: acc in
    Mtv.fold add tv_to_ty args

  let logic_guard kept acc lsymbol =
    match lsymbol.ls_value with
      | None -> acc
      | Some ty_val when Sty.mem ty_val kept -> acc
      | Some ty_val ->
        let varl = List.map (fun v -> create_vsymbol (id_fresh "x") v)
          lsymbol.ls_args in
        let stv = ls_ty_freevars lsymbol in
        let trans varM () =
          let terms = List.map t_var varl in
          let terms = args_transform kept varM ty_val terms ty_val in
          let fmla =
            f_equ (app_type (t_app (findL lsymbol) terms ty_val))
              (term_of_ty varM ty_val) in<commit_msg>encoding guard : use explicit type argument only for types which appear only in the type value<commit_after>(**************************************************************************)
(*                                                                        *)
(*  Copyright (C) 2010-                                                   *)
(*    <NAME>                                                     *)
(*    <NAME>                                          *)
(*    <NAME>                                                      *)
(*    <NAME>                                                    *)
(*                                                                        *)
(*  This software is free software; you can redistribute it and/or        *)
(*  modify it under the terms of the GNU Library General Public           *)
(*  License version 2.1, with the special exception on linking            *)
(*  described in file LICENSE.                                            *)
(*                                                                        *)
(*  This software is distributed in the hope that it will be useful,      *)
(*  but WITHOUT ANY WARRANTY; without even the implied warranty of        *)
(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.                  *)
(*                                                                        *)
(**************************************************************************)

(** transformation from polymorphic logic to untyped logic. The polymorphic
logic must not have finite support types. *)


open Util
open Ident
open Ty
open Term
open Decl
open Task
open Libencoding

(** module with printing functions *)
module Debug = struct
  let print_mtv vprinter fmter m =
    Mtv.iter (fun key value -> Format.fprintf fmter "@[%a@] -> @[%a@]@."
      Pretty.print_tv key vprinter value) m

  (** utility to print a list of items *)
  let rec print_list printer fmter = function
    | [] -> Format.fprintf fmter ""
    | e::es -> if es = []
        then Format.fprintf fmter "@[%a@] %a" printer e (print_list printer) es
        else Format.fprintf fmter "@[%a@], %a" printer e
        (print_list printer) es

  let debug x = Format.eprintf "%s@." x
end

(** {2 module to separate utilities from important functions} *)

module Transform = struct

    (* really return the map that replace all the variable of ty1,
       If the same variable appear in ty1 and ty2 Ty.ty_match doesn't
       bind this variable
    *)
  let rec ty_match2 s ty1 ty2 =
    match ty1.ty_node, ty2.ty_node with
      | Tyvar n1, _ ->
        Mtv.change n1 (function
          | None -> Some ty2
          | Some ty1 as r when ty_equal ty1 ty2 -> r
          | _ -> assert false) s
      | Tyapp (f1, l1), Tyapp (f2, l2) when ts_equal f1 f2 ->
        List.fold_left2 ty_match2 s l1 l2
      | _ -> assert false

  let fs_type =
    let alpha = ty_var (create_tvsymbol (id_fresh "a")) in
    create_fsymbol (id_fresh "type_of") [alpha] ty_type

  let app_type t = t_app fs_type [t] ty_type

  let type_variable_only_in_value lsymbol =
    let tvar_val = ty_freevars Stv.empty (of_option lsymbol.ls_value) in
    let tvar_arg = List.fold_left ty_freevars Stv.empty lsymbol.ls_args in
    Stv.diff tvar_val tvar_arg

  (** creates a new logic symbol, with a different type if the
  given symbol was polymorphic *)
  let findL = Wls.memoize 63 (fun lsymbol ->
    if ls_equal lsymbol ps_equ || lsymbol.ls_value = None then lsymbol else
    let new_ty = type_variable_only_in_value lsymbol in
    (* as many t as type vars *)
    if Stv.is_empty new_ty then lsymbol (* same type *) else
      let add _ acc = ty_type :: acc in
      let args = Stv.fold add new_ty lsymbol.ls_args in
      (* creates a new lsymbol with the same name but a different type *)
      Term.create_lsymbol (id_clone lsymbol.ls_name) args lsymbol.ls_value)

  (** {1 transformations} *)

  (** translation of terms *)
  let rec term_transform kept varM t =
    match t.t_node with
    | Tapp(f, terms) ->
      let terms = args_transform kept varM f terms t.t_ty in
      t_app (findL f) terms t.t_ty
    | _ -> (* default case : traverse *)
      t_map (term_transform kept varM) (fmla_transform kept varM) t

  (** translation of formulae *)
  and fmla_transform kept varM f =
    match f.f_node with
      (* first case : predicate are not translated *)
    | Fapp(p,terms) ->
      let terms = List.map (term_transform kept varM) terms in
      f_app (findL p) terms
    | Fquant(q,b) ->
      let vsl,trl,fmla,cb = f_open_quant_cb b in
        (* TODO : how to modify the triggers? *)
      let guard fmla vs =
        if Sty.mem vs.vs_ty kept then fmla else
          let g = f_equ (app_type (t_var vs)) (term_of_ty varM vs.vs_ty) in
          f_implies g fmla in
      let fmla2 = List.fold_left guard (fmla_transform kept varM fmla) vsl in
      let trl = tr_map (term_transform kept varM)
        (fmla_transform kept varM) trl in
      f_quant q (cb vsl trl fmla2)
    | _ -> (* otherwise : just traverse and translate *)
      f_map (term_transform kept varM) (fmla_transform kept varM) f(*  in *)
    (* Format.eprintf "fmla_to : %a@." Pretty.print_fmla f;f *)

  and args_transform kept varM lsymbol args ty =
    (* Debug.print_list Pretty.print_ty Format.std_formatter type_vars; *)
    let tv_to_ty = ty_match2 Mtv.empty (of_option lsymbol.ls_value) ty in
    let new_ty = type_variable_only_in_value lsymbol in
    let tv_to_ty = Mtv.inter (fun _ tv () -> Some tv) tv_to_ty new_ty in
    (* Debug.print_mtv Pretty.print_ty Format.err_formatter tv_to_ty; *)
    let args = List.map (term_transform kept varM) args in
    (* fresh args to be added at the beginning of the list of arguments *)
    let add _ ty acc = term_of_ty varM ty :: acc in
    Mtv.fold add tv_to_ty args

  let logic_guard kept acc lsymbol =
    match lsymbol.ls_value with
      | None -> acc
      | Some ty_val when Sty.mem ty_val kept -> acc
      | Some ty_val ->
        let varl = List.map (fun v -> create_vsymbol (id_fresh "x") v)
          lsymbol.ls_args in
        let stv = ls_ty_freevars lsymbol in
        let trans varM () =
          let terms = List.map t_var varl in
          let terms = args_transform kept varM lsymbol terms ty_val in
          let fmla =
            f_equ (app_type (t_app (findL lsymbol) terms ty_val))
              (term_of_ty varM ty_val) in
{'fraction_non_alphanumeric': 0.10462955481942313, 'fraction_numerical': 0.005978831703967035, 'mean_word_length': 1.9569995222169134, 'pattern_counts': {'":': 0, '<': 11, '<?xml version=': 0, '>': 52, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 46, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '2991432', 'n_tokens_mistral': 3669, 'n_tokens_neox': 3542, 'n_words': 1313}