@@ -14,13 +14,14 @@ data SCDef = SCDef { sc_args :: [(Name, CType)],
1414 sc_def :: SCExp }
1515 deriving Show
1616
17−data SCExp = SVar Name
18− | SApp Name [SCExp]
17+data SCExp = SRef Name
18+ | SApp SCExp [SCExp]
19+ | SLet Name SCExp SCExp
1920 | SFCall String CType [(SCExp, CType)]
2021 | SCon Tag [SCExp]
2122 | SConst Const
22− | SErased
23− | SCase [SAlt]
23+ | SError String
24+ | SCase Name [SAlt]
2425 deriving Show
2526
2627data SAlt = SConCase Tag [Name] SCExp
@@ -28,20 +29,80 @@ data SAlt = SConCase Tag [Name] SCExp
2829 | SDefaultCase SCExp
2930 deriving Show
3031
32+type SCState = ([(Name, SCDef)], Name)
33+
3134sclift :: (Name, Def) -> [(Name, SCDef)]
32−sclift d = execState (sc d) []
35+sclift (n, d) = fst (execState (sc [] d) ([], n))
36+
37+add x = do (xs, b) <- get
38+ put (x : xs, b)
39+
40+nextSC :: State SCState Name
41+nextSC = do (xs, n) <- get
42+ let n' = getNext n
43+ put (xs, n')
44+ return n'
45+ where getNext (UN n) = MN 0 n
46+ getNext (MN i n) = MN (i+1) n
47+ getNext (NS n ns) = NS (getNext n) ns
3348
34−add :: a -> State [a] ()
35−add x = do xs <- get
36− put (x : xs)
49+sname :: State SCState Name
50+sname = do (xs, n) <- get
51+ return n
3752
3853class Lift s t | s -> t where
39− sc :: s -> State [(Name, SCDef)] t
54+ sc :: [Name] -> s -> State SCState t
55+
56+instance Lift Def () where
57+ sc env (Function ty tm) = do n <- sname
58+ tm' <- sc env tm
59+ add (n, SCDef (zip env (repeat Nothing)) tm')
60+ sc env (TyDecl _ _) = do n <- sname
61+ add (n, SCDef (zip env (repeat Nothing))
62+ (SError $ "undefined " ++ show n))
63+ sc env (Operator _ _ _) = return ()
64+ sc env (CaseOp _ _ _ _ _ args cases)
65+ = do n <- sname
66+ cases' <- sc (env ++ args) cases
67+ add (n, SCDef (zip (env ++ args) (repeat Nothing)) cases')
68+
69+instance Lift (TT Name) SCExp where
70+ sc env (P _ n _) = return $ SRef n
71+ sc env (V i) = return $ SRef (env!!i)
72+ sc env fn@(App _ _)
73+ = do let (f, args) = unApply fn
74+ args' <- mapM (sc env) args
75+ case f of
76+ (P (DCon t a) _ _) -> return $ SCon t args'
77+ (P (TCon t a) _ _) -> return $ SCon t args'
78+ _ -> do f' <- sc env f
79+ return $ SApp f' args'
80+ sc env (Constant c) = return $ SConst c
81+ sc env (Bind n (Let _ v) e) = do v' <- sc env v
82+ e' <- sc (n : env) e
83+ return (SLet n v' e')
84+ sc env (Bind n (Lam _) e) = scLam [n] e
85+ where
86+ scLam args (Bind n (Lam _) e) = scLam (n : args) e
87+ scLam args x = do x' <- sc (args ++ env) x
88+ fn <- nextSC
89+ add (fn, SCDef (zip (env ++ reverse args) (repeat Nothing)) x')
90+ return $ SApp (SRef fn) (map SRef env)
91+ sc _ _ = return $ SConst (I 42424242)
92+
4093
41−instance Lift (Name, Def) () where
42− sc (n, d) = do d' <- sc d
43− add (n, d')
94+instance Lift SC SCExp where
95+ sc env (Case n alts) = do alts' <- mapM (sc env) alts
96+ return (SCase n alts')
97+ sc env (STerm t) = do t' <- sc env t
98+ return t'
99+ sc env (UnmatchedCase s) = return (SError s)
44100
45−instance Lift Def SCDef where
46− sc x = undefined
101+instance Lift CaseAlt SAlt where
102+ sc env (ConCase n t args e) = do e' <- sc env e
103+ return (SConCase t args e')
104+ sc env (ConstCase c e) = do e' <- sc env e
105+ return (SConstCase c e')
106+ sc env (DefaultCase e) = do e' <- sc env e
107+ return (SDefaultCase e')
47108