compute.ml 9.58 KB
Newer Older
MARCHE Claude's avatar
MARCHE Claude committed
1
2
3
4
5
6

open Term
open Decl
open Task
open Theory

7
8
(* obsolete

MARCHE Claude's avatar
MARCHE Claude committed
9
10
11
12
13
14
15
16
type env = {
  tknown : Decl.known_map;
  vsenv : term Mvs.t;
}

let bind_vs v t env =
  { env with vsenv = Mvs.add v t env.vsenv }

17
18
19
20
21
let multibind_vs l tl env =
  try
    List.fold_right2 bind_vs l tl env
  with Invalid_argument _ -> assert false

MARCHE Claude's avatar
MARCHE Claude committed
22
23
24
let get_vs env vs =
  try Mvs.find vs env.vsenv
  with Not_found ->
25
26
27
28
29
30
    Format.eprintf "[Compute] logic variable %s not found in env@." vs.vs_name.Ident.id_string;
    raise Not_found




MARCHE Claude's avatar
MARCHE Claude committed
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57

exception NoMatch
exception Undetermined
exception CannotCompute

let rec matching env t p =
  match p.pat_node with
  | Pwild -> env
  | Pvar v -> bind_vs v t env
  | Por(p1,p2) ->
    begin
      try matching env t p1
      with NoMatch -> matching env t p2
    end
  | Pas(p,v) -> matching (bind_vs v t env) t p
  | Papp(ls1,pl) ->
    match t.t_node with
      | Tapp(ls2,tl) ->
        if ls_equal ls1 ls2 then
          List.fold_left2 matching env tl pl
        else
          if ls2.ls_constr > 0 then raise NoMatch
          else raise Undetermined
      | _ -> raise Undetermined



58
59
60
61
62
63
64
65
66
67
68

(* builtin symbols *)

let builtins = Hls.create 17

let ls_minus = ref ps_equ (* temporary *)

(* all builtin functions *)

let const_equality c1 c2 =
  match c1,c2 with
69
  | Number.ConstInt i1, Number.ConstInt i2 ->
70
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
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
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
    BigInt.eq (Number.compute_int i1) (Number.compute_int i2)
  | _ -> raise Undetermined

let value_equality t1 t2 =
  match (t1.t_node,t2.t_node) with
  | Tconst c1, Tconst c2 -> const_equality c1 c2
  | _ -> raise Undetermined

let to_bool b = if b then t_true else t_false

let eval_equ _ls l _ty =
  match l with
  | [t1;t2] ->
    begin
      try to_bool (value_equality t1 t2)
      with Undetermined -> t_equ t1 t2
    end
  | _ -> assert false


let eval_true _ls _l _ty = t_true

let eval_false _ls _l _ty = t_false

exception NotNum

let big_int_of_const c =
  match c with
    | Number.ConstInt i -> Number.compute_int i
    | _ -> raise NotNum

let const_of_big_int n =
  t_const (Number.ConstInt (Number.int_const_dec (BigInt.to_string n)))

let eval_int_op op ls l ty =
  match l with
  | [{t_node = Tconst c1};{t_node = Tconst c2}] ->
    begin
      try const_of_big_int (op (big_int_of_const c1) (big_int_of_const c2))
      with NotNum | Division_by_zero ->
        t_app ls l ty
    end
  | _ -> t_app ls l ty


let built_in_theories =
  [ ["bool"],"Bool", [],
    [ "True", None, eval_true ;
      "False", None, eval_false ;
    ] ;
    ["int"],"Int", [],
    [ "infix +", None, eval_int_op BigInt.add;
      "infix -", None, eval_int_op BigInt.sub;
      "infix *", None, eval_int_op BigInt.mul;
(*
      "prefix -", Some ls_minus, eval_int_uop BigInt.minus;
      "infix <", None, eval_int_rel BigInt.lt;
      "infix <=", None, eval_int_rel BigInt.le;
      "infix >", None, eval_int_rel BigInt.gt;
      "infix >=", None, eval_int_rel BigInt.ge;
*)
    ] ;
(*
    ["int"],"MinMax", [],
    [ "min", None, eval_int_op BigInt.min;
      "max", None, eval_int_op BigInt.max;
    ] ;
    ["int"],"ComputerDivision", [],
    [ "div", None, eval_int_op BigInt.computer_div;
      "mod", None, eval_int_op BigInt.computer_mod;
    ] ;
    ["int"],"EuclideanDivision", [],
    [ "div", None, eval_int_op BigInt.euclidean_div;
      "mod", None, eval_int_op BigInt.euclidean_mod;
    ] ;
    ["map"],"Map", ["map", builtin_map_type],
    [ "const", Some ls_map_const, eval_map_const;
      "get", Some ls_map_get, eval_map_get;
      "set", Some ls_map_set, eval_map_set;
    ] ;
*)
  ]

let add_builtin_th env (l,n,t,d) =
  try
    let th = Env.find_theory env l n in
    List.iter
      (fun (id,r) ->
        let ts = Theory.ns_find_ts th.Theory.th_export [id] in
        r ts)
      t;
    List.iter
      (fun (id,r,f) ->
        let ls = Theory.ns_find_ls th.Theory.th_export [id] in
        Hls.add builtins ls f;
        match r with
          | None -> ()
          | Some r -> r := ls)
      d
  with Not_found ->
    Format.eprintf "[Compute] theory %s not found@." n

let get_builtins env =
173
  Hls.clear builtins;
174
175
176
177
178
179
180
181
182
  Hls.add builtins ps_equ eval_equ;
  List.iter (add_builtin_th env) built_in_theories





(* computation in terms *)

MARCHE Claude's avatar
MARCHE Claude committed
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
let rec compute_in_term env t =
  let eval_rec = compute_in_term env in
  match t.t_node with
  | Ttrue | Tfalse | Tconst _ -> t
  | Tbinop(Tand,t1,t2) ->
    t_and_simp (eval_rec t1) (eval_rec t2)
  | Tbinop(Tor,t1,t2) ->
    t_or_simp (eval_rec t1) (eval_rec t2)
  | Tbinop(Timplies,t1,t2) ->
    t_implies_simp (eval_rec t1) (eval_rec t2)
  | Tbinop(Tiff,t1,t2) ->
    t_iff_simp (eval_rec t1) (eval_rec t2)
  | Tnot(t1) -> t_not_simp (eval_rec t1)
  | Tvar vs ->
    begin
      try get_vs env vs
      with Not_found -> t
    end
201
202
  | Tapp(ls,tl) ->
    compute_app env ls (List.map eval_rec tl) t.t_ty
MARCHE Claude's avatar
MARCHE Claude committed
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
  | Tif(t1,t2,t3) ->
    let u1 = eval_rec t1 in
    begin match u1.t_node with
    | Ttrue -> eval_rec t2
    | Tfalse -> eval_rec t3
    | _ -> t_if u1 t2 t3
    end
  | Tlet(t1,tb) ->
    let u1 = eval_rec t1 in
    let v,t2 = t_open_bound tb in
    let u2 = compute_in_term (bind_vs v u1 env) t2 in
    t_let_close_simp v u1 u2
  | Tcase(t1,tbl) ->
    let u1 = eval_rec t1 in
    compute_match env u1 tbl
  | Teps _ -> t
  | Tquant _ -> t


and compute_match env u tbl =
  let rec iter tbl =
    match tbl with
    | [] ->
226
      Format.eprintf "[Compute] fatal error: pattern matching not exhaustive in evaluation.@.";
MARCHE Claude's avatar
MARCHE Claude committed
227
228
229
230
231
232
233
234
235
      assert false
    | b::rem ->
      let p,t = t_open_branch b in
      try
        let env' = matching env u p in
        compute_in_term env' t
      with NoMatch -> iter rem
  in
  try iter tbl with Undetermined ->
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
    t_case u tbl


and compute_app env ls tl ty =
  try
    let f = Hls.find builtins ls in
    f ls tl ty
  with Not_found ->
    try
      let d = Ident.Mid.find ls.ls_name env.tknown in
      match d.Decl.d_node with
      | Decl.Dtype _ | Decl.Dprop _ -> assert false
      | Decl.Dlogic dl ->
        (* regular definition *)
        let d = List.assq ls dl in
        let l,t = Decl.open_ls_defn d in
        let env' = multibind_vs l tl env in
        compute_in_term env' t
      | Decl.Dparam _ | Decl.Dind _ ->
        t_app ls tl ty
      | Decl.Ddata dl ->
        (* constructor or projection *)
        match tl with
        | [ { t_node = Tapp(ls1,tl1) } ] ->
          (* if ls is a projection and ls1 is a constructor,
261

262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
             we should compute that projection *)
          let rec iter dl =
            match dl with
            | [] -> t_app ls tl ty
            | (_,csl) :: rem ->
              let rec iter2 csl =
                match csl with
                | [] -> iter rem
                | (cs,prs) :: rem2 ->
                  if ls_equal cs ls1
                  then
                    (* we found the right constructor *)
                    let rec iter3 prs tl1 =
                      match prs,tl1 with
                      | (Some pr)::prs, t::tl1 ->
                        if ls_equal ls pr
                        then (* projection found! *) t
                        else
                          iter3 prs tl1
                      | None::prs, _::tl1 ->
                        iter3 prs tl1
                      | _ -> t_app ls tl ty
                    in iter3 prs tl1
                  else iter2 rem2
              in iter2 csl
          in iter dl
        | _ -> t_app ls tl ty
    with Not_found ->
      Format.eprintf "[Compute] definition of logic symbol %s not found@."
        ls.ls_name.Ident.id_string;
      t_app ls tl ty
MARCHE Claude's avatar
MARCHE Claude committed
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313

let compute_in_decl km d =
  match d.d_node with
  | Dprop(k,pr,f) ->
    let t = compute_in_term { tknown = km; vsenv = Mvs.empty } f in
    create_prop_decl k pr t
  | _ -> d

let compute_in_tdecl km d =
  match d.td_node with
  | Decl d -> create_decl (compute_in_decl km d)
  | _ -> d

let rec compute_in_task task =
  match task with
  | Some d ->
    add_tdecl
      (compute_in_task d.task_prev)
      (compute_in_tdecl d.task_known d.task_decl)
  | None -> None

314
let compute env task =
MARCHE Claude's avatar
MARCHE Claude committed
315
316
317
318
319
320
  let task = compute_in_task task in
  match task with
  | Some
      { task_decl =
          { td_node = Decl { d_node = Dprop (Pgoal, _, f) }}
      } ->
321
    get_builtins env;
MARCHE Claude's avatar
MARCHE Claude committed
322
323
324
325
326
327
328
    begin match f.t_node with
    | Ttrue -> []
    | _ -> [task]
    end
  | _ -> assert false

let () =
329
  Trans.register_env_transform_l "compute"
330
    (fun env -> Trans.store (compute env))
MARCHE Claude's avatar
MARCHE Claude committed
331
    ~desc:"Compute@ as@ much@ as@ possible"
332

333
  *)
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348


