discriminate.ml 11.9 KB
Newer Older
Andrei Paskevich's avatar
Andrei Paskevich committed
1 2 3
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
4
(*  Copyright 2010-2014   --   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
  ~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 244 245 246 247 248 249 250 251 252 253 254 255 256 257 258 259 260 261
  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
262
    in
263 264 265 266
    aux env [] Mtv.empty (oty_cons ls.ls_args ls.ls_value)
  in
  Sls.fold fold_ls lskept env

267 268 269 270 271 272 273 274 275
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

276 277 278 279 280 281 282 283 284 285
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
286 287 288 289
    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
290
  in
291
  Trans.store trans
292 293 294 295 296

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

let discriminate env = Trans.seq [
302
  Libencoding.monomorphise_goal;
303
  select_lsinst env;
304
  Trans.print_meta Libencoding.debug meta_lsinst;
305 306 307 308
  lsymbol_distinction;
]

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

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