User Defined Types

.github/workflows/telomare-ci.yml

@@ -8,8 +8,11 @@ jobs:
     runs-on: ubuntu-latest
     steps:
     - uses: actions/checkout@v4
+      with:
+        fetch-depth: 0
     - uses: cachix/install-nix-action@v25
       with:
+        install_url: https://releases.nixos.org/nix/nix-2.31.5/install
         nix_path: nixpkgs=channel:nixos-unstable
         extra_nix_config: |
           access-tokens = github.com=${{ secrets.GITHUB_TOKEN }}
@@ -46,8 +49,11 @@ jobs:
     steps:
       - name: Checkout telomare repository
         uses: actions/checkout@v4
+        with:
+          fetch-depth: 0
       - uses: cachix/install-nix-action@v25
         with:
+          install_url: https://releases.nixos.org/nix/nix-2.31.5/install
           extra_nix_config: |
             access-tokens = github.com=${{ secrets.GITHUB_TOKEN }}
       - uses: DeterminateSystems/magic-nix-cache-action@v2
@@ -72,8 +78,11 @@ jobs:
     steps:
       - name: Checkout telomare repository
         uses: actions/checkout@v4
+        with:
+          fetch-depth: 0
       - uses: cachix/install-nix-action@v25
         with:
+          install_url: https://releases.nixos.org/nix/nix-2.31.5/install
           extra_nix_config: |
             access-tokens = github.com=${{ secrets.GITHUB_TOKEN }}
       - uses: DeterminateSystems/magic-nix-cache-action@v2
@@ -103,14 +112,17 @@ jobs:
           repository: Stand-In-Language/stand-in-language
           token: ${{ secrets.API_TOKEN_GITHUB }}
           path: ./telomare
+          fetch-depth: 0
       - name: Checkout telomare site repository
         uses: actions/checkout@v4
         with:
           repository: Stand-In-Language/stand-in-language.github.io
           token: ${{ secrets.API_TOKEN_GITHUB }}
           path: ./stand-in-language.github.io
+          fetch-depth: 0
       - uses: cachix/install-nix-action@v25
         with:
+          install_url: https://releases.nixos.org/nix/nix-2.31.5/install
           extra_nix_config: |
             access-tokens = github.com=${{ secrets.GITHUB_TOKEN }}
       - uses: DeterminateSystems/magic-nix-cache-action@v2

Prelude.tel

@@ -142,57 +142,45 @@ gcd = \a b ->
 
 lcm = \a b -> dDiv (dTimes a b) (gcd a b)
 
