Skip to content

Commit

Permalink
Squashed commit of the following:
Browse files Browse the repository at this point in the history 
commit 0f99b138457bf67ac04982524c0947f0eae024a6
Author: Sam Griffin <[email protected]>
Date:   Mon Apr 29 17:42:07 2024 -0400

    adding simpler church numeral sizing test file

commit b8e253f22a2a7744233a8254d1b066a3e47aaaf5
Author: Sam Griffin <[email protected]>
Date:   Tue Apr 23 18:41:33 2024 -0400

    faster, more space-efficient sizing. sizing works for unit tests, but uses too much memory for tictactoe

commit 0563d1f
Author: Sam Griffin <[email protected]>
Date:   Wed Mar 13 21:09:48 2024 -0400

    missed GateSwitch cases

commit 67abaea
Author: Sam Griffin <[email protected]>
Date:   Fri Mar 8 13:18:11 2024 -0500

    Squashed commit of the following:

    commit 627a97a
    Author: Sam Griffin <[email protected]>
    Date:   Tue Jan 16 20:03:42 2024 -0500

        sizing by evaluation, doesn't work because insufficiently lazy

    commit 7dae821
    Author: Sam Griffin <[email protected]>
    Date:   Tue Dec 12 19:41:35 2023 -0500

        make stuck a standard functor, and change evaluation to use custom defer-skipping transform

    commit 0149ba0
    Author: Sam Griffin <[email protected]>
    Date:   Thu Nov 16 14:58:34 2023 -0500

        profiling support and optimizing d2c in Prelude

    commit 012e1c3
    Author: Sam Griffin <[email protected]>
    Date:   Tue Nov 7 17:29:28 2023 -0500

        can now handle sizing multiple bound recursion combinators separately, but still too slow

    commit 83f9272
    Author: Sam Griffin <[email protected]>
    Date:   Mon Oct 30 17:13:55 2023 -0400

        appears to work, but is too slow

    commit f16e675
    Author: Sam Griffin <[email protected]>
    Date:   Wed Oct 18 18:24:18 2023 -0400

        a flawed approach to sizing

        trying to do evaluation of unsizedstubs in place, but the needed
        context isn't there to properly size

    commit f4fc372
    Author: Sam Griffin <[email protected]>
    Date:   Tue Oct 10 13:42:36 2023 -0400

        evalBU works with new base functor

    commit 56b8a34
    Author: Sam Griffin <[email protected]>
    Date:   Fri Oct 6 18:04:07 2023 -0400

        replacing splitfunctor with base functor fragment classes

    commit 077924e
    Author: Sam Griffin <[email protected]>
    Date:   Tue Sep 26 11:54:47 2023 -0400

        ability to dump unsized expression grammar (probably flawed)

    commit 0c45165
    Author: Sam Griffin <[email protected]>
    Date:   Thu Sep 21 11:06:36 2023 -0400

        new unsized recursion wrapper

    commit 2dc6a13
    Author: Sam Griffin <[email protected]>
    Date:   Mon Sep 4 19:10:54 2023 -0400

        memoized sizing results... still too slow/memory hungry

    commit 599235d
    Author: Sam Griffin <[email protected]>
    Date:   Wed Aug 23 10:57:11 2023 -0400

        removed unusedbits and now evalB seems to work

    commit 9e94f07
    Author: Sam Griffin <[email protected]>
    Date:   Fri Jul 21 15:51:49 2023 -0400

        more debugging info

    commit fb8f597
    Author: Sam Griffin <[email protected]>
    Date:   Thu Jul 13 11:05:45 2023 -0400

        debugging info printing for BitsExpr

    commit 43b5258
    Author: Sam Griffin <[email protected]>
    Date:   Mon Jul 3 17:58:18 2023 -0400

        BitsExpr for removing right/left in prep for passing to SAT. Currently untested

    commit b174c3e
    Author: Sam Griffin <[email protected]>
    Date:   Tue Mar 21 12:57:07 2023 -0400

        appears to work but is too slow. Note sizing foldr with nested sizing of d2c inside

    commit b2b1659
    Author: Sam Griffin <[email protected]>
    Date:   Tue Feb 28 16:58:36 2023 -0500

        wip

    commit 6074592
    Author: Sam Griffin <[email protected]>
    Date:   Fri Dec 16 15:58:59 2022 -0500

        partial, some issue with sizingresult evaluation?

    commit 00f7a37
    Author: Sam Griffin <[email protected]>
    Date:   Mon Oct 17 15:38:25 2022 -0400

        partially evaluate sizeTerm test (might make things faster, but currently undetermined

    commit 090a02a
    Author: Sam Griffin <[email protected]>
    Date:   Wed Oct 5 16:18:15 2022 -0400

        unit tests complete in a reasonable time with church sizing, but tictactoe is still to slow

    commit 503f442
    Author: Sam Griffin <[email protected]>
    Date:   Tue Sep 27 18:02:50 2022 -0400

        incremental resizing from the bottom up works, but is too slow

    commit 8d3e98f
    Author: Sam Griffin <[email protected]>
    Date:   Wed Sep 14 13:27:53 2022 -0400

        recursion test needs unsized token, removing old possible design

    commit db70b8a
    Author: Sam Griffin <[email protected]>
    Date:   Thu Sep 8 19:27:47 2022 -0400

        static abort checking works with bottom up eval

    commit d09bb1f
    Author: Sam Griffin <[email protected]>
    Date:   Fri Sep 2 21:06:27 2022 -0400

        fixing build post rebase

    commit 246b6f6
    Author: Sam Griffin <[email protected]>
    Date:   Thu Jul 7 14:12:06 2022 -0400

        handleSuper is implemented but untested

    commit acfded5
    Author: Sam Griffin <[email protected]>
    Date:   Sun Jun 26 14:09:32 2022 -0400

        evalbottomup is extensible

    commit a48222e
    Author: Sam Griffin <[email protected]>
    Date:   Thu Jun 23 20:15:12 2022 -0400

        made stuckF extensible, with multiple reasons for sticking

    commit 30b4fdf
    Author: Sam Griffin <[email protected]>
    Date:   Sun Jun 19 14:06:22 2022 -0400

        bottom up evaluation works!

    commit 8161962
    Author: Sam Griffin <[email protected]>
    Date:   Fri Jun 10 12:30:54 2022 -0400

        effectful bottom up eval for testing

    commit 3995a6d
    Author: Sam Griffin <[email protected]>
    Date:   Fri Jun 10 12:29:15 2022 -0400

        making HLS work. This commit should be in master

    commit 5241211
    Author: Sam Griffin <[email protected]>
    Date:   Wed Jun 8 19:19:55 2022 -0400

        bottom up eval, partially broken

    commit e9b1644
    Author: Sam Griffin <[email protected]>
    Date:   Mon May 16 19:54:14 2022 -0400

        committing for ghc bug report

    commit 75b4474
    Author: Sam Griffin <[email protected]>
    Date:   Tue May 3 18:37:09 2022 -0400

        still uses too much memory for church sizing, but probably less. Also, type checking written for Possible structure

commit a9b7c79
Author: Sam Griffin <[email protected]>
Date:   Fri Mar 8 08:00:52 2024 -0500

    reenabling static checks in main
  • Loading branch information
@sfultong
sfultong committed May 4, 2024
1 parent 0b7663a commit e688e44
Show file tree
Hide file tree
Showing 12 changed files with 1,220 additions and 420 deletions.
13 changes: 9 additions & 4 deletions Prelude.tel
View file
Original file line number Diff line number Diff line change
Expand Up @@ -8,10 +8,10 @@ not = \x -> if x then 0 else 1

succ = \x -> (x,0)

d2c = { id
, \recur i f b -> f (recur (left i) f b)
, \i f b -> b
}
d2c = \n f b -> { id
, \recur i -> f (recur (left i))
, \i -> b
} n

c2d = \c -> c succ 0

Expand Down Expand Up @@ -98,3 +98,8 @@ truncate = \n ->
then (recur (left current), recur (right current))
else 0
in n layer (\x -> 0)

max = \a b -> { \p -> or (left p) (right p)
, \recur p -> recur (left (left p), left (right p))
, \p -> if (left p) then b else a
} (a,b)
23 changes: 7 additions & 16 deletions bench/MemoryBench.hs
View file
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
{-# LANGUAGE CApiFFI #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE ScopedTypeVariables #-}
module Main where
Expand All @@ -20,18 +20,16 @@ import Telomare.Parser
import Telomare.RunTime
import Telomare.TypeChecker (TypeCheckError (..), inferType, typeCheck)

import MemoryBench.Cases
import MemoryBench.LLVM
import Paths_telomare
import MemoryBench.Cases
-- import MemoryBench.LLVM
import Paths_telomare

import Text.Parsec.Error (ParseError)
import qualified Weigh
import Weigh hiding (Case, Max)

import Debug.Trace

foreign import capi "gc.h GC_INIT" gcInit :: IO ()
foreign import ccall "gc.h GC_allow_register_threads" gcAllowRegisterThreads :: IO ()
-- TODO:
-- Get some expressions/groups of expressions.
-- Measure memory needed to:
Expand All @@ -44,17 +42,15 @@ foreign import ccall "gc.h GC_allow_register_threads" gcAllowRegisterThreads ::
instance NFData ParseError where
rnf a = ()

type Bindings = [(String, UnprocessedParsedTerm)]

processCase :: Bindings -> Case -> Weigh ()
processCase bindings (Case label code) = do
let e_parsed = parseMain bindings code
(Right parsed) = e_parsed --Taking advantage of lazy evalutation here
details = benchLLVMDetails parsed
let e_parsed = fmap toTelomare $ parseMain bindings code
(Right (Just parsed)) = e_parsed --Taking advantage of lazy evalutation here
let parsing = func "parsing" (parseMain bindings) code -- Parsing
evals = [ io "simpleEval" benchEvalSimple parsed
, io "fasterEval" benchEvalFaster parsed
, io "optimizedEval" benchEvalOptimized parsed
, details
]
weighs = if isRight e_parsed
then sequence_ (parsing : evals)
Expand All @@ -67,18 +63,13 @@ processAllCases bindings = mapM_ (processCase bindings)
benchEvalSimple :: IExpr -> IO IExpr
benchEvalSimple iexpr = simpleEval (SetEnv (Pair (Defer iexpr) Zero))

benchEvalFaster :: IExpr -> IO IExpr
benchEvalFaster iexpr = fasterEval (SetEnv (Pair (Defer iexpr) Zero))

benchEvalOptimized :: IExpr -> IO IExpr
benchEvalOptimized iexpr = optimizedEval (SetEnv (Pair (Defer iexpr) Zero))

config :: Config
config = Config [Weigh.Case, Allocated, GCs, Live] "" Plain

main = do
gcInit
gcAllowRegisterThreads
preludeFile <- Strict.readFile "Prelude.tel"

let
Expand Down
7 changes: 7 additions & 0 deletions flake.nix
View file
Original file line number Diff line number Diff line change
Expand Up @@ -41,6 +41,13 @@
doRunTests
# hl.dontHaddock
];

overrides = self: super: {
sbv = pkgs.haskell.lib.compose.markUnbroken (pkgs.haskell.lib.dontCheck super.sbv);
};

# uncomment for profiling:
# cabal2nixOptions = "--enable-profiling --benchmark";
};

