Functions — github.com/HigherOrderCO-archive/kind2-archive

CodeHub MCPcopy Create free account

hub / github.com/HigherOrderCO-archive/kind2-archive / functions

Functions89 in github.com/HigherOrderCO-archive/kind2-archive

⨍ Functions 89 ◇ Types & classes 12

↓ 48 callersMethodparse_term

(&mut self, fid: u64, uses: &Uses)

src/term/parse.rs:74

↓ 14 callersFunctioncons

(vector: &im::Vector<A>, value: A)

src/term/mod.rs:96

↓ 14 callersFunctionshadow

Shadows a name on the uses map

src/book/mod.rs:23

↓ 8 callersMethodload

Same as load, mutably adding to a 'book'

src/book/mod.rs:62

↓ 5 callersFunctionstrip_extension

(filename: &str)

↓ 4 callersFunctionload_book

↓ 2 callersMethodas_adt

Interprets a λ-encoded Algebraic Data Type definition as an ADT struct.

src/sugar/mod.rs:389

↓ 2 callersMethoddesugar

Expands syntax sugars like Mch to proper λ-encodings.

src/term/mod.rs:359

↓ 2 callersMethodflatten_into

Helper function.

src/show/mod.rs:95

↓ 2 callersFunctiongenerate_kindc

FIXME: not necessary, already on book

↓ 2 callersMethodparse_adt

(&mut self, fid: u64, uses: &Uses)

src/sugar/mod.rs:727

↓ 2 callersMethodparse_match

MAT ::= match <name> = <term> { <name> : <term> <...> }: <term>

src/sugar/mod.rs:1026

↓ 2 callersFunctionrun_kindc

(book: &Book, cmd: &str, file: &str)

↓ 2 callersMethodwidth

Sums the width of all children ropes, up to a limit.

src/show/mod.rs:166

↓ 1 callersMethodadd_all

Wraps an All around this term.

src/book/parse.rs:228

↓ 1 callersMethodadd_alls

Wraps many Lams around this term.

src/book/parse.rs:238

↓ 1 callersMethodadd_lam

Wraps a Lam around this term.

src/book/parse.rs:159

↓ 1 callersMethodadd_lams

Wraps many lams around this term. Linearizes when possible.

src/book/parse.rs:168

↓ 1 callersMethodas_equal

Interprets as an Equality: - (((Equal _) a) b) Patterns: - (EQUAL a b) ::= (App (App (App (Var "Equal") _) a) b)

src/sugar/mod.rs:327

↓ 1 callersMethodas_list

