module Agda.Compiler.JS.Case where
import Prelude hiding ( null )
import Data.Map ( Map, empty, null, mapWithKey, fromListWith, unionWith )
import Data.List ( genericLength, genericTake, intercalate )
import Agda.Syntax.Common ( Nat )
import Agda.Compiler.JS.Pretty ( Pretty, pretty, pretties )
import Agda.Compiler.JS.Syntax
( Exp(Undefined,Local,Lambda,Object,Apply),
LocalId(LocalId), MemberId )
import Agda.Compiler.JS.Substitution ( shiftFrom )
#include "undefined.h"
import Agda.Utils.Impossible ( Impossible(Impossible), throwImpossible )
data Case = Case { pats :: [Patt], body :: Exp }
deriving (Show)
instance Pretty Case where
pretty n i (Case ps e) =
intercalate " " (pretties n i ps) ++ " -> " ++ pretty (n + numVars ps) i e
data Patt =
VarPatt |
Tagged Tag [Patt]
deriving (Show)
instance Pretty Patt where
pretty n i VarPatt = "x"
pretty n i (Tagged (Tag l _ _) ps) =
"(" ++ intercalate " " (pretty n i l : pretties n i ps) ++ ")"
data Tag = Tag MemberId [MemberId] (Exp -> [Exp] -> Exp)
instance Show Tag where
show (Tag i is _) = show i
numVars :: [Patt] -> Nat
numVars = sum . map numVars'
numVars' :: Patt -> Nat
numVars' (VarPatt) = 1
numVars' (Tagged l ps) = 1 + numVars ps
lambda :: [Case] -> Exp
lambda [] = Undefined
lambda (c:cs) = lambda' 0 0 (genericLength (pats c)) (c:cs)
lambda' :: Nat -> Nat -> Nat -> [Case] -> Exp
lambda' l m n [] = Undefined
lambda' l 0 0 (c : cs) = body c
lambda' l 0 n cs = Lambda 1 (lambda' (l+1) 1 (n1) cs)
lambda' l m n cs =
case null ts of
True -> lambda' l (m1) n (map pop cs)
False -> visit cs (Local (LocalId (m1))) [Object (mapWithKey (match l (m1) n cs) ts)]
where
ts = tags cs
pop :: Case -> Case
pop (Case (VarPatt : ps) e) = (Case ps e)
pop _ = __IMPOSSIBLE__
match :: Nat -> Nat -> Nat -> [Case] -> MemberId -> Nat -> Exp
match l m n cs t x = Lambda x (lambda' (l + x) (m + x) n (concat (map (refine t x) cs)))
refine :: MemberId -> Nat -> Case -> [Case]
refine t x (Case (VarPatt : qs) e) =
[Case (genericTake x (repeat VarPatt) ++ qs) (shiftFrom (numVars qs) x e)]
refine t x (Case (Tagged (Tag u _ _) ps : qs) e) | t == u =
[Case (ps ++ qs) e]
refine _ _ _ = []
visit :: [Case] -> Exp -> [Exp] -> Exp
visit (Case (Tagged (Tag _ _ v) _ : _) _ : _ ) = v
visit (Case (VarPatt : _) _ : cs) = visit cs
visit _ = Apply
tags :: [Case] -> Map MemberId Nat
tags = foldl (unionWith max) empty . map tag
tag :: Case -> Map MemberId Nat
tag (Case (Tagged (Tag t us _) ps : qs) e) =
fromListWith max ((t, genericLength ps) : [ (u, 0) | u <- us ])
tag _ = empty