diff --git a/Prelude.tel b/Prelude.tel index ed3b3bc..d5e2e59 100644 --- a/Prelude.tel +++ b/Prelude.tel @@ -196,3 +196,14 @@ rDiv = \a b -> num = dTimes n1 d2 den = dTimes d1 n2 in fromRational num den + +first = left +second = \x -> left (right x) +third = \x -> left (right (right x)) +fourth = \x -> left (right (right (right x))) +fifth = \x -> left (right (right (right (right x)))) +sixth = \x -> left (right (right (right (right (right x))))) +seventh = \x -> left (right (right (right (right (right (right x)))))) +eighth = \x -> left (right (right (right (right (right (right (right x))))))) +ninth = \x -> left (right (right (right (right (right (right (right (right x)))))))) +tenth = \x -> left (right (right (right (right (right (right (right (right (right x))))))))) diff --git a/app/Evaluare.hs b/app/Evaluare.hs index 2eb1a42..195ea80 100644 --- a/app/Evaluare.hs +++ b/app/Evaluare.hs @@ -1,3 +1,5 @@ +{-# LANGUAGE RecursiveDo #-} + module Main where import Control.Comonad.Cofree (Cofree ((:<))) diff --git a/app/Main.hs b/app/Main.hs index 7396312..22bc59f 100644 --- a/app/Main.hs +++ b/app/Main.hs @@ -2,11 +2,10 @@ module Main where -import qualified Options.Applicative as O -import System.Directory (listDirectory) -import System.FilePath (takeBaseName, takeExtension) -import qualified System.IO.Strict as Strict -import Telomare.Eval (runMain) +import Data.Maybe (mapMaybe) +import qualified Options.Applicative as O +import System.FilePath (takeBaseName) +import Telomare.Eval (runMain) newtype TelomareOpts = TelomareOpts {telomareFile :: String} @@ -16,15 +15,27 @@ telomareOpts :: O.Parser TelomareOpts telomareOpts = TelomareOpts <$> O.argument O.str (O.metavar "TELOMARE-FILE") -getAllModules :: IO [(String, String)] -getAllModules = do - allEntries <- listDirectory "." - let telFiles = filter (\f -> takeExtension f == ".tel") allEntries - readTelFile :: FilePath -> IO (String, String) - readTelFile file = do - content <- readFile file - return (takeBaseName file, content) - mapM readTelFile telFiles +-- | Recursively load only the modules reachable from the entry file. +getModulesFor :: String -> IO [(String, String)] +getModulesFor entryModule = go [entryModule] [] + where + go [] loaded = return loaded + go (m:queue) loaded + | m `elem` map fst loaded = go queue loaded + | otherwise = do + let filePath = m <> ".tel" + content <- readFile filePath + let imports = extractImports content + go (queue ++ imports) ((m, content) : loaded) + + extractImports :: String -> [String] + extractImports = mapMaybe parseImportLine . lines + + parseImportLine :: String -> Maybe String + parseImportLine line = case words line of + ("import":"qualified":name:_) -> Just name + ("import":name:_) -> Just name + _ -> Nothing main :: IO () main = do @@ -32,5 +43,6 @@ main = do ( O.fullDesc <> O.progDesc "A simple but robust virtual machine" ) topts <- O.execParser opts - allModules :: [(String, String)] <- getAllModules - runMain allModules . takeBaseName . telomareFile $ topts + let entryModule = takeBaseName (telomareFile topts) + allModules <- getModulesFor entryModule + runMain allModules entryModule diff --git a/brands.tel b/brands.tel new file mode 100644 index 0000000..7e25501 --- /dev/null +++ b/brands.tel @@ -0,0 +1,20 @@ +-- import Prelude + +[Nat, toNat, nPlus, nMinus] + = let wrapper = \h -> + let N = \(hc, _) x -> assert (dEqual hc h) "not Natural" + in [ N + , \x -> (h, x) + , \((_, aa) : N) ((_, bb) : N) -> (h, d2c aa succ bb) + , \((_, aa) : N) ((_, bb) : N) -> + let sLeft = \x -> case x of + (l, _) -> l + y -> abort "can't subtract larger number from smaller one" + in (h, d2c bb sLeft aa) + ] + in wrapper (# wrapper) + +-- aux = \x -> if dEqual x 8 then "Success" else "Failure" +-- main = \i -> (aux ((left Nat) 8), 0) + +-- main = \i -> ("hello", 0) diff --git a/brands2.tel b/brands2.tel new file mode 100644 index 0000000..d012a32 --- /dev/null +++ b/brands2.tel @@ -0,0 +1,20 @@ +-- import Prelude + +[Nat, toNat, nPlus, nMinus] + = let wrapper = \h -> + let N = \(hc, _) x -> assert (dEqual hc h) "not Natural" + in [ N + , \x -> (h, x) + , \(_, aa) (_, bb) -> (h, d2c aa succ bb) + , \(_, aa) (_, bb) -> + let sLeft = \x -> case x of + (l, _) -> l + y -> abort "can't subtract larger number from smaller one" + in (h, d2c bb sLeft aa) + ] + in wrapper (# wrapper) + +-- aux = \x -> if dEqual x 8 then "Success" else "Failure" +-- main = \i -> (aux ((left Nat) 8), 0) + +-- main = \i -> ("hello", 0) diff --git a/examples.tel b/examples.tel index d7a2054..d37b40c 100644 --- a/examples.tel +++ b/examples.tel @@ -1,28 +1,46 @@ +import Prelude + -- File for small illustrative telomare programs and for testing -- Hello World example. -aux = "Hello" --- main = \input -> (aux, 0) -main = \input -> ("Hello", 0) +-- aux = "Hello" +-- -- main = \input -> (aux, 0) +-- main = \input -> ("Hello", 0) --- -- refinement fail +-- refinement fail -- main : (\x -> if x then "fail" else 0) = 1 +-- main : (\x -> assert 1 "fail") = 1 +-- main : (\x -> assert (not (left x)) "fail") = 1 + +-- main : (\x -> assert (not x) "fail") = 1 -- Ad hoc user defined types example: --- MyInt = let wrapper = \h -> ( \i -> if not i --- then abort "MyInt cannot be 0" --- else i --- , \i -> if dEqual (left i) h --- then 0 --- else abort "Not a MyInt" --- ) --- in wrapper (# wrapper) +MyInt = let wrapper = \h -> ( \i -> if not i + then abort "MyInt cannot be 0" + else i + , \i -> if dEqual (left i) h + then 0 + else abort "Not a MyInt" + ) + in wrapper (# wrapper) --- aux = \x -> if dEqual x 8 then "Success" else "Failure" --- main = \i -> (aux ((left MyInt) 8), 0) +aux = \x -> if dEqual x 8 then "Success" else "Failure" +main = \i -> (aux ((left MyInt) 8), 0) --- aux2 = [1,2,3] +-- [Nat, toNat, nPlus, nMinus] +-- = let wrapper = \h -> +-- let N = \(hc, _) x -> assert (dEqual hc h) "not Natural" +-- in [ N +-- , \x -> (h, x) +-- , \((_, aa) : N) ((_, bb) : N) -> (h, d2c aa succ bb) +-- , \((_, aa) : N) ((_, bb) : N) -> +-- let sLeft = \x -> case x of +-- (l, _) -> l +-- y -> abort "can't subtract larger number from smaller one" +-- in (h, d2c bb sLeft aa) +-- ] +-- in wrapper (# wrapper) -- something -- main = diff --git a/src/PrettyPrint.hs b/src/PrettyPrint.hs index ab7afe1..b71bfd2 100644 --- a/src/PrettyPrint.hs +++ b/src/PrettyPrint.hs @@ -327,61 +327,56 @@ newtype MultiLineShowUPT = MultiLineShowUPT UnprocessedParsedTerm instance Show MultiLineShowUPT where show (MultiLineShowUPT upt) = cata alg upt where alg :: Base UnprocessedParsedTerm String -> String + ind = indentSansFirstLine 2 alg = \case IntUPF i -> "IntUP " <> show i VarUPF str -> "VarUP " <> str - StringUPF str -> "StringUP" <> str - PairUPF x y -> "PairUP" <> "\n" <> - " (" <> indentSansFirstLine 3 x <> ")\n" <> - " (" <> indentSansFirstLine 3 y <> ")" - (ITEUPF x y z) -> "ITEUP" <> "\n" <> - " (" <> indentSansFirstLine 3 x <> ")\n" <> - " (" <> indentSansFirstLine 3 x <> ")\n" <> - " (" <> indentSansFirstLine 3 z <> ")" - (AppUPF x y) -> "AppUP" <> "\n" <> - " (" <> indentSansFirstLine 3 x <> ")\n" <> - " (" <> indentSansFirstLine 3 y <> ")" + StringUPF str -> "StringUP " <> show str + PairUPF x y -> "PairUP\n" <> + " " <> ind x <> "\n" <> + " " <> ind y + (ITEUPF x y z) -> "ITEUP\n" <> + " " <> ind x <> "\n" <> + " " <> ind y <> "\n" <> + " " <> ind z + (AppUPF x y) -> "AppUP\n" <> + " " <> ind x <> "\n" <> + " " <> ind y (LamUPF str y) -> "LamUP " <> str <> "\n" <> - " (" <> indentSansFirstLine 3 y <> ")" + " " <> ind y (ChurchUPF x) -> "ChurchUP " <> show x - (LeftUPF x) -> "LeftUP \n" <> - " (" <> indentSansFirstLine 3 x <> ")" - (RightUPF x) -> "RightUP \n" <> - " (" <> indentSansFirstLine 3 x <> ")" - (TraceUPF x) -> "TraceUP \n" <> - " (" <> indentSansFirstLine 3 x <> ")" - (UnsizedRecursionUPF x y z) -> "UnsizedRecursionUP" <> "\n" <> - " (" <> indentSansFirstLine 3 x <> ")\n" <> - " (" <> indentSansFirstLine 3 x <> ")\n" <> - " (" <> indentSansFirstLine 3 z <> ")" - (HashUPF x) -> "HashUP \n" <> - " (" <> indentSansFirstLine 3 x <> ")" - (CheckUPF x y) -> "CheckUP" <> "\n" <> - " (" <> indentSansFirstLine 3 x <> ")\n" <> - " (" <> indentSansFirstLine 3 y <> ")" + (LeftUPF x) -> "LeftUP\n" <> + " " <> ind x + (RightUPF x) -> "RightUP\n" <> + " " <> ind x + (TraceUPF x) -> "TraceUP\n" <> + " " <> ind x + (UnsizedRecursionUPF x y z) -> "UnsizedRecursionUP\n" <> + " " <> ind x <> "\n" <> + " " <> ind y <> "\n" <> + " " <> ind z + (HashUPF x) -> "HashUP\n" <> + " " <> ind x + (CheckUPF x y) -> "CheckUP\n" <> + " " <> ind x <> "\n" <> + " " <> ind y (ListUPF []) -> "ListUP []" (ListUPF [x]) -> "ListUP [" <> x <> "]" (ListUPF ls) -> "ListUP\n" <> - " [" <> drop 3 (unlines ((" " <>) . indentSansFirstLine 4 . (", " <>) <$> ls)) <> + concatMap (\x -> " , " <> ind x <> "\n") ls <> " ]" (LetUPF ls x) -> "LetUP\n" <> - " [ " <> drop 4 (unlines ( (" " <>) - . indentSansFirstLine 3 - . (", " <>) - . (\(x,y) -> "(" <> x <> ", " <> indentSansFirstLine (length x + 4) y <> ")") - <$> ls - )) <> + concatMap (\(n,v) -> " , (" <> n <> ", " <> ind v <> ")\n") ls <> " ]\n" <> - " (" <> indentSansFirstLine 3 x <> ")" + " " <> ind x (CaseUPF x ls) -> "CaseUP\n" <> - " (" <> indentSansFirstLine 3 x <> ")\n" <> - " [" <> drop 3 (unlines ( (" " <>) - . indentSansFirstLine 3 - . (", " <>) - . (\(x,y) -> "(" <> show x <> ", " <> indentSansFirstLine ((length . show $ x) + 4) y <> ")") - <$> ls - )) <> - " ]\n" + " " <> ind x <> "\n" <> + concatMap (\(p,v) -> " , (" <> show p <> ",\n " <> ind v <> ")\n") ls <> + " ]" + (BrandUPF ss x) -> "BrandUP " <> show ss <> "\n" <> + " " <> ind x + (ImportUPF s) -> "ImportUP " <> show s + (ImportQualifiedUPF s1 s2) -> "ImportQualifiedUP " <> show s1 <> " " <> show s2 newtype PrettyUPT = PrettyUPT UnprocessedParsedTerm diff --git a/src/Telomare.hs b/src/Telomare.hs index 15f3be3..c4d3ec4 100644 --- a/src/Telomare.hs +++ b/src/Telomare.hs @@ -1000,12 +1000,12 @@ convertAbortMessage = \case -- |AST for patterns in `case` expressions data Pattern = PatternVar String + | PatternAnnotated Pattern UnprocessedParsedTerm | PatternInt Int | PatternString String | PatternIgnore | PatternPair Pattern Pattern deriving (Show, Eq, Ord) -makeBaseFunctor ''Pattern -- |Firstly parsed AST sans location annotations data UnprocessedParsedTerm @@ -1025,6 +1025,7 @@ data UnprocessedParsedTerm | TraceUP UnprocessedParsedTerm | CheckUP UnprocessedParsedTerm UnprocessedParsedTerm | HashUP UnprocessedParsedTerm -- ^ On ad hoc user defined types, this term will be substitued to a unique Int. + | BrandUP [String] UnprocessedParsedTerm | CaseUP UnprocessedParsedTerm [(Pattern, UnprocessedParsedTerm)] -- TODO: check if adding this doesn't create partial functions | ImportQualifiedUP String String @@ -1033,6 +1034,8 @@ data UnprocessedParsedTerm makeBaseFunctor ''UnprocessedParsedTerm -- Functorial version UnprocessedParsedTerm makePrisms ''UnprocessedParsedTerm +makeBaseFunctor ''Pattern + instance Eq a => Eq (UnprocessedParsedTermF a) where (==) = eq1 @@ -1077,7 +1080,6 @@ instance Eq1 UnprocessedParsedTermF where mod1 == mod2 liftEq _ _ _ = False - instance (Show a) => Show (UnprocessedParsedTermF a) where show (VarUPF s) = "VarUPF " <> show s show (ITEUPF c t e) = "ITEUPF " <> show c <> " " <> show t <> " " <> show e @@ -1095,7 +1097,10 @@ instance (Show a) => Show (UnprocessedParsedTermF a) where show (TraceUPF x) = "TraceUPF " <> show x show (CheckUPF a b) = "CheckUPF " <> show a <> " " <> show b show (HashUPF x) = "HashUPF " <> show x + show (BrandUPF ss x) = "BrandUPF " <> show ss <> " " <> show x show (CaseUPF scrutinee patterns) = "CaseUPF " <> show scrutinee <> " " <> show patterns + show (ImportQualifiedUPF s1 s2) = "ImportQualifiedUPF " <> show s1 <> " " <> show s2 + show (ImportUPF s) = "ImportUPF " <> show s instance Show1 UnprocessedParsedTermF where liftShowsPrec showsPrecFunc showList d term = case term of @@ -1133,6 +1138,7 @@ instance Show1 UnprocessedParsedTermF where CheckUPF a b -> showString "CheckUPF " . showsPrecFunc 11 a . showChar ' ' . showsPrecFunc 11 b HashUPF x -> showString "HashUPF " . showsPrecFunc 11 x + BrandUPF ss x -> showString "BrandUPF " . shows ss . showChar ' ' . showsPrecFunc 11 x CaseUPF scrutinee patterns -> let showPattern (pat, x) = showChar '(' . shows pat . showString ", " . showsPrecFunc 11 x . showChar ')' diff --git a/src/Telomare/Parser.hs b/src/Telomare/Parser.hs index ac64ad2..1b7e8d1 100644 --- a/src/Telomare/Parser.hs +++ b/src/Telomare/Parser.hs @@ -1,12 +1,13 @@ {-# LANGUAGE LambdaCase #-} {-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TupleSections #-} {-# LANGUAGE TypeFamilies #-} module Telomare.Parser where import Control.Comonad.Cofree (Cofree (..), unwrap) import Control.Lens.Plated (Plated (..)) -import Control.Monad (void) +import Control.Monad (join, void) import Control.Monad.State (State) import Data.Bifunctor (Bifunctor (first, second), bimap) import Data.Functor (($>)) @@ -29,7 +30,7 @@ import Text.Megaparsec.Char (alphaNumChar, char, letterChar, space1, string) import qualified Text.Megaparsec.Char.Lexer as L import Text.Megaparsec.Debug (dbg) import Text.Megaparsec.Pos (Pos) -import Text.Read (readMaybe) +import Text.Read (readMaybe, Lexeme (String)) import Text.Show.Deriving (deriveShow1) type AnnotatedUPT = Cofree UnprocessedParsedTermF LocTag @@ -195,6 +196,14 @@ parseHash = do upt <- parseSingleExpr pure $ x :< HashUPF upt +parseBrand :: TelomareParser AnnotatedUPT +parseBrand = do + x <- getLineColumn + brandElements :: [String] <- scn *> brackets (commaSep (scn *> identifier <*scn)) <* scn + scn *> symbol "=" "brand assignment =" + expr <- scn *> parseLongExpr <* scn + pure $ x :< BrandUPF brandElements expr + parseCase :: TelomareParser AnnotatedUPT parseCase = do x <- getLineColumn @@ -214,6 +223,7 @@ parseSingleCase = do parsePattern :: TelomareParser Pattern parsePattern = choice $ try <$> [ parsePatternIgnore , parsePatternVar + , parsePatternAnnotated , parsePatternString , parsePatternInt , parsePatternPair @@ -233,11 +243,24 @@ parsePatternString :: TelomareParser Pattern parsePatternString = PatternString <$> (char '"' >> manyTill L.charLiteral (char '"')) parsePatternVar :: TelomareParser Pattern -parsePatternVar = PatternVar <$> identifier +parsePatternVar = do + var <- identifier <* scn + annotation <- optional . try $ parseRefinementCheck + case annotation of + Just annot -> pure $ PatternAnnotated (PatternVar var) (forget . annot $ DummyLoc :< VarUPF var) + _ -> pure $ PatternVar var + parsePatternIgnore :: TelomareParser Pattern parsePatternIgnore = symbol "_" >> pure PatternIgnore +parsePatternAnnotated :: TelomareParser Pattern +parsePatternAnnotated = parens $ do + p <- scn *> parsePattern <* scn + symbol ":" <* scn + typeExpr <- parseLongExpr <* scn + pure $ PatternAnnotated p (forget typeExpr) + -- |Parse a single expression. parseSingleExpr :: TelomareParser AnnotatedUPT parseSingleExpr = choice $ try <$> [ parseHash @@ -262,16 +285,50 @@ parseApplied = do pure $ foldl (\a b -> x :< AppUPF a b) f args _ -> fail "expected expression" +-- parseLambdaArgs :: TelomareParser [Pattern] +-- parseLambdaArgs = some parsePattern <* scn + +makeLambda :: LocTag -> Pattern -> AnnotatedUPT -> AnnotatedUPT +makeLambda lt p body = + case p of + PatternVar str -> lt :< LamUPF str body + PatternAnnotated innerPat _typeExpr -> + lt :< LamUPF varName + (lt :< CaseUPF (lt :< VarUPF varName) + [ (innerPat, body) + , (PatternIgnore, abort) + ]) + _ -> lt :< LamUPF varName + (lt :< CaseUPF (lt :< VarUPF varName) + [ (p, body) + , (PatternIgnore, abort) + ]) + where + varName = genPatternVarName p + abort = lt :< AppUPF + (lt :< VarUPF "abort") + (lt :< StringUPF "makeLambda: pattern not reached") + +genPatternVarName :: Pattern -> String +genPatternVarName = ("generatedVar" <>) + . filter (\x -> x /= '\"' + && x /= ' ' + && x /= '(' + && x /= ')' + && x /= '[' + && x /= ']') + . show + -- |Parse lambda expression. parseLambda :: TelomareParser AnnotatedUPT parseLambda = do x <- getLineColumn symbol "\\" <* scn - variables <- some identifier <* scn + variables <- some parsePattern <* scn + -- variables <- some identifier <* scn symbol "->" <* scn - -- TODO make sure lambda names don't collide with bound names term1expr <- parseLongExpr <* scn - pure $ foldr (\str upt -> x :< LamUPF str upt) term1expr variables + pure $ foldr (\p upt -> makeLambda x p upt) term1expr variables -- |Parser that fails if indent level is not `pos`. parseSameLvl :: Pos -> TelomareParser a -> TelomareParser a @@ -343,19 +400,54 @@ parseImportQualified = do qualifier <- identifier <* scn pure $ x :< ImportQualifiedUPF qualifier m +parseOneAssignmentOrBrand :: TelomareParser (String, AnnotatedUPT) +parseOneAssignmentOrBrand = + parseAssignment + <|> (("8@$temp_label$@8",) <$> parseBrand) + +-- |Parse assignment or Brands, and add adding binding to ParserState. +parseAssignmentsAndBrands :: TelomareParser [(String, AnnotatedUPT)] +parseAssignmentsAndBrands = do + tempBindingList :: [(String, AnnotatedUPT)] <- scn *> many parseOneAssignmentOrBrand <* eof + let removeBrands = \case + ("8@$temp_label$@8", exp) -> expandBrand exp + x -> [x] + pure (removeBrands =<< tempBindingList) + -- |Parse top level expressions. parseTopLevelWithExtraModuleBindings :: [(String, AnnotatedUPT)] -> TelomareParser AnnotatedUPT parseTopLevelWithExtraModuleBindings lst = do x <- getLineColumn - bindingList <- scn *> many parseAssignment <* eof + bindingList <- parseAssignmentsAndBrands pure $ x :< LetUPF (lst <> bindingList) (fromJust $ lookup "main" bindingList) -parseDefinitions :: TelomareParser (AnnotatedUPT -> AnnotatedUPT) -parseDefinitions = do - x <- getLineColumn - bindingList <- scn *> many parseAssignment <* eof - pure $ \y -> x :< LetUPF bindingList y +-- expandBrand :: UnprocessedParsedTerm -> [(String, UnprocessedParsedTerm)] +-- expandBrand = \case +-- BrandUP l exp -> undefined +-- _ -> [] + +expandBrand :: AnnotatedUPT -> [(String, AnnotatedUPT)] +expandBrand (loc :< term) = case term of + BrandUPF l exp -> zipWith (\name accessor -> (name, loc :< AppUPF (loc :< VarUPF accessor) exp)) l accessors + where + accessors = ["first", "second", "third", "fourth", "fifth", "sixth", "seventh", "eighth", "ninth", "tenth"] + _ -> [] + +-- expandBrand :: AnnotatedUPT -> [(String, AnnotatedUPT)] +-- expandBrand = \case +-- (_ :< BrandUPF l exp) -> undefined +-- _ -> [] +-- expandBrand = undefined where +-- interim :: AnnotatedUPT -> AnnotatedUPT +-- interim = \case +-- (anno :< BrandUPF l exp) -> undefined + +-- parseDefinitions :: TelomareParser (AnnotatedUPT -> AnnotatedUPT) +-- parseDefinitions = do +-- x <- getLineColumn +-- bindingList <- scn *> many parseAssignment <* eof +-- pure $ \y -> x :< LetUPF bindingList y -- |Helper function to test parsers without a result. runTelomareParser_ :: Show a => TelomareParser a -> String -> IO () @@ -386,7 +478,7 @@ runParseLongExpr str = bimap errorBundlePretty forget' $ runParser parseLongExpr forget' = forget parsePrelude :: String -> Either String [(String, AnnotatedUPT)] -parsePrelude str = let result = runParser (scn *> many parseAssignment <* eof) "" str +parsePrelude str = let result = runParser parseAssignmentsAndBrands "" str in first errorBundlePretty result parseImportOrAssignment :: TelomareParser (Either AnnotatedUPT (String, AnnotatedUPT)) @@ -395,7 +487,7 @@ parseImportOrAssignment = do maybeImport <- optional $ scn *> (try parseImportQualified <|> try parseImport) <* scn case maybeImport of Nothing -> do - maybeAssignment <- optional $ scn *> try parseAssignment <* scn + maybeAssignment <- optional $ scn *> try parseOneAssignmentOrBrand <* scn case maybeAssignment of Nothing -> fail "Expected either an import statement or an assignment" Just a -> pure $ Right a @@ -410,6 +502,40 @@ parseModule :: String -> Either String [Either AnnotatedUPT (String, AnnotatedUP parseModule str = let result = runParser (scn *> many parseImportOrAssignment <* eof) "" str in first errorBundlePretty result +aux :: String +aux = unlines + [ "[Nat, toNat, nPlus, nMinus]" + , " = let wrapper = \\h ->" + , " let N = \\(hc, _) x -> assert (dEqual hc h) \"not Natural\"" + , " in [ N" + , " , \\x -> (h, x)" + , " , \\((_, aa) : N) ((_, bb) : N) -> (h, d2c aa succ bb)" + , " , \\((_, aa) : N) ((_, bb) : N) ->" + , " let sLeft = \\x -> case x of" + , " (l, _) -> l" + , " y -> abort \"can't subtract larger number from smaller one\"" + , " in (h, d2c bb sLeft aa)" + , " ]" + , " in wrapper (# wrapper)" + ] + +aux1 :: String +aux1 = unlines + [ "let wrapper = \\h ->" + , " let N = \\(hc, _) x -> assert (dEqual hc h) \"not Natural\"" + , " in [ N" + , " , \\x -> (h, x)" + , " , \\((_, aa) : N) ((_, bb) : N) -> (h, d2c aa succ bb)" + , " , \\((_, aa) : N) ((_, bb) : N) ->" + , " let sLeft = \\x -> case x of" + , " (l, _) -> l" + , " y -> abort \"can't subtract larger number from smaller one\"" + , " in (h, d2c bb sLeft aa)" + , " ]" + , "in wrapper (# wrapper)" + ] + + -- |Parse either a single expression or top level definitions defaulting to the `main` definition. -- This function was made for telomare-evaluare parseOneExprOrTopLevelDefs :: [(String, AnnotatedUPT)] -> TelomareParser AnnotatedUPT diff --git a/src/Telomare/Resolver.hs b/src/Telomare/Resolver.hs index 49c1d35..112145a 100644 --- a/src/Telomare/Resolver.hs +++ b/src/Telomare/Resolver.hs @@ -159,11 +159,12 @@ pattern2UPT :: LocTag -> Pattern -> AnnotatedUPT pattern2UPT anno = tag anno . cata alg where alg :: Base Pattern UnprocessedParsedTerm -> UnprocessedParsedTerm alg = \case - PatternPairF x y -> PairUP x y - PatternIntF i -> IntUP i - PatternStringF str -> StringUP str - PatternVarF str -> IntUP 0 - PatternIgnoreF -> IntUP 0 + PatternPairF x y -> PairUP x y + PatternIntF i -> IntUP i + PatternStringF str -> StringUP str + PatternVarF str -> IntUP 0 + PatternIgnoreF -> IntUP 0 + PatternAnnotatedF x _ -> x -- Note that "__ignore" is a special variable name and not accessible to users because -- parsing of VarUPs doesn't allow variable names to start with `_` @@ -334,15 +335,21 @@ validateVariables term = [(name, Set.fromList $ getDirectDeps def) | (name, def) <- preludeMap] -- Get direct variable dependencies (only those defined in this let block) + -- Uses Set to properly handle lambda-bound variable shadowing + letBindingNames = Set.fromList (fmap fst preludeMap) getDirectDeps :: AnnotatedUPT -> [String] - getDirectDeps = cata alg where - alg :: CofreeF UnprocessedParsedTermF LocTag [String] -> [String] + getDirectDeps = Set.toList . cata alg where + alg :: CofreeF UnprocessedParsedTermF LocTag (Set String) -> Set String alg = \case - (_ C.:< VarUPF n) -> [n | any ((== n) . fst) preludeMap] - (_ C.:< LamUPF _ body) -> body + (_ C.:< VarUPF n) -> if Set.member n letBindingNames then Set.singleton n else Set.empty + (_ C.:< LamUPF v body) -> Set.delete v body + (_ C.:< LetUPF binds body) -> + let boundNames = Set.fromList (fmap fst binds) + bindDeps = foldMap snd binds + in Set.union (bindDeps Set.\\ boundNames) (body Set.\\ boundNames) (_ C.:< ITEUPF i t e) -> i <> t <> e (_ C.:< PairUPF a b) -> a <> b - (_ C.:< ListUPF l) -> concat l + (_ C.:< ListUPF l) -> foldMap id l (_ C.:< AppUPF f x) -> f <> x (_ C.:< UnsizedRecursionUPF t r b) -> t <> r <> b (_ C.:< LeftUPF x) -> x @@ -350,7 +357,7 @@ validateVariables term = (_ C.:< TraceUPF x) -> x (_ C.:< CheckUPF cf x) -> cf <> x (_ C.:< HashUPF x) -> x - _ -> [] + _ -> Set.empty -- Check if original order works (no forward references) let originalOrder = fmap fst preludeMap