/-
  Ok, so this is newt, a dependent typed programming language that
  I am implementing to learn how they work.  It targets javascript
  and borrows a lot of syntax from Idris and Agda.

  This page is a very simple web playground based on the monaco editor.
  It runs newt, compiled by Idris2, in a web worker.

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

  The output, to the right, is somewhat noisy and obtuse. You'll see
  INFO and sometimes ERROR messages that show up in the editor view
  on hover.  I'm emitting INFO for solved metas.

  The Day1.newt and Day2.newt are last year's advent of code, translated
  from Lean.

-/

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

-- commented out until we preload other files into the worker
-- import Lib

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

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

-- 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 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 _≡_ : {A : U} -> A -> A -> U where
  Refl : {A : U} {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)

-- and it now finds the implicits, you'll see the solutions to the
-- implicits if you hover over the `+`.
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.  Dead code elimination will be done if there is a `main` function.
-- That is not the case in this file.

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

ptype Int : U
ptype String : U
ptype Char : U

-- The names of these three types 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} {{Monad m}} {a b} -> m a -> (a -> m b) -> m b
_>>=_ ma amb = bind ma amb

_>>_ :  {m} {{Monad m}} {a b} -> 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)