4
4
use std:: { cell:: RefCell , cmp, fmt, mem, rc:: Rc , sync:: Arc } ;
5
5
6
6
use crate :: core:: { Term , TypedNode , TypedProgram } ;
7
- use crate :: jet:: type_name:: TypeName ;
8
7
use crate :: jet:: Application ;
9
8
use crate :: merkle:: cmr;
10
9
use crate :: merkle:: common:: { MerkleRoot , TypeMerkleRoot } ;
@@ -14,14 +13,14 @@ use crate::Error;
14
13
use super :: term:: UntypedProgram ;
15
14
16
15
#[ derive( Clone , Debug ) ]
17
- enum Type {
16
+ pub ( crate ) enum Type {
18
17
Unit ,
19
18
Sum ( RcVar , RcVar ) ,
20
19
Product ( RcVar , RcVar ) ,
21
20
}
22
21
23
22
impl Type {
24
- fn into_rcvar ( self ) -> RcVar {
23
+ pub ( crate ) fn into_rcvar ( self ) -> RcVar {
25
24
Rc :: new ( RefCell :: new ( UnificationVar :: concrete ( self ) ) )
26
25
}
27
26
}
@@ -218,7 +217,7 @@ impl FinalType {
218
217
}
219
218
220
219
#[ derive( Clone ) ]
221
- enum Variable {
220
+ pub ( crate ) enum Variable {
222
221
/// Free variable
223
222
Free ,
224
223
/// Bound to some type (which may itself contain other free variables,
@@ -243,7 +242,7 @@ impl fmt::Debug for Variable {
243
242
}
244
243
}
245
244
246
- struct UnificationVar {
245
+ pub ( crate ) struct UnificationVar {
247
246
var : Variable ,
248
247
rank : usize ,
249
248
}
@@ -254,7 +253,7 @@ impl fmt::Debug for UnificationVar {
254
253
}
255
254
}
256
255
257
- type RcVar = Rc < RefCell < UnificationVar > > ;
256
+ pub ( crate ) type RcVar = Rc < RefCell < UnificationVar > > ;
258
257
259
258
impl UnificationVar {
260
259
fn free ( ) -> UnificationVar {
@@ -375,49 +374,6 @@ struct UnificationArrow {
375
374
target : Rc < RefCell < UnificationVar > > ,
376
375
}
377
376
378
- // b'1' = 49
379
- // b'2' = 50
380
- // b'i' = 105
381
- // b'l' = 108
382
- // b'h' = 104
383
- // b'+' = 43
384
- // b'*' = 42
385
- /// Convert a [`TypeName`] into a [`Type`]
386
- fn type_from_name ( name : & TypeName , pow2s : & [ RcVar ] ) -> Type {
387
- let it = name. 0 . iter ( ) . rev ( ) ;
388
- let mut stack = Vec :: new ( ) ;
389
-
390
- for c in it {
391
- match c {
392
- b'1' => stack. push ( Type :: Unit ) ,
393
- b'2' => {
394
- let unit = Type :: Unit . into_rcvar ( ) ;
395
- stack. push ( Type :: Sum ( unit. clone ( ) , unit) )
396
- }
397
- b'i' => stack. push ( Type :: Product ( pow2s[ 4 ] . clone ( ) , pow2s[ 4 ] . clone ( ) ) ) ,
398
- b'l' => stack. push ( Type :: Product ( pow2s[ 5 ] . clone ( ) , pow2s[ 5 ] . clone ( ) ) ) ,
399
- b'h' => stack. push ( Type :: Product ( pow2s[ 7 ] . clone ( ) , pow2s[ 7 ] . clone ( ) ) ) ,
400
- b'+' | b'*' => {
401
- let left = stack. pop ( ) . expect ( "Illegal type name syntax!" ) . into_rcvar ( ) ;
402
- let right = stack. pop ( ) . expect ( "Illegal type name syntax!" ) . into_rcvar ( ) ;
403
-
404
- match c {
405
- b'+' => stack. push ( Type :: Sum ( left, right) ) ,
406
- b'*' => stack. push ( Type :: Product ( left, right) ) ,
407
- _ => unreachable ! ( ) ,
408
- }
409
- }
410
- _ => panic ! ( "Illegal type name syntax!" ) ,
411
- }
412
- }
413
-
414
- if stack. len ( ) == 1 {
415
- stack. pop ( ) . unwrap ( )
416
- } else {
417
- panic ! ( "Illegal type name syntax!" )
418
- }
419
- }
420
-
421
377
/// Attach types to all nodes in a program
422
378
pub ( crate ) fn type_check < Witness , App : Application > (
423
379
program : UntypedProgram < Witness , App > ,
@@ -557,9 +513,9 @@ pub(crate) fn type_check<Witness, App: Application>(
557
513
unify ( rcs[ j] . target . clone ( ) , var_d) ?;
558
514
}
559
515
Term :: Jet ( jet) => {
560
- bind ( & node. source , type_from_name ( & jet. source_ty , & pow2s[ ..] ) ) ?;
516
+ bind ( & node. source , jet. source_ty . to_type ( & pow2s[ ..] ) ) ?;
561
517
562
- bind ( & node. target , type_from_name ( & jet. target_ty , & pow2s[ ..] ) ) ?;
518
+ bind ( & node. target , jet. target_ty . to_type ( & pow2s[ ..] ) ) ?;
563
519
}
564
520
Term :: Witness ( ..) | Term :: Hidden ( ..) | Term :: Fail ( ..) => {
565
521
// No type constraints
0 commit comments