const std = @import("std");
const model_types = @import("model.zig");
const diag = @import("diag.zig");
const fail = diag.fail;
const on = diag.subject;
const text = @import("text.zig");

const instrumentation_open = "## Instrumentation\n\n```zig tj-test\n";
const fence_close = "\n```";

pub const Parsed = struct {
    source: []u8,
    instrumentation: []const u8,

    pub fn deinit(parsed: *Parsed, allocator: std.mem.Allocator) void {
        allocator.free(parsed.source);
        parsed.* = undefined;
    }
};

pub fn parse(
    allocator: std.mem.Allocator,
    io: std.Io,
    path: []const u8,
) !Parsed {
    const source = try std.Io.Dir.cwd().readFileAlloc(
        io,
        path,
        allocator,
        .limited(model_types.file_size_max),
    );
    errdefer allocator.free(source);
    return .{
        .source = source,
        .instrumentation = try extractInstrumentation(source),
    };
}

pub fn extractInstrumentation(source: []const u8) ![]const u8 {
    const opening = std.mem.indexOf(u8, source, instrumentation_open) orelse
        return error.MissingInstrumentationFence;
    if (opening > 0) {
        if (source[opening - 1] != '\n') return error.InvalidInstrumentationFence;
    }
    const body_start = opening + instrumentation_open.len;
    if (std.mem.indexOfPos(u8, source, body_start, instrumentation_open) != null) {
        return error.DuplicateInstrumentationFence;
    }
    const body_end = std.mem.indexOfPos(u8, source, body_start, fence_close) orelse
        return error.UnterminatedInstrumentationFence;
    const body = source[body_start..body_end];
    if (std.mem.trim(u8, body, " \t\r\n").len == 0) {
        return error.EmptyInstrumentationFence;
    }
    return body;
}

/// Generate ordinary Zig tests for every bound fixture, optionally one suite.
pub fn render(
    allocator: std.mem.Allocator,
    io: std.Io,
    model: *const model_types.Graph,
    suite_filter: ?[]const u8,
    writer: *std.Io.Writer,
) !void {
    try writer.writeAll("// Generated from instrumented prose fixtures. Do not edit.\n");
    for (model.test_bindings) |binding| {
        if (!selected(model, &binding, suite_filter)) continue;
        try writer.print("const {s} = @import(\"{s}\");\n", .{ binding.module, binding.module });
    }
    var written: u32 = 0;
    try writer.writeByte('\n');
    for (model.test_bindings) |binding| {
        if (!selected(model, &binding, suite_filter)) continue;
        const test_spec = model_types.findTestSpec(model.test_specs, binding.test_spec.id).?;
        var parsed = try parse(allocator, io, test_spec.fixture.path);
        defer parsed.deinit(allocator);
        if (written > 0) try writer.writeByte('\n');
        try renderTest(&test_spec, &binding, parsed.instrumentation, writer);
        written += 1;
    }
}

fn selected(
    model: *const model_types.Graph,
    binding: *const model_types.TestBinding,
    suite_filter: ?[]const u8,
) bool {
    const filter = suite_filter orelse return true;
    const test_spec = model_types.findTestSpec(model.test_specs, binding.test_spec.id).?;
    return std.mem.eql(u8, @tagName(test_spec.suite), filter);
}

pub fn renderTest(
    test_spec: *const model_types.TestSpec,
    binding: *const model_types.TestBinding,
    instrumentation: []const u8,
    writer: *std.Io.Writer,
) !void {
    try writer.print("test \"{s}@{d}\" {{\n", .{ test_spec.id, test_spec.revision });
    try writer.print("    var fixture = try {s}.Fixture.init();\n", .{binding.module});
    try writer.writeAll("    defer fixture.deinit();\n");
    var lines = std.mem.splitScalar(u8, instrumentation, '\n');
    while (lines.next()) |line| {
        if (line.len > 0) try writer.writeAll("    ");
        try writer.writeAll(line);
        try writer.writeByte('\n');
    }
    try writer.writeAll("}\n");
}

test "instrumentation extraction is exact and bounded by one fence" {
    const source =
        "# Example\n\n## Instrumentation\n\n" ++
        "```zig tj-test\ntry fixture.when_run();\n```\n";
    try std.testing.expectEqualStrings(
        "try fixture.when_run();",
        try extractInstrumentation(source),
    );
    try std.testing.expectError(
        error.MissingInstrumentationFence,
        extractInstrumentation("# Example\n"),
    );
    try std.testing.expectError(
        error.DuplicateInstrumentationFence,
        extractInstrumentation(
            source ++ "\n## Instrumentation\n\n```zig tj-test\nsecond();\n```\n",
        ),
    );
}

