/-
  This is newt, 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 a flat namespace and no cycles,
-- diamonds are ok, Prelude is not imported by default, only explicitly
-- imported modules are in scope

-- commented out because we redefine parts of Prelude in this file.
-- import Prelude

-- We're calling the universe U and are doing type in type for now

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

-- Nat-shaped data is turned into numbers in codegen.

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

-- Enum shaped data becomes a bare string (the constructor name) in codegen.

-- 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 plusInt : Int -> Int -> Int := `(x,y) => x + y`
pfunc plusString : String -> String -> String := `(x,y) => x + y`

-- We can make them Plus instances:

instance Add Int where
  _+_ = plusInt

instance Add String where
  _+_ = plusString

concat : String -> String -> String
concat a b = a + b

-- 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. At the moment, I don't
-- have sugar for Lists,

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

infixr 7 _++_
_++_ : ∀ a.  List a -> List a -> List a
Nil ++ ys = ys
(x :: xs) ++ ys = x :: (xs ++ ys)

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

/-
This desugars to: (the names in guillemots are not user-accessible)

«Monad List,pure» : { a : U } -> a:0 -> List a:1
pure a = _::_ a Nil

«Monad List,bind» : { a : U } -> { b : U } -> (List a) -> (a -> List b) -> List b
bind Nil f = Nil bind (_::_ x xs) f = _++_ (f x) (bind xs f)

«Monad List» : Monad List
«Monad List» = MkMonad «Monad List,pure» «Monad List,bind»

-/

-- We'll want Pair below.  `,` has been left for use as an operator.
-- Also we see that → 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)


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 Prelude_MkIORes(null,Prelude_MkUnit,w)
}`

main : IO Unit
main = putStrLn "Hello, World!"