Nondeterministic substitution by matrix transposition

transpose-args.ml

type term = Var of string | Call of string * term array
[@@deriving show { with_path = false }]

type possibilities = term array [@@deriving show]

let demux ~(x : string) ~(values : term array) : term -> possibilities =
  let rec go = function
    | Var y when x = y -> values
    | Var _ as t -> Array.map (fun _ -> t) values
    | Call (op, args) ->
        let matrix =
          Array.(
            init (length values) (fun _i ->
                Call (op, make (length args) (Var "?"))))
        in
        (* Transpose the nondeterministic matrix. *)
        for i = 0 to Array.length args - 1 do
          let values = go args.(i) in
          for j = 0 to Array.length values - 1 do
            let[@warning "-8"] (Call (_op, args)) = matrix.(j) in
            args.(i) <- values.(j)
          done
        done;
        matrix
  in
  go

(* [|(Call ("f", [|(Var "a"); (Call ("g", [|(Var "y"); (Var "z")|]))|]));
     (Call ("f", [|(Var "b"); (Call ("g", [|(Var "y"); (Var "z")|]))|]));
     (Call ("f", [|(Var "c"); (Call ("g", [|(Var "y"); (Var "z")|]))|]))|] *)
let () =
  let t = Call ("f", [| Var "x"; Call ("g", [| Var "y"; Var "z" |]) |]) in
  t
  |> demux ~x:"x" ~values:[| Var "a"; Var "b"; Var "c" |]
  |> show_possibilities |> print_endline