nar 0.0.8

Narc, a dependently-typed programming language with dependent pattern matching
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55

use voile_util::loc::{Loc, ToLoc};

pub use self::{ast::*, ast_fold::*, ast_util::*, decl::*, decl_impl::*, pretty::*};

/// Core language syntax definitions.
mod ast;
/// Ast traversal functions.
///
/// I don't think these functions should be used much, though.
/// We should use pattern matching instead.
mod ast_fold;
/// Constructor functions & utility functions.
///
/// To avoid too much `Box::new` invocations.
mod ast_util;
/// Checked declarations.
mod decl;
/// Declarations' trivial trait implementations.
mod decl_impl;
/// Pretty printing things.
mod pretty;
/// Substitution is a mapping.
pub mod subst;

impl Term {
    pub fn at(self, loc: Loc) -> TermInfo {
        TermInfo::new(self, loc)
    }
}

/// A value with syntax info.
/// This is what should be stored inside of the context.
#[derive(Debug, PartialEq, Eq, Clone)]
pub struct TermInfo {
    pub ast: Term,
    pub loc: Loc,
}

impl TermInfo {
    pub fn new(ast: Term, loc: Loc) -> Self {
        Self { ast, loc }
    }

    pub fn map_ast(self, f: impl FnOnce(Term) -> Term) -> Self {
        Self::new(f(self.ast), self.loc)
    }
}

/// Telescopes.
pub type Tele = Vec<Bind>;
pub type TeleS = [Bind];
pub type LetList = Vec<Let>;

/// Contexts.
pub type Ctx = Vec<Term>;