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

28
type ty_defn =
29 30 31
  | Tabstract
  | Talgebraic of lsymbol list

32
type ty_decl = tysymbol * ty_defn
33 34 35

(** Logic declaration *)

36
type ls_defn = lsymbol * term
37 38 39

type logic_decl = lsymbol * ls_defn option

40
exception UnboundVar of vsymbol
41 42

let check_fvs f =
43 44
  Mvs.iter (fun vs _ -> raise (UnboundVar vs)) f.t_vars;
  t_prop f
45

46 47
let check_vl ty v = ty_equal_check ty v.vs_ty
let check_tl ty t = ty_equal_check ty (t_type t)
48

49
let make_ls_defn ls vl t =
50 51 52
  (* check for duplicate arguments *)
  let add_v s v = Svs.add_new v (DuplicateVar v) s in
  ignore (List.fold_left add_v Svs.empty vl);
53
  (* build the definition axiom *)
54
  let hd = t_app ls (List.map t_var vl) t.t_ty in
55 56 57 58 59 60 61 62
  let bd = TermTF.t_selecti t_equ t_iff hd t in
  let fd = check_fvs (t_forall_close vl [] bd) in
  (* check for unbound type variables *)
  let htv = t_ty_freevars Stv.empty hd in
  let ttv = t_ty_freevars Stv.empty t in
  if not (Stv.subset ttv htv) then
    raise (UnboundTypeVar (Stv.choose (Stv.diff ttv htv)));
  (* check correspondence with the type signature of ls *)
63 64
  List.iter2 check_vl ls.ls_args vl;
  t_ty_check t ls.ls_value;
65 66
  (* return the definition *)
  ls, Some (ls, fd)
67

Andrei Paskevich's avatar
minor  
Andrei Paskevich committed
68
let open_ls_defn (_,f) =
69
  let vl,_,f = match f.t_node with
70
    | Tquant (Tforall,b) -> t_open_quant b
71 72 73
    | _ -> [],[],f in
  match f.t_node with
    | Tapp (_, [_; f])
74
    | Tbinop (_, _, f) -> vl,f
75 76
    | _ -> assert false

77 78 79 80 81 82 83 84 85
let open_ls_defn_cb ld =
  let ls,_ = ld in
  let vl,t = open_ls_defn ld in
  let close ls' vl' t' =
    if t_equal t t' && list_all2 vs_equal vl vl' && ls_equal ls ls'
    then ls, Some ld else make_ls_defn ls' vl' t'
  in
  vl,t,close

86
let ls_defn_axiom (_,f) = f
87

88 89
(** Termination checking for mutually recursive logic declarations *)

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 116 117 118 119 120 121 122 123 124 125 126 127 128 129
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
130
      | Tvar v -> Mvs.find_default v Unknown vm
131
      | _ -> Unknown
132
    in
133
    Hls.add cgr s (ls, Array.of_list (List.map desc tl))
134
  in
135 136
  let rec term vm () t = match t.t_node with
    | Tapp (s,tl) when Mls.mem s syms ->
137
        t_fold (term vm) () t; call vm s tl
138 139
    | Tlet ({t_node = Tvar v}, b) when Mvs.mem v vm ->
        let u,e = t_open_bound b in
140
        term (Mvs.add u (Mvs.find v vm) vm) () e
141
    | Tcase (e,bl) ->
142
        term vm () e; List.iter (fun b ->
143
          let p,t = t_open_branch b in
144 145
          let vml = match_term vm e [vm] p in
          List.iter (fun vm -> term vm () t) vml) bl
146 147
    | Tquant (_,b) ->
        let _,_,f = t_open_quant b in term vm () f
148
    | _ -> t_fold (term vm) () t
149
  in
150 151 152 153
  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
154
    term vm () e
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 198 199

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)
200 201 202

exception NoTerminationProof of lsymbol

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 228 229
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
230 231

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

245 246
(** Inductive predicate declaration *)

247
type prsymbol = {
248 249
  pr_name : ident;
}
250

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

261
let pr_equal : prsymbol -> prsymbol -> bool = (==)
262

