induction.ml 32.4 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
(**************************************************************************)
(*                                                                        *)
(*  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.                  *)
(*                                                                        *)
(**************************************************************************)
20

Leon Gondelman's avatar
Leon Gondelman committed
21
open Ident
22
open Ty
Leon Gondelman's avatar
Leon Gondelman committed
23 24 25 26 27
open Term
open Decl
open Theory
open Task

Leon Gondelman's avatar
Leon Gondelman committed
28

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

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

37 38 39 40 41 42 43 44 45

(*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*)
    }

46 47 48 49 50 51 52 53 54 55 56 57 58
(*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.
*)  
59 60 61 62 63 64
module VsList =
struct
 
  type t = vsymbol list
  let hash = Hashcons.combine_list vs_hash 3
  let equal = Util.list_all2 vs_equal
65
  let cmp_vs vs1 vs2 = Pervasives.compare (vs_hash vs2) (vs_hash vs1)
66 67 68 69 70 71 72
  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
73
      | _ -> assert false; 
74 75 76 77 78 79 80 81 82 83
    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 ***************************************)
84
let debug = Debug.register_info_flag "induction"
85 86
  ~desc:"About@ the@ transformation@ of@ the@ goal@ using@ induction."

87
let debug_verbose = Debug.register_info_flag "induction-verbose"
88 89
  ~desc:"Same@ as@ induction, but@ print@ also@ the@ variables, the@ \
         heuristics@ and@ the lexicographic@ order@ used."
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

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";
117
  Format.printf "Induction variables (in lexicographic order): [ ";
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
  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 ()


(**********************************************************************)
148
let tyscheme_inst f (km : Decl.known_map) x tx  =
149 150
  let inst_branch = (fun (p, vset) ->
    t_close_branch p ( Svs.fold (fun v tacc ->
151
      (Term.t_implies (t_subst_single x (t_var v) tx) tacc )) vset tx))
152
  in
153 154 155 156 157 158 159 160 161
  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
162

163

164 165
let decompose_forall t =
  let rec aux qvl_acc t = match t.t_node with
Leon Gondelman's avatar
Leon Gondelman committed
166 167 168 169 170
    | 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
171

172 173 174 175 176 177 178 179 180 181

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
182
      | Tvar x when Svs.mem x qvs ->
183
	begin match x.vs_ty.ty_node with
184
	  | Tyvar _ -> acc
185 186 187
	  | Tyapp _ -> Svs.add x acc
	end
      | _ -> acc)
188
  in
189 190 191 192 193
  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
194 195 196 197
	  | [i] -> arg_candidate vs_acc (List.nth tl i)
	  | h :: _ ->
	    arg_candidate vs_acc (List.nth tl h)
	  | _ ->  vs_acc
198 199 200
	end
      | None -> vs_acc)
  in
201 202
  let rec t_candidate vs_acc t =
    let vs_acc = match t.t_node with
203
      | Tapp (ls, tl) -> defn_candidate vs_acc ls tl
204
      | _ ->  vs_acc
205
    in t_fold t_candidate vs_acc t
206
  in Svs.filter filter (t_candidate Svs.empty t)
207

208
let heuristic_svs vset = Svs.choose vset
209

210
let filter_tydef v = not (ty_equal v.vs_ty ty_int)
211

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


let induction_ty km t0 =
244
  let qvs, qvl, t = decompose_forall t0 in
245
  let vset = t_candidates filter_tydef km qvs t in
246
  if Svs.is_empty vset then [t0]
247
  else
248 249 250 251 252 253
    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
254 255 256 257 258 259
    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;
260
    [tcase]
261

262 263 264 265 266
(*****************************************************************************)
(******************** INDUCTION BASED ON TYPE DEFINITIONS ********************)
(************************* WITH LEXICOGRAPHIC ORDER **************************)
(*****************************************************************************)

267 268 269
(** TODO use this label in the following function *)
let label_induction = create_label "induction"

270 271 272
let qvl_labeled qvl = 
  List.filter (fun v -> 
    let slab = Slab.filter (fun v -> 
273 274
      v.lab_string = "induction") v.vs_name.id_label 
    in not (Slab.is_empty slab)) qvl
275 276


277
(* This function collects lists of variables corresponding to
278 279 280 281 282 283 284 285 286 287 288 289 290 291 292 293 294 295
   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
296 297
     | Tvar x when Svs.mem x qvs && ty_equal x.vs_ty ty_int -> 
     Svls.add [x] acc
298
     | _ -> acc) acc tl *) 
