const std = @import("std");
const model_types = @import("model.zig");
const profile = @import("profile");

pub fn renderConcepts(concepts: []const model_types.Concept, writer: *std.Io.Writer) !void {
    try writer.writeAll(
        \\pub const ConceptId = enum {
        \\
    );
    for (concepts) |concept| {
        try writer.writeAll("    ");
        try writeConceptSymbol(writer, concept.id);
        try writer.writeAll(",\n");
    }
    try writer.writeAll(
        \\};
        \\pub const Concept = struct { id: ConceptId, canonical_term: []const u8 };
        \\pub const concepts = [_]Concept{
        \\
    );
    for (concepts) |concept| {
        try writer.writeAll("    .{ .id = .");
        try writeConceptSymbol(writer, concept.id);
        try writer.writeAll(", .canonical_term = ");
        try writeZigString(writer, concept.term);
        try writer.writeAll(" },\n");
    }
    try writer.writeAll(
        \\};
        \\pub fn concept(id: ConceptId) *const Concept {
        \\    return &concepts[@intFromEnum(id)];
        \\}
        \\
    );
}

pub fn writeConceptSymbol(writer: *std.Io.Writer, id: []const u8) !void {
    std.debug.assert(std.mem.startsWith(u8, id, "concept-"));
    for (id[8..]) |byte| try writer.writeByte(if (byte == '-') '_' else byte);
}

