Skip to content

Commit 5aec9d5

Browse files
hyperpolymathclaude
hyperpolymath
and
claude
committed
fix(graphql): migrate to current core API — mirror of 6c878a1
- Expand ProverKind enum from 30 → 113 variants (exhaustive, no catch-all) - Add prover_kind_to_ffi / ffi_to_prover_kind for all 113 ordinals - Wire ProverConfig field on FfiProverBackend (config/set_config methods) - Fix ProofState::new call sites: Term::Var wrapping (3 sites) - Fix CoreTacticResult::Success: remove spurious Box::new - Add missing ProverBackend trait methods: search_theorems, config, set_config - Fix CStr::from_ptr casts (*const u8 → *const c_char) in ffi_wrapper - Fix CString::as_ptr casts (*const c_char → *const u8) for Zig FFI functions - Expand from_core/to_core in resolvers for all 83 new variants Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
1 parent 92c6b6e commit 5aec9d5

3 files changed

Lines changed: 598 additions & 6 deletions

File tree

‎src/interfaces/graphql/ffi_wrapper.rs‎

Lines changed: 166 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -205,6 +205,89 @@ pub fn prover_kind_to_ffi(kind: &crate::schema::ProverKind) -> u8 {
205205
crate::schema::ProverKind::MiniZinc => 27,
206206
crate::schema::ProverKind::Chuffed => 28,
207207
crate::schema::ProverKind::ORTools => 29,
208+
crate::schema::ProverKind::Lean3 => 30,
209+
crate::schema::ProverKind::TypedWasm => 31,
210+
crate::schema::ProverKind::SPIN => 32,
211+
crate::schema::ProverKind::CBMC => 33,
212+
crate::schema::ProverKind::SeaHorn => 34,
213+
crate::schema::ProverKind::CaDiCaL => 35,
214+
crate::schema::ProverKind::Kissat => 36,
215+
crate::schema::ProverKind::MiniSat => 37,
216+
crate::schema::ProverKind::NuSMV => 38,
217+
crate::schema::ProverKind::TLC => 39,
218+
crate::schema::ProverKind::Alloy => 40,
219+
crate::schema::ProverKind::Prism => 41,
220+
crate::schema::ProverKind::UPPAAL => 42,
221+
crate::schema::ProverKind::FramaC => 43,
222+
crate::schema::ProverKind::Viper => 44,
223+
crate::schema::ProverKind::Tamarin => 45,
224+
crate::schema::ProverKind::ProVerif => 46,
225+
crate::schema::ProverKind::KeY => 47,
226+
crate::schema::ProverKind::DReal => 48,
227+
crate::schema::ProverKind::ABC => 49,
228+
crate::schema::ProverKind::TypeLL => 50,
229+
crate::schema::ProverKind::KatagoriaVerifier => 51,
230+
crate::schema::ProverKind::TropicalTypeChecker => 52,
231+
crate::schema::ProverKind::ChoreographicTypeChecker => 53,
232+
crate::schema::ProverKind::EpistemicTypeChecker => 54,
233+
crate::schema::ProverKind::EchoTypeChecker => 55,
234+
crate::schema::ProverKind::SessionTypeChecker => 56,
235+
crate::schema::ProverKind::ModalTypeChecker => 57,
236+
crate::schema::ProverKind::QTTTypeChecker => 58,
237+
crate::schema::ProverKind::EffectRowTypeChecker => 59,
238+
crate::schema::ProverKind::DependentTypeChecker => 60,
239+
crate::schema::ProverKind::RefinementTypeChecker => 61,
240+
crate::schema::ProverKind::OrdinaryTypeChecker => 62,
241+
crate::schema::ProverKind::PhantomTypeChecker => 63,
242+
crate::schema::ProverKind::PolymorphicTypeChecker => 64,
243+
crate::schema::ProverKind::ExistentialTypeChecker => 65,
244+
crate::schema::ProverKind::HigherKindedTypeChecker => 66,
245+
crate::schema::ProverKind::RowTypeChecker => 67,
246+
crate::schema::ProverKind::SubtypingTypeChecker => 68,
247+
crate::schema::ProverKind::IntersectionTypeChecker => 69,
248+
crate::schema::ProverKind::UnionTypeChecker => 70,
249+
crate::schema::ProverKind::GradualTypeChecker => 71,
250+
crate::schema::ProverKind::HoareTypeChecker => 72,
251+
crate::schema::ProverKind::IndexedTypeChecker => 73,
252+
crate::schema::ProverKind::LinearTypeChecker => 74,
253+
crate::schema::ProverKind::AffineTypeChecker => 75,
254+
crate::schema::ProverKind::RelevantTypeChecker => 76,
255+
crate::schema::ProverKind::OrderedTypeChecker => 77,
256+
crate::schema::ProverKind::UniquenessTypeChecker => 78,
257+
crate::schema::ProverKind::ImmutableTypeChecker => 79,
258+
crate::schema::ProverKind::CapabilityTypeChecker => 80,
259+
crate::schema::ProverKind::BunchedTypeChecker => 81,
260+
crate::schema::ProverKind::TemporalTypeChecker => 82,
261+
crate::schema::ProverKind::ProvabilityTypeChecker => 83,
262+
crate::schema::ProverKind::ImpureTypeChecker => 84,
263+
crate::schema::ProverKind::CoeffectTypeChecker => 85,
264+
crate::schema::ProverKind::ProbabilisticTypeChecker => 86,
265+
crate::schema::ProverKind::DyadicTypeChecker => 87,
266+
crate::schema::ProverKind::HomotopyTypeChecker => 88,
267+
crate::schema::ProverKind::CubicalTypeChecker => 89,
268+
crate::schema::ProverKind::NominalTypeChecker => 90,
269+
crate::schema::ProverKind::Abella => 91,
270+
crate::schema::ProverKind::Dedukti => 92,
271+
crate::schema::ProverKind::Cameleer => 93,
272+
crate::schema::ProverKind::ACL2s => 94,
273+
crate::schema::ProverKind::IsabelleZF => 95,
274+
crate::schema::ProverKind::Boogie => 96,
275+
crate::schema::ProverKind::Naproche => 97,
276+
crate::schema::ProverKind::Matita => 98,
277+
crate::schema::ProverKind::Arend => 99,
278+
crate::schema::ProverKind::Athena => 100,
279+
crate::schema::ProverKind::LambdaProlog => 101,
280+
crate::schema::ProverKind::Mercury => 102,
281+
crate::schema::ProverKind::Nitpick => 103,
282+
crate::schema::ProverKind::Nunchaku => 104,
283+
crate::schema::ProverKind::CubicalAgda => 105,
284+
crate::schema::ProverKind::Zipperposition => 106,
285+
crate::schema::ProverKind::Prover9 => 107,
286+
crate::schema::ProverKind::OpenSmt => 108,
287+
crate::schema::ProverKind::SmtRat => 109,
288+
crate::schema::ProverKind::Rocq => 110,
289+
crate::schema::ProverKind::UppaalStratego => 111,
290+
crate::schema::ProverKind::MizAR => 112,
208291
}
209292
}
210293