299 300 301 302 303 304 305 306 307 308 309 310
  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
311
    in 
312 313 314 315
    (*Format.printf "[";
    List.iter (fun i ->
      Format.printf "[%d : %a]" i Pretty.print_term (List.nth tl i)) il;
    Format.printf "]@.";*)
316
    Svsl.add (List.rev (aux il [])) acc
317 318
  in
  let defn_candidates (ls,tl) acc = match (find_logic_definition km ls) with
319
    | Some defn -> 
320 321
      let acc = acc (*int_candidates tl acc*) in
      rec_candidates (ls_defn_decrease defn) tl acc
322 323 324 325 326 327 328 329
    | 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
330 331 332
  if labeledvl <> [] 
  then Svsl.add labeledvl Svsl.empty 
  else t_candidates Svsl.empty t
333 334 335
    
    
exception No_candidates_found
336

337
(*Chooses leftmost (in the formula's quantifiers list ) candidate list from the subset of lists 
338
  of the biggest size ; raises an exception, if the candidate set is empty 
339 340 341 342 343 344 345 346 347 348
  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
    

349 350
(*Generates induction scheme for one variable of some algebraic datatype 
  according to datatype's definition *)
351
let vs_tyscheme km x =
352 353 354 355 356 357 358 359 360 361 362 363 364 365 366 367 368 369 370 371 372 373 374 375 376 377 378
  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)

379
(* Preprocesses selected induction candidate list for 
380 381
   induction scheme instanciation.  
*)
382 383 384
let qsplit km vl qvl  = 
  let rec aux (ivs,ivm) qvl lql lvl acc = match qvl with
    | [] -> List.rev acc, lql
385
    | q :: tl ->
386
      if Svs.mem q ivs 
387 388 389 390 391 392 393 394 395 396
      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;
397 398
	  ts =  vs_tyscheme km q} in
	aux ((Svs.remove q ivs),ivm) tl [] (q :: lvl) (v :: acc)
399
      else
400 401 402 403 404 405 406 407 408 409 410 411 412 413 414 415 416 417 418 419 420 421 422 423 424
	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)
425 426 427

let induction_ty_lex km t0 =
  let qvs, qvl, t = decompose_forall t0 in
428 429
  let lblvl = qvl_labeled qvl in
  let vset = t_candidates_lex km qvs lblvl t in
430
  try
431 432 433
    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
434
    
435
    if Debug.test_flag debug_verbose then
436 437
      begin
	print_vset vset;
438 439 440 441 442 443 444
	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
445
	Format.printf "Old Task: %a \n@." Pretty.print_term t0;
446
	Format.printf "New Task: %a \n@." Pretty.print_term tcase 
447 448 449 450
      end;
    [tcase]
  with No_candidates_found -> Format.printf "No candidates found\n"; [t0]

451 452 453 454
(*****************************************************************************)
(******************** INDUCTION BASED ON FUNCTION DEFINITION *****************)
(************************* WITH LEXICOGRAPHIC ORDER **************************)
(*****************************************************************************)
Leon Gondelman's avatar
Leon Gondelman committed
455

456
type htree = | Snode of (vsymbol * pattern * htree) list
457
	     | Sleaf of Svs.t (*here (int, vsymbol) set*)
458 459

let empty = Sleaf Svs.empty
460 461


462 463 464 465 466 467 468 469 470 471 472 473 474 475 476 477 478 479 480 481 482 483 484 485 486 487 488 489 490
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 =
491
  let rec t_htree acc t =
492 493
    match t.t_node with
      | Tcase ({t_node = (Tvar y)}, bl) when ty_equal x.vs_ty y.vs_ty ->
494
	case_htree acc y bl
495
      | Tapp (ls, tl) when ls_equal ls fname ->
496 497 498 499
	begin
	  match (List.nth tl i).t_node with
	    | Tvar y -> push acc (Sleaf (Svs.add y Svs.empty))
	    | _ -> assert false
500 501 502
	end

      | Tapp (_, tl) -> app_htree acc tl
503
      | _ -> acc
504

505 506
  and app_htree acc tl =
    List.fold_left (fun acc t -> t_htree acc t ) acc tl
507

508
  and case_htree acc y bl =
