author  wenzelm 
Wed, 21 Aug 2019 17:32:44 +0200  
changeset 70601  79831e40e2be 
parent 70597  a896257a3f07 
child 70604  8088cf2576f3 
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 

199 
val encode_const = 

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

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

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

202 
(pair (list string) 
8f2d3a27aff0
more informative Spec_Rules.Equational: support corecursion;
wenzelm
parents:
69992
diff
changeset

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

204 
end; 
68165  205 

68201  206 
fun export_const c (T, abbrev) = 
207 
let 

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

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

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

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

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

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

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

215 
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

216 
in encode_const (syntax, (args, (U0, (abbrev', (propositional, recursion))))) end; 
68165  217 

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

219 
export_entities "consts" (SOME oo export_const) Sign.const_space 
68201  220 
(#constants (Consts.dest (Sign.consts_of thy))); 
221 

68208  222 

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

223 
(* axioms *) 
68208  224 

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

225 
fun standard_prop used extra_shyps raw_prop raw_proof = 
68727  226 
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

227 
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

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

229 
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

230 
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

231 
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

232 
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

233 

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 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

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

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

237 

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

238 
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

239 
encode_prop (#1 (standard_prop used [] prop NONE)); 
68208  240 

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

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

242 
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

243 
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

244 

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

245 

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

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

247 

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

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

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

250 
#> Thm.check_hyps (Context.Theory thy) 
fb876ebbf5a7
export facts with reconstructed proof term (if possible), but its PThm boxes need to be collected separately;
wenzelm
parents:
70529
diff
changeset

251 
#> Thm.strip_shyps; 
69023
cef000855cf4
clarified standardization of variables, with proper treatment of local variables;
wenzelm
parents:
69019
diff
changeset

252 

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

253 
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

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

255 
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

256 
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

257 
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

258 
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

259 

70597  260 
fun encode_thm raw_thm = 
261 
let 

262 
val deps = map (Thm_Name.print o #2) (Thm_Deps.thm_deps thy raw_thm); 

263 
val thm = clean_thm raw_thm; 

264 
val (prop, proof) = 

265 
standard_prop Name.context 

266 
(Thm.extra_shyps thm) 

267 
(Thm.full_prop_of thm) 

268 
(try Thm.reconstruct_proof_of thm); 

269 
in 

270 
(prop, (deps, proof)) > 

271 
let open XML.Encode Term_XML.Encode 

272 
in pair encode_prop (pair (list string) (option Proofterm.encode_full)) end 

273 
end; 

68208  274 

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

275 
fun buffer_export_thm (serial, thm_name) = 
79831e40e2be
more scalable: avoid huge intermediate XML elems;
wenzelm
parents:
70597
diff
changeset

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

277 
val markup = entity_markup_thm (serial, thm_name); 
79831e40e2be
more scalable: avoid huge intermediate XML elems;
wenzelm
parents:
70597
diff
changeset

278 
val body = encode_thm (Global_Theory.get_thm_name thy (thm_name, Position.none)); 
79831e40e2be
more scalable: avoid huge intermediate XML elems;
wenzelm
parents:
70597
diff
changeset

279 
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

280 

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

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

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

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

284 
> export_buffer thy "thms"; 
68232  285 

68264  286 

287 
(* type classes *) 

288 

289 
val encode_class = 

290 
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

291 
in pair (list (pair string typ)) (list (encode_axiom Name.context)) end; 
68264  292 

293 
fun export_class name = 

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

295 
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

296 
 SOME {params, axioms, ...} => (params, map (Thm.plain_prop_of o clean_thm) axioms)) 
68264  297 
> encode_class > SOME; 
298 

299 
val _ = 

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

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

302 

68295  303 

304 
(* sort algebra *) 

305 

70386  306 
local 
307 
val prop = encode_axiom Name.context o Logic.varify_global; 

68295  308 

70386  309 
val encode_classrel = 
310 
let open XML.Encode 

311 
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

312 

70386  313 
val encode_arities = 
314 
let open XML.Encode Term_XML.Encode 

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

316 
in 

317 
val export_classrel = 

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

68295  319 

70386  320 
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

321 

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

324 
(#2 (#classes rep_tsig)); 

325 
end; 

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

326 

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

327 
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

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

68862  330 

331 
(* locales *) 

332 

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

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

335 
triple (list (pair string sort)) (list (pair (pair string typ) encode_syntax)) 
69076  336 
(list (encode_axiom used)) 
337 
end; 

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

338 

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

339 
fun export_locale loc = 
68864  340 
let 
69034  341 
val {typargs, args, axioms} = locale_content thy loc; 
69076  342 
val used = fold Name.declare (map #1 typargs @ map (#1 o #1) args) Name.context; 
69027  343 
in encode_locale used (typargs, args, axioms) end 
344 
handle ERROR msg => 

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

346 
quote (Locale.markup_name thy_ctxt loc)); 

68862  347 

348 
val _ = 

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

349 
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

350 
Locale.locale_space (get_locales thy); 
68862  351 

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

352 

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

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

354 

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

355 
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

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

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

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

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

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

361 
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

362 

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

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

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

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

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

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

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

369 
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

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

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

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

373 

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

374 

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

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

376 

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

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

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

379 
[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

380 

68295  381 
in () end); 
68165  382 

383 
end; 