hirrolot · October 1, 2024 16:54 · hirrolot · Jul 22, 2024
diff --git a/a-preface.md b/a-preface.md
diff --git a/supercomp.ml b/supercomp.ml
 (******************************************************************************)
 (* AST definitions. *)

 type call_kind = CtrKind | FKind | GKind

 and term = Var of string | Call of call_kind * string * term list
 [@@deriving eq, show { with_path = false }]

 let var x = Var x
 let ctr_call (c, args) = Call (CtrKind, c, args)
 let f_call (f, args) = Call (FKind, f, args)
 let g_call (g, scrutinee, args) = Call (GKind, g, scrutinee :: args)

 (******************************************************************************)
 (* Search tables for f- and g-functions. *)

 module String_map = Map.Make (String)
 module F_rules = String_map
 module G_rules_by_name = String_map
 module G_rules_by_pattern = String_map

 type param_list = string list

 type program = {
  f_rules : (param_list * term) F_rules.t;
  g_rules :
    (param_list * param_list * term) G_rules_by_pattern.t G_rules_by_name.t;
 }

 let find_exn ~key ~on_none map =
  match String_map.find_opt key map with
  | Some value -> value
  | None -> on_none ()

 let panic fmt = Format.ksprintf failwith fmt

 let find_f_rule ~program f =
  find_exn ~key:f
    ~on_none:(fun () -> panic "find_f_rule: no such function `%s`" f)
    program.f_rules

 let find_g_rule_list ~program g =
  find_exn ~key:g
    ~on_none:(fun () -> panic "find_g_rule_list: no such function `%s`" g)
    program.g_rules

 let find_g_rule ~program (g, c) =
  find_g_rule_list ~program g
  |> find_exn ~key:c ~on_none:(fun () ->
         panic "find_g_rule: no such pattern `%s` for `%s`" c g)

 (******************************************************************************)
 (* Fresh identifiers generation. *)

 let var_counter, g_counter, f_counter = (ref 0, ref 0, ref 0)

 let fresh_id ?(counter = var_counter) ?(prefix = "v") () =
  let x = !counter in
  counter := !counter + 1;
  prefix ^ string_of_int x

 let fresh_var_list length_list = List.map (fun _ -> fresh_id ()) length_list
 let fresh_ctr (c, fresh_vars) = ctr_call (c, List.map var fresh_vars)

 (******************************************************************************)
 (* Substitution on terms. *)

 module Subst = String_map

 let scan_subst ~f subst = subst |> Subst.to_seq |> Seq.find_map f

 let rec subst ~map = function
  | Var x as default -> Subst.find_opt x map |> Option.value ~default
  | Call (kind, h, args) -> Call (kind, h, List.map (subst ~map) args)

 let subst_params (params, args) t =
  subst ~map:(Subst.of_list (List.combine params args)) t

 type contraction = { c : string; fresh_vars : string list }
 [@@deriving eq, show { with_path = false }]

 let unify ~x ~contraction:{ c; fresh_vars } args =
  List.map (subst_params ([ x ], [ fresh_ctr (c, fresh_vars) ])) args

 (******************************************************************************)
 (* Term matching. *)

 (* Tests whether [t2] is an instance of [t1]. If it is, returns a substitution
   [map] such that [equal_term (subst ~map t1) t2]. *)
 let match_against (t1, t2) =
  let exception Fail in
  let subst = ref Subst.empty in
  let rec go (t1, t2) =
    match t1 with
    | Var x -> (
        match Subst.find_opt x !subst with
        | Some x_subst -> if not (equal_term x_subst t2) then raise Fail
        | None -> subst := Subst.add x t2 !subst)
    | Call (kind, h, args) -> (
        match t2 with
        | Call (kind', h', args') when equal_call_kind kind kind' && h = h' ->
            List.iter2 (fun arg arg' -> go (arg, arg')) args args'
        | _ -> raise Fail)
  in
  try
    go (t1, t2);
    Some !subst
  with Fail -> None

 (******************************************************************************)
 (* Normal-order reduction ("driving"). *)

 type 'a step =
  (* Stop on a free variable. *)
  | Stop of string
  (* Decompose a constructor. *)
  | Decompose of string * 'a list
  (* Unfold a call. *)
  | Transient of 'a
  (* Case-analysis of a g-call. *)
  | Variants of string * (contraction * 'a) list
 [@@deriving eq, show { with_path = false }]

 (* Implements "Fig. 6. Normal-order reduction step". *)
 let rec reduce ~program = function
  | Var x -> Stop x
  | Call (CtrKind, c, args) -> Decompose (c, args)
  | Call (FKind, f, args) ->
      let params, s = find_f_rule ~program f in
      Transient (subst_params (params, args) s)
  | Call (GKind, g, Call (CtrKind, c, args) :: args') ->
      let params, params', s = find_g_rule ~program (g, c) in
      Transient (subst_params (params @ params', args @ args') s)
  | Call (GKind, g, Var x :: args) ->
      Variants (x, reduce_variants ~program (x, g, args))
  | Call (GKind, g, (Call _ as t) :: args) -> reduce_inner ~program (t, g, args)
  | Call (GKind, g, []) -> panic "reduce: no scrutinee for `%s`" g

 and reduce_variants ~program (x, g, args) =
  let unfold_rule (c, (params, params', s)) =
    let fresh_vars = fresh_var_list params in
    let contraction = { c; fresh_vars } in
    let args = List.map var fresh_vars @ unify ~x ~contraction args in
    (contraction, subst_params (params @ params', args) s)
  in
  find_g_rule_list ~program g
  |> G_rules_by_name.bindings |> List.map unfold_rule

 and reduce_inner ~program (t, g, args) =
  match reduce ~program t with
  | Transient t -> Transient (g_call (g, t, args))
  | Variants (x, variants) ->
      let propagate_contraction (contraction, t) =
        (contraction, g_call (g, t, unify ~x ~contraction args))
      in
      Variants (x, List.map propagate_contraction variants)
  | _ -> panic "reduce_inner: impossible"

 (******************************************************************************)
 (* The homeomorphic embedding relation. *)

 (* Implements "Fig. 7. Homeomorphic embedding". *)
 let rec decide_he = function
  | Var _x, Var _y -> true
  | s, (Call _ as t) -> he_by_diving (s, t) || he_by_coupling (s, t)
  | Call _, Var _ -> false

 and he_by_diving = function
  | s, Call (_kind, _h, args) -> List.exists (fun t -> decide_he (s, t)) args
  | _, _ -> false

 and he_by_coupling = function
  | Call (kind, h, args), Call (kind', h', args')
    when equal_call_kind kind kind' && h = h' ->
      List.for_all2 (fun s t -> decide_he (s, t)) args args'
  | _, _ -> false

 (******************************************************************************)
 (* Computing MSG, a "Most Specific Generalization". *)

 let common_functor (g, subst_1, subst_2) =
  subst_1
  |> scan_subst ~f:(function
       | x, Call (kind, h, args) ->
           subst_2
           |> scan_subst ~f:(function
                | y, Call (kind', h', args')
                  when x = y && equal_call_kind kind kind' && h = h' ->
                    Some (x, kind, h, args, args')
                | _ -> None)
       | _ -> None)
  |> Option.map (fun (x, kind, h, args, args') ->
         let fresh_vars = fresh_var_list args in
         let common_call = Call (kind, h, List.map var fresh_vars) in
         let new_subst ~args old_subst =
           List.fold_left
             (fun acc (fresh_var, arg) -> Subst.add fresh_var arg acc)
             (Subst.remove x old_subst)
             (List.combine fresh_vars args)
         in
         ( subst ~map:(Subst.singleton x common_call) g,
           new_subst ~args subst_1,
           new_subst ~args:args' subst_2 ))

 let common_subst (g, subst_1, subst_2) =
  subst_1
  |> scan_subst ~f:(fun (x, s) ->
         subst_1
         |> scan_subst ~f:(fun (y, s') ->
                if
                  x != y && equal_term s s'
                  && Option.bind (Subst.find_opt x subst_2) (fun t ->
                         Subst.find_opt y subst_2
                         |> Option.map (fun t' -> equal_term t t'))
                     |> Option.value ~default:false
                then Some (x, y)
                else None))
  |> Option.map (fun (x, y) ->
         let new_subst old_subst = Subst.remove x old_subst in
         ( subst ~map:(Subst.singleton x (Var y)) g,
           new_subst subst_1,
           new_subst subst_2 ))

 let step ~rules triple = List.find_map (fun f -> f triple) rules

 (* Exhaustively applies the two rewrite rules. *)
 let rec loop triple =
  match step ~rules:[ common_functor; common_subst ] triple with
  | Some triple' -> loop triple'
  | None -> triple

 (* Implements "Fig. 10. Computing most specific generalizations". *)
 let compute_msg (t1, t2) =
  let seed = fresh_id () in
  let g, subst_1, subst_2 =
    (Var seed, Subst.singleton seed t1, Subst.singleton seed t2)
  in
  loop (g, subst_1, subst_2)

 (******************************************************************************)
 (* The supercompilation algorithm itself! *)

 type graph = Step of graph step | Bind of (string * graph) list * bind_kind
 and bind_kind = Let of graph | Fold of de_bruijn_idx
 and de_bruijn_idx = int [@@deriving eq, show { with_path = false }]

 (* Implements "Algorithm 7 (positive supercompilation.)". *)
 let supercompile ~program t =
  let rec go ~history n =
    match
      List.find_mapi
        (fun i m -> if decide_he (m, n) then Some (i, m) else None)
        history
    with
    (* We must stop direct unfolding to avoid non-termination. *)
    | Some (i, m) -> (
        match match_against (m, n) with
        (* [n] is an instance of [m]. *)
        | Some subst -> fold ~history:(n :: history) ~subst i
        | None -> (
            let g, _subst_1, subst_2 = compute_msg (m, n) in
            match g with
            (* [m] and [n] are disjoint. *)
            | Var _x -> split ~history:(n :: history) n
            (* [m] and [n] have a "meaningful" generalization. *)
            | _ -> generalize ~history:(n :: history) ~subst_2 g))
    (* Everything is good, continue unfolding. *)
    | None -> Step (step ~history:(n :: history) n)
  and fold ~history ~subst i =
    Bind
      ( subst |> Subst.bindings
        |> List.map (fun (x, child) -> (x, go ~history child)),
        Fold i )
  and split ~history = function
    | Call (kind, h, args) ->
        let fresh_vars = fresh_var_list args in
        let t_g = Call (kind, h, List.map var fresh_vars) in
        Bind
          ( List.map2 (fun x t -> (x, go ~history t)) fresh_vars args,
            Let (go ~history t_g) )
    | _ -> panic "split: impossible"
  and generalize ~history ~subst_2 g =
    Bind
      ( subst_2 |> Subst.bindings
        |> List.map (fun (x, child) -> (x, go ~history child)),
        Let (go ~history g) )
  and step ~history n =
    match reduce ~program n with
    | Stop x -> Stop x
    | Decompose (c, args) -> Decompose (c, List.map (go ~history) args)
    | Transient t -> Transient (go ~history t)
    | Variants (x, variants) ->
        Variants
          ( x,
            List.map
              (fun (contraction, t) -> (contraction, go ~history t))
              variants )
  in
  go ~history:[] t

 (******************************************************************************)
 (* Residual program generation. *)

 module Free_vars = Set.Make (String)

 let union_free_vars list =
  let out_list, free_vars_list = List.split list in
  let free_vars =
    List.fold_left Free_vars.union Free_vars.empty free_vars_list
  in
  (out_list, free_vars)

 (* Invariants:
   - We always arrange function parameters lexicographically. This ensures that
     recursive functions are called with proper argument positions.
   - We generate only recursive f-functions. This means that useless functions
     are "inlined" automatically.
   - When processing a graph node (either [Step] or [Bind]), the history length
     must be the same as in [supercompile].
 *)

 let residuate graph =
  let f_rules, g_rules = (ref F_rules.empty, ref G_rules_by_name.empty) in
  let gen_f ~def_meta:(fresh_f, is_called) ~free_vars t_out =
    if !is_called then (
      (* If the function is called recursively, generate a new definition. *)
      let free_vars_list = Free_vars.elements free_vars in
      f_rules := F_rules.add fresh_f (free_vars_list, t_out) !f_rules;
      (f_call (fresh_f, List.map var free_vars_list), free_vars))
    else
      (* Otherwise, just return the term that would have resulted in the
         function's body. In essence, this performs definition inlining, but
         without generating a definition! *)
      (t_out, free_vars)
  in
  let f_meta () =
    let fresh_f = fresh_id ~counter:f_counter ~prefix:"f" () in
    let is_called = ref false in
    (fresh_f, is_called)
  in
  let rec go ~history = function
    | Step (Stop x) -> (Var x, Free_vars.singleton x)
    | Step (Decompose (c, args)) -> go_decompose ~history (c, args)
    | Step (Transient t) -> go_transient ~history t
    | Step (Variants (x, variants)) -> go_variants ~history (x, variants)
    | Bind (bindings, Let t) -> go_bind_let ~history (bindings, t)
    | Bind (bindings, Fold i) -> go_bind_fold ~history (bindings, i)
  (* Generate an f-function definition that calls a constructor. *)
  and go_decompose ~history (c, args) =
    let def_meta = f_meta () in
    let args_out, free_vars =
      args |> List.map (go ~history:(`F def_meta :: history)) |> union_free_vars
    in
    gen_f ~def_meta ~free_vars (ctr_call (c, args_out))
  (* Generate a transient f-function definition. *)
  and go_transient ~history t =
    let def_meta = f_meta () in
    let t_out, free_vars = go ~history:(`F def_meta :: history) t in
    gen_f ~def_meta ~free_vars t_out
  (* Generate a g-function definition that describes the variants. *)
  and go_variants ~history (x, variants) =
    let fresh_g = fresh_id ~counter:g_counter ~prefix:"g" () in
    let variants_out, free_vars =
      variants
      |> List.map (fun (({ fresh_vars; _ } as contraction), t) ->
             let t_out, free_vars = go ~history:(`G fresh_g :: history) t in
             let free_vars = Free_vars.(diff free_vars (of_list fresh_vars)) in
             ((contraction, t_out), free_vars))
      |> union_free_vars
    in
    let free_vars_list = Free_vars.elements free_vars in
    let rules =
      variants_out
      |> List.map (fun ({ c; fresh_vars }, t_out) ->
             (c, (fresh_vars, free_vars_list, t_out)))
      |> G_rules_by_pattern.of_list
    in
    g_rules := G_rules_by_name.add fresh_g rules !g_rules;
    ( g_call (fresh_g, Var x, List.map var free_vars_list),
      Free_vars.add x free_vars )
  (* Residuate the bindings and substitute them to the body. *)
  and go_bind_let ~history (bindings, t) =
    let def_meta = f_meta () in
    let bindings_out, free_vars =
      go_bindings ~history:(`F def_meta :: history) bindings
    in
    (* Due to the way how an MSG is computed, [_free_vars'] is the set of fresh
       variables from [bindings_out]. *)
    let t_out, _free_vars' = go ~history:(`F def_meta :: history) t in
    gen_f ~def_meta ~free_vars (subst ~map:(Subst.of_list bindings_out) t_out)
  (* Residuate the bindings and make a recursive function call. *)
  and go_bind_fold ~history (bindings, i) =
    let def_meta = f_meta () in
    let bindings_out, free_vars =
      go_bindings ~history:(`F def_meta :: history) bindings
    in
    let args = List.map (fun (_x, t) -> t) bindings_out in
    let t_out =
      match List.nth history i with
      | `F (f, is_called) ->
          (* We will generate a definition for this recursive function [f]. *)
          is_called := true;
          f_call (f, args)
      | `G g -> Call (GKind, g, args)
    in
    gen_f ~def_meta ~free_vars t_out
  and go_bindings ~history bindings =
    bindings
    |> List.map (fun (x, t) ->
           let t_out, free_vars = go ~history t in
           ((x, t_out), free_vars))
    |> union_free_vars
  in
  let t_out, _free_vars = go ~history:[] graph in
  ({ f_rules = !f_rules; g_rules = !g_rules }, t_out)

 (******************************************************************************)
 (* Initial program construction. *)

 let create_program ?(f_rules = []) ?(g_rules = []) () =
  let prepare_f_rule (f, params, t) = (f, (params, t)) in
  let prepare_g_rule_by_name (g, rules) =
    let prepare_g_rule_by_pattern ((c, params), params', t) =
      (c, (params, params', t))
    in
    ( g,
      rules |> List.map prepare_g_rule_by_pattern |> G_rules_by_pattern.of_list
    )
  in
  {
    f_rules = f_rules |> List.map prepare_f_rule |> F_rules.of_list;
    g_rules =
      g_rules |> List.map prepare_g_rule_by_name |> G_rules_by_name.of_list;
  }

 (******************************************************************************)
 (* Pretty-printing. *)

 let rec term_to_string = function
  | Var x -> x
  | Call (_kind, h, args) ->
      Printf.sprintf "%s(%s)" h
        (String.concat ", " (List.map term_to_string args))

 let print_program { f_rules; g_rules } =
  let go_f_rule (f, params, t) =
    Printf.sprintf "%s(%s) = %s" f
      (String.concat ", " params)
      (term_to_string t)
  in
  let go_g_rule (g, (c, params), params', t) =
    Printf.sprintf "%s(%s(%s)%s%s) = %s" g c
      (String.concat ", " params)
      (if List.is_empty params' then "" else ", ")
      (String.concat ", " params')
      (term_to_string t)
  in
  let f_rules =
    f_rules |> F_rules.bindings
    |> List.map (fun (f, (params, t)) -> go_f_rule (f, params, t))
  in
  let g_rules =
    g_rules |> G_rules_by_name.bindings
    |> List.map (fun (g, rules) ->
           rules |> G_rules_by_pattern.bindings
           |> List.map (fun (c, (params, params', t)) ->
                  go_g_rule (g, (c, params), params', t)))
    |> List.flatten
  in
  f_rules @ g_rules

 (******************************************************************************)
 (* Program optimization. *)

 let optimize ?f_rules ?g_rules t =
  var_counter := 0;
  f_counter := 0;
  g_counter := 0;
  let program = create_program ?f_rules ?g_rules () in
  let program_out, t_out = supercompile ~program t |> residuate in
  (term_to_string t_out, print_program program_out)
	(******************************************************************************)
	(* AST definitions. *)

	type call_kind = CtrKind \| FKind \| GKind

	and term = Var of string \| Call of call_kind * string * term list
	[@@deriving eq, show { with_path = false }]

	let var x = Var x
	let ctr_call (c, args) = Call (CtrKind, c, args)
	let f_call (f, args) = Call (FKind, f, args)
	let g_call (g, scrutinee, args) = Call (GKind, g, scrutinee :: args)

	(******************************************************************************)
	(* Search tables for f- and g-functions. *)

	module String_map = Map.Make (String)
	module F_rules = String_map
	module G_rules_by_name = String_map
	module G_rules_by_pattern = String_map

	type param_list = string list

	type program = {
	f_rules : (param_list * term) F_rules.t;
	g_rules :
	(param_list * param_list * term) G_rules_by_pattern.t G_rules_by_name.t;
	}

	let find_exn ~key ~on_none map =
	match String_map.find_opt key map with
	\| Some value -> value
	\| None -> on_none ()

	let panic fmt = Format.ksprintf failwith fmt

	let find_f_rule ~program f =
	find_exn ~key:f
	~on_none:(fun () -> panic "find_f_rule: no such function `%s`" f)
	program.f_rules

	let find_g_rule_list ~program g =
	find_exn ~key:g
	~on_none:(fun () -> panic "find_g_rule_list: no such function `%s`" g)
	program.g_rules

	let find_g_rule ~program (g, c) =
	find_g_rule_list ~program g
	\|> find_exn ~key:c ~on_none:(fun () ->
	panic "find_g_rule: no such pattern `%s` for `%s`" c g)

	(******************************************************************************)
	(* Fresh identifiers generation. *)

	let var_counter, g_counter, f_counter = (ref 0, ref 0, ref 0)

	let fresh_id ?(counter = var_counter) ?(prefix = "v") () =
	let x = !counter in
	counter := !counter + 1;
	prefix ^ string_of_int x

	let fresh_var_list length_list = List.map (fun _ -> fresh_id ()) length_list
	let fresh_ctr (c, fresh_vars) = ctr_call (c, List.map var fresh_vars)

	(******************************************************************************)
	(* Substitution on terms. *)

	module Subst = String_map

	let scan_subst ~f subst = subst \|> Subst.to_seq \|> Seq.find_map f

	let rec subst ~map = function
	\| Var x as default -> Subst.find_opt x map \|> Option.value ~default
	\| Call (kind, h, args) -> Call (kind, h, List.map (subst ~map) args)

	let subst_params (params, args) t =
	subst ~map:(Subst.of_list (List.combine params args)) t

	type contraction = { c : string; fresh_vars : string list }
	[@@deriving eq, show { with_path = false }]

	let unify ~x ~contraction:{ c; fresh_vars } args =
	List.map (subst_params ([ x ], [ fresh_ctr (c, fresh_vars) ])) args

	(******************************************************************************)
	(* Term matching. *)

	(* Tests whether [t2] is an instance of [t1]. If it is, returns a substitution
	[map] such that [equal_term (subst ~map t1) t2]. *)
	let match_against (t1, t2) =
	let exception Fail in
	let subst = ref Subst.empty in
	let rec go (t1, t2) =
	match t1 with
	\| Var x -> (
	match Subst.find_opt x !subst with
	\| Some x_subst -> if not (equal_term x_subst t2) then raise Fail
	\| None -> subst := Subst.add x t2 !subst)
	\| Call (kind, h, args) -> (
	match t2 with
	\| Call (kind', h', args') when equal_call_kind kind kind' && h = h' ->
	List.iter2 (fun arg arg' -> go (arg, arg')) args args'
	\| _ -> raise Fail)
	in
	try
	go (t1, t2);
	Some !subst
	with Fail -> None

	(******************************************************************************)
	(* Normal-order reduction ("driving"). *)

	type 'a step =
	(* Stop on a free variable. *)
	\| Stop of string
	(* Decompose a constructor. *)
	\| Decompose of string * 'a list
	(* Unfold a call. *)
	\| Transient of 'a
	(* Case-analysis of a g-call. *)
	\| Variants of string * (contraction * 'a) list
	[@@deriving eq, show { with_path = false }]

	(* Implements "Fig. 6. Normal-order reduction step". *)
	let rec reduce ~program = function
	\| Var x -> Stop x
	\| Call (CtrKind, c, args) -> Decompose (c, args)
	\| Call (FKind, f, args) ->
	let params, s = find_f_rule ~program f in
	Transient (subst_params (params, args) s)
	\| Call (GKind, g, Call (CtrKind, c, args) :: args') ->
	let params, params', s = find_g_rule ~program (g, c) in
	Transient (subst_params (params @ params', args @ args') s)
	\| Call (GKind, g, Var x :: args) ->
	Variants (x, reduce_variants ~program (x, g, args))
	\| Call (GKind, g, (Call _ as t) :: args) -> reduce_inner ~program (t, g, args)
	\| Call (GKind, g, []) -> panic "reduce: no scrutinee for `%s`" g

	and reduce_variants ~program (x, g, args) =
	let unfold_rule (c, (params, params', s)) =
	let fresh_vars = fresh_var_list params in
	let contraction = { c; fresh_vars } in
	let args = List.map var fresh_vars @ unify ~x ~contraction args in
	(contraction, subst_params (params @ params', args) s)
	in
	find_g_rule_list ~program g
	\|> G_rules_by_name.bindings \|> List.map unfold_rule

	and reduce_inner ~program (t, g, args) =
	match reduce ~program t with
	\| Transient t -> Transient (g_call (g, t, args))
	\| Variants (x, variants) ->
	let propagate_contraction (contraction, t) =
	(contraction, g_call (g, t, unify ~x ~contraction args))
	in
	Variants (x, List.map propagate_contraction variants)
	\| _ -> panic "reduce_inner: impossible"

	(******************************************************************************)
	(* The homeomorphic embedding relation. *)

	(* Implements "Fig. 7. Homeomorphic embedding". *)
	let rec decide_he = function
	\| Var _x, Var _y -> true
	\| s, (Call _ as t) -> he_by_diving (s, t) \|\| he_by_coupling (s, t)
	\| Call _, Var _ -> false

	and he_by_diving = function
	\| s, Call (_kind, _h, args) -> List.exists (fun t -> decide_he (s, t)) args
	\| _, _ -> false

	and he_by_coupling = function
	\| Call (kind, h, args), Call (kind', h', args')
	when equal_call_kind kind kind' && h = h' ->
	List.for_all2 (fun s t -> decide_he (s, t)) args args'
	\| _, _ -> false

	(******************************************************************************)
	(* Computing MSG, a "Most Specific Generalization". *)

	let common_functor (g, subst_1, subst_2) =
	subst_1
	\|> scan_subst ~f:(function
	\| x, Call (kind, h, args) ->
	subst_2
	\|> scan_subst ~f:(function
	\| y, Call (kind', h', args')
	when x = y && equal_call_kind kind kind' && h = h' ->
	Some (x, kind, h, args, args')
	\| _ -> None)
	\| _ -> None)
	\|> Option.map (fun (x, kind, h, args, args') ->
	let fresh_vars = fresh_var_list args in
	let common_call = Call (kind, h, List.map var fresh_vars) in
	let new_subst ~args old_subst =
	List.fold_left
	(fun acc (fresh_var, arg) -> Subst.add fresh_var arg acc)
	(Subst.remove x old_subst)
	(List.combine fresh_vars args)
	in
	( subst ~map:(Subst.singleton x common_call) g,
	new_subst ~args subst_1,
	new_subst ~args:args' subst_2 ))

	let common_subst (g, subst_1, subst_2) =
	subst_1
	\|> scan_subst ~f:(fun (x, s) ->
	subst_1
	\|> scan_subst ~f:(fun (y, s') ->
	if
	x != y && equal_term s s'
	&& Option.bind (Subst.find_opt x subst_2) (fun t ->
	Subst.find_opt y subst_2
	\|> Option.map (fun t' -> equal_term t t'))
	\|> Option.value ~default:false
	then Some (x, y)
	else None))
	\|> Option.map (fun (x, y) ->
	let new_subst old_subst = Subst.remove x old_subst in
	( subst ~map:(Subst.singleton x (Var y)) g,
	new_subst subst_1,
	new_subst subst_2 ))

	let step ~rules triple = List.find_map (fun f -> f triple) rules

	(* Exhaustively applies the two rewrite rules. *)
	let rec loop triple =
	match step ~rules:[ common_functor; common_subst ] triple with
	\| Some triple' -> loop triple'
	\| None -> triple

	(* Implements "Fig. 10. Computing most specific generalizations". *)
	let compute_msg (t1, t2) =
	let seed = fresh_id () in
	let g, subst_1, subst_2 =
	(Var seed, Subst.singleton seed t1, Subst.singleton seed t2)
	in
	loop (g, subst_1, subst_2)

	(******************************************************************************)
	(* The supercompilation algorithm itself! *)

	type graph = Step of graph step \| Bind of (string * graph) list * bind_kind
	and bind_kind = Let of graph \| Fold of de_bruijn_idx
	and de_bruijn_idx = int [@@deriving eq, show { with_path = false }]

	(* Implements "Algorithm 7 (positive supercompilation.)". *)
	let supercompile ~program t =
	let rec go ~history n =
	match
	List.find_mapi
	(fun i m -> if decide_he (m, n) then Some (i, m) else None)
	history
	with
	(* We must stop direct unfolding to avoid non-termination. *)
	\| Some (i, m) -> (
	match match_against (m, n) with
	(* [n] is an instance of [m]. *)
	\| Some subst -> fold ~history:(n :: history) ~subst i
	\| None -> (
	let g, _subst_1, subst_2 = compute_msg (m, n) in
	match g with
	(* [m] and [n] are disjoint. *)
	\| Var _x -> split ~history:(n :: history) n
	(* [m] and [n] have a "meaningful" generalization. *)
	\| _ -> generalize ~history:(n :: history) ~subst_2 g))
	(* Everything is good, continue unfolding. *)
	\| None -> Step (step ~history:(n :: history) n)
	and fold ~history ~subst i =
	Bind
	( subst \|> Subst.bindings
	\|> List.map (fun (x, child) -> (x, go ~history child)),
	Fold i )
	and split ~history = function
	\| Call (kind, h, args) ->
	let fresh_vars = fresh_var_list args in
	let t_g = Call (kind, h, List.map var fresh_vars) in
	Bind
	( List.map2 (fun x t -> (x, go ~history t)) fresh_vars args,
	Let (go ~history t_g) )
	\| _ -> panic "split: impossible"
	and generalize ~history ~subst_2 g =
	Bind
	( subst_2 \|> Subst.bindings
	\|> List.map (fun (x, child) -> (x, go ~history child)),
	Let (go ~history g) )
	and step ~history n =
	match reduce ~program n with
	\| Stop x -> Stop x
	\| Decompose (c, args) -> Decompose (c, List.map (go ~history) args)
	\| Transient t -> Transient (go ~history t)
	\| Variants (x, variants) ->
	Variants
	( x,
	List.map
	(fun (contraction, t) -> (contraction, go ~history t))
	variants )
	in
	go ~history:[] t

	(******************************************************************************)
	(* Residual program generation. *)

	module Free_vars = Set.Make (String)

	let union_free_vars list =
	let out_list, free_vars_list = List.split list in
	let free_vars =
	List.fold_left Free_vars.union Free_vars.empty free_vars_list
	in
	(out_list, free_vars)

	(* Invariants:
	- We always arrange function parameters lexicographically. This ensures that
	recursive functions are called with proper argument positions.
	- We generate only recursive f-functions. This means that useless functions
	are "inlined" automatically.
	- When processing a graph node (either [Step] or [Bind]), the history length
	must be the same as in [supercompile].
	*)

	let residuate graph =
	let f_rules, g_rules = (ref F_rules.empty, ref G_rules_by_name.empty) in
	let gen_f ~def_meta:(fresh_f, is_called) ~free_vars t_out =
	if !is_called then (
	(* If the function is called recursively, generate a new definition. *)
	let free_vars_list = Free_vars.elements free_vars in
	f_rules := F_rules.add fresh_f (free_vars_list, t_out) !f_rules;
	(f_call (fresh_f, List.map var free_vars_list), free_vars))
	else
	(* Otherwise, just return the term that would have resulted in the
	function's body. In essence, this performs definition inlining, but
	without generating a definition! *)
	(t_out, free_vars)
	in
	let f_meta () =
	let fresh_f = fresh_id ~counter:f_counter ~prefix:"f" () in
	let is_called = ref false in
	(fresh_f, is_called)
	in
	let rec go ~history = function
	\| Step (Stop x) -> (Var x, Free_vars.singleton x)
	\| Step (Decompose (c, args)) -> go_decompose ~history (c, args)
	\| Step (Transient t) -> go_transient ~history t
	\| Step (Variants (x, variants)) -> go_variants ~history (x, variants)
	\| Bind (bindings, Let t) -> go_bind_let ~history (bindings, t)
	\| Bind (bindings, Fold i) -> go_bind_fold ~history (bindings, i)
	(* Generate an f-function definition that calls a constructor. *)
	and go_decompose ~history (c, args) =
	let def_meta = f_meta () in
	let args_out, free_vars =
	args \|> List.map (go ~history:(`F def_meta :: history)) \|> union_free_vars
	in
	gen_f ~def_meta ~free_vars (ctr_call (c, args_out))
	(* Generate a transient f-function definition. *)
	and go_transient ~history t =
	let def_meta = f_meta () in
	let t_out, free_vars = go ~history:(`F def_meta :: history) t in
	gen_f ~def_meta ~free_vars t_out
	(* Generate a g-function definition that describes the variants. *)
	and go_variants ~history (x, variants) =
	let fresh_g = fresh_id ~counter:g_counter ~prefix:"g" () in
	let variants_out, free_vars =
	variants
	\|> List.map (fun (({ fresh_vars; _ } as contraction), t) ->
	let t_out, free_vars = go ~history:(`G fresh_g :: history) t in
	let free_vars = Free_vars.(diff free_vars (of_list fresh_vars)) in
	((contraction, t_out), free_vars))
	\|> union_free_vars
	in
	let free_vars_list = Free_vars.elements free_vars in
	let rules =
	variants_out
	\|> List.map (fun ({ c; fresh_vars }, t_out) ->
	(c, (fresh_vars, free_vars_list, t_out)))
	\|> G_rules_by_pattern.of_list
	in
	g_rules := G_rules_by_name.add fresh_g rules !g_rules;
	( g_call (fresh_g, Var x, List.map var free_vars_list),
	Free_vars.add x free_vars )
	(* Residuate the bindings and substitute them to the body. *)
	and go_bind_let ~history (bindings, t) =
	let def_meta = f_meta () in
	let bindings_out, free_vars =
	go_bindings ~history:(`F def_meta :: history) bindings
	in
	(* Due to the way how an MSG is computed, [_free_vars'] is the set of fresh
	variables from [bindings_out]. *)
	let t_out, _free_vars' = go ~history:(`F def_meta :: history) t in
	gen_f ~def_meta ~free_vars (subst ~map:(Subst.of_list bindings_out) t_out)
	(* Residuate the bindings and make a recursive function call. *)
	and go_bind_fold ~history (bindings, i) =
	let def_meta = f_meta () in
	let bindings_out, free_vars =
	go_bindings ~history:(`F def_meta :: history) bindings
	in
	let args = List.map (fun (_x, t) -> t) bindings_out in
	let t_out =
	match List.nth history i with
	\| `F (f, is_called) ->
	(* We will generate a definition for this recursive function [f]. *)
	is_called := true;
	f_call (f, args)
	\| `G g -> Call (GKind, g, args)
	in
	gen_f ~def_meta ~free_vars t_out
	and go_bindings ~history bindings =
	bindings
	\|> List.map (fun (x, t) ->
	let t_out, free_vars = go ~history t in
	((x, t_out), free_vars))
	\|> union_free_vars
	in
	let t_out, _free_vars = go ~history:[] graph in
	({ f_rules = !f_rules; g_rules = !g_rules }, t_out)

	(******************************************************************************)
	(* Initial program construction. *)

	let create_program ?(f_rules = []) ?(g_rules = []) () =
	let prepare_f_rule (f, params, t) = (f, (params, t)) in
	let prepare_g_rule_by_name (g, rules) =
	let prepare_g_rule_by_pattern ((c, params), params', t) =
	(c, (params, params', t))
	in
	( g,
	rules \|> List.map prepare_g_rule_by_pattern \|> G_rules_by_pattern.of_list
	)
	in
	{
	f_rules = f_rules \|> List.map prepare_f_rule \|> F_rules.of_list;
	g_rules =
	g_rules \|> List.map prepare_g_rule_by_name \|> G_rules_by_name.of_list;
	}

	(******************************************************************************)
	(* Pretty-printing. *)

	let rec term_to_string = function
	\| Var x -> x
	\| Call (_kind, h, args) ->
	Printf.sprintf "%s(%s)" h
	(String.concat ", " (List.map term_to_string args))

	let print_program { f_rules; g_rules } =
	let go_f_rule (f, params, t) =
	Printf.sprintf "%s(%s) = %s" f
	(String.concat ", " params)
	(term_to_string t)
	in
	let go_g_rule (g, (c, params), params', t) =
	Printf.sprintf "%s(%s(%s)%s%s) = %s" g c
	(String.concat ", " params)
	(if List.is_empty params' then "" else ", ")
	(String.concat ", " params')
	(term_to_string t)
	in
	let f_rules =
	f_rules \|> F_rules.bindings
	\|> List.map (fun (f, (params, t)) -> go_f_rule (f, params, t))
	in
	let g_rules =
	g_rules \|> G_rules_by_name.bindings
	\|> List.map (fun (g, rules) ->
	rules \|> G_rules_by_pattern.bindings
	\|> List.map (fun (c, (params, params', t)) ->
	go_g_rule (g, (c, params), params', t)))
	\|> List.flatten
	in
	f_rules @ g_rules

	(******************************************************************************)
	(* Program optimization. *)

	let optimize ?f_rules ?g_rules t =
	var_counter := 0;
	f_counter := 0;
	g_counter := 0;
	let program = create_program ?f_rules ?g_rules () in
	let program_out, t_out = supercompile ~program t \|> residuate in
	(term_to_string t_out, print_program program_out)