decl.ml 26 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
(*    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 29 30
type constructor = lsymbol * lsymbol option list
(** constructor symbol with the list of projections *)

31
type ty_defn =
32
  | Tabstract
33
  | Talgebraic of constructor list
34

35
type ty_decl = tysymbol * ty_defn
36 37 38

(** Logic declaration *)

39
type ls_defn = lsymbol * term
40 41 42

type logic_decl = lsymbol * ls_defn option

43
exception UnboundVar of vsymbol
44 45

let check_fvs f =
46 47
  Mvs.iter (fun vs _ -> raise (UnboundVar vs)) f.t_vars;
  t_prop f
48

49 50
let check_vl ty v = ty_equal_check ty v.vs_ty
let check_tl ty t = ty_equal_check ty (t_type t)
51

52
let make_ls_defn ls vl t =
53
  (* check for duplicate arguments *)
54
  let add_v s v = Svs.add_new (DuplicateVar v) v s in
55
  ignore (List.fold_left add_v Svs.empty vl);
56
  (* build the definition axiom *)
57
  let hd = t_app ls (List.map t_var vl) t.t_ty in
58 59 60 61 62 63 64 65
  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 *)
66 67
  List.iter2 check_vl ls.ls_args vl;
  t_ty_check t ls.ls_value;
68 69
  (* return the definition *)
  ls, Some (ls, fd)
70

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

80 81 82 83 84 85 86 87 88
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

89
let ls_defn_axiom (_,f) = f
90

91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112
let ls_defn_of_axiom f =
  let _,_,f = match f.t_node with
    | Tquant (Tforall,b) -> t_open_quant b
    | _ -> [],[],f in
  let hd,e = match f.t_node with
    | Tapp (ls, [hd; t]) when ls_equal ls ps_equ -> hd,t
    | Tbinop (Tiff, hd, f) -> hd,f
    | _ -> raise Exit in
  let ls,tl = match hd.t_node with
    | Tapp (ls,tl) -> ls,tl
    | _ -> raise Exit in
  let vs_of_t t = match t.t_node with
    | Tvar v -> v
    | _ -> raise Exit in
  let vl = List.map vs_of_t tl in
  make_ls_defn ls vl e

let ls_defn_of_axiom f =
  try Some (ls_defn_of_axiom f) with
    | Exit | UnboundVar _ | UnboundTypeVar _
    | DuplicateVar _ | TypeMismatch _ -> None

113 114
(** Termination checking for mutually recursive logic declarations *)

115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154
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
155
      | Tvar v -> Mvs.find_def Unknown v vm
156
      | _ -> Unknown
157
    in
158
    Hls.add cgr s (ls, Array.of_list (List.map desc tl))
159
  in
160 161
  let rec term vm () t = match t.t_node with
    | Tapp (s,tl) when Mls.mem s syms ->
162
        t_fold (term vm) () t; call vm s tl
163 164
    | Tlet ({t_node = Tvar v}, b) when Mvs.mem v vm ->
        let u,e = t_open_bound b in
165
        term (Mvs.add u (Mvs.find v vm) vm) () e
166
    | Tcase (e,bl) ->
167
        term vm () e; List.iter (fun b ->
168
          let p,t = t_open_branch b in
169 170
          let vml = match_term vm e [vm] p in
          List.iter (fun vm -> term vm () t) vml) bl
171 172
    | Tquant (_,b) ->
        let _,_,f = t_open_quant b in term vm () f
173
    | _ -> t_fold (term vm) () t
174
  in
175 176 177 178
  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
179
    term vm () e
180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214 215 216 217 218 219 220 221 222 223 224

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)
225 226 227

exception NoTerminationProof of lsymbol

228 229 230 231 232 233 234 235 236 237 238 239 240 241 242 243 244 245 246 247 248 249 250 251 252 253 254
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
255 256

let check_termination ldl =
257
  let cgr = Hls.create 5 in
258 259 260 261
  let add acc (ls,ld) = match ld with
    | Some ld -> Mls.add ls (open_ls_defn ld) acc
    | None -> acc
  in
262 263
  let syms = List.fold_left add Mls.empty ldl in
  Mls.iter (build_call_graph cgr syms) syms;