Andrei Paskevich's avatar
Andrei Paskevich committed
263 264
let pr_hash pr = id_hash pr.pr_name

265
let create_prsymbol n = { pr_name = id_register n }
266

267
type ind_decl = lsymbol * (prsymbol * term) list
268 269 270 271

(** Proposition declaration *)

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

277
type prop_decl = prop_kind * prsymbol * term
278 279 280 281 282

(** Declaration type *)

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

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

296
module Hsdecl = Hashcons.Make (struct
297 298 299

  type t = decl

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

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

310
  let eq_iax (pr1,fr1) (pr2,fr2) =
311
    pr_equal pr1 pr2 && t_equal fr1 fr2
312

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

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

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

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

331
  let hs_prop (pr,f) = Hashcons.combine (pr_hash pr) (t_hash f)
332

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

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

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

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

346 347
end)

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

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

357
let d_equal : decl -> decl -> bool = (==)
358

Andrei Paskevich's avatar
Andrei Paskevich committed
359 360
let d_hash d = Hashweak.tag_hash d.d_tag

361 362
(** Declaration constructors *)

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

exception IllegalTypeAlias of tysymbol
exception ClashIdent of ident
372
exception BadLogicDecl of lsymbol * lsymbol
373

374
exception EmptyDecl
375 376
exception EmptyAlgDecl of tysymbol
exception EmptyIndDecl of lsymbol
377

378
exception NonPositiveTypeDecl of tysymbol * lsymbol * ty
379

380
let news_id s id = Sid.add_new id (ClashIdent id) s
381

382 383 384 385
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
386
let syms_term s t = t_s_fold syms_ty syms_ls s t
387

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

let create_logic_decl ldl =
  if ldl = [] then raise EmptyDecl;
424
  let check_decl (syms,news) (ls,ld) = match ld with
425
    | Some (s,_) when not (ls_equal s ls) ->
426
        raise (BadLogicDecl (ls, s))
427 428 429 430
    | Some ld ->
        let _, e = open_ls_defn ld in
        let syms = List.fold_left syms_ty syms ls.ls_args in
        syms_term syms e, news_id news ls.ls_name
431 432 433 434
    | 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
435
  in
436
  let (syms,news) = List.fold_left check_decl (Sid.empty,Sid.empty) ldl in
437
  ignore (check_termination ldl);
438
  mk_decl (Dlogic ldl) syms news
439

440 441
exception InvalidIndDecl of lsymbol * prsymbol
exception NonPositiveIndDecl of lsymbol * prsymbol * lsymbol
442 443 444 445 446

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

447 448 449
let rec f_pos_ps sps pol f = match f.t_node, pol with
  | Tapp (s, _), Some false when ls_mem s sps -> false
  | Tapp (s, _), None when ls_mem s sps -> false
450
  | Tbinop (Tiff, f, g), _ ->
451
      f_pos_ps sps None f && f_pos_ps sps None g
452
  | Tbinop (Timplies, f, g), _ ->
453
      f_pos_ps sps (option_map not pol) f && f_pos_ps sps pol g
454
  | Tnot f, _ ->
455
      f_pos_ps sps (option_map not pol) f
456
  | Tif (f,g,h), _ ->
457
      f_pos_ps sps None f && f_pos_ps sps pol g && f_pos_ps sps pol h
458
  | _ -> TermTF.t_all (t_pos_ps sps) (f_pos_ps sps pol) f
459 460 461 462 463

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
464
  let check_ax ps (syms,news) (pr,f) =
465
    let rec clause acc f = match f.t_node with
466 467 468
      | Tquant (Tforall, f) ->
          let _,_,f = t_open_quant f in clause acc f
      | Tbinop (Timplies, g, f) -> clause (g::acc) f
469 470
      | _ -> (acc, f)
    in
471 472
    let cls, g = clause [] (check_fvs f) in
    match g.t_node with
473
      | Tapp (s, tl) when ls_equal s ps ->
474
          List.iter2 check_tl ps.ls_args tl;
