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

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

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

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

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

Andrei Paskevich's avatar
Andrei Paskevich committed
44
let add_clone =
45
  let r = ref 0 in
Andrei Paskevich's avatar
Andrei Paskevich committed
46
  fun cl th sl ->
47
    incr r;
Andrei Paskevich's avatar
Andrei Paskevich committed
48
    { cl_map = merge_clone cl.cl_map th sl; cl_tag = !r }
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
82


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

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

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

Andrei Paskevich's avatar
Andrei Paskevich committed
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
128
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
129
130
131
132


(** Task *)

133
134
135
type task = task_hd option

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

module Task = struct
143
  type t = task_hd
144
145

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

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

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

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

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

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

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

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

Andrei Paskevich's avatar
Andrei Paskevich committed
238
let split_theory th names =
Francois Bobot's avatar
Francois Bobot committed
239
  let acc = Sid.empty, empty_clone, [], of_option init_task in
240
  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