author  wenzelm 
Sun, 20 Oct 2019 21:34:29 +0200  
changeset 70917  693e811b91bb 
parent 70915  bd4d37edfee4 
child 70919  692095bafcd9 
permissions  rwrr 
68154  1 
(* Title: Pure/Thy/export_theory.ML 
2 
Author: Makarius 

3 

69023
cef000855cf4
clarified standardization of variables, with proper treatment of local variables;
wenzelm
parents:
69019
diff
changeset

4 
Export foundational theory content and locale/class structure. 
68154  5 
*) 
6 

7 
signature EXPORT_THEORY = 

8 
sig 

68201  9 
val setup_presentation: (Thy_Info.presentation_context > theory > unit) > unit 
10 
val export_body: theory > string > XML.body > unit 

68154  11 
end; 
12 

13 
structure Export_Theory: EXPORT_THEORY = 

14 
struct 

15 

69077
11529ae45786
more approximative prefix syntax, including binder;
wenzelm
parents:
69076
diff
changeset

16 
(* approximative syntax *) 
69076  17 

69077
11529ae45786
more approximative prefix syntax, including binder;
wenzelm
parents:
69076
diff
changeset

18 
val get_syntax = Syntax.get_approx o Proof_Context.syn_of; 
11529ae45786
more approximative prefix syntax, including binder;
wenzelm
parents:
69076
diff
changeset

19 
fun get_syntax_type ctxt = get_syntax ctxt o Lexicon.mark_type; 
11529ae45786
more approximative prefix syntax, including binder;
wenzelm
parents:
69076
diff
changeset

20 
fun get_syntax_const ctxt = get_syntax ctxt o Lexicon.mark_const; 
11529ae45786
more approximative prefix syntax, including binder;
wenzelm
parents:
69076
diff
changeset

21 
fun get_syntax_fixed ctxt = get_syntax ctxt o Lexicon.mark_fixed; 
69076  22 

69077
11529ae45786
more approximative prefix syntax, including binder;
wenzelm
parents:
69076
diff
changeset

23 
fun get_syntax_param ctxt loc x = 
69076  24 
let val thy = Proof_Context.theory_of ctxt in 
25 
if Class.is_class thy loc then 

26 
(case AList.lookup (op =) (Class.these_params thy [loc]) x of 

27 
NONE => NONE 

69077
11529ae45786
more approximative prefix syntax, including binder;
wenzelm
parents:
69076
diff
changeset

28 
 SOME (_, (c, _)) => get_syntax_const ctxt c) 
11529ae45786
more approximative prefix syntax, including binder;
wenzelm
parents:
69076
diff
changeset

29 
else get_syntax_fixed ctxt x 
69076  30 
end; 
31 

69077
11529ae45786
more approximative prefix syntax, including binder;
wenzelm
parents:
69076
diff
changeset

32 
val encode_syntax = 
11529ae45786
more approximative prefix syntax, including binder;
wenzelm
parents:
69076
diff
changeset

33 
XML.Encode.variant 
11529ae45786
more approximative prefix syntax, including binder;
wenzelm
parents:
69076
diff
changeset

34 
[fn NONE => ([], []), 
11529ae45786
more approximative prefix syntax, including binder;
wenzelm
parents:
69076
diff
changeset

35 
fn SOME (Syntax.Prefix delim) => ([delim], []), 
11529ae45786
more approximative prefix syntax, including binder;
wenzelm
parents:
69076
diff
changeset

36 
fn SOME (Syntax.Infix {assoc, delim, pri}) => 
11529ae45786
more approximative prefix syntax, including binder;
wenzelm
parents:
69076
diff
changeset

37 
let 
11529ae45786
more approximative prefix syntax, including binder;
wenzelm
parents:
69076
diff
changeset

38 
val ass = 
11529ae45786
more approximative prefix syntax, including binder;
wenzelm
parents:
69076
diff
changeset

39 
(case assoc of 
11529ae45786
more approximative prefix syntax, including binder;
wenzelm
parents:
69076
diff
changeset

40 
Printer.No_Assoc => 0 
11529ae45786
more approximative prefix syntax, including binder;
wenzelm
parents:
69076
diff
changeset

41 
 Printer.Left_Assoc => 1 
11529ae45786
more approximative prefix syntax, including binder;
wenzelm
parents:
69076
diff
changeset

42 
 Printer.Right_Assoc => 2); 
11529ae45786
more approximative prefix syntax, including binder;
wenzelm
parents:
69076
diff
changeset

43 
open XML.Encode Term_XML.Encode; 
11529ae45786
more approximative prefix syntax, including binder;
wenzelm
parents:
69076
diff
changeset

44 
in ([], triple int string int (ass, delim, pri)) end]; 
69076  45 

46 

69023
cef000855cf4
clarified standardization of variables, with proper treatment of local variables;
wenzelm
parents:
69019
diff
changeset

47 
(* free variables: not declared in the context *) 
cef000855cf4
clarified standardization of variables, with proper treatment of local variables;
wenzelm
parents:
69019
diff
changeset

48 

cef000855cf4
clarified standardization of variables, with proper treatment of local variables;
wenzelm
parents:
69019
diff
changeset

49 
val is_free = not oo Name.is_declared; 
cef000855cf4
clarified standardization of variables, with proper treatment of local variables;
wenzelm
parents:
69019
diff
changeset

50 

cef000855cf4
clarified standardization of variables, with proper treatment of local variables;
wenzelm
parents:
69019
diff
changeset

51 
fun add_frees used = 
cef000855cf4
clarified standardization of variables, with proper treatment of local variables;
wenzelm
parents:
69019
diff
changeset

52 
fold_aterms (fn Free (x, T) => is_free used x ? insert (op =) (x, T)  _ => I); 
cef000855cf4
clarified standardization of variables, with proper treatment of local variables;
wenzelm
parents:
69019
diff
changeset

53 

cef000855cf4
clarified standardization of variables, with proper treatment of local variables;
wenzelm
parents:
69019
diff
changeset

54 
fun add_tfrees used = 
cef000855cf4
clarified standardization of variables, with proper treatment of local variables;
wenzelm
parents:
69019
diff
changeset

55 
(fold_types o fold_atyps) (fn TFree (a, S) => is_free used a ? insert (op =) (a, S)  _ => I); 
cef000855cf4
clarified standardization of variables, with proper treatment of local variables;
wenzelm
parents:
69019
diff
changeset

56 

cef000855cf4
clarified standardization of variables, with proper treatment of local variables;
wenzelm
parents:
69019
diff
changeset

57 

69992
bd3c10813cc4
more informative Spec_Rules.Equational, notably primrec argument types;
wenzelm
parents:
69988
diff
changeset

58 
(* spec rules *) 
bd3c10813cc4
more informative Spec_Rules.Equational, notably primrec argument types;
wenzelm
parents:
69988
diff
changeset

59 

