10 implode (map f (Symbol.explode str)) |
10 implode (map f (Symbol.explode str)) |
11 |
11 |
12 fun prefix_lines prfx txt = |
12 fun prefix_lines prfx txt = |
13 map (fn s => prfx ^ s) (split_lines txt) |
13 map (fn s => prfx ^ s) (split_lines txt) |
14 |
14 |
15 fun ml_with_vars ys txt = |
15 fun ml_with_vars' ys txt = |
16 implode ["fn ", (case ys of [] => "_" | _ => enclose "(" ")" (commas ys)), " => (", txt, ")"] |
16 implode ["fn ", (case ys of [] => "_" | _ => enclose "(" ")" (commas ys)), " => (", txt, ")"] |
17 |
17 |
18 fun ml_with_struct (NONE) txt = txt |
18 fun ml_with_vars ys src = |
19 | ml_with_struct (SOME st) txt = implode ["let open ", st, " in ", txt, " end"] |
19 ML_Lex.read "fn " @ ML_Lex.read (case ys of [] => "_" | _ => enclose "(" ")" (commas ys)) @ |
|
20 ML_Lex.read " => (" @ src @ ML_Lex.read ")" |
|
21 |
|
22 fun ml_with_struct (NONE) src = ML_Lex.read_source false src |
|
23 | ml_with_struct (SOME st) src = |
|
24 ML_Lex.read ("let open " ^ st ^ " in ") @ ML_Lex.read_source false src @ ML_Lex.read " end" |
20 |
25 |
21 fun ml_val vs stru txt = |
26 fun ml_val vs stru txt = |
22 txt |> ml_with_struct stru |
27 txt |> ml_with_struct stru |
23 |> ml_with_vars vs |
28 |> ml_with_vars vs |
24 |
29 |
25 fun ml_pat (lhs, pat) = |
30 fun ml_pat pat lhs = |
26 implode ["val ", translate_string (fn "\<dots>" => "_" | s => s) pat, " = ", lhs] |
31 ML_Lex.read "val " @ ML_Lex.read (translate_string (fn "\<dots>" => "_" | s => s) pat) @ |
|
32 ML_Lex.read " = " @ |
|
33 ML_Lex.read_source false lhs |
27 |
34 |
28 fun ml_struct txt = |
35 fun ml_struct src = |
29 implode ["functor DUMMY_FUNCTOR() = struct structure DUMMY = ", txt, " end"] |
36 ML_Lex.read "functor DUMMY_FUNCTOR() = struct structure DUMMY = " @ |
|
37 ML_Lex.read_source false src @ |
|
38 ML_Lex.read " end" |
30 |
39 |
31 fun ml_type txt = |
40 fun ml_type src = |
32 implode ["val _ = NONE : (", txt, ") option"]; |
41 ML_Lex.read "val _ = NONE : (" @ ML_Lex.read_source false src @ ML_Lex.read ") option" |
33 |
42 |
34 (* eval function *) |
43 (* eval function *) |
35 fun eval_fn ctxt exp = |
44 fun eval_fn ctxt prep exp = |
36 ML_Context.eval_source_in (SOME ctxt) ML_Compiler.flags |
45 ML_Context.eval_in (SOME ctxt) ML_Compiler.flags (Input.pos_of exp) (prep exp) |
37 (Input.source false exp Position.no_range) |
|
38 |
46 |
39 (* checks and prints a possibly open expressions, no index *) |
47 (* checks and prints a possibly open expressions, no index *) |
40 fun output_ml ctxt (txt, (vs, stru)) = |
|
41 (eval_fn ctxt (ml_val vs stru txt); |
|
42 output ctxt (split_lines txt)) |
|
43 |
48 |
44 val parser_ml = Scan.lift (Args.name -- |
49 fun output_ml ctxt (src, (vs, stru)) = |
|
50 (eval_fn ctxt (ml_val vs stru) src; |
|
51 output ctxt (split_lines (Input.source_content src))) |
|
52 |
|
53 val parser_ml = Scan.lift (Args.text_input -- |
45 (Scan.optional (Args.$$$ "for" |-- Parse.!!! (Scan.repeat1 Args.name)) [] -- |
54 (Scan.optional (Args.$$$ "for" |-- Parse.!!! (Scan.repeat1 Args.name)) [] -- |
46 Scan.option (Args.$$$ "in" |-- Parse.!!! Args.name))) |
55 Scan.option (Args.$$$ "in" |-- Parse.!!! Args.name))) |
47 |
56 |
|
57 |
48 (* checks and prints a single ML-item and produces an index entry *) |
58 (* checks and prints a single ML-item and produces an index entry *) |
49 fun output_ml_ind ctxt (txt, stru) = |
59 fun output_ml_ind ctxt (txt, stru) = |
50 (eval_fn ctxt (ml_val [] stru txt); |
60 (eval_fn ctxt (ml_val [] stru) (Input.string txt); |
51 case (stru, Long_Name.base_name txt, Long_Name.qualifier txt) of |
61 case (stru, Long_Name.base_name txt, Long_Name.qualifier txt) of |
52 (NONE, _, "") => output_indexed ctxt {main = Code txt, minor = NoString} (split_lines txt) |
62 (NONE, _, "") => output_indexed ctxt {main = Code txt, minor = NoString} (split_lines txt) |
53 | (NONE, bn, qn) => output_indexed ctxt {main = Code bn, minor = Struct qn} (split_lines txt) |
63 | (NONE, bn, qn) => output_indexed ctxt {main = Code bn, minor = Struct qn} (split_lines txt) |
54 | (SOME st, _, _) => output_indexed ctxt {main = Code txt, minor = Struct st} (split_lines txt)) |
64 | (SOME st, _, _) => output_indexed ctxt {main = Code txt, minor = Struct st} (split_lines txt)) |
55 |
65 |
56 val parser_ml_ind = Scan.lift (Args.name -- |
66 val parser_ml_ind = Scan.lift (Args.name -- |
57 Scan.option (Args.$$$ "in" |-- Parse.!!! Args.name)) |
67 Scan.option (Args.$$$ "in" |-- Parse.!!! Args.name)) |
58 |
68 |
59 (* checks and prints structures *) |
69 (* checks and prints structures *) |
60 fun gen_output_struct outfn ctxt txt = |
70 fun gen_output_struct outfn ctxt txt = |
61 (eval_fn ctxt (ml_struct txt); |
71 (eval_fn ctxt ml_struct (Input.string txt); |
62 outfn {main = Code txt, minor = Plain "structure"} (split_lines txt)) |
72 outfn {main = Code txt, minor = Plain "structure"} (split_lines txt)) |
63 |
73 |
64 fun output_struct ctxt = gen_output_struct (K (output ctxt)) ctxt |
74 fun output_struct ctxt = gen_output_struct (K (output ctxt)) ctxt |
65 fun output_struct_ind ctxt = gen_output_struct (output_indexed ctxt) ctxt |
75 fun output_struct_ind ctxt = gen_output_struct (output_indexed ctxt) ctxt |
66 |
76 |
71 fun output_funct ctxt = gen_output_funct (K (output ctxt)) |
81 fun output_funct ctxt = gen_output_funct (K (output ctxt)) |
72 fun output_funct_ind ctxt = gen_output_funct (output_indexed ctxt) |
82 fun output_funct_ind ctxt = gen_output_funct (output_indexed ctxt) |
73 |
83 |
74 (* checks and prints types *) |
84 (* checks and prints types *) |
75 fun gen_output_type outfn ctxt txt = |
85 fun gen_output_type outfn ctxt txt = |
76 (eval_fn ctxt (ml_type txt); |
86 (eval_fn ctxt ml_type (Input.string txt); |
77 outfn {main = Code txt, minor = Plain "type"} (split_lines txt)) |
87 outfn {main = Code txt, minor = Plain "type"} (split_lines txt)) |
78 |
88 |
79 fun output_type ctxt = gen_output_type (K (output ctxt)) ctxt |
89 fun output_type ctxt = gen_output_type (K (output ctxt)) ctxt |
80 fun output_type_ind ctxt = gen_output_type (output_indexed ctxt) ctxt |
90 fun output_type_ind ctxt = gen_output_type (output_indexed ctxt) ctxt |
81 |
91 |
82 (* checks and expression agains a result pattern *) |
92 (* checks and expression against a result pattern *) |
83 fun output_response ctxt (lhs, pat) = |
93 fun output_response ctxt (lhs, pat) = |
84 (eval_fn ctxt (ml_pat (lhs, pat)); |
94 (eval_fn ctxt (ml_pat pat) lhs; |
85 (*eval_fn ctxt (ml_out lhs);*) (*FIXME remove*) |
95 (*eval_fn ctxt (ml_out lhs);*) (*FIXME remove*) |
86 output ctxt ((prefix_lines "" lhs) @ (prefix_lines "> " pat))) |
96 output ctxt ((prefix_lines "" (Input.source_content lhs)) @ (prefix_lines "> " pat))) |
87 |
97 |
88 (* checks the expressions, but does not check it against a result pattern *) |
98 (* checks the expressions, but does not check it against a result pattern *) |
89 fun output_response_fake ctxt (lhs, pat) = |
99 fun output_response_fake ctxt (lhs, pat) = |
90 (eval_fn ctxt (ml_val [] NONE lhs); |
100 (eval_fn ctxt (ml_val [] NONE) lhs; |
91 (*eval_fn ctxt (ml_out lhs);*) (* FIXME remove *) |
101 (*eval_fn ctxt (ml_out lhs);*) (* FIXME remove *) |
92 output ctxt ((split_lines lhs) @ (prefix_lines "> " pat))) |
102 output ctxt ((split_lines (Input.source_content lhs)) @ (prefix_lines "> " pat))) |
93 |
103 |
94 (* checks the expressions, but does not check it against a result pattern *) |
104 (* checks the expressions, but does not check it against a result pattern *) |
95 fun ouput_response_fake_both ctxt (lhs, pat) = |
105 fun ouput_response_fake_both ctxt (lhs, pat) = |
96 (output ctxt ((split_lines lhs) @ (prefix_lines "> " pat))) |
106 (output ctxt ((split_lines (Input.source_content lhs)) @ (prefix_lines "> " pat))) |
97 |
107 |
98 val single_arg = Scan.lift (Args.name) |
108 val single_arg = Scan.lift (Args.name) |
99 val two_args = Scan.lift (Args.name -- Args.name) |
109 val two_args = Scan.lift (Args.text_input -- Args.name) |
100 val test = Scan.lift (Args.name -- Args.name -- Scan.option (Args.$$$ "with" |-- Args.name)) |
110 val test = Scan.lift (Args.name -- Args.name -- Scan.option (Args.$$$ "with" |-- Args.name)) |
101 |
111 |
102 |
|
103 |
|
104 |
|
105 val ml_setup = |
112 val ml_setup = |
106 Thy_Output.antiquotation_raw @{binding "ML"} parser_ml output_ml |
113 Thy_Output.antiquotation_raw @{binding "ML"} parser_ml output_ml |
107 #> Thy_Output.antiquotation_raw @{binding "ML_ind"} parser_ml_ind output_ml_ind |
114 #> Thy_Output.antiquotation_raw @{binding "ML_ind"} parser_ml_ind output_ml_ind |
108 #> Thy_Output.antiquotation_raw @{binding "ML_type"} single_arg output_type |
115 #> Thy_Output.antiquotation_raw @{binding "ML_type"} single_arg output_type |
109 #> Thy_Output.antiquotation_raw @{binding "ML_type_ind"} single_arg output_type_ind |
116 #> Thy_Output.antiquotation_raw @{binding "ML_type_ind"} single_arg output_type_ind |
110 #> Thy_Output.antiquotation_raw @{binding "ML_struct"} single_arg output_struct |
117 #> Thy_Output.antiquotation_raw @{binding "ML_struct"} single_arg output_struct |
111 #> Thy_Output.antiquotation_raw @{binding "ML_struct_ind"} single_arg output_struct_ind |
118 #> Thy_Output.antiquotation_raw @{binding "ML_struct_ind"} single_arg output_struct_ind |
112 #> Thy_Output.antiquotation_raw @{binding "ML_funct"} single_arg output_funct |
119 #> Thy_Output.antiquotation_raw @{binding "ML_funct"} single_arg output_funct |
113 #> Thy_Output.antiquotation_raw @{binding "ML_funct_ind"} single_arg output_funct_ind |
120 #> Thy_Output.antiquotation_raw @{binding "ML_funct_ind"} single_arg output_funct_ind |
114 #> Thy_Output.antiquotation_raw @{binding "ML_response"} two_args output_response |
121 #> Thy_Output.antiquotation_raw @{binding "ML_response"} two_args output_response |
115 #> Thy_Output.antiquotation_raw @{binding "ML_response_fake"} two_args output_response_fake |
122 #> Thy_Output.antiquotation_raw @{binding "ML_response_fake"} two_args output_response_fake |
116 #> Thy_Output.antiquotation_raw @{binding "ML_response_fake_both"} two_args ouput_response_fake_both |
123 #> Thy_Output.antiquotation_raw @{binding "ML_response_fake_both"} two_args ouput_response_fake_both |
117 |
|
118 (* FIXME: experimental *) |
|
119 fun ml_eq (lhs, pat, eq) = |
|
120 implode ["val true = ((", eq, ") (", lhs, ",", pat, "))"] |
|
121 |
|
122 fun output_response_eq ctxt ((lhs, pat), eq) = |
|
123 (case eq of |
|
124 NONE => eval_fn ctxt (ml_pat (lhs, pat)) |
|
125 | SOME e => eval_fn ctxt (ml_eq (lhs, pat, e)); |
|
126 output ctxt ((prefix_lines "" lhs) @ (prefix_lines "> " pat))) |
|
127 |
|
128 val ml_response_setup = |
|
129 Thy_Output.antiquotation_raw @{binding "ML_response_eq"} test output_response_eq |
|
130 |
124 |
131 (* checks whether a file exists in the Isabelle distribution *) |
125 (* checks whether a file exists in the Isabelle distribution *) |
132 fun href_link txt = |
126 fun href_link txt = |
133 let |
127 let |
134 val raw = I (* FIXME: Symbol.encode_raw *) |
128 val raw = I (* FIXME: Symbol.encode_raw *) |