equal
deleted
inserted
replaced
80 (scan_all input1, scan_all input2) |
80 (scan_all input1, scan_all input2) |
81 end" |
81 end" |
82 "(\"foo bar\", \"foo (**test**) bar (**test**)\")"} |
82 "(\"foo bar\", \"foo (**test**) bar (**test**)\")"} |
83 *} |
83 *} |
84 |
84 |
85 text {* \solution{ex:dyckhoff} *} |
85 text {* \solution{ex:contextfree} *} |
86 |
86 |
87 text {* |
87 ML{*datatype expr = |
|
88 Number of int |
|
89 | Mult of expr * expr |
|
90 | Add of expr * expr |
|
91 |
|
92 fun parse_basic xs = |
|
93 (OuterParse.nat >> Number |
|
94 || OuterParse.$$$ "(" |-- parse_expr --| OuterParse.$$$ ")") xs |
|
95 and parse_factor xs = |
|
96 (parse_basic --| OuterParse.$$$ "*" -- parse_factor >> Mult |
|
97 || parse_basic) xs |
|
98 and parse_expr xs = |
|
99 (parse_factor --| OuterParse.$$$ "+" -- parse_expr >> Add |
|
100 || parse_factor) xs*} |
|
101 |
|
102 |
|
103 text {* \solution{ex:dyckhoff} |
88 The axiom rule can be implemented with the function @{ML atac}. The other |
104 The axiom rule can be implemented with the function @{ML atac}. The other |
89 rules correspond to the theorems: |
105 rules correspond to the theorems: |
90 |
106 |
91 \begin{center} |
107 \begin{center} |
92 \begin{tabular}{cc} |
108 \begin{tabular}{cc} |