src/Pure/Thy/export_theory.ML
changeset 69076 90cce2f79e77
parent 69071 3ef82592dc22
child 69077 11529ae45786
     1.1 --- a/src/Pure/Thy/export_theory.ML	Thu Sep 27 07:18:34 2018 +0200
     1.2 +++ b/src/Pure/Thy/export_theory.ML	Fri Sep 28 19:30:07 2018 +0200
     1.3 @@ -13,6 +13,32 @@
     1.4  structure Export_Theory: EXPORT_THEORY =
     1.5  struct
     1.6  
     1.7 +(* infix syntax *)
     1.8 +
     1.9 +fun get_infix_type ctxt = Syntax.get_infix (Proof_Context.syn_of ctxt) o Lexicon.mark_type;
    1.10 +fun get_infix_const ctxt = Syntax.get_infix (Proof_Context.syn_of ctxt) o Lexicon.mark_const;
    1.11 +fun get_infix_fixed ctxt = Syntax.get_infix (Proof_Context.syn_of ctxt) o Lexicon.mark_fixed;
    1.12 +
    1.13 +fun get_infix_param ctxt loc x =
    1.14 +  let val thy = Proof_Context.theory_of ctxt in
    1.15 +    if Class.is_class thy loc then
    1.16 +      (case AList.lookup (op =) (Class.these_params thy [loc]) x of
    1.17 +        NONE => NONE
    1.18 +      | SOME (_, (c, _)) => get_infix_const ctxt c)
    1.19 +    else get_infix_fixed ctxt x
    1.20 +  end;
    1.21 +
    1.22 +fun encode_infix {assoc, delim, pri} =
    1.23 +  let
    1.24 +    val ass =
    1.25 +      (case assoc of
    1.26 +        Printer.No_Assoc => 0
    1.27 +      | Printer.Left_Assoc => 1
    1.28 +      | Printer.Right_Assoc => 2);
    1.29 +    open XML.Encode Term_XML.Encode;
    1.30 +  in triple int string int (ass, delim, pri) end;
    1.31 +
    1.32 +
    1.33  (* standardization of variables: only frees and named bounds *)
    1.34  
    1.35  local
    1.36 @@ -74,12 +100,14 @@
    1.37  
    1.38  fun locale_content thy loc =
    1.39    let
    1.40 -    val args = map #1 (Locale.params_of thy loc);
    1.41 +    val loc_ctxt = Locale.init loc thy;
    1.42 +    val args = Locale.params_of thy loc
    1.43 +      |> map (fn ((x, T), _) => ((x, T), get_infix_param loc_ctxt loc x));
    1.44      val axioms =
    1.45        let
    1.46          val (intro1, intro2) = Locale.intros_of thy loc;
    1.47          fun intros_tac ctxt = Method.try_intros_tac ctxt (the_list intro1 @ the_list intro2);
    1.48 -        val inst = Expression.Named (args |> map (fn (x, T) => (x, Free (x, T))));
    1.49 +        val inst = Expression.Named (args |> map (fn ((x, T), _) => (x, Free (x, T))));
    1.50          val res =
    1.51            Proof_Context.init_global thy
    1.52            |> Interpretation.interpretation ([(loc, (("", false), (inst, [])))], [])
    1.53 @@ -91,7 +119,7 @@
    1.54            SOME st => Thm.prems_of (#goal (Proof.goal st))
    1.55          | NONE => raise Fail ("Cannot unfold locale " ^ quote loc))
    1.56        end;
    1.57 -    val typargs = rev (fold Term.add_tfrees (map Free args @ axioms) []);
    1.58 +    val typargs = rev (fold Term.add_tfrees (map (Free o #1) args @ axioms) []);
    1.59    in {typargs = typargs, args = args, axioms = axioms} end;
    1.60  
    1.61  fun locale_dependency_subst thy (dep: Locale.locale_dependency) =
    1.62 @@ -169,22 +197,6 @@
    1.63        in if null elems then () else export_body thy export_name elems end;
    1.64  
    1.65  
    1.66 -    (* infix syntax *)
    1.67 -
    1.68 -    fun get_infix_const ctxt = Syntax.get_infix (Proof_Context.syn_of ctxt) o Lexicon.mark_const;
    1.69 -    fun get_infix_type ctxt = Syntax.get_infix (Proof_Context.syn_of ctxt) o Lexicon.mark_type;
    1.70 -
    1.71 -    fun encode_infix {assoc, delim, pri} =
    1.72 -      let
    1.73 -        val ass =
    1.74 -          (case assoc of
    1.75 -            Printer.No_Assoc => 0
    1.76 -          | Printer.Left_Assoc => 1
    1.77 -          | Printer.Right_Assoc => 2);
    1.78 -        open XML.Encode Term_XML.Encode;
    1.79 -      in triple int string int (ass, delim, pri) end;
    1.80 -
    1.81 -
    1.82      (* types *)
    1.83  
    1.84      val encode_type =
    1.85 @@ -298,13 +310,15 @@
    1.86      (* locales *)
    1.87  
    1.88      fun encode_locale used =
    1.89 -      let open XML.Encode Term_XML.Encode
    1.90 -      in triple (list (pair string sort)) (list (pair string typ)) (list (encode_axiom used)) end;
    1.91 +      let open XML.Encode Term_XML.Encode in
    1.92 +        triple (list (pair string sort)) (list (pair (pair string typ) (option encode_infix)))
    1.93 +          (list (encode_axiom used))
    1.94 +      end;
    1.95  
    1.96      fun export_locale loc =
    1.97        let
    1.98          val {typargs, args, axioms} = locale_content thy loc;
    1.99 -        val used = fold Name.declare (map #1 typargs @ map #1 args) Name.context;
   1.100 +        val used = fold Name.declare (map #1 typargs @ map (#1 o #1) args) Name.context;
   1.101        in encode_locale used (typargs, args, axioms) end
   1.102        handle ERROR msg =>
   1.103          cat_error msg ("The error(s) above occurred in locale " ^