js.agda

module _ where

open import Core.Set
open import Core.Bool
open import Core.Nat
open import Core.Fin
open import Core.Int
open import Core.List
open import Core.String
open import Core.Vec
open import Core.Operators
open import Core.Pair
open import Core.Unit
open import Core.Equality

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

-- Type for a tuple of n Ints.
-- ex: Tuple 3 = Int * Int * Int
Tuple : Nat -> Set
Tuple 0 = Unit
Tuple 1 = Int
Tuple (2+ n) = Int * Tuple (1+ n)

-- Type of a function that take n Ints and return an A.
-- ex: NArgs 3 A = Int -> Int -> Int -> A
NArgs : Nat -> Set l -> Set l
NArgs 0 A = A
NArgs (1+ n) A = Int -> NArgs n A

-- Returns a function that takes n Ints and maps it with f.
-- ex: packArgs {3} (foldr _+_ 0) = \a \b \c -> a + b + c
packArgs : (Vec Int n -> A) -> NArgs n A
packArgs {0} f = f []
packArgs {1+ n} f x = packArgs {n} \l -> f (x :: l)

-- Applies tuple to a function accepting multiple arguments.
-- ex: applyTuple f (x , y , z) = f x y z
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

-- Applies a vector to a function accepting multiple arguments.
-- ex: applyVec f [ x , y , z ] = f x y z
applyVec : NArgs n A -> Vec Int n -> A
applyVec f [] = f
applyVec f (x :: l) = applyVec (f x) l

-- Type of a function that takes n implicit arguments and returns a type that depends on those arguments.
-- ex: IArgs 3 (\v -> A) = {x : Int} {y : Int} {z : Int} -> A
IArgs : (Vec Int n -> Set l) -> Set l
IArgs {0} f = f []
IArgs {1+ n} f = {x : Int} -> IArgs {n} \v -> f (x :: v)

-- Turns a vector into a tuple.
-- ex: vec2tuple [ x , y , z ] = (x , y , z)
vec2tuple : Vec Int n -> Tuple n
vec2tuple [] = unit
vec2tuple (x :: []) = x
vec2tuple (x :: l@(_ :: _)) = (x , vec2tuple l)

-- Turns a tuple into a vector.
-- ex: tuple2Vec (x , y , z) = [ x , y , z ]
tuple2Vec : Tuple n -> Vec Int n
tuple2Vec {0} unit = []
tuple2Vec {1} x = x :: []
tuple2Vec {2+ _} (x , l) = x :: tuple2Vec l

-- A program in the stack machine, which always ends with fin.
-- 
-- An `Op n m` starts with n elements in the stack and ends with m elements in the stack,
-- these constructors are constrained to ensure the size of the stack is known at compile time.
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

-- Actual interpreter.
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)

-- Wrapper for run' that turns programs into functions that take arguments and return a tuple.
run : Op n m -> NArgs n (Tuple m)
run op = packArgs \a -> vec2tuple (run' op a)

-- A basic program that takes 2 arguments and returns their sum plus one.
2n+1Op : Op 1 1
2n+1Op = push [ 2 ] $ swap $ mul $ push [ 1 ] $ add fin

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

-- Trivial proof that 2n+1 is the same as 2 * n + 1.
2n+1-equal : (n : Int) -> 2n+1 n === [ 2 ] * n + [ 1 ]
2n+1-equal n = refl

-- Translates a program into a JavaScript function body.
op2JS' : Op n m -> String
op2JS' {0} fin = ""
op2JS' {1} fin = "return x1"
op2JS' {1+ n} fin = "return " + retStr 1 n + ";" where
  retStr : Nat -> Nat -> String
  retStr n 0 = "x" + [ n ]
  retStr n (1+ m) = "[x" + [ n ] + "," + retStr (1+ n) m + "]"
op2JS' {n} (push x next) = "x" + [ (1+ n) ] + "=" + [ x ] + "n;" + op2JS' next
op2JS' {n} (copy i next) = "x" + [ (1+ 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)

-- Cheat in an eval function.
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)

2n+1JS : Int -> Int
2n+1JS = runJS 2n+1Op

-- Assume that runJS is the same as run.
postulate
  run=runJS : (op : Op n m) -> IArgs {n} \v -> applyVec (runJS op) v === applyVec (run op) v    

-- Use that assumption to prove that 2n+1JS is the same as 2n+1.
2n+1JS=2n+1 : {n : Int} -> 2n+1JS n === 2n+1 n
2n+1JS=2n+1 = run=runJS 2n+1Op