diff --git a/parser/src/parser.rs b/parser/src/parser.rs index 5714d0ccf90f15e501af4a075905cf052d38c0b7..af63350c17af09fd6a2ccf9d495312a91e3d2928 100644 --- a/parser/src/parser.rs +++ b/parser/src/parser.rs @@ -174,8 +174,9 @@ fn parse_expr(pair: Pair<Rule>) -> Command { Rule::Declaration => { let mut iter = pair.into_inner(); - let s = iter.next().unwrap().as_str(); - let vars = iter.next().unwrap().into_inner().map(|name| name.as_str()).collect(); + let mut string_decl = iter.next().unwrap().into_inner(); + let s = string_decl.next().unwrap().as_str(); + let vars = string_decl.next().unwrap().into_inner().map(|name| name.as_str()).collect(); let body = iter.next().map(parse_term).unwrap(); Command::Declaration(s, None, declaration::Builder::Decl(box body, vars)) diff --git a/parser/src/term.pest b/parser/src/term.pest index 0404636d8cb9f2dc1c7c10b4d747aefde8429340..7298734882ef090d6bbc44d0f7564023ed25f5af 100644 --- a/parser/src/term.pest +++ b/parser/src/term.pest @@ -36,7 +36,8 @@ Max = { ( "max" ~ "(" ~ univ ~ "," ~ univ ~ ")" ) | ( "max" ~ univ ~ univ ) } IMax = { ( "imax" ~ "(" ~ univ ~ "," ~ univ ~ ")" ) | ( "imax" ~ univ ~ univ ) } Var = { string } -VarDecl = { string ~ arg_univ } +VarDecl = ${ string ~ arg_univ } +stringDecl = ${ string ~ univ_decl } arg_univ = {".{" ~ (univ ~ ("," ~ univ)* )? ~ "}"} univ_decl = {".{" ~ (string ~ ("," ~ string)* )? ~ "}"} @@ -44,8 +45,8 @@ univ_decl = {".{" ~ (string ~ ("," ~ string)* )? ~ "}"} Command = _{ Define | Declaration | DeclarationCheckType | CheckType | GetType | DefineCheckType | Eval | ImportFile | Search} Define = { "def" ~ string ~ ":=" ~ Term } DefineCheckType = { "def" ~ string ~ ":" ~ Term ~ ":=" ~ Term } -Declaration = { "def" ~ string ~ univ_decl ~ ":=" ~ Term } -DeclarationCheckType = { "def" ~ string ~ univ_decl ~ ":" ~ Term ~ ":=" ~ Term } +Declaration = { "def" ~ stringDecl ~ ":=" ~ Term } +DeclarationCheckType = { "def" ~ stringDecl ~ ":" ~ Term ~ ":=" ~ Term } CheckType = { "check" ~ Term ~ ":" ~ Term } GetType = { "check" ~ Term } Eval = { "eval" ~ Term }