theory.ml 16 KB
Newer Older
Jean-Christophe Filliâtre's avatar
headers  
Jean-Christophe Filliâtre committed
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18
(**************************************************************************)
(*                                                                        *)
(*  Copyright (C) 2010-                                                   *)
(*    Francois Bobot                                                      *)
(*    Jean-Christophe Filliatre                                           *)
(*    Johannes Kanig                                                      *)
(*    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.                  *)
(*                                                                        *)
(**************************************************************************)
19 20 21

open Format
open Pp
22
open Util
23
open Ident
24
open Ty
25 26
open Term

27
(** Declarations *)
28

29
(* type declaration *)
30

31 32
type ty_def =
  | Tabstract
33
  | Talgebraic of lsymbol list
34

35
type ty_decl = tysymbol * ty_def
36

37
(* logic declaration *)
38

39 40
type fs_defn = lsymbol * vsymbol list * term * fmla
type ps_defn = lsymbol * vsymbol list * fmla * fmla
41

42
type logic_decl =
43 44 45
  | Lfunction  of lsymbol * fs_defn option
  | Lpredicate of lsymbol * ps_defn option
  | Linductive of lsymbol * (ident * fmla) list
46

47 48 49 50 51 52 53 54 55 56
(* proposition declaration *)

type prop_kind =
  | Paxiom
  | Plemma
  | Pgoal

type prop_decl = prop_kind * ident * fmla

(* declaration *)
57

58
type decl_node =
59 60
  | Dtype  of ty_decl list
  | Dlogic of logic_decl list
61
  | Dprop  of prop_decl
62

63 64 65 66
type decl = {
  d_node : decl_node;
  d_tag  : int;
}
67

68 69 70 71 72 73 74 75 76 77 78 79
module D = struct

  type t = decl

  let for_all2 pr l1 l2 =
    try List.for_all2 pr l1 l2 with Invalid_argument _ -> false

  let eq_td (ts1,td1) (ts2,td2) = ts1 == ts2 && match td1,td2 with
    | Tabstract, Tabstract -> true
    | Talgebraic l1, Talgebraic l2 -> for_all2 (==) l1 l2
    | _ -> false

80
  let eq_fd fs1 fd1 fs2 fd2 = fs1 == fs2 && match fd1,fd2 with
81
    | Some (_,_,_,fd1), Some (_,_,_,fd2) -> fd1 == fd2
82 83 84 85
    | None, None -> true
    | _ -> false

  let eq_ld ld1 ld2 = match ld1,ld2 with
86 87 88 89
    | Lfunction  (fs1,fd1), Lfunction  (fs2,fd2) -> eq_fd fs1 fd1 fs2 fd2
    | Lpredicate (ps1,pd1), Lpredicate (ps2,pd2) -> eq_fd ps1 pd1 ps2 pd2
    | Linductive (ps1,al1), Linductive (ps2,al2) -> ps1 == ps2 &&
        for_all2 (fun (i1,f1) (i2,f2) -> i1 == i2 && f1 == f2) al1 al2
90 91 92 93 94 95 96 97 98 99 100
    | _ -> false

  let equal d1 d2 = match d1.d_node, d2.d_node with
    | Dtype  l1, Dtype  l2 -> for_all2 eq_td l1 l2
    | Dlogic l1, Dlogic l2 -> for_all2 eq_ld l1 l2
    | Dprop (k1,i1,f1), Dprop (k2,i2,f2) -> k1 == k2 && i1 == i2 && f1 == f2
    | _ -> false

  let hs_td (ts,td) = match td with
    | Tabstract -> ts.ts_name.id_tag
    | Talgebraic l ->
101
        let tag fs = fs.ls_name.id_tag in
102 103
        1 + Hashcons.combine_list tag ts.ts_name.id_tag l

104
  let hs_fd fd = Hashcons.combine_option (fun (_,_,_,f) -> f.f_tag) fd
105

106
  let hs_ld ld = match ld with
107 108
    | Lfunction  (fs,fd) -> Hashcons.combine fs.ls_name.id_tag (hs_fd fd)
    | Lpredicate (ps,pd) -> Hashcons.combine ps.ls_name.id_tag (hs_fd pd)
109 110
    | Linductive (ps,l)  ->
        let hs_pair (i,f) = Hashcons.combine i.id_tag f.f_tag in
