Enable keyword 'structure' in for clause of locale expression.
authorballarin
Wed Dec 10 10:11:18 2008 +0100 (2008-12-10)
changeset 29033721529248e31
parent 29021 ce100fbc3c8e
child 29034 3dc51c01f9f3
Enable keyword 'structure' in for clause of locale expression.
src/FOL/ex/NewLocaleSetup.thy
src/Pure/Isar/expression.ML
src/Pure/Isar/isar_syn.ML
src/Pure/Isar/spec_parse.ML
     1.1 --- a/src/FOL/ex/NewLocaleSetup.thy	Mon Dec 08 18:44:24 2008 +0100
     1.2 +++ b/src/FOL/ex/NewLocaleSetup.thy	Wed Dec 10 10:11:18 2008 +0100
     1.3 @@ -16,7 +16,7 @@
     1.4  val opt_bang = Scan.optional (P.$$$ "!" >> K true) false;
     1.5  
     1.6  val locale_val =
     1.7 -  Expression.parse_expression --
     1.8 +  SpecParse.locale_expression --
     1.9      Scan.optional (P.$$$ "+" |-- P.!!! (Scan.repeat1 SpecParse.context_element)) [] ||
    1.10    Scan.repeat1 SpecParse.context_element >> pair ([], []);
    1.11  
    1.12 @@ -42,7 +42,7 @@
    1.13  val _ =
    1.14    OuterSyntax.command "interpretation"
    1.15      "prove interpretation of locale expression in theory" K.thy_goal
    1.16 -    (P.!!! Expression.parse_expression
    1.17 +    (P.!!! SpecParse.locale_expression
    1.18          >> (fn expr => Toplevel.print o
    1.19              Toplevel.theory_to_proof (Expression.interpretation_cmd expr)));
    1.20  
    1.21 @@ -50,7 +50,7 @@
    1.22    OuterSyntax.command "interpret"
    1.23      "prove interpretation of locale expression in proof context"
    1.24      (K.tag_proof K.prf_goal)
    1.25 -    (P.!!! Expression.parse_expression
    1.26 +    (P.!!! SpecParse.locale_expression
    1.27          >> (fn expr => Toplevel.print o
    1.28              Toplevel.proof' (fn int => Expression.interpret_cmd expr int)));
    1.29  
     2.1 --- a/src/Pure/Isar/expression.ML	Mon Dec 08 18:44:24 2008 +0100
     2.2 +++ b/src/Pure/Isar/expression.ML	Wed Dec 10 10:11:18 2008 +0100
     2.3 @@ -30,10 +30,6 @@
     2.4    val interpretation: expression_i -> theory -> Proof.state;
     2.5    val interpret_cmd: expression -> bool -> Proof.state -> Proof.state;
     2.6    val interpret: expression_i -> bool -> Proof.state -> Proof.state;
     2.7 -
     2.8 -  (* Debugging and development *)
     2.9 -  val parse_expression: OuterParse.token list -> expression * OuterParse.token list
    2.10 -    (* FIXME to spec_parse.ML *)
    2.11  end;
    2.12  
    2.13  
    2.14 @@ -55,63 +51,6 @@
    2.15  type expression_i = term expr * (Binding.T * typ option * mixfix) list;
    2.16  
    2.17  
    2.18 -(** Parsing and printing **)
    2.19 -
    2.20 -local
    2.21 -
    2.22 -structure P = OuterParse;
    2.23 -
    2.24 -val loc_keyword = P.$$$ "fixes" || P.$$$ "constrains" || P.$$$ "assumes" ||
    2.25 -   P.$$$ "defines" || P.$$$ "notes";
    2.26 -fun plus1_unless test scan =
    2.27 -  scan ::: Scan.repeat (P.$$$ "+" |-- Scan.unless test (P.!!! scan));
    2.28 -
    2.29 -val prefix = P.name --| P.$$$ ":";
    2.30 -val named = P.name -- (P.$$$ "=" |-- P.term);
    2.31 -val position = P.maybe P.term;
    2.32 -val instance = P.$$$ "where" |-- P.and_list1 named >> Named ||
    2.33 -  Scan.repeat1 position >> Positional;
    2.34 -
    2.35 -in
    2.36 -
    2.37 -val parse_expression =
    2.38 -  let
    2.39 -    fun expr2 x = P.xname x;
    2.40 -    fun expr1 x = (Scan.optional prefix "" -- expr2 --
    2.41 -      Scan.optional instance (Named []) >> (fn ((p, l), i) => (l, (p, i)))) x;
    2.42 -    fun expr0 x = (plus1_unless loc_keyword expr1) x;
    2.43 -  in expr0 -- P.for_fixes end;
    2.44 -
    2.45 -end;
    2.46 -
    2.47 -fun pretty_expr thy expr =
    2.48 -  let
    2.49 -    fun pretty_pos NONE = Pretty.str "_"
    2.50 -      | pretty_pos (SOME x) = Pretty.str x;
    2.51 -    fun pretty_named (x, y) = [Pretty.str x, Pretty.brk 1, Pretty.str "=",
    2.52 -          Pretty.brk 1, Pretty.str y] |> Pretty.block;
    2.53 -    fun pretty_ren (Positional ps) = take_suffix is_none ps |> snd |>
    2.54 -          map pretty_pos |> Pretty.breaks
    2.55 -      | pretty_ren (Named []) = []
    2.56 -      | pretty_ren (Named ps) = Pretty.str "where" :: Pretty.brk 1 ::
    2.57 -          (ps |> map pretty_named |> Pretty.separate "and");
    2.58 -    fun pretty_rename (loc, ("", ren)) =
    2.59 -          Pretty.block (Pretty.str (NewLocale.extern thy loc) :: Pretty.brk 1 :: pretty_ren ren) 
    2.60 -      | pretty_rename (loc, (prfx, ren)) =
    2.61 -          Pretty.block (Pretty.str prfx :: Pretty.brk 1 :: Pretty.str (NewLocale.extern thy loc) ::
    2.62 -            Pretty.brk 1 :: pretty_ren ren);
    2.63 -  in Pretty.separate "+" (map pretty_rename expr) |> Pretty.block end;
    2.64 -
    2.65 -fun err_in_expr thy msg expr =
    2.66 -  let
    2.67 -    val err_msg =
    2.68 -      if null expr then msg
    2.69 -      else msg ^ "\n" ^ Pretty.string_of (Pretty.block
    2.70 -        [Pretty.str "The above error(s) occurred in expression:", Pretty.brk 1,
    2.71 -          pretty_expr thy expr])
    2.72 -  in error err_msg end;
    2.73 -
    2.74 -
    2.75  (** Internalise locale names in expr **)
    2.76  
    2.77  fun intern thy instances =  map (apfst (NewLocale.intern thy)) instances;
     3.1 --- a/src/Pure/Isar/isar_syn.ML	Mon Dec 08 18:44:24 2008 +0100
     3.2 +++ b/src/Pure/Isar/isar_syn.ML	Wed Dec 10 10:11:18 2008 +0100
     3.3 @@ -401,7 +401,7 @@
     3.4  val _ =
     3.5    OuterSyntax.command "sublocale"
     3.6      "prove sublocale relation between a locale and a locale expression" K.thy_goal
     3.7 -    (P.xname --| (P.$$$ "\\<subseteq>" || P.$$$ "<") -- P.!!! Expression.parse_expression
     3.8 +    (P.xname --| (P.$$$ "\\<subseteq>" || P.$$$ "<") -- P.!!! SpecParse.locale_expression
     3.9        >> (fn (loc, expr) =>
    3.10          Toplevel.print o (Toplevel.theory_to_proof (Expression.sublocale_cmd loc expr))));
    3.11  
     4.1 --- a/src/Pure/Isar/spec_parse.ML	Mon Dec 08 18:44:24 2008 +0100
     4.2 +++ b/src/Pure/Isar/spec_parse.ML	Wed Dec 10 10:11:18 2008 +0100
     4.3 @@ -26,6 +26,7 @@
     4.4    val locale_insts: token list -> (string option list * (Attrib.binding * string) list) * token list
     4.5    val class_expr: token list -> string list * token list
     4.6    val locale_expr: token list -> Locale.expr * token list
     4.7 +  val locale_expression: OuterParse.token list -> Expression.expression * OuterParse.token list
     4.8    val locale_keyword: token list -> string * token list
     4.9    val context_element: token list -> Element.context * token list
    4.10    val statement: token list -> (Attrib.binding * (string * string list) list) list * token list
    4.11 @@ -103,6 +104,12 @@
    4.12  
    4.13  val rename = P.name -- Scan.option P.mixfix;
    4.14  
    4.15 +val prefix = P.name --| P.$$$ ":";
    4.16 +val named = P.name -- (P.$$$ "=" |-- P.term);
    4.17 +val position = P.maybe P.term;
    4.18 +val instance = P.$$$ "where" |-- P.and_list1 named >> Expression.Named ||
    4.19 +  Scan.repeat1 position >> Expression.Positional;
    4.20 +
    4.21  in
    4.22  
    4.23  val locale_keyword = P.$$$ "fixes" || P.$$$ "constrains" || P.$$$ "assumes" ||
    4.24 @@ -117,6 +124,14 @@
    4.25      and expr0 x = (plus1_unless locale_keyword expr1 >> (fn [e] => e | es => Locale.Merge es)) x;
    4.26    in expr0 end;
    4.27  
    4.28 +val locale_expression =
    4.29 +  let
    4.30 +    fun expr2 x = P.xname x;
    4.31 +    fun expr1 x = (Scan.optional prefix "" -- expr2 --
    4.32 +      Scan.optional instance (Expression.Named []) >> (fn ((p, l), i) => (l, (p, i)))) x;
    4.33 +    fun expr0 x = (plus1_unless locale_keyword expr1) x;
    4.34 +  in expr0 -- Scan.optional (P.$$$ "for" |-- P.!!! locale_fixes) [] end;
    4.35 +
    4.36  val context_element = P.group "context element" loc_element;
    4.37  
    4.38  end;