author  wenzelm 
Sun, 09 Jan 2011 21:33:41 +0100  
changeset 41486  82c1e348bc18 
parent 41472  f6ab14e61604 
child 41944  b97091ae583a 
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 

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

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

40 

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

41 
(** evaluation **) 
33992  42 

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

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

44 

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

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

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

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

48 

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

49 
val target = "Eval"; 
28054  50 

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

51 
datatype truth = Holds; 
39422  52 

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

53 
val _ = Context.>> (Context.map_theory 
33638f4883ac
dynamic and static value computation; builtin evaluation of propositions
haftmann
parents:
39422
diff
changeset

54 
(Code_Target.extend_target (target, (Code_ML.target_SML, K I)) 
39485
f7270a5e2550
closures preserve static serializer context for static evaluation; tuned
haftmann
parents:
39482
diff
changeset

55 
#> Code_Target.add_tyco_syntax target @{type_name prop} 
f7270a5e2550
closures preserve static serializer context for static evaluation; tuned
haftmann
parents:
39482
diff
changeset

56 
(SOME (0, (K o K o K) (Code_Printer.str s_truth))) 
f7270a5e2550
closures preserve static serializer context for static evaluation; tuned
haftmann
parents:
39482
diff
changeset

57 
#> Code_Target.add_const_syntax target @{const_name Code_Generator.holds} 
f7270a5e2550
closures preserve static serializer context for static evaluation; tuned
haftmann
parents:
39482
diff
changeset

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

59 
#> Code_Target.add_reserved target this 
39485
f7270a5e2550
closures preserve static serializer context for static evaluation; tuned
haftmann
parents:
39482
diff
changeset

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

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

62 

40150  63 
val trace = Unsynchronized.ref false; 
64 

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

65 
fun exec verbose code = 
40150  66 
(if ! trace then tracing code else (); 
40257  67 
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

68 

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

69 
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

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

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

72 
^ "\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

73 
^ " (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

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

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

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

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

78 

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

79 

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

80 
(* evaluation into target language values *) 
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 
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

83 

39605  84 
fun reject_vars thy t = 
85 
let 

86 
val ctxt = ProofContext.init_global thy; 

87 
in ((Sign.no_frees ctxt o Sign.no_vars ctxt o map_types (K dummyT)) t; t) end; 

88 

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

89 
fun obtain_evaluator thy some_target = Code_Target.evaluator thy (the_default target some_target); 
39485
f7270a5e2550
closures preserve static serializer context for static evaluation; tuned
haftmann
parents:
39482
diff
changeset

90 

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

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

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

93 
val ctxt = ProofContext.init_global thy; 
41347
064133cb4ef6
evaluator separating static and dynamic operations
haftmann
parents:
41343
diff
changeset

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

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

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

97 
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

98 

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

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

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

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

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

103 

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

104 
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

105 
let 
39605  106 
val _ = reject_vars thy t; 
41099  107 
val _ = if ! trace 
108 
then tracing ("Evaluation of term " ^ quote (Syntax.string_of_term_global thy t)) 

109 
else () 

39482  110 
fun evaluator naming program ((_, vs_ty), t) deps = 
41347
064133cb4ef6
evaluator separating static and dynamic operations
haftmann
parents:
41343
diff
changeset

111 
evaluation cookie thy (obtain_evaluator thy some_target naming program deps) (vs_ty, t) args; 
41184  112 
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

113 

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

114 
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

115 
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

116 

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

117 
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

118 
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

119 

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

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

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

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

123 
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

124 

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

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

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

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

128 

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

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

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

131 

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

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

133 
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

134 

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

135 

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

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

137 

39820  138 
structure Truth_Result = Proof_Data 
139 
( 

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

140 
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

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

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

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

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

145 
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

146 

39605  147 
val reject_vars = fn thy => tap (reject_vars thy o Thm.term_of); 
148 

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

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

150 

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

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

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

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

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

155 
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

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

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

158 
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

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

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

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

162 
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

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

164 

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

165 
val (_, raw_check_holds_oracle) = Context.>>> (Context.map_theory_result 
33638f4883ac
dynamic and static value computation; builtin evaluation of propositions
haftmann
parents:
39422
diff
changeset

166 
(Thm.add_oracle (Binding.name "holds_by_evaluation", 
41349
0e2a3f22f018
evaluator separating static and dynamic operations
haftmann
parents:
41348
diff
changeset

167 
fn (thy, evaluator, vs_t, deps, ct) => check_holds thy evaluator vs_t deps ct))); 
39473
33638f4883ac
dynamic and static value computation; builtin evaluation of propositions
haftmann
parents:
39422
diff
changeset

168 

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

169 
fun check_holds_oracle thy evaluator ((_, vs_ty), t) deps ct = 
0e2a3f22f018
evaluator separating static and dynamic operations
haftmann
parents:
41348
diff
changeset

170 
raw_check_holds_oracle (thy, evaluator, (vs_ty, t), deps, ct); 
0e2a3f22f018
evaluator separating static and dynamic operations
haftmann
parents:
41348
diff
changeset

171 

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

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

173 

41247  174 
fun dynamic_holds_conv thy = Code_Thingol.dynamic_conv thy 
41349
0e2a3f22f018
evaluator separating static and dynamic operations
haftmann
parents:
41348
diff
changeset

175 
(fn naming => fn program => fn vs_t => fn deps => 
0e2a3f22f018
evaluator separating static and dynamic operations
haftmann
parents:
41348
diff
changeset

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

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

178 

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

179 
fun static_holds_conv thy consts = Code_Thingol.static_conv thy consts 
0e2a3f22f018
evaluator separating static and dynamic operations
haftmann
parents:
41348
diff
changeset

180 
(fn naming => fn program => fn consts' => 
0e2a3f22f018
evaluator separating static and dynamic operations
haftmann
parents:
41348
diff
changeset

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

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

183 

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

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

185 

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

186 

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

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

188 

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

189 
fun evaluation_code thy module_name tycos consts = 
33992  190 
let 
36271
2ef9dbddfcb8
optionally ignore errors during translation of equations
haftmann
parents:
35360
diff
changeset

191 
val (consts', (naming, program)) = Code_Thingol.consts_program thy false consts; 
34028
1e6206763036
split off evaluation mechanisms in separte module Code_Eval
haftmann
parents:
33992
diff
changeset

192 
val tycos' = map (the o Code_Thingol.lookup_tyco naming) tycos; 
38921  193 
val (ml_code, target_names) = Code_Target.produce_code_for thy 
38933
bd77e092f67c
avoid strange special treatment of empty module names
haftmann
parents:
38931
diff
changeset

194 
target NONE module_name [] naming program (consts' @ tycos'); 
34028
1e6206763036
split off evaluation mechanisms in separte module Code_Eval
haftmann
parents:
33992
diff
changeset

195 
val (consts'', tycos'') = chop (length consts') target_names; 
1e6206763036
split off evaluation mechanisms in separte module Code_Eval
haftmann
parents:
33992
diff
changeset

196 
val consts_map = map2 (fn const => fn NONE => 
1e6206763036
split off evaluation mechanisms in separte module Code_Eval
haftmann
parents:
33992
diff
changeset

197 
error ("Constant " ^ (quote o Code.string_of_const thy) const 
1e6206763036
split off evaluation mechanisms in separte module Code_Eval
haftmann
parents:
33992
diff
changeset

198 
^ "\nhas a userdefined serialization") 
1e6206763036
split off evaluation mechanisms in separte module Code_Eval
haftmann
parents:
33992
diff
changeset

199 
 SOME const'' => (const, const'')) consts consts'' 
1e6206763036
split off evaluation mechanisms in separte module Code_Eval
haftmann
parents:
33992
diff
changeset

200 
val tycos_map = map2 (fn tyco => fn NONE => 
1e6206763036
split off evaluation mechanisms in separte module Code_Eval
haftmann
parents:
33992
diff
changeset

201 
error ("Type " ^ (quote o Sign.extern_type thy) tyco 
1e6206763036
split off evaluation mechanisms in separte module Code_Eval
haftmann
parents:
33992
diff
changeset

202 
^ "\nhas a userdefined serialization") 
1e6206763036
split off evaluation mechanisms in separte module Code_Eval
haftmann
parents:
33992
diff
changeset

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

204 
in (ml_code, (tycos_map, consts_map)) end; 
28054  205 

206 

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

207 
(* by antiquotation *) 
28054  208 

209 
local 

210 

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

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

213 
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

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

215 
fun init _ = (([], []), (true, (Lazy.value ("", [])))); 
28054  216 
); 
217 

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

218 
val is_first_occ = fst o snd o Code_Antiq_Data.get; 
28054  219 

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

222 
val ((tycos, consts), _) = Code_Antiq_Data.get ctxt; 
30962  223 
val tycos' = fold (insert (op =)) new_tycos tycos; 
224 
val consts' = fold (insert (op =)) new_consts consts; 

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

225 
val acc_code = Lazy.lazy (fn () => 
40421
b41aabb629ce
constructors to datatypes in code_reflect can be globbed; dropped unused code
haftmann
parents:
40320
diff
changeset

226 
evaluation_code (ProofContext.theory_of ctxt) "Code" tycos' consts' 
40422
d425d1ed82af
corrected slip: must keep constant map, not type map; tuned code
haftmann
parents:
40421
diff
changeset

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

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

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

28054  231 

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

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

234 
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

235 
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

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

237 
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

238 
in (ml_code, body) end; 
28054  239 

240 
in 

241 

35019
1ec0a3ff229e
simplified interface for ML antiquotations, struct_name is always "Isabelle";
wenzelm
parents:
34032
diff
changeset

242 
fun ml_code_antiq raw_const background = 
28054  243 
let 
31156  244 
val const = Code.check_const (ProofContext.theory_of background) raw_const; 
28054  245 
val is_first = is_first_occ background; 
246 
val background' = register_const const background; 

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

247 
in (print_code is_first const, background') end; 
30962  248 

28054  249 
end; (*local*) 
250 

251 

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

252 
(* reflection support *) 
36470  253 

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

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

256 
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

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

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

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

260 
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

261 
val _ = if null missing_constrs then [] 
b41aabb629ce
constructors to datatypes in code_reflect can be globbed; dropped unused code
haftmann
parents:
40320
diff
changeset

262 
else error ("Missing constructor(s) " ^ commas (map quote missing_constrs) 
b41aabb629ce
constructors to datatypes in code_reflect can be globbed; dropped unused code
haftmann
parents:
40320
diff
changeset

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

264 
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

265 
val _ = if null false_constrs then [] 
b41aabb629ce
constructors to datatypes in code_reflect can be globbed; dropped unused code
haftmann
parents:
40320
diff
changeset

266 
else error ("Nonconstructor(s) " ^ commas (map quote false_constrs) 
b41aabb629ce
constructors to datatypes in code_reflect can be globbed; dropped unused code
haftmann
parents:
40320
diff
changeset

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

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

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

270 
in (tyco, constrs) end; 
36470  271 

272 
fun add_eval_tyco (tyco, tyco') thy = 

273 
let 

274 
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

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

276 
 pr pr' _ [ty] = 
36470  277 
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

278 
 pr pr' _ tys = 
36470  279 
Code_Printer.concat [Code_Printer.enum "," "(" ")" (map (pr' Code_Printer.BR) tys), tyco'] 
280 
in 

281 
thy 

38923  282 
> Code_Target.add_tyco_syntax target tyco (SOME (k, pr)) 
36470  283 
end; 
284 

36514  285 
fun add_eval_constr (const, const') thy = 
286 
let 

287 
val k = Code.args_number thy const; 

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

38922  289 
(const' :: the_list (Code_Printer.tuplify pr' Code_Printer.BR (map fst ts))); 
36514  290 
in 
291 
thy 

38923  292 
> Code_Target.add_const_syntax target const (SOME (Code_Printer.simple_const_syntax (k, pr))) 
36514  293 
end; 
294 

38923  295 
fun add_eval_const (const, const') = Code_Target.add_const_syntax target 
36470  296 
const (SOME (Code_Printer.simple_const_syntax (0, (K o K o K) const'))); 
297 

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

298 
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

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

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

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

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

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

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

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

307 
val preamble = 
bc285d91041e
moved basic thy file name operations from Thy_Load to Thy_Header;
wenzelm
parents:
37744
diff
changeset

308 
"(* Generated from " ^ Path.implode (Thy_Header.thy_path (Context.theory_name thy)) 
36470  309 
^ "; DO NOT EDIT! *)"; 
39912
2ffe7060ca75
avoid antiquotation processing for code_reflect; moved ML_Context.value to Code_Runtime
haftmann
parents:
39816
diff
changeset

310 
val _ = File.write (Path.explode file_name) (preamble ^ "\n\n" ^ code); 
36470  311 
in 
312 
thy 

313 
end; 

314 

315 
fun gen_code_reflect prep_type prep_const raw_datatypes raw_functions module_name some_file thy = 

316 
let 

317 
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

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

319 
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

320 
> apsnd flat; 
36470  321 
val functions = map (prep_const thy) raw_functions; 
36514  322 
val result = evaluation_code thy module_name tycos (constrs @ functions) 
323 
> (apsnd o apsnd) (chop (length constrs)); 

36470  324 
in 
325 
thy 

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

326 
> process_reflection result module_name some_file 
36470  327 
end; 
328 

39422  329 
val code_reflect = gen_code_reflect Code_Target.cert_tyco (K I); 
36470  330 
val code_reflect_cmd = gen_code_reflect Code_Target.read_tyco Code.read_const; 
331 

332 

28054  333 
(** Isar setup **) 
334 

335 
val _ = ML_Context.add_antiq "code" (fn _ => Args.term >> ml_code_antiq); 

336 

36470  337 
local 
338 

339 
val datatypesK = "datatypes"; 

340 
val functionsK = "functions"; 

341 
val fileK = "file"; 

342 
val andK = "and" 

343 

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

344 
val _ = List.app Keyword.keyword [datatypesK, functionsK]; 
36470  345 

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

346 
val parse_datatype = 
40711
81bc73585eec
globbing constant expressions use more idiomatic underscore rather than star
haftmann
parents:
40422
diff
changeset

347 
Parse.name  Parse.$$$ "="  
81bc73585eec
globbing constant expressions use more idiomatic underscore rather than star
haftmann
parents:
40422
diff
changeset

348 
(((Parse.sym_ident  Parse.string) >> (fn "_" => NONE  _ => Scan.fail ())) 
40421
b41aabb629ce
constructors to datatypes in code_reflect can be globbed; dropped unused code
haftmann
parents:
40320
diff
changeset

349 
 ((Parse.term ::: (Scan.repeat (Parse.$$$ ""  Parse.term))) >> SOME)); 
36470  350 

351 
in 

352 

353 
val _ = 

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

354 
Outer_Syntax.command "code_reflect" "enrich runtime environment with generated code" 
01594f816e3a
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents:
36610
diff
changeset

355 
Keyword.thy_decl (Parse.name  Scan.optional (Parse.$$$ datatypesK  (parse_datatype 
01594f816e3a
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents:
36610
diff
changeset

356 
::: Scan.repeat (Parse.$$$ andK  parse_datatype))) [] 
01594f816e3a
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents:
36610
diff
changeset

357 
 Scan.optional (Parse.$$$ functionsK  Scan.repeat1 Parse.name) [] 
01594f816e3a
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents:
36610
diff
changeset

358 
 Scan.option (Parse.$$$ fileK  Parse.name) 
36534  359 
>> (fn (((module_name, raw_datatypes), raw_functions), some_file) => Toplevel.theory 
36470  360 
(code_reflect_cmd raw_datatypes raw_functions module_name some_file))); 
361 

362 
end; (*local*) 

363 

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

364 

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

365 
(** 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

366 

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

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

368 

39820  369 
structure Loaded_Values = Theory_Data 
370 
( 

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

371 
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

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

373 
val extend = I 
39820  374 
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

375 
); 
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 
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

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

379 
val _ = #enterVal ML_Env.name_space (string, value); 
c7cec137c48a
added polyml_as_definition  using external SML files as substitute for proper definitions  only for polyml!
haftmann
parents:
39605
diff
changeset

380 
val _ = Context.>> ((Context.map_theory o Loaded_Values.map) (insert (op =) string)); 
c7cec137c48a
added polyml_as_definition  using external SML files as substitute for proper definitions  only for polyml!
haftmann
parents:
39605
diff
changeset

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

382 

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

383 
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

384 

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

385 
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

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

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

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

389 
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

390 
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

391 
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

392 
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

393 
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

394 
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

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

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

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

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

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

400 
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

401 
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

402 
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

403 
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

404 
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

405 
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

406 
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

407 
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

408 
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

409 

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

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

411 

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

412 
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

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

414 
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

415 
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

416 
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

417 
(0, Path.implode filepath) false (File.read filepath); 
39912
2ffe7060ca75
avoid antiquotation processing for code_reflect; moved ML_Context.value to Code_Runtime
haftmann
parents:
39816
diff
changeset

418 
val thy'' = (Context.the_theory o the) (Context.thread_data ()); 
2ffe7060ca75
avoid antiquotation processing for code_reflect; moved ML_Context.value to Code_Runtime
haftmann
parents:
39816
diff
changeset

419 
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

420 
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

421 

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

422 
end; 
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 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

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

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

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

428 
> (fn ([Const (const, _)], _) => 
c7cec137c48a
added polyml_as_definition  using external SML files as substitute for proper definitions  only for polyml!
haftmann
parents:
39605
diff
changeset

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

430 
(SOME (Code_Printer.simple_const_syntax (0, (K o K o K o Code_Printer.str) ml_name))) 
2ffe7060ca75
avoid antiquotation processing for code_reflect; moved ML_Context.value to Code_Runtime
haftmann
parents:
39816
diff
changeset

431 
#> tap (fn thy => Code_Target.produce_code thy [const] target NONE "Code" [])); 
39816
c7cec137c48a
added polyml_as_definition  using external SML files as substitute for proper definitions  only for polyml!
haftmann
parents:
39605
diff
changeset

432 

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

433 
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

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

435 
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

436 
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

437 
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

438 
else error ("Value binding(s) " ^ commas_quote superfluous 
c7cec137c48a
added polyml_as_definition  using external SML files as substitute for proper definitions  only for polyml!
haftmann
parents:
39605
diff
changeset

439 
^ " found in external file " ^ quote (Path.implode filepath) 
c7cec137c48a
added polyml_as_definition  using external SML files as substitute for proper definitions  only for polyml!
haftmann
parents:
39605
diff
changeset

440 
^ " 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

441 
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

442 
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

443 
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

444 
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

445 

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

446 
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

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

448 
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

449 
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

450 
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

451 
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

452 
^ " 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

453 
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

454 

28054  455 
end; (*struct*) 