Week 28 - 2023

/home/ping/.cabal/bin/agda-2.6.4 --js --js-optimize --compile-dir=example4 Example4.agda
NODE_PATH=/home/ping/dev/iota/compiler/example4 browserify --bare -p tinyify -e example4/jAgda.Example4.js | uglifyjs > app.js
java -jar cc.jar --compilation_level ADVANCED example4.js --js_output_file example4_2.js

private
  variable
    l l2 l3 : Level
    A : Set l
    B : Set l2
    C : Set l3
    n : Nat
    m : Nat

_$_ : (A -> B) -> A -> B
f $ x = f x
infixr 0 _$_

Tuple : Nat -> Set
Tuple 0 = Unit
Tuple 1 = Int
Tuple (2+ n) = Pair Int (Tuple (1+ n))

NArgs : Nat -> Set l -> Set l
NArgs 0 A = A
NArgs (1+ n) A = Int -> NArgs n A

packArgs : (Vec Int n -> A) -> NArgs n A
packArgs {0} f = f []
packArgs {1+ n} f x = packArgs {n} \l -> f (x :: l)

applyTuple : NArgs n A -> Tuple n -> A
applyTuple {0} f unit = f
applyTuple {1} f x = f x
applyTuple {2+ n} f (x , l) = applyTuple {1+ n} (f x) l

IArgs : (Vec Int n -> Set l) -> Set l
IArgs {0} f = f []
IArgs {1+ n} f = {x : Int} -> IArgs {n} \v -> f (x :: v)

unpackResult : Vec Int n -> Tuple n
unpackResult [] = unit
unpackResult (x :: []) = x
unpackResult (x :: l@(_ :: _)) = (x , unpackResult l)

data Op : Nat -> Nat -> Set where
  fin : Op m m
  push : Int -> Op (1+ n) m -> Op n m
  copy : Fin n -> Op (1+ n) m -> Op n m
  swap : Op (2+ n) m -> Op (2+ n) m
  pop : Op (1+ n) m -> Op (2+ n) m
  add : Op (1+ n) m -> Op (2+ n) m
  sub : Op (1+ n) m -> Op (2+ n) m
  mul : Op (1+ n) m -> Op (2+ n) m
  neg : Op (1+ n) m -> Op (1+ n) m

run' : {n m : Nat} -> Op n m -> Vec Int n -> Vec Int m
run' fin s = s
run' (push x next) s = run' next (x :: s)
run' (copy i next) s = run' next (vecIndex s i :: s)
run' (swap next) (y :: x :: s) = run' next (x :: y :: s)
run' (pop next) (x :: s) = run' next s
run' (add next) (y :: x :: s) = run' next ((x + y) :: s)
run' (sub next) (y :: x :: s) = run' next ((x - y) :: s)
run' (mul next) (y :: x :: s) = run' next ((x * y) :: s)
run' (neg next) (x :: s) = run' next ((- x) :: s)

run : Op n m -> NArgs n (Tuple m)
run op = packArgs \a -> unpackResult (run' op a)

2n+1Op : Op 1 1
2n+1Op = push [ 2 ] $ swap $ mul $ push [ 1 ] $ add fin

2n+1 : Int -> Int
2n+1 = run 2n+1Op

2n+1-equal : (n : Int) -> 2n+1 n === [ 2 ] * n + [ 1 ]
2n+1-equal n = refl

op2JS' : Op n m -> String
op2JS' {0} fin = ""
op2JS' {1} fin = "return x1"
op2JS' {1+ n} fin = "return " + retStr n + "];" where
  retStr : Nat -> String
  retStr 0 = "x1"
  retStr (1+ n) = "[x" + [ 1+ n ] + "," + retStr n + "]"
op2JS' {n} (push x next) = "x" + [ (1+ n) ] + "=" + [ x ] + "n;" + op2JS' next
op2JS' {n} (copy i next) = "x" + [ n ] + "=x" + [ n - [ i ] ] + ";" + op2JS' next
op2JS' n@{1+ m} (swap next) = "[x" + [ m ] + ",x" + [ n ] + "]=[x" + [ n ] + ",x" + [ m ] + "];" + op2JS' next
op2JS' {n} (pop next) = op2JS' next
op2JS' n@{1+ m} (add next) = "x" + [ m ] + "+=x" + [ n ] + ";" + op2JS' next
op2JS' n@{1+ m} (sub next) = "x" + [ m ] + "-=x" + [ n ] + ";" + op2JS' next
op2JS' n@{1+ m} (mul next) = "x" + [ m ] + "*=x" + [ n ] + ";" + op2JS' next
op2JS' {n} (neg next) = "x" + [ n ] + "=-x" + [ n ] + ";" + op2JS' next

op2JS : Op n m -> String
op2JS {_} {0} fin = "z_jAgda_Agda_Primitive[\"unit\"]"
op2JS {n} {m} op = argStr n + " => {" + op2JS' op + "}" where
  argStr : Nat -> String
  argStr 0 = "()"
  argStr 1 = "x1"
  argStr (2+ n) = argStr (1+ n) + " => x" + (2+ n as String)

postulate
  eval : String -> A

{-# COMPILE JS eval = _ => _ => eval #-}

runJS : Op n m -> NArgs n (Tuple m)
runJS {n} {m} op = eval (op2JS {n} {m} op)