111
        Hashcons.combine_list hs_pair ps.ls_name.id_tag l
112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127

  let hash d = match d.d_node with
    | Dtype  l -> Hashcons.combine_list hs_td 0 l
    | Dlogic l -> Hashcons.combine_list hs_ld 1 l
    | Dprop (Paxiom,i,f) -> Hashcons.combine2 0 i.id_tag f.f_tag
    | Dprop (Plemma,i,f) -> Hashcons.combine2 1 i.id_tag f.f_tag
    | Dprop (Pgoal, i,f) -> Hashcons.combine2 2 i.id_tag f.f_tag

  let tag n d = { d with d_tag = n }

  let compare d1 d2 = Pervasives.compare d1.d_tag d2.d_tag

end
module Hdecl = Hashcons.Make(D)
module Mdecl = Map.Make(D)
module Sdecl = Set.Make(D)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
128

129 130 131 132 133 134 135 136
(* smart constructors *)

let mk_decl n = { d_node = n; d_tag = -1 }

let create_type tdl = Hdecl.hashcons (mk_decl (Dtype tdl))
let create_logic ldl = Hdecl.hashcons (mk_decl (Dlogic ldl))
let create_prop k i f = Hdecl.hashcons (mk_decl (Dprop (k, id_register i, f)))

137
(* error reporting *)
138

139
exception ConstructorExpected of lsymbol
140 141
exception IllegalTypeAlias of tysymbol
exception UnboundTypeVar of ident
142

143
exception IllegalConstructor of lsymbol
144
exception UnboundVars of Svs.t
Andrei Paskevich's avatar
minor  
Andrei Paskevich committed
145
exception BadDecl of ident
146

147 148 149 150 151
let check_fvs f =
  let fvs = f_freevars Svs.empty f in
  if Svs.is_empty fvs then f else raise (UnboundVars fvs)

let make_fs_defn fs vl t =
152
  if fs.ls_constr then raise (IllegalConstructor fs);
153
  let hd = t_app fs (List.map t_var vl) t.t_ty in
154 155
  let fd = f_forall vl [] (f_equ hd t) in
  fs, vl, t, check_fvs fd
156

157
let make_ps_defn ps vl f =
158
  let hd = f_app ps (List.map t_var vl) in
159 160 161 162 163 164 165 166
  let pd = f_forall vl [] (f_iff hd f) in
  ps, vl, f, check_fvs pd

let open_fs_defn (fs,vl,t,_) = (fs,vl,t)
let open_ps_defn (ps,vl,f,_) = (ps,vl,f)

let fs_defn_axiom (_,_,_,fd) = fd
let ps_defn_axiom (_,_,_,pd) = pd
167

168 169
let create_type tdl =
  let check_constructor ty fs =
170 171 172
    if not fs.ls_constr then raise (ConstructorExpected fs);
    let vty = of_option fs.ls_value in
    ignore (Ty.matching Mid.empty vty ty);
173 174 175 176
    let add s ty = match ty.ty_node with
      | Tyvar v -> Sid.add v s
      | _ -> assert false
    in
177
    let vs = ty_fold add Sid.empty vty in
178
    let rec check () ty = match ty.ty_node with
179
      | Tyvar v -> if not (Sid.mem v vs) then raise (UnboundTypeVar v)
180 181
      | _ -> ty_fold check () ty
    in
182
    List.iter (check ()) fs.ls_args
183 184 185 186
  in
  let check_decl (ts,td) = match td with
    | Tabstract -> ()
    | Talgebraic fsl ->
187
        if ts.ts_def != None then raise (IllegalTypeAlias ts);
188 189 190 191 192 193 194 195
        let ty = ty_app ts (List.map ty_var ts.ts_args) in
        List.iter (check_constructor ty) fsl
  in
  List.iter check_decl tdl;
  create_type tdl

let create_logic ldl =
  let check_decl = function
Andrei Paskevich's avatar
minor  
Andrei Paskevich committed
196
    | Lfunction (fs, Some (s,_,_,_)) when s != fs ->
197
        raise (BadDecl fs.ls_name)
Andrei Paskevich's avatar
minor  
Andrei Paskevich committed
198
    | Lpredicate (ps, Some (s,_,_,_)) when s != ps ->
199
        raise (BadDecl ps.ls_name)
200
    | Linductive (ps,la) ->
201 202 203 204
        let check_ax (_,f) =
          ignore (check_fvs f);
          assert false (* TODO *)
        in