264
  let check ls _ =
265
    let cl = build_call_list cgr ls in
266 267
    check_call_list ls cl
  in
268
  Mls.mapi check syms
269

270 271
(** Inductive predicate declaration *)

272
type prsymbol = {
273 274
  pr_name : ident;
}
275

Andrei Paskevich's avatar
Andrei Paskevich committed
276
module Prop = WeakStructMake (struct
277
  type t = prsymbol
278 279 280 281 282 283
  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
284
module Wpr = Prop.W
285

286
let pr_equal : prsymbol -> prsymbol -> bool = (==)
287

Andrei Paskevich's avatar
Andrei Paskevich committed
288 289
let pr_hash pr = id_hash pr.pr_name

290
let create_prsymbol n = { pr_name = id_register n }
291

292
type ind_decl = lsymbol * (prsymbol * term) list
293 294 295 296

(** Proposition declaration *)

type prop_kind =
297 298 299 300
  | 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 *)
301

302
type prop_decl = prop_kind * prsymbol * term
303 304 305 306 307

(** Declaration type *)

type decl = {
  d_node : decl_node;
308 309
  d_syms : Sid.t;         (* idents used in declaration *)
  d_news : Sid.t;         (* idents introduced in declaration *)
Andrei Paskevich's avatar
Andrei Paskevich committed
310
  d_tag  : Hashweak.tag;  (* unique magical tag *)
311 312 313 314 315 316 317 318 319 320
}

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

321
module Hsdecl = Hashcons.Make (struct
322 323 324

  type t = decl

325 326 327
  let cs_equal (cs1,pl1) (cs2,pl2) =
    ls_equal cs1 cs2 && list_all2 (option_eq ls_equal) pl1 pl2

328
  let eq_td (ts1,td1) (ts2,td2) = ts_equal ts1 ts2 && match td1,td2 with
329
    | Tabstract, Tabstract -> true
330
    | Talgebraic l1, Talgebraic l2 -> list_all2 cs_equal l1 l2
331 332
    | _ -> false

333
  let eq_ld (ls1,ld1) (ls2,ld2) = ls_equal ls1 ls2 && match ld1,ld2 with
334
    | Some (_,f1), Some (_,f2) -> t_equal f1 f2
335 336 337
    | None, None -> true
    | _ -> false

338
  let eq_iax (pr1,fr1) (pr2,fr2) =
339
    pr_equal pr1 pr2 && t_equal fr1 fr2
340

341 342
  let eq_ind (ps1,al1) (ps2,al2) =
    ls_equal ps1 ps2 && list_all2 eq_iax al1 al2
343 344

  let equal d1 d2 = match d1.d_node, d2.d_node with
Andrei Paskevich's avatar
Andrei Paskevich committed
345 346 347
    | 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
348
    | Dprop (k1,pr1,f1), Dprop (k2,pr2,f2) ->
349
        k1 = k2 && pr_equal pr1 pr2 && t_equal f1 f2
350 351
    | _,_ -> false

352 353 354
  let cs_hash (cs,pl) =
    Hashcons.combine_list (Hashcons.combine_option ls_hash) (ls_hash cs) pl

355
  let hs_td (ts,td) = match td with
Andrei Paskevich's avatar
Andrei Paskevich committed
356
    | Tabstract -> ts_hash ts
357
    | Talgebraic l -> 1 + Hashcons.combine_list cs_hash (ts_hash ts) l
358

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

362
  let hs_prop (pr,f) = Hashcons.combine (pr_hash pr) (t_hash f)
363

Andrei Paskevich's avatar
Andrei Paskevich committed
364
  let hs_ind (ps,al) = Hashcons.combine_list hs_prop (ls_hash ps) al
365 366

  let hs_kind = function
367
    | Plemma -> 11 | Paxiom -> 13 | Pgoal  -> 17 | Pskip  -> 19
368 369

  let hash d = match d.d_node with
370 371 372
    | 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
373
    | Dprop (k,pr,f) -> Hashcons.combine (hs_kind k) (hs_prop (pr,f))
374

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

377 378
end)

