discriminate.ml 11.7 KB
Newer Older
Andrei Paskevich's avatar
Andrei Paskevich committed
1 2 3
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
4
(*  Copyright 2010-2013   --   INRIA - CNRS - Paris-Sud University  *)
Andrei Paskevich's avatar
Andrei Paskevich committed
5 6 7 8 9 10
(*                                                                  *)
(*  This software is distributed under the terms of the GNU Lesser  *)
(*  General Public License version 2.1, with the special exception  *)
(*  on linking described in file LICENSE.                           *)
(*                                                                  *)
(********************************************************************)
11

12
open Stdlib
13 14 15 16 17 18 19
open Ident
open Ty
open Term
open Decl
open Theory
open Task

Andrei Paskevich's avatar
Andrei Paskevich committed
20 21
let meta_inst = register_meta "encoding : inst" [MTty]
  ~desc:"Specify@ which@ types@ should@ instantiate@ symbols@ marked@ by@ \
22
         'encoding : lskept'."
Andrei Paskevich's avatar
Andrei Paskevich committed
23

24
let meta_lskept = register_meta "encoding : lskept" [MTlsymbol]
Andrei Paskevich's avatar
Andrei Paskevich committed
25 26 27 28
  ~desc:"Specify@ which@ function/predicate@ symbols@ should@ be@ kept.@ \
         When@ the@ symbol@ is@ polymorphic,@ generate@ every@ possible@ \
         type@ insntance@ with@ types@ marked@ by@ 'encoding : inst'."

29
let meta_lsinst = register_meta "encoding : lsinst" [MTlsymbol;MTlsymbol]
Andrei Paskevich's avatar
Andrei Paskevich committed
30 31 32 33 34 35 36 37 38 39 40
  ~desc:"Specify@ which@ type@ instances@ of@ symbols@ should@ be@ kept.@ \
         The first@ symbol@ specifies@ the@ polymorphic@ symbol,@ \
         the@ second@ provides@ a@ monomorphic@ type@ signature@ to@ keep."

let meta_select_inst = register_meta_excl "select_inst" [MTstring]
  ~desc:"Specify@ the@ types@ to@ mark@ with@ 'encoding : inst':@;  \
    @[\
      - none: @[don't@ mark@ any@ type@ automatically@]@\n\
      - goal: @[mark@ every@ closed@ type@ in@ the@ goal@]@\n\
      - all:  @[mark@ every@ closed@ type@ in@ the@ task.@]\
    @]"
41

42
let meta_select_lskept = register_meta_excl "select_lskept" [MTstring]
Andrei Paskevich's avatar
Andrei Paskevich committed
43 44 45 46 47 48
  ~desc:"Specify@ the@ symbols@ to@ mark@ with@ 'encoding : lskept':@;  \
    @[\
      - none: @[don't@ mark@ any@ symbol@ automatically@]@\n\
      - goal: @[mark@ every@ polymorphic@ symbol@ in@ the@ goal@]@\n\
      - all:  @[mark@ every@ polymorphic@ symbol@ in@ the@ task.@]\
    @]"
49

50
let meta_select_lsinst = register_meta_excl "select_lsinst" [MTstring]
Andrei Paskevich's avatar
Andrei Paskevich committed
51 52 53 54 55 56
  ~desc:"Specify@ the@ symbols@ to@ mark@ with@ 'encoding : lsinst':@;  \
    @[\
      - none: @[don't@ mark@ any@ symbol@ automatically@]@\n\
      - goal: @[mark@ every@ monomorphic@ instance@ in@ the@ goal@]@\n\
      - all:  @[mark@ every@ monomorphic@ instance@ in@ the@ task.@]\
    @]"
57

58
module OHTy = OrderedHashed(struct
59 60 61
  type t = ty
  let tag = ty_hash
end)
62

63
module OHTyl = OrderedHashedList(struct
64 65 66
  type t = ty
  let tag = ty_hash
end)
67

68
module Mtyl = Extmap.Make(OHTyl)
69 70

module Lsmap = struct
71 72 73 74 75

