mirror of
https://github.com/Kindelia/Kind2.git
synced 2024-10-06 04:17:14 +03:00
fix: fixed capitalized names
This commit is contained in:
parent
921e70d668
commit
82f1c41f79
@ -1,4 +1,4 @@
|
||||
use kind_report::data::DiagnosticFrame;
|
||||
use kind_report::data::{DiagnosticFrame, Marking, Severity, Color};
|
||||
use kind_span::Range;
|
||||
|
||||
use crate::lexer::tokens::Token;
|
||||
@ -19,10 +19,117 @@ pub enum SyntaxError {
|
||||
InvalidNumberRepresentation(EncodeSequence, Range),
|
||||
UnexpectedChar(char, Range),
|
||||
UnexpectedToken(Token, Range, Vec<Token>),
|
||||
LowerCasedDefinition(String, Range),
|
||||
}
|
||||
|
||||
impl Into<DiagnosticFrame> for SyntaxError {
|
||||
fn into(self) -> DiagnosticFrame {
|
||||
todo!()
|
||||
fn encode_name(encode: EncodeSequence) -> &'static str {
|
||||
match encode {
|
||||
EncodeSequence::Hexa => "hexadecimal",
|
||||
EncodeSequence::Octal => "octal",
|
||||
EncodeSequence::Binary => "binary",
|
||||
EncodeSequence::Unicode => "unicode",
|
||||
}
|
||||
}
|
||||
|
||||
impl From<Box<SyntaxError>> for DiagnosticFrame {
|
||||
fn from(err: Box<SyntaxError>) -> Self {
|
||||
match *err {
|
||||
SyntaxError::UnfinishedString(range) => DiagnosticFrame {
|
||||
code: 0,
|
||||
severity: Severity::Error,
|
||||
title: "Unfinished String".to_string(),
|
||||
subtitles: vec![],
|
||||
hints: vec!["You need to close the string with another quote, take a look at the beggining".to_string()],
|
||||
positions: vec![Marking {
|
||||
position: range,
|
||||
color: Color::Fst,
|
||||
text: "The string starts in this position!".to_string(),
|
||||
}],
|
||||
},
|
||||
SyntaxError::LowerCasedDefinition(name, range) => DiagnosticFrame {
|
||||
code: 0,
|
||||
severity: Severity::Error,
|
||||
title: "The definition name should be upper cased.".to_string(),
|
||||
subtitles: vec![],
|
||||
hints: vec![{
|
||||
let mut c = name.chars();
|
||||
let fst = c.next().unwrap().to_uppercase();
|
||||
format!("Change it to '{}{}'", fst, c.as_str()).to_string()
|
||||
}],
|
||||
positions: vec![Marking {
|
||||
position: range,
|
||||
color: Color::Fst,
|
||||
text: "Wrong case for this name".to_string(),
|
||||
}],
|
||||
},
|
||||
SyntaxError::UnfinishedComment(range) => DiagnosticFrame {
|
||||
code: 0,
|
||||
severity: Severity::Error,
|
||||
title: "Unfinished Comment".to_string(),
|
||||
subtitles: vec![],
|
||||
hints: vec!["You need to close the string with '*/', take a look at the beggining".to_string()],
|
||||
positions: vec![Marking {
|
||||
position: range,
|
||||
color: Color::Fst,
|
||||
text: "The comment starts in this position!".to_string(),
|
||||
}],
|
||||
},
|
||||
SyntaxError::InvalidEscapeSequence(kind, range) => {
|
||||
DiagnosticFrame {
|
||||
code: 0,
|
||||
severity: Severity::Error,
|
||||
title: format!("The {} character sequence is invalid!", encode_name(kind)),
|
||||
subtitles: vec![],
|
||||
hints: vec![],
|
||||
positions: vec![Marking {
|
||||
position: range,
|
||||
color: Color::Fst,
|
||||
text: "Here!".to_string(),
|
||||
}],
|
||||
}
|
||||
}
|
||||
SyntaxError::InvalidNumberRepresentation(repr, range) => DiagnosticFrame {
|
||||
code: 0,
|
||||
severity: Severity::Error,
|
||||
title: format!("The {} number sequence is invalid!", encode_name(repr)),
|
||||
subtitles: vec![],
|
||||
hints: vec![],
|
||||
positions: vec![Marking {
|
||||
position: range,
|
||||
color: Color::Fst,
|
||||
text: "Here!".to_string(),
|
||||
}],
|
||||
},
|
||||
SyntaxError::UnexpectedChar(chr, range) => DiagnosticFrame {
|
||||
code: 0,
|
||||
severity: Severity::Error,
|
||||
title: format!("The char '{}' is invalid", chr),
|
||||
subtitles: vec![],
|
||||
hints: vec!["Try to remove it!".to_string()],
|
||||
positions: vec![Marking {
|
||||
position: range,
|
||||
color: Color::Fst,
|
||||
text: "Here!".to_string(),
|
||||
}],
|
||||
},
|
||||
SyntaxError::UnexpectedToken(_token, range, _expect) => DiagnosticFrame {
|
||||
code: 0,
|
||||
severity: Severity::Error,
|
||||
title: "Unexpected token.".to_string(),
|
||||
subtitles: vec![],
|
||||
hints: vec![],
|
||||
positions: vec![Marking {
|
||||
position: range,
|
||||
color: Color::Fst,
|
||||
text: "Here!".to_string(),
|
||||
}],
|
||||
},
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
impl From<&Box<SyntaxError>> for DiagnosticFrame {
|
||||
fn from(err: &Box<SyntaxError>) -> Self {
|
||||
(err.clone()).into()
|
||||
}
|
||||
}
|
@ -54,15 +54,15 @@ impl<'a> Parser<'a> {
|
||||
}
|
||||
|
||||
pub fn is_pi_type(&self) -> bool {
|
||||
self.get().same_variant(Token::LPar) && self.peek(1).is_id() && self.peek(2).same_variant(Token::Colon)
|
||||
self.get().same_variant(Token::LPar) && self.peek(1).is_lower_id() && self.peek(2).same_variant(Token::Colon)
|
||||
}
|
||||
|
||||
pub fn is_lambda(&self) -> bool {
|
||||
self.get().is_id() && self.peek(1).same_variant(Token::FatArrow)
|
||||
self.get().is_lower_id() && self.peek(1).same_variant(Token::FatArrow)
|
||||
}
|
||||
|
||||
pub fn is_sigma_type(&self) -> bool {
|
||||
self.get().same_variant(Token::LBracket) && self.peek(1).is_id() && self.peek(2).same_variant(Token::Colon)
|
||||
self.get().same_variant(Token::LBracket) && self.peek(1).is_lower_id() && self.peek(2).same_variant(Token::Colon)
|
||||
}
|
||||
|
||||
pub fn is_substitution(&self) -> bool {
|
||||
@ -85,11 +85,19 @@ impl<'a> Parser<'a> {
|
||||
|
||||
pub fn parse_id(&mut self) -> Result<Ident, SyntaxError> {
|
||||
let range = self.range();
|
||||
let id = eat_single!(self, Token::Id(x) => x.clone())?;
|
||||
let ident = Ident::new(Symbol(id), self.ctx, range);
|
||||
let id = eat_single!(self, Token::LowerId(x) => x.clone())?;
|
||||
let ident = Ident::new(Symbol(id), self.lexer.ctx, range);
|
||||
Ok(ident)
|
||||
}
|
||||
|
||||
pub fn parse_upper_id(&mut self) -> Result<Ident, SyntaxError> {
|
||||
let range = self.range();
|
||||
let id = eat_single!(self, Token::UpperId(x) => x.clone())?;
|
||||
let ident = Ident::new(Symbol(id), self.lexer.ctx, range);
|
||||
Ok(ident)
|
||||
}
|
||||
|
||||
|
||||
fn parse_lambda(&mut self) -> Result<Box<Expr>, SyntaxError> {
|
||||
let name_span = self.range();
|
||||
|
||||
@ -156,6 +164,14 @@ impl<'a> Parser<'a> {
|
||||
}))
|
||||
}
|
||||
|
||||
fn parse_data(&mut self) -> Result<Box<Expr>, SyntaxError> {
|
||||
let id = self.parse_upper_id()?;
|
||||
Ok(Box::new(Expr {
|
||||
range: id.range,
|
||||
data: ExprKind::Data(id),
|
||||
}))
|
||||
}
|
||||
|
||||
fn parse_num(&mut self, num: u64) -> Result<Box<Expr>, SyntaxError> {
|
||||
let range = self.range();
|
||||
self.bump();
|
||||
@ -260,7 +276,7 @@ impl<'a> Parser<'a> {
|
||||
range,
|
||||
data: ExprKind::Help(Ident {
|
||||
data: Symbol(str),
|
||||
ctx: self.ctx,
|
||||
ctx: self.lexer.ctx,
|
||||
range,
|
||||
}),
|
||||
}))
|
||||
@ -277,7 +293,8 @@ impl<'a> Parser<'a> {
|
||||
|
||||
pub fn parse_atom(&mut self) -> Result<Box<Expr>, SyntaxError> {
|
||||
match self.get().clone() {
|
||||
Token::Id(_) => self.parse_var(),
|
||||
Token::LowerId(_) => self.parse_var(),
|
||||
Token::UpperId(_) => self.parse_data(),
|
||||
Token::Num(num) => self.parse_num(num),
|
||||
Token::Char(chr) => self.parse_char(chr),
|
||||
Token::Str(str) => self.parse_str(str),
|
||||
@ -285,7 +302,7 @@ impl<'a> Parser<'a> {
|
||||
Token::Help(str) => self.parse_help(str),
|
||||
Token::LBracket => self.parse_array(),
|
||||
Token::LPar => self.parse_paren(),
|
||||
_ => self.fail(vec![Token::Id("".to_string())]),
|
||||
_ => self.fail(vec![Token::LowerId("".to_string())]),
|
||||
}
|
||||
}
|
||||
|
||||
|
@ -1,4 +1,4 @@
|
||||
use kind_span::Range;
|
||||
use kind_span::{Range};
|
||||
|
||||
use crate::errors::{EncodeSequence, SyntaxError};
|
||||
use crate::lexer::tokens::Token;
|
||||
|
@ -1,5 +1,3 @@
|
||||
use std::sync::mpsc::Sender;
|
||||
|
||||
use kind_span::Range;
|
||||
|
||||
use crate::errors::SyntaxError;
|
||||
@ -36,8 +34,8 @@ impl<'a> Lexer<'a> {
|
||||
count > 0
|
||||
}
|
||||
|
||||
pub fn to_keyword(str: &str) -> Token {
|
||||
match str {
|
||||
pub fn to_keyword(data: &str) -> Token {
|
||||
match data {
|
||||
"ask" => Token::Ask,
|
||||
"do" => Token::Do,
|
||||
"if" => Token::If,
|
||||
@ -46,16 +44,22 @@ impl<'a> Lexer<'a> {
|
||||
"let" => Token::Let,
|
||||
"open" => Token::Open,
|
||||
"return" => Token::Return,
|
||||
_ => Token::Id(str.to_string()),
|
||||
_ => {
|
||||
if data.bytes().next().map(|x| x.is_ascii_uppercase()).unwrap_or(false) {
|
||||
Token::UpperId(data.to_string())
|
||||
}else {
|
||||
Token::LowerId(data.to_string())
|
||||
}
|
||||
},
|
||||
}
|
||||
}
|
||||
|
||||
pub fn get_next_no_error(&mut self, vec: &Sender<Box<SyntaxError>>) -> (Token, Range) {
|
||||
pub fn get_next_no_error(&mut self, vec: &mut Vec<Box<SyntaxError>>) -> (Token, Range) {
|
||||
loop {
|
||||
let (token, span) = self.lex_token();
|
||||
match token {
|
||||
Token::Error(x) => {
|
||||
let _ = vec.send(x);
|
||||
vec.push(x);
|
||||
continue;
|
||||
}
|
||||
Token::Comment(false, _) => continue,
|
||||
|
@ -2,7 +2,7 @@ use std::{iter::Peekable, str::Chars};
|
||||
|
||||
use kind_span::{Pos, Range, SyntaxCtxIndex};
|
||||
|
||||
use crate::{errors::SyntaxError, lexer::tokens::Token};
|
||||
use crate::{lexer::tokens::Token};
|
||||
|
||||
/// The lexer state.
|
||||
pub struct Lexer<'a> {
|
||||
@ -13,7 +13,6 @@ pub struct Lexer<'a> {
|
||||
|
||||
// Modes
|
||||
pub comment_depth: u16,
|
||||
pub errs: Vec<Box<SyntaxError>>,
|
||||
pub emit_comment: bool,
|
||||
}
|
||||
|
||||
@ -25,7 +24,6 @@ impl<'a> Lexer<'a> {
|
||||
ctx,
|
||||
peekable,
|
||||
comment_depth: 0,
|
||||
errs: Vec::new(),
|
||||
emit_comment: false,
|
||||
}
|
||||
}
|
||||
|
@ -18,7 +18,8 @@ pub enum Token {
|
||||
ColonColon, // ::
|
||||
|
||||
Help(String),
|
||||
Id(String),
|
||||
LowerId(String),
|
||||
UpperId(String),
|
||||
|
||||
// Keywords
|
||||
Do,
|
||||
@ -74,8 +75,12 @@ impl Token {
|
||||
std::mem::discriminant(self) == std::mem::discriminant(&b)
|
||||
}
|
||||
|
||||
pub fn is_id(&self) -> bool {
|
||||
matches!(self, Token::Id(_))
|
||||
pub fn is_lower_id(&self) -> bool {
|
||||
matches!(self, Token::LowerId(_))
|
||||
}
|
||||
|
||||
pub fn is_upper_id(&self) -> bool {
|
||||
matches!(self, Token::UpperId(_))
|
||||
}
|
||||
|
||||
pub fn is_str(&self) -> bool {
|
||||
|
@ -7,13 +7,13 @@ use crate::state::Parser;
|
||||
|
||||
impl<'a> Parser<'a> {
|
||||
pub fn is_pat_cons(&self) -> bool {
|
||||
self.get().same_variant(Token::LPar) && self.peek(1).is_id()
|
||||
self.get().same_variant(Token::LPar) && self.peek(1).is_upper_id()
|
||||
}
|
||||
|
||||
pub fn parse_pat_constructor(&mut self) -> Result<Box<Pat>, SyntaxError> {
|
||||
let start = self.range();
|
||||
self.bump(); // '('
|
||||
let name = self.parse_id()?;
|
||||
let name = self.parse_upper_id()?;
|
||||
let mut pats = Vec::new();
|
||||
while let Some(res) = self.try_single(&|s| s.parse_pat())? {
|
||||
pats.push(res)
|
||||
@ -60,6 +60,15 @@ impl<'a> Parser<'a> {
|
||||
}))
|
||||
}
|
||||
|
||||
pub fn parse_pat_single_cons(&mut self) -> Result<Box<Pat>, SyntaxError> {
|
||||
let id = self.parse_upper_id()?;
|
||||
Ok(Box::new(Pat {
|
||||
range: id.range,
|
||||
data: PatKind::App(id, vec![]),
|
||||
}))
|
||||
}
|
||||
|
||||
|
||||
fn parse_pat_list(&mut self) -> Result<Box<Pat>, SyntaxError> {
|
||||
let range = self.range();
|
||||
self.bump(); // '['
|
||||
@ -103,8 +112,10 @@ impl<'a> Parser<'a> {
|
||||
self.parse_pat_num()
|
||||
} else if self.check_actual(Token::LPar) {
|
||||
self.parse_pat_group()
|
||||
} else if self.get().is_id() {
|
||||
} else if self.get().is_lower_id() {
|
||||
self.parse_pat_var()
|
||||
} else if self.get().is_upper_id() {
|
||||
self.parse_pat_single_cons()
|
||||
} else if self.check_actual(Token::LBrace) {
|
||||
self.parse_pat_list()
|
||||
} else {
|
||||
|
@ -1,7 +1,6 @@
|
||||
use std::collections::VecDeque;
|
||||
use std::sync::mpsc::Sender;
|
||||
|
||||
use kind_span::{Range, SyntaxCtxIndex};
|
||||
use kind_span::{Range};
|
||||
|
||||
use crate::{errors::SyntaxError, lexer::tokens::Token, Lexer};
|
||||
|
||||
@ -17,13 +16,12 @@ pub struct Parser<'a> {
|
||||
// probably the movement will not affect it so much.
|
||||
pub queue: VecDeque<(Token, Range)>,
|
||||
pub breaks: VecDeque<bool>,
|
||||
pub errs: &'a Sender<Box<SyntaxError>>,
|
||||
pub errs: &'a mut Vec<Box<SyntaxError>>,
|
||||
pub eaten: u32,
|
||||
pub ctx: SyntaxCtxIndex,
|
||||
}
|
||||
|
||||
impl<'a> Parser<'a> {
|
||||
pub fn new(mut lexer: Lexer<'a>, ctx: SyntaxCtxIndex, sender: &'a Sender<Box<SyntaxError>>) -> Parser<'a> {
|
||||
pub fn new(mut lexer: Lexer<'a>, sender: &'a mut Vec<Box<SyntaxError>>) -> Parser<'a> {
|
||||
let mut queue = VecDeque::with_capacity(3);
|
||||
let mut breaks = VecDeque::with_capacity(3);
|
||||
for _ in 0..3 {
|
||||
@ -36,7 +34,6 @@ impl<'a> Parser<'a> {
|
||||
breaks,
|
||||
errs: sender,
|
||||
eaten: 0,
|
||||
ctx,
|
||||
}
|
||||
}
|
||||
|
||||
|
@ -13,6 +13,17 @@ fn is_hidden_arg(token: &Token) -> bool {
|
||||
}
|
||||
|
||||
impl<'a> Parser<'a> {
|
||||
pub fn is_top_level_entry(&self) -> bool {
|
||||
self.get().is_upper_id() && (
|
||||
self.peek(1).same_variant(Token::Colon) // ':'
|
||||
| self.peek(1).same_variant(Token::LPar) // '('
|
||||
| self.peek(1).same_variant(Token::Less) // '<'
|
||||
| self.peek(1).same_variant(Token::Minus) // '-'
|
||||
| self.peek(1).same_variant(Token::Plus) // '+'
|
||||
)
|
||||
}
|
||||
|
||||
|
||||
pub fn complement_binding_op(&self) -> Option<Token> {
|
||||
match self.get() {
|
||||
Token::LPar => Some(Token::RPar),
|
||||
@ -53,14 +64,14 @@ impl<'a> Parser<'a> {
|
||||
pub fn parse_rule(&mut self, name: String) -> Result<Box<Rule>, SyntaxError> {
|
||||
let start = self.range();
|
||||
let ident;
|
||||
if let Token::Id(name_id) = self.get() {
|
||||
if let Token::UpperId(name_id) = self.get() {
|
||||
if *name_id == name {
|
||||
ident = self.parse_id()?;
|
||||
ident = self.parse_upper_id()?;
|
||||
} else {
|
||||
return self.fail(vec![Token::Id(name)]);
|
||||
return self.fail(vec![Token::UpperId(name)]);
|
||||
}
|
||||
} else {
|
||||
return self.fail(vec![Token::Id(name)]);
|
||||
return self.fail(vec![Token::UpperId(name)]);
|
||||
}
|
||||
let mut pats = Vec::new();
|
||||
while !self.get().same_variant(Token::Eq) && !self.get().same_variant(Token::Eof) {
|
||||
@ -79,7 +90,19 @@ impl<'a> Parser<'a> {
|
||||
|
||||
pub fn parse_entry(&mut self) -> Result<Box<Entry>, SyntaxError> {
|
||||
let start = self.range();
|
||||
let ident = self.parse_id()?;
|
||||
|
||||
if self.get().is_lower_id() {
|
||||
let ident = self.parse_id()?;
|
||||
return Err(SyntaxError::LowerCasedDefinition(ident.data.0, ident.range));
|
||||
}
|
||||
|
||||
// Just to make errors more localized
|
||||
if !self.is_top_level_entry() {
|
||||
println!("{:?} {:?}", self.get(), self.peek(1));
|
||||
self.fail(vec![])?
|
||||
}
|
||||
|
||||
let ident = self.parse_upper_id()?;
|
||||
let docs = None;
|
||||
let mut args = Vec::new();
|
||||
loop {
|
||||
@ -110,20 +133,32 @@ impl<'a> Parser<'a> {
|
||||
}))
|
||||
}
|
||||
|
||||
pub fn parse_book(&mut self) -> Result<Book, SyntaxError> {
|
||||
pub fn parse_book(&mut self) -> Book {
|
||||
let mut entrs = HashMap::new();
|
||||
let mut names = Vec::new();
|
||||
loop {
|
||||
if let Token::Eof = self.get() {
|
||||
break;
|
||||
}
|
||||
let entry = self.parse_entry()?;
|
||||
if entrs.get(&entry.name.data.0).is_none() {
|
||||
names.push(entry.name.clone());
|
||||
entrs.insert(entry.name.data.0.clone(), entry);
|
||||
while !self.get().same_variant(Token::Eof) {
|
||||
match self.parse_entry() {
|
||||
Ok(entry) => {
|
||||
if entrs.get(&entry.name.data.0).is_none() {
|
||||
names.push(entry.name.clone());
|
||||
entrs.insert(entry.name.data.0.clone(), entry);
|
||||
}
|
||||
}
|
||||
Err(err) => {
|
||||
self.errs.push(Box::new(err));
|
||||
while !self.get().same_variant(Token::Eof) && !self.is_top_level_entry() {
|
||||
self.advance();
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
self.eat_variant(Token::Eof)?;
|
||||
Ok(Book { names, entrs })
|
||||
let res = self.eat_variant(Token::Eof);
|
||||
|
||||
match res {
|
||||
Ok(_) => (),
|
||||
Err(err) => self.errs.push(Box::new(err))
|
||||
}
|
||||
|
||||
Book { names, entrs }
|
||||
}
|
||||
}
|
||||
|
@ -1,6 +1,6 @@
|
||||
use std::path::PathBuf;
|
||||
|
||||
use kind_span::{Range, SyntaxCtxIndex};
|
||||
use kind_span::Range;
|
||||
|
||||
#[derive(Debug, Clone)]
|
||||
pub enum Severity {
|
||||
@ -35,7 +35,6 @@ pub struct Marking {
|
||||
pub position: Range,
|
||||
pub color: Color,
|
||||
pub text: String,
|
||||
pub ctx: SyntaxCtxIndex,
|
||||
}
|
||||
|
||||
#[derive(Debug, Clone)]
|
||||
@ -48,9 +47,14 @@ pub struct DiagnosticFrame {
|
||||
pub positions: Vec<Marking>,
|
||||
}
|
||||
|
||||
impl DiagnosticFrame {
|
||||
pub fn to_diagnostic(self, file_name: PathBuf) -> Diagnostic {
|
||||
Diagnostic { file_name, frame: self }
|
||||
}
|
||||
}
|
||||
|
||||
#[derive(Debug, Clone)]
|
||||
pub struct Diagnostic {
|
||||
pub file_name: PathBuf,
|
||||
pub position: Range,
|
||||
pub frame: DiagnosticFrame,
|
||||
}
|
||||
|
@ -18,7 +18,7 @@ pub struct Point {
|
||||
}
|
||||
|
||||
pub trait FileCache {
|
||||
fn fetch(&mut self, ctx: SyntaxCtxIndex) -> Option<&(PathBuf, String)>;
|
||||
fn fetch(&self, ctx: SyntaxCtxIndex) -> Option<&(PathBuf, String)>;
|
||||
}
|
||||
|
||||
impl Display for Point {
|
||||
@ -30,7 +30,7 @@ impl Display for Point {
|
||||
fn group_markers(markers: &[Marking]) -> SortedMarkers {
|
||||
let mut file_group = SortedMarkers::new();
|
||||
for marker in markers {
|
||||
let group = file_group.entry(marker.ctx).or_insert_with(Vec::new);
|
||||
let group = file_group.entry(marker.position.ctx).or_insert_with(Vec::new);
|
||||
group.push(marker.clone())
|
||||
}
|
||||
for group in file_group.values_mut() {
|
||||
@ -269,7 +269,7 @@ pub fn render_tag<T: Write + Sized>(severity: &Severity, fmt: &mut T) -> std::fm
|
||||
}
|
||||
|
||||
impl Diagnostic {
|
||||
pub fn render<T: Write + Sized, C: FileCache>(&self, cache: &mut C, config: &RenderConfig, fmt: &mut T) -> std::fmt::Result {
|
||||
pub fn render<T: Write + Sized, C: FileCache>(&self, cache: &C, config: &RenderConfig, fmt: &mut T) -> std::fmt::Result {
|
||||
writeln!(fmt)?;
|
||||
|
||||
write!(fmt, " ")?;
|
||||
|
@ -96,6 +96,8 @@ pub struct Sttm {
|
||||
pub enum ExprKind {
|
||||
/// Name of a variable
|
||||
Var(Ident),
|
||||
/// Name of a function/constructor
|
||||
Data(Ident),
|
||||
/// The dependent function space (e.g. (x : Int) -> y)
|
||||
All(Option<Ident>, Box<Expr>, Box<Expr>),
|
||||
/// The dependent product space (e.g. [x : Int] -> y)
|
||||
@ -273,6 +275,7 @@ impl Display for Expr {
|
||||
Sigma(_, _, _) => write!(f, "({})", self.traverse_pi_types()),
|
||||
Lit(lit) => write!(f, "{}", lit),
|
||||
Var(name) => write!(f, "{}", name),
|
||||
Data(name) => write!(f, "{}", name),
|
||||
Lambda(binder, None, body) => write!(f, "({} => {})", binder, body),
|
||||
Lambda(binder, Some(typ), body) => write!(f, "(({} : {}) => {})", binder, typ, body),
|
||||
Pair(fst, snd) => write!(f, "($ {} {})", fst, snd),
|
||||
|
@ -1,4 +1,4 @@
|
||||
use kind_span::{Range, Span, SyntaxCtxIndex};
|
||||
use kind_span::{Range, SyntaxCtxIndex};
|
||||
|
||||
use crate::concrete::expr::*;
|
||||
use crate::symbol::*;
|
||||
@ -239,6 +239,7 @@ pub fn walk_expr<T: Visitor>(ctx: &mut T, expr: &mut Expr) {
|
||||
ctx.visit_range(&mut expr.range);
|
||||
match &mut expr.data {
|
||||
ExprKind::Var(ident) => ctx.visit_ident(ident),
|
||||
ExprKind::Data(ident) => ctx.visit_ident(ident),
|
||||
ExprKind::All(None, typ, body) => {
|
||||
ctx.visit_expr(typ);
|
||||
ctx.visit_expr(body);
|
||||
|
@ -1,6 +1,6 @@
|
||||
use std::fmt::Display;
|
||||
|
||||
use kind_span::{Range, Span, SyntaxCtxIndex};
|
||||
use kind_span::{Range, SyntaxCtxIndex};
|
||||
|
||||
// Stores the name of a variable or constructor
|
||||
#[derive(Clone, PartialEq, Eq, Hash, Debug)]
|
||||
@ -21,7 +21,7 @@ impl Ident {
|
||||
|
||||
/// Changes the syntax context of the range and of the ident
|
||||
pub fn set_ctx(&self, ctx: SyntaxCtxIndex) -> Ident {
|
||||
let mut range = self.range;
|
||||
let range = self.range;
|
||||
range.set_ctx(ctx);
|
||||
Ident {
|
||||
data: self.data.clone(),
|
||||
|
Loading…
Reference in New Issue
Block a user