theory.ml 24.2 KB
Newer Older
1 2
(**************************************************************************)
(*                                                                        *)
3
(*  Copyright (C) 2010-2011                                               *)
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 29
(*    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 *)

type namespace = {
30 31 32 33
  ns_ts : tysymbol Mstr.t;   (* type symbols *)
  ns_ls : lsymbol Mstr.t;    (* logic symbols *)
  ns_pr : prsymbol Mstr.t;   (* propositions *)
  ns_ns : namespace Mstr.t;  (* inner namespaces *)
34 35 36
}

let empty_ns = {
37 38 39 40
  ns_ts = Mstr.empty;
  ns_ls = Mstr.empty;
  ns_pr = Mstr.empty;
  ns_ns = Mstr.empty;
41 42 43 44
}

exception ClashSymbol of string

45 46 47 48 49 50
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 =
51
  Mstr.union (fun x vn vo -> Some (ns_replace eq chk x vo vn))
52 53

let rec merge_ns chk ns1 ns2 =
54
  let fusion _ ns1 ns2 = Some (merge_ns chk ns1 ns2) in
55 56 57
  { 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;
58
    ns_ns = Mstr.union fusion     ns1.ns_ns ns2.ns_ns; }
59

60
let nm_add chk x ns m = Mstr.change x (function
61 62
  | None -> Some ns
  | Some os -> Some (merge_ns chk ns os)) m
63

64
let ns_add eq chk x v m = Mstr.change x (function
65 66
  | None -> Some v
  | Some vo -> Some (ns_replace eq chk x vo v)) m
67

68 69
let ts_add = ns_add ts_equal
let ls_add = ns_add ls_equal
70
let pr_add = ns_add pr_equal
71

72 73 74
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 }
75
let add_ns chk x nn ns = { ns with ns_ns = nm_add chk x nn ns.ns_ns }
76 77 78

let rec ns_find get_map ns = function
  | []   -> assert false
79 80
  | [a]  -> Mstr.find a (get_map ns)
  | a::l -> ns_find get_map (Mstr.find a ns.ns_ns) l
81 82 83

let ns_find_ts = ns_find (fun ns -> ns.ns_ts)
let ns_find_ls = ns_find (fun ns -> ns.ns_ls)
84
let ns_find_pr = ns_find (fun ns -> ns.ns_pr)
85
let ns_find_ns = ns_find (fun ns -> ns.ns_ns)
86

87 88 89
(** Meta properties *)

type meta_arg_type =
90
  | MTty
91 92 93 94 95 96 97
  | MTtysymbol
  | MTlsymbol
  | MTprsymbol
  | MTstring
  | MTint

type meta_arg =
98
  | MAty  of ty
99 100 101 102 103 104
  | MAts  of tysymbol
  | MAls  of lsymbol
  | MApr  of prsymbol
  | MAstr of string
  | MAint of int

105 106
type meta = {
  meta_name : string;
107
  meta_type : meta_arg_type list;
108
  meta_excl : bool;
109
  meta_tag  : int;
110 111 112
}

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

114 115 116 117
module Smeta = SMmeta.S
module Mmeta = SMmeta.M
module Hmeta = SMmeta.H

118
let meta_equal : meta -> meta -> bool = (==)
Andrei Paskevich's avatar
Andrei Paskevich committed
119 120

let meta_hash m = m.meta_tag
121 122

exception KnownMeta of meta
123
exception UnknownMeta of string
124 125
exception BadMetaArity of meta * int * int
exception MetaTypeMismatch of meta * meta_arg_type * meta_arg_type
126 127 128

let meta_table = Hashtbl.create 17

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

137 138
let register_meta s al excl =
  try
139 140 141 142 143 144 145
    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
146 147

let register_meta_excl s al = register_meta s al true
148
let register_meta      s al = register_meta s al false
149

150
let lookup_meta s =
151
  try Hashtbl.find meta_table s
152
  with Not_found -> raise (UnknownMeta s)
153

154
let list_metas () = Hashtbl.fold (fun _ v acc -> v::acc) meta_table []
155 156 157 158

(** Theory *)

type theory = {
159
  th_name   : ident;      (* theory name *)
160
  th_path   : string list;(* environment qualifiers *)
161 162 163 164 165 166 167 168 169 170
  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;
171 172
}

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

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

185
(** Theory declarations *)
186

187
module Hstdecl = Hashcons.Make (struct
188

189 190 191
  type t = tdecl

  let eq_marg a1 a2 = match a1,a2 with
192
    | MAty ty1, MAty ty2 -> ty_equal ty1 ty2
193 194 195 196 197
    | 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
198 199
    | _,_ -> false

200 201 202 203 204
  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

205 206 207
  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
208 209
    | Clone (th1,sm1), Clone (th2,sm2) ->
        id_equal th1.th_name th2.th_name && eq_smap sm1 sm2
210 211 212 213
    | Meta (t1,al1), Meta (t2,al2) ->
        t1 = t2 && list_all2 eq_marg al1 al2
    | _,_ -> false

Andrei Paskevich's avatar
Andrei Paskevich committed
214 215 216
  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)
