subst.ml

open Printf

type term = F of string * (term list) | V of string

let rec subst term ((name, replacement) as sub) =
  match term, name with 
  | V x, V y when String.equal x y -> replacement
  | V x, V y when not (String.equal x y) -> term
  | F (x, args), V y -> F (x, List.map (fun arg -> subst arg sub) args)
  | _, _ -> assert false

let rec subcompose term sublist = 
  List.fold_left (fun term sub -> subst term sub) term sublist

let rec pp_term = function
  | V x -> x 
  | F (s, []) -> s
  | F (s, l) -> 
    let rec join = function
      | [] -> ""
      | hd :: tl -> sprintf "%s,%s" (pp_term hd) (join tl) in
    sprintf "%s(%s)" s (join l)

let p t = pp_term t |> print_endline

let (.%{}) term sub = subst term sub
let (.%{;..}) term sub = subcompose term (Array.to_list sub)
let (-->) a b = (V a, b)

let () =
  let term = F ("f", [V "x"; V "y"])in
  assert (term.%{"w" --> V "w"} = term);
  term.%{"x" --> V "y"} |> p;
  term.%{"x" --> V "y"; "y" --> V "x"} |> p;
  term.%{("x" --> V "y")}.%{"y" --> V "x"} |> p