task.ml 7.35 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
27
28

(** Task *)

29
30
31
type clone_map = Stdecl.t Mid.t
type meta_map = Stdecl.t Mstr.t

32
33
34
type task = task_hd option

and task_hd = {
35
36
37
38
  task_decl  : tdecl;       (* last declaration *)
  task_prev  : task;        (* context *)
  task_known : known_map;   (* known identifiers *)
  task_clone : clone_map;   (* cloning history *)
39
  task_meta  : meta_map;    (* meta properties *)
40
  task_tag   : int;         (* unique task tag *)
41
42
}

43
44
let task_hd_equal = (==)

Andrei Paskevich's avatar
Andrei Paskevich committed
45
let task_equal t1 t2 = match t1, t2 with
46
  | Some t1, Some t2 -> task_hd_equal t1 t2
Andrei Paskevich's avatar
Andrei Paskevich committed
47
  | None, None -> true
48
  | _ -> false
Andrei Paskevich's avatar
Andrei Paskevich committed
49

50
module Hstask = Hashcons.Make (struct
51
  type t = task_hd
52

53
54
  let equal t1 t2 = td_equal t1.task_decl t2.task_decl &&
                  task_equal t1.task_prev t2.task_prev
55

56
  let hash task =
57
58
    let decl = task.task_decl.td_tag in
    let prev = option_apply 0 (fun t -> t.task_tag + 1) task.task_prev in
59
    Hashcons.combine decl prev
60
61

  let tag i task = { task with task_tag = i }
62
end)
63

64
let mk_task decl prev known clone meta = Some (Hstask.hashcons {
65
66
67
  task_decl  = decl;
  task_prev  = prev;
  task_known = known;
68
  task_clone = clone;
69
  task_meta  = meta;
70
  task_tag   = -1;
71
})
72

73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
let task_known = option_apply Mid.empty (fun t -> t.task_known)
let task_clone = option_apply Mid.empty (fun t -> t.task_clone)
let task_meta  = option_apply Mstr.empty (fun t -> t.task_meta)

let find_clone task th =
  try Mid.find th.th_name (task_clone task) with Not_found -> Stdecl.empty

let find_meta task t =
  try Mstr.find t (task_meta task) with Not_found -> Stdecl.empty

let add_decl task d td =
  let kn = known_add_decl (task_known task) d in
  mk_task td task kn (task_clone task) (task_meta task)

let add_clone task th td =
  let st = Stdecl.add td (find_clone task th) in
  let cl = Mid.add th.th_name st (task_clone task) in
  mk_task td task (task_known task) cl (task_meta task)

let add_meta task t td =
  let st = Stdecl.add td (find_meta task t) in
  let mt = Mstr.add t st (task_meta task) in
  mk_task td task (task_known task) (task_clone task) mt

(* add_decl with checks *)

Andrei Paskevich's avatar
Andrei Paskevich committed
99
exception LemmaFound
100
exception SkipFound
Andrei Paskevich's avatar
Andrei Paskevich committed
101
exception GoalFound
102
exception GoalNotFound
Andrei Paskevich's avatar
Andrei Paskevich committed
103

104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
let rec task_goal = function
  | Some task ->
      begin match task.task_decl.td_node with
        | Decl { d_node = Dprop (Pgoal,pr,_) } -> pr
        | Decl _ -> raise GoalNotFound
        | _ -> task_goal task.task_prev
      end
  | None -> raise GoalNotFound

let new_decl task d td = match d.d_node with
  | Dprop (Plemma,_,_) -> raise LemmaFound
  | Dprop (Pskip,_,_)  -> raise SkipFound
  | _ ->
      try ignore (task_goal task); raise GoalFound
      with GoalNotFound -> try add_decl task d td
      with KnownIdent _ -> task
Andrei Paskevich's avatar
Andrei Paskevich committed
120

121
122
(* declaration constructors + add_decl *)

123
124
let add_decl task d = new_decl task d (create_decl d)

125
126
127
128
129
130
131
132
133
let add_ty_decl tk dl = add_decl tk (create_ty_decl dl)
let add_logic_decl tk dl = add_decl tk (create_logic_decl dl)
let add_ind_decl tk dl = add_decl tk (create_ind_decl dl)
let add_prop_decl tk k p f = add_decl tk (create_prop_decl k p f)

