smt-lang 0.7.5

use std::str::FromStr;
use crate::problem::*;
use super::*;
use line_col::LineColLookup;
use fraction::Fraction;
// use std::time::Duration;

grammar<'a>(lookup: &LineColLookup<'input>, parser: &mut Parser<'a>);

match {
    r"\s*" => { }, // The default whitespace skipping is disabled an `ignore pattern` is specified
    r"//[^\n\r]*[\n\r]*" => { }, // Skip `// comments`
    r"/\*[^*]*\*+(?:[^/*][^*]*\*+)*/" => { },  // Skip `/* comments */`
    _
}

//------------------------- Problem -------------------------

pub Problem: () = Entry* Search? => {};

//------------------------- Entry -------------------------

Entry: () = {
    Include,
    Structure,
    Class,
    Instance,
    Variable,
    Function,
    Constraint,
};

//------------------------- Include -------------------------

Include: () = "include" <file:String> => {
    parser.add(file);
};

//------------------------- Structure -------------------------

Structure: () = "struct" <i:Identifier> "{" <elts:StructureElement*> "}" => {
    let position = Some(i.position.clone());
    let mut structure = Structure::new(i.name, position);
    for e in elts.iter() {
        match e {
            StructureElement::Attribute(a) => {
                structure.add_attribute(a.clone());
            },
            StructureElement::Method(m) => {
                structure.add_method(m.clone());
            }
        }
    }
    parser.problem.add_structure(structure);
};

StructureElement: StructureElement = {
    <a:StrucAttribute> => StructureElement::Attribute(a),
    <m:StrucMethod> => StructureElement::Method(m),
};

//------------------------- Strcuture Attribute -------------------------

StrucAttribute: Attribute<StructureId> = <i:Identifier> ":" <t:Type> <e:Assign?> => {
    let position = Some(i.position.clone());
    Attribute::new(i.name, t, e, position)
};

//------------------------- Structure Method -------------------------

StrucMethod: Method<StructureId> = <i:Identifier> "(" <p:Parameters> ")" ":" <t:Type> <e:Assign?> => {
    let position = Some(i.position.clone());
    let mut m = Method::new(i.name, t, e, position);
    for x in p {
        m.add_parameter(x);
    }
    m
};   

//------------------------- Class -------------------------

Class: () = "class" <i:Identifier> <e:Extends?> "{" <elts:ClassElement*> "}" => {
    let position = Some(i.position.clone());
    let mut class = Class::new(i.name, e, position);
    for e in elts.iter() {
        match e {
            ClassElement::Attribute(a) => {
                class.add_attribute(a.clone());
            },
            ClassElement::Method(m) => {
                class.add_method(m.clone());
            }
        }
    }
    parser.problem.add_class(class);
};

Extends: Type = "extends" <t:Type> => t;

ClassElement: ClassElement = {
    <a:ClassAttribute> => ClassElement::Attribute(a),
    <m:ClassMethod> => ClassElement::Method(m),
};

//------------------------- Class Attribute -------------------------

ClassAttribute: Attribute<ClassId> = <i:Identifier> ":" <t:Type> <e:Assign?> => {
    let position = Some(i.position.clone());
    Attribute::new(i.name, t, e, position)
};

//------------------------- Class Method -------------------------

ClassMethod: Method<ClassId> = <i:Identifier> "(" <p:Parameters> ")" ":" <t:Type> <e:Assign?> => {
    let position = Some(i.position.clone());
    let mut m = Method::new(i.name, t, e, position);
    for x in p {
        m.add_parameter(x);
    }
    m
};   

//------------------------- Instance -------------------------

Instance: () = "inst" <l:Identifiers> ":" <t:Type> => {
    for i in l {
        let position = Some(i.position.clone());
        let inst = Instance::new(i.name, t.clone(), position);
        parser.problem.add_instance(inst);
    }
}; 

//------------------------- Variable -------------------------

Variable: () = "let" <l:Identifiers> ":" <t:Type> <e:Assign?> => {
    for i in l {
        let position = Some(i.position.clone());
        let v = Variable::new(i.name, t.clone(), e.clone(), position);
        parser.problem.add_variable(v);
    }
};    

//------------------------- Function -------------------------

Function: () = "let" <i:Identifier> "(" <p:Parameters> ")" ":" <t:Type> <e:Assign?> => {
    let position = Some(i.position.clone());
    let mut f = Function::new(i.name, t, e, position);
    for x in p {
        f.add_parameter(x);
    }
    parser.problem.add_function(f);
};    

//------------------------- Constraint -------------------------

Constraint: () = "constraint" <i:Identifier> <e:Assign> => {
    let position = Some(i.position.clone());
    let c = Constraint::new(i.name, e, position);
    parser.problem.add_constraint(c);
};    

