export plain infix syntax;
authorwenzelm
Sun Sep 16 22:45:34 2018 +0200 (13 months ago)
changeset 69003a015f1d3ba0c
parent 69002 f0d4b1db0ea0
child 69004 f6a0c8115e9c
child 69005 778434adc352
export plain infix syntax;
src/Pure/Syntax/syntax.ML
src/Pure/Syntax/syntax_ext.ML
src/Pure/Thy/export_theory.ML
src/Pure/Thy/export_theory.scala
     1.1 --- a/src/Pure/Syntax/syntax.ML	Sun Sep 16 20:33:37 2018 +0200
     1.2 +++ b/src/Pure/Syntax/syntax.ML	Sun Sep 16 22:45:34 2018 +0200
     1.3 @@ -75,6 +75,7 @@
     1.4    type syntax
     1.5    val eq_syntax: syntax * syntax -> bool
     1.6    val force_syntax: syntax -> unit
     1.7 +  val get_infix: syntax -> string -> {assoc: Syntax_Ext.assoc, delim: string, pri: int} option
     1.8    val lookup_const: syntax -> string -> string option
     1.9    val is_keyword: syntax -> string -> bool
    1.10    val tokenize: syntax -> bool -> Symbol_Pos.T list -> Lexicon.token list
    1.11 @@ -418,6 +419,8 @@
    1.12  
    1.13  fun force_syntax (Syntax ({gram, ...}, _)) = ignore (Lazy.force gram);
    1.14  
    1.15 +fun get_infix (Syntax ({input, ...}, _)) c = Syntax_Ext.get_infix input c;
    1.16 +
    1.17  fun lookup_const (Syntax ({consts, ...}, _)) = Symtab.lookup consts;
    1.18  fun is_keyword (Syntax ({lexicon, ...}, _)) = Scan.is_literal lexicon o Symbol.explode;
    1.19  fun tokenize (Syntax ({lexicon, ...}, _)) = Lexicon.tokenize lexicon;
     2.1 --- a/src/Pure/Syntax/syntax_ext.ML	Sun Sep 16 20:33:37 2018 +0200
     2.2 +++ b/src/Pure/Syntax/syntax_ext.ML	Sun Sep 16 22:45:34 2018 +0200
     2.3 @@ -20,6 +20,8 @@
     2.4    datatype xprod = XProd of string * xsymb list * string * int
     2.5    val chain_pri: int
     2.6    val delims_of: xprod list -> string list list
     2.7 +  datatype assoc = No_Assoc | Left_Assoc | Right_Assoc
     2.8 +  val get_infix: xprod list -> string -> {assoc: assoc, delim: string, pri: int} option
     2.9    datatype syn_ext =
    2.10      Syn_Ext of {
    2.11        xprods: xprod list,
    2.12 @@ -111,6 +113,23 @@
    2.13    |> map Symbol.explode;
    2.14  
    2.15  
    2.16 +(* plain infix syntax *)
    2.17 +
    2.18 +datatype assoc = No_Assoc | Left_Assoc | Right_Assoc;
    2.19 +
    2.20 +fun get_infix xprods c =
    2.21 +  xprods |> get_first (fn XProd (_, xsymbs, const, p) =>
    2.22 +    if c = const then
    2.23 +      (case xsymbs of
    2.24 +        [Bg _, Argument (_, p1), Space _, Delim s, Brk _, Argument (_, p2), En] =>
    2.25 +          if p1 = p + 1 andalso p2 = p + 1 then SOME {assoc = No_Assoc, delim = s, pri = p}
    2.26 +          else if p1 = p andalso p2 = p + 1 then SOME {assoc = Left_Assoc, delim = s, pri = p}
    2.27 +          else if p1 = p + 1 andalso p2 = p then SOME {assoc = Right_Assoc, delim = s, pri = p}
    2.28 +          else NONE
    2.29 +      | _ => NONE)
    2.30 +    else NONE);
    2.31 +
    2.32 +
    2.33  
    2.34  (** datatype mfix **)
    2.35  
     3.1 --- a/src/Pure/Thy/export_theory.ML	Sun Sep 16 20:33:37 2018 +0200
     3.2 +++ b/src/Pure/Thy/export_theory.ML	Sun Sep 16 22:45:34 2018 +0200
     3.3 @@ -52,14 +52,14 @@
     3.4      val parents = Theory.parents_of thy;
     3.5      val rep_tsig = Type.rep_tsig (Sign.tsig_of thy);
     3.6  
     3.7 -    val ctxt = Proof_Context.init_global thy;
     3.8 +    val thy_ctxt = Proof_Context.init_global thy;
     3.9  
    3.10  
    3.11      (* entities *)
    3.12  
    3.13      fun entity_markup space name =
    3.14        let
    3.15 -        val xname = Name_Space.extern_shortest ctxt space name;
    3.16 +        val xname = Name_Space.extern_shortest thy_ctxt space name;
    3.17          val {serial, pos, ...} = Name_Space.the_entry space name;
    3.18          val props =
    3.19            Position.offset_properties_of (adjust_pos pos) @
    3.20 @@ -86,35 +86,53 @@
    3.21        in if null elems then () else export_body thy export_name elems end;
    3.22  
    3.23  
    3.24 +    (* infix syntax *)
    3.25 +
    3.26 +    fun get_infix_const ctxt = Syntax.get_infix (Proof_Context.syn_of ctxt) o Lexicon.mark_const;
    3.27 +    fun get_infix_type ctxt = Syntax.get_infix (Proof_Context.syn_of ctxt) o Lexicon.mark_type;
    3.28 +
    3.29 +    fun encode_infix {assoc, delim, pri} =
    3.30 +      let
    3.31 +        val ass =
    3.32 +          (case assoc of
    3.33 +            Syntax_Ext.No_Assoc => 0
    3.34 +          | Syntax_Ext.Left_Assoc => 1
    3.35 +          | Syntax_Ext.Right_Assoc => 2);
    3.36 +        open XML.Encode Term_XML.Encode;
    3.37 +      in triple int string int (ass, delim, pri) end;
    3.38 +
    3.39 +
    3.40      (* types *)
    3.41  
    3.42      val encode_type =
    3.43        let open XML.Encode Term_XML.Encode
    3.44 -      in pair (list string) (option typ) end;
    3.45 +      in triple (option encode_infix) (list string) (option typ) end;
    3.46  
    3.47 -    fun export_type (Type.LogicalType n) =
    3.48 -          SOME (encode_type (Name.invent Name.context Name.aT n, NONE))
    3.49 -      | export_type (Type.Abbreviation (args, U, false)) =
    3.50 -          SOME (encode_type (args, SOME U))
    3.51 -      | export_type _ = NONE;
    3.52 +    fun export_type c (Type.LogicalType n) =
    3.53 +          SOME (encode_type (get_infix_type thy_ctxt c, Name.invent Name.context Name.aT n, NONE))
    3.54 +      | export_type c (Type.Abbreviation (args, U, false)) =
    3.55 +          SOME (encode_type (get_infix_type thy_ctxt c, args, SOME U))
    3.56 +      | export_type _ _ = NONE;
    3.57  
    3.58      val _ =
    3.59 -      export_entities "types" (K export_type) Sign.type_space
    3.60 +      export_entities "types" export_type Sign.type_space
    3.61          (Name_Space.dest_table (#types rep_tsig));
    3.62  
    3.63  
    3.64      (* consts *)
    3.65  
    3.66      val encode_const =
    3.67 -      let open XML.Encode Term_XML.Encode
    3.68 -      in triple (list string) typ (option (term o named_bounds)) end;
    3.69 +      let open XML.Encode Term_XML.Encode in
    3.70 +        pair (option encode_infix) (pair (list string) (pair typ (option (term o named_bounds))))
    3.71 +      end;
    3.72  
    3.73      fun export_const c (T, abbrev) =
    3.74        let
    3.75 +        val syntax = get_infix_const thy_ctxt c;
    3.76          val T' = T |> Logic.unvarifyT_global |> Type.strip_sorts;
    3.77          val abbrev' = abbrev |> Option.map (Logic.unvarify_global #> map_types Type.strip_sorts);
    3.78          val args = map (#1 o dest_TFree) (Consts.typargs (Sign.consts_of thy) (c, T'));
    3.79 -      in SOME (encode_const (args, T', abbrev')) end;
    3.80 +      in SOME (encode_const (syntax, (args, (T', abbrev')))) end;
    3.81  
    3.82      val _ =
    3.83        export_entities "consts" export_const Sign.const_space
     4.1 --- a/src/Pure/Thy/export_theory.scala	Sun Sep 16 20:33:37 2018 +0200
     4.2 +++ b/src/Pure/Thy/export_theory.scala	Sun Sep 16 22:45:34 2018 +0200
     4.3 @@ -190,12 +190,31 @@
     4.4    }
     4.5  
     4.6  
     4.7 +  /* infix syntax */
     4.8 +
     4.9 +  object Assoc extends Enumeration
    4.10 +  {
    4.11 +    val NO_ASSOC, LEFT_ASSOC, RIGHT_ASSOC = Value
    4.12 +  }
    4.13 +
    4.14 +  sealed case class Infix(assoc: Assoc.Value, delim: String, pri: Int)
    4.15 +
    4.16 +  def decode_infix(body: XML.Body): Infix =
    4.17 +  {
    4.18 +    import XML.Decode._
    4.19 +    val (ass, delim, pri) = triple(int, string, int)(body)
    4.20 +    Infix(Assoc(ass), delim, pri)
    4.21 +  }
    4.22 +
    4.23 +
    4.24    /* types */
    4.25  
    4.26 -  sealed case class Type(entity: Entity, args: List[String], abbrev: Option[Term.Typ])
    4.27 +  sealed case class Type(
    4.28 +    entity: Entity, syntax: Option[Infix], args: List[String], abbrev: Option[Term.Typ])
    4.29    {
    4.30      def cache(cache: Term.Cache): Type =
    4.31        Type(entity.cache(cache),
    4.32 +        syntax,
    4.33          args.map(cache.string(_)),
    4.34          abbrev.map(cache.typ(_)))
    4.35    }
    4.36 @@ -204,22 +223,27 @@
    4.37      provider.uncompressed_yxml(export_prefix + "types").map((tree: XML.Tree) =>
    4.38        {
    4.39          val (entity, body) = decode_entity(Kind.TYPE, tree)
    4.40 -        val (args, abbrev) =
    4.41 +        val (syntax, args, abbrev) =
    4.42          {
    4.43            import XML.Decode._
    4.44 -          pair(list(string), option(Term_XML.Decode.typ))(body)
    4.45 +          triple(option(decode_infix), list(string), option(Term_XML.Decode.typ))(body)
    4.46          }
    4.47 -        Type(entity, args, abbrev)
    4.48 +        Type(entity, syntax, args, abbrev)
    4.49        })
    4.50  
    4.51  
    4.52    /* consts */
    4.53  
    4.54    sealed case class Const(
    4.55 -    entity: Entity, typargs: List[String], typ: Term.Typ, abbrev: Option[Term.Term])
    4.56 +    entity: Entity,
    4.57 +    syntax: Option[Infix],
    4.58 +    typargs: List[String],
    4.59 +    typ: Term.Typ,
    4.60 +    abbrev: Option[Term.Term])
    4.61    {
    4.62      def cache(cache: Term.Cache): Const =
    4.63        Const(entity.cache(cache),
    4.64 +        syntax,
    4.65          typargs.map(cache.string(_)),
    4.66          cache.typ(typ),
    4.67          abbrev.map(cache.term(_)))
    4.68 @@ -229,12 +253,13 @@
    4.69      provider.uncompressed_yxml(export_prefix + "consts").map((tree: XML.Tree) =>
    4.70        {
    4.71          val (entity, body) = decode_entity(Kind.CONST, tree)
    4.72 -        val (args, typ, abbrev) =
    4.73 +        val (syntax, (args, (typ, abbrev))) =
    4.74          {
    4.75            import XML.Decode._
    4.76 -          triple(list(string), Term_XML.Decode.typ, option(Term_XML.Decode.term))(body)
    4.77 +          pair(option(decode_infix), pair(list(string),
    4.78 +            pair(Term_XML.Decode.typ, option(Term_XML.Decode.term))))(body)
    4.79          }
    4.80 -        Const(entity, args, typ, abbrev)
    4.81 +        Const(entity, syntax, args, typ, abbrev)
    4.82        })
    4.83  
    4.84