source: extracted/PROBLEMS @ 2601

Last change on this file since 2601 was 2601, checked in by sacerdot, 8 years ago

Extraction to ocaml is now working, with a couple of bugs left.
One limitation is that it is not possible to have two files with the
same name in different directories. Therefore this commit renames files
to avoid this situation.

The extracted directory contains:

  1. a snapshot of the .ml(i) files extracted from CerCo? by running ocamlc.opt -extract_ocaml compiler.ma The files have been patched by hand to implement all strings and fix the bugs.
  2. a file PROBLEMS that describes the remaining problems, i.e. bugs and axioms to be implemented

To obtain the compiler, run ocamlbuild compiler.byte.
At the moment it fails because of the three remaining axioms.

File size: 1.1 KB
Line 
1================
2EXTRACTION BUGS:
3================
4
51. ASM.subaddressing_modeel__o__mk_subaddressing_mode not extracted
6  val subaddressing_modeel__o__mk_subaddressing_mode:
7 Nat.nat -> Nat.nat -> addressing_mode_tag Vector.vector -> addressing_mode_tag Vector.vector -> addressing_mode -> addressing_mode
8
92. File "monad.ml", line 1, characters 0-1:
10Error: The implementation monad.ml does not match the interface monad.cmi:
11       Type declarations do not match:
12         type monad0 = Preamble.__
13       is not included in
14         type 'a monad0
15       They have different arities.
16
17Error: The implementation smallstepExec.ml
18       does not match the interface smallstepExec.cmi:
19       Type declarations do not match:
20         type global = Preamble.__
21       is not included in
22         type ('a, 'b) global
23       They have different arities.
24
25=========================
26AXIOMS TO BE IMPLEMENTED:
27=========================
28
29a) strings, String.string redefined to be string
30   FIXED BY HAND ATM
31b) two in compiler.ml (the backend and the compiler itself)
32c) registers.ml: register_ord
Note: See TracBrowser for help on using the repository browser.