(* TODO : transmettre les tags des logiques polymorphe vers les logiques
   instantié. Un tag sur un logique polymorphe doit être un tag sur toute
   la famille de fonctions *)

76 77 78 79 80 81 82 83 84 85 86
  let ls_inst = Wls.memoize 3 (fun ls ->
    let m = ref Mtyl.empty in
    fun tyl tyv ->
      let l = oty_cons tyl tyv in
      match Mtyl.find_opt l !m with
      | Some ls -> ls
      | None    ->
          let nls = create_lsymbol (id_clone ls.ls_name) tyl tyv in
          m := Mtyl.add l nls !m;
          nls)

87
  type t = lsymbol Mtyl.t Mls.t
88

89
  let empty = Mls.empty
90

91 92
  let add ls tyl tyv lsmap =
    if ls_equal ls ps_equ then lsmap else
93
    if not (List.for_all Ty.ty_closed (oty_cons tyl tyv)) then lsmap else
94
    let newls = function
95 96
      | None -> Some (ls_inst ls tyl tyv)
      | nls  -> nls in
97 98
    let insts = Mls.find_def Mtyl.empty ls lsmap in
    Mls.add ls (Mtyl.change newls (oty_cons tyl tyv) insts) lsmap
99

100
(* dead code
101 102 103 104 105 106
  let print_env fmt menv =
    Format.fprintf fmt "defined_lsymbol (%a)@."
      (Pp.print_iter2 Mls.iter Pp.semi Pp.comma Pretty.print_ls
         (Pp.print_iter2 Mtyl.iter Pp.semi Pp.arrow
            (Pp.print_list Pp.space Pretty.print_ty)
            Pretty.print_ls)) menv
107
*)
108 109

  (** From/To metas *)
110 111 112 113 114
  let metas lsmap =
    let fold_inst ls _ lsinst decls =
      create_meta meta_lsinst [MAls ls; MAls lsinst] :: decls in
    let fold_ls ls insts decls = Mtyl.fold (fold_inst ls) insts decls in
    Mls.fold fold_ls lsmap []
115

116
  let of_metas metas =
117 118
    let fold env args =
      match args with
119 120 121
        | [MAls ls; MAls lsinst] ->
          let tydisl = oty_cons lsinst.ls_args lsinst.ls_value in
          if not (List.for_all Ty.ty_closed tydisl) then env else
122
          let insts = Mls.find_def Mtyl.empty ls env in
123 124 125 126 127 128 129
          Mls.add ls (Mtyl.add tydisl lsinst insts) env
        | _ -> assert false
    in
    List.fold_left fold Mls.empty metas

end

130 131 132 133
let find_logic env ls tyl tyv =
  if ls_equal ls ps_equ then ls else
  try Mtyl.find (oty_cons tyl tyv) (Mls.find ls env)
  with Not_found -> ls
134

135 136 137
module Ssubst = Set.Make(struct
  type t = ty Mtv.t
  let compare = Mtv.compare OHTy.compare end)
138 139

(* find all the possible instantiation which can create a kept instantiation *)
140
let ty_quant env t =
141
  let add_vs acc0 ls tyl tyv =
142 143 144
    if ls_equal ls ps_equ then acc0 else
      try
        let insts = Mls.find ls env in
145
        let tyl = oty_cons tyl tyv in
146 147 148
        let fold_inst inst _ acc =
          let fold_subst subst acc =
            try
149
              let subst = List.fold_left2 ty_match subst tyl inst in
150 151 152 153 154 155 156 157 158
              Ssubst.add subst acc
            with TypeMismatch _ -> acc
          in
          (* fold on acc0 *)
          Ssubst.fold fold_subst acc0 acc
        in
        Mtyl.fold fold_inst insts acc0
      with Not_found (* no such p *) -> acc0
  in
159 160 161 162 163 164 165
  t_app_fold add_vs (Ssubst.singleton (Mtv.empty)) t

let ts_of_ls env ls decls =
  if ls_equal ls ps_equ then decls else
  let add_ts sts ts = Sts.add ts sts in
  let add_ty sts ty = ty_s_fold add_ts sts ty in
  let add_tyl tyl _ sts = List.fold_left add_ty sts tyl in
