1 2 module Parse where 3 4 import Char(isDigit)--1.3 5 import Token 6 7 import Unparse 8 9 import Build_Tm 10 11 import Build_itrm 12 13 import Core_datatype 14 15 import Type_defs 16 17 import Attributes 18 19 import Kernel 20 21 import Sub_Core1 22 23 import Sub_Core2 24 25 import Sub_Core3 26 27 import Sub_Core4 28 29 import Vtslib 30 31 32 33 type Parse_State = ( [ Tag ] , Sgn ) 34 35 36 37 38 parse_trm sg tgL s 39 = case parse_itm ( tgL , sg ) s of 40 ( Opnd ( Itrm itm )) -> Ok itm 41 Prs_Err mesg -> Bad mesg 42 43 parse_Thm_M sg ps str 44 = if is_valid_Thm th 45 then Ok th 46 else Bad mesg 47 where 48 th = parse_Thm sg ps str 49 ( TH_Err mesg ) = th 50 51 parse_Thm sg ps = parse_deriv (ps, sg) . parse_itm (ps, sg) 52 53 parse_Trm sg ps = parse_tm ( ps , sg ) 54 55 trm_to_Trm = build_trm' 56 57 dec_to_Dec = build_dc 58 59 sgn_to_Sgn = build_sg 60 61 62 63 parse_tm (tgL , sg ) str 64 = build_trm sg flag_itm 65 where 66 ( flag_itm , _ ) = drive_parse ( tgL , sg ) str 67 68 parse_itm sg str 69 = itm 70 where 71 (itm , _ ) = drive_parse sg str 72 73 74 75 76 77 78 79 80 81 82 83 84 drive_parse :: Parse_State -> String -> ( Flagged_ITrm , [Token] ) 85 86 drive_parse sg str 87 = term sg [Rvd ""] ( tokenise str ) 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 term :: Parse_State -> [Token] -> [Token] -> (Flagged_ITrm , [Token]) 107 108 term sg tmnL tkL 109 = ( tm , tkL2 ) 110 where 111 tm = foldl1 app' ( prioritise tmL ) 112 ( tmL , tkL2 ) = term' sg tmnL tkL 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 term' :: Parse_State -> [Token] -> [Token] -> ([Flagged_ITrm] , [Token]) 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 term' sg tmnL ( Rvd "if" : tkL ) 175 = ( [ cond_tm ] , tkL4 ) 176 where 177 cond_tm = cond' dc t_tm f_tm 178 ( dc , _ : tkL2 ) = hyp sg [ Rvd "then" ] tkL 179 ( t_tm , _ : tkL3 ) = term sg2 [ Rvd "else" ] tkL2 180 ( f_tm , tkL4 ) = term sg2 tmnL tkL3 181 sg2 = pst_extend dc sg 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 term' sg tmnL ( Rvd "let" : tkL ) 203 = ( [ let' dc tm1 tm2 ] , tkL4 ) 204 where 205 ( dc , _ : tkL2 ) = abdec sg [ IfxOp "=" ] tkL 206 ( tm1 , _ : tkL3 ) = term sg [ Rvd "in" ] tkL2 207 ( tm2 , tkL4 ) = term sg2 tmnL tkL3 208 sg2 = pst_extend dc sg 209 210 211 212 213 214 215 216 217 218 219 220 221 222 223 224 225 term' sg tmnL ( Rvd "recurse" : tkL ) 226 = ( [ recurse' tmL srt ] , tkL3 ) 227 where 228 ( tmL , tkL2 ) = recurse_cls sg [] tkL 229 ( srt , tkL3 ) = term sg tmnL tkL2 230 231 232 233 234 235 {- 236 term' sg tmnl ( Rvd "fn" : tkl ) 237 = case tkl? of 238 Rvd "|" : tkl?' -> 239 -} 240 241 242 243 244 245 246 247 248 249 250 251 252 253 254 255 256 257 258 259 260 261 262 263 term' sg tmnL ( Rvd "\185" : tkL ) 264 = ( app_op : argtm : tmL , tkL3 ) 265 where 266 ( argtm , _ : tkL2 ) = term sg [ Rvd "\176" ] tkL 267 ( tmL , tkL3 ) = term' sg tmnL tkL2 268 app_op = Opr ( Spl "" ) BinR 100 269 270 271 272 273 274 275 276 277 278 279 280 281 282 283 284 term' sg tmnL ( Bdr nm : tkL ) 285 = ( [ bdr_tm ] , tkL3 ) 286 where 287 bdr_tm = binder' nm dc tm 288 ( dc , _ : tkL2 ) = bdec sg [ Rvd "." ] tkL 289 ( tm , tkL3 ) = term sg2 tmnL tkL2 290 sg2 = pst_extend dc sg 291 292 293 294 295 296 297 298 299 300 301 302 303 304 305 306 307 308 309 310 term' sg tmnL ( Rvd "," : tkL ) 311 = ( pair_op : argtmL , tkL2 ) 312 where 313 ( argtmL, tkL2 ) = term' sg ( Rvd "typed" : tmnL ) tkL 314 pair_op = Opr ( Spl "," ) BinR 20 315 316 317 318 319 320 321 322 323 324 term' sg tmnL ( Rvd "typed" : tkL ) 325 = ( [ tpe_op , tpe ] , tkL2 ) 326 where 327 ( tpe , tkL2 ) = term sg tmnL tkL 328 tpe_op = Opr ( Spl "typed" ) BinL 1 329 330 331 332 333 334 335 336 337 338 339 340 341 342 343 term' sg tmnL ( Rvd "\168": Clr no1 : Rvd ",": Clr no2 : Rvd "\169": tkL ) 344 = ( sym' no1 no2 : tmL , tkL2 ) 345 where 346 ( tmL , tkL2 ) = term' sg tmnL tkL 347 348 349 350 351 352 353 354 355 356 357 term' sg tmnL ( Rvd "\168" : Clr no1 : Rvd "," : Clr no2 : Rvd "," : 358 Clr no3 : Rvd "\169" : tkL ) 359 = ( const' no1 no2 no3 : tmL , tkL2 ) 360 where 361 ( tmL , tkL2 ) = term' sg tmnL tkL 362 363 364 365 366 367 368 369 370 371 372 373 374 term' sg tmnL ( Rvd "{" : tkL ) 375 = ( binder' Subtype dc tm : tmL , tkL4 ) 376 where 377 ( dc , _ : tkL2 ) = bdec sg [ Rvd "|" ] tkL 378 ( tm , _ : tkL3 ) = term sg2 [ Rvd "}" ] tkL2 379 ( tmL , tkL4 ) = term' sg tmnL tkL3 380 sg2 = pst_extend dc sg 381 382 383 384 385 386 387 388 389 390 391 392 393 394 395 396 397 term' sg tmnL ( Rvd "[" : tkL ) 398 = ( dc : tmL , tkL3 ) 399 where 400 ( dc , _ : tkL2 ) = bdec sg [ Rvd "]" ] tkL 401 ( tmL , tkL3 ) = term' sg2 tmnL tkL2 402 sg2 = pst_extend dc sg 403 404 405 406 407 408 409 410 411 412 413 414 415 416 417 418 419 420 term' sg tmnL ( IfxBdr bdr : tkL ) 421 = ( bdrop : tmL , tkL2 ) 422 where 423 bdrop = make_prebdr bdr 424 ( tmL , tkL2 ) = term' sg tmnL tkL 425 426 427 428 429 430 431 432 433 434 435 436 437 term' sg tmnL ( IfxOp op : tkL ) 438 = ( iop : tmL , tkL2 ) 439 where 440 iop = make_iop op 441 ( tmL , tkL2 ) = term' sg tmnL tkL 442 443 444 445 446 447 448 449 450 451 452 453 term' sg tmnL ( Rvd "\181" : tkL ) 454 = ( not_op : tmL , tkL2 ) 455 where 456 not_op = Opr ( Spl "Not" ) Pre 60 457 ( tmL , tkL2 ) = term' sg tmnL tkL 458 459 460 461 462 463 464 465 466 467 468 469 470 471 term' sg tmnL ( Rvd "(" : tkL ) 472 = ( tm : tmL , tkL3 ) 473 where 474 ( tm , _ : tkL2 ) = term sg [ Rvd ")" ] tkL 475 ( tmL , tkL3 ) = term' sg tmnL tkL2 476 477 478 479 480 481 term' sg tmnL ( Rvd "@" : tkL ) 482 = ( [ Prs_Err "@ not implemented " ] , dmy ) 483 484 485 486 487 488 489 490 491 492 493 494 495 496 term' sg tmnL ( Clr ( 'U' : arg@(_:_) ) : tkL ) | and ( map isDigit arg ) 497 = ( universe : tmL , tkL2 ) 498 where 499 universe = ( Opnd . Itrm ) ( Constant ( Univ i ) [] [] ) 500 i = read arg 501 ( tmL , tkL2 ) = term' sg tmnL tkL 502 503 504 505 506 507 508 509 510 511 512 term' sg tmnL ( Clr nm : tkL ) | nm == "true" || nm == "false" || nm == "bool" 513 = ( cst : tmL , tkL2 ) 514 where 515 cst = ( Opnd . Itrm ) ( Constant ( ctr nm ) [] [] ) 516 ctr "true" = T 517 ctr "false" = F 518 ctr "bool" = Bool' 519 ( tmL , tkL2 ) = term' sg tmnL tkL 520 521 522 523 524 525 term' pst@( tgL , sg ) tmnL ( Clr nm : tkL ) 526 = if in_tgL then ( tag' tg argL : tmL2 , tkL3 ) 527 else ( sym_id : tmL1 , tkL2' ) 528 where 529 sym_id = lookUp nm sg 530 ( tmL1 , tkL2' ) = term' pst tmnL tkL 531 ( tmL2 , tkL3 ) = term' pst tmnL tkL2 532 ( in_tgL , tg@( _ , arg_kndL , _ )) = fetch_tg nm tgL 533 ( argL , tkL2 ) = parse_tag_arg [] arg_kndL tkL 534 535 parse_tag_arg tg_resL ( knd : kndL ) lcl_tkL 536 = parse_tag_arg ( tg_res : tg_resL ) kndL lcl_tkL3 537 where 538 ( tg_res , lcl_tkL3 ) 539 = case knd of 540 Term_Arg -> ( Tg_Trm trm_res , lcl_tkL2 ) 541 Deriv_Arg -> ( Tg_Thm thm_res , lcl_tkL2 ) 542 Int_Arg -> parse_iL lcl_tkL 543 trm_res = build_trm sg res_tm 544 thm_res = parse_deriv pst res_tm 545 ( res_tm , lcl_tkL2 ) = aterm pst [] lcl_tkL 546 547 parse_tag_arg tg_resL [] lcl_tkL 548 = ( reverse tg_resL , lcl_tkL ) 549 550 551 552 553 554 555 556 557 558 559 560 {- 561 term' pst@( _ , sg) tmnL ( Clr nm : tkL ) 562 = ( sym_id : tmL , tkL2 ) -- also checks tag list 563 where 564 sym_id = lookup nm sg 565 ( tmL , tkL2 ) = term' pst tmnL tkL 566 -} 567 568 569 570 571 572 573 574 575 576 577 578 term' sg tmnL tkL@( tk : _ ) | tk `elem` tmnL 579 = ( [] , tkL ) 580 581 582 583 584 585 586 587 term' sg tmnl ( Rvd str : tkl ) 588 -- = ( [ Prs_Err (" unexpected '" ++ str ++ "' (term)") ], dmy ) 589 = ( [ Prs_Err (" unexpected '" ++ str ++ "'"++ " (term) tmnl: " ++ concat ( map disp_tk tmnl )++ "|") ], dmy ) 590 591 592 593 594 595 term' sg tmnl [] | Rvd "" `elem` tmnl 596 = ( [] , [] ) 597 598 term' sg tmnl [] 599 = ( [] , [] ) 600 {- end of file with tmnl not empty is not necessarily an error e.g. ';' in sig 601 = ( [ Prs_Err mesg ] , dmy ) 602 where 603 mesg = " expecting '" ++ concat ( map disp_tk tmnl ) ++ "'" 604 -} 605 606 607 608 609 610 611 612 term' sg _ ( Scan_Err mesg : _ ) 613 = ( [ Prs_Err mesg ] , dmy ) 614 615 616 617 618 619 620 621 622 623 624 625 626 627 628 629 aterm sg tmnl ( Rvd "\168": Clr no1 : Rvd ",": Clr no2 : Rvd "\169": tkl ) 630 = ( sym' no1 no2 , tkl ) 631 632 633 634 635 aterm sg tmnl ( Rvd "\168" : Clr no1 : Rvd "," : Clr no2 : Rvd "," : 636 Clr no3 : Rvd "\169" : tkl ) 637 = ( const' no1 no2 no3 , tkl ) 638 639 640 641 aterm sg tmnl ( Rvd "{" : tkl ) 642 = ( binder' Subtype dc tm , tkl3 ) 643 where 644 ( dc , _ : tkl2 ) = bdec sg [ Rvd "|" ] tkl 645 ( tm , tkl3 ) = term sg2 [ Rvd "}" ] tkl2 646 sg2 = pst_extend dc sg 647 648 649 650 651 aterm sg tmnl ( Clr ( 'U' : arg@(_:_) ) : tkl ) | and ( map isDigit arg ) 652 = ( universe , tkl ) 653 where 654 universe = ( Opnd . Itrm ) ( Constant ( Univ i ) [] [] ) 655 i = read arg 656 657 658 659 aterm sg tmnl ( Clr nm : tkl ) | nm == "true" || nm == "false" || nm == "bool" 660 = ( cst , tkl ) 661 where 662 cst = ( Opnd . Itrm ) ( Constant ( ctr nm ) [] [] ) 663 ctr "true" = T 664 ctr "false" = F 665 ctr "bool" = Bool' 666 667 668 669 aterm sg tmnl ( Rvd "(" : tkl ) 670 = ( tm , tkl2 ) 671 where 672 ( tm , _ : tkl2 ) = term sg [ Rvd ")" ] tkl 673 674 675 676 aterm ( _ , sg ) tmnl ( Clr nm : tkl ) 677 = ( sym_id , tkl ) -- also checks tag list 678 where 679 sym_id = lookUp nm sg 680 681 aterm sg tmnl ( tk : tkl ) 682 = ( Prs_Err (" unexpected '" ++ disp_tk tk ++ "' (aterm -- no tmnl check)" ) , dmy ) 683 684 685 686 687 688 689 690 691 692 693 694 695 696 697 698 699 700 701 702 703 704 705 706 707 708 709 hyp :: Parse_State -> [Token] -> [Token] -> ( Flagged_ITrm , [Token] ) 710 711 hyp sg tmnL ( Rvd "[" : tkL ) 712 = case tkL2 of 713 nxt : _ | nxt `elem` tmnL 714 -> ( btm , tkL2 ) 715 nxt : _ -> ( Prs_Err mesg1 , dmy ) 716 where 717 mesg1 = "Unexpected token '"++ disp_tk nxt ++"'" 718 _ -> ( Prs_Err mesg2 , dmy ) 719 where 720 ( btm , _ : tkL2 ) = bdec sg [ Rvd "]" ] tkL 721 mesg2 = "Unexpected end of file" 722 723 724 725 726 727 728 729 730 731 hyp sg tmnL tkL 732 = ( anon_dc , tkL2 ) 733 where 734 anon_dc = symbol_dec' tm ( Name "_" ) [ hyp_ndpnd ] 735 ( tm , tkL2 ) = term sg tmnL tkL 736 737 738 739 740 741 742 743 744 745 746 747 748 749 750 751 752 753 754 755 756 757 758 759 760 761 762 763 764 765 766 767 768 769 bdec :: Parse_State -> [Token] -> [Token] -> ( Flagged_ITrm , [Token] ) 770 771 bdec sg tmnL tkL 772 = case tkL2 of 773 Rvd ";" : tkL2' 774 -> ( decpair' [un_grp] nxt_dc rest , tkL3 ) 775 where 776 ( rest , tkL3 ) = bdec sg2 tmnL tkL2' 777 tk : _ | tk `elem` tmnL 778 -> ( nxt_dc , tkL2 ) 779 -- oth -> ( Prs_Err "Malformed declaration" , dmy ) 780 oth -> error ( "Bdec: " ++ concat ( map disp_tk oth ) ++ "\ntmnl: " ++ concat ( map disp_tk tmnL ) ++ "|" ) 781 where 782 ( nxt_dc , tkL2 ) = bdec' sg tmnL tkL 783 sg2 = pst_extend nxt_dc sg 784 785 786 787 788 789 790 791 792 793 794 795 796 797 798 bdec' :: Parse_State -> [Token] -> [Token] -> ( Flagged_ITrm , [Token] ) 799 800 bdec' sg tmnL ( Rvd "(" : tkL ) 801 = ( nxt_dc , tkL2 ) 802 where 803 ( nxt_dc , _ : tkL2 ) = bdec sg [ Rvd ")" ] tkL 804 805 bdec' sg tmnL tkL 806 = bdec_name sg ( Rvd ";" : tmnL ) [] tkL 807 808 809 810 811 812 813 814 815 816 817 818 819 820 821 822 823 824 825 826 827 828 829 830 831 832 833 834 835 bdec_name :: Parse_State -> [Token] -> [Name'] -> [Token] 836 -> (Flagged_ITrm , [Token]) 837 838 bdec_name sg tmnL nmL tkL 839 = case nm of 840 Ok inm -> switch inm tkL2 841 Bad mesg -> ( Prs_Err mesg , dmy ) 842 where 843 ( nm , tkL2 ) = name tkL 844 845 switch inm ( Rvd "," : tkL2' ) = bdec_name sg tmnL ( inm : nmL ) tkL2' 846 847 switch inm ( IfxOp ":" : tkL2' ) 848 = ( make_dc ( reverse ( inm : nmL )) srt dec_tpe , tkL3 ) 849 where 850 ( srt , tkL3 ) = term sg ( Rvd ";" : tmnL ) tkL2' 851 852 switch inm tkL 853 = ( make_dc ( reverse ( inm : nmL )) dft dec_untpe , tkL ) 854 855 dft = Opnd ( Itrm ( Constant ( Univ 0 ) [] [] )) --temporary default 856 857 858 859 860 861 862 863 864 865 866 867 868 869 870 871 872 873 874 875 876 877 878 make_dc :: [Name'] -> Flagged_ITrm -> Attribute -> Flagged_ITrm 879 880 make_dc nmL ( Opnd ( Itrm srt )) tped 881 = case dcL of 882 [] -> Prs_Err "empty declaration" 883 _ -> foldr1 ( decpair' [grp] ) dcL 884 where 885 dcL = make_dcL 0 nmL 886 make_dcL cnt ( nm : nmL ) 887 = dc : ( make_dcL ( cnt + 1 ) nmL ) 888 where 889 dc = Opnd ( Idec ( Symbol_dec shft_srt [ sym_nm nm , tped ])) 890 shft_srt = shift_trm [] cnt srt 891 make_dcL _ [] = [] 892 893 make_dc nmL ( Prs_Err mesg ) _ 894 = Prs_Err mesg 895 896 make_dc nmL _ _ = error "unexpected term in make_dc" 897 898 899 900 901 902 903 904 905 906 907 908 909 910 911 912 913 914 915 916 abdec :: Parse_State -> [Token] -> [Token] -> ( Flagged_ITrm , [Token] ) 917 918 abdec sg tmnL ( Rvd "(" : tkL ) 919 = ( nxt_dc , tkL2 ) 920 where 921 ( nxt_dc , _ : tkL2 ) = bdec sg [ Rvd ")" ] tkL 922 923 abdec sg tmnL tkL 924 = case nm of 925 Ok inm -> ( symbol_dec' dft inm [] , tkL2 ) 926 Bad mesg -> ( Prs_Err mesg , dmy ) 927 where 928 ( nm , tkL2 ) = name tkL 929 dft = Opnd ( Itrm ( Constant ( Univ 0 ) [] [] )) --temporary default 930 931 932 933 934 935 936 937 938 939 940 941 -- name :: [Token] -> ( MayBe Name' , [Token] ) 942 943 944 945 946 947 948 949 950 951 name ( Rvd "{" : Clr id : tkL ) 952 = case tkL3 of 953 Rvd "}" : tkL3' -> ( Ok ( Operator' id prc optype ) , tkL3' ) 954 _ -> ( Bad "missing '}'" , dmy ) 955 where 956 ( optype , tkL2 ) = optyp tkL 957 ( prc , tkL3 ) = opprc tkL2 958 959 960 961 962 963 964 965 name ( Clr id : tkL ) 966 = ( Ok ( Name id ) , tkL ) 967 968 name ( oth : tkL ) 969 = ( Bad ( " unexpected '" ++ disp_tk oth ++ "' (name)" ) , dmy ) 970 971 name [] = ( Bad "empty identifier" , dmy ) 972 973 974 975 976 977 978 979 980 981 982 983 984 985 986 987 988 989 990 optyp :: [Token] -> ( Oprtype , [Token] ) 991 992 optyp ( Rvd "Pre" : tkL ) 993 = ( Pre , tkL ) 994 995 optyp ( Rvd "BinL" : tkL ) 996 = ( BinL , tkL ) 997 998 optyp ( Rvd "BinR" : tkL ) 999 = ( BinR , tkL ) 1000 1001 optyp ( Rvd "Post" : tkL ) 1002 = ( Post , tkL ) 1003 1004 1005 1006 optyp tkL 1007 = ( BinL , tkL ) 1008 1009 1010 1011 1012 1013 1014 1015 1016 1017 1018 1019 1020 1021 1022 1023 opprc :: [Token] -> ( Int , [Token] ) 1024 1025 opprc ( Clr prcid : tkL ) | and ( map isDigit prcid ) 1026 = ( read prcid , tkL ) 1027 1028 opprc tkL 1029 = ( 1 , tkL ) 1030 1031 1032 1033 1034 1035 1036 1037 1038 1039 1040 1041 1042 1043 1044 1045 1046 1047 1048 1049 recurse_cls :: Parse_State -> [Flagged_ITrm] -> [Token] -> ( [Flagged_ITrm] , [Token]) 1050 1051 recurse_cls sg fnL tkL 1052 = case tkL2 of 1053 Rvd "end" : Rvd "typed" : tkL2' 1054 -> ( fn : fnL , tkL2' ) 1055 Rvd "end" : _ 1056 -> ( [ Prs_Err " recurse must be typed " ] , dmy ) 1057 _ -> recurse_cls sg ( fn : fnL ) tkL2 1058 where 1059 ( fn , tkL2 ) = aterm sg [ Rvd "end" ] tkL 1060 1061 1062 1063 1064 1065 1066 1067 1068 1069 1070 {- 1071 fn_clauses 1072 = case ident_type tkL of 1073 Ok ( i , j , k ) 1074 -> match ctrL nmL ( i , j ) tkL 1075 where 1076 ( Data _ ctrL [ dat_nm nmL ] ) 1077 = fetch_type sg i j 1078 Bad mesg -> ( Prs_Err mesg , dmy ) 1079 1080 1081 match sg ctrL ( tpe_nm : nmL ) tp_id tkl 1082 = ( recurse' fnL srt , tkl2 ) 1083 where 1084 ( fnL , tkl2 ) = match_cls 1085 1086 match_cls ctr_argL nm 1087 = case tkl2 of 1088 Rvd "\167" : tkl2' -> make_rhs 1089 otherwise -> error "" 1090 where 1091 ( ( nm , fmls ) , tkl2 ) = parg sg nm tmnl abdec True tkl 1092 sg2 = extend' sg ( fmls ++ rcL ) 1093 rcL = find_recursive ctr_argL tp_id fmls 1094 1095 make_rhs 1096 = case tkl2 of 1097 Rvd "|" : tkl2' -> match_cls 1098 tk : _ | tk `elem` tmnl -> ( clsL , tkl2 ) 1099 where 1100 tm = add_lambda 1101 ( rhs , tkl2 ) = term sg2 tmnl tkl2' 1102 1103 1104 1105 1106 find_recursive ( arg : argL ) tp_id 1107 1108 1109 ident_type sg ( Clr nm : tkl ) 1110 = case lookUp nm sg of 1111 ( True , Const i j k _ _ ) -> Ok ( i , j , k ) 1112 otherwise -> ident_type sg tkl 1113 1114 ident_type sg ( Rvd "\167" : _ ) 1115 = Bad "No constructor before '\167'" 1116 1117 ident_type sg ( Rvd tk : _ ) 1118 = Bad " Unexpected '" ++ disp_tk tk ++ "'" 1119 1120 -} 1121 1122 1123 1124 1125 1126 1127 1128 1129 1130 1131 1132 1133 1134 1135 1136 1137 1138 1139 1140 1141 prioritise :: [Flagged_ITrm] -> [Flagged_ITrm] 1142 1143 prioritise tmL = case ptse [] [] False tmL of 1144 [] -> [ Prs_Err "Empty term" ] 1145 oth -> oth 1146 1147 1148 1149 1150 1151 1152 1153 1154 1155 1156 1157 1158 1159 1160 1161 1162 1163 type Flag_I = Flagged_ITrm -- shorthand 1164 1165 ptse :: [Flag_I] -> [Flag_I] -> Bool -> [Flag_I] -> [Flag_I] 1166 1167 1168 1169 1170 1171 ptse opnds oprs _ ( Prs_Err tm : opL ) 1172 = [ Prs_Err tm ] 1173 1174 1175 1176 1177 1178 1179 1180 1181 1182 1183 1184 1185 ptse opnds oprs False ( Opnd tm : opL ) 1186 = ptse ( Opnd tm : opnds ) oprs True opL 1187 1188 1189 1190 1191 1192 1193 1194 1195 1196 1197 1198 ptse opnds oprs True opL@( Opnd _ : _ ) 1199 = ptse opnds oprs True ( app_op : opL ) 1200 where 1201 app_op = Opr ( Spl "" ) BinL 100 1202 1203 1204 1205 1206 1207 1208 1209 1210 1211 1212 1213 1214 1215 1216 1217 1218 ptse opnds oprs _ ( op@( Opr _ Pre prc ) : opL ) 1219 = ptse ( op : opnds ) ( op : oprs ) False opL 1220 1221 1222 1223 1224 1225 1226 1227 1228 1229 1230 1231 1232 1233 1234 ptse opnds oprs _ ( op@( Opr _ BinL prc ) : opL ) 1235 = ptse ( swap_op op opnds' ) ( op : oprs' ) False opL 1236 where 1237 ( opnds' , oprs' ) = flush opnds oprs prc null_op 1238 1239 1240 1241 1242 1243 1244 1245 1246 1247 1248 1249 ptse opnds oprs _ ( op@( Opr op_nm BinR prc ) : opL ) 1250 = ptse ( swap_op op opnds' ) ( op : oprs' ) False opL 1251 where 1252 ( opnds' , oprs' ) = flush opnds oprs prc cmp_op 1253 cmp_op ( Opr _ BinR prc' ) = prc' <= prc 1254 cmp_op _ = False 1255 1256 1257 1258 1259 1260 1261 1262 1263 1264 1265 1266 1267 1268 1269 1270 ptse opnds oprs fl ( op@( Opr _ Post prc ) : opL ) 1271 -- = ptse ( swap_op op opnds' ) ( op : oprs' ) False opL 1272 = ptse ( swap_op op opnds' ) oprs' fl opL 1273 where 1274 ( opnds' , oprs' ) = flush opnds oprs prc null_op 1275 1276 1277 1278 1279 1280 ptse opnds oprs _ [] 1281 = opnds' 1282 where 1283 ( opnds' , _ ) = flush opnds oprs (-1) null_op 1284 1285 1286 1287 1288 1289 1290 1291 1292 1293 1294 1295 null_op :: a -> Bool 1296 1297 null_op _ = False 1298 1299 1300 1301 1302 1303 1304 1305 1306 1307 1308 1309 1310 1311 1312 1313 1314 1315 swap_op :: Flagged_ITrm -> [Flagged_ITrm] -> [Flagged_ITrm] 1316 1317 swap_op op ( top_op : opnds ) 1318 = app' op top_op : opnds 1319 1320 swap_op op [] = [ op ] 1321 1322 1323 1324 1325 1326 1327 1328 1329 1330 1331 1332 1333 1334 1335 1336 1337 1338 1339 1340 1341 1342 1343 flush :: [Flagged_ITrm] -> [Flagged_ITrm] -> Int 1344 -> ( Flagged_ITrm -> Bool ) -> ( [Flagged_ITrm] , [Flagged_ITrm] ) 1345 1346 flush opnds oprs@( op@(Opr op_nm op_tpe prc) : opL ) pprc cmp 1347 = if pprc > prc || cmp op 1348 then ( opnds , oprs ) 1349 else flush opnds' opL pprc cmp 1350 where 1351 opnds' = add_op op_nm op_tpe opnds 1352 1353 flush opnds [] _ _ = ( opnds , [] ) 1354 1355 1356 1357 1358 1359 1360 1361 1362 1363 1364 1365 1366 1367 1368 1369 1370 1371 1372 1373 1374 1375 1376 1377 1378 1379 1380 1381 1382 1383 1384 1385 1386 1387 1388 1389 1390 1391 1392 1393 1394 1395 1396 1397 1398 1399 1400 1401 1402 add_op :: Operator -> Oprtype -> [Flagged_ITrm] -> [Flagged_ITrm] 1403 1404 add_op op Pre ( arg : fn : opnds ) 1405 = app' fn arg : opnds 1406 1407 add_op op BinL ( arg : fn : opnds ) 1408 = app' fn arg : opnds 1409 1410 add_op op BinR ( arg : fn : opnds ) 1411 = app' fn arg : opnds 1412 1413 1414 1415 1416 add_op op Post opnds 1417 = opnds 1418 1419 add_op op _ _ 1420 = [ Prs_Err ( " Insufficient arguments for operator" ) ] -- ++ op ) ] 1421 1422 1423 1424 1425 1426 1427 1428 1429 1430 1431 1432 1433 1434 1435 1436 1437 1438 1439 1440 1441 1442 make_prebdr :: String -> Flagged_ITrm 1443 1444 make_prebdr bdr 1445 = Opr ( OpBdr prefix_form ) BinR prc 1446 where 1447 ( prefix_form , prc ) = map_bdr bdr 1448 map_bdr "\167" = ( Lambda , 5 ) 1449 map_bdr "\183" = ( Pi , 80 ) 1450 map_bdr "\184" = ( Sigma , 90 ) 1451 map_bdr "\182" = ( Imp , 20 ) 1452 map_bdr "\187" = ( Delta , 10 ) 1453 1454 1455 1456 1457 1458 1459 1460 1461 1462 1463 1464 1465 1466 1467 1468 1469 1470 1471 1472 make_iop :: String -> Flagged_ITrm 1473 1474 make_iop ":" 1475 = Opr ( Spl ":" ) BinL 15 1476 1477 make_iop op 1478 = Opr ( OpIfx oprep ) BinR prc 1479 where 1480 ( oprep , prc ) = map_op op 1481 map_op "\179" = ( And , 40 ) 1482 map_op "\180" = ( Or , 30 ) 1483 map_op "=" = ( Eq' , 15 ) 1484 map_op "\172" = ( Issubtype , 70 ) 1485 1486 1487 1488 1489 1490 1491 1492 1493 lookup_name sg nm 1494 = case lookUp nm sg of 1495 Opnd (Itrm tm ) -> SOME tm 1496 Prs_Err _ -> NONE 1497 _ -> error "could be ok, check 'lookup_name' in parse.lhs" 1498 1499 1500 1501 1502 1503 1504 1505 1506 1507 1508 1509 1510 1511 1512 1513 1514 lookUp :: String -> Sgn -> Flagged_ITrm 1515 1516 lookUp nm sg 1517 = lookup' isg nm 0 1518 where 1519 isg = internal_Sgn sg 1520 1521 1522 1523 1524 1525 1526 1527 1528 1529 1530 1531 1532 1533 1534 1535 1536 1537 1538 1539 1540 1541 lookup' :: ISgn -> String -> Int -> Flagged_ITrm 1542 1543 lookup' ( Extend dc sg _ ) nm i 1544 = if in_dc then tm 1545 else lookup' sg nm ( i + 1 ) 1546 where 1547 ( in_dc , tm ) = lookup_dc dc [] nm i 0 1548 1549 lookup' ( Empty _ ) nm i 1550 = Prs_Err ( " Undefined symbol: " ++ nm ) 1551 1552 1553 1554 1555 1556 1557 1558 1559 1560 1561 1562 1563 1564 1565 1566 1567 1568 lookup_dc :: IDec -> [IDec] -> String -> Int -> Int -> ( Bool , Flagged_ITrm ) 1569 1570 lookup_dc dc dcL nm i j 1571 = if found then ( found , tm ) 1572 else case dcL of 1573 dc : dcL' -> lookup_dc dc dcL' nm i ( j + 1 ) 1574 [] -> ( False , error "" ) 1575 where 1576 ( found , tm ) = lookup_dc' dc dcL nm i j 1577 1578 1579 1580 1581 1582 1583 1584 1585 1586 1587 1588 lookup_dc' :: IDec -> [IDec] -> String -> Int -> Int -> (Bool , Flagged_ITrm) 1589 1590 1591 1592 1593 1594 1595 1596 1597 lookup_dc' ( Decpair dc1 dc2 _ ) dcL nm i j 1598 = lookup_dc dc1 ( dc2 : dcL ) nm i ( j + 1 ) 1599 1600 1601 1602 1603 lookup_dc' ( Symbol_dec _ ( ( _ , Symbol_Name nm' ) : _ ) ) _ nm i j 1604 = lookup_nm nm' nm i j 1605 1606 lookup_dc' ( Axiom_dec _ ( ( _ , Symbol_Name nm' ) : _ ) ) _ nm i j 1607 = lookup_nm nm' nm i j 1608 1609 1610 1611 1612 lookup_dc' ( Data _ _ [ ( _ , Datatype_Name nmL ) ] ) _ nm i j 1613 = lookup_nml nmL nm i j 0 1614 1615 1616 1617 1618 1619 lookup_dc' ( Def _ _ [ ( _ , Symbol_Name nm' )] ) _ nm i j 1620 = lookup_nm nm' nm i j 1621 1622 1623 1624 1625 1626 1627 1628 1629 1630 1631 lookup_nm :: Name' -> String -> Int -> Int -> ( Bool , Flagged_ITrm ) 1632 1633 1634 1635 1636 1637 1638 1639 1640 lookup_nm ( Name nm' ) nm i j 1641 | nm == nm' = ( True , ( Opnd . Itrm ) ( Sym i j [] [sym_nmd] ) ) 1642 | otherwise = ( False , error "" ) 1643 1644 1645 1646 1647 1648 1649 1650 lookup_nm ( Operator' nm' prc opt ) nm i j 1651 | nm == nm' = ( True , Opr ( OpItrm ( Sym i j [] [sym_nmd] )) opt prc ) 1652 | otherwise = ( False , error "" ) 1653 1654 1655 1656 1657 1658 1659 1660 1661 1662 1663 1664 1665 1666 1667 1668 1669 1670 1671 1672 lookup_nml :: [Name'] -> String -> Int -> Int -> Int -> (Bool , Flagged_ITrm) 1673 1674 lookup_nml ( Name nm' : nml ) nm i j k 1675 | nm == nm' = ( True , ( Opnd . Itrm ) ( Const i j k [] [sym_nmd] ) ) 1676 | otherwise = lookup_nml nml nm i j ( k + 1 ) 1677 1678 lookup_nml ( Operator' nm' prc opt : nml ) nm i j k 1679 | nm == nm' = ( True , Opr 1680 ( OpItrm ( Const i j k [] [sym_nmd] )) opt prc ) 1681 | otherwise = lookup_nml nml nm i j ( k + 1 ) 1682 1683 lookup_nml [] _ _ _ _ 1684 = ( False , error "" ) 1685 1686 1687 1688 1689 1690 1691 1692 1693 1694 1695 1696 1697 1698 dmy :: [Token] 1699 1700 dmy = [ Rvd "" ] 1701 1702 1703 1704 1705 1706 1707 1708 pst_extend :: Flagged_ITrm -> Parse_State -> Parse_State 1709 1710 pst_extend ( Opnd ( Idec idc )) ( tgL , sg ) 1711 = ( tgL , extend dc sg ) 1712 where 1713 dc = build_dc sg idc 1714 1715 1716 1717 1718 1719 1720 1721 fetch_tg tg_nm1 ( tg@( tg_nm2 , _ , _ ) : tgL ) 1722 | tg_nm1 == tg_nm2 = ( True , tg ) 1723 | otherwise = fetch_tg tg_nm1 tgL 1724 1725 fetch_tg _ [] = ( False , ( "" , [] , [] ) ) 1726 1727 1728 1729 1730 1731 1732 1733 1734 1735 parse_deriv :: Parse_State -> Flagged_ITrm -> Thm 1736 1737 parse_deriv pst ( Opnd ( Itrm itm )) 1738 = deriv pst itm 1739 1740 parse_deriv _ _ 1741 = TH_Err "unimplemented feature" 1742 1743 1744 1745 1746 deriv :: Parse_State -> ITrm -> Thm 1747 1748 1749 deriv pst@( tgL , sg ) ( Tagid ( str , _ , cnv_fnL ) argL ) 1750 = case fetch_fn cnv_fnL of 1751 Ok cnv_fn -> cnv_fn argL 1752 Bad mesg -> TH_Err mesg 1753 where 1754 fetch_fn ( Thm_Fn fn : _ ) = Ok fn 1755 fetch_fn ( _ : oth ) = fetch_fn oth 1756 fetch_fn [] = Bad ( "cannot convert tag " ++ str ++ " to theorem" ) 1757 1758 deriv pst@( tgL , sg ) ( Binder Delta idc itm _ _ ) 1759 = case typ_of_trm sg2 dc_typ of 1760 Constant Bool' _ _ -> discharge th 1761 Constant ( Univ _ ) _ _ -> generalise th 1762 otherwise -> TH_Err "dc type not bool or univ" 1763 where 1764 th = deriv ( tgL , extend dc sg ) itm 1765 ( dc_typ , _ , sg2 ) = internal_Trm ( typ_of_Dec dc ) 1766 dc = build_dc sg idc 1767 1768 1769 deriv pst@( _ , sg ) ( App itm1 itm2 _ _ ) 1770 = case th_tm of 1771 Binder Forall _ _ _ _ -> specialise th1 tm 1772 Binder Imp _ _ _ _ -> modus_ponens th1 th2 1773 otherwise -> TH_Err "not \177 or \182" 1774 where 1775 th1 = deriv pst itm1 1776 th2 = deriv pst itm2 1777 tm = build_trm' sg itm2 1778 ( th_tm , _ ) = internal_Thm th1 1779 1780 deriv pst@( _ , sg ) ( Pair itm1 itm2 _ _ _ ) 1781 = modus_ponens ( modus_ponens spec_th th1 ) th2 1782 where 1783 spec_th = specialise ( specialise th tm1 ) tm2 1784 tm1 = typ_of_Thm th1 1785 tm2 = typ_of_Thm th2 1786 th1 = deriv pst itm1 1787 th2 = deriv pst itm2 1788 th = taut ( parse_tm pst str ) 1789 str = "\177 a:bool. \177 b:bool.a \182 b \182 a \179 b" 1790 1791 deriv ( _ , sg ) ( Sym i j _ _ ) 1792 = axiom sg i j 1793 1794 deriv pst@( _ , SG isg ) itm 1795 = TH_Err (" Invalid construction: " ++ unparse' isg itm ) 1796 1797 deriv _ _ = error "deriv error" 1798 1799 1800 1801 1802 1803 1804 1805 1806 1807 1808 1809 1810 1811 1812 1813 1814 1815 parse_iL :: [Token] -> ( Tag_Arg , [Token] ) 1816 1817 parse_iL ( Rvd "\168" : tkL ) 1818 = parse_iL' [] tkL 1819 1820 parse_iL _ = ( Tg_Trm ( TM_Err "Malformed integer list" ) , dmy ) 1821 1822 1823 1824 1825 1826 1827 parse_iL' iL ( Clr str : tkL ) | and ( map isDigit str ) 1828 = parse_iL'' ( read str : iL ) tkL 1829 1830 parse_iL' iL ( Rvd "\169" : tkL ) 1831 = ( Tg_Int iL , tkL ) 1832 1833 parse_iL' iL ( tk : _ ) 1834 = ( Tg_Trm ( TM_Err ( "Malformed item in integer list: " ++ disp_tk tk )) , dmy ) 1835 1836 parse_iL' iL [] 1837 = ( Tg_Trm ( TM_Err "Unexpected end of input" ) , dmy ) 1838 1839 1840 1841 1842 parse_iL'' iL ( Rvd "\169" : tkL ) 1843 = ( Tg_Int iL , tkL ) 1844 1845 parse_iL'' iL ( Rvd "," : tkL ) 1846 = parse_iL' iL tkL 1847 1848 parse_iL'' iL _ 1849 = ( Tg_Trm ( TM_Err " ',' or '\169' expected " ) , dmy )