diff options
Diffstat (limited to 'exportclight')
| -rw-r--r-- | exportclight/Clightdefs.v | 42 | ||||
| -rw-r--r-- | exportclight/ExportClight.ml | 30 |
2 files changed, 41 insertions, 31 deletions
diff --git a/exportclight/Clightdefs.v b/exportclight/Clightdefs.v index fda5bb55..83d82d88 100644 --- a/exportclight/Clightdefs.v +++ b/exportclight/Clightdefs.v @@ -15,17 +15,8 @@ (** All imports and definitions used by .v Clight files generated by clightgen *) -Require Export String. -Require Export List. -Require Export ZArith. -Require Export Integers. -Require Export Floats. -Require Export AST. -Require Export Ctypes. -Require Export Cop. -Require Export Clight. -Require Import Maps. -Require Import Errors. +From Coq Require Import String List ZArith. +From compcert Require Import Integers Floats Maps Errors AST Ctypes Cop Clight. Definition tvoid := Tvoid. Definition tschar := Tint I8 Signed noattr. @@ -65,8 +56,27 @@ Definition talignas (n: N) (ty: type) := Definition tvolatile_alignas (n: N) (ty: type) := tattr {| attr_volatile := true; attr_alignas := Some n |} ty. -Definition make_composite_env (comps: list composite_definition): composite_env := - match build_composite_env comps with - | OK e => e - | Error _ => PTree.empty _ - end. +Definition wf_composites (types: list composite_definition) : Prop := + match build_composite_env types with OK _ => True | Error _ => False end. + +Definition build_composite_env' (types: list composite_definition) + (WF: wf_composites types) + : { ce | build_composite_env types = OK ce }. +Proof. + revert WF. unfold wf_composites. case (build_composite_env types); intros. +- exists c; reflexivity. +- contradiction. +Defined. + +Definition mkprogram (types: list composite_definition) + (defs: list (ident * globdef fundef type)) + (public: list ident) + (main: ident) + (WF: wf_composites types) : Clight.program := + let (ce, EQ) := build_composite_env' types WF in + {| prog_defs := defs; + prog_public := public; + prog_main := main; + prog_types := types; + prog_comp_env := ce; + prog_comp_env_eq := EQ |}. diff --git a/exportclight/ExportClight.ml b/exportclight/ExportClight.ml index 8001dca7..f5b8150d 100644 --- a/exportclight/ExportClight.ml +++ b/exportclight/ExportClight.ml @@ -250,10 +250,10 @@ let external_function p = function | EF_free -> fprintf p "EF_free" | EF_memcpy(sz, al) -> fprintf p "(EF_memcpy %ld %ld)" (Z.to_int32 sz) (Z.to_int32 al) - | EF_annot(text, targs) -> + | EF_annot(kind,text, targs) -> assertions := (camlstring_of_coqstring text, targs) :: !assertions; fprintf p "(EF_annot %a %a)" coqstring text (print_list asttype) targs - | EF_annot_val(text, targ) -> + | EF_annot_val(kind,text, targ) -> assertions := (camlstring_of_coqstring text, [targ]) :: !assertions; fprintf p "(EF_annot_val %a %a)" coqstring text asttype targ | EF_debug(kind, text, targs) -> @@ -478,12 +478,11 @@ let print_assertions p = (* The prologue *) -let prologue = "\n\ -Require Import Clightdefs.\n\ -\ +let prologue = "\ +From Coq Require Import String List ZArith.\n\ +From compcert Require Import Coqlib Integers Floats AST Ctypes Cop Clight Clightdefs.\n\ Local Open Scope Z_scope.\n\ -\ -" +\n" (* Naming the compiler-generated temporaries occurring in the program *) @@ -550,13 +549,14 @@ let print_program p prog = fprintf p "Definition composites : list composite_definition :=@ "; print_list print_composite_definition p prog.prog_types; fprintf p ".@ @ "; - fprintf p "Definition prog : Clight.program := {|@ "; - fprintf p "prog_defs :=@ %a;@ " (print_list print_ident_globdef) prog.Ctypes.prog_defs; - fprintf p "prog_public :=@ %a;@ " (print_list ident) prog.Ctypes.prog_public; - fprintf p "prog_main := %a;@ " ident prog.Ctypes.prog_main; - fprintf p "prog_types := composites;@ "; - fprintf p "prog_comp_env := make_composite_env composites;@ "; - fprintf p "prog_comp_env_eq := refl_equal _@ "; - fprintf p "|}.@ "; + fprintf p "Definition global_definitions :=@ "; + print_list print_ident_globdef p prog.Ctypes.prog_defs; + fprintf p ".@ @ "; + fprintf p "Definition public_idents :=@ "; + print_list ident p prog.Ctypes.prog_public; + fprintf p ".@ @ "; + fprintf p "Definition prog : Clight.program := @ "; + fprintf p " mkprogram composites global_definitions public_idents %a Logic.I.@ @ " + ident prog.Ctypes.prog_main; print_assertions p; fprintf p "@]@." |