From 63a09f1a63bd4a8e245a91f28d95aee01126fb71 Mon Sep 17 00:00:00 2001
From: arthur-adjedj <arthur.adjedj@gmail.com>
Date: Thu, 22 Dec 2022 11:21:55 +0100
Subject: [PATCH] fix(parser): avoid spacing befor univ decls/vars
---
parser/src/parser.rs | 5 +++--
parser/src/term.pest | 7 ++++---
2 files changed, 7 insertions(+), 5 deletions(-)
diff --git a/parser/src/parser.rs b/parser/src/parser.rs
index 5714d0cc..af63350c 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 0404636d..72987348 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 }
--
GitLab