in {
Expand Down
5 changes: 4 additions & 1 deletion hie.yaml
View file
Original file line number Diff line number Diff line change
@@ -1,3 +1,6 @@
cradle:
cabal:
component: "lib:telomare"
- path: "./src"
component: "lib:telomare"
- path: "./test/Spec.hs"
component: "test:telomare-test"
64 changes: 56 additions & 8 deletions src/PrettyPrint.hs
View file
Original file line number Diff line number Diff line change
@@ -1,16 +1,41 @@
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE FlexibleInstances #-}

module PrettyPrint where

import Data.Map (Map)
import Naturals (NExpr (..), NExprs (..), NResult)
import Telomare (FragExpr (..), FragExprUR (..),
FragExprURSansAnnotation (FragExprURSA, unFragExprURSA),
FragIndex (..), IExpr (..), PartialType (..),
PrettyPartialType (..), RecursionSimulationPieces (..),
Term3 (..), forget, forgetAnnotationFragExprUR, rootFrag)
import Control.Monad.State (State)
import Data.Map (Map)
import Naturals (NExpr (..), NExprs (..), NResult)
import Telomare (FragExpr (..), FragExprUR (..), FragIndex (..),
FragExprURSansAnnotation (FragExprURSA, unFragExprURSA),
IExpr (..), PartialType (..), PrettyPartialType (..),
RecursionSimulationPieces (..), Term3 (..), rootFrag, forget,
forgetAnnotationFragExprUR, indentWithTwoChildren', indentWithOneChild',
FragExprF (..), LocTag,
)

import qualified Control.Monad.State as State
import qualified Data.Map as Map
import qualified Control.Comonad.Trans.Cofree as CofreeT (CofreeF (..))

import Control.Comonad.Cofree
import Data.Functor.Foldable
import Data.SBV (sFPHalf)


class PrettyPrintable p where
showP :: p -> State Int String

class PrettyPrintable1 p where
showP1 :: PrettyPrintable a => p a -> State Int String

instance (PrettyPrintable1 f, PrettyPrintable x) => PrettyPrintable (f x) where
showP = showP1

-- instance (Base r ~ PrettyPrintable1 f, Recursive r) => PrettyPrintable r where

prettyPrint :: PrettyPrintable p => p -> String
prettyPrint x = State.evalState (showP x) 0

indent :: Int -> String
indent 0 = []
Expand Down Expand Up @@ -107,6 +132,29 @@ showNExprs (NExprs m) = concatMap
-- termMap, function->type lookup, root frag type
data TypeDebugInfo = TypeDebugInfo Term3 (FragIndex -> PartialType) PartialType

instance PrettyPrintable Term3 where
showP (Term3 termMap) = showFrag (unFragExprUR $ rootFrag termMap) where
showFrag = cata showF
showF (_ CofreeT.:< x) = sf x
showL (a CofreeT.:< _) = show a
sf = \case
ZeroFragF -> pure "Z"
PairFragF a b -> indentWithTwoChildren' "P" a b
EnvFragF -> pure "E"
SetEnvFragF x -> indentWithOneChild' "S" x
DeferFragF fi -> case Map.lookup fi termMap of
Just frag -> let f = unFragExprUR frag
in indentWithOneChild' ("D" <> showL (project f)) $ showFrag f
z -> error $ "PrettyPrint Term3 bad index found: " <> show z
AbortFragF -> pure "A"
GateFragF l r -> indentWithTwoChildren' "G" l r
LeftFragF x -> indentWithOneChild' "L" x
RightFragF x -> indentWithOneChild' "R" x
TraceFragF -> pure "T"
AuxFragF x -> case x of
SizingWrapper _ x' -> indentWithOneChild' "?" . showFrag $ unFragExprUR x'
NestedSetEnvs _ -> pure "%"

showTypeDebugInfo :: TypeDebugInfo -> String
showTypeDebugInfo (TypeDebugInfo (Term3 m) lookup rootType) =
let termMap = forgetAnnotationFragExprUR <$> m
Expand All @@ -128,7 +176,7 @@ showTypeDebugInfo (TypeDebugInfo (Term3 m) lookup rootType) =
LeftFrag x -> "L " <> recur x
RightFrag x -> "R " <> recur x
TraceFrag -> "T"
AuxFrag (RecursionTest (FragExprURSA x)) -> "?" <> recur x
AuxFrag (SizingWrapper _ (FragExprURSA x)) -> "?" <> recur x
AuxFrag (NestedSetEnvs _) -> "%"
in showFrag (FragIndex 0) rootType (unFragExprURSA $ rootFrag termMap) <> "\n"
<> concatMap (\(k, v) -> showFrag k (lookup k) v <> "\n")
Expand Down
88 changes: 72 additions & 16 deletions src/Telomare.hs
View file
Original file line number Diff line number Diff line change
@@ -1,3 +1,4 @@
{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE DeriveTraversable #-}
Expand All @@ -13,7 +14,7 @@
module Telomare where --(IExpr(..), ParserTerm(..), LamType(..), Term1(..), Term2(..), Term3(..), Term4(..)
--, FragExpr(..), FragIndex, TelomareLike, fromTelomare, toTelomare, rootFrag) where

import Control.Applicative (Applicative (liftA2), liftA3)
import Control.Applicative (liftA, Applicative (liftA2), liftA3)
import Control.Comonad.Cofree (Cofree ((:<)))
import qualified Control.Comonad.Trans.Cofree as CofreeT (CofreeF (..))
import Control.DeepSeq (NFData (..))
Expand Down Expand Up @@ -192,6 +193,29 @@ indentWithOneChild str sx = do
x <- sx
pure $ indent i (str <> "\n") <> x

indentWithOneChild' :: String -> State Int String -> State Int String
indentWithOneChild' str sx = do
i <- State.get
State.put $ i + 2
x <- sx
pure $ str <> " " <> x

indentWithTwoChildren' :: String -> State Int String -> State Int String -> State Int String
indentWithTwoChildren' str sl sr = do
i <- State.get
State.put $ i + 2
l <- sl
State.put $ i + 2
r <- sr
-- pure $ indent i (str <> "\n") <> l <> "\n" <> r
pure $ str <> " " <> l <> "\n" <> indent (i + 2) r

indentWithChildren' :: String -> [State Int String] -> State Int String
indentWithChildren' str l = do
i <- State.get
let doLine = (liftA (<> "\n" <> indent (i + 2) "")) . (State.put (i + 2) >>)
foldl (\s c -> (<>) <$> s <*> c) (pure $ str <> " ") $ map doLine l

-- |Two children indentation.
indentWithTwoChildren :: String -> State Int String -> State Int String -> State Int String
indentWithTwoChildren str sl sr = do
Expand Down Expand Up @@ -233,7 +257,7 @@ data FragExpr a
| RightFrag (FragExpr a)
| TraceFrag
| AuxFrag a
deriving (Eq, Ord, Functor)
deriving (Eq, Ord, Generic, NFData)
makeBaseFunctor ''FragExpr -- Functorial version FragExprF.
deriveShow1 ''FragExprF
deriveEq1 ''FragExprF
Expand Down Expand Up @@ -266,31 +290,34 @@ instance Show a => Show (FragExpr a) where

newtype EIndex = EIndex { unIndex :: Int } deriving (Eq, Show, Ord)

newtype UnsizedRecursionToken = UnsizedRecursionToken { unUnsizedRecursionToken :: Int } deriving (Eq, Ord, Show, Enum)
newtype UnsizedRecursionToken = UnsizedRecursionToken { unUnsizedRecursionToken :: Int } deriving (Eq, Ord, Show, Enum, NFData, Generic)

data RecursionSimulationPieces a
= NestedSetEnvs UnsizedRecursionToken
| RecursionTest a
deriving (Eq, Ord, Show, Functor)
| SizingWrapper UnsizedRecursionToken a
deriving (Eq, Ord, Show, NFData, Generic, Functor)

data LocTag
= DummyLoc
| Loc Int Int
deriving (Eq, Show, Ord)
deriving (Eq, Show, Ord, Generic, NFData)

newtype FragExprUR =
FragExprUR { unFragExprUR :: Cofree (FragExprF (RecursionSimulationPieces FragExprUR))
LocTag
}
deriving (Eq, Show)
deriving (Eq, Show, Generic)
instance NFData FragExprUR where
-- rnf (FragExprUR (a :< x)) = seq (rnf a) $ rnf x
rnf (FragExprUR (a :< !x)) = seq (rnf a) () -- TODO fix if we ever care about proper NFData

type RecursionPieceFrag = RecursionSimulationPieces FragExprUR

type Term1 = Cofree (ParserTermF String String) LocTag
type Term2 = Cofree (ParserTermF () Int) LocTag

-- |Term3 :: Map FragIndex (FragExpr BreakExtras) -> Term3
newtype Term3 = Term3 (Map FragIndex FragExprUR) deriving (Eq, Show)
newtype Term3 = Term3 (Map FragIndex FragExprUR) deriving (Eq, Show, Generic, NFData)
newtype Term4 = Term4 (Map FragIndex (Cofree (FragExprF Void) LocTag)) deriving (Eq, Show)

type BreakState a b = State (b, FragIndex, Map FragIndex (Cofree (FragExprF a) LocTag))
Expand Down Expand Up @@ -517,32 +544,35 @@ 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))
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
-- 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
wrapTest = \case
(anno :< PairFragF d@(_ :< DeferFragF _) e) ->
anno :< PairFragF ((anno :< ) . AuxFragF . RecursionTest . FragExprUR $ d) e
_ -> error "unsizedRecursionWrapper unexpected recursion test section"
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)))
trb = pairF b (pairF r (pairF (wrapTest <$> t) (pure . tag DummyLoc $ ZeroFrag)))
in setEnvF $ pairF (deferF $ appF (appF churchNum rWrap) firstArgF) trb
trb = pairF b (pairF r (pairF tWrap (pure . tag DummyLoc $ ZeroFrag)))
in setEnvF . wrapU $ pairF (deferF $ appF (appF churchNum rWrap) firstArgF) trb

