equal
deleted
inserted
replaced
95 (* export_code functionality *) |
95 (* export_code functionality *) |
96 |
96 |
97 fun code thy permissive cs seris = |
97 fun code thy permissive cs seris = |
98 let |
98 let |
99 val code = Program.get thy; |
99 val code = Program.get thy; |
100 val seris' = map (fn (((target, module), file), args) => |
100 fun mk_seri_dest file = case file |
101 CodeTarget.get_serializer thy target permissive module file args cs) seris; |
101 of NONE => CodeTarget.compile |
102 in (map (fn f => f code) seris' : unit list; ()) end; |
102 | SOME "-" => writeln o CodeTarget.string |
|
103 | SOME f => CodeTarget.file (Path.explode f) |
|
104 val _ = map (fn (((target, module), file), args) => |
|
105 (mk_seri_dest file (CodeTarget.serialize thy target permissive module args code cs))) seris; |
|
106 in () end; |
103 |
107 |
104 (* evaluation machinery *) |
108 (* evaluation machinery *) |
105 |
109 |
106 fun evaluate eval_kind thy evaluator = |
110 fun evaluate eval_kind thy evaluator = |
107 let |
111 let |
143 val thy = Context.theory_of ctxt; |
147 val thy = Context.theory_of ctxt; |
144 val (ts, (ctxt', args')) = Scan.repeat1 Args.term (ctxt, args); |
148 val (ts, (ctxt', args')) = Scan.repeat1 Args.term (ctxt, args); |
145 val cs = map (CodeUnit.check_const thy) ts; |
149 val cs = map (CodeUnit.check_const thy) ts; |
146 val (cs', code') = generate thy (CodeFuncgr.make thy cs) |
150 val (cs', code') = generate thy (CodeFuncgr.make thy cs) |
147 (fold_map ooo ensure_const) cs; |
151 (fold_map ooo ensure_const) cs; |
148 val code'' = CodeTarget.sml_of thy cs' code' ^ " ()"; |
152 val code'' = CodeTarget.sml_of thy code' cs' ^ " ()"; |
149 in (("codevals", code''), (ctxt', args')) end; |
153 in (("codevals", code''), (ctxt', args')) end; |
150 |
154 |
151 |
155 |
152 (* const expressions *) |
156 (* const expressions *) |
153 |
157 |