pub fn renderVerification(
    obligations: []const model_types.VerificationObligation,
    writer: *std.Io.Writer,
) !void {
    try writer.writeAll(
        \\pub const VerificationObligationId = enum {
        \\
    );
    for (obligations) |obligation| {
        try writer.writeAll("    ");
        try writePrefixedSymbol(writer, obligation.id, "obligation-");
        try writer.writeAll(",\n");
    }
    try writer.writeAll(
        \\};
        \\pub const VerificationKind = enum { required, forbidden };
        \\pub const ObligationReference = struct {
        \\    id: VerificationObligationId,
        \\    revision: u32,
        \\};
        \\pub const VerificationObligation = struct {
        \\    id: VerificationObligationId,
        \\    revision: u32,
        \\    requirement_id: []const u8,
        \\    requirement_revision: u32,
        \\    kind: VerificationKind,
        \\    label: []const u8,
        \\};
        \\pub const verification_obligations = [_]VerificationObligation{
        \\
    );
    for (obligations) |obligation| {
        try writer.writeAll("    .{ .id = .");
        try writePrefixedSymbol(writer, obligation.id, "obligation-");
        try writer.print(", .revision = {d}, .requirement_id = ", .{obligation.revision});
        try writeZigString(writer, obligation.requirement.id);
        try writer.print(", .requirement_revision = {d}, .kind = .{s}, .label = ", .{
            obligation.requirement.revision,
            @tagName(obligation.kind),
        });
        try writeZigString(writer, obligation.label);
        try writer.writeAll(" },\n");
    }
    try writer.writeAll("};\n\n");
}

pub fn renderImplementationUnits(
    units: []const model_types.ImplementationUnit,
    writer: *std.Io.Writer,
) !void {
    try writer.writeAll(
        \\pub const ImplementationUnitId = enum {
        \\
    );
    for (units) |unit| {
        try writer.writeAll("    ");
        try writePrefixedSymbol(writer, unit.id, "implementation-");
        try writer.writeAll(",\n");
    }
    try writer.writeAll(
        \\};
        \\pub const ImplementationUnit = struct {
        \\    id: ImplementationUnitId,
        \\    revision: u32,
        \\    sources: []const []const u8,
        \\    realizes: []const ObligationReference,
        \\};
        \\pub const implementation_units = [_]ImplementationUnit{
        \\
    );
    for (units) |unit| {
        try writer.writeAll("    .{\n        .id = .");
        try writePrefixedSymbol(writer, unit.id, "implementation-");
        try writer.print(",\n        .revision = {d},\n        .sources = &.{{\n", .{
            unit.revision,
        });
        for (unit.sources) |source| {
            try writer.writeAll("            ");
            try writeZigString(writer, source.path);
            try writer.writeAll(",\n");
        }
        try writer.writeAll("        },\n        .realizes = &.{\n");
        for (unit.realizes) |reference| try renderObligationReference(reference, 12, writer);
        try writer.writeAll("        },\n    },\n");
    }
    try writer.writeAll("};\n\n");
}

pub fn renderTestSpecs(
    test_specs: []const model_types.TestSpec,
    writer: *std.Io.Writer,
) !void {
    try writer.writeAll(
        \\pub const TestSpecId = enum {
        \\
    );
    for (test_specs) |test_spec| {
        try writer.writeAll("    ");
        try writeTestSpecSymbol(writer, test_spec.id);
        try writer.writeAll(",\n");
    }
    try writer.writeAll(
        \\};
        \\pub const TestSuite = enum {
    );
    try writer.writeByte('\n');
    inline for (comptime std.meta.tags(profile.Suite)) |suite| {
        if (comptime profile.suiteIsConcrete(suite)) {
            try writer.print("    {s},\n", .{@tagName(suite)});
        }
    }
    try writer.writeAll(
        \\};
        \\pub const ProductionBoundary = enum { process, state_transition };
        \\pub const FixtureReference = struct {
        \\    id: []const u8,
        \\    revision: u32,
        \\    path: []const u8,
        \\};
        \\pub const VerificationClaim = struct {
        \\    oracle: []const u8,
        \\    kind: VerificationKind,
        \\    obligations: []const ObligationReference,
        \\};
        \\pub const TestSpec = struct {
        \\    id: TestSpecId,
        \\    revision: u32,
        \\    suite: TestSuite,
        \\    fixture: FixtureReference,
        \\    claims: []const VerificationClaim,
        \\    production_boundary: ProductionBoundary,
        \\};
        \\pub const test_specs = [_]TestSpec{
        \\
    );
    for (test_specs) |test_spec| try renderTestSpec(&test_spec, writer);
    try writer.writeAll("};\n\n");
}

pub fn renderTestSpec(test_spec: *const model_types.TestSpec, writer: *std.Io.Writer) !void {
    try writer.writeAll("    .{\n        .id = .");
    try writeTestSpecSymbol(writer, test_spec.id);
    try writer.print(",\n        .revision = {d},\n        .suite = .{s},\n", .{
        test_spec.revision,
        @tagName(test_spec.suite),
    });
    try writer.writeAll("        .fixture = .{\n            .id = ");
    try writeZigString(writer, test_spec.fixture.id);
    try writer.print(",\n            .revision = {d},\n            .path = ", .{
        test_spec.fixture.revision,
    });
    try writeZigString(writer, test_spec.fixture.path);
    try writer.writeAll(",\n        },\n        .claims = &.{\n");
    for (test_spec.claims) |claim| {
        try writer.writeAll("            .{ .oracle = ");
        try writeZigString(writer, claim.oracle);
        try writer.print(", .kind = .{s}, .obligations = &.{{\n", .{@tagName(claim.kind)});
        for (claim.obligations) |reference| try renderObligationReference(reference, 16, writer);
        try writer.writeAll("            } },\n");
    }
    try writer.print("        }},\n        .production_boundary = .{s},\n    }},\n", .{
        @tagName(test_spec.production_boundary),
    });
}

pub fn renderObligationReference(
    reference: model_types.ObligationReference,
    indent: usize,
    writer: *std.Io.Writer,
) !void {
    try writeIndent(writer, indent);
    try writer.writeAll(".{ .id = .");
    try writePrefixedSymbol(writer, reference.id, "obligation-");
    try writer.print(", .revision = {d} }},\n", .{reference.revision});
}

pub fn writeIndent(writer: *std.Io.Writer, indent: usize) !void {
    for (0..indent) |_| try writer.writeByte(' ');
}

pub fn writePrefixedSymbol(writer: *std.Io.Writer, id: []const u8, prefix: []const u8) !void {
    std.debug.assert(std.mem.startsWith(u8, id, prefix));
    for (id[prefix.len..]) |byte| try writer.writeByte(if (byte == '-') '_' else byte);
}

pub fn writeTestSpecSymbol(writer: *std.Io.Writer, id: []const u8) !void {
    std.debug.assert(std.mem.startsWith(u8, id, "test-"));
    for (id[5..]) |byte| try writer.writeByte(if (byte == '-') '_' else byte);
}

pub fn writeZigStringLines(
    writer: *std.Io.Writer,
    source: []const u8,
    indent: []const u8,
    width_max: usize,
) !void {
    var offset: usize = 0;
    while (offset < source.len) {
        const segment_width_max = if (offset == 0) width_max else 84;
        var end = @min(offset + segment_width_max, source.len);
        if (end < source.len) {
            const relative = std.mem.lastIndexOfScalar(u8, source[offset..end], ' ') orelse
                return error.UnbreakableGeneratedString;
            end = offset + relative + 1;
        }
        if (offset > 0) try writer.writeAll(indent);
        try writeZigString(writer, source[offset..end]);
        if (end < source.len) {
            try writer.writeAll(" ++\n");
        } else {
            try writer.writeAll(",\n");
        }
        offset = end;
    }
}

pub fn writeZigString(writer: *std.Io.Writer, source: []const u8) !void {
    const hex = "0123456789abcdef";
    try writer.writeByte('"');
    for (source) |byte| switch (byte) {
        '"' => try writer.writeAll("\\\""),
        '\\' => try writer.writeAll("\\\\"),
        '\n' => try writer.writeAll("\\n"),
        '\r' => try writer.writeAll("\\r"),
        '\t' => try writer.writeAll("\\t"),
        0...8, 11...12, 14...0x1f, 0x7f => {
            const escaped = [_]u8{ '\\', 'x', hex[byte >> 4], hex[byte & 15] };
            try writer.writeAll(&escaped);
        },
        else => try writer.writeByte(byte),
    };
    try writer.writeByte('"');
}

test "generated test suite follows the profile" {
    var output = std.Io.Writer.Allocating.init(std.testing.allocator);
    defer output.deinit();
    try renderTestSpecs(&.{}, &output.writer);
    for (profile.concrete_suites) |suite| {
        try std.testing.expect(std.mem.indexOf(u8, output.written(), @tagName(suite)) != null);
    }
    try std.testing.expect(
        std.mem.indexOf(u8, output.written(), @tagName(profile.wildcard_suite)) == null,
    );
}

test "Zig string rendering escapes code-significant bytes" {
    var output = std.Io.Writer.Allocating.init(std.testing.allocator);
    defer output.deinit();
    try writeZigString(&output.writer, "a\"b\\c\n");
    try std.testing.expectEqualStrings("\"a\\\"b\\\\c\\n\"", output.written());
}