//------------------------- Search -------------------------

Search: () = {
    "solve" => parser.problem.set_search(Search::Solve),
    "minimize" <e:Expr> <b:Bound> => parser.problem.set_search(Search::Optimize(Box::new(e), b, true)),
    "maximize" <e:Expr> <b:Bound> => parser.problem.set_search(Search::Optimize(Box::new(e), b, false)),
};

Bound:Bound = {
    "until" <i:Integer> => Bound::Int(i as isize),
    "until" <r:Decimal> => Bound::Real(r),
};

//------------------------- Parameter -------------------------

ParameterList: Vec<Parameter> = <i:Identifier> <l:CommaIdentifier*> ":" <t:Type> => {
    let position = Some(i.position.clone());
    let mut v = Vec::new();
    v.push(Parameter::new(i.name, t.clone(), position));
    for x in l.iter() {
        let parameter = Parameter::new(x.name.clone(), t.clone(), Some(x.position.clone()));
        v.push(parameter);
    }
    v
};

Parameters: Vec<Parameter> = <p:ParameterList> <l:ParameterNext*> => {
    let mut parameters = Vec::new();
    parameters.extend(p);
    for x in l.iter() {
        parameters.extend(x.clone());
    }
    parameters
};

ParameterNext: Vec<Parameter> = "," <p:ParameterList> => p;

//------------------------- Assign -------------------------

Assign: Expr = "=" <e:Expr> => e;

//========================= Type =========================

Type: Type = {
    "Bool" => Type::Bool,
    "Int"  => Type::Int,
    "Real" => Type::Real,
    <min:Integer> ".." <max:Integer> => Type::Interval(min as isize, max as isize),
    <i:Identifier> => Type::Unresolved(i.name, Some(i.position)),
};

//========================= Expr =========================

Expr: Expr = ImpliesOrExpr;

ImpliesOrExpr: Expr = {
    <left:ImpliesOrExpr> <l:@L><op:ImpliesOrOp> <right:AndExpr> => {
        let position = Some(Position::new(parser.file(), lookup, l));
        Expr::Binary(Box::new(left), op, Box::new(right), position)
    },
    AndExpr,
};

AndExpr: Expr = {
    <left:AndExpr> <l:@L>"and" <right:CompExpr> => {
        let position = Some(Position::new(parser.file(), lookup, l));
        Expr::Binary(Box::new(left), BinOp::And, Box::new(right), position)
    },
    CompExpr,
};

CompExpr: Expr = {
    <left:CompExpr> <l:@L><op:CompOp> <right:AddSubExpr> => {
        let position = Some(Position::new(parser.file(), lookup, l));
        Expr::Binary(Box::new(left), op, Box::new(right), position)
    },
    AddSubExpr,
};

AddSubExpr: Expr = {
    <left:AddSubExpr> <l:@L><op:AddSubOp> <right:MulDivExpr> => {
        let position = Some(Position::new(parser.file(), lookup, l));
        Expr::Binary(Box::new(left), op, Box::new(right), position)
    },
    MulDivExpr,
};

MulDivExpr: Expr = {
    <left:MulDivExpr> <l:@L><op:MulDivOp> <right:UnaryExpr> => {
        let position = Some(Position::new(parser.file(), lookup, l));
        Expr::Binary(Box::new(left), op, Box::new(right), position)
    },
    UnaryExpr,
};

UnaryExpr: Expr = {
    <l:@L><op:UnaryOp> <e: UnaryExpr> => {
        let position = Some(Position::new(parser.file(), lookup, l));
        Expr::Unary(op, Box::new(e), position)
    },
    NaryExpr,
};

NaryExpr: Expr = {
    <l:@L><op:NaryOp> <v: TupleExpr> => {
        let position = Some(Position::new(parser.file(), lookup, l));
        Expr::Nary(op, v, position)
    },
    FunCallExpr,
};

FunCallExpr: Expr = {
    <i:Identifier> <p:TupleExpr> => {
        let position = Some(i.position);
        Expr::UnresolvedFunCall(i.name, p, position)
    },
    StructExpr,
};

StructExpr: Expr = {
    <e:StructExpr> "." <i:Identifier> <p:TupleExpr> => {
        let position = Some(i.position);
        Expr::UnresolvedMethCall(Box::new(e), i.name, p, position)
    },
    <e:StructExpr> "." <i:Identifier> => {
        let position = Some(i.position);
        Expr::UnresolvedAttribute(Box::new(e), i.name, position)
    },
    AsExpr,
};

