Skip to content

Commit 49be86a

Browse files
committed
removing sizingwrapper, since it's no longer necessary
1 parent 1a6d188 commit 49be86a

7 files changed

Lines changed: 13 additions & 100 deletions

File tree

src/PrettyPrint.hs

Lines changed: 0 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -155,7 +155,6 @@ instance PrettyPrintable Term3 where
155155
RightFragF x -> indentWithOneChild' "R" x
156156
TraceFragF -> pure "T"
157157
AuxFragF x -> case x of
158-
SizingWrapper _ ind x' -> indentWithOneChild' ("?" <> show (fromEnum ind)) . showFrag $ unFragExprUR x'
159158
CheckingWrapper l tc x' -> indentWithTwoChildren' (":" <> show l) (showFrag $ unFragExprUR tc) (showFrag $ unFragExprUR x')
160159
NestedSetEnvs _ -> pure "%"
161160

@@ -219,7 +218,6 @@ showTypeDebugInfo (TypeDebugInfo (Term3 m) lookup rootType) =
219218
LeftFrag x -> "L " <> recur x
220219
RightFrag x -> "R " <> recur x
221220
TraceFrag -> "T"
222-
AuxFrag (SizingWrapper _ _ (FragExprURSA x)) -> "?" <> recur x
223221
AuxFrag (NestedSetEnvs _) -> "%"
224222
in showFrag (FragIndex 0) rootType (unFragExprURSA $ rootFrag termMap) <> "\n"
225223
<> concatMap (\(k, v) -> showFrag k (lookup k) v <> "\n")

src/Telomare.hs

Lines changed: 1 addition & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -419,7 +419,6 @@ instance Validity UnsizedRecursionToken
419419

420420
data RecursionSimulationPieces a
421421
= NestedSetEnvs UnsizedRecursionToken
422-
| SizingWrapper LocTag UnsizedRecursionToken a
423422
| CheckingWrapper LocTag a a
424423
deriving (Eq, Ord, Show, NFData, Generic, Functor)
425424

@@ -703,15 +702,14 @@ unsizedRecursionWrapper loc urToken t r b =
703702
-- b is on the stack when this is called, so args are (i, (b, ...))
704703
abrt = nsLamF (setEnvF $ pairF (setEnvF (pairF abortFragF abortToken))
705704
(appF secondArgF firstArgF))
706-
wrapU = fmap ((loc :<) . AuxFragF . SizingWrapper loc urToken . FragExprUR)
707705
-- \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
708706
rWrap = nsLamF . lamF $ iteF (appF fifthArgF firstArgF)
709707
(appF (appF fourthArgF secondArgF) firstArgF)
710708
(appF thirdArgF firstArgF)
711709
-- hack to make sure recursion test wrapper can be put in a definite place when sizing
712710
tWrap = pairF (deferF $ appF secondArgF firstArgF) (pairF t . pure $ loc :< ZeroFragF)
713711
trb = pairF b (pairF r (pairF tWrap (pure . tag loc $ ZeroFrag)))
714-
in wrapU $ pairF (deferF $ appF (appF (appF (repeatFunctionF loc) firstArgF) rWrap) abrt) trb
712+
in pairF (deferF $ appF (appF (appF (repeatFunctionF loc) firstArgF) rWrap) abrt) trb
715713

716714
nextBreakToken :: (Enum b, Show b) => BreakState a b b
717715
nextBreakToken = do
@@ -944,13 +942,6 @@ newtype FragExprURSansAnnotation =
944942
}
945943
deriving (Eq, Show)
946944

