encoding_explicit.ml 6.88 KB
Newer Older
1 2
(**************************************************************************)
(*                                                                        *)
MARCHE Claude's avatar
MARCHE Claude committed
3
(*  Copyright (C) 2010-2012                                               *)
4 5 6
(*    François Bobot                                                      *)
(*    Jean-Christophe Filliâtre                                           *)
(*    Claude Marché                                                       *)
MARCHE Claude's avatar
MARCHE Claude committed
7
(*    Guillaume Melquiond                                                 *)
8 9 10 11 12 13 14 15 16 17 18 19 20
(*    Andrei Paskevich                                                    *)
(*                                                                        *)
(*  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.                  *)
(*                                                                        *)
(**************************************************************************)

Francois Bobot's avatar
Francois Bobot committed
21
(** transformation from polymorphic logic to untyped logic. The polymorphic
22 23 24
logic must not have finite support types. *)


25 26 27 28 29 30
open Util
open Ident
open Ty
open Term
open Decl
open Task
31
open Libencoding
32

33 34 35 36 37
(** 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
Simon Cruanes's avatar
Simon Cruanes committed
38

39 40 41
  (** utility to print a list of items *)
  let rec print_list printer fmter = function
    | [] -> Format.fprintf fmter ""
42 43 44 45 46
    | 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
47 48 49

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

Simon Cruanes's avatar
Simon Cruanes committed
51 52
(** {2 module to separate utilities from important functions} *)

53 54
module Transform = struct

55 56
  (** creates a new logic symbol, with a different type if the
  given symbol was polymorphic *)
57
  let findL = Wls.memoize 63 (fun lsymbol ->
58
    if ls_equal lsymbol ps_equ then lsymbol else
59
    let new_ty = ls_ty_freevars lsymbol in
60
    (* as many t as type vars *)
61
    if Stv.is_empty new_ty then lsymbol (* same type *) else
62
      let add _ acc = ty_type :: acc in
63
      let args = Stv.fold add new_ty lsymbol.ls_args in
64
      (* creates a new lsymbol with the same name but a different type *)
65
      Term.create_lsymbol (id_clone lsymbol.ls_name) args lsymbol.ls_value)
66

67 68 69
  (** {1 transformations} *)

  (** translation of terms *)
70
  let rec term_transform varM t = match t.t_node with
71 72
      (* first case : predicate (not =), we must translate it and its args *)
    | Tapp(f, terms) when not (ls_equal f ps_equ) ->
73
      let terms = args_transform varM f terms t.t_ty in
74
      t_app (findL f) terms t.t_ty
75
    | _ -> (* default case : traverse *)
76
      t_map (term_transform varM) t
77

78
  and args_transform varM ls args ty =
79 80 81
    (* Debug.print_list Pretty.print_ty Format.std_formatter type_vars; *)
    let tv_to_ty = ls_app_inst ls args ty in
    (* Debug.print_mtv Pretty.print_ty Format.err_formatter tv_to_ty; *)
82
    let args = List.map (term_transform varM) args in
83
    (* fresh args to be added at the beginning of the list of arguments *)
84
    let add _ ty acc = term_of_ty varM ty :: acc in
85 86
    Mtv.fold add tv_to_ty args

87 88
  let param_transform ls = [Decl.create_param_decl (findL ls)]

89
  (** transforms a list of logic declarations into another.
90 91
  Declares new lsymbols with explicit polymorphic signatures. *)
  let logic_transform decls =
92
    (* if there is a definition, we must take it into account *)
93
    let helper (lsymbol, ldef) =
94
      let new_lsymbol = findL lsymbol in (* new lsymbol *)
95
      let vars,expr,close = open_ls_defn_cb ldef in
96
      let add v (vl,vm) =
97
        let vs = Term.create_vsymbol (id_fresh "t") ty_type in
98
        vs :: vl, Mtv.add v (t_var vs) vm
99 100
      in
      let vars,varM = Stv.fold add (ls_ty_freevars lsymbol) (vars,Mtv.empty) in
101 102
      let t = term_transform varM expr in
      close new_lsymbol vars t
103 104
    in
    [Decl.create_logic_decl (List.map helper decls)]
105

106
  (** transform an inductive declaration *)
107
  let ind_transform s idl =
108
    let iconv (pr,f) = pr, Libencoding.t_type_close term_transform f in
109
    let conv (ls,il) = findL ls, List.map iconv il in
110
    [Decl.create_ind_decl s (List.map conv idl)]
111 112

  (** transforms a proposition into another (mostly a substitution) *)
113
  let prop_transform (prop_kind, prop_name, f) =
114
    let quantified_fmla = Libencoding.t_type_close term_transform f in
115
    [Decl.create_prop_decl prop_kind prop_name quantified_fmla]
116

117
end
118

Simon Cruanes's avatar
Simon Cruanes committed
119 120
(** {2 main part} *)

121
let decl d = match d.d_node with
122 123 124 125 126 127
  | Dtype { ts_def = Some _ } -> []
  | Dtype ts -> [d; Libencoding.lsdecl_of_ts ts]
  | Ddata _ -> Printer.unsupportedDecl d
      "Algebraic and recursively-defined types are \
            not supported, run eliminate_algebraic"
  | Dparam ls -> Transform.param_transform ls
128
  | Dlogic ldl -> Transform.logic_transform ldl
129
  | Dind (s, idl) -> Transform.ind_transform s idl
130 131 132 133
  | Dprop prop -> Transform.prop_transform prop

let explicit = Trans.decl decl (Task.add_decl None d_ts_type)

134
let explicit =
135 136
  Trans.on_tagged_ty Libencoding.meta_kept (fun kept ->
  Trans.on_tagged_ts Eliminate_algebraic.meta_enum (fun enum ->
Andrei Paskevich's avatar
Andrei Paskevich committed
137
    let check ts = not (ts.ts_args = [] && Sty.mem (ty_app ts []) kept) in
138
    let enum = Sts.filter check enum in
139
    if Sts.is_empty enum then explicit
140
    else
141 142 143
      let ts = Sts.choose enum in
      let ty = ty_app ts (List.map ty_var ts.ts_args) in
      Printer.unsupportedType ty
Andrei Paskevich's avatar
Andrei Paskevich committed
144
      "Encoding_explicit is unsound in presence of unprotected finite types"))
145 146


147 148
(** {2 monomorphise task } *)

149
open Libencoding
150

151
let lsmap kept = Wls.memoize 63 (fun ls ->
152 153 154 155 156 157
  let prot_arg = is_protecting_id ls.ls_name in
  let prot_val = is_protected_id ls.ls_name in
  let neg ty = if prot_arg && Sty.mem ty kept then ty else ty_base in
  let pos ty = if prot_val && Sty.mem ty kept then ty else ty_base in
  let ty_arg = List.map neg ls.ls_args in
  let ty_res = Util.option_map pos ls.ls_value in
158 159 160 161
  if Util.option_eq ty_equal ty_res ls.ls_value &&
     List.for_all2 ty_equal ty_arg ls.ls_args then ls
  else create_lsymbol (id_clone ls.ls_name) ty_arg ty_res)

162
let d_ts_base = create_ty_decl ts_base
163

164
let monomorph = Trans.on_tagged_ty Libencoding.meta_kept (fun kept ->
François Bobot's avatar
François Bobot committed
165
  let kept = Sty.add ty_type kept in
166
  let decl = d_monomorph kept (lsmap kept) in
167 168
  Trans.decl decl (Task.add_decl None d_ts_base))

169
let () = Hashtbl.replace Encoding.ft_enco_poly "explicit"
170
    (fun _ -> Trans.compose explicit monomorph)