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