Skip to content

Commit 8fab53d

Browse files
committed
--no-import-cue option
1 parent 8ceab51 commit 8fab53d

File tree

4 files changed

+28
-8
lines changed

4 files changed

+28
-8
lines changed

app/Commands/Compile/Anoma/Options.hs

+8-1
Original file line numberDiff line numberDiff line change
@@ -14,7 +14,8 @@ data AnomaOptions (k :: InputKind) = AnomaOptions
1414
_anomaModular :: Bool,
1515
_anomaOutputText :: Bool,
1616
_anomaOutputHoon :: Bool,
17-
_anomaNoStdlib :: Bool
17+
_anomaNoStdlib :: Bool,
18+
_anomaNoNockImportDecoding :: Bool
1819
}
1920

2021
deriving stock instance (Typeable k, Data (InputFileType k)) => Data (AnomaOptions k)
@@ -44,11 +45,17 @@ parseAnoma = do
4445
( long "no-anomalib"
4546
<> help "Do not bundle the Anoma standard library"
4647
)
48+
_anomaNoNockImportDecoding <-
49+
switch
50+
( long "no-import-cue"
51+
<> help "Do not generate code to cue imported modules. Required to run the generated code with the builtin evaluator."
52+
)
4753
pure AnomaOptions {..}
4854

4955
instance EntryPointOptions (AnomaOptions k) where
5056
applyOptions opts =
5157
set entryPointPipeline (Just PipelineExec)
5258
. set entryPointTarget (Just TargetAnoma)
5359
. set entryPointNoAnomaStdlib (opts ^. anomaNoStdlib)
60+
. set entryPointNoNockImportDecoding (opts ^. anomaNoNockImportDecoding)
5461
. applyOptions (opts ^. anomaCompileCommonOptions)

src/Juvix/Compiler/Nockma/Translation/FromTree.hs

+17-7
Original file line numberDiff line numberDiff line change
@@ -96,13 +96,15 @@ data BuiltinFunctionId
9696
instance Hashable BuiltinFunctionId
9797

9898
data CompilerOptions = CompilerOptions
99-
{ _compilerOptionsNoStdlib :: Bool
99+
{ _compilerOptionsNoStdlib :: Bool,
100+
_compilerOptionsNoImportDecoding :: Bool
100101
}
101102

102103
fromEntryPoint :: EntryPoint -> CompilerOptions
103104
fromEntryPoint EntryPoint {..} =
104105
CompilerOptions
105-
{ _compilerOptionsNoStdlib = _entryPointNoAnomaStdlib
106+
{ _compilerOptionsNoStdlib = _entryPointNoAnomaStdlib,
107+
_compilerOptionsNoImportDecoding = _entryPointNoNockImportDecoding
106108
}
107109

108110
newtype FunctionCtx = FunctionCtx
@@ -129,6 +131,7 @@ data CompilerCtx = CompilerCtx
129131
_compilerModuleInfos :: HashMap ModuleId ModuleInfo,
130132
_compilerModuleId :: ModuleId,
131133
_compilerBatch :: Bool,
134+
_compilerNoImportDecoding :: Bool,
132135
-- | Maps temporary variables to their stack indices.
133136
_compilerTempVarMap :: HashMap Int TempRef,
134137
_compilerTempVarsNum :: Int,
@@ -149,6 +152,7 @@ emptyCompilerCtx =
149152
_compilerModuleInfos = mempty,
150153
_compilerModuleId = defaultModuleId,
151154
_compilerBatch = True,
155+
_compilerNoImportDecoding = False,
152156
_compilerTempVarMap = mempty,
153157
_compilerTempVarsNum = 0,
154158
_compilerStackHeight = 0
@@ -321,7 +325,11 @@ mkScry :: [Term Natural] -> Term Natural
321325
mkScry key = OpScry # (OpQuote # nockNilTagged "OpScry-typehint") # (foldTermsOrQuotedNil key)
322326

323327
mkScryDecode :: (Member (Reader CompilerCtx) r) => [Term Natural] -> Sem r (Term Natural)
324-
mkScryDecode key = callStdlib StdlibDecode [mkScry key]
328+
mkScryDecode key = do
329+
bNoDecode <- asks (^. compilerNoImportDecoding)
330+
if
331+
| bNoDecode -> return $ mkScry key
332+
| otherwise -> callStdlib StdlibDecode [mkScry key]
325333

326334
allConstructors :: Tree.Module -> Tree.ConstructorInfo -> NonEmpty Tree.ConstructorInfo
327335
allConstructors md ci =
@@ -468,11 +476,12 @@ compileToSubject bundleAnomaLib ctx importsSHA256 importedModuleIds userFuns msy
468476
fromTreeModule :: (Member (Reader CompilerOptions) r) => (ModuleId -> Sem r Module) -> InfoTable -> Tree.Module -> Sem r Module
469477
fromTreeModule fetchModule importsTab md = do
470478
optNoStdlib <- asks (^. compilerOptionsNoStdlib)
479+
optNoImportDecoding <- asks (^. compilerOptionsNoImportDecoding)
471480
importsSHA256 :: HashMap ModuleId ByteString <-
472481
HashMap.fromList
473482
. map (\m -> (m ^. moduleId, fromJust (m ^. moduleInfoTable . infoSHA256)))
474483
<$> mapM fetchModule importedModuleIds
475-
let moduleCode = compileToSubject (not optNoStdlib) compilerCtx importsSHA256 importedModuleIds userFuns (md ^. Tree.moduleInfoTable . Tree.infoMainFunction)
484+
let moduleCode = compileToSubject (not optNoStdlib) (compilerCtx optNoImportDecoding) importsSHA256 importedModuleIds userFuns (md ^. Tree.moduleInfoTable . Tree.infoMainFunction)
476485
jammedCode = jamToByteString moduleCode
477486
tab =
478487
InfoTable
@@ -529,8 +538,8 @@ fromTreeModule fetchModule importsTab md = do
529538
}
530539
)
531540

