decl.ml 19.7 KB
Newer Older
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35
(**************************************************************************)
(*                                                                        *)
(*  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.                  *)
(*                                                                        *)
(**************************************************************************)

open Format
open Util
open Ident
open Ty
open Term

(** Type declaration *)

type ty_def =
  | Tabstract
  | Talgebraic of lsymbol list

type ty_decl = tysymbol * ty_def

(** Logic declaration *)

36
type ls_defn = lsymbol * fmla
37 38 39

type logic_decl = lsymbol * ls_defn option

40
exception UnboundVar of vsymbol
41 42 43

let check_fvs f =
  let fvs = f_freevars Svs.empty f in
44 45
  Svs.iter (fun vs -> raise (UnboundVar vs)) fvs;
  f
46 47 48

let make_fs_defn fs vl t =
  let hd = t_app fs (List.map t_var vl) t.t_ty in
49
  let fd = f_forall_close vl [] (f_equ hd t) in
50
  fs, Some (fs, check_fvs fd)
51 52 53

let make_ps_defn ps vl f =
  let hd = f_app ps (List.map t_var vl) in
54
  let pd = f_forall_close vl [] (f_iff hd f) in
55
  ps, Some (ps, check_fvs pd)
56 57 58

let make_ls_defn ls vl = e_apply (make_fs_defn ls vl) (make_ps_defn ls vl)

Andrei Paskevich's avatar
minor  
Andrei Paskevich committed
59
let open_ls_defn (_,f) =
60 61
  let vl, ef = f_open_forall f in
  match ef.f_node with
62 63
    | Fapp (_, [_; t2]) -> vl, Term t2
    | Fbinop (_, _, f2) -> vl, Fmla f2
64 65
    | _ -> assert false

Andrei Paskevich's avatar
minor  
Andrei Paskevich committed
66
let open_fs_defn ld = let vl,e = open_ls_defn ld in
67
  match e with Term t -> vl,t | _ -> assert false
68

Andrei Paskevich's avatar
minor  
Andrei Paskevich committed
69
let open_ps_defn ld = let vl,e = open_ls_defn ld in
70
  match e with Fmla f -> vl,f | _ -> assert false
71

72
let ls_defn_axiom (_,f) = f
73

74 75
(** Termination checking for mutually recursive logic declarations *)

76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115
type descent =
  | Less of int
  | Equal of int
  | Unknown

let rec match_var link acc p = match p.pat_node with
  | Pwild -> acc
  | Pvar u -> List.rev_map (Mvs.add u link) acc
  | Pas (p,u) -> List.rev_map (Mvs.add u link) (match_var link acc p)
  | Por (p1,p2) ->
      let acc1 = match_var link acc p1 in
      let acc2 = match_var link acc p2 in
      List.rev_append acc1 acc2
  | Papp _ ->
      let link = match link with
        | Unknown -> Unknown
        | Equal i -> Less i
        | Less i  -> Less i
      in
      let join u = Mvs.add u link in
      List.rev_map (Svs.fold join p.pat_vars) acc

let rec match_term vm t acc p = match t.t_node, p.pat_node with
  | _, Pwild -> acc
  | Tvar v, _ when not (Mvs.mem v vm) -> acc
  | Tvar v, _ -> match_var (Mvs.find v vm) acc p
  | Tapp _, Pvar _ -> acc
  | Tapp _, Pas (p,_) -> match_term vm t acc p
  | Tapp _, Por (p1,p2) ->
      let acc1 = match_term vm t acc p1 in
      let acc2 = match_term vm t acc p2 in
      List.rev_append acc1 acc2
  | Tapp (c1,tl), Papp (c2,pl) when ls_equal c1 c2 ->
      let down l t p = match_term vm t l p in
      List.fold_left2 down acc tl pl
  | _,_ -> acc

let build_call_graph cgr syms ls =
  let call vm s tl =
    let desc t = match t.t_node with
116
      | Tvar v -> Mvs.find_default v Unknown vm
117
      | _ -> Unknown
118
    in
