task.ml 9.63 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
(*    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 Util
open Ident
open Ty
open Term
open Decl
25
open Theory
26

27 28 29
(** Clone and meta history *)

type tdecl_set = {
Andrei Paskevich's avatar
Andrei Paskevich committed
30 31
  tds_set : Stdecl.t;
  tds_tag : Hashweak.tag;
32 33 34 35 36
}

module Hstds = Hashcons.Make (struct
  type t = tdecl_set
  let equal s1 s2 = Stdecl.equal s1.tds_set s2.tds_set
Andrei Paskevich's avatar
Andrei Paskevich committed
37
  let hs_td td acc = Hashcons.combine acc (td_hash td)
38
  let hash s = Stdecl.fold hs_td s.tds_set 0
Andrei Paskevich's avatar
Andrei Paskevich committed
39
  let tag n s = { s with tds_tag = Hashweak.create_tag n }
40 41
end)

42
let mk_tds s = Hstds.hashcons {
Andrei Paskevich's avatar
Andrei Paskevich committed
43 44
  tds_set = s;
  tds_tag = Hashweak.dummy_tag;
45
}
46

47
let tds_empty = mk_tds Stdecl.empty
48
let tds_add td s = mk_tds (Stdecl.add td s.tds_set)
49 50
let tds_singleton td = mk_tds (Stdecl.singleton td)

51
let tds_equal : tdecl_set -> tdecl_set -> bool = (==)
Andrei Paskevich's avatar
Andrei Paskevich committed
52
let tds_hash tds = Hashweak.tag_hash tds.tds_tag
53

54
type clone_map = tdecl_set Mid.t
55
type meta_map = tdecl_set Mmeta.t
56

57
let cm_find cm th = Mid.find_default th.th_name tds_empty cm
58

59
let mm_find mm t = Mmeta.find_default t tds_empty mm
60

Andrei Paskevich's avatar
Andrei Paskevich committed
61 62 63
let cm_add cm th td = Mid.change th.th_name (function
  | None -> Some (tds_singleton td)
  | Some tds -> Some (tds_add td tds)) cm
64

65
let mm_add mm t td = if t.meta_excl
66 67
  then Mmeta.add t (tds_singleton td) mm
  else Mmeta.add t (tds_add td (mm_find mm t)) mm
68 69

(** Task *)
70

71 72 73
type task = task_hd option

and task_hd = {
74 75 76 77 78
  task_decl  : tdecl;        (* last declaration *)
  task_prev  : task;         (* context *)
  task_known : known_map;    (* known identifiers *)
  task_clone : clone_map;    (* cloning history *)
  task_meta  : meta_map;     (* meta properties *)
Andrei Paskevich's avatar
Andrei Paskevich committed
79
  task_tag   : Hashweak.tag; (* unique magical tag *)
80 81
}

82
let task_hd_equal : task_hd -> task_hd -> bool = (==)
83

Andrei Paskevich's avatar
Andrei Paskevich committed
84 85
let task_hd_hash t = Hashweak.tag_hash t.task_tag

Andrei Paskevich's avatar
Andrei Paskevich committed
86
let task_equal t1 t2 = match t1, t2 with
87
  | Some t1, Some t2 -> task_hd_equal t1 t2
Andrei Paskevich's avatar
Andrei Paskevich committed
88
  | None, None -> true
89
  | _ -> false
Andrei Paskevich's avatar
Andrei Paskevich committed
90

Andrei Paskevich's avatar
Andrei Paskevich committed
91 92
let task_hash t = option_apply 0 (fun t -> task_hd_hash t + 1) t

93
module Hstask = Hashcons.Make (struct
94
  type t = task_hd
95

96 97
  let equal t1 t2 = td_equal t1.task_decl t2.task_decl &&
                  task_equal t1.task_prev t2.task_prev
98

Andrei Paskevich's avatar
Andrei Paskevich committed
99
  let hash t = Hashcons.combine (td_hash t.task_decl) (task_hash t.task_prev)
100

Andrei Paskevich's avatar
Andrei Paskevich committed
101
  let tag i task = { task with task_tag = Hashweak.create_tag i }
102
end)
103

104
let mk_task decl prev known clone meta = Some (Hstask.hashcons {
105 106 107
  task_decl  = decl;
  task_prev  = prev;
  task_known = known;
108
  task_clone = clone;
109
  task_meta  = meta;
Andrei Paskevich's avatar
Andrei Paskevich committed
110
  task_tag   = Hashweak.dummy_tag;
111
})
112

113 114
let task_known = option_apply Mid.empty (fun t -> t.task_known)
let task_clone = option_apply Mid.empty (fun t -> t.task_clone)
115
let task_meta  = option_apply Mmeta.empty (fun t -> t.task_meta)
116

117 118
let find_clone_tds task th = cm_find (task_clone task) th
let find_meta_tds  task t  = mm_find (task_meta  task) t
119

120
(* constructors with checks *)
121

Andrei Paskevich's avatar
Andrei Paskevich committed
122
exception LemmaFound
123
exception SkipFound
Andrei Paskevich's avatar
Andrei Paskevich committed
124
exception GoalFound
125
exception GoalNotFound
Andrei Paskevich's avatar
Andrei Paskevich committed
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 155 156
let find_goal = function
  | Some {task_decl = {td_node = Decl {d_node = Dprop (Pgoal,p,_)}}} -> Some p
  | _ -> None

let task_goal task  = match find_goal task with
  | Some pr -> pr
  | None    -> raise GoalNotFound

let check_task task = match find_goal task with
  | Some _  -> raise GoalFound
  | None    -> task

let check_decl = function
  | { d_node = Dprop (Plemma,_,_)} -> raise LemmaFound
  | { d_node = Dprop (Pskip,_,_)}  -> raise SkipFound
  | d -> d

let new_decl task d td =
  let kn = known_add_decl (task_known task) (check_decl d) in
  mk_task td (check_task task) kn (task_clone task) (task_meta task)

let new_decl task d td = try new_decl task d td with KnownIdent _ -> task

let new_clone task th td =
  let cl = cm_add (task_clone task) th td in
  mk_task td (check_task task) (task_known task) cl (task_meta task)

let new_meta task t td =
  let mt = mm_add (task_meta task) t td in
  mk_task td (check_task task) (task_known task) (task_clone task) mt
Andrei Paskevich's avatar
Andrei Paskevich committed
157

158 159
(* declaration constructors + add_decl *)

160 161
let add_decl task d = new_decl task d (create_decl d)

162 163 164 165 166
let add_ty_decl tk dl = add_decl tk (create_ty_decl dl)
let add_logic_decl tk dl = add_decl tk (create_logic_decl dl)
let add_ind_decl tk dl = add_decl tk (create_ind_decl dl)
let add_prop_decl tk k p f = add_decl tk (create_prop_decl k p f)

167 168 169 170 171
(* task constructors *)

let rec add_tdecl task td = match td.td_node with
  | Decl d -> new_decl task d td
  | Use th -> use_export task th
172
  | Clone (th,_) -> new_clone task th td
173
  | Meta (t,_) -> new_meta task t td
174

175 176 177 178
and flat_tdecl task td = match td.td_node with
  | Decl { d_node = Dprop (Plemma,pr,f) } -> add_prop_decl task Paxiom pr f
  | Decl { d_node = Dprop ((Pgoal|Pskip),_,_) } -> task
  | _ -> add_tdecl task td
179

180 181
and use_export task th =
  let td = create_null_clone th in
182
  if Stdecl.mem td (find_clone_tds task th).tds_set then task else
183
  let task = List.fold_left flat_tdecl task th.th_decls in
184
  new_clone task th td
185 186 187

let clone_export = clone_theory flat_tdecl

188
let add_meta task t al = new_meta task t (create_meta t al)
189 190 191 192 193

(* split theory *)

let split_tdecl names (res,task) td = match td.td_node with
  | Decl { d_node = Dprop ((Pgoal|Plemma),pr,f) }
194
    when option_apply true (Spr.mem pr) names ->
195 196 197 198
      let res = add_prop_decl task Pgoal pr f :: res in
      res, flat_tdecl task td
  | _ ->
      res, flat_tdecl task td
Andrei Paskevich's avatar
Andrei Paskevich committed
199

200
let split_theory th names init =
201
  fst (List.fold_left (split_tdecl names) ([],init) th.th_decls)
Andrei Paskevich's avatar
Andrei Paskevich committed
202

203 204
(* Generic utilities *)

205 206 207
let rec task_fold fn acc = function
  | Some task -> task_fold fn (fn acc task.task_decl) task.task_prev
  | None      -> acc
208

209 210 211
let rec task_iter fn = function
  | Some task -> fn task.task_decl; task_iter fn task.task_prev
  | None      -> ()
212

213 214 215 216 217
let task_tdecls = task_fold (fun acc td -> td::acc) []

let task_decls  = task_fold (fun acc td ->
  match td.td_node with Decl d -> d::acc | _ -> acc) []

218
(* Selectors *)
219

220
exception NotTaggingMeta of meta
221 222 223 224 225 226 227 228 229 230 231 232 233 234 235 236 237 238 239 240 241 242 243 244 245 246 247 248 249 250 251
exception NotExclusiveMeta of meta

let on_meta t fn acc task =
  let add td acc = match td.td_node with
    | Meta (_,ma) -> fn acc ma
    | _ -> assert false
  in
  let tds = find_meta_tds task t in
  Stdecl.fold add tds.tds_set acc

let on_theory th fn acc task =
  let add td acc = match td.td_node with
    | Clone (_,sm) -> fn acc sm
    | _ -> assert false
  in
  let tds = find_clone_tds task th in
  Stdecl.fold add tds.tds_set acc

let on_meta_excl t task =
  if not t.meta_excl then raise (NotExclusiveMeta t);
  let add td _ = match td.td_node with
    | Meta (_,ma) -> Some ma
    | _ -> assert false
  in
  let tds = find_meta_tds task t in
  Stdecl.fold add tds.tds_set None

let on_used_theory th task =
  let td = create_null_clone th in
  let tds = find_clone_tds task th in
  Stdecl.mem td tds.tds_set
252

253 254 255 256 257 258 259 260 261 262 263 264 265
let on_tagged_ty t task =
  begin match t.meta_type with
    | MTty :: _ -> ()
    | _ -> raise (NotTaggingMeta t)
  end;
  let add td acc = match td.td_node with
    | Meta (_, MAty ty :: _) -> Sty.add ty acc
    | _ -> assert false
  in
  let tds = find_meta_tds task t in
  Stdecl.fold add tds.tds_set Sty.empty

let on_tagged_ts t task =
266
  begin match t.meta_type with
Andrei Paskevich's avatar
Andrei Paskevich committed
267
    | MTtysymbol :: _ -> ()
268 269
    | _ -> raise (NotTaggingMeta t)
  end;
270 271 272 273 274 275 276 277
  let add td acc = match td.td_node with
    | Meta (_, MAts ts :: _) -> Sts.add ts acc
    | _ -> assert false
  in
  let tds = find_meta_tds task t in
  Stdecl.fold add tds.tds_set Sts.empty

let on_tagged_ls t task =
278
  begin match t.meta_type with
Andrei Paskevich's avatar
Andrei Paskevich committed
279
    | MTlsymbol :: _ -> ()
280 281
    | _ -> raise (NotTaggingMeta t)
  end;
282 283 284 285 286 287 288 289
  let add td acc = match td.td_node with
    | Meta (_, MAls ls :: _) -> Sls.add ls acc
    | _ -> assert false
  in
  let tds = find_meta_tds task t in
  Stdecl.fold add tds.tds_set Sls.empty

let on_tagged_pr t task =
290
  begin match t.meta_type with
Andrei Paskevich's avatar
Andrei Paskevich committed
291
    | MTprsymbol :: _ -> ()
292 293
    | _ -> raise (NotTaggingMeta t)
  end;
294 295 296 297 298 299
  let add td acc = match td.td_node with
    | Meta (_, MApr pr :: _) -> Spr.add pr acc
    | _ -> assert false
  in
  let tds = find_meta_tds task t in
  Stdecl.fold add tds.tds_set Spr.empty
300

301 302
(* Exception reporting *)

303
let () = Exn_printer.register (fun fmt exn -> match exn with
304
  | LemmaFound ->   Format.fprintf fmt "Task cannot contain a lemma"
305
  | SkipFound ->    Format.fprintf fmt "Task cannot contain a skip"
306 307
  | GoalFound ->    Format.fprintf fmt "The task already ends with a goal"
  | GoalNotFound -> Format.fprintf fmt "The task does not end with a goal"
308
  | NotTaggingMeta m ->
309
      Format.fprintf fmt "Metaproperty '%s' is not a symbol tag" m.meta_name
310
  | NotExclusiveMeta m ->
311
      Format.fprintf fmt "Metaproperty '%s' is not exclusive" m.meta_name
312
  | _ -> raise exn)
313