decl.ml 21 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 29 30 31 32 33 34 35
(*    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
241
  Mls.mapi check syms
242

243 244
(** Inductive predicate declaration *)

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

Andrei Paskevich's avatar
Andrei Paskevich committed
249
module Prop = WeakStructMake (struct
250
  type t = prsymbol
251 252 253 254 255 256
  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
257
module Wpr = Prop.W
258

259
let pr_equal : prsymbol -> prsymbol -> bool = (==)
260

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

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

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

(** Proposition declaration *)

type prop_kind =
270 271 272 273
  | 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 *)
274

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

(** Declaration type *)

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

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

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

  type t = decl

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

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

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

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

  let equal d1 d2 = match d1.d_node, d2.d_node with
Andrei Paskevich's avatar
Andrei Paskevich committed
315 316 317
    | 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
318
    | Dprop (k1,pr1,f1), Dprop (k2,pr2,f2) ->
319
        k1 = k2 && pr_equal pr1 pr2 && f_equal f1 f2
320 321 322
    | _,_ -> false

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

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

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

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

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

  let hash d = match d.d_node with
337 338 339
    | 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
340
    | Dprop (k,pr,f) -> Hashcons.combine (hs_kind k) (hs_prop (pr,f))
341

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

344 345
end)

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

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

355
let d_equal : decl -> decl -> bool = (==)
356

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

359 360
(** Declaration constructors *)

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

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

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

376 377
exception NonPositiveTypeDecl of tysymbol * lsymbol * tysymbol

378
let news_id s id = Sid.add_new id (ClashIdent id) s
379

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

387 388
let create_ty_decl tdl =
  if tdl = [] then raise EmptyDecl;
389 390 391
  let add s (ts,_) = Sts.add ts s in
  let tss = List.fold_left add Sts.empty tdl in
  let check_constr tys ty (syms,news) fs =
392
    let vty = of_option fs.ls_value in
393
    if not (ty_equal ty vty) then raise (TypeMismatch (ty,vty));
394 395 396 397 398
    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
399
    let rec check seen s ty = match ty.ty_node with
400 401
      | Tyvar v when Stv.mem v vs -> s
      | Tyvar v -> raise (UnboundTypeVar v)
402 403 404 405 406 407 408
      | Tyapp (ts,_) ->
          let now = Sts.mem ts tss in
          if seen && now then
            raise (NonPositiveTypeDecl (tys,fs,ts))
          else
            let s = ty_fold (check (seen || now)) s ty in
            Sid.add ts.ts_name s
409
    in
410
    let syms = List.fold_left (check false) syms fs.ls_args in
411
    syms, news_id news fs.ls_name
412
  in
413 414 415 416
  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
417
    | Talgebraic cl ->
418
        if cl = [] then raise (EmptyAlgDecl ts);
419
        if ts.ts_def <> None then raise (IllegalTypeAlias ts);
420
        let news = news_id news ts.ts_name in
421
        let ty = ty_app ts (List.map ty_var ts.ts_args) in
422
        List.fold_left (check_constr ts ty) (syms,news) cl
423
  in
424
  let (syms,news) = List.fold_left check_decl (Sid.empty,Sid.empty) tdl in
425
  mk_decl (Dtype tdl) syms news
426 427 428

let create_logic_decl ldl =
  if ldl = [] then raise EmptyDecl;
429
  let check_decl (syms,news) (ls,ld) = match ld with
430
    | Some (s,_) when not (ls_equal s ls) ->
431
        raise (BadLogicDecl (ls, s))
432 433 434 435 436 437
    | 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
438
  in
439
  let (syms,news) = List.fold_left check_decl (Sid.empty,Sid.empty) ldl in
440
  ignore (check_termination ldl);
441
  mk_decl (Dlogic ldl) syms news
442

443 444 445
exception InvalidIndDecl of lsymbol * prsymbol
exception TooSpecificIndDecl of lsymbol * prsymbol * term
exception NonPositiveIndDecl of lsymbol * prsymbol * lsymbol
446 447 448 449 450 451 452 453 454 455 456 457 458 459 460 461 462 463 464 465 466 467

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
468
  let check_ax ps (syms,news) (pr,f) =
469
    let rec clause acc f = match f.f_node with
470 471
      | Fquant (Fforall, f) ->
          let _,_,f = f_open_quant f in clause acc f
472 473 474
      | Fbinop (Fimplies, g, f) -> clause (g::acc) f
      | _ -> (acc, f)
    in
475
    let cls, f = clause [] (check_fvs f) in
476
    match f.f_node with
477
      | Fapp (s, tl) when ls_equal s ps ->
478 479
          let mtch t ty =
            if not (ty_equal t.t_ty ty) then
480 481
              raise (TooSpecificIndDecl (ps, pr, t))
          in
482
          List.iter2 mtch tl ps.ls_args;