Andrei Paskevich's avatar
Andrei Paskevich committed
379
module Decl = WeakStructMake (struct
380 381 382
  type t = decl
  let tag d = d.d_tag
end)
383

384 385
module Sdecl = Decl.S
module Mdecl = Decl.M
Andrei Paskevich's avatar
Andrei Paskevich committed
386
module Wdecl = Decl.W
387

388
let d_equal : decl -> decl -> bool = (==)
389

Andrei Paskevich's avatar
Andrei Paskevich committed
390 391
let d_hash d = Hashweak.tag_hash d.d_tag

392 393
(** Declaration constructors *)

394
let mk_decl node syms news = Hsdecl.hashcons {
395 396 397
  d_node = node;
  d_syms = syms;
  d_news = news;
Andrei Paskevich's avatar
Andrei Paskevich committed
398
  d_tag  = Hashweak.dummy_tag;
399
}
400 401 402

exception IllegalTypeAlias of tysymbol
exception ClashIdent of ident
403
exception BadLogicDecl of lsymbol * lsymbol
404 405 406 407 408
exception BadConstructor of lsymbol

exception BadRecordField of lsymbol
exception RecordFieldMissing of lsymbol
exception DuplicateRecordField of lsymbol
409

410
exception EmptyDecl
411 412
exception EmptyAlgDecl of tysymbol
exception EmptyIndDecl of lsymbol
413

414
exception NonPositiveTypeDecl of tysymbol * lsymbol * ty
415

416
let news_id s id = Sid.add_new (ClashIdent id) id s
417

418 419 420 421
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
422
let syms_term s t = t_s_fold syms_ty syms_ls s t
423

424 425
let create_ty_decl tdl =
  if tdl = [] then raise EmptyDecl;
426 427
  let add s (ts,_) = Sts.add ts s in
  let tss = List.fold_left add Sts.empty tdl in
428 429 430 431 432 433 434 435 436 437 438 439 440 441 442
  let check_proj tyv s tya ls = match ls with
    | None -> s
    | Some ({ ls_args = [ptyv]; ls_value = Some ptya } as ls) ->
        ty_equal_check tyv ptyv;
        ty_equal_check tya ptya;
        Sls.add_new (DuplicateRecordField ls) ls s
    | Some ls -> raise (BadRecordField ls)
  in
  let check_constr tys ty pjs (syms,news) (fs,pl) =
    ty_equal_check ty (exn_option (BadConstructor fs) fs.ls_value);
    let fs_pjs =
      try List.fold_left2 (check_proj ty) Sls.empty fs.ls_args pl
      with Invalid_argument _ -> raise (BadConstructor fs) in
    if not (Sls.equal pjs fs_pjs) then
      raise (RecordFieldMissing (Sls.choose (Sls.diff pjs fs_pjs)));
443 444 445
    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 -> ()
446
      | Tyvar v -> raise (UnboundTypeVar v)
447
      | Tyapp (ts,tl) ->
448
          let now = Sts.mem ts tss in
449 450 451
          if seen && now
            then raise (NonPositiveTypeDecl (tys,fs,ty))
            else List.iter (check (seen || now)) tl
452
    in
453 454
    List.iter (check false) fs.ls_args;
    let syms = List.fold_left syms_ty syms fs.ls_args in
455
    syms, news_id news fs.ls_name
456
  in
457 458 459 460
  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
461
    | Talgebraic cl ->
462
        if cl = [] then raise (EmptyAlgDecl ts);
463
        if ts.ts_def <> None then raise (IllegalTypeAlias ts);
464
        let news = news_id news ts.ts_name in
465 466 467
        let pjs = List.fold_left (fun s (_,pl) -> List.fold_left
          (option_fold (fun s ls -> Sls.add ls s)) s pl) Sls.empty cl in
        let news = Sls.fold (fun pj s -> news_id s pj.ls_name) pjs news in
468
        let ty = ty_app ts (List.map ty_var ts.ts_args) in
469
        List.fold_left (check_constr ts ty pjs) (syms,news) cl
470
  in
471
  let (syms,news) = List.fold_left check_decl (Sid.empty,Sid.empty) tdl in
472
  mk_decl (Dtype tdl) syms news
473 474 475

