Position -> Path as a list of directions

app/Commands/Dev/Nockma/Repl.hs

@@ -110,7 +110,7 @@ fromMegaParsecError = \case
 direction' :: String -> Repl ()
 direction' s = Repline.dontCrash $ do
   let n = read s :: Natural
-      p = run (runFailDefault (error "invalid position") (decodePosition n))
+      p = run (runFailDefault (error "invalid position") (decodePath n))
   liftIO (putStrLn (ppPrint p))
 
 readTerm :: String -> Repl (Term Natural)

src/Juvix/Compiler/Nockma/Evaluator.hs

@@ -6,7 +6,7 @@ where
 
 import Juvix.Compiler.Nockma.Evaluator.Error
 import Juvix.Compiler.Nockma.Language
-import Juvix.Prelude hiding (Atom)
+import Juvix.Prelude hiding (Atom, Path)
 
 asAtom :: (Member (Error NockEvalError) r) => Term a -> Sem r (Atom a)
 asAtom = \case
@@ -23,35 +23,35 @@ asBool t = do
   a <- asAtom t
   return (a == nockTrue)
 
-asPosition :: (Members '[Error NockEvalError, Error (ErrNockNatural a)] r, NockNatural a) => Term a -> Sem r Position
-asPosition = asAtom >=> nockPosition
+asPath :: (Members '[Error NockEvalError, Error (ErrNockNatural a)] r, NockNatural a) => Term a -> Sem r Path
+asPath = asAtom >=> nockPath
 
-subTermT' :: Position -> Traversal (Term a) (Term a) (First (Term a)) (Term a)
+subTermT' :: Path -> Traversal (Term a) (Term a) (First (Term a)) (Term a)
 subTermT' pos f = subTermT pos (f . First . Just)
 
-subTermT :: Position -> Traversal' (Term a) (Term a)
+subTermT :: Path -> Traversal' (Term a) (Term a)
 subTermT = go
   where
-    go :: Position -> (forall f. (Applicative f) => (Term a -> f (Term a)) -> Term a -> f (Term a))
-    go p = case p ^. positionDirections of
+    go :: Path -> (forall f. (Applicative f) => (Term a -> f (Term a)) -> Term a -> f (Term a))
+    go = \case
       [] -> id
       d : ds -> \g t -> case t of
         TermAtom {} -> pure t
         TermCell c -> case d of
-          L -> (\l' -> TermCell (set cellLeft l' c)) <$> go (Position ds) g (c ^. cellLeft)
-          R -> (\r' -> TermCell (set cellRight r' c)) <$> go (Position ds) g (c ^. cellRight)
+          L -> (\l' -> TermCell (set cellLeft l' c)) <$> go ds g (c ^. cellLeft)
+          R -> (\r' -> TermCell (set cellRight r' c)) <$> go ds g (c ^. cellRight)
 
-subTerm :: (Member (Error NockEvalError) r) => Term a -> Position -> Sem r (Term a)
+subTerm :: (Member (Error NockEvalError) r) => Term a -> Path -> Sem r (Term a)
 subTerm term pos = do
   case term ^? subTermT pos of
-    Nothing -> throw InvalidPosition
+    Nothing -> throw InvalidPath
     Just t -> return t
 