(* compute with rewrite rules *)



let collect_rule_decl prs e d =
  match d.Decl.d_node with
    | Decl.Dtype _ | Decl.Ddata _ | Decl.Dparam _ | Decl.Dind  _
    | Decl.Dlogic _ -> e
    | Decl.Dprop(_, pr, t) ->
      if Decl.Spr.mem pr prs then
        Reduction_engine.add_rule t e
      else e

349
let collect_rules env km prs t =
350
351
352
353
  Task.task_fold
    (fun e td -> match td.Theory.td_node with
      | Theory.Decl d -> collect_rule_decl prs e d
      | _ -> e)
354
    (Reduction_engine.create env km) t
355

356
let normalize_goal env (prs : Decl.Spr.t) task =
357
358
359
360
361
  match task with
  | Some
      { task_decl =
          { td_node = Decl { d_node = Dprop (Pgoal, pr, f) } };
        task_prev = prev;
362
        task_known = km;
363
      } ->
364
    let engine = collect_rules env km prs task in
365
366
367
368
369
370
371
372
373
374
375
376
377
    let f = Reduction_engine.normalize engine f in
    begin match f.t_node with
    | Ttrue -> []
    | _ ->
      let d = Decl.create_prop_decl Pgoal pr f in
      [Task.add_decl prev d]
    end
  | _ -> assert false


let meta = Theory.register_meta "rewrite" [Theory.MTprsymbol]
  ~desc:"Declares@ the@ given@ prop@ as@ a@ rewrite@ rule."

378
379
let normalize_transf env =
  Trans.on_tagged_pr meta (fun prs -> Trans.store (normalize_goal env prs))
380

381
let () = Trans.register_env_transform_l "compute_in_goal" normalize_transf
382
  ~desc:"Normalize@ terms@ with@ respect@ to@ rewrite@ rules@ declared as metas"