@@ -139,6 +139,9 @@ pub enum Term {
139139 /// - see [`Term::new_var_use`]
140140 #[ display( "{_0}" ) ]
141141 Variable ( TermVar ) ,
142+
143+ /// The type of constants for a runtime type.
144+ Const ( Box < Type > ) ,
142145}
143146
144147impl Term {
@@ -169,6 +172,11 @@ impl Term {
169172 Self :: TupleType ( Box :: new ( item_types. into ( ) ) )
170173 }
171174
175+ /// Creates a new [`Term::Const`] from a runtime type.
176+ pub fn new_const ( ty : impl Into < Type > ) -> Self {
177+ Self :: Const ( Box :: new ( ty. into ( ) ) )
178+ }
179+
172180 /// Checks if this term is a supertype of another.
173181 ///
174182 /// The subtyping relation applies primarily to terms that represent static
@@ -369,6 +377,7 @@ impl Term {
369377 Term :: ListType ( item_type) => item_type. validate ( var_decls) ,
370378 Term :: TupleType ( item_types) => item_types. validate ( var_decls) ,
371379 Term :: StaticType => Ok ( ( ) ) ,
380+ Term :: Const ( ty) => ty. validate ( var_decls) ,
372381 }
373382 }
374383
@@ -432,6 +441,7 @@ impl Term {
432441 Term :: ListType ( item_type) => Term :: new_list_type ( item_type. substitute ( t) ) ,
433442 Term :: TupleType ( item_types) => Term :: new_list_type ( item_types. substitute ( t) ) ,
434443 Term :: StaticType => self . clone ( ) ,
444+ Term :: Const ( ty) => Term :: new_const ( ty. substitute1 ( t) ) ,
435445 }
436446 }
437447
@@ -593,6 +603,7 @@ impl Transformable for Term {
593603 Term :: StaticType => Ok ( false ) ,
594604 TypeArg :: ListConcat ( lists) => lists. transform ( tr) ,
595605 TypeArg :: TupleConcat ( tuples) => tuples. transform ( tr) ,
606+ Term :: Const ( ty) => ty. transform ( tr) ,
596607 }
597608 }
598609}
@@ -685,6 +696,7 @@ pub fn check_term_type(term: &Term, type_: &Term) -> Result<(), TermTypeError> {
685696 ( Term :: ListType { .. } , Term :: StaticType ) => Ok ( ( ) ) ,
686697 ( Term :: TupleType ( _) , Term :: StaticType ) => Ok ( ( ) ) ,
687698 ( Term :: RuntimeType ( _) , Term :: StaticType ) => Ok ( ( ) ) ,
699+ ( Term :: Const ( _) , Term :: StaticType ) => Ok ( ( ) ) ,
688700
689701 _ => Err ( TermTypeError :: TypeMismatch {
690702 term : term. clone ( ) ,
0 commit comments