uniform handling of fixes;
authorwenzelm
Fri Jan 13 01:13:08 2006 +0100 (2006-01-13)
changeset 18669cd6d6baf0411
parent 18668 4a15c09bd46a
child 18670 c3f445b92aff
uniform handling of fixes;
mixfix: added Structure;
src/Pure/Isar/element.ML
src/Pure/Isar/outer_parse.ML
     1.1 --- a/src/Pure/Isar/element.ML	Fri Jan 13 01:13:06 2006 +0100
     1.2 +++ b/src/Pure/Isar/element.ML	Fri Jan 13 01:13:08 2006 +0100
     1.3 @@ -8,7 +8,7 @@
     1.4  signature ELEMENT =
     1.5  sig
     1.6    datatype ('typ, 'term, 'fact) ctxt =
     1.7 -    Fixes of (string * 'typ option * mixfix option) list |
     1.8 +    Fixes of (string * 'typ option * mixfix) list |
     1.9      Constrains of (string * 'typ) list |
    1.10      Assumes of ((string * Attrib.src list) * ('term * ('term list * 'term list)) list) list |
    1.11      Defines of ((string * Attrib.src list) * ('term * 'term list)) list |
    1.12 @@ -16,14 +16,13 @@
    1.13    type context (*= (string, string, thmref) ctxt*)
    1.14    type context_i (*= (typ, term, thm list) ctxt*)
    1.15    val map_ctxt: {name: string -> string,
    1.16 -    var: string * mixfix option -> string * mixfix option,
    1.17 +    var: string * mixfix -> string * mixfix,
    1.18      typ: 'typ -> 'a, term: 'term -> 'b, fact: 'fact -> 'c,
    1.19      attrib: Attrib.src -> Attrib.src} -> ('typ, 'term, 'fact) ctxt -> ('a, 'b, 'c) ctxt
    1.20    val map_ctxt_values: (typ -> typ) -> (term -> term) -> (thm -> thm) -> context_i -> context_i
    1.21    val pretty_ctxt: ProofContext.context -> context_i -> Pretty.T list
    1.22    val rename: (string * (string * mixfix option)) list -> string -> string
    1.23 -  val rename_var: (string * (string * mixfix option)) list ->
    1.24 -   string * mixfix option -> string * mixfix option
    1.25 +  val rename_var: (string * (string * mixfix option)) list -> string * mixfix -> string * mixfix
    1.26    val rename_term: (string * (string * mixfix option)) list -> term -> term
    1.27    val rename_thm: (string * (string * mixfix option)) list -> thm -> thm
    1.28    val rename_ctxt: (string * (string * mixfix option)) list -> context_i -> context_i
    1.29 @@ -44,7 +43,7 @@
    1.30  (* datatype ctxt *)
    1.31  
    1.32  datatype ('typ, 'term, 'fact) ctxt =
    1.33 -  Fixes of (string * 'typ option * mixfix option) list |
    1.34 +  Fixes of (string * 'typ option * mixfix) list |
    1.35    Constrains of (string * 'typ) list |
    1.36    Assumes of ((string * Attrib.src list) * ('term * ('term list * 'term list)) list) list |
    1.37    Defines of ((string * Attrib.src list) * ('term * 'term list)) list |
    1.38 @@ -56,8 +55,7 @@
    1.39  fun map_ctxt {name, var, typ, term, fact, attrib} =
    1.40    fn Fixes fixes => Fixes (fixes |> map (fn (x, T, mx) =>
    1.41         let val (x', mx') = var (x, mx) in (x', Option.map typ T, mx') end))
    1.42 -   | Constrains xs => Constrains (xs |> map (fn (x, T) =>
    1.43 -       (#1 (var (x, SOME Syntax.NoSyn)), typ T)))
    1.44 +   | Constrains xs => Constrains (xs |> map (fn (x, T) => (#1 (var (x, NoSyn)), typ T)))
    1.45     | Assumes asms => Assumes (asms |> map (fn ((a, atts), propps) =>
    1.46        ((name a, map attrib atts), propps |> map (fn (t, (ps, qs)) =>
    1.47          (term t, (map term ps, map term qs))))))
    1.48 @@ -80,13 +78,13 @@
    1.49      val prt_thm = Pretty.backquote o ProofContext.pretty_thm ctxt;
    1.50      val prt_atts = Args.pretty_attribs ctxt;
    1.51  
    1.52 -    fun prt_syn syn =
    1.53 -      let val s = (case syn of NONE => "(structure)" | SOME mx => Syntax.string_of_mixfix mx)
    1.54 +    fun prt_mixfix mx =
    1.55 +      let val s = Syntax.string_of_mixfix mx
    1.56        in if s = "" then [] else [Pretty.brk 2, Pretty.str s] end;
    1.57 -    fun prt_fix (x, SOME T, syn) = Pretty.block (Pretty.str (x ^ " ::") :: Pretty.brk 1 ::
    1.58 -          prt_typ T :: Pretty.brk 1 :: prt_syn syn)
    1.59 -      | prt_fix (x, NONE, syn) = Pretty.block (Pretty.str x :: Pretty.brk 1 :: prt_syn syn);
    1.60 -    fun prt_constrain (x, T) = prt_fix (x, SOME T, SOME (Syntax.NoSyn));
    1.61 +    fun prt_fix (x, SOME T, mx) = Pretty.block (Pretty.str (x ^ " ::") :: Pretty.brk 1 ::
    1.62 +          prt_typ T :: Pretty.brk 1 :: prt_mixfix mx)
    1.63 +      | prt_fix (x, NONE, mx) = Pretty.block (Pretty.str x :: Pretty.brk 1 :: prt_mixfix mx);
    1.64 +    fun prt_constrain (x, T) = prt_fix (x, SOME T, NoSyn);
    1.65  
    1.66      fun prt_name name = Pretty.str (ProofContext.extern_thm ctxt name);
    1.67      fun prt_name_atts (name, atts) sep =
    1.68 @@ -156,13 +154,13 @@
    1.69    | SOME (x', _) => x');
    1.70  
    1.71  fun rename_var ren (x, mx) =
    1.72 -  (case (AList.lookup (op =) ren (x: string), is_some mx) of
    1.73 +  (case (AList.lookup (op =) ren (x: string), mx) of
    1.74      (NONE, _) => (x, mx)
    1.75 -  | (SOME (x', NONE), true) => (x', SOME Syntax.NoSyn)
    1.76 -  | (SOME (x', NONE), false) => (x', mx)
    1.77 -  | (SOME (x', SOME mx'), true) => (x', SOME mx')
    1.78 -  | (SOME (x', SOME _), false) =>
    1.79 -      error ("Attempt to change syntax of structure parameter " ^ quote x));
    1.80 +  | (SOME (x', NONE), Structure) => (x', mx)
    1.81 +  | (SOME (x', SOME _), Structure) =>
    1.82 +      error ("Attempt to change syntax of structure parameter " ^ quote x)
    1.83 +  | (SOME (x', NONE), _) => (x', NoSyn)
    1.84 +  | (SOME (x', SOME mx'), _) => (x', mx'));
    1.85  
    1.86  fun rename_term ren (Free (x, T)) = Free (rename ren x, T)
    1.87    | rename_term ren (t $ u) = rename_term ren t $ rename_term ren u
     2.1 --- a/src/Pure/Isar/outer_parse.ML	Fri Jan 13 01:13:06 2006 +0100
     2.2 +++ b/src/Pure/Isar/outer_parse.ML	Fri Jan 13 01:13:08 2006 +0100
     2.3 @@ -54,13 +54,14 @@
     2.4    val arity: token list -> (string list * string) * token list
     2.5    val type_args: token list -> string list * token list
     2.6    val typ: token list -> string * token list
     2.7 -  val opt_infix: token list -> Syntax.mixfix * token list
     2.8 -  val opt_mixfix: token list -> Syntax.mixfix * token list
     2.9 -  val opt_infix': token list -> Syntax.mixfix * token list
    2.10 -  val opt_mixfix': token list -> Syntax.mixfix * token list
    2.11 -  val mixfix': token list -> Syntax.mixfix * token list
    2.12 -  val const: token list -> (bstring * string * Syntax.mixfix) * token list
    2.13 -  val param: token list -> (bstring * string option * Syntax.mixfix) * token list
    2.14 +  val mixfix: token list -> mixfix * token list
    2.15 +  val opt_infix: token list -> mixfix * token list
    2.16 +  val opt_mixfix: token list -> mixfix * token list
    2.17 +  val opt_infix': token list -> mixfix * token list
    2.18 +  val opt_mixfix': token list -> mixfix * token list
    2.19 +  val const: token list -> (string * string * mixfix) * token list
    2.20 +  val fixes: token list -> (string * string option * mixfix) list * token list
    2.21 +  val simple_fixes: token list -> (string * string option) list * token list
    2.22    val term: token list -> string * token list
    2.23    val prop: token list -> string * token list
    2.24    val propp: token list -> (string * (string list * string list)) * token list
    2.25 @@ -78,6 +79,8 @@
    2.26    val xthms1: token list -> (thmref * Attrib.src list) list * token list
    2.27    val name_facts: token list ->
    2.28      ((bstring * Attrib.src list) * (thmref * Attrib.src list) list) list * token list
    2.29 +  val locale_mixfix: token list -> mixfix * token list
    2.30 +  val locale_fixes: token list -> (string * string option * mixfix) list * token list
    2.31    val locale_target: token list -> xstring * token list
    2.32    val opt_locale_target: token list -> xstring option * token list
    2.33    val locale_expr: token list -> Locale.expr * token list
    2.34 @@ -220,36 +223,40 @@
    2.35  
    2.36  (* mixfix annotations *)
    2.37  
    2.38 -val infx = $$$ "infix" |-- !!! (nat >> Syntax.Infix || string -- nat >> Syntax.InfixName);
    2.39 -val infxl = $$$ "infixl" |-- !!! (nat >> Syntax.Infixl || string -- nat >> Syntax.InfixlName);
    2.40 -val infxr = $$$ "infixr" |-- !!! (nat >> Syntax.Infixr || string -- nat >> Syntax.InfixrName);
    2.41 +val mfix = string --
    2.42 +  !!! (Scan.optional ($$$ "[" |-- !!! (list nat --| $$$ "]")) [] --
    2.43 +    Scan.optional nat Syntax.max_pri) >> (Mixfix o triple2);
    2.44 +
    2.45 +val infx = $$$ "infix" |-- !!! (nat >> Infix || string -- nat >> InfixName);
    2.46 +val infxl = $$$ "infixl" |-- !!! (nat >> Infixl || string -- nat >> InfixlName);
    2.47 +val infxr = $$$ "infixr" |-- !!! (nat >> Infixr || string -- nat >> InfixrName);
    2.48  
    2.49 -val binder =
    2.50 -  $$$ "binder" |--
    2.51 -    !!! (string -- ($$$ "[" |-- nat --| $$$ "]" -- nat || nat >> (fn n => (n, n))))
    2.52 -  >> (Syntax.Binder o triple2);
    2.53 +val binder = $$$ "binder" |--
    2.54 +  !!! (string -- ($$$ "[" |-- nat --| $$$ "]" -- nat || nat >> (fn n => (n, n))))
    2.55 +  >> (Binder o triple2);
    2.56 +
    2.57 +fun annotation guard fix = $$$ "(" |-- guard (fix --| $$$ ")");
    2.58 +fun opt_annotation guard fix = Scan.optional (annotation guard fix) NoSyn;
    2.59 +
    2.60 +val mixfix = annotation !!! (mfix || binder || infxl || infxr || infx);
    2.61 +val opt_infix = opt_annotation !!! (infxl || infxr || infx);
    2.62 +val opt_mixfix = opt_annotation !!! (mfix || binder || infxl || infxr || infx);
    2.63 +val opt_infix' = opt_annotation I (infxl || infxr || infx);
    2.64 +val opt_mixfix' = opt_annotation I (mfix || binder || infxl || infxr || infx);
    2.65  
    2.66  
    2.67 -val opt_pris = Scan.optional ($$$ "[" |-- !!! (list nat --| $$$ "]")) [];
    2.68 -
    2.69 -val mixfix =
    2.70 -  (string -- !!! (opt_pris -- Scan.optional nat Syntax.max_pri))
    2.71 -  >> (Syntax.Mixfix o triple2);
    2.72 -
    2.73 -fun fix_decl guard fix = $$$ "(" |-- guard (fix --| $$$ ")");
    2.74 -fun opt_fix guard fix = Scan.optional (fix_decl guard fix) Syntax.NoSyn;
    2.75 -
    2.76 -val opt_infix = opt_fix !!! (infxl || infxr || infx);
    2.77 -val opt_mixfix = opt_fix !!! (mixfix || binder || infxl || infxr || infx);
    2.78 -val opt_infix' = opt_fix I (infxl || infxr || infx);
    2.79 -val opt_mixfix' = opt_fix I (mixfix || binder || infxl || infxr || infx);
    2.80 -val mixfix' = fix_decl !!! (mixfix || binder || infxl || infxr || infx);
    2.81 -
    2.82 -
    2.83 -(* consts *)
    2.84 +(* fixes *)
    2.85  
    2.86  val const = name -- ($$$ "::" |-- !!! typ) -- opt_mixfix >> triple1;
    2.87 -val param = name -- Scan.option ($$$ "::" |-- !!! typ) -- opt_mixfix >> triple1;
    2.88 +
    2.89 +val params = Scan.repeat1 name -- Scan.option ($$$ "::" |-- !!! typ)
    2.90 +  >> (fn (xs, T) => map (rpair T) xs);
    2.91 +
    2.92 +val simple_fixes = and_list1 params >> List.concat;
    2.93 +
    2.94 +val fixes =
    2.95 +  and_list1 (name -- Scan.option ($$$ "::" |-- typ) -- mixfix >> (single o triple1) ||
    2.96 +    params >> map Syntax.no_syn) >> List.concat;
    2.97  
    2.98  
    2.99  (* terms *)
   2.100 @@ -329,15 +336,19 @@
   2.101  
   2.102  (* locale and context elements *)
   2.103  
   2.104 +val locale_mixfix = $$$ "(" -- $$$ "structure" -- !!! ($$$ ")") >> K Structure || mixfix;
   2.105 +
   2.106 +val locale_fixes =
   2.107 +  and_list1 (name -- Scan.option ($$$ "::" |-- typ) -- locale_mixfix >> (single o triple1) ||
   2.108 +    params >> map Syntax.no_syn) >> List.concat;
   2.109 +
   2.110  local
   2.111  
   2.112 -val loc_mixfix = $$$ "(" -- $$$ "structure" -- !!! ($$$ ")") >> K NONE || opt_mixfix >> SOME;
   2.113  val loc_keyword = $$$ "fixes" || $$$ "constrains" || $$$ "assumes" ||
   2.114     $$$ "defines" || $$$ "notes" || $$$ "includes";
   2.115  
   2.116  val loc_element =
   2.117 -  $$$ "fixes" |-- !!! (and_list1 (name -- Scan.option ($$$ "::" |-- typ) -- loc_mixfix
   2.118 -    >> triple1)) >> Element.Fixes ||
   2.119 +  $$$ "fixes" |-- !!! locale_fixes >> Element.Fixes ||
   2.120    $$$ "constrains" |-- !!! (and_list1 (name -- ($$$ "::" |-- typ)))
   2.121      >> Element.Constrains ||
   2.122    $$$ "assumes" |-- !!! (and_list1 (opt_thm_name ":" -- Scan.repeat1 propp))
   2.123 @@ -350,7 +361,7 @@
   2.124  fun plus1 scan =
   2.125    scan -- Scan.repeat ($$$ "+" |-- Scan.unless loc_keyword (!!! scan)) >> op ::;
   2.126  
   2.127 -val rename = name -- Scan.option mixfix';
   2.128 +val rename = name -- Scan.option mixfix;
   2.129  
   2.130  fun expr2 x = (xname >> Locale.Locale || $$$ "(" |-- !!! (expr0 --| $$$ ")")) x
   2.131  and expr1 x = (expr2 -- Scan.repeat1 (maybe rename) >> Locale.Rename || expr2) x