pub fn validateFixtureInstrumentation(
    test_spec: *const model_types.TestSpec,
    source: []const u8,
    instrumentation: []const u8,
    stderr: *std.Io.Writer,
) !void {
    var offset: usize = 0;
    var previous_rank: u8 = 0;
    var phase_counts = [_]u32{ 0, 0, 0, 0 };
    while (std.mem.indexOfPos(u8, instrumentation, offset, "fixture.")) |start| {
        const method_start = start + "fixture.".len;
        const method_end = std.mem.indexOfScalarPos(
            u8,
            instrumentation,
            method_start,
            '(',
        ) orelse return error.InvalidFixtureCall;
        const method = instrumentation[method_start..method_end];
        const rank = fixtureMethodRank(method) orelse {
            return fail(stderr, on.fixture, "invalid fixture method: {s}", .{method});
        };
        if (rank < previous_rank) {
            return fail(
                stderr,
                on.fixture,
                "fixture phase order is invalid: {s}",
                .{test_spec.fixture.id},
            );
        }
        previous_rank = rank;
        phase_counts[rank] += 1;
        try validateFixtureMethodSource(source, method, stderr);
        offset = method_end + 1;
    }
    if (phase_counts[0] == 0) {
        return fail(
            stderr,
            on.fixture,
            "fixture has no given operation: {s}",
            .{test_spec.fixture.id},
        );
    }
    if (phase_counts[1] != 1) {
        return fail(stderr, on.fixture, "fixture requires exactly one when operation: {s}", .{
            test_spec.fixture.id,
        });
    }
    try validateOracleCalls(test_spec.claims, .required, instrumentation, "then", stderr);
    try validateOracleCalls(test_spec.claims, .forbidden, instrumentation, "forbid", stderr);
    if (phase_counts[2] != claimCount(test_spec.claims, .required)) {
        return fail(
            stderr,
            on.fixture,
            "fixture then-operation count mismatch: {s}",
            .{test_spec.fixture.id},
        );
    }
    if (phase_counts[3] != claimCount(test_spec.claims, .forbidden)) {
        return fail(stderr, on.fixture, "fixture forbid-operation count mismatch: {s}", .{
            test_spec.fixture.id,
        });
    }
}

pub fn fixtureMethodRank(method: []const u8) ?u8 {
    if (std.mem.startsWith(u8, method, "given_")) return 0;
    if (std.mem.startsWith(u8, method, "when_")) return 1;
    if (std.mem.startsWith(u8, method, "then_")) return 2;
    if (std.mem.startsWith(u8, method, "forbid_")) return 3;
    return null;
}

pub fn validateFixtureMethodSource(
    source: []const u8,
    method: []const u8,
    stderr: *std.Io.Writer,
) !void {
    if (!text.symbolValid(method)) {
        return fail(stderr, on.fixture, "invalid fixture method symbol: {s}", .{method});
    }
    var marker_buffer: [160]u8 = undefined;
    const marker = std.fmt.bufPrint(&marker_buffer, "pub fn {s}(", .{method}) catch {
        return error.TestBindingMarkerTooLong;
    };
    if (text.occurrenceCount(source, marker) != 1) {
        return fail(stderr, on.fixture, "missing or duplicate fixture method: {s}", .{method});
    }
}

pub fn validateOracleCalls(
    claims: []const model_types.VerificationClaim,
    kind: model_types.VerificationKind,
    instrumentation: []const u8,
    phase: []const u8,
    stderr: *std.Io.Writer,
) !void {
    for (claims) |claim| {
        if (claim.kind != kind) continue;
        var marker_buffer: [160]u8 = undefined;
        const marker = oracleCallMarker(&marker_buffer, phase, claim.oracle) catch {
            return error.OracleIdentifierTooLong;
        };
        if (text.occurrenceCount(instrumentation, marker) != 1) {
            return fail(
                stderr,
                on.fixture,
                "oracle has no unique fixture call: {s}",
                .{claim.oracle},
            );
        }
    }
}

pub fn claimCount(
    claims: []const model_types.VerificationClaim,
    kind: model_types.VerificationKind,
) u32 {
    var count: u32 = 0;
    for (claims) |claim| {
        if (claim.kind == kind) count += 1;
    }
    return count;
}

pub fn oracleCallMarker(buffer: []u8, phase: []const u8, oracle_id: []const u8) ![]const u8 {
    var writer = std.Io.Writer.fixed(buffer);
    try writer.print("fixture.{s}_", .{phase});
    for (oracle_id) |byte| {
        try writer.writeByte(if (byte == '-') '_' else std.ascii.toLower(byte));
    }
    try writer.writeByte('(');
    return writer.buffered();
}