217 218

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

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

231
  let hash td = match td.td_node with
Andrei Paskevich's avatar
Andrei Paskevich committed
232 233
    | Decl d -> d_hash d
    | Use th -> id_hash th.th_name
234
    | Clone (th,sm) -> hs_smap sm (id_hash th.th_name)
235 236 237 238 239 240 241 242 243 244 245 246 247 248 249 250 251
    | 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

252
let td_equal : tdecl -> tdecl -> bool = (==)
Andrei Paskevich's avatar
Andrei Paskevich committed
253
let td_hash td = td.td_tag
254 255 256 257 258

(** Constructors and utilities *)

type theory_uc = {
  uc_name   : ident;
259
  uc_path   : string list;
260 261 262
  uc_decls  : tdecl list;
  uc_import : namespace list;
  uc_export : namespace list;
263
  uc_known  : known_map;
264
  uc_local  : Sid.t;
265
  uc_used   : Sid.t;
266 267 268 269 270
}

exception CloseTheory
exception NoOpenedNamespace

271
let empty_theory n p = {
272
  uc_name   = id_register n;
273
  uc_path   = p;
274 275 276 277 278 279 280
  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
  | [e] -> {
      th_name   = uc.uc_name;
285
      th_path   = uc.uc_path;
286 287 288 289 290 291
      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
292 293

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

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

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; }
310 311
  | [_], [_] -> raise NoOpenedNamespace
  | _ -> assert false
312

313
(* Base constructors *)
314

315 316 317 318
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
319 320 321

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

330 331 332 333 334 335 336 337 338 339
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) }
340
  | Clone (_,sm) -> known_clone uc.uc_known sm;
341 342 343 344 345
      { 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 *)
346

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

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
365
  let add uc (pr,_) = add_symbol add_pr pr.pr_name pr uc in
366 367
  List.fold_left add uc la

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

let create_decl d = mk_tdecl (Decl d)
371 372

let add_decl uc d =
373 374
  let uc = add_tdecl uc (create_decl d) in
  match d.d_node with
375 376 377 378 379
    | 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

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

382 383 384 385 386
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)

387 388 389 390 391 392 393 394 395 396 397
(** 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
398 399 400 401 402 403 404 405 406 407 408 409 410 411 412 413 414

(** 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
415
let create_inst ~ts ~ls ~lemma ~goal =
416 417 418 419 420 421 422
  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
423

424 425 426
exception CannotInstantiate of ident

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

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

(* populate the clone structure *)

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

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

let cl_find_ls cl ls =
454
  if not (Sid.mem ls.ls_name cl.cl_local) then ls
455
  else try Mls.find ls cl.ls_table
456 457 458
  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
459
    let ls' = create_lsymbol (id_clone ls.ls_name) ta' vt' in
460
    cl.ls_table <- Mls.add ls ls' cl.ls_table;
461 462
    ls'

463
let cl_trans_fmla cl f = t_s_map (cl_trans_ty cl) (cl_find_ls cl) f
464

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

(* 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
480
  if not (Sid.mem id cl.cl_local) then raise (NonLocal id);
481 482
  if List.length ts.ts_args <> List.length ts'.ts_args
    then raise (BadInstance (id, ts'.ts_name));
483
  cl.ts_table <- Mts.add ts ts' cl.ts_table
484 485 486

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

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

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 *)

515 516 517 518 519 520 521 522 523 524 525 526 527 528 529 530 531 532 533
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 [])
534 535

let extract_ls_defn f =
536
  let vl,_,f = match f.t_node with
537
    | Tquant (Tforall,b) -> t_open_quant b
538 539 540
    | _ -> [],[],f in
  match f.t_node with
    | Tapp (_, [{t_node = Tapp (ls,_)}; f])
541
    | Tbinop (_, {t_node = Tapp (ls,_)}, f) -> make_ls_defn ls vl f
542 543
    | _ -> assert false

544 545 546 547 548 549 550 551 552 553 554
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
555
  in
556
  create_logic_decl (List.fold_right add_logic ldl [])
557

558 559 560 561 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
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
590
  | MAty ty -> MAty (cl_trans_ty cl ty)
591 592 593
  | MAts ts -> MAts (cl_find_ts cl ts)
  | MAls ls -> MAls (cl_find_ls cl ls)
  | MApr pr -> MApr (cl_find_pr cl pr)
594 595
  | a -> a

596 597 598 599 600
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}

601 602 603
let cl_tdecl cl inst td = match td.td_node with
  | Decl d -> Decl (cl_decl cl inst d)
  | Use th -> Use th
604
  | Clone (th,sm) -> Clone (th, cl_smap cl sm)
605 606 607 608 609 610 611 612 613 614 615
  | 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
616 617 618 619 620 621
  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)))
622 623 624

let clone_export uc th inst =
  let cl = cl_init th inst in
625
  let uc = clone_theory cl add_tdecl uc th inst in
626

