Functions — github.com/ammkrn/nanoda

CodeHub MCPcopy Create free account

hub / github.com/ammkrn/nanoda / functions

Functions297 in github.com/ammkrn/nanoda

⨍ Functions 297◇ Types & classes 39

↓ 51 callersMethodpush

src/utils.rs:174

↓ 39 callersMethodas_ref

↓ 38 callersMethodconcat

(self, other : impl Into<Doc>)

src/pretty/components.rs:239

↓ 32 callersMethodfold_apps

Note for non-rust users, IntoIterator is idempotent over Iterators; if we pass this something that's already an interator, nothing happens. But if we

src/expr.rs:468

↓ 29 callersMethodinstantiate

Similar shape to abstract; we traverse an expression, but this time we want to substitute variables for other expressions, stil carrying a cache and u

src/expr.rs:344

↓ 26 callersMethodget

(&self, e : &Expr, offset : usize)

src/expr.rs:732

↓ 25 callersMethodparens

(&self, new_priority : usize)

src/pretty/components.rs:294

↓ 21 callersMethodas_ref

src/expr.rs:693

↓ 19 callersMethodgroup

src/pretty/components.rs:136

↓ 18 callersMethodas_ref

src/pretty/components.rs:88

↓ 17 callersMethodconcat_plus

(self, rhs : impl Into<Doc>)

src/pretty/components.rs:248

↓ 17 callersMethodpp_expr

(&self, e : &Expr)

src/pretty/pretty_printer.rs:341

↓ 16 callersFunctionmk_const

A constant; represents a reference to a declaration that has already been added to the environment.

src/expr.rs:140

↓ 16 callersMethodswap_ty

(&self, other : Expr)

↓ 14 callersMethodas_ref

src/level.rs:321

↓ 14 callersMethodinsert

(&mut self, e1 : Expr, e2 : Expr, offset : usize)

src/expr.rs:738

↓ 13 callersMethodget_expr

(&mut self, ws : &mut SplitWhitespace)

src/parser.rs:185

↓ 13 callersFunctionmk_local

