added GHC.read_source: read Haskell source text with antiquotations;
authorwenzelm
Tue Oct 30 22:05:30 2018 +0100 (6 months ago)
changeset 692117062639cfdaa
parent 69210 92fde8f61b0d
child 69212 be8c70794375
added GHC.read_source: read Haskell source text with antiquotations;
added "cartouche" antiquotation for ML string expressions as Haskell string literals;
NEWS
src/Pure/PIDE/markup.ML
src/Pure/Tools/ghc.ML
     1.1 --- a/NEWS	Tue Oct 30 19:25:32 2018 +0100
     1.2 +++ b/NEWS	Tue Oct 30 22:05:30 2018 +0100
     1.3 @@ -87,6 +87,22 @@
     1.4  potentially with variations on ML syntax (existing ML_Env.SML_operations
     1.5  observes the official standard).
     1.6  
     1.7 +* GHC.read_source reads Haskell source text with antiquotations (only
     1.8 +the control-cartouche form). The default "cartouche" antiquotation
     1.9 +evaluates an ML expression of type string and inlines the result as
    1.10 +Haskell string literal. This allows to refer to Isabelle items robustly,
    1.11 +e.g. via Isabelle/ML antiquotations or library operations. For example:
    1.12 +
    1.13 +ML \<open>
    1.14 +  GHC.read_source \<^context> \<open>
    1.15 +    allConst, impConst, eqConst :: String
    1.16 +    allConst = \<open>\<^const_name>\<open>Pure.all\<close>\<close>
    1.17 +    impConst = \<open>\<^const_name>\<open>Pure.imp\<close>\<close>
    1.18 +    eqConst = \<open>\<^const_name>\<open>Pure.eq\<close>\<close>
    1.19 +  \<close>
    1.20 +  |> File.write \<^path>\<open>consts.hs\<close>
    1.21 +\<close>
    1.22 +
    1.23  
    1.24  *** System ***
    1.25  
     2.1 --- a/src/Pure/PIDE/markup.ML	Tue Oct 30 19:25:32 2018 +0100
     2.2 +++ b/src/Pure/PIDE/markup.ML	Tue Oct 30 22:05:30 2018 +0100
     2.3 @@ -31,6 +31,7 @@
     2.4    val language_prop: bool -> T
     2.5    val language_ML: bool -> T
     2.6    val language_SML: bool -> T
     2.7 +  val language_haskell: bool -> T
     2.8    val language_document: bool -> T
     2.9    val language_antiquotation: T
    2.10    val language_text: bool -> T
    2.11 @@ -118,6 +119,7 @@
    2.12    val antiquotedN: string val antiquoted: T
    2.13    val antiquoteN: string val antiquote: T
    2.14    val ML_antiquotationN: string
    2.15 +  val haskell_antiquotationN: string
    2.16    val document_antiquotationN: string
    2.17    val document_antiquotation_optionN: string
    2.18    val paragraphN: string val paragraph: T
    2.19 @@ -302,6 +304,7 @@
    2.20  val language_prop = language' {name = "prop", symbols = true, antiquotes = false};
    2.21  val language_ML = language' {name = "ML", symbols = false, antiquotes = true};
    2.22  val language_SML = language' {name = "SML", symbols = false, antiquotes = false};
    2.23 +val language_haskell = language' {name = "Haskell", symbols = false, antiquotes = true};
    2.24  val language_document = language' {name = "document", symbols = false, antiquotes = true};
    2.25  val language_antiquotation =
    2.26    language {name = "antiquotation", symbols = true, antiquotes = false, delimited = true};
    2.27 @@ -477,6 +480,7 @@
    2.28  val (antiquoteN, antiquote) = markup_elem "antiquote";
    2.29  
    2.30  val ML_antiquotationN = "ML_antiquotation";
    2.31 +val haskell_antiquotationN = "Haskell_antiquotation";
    2.32  val document_antiquotationN = "document_antiquotation";
    2.33  val document_antiquotation_optionN = "document_antiquotation_option";
    2.34  
     3.1 --- a/src/Pure/Tools/ghc.ML	Tue Oct 30 19:25:32 2018 +0100
     3.2 +++ b/src/Pure/Tools/ghc.ML	Tue Oct 30 22:05:30 2018 +0100
     3.3 @@ -9,6 +9,10 @@
     3.4    val print_codepoint: UTF8.codepoint -> string
     3.5    val print_symbol: Symbol.symbol -> string
     3.6    val print_string: string -> string
     3.7 +  val antiquotation: binding -> 'a Token.context_parser ->
     3.8 +    ({context: Proof.context, source: Token.src, argument: 'a} -> string) -> theory -> theory
     3.9 +  val read_source: Proof.context -> Input.source -> string
    3.10 +  val set_result: string -> Proof.context -> Proof.context
    3.11  end;
    3.12  
    3.13  structure GHC: GHC =
    3.14 @@ -42,4 +46,82 @@
    3.15  
    3.16  val print_string = quote o implode o map print_symbol o Symbol.explode;
    3.17  
    3.18 +
    3.19 +(** antiquotations **)
    3.20 +
    3.21 +(* theory data *)
    3.22 +
    3.23 +structure Antiqs = Theory_Data
    3.24 +(
    3.25 +  type T = (Token.src -> Proof.context -> string) Name_Space.table;
    3.26 +  val empty : T = Name_Space.empty_table Markup.haskell_antiquotationN;
    3.27 +  val extend = I;
    3.28 +  fun merge tabs : T = Name_Space.merge_tables tabs;
    3.29 +);
    3.30 +
    3.31 +val get_antiquotations = Antiqs.get o Proof_Context.theory_of;
    3.32 +
    3.33 +fun antiquotation name scan body thy =
    3.34 +  let
    3.35 +    fun antiq src ctxt =
    3.36 +      let val (x, ctxt') = Token.syntax scan src ctxt
    3.37 +      in body {context = ctxt', source = src, argument = x} end;
    3.38 +  in thy |> Antiqs.map (Name_Space.define (Context.Theory thy) true (name, antiq) #> #2) end;
    3.39 +
    3.40 +
    3.41 +(* read source and expand antiquotations *)
    3.42 +
    3.43 +val scan_antiq =
    3.44 +  Antiquote.scan_control >> Antiquote.Control ||
    3.45 +  Scan.one (Symbol.not_eof o Symbol_Pos.symbol) >> (Antiquote.Text o Symbol_Pos.symbol);
    3.46 +
    3.47 +fun read_source ctxt source =
    3.48 +  let
    3.49 +    val _ =
    3.50 +      Context_Position.report ctxt (Input.pos_of source)
    3.51 +        (Markup.language_haskell (Input.is_delimited source));
    3.52 +
    3.53 +    val (input, _) =
    3.54 +      Input.source_explode source
    3.55 +      |> Scan.error (Scan.finite Symbol_Pos.stopper (Scan.repeat scan_antiq));
    3.56 +
    3.57 +    val _ = Context_Position.reports ctxt (Antiquote.antiq_reports input);
    3.58 +
    3.59 +    fun expand antiq =
    3.60 +      (case antiq of
    3.61 +        Antiquote.Text s => s
    3.62 +      | Antiquote.Control {name, body, ...} =>
    3.63 +          let
    3.64 +            val src = Token.make_src name (if null body then [] else [Token.read_cartouche body]);
    3.65 +            val (src', f) = Token.check_src ctxt get_antiquotations src;
    3.66 +          in f src' ctxt end
    3.67 +      | Antiquote.Antiq antiq => error ("Bad antiquotation " ^ Position.here (#1 (#range antiq))));
    3.68 +  in implode (map expand input) end;
    3.69 +
    3.70 +
    3.71 +(* concrete antiquotation: ML expression as Haskell string literal *)
    3.72 +
    3.73 +structure Local_Data = Proof_Data
    3.74 +(
    3.75 +  type T = string option;
    3.76 +  fun init _ = NONE;
    3.77 +);
    3.78 +
    3.79 +val set_result = Local_Data.put o SOME;
    3.80 +
    3.81 +fun the_result ctxt =
    3.82 +  (case Local_Data.get ctxt of
    3.83 +    SOME s => s
    3.84 +  | NONE => raise Fail "No result");
    3.85 +
    3.86 +val _ =
    3.87 +  Theory.setup
    3.88 +    (antiquotation \<^binding>\<open>cartouche\<close> (Scan.lift Args.cartouche_input)
    3.89 +      (fn {context = ctxt, argument, ...} =>
    3.90 +        ctxt |> Context.proof_map
    3.91 +          (ML_Context.expression ("result", Position.thread_data ())
    3.92 +            "string" "Context.map_proof (GHC.set_result result)"
    3.93 +            (ML_Lex.read_source argument))
    3.94 +        |> the_result |> print_string));
    3.95 +
    3.96  end;