File ‹Transform_Parser.ML›
signature TRANSFORM_PARSER =
sig
val dp_fun_part1_parser: ((binding * string) * ((bool * (string * Position.T)) *
(string * string) list) option) parser
val dp_fun_part2_parser: (string * (Facts.ref * Token.src list) list) parser
end
structure Transform_Parser : TRANSFORM_PARSER =
struct
val dp_fun_parser =
Parse.binding
val memoizes_parser =
Parse.name_position
val monadifies_parser =
Parse.term
-- Scan.option (
@{keyword "("}
|-- Parse.thms1 --|
@{keyword ")"})
val dp_monadify_cmd_parser =
Scan.optional (Parse.binding --| Parse.$$$ ":") Binding.empty
-- Parse.term
-- Scan.option (@{keyword "("} |--
Parse.thms1
--| @{keyword ")"})
-- Scan.option (@{keyword with_memory} |-- Parse.name_position)
val instance =
(Parse.where_ |-- Parse.and_list1 (Parse.name -- (Parse.$$$ "=" |-- Parse.term))
|| Scan.succeed [])
val dp_fun_part1_parser =
(Parse.binding --| Parse.$$$ ":")
-- Parse.term
-- Scan.option (@{keyword with_memory}
|-- Parse.opt_keyword "default_proof" -- Parse.name_position -- instance
)
val dp_fun_part2_parser =
(@{keyword "("} |-- Parse.name --| @{keyword ")"}) -- Parse.thms1
end