discriminate.ml 13.1 KB
Newer Older
Andrei Paskevich's avatar
Andrei Paskevich committed
1 2 3
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
4
(*  Copyright 2010-2015   --   INRIA - CNRS - Paris-Sud University  *)
Andrei Paskevich's avatar
Andrei Paskevich committed
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
(*                                                                  *)
Andrei Paskevich's avatar
Andrei Paskevich committed
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
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
  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
82 83 84
      let l = oty_cons tyl tyv in
      match Mtyl.find_opt l !m with
      | Some ls -> ls
85
      | None ->
86 87
          let nls = create_lsymbol (id_clone ls.ls_name) tyl tyv in
          m := Mtyl.add l nls !m;
88
          nls
89

90
  type t = lsymbol Mtyl.t Mls.t
91

92
  let empty = Mls.empty
93

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

103
(* dead code
104 105 106 107 108 109
  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
110
*)
111 112

  (** From/To metas *)
113 114 115 116 117
  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 []
118

119
  let of_metas metas =
120 121
    let fold env args =
      match args with
122 123 124
        | [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
125
          let insts = Mls.find_def Mtyl.empty ls env in
126 127 128 129 130 131 132
          Mls.add ls (Mtyl.add tydisl lsinst insts) env
        | _ -> assert false
    in
    List.fold_left fold Mls.empty metas

end

133 134 135 136
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
137

138 139 140
module Ssubst = Set.Make(struct
  type t = ty Mtv.t
  let compare = Mtv.compare OHTy.compare end)
141 142

(* find all the possible instantiation which can create a kept instantiation *)
143
let ty_quant env t =
144
  let add_vs acc0 ls tyl tyv =
145 146 147
    if ls_equal ls ps_equ then acc0 else
      try
        let insts = Mls.find ls env in
148
        let tyl = oty_cons tyl tyv in
149 150 151
        let fold_inst inst _ acc =
          let fold_subst subst acc =
            try
152
              let subst = List.fold_left2 ty_match subst tyl inst in
153 154 155 156 157 158 159 160 161
              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
162 163 164 165 166 167 168
  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
169
  let insts = Mls.find_def Mtyl.empty ls env in
170
  let sts = Mtyl.fold add_tyl insts Sts.empty in
171
  let add_ts ts dl = create_ty_decl ts :: dl in
172
  Sts.fold add_ts sts decls
173 174

(* The Core of the transformation *)
175
let map env d = match d.d_node with
176 177
  | Dtype _ -> [d]
  | Ddata _ -> Printer.unsupportedDecl d
178 179
      "Algebraic and recursively-defined types are \
            not supported, run eliminate_algebraic"
180
  | Dparam ls ->
181
      let lls = Mtyl.values (Mls.find_def Mtyl.empty ls env) in
182
      let lds = List.map create_param_decl lls in
183
      ts_of_ls env ls (d::lds)
184
  | Dlogic [ls,ld] when not (Sid.mem ls.ls_name d.d_syms) ->
185 186 187 188 189
      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
190 191 192 193 194 195 196
        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
197 198 199 200
      in
      let defns,axioms = Ssubst.fold conv_f substs ([],[]) in
      ts_of_ls env ls (List.rev_append defns axioms)
  | Dlogic _ -> Printer.unsupportedDecl d
201
      "Recursively-defined symbols are not supported, run eliminate_recursion"
202
  | Dind _ -> Printer.unsupportedDecl d
203
      "Inductive predicates are not supported, run eliminate_inductive"
204
  | Dprop (k,pr,f) ->
205 206 207 208
      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 *)
209
        (*   (t_ty_subst tvar Mvs.empty f) *)
210
        (*   print_env env; *)
211 212
        let f = t_ty_subst tvar Mvs.empty f in
        let f = t_app_map (find_logic env) f in
213 214 215 216 217 218 219 220 221 222 223 224 225 226 227
        (* 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

228
let ft_select_inst =
229
  ((Hstr.create 17) : (Env.env,Sty.t) Trans.flag_trans)
230 231

let ft_select_lskept =
232
  ((Hstr.create 17) : (Env.env,Sls.t) Trans.flag_trans)
233 234

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

237 238 239 240
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
241
  let add ty decls = create_meta Libencoding.meta_kept [MAty ty] :: decls in
242 243
  Sty.fold add sty (Lsmap.metas env)

244 245 246 247 248 249 250 251 252 253 254 255 256 257 258 259 260 261 262 263
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

264 265 266 267 268 269 270 271 272 273 274 275 276 277 278 279 280 281
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
282
    in
283 284 285 286
    aux env [] Mtv.empty (oty_cons ls.ls_args ls.ls_value)
  in
  Sls.fold fold_ls lskept env

287 288 289 290 291 292 293 294 295
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

296 297 298 299 300 301 302 303 304 305
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
306
    let lsinst = Task.on_meta meta_lsinst add_user_lsinst lsinst task in
307
    let inst   = inst_completion (Task.task_known task) inst in
308 309 310
    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
311
  in
312
  Trans.store trans
313 314 315 316 317

let lsymbol_distinction =
  Trans.on_meta meta_lsinst (fun metas ->
    if metas = [] then Trans.identity
    else
318
      let env = Lsmap.of_metas metas in
319
      (* Format.eprintf "instantiate %a@." print_env env; *)
320 321 322
      Trans.decl (map env) None)

let discriminate env = Trans.seq [
323
  Libencoding.monomorphise_goal;
324
  select_lsinst env;
325
  Trans.print_meta Libencoding.debug meta_lsinst;
326 327 328 329
  lsymbol_distinction;
]

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

333 334 335 336 337 338 339 340 341 342 343
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."

344 345 346 347 348 349 350 351 352 353 354 355 356 357 358 359 360 361
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)))