mirror of
https://github.com/edwinb/Idris2-boot.git
synced 2024-09-11 16:05:51 +03:00
More progress on TTCs
Added Core.Directory (more or less directly from Blodwen) and now writing out TTCs from the test Main, but it's still not writing out definitions because we're not yet making a note of the names which need saving (this will be the defined names and any holes introduced). Also it's clear from logging that holes/guess/constraints aren't being cleared so this needs to be fixed next.
This commit is contained in:
parent
bc26d74f9b
commit
a48d90f821
@ -117,13 +117,18 @@ readTTCFile modns as r b
|
||||
importHashes <- fromBuf r b
|
||||
-- Read in name map, update 'r'
|
||||
r <- readNameMap r b
|
||||
coreLift $ putStrLn "Read name map"
|
||||
defs <- get Ctxt
|
||||
gam' <- updateEntries (gamma defs) modns as 0 (max r) r
|
||||
setCtxt gam'
|
||||
holes <- fromBuf r b
|
||||
coreLift $ putStrLn $ "Read " ++ show (length holes) ++ " holes"
|
||||
guesses <- fromBuf r b
|
||||
constraints <- fromBuf r b
|
||||
coreLift $ putStrLn $ "Read " ++ show (length guesses) ++ "guesses"
|
||||
constraints <- the (Core (List (Int, Constraint))) $ fromBuf r b
|
||||
coreLift $ putStrLn $ "Read " ++ show (length constraints) ++ "constraints"
|
||||
defs <- fromBuf r b
|
||||
coreLift $ putStrLn ("Read defs of " ++ show (map fullname defs))
|
||||
imp <- fromBuf r b
|
||||
cns <- fromBuf r b
|
||||
ex <- fromBuf r b
|
||||
|
@ -354,6 +354,7 @@ TTC GlobalDef where
|
||||
|
||||
fromBuf r b
|
||||
= do loc <- fromBuf r b; name <- fromBuf r b
|
||||
coreLift $ putStrLn $ "Read " ++ show name
|
||||
ty <- fromBuf r b; mul <- fromBuf r b
|
||||
vis <- fromBuf r b; fl <- fromBuf r b
|
||||
def <- fromBuf r b
|
||||
@ -397,6 +398,14 @@ export
|
||||
getSave : Defs -> List Name
|
||||
getSave = map Basics.fst . toList . toSave
|
||||
|
||||
-- Note that the name should be saved when writing out a .ttc
|
||||
export
|
||||
addToSave : {auto c : Ref Ctxt Defs} ->
|
||||
Name -> Core ()
|
||||
addToSave n
|
||||
= do defs <- get Ctxt
|
||||
put Ctxt (record { toSave $= insert n } defs)
|
||||
|
||||
-- Label for context references
|
||||
export
|
||||
data Ctxt : Type where
|
||||
@ -566,6 +575,53 @@ toFullNames tm
|
||||
= pure (TForce fc !(full gam x))
|
||||
full gam tm = pure tm
|
||||
|
||||
-- Getting and setting various options
|
||||
|
||||
export
|
||||
getPPrint : {auto c : Ref Ctxt Defs} ->
|
||||
Core PPrinter
|
||||
getPPrint
|
||||
= do defs <- get Ctxt
|
||||
pure (printing (options defs))
|
||||
|
||||
export
|
||||
getDirs : {auto c : Ref Ctxt Defs} -> Core Dirs
|
||||
getDirs
|
||||
= do defs <- get Ctxt
|
||||
pure (dirs (options defs))
|
||||
|
||||
export
|
||||
addExtraDir : {auto c : Ref Ctxt Defs} -> String -> Core ()
|
||||
addExtraDir dir
|
||||
= do defs <- get Ctxt
|
||||
put Ctxt (record { options->dirs->extra_dirs $= (++ [dir]) } defs)
|
||||
|
||||
export
|
||||
addDataDir : {auto c : Ref Ctxt Defs} -> String -> Core ()
|
||||
addDataDir dir
|
||||
= do defs <- get Ctxt
|
||||
put Ctxt (record { options->dirs->data_dirs $= (++ [dir]) } defs)
|
||||
|
||||
export
|
||||
setBuildDir : {auto c : Ref Ctxt Defs} -> String -> Core ()
|
||||
setBuildDir dir
|
||||
= do defs <- get Ctxt
|
||||
put Ctxt (record { options->dirs->build_dir = dir } defs)
|
||||
|
||||
export
|
||||
setWorkingDir : {auto c : Ref Ctxt Defs} -> String -> Core ()
|
||||
setWorkingDir dir
|
||||
= do defs <- get Ctxt
|
||||
coreLift $ changeDir dir
|
||||
cdir <- coreLift $ currentDir
|
||||
put Ctxt (record { options->dirs->working_dir = cdir } defs)
|
||||
|
||||
export
|
||||
setPrefix : {auto c : Ref Ctxt Defs} -> String -> Core ()
|
||||
setPrefix dir
|
||||
= do defs <- get Ctxt
|
||||
put Ctxt (record { options->dirs->dir_prefix = dir } defs)
|
||||
|
||||
-- Log message with a term, translating back to human readable names first
|
||||
export
|
||||
logTerm : {auto c : Ref Ctxt Defs} ->
|
||||
|
158
src/Core/Directory.idr
Normal file
158
src/Core/Directory.idr
Normal file
@ -0,0 +1,158 @@
|
||||
module Core.Directory
|
||||
|
||||
import Core.Context
|
||||
import Core.Core
|
||||
import Core.FC
|
||||
import Core.Name
|
||||
import Core.Options
|
||||
|
||||
import System.Info
|
||||
|
||||
%default total
|
||||
|
||||
isWindows : Bool
|
||||
isWindows = os `elem` ["win32", "mingw32", "cygwin32"]
|
||||
|
||||
sep : Char
|
||||
sep = if isWindows then '\\' else '/'
|
||||
|
||||
export
|
||||
dirSep : String
|
||||
dirSep = cast sep
|
||||
|
||||
fullPath : String -> List String
|
||||
fullPath fp = filter (/="") $ split (==sep) fp
|
||||
|
||||
dropExtension : String -> String
|
||||
dropExtension fname
|
||||
= case span (/= '.') (reverse fname) of
|
||||
(all, "") => -- no extension
|
||||
reverse all
|
||||
(ext, root) =>
|
||||
-- assert that root can't be empty
|
||||
reverse (assert_total (strTail root))
|
||||
|
||||
-- Return the contents of the first file available in the list
|
||||
firstAvailable : List String -> Core (Maybe String)
|
||||
firstAvailable [] = pure Nothing
|
||||
firstAvailable (f :: fs)
|
||||
= do Right ok <- coreLift $ openFile f Read
|
||||
| Left err => firstAvailable fs
|
||||
coreLift $ closeFile ok
|
||||
pure (Just f)
|
||||
|
||||
export
|
||||
readDataFile : {auto c : Ref Ctxt Defs} ->
|
||||
String -> Core String
|
||||
readDataFile fname
|
||||
= do d <- getDirs
|
||||
let fs = map (\p => p ++ cast sep ++ fname) (data_dirs d)
|
||||
Just f <- firstAvailable fs
|
||||
| Nothing => throw (InternalError ("Can't find data file " ++ fname))
|
||||
Right d <- coreLift $ readFile f
|
||||
| Left err => throw (FileErr f err)
|
||||
pure d
|
||||
|
||||
-- Given a namespace, return the full path to the checked module,
|
||||
-- looking first in the build directory then in the extra_dirs
|
||||
export
|
||||
nsToPath : {auto c : Ref Ctxt Defs} ->
|
||||
FC -> List String -> Core String
|
||||
nsToPath loc ns
|
||||
= do d <- getDirs
|
||||
let fnameBase = showSep (cast sep) (reverse ns)
|
||||
let fs = map (\p => p ++ cast sep ++ fnameBase ++ ".ttc")
|
||||
(build_dir d :: extra_dirs d)
|
||||
Just f <- firstAvailable fs
|
||||
| Nothing => throw (ModuleNotFound loc ns)
|
||||
pure f
|
||||
|
||||
-- Given a namespace, return the full path to the source module (if it
|
||||
-- exists in the working directory)
|
||||
export
|
||||
nsToSource : {auto c : Ref Ctxt Defs} ->
|
||||
FC -> List String -> Core String
|
||||
nsToSource loc ns
|
||||
= do d <- getDirs
|
||||
let fnameBase = showSep (cast sep) (reverse ns)
|
||||
let fs = map (\ext => fnameBase ++ ext)
|
||||
[".blod", ".idr", ".lidr"]
|
||||
Just f <- firstAvailable fs
|
||||
| Nothing => throw (ModuleNotFound loc ns)
|
||||
pure f
|
||||
|
||||
-- Given a filename in the working directory, return the correct
|
||||
-- namespace for it
|
||||
export
|
||||
pathToNS : String -> String -> List String
|
||||
pathToNS wdir fname
|
||||
= let wsplit = splitSep wdir
|
||||
fsplit = splitSep fname in
|
||||
dropWdir wsplit fsplit fsplit
|
||||
where
|
||||
dropWdir : List String -> List String -> List String -> List String
|
||||
dropWdir wdir orig [] = []
|
||||
dropWdir wdir orig (x :: xs)
|
||||
= if wdir == xs
|
||||
then [x]
|
||||
else x :: dropWdir wdir orig xs
|
||||
|
||||
splitSep : String -> List String
|
||||
splitSep fname
|
||||
= case span (/=sep) fname of
|
||||
(end, "") => [dropExtension end]
|
||||
(mod, rest) => assert_total (splitSep (strTail rest)) ++ [mod]
|
||||
|
||||
-- Create subdirectories, if they don't exist
|
||||
export
|
||||
mkdirs : List String -> IO (Either FileError ())
|
||||
mkdirs [] = pure (Right ())
|
||||
mkdirs (d :: ds)
|
||||
= do ok <- changeDir d
|
||||
if ok
|
||||
then do mkdirs ds
|
||||
changeDir ".."
|
||||
pure (Right ())
|
||||
else do Right _ <- createDir d
|
||||
| Left err => pure (Left err)
|
||||
ok <- changeDir d
|
||||
mkdirs ds
|
||||
changeDir ".."
|
||||
pure (Right ())
|
||||
|
||||
-- Given a namespace (i.e. a module name), make the build directory for the
|
||||
-- corresponding ttc file
|
||||
export
|
||||
makeBuildDirectory : {auto c : Ref Ctxt Defs} ->
|
||||
List String -> Core ()
|
||||
makeBuildDirectory ns
|
||||
= do d <- getDirs
|
||||
let bdir = build_dir d
|
||||
let ndirs = case ns of
|
||||
[] => []
|
||||
(n :: ns) => ns -- first item is file name
|
||||
let fname = showSep (cast sep) (reverse ndirs)
|
||||
Right _ <- coreLift $ mkdirs (build_dir d :: reverse ndirs)
|
||||
| Left err => throw (FileErr (bdir ++ cast sep ++ fname) err)
|
||||
pure ()
|
||||
|
||||
-- Given a source file, return the name of the ttc file to generate
|
||||
export
|
||||
getTTCFileName : {auto c : Ref Ctxt Defs} ->
|
||||
String -> String -> Core String
|
||||
getTTCFileName inp ext
|
||||
= do ns <- getNS
|
||||
d <- getDirs
|
||||
-- Get its namespace from the file relative to the working directory
|
||||
-- and generate the ttc file from that
|
||||
let ns = pathToNS (working_dir d) inp
|
||||
let fname = showSep (cast sep) (reverse ns) ++ ext
|
||||
let bdir = build_dir d
|
||||
pure $ bdir ++ cast sep ++ fname
|
||||
|
||||
-- Given a root executable name, return the name in the build directory
|
||||
export
|
||||
getExecFileName : {auto c : Ref Ctxt Defs} -> String -> Core String
|
||||
getExecFileName efile
|
||||
= do d <- getDirs
|
||||
pure $ build_dir d ++ cast sep ++ efile
|
@ -15,7 +15,8 @@ TTC FC where
|
||||
toBuf b (MkFC file startPos endPos)
|
||||
= do toBuf b file; toBuf b startPos; toBuf b endPos
|
||||
fromBuf r b
|
||||
= do f <- fromBuf r b; s <- fromBuf r b; e <- fromBuf r b
|
||||
= do f <- fromBuf r b;
|
||||
s <- fromBuf r b; e <- fromBuf r b
|
||||
pure (MkFC f s e)
|
||||
|
||||
export
|
||||
@ -206,7 +207,7 @@ TTC (Term vars) where
|
||||
toBuf b fc; toBuf b n; toBuf b i; toBuf b xs
|
||||
toBuf b (Bind fc x bnd scope)
|
||||
= do tag 3;
|
||||
toBuf b fc; toBuf b bnd; toBuf b scope
|
||||
toBuf b fc; toBuf b x; toBuf b bnd; toBuf b scope
|
||||
toBuf b (App fc fn p arg)
|
||||
= do tag 4;
|
||||
toBuf b fc; toBuf b fn; toBuf b p; toBuf b arg
|
||||
|
@ -27,7 +27,7 @@ export
|
||||
processDecls : {vars : _} ->
|
||||
{auto c : Ref Ctxt Defs} ->
|
||||
{auto u : Ref UST UState} ->
|
||||
Env Term vars -> List ImpDecl -> Core ()
|
||||
Env Term vars -> List ImpDecl -> Core Bool
|
||||
processDecls env decls
|
||||
= do traverse (processDecl env) decls
|
||||
pure ()
|
||||
pure True -- TODO: False on error
|
||||
|
@ -4,9 +4,11 @@ import Parser.Support
|
||||
|
||||
import Core.Binary
|
||||
import Core.Context
|
||||
import Core.Directory
|
||||
import Core.Env
|
||||
import Core.FC
|
||||
import Core.Normalise
|
||||
import Core.Options
|
||||
import Core.TT
|
||||
import Core.UnifyState
|
||||
|
||||
@ -18,19 +20,27 @@ import System
|
||||
|
||||
coreMain : String -> Core ()
|
||||
coreMain fname
|
||||
= do Right tti <- coreLift $ parseFile fname
|
||||
(do decls <- prog fname
|
||||
eoi
|
||||
pure decls)
|
||||
| Left err => do coreLift $ printLn err
|
||||
coreLift $ exitWith (ExitFailure 1)
|
||||
coreLift $ putStrLn "Parsed okay"
|
||||
|
||||
defs <- initDefs
|
||||
= do defs <- initDefs
|
||||
c <- newRef Ctxt defs
|
||||
u <- newRef UST initUState
|
||||
processDecls [] tti
|
||||
coreLift $ putStrLn "Done"
|
||||
d <- getDirs
|
||||
case span (/= '.') fname of
|
||||
(_, ".ttc") => do coreLift $ putStrLn "Processing as TTC"
|
||||
readFromTTC {extra = ()} emptyFC True fname [] []
|
||||
coreLift $ putStrLn "Read TTC"
|
||||
_ => do coreLift $ putStrLn "Processing as TTImp"
|
||||
Right tti <- coreLift $ parseFile fname
|
||||
(do decls <- prog fname
|
||||
eoi
|
||||
pure decls)
|
||||
| Left err => do coreLift $ printLn err
|
||||
coreLift $ exitWith (ExitFailure 1)
|
||||
coreLift $ putStrLn "Parsed okay"
|
||||
ok <- processDecls [] tti
|
||||
when ok $
|
||||
do makeBuildDirectory (pathToNS (working_dir d) fname)
|
||||
writeToTTC () !(getTTCFileName fname ".ttc")
|
||||
coreLift $ putStrLn "Written TTC"
|
||||
|
||||
defs <- get Ctxt
|
||||
res <- normalise defs [] (Ref emptyFC Func (NS ["Main"] (UN "main")))
|
||||
|
@ -8,6 +8,7 @@ modules =
|
||||
Core.CaseTree,
|
||||
Core.Context,
|
||||
Core.Core,
|
||||
Core.Directory,
|
||||
Core.Env,
|
||||
Core.FC,
|
||||
Core.Hash,
|
||||
|
Loading…
Reference in New Issue
Block a user