edwinb/Idris2-boot
1
1
Fork 0
mirror of https://github.com/edwinb/Idris2-boot.git synced 2025-01-07 05:36:30 +03:00
Code Issues Projects Releases Wiki Activity

Temporarily disable a couple of unused things

Browse Source 
The Chicken backend and reflection code are currently unused, and add to
memory usage and build time, so best leave them out for the moment.

They will be back! But probably best to wait until we can self host -
which hopefully won't be long - and we can take advantage of some of
the things Idris 2 does to compile quicker and using less space!
This commit is contained in:
Edwin Brady 2020-01-27 19:17:02 +00:00
parent 6f9cca6ce3
commit 56b01f476b
3 changed files with 9 additions and 7 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
src/Idris/IDEMode/REPL.idr
View File

@ -1,7 +1,7 @@
module Idris.IDEMode.REPL module Idris.IDEMode.REPL
import Compiler.Scheme.Chez import Compiler.Scheme.Chez
import Compiler.Scheme.Chicken -- import Compiler.Scheme.Chicken
import Compiler.Scheme.Racket import Compiler.Scheme.Racket
import Compiler.Common import Compiler.Common

5
src/Idris/REPL.idr
View File

@ -1,7 +1,7 @@
module Idris.REPL module Idris.REPL
import Compiler.Scheme.Chez import Compiler.Scheme.Chez
import Compiler.Scheme.Chicken -- import Compiler.Scheme.Chicken
import Compiler.Scheme.Racket import Compiler.Scheme.Racket
import Compiler.Common import Compiler.Common
@ -229,7 +229,8 @@ findCG
= do defs <- get Ctxt = do defs <- get Ctxt
case codegen (session (options defs)) of case codegen (session (options defs)) of
Chez => pure codegenChez Chez => pure codegenChez
Chicken => pure codegenChicken Chicken => throw (InternalError "Chicken CG not available")
-- pure codegenChicken
Racket => pure codegenRacket Racket => pure codegenRacket
anyAt : (FC -> Bool) -> FC -> a -> Bool anyAt : (FC -> Bool) -> FC -> a -> Bool

9
src/TTImp/Elab/Term.idr
View File

@ -5,7 +5,7 @@ import Core.Core
import Core.Env import Core.Env
import Core.Metadata import Core.Metadata
import Core.Normalise import Core.Normalise
import Core.Reflect -- import Core.Reflect
import Core.Unify import Core.Unify
import Core.TT import Core.TT
import Core.Value import Core.Value
@ -22,10 +22,10 @@ import TTImp.Elab.ImplicitBind
import TTImp.Elab.Lazy import TTImp.Elab.Lazy
import TTImp.Elab.Local import TTImp.Elab.Local
import TTImp.Elab.Prim import TTImp.Elab.Prim
import TTImp.Elab.Quote -- import TTImp.Elab.Quote
import TTImp.Elab.Record import TTImp.Elab.Record
import TTImp.Elab.Rewrite import TTImp.Elab.Rewrite
import TTImp.Reflect -- import TTImp.Reflect
import TTImp.TTImp import TTImp.TTImp
%default covering %default covering
@ -168,7 +168,8 @@ checkTerm rig elabinfo nest env (IDelay fc tm) exp
checkTerm rig elabinfo nest env (IForce fc tm) exp checkTerm rig elabinfo nest env (IForce fc tm) exp
= checkForce rig elabinfo nest env fc tm exp = checkForce rig elabinfo nest env fc tm exp
checkTerm rig elabinfo nest env (IQuote fc tm) exp checkTerm rig elabinfo nest env (IQuote fc tm) exp
= checkQuote rig elabinfo nest env fc tm exp = throw (GenericMsg fc "Reflection not implemented yet")
-- = checkQuote rig elabinfo nest env fc tm exp
checkTerm rig elabinfo nest env (IQuoteDecl fc tm) exp checkTerm rig elabinfo nest env (IQuoteDecl fc tm) exp
= throw (GenericMsg fc "Declaration reflection not implemented yet") = throw (GenericMsg fc "Declaration reflection not implemented yet")
checkTerm rig elabinfo nest env (IUnquote fc tm) exp checkTerm rig elabinfo nest env (IUnquote fc tm) exp