nextBreakToken :: (Enum b, Show b) => BreakState a b b
nextBreakToken = do
Expand Down Expand Up @@ -650,6 +680,18 @@ mergePairTypeP = transform f where
f (PairTypeP ZeroTypeP ZeroTypeP) = ZeroTypeP
f x = x

containsFunction :: PartialType -> Bool
containsFunction = \case
ArrTypeP _ _ -> True
PairTypeP a b -> containsFunction a || containsFunction b
_ -> False

cleanType :: PartialType -> Bool
cleanType = \case
ZeroTypeP -> True
PairTypeP a b -> cleanType a && cleanType b
_ -> False

newtype PrettyIExpr = PrettyIExpr IExpr

instance Show PrettyIExpr where
Expand Down Expand Up @@ -799,7 +841,7 @@ forgetAnnotationFragExprUR = FragExprURSA . cata ff . forget' . unFragExprUR whe
(FragExpr (RecursionSimulationPieces FragExprURSansAnnotation))
-> FragExpr (RecursionSimulationPieces FragExprURSansAnnotation)
ff = \case
AuxFragF (RecursionTest x) -> AuxFrag . RecursionTest . forgetAnnotationFragExprUR $ x
AuxFragF (SizingWrapper ind x) -> AuxFrag . SizingWrapper ind . forgetAnnotationFragExprUR $ x
AuxFragF (NestedSetEnvs t) -> AuxFrag . NestedSetEnvs $ t
ZeroFragF -> ZeroFrag
PairFragF a b -> PairFrag a b
Expand Down Expand Up @@ -833,9 +875,23 @@ insertAndGetKey v = do
pure nextKey

-- abort codes
-- t x = if x <= 1
-- fact1 r x = if x <= 1
-- then 1
-- else x * (r (x - 1))
-- fix fact1
-- (\f x -> f x) fact1 (\_ -> error!) 3 -- error!
-- (\f x -> f (f x)) fact1 (\_ -> error!) 3 -- error!
-- (\f x -> f (f (f x))) fact1 (\_ -> error!) 3 -- 3, happy!
-- setenv env -- church numeral 1
-- setenv (setenv env) -- church numeral 2


pattern AbortRecursion :: IExpr
pattern AbortRecursion = Pair Zero Zero
pattern AbortUser :: IExpr -> IExpr
pattern AbortUser m = Pair (Pair Zero Zero) m
pattern AbortAny :: IExpr
pattern AbortAny = Pair (Pair (Pair Zero Zero) Zero) Zero
pattern AbortUnsizeable :: IExpr -> IExpr
pattern AbortUnsizeable t = Pair (Pair (Pair (Pair Zero Zero) Zero) Zero) t
Loading

0 comments on commit e688e44

Please sign in to comment.