Add support to clightgen for generating Csyntax AST as .v files

As proposed in #404.

This is presented as a new option `-clight` to the existing `clightgen` tool.

Revise clightgen testing to test the Csyntax output in addition to
the Clight output.

1 files changed, 65 insertions, 0 deletions

diff --git a/export/Csyntaxdefs.v b/export/Csyntaxdefs.v
new file mode 100644
index 00000000..84ce9f3a
--- /dev/null
+++ b/export/Csyntaxdefs.v
@@ -0,0 +1,65 @@
+(* *********************************************************************)
+(*                                                                     *)
+(*              The Compcert verified compiler                         *)
+(*                                                                     *)
+(*          Xavier Leroy, INRIA Paris-Rocquencourt                     *)
+(*                                                                     *)
+(*  Copyright Institut National de Recherche en Informatique et en     *)
+(*  Automatique.  All rights reserved.  This file is distributed       *)
+(*  under the terms of the GNU Lesser General Public License as        *)
+(*  published by the Free Software Foundation, either version 2.1 of   *)
+(*  the License, or  (at your option) any later version.               *)
+(*  This file is also distributed under the terms of the               *)
+(*  INRIA Non-Commercial License Agreement.                            *)
+(*                                                                     *)
+(* *********************************************************************)
+
+(** Definitions used by .v files generated by clightgen -csyntax *)
+
+From Coq Require Import List.
+From compcert Require Import Maps Errors AST Ctypes Csyntax.
+From compcert Require Export Ctypesdefs.
+
+(** ** Constructor for programs and compilation units *)
+
+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) : Csyntax.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 |}.
+
+(** ** Notations *)
+
+Module CsyntaxNotations.
+
+(** A convenient notation [$ "ident"] to force evaluation of
+    [ident_of_string "ident"] *)
+
+Ltac ident_of_string s :=
+  let x := constr:(ident_of_string s) in
+  let y := eval compute in x in
+  exact y.
+
+Notation "$ s" := (ltac:(ident_of_string s))
+                  (at level 1, only parsing) : csyntax_scope.
+
+End CsyntaxNotations.