pgm_module.ml 5.01 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 17 18 19 20 21
  ns_ns : namespace Mnm.t;  (* inner namespaces *)
}

let empty_ns = {
  ns_pr = Mnm.empty;
  ns_ex = Mnm.empty;
22
  ns_mt = Mnm.empty;
23 24 25 26 27 28 29 30 31 32 33 34 35 36 37
  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
38
  { ns_pr = ns_union p_equal  chk ns1.ns_pr ns2.ns_pr;
39
    ns_ex = ns_union ls_equal chk ns1.ns_ex ns2.ns_ex;
40
    ns_mt = ns_union mt_equal chk ns1.ns_mt ns2.ns_mt;
41 42 43 44 45 46 47 48 49 50
    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

51
let pr_add = ns_add p_equal
52
let ex_add = ns_add ls_equal
53
let mt_add = ns_add mt_equal
54 55 56

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 }
57
let add_mt chk x mt ns = { ns with ns_mt = mt_add chk x mt ns.ns_mt }
58 59 60 61 62 63 64 65 66
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)
67
let ns_find_mt = ns_find (fun ns -> ns.ns_mt)
68 69 70 71 72 73 74 75 76 77 78 79
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;
}

80 81 82
let namespace uc = List.hd uc.uc_import
let theory_uc uc = uc.uc_th

83 84 85 86 87 88 89
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]

90 91
let open_namespace uc = match uc.uc_import with
  | ns :: _ -> { uc with
92
      uc_th     = Theory.open_namespace uc.uc_th;
93 94 95 96 97 98 99 100 101 102 103 104 105
      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
106 107
      let th = Theory.close_namespace uc.uc_th import s in
      { uc with uc_th = th; uc_import = i1 :: sti; uc_export = e1 :: ste; }
108 109 110
  | [_], [_] -> raise NoOpenedNamespace
  | _ -> assert false

111 112 113 114 115 116 117 118 119 120
(** 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 =
121
  add_symbol add_pr ps.p_name ps uc
122 123 124 125

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

126 127 128
let add_mtsymbol mt uc =
  add_symbol add_mt mt.mt_name mt uc

129 130 131 132 133 134 135
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 }

136 137 138 139 140 141 142 143 144 145 146 147 148 149
let ls_Exit = create_lsymbol (id_fresh "%Exit") [] (Some ty_exn)

let create_module n =
  let uc = Theory.create_theory n in
  (* let uc = add_pervasives uc in *)
  let m = { 
    uc_name = id_register n;
    uc_th = uc;
    uc_decls = [];
    uc_import = [empty_ns];
    uc_export = [empty_ns]; } 
  in
  add_esymbol ls_Exit m

150 151
(** Modules *)

152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169
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
170 171 172 173 174 175
(** 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;
176 177
      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
178 179
  | _ -> assert false

180 181
let use_export_theory uc th =
  { uc with uc_th = Theory.use_export uc.uc_th th }
182

183 184
let add_logic_pdecl env ltm d uc =
  { uc with uc_th = Typing.add_decl env ltm uc.uc_th d }
185

186 187 188 189 190 191 192 193



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