pgm_module.ml 5.75 KB
Newer Older
1 2 3 4 5 6 7 8

open Why
open Util
open Ident
open Theory
open Term

open Pgm_types
9
open Pgm_types.T
10 11 12 13 14
open Pgm_ttree

type namespace = {
  ns_pr : psymbol   Mnm.t;  (* program symbols *)
  ns_ex : esymbol   Mnm.t;  (* exceptions*)
15
  ns_mt : mtsymbol  Mnm.t;  (* mutable types *)
16
  ns_rt : rtsymbol  Mnm.t;  (* record types *)
17 18 19 20 21 22
  ns_ns : namespace Mnm.t;  (* inner namespaces *)
}

let empty_ns = {
  ns_pr = Mnm.empty;
  ns_ex = Mnm.empty;
23
  ns_mt = Mnm.empty;
24
  ns_rt = Mnm.empty;
25 26 27 28 29 30 31 32 33 34 35 36 37 38 39
  ns_ns = Mnm.empty;
}

exception ClashSymbol of string

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 =
  Mnm.union (fun x vn vo -> Some (ns_replace eq chk x vo vn))

let rec merge_ns chk ns1 ns2 =
  let fusion _ ns1 ns2 = Some (merge_ns chk ns1 ns2) in
40
  { ns_pr = ns_union p_equal  chk ns1.ns_pr ns2.ns_pr;
41
    ns_ex = ns_union ls_equal chk ns1.ns_ex ns2.ns_ex;
42
    ns_mt = ns_union mt_equal chk ns1.ns_mt ns2.ns_mt;
43
    ns_rt = ns_union rt_equal chk ns1.ns_rt ns2.ns_rt;
44 45 46 47 48 49 50 51 52 53
    ns_ns = Mnm.union fusion      ns1.ns_ns ns2.ns_ns; }

let nm_add chk x ns m = Mnm.change x (function
  | None -> Some ns
  | Some os -> Some (merge_ns chk ns os)) m

let ns_add eq chk x v m = Mnm.change x (function
  | None -> Some v
  | Some vo -> Some (ns_replace eq chk x vo v)) m

54
let pr_add = ns_add p_equal
55
let ex_add = ns_add ls_equal
56
let mt_add = ns_add mt_equal
57
let rt_add = ns_add rt_equal
58 59 60

let add_pr chk x ts ns = { ns with ns_pr = pr_add chk x ts ns.ns_pr }
let add_ex chk x ls ns = { ns with ns_ex = ex_add chk x ls ns.ns_ex }
61
let add_mt chk x mt ns = { ns with ns_mt = mt_add chk x mt ns.ns_mt }
62
let add_rt chk x rt ns = { ns with ns_rt = rt_add chk x rt ns.ns_rt }
63 64 65 66 67 68 69 70 71
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]  -> Mnm.find a (get_map ns)
  | a::l -> ns_find get_map (Mnm.find a ns.ns_ns) l

let ns_find_pr = ns_find (fun ns -> ns.ns_pr)
let ns_find_ex = ns_find (fun ns -> ns.ns_ex)
72
let ns_find_mt = ns_find (fun ns -> ns.ns_mt)
73
let ns_find_rt = ns_find (fun ns -> ns.ns_rt)
74 75 76 77 78 79 80 81 82 83 84 85
let ns_find_ns = ns_find (fun ns -> ns.ns_ns)

(* modules under construction *)

type uc = {
  uc_name   : Ident.ident;
  uc_th     : theory_uc; (* the logic theory used to type annotations *)
  uc_decls  : decl list; (* the program declarations *)
  uc_import : namespace list;
  uc_export : namespace list;
}

86 87 88
let namespace uc = List.hd uc.uc_import
let theory_uc uc = uc.uc_th

89 90 91 92 93 94 95
let add_pervasives uc =
  (* type unit = () *)
  let ts = 
    Ty.create_tysymbol (id_fresh "unit") [] (Some (Ty.ty_app (Ty.ts_tuple 0) []))
  in
  add_ty_decl uc [ts, Decl.Tabstract]

