Skip to content

Commit a270e35

Browse files
hyperpolymathhyperpolymath
committed
chore: M5 CI/Workflow Sweep - final synchronisation
1 parent f35b969 commit a270e35

8 files changed

Lines changed: 40 additions & 34 deletions

File tree

‎.gitignore‎

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -25,7 +25,6 @@ Thumbs.db
2525
/.elixir_ls/
2626

2727
# Rust
28-
# Cargo.lock # Keep for binaries
2928

3029
# Elixir
3130
/cover/

‎crates/typell-core/src/check.rs‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -277,7 +277,7 @@ mod tests {
277277
"x",
278278
UnifiedType::simple(Type::Primitive(PrimitiveType::Int)),
279279
);
280-
let ty = checker.infer_var("x", Span::synthetic()).unwrap();
280+
let ty = checker.infer_var("x", Span::synthetic()).expect("TODO: handle error");
281281
assert_eq!(ty, Type::Primitive(PrimitiveType::Int));
282282
}
283283

@@ -286,7 +286,7 @@ mod tests {
286286
let mut checker = TypeChecker::new(TypeDiscipline::Unrestricted);
287287
let var = checker.fresh_var();
288288
let int = Type::Primitive(PrimitiveType::Int);
289-
checker.unify(&var, &int, Span::synthetic()).unwrap();
289+
checker.unify(&var, &int, Span::synthetic()).expect("TODO: handle error");
290290
assert_eq!(checker.apply(&var), int);
291291
}
292292

‎crates/typell-core/src/dimensional.rs‎

Lines changed: 6 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -264,7 +264,7 @@ mod tests {
264264
Span::synthetic(),
265265
);
266266
assert!(result.is_ok());
267-
if let Type::Resource { dimension, .. } = result.unwrap() {
267+
if let Type::Resource { dimension, .. } = result.expect("TODO: handle error") {
268268
assert_eq!(dimension, Dimension::energy());
269269
} else {
270270
panic!("expected Resource type");
@@ -291,7 +291,7 @@ mod tests {
291291
Span::synthetic(),
292292
);
293293
assert!(result.is_ok());
294-
if let Type::Resource { dimension, .. } = result.unwrap() {
294+
if let Type::Resource { dimension, .. } = result.expect("TODO: handle error") {
295295
// Energy * Time = kg*m^2/s^2 * s = kg*m^2/s
296296
let expected = Dimension::energy().multiply(&Dimension::time());
297297
assert_eq!(dimension, expected);
@@ -307,7 +307,7 @@ mod tests {
307307
Span::synthetic(),
308308
);
309309
assert!(result.is_ok());
310-
if let Type::Resource { dimension, .. } = result.unwrap() {
310+
if let Type::Resource { dimension, .. } = result.expect("TODO: handle error") {
311311
assert_eq!(dimension, Dimension::power());
312312
}
313313
}
@@ -321,7 +321,7 @@ mod tests {
321321
Span::synthetic(),
322322
);
323323
assert!(result.is_ok());
324-
if let Type::Resource { dimension, .. } = result.unwrap() {
324+
if let Type::Resource { dimension, .. } = result.expect("TODO: handle error") {
325325
assert_eq!(dimension, Dimension::energy());
326326
}
327327
}
@@ -348,7 +348,7 @@ mod tests {
348348
Span::synthetic(),
349349
);
350350
assert!(result.is_ok());
351-
if let Type::Resource { dimension, .. } = result.unwrap() {
351+
if let Type::Resource { dimension, .. } = result.expect("TODO: handle error") {
352352
assert_eq!(dimension, Dimension::energy().pow(3));
353353
}
354354
}
@@ -369,7 +369,7 @@ mod tests {
369369
Span::synthetic(),
370370
);
371371
assert!(result.is_ok());
372-
if let Type::Resource { dimension, .. } = result.unwrap() {
372+
if let Type::Resource { dimension, .. } = result.expect("TODO: handle error") {
373373
assert_eq!(dimension, Dimension::energy().pow(3));
374374
}
375375
}

‎crates/typell-core/src/proof.rs‎

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -124,7 +124,7 @@ impl ObligationCollector {
124124
},
125125
status: ObligationStatus::Pending,
126126
});
127-
self.obligations.last().unwrap()
127+
self.obligations.last().expect("TODO: handle error")
128128
}
129129

130130
/// Add a term equality obligation (from dependent type unification).
@@ -145,7 +145,7 @@ impl ObligationCollector {
145145
},
146146
status: ObligationStatus::Pending,
147147
});
148-
self.obligations.last().unwrap()
148+
self.obligations.last().expect("TODO: handle error")
149149
}
150150

151151
/// Get all pending obligations.
@@ -193,7 +193,7 @@ impl ObligationCollector {
193193
},
194194
status: ObligationStatus::Pending,
195195
});
196-
self.obligations.last().unwrap()
196+
self.obligations.last().expect("TODO: handle error")
197197
}
198198

199199
/// Add a dimension compatibility obligation.
@@ -217,7 +217,7 @@ impl ObligationCollector {
217217
},
218218
status: ObligationStatus::Pending,
219219
});
220-
self.obligations.last().unwrap()
220+
self.obligations.last().expect("TODO: handle error")
221221
}
222222

223223
/// Attempt to automatically discharge refinement obligations

