--- a/src/Pure/Syntax/syntax.ML Sun Sep 16 20:33:37 2018 +0200
+++ b/src/Pure/Syntax/syntax.ML Sun Sep 16 22:45:34 2018 +0200
@@ -75,6 +75,7 @@
type syntax
val eq_syntax: syntax * syntax -> bool
val force_syntax: syntax -> unit
+ val get_infix: syntax -> string -> {assoc: Syntax_Ext.assoc, delim: string, pri: int} 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
@@ -418,6 +419,8 @@
fun force_syntax (Syntax ({gram, ...}, _)) = ignore (Lazy.force gram);
+fun get_infix (Syntax ({input, ...}, _)) c = Syntax_Ext.get_infix input c;
+
fun lookup_const (Syntax ({consts, ...}, _)) = Symtab.lookup consts;
fun is_keyword (Syntax ({lexicon, ...}, _)) = Scan.is_literal lexicon o Symbol.explode;
fun tokenize (Syntax ({lexicon, ...}, _)) = Lexicon.tokenize lexicon;
--- a/src/Pure/Syntax/syntax_ext.ML Sun Sep 16 20:33:37 2018 +0200
+++ b/src/Pure/Syntax/syntax_ext.ML Sun Sep 16 22:45:34 2018 +0200
@@ -20,6 +20,8 @@
datatype xprod = XProd of string * xsymb list * string * int
val chain_pri: int
val delims_of: xprod list -> string list list
+ datatype assoc = No_Assoc | Left_Assoc | Right_Assoc
+ val get_infix: xprod list -> string -> {assoc: assoc, delim: string, pri: int} option
datatype syn_ext =
Syn_Ext of {
xprods: xprod list,
@@ -111,6 +113,23 @@
|> map Symbol.explode;
+(* plain infix syntax *)
+
+datatype assoc = No_Assoc | Left_Assoc | Right_Assoc;
+
+fun get_infix xprods c =
+ xprods |> get_first (fn XProd (_, xsymbs, const, p) =>
+ if c = const then
+ (case xsymbs of
+ [Bg _, Argument (_, p1), Space _, Delim s, Brk _, Argument (_, p2), En] =>
+ if p1 = p + 1 andalso p2 = p + 1 then SOME {assoc = No_Assoc, delim = s, pri = p}
+ else if p1 = p andalso p2 = p + 1 then SOME {assoc = Left_Assoc, delim = s, pri = p}
+ else if p1 = p + 1 andalso p2 = p then SOME {assoc = Right_Assoc, delim = s, pri = p}
+ else NONE
+ | _ => NONE)
+ else NONE);
+
+
(** datatype mfix **)
--- a/src/Pure/Thy/export_theory.ML Sun Sep 16 20:33:37 2018 +0200
+++ b/src/Pure/Thy/export_theory.ML Sun Sep 16 22:45:34 2018 +0200
@@ -52,14 +52,14 @@
val parents = Theory.parents_of thy;
val rep_tsig = Type.rep_tsig (Sign.tsig_of thy);
- val ctxt = Proof_Context.init_global thy;
+ val thy_ctxt = Proof_Context.init_global thy;
(* entities *)
fun entity_markup space name =
let
- val xname = Name_Space.extern_shortest ctxt space name;
+ val xname = Name_Space.extern_shortest thy_ctxt space name;
val {serial, pos, ...} = Name_Space.the_entry space name;
val props =
Position.offset_properties_of (adjust_pos pos) @
@@ -86,35 +86,53 @@
in if null elems then () else export_body thy export_name elems end;
+ (* infix syntax *)
+
+ fun get_infix_const ctxt = Syntax.get_infix (Proof_Context.syn_of ctxt) o Lexicon.mark_const;
+ fun get_infix_type ctxt = Syntax.get_infix (Proof_Context.syn_of ctxt) o Lexicon.mark_type;
+
+ fun encode_infix {assoc, delim, pri} =
+ let
+ val ass =
+ (case assoc of
+ Syntax_Ext.No_Assoc => 0
+ | Syntax_Ext.Left_Assoc => 1
+ | Syntax_Ext.Right_Assoc => 2);
+ open XML.Encode Term_XML.Encode;
+ in triple int string int (ass, delim, pri) end;
+
+
(* types *)
val encode_type =
let open XML.Encode Term_XML.Encode
- in pair (list string) (option typ) end;
+ in triple (option encode_infix) (list string) (option typ) end;
- fun export_type (Type.LogicalType n) =
- SOME (encode_type (Name.invent Name.context Name.aT n, NONE))
- | export_type (Type.Abbreviation (args, U, false)) =
- SOME (encode_type (args, SOME U))
- | export_type _ = NONE;
+ fun export_type c (Type.LogicalType n) =
+ SOME (encode_type (get_infix_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))
+ | export_type _ _ = NONE;
val _ =
- export_entities "types" (K export_type) Sign.type_space
+ export_entities "types" export_type Sign.type_space
(Name_Space.dest_table (#types rep_tsig));
(* consts *)
val encode_const =
- let open XML.Encode Term_XML.Encode
- in triple (list string) typ (option (term o named_bounds)) end;
+ let open XML.Encode Term_XML.Encode in
+ pair (option encode_infix) (pair (list string) (pair typ (option (term o named_bounds))))
+ end;
fun export_const c (T, abbrev) =
let
+ val syntax = get_infix_const thy_ctxt c;
val T' = T |> Logic.unvarifyT_global |> Type.strip_sorts;
val abbrev' = abbrev |> Option.map (Logic.unvarify_global #> map_types Type.strip_sorts);
val args = map (#1 o dest_TFree) (Consts.typargs (Sign.consts_of thy) (c, T'));
- in SOME (encode_const (args, T', abbrev')) end;
+ in SOME (encode_const (syntax, (args, (T', abbrev')))) end;
val _ =
export_entities "consts" export_const Sign.const_space
--- a/src/Pure/Thy/export_theory.scala Sun Sep 16 20:33:37 2018 +0200
+++ b/src/Pure/Thy/export_theory.scala Sun Sep 16 22:45:34 2018 +0200
@@ -190,12 +190,31 @@
}
+ /* infix syntax */
+
+ object Assoc extends Enumeration
+ {
+ val NO_ASSOC, LEFT_ASSOC, RIGHT_ASSOC = Value
+ }
+
+ sealed case class Infix(assoc: Assoc.Value, delim: String, pri: Int)
+
+ def decode_infix(body: XML.Body): Infix =
+ {
+ import XML.Decode._
+ val (ass, delim, pri) = triple(int, string, int)(body)
+ Infix(Assoc(ass), delim, pri)
+ }
+
+
/* types */
- sealed case class Type(entity: Entity, args: List[String], abbrev: Option[Term.Typ])
+ sealed case class Type(
+ entity: Entity, syntax: Option[Infix], args: List[String], abbrev: Option[Term.Typ])
{
def cache(cache: Term.Cache): Type =
Type(entity.cache(cache),
+ syntax,
args.map(cache.string(_)),
abbrev.map(cache.typ(_)))
}
@@ -204,22 +223,27 @@
provider.uncompressed_yxml(export_prefix + "types").map((tree: XML.Tree) =>
{
val (entity, body) = decode_entity(Kind.TYPE, tree)
- val (args, abbrev) =
+ val (syntax, args, abbrev) =
{
import XML.Decode._
- pair(list(string), option(Term_XML.Decode.typ))(body)
+ triple(option(decode_infix), list(string), option(Term_XML.Decode.typ))(body)
}
- Type(entity, args, abbrev)
+ Type(entity, syntax, args, abbrev)
})
/* consts */
sealed case class Const(
- entity: Entity, typargs: List[String], typ: Term.Typ, abbrev: Option[Term.Term])
+ entity: Entity,
+ syntax: Option[Infix],
+ typargs: List[String],
+ typ: Term.Typ,
+ abbrev: Option[Term.Term])
{
def cache(cache: Term.Cache): Const =
Const(entity.cache(cache),
+ syntax,
typargs.map(cache.string(_)),
cache.typ(typ),
abbrev.map(cache.term(_)))
@@ -229,12 +253,13 @@
provider.uncompressed_yxml(export_prefix + "consts").map((tree: XML.Tree) =>
{
val (entity, body) = decode_entity(Kind.CONST, tree)
- val (args, typ, abbrev) =
+ val (syntax, (args, (typ, abbrev))) =
{
import XML.Decode._
- triple(list(string), Term_XML.Decode.typ, option(Term_XML.Decode.term))(body)
+ pair(option(decode_infix), pair(list(string),
+ pair(Term_XML.Decode.typ, option(Term_XML.Decode.term))))(body)
}
- Const(entity, args, typ, abbrev)
+ Const(entity, syntax, args, typ, abbrev)
})