Interprets as a list: - (((List/cons _) x) (((List/cons _) y) ... (List/nil _))) Patterns: - (CONS head tail) ::= (App (App (App (Var "List/cons") Met

src/sugar/mod.rs:242

↓ 1 callersMethodas_nat

Interprets as a Nat: - (Nat.succ (Nat.succ ... Nat.zero)) Patterns: - (SUCC pred) ::= (App (Var "Nat.succ") pred) - ZERO ::= (Var "Nat.zero")

src/sugar/mod.rs:200

↓ 1 callersFunctioncheck

↓ 1 callersMethodclean

src/term/mod.rs:252

↓ 1 callersFunctioncompile_to_js

↓ 1 callersFunctioncompile_to_kindc

↓ 1 callersMethodcount_implicits

Counts the number of implicit arguments of a term.

src/term/mod.rs:496

↓ 1 callersFunctiondeps

↓ 1 callersMethodexpand_implicits

Desugars all definitions

src/book/mod.rs:97

↓ 1 callersMethodget_file_id

Gets a file id from its name

src/book/mod.rs:110

↓ 1 callersMethodget_file_name

Gets a file name from its id (FIXME: asymptotics)

src/book/mod.rs:121

↓ 1 callersMethodget_free_vars

(&self, env: im::Vector<String>, free_vars: &mut BTreeSet<String>)

src/term/mod.rs:104

↓ 1 callersMethodhandle_unbound

Handles an unbound definition

src/book/mod.rs:57

↓ 1 callersFunctionnormal

(name: &str, _level: u32)

↓ 1 callersMethodovershadow

(&mut self, name_map: &im::HashMap<String, String>, depth: &mut u64)

src/term/mod.rs:168

↓ 1 callersMethodparse_book

Parses a whole file into a book.

src/book/parse.rs:139

↓ 1 callersMethodparse_def

Parses a top-level definition (datatype or term)

src/book/parse.rs:45

↓ 1 callersMethodparse_info

src/info/parse.rs:5

↓ 1 callersMethodparse_list

(&mut self, fid: u64, uses: &Uses)

src/sugar/mod.rs:302

↓ 1 callersMethodparse_oper

src/term/parse.rs:5

↓ 1 callersMethodparse_term_end

(&mut self, fid: u64, uses: &Uses, term: Term)

src/term/parse.rs:466

↓ 1 callersMethodparse_term_ini

(&mut self, fid: u64, uses: &Uses)

src/term/parse.rs:80

↓ 1 callersMethodparse_use

Parses a top-level use-declaration

src/book/parse.rs:6

↓ 1 callersMethodparse_uses

Parses many top-level use-declarations

src/book/parse.rs:33

↓ 1 callersMethodto_js

src/book/compile.rs:21

↓ 1 callersMethodto_js_go

src/term/compile.rs:223

↓ 1 callersMethodto_kindc

src/book/compile.rs:12

src/term/mod.rs:85

Creates a book, loading a term, its dependencies, and stdlib

src/book/mod.rs:43

Allocs a new Call with given children.

src/show/mod.rs:49

Allocs a new Dec node.

src/show/mod.rs:79

Methodexpand_implicits

Expands implicit calls, applying them to the correct number of metavars. When a variable name ends with "!", we fill erased arguments with metas.

src/term/mod.rs:423

Flattens the Show structure into a string, respecting indentation and width limits.

src/show/mod.rs:84

(&self, f: &mut std::fmt::Formatter<'_>)

src/book/show.rs:12

(&self, f: &mut std::fmt::Formatter<'_>)

src/term/show.rs:20

(&self, f: &mut std::fmt::Formatter<'_>)

src/sugar/mod.rs:291

src/term/mod.rs:77

Allocs a new Glue with given children.

src/show/mod.rs:59

Allocs a new Inc node.

src/show/mod.rs:74

Allocs a new Line node.

src/show/mod.rs:64

Loads an ADT from its λ-encoded file.

src/sugar/mod.rs:662

src/main.rs:104

Allocs a new Many node.

src/show/mod.rs:44

Creates an empty book

src/book/mod.rs:35

(fid: u64, ini: u64, end: u64)

src/term/mod.rs:69

Builds a λ-encoded Algebraic Data Type definition from an ADT struct.

src/sugar/mod.rs:519

Methodnew_equal

Builds an equal chain

src/sugar/mod.rs:346

Builds a chain of applications of List/cons and List/nil from a Vec<Box<Term>>

src/sugar/mod.rs:272

Methodnew_match

Builds a λ-encoded pattern-match.

src/sugar/mod.rs:828

Nats have a dedicated term, for type-checking efficiency

src/sugar/mod.rs:226

Checks if there is no `Line` in a vector of ropes.

src/show/mod.rs:189

Methodparse_equal

(&mut self, fid: u64, uses: &Uses)

src/sugar/mod.rs:372

Methodparse_infos

src/info/mod.rs:75

Allocs a new Pile with given children.

src/show/mod.rs:54

(&self, book: &Book)

src/info/mod.rs:39

Allocs a new Semi node.

src/show/mod.rs:69

src/book/show.rs:6

src/term/show.rs:8

src/info/show.rs:5

Allocs a new Text node from a string slice.

src/show/mod.rs:39

src/book/compile.rs:4

src/term/compile.rs:7

Methodto_hvm2_name

src/term/compile.rs:118

src/term/compile.rs:212

Methodto_js_name

src/term/compile.rs:290

(&self, env: im::Vector<String>, met: &mut usize)

src/term/compile.rs:127

Methodto_kindc_name

src/term/compile.rs:179

src/term/mod.rs:73