module Agda.Compiler.JS.Substitution where

import Prelude hiding ( map, lookup )
import Data.Map ( empty, unionWith, singleton, findWithDefault )
import qualified Data.Map as Map
import Data.Maybe ( fromMaybe )
import qualified Data.List as List

import Agda.Syntax.Common ( Nat )
import Agda.Compiler.JS.Syntax
  ( Exp(Self,Undefined,Local,Lambda,Object,Array,Apply,Lookup,If,BinOp,PreOp),
    MemberId, LocalId(LocalId) )
import Agda.Utils.Function ( iterate' )
import Agda.Utils.List ( (!!!) )

-- Map for expressions

map :: Nat -> (Nat -> LocalId -> Exp) -> Exp -> Exp
map :: Int -> (Int -> LocalId -> Exp) -> Exp -> Exp
map Int
m Int -> LocalId -> Exp
f (Local LocalId
i)       = Int -> LocalId -> Exp
f Int
m LocalId
i
map Int
m Int -> LocalId -> Exp
f (Lambda Int
i Exp
e)    = Int -> Exp -> Exp
Lambda Int
i (Int -> (Int -> LocalId -> Exp) -> Exp -> Exp
map (Int
m Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
i) Int -> LocalId -> Exp
f Exp
e)
map Int
m Int -> LocalId -> Exp
f (Object Map MemberId Exp
o)      = Map MemberId Exp -> Exp
Object ((Exp -> Exp) -> Map MemberId Exp -> Map MemberId Exp
forall a b k. (a -> b) -> Map k a -> Map k b
Map.map (Int -> (Int -> LocalId -> Exp) -> Exp -> Exp
map Int
m Int -> LocalId -> Exp
f) Map MemberId Exp
o)
map Int
m Int -> LocalId -> Exp
f (Array [(Comment, Exp)]
es)      = [(Comment, Exp)] -> Exp
Array (((Comment, Exp) -> (Comment, Exp))
-> [(Comment, Exp)] -> [(Comment, Exp)]
forall a b. (a -> b) -> [a] -> [b]
List.map (\(Comment
c, Exp
e) -> (Comment
c, Int -> (Int -> LocalId -> Exp) -> Exp -> Exp
map Int
m Int -> LocalId -> Exp
f Exp
e)) [(Comment, Exp)]
es)
map Int
m Int -> LocalId -> Exp
f (Apply Exp
e [Exp]
es)    = Exp -> [Exp] -> Exp
Apply (Int -> (Int -> LocalId -> Exp) -> Exp -> Exp
map Int
m Int -> LocalId -> Exp
f Exp
e) ((Exp -> Exp) -> [Exp] -> [Exp]
forall a b. (a -> b) -> [a] -> [b]
List.map (Int -> (Int -> LocalId -> Exp) -> Exp -> Exp
map Int
m Int -> LocalId -> Exp
f) [Exp]
es)
map Int
m Int -> LocalId -> Exp
f (Lookup Exp
e MemberId
l)    = Exp -> MemberId -> Exp
Lookup (Int -> (Int -> LocalId -> Exp) -> Exp -> Exp
map Int
m Int -> LocalId -> Exp
f Exp
e) MemberId
l
map Int
m Int -> LocalId -> Exp
f (If Exp
e Exp
e' Exp
e'')   = Exp -> Exp -> Exp -> Exp
If (Int -> (Int -> LocalId -> Exp) -> Exp -> Exp
map Int
m Int -> LocalId -> Exp
f Exp
e) (Int -> (Int -> LocalId -> Exp) -> Exp -> Exp
map Int
m Int -> LocalId -> Exp
f Exp
e') (Int -> (Int -> LocalId -> Exp) -> Exp -> Exp
map Int
m Int -> LocalId -> Exp
f Exp
e'')
map Int
m Int -> LocalId -> Exp
f (PreOp String
op Exp
e)    = String -> Exp -> Exp
PreOp String
op (Int -> (Int -> LocalId -> Exp) -> Exp -> Exp
map Int
m Int -> LocalId -> Exp
f Exp
e)
map Int
m Int -> LocalId -> Exp
f (BinOp Exp
e String
op Exp
e') = Exp -> String -> Exp -> Exp
BinOp (Int -> (Int -> LocalId -> Exp) -> Exp -> Exp
map Int
m Int -> LocalId -> Exp
f Exp
e) String
op (Int -> (Int -> LocalId -> Exp) -> Exp -> Exp
map Int
m Int -> LocalId -> Exp
f Exp
e')
map Int
m Int -> LocalId -> Exp
f Exp
e               = Exp
e

-- Shifting

shift :: Nat -> Exp -> Exp
shift :: Int -> Exp -> Exp
shift = Int -> Int -> Exp -> Exp
shiftFrom Int
0

shiftFrom :: Nat -> Nat -> Exp -> Exp
shiftFrom :: Int -> Int -> Exp -> Exp
shiftFrom Int
m Int
0 Exp
e = Exp
e
shiftFrom Int
m Int
n Exp
e = Int -> (Int -> LocalId -> Exp) -> Exp -> Exp
map Int
m (Int -> Int -> LocalId -> Exp
shifter Int
n) Exp
e

shifter :: Nat -> Nat -> LocalId -> Exp
shifter :: Int -> Int -> LocalId -> Exp
shifter Int
n Int
m (LocalId Int
i) | Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
m     = LocalId -> Exp
Local (Int -> LocalId
LocalId Int
i)
shifter Int
n Int
m (LocalId Int
i) | Bool
otherwise = LocalId -> Exp
Local (Int -> LocalId
LocalId (Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
n))

-- Substitution

subst :: Nat -> [Exp] -> Exp -> Exp
subst :: Int -> [Exp] -> Exp -> Exp
subst Int
0 [Exp]
es Exp
e = Exp
e
subst Int
n [Exp]
es Exp
e = Int -> (Int -> LocalId -> Exp) -> Exp -> Exp
map Int
0 (Int -> [Exp] -> Int -> LocalId -> Exp
substituter Int
n [Exp]
es) Exp
e

substituter :: Nat -> [Exp] -> Nat -> LocalId -> Exp
substituter :: Int -> [Exp] -> Int -> LocalId -> Exp
substituter Int
n [Exp]
es Int
m (LocalId Int
i) | Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
m       = LocalId -> Exp
Local (Int -> LocalId
LocalId Int
i)
substituter Int
n [Exp]
es Int
m (LocalId Int
i) | (Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
m) Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
n = Int -> Exp -> Exp
shift Int
m (Exp -> Exp) -> Exp -> Exp
forall a b. (a -> b) -> a -> b
$ Exp -> Maybe Exp -> Exp
forall a. a -> Maybe a -> a
fromMaybe Exp
Undefined (Maybe Exp -> Exp) -> Maybe Exp -> Exp
forall a b. (a -> b) -> a -> b
$ [Exp]
es [Exp] -> Int -> Maybe Exp
forall a. [a] -> Int -> Maybe a
!!! (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- (Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1 Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
m))
substituter Int
n [Exp]
es Int
m (LocalId Int
i) | Bool
otherwise   = LocalId -> Exp
Local (Int -> LocalId
LocalId (Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
n))

substShift :: Nat -> Nat -> [Exp] -> Exp -> Exp
substShift :: Int -> Int -> [Exp] -> Exp -> Exp
substShift Int
m Int
n [Exp]
es = Int -> [Exp] -> Exp -> Exp
subst Int
m [Exp]
es (Exp -> Exp) -> (Exp -> Exp) -> Exp -> Exp
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Int -> Exp -> Exp
shiftFrom Int
m Int
n

-- A variant on substitution which performs beta-reduction

map' :: Nat -> (Nat -> LocalId -> Exp) -> Exp -> Exp
map' :: Int -> (Int -> LocalId -> Exp) -> Exp -> Exp
map' Int
m Int -> LocalId -> Exp
f (Local LocalId
i)       = Int -> LocalId -> Exp
f Int
m LocalId
i
map' Int
m Int -> LocalId -> Exp
f (Lambda Int
i Exp
e)    = Int -> Exp -> Exp
Lambda Int
i (Int -> (Int -> LocalId -> Exp) -> Exp -> Exp
map' (Int
m Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
i) Int -> LocalId -> Exp
f Exp
e)
map' Int
m Int -> LocalId -> Exp
f (Object Map MemberId Exp
o)      = Map MemberId Exp -> Exp
Object ((Exp -> Exp) -> Map MemberId Exp -> Map MemberId Exp
forall a b k. (a -> b) -> Map k a -> Map k b
Map.map (Int -> (Int -> LocalId -> Exp) -> Exp -> Exp
map' Int
m Int -> LocalId -> Exp
f) Map MemberId Exp
o)
map' Int
m Int -> LocalId -> Exp
f (Array [(Comment, Exp)]
es)      = [(Comment, Exp)] -> Exp
Array (((Comment, Exp) -> (Comment, Exp))
-> [(Comment, Exp)] -> [(Comment, Exp)]
forall a b. (a -> b) -> [a] -> [b]
List.map (\(Comment
c, Exp
e) -> (Comment
c, Int -> (Int -> LocalId -> Exp) -> Exp -> Exp
map' Int
m Int -> LocalId -> Exp
f Exp
e)) [(Comment, Exp)]
es)
map' Int
m Int -> LocalId -> Exp
f (Apply Exp
e [Exp]
es)    = Exp -> [Exp] -> Exp
apply (Int -> (Int -> LocalId -> Exp) -> Exp -> Exp
map' Int
m Int -> LocalId -> Exp
f Exp
e) ((Exp -> Exp) -> [Exp] -> [Exp]
forall a b. (a -> b) -> [a] -> [b]
List.map (Int -> (Int -> LocalId -> Exp) -> Exp -> Exp
map' Int
m Int -> LocalId -> Exp
f) [Exp]
es)
map' Int
m Int -> LocalId -> Exp
f (Lookup Exp
e MemberId
l)    = Exp -> MemberId -> Exp
lookup (Int -> (Int -> LocalId -> Exp) -> Exp -> Exp
map' Int
m Int -> LocalId -> Exp
f Exp
e) MemberId
l
map' Int
m Int -> LocalId -> Exp
f (If Exp
e Exp
e' Exp
e'')   = Exp -> Exp -> Exp -> Exp
If (Int -> (Int -> LocalId -> Exp) -> Exp -> Exp
map' Int
m Int -> LocalId -> Exp
f Exp
e) (Int -> (Int -> LocalId -> Exp) -> Exp -> Exp
map' Int
m Int -> LocalId -> Exp
f Exp
e') (Int -> (Int -> LocalId -> Exp) -> Exp -> Exp
map' Int
m Int -> LocalId -> Exp
f Exp
e'')
map' Int
m Int -> LocalId -> Exp
f (PreOp String
op Exp
e)    = String -> Exp -> Exp
PreOp String
op (Int -> (Int -> LocalId -> Exp) -> Exp -> Exp
map' Int
m Int -> LocalId -> Exp
f Exp
e)
map' Int
m Int -> LocalId -> Exp
f (BinOp Exp
e String
op Exp
e') = Exp -> String -> Exp -> Exp
BinOp (Int -> (Int -> LocalId -> Exp) -> Exp -> Exp
map' Int
m Int -> LocalId -> Exp
f Exp
e) String
op (Int -> (Int -> LocalId -> Exp) -> Exp -> Exp
map' Int
m Int -> LocalId -> Exp
f Exp
e')
map' Int
m Int -> LocalId -> Exp
f Exp
e               = Exp
e

subst' :: Nat -> [Exp] -> Exp -> Exp
subst' :: Int -> [Exp] -> Exp -> Exp
subst' Int
0 [Exp]
es Exp
e = Exp
e
subst' Int
n [Exp]
es Exp
e = Int -> (Int -> LocalId -> Exp) -> Exp -> Exp
map' Int
0 (Int -> [Exp] -> Int -> LocalId -> Exp
substituter Int
n [Exp]
es) Exp
e

-- Beta-reducing application and field access

apply :: Exp -> [Exp] -> Exp
apply :: Exp -> [Exp] -> Exp
apply (Lambda Int
i Exp
e) [Exp]
es = Int -> [Exp] -> Exp -> Exp
subst' Int
i [Exp]
es Exp
e
apply Exp
e            [Exp]
es = Exp -> [Exp] -> Exp
Apply Exp
e [Exp]
es

lookup :: Exp -> MemberId -> Exp
lookup :: Exp -> MemberId -> Exp
lookup (Object Map MemberId Exp
o) MemberId
l = Exp -> MemberId -> Map MemberId Exp -> Exp
forall k a. Ord k => a -> k -> Map k a -> a
findWithDefault Exp
Undefined MemberId
l Map MemberId Exp
o
lookup Exp
e          MemberId
l = Exp -> MemberId -> Exp
Lookup Exp
e MemberId
l

-- Replace any top-level occurrences of self
-- (needed because JS is a cbv language, so any top-level
-- recursions would evaluate before the module has been defined,
-- e.g. exports = { x: 1, y: exports.x } results in an exception,
-- as exports is undefined at the point that exports.x is evaluated),

self :: Exp -> Exp -> Exp
self :: Exp -> Exp -> Exp
self Exp
e (Exp
Self)         = Exp
e
self Exp
e (Object Map MemberId Exp
o)     = Map MemberId Exp -> Exp
Object ((Exp -> Exp) -> Map MemberId Exp -> Map MemberId Exp
forall a b k. (a -> b) -> Map k a -> Map k b
Map.map (Exp -> Exp -> Exp
self Exp
e) Map MemberId Exp
o)
self Exp
e (Array [(Comment, Exp)]
es)     = [(Comment, Exp)] -> Exp
Array (((Comment, Exp) -> (Comment, Exp))
-> [(Comment, Exp)] -> [(Comment, Exp)]
forall a b. (a -> b) -> [a] -> [b]
List.map (\(Comment
c, Exp
x) -> (Comment
c, Exp -> Exp -> Exp
self Exp
e Exp
x)) [(Comment, Exp)]
es)
self Exp
e (Apply Exp
f [Exp]
es)   = case (Exp -> Exp -> Exp
self Exp
e Exp
f) of
  (Lambda Int
n Exp
g) -> Exp -> Exp -> Exp
self Exp
e (Int -> [Exp] -> Exp -> Exp
subst' Int
n [Exp]
es Exp
g)
  Exp
g            -> Exp -> [Exp] -> Exp
Apply Exp
g ((Exp -> Exp) -> [Exp] -> [Exp]
forall a b. (a -> b) -> [a] -> [b]
List.map (Exp -> Exp -> Exp
self Exp
e) [Exp]
es)
self Exp
e (Lookup Exp
f MemberId
l)   = Exp -> MemberId -> Exp
lookup (Exp -> Exp -> Exp
self Exp
e Exp
f) MemberId
l
self Exp
e (If Exp
f Exp
g Exp
h)     = Exp -> Exp -> Exp -> Exp
If (Exp -> Exp -> Exp
self Exp
e Exp
f) (Exp -> Exp -> Exp
self Exp
e Exp
g) (Exp -> Exp -> Exp
self Exp
e Exp
h)
self Exp
e (BinOp Exp
f String
op Exp
g) = Exp -> String -> Exp -> Exp
BinOp (Exp -> Exp -> Exp
self Exp
e Exp
f) String
op (Exp -> Exp -> Exp
self Exp
e Exp
g)
self Exp
e (PreOp String
op Exp
f)   = String -> Exp -> Exp
PreOp String
op (Exp -> Exp -> Exp
self Exp
e Exp
f)
self Exp
e Exp
f              = Exp
f

-- Find the fixed point of an expression, with no top-level occurrences
-- of self.

fix :: Exp -> Exp
fix :: Exp -> Exp
fix Exp
f = Exp
e where e :: Exp
e = Exp -> Exp -> Exp
self Exp
e Exp
f

-- Some helper functions

curriedApply :: Exp -> [Exp] -> Exp
curriedApply :: Exp -> [Exp] -> Exp
curriedApply = (Exp -> Exp -> Exp) -> Exp -> [Exp] -> Exp
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (\ Exp
f Exp
e -> Exp -> [Exp] -> Exp
apply Exp
f [Exp
e])

curriedLambda :: Nat -> Exp -> Exp
curriedLambda :: Int -> Exp -> Exp
curriedLambda Int
n = Int -> (Exp -> Exp) -> Exp -> Exp
forall i a. Integral i => i -> (a -> a) -> a -> a
iterate' Int
n (Int -> Exp -> Exp
Lambda Int
1)

emp :: Exp
emp :: Exp
emp = Map MemberId Exp -> Exp
Object (Map MemberId Exp
forall k a. Map k a
empty)

union :: Exp -> Exp -> Exp
union :: Exp -> Exp -> Exp
union (Object Map MemberId Exp
o) (Object Map MemberId Exp
p) = Map MemberId Exp -> Exp
Object ((Exp -> Exp -> Exp)
-> Map MemberId Exp -> Map MemberId Exp -> Map MemberId Exp
forall k a. Ord k => (a -> a -> a) -> Map k a -> Map k a -> Map k a
unionWith Exp -> Exp -> Exp
union Map MemberId Exp
o Map MemberId Exp
p)
union Exp
e          Exp
f          = Exp
e

vine :: [MemberId] -> Exp -> Exp
vine :: [MemberId] -> Exp -> Exp
vine [MemberId]
ls Exp
e = (MemberId -> Exp -> Exp) -> Exp -> [MemberId] -> Exp
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\ MemberId
l Exp
e -> Map MemberId Exp -> Exp
Object (MemberId -> Exp -> Map MemberId Exp
forall k a. k -> a -> Map k a
singleton MemberId
l Exp
e)) Exp
e [MemberId]
ls

object :: [([MemberId],Exp)] -> Exp
object :: [([MemberId], Exp)] -> Exp
object = (([MemberId], Exp) -> Exp -> Exp)
-> Exp -> [([MemberId], Exp)] -> Exp
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\ ([MemberId]
ls,Exp
e) -> (Exp -> Exp -> Exp
union ([MemberId] -> Exp -> Exp
vine [MemberId]
ls Exp
e))) Exp
emp