DXModule.v

(**************************************************************************)
(*  This file is part of dx, a tool to derive C from monadic Gallina.     *)
(*                                                                        *)
(*  Copyright (C) 2024 Université de Lille & CNRS                         *)
(*                                                                        *)
(*  This program is free software; you can redistribute it and/or modify  *)
(*  it under the terms of the GNU General Public License as published by  *)
(*  the Free Software Foundation; either version 2 of the License, or     *)
(*  (at your option) any later version.                                   *)
(*                                                                        *)
(*  This program is distributed in the hope that it will be useful,       *)
(*  but WITHOUT ANY WARRANTY; without even the implied warranty of        *)
(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the         *)
(*  GNU General Public License for more details.                          *)
(**************************************************************************)

From Coq Require Import String.

From compcert.common Require AST.
From compcert.cfrontend Require Csyntax Ctypes.

(* Pack together the content of a C module (identifiers and their body but also
   the names (as strings) for all the global and local identifiers *)
Record dxModule := MkDXModule
  { dxModuleContent: Ctypes.program Csyntax.function
  ; dxModuleNames:   list (AST.ident * String.string)
  }.