feature(compiler) Make constant shadowing a warning

mechanization/Common/Result.v

@@ -325,6 +325,10 @@ Section Result.
       end.
     Definition print_warnings {A:Set} (prefix:string) (x:eresult A) : eresult A :=
       elift_warning (fun xy => coq_print_warnings prefix (List.map string_of_warning (snd xy)) (fst xy)) x.
+
+    Definition warning_no_else prov : ewarning :=
+      EWarning prov "No else in enforce".
+    Definition warning_global_shadowing prov (name:string) :=
+      EWarning prov ("Constant " ++ name ++ " hides an existing constant with the same name").
   End warnings.
 End Result.
-

mechanization/Translation/ErgoCInline.v

@@ -205,9 +205,16 @@ Section ErgoCInline.
     | DCExpr prov expr =>
       elift (fun x => (DCExpr prov x, ctxt)) (ergo_inline_expr ctxt expr)
     | DCConstant prov name ta expr =>
-      elift (fun x =>
-               (DCConstant prov name ta x, compilation_context_update_global_env ctxt name x))
-            (ergo_inline_expr ctxt expr)
+      let global_shadowing_warning :=
+          match lookup String.string_dec (ctxt.(compilation_context_global_env)) name with
+          | Some val => warning_global_shadowing prov name :: nil
+          | None => nil
+          end
+      in
+      eolift (fun x =>
+
+                (esuccess (DCConstant prov name ta x, compilation_context_update_global_env ctxt name x) global_shadowing_warning))
+             (ergo_inline_expr ctxt expr)
     | DCFunc prov name fn =>
       elift (fun x =>
                (DCFunc prov name x, compilation_context_update_function_env ctxt name x))

mechanization/Translation/ErgotoErgoC.v

@@ -271,13 +271,10 @@ Section ErgotoErgoC.
              (ergo_stmt_to_expr ctxt s2)
              (ergo_stmt_to_expr ctxt s3)
     | SEnforce prov e1 None s3 =>
-      let warning_no_else :=
-          EWarning prov "No else in enforce"
-      in
       elift3 (EIf prov)
              (elift (EUnaryBuiltin prov OpNeg) (ergo_expr_to_ergoc_expr ctxt e1))
              (esuccess (EFailure prov
-                                 (EConst prov (enforce_error_content prov ""))) (warning_no_else::nil))
+                                 (EConst prov (enforce_error_content prov ""))) (warning_no_else prov::nil))
              (ergo_stmt_to_expr ctxt s3)
     | SEnforce prov e1 (Some s2) s3 =>
       elift3 (EIf prov)