case.ml 26.6 KB
Newer Older
1
open Trans
Sylvain Dailler's avatar
Sylvain Dailler committed
2
3
4
open Term
open Decl
open Theory
5
open Task
6
open Args_wrapper
Sylvain Dailler's avatar
Sylvain Dailler committed
7
8
open Reduction_engine

9
exception Arg_trans of string
10
exception Arg_trans_term of (string * Term.term * Term.term)
11
exception Arg_trans_pattern of (string * pattern * pattern)
12
13
exception Arg_trans_type of (string * Ty.ty * Ty.ty)
exception Arg_bad_hypothesis of (string * Term.term)
Sylvain Dailler's avatar
Sylvain Dailler committed
14
exception Cannot_infer_type of string
15

16
17
let debug_matching = Debug.register_info_flag "print_match"
  ~desc:"Print@ terms@ that@ were@ not@ successfully@ matched@ by@ ITP@ tactic@ apply."
18
19
20

let rec dup n x = if n = 0 then [] else x::(dup (n-1) x)

21
let gen_ident = Ident.id_fresh
Sylvain Dailler's avatar
Sylvain Dailler committed
22

Sylvain Dailler's avatar
Sylvain Dailler committed
23
(* From task [delta |- G] and term t, build the tasks:
24
   [delta, t] |- G] and [delta, not t | - G] *)
25
let case t name =
26
27
28
29
30
  let name =
    match name with
    | Some name -> name
    | None -> "h"
  in
31
32
  let h = Decl.create_prsymbol (gen_ident name) in
  let hnot = Decl.create_prsymbol (gen_ident name) in
33
34
  let t_not_decl = Decl.create_prop_decl Decl.Paxiom hnot (Term.t_not t) in
  let t_decl = Decl.create_prop_decl Decl.Paxiom h t in
35
  Trans.par [Trans.add_decls [t_decl]; Trans.add_decls [t_not_decl]]
36

Sylvain Dailler's avatar
Sylvain Dailler committed
37
(* From task [delta |- G] , build the tasks [delta, t | - G] and [delta] |- t] *)
38
let cut t name =
39
40
41
42
43
  let name =
    match name with
    | Some name -> name
    | None -> "h"
  in
44
  let h = Decl.create_prsymbol (gen_ident name) in
Sylvain Dailler's avatar
Sylvain Dailler committed
45
46
  let g_t = Decl.create_prop_decl Decl.Pgoal h t in
  let h_t = Decl.create_prop_decl Decl.Paxiom h t in
47
48
49
  let goal_cut = Trans.goal (fun _ _ -> [g_t]) in
  let goal = Trans.add_decls [h_t] in
  Trans.par [goal; goal_cut]
50

Sylvain Dailler's avatar
Assert.    
Sylvain Dailler committed
51
52
53
54
55
56
57
58
59
60
61
62
63
64
(* From task [delta |- G] , build the tasks [delta] |- t] and [delta, t | - G] *)
let assert_tac t name =
  let name =
    match name with
    | Some name -> name
    | None -> "h"
  in
  let h = Decl.create_prsymbol (gen_ident name) in
  let g_t = Decl.create_prop_decl Decl.Pgoal h t in
  let h_t = Decl.create_prop_decl Decl.Paxiom h t in
  let goal_cut = Trans.goal (fun _ _ -> [g_t]) in
  let goal = Trans.add_decls [h_t] in
  Trans.par [goal_cut; goal]

Sylvain Dailler's avatar
Sylvain Dailler committed
65
66
67
68
69
70
71
72
let subst_quant c tq x : term =
  let (vsl, tr, te) = t_open_quant tq in
  (match vsl with
  | hdv :: tl ->
      (try
        (let new_t = t_subst_single hdv x te in
        t_quant_close c tl tr new_t)
      with
73
      | Ty.TypeMismatch (ty1, ty2) ->
74
          raise (Arg_trans_type ("subst_quant", ty1, ty2)))
75
  | [] -> failwith "subst_quant: Should not happen, please report")
Sylvain Dailler's avatar
Sylvain Dailler committed
76
77

(* Transform the term (exists v, f) into f[x/v] *)
Sylvain Dailler's avatar
Sylvain Dailler committed
78
79
80
let subst_exist t x =
  match t.t_node with
  | Tquant (Texists, tq) ->
Sylvain Dailler's avatar
Sylvain Dailler committed
81
      subst_quant Texists tq x
82
  | _ -> raise (Arg_trans "subst_exist")
Sylvain Dailler's avatar
Sylvain Dailler committed
83

Sylvain Dailler's avatar
Sylvain Dailler committed
84
(* Transform the term (forall v, f) into f[x/v] *)
Sylvain Dailler's avatar
Sylvain Dailler committed
85
86
87
let subst_forall t x =
  match t.t_node with
  | Tquant (Tforall, tq) ->
