theory ParseWhileCommand imports Com keywords "parseWhileString" :: thy_decl begin ML {* (* Some combinators and Helpers*) fun between (a, b) s = Scan.this_string a |-- s --| Scan.this_string b; fun inParens s = between ("(", ")") s; fun maybeInParens s = inParens s || s; fun inBraces s = between ("{", "}") s; val is_stopper = Scan.is_stopper Symbol.stopper; fun unless_stop s = Scan.unless (Scan.one is_stopper) s; fun init (_::[]) = [] | init (c::cs) = c::init cs | init [] = raise Empty; *} ML {* val test = "x := 4; if (x < 3) {x := 5;}" |> String.explode |> filter (Char.isSpace #> not) |> String.implode |> Symbol.explode; *} ML {* (* Variables and values *) fun alphaToken s = List.all Char.isAlpha (String.explode s); val vname = Scan.many1 alphaToken >> String.concat >> HOLogic.mk_string; fun build_variable name = @{term Var} $ name; val variable = vname >> build_variable; val value_true = Scan.this_string "true" >> K @{term "Bool True"}; val value_false = Scan.this_string "false" >> K @{term "Bool False"}; val value_bool = value_true || value_false; val value_intg_sign = Scan.optional ($$ "-" || $$ "+") "+"; fun digitToken s = List.all Char.isDigit (String.explode s); val value_intg_num = Scan.many1 digitToken; val parseInt = String.concat #> Int.fromString #> Option.valOf #> (fn x => @{term Intg} $ HOLogic.mk_number @{typ int} x); val value_intg = value_intg_sign ::: value_intg_num >> parseInt; val value = maybeInParens (value_bool || value_intg) >> (fn t => @{term "Val"} $ t); *} ML {* (* Expressions and Commands *) val binop_eq = $$ "=" >> K @{term Eq}; val binop_and = $$ "&" >> K @{term And}; val binop_less = $$ "<" >> K @{term Less}; val binop_add = $$ "+" >> K @{term Add}; val binop_sub = $$ "-" >> K @{term Sub}; val binop = binop_eq || binop_and || binop_less || binop_add || binop_sub; fun build_binop ((e1, operator), e2) = @{term BinOp} $ e1 $ operator $ e2; fun expr_binop xs = (maybeInParens (expr_part -- binop -- expr_part) >> build_binop) xs and expr_atom xs = (inParens expr_atom || value || variable) xs and expr_part xs = (inParens expr || expr_atom) xs and expr xs = (expr_binop || expr_atom) xs; *} ML {* (* Commands and blocks *) val stmt_lass = vname --| Scan.this_string ":=" -- expr --| Scan.this_string ";" >> (fn (name, expr) => @{term LAss} $ name $ expr); fun build_seq [] = @{term Skip} | build_seq cs = List.foldr (fn (a,b) => @{term Seq} $ a $ b) (List.last cs) (init cs); fun build_cond ((e, if_block), else_block) = @{term Cond} $ e $ if_block $ else_block; fun build_while (e, b) = @{term While} $ e $ b; fun block xs = (Scan.repeat (unless_stop stmt) >> build_seq) xs and stmt_if xs = (Scan.this_string "if" |-- inParens expr -- inBraces block) xs and stmt_else xs = (Scan.this_string "else" |-- inBraces block) xs and stmt_cond xs = (stmt_if -- Scan.optional (unless_stop stmt_else) @{term Skip} >> build_cond) xs and stmt_while xs = (Scan.this_string "while" |-- inParens expr -- inBraces block >> build_while) xs and stmt xs = (stmt_cond || stmt_while || stmt_lass) xs; *} ML {* val program = Scan.finite Symbol.stopper block; val stripWhitespace = String.explode #> filter Char.isGraph #> String.implode; val programString = stripWhitespace #> Symbol.explode #> program; *} ML {* exception ParseWhileFailed of string; fun define_program (ident, prog) = fn lthy => let val ps = programString prog val v = if (length (snd ps) > 0) then raise (ParseWhileFailed (String.concat ("Parsing failed at: " :: snd ps))) else fst ps val b = (Binding.name ident, NoSyn) val t = ((Binding.name (Thm.def_name ident), []), v) val ((_, (_, def_thm)), newthy) = Local_Theory.define (b, t) lthy in (newthy |> Code.declare_default_eqns [(def_thm, true)]) end; val whileStringParser = Parse.short_ident --| Parse.$$$ "=" -- Parse.string >> define_program; let val description = "parses the given data into an Com.cmd. Syntax: parseWhileString v = \"...\""; in Outer_Syntax.local_theory @{command_keyword parseWhileString} description whileStringParser end; *} end