module Input;

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

inductive Bool {
  true : Bool;
  false : Bool;
};

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

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
--------------------------------------------------------------------------------

inductive 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;