205
        List.iter check_ax la
206 207 208 209 210 211 212
    | _ -> ()
  in
  List.iter check_decl ldl;
  create_logic ldl

let create_prop k i f =
  let fvs = f_freevars Svs.empty f in
213
  if not (Svs.is_empty fvs) then raise (UnboundVars fvs);
214 215
  create_prop k i f

216 217 218 219 220 221 222 223

(** Theory *)

module Snm = Set.Make(String)
module Mnm = Map.Make(String)

type theory = {
  th_name   : ident;
Andrei Paskevich's avatar
Andrei Paskevich committed
224 225
  th_param  : Sid.t;        (* locally declared abstract symbols *)
  th_known  : ident Mid.t;  (* imported and locally declared symbols *)
226 227
  th_export : namespace;
  th_decls  : decl_or_use list;
228 229 230
}

and namespace = {
Andrei Paskevich's avatar
Andrei Paskevich committed
231
  ns_ts : tysymbol Mnm.t;   (* type symbols *)
232
  ns_ls : lsymbol Mnm.t;    (* logic symbols *)
Andrei Paskevich's avatar
Andrei Paskevich committed
233 234
  ns_ns : namespace Mnm.t;  (* inner namespaces *)
  ns_pr : fmla Mnm.t;       (* propositions *)
235 236
}

237 238 239 240 241
and decl_or_use =
  | Decl of decl
  | Use of theory


Andrei Paskevich's avatar
Andrei Paskevich committed
242 243 244 245 246 247 248 249 250 251 252 253
(** Theory under construction *)

type theory_uc = {
  uc_name   : ident;
  uc_param  : Sid.t;
  uc_known  : ident Mid.t;
  uc_import : namespace list;
  uc_export : namespace list;
  uc_decls  : decl_or_use list;
}


254 255 256 257 258
(** Error reporting *)

exception CloseTheory
exception NoOpenedNamespace
exception RedeclaredIdent of ident
259 260
exception UnknownIdent of ident
exception CannotInstantiate of ident
261 262
exception ClashSymbol of string

Jean-Christophe Filliâtre's avatar
egalite  
Jean-Christophe Filliâtre committed
263

Andrei Paskevich's avatar
Andrei Paskevich committed
264
(** Manage known symbols *)
Jean-Christophe Filliâtre's avatar
egalite  
Jean-Christophe Filliâtre committed
265

Andrei Paskevich's avatar
Andrei Paskevich committed
266 267
let known_id kn id =
  if not (Mid.mem id kn) then raise (UnknownIdent id)
Jean-Christophe Filliâtre's avatar
egalite  
Jean-Christophe Filliâtre committed
268

Andrei Paskevich's avatar
Andrei Paskevich committed
269
let known_ts kn () ts = known_id kn ts.ts_name
270
let known_ls kn () ls = known_id kn ls.ls_name
271

Andrei Paskevich's avatar
Andrei Paskevich committed
272
let known_ty kn ty = ty_s_fold (known_ts kn) () ty
273 274
let known_term kn t = t_s_fold (known_ts kn) (known_ls kn) () t
let known_fmla kn f = f_s_fold (known_ts kn) (known_ls kn) () f
Andrei Paskevich's avatar
Andrei Paskevich committed
275 276 277 278 279 280 281 282 283

let merge_known kn1 kn2 =
  let add id tid kn =
    try
      if Mid.find id kn2 != tid then raise (RedeclaredIdent id);
      kn
    with Not_found -> Mid.add id tid kn
  in
  Mid.fold add kn1 kn2
284

Andrei Paskevich's avatar
Andrei Paskevich committed
285 286 287 288 289 290
let add_known id uc =
  if Mid.mem id uc.uc_known then raise (RedeclaredIdent id);
  { uc with uc_known = Mid.add id uc.uc_name uc.uc_known }


(** Manage namespaces *)
291 292

let empty_ns = {
Andrei Paskevich's avatar
Andrei Paskevich committed
293
  ns_ts = Mnm.empty;
294
  ns_ls = Mnm.empty;
Andrei Paskevich's avatar
Andrei Paskevich committed
295 296
  ns_ns = Mnm.empty;
  ns_pr = Mnm.empty;
297 298
}

