juvix/tests/positive/MiniC/Nat/Input.juvix

module Input;

--------------------------------------------------------------------------------
-- Booleans
--------------------------------------------------------------------------------

type Bool :=
     true : Bool
  | false : Bool;

--------------------------------------------------------------------------------
-- Strings
--------------------------------------------------------------------------------

builtin string axiom String : Type;

compile String {
  ghc ↦ "[Char]";
  c ↦ "char*";
};

--------------------------------------------------------------------------------
-- IO
--------------------------------------------------------------------------------

axiom Action : Type;

compile Action {
  ghc ↦ "IO ()";
  c ↦ "int";
};

foreign c {
  int sequence(int a, int b) {
    return a + b;
  \}
};

infixl 1 >>;
axiom >> : Action → Action → Action;

compile >> {
  ghc ↦ "(>>)";
  c ↦ "sequence";
};

axiom put-str : String → Action;

compile put-str {
  ghc ↦ "putStr";
  c ↦ "putStr";
};

axiom put-str-ln : String → Action;

compile put-str-ln {
  ghc ↦ "putStrLn";
  c ↦ "putStrLn";
};

bool-to-str : Bool → String;
bool-to-str true := "True";
bool-to-str false := "False";

--------------------------------------------------------------------------------
-- Integers
--------------------------------------------------------------------------------

axiom Int : Type;
compile Int {
  ghc ↦ "Int";
  c ↦ "int";
};

axiom Int_0 : Int;
compile Int_0 {
  c ↦ "0";
};

axiom Int_1 : Int;
compile Int_1 {
  c ↦ "1";
};

foreign c {
  int plus(int l, int r) {
    return l + r;
  \}
};

infixl 6 +int;
axiom +int : Int -> Int -> Int;

compile +int {
  ghc ↦ "(+)";
  c ↦ "plus";
};

axiom to-str : Int → String;

compile to-str {
  ghc ↦ "show";
  c ↦ "intToStr";
};

--------------------------------------------------------------------------------
-- Natural Numbers
--------------------------------------------------------------------------------

type Nat :=
  zero : Nat
  | suc : Nat → Nat;

infixl 6 +;
+ : Nat → Nat → Nat;
+ zero n := n;
+ (suc m) n := suc (m + n);

is-even : Nat → Bool;
is-even zero := true;
is-even (suc (suc n)) := is-even n;
is-even _ := false;

infix 4 ==Nat;
==Nat : Nat → Nat → Bool;
==Nat zero zero := true;
==Nat (suc n) (suc m) := n ==Nat m;
==Nat _ _ := false;

to-int : Nat → Int;
to-int zero := Int_0;
to-int (suc n) := Int_1 +int (to-int n);

nat-to-str : Nat → String;
nat-to-str n := to-str (to-int n);

one : Nat;
one := suc zero;

two : Nat;
two := suc one;

three : Nat;
three := suc two;

--------------------------------------------------------------------------------
-- Main
--------------------------------------------------------------------------------

three-plus-suc-one : Action;
three-plus-suc-one := (put-str "3 + (1 + 1) = ")
                      >> put-str-ln (nat-to-str (three + (suc one)));

three-eq-suc-two : Action;
three-eq-suc-two := (put-str "3 == 1 + 2 : ")
                    >> put-str-ln (bool-to-str (three ==Nat (one + two)));

three-neq-two : Action;
three-neq-two := (put-str "3 == 2 : ")
                 >> put-str-ln (bool-to-str (three ==Nat two));

three-is-not-even : Action;
three-is-not-even := (put-str "is-even 3 : ")
                 >> put-str-ln (bool-to-str (is-even three));

four-is-even : Action;
four-is-even := (put-str "is-even 4 : ")
                 >> put-str-ln (bool-to-str (is-even (suc three)));

main : Action;
main := three-plus-suc-one
   >> three-eq-suc-two
   >> three-neq-two
   >> three-is-not-even
   >> four-is-even

end;