Source file Decoder.ml

(******************************************************************************)
(*                                                                            *)
(*                                  Inferno                                   *)
(*                                                                            *)
(*                       François Pottier, Inria Paris                        *)
(*                                                                            *)
(*  Copyright Inria. All rights reserved. This file is distributed under the  *)
(*  terms of the MIT License, as described in the file LICENSE.               *)
(*                                                                            *)
(******************************************************************************)

open Signatures

module Make
  (S : OSTRUCTURE)
  (U : MUNIFIER with type 'a structure := 'a S.structure)
  (O : OUTPUT with type 'a structure := 'a S.structure)
= struct
open U

(* -------------------------------------------------------------------------- *)

(* Decoding a variable. *)

(* The public function [decode_variable] decodes a variable, which must have
   leaf structure. The decoded variable is determined by the unique identity
   of the variable [v]. *)

let decode_variable (v : variable) : O.tyvar =
  let data = U.get v in
  assert (S.is_leaf data);
  O.inject (S.id data)

(* The internal function [decode_id] decodes a variable. As above, this
   variable must have leaf structure, and the decoded variable is determined
   by the unique identity [id], which is already at hand. *)

(* [O.variable] is used to convert the result from [O.tyvar] to [O.ty]. *)

let decode_id (id : id) : O.ty =
  O.variable (O.inject id)

(* -------------------------------------------------------------------------- *)

(* An acyclic decoder performs a bottom-up computation over an acyclic graph. *)

let new_acyclic_decoder () : variable -> O.ty =

  (* This hash table records the equivalence classes that have been visited
     and the value that has been computed for them. *)

  let visited : (id, O.ty) Hashtbl.t = Hashtbl.create 128 in

  let rec decode (v :  variable) : O.ty =
    let data = get v in
    let id = S.id data in
    try
      Hashtbl.find visited id
    with Not_found ->
      (* Because the graph is assumed to be acyclic, it is ok to update
         the hash table only after the recursive call. *)
      let a =
        if S.is_leaf data then
          decode_id id
        else
          O.structure (S.map decode data)
      in
      Hashtbl.add visited id a;
      a

  in
  decode

(* -------------------------------------------------------------------------- *)

(* The cyclic decoder is designed so as to be able to construct recursive
   types using μ syntax. We must ensure that every use of a μ-bound variable
   is dominated by its binder. *)

(* One cannot naively use a table of visited nodes, which maps every node to a
   decoded value (as done in the acyclic decoder above). Indeed, when an
   already-visited cycle is re-entered via a different path, we would risk
   producing a decoded value that contain variables that are meant to be
   μ-bound, but are actually unbound, because the μ binder lies along a
   different path. *)

(* Another naive approach would be to perform no memoization at all. This
   can work, but can be exponentially inefficient, because a DAG is decoded
   to a tree. *)

(* We choose to use a memoization table, [visited], but we memoize only the
   vertices that do not participate in a cycle. In practice, we expect cycles
   to be infrequent, so this approach should have good complexity. *)

(* The long-lived hash table [visited] maps the vertices that have been
   decoded already, and that do not participate in a cycle, to a decoded
   value. *)

(* When are asked to decode a vertex [v] that has not been memoized yet, we
   explore the graph formed by the vertices that are reachable from [v] and
   have not yet been memoized. We compute the strongly connected components
   of this graph. At a component of size 1, we memoize the decoded value. At
   a component of size greater than 1, we do not memoize it. The decoding
   process remains top-down, because (as far as I can tell) only a top-down
   process can tell us where μ binders must be placed. *)

(* -------------------------------------------------------------------------- *)

(* [isolated visited root] computes which unvisited vertices are reachable
   from [root]; computes the strongly connected components of this graph;
   and returns a function [isolated] of type [data -> bool] that
   indicates whether a vertex is the sole inhabitant of its component. *)