-setSubTerm :: (Member (Error NockEvalError) r) => Term a -> Position -> Term a -> Sem r (Term a)
+setSubTerm :: (Member (Error NockEvalError) r) => Term a -> Path -> Term a -> Sem r (Term a)
 setSubTerm term pos repTerm =
   let (old, new) = setAndRemember (subTermT' pos) repTerm term
    in if
-          | isNothing (getFirst old) -> throw InvalidPosition
+          | isNothing (getFirst old) -> throw InvalidPath
           | otherwise -> return new
 
 parseCell :: forall r a. (Members '[Error NockEvalError, Error (ErrNockNatural a)] r, NockNatural a) => Cell a -> Sem r (ParsedCell a)
@@ -134,7 +134,7 @@ eval stack = \case
       OpHint -> goOpHint
       where
         goOpAddress :: Sem r (Term a)
-        goOpAddress = asPosition (c ^. operatorCellTerm) >>= subTerm stack
+        goOpAddress = asPath (c ^. operatorCellTerm) >>= subTerm stack
 
         goOpQuote :: Sem r (Term a)
         goOpQuote = return (c ^. operatorCellTerm)
@@ -161,7 +161,7 @@ eval stack = \case
         goOpReplace = do
           cellTerm <- asCell (c ^. operatorCellTerm)
           rt1 <- asCell (cellTerm ^. cellLeft)
-          r <- asPosition (rt1 ^. cellLeft)
+          r <- asPath (rt1 ^. cellLeft)
           let t1 = rt1 ^. cellRight
           t1' <- eval stack t1
           t2' <- eval stack (cellTerm ^. cellRight)
@@ -200,7 +200,7 @@ eval stack = \case
         goOpCall :: Sem r (Term a)
         goOpCall = do
           cellTerm <- asCell (c ^. operatorCellTerm)
-          r <- asPosition (cellTerm ^. cellLeft)
+          r <- asPath (cellTerm ^. cellLeft)
           t' <- eval stack (cellTerm ^. cellRight)
           subTerm t' r >>= eval t'
 

src/Juvix/Compiler/Nockma/Evaluator/Error.hs

@@ -4,7 +4,7 @@ import Juvix.Prelude hiding (Atom)
 import Juvix.Prelude.Pretty
 
 data NockEvalError
-  = InvalidPosition
+  = InvalidPath
   | ExpectedAtom
   | ExpectedCell
   | NoStack

src/Juvix/Compiler/Nockma/Language.hs

@@ -2,7 +2,7 @@ module Juvix.Compiler.Nockma.Language where
 
 import Data.HashMap.Strict qualified as HashMap
 import GHC.Base (Type)
-import Juvix.Prelude hiding (Atom)
+import Juvix.Prelude hiding (Atom, Path)
 import Juvix.Prelude.Pretty
 
 data ReplStatement a
@@ -54,7 +54,7 @@ data Atom a = Atom
 
 data AtomHint
   = AtomHintOp
-  | AtomHintPosition
+  | AtomHintPath
   | AtomHintBool
 
 data NockOp
@@ -106,21 +106,19 @@ data ParsedCell a
   = ParsedOperatorCell (OperatorCell a)
   | ParsedAutoConsCell (AutoConsCell a)
 
-type EncodedPosition = Natural
+type EncodedPath = Natural
 
 data Direction
   = L
   | R
   deriving stock (Show)
 
-newtype Position = Position {_positionDirections :: [Direction]}
-  deriving stock (Show)
+type Path = [Direction]
 
 makeLenses ''Cell
 makeLenses ''Atom
 makeLenses ''OperatorCell
 makeLenses ''AutoConsCell
-makeLenses ''Position
 makeLenses ''Program
 makeLenses ''Assignment
 makeLenses ''WithStack
@@ -149,10 +147,10 @@ serializeOp = \case
   OpReplace -> 10
   OpHint -> 11
 
-decodePosition :: forall r. (Member Fail r) => EncodedPosition -> Sem r Position
-decodePosition ep = Position <$> execOutputList (go ep)
+decodePath :: forall r. (Member Fail r) => EncodedPath -> Sem r Path
+decodePath ep = execOutputList (go ep)
   where
-    go :: EncodedPosition -> Sem (Output Direction ': r) ()
+    go :: EncodedPath -> Sem (Output Direction ': r) ()
     go = \case
       0 -> fail
       1 -> return ()
@@ -165,8 +163,8 @@ decodePosition ep = Position <$> execOutputList (go ep)
                 go ((x - 1) `div` 2)
                 output R
 
-serializePositionNatural :: Position -> Natural
-serializePositionNatural p = foldl' step 1 (p ^. positionDirections)
+serializePathNatural :: Path -> Natural
+serializePathNatural = foldl' step 1
   where
     step :: Natural -> Direction -> Natural
     step n = \case
@@ -177,28 +175,28 @@ class (Eq a) => NockNatural a where
   type ErrNockNatural a :: Type
   nockNatural :: (Member (Error (ErrNockNatural a)) r) => Atom a -> Sem r Natural
   serializeNockOp :: NockOp -> a
-  serializePosition :: Position -> a
+  serializePath :: Path -> a
 
   errInvalidOp :: Atom a -> ErrNockNatural a
 
-  errInvalidPosition :: Atom a -> ErrNockNatural a
+  errInvalidPath :: Atom a -> ErrNockNatural a
 
   nockOp :: (Member (Error (ErrNockNatural a)) r) => Atom a -> Sem r NockOp
   nockOp atm = do
     n <- nockNatural atm
     failWithError (errInvalidOp atm) (parseOp n)
 
-  nockPosition :: (Member (Error (ErrNockNatural a)) r) => Atom a -> Sem r Position
-  nockPosition atm = do
+  nockPath :: (Member (Error (ErrNockNatural a)) r) => Atom a -> Sem r Path
+  nockPath atm = do
     n <- nockNatural atm
-    failWithError (errInvalidPosition atm) (decodePosition n)
+    failWithError (errInvalidPath atm) (decodePath n)
 
   nockTrue :: Atom a
   nockFalse :: Atom a
   nockSucc :: Atom a -> Atom a
 
 data NockNaturalNaturalError
-  = NaturalInvalidPosition (Atom Natural)
+  = NaturalInvalidPath (Atom Natural)
   | NaturalInvalidOp (Atom Natural)
   deriving stock (Show)
 
@@ -209,9 +207,9 @@ instance NockNatural Natural where
   nockFalse = Atom 1 (Irrelevant (Just AtomHintBool))
   nockSucc = over atom succ
   errInvalidOp atm = NaturalInvalidOp atm
-  errInvalidPosition atm = NaturalInvalidPosition atm
+  errInvalidPath atm = NaturalInvalidPath atm
   serializeNockOp = serializeOp
-  serializePosition = serializePositionNatural
+  serializePath = serializePathNatural
 
 class IsNock nock where
   toNock :: nock -> Term Natural
@@ -236,8 +234,8 @@ instance IsNock Bool where
     False -> toNock (nockFalse @Natural)
     True -> toNock (nockTrue @Natural)
 
-instance IsNock Position where
-  toNock pos = toNock (Atom (serializePositionNatural pos) (Irrelevant (Just AtomHintPosition)))
+instance IsNock Path where
+  toNock pos = toNock (Atom (serializePathNatural pos) (Irrelevant (Just AtomHintPath)))
 
 infixr 5 #
 

src/Juvix/Compiler/Nockma/Pretty/Base.hs

@@ -8,7 +8,7 @@ where
 import Juvix.Compiler.Nockma.Language
 import Juvix.Compiler.Nockma.Pretty.Options
 import Juvix.Data.CodeAnn
-import Juvix.Prelude hiding (Atom)
+import Juvix.Prelude hiding (Atom, Path)
 
 doc :: (PrettyCode c) => Options -> c -> Doc Ann
 doc opts =
@@ -29,7 +29,7 @@ instance (PrettyCode a, NockNatural a) => PrettyCode (Atom a) where
       h' <- failMaybe (h ^. unIrrelevant)
       case h' of
         AtomHintOp -> nockOp atm >>= ppCode
-        AtomHintPosition -> nockPosition atm >>= ppCode
+        AtomHintPath -> nockPath atm >>= ppCode
         AtomHintBool
           | atm == nockTrue -> return (annotate (AnnKind KNameInductive) "true")
           | atm == nockFalse -> return (annotate (AnnKind KNameAxiom) "false")
@@ -38,8 +38,8 @@ instance (PrettyCode a, NockNatural a) => PrettyCode (Atom a) where
 instance PrettyCode Natural where
   ppCode = return . pretty
 
-instance PrettyCode Position where
-  ppCode p = case p ^. positionDirections of
+instance PrettyCode Path where
+  ppCode = \case
     [] -> return "S"
     ds -> mconcatMapM ppCode ds
 

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

@@ -74,7 +74,7 @@ atomDirection = do
   dirs <-
     symbol "S" $> []
       <|> NonEmpty.toList <$> some (choice [symbol "L" $> N.L, symbol "R" $> N.R])
-  return (N.Atom (N.serializePosition (N.Position dirs)) (Irrelevant (Just N.AtomHintPosition)))
+  return (N.Atom (N.serializePath dirs) (Irrelevant (Just N.AtomHintPath)))
 
 atomNat :: Parser (N.Atom Natural)
 atomNat = (\n -> N.Atom n (Irrelevant Nothing)) <$> dottedNatural