author  haftmann 
Sun, 23 Feb 2014 10:33:43 +0100  
changeset 55683  5732a55b9232 
parent 55304  55ac31bc08a4 
child 55684  ee49b4f7edc8 
permissions  rwrr 
39401  1 
(* Title: Tools/Code/code_runtime.ML 
28054  2 
Author: Florian Haftmann, TU Muenchen 
3 

34028
1e6206763036
split off evaluation mechanisms in separte module Code_Eval
haftmann
parents:
33992
diff
changeset

4 
Runtime services building on code generation into implementation language SML. 
28054  5 
*) 
6 

39401  7 
signature CODE_RUNTIME = 
28054  8 
sig 
34028
1e6206763036
split off evaluation mechanisms in separte module Code_Eval
haftmann
parents:
33992
diff
changeset

9 
val target: string 
39912
2ffe7060ca75
avoid antiquotation processing for code_reflect; moved ML_Context.value to Code_Runtime
haftmann
parents:
39816
diff
changeset

10 
val value: Proof.context > 
2ffe7060ca75
avoid antiquotation processing for code_reflect; moved ML_Context.value to Code_Runtime
haftmann
parents:
39816
diff
changeset

11 
(Proof.context > unit > 'a) * ((unit > 'a) > Proof.context > Proof.context) * string > 
2ffe7060ca75
avoid antiquotation processing for code_reflect; moved ML_Context.value to Code_Runtime
haftmann
parents:
39816
diff
changeset

12 
string * string > 'a 
39473
33638f4883ac
dynamic and static value computation; builtin evaluation of propositions
haftmann
parents:
39422
diff
changeset

13 
type 'a cookie = (Proof.context > unit > 'a) * ((unit > 'a) > Proof.context > Proof.context) * string 
33638f4883ac
dynamic and static value computation; builtin evaluation of propositions
haftmann
parents:
39422
diff
changeset

14 
val dynamic_value: 'a cookie > theory > string option 
33638f4883ac
dynamic and static value computation; builtin evaluation of propositions
haftmann
parents:
39422
diff
changeset

15 
> ((term > term) > 'a > 'a) > term > string list > 'a option 
33638f4883ac
dynamic and static value computation; builtin evaluation of propositions
haftmann
parents:
39422
diff
changeset

16 
val dynamic_value_strict: 'a cookie > theory > string option 
33638f4883ac
dynamic and static value computation; builtin evaluation of propositions
haftmann
parents:
39422
diff
changeset

17 
> ((term > term) > 'a > 'a) > term > string list > 'a 
33638f4883ac
dynamic and static value computation; builtin evaluation of propositions
haftmann
parents:
39422
diff
changeset

18 
val dynamic_value_exn: 'a cookie > theory > string option 
33638f4883ac
dynamic and static value computation; builtin evaluation of propositions
haftmann
parents:
39422
diff
changeset

19 
> ((term > term) > 'a > 'a) > term > string list > 'a Exn.result 
33638f4883ac
dynamic and static value computation; builtin evaluation of propositions
haftmann
parents:
39422
diff
changeset

20 
val static_value: 'a cookie > theory > string option 
33638f4883ac
dynamic and static value computation; builtin evaluation of propositions
haftmann
parents:
39422
diff
changeset

21 
> ((term > term) > 'a > 'a) > string list > term > 'a option 
33638f4883ac
dynamic and static value computation; builtin evaluation of propositions
haftmann
parents:
39422
diff
changeset

22 
val static_value_strict: 'a cookie > theory > string option 
33638f4883ac
dynamic and static value computation; builtin evaluation of propositions
haftmann
parents:
39422
diff
changeset

23 
> ((term > term) > 'a > 'a) > string list > term > 'a 
33638f4883ac
dynamic and static value computation; builtin evaluation of propositions
haftmann
parents:
39422
diff
changeset

24 
val static_value_exn: 'a cookie > theory > string option 
33638f4883ac
dynamic and static value computation; builtin evaluation of propositions
haftmann
parents:
39422
diff
changeset

25 
> ((term > term) > 'a > 'a) > string list > term > 'a Exn.result 
41247  26 
val dynamic_holds_conv: theory > conv 
39473
33638f4883ac
dynamic and static value computation; builtin evaluation of propositions
haftmann
parents:
39422
diff
changeset

27 
val static_holds_conv: theory > string list > conv 
40421
b41aabb629ce
constructors to datatypes in code_reflect can be globbed; dropped unused code
haftmann
parents:
40320
diff
changeset

28 
val code_reflect: (string * string list option) list > string list > string 
b41aabb629ce
constructors to datatypes in code_reflect can be globbed; dropped unused code
haftmann
parents:
40320
diff
changeset

29 
> string option > theory > theory 
39473
33638f4883ac
dynamic and static value computation; builtin evaluation of propositions
haftmann
parents:
39422
diff
changeset

30 
datatype truth = Holds 
33638f4883ac
dynamic and static value computation; builtin evaluation of propositions
haftmann
parents:
39422
diff
changeset

31 
val put_truth: (unit > truth) > Proof.context > Proof.context 
40150  32 
val trace: bool Unsynchronized.ref 
39816
c7cec137c48a
added polyml_as_definition  using external SML files as substitute for proper definitions  only for polyml!
haftmann
parents:
39605
diff
changeset

33 
val polyml_as_definition: (binding * typ) list > Path.T list > theory > theory 
28054  34 
end; 
35 

39401  36 
structure Code_Runtime : CODE_RUNTIME = 
28054  37 
struct 
38 

55150  39 
open Basic_Code_Symbol; 
39473
33638f4883ac
dynamic and static value computation; builtin evaluation of propositions
haftmann
parents:
39422
diff
changeset

40 
open Basic_Code_Thingol; 
33638f4883ac
dynamic and static value computation; builtin evaluation of propositions
haftmann
parents:
39422
diff
changeset

41 

39404
a8c337299bc1
Code_Runtime.value, corresponding to ML_Context.value; tuned
haftmann
parents:
39401
diff
changeset

42 
(** evaluation **) 
33992  43 

39473
33638f4883ac
dynamic and static value computation; builtin evaluation of propositions
haftmann
parents:
39422
diff
changeset

44 
(* technical prerequisites *) 
33638f4883ac
dynamic and static value computation; builtin evaluation of propositions
haftmann
parents:
39422
diff
changeset

45 

33638f4883ac
dynamic and static value computation; builtin evaluation of propositions
haftmann
parents:
39422
diff
changeset

46 
val this = "Code_Runtime"; 
33638f4883ac
dynamic and static value computation; builtin evaluation of propositions
haftmann
parents:
39422
diff
changeset

47 
val s_truth = Long_Name.append this "truth"; 
33638f4883ac
dynamic and static value computation; builtin evaluation of propositions
haftmann
parents:
39422
diff
changeset

48 
val s_Holds = Long_Name.append this "Holds"; 
33638f4883ac
dynamic and static value computation; builtin evaluation of propositions
haftmann
parents:
39422
diff
changeset

49 

34028
1e6206763036
split off evaluation mechanisms in separte module Code_Eval
haftmann
parents:
33992
diff
changeset

50 
val target = "Eval"; 
44663  51 
val structure_generated = "Generated_Code"; 
28054  52 

39473
33638f4883ac
dynamic and static value computation; builtin evaluation of propositions
haftmann
parents:
39422
diff
changeset

53 
datatype truth = Holds; 
39422  54 

53171  55 
val _ = Theory.setup 
55147
bce3dbc11f95
prefer explicit code symbol type over adhoc name mangling
haftmann
parents:
53171
diff
changeset

56 
(Code_Target.extend_target (target, (Code_ML.target_SML, I)) 
55150  57 
#> Code_Target.set_printings (Type_Constructor (@{type_name prop}, 
52435
6646bb548c6b
migration from code_(consttypeclassinstance) to code_printing and from code_module to code_identifier
haftmann
parents:
52434
diff
changeset

58 
[(target, SOME (0, (K o K o K) (Code_Printer.str s_truth)))])) 
55150  59 
#> Code_Target.set_printings (Constant (@{const_name Code_Generator.holds}, 
52435
6646bb548c6b
migration from code_(consttypeclassinstance) to code_printing and from code_module to code_identifier
haftmann
parents:
52434
diff
changeset

60 
[(target, SOME (Code_Printer.plain_const_syntax s_Holds))])) 
39473
33638f4883ac
dynamic and static value computation; builtin evaluation of propositions
haftmann
parents:
39422
diff
changeset