96 97
let open_namespace uc = match uc.uc_import with
  | ns :: _ -> { uc with
98
      uc_th     = Theory.open_namespace uc.uc_th;
99 100 101 102 103 104 105 106 107 108 109 110 111
      uc_import =       ns :: uc.uc_import;
      uc_export = empty_ns :: uc.uc_export; }
  | [] -> assert false

exception NoOpenedNamespace

let close_namespace uc import s =
  match uc.uc_import, uc.uc_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
112 113
      let th = Theory.close_namespace uc.uc_th import s in
      { uc with uc_th = th; uc_import = i1 :: sti; uc_export = e1 :: ste; }
114 115 116
  | [_], [_] -> raise NoOpenedNamespace
  | _ -> assert false

117 118 119 120 121 122 123 124 125 126
(** Insertion of new declarations *)

let add_symbol add id v uc =
  match uc.uc_import, uc.uc_export with
  | i0 :: sti, e0 :: ste -> { uc with
      uc_import = add false id.id_string v i0 :: sti;
      uc_export = add true  id.id_string v e0 :: ste }
  | _ -> assert false

let add_psymbol ps uc =
127
  add_symbol add_pr ps.p_name ps uc
128 129 130 131 132 133 134 135 136 137 138

let add_esymbol ls uc =
  add_symbol add_ex ls.ls_name ls uc

let add_decl d uc =
  { uc with uc_decls = d :: uc.uc_decls }

let add_logic_decl d uc =
  let th = Typing.with_tuples Theory.add_decl uc.uc_th d in
  { uc with uc_th = th }

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
139 140 141 142 143 144 145 146
let add_mtsymbol mt uc =
  (* added in the logic as an abstract type *)
  let uc = 
    let d = Decl.create_ty_decl [mt.mt_abstr, Decl.Tabstract] in
    add_logic_decl d uc 
  in
  add_symbol add_mt mt.mt_name mt uc

147 148 149 150 151 152 153 154
let add_rtsymbol rt uc =
  (* added in the logic as an abstract type *)
  let uc = 
    let d = Decl.create_ty_decl [rt.rt_abstr, Decl.Tabstract] in
    add_logic_decl d uc 
  in
  add_symbol add_rt rt.rt_name rt uc

155 156 157 158 159 160 161 162 163 164 165
let ls_Exit = create_lsymbol (id_fresh "%Exit") [] (Some ty_exn)

let create_module n =
  let uc = Theory.create_theory n in
  let m = { 
    uc_name = id_register n;
    uc_th = uc;
    uc_decls = [];
    uc_import = [empty_ns];
    uc_export = [empty_ns]; } 
  in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
166 167
  (* pervasives *)
  let m = add_esymbol  ls_Exit    m in
168
(*
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
169 170 171
  let m = add_mtsymbol mt_ghost   m in
  let m = add_psymbol  ps_ghost   m in
  let m = add_psymbol  ps_unghost m in
172
*)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
173
  m
174

175 176
(** Modules *)

177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194
type t = {
  m_name   : Ident.ident;
  m_th     : theory;
  m_decls  : decl list;
  m_export : namespace;
}

exception CloseModule

let close_module uc = match uc.uc_export with
  | [e] ->
      { m_name = uc.uc_name;
	m_decls = List.rev uc.uc_decls;
	m_export = e;
	m_th = close_theory uc.uc_th; }
  | _ ->
      raise CloseModule

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
195 196 197 198 199 200
(** Use *)

let use_export uc m =
  match uc.uc_import, uc.uc_export with
  | i0 :: sti, e0 :: ste -> { uc with
      uc_import = merge_ns false m.m_export i0 :: sti;
201 202
      uc_export = merge_ns true  m.m_export e0 :: ste;
      uc_th = Theory.use_export uc.uc_th m.m_th; }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
203 204
  | _ -> assert false

205 206
let use_export_theory uc th =
  { uc with uc_th = Theory.use_export uc.uc_th th }
207

208 209
let add_logic_pdecl env ltm d uc =
  { uc with uc_th = Typing.add_decl env ltm uc.uc_th d }
210

211 212 213 214 215 216 217 218



(*
Local Variables: 
compile-command: "unset LANG; make -C ../.. testl"
End: 
*)