-- Demo code from 1st AFP Agda lecture
module Demo1 where

-- Installation
---------------

-- https://github.com/agda/agda/releases/tag/v2.8.0

-- $PATH

-- banacorn.agda-mode

-- Interactive development
--------------------------

open import Agda.Builtin.Nat

fib : Nat -> Nat
fib zero = 1
fib (suc x) = suc x * fib x

-- C-c C-l    -- Load file
-- C-c C-f    -- Forwards to next hole
-- C-c C-b    -- Back to previous hole
-- C-c C-c    -- Case split
-- C-c C-SPC  -- Give expression to fill hole

-- Testing
----------

f100 = fib 100
-- C-c C-n    -- Normalize

-- Unicode
----------

-- \ - >
-- \ : :

-- Lists
--------

open import Agda.Builtin.List

l1 = 1 ∷ 2 ∷ 3 ∷ []
l2 = 4 ∷ 5 ∷ []

-- Named parameters, polymorphism
---------------------------------

-- append : List Nat → List Nat → List Nat
-- append : (xs : List Nat) → (ys : List Nat) → List Nat
-- append : (A : Set) → (xs : List A) → (ys : List A) → List A
append : {A : Set} → (xs : List A) → (ys : List A) → List A
append [] ys       = ys
append (x ∷ xs) ys = x ∷ append xs ys

-- C-c C-c    -- Introduce function arguments
-- C-c C-.    -- Inspect hole

l3 = append l1 l2

-- Infix operators, helper function extraction
----------------------------------------------

_++_ = append

open import Agda.Builtin.Bool

if_then_else_ : {A : Set} → Bool → A → A → A
if true  then t else _ = t
if false then _ else e = e

infixr 4 if_then_else_

insert : Nat → List Nat → List Nat
insert n []       = n ∷ [] 
insert n (x ∷ xs) =
    if n < x
    then n ∷ x ∷ xs
    else x ∷ insert x xs

sort : List Nat → List Nat
sort [] = []
sort (x ∷ xs) = insert x (sort xs)

-- C-c C-h    -- Helper function type

l4 = sort (5 ∷ 7 ∷ 2 ∷ 3 ∷ 9 ∷ [])

-- FFI pragmas
--------------

postulate
  Unit : Set
  String : Set
  IO : Set -> Set
  putStrLn : String → IO Unit
  _>>_ : IO Unit → IO Unit → IO Unit

{-# BUILTIN STRING String #-}
{-# COMPILE JS putStrLn = str => _ => console.log(str) #-}
{-# COMPILE JS _>>_ = io1 => io2 => _ => (io1({}) , io2({})) #-}

main = do
  putStrLn "hello world"
  putStrLn "goodbye world"

-- agda --js --js-es6 Demo1.agda

-- <script type="module" src="jAgda.Demo1.mjs"></script>

-- python3 -m http.server

-- Libraries
------------

-- git clone https://github.com/lawcho/iepje

-- .agda-lib

-- include: . iepje/src

{-

open import Iepje.Prelude

main : IO ⊤
main = interact "body" 0
  (λ n → button 1 (text $ primShowNat n))
  _+_

-}