added code
[lambda.git] / 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'