malk_core/
lib.rs

1use std::rc::Rc;
2use std::ops;
3use std::collections::HashMap;
4use std::cmp::Ordering::*;
5
6use TermKind::*;
7
8pub struct Intrinsic {
9    pub arg_type: Term,
10    pub ret_type: Term,
11    pub func: fn(&Term) -> Term,
12}
13
14pub struct World {
15    intrinsics: HashMap<String, Intrinsic>,
16}
17
18/// A pointer to a term.
19#[derive(Debug, Clone, PartialEq)]
20pub struct Term(Rc<TermKind>);
21
22impl ops::Deref for Term {
23    type Target = TermKind;
24
25    fn deref(&self) -> &TermKind {
26        let Term(ref rc_term) = *self;
27        &**rc_term
28    }
29}
30
31impl Term {
32    /// Create a new term.
33    fn new(kind: TermKind) -> Term {
34        Term(Rc::new(kind))
35    }
36}
37
38/// The different kinds of term that can appear in the AST.
39#[derive(Debug, Clone, PartialEq)]
40pub enum TermKind {
41    /// The type of all types, and levels, which does not itself have a type.
42    Omega,
43
44
45    /// The type of universe levels.
46    Level,
47
48    /// Universe level zero.
49    LevelZero,
50
51    /// Universe level (pred + 1).
52    LevelSucc {
53        pred: Term,
54    },
55
56    /// Universe level max(a, b)
57    LevelMax {
58        a: Term,
59        b: Term,
60    },
61
62
63    /// The type of types, indexed by levels.
64    Type {
65        level: Term,
66    },
67
68    /// A variable.
69    Var(usize),
70
71    /// The type of functions. (ie pi types)
72    FuncType {
73        arg_type: Term,
74        res_type: Term,
75    },
76
77    /// Functions.
78    FuncTerm {
79        body: Term,
80    },
81
82    /// Function application.
83    FuncApp {
84        func: Term,
85        arg: Term,
86        arg_type: Term,
87        res_type: Term,
88    },
89
90    /// The unit type.
91    UnitType,
92
93    /// The unit term.
94    UnitTerm,
95
96    /// A dependent pair type (ie. sigma type)
97    PairType {
98        head_type: Term,
99        tail_type: Term,
100    },
101
102    /// A pair term.
103    PairTerm {
104        head: Term,
105        tail: Term,
106    },
107
108    /// Dependent pair elimination.
109    PairElim {
110        pair: Term,
111        res: Term,
112        head_type: Term,
113        tail_type: Term,
114    },
115
116    /// The canonical empty type, (ie. bottom).
117    NeverType,
118
119    /// Never type elimintator
120    NeverElim {
121        never: Term,
122    },
123
124    /// Disjoint union, sum type.
125    EitherType {
126        left_type: Term,
127        right_type: Term,
128    },
129
130    /// Inject left.
131    EitherLeft {
132        val: Term,
133    },
134
135    /// Inject right.
136    EitherRight {
137        val: Term,
138    },
139
140    /// Case match on a sum type.
141    EitherElim {
142        arg: Term,
143        arg_type: Term,
144        res_type: Term,
145        on_left: Term,
146        on_right: Term,
147    },
148
149    /// The type of identifications (a == b)
150    IdentType {
151        term_type: Term,
152        a: Term,
153        b: Term,
154    },
155
156    /// Reflexivity,
157    IdentTerm,
158
159    /// J-elimination for identities.
160    IdentElim {
161        term_type: Term,
162        a: Term,
163        b: Term,
164        path: Term,
165        context: Term,
166        proof: Term,
167    },
168
169    /// A recursive type. `rec_type` is under a context where Var(0) refers back to the type.
170    RecType {
171        rec_type: Term,
172    },
173
174    /// A recursive term. Used to mark `rec_term` as a member of a recursive type.
175    RecTerm {
176        rec_term: Term,
177    },
178
179    /*
180    /// Recursive elimintation. Fold over the term `arg` of recursive type `arg_type`.
181    RecElim {
182        arg: Term,
183        res: Term,
184        arg_type: Term,
185        res_type: Term,
186    }
187    */
188
189    /// The type for interacting with the outside world through intrinsics.
190    WorldType,
191
192    /// The term used to represent a fully-normalised world ready to perform IO on.
193    WorldTerm,
194
195    /// Performs an intrinsic call.
196    WorldElim {
197        /// The name of the intrinsic
198        intrinsic: &'static str,
199
200        /// The world argument.
201        world_in: Term,
202
203        /// The argument type that the intrinsic expects.
204        arg: Term,
205
206        /// The result of the expression. Evaluated with the intrinsic result at Var(1) and another
207        /// World at Var(0).
208        expr: Term,
209    },
210
211    /// Unsigned, memory-sized integers.
212    UmType,
213
214    /// An intger literal.
215    UmTerm {
216        val: u64,
217    },
218
219    /// An integer literal equal to `1 + pred`
220    UmSucc {
221        pred: Term,
222    },
223
224    /// Case match on a Um.
225    UmElim {
226        arg: Term,
227        res_type: Term,
228        on_zero: Term,
229        on_succ: Term,
230    },
231}
232
233/// Normalise a term assuming all it's subterms are already normalised. Does beta/eta reduction on
234/// the head of the term.
235pub fn reduce_head(term: &Term, world: &World) -> Term {
236    match **term {
237        Omega |
238        Level |
239        LevelZero |
240        LevelSucc { .. } |
241        FuncType { .. } |
242        Var(..) |
243        UnitType |
244        UnitTerm |
245        IdentType { .. } |
246        IdentTerm |
247        RecType { .. } |
248        RecTerm { .. } |
249        PairType { .. } |
250        NeverType |
251        NeverElim { .. } |
252        EitherType { .. } |
253        EitherLeft { .. } |
254        EitherRight { .. } |
255        WorldType |
256        WorldTerm |
257        UmType |
258        UmTerm { .. } |
259        Type { .. } => term.clone(),
260
261        LevelMax { ref a, ref b } => {
262            match (&**a, &**b) {
263                (&LevelZero, _) => b.clone(),
264                (_, &LevelZero) => a.clone(),
265                (&LevelSucc { pred: ref a_pred }, &LevelSucc { pred: ref b_pred }) => {
266                    let max = Term::new(LevelMax {
267                        a: a_pred.clone(),
268                        b: b_pred.clone(),
269                    });
270                    let max = reduce_head(&max, world);
271                    Term::new(LevelSucc { pred: max })
272                },
273                _ => term.clone(),
274            }
275        },
276
277        FuncTerm { ref body } => {
278            match **body {
279                FuncApp { ref func, ref arg, .. } => {
280                    match **arg {
281                        Var(0) => func.clone(),
282                        _ => term.clone(),
283                    }
284                },
285                _ => term.clone(),
286            }
287        },
288
289        FuncApp { ref func, ref arg, .. } => {
290            match **func {
291                FuncTerm { ref body } => {
292                    let res = substitute(body, arg, 0);
293                    normalise(&res, world)
294                },
295                _ => term.clone(),
296            }
297        },
298
299        PairTerm { ref head, ref tail } => {
300            match (&**head, &**tail) {
301                (&PairElim { pair: ref head_pair, res: ref head_res, .. },
302                 &PairElim { pair: ref tail_pair, res: ref tail_res, .. }) => {
303                    match (&**head_res, &**tail_res) {
304                        (&Var(1), &Var(0)) => {
305                            match **head_pair == **tail_pair {
306                                true => head_pair.clone(),
307                                false => term.clone(),
308                            }
309                        },
310                        _ => term.clone(),
311                    }
312                },
313                _ => term.clone(),
314            }
315        },
316
317        PairElim { ref pair, ref res, .. } => {
318            match **pair {
319                PairTerm { ref head, ref tail } => {
320                    let res = substitute(res, tail, 0);
321                    let res = substitute(&res, head, 0);
322                    normalise(&res, world)
323                },
324                _ => term.clone(),
325            }
326        },
327
328        EitherElim { ref arg, ref on_left, ref on_right, .. } => {
329            match **arg {
330                EitherLeft { ref val } => {
331                    let res = substitute(on_left, val, 0);
332                    normalise(&res, world)
333                },
334                EitherRight { ref val } => {
335                    let res = substitute(on_right, val, 0);
336                    normalise(&res, world)
337                },
338                _ => term.clone(),
339            }
340        },
341
342        IdentElim { ref a, ref path, ref proof, .. } => {
343            match **path {
344                IdentTerm => {
345                    let res = substitute(proof, a, 0);
346                    normalise(&res, world)
347                },
348                _ => term.clone(),
349            }
350        },
351
352        /*
353        RecElim { ref arg, ref res, ref arg_type, .. } => {
354            match (**arg, **arg_type) => {
355                (RecTerm { ref rec_term }, RecType { ref rec_type }) => {
356                    let folded = recurse(rec_term, rec_type, arg_type, res, 0);
357                    substitute(res, folded, 0)
358                },
359                _ => term.clone(),
360            }
361        },
362        */
363
364        WorldElim { intrinsic, ref world_in, ref arg, ref expr } => {
365            match **world_in {
366                WorldTerm => {
367                    match world.intrinsics.get(intrinsic) {
368                        None => term.clone(),
369                        Some(intrinsic) => {
370                            let ret = (intrinsic.func)(arg);
371                            let res = substitute(expr, &Term::new(WorldTerm), 0);
372                            let res = substitute(&res, &ret, 0);
373                            normalise(&res, world)
374                        },
375                    }
376                },
377                _ => term.clone(),
378            }
379        },
380
381        UmSucc { ref pred } => {
382            match **pred {
383                UmTerm { val } => {
384                    Term::new(UmTerm { val: val + 1 })
385                },
386                _ => term.clone(),
387            }
388        },
389
390        UmElim { ref arg, ref on_zero, ref on_succ, .. } => {
391            match **arg {
392                UmTerm { val: 0 } => {
393                    on_zero.clone()
394                },
395                UmTerm { val } => {
396                    let res = substitute(on_succ, &Term::new(UmTerm { val: val - 1 }), 0);
397                    normalise(&res, world)
398                },
399                UmSucc { ref pred } => {
400                    let res = substitute(on_succ, &pred, 0);
401                    normalise(&res, world)
402                },
403                _ => term.clone(),
404            }
405        },
406    }
407}
408
409/*
410pub fn recurse(rec_term: &Term, rec_type: &Term, w_type: &Term, res: &Term, depth: usize) -> Term {
411    match (**rec_type, **rec_term) {
412        (FuncType { ref arg_type, ref res_type }, FuncTerm { ref body }) => {
413            
414        },
415    }
416}
417*/
418
419/// Normalise a term.
420pub fn normalise(term: &Term, world: &World) -> Term {
421    match **term {
422        Omega |
423        Var(..) |
424        Level |
425        UnitType |
426        UnitTerm |
427        IdentTerm |
428        NeverType |
429        WorldType |
430        WorldTerm |
431        UmType |
432        UmTerm { .. } |
433        LevelZero => term.clone(),
434
435        LevelSucc { ref pred } => {
436            Term::new(LevelSucc {
437                pred: normalise(pred, world),
438            })
439        },
440
441        LevelMax { ref a, ref b } => {
442            let max = Term::new(LevelMax {
443                a: normalise(a, world),
444                b: normalise(b, world),
445            });
446            reduce_head(&max, world)
447        },
448
449        Type { ref level } => {
450            Term::new(Type {
451                level: normalise(level, world),
452            })
453        },
454
455        FuncType { ref arg_type, ref res_type } => {
456            Term::new(FuncType {
457                arg_type: normalise(arg_type, world),
458                res_type: normalise(res_type, world),
459            })
460        },
461
462        FuncTerm { ref body } => {
463            let func_term = Term::new(FuncTerm {
464                body: normalise(body, world),
465            });
466            reduce_head(&func_term, world)
467        },
468
469        FuncApp { ref func, ref arg, ref arg_type, ref res_type } => {
470            let func_app = Term::new(FuncApp {
471                func: normalise(func, world),
472                arg: normalise(arg, world),
473                arg_type: normalise(arg_type, world),
474                res_type: normalise(res_type, world),
475            });
476            reduce_head(&func_app, world)
477        },
478
479        PairType { ref head_type, ref tail_type } => {
480            Term::new(PairType {
481                head_type: normalise(head_type, world),
482                tail_type: normalise(tail_type, world),
483            })
484        },
485
486        PairTerm { ref head, ref tail } => {
487            let pair_term = Term::new(PairTerm {
488                head: normalise(head, world),
489                tail: normalise(tail, world),
490            });
491            reduce_head(&pair_term, world)
492        },
493
494        PairElim { ref pair, ref res, ref head_type, ref tail_type } => {
495            let pair_elim = Term::new(PairElim {
496                pair: normalise(pair, world),
497                res: normalise(res, world),
498                head_type: normalise(head_type, world),
499                tail_type: normalise(tail_type, world),
500            });
501            reduce_head(&pair_elim, world)
502        },
503
504        NeverElim { ref never } => {
505            Term::new(NeverElim {
506                never: normalise(never, world),
507            })
508        },
509
510        EitherType { ref left_type, ref right_type } => {
511            Term::new(EitherType {
512                left_type: normalise(left_type, world),
513                right_type: normalise(right_type, world),
514            })
515        },
516
517        EitherLeft { ref val } => {
518            Term::new(EitherLeft {
519                val: normalise(val, world),
520            })
521        },
522
523        EitherRight { ref val } => {
524            Term::new(EitherRight {
525                val: normalise(val, world),
526            })
527        },
528
529        EitherElim { ref arg, ref arg_type, ref res_type, ref on_left, ref on_right } => {
530            let arg = normalise(arg, world);
531            let arg_type = normalise(arg_type, world);
532            let res_type = normalise(res_type, world);
533            let on_left = normalise(on_left, world);
534            let on_right = normalise(on_right, world);
535            let either_elim = Term::new(EitherElim {
536                arg: arg,
537                arg_type: arg_type,
538                res_type: res_type,
539                on_left: on_left,
540                on_right: on_right,
541            });
542            reduce_head(&either_elim, world)
543        },
544
545        IdentType { ref term_type, ref a, ref b } => {
546            Term::new(IdentType {
547                term_type: normalise(term_type, world),
548                a: normalise(a, world),
549                b: normalise(b, world),
550            })
551        },
552
553        IdentElim { ref term_type, ref a, ref b, ref path, ref context, ref proof } => {
554            let term_type = normalise(term_type, world);
555            let a = normalise(a, world);
556            let b = normalise(b, world);
557            let path = normalise(path, world);
558            let context = normalise(context, world);
559            let proof = normalise(proof, world);
560            let ident_elim = Term::new(IdentElim {
561                term_type: term_type,
562                a: a,
563                b: b,
564                path: path,
565                context: context,
566                proof: proof,
567            });
568            reduce_head(&ident_elim, world)
569        },
570
571        RecType { ref rec_type } => {
572            Term::new(RecType {
573                rec_type: normalise(rec_type, world),
574            })
575        },
576
577        RecTerm { ref rec_term } => {
578            Term::new(RecTerm {
579                rec_term: normalise(rec_term, world),
580            })
581        },
582
583        WorldElim { intrinsic, ref world_in, ref arg, ref expr } => {
584            let world_in = normalise(world_in, world);
585            let arg = normalise(arg, world);
586            let expr = normalise(expr, world);
587            let world_elim = Term::new(WorldElim {
588                intrinsic: intrinsic,
589                world_in: world_in,
590                arg: arg,
591                expr: expr,
592            });
593            reduce_head(&world_elim, world)
594        },
595
596        UmSucc { ref pred } => {
597            let pred = normalise(pred, world);
598            let um_succ = Term::new(UmSucc {
599                pred: pred,
600            });
601            reduce_head(&um_succ, world)
602        },
603
604        UmElim { ref arg, ref res_type, ref on_zero, ref on_succ } => {
605            let arg = normalise(arg, world);
606            let res_type = normalise(res_type, world);
607            let on_zero = normalise(on_zero, world);
608            let on_succ = normalise(on_succ, world);
609            let um_elim = Term::new(UmElim {
610                arg: arg,
611                res_type: res_type,
612                on_zero: on_zero,
613                on_succ: on_succ,
614            });
615            reduce_head(&um_elim, world)
616        },
617    }
618}
619
620/// substitute `sub` for the variable at `index`.
621pub fn substitute(term: &Term, sub: &Term, index: usize) -> Term {
622    match **term {
623        Omega |
624        Level |
625        LevelZero |
626        UnitType |
627        UnitTerm |
628        NeverType |
629        WorldType |
630        WorldTerm |
631        UmType |
632        UmTerm { .. } |
633        IdentTerm => term.clone(),
634
635        LevelSucc { ref pred } => {
636            Term::new(LevelSucc {
637                pred: substitute(pred, sub, index)
638            })
639        },
640
641        LevelMax { ref a, ref b } => {
642            Term::new(LevelMax {
643                a: substitute(a, sub, index),
644                b: substitute(b, sub, index),
645            })
646        },
647
648        Type { ref level } => {
649            Term::new(Type {
650                level: substitute(level, sub, index),
651            })
652        },
653
654        Var(i) => {
655            match i.cmp(&index) {
656                Less => term.clone(),
657                Equal => sub.clone(),
658                Greater => Term::new(Var(i - 1)),
659            }
660        },
661
662        FuncType { ref arg_type, ref res_type } => {
663            let arg_type = substitute(arg_type, sub, index);
664            let sub = bump_index(sub, 1, 0);
665            let res_type = substitute(res_type, &sub, index + 1);
666            Term::new(FuncType {
667                arg_type: arg_type,
668                res_type: res_type,
669            })
670        },
671
672        FuncTerm { ref body } => {
673            let sub = bump_index(sub, 1, 0);
674            Term::new(FuncTerm {
675                body: substitute(body, &sub, index + 1),
676            })
677        },
678
679        FuncApp { ref func, ref arg, ref arg_type, ref res_type } => {
680            let func = substitute(func, sub, index);
681            let arg = substitute(arg, sub, index);
682            let arg_type = substitute(arg_type, sub, index);
683            let sub = bump_index(sub, 1, 0);
684            let res_type = substitute(res_type, &sub, index + 1);
685            Term::new(FuncApp {
686                func: func,
687                arg: arg,
688                arg_type: arg_type,
689                res_type: res_type,
690            })
691        },
692
693        PairType { ref head_type, ref tail_type } => {
694            let head_type = substitute(head_type, sub, index);
695            let new_sub = bump_index(sub, 1, 0);
696            let tail_type = substitute(tail_type, &new_sub, index + 1);
697            Term::new(PairType {
698                head_type: head_type,
699                tail_type: tail_type,
700            })
701        },
702
703        PairTerm { ref head, ref tail } => {
704            Term::new(PairTerm {
705                head: substitute(head, sub, index),
706                tail: substitute(tail, sub, index),
707            })
708        },
709
710        PairElim { ref pair, ref res, ref head_type, ref tail_type } => {
711            let pair = substitute(pair, sub, index);
712            let head_type = substitute(head_type, sub, index);
713            let new_sub = bump_index(sub, 1, 0);
714            let tail_type = substitute(tail_type, &new_sub, index + 1);
715            let new_sub = bump_index(sub, 2, 0);
716            let res = substitute(res, &new_sub, index + 2);
717            Term::new(PairElim {
718                pair: pair,
719                res: res,
720                head_type: head_type,
721                tail_type: tail_type,
722            })
723        },
724
725        NeverElim { ref never } => {
726            Term::new(NeverElim {
727                never: substitute(never, sub, index),
728            })
729        },
730
731        EitherType { ref left_type, ref right_type } => {
732            Term::new(EitherType {
733                left_type: substitute(left_type, sub, index),
734                right_type: substitute(right_type, sub, index),
735            })
736        },
737
738        EitherLeft { ref val } => {
739            Term::new(EitherLeft {
740                val: substitute(val, sub, index),
741            })
742        },
743
744        EitherRight { ref val } => {
745            Term::new(EitherRight {
746                val: substitute(val, sub, index),
747            })
748        },
749
750        EitherElim { ref arg, ref arg_type, ref res_type, ref on_left, ref on_right } => {
751            let arg = substitute(arg, sub, index);
752            let arg_type = substitute(arg_type, sub, index);
753            let new_sub = bump_index(sub, 1, 0);
754            let res_type = substitute(res_type, &new_sub, index + 1);
755            let on_left = substitute(on_left, &new_sub, index + 1);
756            let on_right = substitute(on_right, &new_sub, index + 1);
757            Term::new(EitherElim {
758                arg: arg,
759                arg_type: arg_type,
760                res_type: res_type,
761                on_left: on_left,
762                on_right: on_right,
763            })
764        },
765
766        IdentType { ref term_type, ref a, ref b } => {
767            Term::new(IdentType {
768                term_type: substitute(term_type, sub, index),
769                a: substitute(a, sub, index),
770                b: substitute(b, sub, index),
771            })
772        },
773
774        IdentElim { ref term_type, ref a, ref b, ref path, ref context, ref proof } => {
775            let term_type = substitute(term_type, sub, index);
776            let a = substitute(a, sub, index);
777            let b = substitute(b, sub, index);
778            let path = substitute(path, sub, index);
779            let new_sub = bump_index(sub, 3, 0);
780            let context = substitute(context, &new_sub, index + 3);
781            let new_sub = bump_index(sub, 1, 0);
782            let proof = substitute(proof, &new_sub, index + 1);
783            Term::new(IdentElim {
784                term_type: term_type,
785                a: a,
786                b: b,
787                path: path,
788                context: context,
789                proof: proof,
790            })
791        },
792
793        RecType { ref rec_type } => {
794            let new_sub = bump_index(sub, 1, 0);
795            Term::new(RecType {
796                rec_type: substitute(rec_type, &new_sub, index + 1),
797            })
798        },
799
800        RecTerm { ref rec_term } => {
801            Term::new(RecTerm {
802                rec_term: substitute(rec_term, sub, index),
803            })
804        },
805
806        WorldElim { intrinsic, ref world_in, ref arg, ref expr } => {
807            let world_in = substitute(world_in, sub, index);
808            let arg = substitute(arg, sub, index);
809            let new_sub = bump_index(sub, 2, 0);
810            let expr = substitute(expr, &new_sub, index + 2);
811            Term::new(WorldElim {
812                intrinsic: intrinsic,
813                world_in: world_in,
814                arg: arg,
815                expr: expr,
816            })
817        },
818
819        UmSucc { ref pred } => {
820            Term::new(UmSucc {
821                pred: substitute(pred, sub, index)
822            })
823        },
824
825        UmElim { ref arg, ref res_type, ref on_zero, ref on_succ } => {
826            let arg = substitute(arg, sub, index);
827            let new_sub = bump_index(sub, 1, 0);
828            let res_type = substitute(res_type, &new_sub, index + 1);
829            let on_zero = substitute(on_zero, sub, index);
830            let on_succ = substitute(on_succ, &new_sub, index + 1);
831            Term::new(UmElim {
832                arg: arg,
833                res_type: res_type,
834                on_zero: on_zero,
835                on_succ: on_succ,
836            })
837        },
838    }
839}
840
841/// Bump all the index of the variables in a term by `amount`, ignoring variables whose index is
842/// less than `cutoff`. This is hygenic when it recurses into subcontexts (ie. cutoff is adjusted
843/// appropriately).
844///
845/// # Example
846/// ```ignore
847/// bump_index(`(Var(0), Var(1), Var(2))`, 1, 100) => `(Var(0), Var(101), Var(102))`
848/// bump_index(`(Var(0), FuncTerm(Var(0))))`, 0, 100) => `(Var(100), FuncTerm(Var(0)))`
849/// ```
850pub fn bump_index(term: &Term, amount: usize, cutoff: usize) -> Term {
851    match **term {
852        Omega |
853        Level |
854        LevelZero |
855        UnitType |
856        UnitTerm |
857        NeverType |
858        WorldType |
859        WorldTerm |
860        UmType |
861        UmTerm { .. } |
862        IdentTerm => term.clone(),
863
864        LevelSucc { ref pred } => {
865            Term::new(LevelSucc {
866                pred: bump_index(pred, amount, cutoff),
867            })
868        },
869
870        LevelMax { ref a, ref b } => {
871            Term::new(LevelMax {
872                a: bump_index(a, amount, cutoff),
873                b: bump_index(b, amount, cutoff),
874            })
875        },
876
877        Type { ref level } => {
878            Term::new(Type {
879                level: bump_index(level, amount, cutoff),
880            })
881        },
882
883        Var(i) => {
884            match i < cutoff {
885                true => term.clone(),
886                false => Term::new(Var(i + amount)),
887            }
888        },
889
890        FuncType { ref arg_type, ref res_type } => {
891            Term::new(FuncType {
892                arg_type: bump_index(arg_type, amount, cutoff),
893                res_type: bump_index(res_type, amount, cutoff + 1),
894            })
895        },
896
897        FuncTerm { ref body } => {
898            Term::new(FuncTerm {
899                body: bump_index(body, amount, cutoff + 1),
900            })
901        },
902
903        FuncApp { ref func, ref arg, ref arg_type, ref res_type } => {
904            Term::new(FuncApp {
905                func: bump_index(func, amount, cutoff),
906                arg: bump_index(arg, amount, cutoff),
907                arg_type: bump_index(arg_type, amount, cutoff),
908                res_type: bump_index(res_type, amount, cutoff + 1),
909            })
910        },
911
912        PairType { ref head_type, ref tail_type } => {
913            Term::new(PairType {
914                head_type: bump_index(head_type, amount, cutoff),
915                tail_type: bump_index(tail_type, amount, cutoff + 1),
916            })
917        },
918
919        PairTerm { ref head, ref tail } => {
920            Term::new(PairTerm {
921                head: bump_index(head, amount, cutoff),
922                tail: bump_index(tail, amount, cutoff),
923            })
924        },
925
926        PairElim { ref pair, ref res, ref head_type, ref tail_type } => {
927            Term::new(PairElim {
928                pair: bump_index(pair, amount, cutoff),
929                res: bump_index(res, amount, cutoff + 2),
930                head_type: bump_index(head_type, amount, cutoff),
931                tail_type: bump_index(tail_type, amount, cutoff + 1),
932            })
933        },
934
935        NeverElim { ref never } => {
936            Term::new(NeverElim {
937                never: bump_index(never, amount, cutoff),
938            })
939        },
940
941        EitherType { ref left_type, ref right_type } => {
942            Term::new(EitherType {
943                left_type: bump_index(left_type, amount, cutoff),
944                right_type: bump_index(right_type, amount, cutoff),
945            })
946        },
947
948        EitherLeft { ref val } => {
949            Term::new(EitherLeft {
950                val: bump_index(val, amount, cutoff),
951            })
952        },
953
954        EitherRight { ref val } => {
955            Term::new(EitherRight {
956                val: bump_index(val, amount, cutoff),
957            })
958        },
959
960        EitherElim { ref arg, ref arg_type, ref res_type, ref on_left, ref on_right } => {
961            Term::new(EitherElim {
962                arg: bump_index(arg, amount, cutoff),
963                arg_type: bump_index(arg_type, amount, cutoff),
964                res_type: bump_index(res_type, amount, cutoff + 1),
965                on_left: bump_index(on_left, amount, cutoff + 1),
966                on_right: bump_index(on_right, amount, cutoff + 1),
967            })
968        },
969
970        IdentType { ref term_type, ref a, ref b } => {
971            Term::new(IdentType {
972                term_type: bump_index(term_type, amount, cutoff),
973                a: bump_index(a, amount, cutoff),
974                b: bump_index(b, amount, cutoff),
975            })
976        },
977
978        IdentElim { ref term_type, ref a, ref b, ref path, ref context, ref proof } => {
979            Term::new(IdentElim {
980                term_type: bump_index(term_type, amount, cutoff),
981                a: bump_index(a, amount, cutoff),
982                b: bump_index(b, amount, cutoff),
983                path: bump_index(path, amount, cutoff),
984                context: bump_index(context, amount, cutoff + 3),
985                proof: bump_index(proof, amount, cutoff + 1),
986            })
987        }
988
989        RecType { ref rec_type } => {
990            Term::new(RecType {
991                rec_type: bump_index(rec_type, amount, cutoff + 1),
992            })
993        },
994
995        RecTerm { ref rec_term } => {
996            Term::new(RecTerm {
997                rec_term: bump_index(rec_term, amount, cutoff),
998            })
999        },
1000
1001        WorldElim { intrinsic, ref world_in, ref arg, ref expr } => {
1002            Term::new(WorldElim {
1003                intrinsic: intrinsic,
1004                world_in: bump_index(world_in, amount, cutoff),
1005                arg: bump_index(arg, amount, cutoff),
1006                expr: bump_index(expr, amount, cutoff + 2),
1007            })
1008        },
1009
1010        UmSucc { ref pred } => {
1011            Term::new(UmSucc {
1012                pred: bump_index(pred, amount, cutoff),
1013            })
1014        },
1015
1016        UmElim { ref arg, ref res_type, ref on_zero, ref on_succ } => {
1017            Term::new(UmElim {
1018                arg: bump_index(arg, amount, cutoff),
1019                res_type: bump_index(res_type, amount, cutoff + 1),
1020                on_zero: bump_index(on_zero, amount, cutoff),
1021                on_succ: bump_index(on_succ, amount, cutoff + 1),
1022            })
1023        }
1024    }
1025}
1026
malk_core/lib.rs

malk_core/
lib.rs
