theory.ml 23.2 KB
Newer Older
1 2 3
(**************************************************************************)
(*                                                                        *)
(*  Copyright (C) 2010-                                                   *)
MARCHE Claude's avatar
MARCHE Claude committed
4 5 6
(*    François Bobot                                                     *)
(*    Jean-Christophe Filliâtre                                          *)
(*    Claude Marché                                                      *)
7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28
(*    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 Format
open Util
open Ident
open Ty
open Term
open Decl

(** Namespace *)

Andrei Paskevich's avatar
Andrei Paskevich committed
29 30
module Snm = Sstr
module Mnm = Mstr
31 32 33 34

type namespace = {
  ns_ts : tysymbol Mnm.t;   (* type symbols *)
  ns_ls : lsymbol Mnm.t;    (* logic symbols *)
35
  ns_pr : prsymbol Mnm.t;   (* propositions *)
36 37 38 39 40 41 42
  ns_ns : namespace Mnm.t;  (* inner namespaces *)
}

let empty_ns = {
  ns_ts = Mnm.empty;
  ns_ls = Mnm.empty;
  ns_pr = Mnm.empty;
43
  ns_ns = Mnm.empty;
44 45 46 47
}

exception ClashSymbol of string

48 49 50 51 52 53 54
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))
55 56

let rec merge_ns chk ns1 ns2 =
57
  let fusion _ ns1 ns2 = Some (merge_ns chk ns1 ns2) in
58 59 60
  { ns_ts = ns_union ts_equal chk ns1.ns_ts ns2.ns_ts;
    ns_ls = ns_union ls_equal chk ns1.ns_ls ns2.ns_ls;
    ns_pr = ns_union pr_equal chk ns1.ns_pr ns2.ns_pr;
61
    ns_ns = Mnm.union fusion      ns1.ns_ns ns2.ns_ns; }
62

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

67 68 69
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
70

71 72
let ts_add = ns_add ts_equal
let ls_add = ns_add ls_equal
73
let pr_add = ns_add pr_equal
74

75 76 77
let add_ts chk x ts ns = { ns with ns_ts = ts_add chk x ts ns.ns_ts }
let add_ls chk x ls ns = { ns with ns_ls = ls_add chk x ls ns.ns_ls }
let add_pr chk x pf ns = { ns with ns_pr = pr_add chk x pf ns.ns_pr }
78
let add_ns chk x nn ns = { ns with ns_ns = nm_add chk x nn ns.ns_ns }
79 80 81 82 83 84 85 86

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_ts = ns_find (fun ns -> ns.ns_ts)
let ns_find_ls = ns_find (fun ns -> ns.ns_ls)
87
let ns_find_pr = ns_find (fun ns -> ns.ns_pr)
88
let ns_find_ns = ns_find (fun ns -> ns.ns_ns)
89

90 91 92
(** Meta properties *)

type meta_arg_type =
93
  | MTty
94 95 96 97 98 99 100
  | MTtysymbol
  | MTlsymbol
  | MTprsymbol
  | MTstring
  | MTint

type meta_arg =
101
  | MAty  of ty
102 103 104 105 106 107
  | MAts  of tysymbol
  | MAls  of lsymbol
  | MApr  of prsymbol
  | MAstr of string
  | MAint of int

108 109
type meta = {
  meta_name : string;
110
  meta_type : meta_arg_type list;
111
  meta_excl : bool;
112
  meta_tag  : int;
113 114 115
}

module SMmeta = StructMake(struct type t = meta let tag m = m.meta_tag end)
116

117 118 119 120
module Smeta = SMmeta.S
module Mmeta = SMmeta.M
module Hmeta = SMmeta.H

121
let meta_equal : meta -> meta -> bool = (==)
Andrei Paskevich's avatar
Andrei Paskevich committed
122 123

let meta_hash m = m.meta_tag
124 125

exception KnownMeta of meta
126
exception UnknownMeta of string
127 128
exception BadMetaArity of meta * int * int
exception MetaTypeMismatch of meta * meta_arg_type * meta_arg_type
129 130 131

let meta_table = Hashtbl.create 17

