Skip to content

Commit

Permalink
church num refactoring
Browse files Browse the repository at this point in the history
  • Loading branch information
@sfultong
sfultong committed May 15, 2024
1 parent e688e44 commit 7c082dc
Show file tree
Hide file tree
Showing 2 changed files with 47 additions and 25 deletions.
53 changes: 32 additions & 21 deletions src/Telomare.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Expand Down Expand Up @@ -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

Expand Down Expand Up @@ -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
Expand All @@ -544,35 +570,20 @@ 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)
(appF (appF fourthArgF secondArgF) firstArgF)
(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
Expand Down
19 changes: 15 additions & 4 deletions src/Telomare/Resolver.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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 (..),
Expand All @@ -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
Expand All @@ -59,13 +65,15 @@ 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
inner = apo coalg
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
Expand Down Expand Up @@ -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
Expand All @@ -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)))
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand Down

0 comments on commit 7c082dc

Please sign in to comment.