discriminate.ml 14.1 KB
Newer Older
1 2 3
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
Andrei Paskevich's avatar
Andrei Paskevich committed
4
(*  Copyright 2010-2016   --   INRIA - CNRS - Paris-Sud University  *)
5 6 7 8
(*                                                                  *)
(*  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.                           *)
9
(*                                                                  *)
10
(********************************************************************)
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
  ~desc:"Specify@ which@ function/predicate@ symbols@ should@ be@ kept.@ \
         When@ the@ symbol@ is@ polymorphic,@ generate@ every@ possible@ \
27
         type@ instances@ with@ types@ marked@ by@ 'encoding : inst'."
Andrei Paskevich's avatar
Andrei Paskevich committed
28

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 59 60 61 62 63 64 65 66 67 68 69
let meta_select_inst_default =
  register_meta_excl "select_inst_default" [MTstring]
  ~desc:"Default@ setting@ for@ select_inst"

let meta_select_lskept_default =
  register_meta_excl "select_lskept_default" [MTstring]
  ~desc:"Default@ setting@ for@ select_lskept"

let meta_select_lsinst_default =
  register_meta_excl "select_lsinst_default" [MTstring]
  ~desc:"Default@ setting@ for@ select_lsinst"

70
module OHTy = OrderedHashed(struct
71 72 73
  type t = ty
  let tag = ty_hash
end)
74

75
module OHTyl = OrderedHashedList(struct
76 77 78
  type t = ty
  let tag = ty_hash
end)
79

80
module Mtyl = Extmap.Make(OHTyl)
81 82

module Lsmap = struct
83 84 85 86 87

(* 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 *)

88 89 90 91 92 93
  let ls_inst =
    (* FIXME? Skolem type constants are short-living but
       will stay in lsmap as long as the lsymbol is alive *)
    let lsmap = Wls.memoize 63 (fun _ -> ref Mtyl.empty) in
    fun ls tyl tyv ->
      let m = lsmap ls in
94 95 96
      let l = oty_cons tyl tyv in
      match Mtyl.find_opt l !m with
      | Some ls -> ls
97
      | None ->
98 99
          let nls = create_lsymbol (id_clone ls.ls_name) tyl tyv in
          m := Mtyl.add l nls !m;
100
          nls
101

102
  type t = lsymbol Mtyl.t Mls.t
103

104
  let empty = Mls.empty
105

106 107
  let add ls tyl tyv lsmap =
    if ls_equal ls ps_equ then lsmap else
108
    if not (List.for_all Ty.ty_closed (oty_cons tyl tyv)) then lsmap else
109
    let newls = function
110 111
      | None -> Some (ls_inst ls tyl tyv)
      | nls  -> nls in
112 113
    let insts = Mls.find_def Mtyl.empty ls lsmap in
    Mls.add ls (Mtyl.change newls (oty_cons tyl tyv) insts) lsmap
114

115
(* dead code
116 117 118 119 120 121
  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
122
*)
123 124

  (** From/To metas *)
125 126 127 128 129
  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 []
130

131
  let of_metas metas =
132 133
    let fold env args =
      match args with
