let label s =
  match Sol.Label.of_string s with
  | Ok l -> l
  | Error (`Invalid_label s) -> Alcotest.failf "invalid label in test: %s" s

let term = Alcotest.testable Sol.Term.pp Sol.Term.equal

let rational num den =
  match Sol.Term.rational ~num:(Z.of_int num) ~den:(Z.of_int den) with
  | Ok t -> t
  | Error `Zero_denominator -> Alcotest.fail "unexpected zero denominator"

let record bindings =
  match Sol.Term.record bindings with
  | Ok t -> t
  | Error `Empty_record -> Alcotest.fail "unexpected empty record"
  | Error (`Duplicate_label _) -> Alcotest.fail "unexpected duplicate label"

let int n = Sol.Term.integer (Z.of_int n)

(* Canonical forms: Decision 12, minimal shape. *)

let test_rational_reduces () =
  Alcotest.check term "2/4 = 1/2" (rational 1 2) (rational 2 4)

let test_rational_collapses_to_integer () =
  Alcotest.check term "4/2 = 2" (int 2) (rational 4 2);
  Alcotest.check term "2/2 = 1" (int 1) (rational 2 2);
  Alcotest.check term "0/5 = 0" (int 0) (rational 0 5)

let test_rational_sign_normalizes () =
  Alcotest.check term "1/-2 = -1/2" (rational (-1) 2) (rational 1 (-2));
  Alcotest.check term "-1/-2 = 1/2" (rational 1 2) (rational (-1) (-2))

let test_rational_zero_denominator () =
  match Sol.Term.rational ~num:Z.one ~den:Z.zero with
  | Error `Zero_denominator -> ()
  | Ok _ -> Alcotest.fail "1/0 must be rejected"

(* Records: label order is irrelevant, duplicates are rejected. *)

let test_record_label_order_irrelevant () =
  let ab = record [ (label "a", int 1); (label "b", int 2) ] in
  let ba = record [ (label "b", int 2); (label "a", int 1) ] in
  Alcotest.check term "{a: 1 b: 2} = {b: 2 a: 1}" ab ba

let test_record_duplicate_rejected () =
  match Sol.Term.record [ (label "a", int 1); (label "a", int 2) ] with
  | Error (`Duplicate_label l) ->
      Alcotest.(check string) "offending label" "a" (Sol.Label.to_string l)
  | Ok _ -> Alcotest.fail "duplicate label must be rejected"
  | Error `Empty_record -> Alcotest.fail "wrong error"

let test_record_empty_rejected () =
  match Sol.Term.record [] with
  | Error `Empty_record -> ()
  | Ok _ | Error (`Duplicate_label _) ->
      Alcotest.fail "empty record must be rejected"

(* Sequences: the published elaboration into head/tail cells. *)

let test_sequence_elaboration () =
  let expected =
    Sol.Term.cons ~head:(int 1)
      ~tail:(Sol.Term.cons ~head:(int 2) ~tail:Sol.Term.nil)
  in
  Alcotest.check term "#(1 2) elaborates to nested cells" expected
    (Sol.Term.sequence [ int 1; int 2 ])

let test_empty_sequence_is_nil () =
  Alcotest.check term "#() is Nil" Sol.Term.nil (Sol.Term.sequence [])

(* Printing: Sol notation back out. *)

let print t = Format.asprintf "%a" Sol.Term.pp t

let test_printing () =
  Alcotest.(check string) "integer" "42" (print (int 42));
  Alcotest.(check string) "rational" "1/4" (print (rational 1 4));
  Alcotest.(check string) "string" {|"Sun"|} (print (Sol.Term.string "Sun"));
  Alcotest.(check string) "empty sequence" "#()" (print Sol.Term.nil);
  Alcotest.(check string) "sequence" "#(1 2 3)"
    (print (Sol.Term.sequence [ int 1; int 2; int 3 ]));
  Alcotest.(check string) "record" "{a: 1 b: 2}"
    (print (record [ (label "b", int 2); (label "a", int 1) ]));
  Alcotest.(check string) "reference" "#Person"
    (print (Result.get_ok (Sol.Term.reference "Person")))

let test_reference_validation () =
  Alcotest.(check bool) "well-formed" true
    (Result.is_ok (Sol.Term.reference "Person"));
  Alcotest.(check bool) "empty rejected" false
    (Result.is_ok (Sol.Term.reference ""));
  Alcotest.(check bool) "leading digit rejected" false
    (Result.is_ok (Sol.Term.reference "1st"))

let test_label_validation () =
  let ok s = Result.is_ok (Sol.Label.of_string s) in
  Alcotest.(check bool) "dept_id" true (ok "dept_id");
  Alcotest.(check bool) "empty" false (ok "");
  Alcotest.(check bool) "capitalized" false (ok "Name");
  Alcotest.(check bool) "leading digit" false (ok "1a")

let () =
  Alcotest.run "sol"
    [
      ( "canonical forms",
        [
          Alcotest.test_case "rational reduces" `Quick test_rational_reduces;
          Alcotest.test_case "integer-valued rational is an integer" `Quick
            test_rational_collapses_to_integer;
          Alcotest.test_case "sign normalizes" `Quick
            test_rational_sign_normalizes;
          Alcotest.test_case "zero denominator rejected" `Quick
            test_rational_zero_denominator;
        ] );
      ( "records",
        [
          Alcotest.test_case "label order irrelevant" `Quick
            test_record_label_order_irrelevant;
          Alcotest.test_case "duplicate label rejected" `Quick
            test_record_duplicate_rejected;
          Alcotest.test_case "empty record rejected" `Quick
            test_record_empty_rejected;
        ] );
      ( "sequences",
        [
          Alcotest.test_case "elaboration" `Quick test_sequence_elaboration;
          Alcotest.test_case "empty is nil" `Quick test_empty_sequence_is_nil;
        ] );
      ( "notation",
        [
          Alcotest.test_case "printing" `Quick test_printing;
          Alcotest.test_case "label validation" `Quick test_label_validation;
          Alcotest.test_case "reference validation" `Quick
            test_reference_validation;
        ] );
    ]