119
    Hls.add cgr s (ls, Array.of_list (List.map desc tl))
120
  in
121 122 123
  let rec term vm () t = match t.t_node with
    | Tapp (s,tl) when Mls.mem s syms ->
        t_fold (term vm) (fmla vm) () t; call vm s tl
124 125
    | Tlet ({t_node = Tvar v}, b) when Mvs.mem v vm ->
        let u,e = t_open_bound b in
126
        term (Mvs.add u (Mvs.find v vm) vm) () e
127
    | Tcase (e,bl) ->
128
        term vm () e; List.iter (fun b ->
129
          let p,t = t_open_branch b in
130 131 132 133 134 135
          let vml = match_term vm e [vm] p in
          List.iter (fun vm -> term vm () t) vml) bl
    | _ -> t_fold (term vm) (fmla vm) () t
  and fmla vm () f = match f.f_node with
    | Fapp (s,tl) when Mls.mem s syms ->
        f_fold (term vm) (fmla vm) () f; call vm s tl
136 137
    | Flet ({t_node = Tvar v}, b) when Mvs.mem v vm ->
        let u,e = f_open_bound b in
138
        fmla (Mvs.add u (Mvs.find v vm) vm) () e
139
    | Fcase (e,bl) ->
140
        term vm () e; List.iter (fun b ->
141
          let p,f = f_open_branch b in
142 143
          let vml = match_term vm e [vm] p in
          List.iter (fun vm -> fmla vm () f) vml) bl
144
    | Fquant (_,b) ->
145 146
        let _,_,f = f_open_quant b in fmla vm () f
    | _ -> f_fold (term vm) (fmla vm) () f
147
  in
148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197
  fun (vl,e) ->
    let i = ref (-1) in
    let add vm v = incr i; Mvs.add v (Equal !i) vm in
    let vm = List.fold_left add Mvs.empty vl in
    e_apply (term vm ()) (fmla vm ()) e

let build_call_list cgr ls =
  let htb = Hls.create 5 in
  let local v = Array.mapi (fun i -> function
    | (Less j) as d when i = j -> d
    | (Equal j) as d when i = j -> d
    | _ -> Unknown) v
  in
  let subsumes v1 v2 =
    let sbs d1 d2 = match d1,d2 with
      | _, Unknown -> ()
      | Equal u1, Equal u2 when u1 = u2 -> ()
      | Less  u1, Equal u2 when u1 = u2 -> ()
      | Less  u1, Less  u2 when u1 = u2 -> ()
      | _,_ -> raise Not_found
    in
    let test i d1 = sbs d1 (Array.get v2 i) in
    try Array.iteri test v1; true with Not_found -> false
  in
  let subsumed s c =
    List.exists (subsumes c) (Hls.find_all htb s)
  in
  let multiply v1 v2 =
    let to_less = function
      | Unknown -> Unknown
      | Equal i -> Less i
      | Less i  -> Less i
    in
    Array.map (function
      | Unknown -> Unknown
      | Equal i -> Array.get v2 i
      | Less i -> to_less (Array.get v2 i)) v1
  in
  let resolve s c =
    Hls.add htb s c;
    let mult (s,v) = (s, multiply c v) in
    List.rev_map mult (Hls.find_all cgr s)
  in
  let rec add_call lc = function
    | [] -> lc
    | (s,c)::r when ls_equal ls s -> add_call (local c :: lc) r
    | (s,c)::r when subsumed s c -> add_call lc r
    | (s,c)::r -> add_call lc (List.rev_append (resolve s c) r)
  in
  add_call [] (Hls.find_all cgr ls)
198 199 200

exception NoTerminationProof of lsymbol

