1
1
//! Exporting HUGR graphs to their `hugr-model` representation.
2
2
use crate :: extension:: ExtensionRegistry ;
3
3
use crate :: hugr:: internal:: HugrInternals ;
4
+ use crate :: types:: type_param:: Term ;
4
5
use crate :: {
5
6
Direction , Hugr , HugrView , IncomingPort , Node , NodeIndex as _, Port ,
6
7
extension:: { ExtensionId , OpDef , SignatureFunc } ,
@@ -14,9 +15,7 @@ use crate::{
14
15
} ,
15
16
types:: {
16
17
CustomType , EdgeKind , FuncTypeBase , MaybeRV , PolyFuncTypeBase , RowVariable , SumType ,
17
- TypeArg , TypeBase , TypeBound , TypeEnum ,
18
- type_param:: { TypeArgVariable , TypeParam } ,
19
- type_row:: TypeRowBase ,
18
+ TypeBase , TypeBound , TypeEnum , type_param:: TermVar , type_row:: TypeRowBase ,
20
19
} ,
21
20
} ;
22
21
@@ -385,7 +384,7 @@ impl<'a> Context<'a> {
385
384
let node = self . connected_function ( node) . unwrap ( ) ;
386
385
let symbol = self . node_to_id [ & node] ;
387
386
let mut args = BumpVec :: new_in ( self . bump ) ;
388
- args. extend ( call. type_args . iter ( ) . map ( |arg| self . export_type_arg ( arg) ) ) ;
387
+ args. extend ( call. type_args . iter ( ) . map ( |arg| self . export_term ( arg, None ) ) ) ;
389
388
let args = args. into_bump_slice ( ) ;
390
389
let func = self . make_term ( table:: Term :: Apply ( symbol, args) ) ;
391
390
@@ -401,7 +400,7 @@ impl<'a> Context<'a> {
401
400
let node = self . connected_function ( node) . unwrap ( ) ;
402
401
let symbol = self . node_to_id [ & node] ;
403
402
let mut args = BumpVec :: new_in ( self . bump ) ;
404
- args. extend ( load. type_args . iter ( ) . map ( |arg| self . export_type_arg ( arg) ) ) ;
403
+ args. extend ( load. type_args . iter ( ) . map ( |arg| self . export_term ( arg, None ) ) ) ;
405
404
let args = args. into_bump_slice ( ) ;
406
405
let func = self . make_term ( table:: Term :: Apply ( symbol, args) ) ;
407
406
let runtime_type = self . make_term ( table:: Term :: Wildcard ) ;
@@ -464,7 +463,7 @@ impl<'a> Context<'a> {
464
463
let node = self . export_opdef ( op. def ( ) ) ;
465
464
let params = self
466
465
. bump
467
- . alloc_slice_fill_iter ( op. args ( ) . iter ( ) . map ( |arg| self . export_type_arg ( arg) ) ) ;
466
+ . alloc_slice_fill_iter ( op. args ( ) . iter ( ) . map ( |arg| self . export_term ( arg, None ) ) ) ;
468
467
let operation = self . make_term ( table:: Term :: Apply ( node, params) ) ;
469
468
table:: Operation :: Custom ( operation)
470
469
}
@@ -473,7 +472,7 @@ impl<'a> Context<'a> {
473
472
let node = self . make_named_global_ref ( op. extension ( ) , op. unqualified_id ( ) ) ;
474
473
let params = self
475
474
. bump
476
- . alloc_slice_fill_iter ( op. args ( ) . iter ( ) . map ( |arg| self . export_type_arg ( arg) ) ) ;
475
+ . alloc_slice_fill_iter ( op. args ( ) . iter ( ) . map ( |arg| self . export_term ( arg, None ) ) ) ;
477
476
let operation = self . make_term ( table:: Term :: Apply ( node, params) ) ;
478
477
table:: Operation :: Custom ( operation)
479
478
}
@@ -806,7 +805,7 @@ impl<'a> Context<'a> {
806
805
807
806
for ( i, param) in t. params ( ) . iter ( ) . enumerate ( ) {
808
807
let name = self . bump . alloc_str ( & i. to_string ( ) ) ;
809
- let r#type = self . export_type_param ( param, Some ( ( scope, i as _ ) ) ) ;
808
+ let r#type = self . export_term ( param, Some ( ( scope, i as _ ) ) ) ;
810
809
let param = table:: Param { name, r#type } ;
811
810
params. push ( param) ;
812
811
}
@@ -854,40 +853,12 @@ impl<'a> Context<'a> {
854
853
855
854
let args = self
856
855
. bump
857
- . alloc_slice_fill_iter ( t. args ( ) . iter ( ) . map ( |p| self . export_type_arg ( p ) ) ) ;
856
+ . alloc_slice_fill_iter ( t. args ( ) . iter ( ) . map ( |p| self . export_term ( p , None ) ) ) ;
858
857
let term = table:: Term :: Apply ( symbol, args) ;
859
858
self . make_term ( term)
860
859
}
861
860
862
- pub fn export_type_arg ( & mut self , t : & TypeArg ) -> table:: TermId {
863
- match t {
864
- TypeArg :: Type { ty } => self . export_type ( ty) ,
865
- TypeArg :: BoundedNat { n } => self . make_term ( model:: Literal :: Nat ( * n) . into ( ) ) ,
866
- TypeArg :: String { arg } => self . make_term ( model:: Literal :: Str ( arg. into ( ) ) . into ( ) ) ,
867
- TypeArg :: Float { value } => self . make_term ( model:: Literal :: Float ( * value) . into ( ) ) ,
868
- TypeArg :: Bytes { value } => self . make_term ( model:: Literal :: Bytes ( value. clone ( ) ) . into ( ) ) ,
869
- TypeArg :: List { elems } => {
870
- // For now we assume that the sequence is meant to be a list.
871
- let parts = self . bump . alloc_slice_fill_iter (
872
- elems
873
- . iter ( )
874
- . map ( |elem| table:: SeqPart :: Item ( self . export_type_arg ( elem) ) ) ,
875
- ) ;
876
- self . make_term ( table:: Term :: List ( parts) )
877
- }
878
- TypeArg :: Tuple { elems } => {
879
- let parts = self . bump . alloc_slice_fill_iter (
880
- elems
881
- . iter ( )
882
- . map ( |elem| table:: SeqPart :: Item ( self . export_type_arg ( elem) ) ) ,
883
- ) ;
884
- self . make_term ( table:: Term :: Tuple ( parts) )
885
- }
886
- TypeArg :: Variable { v } => self . export_type_arg_var ( v) ,
887
- }
888
- }
889
-
890
- pub fn export_type_arg_var ( & mut self , var : & TypeArgVariable ) -> table:: TermId {
861
+ pub fn export_type_arg_var ( & mut self , var : & TermVar ) -> table:: TermId {
891
862
let node = self . local_scope . expect ( "local variable out of scope" ) ;
892
863
self . make_term ( table:: Term :: Var ( table:: VarId ( node, var. index ( ) as _ ) ) )
893
864
}
@@ -953,19 +924,19 @@ impl<'a> Context<'a> {
953
924
self . make_term ( table:: Term :: List ( parts) )
954
925
}
955
926
956
- /// Exports a `TypeParam` to a term.
927
+ /// Exports a term.
957
928
///
958
- /// The `var` argument is set when the type parameter being exported is the
929
+ /// The `var` argument is set when the term being exported is the
959
930
/// type of a parameter to a polymorphic definition. In that case we can
960
931
/// generate a `nonlinear` constraint for the type of runtime types marked as
961
932
/// `TypeBound::Copyable`.
962
- pub fn export_type_param (
933
+ pub fn export_term (
963
934
& mut self ,
964
- t : & TypeParam ,
935
+ t : & Term ,
965
936
var : Option < ( table:: NodeId , table:: VarIndex ) > ,
966
937
) -> table:: TermId {
967
938
match t {
968
- TypeParam :: Type { b } => {
939
+ Term :: RuntimeType ( b ) => {
969
940
if let ( Some ( ( node, index) ) , TypeBound :: Copyable ) = ( var, b) {
970
941
let term = self . make_term ( table:: Term :: Var ( table:: VarId ( node, index) ) ) ;
971
942
let non_linear = self . make_term_apply ( model:: CORE_NON_LINEAR , & [ term] ) ;
@@ -974,24 +945,46 @@ impl<'a> Context<'a> {
974
945
975
946
self . make_term_apply ( model:: CORE_TYPE , & [ ] )
976
947
}
977
- // This ignores the bound on the natural for now.
978
- TypeParam :: BoundedNat { .. } => self . make_term_apply ( model:: CORE_NAT_TYPE , & [ ] ) ,
979
- TypeParam :: String => self . make_term_apply ( model:: CORE_STR_TYPE , & [ ] ) ,
980
- TypeParam :: Bytes => self . make_term_apply ( model:: CORE_BYTES_TYPE , & [ ] ) ,
981
- TypeParam :: Float => self . make_term_apply ( model:: CORE_FLOAT_TYPE , & [ ] ) ,
982
- TypeParam :: List { param } => {
983
- let item_type = self . export_type_param ( param, None ) ;
948
+ Term :: BoundedNatType { .. } => self . make_term_apply ( model:: CORE_NAT_TYPE , & [ ] ) ,
949
+ Term :: StringType => self . make_term_apply ( model:: CORE_STR_TYPE , & [ ] ) ,
950
+ Term :: BytesType => self . make_term_apply ( model:: CORE_BYTES_TYPE , & [ ] ) ,
951
+ Term :: FloatType => self . make_term_apply ( model:: CORE_FLOAT_TYPE , & [ ] ) ,
952
+ Term :: ListType ( item_type) => {
953
+ let item_type = self . export_term ( item_type, None ) ;
984
954
self . make_term_apply ( model:: CORE_LIST_TYPE , & [ item_type] )
985
955
}
986
- TypeParam :: Tuple { params } => {
987
- let parts = self . bump . alloc_slice_fill_iter (
956
+ Term :: TupleType ( params) => {
957
+ let item_types = self . bump . alloc_slice_fill_iter (
988
958
params
989
959
. iter ( )
990
- . map ( |param| table:: SeqPart :: Item ( self . export_type_param ( param, None ) ) ) ,
960
+ . map ( |param| table:: SeqPart :: Item ( self . export_term ( param, None ) ) ) ,
991
961
) ;
992
- let types = self . make_term ( table:: Term :: List ( parts ) ) ;
962
+ let types = self . make_term ( table:: Term :: List ( item_types ) ) ;
993
963
self . make_term_apply ( model:: CORE_TUPLE_TYPE , & [ types] )
994
964
}
965
+ Term :: Runtime ( ty) => self . export_type ( ty) ,
966
+ Term :: BoundedNat ( value) => self . make_term ( model:: Literal :: Nat ( * value) . into ( ) ) ,
967
+ Term :: String ( value) => self . make_term ( model:: Literal :: Str ( value. into ( ) ) . into ( ) ) ,
968
+ Term :: Float ( value) => self . make_term ( model:: Literal :: Float ( * value) . into ( ) ) ,
969
+ Term :: Bytes ( value) => self . make_term ( model:: Literal :: Bytes ( value. clone ( ) ) . into ( ) ) ,
970
+ Term :: List ( elems) => {
971
+ let parts = self . bump . alloc_slice_fill_iter (
972
+ elems
973
+ . iter ( )
974
+ . map ( |elem| table:: SeqPart :: Item ( self . export_term ( elem, None ) ) ) ,
975
+ ) ;
976
+ self . make_term ( table:: Term :: List ( parts) )
977
+ }
978
+ Term :: Tuple ( elems) => {
979
+ let parts = self . bump . alloc_slice_fill_iter (
980
+ elems
981
+ . iter ( )
982
+ . map ( |elem| table:: SeqPart :: Item ( self . export_term ( elem, None ) ) ) ,
983
+ ) ;
984
+ self . make_term ( table:: Term :: Tuple ( parts) )
985
+ }
986
+ Term :: Variable ( v) => self . export_type_arg_var ( v) ,
987
+ Term :: StaticType => self . make_term_apply ( model:: CORE_STATIC , & [ ] ) ,
995
988
}
996
989
}
997
990
0 commit comments