Skip to content

Commit 1c7bcf9

Browse files
author
Thomas Mahler
committed
update compiler
1 parent 56ea397 commit 1c7bcf9

2 files changed

Lines changed: 230 additions & 5 deletions

File tree

‎src/CCC/Compiler.hs‎

Lines changed: 214 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,5 @@
11
{-# LANGUAGE LambdaCase #-}
2+
{-# LANGUAGE RankNTypes #-}
23

34
{-- | Compilation from lambda calculus expressions (Expr) and environments
45
to CatExpr categorical morphisms.
@@ -20,9 +21,17 @@ module CCC.Compiler
2021
) where
2122

2223
import CCC.CatExpr (CatExpr (..))
24+
import CCC.Cat (fanC)
2325
import CCC.Rewrite (simplify)
2426
import Parser (Environment, Expr (..))
2527

28+
newtype Closed a = Closed (forall z. CatExpr z a)
29+
30+
data SVal
31+
= SInt (Closed Integer)
32+
| SBool (Closed Bool)
33+
| SFun (SVal -> Either String SVal)
34+
2635
-- | A value that can represent lambda-calculus terms in a typed setting.
2736
-- This bridges untyped lambda expressions with typed categorical morphisms.
2837
data Value
@@ -36,8 +45,9 @@ instance Show Value where
3645
show (FunVal _) = "<function>"
3746

3847

39-
-- | Evaluate an expression in an environment, returning a Value.
40-
-- Built-ins are interpreted directly so the compiler can run example programs.
48+
-- | Legacy evaluator for Expr.
49+
-- Used by helper APIs and as a fallback when structural CatExpr compilation
50+
-- does not yet support a construct (for example recursion via y).
4151
evalExpr :: Environment -> Expr -> Value
4252
evalExpr env = evalWith []
4353
where
@@ -116,10 +126,209 @@ evalExpr env = evalWith []
116126
-- | Compile a numeric expression to a CatExpr integer morphism.
117127
-- The result is a morphism of any input type to Integer.
118128
--
119-
-- Important: compilation is symbolic and does not evaluate the source expression.
120-
-- Evaluation happens when the resulting morphism is interpreted.
129+
-- Compilation first attempts a structural translation to CatExpr.
130+
-- Unsupported constructs currently fall back to the legacy evaluator via Lift.
121131
compileNumExpr :: Environment -> Expr -> CatExpr a Integer
122-
compileNumExpr env expr = simplify (Lift (\_ -> evalNumExpr env expr))
132+
compileNumExpr env expr =
133+
case compileIntExpr env expr of
134+
Right (Closed cat) -> simplify cat
135+
-- Keep old behavior for currently unsupported forms (notably recursion via y).
136+
Left _ -> simplify (Lift (\_ -> evalNumExpr env expr))
137+
138+
compileIntExpr :: Environment -> Expr -> Either String (Closed Integer)
139+
compileIntExpr env expr = do
140+
value <- compileExpr env [] expr
141+
case value of
142+
SInt compiled -> Right compiled
143+
_ -> Left "Expected integer expression"
144+
145+
compileExpr :: Environment -> [(String, SVal)] -> Expr -> Either String SVal
146+
compileExpr env localEnv = \case
147+
Int i -> Right (SInt (Closed (IntConst i)))
148+
Var name ->
149+
case lookup name localEnv of
150+
Just value -> Right value
151+
Nothing ->
152+
case lookup name env of
153+
Just expr -> compileExpr env localEnv expr
154+
Nothing -> compileBuiltin name
155+
App (Var "y") stepExpr -> compileUnaryY env localEnv stepExpr
156+
Lam param body -> Right $ SFun $ \argVal -> compileExpr env ((param, argVal) : localEnv) body
157+
App f x -> do
158+
fVal <- compileExpr env localEnv f
159+
xVal <- compileExpr env localEnv x
160+
applySVal fVal xVal
161+
162+
applySVal :: SVal -> SVal -> Either String SVal
163+
applySVal (SFun f) x = f x
164+
applySVal _ _ = Left "Cannot apply non-function value"
165+
166+
type RecCtx = (CatExpr Integer Integer, Integer)
167+
168+
data RVal
169+
= RInt (CatExpr RecCtx Integer)
170+
| RBool (CatExpr RecCtx Bool)
171+
| RFun (RVal -> Either String RVal)
172+
173+
compileUnaryY :: Environment -> [(String, SVal)] -> Expr -> Either String SVal
174+
compileUnaryY env outerLocal = \case
175+
Lam fName (Lam nName body) ->
176+
Right $ SFun $ \case
177+
SInt (Closed arg) -> do
178+
stepBody <- compileRecBody env outerLocal fName nName body
179+
Right (SInt (Closed (Comp (Fix stepBody) arg)))
180+
_ -> Left "y expects Integer argument"
181+
_ -> Left "Only unary y (\\f n. body) is structurally supported"
182+
183+
compileRecBody ::
184+
Environment ->
185+
[(String, SVal)] ->
186+
String ->
187+
String ->
188+
Expr ->
189+
Either String (CatExpr RecCtx Integer)
190+
compileRecBody env outerLocal fName nName body = do
191+
compiled <- go initialLocal body
192+
case compiled of
193+
RInt out -> Right out
194+
_ -> Left "Recursive body must compile to Integer"
195+
where
196+
initialLocal =
197+
[ (fName, RFun recCall),
198+
(nName, RInt Snd)
199+
] ++ mapMaybeS outerLocal
200+
201+
recCall :: RVal -> Either String RVal
202+
recCall (RInt x) = Right (RInt (Comp Apply (fanC Fst x)))
203+
recCall _ = Left "Recursive call expects Integer argument"
204+
205+
go :: [(String, RVal)] -> Expr -> Either String RVal
206+
go local = \case
207+
Int i -> Right (RInt (IntConst i))
208+
Var name ->
209+
case lookup name local of
210+
Just v -> Right v
211+
Nothing -> compileEnvVar name
212+
Lam param expr -> Right (RFun (\arg -> go ((param, arg) : local) expr))
213+
App (App (App (Var "if") cond) thenExpr) elseExpr -> do
214+
condV <- go local cond
215+
thenV <- go local thenExpr
216+
elseV <- go local elseExpr
217+
case (condV, thenV, elseV) of
218+
(RBool c, RInt t, RInt e) -> Right (RInt (Comp IfVal (fanC c (fanC t e))))
219+
_ -> Left "if expects (Bool, Int, Int)"
220+
App f x -> do
221+
fVal <- go local f
222+
xVal <- go local x
223+
applyRVal fVal xVal
224+
225+
compileEnvVar :: String -> Either String RVal
226+
compileEnvVar name =
227+
case lookup name env of
228+
Just expr -> do
229+
compiled <- compileExpr env outerLocal expr
230+
case compiled of
231+
SInt (Closed c) -> Right (RInt c)
232+
SBool (Closed c) -> Right (RBool c)
233+
_ -> Left ("Unsupported environment value in recursive body: " ++ name)
234+
Nothing ->
235+
case compileRecBuiltin name of
236+
Just v -> Right v
237+
Nothing -> Left ("Unbound variable: " ++ name)
238+
239+
compileRecBuiltin :: String -> Maybe RVal
240+
compileRecBuiltin "+" = Just (rIntBin Add)
241+
compileRecBuiltin "-" = Just (rIntBin Sub)
242+
compileRecBuiltin "*" = Just (rIntBin Mul)
243+
compileRecBuiltin "sub" = Just (rIntBin Sub)
244+
compileRecBuiltin "sub1" = Just (rIntUnary (\x -> Comp Sub (fanC x (IntConst 1))))
245+
compileRecBuiltin "is0" = Just (rIntPred (\x -> Comp Eql (fanC x (IntConst 0))))
246+
compileRecBuiltin "eql" = Just (rIntCmp Eql)
247+
compileRecBuiltin "leq" = Just (rIntCmp Leq)
248+
compileRecBuiltin "geq" = Just (rIntCmp Geq)
249+
compileRecBuiltin "true" = Just (RBool T)
250+
compileRecBuiltin "false" = Just (RBool F)
251+
compileRecBuiltin _ = Nothing
252+
253+
applyRVal :: RVal -> RVal -> Either String RVal
254+
applyRVal (RFun f) x = f x
255+
applyRVal _ _ = Left "Cannot apply non-function value"
256+
257+
rIntUnary :: (CatExpr RecCtx Integer -> CatExpr RecCtx Integer) -> RVal
258+
rIntUnary op = RFun $ \case
259+
RInt x -> Right (RInt (op x))
260+
_ -> Left "Expected integer argument"
261+
262+
rIntBin :: CatExpr (Integer, Integer) Integer -> RVal
263+
rIntBin op = RFun $ \left -> Right $ RFun $ \right ->
264+
case (left, right) of
265+
(RInt x, RInt y) -> Right (RInt (Comp op (fanC x y)))
266+
_ -> Left "Expected integer arguments"
267+
268+
rIntPred :: (CatExpr RecCtx Integer -> CatExpr RecCtx Bool) -> RVal
269+
rIntPred predicate = RFun $ \case
270+
RInt x -> Right (RBool (predicate x))
271+
_ -> Left "Expected integer argument"
272+
273+
rIntCmp :: CatExpr (Integer, Integer) Bool -> RVal
274+
rIntCmp op = RFun $ \left -> Right $ RFun $ \right ->
275+
case (left, right) of
276+
(RInt x, RInt y) -> Right (RBool (Comp op (fanC x y)))
277+
_ -> Left "Expected integer arguments"
278+
279+
mapMaybeS :: [(String, SVal)] -> [(String, RVal)]
280+
mapMaybeS [] = []
281+
mapMaybeS ((name, value) : rest) =
282+
case value of
283+
SInt (Closed c) -> (name, RInt c) : mapMaybeS rest
284+
SBool (Closed c) -> (name, RBool c) : mapMaybeS rest
285+
SFun _ -> mapMaybeS rest
286+
287+
compileBuiltin :: String -> Either String SVal
288+
compileBuiltin "+" = Right (sIntBinOp Add)
289+
compileBuiltin "-" = Right (sIntBinOp Sub)
290+
compileBuiltin "*" = Right (sIntBinOp Mul)
291+
compileBuiltin "sub" = Right (sIntBinOp Sub)
292+
compileBuiltin "sub1" = Right (sIntUnaryOp (\x -> Comp Sub (fanC x (IntConst 1))))
293+
compileBuiltin "is0" = Right (sIntPred (\x -> Comp Eql (fanC x (IntConst 0))))
294+
compileBuiltin "eql" = Right (sIntCompare Eql)
295+
compileBuiltin "leq" = Right (sIntCompare Leq)
296+
compileBuiltin "geq" = Right (sIntCompare Geq)
297+
compileBuiltin "if" = Right sIfFun
298+
compileBuiltin "true" = Right (SBool (Closed T))
299+
compileBuiltin "false" = Right (SBool (Closed F))
300+
compileBuiltin "y" = Left "Recursion via y is not yet structurally compiled"
301+
compileBuiltin "/" = Left "Division is not currently supported in CatExpr compilation"
302+
compileBuiltin name = Left ("Unbound variable: " ++ name)
303+
304+
sIntUnaryOp :: (forall z. CatExpr z Integer -> CatExpr z Integer) -> SVal
305+
sIntUnaryOp op = SFun $ \case
306+
SInt (Closed x) -> Right (SInt (Closed (op x)))
307+
_ -> Left "Expected integer argument"
308+
309+
sIntBinOp :: CatExpr (Integer, Integer) Integer -> SVal
310+
sIntBinOp op = SFun $ \left -> Right $ SFun $ \right ->
311+
case (left, right) of
312+
(SInt (Closed x), SInt (Closed y)) -> Right (SInt (Closed (Comp op (fanC x y))))
313+
_ -> Left "Expected integer arguments"
314+
315+
sIntPred :: (forall z. CatExpr z Integer -> CatExpr z Bool) -> SVal
316+
sIntPred predicate = SFun $ \case
317+
SInt (Closed x) -> Right (SBool (Closed (predicate x)))
318+
_ -> Left "Expected integer argument"
319+
320+
sIntCompare :: CatExpr (Integer, Integer) Bool -> SVal
321+
sIntCompare op = SFun $ \left -> Right $ SFun $ \right ->
322+
case (left, right) of
323+
(SInt (Closed x), SInt (Closed y)) -> Right (SBool (Closed (Comp op (fanC x y))))
324+
_ -> Left "Expected integer arguments"
325+
326+
sIfFun :: SVal
327+
sIfFun = SFun $ \cond -> Right $ SFun $ \thenVal -> Right $ SFun $ \elseVal ->
328+
case (cond, thenVal, elseVal) of
329+
(SBool (Closed c), SInt (Closed t), SInt (Closed e)) ->
330+
Right (SInt (Closed (Comp IfVal (fanC c (fanC t e)))))
331+
_ -> Left "if expects (Bool, Int, Int)"
123332

124333
-- | Evaluate an expression to an Integer value.
125334
-- This is used by runtime interpretation of compiled Lift terms.

‎test/CCCCompilerSpec.hs‎

Lines changed: 16 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -47,6 +47,22 @@ spec = do
4747
evaluate (interp (compileNumExpr [] (Lam "x" (Var "x")) :: CatExpr () Integer) ())
4848
`shouldThrow` anyErrorCall
4949

50+
it "compiles unary y-recursion structurally using Fix" $ do
51+
let expr = App (App (Var "y") (Lam "f" (Lam "n"
52+
(App (App (App (Var "if") (App (Var "is0") (Var "n")))
53+
(Int 1))
54+
(App (App (Var "*") (Var "n"))
55+
(App (Var "f") (App (Var "sub1") (Var "n"))))))))
56+
(Int 5)
57+
morph = compileNumExpr [] expr :: CatExpr () Integer
58+
show morph `shouldSatisfy` isInfixOf "Fix"
59+
interp morph () `shouldBe` 120
60+
61+
it "keeps non-unary y-recursion on fallback path" $ do
62+
let expr = App (App (App (Var "y") (Lam "f" (Lam "x" (Lam "y" (Var "x"))))) (Int 1)) (Int 2)
63+
morph = compileNumExpr [] expr :: CatExpr () Integer
64+
show morph `shouldSatisfy` isInfixOf "Lift"
65+
5066
describe "CCC.Compiler environment helpers" $ do
5167
it "returns Right for numeric bindings" $ do
5268
case tryCompileVar [("k", Int 11)] "k" of

0 commit comments

Comments
 (0)
⚡