edwinb/Idris2-boot
1
1
Fork 0
mirror of https://github.com/edwinb/Idris2-boot.git synced 2024-11-24 04:43:25 +03:00
Code Issues Projects Releases Wiki Activity

Update makefiles and paths

Browse Source 
We can now build and install the prelude, and hello world has
successfully compiled to chez
This commit is contained in:
Edwin Brady 2019-06-13 16:50:24 +01:00
parent 772b098de0
commit 2c1c86639a
11 changed files with 49 additions and 37 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

36
Makefile
View File

@ -1,5 +1,5 @@
PREFIX = ${HOME}/.idris2
export IDRIS2_PATH = ${CURDIR}/prelude/build:${CURDIR}/base/build
export IDRIS2_PATH = ${CURDIR}/libs/prelude/build:${CURDIR}/libs/base/build
export IDRIS2_DATA = ${CURDIR}/support
.PHONY: ttimp idris2 prelude test base clean lib_clean
@ -12,11 +12,11 @@ idris2: src/YafflePaths.idr
src/YafflePaths.idr:
echo 'module YafflePaths; export yprefix : String; yprefix = "${PREFIX}"' > src/YafflePaths.idr
#prelude:
# make -C libs/prelude YAFFLE=../../idris2
prelude:
make -C libs/prelude IDRIS2=../../idris2
#base: prelude
# make -C libs/base YAFFLE=../../idris2
# make -C libs/base IDRIS2=../../idris2
#libs : prelude base
@ -27,22 +27,22 @@ clean: lib_clean
rm -f idris2
lib_clean:
# make -C prelude clean
# make -C base clean
make -C libs/prelude clean
# make -C libs/base clean
test:
idris --build tests.ipkg
make -C tests
#install:
# mkdir -p ${PREFIX}/bin
# mkdir -p ${PREFIX}/blodwen/support/chez
# mkdir -p ${PREFIX}/blodwen/support/chicken
# mkdir -p ${PREFIX}/blodwen/support/racket
# make -C prelude install BLODWEN=../blodwen
# make -C base install BLODWEN=../blodwen
#
# install blodwen ${PREFIX}/bin
# install support/chez/* ${PREFIX}/blodwen/support/chez
# install support/chicken/* ${PREFIX}/blodwen/support/chicken
# install support/racket/* ${PREFIX}/blodwen/support/racket
install:
mkdir -p ${PREFIX}/bin
mkdir -p ${PREFIX}/idris2/support/chez
mkdir -p ${PREFIX}/idris2/support/chicken
mkdir -p ${PREFIX}/idris2/support/racket
make -C libs/prelude install IDRIS2=../../idris2
# make -C libs/base install IDRIS2=../../idris2
install idris2 ${PREFIX}/bin
install support/chez/* ${PREFIX}/idris2/support/chez
install support/chicken/* ${PREFIX}/idris2/support/chicken
install support/racket/* ${PREFIX}/idris2/support/racket

2
idris2.ipkg
View File

@ -118,7 +118,7 @@ modules =
sourcedir = src
executable = idris2
-- opts = "--cg-opt -O2 --partial-eval"
opts = "--cg-opt -g --partial-eval"
opts = "--partial-eval"
main = Idris.Main

4
src/Compiler/CompileExpr.idr
View File

@ -269,12 +269,12 @@ toCDef : {auto c : Ref Ctxt Defs} ->
NameTags -> Name -> Def ->
Core CDef
toCDef tags n None
= pure $ MkError $ CCrash emptyFC ("Encountered undefined name " ++ show n)
= pure $ MkError $ CCrash emptyFC ("Encountered undefined name " ++ show !(getFullName n))
toCDef tags n (PMDef args _ tree _)
= pure $ MkFun _ !(toCExpTree tags n tree)
toCDef tags n (ExternDef arity)
= let (ns ** args) = mkArgList 0 arity in
pure $ MkFun _ (CExtPrim emptyFC n (map toArgExp (getVars args)))
pure $ MkFun _ (CExtPrim emptyFC !(getFullName n) (map toArgExp (getVars args)))
where
toArgExp : (Var ns) -> CExp ns
toArgExp (MkVar p) = CLocal emptyFC p

10
src/Compiler/Scheme/Common.idr
View File

@ -314,19 +314,21 @@ parameters (schExtPrim : {vars : _} -> Int -> SVars vars -> ExtPrim -> List (CEx
schArglist [x] = x
schArglist (x :: xs) = x ++ " " ++ schArglist xs
schDef : Name -> CDef -> Core String
schDef : {auto c : Ref Ctxt Defs} ->
Name -> CDef -> Core String
schDef n (MkFun args exp)
= let vs = initSVars args in
pure $ "(define " ++ schName n ++ " (lambda (" ++ schArglist vs ++ ") "
pure $ "(define " ++ schName !(getFullName n) ++ " (lambda (" ++ schArglist vs ++ ") "
++ !(schExp 0 vs exp) ++ "))\n"
schDef n (MkError exp)
= pure $ "(define (" ++ schName n ++ " . any-args) " ++ !(schExp 0 [] exp) ++ ")\n"
= pure $ "(define (" ++ schName !(getFullName n) ++ " . any-args) " ++ !(schExp 0 [] exp) ++ ")\n"
schDef n (MkCon t a) = pure "" -- Nothing to compile here
-- Convert the name to scheme code
-- (There may be no code generated, for example if it's a constructor)
export
getScheme : (schExtPrim : {vars : _} -> Int -> SVars vars -> ExtPrim -> List (CExp vars) -> Core String) ->
getScheme : {auto c : Ref Ctxt Defs} ->
(schExtPrim : {vars : _} -> Int -> SVars vars -> ExtPrim -> List (CExp vars) -> Core String) ->
Defs -> Name -> Core String
getScheme schExtPrim defs n
= case !(lookupCtxtExact n (gamma defs)) of

2
src/Core/Directory.idr
View File

@ -76,7 +76,7 @@ nsToSource loc ns
= do d <- getDirs
let fnameBase = showSep (cast sep) (reverse ns)
let fs = map (\ext => fnameBase ++ ext)
[".blod", ".idr", ".lidr"]
[".yaff", ".idr", ".lidr"]
Just f <- firstAvailable fs
| Nothing => throw (ModuleNotFound loc ns)
pure f

5
src/Core/Name.idr
View File

@ -23,10 +23,11 @@ userNameRoot _ = Nothing
export
isUserName : Name -> Bool
isUserName (UN _) = True
isUserName (PV _ _) = False
isUserName (MN _ _) = False
isUserName (NS _ n) = isUserName n
isUserName (DN _ n) = isUserName n
isUserName _ = False
isUserName _ = True
export
nameRoot : Name -> String

6
src/Idris/Main.idr
View File

@ -43,12 +43,12 @@ updatePaths : {auto c : Ref Ctxt Defs} ->
updatePaths
= do setPrefix yprefix
defs <- get Ctxt
bpath <- coreLift $ getEnv "BLODWEN_PATH"
bpath <- coreLift $ getEnv "IDRIS2_PATH"
case bpath of
Just path => do traverse addExtraDir (map trim (split (==':') path))
pure ()
Nothing => pure ()
bdata <- coreLift $ getEnv "BLODWEN_DATA"
bdata <- coreLift $ getEnv "IDRIS2_DATA"
case bdata of
Just path => do traverse addDataDir (map trim (split (==':') path))
pure ()
@ -60,7 +60,7 @@ updatePaths
addPkgDir "prelude"
addPkgDir "base"
addDataDir (dir_prefix (dirs (options defs)) ++ dirSep ++
"blodwen" ++ dirSep ++ "support")
"idris2" ++ dirSep ++ "support")
updateREPLOpts : {auto o : Ref ROpts REPLOpts} ->
Core ()

2
src/Idris/Package.idr
View File

@ -220,7 +220,7 @@ install pkg
(mainmod pkg)
srcdir <- coreLift currentDir
-- Make the package installation directory
let installPrefix = dir_prefix (dirs (options defs)) ++ dirSep ++ "blodwen"
let installPrefix = dir_prefix (dirs (options defs)) ++ dirSep ++ "idris2"
True <- coreLift $ changeDir installPrefix
| False => throw (FileErr (name pkg) FileReadError)
Right _ <- coreLift $ mkdirs [name pkg]

8
src/Idris/REPL.idr
View File

@ -45,14 +45,16 @@ import System
%default covering
showInfo : (Name, Int, GlobalDef) -> Core ()
showInfo : {auto c : Ref Ctxt Defs} ->
(Name, Int, GlobalDef) -> Core ()
showInfo (n, idx, d)
= do coreLift $ putStrLn (show (fullname d) ++ " ==> " ++
show (definition d))
case compexpr d of
Nothing => pure ()
Just expr => coreLift $ putStrLn ("Compiled: " ++ show expr)
coreLift $ putStrLn ("Refers to: " ++ show (keys (refersTo d)))
coreLift $ putStrLn ("Refers to: " ++
show !(traverse getFullName (keys (refersTo d))))
when (not (isNil (sizeChange d))) $
let scinfo = map (\s => show (fnCall s) ++ ": " ++
show (fnArgs s)) (sizeChange d) in
@ -223,7 +225,7 @@ execExp : {auto c : Ref Ctxt Defs} ->
execExp ctm
= do ttimp <- desugar AnyExpr [] (PApp replFC (PRef replFC (UN "unsafePerformIO")) ctm)
inidx <- resolveName (UN "[input]")
(tm, _, ty) <- elabTerm inidx InExpr [] (MkNested [])
(_, tm, ty) <- elabTerm inidx InExpr [] (MkNested [])
[] ttimp Nothing
execute !findCG tm

2
src/Idris/SetOptions.idr
View File

@ -19,7 +19,7 @@ addPkgDir : {auto c : Ref Ctxt Defs} ->
addPkgDir p
= do defs <- get Ctxt
addExtraDir (dir_prefix (dirs (options defs)) ++ dirSep ++
"blodwen" ++ dirSep ++ p)
"idris2" ++ dirSep ++ p)
-- Options to be processed before type checking
export

9
src/TTImp/ProcessType.idr
View File

@ -69,7 +69,14 @@ processType {vars} eopts nest env fc rig vis opts (MkImpTy tfc n_in ty_raw)
(Just (gType fc))
logTermNF 5 (show n) [] (abstractEnvType tfc env ty)
-- TODO: Check name visibility
let def = None -- TODO: External definitions
-- If it's declared as externally defined, set the definition to
-- ExternFn <arity>, where the arity is assumed to be fixed (i.e.
-- not dependent on any of the arguments)
def <- if ExternFn `elem` opts
then do defs <- get Ctxt
a <- getArity defs env ty
pure (ExternDef a)
else pure None
addDef (Resolved idx) (newDef fc n rig vars (abstractEnvType tfc env ty) vis def)
-- Flag it as checked, because we're going to check the clauses