Test3.spad

)abbrev domain TEST3 Test3
Test3() : Exports == Implementation where
  NNI ==> NonNegativeInteger

  Exports ==> with
    id1 : PositiveInteger -> PositiveInteger
    id2 : PositiveInteger -> Integer 
    hello1 : () -> Void
    hello2 : () -> Void
    foobar : Integer -> Integer
    baz : Integer -> String
    barf : Integer -> NNI

  Implementation ==> add
    import Integer
    import NonNegativeInteger
    import OutputForm
    import PositiveInteger

    -- [OK] Type checker removes coercion to PositiveInteger.
    id1 x == x :: PositiveInteger
    id2 x == x :: Integer

    hello1() ==
      print((0@Integer)::OutputForm)

    hello2() ==
      print(coerce(0@Integer)@OutputForm)

    -- [OK] Support for %any type.
    foobar x ==
      x < 0 => error "Cannot accept negative integer!"
      x

    baz x ==
      error "Not implemented!"

    barf a ==
      while true repeat
        -- FriCAS will complain about return statement if following expression
        -- is at function top level, so let's cheat a bit
        if a > 0 then
          return (a :: NNI)
        else
          return ((-a) :: NNI)