Parse Brands DO NOT MERGE

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)))))))))

app/Evaluare.hs

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

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,21 +15,34 @@ 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
   let opts = O.info (telomareOpts O.<**> O.helper)
         ( 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

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)

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)

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 =

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
 

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 ')'