From 1b6cd39d510ad4e972d21ea79e65cce677f13c2c Mon Sep 17 00:00:00 2001
From: Oded Padon <oded.padon@gmail.com>
Date: Sat, 22 Jul 2023 19:45:13 -0700
Subject: [PATCH] Add documentation for Sort and a commented out suggestion for
 Sort::Unknown

Signed-off-by: Oded Padon <oded.padon@gmail.com>
---
 fly/src/parser.rs |  2 +-
 fly/src/syntax.rs | 11 +++++++++--
 2 files changed, 10 insertions(+), 3 deletions(-)

diff --git a/fly/src/parser.rs b/fly/src/parser.rs
index 902c9736..294efb60 100644
--- a/fly/src/parser.rs
+++ b/fly/src/parser.rs
@@ -37,7 +37,7 @@ grammar parser() for str {
     =  "(" name:ident() _ ":" _ sort:sort() ")" { Binder {name, sort } } /
         name:ident() sort:(_ ":" _ s:sort() { s })? { Binder {
             name,
-            sort: sort.unwrap_or(Sort::uninterpreted(""))
+            sort: sort.unwrap_or(Sort::unknown())
         } }
 
     pub(super) rule term() -> Term = precedence!{
diff --git a/fly/src/syntax.rs b/fly/src/syntax.rs
index 5b8a9931..b19cf14c 100644
--- a/fly/src/syntax.rs
+++ b/fly/src/syntax.rs
@@ -12,11 +12,19 @@ use crate::ouritertools::OurItertools;
 
 /// A Sort represents a collection of values, which can be the built-in boolean
 /// sort or a named sort (coming from a Signature).
-#[allow(missing_docs)]
 #[derive(PartialEq, Eq, Clone, Debug, Hash, Serialize, PartialOrd, Ord)]
 pub enum Sort {
+    /// Boolean sort
     Bool,
+    /// Uninterpreted sort identified by its name
     Uninterpreted(String),
+    /*
+    /// Unspecified sort
+    ///
+    /// This is used in sort inference, and assumed to not occur anywhere after
+    /// sort inference.
+    Unknown,
+    */
 }
 
 impl Sort {
@@ -192,7 +200,6 @@ impl Term {
     }
 
     /// Smart constructor for Id
-    /// TODO(oded): should this take AsRef<str>?
     pub fn id(name: &str) -> Self {
         Self::Id(name.to_string())
     }