Andrei Paskevich's avatar
Andrei Paskevich committed
299 300 301 302 303 304
let add_to_ns x v m =
  if Mnm.mem x m then raise (ClashSymbol x);
  Mnm.add x v m

let merge_ns ns1 ns2 =
  { ns_ts = Mnm.fold add_to_ns ns1.ns_ts ns2.ns_ts;
305
    ns_ls = Mnm.fold add_to_ns ns1.ns_ls ns2.ns_ls;
Andrei Paskevich's avatar
Andrei Paskevich committed
306 307 308 309
    ns_ns = Mnm.fold add_to_ns ns1.ns_ns ns2.ns_ns;
    ns_pr = Mnm.fold add_to_ns ns1.ns_pr ns2.ns_pr; }

let add_ts x ts ns = { ns with ns_ts = add_to_ns x ts ns.ns_ts }
310
let add_ls x fs ns = { ns with ns_ls = add_to_ns x fs ns.ns_ls }
Andrei Paskevich's avatar
Andrei Paskevich committed
311 312 313 314 315 316 317 318 319 320 321 322 323 324 325
let add_pr x f  ns = { ns with ns_pr = add_to_ns x f  ns.ns_pr }

let add_symbol add id v uc =
  let uc = add_known id uc in
  match uc.uc_import, uc.uc_export with
  | i0 :: sti, e0 :: ste ->
      let im = add id.id_short v i0 :: sti in
      let ex = add id.id_short v e0 :: ste in
      { uc with uc_import = im; uc_export = ex }
  | _ ->
      assert false

let get_namespace uc = List.hd uc.uc_import


326
(** Built-in symbols *)
Andrei Paskevich's avatar
Andrei Paskevich committed
327

328
let builtin_ts = [ts_int; ts_real]
329
let builtin_ls = [ps_equ; ps_neq]
330 331

let ts_name x = x.ts_name
332
let ls_name x = x.ls_name
Andrei Paskevich's avatar
Andrei Paskevich committed
333

334 335
let builtin_ns =
  let add adder name = List.fold_right (fun s -> adder (name s).id_short s) in
336
  let ns = add add_ts ts_name builtin_ts empty_ns in
337
  let ns = add add_ls ls_name builtin_ls ns in
338
  ns
339

340
let builtin_th = id_register (id_fresh "Builtin")
Andrei Paskevich's avatar
Andrei Paskevich committed
341

342
let builtin_known =
343 344
  let add name = List.fold_right (fun s -> Mid.add (name s) builtin_th) in
  let kn = Mid.add builtin_th builtin_th Mid.empty in
345
  let kn = add ts_name builtin_ts kn in
346
  let kn = add ls_name builtin_ls kn in
347
  kn
Andrei Paskevich's avatar
Andrei Paskevich committed
348 349 350 351


(** Manage theories *)

352
let create_theory n = {
Andrei Paskevich's avatar
Andrei Paskevich committed
353 354
  uc_name   = n;
  uc_param  = Sid.empty;
355 356
  uc_known  = Mid.add n n builtin_known;
  uc_import = [builtin_ns];
Andrei Paskevich's avatar
Andrei Paskevich committed
357 358
  uc_export = [empty_ns];
  uc_decls  = [];
359
}
360 361 362 363 364 365 366 367

let create_theory n = create_theory (id_register n)

let close_theory uc = match uc.uc_export with
  | [e] ->
      { th_name   = uc.uc_name;
        th_param  = uc.uc_param;
        th_known  = uc.uc_known;
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
368
        th_export = e;
369 370
        th_decls  = List.rev uc.uc_decls; }
  | _ ->
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
371 372
      raise CloseTheory

Andrei Paskevich's avatar
Andrei Paskevich committed
373 374
let open_namespace uc = match uc.uc_import with
  | ns :: _ ->
375
      { uc with
Andrei Paskevich's avatar
Andrei Paskevich committed
376 377
          uc_import =       ns :: uc.uc_import;
          uc_export = empty_ns :: uc.uc_export; }
378
  | [] ->
379
      assert false
380

381
let close_namespace uc s ~import =
Andrei Paskevich's avatar
Andrei Paskevich committed
382 383
  match uc.uc_import, uc.uc_export with
  | _ :: i1 :: sti, e0 :: e1 :: ste ->
384
      if Mnm.mem s i1.ns_ns then raise (ClashSymbol s);
Andrei Paskevich's avatar
Andrei Paskevich committed
385
      let i1 = if import then merge_ns e0 i1 else i1 in
