1use self::tags::EvalTag;
6use self::tags::{operator_to_constructor, TermTag};
7
8use hvm::syntax::Term;
9use kind_span::Range;
10use kind_tree::desugared::{self, Book, Expr};
11use kind_tree::symbol::{Ident, QualifiedIdent};
12
13use hvm::{syntax as lang, u60};
14
15mod tags;
16
17macro_rules! vec_preppend {
18 ($($f:expr),*; $e:expr) => {
19 vec![[$($f),*].as_slice(), $e.as_slice()].concat()
20 };
21}
22
23fn eval_ctr(quote: bool, head: TermTag) -> String {
25 if quote {
26 head.to_string()
27 } else {
28 match head {
29 TermTag::Binary => EvalTag::Op.to_string(),
30 TermTag::Let => EvalTag::Let.to_string(),
31 TermTag::Ann => EvalTag::Ann.to_string(),
32 TermTag::Sub => EvalTag::Sub.to_string(),
33 TermTag::App => EvalTag::App.to_string(),
34 other => other.to_string(),
35 }
36 }
37}
38
39fn lift_spine(spine: Vec<Box<Term>>) -> Vec<Box<Term>> {
44 if spine.len() > 16 {
45 let mut start = spine[..2].to_vec();
46 start.push(Box::new(Term::Ctr {
47 name: format!("Apps.Kind.Term.args{}", spine.len() - 2),
48 args: spine[2..].to_vec(),
49 }));
50 start
51 } else {
52 spine
53 }
54}
55
56fn mk_lifted_ctr(head: String, spine: Vec<Box<Term>>) -> Box<Term> {
57 let args = lift_spine(spine);
58 Box::new(Term::Ctr { name: head, args })
59}
60
61fn mk_ctr(name: String, args: Vec<Box<Term>>) -> Box<Term> {
62 Box::new(lang::Term::Ctr { name, args })
63}
64
65fn mk_var(ident: &str) -> Box<Term> {
66 Box::new(Term::Var {
67 name: ident.to_string(),
68 })
69}
70
71fn mk_u60(numb: u64) -> Box<Term> {
72 Box::new(Term::U6O {
73 numb: u60::new(numb),
74 })
75}
76
77fn mk_single_ctr(head: String) -> Box<Term> {
78 Box::new(Term::Ctr {
79 name: head,
80 args: vec![],
81 })
82}
83
84fn mk_ctr_name(ident: &QualifiedIdent) -> Box<Term> {
85 mk_single_ctr(format!("{}.", ident))
86}
87
88fn mk_ctr_name_from_str(ident: &str) -> Box<Term> {
89 mk_single_ctr(format!("{}.", ident))
90}
91
92fn range_to_num(lhs: bool, range: Range) -> Box<Term> {
93 if lhs {
94 mk_var("orig")
95 } else {
96 Box::new(Term::U6O {
97 numb: u60::new(range.encode().0),
98 })
99 }
100}
101
102fn set_origin(ident: &Ident) -> Box<Term> {
103 mk_lifted_ctr(
104 "Apps.Kind.Term.set_origin".to_owned(),
105 vec![range_to_num(false, ident.range), mk_var(ident.to_str())],
106 )
107}
108
109fn lam(name: &Ident, body: Box<Term>) -> Box<Term> {
110 Box::new(Term::Lam {
111 name: name.to_string(),
112 body,
113 })
114}
115
116fn desugar_str(input: &str, range: Range) -> Box<desugared::Expr> {
117 let nil = QualifiedIdent::new_static("Data.String.nil", None, range);
118 let cons = QualifiedIdent::new_static("Data.String.cons", None, range);
119 input
120 .chars()
121 .rfold(desugared::Expr::ctr(range, nil, vec![]), |right, chr| {
122 desugared::Expr::ctr(
123 range,
124 cons.clone(),
125 vec![desugared::Expr::num_u60(range, chr as u64), right],
126 )
127 })
128}
129
130fn codegen_str(input: &str) -> Box<Term> {
133 input.chars().rfold(
134 Box::new(Term::Ctr {
135 name: "Data.String.nil".to_string(),
136 args: vec![],
137 }),
138 |right, chr| {
139 Box::new(Term::Ctr {
140 name: "Data.String.cons".to_string(),
141 args: vec![mk_u60(chr as u64), right],
142 })
143 },
144 )
145}
146
147fn codegen_all_expr(
148 lhs_rule: bool,
149 lhs: bool,
150 num: &mut usize,
151 quote: bool,
152 expr: &Expr,
153) -> Box<Term> {
154 use kind_tree::desugared::ExprKind::*;
155 match &expr.data {
156 Typ => mk_lifted_ctr(
157 eval_ctr(quote, TermTag::Typ),
158 vec![range_to_num(lhs, expr.range)],
159 ),
160 NumTypeU60 => mk_lifted_ctr(
161 eval_ctr(quote, TermTag::U60),
162 vec![range_to_num(lhs, expr.range)],
163 ),
164 NumTypeF60 => todo!(),
165 Var { name } => {
166 if quote && !lhs {
167 set_origin(name)
168 } else if lhs_rule {
169 *num += 1;
170 mk_lifted_ctr(
171 eval_ctr(quote, TermTag::Var),
172 vec![
173 range_to_num(lhs, expr.range),
174 mk_u60(name.encode()),
175 mk_u60((*num - 1) as u64),
176 ],
177 )
178 } else {
179 mk_var(name.to_str())
180 }
181 }
182 All {
183 param,
184 typ,
185 body,
186 erased: _,
187 } => mk_lifted_ctr(
188 eval_ctr(quote, TermTag::All),
189 vec![
190 range_to_num(lhs, expr.range),
191 mk_u60(param.encode()),
192 codegen_all_expr(lhs_rule, lhs, num, quote, typ),
193 lam(param, codegen_all_expr(lhs_rule, lhs, num, quote, body)),
194 ],
195 ),
196 Lambda {
197 param,
198 body,
199 erased: _,
200 } => mk_lifted_ctr(
201 eval_ctr(quote, TermTag::Lambda),
202 vec![
203 range_to_num(lhs, expr.range),
204 mk_u60(param.encode()),
205 lam(param, codegen_all_expr(lhs_rule, lhs, num, quote, body)),
206 ],
207 ),
208 App { fun, args } => args.iter().fold(
209 codegen_all_expr(lhs_rule, lhs, num, quote, fun),
210 |left, right| {
211 mk_lifted_ctr(
212 eval_ctr(quote, TermTag::App),
213 vec![
214 range_to_num(lhs, expr.range),
215 left,
216 codegen_all_expr(lhs_rule, lhs, num, quote, &right.data),
217 ],
218 )
219 },
220 ),
221 Ctr { name, args } => mk_lifted_ctr(
222 eval_ctr(quote, TermTag::Ctr(args.len())),
223 vec_preppend![
224 mk_ctr_name(name),
225 range_to_num(lhs, expr.range);
226 args.iter().cloned().map(|x| codegen_all_expr(lhs_rule, lhs, num, quote, &x)).collect::<Vec<Box<Term>>>()
227 ],
228 ),
229 Fun { name, args } => {
230 let new_spine: Vec<Box<Term>> = args
231 .iter()
232 .cloned()
233 .map(|x| codegen_all_expr(lhs_rule, lhs, num, quote, &x))
234 .collect();
235 if quote {
236 mk_lifted_ctr(
237 eval_ctr(quote, TermTag::Fun(new_spine.len())),
238 vec_preppend![
239 mk_ctr_name(name),
240 range_to_num(lhs, expr.range);
241 new_spine
242 ],
243 )
244 } else {
245 mk_ctr(
246 TermTag::HoasF(name.to_string()).to_string(),
247 vec_preppend![
248 range_to_num(lhs, expr.range);
249 new_spine
250 ],
251 )
252 }
253 }
254 Let { name, val, next } => mk_ctr(
255 eval_ctr(quote, TermTag::Let),
256 vec![
257 range_to_num(lhs, expr.range),
258 mk_u60(name.encode()),
259 codegen_all_expr(lhs_rule, lhs, num, quote, val),
260 lam(name, codegen_all_expr(lhs_rule, lhs, num, quote, next)),
261 ],
262 ),
263 Ann { expr, typ } => mk_ctr(
264 eval_ctr(quote, TermTag::Ann),
265 vec![
266 range_to_num(lhs, expr.range),
267 codegen_all_expr(lhs_rule, lhs, num, quote, expr),
268 codegen_all_expr(lhs_rule, lhs, num, quote, typ),
269 ],
270 ),
271 Sub {
272 name,
273 indx,
274 redx,
275 expr,
276 } => mk_ctr(
277 eval_ctr(quote, TermTag::Sub),
278 vec![
279 range_to_num(lhs, expr.range),
280 mk_u60(name.encode()),
281 mk_u60(*indx as u64),
282 mk_u60(*redx as u64),
283 codegen_all_expr(lhs_rule, lhs, num, quote, expr),
284 ],
285 ),
286 NumU60 { numb } => mk_lifted_ctr(
287 eval_ctr(quote, TermTag::NUMU60),
288 vec![range_to_num(lhs, expr.range), mk_u60(*numb)],
289 ),
290 NumF60 { numb: _ } => todo!(),
291 Binary { op, left, right } => mk_lifted_ctr(
292 eval_ctr(quote, TermTag::Binary),
293 vec![
294 range_to_num(lhs, expr.range),
295 mk_single_ctr(operator_to_constructor(*op).to_owned()),
296 codegen_all_expr(lhs_rule, lhs, num, quote, left),
297 codegen_all_expr(lhs_rule, lhs, num, quote, right),
298 ],
299 ),
300 Hole { num } => mk_lifted_ctr(
301 eval_ctr(quote, TermTag::Hole),
302 vec![range_to_num(lhs, expr.range), mk_u60(*num)],
303 ),
304 Str { val } => codegen_all_expr(lhs_rule, lhs, num, quote, &desugar_str(val, expr.range)),
305 Hlp(_) => mk_lifted_ctr(
306 eval_ctr(quote, TermTag::Hlp),
307 vec![range_to_num(lhs, expr.range)],
308 ),
309 Err => panic!("Internal Error: Was not expecting an ERR node inside the HVM checker"),
310 }
311}
312
313fn codegen_expr(quote: bool, expr: &Expr) -> Box<Term> {
314 codegen_all_expr(false, false, &mut 0, quote, expr)
315}
316
317fn codegen_pattern(args: &mut usize, quote: bool, expr: &Expr) -> Box<Term> {
318 codegen_all_expr(false, true, args, quote, expr)
319}
320
321fn codegen_type(args: &[desugared::Argument], typ: &desugared::Expr) -> Box<lang::Term> {
322 if !args.is_empty() {
323 let arg = &args[0];
324 mk_lifted_ctr(
325 eval_ctr(true, TermTag::All),
326 vec![
327 range_to_num(false, arg.range),
328 mk_u60(arg.name.encode()),
329 codegen_expr(true, &arg.typ),
330 lam(&arg.name, codegen_type(&args[1..], typ)),
331 ],
332 )
333 } else {
334 codegen_expr(true, typ)
335 }
336}
337
338fn codegen_vec<T>(exprs: T) -> Box<Term>
339where
340 T: DoubleEndedIterator<Item = Box<Term>>,
341{
342 exprs.rfold(mk_ctr("Data.List.nil".to_string(), vec![]), |left, right| {
343 mk_ctr("Data.List.cons".to_string(), vec![right, left])
344 })
345}
346
347fn codegen_rule_end(file: &mut lang::File, rule: &desugared::Rule) {
348 let base_vars = (0..rule.pats.len())
349 .map(|x| mk_var(&format!("x{}", x)))
350 .collect::<Vec<Box<lang::Term>>>();
351
352 file.rules.push(lang::Rule {
353 lhs: mk_ctr(
354 TermTag::HoasQ(rule.name.to_string()).to_string(),
355 vec_preppend![
356 mk_var("orig");
357 base_vars
358 ],
359 ),
360 rhs: mk_lifted_ctr(
361 eval_ctr(false, TermTag::Fun(base_vars.len())),
362 vec_preppend![
363 mk_ctr_name(&rule.name),
364 mk_var("orig");
365 base_vars
366 ],
367 ),
368 });
369
370 file.rules.push(lang::Rule {
371 lhs: mk_ctr(
372 TermTag::HoasF(rule.name.to_string()).to_string(),
373 vec_preppend![
374 mk_var("orig");
375 base_vars
376 ],
377 ),
378 rhs: mk_lifted_ctr(
379 eval_ctr(false, TermTag::Fun(base_vars.len())),
380 vec_preppend![
381 mk_ctr_name(&rule.name),
382 mk_var("orig");
383 base_vars
384 ],
385 ),
386 });
387}
388
389fn codegen_rule(file: &mut lang::File, rule: &desugared::Rule) {
390 let mut count = 0;
391
392 let lhs_args = rule
393 .pats
394 .iter()
395 .map(|x| codegen_pattern(&mut count, false, x))
396 .collect::<Vec<Box<Term>>>();
397
398 file.rules.push(lang::Rule {
399 lhs: mk_ctr(
400 TermTag::HoasQ(rule.name.to_string()).to_string(),
401 vec_preppend![
402 mk_var("orig");
403 lhs_args
404 ],
405 ),
406 rhs: codegen_expr(true, &rule.body),
407 });
408
409 if rule.name.to_string().as_str() == "Apps.HVM.log" {
410 file.rules.push(lang::Rule {
411 lhs: mk_ctr(
412 TermTag::HoasF(rule.name.to_string()).to_string(),
413 vec![
414 mk_var("orig"),
415 mk_var("a"),
416 mk_var("r"),
417 mk_var("log"),
418 mk_var("ret"),
419 ],
420 ),
421 rhs: mk_ctr(
422 "Apps.HVM.print".to_owned(),
423 vec![
424 mk_ctr("Apps.Kind.Term.show".to_owned(), vec![mk_var("log")]),
425 mk_var("ret"),
426 ],
427 ),
428 });
429 } else {
430 file.rules.push(lang::Rule {
431 lhs: mk_ctr(
432 TermTag::HoasF(rule.name.to_string()).to_string(),
433 vec_preppend![
434 mk_var("orig");
435 lhs_args
436 ],
437 ),
438 rhs: codegen_expr(false, &rule.body),
439 });
440 }
441}
442
443fn codegen_entry_rules(
444 count: &mut usize,
445 index: usize,
446 args: &mut Vec<Box<Term>>,
447 entry: &desugared::Rule,
448 pats: &[Box<desugared::Expr>],
449) -> Box<Term> {
450 if pats.is_empty() {
451 mk_ctr(
452 "Apps.Kind.Rule.rhs".to_owned(),
453 vec![mk_ctr(
454 format!("QT{}", index),
455 vec_preppend![
456 mk_ctr_name(&entry.name),
457 range_to_num(false, entry.range);
458 args
459 ],
460 )],
461 )
462 } else {
463 let pat = &pats[0];
464 let expr = codegen_all_expr(true, false, count, false, pat);
465 args.push(expr.clone());
466 mk_ctr(
467 "Apps.Kind.Rule.lhs".to_owned(),
468 vec![
469 expr,
470 codegen_entry_rules(count, index + 1, args, entry, &pats[1..]),
471 ],
472 )
473 }
474}
475
476fn codegen_entry(file: &mut lang::File, entry: &desugared::Entry) {
477 file.rules.push(lang::Rule {
478 lhs: mk_ctr(
479 "Apps.Kind.Axiom.NameOf".to_owned(),
480 vec![mk_ctr_name(&entry.name)],
481 ),
482 rhs: codegen_str(entry.name.to_string().as_str()),
483 });
484
485 file.rules.push(lang::Rule {
486 lhs: mk_ctr(
487 "Apps.Kind.Axiom.OrigOf".to_owned(),
488 vec![mk_ctr_name(&entry.name)],
489 ),
490 rhs: range_to_num(false, entry.name.range),
491 });
492
493 file.rules.push(lang::Rule {
494 lhs: mk_ctr(
495 "Apps.Kind.Axiom.HashOf".to_owned(),
496 vec![mk_ctr_name(&entry.name)],
497 ),
498 rhs: mk_u60(fxhash::hash64(entry.name.to_string().as_str())),
499 });
500
501 file.rules.push(lang::Rule {
502 lhs: mk_ctr(
503 "Apps.Kind.Axiom.TypeOf".to_owned(),
504 vec![mk_ctr_name(&entry.name)],
505 ),
506 rhs: codegen_type(&entry.args, &entry.typ),
507 });
508
509 let base_vars = (0..entry.args.len())
510 .map(|x| mk_var(&format!("x{}", x)))
511 .collect::<Vec<Box<lang::Term>>>();
512
513 file.rules.push(lang::Rule {
514 lhs: mk_lifted_ctr(
515 format!("Apps.Kind.Term.FN{}", entry.args.len()),
516 vec_preppend![
517 mk_ctr_name(&entry.name),
518 mk_var("orig");
519 base_vars
520 ],
521 ),
522 rhs: mk_ctr(
523 TermTag::HoasF(entry.name.to_string()).to_string(),
524 vec_preppend![
525 mk_var("orig");
526 base_vars
527 ],
528 ),
529 });
530
531 file.rules.push(lang::Rule {
532 lhs: mk_ctr(
533 format!("QT{}", entry.args.len()),
534 vec_preppend![
535 mk_ctr_name(&entry.name),
536 mk_var("orig");
537 base_vars
538 ],
539 ),
540 rhs: mk_ctr(
541 TermTag::HoasQ(entry.name.to_string()).to_string(),
542 vec_preppend![
543 mk_var("orig");
544 base_vars
545 ],
546 ),
547 });
548
549 for rule in &entry.rules {
550 codegen_rule(file, rule);
551 }
552
553 if !entry.rules.is_empty() {
554 codegen_rule_end(file, &entry.rules[0])
555 }
556
557 let rules = entry
558 .rules
559 .iter()
560 .map(|rule| codegen_entry_rules(&mut 0, 0, &mut Vec::new(), rule, &rule.pats));
561
562 file.rules.push(lang::Rule {
563 lhs: mk_ctr(
564 "Apps.Kind.Axiom.RuleOf".to_owned(),
565 vec![mk_ctr_name(&entry.name)],
566 ),
567 rhs: codegen_vec(rules),
568 });
569}
570
571pub fn codegen_coverage(file: &mut lang::File, book: &Book) {
572 for entry in book.entrs.values() {
573 if !entry.rules.is_empty() && !entry.rules[0].pats.is_empty() && !entry.attrs.partial && !entry.attrs.axiom {
574 file.rules.push(lang::Rule {
575 lhs: mk_ctr(
576 "Apps.Kind.Axiom.CoverCheck".to_owned(),
577 vec![mk_ctr_name(&entry.name)],
578 ),
579 rhs: mk_single_ctr("Data.Bool.true".to_string()),
580 });
581 }
582 }
583
584 for family in book.families.values() {
585 file.rules.push(lang::Rule {
586 lhs: mk_ctr(
587 "Apps.Kind.Axiom.Family.Constructors".to_owned(),
588 vec![mk_ctr_name(&family.name)],
589 ),
590 rhs: mk_ctr("Data.Maybe.some".to_string(), vec![codegen_vec(family.constructors.iter().map(mk_ctr_name))]),
591 });
592
593 file.rules.push(lang::Rule {
594 lhs: mk_ctr(
595 "Apps.Kind.Axiom.Family.Params".to_owned(),
596 vec![mk_ctr_name(&family.name)],
597 ),
598 rhs: mk_u60(family.parameters.len() as u64),
599 });
600
601 let type_entry = book.entrs.get(family.name.to_str()).unwrap();
602 let mut args = Vec::with_capacity(type_entry.args.len());
603
604 for arg in family.parameters.iter() {
605 args.push(mk_var(arg.name.to_str()))
606 }
607
608 for idx in 0..type_entry.args.len() - family.parameters.len() {
609 args.push(mk_var(&format!("x_{}", idx)));
610 }
611
612 for constructor in &family.constructors {
613 let entry = book.entrs.get(constructor.to_str()).unwrap();
614
615 let mut maker = mk_ctr(
616 "Apps.Kind.Coverage.Maker.End".to_string(),
617 vec![codegen_expr(
618 false,
619 &kind_tree::desugared::Expr::ctr(
620 constructor.range,
621 constructor.clone(),
622 entry
623 .args
624 .iter()
625 .map(|x| kind_tree::desugared::Expr::var(x.name.clone()))
626 .collect(),
627 ),
628 )],
629 );
630
631 for arg in entry.args[family.parameters.len()..].iter().rev() {
632 maker = mk_ctr(
633 "Apps.Kind.Coverage.Maker.Cons".to_string(),
634 vec![
635 range_to_num(false, arg.range),
636 codegen_all_expr(false, false, &mut 0, false, &arg.typ),
637 lam(&arg.name, maker),
638 ],
639 );
640 }
641
642 file.rules.push(lang::Rule {
643 lhs: mk_ctr(
644 "Apps.Kind.Coverage.Maker.Mk".to_owned(),
645 vec![
646 mk_ctr_name(constructor),
647 mk_var("orig"),
648 mk_lifted_ctr(
649 eval_ctr(true, TermTag::Ctr(args.len())),
650 vec_preppend![
651 mk_ctr_name(&family.name),
652 range_to_num(true, constructor.range);
653 args
654 ],
655 ),
656 ],
657 ),
658 rhs: mk_ctr("Data.Maybe.some".to_string(), vec![maker]),
659 });
660
661 file.rules.push(lang::Rule {
662 lhs: mk_ctr(
663 "Apps.Kind.Axiom.Compare".to_owned(),
664 vec![mk_ctr_name(constructor), mk_ctr_name(constructor)],
665 ),
666 rhs: mk_single_ctr("Data.Bool.true".to_string()),
667 });
668
669 file.rules.push(lang::Rule {
670 lhs: mk_ctr(
671 "Apps.Kind.Axiom.ArgsCount".to_owned(),
672 vec![mk_ctr_name(constructor)],
673 ),
674 rhs: mk_u60(entry.args.len() as u64),
675 });
676
677 file.rules.push(lang::Rule {
678 lhs: mk_ctr(
679 "Apps.Kind.Axiom.Compare".to_owned(),
680 vec![mk_ctr_name(constructor), mk_ctr_name(constructor)],
681 ),
682 rhs: mk_single_ctr("Data.Bool.true".to_string()),
683 });
684 }
685 }
686}
687
688pub fn codegen_book(book: &Book, check_coverage: bool, functions_to_check: Vec<String>) -> lang::File {
691 let mut file = lang::File {
692 rules: vec![],
693 smaps: vec![],
694 };
695
696 let functions_entry = lang::Rule {
697 lhs: mk_ctr("Apps.Kind.Axiom.Functions".to_owned(), vec![]),
698 rhs: codegen_vec(functions_to_check.iter().map(|x| mk_ctr_name_from_str(x))),
699 };
700
701 file.rules.push(functions_entry);
702
703 file.rules.push(lang::Rule {
704 lhs: mk_ctr("HoleInit".to_owned(), vec![]),
705 rhs: mk_u60(book.holes),
706 });
707
708 for rule in &file.rules {
709 match &*rule.lhs {
710 Term::Ctr { name, args } => {
711 file.smaps.push((name.clone(), vec![false; args.len()]));
712 }
713 _ => todo!(),
714 }
715 }
716
717 for entry in book.entrs.values() {
718 codegen_entry(&mut file, entry);
719 }
720
721 if check_coverage {
722 codegen_coverage(&mut file, book);
723 }
724
725 file.rules.push(lang::Rule {
726 lhs: mk_ctr("Apps.Kind.Axiom.CoverCheck".to_owned(), vec![mk_var("_")]),
727 rhs: mk_single_ctr("Data.Bool.false".to_string()),
728 });
729
730 if check_coverage {
731 file.rules.push(lang::Rule {
732 lhs: mk_ctr(
733 "Apps.Kind.Axiom.Compare".to_owned(),
734 vec![mk_var("a"), mk_var("b")],
735 ),
736 rhs: mk_single_ctr("Data.Bool.false".to_string()),
737 });
738
739 file.rules.push(lang::Rule {
740 lhs: mk_ctr(
741 "Apps.Kind.Coverage.Maker.Mk".to_owned(),
742 vec![mk_var("cons"), mk_var("a"), mk_var("b")],
743 ),
744 rhs: mk_single_ctr("Data.Maybe.none".to_string()),
745 });
746
747 file.rules.push(lang::Rule {
748 lhs: mk_ctr("Apps.Kind.Axiom.Family.Constructors".to_owned(), vec![mk_var("_")]),
749 rhs: mk_single_ctr("Data.Maybe.none".to_string()),
750 });
751 }
752
753 file
754}