166
  let insts = Mls.find_def Mtyl.empty ls env in
167
  let sts = Mtyl.fold add_tyl insts Sts.empty in
168
  let add_ts ts dl = create_ty_decl ts :: dl in
169
  Sts.fold add_ts sts decls
170 171

(* The Core of the transformation *)
172
let map env d = match d.d_node with
173 174
  | Dtype _ -> [d]
  | Ddata _ -> Printer.unsupportedDecl d
175 176
      "Algebraic and recursively-defined types are \
            not supported, run eliminate_algebraic"
177
  | Dparam ls ->
178
      let lls = Mtyl.values (Mls.find_def Mtyl.empty ls env) in
179
      let lds = List.map create_param_decl lls in
180
      ts_of_ls env ls (d::lds)
181
  | Dlogic [ls,ld] when not (Sid.mem ls.ls_name d.d_syms) ->
182 183 184 185 186
      let f = ls_defn_axiom ld in
      let substs = ty_quant env f in
      let conv_f tvar (defns,axioms) =
        let f = t_ty_subst tvar Mvs.empty f in
        let f = t_app_map (find_logic env) f in
187 188 189 190 191 192 193
        match ls_defn_of_axiom f with
          | Some ld ->
              create_logic_decl [ld] :: defns, axioms
          | None ->
              let nm = ls.ls_name.id_string ^ "_inst" in
              let pr = create_prsymbol (id_derive nm ls.ls_name) in
              defns, create_prop_decl Paxiom pr f :: axioms
194 195 196 197
      in
      let defns,axioms = Ssubst.fold conv_f substs ([],[]) in
      ts_of_ls env ls (List.rev_append defns axioms)
  | Dlogic _ -> Printer.unsupportedDecl d
198
      "Recursively-defined symbols are not supported, run eliminate_recursion"
199
  | Dind _ -> Printer.unsupportedDecl d
200
      "Inductive predicates are not supported, run eliminate_inductive"
201
  | Dprop (k,pr,f) ->
202 203 204 205
      let substs = ty_quant env f in
      let substs_len = Ssubst.cardinal substs in
      let conv_f tvar task =
        (* Format.eprintf "f0 : %a@. env : %a@." Pretty.print_fmla *)
206
        (*   (t_ty_subst tvar Mvs.empty f) *)
207
        (*   print_env env; *)
208 209
        let f = t_ty_subst tvar Mvs.empty f in
        let f = t_app_map (find_logic env) f in
210 211 212 213 214 215 216 217 218 219 220 221 222 223 224
        (* Format.eprintf "f : %a@. env : %a@." Pretty.print_fmla f *)
        (*   print_env menv; *)
        let pr =
          if substs_len = 1 then pr
          else create_prsymbol (id_clone pr.pr_name) in
        (* Format.eprintf "undef ls : %a, ts : %a@." *)
        (*   (Pp.print_iter1 Sls.iter Pp.comma Pretty.print_ls) *)
        (*   menv.undef_lsymbol *)
        (*   (Pp.print_iter1 Sts.iter Pp.comma Pretty.print_ts) *)
        (*   menv.undef_tsymbol; *)
        create_prop_decl k pr f :: task
      in
      let task = Ssubst.fold conv_f substs [] in
      task

225
let ft_select_inst =
226
  ((Hstr.create 17) : (Env.env,Sty.t) Trans.flag_trans)
227 228

let ft_select_lskept =
229
  ((Hstr.create 17) : (Env.env,Sls.t) Trans.flag_trans)
230 231

let ft_select_lsinst =
232
  ((Hstr.create 17) : (Env.env,Lsmap.t) Trans.flag_trans)
233

234 235 236 237
let metas_from_env env =
  let fold_inst tyl _ s = List.fold_left (fun s ty -> Sty.add ty s) s tyl in
  let fold_ls _ insts s = Mtyl.fold fold_inst insts s in
  let sty = Mls.fold fold_ls env Sty.empty in
238
  let add ty decls = create_meta Libencoding.meta_kept [MAty ty] :: decls in
239 240 241 242 243 244 245 246 247 248 249 250 251 252 253 254 255 256 257 258
  Sty.fold add sty (Lsmap.metas env)

