elsa 0.2.0.0 → 0.2.0.1

raw patch · 4 files changed

+30/−17 lines, 4 files

Files

elsa.cabal +1/−1
src/Language/Elsa/Eval.hs +6/−4
src/Language/Elsa/Runner.hs +22/−11
src/Language/Elsa/Utils.hs +1/−1

elsa.cabal view

@@ -1,5 +1,5 @@ name:                elsa-version:             0.2.0.0+version:             0.2.0.1 synopsis:            A tiny language for understanding the lambda-calculus description:         elsa is a small proof checker for verifying sequences of                      reductions of lambda-calculus terms. The goal is to help

src/Language/Elsa/Eval.hs view

@@ -171,18 +171,20 @@ beta _                    _   = Nothing  substCA :: Expr a -> Id -> Expr a -> Maybe (Expr a)-substCA e x e' = go [] e+substCA e x e'           = go [] e   where     zs                   = freeVars e'-    bnd bs zs            = or [ b `isIn` zs | b <- bs ]+    bnd  bs zs           = or [ b `isIn` zs | b <- bs ]     go bs e@(EVar y _)       | y /= x           = Just e            -- different var, no subst-      | bnd bs zs        = Nothing           -- same var, but free-var-captured+      | bnd  bs zs       = Nothing           -- same var, but free-var-captured       | otherwise        = Just e'           -- same var, but no capture     go bs (EApp e1 e2 l) = do e1' <- go bs e1                               e2' <- go bs e2                               Just (EApp e1' e2' l)-    go bs (ELam b e1  l) = do e1' <- go (b:bs) e1+    go bs e@(ELam b e1  l)+      | x == bindId b    = Just e            -- subst-var has been rebound+      | otherwise        = do e1' <- go (b:bs) e1                               Just (ELam b e1' l)  isIn :: Bind a -> S.HashSet Id -> Bool

src/Language/Elsa/Runner.hs view

@@ -15,6 +15,7 @@ import System.Environment   (getArgs) import System.FilePath import System.Directory+import System.Timeout import Language.Elsa.Parser import Language.Elsa.Types import Language.Elsa.UX@@ -24,8 +25,26 @@ topMain = do   (m, f) <- getSrcFile   s      <- readFile f-  runElsa m f s `catch` exitErrors m f+  res    <- timeout (timeLimit * 10 ^ 6) (runElsa m f s `catch` exitErrors m f)+  case res of+    Just z  -> return z+    Nothing -> putStrLn timeMsg >> exitFailure +timeLimit :: Int+timeLimit = 10++timeMsg :: String+timeMsg = "Timed out after " ++ show timeLimit ++ " seconds."++getSrcFile :: IO (Mode, Text)+getSrcFile = do+  args <- getArgs+  case args of+    ["--json"  , f] -> return (Json,    f)+    ["--server", f] -> return (Server,  f)+    [f]             -> return (Cmdline, f)+    _               -> error "Please run with a single file as input"+ exitErrors :: Mode -> FilePath -> [UserError] -> IO () exitErrors mode f es = esHandle mode (modeWriter mode f) resultExit es @@ -46,7 +65,9 @@                             jsonDir  = takeDirectory f </> ".elsa"                             jsonFile = jsonDir </> addExtension (takeFileName f) ".json" +--------------------------------------------------------------------------------------------------------- runElsa :: Mode -> FilePath -> Text -> IO ()+--------------------------------------------------------------------------------------------------------- runElsa mode f s = do   let rs = elsa (parse f s)   let es = mapMaybe resultError rs@@ -54,16 +75,6 @@   exitErrors mode f es  okMessage rs = "OK " ++ intercalate ", " (successes rs) ++ "."--getSrcFile :: IO (Mode, Text)-getSrcFile = do-  args <- getArgs-  case args of-    ["--json"  , f] -> return (Json,    f)-    ["--server", f] -> return (Server,  f)-    [f]             -> return (Cmdline, f)-    _               -> error "Please run with a single file as input"-  -------------------------------------------------------------------------------- runElsaId :: FilePath -> Id -> IO (Maybe (Result ()))

src/Language/Elsa/Utils.hs view

@@ -40,7 +40,7 @@ traceShow msg x   | False   = trace (printf "TRACE: %s = %s" msg (show x)) x-  | otherwise +  | otherwise   = x  safeHead :: a -> [a] -> a