947-
-- note: throws away SizingWrappers, and just folds their contents
948-
cataFragExprUR :: (CofreeT.CofreeF (FragExprF (RecursionSimulationPieces FragExprUR)) LocTag c -> c) -> FragExprUR -> c
949-
cataFragExprUR f = cata f' . unFragExprUR where
950-
f' = \case
951-
(_ CofreeT.:< AuxFragF (SizingWrapper _ _ x)) -> cataFragExprUR f x
952-
x -> f x
953-
954945
forgetAnnotationFragExprUR :: FragExprUR -> FragExprURSansAnnotation
955946
forgetAnnotationFragExprUR = FragExprURSA . cata ff . forget' . unFragExprUR where
956947
forget' :: Cofree (Base (FragExpr (RecursionSimulationPieces FragExprUR))) anno
@@ -960,7 +951,6 @@ forgetAnnotationFragExprUR = FragExprURSA . cata ff . forget' . unFragExprUR whe
960951
(FragExpr (RecursionSimulationPieces FragExprURSansAnnotation))
961952
-> FragExpr (RecursionSimulationPieces FragExprURSansAnnotation)
962953
ff = \case
963-
AuxFragF (SizingWrapper loc ind x) -> AuxFrag . SizingWrapper loc ind . forgetAnnotationFragExprUR $ x
964954
AuxFragF (NestedSetEnvs t) -> AuxFrag . NestedSetEnvs $ t
965955
ZeroFragF -> ZeroFrag
966956
PairFragF a b -> PairFrag a b

src/Telomare/Eval.hs