let lsinst_completion kept lskept env =
  let fold_ls ls env =
    let rec aux env tydisl subst = function
      | [] ->
          let tydisl = List.rev tydisl in
          let tyl,tyv = match tydisl, ls.ls_value with
            | tyv::tyl, Some _ -> tyl, Some tyv
            | tyl, None -> tyl, None
            | _ -> assert false in
          Lsmap.add ls tyl tyv env
      | ty::tyl ->
          let fold_ty tykept env =
            try
              let subst = ty_match subst ty tykept in
              aux env (tykept::tydisl) subst tyl
            with TypeMismatch _ -> env
          in
          Sty.fold fold_ty kept env
259
    in
260 261 262 263
    aux env [] Mtv.empty (oty_cons ls.ls_args ls.ls_value)
  in
  Sls.fold fold_ls lskept env

264 265 266 267 268 269 270 271 272
let add_user_lsinst env = function
  | [MAls ls; MAls nls] -> Lsmap.add ls nls.ls_args nls.ls_value env
  | _ -> assert false

let clear_metas = Trans.fold (fun hd task ->
  match hd.task_decl.td_node with
    | Meta (m,_) when meta_equal m meta_lsinst -> task
    | _ -> add_tdecl task hd.task_decl) None

273 274 275 276 277 278 279 280 281 282
let select_lsinst env =
  let inst   = Trans.on_flag meta_select_inst   ft_select_inst   "none" env in
  let lskept = Trans.on_flag meta_select_lskept ft_select_lskept "none" env in
  let lsinst = Trans.on_flag meta_select_lsinst ft_select_lsinst "none" env in
  let trans task =
    let inst   = Trans.apply inst   task in
    let lskept = Trans.apply lskept task in
    let lsinst = Trans.apply lsinst task in
    let inst   = Sty.union inst   (Task.on_tagged_ty meta_inst   task) in
    let lskept = Sls.union lskept (Task.on_tagged_ls meta_lskept task) in
283 284 285 286
    let lsinst = Task.on_meta meta_lsinst add_user_lsinst lsinst task in
    let lsinst = lsinst_completion inst lskept lsinst in
    let task   = Trans.apply clear_metas task in
    Trans.apply (Trans.add_tdecls (metas_from_env lsinst)) task
287
  in
288
  Trans.store trans
289 290 291 292 293

let lsymbol_distinction =
  Trans.on_meta meta_lsinst (fun metas ->
    if metas = [] then Trans.identity
    else
294
      let env = Lsmap.of_metas metas in
295
      (* Format.eprintf "instantiate %a@." print_env env; *)
296 297 298
      Trans.decl (map env) None)

let discriminate env = Trans.seq [
299
  Libencoding.monomorphise_goal;
300
  select_lsinst env;
301
  Trans.print_meta Libencoding.debug meta_lsinst;
302 303 304 305
  lsymbol_distinction;
]

let () = Trans.register_env_transform "discriminate" discriminate
Andrei Paskevich's avatar
Andrei Paskevich committed
306 307
  ~desc:"Generate@ monomorphic@ type@ instances@ of@ function@ and@ \
         predicate@ symbols@ and@ monomorphize@ task@ premises."
308 309 310 311 312 313 314 315 316 317 318 319 320 321 322 323 324 325 326

let on_lsinst fn =
  let add_ls acc = function
    | [MAls ls; MAls nls] -> Mls.add nls ls acc
    | _ -> assert false in
  Trans.on_meta meta_lsinst (fun dls ->
    fn (List.fold_left add_ls Mls.empty dls))

let on_syntax_map fn =
  let add_ls sm0 sm = function
    | [MAls ls; MAls nls] ->
        begin match Mid.find_opt ls.ls_name sm0 with
          | Some s -> Mid.add nls.ls_name s sm
          | None -> sm
        end
    | _ -> assert false in
  Printer.on_syntax_map (fun sm0 ->
  Trans.on_meta meta_lsinst (fun dls ->
    fn (List.fold_left (fun sm dl -> add_ls sm0 sm dl) sm0 dls)))