let create_logic_decl ldl =
  if ldl = [] then raise EmptyDecl;
476
  let check_decl (syms,news) (ls,ld) = match ld with
477
    | Some (s,_) when not (ls_equal s ls) ->
478
        raise (BadLogicDecl (ls, s))
479 480 481 482
    | 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
483 484 485 486
    | 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
487
  in
488
  let (syms,news) = List.fold_left check_decl (Sid.empty,Sid.empty) ldl in
489
  ignore (check_termination ldl);
490
  mk_decl (Dlogic ldl) syms news
491

492 493
exception InvalidIndDecl of lsymbol * prsymbol
exception NonPositiveIndDecl of lsymbol * prsymbol * lsymbol
494 495 496 497 498

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

499 500 501
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
502
  | Tbinop (Tiff, f, g), _ ->
503
      f_pos_ps sps None f && f_pos_ps sps None g
504
  | Tbinop (Timplies, f, g), _ ->
505
      f_pos_ps sps (option_map not pol) f && f_pos_ps sps pol g
506
  | Tnot f, _ ->
507
      f_pos_ps sps (option_map not pol) f
508
  | Tif (f,g,h), _ ->
509
      f_pos_ps sps None f && f_pos_ps sps pol g && f_pos_ps sps pol h
510
  | _ -> TermTF.t_all (t_pos_ps sps) (f_pos_ps sps pol) f
511 512 513 514 515

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
516
  let check_ax ps (syms,news) (pr,f) =
517
    let rec clause acc f = match f.t_node with
518 519 520
      | Tquant (Tforall, f) ->
          let _,_,f = t_open_quant f in clause acc f
      | Tbinop (Timplies, g, f) -> clause (g::acc) f
521 522
      | _ -> (acc, f)
    in
523 524
    let cls, g = clause [] (check_fvs f) in
    match g.t_node with
525
      | Tapp (s, tl) when ls_equal s ps ->
526
          List.iter2 check_tl ps.ls_args tl;
527
          (try ignore (List.for_all (f_pos_ps sps (Some true)) cls)
528
          with Found ls -> raise (NonPositiveIndDecl (ps, pr, ls)));
529 530 531 532 533
          (* 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)));
534
          syms_term syms f, news_id news pr.pr_name
535 536
      | _ -> raise (InvalidIndDecl (ps, pr))
  in
537 538 539 540
  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
541
  in
542
  let (syms,news) = List.fold_left check_decl (Sid.empty,Sid.empty) idl in
543
  mk_decl (Dind idl) syms news
544

545
let create_prop_decl k p f =
546
  let syms = syms_term Sid.empty f in
547
  let news = news_id Sid.empty p.pr_name in
548
  mk_decl (Dprop (k,p,check_fvs f)) syms news
549

550 551
(** Utilities *)

552 553
let decl_map fn d = match d.d_node with
  | Dtype _ -> d
554 555 556
  | Dlogic l ->
      let fn = function
        | ls, Some ld ->
557 558
            let vl,e,close = open_ls_defn_cb ld in
            close ls vl (fn e)
559 560 561 562
        | ld -> ld
      in
      create_logic_decl (List.map fn l)
  | Dind l ->
563
      let fn (pr,f) = pr, fn f in
564 565 566
      let fn (ps,l) = ps, List.map fn l in
      create_ind_decl (List.map fn l)
  | Dprop (k,pr,f) ->
567
      create_prop_decl k pr (fn f)
568

569
let decl_fold fn acc d = match d.d_node with
570 571 572 573 574
  | Dtype _ -> acc
  | Dlogic l ->
      let fn acc = function
        | _, Some ld ->
            let _,e = open_ls_defn ld in
575
            fn acc e
576 577 578 579
        | _ -> acc
      in
      List.fold_left fn acc l
  | Dind l ->
580
      let fn acc (_,f) = fn acc f in
581 582
      let fn acc (_,l) = List.fold_left fn acc l in
      List.fold_left fn acc l
583
  | Dprop (_,_,f) ->
584
      fn acc f
585

586 587 588 589
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
590

591
let decl_map_fold fn acc d = match d.d_node with
592 593
  | Dtype _ -> acc, d
  | Dlogic l ->
