/-
  Newt is a self-hosted, dependent typed programming language that
  compiles to javascript and borrows a lot of syntax from Idris and Agda.

  This page is a very simple web playground based on the codemirror editor.
  It runs newt in a web worker.

  Block comments follow Lean because they're easier to type on a
  US keyboard.

-/

-- One-line comments begin with two hyphens

-- every file begins with a `module` declaration
-- it must match the filename
module Tour

-- We can import other modules with no cycles, diamonds are ok, cycles
-- are an error. Prelude is not imported by default. Only explicitly
-- imported modules are in scope. Duplicate names are not allowed.

-- Example import is commented out because we redefine Prelude
-- functions below.

/-

import Prelude

-/


-- The universe is U and are doing type in type for now.

-- INDUCTIVE TYPES

-- Inductive type definitions are similar to Idris, Agda, or Haskell
data Nat : U where
  Z : Nat
  S : Nat -> Nat

-- Like in Idris, Nat-shaped data is turned into numbers at runtime.
-- We are not yet ignoring erased fields though.

-- Multiple names are allowed on the left:
data Bool : U where
  True False : Bool

-- There also is an abbreviated syntactic sugar for simple types:

data Tree a = Node a (Tree a) (Tree a) | Leaf

-- Enum shaped data becomes a number at runtime (the constructor tag).

data Answer = Yes | No | Maybe

-- FUNCTIONS

-- function definitions are equations using dependent pattern matching
plus : Nat -> Nat -> Nat
plus Z m = m
plus (S n) m = S (plus n m)

-- we can also have case statements on the right side
-- the core language includes case statements
-- here `\` is used for a lambda expression:
plus' : Nat -> Nat -> Nat
plus' = \ n m => case n of
    Z => m
    S n => S (plus' n m)

-- We can define operators. Mixfix is supported, but we don't
-- allow ambiguity (so you can't have both [_] and [_,_]). See
-- the Reasoning.newt sample file for a mixfix example.
infixl 2 _≡_

-- Here is an equality, like Idris, everything goes to the right of the colon
-- Implicits are denoted with braces `{ }`
-- unlike idris, you have to declare all of your implicits
data _≡_ : {0 A : U} -> A -> A -> U where
  Refl : {0 A : U} {0 a : A} -> a ≡ a

-- And now the compiler can verify that 1 + 1 = 2
test : plus (S Z) (S Z) ≡ S (S Z)
test = Refl

-- Ok now we do typeclasses. `class` and `instance` are sugar for
-- ordinary data and functions:

-- Let's say we want a generic `_+_` operator
infixl 7 _+_

class Add a where
  _+_ : a -> a -> a

instance Add Nat where
  Z + m = m
  (S n) + m = S (n + m)

two : Nat
two = S Z + S Z

-- We can leave a hole in an expression with ? and the editor will show us the
-- scope and expected type (hover to see)
foo : Nat -> Nat -> Nat
foo a b = ?

-- Newt compiles to javascript, there is a tab to the right that shows the
-- javascript output. There is some erasure, but inlining is not being done
-- yet.

-- We can define native types, if the type is left off, it defaults to U

ptype SomePrimType : U

-- The types Int, String, Char are special. Primitive numbers, strings,
-- and characters inhabit them, respectively. We can match on primitives, but
-- must provide a default case:

isVowel : Char -> Bool
isVowel 'a' = True
isVowel 'e' = True
isVowel 'i' = True
isVowel 'o' = True
isVowel 'u' = True
isVowel _ = False

-- And primitive functions have a type and a javascript definition:

pfunc addInt : Int -> Int -> Int := `(x,y) => x + y`
pfunc addString : String -> String -> String := `(x,y) => x + y`


instance Add Int where
  _+_ = addInt


infixr 7 _++_
class Concat a where
  _++_ : a → a → a

instance Concat String where
  _++_ = addString



-- Now we define Monad
class Monad (m : U -> U) where
  pure : ∀ a. a -> m a
  bind : ∀ a b. m a -> (a -> m b) -> m b

/-
This desugars to:

data Monad : (m : U -> U) -> U where
  MkMonad : {m : U -> U} ->
            (pure : {a : _} -> a -> m a) ->
            (bind : {a : _} -> {b : _} -> m a -> a -> m b -> m b) ->
            Monad m

pure : {m : U -> U} -> {{_ : Monad m}} -> {a : _} -> a -> m a
pure {m} {{MkMonad pure bind}} = pure

bind : {m : U -> U} -> {{_ : Monad m}} -> {a : _} -> {b : _} -> m a -> a -> m b -> m b
bind {m} {{MkMonad pure bind}} = bind

-/

-- we can declare multiple infix operators at once
infixl 1 _>>=_ _>>_

_>>=_ : ∀ m a b. {{Monad m}} -> m a -> (a -> m b) -> m b
_>>=_ ma amb = bind ma amb

_>>_ :  ∀ m a b. {{Monad m}} -> m a -> m b -> m b
ma >> mb = ma >>= (λ _ => mb)

-- Now we define list and show it is a monad.

infixr 3 _::_
data List : U -> U where
  Nil : ∀ A.  List A
  _::_ : ∀ A. A -> List A -> List A

instance Monad List where
  pure a = a :: Nil
  bind Nil f = Nil
  bind (x :: xs) f = f x ++ bind xs f

-- and has the _++_ operator

instance ∀ a. Concat (List a) where
  Nil ++ ys = ys
  (x :: xs) ++ ys = x :: (xs ++ ys)

-- A utility function used in generating Show instances below:

joinBy : String → List String → String
joinBy _ Nil = ""
joinBy _ (x :: Nil) = x
joinBy s (x :: y :: xs) = joinBy s ((x ++ s ++ y) :: xs)

-- We define a product of two types (→ can be used in lieu of ->)
infixr 1 _,_ _×_
data _×_ : U → U → U where
  _,_ : ∀ A B. A → B → A × B

-- The _>>=_ operator is used for desugaring do blocks

prod : ∀ A B. List A → List B → List (A × B)
prod xs ys = do
  x <- xs
  y <- ys
  pure (x, y)

-- The prelude defines Eq and Show, which can be derived

infixl 6 _==_
class Eq a where
  _==_ : a → a → Bool

derive Eq Nat

class Show a where
  show : a → String

derive Show Nat

data Unit = MkUnit

ptype World

data IORes a = MkIORes a World

IO : U -> U
IO a = World -> IORes a

instance Monad IO where
  bind ma mab = \ w => case ma w of
    MkIORes a w => mab a w
  pure = MkIORes

pfunc putStrLn uses (MkIORes MkUnit) : String -> IO Unit := `(s) => (w) => {
  console.log(s)
  return Tour_MkIORes(Tour_MkUnit, w)
}`

main : IO Unit
main = do
  putStrLn "Hello, World!"
  putStrLn $ show (S (S Z))