Extra methods that need defining in C

[HarryBryant99]

I saw that for the natural numbers there were certain methods, such as sw_nat() and S_tag that needed defining so that the example addition program would function.

I have been playing around with CodeGen and I want to write programs that utilise Strings, Characters, and Buffers. However, when extracting programs with other datatypes it produces similar methods that need defining but it is unclear to what these need to be.

To demonstrate this, I made a simple program in Coq that appends two strings using the string_scope.

Require Import codegen.codegen.
Require Import String.

Open Scope string_scope.

Fixpoint eqb s1 s2 : bool :=
 match s1, s2 with
 | EmptyString, EmptyString => true
 | String c1 s1', String c2 s2' => Ascii.eqb c1 c2 && eqb s1' s2'
 | _,_ => false
 end.

Reserved Notation "x ++ y" (right associativity, at level 60).

Definition join a b := (a ++ b).

Compute join "a" "b".

CodeGen SourceFile "Developments/joinstrings.c".

CodeGen Linear string.
CodeGen StaticFunc join.

CodeGen GenerateFile.

The extraction using CodeGen produces:

static string append(string v1_s1, string v2_s2);
static string append(string v1_s1, string v2_s2)
{
  ascii v3_c;
  string v4_s1_;
  string v5_s;
  switch (sw_string(v1_s1))
  {
    default:
      return v2_s2;
    case String_tag:
      v3_c = String_get_member_0(v1_s1);
      v4_s1_ = String_get_member_1(v1_s1);
      v5_s = append(v4_s1_, v2_s2);
      return String(v3_c, v5_s);
[joinstrings_coq.txt](https://github.com/akr/codegen/files/12658493/joinstrings_coq.txt)

  }
}

static string join(string v1_a, string v2_b);
static string join(string v1_a, string v2_b)
{
  return append(v1_a, v2_b);
}

I have defined a String to be a Character Array in C. But this still produces errors. This includes:

• 'String_tag' being undefined
• The method 'append' returns a String but says it has been declared to return an array. Confusion is that String was declared as an array?
• Ascii being unkown - however, I assume I just need to define the type
• Many warnings around implicit declarations of the function 'String_get_member_0', 'String_get_member_1', 'sw_string', and the return statement 'String'

I assume most of these would be solved by having similar definitions to those of the natural numbers? In Coq I saw that Inductive Types can be defined, do all datatypes need to be done in this way?

Any further information or documentation on this that you have would be greatly appreciated.

Many thanks, Harry Bryant joinstrings_coq.txt