feat: add clafer modelling support

Author: oahshtsua

Cargo.lock

@@ -12,6 +12,8 @@ anyhow = "1.0.101"
 chrono = "0.4.44"
 clap = { version = "4.5.59", features = ["derive"] }
 git2 = "0.20.4"
+pest = "2.8.6"
+pest_derive = "2.8.6"
 regex = "1.12.3"
 serde = { version = "1.0.228", features = ["derive"] }
 serde_json = "1.0.149"

Cargo.toml

@@ -0,0 +1,3 @@
+pub mod ast;
+pub mod evaluator;
+pub mod grammar;

src/parser.rs

@@ -0,0 +1,35 @@
+#[derive(Debug, Clone)]
+pub enum Declaration {
+    EnumDecl(String, Vec<String>),
+    Element(Element),
+}
+
+#[derive(Debug, Clone)]
+pub enum Element {
+    Clafer(Clafer),
+    Constraint(Expr),
+}
+
+#[derive(Debug, Clone, PartialEq)]
+pub enum Expr {
+    Ref(String),
+    Not(Box<Expr>),
+    And(Box<Expr>, Box<Expr>),
+    Or(Box<Expr>, Box<Expr>),
+    Xor(Box<Expr>, Box<Expr>),
+    Implies(Box<Expr>, Box<Expr>),
+    Iff(Box<Expr>, Box<Expr>),
+    /// Anything outside the boolean-feature subset (comparisons, arithmetic,
+    /// joins, literals). Always evaluates to "unknown" during resolution.
+    Other(String),
+}
+
+#[derive(Debug, Clone)]
+pub struct Clafer {
+    pub is_abstract: bool,
+    pub gcard: Option<String>,
+    pub name: String,
+    pub super_type: Option<String>,
+    pub card: Option<String>,
+    pub children: Vec<Element>,
+}

src/parser/ast.rs

@@ -0,0 +1,75 @@
+Module.         Module ::= [Declaration] ;
+
+EnumDecl.       Declaration ::= "enum" PosIdent "=" [EnumId] ;
+ElementDecl.    Declaration ::= Element ;
+
+Clafer.         Clafer ::= Abstract GCard PosIdent Super Reference Card Init Elements ;
+Constraint.     Constraint ::= "[" Exp "]" ;
+
+AbstractEmpty.  Abstract ::= ;
+Abstract.       Abstract ::= "abstract" ;
+
+ElementsEmpty.  Elements ::= ;
+ElementsList.   Elements ::= "{" [Element] "}" ;
+
+Subclafer.      Element ::= Clafer ;
+Subconstraint.  Element ::= Constraint ;
+
+SuperEmpty.     Super ::= ;
+SuperSome.      Super ::= ":" Exp8 ;
+
+ReferenceEmpty. Reference ::= ;
+ReferenceSet.   Reference ::= "->" Exp6 ;
+
+InitEmpty.      Init ::= ;
+InitConstant.   Init ::= "=" Exp ;
+
+GCardEmpty.     GCard ::= ;
+GCardXor.       GCard ::= "xor" ;
+GCardOr.        GCard ::= "or" ;
+GCardMux.       GCard ::= "mux" ;
+GCardOpt.       GCard ::= "opt" ;
+GCardInterval.  GCard ::= NCard ;
+
+CardEmpty.      Card ::= ;
+CardLone.       Card ::= "?" ;
+CardSome.       Card ::= "+" ;
+CardAny.        Card ::= "*" ;
+CardNum.        Card ::= PosInteger ;
+CardInterval.   Card ::= NCard ;
+
+NCard.          NCard  ::= PosInteger ".." ExInteger ;
+ExIntegerAst.   ExInteger ::= "*" ;
+ExIntegerNum.   ExInteger ::= PosInteger ;
+
+-- Boolean & Relational Expressions (Precedence modeled via Exp levels)
+EIff.           Exp   ::= Exp "<=>" Exp1 ;
+EImplies.       Exp1  ::= Exp1 "=>"  Exp2 ;
+EOr.            Exp2  ::= Exp2 "||"  Exp3 ;
+EXor.           Exp3  ::= Exp3 "xor" Exp4 ;
+EAnd.           Exp4  ::= Exp4 "&&"  Exp5 ;
+ENeg.           Exp5  ::= "!" Exp5 ;
+ELt.            Exp6  ::= Exp6 "<"  Exp7 ;
+EGt.            Exp6  ::= Exp6 ">"  Exp7 ;
+EEq.            Exp6  ::= Exp6 "="  Exp7 ;
+ELte.           Exp6  ::= Exp6 "<=" Exp7 ;
+EGte.           Exp6  ::= Exp6 ">=" Exp7 ;
+ENeq.           Exp6  ::= Exp6 "!=" Exp7 ;
+EIn.            Exp6  ::= Exp6 "in" Exp7 ;
+ENin.           Exp6  ::= Exp6 "not" "in" Exp7 ;
+EAdd.           Exp7  ::= Exp7 "+" Exp8 ;
+ESub.           Exp7  ::= Exp7 "-" Exp8 ;
+EJoin.          Exp8  ::= Exp8 "." Exp9 ;
+
+EQuantExp.      Exp9  ::= Quant Exp10 ;
+ClaferId.       Exp10 ::= PosIdent ;
+EInt.           Exp10 ::= PosInteger ;
+EStr.           Exp10 ::= PosString ;
+EParens.        Exp10 ::= "(" Exp ")" ;
+
+QuantNo.        Quant ::= "no" ;
+QuantNot.       Quant ::= "not" ;
+QuantLone.      Quant ::= "lone" ;
+QuantOne.       Quant ::= "one" ;
+QuantSome.      Quant ::= "some" ;
+QuantAll.       Quant ::= "all" ;

