(*======================================================================
Copyright Christophe Raffalli & Pierre Hyvernat, Universite de Savoie.

christophe.raffalli@univ-savoie.fr
Pierre.Hyvernat@univ-savoie.fr

This software is a computer program which implements an interpreter
and type-checker for the PML (Proved Meta-Language) computer language.
PML is a language of the ML family with the extra possibility to write
and prove the specifications of your code.

This software is governed by the CeCILL-B license under French law and
abiding by the rules of distribution of free software.  You can  use,
modify and/or redistribute the software under the terms of the CeCILL-B
license as circulated by CEA, CNRS and INRIA at the following URL
"http://www.cecill.info".

The exercising of this freedom is conditional upon a strong obligation
of giving credits for everybody that distributes a software
incorporating a software ruled by the current license so as all
contributions to be properly identified and acknowledged.

As a counterpart to the access to the source code and  rights to copy,
modify and redistribute granted by the license, users are provided only
with a limited warranty  and the software's author,  the holder of the
economic rights,  and the successive licensors  have only  limited
liability.

In this respect, the user's attention is drawn to the risks associated
with loading,  using,  modifying and/or developing or reproducing the
software by the user in light of its specific status of free software,
that may mean  that it is complicated to manipulate,  and  that  also
therefore means  that it is reserved for developers  and  experienced
professionals having in-depth computer knowledge. Users are therefore
encouraged to load and test the software's suitability as regards their
requirements in conditions enabling the security of their systems and/or
data to be ensured and,  more generally, to use and operate it in the
same conditions as regards security.

The fact that you are presently reading this means that you have had
knowledge of the CeCILL-B license and that you accept its terms.
======================================================================*)



(******************************************************************************
 * This is the file implementing the "Size Change Termination Principle",     *
 * adapted from Lee, Jones & Ben-Amram.                                       *
 * The test is described in details in the paper "The Size Change Termination *
 * Principle for Constructor based Languages".                                *
 ******************************************************************************)

(* A couple of differences between this implementation and what is described in
 * the article:
 *
 *   0/ Records rather than tuples
 *   PML uses Records with labels rather than plain tuples. (Tuples are just
 *   records with labels "1", "2", "3" etc.
 *
 *   1/ Default field
 *   PML's records have a "default" field, which is used instead of the whole
 *   record in special cases. One such case is when a record is matched against
 *   a variant destructor. This explains the special case in the definition of
 *   reduction.
 *
 *   2/ Default field, bis
 *   The default field in a record cannot be itself a record. This explains why,
 *   in several places, the Caml variant constructor "Record" is replaced by a
 *   function "_Record" which flattens the default field if necessary.
 *
 *   3/ Partial applications / lambda deficit
 *   This doesn't show in the code but only in the output of the algorithm (in
 *   verbose mode). We consider all the partial applications: a call
 *      f u1 u2 u3
 *   will give rise to 3 calls:
 *      - f u1
 *      - f u1 u2
 *      - f u1 u2 u3
 *   This can be important strange definitions such as
untyped {
val rec f?(? => ? => ?) x  =
  let h = f x in
  fun y ->
    begin
    match y with
       A[y] -> h B[y]
     | _ -> C[]
    end
}
which doesn't terminate whereas
val rec g:(? => ? => ?) x =
  fun y ->
  let h = g x in
    begin
    match y with
       A[y] -> h B[y]
     | _ -> C[]
    end
does terminate

 * 4/ The actual test is incremental: we try with d=0, 1, 2, 4, ...,
 * depth_bound. This seems to be efficient in practice.
 *
 *)


(*
 * Bureaucratic things
 *)
let debugOptions = ref [
  "additional_sanity_checking" , true                   ;
  "use_approximates" , true                             ;
  "initial_collapse_of_graph", true                     ;

(* verbosity of output messages *)
  "show_lambda" , false                                 ;
  "show_initial_call_graph" , false                     ;
  "show_final_call_graph" , false                       ;
  "show_summary_TC" , false                             ;
  "show_all_steps" , false                              ;
  "show_all_compositions" , false                       ;
  "show_coherents" , false                              ;
  "show_decreasing_terms" , false                       ;
  "show_nondecreasing_coherents" , false                ;
]