134 135 136
        | [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
137
          let insts = Mls.find_def Mtyl.empty ls env in
138 139 140 141 142 143 144
          Mls.add ls (Mtyl.add tydisl lsinst insts) env
        | _ -> assert false
    in
    List.fold_left fold Mls.empty metas

end

145 146 147 148
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
149

150 151 152
module Ssubst = Set.Make(struct
  type t = ty Mtv.t
  let compare = Mtv.compare OHTy.compare end)
153 154

(* find all the possible instantiation which can create a kept instantiation *)
155
let ty_quant env t =
156
  let add_vs acc0 ls tyl tyv =
157 158 159
    if ls_equal ls ps_equ then acc0 else
      try
        let insts = Mls.find ls env in
160
        let tyl = oty_cons tyl tyv in
161 162 163
        let fold_inst inst _ acc =
          let fold_subst subst acc =
            try
164
              let subst = List.fold_left2 ty_match subst tyl inst in
165 166 167 168 169 170 171 172 173
              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
174 175 176 177 178 179 180
  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
181
  let insts = Mls.find_def Mtyl.empty ls env in
182
  let sts = Mtyl.fold add_tyl insts Sts.empty in
183
  let add_ts ts dl = create_ty_decl ts :: dl in
184
  Sts.fold add_ts sts decls
185 186

(* The Core of the transformation *)
187 188 189 190 191
let map metas_rewrite_pr env d =
  let decls,metas =
    match d.d_node with
    | Dtype _ -> [d],[]
    | Ddata _ -> Printer.unsupportedDecl d
192 193
      "Algebraic and recursively-defined types are \
            not supported, run eliminate_algebraic"
194
    | Dparam ls ->
195
      let lls = Mtyl.values (Mls.find_def Mtyl.empty ls env) in
196
      let lds = List.map create_param_decl lls in
197 198
      ts_of_ls env ls (d::lds),[]
    | Dlogic [ls,ld] when not (Sid.mem ls.ls_name d.d_syms) ->
199 200 201 202 203
      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
204 205 206 207 208 209 210
        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
211 212
      in
      let defns,axioms = Ssubst.fold conv_f substs ([],[]) in
213
      ts_of_ls env ls (List.rev_append defns axioms),[]
214
  | Dlogic _ -> Printer.unsupportedDecl d
215
      "Recursively-defined symbols are not supported, run eliminate_recursion"
216
  | Dind _ -> Printer.unsupportedDecl d
217
      "Inductive predicates are not supported, run eliminate_inductive"
218
  | Dprop (k,pr,f) ->
219 220
      let substs = ty_quant env f in
      let substs_len = Ssubst.cardinal substs in
221
      let conv_f tvar (task,metas) =
222
        (* Format.eprintf "f0 : %a@. env : %a@." Pretty.print_fmla *)
223
        (*   (t_ty_subst tvar Mvs.empty f) *)
224
        (*   print_env env; *)
225 226
        let f = t_ty_subst tvar Mvs.empty f in
        let f = t_app_map (find_logic env) f in
227 228 229 230 231 232 233
        (* Format.eprintf "f : %a@. env : %a@." Pretty.print_fmla f *)
        (*   print_env menv; *)
        (* 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; *)
234 235 236 237 238 239 240 241
        if substs_len = 1 then
          create_prop_decl k pr f :: task, metas
        else
          let pr' = create_prsymbol (id_clone pr.pr_name) in
          create_prop_decl k pr' f :: task,
          (if Spr.mem pr metas_rewrite_pr then
              create_meta Compute.meta_rewrite [MApr pr'] :: metas
           else metas)
242
      in
243 244 245 246
      Ssubst.fold conv_f substs ([],[])
  in
  List.rev_append (List.rev_map create_decl decls) metas

247

248
let ft_select_inst =
249
  ((Hstr.create 17) : (Env.env,Sty.t) Trans.flag_trans)
250 251

let ft_select_lskept =
252
  ((Hstr.create 17) : (Env.env,Sls.t) Trans.flag_trans)
253 254

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

257 258 259 260
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
261
  let add ty decls = create_meta Libencoding.meta_kept [MAty ty] :: decls in
262 263
  Sty.fold add sty (Lsmap.metas env)

264 265 266 267 268 269 270 271 272 273 274 275 276 277 278 279 280 281 282 283
let inst_completion kn kept =
  let rec inst_constructors ty acc = match ty.ty_node with
    | Tyapp (ts,tyl) when not (Sty.mem ty acc) ->
        let acc = Sty.add ty acc in
        let tys = Sty.of_list tyl in
        let csl = Decl.find_constructors kn ts in
        let tys = if csl = [] then tys else
          let d = Mid.find ts.ts_name kn in
          let base = ty_app ts (List.map ty_var ts.ts_args) in
          let sbs = ty_match Mtv.empty base ty in
          let recu ts = Sid.mem ts.ts_name d.d_news in
          let add_fd tys ty = if ty_s_any recu ty
            then tys else Sty.add (ty_inst sbs ty) tys in
          let add_cs tys (cs,_) =
            List.fold_left add_fd tys cs.ls_args in
          List.fold_left add_cs tys csl in
        Sty.fold inst_constructors tys acc
    | _ -> acc in
  Sty.fold inst_constructors kept Sty.empty

284 285 286 287 288 289 290 291 292 293 294 295 296 297 298 299 300 301
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
302
    in
303 304 305 306
    aux env [] Mtv.empty (oty_cons ls.ls_args ls.ls_value)
  in
  Sls.fold fold_ls lskept env

307 308 309 310 311 312 313 314 315
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

316
let select_lsinst env =
317 318 319 320 321 322 323 324
  let select m1 m2 ft =
    Trans.on_flag_t m1 ft (Trans.on_flag m2 ft "none") env in
  let inst   =
    select meta_select_inst   meta_select_inst_default   ft_select_inst   in
  let lskept =
    select meta_select_lskept meta_select_lskept_default ft_select_lskept in
  let lsinst =
    select meta_select_lsinst meta_select_lsinst_default ft_select_lsinst in
325 326 327 328 329 330
  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
331
    let lsinst = Task.on_meta meta_lsinst add_user_lsinst lsinst task in
332
    let inst   = inst_completion (Task.task_known task) inst in
333 334 335
    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
336
  in
337
  Trans.store trans
338 339 340 341 342

let lsymbol_distinction =
  Trans.on_meta meta_lsinst (fun metas ->
    if metas = [] then Trans.identity
    else
343
      let env = Lsmap.of_metas metas in
344
      (* Format.eprintf "instantiate %a@." print_env env; *)
345 346
      Trans.on_tagged_pr Compute.meta_rewrite (fun rewrite_pr ->
        Trans.tdecl (map rewrite_pr env) None))
347 348

let discriminate env = Trans.seq [
349
  Libencoding.monomorphise_goal;
350
  select_lsinst env;
351
  Trans.print_meta Libencoding.debug meta_lsinst;
352 353 354 355
  lsymbol_distinction;
]

let () = Trans.register_env_transform "discriminate" discriminate
Andrei Paskevich's avatar
Andrei Paskevich committed
356 357
  ~desc:"Generate@ monomorphic@ type@ instances@ of@ function@ and@ \
         predicate@ symbols@ and@ monomorphize@ task@ premises."
358

359 360 361 362 363 364 365 366 367 368 369
let discriminate_if_poly env =
  Trans.on_meta Detect_polymorphism.meta_monomorphic_types_only
    (function
    | [] -> discriminate env
    | _ -> Trans.identity)

let () =
  Trans.register_env_transform "discriminate_if_poly"
    discriminate_if_poly
    ~desc:"Same@ as@ discriminate@ but@ only@ if@ polymorphism@ appear."

370 371 372 373 374 375 376
let li_add_ls acc = function
  | [MAls ls; MAls nls] -> Mls.add nls ls acc
  | _ -> assert false

let get_lsinst task =
  Task.on_meta meta_lsinst li_add_ls Mls.empty task

377 378
let on_lsinst fn =
  Trans.on_meta meta_lsinst (fun dls ->
379 380 381 382 383 384 385 386 387 388 389 390 391
    fn (List.fold_left li_add_ls Mls.empty dls))

let sm_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

let get_syntax_map task =
  let sm0 = Printer.get_syntax_map task in
  Task.on_meta meta_lsinst (sm_add_ls sm0) sm0 task
392 393 394 395

let on_syntax_map fn =
  Printer.on_syntax_map (fun sm0 ->
  Trans.on_meta meta_lsinst (fun dls ->
396
    fn (List.fold_left (sm_add_ls sm0) sm0 dls)))