Remove compilerTheory (put its content at end of codegenTheory)

HOL-Theorem-Prover · Mar 11, 2024 · 3a51c81 · 3a51c81
1 parent 772a64a
commit 3a51c81
Show file tree

Hide file tree

Showing 6 changed files with 11 additions and 22 deletions.
diff --git a/examples/bootstrap/README.md b/examples/bootstrap/README.md
@@ -20,8 +20,8 @@ Functions and proofs about lexing, parsing and pretty printing of source code:
  - [parsing_proofsScript.sml](parsing_proofsScript.sml)
  - [printingScript.sml](printingScript.sml)
 
-Top-level compiler definition as shallow embedding:
- - [compilerScript.sml](compilerScript.sml)
+Top-level compiler definition as shallow embedding is at the bottom of:
+ - [codegenScript.sml](codegenScript.sml)
 
 Automation that converts shallow embeddings into deep embeddings:
  - [automation_lemmasScript.sml](automation_lemmasScript.sml)

diff --git a/examples/bootstrap/codegenScript.sml b/examples/bootstrap/codegenScript.sml
@@ -2,6 +2,7 @@
 open HolKernel Parse boolLib bossLib;
 open arithmeticTheory listTheory pairTheory finite_mapTheory stringTheory;
 open source_valuesTheory source_syntaxTheory x64asm_syntaxTheory;
+open parsingTheory wordsLib;
 
 val _ = new_theory "codegen";
 
@@ -333,4 +334,9 @@ Definition codegen_def:
       flatten (Append (List (init (k+1))) c) []
 End
 
+Definition compiler_def:
+  compiler input =
+    asm2str (codegen (parser (lexer input)))
+End
+
 val _ = export_theory();
diff --git a/examples/bootstrap/compilerScript.sml b/examples/bootstrap/compilerScript.sml
diff --git a/examples/bootstrap/compiler_evalScript.sml b/examples/bootstrap/compiler_evalScript.sml
@@ -1,7 +1,7 @@
 
 open HolKernel Parse boolLib bossLib term_tactic;
 open arithmeticTheory listTheory pairTheory finite_mapTheory stringTheory;
-open wordsTheory wordsLib automationLib compilerTheory compiler_progTheory;
+open wordsTheory wordsLib automationLib compiler_progTheory;
 
 val _ = new_theory "compiler_eval";
 
@@ -25,5 +25,4 @@ Theorem compiler_asm_str  = time EVAL “compiler_asm_str”;
 val _ = write_hol_string_to_file "compiler_prog.txt" (compiler_str |> concl |> rand);
 val _ = write_hol_string_to_file "compiler_asm.s"    (compiler_asm_str |> concl |> rand);
 
-
 val _ = export_theory();
diff --git a/examples/bootstrap/compiler_progScript.sml b/examples/bootstrap/compiler_progScript.sml
@@ -3,7 +3,7 @@ open HolKernel Parse boolLib bossLib term_tactic;
 open arithmeticTheory listTheory pairTheory finite_mapTheory stringTheory;
 open source_valuesTheory source_syntaxTheory source_semanticsTheory mp_then
      source_propertiesTheory parsingTheory codegenTheory x64asm_syntaxTheory
-     wordsTheory wordsLib automation_lemmasTheory automationLib compilerTheory;
+     wordsTheory wordsLib automation_lemmasTheory automationLib;
 
 val _ = new_theory "compiler_prog";
 

diff --git a/examples/bootstrap/compiler_proofsScript.sml b/examples/bootstrap/compiler_proofsScript.sml
@@ -20,7 +20,7 @@ QED
 Theorem compiler_compiler_str:
   compiler compiler_str = compiler_asm_str
 Proof
-  fs [compiler_str_def,compilerTheory.compiler_def,
+  fs [compiler_str_def,codegenTheory.compiler_def,
       parser_lexer_prog2str,compiler_asm_str_def,compiler_asm_def]
 QED