Attention une mise à jour du serveur va être effectuée le vendredi 16 avril entre 12h et 12h30. Cette mise à jour va générer une interruption du service de quelques minutes.

pdriver.ml 9.67 KB
Newer Older
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
(*  Copyright 2010-2016   --   INRIA - CNRS - Paris-Sud University  *)
(*                                                                  *)
(*  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.                           *)
(*                                                                  *)
(********************************************************************)

open Ident
open Ty
open Term
open Theory
open Driver_ast

MARCHE Claude's avatar
MARCHE Claude committed
18 19 20 21
let debug =
  Debug.register_info_flag "extraction"
    ~desc:"Print@ details@ of@ program@ extraction."

22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 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
type driver = {
  drv_env         : Env.env;
  drv_printer     : string option;
  drv_prelude     : Printer.prelude;
  drv_thprelude   : Printer.prelude_map;
  drv_blacklist   : Printer.blacklist;
  drv_syntax      : Printer.syntax_map;
  drv_converter   : Printer.syntax_map;
}

type printer_args = {
  env         : Env.env;
  prelude     : Printer.prelude;
  thprelude   : Printer.prelude_map;
  blacklist   : Printer.blacklist;
  syntax      : Printer.syntax_map;
  converter   : Printer.syntax_map;
}

let load_file file =
  let c = open_in file in
  let lb = Lexing.from_channel c in
  Loc.set_file file lb;
  let to_close = Stack.create () in
  Stack.push c to_close;
  let input_lexer filename =
    let c = open_in filename in
    Stack.push c to_close;
    let lb = Lexing.from_channel c in
    Loc.set_file filename lb;
    lb
  in
  let f = Driver_lexer.parse_file_extract input_lexer lb in
  Stack.iter close_in to_close;
  f

exception Duplicate    of string
exception UnknownType  of (string list * string list)
exception UnknownLogic of (string list * string list)
exception UnknownProp  of (string list * string list)
exception UnknownVal   of (string list * string list)
exception UnknownExn   of (string list * string list)
exception FSymExpected of lsymbol
exception PSymExpected of lsymbol

