cubical/Main.hs at master · simhu/cubical · GitHub

Repository navigation

History

100

101

102

103

104

105

106

107

108

109

110

111

112

113

114

115

116

117

118

119

120

121

122

123

124

125

126

127

128

129

130

131

132

133

134

135

136

137

138

139

140

141

142

143

144

145

146

147

148

149

150

151

152

153

154

155

156

157

158

159

160

161

162

163

164

165

166

167

module Main where

import Control.Monad.Trans.Reader

import Control.Monad.Error

import Data.List

import System.Directory

import System.FilePath

import System.Environment

import System.Console.GetOpt

import System.Console.Haskeline

import Exp.Lex

import Exp.Par

import Exp.Print

import Exp.Abs

import Exp.Layout

import Exp.ErrM

import Concrete

import qualified TypeChecker as TC

import qualified CTT as C

import qualified Eval as E

type Interpreter a = InputT IO a

-- Flag handling

data Flag = Help | Version

deriving (Eq,Show)

options :: [OptDescr Flag]

options = [ Option "" ["help"] (NoArg Help) "print help"

, Option "" ["version"] (NoArg Version) "print version number" ]

-- Version number, welcome message, usage and prompt strings

version, welcome, usage, prompt :: String

version = "0.2.0"

welcome = "cubical, version: " ++ version ++ " (:h for help)\n"

usage = "Usage: cubical [options] <file.cub>\nOptions:"

prompt = "> "

lexer :: String -> [Token]

lexer = resolveLayout True . myLexer

showTree :: (Show a, Print a) => a -> IO ()

showTree tree = do

putStrLn $ "\n[Abstract Syntax]\n\n" ++ show tree

putStrLn $ "\n[Linearized tree]\n\n" ++ printTree tree

-- Used for auto completion

searchFunc :: [String] -> String -> [Completion]

searchFunc ns str = map simpleCompletion $ filter (str `isPrefixOf`) ns

settings :: [String] -> Settings IO

settings ns = Settings

{ historyFile = Nothing

, complete = completeWord Nothing " \t" $ return . searchFunc ns

, autoAddHistory = True }

main :: IO ()

main = do

args <- getArgs

case getOpt Permute options args of

(flags,files,[])

| Help `elem` flags -> putStrLn $ usageInfo usage options

| Version `elem` flags -> putStrLn version

| otherwise -> case files of

[] -> do

putStrLn welcome

runInputT (settings []) (loop flags [] [] TC.verboseEnv)

[f] -> do

putStrLn welcome

putStrLn $ "Loading " ++ show f

initLoop flags f

_ -> putStrLn $ "Input error: zero or one file expected\n\n" ++

usageInfo usage options

(_,_,errs) -> putStrLn $ "Input error: " ++ concat errs ++ "\n" ++

usageInfo usage options

-- Initialize the main loop

initLoop :: [Flag] -> FilePath -> IO ()

initLoop flags f = do

-- Parse and type-check files

(_,_,mods) <- imports True ([],[],[]) f

-- Translate to CTT

let res = runResolver $ resolveModules mods

case res of

Left err -> do

putStrLn $ "Resolver failed: " ++ err

runInputT (settings []) (loop flags f [] TC.verboseEnv)

Right (adefs,names) -> do

(merr,tenv) <- TC.runDeclss TC.verboseEnv adefs

case merr of

Just err -> putStrLn $ "Type checking failed: " ++ err

Nothing -> return ()

putStrLn "File loaded."

-- Compute names for auto completion

runInputT (settings [n | ((n,_),_) <- names]) (loop flags f names tenv)

-- The main loop

loop :: [Flag] -> FilePath -> [(C.Binder,SymKind)] -> TC.TEnv -> Interpreter ()

loop flags f names tenv@(TC.TEnv _ rho _ _) = do

input <- getInputLine prompt

case input of

Nothing -> outputStrLn help >> loop flags f names tenv

Just ":q" -> return ()

Just ":r" -> lift $ initLoop flags f

Just (':':'l':' ':str)

| ' ' `elem` str -> do outputStrLn "Only one file allowed after :l"

loop flags f names tenv

| otherwise -> lift $ initLoop flags str

Just (':':'c':'d':' ':str) -> do lift (setCurrentDirectory str)

loop flags f names tenv

Just ":h" -> outputStrLn help >> loop flags f names tenv

Just str -> case pExp (lexer str) of

Bad err -> outputStrLn ("Parse error: " ++ err) >> loop flags f names tenv

Ok exp ->

case runResolver $ local (insertBinders names) $ resolveExp exp of

Left err -> do outputStrLn ("Resolver failed: " ++ err)

loop flags f names tenv

Right body -> do

x <- liftIO $ TC.runInfer tenv body

case x of

Left err -> do outputStrLn ("Could not type-check: " ++ err)

loop flags f names tenv

Right _ -> do

let e = E.eval rho body

outputStrLn ("EVAL: " ++ show e)

loop flags f names tenv

-- (not ok,loaded,already loaded defs) -> to load ->

-- (new not ok, new loaded, new defs)

-- the bool determines if it should be verbose or not

imports :: Bool -> ([String],[String],[Module]) -> String ->

IO ([String],[String],[Module])

imports v st@(notok,loaded,mods) f

| f `elem` notok = putStrLn ("Looping imports in " ++ f) >> return ([],[],[])

| f `elem` loaded = return st

| otherwise = do

b <- doesFileExist f

let prefix = dropFileName f

if not b

then putStrLn (f ++ " does not exist") >> return ([],[],[])

else do

s <- readFile f

let ts = lexer s

case pModule ts of

Bad s -> do

putStrLn $ "Parse failed in " ++ show f ++ "\n" ++ show s

return ([],[],[])

Ok mod@(Module id imp decls) ->

let name = unAIdent id

imp_cub = [prefix ++ unAIdent i ++ ".cub" | Import i <- imp]

in do

when (name /= dropExtension (takeFileName f)) $

error $ "Module name mismatch " ++ show (f,name)

(notok1,loaded1,mods1) <-

foldM (imports v) (f:notok,loaded,mods) imp_cub

when v $ putStrLn $ "Parsed " ++ show f ++ " successfully!"

return (notok,f:loaded1,mods1 ++ [mod])

help :: String

help = "\nAvailable commands:\n" ++

" <statement> infer type and evaluate statement\n" ++

" :q quit\n" ++

" :l <filename> loads filename (and resets environment before)\n" ++

" :cd <path> change directory to path\n" ++

" :r reload\n" ++

" :h display this message\n"

cubical/Main.hs at master · simhu/cubical · GitHub

Repository navigation

Expand file tree

Breadcrumbs

Main.hs

Latest commit

History

Breadcrumbs

Main.hs

File metadata and controls