Skip to content

Commit e9c5f43

Browse files
Smaug123claude
andcommitted
Add a checked WellFormedSchema constructor to the runtime kernel
The selection semantics assume every addressable --token names at most one claimant under the scanner's case-insensitive matching; without that, matchLeaf silently routes colliding tokens to the first-declared leaf. Generation-time checks cannot see forms supplied via [<Literal>] constants, so generated code will re-check at runtime via WellFormedSchema.checkOrFail before parsing. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
1 parent ab10946 commit e9c5f43

2 files changed

Lines changed: 408 additions & 0 deletions

File tree

WoofWare.Myriad.Plugins.Test/TestArgParser/TestArgParserRuntime.fs

Lines changed: 216 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1059,3 +1059,219 @@ module TestArgParserRuntime =
10591059
// The tricky regime is the bare boolean flag; make sure we are actually exercising it.
10601060
bareBoolCount |> shouldBeGreaterThan 100
10611061
totalUnits |> shouldBeGreaterThan 1000
1062+
1063+
// ----------------------------------------------------------------------------------------
1064+
// Well-formedness: the checked constructor which generated code must pass its schema
1065+
// through before parsing. The selection semantics assume that every addressable `--token`
1066+
// names at most one leaf *under the scanner's case-insensitive matching*; without that,
1067+
// matchLeaf silently routes colliding tokens to whichever leaf is declared first, and for a
1068+
// Sum schema that silently selects the wrong case.
1069+
1070+
[<Test>]
1071+
let ``A well-formed schema passes the checked constructor`` () =
1072+
match WellFormedSchema.check motivating with
1073+
| Ok wellFormed -> WellFormedSchema.schema wellFormed |> shouldEqual motivating
1074+
| Error errors -> failwithf "unexpected schema errors: %O" errors
1075+
1076+
[<Test>]
1077+
let ``Forms which differ only by case collide, even across sum cases`` () =
1078+
// The empirical counterexample from review: `foo` in one case and `FOO` in the other
1079+
// passes a case-sensitive uniqueness check, but the scanner matches case-insensitively,
1080+
// so `--FOO=3` routes to the first-declared leaf and silently selects *its* case.
1081+
let schema =
1082+
{
1083+
Leaves =
1084+
[
1085+
leaf 0 "foo" ErasedArity.One ErasedRequirement.Required
1086+
leaf 1 "FOO" ErasedArity.One ErasedRequirement.Required
1087+
]
1088+
Tree = ErasedTree.Sum (0, [ "CaseA", ErasedTree.Leaf 0 ; "CaseB", ErasedTree.Leaf 1 ])
1089+
Positional = None
1090+
}
1091+
1092+
WellFormedSchema.errors schema
1093+
|> shouldEqual
1094+
[
1095+
SchemaError.TokenCollision ("--foo", [ "argument '--foo'" ; "argument '--FOO'" ])
1096+
]
1097+
1098+
[<Test>]
1099+
let ``A form colliding with another leaf's negated form is rejected, whatever the casing`` () =
1100+
let negatable =
1101+
{ leaf 0 "foo" ErasedArity.BoolLike ErasedRequirement.Required with
1102+
AcceptsNegation = true
1103+
}
1104+
1105+
let schema =
1106+
productSchema [ negatable ; leaf 1 "No-Foo" ErasedArity.One ErasedRequirement.Required ] None
1107+
1108+
WellFormedSchema.errors schema
1109+
|> shouldEqual
1110+
[
1111+
SchemaError.TokenCollision (
1112+
"--no-foo",
1113+
[ "the --no- form of argument '--foo'" ; "argument '--No-Foo'" ]
1114+
)
1115+
]
1116+
1117+
[<Test>]
1118+
let ``No argument may claim the reserved help name, in any casing`` () =
1119+
let schema =
1120+
productSchema [ leaf 0 "HeLp" ErasedArity.One ErasedRequirement.Required ] None
1121+
1122+
WellFormedSchema.errors schema
1123+
|> shouldEqual
1124+
[
1125+
SchemaError.TokenCollision ("--HeLp", [ "argument '--HeLp'" ; "the built-in help flag" ])
1126+
]
1127+
1128+
[<Test>]
1129+
let ``The positional sink's forms collide with leaf forms case-insensitively`` () =
1130+
let sink =
1131+
{
1132+
Id = 99
1133+
Form = "REST"
1134+
FlagLike = ErasedFlagLikeBehaviour.Reject
1135+
TypeDescription = "string"
1136+
Help = None
1137+
}
1138+
1139+
let schema =
1140+
productSchema [ leaf 0 "rest" ErasedArity.One ErasedRequirement.Required ] (Some sink)
1141+
1142+
WellFormedSchema.errors schema
1143+
|> shouldEqual
1144+
[
1145+
SchemaError.TokenCollision ("--rest", [ "argument '--rest'" ; "the positional-args sink '--REST'" ])
1146+
]
1147+
1148+
[<Test>]
1149+
let ``A leaf whose own aliases collide is rejected`` () =
1150+
let doubled =
1151+
{ leaf 0 "foo" ErasedArity.One ErasedRequirement.Required with
1152+
Forms = [ "foo" ; "FOO" ]
1153+
}
1154+
1155+
WellFormedSchema.errors (productSchema [ doubled ] None)
1156+
|> shouldEqual
1157+
[
1158+
SchemaError.TokenCollision ("--foo", [ "argument '--foo'" ; "argument '--FOO'" ])
1159+
]
1160+
1161+
[<Test>]
1162+
let ``Duplicate leaf ids are rejected`` () =
1163+
let schema =
1164+
{
1165+
Leaves =
1166+
[
1167+
leaf 0 "a" ErasedArity.One ErasedRequirement.Required
1168+
leaf 0 "b" ErasedArity.One ErasedRequirement.Required
1169+
]
1170+
Tree = ErasedTree.Product [ ErasedTree.Leaf 0 ]
1171+
Positional = None
1172+
}
1173+
1174+
WellFormedSchema.errors schema |> shouldEqual [ SchemaError.DuplicateLeafId 0 ]
1175+
1176+
[<Test>]
1177+
let ``A leaf repeated in the tree is rejected`` () =
1178+
let schema =
1179+
{ productSchema [ leaf 0 "a" ErasedArity.One ErasedRequirement.Required ] None with
1180+
Tree = ErasedTree.Product [ ErasedTree.Leaf 0 ; ErasedTree.Leaf 0 ]
1181+
}
1182+
1183+
WellFormedSchema.errors schema
1184+
|> shouldEqual [ SchemaError.LeafRepeatedInTree 0 ]
1185+
1186+
[<Test>]
1187+
let ``Tree and leaf table must refer to the same leaves`` () =
1188+
let schema =
1189+
{
1190+
Leaves =
1191+
[
1192+
leaf 0 "a" ErasedArity.One ErasedRequirement.Required
1193+
leaf 1 "b" ErasedArity.One ErasedRequirement.Required
1194+
]
1195+
Tree = ErasedTree.Product [ ErasedTree.Leaf 0 ; ErasedTree.Leaf 2 ]
1196+
Positional = None
1197+
}
1198+
1199+
WellFormedSchema.errors schema
1200+
|> shouldEqual [ SchemaError.LeafNotInTable 2 ; SchemaError.LeafNotInTree 1 ]
1201+
1202+
[<Test>]
1203+
let ``Duplicate sum ids are rejected`` () =
1204+
let schema =
1205+
{
1206+
Leaves =
1207+
[
1208+
leaf 0 "a" ErasedArity.One ErasedRequirement.Required
1209+
leaf 1 "b" ErasedArity.One ErasedRequirement.Required
1210+
]
1211+
Tree =
1212+
ErasedTree.Product
1213+
[
1214+
ErasedTree.Sum (0, [ "A", ErasedTree.Leaf 0 ])
1215+
ErasedTree.Sum (0, [ "B", ErasedTree.Leaf 1 ])
1216+
]
1217+
Positional = None
1218+
}
1219+
1220+
WellFormedSchema.errors schema |> shouldEqual [ SchemaError.DuplicateSumId 0 ]
1221+
1222+
[<Test>]
1223+
let ``Negation requires a boolean-like leaf`` () =
1224+
let bad =
1225+
{ leaf 0 "a" ErasedArity.One ErasedRequirement.Required with
1226+
AcceptsNegation = true
1227+
}
1228+
1229+
WellFormedSchema.errors (productSchema [ bad ] None)
1230+
|> shouldEqual [ SchemaError.NegationOnNonBool 0 ]
1231+
1232+
[<Test>]
1233+
let ``A leaf with no forms at all is rejected`` () =
1234+
let bad =
1235+
{ leaf 0 "a" ErasedArity.One ErasedRequirement.Required with
1236+
Forms = []
1237+
}
1238+
1239+
WellFormedSchema.errors (productSchema [ bad ] None)
1240+
|> shouldEqual [ SchemaError.NoForms 0 ]
1241+
1242+
[<Test>]
1243+
let ``checkOrFail renders every defect`` () =
1244+
let schema =
1245+
{
1246+
Leaves =
1247+
[
1248+
leaf 0 "foo" ErasedArity.One ErasedRequirement.Required
1249+
leaf 1 "FOO" ErasedArity.One ErasedRequirement.Required
1250+
]
1251+
Tree = ErasedTree.Sum (0, [ "CaseA", ErasedTree.Leaf 0 ; "CaseB", ErasedTree.Leaf 1 ])
1252+
Positional = None
1253+
}
1254+
1255+
let exc =
1256+
Assert.Throws<exn> (fun () -> WellFormedSchema.checkOrFail schema |> ignore<WellFormedSchema>)
1257+
1258+
exc.Message
1259+
|> shouldEqual
1260+
"Invalid argument parser definition:\nthe token '--foo' is claimed by: argument '--foo'; argument '--FOO' (argument names are matched case-insensitively)"
1261+
1262+
[<Test>]
1263+
let ``Every generated schema is well-formed`` () =
1264+
// The property generators build schemas which satisfy the invariants by construction
1265+
// (forms are "argN"/"altN"); this pins that the checked constructor has no false
1266+
// positives across that whole family.
1267+
let cases =
1268+
gen {
1269+
let! sumBias = Gen.elements [ 20 ; 50 ; 80 ]
1270+
return! genSchema sumBias
1271+
}
1272+
1273+
let property (schema : ErasedSchema) : unit =
1274+
WellFormedSchema.errors schema |> shouldEqual []
1275+
1276+
let config = Config.QuickThrowOnFailure.WithMaxTest 500
1277+
Check.One (config, Prop.forAll (Arb.fromGen cases) property)

0 commit comments

Comments
 (0)