38 #> Source.exhaust |
37 #> Source.exhaust |
39 #> Chunks.transform_cmts |
38 #> Chunks.transform_cmts |
40 #> implode |
39 #> implode |
41 #> string_explode ""; |
40 #> string_explode ""; |
42 |
41 |
43 (* parser for single and two arguments *) |
|
44 val single_arg = Scan.lift (OuterParse.position Args.name) |
|
45 val two_args = Scan.lift (OuterParse.position (Args.name -- Args.name)) |
|
46 |
|
47 (* output function *) |
42 (* output function *) |
48 val output_fn = Chunks.output_list (fn _ => fn s => Pretty.str s) |
43 fun output_fn txt = Chunks.output (map Pretty.str txt) |
49 |
44 |
50 (* checks and prints open expressions *) |
45 (* checks and prints open expressions *) |
51 fun output_ml () = |
46 fun output_ml {context = ctxt, ...} (txt, ovars) = |
52 let |
47 (eval_fn ctxt (ml_val_open ovars txt); |
53 fun output {state: Toplevel.state, source = src, context = ctxt} ((txt,ovars),pos) = |
48 output_fn (transform_cmts_str txt)) |
54 (eval_fn ctxt pos (ml_val_open ovars txt); |
|
55 output_fn src ctxt (transform_cmts_str txt)) |
|
56 |
49 |
57 val parser = Scan.lift (OuterParse.position (Args.name -- |
50 val parser_ml = Scan.lift (Args.name -- |
58 (Scan.optional (Args.$$$ "for" |-- OuterParse.!!! (Scan.repeat1 Args.name)) [] -- |
51 (Scan.optional (Args.$$$ "for" |-- OuterParse.!!! (Scan.repeat1 Args.name)) [] -- |
59 Scan.optional (Args.$$$ "in" |-- OuterParse.!!! (Scan.repeat1 Args.name)) []))) |
52 Scan.optional (Args.$$$ "in" |-- OuterParse.!!! (Scan.repeat1 Args.name)) [])) |
60 in |
|
61 ThyOutput.antiquotation "ML" parser output |
|
62 end |
|
63 |
53 |
64 (* checks and prints types and structures *) |
54 (* checks and prints types and structures *) |
65 fun output_exp ml = |
55 fun output_exp ml {context = ctxt, ...} txt = |
66 let |
56 (eval_fn ctxt (ml txt); |
67 fun output {state: Toplevel.state, source = src, context = ctxt} (txt,pos) = |
57 output_fn (string_explode "" txt)) |
68 (eval_fn ctxt pos (ml txt); |
|
69 output_fn src ctxt (string_explode "" txt)) |
|
70 in |
|
71 ThyOutput.antiquotation "ML_type" single_arg output |
|
72 end |
|
73 |
58 |
74 (* checks and expression agains a result pattern *) |
59 (* checks and expression agains a result pattern *) |
75 fun output_ml_response () = |
60 fun output_response {context = ctxt, ...} (lhs, pat) = |
76 let |
61 (eval_fn ctxt (ml_pat (lhs, pat)); |
77 fun output {state: Toplevel.state, source = src, context = ctxt} ((lhs,pat),pos) = |
62 output_fn ((string_explode "" lhs) @ (string_explode "> " pat))) |
78 (eval_fn ctxt pos (ml_pat (lhs,pat)); |
|
79 output_fn src ctxt ((string_explode "" lhs) @ (string_explode "> " pat))) |
|
80 in |
|
81 ThyOutput.antiquotation "ML_response" two_args output |
|
82 end |
|
83 |
63 |
84 (* checks the expressions, but does not check it against a result pattern *) |
64 (* checks the expressions, but does not check it against a result pattern *) |
85 fun output_ml_response_fake () = |
65 fun output_response_fake {context = ctxt, ...} (lhs, pat) = |
86 let |
66 (eval_fn ctxt (ml_val lhs); |
87 fun output {state: Toplevel.state, source = src, context = ctxt} ((lhs, pat), pos) = |
67 output_fn ((string_explode "" lhs) @ (string_explode "> " pat))) |
88 (eval_fn ctxt pos (ml_val lhs); |
|
89 output_fn src ctxt ((string_explode "" lhs) @ (string_explode "> " pat))) |
|
90 in |
|
91 ThyOutput.antiquotation "ML_response_fake" two_args output |
|
92 end |
|
93 |
68 |
94 (* just prints an expression and a result pattern *) |
69 (* checks the expressions, but does not check it against a result pattern *) |
95 fun output_ml_response_fake_both () = |
70 fun ouput_response_fake_both _ (lhs, pat) = |
96 let |
71 output_fn ((string_explode "" lhs) @ (string_explode "> " pat)) |
97 fun ouput {state: Toplevel.state, source = src, context = ctxt} ((lhs,pat), _) = |
72 |
98 output_fn src ctxt ((string_explode "" lhs) @ (string_explode "> " pat)) |
73 val single_arg = Scan.lift (Args.name) |
99 in |
74 val two_args = Scan.lift (Args.name -- Args.name) |
100 ThyOutput.antiquotation "ML_response_fake_both" two_args ouput |
75 |
101 end |
76 val _ = ThyOutput.antiquotation "ML" parser_ml output_ml |
|
77 val _ = ThyOutput.antiquotation "ML_type" single_arg (output_exp ml_type) |
|
78 val _ = ThyOutput.antiquotation "ML_struct" single_arg (output_exp ml_struct) |
|
79 val _ = ThyOutput.antiquotation "ML_response" two_args output_response |
|
80 val _ = ThyOutput.antiquotation "ML_response_fake" two_args output_response_fake |
|
81 val _ = ThyOutput.antiquotation "ML_response_fake_both" two_args ouput_response_fake_both |
102 |
82 |
103 (* checks whether a file exists in the Isabelle distribution *) |
83 (* checks whether a file exists in the Isabelle distribution *) |
104 fun check_file_exists () = |
84 fun check_file_exists _ txt = |
105 let |
85 (if File.exists (Path.append (Path.explode ("~~/src")) (Path.explode txt)) |
106 fun check txt = |
86 then output_fn (string_explode "" txt) |
107 if File.exists (Path.append (Path.explode ("~~/src")) (Path.explode txt)) then () |
87 else error ("Source file " ^ (quote txt) ^ " does not exist.")) |
108 else error ("Source file " ^ (quote txt) ^ " does not exist.") |
88 |
109 in |
89 val _ = ThyOutput.antiquotation "ML_file" single_arg check_file_exists |
110 ThyOutput.antiquotation "ML_file" (Scan.lift Args.name) |
90 |
111 (fn _ => fn s => (check s; ThyOutput.output [Pretty.str s])) |
|
112 end |
|
113 |
91 |
114 (* replaces the official subgoal antiquotation with one *) |
92 (* replaces the official subgoal antiquotation with one *) |
115 (* that is closer to the actual output *) |
93 (* that is closer to the actual output *) |
116 (* |
94 fun output_goals {state = node, ...} _ = |
117 fun output_goals {state = node, source: Args.src, context: Proof.context} _ = |
95 let |
118 let |
|
119 fun subgoals 0 = "" |
96 fun subgoals 0 = "" |
120 | subgoals 1 = "goal (1 subgoal):" |
97 | subgoals 1 = "goal (1 subgoal):" |
121 | subgoals n = "goal (" ^ string_of_int n ^ " subgoals):"; |
98 | subgoals n = "goal (" ^ string_of_int n ^ " subgoals):" |
122 |
99 |
123 fun proof_state node = |
100 fun proof_state state = |
124 (case Option.map Toplevel.proof_node node of |
101 (case try Toplevel.proof_of state of |
125 SOME (SOME prf) => ProofNode.current prf |
102 SOME prf => prf |
126 | _ => error "No proof state"); |
103 | _ => error "No proof state") |
127 |
104 |
128 val state = proof_state node; |
105 val state = proof_state node; |
129 val goals = Proof.pretty_goals false state; |
106 val goals = Proof.pretty_goals false state; |
130 |
107 |
131 val {prop, ...} = rep_thm (Proof.get_goal state |> snd |> snd); |
108 val {prop, ...} = rep_thm (Proof.get_goal state |> snd |> snd); |
132 val (As, B) = Logic.strip_horn prop; |
109 val (As, B) = Logic.strip_horn prop; |
133 val output' = (case (length As) of |
110 val output = (case (length As) of |
134 0 => goals |
111 0 => goals |
135 | n => (Pretty.str (subgoals n))::goals) |
112 | n => (Pretty.str (subgoals n))::goals) |
136 in |
113 in |
137 output |
114 ThyOutput.output output |
138 end |
115 end |
139 *) |
|
140 |
116 |
141 |
117 |
142 val _ = output_ml (); |
118 val _ = ThyOutput.antiquotation "subgoals" (Scan.succeed ()) output_goals |
143 val _ = check_file_exists (); |
|
144 val _ = output_ml_response (); |
|
145 val _ = output_ml_response_fake (); |
|
146 val _ = output_ml_response_fake_both (); |
|
147 val _ = output_exp ml_struct; |
|
148 val _ = output_exp ml_type; |
|
149 (*val _ = output_goals*) |
|
150 |
119 |
151 end; |
120 end; |