Permalink
Browse files

Initial commit

Corresponds to the $HOLDIR/examples/miniML/ directory in commit
  f9bf2f1261f3a5bab3b8889c3c63f0d3e0740447
of
  https://github.com/mn200/HOL
(master branch)

(So see that repository for previous history.)

Minor change: renamed `hol2miniml' to `translator'
  • Loading branch information...
0 parents commit 5ae13774a2df62a3fad50b83a32c270786cd03bb @xrchz xrchz committed Oct 9, 2012
Showing with 33,128 additions and 0 deletions.
  1. +14 −0 .gitignore
  2. +38 −0 README
  3. +459 −0 compiler/CexpTypesScript.sml
  4. +1,608 −0 compiler/CompileScript.sml
  5. +13 −0 compiler/Holmakefile
  6. +10 −0 compiler/Makefile
  7. +270 −0 compiler/bytecode/BytecodeScript.sml
  8. +1 −0 compiler/bytecode/Holmakefile
  9. +4 −0 compiler/bytecode/Makefile
  10. +2 −0 compiler/bytecode/benchmarking/Holmakefile
  11. +10 −0 compiler/bytecode/benchmarking/Makefile
  12. +116 −0 compiler/bytecode/benchmarking/asm_exec.s
  13. +10 −0 compiler/bytecode/benchmarking/bytecode_testerLib.sig
  14. +48 −0 compiler/bytecode/benchmarking/bytecode_testerLib.sml
  15. +178 −0 compiler/bytecode/benchmarking/bytecode_x64Script.sml
  16. +55 −0 compiler/bytecode/benchmarking/wrapper.c
  17. +233 −0 compiler/bytecode/bytecode.lem
  18. +331 −0 compiler/bytecode/bytecodeEvalScript.sml
  19. +17 −0 compiler/bytecode/bytecodeTerminationScript.sml
  20. +1,575 −0 compiler/bytecode/hw_bytecodeScript.sml
  21. +1,477 −0 compiler/compile.lem
  22. +211 −0 compiler/compileTerminationScript.sml
  23. +13 −0 compiler/correctness/Holmakefile
  24. +5 −0 compiler/correctness/TODO
  25. +374 −0 compiler/correctness/codeEnvScript.sml
  26. +258 −0 compiler/correctness/compileCorrectnessScript.sml
  27. +1,226 −0 compiler/correctness/expToCexpScript.sml
  28. +1,624 −0 compiler/correctness/intLangScript.sml
  29. +574 −0 compiler/correctness/miniMLExtraScript.sml
  30. +406 −0 compiler/correctness/miscScript.sml
  31. +1,204 −0 compiler/correctness/pmatchScript.sml
  32. +70 −0 compiler/count_exp/count_expScript.sml
  33. +27 −0 compiler/emit/Holmakefile
  34. +96 −0 compiler/emit/benchmark.sml
  35. +184 −0 compiler/emit/benchmarkScript.sml
  36. +40 −0 compiler/emit/bytecode_emitScript.sml
  37. +25 −0 compiler/emit/bytecode_x64_emitScript.sml
  38. +127 −0 compiler/emit/compile_emitScript.sml
  39. +32 −0 compiler/emit/hw_bytecode_emitScript.sml
  40. +86 −0 compiler/emit/hw_test.sml
  41. +7 −0 compiler/emit/selftest.exe
  42. +422 −0 compiler/emit/test_compiler.sml
  43. +133 −0 compiler/emit/test_compilerLib.sml
  44. +11 −0 compiler/lib.lem
  45. +1 −0 computability/Holmakefile
  46. +23 −0 computability/mlrecfunScript.sml
  47. +2 −0 lexer/Holmakefile
  48. +71 −0 lexer/dfaScript.sml
  49. +609 −0 lexer/lexer_runtimeScript.sml
  50. +115 −0 lexer/lexer_specScript.sml
  51. +2 −0 metatheory/Holmakefile
  52. +141 −0 metatheory/bigBigEquivScript.sml
  53. +1,193 −0 metatheory/bigSmallEquivScript.sml
  54. +89 −0 metatheory/determScript.sml
  55. +142 −0 metatheory/evaluateEquationsScript.sml
  56. +1,747 −0 metatheory/typeSoundScript.sml
  57. +874 −0 metatheory/typeSubstitutionScript.sml
  58. +125 −0 metatheory/untypedSafetyScript.sml
  59. +13 −0 preamble.sml
  60. +2 −0 semantics/Holmakefile
  61. +235 −0 semantics/MLlexerScript.sml
  62. +2 −0 semantics/Makefile
  63. +2,199 −0 semantics/MiniMLScript.sml
  64. +144 −0 semantics/MiniMLTerminationScript.sml
  65. +541 −0 semantics/Print_astScript.sml
  66. +81 −0 semantics/Print_astTerminationScript.sml
  67. +14 −0 semantics/lib.lem
  68. +2,065 −0 semantics/miniML.lem
  69. +477 −0 semantics/print_ast.lem
  70. +40 −0 semantics/print_astProofsScript.sml
  71. +13 −0 translator/Holmakefile
  72. +24 −0 translator/mini_preludeScript.sml
  73. +638 −0 translator/ml_optimiseScript.sml
  74. +36 −0 translator/ml_translatorLib.sig
  75. +1,956 −0 translator/ml_translatorLib.sml
  76. +640 −0 translator/ml_translatorScript.sml
  77. +54 −0 translator/ml_translator_demoScript.sml
  78. +69 −0 translator/okasaki-examples/BankersQueueScript.sml
  79. +62 −0 translator/okasaki-examples/BatchedQueueScript.sml
  80. +87 −0 translator/okasaki-examples/BinaryRandomAccessListsScript.sml
  81. +497 −0 translator/okasaki-examples/BinomialHeapScript.sml
  82. +264 −0 translator/okasaki-examples/BottomUpMergeSortScript.sml
  83. +13 −0 translator/okasaki-examples/Holmakefile
  84. +109 −0 translator/okasaki-examples/HoodMelvilleQueueScript.sml
  85. +213 −0 translator/okasaki-examples/ImplicitQueueScript.sml
  86. +256 −0 translator/okasaki-examples/LazyPairingHeapScript.sml
  87. +167 −0 translator/okasaki-examples/LeftistHeapScript.sml
  88. +162 −0 translator/okasaki-examples/PairingHeapScript.sml
  89. +94 −0 translator/okasaki-examples/PhysicistsQueueScript.sml
  90. +92 −0 translator/okasaki-examples/RealTimeQueueScript.sml
  91. +369 −0 translator/okasaki-examples/RedBlackSetScript.sml
  92. +315 −0 translator/okasaki-examples/SplayHeapScript.sml
  93. +85 −0 translator/okasaki-examples/UnbalancedSetScript.sml
  94. +105 −0 translator/okasaki-examples/miscScript.sml
  95. +32 −0 translator/okasaki-examples/test.ml
  96. +2 −0 translator/okasaki-examples/test.sh
  97. +18 −0 translator/other-examples/Holmakefile
  98. +1 −0 translator/other-examples/auxiliary/Holmakefile
  99. +77 −0 translator/other-examples/auxiliary/copying_gcScript.sml
  100. +161 −0 translator/other-examples/auxiliary/ninetyOneScript.sml
  101. +847 −0 translator/other-examples/auxiliary/regexpMatchScript.sml
  102. +180 −0 translator/other-examples/auxiliary/slr_parser_genScript.sml
  103. +15 −0 translator/other-examples/example_91Script.sml
  104. +62 −0 translator/other-examples/example_aesScript.sml
  105. +16 −0 translator/other-examples/example_copying_gcScript.sml
  106. +31 −0 translator/other-examples/example_parser_genScript.sml
  107. +67 −0 translator/other-examples/example_primality_testScript.sml
  108. +17 −0 translator/other-examples/example_qsortScript.sml
  109. +43 −0 translator/other-examples/example_rc6Script.sml
  110. +16 −0 translator/other-examples/example_regexp_matcherScript.sml
  111. +34 −0 translator/other-examples/example_teaScript.sml
  112. +21 −0 translator/other-examples/test.ml
  113. +2 −0 translator/other-examples/test.sh
  114. +423 −0 translator/std_preludeScript.sml
  115. +172 −0 translator/word_preludeScript.sml
