code/ski_evaluator.hs

   1 data Term = I | S | K | FA Term Term deriving (Eq, Show)
   2
   3 skomega = (FA (FA (FA S I) I) (FA (FA S I) I))
   4 test = (FA (FA K I) skomega)
   5
   6 reduce_one_step :: Term -> Term
   7 reduce_one_step t = case t of
   8   FA I a -> a
   9   FA (FA K a) b -> a
  10   FA (FA (FA S a) b) c -> FA (FA a c) (FA b c)
  11   _ -> t
  12
  13 is_redex :: Term -> Bool
  14 is_redex t = not (t == reduce_one_step t)
  15
  16 reduce :: Term -> Term
  17 reduce t = case t of
  18   I -> I
  19   K -> K
  20   S -> S
  21   FA a b ->
  22     let t' = FA (reduce a) (reduce b) in
  23       if (is_redex t') then reduce (reduce_one_step t')
  24                        else t'