289 | "injval (ALT r1 r2) c (Right v2) = Right(injval r2 c v2)" |
289 | "injval (ALT r1 r2) c (Right v2) = Right(injval r2 c v2)" |
290 | "injval (SEQ r1 r2) c (Seq v1 v2) = Seq (injval r1 c v1) v2" |
290 | "injval (SEQ r1 r2) c (Seq v1 v2) = Seq (injval r1 c v1) v2" |
291 | "injval (SEQ r1 r2) c (Left (Seq v1 v2)) = Seq (injval r1 c v1) v2" |
291 | "injval (SEQ r1 r2) c (Left (Seq v1 v2)) = Seq (injval r1 c v1) v2" |
292 | "injval (SEQ r1 r2) c (Right v2) = Seq (mkeps r1) (injval r2 c v2)" |
292 | "injval (SEQ r1 r2) c (Right v2) = Seq (mkeps r1) (injval r2 c v2)" |
293 | "injval (STAR r) c (Seq v (Stars vs)) = Stars ((injval r c v) # vs)" |
293 | "injval (STAR r) c (Seq v (Stars vs)) = Stars ((injval r c v) # vs)" |
294 |
|
295 |
|
296 section {* Matcher *} |
|
297 |
|
298 fun |
|
299 matcher :: "rexp \<Rightarrow> string \<Rightarrow> val option" |
|
300 where |
|
301 "matcher r [] = (if nullable r then Some(mkeps r) else None)" |
|
302 | "matcher r (c#s) = (case (matcher (der c r) s) of |
|
303 None \<Rightarrow> None |
|
304 | Some(v) \<Rightarrow> Some(injval r c v))" |
|
305 |
294 |
306 |
295 |
307 section {* Mkeps, injval *} |
296 section {* Mkeps, injval *} |
308 |
297 |
309 lemma mkeps_nullable: |
298 lemma mkeps_nullable: |
603 have "((c # s1) @ s2) \<in> STAR r \<rightarrow> Stars (injval r c v1 # vs)" by (rule PMatch.intros) |
592 have "((c # s1) @ s2) \<in> STAR r \<rightarrow> Stars (injval r c v1 # vs)" by (rule PMatch.intros) |
604 then show "(c # s) \<in> STAR r \<rightarrow> injval (STAR r) c v" using cons by(simp) |
593 then show "(c # s) \<in> STAR r \<rightarrow> injval (STAR r) c v" using cons by(simp) |
605 qed |
594 qed |
606 qed |
595 qed |
607 |
596 |
|
597 |
|
598 section {* The Lexer by Sulzmann and Lu *} |
|
599 |
|
600 fun |
|
601 lexer :: "rexp \<Rightarrow> string \<Rightarrow> val option" |
|
602 where |
|
603 "lexer r [] = (if nullable r then Some(mkeps r) else None)" |
|
604 | "lexer r (c#s) = (case (lexer (der c r) s) of |
|
605 None \<Rightarrow> None |
|
606 | Some(v) \<Rightarrow> Some(injval r c v))" |
|
607 |
|
608 |
|
609 |
608 lemma lex_correct1: |
610 lemma lex_correct1: |
609 assumes "s \<notin> L r" |
611 assumes "s \<notin> L r" |
610 shows "matcher r s = None" |
612 shows "lexer r s = None" |
611 using assms |
613 using assms |
612 apply(induct s arbitrary: r) |
614 apply(induct s arbitrary: r) |
613 apply(simp add: nullable_correctness) |
615 apply(simp add: nullable_correctness) |
614 apply(drule_tac x="der a r" in meta_spec) |
616 apply(drule_tac x="der a r" in meta_spec) |
615 apply(auto simp add: der_correctness Der_def) |
617 apply(auto simp add: der_correctness Der_def) |
616 done |
618 done |
617 |
619 |
618 lemma lex_correct1a: |
620 lemma lex_correct1a: |
619 shows "s \<notin> L r \<longleftrightarrow> matcher r s = None" |
621 shows "s \<notin> L r \<longleftrightarrow> lexer r s = None" |
620 using assms |
622 using assms |
621 apply(induct s arbitrary: r) |
623 apply(induct s arbitrary: r) |
622 apply(simp add: nullable_correctness) |
624 apply(simp add: nullable_correctness) |
623 apply(drule_tac x="der a r" in meta_spec) |
625 apply(drule_tac x="der a r" in meta_spec) |
624 apply(auto simp add: der_correctness Der_def) |
626 apply(auto simp add: der_correctness Der_def) |
625 done |
627 done |
626 |
628 |
627 lemma lex_correct2: |
629 lemma lex_correct2: |
628 assumes "s \<in> L r" |
630 assumes "s \<in> L r" |
629 shows "\<exists>v. matcher r s = Some(v) \<and> \<turnstile> v : r \<and> flat v = s" |
631 shows "\<exists>v. lexer r s = Some(v) \<and> \<turnstile> v : r \<and> flat v = s" |
630 using assms |
632 using assms |
631 apply(induct s arbitrary: r) |
633 apply(induct s arbitrary: r) |
632 apply(simp) |
634 apply(simp) |
633 apply (metis mkeps_flat mkeps_nullable nullable_correctness) |
635 apply (metis mkeps_flat mkeps_nullable nullable_correctness) |
634 apply(drule_tac x="der a r" in meta_spec) |
636 apply(drule_tac x="der a r" in meta_spec) |
639 apply(rule Prf_injval_flat) |
641 apply(rule Prf_injval_flat) |
640 by simp |
642 by simp |
641 |
643 |
642 lemma lex_correct3: |
644 lemma lex_correct3: |
643 assumes "s \<in> L r" |
645 assumes "s \<in> L r" |
644 shows "\<exists>v. matcher r s = Some(v) \<and> s \<in> r \<rightarrow> v" |
646 shows "\<exists>v. lexer r s = Some(v) \<and> s \<in> r \<rightarrow> v" |
645 using assms |
647 using assms |
646 apply(induct s arbitrary: r) |
648 apply(induct s arbitrary: r) |
647 apply(simp) |
649 apply(simp) |
648 apply (metis PMatch_mkeps nullable_correctness) |
650 apply (metis PMatch_mkeps nullable_correctness) |
649 apply(drule_tac x="der a r" in meta_spec) |
651 apply(drule_tac x="der a r" in meta_spec) |
651 apply(simp add: der_correctness Der_def) |
653 apply(simp add: der_correctness Der_def) |
652 apply(auto) |
654 apply(auto) |
653 by (metis PMatch2_roy_version) |
655 by (metis PMatch2_roy_version) |
654 |
656 |
655 lemma lex_correct3a: |
657 lemma lex_correct3a: |
656 shows "s \<in> L r \<longleftrightarrow> (\<exists>v. matcher r s = Some(v) \<and> s \<in> r \<rightarrow> v)" |
658 shows "s \<in> L r \<longleftrightarrow> (\<exists>v. lexer r s = Some(v) \<and> s \<in> r \<rightarrow> v)" |
657 using assms |
659 using assms |
658 apply(induct s arbitrary: r) |
660 apply(induct s arbitrary: r) |
659 apply(simp) |
661 apply(simp) |
660 apply (metis PMatch_mkeps nullable_correctness) |
662 apply (metis PMatch_mkeps nullable_correctness) |
661 apply(drule_tac x="der a r" in meta_spec) |
663 apply(drule_tac x="der a r" in meta_spec) |
666 apply fastforce |
668 apply fastforce |
667 apply(simp add: der_correctness Der_def) |
669 apply(simp add: der_correctness Der_def) |
668 by (simp add: lex_correct1a) |
670 by (simp add: lex_correct1a) |
669 |
671 |
670 lemma lex_correct3b: |
672 lemma lex_correct3b: |
671 shows "s \<in> L r \<longleftrightarrow> (\<exists>!v. matcher r s = Some(v) \<and> s \<in> r \<rightarrow> v)" |
673 shows "s \<in> L r \<longleftrightarrow> (\<exists>!v. lexer r s = Some(v) \<and> s \<in> r \<rightarrow> v)" |
672 using assms |
674 using assms |
673 apply(induct s arbitrary: r) |
675 apply(induct s arbitrary: r) |
674 apply(simp) |
676 apply(simp) |
675 apply (metis PMatch_mkeps nullable_correctness) |
677 apply (metis PMatch_mkeps nullable_correctness) |
676 apply(drule_tac x="der a r" in meta_spec) |
678 apply(drule_tac x="der a r" in meta_spec) |
677 apply(simp add: der_correctness Der_def) |
679 apply(simp add: der_correctness Der_def) |
678 apply(case_tac "matcher (der a r) s = None") |
680 apply(case_tac "lexer (der a r) s = None") |
679 apply(simp) |
681 apply(simp) |
680 apply(simp) |
682 apply(simp) |
681 apply(clarify) |
683 apply(clarify) |
682 apply(rule iffI) |
684 apply(rule iffI) |
683 apply(auto) |
685 apply(auto) |
684 apply(rule PMatch2_roy_version) |
686 apply(rule PMatch2_roy_version) |
685 apply(simp) |
687 apply(simp) |
686 using PMatch1(1) by auto |
688 using PMatch1(1) by auto |
|
689 |
|
690 section {* Lexer including simplifications *} |
687 |
691 |
688 |
692 |
689 fun F_RIGHT where |
693 fun F_RIGHT where |
690 "F_RIGHT f v = Right (f v)" |
694 "F_RIGHT f v = Right (f v)" |
691 |
695 |
721 "simp (ALT r1 r2) = simp_ALT (simp r1) (simp r2)" |
725 "simp (ALT r1 r2) = simp_ALT (simp r1) (simp r2)" |
722 | "simp (SEQ r1 r2) = simp_SEQ (simp r1) (simp r2)" |
726 | "simp (SEQ r1 r2) = simp_SEQ (simp r1) (simp r2)" |
723 | "simp r = (r, id)" |
727 | "simp r = (r, id)" |
724 |
728 |
725 fun |
729 fun |
726 matcher3 :: "rexp \<Rightarrow> string \<Rightarrow> val option" |
730 slexer :: "rexp \<Rightarrow> string \<Rightarrow> val option" |
727 where |
731 where |
728 "matcher3 r [] = (if nullable r then Some(mkeps r) else None)" |
732 "slexer r [] = (if nullable r then Some(mkeps r) else None)" |
729 | "matcher3 r (c#s) = (let (rs, fr) = simp (der c r) in |
733 | "slexer r (c#s) = (let (rs, fr) = simp (der c r) in |
730 (case (matcher3 rs s) of |
734 (case (slexer rs s) of |
731 None \<Rightarrow> None |
735 None \<Rightarrow> None |
732 | Some(v) \<Rightarrow> Some(injval r c (fr v))))" |
736 | Some(v) \<Rightarrow> Some(injval r c (fr v))))" |
733 |
737 |
734 end |
738 end |