package lambdapi
Install
Dune Dependency
Authors
Maintainers
Sources
sha256=d01e5f13db2eaba6e4fe330667149e0059d4886c651ff9d6b672db2dfc9765ed
sha512=33b68c972aca37985ed73c527076198e7d4961c7e27c89cdabfe4d1cff97cd41ccfb85ae9499eb98ad9a0aefd920bc55555df6393fc441ac2429e4d99cddafa8
doc/lambdapi.parsing/Parsing/Syntax/index.html
Module Parsing.SyntaxSource
Parser-level abstract syntax.
Representation of a (located) identifier.
check_notin id ids checks that id does not occur in ids.
check_distinct ids checks that the elements of ids are pairwise distinct.
check_notin_idopts id idopts checks that id does not occur in idopts.
check_distinct_idopts idopts checks that the elements of idopts of the form Some _ are pairwise distinct.
Identifier of a metavariable.
Representation of a module name.
Representation of a possibly qualified (and located) identifier.
Parser-level (located) term representation.
and p_term_aux = | P_Type(*TYPE constant.
*)| P_Iden of p_qident * bool(*Identifier. The boolean indicates whether the identifier is prefixed by "@".
*)| P_Wild(*Underscore.
*)| P_Meta of p_meta_ident * p_term array(*Meta-variable with explicit substitution.
*)| P_Patt of p_ident option * p_term array option(*Pattern.
*)| P_Appl of p_term * p_term(*Application.
*)| P_Arro of p_term * p_term(*Arrow.
*)| P_Abst of p_params list * p_term(*Abstraction.
*)| P_Prod of p_params list * p_term(*Product.
*)| P_LLet of p_ident * p_params list * p_term option * p_term * p_term(*Let.
*)| P_NLit of string(*Natural number literal.
*)| P_Wrap of p_term(*Term between parentheses.
*)| P_Expl of p_term(*Term between curly brackets.
*)
Parser-level representation of a function argument. The boolean is true if the argument is marked as implicit (i.e., between curly braces).
nb_params ps returns the number of parameters in a list of parameters ps.
get_impl_params_list l gives the implicitness of l.
p_get_args t is like Core.Term.get_args but on syntax-level terms. Note that P_Wrap's are not decomposed (important for handling infix symbols used in prefix notation.
pvars_lhs t computes the set of pattern variable names in t, assuming that t is a rule LHS.
Parser-level inductive type representation.
Rewrite patterns as in Coq/SSReflect. See "A Small Scale Reflection Extension for the Coq system", by Georges Gonthier, Assia Mahboubi and Enrico Tassi, INRIA Research Report 6455, 2016,
Parser-level representation of an assertion.
type p_query_aux = | P_query_verbose of string(*Sets the verbosity level.
*)| P_query_debug of bool * string(*Toggles logging functions described by string according to boolean.
*)| P_query_flag of string * bool(*Sets the boolean flag registered under the given name (if any).
*)| P_query_assert of bool * p_assertion(*Assertion (must fail if boolean is
*)true).| P_query_infer of p_term * Core.Eval.strat(*Type inference command.
*)| P_query_normalize of p_term * Core.Eval.strat(*Normalisation command.
*)| P_query_prover of string(*Set the prover to use inside a proof.
*)| P_query_prover_timeout of string(*Set the timeout of the prover (in seconds).
*)| P_query_print of p_qident option(*Print information about a symbol or the current goals.
*)| P_query_proofterm(*Print the current proof term (possibly containing open goals).
*)| P_query_search of string(*Runs a search query
*)
Parser-level representation of a query command.
type p_tactic_aux = | P_tac_admit| P_tac_apply of p_term| P_tac_assume of p_ident option list| P_tac_fail| P_tac_generalize of p_ident| P_tac_have of p_ident * p_term| P_tac_set of p_ident * p_term| P_tac_induction| P_tac_query of p_query| P_tac_refine of p_term| P_tac_refl| P_tac_remove of p_ident list| P_tac_rewrite of bool * p_rw_patt option * p_term| P_tac_simpl of p_qident option| P_tac_solve| P_tac_sym| P_tac_why3 of string option| P_tac_try of p_tactic
Parser-level representation of a tactic.
is_destructive t says whether tactic t changes the current goal.
Parser-level representation of a proof.
type p_modifier_aux = | P_mstrat of Core.Term.match_strat(*pattern matching strategy
*)| P_expo of Core.Term.expo(*visibility of symbol outside its modules
*)| P_prop of Core.Term.prop(*symbol properties: constant, definable, ...
*)| P_opaq(*opacity
*)
Parser-level representation of modifiers.
type p_symbol = {p_sym_mod : p_modifier list;(*modifiers
*)p_sym_nam : p_ident;(*symbol name
*)p_sym_arg : p_params list;(*arguments before ":"
*)p_sym_typ : p_term option;(*symbol type
*)p_sym_trm : p_term option;(*symbol definition
*)p_sym_prf : (p_proof * p_proof_end) option;(*proof script
*)p_sym_def : bool;(*is it a definition ?
*)
}Parser-level representation of symbol declarations.
type p_command_aux = | P_require of bool * p_path list| P_require_as of p_path * p_ident| P_open of p_path list| P_symbol of p_symbol| P_rules of p_rule list| P_inductive of p_modifier list * p_params list * p_inductive list| P_builtin of string * p_qident| P_notation of p_qident * string Core.Sign.notation| P_unif_rule of p_rule| P_coercion of p_rule| P_query of p_query| P_opaque of p_qident
Parser-level representation of a single command.
Parser-level representation of a single (located) command.
Equality functions on the syntactic expressions ignoring positions.
eq_command c1 c2 tells whether c1 and c2 are the same commands. They are compared up to source code positions.
fold_proof f acc p recursively builds a value of type 'a by starting from acc and by applying f to every tactic of p.
fold_idents f a ast allows to recursively build a value of type 'a starting from a and by applying f on each identifier occurring in ast corresponding to a function symbol: variables (term variables or assumption names) are excluded.
NOTE: This function is incomplete if an assumption name hides a function symbol. Example:
symbol A:TYPE; symbol a:A; symbol p:((A->A)->A->A)->A := begin assume h apply h // proof of A->A assume a apply a // here a is an assumption // proof of A apply a // here a is a function symbol end;