475
          (try ignore (List.for_all (f_pos_ps sps (Some true)) cls)
476
          with Found ls -> raise (NonPositiveIndDecl (ps, pr, ls)));
477 478 479 480 481
          (* check for unbound type variables *)
          let gtv = t_ty_freevars Stv.empty g in
          let ftv = t_ty_freevars Stv.empty f in
          if not (Stv.subset ftv gtv) then
            raise (UnboundTypeVar (Stv.choose (Stv.diff ftv gtv)));
482
          syms_term syms f, news_id news pr.pr_name
483 484
      | _ -> raise (InvalidIndDecl (ps, pr))
  in
485 486 487 488
  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
489
  in
490
  let (syms,news) = List.fold_left check_decl (Sid.empty,Sid.empty) idl in
491
  mk_decl (Dind idl) syms news
492

493
let create_prop_decl k p f =
494
  let syms = syms_term Sid.empty f in
495
  let news = news_id Sid.empty p.pr_name in
496
  mk_decl (Dprop (k,p,check_fvs f)) syms news
497

498 499
(** Utilities *)

500 501
let decl_map fn d = match d.d_node with
  | Dtype _ -> d
502 503 504
  | Dlogic l ->
      let fn = function
        | ls, Some ld ->
505 506
            let vl,e,close = open_ls_defn_cb ld in
            close ls vl (fn e)
507 508 509 510
        | ld -> ld
      in
      create_logic_decl (List.map fn l)
  | Dind l ->
511
      let fn (pr,f) = pr, fn f in
512 513 514
      let fn (ps,l) = ps, List.map fn l in
      create_ind_decl (List.map fn l)
  | Dprop (k,pr,f) ->
515
      create_prop_decl k pr (fn f)
516

517
let decl_fold fn acc d = match d.d_node with
518 519 520 521 522
  | Dtype _ -> acc
  | Dlogic l ->
      let fn acc = function
        | _, Some ld ->
            let _,e = open_ls_defn ld in
523
            fn acc e
524 525 526 527
        | _ -> acc
      in
      List.fold_left fn acc l
  | Dind l ->
528
      let fn acc (_,f) = fn acc f in
529 530
      let fn acc (_,l) = List.fold_left fn acc l in
      List.fold_left fn acc l
531
  | Dprop (_,_,f) ->
532
      fn acc f
533

534 535 536 537
let list_rpair_map_fold fn =
  let fn acc (x1,x2) =
    let acc,x2 = fn acc x2 in acc,(x1,x2) in
  Util.map_fold_left fn
538

539
let decl_map_fold fn acc d = match d.d_node with
540 541
  | Dtype _ -> acc, d
  | Dlogic l ->
542 543 544 545 546 547 548 549
      let fn acc = function
        | ls, Some ld ->
            let vl,e,close = open_ls_defn_cb ld in
            let acc,e = fn acc e in
            acc, close ls vl e
        | ld -> acc, ld
      in
      let acc,l = Util.map_fold_left fn acc l in
550
      acc, create_logic_decl l
551
  | Dind l ->
552
      let acc, l = list_rpair_map_fold (list_rpair_map_fold fn) acc l in
553 554
      acc, create_ind_decl l
  | Dprop (k,pr,f) ->
555
      let acc, f = fn acc f in
556
      acc, create_prop_decl k pr f
557

558
module DeclTF = struct
559 560 561
  let decl_map fnT fnF = decl_map (TermTF.t_select fnT fnF)
  let decl_fold fnT fnF = decl_fold (TermTF.t_selecti fnT fnF)
  let decl_map_fold fnT fnF = decl_map_fold (TermTF.t_selecti fnT fnF)
562
end
563

Andrei Paskevich's avatar
Andrei Paskevich committed
564 565 566 567 568 569
(** Known identifiers *)

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

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

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

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

582
let known_add_decl kn0 decl =
583
  let kn = Mid.map (const decl) decl.d_news in
584 585 586 587
  let check id decl0 _ =
    if d_equal decl0 decl
    then raise (KnownIdent id)
    else raise (RedeclaredIdent id)
