0 | module Text.ILex.Shunting
  1 |
  2 | import Text.ByteBounds
  3 | import Derive.Prelude
  4 |
  5 | %default total
  6 | %language ElabReflection
  7 |
  8 | --------------------------------------------------------------------------------
  9 | -- Operator Precedence
 10 | --------------------------------------------------------------------------------
 11 |
 12 | ||| Infix operator associativity
 13 | public export
 14 | data Assoc = None | InfixR | InfixL
 15 |
 16 | %runElab derive "Assoc" [Show,Eq,Ord]
 17 |
 18 | export
 19 | Interpolation Assoc where
 20 |   interpolate None   = "infix"
 21 |   interpolate InfixR = "infixr"
 22 |   interpolate InfixL = "infixl"
 23 |
 24 | ||| Infix operator associativity and precedence
 25 | public export
 26 | data Precedence : Type where
 27 |   Prefix  : (prec : Nat) -> Precedence
 28 |   Postfix : (prec : Nat) -> Precedence
 29 |   Infix   : (prec : Nat) -> (assoc : Assoc) -> Precedence
 30 |
 31 | %runElab derive "Precedence" [Show,Eq]
 32 |
 33 | export
 34 | Interpolation Precedence where
 35 |   interpolate (Prefix p)  = "prefix \{show p}"
 36 |   interpolate (Postfix p) = "postfix \{show p}"
 37 |   interpolate (Infix p a) = "\{a} \{show p}"
 38 |
 39 | export %inline
 40 | Cast a Precedence => Cast (ByteBounded a) Precedence where
 41 |   cast = cast . val
 42 |
 43 | export %inline
 44 | toPrec : Cast o Precedence => o -> Precedence
 45 | toPrec = cast
 46 |
 47 | export
 48 | prec : Cast o Precedence => o -> Nat
 49 | prec v =
 50 |   case toPrec v of
 51 |     Prefix p  => p
 52 |     Postfix p => p
 53 |     Infix p _ => p
 54 |
 55 | public export
 56 | data ShuntingErr : Type -> Type where
 57 |   AssocNone      : (op : o) -> (prec : Precedence) -> ShuntingErr o
 58 |
 59 | %runElab derive "ShuntingErr" [Show,Eq]
 60 |
 61 | export
 62 | Interpolation o => Interpolation (ShuntingErr o) where
 63 |   interpolate (AssocNone op p) = "operator '\{op}' (\{p}) is non-associative"
 64 |
 65 | ||| Shunting yard algorithm input token.
 66 | ||| A token is either a term followed by an infix operator
 67 | ||| or a single prefix operator
 68 | public export
 69 | data Tok : (t,p,i,o : Type) -> Type where
 70 |   TPre : ByteBounded p -> (prec : Nat) -> Tok t p i o
 71 |   TInf : t -> ByteBounded i -> (prec : Nat) -> Assoc -> Tok t p i o
 72 |   TPst : ByteBounded o -> (prec : Nat) -> Tok t p i o
 73 |
 74 | %runElab derive "Tok" [Show,Eq]
 75 |
 76 | export
 77 | Cast (Tok t p i o) Precedence where
 78 |   cast (TPre _ p)     = Prefix p
 79 |   cast (TInf _ _ p a) = Infix p a
 80 |   cast (TPst _ p)     = Postfix p
 81 |
 82 | public export
 83 | 0 Toks : (t,p,i,o : Type) -> Type
 84 | Toks t p i o = List (Tok t p i o)
 85 |
 86 | public export
 87 | 0 Skot : (t,p,i,o : Type) -> Type
 88 | Skot t p i o = SnocList (Tok t p i o)
 89 |
 90 | --------------------------------------------------------------------------------
 91 | -- Shunting Yard Implementation
 92 | --------------------------------------------------------------------------------
 93 |
 94 | parameters {0 t,p,i,o,e : Type}
 95 |            {auto cst    : Cast (ShuntingErr i) e}
 96 |            (pre         : ByteBounded p -> t -> t)
 97 |            (inf         : t -> ByteBounded i -> t -> t)
 98 |            (pst         : ByteBounded o -> t -> t)
 99 |
100 |   0 Res : Type
101 |   Res = Either (ByteBounded e) (Skot t p i o)
102 |
103 |   err : ByteBounded i -> Precedence -> Either (ByteBounded e) a
104 |   err op p = Left (B (cast $ AssocNone op.val p) op.bounds)
105 |
106 |   app : Tok t p i o -> t -> t
107 |   app (TPre op _)     y = pre op y
108 |   app (TInf x op _ _) y = inf x op y
109 |   app (TPst op _)     y = pst op y
110 |
111 |   apply : Skot t p i o -> t -> t
112 |   apply [<]     lst = lst
113 |   apply (si:<i) lst = apply si (app i lst)
114 |
115 |   insInf : Skot t p i o -> t -> ByteBounded i -> Nat -> Assoc -> Res
116 |   insInf [<]     lst op n a = Right $ [<TInf lst op n a]
117 |   insInf (si:<i) lst op n a =
118 |     case compare (prec i) n of
119 |       LT => Right $ si:<i:<TInf lst op n a
120 |       GT => insInf si (app i lst) op n a
121 |       EQ =>
122 |        let False := InfixL == a | True => insInf si (app i lst) op n a
123 |            False := None == a   | True => err op $ Infix n a
124 |            TInf _ o _ x := i    | _    => Right $ si:<i:<TInf lst op n a
125 |            False := None == x   | True => err o $ Infix n x
126 |         in Right $ si:<i:<TInf lst op n a
127 |
128 |   impl : Skot t p i o -> Toks t p i o -> t -> Either (ByteBounded e) t
129 |   impl si []      lst = Right $ apply si lst
130 |   impl si (i::is) lst =
131 |     case i of
132 |       TPre op n     => impl (si:<TPre op n) is lst
133 |       TInf t op n a => case insInf si t op n a of
134 |         Left err  => Left err
135 |         Right si2 => impl si2 is lst
136 |       TPst op n     => impl (si:<TPst op n) is lst
137 |
138 |   ||| An implementation of the
139 |   ||| [shunting yard algorithm](https://en.wikipedia.org/wiki/Shunting_yard_algorithm)
140 |   ||| used to convert term-operator chains such as `1 + 2 * 3 ^ 4` to proper
141 |   ||| syntax trees based on the operators' associativity and precedence.
142 |   export %inline
143 |   shuntingYard : Skot t p i o -> t -> Either (ByteBounded e) t
144 |   shuntingYard = impl [<] . (<>> [])
145 |