Various homeomorphic embedding implementations

a-classic.ml

type term = Call of string * term list

let rec decide_he (s, (Call _ as t)) =
  he_by_diving (s, t) || he_by_coupling (s, t)

and he_by_diving (s, Call (_h', args')) =
  List.exists (fun t -> decide_he (s, t)) args'

and he_by_coupling (Call (h, args), Call (h', args')) =
  if h = h' then List.for_all2 (fun s t -> decide_he (s, t)) args args'
  else false

b-explicit-booleans.ml

type term = Call of string * term list

let rec decide_he ((Call (h, args) as s), Call (h', args')) =
  match dive s args' with
  | `T -> `T
  | `F -> if h <> h' then `F else couple (args, args')

and dive s = function
  | [] -> `F
  | t :: ts -> ( match decide_he (s, t) with `T -> `T | `F -> dive s ts)

and couple = function
  | [], [] -> `T
  | s :: ss, t :: ts -> (
      match decide_he (s, t) with `F -> `F | `T -> couple (ss, ts))
  | _, _ -> invalid_arg "couple"

c-cps.ml

type term = Call of string * term list

let rec decide_he_cps k ((Call (h, args) as s), Call (h', args')) =
  dive_cps
    (function
      | `T -> k `T | `F -> if h <> h' then k `F else couple_cps k (args, args'))
    s args'

and dive_cps k s = function
  | [] -> k `F
  | t :: ts ->
      decide_he_cps (function `T -> k `T | `F -> dive_cps k s ts) (s, t)

and couple_cps k = function
  | [], [] -> k `T
  | s :: ss, t :: ts ->
      decide_he_cps (function `F -> k `F | `T -> couple_cps k (ss, ts)) (s, t)
  | _, _ -> invalid_arg "couple"

d-defunctionalized-cps.ml

type term = Call of string * term list

type cont =
  | Halt
  | DecideHeCont of term * term * cont
  | DiveCont of term * term list * cont
  | CoupleCont of term list * term list * cont

let rec apply (k, b) =
  match k with
  | Halt -> b
  | DecideHeCont (Call (h, args), Call (h', args'), k) -> (
      match b with
      | `T -> apply (k, `T)
      | `F -> if h <> h' then apply (k, `F) else couple_cps k (args, args'))
  | DiveCont (s, ts, k) -> (
      match b with `T -> apply (k, `T) | `F -> dive_cps k s ts)
  | CoupleCont (ss, ts, k) -> (
      match b with `F -> apply (k, `F) | `T -> couple_cps k (ss, ts))

and decide_he_cps k ((Call _ as s), (Call (_h', args') as t)) =
  dive_cps (DecideHeCont (s, t, k)) s args'

and dive_cps k s = function
  | [] -> apply (k, `F)
  | t :: ts -> decide_he_cps (DiveCont (s, ts, k)) (s, t)

and couple_cps k = function
  | [], [] -> apply (k, `T)
  | s :: ss, t :: ts -> decide_he_cps (CoupleCont (ss, ts, k)) (s, t)
  | _, _ -> invalid_arg "couple"

e-separate-continuations.ml

type term = Call of string * term list

let rec decide_he_cps k1 k2 ((Call (h, args) as s), Call (h', args')) =
  dive_cps k1
    (fun () -> if h <> h' then k2 () else couple_cps k1 k2 (args, args'))
    s args'

and dive_cps k1 k2 s = function
  | [] -> k2 ()
  | t :: ts -> decide_he_cps k1 (fun () -> dive_cps k1 k2 s ts) (s, t)

and couple_cps k1 k2 = function
  | [], [] -> k1 ()
  | s :: ss, t :: ts ->
      decide_he_cps (fun () -> couple_cps k1 k2 (ss, ts)) k2 (s, t)
  | _, _ -> invalid_arg "couple"

f-homeo.pot

main = decideHe s t;

decideHe s t = case s of
    Call(h, args) -> (case t of
        Call(h', args') -> (case dive s args' of
            T -> T
          | F -> (case equalSymbols h h' of
                T -> couple args args'
              | F -> F)));

dive s args' = case args' of
    Nil -> F
  | Cons(t, ts) -> (case decideHe s t of
        T -> T
      | F -> dive s ts);

couple args args' = case args of
    Nil -> (case args' of
        Nil -> T
      | Cons(t, ts) -> F)
  | Cons(s, ss) -> (case args' of
        Nil -> F
      | Cons(t, ts) -> case decideHe s t of
            T -> couple ss ts
          | F -> F);

equalSymbols h h' = case h of
    A -> (case h' of
        A -> T
      | B -> F
      | C -> F)
  | B -> (case h' of
        A -> F
      | B -> T
      | C -> F)
  | C -> (case h' of
        A -> F
      | B -> F
      | C -> T)

g-deforested.pot

main = f s t;

-- <https://github.com/poitin/Higher-Order-Deforester>

f s t = case s of
           Call(h,args) -> case t of
                              Call(h1,args1) -> case args1 of
                                                   Nil -> case (case h of
                                                                   A -> case h1 of
                                                                           A -> T
                                                                         | B -> F
                                                                         | C -> F
                                                                 | B -> case h1 of
                                                                           A -> F
                                                                         | B -> T
                                                                         | C -> F
                                                                 | C -> case h1 of
                                                                           A -> F
                                                                         | B -> F
                                                                         | C -> T) of
                                                             T -> f2 args args1
                                                           | F -> F
                                                 | Cons(t,ts) -> case (f s t) of
                                                                    T -> T
                                                                  | F -> case (f6 s ts) of
                                                                            T -> T
                                                                          | F -> case (case h of
                                                                                          A -> case h1 of
                                                                                                  A -> T
                                                                                                | B -> F
                                                                                                | C -> F
                                                                                        | B -> case h1 of
                                                                                                  A -> F
                                                                                                | B -> T
                                                                                                | C -> F
                                                                                        | C -> case h1 of
                                                                                                  A -> F
                                                                                                | B -> F
                                                                                                | C -> T) of
                                                                                    T -> f2 args args1
                                                                                  | F -> F;
f6 s ts = case ts of
             Nil -> F
           | Cons(t,ts) -> case (f s t) of
                              T -> T
                            | F -> f6 s ts;
f2 args args1 = case args of
                   Nil -> case args1 of
                             Nil -> T
                           | Cons(t,ts) -> F
                 | Cons(s,ss) -> case args1 of
                                    Nil -> F
                                  | Cons(t,ts) -> case (f s t) of
                                                     T -> f2 ss ts
                                                   | F -> F