0 | module Libraries.Utils.Shunting
  1 |
  2 | import Core.Context.Context
  3 | import Core.Core
  4 | import Core.FC
  5 |
  6 | %default total
  7 |
  8 | -- The shunting yard algorithm turns a list of tokens with operators into
  9 | -- a parse tree expressing the precedence and associativity correctly.
 10 | -- We assume that brackets, functions etc are dealt with in a higher level
 11 | -- parser, so we're only dealing with operators here.
 12 |
 13 | -- Precedences/associativities
 14 | public export
 15 | data OpPrec
 16 |           = AssocL Nat
 17 |           | AssocR Nat
 18 |           | NonAssoc Nat
 19 |           | Prefix Nat
 20 |
 21 | -- Tokens are either operators or already parsed expressions in some
 22 | -- higher level language
 23 | public export
 24 | data Tok : (op, a : Type) ->  Type where
 25 |     Op : (expressionLoc : FC) -> (operatorLoc : FC) -> (operatorInfo : op) -> OpPrec -> Tok op a
 26 |     Expr : a -> Tok op a
 27 |
 28 | -- The result of shunting is a parse tree with the precedences made explicit
 29 | -- in the tree.
 30 | -- NOTE: I have been wondering if I can use types to express that the
 31 | -- subtrees use lower precedence operators, but my attempts so far have
 32 | -- ended up with more complicated types than the function 'higher', below,
 33 | -- which is the one that compares precedences. So I've just used simple
 34 | -- types instead and will rely on tests. It would be interesting to see if
 35 | -- there's a better way though!
 36 |
 37 | public export
 38 | data Tree op a = Infix FC FC op (Tree op a) (Tree op a)
 39 |                | Pre FC FC op (Tree op a)
 40 |                | Leaf a
 41 |
 42 | public export
 43 | Bifunctor Tree where
 44 |   bimap f g (Infix fc fc1 x y z) = Infix fc fc1 (f x) (bimap f g y) (bimap f g z)
 45 |   bimap f g (Pre fc fc1 x y) = Pre fc fc1 (f x) (bimap f g y)
 46 |   bimap f g (Leaf x) = Leaf (g x)
 47 |
 48 | export
 49 | (Show op, Show a) => Show (Tree op a) where
 50 |   show (Infix _ _ op l r) = "(" ++ show op ++ " " ++ show l ++ " " ++ show r ++ ")"
 51 |   show (Pre _ _ op l) = "(" ++  show op ++ " " ++ show l ++ ")"
 52 |   show (Leaf val) = show val
 53 |
 54 | Show OpPrec where
 55 |   show (AssocL p) = "infixl " ++ show p
 56 |   show (AssocR p) = "infixr " ++ show p
 57 |   show (NonAssoc p) = "infix " ++ show p
 58 |   show (Prefix p) = "prefix " ++ show p
 59 |
 60 | export
 61 | (Show op, Show a) => Show (Tok op a) where
 62 |   show (Op _ _ op p) = show op ++ " " ++ show p
 63 |   show (Expr val) = show val
 64 |
 65 | -- Label for the output queue state
 66 | data Out : Type where
 67 |
 68 | output : List (Tree op a) -> Tok op a ->
 69 |          Core (List (Tree op a))
 70 | output [] (Op {}) = throw (InternalError "Invalid input to shunting")
 71 | output (x :: stk) (Op loc opFC str (Prefix _)) = pure $ Pre loc opFC str x :: stk
 72 | output (x :: y :: stk) (Op loc opFC str _) = pure $ Infix loc opFC str y x :: stk
 73 | output stk (Expr a) = pure $ Leaf a :: stk
 74 | output _ _ = throw (InternalError "Invalid input to shunting")
 75 |
 76 | emit : {auto o : Ref Out (List (Tree op a))} ->
 77 |        Tok op a -> Core ()
 78 | emit t
 79 |     = do out <- get Out
 80 |          put Out !(output out t)
 81 |
 82 | getPrec : OpPrec -> Nat
 83 | getPrec (AssocL k) = k
 84 | getPrec (AssocR k) = k
 85 | getPrec (NonAssoc k) = k
 86 | getPrec (Prefix k) = k
 87 |
 88 | isLAssoc : OpPrec -> Bool
 89 | isLAssoc (AssocL _) = True
 90 | isLAssoc _ = False
 91 |
 92 | -- Return whether the first operator should be applied before the second.
 93 | -- Interpolation to show the operator naked, show to print the operator with its location
 94 | higher : Interpolation op => (showLoc : Show op) => FC -> op -> OpPrec -> op -> OpPrec -> Core Bool
 95 | higher loc opx op opy (Prefix p) = pure False
 96 | higher loc opx (NonAssoc x) opy oy
 97 |     = if x == getPrec oy
 98 |          then throw (GenericMsgSol loc "Operator \{opx} is non-associative" "Possible solutions"
 99 |                                        [ "Add brackets around every use of \{opx}"
100 |                                        , "Change the fixity of \{show opx} to `infixl` or `infixr`"])
101 |          else pure (x > getPrec oy)
102 | higher loc opx ox opy (NonAssoc y)
103 |     = if getPrec ox == y
104 |          then throw (GenericMsgSol loc "Operator \{opy} is non-associative" "Possible solutions"
105 |                                        [ "Add brackets around every use of \{opy}"
106 |                                        , "Change the fixity of \{show opy} to `infixl` or `infixr`"])
107 |          else pure (getPrec ox > y)
108 | higher loc opl l opr r
109 |     = pure $ (getPrec l > getPrec r) ||
110 |              ((getPrec l == getPrec r) && isLAssoc l)
111 |
112 | processStack : Interpolation op => (showLoc : Show op) => {auto o : Ref Out (List (Tree op a))} ->
113 |                List (FC, FC, op, OpPrec) -> op -> OpPrec ->
114 |                Core (List (FC, FC, op, OpPrec))
115 | processStack [] op prec = pure []
116 | processStack (x@(loc, opFC, opx, sprec) :: xs) opy prec
117 |     = if !(higher loc opx sprec opy prec)
118 |          then do emit (Op loc opFC opx sprec)
119 |                  processStack xs opy prec
120 |          else pure (x :: xs)
121 |
122 | shunt : Interpolation op => (showLoc : Show op) => {auto o : Ref Out (List (Tree op a))} ->
123 |         (opstk : List (FC, FC, op, OpPrec)) ->
124 |         List (Tok op a) -> Core (Tree op a)
125 | shunt stk (Expr x :: rest)
126 |     = do emit (Expr x)
127 |          shunt stk rest
128 | shunt stk (Op loc opFC op prec :: rest)
129 |     = do stk' <- processStack stk op prec
130 |          shunt ((loc, opFC, op, prec) :: stk') rest
131 | shunt stk []
132 |     = do traverse_ (emit . mkOp) stk
133 |          [out] <- get Out
134 |              | out => throw (InternalError "Invalid input to shunting")
135 |          pure out
136 |   where
137 |     mkOp : (FC, FC, op, OpPrec) -> Tok op a
138 |     mkOp (loc, opFC, op, prec) = Op loc opFC op prec
139 |
140 | export
141 | parseOps : Interpolation op => (showLoc : Show op) => List (Tok op a) -> Core (Tree op a)
142 | parseOps toks
143 |     = do o <- newRef {t = List (Tree op a)} Out []
144 |          shunt [] toks
145 |