61 
#> Code_Target.add_reserved target this 
53171  62 
#> fold (Code_Target.add_reserved target) ["oo", "ooo", "oooo", "upto", "downto", "orf", "andf"]); 
39485
f7270a5e2550
closures preserve static serializer context for static evaluation; tuned
haftmann
parents:
39482
diff
changeset

63 
(*avoid further pervasive infix names*) 
39473
33638f4883ac
dynamic and static value computation; builtin evaluation of propositions
haftmann
parents:
39422
diff
changeset

64 

40150  65 
val trace = Unsynchronized.ref false; 
66 

39912
2ffe7060ca75
avoid antiquotation processing for code_reflect; moved ML_Context.value to Code_Runtime
haftmann
parents:
39816
diff
changeset

67 
fun exec verbose code = 
40150  68 
(if ! trace then tracing code else (); 
40257  69 
ML_Context.exec (fn () => Secure.use_text ML_Env.local_context (0, "generated code") verbose code)); 
39912
2ffe7060ca75
avoid antiquotation processing for code_reflect; moved ML_Context.value to Code_Runtime
haftmann
parents:
39816
diff
changeset

70 

2ffe7060ca75
avoid antiquotation processing for code_reflect; moved ML_Context.value to Code_Runtime
haftmann
parents:
39816
diff
changeset

71 
fun value ctxt (get, put, put_ml) (prelude, value) = 
2ffe7060ca75
avoid antiquotation processing for code_reflect; moved ML_Context.value to Code_Runtime
haftmann
parents:
39816
diff
changeset

72 
let 
2ffe7060ca75
avoid antiquotation processing for code_reflect; moved ML_Context.value to Code_Runtime
haftmann
parents:
39816
diff
changeset

73 
val code = (prelude 
2ffe7060ca75
avoid antiquotation processing for code_reflect; moved ML_Context.value to Code_Runtime
haftmann
parents:
39816
diff
changeset

74 
^ "\nval _ = Context.set_thread_data (SOME (Context.map_proof (" ^ put_ml 
2ffe7060ca75
avoid antiquotation processing for code_reflect; moved ML_Context.value to Code_Runtime
haftmann
parents:
39816
diff
changeset

75 
^ " (fn () => " ^ value ^ ")) (ML_Context.the_generic_context ())))"); 
2ffe7060ca75
avoid antiquotation processing for code_reflect; moved ML_Context.value to Code_Runtime
haftmann
parents:
39816
diff
changeset

76 
val ctxt' = ctxt 
2ffe7060ca75
avoid antiquotation processing for code_reflect; moved ML_Context.value to Code_Runtime
haftmann
parents:
39816
diff
changeset

77 
> put (fn () => error ("Bad evaluation for " ^ quote put_ml)) 
2ffe7060ca75
avoid antiquotation processing for code_reflect; moved ML_Context.value to Code_Runtime
haftmann
parents:
39816
diff
changeset

78 
> Context.proof_map (exec false code); 
2ffe7060ca75
avoid antiquotation processing for code_reflect; moved ML_Context.value to Code_Runtime
haftmann
parents:
39816
diff
changeset

79 
in get ctxt' () end; 
2ffe7060ca75
avoid antiquotation processing for code_reflect; moved ML_Context.value to Code_Runtime
haftmann
parents:
39816
diff
changeset

80 

39473
33638f4883ac
dynamic and static value computation; builtin evaluation of propositions
haftmann
parents:
39422
diff
changeset

81 

33638f4883ac
dynamic and static value computation; builtin evaluation of propositions
haftmann
parents:
39422
diff
changeset

82 
(* evaluation into target language values *) 
33638f4883ac
dynamic and static value computation; builtin evaluation of propositions
haftmann
parents:
39422
diff
changeset

83 

33638f4883ac
dynamic and static value computation; builtin evaluation of propositions
haftmann
parents:
39422
diff
changeset