src/parser/clafer-subset.cf

@@ -0,0 +1,65 @@
+// --- Entry Point ---
+module = { SOI ~ declaration* ~ EOI }
+
+// --- Declarations ---
+declaration = { enum_decl | element }
+enum_decl   = { "enum" ~ ident ~ "=" ~ ident ~ ("|" ~ ident)* }
+element     = { clafer | constraint }
+
+// --- Clafer Core ---
+clafer = { 
+    abstract_mod? ~ 
+    gcard? ~ 
+    ident ~ 
+    super_mod? ~ 
+    ref_mod? ~ 
+    card? ~ 
+    init_mod? ~ 
+    elements? 
+}
+
+constraint = { "[" ~ expr ~ "]" }
+elements   = { "{" ~ element* ~ "}" }
+
+// --- Modifiers ---
+abstract_mod = { "abstract" }
+super_mod    = { ":" ~ expr }
+ref_mod      = { "->" ~ expr }
+init_mod     = { "=" ~ expr }
+
+// --- Cardinalities ---
+gcard = { "xor" | "or" | "mux" | "opt" | ncard }
+card  = { "?" | "+" | "*" | ncard | int }
+ncard = { int ~ ".." ~ (int | "*") }
+
+// --- Expressions ---
+expr          =  { iff_expr }
+iff_expr      =  { implies_expr ~ ("<=>" ~ implies_expr)* }
+implies_expr  =  { or_expr ~ ("=>" ~ or_expr)* }
+or_expr       =  { xor_expr ~ ("||" ~ xor_expr)* }
+xor_expr      =  { and_expr ~ ("xor" ~ and_expr)* }
+and_expr      =  { cmp_expr ~ ("&&" ~ cmp_expr)* }
+
+cmp_expr      =  { add_expr ~ (cmp_op ~ add_expr)* }
+cmp_op        =  { "<=" | ">=" | "<" | ">" | "=" | "!=" | "not in" | "in" }
+
+add_expr      =  { join_expr ~ (add_op ~ join_expr)* }
+add_op        =  { "+" | "-" }
+
+join_expr     =  { primary ~ ("." ~ primary)* }
+
+primary       =  { unary_op* ~ quantifier? ~ (ident | int | str | "(" ~ expr ~ ")") }
+unary_op      =  { "!" | "-" }
+quantifier    =  { "no" | "not" | "lone" | "one" | "some" | "all" }
+
+// --- Tokens ---
+ident = @{ ASCII_ALPHA ~ (ASCII_ALPHANUMERIC | "_" | "'")* }
+int   = @{ ASCII_DIGIT+ }
+str   = @{ "\"" ~ (!"\"" ~ ANY)* ~ "\"" }
+
+// --- Implicit Whitespace & Comments (Silent) ---
+WHITESPACE = _{ " " | "\t" | "\r" | "\n" }
+COMMENT    = _{
+    ("//" ~ (!"\n" ~ ANY)*) |
+    ("/*" ~ (!"*/" ~ ANY)* ~ "*/") 
+}