Lines Matching refs:shift
57 (shift _ (MEps) _ = MEps ) /\
58 (shift m (MSym _ x) c = MSym (m /\ (x = c)) x ) /\
59 (shift m (MAlt p q) c = MAlt (shift m p c) (shift m q c) ) /\
60 (shift m (MSeq p q) c = MSeq (shift m p c) (shift ((m /\ (empty p)) \/ final p) q c)) /\
61 (shift m (MRep r) c = MRep (shift (m \/ (final r)) r c) )
68 (acceptM r (c::cs) = final (FOLDL (shift F) (shift T r c) cs))
130 (* rewrites for shift *)
132 (!m c. shift m (MEps) c = MEps ) /\
133 (!m b x c. shift m (MSym b x) c = MSym (m /\ (x = c)) x ) /\
134 (!m p q c. shift m (MAlt p q) c = MAlt (shift m p c) (shift m q c) ) /\
135 (!m p q c. shift m (MSeq p q) c = MSeq (shift m p c) (shift ((m /\ (empty p)) \/ final p) q c)) /\
136 (!m r c. shift m (MRep r) c = MRep (shift (m \/ (final r)) r c) )
145 (!r c cs. acceptM r (c::cs) = final (FOLDL (shift F) (shift T r c) cs))
331 (* --------------------- shift *)
333 (* m means whether to shift marks in from the left, and c says which "next positions" are to be marked *)
336 (* final (shift m r c) <=> ? *)
339 (!mr c. (~HAS_MARKS mr) ==> ((shift F mr c) = mr))
348 (!mr m c. ((UNMARK_REG (shift m mr c)) = (UNMARK_REG mr)))
379 (!mr c cs m. (cs IN (lang_of_MF (shift m mr c))) <=>
497 (cs IN (lang_of_MF (shift T mr c)) <=>
506 (!mr w. (final (FOLDL (shift F) mr w)) <=> (w IN (lang_of_MF mr)))
520 (acceptM r ((c:'a)::cs) = final (FOLDL (shift F) (shift T r c) cs))