Ignore:
Timestamp:
Feb 5, 2013, 1:36:31 PM (8 years ago)
Author:
sacerdot
Message:

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:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Cminor/toRTLabs.ma

    r2390 r2601  
    11include "utilities/lists.ma".
    22include "common/Globalenvs.ma".
    3 include "Cminor/syntax.ma".
    4 include "RTLabs/syntax.ma".
     3include "Cminor/Cminor_syntax.ma".
     4include "RTLabs/RTLabs_syntax.ma".
    55
    66definition env ≝ identifier_map SymbolTag (register × typ).
     
    588588
    589589(* XXX Work around odd disambiguation errors. *)
    590 alias id "R_skip" = "cic:/matita/cerco/RTLabs/syntax/statement.con(0,1,0)".
     590alias id "R_skip" = "cic:/matita/cerco/RTLabs/RTLabs_syntax/statement.con(0,1,0)".
    591591(* If reenabling tailcalls, change 12 to 14. *)
    592 alias id "R_return" = "cic:/matita/cerco/RTLabs/syntax/statement.con(0,11,0)".
     592alias id "R_return" = "cic:/matita/cerco/RTLabs/RTLabs_syntax/statement.con(0,11,0)".
    593593
    594594lemma empty_Cminor_labels_added : ∀fx,s,f'.
Note: See TracChangeset for help on using the changeset viewer.