tak18.str 1.52 KB
Newer Older
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47
module tak18

imports libstrategolib

signature

sorts
   Bool Nat Int

constructors
   true : Bool 
   false : Bool 
   d0 : Nat 
   s : Nat -> Nat 
   Pos : Nat -> Int 
   Neg : Nat -> Int 
   gte : Nat * Nat -> Bool 
   gte_Int : Int * Int -> Bool 
   pred : Int -> Int 
   succ : Int -> Int 
   tak : Int * Int * Int -> Int 

rules
   REC_E: gte (d0(), d0()) -> true()
   REC_E: gte (s (X), d0()) -> true()
   REC_E: gte (d0(), s (X)) -> false()
   REC_E: gte (s (X), s (Y)) -> gte (X, Y)
   REC_E: gte_Int (Pos (X), Pos (Y)) -> gte (X,Y)
   REC_E: gte_Int (Neg (X), Neg (Y)) -> gte (Y,X)
   REC_E: gte_Int (Pos (X), Neg (Y)) -> true()
   REC_E: gte_Int (Neg (X), Pos (Y)) -> false()
   REC_E: pred (Pos (d0())) -> Neg (d0())
   REC_E: pred (Pos (s (X))) -> Pos (X)
   REC_E: pred (Neg (X)) -> Neg (s (X))
   REC_E: succ (Neg (d0())) -> Pos (d0())
   REC_E: succ (Neg (s (X))) -> Neg (X)
   REC_E: succ (Pos (X)) -> Pos (s (X))
   REC_E: tak (I, J, K) -> K where equal-after-eval (|gte_Int (J, I), true())
   REC_E: tak (I, J, K) -> tak (tak (pred (I), J, K), tak (pred (J), K, I), tak (pred (K), I, J)) where equal-after-eval (|gte_Int (J, I), false())

strategies
   eval = memo (innermost (REC_E))
   equal-after-eval (|m1, m2) = equal (|<eval> m1, <eval> m2)
   eval-and-print = eval ; debug (!"result = ")
   main = 
      (<eval-and-print> tak (Pos (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (d0()))))))))))))))))))), Pos (s (s (s (s (s (s (s (s (s (s (s (s (d0()))))))))))))), Pos (s (s (s (s (s (s (d0()))))))))) ;
      <exit> 0