feat(kernel): allow printing of universe-polymorph functions with unbound universes

kernel/src/command.rs

@@ -25,6 +25,12 @@ impl Command {
 
             Command::CheckType(t1, t2) => t1.check(&t2, env).map(|_| None),
 
+            // This is only a temporary workaround. Once metavariables will be part of the system,
+            // there won't be any issue with checking/infering with a term with non-unified metavariables
+            Command::GetType(Term::Const(s, vec)) if vec.is_empty() => {
+                env.get_type_free_univ(&s).map(Some)
+            }
+
             Command::GetType(t) => t.infer(env).map(Some),
 
             Command::Eval(t) => Ok(Some(t.normal_form(env)?)),

kernel/src/declaration.rs

@@ -37,6 +37,11 @@ impl Declaration {
         }
     }
 
+    /// Returns the type linked to a definition in a given environment.
+    pub fn get_type_free_univ(&self) -> Term {
+        self.ty.clone()
+    }
+
     /// Returns the term linked to a definition in a given environment.
     /// Since the declaration might be an axiom, it might not have an associated term to reduce to, hence the Option.
     pub fn get_term(&self, vec: &[UniverseLevel]) -> Result<Option<Term>, KernelError> {

kernel/src/environment.rs

@@ -49,4 +49,12 @@ impl Environment {
             None => Err(KernelError::ConstNotFound(s.clone())),
         }
     }
+
+    /// Returns the type linked to a definition in a given environment.
+    pub fn get_type_free_univ(&self, s: &String) -> Result<Term, KernelError> {
+        match self.0.get(s) {
+            Some(decl) => Ok(decl.get_type_free_univ()),
+            None => Err(KernelError::ConstNotFound(s.clone())),
+        }
+    }
 }

kernel/src/universe.rs

@@ -87,6 +87,10 @@ impl UniverseLevel {
                     format!("{} + {}", u.pretty_print(), n)
                 }
                 Max(box n, box m) => format!("max ({}) ({})", n.pretty_print(), m.pretty_print()),
+                IMax(box _, box Zero) => "Zero".into(),
+                IMax(box n, box m @ Succ(_)) => {
+                    format!("max ({}) ({})", n.pretty_print(), m.pretty_print())
+                }
                 IMax(box n, box m) => format!("imax ({}) ({})", n.pretty_print(), m.pretty_print()),
                 Var(n) => format!("u{}", n),
             },