mlw_module.ml 9.35 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

type prgsymbol =
  | PV of pvsymbol
  | PS of psymbol
  | PL of plsymbol
49
  | PX of xsymbol
50

51 52
type namespace = {
  ns_it : itysymbol Mstr.t;  (* type symbols *)
53
  ns_ps : prgsymbol Mstr.t;  (* program symbols *)
54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70
  ns_ns : namespace Mstr.t;  (* inner namespaces *)
}

let empty_ns = {
  ns_it = Mstr.empty;
  ns_ps = Mstr.empty;
  ns_ns = Mstr.empty;
}

let ns_replace eq chk x vo vn =
  if not chk then vn else
  if eq vo vn then vo else
  raise (ClashSymbol x)

let ns_union eq chk =
  Mstr.union (fun x vn vo -> Some (ns_replace eq chk x vo vn))

71 72 73 74
let prg_equal p1 p2 = match p1,p2 with
  | PV p1, PV p2 -> pv_equal p1 p2
  | PS p1, PS p2 -> ps_equal p1 p2
  | PL p1, PL p2 -> pl_equal p1 p2
75
  | PX p1, PX p2 -> xs_equal p1 p2
76 77
  | _, _ -> false

78 79 80
let rec merge_ns chk ns1 ns2 =
  let fusion _ ns1 ns2 = Some (merge_ns chk ns1 ns2) in
  { ns_it = ns_union its_equal chk ns1.ns_it ns2.ns_it;
81 82
    ns_ps = ns_union prg_equal chk ns1.ns_ps ns2.ns_ps;
    ns_ns = Mstr.union fusion      ns1.ns_ns ns2.ns_ns; }
83

84
let nm_add chk x ns m = Mstr.change (function
85
  | None -> Some ns
86
  | Some os -> Some (merge_ns chk ns os)) x m
87

88
let ns_add eq chk x v m = Mstr.change (function
89
  | None -> Some v
90
  | Some vo -> Some (ns_replace eq chk x vo v)) x m
91 92

let it_add = ns_add its_equal
93
let ps_add = ns_add prg_equal
94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115

let add_it chk x ts ns = { ns with ns_it = it_add chk x ts ns.ns_it }
let add_ps chk x pf ns = { ns with ns_ps = ps_add chk x pf ns.ns_ps }
let add_ns chk x nn ns = { ns with ns_ns = nm_add chk x nn ns.ns_ns }

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

let ns_find_it = ns_find (fun ns -> ns.ns_it)
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 *)
116
  mod_used  : Sid.t;			(* used modules *)
117 118 119 120 121 122 123 124 125 126 127
}

(** 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;
128
  muc_used   : Sid.t;
129 130 131 132 133 134 135 136 137
}

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;
138
  muc_used   = Sid.empty;
139 140 141 142 143 144 145 146
}

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;
147 148
    mod_local  = uc.muc_local;
    mod_used   = uc.muc_used; }
149

150
let get_theory uc = uc.muc_theory
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
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 *)

let use_export uc m =
179 180 181 182 183 184 185 186 187 188
  let mth = m.mod_theory in
  let id = mth.th_name in
  let uc =
    if not (Sid.mem id uc.muc_used) then
      { uc with
          muc_known = merge_known uc.muc_known m.mod_known;
          muc_used  = Sid.add id uc.muc_used; }
    else
      uc
  in
189 190
  match uc.muc_import, uc.muc_export with
  | i0 :: sti, e0 :: ste -> { uc with
191
      muc_theory = Theory.use_export uc.muc_theory mth;
192
      muc_import = merge_ns false m.mod_export i0 :: sti;
193
      muc_export = merge_ns true  m.mod_export e0 :: ste; }
194
  | _ -> assert false
195 196 197 198 199 200 201 202 203 204 205 206 207 208

(** Logic decls *)

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

let add_decl = add_to_theory Theory.add_decl
let use_export_theory = add_to_theory Theory.use_export
let clone_export_theory uc th i =
  { uc with muc_theory = Theory.clone_export uc.muc_theory th i }
let add_meta uc m al =
  { uc with muc_theory = Theory.add_meta uc.muc_theory m al }

(** Program decls *)

209 210 211 212 213 214 215
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

216 217 218 219
let add_type uc its =
  add_symbol add_it its.its_pure.ts_name its uc

let add_data uc (its,csl) =
220 221 222
  let add_pls uc pls = add_symbol add_ps pls.pl_ls.ls_name (PL pls) uc in
  let add_proj = option_fold add_pls in
  let add_constr uc (ps,pjl) = List.fold_left add_proj (add_pls uc ps) pjl in
223
  let uc = add_symbol add_it its.its_pure.ts_name its uc in
224
  if its.its_abst then uc else List.fold_left add_constr uc csl
225

226 227 228 229 230 231 232
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

233 234 235
let add_exn uc xs =
  add_symbol add_ps xs.xs_name (PX xs) uc

236
let add_pdecl uc d =
237
  let uc = { uc with
238 239 240 241 242
    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
243 244 245 246 247
  | 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
248 249
      let projection = option_map (fun pls -> pls.pl_ls) in
      let constructor (pls,pjl) = pls.pl_ls, List.map projection pjl in
250 251 252
      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
253 254
  | PDval { val_name = lv } | PDlet { let_var = lv } ->
      add_let uc lv
255 256
  | PDrec rdl ->
      List.fold_left add_rec uc rdl
257 258
  | PDexn xs ->
      add_exn uc xs
259

260
(*
261 262 263 264 265 266 267 268 269
let add_pdecl_with_tuples uc d =
  let ids = Mid.set_diff d.pd_syms uc.muc_known in
  let ids = Mid.set_diff ids (Theory.get_known uc.muc_theory) in
  let add id s = match is_ts_tuple_id id with
    | Some n -> Sint.add n s
    | None -> s in
  let ixs = Sid.fold add ids Sint.empty in
  let add n uc = use_export_theory uc (tuple_theory n) in
  add_pdecl (Sint.fold add ixs uc) d
270
*)
271

272 273 274 275 276 277 278 279 280 281 282 283
(* 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
284
  let uc = use_export_theory uc (tuple_theory 0) in
285 286 287 288 289 290 291 292 293 294
  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

295 296 297 298
(** Clone *)

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