84 
type 'a cookie = (Proof.context > unit > 'a) * ((unit > 'a) > Proof.context > Proof.context) * string; 
33638f4883ac
dynamic and static value computation; builtin evaluation of propositions
haftmann
parents:
39422
diff
changeset

85 

39605  86 
fun reject_vars thy t = 
87 
let 

42361  88 
val ctxt = Proof_Context.init_global thy; 
39605  89 
in ((Sign.no_frees ctxt o Sign.no_vars ctxt o map_types (K dummyT)) t; t) end; 
90 

55147
bce3dbc11f95
prefer explicit code symbol type over adhoc name mangling
haftmann
parents:
53171
diff
changeset

91 
fun obtain_evaluator thy some_target program consts expr = 
bce3dbc11f95
prefer explicit code symbol type over adhoc name mangling
haftmann
parents:
53171
diff
changeset

92 
Code_Target.evaluator thy (the_default target some_target) program consts expr 
48568  93 
> apfst (fn ml_modules => space_implode "\n\n" (map snd ml_modules)); 
39485
f7270a5e2550
closures preserve static serializer context for static evaluation; tuned
haftmann
parents:
39482
diff
changeset

94 

55147
bce3dbc11f95
prefer explicit code symbol type over adhoc name mangling
haftmann
parents:
53171
diff
changeset

95 
fun obtain_evaluator' thy some_target program = 
55150  96 
obtain_evaluator thy some_target program o map Constant; 
55147
bce3dbc11f95
prefer explicit code symbol type over adhoc name mangling
haftmann
parents:
53171
diff
changeset

97 

41347
064133cb4ef6
evaluator separating static and dynamic operations
haftmann
parents:
41343
diff
changeset

98 
fun evaluation cookie thy evaluator vs_t args = 
39404
a8c337299bc1
Code_Runtime.value, corresponding to ML_Context.value; tuned
haftmann
parents:
39401
diff
changeset

99 
let 
42361  100 
val ctxt = Proof_Context.init_global thy; 
41347
064133cb4ef6
evaluator separating static and dynamic operations
haftmann
parents:
41343
diff
changeset

101 
val (program_code, value_name) = evaluator vs_t; 
39473
33638f4883ac
dynamic and static value computation; builtin evaluation of propositions
haftmann
parents:
39422
diff
changeset

102 
val value_code = space_implode " " 
41347
064133cb4ef6
evaluator separating static and dynamic operations
haftmann
parents:
41343
diff
changeset

103 
(value_name :: "()" :: map (enclose "(" ")") args); 
40235
87998864284e
use Exn.interruptible_capture to keep usercode interruptible (Exn.capture not immediately followed by Exn.release here);
wenzelm
parents:
40150
diff
changeset

104 
in Exn.interruptible_capture (value ctxt cookie) (program_code, value_code) end; 
39473
33638f4883ac
dynamic and static value computation; builtin evaluation of propositions
haftmann
parents:
39422
diff
changeset

105 

33638f4883ac
dynamic and static value computation; builtin evaluation of propositions
haftmann
parents:
39422
diff
changeset

106 
fun partiality_as_none e = SOME (Exn.release e) 
33638f4883ac
dynamic and static value computation; builtin evaluation of propositions
haftmann
parents:
39422
diff
changeset

107 
handle General.Match => NONE 
33638f4883ac
dynamic and static value computation; builtin evaluation of propositions
haftmann
parents:
39422
diff
changeset

108 
 General.Bind => NONE 
33638f4883ac
dynamic and static value computation; builtin evaluation of propositions
haftmann
parents:
39422
diff
changeset

109 
 General.Fail _ => NONE; 
33638f4883ac
dynamic and static value computation; builtin evaluation of propositions
haftmann
parents:
39422
diff
changeset

110 

33638f4883ac
dynamic and static value computation; builtin evaluation of propositions
haftmann
parents:
39422
diff
changeset

111 
fun dynamic_value_exn cookie thy some_target postproc t args = 
33638f4883ac
dynamic and static value computation; builtin evaluation of propositions
haftmann
parents:
39422
diff
changeset

112 
let 
39605  113 
val _ = reject_vars thy t; 
41099  114 
val _ = if ! trace 
115 
then tracing ("Evaluation of term " ^ quote (Syntax.string_of_term_global thy t)) 

116 
else () 

55147
bce3dbc11f95
prefer explicit code symbol type over adhoc name mangling
haftmann
parents:
53171
diff
changeset

117 
fun evaluator program ((_, vs_ty), t) deps = 
bce3dbc11f95
prefer explicit code symbol type over adhoc name mangling
haftmann
parents:
53171
diff
changeset

118 
evaluation cookie thy (obtain_evaluator thy some_target program deps) (vs_ty, t) args; 
41184  119 
in Code_Thingol.dynamic_value thy (Exn.map_result o postproc) evaluator t end; 
39473
33638f4883ac
dynamic and static value computation; builtin evaluation of propositions
haftmann
parents:
39422
diff
changeset

120 

33638f4883ac
dynamic and static value computation; builtin evaluation of propositions
haftmann
parents:
39422
diff
changeset

121 
fun dynamic_value_strict cookie thy some_target postproc t args = 
33638f4883ac
dynamic and static value computation; builtin evaluation of propositions
haftmann
parents:
39422
diff
changeset

122 
Exn.release (dynamic_value_exn cookie thy some_target postproc t args); 
33638f4883ac
dynamic and static value computation; builtin evaluation of propositions
haftmann
parents:
39422
diff
changeset

123 

33638f4883ac
dynamic and static value computation; builtin evaluation of propositions
haftmann
parents:
39422
diff
changeset

124 
fun dynamic_value cookie thy some_target postproc t args = 
33638f4883ac
dynamic and static value computation; builtin evaluation of propositions
haftmann
parents:
39422
diff
changeset

125 
partiality_as_none (dynamic_value_exn cookie thy some_target postproc t args); 
33638f4883ac
dynamic and static value computation; builtin evaluation of propositions
haftmann
parents:
39422
diff
changeset

126 

55147
bce3dbc11f95
prefer explicit code symbol type over adhoc name mangling
haftmann
parents:
53171
diff
changeset

127 
fun static_evaluator cookie thy some_target program consts' = 
39473
33638f4883ac
dynamic and static value computation; builtin evaluation of propositions
haftmann
parents:
39422
diff
changeset

128 
let 
55147
bce3dbc11f95
prefer explicit code symbol type over adhoc name mangling
haftmann
parents:
53171
diff
changeset

129 
val evaluator = obtain_evaluator' thy some_target program consts' 
41347
064133cb4ef6
evaluator separating static and dynamic operations
haftmann
parents:
41343
diff
changeset

130 
in fn ((_, vs_ty), t) => fn _ => evaluation cookie thy evaluator (vs_ty, t) [] end; 
39473
33638f4883ac
dynamic and static value computation; builtin evaluation of propositions
haftmann
parents:
39422
diff
changeset

131 

41347
064133cb4ef6
evaluator separating static and dynamic operations
haftmann
parents:
41343
diff
changeset

132 
fun static_value_exn cookie thy some_target postproc consts = 
064133cb4ef6
evaluator separating static and dynamic operations
haftmann
parents:
41343
diff
changeset

133 
Code_Thingol.static_value thy (Exn.map_result o postproc) consts 
064133cb4ef6
evaluator separating static and dynamic operations
haftmann
parents:
41343
diff
changeset

134 
(static_evaluator cookie thy some_target) o reject_vars thy; 
39473
33638f4883ac
dynamic and static value computation; builtin evaluation of propositions
haftmann
parents:
39422
diff
changeset

135 

41347
064133cb4ef6
evaluator separating static and dynamic operations
haftmann
parents:
41343
diff
changeset

136 
fun static_value_strict cookie thy some_target postproc consts = 
064133cb4ef6
evaluator separating static and dynamic operations
haftmann
parents:
41343
diff
changeset

137 
Exn.release o static_value_exn cookie thy some_target postproc consts; 
064133cb4ef6
evaluator separating static and dynamic operations
haftmann
parents:
41343
diff
changeset

138 

064133cb4ef6
evaluator separating static and dynamic operations
haftmann
parents:
41343
diff
changeset

139 
fun static_value cookie thy some_target postproc consts = 
064133cb4ef6
evaluator separating static and dynamic operations
haftmann
parents:
41343
diff
changeset

140 
partiality_as_none o static_value_exn cookie thy some_target postproc consts; 
39473
33638f4883ac
dynamic and static value computation; builtin evaluation of propositions
haftmann
parents:
39422
diff
changeset

141 

33638f4883ac
dynamic and static value computation; builtin evaluation of propositions
haftmann
parents:
39422
diff
changeset

142 

33638f4883ac
dynamic and static value computation; builtin evaluation of propositions
haftmann
parents:
39422
diff
changeset

143 
(* evaluation for truth or nothing *) 
33638f4883ac
dynamic and static value computation; builtin evaluation of propositions
haftmann
parents:
39422
diff
changeset

144 

39820  145 
structure Truth_Result = Proof_Data 
146 
( 

39473
33638f4883ac
dynamic and static value computation; builtin evaluation of propositions
haftmann
parents:
39422
diff
changeset

147 
type T = unit > truth 
41472
f6ab14e61604
misc tuning and comments based on review of Theory_Data, Proof_Data, Generic_Data usage;
wenzelm
parents:
41376
diff
changeset

148 
(* FIXME avoid user error with nonuser text *) 
39473
33638f4883ac
dynamic and static value computation; builtin evaluation of propositions
haftmann
parents:
39422
diff
changeset

149 
fun init _ () = error "Truth_Result" 
33638f4883ac
dynamic and static value computation; builtin evaluation of propositions
haftmann
parents:
39422
diff
changeset

150 
); 
33638f4883ac
dynamic and static value computation; builtin evaluation of propositions
haftmann
parents:
39422
diff
changeset

151 
val put_truth = Truth_Result.put; 
33638f4883ac
dynamic and static value computation; builtin evaluation of propositions
haftmann
parents:
39422
diff
changeset

152 
val truth_cookie = (Truth_Result.get, put_truth, Long_Name.append this "put_truth"); 
33638f4883ac
dynamic and static value computation; builtin evaluation of propositions
haftmann
parents:
39422
diff
changeset

153 

39605  154 
val reject_vars = fn thy => tap (reject_vars thy o Thm.term_of); 
155 

41349
0e2a3f22f018
evaluator separating static and dynamic operations
haftmann
parents:
41348
diff
changeset

156 
local 
0e2a3f22f018
evaluator separating static and dynamic operations
haftmann
parents:
41348
diff
changeset

157 

47609  158 
fun check_holds thy evaluator vs_t ct = 
39473
33638f4883ac
dynamic and static value computation; builtin evaluation of propositions
haftmann
parents:
39422
diff
changeset

159 
let 
33638f4883ac
dynamic and static value computation; builtin evaluation of propositions
haftmann
parents:
39422
diff
changeset

160 
val t = Thm.term_of ct; 
33638f4883ac
dynamic and static value computation; builtin evaluation of propositions
haftmann
parents:
39422
diff
changeset

161 
val _ = if fastype_of t <> propT 
33638f4883ac
dynamic and static value computation; builtin evaluation of propositions
haftmann
parents:
39422
diff
changeset

162 
then error ("Not a proposition: " ^ Syntax.string_of_term_global thy t) 
33638f4883ac
dynamic and static value computation; builtin evaluation of propositions
haftmann
parents:
39422
diff
changeset

163 
else (); 
33638f4883ac
dynamic and static value computation; builtin evaluation of propositions
haftmann
parents:
39422
diff
changeset

164 
val iff = Thm.cterm_of thy (Term.Const ("==", propT > propT > propT)); 
41349
0e2a3f22f018
evaluator separating static and dynamic operations
haftmann
parents:
41348
diff
changeset

165 
val result = case partiality_as_none (evaluation truth_cookie thy evaluator vs_t []) 
39473
33638f4883ac
dynamic and static value computation; builtin evaluation of propositions
haftmann
parents:
39422
diff
changeset

166 
of SOME Holds => true 
33638f4883ac
dynamic and static value computation; builtin evaluation of propositions
haftmann
parents:
39422
diff
changeset

167 
 _ => false; 
33638f4883ac
dynamic and static value computation; builtin evaluation of propositions
haftmann
parents:
39422
diff
changeset

168 
in 
33638f4883ac
dynamic and static value computation; builtin evaluation of propositions
haftmann
parents:
39422
diff
changeset

169 
Thm.mk_binop iff ct (if result then @{cprop "PROP Code_Generator.holds"} else ct) 
33638f4883ac
dynamic and static value computation; builtin evaluation of propositions
haftmann
parents:
39422
diff
changeset

170 
end; 
33638f4883ac
dynamic and static value computation; builtin evaluation of propositions
haftmann
parents:
39422
diff
changeset

171 

33638f4883ac
dynamic and static value computation; builtin evaluation of propositions
haftmann
parents:
39422
diff
changeset

172 
val (_, raw_check_holds_oracle) = Context.>>> (Context.map_theory_result 
43619
3803869014aa
proper @{binding} antiquotations (relevant for formal references);
wenzelm
parents:
43560
diff
changeset

173 
(Thm.add_oracle (@{binding holds_by_evaluation}, 
47609  174 
fn (thy, evaluator, vs_t, ct) => check_holds thy evaluator vs_t ct))); 
39473
33638f4883ac
dynamic and static value computation; builtin evaluation of propositions
haftmann
parents:
39422
diff
changeset

175 

41349
0e2a3f22f018
evaluator separating static and dynamic operations
haftmann
parents:
41348
diff
changeset

176 
fun check_holds_oracle thy evaluator ((_, vs_ty), t) deps ct = 
47609  177 
raw_check_holds_oracle (thy, evaluator, (vs_ty, t), ct); 
41349
0e2a3f22f018
evaluator separating static and dynamic operations
haftmann
parents:
41348
diff
changeset

178 

0e2a3f22f018
evaluator separating static and dynamic operations
haftmann
parents:
41348
diff
changeset

179 
in 
39485
f7270a5e2550
closures preserve static serializer context for static evaluation; tuned
haftmann
parents:
39482
diff
changeset

180 

41247  181 
fun dynamic_holds_conv thy = Code_Thingol.dynamic_conv thy 
55147
bce3dbc11f95
prefer explicit code symbol type over adhoc name mangling
haftmann
parents:
53171
diff
changeset

182 
(fn program => fn vs_t => fn deps => 
bce3dbc11f95
prefer explicit code symbol type over adhoc name mangling
haftmann
parents:
53171
diff
changeset

183 
check_holds_oracle thy (obtain_evaluator thy NONE program deps) vs_t deps) 
41349
0e2a3f22f018
evaluator separating static and dynamic operations
haftmann
parents:
41348
diff
changeset

184 
o reject_vars thy; 
39473
33638f4883ac
dynamic and static value computation; builtin evaluation of propositions
haftmann
parents:
39422
diff
changeset

185 

41349
0e2a3f22f018
evaluator separating static and dynamic operations
haftmann
parents:
41348
diff
changeset

186 
fun static_holds_conv thy consts = Code_Thingol.static_conv thy consts 
55147
bce3dbc11f95
prefer explicit code symbol type over adhoc name mangling
haftmann
parents:
53171
diff
changeset

187 
(fn program => fn consts' => 
bce3dbc11f95
prefer explicit code symbol type over adhoc name mangling
haftmann
parents:
53171
diff
changeset

188 
check_holds_oracle thy (obtain_evaluator' thy NONE program consts')) 
41349
0e2a3f22f018
evaluator separating static and dynamic operations
haftmann
parents:
41348
diff
changeset

189 
o reject_vars thy; 
0e2a3f22f018
evaluator separating static and dynamic operations
haftmann
parents:
41348
diff
changeset

190 

0e2a3f22f018
evaluator separating static and dynamic operations
haftmann
parents:
41348
diff
changeset

191 
end; (*local*) 
39404
a8c337299bc1
Code_Runtime.value, corresponding to ML_Context.value; tuned
haftmann
parents:
39401
diff
changeset

192 

a8c337299bc1
Code_Runtime.value, corresponding to ML_Context.value; tuned
haftmann
parents:
39401
diff
changeset

193 

a8c337299bc1
Code_Runtime.value, corresponding to ML_Context.value; tuned
haftmann
parents:
39401
diff
changeset

194 
(** instrumentalization **) 
a8c337299bc1
Code_Runtime.value, corresponding to ML_Context.value; tuned
haftmann
parents:
39401
diff
changeset

195 

38930
072363be3fd9
modernized; avoid pointless tinkering with structure names
haftmann
parents:
38929
diff
changeset

196 
fun evaluation_code thy module_name tycos consts = 
33992  197 
let 
42361  198 
val ctxt = Proof_Context.init_global thy; 
55188
7ca0204ece66
reduced prominence of "permissive code generation"
haftmann
parents:
55150
diff
changeset

199 
val program = Code_Thingol.consts_program thy consts; 
48568  200 
val (ml_modules, target_names) = 
42359  201 
Code_Target.produce_code_for thy 
55683  202 
target NONE module_name [] program false (map Constant consts @ map Type_Constructor tycos); 
48568  203 
val ml_code = space_implode "\n\n" (map snd ml_modules); 
55147
bce3dbc11f95
prefer explicit code symbol type over adhoc name mangling
haftmann
parents:
53171
diff
changeset

204 
val (consts', tycos') = chop (length consts) target_names; 
42359  205 
val consts_map = map2 (fn const => 
206 
fn NONE => 

207 
error ("Constant " ^ (quote o Code.string_of_const thy) const ^ 

208 
"\nhas a userdefined serialization") 

55147
bce3dbc11f95
prefer explicit code symbol type over adhoc name mangling
haftmann
parents:
53171
diff
changeset

209 
 SOME const' => (const, const')) consts consts' 
42359  210 
val tycos_map = map2 (fn tyco => 
211 
fn NONE => 

55304  212 
error ("Type " ^ quote (Proof_Context.markup_type ctxt tyco) ^ 
42359  213 
"\nhas a userdefined serialization") 
55147
bce3dbc11f95
prefer explicit code symbol type over adhoc name mangling
haftmann
parents:
53171
diff
changeset

214 
 SOME tyco' => (tyco, tyco')) tycos tycos'; 
