From 7c082dc8046db8ed3cac7432144b10aca065bd90 Mon Sep 17 00:00:00 2001 From: Sam Griffin Date: Mon, 13 May 2024 18:18:12 -0400 Subject: [PATCH] church num refactoring --- src/Telomare.hs | 53 ++++++++++++++++++++++++---------------- src/Telomare/Resolver.hs | 19 +++++++++++--- 2 files changed, 47 insertions(+), 25 deletions(-) diff --git a/src/Telomare.hs b/src/Telomare.hs index cc3ffeb..0241ee0 100644 --- a/src/Telomare.hs +++ b/src/Telomare.hs @@ -131,6 +131,7 @@ data ParserTerm l v | TRight (ParserTerm l v) | TTrace (ParserTerm l v) | THash (ParserTerm l v) + | TChurch Int | TLam (LamType l) (ParserTerm l v) | TLimitedRecursion (ParserTerm l v) (ParserTerm l v) (ParserTerm l v) deriving (Eq, Ord, Functor, Foldable, Traversable) @@ -174,6 +175,7 @@ instance (Show l, Show v) => Show (ParserTerm l v) where alg (TRightF r) = indentWithOneChild "TRight" r alg (TTraceF x) = indentWithOneChild "TTrace" x alg (THashF x) = indentWithOneChild "THash" x + alg (TChurchF n) = sindent $ "TChurch " <> show n alg (TLamF l x) = indentWithOneChild ("TLam " <> show l) x alg (TLimitedRecursionF t r b) = indentWithThreeChildren "TLimitedRecursion" t r b @@ -527,10 +529,34 @@ gateF x y = do iteF :: BreakState' a b -> BreakState' a b -> BreakState' a b -> BreakState' a b iteF x y z = setEnvF (pairF (gateF z y) x) --- to construct a church numeral (\f x -> f ... (f x)) --- the new, optimized church numeral operation iterates on a function "frame" (rf, (rf, (f', (x, env')))) +-- inside two lambdas, (\f x -> ...) +-- creates and iterates on a function "frame" (rf, (rf, (f', (x, env')))) -- rf is the function to pull arguments out of the frame, run f', and construct the next frame -- (f',env') is f (since f may contain a saved environment/closure env we want to use for each iteration) +repeatFunctionF :: (Show a, Enum b) => LocTag -> FragExpr a -> BreakState' a b +repeatFunctionF l repeater = + let applyF = SetEnvFrag $ RightFrag EnvFrag + env' = RightFrag (RightFrag (RightFrag EnvFrag)) + -- takes (rf, (f', (x, env'))), executes f' with (x, env') and creates a new frame + rf = deferF . pure . tag l $ + PairFrag (LeftFrag EnvFrag) + (PairFrag (LeftFrag EnvFrag) + (PairFrag (LeftFrag (RightFrag EnvFrag)) + (PairFrag applyF env'))) + x = pure . tag l $ LeftFrag EnvFrag + f' = pure . tag l . LeftFrag . LeftFrag $ RightFrag EnvFrag + fenv = pure . tag l . RightFrag . LeftFrag $ RightFrag EnvFrag + -- (x, ((f', fenv), 0)) -> (rf, (rf, (f', (x, fenv)))) + frameSetup = rf >>= (\rf' -> pairF (pure rf') (pairF (pure rf') (pairF f' (pairF x fenv)))) + -- run the iterations x' number of times, then unwrap the result from the final frame + unwrapFrame = LeftFrag . RightFrag . RightFrag . RightFrag $ repeater + in clamF (lamF (setEnvF (pairF (deferF (pure . tag l $ unwrapFrame)) frameSetup))) + +-- to construct a church numeral (\f x -> f ... (f x)) +-- the core is nested setenvs around an env, where the number of setenvs is magnitude of church numeral +i2cF :: (Show a, Enum b) => LocTag -> Int -> BreakState' a b +i2cF l n = repeatFunctionF l (iterate SetEnvFrag EnvFrag !! n) + unsizedRecursionWrapper :: UnsizedRecursionToken -> BreakState' RecursionPieceFrag UnsizedRecursionToken -> BreakState' RecursionPieceFrag UnsizedRecursionToken @@ -544,25 +570,9 @@ unsizedRecursionWrapper urToken t r b = fifthArgF = pure . tag DummyLoc . LeftFrag . RightFrag . RightFrag . RightFrag . RightFrag $ EnvFrag abortToken = pure . tag DummyLoc $ PairFrag ZeroFrag ZeroFrag abortFragF = pure $ DummyLoc :< AbortFragF - -- b is on the stack when this is called, so args are (i, (b, 0)) + -- b is on the stack when this is called, so args are (i, (b, ...)) abrt = lamF (setEnvF $ pairF (setEnvF (pairF abortFragF abortToken)) (appF secondArgF firstArgF)) - applyF = SetEnvFrag $ RightFrag EnvFrag - env' = RightFrag (RightFrag (RightFrag EnvFrag)) - -- takes (rf, (f', (x, env'))), executes f' with (x, env') and creates a new frame - rf = deferF . pure . tag DummyLoc $ - PairFrag (LeftFrag EnvFrag) - (PairFrag (LeftFrag EnvFrag) - (PairFrag (LeftFrag (RightFrag EnvFrag)) - (PairFrag applyF env'))) - -- construct the initial frame from f and x ((b, (rWrap, 0)) -> (rf, (rf, (f', (x, env'))))) - frameSetup = do - rf' <- rf - pairF (pure rf') (pairF (pure rf') (pairF (pure . tag DummyLoc $ LeftFrag (LeftFrag (RightFrag EnvFrag))) - (pairF abrt (pure . tag DummyLoc $ - RightFrag (LeftFrag (RightFrag EnvFrag)))))) - -- run the iterations x' number of times, then unwrap the result from the final frame - unwrapFrame = LeftFrag . RightFrag . RightFrag . RightFrag . AuxFrag $ NestedSetEnvs urToken wrapU = fmap ((DummyLoc :<) . AuxFragF . SizingWrapper urToken . FragExprUR) -- \t r b r' i -> if t i then r r' i else b i -- t r b are already on the stack when this is evaluated rWrap = lamF . lamF $ iteF (appF fifthArgF firstArgF) @@ -570,9 +580,10 @@ unsizedRecursionWrapper urToken t r b = (appF thirdArgF firstArgF) -- hack to make sure recursion test wrapper can be put in a definite place when sizing tWrap = pairF (deferF $ appF secondArgF firstArgF) (pairF t . pure $ DummyLoc :< ZeroFragF) - churchNum = clamF (lamF (setEnvF (pairF (deferF (pure . tag DummyLoc $ unwrapFrame)) frameSetup))) + repeater = AuxFrag $ NestedSetEnvs urToken + churchNum = repeatFunctionF DummyLoc repeater trb = pairF b (pairF r (pairF tWrap (pure . tag DummyLoc $ ZeroFrag))) - in setEnvF . wrapU $ pairF (deferF $ appF (appF churchNum rWrap) firstArgF) trb + in setEnvF . wrapU $ pairF (deferF $ appF (appF churchNum rWrap) abrt) trb nextBreakToken :: (Enum b, Show b) => BreakState a b b nextBreakToken = do diff --git a/src/Telomare/Resolver.hs b/src/Telomare/Resolver.hs index 6e35ab0..68d826b 100644 --- a/src/Telomare/Resolver.hs +++ b/src/Telomare/Resolver.hs @@ -25,14 +25,14 @@ import Data.Map.Strict (Map, fromList, keys) import Data.Set (Set, (\\)) import qualified Data.Set as Set import Debug.Trace (trace, traceShow, traceShowId) -import PrettyPrint (TypeDebugInfo (..), showTypeDebugInfo) +import PrettyPrint (TypeDebugInfo (..), showTypeDebugInfo, prettyPrint) import Telomare (BreakState', DataType (..), FragExpr (..), FragExprF (..), FragExprUR (..), FragIndex (..), IExpr (..), IExprF (..), LamType (..), LocTag (..), ParserTerm (..), ParserTermF (..), PartialType (..), RecursionPieceFrag, RecursionSimulationPieces (..), Term1 (..), Term2 (..), Term3 (..), UnsizedRecursionToken, appF, clamF, deferF, forget, - forgetAnnotationFragExprUR, gateF, lamF, nextBreakToken, pairF, + forgetAnnotationFragExprUR, gateF, i2cF, lamF, nextBreakToken, pairF, setEnvF, showRunBreakState', tag, unsizedRecursionWrapper, varNF) import Telomare.Parser (AnnotatedUPT, Pattern (..), PatternF (..), @@ -41,6 +41,12 @@ import Telomare.Parser (AnnotatedUPT, Pattern (..), PatternF (..), parseWithPrelude) import Text.Megaparsec (errorBundlePretty, runParser) +debug :: Bool +debug = True + +debugTrace :: String -> a -> a +debugTrace s x = if debug then trace s x else x + type VarList = [String] -- |Int to ParserTerm @@ -59,6 +65,7 @@ s2t :: LocTag -> String -> Cofree (ParserTermF l v) LocTag s2t anno = ints2t anno . fmap ord -- |Int to Church encoding +{- i2c :: LocTag -> Int -> Term1 i2c anno x = anno :< TLamF (Closed "f") (anno :< TLamF (Open "x") (inner x)) where inner :: Int -> Term1 @@ -66,6 +73,7 @@ i2c anno x = anno :< TLamF (Closed "f") (anno :< TLamF (Open "x") (inner x)) coalg :: Int -> Base Term1 (Either Term1 Int) coalg 0 = anno C.:< TVarF "x" coalg n = anno C.:< TAppF (Left . (anno :<) . TVarF $ "f") (Right $ n - 1) +-} instance MonadFail (Either String) where fail = Left @@ -271,6 +279,7 @@ debruijinize vl = \case (anno :< THashF x) -> (\y -> anno :< THashF y) <$> debruijinize vl x (anno :< TLamF (Open n) x) -> (\y -> anno :< TLamF (Open ()) y) <$> debruijinize (n : vl) x (anno :< TLamF (Closed n) x) -> (\y -> anno :< TLamF (Closed ()) y) <$> debruijinize (n : vl) x + (anno :< TChurchF n) -> pure $ anno :< TChurchF n (anno :< TLimitedRecursionF t r b) -> (\x y z -> anno :< TLimitedRecursionF x y z) <$> debruijinize vl t <*> debruijinize vl r <*> debruijinize vl b rewriteOuterTag :: anno -> Cofree a anno -> Cofree a anno @@ -294,6 +303,7 @@ splitExpr' = \case (anno :< TTraceF x) -> rewriteOuterTag anno <$> setEnvF (pairF (deferF (pure . tag anno $ TraceFrag)) (splitExpr' x)) (anno :< TLamF (Open ()) x) -> rewriteOuterTag anno <$> lamF (splitExpr' x) (anno :< TLamF (Closed ()) x) -> rewriteOuterTag anno <$> clamF (splitExpr' x) + (anno :< TChurchF n) -> i2cF anno n (anno :< TLimitedRecursionF t r b) -> rewriteOuterTag anno <$> (nextBreakToken >>= (\x -> unsizedRecursionWrapper x (splitExpr' t) (splitExpr' r) (splitExpr' b))) @@ -364,7 +374,8 @@ validateVariables prelude term = (\x y z -> anno :< TLimitedRecursionF x y z) <$> validateWithEnvironment t <*> validateWithEnvironment r <*> validateWithEnvironment b - anno :< ChurchUPF n -> pure $ i2c anno n + -- anno :< ChurchUPF n -> pure $ i2c anno n + anno :< ChurchUPF n -> pure $ anno :< TChurchF n anno :< LeftUPF x -> (\y -> anno :< TLeftF y) <$> validateWithEnvironment x anno :< RightUPF x -> (\y -> anno :< TRightF y) <$> validateWithEnvironment x anno :< TraceUPF x -> (\y -> anno :< TTraceF y) <$> validateWithEnvironment x @@ -433,7 +444,7 @@ addBuiltins aupt = DummyLoc :< LetUPF process :: [(String, AnnotatedUPT)] -- ^Prelude -> AnnotatedUPT -> Either String Term3 -process prelude upt = splitExpr <$> process2Term2 prelude upt +process prelude upt = (\dt -> debugTrace ("Resolver process term:\n" <> prettyPrint dt) dt) . splitExpr <$> process2Term2 prelude upt process2Term2 :: [(String, AnnotatedUPT)] -- ^Prelude -> AnnotatedUPT