# HG changeset patch # User Norbert Schirmer # Date 1557848713 -7200 # Node ID 6103b0eadbf2ab7c364ffe5a39e842f97a05c7f3 # Parent cecd7a9418850248abf88865e15327dc380c8c72 tuned parser for patterns in ML_response... antiquotations diff -r cecd7a941885 -r 6103b0eadbf2 ProgTutorial/Essential.thy --- a/ProgTutorial/Essential.thy Tue May 14 17:10:47 2019 +0200 +++ b/ProgTutorial/Essential.thy Tue May 14 17:45:13 2019 +0200 @@ -29,8 +29,8 @@ @{ML_response [display,gray] "@{term \"(a::nat) + b = c\"}" -"Const (\"HOL.eq\", \) $ - (Const (\"Groups.plus_class.plus\", \) $ \ $ \) $ \"} +"Const (\"HOL.eq\", _) $ + (Const (\"Groups.plus_class.plus\", _) $ _ $ _) $ _"} constructs the term @{term "(a::nat) + b = c"}. The resulting term is printed using the internal representation corresponding to the datatype @{ML_type_ind "term"}, @@ -187,14 +187,14 @@ Consider for example the pairs @{ML_response [display,gray] "(@{term \"P x\"}, @{prop \"P x\"})" -"(Free (\"P\", \) $ Free (\"x\", \), - Const (\"HOL.Trueprop\", \) $ (Free (\"P\", \) $ Free (\"x\", \)))"} +"(Free (\"P\", _) $ Free (\"x\", _), + Const (\"HOL.Trueprop\", _) $ (Free (\"P\", _) $ Free (\"x\", _)))"} where a coercion is inserted in the second component and @{ML_response [display,gray] "(@{term \"P x \ Q x\"}, @{prop \"P x \ Q x\"})" - "(Const (\"Pure.imp\", \) $ \ $ \, - Const (\"Pure.imp\", \) $ \ $ \)"} + "(Const (\"Pure.imp\", _) $ _ $ _, + Const (\"Pure.imp\", _) $ _ $ _)"} where it is not (since it is already constructed by a meta-implication). The purpose of the \Trueprop\-coercion is to embed formulae of @@ -202,7 +202,7 @@ is needed whenever a term is constructed that will be proved as a theorem. As already seen above, types can be constructed using the antiquotation - \@{typ \}\. For example: + \@{typ _}\. For example: @{ML_response_fake [display,gray] "@{typ \"bool \ nat\"}" "bool \ nat"} @@ -339,18 +339,18 @@ the given arguments @{ML_response [display,gray] "make_imp @{term S} @{term T}" -"Const \ $ +"Const _ $ Abs (\"x\", Type (\"Nat.nat\",[]), - Const \ $ (Free (\"S\",\) $ \) $ (Free (\"T\",\) $ \))"} + Const _ $ (Free (\"S\",_) $ _) $ (Free (\"T\",_) $ _))"} whereas with @{ML make_wrong_imp} you obtain a term involving the @{term "P"} and \Q\ from the antiquotation. @{ML_response [display,gray] "make_wrong_imp @{term S} @{term T}" -"Const \ $ - Abs (\"x\", \, - Const \ $ (Const \ $ (Free (\"P\",\) $ \)) $ - (Const \ $ (Free (\"Q\",\) $ \)))"} +"Const _ $ + Abs (\"x\", _, + Const _ $ (Const _ $ (Free (\"P\",_) $ _)) $ + (Const _ $ (Free (\"Q\",_) $ _)))"} There are a number of handy functions that are frequently used for constructing terms. One is the function @{ML_ind list_comb in Term}, which @@ -449,7 +449,7 @@ @{ML_response_fake [display, gray] "strip_alls @{term \"\x y. x = (y::bool)\"}" "([Free (\"x\", \"bool\"), Free (\"y\", \"bool\")], - Const (\"op =\", \) $ Bound 1 $ Bound 0)"} + Const (\"op =\", _) $ Bound 1 $ Bound 0)"} Note that we produced in the body two dangling de Bruijn indices. Later on we will also use the inverse function that @@ -605,7 +605,7 @@ because @{term "All"} is such a fundamental constant, which can be referenced by @{ML "Const (\"All\", some_type)" for some_type}. However, if you look at - @{ML_response [display,gray] "@{term \"Nil\"}" "Const (\"List.list.Nil\", \)"} + @{ML_response [display,gray] "@{term \"Nil\"}" "Const (\"List.list.Nil\", _)"} the name of the constant \Nil\ depends on the theory in which the term constructor is defined (\List\) and also in which datatype @@ -614,8 +614,8 @@ \mbox{@{term "times"}}: @{ML_response [display,gray] "(@{term \"0::nat\"}, @{term \"times\"})" - "(Const (\"Groups.zero_class.zero\", \), - Const (\"Groups.times_class.times\", \))"} + "(Const (\"Groups.zero_class.zero\", _), + Const (\"Groups.times_class.times\", _))"} While you could use the complete name, for example @{ML "Const (\"List.list.Nil\", some_type)" for some_type}, for referring to or diff -r cecd7a941885 -r 6103b0eadbf2 ProgTutorial/First_Steps.thy --- a/ProgTutorial/First_Steps.thy Tue May 14 17:10:47 2019 +0200 +++ b/ProgTutorial/First_Steps.thy Tue May 14 17:45:13 2019 +0200 @@ -5,7 +5,6 @@ chapter \First Steps\label{chp:firststeps}\ - text \ \begin{flushright} {\em ``The most effective debugging tool is still careful thought,\\ @@ -104,7 +103,7 @@ for converting values into strings, namely the antiquotation \@{make_string}\: - @{ML_response_fake [display,gray] "writeln (@{make_string} 1)" "\"1\""} + @{ML_response_fake [display,gray] \writeln (@{make_string} 1)\ \"1"\} However, \@{make_string}\ only works if the type of what is converted is monomorphic and not a function. diff -r cecd7a941885 -r 6103b0eadbf2 ProgTutorial/Package/Ind_Interface.thy --- a/ProgTutorial/Package/Ind_Interface.thy Tue May 14 17:10:47 2019 +0200 +++ b/ProgTutorial/Package/Ind_Interface.thy Tue May 14 17:45:13 2019 +0200 @@ -119,9 +119,9 @@ parse spec_parser input end" "(([(even, NONE, NoSyn), (odd, NONE, NoSyn)], - [((even0,\), \), - ((evenS,\), \), - ((oddS,\), \)]), [])"} + [((even0,_), _), + ((evenS,_), _), + ((oddS,_), _)]), [])"} then we get back the specifications of the predicates (with type and syntax annotations), and specifications of the introduction rules. This is all the information we diff -r cecd7a941885 -r 6103b0eadbf2 ProgTutorial/Parsing.thy --- a/ProgTutorial/Parsing.thy Tue May 14 17:10:47 2019 +0200 +++ b/ProgTutorial/Parsing.thy Tue May 14 17:45:13 2019 +0200 @@ -502,11 +502,11 @@ messages. The following code -@{ML_response_fake [display,gray] "Token.explode - (Thy_Header.get_keywords' @{context}) Position.none \"hello world\"" -"[Token (\,(Ident, \"hello\"),\), - Token (\,(Space, \" \"),\), - Token (\,(Ident, \"world\"),\)]"} +@{ML_response_fake [display,gray] \Token.explode + (Thy_Header.get_keywords' @{context}) Position.none "hello world"\ +\[Token (_,(Ident, "hello"),_), + Token (_,(Space, " "),_), + Token (_,(Ident, "world"),_)]\} produces three tokens where the first and the last are identifiers, since @{text [quotes] "hello"} and @{text [quotes] "world"} do not match any @@ -526,9 +526,9 @@ @{ML_response_fake [display,gray] "Token.explode (Thy_Header.get_keywords' @{context}) Position.none \"hello world\"" -"[Token (\,(Keyword, \"hello\"),\), - Token (\,(Space, \" \"),\), - Token (\,(Ident, \"world\"),\)]"} +"[Token (_,(Keyword, \"hello\"),_), + Token (_,(Space, \" \"),_), + Token (_,(Ident, \"world\"),_)]"} Many parsing functions later on will require white space, comments and the like to have already been filtered out. So from now on we are going to use the @@ -541,7 +541,7 @@ in filter Token.is_proper input end" -"[Token (\,(Ident, \"hello\"), \), Token (\,(Ident, \"world\"), \)]"} +"[Token (_,(Ident, \"hello\"), _), Token (_,(Ident, \"world\"), _)]"} For convenience we define the function: \ @@ -555,9 +555,9 @@ @{ML_response_fake [display,gray] "filtered_input \"inductive | for\"" -"[Token (\,(Command, \"inductive\"),\), - Token (\,(Keyword, \"|\"),\), - Token (\,(Keyword, \"for\"),\)]"} +"[Token (_,(Command, \"inductive\"),_), + Token (_,(Keyword, \"|\"),_), + Token (_,(Keyword, \"for\"),_)]"} you obtain a list consisting of only one command and two keyword tokens. If you want to see which keywords and commands are currently known to Isabelle, @@ -575,7 +575,7 @@ in (Parse.$$$ \"where\" input1, Parse.$$$ \"|\" input2) end" -"((\"where\",\), (\"|\",\))"} +"((\"where\",_), (\"|\",_))"} Any non-keyword string can be parsed with the function @{ML_ind reserved in Parse}. For example: @@ -609,7 +609,7 @@ in (Parse.enum \"|\" (Parse.$$$ \"in\")) input end" -"([\"in\", \"in\", \"in\"], [\])"} +"([\"in\", \"in\", \"in\"], [_])"} The function @{ML_ind enum1 in Parse} works similarly, except that the parsed list must be non-empty. Note that we had to add a string @{text @@ -673,8 +673,8 @@ @{ML_response_fake [display,gray] "filtered_input' \"foo \\n bar\"" -"[Token ((\"foo\", ({line=7, end_line=7}, {line=7})), (Ident, \"foo\"), \), - Token ((\"bar\", ({line=8, end_line=8}, {line=8})), (Ident, \"bar\"), \)]"} +"[Token ((\"foo\", ({line=7, end_line=7}, {line=7})), (Ident, \"foo\"), _), + Token ((\"bar\", ({line=8, end_line=8}, {line=8})), (Ident, \"bar\"), _)]"} in which the @{text [quotes] "\\n"} causes the second token to be in line 8. @@ -844,9 +844,9 @@ parse spec_parser input end" "(([(even, NONE, NoSyn), (odd, NONE, NoSyn)], - [((even0,\),\), - ((evenS,\),\), - ((oddS,\),\)]), [])"} + [((even0,_),_), + ((evenS,_),_), + ((oddS,_),_)]), [])"} \ ML \let @@ -875,8 +875,8 @@ in parse Parse.vars input end" -"([(foo, SOME \, NoSyn), - (bar, SOME \, Mixfix (Source {text=\"BAR\",...}, [], 100, \)), +"([(foo, SOME _, NoSyn), + (bar, SOME _, Mixfix (Source {text=\"BAR\",...}, [], 100, _)), (blonk, NONE, NoSyn)],[])"} \ @@ -904,7 +904,7 @@ val ((name, attrib), _) = parse (Parse_Spec.thm_name \":\") input in (name, map Token.name_of_src attrib) -end" "(foo_lemma, [(\"intro\", \), (\"dest\", \)])"} +end" "(foo_lemma, [(\"intro\", _), (\"dest\", _)])"} The function @{ML_ind opt_thm_name in Parse_Spec} is the ``optional'' variant of @{ML_ind thm_name in Parse_Spec}. Theorem names can contain attributes. The name diff -r cecd7a941885 -r 6103b0eadbf2 ProgTutorial/Tactical.thy --- a/ProgTutorial/Tactical.thy Tue May 14 17:10:47 2019 +0200 +++ b/ProgTutorial/Tactical.thy Tue May 14 17:45:13 2019 +0200 @@ -2105,9 +2105,9 @@ in Thm.prop_of (Thm.beta_conversion true ctrm) end" -"Const (\"Pure.eq\",\) $ - (Abs (\"x\",\,Abs (\"y\",\,\)) $\$\) $ - (Const (\"Groups.plus_class.plus\",\) $ \ $ \)"} +"Const (\"Pure.eq\",_) $ + (Abs (\"x\",_,Abs (\"y\",_,_)) $_$_) $ + (Const (\"Groups.plus_class.plus\",_) $ _ $ _)"} or in the pretty-printed form diff -r cecd7a941885 -r 6103b0eadbf2 ProgTutorial/antiquote_setup.ML --- a/ProgTutorial/antiquote_setup.ML Tue May 14 17:10:47 2019 +0200 +++ b/ProgTutorial/antiquote_setup.ML Tue May 14 17:45:13 2019 +0200 @@ -28,10 +28,11 @@ |> ml_with_vars vs fun ml_pat pat lhs = - ML_Lex.read "val " @ ML_Lex.read (translate_string (fn "\" => "_" | s => s) pat) @ + ML_Lex.read "val " @ ML_Lex.read_source false pat @ ML_Lex.read " = " @ ML_Lex.read_source false lhs + fun ml_struct src = ML_Lex.read "functor DUMMY_FUNCTOR() = struct structure DUMMY = " @ ML_Lex.read_source false src @ @@ -89,24 +90,27 @@ fun output_type ctxt = gen_output_type (K (output ctxt)) ctxt fun output_type_ind ctxt = gen_output_type (output_indexed ctxt) ctxt +val dots_pat = translate_string (fn "_" => "\" | s => s) + (* checks and expression against a result pattern *) fun output_response ctxt (lhs, pat) = (eval_fn ctxt (ml_pat pat) lhs; - (*eval_fn ctxt (ml_out lhs);*) (*FIXME remove*) - output ctxt ((prefix_lines "" (Input.source_content lhs)) @ (prefix_lines "> " pat))) + output ctxt ((prefix_lines "" (Input.source_content lhs)) @ + (prefix_lines "> " (dots_pat (Input.source_content pat))))) (* checks the expressions, but does not check it against a result pattern *) fun output_response_fake ctxt (lhs, pat) = (eval_fn ctxt (ml_val [] NONE) lhs; - (*eval_fn ctxt (ml_out lhs);*) (* FIXME remove *) - output ctxt ((split_lines (Input.source_content lhs)) @ (prefix_lines "> " pat))) + output ctxt ( (split_lines (Input.source_content lhs)) @ + (prefix_lines "> " (dots_pat (Input.source_content pat))))) (* checks the expressions, but does not check it against a result pattern *) fun ouput_response_fake_both ctxt (lhs, pat) = - (output ctxt ((split_lines (Input.source_content lhs)) @ (prefix_lines "> " pat))) + (output ctxt ((split_lines (Input.source_content lhs)) @ + (prefix_lines "> " (dots_pat (Input.source_content pat))))) val single_arg = Scan.lift (Args.name) -val two_args = Scan.lift (Args.text_input -- Args.name) +val two_args = Scan.lift (Args.text_input -- Args.text_input) val test = Scan.lift (Args.name -- Args.name -- Scan.option (Args.$$$ "with" |-- Args.name)) val ml_setup =