386 387
      let i1 = { i1 with ns_ns = Mnm.add s e0 i1.ns_ns } in
      let e1 = { e1 with ns_ns = Mnm.add s e0 e1.ns_ns } in
Andrei Paskevich's avatar
Andrei Paskevich committed
388 389
      { uc with uc_import = i1 :: sti; uc_export = e1 :: ste; }
  | [_], [_] ->
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
390 391
      raise NoOpenedNamespace
  | _ ->
392
      assert false
393

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
394
let use_export uc th =
Andrei Paskevich's avatar
Andrei Paskevich committed
395 396
  match uc.uc_import, uc.uc_export with
    | i0 :: sti, e0 :: ste ->
Andrei Paskevich's avatar
Andrei Paskevich committed
397
        { uc with
Andrei Paskevich's avatar
Andrei Paskevich committed
398 399 400 401
            uc_import = merge_ns th.th_export i0 :: sti;
            uc_export = merge_ns th.th_export e0 :: ste;
            uc_known  = merge_known uc.uc_known th.th_known;
            uc_decls  = Use th :: uc.uc_decls;
Andrei Paskevich's avatar
Andrei Paskevich committed
402
        }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
403
    | _ ->
Andrei Paskevich's avatar
Andrei Paskevich committed
404
        assert false
405 406


Andrei Paskevich's avatar
Andrei Paskevich committed
407
(** Manage new declarations *)
408 409 410 411 412 413 414 415 416

let add_param id uc = { uc with uc_param = Sid.add id uc.uc_param }

let add_type uc (ts,def) =
  let uc = add_symbol add_ts ts.ts_name ts uc in
  match def with
  | Tabstract ->
      if ts.ts_def == None then add_param ts.ts_name uc else uc
  | Talgebraic lfs ->
417
      let add_constr uc fs = add_symbol add_ls fs.ls_name fs uc in
418 419 420
      List.fold_left add_constr uc lfs

let check_type kn (ts,def) = match def with
421
  | Tabstract ->
422
      begin match ts.ts_def with
Andrei Paskevich's avatar
Andrei Paskevich committed
423
        | Some ty -> known_ty kn ty
424 425 426
        | None -> ()
      end
  | Talgebraic lfs ->
427
      let check fs = List.iter (known_ty kn) fs.ls_args in
428
      List.iter check lfs
429

Jean-Christophe Filliâtre's avatar
logic  
Jean-Christophe Filliâtre committed
430
let add_logic uc = function
431
  | Lfunction (fs, df) ->
432 433
      let uc = add_symbol add_ls fs.ls_name fs uc in
      if df == None then add_param fs.ls_name uc else uc
434
  | Lpredicate (ps, dp) ->
435 436
      let uc = add_symbol add_ls ps.ls_name ps uc in
      if dp == None then add_param ps.ls_name uc else uc
437
  | Linductive (ps, la) ->
438
      let uc = add_symbol add_ls ps.ls_name ps uc in
Andrei Paskevich's avatar
Andrei Paskevich committed
439
      let add uc (id,f) = add_symbol add_pr id f uc in
440 441 442 443
      List.fold_left add uc la

let check_logic kn = function
  | Lfunction (fs, df) ->
444 445
      known_ty kn (of_option fs.ls_value);
      List.iter (known_ty kn) fs.ls_args;
446
      begin match df with
447
        | Some (_,_,t,_) -> known_term kn t
448 449
        | None -> ()
      end
450
  | Lpredicate (ps, dp) ->
451
      List.iter (known_ty kn) ps.ls_args;
452
      begin match dp with
453
        | Some (_,_,f,_) -> known_fmla kn f
454 455 456
        | None -> ()
      end
  | Linductive (ps, la) ->
457
      List.iter (known_ty kn) ps.ls_args;
Andrei Paskevich's avatar
Andrei Paskevich committed
458
      let check (_,f) = known_fmla kn f in
459
      List.iter check la
Jean-Christophe Filliâtre's avatar
logic  
Jean-Christophe Filliâtre committed
460

461 462
let add_decl uc d =
  let uc = match d.d_node with
463
    | Dtype dl ->
464 465 466
        let uc = List.fold_left add_type uc dl in
        List.iter (check_type uc.uc_known) dl;
        uc