let load_driver env file extra_files =
  let prelude   = ref [] in
  let printer   = ref None in
  let blacklist = Queue.create () in

  let set_or_raise loc r v error = match !r with
    | Some _ -> raise (Loc.Located (loc, Duplicate error))
    | None   -> r := Some v
  in
  let add_to_list r v = (r := v :: !r) in
  let add_global (loc, g) = match g with
    | EPrelude s -> add_to_list prelude s
    | EPrinter s -> set_or_raise loc printer s "printer"
    | EBlacklist sl -> List.iter (fun s -> Queue.add s blacklist) sl
  in
  let f = load_file file in
  List.iter add_global f.fe_global;

  let thprelude = ref Mid.empty in
  let syntax_map = ref Mid.empty in
  let converter_map = ref Mid.empty in
  let qualid    = ref [] in

  let find_pr th (loc,q) = try Theory.ns_find_pr th.th_export q
    with Not_found -> raise (Loc.Located (loc, UnknownProp (!qualid,q)))
  in
  let find_ls th (loc,q) = try Theory.ns_find_ls th.th_export q
    with Not_found -> raise (Loc.Located (loc, UnknownLogic (!qualid,q)))
  in
  let find_ts th (loc,q) = try Theory.ns_find_ts th.th_export q
    with Not_found -> raise (Loc.Located (loc, UnknownType (!qualid,q)))
  in
  let find_fs th q =
    let ls = find_ls th q in
    if ls.ls_value = None then raise (FSymExpected ls) else ls in
  let find_ps th q =
    let ls = find_ls th q in
    if ls.ls_value <> None then raise (PSymExpected ls) else ls in
  let add_syntax id s b =
    syntax_map := Mid.add id (s,if b then 1 else 0) !syntax_map in
  let add_converter id s b =
    converter_map := Mid.add id (s,if b then 1 else 0) !converter_map in
  let add_local th = function
    | Rprelude s ->
        let l = Mid.find_def [] th.th_name !thprelude in
        thprelude := Mid.add th.th_name (s::l) !thprelude
    | Rsyntaxts (q,s,b) ->
        let ts = find_ts th q in
        Printer.check_syntax_type ts s;
        add_syntax ts.ts_name s b
    | Rsyntaxfs (q,s,b) ->
        let fs = find_fs th q in
        Printer.check_syntax_logic fs s;
        add_syntax fs.ls_name s b
    | Rsyntaxps (q,s,b) ->
        let ps = find_ps th q in
        Printer.check_syntax_logic ps s;
        add_syntax ps.ls_name s b
    | Rconverter _ ->
        Loc.errorm "Syntax converter cannot be used in pure theories"
    | Rremovepr (q) ->
      ignore (find_pr th q)
    | Rremoveall ->
      let it key _ = match (Mid.find key th.th_known).Decl.d_node with
        | Decl.Dprop (_,symb,_) -> ignore symb
        | _ -> ()
      in
      Mid.iter it th.th_local
    | Rmeta (s,al) ->
        let rec ty_of_pty = function
          | PTyvar x ->
              Ty.ty_var (Ty.tv_of_string x)
          | PTyapp ((loc,_) as q,tyl) ->
              let ts = find_ts th q in
              let tyl = List.map ty_of_pty tyl in
              Loc.try2 ~loc Ty.ty_app ts tyl
          | PTuple tyl ->
              let ts = Ty.ts_tuple (List.length tyl) in
              Ty.ty_app ts (List.map ty_of_pty tyl)
        in
        let convert = function
          | PMAty (PTyapp (q,[]))
                     -> MAts (find_ts th q)
          | PMAty ty -> MAty (ty_of_pty ty)
          | PMAfs q  -> MAls (find_fs th q)
          | PMAps q  -> MAls (find_ps th q)
          | PMApr q  -> MApr (find_pr th q)
          | PMAstr s -> MAstr s
          | PMAint i -> MAint i
        in
        let m = lookup_meta s in
        ignore (create_meta m (List.map convert al))
  in
  let add_local th (loc,rule) = Loc.try2 ~loc add_local th rule in
  let open Pmodule in
  let find_val m (loc,q) =
    try match ns_find_prog_symbol m.mod_export q with
    | PV pv -> pv.Ity.pv_vs.vs_name
    | RS rs -> rs.Expr.rs_name
    with Not_found -> raise (Loc.Located (loc, UnknownVal (!qualid,q)))
  in
  let find_xs m (loc,q) =
    try ns_find_xs m.mod_export q
    with Not_found -> raise (Loc.Located (loc, UnknownExn (!qualid,q)))
  in
  let add_local_module loc m = function
    | MRexception (q,s) ->
        let xs = find_xs m q in
        add_syntax xs.Ity.xs_name s false
    | MRval (q,s) ->
        let id = find_val m q in
        add_syntax id s false
    | MRtheory (Rconverter (q,s,b)) ->
        let id = find_val m q in
        add_converter id s b
    | MRtheory trule ->
        add_local m.mod_theory (loc,trule)
  in
  let add_local_module m (loc,rule) =
    Loc.try3 ~loc add_local_module loc m rule
  in
  let add_theory { thr_name = (loc,q); thr_rules = trl } =
    let f,id = let l = List.rev q in List.rev (List.tl l),List.hd l in
    let th = Loc.try3 ~loc Env.read_theory env f id in
    qualid := q;
    List.iter (add_local th) trl
  in
  let add_module { mor_name = (loc,q); mor_rules = mrl } =
    let f,id = let l = List.rev q in List.rev (List.tl l),List.hd l in
    let m = Loc.try3 ~loc read_module env f id in
    qualid := q;
    List.iter (add_local_module m) mrl
  in
  List.iter add_theory f.fe_th_rules;
  List.iter add_module f.fe_mo_rules;
  List.iter (fun f ->
    let fe = load_file f in
    List.iter add_theory fe.fe_th_rules;
    List.iter add_module fe.fe_mo_rules)
    extra_files;
  {
    drv_env         = env;
    drv_printer     = !printer;
    drv_prelude     = List.rev !prelude;
    drv_thprelude   = Mid.map List.rev !thprelude;
    drv_blacklist   = Queue.fold (fun l s -> s :: l) [] blacklist;
    drv_syntax      = !syntax_map;
    drv_converter   = !converter_map;
  }

