@@ -215,11 +215,7 @@ Theorem evaluate_prog_thm =
215215
216216
217217val env = get_ml_prog_state() |> ml_progLib.get_env
218- val st = get_ml_prog_state () |> ml_progLib.get_state
219- *)
220-
221-
222- (* )
218+ val st = get_ml_prog_state () |> ml_progLib.get_state
223219ml_progLib.get_Decls_thm (get_ml_prog_state())
224220*)
225221
@@ -235,50 +231,6 @@ val _ = astToSexprLib.write_ast_to_file "test_new.sexp" prog_tm;
235231
236232
237233
238- (*
239- val _ = astToSexprLib.write_ast_to_file "test_new.sexp"
240- (“SNOC
241- (Dlet unknown_loc (Pcon NONE [])
242- (App Opapp [Var (Short "main"); Con NONE []]))
243- ^(get_ml_prog_state() |> get_prog)”
244- |> EVAL |> concl |> rhs) ;
245-
246-
247-
248-
249-
250- val res = append_prog o process_topdecs $ `
251- fun main () =
252- let
253- val args = CommandLine.arguments()
254- val zero_flags = ["-0","--zero"]
255- val help_flags = ["-h","--help"]
256- val help = List.exists (fn f => List.member f help_flags) args
257- val zero = List.exists (fn f => List.member f zero_flags) args
258- val args_filter = List.filter
259- (fn f => not(List.member f (zero_flags @ help_flags))) args
260- val split_char = Char.chr (if zero then 0 else 10)
261- val content = case args_filter of
262- [] => TextIO.inputAll TextIO.stdIn
263- | args => String.concat (List.map (TextIO.inputAll o TextIO.openIn) args)
264- val content_lines = String.tokens (fn c => c = split_char) content
265- in
266- if help then
267- TextIO.print help_string
268- else
269- TextIO.print
270- (String.concatWith
271- (String.str split_char)
272- (List.map (String.implode o qrev o String.explode) content_lines))
273- end;
274- `;
275-
276-
277- *)
278-
279-
280-
281-
282234
283235(* ***************************************************)
284236
@@ -287,15 +239,13 @@ end;
287239val current_prog =
288240Decls_thm |> concl |> strip_comb |> #2 |> el 3
289241
290-
291-
292-
293242val _ = astPP.enable_astPP ();
294243print_term (current_prog);
295244val _ = astPP.disable_astPP();
296245*)
297246
298247
248+ (*
299249(* to get the binary *)
300250open eval_cake_compile_x64Lib;
301251(* val state = get_ml_prog_state();
@@ -304,9 +254,10 @@ val bdd_prog_def = Define ‘out_prog = ^prog_tm’ ;
304254
305255Theorem blah_compiled =
306256 eval_cake_compile_x64 "" bdd_prog_def "bew_bdd.S";
257+ *)
307258
308259
309- (* )
260+ (*
310261val Decls_thm =
311262 get_ml_prog_state ()
312263 |> ml_progLib.clean_state
@@ -372,8 +323,6 @@ val prog =
372323
373324val _ = astToSexprLib.write_ast_to_file "revProg.sexp" prog;
374325
375-
376-
377326 *)
378327
379328
0 commit comments