Ctyping: better typing of conditional expressions.

Ctyping: define a typechecker for whole programs.
Csyntax: introduce the type "pre-program" (non-dependent).
C2C: use Ctyping.econdition instead of Ctyping.econdition'.

Note: Ctyping.typecheck_program could be used as the first step
in the verified compilation pipeline.  Then, retyping would
no longer be performed in C2C.  We keep it this way (for the time
being) because retyping errors are reported more precisely in C2C than
in Ctyping.

1 files changed, 22 insertions, 18 deletions

diff --git a/cfrontend/Csyntax.v b/cfrontend/Csyntax.v
index 8ea4e077..db059791 100644
--- a/cfrontend/Csyntax.v
+++ b/cfrontend/Csyntax.v
@@ -208,13 +208,22 @@ Definition type_of_fundef (f: fundef) : type :=
 
 (** ** Programs *)
 
-(** A program is composed of:
+(** A "pre-program", as produced by the elaborator is composed of:
 - a list of definitions of functions and global variables;
 - the names of functions and global variables that are public (not static);
 - the name of the function that acts as entry point ("main" function).
-- a list of definitions for structure and union names;
-- the corresponding composite environment;
-*)
+- a list of definitions for structure and union names
+
+A program is composed of the same information, plus the corresponding
+composite environment, and a proof that this environment is consistent
+with the composite definitions. *)
+
+Record pre_program : Type := {
+  pprog_defs: list (ident * globdef fundef type);
+  pprog_public: list ident;
+  pprog_main: ident;
+  pprog_types: list composite_definition
+}.
 
 Record program : Type := {
   prog_defs: list (ident * globdef fundef type);
@@ -232,20 +241,15 @@ Definition program_of_program (p: program) : AST.program fundef type :=
 
 Coercion program_of_program: program >-> AST.program.
 
-Program Definition make_program (types: list composite_definition)
-                                (defs: list (ident * globdef fundef type))
-                                (public: list ident)
-                                (main: ident): res program :=
-  match build_composite_env types with
-  | OK env =>
-      OK {| prog_defs := defs;
-            prog_public := public;
-            prog_main := main;
-            prog_types := types;
-            prog_comp_env := env;
+Program Definition program_of_pre_program (p: pre_program) : res program :=
+  match build_composite_env p.(pprog_types) with
+  | Error e => Error e
+  | OK ce =>
+      OK {| prog_defs := p.(pprog_defs);
+            prog_public := p.(pprog_public);
+            prog_main := p.(pprog_main);
+            prog_types := p.(pprog_types);
+            prog_comp_env := ce;
             prog_comp_env_eq := _ |}
-  | Error msg =>
-      Error msg
   end.
 
-