pub fn validateFixtureSource(
    source: []const u8,
    test_spec: *const model_types.TestSpec,
    stderr: *std.Io.Writer,
) !void {
    const fixture = &test_spec.fixture;
    var identity_buffer: [160]u8 = undefined;
    const identity = std.fmt.bufPrint(
        &identity_buffer,
        "**Fixture:** `{s}@{d}`",
        .{ fixture.id, fixture.revision },
    ) catch return error.FixtureIdentityTooLong;
    if (text.occurrenceCount(source, identity) != 1) {
        return fail(
            stderr,
            on.fixture,
            "missing or duplicate fixture identity: {s}",
            .{fixture.id},
        );
    }
    const headings = [_][]const u8{
        "Given",
        "When",
        "Required invariants",
        "Forbidden effects",
        "Variations",
        "Limitations",
    };
    for (headings) |heading| {
        const section = text.markdownSection(source, heading) orelse {
            return fail(
                stderr,
                on.fixture,
                "missing, duplicate, or empty fixture section: {s}",
                .{heading},
            );
        };
        std.debug.assert(section.len > 0);
    }
    const required = text.markdownSection(source, "Required invariants").?;
    const forbidden = text.markdownSection(source, "Forbidden effects").?;
    try validateOracleReferences(
        source,
        required,
        test_spec.claims,
        .required,
        stderr,
    );
    try validateOracleReferences(
        source,
        forbidden,
        test_spec.claims,
        .forbidden,
        stderr,
    );
}

pub fn validateOracleReferences(
    source: []const u8,
    section: []const u8,
    claims: []const model_types.VerificationClaim,
    kind: model_types.VerificationKind,
    stderr: *std.Io.Writer,
) !void {
    const prefix = if (kind == .required) "`INV-" else "`NO-";
    if (text.occurrenceCount(section, prefix) != claimCount(claims, kind)) {
        return fail(
            stderr,
            on.fixture,
            "fixture section contains an unclaimed or missing oracle",
            .{},
        );
    }
    for (claims) |claim| {
        if (claim.kind != kind) continue;
        var token_buffer: [80]u8 = undefined;
        const token = std.fmt.bufPrint(&token_buffer, "`{s}`", .{claim.oracle}) catch {
            return error.OracleIdentifierTooLong;
        };
        if (text.occurrenceCount(section, token) != 1) {
            return fail(
                stderr,
                on.fixture,
                "missing or duplicate fixture oracle: {s}",
                .{claim.oracle},
            );
        }
        if (text.occurrenceCount(source, token) != 1) {
            return fail(stderr, on.fixture, "fixture oracle appears outside its section: {s}", .{
                claim.oracle,
            });
        }
    }
}

test "fixture validation requires claimed oracle identifiers" {
    const claims = [_]model_types.VerificationClaim{
        .{
            .oracle = "INV-EXAMPLE",
            .kind = .required,
            .obligations = &.{.{ .id = "obligation-required", .revision = 1 }},
        },
        .{
            .oracle = "NO-EXAMPLE",
            .kind = .forbidden,
            .obligations = &.{.{ .id = "obligation-forbidden", .revision = 1 }},
        },
    };
    const test_spec: model_types.TestSpec = .{
        .id = "test-example",
        .revision = 1,
        .suite = model_types.testSuite(1),
        .fixture = .{
            .id = "fixture-example",
            .revision = 1,
            .path = "fixture.md",
            .sha256 = "0000000000000000000000000000000000000000000000000000000000000000",
        },
        .claims = &claims,
        .production_boundary = .state_transition,
    };
    const valid =
        \\# Example
        \\
        \\**Fixture:** `fixture-example@1`
        \\
        \\## Given
        \\State.
        \\## When
        \\Event.
        \\## Required invariants
        \\- `INV-EXAMPLE`: Required.
        \\## Forbidden effects
        \\- `NO-EXAMPLE`: Forbidden.
        \\## Variations
        \\None.
        \\## Limitations
        \\None.
    ;
    var output = std.Io.Writer.Allocating.init(std.testing.allocator);
    defer output.deinit();
    try validateFixtureSource(valid, &test_spec, &output.writer);
    const missing = "# Example\n\n**Fixture:** `fixture-example@1`\n\n" ++
        "## Given\nState.\n## When\nEvent.\n## Required invariants\nNone.\n" ++
        "## Forbidden effects\n- `NO-EXAMPLE`: Forbidden.\n" ++
        "## Variations\nNone.\n## Limitations\nNone.\n";
    try std.testing.expectError(
        error.InvalidSpecification,
        validateFixtureSource(missing, &test_spec, &output.writer),
    );
}