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

Andrei Paskevich's avatar
Andrei Paskevich committed
43
let add_clone =
44
  let r = ref 0 in
Andrei Paskevich's avatar
Andrei Paskevich committed
45
  fun cl th sl ->
46
    incr r;
Andrei Paskevich's avatar
Andrei Paskevich committed
47
    { 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
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
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
128
129
130
131


(** Task *)

132
133
134
type task = task_hd option

and task_hd = {
135
  task_decl  : decl;
136
  task_prev  : task;
137
138
139
140
141
  task_known : decl Mid.t;
  task_tag   : int;
}

module Task = struct
142
  type t = task_hd
143
144

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

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

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

Andrei Paskevich's avatar
Andrei Paskevich committed
169
170
exception GoalFound

Francois Bobot's avatar
Francois Bobot committed
171
let push_decl task d =
172
  try
Francois Bobot's avatar
Francois Bobot committed
173
174
    let kn = add_decl task.task_known d in
    ignore (check_decl kn d);
Andrei Paskevich's avatar
Andrei Paskevich committed
175
176
177
178
    begin match task.task_decl.d_node with
      | Dprop (Pgoal,_,_) -> raise GoalFound
      | _ -> ()
    end;
Francois Bobot's avatar
Francois Bobot committed
179
180
181
    mk_task d (Some task) kn
  with DejaVu -> task

182
let init_decl d =
Francois Bobot's avatar
Francois Bobot committed
183
184
185
186
187
188
189
190
  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
191
192
    | Some task -> Some (push_decl task d)
    | None      -> Some (init_decl d)
Francois Bobot's avatar
Francois Bobot committed
193

Andrei Paskevich's avatar
Andrei Paskevich committed
194
let init_task =
Francois Bobot's avatar
Francois Bobot committed
195
  let add opt = function
196
    | Decl d -> add_decl opt d
Francois Bobot's avatar
Francois Bobot committed
197
    | _      -> opt
Andrei Paskevich's avatar
Andrei Paskevich committed
198
199
  in
  List.fold_left add None builtin_theory.th_decls
200

Andrei Paskevich's avatar
Andrei Paskevich committed
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
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 ->
218
              let res = (Some (push_decl task d), cl) :: res in
Andrei Paskevich's avatar
Andrei Paskevich committed
219
220
221
222
223
224
              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
225
              let res = (Some (push_decl task d), cl) :: res in
Andrei Paskevich's avatar
Andrei Paskevich committed
226
              let d = create_prop_decl Paxiom pr f in
Francois Bobot's avatar
Francois Bobot committed
227
              used, cl, res, push_decl task d
Andrei Paskevich's avatar
Andrei Paskevich committed
228
229
          | Dprop (Plemma,pr,f) ->
              let d = create_prop_decl Paxiom pr f in
Francois Bobot's avatar
Francois Bobot committed
230
              used, cl, res, push_decl task d
Andrei Paskevich's avatar
Andrei Paskevich committed
231
          | Dprop (Paxiom,_,_) ->
Francois Bobot's avatar
Francois Bobot committed
232
              used, cl, res, push_decl task d
Andrei Paskevich's avatar
Andrei Paskevich committed
233
          | Dtype _ | Dlogic _ | Dind _  ->
Francois Bobot's avatar
Francois Bobot committed
234
              used, cl, res, push_decl task d
Andrei Paskevich's avatar
Andrei Paskevich committed
235
236
        end

Andrei Paskevich's avatar
Andrei Paskevich committed
237
let split_theory th names =
238
239
240
  let use = Sid.add builtin_theory.th_name Sid.empty in
  let acc = use, empty_clone, [], of_option init_task in
  let _,_,res,_ = List.fold_left (use_export names) acc th.th_decls in
Andrei Paskevich's avatar
Andrei Paskevich committed
241
242
  res

243
244
(* Generic utilities *)

245
246
247
let rec task_fold fn acc = function
  | Some task -> task_fold fn (fn acc task.task_decl) task.task_prev
  | None      -> acc
248

249
250
251
let rec task_iter fn = function
  | Some task -> fn task.task_decl; task_iter fn task.task_prev
  | None      -> ()
252
253
254

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

255
256
exception GoalNotFound

257
258
let task_goal = function
  | Some { task_decl = { d_node = Dprop (Pgoal,pr,_) }} -> pr
259
260
  | _ -> raise GoalNotFound