-Rational =
-  let wrapper = \h -> (
-        \n d -> if dEqual d 0
-                then abort "Denominator cannot be zero"
-                else
-                  let g   = gcd n d
-                      num = dDiv n g
-                      den = dDiv d g
-                  in (h, (num, den))
-      , \i -> if dEqual (left i) h
-              then right i
-              else abort "Not a Rational"
-      )
-  in wrapper (# wrapper)
-
-toRational = right Rational
-
-fromRational = left Rational
-
-rPlus = \a b ->
-  let n1 = left (right a)
-      d1 = right (right a)
-      n2 = left (right b)
-      d2 = right (right b)
-      num = dPlus (dTimes n1 d2) (dTimes n2 d1)
-      den = dTimes d1 d2
-  in fromRational num den
-
-rTimes = \a b ->
-  let n1 = left (right a)
-      d1 = right (right a)
-      n2 = left (right b)
-      d2 = right (right b)
-      num = dTimes n1 n2
-      den = dTimes d1 d2
-  in fromRational num den
-
-rMinus = \a b ->
-  let n1 = left (right a)
-      d1 = right (right a)
-      n2 = left (right b)
-      d2 = right (right b)
-      num = dMinus (dTimes n1 d2) (dTimes n2 d1)
-      den = dTimes d1 d2
-  in fromRational num den
-
-rDiv = \a b ->
-  let n1 = left (right a)
-      d1 = right (right a)
-      n2 = left (right b)
-      d2 = right (right b)
-      num = dTimes n1 d2
-      den = dTimes d1 n2
-  in fromRational num den
+[Rational, fromRational, toRational, rPlus, rTimes, rMinus, rDiv] = \h ->
+  [ \n d -> if dEqual d 0
+            then abort "Denominator cannot be zero"
+            else
+              let g   = gcd n d
+                  num = dDiv n g
+                  den = dDiv d g
+              in (h, (num, den))
+  , \i -> Rational i
+  , \a b ->
+      let n1 = left (right a)
+          d1 = right (right a)
+          n2 = left (right b)
+          d2 = right (right b)
+          num = dPlus (dTimes n1 d2) (dTimes n2 d1)
+          den = dTimes d1 d2
+      in fromRational num den
+  , \a b ->
+      let n1 = left (right a)
+          d1 = right (right a)
+          n2 = left (right b)
+          d2 = right (right b)
+          num = dTimes n1 n2
+          den = dTimes d1 d2
+      in fromRational num den
+  , \a b ->
+      let n1 = left (right a)
+          d1 = right (right a)
+          n2 = left (right b)
+          d2 = right (right b)
+          num = dMinus (dTimes n1 d2) (dTimes n2 d1)
+          den = dTimes d1 d2
+      in fromRational num den
+  , \a b ->
+      let n1 = left (right a)
+          d1 = right (right a)
+          n2 = left (right b)
+          d2 = right (right b)
+          num = dTimes n1 d2
+          den = dTimes d1 n2
+      in fromRational num den
+  ]

app/Evaluare.hs

@@ -1,3 +1,5 @@
+{-# LANGUAGE RecursiveDo #-}
+
 module Main where
 
 import Control.Comonad.Cofree (Cofree ((:<)))
@@ -164,16 +166,29 @@ nodify = removeExtraNumbers . fmap go . allNodes 0 where
 loadModules :: [String] -> IO [(String, [Either AnnotatedUPT (String, AnnotatedUPT)])]
 loadModules filenames = do
   filesStrings :: [String] <- mapM Strict.readFile filenames
-  case sequence $ parseModule <$> filesStrings of
+  case mapM parseModule filesStrings of
     Right p -> pure $ zip filesStrings p
     Left pe -> error pe
 
+mainWidgetInit
+  :: (forall t m.
+       ( MonadVtyApp t m
+       , HasImageWriter t m
+       , MonadNodeId m
+       , HasDisplayRegion t m
+       , HasFocusReader t m
+       , HasTheme t m
+       , HasInput t m
+       ) => Layout t (Focus t m) (Event t ()))
+  -> IO ()
+mainWidgetInit w = mainWidget (initManager_ w)
+
 main :: IO ()
 main = do
   modules :: [(String, [Either AnnotatedUPT (String, AnnotatedUPT)])] <- getArgs >>= loadModules
   let go :: Text -> IO ()
       go textErr =
-        mainWidget $ initManager_ $ do
+        mainWidgetInit $ do
           let cfg = def
                 { _textInputConfig_initialValue = TZ.fromText . T.pack . unlines $
                     [ "-- Example:"
@@ -185,14 +200,14 @@ main = do
               escOrCtrlcQuit :: (Monad m, HasInput t m, Reflex t) => m (Event t ())
               escOrCtrlcQuit = do
                 inp <- input
-                pure $ fforMaybe inp $ \case
+                pure . fforMaybe inp $ \case
                   V.EvKey (V.KChar 'c') [V.MCtrl] -> Just ()
                   V.EvKey V.KEsc []               -> Just ()
                   _                               -> Nothing
           getout <- escOrCtrlcQuit
           tile flex . box (pure roundedBoxStyle) . row $ do
             rec
-              eEitherIExpr :: Event t (Either String IExpr) <- grout flex $ col $ do
+              eEitherIExpr :: Event t (Either String IExpr) <- grout flex . col $ do
                 telomareTextInput :: TextInput t <- grout flex textBox
                 pure . updated $ TE.eval2IExpr modules . T.unpack <$> _textInput_value telomareTextInput
               grout (fixed 2) . col . text $ ""

app/Main.hs

@@ -2,10 +2,9 @@
 
 module Main where
 
+import Data.Maybe (mapMaybe)
 import qualified Options.Applicative as O
-import System.Directory (listDirectory)
-import System.FilePath (takeBaseName, takeExtension)
-import qualified System.IO.Strict as Strict
+import System.FilePath (takeBaseName)
 import Telomare.Eval (runMain)
 
 newtype TelomareOpts
@@ -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` fmap 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

examples.tel

@@ -1,35 +1,38 @@
+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)
-
--- aux = \x -> if dEqual x 8 then "Success" else "Failure"
--- main = \i -> (aux ((left MyInt) 8), 0)
-
--- aux2 = [1,2,3]
-
--- something
--- main =
---   let toCase = (("a string", 99),(8,"pattern-match"))
---       caseTest =
---         case toCase of
---           (0,(8,2)) -> "Failure 1"
---           ("a string",(8,x)) -> concat [x, " failure 2"]
---           (("a string", 99),(8,x)) -> concat [x, " success with ints, strings and variables"]
---   in \input -> (caseTest, 0)
+-- Plain list assignments bind multiple names from a list-shaped value:
+-- [leftName, rightName] = ["left", "right"]
+-- [keep, drop] = \x -> [\_ -> x, \z -> z]
+
+[MyInt, mkMyInt, unMyInt] = \h ->
+  [ \i -> if not i
+          then abort "MyInt cannot be 0"
+          else (h, i)
+  , \(i : MyInt) -> i
+  ]
+
+aux = \x -> if dEqual x 8 then "Success" else "Failure"
+main = \i -> (aux (unMyInt (mkMyInt 8)), 0)
+
+-- User-defined type example used by the test suite:
+--   [Nat, toNat, nPlus, nMinus] = \h ->
+--     [ \x -> (h, x)
+--     , \(aa : Nat) (bb : Nat) -> (h, d2c aa succ bb)
+--     , \(aa : Nat) (bb : Nat) -> ...
+--     ]