34028
1e6206763036
split off evaluation mechanisms in separte module Code_Eval
haftmann
parents:
33992
diff
changeset

215 
in (ml_code, (tycos_map, consts_map)) end; 
28054  216 

217 

39404
a8c337299bc1
Code_Runtime.value, corresponding to ML_Context.value; tuned
haftmann
parents:
39401
diff
changeset

218 
(* by antiquotation *) 
28054  219 

220 
local 

221 

38930
072363be3fd9
modernized; avoid pointless tinkering with structure names
haftmann
parents:
38929
diff
changeset

222 
structure Code_Antiq_Data = Proof_Data 
28054  223 
( 
38930
072363be3fd9
modernized; avoid pointless tinkering with structure names
haftmann
parents:
38929
diff
changeset

224 
type T = (string list * string list) * (bool 
40421
b41aabb629ce
constructors to datatypes in code_reflect can be globbed; dropped unused code
haftmann
parents:
40320
diff
changeset

225 
* (string * (string * string) list) lazy); 
b41aabb629ce
constructors to datatypes in code_reflect can be globbed; dropped unused code
haftmann
parents:
40320
diff
changeset

226 
fun init _ = (([], []), (true, (Lazy.value ("", [])))); 
28054  227 
); 
228 

38930
072363be3fd9
modernized; avoid pointless tinkering with structure names
haftmann
parents:
38929
diff
changeset

229 
val is_first_occ = fst o snd o Code_Antiq_Data.get; 
28054  230 

30962  231 
fun register_code new_tycos new_consts ctxt = 
28054  232 
let 
38930
072363be3fd9
modernized; avoid pointless tinkering with structure names
haftmann
parents:
38929
diff
changeset