A `Local` represents a free variable. All `Local` terms have a unique identifier (here we just use a monotonically increasing counter, with each local

src/expr.rs:181

↓ 13 callersMethodvar_bound

src/expr.rs:213

↓ 12 callersMethodfold_pis

Given a list of Local expressions [L_1, L_2, ... L_n] and a body `E : Expr`, use your favorite method (fold_right is nice) and the Pi constructor to m

src/expr.rs:547

↓ 11 callersMethodas_local

↓ 11 callersMethodconcat_line

(self, other : impl Into<Doc>)

src/pretty/components.rs:243

↓ 11 callersMethodhas_locals

src/expr.rs:205

↓ 11 callersMethodinfer

Main dispatch point for type inference. Attempts to return early by checking a cache of previously inferred terms. Some of the methods are fairly long

↓ 10 callersMethodget_name

(&mut self, ws : &mut SplitWhitespace)

src/parser.rs:174

↓ 10 callersFunctionmk_app

Makes a node in the tree, joining two expressions as application.

src/expr.rs:124

↓ 10 callersMethodnest

(&self, doc : Doc)

src/pretty/pretty_printer.rs:38

↓ 9 callersMethodget_digest

src/expr.rs:201

↓ 9 callersMethodmk_arrow

This is the primitive joining of applying two expressions with the arrow constructor. Given some `e1` and `e2`, constructs `e1 → e2` by turning it int

src/expr.rs:263

↓ 9 callersFunctionmk_param

(n : impl Into<Name>)

src/level.rs:50

↓ 9 callersFunctionmk_sort

Represents a Sort/Level/Universe. You can read more about these in sources like Theorem Proving in Lean.

src/expr.rs:133

↓ 9 callersMethodpp_name

(&self, n : &Name)

src/pretty/pretty_printer.rs:43

↓ 9 callersMethodsimplify

Brief simplification procedure mostly aimed at simplifying IMax terms (the rule about an IMax with a right hand side of Zero becoming Zero is enforced

src/level.rs:95

↓ 8 callersMethodextend_str

Extend some hierarchical name with a string. IE `nat` => `nat.rec`

↓ 8 callersMethodinfer_universe_of_type

(&mut self, term : &Expr)

↓ 8 callersMethodmap_tc

(&self, f : impl FnOnce(&mut TypeChecker) -> T)

src/inductive.rs:100

↓ 8 callersFunctionmk_imax_refs

(lhs : &Level, rhs : &Level)

src/level.rs:46

↓ 8 callersFunctionmk_max

(lhs : Level, rhs : Level)

src/level.rs:38

↓ 7 callersMethodabstract_

The goal here is to traverse an expression, replacing `Local` terms with `Var` terms where possible, while caching terms we've already performed subst

src/expr.rs:282

↓ 7 callersFunctionmk_lambda

A lambda function.

src/expr.rs:148

↓ 7 callersFunctionmk_pi

A Pi (dependent function) type.

src/expr.rs:157

↓ 7 callersFunctionmk_zero

src/level.rs:34

↓ 7 callersMethodunfold_apps_refs

From an already constructed tree, unfold all consecutive `App` constructors along their spine from right to left. ```pseudo `App` nodes, and the botto

src/expr.rs:492

↓ 7 callersMethodwhnf

Outward facing function/entry point for reduction to weak head normal form. Checks cache for a previous result, calling whnf_core on a cache miss.

↓ 7 callersFunctionword_wrap_val

(s : impl Iterator<Item = Doc>)

src/pretty/components.rs:255

↓ 6 callersMethodget_level

(&mut self, ws : &mut SplitWhitespace)

src/parser.rs:180

↓ 6 callersMethodlc_binding

!! Partial function !!

src/expr.rs:218

↓ 6 callersFunctionmk_succ

src/level.rs:54

↓ 6 callersMethodparse_usize

(&mut self, ws : &mut SplitWhitespace)

src/parser.rs:125

↓ 6 callersMethodpop

src/utils.rs:180

↓ 5 callersMethodcheck_def_eq

Main entry point for checking definitional equality of two terms, which dispatches out into a number of different functions. 1. `check_def_eq_core` do

↓ 5 callersMethoddef_eq

(&mut self, a : &Expr, b : &Expr)

↓ 5 callersFunctionfind_true_else_false

I'll fix these at some point; at the moment we're (very) fast and loose with the parsing, and parsing fails silently.

↓ 5 callersMethodget_cache

src/expr.rs:639

↓ 5 callersMethodget_univ_params

src/inductive.rs:117

↓ 5 callersMethodinsert_declaration

(&mut self, d : Declaration)

↓ 4 callersMethodhas_vars

src/expr.rs:209

↓ 4 callersMethodinstantiate_lvl

Given a `Level` `L`, and a mapping of `Level::Param |-> Level` `M`, traverse `L` and execute : for each node `n` in `L` if `n` is a Param, and `M` con

src/level.rs:115

↓ 4 callersMethodis_forall

src/pretty/pretty_printer.rs:540

↓ 4 callersMethodis_proof

(&mut self, p: &Expr)

↓ 4 callersMethodis_zero

There is no level strictly less than Zero, so for any level `L`, if `L` is less than or equal to Zero, it must be that L is equal to Zero. ```pseudo `

src/level.rs:263

↓ 4 callersMethodleq_core

Essentially just a big analysis of different cases to determine (in the presence of variables and IMax's weirdness) whether the left hand side is less

src/level.rs:178

↓ 4 callersFunctionloop_check

Same as above. Constantly poll for new work, with Left(Compiled) indicating an item to be checked, `None` meaning 'try again later' and Right(..) mean

src/main.rs:198

↓ 4 callersFunctionmk_anon

↓ 4 callersFunctionmk_imax

(lhs : Level, rhs : Level)

src/level.rs:42

↓ 4 callersFunctionmk_let

A let binding, IE `let (x : nat) := 5 in 2 * x`

src/expr.rs:166

↓ 4 callersFunctionmk_prop

special constructor for an Expr::Sort that corresponds to `Prop`

src/expr.rs:111

↓ 4 callersFunctionmk_var

Makes a variable expression which contains a [De Brujin index](https://en.wikipedia.org/wiki/De_Bruijn_index).

src/expr.rs:118

↓ 4 callersMethodref_anon

src/parser.rs:67

↓ 4 callersMethodshould_check

↓ 4 callersMethodstyle

src/pretty/pretty_printer.rs:548

↓ 4 callersFunctiontake_while_slice

(s : &[T], f : impl Fn(&T) -> bool)

src/pretty/pretty_printer.rs:576

↓ 4 callersMethodtelescope

(&self, head : Option<Doc>, binders : &[ParsedBinder])

src/pretty/pretty_printer.rs:149

↓ 4 callersMethodty

src/pretty/pretty_printer.rs:552

↓ 3 callersMethodcheck_def_eq_core

(&mut self, e1_0 : &Expr, e2_0 : &Expr)

↓ 3 callersMethodcheck_type

(&mut self, e : &Expr, ty : &Expr)

↓ 3 callersMethoddeclaration_check

(&self, tc : &mut TypeChecker)

↓ 3 callersFunctionexport_file_parse_err

(loc : u32, err : T)

src/errors.rs:102

↓ 3 callersMethodextend_num

Extend some hierarchical name with an integer. IE `prod` => `prod.3`

↓ 3 callersMethodget_indices

src/inductive.rs:108

↓ 3 callersMethodget_params

src/inductive.rs:104

↓ 3 callersMethodinsert_reduction_rule

(&mut self, r : ReductionRule)

↓ 3 callersMethodis_param

src/level.rs:66

↓ 3 callersMethodmake_notation

(&mut self, kind : &str, line : &str, ws : &mut SplitWhitespace)

src/parser.rs:251

↓ 3 callersMethodmk_motive_app

(&self, e : &Expr, indices : &[Expr], motive : &Expr)

src/inductive.rs:159

↓ 3 callersMethodnormalize_pis

More aggressive version of `unfold_pis`. Given some term `E`, repeats `{ apply whnf(e), then unfold_pis(e) }` until that combination fails to strip an

↓ 3 callersMethodparse_binders

(&self, e : &Expr)

src/pretty/pretty_printer.rs:487

↓ 3 callersMethodpp_binders

(&self, binders : &[ParsedBinder], inner : Parenable)

src/pretty/pretty_printer.rs:195

↓ 3 callersMethodpp_level

(&self, lvl : &Level)

src/pretty/pretty_printer.rs:47

↓ 3 callersMethodpp_levels

(&self, lvls : &Vec<Level>)

src/pretty/pretty_printer.rs:139

↓ 3 callersMethodreduce_hdtl

(&mut self, _fn : &Expr, apps : &[&Expr], flag : Option<Flag>)

↓ 3 callersMethodrender

(self, line_width : usize)

src/pretty/components.rs:185

↓ 3 callersMethodrestore_lc_names

(&self, binders : &Vec<ParsedBinder>)

src/pretty/pretty_printer.rs:365

↓ 3 callersFunctionsafe_minus_one

src/utils.rs:66

↓ 3 callersMethodunfold_apps_special

Same as unfold_apps_refs, but returns owned values instead of references and returns the vector backwards. used a couple of times in inductive, and on

src/expr.rs:506

↓ 3 callersMethodwhnf_core

(&mut self, mut e : Expr, mut _flag : Option<Flag>)

↓ 3 callersFunctionwrite_elem_strict

FIXME add command-line flag for strict/non-strict export file parsing. Strict assumes that well-formed export files will not have 'holes' when filling

src/parser.rs:327

↓ 2 callersMethodadd_only

All this does is add the (as of yet unchecked) item to the environment. We then have to come back and check it later.

↓ 2 callersMethodalready_used

(&self, n : &Name)

src/pretty/pretty_printer.rs:78

↓ 2 callersMethodapps_eq

only used in `check_def_eq_patterns`. Broken out to prevent `patterns` from getting too big/hard to read.

next →1–100 of 297, ranked by callers