let isolated visited (root : variable) : data -> bool =

  (* A depth-first search lets us discover the unvisited vertices that
     are reachable from [root]. At the same time, we count them, and
     assign a unique index to each of them. *)

  let n = ref 0 in
  let discovered : (id, int) Hashtbl.t = Hashtbl.create 16 in
  let inhabitants : data list ref = ref [] in
  let rec discover v =
    let data = get v in
    let id = S.id data in
    if not (Hashtbl.mem visited id || Hashtbl.mem discovered id) then begin
      Hashtbl.add discovered id (Utils.postincrement n);
      inhabitants := data :: !inhabitants;
      S.iter discover data
    end
  in
  discover root;

  (* Then, we compute the strongly connected components of this graph. *)

  let module G = struct
    type node = data
    let n = !n
    let index data =
      try Hashtbl.find discovered (S.id data)
      with Not_found -> assert false
    let successors yield data =
      data |> S.iter (fun v ->
        let data = get v in
        if Hashtbl.mem discovered (S.id data) then yield data
      )
    let iter yield = List.iter yield !inhabitants
  end in
  let module T = Tarjan.Run(G) in
  T.isolated

(* -------------------------------------------------------------------------- *)

(* The short-lived hash table [table] (which is empty when the decoder is
   inactive) records which vertices are the target of a back edge and
   therefore need a μ binder. A vertex is mapped to [Active] when it is
   being visited. It is mapped to [Rediscovered] when it is being visited
   and a back edge to it has been discovered. This indicates that this
   vertex needs a μ binder. *)

type status =
  | Active
  | Rediscovered

(* -------------------------------------------------------------------------- *)

(* The cyclic decoder. *)

let new_cyclic_decoder () : variable -> O.ty =

  (* The long-lived table. *)
  let visited : (id, O.ty) Hashtbl.t = Hashtbl.create 128 in
  (* The short-lived table. *)
  let table : (id, status) Hashtbl.t = Hashtbl.create 128 in

  (* The toplevel decoding function. *)

  let decode (root : variable) : O.ty =

    (* If [root] appears in the table [visited], we are done. *)
    let data = get root in
    try
      Hashtbl.find visited (S.id data)
    with Not_found ->

      (* Otherwise, discover the unvisited vertices that are reachable from
         [root], and determine which of them are isolated, that is, which of
         them lie in a component of size 1. *)
      let isolated = isolated visited root in

      (* Then, the following recursive decoding function is used. The
         short-lived table [table] is used to detect back edges and
         determine where μ binders must be placed. *)

      let rec decode (v : variable) : O.ty =
        (* If [v] appears in the table [visited], we are done. *)
        let data = get v in
        let id = S.id data in
        try
          Hashtbl.find visited id
        with Not_found ->
          (* Otherwise, compute a decoded value [a] for this vertex. *)
          let a =
            if S.is_leaf data then
              (* There is no structure. *)
              decode_id id
            else
              (* There is some structure. *)
              if Hashtbl.mem table id then begin
                (* We have just rediscovered this vertex via a back edge. Its
                   status may be [Active] or [Rediscovered]. We change it to
                   [Rediscovered], and stop the traversal. *)
                Hashtbl.replace table id Rediscovered;
                decode_id id
              end
              else begin
                (* This vertex is not being visited. Before the recursive
                   call, mark it as being visited. *)
                Hashtbl.add table id Active;
                (* Perform the recursive traversal. *)
                let a = O.structure (S.map decode data) in
                (* Mark this vertex as no longer being visited. If it was
                   recursively rediscovered during the recursive call,
                   introduce a μ binder. (It would be correct but noisy to
                   always introduce a μ binder.) *)
                let status =
                  try Hashtbl.find table id with Not_found -> assert false
                in
                Hashtbl.remove table id;
                match status with
                | Active -> a
                | Rediscovered -> O.mu (O.inject id) a
              end
          in
          (* If this vertex is isolated, store the decoded value [a] in the
             memoization table [visited]. (It would be correct to never
             memoize. It would be incorrect to always memoize.) *)
          if isolated data then
            Hashtbl.add visited id a;
          a
      in

      assert (Hashtbl.length table = 0);
      let a = decode root in
      assert (Hashtbl.length table = 0);
      a

  in
  decode

(* -------------------------------------------------------------------------- *)

end (* Make *)