code/ski_evaluator.ml

   1 type term = I | S | K | App of (term * term)
   2
   3 let skomega = App (App (App (S,I), I), App (App (S,I), I))
   4 let test = App (App (K,I), skomega)
   5
   6 let reduce_if_redex (t:term):term = match t with
   7   | App(I,a) -> a
   8   | App(App(K,a),b) -> a
   9   | App(App(App(S,a),b),c) -> App(App(a,c),App(b,c))
  10   | _ -> t
  11
  12 let is_redex (t:term):bool = not (t = reduce_if_redex t)
  13
  14 let rec reduce_try2 (t:term):term = match t with
  15   | I -> I
  16   | K -> K
  17   | S -> S
  18   | App (a, b) ->
  19       let t' = App (reduce_try2 a, reduce_try2 b) in
  20       if (is_redex t') then let t'' = reduce_if_redex t'
  21                             in reduce_try2 t''
  22                        else t'
  23
  24 let rec reduce_lazy (t:term):term = match t with
  25   | I -> I
  26   | K -> K
  27   | S -> S
  28   | App (a, b) ->
  29       let t' = App (reduce_lazy a, b) in
  30       if (is_redex t') then let t'' = reduce_if_redex t'
  31                             in reduce_lazt t''
  32                        else t'