let setOption s v =
  let rec aux options s v acc = match options with
      [] -> raise Not_found
    | (s',_)::options when s'=s -> (s',v)::List.rev_append options acc
    | x::options -> aux options s v (x::acc)
  in
  debugOptions := aux !debugOptions s v []

let debugOption s =
  let b = try List.assoc s !debugOptions with Not_found -> assert false
  in b

let ifDebug (s:string) (c:unit->unit) : unit =
  let b = debugOption s in
  if b then c ()


(*************
 * Datatypes *
 *************)

(* Type for integer with a $\infty$ element *)
type z_infty = Number of int | Infty

(*
 * The type of destructors. Projection are along strings because we
 * consider records with labels rather than just tuples.
 *)
type destructor = Project of string | RemoveVariant of string

(*
 * The actual type for term terms ($\mathcal T$ in the
 * paper).
 * Note: the first element of a list of destructors is the rightmost destructor.
 *)
type term =
    Variant of string*term
  | Record of (string*term) list
  | Epsilon of (destructor list)*int
  | Sum of (z_infty*(destructor list)*int) list       (* Note: the list should be sorted... *)

(* The exception for impossible cases. *)
exception Impossible_case

(*
 * The type of calls, ie substitutions: just association lists. I
 * could (should?) replace them by maps. At the moment, they are supposed to be
 * sorted and contain elements indexed by 0, 1, ..., n.
 *)
type call = (int*term) list

(* Sets of substitutions *)
module Calls_Set = Set.Make (struct type t=call let compare=compare end)
type calls_set = Calls_Set.t

(* Call graphs: maps indexed by pairs of function names *)
module Call_Graph = Map.Make (struct type t=string*string let compare=compare end)
type call_graph = calls_set Call_Graph.t


(***********************
 * Printing functions. *
 ***********************)

let print_infty = function
    Infty -> print_string "∞"
  | Number(n) -> print_int n

let sub s = String.sub s 1 ((String.length s)-1) (* PML specific *)

let print_destr = function
    RemoveVariant c -> print_string ((sub c)^"-")
  | Project p -> print_string ("π_"^p)

let rec print_list sep pr l = match l with
    [] -> ()
  | [a] -> pr a
  | a::l -> pr a ; print_string sep ; print_list sep pr l

let print_branch b = match b with
    w,ds,i ->
      print_string "<" ;
      print_infty w;
      print_string ">";
      print_list " " print_destr ds ;
      print_string " x_" ; print_int i

let rec print_term = function
    Variant(c,u) ->
      print_string (sub c);
      print_string " ";
      print_term u;
      print_string " "
  | Record [] -> print_string "{ }"
  | Record(l) ->
        print_string "{ ";
    print_list "  ;  " (function label,u -> print_string (label^" = "); print_term u) l;
    print_string " }"
  | Epsilon(ds,i) ->
    List.iter (fun d -> print_destr d; print_string " ") ds;
    print_string "x_"; print_int i
  | Sum(bs) ->
    print_string "( ";
    print_list " + " print_branch bs;
    print_string " )"

let print_substitution tau =
  if tau = [] then print_string "    empty substitution\n";
  List.iter (function i,arg ->
    if i>0 || debugOption "show_lambda"
    then begin
      print_string "    x_"; print_int i;
      print_string " := "; print_term arg;
      print_newline()
    end
  ) tau

let print_graph g =
  let t = ref 0 in
  Call_Graph.iter (fun fg s ->
    let f,g = fg in
    print_string ("  Calls from "^f^" to "^g^":\n");
    Calls_Set.iter (fun tau ->
      t := !t+1;
      print_substitution tau;
      print_newline()
    ) s
  ) g;
  print_string "  This graph contains "; print_int !t;
  print_string " edge(s).\n"; print_newline()


(**********************************
 * Functions on the z_infty type. *
 **********************************)

(* Collapsing to the set $\{-b,...,0,...,b-1,\infty\}$. *)
let collapse_z_infty b = function
    Infty -> Infty
  | Number(n) -> if (n < -b) then Number (-b)
                 else if (n>=b) then Infty
                 else Number(n)

(*
 * Various helper functions: max, add, less, as well as a function to add a
 * normal integer to an element of the type z_infty
 *)
let max_infty w1 w2 = match w1,w2 with
    Infty,_ | _,Infty -> Infty
  | Number n1, Number n2 -> Number (max n1 n2)
let less_infty w1 w2 = match w1,w2 with
    _,Infty -> true
  | Infty,_ -> false
  | Number n1, Number n2 -> n1 <= n2
let add_infty w1 w2 = match w1,w2 with
    Infty,_ | _,Infty -> Infty
  | Number n1, Number n2 -> Number(n1+n2)
let add_int w n = match w with
    Infty -> Infty
  | Number(m) -> Number(n+m)


(******************************
 * Sanity checking functions. *
 ******************************)

(* checks if a substitution is sorted *)
let sorted_call tau =
  let rec aux tau n =
    match tau with
        [] -> ()
      | (i,_)::tau when i=n -> aux tau (n+1)
      | _ -> assert false
  in
  aux tau 0

(* checks if the labels of a record are sorted *)
let rec sorted_labels l = match l with
    [] -> ()
  | [_] -> ()
  | (a,_)::(((b,_)::_) as l) when (compare a b)<0 -> sorted_labels l
  | (a,_)::(b,_)::_ -> print_string ("OUPS: "^a^" / "^b^"\n"); assert false

(* checks if a list is sorted *)
let rec sorted l = match l with
    [] -> ()
  | [_] -> ()
  | a::((b::_) as l) when (compare a b)<0 -> sorted l
  | a::b::_ -> assert false


(***********************
 * Misc list functions *
 ***********************)

(*
 * Get a suffix of length n and return both the suffix and the
 * remaining elements, in reverse order.
 *)
let get_suffix l n =
  let rec aux l n acc =
    if n=0
    then acc,l
    else match l with
        [] -> acc,[]
      | a::l -> aux l (n-1) (a::acc)
  in
  aux (List.rev l) n []

(*
 * Longest common suffix of l1 and l2; returns a triple containing the suffix,
 * and the remainining elements in l1 and l2 in reverse order:
 *    l1 l2  -->  s r1 r2 s.t. l1 = rev_append r1 s
 *                             l2 = rev_append r2 s
 *)
let suffix l1 l2 =
  let rec rev_prefix l1 l2 p = match l1,l2 with
      a::l1, b::l2 when a=b -> rev_prefix l1 l2 (a::p)
    | l1,l2 -> (p,l1,l2)
  in rev_prefix (List.rev l1) (List.rev l2) []

(* Merging two sorted lists, while keeping only one occurence of each element *)
let rec merge l1 l2 =
  match l1, l2 with
  | [], l2 -> l2
  | l1, [] -> l1
  | h1 :: t1, h2 :: t2 ->
      if h1 < h2
      then h1 :: merge t1 l2
      else if h2 < h1
      then h2 :: merge l1 t2
      else (* if h1=h2 *) h1 :: merge t1 t2

(* Sorting a list and removing keeping only one copy of each element *)
let sort_uniq l =
  let l = List.sort (fun x y -> -(compare x y)) l in
  let rec uniq l acc = match l with
      [] -> acc
    | [a] -> a::acc
    | a::b::l when a=b -> uniq (b::l) acc
    | a::b::l -> uniq (b::l) (a::acc)
  in
  uniq l []


(************************************
 * The approximation order on terms *
 ************************************)

(* approximation for branches of destructors *)
let rec approximates_branch b1 b2 = match b1, b2 with
    (w1,ds1,i1),(w2,ds2,i2) when i1=i2 ->
      begin
        match suffix ds1 ds2 with
            (_,[],ds2') -> less_infty w2 (add_int w1 (List.length ds2'))
          | _ -> false
      end
  | _,_ -> false

(* remove all sequences of destructors that are not maximal for approximates *)
let keep_max l =
  let rec aux1 b l acc = match l with
      [] -> b::acc
    | a::l when approximates_branch a b -> aux1 a l acc
    | a::l when approximates_branch b a -> aux1 b l acc
    | a::l -> aux1 b l (a::acc)
  in
  let rec aux2 l = match l with
      [] -> []
    | b::l -> (aux1 b (aux2 l) [])
  in
  aux2 l


(* computes the normal form of <w>v *)
(* make reduce_approx returns a "Sum [...]" rather than just the list??? *)
let rec reduce_approx w v = match v with
    Variant (_,v) -> reduce_approx (add_int w 1) v
  | Record l -> sort_uniq (keep_max (List.fold_left merge [] (List.map (reduce_approx (add_int w 1)) (List.map snd l))))
  | Sum bs -> sort_uniq (keep_max (List.map (function (w',ds,i) -> (add_infty w w', ds, i)) bs))
  | Epsilon (ds,i) -> [ (w,ds,i) ]


let rec approximates u1 u2 =
  (*
  print_string "approximates with "; print_newline();
  print_term u1 ; print_newline();
  print_term u2 ; print_newline();
  *)
  match u1,u2 with
    Epsilon(ds1,i1), Epsilon(ds2,i2) when ds1=ds2 && i1=i2 -> true
  | Variant(c1,u1), Variant(c2,u2) when c1=c2 -> approximates u1 u2
  | Record l1, Record l2 ->
      let lab1,uu1 = List.split l1 in
      let lab2,uu2 = List.split l2 in
      sorted_labels l1; sorted_labels l2;
      if (lab1=lab2)
      then
        List.for_all2 approximates uu1 uu2
      else false
  | Sum(b1s), Sum(b2s) ->
      List.for_all (fun b2 -> List.exists (fun b1 -> approximates_branch b1 b2) b1s) b2s

  | Sum(_), u2 -> approximates u1 (Sum(reduce_approx (Number 0) u2))

  | _,_ -> false


(* checking if two terms are compatible *)
let rec compatible t1 t2 = match t1,t2 with
    Variant(c1,t1), Variant(c2,t2) when c1=c2 -> compatible t1 t2
  | Record(l1), Record(l2) ->
      let labels1, terms1 = List.split l1 in
      let labels2, terms2 = List.split l2 in
      labels1 = labels2 && List.for_all2 compatible terms1 terms2
  | Sum b1, Sum b2 ->
      List.exists (function b1 ->
      List.exists (function b2 ->
        approximates_branch b1 b2 || approximates_branch b2 b1)
      b2
      )
      b1
  | Epsilon _, Epsilon _ -> t1=t2

  | Sum _, _
  | _, Sum _ -> compatible (Sum(reduce_approx (Number 0) t1))
                           (Sum(reduce_approx (Number 0) t2))

  | _,_ -> false


(*****************************************
 * Flatten the default field of a record *
 * PML specific                          *
 *****************************************)
(* let _Record l = Record(l) *)

(*
 * FIXME: aren't we sure the default field appears as the first field? It seems
 * to be the case in the examples. (See assertion acc=[].)
 *)
let _Record l =
  let rec flatten_default l acc = match l with
      [] -> raise Exit
    | ("#default",Record[])::_ -> raise Exit
    | ("#default",Record(l))::r -> assert (acc=[]);
        let l = List.filter (function label,_ ->
                  not (List.mem_assoc label r) && not (List.mem_assoc label acc))
        l  (*??FIXME aren't the labels appearing in acc supposed to be shadowed by those in l??*)
        in
        Record(List.rev_append acc (List.rev_append l r))
    | ("#default",_)::_ -> raise Exit
    | r::l -> flatten_default l (r::acc)
  in
  match l with
    | ["#default",arg] -> arg
    | ("#default",Record[])::_ -> Record l
    | ("#default",Record l)::r ->
        let l = List.filter (function label,_ -> not (List.mem_assoc label r)) l
        in Record(l@r)
    | _ ->
        begin
          if debugOption "additional_sanity_checking"
          then  (match l with _::l -> assert (not (List.mem_assoc "#default" l))
                          | _ -> ())
        end;
        Record l


(******************
 * substitutions. *
 ******************)

(* Get term inside a substitution. *)
(* FIXME: explain why default to Sum[].
 * (Check if this is really what we want with partial applications) *)
let get_term i tau =
  try List.assoc i tau
  with Not_found -> Sum []

(* approximation order for substitutions *)
let approximates_substitution tau sigma =
  let rec indices a b acc =
    match a,b with
        [],b | b,[] -> List.rev_append (List.rev_map fst b) acc
      | (i,_)::a,(j,_)::b when i=j -> indices a b (i::acc)
      | _ -> assert false
  in
  List.for_all (function i ->
    let v=get_term i sigma in
    let u=get_term i tau in
    approximates u v) (indices tau sigma [])

(* compatibility for substitutions *)
let compatible_substitution =
  try
    List.for_all2 (fun x y -> compatible (snd x) (snd y))
  with
    Invalid_argument _ -> assert false (* we only check compatibility for self loops. *)


(* get a specific subtree inside a term: needed for substitution *)
let rec get_subtree ds v = match ds,v with
    [],v -> v
  | ds, Sum(bs) -> Sum(List.map (function w,d,i -> (add_int w (-(List.length ds))),d,i) bs)
  | ds, Epsilon(ds',i) -> Epsilon(List.rev_append ds ds', i)
  | RemoveVariant c::ds, Variant (c',v) when c=c' -> get_subtree ds v
  | RemoveVariant _::_, Variant _ -> raise Impossible_case
  | Project c::ds, Record l ->
    begin
    try
      let v = List.assoc c l in
      get_subtree ds v
    with
    Not_found -> (* if the label "c" isn't found in the record, we instead use
    its default field. Because records are flattened, the default should be a
    set of delta approximations for this to work. Otherwise something is missing
    from the original record... *)
      try
        let v = List.assoc "#default" l in
        get_subtree (Project c::ds) v
      with
        Not_found -> assert false (* typing problem *)
     end
 | (RemoveVariant _::_) as ds, Record l -> (* PML specific *)
    begin
    try
      let v = List.assoc "#default" l in
      get_subtree ds v
    with
      Not_found ->
        (
          print_string "*** TYPING PROBLEM...\n";
          print_string "*** the branch ";
          print_list " " print_destr ds ;
          print_string "\n*** meets the value ";
          print_term v;
          print_newline();
          assert false (* typing problem *)
        )
    end

  | ds,v ->
      (
        print_string "*** TYPING PROBLEM...\n";
        print_string "*** the branch ";
        print_list " " print_destr ds ;
        print_string "\n*** meets the value ";
        print_term v;
        print_newline();
        assert false (* typing problem *)
      )


(*
 * Syntactical substitution in a term, given an environment, with reducing to
 * normal forms.
 *)
let substitute u tau =
  (*
   * Travels inside the term until it finds a variable, preceded
   * by destructors, then uses the above function.
   *)
  let rec red_aux = function
      Variant(c,u) -> Variant(c,red_aux u)
    | Record l ->
        let labels,args = List.split l in
        let args = List.map red_aux args in
        _Record(List.combine labels args)
    | Epsilon(ds,i) ->
        let v = get_term i tau in
        get_subtree (List.rev ds) v
    | Sum(bs) ->
      let bss = sort_uniq (keep_max
        (List.fold_left merge []
          (List.map (function (w,ds,i) -> reduce_approx w (get_subtree (List.rev ds) (get_term i tau))) bs)))
      in
      if bss = []
      then raise Impossible_case
      else Sum bss

  in
    red_aux u


(**************
 * Collapsing *
 **************)

(* Collapsing the weights. *)
let rec collapse1 b u = match u with
    Variant(c,u) -> Variant(c,collapse1 b u)
  | Record l -> ifDebug "additional_sanity_checking" (fun _ -> sorted_labels l);
      let labels, args = List.split l in
      _Record(List.combine labels (List.map (collapse1 b) args)) (* TODO: _Record shouldn't be necessary here *)
  | Epsilon(ds,i) -> Epsilon(ds,i)
  | Sum(bs) ->  ifDebug "additional_sanity_checking" (fun _ -> sorted bs);
      Sum(sort_uniq (keep_max (List.map (function (w,ds,i) -> (collapse_z_infty b w, ds,i)) bs)))


(* Collapsing the destructors. *)
let rec collapse2 d u = match u with
    Variant(c,u) -> Variant(c,collapse2 d u)
  | Record l ->
      let labels, args = List.split l in
      _Record(List.combine labels (List.map (collapse2 d) args)) (* TODO: _Record shouldn't be necessary here *)
  | Epsilon(ds,i) ->
    begin
      let ds',r = get_suffix ds d in
      match r with
          [] -> Epsilon(ds,i)
        | _ -> Sum [ (Number(-(List.length r)),ds',i) ]
    end
  | Sum(bs) ->
    Sum (sort_uniq (keep_max (List.map (function (w,ds,i) ->
      let ds',r = get_suffix ds d in
      (add_int w (-(List.length r)),ds',i)) bs)))


(* Collapsing the constructors. *)
let rec collapse3 d u =
  if d=0
  then
    match u with
        Epsilon _ -> u
      | _ -> Sum (reduce_approx (Number 0) u)
  else
    match u with
        Record l ->
          let labels,args = List.split l in
            _Record (List.combine labels (List.map (collapse3 (d-1)) args)) (* TODO: _Record shouldn't be necessary here *)
      | Variant(c,u) -> Variant(c,collapse3 (d-1) u)
      | _ -> u


(*
 * The three of them together. (It could be slightly improved to prevent
 * traversing the term term three times, but it's probably not worth it.)
 *)
let collapse d b u = collapse1 b (collapse2 d (collapse3 d u))
let collapse_call d b tau = List.map (function i,u -> i,collapse d b u) tau


(*
 * Composition of substitutions, with collapse. (I don't need the uncollapsed
 * composition in the code.
 *)
let compose d b tau1 tau2 =
  collapse_call d b (List.map (function i,u -> i,(substitute u tau1)) tau2)


(*************************
 * Decreasing arguments. *
 *************************)

(* checks if a coherent loop has a decreasing subterm *)
let is_decreasing tau =

  let isOK ds t i =
    if approximates (Sum [Number(-1), ds, i]) t
    then
    begin
      ifDebug "show_decreasing_terms" begin fun _ ->
        print_string ("** Found decreasing node: **\n");
        print_term (Epsilon(ds,i));
        print_newline();
        print_newline()
      end;
      true
    end
    else false
  in
  (* checks if the i-th term is decreasing *)
  let decr it =
    let i,t = it in
    let rec aux ds t = match t with
        Variant(c,u) ->
          isOK ds t i ||
          aux ((RemoveVariant c)::ds) u
      | Record(l) ->
          isOK ds t i ||
          List.exists (function n,u -> aux ((Project n)::ds) u) l
      | t -> isOK ds t i
    in
    aux [] t
  in
  List.exists decr tau


(*****************************
 * Sets of calls and graphs. *
 *****************************)

(*
 * Adding a call to a set, keeping only maximal elements for the approximation
 * order.
 * It would be better if we could do this at the same time as the following
 * function: try to add the element, and raise an exception if it already
 * appears (or an approximation appears). This requires to use a custom map
 * module...
 *)
let add_call_set tau s =
  ifDebug "additional_sanity_checking" (fun _ -> sorted_call tau);
  if (debugOption "use_approximates")
  then
    if Calls_Set.exists (fun sigma -> approximates_substitution sigma tau) s
    then s
    else Calls_Set.add tau (Calls_Set.filter (fun sigma -> not (approximates_substitution tau sigma)) s)
  else
    Calls_Set.add tau s

(* Checks if a call brings new information. *)
let new_call_set tau s =
    if (debugOption "use_approximates")
    then not (Calls_Set.exists (fun sigma -> approximates_substitution sigma tau) s)
    else not (Calls_Set.mem tau s)  (* FIXME something might be wrong here *)

(* Counts the number of calls in a graph.  *)
let count_edges g = Call_Graph.fold (fun _ s n -> n+(Calls_Set.cardinal s)) g 0

(* Computing the transitive closure of a graph. *)
let transitive_closure initial_graph d b =

  (* references to keep some info about the graph *)
  let new_arcs = ref false in
  let nb_steps = ref 0 in

  (* single step for the TC. "ig" is the initial graph, "g" is the current graph *)
  let one_step_TC ig g =
    (*
     * local reference for the resulting graph: this is initialized to the
     * starting graph
     *)
    let result = ref g in

    Call_Graph.iter (fun fg a ->
      Call_Graph.iter (fun fg' a' ->
        let f,g = fg in
        let f',g' = fg' in
        if g=f'
        then begin
          Calls_Set.iter (fun tau ->
            Calls_Set.iter (fun tau' ->
              let all_calls = try Call_Graph.find (f,g') !result
                              with Not_found -> Calls_Set.empty
              in
              try
                let sigma : call = compose d b tau tau' in
                ifDebug "show_all_compositions"
                begin fun _ ->
                  print_string "** Composing: **\n";
                  print_substitution tau;
                  print_string "    with\n";
                  print_substitution tau';
                  print_string "    with B="; print_int b; print_string " and D="; print_int d; print_string " to give\n";
                  print_substitution sigma;
                  print_newline()
                end;
                if (new_call_set sigma all_calls)
                then begin
                  new_arcs := true;
                  result := Call_Graph.add (f,g') (add_call_set sigma all_calls) !result;
                end
              with Impossible_case -> ()
            ) a'
          ) a
        end
      ) g
    ) ig;
    !result
  in

  (*
   * Computing the actual closure. We know we've reached the TC when no new
   * edge was added.
   *)
  let rec closure ig g =
    new_arcs := false;
    ifDebug "show_all_steps"
    begin fun _ ->
      print_string ("** Graph of paths at iteration "^(string_of_int (!nb_steps))^" **\n");
      print_graph g;
      print_newline()
    end;
    let g = one_step_TC ig g in
    if not !new_arcs
    then g
    else begin
      nb_steps := !nb_steps+1;
      closure ig g
    end
  in

  (* collapse all substitutions *)
  ifDebug "show_initial_call_graph"
  begin fun _ ->
    print_string "** Control-flow graph given by the static analysis: **\n";
    print_graph initial_graph
  end;
  ifDebug "initial_collapse_of_graph"
  begin fun _ ->
  let initial_graph = Call_Graph.map (fun s ->
                Calls_Set.fold (fun tau s ->
                  add_call_set (collapse_call d b tau) s)
                  s Calls_Set.empty)
                  initial_graph in
  ifDebug "show_initial_call_graph"
  begin fun _ ->
    print_string "** Control-flow graph after collapse: **\n";
    print_graph initial_graph
  end
  end;
  let graph_of_paths = closure initial_graph initial_graph in

  ifDebug "show_final_call_graph"
  begin fun _ ->
    print_string "** Graph of paths of the initial control-flow graph: **\n";
    print_graph graph_of_paths
  end;
  ifDebug "show_summary_TC"
  begin fun _ ->
    print_string "* the initial control-flow graph contained "; print_int (count_edges initial_graph); print_string " edge(s) *\n";
    print_string "* its graph of paths contains "; print_int (count_edges graph_of_paths); print_string " edge(s) *\n";
    print_string "* "; print_int !nb_steps; print_string " iteration(s) were necessary to compute the graph of paths. *\n";
    print_newline()
  end;

  (* Returns the value of the TC. *)
  graph_of_paths


(* computes the list of function names (nodes) that are accessible from f in the
 * given graph *)
let accessible_from graph f =
  let seen = ref [] in
  let rec dfs n =
    assert (not (List.mem n !seen));
    seen := n::!seen;
    let next = Call_Graph.fold
                (fun xy s nxt ->
                   let x,y = xy in
                   if n = x && (not (Calls_Set.is_empty s)) && (not (List.mem y !seen))
                   then y::nxt
                   else nxt)
                graph
                []
    in
    List.iter dfs next
  in
  !seen

(**********************************************************************
 * Putting everything together: the size-change termination principle *
 **********************************************************************)

let size_change_termination_bounds graph d b =
  assert (d>=0 && b>0) ;

  let tc_graph = transitive_closure graph d b in
    Call_Graph.for_all
      (fun fg s ->
        let f,g = fg in
        f<>g ||
        Calls_Set.for_all
          (fun sigma ->
            try
              not (compatible_substitution sigma (compose d b sigma sigma)) ||
              begin
                ifDebug "show_coherents"
                begin fun _ ->
                  print_string ("** Found coherent loop from \"" ^ f ^ "\" to itself: **\n");
                  print_substitution sigma
                end;
                is_decreasing sigma ||
                (ifDebug "show_nondecreasing_coherents" begin fun _ ->
                  print_string ("** Found non-decreasing coherent loop from \"" ^ f ^ "\" to itself: **\n");
                  print_substitution sigma;
                  print_newline()
                end;
                false)
              end
            with Impossible_case -> true
          ) s
      ) tc_graph


(*****************************************
 * The functions called from the outside *
 *****************************************)

let size_bound = ref 1
let depth_bound = ref 2

let size_change_termination graph =
  let rec ds n acc =
    if (!depth_bound <= n)
    then List.rev (!depth_bound::acc)
    else ds (2*n) (n::acc)
  in
  let rec test = function
      [] -> false
    | d::ds ->
        ifDebug "show_summary_TC"
        begin fun _ ->
          print_string "** Incremental test: using d = ";
          print_int d;
          print_string " **";
          print_newline()
        end;
        let t = size_change_termination_bounds graph d !size_bound in
        if t
        then (
          ifDebug "show_summary_TC"
          begin fun _ ->
            print_string "** These functions are size change terminating for d=";
            print_int d; print_string " and b=";
            print_int !size_bound;print_string ". **\n\n"
          end;
          true)
        else
          test ds
  in
  let t = test (ds 1 [0]) in
  if t
  then true
  else (
    ifDebug "show_summary_TC"
    begin fun _ ->
      print_string "** These functions are NOT size change terminating for d=";
      print_int (!depth_bound); print_string " and b=";
      print_int (!size_bound);print_string ". **\n\n"
    end;
    false)