decl.ml 14.4 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

(** Inductive predicate declaration *)

76
type prsymbol = {
77 78
  pr_name : ident;
}
79

Andrei Paskevich's avatar
Andrei Paskevich committed
80
module Prop = WeakStructMake (struct
81
  type t = prsymbol
82 83 84 85 86 87
  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
88
module Wpr = Prop.W
89

90
let pr_equal = (==)
91

Andrei Paskevich's avatar
Andrei Paskevich committed
92 93
let pr_hash pr = id_hash pr.pr_name

94
let create_prsymbol n = { pr_name = id_register n }
95

96
type ind_decl = lsymbol * (prsymbol * fmla) list
97 98 99 100

(** Proposition declaration *)

type prop_kind =
101 102 103 104
  | 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 *)
105

106
type prop_decl = prop_kind * prsymbol * fmla
107 108 109 110 111

(** Declaration type *)

type decl = {
  d_node : decl_node;
112 113
  d_syms : Sid.t;         (* idents used in declaration *)
  d_news : Sid.t;         (* idents introduced in declaration *)
Andrei Paskevich's avatar
Andrei Paskevich committed
114
  d_tag  : Hashweak.tag;  (* unique magical tag *)
115 116 117 118 119 120 121 122 123 124
}

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

125
module Hsdecl = Hashcons.Make (struct
126 127 128

  type t = decl

129
  let eq_td (ts1,td1) (ts2,td2) = ts_equal ts1 ts2 && match td1,td2 with
130
    | Tabstract, Tabstract -> true
131
    | Talgebraic l1, Talgebraic l2 -> list_all2 ls_equal l1 l2
132 133
    | _ -> false

134 135
  let eq_ld (ls1,ld1) (ls2,ld2) = ls_equal ls1 ls2 && match ld1,ld2 with
    | Some (_,f1), Some (_,f2) -> f_equal f1 f2
136 137 138
    | None, None -> true
    | _ -> false

139 140
  let eq_iax (pr1,fr1) (pr2,fr2) =
    pr_equal pr1 pr2 && f_equal fr1 fr2
141

142 143
  let eq_ind (ps1,al1) (ps2,al2) =
    ls_equal ps1 ps2 && list_all2 eq_iax al1 al2
144 145

  let equal d1 d2 = match d1.d_node, d2.d_node with
Andrei Paskevich's avatar
Andrei Paskevich committed
146 147 148
    | 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
149
    | Dprop (k1,pr1,f1), Dprop (k2,pr2,f2) ->
150
        k1 = k2 && pr_equal pr1 pr2 && f_equal f1 f2
151 152 153
    | _,_ -> false

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

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

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

Andrei Paskevich's avatar
Andrei Paskevich committed
162
  let hs_ind (ps,al) = Hashcons.combine_list hs_prop (ls_hash ps) al
163 164

  let hs_kind = function
165
    | Plemma -> 11 | Paxiom -> 13 | Pgoal  -> 17 | Pskip  -> 19
166 167

  let hash d = match d.d_node with
168 169 170
    | 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
171
    | Dprop (k,pr,f) -> Hashcons.combine (hs_kind k) (hs_prop (pr,f))
172

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

175 176
end)

Andrei Paskevich's avatar
Andrei Paskevich committed
177
module Decl = WeakStructMake (struct
178 179 180
  type t = decl
  let tag d = d.d_tag
end)
181

182 183
module Sdecl = Decl.S
module Mdecl = Decl.M
Andrei Paskevich's avatar
Andrei Paskevich committed
184
module Wdecl = Decl.W
185

186 187
let d_equal = (==)

Andrei Paskevich's avatar
Andrei Paskevich committed
188 189
let d_hash d = Hashweak.tag_hash d.d_tag

190 191
(** Declaration constructors *)

192
let mk_decl node syms news = Hsdecl.hashcons {
193 194 195
  d_node = node;
  d_syms = syms;
  d_news = news;
Andrei Paskevich's avatar
Andrei Paskevich committed
196
  d_tag  = Hashweak.dummy_tag;
197
}
198 199 200

exception IllegalTypeAlias of tysymbol
exception ClashIdent of ident
201
exception BadLogicDecl of ident * ident
202

203
exception EmptyDecl
204 205
exception EmptyAlgDecl of tysymbol
exception EmptyIndDecl of lsymbol
206

207
let news_id s id =
208 209 210
  if Sid.mem id s then raise (ClashIdent id);
  Sid.add id s

211 212 213 214 215 216 217
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

218 219
let create_ty_decl tdl =
  if tdl = [] then raise EmptyDecl;
220
  let check_constr ty (syms,news) fs =
221
    let vty = of_option fs.ls_value in
222
    ignore (ty_match Mtv.empty vty ty);
223 224 225 226 227
    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
228
    let rec check s ty = match ty.ty_node with
229 230 231
      | 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)
232
    in
233 234
    let syms = List.fold_left check syms fs.ls_args in
    syms, news_id news fs.ls_name
235
  in
236 237 238 239
  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
240
    | Talgebraic cl ->
241
        if cl = [] then raise (EmptyAlgDecl ts);
242
        if ts.ts_def <> None then raise (IllegalTypeAlias ts);
243
        let news = news_id news ts.ts_name in
244
        let ty = ty_app ts (List.map ty_var ts.ts_args) in
245
        List.fold_left (check_constr ty) (syms,news) cl
246
  in
247
  let (syms,news) = List.fold_left check_decl (Sid.empty,Sid.empty) tdl in
248
  mk_decl (Dtype tdl) syms news
249 250 251

let create_logic_decl ldl =
  if ldl = [] then raise EmptyDecl;
252
  let check_decl (syms,news) (ls,ld) = match ld with