201 202 203 204 205 206 207 208 209 210 211 212 213 214 215 216 217 218 219 220 221 222 223 224 225 226 227
let check_call_list ls cl =
  let add d1 d2 = match d1, d2 with
    | Unknown, _ -> d1
    | _, Unknown -> d2
    | Less _, _  -> d1
    | _, Less _  -> d2
    | _, _ -> d1
  in
  let add v1 v2 =
    Array.mapi (fun i d1 -> add d1 (Array.get v2 i)) v1
  in
  let rec check acc mx = match mx with
    | [] -> List.rev acc
    | a :: r ->
        (* calculate the bitwise minimum of all call vectors *)
        let p = List.fold_left add a r in
        (* find the decreasing argument positions *)
        let find l = function Less i -> i :: l | _ -> l in
        let res = Array.fold_left find [] p in
        (* eliminate the decreasing calls *)
        if res = [] then raise (NoTerminationProof ls);
        let test a =
          List.for_all (fun i -> Array.get a i <> Less i) res
        in
        check (List.rev_append res acc) (List.filter test mx)
  in
  check [] cl
228 229

let check_termination ldl =
230
  let cgr = Hls.create 5 in
231 232 233 234
  let add acc (ls,ld) = match ld with
    | Some ld -> Mls.add ls (open_ls_defn ld) acc
    | None -> acc
  in
235 236
  let syms = List.fold_left add Mls.empty ldl in
  Mls.iter (build_call_graph cgr syms) syms;
237
  let check ls _ =
238
    let cl = build_call_list cgr ls in
239 240
    check_call_list ls cl in
  Mls.mapi check syms
241

242 243
(** Inductive predicate declaration *)

244
type prsymbol = {
245 246
  pr_name : ident;
}
247

Andrei Paskevich's avatar
Andrei Paskevich committed
248
module Prop = WeakStructMake (struct
249
  type t = prsymbol
250 251 252 253 254 255
  let tag pr = pr.pr_name.id_tag
end)

module Spr = Prop.S
module Mpr = Prop.M
module Hpr = Prop.H
Andrei Paskevich's avatar
Andrei Paskevich committed
256
module Wpr = Prop.W
257

258
let pr_equal = (==)
259

Andrei Paskevich's avatar
Andrei Paskevich committed
260 261
let pr_hash pr = id_hash pr.pr_name

262
let create_prsymbol n = { pr_name = id_register n }
263

264
type ind_decl = lsymbol * (prsymbol * fmla) list
265 266 267 268

(** Proposition declaration *)

type prop_kind =
269 270 271 272
  | Plemma    (* prove, use as a premise *)
  | Paxiom    (* do not prove, use as a premise *)
  | Pgoal     (* prove, do not use as a premise *)
  | Pskip     (* do not prove, do not use as a premise *)
273

274
type prop_decl = prop_kind * prsymbol * fmla
275 276 277 278 279

(** Declaration type *)

type decl = {
  d_node : decl_node;
280 281
  d_syms : Sid.t;         (* idents used in declaration *)
  d_news : Sid.t;         (* idents introduced in declaration *)
Andrei Paskevich's avatar
Andrei Paskevich committed
282
  d_tag  : Hashweak.tag;  (* unique magical tag *)
283 284 285 286 287 288 289 290 291 292
}

and decl_node =
  | Dtype  of ty_decl list      (* recursive types *)
  | Dlogic of logic_decl list   (* recursive functions/predicates *)
  | Dind   of ind_decl list     (* inductive predicates *)
  | Dprop  of prop_decl         (* axiom / lemma / goal *)

(** Declarations *)

