Une MAJ de sécurité est nécessaire sur notre version actuelle. Elle sera effectuée lundi 02/08 entre 12h30 et 13h. L'interruption de service devrait durer quelques minutes (probablement moins de 5 minutes).

mlw_module.ml 10.8 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
(*    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 Why3
open Util
open Ident
open Ty
25
open Term
26 27
open Theory
open Mlw_ty
28
open Mlw_ty.T
29 30 31 32
open Mlw_expr
open Mlw_decl

(*
33
  module =
34 35 36 37 38 39 40 41 42 43
    theory +
    namespace +
    program decls (no logic decl here)

  extraction to OCaml
    1. all types
         follow order given by theory, and retrieve program types when necessary
    2. logic decls (no types)
    3. program decls
*)
44

45 46 47 48 49
type type_symbol =
  | PT of itysymbol
  | TS of tysymbol

type prog_symbol =
50 51 52
  | PV of pvsymbol
  | PS of psymbol
  | PL of plsymbol
53 54
  | XS of xsymbol
  | LS of lsymbol
55

56
type namespace = {
57 58 59
  ns_ts : type_symbol Mstr.t;  (* type symbols *)
  ns_ps : prog_symbol Mstr.t;  (* program symbols *)
  ns_ns : namespace   Mstr.t;  (* inner namespaces *)
60 61 62
}

let empty_ns = {
63
  ns_ts = Mstr.empty;
64 65 66 67
  ns_ps = Mstr.empty;
  ns_ns = Mstr.empty;
}

68
let ns_replace sub chk x vo vn =
69
  if not chk then vn else
70
  if sub vo vn then vn else
71 72
  raise (ClashSymbol x)

73 74 75 76
let tsym_sub t1 t2 = match t1,t2 with
  | PT t1, PT t2 -> its_equal t1 t2
  | TS t1, TS t2 -> ts_equal t1 t2
  | _, _ -> false
77

78
let psym_sub p1 p2 = match p1,p2 with
79 80 81
  | PV p1, PV p2 -> pv_equal p1 p2
  | PS p1, PS p2 -> ps_equal p1 p2
  | PL p1, PL p2 -> pl_equal p1 p2
82 83 84 85
  | XS p1, XS p2 -> xs_equal p1 p2
  | LS p1, LS p2 -> ls_equal p1 p2
  (* program symbols may overshadow pure symbols *)
  | LS _, (PV _|PS _|PL _|XS _) -> true
86 87
  | _, _ -> false

88
let rec merge_ns chk ns1 ns2 =
89 90
  let join sub x n o = Some (ns_replace sub chk x o n) in
  let ns_union sub m1 m2 = Mstr.union (join sub) m1 m2 in
91
  let fusion _ ns1 ns2 = Some (merge_ns chk ns1 ns2) in
92 93 94
  { ns_ts = ns_union tsym_sub ns1.ns_ts ns2.ns_ts;
    ns_ps = ns_union psym_sub ns1.ns_ps ns2.ns_ps;
    ns_ns = Mstr.union fusion ns1.ns_ns ns2.ns_ns; }
95

96 97 98
let add_ns chk x ns m = Mstr.change (function
  | Some os -> Some (merge_ns chk ns os)
  | None    -> Some ns) x m
99

100 101 102
let ns_add sub chk x vn m = Mstr.change (function
  | Some vo -> Some (ns_replace sub chk x vo vn)
  | None    -> Some vn) x m
103

104 105 106
let add_ts chk x ts ns = { ns with ns_ts = ns_add tsym_sub chk x ts ns.ns_ts }
let add_ps chk x pf ns = { ns with ns_ps = ns_add psym_sub chk x pf ns.ns_ps }
let add_ns chk x nn ns = { ns with ns_ns = add_ns          chk x nn ns.ns_ns }
107

108 109 110 111
let rec convert_pure_ns ns =
  { ns_ts = Mstr.map (fun ts -> TS ts) ns.Theory.ns_ts;
    ns_ps = Mstr.map (fun ls -> LS ls) ns.Theory.ns_ls;
    ns_ns = Mstr.map convert_pure_ns ns.Theory.ns_ns; }
112 113 114 115 116 117

let rec ns_find get_map ns = function
  | []   -> assert false
  | [a]  -> Mstr.find a (get_map ns)
  | a::l -> ns_find get_map (Mstr.find a ns.ns_ns) l

118
let ns_find_ts = ns_find (fun ns -> ns.ns_ts)
119 120 121 122 123 124 125 126 127 128 129
let ns_find_ps = ns_find (fun ns -> ns.ns_ps)
let ns_find_ns = ns_find (fun ns -> ns.ns_ns)

(** Module *)

type modul = {
  mod_theory: theory;			(* pure theory *)
  mod_decls : pdecl list;		(* module declarations *)
  mod_export: namespace;		(* exported namespace *)
  mod_known : known_map;		(* known identifiers *)
  mod_local : Sid.t;			(* locally declared idents *)
130
  mod_used  : Sid.t;			(* used modules *)
131 132 133 134 135 136 137 138 139 140 141
}

(** Module under construction *)

type module_uc = {
  muc_theory : theory_uc;
  muc_decls  : pdecl list;
  muc_import : namespace list;
  muc_export : namespace list;
  muc_known  : known_map;
  muc_local  : Sid.t;
142
  muc_used   : Sid.t;
143 144 145 146 147 148 149 150 151
}

let empty_module n p = {
  muc_theory = create_theory ~path:p n;
  muc_decls  = [];
  muc_import = [empty_ns];
  muc_export = [empty_ns];
  muc_known  = Mid.empty;
  muc_local  = Sid.empty;
152
  muc_used   = Sid.empty;
153 154 155 156 157 158 159 160
}

let close_module uc =
  let th = close_theory uc.muc_theory in (* catches errors *)
  { mod_theory = th;
    mod_decls  = List.rev uc.muc_decls;
    mod_export = List.hd uc.muc_export;
    mod_known  = uc.muc_known;
161 162
    mod_local  = uc.muc_local;
    mod_used   = uc.muc_used; }
163

164
let get_theory uc = uc.muc_theory
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
let get_namespace uc = List.hd uc.muc_import
let get_known uc = uc.muc_known

let open_namespace uc = match uc.muc_import with
  | ns :: _ -> { uc with
      muc_theory = Theory.open_namespace uc.muc_theory;
      muc_import =       ns :: uc.muc_import;
      muc_export = empty_ns :: uc.muc_export; }
  | [] -> assert false

let close_namespace uc import s =
  let th = Theory.close_namespace uc.muc_theory import s in (* catches errors *)
  match uc.muc_import, uc.muc_export with
  | _ :: i1 :: sti, e0 :: e1 :: ste ->
      let i1 = if import then merge_ns false e0 i1 else i1 in
      let _  = if import then merge_ns true  e0 e1 else e1 in
      let i1 = match s with Some s -> add_ns false s e0 i1 | _ -> i1 in
      let e1 = match s with Some s -> add_ns true  s e0 e1 | _ -> e1 in
      { uc with
	  muc_theory = th;
	  muc_import = i1 :: sti;
	  muc_export = e1 :: ste; }
  | _ ->
      assert false

(** Use *)

192 193 194 195 196 197 198 199
let add_to_module uc th ns =
  match uc.muc_import, uc.muc_export with
  | i0 :: sti, e0 :: ste -> { uc with
      muc_theory = th;
      muc_import = merge_ns false ns i0 :: sti;
      muc_export = merge_ns true  ns e0 :: ste; }
  | _ -> assert false

200
let use_export uc m =
201 202 203
  let mth = m.mod_theory in
  let id = mth.th_name in
  let uc =
204 205 206 207 208
    if Sid.mem id uc.muc_used then uc else { uc with
      muc_known = merge_known uc.muc_known m.mod_known;
      muc_used  = Sid.add id uc.muc_used } in
  let th = Theory.use_export uc.muc_theory mth in
  add_to_module uc th m.mod_export
209 210 211 212 213

(** Logic decls *)

let add_to_theory f uc x = { uc with muc_theory = f uc.muc_theory x }

214 215 216 217 218 219 220
let add_symbol add id v uc =
  match uc.muc_import, uc.muc_export with
  | i0 :: sti, e0 :: ste -> { uc with
      muc_import = add false id.id_string v i0 :: sti;
      muc_export = add true  id.id_string v e0 :: ste }
  | _ -> assert false

221 222 223 224 225 226 227 228 229 230 231 232 233 234 235 236 237 238 239 240 241 242 243 244 245 246 247 248 249 250 251 252 253 254 255 256 257 258 259 260 261 262 263
let add_decl uc d =
  let add_ts uc ts = add_symbol add_ts ts.ts_name (TS ts) uc in
  let add_ls uc ls = add_symbol add_ps ls.ls_name (LS ls) uc in
  let add_pj uc pj = Util.option_fold add_ls uc pj in
  let add_cs uc (cs,pjl) = List.fold_left add_pj (add_ls uc cs) pjl in
  let add_data uc (ts,csl) = List.fold_left add_cs (add_ts uc ts) csl in
  let add_logic uc (ls,_) = add_ls uc ls in
  let uc = match d.Decl.d_node with
    | Decl.Dtype ts -> add_ts uc ts
    | Decl.Ddata dl -> List.fold_left add_data uc dl
    | Decl.Dparam ls -> add_ls uc ls
    | Decl.Dlogic dl -> List.fold_left add_logic uc dl
    | Decl.Dind (_,dl) -> List.fold_left add_logic uc dl
    | Decl.Dprop _ -> uc
  in
  add_to_theory Theory.add_decl uc d

let use_export_theory uc th =
  let nth = Theory.use_export uc.muc_theory th in
  let nns = convert_pure_ns th.th_export in
  add_to_module uc nth nns

let clone_export_theory uc th inst =
  let nth = Theory.clone_export uc.muc_theory th inst in
  let sm = match Theory.get_rev_decls nth with
    | { td_node = Clone (_,sm) } :: _ -> sm
    | _ -> assert false in
  let g_ts _ ts = not (Mts.mem ts inst.inst_ts) in
  let g_ls _ ls = not (Mls.mem ls inst.inst_ls) in
  let f_ts ts = TS (Mts.find_def ts ts sm.sm_ts) in
  let f_ls ls = LS (Mls.find_def ls ls sm.sm_ls) in
  let rec f_ns ns = {
    ns_ts = Mstr.map f_ts (Mstr.filter g_ts ns.Theory.ns_ts);
    ns_ps = Mstr.map f_ls (Mstr.filter g_ls ns.Theory.ns_ls);
    ns_ns = Mstr.map f_ns ns.Theory.ns_ns; }
  in
  add_to_module uc nth (f_ns th.th_export)

let add_meta uc m al =
  { uc with muc_theory = Theory.add_meta uc.muc_theory m al }

(** Program decls *)

264
let add_type uc its =
265
  add_symbol add_ts its.its_pure.ts_name (PT its) uc
266 267

let add_data uc (its,csl) =
268 269 270 271 272
  let add_pl uc pl = add_symbol add_ps pl.pl_ls.ls_name (PL pl) uc in
  let add_pj uc pj = Util.option_fold add_pl uc pj in
  let add_cs uc (cs,pjl) = List.fold_left add_pj (add_pl uc cs) pjl in
  let uc = add_symbol add_ts its.its_pure.ts_name (PT its) uc in
  if its.its_abst then uc else List.fold_left add_cs uc csl
273

274 275 276 277 278 279 280
let add_let uc = function
  | LetV pv -> add_symbol add_ps pv.pv_vs.vs_name (PV pv) uc
  | LetA ps -> add_symbol add_ps ps.ps_name (PS ps) uc

let add_rec uc { rec_ps = ps } =
  add_symbol add_ps ps.ps_name (PS ps) uc

281
let add_exn uc xs =
282
  add_symbol add_ps xs.xs_name (XS xs) uc
283

284
let add_pdecl uc d =
285
  let uc = { uc with
286 287 288 289 290
    muc_decls = d :: uc.muc_decls;
    muc_known = known_add_decl (Theory.get_known uc.muc_theory) uc.muc_known d;
    muc_local = Sid.union uc.muc_local d.pd_news }
  in
  match d.pd_node with
291 292 293 294 295
  | PDtype its ->
      let uc = add_type uc its in
      add_to_theory Theory.add_ty_decl uc its.its_pure
  | PDdata dl ->
      let uc = List.fold_left add_data uc dl in
296 297
      let projection = option_map (fun pls -> pls.pl_ls) in
      let constructor (pls,pjl) = pls.pl_ls, List.map projection pjl in
298 299 300
      let defn cl = List.map constructor cl in
      let dl = List.map (fun (its,cl) -> its.its_pure, defn cl) dl in
      add_to_theory Theory.add_data_decl uc dl
301 302
  | PDval { val_name = lv } | PDlet { let_var = lv } ->
      add_let uc lv
303 304
  | PDrec rdl ->
      List.fold_left add_rec uc rdl
305 306
  | PDexn xs ->
      add_exn uc xs
307

308 309 310 311 312 313 314 315 316 317 318 319
(* create module *)

let th_unit =
  let ts = create_tysymbol (id_fresh "unit") [] (Some ty_unit) in
  let uc = create_theory (id_fresh "Unit") in
  let uc = Theory.use_export uc (tuple_theory 0) in
  let uc = Theory.add_ty_decl uc ts in
  close_theory uc

let mod_exit =
  let xs = create_xsymbol (id_fresh "%Exit") ity_unit in
  let uc = empty_module (id_fresh "Exit") [] in
320
  let uc = use_export_theory uc (tuple_theory 0) in
321 322 323 324 325 326 327 328 329 330
  let uc = add_pdecl uc (create_exn_decl xs) in
  close_module uc

let create_module ?(path=[]) n =
  let m = empty_module n path in
  let m = use_export_theory m bool_theory in
  let m = use_export_theory m th_unit in
  let m = use_export m mod_exit in
  m

331 332 333 334
(** Clone *)

let clone_export _uc _m _inst =
  assert false (*TODO*)