AsExpr: Expr = {
    <e:AsExpr> <l:@L>"as" <min:Integer> ".." <max:Integer> => {
        let position = Position::new(parser.file(), lookup, l);
        Expr::AsInterval(Box::new(e), min as isize, max as isize, Some(position))
    },
    <e:AsExpr> <l:@L>"as" "Int" => {
        let position = Position::new(parser.file(), lookup, l);
        Expr::AsInt(Box::new(e), Some(position))
    },
    <e:AsExpr> <l:@L>"as" "Real" => {
        let position = Position::new(parser.file(), lookup, l);
        Expr::AsReal(Box::new(e), Some(position))
    },
    IfThenElseExpr,
};

IfThenElseExpr: Expr = {
    <l:@L>"if" <c:Expr> "then" <t:Expr> <v:ElifExpr*> "else" <e:Expr> "end" => {
        let pos = Some(Position::new(parser.file(), lookup, l));
        let c = Box::new(c);
        let t = Box::new(t);
        let e = Box::new(e);
        Expr::IfThenElse(c, t, v, e, pos)
    },
    QuantifierExpr
};
ElifExpr: (Expr, Expr) = "elif" <x:Expr> "then" <y:Expr> => (x, y);

QuantifierExpr: Expr = {
    <l:@L><op:QtOp><p:Parameters> "|" <e:Expr> "end" => {
        let pos = Some(Position::new(parser.file(), lookup, l));
        let e = Box::new(e);
        Expr::Quantifier(op, p, e, pos)
    },
    Term
};


Term: Expr = {
    <l:@L> <b:Boolean> => {
        let position = Position::new(parser.file(), lookup, l);
        Expr::BoolValue(b, Some(position))
    },
    <l:@L> <i:Integer> => {
        let position = Position::new(parser.file(), lookup, l);
        Expr::IntValue(i as isize, Some(position))
    },
    <l:@L> <d:Decimal> => {
        let position = Position::new(parser.file(), lookup, l);
        Expr::RealValue(d, Some(position))
    },
    <x:Identifier> => Expr::Unresolved(x.name, Some(x.position)),
    "(" <Expr> ")",
};

TupleExpr: Vec<Expr> = "(" <e:Expr> <l:CommaExpr*> ")" => {
    let mut v = Vec::new();
    v.push(e);
    v.extend(l);
    v
};
CommaExpr: Expr = "," <e:Expr> => e;

//------------------------- Operator -------------------------

ImpliesOrOp: BinOp = {
    "=>" => BinOp::Implies,
    "or" => BinOp::Or,
};

CompOp: BinOp = {
    "=" => BinOp::Eq,
    "!=" => BinOp::Ne,
    "<" => BinOp::Lt,
    "<=" => BinOp::Le,
    ">=" => BinOp::Ge,
    ">" => BinOp::Gt,
};

AddSubOp: BinOp = {
    "+" => BinOp::Add,
    "-" => BinOp::Sub,
};

MulDivOp: BinOp = {
    "*" => BinOp::Mul,
    "/" => BinOp::Div,
};

UnaryOp: UnaryOp = {
    "not" => UnaryOp::Not,
    "-" => UnaryOp::Minus,
};

QtOp: QtOp = {
    "forall" => QtOp::Forall,
    "exists" => QtOp::Exists,
    "sum" => QtOp::Sum,
    "prod" => QtOp::Prod,
    "min" => QtOp::Min,
    "max" => QtOp::Max,
};

NaryOp: NaryOp = {
    "min" => NaryOp::Min,
    "max" => NaryOp::Max,
};

//========================= Util =========================

CommaOne<T>: Vec<T> = {
    <mut v:(<T> ",")*> <e:T> => {
        v.push(e);
        v
    }
};

CommaIdentifier: Identifier = "," <i:Identifier> => i;

Identifiers: Vec<Identifier> = <i:Identifier> <l:CommaIdentifier*> => {
    let mut v = Vec::new();
    v.push(i);
    v.extend(l);
    v
};

//========================= Lexer =========================

String: String = <s:r#"".+""#> => s[1..s.len()-1].to_string();

// Duration: Duration = {
//     <i:UInteger> "sec" => Duration::from_secs(i),
//     <i:UInteger> "ms" => Duration::from_millis(i),
// };

Boolean: bool = {
    "false" => false,
    "true" => true,
};

Integer: i64 = <i:r"-?[0-9]+"> => i.parse::<i64>().unwrap();

// UInteger: u64 = <i:r"[0-9]+"> => i.parse::<u64>().unwrap();

Decimal: Fraction = <d:r"[0-9]+\.[0-9]+"> => Fraction::from_str(d).unwrap();

Identifier: Identifier = <l:@L> <s:r"[a-zA-Z][a-zA-Z_0-9]*"> <r:@R> => {
    Identifier::new(parser.file(), lookup, s, l)
};