ProgTutorial/Parsing.thy
changeset 392 47e5b71c7f6c
parent 391 ae2f0b40c840
child 394 0019ebf76e10
equal deleted inserted replaced
391:ae2f0b40c840 392:47e5b71c7f6c
   373 "((\"h\", \"e\"), (1, [\"l\", \"l\", \"o\"]))"}
   373 "((\"h\", \"e\"), (1, [\"l\", \"l\", \"o\"]))"}
   374 
   374 
   375   \footnote{\bf FIXME: In which situations is @{text "lift"} useful? Give examples.} 
   375   \footnote{\bf FIXME: In which situations is @{text "lift"} useful? Give examples.} 
   376 
   376 
   377   Be aware of recursive parsers. Suppose you want to read strings
   377   Be aware of recursive parsers. Suppose you want to read strings
   378   separated by commas and by parentheses into a tree. We assume 
   378   separated by commas and by parentheses into a tree datastructure. 
   379   the trees are represented by the datatype:
   379   We assume the trees are represented by the datatype:
   380 *}
   380 *}
   381 
   381 
   382 ML{*datatype tree = 
   382 ML{*datatype tree = 
   383     Lf of string 
   383     Lf of string 
   384   | Br of tree * tree*}
   384   | Br of tree * tree*}
   407   @{ML_response_fake_both [display, gray]
   407   @{ML_response_fake_both [display, gray]
   408   "parse_tree \"A\""
   408   "parse_tree \"A\""
   409   "*** Exception- TOPLEVEL_ERROR raised"}
   409   "*** Exception- TOPLEVEL_ERROR raised"}
   410 
   410 
   411   raises an exception indicating that the stack limit is reached. Such
   411   raises an exception indicating that the stack limit is reached. Such
   412   looping parser are not useful at all, because of ML's strict evaluation of
   412   looping parser are not useful, because of ML's strict evaluation of
   413   arguments. Therefore we need to delay the execution of the
   413   arguments. Therefore we need to delay the execution of the
   414   parser until an input is given. This can be done by adding the parsed
   414   parser until an input is given. This can be done by adding the parsed
   415   string as an explicit argument.
   415   string as an explicit argument.
   416 *}
   416 *}
   417 
   417