233 
val ((tycos, consts), _) = Code_Antiq_Data.get ctxt; 
30962  234 
val tycos' = fold (insert (op =)) new_tycos tycos; 
235 
val consts' = fold (insert (op =)) new_consts consts; 

38930
072363be3fd9
modernized; avoid pointless tinkering with structure names
haftmann
parents:
38929
diff
changeset

236 
val acc_code = Lazy.lazy (fn () => 
44663  237 
evaluation_code (Proof_Context.theory_of ctxt) structure_generated tycos' consts' 
40422
d425d1ed82af
corrected slip: must keep constant map, not type map; tuned code
haftmann
parents:
40421
diff
changeset

238 
> apsnd snd); 
38930
072363be3fd9
modernized; avoid pointless tinkering with structure names
haftmann
parents:
38929
diff
changeset

239 
in Code_Antiq_Data.put ((tycos', consts'), (false, acc_code)) ctxt end; 
30962  240 

241 
fun register_const const = register_code [] [const]; 

28054  242 

40421
b41aabb629ce
constructors to datatypes in code_reflect can be globbed; dropped unused code
haftmann
parents:
40320
diff
changeset

243 
fun print_code is_first const ctxt = 
30962  244 
let 
38930
072363be3fd9
modernized; avoid pointless tinkering with structure names
haftmann
parents:
38929
diff
changeset

245 
val (_, (_, acc_code)) = Code_Antiq_Data.get ctxt; 
40421
b41aabb629ce
constructors to datatypes in code_reflect can be globbed; dropped unused code
haftmann
parents:
40320
diff
changeset

246 
val (ml_code, consts_map) = Lazy.force acc_code; 
40422
d425d1ed82af
corrected slip: must keep constant map, not type map; tuned code
haftmann
parents:
40421
diff
changeset

247 
val ml_code = if is_first then ml_code else ""; 
41486
82c1e348bc18
reverted 08240feb69c7  breaks positions of reports;
wenzelm
parents:
41472
diff
changeset

248 
val body = "Isabelle." ^ the (AList.lookup (op =) consts_map const); 
41376
08240feb69c7
more robust ML antiquotations  allow original tokens without adjacent whitespace;
wenzelm
parents:
41349
diff
changeset

249 
in (ml_code, body) end; 
28054  250 

251 
in 

252 

53169
e2d31807cbf6
clarified type ML_Context.antiq: context parser maintains compilation context, declaration is applied to final context;
wenzelm
parents:
52435
diff
changeset

253 
fun ml_code_antiq context raw_const = 
28054  254 
let 
53169
e2d31807cbf6
clarified type ML_Context.antiq: context parser maintains compilation context, declaration is applied to final context;
wenzelm
parents:
52435
diff
changeset

255 
val ctxt = Context.the_proof context; 
e2d31807cbf6
clarified type ML_Context.antiq: context parser maintains compilation context, declaration is applied to final context;
wenzelm
parents:
52435
diff
changeset

256 
val thy = Proof_Context.theory_of ctxt; 
e2d31807cbf6
clarified type ML_Context.antiq: context parser maintains compilation context, declaration is applied to final context;
wenzelm
parents:
52435
diff
changeset

257 

e2d31807cbf6
clarified type ML_Context.antiq: context parser maintains compilation context, declaration is applied to final context;
wenzelm
parents:
52435
diff
changeset

258 
val const = Code.check_const thy raw_const; 
e2d31807cbf6
clarified type ML_Context.antiq: context parser maintains compilation context, declaration is applied to final context;
wenzelm
parents:
52435
diff
changeset

259 
val is_first = is_first_occ ctxt; 
e2d31807cbf6
clarified type ML_Context.antiq: context parser maintains compilation context, declaration is applied to final context;
wenzelm
parents:
52435
diff
changeset

260 
val ctxt' = register_const const ctxt; 
e2d31807cbf6
clarified type ML_Context.antiq: context parser maintains compilation context, declaration is applied to final context;
wenzelm
parents:
52435
diff
changeset