532-
compilerCtx :: CompilerCtx
533-
compilerCtx =
541+
compilerCtx :: Bool -> CompilerCtx
542+
compilerCtx optNoImportDecoding =
534543
emptyCompilerCtx
535544
{ _compilerFunctionInfos =
536545
userFunInfos <> importsTab ^. infoFunctions,
@@ -539,7 +548,8 @@ fromTreeModule fetchModule importsTab md = do
539548
_compilerModuleInfos =
540549
HashMap.fromList $ map mkModuleInfo [0 .. length allModuleIds - 1],
541550
_compilerModuleId = md ^. Tree.moduleId,
542-
_compilerBatch = null importedFuns
551+
_compilerBatch = null importedFuns,
552+
_compilerNoImportDecoding = optNoImportDecoding
543553
}
544554
where
545555
mkModuleInfo :: Int -> (ModuleId, ModuleInfo)

src/Juvix/Compiler/Pipeline/EntryPoint.hs

+2
Original file line numberDiff line numberDiff line change
@@ -58,6 +58,7 @@ data EntryPoint = EntryPoint
5858
_entryPointIsabelleOnlyTypes :: Bool,
5959
_entryPointPipeline :: Maybe Pipeline,
6060
_entryPointNoAnomaStdlib :: Bool,
61+
_entryPointNoNockImportDecoding :: Bool,
6162
-- | The SHA256 hash of the source file at _entryPointModulePath
6263
_entryPointSHA256 :: Maybe Text,
6364
-- | Dump verification statements?
@@ -125,6 +126,7 @@ defaultEntryPointNoFile pkg root =
125126
_entryPointIsabelleOnlyTypes = False,
126127
_entryPointPipeline = Nothing,
127128
_entryPointNoAnomaStdlib = False,
129+
_entryPointNoNockImportDecoding = False,
128130
_entryPointSHA256 = Nothing,
129131
_entryPointVerify = False
130132
}

test/Base.hs

+1
Original file line numberDiff line numberDiff line change
@@ -291,6 +291,7 @@ compileAnomaModular enableDebug relRoot mainFile rootCopyDir = do
291291
entryPoint <-
292292
set entryPointPipeline (Just PipelineExec)
293293
. set entryPointTarget (Just TargetAnoma)
294+
. set entryPointNoNockImportDecoding True
294295
. set entryPointDebug enableDebug
295296
<$> testDefaultEntryPointIO testRootDir (testRootDir <//> mainFile)
296297
r <- testRunIOModular (Just Core.CheckAnoma) entryPoint modularCoreToAnoma

0 commit comments

Comments
 (0)