src/Pure/Thy/export_theory.ML
author wenzelm
Fri Sep 21 21:06:23 2018 +0200 (13 months ago)
changeset 69028 f440bedb8e45
parent 69027 5ea3f424e787
child 69029 aec64b88e708
permissions -rw-r--r--
clarified error;
     1 (*  Title:      Pure/Thy/export_theory.ML
     2     Author:     Makarius
     3 
     4 Export foundational theory content and locale/class structure.
     5 *)
     6 
     7 signature EXPORT_THEORY =
     8 sig
     9   val setup_presentation: (Thy_Info.presentation_context -> theory -> unit) -> unit
    10   val export_body: theory -> string -> XML.body -> unit
    11 end;
    12 
    13 structure Export_Theory: EXPORT_THEORY =
    14 struct
    15 
    16 (* standardization of variables: only frees and named bounds *)
    17 
    18 local
    19 
    20 fun declare_names (Abs (_, _, b)) = declare_names b
    21   | declare_names (t $ u) = declare_names t #> declare_names u
    22   | declare_names (Const (c, _)) = Name.declare (Long_Name.base_name c)
    23   | declare_names (Free (x, _)) = Name.declare x
    24   | declare_names _ = I;
    25 
    26 fun variant_abs bs (Abs (x, T, t)) =
    27       let
    28         val names = fold Name.declare bs (declare_names t Name.context);
    29         val x' = #1 (Name.variant x names);
    30         val t' = variant_abs (x' :: bs) t;
    31       in Abs (x', T, t') end
    32   | variant_abs bs (t $ u) = variant_abs bs t $ variant_abs bs u
    33   | variant_abs _ t = t;
    34 
    35 in
    36 
    37 fun standard_vars used =
    38   let
    39     fun zero_var_indexes tm =
    40       Term_Subst.instantiate (Term_Subst.zero_var_indexes_inst used [tm]) tm;
    41 
    42     fun unvarifyT ty = ty |> Term.map_atyps
    43       (fn TVar ((a, _), S) => TFree (a, S)
    44         | T as TFree (a, _) =>
    45             if Name.is_declared used a then T
    46             else raise TYPE (Logic.bad_fixed a, [ty], []));
    47 
    48     fun unvarify tm = tm |> Term.map_aterms
    49       (fn Var ((x, _), T) => Free (x, T)
    50         | t as Free (x, _) =>
    51             if Name.is_declared used x then t
    52             else raise TERM (Logic.bad_fixed x, [tm])
    53         | t => t);
    54 
    55   in zero_var_indexes #> map_types unvarifyT #> unvarify #> variant_abs [] end;
    56 
    57 val standard_vars_global = standard_vars Name.context;
    58 
    59 end;
    60 
    61 
    62 (* free variables: not declared in the context *)
    63 
    64 val is_free = not oo Name.is_declared;
    65 
    66 fun add_frees used =
    67   fold_aterms (fn Free (x, T) => is_free used x ? insert (op =) (x, T) | _ => I);
    68 
    69 fun add_tfrees used =
    70   (fold_types o fold_atyps) (fn TFree (a, S) => is_free used a ? insert (op =) (a, S) | _ => I);
    71 
    72 
    73 (* locale support *)
    74 
    75 fun locale_axioms thy loc =
    76   let
    77     val (intro1, intro2) = Locale.intros_of thy loc;
    78     fun intros_tac ctxt = Method.try_intros_tac ctxt (the_list intro1 @ the_list intro2);
    79     val res =
    80       Proof_Context.init_global thy
    81       |> Interpretation.interpretation ([(loc, (("", false), (Expression.Named [], [])))], [])
    82       |> Proof.refine (Method.Basic (METHOD o intros_tac))
    83       |> Seq.filter_results
    84       |> try Seq.hd;
    85   in
    86     (case res of
    87       SOME st => Thm.prems_of (#goal (Proof.goal st))
    88     | NONE => raise Fail ("Cannot unfold locale " ^ quote loc))
    89   end;
    90 
    91 
    92 (* general setup *)
    93 
    94 fun setup_presentation f =
    95   Theory.setup (Thy_Info.add_presentation (fn context => fn thy =>
    96     if Options.bool (#options context) "export_theory" then f context thy else ()));
    97 
    98 fun export_body thy name body =
    99   Export.export thy ("theory/" ^ name) (Buffer.chunks (YXML.buffer_body body Buffer.empty));
   100 
   101 
   102 (* presentation *)
   103 
   104 val _ = setup_presentation (fn {adjust_pos, ...} => fn thy =>
   105   let
   106     val parents = Theory.parents_of thy;
   107     val rep_tsig = Type.rep_tsig (Sign.tsig_of thy);
   108 
   109     val thy_ctxt = Proof_Context.init_global thy;
   110 
   111 
   112     (* entities *)
   113 
   114     fun entity_markup space name =
   115       let
   116         val xname = Name_Space.extern_shortest thy_ctxt space name;
   117         val {serial, pos, ...} = Name_Space.the_entry space name;
   118         val props =
   119           Position.offset_properties_of (adjust_pos pos) @
   120           Position.id_properties_of pos @
   121           Markup.serial_properties serial;
   122       in (Markup.entityN, (Markup.nameN, name) :: (Markup.xnameN, xname) :: props) end;
   123 
   124     fun export_entities export_name export get_space decls =
   125       let val elems =
   126         let
   127           val parent_spaces = map get_space parents;
   128           val space = get_space thy;
   129         in
   130           (decls, []) |-> fold (fn (name, decl) =>
   131             if exists (fn space => Name_Space.declared space name) parent_spaces then I
   132             else
   133               (case export name decl of
   134                 NONE => I
   135               | SOME body =>
   136                   cons (#serial (Name_Space.the_entry space name),
   137                     XML.Elem (entity_markup space name, body))))
   138           |> sort (int_ord o apply2 #1) |> map #2
   139         end;
   140       in if null elems then () else export_body thy export_name elems end;
   141 
   142 
   143     (* infix syntax *)
   144 
   145     fun get_infix_const ctxt = Syntax.get_infix (Proof_Context.syn_of ctxt) o Lexicon.mark_const;
   146     fun get_infix_type ctxt = Syntax.get_infix (Proof_Context.syn_of ctxt) o Lexicon.mark_type;
   147 
   148     fun encode_infix {assoc, delim, pri} =
   149       let
   150         val ass =
   151           (case assoc of
   152             Syntax_Ext.No_Assoc => 0
   153           | Syntax_Ext.Left_Assoc => 1
   154           | Syntax_Ext.Right_Assoc => 2);
   155         open XML.Encode Term_XML.Encode;
   156       in triple int string int (ass, delim, pri) end;
   157 
   158 
   159     (* types *)
   160 
   161     val encode_type =
   162       let open XML.Encode Term_XML.Encode
   163       in triple (option encode_infix) (list string) (option typ) end;
   164 
   165     fun export_type c (Type.LogicalType n) =
   166           SOME (encode_type (get_infix_type thy_ctxt c, Name.invent Name.context Name.aT n, NONE))
   167       | export_type c (Type.Abbreviation (args, U, false)) =
   168           SOME (encode_type (get_infix_type thy_ctxt c, args, SOME U))
   169       | export_type _ _ = NONE;
   170 
   171     val _ =
   172       export_entities "types" export_type Sign.type_space
   173         (Name_Space.dest_table (#types rep_tsig));
   174 
   175 
   176     (* consts *)
   177 
   178     val encode_const =
   179       let open XML.Encode Term_XML.Encode
   180       in pair (option encode_infix) (pair (list string) (pair typ (option term))) end;
   181 
   182     fun export_const c (T, abbrev) =
   183       let
   184         val syntax = get_infix_const thy_ctxt c;
   185         val T' = T |> Logic.unvarifyT_global |> Type.strip_sorts;
   186         val abbrev' = abbrev |> Option.map (standard_vars_global #> map_types Type.strip_sorts);
   187         val args = map (#1 o dest_TFree) (Consts.typargs (Sign.consts_of thy) (c, T'));
   188       in encode_const (syntax, (args, (T', abbrev'))) end;
   189 
   190     val _ =
   191       export_entities "consts" (SOME oo export_const) Sign.const_space
   192         (#constants (Consts.dest (Sign.consts_of thy)));
   193 
   194 
   195     (* axioms and facts *)
   196 
   197     fun prop_of raw_thm =
   198       let
   199         val thm = raw_thm
   200           |> Thm.transfer thy
   201           |> Thm.check_hyps (Context.Theory thy)
   202           |> Thm.strip_shyps;
   203         val prop = thm
   204           |> Thm.full_prop_of;
   205       in (Thm.extra_shyps thm, prop) end;
   206 
   207     fun encode_prop used (Ss, raw_prop) =
   208       let
   209         val prop = standard_vars used raw_prop;
   210         val args = rev (add_frees used prop []);
   211         val typargs = rev (add_tfrees used prop []);
   212         val used' = fold (Name.declare o #1) typargs used;
   213         val sorts = Name.invent used' Name.aT (length Ss) ~~ Ss;
   214       in
   215         (sorts @ typargs, args, prop) |>
   216           let open XML.Encode Term_XML.Encode
   217           in triple (list (pair string sort)) (list (pair string typ)) term end
   218       end;
   219 
   220     fun encode_axiom used t = encode_prop used ([], t);
   221 
   222     val encode_fact_single = encode_prop Name.context o prop_of;
   223     val encode_fact_multi = XML.Encode.list (encode_prop Name.context) o map prop_of;
   224 
   225     val _ =
   226       export_entities "axioms" (fn _ => fn t => SOME (encode_axiom Name.context t))
   227         Theory.axiom_space (Theory.axioms_of thy);
   228     val _ =
   229       export_entities "facts" (K (SOME o encode_fact_multi))
   230         (Facts.space_of o Global_Theory.facts_of)
   231         (Facts.dest_static true [] (Global_Theory.facts_of thy));
   232 
   233 
   234     (* type classes *)
   235 
   236     val encode_class =
   237       let open XML.Encode Term_XML.Encode
   238       in pair (list (pair string typ)) (list encode_fact_single) end;
   239 
   240     fun export_class name =
   241       (case try (Axclass.get_info thy) name of
   242         NONE => ([], [])
   243       | SOME {params, axioms, ...} => (params, axioms))
   244       |> encode_class |> SOME;
   245 
   246     val _ =
   247       export_entities "classes" (fn name => fn () => export_class name)
   248         Sign.class_space (map (rpair ()) (Graph.keys (Sorts.classes_of (#2 (#classes rep_tsig)))));
   249 
   250 
   251     (* sort algebra *)
   252 
   253     val {classrel, arities} =
   254       Sorts.dest_algebra (map (#2 o #classes o Type.rep_tsig o Sign.tsig_of) parents)
   255         (#2 (#classes rep_tsig));
   256 
   257     val encode_classrel =
   258       let open XML.Encode
   259       in list (pair string (list string)) end;
   260 
   261     val encode_arities =
   262       let open XML.Encode Term_XML.Encode
   263       in list (triple string (list sort) string) end;
   264 
   265     val _ = if null classrel then () else export_body thy "classrel" (encode_classrel classrel);
   266     val _ = if null arities then () else export_body thy "arities" (encode_arities arities);
   267 
   268 
   269     (* locales *)
   270 
   271     fun encode_locale used =
   272       let open XML.Encode Term_XML.Encode
   273       in triple (list (pair string sort)) (list (pair string typ)) (list (encode_axiom used)) end;
   274 
   275     fun export_locale loc ({type_params, params, ...}: Locale.content) =
   276       let
   277         val axioms = locale_axioms thy loc;
   278         val args = map #1 params;
   279 
   280         val typargs = rev (fold Term.add_tfrees (map Free args @ axioms) (rev type_params));
   281         val typargs_dups =
   282           AList.group (op =) typargs |> filter (fn (_, [_]) => false | _ => true)
   283             |> maps (fn (x, ys) => map (pair x) ys);
   284         val typargs_print = Syntax.string_of_typ (Config.put show_sorts true thy_ctxt) o TFree;
   285         val _ =
   286           if null typargs_dups then ()
   287           else error ("Duplicate type parameters " ^ commas (map typargs_print typargs_dups));
   288 
   289         val used = fold Name.declare (map #1 typargs @ map #1 args) Name.context;
   290       in encode_locale used (typargs, args, axioms) end
   291       handle ERROR msg =>
   292         cat_error msg ("The error(s) above occurred in locale " ^
   293           quote (Locale.markup_name thy_ctxt loc));
   294 
   295     val _ =
   296       export_entities "locales" (SOME oo export_locale) Locale.locale_space
   297         (Locale.dest_locales thy);
   298 
   299 
   300     (* parents *)
   301 
   302     val _ =
   303       export_body thy "parents"
   304         (XML.Encode.string (cat_lines (map Context.theory_long_name parents)));
   305 
   306   in () end);
   307 
   308 end;