bd3c10813cc4
more informative Spec_Rules.Equational, notably primrec argument types;
wenzelm
parents:
69988
diff
changeset

60 
fun primrec_types ctxt const = 
bd3c10813cc4
more informative Spec_Rules.Equational, notably primrec argument types;
wenzelm
parents:
69988
diff
changeset

61 
Spec_Rules.retrieve ctxt (Const const) 
69996
8f2d3a27aff0
more informative Spec_Rules.Equational: support corecursion;
wenzelm
parents:
69992
diff
changeset

62 
> get_first 
8f2d3a27aff0
more informative Spec_Rules.Equational: support corecursion;
wenzelm
parents:
69992
diff
changeset

63 
(fn (Spec_Rules.Equational (Spec_Rules.Primrec types), _) => SOME (types, false) 
8f2d3a27aff0
more informative Spec_Rules.Equational: support corecursion;
wenzelm
parents:
69992
diff
changeset

64 
 (Spec_Rules.Equational (Spec_Rules.Primcorec types), _) => SOME (types, true) 
8f2d3a27aff0
more informative Spec_Rules.Equational: support corecursion;
wenzelm
parents:
69992
diff
changeset

65 
 _ => NONE) 
8f2d3a27aff0
more informative Spec_Rules.Equational: support corecursion;
wenzelm
parents:
69992
diff
changeset

66 
> the_default ([], false); 
69992
bd3c10813cc4
more informative Spec_Rules.Equational, notably primrec argument types;
wenzelm
parents:
69988
diff
changeset

67 

bd3c10813cc4
more informative Spec_Rules.Equational, notably primrec argument types;
wenzelm
parents:
69988
diff
changeset

68 

69087
06017b2c4552
suppress aux. locales from command 'experiment'  avoid crash of theory Dict_Construction.Test_Dict_Construction (AFP);
wenzelm
parents:
69086
diff
changeset

69 
(* locales content *) 
69019  70 

69034  71 
fun locale_content thy loc = 
69019  72 
let 
69083
6f8ae6ddc26b
more direct locale goal: avoid renaming of type_parameters;
wenzelm
parents:
69077
diff
changeset

73 
val ctxt = Locale.init loc thy; 
6f8ae6ddc26b
more direct locale goal: avoid renaming of type_parameters;
wenzelm
parents:
69077
diff
changeset

74 
val args = 
6f8ae6ddc26b
more direct locale goal: avoid renaming of type_parameters;
wenzelm
parents:
69077
diff
changeset

75 
Locale.params_of thy loc 
6f8ae6ddc26b
more direct locale goal: avoid renaming of type_parameters;
wenzelm
parents:
69077
diff
changeset

76 
> map (fn ((x, T), _) => ((x, T), get_syntax_param ctxt loc x)); 
69029
aec64b88e708
clarified locale content: proper args with types for interpretation/axioms and typargs derived from the result;
wenzelm
parents:
69028
diff
changeset

77 
val axioms = 
aec64b88e708
clarified locale content: proper args with types for interpretation/axioms and typargs derived from the result;
wenzelm
parents:
69028
diff
changeset

78 
let 
69083
6f8ae6ddc26b
more direct locale goal: avoid renaming of type_parameters;
wenzelm
parents:
69077
diff
changeset

79 
val (asm, defs) = Locale.specification_of thy loc; 
6f8ae6ddc26b
more direct locale goal: avoid renaming of type_parameters;
wenzelm
parents:
69077
diff
changeset

80 
val cprops = map (Thm.cterm_of ctxt) (the_list asm @ defs); 
69029
aec64b88e708
clarified locale content: proper args with types for interpretation/axioms and typargs derived from the result;
wenzelm
parents:
69028
diff
changeset

81 
val (intro1, intro2) = Locale.intros_of thy loc; 
69083
6f8ae6ddc26b
more direct locale goal: avoid renaming of type_parameters;
wenzelm
parents:
69077
diff
changeset

82 
val intros_tac = Method.try_intros_tac ctxt (the_list intro1 @ the_list intro2) []; 
69029
aec64b88e708
clarified locale content: proper args with types for interpretation/axioms and typargs derived from the result;
wenzelm
parents:
69028
diff
changeset

83 
val res = 
69083
6f8ae6ddc26b
more direct locale goal: avoid renaming of type_parameters;
wenzelm
parents:
69077
diff
changeset

84 
Goal.init (Conjunction.mk_conjunction_balanced cprops) 
6f8ae6ddc26b
more direct locale goal: avoid renaming of type_parameters;
wenzelm
parents:
69077
diff
changeset

85 
> (ALLGOALS Goal.conjunction_tac THEN intros_tac) 
69029
aec64b88e708
clarified locale content: proper args with types for interpretation/axioms and typargs derived from the result;
wenzelm
parents:
69028
diff
changeset

86 
> try Seq.hd; 
aec64b88e708
clarified locale content: proper args with types for interpretation/axioms and typargs derived from the result;
wenzelm
parents:
69028
diff
changeset

87 
in 
aec64b88e708
clarified locale content: proper args with types for interpretation/axioms and typargs derived from the result;
wenzelm
parents:
69028
diff
changeset

88 
(case res of 
69083
6f8ae6ddc26b
more direct locale goal: avoid renaming of type_parameters;
wenzelm
parents:
69077
diff
changeset

89 
SOME goal => Thm.prems_of goal 
69029
aec64b88e708
clarified locale content: proper args with types for interpretation/axioms and typargs derived from the result;
wenzelm
parents:
69028
diff
changeset

90 
 NONE => raise Fail ("Cannot unfold locale " ^ quote loc)) 
aec64b88e708
clarified locale content: proper args with types for interpretation/axioms and typargs derived from the result;
wenzelm
parents:
69028
diff
changeset