509
    let ptl = List.map (fun b ->
510 511
      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
512 513 514 515 516 517
    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 ->
518
	  Snode ((List.map (fun (x,p,s) ->
519
	    (x,p, push (Sleaf svs0) s)))  sml)
520
	| Sleaf svs1 -> Sleaf (Svs.union svs0 svs1)
521
  in
522
  t_htree (Sleaf Svs.empty) t
523

524
(*
525 526 527
let htree_tyscheme _ht = ([] : tyscheme)

(* Decl.known_map -> Term.vsymbol -> Term.term -> tyscheme *)
528
let tyscheme_fdef_one km x t =
529 530 531 532
  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

533
let induction_fun km t0 =
534 535
  let qvs, qvl, t = decompose_forall t0 in
  let vset = t_candidates (fun _ -> true) km qvs t in
536 537 538
  if Svs.is_empty vset
  then [t0]
  else
539 540 541 542 543 544
    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
545 546 547
    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);
548
    [t]
549

550
    *)
551 552


553 554
(**********************************************************************)
let filter_int v = ty_equal v.vs_ty ty_int
555

556
let int_strong_induction (le_int,lt_int) x t =
557

558 559 560 561 562
  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] *)
563
  let ih =
564 565
    t_forall_close [k] [] (t_implies ineq (t_subst_single x (t_var k) t)) in
  t_forall_close [x] [] (t_implies ih t)
566 567

let induction_int km (le_int,lt_int) t0 =
568 569
  let qvs, qvl, t = decompose_forall t0 in
  let vset = t_candidates filter_int km qvs t in
570
  if Svs.is_empty vset
571 572 573 574 575 576 577
  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
578 579 580
    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);
581 582 583
    [t]
  end

584 585 586 587 588 589 590 591 592 593 594 595 596 597 598 599 600 601 602 603


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

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


604
(*
605 606 607 608 609 610
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
611
*)
612 613 614


let induction_int th_int = function
615 616 617 618
  | Some
      { task_decl = { td_node = Decl { d_node = Dprop (Pgoal, pr, f) } };
	task_prev = prev; task_known = km } as t ->
    begin
619
      try
620 621 622
	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;
623 624
	List.map (add_prop_decl prev Pgoal pr)
	  (induction_int km (le_int, lt_int) f)
625 626
      with Exit -> [t] end
  | _ -> assert false
627 628 629



630 631 632
let desc_labels = [label_induction,
                   ("Make the induction on the labeled variables." :
                       Pp.formatted)]
633 634 635 636


let () =
  Trans.register_transform_l "induction_ty" (Trans.store induction_ty)
637
    ~desc_labels ~desc:"TODO: induction on type"
638 639 640

let () =
  Trans.register_transform_l "induction_ty_lex" (Trans.store induction_ty_lex)
641
    ~desc_labels ~desc:"TODO: induction on type with lexicographic order"
642

643
(*
644 645
let () =
  Trans.register_transform_l "induction_ty_fdef" (Trans.store induction_fun)
646
    ~desc_labels ~desc:"TODO: induction on type using function definition"
647
*)
648 649

let () =
650 651 652
  Trans.register_env_transform_l "induction_int"
    (fun env ->
      let th_int = Env.find_theory env ["int"] "Int" in
653
      Trans.store (induction_int th_int))
654
    ~desc_labels ~desc:"TODO: induction on integers"
655 656 657 658 659 660 661 662 663 664

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

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

3° defn list -> htree
4° predicate induction
4° benchmark
665 666 667 668 669 670 671
4° labels à la
  {induction j}
  {induction false}
  {induction_int}
  {induction @1} {induction @2}
  {induction @1 generalize}
5° common tactic
672 673
6° mutual recursion
7° lexicographic orders
674
8° termination criterium
675 676
9° warnings
10° indentation
677

678 679 680 681 682 683
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;


684
*)
685 686 687 688




689 690
(******************* ATTIC  **********************)
(*
691 692 693 694 695 696
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
697 698 699 700
    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)
701 702
      | Tcase (t, tbl)     -> t_tcase (acc,n) (t, tbl)
      | Tvar _ | Tconst _  -> acc, n
Leon Gondelman's avatar
Leon Gondelman committed
703
      | Ttrue | Tfalse | Tnot _ | Tbinop (_, _, _) | Tquant (_,_) -> acc, n
704 705
      | Teps _ -> acc,n

Leon Gondelman's avatar
Leon Gondelman committed
706
  and t_tcase (acc,n) (t0, bl) = match t0.t_node with