627 628 629 630 631 632 633 634
  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 = {
635 636 637 638
    ns_ts = Mstr.map f_ts (Mstr.filter g_ts ns.ns_ts);
    ns_ls = Mstr.map f_ls (Mstr.filter g_ls ns.ns_ls);
    ns_pr = Mstr.map f_pr ns.ns_pr;
    ns_ns = Mstr.map f_ns ns.ns_ns; } in
639 640

  let ns = f_ns th.th_export in
641 642 643 644

  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
645
        uc_export = merge_ns true  ns e0 :: ste; }
646 647 648 649 650 651 652
    | _ -> 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)

653
let create_null_clone th =
654 655 656 657 658 659 660 661 662 663 664
  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
665 666 667 668 669


(** Meta properties *)

let get_meta_arg_type = function
670
  | MAty  _ -> MTty
671 672 673 674 675 676
  | MAts  _ -> MTtysymbol
  | MAls  _ -> MTlsymbol
  | MApr  _ -> MTprsymbol
  | MAstr _ -> MTstring
  | MAint _ -> MTint

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

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

696 697
let clone_meta tdt sm = match tdt.td_node with
  | Meta (t,al) ->
698 699 700
      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
701
      let cl_marg = function
702
        | MAty ty -> MAty (ty_s_map find_ts ty)
703 704 705 706 707
        | MAts ts -> MAts (find_ts ts)
        | MAls ls -> MAls (find_ls ls)
        | MApr pr -> MApr (find_pr pr)
        | a -> a
      in
708
      mk_tdecl (Meta (t, List.map cl_marg al))
709
  | _ -> invalid_arg "clone_meta"
710

711 712 713 714 715 716 717 718 719 720 721 722 723 724 725 726
(** access to meta *)

(*
let theory_meta  = option_apply Mmeta.empty (fun t -> t.task_meta)

let find_meta_tds th (t : meta) = mm_find (theory_meta th) t

let on_meta meta fn acc theory =
  let add td acc = match td.td_node with
    | Meta (_,ma) -> fn acc ma
    | _ -> assert false
  in
  let tds = find_meta_tds theory meta in
  Stdecl.fold add tds.tds_set acc
*)

727
(*
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
728
let on_meta _meta fn acc theory =
729 730 731 732
  let tdecls = theory.th_decls in
  List.fold_left
    (fun acc td ->
       match td.td_node with
733 734
         | Meta (_,ma) -> fn acc ma
         | _ -> acc)
735
    acc tdecls
736
*)
737 738


739 740 741
(** Base theories *)

let builtin_theory =
742
  let uc = empty_theory (id_fresh "BuiltIn") [] in
743 744 745 746 747
  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

748 749 750 751 752 753 754 755
let create_theory ?(path=[]) n =
  use_export (empty_theory n path) builtin_theory

let bool_theory =
  let uc = empty_theory (id_fresh "Bool") [] in
  let uc = add_ty_decl uc [ts_bool, Talgebraic [fs_true; fs_false]] in
  close_theory uc

756
let highord_theory =
757
  let uc = empty_theory (id_fresh "HighOrd") [] in
758 759 760 761 762 763
  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

764
let tuple_theory = Util.memo_int 17 (fun n ->
765
  let uc = empty_theory (id_fresh ("Tuple" ^ string_of_int n)) [] in
766
  let uc = add_ty_decl uc [ts_tuple n, Talgebraic [fs_tuple n]] in
767
  close_theory uc)
768

769 770 771 772 773 774 775 776 777 778 779
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

780 781 782 783 784 785 786 787 788
let add_decl_with_tuples uc d =
  let ids = Mid.set_diff d.d_syms uc.uc_known 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 uc (tuple_theory n) in
  add_decl (Sint.fold add ixs uc) d

789 790
(* Exception reporting *)

791
let print_meta_arg_type fmt = function
792
  | MTty -> fprintf fmt "type"
793 794 795 796 797 798
  | MTtysymbol -> fprintf fmt "type_symbol"
  | MTlsymbol -> fprintf fmt "logic_symbol"
  | MTprsymbol -> fprintf fmt "proposition"
  | MTstring -> fprintf fmt "string"
  | MTint -> fprintf fmt "int"

799 800 801 802 803 804 805 806 807 808 809 810 811 812 813
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
814 815
  | UnknownMeta s ->
      Format.fprintf fmt "Unknown metaproperty %s" s
816
  | KnownMeta m ->
817
      Format.fprintf fmt "Metaproperty %s is already registered with \
818 819
        a conflicting signature" m.meta_name
  | BadMetaArity (m,i1,i2) ->
820
      Format.fprintf fmt "Metaproperty %s requires %d arguments but \
821 822
        is applied to %d" m.meta_name i1 i2
  | MetaTypeMismatch (m,t1,t2) ->
823
      Format.fprintf fmt "Metaproperty %s expects %a argument but \
824 825
        is applied to %a"
        m.meta_name print_meta_arg_type t1 print_meta_arg_type t2
826 827 828
  | _ -> raise exn
  end