Jean-Christophe Filliâtre's avatar
logic  
Jean-Christophe Filliâtre committed
467
    | Dlogic dl ->
468 469 470
        let uc = List.fold_left add_logic uc dl in
        List.iter (check_logic uc.uc_known) dl;
        uc
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
471
    | Dprop (k, id, f) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
472 473
        known_fmla uc.uc_known f;
        add_symbol add_pr id f uc
474
  in
475
  { uc with uc_decls = Decl d :: uc.uc_decls }
476 477


Andrei Paskevich's avatar
Andrei Paskevich committed
478 479 480 481
(** Clone theories *)

type th_inst = {
  inst_ts : tysymbol Mts.t;
482
  inst_ls : lsymbol  Mls.t;
Andrei Paskevich's avatar
Andrei Paskevich committed
483 484
}

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
485
let clone_export uc th i =
Andrei Paskevich's avatar
Andrei Paskevich committed
486
  let check_sym id =
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
487
    if not (Sid.mem id th.th_param) then raise (CannotInstantiate id)
Andrei Paskevich's avatar
Andrei Paskevich committed
488 489
  in
  let check_ts s _ = check_sym s.ts_name in Mts.iter check_ts i.inst_ts;
490
  let check_ls s _ = check_sym s.ls_name in Mls.iter check_ls i.inst_ls;
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
491 492 493 494
  (* memo tables *)
  let ts_table = Hashtbl.create 17 in
  let known = ref th.th_known in
  let rec memo_ts ts =
495
    try
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
496 497 498 499 500 501 502 503 504 505 506 507
      Hashtbl.find ts_table ts.ts_name
    with Not_found ->
      let nm = id_clone ts.ts_name in
      let def = match ts.ts_def with
	| None -> None
	| Some ty -> Some (ty_s_map memo_ts ty)
      in
      let ts' = create_tysymbol nm ts.ts_args def in
      Hashtbl.add ts_table ts.ts_name ts';
      known := Mid.add ts'.ts_name uc.uc_name (Mid.remove ts.ts_name !known);
      ts'
  in
508
  let find_ts ts =
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
509 510 511 512 513
    let tid = Mid.find ts.ts_name th.th_known in
    if tid == th.th_name then memo_ts ts else ts
  in
  (* 1. merge in the new namespace *)
  let rec merge_namespace acc ns =
514 515
    let acc =
      Mnm.fold (fun n ts acc -> add_ts n (find_ts ts) acc) ns.ns_ts acc
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
516 517 518 519 520 521 522 523 524 525 526 527 528 529 530 531 532 533
    in
    (* ... *)
    (* let acc = Mnm.fold (fun n ns acc -> ) ns.ns_ns acc in *)
    acc
  in
  let ns = merge_namespace empty_ns th.th_export in
  let uc = match uc.uc_import, uc.uc_export with
    | i0 :: sti, e0 :: ste ->
        { uc with
            uc_import = merge_ns ns i0 :: sti;
            uc_export = merge_ns ns e0 :: ste;
	    uc_known  = merge_known uc.uc_known !known }
    | _ ->
	assert false
  in
  (* 2. merge in the new declarations *)
  (* ... *)
  uc
534 535 536 537


(** Debugging *)

538 539 540 541 542
let print_ident =
  let printer = create_printer () in
  let print fmt id = Format.fprintf fmt "%s" (id_unique printer id) in
  print

543
let rec print_namespace fmt ns =
544
  fprintf fmt "@[<hov 2>types: ";
545 546
  Mnm.iter (fun x ty -> fprintf fmt "%s -> %a;@ " x print_ident ty.ts_name)
    ns.ns_ts;
547 548 549
  fprintf fmt "@]@\n@[<hov 2>logic symbols: ";
  Mnm.iter (fun x s -> fprintf fmt "%s -> %a;@ " x print_ident s.ls_name)
    ns.ns_ls;
550
  fprintf fmt "@]@\n@[<hov 2>namespace: ";
551 552
  Mnm.iter (fun x th -> fprintf fmt "%s -> [@[%a@]];@ " x print_namespace th)
    ns.ns_ns;
553 554
  fprintf fmt "@]"

555 556
let print_uc fmt uc = print_namespace fmt (get_namespace uc)
let print_th fmt th = fprintf fmt "<theory (TODO>"
557 558

(*
559
Local Variables:
560
compile-command: "make -C ../.. test"
561
End:
562
*)