293
module Hsdecl = Hashcons.Make (struct
294 295 296

  type t = decl

297
  let eq_td (ts1,td1) (ts2,td2) = ts_equal ts1 ts2 && match td1,td2 with
298
    | Tabstract, Tabstract -> true
299
    | Talgebraic l1, Talgebraic l2 -> list_all2 ls_equal l1 l2
300 301
    | _ -> false

302 303
  let eq_ld (ls1,ld1) (ls2,ld2) = ls_equal ls1 ls2 && match ld1,ld2 with
    | Some (_,f1), Some (_,f2) -> f_equal f1 f2
304 305 306
    | None, None -> true
    | _ -> false

307 308
  let eq_iax (pr1,fr1) (pr2,fr2) =
    pr_equal pr1 pr2 && f_equal fr1 fr2
309

310 311
  let eq_ind (ps1,al1) (ps2,al2) =
    ls_equal ps1 ps2 && list_all2 eq_iax al1 al2
312 313

  let equal d1 d2 = match d1.d_node, d2.d_node with
Andrei Paskevich's avatar
Andrei Paskevich committed
314 315 316
    | Dtype  l1, Dtype  l2 -> list_all2 eq_td l1 l2
    | Dlogic l1, Dlogic l2 -> list_all2 eq_ld l1 l2
    | Dind   l1, Dind   l2 -> list_all2 eq_ind l1 l2
317
    | Dprop (k1,pr1,f1), Dprop (k2,pr2,f2) ->
318
        k1 = k2 && pr_equal pr1 pr2 && f_equal f1 f2
319 320 321
    | _,_ -> false

  let hs_td (ts,td) = match td with
Andrei Paskevich's avatar
Andrei Paskevich committed
322 323
    | Tabstract -> ts_hash ts
    | Talgebraic l -> 1 + Hashcons.combine_list ls_hash (ts_hash ts) l
324

Andrei Paskevich's avatar
Andrei Paskevich committed
325 326
  let hs_ld (ls,ld) = Hashcons.combine (ls_hash ls)
    (Hashcons.combine_option (fun (_,f) -> f_hash f) ld)
327

Andrei Paskevich's avatar
Andrei Paskevich committed
328
  let hs_prop (pr,f) = Hashcons.combine (pr_hash pr) (f_hash f)
329

Andrei Paskevich's avatar
Andrei Paskevich committed
330
  let hs_ind (ps,al) = Hashcons.combine_list hs_prop (ls_hash ps) al
331 332

  let hs_kind = function
333
    | Plemma -> 11 | Paxiom -> 13 | Pgoal  -> 17 | Pskip  -> 19
334 335

  let hash d = match d.d_node with
336 337 338
    | Dtype  l -> Hashcons.combine_list hs_td 3 l
    | Dlogic l -> Hashcons.combine_list hs_ld 5 l
    | Dind   l -> Hashcons.combine_list hs_ind 7 l
339
    | Dprop (k,pr,f) -> Hashcons.combine (hs_kind k) (hs_prop (pr,f))
340

Andrei Paskevich's avatar
Andrei Paskevich committed
341
  let tag n d = { d with d_tag = Hashweak.create_tag n }
342

343 344
end)

Andrei Paskevich's avatar
Andrei Paskevich committed
345
module Decl = WeakStructMake (struct
346 347 348
  type t = decl
  let tag d = d.d_tag
end)
349

350 351
module Sdecl = Decl.S
module Mdecl = Decl.M
Andrei Paskevich's avatar
Andrei Paskevich committed
352
module Wdecl = Decl.W
353

354 355
let d_equal = (==)

Andrei Paskevich's avatar
Andrei Paskevich committed
356 357
let d_hash d = Hashweak.tag_hash d.d_tag

358 359
(** Declaration constructors *)

360
let mk_decl node syms news = Hsdecl.hashcons {
361 362 363
  d_node = node;
  d_syms = syms;
  d_news = news;
Andrei Paskevich's avatar
Andrei Paskevich committed
364
  d_tag  = Hashweak.dummy_tag;
365
}
366 367 368

exception IllegalTypeAlias of tysymbol
exception ClashIdent of ident
369
exception BadLogicDecl of lsymbol * lsymbol
370

371
exception EmptyDecl
372 373
exception EmptyAlgDecl of tysymbol
exception EmptyIndDecl of lsymbol
374

375 376
let news_id s id = Sid.change id (fun there ->
  if there then raise (ClashIdent id) else true) s
377

378 379 380 381 382 383 384
let syms_ts s ts = Sid.add ts.ts_name s
let syms_ls s ls = Sid.add ls.ls_name s

let syms_ty s ty = ty_s_fold syms_ts s ty
let syms_term s t = t_s_fold syms_ts syms_ls s t
let syms_fmla s f = f_s_fold syms_ts syms_ls s f

385 386
let create_ty_decl tdl =
  if tdl = [] then raise EmptyDecl;
