@@ -251,19 +251,19 @@ export const Real = Symbol("Real");
251
251
export const Tan = Symbol ( "Tan" ) ;
252
252
253
253
/** Representation of the null type. */
254
- type Nulls = typeof Null ;
254
+ export type Nulls = typeof Null ;
255
255
256
256
/** Representation of the boolean type. */
257
- type Bools = typeof Bool ;
257
+ export type Bools = typeof Bool ;
258
258
259
259
/** Representation of the 64-bit floating point type. */
260
- type Reals = typeof Real ;
260
+ export type Reals = typeof Real ;
261
261
262
262
/** Representation of the 64-bit floating point tangent type. */
263
- type Tans = typeof Tan ;
263
+ export type Tans = typeof Tan ;
264
264
265
265
/** Representation of a bounded index type (it's just the upper bound). */
266
- type Nats = number ;
266
+ export type Nats = number ;
267
267
268
268
/** Property key for the index type ID of a vector type. */
269
269
const ind = Symbol ( "index" ) ;
@@ -432,11 +432,11 @@ const call = (f: Fn, generics: Uint32Array, args: unknown[]): unknown => {
432
432
/**
433
433
* Map from a type of a type to the type of the symbolic values it represents.
434
434
*
435
- * The result should be `Symbolic`, so this should be used in any situation
436
- * where the abstract value is being synthesized (e.g. the parameters of the
437
- * body of `fn` or `vec`, or the returned value from a call or `select`).
435
+ * This should be used in any situation where the abstract value is being
436
+ * synthesized (e.g. the parameters of the body of `fn` or `vec`, or the
437
+ * returned value from a call or `select`).
438
438
*/
439
- type ToSymbolic < T > = T extends Nulls
439
+ export type Symbolic < T > = T extends Nulls
440
440
? Null
441
441
: T extends Bools
442
442
? Bool
@@ -447,17 +447,17 @@ type ToSymbolic<T> = T extends Nulls
447
447
: T extends Nats
448
448
? Nat
449
449
: T extends Vecs < any , infer V >
450
- ? Vec < ToSymbolic < V > >
451
- : { [ K in keyof T ] : ToSymbolic < T [ K ] > } ;
450
+ ? Vec < Symbolic < V > >
451
+ : { [ K in keyof T ] : Symbolic < T [ K ] > } ;
452
452
453
453
/**
454
454
* Map from a type of a type to the type of the abstract values it represents.
455
455
*
456
- * The result should be `Value`, so this should be used in any situation where
457
- * the abstract value is provided by the user (e.g. the returned value in the
458
- * body of `fn` or `vec`, or the inputs to a call or `select).
456
+ * This should be used in any situation where the abstract value is provided by
457
+ * the user (e.g. the returned value in the body of `fn` or `vec`, or the inputs
458
+ * to a call or `select).
459
459
*/
460
- type ToValue < T > = T extends Nulls
460
+ export type Value < T > = T extends Nulls
461
461
? Null
462
462
: T extends Bools
463
463
? Bool
@@ -468,25 +468,25 @@ type ToValue<T> = T extends Nulls
468
468
: T extends Nats
469
469
? Nat
470
470
: T extends Vecs < any , infer V >
471
- ? Vec < ToValue < V > > | ToValue < V > [ ]
472
- : { [ K in keyof T ] : ToValue < T [ K ] > } ;
471
+ ? Vec < Value < V > > | Value < V > [ ]
472
+ : { [ K in keyof T ] : Value < T [ K ] > } ;
473
473
474
- /** Map from a parameter type array to a symbolic parameter value type array. */
474
+ /** Map from parameter type array to symbolic parameter value type array. */
475
475
type SymbolicParams < T > = {
476
- [ K in keyof T ] : ToSymbolic < T [ K ] > ;
476
+ [ K in keyof T ] : Symbolic < T [ K ] > ;
477
477
} ;
478
478
479
- /** Map from a parameter type array to an abstract parameter value type array. */
479
+ /** Map from parameter type array to abstract parameter value type array. */
480
480
type ValueParams < T > = {
481
- [ K in keyof T ] : ToValue < T [ K ] > ;
481
+ [ K in keyof T ] : Value < T [ K ] > ;
482
482
} ;
483
483
484
484
/** Construct an abstract function by abstractly interpreting `f` once. */
485
485
export const fn = < const P extends readonly any [ ] , const R > (
486
486
params : P ,
487
487
ret : R ,
488
- f : ( ...args : SymbolicParams < P > ) => ToValue < R > ,
489
- ) : Fn & ( ( ...args : ValueParams < P > ) => ToSymbolic < R > ) => {
488
+ f : ( ...args : SymbolicParams < P > ) => Value < R > ,
489
+ ) : Fn & ( ( ...args : ValueParams < P > ) => Symbolic < R > ) => {
490
490
// TODO: support closures
491
491
if ( context !== undefined )
492
492
throw Error ( "can't define a function while defining another function" ) ;
@@ -535,8 +535,8 @@ export const fn = <const P extends readonly any[], const R>(
535
535
export const opaque = < const P extends readonly Reals [ ] , const R extends Reals > (
536
536
params : P ,
537
537
ret : R ,
538
- f : ( ...args : JsArgs < SymbolicParams < P > > ) => ToJs < ToValue < R > > ,
539
- ) : Fn & ( ( ...args : ValueParams < P > ) => ToSymbolic < R > ) => {
538
+ f : ( ...args : JsArgs < SymbolicParams < P > > ) => ToJs < Value < R > > ,
539
+ ) : Fn & ( ( ...args : ValueParams < P > ) => Symbolic < R > ) => {
540
540
// TODO: support more complicated signatures for opaque functions
541
541
const func = new wasm . Func ( params . length , f ) ;
542
542
const g : any = ( ...args : any ) : any =>
@@ -958,15 +958,15 @@ export const xor = (p: Bool, q: Bool): Bool => {
958
958
export const select = < const T > (
959
959
cond : Bool ,
960
960
ty : T ,
961
- then : ToValue < T > ,
962
- els : ToValue < T > ,
963
- ) : ToSymbolic < T > => {
961
+ then : Value < T > ,
962
+ els : Value < T > ,
963
+ ) : Symbolic < T > => {
964
964
const ctx = getCtx ( ) ;
965
965
const t = tyId ( ctx , ty ) ;
966
966
const p = boolId ( ctx , cond ) ;
967
967
const a = valId ( ctx , t , then ) ;
968
968
const b = valId ( ctx , t , els ) ;
969
- return idVal ( ctx , t , ctx . block . select ( ctx . func , p , t , a , b ) ) as ToSymbolic < T > ;
969
+ return idVal ( ctx , t , ctx . block . select ( ctx . func , p , t , a , b ) ) as Symbolic < T > ;
970
970
} ;
971
971
972
972
/** Return the variable ID for the abstract floating point number `x`. */
@@ -1049,8 +1049,8 @@ export const geq = (x: Real, y: Real): Bool => {
1049
1049
export const vec = < const I , const T > (
1050
1050
index : I ,
1051
1051
elem : T ,
1052
- f : ( i : ToSymbolic < I > ) => ToValue < T > ,
1053
- ) : Vec < ToSymbolic < T > > => {
1052
+ f : ( i : Symbolic < I > ) => Value < T > ,
1053
+ ) : Vec < Symbolic < T > > => {
1054
1054
const ctx = getCtx ( ) ;
1055
1055
const i = tyId ( ctx , index ) ;
1056
1056
const e = tyId ( ctx , elem ) ;
@@ -1061,13 +1061,13 @@ export const vec = <const I, const T>(
1061
1061
const body = new wasm . Block ( ) ;
1062
1062
try {
1063
1063
ctx . block = body ;
1064
- out = valId ( ctx , e , f ( idVal ( ctx , i , arg ) as ToSymbolic < I > ) ) ;
1064
+ out = valId ( ctx , e , f ( idVal ( ctx , i , arg ) as Symbolic < I > ) ) ;
1065
1065
} finally {
1066
1066
if ( out === undefined ) body . free ( ) ;
1067
1067
ctx . block = block ;
1068
1068
}
1069
1069
const id = block . vec ( ctx . func , t , arg , body , out ) ;
1070
- return idVal ( ctx , t , id ) as Vec < ToSymbolic < T > > ;
1070
+ return idVal ( ctx , t , id ) as Vec < Symbolic < T > > ;
1071
1071
} ;
1072
1072
1073
1073
/** Return the variable ID for the abstract number or tangent `x`. */
0 commit comments