task.ml 8.64 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
(**************************************************************************)
(*                                                                        *)
(*  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
open Termlib
open Decl
open Theory2

Andrei Paskevich's avatar
Andrei Paskevich committed
29
30
31
32
33
34
(** Cloning map *)

type clone = {
  cl_map : clone_map;
  cl_tag : int
}
35

Andrei Paskevich's avatar
Andrei Paskevich committed
36
37
38
let empty_clone = {
  cl_map = Mid.empty;
  cl_tag = 0;
39
40
}

Andrei Paskevich's avatar
Andrei Paskevich committed
41
42
43
let cloned_from cl i1 i2 =
  try i1 = i2 || Sid.mem i2 (Mid.find i1 cl.cl_map)
  with Not_found -> false
44

Andrei Paskevich's avatar
Andrei Paskevich committed
45
let add_clone =
46
  let r = ref 0 in
Andrei Paskevich's avatar
Andrei Paskevich committed
47
  fun cl th sl ->
48
    incr r;
Andrei Paskevich's avatar
Andrei Paskevich committed
49
    { cl_map = merge_clone cl.cl_map th sl; cl_tag = !r }
50

Andrei Paskevich's avatar
Andrei Paskevich committed
51
let clone_tag cl = cl.cl_tag
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85


(** Known identifiers *)

exception UnknownIdent of ident
exception RedeclaredIdent of ident

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

let known_ts kn () ts = known_id kn ts.ts_name
let known_ls kn () ls = known_id kn ls.ls_name

let known_ty kn ty = ty_s_fold (known_ts kn) () ty
let known_term kn t = t_s_fold (known_ts kn) (known_ls kn) () t
let known_fmla kn f = f_s_fold (known_ts kn) (known_ls kn) () f

let merge_known kn1 kn2 =
  let add_known id decl kn =
    try
      if Mid.find id kn2 != decl then raise (RedeclaredIdent id);
      kn
    with Not_found -> Mid.add id decl kn
  in
  Mid.fold add_known kn1 kn2

exception DejaVu

let add_known id decl kn =
  try
    if Mid.find id kn != decl then raise (RedeclaredIdent id);
    raise DejaVu
  with Not_found -> Mid.add id decl kn

Andrei Paskevich's avatar
Andrei Paskevich committed
86
let add_constr d kn fs = add_known fs.ls_name d kn
87

Andrei Paskevich's avatar
Andrei Paskevich committed
88
89
90
91
92
let add_type d kn (ts,def) =
  let kn = add_known ts.ts_name d kn in
  match def with
    | Tabstract -> kn
    | Talgebraic lfs -> List.fold_left (add_constr d) kn lfs
93

Andrei Paskevich's avatar
Andrei Paskevich committed
94
95
96
97
98
let check_type kn (ts,def) =
  let check_constr fs = List.iter (known_ty kn) fs.ls_args in
  match def with
    | Tabstract -> option_iter (known_ty kn) ts.ts_def
    | Talgebraic lfs -> List.iter check_constr lfs
99

Andrei Paskevich's avatar
Andrei Paskevich committed
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
let add_logic d kn (ls,_) = add_known ls.ls_name d kn

let check_ls_defn kn ld =
  let _,e = open_ls_defn ld in
  e_apply (known_term kn) (known_fmla kn) e

let check_logic kn (ls,ld) =
  List.iter (known_ty kn) ls.ls_args;
  option_iter (known_ty kn) ls.ls_value;
  option_iter (check_ls_defn kn) ld

let add_ind d kn (ps,la) =
    let kn = add_known ps.ls_name d kn in
    let add kn (pr,_) = add_known (pr_name pr) d kn in
    List.fold_left add kn la

let check_ind kn (ps,la) =
    List.iter (known_ty kn) ps.ls_args;
    let check (_,f) = known_fmla kn f in
    List.iter check la

let add_decl kn d = match d.d_node with
  | Dtype dl  -> List.fold_left (add_type d) kn dl
  | Dlogic dl -> List.fold_left (add_logic d) kn dl
  | Dind dl   -> List.fold_left (add_ind d) kn dl
  | Dprop (_,pr,_) -> add_known (pr_name pr) d kn

let check_decl kn d = match d.d_node with
  | Dtype dl  -> List.iter (check_type kn) dl
  | Dlogic dl -> List.iter (check_logic kn) dl
  | Dind dl   -> List.iter (check_ind kn) dl
  | Dprop (_,_,f) -> known_fmla kn f
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146


(** Task *)

type task = {
  task_decl  : decl;
  task_prev  : task option;
  task_known : decl Mid.t;
  task_tag   : int;
}

module Task = struct
  type t = task

  let equal a b =
Andrei Paskevich's avatar
Andrei Paskevich committed
147
    a.task_decl == b.task_decl &&
148
149
150
151
152
153
154
155
156
157
    match a.task_prev, b.task_prev with
      | Some na, Some nb -> na == nb
      | None, None -> true
      | _ -> false

  let hash task =
    let prev = match task.task_prev with
      | Some task -> 1 + task.task_tag
      | None -> 0
    in
Andrei Paskevich's avatar
Andrei Paskevich committed
158
    Hashcons.combine task.task_decl.d_tag prev
159
160
161
162
163

  let tag i task = { task with task_tag = i }
end
module Htask = Hashcons.Make(Task)

Andrei Paskevich's avatar
Andrei Paskevich committed
164
let mk_task decl prev known = Htask.hashcons {
165
166
167
168
169
170
  task_decl  = decl;
  task_prev  = prev;
  task_known = known;
  task_tag   = -1;
}

Francois Bobot's avatar
Francois Bobot committed
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
let push_decl task d =
  try 
    let kn = add_decl task.task_known d in
    ignore (check_decl kn d);
    mk_task d (Some task) kn
  with DejaVu -> task

let init_decl d =  
  try
    let kn = add_decl Mid.empty d in
    ignore (check_decl kn d);
    mk_task d None kn
  with DejaVu -> assert false

let add_decl opt d =
  match opt with
    | Some task -> push_decl task d
    | None -> init_decl d

Andrei Paskevich's avatar
Andrei Paskevich committed
190
let init_task =
Francois Bobot's avatar
Francois Bobot committed
191
192
193
  let add opt = function
    | Decl d -> Some (add_decl opt d)
    | _      -> opt
Andrei Paskevich's avatar
Andrei Paskevich committed
194
195
  in
  List.fold_left add None builtin_theory.th_decls
196

Francois Bobot's avatar
Francois Bobot committed
197
(* let init_task = of_option init_task *)
198

Andrei Paskevich's avatar
Andrei Paskevich committed
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
let rec use_export names acc td =
  let used, cl, res, task = acc in
  match td with
    | Use th when Sid.mem th.th_name used ->
        acc
    | Use th ->
        let used = Sid.add th.th_name used in
        let acc = used, cl, res, task in
        let names = Some Spr.empty in
        List.fold_left (use_export names) acc th.th_decls
    | Clone (th,sl) ->
        let cl = add_clone cl th sl in
        used, cl, res, task
    | Decl d ->
        begin match d.d_node with
          | Dprop (Pgoal,pr,_)
            when option_apply true (Spr.mem pr) names ->
Francois Bobot's avatar
Francois Bobot committed
216
              let res = (push_decl task d, cl) :: res in
Andrei Paskevich's avatar
Andrei Paskevich committed
217
218
219
220
221
222
              used, cl, res, task
          | Dprop (Pgoal,_,_) ->
              acc
          | Dprop (Plemma,pr,f)
            when option_apply true (Spr.mem pr) names ->
              let d = create_prop_decl Pgoal pr f in
Francois Bobot's avatar
Francois Bobot committed
223
              let res = (push_decl task d, cl) :: res in
Andrei Paskevich's avatar
Andrei Paskevich committed
224
              let d = create_prop_decl Paxiom pr f in
Francois Bobot's avatar
Francois Bobot committed
225
              used, cl, res, push_decl task d
Andrei Paskevich's avatar
Andrei Paskevich committed
226
227
          | Dprop (Plemma,pr,f) ->
              let d = create_prop_decl Paxiom pr f in
Francois Bobot's avatar
Francois Bobot committed
228
              used, cl, res, push_decl task d
Andrei Paskevich's avatar
Andrei Paskevich committed
229
          | Dprop (Paxiom,_,_) ->
Francois Bobot's avatar
Francois Bobot committed
230
              used, cl, res, push_decl task d
Andrei Paskevich's avatar
Andrei Paskevich committed
231
          | Dtype _ | Dlogic _ | Dind _  ->
Francois Bobot's avatar
Francois Bobot committed
232
              used, cl, res, push_decl task d
Andrei Paskevich's avatar
Andrei Paskevich committed
233
234
235
        end

let split_theory_opt th names =
Francois Bobot's avatar
Francois Bobot committed
236
  let acc = Sid.empty, empty_clone, [], of_option init_task in
Andrei Paskevich's avatar
Andrei Paskevich committed
237
238
239
240
241
242
243
244
  let _, _, res, _ =
    List.fold_left (use_export names) acc th.th_decls
  in
  res

let split_theory th names = split_theory_opt th (Some names)
let split_theory_full th  = split_theory_opt th  None

245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
(* Generic utilities *)

let rec task_fold fn acc task =
  let acc = fn acc task.task_decl in
  match task.task_prev with
    | Some task -> task_fold fn acc task
    | None -> acc

let rec task_iter fn task =
  fn task.task_decl;
  match task.task_prev with
    | Some task -> task_iter fn task
    | None -> ()

let task_decls = task_fold (fun acc d -> d::acc) []

261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
exception GoalNotFound

let task_goal task = match task.task_decl.d_node with
  | Dprop (Pgoal,pr,_) -> pr
  | _ -> raise GoalNotFound


(** Task transformation *)

module Tr = struct

type 'a trans = task -> 'a
type 'a tlist = 'a list trans

let identity   x = x
let identity_l x = [x]

let conv_res f c x = c (f x)

let singleton f x = [f x]

let compose f g x = g (f x)

let compose_l f g x =
  List.fold_left (fun acc l -> List.rev_append (g l) acc) [] (f x)

let apply f x = f x

let ymemo f tag h =
  let rec aux x =
    let t = tag x in
    try
      Hashtbl.find h t
    with Not_found ->
      let r = f aux x in
      Hashtbl.add h t r;
      r in
  aux

let memo f tag h = ymemo (fun _ -> f) tag h

let term_tag t = t.t_tag
let fmla_tag f = f.f_tag
let decl_tag d = d.d_tag
let task_tag t = t.task_tag

let store f = memo f task_tag (Hashtbl.create 63)

let fold   fn v = assert false (* TODO *)
let fold_l fn v = assert false (* TODO *)

let fold_map   fn v = conv_res (fold   fn (v, init_task)) snd
let fold_map_l fn v = conv_res (fold_l fn (v, init_task)) (List.rev_map snd)

let map   fn = fold   (fun t1 t2 -> fn t1 t2) init_task
let map_l fn = fold_l (fun t1 t2 -> fn t1 t2) init_task

let decl   fn = assert false (* TODO *)
let decl_l fn = assert false (* TODO *)

let expr fnT fnF d = assert false (* TODO *)

end