From 56b01f476b0f73bf5d04956f260d5614fc89a565 Mon Sep 17 00:00:00 2001 From: Edwin Brady Date: Mon, 27 Jan 2020 19:17:02 +0000 Subject: [PATCH] Temporarily disable a couple of unused things 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! --- src/Idris/IDEMode/REPL.idr | 2 +- src/Idris/REPL.idr | 5 +++-- src/TTImp/Elab/Term.idr | 9 +++++---- 3 files changed, 9 insertions(+), 7 deletions(-) diff --git a/src/Idris/IDEMode/REPL.idr b/src/Idris/IDEMode/REPL.idr index 939dbfd..30b4b07 100644 --- a/src/Idris/IDEMode/REPL.idr +++ b/src/Idris/IDEMode/REPL.idr @@ -1,7 +1,7 @@ module Idris.IDEMode.REPL import Compiler.Scheme.Chez -import Compiler.Scheme.Chicken +-- import Compiler.Scheme.Chicken import Compiler.Scheme.Racket import Compiler.Common diff --git a/src/Idris/REPL.idr b/src/Idris/REPL.idr index 0f57431..9d12a81 100644 --- a/src/Idris/REPL.idr +++ b/src/Idris/REPL.idr @@ -1,7 +1,7 @@ module Idris.REPL import Compiler.Scheme.Chez -import Compiler.Scheme.Chicken +-- import Compiler.Scheme.Chicken import Compiler.Scheme.Racket import Compiler.Common @@ -229,7 +229,8 @@ findCG = do defs <- get Ctxt case codegen (session (options defs)) of Chez => pure codegenChez - Chicken => pure codegenChicken + Chicken => throw (InternalError "Chicken CG not available") + -- pure codegenChicken Racket => pure codegenRacket anyAt : (FC -> Bool) -> FC -> a -> Bool diff --git a/src/TTImp/Elab/Term.idr b/src/TTImp/Elab/Term.idr index ca00046..e068165 100644 --- a/src/TTImp/Elab/Term.idr +++ b/src/TTImp/Elab/Term.idr @@ -5,7 +5,7 @@ import Core.Core import Core.Env import Core.Metadata import Core.Normalise -import Core.Reflect +-- import Core.Reflect import Core.Unify import Core.TT import Core.Value @@ -22,10 +22,10 @@ import TTImp.Elab.ImplicitBind import TTImp.Elab.Lazy import TTImp.Elab.Local import TTImp.Elab.Prim -import TTImp.Elab.Quote +-- import TTImp.Elab.Quote import TTImp.Elab.Record import TTImp.Elab.Rewrite -import TTImp.Reflect +-- import TTImp.Reflect import TTImp.TTImp %default covering @@ -168,7 +168,8 @@ checkTerm rig elabinfo nest env (IDelay fc tm) exp checkTerm rig elabinfo nest env (IForce fc tm) exp = checkForce rig elabinfo nest env 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 = throw (GenericMsg fc "Declaration reflection not implemented yet") checkTerm rig elabinfo nest env (IUnquote fc tm) exp