Sylvain Dailler's avatar
Sylvain Dailler committed
88
      subst_quant Tforall tq x
89
  | _ -> raise (Arg_trans "subst_forall")
Sylvain Dailler's avatar
Sylvain Dailler committed
90

91
92
93
94
95
96
let exists_aux g x =
  let t = subst_exist g x in
  let pr_goal = create_prsymbol (gen_ident "G") in
  let new_goal = Decl.create_prop_decl Decl.Pgoal pr_goal t in
      [new_goal]

Sylvain Dailler's avatar
Sylvain Dailler committed
97
98
(* From task [delta |- exists x. G] and term t, build
   the task  [delta |- G[x -> t]].
Sylvain Dailler's avatar
Sylvain Dailler committed
99
   Return an error if x and t are not unifiable. *)
100
101
let exists x =
  Trans.goal (fun _ g -> exists_aux g x)
102

103
(* Return a new task with hypothesis name removed *)
104
let remove_task_decl (name: Ident.ident) : task trans =
105
106
107
  Trans.decl
    (fun d ->
     match d.d_node with
108
    | Dprop (Paxiom, pr, _) when (Ident.id_equal pr.pr_name name) ->
109
110
111
       []
    | _ -> [d])
    None
112
113

(* from task [delta, name:A |- G]  build the task [delta |- G] *)
114
115
let remove name =
  remove_task_decl name.pr_name
116

117
118
119
120
121
122
123
124
125
126
127
(* from task [delta, name1, name2, ... namen |- G] build the task [delta |- G] *)
let remove_list name_list =
  Trans.decl
    (fun d ->
      match d.d_node with
      | Dprop (Paxiom, pr, _) when
          (List.exists (fun x -> Ident.id_equal pr.pr_name x.pr_name) name_list) ->
        []
      | _ -> [d])
    None

Sylvain Dailler's avatar
Sylvain Dailler committed
128
(* from task [delta, name:forall x.A |- G,
129
     build the task [delta,name:forall x.A,name':A[x -> t]] |- G] *)
130
let instantiate (pr: Decl.prsymbol) t =
131
  let r = ref [] in
132
133
134
135
136
137
138
  Trans.decl
    (fun d ->
      match d.d_node with
      | Dprop (pk, dpr, ht) when Ident.id_equal dpr.pr_name pr.pr_name ->
          let t_subst = subst_forall ht t in
          let new_pr = create_prsymbol (Ident.id_clone dpr.pr_name) in
          let new_decl = create_prop_decl pk new_pr t_subst in
139
140
141
          r := [new_decl];
          [d]
      | Dprop (Pgoal, _, _) -> !r @ [d]
142
143
      | _ -> [d]) None

144
145
146
let term_decl d =
  match d.td_node with
  | Decl ({d_node = Dprop (_pk, _pr, t)}) -> t
147
  | _ -> raise (Arg_trans "term_decl")
148

149
150
151
152
153
154
155
156
157
158
159
160
161
162
let pr_prsymbol pr =
  match pr with
  | Decl {d_node = Dprop (_pk, pr, _t)} -> Some pr
  | _ -> None

(* Looks for the hypothesis name and return it. If not found return None *)
let find_hypothesis (name:Ident.ident) task =
  let ndecl = ref None in
  let _ = task_iter (fun x -> if (
    match (pr_prsymbol x.td_node) with
    | None -> false
    | Some pr -> Ident.id_equal pr.pr_name name) then ndecl := Some x) task in
  !ndecl

163
164
165
166
167
168
169
170
171
172
173
174
175
(* Do as intros: introduce all premises of hypothesis pr and return a triple
   (goal, list_premises, binded variables) *)
let intros f =
  let rec intros_aux lp lv f =
    match f.t_node with
    | Tbinop (Timplies, f1, f2) ->
        intros_aux (f1 :: lp) lv f2
    | Tquant (Tforall, fq) ->
        let vsl, _, fs = t_open_quant fq in
        intros_aux lp (List.fold_left (fun v lv -> Svs.add lv v) lv vsl) fs
    | _ -> (lp, lv, f) in
  intros_aux [] Svs.empty f

176

177
(* Apply:
Sylvain Dailler's avatar
Sylvain Dailler committed
178
179
180
181
182
183
184
   1) takes the hypothesis and introduce parts of it to keep only the last
      element of the implication. It gathers the premises and variables in a
      list.
   2) try to find a good substitution for the list of variables so that last
      element of implication is equal to the goal.
   3) generate new goals corresponding to premises with variables instantiated
      with values found in 2).
185
186
 *)
