doc-src/IsarImplementation/Thy/Syntax.thy
author wenzelm
Fri Aug 12 22:10:49 2011 +0200 (2011-08-12)
changeset 44163 32e0c150c010
parent 42510 b9c106763325
child 45258 97f8806c3ed6
permissions -rw-r--r--
normalized theory dependencies wrt. file_store;
     1 theory Syntax
     2 imports Base
     3 begin
     4 
     5 chapter {* Concrete syntax and type-checking *}
     6 
     7 text FIXME
     8 
     9 section {* Reading and pretty printing \label{sec:read-print} *}
    10 
    11 text FIXME
    12 
    13 text %mlref {*
    14   \begin{mldecls}
    15   @{index_ML Syntax.read_typ: "Proof.context -> string -> typ"} \\
    16   @{index_ML Syntax.read_term: "Proof.context -> string -> term"} \\
    17   @{index_ML Syntax.read_prop: "Proof.context -> string -> term"} \\
    18   @{index_ML Syntax.pretty_typ: "Proof.context -> typ -> Pretty.T"} \\
    19   @{index_ML Syntax.pretty_term: "Proof.context -> term -> Pretty.T"} \\
    20   \end{mldecls}
    21 
    22   \begin{description}
    23 
    24   \item FIXME
    25 
    26   \end{description}
    27 *}
    28 
    29 
    30 section {* Parsing and unparsing \label{sec:parse-unparse} *}
    31 
    32 text FIXME
    33 
    34 text %mlref {*
    35   \begin{mldecls}
    36   @{index_ML Syntax.parse_typ: "Proof.context -> string -> typ"} \\
    37   @{index_ML Syntax.parse_term: "Proof.context -> string -> term"} \\
    38   @{index_ML Syntax.parse_prop: "Proof.context -> string -> term"} \\
    39   @{index_ML Syntax.unparse_typ: "Proof.context -> typ -> Pretty.T"} \\
    40   @{index_ML Syntax.unparse_term: "Proof.context -> term -> Pretty.T"} \\
    41   \end{mldecls}
    42 
    43   \begin{description}
    44 
    45   \item FIXME
    46 
    47   \end{description}
    48 *}
    49 
    50 
    51 section {* Checking and unchecking \label{sec:term-check} *}
    52 
    53 text FIXME
    54 
    55 text %mlref {*
    56   \begin{mldecls}
    57   @{index_ML Syntax.check_typs: "Proof.context -> typ list -> typ list"} \\
    58   @{index_ML Syntax.check_terms: "Proof.context -> term list -> term list"} \\
    59   @{index_ML Syntax.check_props: "Proof.context -> term list -> term list"} \\
    60   @{index_ML Syntax.uncheck_typs: "Proof.context -> typ list -> typ list"} \\
    61   @{index_ML Syntax.uncheck_terms: "Proof.context -> term list -> term list"} \\
    62   \end{mldecls}
    63 
    64   \begin{description}
    65 
    66   \item FIXME
    67 
    68   \end{description}
    69 *}
    70 
    71 
    72 section {* Syntax translations *}
    73 
    74 text FIXME
    75 
    76 text %mlantiq {*
    77   \begin{matharray}{rcl}
    78   @{ML_antiquotation_def "class_syntax"} & : & @{text ML_antiquotation} \\
    79   @{ML_antiquotation_def "type_syntax"} & : & @{text ML_antiquotation} \\
    80   @{ML_antiquotation_def "const_syntax"} & : & @{text ML_antiquotation} \\
    81   @{ML_antiquotation_def "syntax_const"} & : & @{text ML_antiquotation} \\
    82   \end{matharray}
    83 
    84   @{rail "
    85   (@@{ML_antiquotation class_syntax} |
    86    @@{ML_antiquotation type_syntax} |
    87    @@{ML_antiquotation const_syntax} |
    88    @@{ML_antiquotation syntax_const}) name
    89   "}
    90 
    91   \begin{description}
    92 
    93   \item FIXME
    94 
    95   \end{description}
    96 *}
    97 
    98 end