discriminate.ml 10.9 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
  type t = lsymbol Mtyl.t Mls.t
77

78
  let empty = Mls.empty
79

80 81
  let add ls tyl tyv lsmap =
    if ls_equal ls ps_equ then lsmap else
82
    if not (List.for_all Ty.ty_closed (oty_cons tyl tyv)) then lsmap else
83 84 85 86
    let newls = function
      | None -> Some (create_lsymbol (id_clone ls.ls_name) tyl tyv)
      | nls  -> nls
    in
87 88
    let insts = Mls.find_def Mtyl.empty ls lsmap in
    Mls.add ls (Mtyl.change newls (oty_cons tyl tyv) insts) lsmap
89

90
(* dead code
91 92 93 94 95 96
  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
97
*)
98 99

  (** From/To metas *)
100 101 102 103 104
  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 []
105

106
  let of_metas metas =
107 108
    let fold env args =
      match args with
109 110 111
        | [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
112
          let insts = Mls.find_def Mtyl.empty ls env in
113 114 115 116 117 118 119
          Mls.add ls (Mtyl.add tydisl lsinst insts) env
        | _ -> assert false
    in
    List.fold_left fold Mls.empty metas

end

120 121 122 123
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
124

125 126 127
module Ssubst = Set.Make(struct
  type t = ty Mtv.t
  let compare = Mtv.compare OHTy.compare end)
128 129

(* find all the possible instantiation which can create a kept instantiation *)
130
let ty_quant env t =
131
  let add_vs acc0 ls tyl tyv =
132 133 134
    if ls_equal ls ps_equ then acc0 else
      try
        let insts = Mls.find ls env in
135
        let tyl = oty_cons tyl tyv in
136 137 138
        let fold_inst inst _ acc =
          let fold_subst subst acc =
            try
139
              let subst = List.fold_left2 ty_match subst tyl inst in
140 141 142 143 144 145 146 147 148
              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
149 150 151 152 153 154 155
  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
156
  let insts = Mls.find_def Mtyl.empty ls env in
157
  let sts = Mtyl.fold add_tyl insts Sts.empty in
158
  let add_ts ts dl = create_ty_decl ts :: dl in
159
  Sts.fold add_ts sts decls
160 161

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

215 216

let ft_select_inst =
217
  ((Hstr.create 17) : (Env.env,Sty.t) Trans.flag_trans)
218 219

let ft_select_lskept =
220
  ((Hstr.create 17) : (Env.env,Sls.t) Trans.flag_trans)
221 222

let ft_select_lsinst =
223
  ((Hstr.create 17) : (Env.env,Lsmap.t) Trans.flag_trans)
224 225 226 227
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
228
  let add ty decls = create_meta Libencoding.meta_kept [MAty ty] :: decls in
229 230 231 232 233 234 235 236 237 238 239 240 241 242 243 244 245 246 247 248
  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
249
    in
250 251 252 253
    aux env [] Mtv.empty (oty_cons ls.ls_args ls.ls_value)
  in
  Sls.fold fold_ls lskept env

254 255 256 257 258 259 260 261 262
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

263 264 265 266 267 268 269 270 271 272
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
273 274 275 276
    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
277
  in
278
  Trans.store trans
279 280 281 282 283

let lsymbol_distinction =
  Trans.on_meta meta_lsinst (fun metas ->
    if metas = [] then Trans.identity
    else
284
      let env = Lsmap.of_metas metas in
285
      (* Format.eprintf "instantiate %a@." print_env env; *)
286 287 288
      Trans.decl (map env) None)

let discriminate env = Trans.seq [
289
  Libencoding.monomorphise_goal;
290
  select_lsinst env;
291
  Trans.print_meta Libencoding.debug meta_lsinst;
292 293 294 295
  lsymbol_distinction;
]

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