@@ -0,0 +1,14 @@
+# HOL stuff
+*Script
+*Theory.sig
+*Theory.sml
+*.uo
+*.ui
+*.o
+.HOLMK
+
+# HOLHEAP
+miniml-heap
+
+# Translator stuff
+*txt
38 README
@@ -0,0 +1,38 @@
+Directory structure:
+
+- semantics
+ The definition of MiniML, including
+ - its abstract syntax
+ - small step semantics
+ - big step semantics
+ - a type system
+ - a printer for MiniML's AST.
+ The definition is expressed in Lem (http://www.cl.cam.ac.uk/~so294/lem),
+ but might not work on the released version at any given time, so the
+ generated HOL is also included.
+
+- metatheory
+ Proofs about MiniML, including
+ - type soundness
+ - determinism
+ - equivalence of the big and small step semantics
+
+- translator
+ A proof-producing translator from HOL functions to MiniML
+
+- translator/okasaki-examples
+ 15 data structures/algorithms from Chris Okasaki's Purely Functional Data
+ Structures. The translator is applied to them, and 12 of the 15 are
+ verified.
+
+- translator/other-examples
+ Example applications of the translator to existing examples, including AES,
+ TEA, and RC6 from HOL/examples/Crypto; the probabilistic primality checker
+ from examples/miller; and some examples in auxiliary.
+
+- translator/other-examples/auxiliary
+ A copying GC, 91 function, regular expression matched and SLR parser
+ generator taken from other places, and ollected here for the translator.
+
+- compiler
+ The sketchy beginnings of a verified compiler from MiniML to ???
Oops, something went wrong.

0 comments on commit 5ae1377

Please sign in to comment.