132 133 134 135 136 137 138 139
let mk_meta =
  let c = ref (-1) in
  fun s al excl -> {
    meta_name = s;
    meta_type = al;
    meta_excl = excl;
    meta_tag  = (incr c; !c) }

140 141
let register_meta s al excl =
  try
142 143 144 145 146 147 148
    let m = Hashtbl.find meta_table s in
    if al = m.meta_type && excl = m.meta_excl then m
    else raise (KnownMeta m)
  with Not_found ->
    let m = mk_meta s al excl in
    Hashtbl.add meta_table s m;
    m
149 150

let register_meta_excl s al = register_meta s al true
151
let register_meta      s al = register_meta s al false
152

153
let lookup_meta s =
154
  try Hashtbl.find meta_table s
155
  with Not_found -> raise (UnknownMeta s)
156

157
let list_metas () = Hashtbl.fold (fun _ v acc -> v::acc) meta_table []
158 159 160 161

(** Theory *)

type theory = {
162 163 164 165 166 167 168 169 170 171 172
  th_name   : ident;      (* theory name *)
  th_decls  : tdecl list; (* theory declarations *)
  th_export : namespace;  (* exported namespace *)
  th_known  : known_map;  (* known identifiers *)
  th_local  : Sid.t;      (* locally declared idents *)
  th_used   : Sid.t;      (* used theories *)
}

and tdecl = {
  td_node : tdecl_node;
  td_tag  : int;
173 174
}

175
and tdecl_node =
176 177
  | Decl  of decl
  | Use   of theory
178
  | Clone of theory * symbol_map
179
  | Meta  of meta * meta_arg list
180

181 182 183 184 185 186
and symbol_map = {
  sm_ts : tysymbol Mts.t;
  sm_ls : lsymbol Mls.t;
  sm_pr : prsymbol Mpr.t;
}

187
(** Theory declarations *)
188

189
module Hstdecl = Hashcons.Make (struct
190

191 192 193
  type t = tdecl

  let eq_marg a1 a2 = match a1,a2 with
194
    | MAty ty1, MAty ty2 -> ty_equal ty1 ty2
195 196 197 198 199
    | MAts ts1, MAts ts2 -> ts_equal ts1 ts2
    | MAls ls1, MAls ls2 -> ls_equal ls1 ls2
    | MApr pr1, MApr pr2 -> pr_equal pr1 pr2
    | MAstr s1, MAstr s2 -> s1 = s2
    | MAint i1, MAint i2 -> i1 = i2
200 201
    | _,_ -> false

202 203 204 205 206
  let eq_smap sm1 sm2 =
    Mts.equal ts_equal sm1.sm_ts sm2.sm_ts &&
    Mls.equal ls_equal sm1.sm_ls sm2.sm_ls &&
    Mpr.equal pr_equal sm1.sm_pr sm2.sm_pr

207 208 209
  let equal td1 td2 = match td1.td_node, td2.td_node with
    | Decl d1, Decl d2 -> d_equal d1 d2
    | Use th1, Use th2 -> id_equal th1.th_name th2.th_name
210 211
    | Clone (th1,sm1), Clone (th2,sm2) ->
        id_equal th1.th_name th2.th_name && eq_smap sm1 sm2
212 213 214 215
    | Meta (t1,al1), Meta (t2,al2) ->
        t1 = t2 && list_all2 eq_marg al1 al2
    | _,_ -> false

Andrei Paskevich's avatar
Andrei Paskevich committed
216 217 218
  let hs_cl_ts _ ts acc = Hashcons.combine acc (ts_hash ts)
  let hs_cl_ls _ ls acc = Hashcons.combine acc (ls_hash ls)
  let hs_cl_pr _ pr acc = Hashcons.combine acc (pr_hash pr)
219 220

  let hs_ta = function
221
    | MAty ty -> ty_hash ty
Andrei Paskevich's avatar
Andrei Paskevich committed
222 223 224
    | MAts ts -> ts_hash ts
    | MAls ls -> ls_hash ls
    | MApr pr -> pr_hash pr
225 226
    | MAstr s -> Hashtbl.hash s
    | MAint i -> Hashtbl.hash i
227

228 229 230 231 232
  let hs_smap sm h =
    Mts.fold hs_cl_ts sm.sm_ts
      (Mls.fold hs_cl_ls sm.sm_ls
        (Mpr.fold hs_cl_pr sm.sm_pr h))

233
  let hash td = match td.td_node with
Andrei Paskevich's avatar
Andrei Paskevich committed
234 235
    | Decl d -> d_hash d
    | Use th -> id_hash th.th_name
236
    | Clone (th,sm) -> hs_smap sm (id_hash th.th_name)
237 238 239 240 241 242 243 244 245 246 247 248 249 250 251 252 253
    | Meta (t,al) -> Hashcons.combine_list hs_ta (Hashtbl.hash t) al

  let tag n td = { td with td_tag = n }

end)

