task.ml 7.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

Andrei Paskevich's avatar
Andrei Paskevich committed
27
28
29
30
31
32
(** Cloning map *)

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

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

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

43
let add_clone =
44
  let r = ref 0 in
45
46
47
  fun cl th sl ->
    incr r;
    { cl_map = merge_clone cl.cl_map th sl; cl_tag = !r }
48
49
50
51
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


(** 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
82
let add_constr d kn fs = add_known fs.ls_name d kn
83

Andrei Paskevich's avatar
Andrei Paskevich committed
84
85
86
87
88
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
89

Andrei Paskevich's avatar
Andrei Paskevich committed
90
91
92
93
94
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
95

Andrei Paskevich's avatar
Andrei Paskevich committed
96
97
98
99
100
101
102
103
104
105
106
107
108
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
109
    let add kn (pr,_) = add_known pr.pr_name d kn in
Andrei Paskevich's avatar
Andrei Paskevich committed
110
111
112
113
114
115
116
117
118
119
120
    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
121
  | Dprop (_,pr,_) -> add_known pr.pr_name d kn
Andrei Paskevich's avatar
Andrei Paskevich committed
122
123
124
125
126
127

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
128

Andrei Paskevich's avatar
minor    
Andrei Paskevich committed
129
130
131
132
let add_decl kn d =
  let kn = add_decl kn d in
  ignore (check_decl kn d);
  kn
133
134
135

(** Task *)

136
137
138
type task = task_hd option

and task_hd = {
139
  task_decl  : decl;
140
  task_prev  : task;
141
142
143
144
145
  task_known : decl Mid.t;
  task_tag   : int;
}

module Task = struct
146
  type t = task_hd
147
148

  let equal a b =
Andrei Paskevich's avatar
Andrei Paskevich committed
149
    a.task_decl == b.task_decl &&
150
151
152
153
154
155
156
157
158
159
    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
160
    Hashcons.combine task.task_decl.d_tag prev
161
162
163
164
165

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

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

Andrei Paskevich's avatar
Andrei Paskevich committed
173
exception LemmaFound
Andrei Paskevich's avatar
Andrei Paskevich committed
174
175
exception GoalFound

Francois Bobot's avatar
Francois Bobot committed
176
let push_decl task d =
Andrei Paskevich's avatar
Andrei Paskevich committed
177
178
179
180
  begin match task.task_decl.d_node with
    | Dprop (Pgoal,_,_) -> raise GoalFound
    | _ -> ()
  end;
Andrei Paskevich's avatar
minor    
Andrei Paskevich committed
181
  try mk_task d (Some task) (add_decl task.task_known d)
Francois Bobot's avatar
Francois Bobot committed
182
183
  with DejaVu -> task

184
let init_decl d =
Andrei Paskevich's avatar
minor    
Andrei Paskevich committed
185
  try mk_task d None (add_decl Mid.empty d)
Francois Bobot's avatar
Francois Bobot committed
186
187
188
  with DejaVu -> assert false

let add_decl opt d =
Andrei Paskevich's avatar
minor    
Andrei Paskevich committed
189
190
191
192
  begin match d.d_node with
    | Dprop (Plemma,_,_) -> raise LemmaFound
    | _ -> ()
  end;
Francois Bobot's avatar
Francois Bobot committed
193
  match opt with
194
195
    | Some task -> Some (push_decl task d)
    | None      -> Some (init_decl d)
Francois Bobot's avatar
Francois Bobot committed
196

Andrei Paskevich's avatar
minor    
Andrei Paskevich committed
197
198
let rec flat_theory used cl task th =
  if Sid.mem th.th_name used then used,cl,task else
Andrei Paskevich's avatar
Andrei Paskevich committed
199
200
201
  let acc = Sid.add th.th_name used, cl, task in
  List.fold_left flat_tdecl acc th.th_decls

Andrei Paskevich's avatar
minor    
Andrei Paskevich committed
202
and flat_tdecl (used, cl, task) = function
Andrei Paskevich's avatar
Andrei Paskevich committed
203
  | Use th ->
Andrei Paskevich's avatar
minor    
Andrei Paskevich committed
204
      flat_theory used cl task th
Andrei Paskevich's avatar
Andrei Paskevich committed
205
206
207
208
209
  | Clone (th,sl) ->
      used, add_clone cl th sl, task
  | Decl d ->
      begin match d.d_node with
        | Dprop (Pgoal,_,_) ->
Andrei Paskevich's avatar
minor    
Andrei Paskevich committed
210
            used, cl, task
Andrei Paskevich's avatar
Andrei Paskevich committed
211
212
213
214
215
216
217
218
219
220
221
        | Dprop (Plemma,pr,f) ->
            let d = create_prop_decl Paxiom pr f in
            used, cl, add_decl task d
        | Dprop (Paxiom,_,_) ->
            used, cl, add_decl task d
        | Dtype _ | Dlogic _ | Dind _  ->
            used, cl, add_decl task d
      end

let split_tdecl names (res, used, cl, task) = function
  | Use th ->
Andrei Paskevich's avatar
minor    
Andrei Paskevich committed
222
      let used, cl, task = flat_theory used cl task th in
Andrei Paskevich's avatar
Andrei Paskevich committed
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
      res, used, cl, task
  | Clone (th,sl) ->
      res, used, add_clone cl th sl, task
  | Decl d ->
      begin match d.d_node with
        | Dprop (Pgoal,pr,_)
          when option_apply true (Spr.mem pr) names ->
            let t = add_decl task d, cl in
            t :: res, used, cl, task
        | Dprop (Pgoal,_,_) ->
            res, used, cl, task
        | Dprop (Plemma,pr,f)
          when option_apply true (Spr.mem pr) names ->
            let d = create_prop_decl Pgoal pr f in
            let t = add_decl task d, cl in
            let d = create_prop_decl Paxiom pr f in
            t :: res, used, cl, add_decl task d
        | Dprop (Plemma,pr,f) ->
            let d = create_prop_decl Paxiom pr f in
            res, used, cl, add_decl task d
        | Dprop (Paxiom,_,_) ->
            res, used, cl, add_decl task d
        | Dtype _ | Dlogic _ | Dind _  ->
            res, used, cl, add_decl task d
      end
Andrei Paskevich's avatar
Andrei Paskevich committed
248

Andrei Paskevich's avatar
Andrei Paskevich committed
249
let split_theory th names =
Andrei Paskevich's avatar
Andrei Paskevich committed
250
251
  let acc = [], Sid.empty, empty_clone, None in
  let res,_,_,_ = List.fold_left (split_tdecl names) acc th.th_decls in
Andrei Paskevich's avatar
Andrei Paskevich committed
252
253
  res

Andrei Paskevich's avatar
Andrei Paskevich committed
254
let flat_theory task th =
Andrei Paskevich's avatar
minor    
Andrei Paskevich committed
255
  let _,_,task = flat_theory Sid.empty empty_clone task th in
Andrei Paskevich's avatar
Andrei Paskevich committed
256
257
  task

258
259
(* Generic utilities *)

260
261
262
let rec task_fold fn acc = function
  | Some task -> task_fold fn (fn acc task.task_decl) task.task_prev
  | None      -> acc
263

264
265
266
let rec task_iter fn = function
  | Some task -> fn task.task_decl; task_iter fn task.task_prev
  | None      -> ()
267
268
269

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

270
271
exception GoalNotFound

272
273
let task_goal = function
  | Some { task_decl = { d_node = Dprop (Pgoal,pr,_) }} -> pr
274
275
  | _ -> raise GoalNotFound