--- a/src/Pure/Syntax/printer.ML Fri Sep 28 19:30:07 2018 +0200
+++ b/src/Pure/Syntax/printer.ML Fri Sep 28 21:16:24 2018 +0200
@@ -30,6 +30,7 @@
type prtabs
datatype assoc = No_Assoc | Left_Assoc | Right_Assoc
val get_infix: prtabs -> string -> {assoc: assoc, delim: string, pri: int} option
+ val get_prefix: prtabs -> Symtab.key -> string option
val empty_prtabs: prtabs
val update_prtabs: string -> Syntax_Ext.xprod list -> prtabs -> prtabs
val remove_prtabs: string -> Syntax_Ext.xprod list -> prtabs -> prtabs
@@ -96,20 +97,35 @@
fun mode_tabs (prtabs: prtabs) modes = map_filter (AList.lookup (op =) prtabs) (modes @ [""]);
-(* plain infix syntax *)
+(* approximative syntax *)
datatype assoc = No_Assoc | Left_Assoc | Right_Assoc;
+local
+
+fun is_arg (Arg _) = true
+ | is_arg (TypArg _) = true
+ | is_arg _ = false;
+
fun is_space str = forall_string (fn s => s = " ") str;
+val is_delim = not o is_space;
+
+fun is_delimiter (String (_, d)) = is_delim d
+ | is_delimiter _ = false;
+
+fun flatten (Block (_, symbs)) = maps flatten symbs
+ | flatten symb = [symb];
+
+in
fun get_infix prtabs c =
Symtab.lookup_list (mode_tab prtabs "") c
|> map_filter (fn (symbs, _, p) =>
(case symbs of
[Block (_, [Arg p1, String (_, s), String (_, d), Break _, Arg p2])] =>
- if is_space s andalso not (is_space d) then SOME (p1, p2, d, p) else NONE
+ if is_space s andalso is_delim d then SOME (p1, p2, d, p) else NONE
| [Block (_, [TypArg p1, String (_, s), String (_, d), Break _, TypArg p2])] =>
- if is_space s andalso not (is_space d) then SOME (p1, p2, d, p) else NONE
+ if is_space s andalso is_delim d then SOME (p1, p2, d, p) else NONE
| _ => NONE))
|> get_first (fn (p1, p2, d, p) =>
if p1 = p + 1 andalso p2 = p + 1 then SOME {assoc = No_Assoc, delim = d, pri = p}
@@ -117,6 +133,15 @@
else if p1 = p + 1 andalso p2 = p then SOME {assoc = Right_Assoc, delim = d, pri = p}
else NONE);
+fun get_prefix prtabs c =
+ Symtab.lookup_list (mode_tab prtabs "") c
+ |> get_first (fn (symbs, _, _) =>
+ (case filter (is_arg orf is_delimiter) (maps flatten symbs) of
+ String (_, d) :: _ => SOME d
+ | _ => NONE));
+
+end;
+
(* xprod_to_fmt *)
--- a/src/Pure/Syntax/syntax.ML Fri Sep 28 19:30:07 2018 +0200
+++ b/src/Pure/Syntax/syntax.ML Fri Sep 28 21:16:24 2018 +0200
@@ -75,7 +75,8 @@
type syntax
val eq_syntax: syntax * syntax -> bool
val force_syntax: syntax -> unit
- val get_infix: syntax -> string -> {assoc: Printer.assoc, delim: string, pri: int} option
+ datatype approx = Prefix of string | Infix of {assoc: Printer.assoc, delim: string, pri: int}
+ val get_approx: syntax -> string -> approx option
val lookup_const: syntax -> string -> string option
val is_keyword: syntax -> string -> bool
val tokenize: syntax -> bool -> Symbol_Pos.T list -> Lexicon.token list
@@ -419,7 +420,15 @@
fun force_syntax (Syntax ({gram, ...}, _)) = ignore (Lazy.force gram);
-fun get_infix (Syntax ({prtabs, ...}, _)) c = Printer.get_infix prtabs c;
+datatype approx = Prefix of string | Infix of {assoc: Printer.assoc, delim: string, pri: int};
+fun get_approx (Syntax ({prtabs, ...}, _)) c =
+ (case Printer.get_infix prtabs c of
+ SOME infx => SOME (Infix infx)
+ | NONE =>
+ (case Printer.get_prefix prtabs c of
+ SOME prfx => SOME prfx
+ | NONE => Printer.get_prefix prtabs (Mixfix.binder_name c))
+ |> Option.map Prefix);
fun lookup_const (Syntax ({consts, ...}, _)) = Symtab.lookup consts;
fun is_keyword (Syntax ({lexicon, ...}, _)) = Scan.is_literal lexicon o Symbol.explode;
--- a/src/Pure/Thy/export_theory.ML Fri Sep 28 19:30:07 2018 +0200
+++ b/src/Pure/Thy/export_theory.ML Fri Sep 28 21:16:24 2018 +0200
@@ -13,30 +13,35 @@
structure Export_Theory: EXPORT_THEORY =
struct
-(* infix syntax *)
+(* approximative syntax *)
-fun get_infix_type ctxt = Syntax.get_infix (Proof_Context.syn_of ctxt) o Lexicon.mark_type;
-fun get_infix_const ctxt = Syntax.get_infix (Proof_Context.syn_of ctxt) o Lexicon.mark_const;
-fun get_infix_fixed ctxt = Syntax.get_infix (Proof_Context.syn_of ctxt) o Lexicon.mark_fixed;
+val get_syntax = Syntax.get_approx o Proof_Context.syn_of;
+fun get_syntax_type ctxt = get_syntax ctxt o Lexicon.mark_type;
+fun get_syntax_const ctxt = get_syntax ctxt o Lexicon.mark_const;
+fun get_syntax_fixed ctxt = get_syntax ctxt o Lexicon.mark_fixed;
-fun get_infix_param ctxt loc x =
+fun get_syntax_param ctxt loc x =
let val thy = Proof_Context.theory_of ctxt in
if Class.is_class thy loc then
(case AList.lookup (op =) (Class.these_params thy [loc]) x of
NONE => NONE
- | SOME (_, (c, _)) => get_infix_const ctxt c)
- else get_infix_fixed ctxt x
+ | SOME (_, (c, _)) => get_syntax_const ctxt c)
+ else get_syntax_fixed ctxt x
end;
-fun encode_infix {assoc, delim, pri} =
- let
- val ass =
- (case assoc of
- Printer.No_Assoc => 0
- | Printer.Left_Assoc => 1
- | Printer.Right_Assoc => 2);
- open XML.Encode Term_XML.Encode;
- in triple int string int (ass, delim, pri) end;
+val encode_syntax =
+ XML.Encode.variant
+ [fn NONE => ([], []),
+ fn SOME (Syntax.Prefix delim) => ([delim], []),
+ fn SOME (Syntax.Infix {assoc, delim, pri}) =>
+ let
+ val ass =
+ (case assoc of
+ Printer.No_Assoc => 0
+ | Printer.Left_Assoc => 1
+ | Printer.Right_Assoc => 2);
+ open XML.Encode Term_XML.Encode;
+ in ([], triple int string int (ass, delim, pri)) end];
(* standardization of variables: only frees and named bounds *)
@@ -102,7 +107,7 @@
let
val loc_ctxt = Locale.init loc thy;
val args = Locale.params_of thy loc
- |> map (fn ((x, T), _) => ((x, T), get_infix_param loc_ctxt loc x));
+ |> map (fn ((x, T), _) => ((x, T), get_syntax_param loc_ctxt loc x));
val axioms =
let
val (intro1, intro2) = Locale.intros_of thy loc;
@@ -201,12 +206,12 @@
val encode_type =
let open XML.Encode Term_XML.Encode
- in triple (option encode_infix) (list string) (option typ) end;
+ in triple encode_syntax (list string) (option typ) end;
fun export_type c (Type.LogicalType n) =
- SOME (encode_type (get_infix_type thy_ctxt c, Name.invent Name.context Name.aT n, NONE))
+ SOME (encode_type (get_syntax_type thy_ctxt c, Name.invent Name.context Name.aT n, NONE))
| export_type c (Type.Abbreviation (args, U, false)) =
- SOME (encode_type (get_infix_type thy_ctxt c, args, SOME U))
+ SOME (encode_type (get_syntax_type thy_ctxt c, args, SOME U))
| export_type _ _ = NONE;
val _ =
@@ -218,11 +223,11 @@
val encode_const =
let open XML.Encode Term_XML.Encode
- in pair (option encode_infix) (pair (list string) (pair typ (option term))) end;
+ in pair encode_syntax (pair (list string) (pair typ (option term))) end;
fun export_const c (T, abbrev) =
let
- val syntax = get_infix_const thy_ctxt c;
+ val syntax = get_syntax_const thy_ctxt c;
val T' = T |> Logic.unvarifyT_global |> Type.strip_sorts;
val abbrev' = abbrev |> Option.map (standard_vars_global #> map_types Type.strip_sorts);
val args = map (#1 o dest_TFree) (Consts.typargs (Sign.consts_of thy) (c, T'));
@@ -311,7 +316,7 @@
fun encode_locale used =
let open XML.Encode Term_XML.Encode in
- triple (list (pair string sort)) (list (pair (pair string typ) (option encode_infix)))
+ triple (list (pair string sort)) (list (pair (pair string typ) encode_syntax))
(list (encode_axiom used))
end;
--- a/src/Pure/Thy/export_theory.scala Fri Sep 28 19:30:07 2018 +0200
+++ b/src/Pure/Thy/export_theory.scala Fri Sep 28 21:16:24 2018 +0200
@@ -197,27 +197,32 @@
}
- /* infix syntax */
+ /* approximative syntax */
object Assoc extends Enumeration
{
val NO_ASSOC, LEFT_ASSOC, RIGHT_ASSOC = Value
}
- sealed case class Infix(assoc: Assoc.Value, delim: String, pri: Int)
+ sealed abstract class Syntax
+ case object No_Syntax extends Syntax
+ case class Prefix(delim: String) extends Syntax
+ case class Infix(assoc: Assoc.Value, delim: String, pri: Int) extends Syntax
- def decode_infix(body: XML.Body): Infix =
- {
- import XML.Decode._
- val (ass, delim, pri) = triple(int, string, int)(body)
- Infix(Assoc(ass), delim, pri)
- }
+ def decode_syntax: XML.Decode.T[Syntax] =
+ XML.Decode.variant(List(
+ { case (Nil, Nil) => No_Syntax },
+ { case (List(delim), Nil) => Prefix(delim) },
+ { case (Nil, body) =>
+ import XML.Decode._
+ val (ass, delim, pri) = triple(int, string, int)(body)
+ Infix(Assoc(ass), delim, pri) }))
/* types */
sealed case class Type(
- entity: Entity, syntax: Option[Infix], args: List[String], abbrev: Option[Term.Typ])
+ entity: Entity, syntax: Syntax, args: List[String], abbrev: Option[Term.Typ])
{
def cache(cache: Term.Cache): Type =
Type(entity.cache(cache),
@@ -233,7 +238,7 @@
val (syntax, args, abbrev) =
{
import XML.Decode._
- triple(option(decode_infix), list(string), option(Term_XML.Decode.typ))(body)
+ triple(decode_syntax, list(string), option(Term_XML.Decode.typ))(body)
}
Type(entity, syntax, args, abbrev)
})
@@ -243,7 +248,7 @@
sealed case class Const(
entity: Entity,
- syntax: Option[Infix],
+ syntax: Syntax,
typargs: List[String],
typ: Term.Typ,
abbrev: Option[Term.Term])
@@ -263,7 +268,7 @@
val (syntax, (args, (typ, abbrev))) =
{
import XML.Decode._
- pair(option(decode_infix), pair(list(string),
+ pair(decode_syntax, pair(list(string),
pair(Term_XML.Decode.typ, option(Term_XML.Decode.term))))(body)
}
Const(entity, syntax, args, typ, abbrev)
@@ -362,7 +367,7 @@
sealed case class Locale(
entity: Entity,
typargs: List[(String, Term.Sort)],
- args: List[((String, Term.Typ), Option[Infix])],
+ args: List[((String, Term.Typ), Syntax)],
axioms: List[Prop])
{
def cache(cache: Term.Cache): Locale =
@@ -380,7 +385,7 @@
{
import XML.Decode._
import Term_XML.Decode._
- triple(list(pair(string, sort)), list(pair(pair(string, typ), option(decode_infix))),
+ triple(list(pair(string, sort)), list(pair(pair(string, typ), decode_syntax)),
list(decode_prop))(body)
}
Locale(entity, typargs, args, axioms)