let mk_tdecl n = Hstdecl.hashcons { td_node = n ; td_tag = -1 }

module Tdecl = StructMake (struct
  type t = tdecl
  let tag td = td.td_tag
end)

module Stdecl = Tdecl.S
module Mtdecl = Tdecl.M
module Htdecl = Tdecl.H

254
let td_equal : tdecl -> tdecl -> bool = (==)
Andrei Paskevich's avatar
Andrei Paskevich committed
255
let td_hash td = td.td_tag
256 257 258 259 260 261 262 263

(** Constructors and utilities *)

type theory_uc = {
  uc_name   : ident;
  uc_decls  : tdecl list;
  uc_import : namespace list;
  uc_export : namespace list;
264
  uc_known  : known_map;
265
  uc_local  : Sid.t;
266
  uc_used   : Sid.t;
267 268 269 270 271
}

exception CloseTheory
exception NoOpenedNamespace

272 273 274 275 276 277 278 279 280
let empty_theory n = {
  uc_name   = id_register n;
  uc_decls  = [];
  uc_import = [empty_ns];
  uc_export = [empty_ns];
  uc_known  = Mid.empty;
  uc_local  = Sid.empty;
  uc_used   = Sid.empty;
}
281 282

let close_theory uc = match uc.uc_export with
283 284 285 286 287 288 289 290
  | [e] -> {
      th_name   = uc.uc_name;
      th_decls  = List.rev uc.uc_decls;
      th_export = e;
      th_known  = uc.uc_known;
      th_local  = uc.uc_local;
      th_used   = uc.uc_used }
  | _ -> raise CloseTheory
291 292

let get_namespace uc = List.hd uc.uc_import
293
let get_known uc = uc.uc_known
294 295

let open_namespace uc = match uc.uc_import with
296 297 298 299
  | ns :: _ -> { uc with
      uc_import =       ns :: uc.uc_import;
      uc_export = empty_ns :: uc.uc_export; }
  | [] -> assert false
300 301 302 303 304 305 306 307 308

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
      { uc with uc_import = i1 :: sti; uc_export = e1 :: ste; }
309 310
  | [_], [_] -> raise NoOpenedNamespace
  | _ -> assert false
311

312
(* Base constructors *)
313

314 315 316 317
let known_clone kn sm =
  Mts.iter (fun _ ts -> known_id kn ts.ts_name) sm.sm_ts;
  Mls.iter (fun _ ls -> known_id kn ls.ls_name) sm.sm_ls;
  Mpr.iter (fun _ pr -> known_id kn pr.pr_name) sm.sm_pr
318 319 320

let known_meta kn al =
  let check = function
321
    | MAty ty -> ty_s_fold (fun () ts -> known_id kn ts.ts_name) () ty
322 323 324
    | MAts ts -> known_id kn ts.ts_name
    | MAls ls -> known_id kn ls.ls_name
    | MApr pr -> known_id kn pr.pr_name
325
    | _ -> ()
326
  in
327
  List.iter check al
328

329 330 331 332 333 334 335 336 337 338
let add_tdecl uc td = match td.td_node with
  | Decl d -> { uc with
      uc_decls = td :: uc.uc_decls;
      uc_known = known_add_decl uc.uc_known d;
      uc_local = Sid.union uc.uc_local d.d_news }
  | Use th when Sid.mem th.th_name uc.uc_used -> uc
  | Use th -> { uc with
      uc_decls = td :: uc.uc_decls;
      uc_known = merge_known uc.uc_known th.th_known;
      uc_used  = Sid.union uc.uc_used (Sid.add th.th_name th.th_used) }
