Hi,
following Stefan Berghofers presentation at the Isabelle Developer
Workshop I find Parse.term behaving not as expected:
text {* should not Parse.term repeat until a non-term token is reached ? *}
ML {*
parse Parse.term "xxx +++ 111 end";
(*val it =
("\^E\^Ftoken\^Exxx\^E\^F\^E",
[Token (("+++", ({}, {})), (SymIdent, "+++"), Slot), Token (("111", ({}, {})), (Nat,
"111"), Slot),
Token (("end", ({}, {})), (Command, "end"), Slot)])
: string * Token.T list*)
parse (Scan.repeat Parse.term) "xxx +++ 111 end";
(*val it =
(["\^E\^Ftoken\^Exxx\^E\^F\^E", "\^E\^Ftoken\^E+++\^E\^F\^E",
"\^E\^Ftoken\^E111\^E\^F\^E"],
[Token (("end", ({}, {})), (Command, "end"), Slot)])
: string list * Token.T list*)
*}
text {* Parse.term stops at "Keyword" of outer syntax ?!?
Should not be parsed according to inner syntax ? *}
ML {*
parse Parse.term "xxx + 111 end";
(*val it =
("\^E\^Ftoken\^Exxx\^E\^F\^E",
[Token (("+", ({}, {})), (Keyword, "+"), Slot), Token (("111", ({}, {})), (Nat,
"111"), Slot),
Token (("end", ({}, {})), (Command, "end"), Slot)])
: string * Token.T list*)
parse Parse.term "xxx +++ (111) end";
(*val it =
("\^E\^Ftoken\^Exxx\^E\^F\^E",
[Token (("+++", ({}, {})), (SymIdent, "+++"), Slot), Token (("(", ({}, {})),
(Keyword, "("), Slot),
Token (("111", ({}, {})), (Nat, "111"), Slot), Token ((")", ({}, {})), (Keyword,
")"), Slot),
Token (("end", ({}, {})), (Command, "end"), Slot)])
: string * Token.T list*)
*}
What am I doing wrong ?
With kind regards,
Walther
PS: In the attached file I searched for where the inner syntax could
come into Parse.term --- so far without success.
--
------------------------------------------------------------------------
Walther Neuper Mailto: [email protected]
Institute for Software Technology Tel: +43-(0)316/873-5728
University of Technology Fax: +43-(0)316/873-5706
Graz, Austria Home: www.ist.tugraz.at/neuper
------------------------------------------------------------------------
header {* experiments on scanning and parsing
following Stefan Berghofers presentation
at the Isabelle Developer Workshop 2010 *}
theory Test_Parse_Term
imports Main
begin
section {* parse following Stefan Berghofer at Isabelle Developer Workshop 2010
*}
ML {*
fun filtered_input str =
filter Token.is_proper (Outer_Syntax.scan Position.none str);
fun parse p str = Scan.finite Token.stopper p (filtered_input str);
*}
text {* should not Parse.term repeat until a non-term token is reached ? *}
ML {*
parse Parse.term "xxx +++ 111 end";
(*val it =
("\^E\^Ftoken\^Exxx\^E\^F\^E",
[Token (("+++", ({}, {})), (SymIdent, "+++"), Slot), Token (("111", ({},
{})), (Nat, "111"), Slot),
Token (("end", ({}, {})), (Command, "end"), Slot)])
: string * Token.T list*)
parse (Scan.repeat Parse.term) "xxx +++ 111 end";
(*val it =
(["\^E\^Ftoken\^Exxx\^E\^F\^E", "\^E\^Ftoken\^E+++\^E\^F\^E",
"\^E\^Ftoken\^E111\^E\^F\^E"],
[Token (("end", ({}, {})), (Command, "end"), Slot)])
: string list * Token.T list*)
*}
text {* Parse.term stops at "Keyword" of outer syntax ?!?
Should not be parsed according to inner xyntax ? *}
ML {*
parse Parse.term "xxx + 111 end";
(*val it =
("\^E\^Ftoken\^Exxx\^E\^F\^E",
[Token (("+", ({}, {})), (Keyword, "+"), Slot), Token (("111", ({}, {})),
(Nat, "111"), Slot),
Token (("end", ({}, {})), (Command, "end"), Slot)])
: string * Token.T list*)
parse Parse.term "xxx +++ (111) end";
(*val it =
("\^E\^Ftoken\^Exxx\^E\^F\^E",
[Token (("+++", ({}, {})), (SymIdent, "+++"), Slot), Token (("(", ({},
{})), (Keyword, "("), Slot),
Token (("111", ({}, {})), (Nat, "111"), Slot), Token ((")", ({}, {})),
(Keyword, ")"), Slot),
Token (("end", ({}, {})), (Command, "end"), Slot)])
: string * Token.T list*)
*}
section {* decompose term *}
text {* where does the inner syntax come in ? *}
ML {*
"---from src/Pure/Isar/token.ML
----------------------------------------------------------------------------------";
datatype value =
Text of string | Typ of typ | Term of term | Fact of thm list | Attribute of
morphism -> attribute;
datatype slot =
Slot | Value of value option | Assignable of value option Unsynchronized.ref;
datatype kind =
Command | Keyword | Ident | LongIdent | SymIdent | Var | TypeIdent | TypeVar |
Nat | String | AltString | Verbatim | Space | Comment | InternalValue |
Malformed | Error of string | Sync | EOF;
datatype T = Token of (Symbol_Pos.text * Position.range) * (kind * string) *
slot;
fun source_of
(Token ((source, (pos, _)), _, _)) =
YXML.string_of (XML.Elem (Markup.tokenN,
Position.properties_of pos, [XML.Text source]));
(*fn : T ->
string*)
"---from src/Pure/General/scan.ML
--------------------------------------------------------------------------------";
fun ahead scan xs = (fst (scan xs), xs);
(*fn : ('a -> 'b * 'c) -> 'a -> 'b * 'a*)
"---from src/Pure/Isar/parse.ML
----------------------------------------------------------------------------------";
(*fn : Token.T list -> string
* Token.T list*)
fun fail_with s =
Scan.fail_with
(fn [] => s ^ "
expected (past end-of-file!)"
| (tok :: _) =>
(case
Token.text_of tok of
(txt, "") =>
s ^ "
expected,\nbut " ^ txt ^ Token.pos_of tok
^ " was
found"
| (txt1, txt2)
=>
s ^ "
expected,\nbut " ^ txt1 ^ Token.pos_of tok
^ " was
found:\n" ^ txt2));
(*fn : string ->
Token.T list -> 'a*)
fun RESET_VALUE atom =
Scan.ahead (Scan.one (K true)) --
atom >> (fn (arg,
x) => (Token.assign NONE arg; x));
(*fn : (Token.T
list -> 'a * 'b) -> Token.T list -> 'a * 'b*)
val not_eof = RESET_VALUE
(Scan.one Token.not_eof);
(*fn : Token.T list ->
Token.T * Token.T list*)
fun inner_syntax atom = Scan.ahead atom |-- not_eof >> Token.source_of;
(*fn : (Token.T list -> 'a * 'b) -> Token.T list -> string * Token.T
list*)
fun group s scan = scan || fail_with s;
(*fn : string -> (Token.T list -> 'a) ->
Token.T list -> 'a*)
val trm = Parse.short_ident ||
Parse.long_ident || Parse.sym_ident ||
Parse.term_var ||
Parse.number || Parse.string;
val term_group = group "term" trm;
(*fn : Token.T list -> string * Token.T list*)
val term = inner_syntax term_group;
(*fn : Token.T list -> string * Token.T list*)
*}
end_______________________________________________
Isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
