task.ml 7.42 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
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
Andrei Paskevich committed
197
let init_task =
Francois Bobot's avatar
Francois Bobot committed
198
  let add opt = function
199
    | Decl d -> add_decl opt d
Francois Bobot's avatar
Francois Bobot committed
200
    | _      -> opt
Andrei Paskevich's avatar
Andrei Paskevich committed
201
202
  in
  List.fold_left add None builtin_theory.th_decls
203

Andrei Paskevich's avatar
Andrei Paskevich committed
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
    | 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