let add_ty_decls tk dl = List.fold_left add_decl tk (create_ty_decls dl)
let add_logic_decls tk dl = List.fold_left add_decl tk (create_logic_decls dl)
let add_ind_decls tk dl = List.fold_left add_decl tk (create_ind_decls dl)

134
135
136
137
138
139
140
(* task constructors *)

let rec add_tdecl task td = match td.td_node with
  | Decl d -> new_decl task d td
  | Use th -> use_export task th
  | Clone (th,_) -> add_clone task th td
  | Meta (t,_) -> add_meta task t td
141

142
143
144
145
and flat_tdecl task td = match td.td_node with
  | Decl { d_node = Dprop (Plemma,pr,f) } -> add_prop_decl task Paxiom pr f
  | Decl { d_node = Dprop ((Pgoal|Pskip),_,_) } -> task
  | _ -> add_tdecl task td
146

147
148
149
150
151
and use_export task th =
  let td = create_null_clone th in
  if Stdecl.mem td (find_clone task th) then task else
  let task = List.fold_left flat_tdecl task th.th_decls in
  add_clone task th td
152
153
154

let clone_export = clone_theory flat_tdecl

155
156
157
158
159
160
let add_meta task t al = add_meta task t (create_meta t al)

(* split theory *)

let split_tdecl names (res,task) td = match td.td_node with
  | Decl { d_node = Dprop ((Pgoal|Plemma),pr,f) }
161
    when option_apply true (Spr.mem pr) names ->
162
163
164
165
      let res = add_prop_decl task Pgoal pr f :: res in
      res, flat_tdecl task td
  | _ ->
      res, flat_tdecl task td
Andrei Paskevich's avatar
Andrei Paskevich committed
166

Andrei Paskevich's avatar
Andrei Paskevich committed
167
let split_theory th names =
168
  fst (List.fold_left (split_tdecl names) ([],None) th.th_decls)
Andrei Paskevich's avatar
Andrei Paskevich committed
169

170
171
(* Generic utilities *)

172
173
174
let rec task_fold fn acc = function
  | Some task -> task_fold fn (fn acc task.task_decl) task.task_prev
  | None      -> acc
175

176
177
178
let rec task_iter fn = function
  | Some task -> fn task.task_decl; task_iter fn task.task_prev
  | None      -> ()
179

180
181
182
183
184
185
186
187
188
189
190
191
192
193
let task_tdecls = task_fold (fun acc td -> td::acc) []

let task_decls  = task_fold (fun acc td ->
  match td.td_node with Decl d -> d::acc | _ -> acc) []

(* TO BE REMOVED *)

let old_task_clone task =
  Mid.fold (fun _ -> Stdecl.fold (function
  | { td_node = Clone (_,cl) } ->
      Mid.fold (fun id id' m ->
        let s = try Mid.find id' m with Not_found -> Sid.empty in
        Mid.add id' (Sid.add id s) m) cl
  | _ -> assert false)) (task_clone task) Mid.empty
194

195
196
197
198
199
let old_task_use task =
  Mid.fold (fun _ -> Stdecl.fold (function
  | { td_node = Clone (th,cl) } -> (fun m ->
      if Mid.is_empty cl then Mid.add th.th_name th m else m)
  | _ -> assert false)) (task_clone task) Mid.empty
200

201
let rec last_use task = match task with
202
203
  | Some {task_decl={td_node=Clone(_,cl)}} when Mid.is_empty cl -> task
  | Some {task_prev=task} -> last_use task
204
205
206
  | None -> None

let rec last_clone task = match task with
207
208
  | Some {task_decl={td_node=Clone _}} -> task
  | Some {task_prev=task} -> last_clone task
209
210
  | None -> None

211
212
213
214
215
(* Exception reporting *)

let () = Exn_printer.register
  begin fun fmt exn -> match exn with
  | LemmaFound ->   Format.fprintf fmt "Task cannot contain a lemma"
216
  | SkipFound ->    Format.fprintf fmt "Task cannot contain a skip"
217
218
219
220
221
  | GoalFound ->    Format.fprintf fmt "The task already ends with a goal"
  | GoalNotFound -> Format.fprintf fmt "The task does not end with a goal"
  | _ -> raise exn
  end