Lines changed: 6 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -33,13 +33,13 @@ import Telomare (AbstractRunTime, BreakState, BreakState', ExprA (..),
3333
RunTimeError (..), TelomareLike (..), Term3 (Term3),
3434
Term4 (Term4), UnprocessedParsedTerm (..),
3535
UnprocessedParsedTermF (..), UnsizedRecursionToken (..), app,
36-
appF, cataFragExprUR, convertAbortMessage, deferF, eval,
36+
appF, convertAbortMessage, deferF, eval,
3737
forget, g2s, innerChurchF, insertAndGetKey, pairF, rootFrag,
3838
s2g, setEnvF, tag, unFragExprUR)
3939
import Telomare.Parser (AnnotatedUPT, parseModule, parseOneExprOrTopLevelDefs,
4040
parsePrelude)
4141
import Telomare.Possible (abortExprToTerm4, abortPossibilities, appB,
42-
buildUnsizedLocMap, deferB, evalStaticCheck, getSizesM,
42+
deferB, evalStaticCheck, getSizesM,
4343
sizeTermM, term3ToUnsizedExpr, term4toAbortExpr, evalStaticCheck)
4444
import Telomare.PossibleData (AbortExpr, CompiledExpr (..), SizedRecursion (..),
4545
VoidF, envB, leftB, pairB, pattern AbortFW,
@@ -75,7 +75,6 @@ convertPT ll (Term3 termMap) =
7575
(Cofree (FragExprF RecursionPieceFrag) LocTag)
7676
changeFrag = \case
7777
anno :< AuxFragF (NestedSetEnvs n) -> innerChurchF anno $ ll n
78-
_ :< AuxFragF (SizingWrapper _ _ x) -> transformM changeFrag $ unFragExprUR x
7978
_ :< AuxFragF (CheckingWrapper anno tc c) ->
8079
let performTC = deferF ((\ia -> setEnvF (pairF (setEnvF (pairF (pure $ tag anno AbortFrag) ia))
8180
(pure . tag anno $ RightFrag EnvFrag))) $ appF (pure . tag anno $ LeftFrag EnvFrag)
@@ -296,13 +295,14 @@ showSizingInSource prelude s
296295
parsed = parsePrelude prelude >>= (`parseMain` s)
297296
unsizedExpr = term3ToUnsizedExpr 256 <$> parsed
298297
sizedRecursion = unsizedExpr >>= (first (("Could not size token: " <>) . show) . getSizesM 256)
299-
sizeLocs = Map.toAscList . buildUnsizedLocMap <$> unsizedExpr
298+
sizeLocs = error "TODO showSizingInSource implement sizeLocs" --Map.toAscList . buildUnsizedLocMap <$> unsizedExpr
300299
-- (orphanLocs, lineLocs) = partition ((== DummyLoc) . snd) sizeLocs
301300
(orphanLocs, lineLocs) = case sizeLocs of
302-
Left e -> error ("Could not size: " <> show e)
301+
Left e -> error "uh" -- ("Could not size: " <> show e)
303302
Right sl -> partition ((== DummyLoc) . snd) sl
304303
-- orphanList = map ((<> " ") . show . fst) orphanLocs
305-
orphans = "unsized with no location: " <> foldMap ((<> " ") . show . fst) orphanLocs
304+
-- orphans = "unsized with no location: " <> foldMap ((<> " ") . show . fst) orphanLocs
305+
orphans = error "TODO showSizingInSource thing"
306306
fromEnum' = \case
307307
Loc x _ -> x
308308
_ -> error "unexpected DummyLoc"
@@ -327,7 +327,6 @@ showFunctionIndexesInSource prelude s
327327
unAss (a :< _) = a
328328
-- sizeLocs = (\(fi, t) -> (fi))
329329
reduceL (a CofreeT.:< x) = let l = fromEnum' a in (Min l, Max l) <> fold x
330-
bodyLocs = second (cataFragExprUR reduceL) <$> Map.toAscList funMap
331330
sizeLocs = second (unAss . unFragExprUR) <$> Map.toAscList funMap
332331
(orphanLocs, lineLocs) = partition ((== DummyLoc) . snd) sizeLocs
333332
orphans = "functions with no location: " <> foldMap ((<> " ") . show . fst) orphanLocs

src/Telomare/Possible.hs

Lines changed: 0 additions & 72 deletions
Original file line numberDiff line numberDiff line change
@@ -584,16 +584,6 @@ unsizedStep maxSize recursionTest fullStep handleOther =
584584
UnsizedEE (SizeStageF smb x) -> unsizedEE $ SizeStageF (smb <> sm) x
585585
x -> unsizedEE $ SizeStageF sm x
586586
in \case
587-
UnsizedFW (SizingWrapperF _ tok (BasicEE (PairSF d (BasicEE (PairSF b (BasicEE (PairSF r (BasicEE (PairSF tp (BasicEE ZeroSF))))))))))
588-
-> case tp of
589-
BasicEE (PairSF (StuckEE (DeferSF sid tf)) e) ->
590-
let nt = pairB (stuckEE . DeferSF sid . unsizedEE $ RecursionTestF tok tf) e
591-
trb = pairB b (pairB r (pairB nt zeroB))
592-
-- \t r b i ->
593-
rf = lamB unsizedStepMrfa (iteB (appB argFourB argOneB)
594-
(appB (appB argThreeB (unsizedEE $ SizeStepStubF tok 1 envB)) argOneB)
595-
(unsizedEE . SizeStageF (SizedRecursion . Map.singleton tok $ pure 1) $ appB argTwoB argOneB))
596-
in pairB (deferB unsizedStepMw rf) trb
597587
UnsizedFW (SizeStepStubF tok n (BasicEE (PairSF _ e))) -> -- id -- debugTrace ("hit sizestepstub with " <> show n <> "\nand env of\n" <> prettyPrint e)
598588
pairB (deferB unsizedStepMrfa (unsizedEE . SizeStageF (SizedRecursion . Map.singleton tok $ pure (n + 1)) $ iteB (appB argFourB argOneB)
599589
(appB (appB argThreeB (unsizedEE $ SizeStepStubF tok (n + 1) envB)) argOneB)
@@ -615,28 +605,6 @@ unsizedStepM :: forall a f t m. (Base a ~ f, Traversable f, BasicBase f, StuckBa
615605
-> (f a -> t m a) -> f a -> t m a
616606
unsizedStepM maxSize recursionTest handleOther x = f x where
617607
f = \case
618-
UnsizedFW (SizingWrapperF _ tok (BasicEE (PairSF d (BasicEE (PairSF b (BasicEE (PairSF r (BasicEE (PairSF tp (BasicEE ZeroSF))))))))))
619-
-> case tp of
620-
BasicEE (PairSF (StuckEE (DeferSF sid tf)) e) ->
621-
let nt = pairB (stuckEE . DeferSF sid . unsizedEE $ RecursionTestF tok tf) e
622-
trb = pairB b (pairB r (pairB nt zeroB))
623-
argOne = leftB envB
624-
argTwo = leftB (rightB envB)
625-
argThree = leftB (rightB (rightB envB))
626-
argFour = leftB (rightB (rightB (rightB envB)))
627-
argFive = leftB (rightB (rightB (rightB (rightB envB))))
628-
iteB i t e = fillFunction (fillFunction (gateB (deferB unsizedStepMEInd e) (deferB unsizedStepMTInd t)) i) envB -- TODO THIS IS HOW TO DO LAZY IF/ELSE, COPY!
629-
abrt = lamB unsizedStepMa . abortEE . AbortedF $ AbortRecursion (i2g (fromEnum tok))
630-
rf n = lamB unsizedStepMrfb (lamB unsizedStepMrfa (iteB (appB argFive argOne)
631-
(appB (appB argFour argTwo) argOne)
632-
(unsizedEE . SizeStageF (SizedRecursion . Map.singleton tok $ pure n)
633-
$ appB argThree argOne)))
634-
-- rf' n = appB (rf n) (rf' (n + 1))
635-
rf' n = if n > maxSize
636-
-- then error "reached recursion limit"
637-
then abrt
638-
else appB (rf n) (rf' (n + 1))
639-
in pure $ pairB (deferB unsizedStepMw $ rf' 1) trb
640608
UnsizedFW (RecursionTestF ri x) -> pure $ recursionTest ri x
641609
-- UnsizedFW (SizeStageF urt n x) -> debugTrace ("unsizedStepM hit size of " <> show (urt, n)) StrictAccum (SizedRecursion $ Map.singleton urt n) x
642610
UnsizedFW (SizeStageF sr x) -> lift $ StrictAccum sr x
@@ -646,7 +614,6 @@ unsizedStepM maxSize recursionTest handleOther x = f x where
646614

647615
forceSizes :: Int -> UnsizedExpr -> UnsizedExpr
648616
forceSizes n = cata $ \case
649-
UnsizedFW (SizingWrapperF _ _ sx) -> sx
650617
UnsizedFW (UnsizedStubF _ _) -> iterate (basicEE . SetEnvSF) envB !! n
651618
x -> embed x
652619

@@ -655,29 +622,6 @@ unsizedStepM' :: forall a f t m. (Base a ~ f, Traversable f, BasicBase f, StuckB
655622
=> Int -> Set Integer -> (UnsizedRecursionToken -> a -> a) -> (f a -> t m a) -> f a -> t m a
656623
unsizedStepM' maxSize zeros recursionTest handleOther x = f x where
657624
f = \case
658-
UnsizedFW (SizingWrapperF _ tok uwe@(BasicEE (PairSF d (BasicEE (PairSF b (BasicEE (PairSF r (BasicEE (PairSF tp (BasicEE ZeroSF))))))))))
659-
-> case tp of
660-
BasicEE (PairSF (StuckEE (DeferSF sid tf)) e) ->
661-
let nt = pairB (stuckEE . DeferSF sid . unsizedEE $ RecursionTestF tok tf) e
662-
trb = pairB b (pairB r (pairB nt zeroB))
663-
argOne = leftB envB
664-
argTwo = leftB (rightB envB)
665-
argThree = leftB (rightB (rightB envB))
666-
argFour = leftB (rightB (rightB (rightB envB)))
667-
argFive = leftB (rightB (rightB (rightB (rightB envB))))
668-
iteB i t e = fillFunction (fillFunction (gateB (deferB unsizedStepMEInd e) (deferB unsizedStepMTInd t)) i) envB -- TODO THIS IS HOW TO DO LAZY IF/ELSE, COPY!
669-
abrt = lamB unsizedStepMa . abortEE . AbortedF $ AbortRecursion (i2g (fromEnum tok))
670-
rf n = lamB unsizedStepMrfb (lamB unsizedStepMrfa (iteB (appB argFive argOne)
671-
(appB (appB argFour argTwo) argOne)
672-
(unsizedEE . SizeStageF (SizedRecursion . Map.singleton tok $ pure n)
673-
$ appB argThree argOne)))
674-
-- rf' n = appB (rf n) (rf' (n + 1))
675-
rf' n = if n > maxSize
676-
-- then error "reached recursion limit"
677-
then abrt
678-
else appB (rf n) (rf' (n + 1))
679-
dbt = id
680-
in pure . dbt $ pairB (deferB unsizedStepMw $ rf' 1) trb
681625
UnsizedFW (RecursionTestF ri x) -> pure $ recursionTest ri x
682626
-- UnsizedFW (SizeStageF urt n x) -> debugTrace ("unsizedStepM hit size of " <> show (urt, n)) StrictAccum (SizedRecursion $ Map.singleton urt n) x
683627
UnsizedFW (SizeStageF sr x) -> lift $ StrictAccum sr x
@@ -706,7 +650,6 @@ unsizedStepM''' maxSize zeros recursionTest handleOther x = f x where
706650
argT2One = leftB . unsizedEE $ TraceF "env inside unwrapped sizing wrapper" envB
707651
-- argT2One = leftB envB
708652
f = \case
709-
UnsizedFW (SizingWrapperF _ _ x) -> pure x
710653
UnsizedFW (UnsizedStubF tok (BasicEE (PairSF _ (BasicEE (PairSF _ (BasicEE (PairSF _ (BasicEE (PairSF _ env))))))))) -> case env of
711654
BasicEE (PairSF b (BasicEE (PairSF r (BasicEE (PairSF tp (BasicEE ZeroSF)))))) -> case tp of
712655
BasicEE (PairSF (StuckEE (DeferSF sid tf)) e) ->
@@ -1047,7 +990,6 @@ term3ToUnsizedExpr maxSize (Term3 termMap) =
1047990
LeftFrag x -> basicEE . LeftSF $ f x
1048991
RightFrag x -> basicEE . RightSF $ f x
1049992
TraceFrag -> unsizedEE . TraceF "from Term3" $ basicEE EnvSF
1050-
AuxFrag (SizingWrapper loc tok (FragExprUR x)) -> unsizedEE . SizingWrapperF loc tok . f $ forget x
1051993
AuxFrag (NestedSetEnvs t) -> unsizedEE . UnsizedStubF t . embed $ embedB EnvSF
1052994
AuxFrag (CheckingWrapper loc (FragExprUR tc) (FragExprUR c)) -> unsizedEE $ RefinementWrapperF loc (f $ forget tc) (f $ forget c)
1053995
in f . forget . unFragExprUR $ rootFrag termMap
@@ -1057,7 +999,6 @@ term3ToUnsizedExpr maxSize (Term3 termMap) =
1057999
getInputLimits :: UnsizedExpr -> Set Integer
10581000
getInputLimits = getAccum . transformNoDeferM evalStep . convertIS where
10591001
convertU = \case
1060-
UnsizedFW (SizingWrapperF _ _ _) -> indexedEE AnyF
10611002
UnsizedFW (UnsizedStubF _ _) -> indexedEE AnyF
10621003
UnsizedFW (RecursionTestF _ x) -> x
10631004
UnsizedFW rw@(RefinementWrapperF _ _ _) -> unsizedEE rw
@@ -1110,16 +1051,12 @@ sizeTerm maxSize x = tidyUp . foldAborted . debugResult . transformNoDefer evalS
11101051
tracePartialSizes = id
11111052
setSizes :: Map UnsizedRecursionToken (Maybe Int) -> UnsizedExpr -> UnsizedExpr
11121053
setSizes sizeMap = cata $ \case
1113-
UnsizedFW sw@(SizingWrapperF loc tok sx) -> sx
11141054
UnsizedFW us@(UnsizedStubF tok _) -> tracePartialSizes $ case Map.lookup tok sizeMap of
11151055
Just (Just n) -> debugTrace ("sizeTerm setting size: " <> show (tok, n)) iterate (basicEE . SetEnvSF) (basicEE EnvSF) !! n
11161056
_ -> basicEE . SetEnvSF $ basicEE EnvSF
11171057
x -> embed x
11181058
setSomeSizes :: Map UnsizedRecursionToken (Maybe Int) -> InputSizingExpr -> InputSizingExpr
11191059
setSomeSizes sizeMap = cata $ \case
1120-
UnsizedFW sw@(SizingWrapperF loc tok sx) -> case Map.lookup tok sizeMap of
1121-
Just (Just _) -> sx
1122-
_ -> embed $ embedU sw
11231060
UnsizedFW us@(UnsizedStubF tok _) -> tracePartialSizes $ case Map.lookup tok sizeMap of
11241061
Just (Just n) -> iterate (basicEE . SetEnvSF) (basicEE EnvSF) !! n
11251062
_ -> embed $ embedU us
@@ -1180,7 +1117,6 @@ sizeTermM maxSize doCap x = tidyUp . ($ []) . runReaderT . transformNoDeferM eva
11801117
clean = cata (convertBasic (convertStuck (convertAbort failConvert)))
11811118
setSizes :: Map UnsizedRecursionToken (Maybe Int) -> UnsizedExpr -> UnsizedExpr
11821119
setSizes sizeMap = cata $ \case
1183-
UnsizedFW sw@(SizingWrapperF loc tok sx) -> sx
11841120
UnsizedFW us@(UnsizedStubF tok _) -> case Map.lookup tok sizeMap of
11851121
Just (Just n) -> trace ("sizeTermM setting size: " <> show (tok, n)) iterate (basicEE . SetEnvSF) envB !! (n + 1)
11861122
_ -> trace ("no size found for " <> show tok) setEnvB $ leftB envB
@@ -1233,7 +1169,6 @@ abortPossibilities maxSize x = tidyUp . ($ []) . runReaderT . transformNoDeferM
12331169
clean = cata (convertBasic (convertStuck (convertAbort failConvert)))
12341170
setSizes :: Map UnsizedRecursionToken (Maybe Int) -> UnsizedExpr -> UnsizedExpr
12351171
setSizes sizeMap = cata $ \case
1236-
UnsizedFW sw@(SizingWrapperF loc tok sx) -> sx
12371172
UnsizedFW us@(UnsizedStubF tok _) -> case Map.lookup tok sizeMap of
12381173
Just (Just n) -> debugTrace ("abortPossibilities setting size: " <> show (tok, n)) iterate (basicEE . SetEnvSF) (basicEE EnvSF) !! n
12391174
_ -> basicEE . SetEnvSF $ basicEE EnvSF
@@ -1282,12 +1217,6 @@ getSizesM maxSize x = tidyUp . ($ []) . runReaderT . transformNoDeferM evalStep
12821217
-- evalStep = basicStepM (stuckStepDebugM (abortStepM (indexedAbortStepM (indexedInputStepM zeros (indexedSuperStepM (superStepM' gateResult evalStep (superAbortStepM evalStep (unsizedStepM''' maxSize zeros unsizedTest unhandledError))))))))
12831218
evalStep = basicStepM (stuckStepWithTrace (abortStepM (indexedAbortStepM (indexedInputStepM zeros (indexedSuperStepM (superStepM gateResult evalStep (superAbortStepM evalStep (unsizedStepM''' maxSize zeros unsizedTest' failAndPrintStack))))))))
12841219

1285-
buildUnsizedLocMap :: UnsizedExpr -> Map UnsizedRecursionToken LocTag
1286-
buildUnsizedLocMap = cata f where
1287-
f = \case
1288-
UnsizedFW (SizingWrapperF loc tok x) -> x <> Map.singleton tok loc
1289-
x -> Data.Foldable.fold x
1290-
12911220
removeRefinementWrappers :: (Base g ~ f, BasicBase f, StuckBase f, AbortBase f, UnsizedBase f, Recursive g, Corecursive g) => g -> g
12921221
removeRefinementWrappers = cata f where
12931222
f = \case
@@ -1322,7 +1251,6 @@ regularEval = transformNoDefer f . cata ss where
13221251
let innerTC = appB (leftB envB) (rightB envB)
13231252
performTC = deferB removeRefinementWrappersTC . setEnvB $ pairB (setEnvB $ pairB (abortEE AbortF) innerTC) (rightB envB)
13241253
in setEnvB $ pairB performTC (pairB tc c)
1325-
UnsizedFW (SizingWrapperF _ _ x) -> x
13261254
UnsizedFW (UnsizedStubF _ _) -> iterate setEnvB envB !! 255
13271255
x -> embed x
13281256
-- z -> error ("regularEval unhandled case\n" <> prettyPrint (embed z))

0 commit comments

Comments
 (0)