261 
in (Context.Proof ctxt', print_code is_first const) end; 
30962  262 

28054  263 
end; (*local*) 
264 

265 

39404
a8c337299bc1
Code_Runtime.value, corresponding to ML_Context.value; tuned
haftmann
parents:
39401
diff
changeset

266 
(* reflection support *) 
36470  267 

40421
b41aabb629ce
constructors to datatypes in code_reflect can be globbed; dropped unused code
haftmann
parents:
40320
diff
changeset

268 
fun check_datatype thy tyco some_consts = 
36470  269 
let 
40726
16dcfedc4eb7
keep type variable arguments of datatype constructors in bookkeeping
haftmann
parents:
40711
diff
changeset

270 
val constrs = (map fst o snd o fst o Code.get_type thy) tyco; 
40421
b41aabb629ce
constructors to datatypes in code_reflect can be globbed; dropped unused code
haftmann
parents:
40320
diff
changeset

271 
val _ = case some_consts 
b41aabb629ce
constructors to datatypes in code_reflect can be globbed; dropped unused code
haftmann
parents:
40320
diff
changeset

272 
of SOME consts => 
b41aabb629ce
constructors to datatypes in code_reflect can be globbed; dropped unused code
haftmann
parents:
40320
diff
changeset

273 
let 
b41aabb629ce
constructors to datatypes in code_reflect can be globbed; dropped unused code
haftmann
parents:
40320
diff
changeset

274 
val missing_constrs = subtract (op =) consts constrs; 
b41aabb629ce
constructors to datatypes in code_reflect can be globbed; dropped unused code
haftmann
parents:
40320
diff
changeset

275 
val _ = if null missing_constrs then [] 
45430  276 
else error ("Missing constructor(s) " ^ commas_quote missing_constrs 
40421
b41aabb629ce
constructors to datatypes in code_reflect can be globbed; dropped unused code
haftmann
parents:
40320
diff
changeset

277 
^ " for datatype " ^ quote tyco); 
b41aabb629ce
constructors to datatypes in code_reflect can be globbed; dropped unused code
haftmann
parents:
40320
diff
changeset

278 
val false_constrs = subtract (op =) constrs consts; 
b41aabb629ce
constructors to datatypes in code_reflect can be globbed; dropped unused code
haftmann
parents:
40320
diff
changeset

279 
val _ = if null false_constrs then [] 
45430  280 
else error ("Nonconstructor(s) " ^ commas_quote false_constrs 
40421
b41aabb629ce
constructors to datatypes in code_reflect can be globbed; dropped unused code
haftmann
parents:
40320
diff
changeset

281 
^ " for datatype " ^ quote tyco) 
b41aabb629ce
constructors to datatypes in code_reflect can be globbed; dropped unused code
haftmann
parents:
40320
diff
changeset

282 
in () end 
b41aabb629ce
constructors to datatypes in code_reflect can be globbed; dropped unused code
haftmann
parents:
40320
diff
changeset

283 
 NONE => (); 
b41aabb629ce
constructors to datatypes in code_reflect can be globbed; dropped unused code
haftmann
parents:
40320
diff
changeset

284 
in (tyco, constrs) end; 
36470  285 

286 
fun add_eval_tyco (tyco, tyco') thy = 

287 
let 

288 
val k = Sign.arity_number thy tyco; 

40421
b41aabb629ce
constructors to datatypes in code_reflect can be globbed; dropped unused code
haftmann
parents:
40320
diff
changeset

289 
fun pr pr' _ [] = tyco' 
b41aabb629ce
constructors to datatypes in code_reflect can be globbed; dropped unused code
haftmann
parents:
40320
diff
changeset

290 
 pr pr' _ [ty] = 
36470  291 
Code_Printer.concat [pr' Code_Printer.BR ty, tyco'] 
40421
b41aabb629ce
constructors to datatypes in code_reflect can be globbed; dropped unused code
haftmann
parents:
40320
diff
changeset

292 
 pr pr' _ tys = 
36470  293 
Code_Printer.concat [Code_Printer.enum "," "(" ")" (map (pr' Code_Printer.BR) tys), tyco'] 
294 
in 

295 
thy 

55150  296 
> Code_Target.set_printings (Type_Constructor (tyco, [(target, SOME (k, pr))])) 
36470  297 
end; 
298 

36514  299 
fun add_eval_constr (const, const') thy = 
300 
let 

301 
val k = Code.args_number thy const; 

302 
fun pr pr' fxy ts = Code_Printer.brackify fxy 

38922  303 
(const' :: the_list (Code_Printer.tuplify pr' Code_Printer.BR (map fst ts))); 
36514  304 
in 
305 
thy 

55150  306 
> Code_Target.set_printings (Constant (const, 
52435
6646bb548c6b
migration from code_(consttypeclassinstance) to code_printing and from code_module to code_identifier
haftmann
parents:
52434
diff
changeset

307 
[(target, SOME (Code_Printer.simple_const_syntax (k, pr)))])) 
36514  308 
end; 
309 

55150  310 
fun add_eval_const (const, const') = Code_Target.set_printings (Constant 
52435
6646bb548c6b
migration from code_(consttypeclassinstance) to code_printing and from code_module to code_identifier
haftmann
parents:
52434
diff
changeset

311 
(const, [(target, SOME (Code_Printer.simple_const_syntax (0, (K o K o K) const')))])); 
36470  312 

39912
2ffe7060ca75
avoid antiquotation processing for code_reflect; moved ML_Context.value to Code_Runtime
haftmann
parents:
39816
diff
changeset

313 
fun process_reflection (code, (tyco_map, (constr_map, const_map))) module_name NONE thy = 
38935
2cf3d8305b47
corrected misbehaved additional qualification of generated names
haftmann
parents:
38933
diff
changeset

314 
thy 
2cf3d8305b47
corrected misbehaved additional qualification of generated names
haftmann
parents:
38933
diff
changeset

315 
> Code_Target.add_reserved target module_name 
39912
2ffe7060ca75
avoid antiquotation processing for code_reflect; moved ML_Context.value to Code_Runtime
haftmann
parents:
39816
diff
changeset

316 
> Context.theory_map (exec true code) 
38935
2cf3d8305b47
corrected misbehaved additional qualification of generated names
haftmann
parents:
38933
diff
changeset

317 
> fold (add_eval_tyco o apsnd Code_Printer.str) tyco_map 
2cf3d8305b47
corrected misbehaved additional qualification of generated names
haftmann
parents:
38933
diff
changeset

318 
> fold (add_eval_constr o apsnd Code_Printer.str) constr_map 
2cf3d8305b47
corrected misbehaved additional qualification of generated names
haftmann
parents:
38933
diff
changeset

319 
> fold (add_eval_const o apsnd Code_Printer.str) const_map 
39912
2ffe7060ca75
avoid antiquotation processing for code_reflect; moved ML_Context.value to Code_Runtime
haftmann
parents:
39816
diff
changeset

320 
 process_reflection (code, _) _ (SOME file_name) thy = 
36470  321 
let 
37950
bc285d91041e
moved basic thy file name operations from Thy_Load to Thy_Header;
wenzelm
parents:
37744
diff
changeset

322 
val preamble = 
46737  323 
"(* Generated from " ^ 
324 
Path.implode (Thy_Load.thy_path (Path.basic (Context.theory_name thy))) ^ 

325 
"; DO NOT EDIT! *)"; 

39912
2ffe7060ca75
avoid antiquotation processing for code_reflect; moved ML_Context.value to Code_Runtime
haftmann
parents:
39816
diff
changeset

326 
val _ = File.write (Path.explode file_name) (preamble ^ "\n\n" ^ code); 
36470  327 
in 
328 
thy 

329 
end; 

330 

331 
fun gen_code_reflect prep_type prep_const raw_datatypes raw_functions module_name some_file thy = 

332 
let 

333 
val datatypes = map (fn (raw_tyco, raw_cos) => 

40421
b41aabb629ce
constructors to datatypes in code_reflect can be globbed; dropped unused code
haftmann
parents:
40320
diff
changeset

334 
(prep_type thy raw_tyco, (Option.map o map) (prep_const thy) raw_cos)) raw_datatypes; 
b41aabb629ce
constructors to datatypes in code_reflect can be globbed; dropped unused code
haftmann
parents:
40320
diff
changeset

335 
val (tycos, constrs) = map_split (uncurry (check_datatype thy)) datatypes 
b41aabb629ce
constructors to datatypes in code_reflect can be globbed; dropped unused code
haftmann
parents:
40320
diff
changeset

336 
> apsnd flat; 
36470  337 
val functions = map (prep_const thy) raw_functions; 
36514  338 
val result = evaluation_code thy module_name tycos (constrs @ functions) 
339 
> (apsnd o apsnd) (chop (length constrs)); 

36470  340 
in 
341 
thy 

39485
f7270a5e2550
closures preserve static serializer context for static evaluation; tuned
haftmann
parents:
39482
diff
changeset

342 
> process_reflection result module_name some_file 
36470  343 
end; 
344 

39422  345 
val code_reflect = gen_code_reflect Code_Target.cert_tyco (K I); 
36470  346 
val code_reflect_cmd = gen_code_reflect Code_Target.read_tyco Code.read_const; 
347 

348 

28054  349 
(** Isar setup **) 
350 

53171  351 
val _ = Theory.setup 
352 
(ML_Context.add_antiq @{binding code} 

353 
(Scan.depend (fn context => Scan.pass context Args.term >> ml_code_antiq context))); 

28054  354 

36470  355 
local 
356 

36960
01594f816e3a
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents:
36610
diff
changeset

357 
val parse_datatype = 
46949  358 
Parse.name  @{keyword "="}  
40711
81bc73585eec
globbing constant expressions use more idiomatic underscore rather than star
haftmann
parents:
40422
diff
changeset

359 
(((Parse.sym_ident  Parse.string) >> (fn "_" => NONE  _ => Scan.fail ())) 
46949  360 
 ((Parse.term ::: (Scan.repeat (@{keyword ""}  Parse.term))) >> SOME)); 
36470  361 

362 
in 

363 

364 
val _ = 

46961
5c6955f487e5
outer syntax command definitions based on formal command_spec derived from theory header declarations;
wenzelm
parents:
46949
diff
changeset

365 
Outer_Syntax.command @{command_spec "code_reflect"} 
5c6955f487e5
outer syntax command definitions based on formal command_spec derived from theory header declarations;
wenzelm
parents:
46949
diff
changeset

366 
"enrich runtime environment with generated code" 
52434  367 
(Parse.name  Scan.optional (@{keyword "datatypes"}  Parse.!!! (parse_datatype 
46949  368 
::: Scan.repeat (@{keyword "and"}  parse_datatype))) [] 
52434  369 
 Scan.optional (@{keyword "functions"}  Parse.!!! (Scan.repeat1 Parse.name)) [] 
370 
 Scan.option (@{keyword "file"}  Parse.!!! Parse.name) 

46961
5c6955f487e5
outer syntax command definitions based on formal command_spec derived from theory header declarations;
wenzelm
parents:
46949
diff
changeset

371 
>> (fn (((module_name, raw_datatypes), raw_functions), some_file) => Toplevel.theory 
5c6955f487e5
outer syntax command definitions based on formal command_spec derived from theory header declarations;
wenzelm
parents:
46949
diff
changeset

372 
(code_reflect_cmd raw_datatypes raw_functions module_name some_file))); 
36470  373 

374 
end; (*local*) 

375 

39816
c7cec137c48a
added polyml_as_definition  using external SML files as substitute for proper definitions  only for polyml!
haftmann
parents:
39605
diff
changeset

376 

c7cec137c48a
added polyml_as_definition  using external SML files as substitute for proper definitions  only for polyml!
haftmann
parents:
39605
diff
changeset

377 
(** using external SML files as substitute for proper definitions  only for polyml! **) 
c7cec137c48a
added polyml_as_definition  using external SML files as substitute for proper definitions  only for polyml!
haftmann
parents:
39605
diff
changeset

378 

c7cec137c48a
added polyml_as_definition  using external SML files as substitute for proper definitions  only for polyml!
haftmann
parents:
39605
diff
changeset

379 
local 
c7cec137c48a
added polyml_as_definition  using external SML files as substitute for proper definitions  only for polyml!
haftmann
parents:
39605
diff
changeset

380 

39820  381 
structure Loaded_Values = Theory_Data 
382 
( 

39816
c7cec137c48a
added polyml_as_definition  using external SML files as substitute for proper definitions  only for polyml!
haftmann
parents:
39605
diff
changeset

383 
type T = string list 
c7cec137c48a
added polyml_as_definition  using external SML files as substitute for proper definitions  only for polyml!
haftmann
parents:
39605
diff
changeset

384 
val empty = [] 
41472
f6ab14e61604
misc tuning and comments based on review of Theory_Data, Proof_Data, Generic_Data usage;
wenzelm
parents:
41376
diff
changeset

385 
val extend = I 
39820  386 
fun merge data : T = Library.merge (op =) data 
39816
c7cec137c48a
added polyml_as_definition  using external SML files as substitute for proper definitions  only for polyml!
haftmann
parents:
39605
diff
changeset

387 
); 
c7cec137c48a
added polyml_as_definition  using external SML files as substitute for proper definitions  only for polyml!
haftmann
parents:
39605
diff
changeset

388 

c7cec137c48a
added polyml_as_definition  using external SML files as substitute for proper definitions  only for polyml!
haftmann
parents:
39605
diff
changeset

389 
fun notify_val (string, value) = 
c7cec137c48a
added polyml_as_definition  using external SML files as substitute for proper definitions  only for polyml!
haftmann
parents:
39605
diff
changeset

390 
let 
c7cec137c48a
added polyml_as_definition  using external SML files as substitute for proper definitions  only for polyml!
haftmann
parents:
39605
diff
changeset

391 
val _ = #enterVal ML_Env.name_space (string, value); 
53171  392 
val _ = Theory.setup (Loaded_Values.map (insert (op =) string)); 
39816
c7cec137c48a
added polyml_as_definition  using external SML files as substitute for proper definitions  only for polyml!
haftmann
parents:
39605
diff
changeset

393 
in () end; 
c7cec137c48a
added polyml_as_definition  using external SML files as substitute for proper definitions  only for polyml!
haftmann
parents:
39605
diff
changeset

394 

c7cec137c48a
added polyml_as_definition  using external SML files as substitute for proper definitions  only for polyml!
haftmann
parents:
39605
diff
changeset

395 
fun abort _ = error "Only value bindings allowed."; 
c7cec137c48a
added polyml_as_definition  using external SML files as substitute for proper definitions  only for polyml!
haftmann
parents:
39605
diff
changeset

396 

c7cec137c48a
added polyml_as_definition  using external SML files as substitute for proper definitions  only for polyml!
haftmann
parents:
39605
diff
changeset

397 
val notifying_context : use_context = 
c7cec137c48a
added polyml_as_definition  using external SML files as substitute for proper definitions  only for polyml!
haftmann
parents:
39605
diff
changeset

398 
{tune_source = #tune_source ML_Env.local_context, 
c7cec137c48a
added polyml_as_definition  using external SML files as substitute for proper definitions  only for polyml!
haftmann
parents:
39605
diff
changeset

399 
name_space = 
c7cec137c48a
added polyml_as_definition  using external SML files as substitute for proper definitions  only for polyml!
haftmann
parents:
39605
diff
changeset

400 
{lookupVal = #lookupVal ML_Env.name_space, 
c7cec137c48a
added polyml_as_definition  using external SML files as substitute for proper definitions  only for polyml!
haftmann
parents:
39605
diff
changeset

401 
lookupType = #lookupType ML_Env.name_space, 
c7cec137c48a
added polyml_as_definition  using external SML files as substitute for proper definitions  only for polyml!
haftmann
parents:
39605
diff
changeset

402 
lookupFix = #lookupFix ML_Env.name_space, 
c7cec137c48a
added polyml_as_definition  using external SML files as substitute for proper definitions  only for polyml!
haftmann
parents:
39605
diff
changeset

403 
lookupStruct = #lookupStruct ML_Env.name_space, 
c7cec137c48a
added polyml_as_definition  using external SML files as substitute for proper definitions  only for polyml!
haftmann
parents:
39605
diff
changeset

404 
lookupSig = #lookupSig ML_Env.name_space, 
c7cec137c48a
added polyml_as_definition  using external SML files as substitute for proper definitions  only for polyml!
haftmann
parents:
39605
diff
changeset

405 
lookupFunct = #lookupFunct ML_Env.name_space, 
c7cec137c48a
added polyml_as_definition  using external SML files as substitute for proper definitions  only for polyml!
haftmann
parents:
39605
diff
changeset

406 
enterVal = notify_val, 
c7cec137c48a
added polyml_as_definition  using external SML files as substitute for proper definitions  only for polyml!
haftmann
parents:
39605
diff
changeset

407 
enterType = abort, 
c7cec137c48a
added polyml_as_definition  using external SML files as substitute for proper definitions  only for polyml!
haftmann
parents:
39605
diff
changeset

408 
enterFix = abort, 
c7cec137c48a
added polyml_as_definition  using external SML files as substitute for proper definitions  only for polyml!
haftmann
parents:
39605
diff
changeset

409 
enterStruct = abort, 
c7cec137c48a
added polyml_as_definition  using external SML files as substitute for proper definitions  only for polyml!
haftmann
parents:
39605
diff
changeset

410 
enterSig = abort, 
c7cec137c48a
added polyml_as_definition  using external SML files as substitute for proper definitions  only for polyml!
haftmann
parents:
39605
diff
changeset

411 
enterFunct = abort, 
c7cec137c48a
added polyml_as_definition  using external SML files as substitute for proper definitions  only for polyml!
haftmann
parents:
39605
diff
changeset

412 
allVal = #allVal ML_Env.name_space, 
c7cec137c48a
added polyml_as_definition  using external SML files as substitute for proper definitions  only for polyml!
haftmann
parents:
39605
diff
changeset

413 
allType = #allType ML_Env.name_space, 
c7cec137c48a
added polyml_as_definition  using external SML files as substitute for proper definitions  only for polyml!
haftmann
parents:
39605
diff
changeset

414 
allFix = #allFix ML_Env.name_space, 
c7cec137c48a
added polyml_as_definition  using external SML files as substitute for proper definitions  only for polyml!
haftmann
parents:
39605
diff
changeset

415 
allStruct = #allStruct ML_Env.name_space, 
c7cec137c48a
added polyml_as_definition  using external SML files as substitute for proper definitions  only for polyml!
haftmann
parents:
39605
diff
changeset

416 
allSig = #allSig ML_Env.name_space, 
c7cec137c48a
added polyml_as_definition  using external SML files as substitute for proper definitions  only for polyml!
haftmann
parents:
39605
diff
changeset

417 
allFunct = #allFunct ML_Env.name_space}, 
c7cec137c48a
added polyml_as_definition  using external SML files as substitute for proper definitions  only for polyml!
haftmann
parents:
39605
diff
changeset

418 
str_of_pos = #str_of_pos ML_Env.local_context, 
c7cec137c48a
added polyml_as_definition  using external SML files as substitute for proper definitions  only for polyml!
haftmann
parents:
39605
diff
changeset

419 
print = #print ML_Env.local_context, 
c7cec137c48a
added polyml_as_definition  using external SML files as substitute for proper definitions  only for polyml!
haftmann
parents:
39605
diff
changeset

420 
error = #error ML_Env.local_context}; 
c7cec137c48a
added polyml_as_definition  using external SML files as substitute for proper definitions  only for polyml!
haftmann
parents:
39605
diff
changeset

421 

c7cec137c48a
added polyml_as_definition  using external SML files as substitute for proper definitions  only for polyml!
haftmann
parents:
39605
diff
changeset

422 
in 
c7cec137c48a
added polyml_as_definition  using external SML files as substitute for proper definitions  only for polyml!
haftmann
parents:
39605
diff
changeset

423 

c7cec137c48a
added polyml_as_definition  using external SML files as substitute for proper definitions  only for polyml!
haftmann
parents:
39605
diff
changeset

424 
fun use_file filepath thy = 
c7cec137c48a
added polyml_as_definition  using external SML files as substitute for proper definitions  only for polyml!
haftmann
parents:
39605
diff
changeset

425 
let 
c7cec137c48a
added polyml_as_definition  using external SML files as substitute for proper definitions  only for polyml!
haftmann
parents:
39605
diff
changeset

426 
val thy' = Loaded_Values.put [] thy; 
c7cec137c48a
added polyml_as_definition  using external SML files as substitute for proper definitions  only for polyml!
haftmann
parents:
39605
diff
changeset

427 
val _ = Context.set_thread_data ((SOME o Context.Theory) thy'); 
c7cec137c48a
added polyml_as_definition  using external SML files as substitute for proper definitions  only for polyml!
haftmann
parents:
39605
diff
changeset

428 
val _ = Secure.use_text notifying_context 
c7cec137c48a
added polyml_as_definition  using external SML files as substitute for proper definitions  only for polyml!
haftmann
parents:
39605
diff
changeset

429 
(0, Path.implode filepath) false (File.read filepath); 
45268  430 
val thy'' = Context.the_theory (Context.the_thread_data ()); 
39912
2ffe7060ca75
avoid antiquotation processing for code_reflect; moved ML_Context.value to Code_Runtime
haftmann
parents:
39816
diff
changeset

431 
val names = Loaded_Values.get thy''; 
40320
abc52faa7761
polyml_as_definition does not require explicit dependencies on external ML files
haftmann
parents:
40257
diff
changeset

432 
in (names, thy'') end; 
39816
c7cec137c48a
added polyml_as_definition  using external SML files as substitute for proper definitions  only for polyml!
haftmann
parents:
39605
diff
changeset

433 

c7cec137c48a
added polyml_as_definition  using external SML files as substitute for proper definitions  only for polyml!
haftmann
parents:
39605
diff
changeset

434 
end; 
c7cec137c48a
added polyml_as_definition  using external SML files as substitute for proper definitions  only for polyml!
haftmann
parents:
39605
diff
changeset

435 

c7cec137c48a
added polyml_as_definition  using external SML files as substitute for proper definitions  only for polyml!
haftmann
parents:
39605
diff
changeset

436 
fun add_definiendum (ml_name, (b, T)) thy = 
c7cec137c48a
added polyml_as_definition  using external SML files as substitute for proper definitions  only for polyml!
haftmann
parents:
39605
diff
changeset

437 
thy 
c7cec137c48a
added polyml_as_definition  using external SML files as substitute for proper definitions  only for polyml!
haftmann
parents:
39605
diff
changeset

438 
> Code_Target.add_reserved target ml_name 
c7cec137c48a
added polyml_as_definition  using external SML files as substitute for proper definitions  only for polyml!
haftmann
parents:
39605
diff
changeset

439 
> Specification.axiomatization [(b, SOME T, NoSyn)] [] 
c7cec137c48a
added polyml_as_definition  using external SML files as substitute for proper definitions  only for polyml!
haftmann
parents:
39605
diff
changeset

440 
> (fn ([Const (const, _)], _) => 
55150  441 
Code_Target.set_printings (Constant (const, 
52435
6646bb548c6b
migration from code_(consttypeclassinstance) to code_printing and from code_module to code_identifier
haftmann
parents:
52434
diff
changeset

442 
[(target, SOME (Code_Printer.simple_const_syntax (0, (K o K o K o Code_Printer.str) ml_name)))])) 
55683  443 
#> tap (fn thy => Code_Target.produce_code thy false [const] target NONE structure_generated [])); 
39816
c7cec137c48a
added polyml_as_definition  using external SML files as substitute for proper definitions  only for polyml!
haftmann
parents:
39605
diff
changeset

444 

c7cec137c48a
added polyml_as_definition  using external SML files as substitute for proper definitions  only for polyml!
haftmann
parents:
39605
diff
changeset

445 
fun process_file filepath (definienda, thy) = 
c7cec137c48a
added polyml_as_definition  using external SML files as substitute for proper definitions  only for polyml!
haftmann
parents:
39605
diff
changeset

446 
let 
c7cec137c48a
added polyml_as_definition  using external SML files as substitute for proper definitions  only for polyml!
haftmann
parents:
39605
diff
changeset

447 
val (ml_names, thy') = use_file filepath thy; 
c7cec137c48a
added polyml_as_definition  using external SML files as substitute for proper definitions  only for polyml!
haftmann
parents:
39605
diff
changeset

448 
val superfluous = subtract (fn ((name1, _), name2) => name1 = name2) definienda ml_names; 
c7cec137c48a
added polyml_as_definition  using external SML files as substitute for proper definitions  only for polyml!
haftmann
parents:
39605
diff
changeset

449 
val _ = if null superfluous then () 
c7cec137c48a
added polyml_as_definition  using external SML files as substitute for proper definitions  only for polyml!
haftmann
parents:
39605
diff
changeset

450 
else error ("Value binding(s) " ^ commas_quote superfluous 
41944
b97091ae583a
Path.print is the official way to show filesystem paths to users  note that Path.implode often indicates violation of the abstract datatype;
wenzelm
parents:
41486
diff
changeset

451 
^ " found in external file " ^ Path.print filepath 
39816
c7cec137c48a
added polyml_as_definition  using external SML files as substitute for proper definitions  only for polyml!
haftmann
parents:
39605
diff
changeset

452 
^ " not present among the given contants binding(s)."); 
c7cec137c48a
added polyml_as_definition  using external SML files as substitute for proper definitions  only for polyml!
haftmann
parents:
39605
diff
changeset

453 
val these_definienda = AList.make (the o AList.lookup (op =) definienda) ml_names; 
c7cec137c48a
added polyml_as_definition  using external SML files as substitute for proper definitions  only for polyml!
haftmann
parents:
39605
diff
changeset

454 
val thy'' = fold add_definiendum these_definienda thy'; 
c7cec137c48a
added polyml_as_definition  using external SML files as substitute for proper definitions  only for polyml!
haftmann
parents:
39605
diff
changeset

455 
val definienda' = fold (AList.delete (op =)) ml_names definienda; 
c7cec137c48a
added polyml_as_definition  using external SML files as substitute for proper definitions  only for polyml!
haftmann
parents:
39605
diff
changeset

456 
in (definienda', thy'') end; 
c7cec137c48a
added polyml_as_definition  using external SML files as substitute for proper definitions  only for polyml!
haftmann
parents:
39605
diff
changeset

457 

c7cec137c48a
added polyml_as_definition  using external SML files as substitute for proper definitions  only for polyml!
haftmann
parents:
39605
diff
changeset

458 
fun polyml_as_definition bTs filepaths thy = 
c7cec137c48a
added polyml_as_definition  using external SML files as substitute for proper definitions  only for polyml!
haftmann
parents:
39605
diff
changeset

459 
let 
c7cec137c48a
added polyml_as_definition  using external SML files as substitute for proper definitions  only for polyml!
haftmann
parents:
39605
diff
changeset

460 
val definienda = map (fn bT => ((Binding.name_of o fst) bT, bT)) bTs; 
c7cec137c48a
added polyml_as_definition  using external SML files as substitute for proper definitions  only for polyml!
haftmann
parents:
39605
diff
changeset

461 
val (remaining, thy') = fold process_file filepaths (definienda, thy); 
c7cec137c48a
added polyml_as_definition  using external SML files as substitute for proper definitions  only for polyml!
haftmann
parents:
39605
diff
changeset

462 
val _ = if null remaining then () 
c7cec137c48a
added polyml_as_definition  using external SML files as substitute for proper definitions  only for polyml!
haftmann
parents:
39605
diff
changeset

463 
else error ("Constant binding(s) " ^ commas_quote (map fst remaining) 
c7cec137c48a
added polyml_as_definition  using external SML files as substitute for proper definitions  only for polyml!
haftmann
parents:
39605
diff
changeset

464 
^ " not present in external file(s)."); 
c7cec137c48a
added polyml_as_definition  using external SML files as substitute for proper definitions  only for polyml!
haftmann
parents:
39605
diff
changeset

465 
in thy' end; 
c7cec137c48a
added polyml_as_definition  using external SML files as substitute for proper definitions  only for polyml!
haftmann
parents:
39605
diff
changeset

466 

28054  467 
end; (*struct*) 