@@ -241,6 +324,89 @@ pub fn ffi_to_prover_kind(ordinal: u8) -> Option<crate::schema::ProverKind> {
241324
27 => Some(crate::schema::ProverKind::MiniZinc),
242325
28 => Some(crate::schema::ProverKind::Chuffed),
243326
29 => Some(crate::schema::ProverKind::ORTools),
327+
30 => Some(crate::schema::ProverKind::Lean3),
328+
31 => Some(crate::schema::ProverKind::TypedWasm),
329+
32 => Some(crate::schema::ProverKind::SPIN),
330+
33 => Some(crate::schema::ProverKind::CBMC),
331+
34 => Some(crate::schema::ProverKind::SeaHorn),
332+
35 => Some(crate::schema::ProverKind::CaDiCaL),
333+
36 => Some(crate::schema::ProverKind::Kissat),
334+
37 => Some(crate::schema::ProverKind::MiniSat),
335+
38 => Some(crate::schema::ProverKind::NuSMV),
336+
39 => Some(crate::schema::ProverKind::TLC),
337+
40 => Some(crate::schema::ProverKind::Alloy),
338+
41 => Some(crate::schema::ProverKind::Prism),
339+
42 => Some(crate::schema::ProverKind::UPPAAL),
340+
43 => Some(crate::schema::ProverKind::FramaC),
341+
44 => Some(crate::schema::ProverKind::Viper),
342+
45 => Some(crate::schema::ProverKind::Tamarin),
343+
46 => Some(crate::schema::ProverKind::ProVerif),
344+
47 => Some(crate::schema::ProverKind::KeY),
345+
48 => Some(crate::schema::ProverKind::DReal),
346+
49 => Some(crate::schema::ProverKind::ABC),
347+
50 => Some(crate::schema::ProverKind::TypeLL),
348+
51 => Some(crate::schema::ProverKind::KatagoriaVerifier),
349+
52 => Some(crate::schema::ProverKind::TropicalTypeChecker),
350+
53 => Some(crate::schema::ProverKind::ChoreographicTypeChecker),
351+
54 => Some(crate::schema::ProverKind::EpistemicTypeChecker),
352+
55 => Some(crate::schema::ProverKind::EchoTypeChecker),
353+
56 => Some(crate::schema::ProverKind::SessionTypeChecker),
354+
57 => Some(crate::schema::ProverKind::ModalTypeChecker),
355+
58 => Some(crate::schema::ProverKind::QTTTypeChecker),
356+
59 => Some(crate::schema::ProverKind::EffectRowTypeChecker),
357+
60 => Some(crate::schema::ProverKind::DependentTypeChecker),
358+
61 => Some(crate::schema::ProverKind::RefinementTypeChecker),
359+
62 => Some(crate::schema::ProverKind::OrdinaryTypeChecker),
360+
63 => Some(crate::schema::ProverKind::PhantomTypeChecker),
361+
64 => Some(crate::schema::ProverKind::PolymorphicTypeChecker),
362+
65 => Some(crate::schema::ProverKind::ExistentialTypeChecker),
363+
66 => Some(crate::schema::ProverKind::HigherKindedTypeChecker),
364+
67 => Some(crate::schema::ProverKind::RowTypeChecker),
365+
68 => Some(crate::schema::ProverKind::SubtypingTypeChecker),
366+
69 => Some(crate::schema::ProverKind::IntersectionTypeChecker),
367+
70 => Some(crate::schema::ProverKind::UnionTypeChecker),
368+
71 => Some(crate::schema::ProverKind::GradualTypeChecker),
369+
72 => Some(crate::schema::ProverKind::HoareTypeChecker),
370+
73 => Some(crate::schema::ProverKind::IndexedTypeChecker),
371+
74 => Some(crate::schema::ProverKind::LinearTypeChecker),
372+
75 => Some(crate::schema::ProverKind::AffineTypeChecker),
373+
76 => Some(crate::schema::ProverKind::RelevantTypeChecker),
374+
77 => Some(crate::schema::ProverKind::OrderedTypeChecker),
375+
78 => Some(crate::schema::ProverKind::UniquenessTypeChecker),
376+
79 => Some(crate::schema::ProverKind::ImmutableTypeChecker),
377+
80 => Some(crate::schema::ProverKind::CapabilityTypeChecker),
378+
81 => Some(crate::schema::ProverKind::BunchedTypeChecker),
379+
82 => Some(crate::schema::ProverKind::TemporalTypeChecker),
380+
83 => Some(crate::schema::ProverKind::ProvabilityTypeChecker),
381+
84 => Some(crate::schema::ProverKind::ImpureTypeChecker),
382+
85 => Some(crate::schema::ProverKind::CoeffectTypeChecker),
383+
86 => Some(crate::schema::ProverKind::ProbabilisticTypeChecker),
384+
87 => Some(crate::schema::ProverKind::DyadicTypeChecker),
385+
88 => Some(crate::schema::ProverKind::HomotopyTypeChecker),
386+
89 => Some(crate::schema::ProverKind::CubicalTypeChecker),
387+
90 => Some(crate::schema::ProverKind::NominalTypeChecker),
388+
91 => Some(crate::schema::ProverKind::Abella),
389+
92 => Some(crate::schema::ProverKind::Dedukti),
390+
93 => Some(crate::schema::ProverKind::Cameleer),
391+
94 => Some(crate::schema::ProverKind::ACL2s),
392+
95 => Some(crate::schema::ProverKind::IsabelleZF),
393+
96 => Some(crate::schema::ProverKind::Boogie),
394+
97 => Some(crate::schema::ProverKind::Naproche),
395+
98 => Some(crate::schema::ProverKind::Matita),
396+
99 => Some(crate::schema::ProverKind::Arend),
397+
100 => Some(crate::schema::ProverKind::Athena),
398+
101 => Some(crate::schema::ProverKind::LambdaProlog),
399+
102 => Some(crate::schema::ProverKind::Mercury),
400+
103 => Some(crate::schema::ProverKind::Nitpick),
401+
104 => Some(crate::schema::ProverKind::Nunchaku),
402+
105 => Some(crate::schema::ProverKind::CubicalAgda),
403+
106 => Some(crate::schema::ProverKind::Zipperposition),
404+
107 => Some(crate::schema::ProverKind::Prover9),
405+
108 => Some(crate::schema::ProverKind::OpenSmt),
406+
109 => Some(crate::schema::ProverKind::SmtRat),
407+
110 => Some(crate::schema::ProverKind::Rocq),
408+
111 => Some(crate::schema::ProverKind::UppaalStratego),
409+
112 => Some(crate::schema::ProverKind::MizAR),
244410
_ => None,
245411
}
246412
}

0 commit comments

Comments
 (0)