594 595 596 597 598 599 600 601
      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
602
      acc, create_logic_decl l
603
  | Dind l ->
604
      let acc, l = list_rpair_map_fold (list_rpair_map_fold fn) acc l in
605 606
      acc, create_ind_decl l
  | Dprop (k,pr,f) ->
607
      let acc, f = fn acc f in
608
      acc, create_prop_decl k pr f
609

610
module DeclTF = struct
611 612 613
  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)
614
end
615

Andrei Paskevich's avatar
Andrei Paskevich committed
616 617 618 619 620 621
(** Known identifiers *)

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

622
type known_map = decl Mid.t
Andrei Paskevich's avatar
Andrei Paskevich committed
623 624 625 626 627

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

let merge_known kn1 kn2 =
628
  let check_known id decl1 decl2 =
629 630 631
    if d_equal decl1 decl2 then Some decl1
    else raise (RedeclaredIdent id)
  in
632
  Mid.union check_known kn1 kn2
Andrei Paskevich's avatar
Andrei Paskevich committed
633

634
let known_add_decl kn0 decl =
635
  let kn = Mid.map (const decl) decl.d_news in
636 637 638 639
  let check id decl0 _ =
    if d_equal decl0 decl
    then raise (KnownIdent id)
    else raise (RedeclaredIdent id)
640
  in
641
  let kn = Mid.union check kn0 kn in
642
  let unk = Mid.set_diff decl.d_syms kn in
643 644
  if Sid.is_empty unk then kn
  else raise (UnknownIdent (Sid.choose unk))
Andrei Paskevich's avatar
Andrei Paskevich committed
645

646
let find_type_definition kn ts =
647
  match (Mid.find ts.ts_name kn).d_node with
648
  | Dtype dl -> List.assq ts dl
649 650
  | _ -> assert false

651 652 653 654 655
let find_constructors kn ts =
  match find_type_definition kn ts with
  | Talgebraic cl -> cl
  | Tabstract -> []

656 657
let find_inductive_cases kn ps =
  match (Mid.find ps.ls_name kn).d_node with
658
  | Dind dl -> List.assq ps dl
659
  | Dlogic _ -> []
660 661 662 663 664 665 666 667
  | 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
668
  | _ -> assert false
669 670 671 672 673 674

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))
675
  | Dprop (_,_,f) -> f
676
  | _ -> assert false
677

678 679
let find_prop_decl kn pr =
  match (Mid.find pr.pr_name kn).d_node with
680
  | Dind dl ->
681
      let test (_,l) = List.mem_assq pr l in
682
      Paxiom, List.assq pr (snd (List.find test dl))
683 684 685
  | Dprop (k,_,f) -> k,f
  | _ -> assert false

686
exception NonExhaustiveCase of pattern list * term
687 688

let rec check_matchT kn () t = match t.t_node with
Andrei Paskevich's avatar
Andrei Paskevich committed
689 690
  | Tcase (t1,bl) ->
      let bl = List.map (fun b -> let p,t = t_open_branch b in [p],t) bl in
691
      let find_constructors kn ts = List.map fst (find_constructors kn ts) in
Andrei Paskevich's avatar
Andrei Paskevich committed
692
      ignore (try Pattern.CompileTerm.compile (find_constructors kn) [t1] bl
693 694 695
      with Pattern.NonExhaustive p -> raise (NonExhaustiveCase (p,t)));
      t_fold (check_matchT kn) () t
  | _ -> t_fold (check_matchT kn) () t
696

697
let check_match kn d = decl_fold (check_matchT kn) () d
698

699 700 701
exception NonFoundedTypeDecl of tysymbol

let rec check_foundness kn d =
Andrei Paskevich's avatar
Andrei Paskevich committed
702 703 704 705 706 707 708 709 710 711 712
  let rec check_ts tss tvs ts =
    (* recursive data type, abandon *)
    if Sts.mem ts tss then false else
    let cl = find_constructors kn ts in
    (* an abstract type is inhabited iff
       all its type arguments are inhabited *)
    if cl == [] then Stv.is_empty tvs else
    (* an algebraic type is inhabited iff
       we can build a value of this type *)
    let tss = Sts.add ts tss in
    List.exists (check_constr tss tvs) cl