707
    | (Tvar x)  ->
Leon Gondelman's avatar
Leon Gondelman committed
708 709 710
      begin
        match x.vs_ty.ty_node with
          | Tyapp (_, _) ->
711 712 713 714
            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
715
                let ctl,_ = (t_patc ([],(n+1)) t) in ctl @ acc) [] tpl in
716
            let tpl =
Leon Gondelman's avatar
Leon Gondelman committed
717 718 719 720 721 722 723
              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
724 725 726 727 728
    | _ ->
      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
729
    List.fold_left (fun (acc,n) t -> t_patc (acc,n) t) (acc,n) tl
730

Leon Gondelman's avatar
Leon Gondelman committed
731
  and t_tif (acc,n) (_c,t1,t2) =
732 733
    let acc, n = (t_patc (acc,n) t1) in t_patc (acc,n) t2

Leon Gondelman's avatar
Leon Gondelman committed
734
  and t_tlet (acc,n) (_t,_tb) = acc,n  in
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 808 809 810 811 812 813 814 815 816 817 818 819 820 821 822


  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)

	 *)
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 878 879 880 881 882 883 884 885 886 887 888 889 890 891 892






(*
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 )



893
let t_collect_data km qvs t =
894

895
  let defn_collect_data acc ls tl =
896

Leon Gondelman's avatar
Leon Gondelman committed
897
    let arg_collect_data i defn = function
898
      | Tvar x when Svs.mem x qvs ->
899 900 901 902 903
        let lmap =
          try
            Mvs.find x acc
          with Not_found ->
            Mls.empty
Leon Gondelman's avatar
Leon Gondelman committed
904
        in Mvs.add x (Mls.add ls (i,defn) lmap) acc
905 906 907
      | _ -> acc
    in

908 909
    match (find_logic_definition km ls) with
      | Some defn ->
Leon Gondelman's avatar
Leon Gondelman committed
910 911 912 913
        begin match ls_defn_decrease defn with
          | [i] -> arg_collect_data i defn (List.nth tl i).t_node
          | _  -> acc
        end
914
      | None -> acc
915
  in
916

917 918
  let rec t_collect acc t =
    let acc = match t.t_node with
919
      | Tapp (ls, tl) -> defn_collect_data acc ls tl
920 921
      | _ -> acc
    in t_fold t_collect acc t
922

Leon Gondelman's avatar
Leon Gondelman committed
923
  in t_collect (Mvs.empty) t
924
*)
925 926 927



928 929
(*

930 931 932 933 934 935 936 937 938
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;
     }
939

940 941 942 943 944 945 946 947
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
948

949 950 951
let print_ty_skm skm =
  List.iter
    (fun (p,svs) ->
952 953 954 955
      Format.printf "@[ %a : @]" Pretty.print_pat p;
      Svs.iter (Format.printf "%a " Pretty.print_vs) svs;
      Format.printf "@.")
    skm
956

Leon Gondelman's avatar
Leon Gondelman committed
957

958

959 960 961 962

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
963

964 965 966 967 968 969 970 971 972 973 974 975 976 977 978 979 980
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
981

982 983 984 985 986 987 988 989 990 991 992 993 994 995 996 997 998 999 1000 1001 1002 1003 1004 1005 1006 1007 1008 1009 1010 1011 1012 1013 1014 1015 1016 1017
  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
1018
  if Svs.is_empty vs then [t0] else
1019 1020 1021 1022 1023 1024
    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
1025
  | Some { task_decl = { td_node = Decl { d_node = Dprop (Pgoal, pr, f) } };
1026 1027 1028
	   task_prev = prev;
	   task_known = km } ->
      List.map (add_prop_decl prev Pgoal pr) (induction km f)
1029 1030
  | _ -> assert false

1031 1032
let () = Trans.register_transform_l "induction" (Trans.store induction)
*)
1033

1034 1035 1036 1037
  (*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
1038

1039 1040 1041
(*********************************************************)
(******* Induction tactic on function definition *********)
(*********************************************************)
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 1081 1082 1083 1084 1085 1086 1087 1088 1089 1090 1091 1092 1093 1094 1095


(*
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
1096 1097
(*
Local Variables:
1098
compile-command: "unset LANG; make -C ../.. bin/why3.byte"
Leon Gondelman's avatar
Leon Gondelman committed
1099 1100
End:
*)