387
  let check_constr ty (syms,news) fs =
388
    let vty = of_option fs.ls_value in
389
    ignore (ty_match Mtv.empty vty ty);
390 391 392 393 394
    let add s ty = match ty.ty_node with
      | Tyvar v -> Stv.add v s
      | _ -> assert false
    in
    let vs = ty_fold add Stv.empty vty in
395
    let rec check s ty = match ty.ty_node with
396 397 398
      | Tyvar v when Stv.mem v vs -> s
      | Tyvar v -> raise (UnboundTypeVar v)
      | Tyapp (ts,_) -> Sid.add ts.ts_name (ty_fold check s ty)
399
    in
400 401
    let syms = List.fold_left check syms fs.ls_args in
    syms, news_id news fs.ls_name
402
  in
403 404 405 406
  let check_decl (syms,news) (ts,td) = match td with
    | Tabstract ->
        let syms = option_apply syms (syms_ty syms) ts.ts_def in
        syms, news_id news ts.ts_name
407
    | Talgebraic cl ->
408
        if cl = [] then raise (EmptyAlgDecl ts);
409
        if ts.ts_def <> None then raise (IllegalTypeAlias ts);
410
        let news = news_id news ts.ts_name in
411
        let ty = ty_app ts (List.map ty_var ts.ts_args) in
412
        List.fold_left (check_constr ty) (syms,news) cl
413
  in
414
  let (syms,news) = List.fold_left check_decl (Sid.empty,Sid.empty) tdl in
415
  mk_decl (Dtype tdl) syms news
416 417 418

let create_logic_decl ldl =
  if ldl = [] then raise EmptyDecl;
419
  let check_decl (syms,news) (ls,ld) = match ld with
420
    | Some (s,_) when not (ls_equal s ls) ->
421
        raise (BadLogicDecl (ls, s))
422 423 424 425 426 427
    | Some (_,f) ->
        syms_fmla syms f, news_id news ls.ls_name
    | None ->
        let syms = option_apply syms (syms_ty syms) ls.ls_value in
        let syms = List.fold_left syms_ty syms ls.ls_args in
        syms, news_id news ls.ls_name
428
  in
429
  let (syms,news) = List.fold_left check_decl (Sid.empty,Sid.empty) ldl in
430
  (* ignore (check_termination ldl); *)
431
  mk_decl (Dlogic ldl) syms news
432

433 434 435
exception InvalidIndDecl of lsymbol * prsymbol
exception TooSpecificIndDecl of lsymbol * prsymbol * term
exception NonPositiveIndDecl of lsymbol * prsymbol * lsymbol
436 437 438 439 440 441 442 443 444 445 446 447 448 449 450 451 452 453 454 455 456 457

exception Found of lsymbol
let ls_mem s sps = if Sls.mem s sps then raise (Found s) else false
let t_pos_ps sps = t_s_all (fun _ -> true) (fun s -> not (ls_mem s sps))

let rec f_pos_ps sps pol f = match f.f_node, pol with
  | Fapp (s, _), Some false when ls_mem s sps -> false
  | Fapp (s, _), None when ls_mem s sps -> false
  | Fbinop (Fiff, f, g), _ ->
      f_pos_ps sps None f && f_pos_ps sps None g
  | Fbinop (Fimplies, f, g), _ ->
      f_pos_ps sps (option_map not pol) f && f_pos_ps sps pol g
  | Fnot f, _ ->
      f_pos_ps sps (option_map not pol) f
  | Fif (f,g,h), _ ->
      f_pos_ps sps None f && f_pos_ps sps pol g && f_pos_ps sps pol h
  | _ -> f_all (t_pos_ps sps) (f_pos_ps sps pol) f

let create_ind_decl idl =
  if idl = [] then raise EmptyDecl;
  let add acc (ps,_) = Sls.add ps acc in
  let sps = List.fold_left add Sls.empty idl in
458
  let check_ax ps (syms,news) (pr,f) =
459
    let rec clause acc f = match f.f_node with
460 461
      | Fquant (Fforall, f) ->
          let _,_,f = f_open_quant f in clause acc f