339
  | Clone (_,sm) -> known_clone uc.uc_known sm;
340 341 342 343 344
      { uc with uc_decls = td :: uc.uc_decls }
  | Meta (_,al) -> known_meta uc.uc_known al;
      { uc with uc_decls = td :: uc.uc_decls }

(** Declarations *)
345

346 347 348
let add_symbol add id v uc =
  match uc.uc_import, uc.uc_export with
  | i0 :: sti, e0 :: ste -> { uc with
349
      uc_import = add false id.id_string v i0 :: sti;
350 351
      uc_export = add true  id.id_string v e0 :: ste }
  | _ -> assert false
352 353 354 355 356 357 358 359 360 361 362 363

let add_type uc (ts,def) =
  let add_constr uc fs = add_symbol add_ls fs.ls_name fs uc in
  let uc = add_symbol add_ts ts.ts_name ts uc in
  match def with
    | Tabstract -> uc
    | Talgebraic lfs -> List.fold_left add_constr uc lfs

let add_logic uc (ls,_) = add_symbol add_ls ls.ls_name ls uc

let add_ind uc (ps,la) =
  let uc = add_symbol add_ls ps.ls_name ps uc in
364
  let add uc (pr,_) = add_symbol add_pr pr.pr_name pr uc in
365 366
  List.fold_left add uc la

367 368 369
let add_prop uc (_,pr,_) = add_symbol add_pr pr.pr_name pr uc

let create_decl d = mk_tdecl (Decl d)
370 371

let add_decl uc d =
372 373
  let uc = add_tdecl uc (create_decl d) in
  match d.d_node with
374 375 376 377 378
    | Dtype dl  -> List.fold_left add_type uc dl
    | Dlogic dl -> List.fold_left add_logic uc dl
    | Dind dl   -> List.fold_left add_ind uc dl
    | Dprop p   -> add_prop uc p

379
(** Declaration constructors + add_decl *)
Andrei Paskevich's avatar
Andrei Paskevich committed
380

381 382 383 384 385
let add_ty_decl uc dl = add_decl uc (create_ty_decl dl)
let add_logic_decl uc dl = add_decl uc (create_logic_decl dl)
let add_ind_decl uc dl = add_decl uc (create_ind_decl dl)
let add_prop_decl uc k p f = add_decl uc (create_prop_decl k p f)

386 387 388 389 390 391 392 393 394 395 396
(** Use *)

let create_use th = mk_tdecl (Use th)

let use_export uc th =
  let uc = add_tdecl uc (create_use th) in
  match uc.uc_import, uc.uc_export with
  | i0 :: sti, e0 :: ste -> { uc with
      uc_import = merge_ns false th.th_export i0 :: sti;
      uc_export = merge_ns true  th.th_export e0 :: ste }
  | _ -> assert false
397 398 399 400 401 402 403 404 405 406 407 408 409 410 411 412 413

(** Clone *)

type th_inst = {
  inst_ts    : tysymbol Mts.t;
  inst_ls    : lsymbol  Mls.t;
  inst_lemma : Spr.t;
  inst_goal  : Spr.t;
}

let empty_inst = {
  inst_ts    = Mts.empty;
  inst_ls    = Mls.empty;
  inst_lemma = Spr.empty;
  inst_goal  = Spr.empty;
}

Francois Bobot's avatar
 
Francois Bobot committed
414
let create_inst ~ts ~ls ~lemma ~goal =
415 416 417 418 419 420 421
  let add_ts acc (tso,tsn) = Mts.add tso tsn acc in
  let add_ls acc (lso,lsn) = Mls.add lso lsn acc in
  let add_pr acc lem = Spr.add lem acc in {
    inst_ts    = List.fold_left add_ts Mts.empty ts;
    inst_ls    = List.fold_left add_ls Mls.empty ls;
    inst_lemma = List.fold_left add_pr Spr.empty lemma;
    inst_goal  = List.fold_left add_pr Spr.empty goal }
Francois Bobot's avatar
 
Francois Bobot committed
422

423 424 425
exception CannotInstantiate of ident

