CompileNumbers.out 1.6 KB

12345678910111213141516171819202122232425262728293031323334353637383940414243444546474849505152
  1. EXECUTED_PROGRAM
  2. ret > ExitSuccess
  3. out > CompileNumbers.match-on-lit =
  4. out > λ a b →
  5. out > case a of
  6. out > "neg" → 0 - b
  7. out > _ → b
  8. out > CompileNumbers.match-on-lit₂ =
  9. out > λ a b →
  10. out > case a of
  11. out > "neg" → 0 - b
  12. out > _ → b
  13. out > CompileNumbers.nested-match =
  14. out > λ a →
  15. out > case a of
  16. out > 0 → "zero"
  17. out > 1 → "one"
  18. out > _ | a >= 2 → "lots"
  19. out > -1 → "minus one"
  20. out > -2 → "minus two"
  21. out > _ → "minus lots"
  22. out > CompileNumbers.compareNat =
  23. out > λ a b →
  24. out > let c = a < b in
  25. out > case c of
  26. out > Agda.Builtin.Bool.Bool.false →
  27. out > let d = b < a in
  28. out > case d of
  29. out > Agda.Builtin.Bool.Bool.false → CompileNumbers.Diff.equal
  30. out > Agda.Builtin.Bool.Bool.true →
  31. out > CompileNumbers.Diff.greater (a - b - 1)
  32. out > Agda.Builtin.Bool.Bool.true → CompileNumbers.Diff.less (b - a - 1)
  33. out > CompileNumbers.neg = λ a → 0 - a
  34. out > CompileNumbers._-N_ = λ a b → a - b
  35. out > CompileNumbers._+Z_ = λ a b → a + b
  36. out > CompileNumbers._*Z_ = λ a b → a * b
  37. out > CompileNumbers.printInt =
  38. out > λ a → Common.IO.putStrLn (Common.String.intToString a)
  39. out > CompileNumbers.main =
  40. out > Common.IO.then
  41. out > () () _ _
  42. out > (CompileNumbers.printInt (CompileNumbers.match-on-lit "neg" 42))
  43. out > (Common.IO.then
  44. out > () () _ _
  45. out > (CompileNumbers.printInt (CompileNumbers.match-on-lit₂ "neg" 42))
  46. out > (Common.IO.putStrLn (CompileNumbers.nested-match -6)))
  47. out > -42
  48. out > -42
  49. out > minus lots
  50. out >