462 463 464
      | Fbinop (Fimplies, g, f) -> clause (g::acc) f
      | _ -> (acc, f)
    in
465
    let cls, f = clause [] (check_fvs f) in
466
    match f.f_node with
467
      | Fapp (s, tl) when ls_equal s ps ->
468
          let mtch sb t ty =
469
            try ty_match sb (t.t_ty) ty with TypeMismatch _ ->
470 471
              raise (TooSpecificIndDecl (ps, pr, t))
          in
472
          ignore (List.fold_left2 mtch Mtv.empty tl ps.ls_args);
473
          (try ignore (List.for_all (f_pos_ps sps (Some true)) cls)
474 475
          with Found ls -> raise (NonPositiveIndDecl (ps, pr, ls)));
          syms_fmla syms f, news_id news pr.pr_name
476 477
      | _ -> raise (InvalidIndDecl (ps, pr))
  in
478 479 480 481
  let check_decl (syms,news) (ps,al) =
    if al = [] then raise (EmptyIndDecl ps);
    let news = news_id news ps.ls_name in
    List.fold_left (check_ax ps) (syms,news) al
482
  in
483
  let (syms,news) = List.fold_left check_decl (Sid.empty,Sid.empty) idl in
484
  mk_decl (Dind idl) syms news
485

486 487 488
let create_prop_decl k p f =
  let syms = syms_fmla Sid.empty f in
  let news = news_id Sid.empty p.pr_name in
489
  mk_decl (Dprop (k,p,check_fvs f)) syms news
490

491 492 493 494 495 496 497 498 499 500 501 502 503 504 505 506 507 508 509 510
(** Utilities *)

let decl_map fnT fnF d = match d.d_node with
  | Dtype _ ->
      d
  | Dlogic l ->
      let fn = function
        | ls, Some ld ->
            let vl,e = open_ls_defn ld in
            make_ls_defn ls vl (e_map fnT fnF e)
        | ld -> ld
      in
      create_logic_decl (List.map fn l)
  | Dind l ->
      let fn (pr,f) = pr, fnF f in
      let fn (ps,l) = ps, List.map fn l in
      create_ind_decl (List.map fn l)
  | Dprop (k,pr,f) ->
      create_prop_decl k pr (fnF f)

511 512 513 514 515 516 517 518 519 520 521 522 523 524
let decl_fold fnT fnF acc d = match d.d_node with
  | Dtype _ -> acc
  | Dlogic l ->
      let fn acc = function
        | _, Some ld ->
            let _,e = open_ls_defn ld in
            e_fold fnT fnF acc e
        | _ -> acc
      in
      List.fold_left fn acc l
  | Dind l ->
      let fn acc (_,f) = fnF acc f in
      let fn acc (_,l) = List.fold_left fn acc l in
      List.fold_left fn acc l
525 526
  | Dprop (_,_,f) ->
      fnF acc f
527

528 529 530 531 532 533 534 535 536 537 538 539 540 541 542 543 544 545 546 547 548 549 550
let rpair_map_fold f acc (x1,x2) =
  let acc, x2 = f acc x2 in
  acc, (x1, x2)

let list_rpair_map_fold f =
  Util.map_fold_left (rpair_map_fold f)

let decl_map_fold fnT fnF acc d =
  match d.d_node with
  | Dtype _ -> acc, d
  | Dprop (k,pr,f) ->
      let acc, f = f_map_fold fnT fnF acc f in
      acc, create_prop_decl k pr f
  | Dind l ->
      let acc, l =
        list_rpair_map_fold (list_rpair_map_fold (f_map_fold fnT fnF)) acc l in
      acc, create_ind_decl l
  | Dlogic l ->
      let acc, l =
      list_rpair_map_fold (option_map_fold
        (rpair_map_fold (f_map_fold fnT fnF))) acc l in
      acc, create_logic_decl l

551

Andrei Paskevich's avatar
Andrei Paskevich committed
552 553 554 555 556 557
(** Known identifiers *)

