source: src/Cminor/Cminor_abstract.ma @ 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: 953 bytes
Line 
1include "Cminor/Cminor_semantics.ma".
2
3(* Avoid aliasing in interstage proofs *)
4
5definition Cminor_state ≝ state.
6
7(* States about to execute a cost statement.  Other statements may also emit
8   cost labels due to expressions, but these are the only ones relevant for
9   defining measurable subtraces. *)
10
11definition Cminor_labelled : state → bool ≝
12λs. match s with
13[ State _ st _ _ _ _ _ _ _ _ ⇒ match st with [ St_cost _ _ ⇒ true | _ ⇒ false ]
14| _ ⇒ false
15].
16
17(* Usual classification *)
18
19(* only for classification type *)
20include "common/StructuredTraces.ma".
21
22definition Cminor_classify : state → status_class ≝
23λs. match s with
24[ State _ _ _ _ _ _ _ _ _ _ ⇒ cl_other
25| Callstate _ _ _ _ ⇒ cl_call
26| Returnstate _ _ _ ⇒ cl_return
27| Finalstate _ ⇒ cl_other
28].
29
30definition cm_genv ≝ genv.
31
32definition cm_env ≝ env.
33
34definition cm_cont ≝ cont.
35
36definition cm_eval_expr ≝ eval_expr.
37
38definition CmState ≝ State.
39
Note: See TracBrowser for help on using the repository browser.