juvix/tests/positive/MiniC/PolymorphismHoles/Input.juvix

module Input;

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

type 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";


--------------------------------------------------------------------------------
-- Pair
--------------------------------------------------------------------------------

type Pair (A : Type) (B : Type) :=
 mkPair : A → B → Pair A B;

fst : {A : Type} → {B : Type} → Pair A B → A;
fst (mkPair a b) := a;

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

fst-of-pair : Action;
fst-of-pair := (put-str "fst (True, False) = ")
               >> put-str-ln (bool-to-str (fst (mkPair true false)));

main : Action;
main := fst-of-pair;

end;