code/ski_evaluator.ml

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