let apply pr : Task.task Trans.tlist = Trans.store (fun task ->
187
  let name = pr.pr_name in
188
  let g, task = Task.task_separate_goal task in
189
  let g = term_decl g in
190
  let d = find_hypothesis name task in
191
  if d = None then raise (Arg_hyp_not_found "apply");
192
193
  let d = Opt.get d in
  let t = term_decl d in
194
195
  let (lp, lv, nt) = intros t in
  let (_ty, subst) = try first_order_matching lv [nt] [g] with
196
197
198
199
  | Reduction_engine.NoMatch (Some (t1, t2)) ->
      (if (Debug.test_flag debug_matching) then
        Format.printf "Term %a and %a can not be matched. Failure in matching@."
          Pretty.print_term t1 Pretty.print_term t2
200
      else ()); raise (Arg_trans_term ("apply", t1, t2))
201
202
203
204
205
  | Reduction_engine.NoMatchpat (Some (p1, p2)) ->
      (if (Debug.test_flag debug_matching) then
        Format.printf "Term %a and %a can not be matched. Failure in matching@."
          Pretty.print_pat p1 Pretty.print_pat p2
      else ()); raise (Arg_trans_pattern ("apply", p1, p2))
206
  | Reduction_engine.NoMatch None -> raise (Arg_trans ("apply"))
207
  in
208
  let inst_nt = t_subst subst nt in
209
  if (Term.t_equal_nt_nl inst_nt g) then
210
211
212
213
214
    let nlp = List.map (t_subst subst) lp in
    let lt = List.map (fun ng -> Task.add_decl task (create_prop_decl Pgoal
                          (create_prsymbol (gen_ident "G")) ng)) nlp in
    lt
  else
215
    raise (Arg_trans_term ("apply", inst_nt, g)))
216

Sylvain Dailler's avatar
Sylvain Dailler committed
217
(* Replace all occurences of f1 by f2 in t *)
218
let replace_in_term = Term.t_replace
Sylvain Dailler's avatar
Sylvain Dailler committed
219
220
221
222
223
224
225
226
227
228
229
230
231
(* TODO be careful with label copy in t_map *)

let replace rev f1 f2 t =
  match rev with
  | true -> replace_in_term f1 f2 t
  | false -> replace_in_term f2 f1 t

