eliminate_unknown_lsymbols.ml 2.35 KB
Newer Older
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69
open Term
open Decl
open Theory
open Task

let debug = Debug.register_info_flag "eliminate_unknown_lsymbols"
  ~desc:"Print@ debugging@ messages@ of@ the@ eliminate_unknown_types@ transformation."

let abstraction (keep : lsymbol -> bool) =
  let term_table = Hterm.create 257 in
  let extra_decls = ref [] in

  let rec abstract t : term =
    match t.t_node with
    | Tvar _ | Tconst _ | Tapp(_,[]) | Ttrue | Tfalse -> t
    | Tapp (ls,_) when keep ls ->
      t_map abstract t
    | Tlet _ | Tnot _ | Tbinop _ | Tif _ ->
      t_map abstract t
    | _ ->
      if Debug.test_flag debug then
        Format.printf "eliminate@ %a@." Pretty.print_term t;
      let (ls, tabs) = try Hterm.find term_table t with Not_found ->
        let ls = create_lsymbol (Ident.id_fresh "abstr") [] t.t_ty in
        let tabs = t_app ls [] t.t_ty in
        Hterm.add term_table t (ls, tabs);
        ls, tabs in
      extra_decls := ls :: !extra_decls;
      tabs
  in

  let abstract_decl (d : decl) : decl list =
    let d = decl_map abstract d in
    let l = List.fold_left
        (fun acc ls -> create_param_decl ls :: acc)
        [d] !extra_decls in
    extra_decls := [];
    l
  in

  Trans.decl abstract_decl None

let syntactic_transform transf =
  Trans.bind (Trans.fold (fun hd acc ->
  match hd.task_decl.td_node with
  | Decl { d_node = Dlogic ((ls,_def)::[]) } -> Sls.add ls acc
  | _ -> acc) Sls.empty)
  (fun decl ->
  Trans.on_meta Printer.meta_syntax_converter (fun metas_conv ->
  Trans.on_meta Printer.meta_syntax_logic (fun metas ->
    let symbols = List.fold_left (fun acc meta_arg ->
      match meta_arg with
      | [Theory.MAls ls; Theory.MAstr _; Theory.MAint _] -> Sls.add ls acc
      | _ -> assert false) decl metas_conv in
    let symbols = List.fold_left (fun acc meta_arg ->
      match meta_arg with
      | [Theory.MAls ls; Theory.MAstr _; Theory.MAint _] -> Sls.add ls acc
      | _ -> assert false) symbols metas in
    let keep ls =  Sls.exists (ls_equal ls) symbols in
    Trans.compose (transf keep)
      (Trans.decl (fun d -> match d.d_node with
           | Dparam l when not (keep l || l.ls_args = []) -> []
           | _ -> [d]) None))))

let () =
  Trans.register_transform "eliminate_unknown_lsymbols"
    (syntactic_transform abstraction)
    ~desc:"Abstract@ applications@ of@ non-built-in@ symbols@ with@ \
      constants.@ Used@ by@ the@ Gappa@ pretty-printer."