483
          (try ignore (List.for_all (f_pos_ps sps (Some true)) cls)
484 485
          with Found ls -> raise (NonPositiveIndDecl (ps, pr, ls)));
          syms_fmla syms f, news_id news pr.pr_name
486 487
      | _ -> raise (InvalidIndDecl (ps, pr))
  in
488 489 490 491
  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
492
  in
493
  let (syms,news) = List.fold_left check_decl (Sid.empty,Sid.empty) idl in
494
  mk_decl (Dind idl) syms news
495

496 497 498
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
499
  mk_decl (Dprop (k,p,check_fvs f)) syms news
500

501 502 503 504 505 506 507 508 509 510 511 512 513 514 515 516 517 518 519 520
(** 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)

521 522 523 524 525 526 527 528 529 530 531 532 533 534
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
535 536
  | Dprop (_,_,f) ->
      fnF acc f
537

538 539 540 541 542 543 544 545 546 547 548 549 550 551 552 553 554 555 556 557 558 559 560
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

561

Andrei Paskevich's avatar
Andrei Paskevich committed
562 563 564 565 566 567
(** Known identifiers *)

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

568
type known_map = decl Mid.t
Andrei Paskevich's avatar
Andrei Paskevich committed
569 570 571 572 573

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

let merge_known kn1 kn2 =
574
  let check_known id decl1 decl2 =
575 576 577
    if d_equal decl1 decl2 then Some decl1
    else raise (RedeclaredIdent id)
  in
578
  Mid.union check_known kn1 kn2
Andrei Paskevich's avatar
Andrei Paskevich committed
579

580
let known_add_decl kn0 decl =
581 582 583 584 585
  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)
586
  in
587 588 589 590
  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
591

592 593 594
let find_constructors kn ts =
  match (Mid.find ts.ts_name kn).d_node with
  | Dtype dl ->
595
      begin match List.assq ts dl with
596 597 598 599 600 601 602
        | Talgebraic cl -> cl
        | Tabstract -> []
      end
  | _ -> assert false

let find_inductive_cases kn ps =
  match (Mid.find ps.ls_name kn).d_node with
603
  | Dind dl -> List.assq ps dl
604
  | Dlogic _ -> []
605 606 607 608 609 610 611 612
  | Dtype _ -> []
  | _ -> assert false

let find_logic_definition kn ls =
  match (Mid.find ls.ls_name kn).d_node with
  | Dlogic dl -> List.assq ls dl
  | Dind _ -> None
  | Dtype _ -> None
613
  | _ -> assert false
614 615 616 617 618 619

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))
620
  | Dprop (_,_,f) -> f
621
  | _ -> assert false
622

623 624
let find_prop_decl kn pr =
  match (Mid.find pr.pr_name kn).d_node with
625
  | Dind dl ->
626
      let test (_,l) = List.mem_assq pr l in
627
      Paxiom, List.assq pr (snd (List.find test dl))
628 629 630
  | Dprop (k,_,f) -> k,f
  | _ -> assert false

631 632 633
exception NonExhaustiveExpr of (pattern list * expr)

let rec check_matchT kn () t = match t.t_node with
Andrei Paskevich's avatar
Andrei Paskevich committed
634 635 636
  | 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
637 638
      with Pattern.NonExhaustive p -> raise (NonExhaustiveExpr (p,Term t)));
      t_fold (check_matchT kn) (check_matchF kn) () t
639 640 641
  | _ -> 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
642 643 644
  | 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
645 646
      with Pattern.NonExhaustive p -> raise (NonExhaustiveExpr (p,Fmla f)));
      f_fold (check_matchT kn) (check_matchF kn) () f
647 648 649 650
  | _ -> f_fold (check_matchT kn) (check_matchF kn) () f

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

651 652 653 654 655 656 657 658 659 660 661 662 663 664 665 666 667 668 669 670 671 672 673 674 675 676 677
exception NonFoundedTypeDecl of tysymbol

let rec check_foundness kn d =
  let rec check_constr s ty ls =
    let vty = of_option ls.ls_value in
    let m = ty_match Mtv.empty vty ty in
    let check ty = check_type s (ty_inst m ty) in
    List.for_all check ls.ls_args
  and check_type s ty = match ty.ty_node with
    | Tyvar _ -> true
    | Tyapp (ts,_) ->
        if Sts.mem ts s then false else
        let cl = find_constructors kn ts in
        if cl == [] then true else
        let s = Sts.add ts s in
        List.exists (check_constr s ty) cl
  in
  match d.d_node with
  | Dtype tdl ->
      let check () (ts,_) =
        let tl = List.map ty_var ts.ts_args in
        if check_type Sts.empty (ty_app ts tl)
        then () else raise (NonFoundedTypeDecl ts)
      in
      List.fold_left check () tdl
  | _ -> ()

678
let known_add_decl kn d =
679
  let kn = known_add_decl kn d in
680 681
  check_foundness kn d;
  check_match kn d;
Andrei Paskevich's avatar
Andrei Paskevich committed
682 683
  kn