(* Generic fold to be put in Trans ? TODO *)
let fold (f: decl -> 'a -> 'a) (acc: 'a): 'a Trans.trans =
  Trans.fold (fun t acc -> match t.task_decl.td_node with
  | Decl d -> f d acc
  | _ -> acc) acc

232
233
234
235
236
(* - If f1 unifiable to t with substitution s then return s.f2 and replace every
     occurences of s.f1 with s.f2 in the rest of the term
   - Else call recursively on subterms of t *)
(* If a substitution s is found then new premises are computed as e -> s.e *)
let replace_subst lp lv f1 f2 t =
Sylvain Dailler's avatar
Sylvain Dailler committed
237
238
239
  (* is_replced is common to the whole execution of replace_subst. Once an
     occurence is found, it changes to Some (s) so that only one instanciation
     is rewrritten during execution *)
240
241
242
243
244
245
246
247
248
  (* Note that we can't use an accumulator to do this *)
  let is_replaced = ref None in

  let rec replace lv f1 f2 t : Term.term =
  match !is_replaced with
  | Some subst -> replace_in_term (t_subst subst f1) (t_subst subst f2) t
  | None ->
    begin
      let fom = try Some (first_order_matching lv [f1] [t]) with
249
250
251
252
253
      | Reduction_engine.NoMatch (Some (t1, t2)) ->
        (if (Debug.test_flag debug_matching) then
          Format.printf "Term %a and %a can not be matched. Failure in matching@."
          Pretty.print_term t1 Pretty.print_term t2
        else ()); None
254
255
256
257
258
      | Reduction_engine.NoMatchpat (Some (p1, p2)) ->
        (if (Debug.test_flag debug_matching) then
          Format.printf "Term %a and %a can not be matched. Failure in matching@."
          Pretty.print_pat p1 Pretty.print_pat p2
        else ()); None
259
      | Reduction_engine.NoMatch None -> None in
260
261
262
263
264
265
266
267
268
269
270
271
272
273
        (match fom with
        | None -> t_map (fun t -> replace lv f1 f2 t) t
        | Some (_ty, subst) ->
        let sf1 = t_subst subst f1 in
        if (Term.t_equal sf1 t) then
        begin
          is_replaced := Some subst;
          t_subst subst f2
        end
        else
          replace lv f1 f2 t)
    end in
  let t = t_map (replace lv f1 f2) t in
  match !is_replaced with
274
  | None -> raise (Arg_trans "matching/replace")
275
276
  | Some subst ->
    (List.map (t_subst subst) lp, t)
Sylvain Dailler's avatar
Sylvain Dailler committed
277

278
let rewrite_in rev h h1 =
279
280
  let found_eq =
    (* Used to find the equality we are rewriting on *)
Sylvain Dailler's avatar
Sylvain Dailler committed
281
282
    fold (fun d acc ->
      match d.d_node with
283
284
285
      | Dprop (Paxiom, pr, t) when Ident.id_equal pr.pr_name h.pr_name ->
          let lp, lv, f = intros t in
          let t1, t2 = (match f.t_node with
Sylvain Dailler's avatar
Sylvain Dailler committed
286
          | Tapp (ls, [t1; t2]) when ls_equal ls ps_equ ->
287
288
              (* Support to rewrite from the right *)
              if rev then (t1, t2) else (t2, t1)
289
          | _ -> raise (Arg_bad_hypothesis ("rewrite", f))) in
290
          Some (lp, lv, t1, t2)
Sylvain Dailler's avatar
Sylvain Dailler committed
291
      | _ -> acc) None in
292
  (* Return instantiated premises and the hypothesis correctly rewritten *)
293
294
  let lp_new found_eq =
    match found_eq with
295
    | None -> raise (Arg_hyp_not_found "rewrite")
296
297
298
    | Some (lp, lv, t1, t2) ->
      fold (fun d acc ->
        match d.d_node with
Sylvain Dailler's avatar
Sylvain Dailler committed
299
300
301
        | Dprop (p, pr, t)
            when (Ident.id_equal pr.pr_name h1.pr_name &&
                 (p = Paxiom || p = Pgoal)) ->
302
303
304
          let lp, new_term = replace_subst lp lv t1 t2 t in
            Some (lp, create_prop_decl p pr new_term)
        | _ -> acc) None in
Sylvain Dailler's avatar
Sylvain Dailler committed
305
306
  (* Pass the premises as new goals. Replace the former toberewritten
     hypothesis to the new rewritten one *)
307
308
  let recreate_tasks lp_new =
    match lp_new with
309
    | None -> raise (Arg_trans "recreate_tasks")
310
    | Some (lp, new_term) ->
Sylvain Dailler's avatar
Sylvain Dailler committed
311
312
313
314
315
      let trans_rewriting =
        Trans.decl (fun d -> match d.d_node with
        | Dprop (p, pr, _t)
            when (Ident.id_equal pr.pr_name h1.pr_name &&
                 (p = Paxiom || p = Pgoal)) ->
316
317
          [new_term]
        | _ -> [d]) None in
Sylvain Dailler's avatar
Sylvain Dailler committed
318
319
320
321
322
323
324
325
326
327
328
329
      let list_par =
        List.map
          (fun e ->
            Trans.decl (fun d -> match d.d_node with
            | Dprop (p, pr, _t)
              when (Ident.id_equal pr.pr_name h1.pr_name &&
                    p = Paxiom) ->
                [d]
            | Dprop (Pgoal, _, _) ->
                [create_prop_decl Pgoal (Decl.create_prsymbol (gen_ident "G")) e]
            | _ -> [d] )
          None) lp in
330
331
332
333
      Trans.par (trans_rewriting :: list_par) in

  (* Composing previous functions *)
  Trans.bind (Trans.bind found_eq lp_new) recreate_tasks
Sylvain Dailler's avatar
Sylvain Dailler committed
334

335
336
337
338
339
340
let find_target_prop h : prsymbol trans =
  Trans.store (fun task ->
               match h with
                 | Some pr -> pr
                 | None -> Task.task_goal task)

341
let rewrite rev h h1 = Trans.bind (find_target_prop h1) (rewrite_in (not rev) h)
Sylvain Dailler's avatar
Sylvain Dailler committed
342
343
344
345

(* Replace occurences of t1 with t2 in h *)
let replace t1 t2 h =
  if not (Ty.ty_equal (t_type t1) (t_type t2)) then
346
    raise (Arg_trans_term ("replace", t1, t2))
Sylvain Dailler's avatar
Sylvain Dailler committed
347
348
  else
    (* Create a new goal for equality of the two terms *)
Sylvain Dailler's avatar
Sylvain Dailler committed
349
    let g = Decl.create_prop_decl Decl.Pgoal (create_prsymbol (gen_ident "G")) (t_app_infer ps_equ [t1; t2]) in
Sylvain Dailler's avatar
Sylvain Dailler committed
350
351
352
353
354
355
356
357
    let ng = Trans.goal (fun _ _ -> [g]) in
    let g = Trans.decl (fun d ->
      match d.d_node with
      | Dprop (p, pr, t) when (Ident.id_equal pr.pr_name h.pr_name && (p = Paxiom || p = Pgoal)) ->
          [create_prop_decl p pr (replace true t1 t2 t)]
      | _ -> [d]) None in
    Trans.par [g; ng]

Sylvain Dailler's avatar
Sylvain Dailler committed
358
359
360
361
let is_good_type t ty =
  try (Term.t_ty_check t (Some ty); true) with
  | _ -> false

362
let induction x bound env =
Sylvain Dailler's avatar
Sylvain Dailler committed
363
364
365
  let th = Env.read_theory env ["int"] "Int" in
  let le_int = Theory.ns_find_ls th.Theory.th_export ["infix <="] in
  let plus_int = Theory.ns_find_ls th.Theory.th_export ["infix +"] in
MARCHE Claude's avatar
MARCHE Claude committed
366
367
  let one_int =
    Term.t_const (Number.ConstInt (Number.int_const_dec "1")) Ty.ty_int in
Sylvain Dailler's avatar
Sylvain Dailler committed
368
369

  if (not (is_good_type x Ty.ty_int) || not (is_good_type bound Ty.ty_int)) then
370
    raise (Arg_trans "induction")
Sylvain Dailler's avatar
Sylvain Dailler committed
371
372
373
374
  else
    let lsx = match x.t_node with
    | Tvar lsx -> lsx.vs_name
    | Tapp (lsx, []) -> lsx.ls_name
375
    | _ -> raise (Arg_trans "induction") in
Sylvain Dailler's avatar
Sylvain Dailler committed
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390

  let le_bound = Trans.decl (fun d -> match d.d_node with
    | Dprop (Pgoal, _pr, _t) ->
        let nt = Term.t_app_infer le_int [x; bound] in
        let pr = create_prop_decl Paxiom (Decl.create_prsymbol (gen_ident "H")) nt in
        [pr; d]
    | _ -> [d]) None in

  let x_is_passed = ref false in
  let ge_bound =
    Trans.decl (fun d -> match d.d_node with
    | Dparam (ls) when (Ident.id_equal lsx ls.ls_name) ->
        (x_is_passed := true; [d])
    | Dprop (Pgoal, pr, t) ->
        if not (!x_is_passed) then
391
          raise (Arg_trans "induction")
Sylvain Dailler's avatar
Sylvain Dailler committed
392
393
394
395
396
397
        else
          let x_ge_bound_t = t_app_infer le_int [bound; x] in
          let x_ge_bound =
            create_prop_decl Paxiom (Decl.create_prsymbol (gen_ident "H")) x_ge_bound_t in
          let new_pr = create_prsymbol (gen_ident "G") in
          let new_goal = create_prop_decl Pgoal new_pr
398
              (replace_in_term x (t_app_infer plus_int [x; one_int]) t) in
Sylvain Dailler's avatar
Sylvain Dailler committed
399
400
          [x_ge_bound; create_prop_decl Paxiom pr t; new_goal]
    | Dprop (p, pr, t) ->
401
        if !x_is_passed then [create_prop_decl p pr (replace_in_term x (t_app_infer plus_int [x; one_int]) t)] else [d]
Sylvain Dailler's avatar
Sylvain Dailler committed
402
403
404
405
406
407
    (* TODO | Dlogic l ->
        if !x_is_passed then replace things inside and rebuild it else
        [d]*)
    | _ -> [d]) None in
  Trans.par [le_bound; ge_bound]

Sylvain Dailler's avatar
Sylvain Dailler committed
408
409
410
411
412
let create_constant ty =
  let fresh_name = Ident.id_fresh "x" in
  let ls = create_lsymbol fresh_name [] (Some ty) in
  (ls, create_param_decl ls)

Sylvain Dailler's avatar
Assert.    
Sylvain Dailler committed
413
let rec return_list list_types type_subst =
Sylvain Dailler's avatar
Sylvain Dailler committed
414
415
  match list_types with
  | [] -> []
Sylvain Dailler's avatar
Assert.    
Sylvain Dailler committed
416
417
418
419
420
421
422
423
424
  | hd :: tl ->
      create_constant (Ty.ty_inst type_subst hd) :: return_list tl type_subst

let my_ls_app_inst ls ty =
  match ls.ls_value, ty with
    | Some _, None -> raise (PredicateSymbolExpected ls)
    | None, Some _ -> raise (FunctionSymbolExpected ls)
    | Some vty, Some ty -> Ty.ty_match Ty.Mtv.empty vty ty
    | None, None -> Ty.Mtv.empty
Sylvain Dailler's avatar
Sylvain Dailler committed
425
426
427
428
429

let rec build_decls cls x =
  match cls with
  | [] -> []
  | (cs, _) :: tl ->
Sylvain Dailler's avatar
Assert.    
Sylvain Dailler committed
430
431
      let type_subst = my_ls_app_inst cs x.t_ty in
      let l = return_list cs.ls_args type_subst in
Sylvain Dailler's avatar
Sylvain Dailler committed
432
      let ht = t_equ x
Sylvain Dailler's avatar
Assert.    
Sylvain Dailler committed
433
           (t_app cs (List.map (fun x -> t_app_infer (fst x) []) l) x.t_ty) in
Sylvain Dailler's avatar
Sylvain Dailler committed
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
      let h = Decl.create_prsymbol (gen_ident "h") in
      let new_hyp = Decl.create_prop_decl Decl.Paxiom h ht in
      ((List.map snd l) @ [new_hyp]) :: build_decls tl x

(* This tactic acts on a term of algebraic type. It introduces one
   new goal per constructor of the type and introduce corresponding
   variables. It also introduce the equality between the term and
   its destruction in the context.
 *)
let destruct_alg (x: term) : Task.task Trans.tlist =
  let ty = x.t_ty in
  let r = ref [] in
  match ty with
  | None -> raise (Cannot_infer_type "destruct")
  | Some ty ->
    begin
      match ty.Ty.ty_node with
      | Ty.Tyvar _ -> raise (Cannot_infer_type "destruct")
      | Ty.Tyapp (ts, _) ->
        Trans.decl_l (fun d ->
          match d.d_node with
          | Ddata dls ->
              (try
                (let cls = List.assoc ts dls in
                r := build_decls cls x;
                [[d]]
                )
              with Not_found -> [[d]])
          | Dprop (Pgoal, _, _) ->
              if !r = [] then [[d]] else List.map (fun x -> x @ [d]) !r
          | _ -> [[d]]) None
    end

467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
(* Destruct the head term of an hypothesis if it is either
   conjunction, disjunction or exists *)
let destruct pr : Task.task Trans.tlist =
  Trans.decl_l (fun d ->
    match d.d_node with
    | Dprop (Paxiom, dpr, ht) when Ident.id_equal dpr.pr_name pr.pr_name ->
      begin
        match ht.t_node with
        | Tbinop (Tand, t1, t2) ->
          let new_pr1 = create_prsymbol (Ident.id_clone dpr.pr_name) in
          let new_decl1 = create_prop_decl Paxiom new_pr1 t1 in
          let new_pr2 = create_prsymbol (Ident.id_clone dpr.pr_name) in
          let new_decl2 = create_prop_decl Paxiom new_pr2 t2 in
          [[new_decl1;new_decl2]]
        | Tbinop (Tor, t1, t2) ->
          let new_pr1 = create_prsymbol (Ident.id_clone dpr.pr_name) in
          let new_decl1 = create_prop_decl Paxiom new_pr1 t1 in
          let new_pr2 = create_prsymbol (Ident.id_clone dpr.pr_name) in
          let new_decl2 = create_prop_decl Paxiom new_pr2 t2 in
          [[new_decl1];[new_decl2]]
        | Tquant (Texists, tb) ->
          begin
            let (vsl, tr, te) = Term.t_open_quant tb in
            match vsl with
            | x :: tl ->
                let ls = create_lsymbol (Ident.id_clone x.vs_name) [] (Some x.vs_ty) in
                let tx = fs_app ls [] x.vs_ty in
                let x_decl = create_param_decl ls in
                (try
                  let part_t = t_subst_single x tx te in
                  let new_t = t_quant_close Texists tl tr part_t in
                  let new_pr = create_prsymbol (Ident.id_clone dpr.pr_name) in
                  let new_decl = create_prop_decl Paxiom new_pr new_t in
                  [[d; x_decl; new_decl]]
                with
                | Ty.TypeMismatch (ty1, ty2) ->
503
                    raise (Arg_trans_type ("destruct_exists", ty1, ty2)))
504
505
506
507
508
509
            | [] -> raise (Arg_trans ("destruct_exists"))
          end
        | _ -> raise (Arg_trans ("destruct"))
      end
    | _ -> [[d]]) None

510

511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
let or_intro (left: bool) : Task.task Trans.trans =
  Trans.decl (fun d ->
    match d.d_node with
    | Dprop (Pgoal, pr, t) ->
      begin
        match t.t_node with
        | Tbinop (Tor, t1, t2) ->
          if left then
            [create_prop_decl Pgoal pr t1]
          else
            [create_prop_decl Pgoal pr t2]
        | _ -> [d]
      end
    | _ -> [d]) None

526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
(* TODO to be done ... *)
open Ident
open Ty
open Term
open Decl

(* TODO temporary for intros *)
let rec intros n pr f =
  if n = 0 then [create_prop_decl Pgoal pr f] else
  match f.t_node with
  (* (f2 \/ True) => _ *)
  | Tbinop (Timplies,{ t_node = Tbinop (Tor,f2,{ t_node = Ttrue }) },_)
      when Slab.mem Term.asym_label f2.t_label ->
        [create_prop_decl Pgoal pr f]
  | Tbinop (Timplies,f1,f2) ->
      (* split f1 *)
      (* f is going to be removed, preserve its labels and location in f2  *)
      let f2 = t_label_copy f f2 in
      let l = Split_goal.split_intro_right f1 in
      List.fold_right
        (fun f acc ->
           let id = create_prsymbol (id_fresh "H") in
           let d = create_prop_decl Paxiom id f in
           d :: acc)
        l
        (intros (n-1) pr f2)
  | Tquant (Tforall,fq) ->
      let vsl,_trl,f_t = t_open_quant fq in
      let intro_var subst vs =
        let ls = create_lsymbol (id_clone vs.vs_name) [] (Some vs.vs_ty) in
        Mvs.add vs (fs_app ls [] vs.vs_ty) subst,
        create_param_decl ls
      in
      let subst, decl = intro_var Mvs.empty (List.hd vsl) in
      if List.length vsl = 1 then
        begin
          let f = t_label_copy f (t_subst subst f_t) in
          decl :: intros (n-1) pr f
        end
      else
        let f = t_quant Tforall
            (t_close_quant (List.tl vsl) [] (t_subst subst f_t)) in
        decl :: intros (n-1) pr f
  | Tlet (t,fb) ->
      let vs,f = t_open_bound fb in
      let ls = create_lsymbol (id_clone vs.vs_name) [] (Some vs.vs_ty) in
      let f = t_subst_single vs (fs_app ls [] vs.vs_ty) f in
      let d = create_logic_decl [make_ls_defn ls [] t] in
      d :: intros (n-1) pr f
  | _ -> [create_prop_decl Pgoal pr f]

let intros n pr f =
  let tvs = t_ty_freevars Stv.empty f in
  let mk_ts tv () = create_tysymbol (id_clone tv.tv_name) [] NoDef in
  let tvm = Mtv.mapi mk_ts tvs in
  let decls = Mtv.map create_ty_decl tvm in
  let subst = Mtv.map (fun ts -> ty_app ts []) tvm in
  Mtv.values decls @ intros n pr (t_ty_subst subst Mvs.empty f)

let introduce_premises n = Trans.goal (intros n)

587
588
589
590
591
592
593
594
595
596
let t_replace_app unf ls_defn t =
  let (vl, tls) = ls_defn in
  match t.t_node with
  | Tapp (ls, tl) when ls_equal unf ls ->
      let mvs =
        List.fold_left2 (fun acc (v: vsymbol) (t: term) ->
          Mvs.add v t acc) Mvs.empty vl tl in
      t_subst mvs tls
  | _ -> t

Sylvain Dailler's avatar
Sylvain Dailler committed
597
598
let rec t_ls_replace ls ls_defn t =
  t_replace_app ls ls_defn (t_map (t_ls_replace ls ls_defn) t)
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619

let unfold unf h =
  let r = ref None in
  Trans.decl
    (fun d ->
      match d.d_node with
        (* Do not work on mutually recursive functions *)
      | Dlogic [(ls, ls_defn)] when ls_equal ls unf ->
          r := Some (open_ls_defn ls_defn);
          [d]
      | Dprop (k, pr, t) when pr_equal h pr  ->
        begin
          match !r with
          | None -> [d]
          | Some ls_defn ->
              let t = t_ls_replace unf ls_defn t in
              let new_decl = create_prop_decl k pr t in
              [new_decl]
        end
      | _ -> [d]) None

Sylvain Dailler's avatar
Sylvain Dailler committed
620
621
622
623
624
625
626
627
628
629
let clear_but (l: prsymbol list) =
  Trans.decl
    (fun d ->
      match d.d_node with
      | Dprop (Paxiom, pr, _t) when List.mem pr l ->
        [d]
      | Dprop (Paxiom, _pr, _t) ->
        []
      | _ -> [d]) None

630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672

let subst to_subst =
  let found_eq =
    fold (fun d acc ->
      match d.d_node with
      | Dprop (Paxiom, pr, t) ->
          let acc = (match t.t_node with
          | Tapp (ls, [t1; t2]) when ls_equal ls ps_equ ->
              (* Allow to rewrite from the right *)
              begin
                match t1.t_node, t2.t_node with
                | Tapp (ls, []), _ when ls_equal ls to_subst ->
                    Some (pr, t1, t2)
                | _, Tapp (ls, []) when ls_equal ls to_subst ->
                    Some (pr, t2, t1)
                | _ -> acc
              end
          | _ -> acc) in
          acc
      | _ -> acc) None in
  let subst found_eq =
    match found_eq with
    | None -> raise (Arg_trans "subst") (* TODO change exception *)
    | Some (pr_eq, t1, t2) ->
      begin
        Trans.decl (fun d ->
          match d.d_node with
          (* Remove equality over which we subst *)
          | Dprop (Paxiom, pr, _t) when pr_equal pr pr_eq  ->
            []
          (* Replace in all hypothesis *)
          | Dprop (kind, pr, t) ->
            [create_prop_decl kind pr (t_replace t1 t2 t)]
          (* TODO should replace every occurences of t1 everywhere *)
          | _ -> [d]) None
      end
  in
  Trans.bind found_eq subst

let () = wrap_and_register ~desc:"remove a literal using an equality on it"
    "subst"
    (Tlsymbol Ttrans) subst

Sylvain Dailler's avatar
Sylvain Dailler committed
673
674
675
676
677
678
(* TODO give a list of hypothesis *)
let () = wrap_and_register ~desc:"clear all axioms but the hypothesis argument"
    "clear_but"
    (Tprsymbol Ttrans) (fun x -> clear_but [x])


679
680
681
682
683
684
685
686
let () = wrap_and_register ~desc:"left transform a goal of the form A \\/ B into A"
    "left"
    (Ttrans) (or_intro true)

let () = wrap_and_register ~desc:"right transform a goal of the form A \\/ B into B"
    "right"
    (Ttrans) (or_intro false)

687
688
689
690
let () = wrap_and_register ~desc:"unfold ls pr: unfold logic symbol ls in hypothesis pr. Experimental." (* TODO *)
    "unfold"
    (Tlsymbol (Tprsymbol Ttrans)) unfold

691
692
693
694
let () = wrap_and_register ~desc:"intros n"
    "intros"
    (Tint Ttrans) introduce_premises

695
696
697
let use_th th =
  Trans.add_tdecls [Theory.create_use th]

698
let () = wrap_and_register
699
700
    ~desc:"case <term> [name] generates hypothesis 'name: term' in a first goal and 'name: ~ term' in a second one."
    "case"
701
    (Tformula (Topt ("as",Tstring Ttrans_l))) case
702

703
let () = wrap_and_register
704
705
    ~desc:"cut <term> [name] makes a cut with hypothesis 'name: term'"
    "cut"
706
    (Tformula (Topt ("as",Tstring Ttrans_l))) cut
707

Sylvain Dailler's avatar
Assert.    
Sylvain Dailler committed
708
709
710
711
712
let () = wrap_and_register
    ~desc:"cut <term> [name] makes an assert with hypothesis 'name: term'"
    "assert"
    (Tformula (Topt ("as",Tstring Ttrans_l))) assert_tac

713
let () = wrap_and_register
714
715
    ~desc:"exists <term> substitutes the variable quantified by exists with term"
    "exists"
716
    (Tterm Ttrans) exists
717

718
let () = wrap_and_register
719
720
    ~desc:"remove <prop> removes hypothesis named prop"
    "remove"
721
    (Tprsymbol Ttrans) remove
722

723
let () = wrap_and_register
724
    ~desc:"remove_list <prop list>: removes a list of hypothesis when given their names. Example syntax: remove_list a,b,c "
725
726
727
     "remove_list"
     (Tprlist Ttrans) remove_list

728
let () = wrap_and_register
729
730
    ~desc:"instantiate <prop> <term> generates a new hypothesis with first quantified variables of prop replaced with term "
    "instantiate"
731
    (Tprsymbol (Tterm Ttrans)) instantiate
732

733
let () = wrap_and_register
734
    ~desc:"apply <prop> applies prop to the goal" "apply"
735
    (Tprsymbol Ttrans_l) apply
736

737
let () = wrap_and_register
738
    ~desc:"duplicate <int> duplicates the goal int times" "duplicate"
739
    (Tint Ttrans_l) (fun x -> Trans.store (dup x))
740

741
let () = wrap_and_register
742
    ~desc:"use_th <theory> imports the theory" "use_th"
743
    (Ttheory Ttrans) use_th
744

745
746
747
748
749
750
751
let _ = wrap_and_register
    ~desc:"rewrite [<-] <name> [in] <name2> rewrites equality defined in name into name2" "rewrite"
    (Toptbool ("<-",(Tprsymbol (Topt ("in", Tprsymbol Ttrans_l))))) rewrite
  (* register_transform_with_args_l *)
  (*   ~desc:"rewrite [<-] <name> [in] <name2> rewrites equality defined in name into name2" *)
  (*   "rewrite" *)
  (*   (wrap_l (Toptbool ("<-",(Tprsymbol (Topt ("in", Tprsymbol Ttrans_l))))) rewrite) *)
752

753
let () = wrap_and_register
754
755
    ~desc:"replace <term1> <term2> <name> replaces occcurences of term1 by term2 in prop name"
    "replace"
756
    (Tterm (Tterm (Tprsymbol Ttrans_l))) replace
757

758
let () = wrap_and_register
759
760
    ~desc:"induction <term1> <term2> performs induction on int term1 from int term2"
    "induction"
761
    (Tterm (Tterm Tenvtrans_l)) induction
762

763
764
let () = wrap_and_register ~desc:"destruct <name> destructs the head constructor of hypothesis name"
    "destruct" (Tprsymbol Ttrans_l) destruct
Sylvain Dailler's avatar
Sylvain Dailler committed
765
766
767

let () = wrap_and_register ~desc:"destruct <name> destructs as an algebraic type"
    "destruct_alg" (Tterm Ttrans_l) destruct_alg