Permalink
Browse files

Add theory for compiling wordfreq in logic

  • Loading branch information...
xrchz committed May 24, 2017
1 parent 957a035 commit 6de6f7a0e7743b93ac7d22742354d13a51c4344a
Showing with 23 additions and 1 deletion.
  1. +1 −1 tutorial/Holmakefile
  2. +17 −0 tutorial/wordfreqCompileScript.sml
  3. +5 −0 tutorial/wordfreqProgScript.sml
@@ -1 +1 @@
INCLUDES = $(HOLDIR)/examples/balanced_bst .. ../translator ../basis/pure ../basis ../characteristic
INCLUDES = $(HOLDIR)/examples/balanced_bst .. ../translator ../basis/pure ../basis ../characteristic ../compiler
@@ -0,0 +1,17 @@
(*
Compile the wordfreq program to machine code by evaluation of the compiler in
the logic.
*)

open preamble wordfreqProgTheory compilationLib

val _ = new_theory"wordfreqCompile";

val wordfreq_compiled = save_thm("wordfreq_compiled",
compile_x64
1000 (* stack size in MB *)
1000 (* heap size in MB *)
"wordfreq"
wordfreq_prog_def);

val _ = export_theory();
@@ -167,6 +167,11 @@ val spec = wordfreq_spec |> SPEC_ALL |> UNDISCH_ALL |> add_basis_proj;
val name = "wordfreq"
val (sem_thm,prog_tm) = ioProgLib.call_thm (get_ml_prog_state ()) name spec
val wordfreq_prog_def = Define `wordfreq_prog = ^prog_tm`;

(* TODO:
want a way to print this program out as concrete syntax (to be fed
into the bootstrapped compiler for example) *)

val wordfreq_semantics =
sem_thm
|> ONCE_REWRITE_RULE[GSYM wordfreq_prog_def]

0 comments on commit 6de6f7a

Please sign in to comment.