0 | module TyRE.Parser.SMConstruction
  1 |
  2 | import Data.List
  3 | import Data.DPair
  4 |
  5 | import TyRE.Core
  6 | import TyRE.Parser.SM
  7 | import TyRE.Parser.GroupThompson
  8 |
  9 | ||| Compile function creates a state machine from an untyped regex
 10 | export
 11 | compile : {0 a : Type} -> (tyre : TyRE a) -> SM a
 12 | --sm for empty language
 13 | compile Empty =
 14 |   let lookup : Void -> SnocList Type
 15 |       lookup _ impossible
 16 |       init : InitStatesType () Void lookup
 17 |       init = [(Nothing ** [< Push ()] `Element` [< InitPush])]
 18 |       next : TransitionRelation () Void lookup
 19 |       next _ _ = []
 20 |   in MkSM Void lookup init next
 21 | --sm for predicate
 22 | compile (MatchChar f) =
 23 |   let lookup : () -> SnocList Type
 24 |       lookup () = [< ]
 25 |       init : InitStatesType Char () lookup
 26 |       init = [(Just () ** [<] `Element` [<])]
 27 |       next : TransitionRelation Char () lookup
 28 |       next () c =
 29 |         if satisfies f c
 30 |         then [(Nothing ** [< PushChar])]
 31 |         else []
 32 |   in MkSM () lookup init next
 33 | --sm for concatenation
 34 | compile ((<*>) {a,b} x y) =
 35 |   let MkSM s1 l1 i1 n1 := compile x
 36 |       MkSM s2 l2 i2 n2 := compile y
 37 |       0 T : Type
 38 |       T = Either s1 s2
 39 |       0 lookup : T -> SnocList Type
 40 |       lookup (Left s)  = l1 s
 41 |       lookup (Right s) = [< a] ++ l2 s
 42 |       init : InitStatesType (a, b) T lookup
 43 |       init =
 44 |         (i1 >>=
 45 |           (\case
 46 |             (Nothing ** r `Element` p) =>
 47 |               map (\case
 48 |                     (Nothing ** r2 `Element` p2) =>
 49 |                       (Nothing
 50 |                       ** r ++ lift r2 :< ReducePair MkPair `Element`
 51 |                          p ++ lift p2 :< InitReducePair)
 52 |                     (Just st ** r2 `Element` p2) =>
 53 |                       (Just (Right st)
 54 |                       ** (r ++ lift r2) `Element`
 55 |                          (p ++ lift p2)))
 56 |               i2
 57 |             (Just st ** r) => [(Just (Left st) ** r)]))
 58 |       next : TransitionRelation (a,b) T lookup
 59 |       next (Left st) c =
 60 |         (n1 st c >>=
 61 |           (\case
 62 |             (Nothing ** r) =>
 63 |               map (\case
 64 |                     (Nothing ** r2 `Element` _) =>
 65 |                       (Nothing
 66 |                       ** r ++ lift r2 :< ReducePair MkPair)
 67 |                     (Just s2 ** r2 `Element` _) =>
 68 |                       (Just (Right s2)
 69 |                       ** r ++ lift r2))
 70 |                   i2
 71 |             (Just st ** r) => [(Just (Left st) ** r)]))
 72 |       next (Right st) c =
 73 |         map (\case
 74 |                 (Nothing ** r) => (Nothing ** lift r :< ReducePair MkPair)
 75 |                 (Just st ** r) => (Just (Right st) ** lift r))
 76 |               (n2 st c)
 77 |   in MkSM T lookup init next
 78 | -- sm for alternation
 79 | compile ((<|>) {a,b} x y) =
 80 |   let MkSM s1 l1 i1 n1 := compile x
 81 |       MkSM s2 l2 i2 n2 := compile y
 82 |       0 T : Type
 83 |       T = Either s1 s2
 84 |       0 lookup : T -> SnocList Type
 85 |       lookup (Left s)  = l1 s
 86 |       lookup (Right s) = l2 s
 87 |       init : InitStatesType (Either a b) T lookup
 88 |       init = map  (\case
 89 |                       (Nothing ** rt `Element` p) =>
 90 |                         (Nothing
 91 |                         ** rt :< Transform Left `Element`
 92 |                            p :< InitTransform)
 93 |                       (Just st ** r) => (Just (Left st) ** r))
 94 |                   i1
 95 |            ++ map (\case
 96 |                       (Nothing ** rt `Element` p) =>
 97 |                         (Nothing
 98 |                         ** rt :< (Transform Right) `Element`
 99 |                            p :< InitTransform)
100 |                       (Just st ** r) => (Just (Right st) ** r))
101 |                   i2
102 |       next : TransitionRelation (Either a b) T lookup
103 |       next (Left s) c =
104 |         map (\case
105 |                 (Nothing ** rt) =>
106 |                   (Nothing ** rt :< Transform Left)
107 |                 (Just st ** rt) => (Just (Left st) ** rt))
108 |             (n1 s c)
109 |       next (Right s) c =
110 |         map (\case
111 |                 (Nothing ** rt) =>
112 |                   (Nothing ** rt :< Transform Right)
113 |                 (Just st ** rt) => (Just (Right st) ** rt))
114 |             (n2 s c)
115 |   in MkSM T lookup init next
116 | -- sm for Kleene star
117 | compile (Rep {a} re) =
118 |   let MkSM t lookupPrev initPrev nextPrev := compile re
119 |       0 T : Type
120 |       T = t
121 |       0 lookup : T -> SnocList Type
122 |       lookup s = [< SnocList a] ++ lookupPrev s
123 |       init : InitStatesType (SnocList a) T lookup
124 |       init = (Nothing ** [< Push [<]] `Element` [< InitPush])
125 |            :: map (\case
126 |                     (Nothing ** r `Element` p) =>
127 |                       (Nothing ** [< Push [<]] `Element` [< InitPush])
128 |                     (Just st ** r `Element` p) =>
129 |                       (Just st ** ([< Push Prelude.Basics.Lin] ++ lift r)
130 |                         `Element` ([< InitPush] ++ lift p)))
131 |                   initPrev
132 |       next : TransitionRelation (SnocList a) T lookup
133 |       next s c =
134 |         (nextPrev s c) >>=
135 |           \case
136 |             (Nothing ** r) =>
137 |                 (Nothing ** lift r :< ReducePair (:<))
138 |               :: map (\case
139 |                         (Nothing ** r2 `Element` _) =>
140 |                           (Nothing ** lift r :< ReducePair (:<))
141 |                         (Just st ** r2 `Element` _) =>
142 |                           (Just st ** lift r :< ReducePair (:<) ++ lift r2))
143 |                       initPrev
144 |             (Just st ** r) => [(Just st ** lift r)]
145 |   in MkSM T lookup init next
146 | -- sm for group made
147 | compile {a = String} (Group r) = asSM (groupSM r) where
148 |   asSM : GroupSM -> SM String
149 |   asSM (MkGroupSM initStates statesWithNext max) =
150 |     let lookup : Nat -> SnocList Type
151 |         lookup _ = [<]
152 |         init : InitStatesType String Nat lookup
153 |         init = map (\case
154 |                       Just s => (Just s ** [< Record] `Element` [< InitRecord])
155 |                       Nothing => (Nothing ** [< EmitString] `Element`
156 |                                              [< InitEmitString]))
157 |                    initStates
158 |         next : TransitionRelation String Nat lookup
159 |         next s c with (find (\case (n, ns) => n == s) statesWithNext)
160 |           next s c | Nothing = []
161 |           next s c | (Just (_, (MkNextStates condition isSat))) =
162 |             if satisfies condition c
163 |             then map (\case
164 |                         Nothing => (Nothing ** [< EmitString])
165 |                         Just s => (Just s ** [<])) isSat
166 |             else []
167 |     in MkSM Nat lookup init next
168 | compile (Conv {a,b} re f) =
169 |   let MkSM t lookup initPrev nextPrev := compile re
170 |       init : InitStatesType b t lookup
171 |       init = map (\case
172 |                     (Nothing ** r `Element` p) =>
173 |                       (Nothing ** r :< Transform f `Element`
174 |                                        p :< InitTransform)
175 |                     (Just st ** rp) => (Just st ** rp))
176 |                  initPrev
177 |       next : TransitionRelation b t lookup
178 |       next st c = map (\case
179 |                           (Nothing ** r) => (Nothing ** r :< Transform f)
180 |                           (Just st ** r) => (Just st ** r))
181 |                       (nextPrev st c)
182 |   in MkSM t lookup init next
183 |