253 254
    | Some (s,_) when not (ls_equal s ls) ->
        raise (BadLogicDecl (ls.ls_name, s.ls_name))
255 256 257 258 259 260
    | 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
261
  in
262
  let (syms,news) = List.fold_left check_decl (Sid.empty,Sid.empty) ldl in
263
  mk_decl (Dlogic ldl) syms news
264

265 266 267
exception InvalidIndDecl of lsymbol * prsymbol
exception TooSpecificIndDecl of lsymbol * prsymbol * term
exception NonPositiveIndDecl of lsymbol * prsymbol * lsymbol
268 269 270 271 272 273 274 275 276 277 278 279 280 281 282 283 284 285 286 287 288 289

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
290
  let check_ax ps (syms,news) (pr,f) =
291
    let rec clause acc f = match f.f_node with
292 293
      | Fquant (Fforall, f) ->
          let _,_,f = f_open_quant f in clause acc f
294 295 296
      | Fbinop (Fimplies, g, f) -> clause (g::acc) f
      | _ -> (acc, f)
    in
297
    let cls, f = clause [] (check_fvs f) in
298
    match f.f_node with
299
      | Fapp (s, tl) when ls_equal s ps ->
300
          let mtch sb t ty =
301
            try ty_match sb (t.t_ty) ty with TypeMismatch _ ->
302 303
              raise (TooSpecificIndDecl (ps, pr, t))
          in
304
          ignore (List.fold_left2 mtch Mtv.empty tl ps.ls_args);
305
          (try ignore (List.for_all (f_pos_ps sps (Some true)) cls)
306 307
          with Found ls -> raise (NonPositiveIndDecl (ps, pr, ls)));
          syms_fmla syms f, news_id news pr.pr_name
308 309
      | _ -> raise (InvalidIndDecl (ps, pr))
  in
310 311 312 313
  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
314
  in
315
  let (syms,news) = List.fold_left check_decl (Sid.empty,Sid.empty) idl in
316
  mk_decl (Dind idl) syms news
317

318 319 320
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
321
  mk_decl (Dprop (k,p,check_fvs f)) syms news
322

323 324 325 326 327 328 329 330 331 332 333 334 335 336 337 338 339 340 341 342
(** 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)

343 344 345 346 347 348 349 350 351 352 353 354 355 356
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
357 358
  | Dprop (_,_,f) ->
      fnF acc f
359

360 361 362 363 364 365 366 367 368 369 370 371 372 373 374 375 376 377 378 379 380 381 382
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

383

Andrei Paskevich's avatar
Andrei Paskevich committed
384 385 386 387 388 389
(** Known identifiers *)

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

390
type known_map = decl Mid.t
Andrei Paskevich's avatar
Andrei Paskevich committed
391 392 393 394 395 396 397

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

let merge_known kn1 kn2 =
  let add_known id decl kn =
    try
398
      if not (d_equal (Mid.find id kn2) decl) then raise (RedeclaredIdent id);
Andrei Paskevich's avatar
Andrei Paskevich committed
399 400 401 402 403
      kn
    with Not_found -> Mid.add id decl kn
  in
  Mid.fold add_known kn1 kn2

404
let known_add_decl kn0 decl =
405 406
  let add_known id kn =
    try
407
      if not (d_equal (Mid.find id kn0) decl) then raise (RedeclaredIdent id);
408 409 410
      raise (KnownIdent id)
    with Not_found -> Mid.add id decl kn
  in
411
  let kn = Sid.fold add_known decl.d_news kn0 in
412 413 414 415 416
  let check_known id =
    if not (Mid.mem id kn) then raise (UnknownIdent id)
  in
  ignore (Sid.iter check_known decl.d_syms);
  kn
Andrei Paskevich's avatar
Andrei Paskevich committed
417

418 419 420
let find_constructors kn ts =
  match (Mid.find ts.ts_name kn).d_node with
  | Dtype dl ->
421
      begin match List.assq ts dl with
422 423 424 425 426 427 428
        | Talgebraic cl -> cl
        | Tabstract -> []
      end
  | _ -> assert false

let find_inductive_cases kn ps =
  match (Mid.find ps.ls_name kn).d_node with
429
  | Dind dl -> List.assq ps dl
430 431
  | Dlogic _ -> []
  | _ -> assert false
432 433 434 435 436 437

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))
438
  | Dprop (_,_,f) -> f
439
  | _ -> assert false
440

441 442
let find_prop_decl kn pr =
  match (Mid.find pr.pr_name kn).d_node with
443
  | Dind dl ->
444
      let test (_,l) = List.mem_assq pr l in
445
      Paxiom, List.assq pr (snd (List.find test dl))
446 447 448
  | Dprop (k,_,f) -> k,f
  | _ -> assert false

449 450 451
exception NonExhaustiveExpr of (pattern list * expr)

let rec check_matchT kn () t = match t.t_node with
Andrei Paskevich's avatar
Andrei Paskevich committed
452 453 454
  | 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
455 456
      with Pattern.NonExhaustive p -> raise (NonExhaustiveExpr (p,Term t)));
      t_fold (check_matchT kn) (check_matchF kn) () t
457 458 459
  | _ -> 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
460 461 462
  | 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
463 464
      with Pattern.NonExhaustive p -> raise (NonExhaustiveExpr (p,Fmla f)));
      f_fold (check_matchT kn) (check_matchF kn) () f
465 466 467 468
  | _ -> f_fold (check_matchT kn) (check_matchF kn) () f

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

469
let known_add_decl kn d =
470
  let kn = known_add_decl kn d in
471
  ignore (check_match kn d);
Andrei Paskevich's avatar
Andrei Paskevich committed
472 473
  kn