diff -r 50d3059de9c6 -r 6e2479089226 ProgTutorial/antiquote_setup.ML --- a/ProgTutorial/antiquote_setup.ML Tue May 14 13:39:31 2019 +0200 +++ b/ProgTutorial/antiquote_setup.ML Tue May 14 16:59:53 2019 +0200 @@ -12,42 +12,52 @@ fun prefix_lines prfx txt = map (fn s => prfx ^ s) (split_lines txt) -fun ml_with_vars ys txt = +fun ml_with_vars' ys txt = implode ["fn ", (case ys of [] => "_" | _ => enclose "(" ")" (commas ys)), " => (", txt, ")"] -fun ml_with_struct (NONE) txt = txt - | ml_with_struct (SOME st) txt = implode ["let open ", st, " in ", txt, " end"] +fun ml_with_vars ys src = + ML_Lex.read "fn " @ ML_Lex.read (case ys of [] => "_" | _ => enclose "(" ")" (commas ys)) @ + ML_Lex.read " => (" @ src @ ML_Lex.read ")" + +fun ml_with_struct (NONE) src = ML_Lex.read_source false src + | ml_with_struct (SOME st) src = + ML_Lex.read ("let open " ^ st ^ " in ") @ ML_Lex.read_source false src @ ML_Lex.read " end" fun ml_val vs stru txt = txt |> ml_with_struct stru - |> ml_with_vars vs + |> ml_with_vars vs -fun ml_pat (lhs, pat) = - implode ["val ", translate_string (fn "\" => "_" | s => s) pat, " = ", lhs] +fun ml_pat pat lhs = + ML_Lex.read "val " @ ML_Lex.read (translate_string (fn "\" => "_" | s => s) pat) @ + ML_Lex.read " = " @ + ML_Lex.read_source false lhs -fun ml_struct txt = - implode ["functor DUMMY_FUNCTOR() = struct structure DUMMY = ", txt, " end"] +fun ml_struct src = + ML_Lex.read "functor DUMMY_FUNCTOR() = struct structure DUMMY = " @ + ML_Lex.read_source false src @ + ML_Lex.read " end" -fun ml_type txt = - implode ["val _ = NONE : (", txt, ") option"]; +fun ml_type src = + ML_Lex.read "val _ = NONE : (" @ ML_Lex.read_source false src @ ML_Lex.read ") option" (* eval function *) -fun eval_fn ctxt exp = - ML_Context.eval_source_in (SOME ctxt) ML_Compiler.flags - (Input.source false exp Position.no_range) +fun eval_fn ctxt prep exp = + ML_Context.eval_in (SOME ctxt) ML_Compiler.flags (Input.pos_of exp) (prep exp) (* checks and prints a possibly open expressions, no index *) -fun output_ml ctxt (txt, (vs, stru)) = - (eval_fn ctxt (ml_val vs stru txt); - output ctxt (split_lines txt)) -val parser_ml = Scan.lift (Args.name -- +fun output_ml ctxt (src, (vs, stru)) = + (eval_fn ctxt (ml_val vs stru) src; + output ctxt (split_lines (Input.source_content src))) + +val parser_ml = Scan.lift (Args.text_input -- (Scan.optional (Args.$$$ "for" |-- Parse.!!! (Scan.repeat1 Args.name)) [] -- Scan.option (Args.$$$ "in" |-- Parse.!!! Args.name))) + (* checks and prints a single ML-item and produces an index entry *) fun output_ml_ind ctxt (txt, stru) = - (eval_fn ctxt (ml_val [] stru txt); + (eval_fn ctxt (ml_val [] stru) (Input.string txt); case (stru, Long_Name.base_name txt, Long_Name.qualifier txt) of (NONE, _, "") => output_indexed ctxt {main = Code txt, minor = NoString} (split_lines txt) | (NONE, bn, qn) => output_indexed ctxt {main = Code bn, minor = Struct qn} (split_lines txt) @@ -58,7 +68,7 @@ (* checks and prints structures *) fun gen_output_struct outfn ctxt txt = - (eval_fn ctxt (ml_struct txt); + (eval_fn ctxt ml_struct (Input.string txt); outfn {main = Code txt, minor = Plain "structure"} (split_lines txt)) fun output_struct ctxt = gen_output_struct (K (output ctxt)) ctxt @@ -73,37 +83,34 @@ (* checks and prints types *) fun gen_output_type outfn ctxt txt = - (eval_fn ctxt (ml_type txt); + (eval_fn ctxt ml_type (Input.string txt); outfn {main = Code txt, minor = Plain "type"} (split_lines txt)) fun output_type ctxt = gen_output_type (K (output ctxt)) ctxt fun output_type_ind ctxt = gen_output_type (output_indexed ctxt) ctxt -(* checks and expression agains a result pattern *) +(* checks and expression against a result pattern *) fun output_response ctxt (lhs, pat) = - (eval_fn ctxt (ml_pat (lhs, pat)); + (eval_fn ctxt (ml_pat pat) lhs; (*eval_fn ctxt (ml_out lhs);*) (*FIXME remove*) - output ctxt ((prefix_lines "" lhs) @ (prefix_lines "> " pat))) + output ctxt ((prefix_lines "" (Input.source_content lhs)) @ (prefix_lines "> " pat))) (* checks the expressions, but does not check it against a result pattern *) fun output_response_fake ctxt (lhs, pat) = - (eval_fn ctxt (ml_val [] NONE lhs); + (eval_fn ctxt (ml_val [] NONE) lhs; (*eval_fn ctxt (ml_out lhs);*) (* FIXME remove *) - output ctxt ((split_lines lhs) @ (prefix_lines "> " pat))) + output ctxt ((split_lines (Input.source_content lhs)) @ (prefix_lines "> " pat))) (* checks the expressions, but does not check it against a result pattern *) fun ouput_response_fake_both ctxt (lhs, pat) = - (output ctxt ((split_lines lhs) @ (prefix_lines "> " pat))) + (output ctxt ((split_lines (Input.source_content lhs)) @ (prefix_lines "> " pat))) val single_arg = Scan.lift (Args.name) -val two_args = Scan.lift (Args.name -- Args.name) +val two_args = Scan.lift (Args.text_input -- Args.name) val test = Scan.lift (Args.name -- Args.name -- Scan.option (Args.$$$ "with" |-- Args.name)) - - - val ml_setup = - Thy_Output.antiquotation_raw @{binding "ML"} parser_ml output_ml + Thy_Output.antiquotation_raw @{binding "ML"} parser_ml output_ml #> Thy_Output.antiquotation_raw @{binding "ML_ind"} parser_ml_ind output_ml_ind #> Thy_Output.antiquotation_raw @{binding "ML_type"} single_arg output_type #> Thy_Output.antiquotation_raw @{binding "ML_type_ind"} single_arg output_type_ind @@ -115,19 +122,6 @@ #> Thy_Output.antiquotation_raw @{binding "ML_response_fake"} two_args output_response_fake #> Thy_Output.antiquotation_raw @{binding "ML_response_fake_both"} two_args ouput_response_fake_both -(* FIXME: experimental *) -fun ml_eq (lhs, pat, eq) = - implode ["val true = ((", eq, ") (", lhs, ",", pat, "))"] - -fun output_response_eq ctxt ((lhs, pat), eq) = - (case eq of - NONE => eval_fn ctxt (ml_pat (lhs, pat)) - | SOME e => eval_fn ctxt (ml_eq (lhs, pat, e)); - output ctxt ((prefix_lines "" lhs) @ (prefix_lines "> " pat))) - -val ml_response_setup = - Thy_Output.antiquotation_raw @{binding "ML_response_eq"} test output_response_eq - (* checks whether a file exists in the Isabelle distribution *) fun href_link txt = let @@ -188,9 +182,7 @@ val setup = ml_setup #> - ml_response_setup #> ml_file_setup #> subgoals_setup #> raw_goal_state_setup - end;