exception KnownIdent of ident
exception UnknownIdent of ident
exception RedeclaredIdent of ident

558
type known_map = decl Mid.t
Andrei Paskevich's avatar
Andrei Paskevich committed
559 560 561 562 563

let known_id kn id =
  if not (Mid.mem id kn) then raise (UnknownIdent id)

let merge_known kn1 kn2 =
564
  let check_known id decl1 decl2 =
565 566 567
    if d_equal decl1 decl2 then Some decl1
    else raise (RedeclaredIdent id)
  in
568
  Mid.union check_known kn1 kn2
Andrei Paskevich's avatar
Andrei Paskevich committed
569

570
let known_add_decl kn0 decl =
571 572 573 574 575
  let kn = Mid.map (fun _ -> decl) decl.d_news in
  let check id decl0 _ =
    if d_equal decl0 decl
    then raise (KnownIdent id)
    else raise (RedeclaredIdent id)
576
  in
577 578 579 580
  let kn = Mid.union check kn0 kn in
  let unk = Mid.diff (fun _ _ _ -> None) decl.d_syms kn in
  if Sid.is_empty unk then kn
  else raise (UnknownIdent (Sid.choose unk))
Andrei Paskevich's avatar
Andrei Paskevich committed
581

582 583 584
let find_constructors kn ts =
  match (Mid.find ts.ts_name kn).d_node with
  | Dtype dl ->
585
      begin match List.assq ts dl with
586 587 588 589 590 591 592
        | Talgebraic cl -> cl
        | Tabstract -> []
      end
  | _ -> assert false

let find_inductive_cases kn ps =
  match (Mid.find ps.ls_name kn).d_node with
593
  | Dind dl -> List.assq ps dl
594 595
  | Dlogic _ -> []
  | _ -> assert false
596 597 598 599 600 601

let find_prop kn pr =
  match (Mid.find pr.pr_name kn).d_node with
  | Dind dl ->
      let test (_,l) = List.mem_assq pr l in
      List.assq pr (snd (List.find test dl))
602
  | Dprop (_,_,f) -> f
603
  | _ -> assert false
604

605 606
let find_prop_decl kn pr =
  match (Mid.find pr.pr_name kn).d_node with
607
  | Dind dl ->
608
      let test (_,l) = List.mem_assq pr l in
609
      Paxiom, List.assq pr (snd (List.find test dl))
610 611 612
  | Dprop (k,_,f) -> k,f
  | _ -> assert false

613 614 615
exception NonExhaustiveExpr of (pattern list * expr)

let rec check_matchT kn () t = match t.t_node with
Andrei Paskevich's avatar
Andrei Paskevich committed
616 617 618
  | Tcase (t1,bl) ->
      let bl = List.map (fun b -> let p,t = t_open_branch b in [p],t) bl in
      ignore (try Pattern.CompileTerm.compile (find_constructors kn) [t1] bl
619 620
      with Pattern.NonExhaustive p -> raise (NonExhaustiveExpr (p,Term t)));
      t_fold (check_matchT kn) (check_matchF kn) () t
621 622 623
  | _ -> t_fold (check_matchT kn) (check_matchF kn) () t

and check_matchF kn () f = match f.f_node with
Andrei Paskevich's avatar
Andrei Paskevich committed
624 625 626
  | Fcase (t1,bl) ->
      let bl = List.map (fun b -> let p,f = f_open_branch b in [p],f) bl in
      ignore (try Pattern.CompileFmla.compile (find_constructors kn) [t1] bl
627 628
      with Pattern.NonExhaustive p -> raise (NonExhaustiveExpr (p,Fmla f)));
      f_fold (check_matchT kn) (check_matchF kn) () f
629 630 631 632
  | _ -> f_fold (check_matchT kn) (check_matchF kn) () f

let check_match kn d = decl_fold (check_matchT kn) (check_matchF kn) () d

633
let known_add_decl kn d =
634
  let kn = known_add_decl kn d in
635
  ignore (check_match kn d);
Andrei Paskevich's avatar
Andrei Paskevich committed
636 637
  kn