MAJ terminée. Nous sommes passés en version 14.6.2 . Pour consulter les "releases notes" associées c'est ici :

https://about.gitlab.com/releases/2022/01/11/security-release-gitlab-14-6-2-released/
https://about.gitlab.com/releases/2022/01/04/gitlab-14-6-1-released/

task.ml 9.57 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
(**************************************************************************)
(*                                                                        *)
(*  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 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
51
let tds_singleton td = mk_tds (Stdecl.singleton td)

let tds_equal = (==)
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
83
let task_hd_equal = (==)

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