(index ("ident?" 0) ("ident-name" 144) ("ident-stamp" 283) ("ident-create" 409) ("ident-equal?" 547) ("ident-empty" 729) ("ident-add" 842) ("ident-find" 1010) ("path?" 1221) ("Pident" 1364) ("Pdot" 1482) ("path-equal?" 1604) ("subst-add" 1766) ("subst-path" 1922) ("subst-identity" 2053) ("make-core-syntax" 2174) ("make-mod-syntax" 3031) ("make-core-typing" 3974) ("make-mod-typing" 4859) ("st-empty" 5697) ("st-enter-value" 5773) ("st-enter-type" 5908) ("st-enter-module" 6040) ("st-value-path" 6178) ("st-type-path" 6255) ("st-module-path" 6330) ("st-scope-module" 6409) ("make-mod-eval" 6490))
(def (sig (procedure "(ident? X) -> BOOL" (id ident?))) (p "Returns " (tt "#t") " if " (tt "X") " is an identifier, " (tt "#f") " otherwise."))
(def (sig (procedure "(ident-name IDENT) -> STRING" (id ident-name))) (p "Returns the string name associated with the given identifier."))
(def (sig (procedure "(ident-stamp IDENT) -> INT" (id ident-stamp))) (p "Returns the unique stamp of the given identifier."))
(def (sig (procedure "(ident-create NAME) -> IDENT" (id ident-create))) (p "Returns a fresh identifier associated with the given name."))
(def (sig (procedure "(ident-equal? IDENT IDENT) -> BOOL" (id ident-equal?))) (p "Returns " (tt "#t") " if the stamps of the given identifiers are equal, " (tt "#f") " otherwise."))
(def (sig (procedure "(ident-empty) -> IDENV" (id ident-empty))) (p "Returns an empty identifier environment."))
(def (sig (procedure "(ident-add IDENT DATA IDENV) -> IDENV" (id ident-add))) (p "Adds the given identifier and associated data to the given identifier environment."))
(def (sig (procedure "(ident-find IDENT IDENV) -> DATA" (id ident-find))) (p "Looks up the given identifier in the given identifier environment and returns the associated data, or " (tt "#f") " if not found."))
(def (sig (procedure "(path? X) -> BOOL" (id path?))) (p "Returns " (tt "#t") " if " (tt "X") " is an access path, " (tt "#f") " otherwise."))
(def (sig (procedure "(Pident IDENT) -> PATH" (id Pident))) (p "Returns a path consisting of the given identifier."))
(def (sig (procedure "(Pdot PATH STRING) -> PATH" (id Pdot))) (p "Returns an access path for the given path and field."))
(def (sig (procedure "(path-equal? PATH PATH) -> BOOL" (id path-equal?))) (p "Returns " (tt "#t") " if the two given paths are equal, " (tt "#f") " otherwise."))
(def (sig (procedure "(subst-add IDENT PATH IDENV) -> IDENV" (id subst-add))) (p "Extends the substition environment with the given identifier and path."))
(def (sig (procedure "(subst-path PATH IDENV) -> PATH" (id subst-path))) (p "Applies the given substitutions to the given path."))
(def (sig (procedure "(subst-identity) -> IDENV" (id subst-identity))) (p "Returns an empty substitution environment."))
(def (sig (procedure "(make-core-syntax term? valtype? deftype? kind? make-valtype make-deftype subst-valtype subst-deftype subst-kind)" (id make-core-syntax))) (p "This procedure creates the structure describing base language syntax. The meaning of the fields is as follows:") (ul (li (tt "term?") ": predicate for value expressions") (li (tt "valtype?") ": predicate for type expressions") (li (tt "deftype?") ": predicate for type definitions") (li (tt "kind?") ": predicate for the kinds that a type definition can have") (li (tt "make-valtype") ": constructor for type expressions") (li (tt "make-deftype") ": constructor for type definitions") (li (tt "subst-valtype") ": substitution function for type expressions") (li (tt "subst-deftype") ": substitution function for type definitions") (li (tt "subst-kind") ": substitution function for kinds")))
(def (sig (procedure "(make-mod-syntax core)" (id make-mod-syntax))) (p "This procedure creates the structure describing module language syntax. " (tt "core") " is an object created by " (tt "make-core-syntax") ". This procedure returns multiple values with the following meaning:") (ul (li (tt "modtype?") " " (tt "Signature") " " (tt "Functorty") ": predicate and constructors for module type definitions") (li (tt "modspec?") " " (tt "Value_sig") " " (tt "Type_sig") " " (tt "Module_sig") ": predicate and constructors for module type expressions") (li (tt "modterm?") " " (tt "Modid") " " (tt "Structure") " " (tt "Functor") " " (tt "Mapply") " " (tt "Constraint") ": module term constructors") (li (tt "moddef?") "  " (tt "Value_def") " " (tt "Type_def") " " (tt "Module_def") ": predicate and constructor for module definitions") (li (tt "subst-modtype") " " (tt "subst-modspec") " " (tt "subst-typedecl") ": substitution procedures")))
(def (sig (procedure "(make-core-typing type-term kind-deftype check-valtype check-kind valtype-match deftype-equiv kind-match deftype-of-path)" (id make-core-typing))) (p "This procedure creates the structure describing base language type checking. The meaning of the fields is as follows:") (ul (li (tt "type-term") ": the main typing function, which takes a type and an environment, and returns the principal type of the term in the given environment") (li (tt "kind-deftype") ": infers and returns the kind of the given definable type") (li (tt "check-valtype") " " (tt "check-kind") ": check the well-formedness of type and kind expressions in the base language") (li (tt "valtype-match") " " (tt "deftype-equiv") " " (tt "kind-match") ": checking values vs. signatures") (li (tt "deftype-of-path") ": transforms a type path and its kind into the corresponding definable type")))
(def (sig (procedure "(make-mod-typing core-syntax core-typing)" (id make-mod-typing))) (p "This procedure creates the structure describing module language type checking. " (tt "core-syntax") " is an object created by " (tt "make-core-syntax") ", and " (tt "core-typing") " is an object created by " (tt "make-core-typing") ". This procedure returns multiple values with the following meaning:") (ul (li (tt "check-modtype") ": checks the well-formedness of a module type") (li (tt "check-signature") ": checks the well-formedness of a signature") (li (tt "type-modterm") ": infers and returns the type of a module term") (li (tt "type-moddef") ": infers and returns the type of a module definition (sequence of definitions)") (li (tt "type-definition") ": infers and returns the type of a definition (inside a module or at toplevel)")))
(def (sig (procedure "st-empty" (id st-empty))) (p "Empty scoping table."))
(def (sig (procedure "(st-enter-value ID SC) -> SC" (id st-enter-value))) (p "Enters a value identifier in the given scoping table."))
(def (sig (procedure "(st-enter-type ID SC) -> SC" (id st-enter-type))) (p "Enters a type identifier in the given scoping table."))
(def (sig (procedure "(st-enter-module ID SC) -> SC" (id st-enter-module))) (p "Enters a module identifier in the given scoping table."))
(def (sig (procedure "(st-value-path PATH SC) -> PATH" (id st-value-path))))
(def (sig (procedure "(st-type-path PATH SC) -> PATH" (id st-type-path))))
(def (sig (procedure "(st-module-path PATH SC) -> PATH" (id st-module-path))))
(def (sig (procedure "(st-scope-module PATH SC) -> PATH" (id st-scope-module))))
(def (sig (procedure "(make-mod-eval core-syntax core-eval enter-val)" (id make-mod-eval))) (p "This procedure creates the structure describing module language type checking. " (tt "core-syntax") " is an object created by " (tt "make-core-syntax") ", and " (tt "core-eval") " is a procedure to evalue core syntactic terms. This procedure returns multiple values with the following meaning:") (ul (li (tt "modval?") ": predicate for module values") (li (tt "Structure_v") ": constructor for a structure of values") (li (tt "Mclosure_v") ": constructor for a structure closure") (li (tt "path-find-val") ": given a path and value environment, returns the corresponding value, if it exists in the environment") (li (tt "find-module-val") ": like " (tt "path-find-val") ", but only for modules") (li (tt "mod-eval") ": given an evaluation environment and a list of module definitions, evaluates and returns the corresponding value")))
