discriminate.ml 12.2 KB
Newer Older
1 2
(**************************************************************************)
(*                                                                        *)
MARCHE Claude's avatar
MARCHE Claude committed
3
(*  Copyright (C) 2010-2012                                               *)
4 5 6
(*    François Bobot                                                      *)
(*    Jean-Christophe Filliâtre                                           *)
(*    Claude Marché                                                       *)
MARCHE Claude's avatar
MARCHE Claude committed
7
(*    Guillaume Melquiond                                                 *)
8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28
(*    Andrei Paskevich                                                    *)
(*                                                                        *)
(*  This software is free software; you can redistribute it and/or        *)
(*  modify it under the terms of the GNU Library General Public           *)
(*  License version 2.1, with the special exception on linking            *)
(*  described in file LICENSE.                                            *)
(*                                                                        *)
(*  This software is distributed in the hope that it will be useful,      *)
(*  but WITHOUT ANY WARRANTY; without even the implied warranty of        *)
(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.                  *)
(*                                                                        *)
(**************************************************************************)

open Util
open Ident
open Ty
open Term
open Decl
open Theory
open Task

29
let meta_inst   = register_meta "encoding : inst"   [MTty]
30 31
  ~desc:"Specify@ which@ type@ should@ instantiate@ symbol@ marked@ by@ \
         'encoding : lskept'."
32
let meta_lskept = register_meta "encoding : lskept" [MTlsymbol]
33 34 35
  ~desc:"Specify@ which@ function@ symbols@ should@ be@ kept.@ If@ the@ \
         function@ is@ polymorphic,@ the@ monorphisations@ which@ signatures@ \
         contain@ only@ types@ @ marked@ with@ 'encoding : inst'@ are@ kept."
36
let meta_lsinst = register_meta "encoding : lsinst" [MTlsymbol;MTlsymbol]
37 38 39
  ~desc:"Specify@ which@ instantiations@ of@ symbols@ should@ be@ kept.@ \
         The first@ symbol@ specifies@ the@ symbol,@ the@ signature@ of@ the@ \
         second@ specifies@ the@ instantiation@ to@ keep."
40

41
let meta_select_inst   = register_meta_excl "select_inst"   [MTstring]
42 43 44 45 46 47 48 49 50
  ~desc:"@[Specify@ how@ to@ automatically@ mark@ type@ by@ \
'encoding : inst':@]@\n  \
@[\
  - none:@[ don't@ mark@ automatically@]@\n\
  - goal:@[ mark@ all@ the@ closed@ type@ that@ appear@ has@ argument@ \
            in@ the@ goal@]@\n\
  - all:@[ same@ as@ goal@ but@ also@ in@ the@ premises.@]\
@]"

51
let meta_select_lskept = register_meta_excl "select_lskept" [MTstring]
52 53 54 55 56 57 58 59 60 61
  ~desc:"@[Specify@ how@ to@ automatically@ mark@ symbol@ by@ \
'encoding : lskept':@]@\n  \
@[\
  - none:@[ don't@ mark@ automatically@]@\n\
  - goal:@[ mark@ all@ the@ symbols@ acceptable@ that@ appear@ in@ the@ \
            goal.@ The signature@ of an@ acceptable@ symbol@ contain@ at@ \
            least@ one@ type@ that@ is@ not@ a@ type@ variable@ neither@]@\n\
  - all:@[ same@ as@ goal@ but@ also@ in@ the@ premises.@]\
@]"

62
let meta_select_lsinst = register_meta_excl "select_lsinst" [MTstring]
63 64 65 66 67 68 69 70
  ~desc:"@[Specify@ how@ to@ automatically@ mark@ symbol@ by@ \
'encoding : lskept':@]@\n  \
@[\
  - none:@[ don't@ mark@ automatically@]@\n\
  - goal:@[ mark@ all@ the@ instantiation of symbols@ that@ appear@ in@ \
             the@ goal@]@\n\
  - all:@[ same@ as@ goal@ but@ also@ in@ the@ premises.@]\
@]"
71

72 73 74 75
module OHTy = OrderedHash(struct
  type t = ty
  let tag = ty_hash
end)
76

77 78 79 80
module OHTyl = OrderedHashList(struct
  type t = ty
  let tag = ty_hash
end)
81

82 83 84
module Mtyl = Stdlib.Map.Make(OHTyl)

module Lsmap = struct
85 86 87 88 89

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

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 98 99 100
    let newls = function
      | None -> Some (create_lsymbol (id_clone ls.ls_name) tyl tyv)
      | nls  -> nls
    in
101 102
    let insts = Mls.find_def Mtyl.empty ls lsmap in
    Mls.add ls (Mtyl.change newls (oty_cons tyl tyv) insts) lsmap
103 104 105 106 107 108 109 110 111

  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

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

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

end

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

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

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

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

227 228 229 230 231 232 233 234 235 236 237 238 239

let ft_select_inst =
  ((Hashtbl.create 17) : (Env.env,Sty.t) Trans.flag_trans)

let ft_select_lskept =
  ((Hashtbl.create 17) : (Env.env,Sls.t) Trans.flag_trans)

let ft_select_lsinst =
  ((Hashtbl.create 17) : (Env.env,Lsmap.t) Trans.flag_trans)
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
240
  let add ty decls = create_meta Libencoding.meta_kept [MAty ty] :: decls in
241 242 243 244 245 246 247 248 249 250 251 252 253 254 255 256 257 258 259 260
  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
261
    in
262 263 264 265
    aux env [] Mtv.empty (oty_cons ls.ls_args ls.ls_value)
  in
  Sls.fold fold_ls lskept env

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

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

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

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

307 308
let empty_formatted : Pp.formatted = ""

309
let () = Trans.register_env_transform "discriminate" discriminate
310 311 312 313 314 315 316 317 318
  ~desc_metas:[meta_select_inst  , empty_formatted;
               meta_select_lskept, empty_formatted;
               meta_select_lsinst, empty_formatted;
               meta_inst         , empty_formatted;
               meta_lskept       , empty_formatted;
               meta_lsinst       , empty_formatted]
  ~desc:"Discriminate@ polymorphic@ function@ and@ predicate@ symbols.@ \
         Allow@ to@ keep@ some@ instantiations@ from@ being@ touched@ by@ \
         following@ polymorphism@ encodings."
319