11//! Exporting HUGR graphs to their `hugr-model` representation.
22use crate :: extension:: ExtensionRegistry ;
33use crate :: hugr:: internal:: HugrInternals ;
4+ use crate :: types:: type_param:: Term ;
45use crate :: {
56 Direction , Hugr , HugrView , IncomingPort , Node , NodeIndex as _, Port ,
67 extension:: { ExtensionId , OpDef , SignatureFunc } ,
@@ -14,9 +15,7 @@ use crate::{
1415 } ,
1516 types:: {
1617 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 ,
2019 } ,
2120} ;
2221
@@ -385,7 +384,7 @@ impl<'a> Context<'a> {
385384 let node = self . connected_function ( node) . unwrap ( ) ;
386385 let symbol = self . node_to_id [ & node] ;
387386 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 ) ) ) ;
389388 let args = args. into_bump_slice ( ) ;
390389 let func = self . make_term ( table:: Term :: Apply ( symbol, args) ) ;
391390
@@ -401,7 +400,7 @@ impl<'a> Context<'a> {
401400 let node = self . connected_function ( node) . unwrap ( ) ;
402401 let symbol = self . node_to_id [ & node] ;
403402 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 ) ) ) ;
405404 let args = args. into_bump_slice ( ) ;
406405 let func = self . make_term ( table:: Term :: Apply ( symbol, args) ) ;
407406 let runtime_type = self . make_term ( table:: Term :: Wildcard ) ;
@@ -464,7 +463,7 @@ impl<'a> Context<'a> {
464463 let node = self . export_opdef ( op. def ( ) ) ;
465464 let params = self
466465 . 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 ) ) ) ;
468467 let operation = self . make_term ( table:: Term :: Apply ( node, params) ) ;
469468 table:: Operation :: Custom ( operation)
470469 }
@@ -473,7 +472,7 @@ impl<'a> Context<'a> {
473472 let node = self . make_named_global_ref ( op. extension ( ) , op. unqualified_id ( ) ) ;
474473 let params = self
475474 . 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 ) ) ) ;
477476 let operation = self . make_term ( table:: Term :: Apply ( node, params) ) ;
478477 table:: Operation :: Custom ( operation)
479478 }
@@ -806,7 +805,7 @@ impl<'a> Context<'a> {
806805
807806 for ( i, param) in t. params ( ) . iter ( ) . enumerate ( ) {
808807 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 _ ) ) ) ;
810809 let param = table:: Param { name, r#type } ;
811810 params. push ( param) ;
812811 }
@@ -854,40 +853,12 @@ impl<'a> Context<'a> {
854853
855854 let args = self
856855 . 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 ) ) ) ;
858857 let term = table:: Term :: Apply ( symbol, args) ;
859858 self . make_term ( term)
860859 }
861860
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 {
891862 let node = self . local_scope . expect ( "local variable out of scope" ) ;
892863 self . make_term ( table:: Term :: Var ( table:: VarId ( node, var. index ( ) as _ ) ) )
893864 }
@@ -953,19 +924,19 @@ impl<'a> Context<'a> {
953924 self . make_term ( table:: Term :: List ( parts) )
954925 }
955926
956- /// Exports a `TypeParam` to a term.
927+ /// Exports a term.
957928 ///
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
959930 /// type of a parameter to a polymorphic definition. In that case we can
960931 /// generate a `nonlinear` constraint for the type of runtime types marked as
961932 /// `TypeBound::Copyable`.
962- pub fn export_type_param (
933+ pub fn export_term (
963934 & mut self ,
964- t : & TypeParam ,
935+ t : & Term ,
965936 var : Option < ( table:: NodeId , table:: VarIndex ) > ,
966937 ) -> table:: TermId {
967938 match t {
968- TypeParam :: Type { b } => {
939+ Term :: RuntimeType ( b ) => {
969940 if let ( Some ( ( node, index) ) , TypeBound :: Copyable ) = ( var, b) {
970941 let term = self . make_term ( table:: Term :: Var ( table:: VarId ( node, index) ) ) ;
971942 let non_linear = self . make_term_apply ( model:: CORE_NON_LINEAR , & [ term] ) ;
@@ -974,24 +945,46 @@ impl<'a> Context<'a> {
974945
975946 self . make_term_apply ( model:: CORE_TYPE , & [ ] )
976947 }
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 ) ;
984954 self . make_term_apply ( model:: CORE_LIST_TYPE , & [ item_type] )
985955 }
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 (
988958 params
989959 . iter ( )
990- . map ( |param| table:: SeqPart :: Item ( self . export_type_param ( param, None ) ) ) ,
960+ . map ( |param| table:: SeqPart :: Item ( self . export_term ( param, None ) ) ) ,
991961 ) ;
992- let types = self . make_term ( table:: Term :: List ( parts ) ) ;
962+ let types = self . make_term ( table:: Term :: List ( item_types ) ) ;
993963 self . make_term_apply ( model:: CORE_TUPLE_TYPE , & [ types] )
994964 }
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 , & [ ] ) ,
995988 }
996989 }
997990
0 commit comments