588
  in
589
  let kn = Mid.union check kn0 kn in
590
  let unk = Mid.set_diff decl.d_syms kn in
591 592
  if Sid.is_empty unk then kn
  else raise (UnknownIdent (Sid.choose unk))
Andrei Paskevich's avatar
Andrei Paskevich committed
593

594
let find_type_definition kn ts =
595
  match (Mid.find ts.ts_name kn).d_node with
596
  | Dtype dl -> List.assq ts dl
597 598
  | _ -> assert false

599 600 601 602 603
let find_constructors kn ts =
  match find_type_definition kn ts with
  | Talgebraic cl -> cl
  | Tabstract -> []

604 605
let find_inductive_cases kn ps =
  match (Mid.find ps.ls_name kn).d_node with
606
  | Dind dl -> List.assq ps dl
607
  | Dlogic _ -> []
608 609 610 611 612 613 614 615
  | 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
616
  | _ -> assert false
617 618 619 620 621 622

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))
623
  | Dprop (_,_,f) -> f
624
  | _ -> assert false
625

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

634
exception NonExhaustiveCase of pattern list * term
635 636

let rec check_matchT kn () t = match t.t_node with
Andrei Paskevich's avatar
Andrei Paskevich committed
637 638 639
  | 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
640 641 642
      with Pattern.NonExhaustive p -> raise (NonExhaustiveCase (p,t)));
      t_fold (check_matchT kn) () t
  | _ -> t_fold (check_matchT kn) () t
643

644
let check_match kn d = decl_fold (check_matchT kn) () d
645

646 647 648 649 650 651 652 653 654 655 656 657 658 659 660 661 662 663 664 665 666 667 668 669 670 671 672
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
  | _ -> ()

673 674 675 676
let rec ts_extract_pos kn sts ts =
  if ts_equal ts ts_func then [false;true] else
  if ts_equal ts ts_pred then [false] else
  if Sts.mem ts sts then List.map Util.ttrue ts.ts_args else
677 678 679 680 681 682 683 684 685 686 687 688 689 690 691
  match find_type_definition kn ts with
    | Tabstract ->
        List.map Util.ffalse ts.ts_args
    | Talgebraic csl ->
        let sts = Sts.add ts sts in
        let rec get_ty stv ty = match ty.ty_node with
          | Tyvar _ -> stv
          | Tyapp (ts,tl) ->
              let get acc pos =
                if pos then get_ty acc else ty_freevars Stv.empty in
              List.fold_left2 get stv (ts_extract_pos kn sts ts) tl
        in
        let get_cs acc ls = List.fold_left get_ty acc ls.ls_args in
        let negs = List.fold_left get_cs Stv.empty csl in
        List.map (fun v -> not (Stv.mem v negs)) ts.ts_args
692 693 694 695 696 697 698 699 700 701 702 703 704 705 706 707 708 709 710 711 712 713 714 715 716

let check_positivity kn d = match d.d_node with
  | Dtype tdl ->
      let add s (ts,_) = Sts.add ts s in
      let tss = List.fold_left add Sts.empty tdl in
      let check_constr tys cs =
        let rec check_ty ty = match ty.ty_node with
          | Tyvar _ -> ()
          | Tyapp (ts,tl) ->
              let check pos ty =
                if pos then check_ty ty else
                if ty_s_any (fun ts -> Sts.mem ts tss) ty
                then raise (NonPositiveTypeDecl (tys,cs,ty))
              in
              List.iter2 check (ts_extract_pos kn Sts.empty ts) tl
        in
        List.iter check_ty cs.ls_args
      in
      let check_decl (ts,td) = match td with
        | Tabstract -> ()
        | Talgebraic cl -> List.iter (check_constr ts) cl
      in
      List.iter check_decl tdl
  | _ -> ()

717
let known_add_decl kn d =
718
  let kn = known_add_decl kn d in
719
  check_positivity kn d;
720 721
  check_foundness kn d;
  check_match kn d;
Andrei Paskevich's avatar
Andrei Paskevich committed
722 723
  kn