713
  and check_constr tss tvs (ls,_) =
Andrei Paskevich's avatar
Andrei Paskevich committed
714 715 716 717 718 719 720 721 722 723 724
    (* we can construct a value iff every
       argument is of an inhabited type *)
    List.for_all (check_type tss tvs) ls.ls_args
  and check_type tss tvs ty = match ty.ty_node with
    | Tyvar tv ->
        not (Stv.mem tv tvs)
    | Tyapp (ts,tl) ->
        let check acc tv ty =
          if check_type tss tvs ty then acc else Stv.add tv acc in
        let tvs = List.fold_left2 check Stv.empty ts.ts_args tl in
        check_ts tss tvs ts
725 726 727 728
  in
  match d.d_node with
  | Dtype tdl ->
      let check () (ts,_) =
Andrei Paskevich's avatar
Andrei Paskevich committed
729
        if check_ts Sts.empty Stv.empty ts
730 731 732 733 734
        then () else raise (NonFoundedTypeDecl ts)
      in
      List.fold_left check () tdl
  | _ -> ()

735
let rec ts_extract_pos kn sts ts =
736
  assert (ts.ts_def = None);
737 738 739
  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
740 741 742 743 744 745 746 747 748
  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 =
749
                if pos then get_ty acc else ty_freevars acc in
750 751
              List.fold_left2 get stv (ts_extract_pos kn sts ts) tl
        in
752
        let get_cs acc (ls,_) = List.fold_left get_ty acc ls.ls_args in
753 754
        let negs = List.fold_left get_cs Stv.empty csl in
        List.map (fun v -> not (Stv.mem v negs)) ts.ts_args
755 756 757 758 759

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
760
      let check_constr tys (cs,_) =
761 762 763 764 765 766 767 768 769 770 771 772 773 774 775 776 777 778 779
        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
  | _ -> ()

780
let known_add_decl kn d =
781
  let kn = known_add_decl kn d in
782
  check_positivity kn d;
783 784
  check_foundness kn d;
  check_match kn d;
Andrei Paskevich's avatar
Andrei Paskevich committed
785 786
  kn

787 788 789 790 791 792 793 794 795 796 797 798 799 800 801 802 803 804 805 806 807 808 809 810 811 812 813 814 815 816 817 818 819 820 821 822 823 824 825 826 827
(** Records *)

exception EmptyRecord

let parse_record kn fll =
  let fs = match fll with
    | [] -> raise EmptyRecord
    | (fs,_)::_ -> fs in
  let ts = match fs.ls_args with
    | [{ ty_node = Tyapp (ts,_) }] -> ts
    | _ -> raise (BadRecordField fs) in
  let cs, pjl = match find_constructors kn ts with
    | [cs,pjl] -> cs, List.map (exn_option (BadRecordField fs)) pjl
    | _ -> raise (BadRecordField fs) in
  let pjs = List.fold_left (fun s pj -> Sls.add pj s) Sls.empty pjl in
  let flm = List.fold_left (fun m (pj,v) ->
    if not (Sls.mem pj pjs) then raise (BadRecordField pj) else
    Mls.add_new (DuplicateRecordField pj) pj v m) Mls.empty fll in
  cs,pjl,flm

let make_record kn fll ty =
  let cs,pjl,flm = parse_record kn fll in
  let get_arg pj = Mls.find_exn (RecordFieldMissing pj) pj flm in
  fs_app cs (List.map get_arg pjl) ty

let make_record_update kn t fll ty =
  let cs,pjl,flm = parse_record kn fll in
  let get_arg pj = match Mls.find_opt pj flm with
    | Some v -> v
    | None -> t_app_infer pj [t] in
  fs_app cs (List.map get_arg pjl) ty

let make_record_pattern kn fll ty =
  let cs,pjl,flm = parse_record kn fll in
  let s = ty_match Mtv.empty (of_option cs.ls_value) ty in
  let get_arg pj = match Mls.find_opt pj flm with
    | Some v -> v
    | None -> pat_wild (ty_inst s (of_option pj.ls_value))
  in
  pat_app cs (List.map get_arg pjl) ty