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


(** Task *)

52
53
54
type task = task_hd option

and task_hd = {
55
  task_decl  : decl;
56
  task_prev  : task;
57
  task_known : known_map;
58
59
60
61
  task_tag   : int;
}

module Task = struct
62
  type t = task_hd
63
64

  let equal a b =
Andrei Paskevich's avatar
Andrei Paskevich committed
65
    a.task_decl == b.task_decl &&
66
67
68
69
70
71
72
73
74
75
    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
76
    Hashcons.combine task.task_decl.d_tag prev
77
78
79
80
81

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

Andrei Paskevich's avatar
Andrei Paskevich committed
82
let mk_task decl prev known = Htask.hashcons {
83
84
85
86
87
88
  task_decl  = decl;
  task_prev  = prev;
  task_known = known;
  task_tag   = -1;
}

Andrei Paskevich's avatar
Andrei Paskevich committed
89
exception LemmaFound
Andrei Paskevich's avatar
Andrei Paskevich committed
90
91
exception GoalFound

Francois Bobot's avatar
Francois Bobot committed
92
let push_decl task d =
Andrei Paskevich's avatar
Andrei Paskevich committed
93
94
95
96
  begin match task.task_decl.d_node with
    | Dprop (Pgoal,_,_) -> raise GoalFound
    | _ -> ()
  end;
97
  try mk_task d (Some task) (known_add_decl task.task_known d)
Andrei Paskevich's avatar
Andrei Paskevich committed
98
  with KnownIdent _ -> task
Francois Bobot's avatar
Francois Bobot committed
99

100
let init_decl d =
101
  try mk_task d None (known_add_decl Mid.empty d)
Andrei Paskevich's avatar
Andrei Paskevich committed
102
  with KnownIdent _ -> assert false
Francois Bobot's avatar
Francois Bobot committed
103
104

let add_decl opt d =
Andrei Paskevich's avatar
minor    
Andrei Paskevich committed
105
106
107
108
  begin match d.d_node with
    | Dprop (Plemma,_,_) -> raise LemmaFound
    | _ -> ()
  end;
Francois Bobot's avatar
Francois Bobot committed
109
  match opt with
110
111
    | Some task -> Some (push_decl task d)
    | None      -> Some (init_decl d)
Francois Bobot's avatar
Francois Bobot committed
112

Andrei Paskevich's avatar
minor    
Andrei Paskevich committed
113
let rec flat_theory used cl task th =
114
115
  if Mid.mem th.th_name used then used,cl,task else
  let acc = Mid.add th.th_name th used, cl, task in
Andrei Paskevich's avatar
Andrei Paskevich committed
116
117
  List.fold_left flat_tdecl acc th.th_decls

Andrei Paskevich's avatar
minor    
Andrei Paskevich committed
118
and flat_tdecl (used, cl, task) = function
Andrei Paskevich's avatar
Andrei Paskevich committed
119
  | Use th ->
Andrei Paskevich's avatar
minor    
Andrei Paskevich committed
120
      flat_theory used cl task th
Andrei Paskevich's avatar
Andrei Paskevich committed
121
122
123
124
125
  | 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
126
            used, cl, task
Andrei Paskevich's avatar
Andrei Paskevich committed
127
128
129
130
131
132
133
134
135
136
137
        | 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
138
      let used, cl, task = flat_theory used cl task th in
Andrei Paskevich's avatar
Andrei Paskevich committed
139
140
141
142
143
144
145
      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 ->
146
            let t = add_decl task d, cl, used in
Andrei Paskevich's avatar
Andrei Paskevich committed
147
148
149
150
151
152
            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
153
            let t = add_decl task d, cl, used in
Andrei Paskevich's avatar
Andrei Paskevich committed
154
155
156
157
158
159
160
161
162
163
            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
164

Andrei Paskevich's avatar
Andrei Paskevich committed
165
let split_theory th names =
166
  let acc = [], Mid.empty, empty_clone, None in
Andrei Paskevich's avatar
Andrei Paskevich committed
167
  let res,_,_,_ = List.fold_left (split_tdecl names) acc th.th_decls in
Andrei Paskevich's avatar
Andrei Paskevich committed
168
169
  res

Andrei Paskevich's avatar
Andrei Paskevich committed
170
let flat_theory task th =
171
  let _,_,task = flat_theory Mid.empty empty_clone task th in
Andrei Paskevich's avatar
Andrei Paskevich committed
172
173
  task

174
175
(* Generic utilities *)

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

180
181
182
let rec task_iter fn = function
  | Some task -> fn task.task_decl; task_iter fn task.task_prev
  | None      -> ()
183
184
185

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

186
187
exception GoalNotFound

188
189
let task_goal = function
  | Some { task_decl = { d_node = Dprop (Pgoal,pr,_) }} -> pr
190
191
  | _ -> raise GoalNotFound