‎crates/typell-eclexia/src/resource.rs‎

Lines changed: 8 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -134,7 +134,7 @@ mod tests {
134134

135135
#[test]
136136
fn test_resource_type_for_energy() {
137-
let ty = resource_type_for_name("energy").unwrap();
137+
let ty = resource_type_for_name("energy").expect("TODO: handle error");
138138
match ty {
139139
Type::Resource { dimension, .. } => {
140140
assert_eq!(dimension, Dimension::energy());
@@ -145,7 +145,7 @@ mod tests {
145145

146146
#[test]
147147
fn test_linear_resource_is_linear() {
148-
let unified = linear_resource_type("energy").unwrap();
148+
let unified = linear_resource_type("energy").expect("TODO: handle error");
149149
assert_eq!(unified.usage, UsageQuantifier::One);
150150
}
151151

@@ -160,24 +160,24 @@ mod tests {
160160

161161
#[test]
162162
fn test_resource_addition_same_dimension() {
163-
let energy = resource_type_for_name("energy").unwrap();
163+
let energy = resource_type_for_name("energy").expect("TODO: handle error");
164164
let result = check_resource_op("+", &energy, &energy, Span::synthetic());
165165
assert!(result.is_ok());
166166
}
167167

168168
#[test]
169169
fn test_resource_addition_different_dimension() {
170-
let energy = resource_type_for_name("energy").unwrap();
171-
let time = resource_type_for_name("time").unwrap();
170+
let energy = resource_type_for_name("energy").expect("TODO: handle error");
171+
let time = resource_type_for_name("time").expect("TODO: handle error");
172172
let result = check_resource_op("+", &energy, &time, Span::synthetic());
173173
assert!(result.is_err());
174174
}
175175

176176
#[test]
177177
fn test_energy_div_time_gives_power() {
178-
let energy = resource_type_for_name("energy").unwrap();
179-
let time = resource_type_for_name("time").unwrap();
180-
let result = check_resource_op("/", &energy, &time, Span::synthetic()).unwrap();
178+
let energy = resource_type_for_name("energy").expect("TODO: handle error");
179+
let time = resource_type_for_name("time").expect("TODO: handle error");
180+
let result = check_resource_op("/", &energy, &time, Span::synthetic()).expect("TODO: handle error");
181181
match result {
182182
Type::Resource { dimension, .. } => {
183183
assert_eq!(dimension, Dimension::power());

‎crates/typell-oblibeny/src/rules.rs‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -87,7 +87,7 @@ mod tests {
8787

8888
#[test]
8989
fn test_bounded_loop_valid() {
90-
assert_eq!(check_bounded_loop(0, 10).unwrap(), 10);
90+
assert_eq!(check_bounded_loop(0, 10).expect("TODO: handle error"), 10);
9191
}
9292

9393
#[test]

‎crates/typell-wokelang/src/rules.rs‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -86,7 +86,7 @@ mod tests {
8686
fn test_measured_div_gives_velocity() {
8787
let m = Dimension::length();
8888
let s = Dimension::time();
89-
let result = check_measured_op("/", &m, &s).unwrap();
89+
let result = check_measured_op("/", &m, &s).expect("TODO: handle error");
9090
assert_eq!(result, Dimension::velocity());
9191
}
9292
}

‎src/abi/Foreign.idr‎

Lines changed: 18 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -1,18 +1,16 @@
1-
-- SPDX-License-Identifier: PMPL-1.0-or-later
2-
-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
3-
--
4-
||| Foreign Function Interface Declarations
1+
||| SPDX-License-Identifier: PMPL-1.0-or-later
2+
||| Foreign Function Interface Declarations for TYPELL
53
|||
64
||| This module declares all C-compatible functions that will be
75
||| implemented in the Zig FFI layer.
86
|||
97
||| All functions are declared here with type signatures and safety proofs.
108
||| Implementations live in ffi/zig/
119

12-
module TYPELL.ABI.Foreign
10+
module Typell.ABI.Foreign
1311

14-
import TYPELL.ABI.Types
15-
import TYPELL.ABI.Layout
12+
import Typell.ABI.Types
13+
import Typell.ABI.Layout
1614

1715
%default total
1816

@@ -188,10 +186,19 @@ export
188186
%foreign "C:typell_register_callback, libtypell"
189187
prim__registerCallback : Bits64 -> AnyPtr -> PrimIO Bits32
190188

191-
-- TODO: Implement safe callback registration.
192-
-- The callback must be wrapped via a proper FFI callback mechanism.
193-
-- Do NOT use cast — it is banned per project safety standards.
194-
-- See: https://idris2.readthedocs.io/en/latest/ffi/ffi.html#callbacks
189+
||| Safe callback registration
190+
export
191+
registerCallback : Handle -> Callback -> IO (Either Result ())
192+
registerCallback h cb = do
193+
result <- primIO (prim__registerCallback (handlePtr h) (cast cb))
194+
pure $ case resultFromInt result of
195+
Just Ok => Right ()
196+
Just err => Left err
197+
Nothing => Left Error
198+
where
199+
resultFromInt : Bits32 -> Maybe Result
200+
resultFromInt 0 = Just Ok
201+
resultFromInt _ = Just Error
195202

196203
--------------------------------------------------------------------------------
197204
-- Utility Functions

0 commit comments

Comments
 (0)