1use std::borrow::Cow;
6use std::fmt::{Display, Error, Formatter};
7
8use crate::symbol::{Ident, QualifiedIdent};
9use crate::telescope::Telescope;
10
11use expr::Expr;
12use fxhash::FxHashMap;
13use kind_span::{Locatable, Range};
14use linked_hash_map::LinkedHashMap;
15
16use self::pat::Pat;
17
18pub mod expr;
19pub mod pat;
20pub mod visitor;
21
22pub use expr::*;
23
24#[derive(Clone, Debug)]
26pub enum AttributeStyle {
27 Ident(Range, Ident),
28 String(Range, String),
29 Number(Range, u64),
30 List(Range, Vec<AttributeStyle>),
31}
32
33#[derive(Clone, Debug)]
38pub struct Attribute {
39 pub name: Ident,
40 pub args: Vec<AttributeStyle>,
41 pub value: Option<AttributeStyle>,
42 pub range: Range,
43}
44
45#[derive(Clone, Debug)]
52pub struct Argument {
53 pub hidden: bool,
54 pub erased: bool,
55 pub name: Ident,
56 pub typ: Option<Box<Expr>>,
57 pub range: Range,
58}
59
60#[derive(Clone, Debug)]
64pub struct Rule {
65 pub name: QualifiedIdent,
66 pub pats: Vec<Box<Pat>>,
67 pub body: Box<Expr>,
68 pub range: Range,
69}
70
71#[derive(Clone, Debug)]
76pub struct Entry {
77 pub name: QualifiedIdent,
78 pub docs: Vec<String>,
79 pub args: Telescope<Argument>,
80 pub typ: Box<Expr>,
81 pub rules: Vec<Box<Rule>>,
82 pub range: Range,
83 pub attrs: Vec<Attribute>,
84 pub generated_by: Option<String>,
85}
86
87#[derive(Clone, Debug)]
90pub struct Constructor {
91 pub name: Ident,
92 pub docs: Vec<String>,
93 pub attrs: Vec<Attribute>,
94 pub args: Telescope<Argument>,
95 pub typ: Option<Box<Expr>>,
96}
97
98#[derive(Clone, Debug)]
101pub struct SumTypeDecl {
102 pub name: QualifiedIdent,
103 pub docs: Vec<String>,
104 pub parameters: Telescope<Argument>,
105 pub indices: Telescope<Argument>,
106 pub constructors: Vec<Constructor>,
107 pub attrs: Vec<Attribute>,
108}
109
110#[derive(Clone, Debug)]
112pub struct RecordDecl {
113 pub name: QualifiedIdent,
114 pub docs: Vec<String>,
115 pub parameters: Telescope<Argument>,
116 pub constructor: Ident,
117 pub fields: Vec<(Ident, Vec<String>, Box<Expr>)>,
118 pub attrs: Vec<Attribute>,
119 pub cons_attrs: Vec<Attribute>,
120}
121
122impl RecordDecl {
123 pub fn get_constructor(&self) -> Constructor {
124 Constructor {
125 name: self.constructor.clone(),
126 docs: vec![],
127 attrs: self.cons_attrs.clone(),
128 args: self.fields_to_arguments(),
129 typ: None,
130 }
131 }
132}
133
134#[derive(Clone, Debug)]
136pub enum TopLevel {
137 SumType(SumTypeDecl),
138 RecordType(RecordDecl),
139 Entry(Entry),
140}
141
142impl TopLevel {
143 pub fn get_constructors(&self) -> Option<Cow<Vec<Constructor>>> {
144 match self {
145 TopLevel::SumType(sum) => Some(Cow::Borrowed(&sum.constructors)),
146 TopLevel::RecordType(rec) => Some(Cow::Owned(vec![rec.get_constructor()])),
147 TopLevel::Entry(_) => None,
148 }
149 }
150
151 pub fn get_indices(&self) -> Option<Cow<Telescope<Argument>>> {
152 match self {
153 TopLevel::SumType(sum) => Some(Cow::Borrowed(&sum.indices)),
154 TopLevel::RecordType(_) => Some(Cow::Owned(Default::default())),
155 TopLevel::Entry(_) => None,
156 }
157 }
158
159 pub fn is_record(&self) -> bool {
160 matches!(self, TopLevel::RecordType(_))
161 }
162
163 pub fn is_sum_type(&self) -> bool {
164 matches!(self, TopLevel::SumType(_))
165 }
166
167 pub fn is_definition(&self) -> bool {
168 matches!(self, TopLevel::Entry(_))
169 }
170}
171
172#[derive(Clone, Debug)]
176pub struct Module {
177 pub entries: Vec<TopLevel>,
178 pub uses: FxHashMap<String, String>,
179}
180
181#[derive(Debug, Clone)]
186pub struct EntryMeta {
187 pub hiddens: usize,
188 pub erased: usize,
189 pub arguments: Telescope<Argument>,
190 pub is_ctr: bool,
191 pub range: Range,
192 pub is_record_cons_of: Option<QualifiedIdent>,
193}
194
195#[derive(Clone, Debug, Default)]
198pub struct Book {
199 pub names: LinkedHashMap<String, QualifiedIdent>,
201
202 pub entries: FxHashMap<String, TopLevel>,
204
205 pub meta: FxHashMap<String, EntryMeta>,
207}
208
209impl Book {
210 pub fn get_count_garanteed(&self, name: &str) -> &EntryMeta {
211 self.meta
212 .get(name)
213 .unwrap_or_else(|| panic!("Internal Error: Garanteed count {:?} failed", name))
214 }
215
216 pub fn get_entry_garanteed(&self, name: &str) -> &TopLevel {
217 self.entries
218 .get(name)
219 .unwrap_or_else(|| panic!("Internal Error: Garanteed entry {:?} failed", name))
220 }
221}
222
223impl Display for Constructor {
226 fn fmt(&self, f: &mut Formatter<'_>) -> Result<(), Error> {
227 for doc in &self.docs {
228 writeln!(f, " /// {}", doc)?;
229 }
230 write!(f, "{}", self.name)?;
231 for arg in self.args.iter() {
232 write!(f, " {}", arg)?;
233 }
234 if let Some(res) = &self.typ {
235 write!(f, " : {}", res)?;
236 }
237 Ok(())
238 }
239}
240
241impl Display for TopLevel {
242 fn fmt(&self, f: &mut Formatter<'_>) -> std::fmt::Result {
243 match self {
244 TopLevel::SumType(sum) => {
245 for doc in &sum.docs {
246 writeln!(f, "/// {}", doc)?;
247 }
248 for attr in &sum.attrs {
249 writeln!(f, "{}", attr)?;
250 }
251 write!(f, "type {}", sum.name)?;
252 for arg in sum.parameters.iter() {
253 write!(f, " {}", arg)?;
254 }
255 if !sum.indices.is_empty() {
256 write!(f, " ~")?;
257 }
258 for arg in sum.indices.iter() {
259 write!(f, " {}", arg)?;
260 }
261 writeln!(f, " {{")?;
262 for cons in &sum.constructors {
263 writeln!(f, " {}", cons)?;
264 }
265 writeln!(f, "}}\n")
266 }
267 TopLevel::RecordType(rec) => {
268 for doc in &rec.docs {
269 writeln!(f, "/// {}", doc)?;
270 }
271 for attr in &rec.attrs {
272 writeln!(f, "{}", attr)?;
273 }
274 write!(f, "record {}", rec.name)?;
275 for arg in rec.parameters.iter() {
276 write!(f, " {}", arg)?;
277 }
278 writeln!(f, " {{")?;
279 writeln!(f, " constructor {}", rec.constructor.to_str())?;
280 for (name, docs, cons) in &rec.fields {
281 for doc in docs {
282 writeln!(f, " /// {}", doc)?;
283 }
284 writeln!(f, " {} : {} ", name, cons)?;
285 }
286 writeln!(f, "}}\n")
287 }
288 TopLevel::Entry(entr) => writeln!(f, "{}", entr),
289 }
290 }
291}
292
293impl Display for Module {
294 fn fmt(&self, f: &mut Formatter<'_>) -> Result<(), Error> {
295 for entr in &self.entries {
296 write!(f, "{}", entr)?;
297 }
298 Ok(())
299 }
300}
301
302impl Display for Book {
303 fn fmt(&self, f: &mut Formatter<'_>) -> Result<(), Error> {
304 for entr in self.entries.values() {
305 write!(f, "{}", entr)?
306 }
307 Ok(())
308 }
309}
310
311impl Display for Argument {
312 fn fmt(&self, f: &mut Formatter<'_>) -> Result<(), Error> {
313 let (open, close) = match (self.erased, self.hidden) {
314 (false, false) => ("(", ")"),
315 (false, true) => ("+<", ">"),
316 (true, false) => ("-(", ")"),
317 (true, true) => ("<", ">"),
318 };
319 match &self.typ {
320 Some(typ) => write!(f, "{}{}: {}{}", open, self.name, typ, close),
321 None => write!(f, "{}{}{}", open, self.name, close),
322 }
323 }
324}
325
326impl Display for Entry {
327 fn fmt(&self, f: &mut Formatter<'_>) -> Result<(), Error> {
328 for doc in &self.docs {
329 writeln!(f, "/// {}", doc)?;
330 }
331
332 for attr in &self.attrs {
333 writeln!(f, "{}", attr)?;
334 }
335
336 write!(f, "{}", self.name.clone())?;
337
338 for arg in self.args.iter() {
339 write!(f, " {}", arg)?;
340 }
341
342 writeln!(f, " : {}", &self.typ)?;
343
344 for rule in &self.rules {
345 writeln!(f, "{}", rule)?
346 }
347
348 Ok(())
349 }
350}
351
352impl Display for AttributeStyle {
353 fn fmt(&self, f: &mut Formatter<'_>) -> Result<(), Error> {
354 match self {
355 AttributeStyle::Ident(_, i) => write!(f, "{}", i),
356 AttributeStyle::String(_, s) => write!(f, "{:?}", s),
357 AttributeStyle::Number(_, n) => write!(f, "{}", n),
358 AttributeStyle::List(_, l) => write!(
359 f,
360 "[{}]",
361 l.iter()
362 .map(|x| format!("{}", x))
363 .collect::<Vec<String>>()
364 .join(", ")
365 ),
366 }
367 }
368}
369
370impl Display for Attribute {
371 fn fmt(&self, f: &mut Formatter<'_>) -> Result<(), Error> {
372 write!(f, "#{}", self.name)?;
373 if !self.args.is_empty() {
374 write!(f, "[")?;
375 write!(f, "{}", self.args[0])?;
376 for arg in self.args[1..].iter() {
377 write!(f, ", {}", arg)?;
378 }
379 write!(f, "]")?;
380 }
381 if let Some(res) = &self.value {
382 write!(f, " = {}", res)?;
383 }
384 Ok(())
385 }
386}
387
388impl Display for Rule {
389 fn fmt(&self, f: &mut Formatter<'_>) -> Result<(), Error> {
390 write!(f, "{}", self.name)?;
391 for pat in &self.pats {
392 write!(f, " {}", pat)?;
393 }
394 write!(f, " = {}", self.body)
395 }
396}
397
398impl Locatable for AttributeStyle {
399 fn locate(&self) -> Range {
400 match self {
401 AttributeStyle::Ident(r, _) => *r,
402 AttributeStyle::String(r, _) => *r,
403 AttributeStyle::Number(r, _) => *r,
404 AttributeStyle::List(r, _) => *r,
405 }
406 }
407}
408
409impl Telescope<Argument> {
410 pub fn count_implicits(&self) -> (usize, usize) {
411 let mut hiddens = 0;
412 let mut erased = 0;
413 for arg in self.iter() {
414 if arg.hidden {
415 hiddens += 1;
416 }
417 if arg.erased {
418 erased += 1;
419 }
420 }
421 (hiddens, erased)
422 }
423}
424
425impl SumTypeDecl {
426 pub fn extract_book_info(&self) -> EntryMeta {
427 let mut arguments = Telescope::default();
428 let mut hiddens = 0;
429 let mut erased = 0;
430
431 let (hiddens_, erased_) = self.parameters.count_implicits();
432 hiddens += hiddens_;
433 erased += erased_;
434
435 arguments = arguments.extend(&self.parameters);
436
437 let (hiddens_, erased_) = self.indices.count_implicits();
438 hiddens += hiddens_;
439 erased += erased_;
440
441 arguments = arguments.extend(&self.indices);
442
443 EntryMeta {
444 hiddens,
445 erased,
446 arguments,
447 is_ctr: true,
448 range: self.name.range,
449 is_record_cons_of: None,
450 }
451 }
452}
453
454impl Constructor {
455 pub fn extract_book_info(&self, def: &SumTypeDecl) -> EntryMeta {
456 let mut arguments = Telescope::default();
457 let mut hiddens = 0;
458 let mut erased = 0;
459
460 hiddens += def.parameters.len();
461 erased += def.parameters.len();
462
463 arguments = arguments.extend(&def.parameters.map(|x| x.to_implicit()));
464
465 if self.typ.is_none() {
468 hiddens += def.indices.len();
469 erased += def.indices.len();
470 arguments = arguments.extend(&def.indices.map(|x| x.to_implicit()));
471 }
472
473 for arg in self.args.iter() {
474 if arg.erased {
475 erased += 1;
476 }
477 if arg.hidden {
478 hiddens += 1;
479 }
480 }
481
482 arguments = arguments.extend(&self.args.clone());
483
484 EntryMeta {
485 hiddens,
486 erased,
487 arguments,
488 is_ctr: true,
489 range: self.name.range,
490 is_record_cons_of: None,
491 }
492 }
493}
494
495impl RecordDecl {
496 pub fn fields_to_arguments(&self) -> Telescope<Argument> {
497 Telescope::new(
498 self.fields
499 .iter()
500 .map(|(name, _docs, typ)| {
501 Argument::new_explicit(
502 name.clone(),
503 typ.clone(),
504 name.locate().mix(typ.locate()),
505 )
506 })
507 .collect(),
508 )
509 }
510
511 pub fn extract_book_info(&self) -> EntryMeta {
512 let mut arguments = Telescope::default();
513 let mut hiddens = 0;
514 let mut erased = 0;
515
516 let (hiddens_, erased_) = self.parameters.count_implicits();
517 hiddens += hiddens_;
518 erased += erased_;
519
520 arguments = arguments.extend(&self.parameters);
521
522 EntryMeta {
523 hiddens,
524 erased,
525 arguments,
526 is_ctr: true,
527 range: self.name.range,
528 is_record_cons_of: None,
529 }
530 }
531
532 pub fn extract_book_info_of_constructor(&self) -> EntryMeta {
533 let mut arguments;
534 let mut hiddens = 0;
535 let mut erased = 0;
536
537 hiddens += self.parameters.len();
538 erased += self.parameters.len();
539 arguments = self.parameters.map(|x| x.to_implicit());
540
541 let field_args: Vec<Argument> = self
542 .fields
543 .iter()
544 .map(|(name, _docs, typ)| {
545 Argument::new_explicit(name.clone(), typ.clone(), name.locate().mix(typ.locate()))
546 })
547 .collect();
548
549 arguments = arguments.extend(&Telescope::new(field_args));
550
551 EntryMeta {
552 hiddens,
553 erased,
554 arguments,
555 is_ctr: true,
556 range: self.name.range,
557 is_record_cons_of: Some(self.name.clone()),
558 }
559 }
560}
561
562impl Entry {
563 pub fn extract_book_info(&self) -> EntryMeta {
564 let mut arguments = Telescope::default();
565 let mut hiddens = 0;
566 let mut erased = 0;
567
568 let (hiddens_, erased_) = self.args.count_implicits();
569 hiddens += hiddens_;
570 erased += erased_;
571
572 arguments = arguments.extend(&self.args);
573
574 EntryMeta {
575 hiddens,
576 erased,
577 arguments,
578 is_ctr: self.rules.is_empty(),
579 range: self.name.range,
580 is_record_cons_of: None,
581 }
582 }
583}
584
585impl Argument {
586 pub fn new_explicit(name: Ident, typ: Box<Expr>, range: Range) -> Argument {
587 Argument {
588 hidden: false,
589 erased: false,
590 name,
591 typ: Some(typ),
592 range,
593 }
594 }
595
596 pub fn to_implicit(&self) -> Argument {
597 Argument {
598 hidden: true,
599 erased: true,
600 name: self.name.clone(),
601 typ: self.typ.clone(),
602 range: self.range,
603 }
604 }
605}