From 09aa35d256be6cd6690068deb6c11852824fc0a7 Mon Sep 17 00:00:00 2001 From: Paul Cadman Date: Tue, 19 Dec 2023 14:50:47 +0000 Subject: [PATCH] Add decodePath' --- src/Juvix/Compiler/Nockma/Language.hs | 14 ++++++++++---- 1 file changed, 10 insertions(+), 4 deletions(-) diff --git a/src/Juvix/Compiler/Nockma/Language.hs b/src/Juvix/Compiler/Nockma/Language.hs index 771f134390..0f92fc09ae 100644 --- a/src/Juvix/Compiler/Nockma/Language.hs +++ b/src/Juvix/Compiler/Nockma/Language.hs @@ -169,8 +169,11 @@ decodePath ep = execOutputList (go (ep ^. encodedPath)) go ((x - 1) `div` 2) output R -encodePath :: Path -> Natural -encodePath = foldl' step 1 +decodePath' :: EncodedPath -> Path +decodePath' = run . runFailDefault (error "encoded path cannot be 0") . decodePath + +encodePath :: Path -> EncodedPath +encodePath = EncodedPath . foldl' step 1 where step :: Natural -> Direction -> Natural step n = \case @@ -215,7 +218,7 @@ instance NockNatural Natural where errInvalidOp atm = NaturalInvalidOp atm errInvalidPath atm = NaturalInvalidPath atm serializeNockOp = serializeOp - serializePath = encodePath + serializePath = (^. encodedPath) . encodePath class IsNock nock where toNock :: nock -> Term Natural @@ -241,7 +244,10 @@ instance IsNock Bool where True -> toNock (nockTrue @Natural) instance IsNock Path where - toNock pos = toNock (Atom (encodePath pos) (Irrelevant (Just AtomHintPath))) + toNock pos = TermAtom (Atom (encodePath pos ^. encodedPath) (Irrelevant (Just AtomHintPath))) + +instance IsNock EncodedPath where + toNock = toNock . decodePath' infixr 5 #