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;