Module Cpscheck


open Cpsdef

For each kind of check, we provide a function to check an entire expression.
module type S = sig
   val expression: expression → unit
2.  This module allows checking the uplinks. We recursively traverse a expression, and for each expression t we find, we examine its elements (variables, occurrences, subexpressions...). If the element has an uplink, it must point to t.
module Uplinks = struct

   The following function is necessary (rather than just comparing 2 enclosings with =) because comparison of uplinks is done with ; so we must perform a match on the enclosing expression before comparing it with x.
   let check_enclosing_equal_to_expression enclosing expression =

     let print_error() = 
       Format.eprintf "\nError: wrong uplink: should point to %a@."
         Cpsprint.expression expression in

     match enclosing with
     ∣ Enclosing_expression t when t ≡ expression → ()
     ∣ Enclosing_expression t →
         Format.eprintf "Instead, points to %a@." Cpsprint.expression t;
         assert false)
     ∣ _ → (print_error();
               assert false)

   Checks that all the components in an expression (subexpressions, variables, occurrences...) have their uplink correctly set to t.
   let one_expression t =
     (∗ Each of the following helper function performs a complete check on the corresponding element (e.g. var checks variables, occ occurences etc. In addition body recurses. ∗)
     let body t’ =
       check_enclosing_equal_to_expression (Expression.enclosing t’) t in
     let var var =
       let enclosing = Var.Var.binding_site var in
       check_enclosing_equal_to_expression enclosing t in
     let var_list vl = List.iter var vl in

     Note that cont_var, occ and cont_occ do not yet have uplinks.
     let cont_var cont_var = () in
     let occ occ = () in
     let occ_list ol = List.iter occ ol in
     let cont_occ cont_occ = () in

     let value = function
       ∣ Constant(_) ∣ External(_) → ()
       ∣ Tuple(l) → List.iter occ l
       ∣ Injection(_,_,t) → occ t
       ∣ Lambda(_,k,vl,b) → cont_var k; var_list vl; body b in

     let prim = function 
       ∣ Value v → value v
       ∣ Projection(_,t) → occ t
       ∣ Integer_binary_operation(_,a,b) → occ a; occ b
       ∣ Integer_binary_predicate(_,a,b) → occ a; occ b in

     match Expression.get t with
     ∣ Let_prim(x, p, b) → var x; prim p; body b
     ∣ Let_cont(k,x,bc,b) → cont_var k; var x; body bc; body b
     ∣ Apply(_,f,k,xl) → occ f; cont_occ k; occ_list xl
     ∣ Apply_cont(k,x) → cont_occ k; occ x
     ∣ Case(o,l,d) →
       ( occ o;
         CaseMap.iter (fun _ k → cont_occ k) l;
         match d with None → () ∣ Some(k) → cont_occ k)
     ∣ Halt(x) → occ x

   let expression t = Cpstraverse.iter_on_expressions
     ~enter_lambdas:true t one_expression


3.  This module allows checking the occurrences. For each variable, we build the Set of its occurrences, A. Each variable is linked to a set of occurrences, represented by a doubly linked list, B. We check that A = B, i.e. that ABBA. The code performs these two checks separately (in particular because A and B have different data structures)
module Occurrences:S = struct

   This functor factorizes the code common to Var and Cont_var.
   module Make(Var:Cpsdef.VAR_RW) = struct

     For each variable x in a term t, we build a map mapping x to the set of occurrences of x we found in t. This map is build and used using a depth-first traversal on terms. The definition and expression data structures require that the term containing the binding site of a variable v is an ancestor of all the expressions containing occurrences of v. Thus a depth-first traversal of terms will encounter the binding site of the variable on the way down, then all occurrences, then the binding site of the variable on the way up.

When we first encounter the variable, we associate it to the empty set (function add_variable).

When we encounter an occurrence, we update the map associated to its binding variable (function add_occurrence).

When we last encounter the variable, we known that we have found all occurrences in the expression; thus we compare the sets of occurrences (function compare_set).
     Return a new map with x mapped to an empty set.

     let add_variable x map = 
       (∗ Check that x is not already in the map. ∗)
       assert( ¬ (Var.Var.Map.mem x map));
       let map = Var.Var.Map.add x (Var.Occur.Set.empty) map in

     Return a new map with o added to the set of occurrences of x.
     let add_occurrence o map =
       let x = (Var.Occur.binding_variable o) in 
         let set = (Var.Var.Map.find x map) in
         let newset = Var.Occur.Set.add o set in
         Var.Var.Map.add x newset map
       with Not_found → assert false

     Compare the set of occurrences in the doubly-linked list of x with the set given as an argument. Returns void if they are equal, and fails if they are not.

The algorithm is the same for both kind of set comparisons:

  1. First we have or define a function that checks whether one element e in a set s is in the other set s’, by comparing e with every element in s’
  2. We iterate this function on all elements e in s, which tells use that ss′.

Once we know that ss′ and s′ ⊆ s, we deduce that s = s′.

     let compare_sets x set =

       let check_set_subset_of_doubly_linked_list () =
         let is_in_doubly_linked_list occ = 
             Var.Var.fold_on_occurrences x () (fun () o →
               if o ≡ occ then failwith "found");
           with _ → true in

         Var.Occur.Set.iter (fun occ →
           if (is_in_doubly_linked_list occ)
           then ()
             failwith("Element "^(Var.Occur.to_string occ)^" in CPS expression "
                     ^ "was not in the doubly linked list")) set in

       let check_doubly_linked_list_subset_of_set () = 
         Var.Var.fold_on_occurrences x () (fun () o → 
           if Var.Occur.Set.mem o set
           then ()
             failwith ("Element "^(Var.Occur.to_string o)^" in the "
                     ^ "doubly linked list was not in the CPS expression")) in



   module MakeVar = Make(Var)

   module MakeContVar = Make(Cont_var)

   The depth-first traversal of the variables and occurrences in the expression is handled by the fold_on_variables_and_occurrences function.
   let expression t =
     let beforevar (map,contmap) x = (MakeVar.add_variable x map, contmap) in
     let beforecontvar (map,contmap) k = (map,MakeContVar.add_variable k contmap) in

     let focc (map,contmap) o = (MakeVar.add_occurrence o map, contmap) in
     let fcontocc (map,contmap) o = (map, MakeContVar.add_occurrence o contmap) in

     let aftervar (map,contmap) x =
       MakeVar.compare_sets x (Var.Var.Map.find x map);
       (map,contmap) in
     let aftercontvar (map,contmap) x =
       MakeContVar.compare_sets x (Cont_var.Var.Map.find x contmap);
       (map,contmap) in
     let init = (Var.Var.Map.empty, Cont_var.Var.Map.empty) in
     ignore(Cpstraverse.fold_on_variables_and_occurrences t init
               ~before_var:beforevar ~occ:focc ~after_var:aftervar
               ~before_cont_var:beforecontvar ~cont_occ:fcontocc ~after_cont_var:aftercontvar)


module Contains = struct
   let var t_ v = match t_ with
     ∣ Let_prim(x,_,_) when x ≡ v → true
     ∣ Let_cont(_,x,_,_) when x ≡ v → true
     ∣ Let_prim(_,Value(Lambda(_,_,xl,_)),_) when List.memq v xl → true
     ∣ _ → false

   let cont_var t_ cv = match t_ with
     ∣ Let_cont(k,_,_,_) when k ≡ cv → true
     ∣ Let_prim(_,Value(Lambda(_,k,_,_)),_) when k ≡ cv → true
     ∣ _ → false

   let subexpression expr_ subexpr = match expr_ with
   ∣ Let_cont(_,_,t1,t2) when subexpr ≡ t1 ∨ subexpr ≡ t2 → true
   ∣ Let_prim(_,_,t) when subexpr ≡ t → true
   ∣ Let_prim(_,Value(Lambda(_,_,_,t)),_) when subexpr ≡ t → true
   ∣ _ → false


module And = struct
   let set_enclosing t e = (match e with
     ∣ Enclosing_expression(superexpression) →
       assertContains.subexpression (Expression.get superexpression) t));
     Expression.set_enclosing t e

   let set_expression t t_ =
     Expression.set t t_;
     Uplinks.one_expression t

   let fill e t_ =
     let t = Empty.fill e t_ in
     Uplinks.one_expression t;