type clones = {
426
  cl_local : Sid.t;
427 428 429
  mutable ts_table : tysymbol Mts.t;
  mutable ls_table : lsymbol Mls.t;
  mutable pr_table : prsymbol Mpr.t;
430 431 432
}

let empty_clones s = {
433
  cl_local = s;
434 435 436
  ts_table = Mts.empty;
  ls_table = Mls.empty;
  pr_table = Mpr.empty;
437 438 439 440 441
}

(* populate the clone structure *)

let rec cl_find_ts cl ts =
442
  if not (Sid.mem ts.ts_name cl.cl_local) then ts
443
  else try Mts.find ts cl.ts_table
444
  with Not_found ->
445
    let td' = option_map (cl_trans_ty cl) ts.ts_def in
446
    let ts' = create_tysymbol (id_dup ts.ts_name) ts.ts_args td' in
447
    cl.ts_table <- Mts.add ts ts' cl.ts_table;
448 449
    ts'

450
and cl_trans_ty cl ty = ty_s_map (cl_find_ts cl) ty
451 452

let cl_find_ls cl ls =
453
  if not (Sid.mem ls.ls_name cl.cl_local) then ls
454
  else try Mls.find ls cl.ls_table
455 456 457
  with Not_found ->
    let ta' = List.map (cl_trans_ty cl) ls.ls_args in
    let vt' = option_map (cl_trans_ty cl) ls.ls_value in
458
    let ls' = create_lsymbol (id_dup ls.ls_name) ta' vt' in
459
    cl.ls_table <- Mls.add ls ls' cl.ls_table;
460 461 462 463
    ls'

let cl_trans_fmla cl f = f_s_map (cl_find_ts cl) (cl_find_ls cl) f

464
let cl_find_pr cl pr =
465 466
  if not (Sid.mem pr.pr_name cl.cl_local) then pr
  else try Mpr.find pr cl.pr_table
467 468
  with Not_found ->
    let pr' = create_prsymbol (id_dup pr.pr_name) in
469
    cl.pr_table <- Mpr.add pr pr' cl.pr_table;
470
    pr'
471 472 473 474 475 476 477 478

(* initialize the clone structure *)

exception NonLocal of ident
exception BadInstance of ident * ident

let cl_init_ts cl ts ts' =
  let id = ts.ts_name in
479
  if not (Sid.mem id cl.cl_local) then raise (NonLocal id);
