MAJ terminée. Nous sommes passés en version 14.6.2 . Pour consulter les "releases notes" associées c'est ici :

https://about.gitlab.com/releases/2022/01/11/security-release-gitlab-14-6-2-released/
https://about.gitlab.com/releases/2022/01/04/gitlab-14-6-1-released/

induction.ml 31.7 KB
Newer Older
Leon Gondelman's avatar
Leon Gondelman committed
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
(**************************************************************************)
(*                                                                        *)
(*  Copyright (C) 2010-2012                                               *)
(*    François Bobot                                                      *)
(*    Jean-Christophe Filliâtre                                           *)
(*    Claude Marché                                                       *)
(*    Guillaume Melquiond                                                 *)
(*    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 Ident
21
open Ty
Leon Gondelman's avatar
Leon Gondelman committed
22
23
24
25
26
open Term
open Decl
open Theory
open Task

Leon Gondelman's avatar
Leon Gondelman committed
27

28
29
(*********************************************************)
(*******      Data type induction principle      *********)
30
(*********************************************************)
31
32

(**********************************************************************)
33
(*Algebraic datatype induction scheme *)
34
type tyscheme = (pattern * Svs.t) list
35

36
37
38
39
40
41
42
43
44

(*A induction scheme variable*)
type vlex =
    {vs: vsymbol;       (*variable*)
     lq: vsymbol list;  (*left immediate neutral quantifiers *)
     rq: vsymbol list;  (*generalized neutral and induction quantifiers *)
     ts: tyscheme       (*type scheme following its definition*)
    }

45
46
47
48
49
50
51
52
53
54
55
56
57
(*Definitions for Svsl : "Set of variable symbol list". 
  Each list corresponds to the largest prefix of some recursive function
  decreasing argument list, where arguments are instanciated 
  with call actual parameters and recognized as possibles induction candidates
  if they are variables themselves. 
  
  Note, that first are compared lists length, otherwise comparison is made on 
  lexicographic order of vsymbols. Empty list corresponds to non-recurisve 
  functions calls  
  
  This definitions and methods using them are without use if some induction tags
  are provided in the goal by user.
*)  
58
59
60
61
62
63
module VsList =
struct
 
  type t = vsymbol list
  let hash = Hashcons.combine_list vs_hash 3
  let equal = Util.list_all2 vs_equal
64
  let cmp_vs vs1 vs2 = Pervasives.compare (vs_hash vs2) (vs_hash vs1)
65
66
67
68
69
70
71
  let compare t1 t2 = 
    let rec aux t1 t2 = match t1,t2 with
      | [],[] -> 0
      | v1 :: q1, v2 :: q2 ->
	if vs_equal v1 v2 
	then aux q1 q2 
	else cmp_vs v1 v2
72
      | _ -> assert false; 
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
    in
    if List.length t1 < List.length t2 then -1
    else if List.length t1 > List.length t2 then 1
    else aux t1 t2
end

module Mvsl = Stdlib.Map.Make(VsList)
module Svsl = Mvsl.Set    

(**************************** PRINTING ***************************************)
let debug = Debug.register_flag "induction"
let debug_verbose = Debug.register_flag "induction-verbose"

let print_ty_skm skm =
  List.iter
    (fun (p,svs) ->
      Format.printf "@[| %a : @]" Pretty.print_pat p;
      Svs.iter (Format.printf "%a " Pretty.print_vs) svs;
      Format.printf "@.")
    skm;
  Pretty.forget_all ()

let print_vset vset =
  let aux vl =
    Format.printf "[ ";
    List.iter (Format.printf "%a " Pretty.print_vs) vl;
    Format.printf "] " 
  in
  Format.printf "************** t_candidates_lex *****************\n";
  Format.printf "Candidates found : %d @." (Svsl.cardinal vset);
  Format.printf "Candidates : [ ";
  Svsl.iter (fun vl -> aux vl) vset;
  Format.printf "]\n@.";
  Pretty.forget_all ()
    
let print_heuristic_lex vl =
  let _,ivm = List.fold_left (fun (i,m) v -> 
    (i+1, Mvs.add v i m)) (0,Mvs.empty) vl in
  Format.printf "**************** heuristic_lex ******************\n";
112
  Format.printf "Induction variables (in lexicographic order): [ ";
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
  List.iter (Format.printf "%a " Pretty.print_vs) vl;
  Format.printf "]@.";
  Format.printf "Lex. order map : [ ";
  Mvs.iter (fun v i -> Format.printf "%a -> %d; " Pretty.print_vs v i) ivm;
  Format.printf "]\n@.";
  Pretty.forget_all ()

let print_lex lexl =
  let rec aux = function
    | [] -> ()
    | v :: tl ->
      Format.printf "\n%a : [ " Pretty.print_vs v.vs;
      List.iter (Format.printf "%a " Pretty.print_vs) v.lq;
      Format.printf "] [ ";
      List.iter (Format.printf "%a " Pretty.print_vs) v.rq;
      Format.printf "]@.";
      Format.printf "--- Type scheme --- \n";
      print_ty_skm v.ts;
      Format.printf "------------------- \n";
      aux tl
  in
  Format.printf "******************* qsplit_lex ******************\n";
  Format.printf "Induction variables (in the initial order): ";
  List.iter (fun v -> Format.printf "%a " Pretty.print_vs v.vs ) lexl;
  Format.printf "@.(Variable) (Introduced) (Generalized)\n";
  aux lexl;
  Pretty.forget_all ()


(**********************************************************************)
143
let tyscheme_inst f (km : Decl.known_map) x tx  =
144
145
  let inst_branch = (fun (p, vset) ->
    t_close_branch p ( Svs.fold (fun v tacc ->
146
      (Term.t_implies (t_subst_single x (t_var v) tx) tacc )) vset tx))
147
  in
148
149
150
151
152
153
154
155
156
  t_case (t_var x) (List.map inst_branch ((f km x tx) : tyscheme))


let split_quantifiers x qvl =
  let rec aux left = function
    | hd :: tl when vs_equal x hd -> List.rev left, tl
    | hd :: tl -> aux (hd :: left) tl
    | [] -> assert false
  in aux [] qvl
157

158

159
160
let decompose_forall t =
  let rec aux qvl_acc t = match t.t_node with
Leon Gondelman's avatar
Leon Gondelman committed
161
162
163
164
165
    | Tquant (Tforall, qt) ->
      let qvl, _, t = t_open_quant qt in aux (qvl_acc @ qvl) t
    | _ -> qvl_acc, t
  in
  let qvl, t = aux [] t in (List.fold_right Svs.add qvl Svs.empty), qvl, t
166

167
168
169
170
171
172
173
174
175
176

let t_candidates filter km qvs t =
  let int_candidate = (fun acc t ->
    match t.t_node with
      | Tvar x when Svs.mem x qvs && ty_equal x.vs_ty ty_int ->
	Svs.add x acc
      | _ -> acc)
  in
  let arg_candidate = (fun acc t ->
    match t.t_node with
177
      | Tvar x when Svs.mem x qvs ->
178
	begin match x.vs_ty.ty_node with
179
	  | Tyvar _ -> acc
180
181
182
	  | Tyapp _ -> Svs.add x acc
	end
      | _ -> acc)
183
  in
184
185
186
187
188
  let defn_candidate = (fun vs_acc ls tl ->
    match (find_logic_definition km ls) with
      | Some defn ->
	let vs_acc = List.fold_left int_candidate vs_acc tl in
	begin match ls_defn_decrease defn with
189
190
191
192
	  | [i] -> arg_candidate vs_acc (List.nth tl i)
	  | h :: _ ->
	    arg_candidate vs_acc (List.nth tl h)
	  | _ ->  vs_acc
193
194
195
	end
      | None -> vs_acc)
  in
196
197
  let rec t_candidate vs_acc t =
    let vs_acc = match t.t_node with
198
      | Tapp (ls, tl) -> defn_candidate vs_acc ls tl
199
      | _ ->  vs_acc
200
    in t_fold t_candidate vs_acc t
201
  in Svs.filter filter (t_candidate Svs.empty t)
202

203
let heuristic_svs vset = Svs.choose vset
204

205
let filter_tydef v = not (ty_equal v.vs_ty ty_int)
206

207
(* Decl.known_map -> Term.vsymbol -> Term.term -> tyscheme *)
208
let tyscheme_vsty km x (_t : Term.term) =
209
  let ts,ty = match x.vs_ty.ty_node with
210
211
    | Tyapp _ when ty_equal x.vs_ty ty_int -> assert false
    | Tyvar _ ->   assert false
212
213
    | Tyapp (ts, _) -> ts, ty_app ts (List.map ty_var ts.ts_args)
  in
214
215
  let sigma = ty_match Mtv.empty ty x.vs_ty in
  let ty_str ty =
216
217
218
    let s = match ty.ty_node with
      | Tyapp (ts, _) -> ts.ts_name.id_string
      | Tyvar tv -> tv.tv_name.id_string
219
    in if s = "" then "x" else String.make 1 s.[0]
220
  in
221
  let ty_vs ty =
222
    let ty = ty_inst sigma ty in
223
    Term.create_vsymbol (Ident.id_fresh (ty_str ty)) ty
224
  in
225
  let tyscheme_constructor (ls, _) =
226
227
    let vlst = List.map ty_vs ls.ls_args in
    let plst = List.map pat_var vlst in
228
229
230
    let vset = List.fold_left
      (fun s v ->
	if ty_equal x.vs_ty v.vs_ty then Svs.add v s else s)
231
      Svs.empty vlst
232
    in pat_app ls plst x.vs_ty, vset
233
234
235
  in
  let cl = find_constructors km ts in
  ((List.map tyscheme_constructor cl) : tyscheme)
236
237
238


let induction_ty km t0 =
239
  let qvs, qvl, t = decompose_forall t0 in
240
  let vset = t_candidates filter_tydef km qvs t in
241
  if Svs.is_empty vset then [t0]
242
  else
243
244
245
246
247
248
    let x  =  heuristic_svs vset in
    let qvl1, qvl2 = split_quantifiers x qvl in
    let t = t_forall_close qvl2 [] t in
    let tcase = tyscheme_inst tyscheme_vsty km x t in
    let tcase = t_forall_close [x] [] tcase in
    let tcase = t_forall_close qvl1 [] tcase in
249
250
251
252
253
254
    if Debug.test_flag debug then
      begin

	Format.printf "Old Task: %a \n@." Pretty.print_term t0;
	Format.printf "New Task: %a \n@." Pretty.print_term tcase
      end;
255
    [tcase]
256

257
258
259
260
261
(*****************************************************************************)
(******************** INDUCTION BASED ON TYPE DEFINITIONS ********************)
(************************* WITH LEXICOGRAPHIC ORDER **************************)
(*****************************************************************************)

262
263
264
let qvl_labeled qvl = 
  List.filter (fun v -> 
    let slab = Slab.filter (fun v -> 
265
266
      v.lab_string = "induction") v.vs_name.id_label 
    in not (Slab.is_empty slab)) qvl
267
268


269
(* This function collects lists of variables corresponding to
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
   some recursive functions call parameters into the body of formula, 
   if no user made induction tag is provided. 
   
   If some user tags are provided, this function will return the corresponding 
   list of variables will be returned according to the order of tags 
   (from left to right).  
   
   Otherwise, each list respects the lexicographic order of the corresponding 
   recusrive function in which decrease its formal arguments.
   
   Note that one list contain the biggest lexicographic order prefix where all
   actual parameters are variables. For example, if function f(x,a,y,b,z) 
   decreases on [a;b], but is called with some not-variable term T for argument
   b, then the resulting list will be [a]. 
*)
let t_candidates_lex km qvs labeledvl t =
  (* let int_candidates _tl acc = acc 
   List.fold_left (fun acc t -> match t.t_node with
288
289
     | Tvar x when Svs.mem x qvs && ty_equal x.vs_ty ty_int -> 
     Svls.add [x] acc
290
     | _ -> acc) acc tl *) 
291
292
293
294
295
296
297
298
299
300
301
302
  let rec_candidates il tl acc =
    let rec aux il vl = match il with
      | i :: iq ->
	begin match (List.nth tl i).t_node with
	  | Tvar x when Svs.mem x qvs ->
	    begin match x.vs_ty.ty_node with
	      | Tyvar _ -> vl
	      | Tyapp _ -> aux iq (x :: vl)
	    end
	  | _ -> vl
	end
      | [] -> vl
303
    in 
304
305
306
307
    (*Format.printf "[";
    List.iter (fun i ->
      Format.printf "[%d : %a]" i Pretty.print_term (List.nth tl i)) il;
    Format.printf "]@.";*)
308
    Svsl.add (List.rev (aux il [])) acc
309
310
  in
  let defn_candidates (ls,tl) acc = match (find_logic_definition km ls) with
311
    | Some defn -> 
312
313
      let acc = acc (*int_candidates tl acc*) in
      rec_candidates (ls_defn_decrease defn) tl acc
314
315
316
317
318
319
320
321
    | None -> acc
  in
  let rec t_candidates acc t =
    let acc = match t.t_node with
      | Tapp (ls, tl) -> defn_candidates (ls, tl) acc
      | _ ->  acc
    in t_fold t_candidates acc t
  in
322
323
324
  if labeledvl <> [] 
  then Svsl.add labeledvl Svsl.empty 
  else t_candidates Svsl.empty t
325
326
327
    
    
exception No_candidates_found
328

329
(*Chooses leftmost (in the formula's quantifiers list ) candidate list from the subset of lists 
330
  of the biggest size ; raises an exception, if the candidate set is empty 
331
332
333
334
335
336
337
338
339
340
  or contains only an empty list, *)
let heuristic_lex vset =
  try 
    let vl = Svsl.max_elt vset in
    if vl = []
    then raise No_candidates_found
    else vl
  with Not_found -> raise No_candidates_found
    

341
342
(*Generates induction scheme for one variable of some algebraic datatype 
  according to datatype's definition *)
343
let vs_tyscheme km x =
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
  let ts,ty = match x.vs_ty.ty_node with
    | Tyapp _ when ty_equal x.vs_ty ty_int -> assert false
    | Tyvar _ ->   assert false
    | Tyapp (ts, _) -> ts, ty_app ts (List.map ty_var ts.ts_args)
  in
  let sigma = ty_match Mtv.empty ty x.vs_ty in
  let ty_str ty =
    let s = match ty.ty_node with
      | Tyapp (ts, _) -> ts.ts_name.id_string
      | Tyvar tv -> tv.tv_name.id_string
    in if s = "" then "x" else String.make 1 s.[0]
  in
  let ty_vs ty =
    let ty = ty_inst sigma ty in
    Term.create_vsymbol (Ident.id_fresh (ty_str ty)) ty
  in
  let tyscheme_constructor (ls, _) =
    let vlst = List.map ty_vs ls.ls_args in
    let plst = List.map pat_var vlst in
    let vset = List.fold_left
      (fun s v -> if ty_equal x.vs_ty v.vs_ty then Svs.add v s else s)
      Svs.empty vlst
    in pat_app ls plst x.vs_ty, vset
  in
  let cl = find_constructors km ts in
  ((List.map tyscheme_constructor cl) : tyscheme)

371
(* Preprocesses selected induction candidate list for 
372
373
   induction scheme instanciation.  
*)
374
375
376
let qsplit km vl qvl  = 
  let rec aux (ivs,ivm) qvl lql lvl acc = match qvl with
    | [] -> List.rev acc, lql
377
    | q :: tl ->
378
      if Svs.mem q ivs 
379
380
381
382
383
384
385
386
387
388
      then
	let qi = Mvs.find q ivm in
	let rleft = List.filter (fun v -> (Mvs.find v ivm) > qi) lvl in
	let rright = List.filter
	  (fun v -> if (Mvs.mem v ivm) then (Mvs.find v ivm) > qi else true) tl
	in
	let v = {
	  vs = q;
	  lq = List.rev lql;
	  rq = (List.rev rleft) @ rright;
389
390
	  ts =  vs_tyscheme km q} in
	aux ((Svs.remove q ivs),ivm) tl [] (q :: lvl) (v :: acc)
391
      else
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
	if Svs.is_empty ivs 
	then List.rev acc, qvl 
	else aux (ivs,ivm) tl (q :: lql) lvl acc
  in 
  let _, ivs, ivm = List.fold_left (fun (i,s,m) v -> 
    (i+1, Svs.add v s, Mvs.add v i m)) (0,Svs.empty,Mvs.empty) vl in
  aux (ivs,ivm) qvl [] [] []


let make_induction_lex lexl rql t = 
  let make_h v vset timp = 
    Svs.fold (fun x timp -> 
      let t = t_subst_single v.vs (t_var x) t in
      let t = t_forall_close v.rq [] t in
      Term.t_implies t timp) vset timp  
  in
  let rec aux lexl timp = match lexl with
    | [] -> timp
    | v :: vl -> 
      let tbl = List.map (fun (pat, vset) -> 
	let timp = (make_h v vset timp) in 
	t_close_branch pat (aux vl timp)) v.ts in
      let t = t_case (t_var v.vs) tbl in
      let t = t_forall_close (v.lq @ [v.vs]) [] t in t
  in aux lexl (t_forall_close rql [] t)
417
418
419

let induction_ty_lex km t0 =
  let qvs, qvl, t = decompose_forall t0 in
420
421
  let lblvl = qvl_labeled qvl in
  let vset = t_candidates_lex km qvs lblvl t in
422
  try
423
424
425
    let vl = heuristic_lex vset in
    let lexl, rightmost_qvl = qsplit km vl qvl in
    let tcase = make_induction_lex lexl rightmost_qvl t in
426
    
427
    if Debug.test_flag debug_verbose then
428
429
      begin
	print_vset vset;
430
431
432
433
434
435
436
	print_heuristic_lex vl;
	print_lex lexl; 
	Format.printf "Old Task: %a \n@." Pretty.print_term t0;
	Format.printf "New Task: %a \n@." Pretty.print_term tcase 
      end;
    if Debug.test_flag debug then
      begin
437
	Format.printf "Old Task: %a \n@." Pretty.print_term t0;
438
	Format.printf "New Task: %a \n@." Pretty.print_term tcase 
439
440
441
442
      end;
    [tcase]
  with No_candidates_found -> Format.printf "No candidates found\n"; [t0]

443
444
445
446
(*****************************************************************************)
(******************** INDUCTION BASED ON FUNCTION DEFINITION *****************)
(************************* WITH LEXICOGRAPHIC ORDER **************************)
(*****************************************************************************)
Leon Gondelman's avatar
Leon Gondelman committed
447

448
type htree = | Snode of (vsymbol * pattern * htree) list
449
	     | Sleaf of Svs.t (*here (int, vsymbol) set*)
450
451

let empty = Sleaf Svs.empty
452
453


454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
let defn_candidates_lex km qvs t = 
  let rec are_vars il tl = match il with
    | i :: iq ->
      begin match (List.nth tl i).t_node with
	| Tvar x when Svs.mem x qvs ->
	  begin match x.vs_ty.ty_node with
	    | Tyvar _ -> are_vars iq tl
	    | Tyapp _ -> false 
	  end
	| _ -> false
      end
    | [] -> true
  in
  let defn_candidates (ls,tl) acc = match (find_logic_definition km ls) with
    | Some defn -> 
      let il = ls_defn_decrease defn in
      if (are_vars il tl) then Mls.add ls (il, defn) acc else acc
    | None -> acc
  in
  let rec t_candidates acc t =
    let acc = match t.t_node with
      | Tapp (ls, tl) -> defn_candidates (ls, tl) acc
      | _ ->  acc
    in t_fold t_candidates acc t
  in
  t_candidates Mls.empty t


let defn_htree fname x i t =
483
  let rec t_htree acc t =
484
485
    match t.t_node with
      | Tcase ({t_node = (Tvar y)}, bl) when ty_equal x.vs_ty y.vs_ty ->
486
	case_htree acc y bl
487
      | Tapp (ls, tl) when ls_equal ls fname ->
488
489
490
491
	begin
	  match (List.nth tl i).t_node with
	    | Tvar y -> push acc (Sleaf (Svs.add y Svs.empty))
	    | _ -> assert false
492
493
494
	end

      | Tapp (_, tl) -> app_htree acc tl
495
      | _ -> acc
496

497
498
  and app_htree acc tl =
    List.fold_left (fun acc t -> t_htree acc t ) acc tl
499

500
  and case_htree acc y bl =
501
    let ptl = List.map (fun b ->
502
503
      let (p,t) = t_open_branch b in (p, t)) bl in
    let sml = List.map (fun (p,t) -> (y, p, t_htree empty t)) ptl in
504
505
506
507
508
509
    push acc (Snode sml)

  and push acc sm = match acc with
    | Snode l -> Snode (List.map (fun (x,p,s) -> (x,p, push s sm)) l)
    | Sleaf svs0 -> match sm with
	| Snode sml ->
510
	  Snode ((List.map (fun (x,p,s) ->
511
	    (x,p, push (Sleaf svs0) s)))  sml)
512
	| Sleaf svs1 -> Sleaf (Svs.union svs0 svs1)
513
  in
514
  t_htree (Sleaf Svs.empty) t
515

516
(*
517
518
519
let htree_tyscheme _ht = ([] : tyscheme)

(* Decl.known_map -> Term.vsymbol -> Term.term -> tyscheme *)
520
let tyscheme_fdef_one km x t =
521
522
523
524
  let (ls, (i, _defn)) = Mls.choose (t_defn_candidates km x t) in
  let ht = defn_htree km ls x i t in
  htree_tyscheme ht

525
let induction_fun km t0 =
526
527
  let qvs, qvl, t = decompose_forall t0 in
  let vset = t_candidates (fun _ -> true) km qvs t in
528
529
530
  if Svs.is_empty vset
  then [t0]
  else
531
532
533
534
535
536
    let x  =  heuristic_svs vset in
    let qvl1, qvl2 = split_quantifiers x qvl in
    let t = t_forall_close qvl2 [] t in
    let t = tyscheme_inst tyscheme_fdef_one km x t in
    let t = t_forall_close [x] [] t in
    let t = t_forall_close qvl1 [] t in
537
538
539
    if Debug.test_flag debug then
      (Format.printf "Old Task: %a \n@." Pretty.print_term t0;
       Format.printf "New Task: %a \n@." Pretty.print_term t);
540
    [t]
541

542
    *)
543
544


545
546
(**********************************************************************)
let filter_int v = ty_equal v.vs_ty ty_int
547

548
let int_strong_induction (le_int,lt_int) x t =
549

550
551
552
553
554
  let k = Term.create_vsymbol (Ident.id_clone x.vs_name) ty_int in
  (* 0 <= k < x *)
  let ineq = t_and (ps_app le_int [t_int_const "0"; t_var k])
    (ps_app lt_int [t_var k; t_var x]) in
  (* forall k. 0 <= k < x -> P[x <- k] *)
555
  let ih =
556
557
    t_forall_close [k] [] (t_implies ineq (t_subst_single x (t_var k) t)) in
  t_forall_close [x] [] (t_implies ih t)
558
559

let induction_int km (le_int,lt_int) t0 =
560
561
  let qvs, qvl, t = decompose_forall t0 in
  let vset = t_candidates filter_int km qvs t in
562
  if Svs.is_empty vset
563
564
565
566
567
568
569
  then [t0]
  else begin
    let x = heuristic_svs vset in
    let qvl1, qvl2 = split_quantifiers x qvl in
    let t = t_forall_close qvl2 [] t in
    let t = int_strong_induction (le_int,lt_int) x t in
    let t = t_forall_close qvl1 [] t in
570
571
572
    if Debug.test_flag debug then
    (Format.printf "Old Task: %a \n@." Pretty.print_term t0;
     Format.printf "New Task: %a \n@." Pretty.print_term t);
573
574
575
    [t]
  end

576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595


(********************************************************************)

let induction_ty = function
  | Some { task_decl = { td_node = Decl { d_node = Dprop (Pgoal, pr, f) } };
	   task_prev = prev;
	   task_known = km } ->
    List.map (add_prop_decl prev Pgoal pr) (induction_ty km f)
  | _ -> assert false


let induction_ty_lex = function
  | Some { task_decl = { td_node = Decl { d_node = Dprop (Pgoal, pr, f) } };
	   task_prev = prev;
	   task_known = km } ->
    List.map (add_prop_decl prev Pgoal pr) (induction_ty_lex km f)
  | _ -> assert false


596
(*
597
598
599
600
601
602
let induction_fun = function
  | Some { task_decl = { td_node = Decl { d_node = Dprop (Pgoal, pr, f) } };
	   task_prev = prev;
	   task_known = km } ->
    List.map (add_prop_decl prev Pgoal pr) (induction_fun km f)
  | _ -> assert false
603
*)
604
605
606


let induction_int th_int = function
607
608
609
610
  | Some
      { task_decl = { td_node = Decl { d_node = Dprop (Pgoal, pr, f) } };
	task_prev = prev; task_known = km } as t ->
    begin
611
      try
612
613
614
	let le_int = ns_find_ls th_int.th_export ["infix <="] in
	let lt_int = ns_find_ls th_int.th_export ["infix <"] in
	if not (Mid.mem le_int.ls_name km) then raise Exit;
615
616
	List.map (add_prop_decl prev Pgoal pr)
	  (induction_int km (le_int, lt_int) f)
617
618
      with Exit -> [t] end
  | _ -> assert false
619
620
621
622
623
624
625
626
627
628
629





let () =
  Trans.register_transform_l "induction_ty" (Trans.store induction_ty)

let () =
  Trans.register_transform_l "induction_ty_lex" (Trans.store induction_ty_lex)

630
(*
631
632
let () =
  Trans.register_transform_l "induction_ty_fdef" (Trans.store induction_fun)
633
*)
634
635

let () =
636
637
638
  Trans.register_env_transform_l "induction_int"
    (fun env ->
      let th_int = Env.find_theory env ["int"] "Int" in
639
      Trans.store (induction_int th_int))
640
641
642
643
644
645
646
647
648
649

(**********************************************************************)
(*TODO

1° km x t -> htree (optimized)
2° htree -> tyscheme

3° defn list -> htree
4° predicate induction
4° benchmark
650
651
652
653
654
655
656
4° labels à la
  {induction j}
  {induction false}
  {induction_int}
  {induction @1} {induction @2}
  {induction @1 generalize}
5° common tactic
657
658
6° mutual recursion
7° lexicographic orders
659
8° termination criterium
660
661
9° warnings
10° indentation
662

663
664
665
666
667
668
let time = Unix.localtime (Unix.time ()) in
	Format.printf "Last version : %d:%d %d.%d\n"
	  time.Unix.tm_hour time.Unix.tm_min
	  time.Unix.tm_mon time.Unix.tm_mday;


669
*)
670
671
672
673




674
675
(******************* ATTIC  **********************)
(*
676
677
678
679
680
681
let t_iter_scheme km t =

  let ty_cl ts =
    List.map (fun (ls, _) -> ls ) (find_constructors km ts) in

  let rec t_patc (acc,n) t =
Leon Gondelman's avatar
Leon Gondelman committed
682
683
684
685
    match t.t_node with
      | Tapp (ls, tl)      -> t_tapp (acc,n) (ls,tl)
      | Tif (c, t1, t2)    -> t_tif (acc,n)  (c, t1,t2)
      | Tlet (t, tb)       -> t_tlet (acc,n) (t,tb)
686
687
      | Tcase (t, tbl)     -> t_tcase (acc,n) (t, tbl)
      | Tvar _ | Tconst _  -> acc, n
Leon Gondelman's avatar
Leon Gondelman committed
688
      | Ttrue | Tfalse | Tnot _ | Tbinop (_, _, _) | Tquant (_,_) -> acc, n
689
690
      | Teps _ -> acc,n

Leon Gondelman's avatar
Leon Gondelman committed
691
  and t_tcase (acc,n) (t0, bl) = match t0.t_node with
692
    | (Tvar x)  ->
Leon Gondelman's avatar
Leon Gondelman committed
693
694
695
      begin
        match x.vs_ty.ty_node with
          | Tyapp (_, _) ->
696
697
698
699
            let tpl = List.map
	      (fun b -> let (p,t) = t_open_branch b in (p, t)) bl in
            let sub_ctl =
              List.fold_left (fun acc (_, t) ->
Leon Gondelman's avatar
Leon Gondelman committed
700
                let ctl,_ = (t_patc ([],(n+1)) t) in ctl @ acc) [] tpl in
701
            let tpl =
Leon Gondelman's avatar
Leon Gondelman committed
702
703
704
705
706
707
708
              List.map (fun b -> let (p,t) = t_open_branch b in [p], t) bl
            in
            let patc = Pattern.CompileTerm.compile ty_cl [t0] tpl in
            let acc = ((patc, n) :: sub_ctl) @ acc in
            acc,n
          | _ -> assert false
      end
709
710
711
712
713
    | _ ->
      let tl = List.map (fun b -> let (_,t) = t_open_branch b in t) bl in
      List.fold_left (fun (acc,n) t -> t_patc (acc,n) t) (acc,n) tl

  and t_tapp (acc,n) (_ls,tl) =
Leon Gondelman's avatar
Leon Gondelman committed
714
    List.fold_left (fun (acc,n) t -> t_patc (acc,n) t) (acc,n) tl
715

Leon Gondelman's avatar
Leon Gondelman committed
716
  and t_tif (acc,n) (_c,t1,t2) =
717
718
    let acc, n = (t_patc (acc,n) t1) in t_patc (acc,n) t2

Leon Gondelman's avatar
Leon Gondelman committed
719
  and t_tlet (acc,n) (_t,_tb) = acc,n  in
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807


  let acc, _ = t_patc ([],0) t in
  List.iter (fun (pc, n ) ->
    Format.printf "%d: %a \n @." n Pretty.print_term pc  )
    (List.rev acc)



let t_iter_compile_first km t =
  let ty_cl ts =
    List.map (fun (ls, _) -> ls ) (find_constructors km ts) in

  let rec t_patc t =
    match t.t_node with
      | Tapp (_ls, _tl)      -> t (* fs_app ls (List.map t_patc tl) *)
      | Tif (c, t1, t2)    ->  Term.t_if c (t_patc t1) (t_patc t2)
      | Tlet (t, _tb)       -> t (*
	let vs,tb,f = t_open_bound_cb tb in
	t_let t (f vs (t_patc tb)) *)
      | Tcase (t, bl)   ->
	let tpl =
          List.map (fun b -> let (p,t) = t_open_branch b in [p], t) bl
        in
	let ct = Pattern.CompileTerm.compile ty_cl [t] tpl in
	begin
	  match ct.t_node with
	    | Tcase (t, bl) ->
	      let bl =
		List.map (fun b ->
		  let (p,t) = t_open_branch b in
		  t_close_branch p (t_patc t)) bl
	      in
	      Term.t_case t bl
	    | _ -> ct
	end

      | _ -> t
  in
  Format.printf "%a \n @." Pretty.print_term (t_patc t)


t_tcase (acc,n) (t, tbl)
      | _ -> t

  and t_tcase (acc,n) (t0, bl) = match t0.t_node with
    | (Tvar x)  ->
      begin
        match x.vs_ty.ty_node with
          | Tyapp (_, _) ->
	    let tpl =
              List.map (fun b -> let (p,t) = t_open_branch b in [p], t) bl
            in
	    let patc = Pattern.CompileTerm.compile ty_cl [t0] tpl in


	    let tpl = List.map
	      (fun b -> let (p,t) = t_open_branch b in (p, t)) bl in
            let sub_ctl =
              List.fold_left (fun acc (_, t) ->
                let ctl,_ = (t_patc ([],(n+1)) t) in ctl @ acc) [] tpl in
            let tpl =
              List.map (fun b -> let (p,t) = t_open_branch b in [p], t) bl
            in
            let patc = Pattern.CompileTerm.compile ty_cl [t0] tpl in
            let acc = ((patc, n) :: sub_ctl) @ acc in
            acc,n
          | _ -> assert false
      end
    | _ ->
      let tl = List.map (fun b -> let (_,t) = t_open_branch b in t) bl in
      List.fold_left (fun (acc,n) t -> t_patc (acc,n) t) (acc,n) tl

  and t_tapp (acc,n) (_ls,tl) =
    List.fold_left (fun (acc,n) t -> t_patc (acc,n) t) (acc,n) tl

  and t_tif (acc,n) (_c,t1,t2) =
    let acc, n = (t_patc (acc,n) t1) in t_patc (acc,n) t2

  and t_tlet (acc,n) (_t,_tb) = acc,n  in


  let acc, _ = t_patc ([],0) t in
  List.iter (fun (pc, n ) ->
    Format.printf "%d: %a \n @." n Pretty.print_term pc  )
    (List.rev acc)

	 *)
808

809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
863
864
865
866
867
868
869
870
871
872
873
874
875
876
877






(*
let functional_induction km t0 =
  let qvs, _qvl, t = decompose_forall t0 in
  let vmap = t_collect_data km qvs t in
  let x, lmap =  Mvs.choose vmap in
  let (ls, (i, defn)) = Mls.choose lmap in
  let (_,t) = open_ls_defn defn in
  Format.printf "%a@." print_scheme (make_scheme km ls x i t);
  [t0]

  let _ = Mls.iter (fun _ls (_i,defn) ->
    let (_,t) = open_ls_defn defn in t_iter_compile_first km t) lmap in

  if (Mvs.is_empty vmap)
  then
    [t0]
  else
    [t0]
*)


(*

let functional_induction  = function
  | Some { task_decl = { td_node = Decl { d_node = Dprop (Pgoal, pr, f) } };
           task_prev = prev;
           task_known = km } ->
    List.map (add_prop_decl prev Pgoal pr) (functional_induction km f)
  | _ -> assert false


let () = Trans.register_transform_l
  "induction_on_function_definition"
  (Trans.store functional_induction)
  *)


(*
Local Variables:
compile-command: "unset LANG; make -C ../.."
End:
*)

(*


let rec print_scheme fmt = function
  | Snode l ->
      Format.fprintf fmt "Snode@[<hov 2>[";
      List.iter (fun (x,p,s) ->
	Format.printf "@[(%a,@ %a,@ %a)@];@ "
	  Pretty.print_vs x Pretty.print_pat p print_scheme s)
	l;
      Format.fprintf fmt "@]]"
    | Sleaf s ->
      if Svs.cardinal s = 0 then
	Format.fprintf fmt "Sleaf .. "
      else
	( Format.fprintf fmt "Sleaf ";
	  Svs.iter (fun x -> Format.printf "%a " Pretty.print_vs x) s )



878
let t_collect_data km qvs t =
879

880
  let defn_collect_data acc ls tl =
881

Leon Gondelman's avatar
Leon Gondelman committed
882
    let arg_collect_data i defn = function
883
      | Tvar x when Svs.mem x qvs ->
884
885
886
887
888
        let lmap =
          try
            Mvs.find x acc
          with Not_found ->
            Mls.empty
Leon Gondelman's avatar
Leon Gondelman committed
889
        in Mvs.add x (Mls.add ls (i,defn) lmap) acc
890
891
892
      | _ -> acc
    in

893
894
    match (find_logic_definition km ls) with
      | Some defn ->
Leon Gondelman's avatar
Leon Gondelman committed
895
896
897
898
        begin match ls_defn_decrease defn with
          | [i] -> arg_collect_data i defn (List.nth tl i).t_node
          | _  -> acc
        end
899
      | None -> acc
900
  in
901

902
903
  let rec t_collect acc t =
    let acc = match t.t_node with
904
      | Tapp (ls, tl) -> defn_collect_data acc ls tl
905
906
      | _ -> acc
    in t_fold t_collect acc t
907

Leon Gondelman's avatar
Leon Gondelman committed
908
  in t_collect (Mvs.empty) t
909
*)
910
911
912



913
914
(*

915
916
917
918
919
920
921
922
923
type ind_info =
    {tact : string ;
     cands : Term.Svs.t;
     ind_v : Term.vsymbol;
     ind_ty : ty;
     itsk : Term.term;
     pred : Term.term;
     sg : Term.term;
     }
924

925
926
927
928
929
930
931
932
let show_info i =
   Format.printf "\nInduction tactic: %s  @." i.tact;
   Format.printf "Initial task: %a @.Candidates: " Pretty.print_term i.itsk;
   Svs.iter (fun x -> Format.printf "%a @." Pretty.print_vs x) i.cands;
   Format.printf "Induction on variable:   %a @." Pretty.print_vsty i.ind_v;
   Format.printf "Induction on type:   %a @." Pretty.print_ty i.ind_ty;
   Format.printf "Induction predicate:   %a @." Pretty.print_term i.pred;
   Format.printf "Induction sub-task: %a \n@." Pretty.print_term i.sg
933

934
935
936
let print_ty_skm skm =
  List.iter
    (fun (p,svs) ->
937
938
939
940
      Format.printf "@[ %a : @]" Pretty.print_pat p;
      Svs.iter (Format.printf "%a " Pretty.print_vs) svs;
      Format.printf "@.")
    skm
941

Leon Gondelman's avatar
Leon Gondelman committed
942

943

944
945
946
947

let indv_ty x = match x.vs_ty.ty_node with
  | Tyapp (ts, _) -> ts, ty_app ts (List.map ty_var ts.ts_args)
  | Tyvar _ -> assert false
948

949
950
951
952
953
954
955
956
957
958
959
960
961
962
963
964
965
let heuristic vss =
  let x = Svs.choose vss in
  let ts, ty = indv_ty x in
  x, ts, ty

let name_from_type ty =
  let s = match ty.ty_node with
    | Tyapp (ts, _) -> ts.ts_name.id_string
    | Tyvar tv -> tv.tv_name.id_string
  in
  if s = "" then "x" else String.make 1 s.[0]




let make_induction vs km qvl t =
  let x, ts, ty  = heuristic vs in
966

967
968
969
970
971
972
973
974
975
976
977
978
979
980
981
982
983
984
985
986
987
988
989
990
991
992
993
994
995
996
997
998
999
1000
1001
1002
  let sigma = ty_match Mtv.empty ty x.vs_ty in
  let qvl1, qvl2 = split_quantifiers x qvl in
  let p = t_forall_close qvl2 [] t in
  let make_case (ls, _) =
    let create_var ty =
      let ty = ty_inst sigma ty in
      let id = Ident.id_fresh (name_from_type ty) in
      Term.create_vsymbol id ty
    in
    let ind_vl = List.map create_var ls.ls_args in
    let ind_tl = List.map t_var ind_vl in
    let goal = t_subst_single x (t_app ls ind_tl (Some x.vs_ty)) p in
    let goal = List.fold_left
      (fun goal vs ->
	if ty_equal vs.vs_ty x.vs_ty
	then Term.t_implies (t_subst_single x (t_var vs) p) goal
	else goal) goal ind_vl
    in
    let goal = t_forall_close (qvl1 @ ind_vl) [] goal in
     if Debug.test_flag debug then
       begin
	 let data = {
	   tact = ""; cands = vs; ind_v = x;
	   ind_ty = ty;
	   itsk = t_forall_close qvl [] t ;
	   pred = p; sg = goal}
	 in  show_info data
       end; goal
  in
  let cl = find_constructors km ts in
  List.map make_case cl


let induction km t0 =
  let qvs, _qvl, t = decompose_forall t0 in
  let vs = t_candidates km qvs t in
1003
  if Svs.is_empty vs then [t0] else
1004
1005
1006
1007
1008
1009
    let x, _ts, _ty  = heuristic vs in
    let () = print_ty_skm (tyscheme_genvt km x t) in
    [t0]
    (* make_induction vs km qvl t  *)

let induction = function
1010
  | Some { task_decl = { td_node = Decl { d_node = Dprop (Pgoal, pr, f) } };
1011
1012
1013
	   task_prev = prev;
	   task_known = km } ->
      List.map (add_prop_decl prev Pgoal pr) (induction km f)
1014
1015
  | _ -> assert false

1016
1017
let () = Trans.register_transform_l "induction" (Trans.store induction)
*)
1018

1019
1020
1021
1022
  (*Format.printf "[";
    List.iter (fun i ->
      Format.printf "[%d : %a]" i Pretty.print_term (List.nth tl i)) il;
    Format.printf "]@.";*)
Leon Gondelman's avatar
Leon Gondelman committed
1023

1024
1025
1026
(*********************************************************)
(******* Induction tactic on function definition *********)
(*********************************************************)
1027

1028
1029
1030
1031
1032
1033
1034
1035
1036
1037
1038
1039
1040
1041
1042
1043
1044
1045
1046
1047
1048
1049
1050
1051
1052
1053
1054
1055
1056
1057
1058
1059
1060
1061
1062
1063
1064
1065
1066
1067
1068
1069
1070
1071
1072
1073
1074
1075
1076
1077
1078
1079
1080


(*
module Vsl = struct
  type t = Svs.elt list
  let compare t1 t2 =
    let rec aux t1 t2 = match t1,t2 with
      | [],[] -> 0
      | h1 :: q1, h2 :: q2 ->
	if vs_equal h1 h2 
	then aux q1 q2 
	else Pervasives.compare (vs_hash h1) (vs_hash h2)
      | _ -> assert false;
    in
    if List.length t1 < List.length t2 then -1
    else if List.length t1 > List.length t2 then 1
    else aux t1 t2
end

module Svsl = Set.Make(Vsl) *)





(*
module VsList =
struct
 
  type t = Svs.elt list
  let hash = Hashcons.combine_list vs_hash 3
  let equal = list_all2 vs_equal
  let cmp_vs vs1 vs2 = Pervasives.compare (vs_hash vs1) (vs_hash vs2)
  let compare t1 t2 = 
    let rec aux t1 t2 = match t1,t2 with
      | [],[] -> 0
      | v1 :: q1, v2 :: q2 ->
	if vs_equal v1 v2 
	then aux q1 q2 
	else cmp_vs v1 v2
      | _ -> assert false;
    in
    if List.length t1 < List.length t2 then -1
    else if List.length t1 > List.length t2 then 1
    else aux t1 t2
end

module Mvls = Util.StructMake(VsList)
*)




Leon Gondelman's avatar
Leon Gondelman committed
1081
1082
(*
Local Variables:
1083
compile-command: "unset LANG; make -C ../.. bin/why3.byte"
Leon Gondelman's avatar
Leon Gondelman committed
1084
1085
End:
*)