Changeset 2601


Ignore:
Timestamp:
Feb 5, 2013, 1:36:31 PM (7 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.

Files:
191 added
20 edited
15 moved

Legend:

Unmodified
Added
Removed
  • src/ASM/BitVector.ma

    r2126 r2601  
    226226qed.
    227227
     228(*
    228229axiom bitvector_of_string:
    229230  ∀n: nat.
     
    235236  ∀b: BitVector n.
    236237    String.
     238*)
    237239
    238240lemma bitvector_3_cases:
  • src/Clight/toCminor.ma

    r2588 r2601  
    245245] qed.
    246246
    247 include "Cminor/syntax.ma".
     247include "Cminor/Cminor_syntax.ma".
    248248include "common/Errors.ma".
    249249
    250 alias id "CMexpr" = "cic:/matita/cerco/Cminor/syntax/expr.ind(1,0,0)".
     250alias id "CMexpr" = "cic:/matita/cerco/Cminor/Cminor_syntax/expr.ind(1,0,0)".
    251251
    252252axiom BadlyTypedAccess : String.
  • src/Clight/toCminorCorrectness.ma

    r2598 r2601  
    33include "common/Globalenvs.ma".
    44include "Clight/memoryInjections.ma".
    5 include "Clight/abstract.ma".
    6 include "Cminor/abstract.ma".
     5include "Clight/Clight_abstract.ma".
     6include "Cminor/Cminor_abstract.ma".
    77
    88(* Expr simulation. Contains important definitions for statements, too.  *)
  • src/Clight/toCminorCorrectnessExpr.ma

    r2600 r2601  
    44include "Clight/toCminorOps.ma".
    55include "Clight/memoryInjections.ma".
    6 include "Clight/abstract.ma".
    7 include "Cminor/abstract.ma".
     6include "Clight/Clight_abstract.ma".
     7include "Cminor/Cminor_abstract.ma".
    88
    99record clight_cminor_inv : Type[0] ≝ {
  • src/Clight/toCminorOps.ma

    r2600 r2601  
    11include "Clight/toCminor.ma".
    22include "Clight/Cexec.ma".
    3 include "Clight/abstract.ma".
    4 include "Cminor/abstract.ma".
     3include "Clight/Clight_abstract.ma".
     4include "Cminor/Cminor_abstract.ma".
    55include "Clight/frontend_misc.ma".
    66include "Clight/memoryInjections.ma".
  • src/Cminor/Cminor_abstract.ma

    r2600 r2601  
    1 include "Cminor/semantics.ma".
     1include "Cminor/Cminor_semantics.ma".
    22
    33(* Avoid aliasing in interstage proofs *)
  • src/Cminor/Cminor_semantics.ma

    r2600 r2601  
    55include "common/SmallstepExec.ma".
    66
    7 include "Cminor/syntax.ma".
     7include "Cminor/Cminor_syntax.ma".
    88include alias "basics/logic.ma".
    99
  • src/Cminor/initialisation.ma

    r2468 r2601  
    22(* Replace initialisation of global variables with equivalent Cminor code. *)
    33
    4 include "Cminor/syntax.ma".
     4include "Cminor/Cminor_syntax.ma".
    55include "common/Globalenvs.ma".
    66
  • 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'.
  • src/Cminor/toRTLabsCorrectness.ma

    r2597 r2601  
    11
    2 include "Cminor/abstract.ma".
    3 include "RTLabs/abstract.ma".
     2include "Cminor/Cminor_abstract.ma".
     3include "RTLabs/RTLabs_abstract.ma".
    44include "Cminor/toRTLabs.ma".
    55
  • src/ERTLptr/ERTLptr_semantics.ma

    r2600 r2601  
    11include "joint/semanticsUtils.ma".
    22include "ERTLptr/ERTLptr.ma". (* CSC: syntax.ma in RTLabs *)
    3 include "ERTL/semantics.ma".
     3include "ERTL/ERTL_semantics.ma".
    44include alias "common/Identifiers.ma".
    55
  • src/ERTLptr/ERTLtoERTLptrOK.ma

    r2592 r2601  
    1717include "common/StatusSimulation.ma".   
    1818include "joint/Traces.ma".
    19 include "ERTLptr/semantics.ma".
     19include "ERTLptr/ERTLptr_semantics.ma".
    2020include "common/ExtraMonads.ma".
    2121
  • src/RTLabs/CostCheck.ma

    r2315 r2601  
    11
    22include "RTLabs/CostSpec.ma".
    3 include "utilities/bool.ma".
     3include "utilities/extra_bool.ma".
    44include "utilities/listb.ma".
    55include "RTLabs/CostMisc.ma".
  • src/RTLabs/CostInj.ma

    r2420 r2601  
    1 include "RTLabs/Traces.ma".
     1include "RTLabs/RTLabs_traces.ma".
    22
    33(* Check that the RTLabs pc → cost label map is injective for a given RTLabs
  • src/RTLabs/CostSpec.ma

    r2307 r2601  
    11
    2 include "RTLabs/syntax.ma".
     2include "RTLabs/RTLabs_syntax.ma".
    33
    44(* We define a boolean cost label function on statements as well as a cost
  • src/RTLabs/MeasurableTraces.ma

    r2511 r2601  
    11include "common/Measurable.ma".
    2 include "RTLabs/Traces.ma".
     2include "RTLabs/RTLabs_traces.ma".
    33
    44definition RTLabs_system : preclassified_system ≝
  • src/RTLabs/RTLabsToRTL.ma

    r2505 r2601  
    1 include "RTLabs/syntax.ma".
     1include "RTLabs/RTLabs_syntax.ma".
    22include "RTL/RTL.ma".
    33include "common/AssocList.ma".
  • src/RTLabs/RTLabs_abstract.ma

    r2600 r2601  
    1 include "RTLabs/semantics.ma".
     1include "RTLabs/RTLabs_semantics.ma".
    22
    33(* Avoid aliasing in interstage proofs *)
  • src/RTLabs/RTLabs_semantics.ma

    r2600 r2601  
    77include "common/SmallstepExec.ma".
    88
    9 include "RTLabs/syntax.ma".
     9include "RTLabs/RTLabs_syntax.ma".
    1010
    1111definition genv ≝ genv_t (fundef internal_function).
  • src/RTLabs/RTLabs_traces.ma

    r2600 r2601  
    11
    2 include "RTLabs/abstract.ma".
     2include "RTLabs/RTLabs_abstract.ma".
    33include "RTLabs/CostSpec.ma".
    44include "RTLabs/CostMisc.ma".
  • src/RTLabs/debug.ma

    r797 r2601  
    11include "common/Animation.ma".
    2 include "RTLabs/semantics.ma".
     2include "RTLabs/RTLabs_semantics.ma".
    33
    44inductive ministate : Type[0] ≝
  • src/RTLabs/import.ma

    r1633 r2601  
    11
    2 include "RTLabs/semantics.ma".
     2include "RTLabs/RTLabs_semantics.ma".
    33
    44let rec n_idents (n:nat) (tag:String) (g:universe tag) : Vector (identifier tag) n × (universe tag) ≝
  • src/common/Globalenvs.ma

    r2471 r2601  
    11201120}.
    11211121
    1122 include "utilities/bool.ma".
     1122include "utilities/extra_bool.ma".
    11231123
    11241124theorem transform_program_gen_related : ∀tag,A,B,V,init,g,p. ∀tf:∀vs. universe tag → A vs → B vs × (universe tag).
  • src/joint/Traces.ma

    r2590 r2601  
    1 include "joint/semantics.ma".
     1include "joint/joint_semantics.ma".
    22include "common/StructuredTraces.ma".
    33
  • src/joint/semanticsUtils.ma

    r2529 r2601  
    1 include "joint/semantics.ma".
     1include "joint/joint_semantics.ma".
    22include alias "common/Identifiers.ma".
    33include "utilities/hide.ma".
  • src/joint/stacksize.ma

    r2456 r2601  
    11include "basics/lists/list.ma".
    2 include "joint/semantics.ma".
     2include "joint/joint_semantics.ma".
    33include "common/Executions.ma".
    44include "common/StructuredTraces.ma".
Note: See TracChangeset for help on using the changeset viewer.