471 |
471 |
472 |
472 |
473 subsection {* The Pure grammar *} |
473 subsection {* The Pure grammar *} |
474 |
474 |
475 text {* |
475 text {* |
476 \begin{figure}[htb]\small |
476 The priority grammar of the @{text "Pure"} theory is defined as follows: |
|
477 |
477 \begin{center} |
478 \begin{center} |
478 \begin{tabular}{rclc} |
479 \begin{supertabular}{rclr} |
479 |
480 |
480 @{text any} & = & @{text "prop | logic"} \\\\ |
481 @{text any} & = & @{text "prop | logic"} \\\\ |
481 |
482 |
482 @{text prop} & = & @{verbatim "("} @{text prop} @{verbatim ")"} \\ |
483 @{text prop} & = & @{verbatim "("} @{text prop} @{verbatim ")"} \\ |
483 & @{text "|"} & @{text "prop\<^sup>(\<^sup>4\<^sup>)"} @{verbatim "::"} @{text type} & @{text "(3)"} \\ |
484 & @{text "|"} & @{text "prop\<^sup>(\<^sup>4\<^sup>)"} @{verbatim "::"} @{text type} & @{text "(3)"} \\ |
484 & @{text "|"} & @{verbatim PROP} @{text aprop} \\ |
485 & @{text "|"} & @{text "any\<^sup>(\<^sup>3\<^sup>)"} @{verbatim "=?="} @{text "any\<^sup>(\<^sup>2\<^sup>)"} & @{text "(2)"} \\ |
485 & @{text "|"} & @{text "any\<^sup>(\<^sup>3\<^sup>)"} @{verbatim "=="} @{text "any\<^sup>(\<^sup>2\<^sup>)"} & @{text "(2)"} \\ |
486 & @{text "|"} & @{text "any\<^sup>(\<^sup>3\<^sup>)"} @{verbatim "=="} @{text "any\<^sup>(\<^sup>2\<^sup>)"} & @{text "(2)"} \\ |
486 & @{text "|"} & @{text "any\<^sup>(\<^sup>3\<^sup>)"} @{verbatim "=?="} @{text "any\<^sup>(\<^sup>2\<^sup>)"} & @{text "(2)"} \\ |
487 & @{text "|"} & @{text "any\<^sup>(\<^sup>3\<^sup>)"} @{text "\<equiv>"} @{text "any\<^sup>(\<^sup>2\<^sup>)"} & @{text "(2)"} \\ |
487 & @{text "|"} & @{text "prop\<^sup>(\<^sup>2\<^sup>)"} @{verbatim "==>"} @{text "prop\<^sup>(\<^sup>1\<^sup>)"} & @{text "(1)"} \\ |
488 & @{text "|"} & @{text "prop\<^sup>(\<^sup>2\<^sup>)"} @{verbatim "==>"} @{text "prop\<^sup>(\<^sup>1\<^sup>)"} & @{text "(1)"} \\ |
|
489 & @{text "|"} & @{text "prop\<^sup>(\<^sup>2\<^sup>)"} @{text "\<Longrightarrow>"} @{text "prop\<^sup>(\<^sup>1\<^sup>)"} & @{text "(1)"} \\ |
488 & @{text "|"} & @{verbatim "[|"} @{text prop} @{verbatim ";"} @{text "\<dots>"} @{verbatim ";"} @{text prop} @{verbatim "|]"} @{verbatim "==>"} @{text "prop\<^sup>(\<^sup>1\<^sup>)"} & @{text "(1)"} \\ |
490 & @{text "|"} & @{verbatim "[|"} @{text prop} @{verbatim ";"} @{text "\<dots>"} @{verbatim ";"} @{text prop} @{verbatim "|]"} @{verbatim "==>"} @{text "prop\<^sup>(\<^sup>1\<^sup>)"} & @{text "(1)"} \\ |
|
491 & @{text "|"} & @{text "\<lbrakk>"} @{text prop} @{verbatim ";"} @{text "\<dots>"} @{verbatim ";"} @{text prop} @{text "\<rbrakk>"} @{text "\<Longrightarrow>"} @{text "prop\<^sup>(\<^sup>1\<^sup>)"} & @{text "(1)"} \\ |
489 & @{text "|"} & @{verbatim "!!"} @{text idts} @{verbatim "."} @{text prop} & @{text "(0)"} \\ |
492 & @{text "|"} & @{verbatim "!!"} @{text idts} @{verbatim "."} @{text prop} & @{text "(0)"} \\ |
490 & @{text "|"} & @{verbatim OFCLASS} @{verbatim "("} @{text type} @{verbatim ","} @{text logic} @{verbatim ")"} \\\\ |
493 & @{text "|"} & @{text "\<And>"} @{text idts} @{verbatim "."} @{text prop} & @{text "(0)"} \\ |
491 |
494 & @{text "|"} & @{verbatim OFCLASS} @{verbatim "("} @{text type} @{verbatim ","} @{text logic} @{verbatim ")"} \\ |
492 @{text aprop} & = & @{text "id | longid | var | logic\<^sup>(\<^sup>1\<^sup>0\<^sup>0\<^sup>0\<^sup>) "}@{verbatim "("} @{text any} @{verbatim ","} @{text "\<dots>"} @{verbatim ","} @{text any} @{verbatim ")"} \\\\ |
495 & @{text "|"} & @{verbatim SORT_CONSTRAINT} @{verbatim "("} @{text type} @{verbatim ")"} \\ |
|
496 & @{text "|"} & @{verbatim PROP} @{text aprop} \\\\ |
|
497 |
|
498 @{text aprop} & = & @{text "id | longid | var | "}@{verbatim "_"}@{text " | "}@{verbatim "..."} \\ |
|
499 & @{text "|"} & @{text "logic\<^sup>(\<^sup>1\<^sup>0\<^sup>0\<^sup>0\<^sup>) any\<^sup>(\<^sup>1\<^sup>0\<^sup>0\<^sup>0\<^sup>) \<dots> any\<^sup>(\<^sup>1\<^sup>0\<^sup>0\<^sup>0\<^sup>)"} & @{text "(999)"} \\\\ |
493 |
500 |
494 @{text logic} & = & @{verbatim "("} @{text logic} @{verbatim ")"} \\ |
501 @{text logic} & = & @{verbatim "("} @{text logic} @{verbatim ")"} \\ |
495 & @{text "|"} & @{text "logic\<^sup>(\<^sup>4\<^sup>)"} @{verbatim "::"} @{text type} & @{text "(3)"} \\ |
502 & @{text "|"} & @{text "logic\<^sup>(\<^sup>4\<^sup>)"} @{verbatim "::"} @{text type} & @{text "(3)"} \\ |
496 & @{text "|"} & @{text "id | longid | var | logic\<^sup>(\<^sup>1\<^sup>0\<^sup>0\<^sup>0\<^sup>)"} @{verbatim "("} @{text any} @{verbatim ","} @{text "\<dots>"} @{verbatim ","} @{text any} @{verbatim ")"} \\ |
503 & @{text "|"} & @{text "id | longid | var | "}@{verbatim "_"}@{text " | "}@{verbatim "..."} \\ |
|
504 & @{text "|"} & @{text "logic\<^sup>(\<^sup>1\<^sup>0\<^sup>0\<^sup>0\<^sup>) any\<^sup>(\<^sup>1\<^sup>0\<^sup>0\<^sup>0\<^sup>) \<dots> any\<^sup>(\<^sup>1\<^sup>0\<^sup>0\<^sup>0\<^sup>)"} & @{text "(999)"} \\ |
497 & @{text "|"} & @{verbatim "%"} @{text pttrns} @{verbatim "."} @{text "any\<^sup>(\<^sup>3\<^sup>)"} & @{text "(3)"} \\ |
505 & @{text "|"} & @{verbatim "%"} @{text pttrns} @{verbatim "."} @{text "any\<^sup>(\<^sup>3\<^sup>)"} & @{text "(3)"} \\ |
|
506 & @{text "|"} & @{text \<lambda>} @{text pttrns} @{verbatim "."} @{text "any\<^sup>(\<^sup>3\<^sup>)"} & @{text "(3)"} \\ |
|
507 & @{text "|"} & @{verbatim CONST} @{text "id | "}@{verbatim CONST} @{text "longid"} \\ |
498 & @{text "|"} & @{verbatim TYPE} @{verbatim "("} @{text type} @{verbatim ")"} \\\\ |
508 & @{text "|"} & @{verbatim TYPE} @{verbatim "("} @{text type} @{verbatim ")"} \\\\ |
499 |
509 |
500 @{text idts} & = & @{text "idt | idt\<^sup>(\<^sup>1\<^sup>) idts"} \\\\ |
510 @{text idts} & = & @{text "idt | idt\<^sup>(\<^sup>1\<^sup>) idts"} & @{text "(0)"} \\\\ |
501 |
511 |
502 @{text idt} & = & @{text "id | "}@{verbatim "("} @{text idt} @{verbatim ")"} \\ |
512 @{text idt} & = & @{verbatim "("} @{text idt} @{verbatim ")"}@{text " | id | "}@{verbatim "_"} \\ |
503 & @{text "|"} & @{text id} @{verbatim "::"} @{text type} & @{text "(0)"} \\\\ |
513 & @{text "|"} & @{text id} @{verbatim "::"} @{text type} & @{text "(0)"} \\ |
504 |
514 & @{text "|"} & @{verbatim "_"} @{verbatim "::"} @{text type} & @{text "(0)"} \\\\ |
505 @{text pttrns} & = & @{text "pttrn | pttrn\<^sup>(\<^sup>1\<^sup>) pttrns"} \\\\ |
515 |
|
516 @{text pttrns} & = & @{text "pttrn | pttrn\<^sup>(\<^sup>1\<^sup>) pttrns"} & @{text "(0)"} \\\\ |
506 |
517 |
507 @{text pttrn} & = & @{text idt} \\\\ |
518 @{text pttrn} & = & @{text idt} \\\\ |
508 |
519 |
509 @{text type} & = & @{verbatim "("} @{text type} @{verbatim ")"} \\ |
520 @{text type} & = & @{verbatim "("} @{text type} @{verbatim ")"} \\ |
510 & @{text "|"} & @{text "tid | tvar | tid"} @{verbatim "::"} @{text "sort | tvar "}@{verbatim "::"} @{text sort} \\ |
521 & @{text "|"} & @{text "tid | tvar | "}@{verbatim "_"} \\ |
|
522 & @{text "|"} & @{text "tid"} @{verbatim "::"} @{text "sort | tvar "}@{verbatim "::"} @{text "sort | "}@{verbatim "_"} @{verbatim "::"} @{text "sort"} \\ |
511 & @{text "|"} & @{text "id | type\<^sup>(\<^sup>1\<^sup>0\<^sup>0\<^sup>0\<^sup>) id | "}@{verbatim "("} @{text type} @{verbatim ","} @{text "\<dots>"} @{verbatim ","} @{text type} @{verbatim ")"} @{text id} \\ |
523 & @{text "|"} & @{text "id | type\<^sup>(\<^sup>1\<^sup>0\<^sup>0\<^sup>0\<^sup>) id | "}@{verbatim "("} @{text type} @{verbatim ","} @{text "\<dots>"} @{verbatim ","} @{text type} @{verbatim ")"} @{text id} \\ |
512 & @{text "|"} & @{text "longid | type\<^sup>(\<^sup>1\<^sup>0\<^sup>0\<^sup>0\<^sup>) longid | "}@{verbatim "("} @{text type} @{verbatim ","} @{text "\<dots>"} @{verbatim ","} @{text type} @{verbatim ")"} @{text longid} \\ |
524 & @{text "|"} & @{text "longid | type\<^sup>(\<^sup>1\<^sup>0\<^sup>0\<^sup>0\<^sup>) longid | "}@{verbatim "("} @{text type} @{verbatim ","} @{text "\<dots>"} @{verbatim ","} @{text type} @{verbatim ")"} @{text longid} \\ |
513 & @{text "|"} & @{text "type\<^sup>(\<^sup>1\<^sup>)"} @{verbatim "=>"} @{text type} & @{text "(0)"} \\ |
525 & @{text "|"} & @{text "type\<^sup>(\<^sup>1\<^sup>)"} @{verbatim "=>"} @{text type} & @{text "(0)"} \\ |
514 & @{text "|"} & @{verbatim "["} @{text type} @{verbatim ","} @{text "\<dots>"} @{verbatim ","} @{text type} @{verbatim "]"} @{verbatim "=>"} @{text type} & @{text "(0)"} \\\\ |
526 & @{text "|"} & @{text "type\<^sup>(\<^sup>1\<^sup>)"} @{text "\<Rightarrow>"} @{text type} & @{text "(0)"} \\ |
515 |
527 & @{text "|"} & @{verbatim "["} @{text type} @{verbatim ","} @{text "\<dots>"} @{verbatim ","} @{text type} @{verbatim "]"} @{verbatim "=>"} @{text type} & @{text "(0)"} \\ |
516 @{text sort} & = & @{text "id | longid | "}@{verbatim "{}"}@{text " | "}@{verbatim "{"} @{text "id | longid"}@{verbatim ","}@{text "\<dots>"}@{verbatim ","}@{text "id | longid"} @{verbatim "}"} \\ |
528 & @{text "|"} & @{verbatim "["} @{text type} @{verbatim ","} @{text "\<dots>"} @{verbatim ","} @{text type} @{verbatim "]"} @{text "\<Rightarrow>"} @{text type} & @{text "(0)"} \\\\ |
517 \end{tabular} |
529 |
|
530 @{text sort} & = & @{text "id | longid | "}@{verbatim "{}"}@{text " | "}@{verbatim "{"} @{text "id | longid"} @{verbatim ","} @{text "\<dots>"} @{verbatim ","} @{text "id | longid"} @{verbatim "}"} \\ |
|
531 \end{supertabular} |
518 \end{center} |
532 \end{center} |
519 \caption{The Pure grammar}\label{fig:pure-grammar} |
533 |
520 \end{figure} |
534 \medskip The following nonterminals are introduced here: |
521 |
|
522 The priority grammar of the @{text "Pure"} theory is defined in |
|
523 \figref{fig:pure-grammar}. The following nonterminals are |
|
524 introduced: |
|
525 |
535 |
526 \begin{description} |
536 \begin{description} |
527 |
537 |
528 \item @{text "any"} denotes any term. |
538 \item @{text "any"} denotes any term. |
529 |
539 |
569 |
579 |
570 \item @{text sort} denotes meta-level sorts. |
580 \item @{text sort} denotes meta-level sorts. |
571 |
581 |
572 \end{description} |
582 \end{description} |
573 |
583 |
574 \begin{warn} |
584 Some further explanations of certain syntax features are required. |
575 In @{text idts}, note that @{text "x :: nat y"} is parsed as @{text |
585 |
576 "x :: (nat y)"}, treating @{text y} like a type constructor applied |
586 \begin{itemize} |
577 to @{text nat}. To avoid this interpretation, write @{text "(x :: |
587 |
578 nat) y"} with explicit parentheses. |
588 \item In @{text idts}, note that @{text "x :: nat y"} is parsed as |
579 |
589 @{text "x :: (nat y)"}, treating @{text y} like a type constructor |
580 Similarly, @{text "x :: nat y :: nat"} is parsed as @{text "x :: |
590 applied to @{text nat}. To avoid this interpretation, write @{text |
|
591 "(x :: nat) y"} with explicit parentheses. |
|
592 |
|
593 \item Similarly, @{text "x :: nat y :: nat"} is parsed as @{text "x :: |
581 (nat y :: nat)"}. The correct form is @{text "(x :: nat) (y :: |
594 (nat y :: nat)"}. The correct form is @{text "(x :: nat) (y :: |
582 nat)"}, or @{text "(x :: nat) y :: nat"} if @{text y} is last in the |
595 nat)"}, or @{text "(x :: nat) y :: nat"} if @{text y} is last in the |
583 sequence of identifiers. |
596 sequence of identifiers. |
584 \end{warn} |
597 |
585 |
598 \item Type constraints for terms bind very weakly. For example, |
586 \begin{warn} |
599 @{text "x < y :: nat"} is normally parsed as @{text "(x < y) :: |
587 Type constraints for terms bind very weakly. For example, @{text "x |
600 nat"}, unless @{text "<"} has a very low priority, in which case the |
588 < y :: nat"} is normally parsed as @{text "(x < y) :: nat"}, unless |
601 input is likely to be ambiguous. The correct form is @{text "x < (y |
589 @{text "<"} has a very low priority, in which case the input is |
602 :: nat)"}. |
590 likely to be ambiguous. The correct form is @{text "x < (y :: nat)"}. |
603 |
591 \end{warn} |
604 \item Constraints may be either written with two literal colons |
|
605 ``@{verbatim "::"}'' or the double-colon symbol @{verbatim "\<Colon>"}, |
|
606 which actually look exactly the same in some {\LaTeX} styles. |
|
607 |
|
608 \item Placeholders @{verbatim "_"} may occur in different roles: |
|
609 |
|
610 \begin{description} |
|
611 |
|
612 \item A type @{text "_"} or @{text "_::sort"} acts like an anonymous |
|
613 type-inference parameter, which is filled-in according to the most |
|
614 general type produced by the type-checking phase. |
|
615 |
|
616 \item A bound @{text "_"} refers to a vacuous abstraction, where the |
|
617 body does not refer to the binding introduced here. As in @{term |
|
618 "\<lambda>x _. x"} (which is @{text "\<alpha>"}-equivalent to @{text "\<lambda>x y. x"}). |
|
619 |
|
620 \item A free @{text "_"} refers to an implicit outer binding. |
|
621 Higher definitional packages usually allow forms like @{text "f x _ |
|
622 = a"}. |
|
623 |
|
624 \item A free @{text "_"} within a term pattern |
|
625 (\secref{sec:term-decls}) refers to an anonymous schematic variable |
|
626 that is implicitly abstracted over its context of locally bound |
|
627 variables. This allows pattern matching of @{text "{x. x = a} |
|
628 (\<IS> {x. x = _})"}, for example. |
|
629 |
|
630 \item The three literal dots ``@{verbatim "..."}'' may be also |
|
631 written as ellipsis symbol @{verbatim "\<dots>"}. In both cases it refers |
|
632 to a special schematic variable, which is bound in the context. |
|
633 This special term abbreviation works nicely calculational resoning |
|
634 (\secref{sec:calculation}). |
|
635 |
|
636 \end{description} |
|
637 |
|
638 \end{itemize} |
592 *} |
639 *} |
593 |
640 |
594 |
641 |
595 section {* Syntax and translations \label{sec:syn-trans} *} |
642 section {* Syntax and translations \label{sec:syn-trans} *} |
596 |
643 |