formal-languages/context-free/simpleSexpParseScript.sml

12   Induct \\ simp[listTheory.DROP_def] \\ rw[]);
28   Induct \\ rw[EQ_IMP_THM] \\ rw[]
39   rw[n2s_def,rich_listTheory.EVERY_REVERSE,listTheory.EVERY_MAP]
48   rw[num_to_dec_string_def,EVERY_isDigit_n2s]);
52   rw[n2s_def,listTheory.NULL_EQ]
59   rw[num_to_dec_string_def,n2s_not_null]);
73   simp[stringTheory.isDigit_def] \\ rw[]
92   \\ rw[] \\ simp[GSYM isDigit_UNHEX_alt,isDigit_ORD_MOD_10]);
97   rw[num_to_dec_string_def,num_from_dec_string_def]
100   \\ rw[]
101   \\ qspecl_then[`10`,`n`]mp_tac numposrepTheory.l2n_n2l \\ rw[]
109   \\ rw[] \\ res_tac \\ simp[UNHEX_HEX]);
114   rw[Once peg_eval_list,peg_eval_tok_NONE,listTheory.EVERY_MEM]
121   Induct \\ rw[Once peg_eval_list,listTheory.NULL_EQ,peg_eval_tok_SOME]
126   \\ rw[] \\ fs[listTheory.NULL_EQ]);
133   \\ rw[]
168   Cases_on`xs` \\ rw[print_space_separated_def]);
181   ho_match_mp_tac strip_sxcons_ind \\ rw[]
182   \\ rw[Once strip_sxcons_def]
184   \\ TRY(simp[Once strip_dot_def] \\ rw[] \\ NO_TAC)
186   \\ simp[] \\ pairarg_tac \\ fs[] \\ rw[EQ_IMP_THM]);
190   ho_match_mp_tac strip_dot_ind \\ rw[]
195   \\ rw[sexp_size_def] \\ simp[]
196   \\ rw[sexp_size_def]);
200   ho_match_mp_tac strip_dot_ind \\ rw[]
205   \\ rw[sexp_size_def] \\ simp[]
206   \\ rw[sexp_size_def]
208   \\ TRY (spose_not_then strip_assume_tac \\ fs[] \\ rw[] \\ fs[] \\ NO_TAC)
213   \\ rw[] \\ fs[]);
217   ho_match_mp_tac strip_dot_ind \\ rw[]
222   \\ rw[sexp_size_def] \\ fs[]
228   ho_match_mp_tac strip_dot_ind \\ rw[]
231   \\ CASE_TAC \\ fs[] \\ rw[] \\ rw[]
232   \\ pairarg_tac \\ fs[] \\ rw[]);
247   (WF_REL_TAC`measure sexp_size` >> rw[] >> simp[sexp_size_def] >>
249    pairarg_tac \\ fs[] \\ rw[sexp_size_def] \\ fs[]
253    \\ fs[quantHeuristicsTheory.LIST_LENGTH_2] \\ rw[] \\ fs[]
269   rw[Once peg_eval_cases] >>
296   simp[destSXSYM_def] >> rw[] >>
297   rw[Once peg_eval_cases] >> simp[peg_eval_tok_NONE]);
301   Cases_on`s` \\ rw[valid_symbol_def]
304   \\ rw[]
312   \\ fs[listTheory.EVERY_MEM] \\ rw[]
330   \\ rw[] \\ fs[]
349   \\ rw[] \\ fs[] \\ simp[Once peg_eval_list]
389   \\ rw[] \\ rw[sexp_size_def]);
429   \\ rw[]
431     Induct_on`str` \\ rw[listTheory.list_size_def] \\ fs[] \\ NO_TAC)
442   Cases_on`s` \\ rw[print_nt_def] \\ rw[]
444     rw[GSYM listTheory.NULL_EQ,num_to_dec_string_not_null]
448     \\ rw[listTheory.NULL_EQ]
460   Cases_on`s` \\ rw[print_nt_def] \\ rw[]
462     rw[GSYM listTheory.NULL_EQ,num_to_dec_string_not_null]
466     \\ rw[listTheory.NULL_EQ]
483   \\ rw[Ntimes pnt_def 2,Ntimes peg_eval_NT_SOME 2,FDOM_sexpPEG,sexpPEG_applied,
505   rw[Once peg_eval_cases,FDOM_sexpPEG,sexpPEG_applied,peg_eval_choicel_CONS]
506   \\ rw[tokeq_def,pnt_def,pegf_def,ignoreR_def,ignoreL_def]
507   \\ rw[peg_eval_seq_SOME,peg_eval_seq_NONE,peg_eval_NT_SOME,FDOM_sexpPEG,sexpPEG_applied]
508   \\ rw[peg_eval_tok_SOME,peg_eval_tok_NONE]
509   \\ rw[pnt_def,peg_eval_NT_SOME,FDOM_sexpPEG,sexpPEG_applied,peg_eval_tok_SOME]
510   \\ EVAL_TAC \\ rw[]
511   \\ rw[Once peg_eval_cases,FDOM_sexpPEG,sexpPEG_applied]
512   \\ rw[peg_eval_seq_SOME,peg_eval_seq_NONE,peg_eval_NT_SOME,FDOM_sexpPEG,sexpPEG_applied]
513   \\ rw[peg_eval_tok_SOME,peg_eval_tok_NONE]
514   \\ rw[pnt_def,peg_eval_NT_SOME,FDOM_sexpPEG,sexpPEG_applied,peg_eval_tok_SOME]
515   \\ EVAL_TAC \\ rw[]
516   \\ rw[Once peg_eval_cases,FDOM_sexpPEG,sexpPEG_applied]
517   \\ rw[peg_eval_tok_SOME,peg_eval_tok_NONE]
518   \\ EVAL_TAC \\ rw[]
519   \\ rw[Once peg_eval_cases,FDOM_sexpPEG,sexpPEG_applied]
520   \\ rw[peg_eval_seq_SOME,peg_eval_seq_NONE,peg_eval_NT_SOME,FDOM_sexpPEG,sexpPEG_applied]
521   \\ rw[peg_eval_tok_SOME,peg_eval_tok_NONE]);
541     rw[print_nt_def,pnt_def,peg_eval_NT_SOME,FDOM_sexpPEG,sexpPEG_applied,
546     rw[print_nt_def,pnt_def,peg_eval_NT_SOME,FDOM_sexpPEG,sexpPEG_applied,
554     rw[print_nt_def,pnt_def,peg_eval_NT_SOME,FDOM_sexpPEG,sexpPEG_applied,
560     \\ Induct_on`str` \\ rw[] \\ fs[]
565         \\ rw[Once peg_eval_cases,FDOM_sexpPEG,sexpPEG_applied]
568         \\ rw[Once peg_eval_cases,FDOM_sexpPEG,sexpPEG_applied]
576       \\ rw[Once peg_eval_cases,FDOM_sexpPEG,sexpPEG_applied]
579       \\ rw[Once peg_eval_cases,FDOM_sexpPEG,sexpPEG_applied]
588       rw[Once peg_eval_list,PULL_EXISTS,
594     \\ Cases_on`strl` \\ fs[] \\ rw[]
595     \\ rw[Once peg_eval_list,PULL_EXISTS,
600     \\ rw[pairTheory.UNCURRY,destSXSYM_def] )
602     rw[print_nt_def,pnt_def,peg_eval_NT_SOME,FDOM_sexpPEG,sexpPEG_applied,
623     \\ disch_then(qspec_then`cs`mp_tac) \\ rw[]
625     \\ rw[]
627     \\ rw[FOLDR_STRCAT_destSXSYM_FST] )
629     rw[print_nt_def]
631     \\ fs[option_sequence_SOME] \\ rw[]
632     \\ rw[pnt_def,peg_eval_NT_SOME,FDOM_sexpPEG,sexpPEG_applied,peg_eval_choicel_CONS]
636       \\ Cases_on`n` \\ fs[] \\ rw[]
638       \\ rw[pegf_def,peg_eval_seq_SOME,tokeq_def,grabWS_def,ignoreL_def,peg_eval_tok_SOME,peg_eval_rpt,PULL_EXISTS]
642       \\ pop_assum mp_tac \\ rw[]
644       \\ qexists_tac`x0` \\ rw[]
652       rw[pegf_def,peg_eval_seq_NONE,grabWS_def,ignoreL_def,peg_eval_rpt,PULL_EXISTS,tokeq_def,peg_eval_tok_NONE]
669     \\ rw[peg_eval_seq_SOME]
674       rw[] \\ spose_not_then strip_assume_tac \\ fs[] \\ rw[] \\ fs[] \\ NO_TAC)
675     \\ pairarg_tac \\ fs[] \\ rw[] \\ fs[]
677     \\ rw[grabWS_def,ignoreL_def,peg_eval_seq_SOME,PULL_EXISTS,peg_eval_rpt]
693     \\ impl_tac >- rw[]
734       rw[]
737       \\ fs[] \\ rw[]
741         \\ rw[Once peg_eval_list,peg_eval_seq_NONE,peg_eval_rpt]
742         \\ rw[Once peg_eval_list,peg_eval_tok_NONE,stringTheory.isSpace_def,peg_eval_tok_SOME]
743         \\ rw[peg_eval_sexp0_NONE]
744         \\ rw[peg_eval_seq_SOME,peg_eval_rpt,PULL_EXISTS]
745         \\ rw[Once peg_eval_list,peg_eval_tok_NONE,peg_eval_tok_SOME]
746         \\ rw[stringTheory.isSpace_def]
747         \\ rw[peg_eval_sexp0_NONE]
748         \\ rw[peg_eval_choicel_CONS,pegf_def,peg_eval_seq_SOME,
751         \\ rw[peg_eval_tok_NONE,peg_eval_tok_SOME]
752         \\ rw[replace_nil_def]
753         \\ rw[Once peg_eval_list]
754         \\ rw[peg_eval_tok_NONE,peg_eval_tok_SOME]
755         \\ rw[stringTheory.isSpace_def]
757         \\ pop_assum mp_tac \\ CASE_TAC \\ fs[] \\ rw[]
762       \\ rw[Once peg_eval_list,peg_eval_seq_NONE,peg_eval_rpt,PULL_EXISTS,peg_eval_seq_SOME]
763       \\ rw[Once peg_eval_list,peg_eval_tok_NONE,peg_eval_tok_SOME]
764       \\ rw[stringTheory.isSpace_def,PULL_EXISTS]
765       \\ rw[Once peg_eval_list,peg_eval_tok_NONE,peg_eval_tok_SOME]
766       \\ rw[stringTheory.isSpace_def,PULL_EXISTS]
767       \\ rw[peg_eval_sexp0_NONE]
768       \\ rw[Once peg_eval_list,peg_eval_tok_NONE,peg_eval_tok_SOME]
769       \\ rw[stringTheory.isSpace_def,PULL_EXISTS]
770       \\ rw[Once peg_eval_list,peg_eval_tok_NONE,peg_eval_tok_SOME]
771       \\ rw[stringTheory.isSpace_def,PULL_EXISTS]
772       \\ rw[peg_eval_sexp0_NONE]
773       \\ rw[peg_eval_choicel_CONS,pegf_def,peg_eval_seq_SOME,
776       \\ rw[Once peg_eval_list,peg_eval_tok_NONE,peg_eval_tok_SOME]
777       \\ rw[stringTheory.isSpace_def,PULL_EXISTS]
778       \\ rw[Once peg_eval_list,peg_eval_tok_NONE,peg_eval_tok_SOME]
779       \\ rw[stringTheory.isSpace_def,PULL_EXISTS]
780       \\ rw[Once peg_eval_list,peg_eval_tok_NONE,peg_eval_tok_SOME]
781       \\ rw[stringTheory.isSpace_def,PULL_EXISTS]
782       \\ rw[Once peg_eval_list,peg_eval_tok_NONE,peg_eval_tok_SOME]
783       \\ rw[stringTheory.isSpace_def,PULL_EXISTS]
784       \\ rw[Once peg_eval_list,peg_eval_tok_NONE,peg_eval_tok_SOME]
785       \\ rw[stringTheory.isSpace_def,PULL_EXISTS]
786       \\ rw[Once peg_eval_list,peg_eval_tok_NONE,peg_eval_tok_SOME]
787       \\ rw[stringTheory.isSpace_def,PULL_EXISTS]
788       \\ rw[Once peg_eval_list,peg_eval_tok_NONE,peg_eval_tok_SOME]
789       \\ rw[stringTheory.isSpace_def,PULL_EXISTS]
790       \\ rw[replace_nil_def] \\ fs[]
791       \\ rw[Once peg_eval_list,peg_eval_tok_NONE,peg_eval_tok_SOME]
798         \\ CASE_TAC \\ rw[]
800       \\ rw[]
810       \\ impl_tac >- (simp[IN_DEF,MAP_FRONT] \\ EVAL_TAC \\ rw[]
815       \\ rw[Once peg_eval_list,peg_eval_tok_NONE,peg_eval_tok_SOME]
816       \\ rw[stringTheory.isSpace_def,PULL_EXISTS] )
817     \\ rw[] \\ fs[]
822     \\ rw[Once peg_eval_list]
826     \\ rw[Once peg_eval_list,peg_eval_tok_NONE,peg_eval_tok_SOME]
827     \\ rw[stringTheory.isSpace_def,PULL_EXISTS]
857     \\ rw[Once peg_eval_list,peg_eval_tok_NONE,peg_eval_tok_SOME]
864     \\ rw[replace_nil_def]
867     \\ CASE_TAC \\ rw[]
868     \\ pairarg_tac \\ fs[] \\ rw[])
870     rw[print_nt_def,pnt_def,peg_eval_NT_SOME,FDOM_sexpPEG,sexpPEG_applied,
886     \\ impl_tac >- simp[stoppers_def] \\ rw[]
889     rw[print_nt_def,pnt_def,peg_eval_NT_SOME,FDOM_sexpPEG,sexpPEG_applied,
892     \\ rw[listTheory.NULL_EQ]
896     \\ Cases_on`strl` \\ fs[] \\ rw[]
902     \\ rw[]
909     \\ rw[Abbr`a`]
915       \\ rw[numposrepTheory.l2n_def,listTheory.FOLDL_SNOC,listTheory.EVERY_SNOC,
926     rw[print_nt_def,pnt_def,peg_eval_NT_SOME,FDOM_sexpPEG,sexpPEG_applied,
933       rw[Once peg_eval_cases,FDOM_sexpPEG,sexpPEG_applied,peg_eval_seq_NONE,pnt_def]
934       \\ rw[Once peg_eval_cases,FDOM_sexpPEG,sexpPEG_applied,peg_eval_tok_NONE]
937     \\ rw[peg_eval_seq_NONE,peg_eval_tok_NONE,peg_eval_tok_SOME]
940     \\ first_x_assum(qspec_then`h::t`mp_tac) \\ rw[]
944     rw[print_nt_def,pnt_def,peg_eval_NT_SOME,FDOM_sexpPEG,sexpPEG_applied,
950     rw[print_nt_def]
952     \\ TRY pairarg_tac \\ fs[] \\ rw[]
955       \\ Cases_on`strl` \\ fs[] \\ rw[]
956       \\ rw[peg_eval_NT_SOME,FDOM_sexpPEG,sexpPEG_applied,peg_eval_choicel_CONS,
961         rw[Once peg_eval_cases,FDOM_sexpPEG,sexpPEG_applied]
962         \\ rw[peg_eval_NT_SOME,FDOM_sexpPEG,sexpPEG_applied,peg_eval_choicel_CONS,
966         \\ rw[Once peg_eval_cases,FDOM_sexpPEG,sexpPEG_applied]
967         \\ rw[peg_eval_NT_SOME,FDOM_sexpPEG,sexpPEG_applied,peg_eval_choicel_CONS,
970       \\ rw[grabWS_def,ignoreR_def,ignoreL_def,peg_eval_seq_SOME,peg_eval_rpt]
972       \\ Cases_on`d` \\ fs[] \\ rw[] \\ rfs[]
974       \\ rw[Once peg_eval_list]
975       \\ rw[peg_eval_tok_NONE,peg_eval_tok_SOME]
979       \\ rw[])
980     \\ fs[option_sequence_SOME] \\ rw[]
981     \\ Cases_on`strl` \\ fs[] \\ rw[]
982     \\ rw[pnt_def,peg_eval_NT_SOME,FDOM_sexpPEG,sexpPEG_applied,peg_eval_choicel_CONS]
986       \\ Cases_on`n` \\ fs[] \\ rw[]
988       \\ rw[pegf_def,peg_eval_seq_SOME,tokeq_def,grabWS_def,ignoreL_def,peg_eval_tok_SOME,peg_eval_rpt,PULL_EXISTS]
994       rw[Once peg_eval_cases,FDOM_sexpPEG,sexpPEG_applied,peg_eval_seq_NONE,pnt_def]
995       \\ rw[Once peg_eval_cases,FDOM_sexpPEG,sexpPEG_applied,peg_eval_tok_NONE,stringTheory.isDigit_def] )
997     \\ rw[tokeq_def,ignoreL_def,peg_eval_seq_SOME,peg_eval_tok_SOME]
1005     \\ rw[pnt_def]
1007     \\ rw[stoppers_def] )
1009     rw[print_nt_def] \\ fs[]
1026   \\ conj_tac >- ( rw[print_nt_def,print_sexp_def] )
1029     rw[print_nt_def,print_sexp_def]
1031     >- rw[escape_string_def]
1035       rw[] \\ fs[]
1043   \\ rw[] \\ fs[]
1044   \\ rw[print_nt_def]
1070     \\ CASE_TAC \\ fs[] \\ rw[]
1072     \\ spose_not_then strip_assume_tac \\ rw[]
1075     \\ CASE_TAC \\ fs[] \\ rw[]
1084       rw[]
1087       \\ rw[print_nt_def] )
1090     \\ rw[]
1093     \\ rw[print_nt_def] )
1094   \\ fs[markerTheory.Abbrev_def] \\ rw[]
1107   \\ rw[]
1115   rw[]
1124   rw[parse_sexp_def,pairTheory.EXISTS_PROD]