New lambdas don't break everything now

Author: hhefesto

app/Evaluare.hs

@@ -1,3 +1,5 @@
+{-# LANGUAGE RecursiveDo #-}
+
 module Main where
 
 import Control.Comonad.Cofree (Cofree ((:<)))

examples.tel

@@ -7,22 +7,40 @@ import Prelude
 -- -- 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)
-
-aux = \x -> if dEqual x 0 then "Success" else "Failure"
-main = \i -> (aux ((left MyInt) 0), 0)
+-- 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)
+
+-- [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 =

src/Telomare.hs

@@ -1000,12 +1000,12 @@ convertAbortMessage = \case
 -- |AST for patterns in `case` expressions
 data Pattern
   = PatternVar String
+  | PatternVarAnnotated UnprocessedParsedTerm String
   | PatternInt Int
   | PatternString String
   | PatternIgnore
   | PatternPair Pattern Pattern
   deriving (Show, Eq, Ord)
-makeBaseFunctor ''Pattern
 
 -- |Firstly parsed AST sans location annotations
 data UnprocessedParsedTerm
@@ -1034,6 +1034,8 @@ data UnprocessedParsedTerm
 makeBaseFunctor ''UnprocessedParsedTerm -- Functorial version UnprocessedParsedTerm
 makePrisms ''UnprocessedParsedTerm
 
+makeBaseFunctor ''Pattern
+
 instance Eq a => Eq (UnprocessedParsedTermF a) where
   (==) = eq1
 
@@ -1078,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

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, join)
+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
@@ -198,7 +199,7 @@ parseHash = do
 parseBrand :: TelomareParser AnnotatedUPT
 parseBrand = do
   x <- getLineColumn
-  brandElements :: [String] <- brackets (commaSep (scn *> identifier <*scn))
+  brandElements :: [String] <- scn *> brackets (commaSep (scn *> identifier <*scn)) <* scn
   scn *> symbol "=" <?> "brand assignment ="
   expr <- scn *> parseLongExpr <* scn
   pure $ x :< BrandUPF brandElements expr
@@ -241,7 +242,13 @@ 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 $ PatternVarAnnotated (forget . annot $ DummyLoc :< VarUPF var) var
+    _          -> pure $ PatternVar var
+
 
 parsePatternIgnore :: TelomareParser Pattern
 parsePatternIgnore = symbol "_" >> pure PatternIgnore
@@ -270,16 +277,44 @@ 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
+    _ -> 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
@@ -354,7 +389,7 @@ parseImportQualified = do
 parseOneAssignmentOrBrand :: TelomareParser (String, AnnotatedUPT)
 parseOneAssignmentOrBrand =
   parseAssignment
-    <|> ((\exp -> ("8@$temp_label$@8", exp)) <$> parseBrand)
+    <|> (("8@$temp_label$@8",) <$> parseBrand)
 
 -- |Parse assignment or Brands, and add adding binding to ParserState.
 parseAssignmentsAndBrands :: TelomareParser [(String, AnnotatedUPT)]
@@ -363,7 +398,7 @@ parseAssignmentsAndBrands = do
   let removeBrands = \case
         ("8@$temp_label$@8", exp) -> expandBrand exp
         x -> [x]
-  pure . join $  removeBrands <$> tempBindingList
+  pure (removeBrands =<< tempBindingList)
 
 -- |Parse top level expressions.
 parseTopLevelWithExtraModuleBindings :: [(String, AnnotatedUPT)]
@@ -453,6 +488,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