# HG changeset patch # User Christian Urban # Date 1236867935 0 # Node ID 18f90044c7774bdbb8c7290b920439cbf520127c # Parent 90bee31628dcb4600c961ba5bf44caf093e2c5e3 simplified antiquotations diff -r 90bee31628dc -r 18f90044c777 CookBook/FirstSteps.thy --- a/CookBook/FirstSteps.thy Thu Mar 12 08:11:02 2009 +0100 +++ b/CookBook/FirstSteps.thy Thu Mar 12 14:25:35 2009 +0000 @@ -169,11 +169,7 @@ end fun str_of_thm ctxt thm = -let - val {prop, ...} = crep_thm (no_vars ctxt thm) -in - str_of_cterm ctxt prop -end*} + str_of_cterm ctxt (#prop (crep_thm (no_vars ctxt thm)))*} text {* Again the function @{ML commas} helps with printing more than one theorem. @@ -533,7 +529,7 @@ ML{*fun make_imp P Q tau = let - val x = Free ("x",tau) + val x = Free ("x", tau) in Logic.all x (Logic.mk_implies (P $ x, Q $ x)) end *} diff -r 90bee31628dc -r 18f90044c777 CookBook/Recipes/Antiquotes.thy --- a/CookBook/Recipes/Antiquotes.thy Thu Mar 12 08:11:02 2009 +0100 +++ b/CookBook/Recipes/Antiquotes.thy Thu Mar 12 14:25:35 2009 +0000 @@ -46,13 +46,13 @@ text {* - Note that the parser @{ML "(Scan.lift Args.name)"} in line 9 parses a string, + The parser @{ML "(Scan.lift Args.name)"} in line 9 parses a string, in this case the code. As mentioned before, the code is sent to the ML-compiler in the line 4 using the function @{ML ml_val}, which constructs the appropriate ML-expression. If the code is ``approved'' by the compiler, then the output function @{ML "ThyOutput.output"} in the next line pretty prints the - code. This function expects that the code is a list of strings where each + code. This function expects that the code is a list of (pretty)strings where each string correspond to a line in the output. Therefore the use of @{ML "(space_explode \"\\n\" txt)" for txt} which produces this list according to linebreaks. There are a number of options @@ -69,7 +69,7 @@ can improve the code above slightly by writing *} -ML%linenosgray{*fun output_ml {context = ctxt, ...} (code_txt,pos) = +ML%linenosgray{*fun output_ml {context = ctxt, ...} (code_txt, pos) = (ML_Context.eval_in (SOME ctxt) false pos (ml_val code_txt); ThyOutput.output (map Pretty.str (space_explode "\n" code_txt))) @@ -77,7 +77,9 @@ (Scan.lift (OuterParse.position Args.name)) output_ml *} text {* - where in Lines 1 and 2 the positional information is properly treated. + where in Lines 1 and 2 the positional information is properly treated. The + parser @{ML OuterParse.position} encodes the positional information in the + result. We can now write in a document @{text "@{ML_checked \"2 + 3\"}"} in order to obtain @{ML_checked "2 + 3"} and be sure that this code compiles until diff -r 90bee31628dc -r 18f90044c777 CookBook/antiquote_setup.ML --- a/CookBook/antiquote_setup.ML Thu Mar 12 08:11:02 2009 +0100 +++ b/CookBook/antiquote_setup.ML Thu Mar 12 14:25:35 2009 +0000 @@ -4,7 +4,6 @@ struct (* functions for generating appropriate expressions *) - fun ml_val_open (ys, xs) txt = let fun ml_val_open_aux ys txt = "fn " ^ (case ys of [] => "_" | _ => enclose "(" ")" (commas ys)) ^ " => (" ^ txt ^ ")"; @@ -25,8 +24,8 @@ fun ml_type txt = "val _ = NONE : (" ^ txt ^ ") option"; (* eval function *) -fun eval_fn ctxt pos exp = - ML_Context.eval_in (SOME ctxt) false pos exp +fun eval_fn ctxt exp = + ML_Context.eval_in (SOME ctxt) false Position.none exp (* string functions *) fun string_explode str txt = @@ -40,112 +39,82 @@ #> implode #> string_explode ""; -(* parser for single and two arguments *) -val single_arg = Scan.lift (OuterParse.position Args.name) -val two_args = Scan.lift (OuterParse.position (Args.name -- Args.name)) - (* output function *) -val output_fn = Chunks.output_list (fn _ => fn s => Pretty.str s) +fun output_fn txt = Chunks.output (map Pretty.str txt) (* checks and prints open expressions *) -fun output_ml () = -let - fun output {state: Toplevel.state, source = src, context = ctxt} ((txt,ovars),pos) = - (eval_fn ctxt pos (ml_val_open ovars txt); - output_fn src ctxt (transform_cmts_str txt)) +fun output_ml {context = ctxt, ...} (txt, ovars) = + (eval_fn ctxt (ml_val_open ovars txt); + output_fn (transform_cmts_str txt)) - val parser = Scan.lift (OuterParse.position (Args.name -- - (Scan.optional (Args.$$$ "for" |-- OuterParse.!!! (Scan.repeat1 Args.name)) [] -- - Scan.optional (Args.$$$ "in" |-- OuterParse.!!! (Scan.repeat1 Args.name)) []))) -in - ThyOutput.antiquotation "ML" parser output -end +val parser_ml = Scan.lift (Args.name -- + (Scan.optional (Args.$$$ "for" |-- OuterParse.!!! (Scan.repeat1 Args.name)) [] -- + Scan.optional (Args.$$$ "in" |-- OuterParse.!!! (Scan.repeat1 Args.name)) [])) (* checks and prints types and structures *) -fun output_exp ml = -let - fun output {state: Toplevel.state, source = src, context = ctxt} (txt,pos) = - (eval_fn ctxt pos (ml txt); - output_fn src ctxt (string_explode "" txt)) -in - ThyOutput.antiquotation "ML_type" single_arg output -end +fun output_exp ml {context = ctxt, ...} txt = + (eval_fn ctxt (ml txt); + output_fn (string_explode "" txt)) (* checks and expression agains a result pattern *) -fun output_ml_response () = -let - fun output {state: Toplevel.state, source = src, context = ctxt} ((lhs,pat),pos) = - (eval_fn ctxt pos (ml_pat (lhs,pat)); - output_fn src ctxt ((string_explode "" lhs) @ (string_explode "> " pat))) -in - ThyOutput.antiquotation "ML_response" two_args output -end +fun output_response {context = ctxt, ...} (lhs, pat) = + (eval_fn ctxt (ml_pat (lhs, pat)); + output_fn ((string_explode "" lhs) @ (string_explode "> " pat))) + +(* checks the expressions, but does not check it against a result pattern *) +fun output_response_fake {context = ctxt, ...} (lhs, pat) = + (eval_fn ctxt (ml_val lhs); + output_fn ((string_explode "" lhs) @ (string_explode "> " pat))) (* checks the expressions, but does not check it against a result pattern *) -fun output_ml_response_fake () = -let - fun output {state: Toplevel.state, source = src, context = ctxt} ((lhs, pat), pos) = - (eval_fn ctxt pos (ml_val lhs); - output_fn src ctxt ((string_explode "" lhs) @ (string_explode "> " pat))) -in - ThyOutput.antiquotation "ML_response_fake" two_args output -end +fun ouput_response_fake_both _ (lhs, pat) = + output_fn ((string_explode "" lhs) @ (string_explode "> " pat)) + +val single_arg = Scan.lift (Args.name) +val two_args = Scan.lift (Args.name -- Args.name) -(* just prints an expression and a result pattern *) -fun output_ml_response_fake_both () = -let - fun ouput {state: Toplevel.state, source = src, context = ctxt} ((lhs,pat), _) = - output_fn src ctxt ((string_explode "" lhs) @ (string_explode "> " pat)) -in - ThyOutput.antiquotation "ML_response_fake_both" two_args ouput -end +val _ = ThyOutput.antiquotation "ML" parser_ml output_ml +val _ = ThyOutput.antiquotation "ML_type" single_arg (output_exp ml_type) +val _ = ThyOutput.antiquotation "ML_struct" single_arg (output_exp ml_struct) +val _ = ThyOutput.antiquotation "ML_response" two_args output_response +val _ = ThyOutput.antiquotation "ML_response_fake" two_args output_response_fake +val _ = ThyOutput.antiquotation "ML_response_fake_both" two_args ouput_response_fake_both (* checks whether a file exists in the Isabelle distribution *) -fun check_file_exists () = -let - fun check txt = - if File.exists (Path.append (Path.explode ("~~/src")) (Path.explode txt)) then () - else error ("Source file " ^ (quote txt) ^ " does not exist.") -in - ThyOutput.antiquotation "ML_file" (Scan.lift Args.name) - (fn _ => fn s => (check s; ThyOutput.output [Pretty.str s])) -end +fun check_file_exists _ txt = + (if File.exists (Path.append (Path.explode ("~~/src")) (Path.explode txt)) + then output_fn (string_explode "" txt) + else error ("Source file " ^ (quote txt) ^ " does not exist.")) + +val _ = ThyOutput.antiquotation "ML_file" single_arg check_file_exists + (* replaces the official subgoal antiquotation with one *) (* that is closer to the actual output *) -(* -fun output_goals {state = node, source: Args.src, context: Proof.context} _ = -let +fun output_goals {state = node, ...} _ = +let fun subgoals 0 = "" | subgoals 1 = "goal (1 subgoal):" - | subgoals n = "goal (" ^ string_of_int n ^ " subgoals):"; - - fun proof_state node = - (case Option.map Toplevel.proof_node node of - SOME (SOME prf) => ProofNode.current prf - | _ => error "No proof state"); + | subgoals n = "goal (" ^ string_of_int n ^ " subgoals):" + + fun proof_state state = + (case try Toplevel.proof_of state of + SOME prf => prf + | _ => error "No proof state") val state = proof_state node; val goals = Proof.pretty_goals false state; val {prop, ...} = rep_thm (Proof.get_goal state |> snd |> snd); val (As, B) = Logic.strip_horn prop; - val output' = (case (length As) of + val output = (case (length As) of 0 => goals | n => (Pretty.str (subgoals n))::goals) in - output + ThyOutput.output output end -*) -val _ = output_ml (); -val _ = check_file_exists (); -val _ = output_ml_response (); -val _ = output_ml_response_fake (); -val _ = output_ml_response_fake_both (); -val _ = output_exp ml_struct; -val _ = output_exp ml_type; -(*val _ = output_goals*) +val _ = ThyOutput.antiquotation "subgoals" (Scan.succeed ()) output_goals end; diff -r 90bee31628dc -r 18f90044c777 CookBook/chunks.ML --- a/CookBook/chunks.ML Thu Mar 12 08:11:02 2009 +0100 +++ b/CookBook/chunks.ML Thu Mar 12 14:25:35 2009 +0000 @@ -2,20 +2,14 @@ structure Chunks = struct -(* rebuilding the output_list function from ThyOutput in order to *) -(* enable the options [gray, linenos] *) +(* rebuilding the output function from ThyOutput in order to *) +(* enable the options [gray, linenos] *) val gray = ref false; val linenos = ref false -fun boolean "" = true - | boolean "true" = true - | boolean "false" = false - | boolean s = error ("Bad boolean value: " ^ quote s); - -fun output_list pretty src ctxt xs = - map (pretty ctxt) xs (*always pretty in order to exhibit errors!*) - |> (if ! ThyOutput.source then K [ThyOutput.pretty_text (ThyOutput.str_of_source src)] else I) +fun output prts = + prts |> (if ! ThyOutput.quotes then map Pretty.quote else I) |> (if ! ThyOutput.display then map (Output.output o Pretty.string_of o Pretty.indent (! ThyOutput.indent)) @@ -23,12 +17,16 @@ #> (if ! linenos then (enclose "\\begin{linenos}%\n" "%\n\\end{linenos}") else I) #> (if ! gray then (enclose "\\begin{graybox}%\n" "%\n\\end{graybox}") else I) #> enclose "\\begin{isabelle}%\n" "%\n\\end{isabelle}" - else + else map (Output.output o (if ! ThyOutput.break then Pretty.string_of else Pretty.str_of)) #> space_implode "\\isasep\\isanewline%\n" #> enclose "\\isa{" "}"); -fun output pretty src ctxt = output_list pretty src ctxt o single + +fun boolean "" = true + | boolean "true" = true + | boolean "false" = false + | boolean s = error ("Bad boolean value: " ^ quote s); val _ = ThyOutput.add_options [("gray", Library.setmp gray o boolean), @@ -161,7 +159,7 @@ val txt = spc ^ implode (transform_cmts toks') in txt |> split_lines |> - output_list (fn _ => fn s => Pretty.str s) src ctxt + (map Pretty.str) |> output end; val _ = ThyOutput.antiquotation "ML_chunk" (Scan.lift Args.name) output_chunk; diff -r 90bee31628dc -r 18f90044c777 cookbook.pdf Binary file cookbook.pdf has changed