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 8.83 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
48
let empty_tds = mk_tds Stdecl.empty
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 = try Mid.find th.th_name cm with Not_found -> empty_tds
58
59

let mm_find mm t =
60
  try Mmeta.find t mm with Not_found -> empty_tds
61
62

let cm_add cm th td = Mid.add th.th_name (tds_add td (cm_find cm th)) cm
63

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

(** Task *)
69

70
71
72
type task = task_hd option

and task_hd = {
73
74
75
76
77
  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
78
  task_tag   : Hashweak.tag; (* unique magical tag *)
79
80
}

81
82
let task_hd_equal = (==)

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

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

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

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

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

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

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

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

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

116
117
let find_clone task th = cm_find (task_clone task) th
let find_meta  task t  = mm_find (task_meta  task) t
118

119
(* constructors with checks *)
120

Andrei Paskevich's avatar
Andrei Paskevich committed
121
exception LemmaFound
122
exception SkipFound
Andrei Paskevich's avatar
Andrei Paskevich committed
123
exception GoalFound
124
exception GoalNotFound
Andrei Paskevich's avatar
Andrei Paskevich committed
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
155
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
156

157
158
(* declaration constructors + add_decl *)

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

161
162
163
164
165
166
167
168
169
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)

let add_ty_decls tk dl = List.fold_left add_decl tk (create_ty_decls dl)
let add_logic_decls tk dl = List.fold_left add_decl tk (create_logic_decls dl)
let add_ind_decls tk dl = List.fold_left add_decl tk (create_ind_decls dl)

170
171
172
173
174
(* 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
175
176
  | Clone (th,_,_,_) -> new_clone task th td
  | Meta (t,_) -> new_meta task t td
177

178
179
180
181
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
182

183
184
and use_export task th =
  let td = create_null_clone th in
185
  if Stdecl.mem td (find_clone task th).tds_set then task else
186
  let task = List.fold_left flat_tdecl task th.th_decls in
187
  new_clone task th td
188
189
190

let clone_export = clone_theory flat_tdecl

191
let add_meta task t al = new_meta task t (create_meta t al)
192
193
194
195
196

(* split theory *)

let split_tdecl names (res,task) td = match td.td_node with
  | Decl { d_node = Dprop ((Pgoal|Plemma),pr,f) }
197
    when option_apply true (Spr.mem pr) names ->
198
199
200
201
      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
202

203
let split_theory th names init =
204
  fst (List.fold_left (split_tdecl names) ([],init) th.th_decls)
Andrei Paskevich's avatar
Andrei Paskevich committed
205

206
207
(* Generic utilities *)

208
209
210
let rec task_fold fn acc = function
  | Some task -> task_fold fn (fn acc task.task_decl) task.task_prev
  | None      -> acc
211

212
213
214
let rec task_iter fn = function
  | Some task -> fn task.task_decl; task_iter fn task.task_prev
  | None      -> ()
215

216
217
218
219
220
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) []

221
(* special selector for metaproperties of a single ident *)
222

223
exception NotTaggingMeta of meta
224

225
let find_tagged_ts t tds acc =
226
  begin match t.meta_type with
227
    | [MTtysymbol] -> ()
228
229
230
    | _ -> raise (NotTaggingMeta t)
  end;
  Stdecl.fold (fun td acc -> match td.td_node with
231
    | Meta (s, [MAts ts]) when meta_equal s t -> Sts.add ts acc
232
233
234
    | _ -> assert false) tds.tds_set acc

let find_tagged_ls t tds acc =
235
  begin match t.meta_type with
236
237
238
239
    | [MTlsymbol] -> ()
    | _ -> raise (NotTaggingMeta t)
  end;
  Stdecl.fold (fun td acc -> match td.td_node with
240
    | Meta (s, [MAls ls]) when meta_equal s t -> Sls.add ls acc
241
242
243
    | _ -> assert false) tds.tds_set acc

let find_tagged_pr t tds acc =
244
  begin match t.meta_type with
245
246
247
248
    | [MTprsymbol] -> ()
    | _ -> raise (NotTaggingMeta t)
  end;
  Stdecl.fold (fun td acc -> match td.td_node with
249
    | Meta (s, [MApr pr]) when meta_equal s t -> Spr.add pr acc
250
    | _ -> assert false) tds.tds_set acc
251

252
exception NotExclusiveMeta of meta
253

254
let get_meta_excl t tds =
255
  if not t.meta_excl then raise (NotExclusiveMeta t);
256
  Stdecl.fold (fun td _ -> match td.td_node with
257
    | Meta (s,arg) when s = t -> Some arg
258
259
    | _ -> assert false) tds.tds_set None

260
261
(* Exception reporting *)

262
let () = Exn_printer.register (fun fmt exn -> match exn with
263
  | LemmaFound ->   Format.fprintf fmt "Task cannot contain a lemma"
264
  | SkipFound ->    Format.fprintf fmt "Task cannot contain a skip"
265
266
  | GoalFound ->    Format.fprintf fmt "The task already ends with a goal"
  | GoalNotFound -> Format.fprintf fmt "The task does not end with a goal"
267
  | NotTaggingMeta m ->
268
      Format.fprintf fmt "Metaproperty '%s' is not a symbol tag" m.meta_name
269
  | NotExclusiveMeta m ->
270
      Format.fprintf fmt "Metaproperty '%s' is not exclusive" m.meta_name
271
  | _ -> raise exn)
272