1 (* Auxiliary antiquotations for the tutorial. *)

     2 

     3 structure AntiquoteSetup: sig end =

     4 struct

     5 

     6 (* functions for generating appropriate expressions *)

     7 fun ml_val_open (ys, xs) txt = 

     8   let fun ml_val_open_aux ys txt = 

     9           "fn " ^ (case ys of [] => "_" | _ => enclose "(" ")" (commas ys)) ^ " => (" ^ txt ^ ")";

    10   in

    11     (case xs of

    12        [] => ml_val_open_aux ys txt

    13      | _  => ml_val_open_aux ys ("let open " ^ (space_implode " " xs) ^ " in " ^ txt ^ " end"))

    14   end;

    15 

    16 fun ml_val txt = ml_val_open ([],[]) txt;

    17 

    18 fun ml_pat (lhs, pat) =

    19   let 

    20      val pat' = implode (map (fn "\\<dots>" => "_" | s => s) (Symbol.explode pat))

    21   in "val " ^ pat' ^ " = " ^ lhs end;

    22 

    23 fun ml_struct txt = "functor DUMMY_FUNCTOR() = struct structure DUMMY = " ^ txt ^ " end";

    24 fun ml_type txt = "val _ = NONE : (" ^ txt ^ ") option";

    25 

    26 (* eval function *)

    27 fun eval_fn ctxt exp =

    28   ML_Context.eval_in (SOME ctxt) false Position.none exp

    29 

    30 (* string functions *)

    31 fun string_explode str txt =

    32   map (fn s => str ^ s) (space_explode "\n" txt)

    33 

    34 val transform_cmts_str =

    35      Source.of_string 

    36   #> ML_Lex.source 

    37   #> Source.exhaust 

    38   #> Chunks.transform_cmts 

    39   #> implode 

    40   #> string_explode "";

    41 

    42 (* output function *)

    43 fun output_fn txt =  Chunks.output (map Pretty.str txt)

    44 

    45 (* checks and prints open expressions *)

    46 fun output_ml {context = ctxt, ...} (txt, ovars) =

    47   (eval_fn ctxt (ml_val_open ovars txt);

    48    output_fn (transform_cmts_str txt))

    49 

    50 val parser_ml = Scan.lift (Args.name --

    51   (Scan.optional (Args.$$$ "for" |-- OuterParse.!!! (Scan.repeat1 Args.name)) [] --

    52    Scan.optional (Args.$$$ "in"  |-- OuterParse.!!! (Scan.repeat1 Args.name)) [])) 

    53 

    54 (* checks and prints types and structures *)

    55 fun output_exp ml {context = ctxt, ...} txt = 

    56   (eval_fn ctxt (ml txt);

    57    output_fn (string_explode "" txt))

    58 

    59 (* checks and expression agains a result pattern *)

    60 fun output_response {context = ctxt, ...} (lhs, pat) = 

    61     (eval_fn ctxt (ml_pat (lhs, pat));

    62      output_fn ((string_explode "" lhs) @ (string_explode "> " pat)))

    63 

    64 (* checks the expressions, but does not check it against a result pattern *)

    65 fun output_response_fake {context = ctxt, ...} (lhs, pat) = 

    66     (eval_fn ctxt (ml_val lhs);

    67      output_fn ((string_explode "" lhs) @ (string_explode "> " pat)))

    68 

    69 (* checks the expressions, but does not check it against a result pattern *)

    70 fun ouput_response_fake_both _ (lhs, pat) = 

    71     output_fn ((string_explode "" lhs) @ (string_explode "> " pat))

    72 

    73 val single_arg = Scan.lift (Args.name)

    74 val two_args   = Scan.lift (Args.name -- Args.name)

    75 

    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

    82 

    83 fun href_link txt =

    84 let 

    85   val raw = Symbol.encode_raw

    86   val path = "http://isabelle.in.tum.de/repos/isabelle/raw-file/tip/src/"    

    87 in

    88  (raw "\\href{") ^ (raw path) ^ (raw txt) ^ (raw "}{") ^ txt ^ (raw "}")

    89 end 

    90 

    91 (* checks whether a file exists in the Isabelle distribution *)

    92 fun check_file_exists _ txt =

    93   (if File.exists (Path.append (Path.explode ("~~/src")) (Path.explode txt)) 

    94    then output_fn [href_link txt]

    95    else error ("Source file " ^ (quote txt) ^ " does not exist."))

    96 

    97 val _ = ThyOutput.antiquotation "ML_file" single_arg check_file_exists

    98 

    99 

   100 (* replaces the official subgoal antiquotation with one *)

   101 (* that is closer to the actual output                  *)

   102 fun output_goals  {state = node, ...}  _ = 

   103 let

   104   fun subgoals 0 = ""

   105     | subgoals 1 = "goal (1 subgoal):"

   106     | subgoals n = "goal (" ^ string_of_int n ^ " subgoals):"

   107 

   108   fun proof_state state =

   109     (case try Toplevel.proof_of state of

   110       SOME prf => prf

   111     | _ => error "No proof state")

   112 

   113   val state = proof_state node;

   114   val goals = Proof.pretty_goals false state;

   115 

   116   val {prop, ...} = rep_thm (Proof.get_goal state |> snd |> snd);

   117   val (As, B) = Logic.strip_horn prop;

   118   val output  = (case (length As) of

   119                       0 => goals 

   120                     | n => (Pretty.str (subgoals n))::goals)  

   121 in 

   122   ThyOutput.output output

   123 end

   124 

   125 

   126 val _ = ThyOutput.antiquotation "subgoals" (Scan.succeed ()) output_goals

   127    

   128 end;