91 
end; 
69076  92 
val typargs = rev (fold Term.add_tfrees (map (Free o #1) args @ axioms) []); 
69029
aec64b88e708
clarified locale content: proper args with types for interpretation/axioms and typargs derived from the result;
wenzelm
parents:
69028
diff
changeset

93 
in {typargs = typargs, args = args, axioms = axioms} end; 
69019  94 

69087
06017b2c4552
suppress aux. locales from command 'experiment'  avoid crash of theory Dict_Construction.Test_Dict_Construction (AFP);
wenzelm
parents:
69086
diff
changeset

95 
fun get_locales thy = 
06017b2c4552
suppress aux. locales from command 'experiment'  avoid crash of theory Dict_Construction.Test_Dict_Construction (AFP);
wenzelm
parents:
69086
diff
changeset

96 
Locale.get_locales thy > map_filter (fn loc => 
06017b2c4552
suppress aux. locales from command 'experiment'  avoid crash of theory Dict_Construction.Test_Dict_Construction (AFP);
wenzelm
parents:
69086
diff
changeset

97 
if Experiment.is_experiment thy loc then NONE else SOME (loc, ())); 
06017b2c4552
suppress aux. locales from command 'experiment'  avoid crash of theory Dict_Construction.Test_Dict_Construction (AFP);
wenzelm
parents:
69086
diff
changeset

98 

06017b2c4552
suppress aux. locales from command 'experiment'  avoid crash of theory Dict_Construction.Test_Dict_Construction (AFP);
wenzelm
parents:
69086
diff
changeset

99 
fun get_dependencies prev_thys thy = 
06017b2c4552
suppress aux. locales from command 'experiment'  avoid crash of theory Dict_Construction.Test_Dict_Construction (AFP);
wenzelm
parents:
69086
diff
changeset

100 
Locale.dest_dependencies prev_thys thy > map_filter (fn dep => 
06017b2c4552
suppress aux. locales from command 'experiment'  avoid crash of theory Dict_Construction.Test_Dict_Construction (AFP);
wenzelm
parents:
69086
diff
changeset

101 
if Experiment.is_experiment thy (#source dep) orelse 
06017b2c4552
suppress aux. locales from command 'experiment'  avoid crash of theory Dict_Construction.Test_Dict_Construction (AFP);
wenzelm
parents:
69086
diff
changeset

102 
Experiment.is_experiment thy (#target dep) then NONE 
06017b2c4552
suppress aux. locales from command 'experiment'  avoid crash of theory Dict_Construction.Test_Dict_Construction (AFP);
wenzelm
parents:
69086
diff
changeset

103 
else 
06017b2c4552
suppress aux. locales from command 'experiment'  avoid crash of theory Dict_Construction.Test_Dict_Construction (AFP);
wenzelm
parents:
69086
diff
changeset

104 
let 
06017b2c4552
suppress aux. locales from command 'experiment'  avoid crash of theory Dict_Construction.Test_Dict_Construction (AFP);
wenzelm
parents:
69086
diff
changeset

105 
val (type_params, params) = Locale.parameters_of thy (#source dep); 
06017b2c4552
suppress aux. locales from command 'experiment'  avoid crash of theory Dict_Construction.Test_Dict_Construction (AFP);
wenzelm
parents:
69086
diff
changeset

106 
val typargs = fold (Term.add_tfreesT o #2 o #1) params type_params; 
06017b2c4552
suppress aux. locales from command 'experiment'  avoid crash of theory Dict_Construction.Test_Dict_Construction (AFP);
wenzelm
parents:
69086
diff
changeset

107 
val substT = 
06017b2c4552
suppress aux. locales from command 'experiment'  avoid crash of theory Dict_Construction.Test_Dict_Construction (AFP);
wenzelm
parents:
69086
diff
changeset

108 
typargs > map_filter (fn v => 
06017b2c4552
suppress aux. locales from command 'experiment'  avoid crash of theory Dict_Construction.Test_Dict_Construction (AFP);
wenzelm
parents:
69086
diff
changeset

109 
let 
06017b2c4552
suppress aux. locales from command 'experiment'  avoid crash of theory Dict_Construction.Test_Dict_Construction (AFP);
wenzelm
parents:
69086
diff
changeset

110 
val T = TFree v; 
06017b2c4552
suppress aux. locales from command 'experiment'  avoid crash of theory Dict_Construction.Test_Dict_Construction (AFP);
wenzelm
parents:
69086
diff
changeset

111 
val T' = Morphism.typ (#morphism dep) T; 
06017b2c4552
suppress aux. locales from command 'experiment'  avoid crash of theory Dict_Construction.Test_Dict_Construction (AFP);
wenzelm
parents:
69086
diff
changeset

112 
in if T = T' then NONE else SOME (v, T') end); 
06017b2c4552
suppress aux. locales from command 'experiment'  avoid crash of theory Dict_Construction.Test_Dict_Construction (AFP);
wenzelm
parents:
69086
diff
changeset

113 
val subst = 
06017b2c4552
suppress aux. locales from command 'experiment'  avoid crash of theory Dict_Construction.Test_Dict_Construction (AFP);
wenzelm
parents:
69086
diff
changeset

114 
params > map_filter (fn (v, _) => 
06017b2c4552
suppress aux. locales from command 'experiment'  avoid crash of theory Dict_Construction.Test_Dict_Construction (AFP);
wenzelm
parents:
69086
diff
changeset

115 
let 
06017b2c4552
suppress aux. locales from command 'experiment'  avoid crash of theory Dict_Construction.Test_Dict_Construction (AFP);
wenzelm
parents:
69086
diff
changeset

116 
val t = Free v; 
06017b2c4552
suppress aux. locales from command 'experiment'  avoid crash of theory Dict_Construction.Test_Dict_Construction (AFP);
wenzelm
parents:
69086
diff
changeset

117 
val t' = Morphism.term (#morphism dep) t; 
06017b2c4552
suppress aux. locales from command 'experiment'  avoid crash of theory Dict_Construction.Test_Dict_Construction (AFP);
wenzelm
parents:
69086
diff
changeset

118 
in if t aconv t' then NONE else SOME (v, t') end); 
06017b2c4552
suppress aux. locales from command 'experiment'  avoid crash of theory Dict_Construction.Test_Dict_Construction (AFP);
wenzelm
parents:
69086
diff
changeset

119 
in SOME (dep, (substT, subst)) end); 
69069
b9aca3b9619f
export locale dependencies, with approx. morphism as type/term substitution;
wenzelm
parents:
69034
diff
changeset

120 

69019  121 

68201  122 
(* general setup *) 
68154  123 

68201  124 
fun setup_presentation f = 
125 
Theory.setup (Thy_Info.add_presentation (fn context => fn thy => 

126 
if Options.bool (#options context) "export_theory" then f context thy else ())); 

68154  127 

70601
79831e40e2be
more scalable: avoid huge intermediate XML elems;
wenzelm
parents:
70597
diff
changeset

128 
fun export_buffer thy name buffer = 
79831e40e2be
more scalable: avoid huge intermediate XML elems;
wenzelm
parents:
70597
diff
changeset

129 
if Buffer.is_empty buffer then () 
79831e40e2be
more scalable: avoid huge intermediate XML elems;
wenzelm
parents:
70597
diff
changeset

130 
else Export.export thy (Path.binding0 (Path.make ["theory", name])) (Buffer.chunks buffer); 
79831e40e2be
more scalable: avoid huge intermediate XML elems;
wenzelm
parents:
70597
diff
changeset

131 

79831e40e2be
more scalable: avoid huge intermediate XML elems;
wenzelm
parents:
70597
diff
changeset

132 
fun export_body thy name elems = 
79831e40e2be
more scalable: avoid huge intermediate XML elems;
wenzelm
parents:
70597
diff
changeset

133 
export_buffer thy name (YXML.buffer_body elems Buffer.empty); 
68165  134 

68154  135 

68201  136 
(* presentation *) 
137 

138 
val _ = setup_presentation (fn {adjust_pos, ...} => fn thy => 

139 
let 

68900
1145b25c53de
more robust: parents are strict in Export_Theory.read_theory and thus approximate "commit" of exports;
wenzelm
parents:
68864
diff
changeset

140 
val parents = Theory.parents_of thy; 
68264  141 
val rep_tsig = Type.rep_tsig (Sign.tsig_of thy); 
142 

69003  143 
val thy_ctxt = Proof_Context.init_global thy; 
68997  144 

68264  145 

68201  146 
(* entities *) 
68154  147 

69069
b9aca3b9619f
export locale dependencies, with approx. morphism as type/term substitution;
wenzelm
parents:
69034
diff
changeset

148 
fun make_entity_markup name xname pos serial = 
68201  149 
let 
150 
val props = 

68830
44ec6fdaacf8
retain original id, which is command_id/exec_id for PIDE;
wenzelm
parents:
68727
diff
changeset

151 
Position.offset_properties_of (adjust_pos pos) @ 
44ec6fdaacf8
retain original id, which is command_id/exec_id for PIDE;
wenzelm
parents:
68727
diff
changeset

152 
Position.id_properties_of pos @ 
44ec6fdaacf8
retain original id, which is command_id/exec_id for PIDE;
wenzelm
parents:
68727
diff
changeset

153 
Markup.serial_properties serial; 
68997  154 
in (Markup.entityN, (Markup.nameN, name) :: (Markup.xnameN, xname) :: props) end; 
68154  155 

69069
b9aca3b9619f
export locale dependencies, with approx. morphism as type/term substitution;
wenzelm
parents:
69034
diff
changeset

156 
fun entity_markup space name = 
b9aca3b9619f
export locale dependencies, with approx. morphism as type/term substitution;
wenzelm
parents:
69034
diff
changeset

157 
let 
b9aca3b9619f
export locale dependencies, with approx. morphism as type/term substitution;
wenzelm
parents:
69034
diff
changeset

158 
val xname = Name_Space.extern_shortest thy_ctxt space name; 
b9aca3b9619f
export locale dependencies, with approx. morphism as type/term substitution;
wenzelm
parents:
69034
diff
changeset

159 
val {serial, pos, ...} = Name_Space.the_entry space name; 
b9aca3b9619f
export locale dependencies, with approx. morphism as type/term substitution;
wenzelm
parents:
69034
diff
changeset

160 
in make_entity_markup name xname pos serial end; 
b9aca3b9619f
export locale dependencies, with approx. morphism as type/term substitution;
wenzelm
parents:
69034
diff
changeset

161 

68201  162 
fun export_entities export_name export get_space decls = 
70601
79831e40e2be
more scalable: avoid huge intermediate XML elems;
wenzelm
parents:
70597
diff
changeset

163 
let 
79831e40e2be
more scalable: avoid huge intermediate XML elems;
wenzelm
parents:
70597
diff
changeset

164 
val parent_spaces = map get_space parents; 
79831e40e2be
more scalable: avoid huge intermediate XML elems;
wenzelm
parents:
70597
diff
changeset

165 
val space = get_space thy; 
79831e40e2be
more scalable: avoid huge intermediate XML elems;
wenzelm
parents:
70597
diff
changeset

166 
in 
79831e40e2be
more scalable: avoid huge intermediate XML elems;
wenzelm
parents:
70597
diff
changeset

167 
(decls, []) > fold (fn (name, decl) => 
79831e40e2be
more scalable: avoid huge intermediate XML elems;
wenzelm
parents:
70597
diff
changeset

168 
if exists (fn space => Name_Space.declared space name) parent_spaces then I 
79831e40e2be
more scalable: avoid huge intermediate XML elems;
wenzelm
parents:
70597
diff
changeset

169 
else 
79831e40e2be
more scalable: avoid huge intermediate XML elems;
wenzelm
parents:
70597
diff
changeset

170 
(case export name decl of 
79831e40e2be
more scalable: avoid huge intermediate XML elems;
wenzelm
parents:
70597
diff
changeset

171 
NONE => I 
79831e40e2be
more scalable: avoid huge intermediate XML elems;
wenzelm
parents:
70597
diff
changeset

172 
 SOME body => 
79831e40e2be
more scalable: avoid huge intermediate XML elems;
wenzelm
parents:
70597
diff
changeset

173 
cons (#serial (Name_Space.the_entry space name), 
79831e40e2be
more scalable: avoid huge intermediate XML elems;
wenzelm
parents:
70597
diff
changeset

174 
XML.Elem (entity_markup space name, body)))) 
79831e40e2be
more scalable: avoid huge intermediate XML elems;
wenzelm
parents:
70597
diff
changeset

175 
> sort (int_ord o apply2 #1) > map #2 
79831e40e2be
more scalable: avoid huge intermediate XML elems;
wenzelm
parents:
70597
diff
changeset

176 
> export_body thy export_name 
79831e40e2be
more scalable: avoid huge intermediate XML elems;
wenzelm
parents:
70597
diff
changeset

177 
end; 
68165  178 

179 

68201  180 
(* types *) 
68165  181 

68201  182 
val encode_type = 
183 
let open XML.Encode Term_XML.Encode 

69077
11529ae45786
more approximative prefix syntax, including binder;
wenzelm
parents:
69076
diff
changeset

184 
in triple encode_syntax (list string) (option typ) end; 
68165  185 

69003  186 
fun export_type c (Type.LogicalType n) = 
69077
11529ae45786
more approximative prefix syntax, including binder;
wenzelm
parents:
69076
diff
changeset

187 
SOME (encode_type (get_syntax_type thy_ctxt c, Name.invent Name.context Name.aT n, NONE)) 
69003  188 
 export_type c (Type.Abbreviation (args, U, false)) = 
69077
11529ae45786
more approximative prefix syntax, including binder;
wenzelm
parents:
69076
diff
changeset

189 
SOME (encode_type (get_syntax_type thy_ctxt c, args, SOME U)) 
69003  190 
 export_type _ _ = NONE; 
68165  191 

68201  192 
val _ = 
69003  193 
export_entities "types" export_type Sign.type_space 
68264  194 
(Name_Space.dest_table (#types rep_tsig)); 
68201  195 

68173  196 

68201  197 
(* consts *) 
198 

70784
799437173553
Term_XML.Encode/Decode.term uses Const "typargs";
wenzelm
parents:
70605
diff
changeset

199 
val consts = Sign.consts_of thy; 
799437173553
Term_XML.Encode/Decode.term uses Const "typargs";
wenzelm
parents:
70605
diff
changeset

200 
val encode_term = Term_XML.Encode.term consts; 
799437173553
Term_XML.Encode/Decode.term uses Const "typargs";
wenzelm
parents:
70605
diff
changeset

201 

68201  202 
val encode_const = 
69992
bd3c10813cc4
more informative Spec_Rules.Equational, notably primrec argument types;
wenzelm
parents:
69988
diff
changeset

203 
let open XML.Encode Term_XML.Encode in 
bd3c10813cc4
more informative Spec_Rules.Equational, notably primrec argument types;
wenzelm
parents:
69988
diff
changeset

204 
pair encode_syntax 
69996
8f2d3a27aff0
more informative Spec_Rules.Equational: support corecursion;
wenzelm
parents:
69992
diff
changeset

205 
(pair (list string) 
70784
799437173553
Term_XML.Encode/Decode.term uses Const "typargs";
wenzelm
parents:
70605
diff
changeset

206 
(pair typ (pair (option encode_term) (pair bool (pair (list string) bool))))) 
69992
bd3c10813cc4
more informative Spec_Rules.Equational, notably primrec argument types;
wenzelm
parents:
69988
diff
changeset

207 
end; 
68165  208 

68201  209 
fun export_const c (T, abbrev) = 
210 
let 

69077
11529ae45786
more approximative prefix syntax, including binder;
wenzelm
parents:
69076
diff
changeset

211 
val syntax = get_syntax_const thy_ctxt c; 
69992
bd3c10813cc4
more informative Spec_Rules.Equational, notably primrec argument types;
wenzelm
parents:
69988
diff
changeset

212 
val U = Logic.unvarifyT_global T; 
bd3c10813cc4
more informative Spec_Rules.Equational, notably primrec argument types;
wenzelm
parents:
69988
diff
changeset

213 
val U0 = Type.strip_sorts U; 
69996
8f2d3a27aff0
more informative Spec_Rules.Equational: support corecursion;
wenzelm
parents:
69992
diff
changeset

214 
val recursion = primrec_types thy_ctxt (c, U); 
70529  215 
val abbrev' = abbrev 
216 
> Option.map (Proofterm.standard_vars_term Name.context #> map_types Type.strip_sorts); 

70784
799437173553
Term_XML.Encode/Decode.term uses Const "typargs";
wenzelm
parents:
70605
diff
changeset

217 
val args = map (#1 o dest_TFree) (Consts.typargs consts (c, U0)); 
69992
bd3c10813cc4
more informative Spec_Rules.Equational, notably primrec argument types;
wenzelm
parents:
69988
diff
changeset

218 
val propositional = Object_Logic.is_propositional thy_ctxt (Term.body_type U0); 
69996
8f2d3a27aff0
more informative Spec_Rules.Equational: support corecursion;
wenzelm
parents:
69992
diff
changeset

219 
in encode_const (syntax, (args, (U0, (abbrev', (propositional, recursion))))) end; 
68165  220 

68201  221 
val _ = 
69023
cef000855cf4
clarified standardization of variables, with proper treatment of local variables;
wenzelm
parents:
69019
diff
changeset

222 
export_entities "consts" (SOME oo export_const) Sign.const_space 
70784
799437173553
Term_XML.Encode/Decode.term uses Const "typargs";
wenzelm
parents:
70605
diff
changeset

223 
(#constants (Consts.dest consts)); 
68201  224 

68208  225 

70579
5a8e3e4b3760
clarified export of axioms and theorems (identified derivations instead of projected facts);
wenzelm
parents:
70541
diff
changeset

226 
(* axioms *) 
68208  227 

70534
fb876ebbf5a7
export facts with reconstructed proof term (if possible), but its PThm boxes need to be collected separately;
wenzelm
parents:
70529
diff
changeset

228 
fun standard_prop used extra_shyps raw_prop raw_proof = 
68727  229 
let 
70541
f3fbc7f3559d
more careful treatment of hidden type variable names: smash before zero_var_indexes to get standard enumeration;
wenzelm
parents:
70540
diff
changeset

230 
val (prop, proof) = Proofterm.standard_vars used (raw_prop, raw_proof); 
69023
cef000855cf4
clarified standardization of variables, with proper treatment of local variables;
wenzelm
parents:
69019
diff
changeset

231 
val args = rev (add_frees used prop []); 
cef000855cf4
clarified standardization of variables, with proper treatment of local variables;
wenzelm
parents:
69019
diff
changeset

232 
val typargs = rev (add_tfrees used prop []); 
70534
fb876ebbf5a7
export facts with reconstructed proof term (if possible), but its PThm boxes need to be collected separately;
wenzelm
parents:
70529
diff
changeset

233 
val used_typargs = fold (Name.declare o #1) typargs used; 
fb876ebbf5a7
export facts with reconstructed proof term (if possible), but its PThm boxes need to be collected separately;
wenzelm
parents:
70529
diff
changeset

234 
val sorts = Name.invent used_typargs Name.aT (length extra_shyps) ~~ extra_shyps; 
70541
f3fbc7f3559d
more careful treatment of hidden type variable names: smash before zero_var_indexes to get standard enumeration;
wenzelm
parents:
70540
diff
changeset

235 
in ((sorts @ typargs, args, prop), proof) end; 
70534
fb876ebbf5a7
export facts with reconstructed proof term (if possible), but its PThm boxes need to be collected separately;
wenzelm
parents:
70529
diff
changeset

236 

fb876ebbf5a7
export facts with reconstructed proof term (if possible), but its PThm boxes need to be collected separately;
wenzelm
parents:
70529
diff
changeset

237 
val encode_prop = 
fb876ebbf5a7
export facts with reconstructed proof term (if possible), but its PThm boxes need to be collected separately;
wenzelm
parents:
70529
diff
changeset

238 
let open XML.Encode Term_XML.Encode 
70784
799437173553
Term_XML.Encode/Decode.term uses Const "typargs";
wenzelm
parents:
70605
diff
changeset

239 
in triple (list (pair string sort)) (list (pair string typ)) encode_term end; 
70534
fb876ebbf5a7
export facts with reconstructed proof term (if possible), but its PThm boxes need to be collected separately;
wenzelm
parents:
70529
diff
changeset

240 

fb876ebbf5a7
export facts with reconstructed proof term (if possible), but its PThm boxes need to be collected separately;
wenzelm
parents:
70529
diff
changeset

241 
fun encode_axiom used prop = 
fb876ebbf5a7
export facts with reconstructed proof term (if possible), but its PThm boxes need to be collected separately;
wenzelm
parents:
70529
diff
changeset

242 
encode_prop (#1 (standard_prop used [] prop NONE)); 
68208  243 

70579
5a8e3e4b3760
clarified export of axioms and theorems (identified derivations instead of projected facts);
wenzelm
parents:
70541
diff
changeset

244 
val _ = 
5a8e3e4b3760
clarified export of axioms and theorems (identified derivations instead of projected facts);
wenzelm
parents:
70541
diff
changeset

245 
export_entities "axioms" (fn _ => fn t => SOME (encode_axiom Name.context t)) 
5a8e3e4b3760
clarified export of axioms and theorems (identified derivations instead of projected facts);
wenzelm
parents:
70541
diff
changeset

246 
Theory.axiom_space (Theory.axioms_of thy); 
5a8e3e4b3760
clarified export of axioms and theorems (identified derivations instead of projected facts);
wenzelm
parents:
70541
diff
changeset

247 

5a8e3e4b3760
clarified export of axioms and theorems (identified derivations instead of projected facts);
wenzelm
parents:
70541
diff
changeset

248 

70914
05c4c6a99b3f
option to export standardized proof terms (not scalable);
wenzelm
parents:
70909
diff
changeset

249 
(* theorems and proof terms *) 
05c4c6a99b3f
option to export standardized proof terms (not scalable);
wenzelm
parents:
70909
diff
changeset

250 

05c4c6a99b3f
option to export standardized proof terms (not scalable);
wenzelm
parents:
70909
diff
changeset

251 
val export_standard_proofs = Options.default_bool @{system_option export_standard_proofs}; 
70579
5a8e3e4b3760
clarified export of axioms and theorems (identified derivations instead of projected facts);
wenzelm
parents:
70541
diff
changeset

252 

70895
2a318149b01b
proof boxes based on proof digest (not proof term): thus it works with prune_proofs;
wenzelm
parents:
70892
diff
changeset

253 
val clean_thm = Thm.check_hyps (Context.Theory thy) #> Thm.strip_shyps; 
69023
cef000855cf4
clarified standardization of variables, with proper treatment of local variables;
wenzelm
parents:
69019
diff
changeset

254 

70892
aadb5c23af24
clarified proof_boxes (requires prune_proofs=false);
wenzelm
parents:
70884
diff
changeset

255 
val lookup_thm_id = Global_Theory.lookup_thm_id thy; 
aadb5c23af24
clarified proof_boxes (requires prune_proofs=false);
wenzelm
parents:
70884
diff
changeset

256 

70914
05c4c6a99b3f
option to export standardized proof terms (not scalable);
wenzelm
parents:
70909
diff
changeset

257 
fun proof_boxes_of thm thm_id = 
70917
693e811b91bb
more robust hybrid treatment of Pure, notably for Isabelle/Dedukti;
wenzelm
parents:
70915
diff
changeset

258 
let 
693e811b91bb
more robust hybrid treatment of Pure, notably for Isabelle/Dedukti;
wenzelm
parents:
70915
diff
changeset

259 
val dep_boxes = 
693e811b91bb
more robust hybrid treatment of Pure, notably for Isabelle/Dedukti;
wenzelm
parents:
70915
diff
changeset

260 
thm > Thm_Deps.proof_boxes (fn thm_id' => 
693e811b91bb
more robust hybrid treatment of Pure, notably for Isabelle/Dedukti;
wenzelm
parents:
70915
diff
changeset

261 
if #serial thm_id = #serial thm_id' then false else is_some (lookup_thm_id thm_id')); 
693e811b91bb
more robust hybrid treatment of Pure, notably for Isabelle/Dedukti;
wenzelm
parents:
70915
diff
changeset

262 
in dep_boxes @ [thm_id] end; 
70914
05c4c6a99b3f
option to export standardized proof terms (not scalable);
wenzelm
parents:
70909
diff
changeset

263 

70915
bd4d37edfee4
clarified expand_proof/expand_name: allow more detailed control via thm_header;
wenzelm
parents:
70914
diff
changeset

264 
fun expand_name thm_id (header: Proofterm.thm_header) = 
bd4d37edfee4
clarified expand_proof/expand_name: allow more detailed control via thm_header;
wenzelm
parents:
70914
diff
changeset

265 
if #serial header = #serial thm_id then "" 
bd4d37edfee4
clarified expand_proof/expand_name: allow more detailed control via thm_header;
wenzelm
parents:
70914
diff
changeset

266 
else 
bd4d37edfee4
clarified expand_proof/expand_name: allow more detailed control via thm_header;
wenzelm
parents:
70914
diff
changeset

267 
(case lookup_thm_id (Proofterm.thm_header_id header) of 
bd4d37edfee4
clarified expand_proof/expand_name: allow more detailed control via thm_header;
wenzelm
parents:
70914
diff
changeset

268 
NONE => "" 
bd4d37edfee4
clarified expand_proof/expand_name: allow more detailed control via thm_header;
wenzelm
parents:
70914
diff
changeset

269 
 SOME thm_name => Thm_Name.print thm_name); 
bd4d37edfee4
clarified expand_proof/expand_name: allow more detailed control via thm_header;
wenzelm
parents:
70914
diff
changeset

270 

70579
5a8e3e4b3760
clarified export of axioms and theorems (identified derivations instead of projected facts);
wenzelm
parents:
70541
diff
changeset

271 
fun entity_markup_thm (serial, (name, i)) = 
5a8e3e4b3760
clarified export of axioms and theorems (identified derivations instead of projected facts);
wenzelm
parents:
70541
diff
changeset

272 
let 
5a8e3e4b3760
clarified export of axioms and theorems (identified derivations instead of projected facts);
wenzelm
parents:
70541
diff
changeset

273 
val space = Facts.space_of (Global_Theory.facts_of thy); 
5a8e3e4b3760
clarified export of axioms and theorems (identified derivations instead of projected facts);
wenzelm
parents:
70541
diff
changeset

274 
val xname = Name_Space.extern_shortest thy_ctxt space name; 
5a8e3e4b3760
clarified export of axioms and theorems (identified derivations instead of projected facts);
wenzelm
parents:
70541
diff
changeset

275 
val {pos, ...} = Name_Space.the_entry space name; 
5a8e3e4b3760
clarified export of axioms and theorems (identified derivations instead of projected facts);
wenzelm
parents:
70541
diff
changeset

276 
in make_entity_markup (Thm_Name.print (name, i)) (Thm_Name.print (xname, i)) pos serial end; 
5a8e3e4b3760
clarified export of axioms and theorems (identified derivations instead of projected facts);
wenzelm
parents:
70541
diff
changeset

277 

70915
bd4d37edfee4
clarified expand_proof/expand_name: allow more detailed control via thm_header;
wenzelm
parents:
70914
diff
changeset

278 
fun encode_thm thm_id raw_thm = 
70597  279 
let 
70605  280 
val deps = map (Thm_Name.print o #2) (Thm_Deps.thm_deps thy [raw_thm]); 
70909  281 
val thm = Thm.unconstrainT (clean_thm raw_thm); 
70914
05c4c6a99b3f
option to export standardized proof terms (not scalable);
wenzelm
parents:
70909
diff
changeset

282 
val boxes = proof_boxes_of thm thm_id; 
05c4c6a99b3f
option to export standardized proof terms (not scalable);
wenzelm
parents:
70909
diff
changeset

283 

05c4c6a99b3f
option to export standardized proof terms (not scalable);
wenzelm
parents:
70909
diff
changeset

284 
val proof0 = 
70915
bd4d37edfee4
clarified expand_proof/expand_name: allow more detailed control via thm_header;
wenzelm
parents:
70914
diff
changeset

285 
if export_standard_proofs then 
bd4d37edfee4
clarified expand_proof/expand_name: allow more detailed control via thm_header;
wenzelm
parents:
70914
diff
changeset

286 
Thm.standard_proof_of {full = true, expand_name = SOME o expand_name thm_id} thm 
70914
05c4c6a99b3f
option to export standardized proof terms (not scalable);
wenzelm
parents:
70909
diff
changeset

287 
else if Proofterm.export_enabled () then Thm.reconstruct_proof_of thm 
05c4c6a99b3f
option to export standardized proof terms (not scalable);
wenzelm
parents:
70909
diff
changeset

288 
else MinProof; 
70884  289 
val (prop, SOME proof) = 
70914
05c4c6a99b3f
option to export standardized proof terms (not scalable);
wenzelm
parents:
70909
diff
changeset

290 
standard_prop Name.context (Thm.extra_shyps thm) (Thm.full_prop_of thm) (SOME proof0); 
70909  291 
val _ = Proofterm.commit_proof proof; 
70597  292 
in 
70896  293 
(prop, (deps, (boxes, proof))) > 
70843
cc987440d776
more compact XML: separate environment for free variables;
wenzelm
parents:
70829
diff
changeset

294 
let 
cc987440d776
more compact XML: separate environment for free variables;
wenzelm
parents:
70829
diff
changeset

295 
open XML.Encode Term_XML.Encode; 
70896  296 
fun encode_box {serial, theory_name} = pair int string (serial, theory_name); 
70843
cc987440d776
more compact XML: separate environment for free variables;
wenzelm
parents:
70829
diff
changeset

297 
val encode_proof = Proofterm.encode_standard_proof consts; 
70896  298 
in pair encode_prop (pair (list string) (pair (list encode_box) encode_proof)) end 
70597  299 
end; 
68208  300 

70904  301 
fun buffer_export_thm (thm_id, thm_name) = 
70601
79831e40e2be
more scalable: avoid huge intermediate XML elems;
wenzelm
parents:
70597
diff
changeset

302 
let 
70904  303 
val markup = entity_markup_thm (#serial thm_id, thm_name); 
70914
05c4c6a99b3f
option to export standardized proof terms (not scalable);
wenzelm
parents:
70909
diff
changeset

304 
val thm = Global_Theory.get_thm_name thy (thm_name, Position.none); 
70915
bd4d37edfee4
clarified expand_proof/expand_name: allow more detailed control via thm_header;
wenzelm
parents:
70914
diff
changeset

305 
val body = encode_thm thm_id thm; 
70601
79831e40e2be
more scalable: avoid huge intermediate XML elems;
wenzelm
parents:
70597
diff
changeset

306 
in YXML.buffer (XML.Elem (markup, body)) end; 
70579
5a8e3e4b3760
clarified export of axioms and theorems (identified derivations instead of projected facts);
wenzelm
parents:
70541
diff
changeset

307 

70601
79831e40e2be
more scalable: avoid huge intermediate XML elems;
wenzelm
parents:
70597
diff
changeset

308 
val _ = 
79831e40e2be
more scalable: avoid huge intermediate XML elems;
wenzelm
parents:
70597
diff
changeset

309 
Buffer.empty 
79831e40e2be
more scalable: avoid huge intermediate XML elems;
wenzelm
parents:
70597
diff
changeset

310 
> fold buffer_export_thm (Global_Theory.dest_thm_names thy) 
79831e40e2be
more scalable: avoid huge intermediate XML elems;
wenzelm
parents:
70597
diff
changeset

311 
> export_buffer thy "thms"; 
68232  312 

68264  313 

314 
(* type classes *) 

315 

316 
val encode_class = 

317 
let open XML.Encode Term_XML.Encode 

70534
fb876ebbf5a7
export facts with reconstructed proof term (if possible), but its PThm boxes need to be collected separately;
wenzelm
parents:
70529
diff
changeset

318 
in pair (list (pair string typ)) (list (encode_axiom Name.context)) end; 
68264  319 

320 
fun export_class name = 

321 
(case try (Axclass.get_info thy) name of 

322 
NONE => ([], []) 

70534
fb876ebbf5a7
export facts with reconstructed proof term (if possible), but its PThm boxes need to be collected separately;
wenzelm
parents:
70529
diff
changeset

323 
 SOME {params, axioms, ...} => (params, map (Thm.plain_prop_of o clean_thm) axioms)) 
68264  324 
> encode_class > SOME; 
325 

326 
val _ = 

327 
export_entities "classes" (fn name => fn () => export_class name) 

328 
Sign.class_space (map (rpair ()) (Graph.keys (Sorts.classes_of (#2 (#classes rep_tsig))))); 

329 

68295  330 

331 
(* sort algebra *) 

332 

70386  333 
local 
334 
val prop = encode_axiom Name.context o Logic.varify_global; 

68295  335 

70386  336 
val encode_classrel = 
337 
let open XML.Encode 

338 
in list (pair prop (pair string string)) end; 

70384
8ce08b154aa1
clarified export of sort algebra: avoid logical operations in Isabelle/Scala;
wenzelm
parents:
70015
diff
changeset

339 

70386  340 
val encode_arities = 
341 
let open XML.Encode Term_XML.Encode 

342 
in list (pair prop (triple string (list sort) string)) end; 

343 
in 

344 
val export_classrel = 

345 
maps (fn (c, cs) => map (pair c) cs) #> map (`Logic.mk_classrel) #> encode_classrel; 

68295  346 

70386  347 
val export_arities = map (`Logic.mk_arity) #> encode_arities; 
70384
8ce08b154aa1
clarified export of sort algebra: avoid logical operations in Isabelle/Scala;
wenzelm
parents:
70015
diff
changeset

348 

70386  349 
val {classrel, arities} = 
350 
Sorts.dest_algebra (map (#2 o #classes o Type.rep_tsig o Sign.tsig_of) parents) 

351 
(#2 (#classes rep_tsig)); 

352 
end; 

70384
8ce08b154aa1
clarified export of sort algebra: avoid logical operations in Isabelle/Scala;
wenzelm
parents:
70015
diff
changeset

353 

8ce08b154aa1
clarified export of sort algebra: avoid logical operations in Isabelle/Scala;
wenzelm
parents:
70015
diff
changeset

354 
val _ = if null classrel then () else export_body thy "classrel" (export_classrel classrel); 
8ce08b154aa1
clarified export of sort algebra: avoid logical operations in Isabelle/Scala;
wenzelm
parents:
70015
diff
changeset

355 
val _ = if null arities then () else export_body thy "arities" (export_arities arities); 
68295  356 

68862  357 

358 
(* locales *) 

359 

69023
cef000855cf4
clarified standardization of variables, with proper treatment of local variables;
wenzelm
parents:
69019
diff
changeset

360 
fun encode_locale used = 
69076  361 
let open XML.Encode Term_XML.Encode in 
69077
11529ae45786
more approximative prefix syntax, including binder;
wenzelm
parents:
69076
diff
changeset

362 
triple (list (pair string sort)) (list (pair (pair string typ) encode_syntax)) 
69076  363 
(list (encode_axiom used)) 
364 
end; 

69023
cef000855cf4
clarified standardization of variables, with proper treatment of local variables;
wenzelm
parents:
69019
diff
changeset

365 

69029
aec64b88e708
clarified locale content: proper args with types for interpretation/axioms and typargs derived from the result;
wenzelm
parents:
69028
diff
changeset

366 
fun export_locale loc = 
68864  367 
let 
69034  368 
val {typargs, args, axioms} = locale_content thy loc; 
69076  369 
val used = fold Name.declare (map #1 typargs @ map (#1 o #1) args) Name.context; 
69027  370 
in encode_locale used (typargs, args, axioms) end 
371 
handle ERROR msg => 

372 
cat_error msg ("The error(s) above occurred in locale " ^ 

373 
quote (Locale.markup_name thy_ctxt loc)); 

68862  374 

375 
val _ = 

69029
aec64b88e708
clarified locale content: proper args with types for interpretation/axioms and typargs derived from the result;
wenzelm
parents:
69028
diff
changeset

376 
export_entities "locales" (fn loc => fn () => SOME (export_locale loc)) 
69087
06017b2c4552
suppress aux. locales from command 'experiment'  avoid crash of theory Dict_Construction.Test_Dict_Construction (AFP);
wenzelm
parents:
69086
diff
changeset

377 
Locale.locale_space (get_locales thy); 
68862  378 

68900
1145b25c53de
more robust: parents are strict in Export_Theory.read_theory and thus approximate "commit" of exports;
wenzelm
parents:
68864
diff
changeset

379 

69069
b9aca3b9619f
export locale dependencies, with approx. morphism as type/term substitution;
wenzelm
parents:
69034
diff
changeset

380 
(* locale dependencies *) 
b9aca3b9619f
export locale dependencies, with approx. morphism as type/term substitution;
wenzelm
parents:
69034
diff
changeset

381 

69087
06017b2c4552
suppress aux. locales from command 'experiment'  avoid crash of theory Dict_Construction.Test_Dict_Construction (AFP);
wenzelm
parents:
69086
diff
changeset

382 
fun encode_locale_dependency (dep: Locale.locale_dependency, subst) = 
06017b2c4552
suppress aux. locales from command 'experiment'  avoid crash of theory Dict_Construction.Test_Dict_Construction (AFP);
wenzelm
parents:
69086
diff
changeset

383 
(#source dep, (#target dep, (#prefix dep, subst))) > 
69069
b9aca3b9619f
export locale dependencies, with approx. morphism as type/term substitution;
wenzelm
parents:
69034
diff
changeset

384 
let 
b9aca3b9619f
export locale dependencies, with approx. morphism as type/term substitution;
wenzelm
parents:
69034
diff
changeset

385 
open XML.Encode Term_XML.Encode; 
b9aca3b9619f
export locale dependencies, with approx. morphism as type/term substitution;
wenzelm
parents:
69034
diff
changeset

386 
val encode_subst = 
70784
799437173553
Term_XML.Encode/Decode.term uses Const "typargs";
wenzelm
parents:
70605
diff
changeset

387 
pair (list (pair (pair string sort) typ)) (list (pair (pair string typ) (term consts))); 
69069
b9aca3b9619f
export locale dependencies, with approx. morphism as type/term substitution;
wenzelm
parents:
69034
diff
changeset

388 
in pair string (pair string (pair (list (pair string bool)) encode_subst)) end; 
b9aca3b9619f
export locale dependencies, with approx. morphism as type/term substitution;
wenzelm
parents:
69034
diff
changeset

389 

b9aca3b9619f
export locale dependencies, with approx. morphism as type/term substitution;
wenzelm
parents:
69034
diff
changeset

390 
val _ = 
70601
79831e40e2be
more scalable: avoid huge intermediate XML elems;
wenzelm
parents:
70597
diff
changeset

391 
get_dependencies parents thy 
79831e40e2be
more scalable: avoid huge intermediate XML elems;
wenzelm
parents:
70597
diff
changeset

392 
> map_index (fn (i, dep) => 
79831e40e2be
more scalable: avoid huge intermediate XML elems;
wenzelm
parents:
70597
diff
changeset

393 
let 
79831e40e2be
more scalable: avoid huge intermediate XML elems;
wenzelm
parents:
70597
diff
changeset

394 
val xname = string_of_int (i + 1); 
79831e40e2be
more scalable: avoid huge intermediate XML elems;
wenzelm
parents:
70597
diff
changeset

395 
val name = Long_Name.implode [Context.theory_name thy, xname]; 
79831e40e2be
more scalable: avoid huge intermediate XML elems;
wenzelm
parents:
70597
diff
changeset

396 
val markup = make_entity_markup name xname (#pos (#1 dep)) (#serial (#1 dep)); 
79831e40e2be
more scalable: avoid huge intermediate XML elems;
wenzelm
parents:
70597
diff
changeset

397 
val body = encode_locale_dependency dep; 
79831e40e2be
more scalable: avoid huge intermediate XML elems;
wenzelm
parents:
70597
diff
changeset

398 
in XML.Elem (markup, body) end) 
79831e40e2be
more scalable: avoid huge intermediate XML elems;
wenzelm
parents:
70597
diff
changeset

399 
> export_body thy "locale_dependencies"; 
69069
b9aca3b9619f
export locale dependencies, with approx. morphism as type/term substitution;
wenzelm
parents:
69034
diff
changeset

400 

b9aca3b9619f
export locale dependencies, with approx. morphism as type/term substitution;
wenzelm
parents:
69034
diff
changeset

401 

68900
1145b25c53de
more robust: parents are strict in Export_Theory.read_theory and thus approximate "commit" of exports;
wenzelm
parents:
68864
diff
changeset

402 
(* parents *) 
1145b25c53de
more robust: parents are strict in Export_Theory.read_theory and thus approximate "commit" of exports;
wenzelm
parents:
68864
diff
changeset

403 

1145b25c53de
more robust: parents are strict in Export_Theory.read_theory and thus approximate "commit" of exports;
wenzelm
parents:
68864
diff
changeset

404 
val _ = 
70601
79831e40e2be
more scalable: avoid huge intermediate XML elems;
wenzelm
parents:
70597
diff
changeset

405 
Export.export thy \<^path_binding>\<open>theory/parents\<close> 
79831e40e2be
more scalable: avoid huge intermediate XML elems;
wenzelm
parents:
70597
diff
changeset

406 
[YXML.string_of_body (XML.Encode.string (cat_lines (map Context.theory_long_name parents)))]; 
68900
1145b25c53de
more robust: parents are strict in Export_Theory.read_theory and thus approximate "commit" of exports;
wenzelm
parents:
68864
diff
changeset

407 

68295  408 
in () end); 
68165  409 

410 
end; 