Skip to content

Commit

Permalink
Add documentation for Sort and a commented out suggestion for Sort::U…
Browse files Browse the repository at this point in the history
…nknown

Signed-off-by: Oded Padon <[email protected]>
  • Loading branch information
odedp committed Jul 23, 2023
1 parent 22c9451 commit 1b6cd39
Show file tree
Hide file tree
Showing 2 changed files with 10 additions and 3 deletions.
2 changes: 1 addition & 1 deletion fly/src/parser.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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!{
Expand Down
11 changes: 9 additions & 2 deletions fly/src/syntax.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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 {
Expand Down Expand Up @@ -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())
}
Expand Down

0 comments on commit 1b6cd39

Please sign in to comment.