discriminate.ml 10.1 KB
Newer Older
1 2
(**************************************************************************)
(*                                                                        *)
3
(*  Copyright (C) 2010-2011                                               *)
4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27
(*    François Bobot                                                     *)
(*    Jean-Christophe Filliâtre                                          *)
(*    Claude Marché                                                      *)
(*    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

28 29 30
let meta_inst   = register_meta "encoding : inst"   [MTty]
let meta_lskept = register_meta "encoding : lskept" [MTlsymbol]
let meta_lsinst = register_meta "encoding : lsinst" [MTlsymbol;MTlsymbol]
31

32 33 34
let meta_select_inst   = register_meta_excl "select_inst"   [MTstring]
let meta_select_lskept = register_meta_excl "select_lskept" [MTstring]
let meta_select_lsinst = register_meta_excl "select_lsinst" [MTstring]
35

36 37 38 39
module OHTy = OrderedHash(struct
  type t = ty
  let tag = ty_hash
end)
40

41 42 43 44
module OHTyl = OrderedHashList(struct
  type t = ty
  let tag = ty_hash
end)
45

46 47 48
module Mtyl = Stdlib.Map.Make(OHTyl)

module Lsmap = struct
49 50 51 52 53

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

54
  type t = lsymbol Mtyl.t Mls.t
55

56
  let empty = Mls.empty
57

58 59
  let add ls tyl tyv lsmap =
    if ls_equal ls ps_equ then lsmap else
60
    if not (List.for_all Ty.ty_closed (oty_cons tyl tyv)) then lsmap else
61 62 63 64 65 66
    let newls = function
      | None -> Some (create_lsymbol (id_clone ls.ls_name) tyl tyv)
      | nls  -> nls
    in
    let insts = Mls.find_default ls Mtyl.empty lsmap in
    Mls.add ls (Mtyl.change (oty_cons tyl tyv) newls insts) lsmap
67 68 69 70 71 72 73 74 75

  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 *)
76 77 78 79 80
  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 []
81

82
  let of_metas metas =
83 84
    let fold env args =
      match args with
85 86 87
        | [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
88 89 90 91 92 93 94 95
          let insts = Mls.find_default ls Mtyl.empty env in
          Mls.add ls (Mtyl.add tydisl lsinst insts) env
        | _ -> assert false
    in
    List.fold_left fold Mls.empty metas

end

96 97 98 99
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
100 101 102 103 104 105

module Ssubst =
  Set.Make(struct type t = ty Mtv.t
                  let compare = Mtv.compare OHTy.compare end)

(* find all the possible instantiation which can create a kept instantiation *)
106
let ty_quant env t =
107 108 109 110
  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
111
        let tyl = oty_cons tyl tyv in
112 113 114 115 116 117 118 119 120 121 122 123 124
        let fold_inst inst _ acc =
          let fold_subst subst acc =
            try
              let subst = List.fold_left2 ty_match subst tyl inst  in
              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
125 126 127 128 129 130 131 132 133 134 135
  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
  let insts = Mls.find_default ls Mtyl.empty env in
  let sts = Mtyl.fold add_tyl insts Sts.empty in
  let add_ts ts dl = create_ty_decl [ts,Tabstract] :: dl in
  Sts.fold add_ts sts decls
136 137

(* The Core of the transformation *)
138 139 140 141 142 143 144 145 146 147 148 149 150 151 152
let map env d = match d.d_node with
  | Dtype [_,Tabstract] -> [d]
  | Dtype _ -> Printer.unsupportedDecl d
      "Algebraic and recursively-defined types are \
            not supported, run eliminate_algebraic"
  | Dlogic [ls, None] ->
      let lls = Mtyl.values (Mls.find_default ls Mtyl.empty env) in
      let lds = List.map (fun ls -> create_logic_decl [ls,None]) lls in
      ts_of_ls env ls (d::lds)
  | Dlogic [ls, Some ld] when not (Sid.mem ls.ls_name d.d_syms) ->
      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
153 154 155 156 157 158 159
        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
160 161 162 163 164 165 166 167 168 169
      in
      let defns,axioms = Ssubst.fold conv_f substs ([],[]) in
      ts_of_ls env ls (List.rev_append defns axioms)
  | Dlogic _ -> Printer.unsupportedDecl d
      "Recursively-defined symbols are not supported, \
            run eliminate_recursion"
  | Dind _ -> Printer.unsupportedDecl d
      "Inductive predicates are not supported, \
            run eliminate_inductive"
  | Dprop (k,pr,f) ->
170 171 172 173
      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 *)
174
        (*   (t_ty_subst tvar Mvs.empty f) *)
175
        (*   print_env env; *)
176 177
        let f = t_ty_subst tvar Mvs.empty f in
        let f = t_app_map (find_logic env) f in
178 179 180 181 182 183 184 185 186 187 188 189 190 191 192
        (* 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

193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214 215 216 217 218 219 220 221 222 223 224 225 226 227

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
  let add ty decls = create_meta Encoding.meta_kept [MAty ty] :: decls in
  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
228
    in
229 230 231 232
    aux env [] Mtv.empty (oty_cons ls.ls_args ls.ls_value)
  in
  Sls.fold fold_ls lskept env

233 234 235 236 237 238 239 240 241
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

242 243 244 245 246 247 248 249 250 251
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
252 253 254 255
    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
256
  in
257
  Trans.store trans
258 259 260 261 262

let lsymbol_distinction =
  Trans.on_meta meta_lsinst (fun metas ->
    if metas = [] then Trans.identity
    else
263
      let env = Lsmap.of_metas metas in
264
      (* Format.eprintf "instantiate %a@." print_env env; *)
265 266 267 268 269 270 271 272 273 274 275
      Trans.decl (map env) None)

let discriminate env = Trans.seq [
  Encoding.monomorphise_goal;
  select_lsinst env;
  Trans.print_meta Encoding.debug meta_lsinst;
  lsymbol_distinction;
]

let () = Trans.register_env_transform "discriminate" discriminate