|
29 | 29 |
|
30 | 30 | module CCC.Compiler |
31 | 31 | ( compileNumExpr, |
| 32 | + compileNumExprNaive, |
32 | 33 | compileEnvironment, |
33 | 34 | tryCompileVar, |
34 | 35 | compileNumericBindings |
@@ -438,6 +439,116 @@ sIfFun = SFun $ \case |
438 | 439 | _ -> Left "if: then branch must be integer" |
439 | 440 | _ -> Left "if: condition must be a Scott boolean (selector)" |
440 | 441 |
|
| 442 | +-- --------------------------------------------------------------------------- |
| 443 | +-- Naive (explicit CatExpr) compilation — no NBE |
| 444 | +-- --------------------------------------------------------------------------- |
| 445 | + |
| 446 | +-- | Naive CCC compilation: builds explicit CatExpr nodes directly. |
| 447 | +-- Unlike compileNumExpr (which uses NBE with Haskell closures for |
| 448 | +-- beta-reduction), this compiles into the RVal domain from a unit |
| 449 | +-- context, producing explicit Comp/fanC/Apply nodes at every step. |
| 450 | +-- |
| 451 | +-- For first-order integer programs (no higher-order function passing), |
| 452 | +-- the output is identical to the NBE version — NBE only gains an |
| 453 | +-- advantage for higher-order terms where it can beta-reduce at compile time. |
| 454 | +compileNumExprNaive :: Environment -> Expr -> CatExpr () Integer |
| 455 | +compileNumExprNaive env expr = |
| 456 | + case compileNaive env [] expr of |
| 457 | + Right (RInt e) -> e |
| 458 | + Right _ -> error "Naive compilation: expected integer result" |
| 459 | + Left err -> error ("Naive compilation failed: " ++ err) |
| 460 | + |
| 461 | +-- Direct CatExpr compilation (no NBE). |
| 462 | +-- Uses the same RVal machinery as compileRecExpr but starts from any context. |
| 463 | +-- Builtins are RFun closures (primitives), user-level code builds explicit nodes. |
| 464 | +-- |
| 465 | +-- Key difference from compileExpr (NBE): |
| 466 | +-- NBE: Lam → Haskell closure; App → Haskell application (beta-reduces) |
| 467 | +-- Naive: Lam → RFun closure; App → RFun application (same node building) |
| 468 | +-- For first-order programs, both produce identical CatExpr output because |
| 469 | +-- builtins build the same Comp/fanC nodes. The difference appears only |
| 470 | +-- with higher-order terms where NBE can beta-reduce at compile time. |
| 471 | +compileNaive :: forall c. Environment -> [(String, RVal c)] -> Expr -> Either String (RVal c) |
| 472 | +compileNaive env local = \case |
| 473 | + Int i -> Right (RInt (IntConst i)) |
| 474 | + Var name -> |
| 475 | + case lookup name local of |
| 476 | + Just v -> Right v |
| 477 | + Nothing -> compileNaiveVar name |
| 478 | + App fixHead stepExpr |
| 479 | + | isNaiveFixOp env local fixHead -> compileNaiveFix env stepExpr |
| 480 | + Lam param body -> |
| 481 | + Right (RFun (\arg -> compileNaive env ((param, arg) : local) body)) |
| 482 | + App f x -> do |
| 483 | + fVal <- compileNaive env local f |
| 484 | + xVal <- compileNaive env local x |
| 485 | + applyNaiveVal fVal xVal |
| 486 | + where |
| 487 | + compileNaiveVar name = |
| 488 | + case lookup name env of |
| 489 | + Just expr -> compileNaive env local expr |
| 490 | + Nothing -> case compileRecBuiltin name of |
| 491 | + Just v -> Right v |
| 492 | + Nothing -> Left ("Unbound variable: " ++ name) |
| 493 | + |
| 494 | + applyNaiveVal (RFun fn) x = fn x |
| 495 | + applyNaiveVal _ _ = Left "Cannot apply non-function value" |
| 496 | + |
| 497 | +isNaiveFixOp :: Environment -> [(String, RVal c)] -> Expr -> Bool |
| 498 | +isNaiveFixOp env local = go [] |
| 499 | + where |
| 500 | + go _ (Int _) = False |
| 501 | + go _ (Lam _ _) = False |
| 502 | + go _ (App _ _) = False |
| 503 | + go seen (Var name) |
| 504 | + | name `elem` map fst local = False |
| 505 | + | name == "y" || name == "fix" = True |
| 506 | + | name `elem` seen = False |
| 507 | + | otherwise = |
| 508 | + case lookup name env of |
| 509 | + Just expr -> go (name : seen) expr |
| 510 | + Nothing -> False |
| 511 | + |
| 512 | +compileNaiveFix :: forall c. Environment -> Expr -> Either String (RVal c) |
| 513 | +compileNaiveFix env = \case |
| 514 | + Lam fName stepExpr -> |
| 515 | + case collectLams stepExpr of |
| 516 | + (params, body) -> |
| 517 | + case mkIntArgs (length params) of |
| 518 | + Just (SomeIntArgs args) -> compileNaiveFixGeneric env args fName params body |
| 519 | + Nothing -> Left "fix expects at least one integer argument" |
| 520 | + _ -> Left "fix expects a lambda step function" |
| 521 | + |
| 522 | +compileNaiveFixGeneric :: |
| 523 | + forall c input. |
| 524 | + Environment -> |
| 525 | + IntArgs input -> |
| 526 | + String -> |
| 527 | + [String] -> |
| 528 | + Expr -> |
| 529 | + Either String (RVal c) |
| 530 | +compileNaiveFixGeneric env args fName params body = buildCurried args [] |
| 531 | + where |
| 532 | + buildCurried :: IntArgs remaining -> [CatExpr c Integer] -> Either String (RVal c) |
| 533 | + buildCurried OneArg acc = |
| 534 | + Right $ RFun $ \case |
| 535 | + RInt arg -> applyNaiveFix (acc ++ [arg]) |
| 536 | + _ -> Left "fix expects Integer argument" |
| 537 | + buildCurried (MoreArgs rest) acc = |
| 538 | + Right $ RFun $ \case |
| 539 | + RInt arg -> buildCurried rest (acc ++ [arg]) |
| 540 | + _ -> Left "fix expects Integer argument" |
| 541 | + |
| 542 | + applyNaiveFix :: [CatExpr c Integer] -> Either String (RVal c) |
| 543 | + applyNaiveFix actualArgs = do |
| 544 | + paramTuple <- tupleFromExprs args actualArgs |
| 545 | + recFun <- buildRecFun args |
| 546 | + let fixLocal = |
| 547 | + (fName, recFun) : |
| 548 | + zipWith (\name proj -> (name, RInt proj)) params (argProjections args Snd) |
| 549 | + stepBody <- compileNaive env fixLocal body >>= expectRInt "Recursive body must compile to Integer" |
| 550 | + Right (RInt (Comp (Fix stepBody) paramTuple)) |
| 551 | + |
441 | 552 | -- | Compile an expression, extracting environment variables to morphisms. |
442 | 553 | -- Returns a list of (name, morphism_string_representation) for inspection. |
443 | 554 | compileEnvironment :: Environment -> [(String, String)] |
|
0 commit comments