480 481
  if List.length ts.ts_args <> List.length ts'.ts_args
    then raise (BadInstance (id, ts'.ts_name));
482
  cl.ts_table <- Mts.add ts ts' cl.ts_table
483 484 485

let cl_init_ls cl ls ls' =
  let id = ls.ls_name in
486
  if not (Sid.mem id cl.cl_local) then raise (NonLocal id);
487 488
  let mtch sb ty ty' =
    try ty_match sb ty' (cl_trans_ty cl ty)
489
    with TypeMismatch _ -> raise (BadInstance (id, ls'.ls_name))
490 491
  in
  let sb = match ls.ls_value,ls'.ls_value with
492
    | Some ty, Some ty' -> mtch Mtv.empty ty ty'
493 494 495
    | None, None -> Mtv.empty
    | _ -> raise (BadInstance (id, ls'.ls_name))
  in
496
  ignore (try List.fold_left2 mtch sb ls.ls_args ls'.ls_args
497
  with Invalid_argument _ -> raise (BadInstance (id, ls'.ls_name)));
498
  cl.ls_table <- Mls.add ls ls' cl.ls_table
499 500

let cl_init_pr cl pr =
501 502
  let id = pr.pr_name in
  if not (Sid.mem id cl.cl_local) then raise (NonLocal id)
503 504 505 506 507 508 509 510 511 512 513

let cl_init th inst =
  let cl = empty_clones th.th_local in
  Mts.iter (cl_init_ts cl) inst.inst_ts;
  Mls.iter (cl_init_ls cl) inst.inst_ls;
  Spr.iter (cl_init_pr cl) inst.inst_lemma;
  Spr.iter (cl_init_pr cl) inst.inst_goal;
  cl

(* clone declarations *)

514 515 516 517 518 519 520 521 522 523 524 525 526 527 528 529 530 531 532
let cl_type cl inst tdl =
  let add_constr ls =
    if Mls.mem ls inst.inst_ls
      then raise (CannotInstantiate ls.ls_name)
      else cl_find_ls cl ls
  in
  let add_type (ts,td) acc =
    if Mts.mem ts inst.inst_ts then
      if ts.ts_def = None && td = Tabstract then acc
      else raise (CannotInstantiate ts.ts_name)
    else
      let ts' = cl_find_ts cl ts in
      let td' = match td with
        | Tabstract -> Tabstract
        | Talgebraic cl -> Talgebraic (List.map add_constr cl)
      in
      (ts',td') :: acc
  in
  create_ty_decl (List.fold_right add_type tdl [])
533 534 535 536

let extract_ls_defn f =
  let vl, ef = f_open_forall f in
  match ef.f_node with
537
    | Fapp (s, [t1; t2]) when ls_equal s ps_equ ->
538 539 540 541 542 543 544 545 546 547 548
        begin match t1.t_node with
          | Tapp (fs, _) -> make_fs_defn fs vl t2
          | _ -> assert false
        end
    | Fbinop (Fiff, f1, f2) ->
        begin match f1.f_node with
          | Fapp (ps, _) -> make_ps_defn ps vl f2
          | _ -> assert false
        end
    | _ -> assert false

549 550 551 552 553 554 555 556 557 558 559
let cl_logic cl inst ldl =
  let add_logic (ls,ld) acc = match ld with
    | None when Mls.mem ls inst.inst_ls ->
        acc
    | None ->
        (cl_find_ls cl ls, None) :: acc
    | Some _ when Mls.mem ls inst.inst_ls ->
        raise (CannotInstantiate ls.ls_name)
    | Some ld ->
        let f = ls_defn_axiom ld in
        extract_ls_defn (cl_trans_fmla cl f) :: acc
560
  in
561
  create_logic_decl (List.fold_right add_logic ldl [])
562

563 564 565 566 567 568 569 570 571 572 573 574 575 576 577 578 579 580 581 582 583 584 585 586 587 588 589 590 591 592 593 594
let cl_ind cl inst idl =
  let add_case (pr,f) =
    if Spr.mem pr inst.inst_lemma || Spr.mem pr inst.inst_goal
      then raise (CannotInstantiate pr.pr_name)
      else cl_find_pr cl pr, cl_trans_fmla cl f
  in
  let add_ind (ps,la) =
    if Mls.mem ps inst.inst_ls
      then raise (CannotInstantiate ps.ls_name)
      else cl_find_ls cl ps, List.map add_case la
  in
  create_ind_decl (List.map add_ind idl)

let cl_prop cl inst (k,pr,f) =
  let k' = match k with
    | Pskip | Pgoal -> Pskip
    | Plemma when Spr.mem pr inst.inst_goal -> Pskip
    | Paxiom when Spr.mem pr inst.inst_goal -> Pgoal
    | Paxiom when Spr.mem pr inst.inst_lemma -> Plemma
    | Paxiom | Plemma -> Paxiom
  in
  let pr' = cl_find_pr cl pr in
  let f' = cl_trans_fmla cl f in
  create_prop_decl k' pr' f'

let cl_decl cl inst d = match d.d_node with
  | Dtype tdl -> cl_type cl inst tdl
  | Dlogic ldl -> cl_logic cl inst ldl
  | Dind idl -> cl_ind cl inst idl
  | Dprop p -> cl_prop cl inst p

let cl_marg cl = function
595
  | MAty ty -> MAty (cl_trans_ty cl ty)
596 597 598
  | MAts ts -> MAts (cl_find_ts cl ts)
  | MAls ls -> MAls (cl_find_ls cl ls)
  | MApr pr -> MApr (cl_find_pr cl pr)
599 600
  | a -> a

601 602 603 604 605
let cl_smap cl sm = {
  sm_ts = Mts.map (cl_find_ts cl) sm.sm_ts;
  sm_ls = Mls.map (cl_find_ls cl) sm.sm_ls;
  sm_pr = Mpr.map (cl_find_pr cl) sm.sm_pr}

606 607 608
let cl_tdecl cl inst td = match td.td_node with
  | Decl d -> Decl (cl_decl cl inst d)
  | Use th -> Use th
609
  | Clone (th,sm) -> Clone (th, cl_smap cl sm)
610 611 612 613 614 615 616 617 618 619 620
  | Meta (id,al) -> Meta (id, List.map (cl_marg cl) al)

let clone_theory cl add_td acc th inst =
  let add acc td =
    let td =
      try  Some (mk_tdecl (cl_tdecl cl inst td))
      with EmptyDecl -> None
    in
    option_apply acc (add_td acc) td
  in
  let acc = List.fold_left add acc th.th_decls in
621 622 623 624 625 626
  let sm = {
    sm_ts = cl.ts_table;
    sm_ls = cl.ls_table;
    sm_pr = cl.pr_table}
  in
  add_td acc (mk_tdecl (Clone (th, sm)))
627 628 629

let clone_export uc th inst =
  let cl = cl_init th inst in
630
  let uc = clone_theory cl add_tdecl uc th inst in
631

632 633 634 635 636 637 638 639 640 641 642 643 644 645
  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 = Mts.find_default ts ts cl.ts_table in
  let f_ls ls = Mls.find_default ls ls cl.ls_table in
  let f_pr pr = Mpr.find_default pr pr cl.pr_table in

  let rec f_ns ns = {
    ns_ts = Mnm.map f_ts (Mnm.filter g_ts ns.ns_ts);
    ns_ls = Mnm.map f_ls (Mnm.filter g_ls ns.ns_ls);
    ns_pr = Mnm.map f_pr ns.ns_pr;
    ns_ns = Mnm.map f_ns ns.ns_ns; } in

  let ns = f_ns th.th_export in
646 647 648 649

  match uc.uc_import, uc.uc_export with
    | i0 :: sti, e0 :: ste -> { uc with
        uc_import = merge_ns false ns i0 :: sti;
Andrei Paskevich's avatar
Andrei Paskevich committed
650
        uc_export = merge_ns true  ns e0 :: ste; }
651 652 653 654 655 656 657
    | _ -> assert false

let clone_theory add_td acc th inst =
  clone_theory (cl_init th inst) add_td acc th inst

let create_clone = clone_theory (fun tdl td -> td :: tdl)

658
let create_null_clone th =
659 660 661 662 663 664 665 666 667 668 669
  let sm = {
    sm_ts = Mts.empty;
    sm_ls = Mls.empty;
    sm_pr = Mpr.empty}
  in
  mk_tdecl (Clone (th,sm))

let is_empty_sm sm =
  Mts.is_empty sm.sm_ts &&
  Mls.is_empty sm.sm_ls &&
  Mpr.is_empty sm.sm_pr
670 671 672 673 674


(** Meta properties *)

let get_meta_arg_type = function
675
  | MAty  _ -> MTty
676 677 678 679 680 681
  | MAts  _ -> MTtysymbol
  | MAls  _ -> MTlsymbol
  | MApr  _ -> MTprsymbol
  | MAstr _ -> MTstring
  | MAint _ -> MTint

682
let create_meta m al =
683
  let get_meta_arg at a =
684 685 686
    (* we allow "constant tysymbol <=> ty" conversion *)
    let a = match at,a with
      | MTtysymbol, MAty ({ ty_node = Tyapp (ts,[]) }) -> MAts ts
687
      | MTty, MAts ({ts_args = []} as ts) -> MAty (ty_app ts [])
688 689
      | _, _ -> a
    in
690
    let mt = get_meta_arg_type a in
691
    if at = mt then a else raise (MetaTypeMismatch (m,at,mt))
692
  in
693
  let al = try List.map2 get_meta_arg m.meta_type al
694
    with Invalid_argument _ ->
695
      raise (BadMetaArity (m, List.length m.meta_type, List.length al))
696
  in
697
  mk_tdecl (Meta (m,al))
698 699 700

let add_meta uc s al = add_tdecl uc (create_meta s al)

701 702
let clone_meta tdt sm = match tdt.td_node with
  | Meta (t,al) ->
703 704 705
      let find_ts ts = Mts.find_default ts ts sm.sm_ts in
      let find_ls ls = Mls.find_default ls ls sm.sm_ls in
      let find_pr pr = Mpr.find_default pr pr sm.sm_pr in
706
      let cl_marg = function
707
        | MAty ty -> MAty (ty_s_map find_ts ty)
708 709 710 711 712
        | MAts ts -> MAts (find_ts ts)
        | MAls ls -> MAls (find_ls ls)
        | MApr pr -> MApr (find_pr pr)
        | a -> a
      in
713
      mk_tdecl (Meta (t, List.map cl_marg al))
714
  | _ -> invalid_arg "clone_meta"
715

716

717 718 719 720 721 722 723 724 725
(** Base theories *)

let builtin_theory =
  let uc = empty_theory (id_fresh "BuiltIn") in
  let uc = add_ty_decl uc [ts_int, Tabstract] in
  let uc = add_ty_decl uc [ts_real, Tabstract] in
  let uc = add_logic_decl uc [ps_equ, None] in
  close_theory uc

726 727 728 729 730 731 732 733
let highord_theory =
  let uc = empty_theory (id_fresh "HighOrd") in
  let uc = add_ty_decl uc [ts_func, Tabstract] in
  let uc = add_ty_decl uc [ts_pred, Tabstract] in
  let uc = add_logic_decl uc [fs_func_app, None] in
  let uc = add_logic_decl uc [ps_pred_app, None] in
  close_theory uc

734
let create_theory n = use_export (empty_theory n) builtin_theory
735

736
let tuple_theory = Util.memo_int 17 (fun n ->
737
  let uc = empty_theory (id_fresh ("Tuple" ^ string_of_int n)) in
738
  let uc = add_ty_decl uc [ts_tuple n, Talgebraic [fs_tuple n]] in
739
  close_theory uc)
740

741 742 743 744 745 746 747 748 749 750 751
let tuple_theory_name s =
  let l = String.length s in
  if l < 6 then None else
  let p = String.sub s 0 5 in
  if p <> "Tuple" then None else
  let q = String.sub s 5 (l - 5) in
  let i = try int_of_string q with _ -> 0 in
  (* we only accept the decimal notation *)
  if q <> string_of_int i then None else
  Some i

752 753
(* Exception reporting *)

754
let print_meta_arg_type fmt = function
755
  | MTty -> fprintf fmt "type"
756 757 758 759 760 761
  | MTtysymbol -> fprintf fmt "type_symbol"
  | MTlsymbol -> fprintf fmt "logic_symbol"
  | MTprsymbol -> fprintf fmt "proposition"
  | MTstring -> fprintf fmt "string"
  | MTint -> fprintf fmt "int"

762 763 764 765 766 767 768 769 770 771 772 773 774 775 776
let () = Exn_printer.register
  begin fun fmt exn -> match exn with
  | NonLocal id ->
      Format.fprintf fmt "Non-local ident: %s" id.id_string
  | CannotInstantiate id ->
      Format.fprintf fmt "Cannot instantiate a defined ident %s" id.id_string
  | BadInstance (id1, id2) ->
      Format.fprintf fmt "Cannot instantiate ident %s with %s"
        id1.id_string id2.id_string
  | CloseTheory ->
      Format.fprintf fmt "Cannot close theory: some namespaces are still open"
  | NoOpenedNamespace ->
      Format.fprintf fmt "No opened namespaces"
  | ClashSymbol s ->
      Format.fprintf fmt "Symbol %s is already defined in the current scope" s
777 778
  | UnknownMeta s ->
      Format.fprintf fmt "Unknown metaproperty %s" s
779
  | KnownMeta m ->
780
      Format.fprintf fmt "Metaproperty %s is already registered with \
781 782
        a conflicting signature" m.meta_name
  | BadMetaArity (m,i1,i2) ->
783
      Format.fprintf fmt "Metaproperty %s requires %d arguments but \
784 785
        is applied to %d" m.meta_name i1 i2
  | MetaTypeMismatch (m,t1,t2) ->
786
      Format.fprintf fmt "Metaproperty %s expects %a argument but \
787 788
        is applied to %a"
        m.meta_name print_meta_arg_type t1 print_meta_arg_type t2
789 790 791
  | _ -> raise exn
  end