(* registering printers for programs *)

open Stdlib

221 222
type filename_generator = ?fname:string -> Pmodule.pmodule -> string

Mário Pereira's avatar
Mário Pereira committed
223
type printer = printer_args -> ?old:in_channel -> ?fname:string -> Pmodule.pmodule Pp.pp
224

225
type reg_printer = Pp.formatted * filename_generator * printer
226 227 228 229 230 231 232

let printers : reg_printer Hstr.t = Hstr.create 17

exception KnownPrinter of string
exception UnknownPrinter of string
exception NoPrinter

233
let register_printer ~desc s fg p =
234
  if Hstr.mem printers s then raise (KnownPrinter s);
235
  Hstr.replace printers s (desc, fg, p)
236

237
let lookup_printer drv =
238 239 240 241 242 243 244 245 246 247 248
  let p = match drv.drv_printer with
    | None -> raise NoPrinter
    | Some p -> p
  in
  let printer_args = {
      env         = drv.drv_env;
      prelude     = drv.drv_prelude;
      thprelude   = drv.drv_thprelude;
      blacklist   = drv.drv_blacklist;
      syntax      = drv.drv_syntax;
      converter   = drv.drv_converter;
249 250 251 252 253 254 255 256 257 258 259
    }
  in
  try
    let (_,fg,p) = Hstr.find printers p in (fg,printer_args,p)
  with Not_found -> raise (UnknownPrinter p)

let list_printers () =
  Hstr.fold (fun k (desc,_,_) acc -> (k,desc)::acc) printers []

(*
let extract_module ?old drv fmt m =
260 261
  let printer = lookup_printer p printer_args in
  Format.fprintf fmt "@[%a@]@?" (printer ?old) m
262
 *)
263 264 265 266 267 268 269 270 271 272 273 274 275 276 277 278 279 280 281 282 283 284 285 286 287 288 289 290 291 292

(* exception report *)

let string_of_qualid thl idl =
  String.concat "." thl ^ "." ^ String.concat "." idl

let () = Exn_printer.register (fun fmt exn ->
  let open Format in
  match exn with
  | Duplicate s -> fprintf fmt
      "Duplicate %s specification" s
  | UnknownType (thl,idl) -> fprintf fmt
      "Unknown type symbol %s" (string_of_qualid thl idl)
  | UnknownLogic (thl,idl) -> fprintf fmt
      "Unknown logical symbol %s" (string_of_qualid thl idl)
  | UnknownProp (thl,idl) -> fprintf fmt
      "Unknown proposition %s" (string_of_qualid thl idl)
  | UnknownVal (thl,idl) -> fprintf fmt
      "Unknown val %s" (string_of_qualid thl idl)
  | UnknownExn (thl,idl) -> fprintf fmt
      "Unknown exception %s" (string_of_qualid thl idl)
  | FSymExpected ls -> fprintf fmt
      "%a is not a function symbol" Pretty.print_ls ls
  | PSymExpected ls -> fprintf fmt
      "%a is not a predicate symbol" Pretty.print_ls ls
  | KnownPrinter s ->
      fprintf fmt "Program printer '%s' is already registered" s
  | UnknownPrinter s ->
      fprintf fmt "Unknown program printer '%s'" s
  | e -> raise e)