explicit_polymorphism.ml 14.6 KB
Newer Older
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19
(**************************************************************************)
(*                                                                        *)
(*  Copyright (C) 2010-                                                   *)
(*    Francois Bobot                                                      *)
(*    Jean-Christophe Filliatre                                           *)
(*    Johannes Kanig                                                      *)
(*    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.                  *)
(*                                                                        *)
(**************************************************************************)

20
(**s transformation from polymorphic logic to untyped logic. The polymorphic
21 22 23
logic must not have finite support types. *)


24 25 26 27 28 29 30
open Util
open Ident
open Ty
open Term
open Decl
open Task

31

32 33 34 35 36
(** 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
37

38
  let print_mty vprinter fmter m =
39 40
    Mty.iter (fun key value -> Format.fprintf fmter "@[%a@] -> @[%a@]@."
      Pretty.print_ty key vprinter value) m
41

42 43 44 45 46 47 48 49 50
  (** 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
51

52 53 54



55 56 57 58 59 60 61
(** {2 small functions} *)

module Utils = struct

  (** parenthesing operator *)
  let ($) f x = f x

62 63 64 65 66 67
  let const x _ = x

  let map_keys m = Mty.fold (fun key _ acc -> key::acc) m []
  let map_values m = Mty.fold (fun _ value acc -> value::acc) m []


68
  (** type representing types *)
69
  let t = Ty.create_tysymbol (id_fresh "ty") [] None
70
  let my_t = ty_app t []
71 72
  let t_decl = Decl.create_ty_decl [(t, Tabstract)]

73
  let has_type_t = ty_equal my_t
74 75 76

  let is_tyvar = function
    | Tyvar _ -> true | _ -> false
77
  let from_tyvar = function
78
    | Tyvar x -> x | _ -> failwith "from_tyvar called on non-tyvar"
79 80
  let isSome = function
    | Some _ -> true | _ -> false
81 82 83
  let fromSome = function
    | Some x -> x | None -> failwith "fromSome called on None"

84 85 86 87 88 89 90 91 92 93
  (** list from 1 to n *)
  let range n =
    let rec helper acc = function
      | 0 -> acc
      | n -> helper (n :: acc) (n-1)
    in helper [] n

  (** [drop n l] is [l], without its [n] first elements *)
  let rec drop n l = match (n,l) with
    | (0, _) -> l
94 95
    | (_, []) -> failwith "dropping items from empty list"
    | (_, _::xs) -> drop (n-1) xs
96 97 98 99 100 101 102 103 104 105 106 107 108 109 110

  (** explore a type to seek all type vars *)
  let rec find_tyvars tyvars ty = match ty.ty_node with
    | Tyvar _ -> (* test if ty has already been found *)
      (try ignore $ List.find
        (fun x -> x.ty_tag = ty.ty_tag) tyvars; tyvars
      with Not_found -> ty::tyvars)
    | Tyapp (_, tys) -> List.fold_left find_tyvars tyvars tys
  (** predicate to check whether a type has type vars *)
  and has_tyvars ty = match ty.ty_node with
    | Tyvar _ -> true
    | Tyapp (_, tys) -> List.exists has_tyvars tys

  (** returns all type vars (free) in given fmla [f] *)
  let rec f_find_type_vars acc f = match f.f_node with
111
    | Fapp (p, terms) ->
112
      let new_acc = if isSome p.ls_value
113 114
        then find_tyvars acc (fromSome p.ls_value) else acc in
      List.fold_left t_find_type_vars new_acc terms
115 116
    | _ -> f_fold t_find_type_vars f_find_type_vars acc f
  (** returns all type vars in given term *)
117 118 119
  and t_find_type_vars acc t =
    let acc = find_tyvars acc t.t_ty in
    match t.t_node with
120 121 122 123 124 125 126 127
    | Tvar x -> find_tyvars acc x.vs_ty
    | _ -> t_fold t_find_type_vars f_find_type_vars acc t
  (** returns all type vars in given lsymbol *)
  and l_find_type_vars l =
    let acc = match l.ls_value with
      | None -> []
      | Some ty -> find_tyvars [] ty in
    List.fold_left find_tyvars acc l.ls_args
128 129


130 131 132 133 134
  (** [find_matching_vars tv_to_ty left right] matches [left]
  against [right] to deduce a mapping from type vars in [left]
  to types in [right]. [tv_to_ty] is a mapping given in argument.
  It must be compliant with the unification between [left] and [right] *)
  let rec find_matching_vars tv_to_ty left right =
135
    (*Format.eprintf "matching @[%a@] with @[%a@]@."
136
      (Debug.print_list Pretty.print_ty) left
137
      (Debug.print_list Pretty.print_ty) right;*)
Simon Cruanes's avatar
Simon Cruanes committed
138
    assert (List.length left = List.length right);
139
    let tv_to_ty = List.fold_left2 ty_match tv_to_ty left right in
140 141
    (*Format.eprintf "gives @[%a@]@."
      (Debug.print_mtv Pretty.print_ty) tv_to_ty; flush stderr;*)
142 143
    tv_to_ty

144 145 146 147 148
  module Mint = Map.Make(
    struct
      type t = int
      let compare = Pervasives.compare
    end)
149 150 151 152 153 154 155 156

  (** [bind_nums_to_type_vars l] takes a lsymbol [l], and binds 1..n (where
  n is the number of type vars in [l]) to type vars of [l] *)
  let bind_nums_to_type_vars l =
    let type_vars = l_find_type_vars l in
    let n = List.length type_vars in
    List.fold_left2 (fun acc key value -> Mint.add key value acc)
      Mint.empty (range n) type_vars
157 158 159 160


end

161 162
let ts_ty = Utils.t

163
(* from now on, we shall use those functions without module qualification *)
164 165
open Utils

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

168 169 170
module Transform = struct

  (** {1 memoization facilities} *)
171

Simon Cruanes's avatar
Simon Cruanes committed
172
  (** [find construct tbl id] searches for the object associated with
173 174
  [id] in [tbl]. It creates it with [construct id] if it cannot find it. *)
  let find_generic construct tbl id =
175
    try Hashtbl.find tbl id
176
    with Not_found ->
177
      let new_image = construct id in
178
      Hashtbl.add tbl id new_image;
179
      new_image
Simon Cruanes's avatar
Simon Cruanes committed
180

181 182 183

  (** creates a new logic symbol, with a different type if the
  given symbol was polymorphic *)
184
  let logic_to_logic lsymbol =
185
    if ls_equal lsymbol ps_equ || ls_equal lsymbol ps_neq then lsymbol else
186 187 188
    let ty_vars = match lsymbol.ls_value with (* do not forget result type *)
      | Some t -> t::lsymbol.ls_args | None -> lsymbol.ls_args in
    let new_ty = (List.fold_left find_tyvars [] ty_vars) in
189 190
    (* as many t as type vars *)
    if new_ty = [] then lsymbol (* same type *) else
191
      let new_ty = List.map (const my_t) new_ty in
192
      let all_new_ty = new_ty @ lsymbol.ls_args in
193
      (* creates a new lsymbol with the same name but a different type *)
194
      let new_lsymbol =
195 196
        Term.create_lsymbol (id_clone lsymbol.ls_name)
          all_new_ty lsymbol.ls_value in
197
      new_lsymbol
198

199
  (** creates a lsymbol associated with the given tysymbol *)
200
  let type_to_logic ty =
Simon Cruanes's avatar
Simon Cruanes committed
201
    let name = id_clone ty.ts_name in
202 203
    let args = (List.map (const my_t) ty.ts_args) in
    Term.create_lsymbol name args (Some my_t)
204

205

206
  (** different finders for logic and type declarations *)
207

208 209
  let findL tbl x = find_generic logic_to_logic tbl x
  let findT tbl x = find_generic type_to_logic tbl x
210

211 212 213 214 215 216 217
  (** {1 transformations} *)

  (** transforms a type into another *)
  let rec ty_to_ty tv_to_ty ty = match ty.ty_node with
    | Tyvar x -> (try Mtv.find x tv_to_ty with Not_found -> ty)
    | Tyapp(typ, tys) -> ty_app typ (List.map (ty_to_ty tv_to_ty) tys)

218 219 220
  (** transforms a type into a term (new args of polymorphic symbols).
      [tblT] is a hashtable used to associate types and symbols
      [varM] is a Map used to associate some type vars and symbols *)
221 222
  let rec ty_to_term tblT varM tv_to_ty ty =
    match ty.ty_node with
223
    | Tyvar _ ->
224 225 226 227 228 229 230 231 232 233 234 235 236 237 238 239 240
      let new_ty = ty_to_ty tv_to_ty ty in
      begin match new_ty.ty_node with
        | Tyvar _ -> (* var -> var, stop there *)
          assert (Mty.mem new_ty varM);
          t_var (Mty.find new_ty varM)
        | Tyapp _ -> (* recur *)
          ty_to_term tblT varM tv_to_ty new_ty
      end
    | Tyapp(typ, tys) ->
      assert (Hashtbl.mem tblT typ); (* nonsense otherwise *)
      let lsymbol = Hashtbl.find tblT typ in
      let terms = List.map (ty_to_term tblT varM tv_to_ty) tys in
      t_app lsymbol terms my_t



  (** translation of terms *)
241
  let rec term_transform tblT tblL varM t = match t.t_node with
242
    | Tapp(f, terms) ->
243 244 245
      let new_f = findL tblL f in
      (* first, remember an order for type vars of new_f *)
      let type_vars = l_find_type_vars new_f in
246
      (* Debug.print_list Pretty.print_ty Format.std_formatter type_vars; *)
247 248 249 250
      let int_to_tyvars = bind_nums_to_type_vars new_f in
      (* match types *)
      let args_to_match = drop (List.length type_vars) new_f.ls_args in
      let concrete_ty = List.map (fun x-> x.t_ty) terms in
Simon Cruanes's avatar
Simon Cruanes committed
251 252
      let result_to_match = fromSome new_f.ls_value in
      let result_ty = t.t_ty in
253
      let tv_to_ty = find_matching_vars Mtv.empty
Simon Cruanes's avatar
Simon Cruanes committed
254
        (result_to_match :: args_to_match) (result_ty :: concrete_ty) in
255
      (* Debug.print_mtv Pretty.print_ty Format.err_formatter tv_to_ty; *)
256 257 258 259 260
      (* fresh terms to be added at the beginning of the list of arguments *)
      let new_ty_int = range (List.length type_vars) in
      let new_ty = List.map (fun x -> Mint.find x int_to_tyvars) new_ty_int in
      let new_terms = List.map (ty_to_term tblT varM tv_to_ty) new_ty in
      let transformed_terms = List.map
261
        (term_transform tblT tblL varM) terms in
262 263
      let transformed_result = ty_to_ty tv_to_ty (fromSome new_f.ls_value) in
      t_app new_f (new_terms @ transformed_terms) transformed_result
Simon Cruanes's avatar
Simon Cruanes committed
264
      | _ -> (* default case : traverse *)
265 266
        t_map (term_transform tblT tblL varM)
          (fmla_transform tblT tblL varM) t
267
  (** translation of formulae *)
268
  and fmla_transform tblT tblL varM f = match f.f_node with
269
      (* first case : predicate (not = or <>), we must translate it and its args *)
Simon Cruanes's avatar
Simon Cruanes committed
270 271 272 273 274 275 276 277 278
    | Fapp(p,terms) when (not (ls_equal p ps_equ)) && not(ls_equal p ps_neq) ->
      let new_p = findL tblL p in
      (* first, remember an order for type vars of new_f *)
      let type_vars = l_find_type_vars new_p in
      (* Debug.print_list Pretty.print_ty Format.std_formatter type_vars; *)
      let int_to_tyvars = bind_nums_to_type_vars new_p in
      (* match types *)
      let args_to_match = drop (List.length type_vars) new_p.ls_args in
      let concrete_ty = List.map (fun x-> x.t_ty) terms in
279
      let tv_to_ty = find_matching_vars Mtv.empty
Simon Cruanes's avatar
Simon Cruanes committed
280 281 282 283 284 285 286
         args_to_match concrete_ty in
      (* Debug.print_mtv Pretty.print_ty Format.err_formatter tv_to_ty; *)
      (* fresh terms to be added at the beginning of the list of arguments *)
      let new_ty_int = range (List.length type_vars) in
      let new_ty = List.map (fun x -> Mint.find x int_to_tyvars) new_ty_int in
      let new_terms = List.map (ty_to_term tblT varM tv_to_ty) new_ty in
      let transformed_terms = List.map
287
        (term_transform tblT tblL varM) terms in
Simon Cruanes's avatar
Simon Cruanes committed
288
      f_app new_p (new_terms @ transformed_terms)
289
    | _ -> (* otherwise : just traverse and translate *)
290 291
      f_map (term_transform tblT tblL varM)
        (fmla_transform tblT tblL varM) f
292

293 294


295 296
  (** transforms a list of logic declarations into another.
  Declares new lsymbols with explicit polymorphic signatures.
297 298
  @param tbl hashtable used to memoize new lsymbols *)
  let logic_transform tbl decls =
299
    (* if there is a definition, we must take it into account *)
300
    let helper = function
301
    | (lsymbol, Some ldef) ->
302
      let new_lsymbol = findL tbl lsymbol in (* new lsymbol *)
303 304
      let polymorphic_vars = List.fold_left find_tyvars []
          lsymbol.ls_args in (* get unique type vars *)
305 306
      let vars,expr = open_ls_defn ldef in
      let new_vars = List.map
307
        (fun _ -> Term.create_vsymbol (id_fresh "t") my_t)
308 309
        polymorphic_vars in (* new vars for polymorphism *)
      let vars = List.append new_vars vars in (* add new vars in signature *)
310
      (match expr with
311 312
      | Term t -> Decl.make_fs_defn new_lsymbol vars t
      | Fmla f -> Decl.make_ps_defn new_lsymbol vars (f_forall new_vars [] f))
313
    | (lsymbol, None) ->
314 315 316 317
      let new_lsymbol = findL tbl lsymbol in
      (new_lsymbol, None) in
    let cur_decl = List.map helper decls
    in [Decl.create_logic_decl cur_decl]
318 319 320 321 322


  (** transforms a list of type declarations *)
  let type_transform tbl tys =
    let helper = function
323 324 325 326
      | (ty_symbol, Tabstract) -> (findT tbl ty_symbol, None)
      | _ -> failwith "type_transform : no algebraic type should remain !" in
    let cur_decl = List.map helper tys in
    [Decl.create_ty_decl tys; Decl.create_logic_decl cur_decl]
327

328
  (** transforms a proposition into another (mostly a substitution) *)
329
  let prop_transform tblT tblL (prop_kind, prop_name, fmla) =
330 331 332 333
    let type_vars = (f_find_type_vars [] fmla) in
    let varM = List.fold_left (* create a vsymbol for each type var *)
      (fun m x -> Mty.add x (create_vsymbol (id_fresh "v") my_t) m)
      Mty.empty type_vars in
334 335
    (* Debug.print_mty Pretty.print_vs Format.err_formatter varM;
    Format.eprintf "-----------@."; *)
336
    (*universal quantification over ty vars*)
337
    let new_fmla = (fmla_transform tblT tblL varM fmla) in
338 339
    let quantified_fmla = f_forall (map_values varM) [] new_fmla in
    [Decl.create_prop_decl prop_kind prop_name quantified_fmla]
340

341
end
342

Simon Cruanes's avatar
Simon Cruanes committed
343 344
(** {2 main part} *)

345
(** main function, takes hashtables (for memoization of types and logic
346 347 348
    symbols) and a declaration, and returns the corresponding declaration in
    explicit polymorphism logic.
    It is to be applied on every declarations of the task. *)
349
let decl_transform tblT tblL d =
350
  (*Format.eprintf "%a@." Pretty.print_decl d;*)
351 352 353
  let result = match d.d_node with
    | Dind _inds ->
    failwith "Dind : should not have inductives declarations at this point !"
354 355 356
    | Dtype tys -> Transform.type_transform tblT tys
    | Dlogic decls -> Transform.logic_transform tblL decls
    | Dprop prop -> Transform.prop_transform tblT tblL prop in
357
  (*Format.eprintf "===@.%a@.@." (Debug.print_list Pretty.print_decl) result;*)
358
  result
359

360 361

(** the transformation to be registered.
362 363
    It creates two new hashtables, used everywhere, which updates are
    shared by side effects. *)
364 365
let explicit_polymorphism =
  let prelude_task = Task.add_decl None t_decl in (* declare t first *)
366 367
  Trans.decl
      (decl_transform (Hashtbl.create 21) (Hashtbl.create 42)) prelude_task
368

369

370
let () = Trans.register_transform "explicit_polymorphism" explicit_polymorphism
371